diff -r 545fef826fa9 -r ceb0bdc99893 thys/TM_Assemble.thy
--- /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