diff --git a/thys/Labeled_Transition_Systems/LTS.thy b/thys/Labeled_Transition_Systems/LTS.thy new file mode 100644 --- /dev/null +++ b/thys/Labeled_Transition_Systems/LTS.thy @@ -0,0 +1,1761 @@ +theory LTS imports Main "HOL-Library.Multiset_Order" begin + + +section \LTS\ + + +subsection \Transitions\ + +type_synonym ('state, 'label) transition = "'state \ 'label \ 'state" + + +subsection \LTS functions\ + +fun trans_hd :: "('state, 'label) transition \ 'state" where + "trans_hd (s1,\,s2) = s1" + +fun trans_tl :: "('state, 'label) transition \ 'state" where + "trans_tl (s1,\,s2) = s2" + +fun transitions_of :: "'state list * 'label list \ ('state, 'label) transition multiset" where + "transitions_of (s1#s2#ss, \#w) = {# (s1, \, s2) #} + transitions_of (s2#ss, w)" +| "transitions_of ([s1],_) = {#}" +| "transitions_of ([],_) = {#}" +| "transitions_of (_,[]) = {#}" + +fun transition_list :: "'state list * 'label list \ ('state, 'label) transition list" where + "transition_list (s1#s2#ss, \#w) = (s1, \, s2) # (transition_list (s2#ss, w))" +| "transition_list ([s1],_) = []" +| "transition_list ([],_) = []" +| "transition_list (_,[]) = []" + +fun transition_list' :: "'state * 'label list * 'state list * 'state \ ('state, 'label) transition list" where + "transition_list' (p,w,ss,q) = transition_list (ss, w)" + +fun transitions_of' :: "'state * 'label list * 'state list * 'state \ ('state, 'label) transition multiset" where + "transitions_of' (p,w,ss,q) = transitions_of (ss, w)" + +fun transition_list_of' where + "transition_list_of' (p,\#w,p'#p''#ss,q) = (p, \, p'')#(transition_list_of' (p'',w,p''#ss,q))" +| "transition_list_of' (p, [], _, p'') = []" +| "transition_list_of' (p, _, [], p'') = []" (* Equivalent to the above *) +| "transition_list_of' (v, va # vc, [vf], ve) = []" (* Should not occur *) + +fun append_path_with_word :: "('a list \ 'b list) \ ('a list \ 'b list) \ ('a list \ 'b list)" (infix "@\" 65) where + "(ss1,w1) @\ (ss2,w2) = (ss1@(tl ss2), w1 @ w2)" + +fun append_path_with_word_\ :: "(('a list \ 'b list) * 'b) \ ('a list \ 'b list) \ ('a list \ 'b list)" (infix "@\<^sup>\" 65) where + "((ss1,w1),\) @\<^sup>\ (ss2,w2) = (ss1@ss2, w1 @ [\] @ w2)" + +fun append_trans_star_states :: "('a \ 'b list \ 'a list \ 'a) \ ('a \ 'b list \ 'a list \ 'a) \ ('a \ 'b list \ 'a list \ 'a)" (infix "@@\" 65) where + "(p1,w1,ss1,q1) @@\ (p2,w2,ss2,q2) = (p1, w1 @ w2, ss1@(tl ss2), q2)" + +fun append_trans_star_states_\ :: "(('a \ 'b list \ 'a list \ 'a) * 'b) \ ('a \ 'b list \ 'a list \ 'a) \ ('a \ 'b list \ 'a list \ 'a)" (infix "@@\<^sup>\" 65) where + "((p1,w1,ss1,q1),\) @@\<^sup>\ (p2,w2,ss2,q2) = (p1, w1 @ [\] @ w2, ss1@ss2, q2)" + +definition inters :: "('state, 'label) transition set \ ('state, 'label) transition set \ (('state * 'state), 'label) transition set" where + "inters ts1 ts2 = {((p1, q1), \, (p2, q2)). (p1, \, p2) \ ts1 \ (q1, \, q2) \ ts2}" + +definition inters_finals :: "'state set \ 'state set \ ('state * 'state) set" where + "inters_finals finals1 finals2 = finals1 \ finals2" + +lemma inters_code[code]: + "inters ts1 ts2 = (\(p1, \, p2) \ ts1. \(q1, \', q2) \ ts2. if \ = \' then {((p1, q1), \, (p2, q2))} else {})" + unfolding inters_def by (force split: if_splits) + + +subsection \LTS locale\ + +locale LTS = + fixes transition_relation :: "('state, 'label) transition set" +begin + +text \More definitions.\ + +definition step_relp :: "'state \ 'state \ bool" (infix "\" 80) where + "c \ c' \ (\l. (c, l, c') \ transition_relation)" + +abbreviation step_starp :: "'state \ 'state \ bool" (infix "\\<^sup>*" 80) where + "c \\<^sup>* c' \ step_relp\<^sup>*\<^sup>* c c'" + +definition step_rel :: "'state rel" where + "step_rel = {(c, c'). step_relp c c'}" + +definition step_star :: "'state rel" where + "step_star = {(c, c'). step_starp c c'}" + +(* For a set of states C, post*(C) is the set of all states reachable from C. *) +definition post_star :: "'state set \ 'state set" where + "post_star C = {c'. \c \ C. c \\<^sup>* c'}" + +(* And pre*(C) is the set of all states that can reach a state in C. *) +definition pre_star :: "'state set \ 'state set" where + "pre_star C = {c'. \c \ C. c' \\<^sup>* c}" + +inductive_set path :: "'state list set" where + "[s] \ path" +| "(s'#ss) \ path \ (s,l,s') \ transition_relation \ s#s'#ss \ path" + +inductive_set trans_star :: "('state * 'label list * 'state) set" where + trans_star_refl[iff]: + "(p, [], p) \ trans_star" +| trans_star_step: + "(p,\,q') \ transition_relation \ + (q',w,q) \ trans_star \ + (p, \#w, q) \ trans_star" + +inductive_cases trans_star_empty [elim]: "(p, [], q) \ trans_star" +inductive_cases trans_star_cons: "(p, \#w, q) \ trans_star" + + +inductive_set trans_star_states :: "('state * 'label list * 'state list * 'state) set" where + trans_star_states_refl[iff]: + "(p,[],[p],p) \ trans_star_states" +| trans_star_states_step: + "(p,\,q') \ transition_relation \ + (q',w,ss,q) \ trans_star_states \ + (p, \#w, p#ss, q) \ trans_star_states" + +inductive_set path_with_word :: "('state list * 'label list) set" where + path_with_word_refl[iff]: + "([s],[]) \ path_with_word" +| path_with_word_step: + "(s'#ss, w) \ path_with_word \ + (s,l,s') \ transition_relation \ + (s#s'#ss,l#w) \ path_with_word" + +definition start_of :: "('state list \ 'label list) \ 'state" where + "start_of \ = hd (fst \)" + +definition end_of :: "('state list \ 'label list) \ 'state" where + "end_of \ = last (fst \)" + +abbreviation path_with_word_from :: "'state \ ('state list * 'label list) set" where + "path_with_word_from q == {\. \ \ path_with_word \ start_of \ = q}" + +abbreviation path_with_word_to :: "'state \ ('state list * 'label list) set" where + "path_with_word_to q == {\. \ \ path_with_word \ end_of \ = q}" + +abbreviation path_with_word_from_to :: "'state \ 'state \ ('state list * 'label list) set" where + "path_with_word_from_to start end == {\. \ \ path_with_word \ start_of \ = start \ end_of \ = end}" + +inductive_set transition_list_path :: "('state, 'label) transition list set" where + "(q, l, q') \ transition_relation \ + [(q, l, q')] \ transition_list_path" +| "(q, l, q') \ transition_relation \ + (q', l', q'') # ts \ transition_list_path \ + (q, l, q') # (q', l', q'') # ts \ transition_list_path" + +lemma singleton_path_start_end: + assumes "([s], []) \ LTS.path_with_word pg" + shows "start_of ([s], []) = end_of ([s], [])" + using assms + by (simp add: end_of_def start_of_def) + +lemma path_with_word_length: + assumes "(ss, w) \ path_with_word" + shows "length ss = length w + 1" + using assms +proof (induction rule: path_with_word.induct) + case (path_with_word_refl s) + then show ?case by auto +next + case (path_with_word_step s' ss w s l) + then show ?case by auto +qed + +lemma path_with_word_lengths: + assumes "(qs @ [qnminus1], w) \ path_with_word" + shows "length qs = length w" + using assms + by (metis LTS.path_with_word_length Suc_eq_plus1 Suc_inject length_Cons length_append + list.size(3,4)) + +lemma path_with_word_butlast: + assumes "(ss, w) \ path_with_word" + assumes "length ss \ 2" + shows "(butlast ss, butlast w) \ path_with_word" + using assms +proof (induction rule: path_with_word.induct) + case (path_with_word_refl s) + then show ?case + by force +next + case (path_with_word_step s' ss w s l) + then show ?case + by (metis (no_types) LTS.path_with_word.path_with_word_refl + LTS.path_with_word.path_with_word_step LTS.path_with_word_length One_nat_def Suc_1 + Suc_inject Suc_leI Suc_le_mono butlast.simps(2) length_0_conv length_Cons list.distinct(1) + list.size(4) not_gr0) +qed + +lemma transition_butlast: + assumes "(ss, w) \ path_with_word" + assumes "length ss \ 2" + shows "(last (butlast ss), last w, last ss) \ transition_relation" + using assms +proof (induction rule: path_with_word.induct) + case (path_with_word_refl s) + then show ?case + by force +next + case (path_with_word_step s' ss w s l) + then show ?case + by (metis (no_types) LTS.path_with_word_length One_nat_def Suc_1 Suc_inject Suc_leI Suc_le_mono + butlast.simps(2) last.simps length_Cons length_greater_0_conv list.distinct(1) list.size(4)) +qed + +lemma path_with_word_induct_reverse [consumes 1, case_names path_with_word_refl path_with_word_step_rev]: + "(ss, w) \ path_with_word \ + (\s. P [s] []) \ + (\ss s w l s'. (ss @ [s], w) \ path_with_word \ + P (ss @ [s]) w \ + (s, l, s') \ transition_relation \ + P (ss @ [s, s']) (w @ [l])) + \ P ss w" +proof (induction "length ss" arbitrary: ss w) + case 0 + then show ?case + by (metis LTS.path_with_word_length Suc_eq_plus1 Zero_not_Suc) +next + case (Suc n) + + show ?case + proof (cases "n = 0") + case True + then show ?thesis + by (metis LTS.path_with_word_length Suc.hyps(2) Suc.prems(1) Suc.prems(2) Suc_eq_plus1 Suc_inject Suc_length_conv length_0_conv) + next + case False + define ss' where "ss' = butlast (butlast ss)" + define s where "s = last (butlast ss)" + define s' where "s' = last ss" + define w' where "w' = butlast w" + define l where "l = last w" + + have "length ss \ 2" + using False Suc.hyps(2) by linarith + + then have s_split: "ss' @ [s, s'] = ss" + by (metis One_nat_def Suc_1 Suc_le_mono Zero_not_Suc append.assoc append.simps(1) append_Cons + append_butlast_last_id le_less length_append_singleton list.size(3) s'_def s_def ss'_def + zero_order(3)) + + have w_split: "w' @ [l] = w" + by (metis LTS.path_with_word_length Suc.prems(1) add.commute butlast.simps(2) butlast_append + l_def length_0_conv length_Suc_conv list.simps(3) plus_1_eq_Suc s_split + snoc_eq_iff_butlast w'_def) + + have ss'w'_path: "(ss' @ [s], w') \ path_with_word" + using Suc(3) path_with_word_butlast + by (metis (no_types, lifting) \2 \ length ss\ butlast.simps(2) butlast_append list.simps(3) + s_split w'_def) + + have tr: "(s, l, s') \ transition_relation" + using Suc(3) s'_def s_def l_def transition_butlast \2 \ length ss\ by presburger + + have nl: "n = length (ss' @ [s])" + by (metis LTS.path_with_word_length Suc.hyps(2) Suc.prems(1) Suc_eq_plus1 + length_append_singleton nat.inject ss'w'_path w_split) + + have "P (ss' @ [s]) w'" + using Suc(1)[of "ss' @ [s]" w', OF nl ss'w'_path Suc(4)] Suc(5) by metis + + then have "P (ss' @ [s, s']) (w' @ [l])" + using Suc(5)[of ss' s w' l s'] ss'w'_path tr by auto + then show ?thesis + using s_split w_split by auto + qed +qed + +lemma path_with_word_from_induct_reverse: + "(ss, w) \ path_with_word_from start \ + (\s. P [s] []) \ + (\ss s w l s'. (ss @ [s], w) \ path_with_word_from start \ + P (ss @ [s]) w \ + (s, l, s') \ transition_relation \ + P (ss @ [s, s']) (w @ [l])) + \ P ss w" +proof (induction "length ss" arbitrary: ss w) + case 0 + then show ?case + by (metis (no_types, lifting) Suc_eq_plus1 mem_Collect_eq nat.simps(3) path_with_word_length) +next + case (Suc n) + + show ?case + proof (cases "n = 0") + case True + then show ?thesis + using Suc.prems(1,2) length_0_conv list.distinct(1) path_with_word.cases + by (metis (no_types, lifting) Suc.hyps(2) length_Suc_conv list.inject mem_Collect_eq) + next + case False + define ss' where "ss' = butlast (butlast ss)" + define s where "s = last (butlast ss)" + define s' where "s' = last ss" + define w' where "w' = butlast w" + define l where "l = last w" + + have len_ss: "length ss \ 2" + using False Suc.hyps(2) by linarith + + then have s_split: "ss' @ [s, s'] = ss" + by (metis One_nat_def Suc_1 Suc_le_mono Zero_not_Suc append.assoc append.simps(1) append_Cons + append_butlast_last_id le_less length_append_singleton list.size(3) s'_def s_def ss'_def + zero_order(3)) + + have w_split: "w' @ [l] = w" + by (metis (no_types, lifting) False LTS.path_with_word_length One_nat_def Suc.hyps(2) + Suc.prems(1) Suc_inject add.right_neutral add_Suc_right l_def list.size(3) mem_Collect_eq + snoc_eq_iff_butlast w'_def) + + have ss'w'_path: "(ss' @ [s], w') \ path_with_word" + using Suc(3) path_with_word_butlast len_ss + by (metis (no_types, lifting) butlast.simps(2) butlast_append list.discI mem_Collect_eq + not_Cons_self2 s_split w'_def) + + have ss'w'_path_from: "(ss' @ [s], w') \ path_with_word_from start" + using Suc(3) butlast.simps(2) start_of_def list.sel(1) list.simps(3) mem_Collect_eq + path_with_word.simps prod.sel(1) s_def snoc_eq_iff_butlast ss'_def ss'w'_path w_split + by (metis (no_types, lifting) hd_append) + + have tr: "(s, l, s') \ transition_relation" + using Suc(3) s'_def s_def l_def transition_butlast len_ss by blast + + have nl: "n = length (ss' @ [s])" + using False Suc.hyps(2) ss'_def by force + + have "P (ss' @ [s]) w'" + using Suc(1)[of "ss' @ [s]" w', OF nl ss'w'_path_from Suc(4) ] Suc(5) by fastforce + + then have "P (ss' @ [s, s']) (w' @ [l])" + using Suc(5)[of ss' s w' l s'] tr ss'w'_path_from by blast + then show ?thesis + using s_split w_split by auto + qed +qed + +inductive transition_of :: "('state, 'label) transition \ 'state list * 'label list \ bool" where + "transition_of (s1,\,s2) (s1#s2#ss, \#w)" +| "transition_of (s1,\,s2) (ss, w) \ + transition_of (s1,\,s2) (s#ss, \#w)" + +lemma path_with_word_not_empty[simp]: "\([],w) \ path_with_word" + using LTS.path_with_word.cases by blast + +lemma trans_star_path_with_word: + assumes "(p, w, q) \ trans_star" + shows "\ss. hd ss = p \ last ss = q \ (ss, w) \ path_with_word" + using assms +proof (induction rule: trans_star.inducts) + case (trans_star_refl p) + then show ?case + by (meson LTS.path_with_word.path_with_word_refl last.simps list.sel(1)) +next + case (trans_star_step p \ q' w q) + then show ?case + by (metis LTS.path_with_word.simps hd_Cons_tl last_ConsR list.discI list.sel(1)) +qed + +lemma trans_star_trans_star_states: + assumes "(p, w, q) \ trans_star" + shows "\ss. (p, w, ss, q) \ trans_star_states" + using assms +proof (induction rule: trans_star.induct) + case (trans_star_refl p) + then show ?case by auto +next + case (trans_star_step p \ q' w q) + then show ?case + by (meson LTS.trans_star_states_step) +qed + +lemma trans_star_states_trans_star: + assumes "(p, w, ss, q) \ trans_star_states" + shows "(p, w, q) \ trans_star" + using assms +proof (induction rule: trans_star_states.induct) + case (trans_star_states_refl p) + then show ?case by auto +next + case (trans_star_states_step p \ q' w q) + then show ?case + by (meson LTS.trans_star.trans_star_step) +qed + +lemma path_with_word_trans_star: + assumes "(ss, w) \ path_with_word" + assumes "length ss \ 0" + shows "(hd ss, w, last ss) \ trans_star" + using assms +proof (induction rule: path_with_word.inducts) + case (path_with_word_refl s) + show ?case + by simp +next + case (path_with_word_step s' ss w s l) + then show ?case + using LTS.trans_star.trans_star_step by fastforce +qed + +lemma path_with_word_trans_star_Cons: + assumes "(s1#ss@[s2], w) \ path_with_word" + shows "(s1, w, s2) \ trans_star" + using assms path_with_word_trans_star by force + +lemma path_with_word_trans_star_Singleton: + assumes "([s2], w) \ path_with_word" + shows "(s2, [], s2) \ trans_star" + using assms path_with_word_trans_star by force + +lemma trans_star_split: + assumes "(p'', u1 @ w1, q) \ trans_star" + shows "\q1. (p'', u1, q1) \ trans_star \ (q1, w1, q) \ trans_star" + using assms +proof(induction u1 arbitrary: p'') + case Nil + then show ?case by auto +next + case (Cons a u1) + then show ?case + by (metis LTS.trans_star.trans_star_step LTS.trans_star_cons append_Cons) +qed + +lemma trans_star_states_append: + assumes "(p2, w2, w2_ss, q') \ trans_star_states" + assumes "(q', v, v_ss, q) \ trans_star_states" + shows "(p2, w2 @ v, w2_ss @ tl v_ss, q) \ trans_star_states" + using assms +proof (induction rule: trans_star_states.induct) + case (trans_star_states_refl p) + then show ?case + by (metis append_Cons append_Nil list.sel(3) trans_star_states.simps) +next + case (trans_star_states_step p \ q' w ss q) + then show ?case + using LTS.trans_star_states.trans_star_states_step by fastforce +qed + +lemma trans_star_states_length: + assumes "(p, u, u_ss, p1) \ trans_star_states" + shows "length u_ss = Suc (length u)" + using assms +proof (induction rule: trans_star_states.induct) + case (trans_star_states_refl p) + then show ?case + by simp +next + case (trans_star_states_step p \ q' w ss q) + then show ?case + by simp +qed + +lemma trans_star_states_last: + assumes "(p, u, u_ss, p1) \ trans_star_states" + shows "p1 = last u_ss" + using assms +proof (induction rule: trans_star_states.induct) + case (trans_star_states_refl p) + then show ?case + by simp +next + case (trans_star_states_step p \ q' w ss q) + then show ?case + using LTS.trans_star_states.cases by force +qed + +lemma trans_star_states_hd: + assumes "(q', v, v_ss, q) \ trans_star_states" + shows "q' = hd v_ss" + using assms +proof (induction rule: trans_star_states.induct) + case (trans_star_states_refl p) + then show ?case + by simp +next + case (trans_star_states_step p \ q' w ss q) + then show ?case + by force +qed + +lemma trans_star_states_transition_relation: + assumes "(p, \#w_rest, ss, q) \ trans_star_states" + shows "\s \'. (s, \', q) \ transition_relation" + using assms +proof (induction w_rest arbitrary: ss p \) + case Nil + then show ?case + by (metis LTS.trans_star_empty LTS.trans_star_states_trans_star trans_star_cons) +next + case (Cons a w_rest) + then show ?case + by (meson LTS.trans_star_cons LTS.trans_star_states_trans_star trans_star_trans_star_states) +qed + +lemma trans_star_states_path_with_word: + assumes "(p, w, ss, q) \ trans_star_states" + shows "(ss,w) \ path_with_word" + using assms +proof (induction rule: trans_star_states.induct) + case (trans_star_states_refl p) + then show ?case by auto +next + case (trans_star_states_step p \ q' w ss q) + then show ?case + by (metis LTS.trans_star_states.simps path_with_word.path_with_word_step) +qed + +lemma path_with_word_trans_star_states: + assumes "(ss,w) \ path_with_word" + assumes "p = hd ss" + assumes "q = last ss" + shows "(p, w, ss, q) \ trans_star_states" + using assms +proof (induction arbitrary: p q rule: path_with_word.induct) + case (path_with_word_refl s) + then show ?case + by simp +next + case (path_with_word_step s' ss w s l) + then show ?case + using trans_star_states.trans_star_states_step by auto +qed + +lemma append_path_with_word_path_with_word: + assumes "last \2ss = hd v_ss" + assumes "(\2ss, \2\) \ path_with_word" + assumes "(v_ss, v) \ path_with_word" + shows "(\2ss, \2\) @\ (v_ss, v) \ path_with_word" + by (metis LTS.trans_star_states_path_with_word append_path_with_word.simps + path_with_word_trans_star_states assms(1,2,3) trans_star_states_append) + +lemma hd_is_hd: + assumes "(p, w, ss, q) \ trans_star_states" + assumes "(p1, \, q1) = hd (transition_list' (p, w, ss, q))" + assumes "transition_list' (p, w, ss, q) \ []" + shows "p = p1" + using assms +proof (induction rule: trans_star_states.inducts) + case (trans_star_states_refl p) + then show ?case + by auto +next + case (trans_star_states_step p \ q' w ss q) + then show ?case + by (metis LTS.trans_star_states.simps Pair_inject list.sel(1) transition_list'.simps + transition_list.simps(1)) +qed + +definition srcs :: "'state set" where + "srcs = {p. \q \. (q, \, p) \ transition_relation}" + +definition sinks :: "'state set" where + "sinks = {p. \q \. (p, \, q) \ transition_relation}" + +definition isolated :: "'state set" where + "isolated = srcs \ sinks" + +lemma srcs_def2: + "q \ srcs \ (\q' \. (q', \, q) \ transition_relation)" + by (simp add: LTS.srcs_def) + +lemma sinks_def2: + "q \ sinks \ (\q' \. (q, \, q') \ transition_relation)" + by (simp add: LTS.sinks_def) + +lemma isolated_no_edges: + assumes "(p, \, q) \ transition_relation" + shows "p \ isolated \ q \ isolated" + using assms isolated_def srcs_def2 sinks_def2 by fastforce + +lemma source_never_or_hd: + assumes "(ss, w) \ path_with_word" + assumes "p1 \ srcs" + assumes "t = (p1, \, q1)" + shows "count (transitions_of (ss, w)) t = 0 \ + ((hd (transition_list (ss, w)) = t \ count (transitions_of (ss, w)) t = 1))" + using assms +proof (induction rule: path_with_word.induct) + case (path_with_word_refl s) + then show ?case + by simp +next + case (path_with_word_step s' ss w s l) + then have "count (transitions_of (s' # ss, w)) t = 0 \ + (hd (transition_list (s' # ss, w)) = t \ count (transitions_of (s' # ss, w)) t = 1)" + by auto + then show ?case + proof + assume asm: "count (transitions_of (s' # ss, w)) t = 0" + show ?case + proof (cases "s = p1 \ l = \ \ q1 = s'") + case True + then have "hd (transition_list (s # s' # ss, l # w)) = t \ + count (transitions_of (s # s' # ss, l # w)) t = 1" + using path_with_word_step asm by simp + then show ?thesis + by auto + next + case False + then have "count (transitions_of (s # s' # ss, l # w)) t = 0" + using path_with_word_step asm by auto + then show ?thesis + by auto + qed + next + assume "hd (transition_list (s' # ss, w)) = t \ count (transitions_of (s' # ss, w)) t = 1" + moreover + have "(\q \. (q, \, p1) \ transition_relation)" + by (meson LTS.srcs_def2 assms(2)) + ultimately + have False + using path_with_word_step by (auto elim: path_with_word.cases) + then show ?case + by auto + qed +qed + +lemma source_only_hd: + assumes "(ss, w) \ path_with_word" + assumes "p1 \ srcs" + assumes "count (transitions_of (ss, w)) t > 0" + assumes "t = (p1, \, q1)" + shows "hd (transition_list (ss, w)) = t \ count (transitions_of (ss, w)) t = 1" + using source_never_or_hd assms not_gr_zero + by metis + +lemma no_end_in_source: + assumes "(p, w, qq) \ trans_star" + assumes "w \ []" + shows "qq \ srcs" + using assms +proof (induction rule: trans_star.induct) + case (trans_star_refl p) + then show ?case + by blast +next + case (trans_star_step p \ q' w q) + then show ?case + by (metis LTS.srcs_def2 LTS.trans_star_empty) +qed + +lemma transition_list_length_Cons: + assumes "length ss = Suc (length w)" + assumes "hd (transition_list (ss, w)) = (p, \, q)" + assumes "transition_list (ss, w) \ []" + shows "\w' ss'. w = \ # w' \ ss = p # q # ss'" +proof (cases ss) + case Nil + note Nil_outer = Nil + show ?thesis + proof (cases w) + case Nil + then show ?thesis + using assms Nil_outer by auto + next + case (Cons a list) + then show ?thesis + using assms Nil_outer by auto + qed +next + case (Cons a list) + note Cons_outer = Cons + then show ?thesis + proof (cases w) + case Nil + then show ?thesis + using assms Cons_outer by auto + next + case (Cons aa llist) + with Cons_outer assms show ?thesis + by (cases list) auto + qed +qed + +lemma transition_list_Cons: + assumes "(p, w, ss, q) \ trans_star_states" + assumes "hd (transition_list (ss, w)) = (p, \, q1)" + assumes "transition_list (ss, w) \ []" + shows "\w' ss'. w = \ # w' \ ss = p # q1 # ss'" + using assms transition_list_length_Cons by (metis LTS.trans_star_states_length) + +lemma nothing_after_sink: + assumes "([q, q']@ss, \1#w) \ path_with_word" + assumes "q' \ sinks" + shows "ss = [] \ w = []" + using assms +proof (induction rule: path_with_word.induct) + case (path_with_word_refl s) + then have "\q'' \. (q', \, q'') \ transition_relation" + using sinks_def2[of "q'"] + by auto + with assms(1) show ?case + by (auto elim: path_with_word.cases) +next + case (path_with_word_step s' ss w s l) + then show ?case + by metis +qed + +lemma count_transitions_of'_tails: + assumes "(p, \', q'_add) \ (p1, \, q')" + shows "count (transitions_of' (p, \' # w, p # q'_add # ss_rest, q)) (p1, \, q') = + count (transitions_of' (q'_add, w, q'_add # ss_rest, q)) (p1, \, q')" + using assms by (cases w) auto + +lemma avoid_count_zero: + assumes "(p, w, ss, q) \ trans_star_states" + assumes "(p1, \, q') \ transition_relation" + shows "count (transitions_of' (p, w, ss, q)) (p1, \, q') = 0" + using assms +proof(induction arbitrary: p rule: trans_star_states.induct) + case (trans_star_states_refl p) + then show ?case + by auto +next + case (trans_star_states_step p \ q' w ss q) + show ?case + by (metis trans_star_states_step trans_star_states.cases assms(2) + count_transitions_of'_tails transitions_of'.simps) +qed + +lemma transition_list_append: + assumes "(ss,w) \ path_with_word" + assumes "(ss',w') \ path_with_word" + assumes "last ss = hd ss'" + shows "transition_list ((ss,w) @\ (ss',w')) = transition_list (ss,w) @ transition_list (ss',w')" + using assms +proof (induction rule: path_with_word.induct) + case (path_with_word_refl s) + then have "transition_list (hd ss' # tl ss', w') = transition_list (ss', w')" + by (metis LTS.path_with_word_not_empty list.exhaust_sel) + then show ?case + using path_with_word_refl by auto +next + case (path_with_word_step s' ss w s l) + then show ?case + by auto +qed + +lemma split_path_with_word_beginning'': + assumes "(SS,WW) \ path_with_word" + assumes "SS = (ss @ ss')" + assumes "length ss = Suc (length w)" + assumes "WW = w @ w'" + shows "(ss,w) \ path_with_word" + using assms +proof (induction arbitrary: ss ss' w w' rule: path_with_word.induct) + case (path_with_word_refl s) + then show ?case + by (metis append.right_neutral append_is_Nil_conv list.sel(3) list.size(3) nat.discI + path_with_word.path_with_word_refl tl_append2) +next + case (path_with_word_step s'a ssa wa s l) + then show ?case + proof (cases "w") + case Nil + then show ?thesis + using path_with_word_step by (metis LTS.path_with_word.simps length_0_conv length_Suc_conv) + next + case (Cons) + have "(s'a # ssa, wa) \ LTS.path_with_word transition_relation" + by (simp add: "path_with_word_step.hyps"(1)) + moreover + have "s'a # ssa = tl ss @ ss'" + by (metis "path_with_word_step.prems"(1,2) Zero_not_Suc + length_0_conv list.sel(3) tl_append2) + moreover + have "length (tl ss) = Suc (length (tl w))" + using "path_with_word_step.prems" Cons by auto + moreover + have "wa = tl w @ w'" + by (metis path_with_word_step(5,6) calculation(3) length_Suc_conv list.sel(3) list.size(3) + nat.simps(3) tl_append2) + ultimately + have "(tl ss, tl w) \ LTS.path_with_word transition_relation" + using path_with_word_step(3)[of "tl ss" ss' "tl w" w'] by auto + then show ?thesis + using path_with_word_step + by (auto simp: Cons_eq_append_conv intro: path_with_word.path_with_word_step) + qed +qed + +lemma split_path_with_word_end': + assumes "(SS,WW) \ path_with_word" + assumes "SS = (ss @ ss')" + assumes "length ss' = Suc (length w')" + assumes "WW = w @ w'" + shows "(ss',w') \ path_with_word" + using assms(1) assms +proof (induction arbitrary: ss ss' w w' rule: path_with_word.induct) + case (path_with_word_refl s) + then show ?case + by (metis Nil_is_append_conv Zero_not_Suc append_Nil list.sel(3) list.size(3) tl_append2) +next + case (path_with_word_step s' ssa wa s l) + show ?case + proof (cases "ss") + case Nil + then show ?thesis + using path_with_word_step(4,5,6,7) path_with_word_length + by (auto simp: Cons_eq_append_conv) + next + case (Cons x xs) + have "(s' # ssa, wa) \ LTS.path_with_word transition_relation" + using "path_with_word_step.hyps"(1) by blast + moreover + have "s' # ssa = tl ss @ ss'" + using path_with_word_step(5) using local.Cons by auto + moreover + have "length ss' = Suc (length w')" + using "path_with_word_step.prems"(3) by blast + moreover + have "wa = tl w @ w'" + proof (cases "wa = []") + assume "wa \[]" + then show ?thesis + using path_with_word_step(4-7) Cons path_with_word_length + by (fastforce simp: Cons_eq_append_conv) + next + assume wa_empty: "wa = []" + have "tl ss @ ss' \ []" + using calculation(2) by force + then have "(butlast (tl ss @ ss') @ [last (s' # ssa)], []) = (s' # ssa, wa)" + using wa_empty by (simp add: calculation(2)) + then have "(butlast (tl ss @ ss') @ [last (s' # ssa)], []) \ LTS.path_with_word transition_relation" + using "path_with_word_step"(1) by metis + then have "length (butlast (tl ss @ ss')) = length ([]::'v list)" + using LTS.path_with_word_lengths by (metis list.size(3)) + then have "w' = []" + by (simp add: calculation(3)) + then show ?thesis + using "path_with_word_step.prems"(4) by force + qed + ultimately + show ?thesis + using path_with_word_step(3)[of "tl ss" ss' w' "tl w"] by auto + qed +qed + +lemma split_path_with_word_end: + assumes "(ss @ ss',w @ w') \ path_with_word" + assumes "length ss' = Suc (length w')" + shows "(ss',w') \ path_with_word" + using split_path_with_word_end' assms by blast + +lemma split_path_with_word_beginning': + assumes "(ss @ ss',w @ w') \ path_with_word" + assumes "length ss = Suc (length w)" + shows "(ss,w) \ path_with_word" + using assms split_path_with_word_beginning'' by blast + +lemma split_path_with_word_beginning: + assumes "(ss, w) @\ (ss', w') \ path_with_word" + assumes "length ss = Suc (length w)" + shows "(ss,w) \ path_with_word" + using assms split_path_with_word_beginning'' by (metis append_path_with_word.simps) + +lemma path_with_word_remove_last': + assumes "(SS, W) \ path_with_word" + assumes "SS = ss @ [s, s']" + assumes "W = w @ [l]" + shows "(ss @ [s], w) \ path_with_word" + using assms +proof (induction arbitrary: ss w rule: path_with_word_induct_reverse) + case (path_with_word_refl s) + then show ?case + by auto +next + case (path_with_word_step_rev ss s w l s') + then show ?case + by auto +qed + +lemma path_with_word_remove_last: + assumes "(ss @ [s, s'], w @ [l]) \ path_with_word" + shows "(ss @ [s], w) \ path_with_word" + using path_with_word_remove_last' assms by auto + +lemma transition_list_append_edge: + assumes "(ss @ [s, s'], w @ [l]) \ path_with_word" + shows "transition_list (ss @ [s, s'], w @ [l]) = transition_list (ss @ [s], w) @ [(s, l, s')]" +proof - + have "(ss @ [s], w) \ path_with_word" + using assms path_with_word_remove_last by auto + moreover + have "([s, s'], [l]) \ path_with_word" + using assms length_Cons list.size(3) by (metis split_path_with_word_end') + moreover + have "last (ss @ [s]) = hd [s, s']" + by auto + ultimately + show ?thesis + using transition_list_append[of "ss @ [s]" w "[s, s']" "[l]"] by auto +qed + +end + + +subsection \More LTS lemmas\ + +lemma hd_transition_list_append_path_with_word: + assumes "hd (transition_list (ss, w)) = (p1, \, q1)" + assumes "transition_list (ss, w) \ []" + shows "([p1, q1], [\]) @\ (tl ss, tl w) = (ss, w)" +proof - + have "p1 # q1 # tl (tl ss) = ss \ \ # tl w = w" + proof (cases ss) + case Nil + note Nil_outer = Nil + show ?thesis + proof (cases w) + case Nil + then show ?thesis + using assms Nil_outer by auto + next + case (Cons a list) + then show ?thesis + using assms Nil_outer by auto + qed + next + case (Cons a list) + note Cons_outer = Cons + show ?thesis + proof (cases w) + case Nil + then show ?thesis + using assms Cons_outer using list.collapse by (metis transition_list.simps(2,4)) + next + case (Cons aa llist) + have "p1 = a" + using assms Cons Cons_outer + by (metis Pair_inject list.exhaust list.sel(1) transition_list.simps(1,2)) + moreover + have "q1 # tl list = list" + using assms Cons Cons_outer + by (cases list) auto + moreover + have "\ = aa" + by (metis Cons_outer Pair_inject assms(1) calculation(2) list.sel(1) local.Cons + transition_list.simps(1)) + ultimately + show ?thesis + using assms Cons_outer Cons by auto + qed + qed + then show ?thesis + by auto +qed + +lemma counting: + "count (transitions_of' ((hdss1,ww1,ss1,lastss1))) (s1, \, s2) = + count (transitions_of ((ss1,ww1))) (s1, \, s2)" + by force + +lemma count_append_path_with_word_\: + assumes "length ss1 = Suc (length ww1)" + assumes "ss2 \ []" + shows "count (transitions_of (((ss1,ww1),\') @\<^sup>\ (ss2,ww2))) (s1, \, s2) = + count (transitions_of (ss1,ww1)) (s1, \, s2) + + (if s1 = last ss1 \ s2 = hd ss2 \ \ = \' then 1 else 0) + + count (transitions_of (ss2,ww2)) (s1, \, s2)" +using assms proof (induction ww1 arbitrary: ss1) + case Nil + note Nil_outer = Nil + obtain s where s_p: "ss1 = [s]" + by (metis Suc_length_conv length_0_conv local.Nil(1)) + then show ?case + proof (cases ss2) + case Nil + then show ?thesis + using assms by blast + next + case (Cons s2' ss2') + then show ?thesis + proof (cases "s1 = s2'") + case True + then show ?thesis + by (simp add: local.Cons s_p) + next + case False + then show ?thesis + using s_p local.Cons by fastforce + qed + qed +next + case (Cons w ww11) + obtain s2' ss2' where s2'_ss2'_p: "ss2 = s2' # ss2'" + by (meson assms list.exhaust) + obtain s1' ss1' where s1'_ss1'_p: "ss1 = s1' # ss1'" + by (meson Cons.prems(1) length_Suc_conv) + show ?case + using Cons(1)[of "ss1'"] Cons(2-) s2'_ss2'_p s1'_ss1'_p + by (auto simp: length_Suc_conv) +qed + +lemma count_append_path_with_word: + assumes "length ss1 = Suc (length ww1)" + assumes "ss2 \ []" + assumes "last ss1 = hd ss2" + shows "count (transitions_of (((ss1, ww1)) @\ (ss2, ww2))) (s1, \, s2) = + count (transitions_of (ss1, ww1)) (s1, \, s2) + + count (transitions_of (ss2, ww2)) (s1, \, s2)" +using assms proof (induction ww1 arbitrary: ss1) + case Nil + note Nil_outer = Nil + obtain s where s_p: "ss1 = [s]" + by (metis Suc_length_conv length_0_conv local.Nil(1)) + then show ?case + proof (cases ss2) + case Nil + then show ?thesis + using assms by blast + next + case (Cons s2' ss2') + then show ?thesis + proof (cases "s1 = s2'") + case True + then show ?thesis + using local.Cons s_p + using Nil_outer(3) by auto + next + case False + then show ?thesis + using s_p local.Cons + using Nil_outer(3) by fastforce + qed + qed +next + case (Cons w ww11) + show ?case + using Cons by (fastforce simp: length_Suc_conv split: if_splits) +qed + +lemma count_append_trans_star_states_\_length: + assumes "length (ss1) = Suc (length (ww1))" + assumes "ss2 \ []" + shows "count (transitions_of' (((hdss1,ww1,ss1,lastss1),\') @@\<^sup>\ (hdss2,ww2,ss2,lastss2))) (s1, \, s2) = + count (transitions_of' (hdss1,ww1,ss1,lastss1)) (s1, \, s2) + + (if s1 = last ss1 \ s2 = hd ss2 \ \ = \' then 1 else 0) + + count (transitions_of' (hdss2,ww2,ss2,lastss2)) (s1, \, s2)" + using assms count_append_path_with_word_\ by force + +lemma count_append_trans_star_states_\: + assumes "(hdss1,ww1,ss1,lastss1) \ LTS.trans_star_states A" + assumes "(hdss2,ww2,ss2,lastss2) \ LTS.trans_star_states A" + shows "count (transitions_of' (((hdss1,ww1,ss1,lastss1),\') @@\<^sup>\ (hdss2,ww2,ss2,lastss2))) (s1, \, s2) = + count (transitions_of' (hdss1,ww1,ss1,lastss1)) (s1, \, s2) + + (if s1 = last ss1 \ s2 = hd ss2 \ \ = \' then 1 else 0) + + count (transitions_of' (hdss2,ww2,ss2,lastss2)) (s1, \, s2)" +proof - + have "length (ss1) = Suc (length (ww1))" + by (meson LTS.trans_star_states_length assms(1)) + moreover + have "ss2 \ []" + by (metis LTS.trans_star_states.simps assms(2) list.discI) + ultimately + show ?thesis + using count_append_trans_star_states_\_length by metis +qed + +lemma count_append_trans_star_states_length: + assumes "length (ss1) = Suc (length (ww1))" + assumes "ss2 \ []" + assumes "last ss1 = hd ss2" + shows "count (transitions_of' (((hdss1,ww1,ss1,lastss1)) @@\ (hdss2,ww2,ss2,lastss2))) (s1, \, s2) = + count (transitions_of' (hdss1,ww1,ss1,lastss1)) (s1, \, s2) + + count (transitions_of' (hdss2,ww2,ss2,lastss2)) (s1, \, s2)" + using count_append_path_with_word[OF assms(1) assms(2) assms(3), of ww2 s1 \ s2] by auto + +lemma count_append_trans_star_states: + assumes "(hdss1,ww1,ss1,lastss1) \ LTS.trans_star_states A" + assumes "(lastss1,ww2,ss2,lastss2) \ LTS.trans_star_states A" + shows "count (transitions_of' (((hdss1,ww1,ss1,lastss1)) @@\ (lastss1,ww2,ss2,lastss2))) (s1, \, s2) = + count (transitions_of' (hdss1,ww1,ss1,lastss1)) (s1, \, s2) + + count (transitions_of' (lastss1,ww2,ss2,lastss2)) (s1, \, s2)" +proof - + have "length (ss1) = Suc (length (ww1))" + by (meson LTS.trans_star_states_length assms(1)) + moreover + have "last ss1 = hd ss2" + by (metis LTS.trans_star_states_hd LTS.trans_star_states_last assms(1) assms(2)) + moreover + have "ss2 \ []" + by (metis LTS.trans_star_states_length Zero_not_Suc assms(2) list.size(3)) + ultimately + show ?thesis + using count_append_trans_star_states_length assms by auto +qed + + +context fixes \ :: "('state, 'label) transition set" begin +fun reach where + "reach p [] = {p}" +| "reach p (\#w) = + (\q' \ (\(p',\',q') \ \. if p' = p \ \' = \ then {q'} else {}). + reach q' w)" +end +lemma trans_star_imp_exec: "(p,w,q) \ LTS.trans_star \ \ q \ reach \ p w" + by (induct p w q rule: LTS.trans_star.induct[of _ _ _ \, consumes 1]) force+ +lemma reach_imp: "q \ reach \ p w \ (p,w,q) \ LTS.trans_star \" + by (induct p w rule: reach.induct) + (auto intro!: LTS.trans_star_refl[of _ \] LTS.trans_star_step[of _ _ _ \] split: if_splits) +lemma trans_star_code[code_unfold]: "(p,w,q) \ LTS.trans_star \ \ q \ reach \ p w" + by (meson reach_imp trans_star_imp_exec) + +lemma subset_srcs_code[code_unfold]: + "X \ LTS.srcs A \ (\q \ X. q \ snd ` snd ` A)" + by (auto simp add: LTS.srcs_def image_iff) + + +lemma LTS_trans_star_mono: + "mono LTS.trans_star" +proof (rule, rule) + fix pwq :: "'a \ 'b list \ 'a" + fix ts ts' :: "('a, 'b) transition set" + assume sub: "ts \ ts'" + assume pwq_ts: "pwq \ LTS.trans_star ts" + then obtain p w q where pwq_p: "pwq = (p, w, q)" + using prod_cases3 by blast + then have "(p, w, q) \ LTS.trans_star ts" + using pwq_ts by auto + then have "(p, w, q) \ LTS.trans_star ts'" + proof(induction w arbitrary: p) + case Nil + then show ?case + by (metis LTS.trans_star.trans_star_refl LTS.trans_star_empty) + next + case (Cons \ w) + then show ?case + by (meson LTS.trans_star.simps LTS.trans_star_cons sub subsetD) + qed + then show "pwq \ LTS.trans_star ts'" + unfolding pwq_p . +qed + +lemma count_next_0: + assumes "count (transitions_of (s # s' # ss, l # w)) (p1, \, q') = 0" + shows "count (transitions_of (s' # ss, w)) (p1, \, q') = 0" + using assms by (cases "s = p1 \ l = \ \ s' = q'") auto + +lemma count_next_hd: + assumes "count (transitions_of (s # s' # ss, l # w)) (p1, \, q') = 0" + shows "(s, l, s') \ (p1, \, q')" + using assms by auto + +lemma count_empty_zero: "count (transitions_of' (p, [], [p_add], p_add)) (p1, \, q') = 0" + by simp + +lemma count_zero_remove_path_with_word: + assumes "(ss, w) \ LTS.path_with_word Ai" + assumes "0 = count (transitions_of (ss, w)) (p1, \, q')" + assumes "Ai = Aiminus1 \ {(p1, \, q')}" + shows "(ss, w) \ LTS.path_with_word Aiminus1" + using assms +proof (induction rule: LTS.path_with_word.induct[OF assms(1)]) + case (1 s) + then show ?case + by (simp add: LTS.path_with_word.path_with_word_refl) +next + case (2 s' ss w s l) + from 2(5) have "0 = count (transitions_of (s' # ss, w)) (p1, \, q')" + using count_next_0 by auto + then have s'_ss_w_Aiminus1: "(s' # ss, w) \ LTS.path_with_word Aiminus1" + using 2 by auto + have "(s, l, s') \ Aiminus1" + using 2(2,5) assms(3) by force + then show ?case + using s'_ss_w_Aiminus1 by (simp add: LTS.path_with_word.path_with_word_step) +qed + +lemma count_zero_remove_path_with_word_trans_star_states: + assumes "(p, w, ss ,q) \ LTS.trans_star_states Ai" + assumes "0 = count (transitions_of' (p, w, ss, q)) (p1, \, q')" + assumes "Ai = Aiminus1 \ {(p1, \, q')}" + shows "(p, w, ss, q) \ LTS.trans_star_states Aiminus1" + using assms +proof (induction arbitrary: p rule: LTS.trans_star_states.induct[OF assms(1)]) + case (1 p) + then show ?case + by (metis LTS.trans_star_states.simps list.distinct(1)) +next + case (2 p' \' q'' w ss q) + have p_is_p': "p' = p" + by (meson "2.prems"(1) LTS.trans_star_states.cases list.inject) + { + assume len: "length ss > 0" + have not_found: "(p, \', hd ss) \ (p1, \, q')" + using LTS.trans_star_states.cases count_next_hd list.sel(1) transitions_of'.simps + using 2(4) 2(5) by (metis len hd_Cons_tl length_greater_0_conv) + have hdAI: "(p, \', hd ss) \ Ai" + by (metis "2.hyps"(1) "2.hyps"(2) LTS.trans_star_states.cases list.sel(1) p_is_p') + have t_Aiminus1: "(p, \', hd ss) \ Aiminus1" + using 2 hdAI not_found by force + have "(p, \' # w, p' # ss, q) \ LTS.trans_star_states (Aiminus1 \ {(p1, \, q')})" + using "2.prems"(1) assms(3) by fastforce + have ss_hd_tl: "hd ss # tl ss = ss" + using len hd_Cons_tl by blast + moreover + have "(hd ss, w, ss, q) \ LTS.trans_star_states Ai" + using ss_hd_tl "2.hyps"(2) using LTS.trans_star_states.cases + by (metis list.sel(1)) + ultimately have "(hd ss, w, ss, q) \ LTS.trans_star_states Aiminus1" + using ss_hd_tl using "2.IH" "2.prems"(2) not_found assms(3) p_is_p' + LTS.count_transitions_of'_tails by (metis) + from this t_Aiminus1 have ?case + using LTS.trans_star_states.intros(2)[of p \' "hd ss" Aiminus1 w ss q] using p_is_p' by auto + } + moreover + { + assume "length ss = 0" + then have ?case + using "2.hyps"(2) LTS.trans_star_states.cases by force + } + ultimately show ?case + by auto +qed + +lemma count_zero_remove_trans_star_states_trans_star: + assumes "(p, w, ss ,q) \ LTS.trans_star_states Ai" + assumes "0 = count (transitions_of' (p, w, ss, q)) (p1, \, q')" + assumes "Ai = Aiminus1 \ {(p1, \, q')}" + shows "(p, w, q) \ LTS.trans_star Aiminus1" + using assms count_zero_remove_path_with_word_trans_star_states by (metis LTS.trans_star_states_trans_star) + +lemma split_at_first_t: + assumes "(p, w, ss, q) \ LTS.trans_star_states Ai" + assumes "Suc j' = count (transitions_of' (p, w, ss, q)) (p1, \, q')" + assumes "(p1, \, q') \ Aiminus1" + assumes "Ai = Aiminus1 \ {(p1, \, q')}" + shows "\u v u_ss v_ss. + ss = u_ss @ v_ss \ + w = u @ [\] @ v \ + (p, u, u_ss, p1) \ LTS.trans_star_states Aiminus1 \ + (p1, [\], q') \ LTS.trans_star Ai \ + (q', v, v_ss, q) \ LTS.trans_star_states Ai \ + (p, w, ss, q) = ((p, u, u_ss, p1),\) @@\<^sup>\ (q', v, v_ss,q)" + using assms +proof(induction arbitrary: p rule: LTS.trans_star_states.induct[OF assms(1)]) + case (1 p_add p) + from 1(2) have "False" + using count_empty_zero by auto + then show ?case + by auto +next + case (2 p_add \' q'_add w ss q p) + then have p_add_p: "p_add = p" + by (meson LTS.trans_star_states.cases list.inject) + from p_add_p have p_Ai: "(p, \', q'_add) \ Ai" + using 2(1) by auto + from p_add_p have p_\'_w_ss_Ai: "(p, \' # w, p # ss, q) \ LTS.trans_star_states Ai" + using 2(4) by auto + from p_add_p have count_p_\'_w_ss: "Suc j' = count (transitions_of' (p, \' # w, p # ss, q)) (p1, \, q')" + using 2(5) by auto + show ?case + proof(cases "(p, \', q'_add) = (p1, \, q')") + case True + define u :: "'b list" where "u = []" + define u_ss :: "'a list" where "u_ss = [p]" + define v where "v = w" + define v_ss where "v_ss = ss" + have "(p, u, u_ss, p1) \ LTS.trans_star_states Aiminus1" + unfolding u_def u_ss_def using LTS.trans_star_states.intros + using True by fastforce + have "(p1, [\], q') \ LTS.trans_star Ai" + using p_Ai by (metis LTS.trans_star.trans_star_refl LTS.trans_star.trans_star_step True) + have "(q', v, v_ss, q) \ LTS.trans_star_states Ai" + using 2(2) True v_def v_ss_def by blast + show ?thesis + using Pair_inject True \(p, u, u_ss, p1) \ LTS.trans_star_states Aiminus1\ + \(p1, [\], q') \ LTS.trans_star Ai\ \(q', v, v_ss, q) \ LTS.trans_star_states Ai\ + append_Cons p_add_p self_append_conv2 u_def u_ss_def v_def v_ss_def + by (metis (no_types) append_trans_star_states_\.simps) + next + case False + have "hd ss = q'_add" + by (metis LTS.trans_star_states.cases 2(2) list.sel(1)) + from this False have g: "Suc j' = count (transitions_of' (q'_add, w, ss, q)) (p1, \, q')" + using count_p_\'_w_ss by (cases ss) auto + have "\u_ih v_ih u_ss_ih v_ss_ih. + ss = u_ss_ih @ v_ss_ih \ + w = u_ih @ [\] @ v_ih \ + (q'_add, u_ih, u_ss_ih, p1) \ LTS.trans_star_states Aiminus1 \ + (p1, [\], q') \ LTS.trans_star Ai \ + (q', v_ih, v_ss_ih, q) \ LTS.trans_star_states Ai" + using 2(3)[of q'_add, OF 2(2) g 2(6) 2(7)] by auto + then obtain u_ih v_ih u_ss_ih v_ss_ih where splitting_p: + "ss = u_ss_ih @ v_ss_ih" + "w = u_ih @ [\] @ v_ih" + "(q'_add, u_ih, u_ss_ih, p1) \ LTS.trans_star_states Aiminus1" + "(p1, [\], q') \ LTS.trans_star Ai" + "(q', v_ih, v_ss_ih, q) \ LTS.trans_star_states Ai" + by metis + define v where "v = v_ih" + define v_ss where "v_ss = v_ss_ih" + define u where "u = \' # u_ih" + define u_ss where "u_ss = p # u_ss_ih" + have "p_add # ss = u_ss @ v_ss" + by (simp add: p_add_p splitting_p(1) u_ss_def v_ss_def) + have "\' # w = u @ [\] @ v" + using splitting_p(2) u_def v_def by auto + have "(p, u, u_ss, p1) \ LTS.trans_star_states Aiminus1" + using False LTS.trans_star_states.trans_star_states_step 2(7) p_Ai splitting_p(3) u_def + u_ss_def by fastforce + have "(p1, [\], q') \ LTS.trans_star Ai" + by (simp add: splitting_p(4)) + have "(q', v, v_ss, q) \ LTS.trans_star_states Ai" + by (simp add: splitting_p(5) v_def v_ss_def) + show ?thesis + using \(p, u, u_ss, p1) \ LTS.trans_star_states Aiminus1\ + \(q', v, v_ss, q) \ LTS.trans_star_states Ai\ \\' # w = u @ [\] @ v\ + \p_add # ss = u_ss @ v_ss\ splitting_p(4) + by auto + qed +qed + +lemma trans_star_states_mono: + assumes "(p, w, ss, q) \ LTS.trans_star_states A1" + assumes "A1 \ A2" + shows "(p, w, ss, q) \ LTS.trans_star_states A2" + using assms +proof (induction rule: LTS.trans_star_states.induct[OF assms(1)]) + case (1 p) + then show ?case + by (simp add: LTS.trans_star_states.trans_star_states_refl) +next + case (2 p \ q' w ss q) + then show ?case + by (meson LTS.trans_star_states.trans_star_states_step in_mono) +qed + +lemma count_combine_trans_star_states_append: + assumes "ss = u_ss @ v_ss \ w = u @ [\] @ v" + assumes "t = (p1, \, q')" + assumes "(p, u, u_ss, p1) \ LTS.trans_star_states A" + assumes "(q', v, v_ss, q) \ LTS.trans_star_states B" + shows "count (transitions_of' (p, w, ss, q)) t = + count (transitions_of' (p, u, u_ss, p1)) t + + 1 + + count (transitions_of' (q', v, v_ss, q)) t" +proof - + have v_ss_non_empt: "v_ss \ []" + using LTS.trans_star_states.cases assms by force + + have u_ss_l: "length u_ss = Suc (length u)" + using assms LTS.trans_star_states_length by metis + + have p1_u_ss: "p1 = last u_ss" + using assms LTS.trans_star_states_last by metis + + have q'_v_ss: "q' = hd v_ss" + using assms LTS.trans_star_states_hd by metis + + have one: "(if p1 = last u_ss \ q' = hd v_ss then 1 else 0) = 1" + using p1_u_ss q'_v_ss by auto + + from count_append_trans_star_states_\_length[of u_ss u v_ss p q \ q' v q p1 ] show ?thesis + using assms(1) assms(2) assms(3) by (auto simp add: assms(3) one u_ss_l v_ss_non_empt) +qed + +lemma count_combine_trans_star_states: + assumes "t = (p1, \, q')" + assumes "(p, u, u_ss, p1) \ LTS.trans_star_states A" + assumes "(q', v, v_ss, q) \ LTS.trans_star_states B" + shows "count (transitions_of' (((p, u, u_ss, p1),\) @@\<^sup>\ (q', v, v_ss, q))) t = + count (transitions_of' (p, u, u_ss, p1)) t + 1 + count (transitions_of' (q', v, v_ss, q)) t" + by (metis append_trans_star_states_\.simps assms count_combine_trans_star_states_append) + +lemma transition_list_reversed_simp: + assumes "length ss = length w" + shows "transition_list (ss @ [s, s'], w @ [l]) = (transition_list (ss@[s],w)) @ [(s,l,s')]" + using assms +proof (induction ss arbitrary: w) + case Nil + then show ?case + by auto +next + case (Cons a ss) + define w' where "w' = tl w" + define l' where "l' = hd w" + have w_split: "l' # w' = w" + by (metis Cons.prems l'_def length_0_conv list.distinct(1) list.exhaust_sel w'_def) + then have "length ss = length w'" + using Cons.prems by force + then have "transition_list (ss @ [s, s'], w' @ [l]) = transition_list (ss @ [s], w') @ [(s, l, s')]" + using Cons(1)[of w'] by auto + then have "transition_list (a # ss @ [s, s'], l' # w' @ [l]) = transition_list (a # ss @ [s], l' # w') @ [(s, l, s')]" + by (cases ss) auto + then show ?case + using w_split by auto +qed + +lemma LTS_trans_star_mono': + "mono LTS.trans_star_states" + by (auto simp: mono_def trans_star_states_mono) + +lemma path_with_word_mono': + assumes "(ss, w) \ LTS.path_with_word A1" + assumes "A1 \ A2" + shows "(ss, w) \ LTS.path_with_word A2" + by (meson LTS.trans_star_states_path_with_word LTS.path_with_word_trans_star_states assms(1,2) + trans_star_states_mono) + +lemma LTS_path_with_word_mono: + "mono LTS.path_with_word" + by (auto simp: mono_def path_with_word_mono') + + +subsection \Reverse transition system\ + +fun rev_edge :: "('n,'v) transition \ ('n,'v) transition" where + "rev_edge (q\<^sub>s,\,q\<^sub>o) = (q\<^sub>o, \, q\<^sub>s)" + +lemma rev_edge_rev_edge_id[simp]: "rev_edge (rev_edge x) = x" + by (cases x) auto + +fun rev_path_with_word :: "'n list * 'v list \ 'n list * 'v list" where + "rev_path_with_word (es,ls) = (rev es, rev ls)" + +definition rev_edge_list :: "('n,'v) transition list \ ('n,'v) transition list" where + "rev_edge_list ts = rev (map rev_edge ts)" + +context LTS begin + +interpretation rev_LTS: LTS "(rev_edge ` transition_relation)" + . + +lemma rev_path_in_rev_pg: + assumes "(ss, w) \ path_with_word" + shows "(rev ss, rev w) \ rev_LTS.path_with_word" + using assms(1) assms +proof (induction rule: path_with_word_induct_reverse) + case (path_with_word_refl s) + then show ?case + by (simp add: LTS.path_with_word.path_with_word_refl) +next + case (path_with_word_step_rev ss s w l s') + have "(s', l, s) \ rev_edge ` transition_relation" + using path_with_word_step_rev by (simp add: rev_image_eqI) + moreover + have "(rev (ss @ [s]), rev w) \ LTS.path_with_word (rev_edge ` transition_relation)" + using "path_with_word_step_rev.IH" "path_with_word_step_rev.hyps"(1) by blast + then have "(s # rev ss, rev w) \ LTS.path_with_word (rev_edge ` transition_relation)" + by auto + ultimately + have "(s' # s # rev ss, l # rev w) \ LTS.path_with_word (rev_edge ` transition_relation)" + by (simp add: LTS.path_with_word.path_with_word_step) + then show ?case + by auto +qed + +lemma transition_list_rev_edge_list: + assumes "(ss,w) \ path_with_word" + shows "transition_list (rev ss, rev w) = rev_edge_list (transition_list (ss, w))" + using assms(1) assms +proof (induction rule: path_with_word.induct) + case (path_with_word_refl s) + then show ?case + by (simp add: rev_edge_list_def) +next + case (path_with_word_step s' ss w s l) + have "transition_list (rev (s # s' # ss), rev (l # w)) = transition_list (rev ss @ [s', s], rev w @ [l])" + by auto + moreover + have "... = transition_list (rev ss @ [s'], rev w) @ [(s', l, s)]" + using transition_list_reversed_simp[of "rev ss" "rev w" s' s l] + using "path_with_word_step.hyps"(1) LTS.path_with_word_lengths rev_path_in_rev_pg by fastforce + moreover + have "... = rev_edge_list (transition_list (s' # ss, w)) @ [(s', l, s)]" + using path_with_word_step by auto + moreover + have "... = rev_edge_list ((s, l, s') # transition_list (s' # ss, w))" + unfolding rev_edge_list_def by auto + moreover + have "... = rev_edge_list (transition_list (s # s' # ss, l # w))" + by auto + ultimately + show ?case + by metis +qed + +end + + +section \LTS with epsilon\ + + +subsection \LTS functions\ + +context begin + +private abbreviation \ :: "'label option" where + "\ == None" + +definition inters_\ :: "('state, 'label option) transition set \ ('state, 'label option) transition set \ (('state * 'state), 'label option) transition set" where + "inters_\ ts1 ts2 = + {((p1, q1), \, (p2, q2)) | p1 q1 \ p2 q2. (p1, \, p2) \ ts1 \ (q1, \, q2) \ ts2} \ + {((p1, q1), \, (p2, q1)) | p1 p2 q1. (p1, \, p2) \ ts1} \ + {((p1, q1), \, (p1, q2)) | p1 q1 q2. (q1, \, q2) \ ts2}" + +end + + +subsection \LTS with epsilon locale\ + +locale LTS_\ = LTS transition_relation for transition_relation :: "('state, 'label option) transition set" +begin + +abbreviation \ :: "'label option" where + "\ == None" + +inductive_set trans_star_\ :: "('state * 'label list * 'state) set" where + trans_star_\_refl[iff]: "(p, [], p) \ trans_star_\" +| trans_star_\_step_\: "(p, Some \, q') \ transition_relation \ (q',w,q) \ trans_star_\ + \ (p, \#w, q) \ trans_star_\" +| trans_star_\_step_\: "(p, \, q') \ transition_relation \ (q',w,q) \ trans_star_\ + \ (p, w, q) \ trans_star_\" + +inductive_cases trans_star_\_empty [elim]: "(p, [], q) \ trans_star_\" +inductive_cases trans_star_cons_\: "(p, \#w, q) \ trans_star" + +definition remove_\ :: "'label option list \ 'label list" where + "remove_\ w = map the (removeAll \ w)" + +definition \_exp :: "'label option list \ 'label list \ bool" where + "\_exp w' w \ map the (removeAll \ w') = w" + +lemma trans_star_trans_star_\: + assumes "(p, w, q) \ trans_star" + shows "(p, map the (removeAll \ w), q) \ trans_star_\" + using assms +proof (induction rule: trans_star.induct) + case (trans_star_refl p) + then show ?case + by simp +next + case (trans_star_step p \ q' w q) + show ?case + proof (cases \) + case None + then show ?thesis + using trans_star_step by (simp add: trans_star_\.trans_star_\_step_\) + next + case (Some \') + then show ?thesis + using trans_star_step by (simp add: trans_star_\.trans_star_\_step_\) + qed +qed + +lemma trans_star_\_\_exp_trans_star: + assumes "(p, w, q) \ trans_star_\" + shows "\w'. \_exp w' w \ (p, w', q) \ trans_star" + using assms +proof (induction rule: trans_star_\.induct) + case (trans_star_\_refl p) + then show ?case + by (metis LTS.trans_star.trans_star_refl \_exp_def list.simps(8) removeAll.simps(1)) +next + case (trans_star_\_step_\ p \ q' w q) + obtain w\ :: "'label option list" where + f1: "(q', w\, q) \ trans_star \ \_exp w\ w" + using trans_star_\_step_\.IH by blast + then have "\_exp (Some \ # w\) (\ # w)" + by (simp add: LTS_\.\_exp_def) + then show ?case + using f1 by (meson trans_star.simps trans_star_\_step_\.hyps(1)) +next + case (trans_star_\_step_\ p q' w q) + then show ?case + by (metis trans_starp.trans_star_step trans_starp_trans_star_eq \_exp_def removeAll.simps(2)) +qed + +lemma trans_star_\_iff_\_exp_trans_star: + "(p, w, q) \ trans_star_\ \ (\w'. \_exp w' w \ (p, w', q) \ trans_star)" +proof + assume "(p, w, q) \ trans_star_\" + then show "\w'. \_exp w' w \ (p, w', q) \ trans_star" + using trans_star_\_\_exp_trans_star trans_star_trans_star_\ by auto +next + assume "\w'. \_exp w' w \ (p, w', q) \ trans_star" + then show "(p, w, q) \ trans_star_\" + using trans_star_\_\_exp_trans_star trans_star_trans_star_\ \_exp_def by auto +qed + +lemma \_exp_split': + assumes "\_exp u_\ (\1 # u1)" + shows "\\1_\ u1_\. \_exp \1_\ [\1] \ \_exp u1_\ u1 \ u_\ = \1_\ @ u1_\" + using assms +proof (induction u_\ arbitrary: u1 \1) + case Nil + then show ?case + by (metis LTS_\.\_exp_def list.distinct(1) list.simps(8) removeAll.simps(1)) +next + case (Cons a u_\) + then show ?case + proof (induction a) + case None + then have "\_exp u_\ (\1 # u1)" + using \_exp_def by force + then have "\\1_\ u1_\. \_exp \1_\ [\1] \ \_exp u1_\ u1 \ u_\ = \1_\ @ u1_\" + using None(1) by auto + then show ?case + by (metis LTS_\.\_exp_def append_Cons removeAll.simps(2)) + next + case (Some \1') + have "\1' = \1" + using Some.prems(2) \_exp_def by auto + have "\_exp u_\ u1" + using Some.prems(2) \_exp_def by force + show ?case + proof (cases u1) + case Nil + then show ?thesis + by (metis Some.prems(2) \_exp_def append_Nil2 list.simps(8) removeAll.simps(1)) + next + case (Cons a list) + then show ?thesis + using LTS_\.\_exp_def \\_exp u_\ u1\ \\1' = \1\ by force + qed + qed +qed + +lemma remove_\_append_dist: + "remove_\ (w @ w') = remove_\ w @ remove_\ w'" +proof (induction w) + case Nil + then show ?case + by (simp add: LTS_\.remove_\_def) +next + case (Cons a w) + then show ?case + by (simp add: LTS_\.remove_\_def) +qed + +lemma remove_\_Cons_tl: + assumes "remove_\ w = remove_\ (Some \' # tl w)" + shows "\' # remove_\ (tl w) = remove_\ w" + using assms unfolding remove_\_def by auto + + +lemma trans_star_states_trans_star_\: + assumes "(p, w, ss, q) \ trans_star_states" + shows "(p, LTS_\.remove_\ w, q) \ trans_star_\" + by (metis LTS_\.trans_star_trans_star_\ assms remove_\_def trans_star_states_trans_star) + +lemma no_edge_to_source_\: + assumes "(p, [\], qq) \ trans_star_\" + shows "qq \ srcs" +proof - + have "\w. LTS_\.\_exp w [\] \ (p, w, qq) \ trans_star \ w \ []" + by (metis (no_types) LTS_\.\_exp_def LTS_\.\_exp_split' LTS_\.trans_star_\_iff_\_exp_trans_star + append_Cons append_Nil assms(1) list.distinct(1) list.exhaust) + then obtain w where "LTS_\.\_exp w [\] \ (p, w, qq) \ trans_star \ w \ []" + by blast + then show ?thesis + using LTS.no_end_in_source[of p w qq] assms by auto +qed + +lemma trans_star_not_to_source_\: + assumes "(p''', w, q) \ trans_star_\" + assumes "p''' \ q" + assumes "q' \ srcs" + shows "q' \ q" + using assms +proof (induction rule: trans_star_\.induct) + case (trans_star_\_refl p) + then show ?case + by blast +next + case (trans_star_\_step_\ p \ q' w q) + then show ?case + using srcs_def2 by metis +next + case (trans_star_\_step_\ p q' w q) + then show ?case + using srcs_def2 by metis +qed + +lemma append_edge_edge_trans_star_\: + assumes "(p1, Some \', p2) \ transition_relation" + assumes "(p2, Some \'', q1) \ transition_relation" + assumes "(q1, u1, q) \ trans_star_\" + shows "(p1, [\', \''] @ u1, q) \ trans_star_\" + using assms by (metis trans_star_\_step_\ append_Cons append_Nil) + +inductive_set trans_star_states_\ :: "('state * 'label list * 'state list * 'state) set" where + trans_star_states_\_refl[iff]: + "(p,[],[p],p) \ trans_star_states_\" +| trans_star_states_\_step_\: + "(p,Some \,q') \ transition_relation \ + (q',w,ss,q) \ trans_star_states_\ \ + (p, \#w, p#ss, q) \ trans_star_states_\" +| trans_star_states_\_step_\: + "(p, \ ,q') \ transition_relation \ + (q',w,ss,q) \ trans_star_states_\ \ +(p, w, p#ss, q) \ trans_star_states_\" + +inductive_set path_with_word_\ :: "('state list * 'label list) set" where + path_with_word_\_refl[iff]: + "([s],[]) \ path_with_word_\" +| path_with_word_\_step_\: + "(s'#ss, w) \ path_with_word_\ \ + (s,Some l,s') \ transition_relation \ + (s#s'#ss,l#w) \ path_with_word_\" +| path_with_word_\_step_\: + "(s'#ss, w) \ path_with_word_\ \ + (s,\,s') \ transition_relation \ + (s#s'#ss,w) \ path_with_word_\" + +lemma \_exp_Some_length: + assumes "\_exp (Some \ # w1') w" + shows "0 < length w" + using assms + by (metis LTS_\.\_exp_def length_greater_0_conv list.map(2) neq_Nil_conv option.simps(3) + removeAll.simps(2)) + +lemma \_exp_Some_hd: + assumes "\_exp (Some \ # w1') w" + shows "hd w = \" + using assms + by (metis LTS_\.\_exp_def list.sel(1) list.simps(9) option.sel option.simps(3) removeAll.simps(2)) + +lemma exp_empty_empty: + assumes "\_exp [] w" + shows "w = []" + using assms by (metis LTS_\.\_exp_def list.simps(8) removeAll.simps(1)) + +end + + +subsection \More LTS lemmas\ + +lemma LTS_\_trans_star_\_mono: + "mono LTS_\.trans_star_\" +proof (rule, rule) + fix pwq :: "'a \ 'b list \ 'a" + fix ts ts' :: "('a, 'b option) transition set" + assume sub: "ts \ ts'" + assume pwq_ts: "pwq \ LTS_\.trans_star_\ ts" + then obtain p w q where pwq_p: "pwq = (p, w, q)" + using prod_cases3 by blast + then have x: "(p, w, q) \ LTS_\.trans_star_\ ts" + using pwq_ts by auto + then have "(\w'. LTS_\.\_exp w' w \ (p, w', q) \ LTS.trans_star ts)" + using LTS_\.trans_star_\_iff_\_exp_trans_star[of p w q ts] by auto + then have "(\w'. LTS_\.\_exp w' w \ (p, w', q) \ LTS.trans_star ts')" + using LTS_trans_star_mono sub + using monoD by blast + then have "(p, w, q) \ LTS_\.trans_star_\ ts'" + using LTS_\.trans_star_\_iff_\_exp_trans_star[of p w q ts'] by auto + then show "pwq \ LTS_\.trans_star_\ ts'" + unfolding pwq_p . +qed + +definition \_edge_of_edge where + "\_edge_of_edge = (\(a, l, b). (a, Some l, b))" + +definition LTS_\_of_LTS where + "LTS_\_of_LTS transition_relation = \_edge_of_edge ` transition_relation" + +end \ No newline at end of file diff --git a/thys/Labeled_Transition_Systems/ROOT b/thys/Labeled_Transition_Systems/ROOT new file mode 100644 --- /dev/null +++ b/thys/Labeled_Transition_Systems/ROOT @@ -0,0 +1,9 @@ +chapter AFP + +session Labeled_Transition_Systems = "Deriving" + + options [timeout = 300] + theories + LTS + document_files + "root.bib" + "root.tex" diff --git a/thys/Labeled_Transition_Systems/document/root.bib b/thys/Labeled_Transition_Systems/document/root.bib new file mode 100644 --- /dev/null +++ b/thys/Labeled_Transition_Systems/document/root.bib @@ -0,0 +1,6 @@ +@inproceedings{graphs, + title={Archive of Graph Formalizations}, + author={Simon Wimmer}, + note={\url{https://github.com/wimmers/archive-of-graph-formalizations}}, + year={2020}, +} diff --git a/thys/Labeled_Transition_Systems/document/root.tex b/thys/Labeled_Transition_Systems/document/root.tex new file mode 100644 --- /dev/null +++ b/thys/Labeled_Transition_Systems/document/root.tex @@ -0,0 +1,54 @@ +\documentclass[10pt,a4paper]{article} +\usepackage[T1]{fontenc} +\usepackage{amssymb} +\usepackage[left=2.25cm,right=2.25cm,top=2.25cm,bottom=2.75cm]{geometry} +\usepackage{graphicx} +\usepackage{isabelle} +\usepackage{isabellesym} +\usepackage[only,bigsqcap]{stmaryrd} +\usepackage{pdfsetup} + +\urlstyle{tt} +\isabellestyle{it} + +\renewcommand{\isacharunderscore}{\_} +\renewcommand{\isachardoublequoteopen}{``} +\renewcommand{\isachardoublequoteclose}{''} + +\begin{document} + +\title{Labeled Transition Systems} +\author{Anders Schlichtkrull, Morten Konggaard Schou, Ji\v{r}\'i Srba and Dmitriy Traytel} +\date{} + +\maketitle + +\begin{abstract} +\noindent +Labeled transition systems are ubiquitous in computer science. They are used e.g.\ for automata and for program graphs in program analysis. +We formalize labeled transition systems with and without epsilon transitions. +The main difference between formalizations of labeled transition systems is in their choice of how to represent the transition system. +In the present formalization the set of nodes is a type, and a labeled transition system is represented as a locale fixing a set +of transitions where each transition is a triple of respectively a start node, a label and an end node. +Wimmer~\cite{graphs} provides an overview of formalizations of graphs and transition systems. + +\end{abstract} + +\tableofcontents + +\newpage + +% sane default for proof documents +\parindent 0pt +\parskip 0.5ex + +\newpage + +% generated text of all theories +\input{session} + +% optional bibliography +\bibliographystyle{alpha} +\bibliography{root} + +\end{document} diff --git a/thys/Pushdown_Systems/Ex.thy b/thys/Pushdown_Systems/Ex.thy new file mode 100644 --- /dev/null +++ b/thys/Pushdown_Systems/Ex.thy @@ -0,0 +1,117 @@ +theory Ex + imports Pushdown_Systems.PDS_Code +begin + +(* Query specific part START *) +abbreviation ctr_locN :: nat where "ctr_locN \ 3" +abbreviation labelN :: nat where "labelN \ 2" +abbreviation stateN :: nat where "stateN \ 3" +typedef ctr_loc = "{0 ..< ctr_locN}" by (auto intro!: exI[of _ 0]) +typedef label = "{0 ..< labelN}" by (auto intro!: exI[of _ 0]) +typedef state = "{0 ..< stateN}" by (auto intro!: exI[of _ 0]) +setup_lifting type_definition_ctr_loc +setup_lifting type_definition_label +setup_lifting type_definition_state + +lift_definition p1 :: ctr_loc is 0 by auto +lift_definition p2 :: ctr_loc is 1 by auto +lift_definition p3 :: ctr_loc is 2 by auto +lift_definition x :: label is 0 by auto +lift_definition y :: label is 1 by auto +lift_definition q1 :: state is 0 by auto +lift_definition q2 :: state is 1 by auto +lift_definition qf :: state is 2 by auto + +(* Define rules of PDS, and the two P-automata *) +definition pds_rules :: "(ctr_loc, label) rule set" where + "pds_rules = { + ((p1, y), (p1, push x y)), + ((p1, x), (p2, swap y)), + ((p2, x), (p3, pop)), + ((p3, y), (p2, swap x))}" +definition initial_automaton :: "((ctr_loc, state, label) PDS.state, label) transition set" where + "initial_automaton = { + ((Init p1, y, Noninit qf)), + ((Init p2, y, Noninit qf)), + ((Init p2, x, Init p2)), + ((Init p3, x, Noninit qf))}" +definition final_automaton :: "((ctr_loc, state, label) PDS.state, label) transition set" where + "final_automaton = { + ((Init p2, y, Noninit q1)), + ((Init p3, x, Noninit q1)), + ((Noninit q1, y, Noninit q2))}" + +definition final_ctr_loc where "final_ctr_loc = {}" +definition final_ctr_loc_st where "final_ctr_loc_st = {q2}" +definition initial_ctr_loc where "initial_ctr_loc = {}" +definition initial_ctr_loc_st where "initial_ctr_loc_st = {qf}" +(* Query specific part END *) + +instantiation ctr_loc :: finite begin +instance by (standard, rule finite_surj[of "{0 ..< ctr_locN}" _ Abs_ctr_loc]) + (simp, metis Rep_ctr_loc Rep_ctr_loc_inverse imageI subsetI) +end +instantiation label :: finite begin +instance by (standard, rule finite_surj[of "{0 ..< labelN}" _ Abs_label]) + (simp, metis Rep_label Rep_label_inverse imageI subsetI) +end +instantiation state :: finite begin +instance by (standard, rule finite_surj[of "{0 ..< stateN}" _ Abs_state]) + (simp, metis Rep_state Rep_state_inverse imageI subsetI) +end + +lift_definition (code_dt) ctr_loc_list :: "ctr_loc list" is "[0 ..< ctr_locN]" by (auto simp: list.pred_set) +instantiation ctr_loc :: enum begin +definition "enum_ctr_loc = ctr_loc_list" +definition "enum_all_ctr_loc P = list_all P ctr_loc_list" +definition "enum_ex_ctr_loc P = list_ex P ctr_loc_list" +instance by (standard, auto simp: enum_ctr_loc_def enum_all_ctr_loc_def enum_ex_ctr_loc_def + ctr_loc_list_def image_iff distinct_map inj_on_def Abs_ctr_loc_inject + list.pred_map list.pred_set list_ex_iff) (metis Abs_ctr_loc_cases)+ +end + +instantiation ctr_loc :: linorder begin +lift_definition less_ctr_loc :: "ctr_loc \ ctr_loc \ bool" is "(<)" . +lift_definition less_eq_ctr_loc :: "ctr_loc \ ctr_loc \ bool" is "(\)" . +instance by (standard; transfer) auto +end + +instantiation ctr_loc :: equal begin +lift_definition equal_ctr_loc :: "ctr_loc \ ctr_loc \ bool" is "(=)" . +instance by (standard; transfer) auto +end + +lift_definition (code_dt) label_list :: "label list" is "[0 ..< labelN]" by (auto simp: list.pred_set) +instantiation label :: enum begin +definition "enum_label = label_list" +definition "enum_all_label P = list_all P label_list" +definition "enum_ex_label P = list_ex P label_list" +instance by (standard, auto simp: enum_label_def enum_all_label_def enum_ex_label_def + label_list_def image_iff distinct_map inj_on_def Abs_label_inject + list.pred_map list.pred_set list_ex_iff) (metis Abs_label_cases)+ +end + +instantiation label :: linorder begin +lift_definition less_label :: "label \ label \ bool" is "(<)" . +lift_definition less_eq_label :: "label \ label \ bool" is "(\)" . +instance by (standard; transfer) auto +end + +instantiation label :: equal begin +lift_definition equal_label :: "label \ label \ bool" is "(=)" . +instance by (standard; transfer) auto +end + +instantiation state :: equal begin +lift_definition equal_state :: "state \ state \ bool" is "(=)" . +instance by (standard; transfer) auto +end + +(* The check function agrees with the encoded answer (Some True) + and therefore the proof succeeds as expected. *) +lemma + "check pds_rules initial_automaton initial_ctr_loc initial_ctr_loc_st + final_automaton final_ctr_loc final_ctr_loc_st = Some True" + by eval + +end \ No newline at end of file diff --git a/thys/Pushdown_Systems/PDS.thy b/thys/Pushdown_Systems/PDS.thy new file mode 100644 --- /dev/null +++ b/thys/Pushdown_Systems/PDS.thy @@ -0,0 +1,2717 @@ +theory PDS imports "P_Automata" "HOL-Library.While_Combinator" begin + + +section \PDS\ + +datatype 'label operation = pop | swap 'label | push 'label 'label +type_synonym ('ctr_loc, 'label) rule = "('ctr_loc \ 'label) \ ('ctr_loc \ 'label operation)" +type_synonym ('ctr_loc, 'label) conf = "'ctr_loc \ 'label list" + + +text \We define push down systems.\ + +locale PDS = + fixes \ :: "('ctr_loc, 'label::finite) rule set" + (* 'ctr_loc is the type of control locations *) + +begin + +primrec lbl :: "'label operation \ 'label list" where + "lbl pop = []" +| "lbl (swap \) = [\]" +| "lbl (push \ \') = [\, \']" + +definition is_rule :: "'ctr_loc \ 'label \ 'ctr_loc \ 'label operation \ bool" (infix "\" 80) where + "p\ \ p'w \ (p\,p'w) \ \" + +inductive_set transition_rel :: "(('ctr_loc, 'label) conf \ unit \ ('ctr_loc, 'label) conf) set" where + "(p, \) \ (p', w) \ + ((p, \#w'), (), (p', (lbl w)@w')) \ transition_rel" + +interpretation LTS transition_rel . + +notation step_relp (infix "\" 80) +notation step_starp (infix "\\<^sup>*" 80) + +lemma step_relp_def2: + "(p, \w') \ (p',ww') \ (\\ w' w. \w' = \#w' \ ww' = (lbl w)@w' \ (p, \) \ (p', w))" + by (metis (no_types, lifting) PDS.transition_rel.intros step_relp_def transition_rel.cases) + +end + + +section \PDS with P automata\ + +type_synonym ('ctr_loc, 'label) sat_rule = "('ctr_loc, 'label) transition set \ ('ctr_loc, 'label) transition set \ bool" + +datatype ('ctr_loc, 'noninit, 'label) state = + is_Init: Init (the_Ctr_Loc: 'ctr_loc) (* p \ P *) + | is_Noninit: Noninit (the_St: 'noninit) (* q \ Q \ q \ P *) + | is_Isolated: Isolated (the_Ctr_Loc: 'ctr_loc) (the_Label: 'label) (* q\<^sub>p\<^sub>\ *) + +lemma finitely_many_states: + assumes "finite (UNIV :: 'ctr_loc set)" + assumes "finite (UNIV :: 'noninit set)" + assumes "finite (UNIV :: 'label set)" + shows "finite (UNIV :: ('ctr_loc, 'noninit, 'label) state set)" +proof - + define Isolated' :: "('ctr_loc * 'label) \ ('ctr_loc, 'noninit, 'label) state" where + "Isolated' == \(c :: 'ctr_loc, l:: 'label). Isolated c l" + define Init' :: "'ctr_loc \ ('ctr_loc, 'noninit, 'label) state" where + "Init' = Init" + define Noninit' :: "'noninit \ ('ctr_loc, 'noninit, 'label) state" where + "Noninit' = Noninit" + + have split: "UNIV = (Init' ` UNIV) \ (Noninit' ` UNIV) \ (Isolated' ` (UNIV :: (('ctr_loc * 'label) set)))" + unfolding Init'_def Noninit'_def + proof (rule; rule; rule; rule) + fix x :: "('ctr_loc, 'noninit, 'label) state" + assume "x \ UNIV" + moreover + assume "x \ range Isolated'" + moreover + assume "x \ range Noninit" + ultimately + show "x \ range Init" + by (metis Isolated'_def prod.simps(2) range_eqI state.exhaust) + qed + + have "finite (Init' ` (UNIV:: 'ctr_loc set))" + using assms by auto + moreover + have "finite (Noninit' ` (UNIV:: 'noninit set))" + using assms by auto + moreover + have "finite (UNIV :: (('ctr_loc * 'label) set))" + using assms by (simp add: finite_Prod_UNIV) + then have "finite (Isolated' ` (UNIV :: (('ctr_loc * 'label) set)))" + by auto + ultimately + show "finite (UNIV :: ('ctr_loc, 'noninit, 'label) state set)" + unfolding split by auto +qed + +instantiation state :: (finite, finite, finite) finite begin + +instance by standard (simp add: finitely_many_states) + +end + + +locale PDS_with_P_automata = PDS \ + for \ :: "('ctr_loc::enum, 'label::finite) rule set" + + + fixes final_inits :: "('ctr_loc::enum) set" + fixes final_noninits :: "('noninit::finite) set" +begin + +(* Corresponds to Schwoon's F *) +definition finals :: "('ctr_loc, 'noninit::finite, 'label) state set" where + "finals = Init ` final_inits \ Noninit ` final_noninits" + +lemma F_not_Ext: "\(\f\finals. is_Isolated f)" + using finals_def by fastforce + +(* Corresponds to Schwoon's P *) +definition inits :: "('ctr_loc, 'noninit, 'label) state set" where + "inits = {q. is_Init q}" + +lemma inits_code[code]: "inits = set (map Init Enum.enum)" + by (auto simp: inits_def is_Init_def simp flip: UNIV_enum) + +definition noninits :: "('ctr_loc, 'noninit, 'label) state set" where + "noninits = {q. is_Noninit q}" + +definition isols :: "('ctr_loc, 'noninit, 'label) state set" where + "isols = {q. is_Isolated q}" + +sublocale LTS transition_rel . +notation step_relp (infix "\" 80) +notation step_starp (infix "\\<^sup>*" 80) + +definition accepts :: "(('ctr_loc, 'noninit, 'label) state, 'label) transition set \ ('ctr_loc, 'label) conf \ bool" where + "accepts ts \ \(p,w). (\q \ finals. (Init p,w,q) \ LTS.trans_star ts)" + +lemma accepts_accepts_aut: "accepts ts (p, w) \ P_Automaton.accepts_aut ts Init finals p w" + unfolding accepts_def P_Automaton.accepts_aut_def inits_def by auto + +definition accepts_\ :: "(('ctr_loc, 'noninit, 'label) state, 'label option) transition set \ ('ctr_loc, 'label) conf \ bool" where + "accepts_\ ts \ \(p,w). (\q \ finals. (Init p,w,q) \ LTS_\.trans_star_\ ts)" + +abbreviation \ :: "'label option" where + "\ == None" + +lemma accepts_mono[mono]: "mono accepts" +proof (rule, rule) + fix c :: "('ctr_loc, 'label) conf" + fix ts ts' :: "(('ctr_loc, 'noninit, 'label) state, 'label) transition set" + assume accepts_ts: "accepts ts c" + assume tsts': "ts \ ts'" + obtain p l where pl_p: "c = (p,l)" + by (cases c) + obtain q where q_p: "q \ finals \ (Init p, l, q) \ LTS.trans_star ts" + using accepts_ts unfolding pl_p accepts_def by auto + then have "(Init p, l, q) \ LTS.trans_star ts'" + using tsts' LTS_trans_star_mono monoD by blast + then have "accepts ts' (p,l)" + unfolding accepts_def using q_p by auto + then show "accepts ts' c" + unfolding pl_p . +qed + +lemma accepts_cons: "(Init p, \, Init p') \ ts \ accepts ts (p', w) \ accepts ts (p, \ # w)" + using LTS.trans_star.trans_star_step accepts_def by fastforce + +definition lang :: "(('ctr_loc, 'noninit, 'label) state, 'label) transition set \ ('ctr_loc, 'label) conf set" where + "lang ts = {c. accepts ts c}" + +lemma lang_lang_aut: "lang ts = (\(s,w). (s, w)) ` (P_Automaton.lang_aut ts Init finals)" + unfolding lang_def P_Automaton.lang_aut_def + by (auto simp: inits_def accepts_def P_Automaton.accepts_aut_def image_iff intro!: exI[of _ "Init _"]) + +lemma lang_aut_lang: "P_Automaton.lang_aut ts Init finals = lang ts" + unfolding lang_lang_aut + by (auto 0 3 simp: P_Automaton.lang_aut_def P_Automaton.accepts_aut_def inits_def image_iff) + +definition lang_\ :: "(('ctr_loc, 'noninit, 'label) state, 'label option) transition set \ ('ctr_loc, 'label) conf set" where + "lang_\ ts = {c. accepts_\ ts c}" + + +subsection \Saturations\ + +definition saturated :: "('c, 'l) sat_rule \ ('c, 'l) transition set \ bool" where + "saturated rule ts \ (\ts'. rule ts ts')" + +definition saturation :: "('c, 'l) sat_rule \ ('c, 'l) transition set \ ('c, 'l) transition set \ bool" where + "saturation rule ts ts' \ rule\<^sup>*\<^sup>* ts ts' \ saturated rule ts'" + +lemma no_infinite: + assumes "\ts ts' :: ('c ::finite, 'l::finite) transition set. rule ts ts' \ card ts' = Suc (card ts)" + assumes "\i :: nat. rule (tts i) (tts (Suc i))" + shows "False" +proof - + define f where "f i = card (tts i)" for i + have f_Suc: "\i. f i < f (Suc i)" + using assms f_def lessI by metis + have "\i. \j. f j > i" + proof + fix i + show "\j. i < f j" + proof(induction i) + case 0 + then show ?case + by (metis f_Suc neq0_conv) + next + case (Suc i) + then show ?case + by (metis Suc_lessI f_Suc) + qed + qed + then have "\j. f j > card (UNIV :: ('c, 'l) transition set)" + by auto + then show False + by (metis card_seteq f_def finite_UNIV le_eq_less_or_eq nat_neq_iff subset_UNIV) +qed + +lemma saturation_termination: + assumes "\ts ts' :: ('c ::finite, 'l::finite) transition set. rule ts ts' \ card ts' = Suc (card ts)" + shows "\(\tts. (\i :: nat. rule (tts i) (tts (Suc i))))" + using assms no_infinite by blast + +lemma saturation_exi: + assumes "\ts ts' :: ('c ::finite, 'l::finite) transition set. rule ts ts' \ card ts' = Suc (card ts)" + shows "\ts'. saturation rule ts ts'" +proof (rule ccontr) + assume a: "\ts'. saturation rule ts ts'" + define g where "g ts = (SOME ts'. rule ts ts')" for ts + define tts where "tts i = (g ^^ i) ts" for i + have "\i :: nat. rule\<^sup>*\<^sup>* ts (tts i) \ rule (tts i) (tts (Suc i))" + proof + fix i + show "rule\<^sup>*\<^sup>* ts (tts i) \ rule (tts i) (tts (Suc i))" + proof (induction i) + case 0 + have "rule ts (g ts)" + by (metis g_def a rtranclp.rtrancl_refl saturation_def saturated_def someI) + then show ?case + using tts_def a saturation_def by auto + next + case (Suc i) + then have sat_Suc: "rule\<^sup>*\<^sup>* ts (tts (Suc i))" + by fastforce + then have "rule (g ((g ^^ i) ts)) (g (g ((g ^^ i) ts)))" + by (metis Suc.IH tts_def g_def a r_into_rtranclp rtranclp_trans saturation_def saturated_def + someI) + then have "rule (tts (Suc i)) (tts (Suc (Suc i)))" + unfolding tts_def by simp + then show ?case + using sat_Suc by auto + qed + qed + then have "\i. rule (tts i) (tts (Suc i))" + by auto + then show False + using no_infinite assms by auto +qed + + +subsection \Saturation rules\ + +inductive pre_star_rule :: "(('ctr_loc, 'noninit, 'label) state, 'label) transition set \ (('ctr_loc, 'noninit, 'label) state, 'label) transition set \ bool" where + add_trans: "(p, \) \ (p', w) \ (Init p', lbl w, q) \ LTS.trans_star ts \ + (Init p, \, q) \ ts \ pre_star_rule ts (ts \ {(Init p, \, q)})" + +definition pre_star1 :: "(('ctr_loc, 'noninit, 'label) state, 'label) transition set \ (('ctr_loc, 'noninit, 'label) state, 'label) transition set" where + "pre_star1 ts = + (\((p, \), (p', w)) \ \. \q \ LTS.reach ts (Init p') (lbl w). {(Init p, \, q)})" + +lemma pre_star1_mono: "mono pre_star1" + unfolding pre_star1_def + by (auto simp: mono_def LTS.trans_star_code[symmetric] elim!: bexI[rotated] + LTS_trans_star_mono[THEN monoD, THEN subsetD]) + +lemma pre_star_rule_pre_star1: + assumes "X \ pre_star1 ts" + shows "pre_star_rule\<^sup>*\<^sup>* ts (ts \ X)" +proof - + have "finite X" + by simp + from this assms show ?thesis + proof (induct X arbitrary: ts rule: finite_induct) + case (insert x F) + then obtain p \ p' w q where *: "(p, \) \ (p', w)" + "(Init p', lbl w, q) \ LTS.trans_star ts" and x: + "x = (Init p, \, q)" + by (auto simp: pre_star1_def is_rule_def LTS.trans_star_code) + with insert show ?case + proof (cases "(Init p, \, q) \ ts") + case False + with insert(1,2,4) x show ?thesis + by (intro converse_rtranclp_into_rtranclp[of pre_star_rule, OF add_trans[OF * False]]) + (auto intro!: insert(3)[of "insert x ts", simplified x Un_insert_left] + intro: pre_star1_mono[THEN monoD, THEN set_mp, of ts]) + qed (simp add: insert_absorb) + qed simp +qed + +lemma pre_star_rule_pre_star1s: "pre_star_rule\<^sup>*\<^sup>* ts (((\s. s \ pre_star1 s) ^^ k) ts)" + by (induct k) (auto elim!: rtranclp_trans intro: pre_star_rule_pre_star1) + +definition "pre_star_loop = while_option (\s. s \ pre_star1 s \ s) (\s. s \ pre_star1 s)" +definition "pre_star_exec = the o pre_star_loop" +definition "pre_star_exec_check A = (if inits \ LTS.srcs A then pre_star_loop A else None)" + +definition "accept_pre_star_exec_check A c = (if inits \ LTS.srcs A then Some (accepts (pre_star_exec A) c) else None)" + +lemma while_option_finite_subset_Some: fixes C :: "'a set" + assumes "mono f" and "!!X. X \ C \ f X \ C" and "finite C" and X: "X \ C" "X \ f X" + shows "\P. while_option (\A. f A \ A) f X = Some P" +proof(rule measure_while_option_Some[where + f= "%A::'a set. card C - card A" and P= "%A. A \ C \ A \ f A" and s= X]) + fix A assume A: "A \ C \ A \ f A" "f A \ A" + show "(f A \ C \ f A \ f (f A)) \ card C - card (f A) < card C - card A" + (is "?L \ ?R") + proof + show ?L by(metis A(1) assms(2) monoD[OF \mono f\]) + show ?R + by (metis A assms(2,3) card_seteq diff_less_mono2 equalityI linorder_le_less_linear + rev_finite_subset) + qed +qed (simp add: X) + +lemma pre_star_exec_terminates: "\t. pre_star_loop s = Some t" + unfolding pre_star_loop_def + by (rule while_option_finite_subset_Some[where C=UNIV]) + (auto simp: mono_def dest: pre_star1_mono[THEN monoD]) + +lemma pre_star_exec_code[code]: + "pre_star_exec s = (let s' = pre_star1 s in if s' \ s then s else pre_star_exec (s \ s'))" + unfolding pre_star_exec_def pre_star_loop_def o_apply + by (subst while_option_unfold)(auto simp: Let_def) + +lemma saturation_pre_star_exec: "saturation pre_star_rule ts (pre_star_exec ts)" +proof - + from pre_star_exec_terminates obtain t where t: "pre_star_loop ts = Some t" + by blast + obtain k where k: "t = ((\s. s \ pre_star1 s) ^^ k) ts" and le: "pre_star1 t \ t" + using while_option_stop2[OF t[unfolded pre_star_loop_def]] by auto + have "(\{us. pre_star_rule t us}) - t \ pre_star1 t" + by (auto simp: pre_star1_def LTS.trans_star_code[symmetric] prod.splits is_rule_def + pre_star_rule.simps) + from subset_trans[OF this le] show ?thesis + unfolding saturation_def saturated_def pre_star_exec_def o_apply k t + by (auto 9 0 simp: pre_star_rule_pre_star1s subset_eq pre_star_rule.simps) +qed + +inductive post_star_rules :: "(('ctr_loc, 'noninit, 'label) state, 'label option) transition set \ (('ctr_loc, 'noninit, 'label) state, 'label option) transition set \ bool" where + add_trans_pop: + "(p, \) \ (p', pop) \ + (Init p, [\], q) \ LTS_\.trans_star_\ ts \ + (Init p', \, q) \ ts \ + post_star_rules ts (ts \ {(Init p', \, q)})" +| add_trans_swap: + "(p, \) \ (p', swap \') \ + (Init p, [\], q) \ LTS_\.trans_star_\ ts \ + (Init p', Some \', q) \ ts \ + post_star_rules ts (ts \ {(Init p', Some \', q)})" +| add_trans_push_1: + "(p, \) \ (p', push \' \'') \ + (Init p, [\], q) \ LTS_\.trans_star_\ ts \ + (Init p', Some \', Isolated p' \') \ ts \ + post_star_rules ts (ts \ {(Init p', Some \', Isolated p' \')})" +| add_trans_push_2: + "(p, \) \ (p', push \' \'') \ + (Init p, [\], q) \ LTS_\.trans_star_\ ts \ + (Isolated p' \', Some \'', q) \ ts \ + (Init p', Some \', Isolated p' \') \ ts \ + post_star_rules ts (ts \ {(Isolated p' \', Some \'', q)})" + +lemma pre_star_rule_mono: + "pre_star_rule ts ts' \ ts \ ts'" + unfolding pre_star_rule.simps by auto + +lemma post_star_rules_mono: + "post_star_rules ts ts' \ ts \ ts'" +proof(induction rule: post_star_rules.induct) + case (add_trans_pop p \ p' q ts) + then show ?case by auto +next + case (add_trans_swap p \ p' \' q ts) + then show ?case by auto +next + case (add_trans_push_1 p \ p' \' \'' q ts) + then show ?case by auto +next + case (add_trans_push_2 p \ p' \' \'' q ts) + then show ?case by auto +qed + +lemma pre_star_rule_card_Suc: "pre_star_rule ts ts' \ card ts' = Suc (card ts)" + unfolding pre_star_rule.simps by auto + +lemma post_star_rules_card_Suc: "post_star_rules ts ts' \ card ts' = Suc (card ts)" +proof(induction rule: post_star_rules.induct) + case (add_trans_pop p \ p' q ts) + then show ?case by auto +next + case (add_trans_swap p \ p' \' q ts) + then show ?case by auto +next + case (add_trans_push_1 p \ p' \' \'' q ts) + then show ?case by auto +next + case (add_trans_push_2 p \ p' \' \'' q ts) + then show ?case by auto +qed + + +lemma pre_star_saturation_termination: + "\(\tts. (\i :: nat. pre_star_rule (tts i) (tts (Suc i))))" + using no_infinite pre_star_rule_card_Suc by blast + +lemma post_star_saturation_termination: + "\(\tts. (\i :: nat. post_star_rules (tts i) (tts (Suc i))))" + using no_infinite post_star_rules_card_Suc by blast + +lemma pre_star_saturation_exi: + shows "\ts'. saturation pre_star_rule ts ts'" + using pre_star_rule_card_Suc saturation_exi by blast + +lemma post_star_saturation_exi: + shows "\ts'. saturation post_star_rules ts ts'" + using post_star_rules_card_Suc saturation_exi by blast + +lemma pre_star_rule_incr: "pre_star_rule A B \ A \ B" +proof(induction rule: pre_star_rule.inducts) + case (add_trans p \ p' w q rel) + then show ?case + by auto +qed + +lemma post_star_rules_incr: "post_star_rules A B \ A \ B" +proof(induction rule: post_star_rules.inducts) + case (add_trans_pop p \ p' q ts) + then show ?case + by auto +next + case (add_trans_swap p \ p' \' q ts) + then show ?case + by auto +next + case (add_trans_push_1 p \ p' \' \'' q ts) + then show ?case + by auto +next + case (add_trans_push_2 p \ p' \' \'' q ts) + then show ?case + by auto +qed + +lemma saturation_rtranclp_pre_star_rule_incr: "pre_star_rule\<^sup>*\<^sup>* A B \ A \ B" +proof (induction rule: rtranclp_induct) + case base + then show ?case by auto +next + case (step y z) + then show ?case + using pre_star_rule_incr by auto +qed + +lemma saturation_rtranclp_post_star_rule_incr: "post_star_rules\<^sup>*\<^sup>* A B \ A \ B" +proof (induction rule: rtranclp_induct) + case base + then show ?case by auto +next + case (step y z) + then show ?case + using post_star_rules_incr by auto +qed + +lemma pre_star'_incr_trans_star: + "pre_star_rule\<^sup>*\<^sup>* A A' \ LTS.trans_star A \ LTS.trans_star A'" + using mono_def LTS_trans_star_mono saturation_rtranclp_pre_star_rule_incr by metis + +lemma post_star'_incr_trans_star: + "post_star_rules\<^sup>*\<^sup>* A A' \ LTS.trans_star A \ LTS.trans_star A'" + using mono_def LTS_trans_star_mono saturation_rtranclp_post_star_rule_incr by metis + +lemma post_star'_incr_trans_star_\: + "post_star_rules\<^sup>*\<^sup>* A A' \ LTS_\.trans_star_\ A \ LTS_\.trans_star_\ A'" + using mono_def LTS_\_trans_star_\_mono saturation_rtranclp_post_star_rule_incr by metis + +lemma pre_star_lim'_incr_trans_star: + "saturation pre_star_rule A A' \ LTS.trans_star A \ LTS.trans_star A'" + by (simp add: pre_star'_incr_trans_star saturation_def) + +lemma post_star_lim'_incr_trans_star: + "saturation post_star_rules A A' \ LTS.trans_star A \ LTS.trans_star A'" + by (simp add: post_star'_incr_trans_star saturation_def) + +lemma post_star_lim'_incr_trans_star_\: + "saturation post_star_rules A A' \ LTS_\.trans_star_\ A \ LTS_\.trans_star_\ A'" + by (simp add: post_star'_incr_trans_star_\ saturation_def) + + +subsection \Pre* lemmas\ + +lemma inits_srcs_iff_Ctr_Loc_srcs: + "inits \ LTS.srcs A \ (\q \ q'. (q, \, Init q') \ A)" +proof + assume "inits \ LTS.srcs A" + then show "\q \ q'. (q, \, Init q') \ A" + by (simp add: Collect_mono_iff LTS.srcs_def inits_def) +next + assume "\q \ q'. (q, \, Init q') \ A" + show "inits \ LTS.srcs A" + by (metis LTS.srcs_def2 inits_def \\q \ q'. (q, \, Init q') \ A\ mem_Collect_eq + state.collapse(1) subsetI) +qed + +lemma lemma_3_1: + assumes "p'w \\<^sup>* pv" + assumes "pv \ lang A" + assumes "saturation pre_star_rule A A'" + shows "accepts A' p'w" + using assms +proof (induct rule: converse_rtranclp_induct) + case base + define p where "p = fst pv" + define v where "v = snd pv" + from base have "\q \ finals. (Init p, v, q) \ LTS.trans_star A'" + unfolding lang_def p_def v_def using pre_star_lim'_incr_trans_star accepts_def by fastforce + then show ?case + unfolding accepts_def p_def v_def by auto +next + case (step p'w p''u) + define p' where "p' = fst p'w" + define w where "w = snd p'w" + define p'' where "p'' = fst p''u" + define u where "u = snd p''u" + have p'w_def: "p'w = (p', w)" + using p'_def w_def by auto + have p''u_def: "p''u = (p'', u)" + using p''_def u_def by auto + + then have "accepts A' (p'', u)" + using step by auto + then obtain q where q_p: "q \ finals \ (Init p'', u, q) \ LTS.trans_star A'" + unfolding accepts_def by auto + have "\\ w1 u1. w=\#w1 \ u=lbl u1@w1 \ (p', \) \ (p'', u1)" + using p''u_def p'w_def step.hyps(1) step_relp_def2 by auto + then obtain \ w1 u1 where \_w1_u1_p: "w=\#w1 \ u=lbl u1@w1 \ (p', \) \ (p'', u1)" + by blast + + then have "\q1. (Init p'', lbl u1, q1) \ LTS.trans_star A' \ (q1, w1, q) \ LTS.trans_star A'" + using q_p LTS.trans_star_split by auto + + then obtain q1 where q1_p: "(Init p'', lbl u1, q1) \ LTS.trans_star A' \ (q1, w1, q) \ LTS.trans_star A'" + by auto + + then have in_A': "(Init p', \, q1) \ A'" + using \_w1_u1_p add_trans[of p' \ p'' u1 q1 A'] saturated_def saturation_def step.prems by metis + + then have "(Init p', \#w1, q) \ LTS.trans_star A'" + using LTS.trans_star.trans_star_step q1_p by meson + then have t_in_A': "(Init p', w, q) \ LTS.trans_star A'" + using \_w1_u1_p by blast + + from q_p t_in_A' have "q \ finals \ (Init p', w, q) \ LTS.trans_star A'" + by auto + then show ?case + unfolding accepts_def p'w_def by auto +qed + +lemma word_into_init_empty_states: + fixes A :: "(('ctr_loc, 'noninit, 'label) state, 'label) transition set" + assumes "(p, w, ss, Init q) \ LTS.trans_star_states A" + assumes "inits \ LTS.srcs A" + shows "w = [] \ p = Init q \ ss=[p]" +proof - + define q1 :: "('ctr_loc, 'noninit, 'label) state" where + "q1 = Init q" + have q1_path: "(p, w, ss, q1) \ LTS.trans_star_states A" + by (simp add: assms(1) q1_def) + moreover + have "q1 \ inits" + by (simp add: inits_def q1_def) + ultimately + have "w = [] \ p = q1 \ ss=[p]" + proof(induction rule: LTS.trans_star_states.induct[OF q1_path]) + case (1 p) + then show ?case by auto + next + case (2 p \ q' w ss q) + have "\q \ q'. (q, \, Init q') \ A" + using assms(2) unfolding inits_def LTS.srcs_def by (simp add: Collect_mono_iff) + then show ?case + using 2 assms(2) by (metis inits_def is_Init_def mem_Collect_eq) + qed + then show ?thesis + using q1_def by fastforce +qed + +(* This corresponds to and slightly generalizes Schwoon's lemma 3.2(b) *) +lemma word_into_init_empty: + fixes A :: "(('ctr_loc, 'noninit, 'label) state, 'label) transition set" + assumes "(p, w, Init q) \ LTS.trans_star A" + assumes "inits \ LTS.srcs A" + shows "w = [] \ p = Init q" + using assms word_into_init_empty_states LTS.trans_star_trans_star_states by metis + +lemma step_relp_append_aux: + assumes "pu \\<^sup>* p1y" + shows "(fst pu, snd pu @ v) \\<^sup>* (fst p1y, snd p1y @ v)" + using assms +proof (induction rule: rtranclp_induct) + case base + then show ?case by auto +next + case (step p'w p1y) + define p where "p = fst pu" + define u where "u = snd pu" + define p' where "p' = fst p'w" + define w where "w = snd p'w" + define p1 where "p1 = fst p1y" + define y where "y = snd p1y" + have step_1: "(p,u) \\<^sup>* (p',w)" + by (simp add: p'_def p_def step.hyps(1) u_def w_def) + have step_2: "(p',w) \ (p1,y)" + by (simp add: p'_def p1_def step.hyps(2) w_def y_def) + have step_3: "(p, u @ v) \\<^sup>* (p', w @ v)" + by (simp add: p'_def p_def step.IH u_def w_def) + + note step' = step_1 step_2 step_3 + + from step'(2) have "\\ w' wa. w = \ # w' \ y = lbl wa @ w' \ (p', \) \ (p1, wa)" + using step_relp_def2[of p' w p1 y] by auto + then obtain \ w' wa where \_w'_wa_p: " w = \ # w' \ y = lbl wa @ w' \ (p', \) \ (p1, wa)" + by metis + then have "(p, u @ v) \\<^sup>* (p1, y @ v)" + by (metis (no_types, lifting) PDS.step_relp_def2 append.assoc append_Cons rtranclp.simps step_3) + then show ?case + by (simp add: p1_def p_def u_def y_def) +qed + +lemma step_relp_append: + assumes "(p, u) \\<^sup>* (p1, y)" + shows "(p, u @ v) \\<^sup>* (p1, y @ v)" + using assms step_relp_append_aux by auto + +lemma step_relp_append_empty: + assumes "(p, u) \\<^sup>* (p1, [])" + shows "(p, u @ v) \\<^sup>* (p1, v)" + using step_relp_append[OF assms] by auto + +lemma lemma_3_2_a': + assumes "inits \ LTS.srcs A" + assumes "pre_star_rule\<^sup>*\<^sup>* A A'" + assumes "(Init p, w, q) \ LTS.trans_star A'" + shows "\p' w'. (Init p', w', q) \ LTS.trans_star A \ (p, w) \\<^sup>* (p', w')" + using assms(2) assms(3) +proof (induction arbitrary: p q w rule: rtranclp_induct) + case base + then have "(Init p, w, q) \ LTS.trans_star A \ (p, w) \\<^sup>* (p, w)" + by auto + then show ?case + by auto +next + case (step Aiminus1 Ai) + + from step(2) obtain p1 \ p2 w2 q' where p1_\_p2_w2_q'_p: + "Ai = Aiminus1 \ {(Init p1, \, q')}" + "(p1, \) \ (p2, w2)" + "(Init p2, lbl w2, q') \ LTS.trans_star Aiminus1" + "(Init p1, \, q') \ Aiminus1" + by (meson pre_star_rule.cases) + + define t :: "(('ctr_loc, 'noninit, 'label) state, 'label) transition" + where "t = (Init p1, \, q')" + + obtain ss where ss_p: "(Init p, w, ss, q) \ LTS.trans_star_states Ai" + using step(4) LTS.trans_star_trans_star_states by metis + + define j where "j = count (transitions_of' (Init p, w, ss, q)) t" + + from j_def ss_p show ?case + proof (induction j arbitrary: p q w ss) + case 0 + then have "(Init p, w, q) \ LTS.trans_star Aiminus1" + using count_zero_remove_trans_star_states_trans_star p1_\_p2_w2_q'_p(1) t_def by metis + then show ?case + using step.IH by metis + next + case (Suc j') + have "\u v u_ss v_ss. + ss = u_ss@v_ss \ w = u@[\]@v \ + (Init p,u,u_ss, Init p1) \ LTS.trans_star_states Aiminus1 \ + (Init p1,[\],q') \ LTS.trans_star Ai \ + (q',v,v_ss,q) \ LTS.trans_star_states Ai \ + (Init p, w, ss, q) = ((Init p, u, u_ss, Init p1), \) @@\<^sup>\ (q', v, v_ss, q)" + using split_at_first_t[of "Init p" w ss q Ai j' "Init p1" \ q' Aiminus1] + using Suc(2,3) t_def p1_\_p2_w2_q'_p(1,4) t_def by auto + then obtain u v u_ss v_ss where u_v_u_ss_v_ss_p: + "ss = u_ss@v_ss \ w = u@[\]@v" + "(Init p,u,u_ss, Init p1) \ LTS.trans_star_states Aiminus1" + "(Init p1,[\],q') \ LTS.trans_star Ai" + "(q',v,v_ss,q) \ LTS.trans_star_states Ai" + "(Init p, w, ss, q) = ((Init p, u, u_ss, Init p1), \) @@\<^sup>\ (q', v, v_ss, q)" + by blast + from this(2) have "\p'' w''. (Init p'', w'', Init p1) \ LTS.trans_star A \ (p, u) \\<^sup>* (p'', w'')" + using Suc(1)[of p u _ "Init p1"] step.IH step.prems(1) + by (meson LTS.trans_star_states_trans_star LTS.trans_star_trans_star_states) + from this this(1) have VIII: "(p, u) \\<^sup>* (p1, [])" + using word_into_init_empty assms(1) by blast + + note IX = p1_\_p2_w2_q'_p(2) + note III = p1_\_p2_w2_q'_p(3) + from III have III_2: "\w2_ss. (Init p2, lbl w2, w2_ss, q') \ LTS.trans_star_states Aiminus1" + using LTS.trans_star_trans_star_states[of "Init p2" "lbl w2" q' Aiminus1] by auto + then obtain w2_ss where III_2: "(Init p2, lbl w2, w2_ss, q') \ LTS.trans_star_states Aiminus1" + by blast + + from III have V: + "(Init p2, lbl w2, w2_ss, q') \ LTS.trans_star_states Aiminus1" + "(q', v, v_ss, q) \ LTS.trans_star_states Ai" + using III_2 \(q', v, v_ss, q) \ LTS.trans_star_states Ai\ by auto + + define w2v where "w2v = lbl w2 @ v" + define w2v_ss where "w2v_ss = w2_ss @ tl v_ss" + + from V(1) have "(Init p2, lbl w2, w2_ss, q') \ LTS.trans_star_states Ai" + using trans_star_states_mono p1_\_p2_w2_q'_p(1) using Un_iff subsetI by (metis (no_types)) + then have V_merged: "(Init p2, w2v, w2v_ss, q) \ LTS.trans_star_states Ai" + using V(2) unfolding w2v_def w2v_ss_def by (meson LTS.trans_star_states_append) + + have j'_count: "j' = count (transitions_of' (Init p2, w2v, w2v_ss, q)) t" + proof - + define countts where + "countts == \x. count (transitions_of' x) t" + + have "countts (Init p, w, ss, q) = Suc j' " + using Suc.prems(1) countts_def by force + moreover + have "countts (Init p, u, u_ss, Init p1) = 0" + using LTS.avoid_count_zero countts_def p1_\_p2_w2_q'_p(4) t_def u_v_u_ss_v_ss_p(2) + by fastforce + moreover + from u_v_u_ss_v_ss_p(5) have "countts (Init p, w, ss, q) = countts (Init p, u, u_ss, Init p1) + 1 + countts (q', v, v_ss, q)" + using count_combine_trans_star_states countts_def t_def u_v_u_ss_v_ss_p(2) + u_v_u_ss_v_ss_p(4) by fastforce + ultimately + have "Suc j' = 0 + 1 + countts (q', v, v_ss, q)" + by auto + then have "j' = countts (q', v, v_ss, q)" + by auto + moreover + have "countts (Init p2, lbl w2, w2_ss, q') = 0" + using III_2 LTS.avoid_count_zero countts_def p1_\_p2_w2_q'_p(4) t_def by fastforce + moreover + have "(Init p2, w2v, w2v_ss, q) = (Init p2, lbl w2, w2_ss, q') @@\ (q', v, v_ss, q)" + using w2v_def w2v_ss_def by auto + then have "countts (Init p2, w2v, w2v_ss, q) = countts (Init p2, lbl w2, w2_ss, q') + countts (q', v, v_ss, q)" + using \(Init p2, lbl w2, w2_ss, q') \ LTS.trans_star_states Ai\ + count_append_trans_star_states countts_def t_def u_v_u_ss_v_ss_p(4) by fastforce + ultimately + show ?thesis + by (simp add: countts_def) + qed + + have "\p' w'. (Init p', w', q) \ LTS.trans_star A \ (p2, w2v) \\<^sup>* (p', w')" + using Suc(1) using j'_count V_merged by auto + then obtain p' w' where p'_w'_p: "(Init p', w', q) \ LTS.trans_star A" "(p2, w2v) \\<^sup>* (p', w')" + by blast + + note X = p'_w'_p(2) + + have "(p,w) = (p,u@[\]@v)" + using \ss = u_ss @ v_ss \ w = u @ [\] @ v\ by blast + + have "(p,u@[\]@v) \\<^sup>* (p1,\#v)" + using VIII step_relp_append_empty by auto + + from X have "(p1,\#v) \ (p2, w2v)" + by (metis IX LTS.step_relp_def transition_rel.intros w2v_def) + + from X have + "(p2, w2v) \\<^sup>* (p', w')" + by simp + + have "(p, w) \\<^sup>* (p', w')" + using X \(p, u @ [\] @ v) \\<^sup>* (p1, \ # v)\ \(p, w) = (p, u @ [\] @ v)\ \(p1, \ # v) \ (p2, w2v)\ by auto + + then have "(Init p', w', q) \ LTS.trans_star A \ (p, w) \\<^sup>* (p', w')" + using p'_w'_p(1) by auto + then show ?case + by metis + qed +qed + +lemma lemma_3_2_a: + assumes "inits \ LTS.srcs A" + assumes "saturation pre_star_rule A A'" + assumes "(Init p, w, q) \ LTS.trans_star A'" + shows "\p' w'. (Init p', w', q) \ LTS.trans_star A \ (p, w) \\<^sup>* (p', w')" + using assms lemma_3_2_a' saturation_def by metis + +\ \Corresponds to one direction of Schwoon's theorem 3.2\ +theorem pre_star_rule_subset_pre_star_lang: + assumes "inits \ LTS.srcs A" + assumes "pre_star_rule\<^sup>*\<^sup>* A A'" + shows "{c. accepts A' c} \ pre_star (lang A)" +proof + fix c :: "'ctr_loc \ 'label list" + assume c_a: "c \ {w. accepts A' w}" + define p where "p = fst c" + define w where "w = snd c" + from p_def w_def c_a have "accepts A' (p,w)" + by auto + then have "\q \ finals. (Init p, w, q) \ LTS.trans_star A'" + unfolding accepts_def by auto + then obtain q where q_p: "q \ finals" "(Init p, w, q) \ LTS.trans_star A'" + by auto + then have "\p' w'. (p,w) \\<^sup>* (p',w') \ (Init p', w', q) \ LTS.trans_star A" + using lemma_3_2_a' assms(1) assms(2) by metis + then obtain p' w' where p'_w'_p: "(p,w) \\<^sup>* (p',w')" "(Init p', w', q) \ LTS.trans_star A" + by auto + then have "(p', w') \ lang A" + unfolding lang_def unfolding accepts_def using q_p(1) by auto + then have "(p,w) \ pre_star (lang A)" + unfolding pre_star_def using p'_w'_p(1) by auto + then show "c \ pre_star (lang A)" + unfolding p_def w_def by auto +qed + +\ \Corresponds to Schwoon's theorem 3.2\ +theorem pre_star_rule_accepts_correct: + assumes "inits \ LTS.srcs A" + assumes "saturation pre_star_rule A A'" + shows "{c. accepts A' c} = pre_star (lang A)" +proof (rule; rule) + fix c :: "'ctr_loc \ 'label list" + define p where "p = fst c" + define w where "w = snd c" + assume "c \ pre_star (lang A)" + then have "(p,w) \ pre_star (lang A)" + unfolding p_def w_def by auto + then have "\p' w'. (p',w') \ lang A \ (p,w) \\<^sup>* (p',w')" + unfolding pre_star_def by force + then obtain p' w' where "(p',w') \ lang A \ (p,w) \\<^sup>* (p',w')" + by auto + then have "\q \ finals. (Init p, w, q) \ LTS.trans_star A'" + using lemma_3_1 assms(2) unfolding accepts_def by force + then have "accepts A' (p,w)" + unfolding accepts_def by auto + then show "c \ {c. accepts A' c}" + using p_def w_def by auto +next + fix c :: "'ctr_loc \ 'label list" + assume "c \ {w. accepts A' w}" + then show "c \ pre_star (lang A)" + using pre_star_rule_subset_pre_star_lang assms unfolding saturation_def by auto +qed + +\ \Corresponds to Schwoon's theorem 3.2\ +theorem pre_star_rule_correct: + assumes "inits \ LTS.srcs A" + assumes "saturation pre_star_rule A A'" + shows "lang A' = pre_star (lang A)" + using assms(1) assms(2) lang_def pre_star_rule_accepts_correct by auto + +theorem pre_star_exec_accepts_correct: + assumes "inits \ LTS.srcs A" + shows "{c. accepts (pre_star_exec A) c} = pre_star (lang A)" + using pre_star_rule_accepts_correct[of A "pre_star_exec A"] saturation_pre_star_exec[of A] + assms by auto + +theorem pre_star_exec_lang_correct: + assumes "inits \ LTS.srcs A" + shows "lang (pre_star_exec A) = pre_star (lang A)" + using pre_star_rule_correct[of A "pre_star_exec A"] saturation_pre_star_exec[of A] assms by auto + +theorem pre_star_exec_check_accepts_correct: + assumes "pre_star_exec_check A \ None" + shows "{c. accepts (the (pre_star_exec_check A)) c} = pre_star (lang A)" + using pre_star_exec_accepts_correct assms unfolding pre_star_exec_check_def pre_star_exec_def + by (auto split: if_splits) + +theorem pre_star_exec_check_correct: + assumes "pre_star_exec_check A \ None" + shows "lang (the (pre_star_exec_check A)) = pre_star (lang A)" + using pre_star_exec_check_accepts_correct assms unfolding lang_def by auto + +theorem accept_pre_star_exec_correct_True: + assumes "inits \ LTS.srcs A" + assumes "accepts (pre_star_exec A) c" + shows "c \ pre_star (lang A)" + using pre_star_exec_accepts_correct assms(1) assms(2) by blast + +theorem accept_pre_star_exec_correct_False: + assumes "inits \ LTS.srcs A" + assumes "\accepts (pre_star_exec A) c" + shows "c \ pre_star (lang A)" + using pre_star_exec_accepts_correct assms(1) assms(2) by blast + +theorem accept_pre_star_exec_correct_Some_True: + assumes "accept_pre_star_exec_check A c = Some True" + shows "c \ pre_star (lang A)" +proof - + have "inits \ LTS.srcs A" + using assms unfolding accept_pre_star_exec_check_def + by (auto split: if_splits) + moreover + have "accepts (pre_star_exec A) c" + using assms + using accept_pre_star_exec_check_def calculation by auto + ultimately + show "c \ pre_star (lang A)" + using accept_pre_star_exec_correct_True by auto +qed + +theorem accept_pre_star_exec_correct_Some_False: + assumes "accept_pre_star_exec_check A c = Some False" + shows "c \ pre_star (lang A)" +proof - + have "inits \ LTS.srcs A" + using assms unfolding accept_pre_star_exec_check_def + by (auto split: if_splits) + moreover + have "\accepts (pre_star_exec A) c" + using assms + using accept_pre_star_exec_check_def calculation by auto + ultimately + show "c \ pre_star (lang A)" + using accept_pre_star_exec_correct_False by auto +qed + +theorem accept_pre_star_exec_correct_None: + assumes "accept_pre_star_exec_check A c = None" + shows "\inits \ LTS.srcs A" + using assms unfolding accept_pre_star_exec_check_def by auto + + +subsection \Post* lemmas\ + +lemma lemma_3_3': + assumes "pv \\<^sup>* p'w" + and "(fst pv, snd pv) \ lang_\ A" + and "saturation post_star_rules A A'" + shows "accepts_\ A' (fst p'w, snd p'w)" + using assms +proof (induct arbitrary: pv rule: rtranclp_induct) + case base + show ?case + using assms post_star_lim'_incr_trans_star_\ + by (auto simp: lang_\_def accepts_\_def) +next + case (step p''u p'w) + define p' where "p' = fst p'w" + define w where "w = snd p'w" + define p'' where "p'' = fst p''u" + define u where "u = snd p''u" + have p'w_def: "p'w = (p', w)" + using p'_def w_def by auto + have p''u_def: "p''u = (p'', u)" + using p''_def u_def by auto + + then have "accepts_\ A' (p'', u)" + using assms(2) p''_def step.hyps(3) step.prems(2) u_def by metis + then have "\q. q \ finals \ (Init p'', u, q) \ LTS_\.trans_star_\ A'" + by (auto simp: accepts_\_def) + then obtain q where q_p: "q \ finals \ (Init p'', u, q) \ LTS_\.trans_star_\ A'" + by metis + then have "\u_\. q \ finals \ LTS_\.\_exp u_\ u \ (Init p'', u_\, q) \ LTS.trans_star A'" + using LTS_\.trans_star_\_iff_\_exp_trans_star[of "Init p''" u q A'] by auto + then obtain u_\ where II: "q \ finals" "LTS_\.\_exp u_\ u" "(Init p'', u_\, q) \ LTS.trans_star A'" + by blast + have "\\ u1 w1. u=\#u1 \ w=lbl w1@u1 \ (p'', \) \ (p', w1)" + using p''u_def p'w_def step.hyps(2) step_relp_def2 by auto + then obtain \ u1 w1 where III: "u=\#u1" "w=lbl w1@u1" "(p'', \) \ (p', w1)" + by blast + + have p'_inits: "Init p' \ inits" + unfolding inits_def by auto + have p''_inits: "Init p'' \ inits" + unfolding inits_def by auto + + have "\\_\ u1_\. LTS_\.\_exp \_\ [\] \ LTS_\.\_exp u1_\ u1 \ (Init p'', \_\@u1_\, q) \ LTS.trans_star A'" + proof - + have "\\_\ u1_\. LTS_\.\_exp \_\ [\] \ LTS_\.\_exp u1_\ u1 \ u_\ = \_\ @ u1_\" + using LTS_\.\_exp_split'[of u_\ \ u1] II(2) III(1) by auto + then obtain \_\ u1_\ where "LTS_\.\_exp \_\ [\] \ LTS_\.\_exp u1_\ u1 \ u_\ = \_\ @ u1_\" + by auto + then have "(Init p'', \_\@u1_\ , q) \ LTS.trans_star A'" + using II(3) by auto + then show ?thesis + using \LTS_\.\_exp \_\ [\] \ LTS_\.\_exp u1_\ u1 \ u_\ = \_\ @ u1_\\ by blast + qed + then obtain \_\ u1_\ where + iii: "LTS_\.\_exp \_\ [\]" and + iv: "LTS_\.\_exp u1_\ u1" "(Init p'', \_\@u1_\, q) \ LTS.trans_star A'" + by blast + then have VI: "\q1. (Init p'', \_\, q1) \ LTS.trans_star A' \ (q1, u1_\, q) \ LTS.trans_star A'" + by (simp add: LTS.trans_star_split) + then obtain q1 where VI: "(Init p'', \_\, q1) \ LTS.trans_star A'" "(q1, u1_\, q) \ LTS.trans_star A'" + by blast + + then have VI_2: "(Init p'', [\], q1) \ LTS_\.trans_star_\ A'" "(q1, u1, q) \ LTS_\.trans_star_\ A'" + by (meson LTS_\.trans_star_\_iff_\_exp_trans_star iii VI(2) iv(1))+ + + show ?case + proof (cases w1) + case pop + then have r: "(p'', \) \ (p', pop)" + using III(3) by blast + then have "(Init p', \, q1) \ A'" + using VI_2(1) add_trans_pop assms saturated_def saturation_def p'_inits by metis + then have "(Init p', w, q) \ LTS_\.trans_star_\ A'" + using III(2) VI_2(2) pop LTS_\.trans_star_\.trans_star_\_step_\ by fastforce + then have "accepts_\ A' (p', w)" + unfolding accepts_\_def using II(1) by blast + then show ?thesis + using p'_def w_def by force + next + case (swap \') + then have r: "(p'', \) \ (p', swap \')" + using III(3) by blast + then have "(Init p', Some \', q1) \ A'" + by (metis VI_2(1) add_trans_swap assms(3) saturated_def saturation_def) + have "(Init p', w, q) \ LTS_\.trans_star_\ A'" + using III(2) LTS_\.trans_star_\.trans_star_\_step_\ VI_2(2) append_Cons append_self_conv2 + lbl.simps(3) swap \(Init p', Some \', q1) \ A'\ by fastforce + then have "accepts_\ A' (p', w)" + unfolding accepts_\_def + using II(1) by blast + then show ?thesis + using p'_def w_def by force + next + case (push \' \'') + then have r: "(p'', \) \ (p', push \' \'')" + using III(3) by blast + from this VI_2 iii post_star_rules.intros(3)[OF this, of q1 A', OF VI_2(1)] + have "(Init p', Some \', Isolated p' \') \ A'" + using assms(3) by (meson saturated_def saturation_def) + from this r VI_2 iii post_star_rules.intros(4)[OF r, of q1 A', OF VI_2(1)] + have "(Isolated p' \', Some \'', q1) \ A'" + using assms(3) using saturated_def saturation_def by metis + have "(Init p', [\'], Isolated p' \') \ LTS_\.trans_star_\ A' \ + (Isolated p' \', [\''], q1) \ LTS_\.trans_star_\ A' \ + (q1, u1, q) \ LTS_\.trans_star_\ A'" + by (metis LTS_\.trans_star_\.simps VI_2(2) \(Init p', Some \', Isolated p' \') \ A'\ + \(Isolated p' \', Some \'', q1) \ A'\) + have "(Init p', w, q) \ LTS_\.trans_star_\ A'" + using III(2) VI_2(2) \(Init p', Some \', Isolated p' \') \ A'\ + \(Isolated p' \', Some \'', q1) \ A'\ push LTS_\.append_edge_edge_trans_star_\ by auto + then have "accepts_\ A' (p', w)" + unfolding accepts_\_def + using II(1) by blast + then show ?thesis + using p'_def w_def by force + + qed +qed + +lemma lemma_3_3: + assumes "(p,v) \\<^sup>* (p',w)" + and "(p, v) \ lang_\ A" + and "saturation post_star_rules A A'" + shows "accepts_\ A' (p', w)" + using assms lemma_3_3' by force + +lemma init_only_hd: + assumes "(ss, w) \ LTS.path_with_word A" + assumes "inits \ LTS.srcs A" + assumes "count (transitions_of (ss, w)) t > 0" + assumes "t = (Init p1, \, q1)" + shows "hd (transition_list (ss, w)) = t \ count (transitions_of (ss, w)) t = 1" + using assms LTS.source_only_hd by (metis LTS.srcs_def2 inits_srcs_iff_Ctr_Loc_srcs) + +lemma no_edge_to_Ctr_Loc_avoid_Ctr_Loc: + assumes "(p, w, qq) \ LTS.trans_star Aiminus1" + assumes "w \ []" + assumes "inits \ LTS.srcs Aiminus1" + shows "qq \ inits" + using assms LTS.no_end_in_source by (metis subset_iff) + +lemma no_edge_to_Ctr_Loc_avoid_Ctr_Loc_\: + assumes "(p, [\], qq) \ LTS_\.trans_star_\ Aiminus1" + assumes "inits \ LTS.srcs Aiminus1" + shows "qq \ inits" + using assms LTS_\.no_edge_to_source_\ by (metis subset_iff) + +lemma no_edge_to_Ctr_Loc_post_star_rules': + assumes "post_star_rules\<^sup>*\<^sup>* A Ai" + assumes "\q \ q'. (q, \, Init q') \ A" + shows "\q \ q'. (q, \, Init q') \ Ai" +using assms +proof (induction rule: rtranclp_induct) + case base + then show ?case by auto +next + case (step Aiminus1 Ai) + then have ind: "\q \ q'. (q, \, Init q') \ Aiminus1" + by auto + from step(2) show ?case + proof (cases rule: post_star_rules.cases) + case (add_trans_pop p \ p' q) + have "q \ inits" + using ind no_edge_to_Ctr_Loc_avoid_Ctr_Loc_\ inits_srcs_iff_Ctr_Loc_srcs + by (metis local.add_trans_pop(3)) + then have "\qq. q = Init qq" + by (simp add: inits_def is_Init_def) + then show ?thesis + using ind local.add_trans_pop(1) by auto + next + case (add_trans_swap p \ p' \' q) + have "q \ inits" + using add_trans_swap ind no_edge_to_Ctr_Loc_avoid_Ctr_Loc_\ inits_srcs_iff_Ctr_Loc_srcs + by metis + then have "\qq. q = Init qq" + by (simp add: inits_def is_Init_def) + then show ?thesis + using ind local.add_trans_swap(1) by auto + next + case (add_trans_push_1 p \ p' \' \'' q) + have "q \ inits" + using add_trans_push_1 ind no_edge_to_Ctr_Loc_avoid_Ctr_Loc_\ inits_srcs_iff_Ctr_Loc_srcs + by metis + then have "\qq. q = Init qq" + by (simp add: inits_def is_Init_def) + then show ?thesis + using ind local.add_trans_push_1(1) by auto + next + case (add_trans_push_2 p \ p' \' \'' q) + have "q \ inits" + using add_trans_push_2 ind no_edge_to_Ctr_Loc_avoid_Ctr_Loc_\ inits_srcs_iff_Ctr_Loc_srcs + by metis + then have "\qq. q = Init qq" + by (simp add: inits_def is_Init_def) + then show ?thesis + using ind local.add_trans_push_2(1) by auto + qed +qed + +lemma no_edge_to_Ctr_Loc_post_star_rules: + assumes "post_star_rules\<^sup>*\<^sup>* A Ai" + assumes "inits \ LTS.srcs A" + shows "inits \ LTS.srcs Ai" + using assms no_edge_to_Ctr_Loc_post_star_rules' inits_srcs_iff_Ctr_Loc_srcs by metis + +lemma source_and_sink_isolated: + assumes "N \ LTS.srcs A" + assumes "N \ LTS.sinks A" + shows "\p \ q. (p, \, q) \ A \ p \ N \ q \ N" + by (metis LTS.srcs_def2 LTS.sinks_def2 assms(1) assms(2) in_mono) + +lemma post_star_rules_Isolated_source_invariant': + assumes "post_star_rules\<^sup>*\<^sup>* A A'" + assumes "isols \ LTS.isolated A" + assumes "(Init p', Some \', Isolated p' \') \ A'" + shows "\p \. (p, \, Isolated p' \') \ A'" + using assms +proof (induction rule: rtranclp_induct) + case base + then show ?case + unfolding isols_def is_Isolated_def using LTS.isolated_no_edges by fastforce +next + case (step Aiminus1 Ai) + from step(2) show ?case + proof (cases rule: post_star_rules.cases) + case (add_trans_pop p''' \'' p'' q) + then have "(Init p', Some \', Isolated p' \') \ Ai" + using step.prems(2) by blast + then have nin: "\p \. (p, \, Isolated p' \') \ Aiminus1" + using local.add_trans_pop(1) step.IH step.prems(1,2) by fastforce + then have "Isolated p' \' \ q" + using add_trans_pop(4) LTS_\.trans_star_not_to_source_\ LTS.srcs_def2 + by (metis local.add_trans_pop(3) state.distinct(3)) + then have "\p \. (p, \, Isolated p' \') = (Init p'', \, q)" + by auto + then show ?thesis + using nin add_trans_pop(1) by auto + next + case (add_trans_swap p'''' \'' p'' \''' q) + then have "(Init p', Some \', Isolated p' \') \ Ai" + using step.prems(2) by blast + then have nin: "\p \. (p, \, Isolated p' \') \ Aiminus1" + using local.add_trans_swap(1) step.IH step.prems(1,2) by fastforce + then have "Isolated p' \' \ q" + using LTS.srcs_def2 + by (metis state.distinct(4) LTS_\.trans_star_not_to_source_\ local.add_trans_swap(3)) + then have "\p \. (p, \, Isolated p' \') = (Init p'', Some \''', q)" + by auto + then show ?thesis + using nin add_trans_swap(1) by auto + next + case (add_trans_push_1 p'''' \'' p'' \''' \''''' q) + then have "(Init p', Some \', Isolated p' \') \ Ai" + using step.prems(2) by blast + then show ?thesis + using add_trans_push_1(1) Un_iff state.inject(2) prod.inject singleton_iff step.IH + step.prems(1,2) by blast + next + case (add_trans_push_2 p'''' \'' p'' \''' \'''' q) + have "(Init p', Some \', Isolated p' \') \ Ai" + using step.prems(2) . + then have nin: "\p \. (p, \, Isolated p' \') \ Aiminus1" + using local.add_trans_push_2(1) step.IH step.prems(1) by fastforce + then have "Isolated p' \' \ q" + using LTS.srcs_def2 local.add_trans_push_2(3) + by (metis state.disc(1,3) LTS_\.trans_star_not_to_source_\) + then have "\p \. (p, \, Isolated p' \') = (Init p'', \, q)" + by auto + then show ?thesis + using nin add_trans_push_2(1) by auto + qed +qed + +lemma post_star_rules_Isolated_source_invariant: + assumes "post_star_rules\<^sup>*\<^sup>* A A'" + assumes "isols \ LTS.isolated A" + assumes "(Init p', Some \', Isolated p' \') \ A'" + shows "Isolated p' \' \ LTS.srcs A'" + by (meson LTS.srcs_def2 assms(1) assms(2) assms(3) post_star_rules_Isolated_source_invariant') + +lemma post_star_rules_Isolated_sink_invariant': + assumes "post_star_rules\<^sup>*\<^sup>* A A'" + assumes "isols \ LTS.isolated A" + assumes "(Init p', Some \', Isolated p' \') \ A'" + shows "\p \. (Isolated p' \', \, p) \ A'" + using assms +proof (induction rule: rtranclp_induct) + case base + then show ?case + unfolding isols_def is_Isolated_def + using LTS.isolated_no_edges by fastforce +next + case (step Aiminus1 Ai) + from step(2) show ?case + proof (cases rule: post_star_rules.cases) + case (add_trans_pop p''' \'' p'' q) + then have "(Init p', Some \', Isolated p' \') \ Ai" + using step.prems(2) by blast + then have nin: "\p \. (Isolated p' \', \, p) \ Aiminus1" + using local.add_trans_pop(1) step.IH step.prems(1,2) by fastforce + then have "Isolated p' \' \ q" + using add_trans_pop(4) + LTS_\.trans_star_not_to_source_\[of "Init p'''" "[\'']" q Aiminus1 "Isolated p' \'"] + post_star_rules_Isolated_source_invariant local.add_trans_pop(1) step.hyps(1) step.prems(1,2) + UnI1 local.add_trans_pop(3) by (metis (full_types) state.distinct(3)) + then have "\p \. (p, \, Isolated p' \') = (Init p'', \, q)" + by auto + then show ?thesis + using nin add_trans_pop(1) by auto + next + case (add_trans_swap p'''' \'' p'' \''' q) + then have "(Init p', Some \', Isolated p' \') \ Ai" + using step.prems(2) by blast + then have nin: "\p \. (Isolated p' \', \, p) \ Aiminus1" + using local.add_trans_swap(1) step.IH step.prems(1,2) by fastforce + then have "Isolated p' \' \ q" + using LTS_\.trans_star_not_to_source_\[of "Init p''''" "[\'']" q Aiminus1] + local.add_trans_swap(3) post_star_rules_Isolated_source_invariant[of _ Aiminus1 p' \'] UnCI + local.add_trans_swap(1) step.hyps(1) step.prems(1,2) state.simps(7) by metis + then have "\p \. (p, \, Isolated p' \') = (Init p'', Some \''', q)" + by auto + then show ?thesis + using nin add_trans_swap(1) by auto + next + case (add_trans_push_1 p'''' \'' p'' \''' \''''' q) + then have "(Init p', Some \', Isolated p' \') \ Ai" + using step.prems(2) by blast + then show ?thesis + using add_trans_push_1(1) Un_iff state.inject prod.inject singleton_iff step.IH + step.prems(1,2) by blast + next + case (add_trans_push_2 p'''' \'' p'' \''' \'''' q) + have "(Init p', Some \', Isolated p' \') \ Ai" + using step.prems(2) by blast + then have nin: "\p \. (Isolated p' \', \, p) \ Aiminus1" + using local.add_trans_push_2(1) step.IH step.prems(1,2) by fastforce + then have "Isolated p' \' \ q" + using state.disc(3) + LTS_\.trans_star_not_to_source_\[of "Init p''''" "[\'']" q Aiminus1 "Isolated p' \'"] + local.add_trans_push_2(3) + using post_star_rules_Isolated_source_invariant[of _ Aiminus1 p' \'] UnCI + local.add_trans_push_2(1) step.hyps(1) step.prems(1,2) state.disc(1) by metis + then have "\p \. (Isolated p' \', \, p) = (Init p'', \, q)" + by auto + then show ?thesis + using nin add_trans_push_2(1) + using local.add_trans_push_2 step.prems(2) by auto + qed +qed + +lemma post_star_rules_Isolated_sink_invariant: + assumes "post_star_rules\<^sup>*\<^sup>* A A'" + assumes "isols \ LTS.isolated A" + assumes "(Init p', Some \', Isolated p' \') \ A'" + shows "Isolated p' \' \ LTS.sinks A'" + by (meson LTS.sinks_def2 assms(1,2,3) post_star_rules_Isolated_sink_invariant') + + +\ \Corresponds to Schwoon's lemma 3.4\ +lemma rtranclp_post_star_rules_constains_successors_states: + assumes "post_star_rules\<^sup>*\<^sup>* A A'" + assumes "inits \ LTS.srcs A" + assumes "isols \ LTS.isolated A" + assumes "(Init p, w, ss, q) \ LTS.trans_star_states A'" + shows "(\is_Isolated q \ (\p' w'. (Init p', w', q) \ LTS_\.trans_star_\ A \ (p',w') \\<^sup>* (p, LTS_\.remove_\ w))) \ + (is_Isolated q \ (the_Ctr_Loc q, [the_Label q]) \\<^sup>* (p, LTS_\.remove_\ w))" + using assms +proof (induction arbitrary: p q w ss rule: rtranclp_induct) + case base + { + assume ctr_loc: "is_Init q \ is_Noninit q" + then have "(Init p, LTS_\.remove_\ w, q) \ LTS_\.trans_star_\ A" + using base LTS_\.trans_star_states_trans_star_\ by metis + then have "\p' w'. (p', w', q) \ LTS_\.trans_star_\ A" + by auto + then have ?case + using ctr_loc \(Init p, LTS_\.remove_\ w, q) \ LTS_\.trans_star_\ A\ by blast + } + moreover + { + assume "is_Isolated q" + then have ?case + proof (cases w) + case Nil + then have False using base + using LTS.trans_star_empty LTS.trans_star_states_trans_star \is_Isolated q\ + by (metis state.disc(7)) + then show ?thesis + by metis + next + case (Cons \ w_rest) + then have "(Init p, \#w_rest, ss, q) \ LTS.trans_star_states A" + using base Cons by blast + then have "\s \'. (s, \', q) \ A" + using LTS.trans_star_states_transition_relation by metis + then have False + using \is_Isolated q\ isols_def base.prems(2) LTS.isolated_no_edges + by (metis mem_Collect_eq subset_eq) + then show ?thesis + by auto + qed + } + ultimately + show ?case + by (meson state.exhaust_disc) +next + case (step Aiminus1 Ai) + from step(2) have "\p1 \ p2 w2 q1. Ai = Aiminus1 \ {(p1, \, q1)} \ (p1, \, q1) \ Aiminus1" + by (cases rule: post_star_rules.cases) auto + then obtain p1 \ q1 where p1_\_p2_w2_q'_p: + "Ai = Aiminus1 \ {(p1, \, q1)}" + "(p1, \, q1) \ Aiminus1" + by auto + + define t where "t = (p1, \, q1)" + define j where "j = count (transitions_of' (Init p, w, ss, q)) t" + + note ss_p = step(6) + + from j_def ss_p show ?case + proof (induction j arbitrary: p q w ss) + case 0 + then have "(Init p, w, ss, q) \ LTS.trans_star_states Aiminus1" + using count_zero_remove_path_with_word_trans_star_states p1_\_p2_w2_q'_p(1) t_def + by metis + then show ?case + using step by auto + next + case (Suc j) + from step(2) show ?case + proof (cases rule: post_star_rules.cases) + case (add_trans_pop p2 \2 p1 q1) (* Note: p1 shadows p1 from above. q1 shadows q1 from above. *) + note III = add_trans_pop(3) + note VI = add_trans_pop(2) + have t_def: "t = (Init p1, \, q1)" + using local.add_trans_pop(1) local.add_trans_pop p1_\_p2_w2_q'_p(1) t_def by blast + have init_Ai: "inits \ LTS.srcs Ai" + using step(1,2) step(4) + using no_edge_to_Ctr_Loc_post_star_rules + using r_into_rtranclp by (metis) + have t_hd_once: "hd (transition_list (ss, w)) = t \ count (transitions_of (ss, w)) t = 1" + proof - + have "(ss, w) \ LTS.path_with_word Ai" + using Suc(3) LTS.trans_star_states_path_with_word by metis + moreover + have "inits \ LTS.srcs Ai" + using init_Ai by auto + moreover + have "0 < count (transitions_of (ss, w)) t" + by (metis Suc.prems(1) transitions_of'.simps zero_less_Suc) + moreover + have "t = (Init p1, \, q1)" + using t_def by auto + moreover + have "Init p1 \ inits" + by (simp add: inits_def) + ultimately + show "hd (transition_list (ss, w)) = t \ count (transitions_of (ss, w)) t = 1" + using init_only_hd[of ss w Ai t p1 \ q1] by auto + qed + + have "transition_list (ss, w) \ []" + by (metis LTS.trans_star_states_path_with_word LTS.path_with_word.simps Suc.prems(1) + Suc.prems(2) count_empty less_not_refl2 list.distinct(1) transition_list.simps(1) + transitions_of'.simps transitions_of.simps(2) zero_less_Suc) + then have ss_w_split: "([Init p1,q1], [\]) @\ (tl ss, tl w) = (ss, w)" + using t_hd_once t_def hd_transition_list_append_path_with_word by metis + then have ss_w_split': "(Init p1, [\], [Init p1,q1], q1) @@\ (q1, tl w, tl ss, q) = (Init p1, w, ss, q)" + by auto + have VII: "p = p1" + proof - + have "(Init p, w, ss, q) \ LTS.trans_star_states Ai" + using Suc.prems(2) by blast + moreover + have "t = hd (transition_list' (Init p, w, ss, q))" + using \hd (transition_list (ss, w)) = t \ count (transitions_of (ss, w)) t = 1\ + by fastforce + moreover + have "transition_list' (Init p, w, ss, q) \ []" + by (simp add: \transition_list (ss, w) \ []\) + moreover + have "t = (Init p1, \, q1)" + using t_def by auto + ultimately + show "p = p1" + using LTS.hd_is_hd by fastforce + qed + have "j=0" + using Suc(2) \hd (transition_list (ss, w)) = t \ count (transitions_of (ss, w)) t = 1\ + by force + have "(Init p1, [\], [Init p1, q1], q1) \ LTS.trans_star_states Ai" + proof - + have "(Init p1, \, q1) \ Ai" + using local.add_trans_pop(1) by auto + moreover + have "(Init p1, \, q1) \ Aiminus1" + by (simp add: local.add_trans_pop) + ultimately + show "(Init p1, [\], [Init p1, q1], q1) \ LTS.trans_star_states Ai" + by (meson LTS.trans_star_states.trans_star_states_refl + LTS.trans_star_states.trans_star_states_step) + qed + have "(q1, tl w, tl ss, q) \ LTS.trans_star_states Aiminus1" + proof - + from Suc(3) have "(ss, w) \ LTS.path_with_word Ai" + by (meson LTS.trans_star_states_path_with_word) + then have tl_ss_w_Ai: "(tl ss, tl w) \ LTS.path_with_word Ai" + by (metis LTS.path_with_word.simps \transition_list (ss, w) \ []\ list.sel(3) + transition_list.simps(2)) + from t_hd_once have zero_p1_\_q1: "0 = count (transitions_of (tl ss, tl w)) (Init p1, \, q1)" + using count_append_path_with_word_\[of "[hd ss]" "[]" "tl ss" "hd w" "tl w" "Init p1" \ q1, simplified] + \(Init p1, [\], [Init p1, q1], q1) \ LTS.trans_star_states Ai\ + \transition_list (ss, w) \ []\ Suc.prems(2) VII + LTS.transition_list_Cons[of "Init p" w ss q Ai \ q1] by (auto simp: t_def) + have Ai_Aiminus1: "Ai = Aiminus1 \ {(Init p1, \, q1)}" + using local.add_trans_pop(1) by auto + from t_hd_once tl_ss_w_Ai zero_p1_\_q1 Ai_Aiminus1 + count_zero_remove_path_with_word[OF tl_ss_w_Ai, of "Init p1" \ q1 Aiminus1] + have "(tl ss, tl w) \ LTS.path_with_word Aiminus1" + by auto + moreover + have "hd (tl ss) = q1" + using Suc.prems(2) VII \transition_list (ss, w) \ []\ t_def + LTS.transition_list_Cons t_hd_once by fastforce + moreover + have "last ss = q" + by (metis LTS.trans_star_states_last Suc.prems(2)) + ultimately + show "(q1, tl w, tl ss, q) \ LTS.trans_star_states Aiminus1" + by (metis (no_types, lifting) LTS.trans_star_states_path_with_word + LTS.path_with_word_trans_star_states LTS.path_with_word_not_empty Suc.prems(2) + last_ConsR list.collapse) + qed + have "w = \ # (tl w)" + by (metis Suc(3) VII \transition_list (ss, w) \ []\ list.distinct(1) list.exhaust_sel + list.sel(1) t_def LTS.transition_list_Cons t_hd_once) + then have w_tl_\: "LTS_\.remove_\ w = LTS_\.remove_\ (tl w)" + by (metis LTS_\.remove_\_def removeAll.simps(2)) + + have "\\2'. LTS_\.\_exp \2' [\2] \ (Init p2, \2', q1) \ LTS.trans_star Aiminus1" + using add_trans_pop + by (simp add: LTS_\.trans_star_\_\_exp_trans_star) + then obtain \2' where "LTS_\.\_exp \2' [\2] \ (Init p2, \2', q1) \ LTS.trans_star Aiminus1" + by blast + then have "\ss2. (Init p2, \2', ss2, q1) \ LTS.trans_star_states Aiminus1" + by (simp add: LTS.trans_star_trans_star_states) + then obtain ss2 where IIII_1: "(Init p2, \2', ss2, q1) \ LTS.trans_star_states Aiminus1" + by blast + have IIII_2: "(q1, tl w, tl ss, q) \ LTS.trans_star_states Aiminus1" + using ss_w_split' Suc(3) Suc(2) \j=0\ + using \(q1, tl w, tl ss, q) \ LTS.trans_star_states Aiminus1\ by blast + have IIII: "(Init p2, \2' @ tl w, ss2 @ (tl (tl ss)), q) \ LTS.trans_star_states Aiminus1" + using IIII_1 IIII_2 by (meson LTS.trans_star_states_append) + + from Suc(1)[of p2 "\2' @ tl w" "ss2 @ (tl (tl ss))" q] + have V: "(\is_Isolated q \ + (\p' w'. (Init p', w', q) \ LTS_\.trans_star_\ A \ (p', w') \\<^sup>* (p2, LTS_\.remove_\ (\2' @ tl w)))) \ + (is_Isolated q \ (the_Ctr_Loc q, [the_Label q]) \\<^sup>* (p2, LTS_\.remove_\ (\2' @ tl w)))" + using IIII + using step.IH step.prems(1,2,3) by blast + + have "\is_Isolated q \ is_Isolated q" + using state.exhaust_disc by blast + then show ?thesis + proof + assume ctr_q: "\is_Isolated q" + then have "\p' w'. (Init p', w', q) \ LTS_\.trans_star_\ A \ (p', w') \\<^sup>* (p2, LTS_\.remove_\ (\2' @ tl w))" + using V by auto + then obtain p' w' where + VIII:"(Init p', w', q) \ LTS_\.trans_star_\ A" and steps: "(p', w') \\<^sup>* (p2, LTS_\.remove_\ (\2' @ tl w))" + by blast + then have "(p',w') \\<^sup>* (p2, LTS_\.remove_\ (\2' @ tl w)) \ + (p2, LTS_\.remove_\ (\2' @ tl w)) \\<^sup>* (p, LTS_\.remove_\ (tl w))" + proof - + have \2'_\2: "LTS_\.remove_\ \2' = [\2]" + by (metis LTS_\.\_exp_def LTS_\.remove_\_def \LTS_\.\_exp \2' [\2] \ (Init p2, \2', q1) \ LTS.trans_star Aiminus1\) + have "(p',w') \\<^sup>* (p2, LTS_\.remove_\ (\2' @ tl w))" + using steps by auto + moreover + have rule: "(p2, \2) \ (p, pop)" + using VI VII by auto + from steps have steps': "(p', w') \\<^sup>* (p2, \2 # (LTS_\.remove_\ (tl w)))" + using \2'_\2 + by (metis Cons_eq_appendI LTS_\.remove_\_append_dist self_append_conv2) + from rule steps' have "(p2, \2 # (LTS_\.remove_\ (tl w))) \\<^sup>* (p, LTS_\.remove_\ (tl w))" + using VIII + by (metis PDS.transition_rel.intros append_self_conv2 lbl.simps(1) r_into_rtranclp + step_relp_def) (* VII *) + then have "(p2, LTS_\.remove_\ (\2' @ tl w)) \\<^sup>* (p, LTS_\.remove_\ (tl w))" + by (simp add: LTS_\.remove_\_append_dist \2'_\2) + ultimately + show "(p',w') \\<^sup>* (p2, LTS_\.remove_\ (\2' @ tl w)) \ + (p2, LTS_\.remove_\ (\2' @ tl w)) \\<^sup>* (p, LTS_\.remove_\ (tl w))" + by auto + qed + then have "(p',w') \\<^sup>* (p, LTS_\.remove_\ (tl w)) \ (Init p', w', q) \ LTS_\.trans_star_\ A" + using VIII by force + then have "\p' w'. (Init p', w', q) \ LTS_\.trans_star_\ A \ (p', w') \\<^sup>* (p, LTS_\.remove_\ w)" + using w_tl_\ by auto + then show ?thesis + using ctr_q \p = p1\ by blast + next + assume "is_Isolated q" + from V have "(the_Ctr_Loc q, [the_Label q]) \\<^sup>* (p2, \2#(LTS_\.remove_\ w))" + by (metis LTS_\.\_exp_def LTS_\.remove_\_append_dist LTS_\.remove_\_def + \LTS_\.\_exp \2' [\2] \ (Init p2, \2', q1) \ LTS.trans_star Aiminus1\ \is_Isolated q\ + append_Cons append_self_conv2 w_tl_\) + + then have "(the_Ctr_Loc q, [the_Label q]) \\<^sup>* (p1, LTS_\.remove_\ w)" + using VI by (metis append_Nil lbl.simps(1) rtranclp.simps step_relp_def2) + then have "(the_Ctr_Loc q, [the_Label q]) \\<^sup>* (p, LTS_\.remove_\ w)" + using VII by auto + then show ?thesis + using \is_Isolated q\ by blast + qed + next + case (add_trans_swap p2 \2 p1 \' q1) (* Adjusted from previous case *) + note III = add_trans_swap(3) + note VI = add_trans_swap(2) + have t_def: "t = (Init p1, Some \', q1)" + using local.add_trans_swap(1) local.add_trans_swap p1_\_p2_w2_q'_p(1) t_def by blast + have init_Ai: "inits \ LTS.srcs Ai" + using step(1,2,4) no_edge_to_Ctr_Loc_post_star_rules by (meson r_into_rtranclp) + have t_hd_once: "hd (transition_list (ss, w)) = t \ count (transitions_of (ss, w)) t = 1" + proof - + have "(ss, w) \ LTS.path_with_word Ai" + using Suc(3) LTS.trans_star_states_path_with_word by metis + moreover + have "inits \ LTS.srcs Ai" + using init_Ai by auto + moreover + have "0 < count (transitions_of (ss, w)) t" + by (metis Suc.prems(1) transitions_of'.simps zero_less_Suc) + moreover + have "t = (Init p1, Some \', q1)" + using t_def + by auto + moreover + have "Init p1 \ inits" + using inits_def by force + ultimately + show "hd (transition_list (ss, w)) = t \ count (transitions_of (ss, w)) t = 1" + using init_only_hd[of ss w Ai t p1 _ q1] by auto + qed + + have "transition_list (ss, w) \ []" + by (metis LTS.trans_star_states_path_with_word LTS.path_with_word.simps Suc.prems(1,2) + count_empty less_not_refl2 list.distinct(1) transition_list.simps(1) transitions_of'.simps + transitions_of.simps(2) zero_less_Suc) + then have ss_w_split: "([Init p1,q1], [Some \']) @\ (tl ss, tl w) = (ss, w)" + using t_hd_once t_def hd_transition_list_append_path_with_word by metis + then have ss_w_split': "(Init p1, [Some \'], [Init p1,q1], q1) @@\ (q1, tl w, tl ss, q) = (Init p1, w, ss, q)" + by auto + have VII: "p = p1" + proof - + have "(Init p, w, ss, q) \ LTS.trans_star_states Ai" + using Suc.prems(2) by blast + moreover + have "t = hd (transition_list' (Init p, w, ss, q))" + using \hd (transition_list (ss, w)) = t \ count (transitions_of (ss, w)) t = 1\ by fastforce + moreover + have "transition_list' (Init p, w, ss, q) \ []" + by (simp add: \transition_list (ss, w) \ []\) + moreover + have "t = (Init p1, Some \', q1)" + using t_def by auto + ultimately + show "p = p1" + using LTS.hd_is_hd by fastforce + qed + have "j=0" + using Suc(2) \hd (transition_list (ss, w)) = t \ count (transitions_of (ss, w)) t = 1\ by force + have "(Init p1, [Some \'], [Init p1, q1], q1) \ LTS.trans_star_states Ai" + proof - + have "(Init p1, Some \', q1) \ Ai" + using local.add_trans_swap(1) by auto + moreover + have "(Init p1, Some \', q1) \ Aiminus1" + using local.add_trans_swap(4) by blast + ultimately + show "(Init p1, [Some \'], [Init p1, q1], q1) \ LTS.trans_star_states Ai" + by (meson LTS.trans_star_states.trans_star_states_refl LTS.trans_star_states.trans_star_states_step) + qed + have "(q1, tl w, tl ss, q) \ LTS.trans_star_states Aiminus1" + proof - + from Suc(3) have "(ss, w) \ LTS.path_with_word Ai" + by (meson LTS.trans_star_states_path_with_word) + then have tl_ss_w_Ai: "(tl ss, tl w) \ LTS.path_with_word Ai" + by (metis LTS.path_with_word.simps \transition_list (ss, w) \ []\ list.sel(3) + transition_list.simps(2)) + from t_hd_once have zero_p1_\_q1: "0 = count (transitions_of (tl ss, tl w)) (Init p1, Some \', q1)" + using count_append_path_with_word_\[of "[hd ss]" "[]" "tl ss" "hd w" "tl w" "Init p1" "Some \'" q1, simplified] + \(Init p1, [Some \'], [Init p1, q1], q1) \ LTS.trans_star_states Ai\ \transition_list (ss, w) \ []\ + Suc.prems(2) VII LTS.transition_list_Cons[of "Init p" w ss q Ai "Some \'" q1] + by (auto simp: t_def) + have Ai_Aiminus1: "Ai = Aiminus1 \ {(Init p1, Some \', q1)}" + using local.add_trans_swap(1) by auto + from t_hd_once tl_ss_w_Ai zero_p1_\_q1 Ai_Aiminus1 + count_zero_remove_path_with_word[OF tl_ss_w_Ai, of "Init p1" _ q1 Aiminus1] + have "(tl ss, tl w) \ LTS.path_with_word Aiminus1" + by auto + moreover + have "hd (tl ss) = q1" + using Suc.prems(2) VII \transition_list (ss, w) \ []\ t_def LTS.transition_list_Cons t_hd_once by fastforce + moreover + have "last ss = q" + by (metis LTS.trans_star_states_last Suc.prems(2)) + ultimately + show "(q1, tl w, tl ss, q) \ LTS.trans_star_states Aiminus1" + by (metis (no_types, lifting) LTS.trans_star_states_path_with_word + LTS.path_with_word_trans_star_states LTS.path_with_word_not_empty Suc.prems(2) + last_ConsR list.collapse) + qed + have "w = Some \' # (tl w)" + by (metis Suc(3) VII \transition_list (ss, w) \ []\ list.distinct(1) list.exhaust_sel + list.sel(1) t_def LTS.transition_list_Cons t_hd_once) + then have w_tl_\: "LTS_\.remove_\ w = LTS_\.remove_\ (Some \'#tl w)" + using LTS_\.remove_\_def removeAll.simps(2) + by presburger + have "\\2'. LTS_\.\_exp \2' [\2] \ (Init p2, \2', q1) \ LTS.trans_star Aiminus1" + using add_trans_swap by (simp add: LTS_\.trans_star_\_\_exp_trans_star) + then obtain \2' where "LTS_\.\_exp \2' [\2] \ (Init p2, \2', q1) \ LTS.trans_star Aiminus1" + by blast + then have "\ss2. (Init p2, \2', ss2, q1) \ LTS.trans_star_states Aiminus1" + by (simp add: LTS.trans_star_trans_star_states) + then obtain ss2 where IIII_1: "(Init p2, \2', ss2, q1) \ LTS.trans_star_states Aiminus1" + by blast + have IIII_2: "(q1, tl w, tl ss, q) \ LTS.trans_star_states Aiminus1" + using ss_w_split' Suc(3) Suc(2) \j=0\ + using \(q1, tl w, tl ss, q) \ LTS.trans_star_states Aiminus1\ by blast + have IIII: "(Init p2, \2' @ tl w, ss2 @ (tl (tl ss)), q) \ LTS.trans_star_states Aiminus1" + using IIII_1 IIII_2 by (meson LTS.trans_star_states_append) + + from Suc(1)[of p2 "\2' @ tl w" "ss2 @ (tl (tl ss))" q] + have V: "(\is_Isolated q \ + (\p' w'. (Init p', w', q) \ LTS_\.trans_star_\ A \ (p', w') \\<^sup>* (p2, LTS_\.remove_\ (\2' @ tl w)))) \ + (is_Isolated q \ (the_Ctr_Loc q, [the_Label q]) \\<^sup>* (p2, LTS_\.remove_\ (\2' @ tl w)))" + using IIII + using step.IH step.prems(1,2,3) by blast + + have "\is_Isolated q \ is_Isolated q" + using state.exhaust_disc by blast + then show ?thesis + proof + assume ctr_q: "\is_Isolated q" + then have "\p' w'. (Init p', w', q) \ LTS_\.trans_star_\ A \ (p', w') \\<^sup>* (p2, LTS_\.remove_\ (\2' @ tl w))" + using V by auto + then obtain p' w' where + VIII:"(Init p', w', q) \ LTS_\.trans_star_\ A" and steps: "(p', w') \\<^sup>* (p2, LTS_\.remove_\ (\2' @ tl w))" + by blast + then have "(p',w') \\<^sup>* (p2, LTS_\.remove_\ (\2' @ tl w)) \ + (p2, LTS_\.remove_\ (\2' @ tl w)) \\<^sup>* (p, \' # LTS_\.remove_\ (tl w))" + proof - + have \2'_\2: "LTS_\.remove_\ \2' = [\2]" + by (metis LTS_\.\_exp_def LTS_\.remove_\_def \LTS_\.\_exp \2' [\2] \ (Init p2, \2', q1) \ LTS.trans_star Aiminus1\) + have "(p',w') \\<^sup>* (p2, LTS_\.remove_\ (\2' @ tl w))" + using steps by auto + moreover + have rule: "(p2, \2) \ (p, swap \')" + using VI VII by auto + from steps have steps': "(p', w') \\<^sup>* (p2, \2 # (LTS_\.remove_\ (tl w)))" + using \2'_\2 + by (metis Cons_eq_appendI LTS_\.remove_\_append_dist self_append_conv2) + from rule steps' have "(p2, \2 # (LTS_\.remove_\ (tl w))) \\<^sup>* (p, \' # LTS_\.remove_\ (tl w))" + using VIII + using PDS.transition_rel.intros append_self_conv2 lbl.simps(1) r_into_rtranclp step_relp_def + by fastforce + then have "(p2, LTS_\.remove_\ (\2' @ tl w)) \\<^sup>* (p, \' # LTS_\.remove_\ (tl w))" + by (simp add: LTS_\.remove_\_append_dist \2'_\2) + ultimately + show "(p',w') \\<^sup>* (p2, LTS_\.remove_\ (\2' @ tl w)) \ + (p2, LTS_\.remove_\ (\2' @ tl w)) \\<^sup>* (p, \' # LTS_\.remove_\ (tl w))" + by auto + qed + then have "(p',w') \\<^sup>* (p, \' # LTS_\.remove_\ (tl w)) \ (Init p', w', q) \ LTS_\.trans_star_\ A" + using VIII by force + then have "\p' w'. (Init p', w', q) \ LTS_\.trans_star_\ A \ (p', w') \\<^sup>* (p, LTS_\.remove_\ w)" + using LTS_\.remove_\_Cons_tl by (metis \w = Some \' # tl w\) + then show ?thesis + using ctr_q \p = p1\ by blast + next + assume "is_Isolated q" + from V this have "(the_Ctr_Loc q, [the_Label q]) \\<^sup>* (p2, LTS_\.remove_\ (\2' @ tl w))" + by auto + then have "(the_Ctr_Loc q, [the_Label q]) \\<^sup>* (p2, \2#(LTS_\.remove_\ (tl w)))" + by (metis LTS_\.\_exp_def LTS_\.remove_\_append_dist LTS_\.remove_\_def + \LTS_\.\_exp \2' [\2] \ (Init p2, \2', q1) \ LTS.trans_star Aiminus1\ append_Cons + append_self_conv2) + then have "(the_Ctr_Loc q, [the_Label q]) \\<^sup>* (p1, \' # LTS_\.remove_\ (tl w))" + using VI + by (metis (no_types) append_Cons append_Nil lbl.simps(2) rtranclp.rtrancl_into_rtrancl + step_relp_def2) + then have "(the_Ctr_Loc q, [the_Label q]) \\<^sup>* (p, \' # LTS_\.remove_\ (tl w))" + using VII by auto + then show ?thesis + using \is_Isolated q\ + by (metis LTS_\.remove_\_Cons_tl w_tl_\) + qed + next + case (add_trans_push_1 p2 \2 p1 \1 \'' q1') + then have t_def: "t = (Init p1, Some \1, Isolated p1 \1)" + using local.add_trans_pop(1) local.add_trans_pop p1_\_p2_w2_q'_p(1) t_def by blast + have init_Ai: "inits \ LTS.srcs Ai" + using step(1,2) step(4) + using no_edge_to_Ctr_Loc_post_star_rules + by (meson r_into_rtranclp) + have t_hd_once: "hd (transition_list (ss, w)) = t \ count (transitions_of (ss, w)) t = 1" + proof - + have "(ss, w) \ LTS.path_with_word Ai" + using Suc(3) LTS.trans_star_states_path_with_word by metis + moreover + have "inits \ LTS.srcs Ai" + using init_Ai by auto + moreover + have "0 < count (transitions_of (ss, w)) t" + by (metis Suc.prems(1) transitions_of'.simps zero_less_Suc) + moreover + have "t = (Init p1, Some \1, Isolated p1 \1)" + using t_def by auto + moreover + have "Init p1 \ inits" + using inits_def by fastforce + ultimately + show "hd (transition_list (ss, w)) = t \ count (transitions_of (ss, w)) t = 1" + using init_only_hd[of ss w Ai t] by auto + qed + have "transition_list (ss, w) \ []" + by (metis LTS.trans_star_states_path_with_word LTS.path_with_word.simps Suc.prems(1,2) + count_empty less_not_refl2 list.distinct(1) transition_list.simps(1) + transitions_of'.simps transitions_of.simps(2) zero_less_Suc) + + have VII: "p = p1" + proof - + have "(Init p, w, ss, q) \ LTS.trans_star_states Ai" + using Suc.prems(2) by blast + moreover + have "t = hd (transition_list' (Init p, w, ss, q))" + using \hd (transition_list (ss, w)) = t \ count (transitions_of (ss, w)) t = 1\ by fastforce + moreover + have "transition_list' (Init p, w, ss, q) \ []" + by (simp add: \transition_list (ss, w) \ []\) + moreover + have "t = (Init p1, Some \1, Isolated p1 \1)" + using t_def by auto + ultimately + show "p = p1" + using LTS.hd_is_hd by fastforce + qed + from add_trans_push_1(4) have "\p \. (Isolated p1 \1, \, p) \ Aiminus1" + using post_star_rules_Isolated_sink_invariant[of A Aiminus1 p1 \1] step.hyps(1) + step.prems(1,2,3) unfolding LTS.sinks_def by blast + then have "\p \. (Isolated p1 \1, \, p) \ Ai" + using local.add_trans_push_1(1) by blast + then have ss_w_short: "ss = [Init p1, Isolated p1 \1] \ w = [Some \1]" + using Suc.prems(2) VII \hd (transition_list (ss, w)) = t \ count (transitions_of (ss, w)) t = 1\ t_def + LTS.nothing_after_sink[of "Init p1" "Isolated p1 \1" "tl (tl ss)" "Some \1" "tl w" Ai] \transition_list (ss, w) \ []\ + LTS.trans_star_states_path_with_word[of "Init p" w ss q Ai] + LTS.transition_list_Cons[of "Init p" w ss q Ai] + by (auto simp: LTS.sinks_def2) + then have q_ext: "q = Isolated p1 \1" + using LTS.trans_star_states_last Suc.prems(2) by fastforce + have "(p1, [\1]) \\<^sup>* (p, LTS_\.remove_\ w)" + using ss_w_short unfolding LTS_\.remove_\_def + using VII by force + have "(the_Ctr_Loc q, [the_Label q]) \\<^sup>* (p, LTS_\.remove_\ w)" + by (simp add: \(p1, [\1]) \\<^sup>* (p, LTS_\.remove_\ w)\ q_ext) + then show ?thesis + using q_ext by auto + next + case (add_trans_push_2 p2 \2 p1 \1 \'' q') (* Adjusted from previous case *) + note IX = add_trans_push_2(3) + note XIII = add_trans_push_2(2) + have t_def: "t = (Isolated p1 \1, Some \'', q')" + using local.add_trans_push_2(1,4) p1_\_p2_w2_q'_p(1) t_def by blast + have init_Ai: "inits \ LTS.srcs Ai" + using step(1,2) step(4) + using no_edge_to_Ctr_Loc_post_star_rules + by (meson r_into_rtranclp) + + from Suc(2,3) split_at_first_t[of "Init p" w ss q Ai j "Isolated p1 \1" "Some \''" q' Aiminus1] t_def + have "\u v u_ss v_ss. + ss = u_ss @ v_ss \ + w = u @ [Some \''] @ v \ + (Init p, u, u_ss, Isolated p1 \1) \ LTS.trans_star_states Aiminus1 \ + (Isolated p1 \1, [Some \''], q') \ LTS.trans_star Ai \ (q', v, v_ss, q) \ LTS.trans_star_states Ai" + using local.add_trans_push_2(1,4) by blast + then obtain u v u_ss v_ss where + ss_split: "ss = u_ss @ v_ss" and + w_split: "w = u @ [Some \''] @ v" and + X_1: "(Init p, u, u_ss, Isolated p1 \1) \ LTS.trans_star_states Aiminus1" and + out_trans: "(Isolated p1 \1, [Some \''], q') \ LTS.trans_star Ai" and + path: "(q', v, v_ss, q) \ LTS.trans_star_states Ai" + by auto + from step(3)[of p u u_ss "Isolated p1 \1"] X_1 have + "(\is_Isolated (Isolated p1 \1) \ + (\p' w'. (Init p', w', Isolated p1 \1) \ LTS_\.trans_star_\ A \ (p', w') \\<^sup>* (p, LTS_\.remove_\ u))) \ + (is_Isolated (Isolated p1 \1) \ + (the_Ctr_Loc (Isolated p1 \1), [the_Label (Isolated p1 \1)]) \\<^sup>* (p, LTS_\.remove_\ u))" + using step.prems(1,2,3) by auto + then have "(the_Ctr_Loc (Isolated p1 \1), [the_Label (Isolated p1 \1)]) \\<^sup>* (p, LTS_\.remove_\ u)" + by auto + then have p1_\1_p_u: "(p1, [\1]) \\<^sup>* (p, LTS_\.remove_\ u)" + by auto + from IX have "\\2\ \2ss. LTS_\.\_exp \2\ [\2] \ (Init p2, \2\, \2ss, q') \ LTS.trans_star_states Aiminus1" + by (meson LTS.trans_star_trans_star_states LTS_\.trans_star_\_\_exp_trans_star) + then obtain \2\ \2ss where XI_1: "LTS_\.\_exp \2\ [\2] \ (Init p2, \2\, \2ss, q') \ LTS.trans_star_states Aiminus1" + by blast + have "(q', v, v_ss, q) \ LTS.trans_star_states Ai" + using path . + have ind: + "(\is_Isolated q \ (\p' w'. (Init p', w', q) \ LTS_\.trans_star_\ A \ (p', w') \\<^sup>* (p2, LTS_\.remove_\ (\2\ @ v)))) \ + (is_Isolated q \ (the_Ctr_Loc q, [the_Label q]) \\<^sup>* (p2, LTS_\.remove_\ (\2\ @ v)))" + proof - + have \2ss_len: "length \2ss = Suc (length \2\)" + by (meson LTS.trans_star_states_length XI_1) + + have v_ss_empty: "v_ss \ []" + by (metis LTS.trans_star_states.simps path list.distinct(1)) + + have \2ss_last: "last \2ss = hd v_ss" + by (metis LTS.trans_star_states_hd LTS.trans_star_states_last XI_1 path) + + + have cv: "j = count (transitions_of ((v_ss, v))) t" + proof - + have last_u_ss: "Isolated p1 \1 = last u_ss" + by (meson LTS.trans_star_states_last X_1) + have q'_hd_v_ss: "q' = hd v_ss" + by (meson LTS.trans_star_states_hd path) + + have "count (transitions_of' (((Init p, u, u_ss, Isolated p1 \1), Some \'') @@\<^sup>\ (q', v, v_ss, q))) + (Isolated p1 \1, Some \'', q') = + count (transitions_of' (Init p, u, u_ss, Isolated p1 \1)) (Isolated p1 \1, Some \'', q') + + (if Isolated p1 \1 = last u_ss \ q' = hd v_ss \ Some \'' = Some \'' then 1 else 0) + + count (transitions_of' (q', v, v_ss, q)) (Isolated p1 \1, Some \'', q')" + using count_append_trans_star_states_\_length[of u_ss u v_ss "Init p" "Isolated p1 \1" "Some \''" q' v q "Isolated p1 \1" "Some \''" q'] t_def ss_split w_split X_1 + by (meson LTS.trans_star_states_length v_ss_empty) + then have "count (transitions_of (u_ss @ v_ss, u @ Some \'' # v)) (last u_ss, Some \'', hd v_ss) = Suc (count (transitions_of (u_ss, u)) (last u_ss, Some \'', hd v_ss) + count (transitions_of (v_ss, v)) (last u_ss, Some \'', hd v_ss))" + using last_u_ss q'_hd_v_ss by auto + then have "j = count (transitions_of' ((q',v, v_ss, q))) t" + using last_u_ss q'_hd_v_ss X_1 ss_split w_split add_trans_push_2(4) Suc(2) + LTS.avoid_count_zero[of "Init p" u u_ss "Isolated p1 \1" Aiminus1 "Isolated p1 \1" "Some \''" q'] + by (auto simp: t_def) + then show "j = count (transitions_of ((v_ss, v))) t" + by force + qed + have p2_q'_states_Aiminus1: "(Init p2, \2\, \2ss, q') \ LTS.trans_star_states Aiminus1" + using XI_1 by blast + then have c\2: "count (transitions_of (\2ss, \2\)) t = 0" + using LTS.avoid_count_zero local.add_trans_push_2(4) t_def by fastforce + have "j = count (transitions_of ((\2ss, \2\) @\ (v_ss, v))) t" + using LTS.count_append_path_with_word[of \2ss \2\ v_ss v "Isolated p1 \1" "Some \''" q'] t_def + c\2 cv \2ss_len v_ss_empty \2ss_last + by force + then have j_count: "j = count (transitions_of' (Init p2, \2\ @ v, \2ss @ tl v_ss, q)) t" + by simp + + have "(\2ss, \2\) \ LTS.path_with_word Aiminus1" + by (meson LTS.trans_star_states_path_with_word p2_q'_states_Aiminus1) + then have \2ss_path: "(\2ss, \2\) \ LTS.path_with_word Ai" + using add_trans_push_2(1) + path_with_word_mono'[of \2ss \2\ Aiminus1 Ai] by auto + + have path': "(v_ss, v) \ LTS.path_with_word Ai" + by (meson LTS.trans_star_states_path_with_word path) + have "(\2ss, \2\) @\ (v_ss, v) \ LTS.path_with_word Ai" + using \2ss_path path' LTS.append_path_with_word_path_with_word \2ss_last + by auto + then have "(\2ss @ tl v_ss, \2\ @ v) \ LTS.path_with_word Ai" + by auto + + + have "(Init p2, \2\ @ v, \2ss @ tl v_ss, q) \ LTS.trans_star_states Ai" + by (metis (no_types, lifting) LTS.path_with_word_trans_star_states + LTS.trans_star_states_append LTS.trans_star_states_hd XI_1 path \2ss_path \2ss_last) + + from this Suc(1)[of p2 "\2\ @ v" "\2ss @ tl v_ss" q] + show + "(\is_Isolated q \ (\p' w'. (Init p', w', q) \ LTS_\.trans_star_\ A \ (p', w') \\<^sup>* (p2, LTS_\.remove_\ (\2\ @ v)))) \ + (is_Isolated q \ (the_Ctr_Loc q, [the_Label q]) \\<^sup>* (p2, LTS_\.remove_\ (\2\ @ v)))" + using j_count by fastforce + qed + + show ?thesis + proof (cases "is_Init q \ is_Noninit q") + case True + have "(\p' w'. (Init p', w', q) \ LTS_\.trans_star_\ A \ (p', w') \\<^sup>* (p2, LTS_\.remove_\ (\2\ @ v)))" + using True ind by fastforce + then obtain p' w' where p'_w'_p: "(Init p', w', q) \ LTS_\.trans_star_\ A \ (p', w') \\<^sup>* (p2, LTS_\.remove_\ (\2\ @ v))" + by auto + then have "(p', w') \\<^sup>* (p2, LTS_\.remove_\ (\2\ @ v))" + by auto + have p2_\2\v_p1_\1_\''_v: "(p2, LTS_\.remove_\ (\2\ @ v)) \\<^sup>* (p1, \1#\''#LTS_\.remove_\ v)" + proof - + have "\2 #(LTS_\.remove_\ v) = LTS_\.remove_\ (\2\ @ v)" + using XI_1 + by (metis LTS_\.\_exp_def LTS_\.remove_\_append_dist LTS_\.remove_\_def append_Cons + self_append_conv2) + moreover + from XIII have "(p2, \2 #(LTS_\.remove_\ v)) \\<^sup>* (p1, \1#\''#LTS_\.remove_\ v)" + by (metis PDS.transition_rel.intros append_Cons append_Nil lbl.simps(3) r_into_rtranclp + step_relp_def) + ultimately + show "(p2, LTS_\.remove_\ (\2\ @ v)) \\<^sup>* (p1, \1#\''#LTS_\.remove_\ v)" + by auto + qed + have p1_\1\''v_p_uv: "(p1, \1#\''#LTS_\.remove_\ v) \\<^sup>* (p, (LTS_\.remove_\ u) @ (\''#LTS_\.remove_\ v))" + by (metis p1_\1_p_u append_Cons append_Nil step_relp_append) + have "(p, (LTS_\.remove_\ u) @ (\''#LTS_\.remove_\ v)) = (p, LTS_\.remove_\ w)" + by (metis (no_types, lifting) Cons_eq_append_conv LTS_\.remove_\_Cons_tl + LTS_\.remove_\_append_dist w_split hd_Cons_tl list.inject list.sel(1) list.simps(3) + self_append_conv2) + then show ?thesis + using True p1_\1\''v_p_uv p2_\2\v_p1_\1_\''_v p'_w'_p by fastforce + next + case False + then have q_nlq_p2_\2\v: "(the_Ctr_Loc q, [the_Label q]) \\<^sup>* (p2, LTS_\.remove_\ (\2\ @ v))" + using ind state.exhaust_disc + by blast + have p2_\2\v_p1_\1\''v: "(p2, LTS_\.remove_\ (\2\ @ v)) \\<^sup>* (p1, \1 # \'' # LTS_\.remove_\ v)" + by (metis (mono_tags) LTS_\.\_exp_def LTS_\.remove_\_append_dist LTS_\.remove_\_def XIII + XI_1 append_Cons append_Nil lbl.simps(3) r_into_rtranclp step_relp_def2) + + have p1_\1\''_v_p_u\''v: "(p1, \1 # \'' # LTS_\.remove_\ v) \\<^sup>* (p, LTS_\.remove_\ u @ \'' # LTS_\.remove_\ v)" + by (metis p1_\1_p_u append_Cons append_Nil step_relp_append) + + have "(p, LTS_\.remove_\ u @ \'' # LTS_\.remove_\ v) = (p, LTS_\.remove_\ w)" + by (metis LTS_\.remove_\_Cons_tl LTS_\.remove_\_append_dist append_Cons append_Nil w_split + hd_Cons_tl list.distinct(1) list.inject) + + then show ?thesis + using False p1_\1\''_v_p_u\''v p2_\2\v_p1_\1\''v q_nlq_p2_\2\v + by (metis (no_types, lifting) ind rtranclp_trans) + qed + qed + qed +qed + +\ \Corresponds to Schwoon's lemma 3.4\ +lemma rtranclp_post_star_rules_constains_successors: + assumes "post_star_rules\<^sup>*\<^sup>* A A'" + assumes "inits \ LTS.srcs A" + assumes "isols \ LTS.isolated A" + assumes "(Init p, w, q) \ LTS.trans_star A'" + shows "(\is_Isolated q \ (\p' w'. (Init p', w', q) \ LTS_\.trans_star_\ A \ (p',w') \\<^sup>* (p, LTS_\.remove_\ w))) \ + (is_Isolated q \ (the_Ctr_Loc q, [the_Label q]) \\<^sup>* (p, LTS_\.remove_\ w))" + using rtranclp_post_star_rules_constains_successors_states assms + by (metis LTS.trans_star_trans_star_states) + + +\ \Corresponds to Schwoon's lemma 3.4\ +lemma post_star_rules_saturation_constains_successors: + assumes "saturation post_star_rules A A'" + assumes "inits \ LTS.srcs A" + assumes "isols \ LTS.isolated A" + assumes "(Init p, w, q) \ LTS.trans_star A'" + shows "(\is_Isolated q \ (\p' w'. (Init p', w', q) \ LTS_\.trans_star_\ A \ (p',w') \\<^sup>* (p, LTS_\.remove_\ w))) \ + (is_Isolated q \ (the_Ctr_Loc q, [the_Label q]) \\<^sup>* (p, LTS_\.remove_\ w))" + using rtranclp_post_star_rules_constains_successors assms saturation_def by metis + +\ \Corresponds to one direction of Schwoon's theorem 3.3\ +theorem post_star_rules_subset_post_star_lang: + assumes "post_star_rules\<^sup>*\<^sup>* A A'" + assumes "inits \ LTS.srcs A" + assumes "isols \ LTS.isolated A" + shows "{c. accepts_\ A' c} \ post_star (lang_\ A)" +proof + fix c :: "('ctr_loc, 'label) conf" + define p where "p = fst c" + define w where "w = snd c" + assume "c \ {c. accepts_\ A' c}" + then have "accepts_\ A' (p,w)" + unfolding p_def w_def by auto + then obtain q where q_p: "q \ finals" "(Init p, w, q) \ LTS_\.trans_star_\ A'" + unfolding accepts_\_def by auto + then obtain w' where w'_def: "LTS_\.\_exp w' w \ (Init p, w', q) \ LTS.trans_star A'" + by (meson LTS_\.trans_star_\_iff_\_exp_trans_star) + then have path: "(Init p, w', q) \ LTS.trans_star A'" + by auto + have "\ is_Isolated q" + using F_not_Ext q_p(1) by blast + then obtain p' w'a where "(Init p', w'a, q) \ LTS_\.trans_star_\ A \ (p', w'a) \\<^sup>* (p, LTS_\.remove_\ w')" + using rtranclp_post_star_rules_constains_successors[OF assms(1) assms(2) assms(3) path] by auto + then have "(Init p', w'a, q) \ LTS_\.trans_star_\ A \ (p', w'a) \\<^sup>* (p, w)" + using w'_def + by (metis LTS_\.\_exp_def LTS_\.remove_\_def + \LTS_\.\_exp w' w \ (Init p, w', q) \ LTS.trans_star A'\) + then have "(p,w) \ post_star (lang_\ A)" + using \q \ finals\ unfolding LTS.post_star_def accepts_\_def lang_\_def by fastforce + then show "c \ post_star (lang_\ A)" + unfolding p_def w_def by auto +qed + +\ \Corresponds to Schwoon's theorem 3.3\ +theorem post_star_rules_accepts_\_correct: + assumes "saturation post_star_rules A A'" + assumes "inits \ LTS.srcs A" + assumes "isols \ LTS.isolated A" + shows "{c. accepts_\ A' c} = post_star (lang_\ A)" +proof (rule; rule) + fix c :: "('ctr_loc, 'label) conf" + define p where "p = fst c" + define w where "w = snd c" + assume "c \ post_star (lang_\ A)" + then obtain p' w' where "(p', w') \\<^sup>* (p, w) \ (p', w') \ lang_\ A" + by (auto simp: post_star_def p_def w_def) + then have "accepts_\ A' (p, w)" + using lemma_3_3[of p' w' p w A A'] assms(1) by auto + then have "accepts_\ A' c" + unfolding p_def w_def by auto + then show "c \ {c. accepts_\ A' c}" + by auto +next + fix c :: "('ctr_loc, 'label) conf" + assume "c \ {c. accepts_\ A' c}" + then show "c \ post_star (lang_\ A)" + using assms post_star_rules_subset_post_star_lang unfolding saturation_def by blast +qed + +\ \Corresponds to Schwoon's theorem 3.3\ +theorem post_star_rules_correct: + assumes "saturation post_star_rules A A'" + assumes "inits \ LTS.srcs A" + assumes "isols \ LTS.isolated A" + shows "lang_\ A' = post_star (lang_\ A)" + using assms lang_\_def post_star_rules_accepts_\_correct by presburger + +end + +subsection \Intersection Automata\ + +definition accepts_inters :: "(('ctr_loc, 'noninit, 'label) state * ('ctr_loc, 'noninit, 'label) state, 'label) transition set \ (('ctr_loc, 'noninit, 'label) state * ('ctr_loc, 'noninit, 'label) state) set \ ('ctr_loc, 'label) conf \ bool" where + "accepts_inters ts finals \ \(p,w). (\qq \ finals. ((Init p, Init p),w,qq) \ LTS.trans_star ts)" + +lemma accepts_inters_accepts_aut_inters: + assumes "ts12 = inters ts1 ts2" + assumes "finals12 = inters_finals finals1 finals2" + shows "accepts_inters ts12 finals12 (p,w) \ + Intersection_P_Automaton.accepts_aut_inters ts1 Init finals1 ts2 + finals2 p w" + by (simp add: Intersection_P_Automaton.accepts_aut_inters_def PDS_with_P_automata.inits_def + P_Automaton.accepts_aut_def accepts_inters_def assms) + +definition lang_inters :: "(('ctr_loc, 'noninit, 'label) state * ('ctr_loc, 'noninit, 'label) state, 'label) transition set \ (('ctr_loc, 'noninit, 'label) state * ('ctr_loc, 'noninit, 'label) state) set \ ('ctr_loc, 'label) conf set" where + "lang_inters ts finals = {c. accepts_inters ts finals c}" + +lemma lang_inters_lang_aut_inters: + assumes "ts12 = inters ts1 ts2" + assumes "finals12 = inters_finals finals1 finals2" + shows "(\(p,w). (p, w)) ` lang_inters ts12 finals12 = + Intersection_P_Automaton.lang_aut_inters ts1 Init finals1 ts2 finals2" + using assms + by (auto simp: Intersection_P_Automaton.lang_aut_inters_def + Intersection_P_Automaton.inters_accept_iff + accepts_inters_accepts_aut_inters lang_inters_def is_Init_def + PDS_with_P_automata.inits_def P_Automaton.accepts_aut_def image_iff) + +lemma inters_accept_iff: + assumes "ts12 = inters ts1 ts2" + assumes "finals12 = inters_finals (PDS_with_P_automata.finals final_initss1 final_noninits1) + (PDS_with_P_automata.finals final_initss2 final_noninits2)" + shows + "accepts_inters ts12 finals12 (p,w) \ + PDS_with_P_automata.accepts final_initss1 final_noninits1 ts1 (p,w) \ + PDS_with_P_automata.accepts final_initss2 final_noninits2 ts2 (p,w)" + using accepts_inters_accepts_aut_inters Intersection_P_Automaton.inters_accept_iff assms + by (simp add: Intersection_P_Automaton.inters_accept_iff accepts_inters_accepts_aut_inters + PDS_with_P_automata.accepts_accepts_aut) + +lemma inters_lang: + assumes "ts12 = inters ts1 ts2" + assumes "finals12 = + inters_finals (PDS_with_P_automata.finals final_initss1 final_noninits1) + (PDS_with_P_automata.finals final_initss2 final_noninits2)" + shows "lang_inters ts12 finals12 = + PDS_with_P_automata.lang final_initss1 final_noninits1 ts1 \ + PDS_with_P_automata.lang final_initss2 final_noninits2 ts2" + using assms by (auto simp add: PDS_with_P_automata.lang_def inters_accept_iff lang_inters_def) + + +subsection \Intersection epsilon-Automata\ + +context PDS_with_P_automata begin + +interpretation LTS transition_rel . +notation step_relp (infix "\" 80) +notation step_starp (infix "\\<^sup>*" 80) + +definition accepts_\_inters :: "(('ctr_loc, 'noninit, 'label) state * ('ctr_loc, 'noninit, 'label) state, 'label option) transition set \ ('ctr_loc, 'label) conf \ bool" where + "accepts_\_inters ts \ \(p,w). (\q1 \ finals. \q2 \ finals. ((Init p, Init p),w,(q1,q2)) \ LTS_\.trans_star_\ ts)" + +definition lang_\_inters :: "(('ctr_loc, 'noninit, 'label) state * ('ctr_loc, 'noninit, 'label) state, 'label option) transition set \ ('ctr_loc, 'label) conf set" where + "lang_\_inters ts = {c. accepts_\_inters ts c}" + +lemma trans_star_trans_star_\_inter: + assumes "LTS_\.\_exp w1 w" + assumes "LTS_\.\_exp w2 w" + assumes "(p1, w1, p2) \ LTS.trans_star ts1" + assumes "(q1, w2, q2) \ LTS.trans_star ts2" + shows "((p1,q1), w :: 'label list, (p2,q2)) \ LTS_\.trans_star_\ (inters_\ ts1 ts2)" + using assms +proof (induction "length w1 + length w2" arbitrary: w1 w2 w p1 q1 rule: less_induct) + case less + then show ?case + proof (cases "\\ w1' w2' \. w1=Some \#w1' \ w2=Some \#w2'") + case True + from True obtain \ \ w1' w2' where True'': + "w1=Some \#w1'" + "w2=Some \#w2'" + by auto + have "\ = \" + by (metis True''(1) True''(2) LTS_\.\_exp_Some_hd less.prems(1) less.prems(2)) + then have True': + "w1=Some \#w1'" + "w2=Some \#w2'" + using True'' by auto + define w' where "w' = tl w" + obtain p' where p'_p: "(p1, Some \, p') \ ts1 \ (p', w1', p2) \ LTS.trans_star ts1" + using less True'(1) by (metis LTS_\.trans_star_cons_\) + obtain q' where q'_p: "(q1, Some \, q') \ ts2 \(q', w2', q2) \ LTS.trans_star ts2" + using less True'(2) by (metis LTS_\.trans_star_cons_\) + have ind: "((p', q'), w', p2, q2) \ LTS_\.trans_star_\ (inters_\ ts1 ts2)" + proof - + have "length w1' + length w2' < length w1 + length w2" + using True'(1) True'(2) by simp + moreover + have "LTS_\.\_exp w1' w'" + by (metis (no_types) LTS_\.\_exp_def less(2) True'(1) list.map(2) list.sel(3) + option.simps(3) removeAll.simps(2) w'_def) + moreover + have "LTS_\.\_exp w2' w'" + by (metis (no_types) LTS_\.\_exp_def less(3) True'(2) list.map(2) list.sel(3) + option.simps(3) removeAll.simps(2) w'_def) + moreover + have "(p', w1', p2) \ LTS.trans_star ts1" + using p'_p by simp + moreover + have "(q', w2', q2) \ LTS.trans_star ts2" + using q'_p by simp + ultimately + show "((p', q'), w', p2, q2) \ LTS_\.trans_star_\ (inters_\ ts1 ts2)" + using less(1)[of w1' w2' w' p' q'] by auto + qed + moreover + have "((p1, q1), Some \, (p', q')) \ (inters_\ ts1 ts2)" + by (simp add: inters_\_def p'_p q'_p) + ultimately + have "((p1, q1), \#w', p2, q2) \ LTS_\.trans_star_\ (inters_\ ts1 ts2)" + by (meson LTS_\.trans_star_\.trans_star_\_step_\) + moreover + have "length w > 0" + using less(3) True' LTS_\.\_exp_Some_length by metis + moreover + have "hd w = \" + using less(3) True' LTS_\.\_exp_Some_hd by metis + ultimately + show ?thesis + using w'_def by force + next + case False + note False_outer_outer_outer_outer = False + show ?thesis + proof (cases "w1 = [] \ w2 = []") + case True + then have same: "p1 = p2 \ q1 = q2" + by (metis LTS.trans_star_empty less.prems(3) less.prems(4)) + have "w = []" + using True less(2) LTS_\.exp_empty_empty by auto + then show ?thesis + using less True + by (simp add: LTS_\.trans_star_\.trans_star_\_refl same) + next + case False + note False_outer_outer_outer = False + show ?thesis + proof (cases "\w1'. w1=\#w1'") + case True (* Adapted from above. *) + then obtain w1' where True': + "w1=\#w1'" + by auto + obtain p' where p'_p: "(p1, \, p') \ ts1 \ (p', w1', p2) \ LTS.trans_star ts1" + using less True'(1) by (metis LTS_\.trans_star_cons_\) + have q'_p: " (q1, w2, q2) \ LTS.trans_star ts2" + using less by (metis) + have ind: "((p', q1), w, p2, q2) \ LTS_\.trans_star_\ (inters_\ ts1 ts2)" + proof - + have "length w1' + length w2 < length w1 + length w2" + using True'(1) by simp + moreover + have "LTS_\.\_exp w1' w" + by (metis (no_types) LTS_\.\_exp_def less(2) True'(1) removeAll.simps(2)) + moreover + have "LTS_\.\_exp w2 w" + by (metis (no_types) less(3)) + moreover + have "(p', w1', p2) \ LTS.trans_star ts1" + using p'_p by simp + moreover + have "(q1, w2, q2) \ LTS.trans_star ts2" + using q'_p by simp + ultimately + show "((p', q1), w, p2, q2) \ LTS_\.trans_star_\ (inters_\ ts1 ts2)" + using less(1)[of w1' w2 w p' q1] by auto + qed + moreover + have "((p1, q1), \, (p', q1)) \ (inters_\ ts1 ts2)" + by (simp add: inters_\_def p'_p q'_p) + ultimately + have "((p1, q1), w, p2, q2) \ LTS_\.trans_star_\ (inters_\ ts1 ts2)" + using LTS_\.trans_star_\.simps by fastforce + then + show ?thesis + by force + next + case False + note False_outer_outer = False + then show ?thesis + proof (cases "\w2'. w2 = \ # w2'") + case True (* Adapted from above. *) + then obtain w2' where True': + "w2=\#w2'" + by auto + have p'_p: "(p1, w1, p2) \ LTS.trans_star ts1" + using less by (metis) + obtain q' where q'_p: "(q1, \, q') \ ts2 \(q', w2', q2) \ LTS.trans_star ts2" + using less True'(1) by (metis LTS_\.trans_star_cons_\) + have ind: "((p1, q'), w, p2, q2) \ LTS_\.trans_star_\ (inters_\ ts1 ts2)" + proof - + have "length w1 + length w2' < length w1 + length w2" + using True'(1) True'(1) by simp + moreover + have "LTS_\.\_exp w1 w" + by (metis (no_types) less(2)) + moreover + have "LTS_\.\_exp w2' w" + by (metis (no_types) LTS_\.\_exp_def less(3) True'(1) removeAll.simps(2)) + moreover + have "(p1, w1, p2) \ LTS.trans_star ts1" + using p'_p by simp + moreover + have "(q', w2', q2) \ LTS.trans_star ts2" + using q'_p by simp + ultimately + show "((p1, q'), w, p2, q2) \ LTS_\.trans_star_\ (inters_\ ts1 ts2)" + using less(1)[of w1 w2' w p1 q'] by auto + qed + moreover + have "((p1, q1), \, (p1, q')) \ (inters_\ ts1 ts2)" + by (simp add: inters_\_def p'_p q'_p) + ultimately + have "((p1, q1), w, p2, q2) \ LTS_\.trans_star_\ (inters_\ ts1 ts2)" + using LTS_\.trans_star_\.simps by fastforce + then + show ?thesis + by force + next + case False + then have "(w1 = [] \ (\\ w2'. w2 = Some \ # w2')) \ ((\\ w1'. w1 = Some \ # w1') \ w2 = [])" + using False_outer_outer False_outer_outer_outer False_outer_outer_outer_outer + by (metis neq_Nil_conv option.exhaust_sel) + then show ?thesis + by (metis LTS_\.\_exp_def LTS_\.\_exp_Some_length less.prems(1,2) less_numeral_extra(3) + list.simps(8) list.size(3) removeAll.simps(1)) + qed + qed + qed + qed +qed + +lemma trans_star_\_inter: + assumes "(p1, w :: 'label list, p2) \ LTS_\.trans_star_\ ts1" + assumes "(q1, w, q2) \ LTS_\.trans_star_\ ts2" + shows "((p1, q1), w, (p2, q2)) \ LTS_\.trans_star_\ (inters_\ ts1 ts2)" +proof - + have "\w1'. LTS_\.\_exp w1' w \ (p1, w1', p2) \ LTS.trans_star ts1" + using assms by (simp add: LTS_\.trans_star_\_\_exp_trans_star) + then obtain w1' where "LTS_\.\_exp w1' w \ (p1, w1', p2) \ LTS.trans_star ts1" + by auto + moreover + have "\w2'. LTS_\.\_exp w2' w \ (q1, w2', q2) \ LTS.trans_star ts2" + using assms by (simp add: LTS_\.trans_star_\_\_exp_trans_star) + then obtain w2' where "LTS_\.\_exp w2' w \ (q1, w2', q2) \ LTS.trans_star ts2" + by auto + ultimately + show ?thesis + using trans_star_trans_star_\_inter by metis +qed + +lemma inters_trans_star_\1: + assumes "(p1q2, w :: 'label list, p2q2) \ LTS_\.trans_star_\ (inters_\ ts1 ts2)" + shows "(fst p1q2, w, fst p2q2) \ LTS_\.trans_star_\ ts1" + using assms +proof (induction rule: LTS_\.trans_star_\.induct[OF assms(1)]) + case (1 p) + then show ?case + by (simp add: LTS_\.trans_star_\.trans_star_\_refl) +next + case (2 p \ q' w q) + then have ind: "(fst q', w, fst q) \ LTS_\.trans_star_\ ts1" + by auto + from 2(1) have "(p, Some \, q') \ + {((p1, q1), \, p2, q2) |p1 q1 \ p2 q2. (p1, \, p2) \ ts1 \ (q1, \, q2) \ ts2} \ + {((p1, q1), \, p2, q1) |p1 p2 q1. (p1, \, p2) \ ts1} \ + {((p1, q1), \, p1, q2) |p1 q1 q2. (q1, \, q2) \ ts1}" + unfolding inters_\_def by auto + moreover + { + assume "(p, Some \, q') \ {((p1, q1), \, p2, q2) |p1 q1 \ p2 q2. (p1, \, p2) \ ts1 \ (q1, \, q2) \ ts2}" + then have "\p1 q1. p = (p1, q1) \ (\p2 q2. q' = (p2, q2) \ (p1, Some \, p2) \ ts1 \ (q1, Some \, q2) \ ts2)" + by simp + then obtain p1 q1 where "p = (p1, q1) \ (\p2 q2. q' = (p2, q2) \ (p1, Some \, p2) \ ts1 \ (q1, Some \, q2) \ ts2)" + by auto + then have ?case + using LTS_\.trans_star_\.trans_star_\_step_\ ind by fastforce + } + moreover + { + assume "(p, Some \, q') \ {((p1, q1), \, p2, q1) |p1 p2 q1. (p1, \, p2) \ ts1}" + then have ?case + by auto + } + moreover + { + assume "(p, Some \, q') \ {((p1, q1), \, p1, q2) |p1 q1 q2. (q1, \, q2) \ ts1}" + then have ?case + by auto + } + ultimately + show ?case + by auto +next + case (3 p q' w q) + then have ind: "(fst q', w, fst q) \ LTS_\.trans_star_\ ts1" + by auto + from 3(1) have "(p, \, q') \ + {((p1, q1), \, (p2, q2)) | p1 q1 \ p2 q2. (p1, \, p2) \ ts1 \ (q1, \, q2) \ ts2} \ + {((p1, q1), \, (p2, q1)) | p1 p2 q1. (p1, \, p2) \ ts1} \ + {((p1, q1), \, (p1, q2)) | p1 q1 q2. (q1, \, q2) \ ts2}" + unfolding inters_\_def by auto + moreover + { + assume "(p, \, q') \ {((p1, q1), \, p2, q2) |p1 q1 \ p2 q2. (p1, \, p2) \ ts1 \ (q1, \, q2) \ ts2}" + then have "\p1 q1. p = (p1, q1) \ (\p2 q2. q' = (p2, q2) \ (p1, \, p2) \ ts1 \ (q1, \, q2) \ ts2)" + by simp + then obtain p1 q1 where "p = (p1, q1) \ (\p2 q2. q' = (p2, q2) \ (p1, \, p2) \ ts1 \ (q1, \, q2) \ ts2)" + by auto + then have ?case + using LTS_\.trans_star_\.trans_star_\_step_\ ind by fastforce + } + moreover + { + assume "(p, \, q') \ {((p1, q1), \, p2, q1) |p1 p2 q1. (p1, \, p2) \ ts1}" + then have "\p1 p2 q1. p = (p1, q1) \ q' = (p2, q1) \ (p1, \, p2) \ ts1" + by auto + then obtain p1 p2 q1 where "p = (p1, q1) \ q' = (p2, q1) \ (p1, \, p2) \ ts1" + by auto + then have ?case + using LTS_\.trans_star_\.trans_star_\_step_\ ind by fastforce + } + moreover + { + assume "(p, \, q') \ {((p1, q1), \, p1, q2) |p1 q1 q2. (q1, \, q2) \ ts2}" + then have "\p1 q1 q2. p = (p1, q1) \ q' = (p1, q2) \ (q1, \, q2) \ ts2" + by auto + then obtain p1 q1 q2 where "p = (p1, q1) \ q' = (p1, q2) \ (q1, \, q2) \ ts2" + by auto + then have ?case + using LTS_\.trans_star_\.trans_star_\_step_\ ind by fastforce + } + ultimately + show ?case + by auto +qed + +lemma inters_trans_star_\: + assumes "(p1q2, w :: 'label list, p2q2) \ LTS_\.trans_star_\ (inters_\ ts1 ts2)" + shows "(snd p1q2, w, snd p2q2) \ LTS_\.trans_star_\ ts2" + using assms +proof (induction rule: LTS_\.trans_star_\.induct[OF assms(1)]) + case (1 p) + then show ?case + by (simp add: LTS_\.trans_star_\.trans_star_\_refl) +next + case (2 p \ q' w q) + then have ind: "(snd q', w, snd q) \ LTS_\.trans_star_\ ts2" + by auto + from 2(1) have "(p, Some \, q') \ + {((p1, q1), \, p2, q2) |p1 q1 \ p2 q2. (p1, \, p2) \ ts1 \ (q1, \, q2) \ ts2} \ + {((p1, q1), \, p2, q1) |p1 p2 q1. (p1, \, p2) \ ts1} \ + {((p1, q1), \, p1, q2) |p1 q1 q2. (q1, \, q2) \ ts2}" + unfolding inters_\_def by auto + moreover + { + assume "(p, Some \, q') \ {((p1, q1), \, p2, q2) |p1 q1 \ p2 q2. (p1, \, p2) \ ts1 \ (q1, \, q2) \ ts2}" + then have "\p1 q1. p = (p1, q1) \ (\p2 q2. q' = (p2, q2) \ (p1, Some \, p2) \ ts1 \ (q1, Some \, q2) \ ts2)" + by simp + then obtain p1 q1 where "p = (p1, q1) \ (\p2 q2. q' = (p2, q2) \ (p1, Some \, p2) \ ts1 \ (q1, Some \, q2) \ ts2)" + by auto + then have ?case + using LTS_\.trans_star_\.trans_star_\_step_\ ind by fastforce + } + moreover + { + assume "(p, Some \, q') \ {((p1, q1), \, p2, q1) |p1 p2 q1. (p1, \, p2) \ ts1}" + then have ?case + by auto + } + moreover + { + assume "(p, Some \, q') \ {((p1, q1), \, p1, q2) |p1 q1 q2. (q1, \, q2) \ ts2}" + then have ?case + by auto + } + ultimately + show ?case + by auto +next + case (3 p q' w q) + then have ind: "(snd q', w, snd q) \ LTS_\.trans_star_\ ts2" + by auto + from 3(1) have "(p, \, q') \ + {((p1, q1), \, (p2, q2)) | p1 q1 \ p2 q2. (p1, \, p2) \ ts1 \ (q1, \, q2) \ ts2} \ + {((p1, q1), \, (p2, q1)) | p1 p2 q1. (p1, \, p2) \ ts1} \ + {((p1, q1), \, (p1, q2)) | p1 q1 q2. (q1, \, q2) \ ts2}" + unfolding inters_\_def by auto + moreover + { + assume "(p, \, q') \ {((p1, q1), \, p2, q2) |p1 q1 \ p2 q2. (p1, \, p2) \ ts1 \ (q1, \, q2) \ ts2}" + then have "\p1 q1. p = (p1, q1) \ (\p2 q2. q' = (p2, q2) \ (p1, \, p2) \ ts1 \ (q1, \, q2) \ ts2)" + by simp + then obtain p1 q1 where "p = (p1, q1) \ (\p2 q2. q' = (p2, q2) \ (p1, \, p2) \ ts1 \ (q1, \, q2) \ ts2)" + by auto + then have ?case + using LTS_\.trans_star_\.trans_star_\_step_\ ind by fastforce + } + moreover + { + assume "(p, \, q') \ {((p1, q1), \, p2, q1) |p1 p2 q1. (p1, \, p2) \ ts1}" + then have "\p1 p2 q1. p = (p1, q1) \ q' = (p2, q1) \ (p1, \, p2) \ ts1" + by auto + then obtain p1 p2 q1 where "p = (p1, q1) \ q' = (p2, q1) \ (p1, \, p2) \ ts1" + by auto + then have ?case + using LTS_\.trans_star_\.trans_star_\_step_\ ind by fastforce + } + moreover + { + assume "(p, \, q') \ {((p1, q1), \, p1, q2) |p1 q1 q2. (q1, \, q2) \ ts2}" + then have "\p1 q1 q2. p = (p1, q1) \ q' = (p1, q2) \ (q1, \, q2) \ ts2" + by auto + then obtain p1 q1 q2 where "p = (p1, q1) \ q' = (p1, q2) \ (q1, \, q2) \ ts2" + by auto + then have ?case + using LTS_\.trans_star_\.trans_star_\_step_\ ind by fastforce + } + ultimately + show ?case + by auto +qed + +lemma inters_trans_star_\_iff: + "((p1,q2), w :: 'label list, (p2,q2)) \ LTS_\.trans_star_\ (inters_\ ts1 ts2) \ + (p1, w, p2) \ LTS_\.trans_star_\ ts1 \ (q2, w, q2) \ LTS_\.trans_star_\ ts2" + by (metis fst_conv inters_trans_star_\ inters_trans_star_\1 snd_conv trans_star_\_inter) + +lemma inters_\_accept_\_iff: + "accepts_\_inters (inters_\ ts1 ts2) c \ accepts_\ ts1 c \ accepts_\ ts2 c" +proof + assume "accepts_\_inters (inters_\ ts1 ts2) c" + then show "accepts_\ ts1 c \ accepts_\ ts2 c" + using accepts_\_def accepts_\_inters_def inters_trans_star_\ inters_trans_star_\1 by fastforce +next + assume asm: "accepts_\ ts1 c \ accepts_\ ts2 c" + define p where "p = fst c" + define w where "w = snd c" + + from asm have "accepts_\ ts1 (p,w) \ accepts_\ ts2 (p,w)" + using p_def w_def by auto + then have "(\q\finals. (Init p, w, q) \ LTS_\.trans_star_\ ts1) \ + (\q\finals. (Init p, w, q) \ LTS_\.trans_star_\ ts2)" + unfolding accepts_\_def by auto + then show "accepts_\_inters (inters_\ ts1 ts2) c" + using accepts_\_inters_def p_def trans_star_\_inter w_def by fastforce +qed + +lemma inters_\_lang_\: "lang_\_inters (inters_\ ts1 ts2) = lang_\ ts1 \ lang_\ ts2" + unfolding lang_\_inters_def lang_\_def using inters_\_accept_\_iff by auto + + +subsection \Dual search\ + +lemma dual1: + "post_star (lang_\ A1) \ pre_star (lang A2) = {c. \c1 \ lang_\ A1. \c2 \ lang A2. c1 \\<^sup>* c \ c \\<^sup>* c2}" +proof - + have "post_star (lang_\ A1) \ pre_star (lang A2) = {c. c \ post_star (lang_\ A1) \ c \ pre_star (lang A2)}" + by auto + moreover + have "... = {c. (\c1 \ lang_\ A1. c1 \\<^sup>* c) \ (\c2 \ lang A2. c \\<^sup>* c2)}" + unfolding post_star_def pre_star_def by auto + moreover + have "... = {c. \c1 \ lang_\ A1. \c2 \ lang A2. c1 \\<^sup>* c \ c \\<^sup>* c2}" + by auto + ultimately + show ?thesis by metis +qed + +lemma dual2: + "post_star (lang_\ A1) \ pre_star (lang A2) \ {} \ (\c1 \ lang_\ A1. \c2 \ lang A2. c1 \\<^sup>* c2)" +proof (rule) + assume "post_star (lang_\ A1) \ pre_star (lang A2) \ {}" + then show "\c1\lang_\ A1. \c2\lang A2. c1 \\<^sup>* c2" + by (auto simp: pre_star_def post_star_def intro: rtranclp_trans) +next + assume "\c1\lang_\ A1. \c2\lang A2. c1 \\<^sup>* c2" + then show "post_star (lang_\ A1) \ pre_star (lang A2) \ {}" + using dual1 by auto +qed + +lemma LTS_\_of_LTS_Some: "(p, Some \, q') \ LTS_\_of_LTS A2' \ (p, \, q') \ A2'" + unfolding LTS_\_of_LTS_def \_edge_of_edge_def by (auto simp add: rev_image_eqI) + +lemma LTS_\_of_LTS_None: "(p, None, q') \ LTS_\_of_LTS A2'" + unfolding LTS_\_of_LTS_def \_edge_of_edge_def by (auto) + +lemma trans_star_\_LTS_\_of_LTS_trans_star: + assumes "(p,w,q) \ LTS_\.trans_star_\ (LTS_\_of_LTS A2')" + shows "(p,w,q) \ LTS.trans_star A2'" + using assms +proof (induction rule: LTS_\.trans_star_\.induct[OF assms(1)] ) + case (1 p) + then show ?case + by (simp add: LTS.trans_star.trans_star_refl) +next + case (2 p \ q' w q) + moreover + have "(p, \, q') \ A2'" + using 2(1) using LTS_\_of_LTS_Some by metis + moreover + have "(q', w, q) \ LTS.trans_star A2'" + using "2.IH" 2(2) by auto + ultimately show ?case + by (meson LTS.trans_star.trans_star_step) +next + case (3 p q' w q) + then show ?case + using LTS_\_of_LTS_None by fastforce +qed + +lemma trans_star_trans_star_\_LTS_\_of_LTS: + assumes "(p,w,q) \ LTS.trans_star A2'" + shows "(p,w,q) \ LTS_\.trans_star_\ (LTS_\_of_LTS A2')" + using assms +proof (induction rule: LTS.trans_star.induct[OF assms(1)]) + case (1 p) + then show ?case + by (simp add: LTS_\.trans_star_\.trans_star_\_refl) +next + case (2 p \ q' w q) + then show ?case + by (meson LTS_\.trans_star_\.trans_star_\_step_\ LTS_\_of_LTS_Some) +qed + + +lemma accepts_\_LTS_\_of_LTS_iff_accepts: "accepts_\ (LTS_\_of_LTS A2') (p, w) \ accepts A2' (p, w)" + using accepts_\_def accepts_def trans_star_\_LTS_\_of_LTS_trans_star + trans_star_trans_star_\_LTS_\_of_LTS by fastforce + +lemma lang_\_LTS_\_of_LTS_is_lang: "lang_\ (LTS_\_of_LTS A2') = lang A2'" + unfolding lang_\_def lang_def using accepts_\_LTS_\_of_LTS_iff_accepts by auto + +theorem dual_star_correct_early_termination: + assumes "inits \ LTS.srcs A1" + assumes "inits \ LTS.srcs A2" + assumes "isols \ LTS.isolated A1" + assumes "isols \ LTS.isolated A2" + assumes "post_star_rules\<^sup>*\<^sup>* A1 A1'" + assumes "pre_star_rule\<^sup>*\<^sup>* A2 A2'" + assumes "lang_\_inters (inters_\ A1' (LTS_\_of_LTS A2')) \ {}" + shows "\c1 \ lang_\ A1. \c2 \ lang A2. c1 \\<^sup>* c2" +proof - + have "{c. accepts_\ A1' c} \ post_star (lang_\ A1)" + using assms using post_star_rules_subset_post_star_lang by auto + then have A1'_correct: "lang_\ A1' \ post_star (lang_\ A1)" + unfolding lang_\_def by auto + + have "{c. accepts A2' c} \ pre_star (lang A2)" + using pre_star_rule_subset_pre_star_lang[of A2 A2'] assms by auto + then have A2'_correct: "lang A2' \ pre_star (lang A2)" + unfolding lang_def by auto + + have "lang_\_inters (inters_\ A1' (LTS_\_of_LTS A2')) = lang_\ A1' \ lang_\ (LTS_\_of_LTS A2')" + using inters_\_lang_\[of A1' "(LTS_\_of_LTS A2')"] by auto + moreover + have "... = lang_\ A1' \ lang A2'" + using lang_\_LTS_\_of_LTS_is_lang by auto + moreover + have "... \ post_star (lang_\ A1) \ pre_star (lang A2)" + using A1'_correct A2'_correct by auto + ultimately + have inters_correct: "lang_\_inters (inters_\ A1' (LTS_\_of_LTS A2')) \ post_star (lang_\ A1) \ pre_star (lang A2)" + by metis + + from assms have "post_star (lang_\ A1) \ pre_star (lang A2) \ {}" + using inters_correct by auto + then show "\c1\lang_\ A1. \c2\lang A2. c1 \\<^sup>* c2" + using dual2 by auto + +qed + +theorem dual_star_correct_saturation: + assumes "inits \ LTS.srcs A1" + assumes "inits \ LTS.srcs A2" + assumes "isols \ LTS.isolated A1" + assumes "isols \ LTS.isolated A2" + assumes "saturation post_star_rules A1 A1'" + assumes "saturation pre_star_rule A2 A2'" + shows "lang_\_inters (inters_\ A1' (LTS_\_of_LTS A2')) \ {} \ (\c1 \ lang_\ A1. \c2 \ lang A2. c1 \\<^sup>* c2)" +proof - + have "{c. accepts_\ A1' c} = post_star (lang_\ A1)" + using post_star_rules_accepts_\_correct[of A1 A1'] assms by auto + then have A1'_correct: "lang_\ A1' = post_star (lang_\ A1)" + unfolding lang_\_def by auto + + have "{c. accepts A2' c} = pre_star (lang A2)" + using pre_star_rule_accepts_correct[of A2 A2'] assms by auto + then have A2'_correct: "lang A2' = pre_star (lang A2)" + unfolding lang_def by auto + + have "lang_\_inters (inters_\ A1' (LTS_\_of_LTS A2')) = lang_\ A1' \ lang_\ (LTS_\_of_LTS A2')" + using inters_\_lang_\[of A1' "(LTS_\_of_LTS A2')"] by auto + moreover + have "... = lang_\ A1' \ lang A2'" + using lang_\_LTS_\_of_LTS_is_lang by auto + moreover + have "... = post_star (lang_\ A1) \ pre_star (lang A2)" + using A1'_correct A2'_correct by auto + ultimately + have inters_correct: "lang_\_inters (inters_\ A1' (LTS_\_of_LTS A2')) = post_star (lang_\ A1) \ pre_star (lang A2)" + by metis + + show ?thesis + proof + assume "lang_\_inters (inters_\ A1' (LTS_\_of_LTS A2')) \ {}" + then have "post_star (lang_\ A1) \ pre_star (lang A2) \ {}" + using inters_correct by auto + then show "\c1\lang_\ A1. \c2\lang A2. c1 \\<^sup>* c2" + using dual2 by auto + next + assume "\c1\lang_\ A1. \c2\lang A2. c1 \\<^sup>* c2" + then have "post_star (lang_\ A1) \ pre_star (lang A2) \ {}" + using dual2 by auto + then show "lang_\_inters (inters_\ A1' (LTS_\_of_LTS A2')) \ {}" + using inters_correct by auto + qed +qed + +theorem dual_star_correct_early_termination_configs: + assumes "inits \ LTS.srcs A1" + assumes "inits \ LTS.srcs A2" + assumes "isols \ LTS.isolated A1" + assumes "isols \ LTS.isolated A2" + assumes "lang_\ A1 = {c1}" + assumes "lang A2 = {c2}" + assumes "post_star_rules\<^sup>*\<^sup>* A1 A1'" + assumes "pre_star_rule\<^sup>*\<^sup>* A2 A2'" + assumes "lang_\_inters (inters_\ A1' (LTS_\_of_LTS A2')) \ {}" + shows "c1 \\<^sup>* c2" + using dual_star_correct_early_termination assms by (metis singletonD) + +theorem dual_star_correct_saturation_configs: + assumes "inits \ LTS.srcs A1" + assumes "inits \ LTS.srcs A2" + assumes "isols \ LTS.isolated A1" + assumes "isols \ LTS.isolated A2" + assumes "lang_\ A1 = {c1}" + assumes "lang A2 = {c2}" + assumes "saturation post_star_rules A1 A1'" + assumes "saturation pre_star_rule A2 A2'" + shows "lang_\_inters (inters_\ A1' (LTS_\_of_LTS A2')) \ {} \ c1 \\<^sup>* c2" + using assms dual_star_correct_saturation by auto + +end + +end diff --git a/thys/Pushdown_Systems/PDS_Code.thy b/thys/Pushdown_Systems/PDS_Code.thy new file mode 100644 --- /dev/null +++ b/thys/Pushdown_Systems/PDS_Code.thy @@ -0,0 +1,57 @@ +theory PDS_Code + imports PDS "Deriving.Derive" +begin + +global_interpretation pds: PDS_with_P_automata \ F_ctr_loc F_ctr_loc_st + for \ :: "('ctr_loc::{enum, linorder}, 'label::{finite, linorder}) rule set" + and F_ctr_loc :: "('ctr_loc) set" + and F_ctr_loc_st :: "('state::finite) set" + defines pre_star = "PDS_with_P_automata.pre_star_exec \" + and pre_star_check = "PDS_with_P_automata.pre_star_exec_check \" + and inits = "PDS_with_P_automata.inits" + and finals = "PDS_with_P_automata.finals F_ctr_loc F_ctr_loc_st" + and accepts = "PDS_with_P_automata.accepts F_ctr_loc F_ctr_loc_st" + and language = "PDS_with_P_automata.lang F_ctr_loc F_ctr_loc_st" + and step_starp = "rtranclp (LTS.step_relp (PDS.transition_rel \))" + and accepts_pre_star_check = "PDS_with_P_automata.accept_pre_star_exec_check \ F_ctr_loc F_ctr_loc_st" + . + +global_interpretation inter: Intersection_P_Automaton + initial_automaton Init "finals initial_F_ctr_loc initial_F_ctr_loc_st" + "pre_star \ final_automaton" "finals final_F_ctr_loc final_F_ctr_loc_st" + for \ :: "('ctr_loc::{enum, linorder}, 'label::{finite, linorder}) rule set" + and initial_automaton :: "(('ctr_loc, 'state::finite, 'label) state, 'label) transition set" + and initial_F_ctr_loc :: "'ctr_loc set" + and initial_F_ctr_loc_st :: "'state set" + and final_automaton :: "(('ctr_loc, 'state, 'label) state, 'label) transition set" + and final_F_ctr_loc :: "'ctr_loc set" + and final_F_ctr_loc_st :: "'state set" + defines nonempty_inter = "P_Automaton.nonempty + (inters initial_automaton (pre_star \ final_automaton)) + ((\p. (Init p, Init p))) + (inters_finals (finals initial_F_ctr_loc initial_F_ctr_loc_st) + (finals final_F_ctr_loc final_F_ctr_loc_st))" + . + +definition "check \ I IF IF_st F FF FF_st = + (if pds.inits \ LTS.srcs F then Some (nonempty_inter \ I IF IF_st F FF FF_st) else None)" + +lemma check_None: "check \ I IF IF_st F FF FF_st = None \ \ (inits \ LTS.srcs F)" + unfolding check_def by auto + +lemma check_Some: "check \ I IF IF_st F FF FF_st = Some b \ + (inits \ LTS.srcs F \ b = (\p w p' w'. + (p, w) \ language IF IF_st I \ + (p', w') \ language FF FF_st F \ + step_starp \ (p, w) (p', w')))" + unfolding check_def nonempty_inter_def P_Automaton.nonempty_def + inter.lang_aut_alt inter.inters_lang + pds.lang_aut_lang + by (auto 0 5 simp: pds.pre_star_exec_lang_correct pds.pre_star_def image_iff + elim!: bexI[rotated]) + +declare P_Automaton.mark.simps[code] + +export_code check checking SML + +end diff --git a/thys/Pushdown_Systems/P_Automata.thy b/thys/Pushdown_Systems/P_Automata.thy new file mode 100644 --- /dev/null +++ b/thys/Pushdown_Systems/P_Automata.thy @@ -0,0 +1,704 @@ +theory P_Automata imports Labeled_Transition_Systems.LTS begin + + +section \Automata\ + + +subsection \P-Automaton locale\ + +locale P_Automaton = LTS transition_relation + for transition_relation :: "('state::finite, 'label) transition set" + + fixes Init :: "'ctr_loc::enum \ 'state" + and finals :: "'state set" +begin + +definition initials :: "'state set" where + "initials \ Init ` UNIV" + +lemma initials_list: + "initials = set (map Init Enum.enum)" + using enum_UNIV unfolding initials_def by force + +definition accepts_aut :: "'ctr_loc \ 'label list \ bool" where + "accepts_aut \ \p w. (\q \ finals. (Init p, w, q) \ trans_star)" + +definition lang_aut :: "('ctr_loc * 'label list) set" where + "lang_aut = {(p,w). accepts_aut p w}" + +definition nonempty where + "nonempty \ lang_aut \ {}" + +lemma nonempty_alt: + "nonempty \ (\p. \q \ finals. \w. (Init p, w, q) \ trans_star)" + unfolding lang_aut_def nonempty_def accepts_aut_def by auto + +typedef 'a mark_state = "{(Q :: 'a set, I). I \ Q}" + by auto +setup_lifting type_definition_mark_state +lift_definition get_visited :: "'a mark_state \ 'a set" is fst . +lift_definition get_next :: "'a mark_state \ 'a set" is snd . +lift_definition make_mark_state :: "'a set \ 'a set \ 'a mark_state" is "\Q J. (Q \ J, J)" by auto +lemma get_next_get_visited: "get_next ms \ get_visited ms" + by transfer auto +lemma get_next_set_next[simp]: "get_next (make_mark_state Q J) = J" + by transfer auto +lemma get_visited_set_next[simp]: "get_visited (make_mark_state Q J) = Q \ J" + by transfer auto + +function mark where + "mark ms \ + (let Q = get_visited ms; I = get_next ms in + if I \ finals \ {} then True + else let J = (\(q,w,q')\transition_relation. if q \ I \ q' \ Q then {q'} else {}) in + if J = {} then False else mark (make_mark_state Q J))" + by auto +termination by (relation "measure (\ms. card (UNIV :: 'a set) - card (get_visited ms :: 'a set))") + (fastforce intro!: diff_less_mono2 psubset_card_mono split: if_splits)+ + +declare mark.simps[simp del] + +lemma trapped_transitions: "(p, w, q) \ trans_star \ + \p \ Q. (\\ q. (p, \, q) \ transition_relation \ q \ Q) \ + p \ Q \ q \ Q" + by (induct p w q rule: trans_star.induct) auto + +lemma mark_complete: "(p, w, q) \ trans_star \ (get_visited ms - get_next ms) \ finals = {} \ + \p \ get_visited ms - get_next ms. \q \. (p, \, q) \ transition_relation \ q \ get_visited ms \ + p \ get_visited ms \ q \ finals \ mark ms" +proof (induct p w q arbitrary: ms rule: trans_star.induct) + case (trans_star_refl p) + then show ?case by (subst mark.simps) (auto simp: Let_def) +next + case step: (trans_star_step p \ q' w q) + define J where "J \ \(q, w, q')\transition_relation. if q \ get_next ms \ q' \ get_visited ms then {q'} else {}" + show ?case + proof (cases "J = {}") + case True + then have "q' \ get_visited ms" + by (smt (z3) DiffI Diff_disjoint Int_iff J_def SUP_bot_conv(2) case_prod_conv insertI1 + step.hyps(1) step.prems(2) step.prems(3)) + with True show ?thesis + using step(1,2,4,5,7) + by (subst mark.simps) + (auto 10 0 intro!: step(3) elim!: set_mp[of _ "get_next ms"] simp: split_beta J_def + dest: trapped_transitions[of q' w q "get_visited ms"]) + next + case False + then have [simp]: "get_visited ms \ J - J = get_visited ms" + by (auto simp: J_def split: if_splits) + then have "p \ get_visited ms \ (p, \, q) \ transition_relation \ q \ get_visited ms \ q \ J" for p \ q + using step(5) + by (cases "p \ get_next ms") + (auto simp only: J_def simp_thms if_True if_False intro!: UN_I[of "(p, \, q)"]) + with False show ?thesis + using step(1,4,5,6,7) + by (subst mark.simps) + (auto 0 2 simp add: Let_def J_def[symmetric] disj_commute + intro!: step(3)[of "make_mark_state (get_visited ms) J"]) + qed +qed + + +lemma mark_sound: "mark ms \ (\p \ get_next ms. \q \ finals. \w. (p, w, q) \ trans_star)" + by (induct ms rule: mark.induct) + (subst (asm) (2) mark.simps, fastforce dest: trans_star_step simp: Let_def split: if_splits) + +lemma nonempty_code[code]: "nonempty = mark (make_mark_state {} (set (map Init Enum.enum)))" + using mark_complete[of _ _ _ "make_mark_state {} initials"] + mark_sound[of "make_mark_state {} initials"] nonempty_alt + unfolding initials_def initials_list[symmetric] by auto + + +end + + +subsection \Intersection P-Automaton locale\ + +locale Intersection_P_Automaton = + A1: P_Automaton ts1 Init finals1 + + A2: P_Automaton ts2 Init finals2 + for ts1 :: "('state :: finite, 'label) transition set" + and Init :: "'ctr_loc :: enum \ 'state" + and finals1 :: "'state set" + and ts2 :: "('state, 'label) transition set" + and finals2 :: "'state set" +begin + +sublocale pa: P_Automaton "inters ts1 ts2" "(\p. (Init p, Init p))" "inters_finals finals1 finals2" + . + +definition accepts_aut_inters where + "accepts_aut_inters p w = pa.accepts_aut p w" + +definition lang_aut_inters :: "('ctr_loc * 'label list) set" where + "lang_aut_inters = {(p,w). accepts_aut_inters p w}" + +lemma trans_star_inter: + assumes "(p1, w, p2) \ A1.trans_star" + assumes "(q1, w, q2) \ A2.trans_star" + shows "((p1,q1), w :: 'label list, (p2,q2)) \ pa.trans_star" + using assms +proof (induction w arbitrary: p1 q1) + case (Cons \ w1') + obtain p' where p'_p: "(p1, \, p') \ ts1 \ (p', w1', p2) \ A1.trans_star" + using Cons by (metis LTS.trans_star_cons) + obtain q' where q'_p: "(q1, \, q') \ ts2 \(q', w1', q2) \ A2.trans_star" + using Cons by (metis LTS.trans_star_cons) + have ind: "((p', q'), w1', p2, q2) \ pa.trans_star" + proof - + have "Suc (length w1') = length (\#w1')" + by auto + moreover + have "(p', w1', p2) \ A1.trans_star" + using p'_p by simp + moreover + have "(q', w1', q2) \ A2.trans_star" + using q'_p by simp + ultimately + show "((p', q'), w1', p2, q2) \ pa.trans_star" + using Cons(1) by auto + qed + moreover + have "((p1, q1), \, (p', q')) \ (inters ts1 ts2)" + by (simp add: inters_def p'_p q'_p) + ultimately + have "((p1, q1), \#w1', p2, q2) \ pa.trans_star" + by (meson LTS.trans_star.trans_star_step) + moreover + have "length ((\#w1')) > 0" + by auto + moreover + have "hd ((\#w1')) = \" + by auto + ultimately + show ?case + by force +next + case Nil + then show ?case + by (metis LTS.trans_star.trans_star_refl LTS.trans_star_empty) +qed + +lemma inters_trans_star1: + assumes "(p1q2, w :: 'label list, p2q2) \ pa.trans_star" + shows "(fst p1q2, w, fst p2q2) \ A1.trans_star" + using assms +proof (induction rule: LTS.trans_star.induct[OF assms(1)]) + case (1 p) + then show ?case + by (simp add: LTS.trans_star.trans_star_refl) +next + case (2 p \ q' w q) + then have ind: "(fst q', w, fst q) \ A1.trans_star" + by auto + from 2(1) have "(p, \, q') \ + {((p1, q1), \, p2, q2) |p1 q1 \ p2 q2. (p1, \, p2) \ ts1 \ (q1, \, q2) \ ts2}" + unfolding inters_def by auto + then have "\p1 q1. p = (p1, q1) \ (\p2 q2. q' = (p2, q2) \ (p1, \, p2) \ ts1 \ (q1, \, q2) \ ts2)" + by simp + then obtain p1 q1 where "p = (p1, q1) \ (\p2 q2. q' = (p2, q2) \ (p1, \, p2) \ ts1 \ (q1, \, q2) \ ts2)" + by auto + then show ?case + using LTS.trans_star.trans_star_step ind by fastforce +qed + +lemma inters_trans_star: + assumes "(p1q2, w :: 'label list, p2q2) \ pa.trans_star" + shows "(snd p1q2, w, snd p2q2) \ A2.trans_star" + using assms +proof (induction rule: LTS.trans_star.induct[OF assms(1)]) + case (1 p) + then show ?case + by (simp add: LTS.trans_star.trans_star_refl) +next + case (2 p \ q' w q) + then have ind: "(snd q', w, snd q) \ A2.trans_star" + by auto + from 2(1) have "(p, \, q') \ + {((p1, q1), \, p2, q2) |p1 q1 \ p2 q2. (p1, \, p2) \ ts1 \ (q1, \, q2) \ ts2}" + unfolding inters_def by auto + then have "\p1 q1. p = (p1, q1) \ (\p2 q2. q' = (p2, q2) \ (p1, \, p2) \ ts1 \ (q1, \, q2) \ ts2)" + by simp + then obtain p1 q1 where "p = (p1, q1) \ (\p2 q2. q' = (p2, q2) \ (p1, \, p2) \ ts1 \ (q1, \, q2) \ ts2)" + by auto + then show ?case + using LTS.trans_star.trans_star_step ind by fastforce +qed + +lemma inters_trans_star_iff: + "((p1,q2), w :: 'label list, (p2,q2)) \ pa.trans_star \ (p1, w, p2) \ A1.trans_star \ (q2, w, q2) \ A2.trans_star" + by (metis fst_conv inters_trans_star inters_trans_star1 snd_conv trans_star_inter) + +lemma inters_accept_iff: "accepts_aut_inters p w \ A1.accepts_aut p w \ A2.accepts_aut p w" +proof + assume "accepts_aut_inters p w" + then show "A1.accepts_aut p w \ A2.accepts_aut p w" + unfolding accepts_aut_inters_def A1.accepts_aut_def A2.accepts_aut_def pa.accepts_aut_def + unfolding inters_finals_def + using inters_trans_star_iff[of _ _ w _ ] + using SigmaE fst_conv inters_trans_star inters_trans_star1 snd_conv + by (metis (no_types, lifting)) +next + assume a: "A1.accepts_aut p w \ A2.accepts_aut p w" + then have "(\q\finals1. (Init p, w, q) \ A1.trans_star) \ + (\q\finals2. (Init p, w, q) \ A2.trans_star)" + unfolding A1.accepts_aut_def A2.accepts_aut_def by auto + then show "accepts_aut_inters p w" + unfolding accepts_aut_inters_def pa.accepts_aut_def inters_finals_def + by (auto simp: P_Automaton.accepts_aut_def intro: trans_star_inter) +qed + +lemma lang_aut_alt: + "pa.lang_aut = {(p, w). (p, w) \ lang_aut_inters}" + unfolding pa.lang_aut_def lang_aut_inters_def accepts_aut_inters_def pa.accepts_aut_def + by auto + +lemma inters_lang: "lang_aut_inters = A1.lang_aut \ A2.lang_aut" + unfolding lang_aut_inters_def A1.lang_aut_def A2.lang_aut_def using inters_accept_iff by auto + +end + + +section \Automata with epsilon\ + + +subsection \P-Automaton with epsilon locale\ + +locale P_Automaton_\ = LTS_\ transition_relation for transition_relation :: "('state::finite, 'label option) transition set" + + fixes finals :: "'state set" and Init :: "'ctr_loc :: enum \ 'state" +begin + +definition accepts_aut_\ :: "'ctr_loc \ 'label list \ bool" where + "accepts_aut_\ \ \p w. (\q \ finals. (Init p, w, q) \ trans_star_\)" + +definition lang_aut_\ :: "('ctr_loc * 'label list) set" where + "lang_aut_\ = {(p,w). accepts_aut_\ p w}" + +definition nonempty_\ where + "nonempty_\ \ lang_aut_\ \ {}" + +end + + +subsection \Intersection P-Automaton with epsilon locale\ + +locale Intersection_P_Automaton_\ = + A1: P_Automaton_\ ts1 finals1 Init + + A2: P_Automaton_\ ts2 finals2 Init + for ts1 :: "('state :: finite, 'label option) transition set" + and finals1 :: "'state set" + and Init :: "'ctr_loc :: enum \ 'state" + and ts2 :: "('state, 'label option) transition set" + and finals2 :: "'state set" +begin + +abbreviation \ :: "'label option" where + "\ == None" + +sublocale pa: P_Automaton_\ "inters_\ ts1 ts2" "inters_finals finals1 finals2" "(\p. (Init p, Init p))" + . + +definition accepts_aut_inters_\ where + "accepts_aut_inters_\ p w = pa.accepts_aut_\ p w" + +definition lang_aut_inters_\ :: "('ctr_loc * 'label list) set" where + "lang_aut_inters_\ = {(p,w). accepts_aut_inters_\ p w}" + + +lemma trans_star_trans_star_\_inter: + assumes "LTS_\.\_exp w1 w" + assumes "LTS_\.\_exp w2 w" + assumes "(p1, w1, p2) \ A1.trans_star" + assumes "(q1, w2, q2) \ A2.trans_star" + shows "((p1,q1), w :: 'label list, (p2,q2)) \ pa.trans_star_\" + using assms +proof (induction "length w1 + length w2" arbitrary: w1 w2 w p1 q1 rule: less_induct) + case less + then show ?case + proof (cases "\\ w1' w2' \. w1=Some \#w1' \ w2=Some \#w2'") + case True + from True obtain \ \ w1' w2' where True'': + "w1=Some \#w1'" + "w2=Some \#w2'" + by auto + have "\ = \" + by (metis True''(1) True''(2) LTS_\.\_exp_Some_hd less.prems(1) less.prems(2)) + then have True': + "w1=Some \#w1'" + "w2=Some \#w2'" + using True'' by auto + define w' where "w' = tl w" + obtain p' where p'_p: "(p1, Some \, p') \ ts1 \ (p', w1', p2) \ A1.trans_star" + using less True'(1) by (metis LTS_\.trans_star_cons_\) + obtain q' where q'_p: "(q1, Some \, q') \ ts2 \(q', w2', q2) \ A2.trans_star" + using less True'(2) by (metis LTS_\.trans_star_cons_\) + have ind: "((p', q'), w', p2, q2) \ pa.trans_star_\" + proof - + have "length w1' + length w2' < length w1 + length w2" + using True'(1) True'(2) by simp + moreover + have "LTS_\.\_exp w1' w'" + by (metis (no_types) LTS_\.\_exp_def less(2) True'(1) list.map(2) list.sel(3) + option.simps(3) removeAll.simps(2) w'_def) + moreover + have "LTS_\.\_exp w2' w'" + by (metis (no_types) LTS_\.\_exp_def less(3) True'(2) list.map(2) list.sel(3) + option.simps(3) removeAll.simps(2) w'_def) + moreover + have "(p', w1', p2) \ A1.trans_star" + using p'_p by simp + moreover + have "(q', w2', q2) \ A2.trans_star" + using q'_p by simp + ultimately + show "((p', q'), w', p2, q2) \ pa.trans_star_\" + using less(1)[of w1' w2' w' p' q'] by auto + qed + moreover + have "((p1, q1), Some \, (p', q')) \ (inters_\ ts1 ts2)" + by (simp add: inters_\_def p'_p q'_p) + ultimately + have "((p1, q1), \#w', p2, q2) \ pa.trans_star_\" + by (meson LTS_\.trans_star_\.trans_star_\_step_\) + moreover + have "length w > 0" + using less(3) True' LTS_\.\_exp_Some_length by metis + moreover + have "hd w = \" + using less(3) True' LTS_\.\_exp_Some_hd by metis + ultimately + show ?thesis + using w'_def by force + next + case False + note False_outer_outer_outer_outer = False + show ?thesis + proof (cases "w1 = [] \ w2 = []") + case True + then have same: "p1 = p2 \ q1 = q2" + by (metis LTS.trans_star_empty less.prems(3) less.prems(4)) + have "w = []" + using True less(2) LTS_\.exp_empty_empty by auto + then show ?thesis + using less True + by (simp add: LTS_\.trans_star_\.trans_star_\_refl same) + next + case False + note False_outer_outer_outer = False + show ?thesis + proof (cases "\w1'. w1=\#w1'") + case True (* Adapted from above. Maybe they can be merged. *) + then obtain w1' where True': + "w1=\#w1'" + by auto + obtain p' where p'_p: "(p1, \, p') \ ts1 \ (p', w1', p2) \ A1.trans_star" + using less True'(1) by (metis LTS_\.trans_star_cons_\) + have q'_p: "(q1, w2, q2) \ A2.trans_star" + using less by metis + have ind: "((p', q1), w, p2, q2) \ pa.trans_star_\" + proof - + have "length w1' + length w2 < length w1 + length w2" + using True'(1) by simp + moreover + have "LTS_\.\_exp w1' w" + by (metis (no_types) LTS_\.\_exp_def less(2) True'(1) removeAll.simps(2)) + moreover + have "LTS_\.\_exp w2 w" + by (metis (no_types) less(3)) + moreover + have "(p', w1', p2) \ A1.trans_star" + using p'_p by simp + moreover + have "(q1, w2, q2) \ A2.trans_star" + using q'_p by simp + ultimately + show "((p', q1), w, p2, q2) \ pa.trans_star_\" + using less(1)[of w1' w2 w p' q1] by auto + qed + moreover + have "((p1, q1), \, (p', q1)) \ (inters_\ ts1 ts2)" + by (simp add: inters_\_def p'_p q'_p) + ultimately + have "((p1, q1), w, p2, q2) \ pa.trans_star_\" + using LTS_\.trans_star_\.simps by fastforce + then + show ?thesis + by force + next + case False + note False_outer_outer = False + then show ?thesis + proof (cases "\w2'. w2 = \ # w2'") + case True (* Adapted from above. Maybe they can be merged. *) + then obtain w2' where True': + "w2=\#w2'" + by auto + have p'_p: "(p1, w1, p2) \ A1.trans_star" + using less by (metis) + obtain q' where q'_p: "(q1, \, q') \ ts2 \(q', w2', q2) \ A2.trans_star" + using less True'(1) by (metis LTS_\.trans_star_cons_\) + have ind: "((p1, q'), w, p2, q2) \ pa.trans_star_\" + proof - + have "length w1 + length w2' < length w1 + length w2" + using True'(1) True'(1) by simp + moreover + have "LTS_\.\_exp w1 w" + by (metis (no_types) less(2)) + moreover + have "LTS_\.\_exp w2' w" + by (metis (no_types) LTS_\.\_exp_def less(3) True'(1) removeAll.simps(2)) + moreover + have "(p1, w1, p2) \ A1.trans_star" + using p'_p by simp + moreover + have "(q', w2', q2) \ A2.trans_star" + using q'_p by simp + ultimately + show "((p1, q'), w, p2, q2) \ pa.trans_star_\" + using less(1)[of w1 w2' w p1 q'] by auto + qed + moreover + have "((p1, q1), \, (p1, q')) \ inters_\ ts1 ts2" + by (simp add: inters_\_def p'_p q'_p) + ultimately + have "((p1, q1), w, p2, q2) \ pa.trans_star_\" + using LTS_\.trans_star_\.simps by fastforce + then + show ?thesis + by force + next + case False + then have "(w1 = [] \ (\\ w2'. w2 = Some \ # w2')) \ ((\\ w1'. w1 = Some \ # w1') \ w2 = [])" + using False_outer_outer False_outer_outer_outer False_outer_outer_outer_outer + by (metis neq_Nil_conv option.exhaust_sel) + then show ?thesis + by (metis LTS_\.\_exp_def LTS_\.\_exp_Some_length less.prems(1) less.prems(2) + less_numeral_extra(3) list.simps(8) list.size(3) removeAll.simps(1)) + qed + qed + qed + qed +qed + +lemma trans_star_\_inter: + assumes "(p1, w :: 'label list, p2) \ A1.trans_star_\" + assumes "(q1, w, q2) \ A2.trans_star_\" + shows "((p1, q1), w, (p2, q2)) \ pa.trans_star_\" +proof - + have "\w1'. LTS_\.\_exp w1' w \ (p1, w1', p2) \ A1.trans_star" + using assms by (simp add: LTS_\.trans_star_\_\_exp_trans_star) + then obtain w1' where "LTS_\.\_exp w1' w \ (p1, w1', p2) \ A1.trans_star" + by auto + moreover + have "\w2'. LTS_\.\_exp w2' w \ (q1, w2', q2) \ A2.trans_star" + using assms by (simp add: LTS_\.trans_star_\_\_exp_trans_star) + then obtain w2' where "LTS_\.\_exp w2' w \ (q1, w2', q2) \ A2.trans_star" + by auto + ultimately + show ?thesis + using trans_star_trans_star_\_inter by metis +qed + +lemma inters_trans_star_\1: + assumes "(p1q2, w :: 'label list, p2q2) \ pa.trans_star_\" + shows "(fst p1q2, w, fst p2q2) \ A1.trans_star_\" + using assms +proof (induction rule: LTS_\.trans_star_\.induct[OF assms(1)]) + case (1 p) + then show ?case + by (simp add: LTS_\.trans_star_\.trans_star_\_refl) +next + case (2 p \ q' w q) + then have ind: "(fst q', w, fst q) \ A1.trans_star_\" + by auto + from 2(1) have "(p, Some \, q') \ + {((p1, q1), \, p2, q2) |p1 q1 \ p2 q2. (p1, \, p2) \ ts1 \ (q1, \, q2) \ ts2} \ + {((p1, q1), \, p2, q1) |p1 p2 q1. (p1, \, p2) \ ts1} \ + {((p1, q1), \, p1, q2) |p1 q1 q2. (q1, \, q2) \ ts1}" + unfolding inters_\_def by auto + moreover + { + assume "(p, Some \, q') \ {((p1, q1), \, p2, q2) |p1 q1 \ p2 q2. (p1, \, p2) \ ts1 \ (q1, \, q2) \ ts2}" + then have "\p1 q1. p = (p1, q1) \ (\p2 q2. q' = (p2, q2) \ (p1, Some \, p2) \ ts1 \ (q1, Some \, q2) \ ts2)" + by simp + then obtain p1 q1 where "p = (p1, q1) \ (\p2 q2. q' = (p2, q2) \ (p1, Some \, p2) \ ts1 \ (q1, Some \, q2) \ ts2)" + by auto + then have ?case + using LTS_\.trans_star_\.trans_star_\_step_\ ind by fastforce + } + moreover + { + assume "(p, Some \, q') \ {((p1, q1), \, p2, q1) |p1 p2 q1. (p1, \, p2) \ ts1}" + then have ?case + by auto + } + moreover + { + assume "(p, Some \, q') \ {((p1, q1), \, p1, q2) |p1 q1 q2. (q1, \, q2) \ ts1}" + then have ?case + by auto + } + ultimately + show ?case + by auto +next + case (3 p q' w q) + then have ind: "(fst q', w, fst q) \ A1.trans_star_\" + by auto + from 3(1) have "(p, \, q') \ + {((p1, q1), \, (p2, q2)) | p1 q1 \ p2 q2. (p1, \, p2) \ ts1 \ (q1, \, q2) \ ts2} \ + {((p1, q1), \, (p2, q1)) | p1 p2 q1. (p1, \, p2) \ ts1} \ + {((p1, q1), \, (p1, q2)) | p1 q1 q2. (q1, \, q2) \ ts2}" + unfolding inters_\_def by auto + moreover + { + assume "(p, \, q') \ {((p1, q1), \, p2, q2) |p1 q1 \ p2 q2. (p1, \, p2) \ ts1 \ (q1, \, q2) \ ts2}" + then have "\p1 q1. p = (p1, q1) \ (\p2 q2. q' = (p2, q2) \ (p1, \, p2) \ ts1 \ (q1, \, q2) \ ts2)" + by simp + then obtain p1 q1 where "p = (p1, q1) \ (\p2 q2. q' = (p2, q2) \ (p1, \, p2) \ ts1 \ (q1, \, q2) \ ts2)" + by auto + then have ?case + using LTS_\.trans_star_\.trans_star_\_step_\ ind by fastforce + } + moreover + { + assume "(p, \, q') \ {((p1, q1), \, p2, q1) |p1 p2 q1. (p1, \, p2) \ ts1}" + then have "\p1 p2 q1. p = (p1, q1) \ q' = (p2, q1) \ (p1, \, p2) \ ts1" + by auto + then obtain p1 p2 q1 where "p = (p1, q1) \ q' = (p2, q1) \ (p1, \, p2) \ ts1" + by auto + then have ?case + using LTS_\.trans_star_\.trans_star_\_step_\ ind by fastforce + } + moreover + { + assume "(p, \, q') \ {((p1, q1), \, p1, q2) |p1 q1 q2. (q1, \, q2) \ ts2}" + then have "\p1 q1 q2. p = (p1, q1) \ q' = (p1, q2) \ (q1, \, q2) \ ts2" + by auto + then obtain p1 q1 q2 where "p = (p1, q1) \ q' = (p1, q2) \ (q1, \, q2) \ ts2" + by auto + then have ?case + using LTS_\.trans_star_\.trans_star_\_step_\ ind by fastforce + } + ultimately + show ?case + by auto +qed + +lemma inters_trans_star_\: + assumes "(p1q2, w :: 'label list, p2q2) \ pa.trans_star_\" + shows "(snd p1q2, w, snd p2q2) \ A2.trans_star_\" + using assms +proof (induction rule: LTS_\.trans_star_\.induct[OF assms(1)]) + case (1 p) + then show ?case + by (simp add: LTS_\.trans_star_\.trans_star_\_refl) +next + case (2 p \ q' w q) + then have ind: "(snd q', w, snd q) \ A2.trans_star_\" + by auto + from 2(1) have "(p, Some \, q') \ + {((p1, q1), \, p2, q2) |p1 q1 \ p2 q2. (p1, \, p2) \ ts1 \ (q1, \, q2) \ ts2} \ + {((p1, q1), \, p2, q1) |p1 p2 q1. (p1, \, p2) \ ts1} \ + {((p1, q1), \, p1, q2) |p1 q1 q2. (q1, \, q2) \ ts2}" + unfolding inters_\_def by auto + moreover + { + assume "(p, Some \, q') \ {((p1, q1), \, p2, q2) |p1 q1 \ p2 q2. (p1, \, p2) \ ts1 \ (q1, \, q2) \ ts2}" + then have "\p1 q1. p = (p1, q1) \ (\p2 q2. q' = (p2, q2) \ (p1, Some \, p2) \ ts1 \ (q1, Some \, q2) \ ts2)" + by simp + then obtain p1 q1 where "p = (p1, q1) \ (\p2 q2. q' = (p2, q2) \ (p1, Some \, p2) \ ts1 \ (q1, Some \, q2) \ ts2)" + by auto + then have ?case + using LTS_\.trans_star_\.trans_star_\_step_\ ind by fastforce + } + moreover + { + assume "(p, Some \, q') \ {((p1, q1), \, p2, q1) |p1 p2 q1. (p1, \, p2) \ ts1}" + then have ?case + by auto + } + moreover + { + assume "(p, Some \, q') \ {((p1, q1), \, p1, q2) |p1 q1 q2. (q1, \, q2) \ ts2}" + then have ?case + by auto + } + ultimately + show ?case + by auto +next + case (3 p q' w q) + then have ind: "(snd q', w, snd q) \ A2.trans_star_\" + by auto + from 3(1) have "(p, \, q') \ + {((p1, q1), \, (p2, q2)) | p1 q1 \ p2 q2. (p1, \, p2) \ ts1 \ (q1, \, q2) \ ts2} \ + {((p1, q1), \, (p2, q1)) | p1 p2 q1. (p1, \, p2) \ ts1} \ + {((p1, q1), \, (p1, q2)) | p1 q1 q2. (q1, \, q2) \ ts2}" + unfolding inters_\_def by auto + moreover + { + assume "(p, \, q') \ {((p1, q1), \, p2, q2) |p1 q1 \ p2 q2. (p1, \, p2) \ ts1 \ (q1, \, q2) \ ts2}" + then have "\p1 q1. p = (p1, q1) \ (\p2 q2. q' = (p2, q2) \ (p1, \, p2) \ ts1 \ (q1, \, q2) \ ts2)" + by simp + then obtain p1 q1 where "p = (p1, q1) \ (\p2 q2. q' = (p2, q2) \ (p1, \, p2) \ ts1 \ (q1, \, q2) \ ts2)" + by auto + then have ?case + using LTS_\.trans_star_\.trans_star_\_step_\ ind by fastforce + } + moreover + { + assume "(p, \, q') \ {((p1, q1), \, p2, q1) |p1 p2 q1. (p1, \, p2) \ ts1}" + then have "\p1 p2 q1. p = (p1, q1) \ q' = (p2, q1) \ (p1, \, p2) \ ts1" + by auto + then obtain p1 p2 q1 where "p = (p1, q1) \ q' = (p2, q1) \ (p1, \, p2) \ ts1" + by auto + then have ?case + using LTS_\.trans_star_\.trans_star_\_step_\ ind by fastforce + } + moreover + { + assume "(p, \, q') \ {((p1, q1), \, p1, q2) |p1 q1 q2. (q1, \, q2) \ ts2}" + then have "\p1 q1 q2. p = (p1, q1) \ q' = (p1, q2) \ (q1, \, q2) \ ts2" + by auto + then obtain p1 q1 q2 where "p = (p1, q1) \ q' = (p1, q2) \ (q1, \, q2) \ ts2" + by auto + then have ?case + using LTS_\.trans_star_\.trans_star_\_step_\ ind by fastforce + } + ultimately + show ?case + by auto +qed + +lemma inters_trans_star_\_iff: + "((p1,q2), w :: 'label list, (p2,q2)) \ pa.trans_star_\ \ + (p1, w, p2) \ A1.trans_star_\ \ (q2, w, q2) \ A2.trans_star_\" + by (metis fst_conv inters_trans_star_\ inters_trans_star_\1 snd_conv trans_star_\_inter) + +lemma inters_\_accept_\_iff: + "accepts_aut_inters_\ p w \ A1.accepts_aut_\ p w \ A2.accepts_aut_\ p w" +proof + assume "accepts_aut_inters_\ p w" + then show "A1.accepts_aut_\ p w \ A2.accepts_aut_\ p w" + unfolding accepts_aut_inters_\_def A1.accepts_aut_\_def A2.accepts_aut_\_def pa.accepts_aut_\_def + unfolding inters_finals_def + using inters_trans_star_\_iff[of _ _ w _ ] + using SigmaE fst_conv inters_trans_star_\ inters_trans_star_\1 snd_conv + by (metis (no_types, lifting)) +next + assume a: "A1.accepts_aut_\ p w \ A2.accepts_aut_\ p w" + then have "(\q\finals1. (Init p, w, q) \ A1.trans_star_\) \ + (\q\finals2. (Init p, w, q) \ LTS_\.trans_star_\ ts2)" + unfolding A1.accepts_aut_\_def A2.accepts_aut_\_def by auto + then show "accepts_aut_inters_\ p w" + unfolding accepts_aut_inters_\_def pa.accepts_aut_\_def inters_finals_def + by (auto simp: P_Automaton_\.accepts_aut_\_def intro: trans_star_\_inter) +qed + +lemma inters_\_lang_\: "lang_aut_inters_\ = A1.lang_aut_\ \ A2.lang_aut_\" + unfolding lang_aut_inters_\_def P_Automaton_\.lang_aut_\_def using inters_\_accept_\_iff by auto + +end + +end diff --git a/thys/Pushdown_Systems/ROOT b/thys/Pushdown_Systems/ROOT new file mode 100644 --- /dev/null +++ b/thys/Pushdown_Systems/ROOT @@ -0,0 +1,14 @@ +chapter AFP + +session Pushdown_Systems = "Labeled_Transition_Systems" + + options [timeout = 300] + theories + P_Automata + PDS + PDS_Code + theories [document = false] + Ex + document_files + "root.bib" + "root.tex" + diff --git a/thys/Pushdown_Systems/document/root.bib b/thys/Pushdown_Systems/document/root.bib new file mode 100644 --- /dev/null +++ b/thys/Pushdown_Systems/document/root.bib @@ -0,0 +1,227 @@ +@inproceedings{DBLP:conf/atva/JensenSSSVD21, + author = {Peter Gj{\o}l Jensen and + Stefan Schmid and + Morten Konggaard Schou and + Jir{\'{\i}} Srba and + Juan Vanerio and + Ingo van Duijn}, + editor = {Zhe Hou and + Vijay Ganesh}, + title = {Faster Pushdown Reachability Analysis with Applications in Network + Verification}, + booktitle = {Automated Technology for Verification and Analysis - 19th International + Symposium, {ATVA} 2021, Gold Coast, QLD, Australia, October 18-22, + 2021, Proceedings}, + series = {Lecture Notes in Computer Science}, + volume = {12971}, + pages = {170--186}, + publisher = {Springer}, + year = {2021}, + url = {https://doi.org/10.1007/978-3-030-88885-5\_12}, + doi = {10.1007/978-3-030-88885-5\_12}, + timestamp = {Tue, 21 Mar 2023 20:59:41 +0100}, + biburl = {https://dblp.org/rec/conf/atva/JensenSSSVD21.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@phdthesis{schwoon2002model, + author = {Stefan Schwoon}, +title = {Model checking pushdown systems}, +school = {Technical University Munich, Germany}, +year = {2002}, +note = {\url{https://d-nb.info/96638976X/34}}, +} + +@inproceedings{DBLP:conf/fmcad/SchlichtkrullSST22, + author = {Anders Schlichtkrull and + Morten Konggaard Schou and + Jir{\'{\i}} Srba and + Dmitriy Traytel}, + editor = {Alberto Griggio and + Neha Rungta}, + title = {Differential Testing of Pushdown Reachability with a Formally Verified + Oracle}, + booktitle = {22nd Formal Methods in Computer-Aided Design, {FMCAD} 2022, Trento, + Italy, October 17-21, 2022}, + pages = {369--379}, + publisher = {{IEEE}}, + year = {2022}, + url = {https://doi.org/10.34727/2022/isbn.978-3-85448-053-2\_44}, + doi = {10.34727/2022/isbn.978-3-85448-053-2\_44}, + timestamp = {Tue, 21 Mar 2023 21:02:10 +0100}, + biburl = {https://dblp.org/rec/conf/fmcad/SchlichtkrullSST22.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@article{buchi1964regular, + title={Regular canonical systems}, + author={B{\"u}chi, J Richard}, + journal={Archiv f{\"u}r mathematische Logik und Grundlagenforschung}, + volume={6}, + number={3-4}, + pages={91--111}, + year={1964}, + publisher={Springer}, + doi={https://doi.org/10.1007/BF01969548} +} + +@inproceedings{esparza1999automata, + author = {Javier Esparza and +Jens Knoop}, +editor = {Wolfgang Thomas}, +title = {An Automata-Theoretic Approach to Interprocedural Data-Flow Analysis}, +booktitle = {FoSSaCS 1999}, +series = {LNCS}, +volume = {1578}, +pages = {14--30}, +publisher = {Springer}, +year = {1999}, +doi = {10.1007/3-540-49019-1\_2}, +} + +@inproceedings{conway2005incremental, + author = {Christopher L. Conway and +Kedar S. Namjoshi and +Dennis Dams and +Stephen A. Edwards}, +editor = {Kousha Etessami and +Sriram K. Rajamani}, +title = {Incremental Algorithms for Inter-procedural Analysis of Safety Properties}, +booktitle = {{CAV} 2005}, +series = {LNCS}, +volume = {3576}, +pages = {449--461}, +publisher = {Springer}, +year = {2005}, +doi = {10.1007/11513988\_45}, +} + +@inproceedings{esparza2001bdd, + author = {Javier Esparza and +Stefan Schwoon}, +editor = {G{\'{e}}rard Berry and +Hubert Comon and +Alain Finkel}, +title = {A BDD-Based Model Checker for Recursive Programs}, +booktitle = {CAV 2001}, +series = {LNCS}, +volume = {2102}, +pages = {324--336}, +publisher = {Springer}, +year = {2001}, +doi = {10.1007/3-540-44585-4\_30}, +} + +@inproceedings{moped, + title={Moped}, + author={Stefan Schwoon}, + note={\url{http://www2.informatik.uni-stuttgart.de/fmi/szs/tools/moped/}}, + year={2002}, +} + +@inproceedings{jmoped, +author = {Dejvuth Suwimonteerabuth and +Stefan Schwoon and +Javier Esparza}, +editor = {Nicolas Halbwachs and +Lenore D. Zuck}, +title = {{jMoped}: {A} {J}ava Bytecode Checker Based on {Moped}}, +booktitle = {{TACAS} 2005}, +series = {LNCS}, +volume = {3440}, +pages = {541--545}, +publisher = {Springer}, +year = {2005}, +doi = {10.1007/978-3-540-31980-1\_35}, +} + +@inproceedings{bouajjani1997reachability, + author = {Ahmed Bouajjani and +Javier Esparza and +Oded Maler}, +editor = {Antoni W. Mazurkiewicz and +J{\'{o}}zef Winkowski}, +title = {Reachability Analysis of Pushdown Automata: Application to Model-Checking}, +booktitle = {{CONCUR} 1997}, +series = {LNCS}, +volume = {1243}, +pages = {135--150}, +publisher = {Springer}, +year = {1997}, +doi = {10.1007/3-540-63141-0\_10}, +} + +@inproceedings{JKMSST:coNEXT:18, + author = {Jesper Stenbjerg Jensen and +Troels Beck Kr{\o}gh and +Jonas Sand Madsen and +Stefan Schmid and +Jir{\'{\i}} Srba and +Marc Tom Thorgersen}, +editor = {Xenofontas A. Dimitropoulos and +Alberto Dainotti and +Laurent Vanbever and +Theophilus Benson}, +title = {P-{Rex}: fast verification of {MPLS} networks with multiple link failures}, +booktitle = {CoNEXT 2018}, +pages = {217--227}, +publisher = {{ACM}}, +year = {2018}, +doi = {10.1145/3281411.3281432}, +} + +@inproceedings{jensen2020aalwines, + author = {Peter Gj{\o}l Jensen and +Dan Kristiansen and +Stefan Schmid and +Morten Konggaard Schou and +Bernhard Clemens Schrenk and +Jir{\'{\i}} Srba}, +editor = {Dongsu Han and +Anja Feldmann}, +title = {{AalWiNes}: a fast and quantitative what-if analysis tool for {MPLS} +networks}, +booktitle = {CoNEXT 2020}, +pages = {474--481}, +publisher = {{ACM}}, +year = {2020}, +doi = {10.1145/3386367.3431308}, +} + +@article{DJJKMSST:TON:21, +author ={I. van Duijn and P.G. Jensen and J.S. Jensen and T.B. Kr{\o}gh and J.S. Madsen and S. Schmid and J. Srba and M.T. Thorgersen}, +title ={Automata-Theoretic Approach to Verification of {MPLS} Networks under Link Failures}, +journal ={IEEE/ACM Transactions on Networking}, +year ={2021}, +volume ={}, +number ={}, +publisher ={IEEE}, +pages ={1--16}, +pdf ={http://www.cs.aau.dk/~srba/files/DJJKMSST:TON:21.pdf}, +ee ={https://ieeexplore.ieee.org/document/9619760}, +doi ={10.1109/TNET.2021.3126572}, +} + +@misc{Lammich-DPN, + author={Peter Lammich}, + title={Formalization of Dynamic Pushdown Networks in {I}sabelle/{HOL}}, + year={2009}, + note={\url{https://www21.in.tum.de/~lammich/isabelle/dpn-document.pdf}} +} + +@inproceedings{DBLP:conf/cav/LammichMW09, + author = {Peter Lammich and + Markus M{\"{u}}ller{-}Olm and + Alexander Wenner}, + editor = {Ahmed Bouajjani and + Oded Maler}, + title = {Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints}, + booktitle = {{CAV} 2009}, + series = {LNCS}, + volume = {5643}, + pages = {525--539}, + publisher = {Springer}, + year = {2009}, + doi = {10.1007/978-3-642-02658-4\_39} +} + diff --git a/thys/Pushdown_Systems/document/root.tex b/thys/Pushdown_Systems/document/root.tex new file mode 100644 --- /dev/null +++ b/thys/Pushdown_Systems/document/root.tex @@ -0,0 +1,75 @@ +\documentclass[10pt,a4paper]{article} +\usepackage[T1]{fontenc} +\usepackage{amssymb} +\usepackage[left=2.25cm,right=2.25cm,top=2.25cm,bottom=2.75cm]{geometry} +\usepackage{graphicx} +\usepackage{isabelle} +\usepackage{isabellesym} +\usepackage[only,bigsqcap]{stmaryrd} +\usepackage{pdfsetup} + +\urlstyle{tt} +\isabellestyle{it} + +\renewcommand{\isacharunderscore}{\_} +\renewcommand{\isachardoublequoteopen}{``} +\renewcommand{\isachardoublequoteclose}{''} + +\begin{document} + +\title{Pushdown Systems} +\author{Anders Schlichtkrull, Morten Konggaard Schou, Ji\v{r}\'i Srba and Dmitriy Traytel} +\date{} + +\maketitle + +\begin{abstract} +\noindent +We formalize pushdown systems and the correctness of the pushdown reachability algorithms post* (forward search), pre* (backward search) and dual* (bi-directional search). +For pre* we refine the algorithm to an executable version for which one can generate code using Isabelle's code generator. +For pre* and post* we follow Stefan Schwoon's PhD thesis \cite{schwoon2002model}. The dual* algorithm is from a paper by Jensen et. al presented at ATVA2021 \cite{DBLP:conf/atva/JensenSSSVD21}. +The formalization is described in our FMCAD2022 paper \cite{DBLP:conf/fmcad/SchlichtkrullSST22} in which we also document how we have used it to do differential +testing against a C++ implementation of pushdown reachability called PDAAAL. +Lammich et al.\ \cite{Lammich-DPN,DBLP:conf/cav/LammichMW09} formalized the pre* algorithm for +dynamic pushdown networks (DPN) which is a generalization of pushdown systems. +Our work is independent from that because the post* of DPNs is not regular and +additionally the DPN formalization does not support epsilon transitions which we use for post* and dual*. + + +\end{abstract} + +\tableofcontents + +\newpage + +% sane default for proof documents +\parindent 0pt +\parskip 0.5ex + +\section{Introduction} +Pushdown reachability was studied by B{\"u}chi in 1964~\cite{buchi1964regular} and has been used for, among other things, +interprocedural control-flow analysis of recursive programs~\cite{esparza1999automata,conway2005incremental}, +model checking~\cite{esparza2001bdd,moped,jmoped,bouajjani1997reachability} and communication network analysis \cite{JKMSST:coNEXT:18,jensen2020aalwines,DJJKMSST:TON:21}. +In this formalization we formalize the pre* and post* algorithms \cite{schwoon2002model} and the dual* algorithm \cite{DBLP:conf/atva/JensenSSSVD21}. For pre* we have also an executable version. +In our FMCAD2022 paper \cite{DBLP:conf/fmcad/SchlichtkrullSST22} we describe the formalization and use it to +do differential testing against a C++ implementation of pushdown reachability called PDAAAL \cite{DBLP:conf/atva/JensenSSSVD21}. +The differential testing revealed a number of bugs in PDAAAL that we were then able to fix. + +\begin{figure} +\begin{center} + \includegraphics[width=0.2\textwidth,keepaspectratio]{session_graph} +\end{center} +\caption{Theory dependency graph} +\label{fig:thys} +\end{figure} + +\newpage + +% generated text of all theories +\input{session} + +% optional bibliography +\bibliographystyle{alpha} +\bibliography{root} + +\end{document} diff --git a/thys/ROOTS b/thys/ROOTS --- a/thys/ROOTS +++ b/thys/ROOTS @@ -1,780 +1,782 @@ ABY3_Protocols ADS_Functor AI_Planning_Languages_Semantics AODV AOT AVL-Trees AWN Abortable_Linearizable_Modules Abs_Int_ITP2012 Abstract-Hoare-Logics Abstract-Rewriting Abstract_Completeness Abstract_Soundness Ackermanns_not_PR Actuarial_Mathematics Adaptive_State_Counting Affine_Arithmetic Aggregation_Algebras Akra_Bazzi Algebraic_Numbers Algebraic_VCs Allen_Calculus Amicable_Numbers Amortized_Complexity AnselmGod Applicative_Lifting Approximation_Algorithms Architectural_Design_Patterns Aristotles_Assertoric_Syllogistic Arith_Prog_Rel_Primes ArrowImpossibilityGS Attack_Trees Auto2_HOL Auto2_Imperative_HOL AutoFocus-Stream Automated_Stateful_Protocol_Verification Automatic_Refinement AxiomaticCategoryTheory BDD BD_Security_Compositional BNF_CC BNF_Operations BTree Balog_Szemeredi_Gowers Banach_Steinhaus Belief_Revision Bell_Numbers_Spivey BenOr_Kozen_Reif Berlekamp_Zassenhaus Bernoulli Bertrands_Postulate Bicategory BinarySearchTree Binary_Code_Imprimitive Binding_Syntax_Theory Binomial-Heaps Binomial-Queues BirdKMP Birkhoff_Finite_Distributive_Lattices Blue_Eyes Bondy Boolean_Expression_Checkers Boolos_Curious_Inference Boolos_Curious_Inference_Automated Bounded_Deducibility_Security Buchi_Complementation Budan_Fourier Buffons_Needle Buildings BytecodeLogicJmlTypes C2KA_DistributedSystems CAVA_Automata CAVA_LTL_Modelchecker CCS CHERI-C_Memory_Model CISC-Kernel CRDT CRYSTALS-Kyber CSP_RefTK CVP_Hardness CYK CZH_Elementary_Categories CZH_Foundations CZH_Universal_Constructions CakeML CakeML_Codegen Call_Arity Card_Equiv_Relations Card_Multisets Card_Number_Partitions Card_Partitions Cartan_FP Case_Labeling Catalan_Numbers Category Category2 Category3 Catoids Cauchy Cayley_Hamilton Certification_Monads Ceva Chandy_Lamport Chord_Segments Circus Clean Clique_and_Monotone_Circuits ClockSynchInst Closest_Pair_Points CoCon CoSMeDis CoSMed CofGroups Coinductive Coinductive_Languages Collections Combinable_Wands Combinatorial_Enumeration_Algorithms Combinatorics_Words Combinatorics_Words_Graph_Lemma Combinatorics_Words_Lyndon CommCSL Commuting_Hermitian Comparison_Sort_Lower_Bound Compiling-Exceptions-Correctly Complete_Non_Orders Completeness Complex_Bounded_Operators Complex_Geometry Complx ComponentDependencies ConcurrentGC ConcurrentIMP Concurrent_Ref_Alg Concurrent_Revisions Conditional_Simplification Conditional_Transfer_Rule Consensus_Refined Constructive_Cryptography Constructive_Cryptography_CM Constructor_Funs Containers Cook_Levin CoreC++ Core_DOM Core_SC_DOM Correctness_Algebras Cotangent_PFD_Formula Count_Complex_Roots Coupledsim_Contrasim CryptHOL CryptoBasedCompositionalProperties Crypto_Standards Cubic_Quartic_Equations DCR-ExecutionEquivalence DFS_Framework DOM_Components DPRM_Theorem DPT-SAT-Solver DataRefinementIBP Datatype_Order_Generator Decl_Sem_Fun_PL Decreasing-Diagrams Decreasing-Diagrams-II Dedekind_Real Deep_Learning Delta_System_Lemma Density_Compiler Dependent_SIFUM_Refinement Dependent_SIFUM_Type_Systems Depth-First-Search Derangements Deriving Descartes_Sign_Rule Design_Theory Dict_Construction Differential_Dynamic_Logic Differential_Game_Logic DigitsInBase Digit_Expansions Dijkstra_Shortest_Path Diophantine_Eqns_Lin_Hom Directed_Sets Dirichlet_L Dirichlet_Series DiscretePricing Discrete_Summation Disintegration DiskPaxos Distributed_Distinct_Elements Dominance_CHK DynamicArchitectures Dynamic_Tables E_Transcendental Earley_Parser Echelon_Form EdmondsKarp_Maxflow Edwards_Elliptic_Curves_Group Efficient-Mergesort Efficient_Weighted_Path_Order Elimination_Of_Repeated_Factors Elliptic_Curves_Group_Law Encodability_Process_Calculi Epistemic_Logic Equivalence_Relation_Enumeration Ergodic_Theory Error_Function Euler_MacLaurin Euler_Partition Euler_Polyhedron_Formula Eudoxus_Reals Eval_FO Example-Submission Executable_Randomized_Algorithms Expander_Graphs Extended_Finite_State_Machine_Inference Extended_Finite_State_Machines FFT FLP FOL-Fitting FOL_Axiomatic FOL_Harrison FOL_Seq_Calc1 FOL_Seq_Calc2 FOL_Seq_Calc3 FO_Theory_Rewriting FSM_Tests Factor_Algebraic_Polynomial Factored_Transition_System_Bounding Falling_Factorial_Sum Farkas FeatherweightJava Featherweight_OCL Fermat3_4 FileRefinement FinFun Finger-Trees Finite-Map-Extras Finite_Automata_HF Finite_Fields Finitely_Generated_Abelian_Groups First_Order_Terms First_Welfare_Theorem Fishburn_Impossibility Fisher_Yates Fishers_Inequality Fixed_Length_Vector Flow_Networks Floyd_Warshall Flyspeck-Tame FocusStreamsCaseStudies Forcing Formal_Puiseux_Series Formal_SSA Formula_Derivatives Foundation_of_geometry Fourier Free-Boolean-Algebra Free-Groups Frequency_Moments Fresh_Identifiers FunWithFunctions FunWithTilings Functional-Automata Functional_Ordered_Resolution_Prover Furstenberg_Topology GPU_Kernel_PL Gabow_SCC GaleStewart_Games Gale_Shapley Game_Based_Crypto Gauss-Jordan-Elim-Fun Gauss_Jordan Gauss_Sums Gaussian_Integers GenClock General-Triangle Generalized_Counting_Sort Generic_Deriving Generic_Join GewirthPGCProof Girth_Chromatic Given_Clause_Loops GoedelGod Goedel_HFSet_Semantic Goedel_HFSet_Semanticless Goedel_Incompleteness Goodstein_Lambda GraphMarkingIBP Graph_Saturation Graph_Theory Gray_Codes Green Groebner_Bases Groebner_Macaulay Gromov_Hyperbolicity Grothendieck_Schemes Group-Ring-Module HOL-CSP HOLCF-Prelude HRB-Slicing Hahn_Jordan_Decomposition Hales_Jewett Heard_Of Hello_World HereditarilyFinite Hermite Hermite_Lindemann Hidden_Markov_Models Higher_Order_Terms HoareForDivergence Hoare_Time Hood_Melville_Queue HotelKeyCards Huffman Hybrid_Logic Hybrid_Multi_Lane_Spatial_Logic Hybrid_Systems_VCs HyperCTL HyperHoareLogic Hyperdual Hypergraph_Basics Hypergraph_Colourings IEEE_Floating_Point IFC_Tracking IMAP-CRDT IMO2019 IMP2 IMP2_Binary_Heap IMP_Compiler IMP_Compiler_Reuse IO_Language_Conformance IP_Addresses Imperative_Insertion_Sort Implicational_Logic Impossible_Geometry Incompleteness Incredible_Proof_Machine Independence_CH Inductive_Confidentiality Inductive_Inference InfPathElimination InformationFlowSlicing InformationFlowSlicing_Inter Integration Interpolation_Polynomials_HOL_Algebra Interpreter_Optimizations Interval_Arithmetic_Word32 Intro_Dest_Elim Involutions2Squares Iptables_Semantics Irrational_Series_Erdos_Straus Irrationality_J_Hancl Irrationals_From_THEBOOK IsaGeoCoq IsaNet Isabelle_C Isabelle_Marries_Dirac Isabelle_Meta_Model Jacobson_Basic_Algebra Jinja JinjaDCI JinjaThreads JiveDataStoreModel Jordan_Hoelder Jordan_Normal_Form KAD KAT_and_DRA KBPs KD_Tree Key_Agreement_Strong_Adversaries Khovanskii_Theorem Kleene_Algebra Kneser_Cauchy_Davenport Knights_Tour Knot_Theory Knuth_Bendix_Order Knuth_Morris_Pratt Koenigsberg_Friendship Kruskal Kuratowski_Closure_Complement LLL_Basis_Reduction LLL_Factorization LOFT LP_Duality LTL LTL_Master_Theorem LTL_Normal_Form LTL_to_DRA LTL_to_GBA Lam-ml-Normalization LambdaAuth LambdaMu Lambda_Free_EPO Lambda_Free_KBOs Lambda_Free_RPOs Lambert_W Landau_Symbols Laplace_Transform Latin_Square LatticeProperties Launchbury Laws_of_Large_Numbers Lazy-Lists-II Lazy_Case Lehmer Lifting_Definition_Option Lifting_the_Exponent LightweightJava LinearQuantifierElim Linear_Inequalities Linear_Programming Linear_Recurrences Liouville_Numbers List-Index List-Infinite List_Interleaving List_Inversions List_Update LocalLexing Localization_Ring Locally-Nameless-Sigma Logging_Independent_Anonymity Lovasz_Local Lowe_Ontological_Argument Lower_Semicontinuous Lp Lucas_Theorem MDP-Algorithms MDP-Rewards MFMC_Countable MFODL_Monitor_Optimized MFOTL_Monitor MSO_Regex_Equivalence Markov_Models Marriage Mason_Stothers Matrices_for_ODEs Matrix Matrix_Tensor Matroids Max-Card-Matching Maximum_Segment_Sum Median_Method Median_Of_Medians_Selection Menger Mereology Mersenne_Primes Metalogic_ProofChecker MHComputation MiniML MiniSail Minimal_SSA Minkowskis_Theorem Minsky_Machines MLSS_Decision_Proc ML_Unification Modal_Logics_for_NTS Modular_Assembly_Kit_Security Modular_arithmetic_LLL_and_HNF_algorithms Monad_Memo_DP Monad_Normalisation MonoBoolTranAlgebra MonoidalCategory Monomorphic_Monad MuchAdoAboutTwo Multi_Party_Computation Multirelations Multirelations_Heterogeneous Multiset_Ordering_NPC Multitape_To_Singletape_TM Myhill-Nerode Name_Carrying_Type_Inference Nano_JSON Nash_Williams Nat-Interval-Logic Native_Word Nested_Multisets_Ordinals Network_Security_Policy_Verification Neumann_Morgenstern_Utility No_FTL_observers No_FTL_observers_Gen_Rel Nominal2 Nominal_Myhill_Nerode Noninterference_CSP Noninterference_Concurrent_Composition Noninterference_Generic_Unwinding Noninterference_Inductive_Unwinding Noninterference_Ipurge_Unwinding Noninterference_Sequential_Composition NormByEval Nullstellensatz Number_Theoretic_Transform Octonions OpSets Open_Induction Optics Optimal_BST Orbit_Stabiliser Order_Lattice_Props Ordered_Resolution_Prover Ordinal Ordinal_Partitions Ordinals_and_Cardinals Ordinary_Differential_Equations PAC_Checker PAL PAPP_Impossibility PCF PLM POPLmark-deBruijn PSemigroupsConvolution Package_logic Padic_Field Padic_Ints Pairing_Heap Paraconsistency Parity_Game Partial_Function_MR Partial_Order_Reduction Password_Authentication_Protocol Pell Perfect_Fields Perfect-Number-Thm Perron_Frobenius Physical_Quantities Pi_Calculus Pi_Transcendental Planarity_Certificates Pluennecke_Ruzsa_Inequality Poincare_Bendixson Poincare_Disc Polygonal_Number_Theorem Polynomial_Factorization Polynomial_Interpolation Polynomials Pop_Refinement Posix-Lexing Possibilistic_Noninterference Power_Sum_Polynomials Pratt_Certificate Prefix_Free_Code_Combinators Presburger-Automata Prim_Dijkstra_Simple Prime_Distribution_Elementary Prime_Harmonic_Series Prime_Number_Theorem Priority_Queue_Braun Priority_Search_Trees Probabilistic_Noninterference Probabilistic_Prime_Tests Probabilistic_System_Zoo Probabilistic_Timed_Automata Probabilistic_While Probability_Inequality_Completeness Program-Conflict-Analysis Progress_Tracking Projective_Geometry Projective_Measurements Promela Proof_Strategy_Language PropResPI Propositional_Logic_Class Propositional_Proof_Systems Prpu_Maxflow PseudoHoops Psi_Calculi Ptolemys_Theorem Public_Announcement_Logic Q0_Metatheory QHLProver QR_Decomposition Quantales Quantales_Converse Quantifier_Elimination_Hybrid Quasi_Borel_Spaces Quaternions Query_Optimization Quick_Sort_Cost RIPEMD-160-SPARK ROBDD RSAPSS Ramsey-Infinite Random_BSTs Random_Graph_Subgraph_Threshold Randomised_BSTs Randomised_Social_Choice Rank_Nullity_Theorem Real_Impl Real_Power Real_Time_Deque Recursion-Addition Recursion-Theory-I Refine_Imperative_HOL Refine_Monadic RefinementReactive Regex_Equivalence Registers Regression_Test_Selection Regular-Sets Regular_Algebras Regular_Tree_Relations Relation_Algebra Relational-Incorrectness-Logic Relational_Cardinality Relational_Disjoint_Set_Forests Relational_Forests Relational_Method Relational_Minimum_Spanning_Trees Relational_Paths Rensets Rep_Fin_Groups ResiduatedTransitionSystem Residuated_Lattices Resolution_FOL Rewrite_Properties_Reduction Rewriting_Z Ribbon_Proofs Risk_Free_Lending Robbins-Conjecture Robinson_Arithmetic Root_Balanced_Tree Roth_Arithmetic_Progressions Routing Roy_Floyd_Warshall SATSolverVerification SCC_Bloemen_Sequential SC_DOM_Components SDS_Impossibility SIFPL SIFUM_Type_Systems SPARCv8 S_Finite_Measure_Monad Safe_Distance Safe_OCL Safe_Range_RC Saturation_Framework Saturation_Framework_Extensions Sauer_Shelah_Lemma Schutz_Spacetime Schwartz_Zippel Secondary_Sylow Security_Protocol_Refinement Selection_Heap_Sort SenSocialChoice Separata Separation_Algebra Separation_Logic_Imperative_HOL Separation_Logic_Unbounded SequentInvertibility Shadow_DOM Shadow_SC_DOM Shivers-CFA ShortestPath Show Sigma_Commit_Crypto Signature_Groebner Simpl Simple_Clause_Learning Simple_Firewall Simplex Simplicial_complexes_and_boolean_functions SimplifiedOntologicalArgument Skew_Heap Skip_Lists Slicing Sliding_Window_Algorithm Smith_Normal_Form Smooth_Manifolds Solidity Sophomores_Dream Sort_Encodings Source_Coding_Theorem SpecCheck Special_Function_Bounds Splay_Tree Sqrt_Babylonian Stable_Matching Stalnaker_Logic Standard_Borel_Spaces Statecharts Stateful_Protocol_Composition_and_Typing Stellar_Quorums Stern_Brocot Stewart_Apollonius Stirling_Formula Stochastic_Matrices Stone_Algebras Stone_Kleene_Relation_Algebras Stone_Relation_Algebras Store_Buffer_Reduction Stream-Fusion Stream_Fusion_Code StrictOmegaCategories Strong_Security Sturm_Sequences Sturm_Tarski Stuttering_Equivalence Subresultants Subset_Boolean_Algebras SumSquares Sunflowers SuperCalc Suppes_Theorem Surprise_Paradox Symmetric_Polynomials Syntax_Independent_Logic Synthetic_Completeness Szemeredi_Regularity Szpilrajn TESL_Language TLA Tail_Recursive_Functions Tarskis_Geometry Taylor_Models Three_Circles Three_Squares Timed_Automata Topological_Semantics Topology TortoiseHare TsirelsonBound Transcendence_Series_Hancl_Rucki Transformer_Semantics Transition_Systems_and_Automata Transitive-Closure Transitive-Closure-II Transitive_Models Transport Treaps Tree-Automata Tree_Decomposition Tree_Enumeration Triangle Trie Turans_Graph_Theorem Twelvefold_Way Two_Generated_Word_Monoids_Intersection Tycon Types_Tableaus_and_Goedels_God Types_To_Sets_Extension UPF UPF_Firewall UTP Undirected_Graph_Theory Universal_Hash_Families Universal_Turing_Machine UpDown_Scheme VYDRA_MDL Valuation Van_Emde_Boas_Trees Van_der_Waerden VectorSpace VeriComp Verified-Prover Verified_SAT_Based_AI_Planning VerifyThis2018 VerifyThis2019 Vickrey_Clarke_Groves Virtual_Substitution VolpanoSmith WHATandWHERE_Security WOOT_Strong_Eventual_Consistency WebAssembly Weight_Balanced_Trees Weighted_Arithmetic_Geometric_Mean Weighted_Path_Order Well_Quasi_Orders Wetzels_Problem Winding_Number_Eval Word_Lib WorkerWrapper X86_Semantics XML Youngs_Inequality ZFC_in_HOL Zeckendorf Zeta_3_Irrational Zeta_Function pGCL +Labeled_Transition_Systems +Pushdown_Systems