diff --git a/thys/Transition_Systems_and_Automata/Automata/Deterministic.thy b/thys/Transition_Systems_and_Automata/Automata/Deterministic.thy
--- a/thys/Transition_Systems_and_Automata/Automata/Deterministic.thy
+++ b/thys/Transition_Systems_and_Automata/Automata/Deterministic.thy
@@ -1,559 +1,556 @@
 theory Deterministic
 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"
 
   (* TODO: is there a way to be less verbose in these locales? do we need to specify all the types? *)
   locale automaton =
     fixes automaton :: "'label set \<Rightarrow> 'state \<Rightarrow> ('label, 'state) trans \<Rightarrow> 'condition \<Rightarrow> 'automaton"
     fixes alphabet :: "'automaton \<Rightarrow> 'label set"
     fixes initial :: "'automaton \<Rightarrow> 'state"
     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
 
     (* TODO: is there a way to use defines without renaming the constants? *)
     sublocale transition_system_initial
       "transition A" "\<lambda> a p. a \<in> alphabet A" "\<lambda> p. p = initial A"
       for A
       defines path' = path and run' = run and reachable' = reachable and nodes' = nodes
       by this
 
     lemma path_alt_def: "path A w p \<longleftrightarrow> set w \<subseteq> alphabet A"
     unfolding lists_iff_set[symmetric]
     proof
       show "w \<in> lists (alphabet A)" if "path A w p" using that by (induct arbitrary: p) (auto)
       show "path A w p" if "w \<in> lists (alphabet A)" using that by (induct arbitrary: p) (auto)
     qed
     lemma run_alt_def: "run A w p \<longleftrightarrow> sset w \<subseteq> alphabet A"
     unfolding streams_iff_sset[symmetric]
     proof
       show "w \<in> streams (alphabet A)" if "run A w p"
         using that by (coinduction arbitrary: w p) (force elim: run.cases)
       show "run A w p" if "w \<in> streams (alphabet A)"
         using that by (coinduction arbitrary: w p) (force elim: streams.cases)
     qed
 
   end
 
   (* TODO: create analogous locale for DFAs (automaton_target) *)
   locale automaton_trace =
     automaton automaton alphabet initial transition condition
     for automaton :: "'label set \<Rightarrow> 'state \<Rightarrow> ('label, 'state) trans \<Rightarrow> 'condition \<Rightarrow> 'automaton"
     and alphabet :: "'automaton \<Rightarrow> 'label set"
     and initial :: "'automaton \<Rightarrow> 'state"
     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. run A w (initial A) \<and> test (condition A) (trace A w (initial A))}"
   
     lemma language[intro]:
       assumes "run A w (initial A)" "test (condition A) (trace A w (initial A))"
       shows "w \<in> language A"
       using assms unfolding language_def by auto
     lemma language_elim[elim]:
       assumes "w \<in> language A"
       obtains "run A w (initial A)" "test (condition A) (trace A w (initial A))"
       using assms unfolding language_def by auto
   
     lemma language_alphabet: "language A \<subseteq> streams (alphabet A)"
       unfolding language_def run_alt_def using sset_streams by auto
 
   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 \<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"
     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 \<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"
     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, 0)
         (\<lambda> a (p, k). (transition\<^sub>1 A a p, 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, 0)"
       "transition\<^sub>2 (degeneralize A) a (p, k) = (transition\<^sub>1 A a p, count (condition\<^sub>1 A) p k)"
       "condition\<^sub>2 (degeneralize A) = degen (condition\<^sub>1 A)"
       unfolding degeneralize_def by auto
 
     lemma degeneralize_target[simp]: "b.target (degeneralize A) w (p, k) =
       (a.target A w p, fold (count (condition\<^sub>1 A)) (butlast (p # a.states A w p)) k)"
       by (induct w arbitrary: p k) (auto)
     lemma degeneralize_states[simp]: "b.states (degeneralize A) w (p, k) =
       a.states A w p || scan (count (condition\<^sub>1 A)) (p # a.states A w p) k"
       by (induct w arbitrary: p k) (auto)
     lemma degeneralize_trace[simp]: "b.trace (degeneralize A) w (p, k) =
       a.trace A w p ||| sscan (count (condition\<^sub>1 A)) (p ## a.trace A w p) k"
       by (coinduction arbitrary: w p k) (auto)
 
     lemma degeneralize_path[iff]: "b.path (degeneralize A) w (p, k) \<longleftrightarrow> a.path A w p"
       unfolding a.path_alt_def b.path_alt_def by simp
     lemma degeneralize_run[iff]: "b.run (degeneralize A) w (p, k) \<longleftrightarrow> a.run A w p"
       unfolding a.run_alt_def b.run_alt_def by simp
 
     lemma degeneralize_reachable_fst[simp]: "fst ` b.reachable (degeneralize A) (p, k) = a.reachable A p"
       unfolding a.reachable_alt_def b.reachable_alt_def image_def by simp
     lemma degeneralize_reachable_snd_empty[simp]:
       assumes "condition\<^sub>1 A = []"
       shows "snd ` b.reachable (degeneralize A) (p, k) = {k}"
     proof -
       have "snd ql = k" if "ql \<in> b.reachable (degeneralize A) (p, k)" for ql
         using that assms by induct auto
       then show ?thesis by auto
     qed
     lemma degeneralize_reachable_empty[simp]:
       assumes "condition\<^sub>1 A = []"
       shows "b.reachable (degeneralize A) (p, k) = a.reachable A p \<times> {k}"
       using degeneralize_reachable_fst degeneralize_reachable_snd_empty assms
       by (metis prod_singleton(2))
     lemma degeneralize_reachable_snd:
       "snd ` b.reachable (degeneralize A) (p, k) \<subseteq> insert k {0 ..< length (condition\<^sub>1 A)}"
       by (cases "condition\<^sub>1 A = []") (auto)
     lemma degeneralize_reachable:
       "b.reachable (degeneralize A) (p, k) \<subseteq> a.reachable A p \<times> insert k {0 ..< length (condition\<^sub>1 A)}"
       by (cases "condition\<^sub>1 A = []") (auto 0 3)
 
     lemma degeneralize_nodes_fst[simp]: "fst ` b.nodes (degeneralize A) = a.nodes A"
       unfolding a.nodes_alt_def b.nodes_alt_def by simp
     lemma degeneralize_nodes_snd_empty:
       assumes "condition\<^sub>1 A = []"
       shows "snd ` b.nodes (degeneralize A) = {0}"
       using assms unfolding b.nodes_alt_def by auto
     lemma degeneralize_nodes_empty:
       assumes "condition\<^sub>1 A = []"
       shows "b.nodes (degeneralize A) = a.nodes A \<times> {0}"
       using assms unfolding b.nodes_alt_def by auto
     lemma degeneralize_nodes_snd:
       "snd ` b.nodes (degeneralize A) \<subseteq> insert 0 {0 ..< length (condition\<^sub>1 A)}"
       using degeneralize_reachable_snd unfolding b.nodes_alt_def by auto
     lemma degeneralize_nodes:
       "b.nodes (degeneralize A) \<subseteq> a.nodes A \<times> insert 0 {0 ..< length (condition\<^sub>1 A)}"
       using degeneralize_reachable unfolding a.nodes_alt_def b.nodes_alt_def by simp
   
     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 that by (auto simp flip: degeneralize_nodes_fst)
       show "finite (b.nodes (degeneralize A))" if "finite (a.nodes A)"
         using finite_subset degeneralize_nodes that by blast
     qed
     lemma degeneralize_nodes_card: "card (b.nodes (degeneralize A)) \<le>
       max 1 (length (condition\<^sub>1 A)) * card (a.nodes A)"
     proof (cases "finite (a.nodes A)")
       case True
       have "card (b.nodes (degeneralize A)) \<le> card (a.nodes A \<times> insert 0 {0 ..< length (condition\<^sub>1 A)})"
         using degeneralize_nodes True by (blast intro: card_mono)
       also have "\<dots> = card (insert 0 {0 ..< length (condition\<^sub>1 A)}) * card (a.nodes A)"
         unfolding card_cartesian_product by simp
       also have "card (insert 0 {0 ..< length (condition\<^sub>1 A)}) = max 1 (length (condition\<^sub>1 A))"
         by (simp add: card_insert_if Suc_leI max_absorb2)
       finally show ?thesis by this
     next
       case False
       then have "card (a.nodes A) = 0" "card (b.nodes (degeneralize A)) = 0" by auto
       then show ?thesis by simp
     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 \<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"
     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 \<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"
     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"
       by (force simp del: sscan_scons)
 
   end
 
   locale automaton_combination =
     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 \<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"
     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 \<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"
     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 \<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"
     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 combine :: "'automaton\<^sub>1 \<Rightarrow> 'automaton\<^sub>2 \<Rightarrow> 'automaton\<^sub>3" where
       "combine A B \<equiv> automaton\<^sub>3
         (alphabet\<^sub>1 A \<inter> alphabet\<^sub>2 B)
         (initial\<^sub>1 A, initial\<^sub>2 B)
         (\<lambda> a (p, q). (transition\<^sub>1 A a p, transition\<^sub>2 B a q))
         (condition (condition\<^sub>1 A) (condition\<^sub>2 B))"
 
     lemma combine_simps[simp]:
       "alphabet\<^sub>3 (combine A B) = alphabet\<^sub>1 A \<inter> alphabet\<^sub>2 B"
       "initial\<^sub>3 (combine A B) = (initial\<^sub>1 A, initial\<^sub>2 B)"
       "transition\<^sub>3 (combine A B) a (p, q) = (transition\<^sub>1 A a p, transition\<^sub>2 B a q)"
       "condition\<^sub>3 (combine A B) = condition (condition\<^sub>1 A) (condition\<^sub>2 B)"
       unfolding combine_def by auto
 
     lemma combine_target[simp]: "c.target (combine A B) w (p, q) = (a.target A w p, b.target B w q)"
       by (induct w arbitrary: p q) (auto)
     lemma combine_states[simp]: "c.states (combine A B) w (p, q) = a.states A w p || b.states B w q"
       by (induct w arbitrary: p q) (auto)
     lemma combine_trace[simp]: "c.trace (combine A B) w (p, q) = a.trace A w p ||| b.trace B w q"
       by (coinduction arbitrary: w p q) (auto)
 
     lemma combine_path[iff]: "c.path (combine A B) w (p, q) \<longleftrightarrow> a.path A w p \<and> b.path B w q"
       unfolding a.path_alt_def b.path_alt_def c.path_alt_def by simp
     lemma combine_run[iff]: "c.run (combine A B) w (p, q) \<longleftrightarrow> a.run A w p \<and> b.run B w q"
       unfolding a.run_alt_def b.run_alt_def c.run_alt_def by simp
 
     lemma combine_reachable[simp]: "c.reachable (combine A B) (p, q) \<subseteq> a.reachable A p \<times> b.reachable B q"
       unfolding c.reachable_alt_def by auto
     lemma combine_nodes[simp]: "c.nodes (combine A B) \<subseteq> a.nodes A \<times> b.nodes B"
       unfolding a.nodes_alt_def b.nodes_alt_def c.nodes_alt_def by auto
     lemma combine_reachable_fst[simp]:
       assumes "alphabet\<^sub>1 A \<subseteq> alphabet\<^sub>2 B"
       shows "fst ` c.reachable (combine A B) (p, q) = a.reachable A p"
       using assms
       unfolding a.reachable_alt_def a.path_alt_def
       unfolding b.reachable_alt_def b.path_alt_def
       unfolding c.reachable_alt_def c.path_alt_def
       by auto force
     lemma combine_reachable_snd[simp]:
       assumes "alphabet\<^sub>1 A \<supseteq> alphabet\<^sub>2 B"
       shows "snd ` c.reachable (combine A B) (p, q) = b.reachable B q"
       using assms
       unfolding a.reachable_alt_def a.path_alt_def
       unfolding b.reachable_alt_def b.path_alt_def
       unfolding c.reachable_alt_def c.path_alt_def
       by auto force
     lemma combine_nodes_fst[simp]:
       assumes "alphabet\<^sub>1 A \<subseteq> alphabet\<^sub>2 B"
       shows "fst ` c.nodes (combine A B) = a.nodes A"
       using assms combine_reachable_fst
       unfolding a.nodes_alt_def b.nodes_alt_def c.nodes_alt_def
       by fastforce
     lemma combine_nodes_snd[simp]:
       assumes "alphabet\<^sub>1 A \<supseteq> alphabet\<^sub>2 B"
       shows "snd ` c.nodes (combine A B) = b.nodes B"
       using assms combine_reachable_snd
       unfolding a.nodes_alt_def b.nodes_alt_def c.nodes_alt_def
       by fastforce
 
     lemma combine_nodes_finite[intro]:
       assumes "finite (a.nodes A)" "finite (b.nodes B)"
       shows "finite (c.nodes (combine A B))"
     proof (rule finite_subset)
       show "c.nodes (combine A B) \<subseteq> a.nodes A \<times> b.nodes B" using combine_nodes by this
       show "finite (a.nodes A \<times> b.nodes B)" using assms by simp
     qed
     lemma combine_nodes_finite_strong[iff]:
       assumes "alphabet\<^sub>1 A = alphabet\<^sub>2 B"
       shows "finite (c.nodes (combine A B)) \<longleftrightarrow> finite (a.nodes A) \<and> finite (b.nodes B)"
     proof safe
       show "finite (a.nodes A)" if "finite (c.nodes (combine A B))"
         using combine_nodes_fst assms that by (metis finite_imageI equalityD1)
       show "finite (b.nodes B)" if "finite (c.nodes (combine A B))"
         using combine_nodes_snd assms that by (metis finite_imageI equalityD2)
       show "finite (c.nodes (combine A B))" if "finite (a.nodes A)" "finite (b.nodes B)"
         using that by rule
     qed
     lemma combine_nodes_card[intro]:
       assumes "finite (a.nodes A)" "finite (b.nodes B)"
       shows "card (c.nodes (combine A B)) \<le> card (a.nodes A) * card (b.nodes B)"
     proof -
       have "card (c.nodes (combine A B)) \<le> card (a.nodes A \<times> b.nodes B)"
       proof (rule card_mono)
         show "finite (a.nodes A \<times> b.nodes B)" using assms by simp
         show "c.nodes (combine A B) \<subseteq> a.nodes A \<times> b.nodes B" using combine_nodes by this
       qed
       also have "\<dots> = card (a.nodes A) * card (b.nodes B)" using card_cartesian_product by this
       finally show ?thesis by this
     qed
     lemma combine_nodes_card_strong[intro]:
       assumes "alphabet\<^sub>1 A = alphabet\<^sub>2 B"
       shows "card (c.nodes (combine A B)) \<le> card (a.nodes A) * card (b.nodes B)"
     proof (cases "finite (a.nodes A) \<and> finite (b.nodes B)")
       case True
       show ?thesis using True by auto
     next
       case False
       have 1: "card (c.nodes (combine A B)) = 0" using False assms by simp
       have 2: "card (a.nodes A) * card (b.nodes B) = 0" using False by auto
       show ?thesis using 1 2 by simp
     qed
 
   end
 
   locale automaton_intersection_trace =
     automaton_combination
       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 \<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"
     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 \<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"
     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 \<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"
     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 combine_language[simp]: "c.language (combine A B) = a.language A \<inter> b.language B" by force
 
   end
 
   locale automaton_union_trace =
     automaton_combination
       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 \<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"
     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 \<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"
     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 \<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"
     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 \<or> test\<^sub>2 c\<^sub>2 v"
   begin
 
     lemma combine_language[simp]:
       assumes "alphabet\<^sub>1 A = alphabet\<^sub>2 B"
       shows "c.language (combine A B) = a.language A \<union> b.language B"
       using assms by (force simp: a.run_alt_def b.run_alt_def)
 
   end
 
   (* TODO: complete this in analogy to the pair case *)
   locale automaton_combination_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 \<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"
     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 \<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"
     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 combine :: "'automaton\<^sub>1 list \<Rightarrow> 'automaton\<^sub>2" where
       "combine AA \<equiv> automaton\<^sub>2
         (\<Inter> (alphabet\<^sub>1 ` set AA))
         (map initial\<^sub>1 AA)
         (\<lambda> a pp. map2 (\<lambda> A p. transition\<^sub>1 A a p) AA pp)
         (condition (map condition\<^sub>1 AA))"
 
     lemma combine_simps[simp]:
       "alphabet\<^sub>2 (combine AA) = \<Inter> (alphabet\<^sub>1 ` set AA)"
       "initial\<^sub>2 (combine AA) = map initial\<^sub>1 AA"
       "transition\<^sub>2 (combine AA) a pp = map2 (\<lambda> A p. transition\<^sub>1 A a p) AA pp"
       "condition\<^sub>2 (combine AA) = condition (map condition\<^sub>1 AA)"
       unfolding combine_def by auto
 
-    (* TODO: get rid of indices, express this using stranspose *)
+    (* TODO: get rid of indices, express this using stranspose and listset *)
     lemma combine_trace_smap:
       assumes "length pp = length AA" "k < length AA"
       shows "smap (\<lambda> pp. pp ! k) (b.trace (combine AA) w pp) = a.trace (AA ! k) w (pp ! k)"
       using assms by (coinduction arbitrary: w pp) (force)
     lemma combine_nodes_length:
       assumes "pp \<in> b.nodes (combine AA)"
       shows "length pp = length AA"
       using assms by induct auto
     lemma combine_nodes[intro]:
       assumes "pp \<in> b.nodes (combine AA)" "k < length pp"
       shows "pp ! k \<in> a.nodes (AA ! k)"
       using assms by induct auto
 
     lemma combine_nodes_finite[intro]:
       assumes "list_all (finite \<circ> a.nodes) AA"
       shows "finite (b.nodes (combine AA))"
     proof (rule finite_subset)
+      (* TODO: this is used more than once, make top level theorem *)
       show "b.nodes (combine AA) \<subseteq> listset (map a.nodes AA)"
         by (force simp: listset_member list_all2_conv_all_nth combine_nodes_length)
-      have "finite (listset (map a.nodes AA)) \<longleftrightarrow> list_all finite (map a.nodes AA)"
-        by (rule listset_finite) (auto simp: list_all_iff)
-      then show "finite (listset (map a.nodes AA))" using assms by (simp add: list.pred_map)
+      show "finite (listset (map a.nodes AA))" using list.pred_map assms by auto
     qed
     lemma combine_nodes_card:
       assumes "list_all (finite \<circ> a.nodes) AA"
       shows "card (b.nodes (combine AA)) \<le> prod_list (map (card \<circ> a.nodes) AA)"
     proof -
       have "card (b.nodes (combine AA)) \<le> card (listset (map a.nodes AA))"
       proof (rule card_mono)
-        have "finite (listset (map a.nodes AA)) \<longleftrightarrow> list_all finite (map a.nodes AA)"
-          by (rule listset_finite) (auto simp: list_all_iff)
-        then show "finite (listset (map a.nodes AA))" using assms by (simp add: list.pred_map)
+        show "finite (listset (map a.nodes AA))" using list.pred_map assms by auto
         show "b.nodes (combine AA) \<subseteq> listset (map a.nodes AA)"
           by (force simp: listset_member list_all2_conv_all_nth combine_nodes_length)
       qed
       also have "\<dots> = prod_list (map (card \<circ> a.nodes) AA)" by simp
       finally show ?thesis by this
     qed
 
   end
 
   locale automaton_intersection_list_trace =
     automaton_combination_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 \<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"
     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 \<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"
     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]: "test\<^sub>2 (condition cs) w \<longleftrightarrow>
       (\<forall> k < length cs. test\<^sub>1 (cs ! k) (smap (\<lambda> pp. pp ! k) w))"
   begin
 
     lemma combine_language[simp]: "b.language (combine AA) = \<Inter> (a.language ` set AA)"
       unfolding a.language_def b.language_def
       unfolding a.run_alt_def b.run_alt_def
       by (auto simp: combine_trace_smap iff: in_set_conv_nth)
 
   end
 
   locale automaton_union_list_trace =
     automaton_combination_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 \<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"
     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 \<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"
     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]: "test\<^sub>2 (condition cs) w \<longleftrightarrow>
       (\<exists> k < length cs. test\<^sub>1 (cs ! k) (smap (\<lambda> pp. pp ! k) w))"
   begin
 
     lemma combine_language[simp]:
       assumes "\<Inter> (alphabet\<^sub>1 ` set AA) = \<Union> (alphabet\<^sub>1 ` set AA)"
       shows "b.language (combine AA) = \<Union> (a.language ` set AA)"
       using assms
       unfolding a.language_def b.language_def
       unfolding a.run_alt_def b.run_alt_def
       by (auto simp: combine_trace_smap iff: in_set_conv_nth) (metis INT_subset_iff in_set_conv_nth)
 
   end
 
 end
\ No newline at end of file
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,46 +1,77 @@
 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
 
   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,438 +1,612 @@
 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
 
   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
 
 end
\ No newline at end of file
diff --git a/thys/Transition_Systems_and_Automata/Basic/Sequence.thy b/thys/Transition_Systems_and_Automata/Basic/Sequence.thy
--- a/thys/Transition_Systems_and_Automata/Basic/Sequence.thy
+++ b/thys/Transition_Systems_and_Automata/Basic/Sequence.thy
@@ -1,441 +1,468 @@
 section \<open>Finite and Infinite Sequences\<close>
 
 theory Sequence
 imports
   "Basic"
   "HOL-Library.Stream"
   "HOL-Library.Monad_Syntax"
 begin
 
   subsection \<open>List Basics\<close>
 
   declare upt_Suc[simp del]
   declare last.simps[simp del]
   declare butlast.simps[simp del]
   declare Cons_nth_drop_Suc[simp]
   declare list.pred_True[simp]
 
   lemma list_pred_cases:
     assumes "list_all P xs"
     obtains (nil) "xs = []" | (cons) y ys where "xs = y # ys" "P y" "list_all P ys"
     using assms by (cases xs) (auto)
 
   lemma lists_iff_set: "w \<in> lists A \<longleftrightarrow> set w \<subseteq> A" by auto
 
   lemma fold_const: "fold const xs a = last (a # xs)"
     by (induct xs arbitrary: a) (auto simp: last.simps)
 
   lemma take_Suc: "take (Suc n) xs = (if xs = [] then [] else hd xs # take n (tl xs))"
     by (simp add: take_Suc)
 
   lemma bind_map[simp]: "map f xs \<bind> g = xs \<bind> g \<circ> f" unfolding List.bind_def by simp
 
   lemma ball_bind[iff]: "Ball (set (xs \<bind> f)) P \<longleftrightarrow> (\<forall> x \<in> set xs. \<forall> y \<in> set (f x). P y)"
     unfolding set_list_bind by simp
   lemma bex_bind[iff]: "Bex (set (xs \<bind> f)) P \<longleftrightarrow> (\<exists> x \<in> set xs. \<exists> y \<in> set (f x). P y)"
     unfolding set_list_bind by simp
 
+  lemma list_choice: "list_all (\<lambda> x. \<exists> y. P x y) xs \<longleftrightarrow> (\<exists> ys. list_all2 P xs ys)"
+    by (induct xs) (auto simp: list_all2_Cons1)
+
   lemma listset_member: "ys \<in> listset XS \<longleftrightarrow> list_all2 (\<in>) ys XS"
     by (induct XS arbitrary: ys) (auto simp: set_Cons_def list_all2_Cons2)
   lemma listset_empty[iff]: "listset XS = {} \<longleftrightarrow> \<not> list_all (\<lambda> A. A \<noteq> {}) XS"
     by (induct XS) (auto simp: set_Cons_def)
   lemma listset_finite[iff]:
     assumes "list_all (\<lambda> A. A \<noteq> {}) XS"
     shows "finite (listset XS) \<longleftrightarrow> list_all finite XS"
   using assms
   proof (induct XS)
     case Nil
     show ?case by simp
   next
     case (Cons A XS)
     note [simp] = finite_image_iff finite_cartesian_product_iff
     have "listset (A # XS) = case_prod Cons ` (A \<times> listset XS)" by (auto simp: set_Cons_def)
     also have "finite \<dots> \<longleftrightarrow> finite (A \<times> listset XS)" by (simp add: inj_on_def)
     also have "\<dots> \<longleftrightarrow> finite A \<and> finite (listset XS)" using Cons(2) by simp
     also have "finite (listset XS) \<longleftrightarrow> list_all finite XS" using Cons by simp
     also have "finite A \<and> \<dots> \<longleftrightarrow> list_all finite (A # XS)" by simp
     finally show ?case by this
   qed
+  lemma listset_finite'[intro]:
+    assumes "list_all finite XS"
+    shows "finite (listset XS)"
+    using infinite_imp_nonempty assms by blast
   lemma listset_card[simp]: "card (listset XS) = prod_list (map card XS)"
   proof (induct XS)
     case Nil
     show ?case by simp
   next
     case (Cons A XS)
     have 1: "inj (case_prod Cons)" unfolding inj_def by simp
     have "listset (A # XS) = case_prod Cons ` (A \<times> listset XS)" by (auto simp: set_Cons_def)
     also have "card \<dots> = card (A \<times> listset XS)" using card_image 1 by auto
     also have "\<dots> = card A * card (listset XS)" using card_cartesian_product by this
     also have "card (listset XS) = prod_list (map card XS)" using Cons by this
     also have "card A * \<dots> = prod_list (map card (A # XS))" by simp
     finally show ?case by this
   qed
 
   subsection \<open>Stream Basics\<close>
 
   declare stream.map_id[simp]
   declare stream.set_map[simp]
   declare stream.set_sel(1)[intro!, simp]
   declare stream.pred_True[simp]
   declare stream.pred_map[iff]
   declare stream.rel_map[iff]
   declare shift_simps[simp del]
   declare stake_sdrop[simp]
   declare stake_siterate[simp del]
   declare sdrop_snth[simp]
 
   lemma stream_pred_cases:
     assumes "pred_stream P xs"
     obtains (scons) y ys where "xs = y ## ys" "P y" "pred_stream P ys"
     using assms by (cases xs) (auto)
 
   lemma stream_rel_coinduct[case_names stream_rel, coinduct pred: stream_all2]:
     assumes "R u v"
     assumes "\<And> a u b v. R (a ## u) (b ## v) \<Longrightarrow> P a b \<and> R u v"
     shows "stream_all2 P u v"
     using assms by (coinduct) (metis stream.collapse)
   lemma stream_rel_coinduct_shift[case_names stream_rel, consumes 1]:
     assumes "R u v"
     assumes "\<And> u v. R u v \<Longrightarrow>
       \<exists> u\<^sub>1 u\<^sub>2 v\<^sub>1 v\<^sub>2. u = u\<^sub>1 @- u\<^sub>2 \<and> v = v\<^sub>1 @- v\<^sub>2 \<and> u\<^sub>1 \<noteq> [] \<and> v\<^sub>1 \<noteq> [] \<and> list_all2 P u\<^sub>1 v\<^sub>1 \<and> R u\<^sub>2 v\<^sub>2"
     shows "stream_all2 P u v"
   proof -
     have "\<exists> u\<^sub>1 u\<^sub>2 v\<^sub>1 v\<^sub>2. u = u\<^sub>1 @- u\<^sub>2 \<and> v = v\<^sub>1 @- v\<^sub>2 \<and> list_all2 P u\<^sub>1 v\<^sub>1 \<and> R u\<^sub>2 v\<^sub>2"
       using assms(1) by force
     then show ?thesis using assms(2) by (coinduct) (force elim: list.rel_cases)
   qed
 
   lemma stream_pred_coinduct[case_names stream_pred, coinduct pred: pred_stream]:
     assumes "R w"
     assumes "\<And> a w. R (a ## w) \<Longrightarrow> P a \<and> R w"
     shows "pred_stream P w"
     using assms unfolding stream.pred_rel eq_onp_def by (coinduction arbitrary: w) (auto)
   lemma stream_pred_coinduct_shift[case_names stream_pred, consumes 1]:
     assumes "R w"
     assumes "\<And> w. R w \<Longrightarrow> \<exists> u v. w = u @- v \<and> u \<noteq> [] \<and> list_all P u \<and> R v"
     shows "pred_stream P w"
   proof -
     have "\<exists> u v. w = u @- v \<and> list_all P u \<and> R v"
       using assms(1) by (metis list_all_simps(2) shift.simps(1))
     then show ?thesis using assms(2) by (coinduct) (force elim: list_pred_cases)
   qed
   lemma stream_pred_flat_coinduct[case_names stream_pred, consumes 1]:
     assumes "R ws"
     assumes "\<And> w ws. R (w ## ws) \<Longrightarrow> w \<noteq> [] \<and> list_all P w \<and> R ws"
     shows "pred_stream P (flat ws)"
     using assms
     by (coinduction arbitrary: ws rule: stream_pred_coinduct_shift) (metis stream.exhaust flat_Stream)
 
   lemmas stream_eq_coinduct[case_names stream_eq, coinduct pred: HOL.eq] =
     stream_rel_coinduct[where ?P = HOL.eq, unfolded stream.rel_eq]
   lemmas stream_eq_coinduct_shift[case_names stream_eq, consumes 1] =
     stream_rel_coinduct_shift[where ?P = HOL.eq, unfolded stream.rel_eq list.rel_eq]
 
   lemma stream_pred_shift[iff]: "pred_stream P (u @- v) \<longleftrightarrow> list_all P u \<and> pred_stream P v"
     by (induct u) (auto)
   lemma stream_rel_shift[iff]:
     assumes "length u\<^sub>1 = length v\<^sub>1"
     shows "stream_all2 P (u\<^sub>1 @- u\<^sub>2) (v\<^sub>1 @- v\<^sub>2) \<longleftrightarrow> list_all2 P u\<^sub>1 v\<^sub>1 \<and> stream_all2 P u\<^sub>2 v\<^sub>2"
     using assms by (induct rule: list_induct2) (auto)
 
   lemma sset_subset_stream_pred: "sset w \<subseteq> A \<longleftrightarrow> pred_stream (\<lambda> a. a \<in> A) w"
     unfolding stream.pred_set by auto
 
   lemma eq_scons: "w = a ## v \<longleftrightarrow> a = shd w \<and> v = stl w" by auto
   lemma scons_eq: "a ## v = w \<longleftrightarrow> shd w = a \<and> stl w = v" by auto
   lemma eq_shift: "w = u @- v \<longleftrightarrow> stake (length u) w = u \<and> sdrop (length u) w = v"
     by (induct u arbitrary: w) (force+)
   lemma shift_eq: "u @- v = w \<longleftrightarrow> u = stake (length u) w \<and> v = sdrop (length u) w"
     by (induct u arbitrary: w) (force+)
   lemma scons_eq_shift: "a ## w = u @- v \<longleftrightarrow> ([] = u \<and> a ## w = v) \<or> (\<exists> u'. a # u' = u \<and> w = u' @- v)"
     by (cases u) (auto)
   lemma shift_eq_scons: "u @- v = a ## w \<longleftrightarrow> (u = [] \<and> v = a ## w) \<or> (\<exists> u'. u = a # u' \<and> u' @- v = w)"
     by (cases u) (auto)
 
   lemma stream_all2_sset1:
     assumes "stream_all2 P xs ys"
     shows "\<forall> x \<in> sset xs. \<exists> y \<in> sset ys. P x y"
   proof -
     have "pred_stream (\<lambda> x. \<exists> y \<in> S. P x y) xs" if "sset ys \<subseteq> S" for S
       using assms that by (coinduction arbitrary: xs ys) (force elim: stream.rel_cases)
     then show ?thesis unfolding stream.pred_set by auto
   qed
   lemma stream_all2_sset2:
     assumes "stream_all2 P xs ys"
     shows "\<forall> y \<in> sset ys. \<exists> x \<in> sset xs. P x y"
   proof -
     have "pred_stream (\<lambda> y. \<exists> x \<in> S. P x y) ys" if "sset xs \<subseteq> S" for S
       using assms that by (coinduction arbitrary: xs ys) (force elim: stream.rel_cases)
     then show ?thesis unfolding stream.pred_set by auto
   qed
 
   lemma smap_eq_scons[iff]: "smap f xs = y ## ys \<longleftrightarrow> f (shd xs) = y \<and> smap f (stl xs) = ys"
     using smap_ctr by metis
   lemma scons_eq_smap[iff]: "y ## ys = smap f xs \<longleftrightarrow> y = f (shd xs) \<and> ys = smap f (stl xs)"
     using smap_ctr by metis
   lemma smap_eq_shift[iff]:
     "smap f w = u @- v \<longleftrightarrow> (\<exists> w\<^sub>1 w\<^sub>2. w = w\<^sub>1 @- w\<^sub>2 \<and> map f w\<^sub>1 = u \<and> smap f w\<^sub>2 = v)"
     using sdrop_smap eq_shift stake_sdrop stake_smap by metis
   lemma shift_eq_smap[iff]:
     "u @- v = smap f w \<longleftrightarrow> (\<exists> w\<^sub>1 w\<^sub>2. w = w\<^sub>1 @- w\<^sub>2 \<and> u = map f w\<^sub>1 \<and> v = smap f w\<^sub>2)"
     using sdrop_smap eq_shift stake_sdrop stake_smap by metis
 
   lemma szip_eq_scons[iff]: "szip xs ys = z ## zs \<longleftrightarrow> (shd xs, shd ys) = z \<and> szip (stl xs) (stl ys) = zs"
     using szip.ctr stream.inject by metis
   lemma scons_eq_szip[iff]: "z ## zs = szip xs ys \<longleftrightarrow> z = (shd xs, shd ys) \<and> zs = szip (stl xs) (stl ys)"
     using szip.ctr stream.inject by metis
 
   lemma siterate_eq_scons[iff]: "siterate f s = a ## w \<longleftrightarrow> s = a \<and> siterate f (f s) = w"
     using siterate.ctr stream.inject by metis
   lemma scons_eq_siterate[iff]: "a ## w = siterate f s \<longleftrightarrow> a = s \<and> w = siterate f (f s)"
     using siterate.ctr stream.inject by metis
 
   lemma snth_0: "(a ## w) !! 0 = a" by simp
   lemma eqI_snth:
     assumes "\<And> i. u !! i = v !! i"
     shows "u = v"
     using assms by (coinduction arbitrary: u v) (metis stream.sel snth.simps)
 
   lemma stream_pred_snth: "pred_stream P w \<longleftrightarrow> (\<forall> i. P (w !! i))"
     unfolding stream.pred_set sset_range by simp
   lemma stream_rel_snth: "stream_all2 P u v \<longleftrightarrow> (\<forall> i. P (u !! i) (v !! i))"
   proof safe
     show "P (u !! i) (v !! i)" if "stream_all2 P u v" for i
       using that by (induct i arbitrary: u v) (auto elim: stream.rel_cases)
     show "stream_all2 P u v" if "\<forall> i. P (u !! i) (v !! i)"
       using that by (coinduct) (metis snth_0 snth_Stream)
   qed
 
   lemma stream_rel_pred_szip: "stream_all2 P u v \<longleftrightarrow> pred_stream (case_prod P) (szip u v)"
     unfolding stream_pred_snth stream_rel_snth by simp
 
   lemma sconst_eq[iff]: "sconst x = sconst y \<longleftrightarrow> x = y" by (auto) (metis siterate.simps(1))
   lemma stream_pred__sconst[iff]: "pred_stream P (sconst x) \<longleftrightarrow> P x"
     unfolding stream_pred_snth by simp
   lemma stream_rel_sconst[iff]: "stream_all2 P (sconst x) (sconst y) \<longleftrightarrow> P x y"
     unfolding stream_rel_snth by simp
 
   lemma set_sset_stake[intro!, simp]: "set (stake n xs) \<subseteq> sset xs"
     by (metis sset_shift stake_sdrop sup_ge1)
   lemma sset_sdrop[intro!, simp]: "sset (sdrop n xs) \<subseteq> sset xs"
     by (metis sset_shift stake_sdrop sup_ge2)
 
   lemma set_stake_snth: "x \<in> set (stake n xs) \<longleftrightarrow> (\<exists> i < n. xs !! i = x)"
     unfolding in_set_conv_nth by auto
 
   (* TODO: these should be generated by the transfer option on the primcorec definitions *)
   (* TODO: transfer_prover cannot handle corecursive definitions due to the \<lambda>(s1, s2). undefined
     abortion term that is never used *)
   lemma szip_transfer[transfer_rule]:
     includes lifting_syntax
     shows "(stream_all2 A ===> stream_all2 B ===> stream_all2 (rel_prod A B)) szip szip"
     by (intro rel_funI, coinduction) (force elim: stream.rel_cases)
   lemma siterate_transfer[transfer_rule]:
     includes lifting_syntax
     shows "((A ===> A) ===> A ===> stream_all2 A) siterate siterate"
     by (intro rel_funI, coinduction) (force dest: rel_funD)
 
   lemma split_stream_first:
     assumes "A \<inter> sset xs \<noteq> {}"
     obtains ys a zs
     where "xs = ys @- a ## zs" "A \<inter> set ys = {}" "a \<in> A"
   proof
     let ?n = "LEAST n. xs !! n \<in> A"
     have 1: "xs !! n \<notin> A" if "n < ?n" for n using that by (metis (full_types) not_less_Least)
     show "xs = stake ?n xs @- (xs !! ?n) ## sdrop (Suc ?n) xs" using id_stake_snth_sdrop by blast
     show "A \<inter> set (stake ?n xs) = {}" using 1 by (metis (no_types, lifting) disjoint_iff_not_equal set_stake_snth)
     show "xs !! ?n \<in> A" using assms unfolding sset_range by (auto intro: LeastI)
   qed
   lemma split_stream_first':
     assumes "x \<in> sset xs"
     obtains ys zs
     where "xs = ys @- x ## zs" "x \<notin> set ys"
   proof
     let ?n = "LEAST n. xs !! n = x"
     have 1: "xs !! ?n = x" using assms unfolding sset_range by (auto intro: LeastI)
     have 2: "xs !! n \<noteq> x" if "n < ?n" for n using that by (metis (full_types) not_less_Least)
     show "xs = stake ?n xs @- x ## sdrop (Suc ?n) xs" using 1 by (metis id_stake_snth_sdrop)
     show "x \<notin> set (stake ?n xs)" using 2 by (meson set_stake_snth)
   qed
 
   lemma streams_UNIV[iff]: "streams A = UNIV \<longleftrightarrow> A = UNIV"
   proof
     show "A = UNIV \<Longrightarrow> streams A = UNIV" by simp
   next
     assume "streams A = UNIV"
     then have "w \<in> streams A" for w by simp
     then have "sset w \<subseteq> A" for w unfolding streams_iff_sset by this
     then have "sset (sconst a) \<subseteq> A" for a by blast
     then have "a \<in> A" for a by simp
     then show "A = UNIV" by auto
   qed
 
   lemma pred_list_listsp[pred_set_conv]: "list_all = listsp"
     unfolding list.pred_set by auto
   lemma pred_stream_streamsp[pred_set_conv]: "pred_stream = streamsp"
     unfolding stream.pred_set streams_iff_sset[to_pred] by auto
 
   subsection \<open>The scan Function\<close>
 
   primrec (transfer) scan :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b list" where
     "scan f [] a = []" | "scan f (x # xs) a = f x a # scan f xs (f x a)"
 
   lemma scan_append[simp]: "scan f (xs @ ys) a = scan f xs a @ scan f ys (fold f xs a)"
     by (induct xs arbitrary: a) (auto)
 
   lemma scan_eq_nil[iff]: "scan f xs a = [] \<longleftrightarrow> xs = []" by (cases xs) (auto)
   lemma scan_eq_cons[iff]:
     "scan f xs a = b # w \<longleftrightarrow> (\<exists> y ys. xs = y # ys \<and> f y a = b \<and> scan f ys (f y a) = w)"
     by (cases xs) (auto)
   lemma scan_eq_append[iff]:
     "scan f xs a = u @ v \<longleftrightarrow> (\<exists> ys zs. xs = ys @ zs \<and> scan f ys a = u \<and> scan f zs (fold f ys a) = v)"
     by (induct u arbitrary: xs a) (auto, metis append_Cons fold_simps(2), blast)
 
   lemma scan_length[simp]: "length (scan f xs a) = length xs"
     by (induct xs arbitrary: a) (auto)
   (* TODO: figure out how this is used, should it be a simp rule? or flipped? also target_alt_def *)
   lemma scan_last: "last (a # scan f xs a) = fold f xs a"
     by (induct xs arbitrary: a) (auto simp: last.simps)
   lemma scan_butlast[simp]: "scan f (butlast xs) a = butlast (scan f xs a)"
     by (induct xs arbitrary: a) (auto simp: butlast.simps)
 
   lemma scan_const[simp]: "scan const xs a = xs"
     by (induct xs arbitrary: a) (auto)
   lemma scan_nth[simp]:
     assumes "i < length (scan f xs a)"
     shows "scan f xs a ! i = fold f (take (Suc i) xs) a"
     using assms by (cases xs, simp, induct i arbitrary: xs a, auto simp: take_Suc neq_Nil_conv)
   lemma scan_map[simp]: "scan f (map g xs) a = scan (f \<circ> g) xs a"
     by (induct xs arbitrary: a) (auto)
   lemma scan_take[simp]: "take k (scan f xs a) = scan f (take k xs) a"
     by (induct k arbitrary: xs a) (auto simp: take_Suc neq_Nil_conv)
   lemma scan_drop[simp]: "drop k (scan f xs a) = scan f (drop k xs) (fold f (take k xs) a)"
     by (induct k arbitrary: xs a) (auto simp: take_Suc neq_Nil_conv)
 
   primcorec (transfer) sscan :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a stream \<Rightarrow> 'b \<Rightarrow> 'b stream" where
     "sscan f xs a = f (shd xs) a ## sscan f (stl xs) (f (shd xs) a)"
 
   lemma sscan_scons[simp]: "sscan f (x ## xs) a = f x a ## sscan f xs (f x a)"
     by (simp add: stream.expand)
   lemma sscan_shift[simp]: "sscan f (xs @- ys) a = scan f xs a @- sscan f ys (fold f xs a)"
     by (induct xs arbitrary: a) (auto)
 
   lemma sscan_eq_scons[iff]:
     "sscan f xs a = b ## w \<longleftrightarrow> f (shd xs) a = b \<and> sscan f (stl xs) (f (shd xs) a) = w"
     using sscan.ctr stream.inject by metis
   lemma scons_eq_sscan[iff]:
     "b ## w = sscan f xs a \<longleftrightarrow> b = f (shd xs) a \<and> w = sscan f (stl xs) (f (shd xs) a)"
     using sscan.ctr stream.inject by metis
 
   lemma sscan_const[simp]: "sscan const xs a = xs"
     by (coinduction arbitrary: xs a) (auto)
   lemma sscan_snth[simp]: "sscan f xs a !! i = fold f (stake (Suc i) xs) a"
     by (induct i arbitrary: xs a) (auto)
   lemma sscan_scons_snth[simp]: "(a ## sscan f xs a) !! i = fold f (stake i xs) a"
     by (induct i arbitrary: xs a) (auto)
   lemma sscan_smap[simp]: "sscan f (smap g xs) a = sscan (f \<circ> g) xs a"
     by (coinduction arbitrary: xs a) (auto)
   lemma sscan_stake[simp]: "stake k (sscan f xs a) = scan f (stake k xs) a"
     by (induct k arbitrary: a xs) (auto)
   lemma sscan_sdrop[simp]: "sdrop k (sscan f xs a) = sscan f (sdrop k xs) (fold f (stake k xs) a)"
     by (induct k arbitrary: a xs) (auto)
 
+  subsection \<open>Transposing Streams\<close>
+
+  primcorec (transfer) stranspose :: "'a stream list \<Rightarrow> 'a list stream" where
+    "stranspose ws = map shd ws ## stranspose (map stl ws)"
+
+  lemma stranspose_eq_scons[iff]: "stranspose ws = a ## w \<longleftrightarrow> map shd ws = a \<and> stranspose (map stl ws) = w"
+    using stranspose.ctr stream.inject by metis
+  lemma scons_eq_stranspose[iff]: "a ## w = stranspose ws \<longleftrightarrow> a = map shd ws \<and> w = stranspose (map stl ws)"
+    using stranspose.ctr stream.inject by metis
+
+  lemma stranspose_nil[simp]: "stranspose [] = sconst []" by coinduction auto
+  lemma stranspose_cons[simp]: "stranspose (w # ws) = smap2 Cons w (stranspose ws)"
+    by (coinduction arbitrary: w ws) (metis list.simps(9) smap2.simps stranspose.simps stream.sel)
+
+  lemma snth_stranspose[simp]: "stranspose ws !! k = map (\<lambda> w. w !! k) ws" by (induct k arbitrary: ws) (auto)
+  lemma stranspose_nth[simp]:
+    assumes "k < length ws"
+    shows "smap (\<lambda> xs. xs ! k) (stranspose ws) = ws ! k"
+    using assms by (auto intro: eqI_snth)
+
   subsection \<open>Distinct Streams\<close>
 
   coinductive sdistinct :: "'a stream \<Rightarrow> bool" where
     scons[intro!]: "x \<notin> sset xs \<Longrightarrow> sdistinct xs \<Longrightarrow> sdistinct (x ## xs)"
 
   lemma sdistinct_scons_elim[elim!]:
     assumes "sdistinct (x ## xs)"
     obtains "x \<notin> sset xs" "sdistinct xs"
     using assms by (auto elim: sdistinct.cases)
 
   lemma sdistinct_coinduct[case_names sdistinct, coinduct pred: sdistinct]:
     assumes "P xs"
     assumes "\<And> x xs. P (x ## xs) \<Longrightarrow> x \<notin> sset xs \<and> P xs"
     shows "sdistinct xs"
     using stream.collapse sdistinct.coinduct assms by metis
 
   lemma sdistinct_shift[intro!]:
     assumes "distinct xs" "sdistinct ys" "set xs \<inter> sset ys = {}"
     shows "sdistinct (xs @- ys)"
     using assms by (induct xs) (auto)
   lemma sdistinct_shift_elim[elim!]:
     assumes "sdistinct (xs @- ys)"
     obtains "distinct xs" "sdistinct ys" "set xs \<inter> sset ys = {}"
     using assms by (induct xs) (auto)
 
   lemma sdistinct_infinite_sset:
     assumes "sdistinct w"
     shows "infinite (sset w)"
     using assms by (coinduction arbitrary: w) (force elim: sdistinct.cases)
 
   lemma not_sdistinct_decomp:
     assumes "\<not> sdistinct w"
     obtains u v a w'
     where "w = u @- a ## v @- a ## w'"
   proof (rule ccontr)
     assume 1: "\<not> thesis"
     assume 2: "w = u @- a ## v @- a ## w' \<Longrightarrow> thesis" for u a v w'
     have 3: "\<forall> u v a w'. w \<noteq> u @- a ## v @- a ## w'" using 1 2 by auto
     have 4: "sdistinct w" using 3 by (coinduct) (metis id_stake_snth_sdrop imageE shift.simps sset_range)
     show False using assms 4 by auto
   qed
 
   subsection \<open>Sorted Streams\<close>
 
   coinductive (in order) sascending :: "'a stream \<Rightarrow> bool" where
     "a \<le> b \<Longrightarrow> sascending (b ## w) \<Longrightarrow> sascending (a ## b ## w)"
 
   coinductive (in order) sdescending :: "'a stream \<Rightarrow> bool" where
     "a \<ge> b \<Longrightarrow> sdescending (b ## w) \<Longrightarrow> sdescending (a ## b ## w)"
 
   lemma sdescending_coinduct[case_names sdescending, coinduct pred: sdescending]:
     assumes "P w"
     assumes "\<And> a b w. P (a ## b ## w) \<Longrightarrow> a \<ge> b \<and> P (b ## w)"
     shows "sdescending w"
     using stream.collapse sdescending.coinduct assms by (metis (no_types))
 
   lemma sdescending_sdrop:
     assumes "sdescending w"
     shows "sdescending (sdrop k w)"
     using assms by (induct k) (auto, metis sdescending.cases sdrop_stl stream.sel(2))
 
   lemma sdescending_snth_antimono:
     assumes "sdescending w"
     shows "antimono (snth w)"
   unfolding antimono_iff_le_Suc
   proof
     fix k
     have "sdescending (sdrop k w)" using sdescending_sdrop assms by this
     then obtain a b v where 2: "sdrop k w = a ## b ## v" "a \<ge> b" by rule
     then show "w !! k \<ge> w !! Suc k" by (metis sdrop_simps stream.sel)
   qed
 
   lemma sdescending_stuck:
     fixes w :: "'a :: wellorder stream"
     assumes "sdescending w"
     obtains k
     where "sdrop k w = sconst (w !! k)"
   using assms
   proof (induct "w !! 0" arbitrary: w thesis rule: less_induct)
     case less
     show ?case
     proof (cases "w = sconst (w !! 0)")
       case True
       show ?thesis using less(2)[of 0] True by simp
     next
       case False
       obtain k where 1: "w !! k \<noteq> w !! 0"
         using False by (metis empty_iff eqI_snth insert_iff snth_sset sset_sconst)
       have 2: "antimono (snth w)" using sdescending_snth_antimono less(3) by this
       have 3: "w !! k \<le> w !! 0" using 1 2 by (blast dest: antimonoD)
       have 4: "sdrop k w !! 0 < w !! 0" using 1 3 by auto
       have 5: "sdescending (sdrop k w)" using sdescending_sdrop less(3) by this
       obtain l where 5: "sdrop l (sdrop k w) = sconst (sdrop k w !! l)"
         using less(1)[OF 4 _ 5] by this
       show ?thesis using less(2) 5 by simp
     qed
   qed
 
 end
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,143 +1,159 @@
 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 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