diff --git a/thys/Dominance_CHK/Dom_Kildall_Property.thy b/thys/Dominance_CHK/Dom_Kildall_Property.thy --- a/thys/Dominance_CHK/Dom_Kildall_Property.thy +++ b/thys/Dominance_CHK/Dom_Kildall_Property.thy @@ -1,2160 +1,2158 @@ (* Author: Nan Jiang *) section \Properties of the kildall's algorithm on the semilattice \ theory Dom_Kildall_Property imports Dom_Kildall "Jinja.Listn" "Jinja.Kildall_1" begin lemma sorted_list_len_lt: "x \ y \ finite y \ length (sorted_list_of_set x) < length (sorted_list_of_set y)" proof- let ?x = "sorted_list_of_set x" let ?y = "sorted_list_of_set y" assume x_y: "x \ y" and fin_y: "finite y" then have card_x_y: "card x < card y" and fin_x: "finite x" by (auto simp add:psubset_card_mono finite_subset) with fin_y have "length ?x = card x" and "length ?y = card y" by auto with card_x_y show ?thesis by auto qed lemma wf_sorted_list: "wf ((\(x,y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset)" apply (unfold finite_psubset_def) apply (rule wf_measure [THEN wf_subset]) apply (simp add: measure_def inv_image_def image_def) by (auto intro: sorted_list_len_lt) lemma sorted_list_psub: "sorted w \ w \ [] \ (sorted_list_of_set (set (tl w)), w) \ (\(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` {(A, B). A \ B \ finite B}" proof(intro strip, simp add:image_iff) assume sorted_w: "sorted w" and w_n_nil: "w \ []" let ?a = "set (tl w)" let ?b = "set w" from sorted_w have sorted_tl_w: "sorted (tl w)" and dist: "distinct w" by (induct w) (auto simp add: sorted_wrt_append ) with w_n_nil have a_psub_b: "?a \ ?b" by (induct w)auto from sorted_w sorted_tl_w have "w = sorted_list_of_set ?b" and "tl w = sorted_list_of_set (set (tl w))" by (auto simp add: sorted_less_set_eq) with a_psub_b show "\a b. a \ b \ finite b \ sorted_list_of_set (set (tl w)) = sorted_list_of_set a \ w = sorted_list_of_set b" by auto qed locale dom_sl = cfg_doms + fixes A and r and f and step and start and n defines "A \ ((rev \ sorted_list_of_set) ` (Pow (set (nodes))))" defines "r \ nodes_le" defines "f \ nodes_sup" defines "n \ (size nodes)" defines "step \ exec" defines "start \ ([] # (replicate (length (g_V G) - 1) ( (rev[0..\used by acc\_le\_listI\ lemma Cons_less_Conss [simp]: "x#xs [\\<^sub>r] y#ys = (x \\<^sub>r y \ xs [\\<^bsub>r\<^esub>] ys \ x = y \ xs [\\<^sub>r] ys)" apply (unfold lesssub_def) apply auto apply (unfold lesssub_def lesub_def r_def) apply (simp only: nodes_le_refl) done lemma acc_le_listI [intro!]: "acc r \ acc (Listn.le r) " apply (unfold acc_def) apply (subgoal_tac "Wellfounded.wf(UN n. {(ys,xs). size xs = n \ size ys = n \ xs <_(Listn.le r) ys})") apply (erule wf_subset) apply (blast intro: lesssub_lengthD) apply (rule wf_UN) prefer 2 apply (rename_tac m n) apply (case_tac "m=n") apply simp apply (fast intro!: equals0I dest: not_sym) apply (rename_tac n) apply (induct_tac n) apply (simp add: lesssub_def cong: conj_cong) apply (rename_tac k) apply (simp add: wf_eq_minimal) apply (simp (no_asm) add: length_Suc_conv cong: conj_cong) apply clarify apply (rename_tac M m) apply (case_tac "\x xs. size xs = k \ x#xs \ M") prefer 2 apply (erule thin_rl) apply (erule thin_rl) apply blast apply (erule_tac x = "{a. \xs. size xs = k \ a#xs:M}" in allE) apply (erule impE) apply blast apply (thin_tac "\x xs. P x xs" for P) apply clarify apply (rename_tac maxA xs) apply (erule_tac x = "{ys. size ys = size xs \ maxA#ys \ M}" in allE) apply (erule impE) apply blast apply clarify apply (thin_tac "m \ M") apply (thin_tac "maxA#xs \ M") apply (rule bexI) prefer 2 apply assumption apply clarify apply simp apply blast done lemma wf_listn: "wf {(y,x). x \\<^bsub>Listn.le r\<^esub> y}" by(insert acc_nodes_le acc_le_listI r_def) (simp add:acc_def) lemma wf_listn': "wf {(y,x). x [\\<^sub>r] y}" by (rule wf_listn) lemma wf_listn_termination_rel: "wf ({(y,x). x \\<^bsub>Listn.le r\<^esub> y} <*lex*> (\(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset)" by (insert wf_listn wf_sorted_list) (fastforce dest:wf_lex_prod) lemma inA_is_sorted: "xs \ A \ sorted (rev xs)" by (auto simp add:A_def sorted_less_sorted_list_of_set) -lemma list_nA_lt_refl: "xs \ list n A \ xs [\\<^bsub>r\<^esub>] xs" +lemma list_nA_lt_refl: "xs \ nlists n A \ xs [\\<^bsub>r\<^esub>] xs" proof - assume "xs \ list n A" - then have "set xs \ A" by (rule listE_set) + assume "xs \ nlists n A" + then have "set xs \ A" by (rule nlistsE_set) then have "\i A" by auto then have "\i\<^bsub>r\<^esub>] xs" by(unfold Listn.le_def lesub_def) (auto simp add:list_all2_conv_all_nth Listn.le_def r_def nodes_le_def) qed lemma nil_inA: "[] \ A" apply (unfold A_def) apply (subgoal_tac "{} \ Pow (set nodes)") apply (subgoal_tac "[] = (\x. rev (sorted_list_of_set x)) {}") apply (fastforce intro:rev_image_eqI) by auto lemma upt_n_in_pow_nodes: "{0.. Pow (set nodes)" by(auto simp add:n_def nodes_def verts_set) lemma rev_all_inA: "rev [0.. A" proof(unfold A_def,simp) let ?f = "\x. rev (sorted_list_of_set x)" have "rev [0.. ?f ` Pow (set nodes)" by (fastforce intro: image_eqI) qed lemma len_start_is_n: "length start = n" by (insert len_verts_gt0) (auto simp add:start_def n_def nodes_def dest:Suc_pred) lemma len_start_is_len_verts: "length start = length (g_V G)" using len_verts_gt0 by (simp add:start_def) lemma start_len_gt_0: "length start > 0" by (insert len_verts_gt0) (simp add:start_def) lemma start_subset_A: "set start \ A" by(auto simp add:nil_inA rev_all_inA start_def) -lemma start_in_A : "start \ (list n A)" - by (insert start_subset_A len_start_is_n)(fastforce intro:listI) +lemma start_in_A : "start \ (nlists n A)" + by (insert start_subset_A len_start_is_n)(fastforce intro:nlistsI) lemma sorted_start_nth: "i < n \ sorted (rev (start!i))" apply(subgoal_tac "start!i \ A") apply (fastforce dest:inA_is_sorted) by (auto simp add:start_subset_A len_start_is_n) lemma start_nth0_empty: "start!0 = []" by (simp add:start_def) lemma start_nth_lt0_all: "\p\{1..< length start}. start!p = (rev [0.. set (g_V G) \ x < n" by (simp add:n_def nodes_def verts_set) lemma start_nth0_unstable_auxi: "\ [0] \\<^bsub>r\<^esub> (rev [0.. stable r step start 0" proof(rule notI,auto simp add: start_nth0_empty stable_def step_def exec_def transf_def) assume ass: "\x\set (sorted_list_of_set (succs 0)). [0] \\<^bsub>r\<^esub> start ! x" from succ_of_entry0 obtain s where "s \ succs 0" and "s \ 0 \ s \ set (g_V G)" using head_is_vert by (auto simp add:succs_def) then have "s \ set (sorted_list_of_set (succs 0))" and "start!s = (rev [0.. {1 ..< length (g_V G)} " and "succs p \ {}" shows "\ stable r step start p" proof (rule notI, unfold stable_def) let ?step_p = "step p (start ! p)" let ?rev_all = "rev[0..(q, \)\set ?step_p. \ \\<^bsub>r\<^esub> start ! q" from assms(1) have n_sorted: "\ sorted (rev (p # ?rev_all))" and p:"p \ set (g_V G)" and "start!p = ?rev_all" using verts_set by (auto simp add:n_def nodes_def start_def sorted_wrt_append) with sta have step_p: "\(q, \)\set ?step_p. sorted (rev (p # ?rev_all)) \ (p # ?rev_all = start!q)" by (auto simp add:step_def exec_def transf_def lesssub_def lesub_def r_def nodes_le_def) from assms(2) fin_succs p obtain a b where a_b: "(a, b) \ set ?step_p" by (auto simp add:step_def exec_def transf_def) with step_p have "sorted (rev (p # ?rev_all)) \ (p # ?rev_all = start!a)" by auto with n_sorted have eq_p_cons: "(p # ?rev_all = start!a)" by auto from p have "\(q, \)\set ?step_p. q < n" using succ_in_G fin_succs verts_set n_def nodes_def by (auto simp add:step_def exec_def) with a_b have "a < n" using len_start_is_n by auto then have "sorted (rev (start!a))" using sorted_start_nth by auto with eq_p_cons n_sorted show False by auto qed lemma start_unstable_cond: assumes "succs p \ {} " and "p < length (g_V G)" shows "\ stable r step start p" using assms start_nth0_unstable start_nth_unstable by(cases "p = 0") auto lemma unstable_start: "unstables r step start = sorted_list_of_set ({p. succs p \ {} \ p < length start})" using len_start_is_len_verts start_unstable_cond by (subgoal_tac "{p. p < length start \ \ stable r step start p} = {p. succs p \ {} \ p < length start}") (auto simp add: unstables_def stable_def step_def exec_def) end declare sorted_list_of_set_insert_remove[simp del] context dom_sl begin lemma (in dom_sl) decomp_propa: "\ss w. (\(q,t)\set qs. q < size ss \ t \ A ) \ sorted w \ set ss \ A \ propa f qs ss w = (merges f qs ss, (sorted_list_of_set ({q. \t.(q,t)\set qs \ t \\<^bsub>f\<^esub> (ss!q) \ ss!q} \ set w)))" (*<*) apply (induct qs) apply (fastforce intro:sorted_less_set_eq) apply (simp (no_asm)) apply clarify apply (subst sorted_insort_remove1) apply simp apply (simp add: sorted_less_sorted_list_of_set Semilat.closed_f[OF Semilat.intro, OF is_semi]) apply (rule conjI) apply (blast intro: arg_cong) apply(simp add: nth_list_update) by (auto intro: arg_cong) lemma distinct_pair_filter_n: "distinct (map fst xs) \ a \ set (map fst xs) \ (map snd (filter (\(x,y). x = a) xs)) = []" by (induct xs) (auto simp add: distinct_map_filter image_def) lemma map_fst: "map fst (map (\pc. (pc, x)) xs) = xs" by (induct xs) auto lemma distinct_p: "p < n \ distinct (map fst (step p (ss!p)))" proof- let ?qs = "step p (ss!p)" have "map fst ?qs = (rev (sorted_list_of_set(succs p)))" using map_fst[of _ "(rev (sorted_list_of_set(succs p)))"] by (auto simp add:step_def exec_def) then show ?thesis by auto qed lemma distinct_pair_filter: "distinct (map fst xs) \ (a,b)\ set xs \ map snd (filter (\x. fst x = a) xs) = [b]" apply (induct xs) apply simp apply (auto simp add: distinct_map_filter image_def) proof- { fix xs assume "\x\set xs. a \ fst x " and " distinct (map fst xs)" then show "filter (\x. fst x = a) xs = []" by (induct xs) auto } qed lemma split_comp_eq_pair: "(\x. fst x = a) = (\(x,y). x = a)" by (rule split_comp_eq) lemma distinct_pair_filter': "distinct (map fst xs) \ (a,b)\ set xs \ (map snd (filter (\(x,y). x = a) xs)) = [b]" using distinct_pair_filter by (simp only: split_comp_eq_pair) lemma merges_property1: fixes ss w qs assumes step_bounded_pres: "\(q, \) \ set qs. q < size ss \ \ \ A" and subset_ss_A: "set ss \ A " and len_ss_n: "length ss = n " and dist: "distinct (map fst qs) " shows "\(q, \) \ set qs. merges f qs ss!q = \ \\<^bsub>f\<^esub>ss!q" proof fix x assume "x \ set qs" from dist have \: "\(q, \) \ set qs. (map snd (filter (\(x,y). x = q) qs)) = [\]" using distinct_pair_filter' by fastforce - from len_ss_n subset_ss_A have "ss \ list n A" by (rule listI) + from len_ss_n subset_ss_A have "ss \ nlists n A" by (rule nlistsI) with step_bounded_pres have merge_nth: "\(q, \) \ set qs. (merges f qs ss)!q = map snd [(p',t') \ qs. p'=q] \\<^bsub>f\<^esub> ss!q" by (fastforce intro:Semilat.nth_merges[OF Semilat.intro, OF is_semi]) \ \use lemma: listE_length\ with \ have "\(q, \) \ set qs. (merges f qs ss)!q = [\]\\<^bsub>f\<^esub> ss!q" by fastforce then show "case x of (q, \) \ merges f qs ss ! q = \ \\<^bsub>f\<^esub> ss ! q" using \x \ set qs\ by auto qed lemma propa_property1: fixes ss w qs assumes step_bounded_pres: "\(q, \) \ set qs. q < size ss \ \ \ A " and sorted_w: "sorted (w ::nat list)" and subset_ss_A: "set ss \ A " and len_ss_n: "length ss = n " and dist: "distinct (map fst qs) " shows "\(q, \) \ set qs. (fst(propa f qs ss w))!q = \ \\<^bsub>f\<^esub>ss!q" using assms apply (subgoal_tac "fst (propa f qs ss w) = merges f qs ss") apply(simp add: merges_property1) by (auto dest:decomp_propa) lemma merges_property2: fixes ss w qs q assumes step_bounded_pres: "\(q, \) \ set qs. q < size ss \ \ \ A" and subset_ss_A: "set ss \ A" and len_ss_n: "length ss = n " and dist: "distinct (map fst qs) " and q_nin: "q \ set(map fst qs) " and q_lt_len_ss: "q < length ss " shows "(merges f qs ss)!q = ss!q" proof- - from len_ss_n subset_ss_A have "ss \ list n A" by (rule listI) + from len_ss_n subset_ss_A have "ss \ nlists n A" by (rule nlistsI) with step_bounded_pres q_lt_len_ss have merge_nth: "(merges f qs ss)!q = map snd [(p',t') \ qs. p'=q] \\<^bsub>f\<^esub> ss!q" by (fastforce intro:Semilat.nth_merges[OF Semilat.intro, OF is_semi]) from dist have "q \ set(map fst qs) \ (map snd (filter (\(x,y). x = q) qs)) = []" using distinct_pair_filter_n by fastforce with merge_nth q_nin have "(merges f qs ss)!q = []\\<^bsub>f\<^esub> ss!q" by fastforce then show "(merges f qs ss)!q = ss ! q" by auto qed lemma propa_property2: fixes ss w qs q assumes step_bounded_pres: "\(q, \) \ set qs. q < size ss \ \ \ A" and sorted_w: "sorted (w ::nat list)" and subset_ss_A: "set ss \ A" and len_ss_n: "length ss = n " and dist: "distinct (map fst qs) " and q_nin: "q \ set(map fst qs) " and q_lt_len_ss: "q < length ss " shows "(fst(propa f qs ss w))!q = ss!q" using assms apply (subgoal_tac "fst (propa f qs ss w) = merges f qs ss") apply(simp add: merges_property2) by (auto dest:decomp_propa) lemma merges_incr_lemma_dom: - "\xs. xs \ list n A \ distinct (map fst ps) \ (\(p,x)\set ps. p x \ A) \ xs [\\<^bsub>r\<^esub>] merges f ps xs" + "\xs. xs \ nlists n A \ distinct (map fst ps) \ (\(p,x)\set ps. p x \ A) \ xs [\\<^bsub>r\<^esub>] merges f ps xs" proof(intro strip) fix xs - assume xs_inA: "xs \ list n A " + assume xs_inA: "xs \ nlists n A " and step_bounded_pres: "\(p, x)\set ps. p < length xs \ x \ A" and dist: "distinct (map fst ps)" - then have len_xs_n: "length xs = n" and subset_xs_inA: "set xs \ A" by (auto simp add:listE_length) + then have len_xs_n: "length xs = n" and subset_xs_inA: "set xs \ A" by (auto simp add:nlistsE_length) with step_bounded_pres dist have merge1: "\(q, \) \ set ps. (merges f ps xs)!q = \ \\<^bsub>f\<^esub>xs!q" using merges_property1 by auto from step_bounded_pres dist len_xs_n subset_xs_inA have merge2: "\q. q \ set(map fst ps) \ q < length xs \ (merges f ps xs)!q = xs!q" using merges_property2 by auto have len_eq: "length xs = length (merges f ps xs)" by simp have "\i\<^bsub>r\<^esub> (merges f ps xs)!i" proof(intro strip) fix i assume i_lt_len_xs: "i < length xs" with xs_inA have xs_i_inA: "xs!i \ A" by auto show " xs ! i \\<^bsub>r\<^esub> (merges f ps xs) ! i " proof(cases "i \ set (map fst ps)") case True then obtain s' where s': "(i, s') \ set ps" by auto with merge1 have merge1': "(merges f ps xs)!i = s' \\<^bsub>f\<^esub> xs ! i" by auto from s' step_bounded_pres have "s' \ A" by auto with xs_i_inA merge1' show ?thesis by (auto intro: Semilat.ub2[OF Semilat.intro, OF is_semi]) next case False note i_nin = this with i_lt_len_xs merge2 have "(merges f ps xs)!i = xs!i" by auto with xs_i_inA show ?thesis by (auto simp add:Semilat.refl_r[OF Semilat.intro, OF is_semi]) qed qed then have "\i\<^bsub>r\<^esub> (merges f ps xs)!i" by auto then have "\iix y. lesub x r y) (xs!i)((merges f ps xs)!i)" by simp then have nth_lt: "\i. i (\x y. lesub x r y) (xs!i)((merges f ps xs)!i)" by simp with len_eq show "xs [\\<^bsub>r\<^esub>] merges f ps xs" by (auto simp only:list_all2_conv_all_nth Listn.le_def lesssub_def lesub_def) qed lemma merges_incr_dom: - "\ xs \ list n A; distinct (map fst ps); \(p,x)\set ps. p x \ A \ \ xs [\\<^bsub>r\<^esub>] merges f ps xs" + "\ xs \ nlists n A; distinct (map fst ps); \(p,x)\set ps. p x \ A \ \ xs [\\<^bsub>r\<^esub>] merges f ps xs" by (simp add: merges_incr_lemma_dom) lemma merges_same_conv_dom [rule_format]: - "(\xs. xs \ list n A \ distinct (map fst ps) \ + "(\xs. xs \ nlists n A \ distinct (map fst ps) \ (\(p,x)\set ps. p x\A) \ (merges f ps xs = xs) = (\(p,x)\set ps. x \\<^bsub>r\<^esub> xs!p))" apply (induct_tac ps) apply (simp) apply clarsimp apply (rename_tac p x ps xs) apply (rule iffI) apply (rule context_conjI) apply (subgoal_tac "xs[p := x \\<^bsub>f\<^esub> xs!p] [\\<^bsub>r\<^esub>] xs") apply (fastforce dest!: le_listD simp add: nth_list_update Semilat.plus_le_conv[OF Semilat.intro,OF is_semi] Semilat.ub1[OF Semilat.intro,OF is_semi] Semilat.ub2[OF Semilat.intro,OF is_semi] Semilat.lub[OF Semilat.intro,OF is_semi] ) apply (erule subst, rule merges_incr_dom) - apply (blast intro!: listE_set intro: closedD listE_length [THEN nth_in] + apply (blast intro!: nlistsE_set intro: closedD nlistsE_length [THEN nth_in] Semilat.closed_f[OF Semilat.intro, OF is_semi]) apply clarify apply(intro strip) apply auto apply (erule allE) apply (erule impE) apply assumption apply (drule bspec) apply assumption apply (simp add: Semilat.le_iff_plus_unchanged [OF Semilat.intro, OF is_semi, THEN iffD1] list_update_same_conv [THEN iffD2]) apply blast apply (simp add: Semilat.le_iff_plus_unchanged[OF Semilat.intro, OF is_semi, THEN iffD1] list_update_same_conv [THEN iffD2]) done (*>*) lemma (in Semilat)list_update_le_listI [rule_format]: "set xs \ A \ set ys \ A \ xs [\\<^sub>r] ys \ p < size xs \ x \\<^sub>r ys!p \ x\A \ xs[p := x \\<^sub>f xs!p] [\\<^sub>r] ys" (*<*) apply (insert semilat) apply (simp only: Listn.le_def lesub_def semilat_def) apply (simp add: list_all2_conv_all_nth nth_list_update) done lemma (in Semilat) merges_pres_le_ub: assumes "set ts \ A" "set ss \ A" "\(p,t)\set ps. t \\<^bsub>r\<^esub> ts!p \ t \ A \ p < size ts" "ss [\\<^bsub>r\<^esub>] ts" shows "merges f ps ss [\\<^bsub>r\<^esub>] ts" (*<*) proof - { fix t ts ps have "\qs. \set ts \ A; \(p,t)\set ps. t \\<^bsub>r\<^esub> ts!p \ t \ A \ p< size ts \ \ set qs \ set ps \ (\ss. set ss \ A \ ss [\\<^bsub>r\<^esub>] ts \ merges f qs ss [\\<^bsub>r\<^esub>] ts)" apply (induct_tac qs) apply simp apply (simp (no_asm_simp)) apply clarify apply simp apply (erule allE, erule impE, erule_tac [2] mp) apply (drule bspec, assumption) apply (simp add: closedD Semilat.closed_f) apply (drule bspec, assumption) apply (simp ) apply(rule list_update_le_listI) apply auto done } note this [dest] from assms show ?thesis by blast qed (*>*) lemma termination_lemma: -shows "\ss \ list n A; distinct (map fst qs); \(q,t)\set qs. q t\A; sorted w; w \ [] \ \ +shows "\ss \ nlists n A; distinct (map fst qs); \(q,t)\set qs. q t\A; sorted w; w \ [] \ \ ss [\\<^sub>r] merges f qs ss \ merges f qs ss = ss \ (sorted_list_of_set ({q. \t. (q,t)\set qs \ t \\<^bsub>f\<^esub> ss!q \ ss!q} \ set (tl w)),w) \ (\x. case x of (x, y) \ (sorted_list_of_set x, sorted_list_of_set y)) ` {(A, B). A \ B \ finite B}" apply(insert is_semi) apply (unfold lesssub_def) apply (simp (no_asm_simp) add: merges_incr_dom) apply (rule impI) apply (rule merges_same_conv_dom [THEN iffD1, elim_format]) apply assumption+ defer apply (rule sym, assumption) defer apply simp apply (subgoal_tac "\q t. \((q, t) \ set qs \ t \\<^bsub>f\<^esub> ss ! q \ ss ! q)") defer apply clarsimp apply (drule bspec, assumption) apply (drule bspec, assumption) apply clarsimp apply(subgoal_tac "{q. \t. (q, t) \ set qs \ t \\<^bsub>f\<^esub> ss ! q \ ss ! q} \ set (tl w) = set (tl w)") apply (auto simp add: sorted_list_psub) done lemma bounded_exec: "bounded step n" apply (insert is_semi,unfold semilat_def bounded_def step_def exec_def transf_def ) by (auto simp add: n_def nodes_def verts_set fin_succs' succ_range) lemma bounded_exec': fixes ss w a b assumes w_n_nil: " w \ [] " and step_hdw: " (a, b) \ set (step (hd w) (ss ! hd w)) " and w_lt_n:"\p\set w. p < n " shows" a < n" using assms proof- from w_lt_n have "hd w < n" using w_n_nil by auto with bounded_exec have "( \\. \(q,\') \ set (step (hd w) \). q (\\\set ss. \ \ A) \ (\p < n. sorted (rev ( (ss!p))) \ (ss!p \ rev [0..< n] \ (\x\set ( (ss!p)). x < p)) \ (ss!p = rev [0.. (\x\ set w. (x,p)\ g_E G \ x < p)) \ (p \ set w \ stable r step ss p)) \ sorted w \ length ss = n \ (\x\set w. x < n) " lemma wf_dom_w: assumes "wf_dom ss w" shows "sorted w" using assms by (auto simp add:wf_dom_def) lemma wf_dom_w2: assumes "wf_dom ss w" shows "(\x\set w. x < n)" using assms by (auto simp add:wf_dom_def) lemma wf_dom_len_eq: assumes "wf_dom ss w" shows "(length ss = n)" using assms by (auto simp add:wf_dom_def) lemma wf_dom_inA: assumes "wf_dom ss w" - shows "ss \ list n A" - using assms by (auto simp add:wf_dom_def intro: listI) + shows "ss \ nlists n A" + using assms by (auto simp add:wf_dom_def intro: nlistsI) lemma wf_dom_le: assumes wf_ss_w: "wf_dom ss w" shows "ss [\\<^bsub>r\<^esub>] ss" using assms proof- from wf_ss_w have "\i A" by (auto simp add:wf_dom_def) then have "\iss\A. p < n \ (\x ss!x) \ transf p ss \ A" proof(intro strip, unfold transf_def) fix ss assume p_lt_n: "p < n" and p_gt: "\x_in_A: "ss \ A" then have "set ss \ set nodes" by (unfold A_def) (rule inpow_subset_nodes) with p_lt_n have p_\_in: "set (p # ss) \ set nodes" by (auto simp add:n_def nodes_def verts_set) from \_in_A have sorted_\: "sorted (rev ss)" by (simp add:inA_is_sorted) with p_gt have "sorted (rev (p # ss))" using Cons_sorted_less_nth by auto with p_\_in show "(p # ss) \ A" by (unfold A_def) (fastforce intro: subset_nodes_inpow) qed lemma pres_exec: assumes "(q,\) \ set (step p (ss!p))" and "\n \ set (ss!p). p > n" and "ss!p \ A" and "p < n" shows "\ \ A " using assms by (auto simp add:step_def exec_def pres_transf) lemma wf_hd_neq_all: assumes wf_ss_w: "wf_dom ss w " and w_n_nil: "w \ [] " shows " ss!(hd w) \ rev [0.. ss ! hd w \ (rev [0..x\ set w. x < n" and "sorted w" by (auto simp add:wf_dom_def) then have "hd w < n" and y:"\x \ set w. x \ hd w" using w_n_nil by (induct w) (auto simp add:sorted_wrt_append) with wf_ss_w x have "(\x\ set w. (x,hd w)\ g_E G \ x < hd w)" by (auto simp add:wf_dom_def) with y show False by auto qed lemma pres_wf_exec: fixes ss w a b assumes wf_ss_w: "wf_dom ss w " and w_n_nil: "w \ [] " shows "\(q,\) \ set (step (hd w) (ss!(hd w))). \ \ A " using assms proof(intro strip, auto) fix a b assume a_b: "(a, b) \ set (step (hd w) (ss ! hd w))" from wf_ss_w have sorted_w: "sorted w" and hd_w_lt_n: "hd w < n" and ss_hdw_inA: "ss!hd w \ A" using w_n_nil by (auto simp add:wf_dom_def) from assms have ss_hd_w_neq_all: "ss!hd w \ (rev [0..x\set (ss!hd w). hd w > x" by (auto simp add:wf_dom_def) with ss_hdw_inA hd_w_lt_n a_b show "b \ A" using pres_exec by auto qed lemma propa_dom_invariant_auxi: assumes wf_a_b: "wf_dom a b" and b_n_nil: "b \ [] " shows "a!hd b \ rev [0.. sorted (rev (hd b # (a!hd b))) \ set (hd b # (a!hd b)) \ set nodes \ hd b # (a!hd b) \ A \ (\(q, \)\set (step (hd b) (a!hd b)). q < length a \ \ \ A)" using assms proof- from assms have "a!hd b \ (rev \ sorted_list_of_set) ` (Pow (set nodes))" and sorted_hdb: "sorted (rev (a!hd b))" and hd_b_lt_n: "hd b < n" and sorted_b: "sorted b" and len_eq: "length a = n" by (auto simp add:A_def wf_dom_def) then have as_subset_nodes: "set (a!hd b) \ set nodes" by (auto simp add:inpow_subset_nodes) with n_def verts_set assms nodes_def have hdb_cons_subset_nodes: "set (hd b # (a!hd b)) \ set nodes" by (auto simp add:wf_dom_def) then have hdb_subset_n: "set (hd b # (a!hd b)) \ {0.. (rev [0.. Pow (set (g_V G))" by (auto simp add:nodes_def) then have pow1: "set ((hd b # (a!hd b))) \ set nodes" by (auto simp add:nodes_def) from hdb_cons_subset_nodes sorted_hd_b_cons have "hd b # (a!hd b) \ (rev \ sorted_list_of_set) ` (Pow (set nodes))" by (fastforce intro: subset_nodes_inpow) then have hd_b_cons_in_A: "(hd b # (a!hd b)) \ A" by (unfold A_def ) (auto simp add:nodes_def) have "(\p\. \(q,\') \ set (step p \). q(q,\') \ set (step (hd b) (a!hd b)). q(q, \)\set(step (hd b) (a!hd b)). \ \ A" by (rule pres_wf_exec) with bounded pres have step_pres_bounded: "\(q, \)\set (step (hd b) (a!hd b)). q < length a \ \ \ A " using len_eq by auto with a_hd_b_neq_all sorted_hd_b_cons hdb_cons_subset_nodes hd_b_cons_in_A show ?thesis by auto qed lemma propa_dom_invariant_aux: fixes a b ss w assumes propa: "propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w) " and b_n_nil: "b \ [] " and a_in_A: "\\\set a. \ \ A" and ass: "\p (a!p \ rev [0.. (\x\set (a!p). x < p)) \ (a!p = rev [0.. (\x\set b. (x,p)\ g_E G \ x < p)) \ (p \ set b \ stable r step a p)" and sorted_b: "sorted b " and len_eq: "length a = n " and b_lt_n: "\x\set b. x < n " shows "(\\\set ss. \ \ A) \ (\p (ss!p \ rev [0.. (\x\set (ss!p). x < p)) \ (ss!p = rev [0.. (\x\ set w. (x,p)\ g_E G \ x < p)) \ (p \ set w \ stable r step ss p)) \ sorted w \ length ss = n \ (\x\set w. x list n A" by (auto intro: listI) + from a_in_A len_eq have a_in_list_nA: "a \ nlists n A" by (auto intro: nlistsI) from a_in_A have "\p< length a. a!p \ A" by (auto simp add:A_def) then have a_p_subset: "\p< length a. set (a!p) \ set nodes" by (auto simp add:inpow_subset_nodes A_def) from a_in_A ass sorted_b len_eq b_lt_n b_n_nil have wf_a_b: "wf_dom a b" by (auto simp add:wf_dom_def) with b_n_nil have a_hd_b_neq_all: "?a_hdb \ rev [0.. set nodes" and hd_b_cons_in_A: "hd b # ?a_hdb \ A" and step_pres_bounded: "(\(q, \)\set (step (hd b) ?a_hdb). q < length a \ \ \ A)" using propa_dom_invariant_auxi by auto then have hdb_subset_n: "set (hd b # ?a_hdb) \ {0..x\ set (tl b). x < n" by (induct b)(auto simp add:wf_dom_def) then have dist: "distinct (map fst ?qs_a)" using distinct_p by auto from b_lt_n len_eq sorted_b have sorted_tl_b: "sorted (tl b)" by (induct b) auto from b_lt_n verts n_def nodes_def verts_set have b_in_verts: "\x\set b. x \ set (g_V G)" by auto then have hd_b_in_verts: "hd b \ set (g_V G)" using b_n_nil by auto then have fin_succ_hd_b: "finite (succs (hd b))" using fin_succs by auto have fin_q1: "finite {q. \t.(q,t)\set ?qs_a}" and fin_q2: "finite ?q_a_wl" by (auto simp add:step_def exec_def image_def) then have fin: "finite (?q_a_wl \ set (tl b))" by auto from a_in_A have set_a: "set a \ A" by auto with step_pres_bounded sorted_tl_b len_eq dist have "\(q, \) \ set ?qs_a. (fst(propa f ?qs_a a (tl b)))!q = \ \\<^bsub>f\<^esub>a!q" by (auto dest:propa_property1) with propa have propa_ss1: "\(q, \) \ set ?qs_a. ss!q = \ \\<^bsub>f\<^esub>a!q" by simp then have propa_ss1': "\(q, \) \ set ?qs_a. ss!q = (hd b # ?a_hdb) \\<^bsub>f\<^esub>a!q" by (auto simp add:step_def exec_def transf_def) then have succ_self_eq: "\(q, \) \ set ?qs_a. q = hd b \ ss!q = a!q" by(auto simp add: f_def nodes_sup_def plussub_def inter_sorted_cons[OF sorted_hd_b_cons]) have step_hd_b: "\(q,\)\set ?qs_a. \ = (hd b # ?a_hdb)" by(auto simp add:step_def exec_def transf_def) from step_pres_bounded sorted_tl_b set_a len_eq dist have "\q. q \ set(map fst ?qs_a) \ q < length a \ (fst(propa f ?qs_a a (tl b)))!q = a!q" by (auto intro:propa_property2) with propa have exec2: "\q. q \ set(map fst ?qs_a) \ q < length a \ ss!q = a!q" by auto then have ss_hd_b_eq_a: "ss!hd b = a!hd b" using hd_b_lt_n len_eq fin_succ_hd_b succ_self_eq by (auto simp add:step_def exec_def) then have hdb_nin_w: "hd b \ ?q_a_wl" using fin_succ_hd_b propa_ss1 by (auto simp add:step_def exec_def) from step_pres_bounded sorted_tl_b set_a have "snd (propa f ?qs_a a (tl b)) = (sorted_list_of_set (?q_a_wl \ set (tl b)))" by (fastforce dest:decomp_propa) with propa have ww: "w = sorted_list_of_set (?q_a_wl \ set (tl b))" by simp then have sorted_w:"sorted w" by (simp add:sorted_less_sorted_list_of_set) from ww have set_ww: "set w =?q_a_wl \ set (tl b)" using fin by auto with step_pres_bounded tl_b_lt_n ww fin len_eq have w_lt_n: "(\x\set w. x < n)" using len_eq by auto then have w_set': "\x\set w. x \ {0.. {0.. set (tl b) " by (induct b) (auto simp add:sorted_wrt_append) with hdb_nin_w ww have "hd b \ set w" using fin by auto from step_pres_bounded sorted_tl_b set_a propa have ss_merge: "ss = merges f ?qs_a a" by (auto dest: decomp_propa) from step_pres_bounded a_in_list_nA have "\(q, \)\set (step (hd b) (a ! hd b)). q < n \ \ \ A" using len_eq by simp - with a_in_list_nA have "merges f ?qs_a a \ list n A" + with a_in_list_nA have "merges f ?qs_a a \ nlists n A" by (rule Semilat.merges_preserves_type[OF Semilat.intro, OF is_semi]) - with ss_merge have ss_in_A: "ss \ list n A" by simp + with ss_merge have ss_in_A: "ss \ nlists n A" by simp then have len_ss_n: "length ss = n" using len_eq by simp with len_eq have len_ss_n: "length ss = n" by auto - from ss_in_A have set_ss: "set ss \ A " by (rule listE_set) + from ss_in_A have set_ss: "set ss \ A " by (rule nlistsE_set) then have ss_inA: "\\\set ss. \ \ A" by auto then have ss_p_subset: "\p< length ss. set (ss!p) \ set nodes" by (auto simp add:inpow_subset_nodes A_def) from w_lt_n len_ss_n have bounded_a: "\a b. w \ [] \ (a, b) \ set ?qs_ss \ a < length ss" by (auto simp add:bounded_exec') have sorted_a_hdw_n: "w \ [] \ sorted (rev ?a_hdw)" using wf_a_b len_eq w_set' by (auto simp add:wf_dom_def) have sorted_ss_hdw_n: "w \ [] \ sorted (rev ?ss_hdw)" using ss_in_A inA_is_sorted w_lt_n by auto have "w \ [] \ (hd w # ?ss_hdw) \ A" proof assume w_n_nil: "w \ []" with w_lt_n have hd_w_lt_n: "hd w < n" by auto with a_in_A have a_hdw_inA: "?a_hdw \ A" using len_eq by auto then have a_hdw_in_nodes: "set ?a_hdw \ set nodes" by (unfold A_def )(rule inpow_subset_nodes) from hd_w_lt_n have hdw_in_nodes: "hd w \ set nodes" using verts_set by (simp add:n_def nodes_def) from sorted_a_hdw_n w_n_nil have sorted_a_hdw: "sorted (rev ?a_hdw)" by auto show "(hd w # ?ss_hdw) \ A" proof(cases "hd w \ succs (hd b)") case True then obtain s where s: "(hd w, s) \ set ?qs_a" using fin_succ_hd_b by (auto simp add:step_def exec_def) with step_hd_b have "s = (hd b # ?a_hdb)" by auto with s propa_ss1 have ss_hd_w: "?ss_hdw = (hd b # ?a_hdb) \\<^bsub>f\<^esub> ?a_hdw" by auto with hd_b_cons_in_A a_hdw_inA have "?ss_hdw \ A" by (simp add: Semilat.closed_f[OF Semilat.intro, OF is_semi]) then have ss_hdw_in_nodes: "set ?ss_hdw \ set nodes" by (auto simp add:inpow_subset_nodes A_def) with hdw_in_nodes have hdw_cons_ss_in_nodes: "set (hd w # ?ss_hdw) \ set nodes" by auto then have in_pow: "set (hd w # ?ss_hdw) \ Pow (set (g_V G))" by (auto simp add:nodes_def) from sorted_a_hdw ss_hd_w sorted_hd_b_cons have "sorted (rev ?ss_hdw)" and "set ?ss_hdw = set (hd b # ?a_hdb) \ set ?a_hdw" by (auto simp add:f_def plussub_def nodes_sup_def inter_sorted_correct) then have sorted_ss_hdw: "sorted (rev ?ss_hdw)" and ss_hdw_subset_a_hdb_cons: "set ?ss_hdw \ set (hd b # ?a_hdb)" and ss_hdw_subset_a_hdw: "set ?ss_hdw \ set ?a_hdw" by auto from sorted_hd_b_cons have "\x\ set (hd b # ?a_hdb). x \ hd b" using b_n_nil by (induct b) (auto simp add:sorted_wrt_append) with ss_hdw_subset_a_hdb_cons have ss_hdw_lt_hdb: "\x\set ?ss_hdw. x \ hd b" using sorted_hd_b_cons by auto have sorted_rev_hdw: "sorted (rev (hd w # ?ss_hdw))" proof(cases "?a_hdw = rev [0..x\ set b. (x,hd w)\ g_E G \ x < hd w" using hd_w_lt_n by (auto simp add:wf_dom_def) then obtain prev_hd_w where prev_hd_w_in_b: "prev_hd_w \ set b" and prev_hd_w: "(prev_hd_w, hd w)\ g_E G" and prev_hd_w_lt: "prev_hd_w < hd w" by auto show ?thesis proof(cases "prev_hd_w = hd b") case True with prev_hd_w_lt have "hd b < hd w" by auto with ss_hdw_lt_hdb have "\x\set ?ss_hdw. hd w > x" by auto with sorted_ss_hdw show ?thesis by (auto simp add:sorted_wrt_append) next case False with prev_hd_w_in_b have "prev_hd_w \ set (tl b)" by (induct b) auto with ww have prev_hd_w_nin_w: "prev_hd_w \ set w" using fin by auto from sorted_w have "\x\ set w. x \ hd w" by(induct w) (auto simp add:sorted_wrt_append sorted_less_sorted_list_of_set) with prev_hd_w_lt have "prev_hd_w \ set w" by auto with prev_hd_w_nin_w show ?thesis by auto qed next case False with wf_a_b have "(\x\set ?a_hdw. x < hd w)" using hd_w_lt_n by (auto simp add:wf_dom_def) with ss_hdw_subset_a_hdw have "(\x\set ?ss_hdw. x < hd w)" by auto with sorted_ss_hdw show ?thesis by (auto simp add:sorted_wrt_append) qed with hdw_cons_ss_in_nodes show "hd w # ?ss_hdw \ A" using A_def by (fastforce dest:subset_nodes_inpow) next case False note hd_w_nin_succ_hdb = this then have "hd w \ set (map fst ?qs_a)" using fin_succ_hd_b by (auto simp add:step_def exec_def) with exec2 have ss_hd_w_eq_a: "?ss_hdw = ?a_hdw" using hd_w_lt_n len_ss_n len_eq by auto with a_hdw_in_nodes sorted_a_hdw have ss_hdw_in_nodes: "set ?ss_hdw \ set nodes" and sorted_ss_hdw: "sorted (rev ?ss_hdw)" by auto with hdw_in_nodes have hdw_cons_in_nodes: "set (hd w # ?ss_hdw) \ set nodes" by (auto) from hd_w_nin_succ_hdb ww have hd_w_non: "hd w \{q. \t. (q, t) \ set ?qs_a \ t \\<^bsub>f\<^esub> a ! q \ a ! q}" using fin_succ_hd_b by (auto simp add:step_def exec_def ) from set_ww hd_w_non have hd_w_in_tl_b: "hd w \ set (tl b)" using sorted_tl_b \w \ []\ by auto have sorted_rev_hdw: "sorted (rev (hd w # ?ss_hdw))" proof(cases "?a_hdw = rev [0..x\ set b. (x,hd w)\ g_E G \ x < hd w" using hd_w_lt_n by (auto simp add:wf_dom_def) then obtain prev_hd_w where prev_hd_w_in_b: "prev_hd_w \ set b" and prev_hd_w: "(prev_hd_w, hd w)\ g_E G" and prev_hd_w_lt: "prev_hd_w < hd w" by auto from ww have "sorted w" by(simp add:sorted_less_sorted_list_of_set) then have "\x\ set w. x \ hd w" using w_n_nil by (induct w) (auto simp add:sorted_wrt_append) with prev_hd_w_lt have prev_hd_w_nin_w: "prev_hd_w \ set w" using w_n_nil by auto with set_ww have "prev_hd_w \ set (tl b)" by auto with prev_hd_w_in_b have "prev_hd_w = hd b" using sorted_b by (induct b) auto with prev_hd_w have "(hd b, hd w) \ g_E G" by auto with hd_w_nin_succ_hdb show ?thesis by (auto simp add:succs_def) next case False with wf_a_b have a_hdw_lt: "(\x\set ?a_hdw. x < hd w)" and "sorted (rev ?a_hdw)" using hd_w_lt_n by (auto simp add:wf_dom_def) with ss_hd_w_eq_a have "sorted (rev ?ss_hdw)" by simp from ss_hd_w_eq_a have "?a_hdw = ?ss_hdw" by auto with a_hdw_lt have "\x\set ?ss_hdw. x < hd w" by auto with sorted_ss_hdw show ?thesis by (auto simp add:sorted_wrt_append) qed with hdw_cons_in_nodes show " (hd w # ss ! hd w) \ A" by (unfold A_def) (rule subset_nodes_inpow) qed qed then have pres_ss: "\q \. w \ [] \ (q, \) \ set (step (hd w) ?ss_hdw) \ \ \ A" by (auto simp add:step_def exec_def transf_def) have hd_b_ss_sta: "stable r step ss (hd b)" proof(unfold stable_def, clarsimp) fix q \ assume "(q, \) \ set ?qs_ss_hdb " then have "q \ succs (hd b)" and "\ = transf (hd b) ?ss_hdb" using hd_b_lt_n fin_succ_hd_b by (auto simp add:step_def exec_def) then have \:"\ = (hd b # ?a_hdb)" using ss_hd_b_eq_a by (auto simp add:transf_def) from \q \ succs (hd b)\ hd_b_lt_n have "q\ set (g_V G)" using succ_in_G by auto then have "q < n" using verts_set by (auto simp add:n_def nodes_def) with wf_a_b have a_q_inA: "a!q \ A" by (auto simp add:wf_dom_def) from wf_a_b a_hd_b_neq_all hd_b_lt_n have "\x\ set ( (a!hd b)). x < hd b" by (auto simp add:wf_dom_def) with sorted_hd_b_cons have "sorted (rev (hd b # ?a_hdb))" by (auto simp add:sorted_wrt_append) from propa_ss1 \(q, \) \ set (step (hd b) (ss ! hd b))\ have "ss!q = \ \\<^bsub>f\<^esub> a ! q" using \ss!hd b = a!hd b\ by auto with \ have "ss!q = (hd b # ?a_hdb) \\<^bsub>f\<^esub> a ! q" by simp with hd_b_cons_in_A a_q_inA have " (hd b # ?a_hdb)\\<^bsub>r\<^esub> ss!q " by (auto simp add: Semilat.ub1[OF Semilat.intro, OF is_semi]) with \ show "\ \\<^bsub>r\<^esub> ss ! q" by auto qed have wf_dom_2: "\p (ss ! p \ rev [0.. (\x\set ( (ss ! p)). x < p)) \ (ss ! p = rev [0.. (\x\ set w. (x,p)\ g_E G \ x < p)) \ (p \ set w \ stable r step ss p)" proof (intro strip) fix p let ?a_p = "a!p" let ?ss_p = "ss!p" assume p_lt_n: "p < n" with wf_a_b have a_p_inA: "?a_p \ A" and sorted_a_p: "sorted (rev ?a_p)" and sta_a_p: "p \ set b \ stable r step a p" by (auto simp add:wf_dom_def) from p_lt_n have "p \ set (g_V G)" using verts_set n_def nodes_def by auto then have fin_succ_p: "finite (succs p)" using fin_succs by auto from set_a p_lt_n have a_p_inA: "?a_p \ A" using \length a = n\ by (auto simp add:A_def) then have "set ?a_p \ set nodes" using inpow_subset_nodes by (auto simp add:A_def) with p_lt_n have set_p_a_p: "set (p#?a_p) \ set nodes" using n_def nodes_def verts_set by auto from p_lt_n len_eq have p_lt_len_a: "p < length a" by auto with ss_inA have ss_p_in_A: "ss!p \ A" using len_eq len_ss_n by auto with p_lt_n have sorted_ss_p: "sorted (rev ?ss_p)" by (auto simp add:A_def sorted_less_sorted_list_of_set) have len_ss_eq_a: "length ss = length a" using len_eq len_ss_n by auto have p_nin_w_eq: "p \ set w \ (p \ set b \ p = hd b) \ (\s. (p, s) \ set ?qs_a \ s \\<^bsub>f\<^esub> ?a_p = ?a_p)" proof assume "p \ set w" with set_ww have p_nin1: "p \ {q. \t. (q, t) \ set ?qs_a\ t \\<^bsub>f\<^esub> a ! q \ a ! q}" and p_nin2: "p \ set (tl b)" by auto from p_nin1 have p_nin: "(\s. (p, s) \ set ?qs_a \ s \\<^bsub>f\<^esub> ?a_p = ?a_p)" by auto from p_nin2 have "p \ set b \ p = hd b" by (induct b) auto with p_nin show "(p \ set b \ p = hd b) \ (\s. (p, s) \ set ?qs_a \ s \\<^bsub>f\<^esub> ?a_p = ?a_p)" by auto next assume "(p \ set b \ p = hd b) \ (\s. (p, s) \ set ?qs_a \ s \\<^bsub>f\<^esub> ?a_p = ?a_p)" then have p1: "p \ set b \ p = hd b" and p2: "\s. (p, s) \ set ?qs_a \ s \\<^bsub>f\<^esub> a ! p = ?a_p" by auto from p1 have "p \ set (tl b)" proof assume "p \ set b" then show ?thesis by(induct b) auto next assume "p = hd b" with sorted_b show ?thesis by (induct b) (auto simp add:sorted_wrt_append) qed with p2 set_ww show "p \ set w" using set_ww by auto qed have stable_ss_p: "p \ set w \ w \ Nil \ stable r step ss p" proof (clarsimp simp add: stable_def split_paired_all) fix q \ assume p_nin_w: "p \ set w" and w_n_nil: "w \ Nil" and step_ss_p: "(q, \) \ set (step p ?ss_p) " from p_nin_w have p_cond: "(p \ set b \ p = hd b) \ (\s. (p, s) \ set ?qs_a \ (hd b # ?a_hdb) \\<^bsub>f\<^esub> ?a_p = ?a_p)" using p_nin_w_eq by (auto simp add:transf_def step_def exec_def) then have p_cond1: "(p \ set b \ p = hd b)" and p_cond2: "(\s. (p, s) \ set ?qs_a \ (hd b # ?a_hdb) \\<^bsub>f\<^esub> ?a_p = ?a_p)"by auto from bounded_a pres_ss w_n_nil have " \(q, t)\set ?qs_ss. q < length ss \ t \ A" by auto then have "\(q, t)\set (step (hd w) (ss ! hd w)). q < length ss \ (transf (hd w) (ss!hd w)) \ A" by (auto simp add:step_def exec_def) have ss_a_p_eq: "?ss_p = ?a_p" proof(cases "p \ succs (hd b)") case True note p_in_succ_hd_b = this from \p \ succs (hd b)\ propa_ss1' have ss_p: "?ss_p = (hd b # ?a_hdb) \\<^bsub>f\<^esub> ?a_p" using fin_succ_hd_b by (auto simp add:step_def exec_def) from p_in_succ_hd_b p_cond2 have " (hd b # ?a_hdb) \\<^bsub>f\<^esub> ?a_p= ?a_p" using fin_succ_hd_b by (auto simp add:step_def exec_def) with ss_p show ?thesis by auto next case False then have "p \ {q. \t. (q, t) \ set ?qs_a}" using fin fin_succ_hd_b by (auto simp add:step_def exec_def) then have "p \ set ( map fst ?qs_a)" by auto with p_lt_n show ?thesis using exec2 len_eq by auto qed have "(\(q, \)\set (step p ?ss_p). transf p ?ss_p \\<^bsub>r\<^esub> ss ! q) " proof(intro strip, clarsimp) fix succ_p z let ?a_succ_p = "a!succ_p" let ?ss_succ_p = "ss!succ_p" assume "(succ_p, z) \ set (step p ?ss_p)" then have succ_p: "succ_p \ succs p" using p_lt_n fin_succ_p by (auto simp add:step_def exec_def) with p_lt_n have succ_p_lt_n: "succ_p < n" using succ_in_verts n_def nodes_def verts_set by auto with wf_a_b have a_succ_p_inA: "?a_succ_p \ A" by (auto simp add:wf_dom_def) from succ_p_lt_n ss_in_A have ss_succ_p_inA: "?ss_succ_p \ A" by auto have p_nin_b_ssp: "p \ set b \ transf p ?ss_p \ A \ transf p ?ss_p \\<^sub>r ?a_succ_p" proof- assume "p \ set b" with sta_a_p have "(\(q,\) \ set (step p ?a_p). \ \\<^sub>r a!q)" by (simp add:stable_def) with succ_p have transf_p_succp':"transf p ?a_p \\<^sub>r ?a_succ_p" using fin_succ_p by (auto simp add:stable_def step_def exec_def) with ss_a_p_eq have transf_lt_p: "transf p ?ss_p \\<^sub>r ?a_succ_p" by auto from transf_p_succp' have "(p# ?a_p) \\<^sub>r ?a_succ_p" by (auto simp add:transf_def) then have "sorted (rev (p#?a_p)) \ (p#?a_p = ?a_succ_p)" by (auto simp add:step_def exec_def transf_def r_def lesssub_def lesub_def nodes_le_def) with set_p_a_p a_succ_p_inA have "(p#?a_p) \ (rev \ sorted_list_of_set) ` (Pow (set nodes))" using subset_nodes_inpow by (auto simp add:A_def) then have "transf p ?a_p \ A" using transf_def by (auto simp add:A_def transf_def) then show ?thesis using ss_a_p_eq transf_lt_p by auto qed show "transf p ?ss_p \\<^bsub>r\<^esub> ?ss_succ_p" proof(cases "p \ succs (hd b)") case True note p_in_succ_hd_b = this with p_cond have " (hd b # ?a_hdb) \\<^bsub>f\<^esub> ?a_p =?a_p" using fin_succ_hd_b by (auto simp add:step_def exec_def) from p_in_succ_hd_b propa_ss1' have ss_p: "?ss_p = (hd b # ?a_hdb) \\<^bsub>f\<^esub> ?a_p" using fin_succ_hd_b by (auto simp add:step_def exec_def) then have transf_p2: "transf p ?ss_p = (p # (inter_sorted_rev (hd b # ?a_hdb) ?a_p))" by (auto simp add:f_def plussub_def nodes_sup_def transf_def ) then show ?thesis proof(cases "succ_p \ succs (hd b)") case True note succ_p_is_succ_hdb = this with propa_ss1 have ss_succ_p: "?ss_succ_p = (hd b # ?a_hdb) \\<^bsub>f\<^esub> ?a_succ_p" using fin_succ_hd_b by (auto simp add:step_def exec_def transf_def) with a_succ_p_inA hd_b_cons_in_A have succ_p1: "(hd b # ?a_hdb) \\<^bsub>r\<^esub>?ss_succ_p" and succ_p2: "?a_succ_p\\<^bsub>r\<^esub> ?ss_succ_p " by (auto simp add:Semilat.ub1[OF Semilat.intro, OF is_semi] Semilat.ub2[OF Semilat.intro, OF is_semi]) show ?thesis proof(cases "p \ set b") case True note p_in_set_b = this then have p_eq_hdb: "p = hd b" using p_cond by auto with succ_p have succ_p_is_succ_hdb: "succ_p \ succs (hd b)" by auto from ss_a_p_eq p_eq_hdb have "(hd b # ?ss_hdb) = hd b # ?a_hdb" by auto with succ_p1 have "hd b # ss ! hd b \\<^bsub>r\<^esub> ss ! succ_p" by auto with p_eq_hdb show ?thesis by (auto simp add:transf_def) next case False then have "transf p ?ss_p \ A" and "transf p ?ss_p \\<^sub>r ?a_succ_p" using p_nin_b_ssp by auto with succ_p2 a_succ_p_inA ss_succ_p_inA show ?thesis by (auto intro: order_trans Semilat.orderI[OF Semilat.intro, OF is_semi]) qed next case False note succ_p_n_succ_hdb = this with exec2 have ss_succ_p_eq_a: "?ss_succ_p = ?a_succ_p" using fin_succ_hd_b succ_p_lt_n len_eq by (auto simp add:step_def exec_def) show ?thesis proof(cases "p \ set b") case True with p_cond have p_eq_hdb: "p = hd b" by auto with succ_p have succ_p_is_succ_hdb: "succ_p \ succs (hd b)" by auto with succ_p_n_succ_hdb show ?thesis by auto next case False with sta_a_p have "\(q,\) \ set (step p ?a_p). \ \\<^sub>r a!q" by (simp add:stable_def) with succ_p fin_succ_p have "transf p ?a_p \\<^sub>r ?a_succ_p" by (auto simp add:step_def exec_def) with ss_succ_p_eq_a ss_a_p_eq show ?thesis by auto qed qed next case False note p_nin_succ_hd_b = this from p_nin_succ_hd_b p_cond have "p \ set b \ p = hd b" by auto then show ?thesis proof assume "p \ set b" then have transf_ss_p_inA: "transf p ?ss_p \ A" and transf_lt_p: "transf p ?ss_p \\<^sub>r ?a_succ_p" using p_nin_b_ssp by auto show "transf p ?ss_p \\<^bsub>r\<^esub> ?ss_succ_p" proof(cases "succ_p \ succs (hd b)") case True with succ_p_lt_n propa_ss1' len_eq fin_succ_hd_b have "?ss_succ_p = (hd b # ?a_hdb) \\<^bsub>f\<^esub> ?a_succ_p" by (auto simp add:step_def exec_def) with a_succ_p_inA hd_b_cons_in_A have "?a_succ_p \\<^sub>r ?ss_succ_p" by (auto simp add:Semilat.ub2[OF Semilat.intro, OF is_semi]) with transf_lt_p transf_ss_p_inA a_succ_p_inA ss_succ_p_inA show ?thesis by (auto intro: order_trans Semilat.orderI[OF Semilat.intro, OF is_semi]) next case False with succ_p_lt_n exec2 len_eq fin_succ_hd_b have "?ss_succ_p = ?a_succ_p" by (auto simp add:step_def exec_def) with transf_lt_p show ?thesis by auto qed next assume "p = hd b" with hd_b_ss_sta have "(\(q,\) \ set (step p ?ss_p). \ \\<^sub>r ss!q)" by (simp add:stable_def) with succ_p \p = hd b\ show "transf p ?ss_p \\<^bsub>r\<^esub> ?ss_succ_p" using fin_succ_hd_b by (auto simp add:stable_def step_def exec_def transf_def) qed qed qed with step_ss_p show "\ \\<^bsub>r\<^esub> ss ! q" by (auto simp add:step_def exec_def) qed show "sorted (rev ?ss_p) \ (?ss_p \ rev [0.. (\x\set?ss_p. x < p)) \ (?ss_p = rev [0.. (\x\ set w. (x,p)\ g_E G \ x < p)) \ (p \ set w \ stable r step ss p)" proof(cases "w \ []") case True note w_n_nil = this show ?thesis proof (cases "p \ set( map fst (?qs_a))") case True with propa_ss1 have ss_p: "?ss_p = (hd b # ?a_hdb) \\<^bsub>f\<^esub> ?a_p" by (simp add:step_def exec_def transf_def) with sorted_hd_b_cons sorted_a_p have ss_p_lt_hdb: "set ?ss_p \ set (hd b # ?a_hdb)" and ss_p_lt: "set ?ss_p \ set ?a_p" and ss_p_inter: "set ?ss_p = set (hd b # ?a_hdb) \ set ?a_p" by (auto simp add:f_def plussub_def nodes_sup_def inter_sorted_correct) from sorted_hd_b_cons sorted_a_p have "inter_sorted_rev (hd b # ?a_hdb) ?a_p = rev (sorted_list_of_set (set (hd b # ?a_hdb) \ set ?a_p))" by (rule inter_sorted_correct_col) with ss_p have ss_p2: "?ss_p = (rev (sorted_list_of_set (set (hd b # ?a_hdb) \ set ?a_p)))" by (auto simp add:f_def plussub_def nodes_sup_def) show ?thesis proof(cases "?a_p \ (rev [0.. {0..x\set ?a_p. x < p)" using n_def len_eq by (auto simp add:wf_dom_def) with ss_p_lt have "\x\set ?ss_p. x < p" by auto then have ss_lt_p: "?ss_p \ rev [0.. (\x\set ?ss_p. x < p)" by auto have "set ?ss_p \ {0.. set ?ss_p \ {0.. set ?a_p" by auto from a_in_A p_lt_len_a have " ?a_p \ ((rev \ sorted_list_of_set) ` (Pow (set nodes)))" by (auto simp add: A_def) then have ass_set_in_nodes: "set ?a_p \ set nodes" by (rule inpow_subset_nodes) then have "set ?a_p \ {0.. rev [0.. (\x\set w. (x,p)\ g_E G \ x < p)" by auto with sorted_ss_p ss_lt_p stable_ss_p w_n_nil show ?thesis by fastforce next case False then have a_p_all: "?a_p = (rev [0..x\ set b. (x,p)\ g_E G \ x < p)" by (auto simp add:wf_dom_def) have "hd b \ set b" using b_n_nil by auto from a_p_all have "set ?a_p = {0.. {0..set ?a_p = {0.. have "(set (hd b # ?a_hdb) \ set ?a_p) = set (hd b # ?a_hdb)" by auto with ss_p2 have ss_p3: "?ss_p = (rev (sorted_list_of_set (set (hd b # ?a_hdb))))" by auto from sorted_hd_b_cons have "sorted_list_of_set (set (hd b # ?a_hdb)) = rev (hd b # ?a_hdb)" by (fastforce dest: sorted_less_rev_set_eq) with ss_p3 have ss_p_4: "?ss_p = (hd b # ?a_hdb)" by auto have "(?ss_p \ rev [0.. (\x\set ?ss_p. x < p)) \ (?ss_p = rev [0.. (\x\ set w. (x,p)\ g_E G \ x < p)) \ (p \ set w \ stable r step ss p)" proof(cases "?ss_p \ (rev [0..x\set ( (ss ! p)). x < p" by (auto simp add:sorted_wrt_append) with ss_p_4 ss_p_n_all stable_ss_p \w \ []\ show ?thesis by auto next case False note hd_b_ge_p = this from ex_lt_p obtain x where "x\ set b " and " (x,p)\ g_E G " and "x < p"by auto from \x \ set b\ \x < p\ hd_b_ge_p have "tl b \ []" by (induct b) auto with hd_b_ge_p sorted_b have temp_t: "\x\ set (tl b). x \ p" by (induct b) auto with \\hd b < p\ have "x \ set (tl b)" using \(x,p)\ g_E G \ \x \ set b\ \x < p\ by (induct b) auto with \x < p\ temp_t have False by auto then show ?thesis by auto qed next case False then have "?ss_p = (rev [0.. 0 "using n_def nodes_def len_verts_gt0 by auto then have last_hd: "last [0..n> 0\ by auto then have "hd (rev [0..set b \ (x, p) \ g_E G \ x < p" by auto then have "x\set b " and " (x, p) \ g_E G " and " x < p"by auto from x \\hd b have x_n_hd_b: "x \ hd b" by auto with \x\set b \ have "tl b \ []" by (induct b) auto with \x\set b \ x_n_hd_b have "x \ set (tl b)" by (induct b) auto with ww have "x \ set w" using fin by auto then show ?thesis using \ss!p = (rev [0.. \(x, p) \ g_E G\ \x stable_ss_p \w \ []\ by auto qed qed then show ?thesis using sorted_ss_p by auto qed next case False note p_not_in_succ = this with exec2 p_lt_n len_eq have ss_a_p_eq: "ss!p = a!p" by auto with ass p_lt_n wf_a_b have cond1: "(?ss_p \ rev [0.. (\x\set ?ss_p. x < p))" by (auto simp add:wf_dom_def) show ?thesis proof(cases "?a_p \ (rev [0..x\set ?a_p. x < p)" using p_lt_n len_eq by (auto simp add:wf_dom_def) with ss_a_p_eq have "(\x\set ?ss_p. x < p)" by auto with cond1 sorted_ss_p show ?thesis using p_lt_n len_eq stable_ss_p w_n_nil by auto next case False then have "?a_p = (rev [0.. (\x\ set b. (x,p)\ g_E G \ x < p)" by (auto simp add:wf_dom_def) with ss_a_p_eq \a!p = (rev [0.. have hd_b_lt_p: " (\x\ set b. (x,p)\ g_E G \ x < p)" using len_eq by auto then obtain x where "x\ set b " and " (x,p) \ g_E G" and " x < p" by auto from fin_succ_hd_b \(x,p) \ g_E G\ p_not_in_succ have "x \ hd b " by (auto simp add:step_def exec_def succs_def) with \x\ set b\ have "x \ set (tl b)" using b_n_nil by (induct b) auto with ww have "x \ set w" using fin by auto with \(x,p) \ g_E G\ and \ x < p\ have "(\x\ set w. (x,p)\ g_E G \ x < p)" by auto with cond1 sorted_ss_p show ?thesis using stable_ss_p w_n_nil by auto qed qed next case False then have w_n_nil: "w =[]" by auto with set_ww have "tl b = []" and succ_hd_b_eq: "\(q, t) \ set ?qs_a. t \\<^bsub>f\<^esub> a ! q = a ! q" by auto from succ_hd_b_eq propa have "\p(q, t)\set ?qs_a. t \\<^bsub>f\<^esub> a ! q = a ! q " and " propa f ?qs_a a (tl b) = (ss, w) " and p_lt_n: " p < n " show "ss ! p = a ! p" proof(cases "p \ succs (hd b)") case True with fin_succ_hd_b propa_ss1 have ss_p_eq: "ss!p = transf (hd b) (a!hd b) \\<^bsub>f\<^esub> a ! p" by (auto simp add:step_def exec_def) with ass_eq \p \ succs (hd b)\ fin_succ_hd_b have "transf (hd b) (a!hd b) \\<^bsub>f\<^esub> a ! p = a ! p" by (auto simp add:step_def exec_def) with ss_p_eq show ?thesis by auto next case False with fin_succ_hd_b exec2 p_lt_n n_def len_eq nodes_def show ?thesis by (auto simp add:step_def exec_def) qed qed then have "\p< length ss. ss!p = a!p" using \length ss = n\ by auto then have ss_eq_a: "ss = a" using n_def len_eq nodes_def \length ss = n\ by (auto simp add:list_eq_iff_nth_eq) with wf_a_b p_lt_n have t3: "(?ss_p \ rev [0.. (\x\set ?ss_p. x < p))" and t4: "(?ss_p = rev [0.. (\x\set b. (x, p) \ g_E G \ x < p))" and sta_temp: "(p \ set b \ stable r step ss p)" by (auto simp add:wf_dom_def) from \tl b = []\ \b \ []\ have "p \ set b \ p \ hd b " by (induct b) auto with sta_temp have "p \ hd b \ stable r step ss p" by auto with hd_b_ss_sta have "stable r step ss p" by auto then have sta_temp': "p \ set w \ stable r step ss p" using w_n_nil by auto have "?ss_p \ (rev [0..?ss_p \ (rev [0..ss = a\ have "a!p = (rev [0..?ss_p = (rev [0.. have " ?ss_p = rev [0..x\set b. (x, p) \ g_E G \ x < p)" by auto then obtain x where x: "x \ set b \ (x, p) \ g_E G \ x < p" by auto with \tl b = []\ \b \ []\ have "x =hd b" by (induct b) auto with x have " (hd b, p) \ g_E G" and hdb_lt_p: "hd b < p" by auto then have "p \ succs (hd b)" by (simp add:succs_def) with succ_hd_b_eq have transf_hd_b_ap: "transf (hd b) (a!hd b) \\<^bsub>f\<^esub> a ! p = a ! p" using fin_succ_hd_b by (auto simp add:step_def exec_def) have a_p_neq_all: "?a_p \ (rev [0.. ?a_p \ (rev [0..\<^bsub>f\<^esub> ?a_p = (hd b # ?a_hdb) \\<^bsub>f\<^esub> (rev [0..\<^bsub>f\<^esub>?a_p = ( (inter_sorted_rev (hd b # ?a_hdb) (rev [0.. set (hd b # ?a_hdb)" by (auto simp add: inter_sorted_correct) with tx have "set (rev [0.. set (hd b # ?a_hdb)" by auto then have ty: "{0.. set (hd b # ?a_hdb)" by auto from hdb_subset_n ty have "{0.. 0" by auto with tz have tzz: "hd b = n - 1" by (induct n) auto from p_lt_n tzz hdb_lt_p show False by auto qed with ss_p_all ss_eq_a show False by auto qed with sta_temp' sorted_ss_p t3 show ?thesis by auto qed qed from ss_inA wf_dom_2 sorted_w len_ss_n w_lt_n show ?thesis by auto qed lemma propa_dom_invariant_aux': fixes a b ss w assumes propa: "propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w) " and b_n_nil: "b \ [] " and a_in_A: "\\\set a. \ \ A " and ass: "\p (a ! p \ rev [0.. (\x\set ( (a ! p)). x < p)) \ (a ! p = rev [0.. (\x\ set b. (x,p)\ g_E G \ x < p)) \ (p \ set b \ stable r step a p)" and sorted_b: "sorted b " and n_len: "n = length ss0 " and len_eq: "length a = length ss0 " and b_lt_n: "\x\set b. x < length ss0 " shows "(\\\set ss. \ \ A) \ (\p (ss ! p \ rev [0.. (\x\set (ss ! p). x < p)) \ (ss ! p = rev [0.. (\x\ set w. (x,p)\ g_E G \ x < p)) \ (p \ set w \ stable r step ss p)) \ sorted w \ length ss = length ss0 \ (\x\set w. x < length ss0) " using assms by (auto dest: propa_dom_invariant_aux) lemma propa_dom_invariant: assumes wf_ss_w: "wf_dom ss w " and w_n_nil: "w \ []" and propa: "propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss', w') " shows "wf_dom ss' w'" using assms proof- from wf_ss_w have ass: "(\p< n. sorted (rev (ss!p)) \ (ss!p \ rev [0..< n] \ (\x\set (ss!p). x < p)) \ (ss!p = rev [0..< n] \ (\x\ set w. (x,p)\ g_E G \ x < p)) \ (p \ set w \ stable r step ss p)) " and sorted_b: "sorted w" and a_in_A: "\\\set ss. \ \ A" and len_eq: "length ss = n" and b_lt_n: "(\x\set w. x < n)" by (auto simp add:wf_dom_def) from propa w_n_nil a_in_A ass sorted_b len_eq b_lt_n show ?thesis by (unfold wf_dom_def) (rule propa_dom_invariant_aux) qed lemma step_dom_mono_aux: fixes \ p \' a b assumes sorted: "sorted (rev (transf p \)) " and a_b_step: "(a, b) \ set (step p \) " and "\ \ A " and " p < n " and " \ \\<^bsub>r\<^esub> \'" shows "\\''. (a, \'') \ set (step p \') \ b \\<^bsub>r\<^esub> \''" proof- have step1: "step p \ = map (\pc. (pc, (transf p \))) (rev (sorted_list_of_set(succs p)))" by (simp add:step_def exec_def) from a_b_step have "set (step p \) \ {}" by auto with step1 have succ_p_n_nil: "(rev (sorted_list_of_set(succs p))) \ []" by auto from \p have "p \ set (g_V G)" using n_def nodes_def verts_set len_verts_gt0 by auto then have fin: "finite (succs p)" using fin_succs by auto with step1 have "\(x,y)\ set (step p \). x \ succs p" and step2: "\(x,y)\ set (step p \). y = transf p \" by (auto simp add:step_def exec_def) with a_b_step have "a \ succs p" by auto then have "succs p \ {}" by auto from step2 a_b_step have b: "b = transf p \" by auto have step2: "step p \' = map (\pc. (pc, (transf p \'))) (rev (sorted_list_of_set(succs p)))" by (simp add:step_def exec_def) with fin have g1: "\(x,y)\ set (step p \'). x \ succs p" and g2: "\(x,y)\ set (step p \'). y = transf p \'" by (auto simp add:step_def exec_def) with \a \ succs p\ have "\t. (a,t)\ set (step p \')" using fin by (auto simp add:step_def exec_def) then obtain t where ex: "(a,t)\ set (step p \')" by auto with g2 have t: "t = transf p \'" by auto from\ \ \\<^bsub>r\<^esub> \'\ have g: "sorted (rev \) \ sorted (rev \')\ set \' \ set \ \ \ = \'" by (auto simp add:r_def lesssub_def lesub_def nodes_le_def) then have subset_p: "set (p#\') \ set (p# \)" and "set \' \ set \" by auto from sorted have "\x\ set \. x < p" and "sorted (rev \')" using g by (auto simp add:sorted_wrt_append transf_def) with \set \' \ set \\ have "\x\ set \'. x < p" by auto with \sorted (rev \')\ have "sorted (rev (p#\'))" by (auto simp add:sorted_wrt_append) with sorted b t subset_p have "b \\<^bsub>r\<^esub> t" by (auto simp add:r_def lesssub_def lesub_def nodes_le_def transf_def) with ex show ?thesis by auto qed lemma step_dom_mono: "(\\ p \'. \ \ A \ p \ \\<^sub>r \' \ sorted (rev (transf p \)) \ set (step p \) {\\<^bsub>r\<^esub>} set (step p \'))" apply(unfold mono_def lesubstep_type_def) by(auto simp add:step_dom_mono_aux n_def nodes_def transf_def) lemma propa_termination: fixes a b assumes wf_a_b: "wf_dom a b" and b_n_nil: "b \ [] " shows "(propa f (step (hd b) (a ! hd b)) a (tl b), a, b) \ {(ss', ss). ss [\\<^bsub>r\<^esub>] ss'} <*lex*> (\x. case x of (x, y) \ (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset" proof- let ?qs = "(step (hd b) (a ! hd b))" from wf_a_b have "\x\set b. x < n" and n_len: "length a = n" and sorted_b: "sorted b" and set_a: "set a \ A" by (auto simp add:wf_dom_def) then have sorted_tl_b: "sorted (tl b)" and hd_b_lt_n: "hd b < n" using b_n_nil by (induct b) (auto simp add:sorted_wrt_append) - from set_a have a_inA: "a \ list n A" using n_len by (auto intro: listI) + from set_a have a_inA: "a \ nlists n A" using n_len by (auto intro: nlistsI) from hd_b_lt_n have dist: "distinct (map fst ?qs)" using distinct_p by auto from wf_a_b b_n_nil have step_pres_bounded: "\(q, \)\set ?qs. q < n \ \ \ A" using propa_dom_invariant_auxi n_len by fastforce with sorted_tl_b set_a n_len have propa: "propa f ?qs a (tl b) = (merges f ?qs a, (sorted_list_of_set ({q. \t.(q,t)\set ?qs \ t \\<^bsub>f\<^esub> (a!q) \ a!q} \ set(tl b))))" by (auto dest: decomp_propa) from a_inA step_pres_bounded sorted_b b_n_nil dist have "((merges f ?qs a, (sorted_list_of_set ({q. \t.(q,t)\set ?qs \ t \\<^bsub>f\<^esub> (a!q) \ a!q} \ set(tl b)))),(a,b)) \ {(ss', ss). ss [\\<^bsub>r\<^esub>] ss'} <*lex*> (\x. case x of (x, y) \ (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset" by (auto simp add: finite_psubset_def dest: termination_lemma) with propa show ?thesis by auto qed lemma iter_dom_invariant: assumes "wf_dom ss0 w0" shows "iter f step ss0 w0 = (ss',w') \ wf_dom ss' w'" using assms apply (unfold iter_def) apply(rule_tac P = "(\(ss, w). wf_dom ss w )" and r = "{(ss',ss). ss [\\<^sub>r] ss'} <*lex*> (\(x,y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset" in while_rule) \ \Invariant holds initially:\ apply (clarsimp) \ \Invariant is preserved:\ apply(simp add: wf_dom_def) apply clarsimp apply(rule propa_dom_invariant_aux') apply assumption+ \ \Postcondition holds upon termination:\ apply clarsimp \ \Well-foundedness of the termination relation:\ apply (simp add: wf_listn_termination_rel) \ \Loop decreases along termination relation:\ apply clarsimp apply (fastforce intro:propa_termination) done lemma propa_dom_invariant_aux2: fixes ss w ssa wa assumes wf_dom_ss0_w0: "wf_dom ss0 w0" and w_n_nil: "w \ [] " and propa: "propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ssa, wa) " and wf_ss_w: "wf_dom ss w " and ss0_lt_ss: "ss0 [\\<^bsub>r\<^esub>] ss" - and sta: " \ts\list n A. ss0 [\\<^bsub>r\<^esub>] ts \ (\p ss [\\<^bsub>r\<^esub>] ts" + and sta: " \ts\nlists n A. ss0 [\\<^bsub>r\<^esub>] ts \ (\p ss [\\<^bsub>r\<^esub>] ts" shows "ss0 [\\<^bsub>r\<^esub>] ssa \ - (\ts\list n A. ss0 [\\<^bsub>r\<^esub>] ts \ (\p ssa [\\<^bsub>r\<^esub>] ts)" + (\ts\nlists n A. ss0 [\\<^bsub>r\<^esub>] ts \ (\p ssa [\\<^bsub>r\<^esub>] ts)" using assms proof- let ?ss_hdw = "ss!hd w" from wf_dom_ss0_w0 have len_ss0: "length ss0 = n" and "\x\ set ss0. x \ A" by (auto simp add:wf_dom_def) - then have ss0_inA: "ss0 \ list n A" and set_ss0: "set ss0 \ A"by (auto intro:listI) + then have ss0_inA: "ss0 \ nlists n A" and set_ss0: "set ss0 \ A"by (auto intro:nlistsI) then have ss0_nth_inA: "\i A" by auto then have ss0_p_subset: "\p< length ss0. set (ss0!p) \ set nodes" by (auto simp add:inpow_subset_nodes A_def) from len_ss0 n_def nodes_def len_verts_gt0 have "0 < length ss0" by auto from ss0_lt_ss have "list_all2 (\x y. x \\<^sub>r y) ss0 ss" by (auto simp add:lesssub_def lesub_def list_all2_def Listn.le_def) then have lt1: "\p\<^bsub>r\<^esub> ss!p" by (auto simp add: list_all2_conv_all_nth) from wf_ss_w have "\\\set ss. \ \ A" and ass1: "\p (ss!p \ rev [0.. (\x\set (ss ! p). x < p)) \ (ss!p = rev [0.. (\x\ set w. (x,p)\ g_E G \ x < p)) \ (p \ set w \ stable r step ss p)" and sorted_w: "sorted w" and len_ss: "length ss = n" and w_lt_n: "\x\set w. x < n "by (auto simp add:wf_dom_def) - then have ss_inA: "ss \ list n A" and set_ss: "set ss \ A" by (auto intro:listI) + then have ss_inA: "ss \ nlists n A" and set_ss: "set ss \ A" by (auto intro:nlistsI) then have ss_nth_inA: "\i A" by auto then have ss_p_subset: "\p< length ss. set (ss!p) \ set nodes" by (auto simp add:inpow_subset_nodes A_def) then have ss_hdw_nodes: "set ?ss_hdw \ set nodes" using w_lt_n w_n_nil len_ss by auto let ?qs = "step (hd w) ?ss_hdw" from w_lt_n have hd_w_lt_n: "hd w < n" using w_n_nil by auto then have dist: "distinct (map fst ?qs)" using distinct_p by auto from ss_nth_inA have ss_hdw_inA: "?ss_hdw \ A" using w_lt_n w_n_nil len_ss by auto from ass1 have sorted_ss_hdw: "sorted (rev ?ss_hdw)" using w_lt_n w_n_nil by auto then have "\q\succs (hd w). q \ set (g_V G)" by (auto simp add:succ_in_G) then have hd_w_suc_lt_n: "\q\succs (hd w). q < n" using n_def verts_set nodes_def by auto have hdw_in_nodes:"hd w \ set (g_V G)" using verts_set n_def nodes_def w_lt_n w_n_nil by auto then have fin_succ_hd_w: "finite (succs (hd w))" using fin_succs by auto from sorted_w have sorted_tl_w': "sorted (tl w)" using w_n_nil by (induct w) auto from wf_ss_w w_n_nil have ss_hd_w_neq_all: "?ss_hdw \ (rev [0.. set nodes" and hd_w_ss_in_A: " (hd w # ?ss_hdw) \ A" and step_pres_bounded: " \(q, \)\set (step (hd w) ?ss_hdw). q < length ss \ \ \ A" using propa_dom_invariant_auxi by auto from ss_hd_w_neq_all have ss_lt_hd_w: "\x\set ?ss_hdw. x < hd w" using hd_w_lt_n wf_ss_w by (auto simp add:wf_dom_def) from wf_ss_w w_n_nil propa have wf_ssa_wa: "wf_dom ssa wa" using propa_dom_invariant by auto then have sorted_ssa_p: "\px\ set ssa. x \ A" and sorted_wa: "sorted wa" and len_ssa: "length ssa = n" and wa_lt_n: "\x\ set wa. x < n" by (auto simp add:wf_dom_def) - then have ssa_inA: "ssa\ list n A" and set_ssa: "set ssa \ A"by (auto intro:listI) + then have ssa_inA: "ssa\ nlists n A" and set_ssa: "set ssa \ A"by (auto intro:nlistsI) then have ssa_nth_inA: "\i A" by auto then have ssa_p_subset: "\p< length ssa. set (ssa!p) \ set nodes" by (auto simp add:inpow_subset_nodes A_def) from len_ss0 len_ssa have len_ss0_ssa: "length ss0 = length ssa" by simp from len_ss0 len_ss have len_ss0_ss: "length ss0 = length ss" by simp have "\(q, \)\set ?qs. \ = transf (hd w) (ss!(hd w))" by (simp add:step_def exec_def) then have transf_ss_hd_w: "\(q, \)\set ?qs. \ = (hd w # ?ss_hdw)" by (simp add:transf_def) from set_ss step_pres_bounded sorted_tl_w' len_ss dist have "\(q, \) \ set ?qs. (fst(propa f ?qs ss (tl w)))!q = \ \\<^bsub>f\<^esub>ss!q" by (auto dest:propa_property1) with propa have propa_ss: "\(q, \) \ set ?qs. ssa!q = \ \\<^bsub>f\<^esub>ss!q" by simp with transf_ss_hd_w have propa_ss1: "\(q, \) \ set ?qs. ssa!q = (hd w # ?ss_hdw) \\<^bsub>f\<^esub>ss!q" by auto from ss_nth_inA step_pres_bounded have "\(q, \) \ set ?qs. ss!q \ A" using hd_w_suc_lt_n fin_succ_hd_w by (auto simp add:step_def exec_def) from hd_w_ss_in_A this propa_ss1 have ss_lt_ssa_q: "\(q, \) \ set ?qs. ss!q \\<^bsub>r\<^esub> ssa!q" by (fastforce dest:Semilat.ub2[OF Semilat.intro, OF is_semi]) from step_pres_bounded sorted_tl_w' set_ss len_ss dist have "\q. q \ set(map fst ?qs) \ q < length ss \ (fst(propa f ?qs ss (tl w)))!q = ss!q" by (auto intro:propa_property2) with propa have exec2: "\q. q \ set(map fst ?qs) \ q < length ss \ ssa!q = ss!q" by auto have tran_ss_ssa: "\p\<^bsub>r\<^esub> ssa!p" proof(intro strip) fix p assume "p < length ss" with ssa_nth_inA have ssa_p_inA: "ssa!p \ A" using \length ssa = n\ \length ss = n\ by auto from ss_nth_inA have ss_p_inA: "ss!p \ A" using \length ss = n\ \p < length ss\ by auto show " ss ! p \\<^bsub>r\<^esub> ssa ! p" proof(cases "p \ succs (hd w)") case True then show "ss!p \\<^bsub>r\<^esub> ssa!p" using ss_lt_ssa_q using fin_succ_hd_w by (auto simp add:step_def exec_def) next case False then have "p \ set (map fst ?qs)" using fin_succ_hd_w by (auto simp add:step_def exec_def) then show ?thesis using exec2 \p < length ss\ using ssa_p_inA ss_p_inA by(auto simp add:step_def exec_def intro: Semilat.orderI[OF Semilat.intro, OF is_semi]) qed qed then have "\p\<^bsub>r\<^esub> ssa ! p" using len_ss0_ss by auto with lt1 have "\p\<^bsub>r\<^esub> ssa!p" using ss0_nth_inA ssa_nth_inA ss_nth_inA using len_ss0_ss len_ss0_ssa by (auto intro: order_trans Semilat.orderI[OF Semilat.intro, OF is_semi]) with len_ss0_ssa have g1: "ss0 [\\<^bsub>r\<^esub>] ssa" by (auto simp only:Listn.le_def lesssub_def lesub_def intro:list_all2_all_nthI) - have "(\ts\list n A. ss0 [\\<^bsub>r\<^esub>] ts \ (\p ssa [\\<^bsub>r\<^esub>] ts)" + have "(\ts\nlists n A. ss0 [\\<^bsub>r\<^esub>] ts \ (\p ssa [\\<^bsub>r\<^esub>] ts)" proof(intro strip) fix ts - assume ts_inA: "ts \ list n A" and ass: "ss0 [\\<^bsub>r\<^esub>] ts \ (\p nlists n A" and ass: "ss0 [\\<^bsub>r\<^esub>] ts \ (\p\<^bsub>r\<^esub>] ts" and sta_ts: "(\p\<^bsub>r\<^esub> ?ts_hdw "using le_listD len_ss hd_w_lt_n by auto then have "sorted (rev (?ts_hdw)) \ set ?ts_hdw \ set ?ss_hdw \ ?ss_hdw =?ts_hdw " by (auto simp add:r_def lesssub_def lesub_def nodes_le_def) then have sorted_ts_hdw: "sorted (rev (?ts_hdw))" and ts_ss_subset: "set ?ts_hdw \ set ?ss_hdw" using sorted_ss_hdw by (auto simp add:r_def lesssub_def lesub_def nodes_le_def) then have "\x\ set ?ts_hdw. x < hd w" using ss_lt_hd_w by auto with sorted_ts_hdw have sorted_hd_w_ts: "sorted (rev (hd w # ?ts_hdw))" by (auto simp add:sorted_wrt_append) with sorted_hd_w_ss ts_ss_subset have "(hd w # ?ss_hdw) \\<^bsub>r\<^esub> (hd w # ?ts_hdw)" by (auto simp add:transf_def lesssub_def lesub_def r_def nodes_le_def) then have transf_ss_ts: "transf (hd w) ?ss_hdw \\<^bsub>r\<^esub> transf (hd w) ?ts_hdw" by (auto simp add:transf_def) from sta_ts hd_w_lt_n have sta_ts_hdw: "stable r step ts (hd w)" by auto from ss_hdw_nodes ts_ss_subset have "set ?ts_hdw \ set nodes" by auto with hd_w_lt_n have hdw_ts_subset_nodes: "set (hd w # ?ts_hdw) \ set nodes" using nodes_def n_def verts_set by auto with sorted_hd_w_ts have "(hd w # ?ts_hdw) \ ( (rev \ sorted_list_of_set) ` (Pow (set nodes)))" by (fastforce intro: subset_nodes_inpow) then have transf_ts_inA: "(hd w #?ts_hdw) \ A" by (simp add:A_def) then have sorted_hdw_ts_hdw: "sorted (rev (hd w # ?ts_hdw))" by (rule inA_is_sorted) have "\p\<^bsub>r\<^esub> ts!p" proof(intro strip) fix p assume p_lt_len_ssa: "p < length ssa" then have "p < length ss" and "p < n" using len_ssa len_ss by auto with ss_ts have ss_ts_p: "ss!p \\<^bsub>r\<^esub> ts!p " using le_listD by auto show "ssa ! p \\<^bsub>r\<^esub> ts ! p" proof(cases "p \ succs (hd w)") case True note p_in_succs_hdw = this then have "ss!p \\<^bsub>r\<^esub> ssa!p" using ss_lt_ssa_q using fin_succ_hd_w by (auto simp add:step_def exec_def) from p_in_succs_hdw have ssa_p: "ssa!p = transf (hd w) (ss!hd w) \\<^bsub>f\<^esub>ss!p" using propa_ss fin_succ_hd_w by (auto simp add:step_def exec_def) from sta_ts_hdw have transf_hdw_ts_hdw: "transf (hd w) (ts!hd w) \\<^bsub>r\<^esub> ts!p" using p_in_succs_hdw fin_succ_hd_w by (auto simp add:step_def exec_def stable_def) then have ts_p_subset: "(hd w # ?ts_hdw) \\<^bsub>r\<^esub> ts!p" by (auto simp add:transf_def) then have "(sorted (rev (ts!p)) \ set (ts!p)\ set (hd w # ?ts_hdw)\ sorted (rev (hd w # ?ts_hdw))) \ hd w # ?ts_hdw = ts!p" by (auto simp add:r_def lesssub_def lesub_def nodes_le_def) then have "sorted (rev (ts!p)) \ set (ts!p)\ set (hd w # ?ts_hdw)" proof assume "sorted (rev (ts ! p)) \ set (ts ! p) \ set (hd w # ts ! hd w) \ sorted (rev (hd w # ts ! hd w))" then show ?thesis by auto next assume " hd w # ts ! hd w = ts ! p" with sorted_hdw_ts_hdw show ?thesis by auto qed then have sorted_ts_p: "sorted (rev (ts!p))" and ts_as_subset: "set (ts!p)\ set (hd w # ?ts_hdw)" by auto with hdw_ts_subset_nodes have "set (ts!p) \ set nodes" by auto with sorted_ts_p have "(ts!p) \ ( (rev \ sorted_list_of_set) ` (Pow (set nodes)))" by (fastforce intro: subset_nodes_inpow) then have ts_p_inA: "ts!p \ A" by (simp add:A_def) from sorted_hdw_ts_hdw have "\x\ set ?ts_hdw. x < hd w" by (auto simp add:sorted_wrt_append) with \hd w < n\ have "\x\ set ?ts_hdw. x < n" by auto then have "set(hd w # ?ts_hdw) \ set nodes"using \hd w < n\ n_def verts_set nodes_def by auto with sorted_hdw_ts_hdw have "hd w # ?ts_hdw \ ( (rev \ sorted_list_of_set) ` (Pow (set nodes)))" by (fastforce intro: subset_nodes_inpow) then have "(hd w # ?ts_hdw) \ A" by (auto simp add:A_def) then have trans_hdw_ts_inA: "transf (hd w) (ts!hd w) \ A" by (auto simp add:transf_def) have transf_hdw_ss_inA: "transf (hd w) ?ss_hdw \ A" using hd_w_ss_in_A by (auto simp add:transf_def) have ss_p_inA: "ss!p \ A" using \p ss_inA by auto from transf_ss_ts transf_hdw_ts_hdw transf_hdw_ss_inA trans_hdw_ts_inA ts_p_inA have "transf (hd w) ?ss_hdw \\<^bsub>r\<^esub> ts ! p" by (auto intro: order_trans Semilat.orderI[OF Semilat.intro, OF is_semi]) with \ss!p \\<^bsub>r\<^esub> ts ! p\ trans_hdw_ts_inA ss_p_inA transf_hdw_ss_inA ssa_p ts_p_inA show "ssa ! p \\<^bsub>r\<^esub> ts ! p" by (auto intro: Semilat.lub[OF Semilat.intro, OF is_semi]) next case False then have "p \ set (map fst ?qs)" using fin_succ_hd_w by (auto simp add:step_def exec_def) then have "ssa!p = ss!p"using exec2 p_lt_len_ssa len_ss len_ssa by(auto simp add:step_def exec_def) with ss_ts_p show ?thesis by auto qed qed with \length ss = length ts\ len_ss len_ssa show "ssa [\\<^bsub>r\<^esub>] ts" by (auto simp only:Listn.le_def lesssub_def lesub_def intro:list_all2_all_nthI) qed with g1 show ?thesis by auto qed -lemma in_list_nA_refl: "ss \ list n A \ ss [\\<^bsub>r\<^esub>] ss" +lemma in_list_nA_refl: "ss \ nlists n A \ ss [\\<^bsub>r\<^esub>] ss" apply (unfold Listn.le_def lesssub_def lesub_def) proof- - assume "ss \ list n A" + assume "ss \ nlists n A" then have "set ss \ A" and "length ss = n" by auto then have "\i A" by auto then have "\i\<^bsub>r\<^esub> ss!i" by (auto simp add:r_def lesssub_def lesub_def nodes_le_def ) then show " list_all2 r ss ss" by (auto simp add:lesssub_def lesub_def intro: list_all2_all_nthI) qed lemma iter_dom: assumes "wf_dom ss0 w0" shows "iter f step ss0 w0 = (ss',w') \ wf_dom ss' w' \ stables r step ss' \ ss0 [\\<^sub>r] ss' \ - (\ts\list n A. ss0 [\\<^sub>r] ts \ stables r step ts \ ss' [\\<^sub>r] ts)" + (\ts\nlists n A. ss0 [\\<^sub>r] ts \ stables r step ts \ ss' [\\<^sub>r] ts)" using assms apply (unfold iter_def stables_def) - apply (rule_tac P = "\(ss,w). wf_dom ss w \ ss0 [\\<^sub>r] ss \ (\ts\list n A. ss0 [\\<^sub>r] ts \ stables r step ts \ ss [\\<^sub>r] ts)" + apply (rule_tac P = "\(ss,w). wf_dom ss w \ ss0 [\\<^sub>r] ss \ (\ts\nlists n A. ss0 [\\<^sub>r] ts \ stables r step ts \ ss [\\<^sub>r] ts)" and r = "{(ss',ss). ss [\\<^sub>r] ss'} <*lex*> (\(x,y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset" in while_rule) \ \Invariant holds initially:\ apply(fastforce simp add: wf_dom_def intro:wf_dom_le) \ \Invariant is preserved:\ apply clarsimp apply (rule conjI) apply(fastforce dest:propa_dom_invariant) apply(simp add:stables_def) apply (rule propa_dom_invariant_aux2) apply assumption+ \ \Postcondition holds upon termination:\ apply(clarsimp simp add: stables_def split_paired_all) apply(subgoal_tac "length ss0 = n") apply(simp add:wf_dom_def)+ \ \Well-foundedness of the termination relation:\ apply clarsimp apply(simp add:wf_listn_termination_rel) \ \Loop decreases along termination relation:\ apply clarsimp apply (fastforce intro:propa_termination) done lemma wf_start: "wf_dom start (unstables r step start)" proof- let ?w0 = "unstables r step start" have sorted_w: "sorted ?w0" using unstables_def by (simp add:sorted_less_sorted_list_of_set) have w0_lt_n: "\x\set ?w0. x < n" using unstables_def len_start_is_n by auto have neq_all: "\p < n. start!p \ rev [0..< n] \ (\x\set (start!p). x < p) " proof(intro strip) fix p x assume p_lt_n: "p < n" and p_neq_all: "start ! p \ rev [0..< n]" and x_in: "x \ set (start ! p)" then have "p = 0" using start_nth_lt0_all len_start_is_n by auto with start_nth0_empty show "x < p" using x_in by auto qed have eq_all:"(\p < n. start!p = rev [0..< n] \ (\x\ set ?w0. (x,p)\ g_E G \ x < p))" proof(intro strip) fix p assume p_lt_n: "p < n" and p_eq_all: "start ! p = rev [0..< n]" from \p < n\ have "p = 0 \ p > 0 \ p < length start" using len_start_is_n by auto with p_eq_all have "p > 0" and p_lt_len_start: "p < length start" using start_nth0_empty n_def nodes_def len_verts_gt0 by auto then have "p \ set (g_V G) - {0}" using len_start_is_n n_def nodes_def verts_set by auto with dfst obtain prev where "(prev, p) \ g_E G" and "prev < p" by auto then have "succs prev \ {}" and "prev < length start" using p_lt_len_start by (auto simp add:succs_def) with unstable_start have "prev \ set ?w0" by auto with \(prev, p) \ g_E G\ \prev < p\ show "\x\set (unstables r step start). (x, p) \ g_E G \ x < p" by auto qed have "\p set (unstables r step start)\ stable r step start p)" by (unfold unstables_def) (simp add:n_def start_def nodes_def) with sorted_start_nth neq_all eq_all start_subset_A sorted_w len_start_is_n w0_lt_n show ?thesis by (auto simp only:wf_dom_def) qed lemma iter_dom_properties: "iter f step start (unstables r step start) = (ss',w') \ wf_dom ss' w' \ stables r step ss' \ start [\\<^sub>r] ss' \ - (\ts\list n A. start [\\<^sub>r] ts \ stables r step ts \ ss' [\\<^sub>r] ts)" + (\ts\nlists n A. start [\\<^sub>r] ts \ stables r step ts \ ss' [\\<^sub>r] ts)" using iter_dom[OF wf_start] by auto lemma iter_dom_properties2: - "iter f step start (unstables r step start) = (ss',w') \ ss' \ list n A" - using iter_dom_properties by (auto simp only:wf_dom_def list_def) + "iter f step start (unstables r step start) = (ss',w') \ ss' \ nlists n A" + using iter_dom_properties by (auto simp only:wf_dom_def nlists_def) lemma iter_dom_termination: "iter f step start (unstables r step start) = (ss,w) \ w \ [] \ propa f (step (hd w) (ss!(hd w))) ss (tl w) = (ss, tl w)" proof (intro strip) assume iter: "iter f step start (unstables r step start) = (ss, w)" and w_n_nil: "w \ []" with iter_dom_properties have stas: "stables r step ss" and wf_ss_w: "wf_dom ss w" and start_le_ss: "start [\\<^sub>r] ss" by auto from stas have sta_p: "(\p < size ss. stable r step ss p)"by (auto simp add:stables_def) from wf_ss_w have n_w_sta: "\pset w \ stable r step ss p" and len_eq: "length ss = n" and w_lt_n: "\x\ set w. x < n" and ss_inA: "\x\set ss. x \ A" and sorted_w: "sorted w " by (auto simp add:wf_dom_def) from w_lt_n have hd_w_lt_n: "hd w < n" using w_n_nil by auto then have hd_w_in_verts: "hd w \ set (g_V G)" using n_def nodes_def verts_set by auto then have fin_succ_hd_w: "finite (succs (hd w))" using fin_succs hd_w_in_verts by auto let ?ss_hdw = "ss!hd w" let ?qs = "step (hd w) ?ss_hdw" from hd_w_lt_n have dist: "distinct (map fst ?qs)" using distinct_p by auto from wf_ss_w w_n_nil have hdw_ss_subset_nodes: "set (hd w # ?ss_hdw) \ set nodes" and sorted_hd_w_ss: "sorted (rev (hd w # ?ss_hdw))" and hd_w_ss_in_A: " ((hd w # ?ss_hdw)) \ A" and step_pres_bounded: "\(q, \)\set ?qs. q < length ss \ \ \ A" using propa_dom_invariant_auxi by auto let ?res = "propa f (step (hd w) (ss!(hd w))) ss (tl w) " have "propa f (step (hd w) (ss!(hd w))) ss (tl w) = ?res" by simp then obtain ss' w' where propa: "propa f (step (hd w) (ss!(hd w))) ss (tl w) = (ss', w')" by (cases ?res) auto from sorted_w have sorted_tl_b: "sorted (tl w)" by (induct w) auto from ss_inA have set_a: "set ss \ A" by auto with step_pres_bounded sorted_tl_b len_eq dist have "\(q, \) \ set ?qs. (fst(propa f ?qs ss (tl w)))!q = \ \\<^bsub>f\<^esub>ss!q" by (auto dest:propa_property1) with propa have propa_ss1: "\(q, \) \ set ?qs. ss'!q = (hd w # ?ss_hdw) \\<^bsub>f\<^esub>ss!q" by (simp add:step_def exec_def transf_def) from step_pres_bounded sorted_tl_b set_a len_eq dist have "\q. q \ set(map fst ?qs) \ q < length ss \ (fst(propa f ?qs ss (tl w)))!q = ss!q" by (auto intro:propa_property2) with propa have g2: "\q. q \ set(map fst ?qs) \ q < length ss \ ss'!q = ss!q" by auto from sorted_w have sorted_tl_w: "sorted (tl w)" by (induct w) auto with step_pres_bounded set_a have fst_propa: "fst (propa f ?qs ss (tl w)) = (merges f ?qs ss)" and snd_propa: "snd (propa f ?qs ss (tl w)) = (sorted_list_of_set ({q. \t.(q,t)\set ?qs \ t \\<^bsub>f\<^esub> (ss!q) \ ss!q} \ set (tl w)))" using decomp_propa by auto with propa have len_ss_eq_ss': "length ss' = length ss" using length_merges by auto have ss_ss'_eq: "\ilength ss = n\ by auto show "fst (propa f ?qs ss (tl w)) ! i = ss ! i " proof(cases "i \ set(map fst ?qs)") case True assume ass1: "i \ set (map fst ?qs)" with propa_ss1 have ss': "ss'!i = (hd w # ?ss_hdw) \\<^bsub>f\<^esub>ss!i" by (auto simp add: step_def exec_def) from ass1 have "i \ set (g_V G)" using succ_in_G fin_succ_hd_w by (auto simp add:step_def exec_def) then have q_lt_len_ss: "i < length ss" using len_eq by (auto simp add:n_def nodes_def verts_set) from hd_w_lt_n len_eq stas have "stable r step ss (hd w)" by (auto simp add:stables_def) with ass1 have "(hd w # ?ss_hdw) \\<^sub>r ss!i" by (auto simp add:stables_def stable_def step_def exec_def transf_def) then have "set (ss!i) \ set (hd w # ?ss_hdw) \ (hd w # ?ss_hdw) = ss!i" by (auto simp add:lesssub_def lesub_def r_def nodes_le_def) then have set_ss_q_subst_hdw_ss: "set (ss!i) \ set (hd w # ?ss_hdw)" by (rule disjE)(auto simp add:lesssub_def lesub_def r_def nodes_le_def) then have ss_q: "set (ss!i) \ set (hd w # ?ss_hdw) = set (ss!i)" by auto from wf_ss_w q_lt_len_ss have sorted_ss_q: "sorted (rev (ss!i))" by (simp add:wf_dom_def) with sorted_hd_w_ss have ss_q': "set (ss'!i) = set (ss!i) \ set (hd w # ?ss_hdw)" and sorrted_ss_q': "sorted (rev (ss'!i))" using ss' by (auto simp add:plussub_def f_def nodes_sup_def inter_sorted_correct) with ss_q sorted_ss_q sorrted_ss_q' show ?thesis using sorted_less_rev_set_unique propa by auto next case False note i_nin = this from step_pres_bounded sorted_tl_b set_a len_eq dist propa i_lt_len_ss i_nin show ?thesis by (fastforce dest:propa_property2) qed qed with len_ss_eq_ss' have eq_ss: "ss' = ss" using len_eq propa by (auto simp add:list_eq_iff_nth_eq) then have qs_empty: "(({q. \t.(q,t)\set ?qs \ t \\<^bsub>f\<^esub> (ss!q) \ ss!q} \ set (tl w))) = (set (tl w))" using propa_ss1 propa transf_def step_def exec_def by fastforce with snd_propa have "snd (propa f ?qs ss (tl w)) = sorted_list_of_set (set (tl w))" using sorted_w by auto with sorted_tl_w have "snd (propa f ?qs ss (tl w)) = tl w" by (fastforce dest:sorted_less_set_eq) with propa have "w' = tl w" by simp with eq_ss show "propa f (step (hd w) (ss ! hd w)) ss (tl w) = (ss, tl w)" using propa by auto qed lemma dom_iter_properties: "iter f step start (unstables r step start) = (ss, w) \ ss!0 = [] \ (\p 0 \ ss!p \ (rev [0..\<^sub>r] ss" - and ss_inA: "ss \ list n A" by auto - then have len_ss_n: "length ss = n" by (auto simp only:list_def) + and ss_inA: "ss \ nlists n A" by auto + then have len_ss_n: "length ss = n" by (auto simp only:nlists_def) from start_le_ss have "start!0 \\<^sub>r ss!0" using start_len_gt_0 by (unfold Listn.le_def lesssub_def lesub_def) (auto simp add:lesssub_def lesub_def intro:list_all2_nthD) then have ss_0th: "ss!0 = []" by (auto simp add:r_def nodes_le_def lesssub_def lesub_def start_def) have "(\p 0 \ ss ! p \ (rev [0..0" and ss_p_eq_all: "\ ss ! p \ rev [0..(q,\) \ set (step p (ss!p)). \ \\<^sub>r ss!q" by (simp add: stables_def stable_def) from p_lt_n len_start_is_n verts_set have p_is_vert: "p \ set (g_V G)" by (auto simp add:n_def nodes_def) then have step_p: "\(q,\) \ set (step p (ss!p)). q \ succs p" using fin_succs by (auto simp add:step_def exec_def) from p_is_vert p_neq_0 dfst obtain prev where "(prev, p) \ g_E G" and prev_lt_p: "prev < p" by auto then have prev_lt_n: "prev < n" and prev_p: "p \ succs prev" and "prev \ set (g_V G)" using p_lt_n tail_is_vert by (auto simp add:succs_def) then have fin_suc_prev : "finite (succs prev)" using fin_succs by auto let ?prev_\ = "ss!prev" from prev_lt_n stas \length ss = n\ have "stable r step ss prev" by (auto simp add:stables_def) then have "\(q,\) \ set (step prev ?prev_\). (prev # ?prev_\) \\<^sub>r ss!q" by (auto simp add: stable_def transf_def step_def exec_def) with prev_p have "(prev # ?prev_\) \\<^bsub>r\<^esub> ss ! p" using fin_suc_prev by (auto simp add: stable_def transf_def step_def exec_def) with ss_p_eq_all have "sorted (rev (prev # ?prev_\)) \ {0.. set (prev # ?prev_\) \ (prev # ss ! prev) = (rev [0..)) \ {0.. set (prev # ?prev_\)" by(rule disjE) auto then have sorted_rev: "sorted (rev (prev # ?prev_\))" and pres_subset: "{0.. set (prev # ?prev_\)" by auto then have prev_set: "\x\ set ?prev_\. x < prev" by (induct ?prev_\) (auto simp add:sorted_wrt_append) from p_lt_n prev_lt_p have "prev < n - 1" using n_def nodes_def len_verts_gt0 by auto with prev_set have prev_lt_n: "\x\set(prev # ?prev_\). x < n - 1" by auto from pres_subset have "n - 1 \ set (prev # ?prev_\)" using n_def nodes_def len_verts_gt0 by fastforce with prev_lt_n show False by auto qed with ss_0th show " ss ! 0 = [] \ (\p 0 \ ss ! p \ rev [0.. (\p (rev [0.. (rev [0.. list n A \ + "kildall r f step start \ nlists n A \ stables r step (kildall r f step start) \ start [\\<^sub>r] (kildall r f step start) \ - (\ts\list n A. start [\\<^sub>r] ts \ stables r step ts \ (kildall r f step start) [\\<^sub>r] ts)" (is "PROP ?P") + (\ts\nlists n A. start [\\<^sub>r] ts \ stables r step ts \ (kildall r f step start) [\\<^sub>r] ts)" (is "PROP ?P") by (case_tac "iter f step start (unstables r step start)")(simp add: kildall_def iter_dom_properties iter_dom_properties2) lemma dom_kildall_stables: "stables r step (dom_kildall start)" using kildall_dom_properties by(unfold dom_kildall_def nodes_semi_def) (simp add: r_def f_def step_def) lemma dom_kildall_entry: "dom_kildall start !0 = []" by (case_tac "iter f step start (unstables r step start)") (auto simp add:dom_kildall_def nodes_semi_def dom_iter_properties r_def f_def step_def kildall_def) lemma zero_dom_zero: "dom i 0 \ i = 0" using start_def n_def nodes_def dom_kildall_entry by (simp add:dom_def) (*lemma sadom_succs: "strict_dom i j \ j \ succs k \ strict_dom i k"*) lemma sdom_dom_succs: "strict_dom i j \ j \ succs k \ dom i k" proof - assume sdom_i_j: "strict_dom i j" and k_j: "j \ succs k" then have j: "j \ set (g_V G)" and k: "k \ set (g_V G)" using verts_set succ_in_verts by auto then have j_lt_n: "j < n" and k_lt_n: "k < n" using n_def nodes_def verts_set by auto have fin_succs_k: "finite (succs k)" using fin_succs k by auto with k_j have k_j2: "j \ set (rev (sorted_list_of_set(succs k)))" by auto let ?ss0 = "start" let ?w0 = "unstables r step start" let ?res = "dom_kildall start" have dom_kil: "?res = kildall r f step ?ss0" by (auto simp add:dom_kildall_def r_def f_def step_def nodes_semi_def) have sorted_unstables: "sorted ?w0" by (auto simp add:unstables_def sorted_less_sorted_list_of_set) have ss: "?res = fst (iter f step ?ss0 ?w0)" by (auto simp add:dom_kildall_def kildall_def f_def step_def nodes_semi_def start_def r_def) then obtain ww where dom_iter: "iter f step ?ss0 ?w0 = (?res, ww)" by (cases "iter f step ?ss0 ?w0") auto with iter_dom_properties have wf_res: "wf_dom (dom_kildall start) ww" by auto with sdom_i_j have i_dom_j: "i \ set (?res!j)" by (auto simp add:strict_dom_def start_def n_def nodes_def) from wf_res have len_res: "length ?res = n" by (auto simp add:wf_dom_def) show "dom i k" proof(rule ccontr) assume ass: "\ dom i k" then have i_neq_k: "i \ k" by (auto simp add:dom_refl) with ass have "(\res. ?res!k = res \ i \ set res)" using ass by (auto simp add:dom_def start_def nodes_def n_def) then show False proof - assume "\res. ?res ! k = res \ i \ set res" then obtain rs where k_dom: "?res ! k = rs" and i_notin_rs: "i \ set rs" by auto from iter_dom_properties dom_iter have "(\p < length ?res. stable r step ?res p)" by (auto simp add:stables_def) with k_lt_n have "stable r step ?res k" using len_res by auto with k_dom have aux: "\(q,\) \ set (map (\pc. (pc, (k # rs))) (rev (sorted_list_of_set(succs k)))). \ \\<^sub>r ?res!q" by (simp add:stable_def r_def step_def exec_def transf_def) with k_j2 have "(k # rs) \\<^sub>r ?res!j" by auto then have "set (?res!j) \ set (k # rs) \ ?res!j = k#rs" by (auto simp add:lesssub_def lesub_def nodes_semi_def nodes_le_def r_def f_def) then have "set (?res!j) \ set (k # rs)" by auto with i_dom_j i_neq_k have " i \ set rs" by auto with i_notin_rs show False by auto qed qed qed lemma adom_succs: "dom i j \ i \ j \ j \ succs k \ dom i k" by (auto intro: dom_sdom sdom_dom_succs) lemma dom_kildall_is_strict: "j < length start \ dom_kildall start ! j = res \ j \ set res" proof - assume j_dom: "dom_kildall start ! j = res" and j_lt: "j < length start" from j_dom have iter_fst: "(fst (iter f step start (unstables r step start))) ! j = res" by (auto simp add:dom_kildall_def r_def f_def step_def start_def nodes_semi_def kildall_def) then obtain ss w where iter: "iter f step start (unstables r step start) = (ss, w)" by fastforce with iter_fst have res: "ss!j = res" by auto with dom_iter_properties2 iter have res_neq_all: "res \ rev [0..p < n. (ss!p) \ rev [0..< n] \ (\x\set ( (ss!p)). x < p)" by (auto simp add:wf_dom_def) with j_lt len_start_is_n res res_neq_all have "(\x\set res. x < j)" by (auto simp add:wf_dom_def) then show "j \ set res" by auto qed lemma sdom_asyc: "strict_dom i j \ j \ set (g_V G) \ i \ j" proof- assume sdom_i_j: "strict_dom i j" and "j \ set (g_V G)" then have j_lt: "j < length start" using start_def n_def nodes_def verts_set by auto let ?start = " [] # (replicate (length (g_V G) - 1) ( (rev[0.. set (dom_kildall ?start !j)" by (auto simp add:strict_dom_def) from j_lt have j_nin: "j \ set (dom_kildall ?start !j)" using eq_start by (simp add: dom_kildall_is_strict) with i_in show "i \ j" by auto qed lemma propa_dom_invariant_complete: fixes i a b ss w assumes b_n_nil: "b \ [] " and propa: "propa f (step (hd b) (a ! hd b)) a (tl b) = (ss, w) " and wf_a_b: "wf_dom a b" and non_strict: "\i. i < n \ k \ set (a!i) \ non_strict_dominate k i " shows "wf_dom ss w \ (\i. i < n \ k \ set ( ss ! i) \ non_strict_dominate k i)" (is "?PROP ?P") using assms proof- let ?a_hdb = "a!hd b" let ?qs = "step (hd b) (a!hd b)" from wf_a_b b_n_nil propa have wf_ss_w: "wf_dom ss w" using propa_dom_invariant by auto from wf_a_b have "\\\set a. \ \ A" and sorted_b: "sorted b" and len_a: "length a = n" and b_lt_n: "\x\set b. x < n "by (auto simp add:wf_dom_def) - then have set_a: "set a \ A" by (auto intro:listI) + then have set_a: "set a \ A" by (auto intro:nlistsI) from sorted_b have sorted_tl_b: "sorted (tl b)" using b_n_nil by (induct b) auto from b_lt_n b_n_nil have hd_b_lt_n: "hd b < n" by auto with n_def nodes_def verts_set have "hd b \ set (g_V G)" using b_n_nil by auto then have fin_succ_hd_b: "finite (succs (hd b))" using fin_succs by auto from wf_a_b b_n_nil have sorted_hd_b_a: "sorted (rev (hd b # ?a_hdb))" and step_pres_bounded: " \(q, \)\set (step (hd b) ?a_hdb). q < length a \ \ \ A" using propa_dom_invariant_auxi by auto from hd_b_lt_n have dist: "distinct (map fst ?qs)" using distinct_p by auto with set_a step_pres_bounded sorted_tl_b len_a have "\(q, \) \ set ?qs. (fst(propa f ?qs a (tl b)))!q = \ \\<^bsub>f\<^esub>a!q" by (auto dest:propa_property1) with propa have propa_ss1: "\(q, \) \ set ?qs. ss!q = (hd b # ?a_hdb) \\<^bsub>f\<^esub>a!q" by (auto simp add:step_def exec_def transf_def) from step_pres_bounded sorted_tl_b set_a len_a dist have "\q. q \ set(map fst ?qs) \ q < length a \ (fst(propa f ?qs a (tl b)))!q = a!q" by (auto intro:propa_property2) with propa have exec2: "\q. q \ set(map fst ?qs) \ q < length a \ ss!q = a!q" by auto have "(\i. i < n \ k \ set ( ss ! i) \ non_strict_dominate k i)" proof(intro strip) fix i let ?a_i = "a!i" assume "i < n \ k \ set ( ss ! i) " then have i_lt_n: "i < n" and k_nin_ss: "k \ set (ss ! i) " by auto from non_strict have g: "i < n \ a ! i = ?a_i \ k \ set ?a_i \ non_strict_dominate k i" by auto have sorted_a_i: "sorted (rev ?a_i)" using wf_a_b i_lt_n by (auto simp add:_wf_dom_def) show "non_strict_dominate k i" proof(cases "i \ (succs (hd b))") case True note i_succ_hdb = this with propa_ss1 have ss_i: "ss!i = (hd b # ?a_hdb) \\<^bsub>f\<^esub> a!i" using fin_succ_hd_b by (auto simp add:step_def exec_def) then have "ss!i = (hd b # ?a_hdb ) \\<^bsub>f\<^esub> ?a_i" by auto with sorted_hd_b_a sorted_a_i have "set (ss!i) = set (hd b # ?a_hdb) \ set ?a_i" and ss_i_merge: "ss!i = ((inter_sorted_rev (hd b # ?a_hdb) ?a_i))" by (auto simp add:inter_sorted_correct f_def nodes_sup_def plussub_def) with k_nin_ss have k_nin': "k \ set (hd b # ?a_hdb) \ set ?a_i" by auto show ?thesis proof(cases "k \ set ?a_i") case True then show ?thesis using i_lt_n g by auto next case False with k_nin' have "k \ set ?a_hdb" and k_neq_hdb: "k \ hd b" by auto with hd_b_lt_n non_strict have n_k_hdb: "non_strict_dominate k (hd b)" by auto from i_succ_hdb have "(hd b, i)\ g_E G" by (auto simp add:succs_def) with n_k_hdb k_neq_hdb show ?thesis using non_sdominate_succ by auto qed next case False with exec2 have "ss!i = a!i" using fin_succ_hd_b len_a i_lt_n by (auto simp add:step_def exec_def) with k_nin_ss have "k \ set (a!i)" by auto with non_strict show ?thesis using i_lt_n by fastforce qed qed with wf_ss_w show "?PROP ?P" by auto qed lemma start_non_sdom: " i < n \ start!i = res \ k \ set res \ non_strict_dominate k i" proof(auto) assume i_lt_n: "i < n" and k_nin: "k \ set (start ! i)" then have reach_i: "reachable i" using n_def nodes_def verts_set len_verts_gt0 reachable by (simp add:reachable_def) then obtain pa where pa_i: "path_entry (g_E G) pa i" using reachable_path_entry by auto show "non_strict_dominate k i" proof(cases "k \ set (g_V G)") case True then have "k < n" using verts_set by (auto simp add:n_def nodes_def) then have k_in_verts: "k \ set (g_V G)" and k_in_verts': "k \ {0..pa. path_entry (g_E G) pa i \ set pa \ set (g_V G)" using path_in_verts nodes_def by auto with k_nin_verts have k_nin: "\pa. path_entry (g_E G) pa i \ k \ set pa" by (fastforce dest: contra_subsetD) with pa_i have "k \ set pa" by auto with pa_i show ?thesis by (auto simp add: non_strict_dominate_def) qed qed lemma iter_dom_invariant_complete: shows "\res. iter f step start (unstables r step start) = (ss',w') \ i < n \ ss'!i = res \ k \ set res \ non_strict_dominate k i" apply (unfold iter_def) apply(rule_tac P = "(\(ss, w). wf_dom ss w \ (\i. (\rs. i < n \ ss!i = rs \ k \ set rs) \ non_strict_dominate k i))" and r = "{(ss',ss). ss [\\<^sub>r] ss'} <*lex*> (\(x,y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset" in while_rule) \ \Invariant holds initially:\ apply clarsimp apply (fastforce simp add:start_non_sdom wf_start) \ \Invariant is preserved:\ apply (fastforce dest:propa_dom_invariant_complete) \ \Postcondition holds upon termination:\ apply clarsimp \ \Well-foundedness of the termination relation:\ apply (simp add:wf_listn_termination_rel) \ \Loop decreases along termination relation:\ apply clarsimp apply (fastforce dest:propa_termination) done end end - - diff --git a/thys/HRB-Slicing/JinjaVM_Inter/JVMCFG.thy b/thys/HRB-Slicing/JinjaVM_Inter/JVMCFG.thy --- a/thys/HRB-Slicing/JinjaVM_Inter/JVMCFG.thy +++ b/thys/HRB-Slicing/JinjaVM_Inter/JVMCFG.thy @@ -1,825 +1,825 @@ chapter \A Control Flow Graph for Jinja Byte Code\ section \Formalizing the CFG\ theory JVMCFG imports "../StaticInter/BasicDefs" Jinja.BVExample begin declare lesub_list_impl_same_size [simp del] -declare listE_length [simp del] +declare nlistsE_length [simp del] subsection \Type definitions\ subsubsection \Wellformed Programs\ definition "wf_jvmprog = {(P, Phi). wf_jvm_prog\<^bsub>Phi\<^esub> P}" typedef wf_jvmprog = "wf_jvmprog" proof show "(E, Phi) \ wf_jvmprog" unfolding wf_jvmprog_def by (auto intro: wf_prog) qed hide_const Phi E abbreviation PROG :: "wf_jvmprog \ jvm_prog" where "PROG P \ fst(Rep_wf_jvmprog(P))" abbreviation TYPING :: "wf_jvmprog \ ty\<^sub>P" where "TYPING P \ snd(Rep_wf_jvmprog(P))" lemma wf_jvmprog_is_wf_typ: "wf_jvm_prog\<^bsub>TYPING P\<^esub> (PROG P)" using Rep_wf_jvmprog [of P] by (auto simp: wf_jvmprog_def split_beta) lemma wf_jvmprog_is_wf: "wf_jvm_prog (PROG P)" using wf_jvmprog_is_wf_typ unfolding wf_jvm_prog_def by blast subsubsection \Interprocedural CFG\ type_synonym jvm_method = "wf_jvmprog \ cname \ mname" datatype var = Heap | Local "nat" | Stack "nat" | Exception datatype val = Hp "heap" | Value "Value.val" type_synonym state = "var \ val" definition valid_state :: "state \ bool" where "valid_state s \ (\val. s Heap \ Some (Value val)) \ (s Exception = None \ (\addr. s Exception = Some (Value (Addr addr)))) \ (\var. var \ Heap \ var \ Exception \ (\h. s var \ Some (Hp h)))" fun the_Heap :: "val \ heap" where "the_Heap (Hp h) = h" fun the_Value :: "val \ Value.val" where "the_Value (Value v) = v" abbreviation heap_of :: "state \ heap" where "heap_of s \ the_Heap (the (s Heap))" abbreviation exc_flag :: "state \ addr option" where "exc_flag s \ case (s Exception) of None \ None | Some v \ Some (THE a. v = Value (Addr a))" abbreviation stkAt :: "state \ nat \ Value.val" where "stkAt s n \ the_Value (the (s (Stack n)))" abbreviation locAt :: "state \ nat \ Value.val" where "locAt s n \ the_Value (the (s (Local n)))" datatype nodeType = Enter | Normal | Return | Exceptional "pc option" "nodeType" type_synonym cfg_node = "cname \ mname \ pc option \ nodeType" type_synonym cfg_edge = "cfg_node \ (var, val, cname \ mname \ pc, cname \ mname) edge_kind \ cfg_node" definition ClassMain :: "wf_jvmprog \ cname" where "ClassMain P \ SOME Name. \ is_class (PROG P) Name" definition MethodMain :: "wf_jvmprog \ mname" where "MethodMain P \ SOME Name. \C D fs ms. class (PROG P) C = \(D, fs, ms)\ \ (\m \ set ms. Name \ fst m)" definition stkLength :: "jvm_method \ pc \ nat" where "stkLength m pc \ let (P, C, M) = m in ( if (C = ClassMain P) then 1 else ( length (fst(the(((TYPING P) C M) ! pc))) ))" definition locLength :: "jvm_method \ pc \ nat" where "locLength m pc \ let (P, C, M) = m in ( if (C = ClassMain P) then 1 else ( length (snd(the(((TYPING P) C M) ! pc))) ))" lemma ex_new_class_name: "\C. \ is_class P C" proof - have "\ finite (UNIV :: cname set)" by (rule infinite_UNIV_listI) hence "\C. C \ set (map fst P)" by -(rule ex_new_if_finite, auto) then obtain C where "C \ set (map fst P)" by blast have "\ is_class P C" proof assume "is_class P C" then obtain D fs ms where "class P C = \(D, fs, ms)\" by auto with \C \ set (map fst P)\ show False by (auto dest: map_of_SomeD intro!: image_eqI simp: class_def) qed thus ?thesis by blast qed lemma ClassMain_unique_in_P: assumes "is_class (PROG P) C" shows "ClassMain P \ C" proof - from ex_new_class_name [of "PROG P"] obtain D where "\ is_class (PROG P) D" by blast with \is_class (PROG P) C\ show ?thesis unfolding ClassMain_def by -(rule someI2, fastforce+) qed lemma map_of_fstD: "\ map_of xs a = \b\; \x \ set xs. fst x \ a \ \ False" by (induct xs, auto) lemma map_of_fstE: "\ map_of xs a = \b\; \x \ set xs. fst x = a \ thesis \ \ thesis" by (induct xs) (auto split: if_split_asm) lemma ex_unique_method_name: "\Name. \C D fs ms. class (PROG P) C = \(D, fs, ms)\ \ (\m\set ms. Name \ fst m)" proof - from wf_jvmprog_is_wf [of P] have "distinct_fst (PROG P)" by (simp add: wf_jvm_prog_def wf_jvm_prog_phi_def wf_prog_def) hence "{C. \D fs ms. class (PROG P) C = \(D, fs, ms)\} = fst ` set (PROG P)" by (fastforce elim: map_of_fstE simp: class_def intro: map_of_SomeI) hence "finite {C. \D fs ms. class (PROG P) C = \(D, fs, ms)\}" by auto moreover have "{ms. \C D fs. class (PROG P) C = \(D, fs, ms)\} = snd ` snd ` the ` (\C. class (PROG P) C) ` {C. \D fs ms. class (PROG P) C = \(D, fs, ms)\}" by (fastforce intro: rev_image_eqI map_of_SomeI simp: class_def) ultimately have "finite {ms. \C D fs. class (PROG P) C = \(D, fs, ms)\}" by auto moreover have "\ finite (UNIV :: mname set)" by (rule infinite_UNIV_listI) ultimately have "\Name. Name \ fst ` (\ms \ {ms. \C D fs. class (PROG P) C = \(D, fs, ms)\}. set ms)" by -(rule ex_new_if_finite, auto) thus ?thesis by fastforce qed lemma MethodMain_unique_in_P: assumes "PROG P \ D sees M:Ts\T = mb in C" shows "MethodMain P \ M" proof - from ex_unique_method_name [of P] obtain M' where "\C D fs ms. class (PROG P) C = \(D, fs, ms)\ \ (\m \ set ms. M' \ fst m)" by blast with \PROG P \ D sees M:Ts\T = mb in C\ show ?thesis unfolding MethodMain_def by -(rule someI2_ex, fastforce, fastforce dest!: visible_method_exists elim: map_of_fstE) qed lemma ClassMain_is_no_class [dest!]: "is_class (PROG P) (ClassMain P) \ False" proof (erule rev_notE) from ex_new_class_name [of "PROG P"] obtain C where "\ is_class (PROG P) C" by blast thus "\ is_class (PROG P) (ClassMain P)" unfolding ClassMain_def by (rule someI) qed lemma MethodMain_not_seen [dest!]: "PROG P \ C sees (MethodMain P):Ts\T = mb in D \ False" by (fastforce dest: MethodMain_unique_in_P) lemma no_Call_from_ClassMain [dest!]: "PROG P \ ClassMain P sees M:Ts\T = mb in C \ False" by (fastforce dest: sees_method_is_class) lemma no_Call_in_ClassMain [dest!]: "PROG P \ C sees M:Ts\T = mb in ClassMain P \ False" by (fastforce dest: sees_method_idemp) inductive JVMCFG :: "jvm_method \ cfg_node \ (var, val, cname \ mname \ pc, cname \ mname) edge_kind \ cfg_node \ bool" (" _ \ _ -_\ _") and reachable :: "jvm_method \ cfg_node \ bool" (" _ \ \_") where Entry_reachable: "(P, C0, Main) \ \(ClassMain P, MethodMain P, None, Enter)" | reachable_step: "\ P \ \n; P \ n -(e)\ n' \ \ P \ \n'" | Main_to_Call: "(P, C0, Main) \ \(ClassMain P, MethodMain P, \0\, Enter) \ (P, C0, Main) \ (ClassMain P, MethodMain P, \0\, Enter) -\id\ (ClassMain P, MethodMain P, \0\, Normal)" | Main_Call_LFalse: "(P, C0, Main) \ \(ClassMain P, MethodMain P, \0\, Normal) \ (P, C0, Main) \ (ClassMain P, MethodMain P, \0\, Normal) -(\s. False)\<^sub>\\ (ClassMain P, MethodMain P, \0\, Return)" | Main_Call: "\ (P, C0, Main) \ \(ClassMain P, MethodMain P, \0\, Normal); PROG P \ C0 sees Main:[]\T = (mxs, mxl\<^sub>0, is, xt) in D; initParams = [(\s. s Heap),(\s. \Value Null\)]; ek = (\(s, ret). True):(ClassMain P, MethodMain P, 0)\\<^bsub>(D, Main)\<^esub>initParams \ \ (P, C0, Main) \ (ClassMain P, MethodMain P, \0\, Normal) -(ek)\ (D, Main, None, Enter)" | Main_Return_to_Exit: "(P, C0, Main) \ \(ClassMain P, MethodMain P, \0\, Return) \ (P, C0, Main) \ (ClassMain P, MethodMain P, \0\, Return) -(\id)\ (ClassMain P, MethodMain P, None, Return)" | Method_LFalse: "(P, C0, Main) \ \(C, M, None, Enter) \ (P, C0, Main) \ (C, M, None, Enter) -(\s. False)\<^sub>\\ (C, M, None, Return)" | Method_LTrue: "(P, C0, Main) \ \(C, M, None, Enter) \ (P, C0, Main) \ (C, M, None, Enter) -(\s. True)\<^sub>\\ (C, M, \0\, Enter)" | CFG_Load: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Enter); instrs_of (PROG P) C M ! pc = Load n; ek = \(\s. s(Stack (stkLength (P, C, M) pc) := s (Local n))) \ \ (P, C0, Main) \ (C, M, \pc\, Enter) -(ek)\ (C, M, \Suc pc\, Enter)" | CFG_Store: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Enter); instrs_of (PROG P) C M ! pc = Store n; ek = \(\s. s(Local n := s (Stack (stkLength (P, C, M) pc - 1)))) \ \ (P, C0, Main) \ (C, M, \pc\, Enter) -(ek)\ (C, M, \Suc pc\, Enter)" | CFG_Push: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Enter); instrs_of (PROG P) C M ! pc = Push v; ek = \(\s. s(Stack (stkLength (P, C, M) pc) \ Value v)) \ \ (P, C0, Main) \ (C, M, \pc\, Enter) -(ek)\ (C, M, \Suc pc\, Enter)" | CFG_Pop: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Enter); instrs_of (PROG P) C M ! pc = Pop; ek = \id \ \ (P, C0, Main) \ (C, M, \pc\, Enter) -(ek)\ (C, M, \Suc pc\, Enter)" | CFG_IAdd: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Enter); instrs_of (PROG P) C M ! pc = IAdd; ek = \(\s. let i1 = the_Intg (stkAt s (stkLength (P, C, M) pc - 1)); i2 = the_Intg (stkAt s (stkLength (P, C, M) pc - 2)) in s(Stack (stkLength (P, C, M) pc - 2) \ Value (Intg (i1 + i2)))) \ \ (P, C0, Main) \ (C, M, \pc\, Enter) -(ek)\ (C, M, \Suc pc\, Enter)" | CFG_Goto: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Enter); instrs_of (PROG P) C M ! pc = Goto i \ \ (P, C0, Main) \ (C, M, \pc\, Enter) -((\s. True)\<^sub>\)\ (C, M, \nat (int pc + i)\, Enter)" | CFG_CmpEq: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Enter); instrs_of (PROG P) C M ! pc = CmpEq; ek = \(\s. let e1 = stkAt s (stkLength (P, C, M) pc - 1); e2 = stkAt s (stkLength (P, C, M) pc - 2) in s(Stack (stkLength (P, C, M) pc - 2) \ Value (Bool (e1 = e2)))) \ \ (P, C0, Main) \ (C, M, \pc\, Enter) -(ek)\ (C, M, \Suc pc\, Enter)" | CFG_IfFalse_False: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Enter); instrs_of (PROG P) C M ! pc = IfFalse i; i \ 1; ek = (\s. stkAt s (stkLength(P, C, M) pc - 1) = Bool False)\<^sub>\ \ \ (P, C0, Main) \ (C, M, \pc\, Enter) -(ek)\ (C, M, \nat (int pc + i)\, Enter)" | CFG_IfFalse_True: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Enter); instrs_of (PROG P) C M ! pc = IfFalse i; ek = (\s. stkAt s (stkLength(P, C, M) pc - 1) \ Bool False \ i = 1)\<^sub>\ \ \ (P, C0, Main) \ (C, M, \pc\, Enter) -(ek)\ (C, M, \Suc pc\, Enter)" | CFG_New_Check_Normal: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Enter); instrs_of (PROG P) C M ! pc = New Cl; ek = (\s. new_Addr (heap_of s) \ None)\<^sub>\ \ \ (P, C0, Main) \ (C, M, \pc\, Enter) -(ek)\ (C, M, \pc\, Normal)" | CFG_New_Check_Exceptional: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Enter); instrs_of (PROG P) C M ! pc = New Cl; pc' = (case (match_ex_table (PROG P) OutOfMemory pc (ex_table_of (PROG P) C M)) of None \ None | Some (pc'', d) \ \pc''\); ek = (\s. new_Addr (heap_of s) = None)\<^sub>\ \ \ (P, C0, Main) \ (C, M, \pc\, Enter) -(ek)\ (C, M, \pc\, Exceptional pc' Enter)" | CFG_New_Update: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Normal); instrs_of (PROG P) C M ! pc = New Cl; ek = \(\s. let a = the (new_Addr (heap_of s)) in s(Heap \ Hp ((heap_of s)(a \ blank (PROG P) Cl))) (Stack (stkLength(P, C, M) pc) \ Value (Addr a))) \ \ (P, C0, Main) \ (C, M, \pc\, Normal) -(ek)\ (C, M, \Suc pc\, Enter)" | CFG_New_Exceptional_prop: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Exceptional None Enter); instrs_of (PROG P) C M ! pc = New Cl; ek = \(\s. s(Exception \ Value (Addr (addr_of_sys_xcpt OutOfMemory)))) \ \ (P, C0, Main) \ (C, M, \pc\, Exceptional None Enter) -(ek)\ (C, M, None, Return)" | CFG_New_Exceptional_handle: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Exceptional \pc'\ Enter); instrs_of (PROG P) C M ! pc = New Cl; ek = \(\s. s(Exception := None) (Stack (stkLength (P, C, M) pc' - 1) \ Value (Addr (addr_of_sys_xcpt OutOfMemory)))) \ \ (P, C0, Main) \ (C, M, \pc\, Exceptional \pc'\ Enter) -(ek)\ (C, M, \pc'\, Enter)" | CFG_Getfield_Check_Normal: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Enter); instrs_of (PROG P) C M ! pc = Getfield F Cl; ek = (\s. stkAt s (stkLength (P, C, M) pc - 1) \ Null)\<^sub>\ \ \ (P, C0, Main) \ (C, M, \pc\, Enter) -(ek)\ (C, M, \pc\, Normal)" | CFG_Getfield_Check_Exceptional: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Enter); instrs_of (PROG P) C M ! pc = Getfield F Cl; pc' = (case (match_ex_table (PROG P) NullPointer pc (ex_table_of (PROG P) C M)) of None \ None | Some (pc'', d) \ \pc''\); ek = (\s. stkAt s (stkLength (P, C, M) pc - 1) = Null)\<^sub>\ \ \ (P, C0, Main) \ (C, M, \pc\, Enter) -(ek)\ (C, M, \pc\, Exceptional pc' Enter)" | CFG_Getfield_Update: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Normal); instrs_of (PROG P) C M ! pc = Getfield F Cl; ek = \(\s. let (D, fs) = the (heap_of s (the_Addr (stkAt s (stkLength (P, C, M) pc - 1)))) in s(Stack (stkLength(P, C, M) pc - 1) \ Value (the (fs (F, Cl))))) \ \ (P, C0, Main) \ (C, M, \pc\, Normal) -(ek)\ (C, M, \Suc pc\, Enter)" | CFG_Getfield_Exceptional_prop: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Exceptional None Enter); instrs_of (PROG P) C M ! pc = Getfield F Cl; ek = \(\s. s(Exception \ Value (Addr (addr_of_sys_xcpt NullPointer)))) \ \ (P, C0, Main) \ (C, M, \pc\, Exceptional None Enter) -(ek)\ (C, M, None, Return)" | CFG_Getfield_Exceptional_handle: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Exceptional \pc'\ Enter); instrs_of (PROG P) C M ! pc = Getfield F Cl; ek = \(\s. s(Exception := None) (Stack (stkLength (P, C, M) pc' - 1) \ Value (Addr (addr_of_sys_xcpt NullPointer)))) \ \ (P, C0, Main) \ (C, M, \pc\, Exceptional \pc'\ Enter) -(ek)\ (C, M, \pc'\, Enter)" | CFG_Putfield_Check_Normal: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Enter); instrs_of (PROG P) C M ! pc = Putfield F Cl; ek = (\s. stkAt s (stkLength (P, C, M) pc - 2) \ Null)\<^sub>\ \ \ (P, C0, Main) \ (C, M, \pc\, Enter) -(ek)\ (C, M, \pc\, Normal)" | CFG_Putfield_Check_Exceptional: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Enter); instrs_of (PROG P) C M ! pc = Putfield F Cl; pc' = (case (match_ex_table (PROG P) NullPointer pc (ex_table_of (PROG P) C M)) of None \ None | Some (pc'', d) \ \pc''\); ek = (\s. stkAt s (stkLength (P, C, M) pc - 2) = Null)\<^sub>\ \ \ (P, C0, Main) \ (C, M, \pc\, Enter) -(ek)\ (C, M, \pc\, Exceptional pc' Enter)" | CFG_Putfield_Update: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Normal); instrs_of (PROG P) C M ! pc = Putfield F Cl; ek = \(\s. let v = stkAt s (stkLength (P, C, M) pc - 1); r = stkAt s (stkLength (P, C, M) pc - 2); a = the_Addr r; (D, fs) = the (heap_of s a); h' = (heap_of s)(a \ (D, fs((F, Cl) \ v))) in s(Heap \ Hp h')) \ \ (P, C0, Main) \ (C, M, \pc\, Normal) -(ek)\ (C, M, \Suc pc\, Enter)" | CFG_Putfield_Exceptional_prop: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Exceptional None Enter); instrs_of (PROG P) C M ! pc = Putfield F Cl; ek = \(\s. s(Exception \ Value (Addr (addr_of_sys_xcpt NullPointer)))) \ \ (P, C0, Main) \ (C, M, \pc\, Exceptional None Enter) -(ek)\ (C, M, None, Return)" | CFG_Putfield_Exceptional_handle: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Exceptional \pc'\ Enter); instrs_of (PROG P) C M ! pc = Putfield F Cl; ek = \(\s. s(Exception := None) (Stack (stkLength (P, C, M) pc' - 1) \ Value (Addr (addr_of_sys_xcpt NullPointer)))) \ \ (P, C0, Main) \ (C, M, \pc\, Exceptional \pc'\ Enter) -(ek)\ (C, M, \pc'\, Enter)" | CFG_Checkcast_Check_Normal: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Enter); instrs_of (PROG P) C M ! pc = Checkcast Cl; ek = (\s. cast_ok (PROG P) Cl (heap_of s) (stkAt s (stkLength (P, C, M) pc - 1)))\<^sub>\ \ \ (P, C0, Main) \ (C, M, \pc\, Enter) -(ek)\ (C, M, \Suc pc\, Enter)" | CFG_Checkcast_Check_Exceptional: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Enter); instrs_of (PROG P) C M ! pc = Checkcast Cl; pc' = (case (match_ex_table (PROG P) ClassCast pc (ex_table_of (PROG P) C M)) of None \ None | Some (pc'', d) \ \pc''\); ek = (\s. \ cast_ok (PROG P) Cl (heap_of s) (stkAt s (stkLength (P, C, M) pc - 1)))\<^sub>\ \ \ (P, C0, Main) \ (C, M, \pc\, Enter) -(ek)\ (C, M, \pc\, Exceptional pc' Enter)" | CFG_Checkcast_Exceptional_prop: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Exceptional None Enter); instrs_of (PROG P) C M ! pc = Checkcast Cl; ek = \(\s. s(Exception \ Value (Addr (addr_of_sys_xcpt ClassCast)))) \ \ (P, C0, Main) \ (C, M, \pc\, Exceptional None Enter) -(ek)\ (C, M, None, Return)" | CFG_Checkcast_Exceptional_handle: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Exceptional \pc'\ Enter); instrs_of (PROG P) C M ! pc = Checkcast Cl; ek = \(\s. s(Exception := None) (Stack (stkLength (P, C, M) pc' - 1) \ Value (Addr (addr_of_sys_xcpt ClassCast)))) \ \ (P, C0, Main) \ (C, M, \pc\, Exceptional \pc'\ Enter) -(ek)\ (C, M, \pc'\, Enter)" | CFG_Throw_Check: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Enter); instrs_of (PROG P) C M ! pc = Throw; pc' = None \ match_ex_table (PROG P) Exc pc (ex_table_of (PROG P) C M) = \(the pc', d)\; ek = (\s. let v = stkAt s (stkLength (P, C, M) pc - 1); Cl = if (v = Null) then NullPointer else (cname_of (heap_of s) (the_Addr v)) in case pc' of None \ match_ex_table (PROG P) Cl pc (ex_table_of (PROG P) C M) = None | Some pc'' \ \d. match_ex_table (PROG P) Cl pc (ex_table_of (PROG P) C M) = \(pc'', d)\ )\<^sub>\ \ \ (P, C0, Main) \ (C, M, \pc\, Enter) -(ek)\ (C, M, \pc\, Exceptional pc' Enter)" | CFG_Throw_prop: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Exceptional None Enter); instrs_of (PROG P) C M ! pc = Throw; ek = \(\s. s(Exception \ Value (stkAt s (stkLength (P, C, M) pc - 1)))) \ \ (P, C0, Main) \ (C, M, \pc\, Exceptional None Enter) -(ek)\ (C, M, None, Return)" | CFG_Throw_handle: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Exceptional \pc'\ Enter); pc' \ length (instrs_of (PROG P) C M); instrs_of (PROG P) C M ! pc = Throw; ek = \(\s. s(Exception := None) (Stack (stkLength (P, C, M) pc' - 1) \ Value (stkAt s (stkLength (P, C, M) pc - 1)))) \ \ (P, C0, Main) \ (C, M, \pc\, Exceptional \pc'\ Enter) -(ek)\ (C, M, \pc'\, Enter)" | CFG_Invoke_Check_NP_Normal: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Enter); instrs_of (PROG P) C M ! pc = Invoke M' n; ek = (\s. stkAt s (stkLength (P, C, M) pc - Suc n) \ Null)\<^sub>\ \ \ (P, C0, Main) \ (C, M, \pc\, Enter) -(ek)\ (C, M, \pc\, Normal)" | CFG_Invoke_Check_NP_Exceptional: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Enter); instrs_of (PROG P) C M ! pc = Invoke M' n; pc' = (case (match_ex_table (PROG P) NullPointer pc (ex_table_of (PROG P) C M)) of None \ None | Some (pc'', d) \ \pc''\); ek = (\s. stkAt s (stkLength (P, C, M) pc - Suc n) = Null)\<^sub>\ \ \ (P, C0, Main) \ (C, M, \pc\, Enter) -(ek)\ (C, M, \pc\, Exceptional pc' Enter)" | CFG_Invoke_NP_prop: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Exceptional None Enter); instrs_of (PROG P) C M ! pc = Invoke M' n; ek = \(\s. s(Exception \ Value (Addr (addr_of_sys_xcpt NullPointer)))) \ \ (P, C0, Main) \ (C, M, \pc\, Exceptional None Enter) -(ek)\ (C, M, None, Return)" | CFG_Invoke_NP_handle: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Exceptional \pc'\ Enter); instrs_of (PROG P) C M ! pc = Invoke M' n; ek = \(\s. s(Exception := None) (Stack (stkLength (P, C, M) pc' - 1) \ Value (Addr (addr_of_sys_xcpt NullPointer)))) \ \ (P, C0, Main) \ (C, M, \pc\, Exceptional \pc'\ Enter) -(ek)\ (C, M, \pc'\, Enter)" | CFG_Invoke_Call: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Normal); instrs_of (PROG P) C M ! pc = Invoke M' n; TYPING P C M ! pc = \(ST, LT)\; ST ! n = Class D'; PROG P \ D' sees M':Ts\T = (mxs, mxl\<^sub>0, is, xt) in D; Q = (\(s, ret). let r = stkAt s (stkLength (P, C, M) pc - Suc n); C' = fst (the (heap_of s (the_Addr r))) in D = fst (method (PROG P) C' M')); paramDefs = (\s. s Heap) # (\s. s (Stack (stkLength (P, C, M) pc - Suc n))) # (rev (map (\i. (\s. s (Stack (stkLength (P, C, M) pc - Suc i)))) [0..\<^bsub>(D,M')\<^esub>paramDefs \ \ (P, C0, Main) \ (C, M, \pc\, Normal) -(ek)\ (D, M', None, Enter)" | CFG_Invoke_False: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Normal); instrs_of (PROG P) C M ! pc = Invoke M' n; ek = (\s. False)\<^sub>\ \ \ (P, C0, Main) \ (C, M, \pc\, Normal) -(ek)\ (C, M, \pc\, Return)" | CFG_Invoke_Return_Check_Normal: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Return); instrs_of (PROG P) C M ! pc = Invoke M' n; (TYPING P) C M ! pc = \(ST, LT)\; ST ! n \ NT; ek = (\s. s Exception = None)\<^sub>\ \ \ (P, C0, Main) \ (C, M, \pc\, Return) -(ek)\ (C, M, \Suc pc\, Enter)" | CFG_Invoke_Return_Check_Exceptional: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Return); instrs_of (PROG P) C M ! pc = Invoke M' n; match_ex_table (PROG P) Exc pc (ex_table_of (PROG P) C M) = \(pc', diff)\; pc' \ length (instrs_of (PROG P) C M); ek = (\s. \v d. s Exception = \v\ \ match_ex_table (PROG P) (cname_of (heap_of s) (the_Addr (the_Value v))) pc (ex_table_of (PROG P) C M) = \(pc', d)\)\<^sub>\ \ \ (P, C0, Main) \ (C, M, \pc\, Return) -(ek)\ (C, M, \pc\, Exceptional \pc'\ Return)" | CFG_Invoke_Return_Exceptional_handle: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Exceptional \pc'\ Return); instrs_of (PROG P) C M ! pc = Invoke M' n; ek = \(\s. s(Exception := None, Stack (stkLength (P, C, M) pc' - 1) := s Exception)) \ \ (P, C0, Main) \ (C, M, \pc\, Exceptional \pc'\ Return) -(ek)\ (C, M, \pc'\, Enter)" | CFG_Invoke_Return_Exceptional_prop: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Return); instrs_of (PROG P) C M ! pc = Invoke M' n; ek = (\s. \v. s Exception = \v\ \ match_ex_table (PROG P) (cname_of (heap_of s) (the_Addr (the_Value v))) pc (ex_table_of (PROG P) C M) = None)\<^sub>\ \ \ (P, C0, Main) \ (C, M, \pc\, Return) -(ek)\ (C, M, None, Return)" | CFG_Return: "\ C \ ClassMain P; (P, C0, Main) \ \(C, M, \pc\, Enter); instrs_of (PROG P) C M ! pc = instr.Return; ek = \(\s. s(Stack 0 := s (Stack (stkLength (P, C, M) pc - 1)))) \ \ (P, C0, Main) \ (C, M, \pc\, Enter) -(ek)\ (C, M, None, Return)" | CFG_Return_from_Method: "\ (P, C0, Main) \ \(C, M, None, Return); (P, C0, Main) \ (C', M', \pc'\, Normal) -(Q':(C', M', pc')\\<^bsub>(C,M)\<^esub>ps)\ (C, M, None, Enter); Q = (\(s, ret). ret = (C', M', pc')); stateUpdate = (\s s'. s'(Heap := s Heap, Exception := s Exception, Stack (stkLength (P, C', M') (Suc pc') - 1) := s (Stack 0)) ); ek = Q\\<^bsub>(C, M)\<^esub>stateUpdate \ \ (P, C0, Main) \ (C, M, None, Return) -(ek)\ (C', M', \pc'\, Return)" (* This takes veeeery long *) lemma JVMCFG_edge_det: "\ P \ n -(et)\ n'; P \ n -(et')\ n' \ \ et = et'" by (erule JVMCFG.cases) (erule JVMCFG.cases, (fastforce dest: sees_method_fun)+)+ lemma sourcenode_reachable: "P \ n -(ek)\ n' \ P \ \n" by (erule JVMCFG.cases, auto) lemma targetnode_reachable: assumes edge: "P \ n -(ek)\ n'" shows "P \ \n'" proof - from edge have "P \ \n" by -(drule sourcenode_reachable) with edge show ?thesis by -(rule JVMCFG_reachable.intros) qed lemmas JVMCFG_reachable_inducts = JVMCFG_reachable.inducts[split_format (complete)] lemma ClassMain_imp_MethodMain: "(P, C0, Main) \ (C', M', pc', nt') -ek\ (ClassMain P, M, pc, nt) \ M = MethodMain P" "(P, C0, Main) \ \(ClassMain P, M, pc, nt) \ M = MethodMain P" proof (induct P=="P" C0\"C0" Main\Main C' M' pc' nt' ek C''=="ClassMain P" M pc nt and P=="P" C0\"C0" Main\Main C'=="ClassMain P" M pc nt rule: JVMCFG_reachable_inducts) case CFG_Return_from_Method thus ?case by (fastforce elim: JVMCFG.cases) qed auto lemma ClassMain_no_Call_target [dest!]: "(P, C0, Main) \ (C, M, pc, nt) -Q:(C', M', pc')\\<^bsub>(D,M'')\<^esub>paramDefs\ (ClassMain P, M''', pc'', nt') \ False" and "(P, C0, Main) \ \(C, M, pc, nt) \ True" by (induct P C0 Main C M pc nt ek=="Q:(C', M', pc')\\<^bsub>(D,M'')\<^esub>paramDefs" C''=="ClassMain P" M''' pc'' nt' and P C0 Main C M pc nt rule: JVMCFG_reachable_inducts) auto lemma method_of_src_and_trg_exists: "\ (P, C0, Main) \ (C', M', pc', nt') -ek\ (C, M, pc, nt); C \ ClassMain P; C' \ ClassMain P \ \ (\Ts T mb. (PROG P) \ C sees M:Ts\T = mb in C) \ (\Ts T mb. (PROG P) \ C' sees M':Ts\T = mb in C')" and method_of_reachable_node_exists: "\ (P, C0, Main) \ \(C, M, pc, nt); C \ ClassMain P \ \ \Ts T mb. (PROG P) \ C sees M:Ts\T = mb in C" proof (induct rule: JVMCFG_reachable_inducts) case CFG_Invoke_Call thus ?case by (blast dest: sees_method_idemp) next case (reachable_step P C0 Main C M pc nt ek C' M' pc' nt') show ?case proof (cases "C = ClassMain P") case True with \(P, C0, Main) \ (C, M, pc, nt) -ek\ (C', M', pc', nt')\ \C' \ ClassMain P\ show ?thesis proof cases case Main_Call thus ?thesis by (blast dest: sees_method_idemp) qed auto next case False with reachable_step show ?thesis by simp qed qed simp_all lemma "\ (P, C0, Main) \ (C', M', pc', nt') -ek\ (C, M, pc, nt); C \ ClassMain P; C' \ ClassMain P \ \ (case pc of None \ True | \pc''\ \ (TYPING P) C M ! pc'' \ None \ pc'' < length (instrs_of (PROG P) C M)) \ (case pc' of None \ True | \pc''\ \ (TYPING P) C' M' ! pc'' \ None \ pc'' < length (instrs_of (PROG P) C' M'))" and instr_of_reachable_node_typable: "\ (P, C0, Main) \ \(C, M, pc, nt); C \ ClassMain P \ \ case pc of None \ True | \pc''\ \ (TYPING P) C M ! pc'' \ None \ pc'' < length (instrs_of (PROG P) C M)" proof (induct rule: JVMCFG_reachable_inducts) case (CFG_Load C P C0 Main M pc n ek) from \(P, C0, Main) \ \(C, M, \pc\, Enter)\ \C \ ClassMain P\ obtain Ts T mxs mxl\<^sub>0 "is" xt where "PROG P \ C sees M:Ts\T = (mxs, mxl\<^sub>0, is, xt) in C" and "instrs_of (PROG P) C M = is" by -(drule method_of_reachable_node_exists, auto) with CFG_Load show ?case by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ]) next case (CFG_Store C P C0 Main M pc n ek) from \(P, C0, Main) \ \(C, M, \pc\, Enter)\ \C \ ClassMain P\ obtain Ts T mxs mxl\<^sub>0 "is" xt where "PROG P \ C sees M:Ts\T = (mxs, mxl\<^sub>0, is, xt) in C" and "instrs_of (PROG P) C M = is" by -(drule method_of_reachable_node_exists, auto) with CFG_Store show ?case by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ]) next case (CFG_Push C P C0 Main M pc v ek) from \(P, C0, Main) \ \(C, M, \pc\, Enter)\ \C \ ClassMain P\ obtain Ts T mxs mxl\<^sub>0 "is" xt where "PROG P \ C sees M:Ts\T = (mxs, mxl\<^sub>0, is, xt) in C" and "instrs_of (PROG P) C M = is" by -(drule method_of_reachable_node_exists, auto) with CFG_Push show ?case by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ]) next case (CFG_Pop C P C0 Main M pc ek) from \(P, C0, Main) \ \(C, M, \pc\, Enter)\ \C \ ClassMain P\ obtain Ts T mxs mxl\<^sub>0 "is" xt where "PROG P \ C sees M:Ts\T = (mxs, mxl\<^sub>0, is, xt) in C" and "instrs_of (PROG P) C M = is" by -(drule method_of_reachable_node_exists, auto) with CFG_Pop show ?case by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ]) next case (CFG_IAdd C P C0 Main M pc ek) from \(P, C0, Main) \ \(C, M, \pc\, Enter)\ \C \ ClassMain P\ obtain Ts T mxs mxl\<^sub>0 "is" xt where "PROG P \ C sees M:Ts\T = (mxs, mxl\<^sub>0, is, xt) in C" and "instrs_of (PROG P) C M = is" by -(drule method_of_reachable_node_exists, auto) with CFG_IAdd show ?case by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ]) next case (CFG_Goto C P C0 Main M pc i) from \(P, C0, Main) \ \(C, M, \pc\, Enter)\ \C \ ClassMain P\ obtain Ts T mxs mxl\<^sub>0 "is" xt where "PROG P \ C sees M:Ts\T = (mxs, mxl\<^sub>0, is, xt) in C" and "instrs_of (PROG P) C M = is" by -(drule method_of_reachable_node_exists, auto) with CFG_Goto show ?case by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ]) next case (CFG_CmpEq C P C0 Main M pc ek) from \(P, C0, Main) \ \(C, M, \pc\, Enter)\ \C \ ClassMain P\ obtain Ts T mxs mxl\<^sub>0 "is" xt where "PROG P \ C sees M:Ts\T = (mxs, mxl\<^sub>0, is, xt) in C" and "instrs_of (PROG P) C M = is" by -(drule method_of_reachable_node_exists, auto) with CFG_CmpEq show ?case by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ]) next case (CFG_IfFalse_False C P C0 Main M pc i ek) from \(P, C0, Main) \ \(C, M, \pc\, Enter)\ \C \ ClassMain P\ obtain Ts T mxs mxl\<^sub>0 "is" xt where "PROG P \ C sees M:Ts\T = (mxs, mxl\<^sub>0, is, xt) in C" and "instrs_of (PROG P) C M = is" by -(drule method_of_reachable_node_exists, auto) with CFG_IfFalse_False show ?case by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ]) next case (CFG_IfFalse_True C P C0 Main M pc i ek) from \(P, C0, Main) \ \(C, M, \pc\, Enter)\ \C \ ClassMain P\ obtain Ts T mxs mxl\<^sub>0 "is" xt where "PROG P \ C sees M:Ts\T = (mxs, mxl\<^sub>0, is, xt) in C" and "instrs_of (PROG P) C M = is" by -(drule method_of_reachable_node_exists, auto) with CFG_IfFalse_True show ?case using [[simproc del: list_to_set_comprehension]] by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ]) next case (CFG_New_Update C P C0 Main M pc Cl ek) from \(P, C0, Main) \ \(C, M, \pc\, Normal)\ \C \ ClassMain P\ obtain Ts T mxs mxl\<^sub>0 "is" xt where "PROG P \ C sees M:Ts\T = (mxs, mxl\<^sub>0, is, xt) in C" and "instrs_of (PROG P) C M = is" by -(drule method_of_reachable_node_exists, auto) with CFG_New_Update show ?case by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ]) next case (CFG_New_Exceptional_handle C P C0 Main M pc pc' Cl ek) hence "TYPING P C M ! pc \ None" and "pc < length (instrs_of (PROG P) C M)" by simp_all moreover from \(P, C0, Main) \ \(C, M, \pc\, Exceptional \pc'\ Enter)\ \C \ ClassMain P\ obtain Ts T mxs mxl\<^sub>0 where "PROG P \ C sees M:Ts\T = (mxs, mxl\<^sub>0, instrs_of (PROG P) C M, ex_table_of (PROG P) C M) in C" by (fastforce dest: method_of_reachable_node_exists) with \pc < length (instrs_of (PROG P) C M)\ \instrs_of (PROG P) C M ! pc = New Cl\ have "PROG P,T,mxs,length (instrs_of (PROG P) C M),ex_table_of (PROG P) C M \ New Cl,pc :: TYPING P C M" by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ]) moreover from \(P, C0, Main) \ \(C, M, \pc\, Exceptional \pc'\ Enter)\ \C \ ClassMain P\ \instrs_of (PROG P) C M ! pc = New Cl\ obtain d' where "match_ex_table (PROG P) OutOfMemory pc (ex_table_of (PROG P) C M) = \(pc', d')\" by cases (fastforce elim: JVMCFG.cases) hence "\(f, t, D, h, d)\set (ex_table_of (PROG P) C M). matches_ex_entry (PROG P) OutOfMemory pc (f, t, D, h, d) \ h = pc' \ d = d'" by -(drule match_ex_table_SomeD) ultimately show ?case using \instrs_of (PROG P) C M ! pc = New Cl\ by (fastforce simp: relevant_entries_def is_relevant_entry_def matches_ex_entry_def) next case (CFG_Getfield_Update C P C0 Main M pc F Cl ek) from \(P, C0, Main) \ \(C, M, \pc\, Normal)\ \C \ ClassMain P\ obtain Ts T mxs mxl\<^sub>0 "is" xt where "PROG P \ C sees M:Ts\T = (mxs, mxl\<^sub>0, is, xt) in C" and "instrs_of (PROG P) C M = is" by -(drule method_of_reachable_node_exists, auto) with CFG_Getfield_Update show ?case by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ]) next case (CFG_Getfield_Exceptional_handle C P C0 Main M pc pc' F Cl ek) hence "TYPING P C M ! pc \ None" and "pc < length (instrs_of (PROG P) C M)" by simp_all moreover from \(P, C0, Main) \ \(C, M, \pc\, Exceptional \pc'\ Enter)\ \C \ ClassMain P\ obtain Ts T mxs mxl\<^sub>0 where "PROG P \ C sees M:Ts\T = (mxs, mxl\<^sub>0, instrs_of (PROG P) C M, ex_table_of (PROG P) C M) in C" by (fastforce dest: method_of_reachable_node_exists) with \pc < length (instrs_of (PROG P) C M)\ \instrs_of (PROG P) C M ! pc = Getfield F Cl\ have "PROG P,T,mxs,length (instrs_of (PROG P) C M),ex_table_of (PROG P) C M \ Getfield F Cl,pc :: TYPING P C M" by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ]) moreover from \(P, C0, Main) \ \(C, M, \pc\, Exceptional \pc'\ Enter)\ \C \ ClassMain P\ \instrs_of (PROG P) C M ! pc = Getfield F Cl\ obtain d' where "match_ex_table (PROG P) NullPointer pc (ex_table_of (PROG P) C M) = \(pc', d')\" by cases (fastforce elim: JVMCFG.cases) hence "\(f, t, D, h, d)\set (ex_table_of (PROG P) C M). matches_ex_entry (PROG P) NullPointer pc (f, t, D, h, d) \ h = pc' \ d = d'" by -(drule match_ex_table_SomeD) ultimately show ?case using \instrs_of (PROG P) C M ! pc = Getfield F Cl\ by (fastforce simp: relevant_entries_def is_relevant_entry_def matches_ex_entry_def) next case (CFG_Putfield_Update C P C0 Main M pc F Cl ek) from \(P, C0, Main) \ \(C, M, \pc\, Normal)\ \C \ ClassMain P\ obtain Ts T mxs mxl\<^sub>0 "is" xt where "PROG P \ C sees M:Ts\T = (mxs, mxl\<^sub>0, is, xt) in C" and "instrs_of (PROG P) C M = is" by -(drule method_of_reachable_node_exists, auto) with CFG_Putfield_Update show ?case by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ]) next case (CFG_Putfield_Exceptional_handle C P C0 Main M pc pc' F Cl ek) hence "TYPING P C M ! pc \ None" and "pc < length (instrs_of (PROG P) C M)" by simp_all moreover from \(P, C0, Main) \ \(C, M, \pc\, Exceptional \pc'\ Enter)\ \C \ ClassMain P\ obtain Ts T mxs mxl\<^sub>0 where "PROG P \ C sees M:Ts\T = (mxs, mxl\<^sub>0, instrs_of (PROG P) C M, ex_table_of (PROG P) C M) in C" by (fastforce dest: method_of_reachable_node_exists) with \pc < length (instrs_of (PROG P) C M)\ \instrs_of (PROG P) C M ! pc = Putfield F Cl\ have "PROG P,T,mxs,length (instrs_of (PROG P) C M),ex_table_of (PROG P) C M \ Putfield F Cl,pc :: TYPING P C M" by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ]) moreover from \(P, C0, Main) \ \(C, M, \pc\, Exceptional \pc'\ Enter)\ \C \ ClassMain P\ \instrs_of (PROG P) C M ! pc = Putfield F Cl\ obtain d' where "match_ex_table (PROG P) NullPointer pc (ex_table_of (PROG P) C M) = \(pc', d')\" by cases (fastforce elim: JVMCFG.cases) hence "\(f, t, D, h, d)\set (ex_table_of (PROG P) C M). matches_ex_entry (PROG P) NullPointer pc (f, t, D, h, d) \ h = pc' \ d = d'" by -(drule match_ex_table_SomeD) ultimately show ?case using \instrs_of (PROG P) C M ! pc = Putfield F Cl\ by (fastforce simp: relevant_entries_def is_relevant_entry_def matches_ex_entry_def) next case (CFG_Checkcast_Check_Normal C P C0 Main M pc Cl ek) from \(P, C0, Main) \ \(C, M, \pc\, Enter)\ \C \ ClassMain P\ obtain Ts T mxs mxl\<^sub>0 "is" xt where "PROG P \ C sees M:Ts\T = (mxs, mxl\<^sub>0, is, xt) in C" and "instrs_of (PROG P) C M = is" by -(drule method_of_reachable_node_exists, auto) with CFG_Checkcast_Check_Normal show ?case by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ]) next case (CFG_Checkcast_Exceptional_handle C P C0 Main M pc pc' Cl ek) hence "TYPING P C M ! pc \ None" and "pc < length (instrs_of (PROG P) C M)" by simp_all moreover from \(P, C0, Main) \ \(C, M, \pc\, Exceptional \pc'\ Enter)\ \C \ ClassMain P\ obtain Ts T mxs mxl\<^sub>0 where "PROG P \ C sees M:Ts\T = (mxs, mxl\<^sub>0, instrs_of (PROG P) C M, ex_table_of (PROG P) C M) in C" by (fastforce dest: method_of_reachable_node_exists) with \pc < length (instrs_of (PROG P) C M)\ \instrs_of (PROG P) C M ! pc = Checkcast Cl\ have "PROG P,T,mxs,length (instrs_of (PROG P) C M),ex_table_of (PROG P) C M \ Checkcast Cl,pc :: TYPING P C M" by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ]) moreover from \(P, C0, Main) \ \(C, M, \pc\, Exceptional \pc'\ Enter)\ \C \ ClassMain P\ \instrs_of (PROG P) C M ! pc = Checkcast Cl\ obtain d' where "match_ex_table (PROG P) ClassCast pc (ex_table_of (PROG P) C M) = \(pc', d')\" by cases (fastforce elim: JVMCFG.cases) hence "\(f, t, D, h, d)\set (ex_table_of (PROG P) C M). matches_ex_entry (PROG P) ClassCast pc (f, t, D, h, d) \ h = pc' \ d = d'" by -(drule match_ex_table_SomeD) ultimately show ?case using \instrs_of (PROG P) C M ! pc = Checkcast Cl\ by (fastforce simp: relevant_entries_def is_relevant_entry_def matches_ex_entry_def) next case (CFG_Throw_handle C P C0 Main M pc pc' ek) hence "TYPING P C M ! pc \ None" and "pc < length (instrs_of (PROG P) C M)" by simp_all moreover from \(P, C0, Main) \ \(C, M, \pc\, Exceptional \pc'\ Enter)\ \C \ ClassMain P\ obtain Ts T mxs mxl\<^sub>0 where "PROG P \ C sees M:Ts\T = (mxs, mxl\<^sub>0, instrs_of (PROG P) C M, ex_table_of (PROG P) C M) in C" by (fastforce dest: method_of_reachable_node_exists) with \pc < length (instrs_of (PROG P) C M)\ \instrs_of (PROG P) C M ! pc = Throw\ have "PROG P,T,mxs,length (instrs_of (PROG P) C M),ex_table_of (PROG P) C M \ Throw,pc :: TYPING P C M" by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ]) moreover from \(P, C0, Main) \ \(C, M, \pc\, Exceptional \pc'\ Enter)\ \C \ ClassMain P\ \instrs_of (PROG P) C M ! pc = Throw\ obtain d' Exc where "match_ex_table (PROG P) Exc pc (ex_table_of (PROG P) C M) = \(pc', d')\" by cases (fastforce elim: JVMCFG.cases) hence "\(f, t, D, h, d)\set (ex_table_of (PROG P) C M). matches_ex_entry (PROG P) Exc pc (f, t, D, h, d) \ h = pc' \ d = d'" by -(drule match_ex_table_SomeD) ultimately show ?case using \instrs_of (PROG P) C M ! pc = Throw\ by (fastforce simp: relevant_entries_def is_relevant_entry_def matches_ex_entry_def) next case (CFG_Invoke_NP_handle C P C0 Main M pc pc' M' n ek) hence "TYPING P C M ! pc \ None" and "pc < length (instrs_of (PROG P) C M)" by simp_all moreover from \(P, C0, Main) \ \(C, M, \pc\, Exceptional \pc'\ Enter)\ \C \ ClassMain P\ obtain Ts T mxs mxl\<^sub>0 where "PROG P \ C sees M:Ts\T = (mxs, mxl\<^sub>0, instrs_of (PROG P) C M, ex_table_of (PROG P) C M) in C" by (fastforce dest: method_of_reachable_node_exists) with \pc < length (instrs_of (PROG P) C M)\ \instrs_of (PROG P) C M ! pc = Invoke M' n\ have "PROG P,T,mxs,length (instrs_of (PROG P) C M),ex_table_of (PROG P) C M \ Invoke M' n,pc :: TYPING P C M" by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ]) moreover from \(P, C0, Main) \ \(C, M, \pc\, Exceptional \pc'\ Enter)\ \C \ ClassMain P\ \instrs_of (PROG P) C M ! pc = Invoke M' n\ obtain d' where "match_ex_table (PROG P) NullPointer pc (ex_table_of (PROG P) C M) = \(pc', d')\" by cases (fastforce elim: JVMCFG.cases) hence "\(f, t, D, h, d)\set (ex_table_of (PROG P) C M). matches_ex_entry (PROG P) NullPointer pc (f, t, D, h, d) \ h = pc' \ d = d'" by -(drule match_ex_table_SomeD) ultimately show ?case using \instrs_of (PROG P) C M ! pc = Invoke M' n\ by (fastforce simp: relevant_entries_def is_relevant_entry_def matches_ex_entry_def) next case (CFG_Invoke_Return_Exceptional_handle C P C0 Main M pc pc' M' n ek) hence "TYPING P C M ! pc \ None" and "pc < length (instrs_of (PROG P) C M)" by simp_all moreover from \(P, C0, Main) \ \(C, M, \pc\, Exceptional \pc'\ Return)\ \C \ ClassMain P\ obtain Ts T mxs mxl\<^sub>0 where "PROG P \ C sees M:Ts\T = (mxs, mxl\<^sub>0, instrs_of (PROG P) C M, ex_table_of (PROG P) C M) in C" by (fastforce dest: method_of_reachable_node_exists) with \pc < length (instrs_of (PROG P) C M)\ \instrs_of (PROG P) C M ! pc = Invoke M' n\ have "PROG P,T,mxs,length (instrs_of (PROG P) C M),ex_table_of (PROG P) C M \ Invoke M' n,pc :: TYPING P C M" by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ]) moreover from \(P, C0, Main) \ \(C, M, \pc\, Exceptional \pc'\ Return)\ \C \ ClassMain P\ \instrs_of (PROG P) C M ! pc = Invoke M' n\ obtain d' Exc where "match_ex_table (PROG P) Exc pc (ex_table_of (PROG P) C M) = \(pc', d')\" by cases (fastforce elim: JVMCFG.cases) hence "\(f, t, D, h, d)\set (ex_table_of (PROG P) C M). matches_ex_entry (PROG P) Exc pc (f, t, D, h, d) \ h = pc' \ d = d'" by -(drule match_ex_table_SomeD) ultimately show ?case using \instrs_of (PROG P) C M ! pc = Invoke M' n\ by (fastforce simp: relevant_entries_def is_relevant_entry_def matches_ex_entry_def) next case (CFG_Invoke_Return_Check_Normal C P C0 Main M pc M' n ST LT ek) from \(P, C0, Main) \ \(C, M, \pc\, Return)\ \C \ ClassMain P\ obtain Ts T mxs mxl\<^sub>0 "is" xt where "PROG P \ C sees M:Ts\T = (mxs, mxl\<^sub>0, is, xt) in C" and "instrs_of (PROG P) C M = is" by -(drule method_of_reachable_node_exists, auto) with CFG_Invoke_Return_Check_Normal show ?case by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ]) next case (Method_LTrue P C0 Main C M) from \(P, C0, Main) \ \(C, M, None, Enter)\ \C \ ClassMain P\ obtain Ts T mxs mxl\<^sub>0 "is" xt where "PROG P \ C sees M:Ts\T = (mxs, mxl\<^sub>0, is, xt) in C" and "instrs_of (PROG P) C M = is" by -(drule method_of_reachable_node_exists, auto) with Method_LTrue show ?case by (fastforce dest!: wt_jvm_prog_impl_wt_start [OF wf_jvmprog_is_wf_typ] simp: wt_start_def) next case (reachable_step P C0 Main C M opc nt ek C' M' opc' nt') thus ?case by (cases "C = ClassMain P") (fastforce elim: JVMCFG.cases, simp) qed simp_all lemma reachable_node_impl_wt_instr: assumes "(P, C0, Main) \ \(C, M, \pc\, nt)" and "C \ ClassMain P" shows "\T mxs mpc xt. PROG P,T,mxs,mpc,xt \ (instrs_of (PROG P) C M ! pc),pc :: TYPING P C M" proof - from \C \ ClassMain P\ \(P, C0, Main) \ \(C, M, \pc\, nt)\ method_of_reachable_node_exists [of P C0 Main C M "\pc\" nt] instr_of_reachable_node_typable [of P C0 Main C M "\pc\" nt] obtain Ts T mxs mxl\<^sub>0 "is" xt where "PROG P \ C sees M:Ts\T = (mxs, mxl\<^sub>0, is, xt) in C" and "TYPING P C M ! pc \ None" and "pc < length (instrs_of (PROG P) C M)" by fastforce+ with wf_jvmprog_is_wf_typ [of P] have "PROG P,T,mxs,length is,xt \ instrs_of (PROG P) C M ! pc,pc :: TYPING P C M" by (fastforce dest!: wt_jvm_prog_impl_wt_instr) thus ?thesis by blast qed lemma "\ (P, C0, Main) \ (C, M, pc, nt) -ek\ (C', M', pc', nt'); C \ ClassMain P \ C' \ ClassMain P \ \ \T mb D. PROG P \ C0 sees Main:[]\T = mb in D" and reachable_node_impl_Main_ex: "\ (P, C0, Main) \ \(C, M, pc, nt); C \ ClassMain P\ \ \T mb D. PROG P \ C0 sees Main:[]\T = mb in D" by (induct rule: JVMCFG_reachable_inducts) fastforce+ end diff --git a/thys/Slicing/JinjaVM/JVMCFG.thy b/thys/Slicing/JinjaVM/JVMCFG.thy --- a/thys/Slicing/JinjaVM/JVMCFG.thy +++ b/thys/Slicing/JinjaVM/JVMCFG.thy @@ -1,811 +1,811 @@ (* This work was done by Denis Lohner (denis.lohner@kit.edu). *) chapter \A Control Flow Graph for Jinja Byte Code\ section \Formalizing the CFG\ theory JVMCFG imports "../Basic/BasicDefs" Jinja.BVExample begin declare lesub_list_impl_same_size [simp del] -declare listE_length [simp del] +declare nlistsE_length [simp del] subsection \Type definitions\ subsubsection \Wellformed Programs\ definition "wf_jvmprog = {(P, Phi). wf_jvm_prog\<^bsub>Phi\<^esub> P}" typedef wf_jvmprog = wf_jvmprog proof show "(E, Phi) \ wf_jvmprog" unfolding wf_jvmprog_def by (auto intro: wf_prog) qed hide_const Phi E abbreviation rep_jvmprog_jvm_prog :: "wf_jvmprog \ jvm_prog" ("_\<^bsub>wf\<^esub>") where "P\<^bsub>wf\<^esub> \ fst(Rep_wf_jvmprog(P))" abbreviation rep_jvmprog_phi :: "wf_jvmprog \ ty\<^sub>P" ("_\<^bsub>\\<^esub>") where "P\<^bsub>\\<^esub> \ snd(Rep_wf_jvmprog(P))" lemma wf_jvmprog_is_wf: "wf_jvm_prog\<^bsub>P\<^bsub>\\<^esub>\<^esub> (P\<^bsub>wf\<^esub>)" using Rep_wf_jvmprog [of P] by (auto simp: wf_jvmprog_def split_beta) subsubsection \Basic Types\ text \ We consider a program to be a well-formed Jinja program, together with a given base class and a main method \ type_synonym jvmprog = "wf_jvmprog \ cname \ mname" type_synonym callstack = "(cname \ mname \ pc) list" text \ The state is modeled as $\textrm{heap} \times \textrm{stack-variables} \times \textrm{local-variables}$ stack and local variables are modeled as pairs of natural numbers. The first number gives the position in the call stack (i.e. the method in which the variable is used), the second the position in the method's stack or array of local variables resp. The stack variables are numbered from bottom up (which is the reverse order of the array for the stack in Jinja's state representation), whereas local variables are identified by their position in the array of local variables of Jinja's state representation. \ type_synonym state = "heap \ ((nat \ nat) \ val) \ ((nat \ nat) \ val)" abbreviation heap_of :: "state \ heap" where "heap_of s \ fst(s)" abbreviation stk_of :: "state \ ((nat \ nat) \ val)" where "stk_of s \ fst(snd(s))" abbreviation loc_of :: "state \ ((nat \ nat) \ val)" where "loc_of s \ snd(snd(s))" subsection \Basic Definitions\ subsubsection \State update (instruction execution)\ text \ This function models instruction execution for our state representation. Additional parameters are the call depth of the current program point, the stack length of the current program point, the length of the stack in the underlying call frame (needed for {\sc Return}), and (for {\sc Invoke}) the length of the array of local variables of the invoked method. Exception handling is not covered by this function. \ fun exec_instr :: "instr \ wf_jvmprog \ state \ nat \ nat \ nat \ nat \ state" where exec_instr_Load: "exec_instr (Load n) P s calldepth stk_length rs ill = (let (h,stk,loc) = s in (h, stk((calldepth,stk_length):=loc(calldepth,n)), loc))" | exec_instr_Store: "exec_instr (Store n) P s calldepth stk_length rs ill = (let (h,stk,loc) = s in (h, stk, loc((calldepth,n):=stk(calldepth,stk_length - 1))))" | exec_instr_Push: "exec_instr (Push v) P s calldepth stk_length rs ill = (let (h,stk,loc) = s in (h, stk((calldepth,stk_length):=v), loc))" | exec_instr_New: "exec_instr (New C) P s calldepth stk_length rs ill = (let (h,stk,loc) = s; a = the(new_Addr h) in (h(a \ (blank (P\<^bsub>wf\<^esub>) C)), stk((calldepth,stk_length):=Addr a), loc))" | exec_instr_Getfield: "exec_instr (Getfield F C) P s calldepth stk_length rs ill = (let (h,stk,loc) = s; a = the_Addr (stk (calldepth,stk_length - 1)); (D,fs) = the(h a) in (h, stk((calldepth,stk_length - 1) := the(fs(F,C))), loc))" | exec_instr_Putfield: "exec_instr (Putfield F C) P s calldepth stk_length rs ill = (let (h,stk,loc) = s; v = stk (calldepth,stk_length - 1); a = the_Addr (stk (calldepth,stk_length - 2)); (D,fs) = the(h a) in (h(a \ (D,fs((F,C) \ v))), stk, loc))" | exec_instr_Checkcast: "exec_instr (Checkcast C) P s calldepth stk_length rs ill = s" | exec_instr_Pop: "exec_instr (Pop) P s calldepth stk_length rs ill = s" | exec_instr_IAdd: "exec_instr (IAdd) P s calldepth stk_length rs ill = (let (h,stk,loc) = s; i\<^sub>1 = the_Intg (stk (calldepth, stk_length - 1)); i\<^sub>2 = the_Intg (stk (calldepth, stk_length - 2)) in (h, stk((calldepth, stk_length - 2) := Intg (i\<^sub>1 + i\<^sub>2)), loc))" | exec_instr_IfFalse: "exec_instr (IfFalse b) P s calldepth stk_length rs ill = s" | exec_instr_CmpEq: "exec_instr (CmpEq) P s calldepth stk_length rs ill = (let (h,stk,loc) = s; v\<^sub>1 = stk (calldepth, stk_length - 1); v\<^sub>2 = stk (calldepth, stk_length - 2) in (h, stk((calldepth, stk_length - 2) := Bool (v\<^sub>1 = v\<^sub>2)), loc))" | exec_instr_Goto: "exec_instr (Goto i) P s calldepth stk_length rs ill = s" | exec_instr_Throw: "exec_instr (Throw) P s calldepth stk_length rs ill = s" | exec_instr_Invoke: "exec_instr (Invoke M n) P s calldepth stk_length rs invoke_loc_length = (let (h,stk,loc) = s; loc' = (\(a,b). if (a \ Suc calldepth \ b \ invoke_loc_length) then loc(a,b) else (if (b \ n) then stk(calldepth, stk_length - (Suc n - b)) else arbitrary)) in (h,stk,loc'))" | exec_instr_Return: "exec_instr (Return) P s calldepth stk_length ret_stk_length ill = (if (calldepth = 0) then s else (let (h,stk,loc) = s; v = stk(calldepth, stk_length - 1) in (h,stk((calldepth - 1, ret_stk_length - 1) := v),loc)) )" subsubsection \length of stack and local variables\ text \The following terms extract the stack length at a given program point from the well-typing of the given program\ abbreviation stkLength :: "wf_jvmprog \ cname \ mname \ pc \ nat" where "stkLength P C M pc \ length (fst(the(((P\<^bsub>\\<^esub>) C M)!pc)))" abbreviation locLength :: "wf_jvmprog \ cname \ mname \ pc \ nat" where "locLength P C M pc \ length (snd(the(((P\<^bsub>\\<^esub>) C M)!pc)))" subsubsection \Conversion functions\ text \ This function takes a natural number n and a function f with domain \nat\ and creates the array [f 0, f 1, f 2, ..., f (n - 1)]. This is used for extracting the array of local variables \ (* fun locs :: "nat \ (nat \ 'a) \ 'a list" where "locs 0 loc = []" | "locs (Suc n) loc = (locs n loc)@[loc n]" *) abbreviation locs :: "nat \ (nat \ 'a) \ 'a list" where "locs n loc \ map loc [0.. This function takes a natural number n and a function f with domain \nat\ and creates the array [f (n - 1), ..., f 1, f 0]. This is used for extracting the stack as a list \ (* fun stks :: "nat \ (nat \ 'a) \ 'a list" where "stks 0 stk = []" | "stks (Suc n) stk = (stk n)#(stks n stk)" *) abbreviation stks :: "nat \ (nat \ 'a) \ 'a list" where "stks n stk \ map stk (rev [0.. This function creates a list of the arrays for local variables from the given state corresponding to the given callstack \ fun locss :: "wf_jvmprog \ callstack \ ((nat \ nat) \ 'a) \ 'a list list" where "locss P [] loc = []" | "locss P ((C,M,pc)#cs) loc = (locs (locLength P C M pc) (\a. loc (length cs, a)))#(locss P cs loc)" text \ This function creates a list of the (methods') stacks from the given state corresponding to the given callstack \ fun stkss :: "wf_jvmprog \ callstack \ ((nat \ nat) \ 'a) \ 'a list list" where "stkss P [] stk = []" | "stkss P ((C,M,pc)#cs) stk = (stks (stkLength P C M pc) (\a. stk (length cs, a)))#(stkss P cs stk)" text \Given a callstack and a state, this abbreviation converts the state to Jinja's state representation \ abbreviation state_to_jvm_state :: "wf_jvmprog \ callstack \ state \ jvm_state" where "state_to_jvm_state P cs s \ (None, heap_of s, zip (stkss P cs (stk_of s)) (zip (locss P cs (loc_of s)) cs))" text \This function extracts the call stack from a given frame stack (as it is given by Jinja's state representation) \ definition framestack_to_callstack :: "frame list \ callstack" where "framestack_to_callstack frs \ map snd (map snd frs)" subsubsection \State Conformance\ text \Now we lift byte code verifier conformance to our state representation\ definition bv_conform :: "wf_jvmprog \ callstack \ state \ bool" ("_,_ \\<^bsub>BV\<^esub> _ \") where "P,cs \\<^bsub>BV\<^esub> s \ \ correct_state (P\<^bsub>wf\<^esub>) (P\<^bsub>\\<^esub>) (state_to_jvm_state P cs s)" subsubsection \Statically determine catch-block\ text \This function is equivalent to Jinja's \find_handler\ function\ fun find_handler_for :: "wf_jvmprog \ cname \ callstack \ callstack" where "find_handler_for P C [] = []" | "find_handler_for P C (c#cs) = (let (C',M',pc') = c in (case match_ex_table (P\<^bsub>wf\<^esub>) C pc' (ex_table_of (P\<^bsub>wf\<^esub>) C' M') of None \ find_handler_for P C cs | Some pc_d \ (C', M', fst pc_d)#cs))" subsection \Simplification lemmas\ lemma find_handler_decr [simp]: "find_handler_for P Exc cs \ c#cs" proof assume "find_handler_for P Exc cs = c#cs" hence "length cs < length (find_handler_for P Exc cs)" by simp thus False by (induct cs, auto) qed (* lemma locs_length [simp]: "length (locs n loc) = n" by (induct n) auto lemma stks_length [simp]: "length (stks n stk) = n" by (induct n) auto *) lemma stkss_length [simp]: "length (stkss P cs stk) = length cs" by (induct cs) auto lemma locss_length [simp]: "length (locss P cs loc) = length cs" by (induct cs) auto (* lemma nth_stks: "b < n \ stks n stk ! b = stk(n - Suc b)" by (auto simp: rev_nth) proof (induct n arbitrary: b) case (0 b) thus ?case by simp next case (Suc n b) thus ?case by (auto simp: nth_Cons' less_Suc_eq) qed *) lemma nth_stkss: "\ a < length cs; b < length (stkss P cs stk ! (length cs - Suc a)) \ \ stkss P cs stk ! (length cs - Suc a) ! (length (stkss P cs stk ! (length cs - Suc a)) - Suc b) = stk (a,b)" proof (induct cs) case Nil thus ?case by (simp add: nth_Cons') next case (Cons aa cs) thus ?case by (cases aa, auto simp add: nth_Cons' rev_nth less_Suc_eq) qed (* lemma nth_locs: "b < n \ locs n loc ! b = loc b" proof (induct n) case 0 thus ?case by simp next case (Suc n) thus ?case by (auto simp: nth_append less_Suc_eq) qed *) lemma nth_locss: "\ a < length cs; b < length (locss P cs loc ! (length cs - Suc a)) \ \ locss P cs loc ! (length cs - Suc a) ! b = loc (a,b)" proof (induct cs) case Nil thus ?case by (simp add: nth_Cons') next case (Cons aa cs) thus ?case by (cases aa, auto simp: nth_Cons' (* nth_locs *) less_Suc_eq) qed lemma hd_stks [simp]: "n \ 0 \ hd (stks n stk) = stk(n - 1)" by (cases n, simp_all) lemma hd_tl_stks: "n > 1 \ hd (tl (stks n stk)) = stk(n - 2)" by (cases n, auto) (* lemma stks_purge: "d \ b \ stks b (stk(d := e)) = stks b stk" by (induct b, auto) lemma stks_purge': "d \ b \ stks b (\x. if x = d then e else stk x) = stks b stk" by (fold fun_upd_def, simp only: stks_purge) *) lemma stkss_purge: "length cs \ a \ stkss P cs (stk((a,b) := c)) = stkss P cs stk" by (induct cs, auto (* simp: stks_purge *)) lemma stkss_purge': "length cs \ a \ stkss P cs (\s. if s = (a, b) then c else stk s) = stkss P cs stk" by (fold fun_upd_def, simp only: stkss_purge) (* lemma locs_purge: "d \ b \ locs b (loc(d := e)) = locs b loc" by (induct b, auto) lemma locs_purge': "d \ b \ locs b (\b. if b = d then e else loc b) = locs b loc" by (fold fun_upd_def, simp only: locs_purge) *) lemma locss_purge: "length cs \ a \ locss P cs (loc((a,b) := c)) = locss P cs loc" by (induct cs, auto (*simp: locs_purge *)) lemma locss_purge': "length cs \ a \ locss P cs (\s. if s = (a, b) then c else loc s) = locss P cs loc" by (fold fun_upd_def, simp only: locss_purge) lemma locs_pullout [simp]: "locs b (loc(n := e)) = (locs b loc) [n := e]" proof (induct b) case 0 thus ?case by simp next case (Suc b) thus ?case by (cases "n - b", auto simp: list_update_append not_less_eq less_Suc_eq) qed lemma locs_pullout' [simp]: "locs b (\a. if a = n then e else loc (c, a)) = (locs b (\a. loc (c, a))) [n := e]" by (fold fun_upd_def) simp lemma stks_pullout: "n < b \ stks b (stk(n := e)) = (stks b stk) [b - Suc n := e]" proof (induct b) case 0 thus ?case by simp next case (Suc b) thus ?case proof (cases "b = n") case True with Suc show ?thesis by auto (* by (auto simp: stks_purge') *) next case False with Suc show ?thesis by (cases "b - n") (auto intro!: nth_equalityI simp: nth_list_update) qed qed lemma nth_tl : "xs \ [] \ tl xs ! n = xs ! (Suc n)" by (cases xs, simp_all) lemma f2c_Nil [simp]: "framestack_to_callstack [] = []" by (simp add: framestack_to_callstack_def) lemma f2c_Cons [simp]: "framestack_to_callstack ((stk,loc,C,M,pc)#frs) = (C,M,pc)#(framestack_to_callstack frs)" by (simp add: framestack_to_callstack_def) lemma f2c_length [simp]: "length (framestack_to_callstack frs) = length frs" by (simp add: framestack_to_callstack_def) lemma f2c_s2jvm_id [simp]: "framestack_to_callstack (snd(snd(state_to_jvm_state P cs s))) = cs" by (cases s, simp add: framestack_to_callstack_def) lemma f2c_s2jvm_id' [simp]: "framestack_to_callstack (zip (stkss P cs stk) (zip (locss P cs loc) cs)) = cs" by (simp add: framestack_to_callstack_def) lemma f2c_append [simp]: "framestack_to_callstack (frs @ frs') = (framestack_to_callstack frs) @ (framestack_to_callstack frs')" by (simp add: framestack_to_callstack_def) subsection \CFG construction\ subsection \Datatypes\ text \Nodes are labeled with a callstack and an optional tuple (consisting of a callstack and a flag). The first callstack determines the current program point (i.e. the next statement to execute). If the second parameter is not None, we are at an intermediate state, where the target of the instruction is determined (the second callstack) and the flag is set to whether an exception is thrown or not. \ datatype j_node = Entry ("'('_Entry'_')") | Node "callstack" "(callstack \ bool) option" ("'('_ _,_ '_')") text \The empty callstack indicates the exit node\ abbreviation j_node_Exit :: "j_node" ("'('_Exit'_')") where "j_node_Exit \ (_ [],None _)" text \An edge is a triple, consisting of two nodes and the edge kind\ type_synonym j_edge = "(j_node \ state edge_kind \ j_node)" subsection \CFG\ text \ The CFG is constructed by a case analysis on the instructions and their different behavior in different states. E.g. the exceptional behavior of {\sc New}, if there is no more space in the heap, vs. the normal behavior. Note: The set of edges defined by this predicate is a first approximation to the real set of edges in the CFG. We later (theory JVMInterpretation) add some well-formedness requirements to the nodes. \ inductive JVM_CFG :: "jvmprog \ j_node \ state edge_kind \ j_node \ bool" ("_ \ _ -_\ _") where JCFG_EntryExit: "prog \ (_Entry_) -(\s. False)\<^sub>\\ (_Exit_)" | JCFG_EntryStart: "prog = (P, C0, Main) \ prog \ (_Entry_) -(\s. True)\<^sub>\\ (_ [(C0, Main, 0)],None _)" | JCFG_ReturnExit: "\ prog = (P,C0,Main); (instrs_of (P\<^bsub>wf\<^esub>) C M) ! pc = Return \ \ prog \ (_ [(C, M, pc)],None _) -\id\ (_Exit_)" | JCFG_Straight_NoExc: "\ prog = (P, C0, Main); instrs_of (P\<^bsub>wf\<^esub>) C M ! pc \ {Load idx, Store idx, Push val, Pop, IAdd, CmpEq}; ek = \(\s. exec_instr ((instrs_of (P\<^bsub>wf\<^esub>) C M) ! pc) P s (length cs) (stkLength P C M pc) arbitrary arbitrary) \ \ prog \ (_ (C, M, pc)#cs,None _) -ek\ (_ (C, M, Suc pc)#cs,None _)" | JCFG_New_Normal_Pred: "\ prog = (P, C0, Main); (instrs_of (P\<^bsub>wf\<^esub>) C M) ! pc = (New Cl); ek = (\(h,stk,loc). new_Addr h \ None)\<^sub>\\ \ prog \ (_ (C, M, pc)#cs,None _) -ek\ (_ (C, M, pc)#cs,\((C, M, Suc pc)#cs,False)\ _)" | JCFG_New_Normal_Update: "\ prog = (P, C0, Main); (instrs_of (P\<^bsub>wf\<^esub>) C M) ! pc = (New Cl); ek = \(\s. exec_instr (New Cl) P s (length cs) (stkLength P C M pc) arbitrary arbitrary) \ \ prog \ (_ (C, M, pc)#cs,\((C, M, Suc pc)#cs, False)\ _) -ek\ (_ (C, M, Suc pc)#cs,None _)" | JCFG_New_Exc_Pred: "\ prog = (P, C0, Main); (instrs_of (P\<^bsub>wf\<^esub>) C M) ! pc = (New Cl); find_handler_for P OutOfMemory ((C, M, pc)#cs) = cs'; ek = (\(h,stk,loc). new_Addr h = None)\<^sub>\ \ \ prog \ (_ (C, M, pc)#cs,None _) -ek\ (_ (C, M, pc)#cs,\(cs',True)\ _)" | JCFG_New_Exc_Update: "\ prog = (P, C0, Main); (instrs_of (P\<^bsub>wf\<^esub>) C M) ! pc = (New Cl); find_handler_for P OutOfMemory ((C, M, pc)#cs) = (C', M', pc')#cs'; ek = \(\(h,stk,loc). (h, stk((length cs',(stkLength P C' M' pc') - 1) := Addr (addr_of_sys_xcpt OutOfMemory)), loc) ) \ \ prog \ (_ (C, M, pc)#cs,\((C', M', pc')#cs', True)\ _) -ek\ (_ (C', M', pc')#cs',None _)" | JCFG_New_Exc_Exit: "\ prog = (P, C0, Main); (instrs_of (P\<^bsub>wf\<^esub>) C M) ! pc = (New Cl); find_handler_for P OutOfMemory ((C, M, pc)#cs) = [] \ \ prog \ (_ (C, M, pc)#cs,\([], True)\ _) -\id\ (_Exit_)" | JCFG_Getfield_Normal_Pred: "\ prog = (P, C0, Main); (instrs_of (P\<^bsub>wf\<^esub>) C M) ! pc = (Getfield Fd Cl); ek = (\(h,stk,loc). stk(length cs, stkLength P C M pc - 1) \ Null)\<^sub>\ \ \ prog \ (_ (C, M, pc)#cs,None _) -ek\ (_ (C, M, pc)#cs,\((C, M, Suc pc)#cs, False)\ _)" | JCFG_Getfield_Normal_Update: "\ prog = (P, C0, Main); (instrs_of (P\<^bsub>wf\<^esub>) C M) ! pc = (Getfield Fd Cl); ek = \(\s. exec_instr (Getfield Fd Cl) P s (length cs) (stkLength P C M pc) arbitrary arbitrary) \ \ prog \ (_ (C, M, pc)#cs,\((C, M, Suc pc)#cs, False)\ _) -ek\ (_ (C, M, Suc pc)#cs,None _)" | JCFG_Getfield_Exc_Pred: "\ prog = (P, C0, Main); (instrs_of (P\<^bsub>wf\<^esub>) C M) ! pc = (Getfield Fd Cl); find_handler_for P NullPointer ((C, M, pc)#cs) = cs'; ek = (\(h,stk,loc). stk(length cs, stkLength P C M pc - 1) = Null)\<^sub>\ \ \ prog \ (_ (C, M, pc)#cs,None _) -ek\ (_ (C, M, pc)#cs,\(cs', True)\ _)" | JCFG_Getfield_Exc_Update: "\ prog = (P, C0, Main); (instrs_of (P\<^bsub>wf\<^esub>) C M) ! pc = (Getfield Fd Cl); find_handler_for P NullPointer ((C, M, pc)#cs) = (C', M', pc')#cs'; ek = \(\(h,stk,loc). (h, stk((length cs',(stkLength P C' M' pc') - 1) := Addr (addr_of_sys_xcpt NullPointer)), loc) ) \ \ prog \ (_ (C, M, pc)#cs,\((C', M', pc')#cs', True)\ _) -ek\ (_ (C', M', pc')#cs',None _)" | JCFG_Getfield_Exc_Exit: "\ prog = (P, C0, Main); (instrs_of (P\<^bsub>wf\<^esub>) C M) ! pc = (Getfield Fd Cl); find_handler_for P NullPointer ((C, M, pc)#cs) = [] \ \ prog \ (_ (C, M, pc)#cs,\([], True)\ _) -\id\ (_Exit_)" | JCFG_Putfield_Normal_Pred: "\ prog = (P, C0, Main); (instrs_of (P\<^bsub>wf\<^esub>) C M) ! pc = (Putfield Fd Cl); ek = (\(h,stk,loc). stk(length cs, stkLength P C M pc - 2) \ Null)\<^sub>\ \ \ prog \ (_ (C, M, pc)#cs,None _) -ek\ (_ (C, M, pc)#cs,\((C, M, Suc pc)#cs, False)\ _)" | JCFG_Putfield_Normal_Update: "\ prog = (P, C0, Main); (instrs_of (P\<^bsub>wf\<^esub>) C M) ! pc = (Putfield Fd Cl); ek = \(\s. exec_instr (Putfield Fd Cl) P s (length cs) (stkLength P C M pc) arbitrary arbitrary) \ \ prog \ (_ (C, M, pc)#cs,\((C, M, Suc pc)#cs, False)\ _) -ek\ (_ (C, M, Suc pc)#cs,None _)" | JCFG_Putfield_Exc_Pred: "\ prog = (P, C0, Main); (instrs_of (P\<^bsub>wf\<^esub>) C M) ! pc = (Putfield Fd Cl); find_handler_for P NullPointer ((C, M, pc)#cs) = cs'; ek = (\(h,stk,loc). stk(length cs, stkLength P C M pc - 2) = Null)\<^sub>\ \ \ prog \ (_ (C, M, pc)#cs,None _) -ek\ (_ (C, M, pc)#cs,\(cs', True)\ _)" | JCFG_Putfield_Exc_Update: "\ prog = (P, C0, Main); (instrs_of (P\<^bsub>wf\<^esub>) C M) ! pc = (Putfield Fd Cl); find_handler_for P NullPointer ((C, M, pc)#cs) = (C', M', pc')#cs'; ek = \(\(h,stk,loc). (h, stk((length cs',(stkLength P C' M' pc') - 1) := Addr (addr_of_sys_xcpt NullPointer)), loc) ) \ \ prog \ (_ (C, M, pc)#cs,\((C', M', pc')#cs', True)\ _) -ek\ (_ (C', M', pc')#cs',None _)" | JCFG_Putfield_Exc_Exit: "\ prog = (P, C0, Main); (instrs_of (P\<^bsub>wf\<^esub>) C M) ! pc = (Putfield Fd Cl); find_handler_for P NullPointer ((C, M, pc)#cs) = [] \ \ prog \ (_ (C, M, pc)#cs,\([], True)\ _) -\id\ (_Exit_)" | JCFG_Checkcast_Normal_Pred: "\ prog = (P, C0, Main); (instrs_of (P\<^bsub>wf\<^esub>) C M) ! pc = (Checkcast Cl); ek = (\(h,stk,loc). cast_ok (P\<^bsub>wf\<^esub>) Cl h (stk(length cs, stkLength P C M pc - Suc 0)))\<^sub>\ \ \ prog \ (_ (C, M, pc)#cs,None _) -ek\ (_ (C, M, Suc pc)#cs,None _)" | JCFG_Checkcast_Exc_Pred: "\ prog = (P, C0, Main); (instrs_of (P\<^bsub>wf\<^esub>) C M) ! pc = (Checkcast Cl); find_handler_for P ClassCast ((C, M, pc)#cs) = cs'; ek = (\(h,stk,loc). \ cast_ok (P\<^bsub>wf\<^esub>) Cl h (stk(length cs, stkLength P C M pc - Suc 0)))\<^sub>\ \ \ prog \ (_ (C, M, pc)#cs,None _) -ek\ (_ (C, M, pc)#cs,\(cs', True)\ _)" | JCFG_Checkcast_Exc_Update: "\ prog = (P, C0, Main); (instrs_of (P\<^bsub>wf\<^esub>) C M) ! pc = (Checkcast Cl); find_handler_for P ClassCast ((C, M, pc)#cs) = (C', M', pc')#cs'; ek = \(\(h,stk,loc). (h, stk((length cs',(stkLength P C' M' pc') - 1) := Addr (addr_of_sys_xcpt ClassCast)), loc) ) \ \ prog \ (_ (C, M, pc)#cs,\((C', M', pc')#cs', True)\ _) -ek\ (_ (C', M', pc')#cs',None _)" | JCFG_Checkcast_Exc_Exit: "\ prog = (P, C0, Main); (instrs_of (P\<^bsub>wf\<^esub>) C M) ! pc = (Checkcast Cl); find_handler_for P ClassCast ((C, M, pc)#cs) = [] \ \ prog \ (_ (C, M, pc)#cs,\([], True)\ _) -\id\ (_Exit_)" | JCFG_Invoke_Normal_Pred: "\ prog = (P, C0, Main); (instrs_of (P\<^bsub>wf\<^esub>) C M) ! pc = (Invoke M2 n); cd = length cs; stk_length = stkLength P C M pc; ek = (\(h,stk,loc). stk(cd, stk_length - Suc n) \ Null \ fst(method (P\<^bsub>wf\<^esub>) (cname_of h (the_Addr(stk(cd, stk_length - Suc n)))) M2) = D )\<^sub>\ \ \ prog \ (_ (C, M, pc)#cs,None _) -ek\ (_ (C, M, pc)#cs,\((D, M2, 0)#(C, M, pc)#cs, False)\ _)" | JCFG_Invoke_Normal_Update: "\ prog = (P, C0, Main); (instrs_of (P\<^bsub>wf\<^esub>) C M) ! pc = (Invoke M2 n); stk_length = stkLength P C M pc; loc_length = locLength P D M2 0; ek = \(\s. exec_instr (Invoke M2 n) P s (length cs) stk_length arbitrary loc_length) \ \ prog \ (_ (C, M, pc)#cs,\((D, M2, 0)#(C, M, pc)#cs, False)\ _) -ek\ (_ (D, M2, 0)#(C, M, pc)#cs,None _)" | JCFG_Invoke_Exc_Pred: "\ prog = (P, C0, Main); (instrs_of (P\<^bsub>wf\<^esub>) C M) ! pc = (Invoke m2 n); find_handler_for P NullPointer ((C, M, pc)#cs) = cs'; ek = (\(h,stk,loc). stk(length cs, stkLength P C M pc - Suc n) = Null)\<^sub>\ \ \ prog \ (_ (C, M, pc)#cs,None _) -ek\ (_ (C, M, pc)#cs,\(cs', True)\ _)" | JCFG_Invoke_Exc_Update: "\ prog = (P, C0, Main); (instrs_of (P\<^bsub>wf\<^esub>) C M) ! pc = (Invoke M2 n); find_handler_for P NullPointer ((C, M, pc)#cs) = (C', M', pc')#cs'; ek = \(\(h,stk,loc). (h, stk((length cs',(stkLength P C' M' pc') - 1) := Addr (addr_of_sys_xcpt NullPointer)), loc) ) \ \ prog \ (_ (C, M, pc)#cs,\((C', M', pc')#cs', True)\ _) -ek\ (_ (C', M', pc')#cs',None _)" | JCFG_Invoke_Exc_Exit: "\ prog = (P, C0, Main); (instrs_of (P\<^bsub>wf\<^esub>) C M) ! pc = (Invoke M2 n); find_handler_for P NullPointer ((C, M, pc)#cs) = [] \ \ prog \ (_ (C, M, pc)#cs,\([], True)\ _) -\id\ (_Exit_)" | JCFG_Return_Update: "\ prog = (P, C0, Main); (instrs_of (P\<^bsub>wf\<^esub>) C M) ! pc = Return; stk_length = stkLength P C M pc; r_stk_length = stkLength P C' M' (Suc pc'); ek = \(\s. exec_instr Return P s (Suc (length cs)) stk_length r_stk_length arbitrary) \ \ prog \ (_ (C, M, pc)#(C', M', pc')#cs,None _) -ek\ (_ (C', M', Suc pc')#cs,None _)" | JCFG_Goto_Update: "\ prog = (P, C0, Main); (instrs_of (P\<^bsub>wf\<^esub>) C M) ! pc = Goto idx \ \ prog \ (_ (C, M, pc)#cs,None _) -\id\ (_ (C, M, nat (int pc + idx))#cs,None _)" | JCFG_IfFalse_False: "\ prog = (P, C0, Main); (instrs_of (P\<^bsub>wf\<^esub>) C M) ! pc = (IfFalse b); b \ 1; ek = (\(h,stk,loc). stk(length cs, stkLength P C M pc - 1) = Bool False)\<^sub>\ \ \ prog \ (_ (C, M, pc)#cs,None _) -ek\ (_ (C, M, nat (int pc + b))#cs,None _)" | JCFG_IfFalse_Next: "\ prog = (P, C0, Main); (instrs_of (P\<^bsub>wf\<^esub>) C M) ! pc = (IfFalse b); ek = (\(h,stk,loc). stk(length cs, stkLength P C M pc - 1) \ Bool False \ b = 1)\<^sub>\ \ \ prog \ (_ (C, M, pc)#cs,None _) -ek\ (_ (C, M, Suc pc)#cs,None _)" | JCFG_Throw_Pred: "\ prog = (P, C0, Main); (instrs_of (P\<^bsub>wf\<^esub>) C M) ! pc = Throw; cd = length cs; stk_length = stkLength P C M pc; \Exc. find_handler_for P Exc ((C, M, pc)#cs) = cs'; ek = (\(h,stk,loc). (stk(length cs, stkLength P C M pc - 1) = Null \ find_handler_for P NullPointer ((C, M, pc)#cs) = cs') \ (stk(length cs, stkLength P C M pc - 1) \ Null \ find_handler_for P (cname_of h (the_Addr(stk(cd, stk_length - 1)))) ((C, M, pc)#cs) = cs') )\<^sub>\ \ \ prog \ (_ (C, M, pc)#cs,None _) -ek\ (_ (C, M, pc)#cs,\(cs', True)\ _)" | JCFG_Throw_Update: "\ prog = (P, C0, Main); (instrs_of (P\<^bsub>wf\<^esub>) C M) ! pc = Throw; ek = \(\(h,stk,loc). (h, stk((length cs',(stkLength P C' M' pc') - 1) := if (stk(length cs, stkLength P C M pc - 1) = Null) then Addr (addr_of_sys_xcpt NullPointer) else (stk(length cs, stkLength P C M pc - 1))), loc) ) \ \ prog \ (_ (C, M, pc)#cs,\((C', M', pc')#cs', True)\ _) -ek\ (_ (C', M', pc')#cs',None _)" | JCFG_Throw_Exit: "\ prog = (P, C0, Main); (instrs_of (P\<^bsub>wf\<^esub>) C M) ! pc = Throw \ \ prog \ (_ (C, M, pc)#cs,\([],True)\ _) -\id\ (_Exit_)" subsection \CFG properties\ lemma JVMCFG_Exit_no_sourcenode [dest]: assumes edge:"prog \ (_Exit_) -et\ n'" shows "False" proof - { fix n have "\prog \ n -et\ n'; n = (_Exit_)\ \ False" by (auto elim!: JVM_CFG.cases) } with edge show ?thesis by fastforce qed lemma JVMCFG_Entry_no_targetnode [dest]: assumes edge:"prog \ n -et\ (_Entry_)" shows "False" proof - { fix n' have "\prog \ n -et\ n'; n' = (_Entry_)\ \ False" by (auto elim!: JVM_CFG.cases) } with edge show ?thesis by fastforce qed lemma JVMCFG_EntryD: "\(P,C,M) \ n -et\ n'; n = (_Entry_)\ \ (n' = (_Exit_) \ et = (\s. False)\<^sub>\) \ (n' = (_ [(C,M,0)],None _) \ et = (\s. True)\<^sub>\)" by (erule JVM_CFG.cases) simp_all declare split_def [simp add] declare find_handler_for.simps [simp del] (* The following lemma explores many cases, it takes a little to prove *) lemma JVMCFG_edge_det: "\prog \ n -et\ n'; prog \ n -et'\ n'\ \ et = et'" by (erule JVM_CFG.cases, (erule JVM_CFG.cases, fastforce+)+) declare split_def [simp del] declare find_handler_for.simps [simp add] end