diff --git a/thys/Buchi_Complementation/Ranking.thy b/thys/Buchi_Complementation/Ranking.thy --- a/thys/Buchi_Complementation/Ranking.thy +++ b/thys/Buchi_Complementation/Ranking.thy @@ -1,481 +1,481 @@ section \Rankings\ theory Ranking imports "Alternate" "Graph" begin subsection \Rankings\ type_synonym 'state ranking = "'state node \ nat" definition ranking :: "('label, 'state) nba \ 'label stream \ 'state ranking \ bool" where "ranking A w f \ (\ v \ gunodes A w. f v \ 2 * card (nodes A)) \ (\ v \ gunodes A w. \ u \ gusuccessors A w v. f u \ f v) \ (\ v \ gunodes A w. gaccepting A v \ even (f v)) \ (\ v \ gunodes A w. \ r k. gurun A w r v \ smap f (gtrace r v) = sconst k \ odd k)" subsection \Ranking Implies Word not in Language\ lemma ranking_stuck: assumes "ranking A w f" assumes "v \ gunodes A w" "gurun A w r v" obtains n k where "smap f (gtrace (sdrop n r) (gtarget (stake n r) v)) = sconst k" proof - have 0: "f u \ f v" if "v \ gunodes A w" "u \ gusuccessors A w v" for v u using assms(1) that unfolding ranking_def by auto have 1: "shd (v ## gtrace r v) \ gunodes A w" using assms(2) by auto have 2: "sdescending (smap f (v ## gtrace r v))" using 1 assms(3) proof (coinduction arbitrary: r v rule: sdescending.coinduct) case sdescending obtain u s where 1: "r = u ## s" using stream.exhaust by blast have 2: "v \ gunodes A w" using sdescending(1) by simp have 3: "gurun A w (u ## s) v" using sdescending(2) 1 by auto have 4: "u \ gusuccessors A w v" using 3 by auto have 5: "u \ gureachable A w v" using graph.reachable_successors 4 by blast show ?case unfolding 1 proof (intro exI conjI disjI1) show "f u \ f v" using 0 2 4 by this show "shd (u ## gtrace s u) \ gunodes A w" using 2 5 by auto show "gurun A w s u" using 3 by auto qed auto qed obtain n k where 3: "sdrop n (smap f (v ## gtrace r v)) = sconst k" using sdescending_stuck[OF 2] by metis have "gtrace (sdrop (Suc n) r) (gtarget (stake (Suc n) r) v) = sdrop (Suc n) (gtrace r v)" using sscan_sdrop by rule also have "smap f \ = sdrop n (smap f (v ## gtrace r v))" by (auto, metis 3 id_apply sdrop_smap sdrop_stl siterate.simps(2) sscan_const stream.map stream.map_sel(2) stream.sel(2)) also have "\ = sconst k" using 3 by this finally show ?thesis using that by blast qed lemma ranking_stuck_odd: assumes "ranking A w f" assumes "v \ gunodes A w" "gurun A w r v" obtains n where "sset (smap f (gtrace (sdrop n r) (gtarget (stake n r) v))) \ Collect odd" proof - obtain n k where 1: "smap f (gtrace (sdrop n r) (gtarget (stake n r) v)) = sconst k" using ranking_stuck assms by this have 2: "gtarget (stake n r) v \ gunodes A w" using assms(2, 3) by (simp add: graph.nodes_target graph.run_stake) have 3: "gurun A w (sdrop n r) (gtarget (stake n r) v)" using assms(2, 3) by (simp add: graph.run_sdrop) have 4: "odd k" using 1 2 3 assms(1) unfolding ranking_def by meson have "sset (smap f (gtrace (sdrop n r) (gtarget (stake n r) v))) = sset (sconst k)" unfolding 1 by rule also have "\ \ Collect odd" using 4 by simp finally show ?thesis using that by simp qed lemma ranking_language: assumes "ranking A w f" shows "w \ language A" proof assume 1: "w \ language A" obtain r p where 2: "run A (w ||| r) p" "p \ initial A" "infs (accepting A) (trace (w ||| r) p)" using 1 by rule let ?r = "fromN 1 ||| r" let ?v = "(0, p)" have 3: "?v \ gunodes A w" "gurun A w ?r ?v" using 2(1, 2) by (auto intro: run_grun) obtain n where 4: "sset (smap f (gtrace (sdrop n ?r) (gtarget (stake n ?r) ?v))) \ {a. odd a}" using ranking_stuck_odd assms 3 by this let ?s = "stake n ?r" let ?t = "sdrop n ?r" let ?u = "gtarget ?s ?v" have "sset (gtrace ?t ?u) \ gureachable A w ?v" proof (intro graph.reachable_trace graph.reachable_target graph.reachable.reflexive) show "gupath A w ?s ?v" using graph.run_stake 3(2) by this show "gurun A w ?t ?u" using graph.run_sdrop 3(2) by this qed also have "\ \ gunodes A w" using 3(1) by blast finally have 7: "sset (gtrace ?t ?u) \ gunodes A w" by this have 8: "\ p. p \ gunodes A w \ gaccepting A p \ even (f p)" using assms unfolding ranking_def by auto have 9: "\ p. p \ sset (gtrace ?t ?u) \ gaccepting A p \ even (f p)" using 7 8 by auto have 19: "infs (accepting A) (smap snd ?r)" using 2(3) unfolding trace_alt_def by simp - have 18: "infs (gaccepting A) ?r" using 19 by force + have 18: "infs (gaccepting A) ?r" using 19 by (force simp: comp_def) have 17: "infs (gaccepting A) (gtrace ?r ?v)" using 18 unfolding gtrace_alt_def by this have 16: "infs (gaccepting A) (gtrace (?s @- ?t) ?v)" using 17 unfolding stake_sdrop by this have 15: "infs (gaccepting A) (gtrace ?t ?u)" using 16 by simp have 13: "infs (even \ f) (gtrace ?t ?u)" using infs_mono[OF _ 15] 9 by simp - have 12: "infs even (smap f (gtrace ?t ?u))" using 13 by simp + have 12: "infs even (smap f (gtrace ?t ?u))" using 13 by (simp add: comp_def) have 11: "Bex (sset (smap f (gtrace ?t ?u))) even" using 12 infs_any by metis show False using 4 11 by auto qed subsection \Word not in Language implies Ranking\ subsubsection \Removal of Endangered Nodes\ definition clean :: "('label, 'state) nba \ 'label stream \ 'state node set \ 'state node set" where "clean A w V \ {v \ V. infinite (greachable A w V v)}" lemma clean_decreasing: "clean A w V \ V" unfolding clean_def by auto lemma clean_successors: assumes "v \ V" "u \ gusuccessors A w v" shows "u \ clean A w V \ v \ clean A w V" proof - assume 1: "u \ clean A w V" have 2: "u \ V" "infinite (greachable A w V u)" using 1 unfolding clean_def by auto have 3: "u \ greachable A w V v" using graph.reachable.execute assms(2) 2(1) by blast have 4: "greachable A w V u \ greachable A w V v" using 3 by blast have 5: "infinite (greachable A w V v)" using 2(2) 4 by (simp add: infinite_super) show "v \ clean A w V" unfolding clean_def using assms(1) 5 by simp qed subsubsection \Removal of Safe Nodes\ definition prune :: "('label, 'state) nba \ 'label stream \ 'state node set \ 'state node set" where "prune A w V \ {v \ V. \ u \ greachable A w V v. gaccepting A u}" lemma prune_decreasing: "prune A w V \ V" unfolding prune_def by auto lemma prune_successors: assumes "v \ V" "u \ gusuccessors A w v" shows "u \ prune A w V \ v \ prune A w V" proof - assume 1: "u \ prune A w V" have 2: "u \ V" "\ x \ greachable A w V u. gaccepting A x" using 1 unfolding prune_def by auto have 3: "u \ greachable A w V v" using graph.reachable.execute assms(2) 2(1) by blast have 4: "greachable A w V u \ greachable A w V v" using 3 by blast show "v \ prune A w V" unfolding prune_def using assms(1) 2(2) 4 by auto qed subsubsection \Run Graph Interation\ definition graph :: "('label, 'state) nba \ 'label stream \ nat \ 'state node set" where "graph A w k \ alternate (clean A w) (prune A w) k (gunodes A w)" abbreviation "level A w k l \ {v \ graph A w k. fst v = l}" lemma graph_0[simp]: "graph A w 0 = gunodes A w" unfolding graph_def by simp lemma graph_Suc[simp]: "graph A w (Suc k) = (if even k then clean A w else prune A w) (graph A w k)" unfolding graph_def by simp lemma graph_antimono: "antimono (graph A w)" using alternate_antimono clean_decreasing prune_decreasing unfolding antimono_def le_fun_def graph_def by metis lemma graph_nodes: "graph A w k \ gunodes A w" using graph_0 graph_antimono le0 antimonoD by metis lemma graph_successors: assumes "v \ gunodes A w" "u \ gusuccessors A w v" shows "u \ graph A w k \ v \ graph A w k" using assms proof (induct k arbitrary: u v) case 0 show ?case using 0(2) by simp next case (Suc k) have 1: "v \ graph A w k" using Suc using antimono_iff_le_Suc graph_antimono rev_subsetD by blast show ?case using Suc(2) clean_successors[OF 1 Suc(4)] prune_successors[OF 1 Suc(4)] by auto qed lemma graph_level_finite: assumes "finite (nodes A)" shows "finite (level A w k l)" proof - have "level A w k l \ {v \ gunodes A w. fst v = l}" by (simp add: graph_nodes subset_CollectI) also have "{v \ gunodes A w. fst v = l} \ {l} \ nodes A" using gnodes_nodes by force also have "finite ({l} \ nodes A)" using assms(1) by simp finally show ?thesis by this qed lemma find_safe: assumes "w \ language A" assumes "V \ {}" "V \ gunodes A w" assumes "\ v. v \ V \ gsuccessors A w V v \ {}" obtains v where "v \ V" "\ u \ greachable A w V v. \ gaccepting A u" proof (rule ccontr) assume 1: "\ thesis" have 2: "\ v. v \ V \ \ u \ greachable A w V v. gaccepting A u" using that 1 by auto have 3: "\ r v. v \ initial A \ run A (w ||| r) v \ \ infs (accepting A) (trace (w ||| r) v)" using assms(1) by auto obtain v where 4: "v \ V" using assms(2) by force obtain x where 5: "x \ greachable A w V v" "gaccepting A x" using 2 4 by blast obtain y where 50: "gpath A w V y v" "x = gtarget y v" using 5(1) by rule obtain r where 6: "grun A w V r x" "infs (\ x. x \ V \ gaccepting A x) r" proof (rule graph.recurring_condition) show "x \ V \ gaccepting A x" using greachable_subset 4 5 by blast next fix v assume 1: "v \ V \ gaccepting A v" obtain v' where 20: "v' \ gsuccessors A w V v" using assms(4) 1 by (meson IntE equals0I) have 21: "v' \ V" using 20 by auto have 22: "\ u \ greachable A w V v'. u \ V \ gaccepting A u" using greachable_subset 2 21 by blast obtain r where 30: "gpath A w V r v'" "gtarget r v' \ V \ gaccepting A (gtarget r v')" using 22 by blast show "\ r. r \ [] \ gpath A w V r v \ gtarget r v \ V \ gaccepting A (gtarget r v)" proof (intro exI conjI) show "v' # r \ []" by simp show "gpath A w V (v' # r) v" using 20 30 by auto show "gtarget (v' # r) v \ V" using 30 by simp show "gaccepting A (gtarget (v' # r) v)" using 30 by simp qed qed auto obtain u where 100: "u \ ginitial A" "v \ gureachable A w u" using 4 assms(3) by blast have 101: "gupath A w y v" using gpath_subset 50(1) subset_UNIV by this have 102: "gurun A w r x" using grun_subset 6(1) subset_UNIV by this obtain t where 103: "gupath A w t u" "v = gtarget t u" using 100(2) by rule have 104: "gurun A w (t @- y @- r) u" using 101 102 103 50(2) by auto obtain s q where 7: "t @- y @- r = fromN (Suc 0) ||| s" "u = (0, q)" using grun_elim[OF 104] 100(1) by blast have 8: "run A (w ||| s) q" using grun_run[OF 104[unfolded 7]] by simp have 9: "q \ initial A" using 100(1) 7(2) by auto have 91: "sset (trace (w ||| s) q) \ reachable A q" using nba.reachable_trace nba.reachable.reflexive 8 by this have 10: "\ infs (accepting A) (trace (w ||| s) q)" using 3 9 8 by this have 11: "\ infs (accepting A) s" using 10 unfolding trace_alt_def by simp have 12: "infs (gaccepting A) r" using infs_mono[OF _ 6(2)] by simp have "s = smap snd (t @- y @- r)" unfolding 7(1) by simp - also have "infs (accepting A) \" using 12 by simp + also have "infs (accepting A) \" using 12 by (simp add: comp_def) finally have 13: "infs (accepting A) s" by this show False using 11 13 by simp qed lemma remove_run: assumes "finite (nodes A)" "w \ language A" assumes "V \ gunodes A w" "clean A w V \ {}" obtains v r where "grun A w V r v" "sset (gtrace r v) \ clean A w V" "sset (gtrace r v) \ - prune A w (clean A w V)" proof - obtain u where 1: "u \ clean A w V" "\ x \ greachable A w (clean A w V) u. \ gaccepting A x" proof (rule find_safe) show "w \ language A" using assms(2) by this show "clean A w V \ {}" using assms(4) by this show "clean A w V \ gunodes A w" using assms(3) by (meson clean_decreasing subset_iff) next fix v assume 1: "v \ clean A w V" have 2: "v \ V" using 1 clean_decreasing by blast have 3: "infinite (greachable A w V v)" using 1 clean_def by auto have "gsuccessors A w V v \ gusuccessors A w v" by auto also have "finite \" using 2 assms(1, 3) finite_nodes_gsuccessors by blast finally have 4: "finite (gsuccessors A w V v)" by this have 5: "infinite (insert v (\((greachable A w V) ` (gsuccessors A w V v))))" using graph.reachable_step 3 by metis obtain u where 6: "u \ gsuccessors A w V v" "infinite (greachable A w V u)" using 4 5 by auto have 7: "u \ clean A w V" using 6 unfolding clean_def by auto show "gsuccessors A w (clean A w V) v \ {}" using 6(1) 7 by auto qed auto have 2: "u \ V" using 1(1) unfolding clean_def by auto have 3: "infinite (greachable A w V u)" using 1(1) unfolding clean_def by simp have 4: "finite (gsuccessors A w V v)" if "v \ greachable A w V u" for v proof - have 1: "v \ V" using that greachable_subset 2 by blast have "gsuccessors A w V v \ gusuccessors A w v" by auto also have "finite \" using 1 assms(1, 3) finite_nodes_gsuccessors by blast finally show ?thesis by this qed obtain r where 5: "grun A w V r u" using graph.koenig[OF 3 4] by this have 6: "greachable A w V u \ V" using 2 greachable_subset by blast have 7: "sset (gtrace r u) \ V" using graph.reachable_trace[OF graph.reachable.reflexive 5(1)] 6 by blast have 8: "sset (gtrace r u) \ clean A w V" unfolding clean_def using 7 infinite_greachable_gtrace[OF 5(1)] by auto have 9: "sset (gtrace r u) \ greachable A w (clean A w V) u" using 5 8 by (metis graph.reachable.reflexive graph.reachable_trace grun_subset) show ?thesis proof show "grun A w V r u" using 5(1) by this show "sset (gtrace r u) \ clean A w V" using 8 by this show "sset (gtrace r u) \ - prune A w (clean A w V)" proof (intro subsetI ComplI) fix p assume 10: "p \ sset (gtrace r u)" "p \ prune A w (clean A w V)" have 20: "\ x \ greachable A w (clean A w V) p. gaccepting A x" using 10(2) unfolding prune_def by auto have 30: "greachable A w (clean A w V) p \ greachable A w (clean A w V) u" using 10(1) 9 by blast show "False" using 1(2) 20 30 by force qed qed qed lemma level_bounded: assumes "finite (nodes A)" "w \ language A" obtains n where "\ l. l \ n \ card (level A w (2 * k) l) \ card (nodes A) - k" proof (induct k arbitrary: thesis) case (0) show ?case proof (rule 0) fix l :: nat have "finite ({l} \ nodes A)" using assms(1) by simp also have "level A w 0 l \ {l} \ nodes A" using gnodes_nodes by force also (card_mono) have "card \ = card (nodes A)" using assms(1) by simp finally show "card (level A w (2 * 0) l) \ card (nodes A) - 0" by simp qed next case (Suc k) show ?case proof (cases "graph A w (Suc (2 * k)) = {}") case True have 3: "graph A w (2 * Suc k) = {}" using True prune_decreasing by simp blast show ?thesis using Suc(2) 3 by simp next case False obtain v r where 1: "grun A w (graph A w (2 * k)) r v" "sset (gtrace r v) \ graph A w (Suc (2 * k))" "sset (gtrace r v) \ - graph A w (Suc (Suc (2 * k)))" proof (rule remove_run) show "finite (nodes A)" "w \ language A" using assms by this show "clean A w (graph A w (2 * k)) \ {}" using False by simp show "graph A w (2 * k) \ gunodes A w" using graph_nodes by this qed auto obtain l q where 2: "v = (l, q)" by force obtain n where 90: "\ l. n \ l \ card (level A w (2 * k) l) \ card (nodes A) - k" using Suc(1) by blast show ?thesis proof (rule Suc(2)) fix j assume 100: "n + Suc l \ j" have 6: "graph A w (Suc (Suc (2 * k))) \ graph A w (Suc (2 * k))" using graph_antimono antimono_iff_le_Suc by blast have 101: "gtrace r v !! (j - Suc l) \ graph A w (Suc (2 * k))" using 1(2) snth_sset by auto have 102: "gtrace r v !! (j - Suc l) \ graph A w (Suc (Suc (2 * k)))" using 1(3) snth_sset by blast have 103: "gtrace r v !! (j - Suc l) \ level A w (Suc (2 * k)) j" using 1(1) 100 101 2 by (auto elim: grun_elim) have 104: "gtrace r v !! (j - Suc l) \ level A w (Suc (Suc (2 * k))) j" using 100 102 by simp have "level A w (2 * Suc k) j = level A w (Suc (Suc (2 * k))) j" by simp also have "\ \ level A w (Suc (2 * k)) j" using 103 104 6 by blast also have "\ \ level A w (2 * k) j" by (simp add: Collect_mono clean_def) finally have 105: "level A w (2 * Suc k) j \ level A w (2 * k) j" by this have "card (level A w (2 * Suc k) j) < card (level A w (2 * k) j)" using assms(1) 105 by (simp add: graph_level_finite psubset_card_mono) also have "\ \ card (nodes A) - k" using 90 100 by simp finally show "card (level A w (2 * Suc k) j) \ card (nodes A) - Suc k" by simp qed qed qed lemma graph_empty: assumes "finite (nodes A)" "w \ language A" shows "graph A w (Suc (2 * card (nodes A))) = {}" proof - obtain n where 1: "\ l. l \ n \ card (level A w (2 * card (nodes A)) l) = 0" using level_bounded[OF assms(1, 2), of "card (nodes A)"] by auto have "graph A w (2 * card (nodes A)) = (\ l \ {..< n}. level A w (2 * card (nodes A)) l) \ (\ l \ {n ..}. level A w (2 * card (nodes A)) l)" by auto also have "(\ l \ {n ..}. level A w (2 * card (nodes A)) l) = {}" using graph_level_finite assms(1) 1 by fastforce also have "finite ((\ l \ {..< n}. level A w (2 * card (nodes A)) l) \ {})" using graph_level_finite assms(1) by auto finally have 100: "finite (graph A w (2 * card (nodes A)))" by this have 101: "finite (greachable A w (graph A w (2 * card (nodes A))) v)" for v using 100 greachable_subset[of A w "graph A w (2 * card (nodes A))" v] using finite_insert infinite_super by auto show ?thesis using 101 by (simp add: clean_def) qed lemma graph_le: assumes "finite (nodes A)" "w \ language A" assumes "v \ graph A w k" shows "k \ 2 * card (nodes A)" using graph_empty graph_antimono assms by (metis (no_types, lifting) Suc_leI antimono_def basic_trans_rules(30) empty_iff not_le_imp_less) subsection \Node Ranks\ definition rank :: "('label, 'state) nba \ 'label stream \ 'state node \ nat" where "rank A w v \ GREATEST k. v \ graph A w k" lemma rank_member: assumes "finite (nodes A)" "w \ language A" "v \ gunodes A w" shows "v \ graph A w (rank A w v)" unfolding rank_def proof (rule GreatestI_nat) show "v \ graph A w 0" using assms(3) by simp show "\ k. v \ graph A w k \ k \ 2 * card (nodes A)" using graph_le assms(1, 2) by blast qed lemma rank_removed: assumes "finite (nodes A)" "w \ language A" shows "v \ graph A w (Suc (rank A w v))" proof assume "v \ graph A w (Suc (rank A w v))" then have 2: "Suc (rank A w v) \ rank A w v" unfolding rank_def using Greatest_le_nat graph_le assms by metis then show "False" by auto qed lemma rank_le: assumes "finite (nodes A)" "w \ language A" assumes "v \ gunodes A w" "u \ gusuccessors A w v" shows "rank A w u \ rank A w v" unfolding rank_def proof (rule Greatest_le_nat) have 1: "u \ gureachable A w v" using graph.reachable_successors assms(4) by blast have 2: "u \ gunodes A w" using assms(3) 1 by auto show "v \ graph A w (GREATEST k. u \ graph A w k)" unfolding rank_def[symmetric] proof (rule graph_successors) show "v \ gunodes A w" using assms(3) by this show "u \ gusuccessors A w v" using assms(4) by this show "u \ graph A w (rank A w u)" using rank_member assms(1, 2) 2 by this qed show "\ k. v \ graph A w k \ k \ 2 * card (nodes A)" using graph_le assms(1, 2) by blast qed lemma language_ranking: assumes "finite (nodes A)" "w \ language A" shows "ranking A w (rank A w)" unfolding ranking_def proof (intro conjI ballI allI impI) fix v assume 1: "v \ gunodes A w" have 2: "v \ graph A w (rank A w v)" using rank_member assms 1 by this show "rank A w v \ 2 * card (nodes A)" using graph_le assms 2 by this next fix v u assume 1: "v \ gunodes A w" "u \ gusuccessors A w v" show "rank A w u \ rank A w v" using rank_le assms 1 by this next fix v assume 1: "v \ gunodes A w" "gaccepting A v" have 2: "v \ graph A w (rank A w v)" using rank_member assms 1(1) by this have 3: "v \ graph A w (Suc (rank A w v))" using rank_removed assms by this have 4: "v \ prune A w (graph A w (rank A w v))" using 2 1(2) unfolding prune_def by auto have 5: "graph A w (Suc (rank A w v)) \ prune A w (graph A w (rank A w v))" using 3 4 by blast show "even (rank A w v)" using 5 by auto next fix v r k assume 1: "v \ gunodes A w" "gurun A w r v" "smap (rank A w) (gtrace r v) = sconst k" have "sset (gtrace r v) \ gureachable A w v" using 1(2) by (metis graph.reachable.reflexive graph.reachable_trace) then have 6: "sset (gtrace r v) \ gunodes A w" using 1(1) by blast have 60: "rank A w ` sset (gtrace r v) \ {k}" using 1(3) by (metis equalityD1 sset_sconst stream.set_map) have 50: "sset (gtrace r v) \ graph A w k" using rank_member[OF assms] subsetD[OF 6] 60 unfolding image_subset_iff by auto have 70: "grun A w (graph A w k) r v" using grun_subset 1(2) 50 by this have 7: "sset (gtrace r v) \ clean A w (graph A w k)" unfolding clean_def using 50 infinite_greachable_gtrace[OF 70] by auto have 8: "sset (gtrace r v) \ graph A w (Suc k) = {}" using rank_removed[OF assms] 60 by blast have 9: "sset (gtrace r v) \ {}" using stream.set_sel(1) by auto have 10: "graph A w (Suc k) \ clean A w (graph A w k)" using 7 8 9 by blast show "odd k" using 10 unfolding graph_Suc by auto qed subsection \Correctness Theorem\ theorem language_ranking_iff: assumes "finite (nodes A)" shows "w \ language A \ (\ f. ranking A w f)" using ranking_language language_ranking assms by blast end diff --git a/thys/Transition_Systems_and_Automata/Automata/DBA/DBA_Combine.thy b/thys/Transition_Systems_and_Automata/Automata/DBA/DBA_Combine.thy --- a/thys/Transition_Systems_and_Automata/Automata/DBA/DBA_Combine.thy +++ b/thys/Transition_Systems_and_Automata/Automata/DBA/DBA_Combine.thy @@ -1,302 +1,303 @@ section \Deterministic Büchi Automata Combinations\ theory DBA_Combine imports "DBA" "DGBA" begin definition dbgail :: "('label, 'state) dba list \ ('label, 'state list) dgba" where "dbgail AA \ dgba (INTER (set AA) dba.alphabet) (map dba.initial AA) (\ a pp. map2 (\ A p. dba.succ A a p) AA pp) (map (\ k pp. dba.accepting (AA ! k) (pp ! k)) [0 ..< length AA])" lemma dbgail_trace_smap: assumes "length pp = length AA" "k < length AA" shows "smap (\ pp. pp ! k) (dgba.trace (dbgail AA) w pp) = dba.trace (AA ! k) w (pp ! k)" using assms unfolding dbgail_def by (coinduction arbitrary: w pp) (force) lemma dbgail_nodes_length: assumes "pp \ DGBA.nodes (dbgail AA)" shows "length pp = length AA" using assms unfolding dbgail_def by induct auto lemma dbgail_nodes[intro]: assumes "pp \ DGBA.nodes (dbgail AA)" "k < length pp" shows "pp ! k \ DBA.nodes (AA ! k)" using assms unfolding dbgail_def by induct auto lemma dbgail_nodes_finite[intro]: assumes "list_all (finite \ DBA.nodes) AA" shows "finite (DGBA.nodes (dbgail AA))" proof (rule finite_subset) show "DGBA.nodes (dbgail AA) \ listset (map DBA.nodes AA)" by (force simp: listset_member list_all2_conv_all_nth dbgail_nodes_length) have "finite (listset (map DBA.nodes AA)) \ list_all finite (map DBA.nodes AA)" by (rule listset_finite) (auto simp: list_all_iff) then show "finite (listset (map DBA.nodes AA))" using assms by (simp add: list.pred_map) qed lemma dbgail_nodes_card: assumes "list_all (finite \ DBA.nodes) AA" shows "card (DGBA.nodes (dbgail AA)) \ prod_list (map (card \ DBA.nodes) AA)" proof - have "card (DGBA.nodes (dbgail AA)) \ card (listset (map DBA.nodes AA))" proof (rule card_mono) have "finite (listset (map DBA.nodes AA)) \ list_all finite (map DBA.nodes AA)" by (rule listset_finite) (auto simp: list_all_iff) then show "finite (listset (map DBA.nodes AA))" using assms by (simp add: list.pred_map) show "DGBA.nodes (dbgail AA) \ listset (map DBA.nodes AA)" by (force simp: listset_member list_all2_conv_all_nth dbgail_nodes_length) qed also have "\ = prod_list (map (card \ DBA.nodes) AA)" by simp finally show ?thesis by this qed lemma dbgail_language[simp]: "DGBA.language (dbgail AA) = INTER (set AA) DBA.language" proof safe fix w A assume 1: "w \ DGBA.language (dbgail AA)" "A \ set AA" obtain 2: "dgba.run (dbgail AA) w (dgba.initial (dbgail AA))" "gen infs (dgba.accepting (dbgail AA)) (dgba.trace (dbgail AA) w (dgba.initial (dbgail AA)))" using 1(1) by rule obtain k where 3: "A = AA ! k" "k < length AA" using 1(2) unfolding in_set_conv_nth by auto have 4: "(\ pp. dba.accepting A (pp ! k)) \ set (dgba.accepting (dbgail AA))" using 3 unfolding dbgail_def by auto show "w \ DBA.language A" proof show "dba.run A w (dba.initial A)" using 1(2) 2(1) unfolding DBA.run_alt_def DGBA.run_alt_def dbgail_def by auto have "True \ infs (\ pp. dba.accepting A (pp ! k)) (dgba.trace (dbgail AA) w (map dba.initial AA))" using 2(2) 4 unfolding dbgail_def by auto also have "\ \ infs (dba.accepting A) (smap (\ pp. pp ! k) (dgba.trace (dbgail AA) w (map dba.initial AA)))" by (simp add: comp_def) also have "smap (\ pp. pp ! k) (dgba.trace (dbgail AA) w (map dba.initial AA)) = dba.trace (AA ! k) w (map dba.initial AA ! k)" using 3(2) by (fastforce intro: dbgail_trace_smap) also have "\ = dba.trace A w (dba.initial A)" using 3 by auto finally show "infs (dba.accepting A) (dba.trace A w (dba.initial A))" by simp qed next fix w assume 1: "w \ INTER (set AA) DBA.language" have 2: "dba.run A w (dba.initial A)" "infs (dba.accepting A) (dba.trace A w (dba.initial A))" if "A \ set AA" for A using 1 that by auto show "w \ DGBA.language (dbgail AA)" proof (intro DGBA.language ballI gen) show "dgba.run (dbgail AA) w (dgba.initial (dbgail AA))" using 2(1) unfolding DBA.run_alt_def DGBA.run_alt_def dbgail_def by auto next fix P assume 3: "P \ set (dgba.accepting (dbgail AA))" obtain k where 4: "P = (\ pp. dba.accepting (AA ! k) (pp ! k))" "k < length AA" using 3 unfolding dbgail_def by auto have "True \ infs (dba.accepting (AA ! k)) (dba.trace (AA ! k) w (map dba.initial AA ! k))" using 2(2) 4(2) by auto also have "dba.trace (AA ! k) w (map dba.initial AA ! k) = smap (\ pp. pp ! k) (dgba.trace (dbgail AA) w (map dba.initial AA))" using 4(2) by (fastforce intro: dbgail_trace_smap[symmetric]) also have "infs (dba.accepting (AA ! k)) \ \ infs P (dgba.trace (dbgail AA) w (map dba.initial AA))" unfolding 4(1) by (simp add: comp_def) also have "map dba.initial AA = dgba.initial (dbgail AA)" unfolding dbgail_def by simp finally show "infs P (dgba.trace (dbgail AA) w (dgba.initial (dbgail AA)))" by simp qed qed definition dbail :: "('label, 'state) dba list \ ('label, 'state list degen) dba" where "dbail = degen \ dbgail" lemma dbail_nodes_finite[intro]: assumes "list_all (finite \ DBA.nodes) AA" shows "finite (DBA.nodes (dbail AA))" using dbgail_nodes_finite assms unfolding dbail_def by auto lemma dbail_nodes_card: assumes"list_all (finite \ DBA.nodes) AA" shows "card (DBA.nodes (dbail AA)) \ max 1 (length AA) * prod_list (map (card \ DBA.nodes) AA)" proof - have "card (DBA.nodes (dbail AA)) \ max 1 (length (dgba.accepting (dbgail AA))) * card (DGBA.nodes (dbgail AA))" unfolding dbail_def using degen_nodes_card by simp also have "length (dgba.accepting (dbgail AA)) = length AA" unfolding dbgail_def by simp also have "card (DGBA.nodes (dbgail AA)) \ prod_list (map (card \ DBA.nodes) AA)" using dbgail_nodes_card assms by this finally show ?thesis by simp qed lemma dbail_language[simp]: "DBA.language (dbail AA) = INTER (set AA) DBA.language" unfolding dbail_def using degen_language dbgail_language by auto definition dbau :: "('label, 'state\<^sub>1) dba \ ('label, 'state\<^sub>2) dba \ ('label, 'state\<^sub>1 \ 'state\<^sub>2) dba" where "dbau A B \ dba (dba.alphabet A \ dba.alphabet B) (dba.initial A, dba.initial B) (\ a (p, q). (dba.succ A a p, dba.succ B a q)) (\ (p, q). dba.accepting A p \ dba.accepting B q)" + (* TODO: can these be extracted as more general theorems about sscan? *) lemma dbau_fst[iff]: "infs (P \ fst) (dba.trace (dbau A B) w (p, q)) \ infs P (dba.trace A w p)" proof - let ?t = "dba.trace (dbau A B) w (p, q)" - have "infs (P \ fst) ?t \ infs P (smap fst ?t)" by simp + have "infs (P \ fst) ?t \ infs P (smap fst ?t)" by (simp add: comp_def) also have "smap fst ?t = dba.trace A w p" unfolding dbau_def by (coinduction arbitrary: w p q) (auto) finally show ?thesis by this qed lemma dbau_snd[iff]: "infs (P \ snd) (dba.trace (dbau A B) w (p, q)) \ infs P (dba.trace B w q)" proof - let ?t = "dba.trace (dbau A B) w (p, q)" - have "infs (P \ snd) ?t \ infs P (smap snd ?t)" by simp + have "infs (P \ snd) ?t \ infs P (smap snd ?t)" by (simp add: comp_def) also have "smap snd ?t = dba.trace B w q" unfolding dbau_def by (coinduction arbitrary: w p q) (auto) finally show ?thesis by this qed lemma dbau_nodes_fst[intro]: assumes "dba.alphabet A = dba.alphabet B" shows "fst ` DBA.nodes (dbau A B) \ DBA.nodes A" proof (rule subsetI, erule imageE) fix pq p assume "pq \ DBA.nodes (dbau A B)" "p = fst pq" then show "p \ DBA.nodes A" using assms unfolding dbau_def by (induct arbitrary: p) (auto) qed lemma dbau_nodes_snd[intro]: assumes "dba.alphabet A = dba.alphabet B" shows "snd ` DBA.nodes (dbau A B) \ DBA.nodes B" proof (rule subsetI, erule imageE) fix pq q assume "pq \ DBA.nodes (dbau A B)" "q = snd pq" then show "q \ DBA.nodes B" using assms unfolding dbau_def by (induct arbitrary: q) (auto) qed lemma dbau_nodes_finite[intro]: assumes "dba.alphabet A = dba.alphabet B" assumes "finite (DBA.nodes A)" "finite (DBA.nodes B)" shows "finite (DBA.nodes (dbau A B))" proof (rule finite_subset) show "DBA.nodes (dbau A B) \ DBA.nodes A \ DBA.nodes B" using dbau_nodes_fst[OF assms(1)] dbau_nodes_snd[OF assms(1)] unfolding image_subset_iff by force show "finite (DBA.nodes A \ DBA.nodes B)" using assms(2, 3) by simp qed lemma dbau_nodes_card[intro]: assumes "dba.alphabet A = dba.alphabet B" assumes "finite (DBA.nodes A)" "finite (DBA.nodes B)" shows "card (DBA.nodes (dbau A B)) \ card (DBA.nodes A) * card (DBA.nodes B)" proof - have "card (DBA.nodes (dbau A B)) \ card (DBA.nodes A \ DBA.nodes B)" proof (rule card_mono) show "finite (DBA.nodes A \ DBA.nodes B)" using assms(2, 3) by simp show "DBA.nodes (dbau A B) \ DBA.nodes A \ DBA.nodes B" using dbau_nodes_fst[OF assms(1)] dbau_nodes_snd[OF assms(1)] unfolding image_subset_iff by force qed also have "\ = card (DBA.nodes A) * card (DBA.nodes B)" using card_cartesian_product by this finally show ?thesis by this qed lemma dbau_language[simp]: assumes "dba.alphabet A = dba.alphabet B" shows "DBA.language (dbau A B) = DBA.language A \ DBA.language B" proof - have 1: "dba.alphabet (dbau A B) = dba.alphabet A \ dba.alphabet B" unfolding dbau_def by simp have 2: "dba.initial (dbau A B) = (dba.initial A, dba.initial B)" unfolding dbau_def by simp have 3: "dba.accepting (dbau A B) = (\ pq. (dba.accepting A \ fst) pq \ (dba.accepting B \ snd) pq)" unfolding dbau_def by auto have 4: "infs (dba.accepting (dbau A B)) (DBA.trace (dbau A B) w (p, q)) \ infs (dba.accepting A) (DBA.trace A w p) \ infs (dba.accepting B) (DBA.trace B w q)" for w p q unfolding 3 by blast show ?thesis using assms unfolding DBA.language_def DBA.run_alt_def 1 2 4 by auto qed definition dbaul :: "('label, 'state) dba list \ ('label, 'state list) dba" where "dbaul AA \ dba (UNION (set AA) dba.alphabet) (map dba.initial AA) (\ a pp. map2 (\ A p. dba.succ A a p) AA pp) (\ pp. \ k < length AA. dba.accepting (AA ! k) (pp ! k))" lemma dbaul_trace_smap: assumes "length pp = length AA" "k < length AA" shows "smap (\ pp. pp ! k) (dba.trace (dbaul AA) w pp) = dba.trace (AA ! k) w (pp ! k)" using assms unfolding dbaul_def by (coinduction arbitrary: w pp) (force) lemma dbaul_nodes_length: assumes "pp \ DBA.nodes (dbaul AA)" shows "length pp = length AA" using assms unfolding dbaul_def by induct auto lemma dbaul_nodes[intro]: assumes "INTER (set AA) dba.alphabet = UNION (set AA) dba.alphabet" assumes "pp \ DBA.nodes (dbaul AA)" "k < length pp" shows "pp ! k \ DBA.nodes (AA ! k)" using assms(2, 3, 1) unfolding dbaul_def by induct force+ lemma dbaul_nodes_finite[intro]: assumes "INTER (set AA) dba.alphabet = UNION (set AA) dba.alphabet" assumes "list_all (finite \ DBA.nodes) AA" shows "finite (DBA.nodes (dbaul AA))" proof (rule finite_subset) show "DBA.nodes (dbaul AA) \ listset (map DBA.nodes AA)" using assms(1) by (force simp: listset_member list_all2_conv_all_nth dbaul_nodes_length) have "finite (listset (map DBA.nodes AA)) \ list_all finite (map DBA.nodes AA)" by (rule listset_finite) (auto simp: list_all_iff) then show "finite (listset (map DBA.nodes AA))" using assms(2) by (simp add: list.pred_map) qed lemma dbaul_nodes_card: assumes "INTER (set AA) dba.alphabet = UNION (set AA) dba.alphabet" assumes "list_all (finite \ DBA.nodes) AA" shows "card (DBA.nodes (dbaul AA)) \ prod_list (map (card \ DBA.nodes) AA)" proof - have "card (DBA.nodes (dbaul AA)) \ card (listset (map DBA.nodes AA))" proof (rule card_mono) have "finite (listset (map DBA.nodes AA)) \ list_all finite (map DBA.nodes AA)" by (rule listset_finite) (auto simp: list_all_iff) then show "finite (listset (map DBA.nodes AA))" using assms(2) by (simp add: list.pred_map) show "DBA.nodes (dbaul AA) \ listset (map DBA.nodes AA)" using assms(1) by (force simp: listset_member list_all2_conv_all_nth dbaul_nodes_length) qed also have "\ = prod_list (map (card \ DBA.nodes) AA)" by simp finally show ?thesis by this qed lemma dbaul_language[simp]: assumes "INTER (set AA) dba.alphabet = UNION (set AA) dba.alphabet" shows "DBA.language (dbaul AA) = UNION (set AA) DBA.language" proof safe fix w assume 1: "w \ DBA.language (dbaul AA)" obtain 2: "dba.run (dbaul AA) w (dba.initial (dbaul AA))" "infs (dba.accepting (dbaul AA)) (dba.trace (dbaul AA) w (dba.initial (dbaul AA)))" using 1 by rule obtain k where 3: "k < length AA" "infs (\ pp. dba.accepting (AA ! k) (pp ! k)) (dba.trace (dbaul AA) w (map dba.initial AA))" using 2(2) unfolding dbaul_def by auto show "w \ UNION (set AA) DBA.language" proof (intro UN_I DBA.language) show "AA ! k \ set AA" using 3(1) by simp show "dba.run (AA ! k) w (dba.initial (AA ! k))" using assms 2(1) 3(1) unfolding DBA.run_alt_def DGBA.run_alt_def dbaul_def by force have "True \ infs (\ pp. dba.accepting (AA ! k) (pp ! k)) (dba.trace (dbaul AA) w (map dba.initial AA))" using 3(2) by auto also have "\ \ infs (dba.accepting (AA ! k)) (smap (\ pp. pp ! k) (dba.trace (dbaul AA) w (map dba.initial AA)))" by (simp add: comp_def) also have "smap (\ pp. pp ! k) (dba.trace (dbaul AA) w (map dba.initial AA)) = dba.trace (AA ! k) w (map dba.initial AA ! k)" using 3(1) by (fastforce intro: dbaul_trace_smap) also have "\ = dba.trace (AA ! k) w (dba.initial (AA ! k))" using 3 by auto finally show "infs (dba.accepting (AA ! k)) (dba.trace (AA ! k) w (dba.initial (AA ! k)))" by simp qed next fix A w assume 1: "A \ set AA" "w \ DBA.language A" obtain 2: "dba.run A w (dba.initial A)" "infs (dba.accepting A) (dba.trace A w (dba.initial A))" using 1(2) by rule obtain k where 3: "A = AA ! k" "k < length AA" using 1(1) unfolding in_set_conv_nth by auto show "w \ DBA.language (dbaul AA)" proof show "dba.run (dbaul AA) w (dba.initial (dbaul AA))" using 1(1) 2(1) unfolding DBA.run_alt_def DGBA.run_alt_def dbaul_def by auto have "True \ infs (dba.accepting (AA ! k)) (dba.trace (AA ! k) w (map dba.initial AA ! k))" using 2(2) 3 by auto also have "dba.trace (AA ! k) w (map dba.initial AA ! k) = smap (\ pp. pp ! k) (dba.trace (dbaul AA) w (map dba.initial AA))" using 3(2) by (fastforce intro: dbaul_trace_smap[symmetric]) also have "infs (dba.accepting (AA ! k)) \ \ infs (\ pp. dba.accepting (AA ! k) (pp ! k)) (dba.trace (dbaul AA) w (map dba.initial AA))" by (simp add: comp_def) finally show "infs (dba.accepting (dbaul AA)) (dba.trace (dbaul AA) w (dba.initial (dbaul AA)))" using 3(2) unfolding dbaul_def by auto qed qed end \ No newline at end of file diff --git a/thys/Transition_Systems_and_Automata/Automata/DCA/DCA_Combine.thy b/thys/Transition_Systems_and_Automata/Automata/DCA/DCA_Combine.thy --- a/thys/Transition_Systems_and_Automata/Automata/DCA/DCA_Combine.thy +++ b/thys/Transition_Systems_and_Automata/Automata/DCA/DCA_Combine.thy @@ -1,298 +1,298 @@ section \Deterministic Co-Büchi Automata Combinations\ theory DCA_Combine imports "DCA" "DGCA" begin definition dcai :: "('label, 'state\<^sub>1) dca \ ('label, 'state\<^sub>2) dca \ ('label, 'state\<^sub>1 \ 'state\<^sub>2) dca" where "dcai A B \ dca (dca.alphabet A \ dca.alphabet B) (dca.initial A, dca.initial B) (\ a (p, q). (dca.succ A a p, dca.succ B a q)) (\ (p, q). dca.rejecting A p \ dca.rejecting B q)" lemma dcai_fst[iff]: "infs (P \ fst) (dca.trace (dcai A B) w (p, q)) \ infs P (dca.trace A w p)" proof - let ?t = "dca.trace (dcai A B) w (p, q)" - have "infs (P \ fst) ?t \ infs P (smap fst ?t)" by simp + have "infs (P \ fst) ?t \ infs P (smap fst ?t)" by (simp add: comp_def) also have "smap fst ?t = dca.trace A w p" unfolding dcai_def by (coinduction arbitrary: w p q) (auto) finally show ?thesis by this qed lemma dcai_snd[iff]: "infs (P \ snd) (dca.trace (dcai A B) w (p, q)) \ infs P (dca.trace B w q)" proof - let ?t = "dca.trace (dcai A B) w (p, q)" - have "infs (P \ snd) ?t \ infs P (smap snd ?t)" by simp + have "infs (P \ snd) ?t \ infs P (smap snd ?t)" by (simp add: comp_def) also have "smap snd ?t = dca.trace B w q" unfolding dcai_def by (coinduction arbitrary: w p q) (auto) finally show ?thesis by this qed lemma dcai_nodes_fst[intro]: "fst ` DCA.nodes (dcai A B) \ DCA.nodes A" proof (rule subsetI, erule imageE) fix pq p assume "pq \ DCA.nodes (dcai A B)" "p = fst pq" then show "p \ DCA.nodes A" unfolding dcai_def by (induct arbitrary: p) (auto) qed lemma dcai_nodes_snd[intro]: "snd ` DCA.nodes (dcai A B) \ DCA.nodes B" proof (rule subsetI, erule imageE) fix pq q assume "pq \ DCA.nodes (dcai A B)" "q = snd pq" then show "q \ DCA.nodes B" unfolding dcai_def by (induct arbitrary: q) (auto) qed lemma dcai_nodes_finite[intro]: assumes "finite (DCA.nodes A)" "finite (DCA.nodes B)" shows "finite (DCA.nodes (dcai A B))" proof (rule finite_subset) show "DCA.nodes (dcai A B) \ DCA.nodes A \ DCA.nodes B" using dcai_nodes_fst dcai_nodes_snd unfolding image_subset_iff by force show "finite (DCA.nodes A \ DCA.nodes B)" using assms by simp qed lemma dcai_nodes_card[intro]: assumes "finite (DCA.nodes A)" "finite (DCA.nodes B)" shows "card (DCA.nodes (dcai A B)) \ card (DCA.nodes A) * card (DCA.nodes B)" proof - have "card (DCA.nodes (dcai A B)) \ card (DCA.nodes A \ DCA.nodes B)" proof (rule card_mono) show "finite (DCA.nodes A \ DCA.nodes B)" using assms by simp show "DCA.nodes (dcai A B) \ DCA.nodes A \ DCA.nodes B" using dcai_nodes_fst dcai_nodes_snd unfolding image_subset_iff by force qed also have "\ = card (DCA.nodes A) * card (DCA.nodes B)" using card_cartesian_product by this finally show ?thesis by this qed lemma dcai_language[simp]: "DCA.language (dcai A B) = DCA.language A \ DCA.language B" proof - have 1: "dca.alphabet (dcai A B) = dca.alphabet A \ dca.alphabet B" unfolding dcai_def by simp have 2: "dca.initial (dcai A B) = (dca.initial A, dca.initial B)" unfolding dcai_def by simp have 3: "dca.rejecting (dcai A B) = (\ pq. (dca.rejecting A \ fst) pq \ (dca.rejecting B \ snd) pq)" unfolding dcai_def by auto have 4: "infs (dca.rejecting (dcai A B)) (DCA.trace (dcai A B) w (p, q)) \ infs (dca.rejecting A) (DCA.trace A w p) \ infs (dca.rejecting B) (DCA.trace B w q)" for w p q unfolding 3 by blast show ?thesis unfolding DCA.language_def DCA.run_alt_def 1 2 4 by auto qed definition dcail :: "('label, 'state) dca list \ ('label, 'state list) dca" where "dcail AA \ dca (INTER (set AA) dca.alphabet) (map dca.initial AA) (\ a pp. map2 (\ A p. dca.succ A a p) AA pp) (\ pp. \ k < length AA. dca.rejecting (AA ! k) (pp ! k))" lemma dcail_trace_smap: assumes "length pp = length AA" "k < length AA" shows "smap (\ pp. pp ! k) (dca.trace (dcail AA) w pp) = dca.trace (AA ! k) w (pp ! k)" using assms unfolding dcail_def by (coinduction arbitrary: w pp) (force) lemma dcail_nodes_length: assumes "pp \ DCA.nodes (dcail AA)" shows "length pp = length AA" using assms unfolding dcail_def by induct auto lemma dcail_nodes[intro]: assumes "pp \ DCA.nodes (dcail AA)" "k < length pp" shows "pp ! k \ DCA.nodes (AA ! k)" using assms unfolding dcail_def by induct auto lemma dcail_finite[intro]: assumes "list_all (finite \ DCA.nodes) AA" shows "finite (DCA.nodes (dcail AA))" proof (rule finite_subset) show "DCA.nodes (dcail AA) \ listset (map DCA.nodes AA)" by (force simp: listset_member list_all2_conv_all_nth dcail_nodes_length) have "finite (listset (map DCA.nodes AA)) \ list_all finite (map DCA.nodes AA)" by (rule listset_finite) (auto simp: list_all_iff) then show "finite (listset (map DCA.nodes AA))" using assms by (simp add: list.pred_map) qed lemma dcail_nodes_card: assumes "list_all (finite \ DCA.nodes) AA" shows "card (DCA.nodes (dcail AA)) \ prod_list (map (card \ DCA.nodes) AA)" proof - have "card (DCA.nodes (dcail AA)) \ card (listset (map DCA.nodes AA))" proof (rule card_mono) have "finite (listset (map DCA.nodes AA)) \ list_all finite (map DCA.nodes AA)" by (rule listset_finite) (auto simp: list_all_iff) then show "finite (listset (map DCA.nodes AA))" using assms by (simp add: list.pred_map) show "DCA.nodes (dcail AA) \ listset (map DCA.nodes AA)" by (force simp: listset_member list_all2_conv_all_nth dcail_nodes_length) qed also have "\ = prod_list (map (card \ DCA.nodes) AA)" by simp finally show ?thesis by this qed lemma dcail_language[simp]: "DCA.language (dcail AA) = INTER (set AA) DCA.language" proof safe fix A w assume 1: "w \ DCA.language (dcail AA)" "A \ set AA" obtain 2: "dca.run (dcail AA) w (dca.initial (dcail AA))" "\ infs (dca.rejecting (dcail AA)) (dca.trace (dcail AA) w (dca.initial (dcail AA)))" using 1(1) by rule obtain k where 3: "A = AA ! k" "k < length AA" using 1(2) unfolding in_set_conv_nth by auto have 4: "\ infs (\ pp. dca.rejecting A (pp ! k)) (dca.trace (dcail AA) w (map dca.initial AA))" using 2(2) 3 unfolding dcail_def by auto show "w \ DCA.language A" proof show "dca.run A w (dca.initial A)" using 1(2) 2(1) unfolding DCA.run_alt_def dcail_def by auto have "True \ \ infs (\ pp. dca.rejecting A (pp ! k)) (dca.trace (dcail AA) w (map dca.initial AA))" using 4 by simp also have "\ \ \ infs (dca.rejecting A) (smap (\ pp. pp ! k) (dca.trace (dcail AA) w (map dca.initial AA)))" by (simp add: comp_def) also have "smap (\ pp. pp ! k) (dca.trace (dcail AA) w (map dca.initial AA)) = dca.trace (AA ! k) w (map dca.initial AA ! k)" using 3(2) by (fastforce intro: dcail_trace_smap) also have "\ = dca.trace A w (dca.initial A)" using 3 by auto finally show "\ infs (dca.rejecting A) (DCA.trace A w (dca.initial A))" by simp qed next fix w assume 1: "w \ INTER (set AA) DCA.language" have 2: "dca.run A w (dca.initial A)" "\ infs (dca.rejecting A) (dca.trace A w (dca.initial A))" if "A \ set AA" for A using 1 that by auto have 3: "\ infs (\ pp. dca.rejecting (AA ! k) (pp ! k)) (dca.trace (dcail AA) w (map dca.initial AA))" if "k < length AA" for k proof - have "True \ \ infs (dca.rejecting (AA ! k)) (dca.trace (AA ! k) w (map dca.initial AA ! k))" using 2(2) that by auto also have "dca.trace (AA ! k) w (map dca.initial AA ! k) = smap (\ pp. pp ! k) (dca.trace (dcail AA) w (map dca.initial AA))" using that by (fastforce intro: dcail_trace_smap[symmetric]) also have "infs (dca.rejecting (AA ! k)) \ \ infs (\ pp. dca.rejecting (AA ! k) (pp ! k)) (dca.trace (dcail AA) w (map dca.initial AA))" by (simp add: comp_def) finally show ?thesis by simp qed show "w \ DCA.language (dcail AA)" proof show "dca.run (dcail AA) w (dca.initial (dcail AA))" using 2(1) unfolding DCA.run_alt_def dcail_def by auto show "\ infs (dca.rejecting (dcail AA)) (dca.trace (dcail AA) w (dca.initial (dcail AA)))" using 3 unfolding dcail_def by auto qed qed definition dcgaul :: "('label, 'state) dca list \ ('label, 'state list) dgca" where "dcgaul AA \ dgca (UNION (set AA) dca.alphabet) (map dca.initial AA) (\ a pp. map2 (\ A p. dca.succ A a p) AA pp) (map (\ k pp. dca.rejecting (AA ! k) (pp ! k)) [0 ..< length AA])" lemma dcgaul_trace_smap: assumes "length pp = length AA" "k < length AA" shows "smap (\ pp. pp ! k) (dgca.trace (dcgaul AA) w pp) = dca.trace (AA ! k) w (pp ! k)" using assms unfolding dcgaul_def by (coinduction arbitrary: w pp) (force) lemma dcgaul_nodes_length: assumes "pp \ DGCA.nodes (dcgaul AA)" shows "length pp = length AA" using assms unfolding dcgaul_def by induct auto lemma dcgaul_nodes[intro]: assumes "INTER (set AA) dca.alphabet = UNION (set AA) dca.alphabet" assumes "pp \ DGCA.nodes (dcgaul AA)" "k < length pp" shows "pp ! k \ DCA.nodes (AA ! k)" using assms(2, 3, 1) unfolding dcgaul_def by induct force+ lemma dcgaul_nodes_finite[intro]: assumes "INTER (set AA) dca.alphabet = UNION (set AA) dca.alphabet" assumes "list_all (finite \ DCA.nodes) AA" shows "finite (DGCA.nodes (dcgaul AA))" proof (rule finite_subset) show "DGCA.nodes (dcgaul AA) \ listset (map DCA.nodes AA)" using assms(1) by (force simp: listset_member list_all2_conv_all_nth dcgaul_nodes_length) have "finite (listset (map DCA.nodes AA)) \ list_all finite (map DCA.nodes AA)" by (rule listset_finite) (auto simp: list_all_iff) then show "finite (listset (map DCA.nodes AA))" using assms(2) by (simp add: list.pred_map) qed lemma dcgaul_nodes_card: assumes "INTER (set AA) dca.alphabet = UNION (set AA) dca.alphabet" assumes "list_all (finite \ DCA.nodes) AA" shows "card (DGCA.nodes (dcgaul AA)) \ prod_list (map (card \ DCA.nodes) AA)" proof - have "card (DGCA.nodes (dcgaul AA)) \ card (listset (map DCA.nodes AA))" proof (rule card_mono) have "finite (listset (map DCA.nodes AA)) \ list_all finite (map DCA.nodes AA)" by (rule listset_finite) (auto simp: list_all_iff) then show "finite (listset (map DCA.nodes AA))" using assms(2) by (simp add: list.pred_map) show "DGCA.nodes (dcgaul AA) \ listset (map DCA.nodes AA)" using assms(1) by (force simp: listset_member list_all2_conv_all_nth dcgaul_nodes_length) qed also have "\ = prod_list (map (card \ DCA.nodes) AA)" by simp finally show ?thesis by this qed lemma dcgaul_language[simp]: assumes "INTER (set AA) dca.alphabet = UNION (set AA) dca.alphabet" shows "DGCA.language (dcgaul AA) = UNION (set AA) DCA.language" proof safe fix w assume 1: "w \ DGCA.language (dcgaul AA)" obtain k where 2: "dgca.run (dcgaul AA) w (dgca.initial (dcgaul AA))" "k < length AA" "\ infs (\ pp. dca.rejecting (AA ! k) (pp ! k)) (dgca.trace (dcgaul AA) w (dgca.initial (dcgaul AA)))" using 1 unfolding dcgaul_def by force show "w \ UNION (set AA) DCA.language" proof (intro UN_I DCA.language) show "AA ! k \ set AA" using 2(2) by simp show "dca.run (AA ! k) w (dca.initial (AA ! k))" using assms 2(1, 2) unfolding DCA.run_alt_def DGCA.run_alt_def dcgaul_def by force have "True \ \ infs (\ pp. dca.rejecting (AA ! k) (pp ! k)) (dgca.trace (dcgaul AA) w (map dca.initial AA))" using 2(3) unfolding dcgaul_def by auto also have "\ \ \ infs (dca.rejecting (AA ! k)) (smap (\ pp. pp ! k) (dgca.trace (dcgaul AA) w (map dca.initial AA)))" by (simp add: comp_def) also have "smap (\ pp. pp ! k) (dgca.trace (dcgaul AA) w (map dca.initial AA)) = dca.trace (AA ! k) w (map dca.initial AA ! k)" using 2(2) by (fastforce intro: dcgaul_trace_smap) also have "\ = dca.trace (AA ! k) w (dca.initial (AA ! k))" using 2(2) by auto finally show "\ infs (dca.rejecting (AA ! k)) (dca.trace (AA ! k) w (dca.initial (AA ! k)))" by simp qed next fix A w assume 1: "A \ set AA" "w \ DCA.language A" obtain 2: "dca.run A w (dca.initial A)" "\ infs (dca.rejecting A) (dca.trace A w (dca.initial A))" using 1(2) by rule obtain k where 3: "A = AA ! k" "k < length AA" using 1(1) unfolding in_set_conv_nth by auto show "w \ DGCA.language (dcgaul AA)" proof (intro DGCA.language bexI cogen) show "dgca.run (dcgaul AA) w (dgca.initial (dcgaul AA))" using 1(1) 2(1) unfolding DCA.run_alt_def DGCA.run_alt_def dcgaul_def by auto have "True \ \ infs (dca.rejecting (AA ! k)) (dca.trace (AA ! k) w (map dca.initial AA ! k))" using 2(2) 3 by auto also have "dca.trace (AA ! k) w (map dca.initial AA ! k) = smap (\ pp. pp ! k) (dgca.trace (dcgaul AA) w (map dca.initial AA))" using 3(2) by (fastforce intro: dcgaul_trace_smap[symmetric]) also have "\ infs (dca.rejecting (AA ! k)) \ \ \ infs (\ pp. dca.rejecting (AA ! k) (pp ! k)) (dgca.trace (dcgaul AA) w (map dca.initial AA))" by (simp add: comp_def) also have "map dca.initial AA = dgca.initial (dcgaul AA)" unfolding dcgaul_def by simp finally show "\ infs (\ pp. dca.rejecting (AA ! k) (pp ! k)) (dgca.trace (dcgaul AA) w (dgca.initial (dcgaul AA)))" by simp show "(\ pp. dca.rejecting (AA ! k) (pp ! k)) \ set (dgca.rejecting (dcgaul AA))" unfolding dcgaul_def using 3(2) by simp qed qed definition dcaul :: "('label, 'state) dca list \ ('label, 'state list degen) dca" where "dcaul = degen \ dcgaul" lemma dcaul_nodes_finite[intro]: assumes "INTER (set AA) dca.alphabet = UNION (set AA) dca.alphabet" assumes "list_all (finite \ DCA.nodes) AA" shows "finite (DCA.nodes (dcaul AA))" using dcgaul_nodes_finite assms unfolding dcaul_def by auto lemma dcaul_nodes_card: assumes "INTER (set AA) dca.alphabet = UNION (set AA) dca.alphabet" assumes "list_all (finite \ DCA.nodes) AA" shows "card (DCA.nodes (dcaul AA)) \ max 1 (length AA) * prod_list (map (card \ DCA.nodes) AA)" proof - have "card (DCA.nodes (dcaul AA)) \ max 1 (length (dgca.rejecting (dcgaul AA))) * card (DGCA.nodes (dcgaul AA))" unfolding dcaul_def using degen_nodes_card by simp also have "length (dgca.rejecting (dcgaul AA)) = length AA" unfolding dcgaul_def by simp also have "card (DGCA.nodes (dcgaul AA)) \ prod_list (map (card \ DCA.nodes) AA)" using dcgaul_nodes_card assms by this finally show ?thesis by simp qed lemma dcaul_language[simp]: assumes "INTER (set AA) dca.alphabet = UNION (set AA) dca.alphabet" shows "DCA.language (dcaul AA) = UNION (set AA) DCA.language" unfolding dcaul_def using degen_language dcgaul_language[OF assms] by auto end \ No newline at end of file diff --git a/thys/Transition_Systems_and_Automata/Automata/DRA/DRA_Combine.thy b/thys/Transition_Systems_and_Automata/Automata/DRA/DRA_Combine.thy --- a/thys/Transition_Systems_and_Automata/Automata/DRA/DRA_Combine.thy +++ b/thys/Transition_Systems_and_Automata/Automata/DRA/DRA_Combine.thy @@ -1,223 +1,223 @@ section \Deterministic Rabin Automata Combinations\ theory DRA_Combine imports "DRA" "../DBA/DBA" "../DCA/DCA" begin definition from_dba :: "('label, 'state) dba \ ('label, 'state) dra" where "from_dba A \ dra (dba.alphabet A) (dba.initial A) (dba.succ A) [(dba.accepting A, bot)]" lemma from_dba_language[simp]: "DRA.language (from_dba A) = DBA.language A" unfolding DBA.language_def DRA.language_def from_dba_def DBA.run_def DRA.run_def by (auto 0 3) definition from_dca :: "('label, 'state) dca \ ('label, 'state) dra" where "from_dca A \ dra (dca.alphabet A) (dca.initial A) (dca.succ A) [(top, dca.rejecting A)]" lemma from_dca_language[simp]: "DRA.language (from_dca A) = DCA.language A" unfolding DCA.language_def DRA.language_def from_dca_def DCA.run_def DRA.run_def by (auto 0 3) definition dbcrai :: "('label, 'state\<^sub>1) dba \ ('label, 'state\<^sub>2) dca \ ('label, 'state\<^sub>1 \ 'state\<^sub>2) dra" where "dbcrai A B \ dra (dba.alphabet A \ dca.alphabet B) (dba.initial A, dca.initial B) (\ a (p, q). (dba.succ A a p, dca.succ B a q)) [(dba.accepting A \ fst, dca.rejecting B \ snd)]" lemma dbcrai_fst[iff]: "infs (P \ fst) (dra.trace (dbcrai A B) w (p, q)) \ infs P (dba.trace A w p)" proof - let ?t = "dra.trace (dbcrai A B) w (p, q)" - have "infs (P \ fst) ?t \ infs P (smap fst ?t)" by simp + have "infs (P \ fst) ?t \ infs P (smap fst ?t)" by (simp add: comp_def) also have "smap fst ?t = dba.trace A w p" unfolding dbcrai_def by (coinduction arbitrary: w p q) (auto) finally show ?thesis by this qed lemma dbcrai_snd[iff]: "infs (P \ snd) (dra.trace (dbcrai A B) w (p, q)) \ infs P (dca.trace B w q)" proof - let ?t = "dra.trace (dbcrai A B) w (p, q)" - have "infs (P \ snd) ?t \ infs P (smap snd ?t)" by simp + have "infs (P \ snd) ?t \ infs P (smap snd ?t)" by (simp add: comp_def) also have "smap snd ?t = dca.trace B w q" unfolding dbcrai_def by (coinduction arbitrary: w p q) (auto) finally show ?thesis by this qed lemma dbcrai_nodes_fst[intro]: "fst ` DRA.nodes (dbcrai A B) \ DBA.nodes A" proof (rule subsetI, erule imageE) fix pq p assume "pq \ DRA.nodes (dbcrai A B)" "p = fst pq" then show "p \ DBA.nodes A" unfolding dbcrai_def by (induct arbitrary: p) (auto) qed lemma dbcrai_nodes_snd[intro]: "snd ` DRA.nodes (dbcrai A B) \ DCA.nodes B" proof (rule subsetI, erule imageE) fix pq q assume "pq \ DRA.nodes (dbcrai A B)" "q = snd pq" then show "q \ DCA.nodes B" unfolding dbcrai_def by (induct arbitrary: q) (auto) qed lemma dbcrai_nodes_finite[intro]: assumes "finite (DBA.nodes A)" "finite (DCA.nodes B)" shows "finite (DRA.nodes (dbcrai A B))" proof (rule finite_subset) show "DRA.nodes (dbcrai A B) \ DBA.nodes A \ DCA.nodes B" using dbcrai_nodes_fst dbcrai_nodes_snd unfolding image_subset_iff by force show "finite (DBA.nodes A \ DCA.nodes B)" using assms by simp qed lemma dbcrai_nodes_card[intro]: assumes "finite (DBA.nodes A)" "finite (DCA.nodes B)" shows "card (DRA.nodes (dbcrai A B)) \ card (DBA.nodes A) * card (DCA.nodes B)" proof - have "card (DRA.nodes (dbcrai A B)) \ card (DBA.nodes A \ DCA.nodes B)" proof (rule card_mono) show "finite (DBA.nodes A \ DCA.nodes B)" using assms by simp show "DRA.nodes (dbcrai A B) \ DBA.nodes A \ DCA.nodes B" using dbcrai_nodes_fst dbcrai_nodes_snd unfolding image_subset_iff by force qed also have "\ = card (DBA.nodes A) * card (DCA.nodes B)" using card_cartesian_product by this finally show ?thesis by this qed lemma dbcrai_language[simp]: "DRA.language (dbcrai A B) = DBA.language A \ DCA.language B" proof - have 1: "dra.alphabet (dbcrai A B) = dba.alphabet A \ dca.alphabet B" unfolding dbcrai_def by simp have 2: "dra.initial (dbcrai A B) = (dba.initial A, dca.initial B)" unfolding dbcrai_def by simp have 3: "dra.accepting (dbcrai A B) = [(dba.accepting A \ fst, dca.rejecting B \ snd)]" unfolding dbcrai_def by simp have 4: "cogen rabin (dra.accepting (dbcrai A B)) (DRA.trace (dbcrai A B) w (p, q)) \ infs (dba.accepting A) (DBA.trace A w p) \ fins (rejecting B) (DCA.trace B w q)" for w p q unfolding cogen_def rabin_def 3 by simp show ?thesis unfolding DRA.language_def DBA.language_def DCA.language_def unfolding DRA.run_alt_def DBA.run_alt_def DCA.run_alt_def unfolding 1 2 4 by auto qed abbreviation (input) "get k pp \ pp ! k" definition draul :: "('label, 'state) dra list \ ('label, 'state list) dra" where "draul AA \ dra (UNION (set AA) dra.alphabet) (map dra.initial AA) (\ a pp. map2 (\ A p. dra.succ A a p) AA pp) (do { k \ [0 ..< length AA]; (f, g) \ dra.accepting (AA ! k); [(f \ get k, g \ get k)] })" lemma draul_get: assumes "length pp = length AA" "k < length AA" shows "infs (P \ get k) (dra.trace (draul AA) w pp) \ infs P (dra.trace (AA ! k) w (pp ! k))" proof - have "infs (P \ get k) (dra.trace (draul AA) w pp) \ - infs P (smap (get k) (dra.trace (draul AA) w pp))" by simp + infs P (smap (get k) (dra.trace (draul AA) w pp))" by (simp add: comp_def) also have "smap (get k) (dra.trace (draul AA) w pp) = dra.trace (AA ! k) w (pp ! k)" using assms unfolding draul_def by (coinduction arbitrary: w pp) (force) finally show ?thesis by this qed lemma draul_nodes_length: assumes "pp \ DRA.nodes (draul AA)" shows "length pp = length AA" using assms unfolding draul_def by induct auto lemma draul_nodes[intro]: assumes "INTER (set AA) dra.alphabet = UNION (set AA) dra.alphabet" assumes "pp \ DRA.nodes (draul AA)" "k < length pp" shows "pp ! k \ DRA.nodes (AA ! k)" using assms(2, 3, 1) unfolding draul_def by induct force+ lemma draul_nodes_finite[intro]: assumes "INTER (set AA) dra.alphabet = UNION (set AA) dra.alphabet" assumes "list_all (finite \ DRA.nodes) AA" shows "finite (DRA.nodes (draul AA))" proof (rule finite_subset) show "DRA.nodes (draul AA) \ listset (map DRA.nodes AA)" using assms(1) by (force simp: listset_member list_all2_conv_all_nth draul_nodes_length) have "finite (listset (map DRA.nodes AA)) \ list_all finite (map DRA.nodes AA)" by (rule listset_finite) (auto simp: list_all_iff) then show "finite (listset (map DRA.nodes AA))" using assms(2) by (simp add: list.pred_map) qed lemma draul_nodes_card: assumes "INTER (set AA) dra.alphabet = UNION (set AA) dra.alphabet" assumes "list_all (finite \ DRA.nodes) AA" shows "card (DRA.nodes (draul AA)) \ prod_list (map (card \ DRA.nodes) AA)" proof - have "card (DRA.nodes (draul AA)) \ card (listset (map DRA.nodes AA))" proof (rule card_mono) have "finite (listset (map DRA.nodes AA)) \ list_all finite (map DRA.nodes AA)" by (rule listset_finite) (auto simp: list_all_iff) then show "finite (listset (map DRA.nodes AA))" using assms(2) by (simp add: list.pred_map) show "DRA.nodes (draul AA) \ listset (map DRA.nodes AA)" using assms(1) by (force simp: listset_member list_all2_conv_all_nth draul_nodes_length) qed also have "\ = prod_list (map (card \ DRA.nodes) AA)" by simp finally show ?thesis by this qed lemma draul_language[simp]: assumes "INTER (set AA) dra.alphabet = UNION (set AA) dra.alphabet" shows "DRA.language (draul AA) = UNION (set AA) DRA.language" proof safe fix w assume 1: "w \ DRA.language (draul AA)" obtain 2: "dra.run (draul AA) w (dra.initial (draul AA))" "cogen rabin (dra.accepting (draul AA)) (dra.trace (draul AA) w (dra.initial (draul AA)))" using 1 by rule obtain I F where 3: "(I, F) \ set (dra.accepting (draul AA))" "infs I (dra.trace (draul AA) w (dra.initial (draul AA)))" "fins F (dra.trace (draul AA) w (dra.initial (draul AA)))" using 2(2) by blast obtain k P Q where 4: "k < length AA" "I = P \ get k" "F = Q \ get k" "(P, Q) \ set (dra.accepting (AA ! k))" using 3(1) unfolding draul_def List.bind_def by (auto simp: comp_def) show "w \ UNION (set AA) DRA.language" proof (intro UN_I DRA.language cogen rabin) show "AA ! k \ set AA" using 4(1) by auto show "DRA.run (AA ! k) w (dra.initial (AA ! k))" using assms 2(1) 4(1) unfolding DRA.run_alt_def draul_def by force show "(P, Q) \ set (dra.accepting (AA ! k))" using 4(4) by this show "(P, Q) = (P, Q)" by rule have "True \ infs (P \ get k) (dra.trace (draul AA) w (map dra.initial AA))" using 3(2) unfolding draul_def 4(2) by simp also have "\ \ infs P (dra.trace (AA ! k) w (map dra.initial AA ! k))" using 4(1) by (force intro!: draul_get) also have "map dra.initial AA ! k = dra.initial (AA ! k)" using 4(1) by simp finally show "infs P (dra.trace (AA ! k) w (dra.initial (AA ! k)))" by simp have "False \ infs (Q \ get k) (dra.trace (draul AA) w (map dra.initial AA))" using 3(3) unfolding draul_def 4(3) by simp also have "\ \ infs Q (dra.trace (AA ! k) w (map dra.initial AA ! k))" using 4(1) by (force intro!: draul_get) also have "map dra.initial AA ! k = dra.initial (AA ! k)" using 4(1) by simp finally show "fins Q (dra.trace (AA ! k) w (dra.initial (AA ! k)))" by simp qed next fix A w assume 1: "A \ set AA" "w \ DRA.language A" obtain 2: "dra.run A w (dra.initial A)" "cogen rabin (dra.accepting A) (dra.trace A w (dra.initial A))" using 1(2) by rule obtain I F where 3: "(I, F) \ set (dra.accepting A)" "infs I (dra.trace A w (dra.initial A))" "fins F (dra.trace A w (dra.initial A))" using 2(2) by blast obtain k where 4: "A = AA ! k" "k < length AA" using 1(1) unfolding in_set_conv_nth by auto show "w \ DRA.language (draul AA)" proof (intro DRA.language cogen rabin) show "dra.run (draul AA) w (dra.initial (draul AA))" using 1(1) 2(1) unfolding DRA.run_alt_def draul_def by auto show "(I \ get k, F \ get k) \ set (dra.accepting (draul AA))" unfolding draul_def List.bind_def using 3(1) 4 by (force simp: comp_def) show "(I \ get k, F \ get k) = (I \ get k, F \ get k)" by rule have "infs (I \ get k) (dra.trace (draul AA) w (dra.initial (draul AA))) \ infs (I \ get k) (dra.trace (draul AA) w (map dra.initial AA))" unfolding draul_def by simp also have "\ \ infs I (dra.trace (AA ! k) w (map dra.initial AA ! k))" using 4(2) by (force intro!: draul_get) also have "\ \ True" using 3(2) 4 by simp finally show "infs (I \ get k) (dra.trace (draul AA) w (dra.initial (draul AA)))" by simp have "infs (F \ get k) (dra.trace (draul AA) w (dra.initial (draul AA))) \ infs (F \ get k) (dra.trace (draul AA) w (map dra.initial AA))" unfolding draul_def by simp also have "\ \ infs F (dra.trace (AA ! k) w (map dra.initial AA ! k))" using 4(2) by (force intro!: draul_get) also have "\ \ False" using 3(3) 4 by simp finally show "fins (F \ get k) (dra.trace (draul AA) w (dra.initial (draul AA)))" by simp qed qed end \ No newline at end of file diff --git a/thys/Transition_Systems_and_Automata/Basic/Acceptance.thy b/thys/Transition_Systems_and_Automata/Basic/Acceptance.thy --- a/thys/Transition_Systems_and_Automata/Basic/Acceptance.thy +++ b/thys/Transition_Systems_and_Automata/Basic/Acceptance.thy @@ -1,48 +1,51 @@ theory Acceptance -imports "Sequence_LTL" +imports Sequence_LTL begin type_synonym 'a pred = "'a \ bool" type_synonym 'a rabin = "'a pred \ 'a pred" type_synonym 'a gen = "'a list" + (* TODO: move to degeneralization theory *) type_synonym 'a degen = "'a \ nat" definition rabin :: "'a rabin \ 'a stream pred" where "rabin \ \ (I, F) w. infs I w \ fins F w" lemma rabin[intro]: assumes "IF = (I, F)" "infs I w" "fins F w" shows "rabin IF w" using assms unfolding rabin_def by auto lemma rabin_elim[elim]: assumes "rabin IF w" obtains I F where "IF = (I, F)" "infs I w" "fins F w" using assms unfolding rabin_def by auto definition gen :: "('a \ 'b pred) \ ('a gen \ 'b pred)" where - "gen P xs w \ \ x \ set xs. P x w" + "gen P cs w \ \ c \ set cs. P c w" lemma gen[intro]: - assumes "\ x. x \ set xs \ P x w" - shows "gen P xs w" + assumes "\ c. c \ set cs \ P c w" + shows "gen P cs w" using assms unfolding gen_def by auto lemma gen_elim[elim]: - assumes "gen P xs w" - obtains "\ x. x \ set xs \ P x w" + assumes "gen P cs w" + obtains "\ c. c \ set cs \ P c w" using assms unfolding gen_def by auto definition cogen :: "('a \ 'b pred) \ ('a gen \ 'b pred)" where - "cogen P xs w \ \ x \ set xs. P x w" + "cogen P cs w \ \ c \ set cs. P c w" lemma cogen[intro]: - assumes "x \ set xs" "P x w" - shows "cogen P xs w" + assumes "c \ set cs" "P c w" + shows "cogen P cs w" using assms unfolding cogen_def by auto lemma cogen_elim[elim]: - assumes "cogen P xs w" - obtains x - where "x \ set xs" "P x w" + assumes "cogen P cs w" + obtains c + where "c \ set cs" "P c w" using assms unfolding cogen_def by auto + lemma cogen_alt_def: "cogen P cs w \ \ gen (\ c w. Not (P c w)) cs w" by auto + end \ No newline at end of file diff --git a/thys/Transition_Systems_and_Automata/Basic/Basic.thy b/thys/Transition_Systems_and_Automata/Basic/Basic.thy --- a/thys/Transition_Systems_and_Automata/Basic/Basic.thy +++ b/thys/Transition_Systems_and_Automata/Basic/Basic.thy @@ -1,32 +1,31 @@ section \Basics\ theory Basic imports Main begin subsection \Miscellaneous\ abbreviation (input) "const x \ \ _. x" lemmas [simp] = map_prod.id map_prod.comp[symmetric] lemma prod_UNIV[iff]: "A \ B = UNIV \ A = UNIV \ B = UNIV" by auto lemma infinite_subset[trans]: "infinite A \ A \ B \ infinite B" using infinite_super by this lemma finite_subset[trans]: "A \ B \ finite B \ finite A" using finite_subset by this declare infinite_coinduct[case_names infinite, coinduct pred: infinite] lemma infinite_psubset_coinduct[case_names infinite, consumes 1]: assumes "R A" assumes "\ A. R A \ \ B \ A. R B" shows "infinite A" proof - assume "finite A" - then show "False" using assms by (induct rule: finite_psubset_induct) (auto) + show "False" if "finite A" using that assms by (induct rule: finite_psubset_induct) (auto) qed (* TODO: why are there two copies of this theorem? *) thm inj_on_subset subset_inj_on lemma inj_inj_on[dest]: "inj f \ inj_on f S" using inj_on_subset by auto end 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,433 +1,436 @@ section \Finite and Infinite Sequences\ theory Sequence imports "Basic" "HOL-Library.Stream" "HOL-Library.Monad_Syntax" begin subsection \List Basics\ 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 \ lists A \ set w \ 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 \ g = xs \ g \ f" unfolding List.bind_def by simp lemma listset_member: "ys \ listset XS \ list_all2 (\) ys XS" by (induct XS arbitrary: ys) (auto simp: set_Cons_def list_all2_Cons2) lemma listset_empty[iff]: "listset XS = {} \ \ list_all (\ A. A \ {}) XS" by (induct XS) (auto simp: set_Cons_def) lemma listset_finite[iff]: assumes "list_all (\ A. A \ {}) XS" shows "finite (listset XS) \ 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 \ listset XS)" by (auto simp: set_Cons_def) also have "finite \ \ finite (A \ listset XS)" by (simp add: inj_on_def) also have "\ \ finite A \ finite (listset XS)" using Cons(2) by simp also have "finite (listset XS) \ list_all finite XS" using Cons by simp also have "finite A \ \ \ list_all finite (A # XS)" by simp finally show ?case by this qed 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 \ listset XS)" by (auto simp: set_Cons_def) also have "card \ = card (A \ listset XS)" using card_image 1 by auto also have "\ = 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 * \ = prod_list (map card (A # XS))" by simp finally show ?case by this qed subsection \Stream Basics\ 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 "\ a u b v. R (a ## u) (b ## v) \ P a b \ 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 "\ u v. R u v \ \ u\<^sub>1 u\<^sub>2 v\<^sub>1 v\<^sub>2. u = u\<^sub>1 @- u\<^sub>2 \ v = v\<^sub>1 @- v\<^sub>2 \ u\<^sub>1 \ [] \ v\<^sub>1 \ [] \ list_all2 P u\<^sub>1 v\<^sub>1 \ R u\<^sub>2 v\<^sub>2" shows "stream_all2 P u v" proof - have "\ u\<^sub>1 u\<^sub>2 v\<^sub>1 v\<^sub>2. u = u\<^sub>1 @- u\<^sub>2 \ v = v\<^sub>1 @- v\<^sub>2 \ list_all2 P u\<^sub>1 v\<^sub>1 \ 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 "\ a w. R (a ## w) \ P a \ 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 "\ w. R w \ \ u v. w = u @- v \ u \ [] \ list_all P u \ R v" shows "pred_stream P w" proof - have "\ u v. w = u @- v \ list_all P u \ 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 "\ w ws. R (w ## ws) \ w \ [] \ list_all P w \ 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) \ list_all P u \ 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) \ list_all2 P u\<^sub>1 v\<^sub>1 \ stream_all2 P u\<^sub>2 v\<^sub>2" using assms by (induct rule: list_induct2) (auto) lemma sset_subset_stream_pred: "sset w \ A \ pred_stream (\ a. a \ A) w" unfolding stream.pred_set by auto lemma eq_scons: "w = a ## v \ a = shd w \ v = stl w" by auto lemma scons_eq: "a ## v = w \ shd w = a \ stl w = v" by auto lemma eq_shift: "w = u @- v \ stake (length u) w = u \ sdrop (length u) w = v" by (induct u arbitrary: w) (force+) lemma shift_eq: "u @- v = w \ u = stake (length u) w \ v = sdrop (length u) w" by (induct u arbitrary: w) (force+) lemma scons_eq_shift: "a ## w = u @- v \ ([] = u \ a ## w = v) \ (\ u'. a # u' = u \ w = u' @- v)" by (cases u) (auto) lemma shift_eq_scons: "u @- v = a ## w \ (u = [] \ v = a ## w) \ (\ u'. u = a # u' \ u' @- v = w)" by (cases u) (auto) lemma stream_all2_sset1: assumes "stream_all2 P xs ys" shows "\ x \ sset xs. \ y \ sset ys. P x y" proof - have "pred_stream (\ x. \ y \ S. P x y) xs" if "sset ys \ 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 "\ y \ sset ys. \ x \ sset xs. P x y" proof - have "pred_stream (\ y. \ x \ S. P x y) ys" if "sset xs \ 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 \ f (shd xs) = y \ smap f (stl xs) = ys" using smap_ctr by metis lemma scons_eq_smap[iff]: "y ## ys = smap f xs \ y = f (shd xs) \ ys = smap f (stl xs)" using smap_ctr by metis lemma smap_eq_shift[iff]: "smap f w = u @- v \ (\ w\<^sub>1 w\<^sub>2. w = w\<^sub>1 @- w\<^sub>2 \ map f w\<^sub>1 = u \ 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 \ (\ w\<^sub>1 w\<^sub>2. w = w\<^sub>1 @- w\<^sub>2 \ u = map f w\<^sub>1 \ 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 \ (shd xs, shd ys) = z \ szip (stl xs) (stl ys) = zs" using szip.ctr stream.inject by metis lemma scons_eq_szip[iff]: "z ## zs = szip xs ys \ z = (shd xs, shd ys) \ zs = szip (stl xs) (stl ys)" using szip.ctr stream.inject by metis lemma siterate_eq_scons[iff]: "siterate f s = a ## w \ s = a \ siterate f (f s) = w" using siterate.ctr stream.inject by metis lemma scons_eq_siterate[iff]: "a ## w = siterate f s \ a = s \ 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 "\ 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 \ (\ i. P (w !! i))" unfolding stream.pred_set sset_range by simp lemma stream_rel_snth: "stream_all2 P u v \ (\ 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 "\ 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 \ 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 \ x = y" by (auto) (metis siterate.simps(1)) lemma stream_pred__sconst[iff]: "pred_stream P (sconst x) \ P x" unfolding stream_pred_snth by simp lemma stream_rel_sconst[iff]: "stream_all2 P (sconst x) (sconst y) \ P x y" unfolding stream_rel_snth by simp lemma set_sset_stake[intro!, simp]: "set (stake n xs) \ sset xs" by (metis sset_shift stake_sdrop sup_ge1) lemma sset_sdrop[intro!, simp]: "sset (sdrop n xs) \ sset xs" by (metis sset_shift stake_sdrop sup_ge2) lemma set_stake_snth: "x \ set (stake n xs) \ (\ 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 \(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 \ sset xs \ {}" obtains ys a zs where "xs = ys @- a ## zs" "A \ set ys = {}" "a \ A" proof let ?n = "LEAST n. xs !! n \ A" have 1: "xs !! n \ 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 \ set (stake ?n xs) = {}" using 1 by (metis (no_types, lifting) disjoint_iff_not_equal set_stake_snth) show "xs !! ?n \ A" using assms unfolding sset_range by (auto intro: LeastI) qed lemma split_stream_first': assumes "x \ sset xs" obtains ys zs where "xs = ys @- x ## zs" "x \ 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 \ 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 \ set (stake ?n xs)" using 2 by (meson set_stake_snth) qed lemma streams_UNIV[iff]: "streams A = UNIV \ A = UNIV" proof show "A = UNIV \ streams A = UNIV" by simp next assume "streams A = UNIV" then have "w \ streams A" for w by simp then have "sset w \ A" for w unfolding streams_iff_sset by this then have "sset (sconst a) \ A" for a by blast then have "a \ 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 \The @{term scan} Function\ + subsection \The scan Function\ primrec (transfer) scan :: "('a \ 'b \ 'b) \ 'a list \ 'b \ '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 = [] \ xs = []" by (cases xs) (auto) lemma scan_eq_cons[iff]: "scan f xs a = b # w \ (\ y ys. xs = y # ys \ f y a = b \ scan f ys (f y a) = w)" by (cases xs) (auto) lemma scan_eq_append[iff]: "scan f xs a = u @ v \ (\ ys zs. xs = ys @ zs \ scan f ys a = u \ 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 \ 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 \ 'b \ 'b) \ 'a stream \ 'b \ '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 \ f (shd xs) a = b \ 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 \ b = f (shd xs) a \ 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 \ 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 \Distinct Streams\ coinductive sdistinct :: "'a stream \ bool" where scons[intro!]: "x \ sset xs \ sdistinct xs \ sdistinct (x ## xs)" lemma sdistinct_scons_elim[elim!]: assumes "sdistinct (x ## xs)" obtains "x \ sset xs" "sdistinct xs" using assms by (auto elim: sdistinct.cases) lemma sdistinct_coinduct[case_names sdistinct, coinduct pred: sdistinct]: assumes "P xs" assumes "\ x xs. P (x ## xs) \ x \ sset xs \ P xs" shows "sdistinct xs" using stream.collapse sdistinct.coinduct assms by metis lemma sdistinct_shift[intro!]: assumes "distinct xs" "sdistinct ys" "set xs \ 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 \ 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 "\ sdistinct w" obtains u v a w' where "w = u @- a ## v @- a ## w'" proof (rule ccontr) assume 1: "\ thesis" assume 2: "w = u @- a ## v @- a ## w' \ thesis" for u a v w' have 3: "\ u v a w'. w \ 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 \Sorted Streams\ coinductive (in order) sascending :: "'a stream \ bool" where "a \ b \ sascending (b ## w) \ sascending (a ## b ## w)" coinductive (in order) sdescending :: "'a stream \ bool" where "a \ b \ sdescending (b ## w) \ sdescending (a ## b ## w)" lemma sdescending_coinduct[case_names sdescending, coinduct pred: sdescending]: assumes "P w" assumes "\ a b w. P (a ## b ## w) \ a \ b \ 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 \ b" by rule then show "w !! k \ 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 \ 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 \ 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_LTL.thy b/thys/Transition_Systems_and_Automata/Basic/Sequence_LTL.thy --- a/thys/Transition_Systems_and_Automata/Basic/Sequence_LTL.thy +++ b/thys/Transition_Systems_and_Automata/Basic/Sequence_LTL.thy @@ -1,112 +1,114 @@ section \Linear Temporal Logic on Streams\ theory Sequence_LTL imports "Sequence" "HOL-Library.Linear_Temporal_Logic_on_Streams" begin subsection \Basics\ - text \Avoid destroying the constant @{term holds} prematurely.\ + text \Avoid destroying the constant @{const holds} prematurely.\ lemmas [simp del] = holds.simps holds_eq1 holds_eq2 not_holds_eq + lemma ev_smap[iff]: "ev P (smap f w) \ ev (P \ smap f) w" using ev_smap unfolding comp_apply by this + lemma alw_smap[iff]: "alw P (smap f w) \ alw (P \ smap f) w" using alw_smap unfolding comp_apply by this lemma holds_smap[iff]: "holds P (smap f w) \ holds (P \ f) w" unfolding holds.simps by simp - lemmas [iff] = ev_sconst alw_sconst ev_smap alw_smap hld_smap' + lemmas [iff] = ev_sconst alw_sconst hld_smap' lemmas [iff] = alw_ev_stl lemma alw_ev_sdrop[iff]: "alw (ev P) (sdrop n w) \ alw (ev P) w" using alw_ev_sdrop alw_sdrop by blast lemma alw_ev_scons[iff]: "alw (ev P) (a ## w) \ alw (ev P) w" by (metis alw_ev_stl stream.sel(2)) lemma alw_ev_shift[iff]: "alw (ev P) (u @- v) \ alw (ev P) v" by (induct u) (auto) lemmas [simp del, iff] = ev_alw_stl lemma ev_alw_sdrop[iff]: "ev (alw P) (sdrop n w) \ ev (alw P) w" using alwD alw_alw alw_sdrop ev_alw_imp_alw_ev not_ev_iff by metis lemma ev_alw_scons[iff]: "ev (alw P) (a ## w) \ ev (alw P) w" by (metis ev_alw_stl stream.sel(2)) lemma ev_alw_shift[iff]: "ev (alw P) (u @- v) \ ev (alw P) v" by (induct u) (auto) lemma holds_sconst[iff]: "holds P (sconst a) \ P a" unfolding holds.simps by simp lemma HLD_sconst[iff]: "HLD A (sconst a) \ a \ A" unfolding HLD_def holds.simps by simp lemma ev_alt_def: "ev \ w \ (\ u v. w = u @- v \ \ v)" using ev.base ev_shift ev_imp_shift by metis lemma ev_stl_alt_def: "ev \ (stl w) \ (\ u v. w = u @- v \ u \ [] \ \ v)" unfolding ev_alt_def by (cases w) (force simp: scons_eq) lemma ev_HLD_sset: "ev (HLD A) w \ sset w \ A \ {}" unfolding HLD_def ev_holds_sset by auto lemma alw_ev_coinduct[case_names alw_ev, consumes 1]: assumes "R w" assumes "\ w. R w \ ev \ w \ ev R (stl w)" shows "alw (ev \) w" proof - have "ev R w" using assms(1) by rule then show ?thesis using assms(2) by (coinduct) (metis alw_sdrop not_ev_iff sdrop_stl sdrop_wait) qed subsection \Infinite Occurrence\ abbreviation "infs P w \ alw (ev (holds P)) w" abbreviation "fins P w \ \ infs P w" lemma infs_suffix: "infs P w \ (\ u v. w = u @- v \ Bex (sset v) P)" using alwD alw_iff_sdrop alw_shift ev_holds_sset stake_sdrop by (metis (mono_tags, hide_lams)) lemma infs_snth: "infs P w \ (\ n. \ k \ n. P (w !! k))" by (auto simp: alw_iff_sdrop ev_iff_sdrop holds.simps intro: le_add1 dest: le_Suc_ex) lemma infs_infm: "infs P w \ (\\<^sub>\ i. P (w !! i))" unfolding infs_snth INFM_nat_le by rule lemma infs_coinduct[case_names infs, coinduct pred: infs]: assumes "R w" assumes "\ w. R w \ Bex (sset w) P \ ev R (stl w)" shows "infs P w" using assms by (coinduct rule: alw_ev_coinduct) (auto simp: ev_holds_sset) lemma infs_set_coinduct[case_names infs_set, consumes 1]: assumes "R w" assumes "\ w. R w \ \ u v. w = u @- v \ Bex (set u) P \ R v" shows "infs P w" using assms by (coinduct) (force simp: ev_stl_alt_def) lemma infs_flat_coinduct[case_names infs_flat, consumes 1]: assumes "R w" assumes "\ u v. R (u ## v) \ Bex (set u) P \ R v" shows "infs P (flat w)" using assms by (coinduction arbitrary: w rule: infs_set_coinduct) (metis empty_iff flat_Stream list.set(1) stream.exhaust) lemma infs_mono: "(\ a. a \ sset w \ P a \ Q a) \ infs P w \ infs Q w" unfolding infs_snth by force lemma infs_mono_strong: "stream_all2 (\ a b. P a \ Q b) u v \ infs P u \ infs Q v" unfolding stream_rel_snth infs_snth by blast lemma infs_all: "Ball (sset w) P \ infs P w" unfolding infs_snth by auto lemma infs_any: "infs P w \ Bex (sset w) P" unfolding ev_holds_sset by auto lemma infs_bot[iff]: "infs bot w \ False" using infs_any by auto lemma infs_top[iff]: "infs top w \ True" by (simp add: infs_all) lemma infs_disj[iff]: "infs (\ a. P a \ Q a) w \ infs P w \ infs Q w" unfolding infs_snth using le_trans le_cases by metis lemma infs_bex[iff]: assumes "finite S" shows "infs (\ a. \ x \ S. P x a) w \ (\ x \ S. infs (P x) w)" using assms infs_any by induct auto lemma infs_bex_le_nat[iff]: "infs (\ a. \ k < n :: nat. P k a) w \ (\ k < n. infs (P k) w)" proof - have "infs (\ a. \ k < n. P k a) w \ infs (\ a. \ k \ {k. k < n}. P k a) w" by simp also have "\ \ (\ k \ {k. k < n}. infs (P k) w)" by blast also have "\ \ (\ k < n. infs (P k) w)" by simp finally show ?thesis by this qed lemma infs_cycle[iff]: assumes "w \ []" shows "infs P (cycle w) \ Bex (set w) P" proof show "infs P (cycle w) \ Bex (set w) P" using assms by (auto simp: ev_holds_sset dest: alwD) show "Bex (set w) P \ infs P (cycle w)" using assms by (coinduction rule: infs_set_coinduct) (blast dest: cycle_decomp) qed end \ No newline at end of file