1 theory TM_Assemble

     2 imports Hoare_tm StateMonad AList 

     3         "~~/src/HOL/Library/FinFun_Syntax"

     4         "~~/src/HOL/Library/Sublist"

     5         LetElim

     6 begin

     7 

     8 section {* The assembler based on Benton's x86 paper *}

     9 

    10 text {*

    11   The problem with the assembler is that it is too slow to be useful.

    12 *}

    13 

    14 primrec pass1 :: "tpg \<Rightarrow> (unit, (nat \<times> nat \<times> (nat \<rightharpoonup> nat))) SM" 

    15   where 

    16   "pass1 (TInstr ai) = sm_map (\<lambda> (pos, lno, lmap). (pos + 1, lno, lmap))" |

    17   "pass1 (TSeq p1 p2) = do {pass1 p1; pass1 p2 }" |

    18   "pass1 (TLocal fp) = do { lno \<leftarrow> tap (\<lambda> (pos, lno, lmap). lno); 

    19                             sm_map (\<lambda> (pos, lno, lmap). (pos, lno+1, lmap)); 

    20                             pass1 (fp lno) }" |

    21   "pass1 (TLabel l) = sm_map ((\<lambda> (pos, lno, lmap). (pos, lno, lmap(l \<mapsto> pos))))"

    22 

    23 declare pass1.simps[simp del]

    24 

    25 type_synonym ('a, 'b) alist = "('a \<times> 'b) list"

    26 

    27 primrec pass2 :: "tpg \<Rightarrow> (nat \<rightharpoonup> nat) \<Rightarrow> (unit, (nat \<times> nat \<times> (nat, tm_inst) alist)) SM" 

    28   where

    29   "pass2 (TInstr ai) lmap = sm_map (\<lambda> (pos, lno, prog). (pos + 1, lno, (pos, ai)#prog))" |

    30   "pass2 (TSeq p1 p2) lmap = do {pass2 p1 lmap; pass2 p2 lmap}" |

    31   "pass2 (TLocal fp) lmap = do { lno \<leftarrow> tap (\<lambda> (pos, lno, prog). lno);

    32                                  sm_map (\<lambda> (pos, lno, prog). (pos, lno + 1, prog));

    33                                  (case (lmap lno) of

    34                                     Some l => pass2 (fp l) lmap |

    35                                     None => (raise ''Undefined label''))} " |

    36   "pass2 (TLabel l) lmap = do { pos \<leftarrow> tap (\<lambda> (pos, lno, prog). pos);

    37                                 if (l = pos) then return ()

    38                                              else (raise ''Label mismatch'') }"

    39 declare pass2.simps[simp del]

    40 

    41 definition "assembleM i tpg = 

    42   do {(x, (pos, lno, lmap)) \<leftarrow> execute (pass1 tpg) (i, 0, empty);

    43       execute (pass2 tpg lmap) (i, 0, [])}"

    44 

    45 definition 

    46  "assemble i tpg = Option.map (\<lambda> (x, (j, lno, prog)).(prog, j)) (assembleM i tpg)"

    47 

    48 

    49 lemma tprog_set_union:

    50   assumes "(fst ` set pg3) \<inter> (fst ` set pg2) = {}"

    51   shows "tprog_set (map_of pg3 ++ map_of pg2) = tprog_set (map_of pg3) \<union> tprog_set (map_of pg2)"

    52 proof -

    53   from assms have "dom (map_of pg3) \<inter> dom (map_of pg2) = {}"

    54     by (metis dom_map_of_conv_image_fst)

    55   hence map_comm: "map_of pg3 ++ map_of pg2 = map_of pg2 ++ map_of pg3"

    56     by (metis map_add_comm)

    57   show ?thesis

    58   proof

    59     show "tprog_set (map_of pg3 ++ map_of pg2) \<subseteq> tprog_set (map_of pg3) \<union> tprog_set (map_of pg2)"

    60     proof

    61       fix x

    62       assume " x \<in> tprog_set (map_of pg3 ++ map_of pg2)"

    63       then obtain i inst where h:

    64             "x = TC i inst"

    65             "(map_of pg3 ++ map_of pg2) i = Some inst"

    66         apply (unfold tprog_set_def)

    67         by (smt mem_Collect_eq)

    68       from map_add_SomeD[OF h(2)] h(1)

    69       show " x \<in> tprog_set (map_of pg3) \<union> tprog_set (map_of pg2)"

    70         apply (unfold tprog_set_def)

    71         by (smt mem_Collect_eq sup1CI sup_Un_eq)

    72     qed

    73   next

    74     show "tprog_set (map_of pg3) \<union> tprog_set (map_of pg2) \<subseteq> tprog_set (map_of pg3 ++ map_of pg2)"

    75     proof

    76       fix x

    77       assume " x \<in> tprog_set (map_of pg3) \<union> tprog_set (map_of pg2)"

    78       then obtain i inst

    79         where h: "x = TC i inst" "map_of pg3 i = Some inst \<or> map_of pg2 i = Some inst"

    80         apply (unfold tprog_set_def)

    81         by (smt Un_iff mem_Collect_eq)

    82       from h(2)

    83       show "x \<in> tprog_set (map_of pg3 ++ map_of pg2)"

    84       proof

    85         assume "map_of pg2 i = Some inst"

    86         hence "(map_of pg3 ++ map_of pg2) i = Some inst"

    87           by (metis map_add_find_right)

    88         with h(1) show ?thesis 

    89           apply (unfold tprog_set_def)

    90           by (smt mem_Collect_eq)

    91       next

    92         assume "map_of pg3 i = Some inst"

    93         hence "(map_of pg2 ++ map_of pg3) i = Some inst"

    94           by (metis map_add_find_right)

    95         with h(1) show ?thesis

    96           apply (unfold map_comm)

    97           apply (unfold tprog_set_def)

    98           by (smt mem_Collect_eq)

    99       qed

   100     qed

   101   qed

   102 qed

   103 

   104 

   105 lemma assumes "assemble i c = Some (prog, j)"

   106   shows "(i:[c]:j) (tprog_set (map_of prog))"

   107 proof -

   108   from assms obtain x lno

   109     where "(assembleM i c) = Some (x, (j, lno, prog))"

   110     apply(unfold assemble_def)

   111     by (cases "(assembleM i c)", auto)

   112   then obtain y pos lno' lmap where

   113        "execute (pass1 c) (i, 0, empty) = Some (y, (pos, lno', lmap))"

   114        "execute (pass2 c lmap) (i, 0, []) = Some (x, (j, lno, prog))"

   115     apply (unfold assembleM_def)

   116     by (cases "execute (pass1 c) (i, 0, Map.empty)", auto simp:Option.bind.simps)

   117   hence mid: "effect (pass1 c) (i, 0, empty) (pos, lno', lmap) y"

   118              "effect (pass2 c lmap) (i, 0, []) (j, lno, prog) x"

   119     by (auto intro:effectI)

   120   { fix lnos lmap lmap' prog1 prog2

   121     assume "effect (pass2 c lmap') (i, lnos, prog1) (j, lno, prog2) x"

   122     hence "\<exists> prog. (prog2 = prog@prog1 \<and> (i:[c]:j) (tprog_set (map_of prog)) \<and>

   123                    (\<forall> k \<in> fst ` (set prog). i \<le> k \<and> k < j) \<and> i \<le> j)" 

   124     proof(induct c arbitrary:lmap' i lnos prog1 j lno prog2 x)

   125       case  (TInstr instr lmap' i lnos prog1 j lno prog2 x)

   126       thus ?case

   127         apply (auto simp: effect_def assemble_def assembleM_def execute.simps sm_map_def sm_def 

   128                     tprog_set_def tassemble_to.simps sg_def pass1.simps pass2.simps

   129                      split:if_splits)

   130         by (cases instr, auto)

   131     next

   132       case (TLabel l lmap' i lnos prog1 j lno prog2 x)

   133       thus ?case 

   134         apply (rule_tac x = "[]" in exI)

   135         apply (unfold tassemble_to.simps)

   136         by (auto simp: effect_def assemble_def assembleM_def execute.simps sm_map_def sm_def 

   137                     tprog_set_def tassemble_to.simps sg_def pass1.simps pass2.simps tap_def bind_def

   138                     return_def raise_def sep_empty_def set_ins_def

   139                      split:if_splits)

   140     next

   141       case (TSeq c1 c2 lmap' i lnos prog1 j lno prog2 x)

   142       from TSeq(3)

   143       obtain h' r where 

   144         "effect (pass2 c1 lmap') (i, lnos, prog1) h' r"

   145         "effect (pass2 c2 lmap') h' (j, lno, prog2) x"

   146         apply (unfold pass2.simps)

   147         by (auto elim!:effect_elims)

   148       then obtain pos1 lno1 pg1

   149         where h:

   150         "effect (pass2 c1 lmap') (i, lnos, prog1) (pos1, lno1, pg1) r"

   151         "effect (pass2 c2 lmap') (pos1, lno1, pg1) (j, lno, prog2) x"

   152         by (cases h', auto)

   153       from TSeq(1)[OF h(1)] TSeq(2)[OF h(2)]

   154       obtain pg2 pg3

   155         where hh: "pg1 = pg2 @ prog1 \<and> (i :[ c1 ]: pos1) (tprog_set (map_of pg2))"

   156                   "(\<forall>k\<in> fst ` (set pg2). i \<le> k \<and> k < pos1)"

   157                   "i \<le> pos1"

   158                   "prog2 = pg3 @ pg1 \<and> (pos1 :[ c2 ]: j) (tprog_set (map_of pg3))"

   159                   "(\<forall>k\<in>fst ` (set pg3). pos1 \<le> k \<and> k < j)"

   160                   "pos1 \<le> j"

   161         by auto

   162       thus ?case

   163         apply (rule_tac x = "pg3 @ pg2" in exI, auto)

   164         apply (unfold tassemble_to.simps)

   165         apply (rule_tac x = pos1 in EXS_intro)

   166         my_block have 

   167           "(tprog_set (map_of pg2 ++ map_of pg3)) = tprog_set (map_of pg2) \<union> tprog_set (map_of pg3)"

   168           proof(rule tprog_set_union)

   169             from hh(2, 5) show "fst ` set pg2 \<inter> fst ` set pg3 = {}"

   170               by (smt disjoint_iff_not_equal)

   171           qed

   172         my_block_end

   173         apply (unfold this, insert this)

   174         my_block

   175           have "tprog_set (map_of pg2) \<inter>  tprog_set (map_of pg3) = {}" 

   176           proof -

   177             { fix x

   178               assume h: "x \<in> tprog_set (map_of pg2)" "x \<in> tprog_set (map_of pg3)"

   179               then obtain i inst where "x = TC i inst" 

   180                                        "map_of pg2 i = Some inst" 

   181                                        "map_of pg3 i = Some inst"

   182                 apply (unfold tprog_set_def)

   183                 by (smt mem_Collect_eq tresource.inject(2))

   184               hence "(i, inst) \<in> set pg2" "(i, inst) \<in> set pg3"

   185                 by (metis map_of_SomeD)+

   186               with hh(2, 5)

   187               have "False"

   188                 by (smt rev_image_eqI)

   189             } thus ?thesis by auto

   190           qed

   191         my_block_end

   192         apply (insert this)

   193         apply (fold set_ins_def)

   194         by (rule sep_conjI, assumption+, simp)

   195     next

   196       case (TLocal body lmap' i lnos prog1 j lno prog2 x)

   197       from TLocal(2)

   198       obtain l where h:

   199         "lmap' lnos = Some l"

   200         "effect (pass2 (body l) lmap') (i, Suc lnos, prog1) (j, lno, prog2) ()"

   201         apply (unfold pass2.simps)

   202         by (auto elim!:effect_elims split:option.splits simp:sm_map_def)

   203       from TLocal(1)[OF this(2)]

   204       obtain pg where hh: "prog2 = pg @ prog1 \<and> (i :[ body l ]: j) (tprog_set (map_of pg))"

   205                           "(\<forall>k\<in> fst ` (set pg). i \<le> k \<and> k < j)"

   206                           "i \<le> j"

   207         by auto

   208       thus ?case

   209         apply (rule_tac x = pg in exI, auto)

   210         apply (unfold tassemble_to.simps)

   211         by (rule_tac x = l in EXS_intro, auto)

   212     qed 

   213   } from this[OF mid(2)] show ?thesis by auto

   214 qed

   215 

   216 definition "valid_tpg tpg = (\<forall> i. \<exists> j prog. assemble i tpg = Some (j, prog))"

   217 

   218 

   219 section {* A new method based on DB indexing *}

   220 

   221 text {*

   222   In this section, we introduced a new method based on DB-indexing to provide a quick check of 

   223    assemblebility of TM assmbly programs in the format of @{text "tpg"}. The 

   224    lemma @{text "ct_left_until_zero"} at the end shows how the well-formedness of @{text "left_until_zero"}

   225    is proved in a modular way.

   226 *}

   227 

   228 datatype cpg = 

   229    CInstr tm_inst

   230  | CLabel nat

   231  | CSeq cpg cpg

   232  | CLocal cpg

   233 

   234 datatype status = Free | Bound

   235 

   236 definition "lift_b t i j = (if (j \<ge> t) then (j + i) else j)"

   237 

   238 fun lift_t :: "nat \<Rightarrow> nat \<Rightarrow> cpg \<Rightarrow> cpg"

   239 where "lift_t t i (CInstr ((act0, l0), (act1, l1))) = 

   240                            (CInstr ((act0, lift_b t i l0), (act1, lift_b t i l1)))" |

   241       "lift_t t i (CLabel l) = CLabel (lift_b t i l)" |

   242       "lift_t t i (CSeq c1 c2) = CSeq (lift_t t i c1) (lift_t t i c2)" |

   243       "lift_t t i (CLocal c) = CLocal (lift_t (t + 1) i c)"

   244 

   245 definition "lift0 (i::nat) cpg = lift_t 0 i cpg"

   246 

   247 definition "perm_b t i j k = (if ((k::nat) = i \<and> i < t \<and> j < t) then j else 

   248                               if (k = j \<and> i < t \<and> j < t) then i else k)"

   249 

   250 lemma inj_perm_b: "inj (perm_b t i j)"

   251 proof(induct rule:injI)

   252   case (1 x y)

   253   thus ?case

   254     by (unfold perm_b_def, auto split:if_splits)

   255 qed

   256 

   257 fun perm :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> cpg \<Rightarrow> cpg"

   258 where "perm t i j (CInstr ((act0, l0), (act1, l1))) = 

   259                            (CInstr ((act0, perm_b t i j l0), (act1, perm_b t i j l1)))" |

   260       "perm t i j (CLabel l) = CLabel (perm_b t i j l)" |

   261       "perm t i j (CSeq c1 c2) = CSeq (perm t i j c1) (perm t i j c2)" |

   262       "perm t i j (CLocal c) = CLocal (perm (t + 1) (i + 1) (j + 1) c)"

   263 

   264 definition "map_idx f sts = map (\<lambda> k. sts!(f (nat k))) [0 .. int (length sts) - 1]"

   265 

   266 definition "perm_s i j sts = map_idx (perm_b (length sts) i j) sts" 

   267 

   268 value "perm_s 2 5 [(0::int), 1, 2, 3, 4, 5, 6, 7, 8, 9, 10]"

   269 

   270 lemma "perm_s 2 20 [(0::int), 1, 2, 3, 4, 5, 6, 7, 8, 9, 10] = x"

   271   apply (unfold perm_s_def map_idx_def perm_b_def, simp add:upto.simps)

   272   oops

   273 

   274 lemma upto_len: "length [i .. j] = (if j < i then 0 else (nat (j - i + 1)))"

   275 proof(induct i j rule:upto.induct)

   276   case (1 i j)

   277   show ?case

   278   proof(cases "j < i")

   279     case True

   280     thus ?thesis by simp

   281   next

   282     case False

   283     hence eq_ij: "[i..j] = i # [i + 1..j]" by (simp add:upto.simps)

   284     from 1 False

   285     show ?thesis

   286       by (auto simp:eq_ij)

   287   qed

   288 qed

   289 

   290 lemma perm_s_len: "length (perm_s i j sts') = length sts'"

   291   apply (unfold perm_s_def map_idx_def)

   292   by (smt Nil_is_map_conv length_0_conv length_greater_0_conv length_map neq_if_length_neq upto_len)

   293 

   294 fun c2t :: "nat list \<Rightarrow> cpg \<Rightarrow> tpg" where 

   295   "c2t env (CInstr ((act0, st0), (act1, st1))) = TInstr ((act0, env!st0), (act1, env!st1))" |

   296   "c2t env (CLabel l) = TLabel (env!l)" |

   297   "c2t env (CSeq cpg1 cpg2) = TSeq (c2t env cpg1) (c2t env cpg2)" |

   298   "c2t env (CLocal cpg) = TLocal (\<lambda> x. c2t (x#env) cpg)" 

   299 

   300 instantiation status :: minus

   301 begin

   302    fun minus_status :: "status \<Rightarrow> status \<Rightarrow> status" where

   303      "minus_status Bound Bound = Free" |

   304      "minus_status Bound Free = Bound" |

   305      "minus_status Free x = Free "

   306    instance ..

   307 end

   308 

   309 instantiation status :: plus

   310 begin

   311    fun plus_status :: "status \<Rightarrow> status \<Rightarrow> status" where

   312      "plus_status Free x = x" |

   313      "plus_status Bound x = Bound"

   314    instance ..

   315 end

   316 

   317 instantiation list :: (plus)plus

   318 begin

   319    fun plus_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where

   320      "plus_list [] ys = []" |

   321      "plus_list (x#xs) [] = []" |

   322      "plus_list (x#xs) (y#ys) = ((x + y)#plus_list xs ys)"

   323    instance ..

   324 end

   325 

   326 instantiation list :: (minus)minus

   327 begin

   328    fun minus_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where

   329      "minus_list [] ys = []" |

   330      "minus_list (x#xs) [] = []" |

   331      "minus_list (x#xs) (y#ys) = ((x - y)#minus_list xs ys)"

   332    instance ..

   333 end

   334 

   335 (* consts castr :: "nat list \<Rightarrow> nat \<Rightarrow> cpg \<Rightarrow> nat \<Rightarrow> tassert"

   336 

   337 definition "castr env i cpg j = (i:[c2t env cpg]:j)" *)

   338 

   339 (*

   340 definition 

   341    "c2p sts i cpg j = (\<forall> x. ((length x = length sts \<and> 

   342                                (\<forall> k < length sts. sts!k = Bound \<longrightarrow> (\<exists> f. x!k = f i)))

   343                                 \<longrightarrow> (\<exists> s. (i:[(c2t x cpg)]:j) s)))"

   344 *)

   345 

   346 definition 

   347    "c2p sts i cpg j = 

   348            (\<exists> f. \<forall> x. ((length x = length sts \<and> 

   349                         (\<forall> k < length sts. sts!k = Bound \<longrightarrow> (x!k = f i k)))

   350                    \<longrightarrow> (\<exists> s. (i:[(c2t x cpg)]:j) s)))"

   351 

   352 fun  wf_cpg_test :: "status list \<Rightarrow> cpg \<Rightarrow> (bool \<times> status list)" where

   353   "wf_cpg_test sts (CInstr ((a0, l0), (a1, l1))) = ((l0 < length sts \<and> l1 < length sts), sts)" |

   354   "wf_cpg_test sts (CLabel l) = ((l < length sts) \<and> sts!l = Free, sts[l:=Bound])" |

   355   "wf_cpg_test sts (CSeq c1 c2) = (let (b1, sts1) = wf_cpg_test sts c1;

   356                                   (b2, sts2) = wf_cpg_test sts1 c2 in

   357                                      (b1 \<and> b2, sts2))" |

   358   "wf_cpg_test sts (CLocal body) = (let (b, sts') = (wf_cpg_test (Free#sts) body) in 

   359                                    (b, tl sts'))" 

   360 

   361 instantiation status :: order

   362 begin

   363   definition less_eq_status_def: "((st1::status) \<le> st2) = (st1 = Free \<or> st2 = Bound)"

   364   definition less_status_def: "((st1::status) < st2) = (st1 \<le> st2 \<and> st1 \<noteq> st2)"

   365 instance

   366 proof

   367   fix x y 

   368   show "(x < (y::status)) = (x \<le> y \<and> \<not> y \<le> x)"

   369     by (metis less_eq_status_def less_status_def status.distinct(1))

   370 next

   371   fix x show "x \<le> (x::status)"

   372     by (metis (full_types) less_eq_status_def status.exhaust)

   373 next

   374   fix x y z

   375   assume "x \<le> y" "y \<le> (z::status)" show "x \<le> (z::status)"

   376     by (metis `x \<le> y` `y \<le> z` less_eq_status_def status.distinct(1))

   377 next

   378   fix x y

   379   assume "x \<le> y" "y \<le> (x::status)" show "x = y"

   380     by (metis `x \<le> y` `y \<le> x` less_eq_status_def status.distinct(1))

   381 qed

   382 end

   383 

   384 instantiation list :: (order)order

   385 begin

   386   definition "((sts::('a::order) list)  \<le> sts') = 

   387                    ((length sts = length sts') \<and> (\<forall> i < length sts. sts!i \<le> sts'!i))"

   388   definition "((sts::('a::order) list)  < sts') = ((sts \<le> sts') \<and> sts \<noteq> sts')"

   389 

   390   lemma anti_sym: assumes h: "x \<le> (y::'a list)" "y \<le> x"

   391       shows "x = y"

   392   proof -

   393     from h have "length x = length y"

   394       by (metis less_eq_list_def)

   395     moreover from h have " (\<forall> i < length x. x!i = y!i)"

   396       by (metis (full_types) antisym_conv less_eq_list_def)

   397     ultimately show ?thesis

   398       by (metis nth_equalityI)

   399   qed

   400 

   401   lemma refl: "x \<le> (x::('a::order) list)"

   402     apply (unfold less_eq_list_def)

   403     by (metis order_refl)

   404 

   405   instance

   406   proof

   407     fix x y

   408     show "((x::('a::order) list) < y) = (x \<le> y \<and> \<not> y \<le> x)"

   409     proof

   410       assume h: "x \<le> y \<and> \<not> y \<le> x"

   411       have "x \<noteq> y"

   412       proof

   413         assume "x = y" with h have "\<not> (x \<le> x)" by simp

   414         with refl show False by auto

   415       qed

   416       moreover from h have "x \<le> y" by blast

   417       ultimately show "x < y" by (auto simp:less_list_def)

   418     next

   419       assume h: "x < y"

   420       hence hh: "x \<le> y"

   421         by (metis TM_Assemble.less_list_def)

   422       moreover have "\<not> y \<le> x"

   423       proof

   424         assume "y \<le> x"

   425         from anti_sym[OF hh this] have "x = y" .

   426         with h show False

   427           by (metis less_list_def) 

   428       qed

   429       ultimately show "x \<le> y \<and> \<not> y \<le> x" by auto

   430     qed

   431   next

   432     fix x from refl show "(x::'a list) \<le> x" .

   433   next

   434     fix x y assume "(x::'a list) \<le> y" "y \<le> x" 

   435     from anti_sym[OF this] show "x = y" .

   436   next

   437     fix x y z

   438     assume h: "(x::'a list) \<le> y" "y \<le> z"

   439     show "x \<le> z"

   440     proof -

   441       from h have "length x = length z" by (metis TM_Assemble.less_eq_list_def)

   442       moreover from h have "\<forall> i < length x. x!i \<le> z!i"

   443         by (metis TM_Assemble.less_eq_list_def order_trans)

   444       ultimately show "x \<le> z"

   445         by (metis TM_Assemble.less_eq_list_def)

   446     qed

   447   qed

   448 end

   449 

   450 lemma sts_bound_le: "sts \<le> sts[l := Bound]"

   451 proof -

   452   have "length sts = length (sts[l := Bound])"

   453     by (metis length_list_update)

   454   moreover have "\<forall> i < length sts. sts!i \<le> (sts[l:=Bound])!i"

   455   proof -

   456     { fix i

   457       assume "i < length sts"

   458       have "sts ! i \<le> sts[l := Bound] ! i"

   459       proof(cases "l < length sts")

   460         case True

   461         note le_l = this

   462         show ?thesis

   463         proof(cases "l = i")

   464           case True with le_l

   465           have "sts[l := Bound] ! i = Bound" by auto

   466           thus ?thesis by (metis less_eq_status_def) 

   467         next

   468           case False

   469           with le_l have "sts[l := Bound] ! i = sts!i" by auto

   470           thus ?thesis by auto

   471         qed

   472       next

   473         case False

   474         hence "sts[l := Bound] = sts" by auto

   475         thus ?thesis by auto

   476       qed

   477     } thus ?thesis by auto

   478   qed

   479   ultimately show ?thesis by (metis less_eq_list_def) 

   480 qed

   481 

   482 lemma sts_tl_le:

   483   assumes "sts \<le> sts'"

   484   shows "tl sts \<le> tl sts'"

   485 proof -

   486   from assms have "length (tl sts) = length (tl sts')"

   487     by (metis (hide_lams, no_types) length_tl less_eq_list_def)

   488   moreover from assms have "\<forall> i < length (tl sts). (tl sts)!i \<le> (tl sts')!i"

   489     by (smt calculation length_tl less_eq_list_def nth_tl)

   490   ultimately show ?thesis

   491     by (metis less_eq_list_def)

   492 qed

   493 

   494 lemma wf_cpg_test_le:

   495   assumes "wf_cpg_test sts cpg = (True, sts')"

   496   shows "sts \<le> sts'" using assms

   497 proof(induct cpg arbitrary:sts sts')

   498   case (CInstr instr sts sts')

   499   obtain a0 l0 a1 l1 where eq_instr: "instr = ((a0, l0), (a1, l1))" 

   500     by (metis prod.exhaust)

   501   from CInstr[unfolded this]

   502   show ?case by simp

   503 next

   504   case (CLabel l sts sts')

   505   thus ?case by (auto simp:sts_bound_le)

   506 next

   507   case (CLocal body sts sts')

   508   from this(2)

   509   obtain sts1 where h: "wf_cpg_test (Free # sts) body = (True, sts1)" "sts' = tl sts1"

   510     by (auto split:prod.splits)

   511   from CLocal(1)[OF this(1)] have "Free # sts \<le> sts1" .

   512   from sts_tl_le[OF this]

   513   have "sts \<le> tl sts1" by simp

   514   from this[folded h(2)]

   515   show ?case .

   516 next

   517   case (CSeq cpg1 cpg2 sts sts')

   518   from this(3)

   519   show ?case

   520     by (auto split:prod.splits dest!:CSeq(1, 2))

   521 qed

   522 

   523 lemma c2p_assert:

   524   assumes "(c2p [] i cpg j)"

   525   shows "\<exists> s. (i :[(c2t [] cpg)]: j) s"

   526 proof -

   527   from assms obtain f where

   528     h [rule_format]: 

   529     "\<forall> x. length x = length [] \<and> (\<forall>k<length []. [] ! k = Bound \<longrightarrow> (x ! k = f i k)) \<longrightarrow>

   530                         (\<exists> s. (i :[ c2t [] cpg ]: j) s)"

   531     by (unfold c2p_def, auto)

   532   have "length [] = length [] \<and> (\<forall>k<length []. [] ! k = Bound \<longrightarrow> ([] ! k = f i k))"

   533     by auto

   534   from h[OF this] obtain s where "(i :[ c2t [] cpg ]: j) s" by blast

   535   thus ?thesis by auto

   536 qed

   537 

   538 definition "sts_disj sts sts' = ((length sts = length sts') \<and> 

   539                                  (\<forall> i < length sts. \<not>(sts!i = Bound \<and> sts'!i = Bound)))"

   540 

   541 lemma length_sts_plus:

   542   assumes "length (sts1 :: status list) = length sts2"

   543   shows "length (sts1 + sts2) = length sts1"

   544   using assms

   545 proof(induct sts1 arbitrary: sts2)

   546   case Nil

   547   thus ?case

   548     by (metis plus_list.simps(1))

   549 next

   550   case (Cons s' sts' sts2)

   551   thus ?case

   552   proof(cases "sts2 = []")

   553     case True

   554     with Cons show ?thesis by auto

   555   next

   556     case False

   557     then obtain s'' sts'' where eq_sts2: "sts2 = s''#sts''"

   558       by (metis neq_Nil_conv)

   559     with Cons

   560     show ?thesis

   561       by (metis length_Suc_conv list.inject plus_list.simps(3))

   562   qed

   563 qed

   564 

   565 

   566 lemma nth_sts_plus:

   567   assumes "i < length ((sts1::status list) + sts2)"

   568   shows "(sts1 + sts2)!i = sts1!i + sts2!i"

   569   using assms

   570 proof(induct sts1 arbitrary:i sts2)

   571   case (Nil i sts2)

   572   thus ?case by auto

   573 next

   574   case (Cons s' sts' i sts2)

   575   show ?case

   576   proof(cases "sts2 = []")

   577     case True

   578     with Cons show ?thesis by auto

   579   next

   580     case False

   581     then obtain s'' sts'' where eq_sts2: "sts2 = s''#sts''"

   582       by (metis neq_Nil_conv)

   583     with Cons

   584     show ?thesis

   585       by (smt list.size(4) nth_Cons' plus_list.simps(3))

   586   qed

   587 qed

   588 

   589 lemma nth_sts_minus:

   590   assumes "i < length ((sts1::status list) - sts2)"

   591   shows "(sts1 - sts2)!i = sts1!i - sts2!i"

   592   using assms

   593 proof(induct  arbitrary:i rule:minus_list.induct)

   594   case (3 x xs y ys i)

   595   show ?case

   596   proof(cases i)

   597     case 0

   598     thus ?thesis by simp

   599   next

   600     case (Suc k)

   601     with 3(2) have "k < length (xs - ys)" by auto

   602     from 3(1)[OF this] and Suc

   603     show ?thesis

   604       by auto

   605   qed

   606 qed auto

   607 

   608 fun taddr :: "tresource \<Rightarrow> nat" where

   609    "taddr (TC i instr) = i"

   610 

   611 lemma tassemble_to_range:

   612   assumes "(i :[tpg]: j) s"

   613   shows "(i \<le> j) \<and> (\<forall> r \<in> s. i \<le> taddr r \<and> taddr r < j)"

   614   using assms

   615 proof(induct tpg arbitrary: i j s)

   616   case (TInstr instr i j s)

   617   obtain a0 l0 a1 l1 where "instr = ((a0, l0), (a1, l1))"

   618     by (metis pair_collapse)

   619   with TInstr

   620   show ?case

   621     apply (simp add:tassemble_to.simps sg_def)

   622     by (smt `instr = ((a0, l0), a1, l1)` cond_eq cond_true_eq1 

   623         empty_iff insert_iff le_refl lessI sep.mult_commute taddr.simps)

   624 next

   625   case (TLabel l i j s)

   626   thus ?case

   627     apply (simp add:tassemble_to.simps)

   628     by (smt equals0D pasrt_def set_zero_def)

   629 next

   630   case (TSeq c1 c2 i j s)

   631   from TSeq(3) obtain s1 s2 j' where 

   632     h: "(i :[ c1 ]: j') s1" "(j' :[ c2 ]: j) s2" "s1 ## s2" "s = s1 + s2"

   633     by (auto simp:tassemble_to.simps elim!:EXS_elim sep_conjE)

   634   show ?case

   635   proof -

   636     { fix r 

   637       assume "r \<in> s"

   638       with h (3, 4) have "r \<in> s1 \<or> r \<in> s2"

   639         by (auto simp:set_ins_def)

   640       hence "i \<le> j \<and> i \<le> taddr r \<and> taddr r < j" 

   641       proof

   642         assume " r \<in> s1"

   643         from TSeq(1)[OF h(1)]

   644         have "i \<le> j'" "(\<forall>r\<in>s1. i \<le> taddr r \<and> taddr r < j')" by auto

   645         from this(2)[rule_format, OF `r \<in> s1`]

   646         have "i \<le> taddr r" "taddr r < j'" by auto

   647         with TSeq(2)[OF h(2)]

   648         show ?thesis by auto

   649       next

   650         assume "r \<in> s2"

   651         from TSeq(2)[OF h(2)]

   652         have "j' \<le> j" "(\<forall>r\<in>s2. j' \<le> taddr r \<and> taddr r < j)" by auto

   653         from this(2)[rule_format, OF `r \<in> s2`]

   654         have "j' \<le> taddr r" "taddr r < j" by auto

   655         with TSeq(1)[OF h(1)]

   656         show ?thesis by auto

   657       qed

   658     } thus ?thesis

   659       by (smt TSeq.hyps(1) TSeq.hyps(2) h(1) h(2))

   660   qed

   661 next

   662   case (TLocal body i j s)

   663   from this(2) obtain l s' where "(i :[ body l ]: j) s"

   664     by (simp add:tassemble_to.simps, auto elim!:EXS_elim)

   665   from TLocal(1)[OF this]

   666   show ?case by auto

   667 qed

   668 

   669 lemma c2p_seq:

   670   assumes "c2p sts1 i cpg1 j'"

   671           "c2p sts2 j' cpg2 j"

   672           "sts_disj sts1 sts2"

   673   shows "(c2p (sts1 + sts2) i (CSeq cpg1 cpg2) j)" 

   674 proof -

   675   from assms(1)[unfolded c2p_def]

   676   obtain f1 where

   677     h1[rule_format]: 

   678         "\<forall>x. length x = length sts1 \<and> (\<forall>k<length sts1. sts1 ! k = Bound \<longrightarrow> (x ! k = f1 i k)) \<longrightarrow>

   679               Ex (i :[ c2t x cpg1 ]: j')" by blast

   680   from assms(2)[unfolded c2p_def]

   681   obtain f2 where h2[rule_format]: 

   682         "\<forall>x. length x = length sts2 \<and> (\<forall>k<length sts2. sts2 ! k = Bound \<longrightarrow> (x ! k = f2 j' k)) \<longrightarrow>

   683               Ex (j' :[ c2t x cpg2 ]: j)" by blast

   684   from assms(3)[unfolded sts_disj_def]

   685   have h3: "length sts1 = length sts2" 

   686     and h4[rule_format]: 

   687         "(\<forall>i<length sts1. \<not> (sts1 ! i = Bound \<and> sts2 ! i = Bound))" by auto

   688   let ?f = "\<lambda> i k. if (sts1!k = Bound) then f1 i k else f2 j' k"

   689   { fix x 

   690     assume h5: "length x = length (sts1 + sts2)" and

   691            h6[rule_format]: "(\<forall>k<length (sts1 + sts2). (sts1 + sts2) ! k = Bound \<longrightarrow> x ! k = ?f i k)"

   692     obtain s1 where h_s1: "(i :[ c2t x cpg1 ]: j') s1"

   693     proof(atomize_elim, rule h1)

   694       from h3 h5 have "length x = length sts1"

   695         by (metis length_sts_plus)

   696       moreover {

   697         fix k assume hh: "k<length sts1" "sts1 ! k = Bound"

   698         from hh(1) h3 h5 have p1: "k < length (sts1 + sts2)"

   699           by (metis calculation)

   700         from h3 hh(2) have p2: "(sts1 + sts2)!k = Bound"

   701           by (metis nth_sts_plus p1 plus_status.simps(2))

   702         from h6[OF p1 p2] have "x ! k = (if sts1 ! k = Bound then f1 i k else f2 j' k)" .

   703         with hh(2)

   704         have "x ! k = f1 i k" by simp

   705       } ultimately show "length x = length sts1 \<and> 

   706           (\<forall>k<length sts1. sts1 ! k = Bound \<longrightarrow> (x ! k = f1 i k))"

   707         by blast

   708     qed

   709     obtain s2 where h_s2: "(j' :[ c2t x cpg2 ]: j) s2"

   710     proof(atomize_elim, rule h2)

   711       from h3 h5 have "length x = length sts2"

   712         by (metis length_sts_plus) 

   713       moreover {

   714         fix k

   715         assume hh: "k<length sts2" "sts2 ! k = Bound"

   716         from hh(1) h3 h5 have p1: "k < length (sts1 + sts2)"

   717           by (metis calculation)

   718         from  hh(1) h3 h5 hh(2) have p2: "(sts1 + sts2)!k = Bound"

   719           by (metis `length sts1 = length sts2 \<and> 

   720                (\<forall>i<length sts1. \<not> (sts1 ! i = Bound \<and> sts2 ! i = Bound))` 

   721              calculation nth_sts_plus plus_status.simps(1) status.distinct(1) status.exhaust)

   722         from h6[OF p1 p2] have "x ! k = (if sts1 ! k = Bound then f1 i k else f2 j' k)" .

   723         moreover from h4[OF hh(1)[folded h3]] hh(2) have "sts1!k \<noteq> Bound" by auto

   724         ultimately have "x!k = f2 j' k" by simp

   725       } ultimately show "length x = length sts2 \<and> 

   726                                (\<forall>k<length sts2. sts2 ! k = Bound \<longrightarrow> (x ! k = f2 j' k))"

   727         by blast

   728     qed

   729     have h_s12: "s1 ## s2"

   730     proof -

   731       { fix r assume h: "r \<in> s1" "r \<in> s2"

   732         with h_s1 h_s2

   733         have "False"by (smt tassemble_to_range) 

   734       } thus ?thesis by (auto simp:set_ins_def)

   735     qed  

   736     have "(EXS j'. i :[ c2t x cpg1 ]: j' \<and>* j' :[ c2t x cpg2 ]: j) (s1 + s2)"

   737     proof(rule_tac x = j' in EXS_intro)

   738       from h_s1 h_s2 h_s12

   739       show "(i :[ c2t x cpg1 ]: j' \<and>* j' :[ c2t x cpg2 ]: j) (s1 + s2)"

   740         by (metis sep_conjI)

   741     qed

   742     hence "\<exists> s. (i :[ c2t x (CSeq cpg1 cpg2) ]: j) s" 

   743       by (auto simp:tassemble_to.simps)

   744   }

   745   hence "\<exists>f. \<forall>x. length x = length (sts1 + sts2) \<and>

   746                (\<forall>k<length (sts1 + sts2). (sts1 + sts2) ! k = Bound \<longrightarrow> x ! k = f i k) \<longrightarrow>

   747                Ex (i :[ c2t x (CSeq cpg1 cpg2) ]: j)"

   748     by (rule_tac x = ?f in exI, auto)

   749   thus ?thesis 

   750     by(unfold c2p_def, auto)

   751 qed

   752 

   753 lemma plus_list_len:

   754   "length ((sts1::status list) + sts2) = min (length sts1) (length sts2)"

   755   by(induct rule:plus_list.induct, auto)

   756 

   757 lemma minus_list_len:

   758   "length ((sts1::status list) - sts2) = min (length sts1) (length sts2)"

   759   by(induct rule:minus_list.induct, auto)

   760 

   761 lemma sts_le_comb:

   762   assumes "sts1 \<le> sts2"

   763   and "sts2 \<le> sts3"

   764   shows "sts_disj (sts2 - sts1) (sts3 - sts2)" and

   765         "(sts3 - sts1) = (sts2 - sts1) + (sts3 - sts2)"

   766 proof -

   767   from assms 

   768   have h1: "length sts1 = length sts2" "\<forall>i<length sts1. sts1 ! i \<le> sts2 ! i"

   769     and h2: "length sts2 = length sts3" "\<forall>i<length sts1. sts2 ! i \<le> sts3 ! i"

   770     by (unfold less_eq_list_def, auto)

   771   have "sts_disj (sts2 - sts1) (sts3 - sts2)"

   772   proof -

   773     from h1(1) h2(1)

   774     have "length (sts2 - sts1) = length (sts3 - sts2)"

   775       by (metis minus_list_len)

   776     moreover {

   777       fix i

   778       assume lt_i: "i<length (sts2 - sts1)"

   779       from lt_i h1(1) h2(1) have "i < length sts1"

   780         by (smt minus_list_len)

   781       from h1(2)[rule_format, of i, OF this] h2(2)[rule_format, of i, OF this]

   782       have "sts1 ! i \<le> sts2 ! i" "sts2 ! i \<le> sts3 ! i" .

   783       moreover have "(sts2 - sts1) ! i = sts2!i - sts1!i"

   784         by (metis lt_i nth_sts_minus)

   785       moreover have "(sts3 - sts2)!i = sts3!i - sts2!i"

   786         by (metis `length (sts2 - sts1) = length (sts3 - sts2)` lt_i nth_sts_minus)

   787       ultimately have " \<not> ((sts2 - sts1) ! i = Bound \<and> (sts3 - sts2) ! i = Bound)"

   788         apply (cases "sts2!i", cases "sts1!i", cases "sts3!i", simp, simp)

   789         apply (cases "sts3!i", simp, simp)

   790         apply (cases "sts1!i", cases "sts3!i", simp, simp)

   791         by (cases "sts3!i", simp, simp)

   792     } ultimately show ?thesis by (unfold sts_disj_def, auto)

   793   qed

   794   moreover have "(sts3 - sts1) = (sts2 - sts1) + (sts3 - sts2)"

   795   proof(induct rule:nth_equalityI)

   796     case 1

   797     show ?case by (metis h1(1) h2(1) length_sts_plus minus_list_len)

   798   next 

   799     case 2

   800     { fix i

   801       assume lt_i: "i<length (sts3 - sts1)"

   802       have "(sts3 - sts1) ! i = (sts2 - sts1 + (sts3 - sts2)) ! i" (is "?L = ?R")

   803       proof -

   804         have "?R = sts2!i - sts1!i + (sts3!i - sts2!i)"

   805           by (smt `i < length (sts3 - sts1)` h2(1) minus_list_len nth_sts_minus 

   806                    nth_sts_plus plus_list_len)

   807         moreover have "?L = sts3!i - sts1!i"

   808           by (metis `i < length (sts3 - sts1)` nth_sts_minus)

   809         moreover 

   810         have "sts2!i - sts1!i + (sts3!i - sts2!i) = sts3!i - sts1!i"

   811         proof -

   812           from lt_i h1(1) h2(1) have "i < length sts1"

   813             by (smt minus_list_len)

   814           from h1(2)[rule_format, of i, OF this] h2(2)[rule_format, of i, OF this]

   815           show ?thesis

   816             apply (cases "sts2!i", cases "sts1!i", cases "sts3!i", simp, simp)

   817             apply (cases "sts3!i", simp, simp)

   818             apply (cases "sts1!i", cases "sts3!i", simp, simp)

   819             by (cases "sts3!i", simp, simp)

   820         qed

   821         ultimately show ?thesis by simp

   822       qed

   823     } thus ?case by auto

   824   qed

   825   ultimately show "sts_disj (sts2 - sts1) (sts3 - sts2)" and

   826                   "(sts3 - sts1) = (sts2 - sts1) + (sts3 - sts2)" by auto

   827 qed

   828 

   829 lemma wf_cpg_test_correct: 

   830   assumes "wf_cpg_test sts cpg = (True, sts')"

   831   shows "(\<forall> i. \<exists> j. (c2p (sts' - sts) i cpg j))" 

   832   using assms

   833 proof(induct cpg arbitrary:sts sts')

   834   case (CInstr instr sts sts')

   835   obtain a0 l0 a1 l1 where eq_instr: "instr = ((a0, l0), (a1, l1))" 

   836     by (metis prod.exhaust)

   837   show ?case 

   838   proof(unfold eq_instr c2p_def, clarsimp simp:tassemble_to.simps)

   839     fix i

   840     let ?a = "Suc i" and ?f = "\<lambda> i k. i"

   841     show "\<exists>a f. \<forall>x. length x = length (sts' - sts) \<and>

   842                   (\<forall>k<length (sts' - sts). (sts' - sts) ! k = Bound \<longrightarrow> x ! k = f i k) \<longrightarrow>

   843                   Ex (sg {TC i ((a0, x ! l0), a1, x ! l1)} \<and>* <(a = Suc i)>)"

   844     proof(rule_tac x = ?a in exI, rule_tac x = ?f in exI, default, clarsimp)

   845       fix x

   846       let ?j = "Suc i"

   847       let ?s = " {TC i ((a0, x ! l0), a1, x ! l1)}"

   848       have "(sg {TC i ((a0, x ! l0), a1, x ! l1)} \<and>* <(Suc i = Suc i)>) ?s"

   849         by (simp add:tassemble_to.simps sg_def)

   850       thus "Ex (sg {TC i ((a0, x ! l0), a1, x ! l1)})" by auto

   851     qed

   852   qed

   853 next

   854   case (CLabel l sts sts')

   855   show ?case

   856   proof

   857     fix i

   858     from CLabel 

   859     have h1: "l < length sts" 

   860       and h2: "sts ! l = Free"

   861       and h3: "sts[l := Bound] = sts'" by auto

   862     let ?f = "\<lambda> i k. i"

   863     have "\<exists>a f. \<forall>x. length x = length (sts' - sts) \<and>

   864                   (\<forall>k<length (sts' - sts). (sts' - sts) ! k = Bound \<longrightarrow> x ! k = f (i::nat) k) \<longrightarrow>

   865                   Ex (<(i = a \<and> a = x ! l)>)"

   866     proof(rule_tac x = i in exI, rule_tac x = ?f in exI, clarsimp)

   867       fix x

   868       assume h[rule_format]:

   869         "\<forall>k<length (sts' - sts). (sts' - sts) ! k = Bound \<longrightarrow> x ! k = i"

   870       from h1 h3 have p1: "l < length (sts' - sts)"

   871         by (metis length_list_update min_max.inf.idem minus_list_len)

   872       from p1 h2 h3 have p2: "(sts' - sts)!l = Bound"

   873         by (metis h1 minus_status.simps(2) nth_list_update_eq nth_sts_minus)

   874       from h[OF p1 p2] have "(<(i = x ! l)>) 0" 

   875         by (simp add:set_ins_def)

   876       thus "\<exists> s.  (<(i = x ! l)>) s" by auto

   877     qed 

   878     thus "\<exists>a. c2p (sts' - sts) i (CLabel l) a"

   879       by (auto simp:c2p_def tassemble_to.simps)

   880   qed

   881 next

   882   case (CSeq cpg1 cpg2 sts sts')

   883   show ?case

   884   proof

   885     fix i

   886     from CSeq(3)[unfolded wf_cpg_test.simps] 

   887     show "\<exists> j. c2p (sts' - sts) i (CSeq cpg1 cpg2) j"

   888     proof(let_elim) 

   889       case (LetE b1 sts1)

   890       from this(1)

   891       obtain b2 where h: "(b2, sts') = wf_cpg_test sts1 cpg2" "b1=True" "b2=True" 

   892         by (atomize_elim, unfold Let_def, auto split:prod.splits)

   893       from wf_cpg_test_le[OF LetE(2)[symmetric, unfolded h(2)]]

   894       have sts_le1: "sts \<le> sts1" .

   895       from CSeq(1)[OF LetE(2)[unfolded h(2), symmetric], rule_format, of i]

   896       obtain j1 where h1: "(c2p (sts1 - sts) i cpg1 j1)" by blast

   897       from wf_cpg_test_le[OF h(1)[symmetric, unfolded h(3)]]

   898       have sts_le2: "sts1 \<le> sts'" .

   899       from sts_le_comb[OF sts_le1 sts_le2]

   900       have hh: "sts_disj (sts1 - sts) (sts' - sts1)"

   901                "sts' - sts = (sts1 - sts) + (sts' - sts1)" .

   902       from CSeq(2)[OF h(1)[symmetric, unfolded h(3)], rule_format, of j1]

   903       obtain j2 where h2: "(c2p (sts' - sts1) j1 cpg2 j2)" by blast

   904       have "c2p (sts' - sts) i (CSeq cpg1 cpg2) j2"

   905         by(unfold hh(2), rule c2p_seq[OF h1 h2 hh(1)])

   906       thus ?thesis by blast 

   907     qed

   908   qed

   909 next

   910   case (CLocal body sts sts')

   911   from this(2) obtain b sts1 s where 

   912       h: "wf_cpg_test (Free # sts) body = (True, sts1)"

   913          "sts' = tl sts1" 

   914     by (unfold wf_cpg_test.simps, auto split:prod.splits)

   915   from wf_cpg_test_le[OF h(1), unfolded less_eq_list_def] h(2)

   916   obtain s where eq_sts1: "sts1 = s#sts'"

   917     by (metis Suc_length_conv list.size(4) tl.simps(2))

   918   from CLocal(1)[OF h(1)] have p1: "\<forall>i. \<exists>a. c2p (sts1 - (Free # sts)) i body a" .

   919   show ?case

   920   proof

   921     fix i

   922     from p1[rule_format, of i] obtain j where "(c2p (sts1 - (Free # sts)) i body) j" by blast

   923     then obtain f where hh [rule_format]: 

   924            "\<forall>x. length x = length (sts1 - (Free # sts)) \<and>

   925                 (\<forall>k<length (sts1 - (Free # sts)). (sts1 - (Free # sts)) ! k = Bound \<longrightarrow> x ! k = f i k) \<longrightarrow>

   926                         (\<exists>s. (i :[ c2t x body ]: j) s)"

   927       by (auto simp:c2p_def)

   928     let ?f = "\<lambda> i k. f i (Suc k)"

   929     have "\<exists>j f. \<forall>x. length x = length (sts' - sts) \<and>

   930               (\<forall>k<length (sts' - sts). (sts' - sts) ! k = Bound \<longrightarrow> x ! k = f i k) \<longrightarrow>

   931               (\<exists>s. (i :[ (TL xa. c2t (xa # x) body) ]: j) s)"

   932     proof(rule_tac x = j in exI, rule_tac x = ?f in exI, default, clarsimp)

   933       fix x

   934       assume h1: "length x = length (sts' - sts)"

   935         and h2: "\<forall>k<length (sts' - sts). (sts' - sts) ! k = Bound \<longrightarrow> x ! k = f i (Suc k)"

   936       let ?l = "f i 0" let ?x = " ?l#x"

   937       from wf_cpg_test_le[OF h(1)] have "length (Free#sts) = length sts1"

   938         by (unfold less_eq_list_def, simp)

   939       with h1 h(2) have q1: "length (?l # x) = length (sts1 - (Free # sts))"

   940         by (smt Suc_length_conv length_Suc_conv list.inject list.size(4) 

   941                 minus_list.simps(3) minus_list_len tl.simps(2))

   942       have q2: "(\<forall>k<length (sts1 - (Free # sts)). 

   943                   (sts1 - (Free # sts)) ! k = Bound \<longrightarrow> (f i 0 # x) ! k = f i k)" 

   944       proof -

   945         { fix k

   946           assume lt_k: "k<length (sts1 - (Free # sts))"

   947             and  bd_k: "(sts1 - (Free # sts)) ! k = Bound"

   948           have "(f i 0 # x) ! k = f i k"

   949           proof(cases "k")

   950             case (Suc k')

   951             moreover have "x ! k' = f i (Suc k')"

   952             proof(rule h2[rule_format])

   953               from bd_k Suc eq_sts1 show "(sts' - sts) ! k' = Bound" by simp

   954             next

   955               from Suc lt_k eq_sts1 show "k' < length (sts' - sts)" by simp

   956             qed

   957             ultimately show ?thesis by simp

   958           qed simp

   959         } thus ?thesis by auto

   960       qed

   961       from conjI[THEN hh[of ?x], OF q1 q2] obtain s 

   962         where h_s: "(i :[ c2t (f i 0 # x) body ]: j) s" by blast

   963       thus "\<exists>s. (i :[ (TL xa. c2t (xa # x) body) ]: j) s"

   964         apply (simp add:tassemble_to.simps)

   965         by (rule_tac x = s in exI, rule_tac x = ?l in EXS_intro, simp)

   966     qed

   967     thus "\<exists>j. c2p (sts' - sts) i (CLocal body) j" 

   968       by (auto simp:c2p_def)

   969   qed

   970 qed

   971 

   972 lemma 

   973   assumes "wf_cpg_test [] cpg = (True, sts')"

   974   and "tpg = c2t [] cpg"

   975   shows "\<forall> i. \<exists> j s.  ((i:[tpg]:j) s)"

   976 proof

   977   fix i

   978   have eq_sts_minus: "(sts' - []) = []"

   979     by (metis list.exhaust minus_list.simps(1) minus_list.simps(2))

   980   from wf_cpg_test_correct[OF assms(1), rule_format, of i]

   981   obtain j where "c2p (sts' - []) i cpg j" by auto

   982   from c2p_assert [OF this[unfolded eq_sts_minus]]

   983   obtain s where "(i :[ c2t [] cpg ]: j) s" by blast

   984   from this[folded assms(2)]

   985   show " \<exists> j s.  ((i:[tpg]:j) s)" by blast

   986 qed

   987 

   988 lemma replicate_nth: "(replicate n x @ sts) ! (l + n)  = sts!l"

   989   by (smt length_replicate nth_append)

   990 

   991 lemma replicate_update: 

   992   "(replicate n x @ sts)[l + n := v] = replicate n x @ sts[l := v]"

   993   by (smt length_replicate list_update_append)

   994 

   995 lemma l_n_v_orig:

   996   assumes "l0 < length env"

   997   and "t \<le> l0"

   998   shows "(take t env @ es @ drop t env) ! (l0 + length es) = env ! l0"

   999 proof -

  1000   from assms(1, 2) have "t < length env" by auto

  1001   hence h: "env = take t env @ drop t env" 

  1002            "length (take t env) = t"

  1003     apply (metis append_take_drop_id)

  1004     by (smt `t < length env` length_take)

  1005   with assms(2) have eq_sts_l: "env!l0 = (drop t env)!(l0 - t)"

  1006     by (metis nth_app)

  1007   from h(2) have "length (take t env @ es) = t + length es"

  1008     by (metis length_append length_replicate nat_add_commute)

  1009   moreover from assms(2) have "t + (length es) \<le> l0 + (length es)" by auto

  1010   ultimately have "((take t env @ es) @ drop t env)!(l0 + length es) = 

  1011                           (drop t env)!(l0+ length es - (t + length es))"

  1012     by (smt length_replicate length_splice nth_append)

  1013   with eq_sts_l[symmetric, unfolded assms]

  1014   show ?thesis by auto

  1015 qed

  1016 

  1017 lemma l_n_v:

  1018   assumes "l < length sts"

  1019   and "sts!l = v"

  1020   and "t \<le> l"

  1021   shows "(take t sts @ replicate n x @ drop t sts) ! (l + n) = v"

  1022 proof -

  1023   from l_n_v_orig[OF assms(1) assms(3), of "replicate n x"]

  1024   and assms(2)

  1025   show ?thesis by auto

  1026 qed

  1027 

  1028 lemma l_n_v_s:

  1029   assumes "l < length sts"

  1030   and "t \<le> l"

  1031   shows "(take t sts @ sts0 @ drop t sts)[l + length sts0 := v] = 

  1032           take t (sts[l:=v])@ sts0 @ drop t (sts[l:=v])"

  1033 proof -

  1034   let ?n = "length sts0"

  1035   from assms(1, 2) have "t < length sts" by auto

  1036   hence h: "sts = take t sts @ drop t sts" 

  1037            "length (take t sts) = t"

  1038     apply (metis append_take_drop_id)

  1039     by (smt `t < length sts` length_take)

  1040   with assms(2) have eq_sts_l: "sts[l:=v] = take t sts @ drop t sts [(l - t) := v]"

  1041     by (smt list_update_append)

  1042   with h(2) have eq_take_drop_t: "take t (sts[l:=v]) = take t sts"

  1043                                  "drop t (sts[l:=v]) = (drop t sts)[l - t:=v]"

  1044     apply (metis append_eq_conv_conj)

  1045     by (metis append_eq_conv_conj eq_sts_l h(2))

  1046   from h(2) have "length (take t sts @ sts0) = t + ?n"

  1047     by (metis length_append length_replicate nat_add_commute)

  1048   moreover from assms(2) have "t + ?n \<le> l + ?n" by auto

  1049   ultimately have "((take t sts @ sts0) @ drop t sts)[l + ?n := v] = 

  1050                    (take t sts @ sts0) @ (drop t sts)[(l + ?n - (t + ?n)) := v]"

  1051     by (smt list_update_append replicate_nth)

  1052   with eq_take_drop_t

  1053   show ?thesis by auto

  1054 qed

  1055 

  1056 lemma l_n_v_s1: 

  1057   assumes "l < length sts"

  1058       and "\<not> t \<le> l"

  1059   shows "(take t sts @ sts0 @ drop t sts)[l := v] =

  1060          take t (sts[l := v]) @ sts0 @ drop t (sts[l := v])"

  1061 proof(cases "t < length sts")

  1062   case False

  1063   hence h: "take t sts = sts" "drop t sts = []"

  1064            "take t (sts[l:=v]) = sts [l:=v]"

  1065            "drop t (sts[l:=v]) = []"

  1066     by auto

  1067   with assms(1)

  1068   show ?thesis 

  1069     by (metis list_update_append)

  1070 next

  1071   case True

  1072   with assms(2)

  1073   have h: "(take t sts)[l:=v] = take t (sts[l:=v])"

  1074           "(sts[l:=v]) = (take t sts)[l:=v]@drop t sts"

  1075           "length (take t sts) = t"

  1076     apply (smt length_list_update length_take nth_equalityI nth_list_update nth_take)

  1077     apply (smt True append_take_drop_id assms(2) length_take list_update_append1)

  1078     by (smt True length_take)

  1079   from h(2,3) have "drop t (sts[l := v]) = drop t sts"

  1080     by (metis append_eq_conv_conj length_list_update)

  1081   with h(1)

  1082   show ?thesis

  1083     apply simp

  1084     by (metis assms(2) h(3) list_update_append1 not_leE)

  1085 qed

  1086 

  1087 lemma l_n_v_s2:

  1088   assumes "l0 < length env"

  1089   and "t \<le> l0"

  1090   and "\<not> t \<le> l1"

  1091   shows "(take t env @ es @ drop t env) ! l1 = env ! l1"

  1092 proof -

  1093   from assms(1, 2) have "t < length env" by auto

  1094   hence  h: "env = take t env @ drop t env" 

  1095             "length (take t env) = t"

  1096     apply (metis append_take_drop_id)

  1097     by (smt `t < length env` length_take)

  1098   with assms(3) show ?thesis

  1099     by (smt nth_append)

  1100 qed

  1101 

  1102 lemma l_n_v_s3:

  1103   assumes "l0 < length env"

  1104   and "\<not> t \<le> l0"

  1105   shows "(take t env @ es @ drop t env) ! l0 = env ! l0"

  1106 proof(cases "t < length env")

  1107   case True

  1108    hence  h: "env = take t env @ drop t env" 

  1109             "length (take t env) = t"

  1110     apply (metis append_take_drop_id)

  1111     by (smt `t < length env` length_take)

  1112   with assms(2)  show ?thesis

  1113     by (smt nth_append)

  1114 next

  1115   case False

  1116   hence "take t env = env" by auto

  1117   with assms(1) show ?thesis

  1118     by (metis nth_append)

  1119 qed

  1120 

  1121 lemma lift_wf_cpg_test:

  1122   assumes "wf_cpg_test sts cpg = (True, sts')"

  1123   shows "wf_cpg_test (take t sts @ sts0 @ drop t sts) (lift_t t (length sts0) cpg) = 

  1124                (True, take t sts' @ sts0 @ drop t sts')"

  1125   using assms

  1126 proof(induct cpg arbitrary:t sts0 sts sts')

  1127   case (CInstr instr t sts0 sts sts')

  1128   obtain a0 l0 a1 l1 where eq_instr: "instr = ((a0, l0), (a1, l1))" 

  1129     by (metis prod.exhaust)

  1130   from CInstr

  1131   show ?case

  1132     by (auto simp:eq_instr lift_b_def)

  1133 next

  1134   case (CLabel l t sts0 sts sts')

  1135   thus ?case