diff --git a/thys/Priority_Queue_Braun/Priority_Queue_Braun2.thy b/thys/Priority_Queue_Braun/Priority_Queue_Braun2.thy
--- a/thys/Priority_Queue_Braun/Priority_Queue_Braun2.thy
+++ b/thys/Priority_Queue_Braun/Priority_Queue_Braun2.thy
@@ -1,203 +1,129 @@
 section "Priority Queues Based on Braun Trees 2"
 
 theory Priority_Queue_Braun2
 imports Priority_Queue_Braun
 begin
 
 text \<open>This is the version verified by Jean-Christophe Filliâtre with the help of the Why3 system
 \<^url>\<open>http://toccata.lri.fr/gallery/braun_trees.en.html\<close>.
 Only the deletion function (\<open>del_min2\<close> below) differs from Paulson's version.
 But the difference turns out to be minor --- see below.\<close>
 
-(* TODO mv *)
-lemma neq_Leaf_iff_size: "t \<noteq> Leaf \<longleftrightarrow> size t > 0"
-by (simp add: zero_less_iff_neq_zero)
-
 
 subsection "Function \<open>del_min2\<close>"
 
 fun le_root :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> bool" where
 "le_root a t = (t = Leaf \<or> a \<le> value t)"
 
 fun replace_min :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
 "replace_min x (Node l _ r) =
   (if le_root x l & le_root x r then Node l x r
    else
      let a = value l in
      if le_root a r then Node (replace_min x l) a r
      else Node l (value r) (replace_min x r))"
 
 fun merge :: "'a::linorder tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
 "merge l Leaf = l" |
 "merge (Node l1 a1 r1) (Node l2 a2 r2) =
    (if a1 \<le> a2 then Node (Node l2 a2 r2) a1 (merge l1 r1)
     else let (x, l') = del_left (Node l1 a1 r1)
          in Node (replace_min x (Node l2 a2 r2)) a2 l')"
 
 fun del_min2 where
 "del_min2 Leaf = Leaf" |
 "del_min2 (Node l x r) = merge l r"
 
 
 subsection "Correctness Proof"
 
 text \<open>It turns out that @{const replace_min} is just @{const sift_down} in disguise:\<close>
 
 lemma replace_min_sift_down: "braun (Node l a r) \<Longrightarrow> replace_min x (Node l a r) = sift_down l x r"
 by(induction l x r rule: sift_down.induct)(auto)
 
 text \<open>This means that @{const del_min2} is merely a slight optimization of @{const del_min}:
 instead of calling @{const del_left} right away, @{const merge} can take advantage of the case
 where the smaller element is at the root of the left heap and can be moved up without complications.
 However, on average this is just the case on the first level.\<close>
 
-lemma mset_tree_replace_min:
-  "\<lbrakk> braun t; t \<noteq> Leaf \<rbrakk> \<Longrightarrow>
-  mset_tree(replace_min x t) = (mset_tree t - {#value t#}) + {#x#}"
-by(auto simp add: mset_sift_down neq_Leaf_iff replace_min_sift_down simp del: replace_min.simps)
-(* An explicit proof:
-apply(induction t)
-apply(auto simp: Let_def neq_Leaf_iff_size tree.set_sel(2))
-done
-*)
-
-lemma braun_size_replace_min:
-  "\<lbrakk> braun t; t \<noteq> Leaf \<rbrakk> \<Longrightarrow> braun(replace_min x t) \<and> size(replace_min x t) = size t"
-by(auto simp add: size_sift_down braun_sift_down neq_Leaf_iff replace_min_sift_down
-        simp del: replace_min.simps)
-(* An explicit proof:
-apply(induction t)
-apply(auto simp add: Let_def neq_Leaf_iff_size)
-done
-*)
-(*
-lemma heap_value_least: "\<lbrakk> heap t; x \<le> value t \<rbrakk>
-       \<Longrightarrow> \<forall>a \<in> set_tree t. x \<le> a \<longleftrightarrow> True"
-by (metis Min.boundedE empty_iff finite_set_tree get_min set_mset_tree tree.simps(14))
-*)
-lemma heap_replace_min:
-  "\<lbrakk> braun t; heap t; t \<noteq> Leaf \<rbrakk> \<Longrightarrow> heap(replace_min x t)"
-by(auto simp add: heap_sift_down neq_Leaf_iff replace_min_sift_down simp del: replace_min.simps)
-(* A long explicit proof:
-proof(induction t)
-  case Leaf thus ?case by simp
-next
-  case (Node l a r)
-  have "braun l" "braun r" using Node.prems(1) by auto
-  show ?case
-  proof (cases "le_root x l & le_root x r")
-    case True
-    with Node(4) show ?thesis by(auto dest: heap_value_least)
-  next
-    case False
-    hence "l \<noteq> Leaf" using Node.prems(1) by(auto)
-    show ?thesis
-    proof cases
-      assume "le_root (value l) r"
-      have "value l \<le> x" using False \<open>le_root (value l) r\<close> by auto
-      moreover have "\<forall>a \<in># mset_tree l. value l \<le> a"
-        using Node.prems(2) heap_value_least by auto
-      ultimately have 1: "\<forall>a \<in> set_tree(replace_min x l). value l \<le> a"
-        using mset_tree_replace_min[OF \<open>braun l\<close> \<open>l \<noteq> Leaf\<close>]
-        by(auto simp flip: set_mset_tree dest: in_diffD)
-      have "\<forall>a \<in> set_tree r. value l \<le> a"
-        using Node.prems(2) \<open>le_root (value l) r\<close> heap_value_least by auto
-      thus ?thesis
-        using False \<open>le_root (value l) r\<close> \<open>l \<noteq> Leaf\<close> Node.IH(1)[OF \<open>braun l\<close>] Node.prems(2) 1
-        by (auto)
-    next
-      assume "\<not> le_root (value l) r"
-      hence "r \<noteq> Leaf" "le_root (value r) l" "value r \<le> x" using Node.prems(1) False by(auto)
-      have "\<forall>a \<in># mset_tree r. value r \<le> a"
-        using Node.prems(2) heap_value_least by auto
-      with \<open>value r \<le> x\<close> have 1: "\<forall>a \<in> set_tree(replace_min x r). value r \<le> a"
-        using mset_tree_replace_min[OF \<open>braun r\<close> \<open>r \<noteq> Leaf\<close>]
-        by(auto simp flip: set_mset_tree dest: in_diffD)
-      have "\<forall>x\<in>set_tree l. value r \<le> x"
-        using Node.prems(2) \<open>le_root (value r) l\<close> heap_value_least by auto
-      thus ?thesis
-        using False \<open>\<not> le_root (value l) r\<close> \<open>l \<noteq> Leaf\<close> Node.IH(2)[OF \<open>braun r\<close>] Node.prems(2) 1
-        by (auto)
-    qed
-  qed
-qed
-*)
-
 text \<open>Function @{const merge}:\<close>
 
 lemma mset_tree_merge:
   "braun (Node l x r) \<Longrightarrow> mset_tree(merge l r) = mset_tree l + mset_tree r"
 by(induction l r rule: merge.induct)
-  (auto simp: Let_def mset_tree_replace_min neq_Leaf_iff_size tree.set_sel(2)
-        dest!: del_left_mset split!: prod.split)
+  (auto simp: Let_def tree.set_sel(2) mset_sift_down replace_min_sift_down
+        simp del: replace_min.simps dest!: del_left_mset split!: prod.split)
 
 lemma heap_merge:
   "\<lbrakk> braun (Node l x r); heap l; heap r \<rbrakk> \<Longrightarrow> heap(merge l r)"
 proof(induction l r rule: merge.induct)
   case 1 thus ?case by simp
 next
   case (2 l1 a1 r1 l2 a2 r2)
   show ?case
   proof cases
     assume "a1 \<le> a2"
     thus ?thesis using 2 by(auto simp: ball_Un mset_tree_merge simp flip: set_mset_tree)
   next
     assume "\<not> a1 \<le> a2"
     let ?l = "Node l1 a1 r1" let ?r = "Node l2 a2 r2"
     have "braun ?r" using "2.prems"(1) by auto
     obtain x l' where dl: "del_left ?l = (x, l')" by (metis surj_pair)
     from del_left_heap[OF this _ "2.prems"(2)] have "heap l'" by auto
-    have hr: "heap(replace_min x ?r)" using heap_replace_min[OF \<open>braun ?r\<close> "2.prems"(3)] by simp
+    have hr: "heap(replace_min x ?r)" using \<open>braun ?r\<close> "2.prems"(3)
+      by(simp add: heap_sift_down neq_Leaf_iff replace_min_sift_down del: replace_min.simps)
     have 0: "\<forall>x \<in> set_tree ?l. a2 \<le> x" using "2.prems"(2) \<open>\<not> a1 \<le> a2\<close> by (auto simp: ball_Un)
     moreover have "set_tree l' \<subseteq> set_tree ?l" "x \<in> set_tree ?l"
       using del_left_mset[OF dl] by (auto simp flip: set_mset_tree dest:in_diffD simp: union_iff)
     ultimately have 1: "\<forall>x \<in> set_tree l'. a2 \<le> x" by blast
     have "\<forall>x \<in> set_tree ?r. a2 \<le> x" using \<open>heap ?r\<close> by auto
     thus ?thesis
-      using \<open>\<not> a1 \<le> a2\<close> dl \<open>heap(replace_min x ?r)\<close> \<open>heap l'\<close> \<open>x \<in> set_tree ?l\<close> 0 1
-      by(auto simp: mset_tree_replace_min[OF \<open>braun ?r\<close>] simp flip: set_mset_tree
+      using \<open>\<not> a1 \<le> a2\<close> dl \<open>heap(replace_min x ?r)\<close> \<open>heap l'\<close> \<open>x \<in> set_tree ?l\<close> 0 1 \<open>braun ?r\<close>
+      by(auto simp: mset_sift_down replace_min_sift_down simp flip: set_mset_tree
               simp del: replace_min.simps)
   qed
 next
   case 3 thus ?case by simp
 qed
 
 lemma del_left_braun_size:
   "del_left t = (x,t') \<Longrightarrow> braun t \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> braun t' \<and> size t = size t' + 1"
 by (simp add: del_left_braun del_left_size)
 
 lemma braun_size_merge:
   "braun (Node l x r) \<Longrightarrow> braun(merge l r) \<and> size(merge l r) = size l + size r"
 apply(induction l r rule: merge.induct)
-apply(auto simp: Let_def neq_Leaf_iff_size braun_size_replace_min
+apply(auto simp: size_sift_down braun_sift_down replace_min_sift_down
+           simp del: replace_min.simps
            dest!: del_left_braun_size split!: prod.split)
 done
 
 
 text \<open>Last step: prove all axioms of the priority queue specification:\<close>
 
 interpretation braun: Priority_Queue
 where empty = Leaf and is_empty = "\<lambda>h. h = Leaf"
 and insert = insert and del_min = del_min2
 and get_min = "value" and invar = "\<lambda>h. braun h \<and> heap h"
 and mset = mset_tree
 proof(standard, goal_cases)
   case 1 show ?case by simp
 next
   case 2 show ?case by simp
 next
   case 3 show ?case by(simp add: mset_insert)
 next
   case 4 thus ?case by(auto simp: mset_tree_merge neq_Leaf_iff)
 next
   case 5 thus ?case using get_min mset_tree.simps(1) by blast
 next
   case 6 thus ?case by(simp)
 next
   case 7 thus ?case by(simp add: heap_insert braun_insert)
 next
   case 8 thus ?case by(auto simp: heap_merge braun_size_merge neq_Leaf_iff)
 qed
 
 
 end
diff --git a/thys/Transition_Systems_and_Automata/Automata/NBA/NBA_Combine.thy b/thys/Transition_Systems_and_Automata/Automata/NBA/NBA_Combine.thy
--- a/thys/Transition_Systems_and_Automata/Automata/NBA/NBA_Combine.thy
+++ b/thys/Transition_Systems_and_Automata/Automata/NBA/NBA_Combine.thy
@@ -1,77 +1,88 @@
 section \<open>Nondeterministic Büchi Automata Combinations\<close>
 
 theory NBA_Combine
 imports NBA NGBA
 begin
 
   global_interpretation degeneralization: automaton_degeneralization_trace
     ngba ngba.alphabet ngba.initial ngba.transition ngba.accepting "gen infs"
     nba nba.alphabet nba.initial nba.transition nba.accepting infs
     defines degeneralize = degeneralization.degeneralize
     by unfold_locales auto
 
   lemmas degeneralize_language[simp] = degeneralization.degeneralize_language[folded NBA.language_def]
   lemmas degeneralize_nodes_finite[iff] = degeneralization.degeneralize_nodes_finite[folded NBA.nodes_def]
 
   global_interpretation intersection: automaton_intersection_trace
     nba nba.alphabet nba.initial nba.transition nba.accepting infs
     nba nba.alphabet nba.initial nba.transition nba.accepting infs
     ngba ngba.alphabet ngba.initial ngba.transition ngba.accepting "gen infs"
     "\<lambda> c\<^sub>1 c\<^sub>2. [c\<^sub>1 \<circ> fst, c\<^sub>2 \<circ> snd]"
     defines intersect' = intersection.intersect
     by unfold_locales auto
 
   lemmas intersect'_language[simp] = intersection.intersect_language[folded NGBA.language_def]
   lemmas intersect'_nodes_finite[intro] = intersection.intersect_nodes_finite[folded NGBA.nodes_def]
 
   global_interpretation intersection_list: automaton_intersection_list_trace
     nba nba.alphabet nba.initial nba.transition nba.accepting infs
     ngba ngba.alphabet ngba.initial ngba.transition ngba.accepting "gen infs"
     "\<lambda> cs. map (\<lambda> k pp. (cs ! k) (pp ! k)) [0 ..< length cs]"
     defines intersect_list' = intersection_list.intersect
   proof unfold_locales
     fix cs :: "('b \<Rightarrow> bool) list" and ws :: "'b stream list"
     assume 1: "length cs = length ws"
     have "gen infs (map (\<lambda> k pp. (cs ! k) (pp ! k)) [0 ..< length cs]) (stranspose ws) \<longleftrightarrow>
       (\<forall> k < length cs. infs (\<lambda> pp. (cs ! k) (pp ! k)) (stranspose ws))"
       by (auto simp: gen_def)
     also have "\<dots> \<longleftrightarrow> (\<forall> k < length cs. infs (cs ! k) (smap (\<lambda> pp. pp ! k) (stranspose ws)))"
       by (simp add: comp_def)
     also have "\<dots> \<longleftrightarrow> (\<forall> k < length cs. infs (cs ! k) (ws ! k))" using 1 by simp
     also have "\<dots> \<longleftrightarrow> list_all2 infs cs ws" using 1 unfolding list_all2_conv_all_nth by simp
     finally show "gen infs (map (\<lambda> k pp. (cs ! k) (pp ! k)) [0 ..< length cs]) (stranspose ws) \<longleftrightarrow>
       list_all2 infs cs ws" by this
   qed
 
   lemmas intersect_list'_language[simp] = intersection_list.intersect_language[folded NGBA.language_def]
   lemmas intersect_list'_nodes_finite[intro] = intersection_list.intersect_nodes_finite[folded NGBA.nodes_def]
 
   global_interpretation union: automaton_union_trace
     nba nba.alphabet nba.initial nba.transition nba.accepting infs
     nba nba.alphabet nba.initial nba.transition nba.accepting infs
     nba nba.alphabet nba.initial nba.transition nba.accepting infs
     case_sum
     defines union = union.union
     by (unfold_locales) (auto simp: comp_def)
 
   lemmas union_language = union.union_language
+  lemmas union_nodes_finite = union.union_nodes_finite
+
+  global_interpretation union_list: automaton_union_list_trace
+    nba nba.alphabet nba.initial nba.transition nba.accepting infs
+    nba nba.alphabet nba.initial nba.transition nba.accepting infs
+    "\<lambda> cs (k, p). (cs ! k) p"
+    defines union_list = union_list.union
+    by (unfold_locales) (auto simp: szip_sconst_smap_fst comp_def)
+
+  lemmas union_list_language = union_list.union_language
+  lemmas union_list_nodes_finite = union_list.union_nodes_finite
 
   abbreviation intersect where "intersect A B \<equiv> degeneralize (intersect' A B)"
 
   lemma intersect_language[simp]: "NBA.language (intersect A B) = NBA.language A \<inter> NBA.language B"
     by simp
   lemma intersect_nodes_finite[intro]:
     assumes "finite (NBA.nodes A)" "finite (NBA.nodes B)"
     shows "finite (NBA.nodes (intersect A B))"
     using intersect'_nodes_finite assms by simp
 
   abbreviation intersect_list where "intersect_list AA \<equiv> degeneralize (intersect_list' AA)"
 
   lemma intersect_list_language[simp]: "NBA.language (intersect_list AA) = \<Inter> (NBA.language ` set AA)"
     by simp
   lemma intersect_list_nodes_finite[intro]:
     assumes "list_all (finite \<circ> NBA.nodes) AA"
     shows "finite (NBA.nodes (intersect_list AA))"
     using intersect_list'_nodes_finite assms by simp
 
 end
\ No newline at end of file
diff --git a/thys/Transition_Systems_and_Automata/Automata/Nondeterministic.thy b/thys/Transition_Systems_and_Automata/Automata/Nondeterministic.thy
--- a/thys/Transition_Systems_and_Automata/Automata/Nondeterministic.thy
+++ b/thys/Transition_Systems_and_Automata/Automata/Nondeterministic.thy
@@ -1,612 +1,746 @@
 theory Nondeterministic
 imports
   "../Transition_Systems/Transition_System"
   "../Transition_Systems/Transition_System_Extra"
   "../Transition_Systems/Transition_System_Construction"
   "../Basic/Degeneralization"
 begin
 
   type_synonym ('label, 'state) trans = "'label \<Rightarrow> 'state \<Rightarrow> 'state set"
 
   locale automaton =
     fixes automaton :: "'label set \<Rightarrow> 'state set \<Rightarrow> ('label, 'state) trans \<Rightarrow> 'condition \<Rightarrow> 'automaton"
     fixes alphabet :: "'automaton \<Rightarrow> 'label set"
     fixes initial :: "'automaton \<Rightarrow> 'state set"
     fixes transition :: "'automaton \<Rightarrow> ('label, 'state) trans"
     fixes condition :: "'automaton \<Rightarrow> 'condition"
     assumes automaton[simp]: "automaton (alphabet A) (initial A) (transition A) (condition A) = A"
     assumes alphabet[simp]: "alphabet (automaton a i t c) = a"
     assumes initial[simp]: "initial (automaton a i t c) = i"
     assumes transition[simp]: "transition (automaton a i t c) = t"
     assumes condition[simp]: "condition (automaton a i t c) = c"
   begin
 
     sublocale transition_system_initial
       "\<lambda> a p. snd a" "\<lambda> a p. fst a \<in> alphabet A \<and> snd a \<in> transition A (fst a) p" "\<lambda> p. p \<in> initial A"
       for A
       defines path' = path and run' = run and reachable' = reachable and nodes' = nodes
       by this
 
     lemma states_alt_def: "states r p = map snd r" by (induct r arbitrary: p) (auto)
     lemma trace_alt_def: "trace r p = smap snd r" by (coinduction arbitrary: r p) (auto)
 
     lemma successors_alt_def: "successors A p = (\<Union> a \<in> alphabet A. transition A a p)" by auto
 
     lemma reachable_transition[intro]:
       assumes "a \<in> alphabet A" "q \<in> reachable A p" "r \<in> transition A a q"
       shows "r \<in> reachable A p"
       using reachable.execute assms by force
     lemma nodes_transition[intro]:
       assumes "a \<in> alphabet A" "p \<in> nodes A" "q \<in> transition A a p"
       shows "q \<in> nodes A"
       using nodes.execute assms by force
 
     definition restrict :: "'automaton \<Rightarrow> 'automaton" where
       "restrict A \<equiv> automaton
         (alphabet A)
         (initial A)
         (\<lambda> a p. if a \<in> alphabet A then transition A a p else {})
         (condition A)"
 
     lemma restrict_simps[simp]:
       "alphabet (restrict A) = alphabet A"
       "initial (restrict A) = initial A"
       "transition (restrict A) a p = (if a \<in> alphabet A then transition A a p else {})"
       "condition (restrict A) = condition A"
       unfolding restrict_def by auto
 
     lemma restrict_path[simp]: "path (restrict A) = path A"
     proof (intro ext iffI)
       show "path A wr p" if "path (restrict A) wr p" for wr p using that by induct auto
       show "path (restrict A) wr p" if "path A wr p" for wr p using that by induct auto
     qed
     lemma restrict_run[simp]: "run (restrict A) = run A"
     proof (intro ext iffI)
       show "run A wr p" if "run (restrict A) wr p" for wr p using that by coinduct auto
       show "run (restrict A) wr p" if "run A wr p" for wr p using that by coinduct auto
     qed
 
   end
 
   (* TODO: create analogous thing for NFAs (automaton_target) *)
   locale automaton_trace =
     automaton automaton alphabet initial transition condition
     for automaton :: "'label set \<Rightarrow> 'state set \<Rightarrow> ('label, 'state) trans \<Rightarrow> 'condition \<Rightarrow> 'automaton"
     and alphabet :: "'automaton \<Rightarrow> 'label set"
     and initial :: "'automaton \<Rightarrow> 'state set"
     and transition :: "'automaton \<Rightarrow> ('label, 'state) trans"
     and condition :: "'automaton \<Rightarrow> 'condition"
     +
     fixes test :: "'condition \<Rightarrow> 'state stream \<Rightarrow> bool"
   begin
 
     definition language :: "'automaton \<Rightarrow> 'label stream set" where
       "language A \<equiv> {w |w r p. p \<in> initial A \<and> run A (w ||| r) p \<and> test (condition A) (trace (w ||| r) p)}"
 
     lemma language[intro]:
       assumes "p \<in> initial A" "run A (w ||| r) p" "test (condition A) (trace (w ||| r) p)"
       shows "w \<in> language A"
       using assms unfolding language_def by auto
     lemma language_elim[elim]:
       assumes "w \<in> language A"
       obtains r p
       where "p \<in> initial A" "run A (w ||| r) p" "test (condition A) (trace (w ||| r) p)"
       using assms unfolding language_def by auto
 
     lemma run_alphabet:
       assumes "run A (w ||| r) p"
       shows "w \<in> streams (alphabet A)"
       using assms by (coinduction arbitrary: w r p) (metis run.cases stream.map szip_smap szip_smap_fst)
     lemma language_alphabet: "language A \<subseteq> streams (alphabet A)"
       unfolding language_def by (auto dest: run_alphabet)
 
     lemma restrict_language[simp]: "language (restrict A) = language A" by force
 
   end
 
   locale automaton_degeneralization =
     a: automaton automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 +
     b: automaton automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2
     for automaton\<^sub>1 :: "'label set \<Rightarrow> 'state set \<Rightarrow> ('label, 'state) trans \<Rightarrow> 'state pred gen \<Rightarrow> 'automaton\<^sub>1"
     and alphabet\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'label set"
     and initial\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'state set"
     and transition\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> ('label, 'state) trans"
     and condition\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'state pred gen"
     and automaton\<^sub>2 :: "'label set \<Rightarrow> 'state degen set \<Rightarrow> ('label, 'state degen) trans \<Rightarrow> 'state degen pred \<Rightarrow> 'automaton\<^sub>2"
     and alphabet\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'label set"
     and initial\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'state degen set"
     and transition\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> ('label, 'state degen) trans"
     and condition\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'state degen pred"
   begin
 
     definition degeneralize :: "'automaton\<^sub>1 \<Rightarrow> 'automaton\<^sub>2" where
       "degeneralize A \<equiv> automaton\<^sub>2
         (alphabet\<^sub>1 A)
         (initial\<^sub>1 A \<times> {0})
         (\<lambda> a (p, k). transition\<^sub>1 A a p \<times> {count (condition\<^sub>1 A) p k})
         (degen (condition\<^sub>1 A))"
 
     lemma degeneralize_simps[simp]:
       "alphabet\<^sub>2 (degeneralize A) = alphabet\<^sub>1 A"
       "initial\<^sub>2 (degeneralize A) = initial\<^sub>1 A \<times> {0}"
       "transition\<^sub>2 (degeneralize A) a (p, k) = transition\<^sub>1 A a p \<times> {count (condition\<^sub>1 A) p k}"
       "condition\<^sub>2 (degeneralize A) = degen (condition\<^sub>1 A)"
       unfolding degeneralize_def by auto
 
     lemma run_degeneralize:
       assumes "a.run A (w ||| r) p"
       shows "b.run (degeneralize A) (w ||| r ||| sscan (count (condition\<^sub>1 A)) (p ## r) k) (p, k)"
       using assms by (coinduction arbitrary: w r p k) (force elim: a.run.cases)
     lemma degeneralize_run:
       assumes "b.run (degeneralize A) (w ||| rs) pk"
       obtains r s p k
       where "rs = r ||| s" "pk = (p, k)" "a.run A (w ||| r) p" "s = sscan (count (condition\<^sub>1 A)) (p ## r) k"
     proof
       show "rs = smap fst rs ||| smap snd rs" "pk = (fst pk, snd pk)" by auto
       show "a.run A (w ||| smap fst rs) (fst pk)"
         using assms by (coinduction arbitrary: w rs pk) (force elim: b.run.cases)
       show "smap snd rs = sscan (count (condition\<^sub>1 A)) (fst pk ## smap fst rs) (snd pk)"
         using assms by (coinduction arbitrary: w rs pk) (force elim: b.run.cases)
     qed
 
     lemma degeneralize_nodes:
       "b.nodes (degeneralize A) \<subseteq> a.nodes A \<times> insert 0 {0 ..< length (condition\<^sub>1 A)}"
     proof
       fix pk
       assume "pk \<in> b.nodes (degeneralize A)"
       then show "pk \<in> a.nodes A \<times> insert 0 {0 ..< length (condition\<^sub>1 A)}"
         by (induct) (force, cases "condition\<^sub>1 A = []", auto)
     qed
     lemma nodes_degeneralize: "a.nodes A \<subseteq> fst ` b.nodes (degeneralize A)"
     proof
       fix p
       assume "p \<in> a.nodes A"
       then show "p \<in> fst ` b.nodes (degeneralize A)"
       proof induct
         case (initial p)
         have "(p, 0) \<in> b.nodes (degeneralize A)" using initial by auto
         then show ?case using image_iff fst_conv by force
       next
         case (execute p aq)
         obtain k where "(p, k) \<in> b.nodes (degeneralize A)" using execute(2) by auto
         then have "(snd aq, count (condition\<^sub>1 A) p k) \<in> b.nodes (degeneralize A)"
           using execute(3) by auto
         then show ?case using image_iff snd_conv by force
       qed
     qed
 
     lemma degeneralize_nodes_finite[iff]: "finite (b.nodes (degeneralize A)) \<longleftrightarrow> finite (a.nodes A)"
     proof
       show "finite (a.nodes A)" if "finite (b.nodes (degeneralize A))"
         using finite_subset nodes_degeneralize that by blast
       show "finite (b.nodes (degeneralize A))" if "finite (a.nodes A)"
         using finite_subset degeneralize_nodes that by blast
     qed
 
   end
 
   locale automaton_degeneralization_trace =
     automaton_degeneralization
       automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1
       automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 +
     a: automaton_trace automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 +
     b: automaton_trace automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2
     for automaton\<^sub>1 :: "'label set \<Rightarrow> 'state set \<Rightarrow> ('label, 'state) trans \<Rightarrow> 'state pred gen \<Rightarrow> 'automaton\<^sub>1"
     and alphabet\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'label set"
     and initial\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'state set"
     and transition\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> ('label, 'state) trans"
     and condition\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'state pred gen"
     and test\<^sub>1 :: "'state pred gen \<Rightarrow> 'state stream \<Rightarrow> bool"
     and automaton\<^sub>2 :: "'label set \<Rightarrow> 'state degen set \<Rightarrow> ('label, 'state degen) trans \<Rightarrow> 'state degen pred \<Rightarrow> 'automaton\<^sub>2"
     and alphabet\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'label set"
     and initial\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'state degen set"
     and transition\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> ('label, 'state degen) trans"
     and condition\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'state degen pred"
     and test\<^sub>2 :: "'state degen pred \<Rightarrow> 'state degen stream \<Rightarrow> bool"
     +
     assumes test[iff]: "test\<^sub>2 (degen cs) (r ||| sscan (count cs) (p ## r) k) \<longleftrightarrow> test\<^sub>1 cs r"
   begin
 
     lemma degeneralize_language[simp]: "b.language (degeneralize A) = a.language A"
       unfolding a.language_def b.language_def
       unfolding a.trace_alt_def b.trace_alt_def
       by (auto dest: run_degeneralize elim!: degeneralize_run)
 
   end
 
   locale automaton_intersection =
     a: automaton automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 +
     b: automaton automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 +
     c: automaton automaton\<^sub>3 alphabet\<^sub>3 initial\<^sub>3 transition\<^sub>3 condition\<^sub>3
     for automaton\<^sub>1 :: "'label set \<Rightarrow> 'state\<^sub>1 set \<Rightarrow> ('label, 'state\<^sub>1) trans \<Rightarrow> 'condition\<^sub>1 \<Rightarrow> 'automaton\<^sub>1"
     and alphabet\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'label set"
     and initial\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'state\<^sub>1 set"
     and transition\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> ('label, 'state\<^sub>1) trans"
     and condition\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'condition\<^sub>1"
     and automaton\<^sub>2 :: "'label set \<Rightarrow> 'state\<^sub>2 set \<Rightarrow> ('label, 'state\<^sub>2) trans \<Rightarrow> 'condition\<^sub>2 \<Rightarrow> 'automaton\<^sub>2"
     and alphabet\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'label set"
     and initial\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'state\<^sub>2 set"
     and transition\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> ('label, 'state\<^sub>2) trans"
     and condition\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'condition\<^sub>2"
     and automaton\<^sub>3 :: "'label set \<Rightarrow> ('state\<^sub>1 \<times> 'state\<^sub>2) set \<Rightarrow> ('label, 'state\<^sub>1 \<times> 'state\<^sub>2) trans \<Rightarrow>
       'condition\<^sub>3 \<Rightarrow> 'automaton\<^sub>3"
     and alphabet\<^sub>3 :: "'automaton\<^sub>3 \<Rightarrow> 'label set"
     and initial\<^sub>3 :: "'automaton\<^sub>3 \<Rightarrow> ('state\<^sub>1 \<times> 'state\<^sub>2) set"
     and transition\<^sub>3 :: "'automaton\<^sub>3 \<Rightarrow> ('label, 'state\<^sub>1 \<times> 'state\<^sub>2) trans"
     and condition\<^sub>3 :: "'automaton\<^sub>3 \<Rightarrow> 'condition\<^sub>3"
     +
     fixes condition :: "'condition\<^sub>1 \<Rightarrow> 'condition\<^sub>2 \<Rightarrow> 'condition\<^sub>3"
   begin
 
     definition intersect :: "'automaton\<^sub>1 \<Rightarrow> 'automaton\<^sub>2 \<Rightarrow> 'automaton\<^sub>3" where
       "intersect A B \<equiv> automaton\<^sub>3
         (alphabet\<^sub>1 A \<inter> alphabet\<^sub>2 B)
         (initial\<^sub>1 A \<times> initial\<^sub>2 B)
         (\<lambda> a (p, q). transition\<^sub>1 A a p \<times> transition\<^sub>2 B a q)
         (condition (condition\<^sub>1 A) (condition\<^sub>2 B))"
 
     lemma intersect_simps[simp]:
       "alphabet\<^sub>3 (intersect A B) = alphabet\<^sub>1 A \<inter> alphabet\<^sub>2 B"
       "initial\<^sub>3 (intersect A B) = initial\<^sub>1 A \<times> initial\<^sub>2 B"
       "transition\<^sub>3 (intersect A B) a (p, q) = transition\<^sub>1 A a p \<times> transition\<^sub>2 B a q"
       "condition\<^sub>3 (intersect A B) = condition (condition\<^sub>1 A) (condition\<^sub>2 B)"
       unfolding intersect_def by auto
 
     lemma intersect_path[iff]:
       assumes "length w = length r" "length r = length s"
       shows "c.path (intersect A B) (w || r || s) (p, q) \<longleftrightarrow>
         a.path A (w || r) p \<and> b.path B (w || s) q"
       using assms by (induct arbitrary: p q rule: list_induct3) (auto)
     lemma intersect_run[iff]: "c.run (intersect A B) (w ||| r ||| s) (p, q) \<longleftrightarrow>
       a.run A (w ||| r) p \<and> b.run B (w ||| s) q"
     proof safe
       show "a.run A (w ||| r) p" if "c.run (intersect A B) (w ||| r ||| s) (p, q)"
         using that by (coinduction arbitrary: w r s p q) (force elim: c.run.cases)
       show "b.run B (w ||| s) q" if "c.run (intersect A B) (w ||| r ||| s) (p, q)"
         using that by (coinduction arbitrary: w r s p q) (force elim: c.run.cases)
       show "c.run (intersect A B) (w ||| r ||| s) (p, q)" if "a.run A (w ||| r) p" "b.run B (w ||| s) q"
         using that by (coinduction arbitrary: w r s p q) (auto elim: a.run.cases b.run.cases)
     qed
 
     lemma intersect_nodes: "c.nodes (intersect A B) \<subseteq> a.nodes A \<times> b.nodes B"
     proof
       fix pq
       assume "pq \<in> c.nodes (intersect A B)"
       then show "pq \<in> a.nodes A \<times> b.nodes B" by induct auto
     qed
 
     lemma intersect_nodes_finite[intro]:
       assumes "finite (a.nodes A)" "finite (b.nodes B)"
       shows "finite (c.nodes (intersect A B))"
       using finite_subset intersect_nodes assms by blast
 
   end
 
   locale automaton_intersection_trace =
     automaton_intersection
       automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1
       automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2
       automaton\<^sub>3 alphabet\<^sub>3 initial\<^sub>3 transition\<^sub>3 condition\<^sub>3 condition +
     a: automaton_trace automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 +
     b: automaton_trace automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2 +
     c: automaton_trace automaton\<^sub>3 alphabet\<^sub>3 initial\<^sub>3 transition\<^sub>3 condition\<^sub>3 test\<^sub>3
     for automaton\<^sub>1 :: "'label set \<Rightarrow> 'state\<^sub>1 set \<Rightarrow> ('label, 'state\<^sub>1) trans \<Rightarrow> 'condition\<^sub>1 \<Rightarrow> 'automaton\<^sub>1"
     and alphabet\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'label set"
     and initial\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'state\<^sub>1 set"
     and transition\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> ('label, 'state\<^sub>1) trans"
     and condition\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'condition\<^sub>1"
     and test\<^sub>1 :: "'condition\<^sub>1 \<Rightarrow> 'state\<^sub>1 stream \<Rightarrow> bool"
     and automaton\<^sub>2 :: "'label set \<Rightarrow> 'state\<^sub>2 set \<Rightarrow> ('label, 'state\<^sub>2) trans \<Rightarrow> 'condition\<^sub>2 \<Rightarrow> 'automaton\<^sub>2"
     and alphabet\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'label set"
     and initial\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'state\<^sub>2 set"
     and transition\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> ('label, 'state\<^sub>2) trans"
     and condition\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'condition\<^sub>2"
     and test\<^sub>2 :: "'condition\<^sub>2 \<Rightarrow> 'state\<^sub>2 stream \<Rightarrow> bool"
     and automaton\<^sub>3 :: "'label set \<Rightarrow> ('state\<^sub>1 \<times> 'state\<^sub>2) set \<Rightarrow> ('label, 'state\<^sub>1 \<times> 'state\<^sub>2) trans \<Rightarrow>
       'condition\<^sub>3 \<Rightarrow> 'automaton\<^sub>3"
     and alphabet\<^sub>3 :: "'automaton\<^sub>3 \<Rightarrow> 'label set"
     and initial\<^sub>3 :: "'automaton\<^sub>3 \<Rightarrow> ('state\<^sub>1 \<times> 'state\<^sub>2) set"
     and transition\<^sub>3 :: "'automaton\<^sub>3 \<Rightarrow> ('label, 'state\<^sub>1 \<times> 'state\<^sub>2) trans"
     and condition\<^sub>3 :: "'automaton\<^sub>3 \<Rightarrow> 'condition\<^sub>3"
     and test\<^sub>3 :: "'condition\<^sub>3 \<Rightarrow> ('state\<^sub>1 \<times> 'state\<^sub>2) stream \<Rightarrow> bool"
     and condition :: "'condition\<^sub>1 \<Rightarrow> 'condition\<^sub>2 \<Rightarrow> 'condition\<^sub>3"
     +
     assumes test[iff]: "test\<^sub>3 (condition c\<^sub>1 c\<^sub>2) (u ||| v) \<longleftrightarrow> test\<^sub>1 c\<^sub>1 u \<and> test\<^sub>2 c\<^sub>2 v"
   begin
 
     lemma intersect_language[simp]: "c.language (intersect A B) = a.language A \<inter> b.language B"
       unfolding a.language_def b.language_def c.language_def
       unfolding a.trace_alt_def b.trace_alt_def c.trace_alt_def
       by (fastforce iff: split_szip)
 
   end
 
   locale automaton_intersection_list =
     a: automaton automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 +
     b: automaton automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2
     for automaton\<^sub>1 :: "'label set \<Rightarrow> 'state set \<Rightarrow> ('label, 'state) trans \<Rightarrow> 'condition\<^sub>1 \<Rightarrow> 'automaton\<^sub>1"
     and alphabet\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'label set"
     and initial\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'state set"
     and transition\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> ('label, 'state) trans"
     and condition\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'condition\<^sub>1"
     and automaton\<^sub>2 :: "'label set \<Rightarrow> 'state list set \<Rightarrow> ('label, 'state list) trans \<Rightarrow> 'condition\<^sub>2 \<Rightarrow> 'automaton\<^sub>2"
     and alphabet\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'label set"
     and initial\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'state list set"
     and transition\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> ('label, 'state list) trans"
     and condition\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'condition\<^sub>2"
     +
     fixes condition :: "'condition\<^sub>1 list \<Rightarrow> 'condition\<^sub>2"
   begin
 
     definition intersect :: "'automaton\<^sub>1 list \<Rightarrow> 'automaton\<^sub>2" where
       "intersect AA \<equiv> automaton\<^sub>2
         (\<Inter> (alphabet\<^sub>1 ` set AA))
         (listset (map initial\<^sub>1 AA))
         (\<lambda> a pp. listset (map2 (\<lambda> A p. transition\<^sub>1 A a p) AA pp))
         (condition (map condition\<^sub>1 AA))"
 
     lemma intersect_simps[simp]:
       "alphabet\<^sub>2 (intersect AA) = \<Inter> (alphabet\<^sub>1 ` set AA)"
       "initial\<^sub>2 (intersect AA) = listset (map initial\<^sub>1 AA)"
       "transition\<^sub>2 (intersect AA) a pp = listset (map2 (\<lambda> A p. transition\<^sub>1 A a p) AA pp)"
       "condition\<^sub>2 (intersect AA) = condition (map condition\<^sub>1 AA)"
       unfolding intersect_def by auto
 
     lemma intersect_run_length:
       assumes "length pp = length AA"
       assumes "b.run (intersect AA) (w ||| r) pp"
       assumes "qq \<in> sset r"
       shows "length qq = length AA"
     proof -
       have "pred_stream (\<lambda> qq. length qq = length AA) r"
         using assms(1, 2) by (coinduction arbitrary: w r pp)
           (force elim: b.run.cases simp: listset_member list_all2_conv_all_nth)
       then show ?thesis using assms(3) unfolding stream.pred_set by auto
     qed
     lemma intersect_run_stranspose:
       assumes "length pp = length AA"
       assumes "b.run (intersect AA) (w ||| r) pp"
       obtains rr where "r = stranspose rr" "length rr = length AA"
     proof
       define rr where "rr \<equiv> map (\<lambda> k. smap (\<lambda> pp. pp ! k) r) [0 ..< length AA]"
       have "length qq = length AA" if "qq \<in> sset r" for qq using intersect_run_length assms that by this
       then show "r = stranspose rr"
         unfolding rr_def by (coinduction arbitrary: r) (auto intro: nth_equalityI simp: comp_def)
       show "length rr = length AA" unfolding rr_def by auto
     qed
 
     lemma intersect_run:
       assumes "length rr = length AA" "length pp = length AA"
       assumes "\<And> k. k < length AA \<Longrightarrow> a.run (AA ! k) (w ||| rr ! k) (pp ! k)"
       shows "b.run (intersect AA) (w ||| stranspose rr) pp"
     using assms
     proof (coinduction arbitrary: w rr pp)
       case (run ap r)
       then show ?case
       proof (intro conjI exI)
         show "fst ap \<in> alphabet\<^sub>2 (intersect AA)"
           using run by (force elim: a.run.cases simp: set_conv_nth)
         show "snd ap \<in> transition\<^sub>2 (intersect AA) (fst ap) pp"
           using run by (force elim: a.run.cases simp: listset_member list_all2_conv_all_nth)
         show "\<forall> k < length AA. a.run' (AA ! k) (stl w ||| map stl rr ! k) (map shd rr ! k)"
           using run by (force elim: a.run.cases)
       qed auto
     qed
     lemma intersect_run_elim:
       assumes "length rr = length AA" "length pp = length AA"
       assumes "b.run (intersect AA) (w ||| stranspose rr) pp"
       shows "k < length AA \<Longrightarrow> a.run (AA ! k) (w ||| rr ! k) (pp ! k)"
     using assms
     proof (coinduction arbitrary: w rr pp)
       case (run ap wr)
       then show ?case
       proof (intro exI conjI)
         show "fst ap \<in> alphabet\<^sub>1 (AA ! k)"
           using run by (force elim: b.run.cases)
         show "snd ap \<in> transition\<^sub>1 (AA ! k) (fst ap) (pp ! k)"
           using run by (force elim: b.run.cases simp: listset_member list_all2_conv_all_nth)
         show "b.run' (intersect AA) (stl w ||| stranspose (map stl rr)) (shd (stranspose rr))"
           using run by (force elim: b.run.cases)
       qed auto
     qed
 
     lemma intersect_nodes: "b.nodes (intersect AA) \<subseteq> listset (map a.nodes AA)"
     proof
       show "pp \<in> listset (map a.nodes AA)" if "pp \<in> b.nodes (intersect AA)" for pp
         using that by (induct) (auto 0 3 simp: listset_member list_all2_conv_all_nth)
     qed
 
     lemma intersect_nodes_finite[intro]:
       assumes "list_all (finite \<circ> a.nodes) AA"
       shows "finite (b.nodes (intersect AA))"
     proof (rule finite_subset)
       show "b.nodes (intersect AA) \<subseteq> listset (map a.nodes AA)" using intersect_nodes by this
       show "finite (listset (map a.nodes AA))" using list.pred_map assms by auto
     qed
 
   end
 
   locale automaton_intersection_list_trace =
     automaton_intersection_list
       automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1
       automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 condition +
     a: automaton_trace automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 +
     b: automaton_trace automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2
     for automaton\<^sub>1 :: "'label set \<Rightarrow> 'state set \<Rightarrow> ('label, 'state) trans \<Rightarrow> 'condition\<^sub>1 \<Rightarrow> 'automaton\<^sub>1"
     and alphabet\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'label set"
     and initial\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'state set"
     and transition\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> ('label, 'state) trans"
     and condition\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'condition\<^sub>1"
     and test\<^sub>1 :: "'condition\<^sub>1 \<Rightarrow> 'state stream \<Rightarrow> bool"
     and automaton\<^sub>2 :: "'label set \<Rightarrow> 'state list set \<Rightarrow> ('label, 'state list) trans \<Rightarrow> 'condition\<^sub>2 \<Rightarrow> 'automaton\<^sub>2"
     and alphabet\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'label set"
     and initial\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'state list set"
     and transition\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> ('label, 'state list) trans"
     and condition\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'condition\<^sub>2"
     and test\<^sub>2 :: "'condition\<^sub>2 \<Rightarrow> 'state list stream \<Rightarrow> bool"
     and condition :: "'condition\<^sub>1 list \<Rightarrow> 'condition\<^sub>2"
     +
     assumes test[iff]: "length cs = length ws \<Longrightarrow> test\<^sub>2 (condition cs) (stranspose ws) \<longleftrightarrow> list_all2 test\<^sub>1 cs ws"
   begin
 
     lemma intersect_language[simp]: "b.language (intersect AA) = \<Inter> (a.language ` set AA)"
     proof safe
       fix A w
       assume 1: "w \<in> b.language (intersect AA)" "A \<in> set AA"
       obtain r pp where 2:
         "pp \<in> initial\<^sub>2 (intersect AA)"
         "b.run (intersect AA) (w ||| r) pp"
         "test\<^sub>2 (condition\<^sub>2 (intersect AA)) r"
         using 1(1) unfolding b.language_def b.trace_alt_def by auto
       have 3: "length pp = length AA" using 2(1) by (simp add: listset_member list_all2_conv_all_nth)
       obtain rr where 4: "r = stranspose rr" "length rr = length AA"
         using intersect_run_stranspose 3 2(2) by blast
       obtain k where 5: "k < length AA" "A = AA ! k" using 1(2) unfolding set_conv_nth by auto
       show "w \<in> a.language A"
       proof
         show "pp ! k \<in> initial\<^sub>1 A" using 2(1) 5 by (auto simp: listset_member list_all2_conv_all_nth)
         show "a.run A (w ||| rr ! k) (pp ! k)" using intersect_run_elim 2(2) 3 4 5 by auto
         show "test\<^sub>1 (condition\<^sub>1 A) (a.trace (w ||| rr ! k) (pp ! k))"
           using 2(3) 4 5 unfolding a.trace_alt_def by (force simp: list_all2_iff set_conv_nth)
       qed
     next
       fix w
       assume 1: "w \<in> \<Inter> (a.language ` set AA)"
       have 2: "\<forall> A \<in> set AA. \<exists> r p. p \<in> initial\<^sub>1 A \<and> a.run A (w ||| r) p \<and> test\<^sub>1 (condition\<^sub>1 A) r"
         using 1 unfolding a.language_def a.trace_alt_def by auto
       obtain rr pp where 3:
         "length rr = length AA" "length pp = length AA"
         "\<And> k. k < length AA \<Longrightarrow> pp ! k \<in> initial\<^sub>1 (AA ! k)"
         "\<And> k. k < length AA \<Longrightarrow> a.run (AA ! k) (w ||| rr ! k) (pp ! k)"
         "\<And> k. k < length AA \<Longrightarrow> test\<^sub>1 (condition\<^sub>1 (AA ! k)) (rr ! k)"
         using 2
         unfolding Ball_set list_choice_zip list_choice_pair
         unfolding list.pred_set set_conv_nth
         by force
       show "w \<in> b.language (intersect AA)"
       proof
         show "pp \<in> initial\<^sub>2 (intersect AA)"
           using 3 by (force simp: listset_member list_all2_iff set_conv_nth)
         show "b.run (intersect AA) (w ||| stranspose rr) pp" using intersect_run 3 by auto
         show "test\<^sub>2 (condition\<^sub>2 (intersect AA)) (b.trace (w ||| stranspose rr) pp)"
           using 3 unfolding b.trace_alt_def by (force simp: list_all2_iff set_conv_nth)
       qed
     qed
 
   end
 
   locale automaton_union =
     a: automaton automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 +
     b: automaton automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 +
     c: automaton automaton\<^sub>3 alphabet\<^sub>3 initial\<^sub>3 transition\<^sub>3 condition\<^sub>3
     for automaton\<^sub>1 :: "'label set \<Rightarrow> 'state\<^sub>1 set \<Rightarrow> ('label, 'state\<^sub>1) trans \<Rightarrow> 'condition\<^sub>1 \<Rightarrow> 'automaton\<^sub>1"
     and alphabet\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'label set"
     and initial\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'state\<^sub>1 set"
     and transition\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> ('label, 'state\<^sub>1) trans"
     and condition\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'condition\<^sub>1"
     and automaton\<^sub>2 :: "'label set \<Rightarrow> 'state\<^sub>2 set \<Rightarrow> ('label, 'state\<^sub>2) trans \<Rightarrow> 'condition\<^sub>2 \<Rightarrow> 'automaton\<^sub>2"
     and alphabet\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'label set"
     and initial\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'state\<^sub>2 set"
     and transition\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> ('label, 'state\<^sub>2) trans"
     and condition\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'condition\<^sub>2"
     and automaton\<^sub>3 :: "'label set \<Rightarrow> ('state\<^sub>1 + 'state\<^sub>2) set \<Rightarrow> ('label, 'state\<^sub>1 + 'state\<^sub>2) trans \<Rightarrow>
       'condition\<^sub>3 \<Rightarrow> 'automaton\<^sub>3"
     and alphabet\<^sub>3 :: "'automaton\<^sub>3 \<Rightarrow> 'label set"
     and initial\<^sub>3 :: "'automaton\<^sub>3 \<Rightarrow> ('state\<^sub>1 + 'state\<^sub>2) set"
     and transition\<^sub>3 :: "'automaton\<^sub>3 \<Rightarrow> ('label, 'state\<^sub>1 + 'state\<^sub>2) trans"
     and condition\<^sub>3 :: "'automaton\<^sub>3 \<Rightarrow> 'condition\<^sub>3"
     +
     fixes condition :: "'condition\<^sub>1 \<Rightarrow> 'condition\<^sub>2 \<Rightarrow> 'condition\<^sub>3"
   begin
 
     definition union :: "'automaton\<^sub>1 \<Rightarrow> 'automaton\<^sub>2 \<Rightarrow> 'automaton\<^sub>3" where
       "union A B \<equiv> automaton\<^sub>3
         (alphabet\<^sub>1 A \<union> alphabet\<^sub>2 B)
         (initial\<^sub>1 A <+> initial\<^sub>2 B)
         (\<lambda> a. \<lambda> Inl p \<Rightarrow> Inl ` transition\<^sub>1 A a p | Inr q \<Rightarrow> Inr ` transition\<^sub>2 B a q)
         (condition (condition\<^sub>1 A) (condition\<^sub>2 B))"
 
     lemma union_simps[simp]:
       "alphabet\<^sub>3 (union A B) = alphabet\<^sub>1 A \<union> alphabet\<^sub>2 B"
       "initial\<^sub>3 (union A B) = initial\<^sub>1 A <+> initial\<^sub>2 B"
       "transition\<^sub>3 (union A B) a (Inl p) = Inl ` transition\<^sub>1 A a p"
       "transition\<^sub>3 (union A B) a (Inr q) = Inr ` transition\<^sub>2 B a q"
       "condition\<^sub>3 (union A B) = condition (condition\<^sub>1 A) (condition\<^sub>2 B)"
       unfolding union_def by auto
 
     lemma run_union_a:
       assumes "a.run A (w ||| r) p"
       shows "c.run (union A B) (w ||| smap Inl r) (Inl p)"
       using assms by (coinduction arbitrary: w r p) (force elim: a.run.cases)
     lemma run_union_b:
       assumes "b.run B (w ||| s) q"
       shows "c.run (union A B) (w ||| smap Inr s) (Inr q)"
       using assms by (coinduction arbitrary: w s q) (force elim: b.run.cases)
     lemma run_union:
       assumes "alphabet\<^sub>1 A = alphabet\<^sub>2 B"
       assumes "c.run (union A B) (w ||| rs) pq"
       obtains
         (a) r p where "rs = smap Inl r" "pq = Inl p" "a.run A (w ||| r) p" |
         (b) s q where "rs = smap Inr s" "pq = Inr q" "b.run B (w ||| s) q"
     proof (cases pq)
       case (Inl p)
       have 1: "rs = smap Inl (smap projl rs)"
         using assms(2) unfolding Inl by (coinduction arbitrary: w rs p) (force elim: c.run.cases)
       have 2: "a.run A (w ||| smap projl rs) p"
         using assms unfolding Inl by (coinduction arbitrary: w rs p) (force elim: c.run.cases)
       show ?thesis using a 1 Inl 2 by this
     next
       case (Inr q)
       have 1: "rs = smap Inr (smap projr rs)"
         using assms(2) unfolding Inr by (coinduction arbitrary: w rs q) (force elim: c.run.cases)
       have 2: "b.run B (w ||| smap projr rs) q"
         using assms unfolding Inr by (coinduction arbitrary: w rs q) (force elim: c.run.cases)
       show ?thesis using b 1 Inr 2 by this
     qed
 
+    lemma union_nodes:
+      assumes "alphabet\<^sub>1 A = alphabet\<^sub>2 B"
+      shows "c.nodes (union A B) \<subseteq> a.nodes A <+> b.nodes B"
+    proof
+      fix pq
+      assume "pq \<in> c.nodes (union A B)"
+      then show "pq \<in> a.nodes A <+> b.nodes B" using assms by (induct) (auto 0 3)
+    qed
+
+    lemma union_nodes_finite[intro]:
+      assumes "alphabet\<^sub>1 A = alphabet\<^sub>2 B"
+      assumes "finite (a.nodes A)" "finite (b.nodes B)"
+      shows "finite (c.nodes (union A B))"
+      using finite_subset union_nodes assms by (auto intro: finite_Plus)
+
   end
 
   locale automaton_union_trace =
     automaton_union
       automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1
       automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2
       automaton\<^sub>3 alphabet\<^sub>3 initial\<^sub>3 transition\<^sub>3 condition\<^sub>3 condition +
     a: automaton_trace automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 +
     b: automaton_trace automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2 +
     c: automaton_trace automaton\<^sub>3 alphabet\<^sub>3 initial\<^sub>3 transition\<^sub>3 condition\<^sub>3 test\<^sub>3
     for automaton\<^sub>1 :: "'label set \<Rightarrow> 'state\<^sub>1 set \<Rightarrow> ('label, 'state\<^sub>1) trans \<Rightarrow> 'condition\<^sub>1 \<Rightarrow> 'automaton\<^sub>1"
     and alphabet\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'label set"
     and initial\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'state\<^sub>1 set"
     and transition\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> ('label, 'state\<^sub>1) trans"
     and condition\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'condition\<^sub>1"
     and test\<^sub>1 :: "'condition\<^sub>1 \<Rightarrow> 'state\<^sub>1 stream \<Rightarrow> bool"
     and automaton\<^sub>2 :: "'label set \<Rightarrow> 'state\<^sub>2 set \<Rightarrow> ('label, 'state\<^sub>2) trans \<Rightarrow> 'condition\<^sub>2 \<Rightarrow> 'automaton\<^sub>2"
     and alphabet\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'label set"
     and initial\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'state\<^sub>2 set"
     and transition\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> ('label, 'state\<^sub>2) trans"
     and condition\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'condition\<^sub>2"
     and test\<^sub>2 :: "'condition\<^sub>2 \<Rightarrow> 'state\<^sub>2 stream \<Rightarrow> bool"
     and automaton\<^sub>3 :: "'label set \<Rightarrow> ('state\<^sub>1 + 'state\<^sub>2) set \<Rightarrow> ('label, 'state\<^sub>1 + 'state\<^sub>2) trans \<Rightarrow>
       'condition\<^sub>3 \<Rightarrow> 'automaton\<^sub>3"
     and alphabet\<^sub>3 :: "'automaton\<^sub>3 \<Rightarrow> 'label set"
     and initial\<^sub>3 :: "'automaton\<^sub>3 \<Rightarrow> ('state\<^sub>1 + 'state\<^sub>2) set"
     and transition\<^sub>3 :: "'automaton\<^sub>3 \<Rightarrow> ('label, 'state\<^sub>1 + 'state\<^sub>2) trans"
     and condition\<^sub>3 :: "'automaton\<^sub>3 \<Rightarrow> 'condition\<^sub>3"
     and test\<^sub>3 :: "'condition\<^sub>3 \<Rightarrow> ('state\<^sub>1 + 'state\<^sub>2) stream \<Rightarrow> bool"
     and condition :: "'condition\<^sub>1 \<Rightarrow> 'condition\<^sub>2 \<Rightarrow> 'condition\<^sub>3"
     +
     assumes test\<^sub>1[iff]: "test\<^sub>3 (condition c\<^sub>1 c\<^sub>2) (smap Inl u) \<longleftrightarrow> test\<^sub>1 c\<^sub>1 u"
     assumes test\<^sub>2[iff]: "test\<^sub>3 (condition c\<^sub>1 c\<^sub>2) (smap Inr v) \<longleftrightarrow> test\<^sub>2 c\<^sub>2 v"
   begin
 
     lemma union_language[simp]:
       assumes "alphabet\<^sub>1 A = alphabet\<^sub>2 B"
       shows "c.language (union A B) = a.language A \<union> b.language B"
       using assms
       unfolding a.language_def b.language_def c.language_def
       unfolding a.trace_alt_def b.trace_alt_def c.trace_alt_def
       by (auto dest: run_union_a run_union_b elim!: run_union)
 
   end
 
+  locale automaton_union_list =
+    a: automaton automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 +
+    b: automaton automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2
+    for automaton\<^sub>1 :: "'label set \<Rightarrow> 'state set \<Rightarrow> ('label, 'state) trans \<Rightarrow> 'condition\<^sub>1 \<Rightarrow> 'automaton\<^sub>1"
+    and alphabet\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'label set"
+    and initial\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'state set"
+    and transition\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> ('label, 'state) trans"
+    and condition\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'condition\<^sub>1"
+    and automaton\<^sub>2 :: "'label set \<Rightarrow> (nat \<times> 'state) set \<Rightarrow> ('label, nat \<times> 'state) trans \<Rightarrow> 'condition\<^sub>2 \<Rightarrow> 'automaton\<^sub>2"
+    and alphabet\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'label set"
+    and initial\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> (nat \<times> 'state) set"
+    and transition\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> ('label, nat \<times> 'state) trans"
+    and condition\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'condition\<^sub>2"
+    +
+    fixes condition :: "'condition\<^sub>1 list \<Rightarrow> 'condition\<^sub>2"
+  begin
+
+    definition union :: "'automaton\<^sub>1 list \<Rightarrow> 'automaton\<^sub>2" where
+      "union AA \<equiv> automaton\<^sub>2
+        (\<Union> (alphabet\<^sub>1 ` set AA))
+        (\<Union> k < length AA. {k} \<times> initial\<^sub>1 (AA ! k))
+        (\<lambda> a (k, p). {k} \<times> transition\<^sub>1 (AA ! k) a p)
+        (condition (map condition\<^sub>1 AA))"
+
+    lemma union_simps[simp]:
+      "alphabet\<^sub>2 (union AA) = \<Union> (alphabet\<^sub>1 ` set AA)"
+      "initial\<^sub>2 (union AA) = (\<Union> k < length AA. {k} \<times> initial\<^sub>1 (AA ! k))"
+      "transition\<^sub>2 (union AA) a (k, p) = {k} \<times> transition\<^sub>1 (AA ! k) a p"
+      "condition\<^sub>2 (union AA) = condition (map condition\<^sub>1 AA)"
+      unfolding union_def by auto
+
+    lemma union_run:
+      assumes "\<Inter> (alphabet\<^sub>1 ` set AA) = \<Union> (alphabet\<^sub>1 ` set AA)"
+      assumes "A \<in> set AA"
+      assumes "a.run A (w ||| s) p"
+      obtains k where "k < length AA" "A = AA ! k" "b.run (union AA) (w ||| sconst k ||| s) (k, p)"
+    proof -
+      obtain k where 1: "k < length AA" "A = AA ! k" using assms(2) unfolding set_conv_nth by auto
+      show ?thesis
+      proof
+        show "k < length AA" "A = AA ! k" using 1 by this
+        show "b.run (union AA) (w ||| sconst k ||| s) (k, p)"
+          using assms 1(2) by (coinduction arbitrary: w s p) (force elim: a.run.cases)
+      qed
+    qed
+    lemma run_union:
+      assumes "\<Inter> (alphabet\<^sub>1 ` set AA) = \<Union> (alphabet\<^sub>1 ` set AA)"
+      assumes "k < length AA"
+      assumes "b.run (union AA) (w ||| r) (k, p)"
+      obtains s where "r = sconst k ||| s" "a.run (AA ! k) (w ||| s) p"
+    proof
+      show "r = sconst k ||| smap snd r"
+        using assms by (coinduction arbitrary: w r p) (force elim: b.run.cases)
+      show "a.run (AA ! k) (w ||| smap snd r) p"
+        using assms by (coinduction arbitrary: w r p) (force elim: b.run.cases)
+    qed
+
+    lemma union_nodes:
+      assumes "\<Inter> (alphabet\<^sub>1 ` set AA) = \<Union> (alphabet\<^sub>1 ` set AA)"
+      shows "b.nodes (union AA) \<subseteq> (\<Union> k < length AA. {k} \<times> a.nodes (AA ! k))"
+    proof
+      show "kp \<in> (\<Union> k < length AA. {k} \<times> a.nodes (AA ! k))" if "kp \<in> b.nodes (union AA)" for kp
+        using that assms by (induct) (auto 0 4)
+    qed
+
+    lemma union_nodes_finite[intro]:
+      assumes "\<Inter> (alphabet\<^sub>1 ` set AA) = \<Union> (alphabet\<^sub>1 ` set AA)"
+      assumes "list_all (finite \<circ> a.nodes) AA"
+      shows "finite (b.nodes (union AA))"
+    proof (rule finite_subset)
+      show "b.nodes (union AA) \<subseteq> (\<Union> k < length AA. {k} \<times> a.nodes (AA ! k))"
+        using union_nodes assms(1) by this
+      show "finite (\<Union> k < length AA. {k} \<times> a.nodes' (AA ! k))"
+        using assms(2) unfolding list_all_length by auto
+    qed
+
+  end
+
+  locale automaton_union_list_trace =
+    automaton_union_list
+      automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1
+      automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 condition +
+    a: automaton_trace automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 +
+    b: automaton_trace automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2
+    for automaton\<^sub>1 :: "'label set \<Rightarrow> 'state set \<Rightarrow> ('label, 'state) trans \<Rightarrow> 'condition\<^sub>1 \<Rightarrow> 'automaton\<^sub>1"
+    and alphabet\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'label set"
+    and initial\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'state set"
+    and transition\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> ('label, 'state) trans"
+    and condition\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'condition\<^sub>1"
+    and test\<^sub>1 :: "'condition\<^sub>1 \<Rightarrow> 'state stream \<Rightarrow> bool"
+    and automaton\<^sub>2 :: "'label set \<Rightarrow> (nat \<times> 'state) set \<Rightarrow> ('label, nat \<times> 'state) trans \<Rightarrow> 'condition\<^sub>2 \<Rightarrow> 'automaton\<^sub>2"
+    and alphabet\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'label set"
+    and initial\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> (nat \<times> 'state) set"
+    and transition\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> ('label, nat \<times> 'state) trans"
+    and condition\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'condition\<^sub>2"
+    and test\<^sub>2 :: "'condition\<^sub>2 \<Rightarrow> (nat \<times> 'state) stream \<Rightarrow> bool"
+    and condition :: "'condition\<^sub>1 list \<Rightarrow> 'condition\<^sub>2"
+    +
+    assumes test[iff]: "test\<^sub>2 (condition cs) (sconst k ||| w) \<longleftrightarrow> test\<^sub>1 (cs ! k) w"
+  begin
+
+    lemma union_language[simp]:
+      assumes "\<Inter> (alphabet\<^sub>1 ` set AA) = \<Union> (alphabet\<^sub>1 ` set AA)"
+      shows "b.language (union AA) = \<Union> (a.language ` set AA)"
+    proof
+      show "b.language (union AA) \<subseteq> \<Union> (a.language ` set AA)"
+        using assms
+        unfolding a.language_def b.language_def
+        unfolding a.trace_alt_def b.trace_alt_def
+        by (force elim: run_union)
+      show "\<Union> (a.language ` set AA) \<subseteq> b.language (union AA)"
+        using assms
+        unfolding a.language_def b.language_def
+        unfolding a.trace_alt_def b.trace_alt_def
+        by (force elim!: union_run)
+    qed
+
+  end
+
 end
\ No newline at end of file
diff --git a/thys/Transition_Systems_and_Automata/Basic/Sequence_Zip.thy b/thys/Transition_Systems_and_Automata/Basic/Sequence_Zip.thy
--- a/thys/Transition_Systems_and_Automata/Basic/Sequence_Zip.thy
+++ b/thys/Transition_Systems_and_Automata/Basic/Sequence_Zip.thy
@@ -1,159 +1,164 @@
 section \<open>Zipping Sequences\<close>
 
 theory Sequence_Zip
 imports "Sequence_LTL"
 begin
 
   subsection \<open>Zipping Lists\<close>
 
   notation zip (infixr "||" 51)
 
   lemmas [simp] = zip_map_fst_snd
 
   lemma split_zip[no_atp]: "(\<And> x. PROP P x) \<equiv> (\<And> y z. length y = length z \<Longrightarrow> PROP P (y || z))"
   proof
     fix y z
     assume 1: "\<And> x. PROP P x"
     show "PROP P (y || z)" using 1 by this
   next
     fix x :: "('a \<times> 'b) list"
     assume 1: "\<And> y z. length y = length z \<Longrightarrow> PROP P (y || z)"
     have 2: "length (map fst x) = length (map snd x)" by simp
     have 3: "PROP P (map fst x || map snd x)" using 1 2 by this
     show "PROP P x" using 3 by simp
   qed
   lemma split_zip_all[no_atp]: "(\<forall> x. P x) \<longleftrightarrow> (\<forall> y z. length y = length z \<longrightarrow> P (y || z))"
     by (fastforce iff: split_zip)
   lemma split_zip_ex[no_atp]: "(\<exists> x. P x) \<longleftrightarrow> (\<exists> y z. length y = length z \<and> P (y || z))"
     by (fastforce iff: split_zip)
 
   lemma zip_eq[iff]:
     assumes "length u = length v" "length r = length s"
     shows "u || v = r || s \<longleftrightarrow> u = r \<and> v = s"
     using assms zip_eq_conv by metis
 
   lemma list_rel_pred_zip: "list_all2 P xs ys \<longleftrightarrow> length xs = length ys \<and> list_all (case_prod P) (xs || ys)"
     unfolding list_all2_conv_all_nth list_all_length by auto
 
   lemma list_choice_zip: "list_all (\<lambda> x. \<exists> y. P x y) xs \<longleftrightarrow>
     (\<exists> ys. length ys = length xs \<and> list_all (case_prod P) (xs || ys))"
     unfolding list_choice list_rel_pred_zip by metis
   lemma list_choice_pair: "list_all (\<lambda> xy. case_prod (\<lambda> x y. \<exists> z. P x y z) xy) (xs || ys) \<longleftrightarrow>
     (\<exists> zs. length zs = min (length xs) (length ys) \<and> list_all (\<lambda> (x, y, z). P x y z) (xs || ys || zs))"
   proof -
     have 1: "list_all (\<lambda> (xy, z). case xy of (x, y) \<Rightarrow> P x y z) ((xs || ys) || zs) \<longleftrightarrow>
       list_all (\<lambda> (x, y, z). P x y z) (xs || ys || zs)" for zs
       unfolding zip_assoc list.pred_map by (auto intro!: list.pred_cong)
     have 2: "(\<lambda> (x, y). \<exists> z. P x y z) = (\<lambda> xy. \<exists> z. case xy of (x, y) \<Rightarrow> P x y z)" by auto
     show ?thesis unfolding list_choice_zip 1 2 by force
   qed
 
   lemma list_rel_zip[iff]:
     assumes "length u = length v" "length r = length s"
     shows "list_all2 (rel_prod A B) (u || v) (r || s) \<longleftrightarrow> list_all2 A u r \<and> list_all2 B v s"
   proof safe
     assume [transfer_rule]: "list_all2 (rel_prod A B) (u || v) (r || s)"
     have "list_all2 A (map fst (u || v)) (map fst (r || s))" by transfer_prover
     then show "list_all2 A u r" using assms by simp
     have "list_all2 B (map snd (u || v)) (map snd (r || s))" by transfer_prover
     then show "list_all2 B v s" using assms by simp
   next
     assume [transfer_rule]: "list_all2 A u r" "list_all2 B v s"
     show "list_all2 (rel_prod A B) (u || v) (r || s)" by transfer_prover
   qed
 
   lemma zip_last[simp]:
     assumes "xs || ys \<noteq> []" "length xs = length ys"
     shows "last (xs || ys) = (last xs, last ys)"
   proof -
     have 1: "xs \<noteq> []" "ys \<noteq> []" using assms(1) by auto
     have "last (xs || ys) = (xs || ys) ! (length (xs || ys) - 1)" using last_conv_nth assms by blast
     also have "\<dots> = (xs ! (length (xs || ys) - 1), ys ! (length (xs || ys) - 1))" using assms 1 by simp
     also have "\<dots> = (xs ! (length xs - 1), ys ! (length ys - 1))" using assms(2) by simp
     also have "\<dots> = (last xs, last ys)" using last_conv_nth 1 by metis
     finally show ?thesis by this
   qed
 
   subsection \<open>Zipping Streams\<close>
 
   notation szip (infixr "|||" 51)
 
   lemmas [simp] = szip_unfold
 
   lemma szip_smap[simp]: "smap fst zs ||| smap snd zs = zs" by (coinduction arbitrary: zs) (auto)
   lemma szip_smap_fst[simp]: "smap fst (xs ||| ys) = xs" by (coinduction arbitrary: xs ys) (auto)
   lemma szip_smap_snd[simp]: "smap snd (xs ||| ys) = ys" by (coinduction arbitrary: xs ys) (auto)
 
+  lemma szip_sconst_smap_fst: "sconst a ||| xs = smap (Pair a) xs"
+    by (coinduction arbitrary: xs) (auto)
+  lemma szip_sconst_smap_snd: "xs ||| sconst a = smap (prod.swap \<circ> Pair a) xs"
+    by (coinduction arbitrary: xs) (auto)
+
   lemma split_szip[no_atp]: "(\<And> x. PROP P x) \<equiv> (\<And> y z. PROP P (y ||| z))"
   proof
     fix y z
     assume 1: "\<And> x. PROP P x"
     show "PROP P (y ||| z)" using 1 by this
   next
     fix x
     assume 1: "\<And> y z. PROP P (y ||| z)"
     have 2: "PROP P (smap fst x ||| smap snd x)" using 1 by this
     show "PROP P x" using 2 by simp
   qed
   lemma split_szip_all[no_atp]: "(\<forall> x. P x) \<longleftrightarrow> (\<forall> y z. P (y ||| z))" by (fastforce iff: split_szip)
   lemma split_szip_ex[no_atp]: "(\<exists> x. P x) \<longleftrightarrow> (\<exists> y z. P (y ||| z))" by (fastforce iff: split_szip)
 
   lemma szip_eq[iff]: "u ||| v = r ||| s \<longleftrightarrow> u = r \<and> v = s"
     using szip_smap_fst szip_smap_snd by metis
 
   lemma stream_rel_szip[iff]:
     "stream_all2 (rel_prod A B) (u ||| v) (r ||| s) \<longleftrightarrow> stream_all2 A u r \<and> stream_all2 B v s"
   proof safe
     assume [transfer_rule]: "stream_all2 (rel_prod A B) (u ||| v) (r ||| s)"
     have "stream_all2 A (smap fst (u ||| v)) (smap fst (r ||| s))" by transfer_prover
     then show "stream_all2 A u r" by simp
     have "stream_all2 B (smap snd (u ||| v)) (smap snd (r ||| s))" by transfer_prover
     then show "stream_all2 B v s" by simp
   next
     assume [transfer_rule]: "stream_all2 A u r" "stream_all2 B v s"
     show "stream_all2 (rel_prod A B) (u ||| v) (r ||| s)" by transfer_prover
   qed
 
   lemma szip_shift[simp]:
     assumes "length u = length s"
     shows "u @- v ||| s @- t = (u || s) @- (v ||| t)"
     using assms by (simp add: eq_shift stake_shift sdrop_shift)
 
   lemma szip_sset_fst[simp]: "fst ` sset (u ||| v) = sset u" by (metis stream.set_map szip_smap_fst)
   lemma szip_sset_snd[simp]: "snd ` sset (u ||| v) = sset v" by (metis stream.set_map szip_smap_snd)
   lemma szip_sset_elim[elim]:
     assumes "(a, b) \<in> sset (u ||| v)"
     obtains "a \<in> sset u" "b \<in> sset v"
     using assms by (metis image_eqI fst_conv snd_conv szip_sset_fst szip_sset_snd)
   lemma szip_sset[simp]: "sset (u ||| v) \<subseteq> sset u \<times> sset v" by auto
 
   lemma sset_szip_finite[iff]: "finite (sset (u ||| v)) \<longleftrightarrow> finite (sset u) \<and> finite (sset v)"
   proof safe
     assume 1: "finite (sset (u ||| v))"
     have 2: "finite (fst ` sset (u ||| v))" using 1 by blast
     have 3: "finite (snd ` sset (u ||| v))" using 1 by blast
     show "finite (sset u)" using 2 by simp
     show "finite (sset v)" using 3 by simp
   next
     assume 1: "finite (sset u)" "finite (sset v)"
     have "sset (u ||| v) \<subseteq> sset u \<times> sset v" by simp
     also have "finite \<dots>" using 1 by simp
     finally show "finite (sset (u ||| v))" by this
   qed
 
   lemma infs_szip_fst[iff]: "infs (P \<circ> fst) (u ||| v) \<longleftrightarrow> infs P u"
   proof -
     have "infs (P \<circ> fst) (u ||| v) \<longleftrightarrow> infs P (smap fst (u ||| v))"
       by (simp add: comp_def del: szip_smap_fst)
     also have "\<dots> \<longleftrightarrow> infs P u" by simp
     finally show ?thesis by this
   qed
   lemma infs_szip_snd[iff]: "infs (P \<circ> snd) (u ||| v) \<longleftrightarrow> infs P v"
   proof -
     have "infs (P \<circ> snd) (u ||| v) \<longleftrightarrow> infs P (smap snd (u ||| v))"
       by (simp add: comp_def del: szip_smap_snd)
     also have "\<dots> \<longleftrightarrow> infs P v" by simp
     finally show ?thesis by this
   qed
 
 end
\ No newline at end of file