--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/TM_Assemble.thy Fri Mar 21 21:40:51 2014 +0800
@@ -0,0 +1,1885 @@
+theory TM_Assemble
+imports Hoare_tm StateMonad AList
+ "~~/src/HOL/Library/FinFun_Syntax"
+ "~~/src/HOL/Library/Sublist"
+ LetElim
+begin
+
+section {* 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
+ qed
+qed
+
+
+lemma 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 auto
+qed
+
+definition "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 cpg
+
+datatype status = Free | Bound
+
+definition "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)
+qed
+
+fun 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)
+ oops
+
+lemma 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)
+ qed
+qed
+
+lemma 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 :: minus
+begin
+ 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 ..
+end
+
+instantiation status :: plus
+begin
+ fun plus_status :: "status \<Rightarrow> status \<Rightarrow> status" where
+ "plus_status Free x = x" |
+ "plus_status Bound x = Bound"
+ instance ..
+end
+
+instantiation list :: (plus)plus
+begin
+ 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 ..
+end
+
+instantiation list :: (minus)minus
+begin
+ 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 :: order
+begin
+ 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)"
+instance
+proof
+ 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))
+qed
+end
+
+instantiation list :: (order)order
+begin
+ 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
+ qed
+end
+
+lemma 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)
+qed
+
+lemma 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)
+qed
+
+lemma wf_cpg_test_le:
+ assumes "wf_cpg_test sts cpg = (True, sts')"
+ shows "sts \<le> sts'" using assms
+proof(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 simp
+next
+ 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))
+qed
+
+lemma 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 auto
+qed
+
+definition "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 assms
+proof(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))
+ qed
+qed
+
+
+lemma nth_sts_plus:
+ assumes "i < length ((sts1::status list) + sts2)"
+ shows "(sts1 + sts2)!i = sts1!i + sts2!i"
+ using assms
+proof(induct sts1 arbitrary:i sts2)
+ case (Nil i sts2)
+ thus ?case by auto
+next
+ 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))
+ qed
+qed
+
+lemma nth_sts_minus:
+ assumes "i < length ((sts1::status list) - sts2)"
+ shows "(sts1 - sts2)!i = sts1!i - sts2!i"
+ using assms
+proof(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
+ qed
+qed auto
+
+fun 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 assms
+proof(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))
+ qed
+next
+ 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 auto
+qed
+
+lemma 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)
+qed
+
+lemma 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 auto
+qed
+
+lemma wf_cpg_test_correct:
+ assumes "wf_cpg_test sts cpg = (True, sts')"
+ shows "(\<forall> i. \<exists> j. (c2p (sts' - sts) i cpg j))"
+ using assms
+proof(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
+ qed
+next
+ 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_max.inf.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)
+ qed
+next
+ 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
+ qed
+next
+ 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)
+ qed
+qed
+
+lemma
+ 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 blast
+qed
+
+lemma 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 auto
+qed
+
+lemma 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 auto
+qed
+
+lemma 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 auto
+qed
+
+lemma 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)
+qed
+
+lemma 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)
+qed
+
+lemma 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)
+qed
+
+lemma 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 assms
+proof(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))
+qed
+
+lemma 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 assms
+proof(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 simp
+qed
+
+pr 20
+
+lemma 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 assms
+proof(induct sts arbitrary:l)
+ case Nil
+ thus ?case by simp
+next
+ 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)
+ qed
+qed
+
+lemma 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)
+qed
+
+lemma 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 auto
+qed
+
+lemma 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 smt
+
+lemma 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 auto
+qed
+
+lemma 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)
+qed
+
+lemma perm_s_lt:
+ assumes "\<not> i < length sts \<or> \<not> j < length sts"
+ shows "perm_s i j sts = sts"
+ using assms
+proof
+ 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 .
+qed
+
+lemma 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)
+qed
+
+lemma 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)
+qed
+
+lemma 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 auto
+qed
+
+lemma 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)
+qed
+
+lemma 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 simp
+next
+ 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
+ qed
+qed
+
+lemma 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 simp
+qed
+
+lemma upto_map:
+ assumes "i \<le> j"
+ shows "[i .. j] = i # map (\<lambda> x. x + 1) [i .. (j - 1)]"
+ using assms
+proof(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
+ qed
+qed
+
+lemma 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)
+qed
+
+lemma 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 assms
+proof(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))
+qed
+
+lemma 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 assms
+proof(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 auto
+next
+ 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 simp
+qed
+
+lemma 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)
+qed
+
+lemma 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
+ qed
+qed
+
+lemma sts_list_plus_commut:
+ shows "sts1 + sts2 = sts2 + (sts1:: status list)"
+proof(induct rule:nth_equalityI)
+ case 1
+ show ?case
+ by (metis min_max.inf.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 auto
+qed
+
+lemma sts_disj_cons:
+ assumes "sts_disj sts1 sts2"
+ shows "sts_disj (Free # sts1) (s # sts2)"
+ using assms
+proof -
+ 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)
+qed
+
+lemma 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 assms
+proof(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 simp
+next
+ 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)
+qed
+
+section {* 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)
+qed
+
+definition "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))
+qed
+
+definition "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_def
+
+definition "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 metis
+qed
+
+end
\ No newline at end of file