theory TM_Assembleimports Hoare_tm StateMonad "~~/src/HOL/Library/FinFun_Syntax" "~~/src/HOL/Library/Sublist" LetElimbeginsection {* The assembler based on Benton's x86 paper *}text {* The problem with the assembler is that it is too slow to be useful.*}primrec pass1 :: "tpg \<Rightarrow> (unit, (nat \<times> nat \<times> (nat \<rightharpoonup> nat))) SM" where "pass1 (TInstr ai) = sm_map (\<lambda> (pos, lno, lmap). (pos + 1, lno, lmap))" | "pass1 (TSeq p1 p2) = do {pass1 p1; pass1 p2 }" | "pass1 (TLocal fp) = do { lno \<leftarrow> tap (\<lambda> (pos, lno, lmap). lno); sm_map (\<lambda> (pos, lno, lmap). (pos, lno+1, lmap)); pass1 (fp lno) }" | "pass1 (TLabel l) = sm_map ((\<lambda> (pos, lno, lmap). (pos, lno, lmap(l \<mapsto> pos))))"declare pass1.simps[simp del]type_synonym ('a, 'b) alist = "('a \<times> 'b) list"primrec pass2 :: "tpg \<Rightarrow> (nat \<rightharpoonup> nat) \<Rightarrow> (unit, (nat \<times> nat \<times> (nat, tm_inst) alist)) SM" where "pass2 (TInstr ai) lmap = sm_map (\<lambda> (pos, lno, prog). (pos + 1, lno, (pos, ai)#prog))" | "pass2 (TSeq p1 p2) lmap = do {pass2 p1 lmap; pass2 p2 lmap}" | "pass2 (TLocal fp) lmap = do { lno \<leftarrow> tap (\<lambda> (pos, lno, prog). lno); sm_map (\<lambda> (pos, lno, prog). (pos, lno + 1, prog)); (case (lmap lno) of Some l => pass2 (fp l) lmap | None => (raise ''Undefined label''))} " | "pass2 (TLabel l) lmap = do { pos \<leftarrow> tap (\<lambda> (pos, lno, prog). pos); if (l = pos) then return () else (raise ''Label mismatch'') }"declare pass2.simps[simp del]definition "assembleM i tpg = do {(x, (pos, lno, lmap)) \<leftarrow> execute (pass1 tpg) (i, 0, empty); execute (pass2 tpg lmap) (i, 0, [])}"definition "assemble i tpg = Option.map (\<lambda> (x, (j, lno, prog)).(prog, j)) (assembleM i tpg)"lemma tprog_set_union: assumes "(fst ` set pg3) \<inter> (fst ` set pg2) = {}" shows "tprog_set (map_of pg3 ++ map_of pg2) = tprog_set (map_of pg3) \<union> tprog_set (map_of pg2)"proof - from assms have "dom (map_of pg3) \<inter> dom (map_of pg2) = {}" by (metis dom_map_of_conv_image_fst) hence map_comm: "map_of pg3 ++ map_of pg2 = map_of pg2 ++ map_of pg3" by (metis map_add_comm) show ?thesis proof show "tprog_set (map_of pg3 ++ map_of pg2) \<subseteq> tprog_set (map_of pg3) \<union> tprog_set (map_of pg2)" proof fix x assume " x \<in> tprog_set (map_of pg3 ++ map_of pg2)" then obtain i inst where h: "x = TC i inst" "(map_of pg3 ++ map_of pg2) i = Some inst" apply (unfold tprog_set_def) by (smt mem_Collect_eq) from map_add_SomeD[OF h(2)] h(1) show " x \<in> tprog_set (map_of pg3) \<union> tprog_set (map_of pg2)" apply (unfold tprog_set_def) by (smt mem_Collect_eq sup1CI sup_Un_eq) qed next show "tprog_set (map_of pg3) \<union> tprog_set (map_of pg2) \<subseteq> tprog_set (map_of pg3 ++ map_of pg2)" proof fix x assume " x \<in> tprog_set (map_of pg3) \<union> tprog_set (map_of pg2)" then obtain i inst where h: "x = TC i inst" "map_of pg3 i = Some inst \<or> map_of pg2 i = Some inst" apply (unfold tprog_set_def) by (smt Un_iff mem_Collect_eq) from h(2) show "x \<in> tprog_set (map_of pg3 ++ map_of pg2)" proof assume "map_of pg2 i = Some inst" hence "(map_of pg3 ++ map_of pg2) i = Some inst" by (metis map_add_find_right) with h(1) show ?thesis apply (unfold tprog_set_def) by (smt mem_Collect_eq) next assume "map_of pg3 i = Some inst" hence "(map_of pg2 ++ map_of pg3) i = Some inst" by (metis map_add_find_right) with h(1) show ?thesis apply (unfold map_comm) apply (unfold tprog_set_def) by (smt mem_Collect_eq) qed qed qedqedlemma assumes "assemble i c = Some (prog, j)" shows "(i:[c]:j) (tprog_set (map_of prog))"proof - from assms obtain x lno where "(assembleM i c) = Some (x, (j, lno, prog))" apply(unfold assemble_def) by (cases "(assembleM i c)", auto) then obtain y pos lno' lmap where "execute (pass1 c) (i, 0, empty) = Some (y, (pos, lno', lmap))" "execute (pass2 c lmap) (i, 0, []) = Some (x, (j, lno, prog))" apply (unfold assembleM_def) by (cases "execute (pass1 c) (i, 0, Map.empty)", auto simp:Option.bind.simps) hence mid: "effect (pass1 c) (i, 0, empty) (pos, lno', lmap) y" "effect (pass2 c lmap) (i, 0, []) (j, lno, prog) x" by (auto intro:effectI) { fix lnos lmap lmap' prog1 prog2 assume "effect (pass2 c lmap') (i, lnos, prog1) (j, lno, prog2) x" hence "\<exists> prog. (prog2 = prog@prog1 \<and> (i:[c]:j) (tprog_set (map_of prog)) \<and> (\<forall> k \<in> fst ` (set prog). i \<le> k \<and> k < j) \<and> i \<le> j)" proof(induct c arbitrary:lmap' i lnos prog1 j lno prog2 x) case (TInstr instr lmap' i lnos prog1 j lno prog2 x) thus ?case apply (auto simp: effect_def assemble_def assembleM_def execute.simps sm_map_def sm_def tprog_set_def tassemble_to.simps sg_def pass1.simps pass2.simps split:if_splits) by (cases instr, auto) next case (TLabel l lmap' i lnos prog1 j lno prog2 x) thus ?case apply (rule_tac x = "[]" in exI) apply (unfold tassemble_to.simps) by (auto simp: effect_def assemble_def assembleM_def execute.simps sm_map_def sm_def tprog_set_def tassemble_to.simps sg_def pass1.simps pass2.simps tap_def bind_def return_def raise_def sep_empty_def set_ins_def split:if_splits) next case (TSeq c1 c2 lmap' i lnos prog1 j lno prog2 x) from TSeq(3) obtain h' r where "effect (pass2 c1 lmap') (i, lnos, prog1) h' r" "effect (pass2 c2 lmap') h' (j, lno, prog2) x" apply (unfold pass2.simps) by (auto elim!:effect_elims) then obtain pos1 lno1 pg1 where h: "effect (pass2 c1 lmap') (i, lnos, prog1) (pos1, lno1, pg1) r" "effect (pass2 c2 lmap') (pos1, lno1, pg1) (j, lno, prog2) x" by (cases h', auto) from TSeq(1)[OF h(1)] TSeq(2)[OF h(2)] obtain pg2 pg3 where hh: "pg1 = pg2 @ prog1 \<and> (i :[ c1 ]: pos1) (tprog_set (map_of pg2))" "(\<forall>k\<in> fst ` (set pg2). i \<le> k \<and> k < pos1)" "i \<le> pos1" "prog2 = pg3 @ pg1 \<and> (pos1 :[ c2 ]: j) (tprog_set (map_of pg3))" "(\<forall>k\<in>fst ` (set pg3). pos1 \<le> k \<and> k < j)" "pos1 \<le> j" by auto thus ?case apply (rule_tac x = "pg3 @ pg2" in exI, auto) apply (unfold tassemble_to.simps) apply (rule_tac x = pos1 in EXS_intro) my_block have "(tprog_set (map_of pg2 ++ map_of pg3)) = tprog_set (map_of pg2) \<union> tprog_set (map_of pg3)" proof(rule tprog_set_union) from hh(2, 5) show "fst ` set pg2 \<inter> fst ` set pg3 = {}" by (smt disjoint_iff_not_equal) qed my_block_end apply (unfold this, insert this) my_block have "tprog_set (map_of pg2) \<inter> tprog_set (map_of pg3) = {}" proof - { fix x assume h: "x \<in> tprog_set (map_of pg2)" "x \<in> tprog_set (map_of pg3)" then obtain i inst where "x = TC i inst" "map_of pg2 i = Some inst" "map_of pg3 i = Some inst" apply (unfold tprog_set_def) by (smt mem_Collect_eq tresource.inject(2)) hence "(i, inst) \<in> set pg2" "(i, inst) \<in> set pg3" by (metis map_of_SomeD)+ with hh(2, 5) have "False" by (smt rev_image_eqI) } thus ?thesis by auto qed my_block_end apply (insert this) apply (fold set_ins_def) by (rule sep_conjI, assumption+, simp) next case (TLocal body lmap' i lnos prog1 j lno prog2 x) from TLocal(2) obtain l where h: "lmap' lnos = Some l" "effect (pass2 (body l) lmap') (i, Suc lnos, prog1) (j, lno, prog2) ()" apply (unfold pass2.simps) by (auto elim!:effect_elims split:option.splits simp:sm_map_def) from TLocal(1)[OF this(2)] obtain pg where hh: "prog2 = pg @ prog1 \<and> (i :[ body l ]: j) (tprog_set (map_of pg))" "(\<forall>k\<in> fst ` (set pg). i \<le> k \<and> k < j)" "i \<le> j" by auto thus ?case apply (rule_tac x = pg in exI, auto) apply (unfold tassemble_to.simps) by (rule_tac x = l in EXS_intro, auto) qed } from this[OF mid(2)] show ?thesis by autoqeddefinition "valid_tpg tpg = (\<forall> i. \<exists> j prog. assemble i tpg = Some (j, prog))"section {* A new method based on DB indexing *}text {* In this section, we introduced a new method based on DB-indexing to provide a quick check of assemblebility of TM assmbly programs in the format of @{text "tpg"}. The lemma @{text "ct_left_until_zero"} at the end shows how the well-formedness of @{text "left_until_zero"} is proved in a modular way.*}datatype cpg = CInstr tm_inst | CLabel nat | CSeq cpg cpg | CLocal cpgdatatype status = Free | Bounddefinition "lift_b t i j = (if (j \<ge> t) then (j + i) else j)"fun lift_t :: "nat \<Rightarrow> nat \<Rightarrow> cpg \<Rightarrow> cpg"where "lift_t t i (CInstr ((act0, l0), (act1, l1))) = (CInstr ((act0, lift_b t i l0), (act1, lift_b t i l1)))" | "lift_t t i (CLabel l) = CLabel (lift_b t i l)" | "lift_t t i (CSeq c1 c2) = CSeq (lift_t t i c1) (lift_t t i c2)" | "lift_t t i (CLocal c) = CLocal (lift_t (t + 1) i c)"definition "lift0 (i::nat) cpg = lift_t 0 i cpg"definition "perm_b t i j k = (if ((k::nat) = i \<and> i < t \<and> j < t) then j else if (k = j \<and> i < t \<and> j < t) then i else k)"lemma inj_perm_b: "inj (perm_b t i j)"proof(induct rule:injI) case (1 x y) thus ?case by (unfold perm_b_def, auto split:if_splits)qedfun perm :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> cpg \<Rightarrow> cpg"where "perm t i j (CInstr ((act0, l0), (act1, l1))) = (CInstr ((act0, perm_b t i j l0), (act1, perm_b t i j l1)))" | "perm t i j (CLabel l) = CLabel (perm_b t i j l)" | "perm t i j (CSeq c1 c2) = CSeq (perm t i j c1) (perm t i j c2)" | "perm t i j (CLocal c) = CLocal (perm (t + 1) (i + 1) (j + 1) c)"definition "map_idx f sts = map (\<lambda> k. sts!(f (nat k))) [0 .. int (length sts) - 1]"definition "perm_s i j sts = map_idx (perm_b (length sts) i j) sts" value "perm_s 2 5 [(0::int), 1, 2, 3, 4, 5, 6, 7, 8, 9, 10]"lemma "perm_s 2 20 [(0::int), 1, 2, 3, 4, 5, 6, 7, 8, 9, 10] = x" apply (unfold perm_s_def map_idx_def perm_b_def, simp add:upto.simps) oopslemma upto_len: "length [i .. j] = (if j < i then 0 else (nat (j - i + 1)))"proof(induct i j rule:upto.induct) case (1 i j) show ?case proof(cases "j < i") case True thus ?thesis by simp next case False hence eq_ij: "[i..j] = i # [i + 1..j]" by (simp add:upto.simps) from 1 False show ?thesis by (auto simp:eq_ij) qedqedlemma perm_s_len: "length (perm_s i j sts') = length sts'" apply (unfold perm_s_def map_idx_def) by (smt Nil_is_map_conv length_0_conv length_greater_0_conv length_map neq_if_length_neq upto_len)fun c2t :: "nat list \<Rightarrow> cpg \<Rightarrow> tpg" where "c2t env (CInstr ((act0, st0), (act1, st1))) = TInstr ((act0, env!st0), (act1, env!st1))" | "c2t env (CLabel l) = TLabel (env!l)" | "c2t env (CSeq cpg1 cpg2) = TSeq (c2t env cpg1) (c2t env cpg2)" | "c2t env (CLocal cpg) = TLocal (\<lambda> x. c2t (x#env) cpg)" instantiation status :: minusbegin fun minus_status :: "status \<Rightarrow> status \<Rightarrow> status" where "minus_status Bound Bound = Free" | "minus_status Bound Free = Bound" | "minus_status Free x = Free " instance ..endinstantiation status :: plusbegin fun plus_status :: "status \<Rightarrow> status \<Rightarrow> status" where "plus_status Free x = x" | "plus_status Bound x = Bound" instance ..endinstantiation list :: (plus)plusbegin fun plus_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where "plus_list [] ys = []" | "plus_list (x#xs) [] = []" | "plus_list (x#xs) (y#ys) = ((x + y)#plus_list xs ys)" instance ..endinstantiation list :: (minus)minusbegin fun minus_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where "minus_list [] ys = []" | "minus_list (x#xs) [] = []" | "minus_list (x#xs) (y#ys) = ((x - y)#minus_list xs ys)" instance ..end(* consts castr :: "nat list \<Rightarrow> nat \<Rightarrow> cpg \<Rightarrow> nat \<Rightarrow> tassert"definition "castr env i cpg j = (i:[c2t env cpg]:j)" *)(*definition "c2p sts i cpg j = (\<forall> x. ((length x = length sts \<and> (\<forall> k < length sts. sts!k = Bound \<longrightarrow> (\<exists> f. x!k = f i))) \<longrightarrow> (\<exists> s. (i:[(c2t x cpg)]:j) s)))"*)definition "c2p sts i cpg j = (\<exists> f. \<forall> x. ((length x = length sts \<and> (\<forall> k < length sts. sts!k = Bound \<longrightarrow> (x!k = f i k))) \<longrightarrow> (\<exists> s. (i:[(c2t x cpg)]:j) s)))"fun wf_cpg_test :: "status list \<Rightarrow> cpg \<Rightarrow> (bool \<times> status list)" where "wf_cpg_test sts (CInstr ((a0, l0), (a1, l1))) = ((l0 < length sts \<and> l1 < length sts), sts)" | "wf_cpg_test sts (CLabel l) = ((l < length sts) \<and> sts!l = Free, sts[l:=Bound])" | "wf_cpg_test sts (CSeq c1 c2) = (let (b1, sts1) = wf_cpg_test sts c1; (b2, sts2) = wf_cpg_test sts1 c2 in (b1 \<and> b2, sts2))" | "wf_cpg_test sts (CLocal body) = (let (b, sts') = (wf_cpg_test (Free#sts) body) in (b, tl sts'))" instantiation status :: orderbegin definition less_eq_status_def: "((st1::status) \<le> st2) = (st1 = Free \<or> st2 = Bound)" definition less_status_def: "((st1::status) < st2) = (st1 \<le> st2 \<and> st1 \<noteq> st2)"instanceproof fix x y show "(x < (y::status)) = (x \<le> y \<and> \<not> y \<le> x)" by (metis less_eq_status_def less_status_def status.distinct(1))next fix x show "x \<le> (x::status)" by (metis (full_types) less_eq_status_def status.exhaust)next fix x y z assume "x \<le> y" "y \<le> (z::status)" show "x \<le> (z::status)" by (metis `x \<le> y` `y \<le> z` less_eq_status_def status.distinct(1))next fix x y assume "x \<le> y" "y \<le> (x::status)" show "x = y" by (metis `x \<le> y` `y \<le> x` less_eq_status_def status.distinct(1))qedendinstantiation list :: (order)orderbegin definition "((sts::('a::order) list) \<le> sts') = ((length sts = length sts') \<and> (\<forall> i < length sts. sts!i \<le> sts'!i))" definition "((sts::('a::order) list) < sts') = ((sts \<le> sts') \<and> sts \<noteq> sts')" lemma anti_sym: assumes h: "x \<le> (y::'a list)" "y \<le> x" shows "x = y" proof - from h have "length x = length y" by (metis less_eq_list_def) moreover from h have " (\<forall> i < length x. x!i = y!i)" by (metis (full_types) antisym_conv less_eq_list_def) ultimately show ?thesis by (metis nth_equalityI) qed lemma refl: "x \<le> (x::('a::order) list)" apply (unfold less_eq_list_def) by (metis order_refl) instance proof fix x y show "((x::('a::order) list) < y) = (x \<le> y \<and> \<not> y \<le> x)" proof assume h: "x \<le> y \<and> \<not> y \<le> x" have "x \<noteq> y" proof assume "x = y" with h have "\<not> (x \<le> x)" by simp with refl show False by auto qed moreover from h have "x \<le> y" by blast ultimately show "x < y" by (auto simp:less_list_def) next assume h: "x < y" hence hh: "x \<le> y" by (metis TM_Assemble.less_list_def) moreover have "\<not> y \<le> x" proof assume "y \<le> x" from anti_sym[OF hh this] have "x = y" . with h show False by (metis less_list_def) qed ultimately show "x \<le> y \<and> \<not> y \<le> x" by auto qed next fix x from refl show "(x::'a list) \<le> x" . next fix x y assume "(x::'a list) \<le> y" "y \<le> x" from anti_sym[OF this] show "x = y" . next fix x y z assume h: "(x::'a list) \<le> y" "y \<le> z" show "x \<le> z" proof - from h have "length x = length z" by (metis TM_Assemble.less_eq_list_def) moreover from h have "\<forall> i < length x. x!i \<le> z!i" by (metis TM_Assemble.less_eq_list_def order_trans) ultimately show "x \<le> z" by (metis TM_Assemble.less_eq_list_def) qed qedendlemma sts_bound_le: "sts \<le> sts[l := Bound]"proof - have "length sts = length (sts[l := Bound])" by (metis length_list_update) moreover have "\<forall> i < length sts. sts!i \<le> (sts[l:=Bound])!i" proof - { fix i assume "i < length sts" have "sts ! i \<le> sts[l := Bound] ! i" proof(cases "l < length sts") case True note le_l = this show ?thesis proof(cases "l = i") case True with le_l have "sts[l := Bound] ! i = Bound" by auto thus ?thesis by (metis less_eq_status_def) next case False with le_l have "sts[l := Bound] ! i = sts!i" by auto thus ?thesis by auto qed next case False hence "sts[l := Bound] = sts" by auto thus ?thesis by auto qed } thus ?thesis by auto qed ultimately show ?thesis by (metis less_eq_list_def) qedlemma sts_tl_le: assumes "sts \<le> sts'" shows "tl sts \<le> tl sts'"proof - from assms have "length (tl sts) = length (tl sts')" by (metis (hide_lams, no_types) length_tl less_eq_list_def) moreover from assms have "\<forall> i < length (tl sts). (tl sts)!i \<le> (tl sts')!i" by (smt calculation length_tl less_eq_list_def nth_tl) ultimately show ?thesis by (metis less_eq_list_def)qedlemma wf_cpg_test_le: assumes "wf_cpg_test sts cpg = (True, sts')" shows "sts \<le> sts'" using assmsproof(induct cpg arbitrary:sts sts') case (CInstr instr sts sts') obtain a0 l0 a1 l1 where eq_instr: "instr = ((a0, l0), (a1, l1))" by (metis prod.exhaust) from CInstr[unfolded this] show ?case by simpnext case (CLabel l sts sts') thus ?case by (auto simp:sts_bound_le)next case (CLocal body sts sts') from this(2) obtain sts1 where h: "wf_cpg_test (Free # sts) body = (True, sts1)" "sts' = tl sts1" by (auto split:prod.splits) from CLocal(1)[OF this(1)] have "Free # sts \<le> sts1" . from sts_tl_le[OF this] have "sts \<le> tl sts1" by simp from this[folded h(2)] show ?case .next case (CSeq cpg1 cpg2 sts sts') from this(3) show ?case by (auto split:prod.splits dest!:CSeq(1, 2))qedlemma c2p_assert: assumes "(c2p [] i cpg j)" shows "\<exists> s. (i :[(c2t [] cpg)]: j) s"proof - from assms obtain f where h [rule_format]: "\<forall> x. length x = length [] \<and> (\<forall>k<length []. [] ! k = Bound \<longrightarrow> (x ! k = f i k)) \<longrightarrow> (\<exists> s. (i :[ c2t [] cpg ]: j) s)" by (unfold c2p_def, auto) have "length [] = length [] \<and> (\<forall>k<length []. [] ! k = Bound \<longrightarrow> ([] ! k = f i k))" by auto from h[OF this] obtain s where "(i :[ c2t [] cpg ]: j) s" by blast thus ?thesis by autoqeddefinition "sts_disj sts sts' = ((length sts = length sts') \<and> (\<forall> i < length sts. \<not>(sts!i = Bound \<and> sts'!i = Bound)))"lemma length_sts_plus: assumes "length (sts1 :: status list) = length sts2" shows "length (sts1 + sts2) = length sts1" using assmsproof(induct sts1 arbitrary: sts2) case Nil thus ?case by (metis plus_list.simps(1))next case (Cons s' sts' sts2) thus ?case proof(cases "sts2 = []") case True with Cons show ?thesis by auto next case False then obtain s'' sts'' where eq_sts2: "sts2 = s''#sts''" by (metis neq_Nil_conv) with Cons show ?thesis by (metis length_Suc_conv list.inject plus_list.simps(3)) qedqedlemma nth_sts_plus: assumes "i < length ((sts1::status list) + sts2)" shows "(sts1 + sts2)!i = sts1!i + sts2!i" using assmsproof(induct sts1 arbitrary:i sts2) case (Nil i sts2) thus ?case by autonext case (Cons s' sts' i sts2) show ?case proof(cases "sts2 = []") case True with Cons show ?thesis by auto next case False then obtain s'' sts'' where eq_sts2: "sts2 = s''#sts''" by (metis neq_Nil_conv) with Cons show ?thesis by (smt list.size(4) nth_Cons' plus_list.simps(3)) qedqedlemma nth_sts_minus: assumes "i < length ((sts1::status list) - sts2)" shows "(sts1 - sts2)!i = sts1!i - sts2!i" using assmsproof(induct arbitrary:i rule:minus_list.induct) case (3 x xs y ys i) show ?case proof(cases i) case 0 thus ?thesis by simp next case (Suc k) with 3(2) have "k < length (xs - ys)" by auto from 3(1)[OF this] and Suc show ?thesis by auto qedqed autofun taddr :: "tresource \<Rightarrow> nat" where "taddr (TC i instr) = i"lemma tassemble_to_range: assumes "(i :[tpg]: j) s" shows "(i \<le> j) \<and> (\<forall> r \<in> s. i \<le> taddr r \<and> taddr r < j)" using assmsproof(induct tpg arbitrary: i j s) case (TInstr instr i j s) obtain a0 l0 a1 l1 where "instr = ((a0, l0), (a1, l1))" by (metis pair_collapse) with TInstr show ?case apply (simp add:tassemble_to.simps sg_def) by (smt `instr = ((a0, l0), a1, l1)` cond_eq cond_true_eq1 empty_iff insert_iff le_refl lessI sep.mult_commute taddr.simps)next case (TLabel l i j s) thus ?case apply (simp add:tassemble_to.simps) by (smt equals0D pasrt_def set_zero_def)next case (TSeq c1 c2 i j s) from TSeq(3) obtain s1 s2 j' where h: "(i :[ c1 ]: j') s1" "(j' :[ c2 ]: j) s2" "s1 ## s2" "s = s1 + s2" by (auto simp:tassemble_to.simps elim!:EXS_elim sep_conjE) show ?case proof - { fix r assume "r \<in> s" with h (3, 4) have "r \<in> s1 \<or> r \<in> s2" by (auto simp:set_ins_def) hence "i \<le> j \<and> i \<le> taddr r \<and> taddr r < j" proof assume " r \<in> s1" from TSeq(1)[OF h(1)] have "i \<le> j'" "(\<forall>r\<in>s1. i \<le> taddr r \<and> taddr r < j')" by auto from this(2)[rule_format, OF `r \<in> s1`] have "i \<le> taddr r" "taddr r < j'" by auto with TSeq(2)[OF h(2)] show ?thesis by auto next assume "r \<in> s2" from TSeq(2)[OF h(2)] have "j' \<le> j" "(\<forall>r\<in>s2. j' \<le> taddr r \<and> taddr r < j)" by auto from this(2)[rule_format, OF `r \<in> s2`] have "j' \<le> taddr r" "taddr r < j" by auto with TSeq(1)[OF h(1)] show ?thesis by auto qed } thus ?thesis by (smt TSeq.hyps(1) TSeq.hyps(2) h(1) h(2)) qednext case (TLocal body i j s) from this(2) obtain l s' where "(i :[ body l ]: j) s" by (simp add:tassemble_to.simps, auto elim!:EXS_elim) from TLocal(1)[OF this] show ?case by autoqedlemma c2p_seq: assumes "c2p sts1 i cpg1 j'" "c2p sts2 j' cpg2 j" "sts_disj sts1 sts2" shows "(c2p (sts1 + sts2) i (CSeq cpg1 cpg2) j)" proof - from assms(1)[unfolded c2p_def] obtain f1 where h1[rule_format]: "\<forall>x. length x = length sts1 \<and> (\<forall>k<length sts1. sts1 ! k = Bound \<longrightarrow> (x ! k = f1 i k)) \<longrightarrow> Ex (i :[ c2t x cpg1 ]: j')" by blast from assms(2)[unfolded c2p_def] obtain f2 where h2[rule_format]: "\<forall>x. length x = length sts2 \<and> (\<forall>k<length sts2. sts2 ! k = Bound \<longrightarrow> (x ! k = f2 j' k)) \<longrightarrow> Ex (j' :[ c2t x cpg2 ]: j)" by blast from assms(3)[unfolded sts_disj_def] have h3: "length sts1 = length sts2" and h4[rule_format]: "(\<forall>i<length sts1. \<not> (sts1 ! i = Bound \<and> sts2 ! i = Bound))" by auto let ?f = "\<lambda> i k. if (sts1!k = Bound) then f1 i k else f2 j' k" { fix x assume h5: "length x = length (sts1 + sts2)" and h6[rule_format]: "(\<forall>k<length (sts1 + sts2). (sts1 + sts2) ! k = Bound \<longrightarrow> x ! k = ?f i k)" obtain s1 where h_s1: "(i :[ c2t x cpg1 ]: j') s1" proof(atomize_elim, rule h1) from h3 h5 have "length x = length sts1" by (metis length_sts_plus) moreover { fix k assume hh: "k<length sts1" "sts1 ! k = Bound" from hh(1) h3 h5 have p1: "k < length (sts1 + sts2)" by (metis calculation) from h3 hh(2) have p2: "(sts1 + sts2)!k = Bound" by (metis nth_sts_plus p1 plus_status.simps(2)) from h6[OF p1 p2] have "x ! k = (if sts1 ! k = Bound then f1 i k else f2 j' k)" . with hh(2) have "x ! k = f1 i k" by simp } ultimately show "length x = length sts1 \<and> (\<forall>k<length sts1. sts1 ! k = Bound \<longrightarrow> (x ! k = f1 i k))" by blast qed obtain s2 where h_s2: "(j' :[ c2t x cpg2 ]: j) s2" proof(atomize_elim, rule h2) from h3 h5 have "length x = length sts2" by (metis length_sts_plus) moreover { fix k assume hh: "k<length sts2" "sts2 ! k = Bound" from hh(1) h3 h5 have p1: "k < length (sts1 + sts2)" by (metis calculation) from hh(1) h3 h5 hh(2) have p2: "(sts1 + sts2)!k = Bound" by (metis `length sts1 = length sts2 \<and> (\<forall>i<length sts1. \<not> (sts1 ! i = Bound \<and> sts2 ! i = Bound))` calculation nth_sts_plus plus_status.simps(1) status.distinct(1) status.exhaust) from h6[OF p1 p2] have "x ! k = (if sts1 ! k = Bound then f1 i k else f2 j' k)" . moreover from h4[OF hh(1)[folded h3]] hh(2) have "sts1!k \<noteq> Bound" by auto ultimately have "x!k = f2 j' k" by simp } ultimately show "length x = length sts2 \<and> (\<forall>k<length sts2. sts2 ! k = Bound \<longrightarrow> (x ! k = f2 j' k))" by blast qed have h_s12: "s1 ## s2" proof - { fix r assume h: "r \<in> s1" "r \<in> s2" with h_s1 h_s2 have "False"by (smt tassemble_to_range) } thus ?thesis by (auto simp:set_ins_def) qed have "(EXS j'. i :[ c2t x cpg1 ]: j' \<and>* j' :[ c2t x cpg2 ]: j) (s1 + s2)" proof(rule_tac x = j' in EXS_intro) from h_s1 h_s2 h_s12 show "(i :[ c2t x cpg1 ]: j' \<and>* j' :[ c2t x cpg2 ]: j) (s1 + s2)" by (metis sep_conjI) qed hence "\<exists> s. (i :[ c2t x (CSeq cpg1 cpg2) ]: j) s" by (auto simp:tassemble_to.simps) } hence "\<exists>f. \<forall>x. length x = length (sts1 + sts2) \<and> (\<forall>k<length (sts1 + sts2). (sts1 + sts2) ! k = Bound \<longrightarrow> x ! k = f i k) \<longrightarrow> Ex (i :[ c2t x (CSeq cpg1 cpg2) ]: j)" by (rule_tac x = ?f in exI, auto) thus ?thesis by(unfold c2p_def, auto)qedlemma plus_list_len: "length ((sts1::status list) + sts2) = min (length sts1) (length sts2)" by(induct rule:plus_list.induct, auto)lemma minus_list_len: "length ((sts1::status list) - sts2) = min (length sts1) (length sts2)" by(induct rule:minus_list.induct, auto)lemma sts_le_comb: assumes "sts1 \<le> sts2" and "sts2 \<le> sts3" shows "sts_disj (sts2 - sts1) (sts3 - sts2)" and "(sts3 - sts1) = (sts2 - sts1) + (sts3 - sts2)"proof - from assms have h1: "length sts1 = length sts2" "\<forall>i<length sts1. sts1 ! i \<le> sts2 ! i" and h2: "length sts2 = length sts3" "\<forall>i<length sts1. sts2 ! i \<le> sts3 ! i" by (unfold less_eq_list_def, auto) have "sts_disj (sts2 - sts1) (sts3 - sts2)" proof - from h1(1) h2(1) have "length (sts2 - sts1) = length (sts3 - sts2)" by (metis minus_list_len) moreover { fix i assume lt_i: "i<length (sts2 - sts1)" from lt_i h1(1) h2(1) have "i < length sts1" by (smt minus_list_len) from h1(2)[rule_format, of i, OF this] h2(2)[rule_format, of i, OF this] have "sts1 ! i \<le> sts2 ! i" "sts2 ! i \<le> sts3 ! i" . moreover have "(sts2 - sts1) ! i = sts2!i - sts1!i" by (metis lt_i nth_sts_minus) moreover have "(sts3 - sts2)!i = sts3!i - sts2!i" by (metis `length (sts2 - sts1) = length (sts3 - sts2)` lt_i nth_sts_minus) ultimately have " \<not> ((sts2 - sts1) ! i = Bound \<and> (sts3 - sts2) ! i = Bound)" apply (cases "sts2!i", cases "sts1!i", cases "sts3!i", simp, simp) apply (cases "sts3!i", simp, simp) apply (cases "sts1!i", cases "sts3!i", simp, simp) by (cases "sts3!i", simp, simp) } ultimately show ?thesis by (unfold sts_disj_def, auto) qed moreover have "(sts3 - sts1) = (sts2 - sts1) + (sts3 - sts2)" proof(induct rule:nth_equalityI) case 1 show ?case by (metis h1(1) h2(1) length_sts_plus minus_list_len) next case 2 { fix i assume lt_i: "i<length (sts3 - sts1)" have "(sts3 - sts1) ! i = (sts2 - sts1 + (sts3 - sts2)) ! i" (is "?L = ?R") proof - have "?R = sts2!i - sts1!i + (sts3!i - sts2!i)" by (smt `i < length (sts3 - sts1)` h2(1) minus_list_len nth_sts_minus nth_sts_plus plus_list_len) moreover have "?L = sts3!i - sts1!i" by (metis `i < length (sts3 - sts1)` nth_sts_minus) moreover have "sts2!i - sts1!i + (sts3!i - sts2!i) = sts3!i - sts1!i" proof - from lt_i h1(1) h2(1) have "i < length sts1" by (smt minus_list_len) from h1(2)[rule_format, of i, OF this] h2(2)[rule_format, of i, OF this] show ?thesis apply (cases "sts2!i", cases "sts1!i", cases "sts3!i", simp, simp) apply (cases "sts3!i", simp, simp) apply (cases "sts1!i", cases "sts3!i", simp, simp) by (cases "sts3!i", simp, simp) qed ultimately show ?thesis by simp qed } thus ?case by auto qed ultimately show "sts_disj (sts2 - sts1) (sts3 - sts2)" and "(sts3 - sts1) = (sts2 - sts1) + (sts3 - sts2)" by autoqedlemma wf_cpg_test_correct: assumes "wf_cpg_test sts cpg = (True, sts')" shows "(\<forall> i. \<exists> j. (c2p (sts' - sts) i cpg j))" using assmsproof(induct cpg arbitrary:sts sts') case (CInstr instr sts sts') obtain a0 l0 a1 l1 where eq_instr: "instr = ((a0, l0), (a1, l1))" by (metis prod.exhaust) show ?case proof(unfold eq_instr c2p_def, clarsimp simp:tassemble_to.simps) fix i let ?a = "Suc i" and ?f = "\<lambda> i k. i" show "\<exists>a f. \<forall>x. length x = length (sts' - sts) \<and> (\<forall>k<length (sts' - sts). (sts' - sts) ! k = Bound \<longrightarrow> x ! k = f i k) \<longrightarrow> Ex (sg {TC i ((a0, x ! l0), a1, x ! l1)} \<and>* <(a = Suc i)>)" proof(rule_tac x = ?a in exI, rule_tac x = ?f in exI, default, clarsimp) fix x let ?j = "Suc i" let ?s = " {TC i ((a0, x ! l0), a1, x ! l1)}" have "(sg {TC i ((a0, x ! l0), a1, x ! l1)} \<and>* <(Suc i = Suc i)>) ?s" by (simp add:tassemble_to.simps sg_def) thus "Ex (sg {TC i ((a0, x ! l0), a1, x ! l1)})" by auto qed qednext case (CLabel l sts sts') show ?case proof fix i from CLabel have h1: "l < length sts" and h2: "sts ! l = Free" and h3: "sts[l := Bound] = sts'" by auto let ?f = "\<lambda> i k. i" have "\<exists>a f. \<forall>x. length x = length (sts' - sts) \<and> (\<forall>k<length (sts' - sts). (sts' - sts) ! k = Bound \<longrightarrow> x ! k = f (i::nat) k) \<longrightarrow> Ex (<(i = a \<and> a = x ! l)>)" proof(rule_tac x = i in exI, rule_tac x = ?f in exI, clarsimp) fix x assume h[rule_format]: "\<forall>k<length (sts' - sts). (sts' - sts) ! k = Bound \<longrightarrow> x ! k = i" from h1 h3 have p1: "l < length (sts' - sts)" by (metis length_list_update min.idem minus_list_len) from p1 h2 h3 have p2: "(sts' - sts)!l = Bound" by (metis h1 minus_status.simps(2) nth_list_update_eq nth_sts_minus) from h[OF p1 p2] have "(<(i = x ! l)>) 0" by (simp add:set_ins_def) thus "\<exists> s. (<(i = x ! l)>) s" by auto qed thus "\<exists>a. c2p (sts' - sts) i (CLabel l) a" by (auto simp:c2p_def tassemble_to.simps) qednext case (CSeq cpg1 cpg2 sts sts') show ?case proof fix i from CSeq(3)[unfolded wf_cpg_test.simps] show "\<exists> j. c2p (sts' - sts) i (CSeq cpg1 cpg2) j" proof(let_elim) case (LetE b1 sts1) from this(1) obtain b2 where h: "(b2, sts') = wf_cpg_test sts1 cpg2" "b1=True" "b2=True" by (atomize_elim, unfold Let_def, auto split:prod.splits) from wf_cpg_test_le[OF LetE(2)[symmetric, unfolded h(2)]] have sts_le1: "sts \<le> sts1" . from CSeq(1)[OF LetE(2)[unfolded h(2), symmetric], rule_format, of i] obtain j1 where h1: "(c2p (sts1 - sts) i cpg1 j1)" by blast from wf_cpg_test_le[OF h(1)[symmetric, unfolded h(3)]] have sts_le2: "sts1 \<le> sts'" . from sts_le_comb[OF sts_le1 sts_le2] have hh: "sts_disj (sts1 - sts) (sts' - sts1)" "sts' - sts = (sts1 - sts) + (sts' - sts1)" . from CSeq(2)[OF h(1)[symmetric, unfolded h(3)], rule_format, of j1] obtain j2 where h2: "(c2p (sts' - sts1) j1 cpg2 j2)" by blast have "c2p (sts' - sts) i (CSeq cpg1 cpg2) j2" by(unfold hh(2), rule c2p_seq[OF h1 h2 hh(1)]) thus ?thesis by blast qed qednext case (CLocal body sts sts') from this(2) obtain b sts1 s where h: "wf_cpg_test (Free # sts) body = (True, sts1)" "sts' = tl sts1" by (unfold wf_cpg_test.simps, auto split:prod.splits) from wf_cpg_test_le[OF h(1), unfolded less_eq_list_def] h(2) obtain s where eq_sts1: "sts1 = s#sts'" by (metis Suc_length_conv list.size(4) tl.simps(2)) from CLocal(1)[OF h(1)] have p1: "\<forall>i. \<exists>a. c2p (sts1 - (Free # sts)) i body a" . show ?case proof fix i from p1[rule_format, of i] obtain j where "(c2p (sts1 - (Free # sts)) i body) j" by blast then obtain f where hh [rule_format]: "\<forall>x. length x = length (sts1 - (Free # sts)) \<and> (\<forall>k<length (sts1 - (Free # sts)). (sts1 - (Free # sts)) ! k = Bound \<longrightarrow> x ! k = f i k) \<longrightarrow> (\<exists>s. (i :[ c2t x body ]: j) s)" by (auto simp:c2p_def) let ?f = "\<lambda> i k. f i (Suc k)" have "\<exists>j f. \<forall>x. length x = length (sts' - sts) \<and> (\<forall>k<length (sts' - sts). (sts' - sts) ! k = Bound \<longrightarrow> x ! k = f i k) \<longrightarrow> (\<exists>s. (i :[ (TL xa. c2t (xa # x) body) ]: j) s)" proof(rule_tac x = j in exI, rule_tac x = ?f in exI, default, clarsimp) fix x assume h1: "length x = length (sts' - sts)" and h2: "\<forall>k<length (sts' - sts). (sts' - sts) ! k = Bound \<longrightarrow> x ! k = f i (Suc k)" let ?l = "f i 0" let ?x = " ?l#x" from wf_cpg_test_le[OF h(1)] have "length (Free#sts) = length sts1" by (unfold less_eq_list_def, simp) with h1 h(2) have q1: "length (?l # x) = length (sts1 - (Free # sts))" by (smt Suc_length_conv length_Suc_conv list.inject list.size(4) minus_list.simps(3) minus_list_len tl.simps(2)) have q2: "(\<forall>k<length (sts1 - (Free # sts)). (sts1 - (Free # sts)) ! k = Bound \<longrightarrow> (f i 0 # x) ! k = f i k)" proof - { fix k assume lt_k: "k<length (sts1 - (Free # sts))" and bd_k: "(sts1 - (Free # sts)) ! k = Bound" have "(f i 0 # x) ! k = f i k" proof(cases "k") case (Suc k') moreover have "x ! k' = f i (Suc k')" proof(rule h2[rule_format]) from bd_k Suc eq_sts1 show "(sts' - sts) ! k' = Bound" by simp next from Suc lt_k eq_sts1 show "k' < length (sts' - sts)" by simp qed ultimately show ?thesis by simp qed simp } thus ?thesis by auto qed from conjI[THEN hh[of ?x], OF q1 q2] obtain s where h_s: "(i :[ c2t (f i 0 # x) body ]: j) s" by blast thus "\<exists>s. (i :[ (TL xa. c2t (xa # x) body) ]: j) s" apply (simp add:tassemble_to.simps) by (rule_tac x = s in exI, rule_tac x = ?l in EXS_intro, simp) qed thus "\<exists>j. c2p (sts' - sts) i (CLocal body) j" by (auto simp:c2p_def) qedqedlemma assumes "wf_cpg_test [] cpg = (True, sts')" and "tpg = c2t [] cpg" shows "\<forall> i. \<exists> j s. ((i:[tpg]:j) s)"proof fix i have eq_sts_minus: "(sts' - []) = []" by (metis list.exhaust minus_list.simps(1) minus_list.simps(2)) from wf_cpg_test_correct[OF assms(1), rule_format, of i] obtain j where "c2p (sts' - []) i cpg j" by auto from c2p_assert [OF this[unfolded eq_sts_minus]] obtain s where "(i :[ c2t [] cpg ]: j) s" by blast from this[folded assms(2)] show " \<exists> j s. ((i:[tpg]:j) s)" by blastqedlemma replicate_nth: "(replicate n x @ sts) ! (l + n) = sts!l" by (smt length_replicate nth_append)lemma replicate_update: "(replicate n x @ sts)[l + n := v] = replicate n x @ sts[l := v]" by (smt length_replicate list_update_append)lemma l_n_v_orig: assumes "l0 < length env" and "t \<le> l0" shows "(take t env @ es @ drop t env) ! (l0 + length es) = env ! l0"proof - from assms(1, 2) have "t < length env" by auto hence h: "env = take t env @ drop t env" "length (take t env) = t" apply (metis append_take_drop_id) by (smt `t < length env` length_take) with assms(2) have eq_sts_l: "env!l0 = (drop t env)!(l0 - t)" by (metis nth_app) from h(2) have "length (take t env @ es) = t + length es" by (metis length_append length_replicate nat_add_commute) moreover from assms(2) have "t + (length es) \<le> l0 + (length es)" by auto ultimately have "((take t env @ es) @ drop t env)!(l0 + length es) = (drop t env)!(l0+ length es - (t + length es))" by (smt length_replicate length_splice nth_append) with eq_sts_l[symmetric, unfolded assms] show ?thesis by autoqedlemma l_n_v: assumes "l < length sts" and "sts!l = v" and "t \<le> l" shows "(take t sts @ replicate n x @ drop t sts) ! (l + n) = v"proof - from l_n_v_orig[OF assms(1) assms(3), of "replicate n x"] and assms(2) show ?thesis by autoqedlemma l_n_v_s: assumes "l < length sts" and "t \<le> l" shows "(take t sts @ sts0 @ drop t sts)[l + length sts0 := v] = take t (sts[l:=v])@ sts0 @ drop t (sts[l:=v])"proof - let ?n = "length sts0" from assms(1, 2) have "t < length sts" by auto hence h: "sts = take t sts @ drop t sts" "length (take t sts) = t" apply (metis append_take_drop_id) by (smt `t < length sts` length_take) with assms(2) have eq_sts_l: "sts[l:=v] = take t sts @ drop t sts [(l - t) := v]" by (smt list_update_append) with h(2) have eq_take_drop_t: "take t (sts[l:=v]) = take t sts" "drop t (sts[l:=v]) = (drop t sts)[l - t:=v]" apply (metis append_eq_conv_conj) by (metis append_eq_conv_conj eq_sts_l h(2)) from h(2) have "length (take t sts @ sts0) = t + ?n" by (metis length_append length_replicate nat_add_commute) moreover from assms(2) have "t + ?n \<le> l + ?n" by auto ultimately have "((take t sts @ sts0) @ drop t sts)[l + ?n := v] = (take t sts @ sts0) @ (drop t sts)[(l + ?n - (t + ?n)) := v]" by (smt list_update_append replicate_nth) with eq_take_drop_t show ?thesis by autoqedlemma l_n_v_s1: assumes "l < length sts" and "\<not> t \<le> l" shows "(take t sts @ sts0 @ drop t sts)[l := v] = take t (sts[l := v]) @ sts0 @ drop t (sts[l := v])"proof(cases "t < length sts") case False hence h: "take t sts = sts" "drop t sts = []" "take t (sts[l:=v]) = sts [l:=v]" "drop t (sts[l:=v]) = []" by auto with assms(1) show ?thesis by (metis list_update_append)next case True with assms(2) have h: "(take t sts)[l:=v] = take t (sts[l:=v])" "(sts[l:=v]) = (take t sts)[l:=v]@drop t sts" "length (take t sts) = t" apply (smt length_list_update length_take nth_equalityI nth_list_update nth_take) apply (smt True append_take_drop_id assms(2) length_take list_update_append1) by (smt True length_take) from h(2,3) have "drop t (sts[l := v]) = drop t sts" by (metis append_eq_conv_conj length_list_update) with h(1) show ?thesis apply simp by (metis assms(2) h(3) list_update_append1 not_leE)qedlemma l_n_v_s2: assumes "l0 < length env" and "t \<le> l0" and "\<not> t \<le> l1" shows "(take t env @ es @ drop t env) ! l1 = env ! l1"proof - from assms(1, 2) have "t < length env" by auto hence h: "env = take t env @ drop t env" "length (take t env) = t" apply (metis append_take_drop_id) by (smt `t < length env` length_take) with assms(3) show ?thesis by (smt nth_append)qedlemma l_n_v_s3: assumes "l0 < length env" and "\<not> t \<le> l0" shows "(take t env @ es @ drop t env) ! l0 = env ! l0"proof(cases "t < length env") case True hence h: "env = take t env @ drop t env" "length (take t env) = t" apply (metis append_take_drop_id) by (smt `t < length env` length_take) with assms(2) show ?thesis by (smt nth_append)next case False hence "take t env = env" by auto with assms(1) show ?thesis by (metis nth_append)qedlemma lift_wf_cpg_test: assumes "wf_cpg_test sts cpg = (True, sts')" shows "wf_cpg_test (take t sts @ sts0 @ drop t sts) (lift_t t (length sts0) cpg) = (True, take t sts' @ sts0 @ drop t sts')" using assmsproof(induct cpg arbitrary:t sts0 sts sts') case (CInstr instr t sts0 sts sts') obtain a0 l0 a1 l1 where eq_instr: "instr = ((a0, l0), (a1, l1))" by (metis prod.exhaust) from CInstr show ?case by (auto simp:eq_instr lift_b_def)next case (CLabel l t sts0 sts sts') thus ?case apply (auto simp:lift_b_def replicate_nth replicate_update l_n_v_orig l_n_v_s) apply (metis (mono_tags) diff_diff_cancel length_drop length_rev linear not_less nth_append nth_take rev_take take_all) by (simp add:l_n_v_s1)next case (CSeq c1 c2 sts0 sts sts') thus ?case by (auto simp: lift0_def lift_b_def split:prod.splits)next case (CLocal body t sts0 sts sts') from this(2) obtain sts1 where h: "wf_cpg_test (Free # sts) body = (True, sts1)" "tl sts1 = sts'" by (auto simp:lift0_def lift_b_def split:prod.splits) let ?lift_s = "\<lambda> t sts. take t sts @ sts0 @ drop t sts" have eq_lift_1: "(?lift_s (Suc t) (Free # sts)) = Free#?lift_s t sts" by (simp) from wf_cpg_test_le[OF h(1)] have "length (Free#sts) = length sts1" by (unfold less_eq_list_def, simp) hence eq_sts1: "sts1 = hd sts1 # tl sts1" by (metis append_Nil append_eq_conv_conj hd.simps list.exhaust tl.simps(2)) from CLocal(1)[OF h(1), of "Suc t", of "sts0", unfolded eq_lift_1] show ?case apply (simp, subst eq_sts1, simp) apply (simp add:h(2)) by (subst eq_sts1, simp add:h(2))qedlemma lift_c2t: assumes "wf_cpg_test sts cpg = (True, sts')" and "length env = length sts" shows "c2t (take t env @ es @ drop t env) (lift_t t (length es) cpg) = c2t env cpg" using assmsproof(induct cpg arbitrary: t env es sts sts') case (CInstr instr t env es sts sts') obtain a0 l0 a1 l1 where eq_instr: "instr = ((a0, l0), (a1, l1))" by (metis prod.exhaust) from CInstr have h: "l0 < length env" "l1 < length env" by (auto simp:eq_instr) with CInstr(2) show ?case by (auto simp:eq_instr lift_b_def l_n_v_orig l_n_v_s2 l_n_v_s3)next case (CLabel l t env es sts sts') thus ?case by (auto simp:lift_b_def replicate_nth replicate_update l_n_v_orig l_n_v_s3)next case (CSeq c1 c2 t env es sts sts') from CSeq(3) obtain sts1 where h: "wf_cpg_test sts c1 = (True, sts1)" "wf_cpg_test sts1 c2 = (True, sts')" by (auto split:prod.splits) from wf_cpg_test_le[OF h(1)] have "length sts = length sts1" by (auto simp:less_eq_list_def) from CSeq(4)[unfolded this] have eq_len_env: "length env = length sts1" . from CSeq(1)[OF h(1) CSeq(4)] CSeq(2)[OF h(2) eq_len_env] show ?case by (auto simp: lift0_def lift_b_def split:prod.splits)next case (CLocal body t env es sts sts') { fix x from CLocal(2) obtain sts1 where h1: "wf_cpg_test (Free # sts) body = (True, sts1)" by (auto split:prod.splits) from CLocal(3) have "length (x#env) = length (Free # sts)" by simp from CLocal(1)[OF h1 this, of "Suc t"] have "c2t (x # take t env @ es @ drop t env) (lift_t (Suc t) (length es) body) = c2t (x # env) body" by simp } thus ?case by simpqedpr 20lemma upto_append: assumes "x \<le> y + 1" shows "[x .. y + 1] = [x .. y]@[y + 1]" using assms by (induct x y rule:upto.induct, auto simp:upto.simps)lemma nth_upto: assumes "l < length sts" shows "[0..(int (length sts)) - 1]!l = int l" using assmsproof(induct sts arbitrary:l) case Nil thus ?case by simpnext case (Cons s sts l) from Cons(2) have "0 \<le> (int (length sts) - 1) + 1" by auto from upto_append[OF this] have eq_upto: "[0..int (length sts)] = [0..int (length sts) - 1] @ [int (length sts)]" by simp show ?case proof(cases "l < length sts") case True with Cons(1)[OF True] eq_upto show ?thesis apply simp by (smt nth_append take_eq_Nil upto_len) next case False with Cons(2) have eq_l: "l = length sts" by simp show ?thesis proof(cases sts) case (Cons x xs) have "[0..1 + int (length xs)] = [0 .. int (length xs)]@[1 + int (length xs)]" by (smt upto_append) moreover have "length [0 .. int (length xs)] = Suc (length xs)" by (smt upto_len) moreover note Cons ultimately show ?thesis apply (simp add:eq_l) by (smt nth_Cons' nth_append) qed (simp add:upto_len upto.simps eq_l) qedqedlemma map_idx_idx: assumes "l < length sts" shows "(map_idx f sts)!l = sts!(f l)"proof - from assms have lt_l: "l < length [0..int (length sts) - 1]" by (smt upto_len) show ?thesis apply (unfold map_idx_def nth_map[OF lt_l]) by (metis assms nat_int nth_upto)qedlemma map_idx_len: "length (map_idx f sts) = length sts" apply (unfold map_idx_def) by (smt length_map upto_len)lemma map_idx_eq: assumes "\<forall> l < length sts. f l = g l" shows "map_idx f sts = map_idx g sts"proof(induct rule: nth_equalityI) case 1 show "length (map_idx f sts) = length (map_idx g sts)" by (metis map_idx_len)next case 2 { fix l assume "l < length (map_idx f sts)" hence "l < length sts" by (metis map_idx_len) from map_idx_idx[OF this] and assms and this have "map_idx f sts ! l = map_idx g sts ! l" by (smt list_eq_iff_nth_eq map_idx_idx map_idx_len) } thus ?case by autoqedlemma perm_s_commut: "perm_s i j sts = perm_s j i sts" apply (unfold perm_s_def, rule map_idx_eq, unfold perm_b_def) by smtlemma map_idx_id: "map_idx id sts = sts"proof(induct rule:nth_equalityI) case 1 from map_idx_len show "length (map_idx id sts) = length sts" .next case 2 { fix l assume "l < length (map_idx id sts)" from map_idx_idx[OF this[unfolded map_idx_len]] have "map_idx id sts ! l = sts ! l" by simp } thus ?case by autoqedlemma perm_s_lt_i: assumes "\<not> i < length sts" shows "perm_s i j sts = sts"proof - have "map_idx (perm_b (length sts) i j) sts = map_idx id sts" proof(rule map_idx_eq, default, clarsimp) fix l assume "l < length sts" with assms show "perm_b (length sts) i j l = l" by (unfold perm_b_def, auto) qed with map_idx_id have "map_idx (perm_b (length sts) i j) sts = sts" by simp thus ?thesis by (simp add:perm_s_def)qedlemma perm_s_lt: assumes "\<not> i < length sts \<or> \<not> j < length sts" shows "perm_s i j sts = sts" using assmsproof assume "\<not> i < length sts" from perm_s_lt_i[OF this] show ?thesis .next assume "\<not> j < length sts" from perm_s_lt_i[OF this, of i, unfolded perm_s_commut] show ?thesis .qedlemma perm_s_update_i: assumes "i < length sts" and "j < length sts" shows "sts ! i = perm_s i j sts ! j"proof - from map_idx_idx[OF assms(2)] have "map_idx (perm_b (length sts) i j) sts ! j = sts!(perm_b (length sts) i j j)" . with assms show ?thesis by (auto simp:perm_s_def perm_b_def)qedlemma nth_perm_s_neq: assumes "l \<noteq> j" and "l \<noteq> i" and "l < length sts" shows "sts ! l = perm_s i j sts ! l"proof - have "map_idx (perm_b (length sts) i j) sts ! l = sts!(perm_b (length sts) i j l)" by (metis assms(3) map_idx_def map_idx_idx) with assms show ?thesis by (unfold perm_s_def perm_b_def, auto)qedlemma map_idx_update: assumes "f j = i" and "inj f" and "i < length sts" and "j < length sts" shows "map_idx f (sts[i:=v]) = map_idx f sts[j := v]"proof(induct rule:nth_equalityI) case 1 show "length (map_idx f (sts[i := v])) = length (map_idx f sts[j := v])" by (metis length_list_update map_idx_len)next case 2 { fix l assume lt_l: "l < length (map_idx f (sts[i := v]))" have eq_nth: "sts[i := v] ! f l = map_idx f sts[j := v] ! l" proof(cases "f l = i") case False from lt_l have "l < length sts" by (metis length_list_update map_idx_len) from map_idx_idx[OF this, of f] have " map_idx f sts ! l = sts ! f l" . moreover from False assms have "l \<noteq> j" by auto moreover note False ultimately show ?thesis by simp next case True with assms have eq_l: "l = j" by (metis inj_eq) moreover from lt_l eq_l have "j < length (map_idx f sts[j := v])" by (metis length_list_update map_idx_len) moreover note True assms ultimately show ?thesis by simp qed from lt_l have "l < length (sts[i := v])" by (metis map_idx_len) from map_idx_idx[OF this] eq_nth have "map_idx f (sts[i := v]) ! l = map_idx f sts[j := v] ! l" by simp } thus ?case by autoqedlemma perm_s_update: assumes "i < length sts" and "j < length sts" shows "(perm_s i j sts)[i := v] = perm_s i j (sts[j := v])"proof - have "map_idx (perm_b (length (sts[j := v])) i j) (sts[j := v]) = map_idx (perm_b (length (sts[j := v])) i j) sts[i := v]" proof(rule map_idx_update[OF _ _ assms(2, 1)]) from inj_perm_b show "inj (perm_b (length (sts[j := v])) i j)" . next from assms show "perm_b (length (sts[j := v])) i j i = j" by (auto simp:perm_b_def) qed hence "map_idx (perm_b (length sts) i j) sts[i := v] = map_idx (perm_b (length (sts[j := v])) i j) (sts[j := v])" by simp thus ?thesis by (simp add:perm_s_def)qedlemma perm_s_update_neq: assumes "l \<noteq> i" and "l \<noteq> j" shows "perm_s i j sts[l := v] = perm_s i j (sts[l := v])"proof(cases "i < length sts \<and> j < length sts") case False with perm_s_lt have "perm_s i j sts = sts" by auto moreover have "perm_s i j (sts[l:=v]) = sts[l:=v]" proof - have "length (sts[l:=v]) = length sts" by auto from False[folded this] perm_s_lt show ?thesis by metis qed ultimately show ?thesis by simpnext case True note lt_ij = this show ?thesis proof(cases "l < length sts") case False hence "sts[l:=v] = sts" by auto moreover have "perm_s i j sts[l := v] = perm_s i j sts" proof - from False and perm_s_len have "\<not> l < length (perm_s i j sts)" by metis thus ?thesis by auto qed ultimately show ?thesis by simp next case True show ?thesis proof - have "map_idx (perm_b (length (sts[l := v])) i j) (sts[l := v]) = map_idx (perm_b (length (sts[l := v])) i j) sts[l := v]" proof(induct rule:map_idx_update [OF _ inj_perm_b True True]) case 1 from assms lt_ij show ?case by (unfold perm_b_def, auto) qed thus ?thesis by (unfold perm_s_def, simp) qed qedqedlemma perm_sb: "(perm_s i j sts)[perm_b (length sts) i j l := v] = perm_s i j (sts[l := v])" apply(subst perm_b_def, auto simp:perm_s_len perm_s_lt perm_s_update) apply (subst perm_s_commut, subst (2) perm_s_commut, rule_tac perm_s_update, auto) by (rule_tac perm_s_update_neq, auto)lemma perm_s_id: "perm_s i i sts = sts" (is "?L = ?R")proof - from map_idx_id have "?R = map_idx id sts" by metis also have "\<dots> = ?L" by (unfold perm_s_def, rule map_idx_eq, unfold perm_b_def, auto) finally show ?thesis by simpqedlemma upto_map: assumes "i \<le> j" shows "[i .. j] = i # map (\<lambda> x. x + 1) [i .. (j - 1)]" using assmsproof(induct i j rule:upto.induct) case (1 i j) show ?case (is "?L = ?R") proof - from 1(2) have eq_l: "?L = i # [i+1 .. j]" by (simp add:upto.simps) show ?thesis proof(cases "i + 1 \<le> j") case False with eq_l show ?thesis by (auto simp:upto.simps) next case True have "[i + 1..j] = map (\<lambda>x. x + 1) [i..j - 1]" by (smt "1.hyps" Cons_eq_map_conv True upto.simps) with eq_l show ?thesis by simp qed qedqedlemma perm_s_cons: "(perm_s (Suc i) (Suc j) (s # sts)) = s#perm_s i j sts"proof - have le_0: "0 \<le> int (length (s # sts)) - 1" by simp have "map (\<lambda>k. (s # sts) ! perm_b (length (s # sts)) (Suc i) (Suc j) (nat k)) [0..int (length (s # sts)) - 1] = s # map (\<lambda>k. sts ! perm_b (length sts) i j (nat k)) [0..int (length sts) - 1]" by (unfold upto_map[OF le_0], auto simp:perm_b_def, smt+) thus ?thesis by (unfold perm_s_def map_idx_def, simp)qedlemma perm_wf_cpg_test: assumes "wf_cpg_test sts cpg = (True, sts')" shows "wf_cpg_test (perm_s i j sts) (perm (length sts) i j cpg) = (True, perm_s i j sts')" using assmsproof(induct cpg arbitrary:t i j sts sts') case (CInstr instr i j sts sts') obtain a0 l0 a1 l1 where eq_instr: "instr = ((a0, l0), (a1, l1))" by (metis prod.exhaust) from CInstr show ?case apply (unfold eq_instr, clarsimp) by (unfold perm_s_len perm_b_def, clarsimp)next case (CLabel l i j sts sts') have "(perm_s i j sts)[perm_b (length sts) i j l := Bound] = perm_s i j (sts[l := Bound])" by (metis perm_sb) with CLabel show ?case apply (auto simp:perm_s_len perm_sb) apply (subst perm_b_def, auto simp:perm_sb) apply (subst perm_b_def, auto simp:perm_s_lt perm_s_update_i) apply (unfold perm_s_id, subst perm_s_commut, simp add: perm_s_update_i[symmetric]) apply (simp add:perm_s_update_i[symmetric]) by (simp add: nth_perm_s_neq[symmetric])next case (CSeq c1 c2 i j sts sts') thus ?case apply (auto split:prod.splits) apply (metis (hide_lams, no_types) less_eq_list_def prod.inject wf_cpg_test_le) by (metis (hide_lams, no_types) less_eq_list_def prod.inject wf_cpg_test_le)next case (CLocal body i j sts sts') from this(2) obtain sts1 where h: "wf_cpg_test (Free # sts) body = (True, sts1)" "tl sts1 = sts'" by (auto simp:lift0_def lift_b_def split:prod.splits) from wf_cpg_test_le[OF h(1)] have "length (Free#sts) = length sts1" by (unfold less_eq_list_def, simp) hence eq_sts1: "sts1 = hd sts1 # tl sts1" by (metis append_Nil append_eq_conv_conj hd.simps list.exhaust tl.simps(2)) from CLocal(1)[OF h(1), of "Suc i" "Suc j"] h(2) eq_sts1 show ?case apply (auto split:prod.splits simp:perm_s_cons) by (metis perm_s_cons tl.simps(2))qedlemma nth_perm_sb: assumes "l0 < length env" shows "perm_s i j env ! perm_b (length env) i j l0 = env ! l0" by (metis assms nth_perm_s_neq perm_b_def perm_s_commut perm_s_lt perm_s_update_i)lemma perm_c2t: assumes "wf_cpg_test sts cpg = (True, sts')" and "length env = length sts" shows "c2t (perm_s i j env) (perm (length env) i j cpg) = c2t env cpg" using assmsproof(induct cpg arbitrary:i j env sts sts') case (CInstr instr i j env sts sts') obtain a0 l0 a1 l1 where eq_instr: "instr = ((a0, l0), (a1, l1))" by (metis prod.exhaust) from CInstr have h: "l0 < length env" "l1 < length env" by (auto simp:eq_instr) with CInstr(2) show ?case apply (auto simp:eq_instr) by (metis nth_perm_sb)+next case (CLabel l t env es sts sts') thus ?case apply (auto) by (metis nth_perm_sb)next case (CSeq c1 c2 i j env sts sts') from CSeq(3) obtain sts1 where h: "wf_cpg_test sts c1 = (True, sts1)" "wf_cpg_test sts1 c2 = (True, sts')" by (auto split:prod.splits) from wf_cpg_test_le[OF h(1)] have "length sts = length sts1" by (auto simp:less_eq_list_def) from CSeq(4)[unfolded this] have eq_len_env: "length env = length sts1" . from CSeq(1)[OF h(1) CSeq(4)] CSeq(2)[OF h(2) eq_len_env] show ?case by autonext case (CLocal body i j env sts sts') { fix x from CLocal(2, 3) obtain sts1 where "wf_cpg_test (Free # sts) body = (True, sts1)" "length (x#env) = length (Free # sts)" by (auto split:prod.splits) from CLocal(1)[OF this] have "(c2t (x # perm_s i j env) (perm (Suc (length env)) (Suc i) (Suc j) body)) = (c2t (x # env) body)" by (metis Suc_length_conv perm_s_cons) } thus ?case by simpqedlemma wf_cpg_test_disj_aux1: assumes "sts_disj sts1 (sts[l := Bound] - sts)" "l < length sts" "sts ! l = Free" shows "(sts1 + sts) ! l = Free"proof - from assms(1)[unfolded sts_disj_def] have h: "length sts1 = length (sts[l := Bound] - sts)" "(\<forall>i<length sts1. \<not> (sts1 ! i = Bound \<and> (sts[l := Bound] - sts) ! i = Bound))" by auto from h(1) assms(2) have lt_l: "l < length sts1" "l < length (sts[l := Bound] - sts)" "l < length (sts1 + sts)" apply (smt length_list_update minus_list_len) apply (smt assms(2) length_list_update minus_list_len) by (smt assms(2) h(1) length_list_update length_sts_plus minus_list_len) from h(2)[rule_format, of l, OF this(1)] have " \<not> (sts1 ! l = Bound \<and> (sts[l := Bound] - sts) ! l = Bound)" . with assms(3) nth_sts_minus[OF lt_l(2)] nth_sts_plus[OF lt_l(3)] assms(2) show ?thesis by (cases "sts1!l", auto)qedlemma wf_cpg_test_disj_aux2: assumes "sts_disj sts1 (sts[l := Bound] - sts)" " l < length sts" shows "(sts1 + sts)[l := Bound] = sts1 + sts[l := Bound]"proof - from assms have lt_l: "l < length (sts1 + sts[l:=Bound])" "l < length (sts1 + sts)" apply (smt length_list_update length_sts_plus minus_list_len sts_disj_def) by (smt assms(1) assms(2) length_list_update length_sts_plus minus_list_len sts_disj_def) show ?thesis proof(induct rule:nth_equalityI) case 1 show ?case by (smt assms(1) length_list_update length_sts_plus minus_list_len sts_disj_def) next case 2 { fix i assume lt_i: "i < length ((sts1 + sts)[l := Bound])" have " (sts1 + sts)[l := Bound] ! i = (sts1 + sts[l := Bound]) ! i" proof(cases "i = l") case True with nth_sts_plus[OF lt_l(1)] assms(2) nth_sts_plus[OF lt_l(2)] lt_l show ?thesis by (cases "sts1 ! l", auto) next case False from lt_i have "i < length (sts1 + sts)" "i < length (sts1 + sts[l := Bound])" apply auto by (metis length_list_update plus_list_len) from nth_sts_plus[OF this(1)] nth_sts_plus[OF this(2)] lt_i lt_l False show ?thesis by simp qed } thus ?case by auto qedqedlemma sts_list_plus_commut: shows "sts1 + sts2 = sts2 + (sts1:: status list)"proof(induct rule:nth_equalityI) case 1 show ?case by (metis min.commute plus_list_len)next case 2 { fix i assume lt_i1: "i<length (sts1 + sts2)" hence lt_i2: "i < length (sts2 + sts1)" by (smt plus_list_len) from nth_sts_plus[OF this] nth_sts_plus[OF lt_i1] have "(sts1 + sts2) ! i = (sts2 + sts1) ! i" apply simp apply (cases "sts1!i", cases "sts2!i", auto) by (cases "sts2!i", auto) } thus ?case by autoqedlemma sts_disj_cons: assumes "sts_disj sts1 sts2" shows "sts_disj (Free # sts1) (s # sts2)" using assmsproof - from assms have h: "length sts1 = length sts2" "(\<forall>i<length sts1. \<not> (sts1 ! i = Bound \<and> sts2 ! i = Bound))" by (unfold sts_disj_def, auto) from h(1) have "length (Free # sts1) = length (s # sts2)" by simp moreover { fix i assume lt_i: "i<length (Free # sts1)" have "\<not> ((Free # sts1) ! i = Bound \<and> (s # sts2) ! i = Bound)" proof(cases "i") case 0 thus ?thesis by simp next case (Suc k) from h(2)[rule_format, of k] lt_i[unfolded Suc] Suc show ?thesis by auto qed } ultimately show ?thesis by (auto simp:sts_disj_def)qedlemma sts_disj_uncomb: assumes "sts_disj sts (sts1 + sts2)" and "sts_disj sts1 sts2" shows "sts_disj sts sts1" "sts_disj sts sts2" using assms apply (smt assms(1) assms(2) length_sts_plus nth_sts_plus plus_status.simps(2) sts_disj_def) by (smt assms(1) assms(2) length_sts_plus nth_sts_plus plus_status.simps(2) sts_disj_def sts_list_plus_commut)lemma wf_cpg_test_disj: assumes "wf_cpg_test sts cpg = (True, sts')" and "sts_disj sts1 (sts' - sts)" shows "wf_cpg_test (sts1 + sts) cpg = (True, sts1 + sts')" using assmsproof(induct cpg arbitrary:sts sts1 sts') case (CInstr instr sts sts1 sts') obtain a0 l0 a1 l1 where eq_instr: "instr = ((a0, l0), (a1, l1))" by (metis pair_collapse) with CInstr(1) have h: "l0 < length sts" "l1 < length sts" "sts = sts'" by auto with CInstr eq_instr show ?case apply (auto) by (smt length_sts_plus minus_list_len sts_disj_def)+next case (CLabel l sts sts1 sts') thus ?case apply auto apply (smt length_list_update length_sts_plus minus_list_len sts_disj_def) by (auto simp: wf_cpg_test_disj_aux1 wf_cpg_test_disj_aux2)next case (CSeq c1 c2 sts sts1 sts') from CSeq(3) obtain sts'' where h: "wf_cpg_test sts c1 = (True, sts'')" "wf_cpg_test sts'' c2 = (True, sts')" by (auto split:prod.splits) from wf_cpg_test_le[OF h(1)] have "length sts = length sts''" by (auto simp:less_eq_list_def) from sts_le_comb[OF wf_cpg_test_le[OF h(1)] wf_cpg_test_le[OF h(2)]] have " sts' - sts = (sts'' - sts) + (sts' - sts'')" "sts_disj (sts'' - sts) (sts' - sts'')" by auto from sts_disj_uncomb[OF CSeq(4)[unfolded this(1)] this(2)] have "sts_disj sts1 (sts'' - sts)" "sts_disj sts1 (sts' - sts'')" . from CSeq(1)[OF h(1) this(1)] CSeq(2)[OF h(2) this(2)] have "wf_cpg_test (sts1 + sts) c1 = (True, sts1 + sts'')" "wf_cpg_test (sts1 + sts'') c2 = (True, sts1 + sts')" . thus ?case by simpnext case (CLocal body sts sts1 sts') from this(2) obtain sts'' where h: "wf_cpg_test (Free # sts) body = (True, sts'')" "sts' = tl sts''" by (auto split:prod.splits) from wf_cpg_test_le[OF h(1), unfolded less_eq_list_def] h(2) obtain s where eq_sts'': "sts'' = s#sts'" by (metis Suc_length_conv list.size(4) tl.simps(2)) let ?sts = "Free#sts1" from CLocal(3) have "sts_disj ?sts (sts'' - (Free # sts))" apply (unfold eq_sts'', simp) by (metis sts_disj_cons) from CLocal(1)[OF h(1) this] eq_sts'' show ?case by (auto split:prod.splits)qedsection {* Application of the theory above *}definition "move_left_skel = CLocal (CSeq (CInstr ((L, 0), (L, 0))) (CLabel 0))"lemma wt_move_left: "wf_cpg_test [] move_left_skel = (True, [])" by (unfold move_left_skel_def, simp)lemma ct_move_left: "c2t [] move_left_skel = move_left" by (unfold move_left_skel_def move_left_def, simp)lemma wf_move_left: "\<forall> i. \<exists> s j. (i:[move_left]:j ) s"proof - from wf_cpg_test_correct[OF wt_move_left] ct_move_left show ?thesis by (unfold c2p_def, simp, metis)qeddefinition "jmp_skel = CInstr ((W0, 0), (W1, 0))"lemma wt_jmp: "wf_cpg_test [Free] jmp_skel = (True, [Free])" by (unfold jmp_skel_def, simp)lemma ct_jmp: "c2t [l] jmp_skel = (jmp l)" by (unfold jmp_skel_def jmp_def, simp)lemma wf_jmp: "\<forall> i. \<exists> s j. (i:[jmp l]:j ) s"proof - from wf_cpg_test_correct[OF wt_jmp] ct_jmp show ?thesis apply (unfold c2p_def, simp) by (metis One_nat_def Suc_eq_plus1 list.size(3) list.size(4))qeddefinition "label_skel = CLabel 0"lemma wt_label: "wf_cpg_test [Free] label_skel = (True, [Bound])" by (simp add:label_skel_def)lemma ct_label: "c2t [l] label_skel = (TLabel l)" by (simp add:label_skel_def)thm if_zero_defdefinition "if_zero_skel = CLocal (CSeq (CInstr ((W0, 1), (W1, 0))) ( CLabel 0 ) )"lemma wt_if_zero: "wf_cpg_test [Free] if_zero_skel = (True, [Free])" by (simp add:if_zero_skel_def)definition "left_until_zero_skel = CLocal (CLocal ( CSeq (CLabel 1) ( CSeq if_zero_skel ( CSeq move_left_skel ( CSeq (lift_t 0 1 jmp_skel) ( label_skel )))) ))"lemma w1: "wf_cpg_test [Free, Bound] if_zero_skel = (True, [Free, Bound])" by (simp add:if_zero_skel_def)lemma w2: "wf_cpg_test [Free, Bound] move_left_skel = (True, [Free, Bound])" by (simp add:move_left_skel_def)lemma w3: "wf_cpg_test [Free, Bound] (lift_t 0 (Suc 0) jmp_skel) = (True, [Free, Bound])" by (simp add:jmp_skel_def lift_b_def)lemma w4: "wf_cpg_test [Free, Bound] label_skel = (True, [Bound, Bound])" by (unfold label_skel_def, simp)lemma wt_left_until_zero: "wf_cpg_test [] left_until_zero_skel = (True, [])" by (unfold left_until_zero_skel_def, simp add:w1 w2 w3 w4)lemma c1: "c2t [xa, x] if_zero_skel = if_zero xa" by (simp add:if_zero_skel_def if_zero_def)lemma c2: "c2t [xa, x] move_left_skel = move_left" by (simp add:move_left_skel_def move_left_def)lemma c3: "c2t [xa, x] (lift_t 0 (Suc 0) jmp_skel) = jmp x" by (simp add:jmp_skel_def jmp_def lift_b_def)lemma c4: "c2t [xa, x] label_skel = TLabel xa" by (simp add:label_skel_def)lemma ct_left_until_zero: "c2t [] left_until_zero_skel = left_until_zero" apply (unfold left_until_zero_def left_until_zero_skel_def) by (simp add:c1 c2 c3 c4)lemma wf_left_until_zero: "\<forall> i. \<exists> s j. (i:[left_until_zero]:j) s"proof - from wf_cpg_test_correct[OF wt_left_until_zero] ct_left_until_zero show ?thesis apply (unfold c2p_def, simp) by metisqedend