1 header {* 

     2   Separation logic for TM

     3 *}

     4 

     5 theory Hoare_tm

     6 imports Hoare_gen My_block Data_slot

     7 begin

     8 

     9 

    10 ML {*

    11 fun pretty_terms ctxt trms =

    12   Pretty.block (Pretty.commas (map (Syntax.pretty_term ctxt) trms))

    13 *}

    14 

    15 lemma int_add_C :"x + (y::int) = y + x"

    16   by simp

    17 

    18 lemma int_add_A : "(x + y) + z = x + (y + (z::int))"

    19   by simp

    20 

    21 lemma int_add_LC: "x + (y + (z::int)) = y + (x + z)"

    22   by simp

    23 

    24 lemmas int_add_ac = int_add_A int_add_C int_add_LC

    25 

    26 method_setup prune = {* Scan.succeed (SIMPLE_METHOD' o (K (K prune_params_tac))) *} 

    27                        "pruning parameters"

    28 

    29 ML {*

    30 structure StepRules = Named_Thms

    31   (val name = @{binding "step"}

    32    val description = "Theorems for hoare rules for every step")

    33 *}

    34 

    35 ML {*

    36 structure FwdRules = Named_Thms

    37   (val name = @{binding "fwd"}

    38    val description = "Theorems for fwd derivation of seperation implication")

    39 *}

    40 

    41 setup {* StepRules.setup *}

    42 

    43 setup {* FwdRules.setup *}

    44 

    45 section {* Operational Semantics of TM *}

    46 

    47 datatype taction = W0 | W1 | L | R

    48 

    49 type_synonym tstate = nat

    50 

    51 type_synonym tm_inst = "(taction \<times> tstate) \<times> (taction \<times> tstate)"

    52 

    53 datatype Block = Oc | Bk

    54 

    55 type_synonym tconf = "nat \<times> (nat \<rightharpoonup> tm_inst) \<times> nat \<times> int \<times> (int \<rightharpoonup> Block)"

    56 

    57 fun next_tape :: "taction \<Rightarrow> (int \<times>  (int \<rightharpoonup> Block)) \<Rightarrow> (int \<times>  (int \<rightharpoonup> Block))"

    58 where "next_tape W0 (pos, m) = (pos, m(pos \<mapsto> Bk))" |

    59       "next_tape W1 (pos, m) = (pos, m(pos \<mapsto> Oc))" |

    60       "next_tape L  (pos, m) = (pos - 1, m)" |

    61       "next_tape R  (pos, m) = (pos + 1, m)"

    62 

    63 fun tstep :: "tconf \<Rightarrow> tconf"

    64   where "tstep (faults, prog, pc, pos, m) = 

    65               (case (prog pc) of

    66                   Some ((action0, pc0), (action1, pc1)) \<Rightarrow> 

    67                      case (m pos) of

    68                        Some Bk \<Rightarrow> (faults, prog, pc0, next_tape action0 (pos, m)) |

    69                        Some Oc \<Rightarrow> (faults, prog, pc1, next_tape action1 (pos, m)) |

    70                        None \<Rightarrow> (faults + 1, prog, pc, pos, m)

    71                 | None \<Rightarrow> (faults + 1, prog, pc, pos, m))"

    72 

    73 lemma tstep_splits: 

    74   "(P (tstep s)) = ((\<forall> faults prog pc pos m action0 pc0 action1 pc1. 

    75                           s = (faults, prog, pc, pos, m) \<longrightarrow> 

    76                           prog pc = Some ((action0, pc0), (action1, pc1)) \<longrightarrow> 

    77                           m pos = Some Bk \<longrightarrow> P (faults, prog, pc0, next_tape action0 (pos, m))) \<and>

    78                     (\<forall> faults prog pc pos m action0 pc0 action1 pc1. 

    79                           s = (faults, prog, pc, pos, m) \<longrightarrow> 

    80                           prog pc = Some ((action0, pc0), (action1, pc1)) \<longrightarrow> 

    81                           m pos = Some Oc \<longrightarrow> P (faults, prog, pc1, next_tape action1 (pos, m))) \<and>

    82                     (\<forall> faults prog pc pos m action0 pc0 action1 pc1. 

    83                           s = (faults, prog, pc, pos, m) \<longrightarrow> 

    84                           prog pc = Some ((action0, pc0), (action1, pc1)) \<longrightarrow> 

    85                           m pos = None \<longrightarrow> P (faults + 1, prog, pc, pos, m)) \<and>

    86                     (\<forall> faults prog pc pos m . 

    87                           s =  (faults, prog, pc, pos, m) \<longrightarrow>

    88                           prog pc  = None \<longrightarrow> P (faults + 1, prog, pc, pos, m))

    89                    )"

    90   by (case_tac s, auto split:option.splits Block.splits)

    91 

    92 datatype tresource = 

    93     TM int Block

    94   | TC nat tm_inst

    95   | TAt nat

    96   | TPos int

    97   | TFaults nat

    98 

    99 definition "tprog_set prog = {TC i inst | i inst. prog i = Some inst}"

   100 definition "tpc_set pc = {TAt pc}"

   101 definition "tmem_set m = {TM i n | i n. m (i) = Some n}"

   102 definition "tpos_set pos = {TPos pos}"

   103 definition "tfaults_set faults = {TFaults faults}"

   104 

   105 lemmas tpn_set_def = tprog_set_def tpc_set_def tmem_set_def tfaults_set_def tpos_set_def

   106 

   107 fun trset_of :: "tconf \<Rightarrow> tresource set"

   108   where "trset_of (faults, prog, pc, pos, m) = 

   109                tprog_set prog \<union> tpc_set pc \<union> tpos_set pos \<union> tmem_set m \<union> tfaults_set faults"

   110 

   111 interpretation tm: sep_exec tstep trset_of .

   112 

   113 section {* Assembly language and its program logic *}

   114 

   115 subsection {* The assembly language *}

   116 

   117 datatype tpg = 

   118    TInstr tm_inst

   119  | TLabel nat

   120  | TSeq tpg tpg

   121  | TLocal "(nat \<Rightarrow> tpg)"

   122 

   123 notation TLocal (binder "TL " 10)

   124 

   125 abbreviation tprog_instr :: "tm_inst \<Rightarrow> tpg" ("\<guillemotright> _" [61] 61)

   126 where "\<guillemotright> i \<equiv> TInstr i"

   127 

   128 abbreviation tprog_seq :: "tpg \<Rightarrow> tpg \<Rightarrow> tpg" (infixr ";" 52)

   129 where "c1 ; c2 \<equiv> TSeq c1 c2"

   130 

   131 definition "sg e = (\<lambda> s. s = e)"

   132 

   133 type_synonym tassert = "tresource set \<Rightarrow> bool"

   134 

   135 abbreviation t_hoare :: 

   136   "tassert \<Rightarrow> tassert  \<Rightarrow> tassert \<Rightarrow> bool" ("(\<lbrace>(1_)\<rbrace> / (_)/ \<lbrace>(1_)\<rbrace>)" 50)

   137   where "\<lbrace> p \<rbrace> c \<lbrace> q \<rbrace> == sep_exec.Hoare_gen tstep trset_of p c q"

   138 

   139 abbreviation it_hoare ::

   140   "(('a::sep_algebra) \<Rightarrow> tresource set \<Rightarrow> bool) \<Rightarrow> 

   141       ('a \<Rightarrow> bool) \<Rightarrow> (tresource set \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"

   142   ("(1_).(\<lbrace>(1_)\<rbrace> / (_)/ \<lbrace>(1_)\<rbrace>)" 50)

   143 where "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace> == sep_exec.IHoare tstep trset_of I P c Q"

   144 

   145 (*

   146 primrec tpg_len :: "tpg \<Rightarrow> nat" where 

   147   "tpg_len (TInstr ai) = 1" |

   148   "tpg_len (TSeq p1 p2) = tpg_len p1 + tpg_len " |

   149   "tpg_len (TLocal fp) = tpg_len (fp 0)" |

   150   "tpg_len (TLabel l) = 0" *)

   151 

   152 primrec tassemble_to :: "tpg \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> tassert" 

   153   where 

   154   "tassemble_to (TInstr ai) i j = (sg ({TC i ai}) ** <(j = i + 1)>)" |

   155   "tassemble_to (TSeq p1 p2) i j = (EXS j'. (tassemble_to p1 i j') ** (tassemble_to p2 j' j))" |

   156   "tassemble_to (TLocal fp) i j  = (EXS l. (tassemble_to (fp l) i j))" | 

   157   "tassemble_to (TLabel l) i j = <(i = j \<and> j = l)>"

   158 

   159 declare tassemble_to.simps [simp del]

   160 

   161 lemmas tasmp = tassemble_to.simps (2, 3, 4)

   162 

   163 abbreviation tasmb_to :: "nat \<Rightarrow> tpg \<Rightarrow> nat \<Rightarrow> tassert" ("_ :[ _ ]: _" [60, 60, 60] 60)

   164   where "i :[ tpg ]: j \<equiv> tassemble_to tpg i j"

   165 

   166 lemma EXS_intro: 

   167   assumes h: "(P x) s"

   168   shows "((EXS x. P(x))) s"

   169   by (smt h pred_ex_def sep_conj_impl)

   170 

   171 lemma EXS_elim: 

   172   assumes "(EXS x. P x) s"

   173   obtains x where "P x s"

   174   by (metis assms pred_ex_def)

   175 

   176 lemma EXS_eq:

   177   fixes x

   178   assumes h: "Q (p x)" 

   179   and h1: "\<And> y s. \<lbrakk>p y s\<rbrakk> \<Longrightarrow> y = x"

   180   shows "p x = (EXS x. p x)"

   181 proof

   182   fix s

   183   show "p x s = (EXS x. p x) s"

   184   proof

   185     assume "p x s"

   186     thus "(EXS x. p x) s" by (auto simp:pred_ex_def)

   187   next

   188     assume "(EXS x. p x) s"

   189     thus "p x s"

   190     proof(rule EXS_elim)

   191       fix y

   192       assume "p y s"

   193       from this[unfolded h1[OF this]] show "p x s" .

   194     qed

   195   qed

   196 qed

   197 

   198 definition "tpg_fold tpgs = foldr TSeq (butlast tpgs) (last tpgs)"

   199 

   200 lemma tpg_fold_sg: "tpg_fold [tpg] = tpg"

   201   by (simp add:tpg_fold_def)

   202 

   203 lemma tpg_fold_cons: 

   204   assumes h: "tpgs \<noteq> []"

   205   shows "tpg_fold (tpg#tpgs) = (tpg; (tpg_fold tpgs))"

   206   using h

   207 proof(induct tpgs arbitrary:tpg)

   208   case (Cons tpg1 tpgs1)

   209   thus ?case

   210   proof(cases "tpgs1 = []")

   211     case True

   212     thus ?thesis by (simp add:tpg_fold_def)

   213   next

   214     case False

   215     show ?thesis

   216     proof -

   217       have eq_1: "butlast (tpg # tpg1 # tpgs1) = tpg # (butlast (tpg1 # tpgs1))"

   218         by simp

   219       from False have eq_2: "last (tpg # tpg1 # tpgs1) = last (tpg1 # tpgs1)"

   220         by simp

   221       have eq_3: "foldr (op ;) (tpg # butlast (tpg1 # tpgs1)) (last (tpg1 # tpgs1)) = 

   222             (tpg ; (foldr (op ;) (butlast (tpg1 # tpgs1)) (last (tpg1 # tpgs1))))"

   223         by simp

   224       show ?thesis

   225         apply (subst (1) tpg_fold_def, unfold eq_1 eq_2 eq_3)

   226         by (fold tpg_fold_def, simp)

   227     qed

   228   qed

   229 qed auto

   230 

   231 lemmas tpg_fold_simps = tpg_fold_sg tpg_fold_cons

   232 

   233 lemma tpg_fold_app:

   234   assumes h1: "tpgs1 \<noteq> []" 

   235   and h2: "tpgs2 \<noteq> []"

   236   shows "i:[(tpg_fold (tpgs1 @ tpgs2))]:j = i:[(tpg_fold (tpgs1); tpg_fold tpgs2)]:j"

   237   using h1 h2

   238 proof(induct tpgs1 arbitrary: i j tpgs2)

   239   case (Cons tpg1' tpgs1')

   240   thus ?case (is "?L = ?R")

   241   proof(cases "tpgs1' = []")

   242     case False

   243     from h2 have "(tpgs1' @ tpgs2) \<noteq> []"

   244       by (metis Cons.prems(2) Nil_is_append_conv) 

   245     have "?L = (i :[ tpg_fold (tpg1' # (tpgs1' @ tpgs2)) ]: j )" by simp

   246     also have "\<dots> =  (i:[(tpg1'; (tpg_fold (tpgs1' @ tpgs2)))]:j )"

   247       by (simp add:tpg_fold_cons[OF `(tpgs1' @ tpgs2) \<noteq> []`])

   248     also have "\<dots> = ?R"

   249     proof -

   250       have "(EXS j'. i :[ tpg1' ]: j' \<and>* j' :[ tpg_fold (tpgs1' @ tpgs2) ]: j) =

   251               (EXS j'. (EXS j'a. i :[ tpg1' ]: j'a \<and>* j'a :[ tpg_fold tpgs1' ]: j') \<and>* 

   252                                j' :[ tpg_fold tpgs2 ]: j)"

   253       proof(default+)

   254         fix s

   255         assume "(EXS j'. i :[ tpg1' ]: j' \<and>* j' :[ tpg_fold (tpgs1' @ tpgs2) ]: j) s"

   256         thus "(EXS j'. (EXS j'a. i :[ tpg1' ]: j'a \<and>* j'a :[ tpg_fold tpgs1' ]: j') \<and>*

   257                   j' :[ tpg_fold tpgs2 ]: j) s"

   258         proof(elim EXS_elim)

   259           fix j'

   260           assume "(i :[ tpg1' ]: j' \<and>* j' :[ tpg_fold (tpgs1' @ tpgs2) ]: j) s"

   261           from this[unfolded Cons(1)[OF False Cons(3)] tassemble_to.simps]

   262           show "(EXS j'. (EXS j'a. i :[ tpg1' ]: j'a \<and>* j'a :[ tpg_fold tpgs1' ]: j') \<and>*

   263                            j' :[ tpg_fold tpgs2 ]: j) s"

   264           proof(elim sep_conjE EXS_elim)

   265             fix x y j'a xa ya

   266             assume h: "(i :[ tpg1' ]: j') x"

   267                       "x ## y" "s = x + y"

   268                       "(j' :[ tpg_fold tpgs1' ]: j'a) xa"

   269                       "(j'a :[ tpg_fold tpgs2 ]: j) ya"

   270                       " xa ## ya" "y = xa + ya"

   271             show "(EXS j'. (EXS j'a. i :[ tpg1' ]: j'a \<and>* 

   272                                 j'a :[ tpg_fold tpgs1' ]: j') \<and>* j' :[ tpg_fold tpgs2 ]: j) s"

   273                (is "(EXS j'. (?P j' \<and>* ?Q j')) s")

   274             proof(rule EXS_intro[where x = "j'a"])

   275               from `(j'a :[ tpg_fold tpgs2 ]: j) ya` have "(?Q j'a) ya" .

   276               moreover have "(?P j'a) (x + xa)" 

   277               proof(rule EXS_intro[where x = j'])

   278                 have "x + xa = x + xa" by simp

   279                 moreover from `x ## y` `y = xa + ya` `xa ## ya` 

   280                 have "x ## xa" by (metis sep_disj_addD) 

   281                 moreover note `(i :[ tpg1' ]: j') x` `(j' :[ tpg_fold tpgs1' ]: j'a) xa`

   282                 ultimately show "(i :[ tpg1' ]: j' \<and>* j' :[ tpg_fold tpgs1' ]: j'a) (x + xa)"

   283                   by (auto intro!:sep_conjI)

   284               qed

   285               moreover from `x##y` `y = xa + ya` `xa ## ya` 

   286               have "(x + xa) ## ya"

   287                 by (metis sep_disj_addI1 sep_disj_commuteI)

   288               moreover from `s = x + y` `y = xa + ya`

   289               have "s = (x + xa) + ya"

   290                 by (metis h(2) h(6) sep_add_assoc sep_disj_addD1 sep_disj_addD2) 

   291               ultimately show "(?P j'a \<and>* ?Q j'a) s"

   292                 by (auto intro!:sep_conjI)

   293             qed

   294           qed

   295         qed

   296       next

   297         fix s

   298         assume "(EXS j'. (EXS j'a. i :[ tpg1' ]: j'a \<and>* j'a :[ tpg_fold tpgs1' ]: j') \<and>*

   299                                     j' :[ tpg_fold tpgs2 ]: j) s"

   300         thus "(EXS j'. i :[ tpg1' ]: j' \<and>* j' :[ tpg_fold (tpgs1' @ tpgs2) ]: j) s"

   301         proof(elim EXS_elim sep_conjE)

   302           fix j' x y j'a xa ya

   303           assume h: "(j' :[ tpg_fold tpgs2 ]: j) y"

   304                     "x ## y" "s = x + y" "(i :[ tpg1' ]: j'a) xa"

   305                     "(j'a :[ tpg_fold tpgs1' ]: j') ya" "xa ## ya" "x = xa + ya"

   306           show "(EXS j'. i :[ tpg1' ]: j' \<and>* j' :[ tpg_fold (tpgs1' @ tpgs2) ]: j) s"

   307           proof(rule EXS_intro[where x = j'a])

   308             from `(i :[ tpg1' ]: j'a) xa` have "(i :[ tpg1' ]: j'a) xa" .

   309             moreover have "(j'a :[ tpg_fold (tpgs1' @ tpgs2) ]: j) (ya + y)"

   310             proof(unfold Cons(1)[OF False Cons(3)] tassemble_to.simps)

   311               show "(EXS j'. j'a :[ tpg_fold tpgs1' ]: j' \<and>* j' :[ tpg_fold tpgs2 ]: j) (ya + y)"

   312               proof(rule EXS_intro[where x = "j'"])

   313                 from `x ## y` `x = xa + ya` `xa ## ya`

   314                 have "ya ## y" by (metis sep_add_disjD)

   315                 moreover have "ya + y = ya + y" by simp

   316                 moreover note `(j'a :[ tpg_fold tpgs1' ]: j') ya` 

   317                                `(j' :[ tpg_fold tpgs2 ]: j) y`

   318                 ultimately show "(j'a :[ tpg_fold tpgs1' ]: j' \<and>* 

   319                                  j' :[ tpg_fold tpgs2 ]: j) (ya + y)"

   320                   by (auto intro!:sep_conjI)

   321               qed

   322             qed

   323             moreover from `s = x + y` `x = xa + ya`

   324             have "s = xa + (ya + y)"

   325               by (metis h(2) h(6) sep_add_assoc sep_add_disjD)

   326             moreover from `xa ## ya` `x ## y` `x = xa + ya`

   327             have "xa ## (ya + y)" by (metis sep_disj_addI3) 

   328             ultimately show "(i :[ tpg1' ]: j'a \<and>* j'a :[ tpg_fold (tpgs1' @ tpgs2) ]: j) s"

   329               by (auto intro!:sep_conjI)

   330           qed

   331         qed

   332       qed

   333       thus ?thesis 

   334         by (simp add:tassemble_to.simps, unfold tpg_fold_cons[OF False], 

   335              unfold tassemble_to.simps, simp)

   336     qed

   337     finally show ?thesis . 

   338   next

   339     case True

   340     thus ?thesis

   341       by (simp add:tpg_fold_cons[OF Cons(3)] tpg_fold_sg)

   342   qed 

   343 qed auto

   344  

   345 

   346 subsection {* Assertions and program logic for this assembly language *}

   347 

   348 definition "st l = sg (tpc_set l)"

   349 definition "ps p = sg (tpos_set p)" 

   350 definition "tm a v =sg ({TM a v})"

   351 definition "one i = tm i Oc"

   352 definition "zero i= tm i Bk"

   353 definition "any i = (EXS v. tm i v)"

   354 

   355 declare trset_of.simps[simp del]

   356 

   357 lemma stimes_sgD: "(sg x ** q) s \<Longrightarrow> q (s - x) \<and> x \<subseteq> s"

   358   apply(erule_tac sep_conjE)

   359   apply(unfold set_ins_def sg_def)

   360   by (metis Diff_Int2 Diff_Int_distrib2 Diff_Un Diff_cancel 

   361     Diff_empty Diff_idemp Diff_triv Int_Diff Un_Diff 

   362     Un_Diff_cancel inf_commute inf_idem sup_bot_right sup_commute sup_ge2)

   363 

   364 lemma stD: "(st i ** r) (trset_of (ft, prog, i', pos, mem))

   365        \<Longrightarrow> i' = i"

   366 proof -

   367   assume "(st i ** r) (trset_of (ft, prog, i', pos, mem))"

   368   from stimes_sgD [OF this[unfolded st_def], unfolded trset_of.simps]

   369   have "tpc_set i \<subseteq> tprog_set prog \<union> tpc_set i' \<union> tpos_set pos \<union>  

   370             tmem_set mem \<union> tfaults_set ft" by auto

   371   thus ?thesis

   372     by (unfold tpn_set_def, auto)

   373 qed

   374 

   375 lemma psD: "(ps p ** r) (trset_of (ft, prog, i', pos, mem))

   376        \<Longrightarrow> pos = p"

   377 proof -

   378   assume "(ps p ** r) (trset_of (ft, prog, i', pos, mem))"

   379   from stimes_sgD [OF this[unfolded ps_def], unfolded trset_of.simps]

   380   have "tpos_set p \<subseteq> tprog_set prog \<union> tpc_set i' \<union> 

   381                        tpos_set pos \<union> tmem_set mem \<union> tfaults_set ft"

   382     by simp

   383   thus ?thesis

   384     by (unfold tpn_set_def, auto)

   385 qed

   386 

   387 lemma codeD: "(st i ** sg {TC i inst} ** r) (trset_of (ft, prog, i', pos, mem))

   388        \<Longrightarrow> prog i = Some inst"

   389 proof -

   390   assume "(st i ** sg {TC i inst} ** r) (trset_of (ft, prog, i', pos, mem))"

   391   thus ?thesis

   392     apply(unfold sep_conj_def set_ins_def sg_def trset_of.simps tpn_set_def)

   393     by auto

   394 qed

   395 

   396 lemma memD: "((tm a v) ** r) (trset_of (ft, prog, i, pos, mem))  \<Longrightarrow> mem a = Some v"

   397 proof -

   398   assume "((tm a v) ** r) (trset_of (ft, prog, i, pos, mem))"

   399   from stimes_sgD[OF this[unfolded trset_of.simps tpn_set_def tm_def]]

   400   have "{TM a v} \<subseteq> {TC i inst |i inst. prog i = Some inst} \<union> {TAt i} \<union> 

   401     {TPos pos} \<union> {TM i n |i n. mem i = Some n} \<union> {TFaults ft}" by simp

   402   thus ?thesis by auto

   403 qed

   404 

   405 lemma t_hoare_seq: 

   406   "\<lbrakk>\<And> i j. \<lbrace>st i ** p\<rbrace> i:[c1]:j \<lbrace>st j ** q\<rbrace>; 

   407     \<And> j k. \<lbrace>st j ** q\<rbrace> j:[c2]:k \<lbrace>st k ** r\<rbrace>\<rbrakk> \<Longrightarrow>  \<lbrace>st i ** p\<rbrace> i:[(c1 ; c2)]:k \<lbrace>st k ** r\<rbrace>"

   408 proof -

   409   assume h: "\<And> i j. \<lbrace>st i ** p\<rbrace> i:[c1]:j \<lbrace>st j ** q\<rbrace>" 

   410             "\<And> j k. \<lbrace>st j ** q\<rbrace> j:[c2]:k \<lbrace>st k ** r\<rbrace>"

   411   show "\<lbrace>st i ** p\<rbrace> i:[(c1 ; c2)]:k \<lbrace>st k ** r\<rbrace>"

   412   proof(subst tassemble_to.simps, rule tm.code_exI)

   413     fix j'

   414     show "\<lbrace>st i \<and>* p\<rbrace>  i :[ c1 ]: j' \<and>* j' :[ c2 ]: k \<lbrace>st k \<and>* r\<rbrace>"

   415     proof(rule tm.composition)

   416       from h(1) show "\<lbrace>st i \<and>* p\<rbrace>  i :[ c1 ]: j' \<lbrace> st j' \<and>* q \<rbrace>" by auto

   417     next

   418       from h(2) show "\<lbrace>st j' \<and>* q\<rbrace>  j' :[ c2 ]: k \<lbrace>st k \<and>* r\<rbrace>" by auto

   419     qed

   420   qed

   421 qed

   422 

   423 lemma t_hoare_seq1:

   424    "\<lbrakk>\<And>j'. \<lbrace>st i ** p\<rbrace> i:[c1]:j' \<lbrace>st j' ** q\<rbrace>;

   425     \<And>j'. \<lbrace>st j' ** q\<rbrace> j':[c2]:k \<lbrace>st k' ** r\<rbrace>\<rbrakk> \<Longrightarrow>  

   426            \<lbrace>st i ** p\<rbrace> i:[(c1 ; c2)]:k \<lbrace>st k' ** r\<rbrace>"

   427 proof -

   428   assume h: "\<And>j'. \<lbrace>st i \<and>* p\<rbrace>  i :[ c1 ]: j' \<lbrace>st j' \<and>* q\<rbrace>" 

   429             "\<And>j'. \<lbrace>st j' \<and>* q\<rbrace>  j' :[ c2 ]: k \<lbrace>st k' \<and>* r\<rbrace>"

   430   show "\<lbrace>st i \<and>* p\<rbrace>  i :[ (c1 ; c2) ]: k \<lbrace>st k' \<and>* r\<rbrace>"

   431   proof(subst tassemble_to.simps, rule tm.code_exI)

   432     fix j'

   433     show "\<lbrace>st i \<and>* p\<rbrace>  i :[ c1 ]: j' \<and>* j' :[ c2 ]: k \<lbrace>st k' \<and>* r\<rbrace>"

   434     proof(rule tm.composition)

   435       from h(1) show "\<lbrace>st i \<and>* p\<rbrace>  i :[ c1 ]: j' \<lbrace> st j' \<and>* q \<rbrace>" by auto

   436     next

   437       from h(2) show " \<lbrace>st j' \<and>* q\<rbrace>  j' :[ c2 ]: k \<lbrace>st k' \<and>* r\<rbrace>" by auto

   438     qed

   439   qed

   440 qed

   441 

   442 lemma t_hoare_seq2:

   443  assumes h: "\<And>j. \<lbrace>st i ** p\<rbrace> i:[c1]:j \<lbrace>st k' \<and>* r\<rbrace>"

   444  shows "\<lbrace>st i ** p\<rbrace> i:[(c1 ; c2)]:j \<lbrace>st k' ** r\<rbrace>"

   445   apply (unfold tassemble_to.simps, rule tm.code_exI)

   446   by (rule tm.code_extension, rule h)

   447 

   448 lemma t_hoare_local: 

   449   assumes h: "(\<And>l. \<lbrace>st i \<and>* p\<rbrace>  i :[ c l ]: j \<lbrace>st k \<and>* q\<rbrace>)"

   450   shows "\<lbrace>st i ** p\<rbrace> i:[TLocal c]:j \<lbrace>st k ** q\<rbrace>" using h

   451   by (unfold tassemble_to.simps, intro tm.code_exI, simp)

   452 

   453 lemma t_hoare_label: 

   454       "(\<And>l. l = i \<Longrightarrow> \<lbrace>st l \<and>* p\<rbrace>  l :[ c l ]: j \<lbrace>st k \<and>* q\<rbrace>) \<Longrightarrow>

   455              \<lbrace>st i \<and>* p \<rbrace> 

   456                i:[(TLabel l; c l)]:j

   457              \<lbrace>st k \<and>* q\<rbrace>"

   458 by (unfold tassemble_to.simps, intro tm.code_exI tm.code_condI, clarify, auto)

   459 

   460 primrec t_split_cmd :: "tpg \<Rightarrow> (tpg \<times> tpg option)"

   461   where "t_split_cmd (\<guillemotright>inst) = (\<guillemotright>inst, None)" |

   462         "t_split_cmd (TLabel l) = (TLabel l, None)" |

   463         "t_split_cmd (TSeq c1 c2) = (case (t_split_cmd c2) of

   464                                       (c21, Some c22) \<Rightarrow> (TSeq c1 c21, Some c22) |

   465                                       (c21, None) \<Rightarrow> (c1, Some c21))" |

   466         "t_split_cmd (TLocal c) = (TLocal c, None)"

   467 

   468 definition "t_last_cmd tpg = (snd (t_split_cmd tpg))"

   469 

   470 declare t_last_cmd_def [simp]

   471 

   472 definition "t_blast_cmd tpg = (fst (t_split_cmd tpg))"

   473 

   474 declare t_blast_cmd_def [simp]

   475 

   476 lemma "t_last_cmd (c1; c2; (TLabel l)) = (Some (TLabel l))"

   477   by simp

   478 

   479 lemma "t_blast_cmd (c1; c2; TLabel l) = (c1; c2)"

   480   by simp

   481 

   482 lemma t_split_cmd_eq:

   483   assumes "t_split_cmd c = (c1, Some c2)"

   484   shows "(i:[c]:j) = (i:[(c1; c2)]:j)"

   485   using assms

   486 proof(induct c arbitrary: c1 c2 i j)

   487   case (TSeq cx cy)

   488   from `t_split_cmd (cx ; cy) = (c1, Some c2)`

   489   show ?case

   490     apply (simp split:prod.splits option.splits)

   491     apply (cases cy, auto split:prod.splits option.splits)

   492     proof -

   493       fix a

   494       assume h: "t_split_cmd cy = (a, Some c2)"

   495       show "i :[ (cx ; cy) ]: j = i :[ ((cx ; a) ; c2) ]: j"

   496         apply (simp only: tassemble_to.simps(2) TSeq(2)[OF h] sep_conj_exists)

   497         apply (simp add:sep_conj_ac)

   498         by (simp add:pred_ex_def, default, auto)

   499     qed

   500 qed auto

   501 

   502 lemma t_hoare_label_last_pre: 

   503   fixes l

   504   assumes h1: "t_split_cmd c = (c', Some (TLabel l))"

   505   and h2: "l = j \<Longrightarrow> \<lbrace>p\<rbrace> i:[c']:j \<lbrace>q\<rbrace>"

   506   shows "\<lbrace>p\<rbrace> i:[c]:j \<lbrace>q\<rbrace>"

   507 by (unfold t_split_cmd_eq[OF h1], 

   508     simp only:tassemble_to.simps sep_conj_cond, 

   509     intro tm.code_exI tm.code_condI, insert h2, auto)

   510 

   511 lemma t_hoare_label_last: 

   512   fixes l

   513   assumes h1: "t_last_cmd c = Some (TLabel l)"

   514   and h2: "l = j \<Longrightarrow> \<lbrace>p\<rbrace> i:[t_blast_cmd c]:j \<lbrace>q\<rbrace>"

   515   shows "\<lbrace>p\<rbrace> i:[c]:j \<lbrace>q\<rbrace>"

   516 proof -

   517     have "t_split_cmd c = (t_blast_cmd c, t_last_cmd c)"

   518       by simp

   519   from t_hoare_label_last_pre[OF this[unfolded h1]] h2

   520   show ?thesis by auto

   521 qed

   522 

   523 subsection {* Basic assertions for TM *}

   524 

   525 function ones :: "int \<Rightarrow> int \<Rightarrow> tassert" where

   526   "ones i j = (if j < i then <(i = j + 1)> else

   527                 (one i) ** ones (i + 1) j)"

   528 by auto

   529 termination by (relation "measure(\<lambda> (i::int, j). nat (j - i + 1))") auto

   530 

   531 lemma ones_base_simp: "j < i \<Longrightarrow> ones i j = <(i = j + 1)>"

   532   by simp

   533 

   534 lemma ones_step_simp: "\<not> j < i \<Longrightarrow> ones i j =  ((one i) ** ones (i + 1) j)"

   535   by simp

   536 

   537 lemmas ones_simps = ones_base_simp ones_step_simp

   538 

   539 declare ones.simps [simp del] ones_simps [simp]

   540 

   541 lemma ones_induct [case_names Base Step]:

   542   fixes P i j

   543   assumes h1: "\<And> i j. j < i \<Longrightarrow> P i j (<(i = j + (1::int))>)"

   544   and h2: "\<And> i j. \<lbrakk>\<not> j < i; P (i + 1) j (ones (i + 1) j)\<rbrakk> \<Longrightarrow> P i j ((one i) ** ones (i + 1) j)"

   545   shows "P i j (ones i j)"

   546 proof(induct i j rule:ones.induct)

   547   fix i j 

   548   assume ih: "(\<not> j < i \<Longrightarrow> P (i + 1) j (ones (i + 1) j))"

   549   show "P i j (ones i j)"

   550   proof(cases "j < i")

   551     case True

   552     with h1 [OF True]

   553     show ?thesis by auto

   554   next

   555     case False

   556     from h2 [OF False] and ih[OF False]

   557     have "P i j (one i \<and>* ones (i + 1) j)" by blast

   558     with False show ?thesis by auto

   559   qed

   560 qed

   561 

   562 function ones' ::  "int \<Rightarrow> int \<Rightarrow> tassert" where

   563   "ones' i j = (if j < i then <(i = j + 1)> else

   564                 ones' i (j - 1) ** one j)"

   565 by auto

   566 termination by (relation "measure(\<lambda> (i::int, j). nat (j - i + 1))") auto

   567 

   568 lemma ones_rev: "\<not> j < i \<Longrightarrow> (ones i j) = ((ones i (j - 1)) ** one j)"

   569 proof(induct i j rule:ones_induct)

   570   case Base

   571   thus ?case by auto

   572 next

   573   case (Step i j)

   574   show ?case

   575   proof(cases "j < i + 1")

   576     case True

   577     with Step show ?thesis

   578       by simp

   579   next

   580     case False

   581     with Step show ?thesis 

   582       by (auto simp:sep_conj_ac)

   583   qed

   584 qed

   585 

   586 lemma ones_rev_induct [case_names Base Step]:

   587   fixes P i j

   588   assumes h1: "\<And> i j. j < i \<Longrightarrow> P i j (<(i = j + (1::int))>)"

   589   and h2: "\<And> i j. \<lbrakk>\<not> j < i; P i (j - 1) (ones i (j - 1))\<rbrakk> \<Longrightarrow> P i j ((ones i (j - 1)) ** one j)"

   590   shows "P i j (ones i j)"

   591 proof(induct i j rule:ones'.induct)

   592   fix i j 

   593   assume ih: "(\<not> j < i \<Longrightarrow> P i (j - 1) (ones i (j - 1)))"

   594   show "P i j (ones i j)"

   595   proof(cases "j < i")

   596     case True

   597     with h1 [OF True]

   598     show ?thesis by auto

   599   next

   600     case False

   601     from h2 [OF False] and ih[OF False]

   602     have "P i j (ones i (j - 1) \<and>* one j)" by blast

   603     with ones_rev and False

   604     show ?thesis

   605       by simp

   606   qed

   607 qed

   608 

   609 function zeros :: "int \<Rightarrow> int \<Rightarrow> tassert" where

   610   "zeros i j = (if j < i then <(i = j + 1)> else

   611                 (zero i) ** zeros (i + 1) j)"

   612 by auto

   613 termination by (relation "measure(\<lambda> (i::int, j). nat (j - i + 1))") auto

   614 

   615 lemma zeros_base_simp: "j < i \<Longrightarrow> zeros i j = <(i = j + 1)>"

   616   by simp

   617 

   618 lemma zeros_step_simp: "\<not> j < i \<Longrightarrow> zeros i j = ((zero i) ** zeros (i + 1) j)"

   619   by simp

   620 

   621 declare zeros.simps [simp del]

   622 lemmas zeros_simps [simp] = zeros_base_simp zeros_step_simp

   623 

   624 lemma zeros_induct [case_names Base Step]:

   625   fixes P i j

   626   assumes h1: "\<And> i j. j < i \<Longrightarrow> P i j (<(i = j + (1::int))>)"

   627   and h2: "\<And> i j. \<lbrakk>\<not> j < i; P (i + 1) j (zeros (i + 1) j)\<rbrakk> \<Longrightarrow> 

   628                                    P i j ((zero i) ** zeros (i + 1) j)"

   629   shows "P i j (zeros i j)"

   630 proof(induct i j rule:zeros.induct)

   631   fix i j 

   632   assume ih: "(\<not> j < i \<Longrightarrow> P (i + 1) j (zeros (i + 1) j))"

   633   show "P i j (zeros i j)"

   634   proof(cases "j < i")

   635     case True

   636     with h1 [OF True]

   637     show ?thesis by auto

   638   next

   639     case False

   640     from h2 [OF False] and ih[OF False]

   641     have "P i j (zero i \<and>* zeros (i + 1) j)" by blast

   642     with False show ?thesis by auto

   643   qed

   644 qed

   645 

   646 lemma zeros_rev: "\<not> j < i \<Longrightarrow> (zeros i j) = ((zeros i (j - 1)) ** zero j)"

   647 proof(induct i j rule:zeros_induct)

   648   case (Base i j)

   649   thus ?case by auto

   650 next

   651   case (Step i j)

   652   show ?case

   653   proof(cases "j < i + 1")

   654     case True

   655     with Step show ?thesis by auto

   656   next

   657     case False

   658     with Step show ?thesis by (auto simp:sep_conj_ac)

   659   qed

   660 qed

   661 

   662 lemma zeros_rev_induct [case_names Base Step]:

   663   fixes P i j

   664   assumes h1: "\<And> i j. j < i \<Longrightarrow> P i j (<(i = j + (1::int))>)"

   665   and h2: "\<And> i j. \<lbrakk>\<not> j < i; P i (j - 1) (zeros i (j - 1))\<rbrakk> \<Longrightarrow> 

   666                        P i j ((zeros i (j - 1)) ** zero j)"

   667   shows "P i j (zeros i j)"

   668 proof(induct i j rule:ones'.induct)

   669   fix i j 

   670   assume ih: "(\<not> j < i \<Longrightarrow> P i (j - 1) (zeros i (j - 1)))"

   671   show "P i j (zeros i j)"

   672   proof(cases "j < i")

   673     case True

   674     with h1 [OF True]

   675     show ?thesis by auto

   676   next

   677     case False

   678     from h2 [OF False] and ih[OF False]

   679     have "P i j (zeros i (j - 1) \<and>* zero j)" by blast

   680     with zeros_rev and False

   681     show ?thesis by simp

   682   qed

   683 qed

   684 

   685 definition "rep i j k = ((ones i (i + (int k))) ** <(j = i + int k)>)"

   686 

   687 fun reps :: "int \<Rightarrow> int \<Rightarrow> nat list\<Rightarrow> tassert"

   688   where

   689   "reps i j [] = <(i = j + 1)>" |

   690   "reps i j [k] = (ones i (i + int k) ** <(j = i + int k)>)" |

   691   "reps i j (k # ks) = (ones i (i + int k) ** zero (i + int k + 1) ** reps (i + int k + 2) j ks)"

   692 

   693 lemma reps_simp3: "ks \<noteq> [] \<Longrightarrow> 

   694   reps i j (k # ks) = (ones i (i + int k) ** zero (i + int k + 1) ** reps (i + int k + 2) j ks)"

   695   by (cases ks, auto)

   696 

   697 definition "reps_sep_len ks = (if length ks \<le> 1 then 0 else (length ks) - 1)"

   698 

   699 definition "reps_ctnt_len ks = (\<Sum> k \<leftarrow> ks. (1 + k))"

   700 

   701 definition "reps_len ks = (reps_sep_len ks) + (reps_ctnt_len ks)"

   702 

   703 definition "splited xs ys zs = ((xs = ys @ zs) \<and> (ys \<noteq> []) \<and> (zs \<noteq> []))"

   704 

   705 lemma list_split: 

   706   assumes h: "k # ks = ys @ zs"

   707       and h1: "ys \<noteq> []"

   708   shows "(ys = [k] \<and> zs = ks) \<or> (\<exists> ys'. ys' \<noteq> [] \<and> ys = k # ys' \<and> ks = ys' @ zs)"

   709 proof(cases ys)

   710   case Nil

   711   with h1 show ?thesis by auto

   712 next

   713   case (Cons y' ys')

   714   with h have "k#ks = y'#(ys' @ zs)" by simp

   715   hence hh: "y' = k" "ks = ys' @ zs" by auto

   716   show ?thesis

   717   proof(cases "ys' = []")

   718     case False

   719     show ?thesis

   720     proof(rule disjI2)

   721       show " \<exists>ys'. ys' \<noteq> [] \<and> ys = k # ys' \<and> ks = ys' @ zs"

   722       proof(rule exI[where x = ys'])

   723         from False hh Cons show "ys' \<noteq> [] \<and> ys = k # ys' \<and> ks = ys' @ zs" by auto

   724       qed

   725     qed

   726   next

   727     case True

   728     show ?thesis

   729     proof(rule disjI1)

   730       from hh True Cons

   731       show "ys = [k] \<and> zs = ks" by auto

   732     qed

   733   qed

   734 qed

   735 

   736 lemma splited_cons[elim_format]: 

   737   assumes h: "splited (k # ks) ys zs"

   738   shows "(ys = [k] \<and> zs = ks) \<or> (\<exists> ys'. ys' \<noteq> [] \<and> ys = k # ys' \<and> splited ks ys' zs)"

   739 proof -

   740   from h have "k # ks = ys @ zs" "ys \<noteq> [] " unfolding splited_def by auto

   741   from list_split[OF this]

   742   have "ys = [k] \<and> zs = ks \<or> (\<exists>ys'. ys' \<noteq> [] \<and> ys = k # ys' \<and> ks = ys' @ zs)" .

   743   thus ?thesis

   744   proof

   745     assume " ys = [k] \<and> zs = ks" thus ?thesis by auto

   746   next

   747     assume "\<exists>ys'. ys' \<noteq> [] \<and> ys = k # ys' \<and> ks = ys' @ zs"

   748     then obtain ys' where hh: "ys' \<noteq> []" "ys = k # ys'" "ks = ys' @ zs" by auto

   749     show ?thesis

   750     proof(rule disjI2)

   751       show "\<exists>ys'. ys' \<noteq> [] \<and> ys = k # ys' \<and> splited ks ys' zs"

   752       proof(rule exI[where x = ys'])

   753         from h have "zs \<noteq> []" by (unfold splited_def, simp)

   754         with hh(1) hh(3)

   755         have "splited ks ys' zs"

   756           by (unfold splited_def, auto)

   757         with hh(1) hh(2) show "ys' \<noteq> [] \<and> ys = k # ys' \<and> splited ks ys' zs" by auto

   758       qed

   759     qed

   760   qed

   761 qed

   762 

   763 lemma splited_cons_elim:

   764   assumes h: "splited (k # ks) ys zs"

   765   and h1: "\<lbrakk>ys = [k]; zs = ks\<rbrakk> \<Longrightarrow> P"

   766   and h2: "\<And> ys'. \<lbrakk>ys' \<noteq> []; ys = k#ys'; splited ks ys' zs\<rbrakk> \<Longrightarrow> P"

   767   shows P

   768 proof(rule splited_cons[OF h])

   769   assume "ys = [k] \<and> zs = ks \<or> (\<exists>ys'. ys' \<noteq> [] \<and> ys = k # ys' \<and> splited ks ys' zs)"

   770   thus P

   771   proof

   772     assume hh: "ys = [k] \<and> zs = ks"

   773     show P

   774     proof(rule h1)

   775       from hh show "ys = [k]" by simp

   776     next

   777       from hh show "zs = ks" by simp

   778     qed

   779   next

   780     assume "\<exists>ys'. ys' \<noteq> [] \<and> ys = k # ys' \<and> splited ks ys' zs"

   781     then obtain ys' where hh: "ys' \<noteq> []" "ys = k # ys'"  "splited ks ys' zs" by auto

   782     from h2[OF this]

   783     show P .

   784   qed

   785 qed

   786 

   787 lemma list_nth_expand:

   788   "i < length xs \<Longrightarrow> xs = take i xs @ [xs!i] @ drop (Suc i) xs"

   789   by (metis Cons_eq_appendI append_take_drop_id drop_Suc_conv_tl eq_Nil_appendI)

   790 

   791 lemma reps_len_nil: "reps_len [] = 0"

   792    by (auto simp:reps_len_def reps_sep_len_def reps_ctnt_len_def)

   793 

   794 lemma reps_len_sg: "reps_len [k] = 1 + k"

   795   by (auto simp:reps_len_def reps_sep_len_def reps_ctnt_len_def)

   796 

   797 lemma reps_len_cons: "ks \<noteq> [] \<Longrightarrow> (reps_len (k # ks)) = 2 + k + reps_len ks "

   798 proof(induct ks arbitrary:k)

   799   case (Cons n ns)

   800   thus ?case

   801     by(cases "ns = []", 

   802       auto simp:reps_len_def reps_sep_len_def reps_ctnt_len_def)

   803 qed auto

   804 

   805 lemma reps_len_correct:

   806   assumes h: "(reps i j ks) s"

   807   shows "j = i + int (reps_len ks) - 1"

   808   using h

   809 proof(induct ks arbitrary:i j s)

   810   case Nil

   811   thus ?case

   812     by (auto simp:reps_len_nil pasrt_def)

   813 next

   814   case (Cons n ns)

   815   thus ?case

   816   proof(cases "ns = []")

   817     case False

   818     from Cons(2)[unfolded reps_simp3[OF False]]

   819     obtain s' where "(reps (i + int n + 2) j ns) s'"

   820       by (auto elim!:sep_conjE)

   821     from Cons.hyps[OF this]

   822     show ?thesis

   823       by (unfold reps_len_cons[OF False], simp)

   824   next

   825     case True

   826     with Cons(2)

   827     show ?thesis

   828       by (auto simp:reps_len_sg pasrt_def)

   829   qed

   830 qed

   831 

   832 lemma reps_len_expand: 

   833   shows "(EXS j. (reps i j ks)) = (reps i (i + int (reps_len ks) - 1) ks)"

   834 proof(default+)

   835   fix s

   836   assume "(EXS j. reps i j ks) s"

   837   with reps_len_correct show "reps i (i + int (reps_len ks) - 1) ks s"

   838     by (auto simp:pred_ex_def)

   839 next

   840   fix s

   841   assume "reps i (i + int (reps_len ks) - 1) ks s"

   842   thus "(EXS j. reps i j ks) s"  by (auto simp:pred_ex_def)

   843 qed

   844 

   845 lemma reps_len_expand1: "(EXS j. (reps i j ks \<and>* r)) = (reps i (i + int (reps_len ks) - 1) ks \<and>* r)"

   846 by (metis reps_len_def reps_len_expand sep.mult_commute sep_conj_exists1)

   847 

   848 lemma reps_splited:

   849   assumes h: "splited xs ys zs"

   850   shows "reps i j xs = (reps i (i + int (reps_len ys) - 1) ys \<and>* 

   851                         zero (i + int (reps_len ys)) \<and>* 

   852                         reps (i + int (reps_len ys) + 1) j zs)"

   853   using h

   854 proof(induct xs arbitrary: i j ys zs)

   855   case Nil

   856   thus ?case

   857     by (unfold splited_def, auto)

   858 next

   859   case (Cons k ks)

   860   from Cons(2)

   861   show ?case

   862   proof(rule splited_cons_elim)

   863     assume h: "ys = [k]" "zs = ks"

   864     with Cons(2)

   865     show ?thesis

   866     proof(cases "ks = []")

   867       case True

   868       with Cons(2) have False

   869         by (simp add:splited_def, cases ys, auto)

   870       thus ?thesis by auto

   871     next

   872       case False

   873       have ss: "i + int k + 1 = i + (1 + int k)"

   874            "i + int k + 2 = 2 + (i + int k)" by auto

   875       show ?thesis

   876         by (unfold h(1), unfold reps_simp3[OF False] reps.simps(2) 

   877             reps_len_sg, auto simp:sep_conj_ac,

   878             unfold ss h(2), simp)

   879     qed

   880   next

   881     fix ys'

   882     assume h: "ys' \<noteq> []" "ys = k # ys'" "splited ks ys' zs"

   883     hence nnks: "ks \<noteq> []"

   884       by (unfold splited_def, auto)

   885     have ss: "i + int k + 2 + int (reps_len ys') = 

   886               i + (2 + (int k + int (reps_len ys')))" by auto

   887     show ?thesis

   888       by (simp add: reps_simp3[OF nnks] reps_simp3[OF h(1)] 

   889                     Cons(1)[OF h(3)] h(2) 

   890                     reps_len_cons[OF h(1)]

   891                     sep_conj_ac, subst ss, simp)

   892   qed

   893 qed

   894 

   895 subsection {* A theory of list extension *}

   896 

   897 definition "list_ext n xs = xs @ replicate ((Suc n) - length xs) 0"

   898 

   899 lemma list_ext_len_eq: "length (list_ext a xs) = length xs + (Suc a - length xs)"

   900   by (metis length_append length_replicate list_ext_def)

   901 

   902 lemma list_ext_len: "a < length (list_ext a xs)"

   903   by (unfold list_ext_len_eq, auto)

   904 

   905 lemma list_ext_lt: "a < length xs \<Longrightarrow> list_ext a xs = xs"

   906   by (smt append_Nil2 list_ext_def replicate_0)

   907 

   908 lemma list_ext_lt_get: 

   909   assumes h: "a' < length xs"

   910   shows "(list_ext a xs)!a' = xs!a'"

   911 proof(cases "a < length xs")

   912   case True

   913   with h

   914   show ?thesis by (auto simp:list_ext_lt)

   915 next

   916   case False

   917   with h show ?thesis

   918     apply (unfold list_ext_def)

   919     by (metis nth_append)

   920 qed

   921 

   922 lemma list_ext_get_upd: "((list_ext a xs)[a:=v])!a = v"

   923   by (metis list_ext_len nth_list_update_eq)

   924 

   925 lemma nth_app: "length xs \<le> a \<Longrightarrow> (xs @ ys)!a = ys!(a - length xs)"

   926   by (metis not_less nth_append)

   927 

   928 lemma pred_exI: 

   929   assumes "(P(x) \<and>* r) s"

   930   shows "((EXS x. P(x)) \<and>* r) s"

   931   by (metis assms pred_ex_def sep_globalise)

   932 

   933 lemma list_ext_tail:

   934   assumes h1: "length xs \<le> a"

   935   and h2: "length xs \<le> a'"

   936   and h3: "a' \<le> a"

   937   shows "(list_ext a xs)!a' = 0"

   938 proof -

   939   from h1 h2

   940   have "a' - length xs < length (replicate (Suc a - length xs) 0)"

   941     by (metis diff_less_mono h3 le_imp_less_Suc length_replicate)

   942   moreover from h1 have "replicate (Suc a - length xs) 0 \<noteq> []"

   943     by (smt empty_replicate)

   944   ultimately have "(replicate (Suc a - length xs) 0)!(a' - length xs) = 0"

   945     by (metis length_replicate nth_replicate)

   946   moreover have "(xs @ (replicate (Suc a - length xs) 0))!a' = 

   947             (replicate (Suc a - length xs) 0)!(a' - length xs)"

   948     by (rule nth_app[OF h2])

   949   ultimately show ?thesis

   950     by (auto simp:list_ext_def)

   951 qed

   952 

   953 lemmas list_ext_simps = list_ext_lt_get list_ext_lt list_ext_len list_ext_len_eq

   954 

   955 lemma listsum_upd_suc:

   956   "a < length ks \<Longrightarrow> listsum (map Suc (ks[a := Suc (ks ! a)]))= (Suc (listsum (map Suc ks)))"

   957 by (smt Ex_list_of_length Skolem_list_nth elem_le_listsum_nat 

   958      length_induct length_list_update length_map length_splice 

   959      list_eq_iff_nth_eq list_ext_get_upd list_ext_lt_get list_update_beyond 

   960      list_update_id list_update_overwrite list_update_same_conv list_update_swap 

   961      listsum_update_nat map_eq_imp_length_eq map_update neq_if_length_neq 

   962      nth_equalityI nth_list_update nth_list_update_eq nth_list_update_neq nth_map reps_sep_len_def)

   963 

   964 lemma reps_len_suc:

   965   assumes "a < length ks"

   966   shows "reps_len (ks[a:=Suc(ks!a)]) = 1 + reps_len ks"

   967 proof(cases "length ks \<le> 1")

   968   case True

   969   with `a < length ks` 

   970   obtain k where "ks = [k]" "a = 0"

   971     by (smt length_0_conv length_Suc_conv)

   972   thus ?thesis

   973       apply (unfold `ks = [k]` `a = 0`)

   974       by (unfold reps_len_def reps_sep_len_def reps_ctnt_len_def, auto)

   975 next

   976   case False

   977   have "Suc = (op + (Suc 0))"

   978     by (default, auto)

   979   with listsum_upd_suc[OF `a < length ks`] False

   980   show ?thesis

   981      by (unfold reps_len_def reps_sep_len_def reps_ctnt_len_def, simp)

   982 qed

   983   

   984 lemma ks_suc_len:

   985   assumes h1: "(reps i j ks) s"

   986   and h2: "ks!a = v"

   987   and h3: "a < length ks"

   988   and h4: "(reps i j' (ks[a:=Suc v])) s'"

   989   shows "j' = j + int (reps_len (list_ext a ks)) - int (reps_len ks) + 1"

   990 proof -

   991   from reps_len_correct[OF h1, unfolded list_ext_len_eq]

   992        reps_len_correct[OF h4, unfolded list_ext_len_eq] 

   993        reps_len_suc[OF `a < length ks`] h2 h3

   994   show ?thesis

   995     by (unfold list_ext_lt[OF `a < length ks`], auto)

   996 qed

   997 

   998 lemma ks_ext_len:

   999   assumes h1: "(reps i j ks) s"

  1000   and h3: "length ks \<le> a"

  1001   and h4: "reps i j' (list_ext a ks) s'"

  1002   shows "j' = j + int (reps_len (list_ext a ks)) - int (reps_len ks)"

  1003 proof -

  1004   from reps_len_correct[OF h1, unfolded  list_ext_len_eq]

  1005     and reps_len_correct[OF h4, unfolded list_ext_len_eq]

  1006   h3

  1007   show ?thesis by auto

  1008 qed

  1009 

  1010 definition 

  1011   "reps' i j ks = 

  1012      (if ks = [] then (<(i = j + 1)>)  else (reps i (j - 1) ks \<and>* zero j))"

  1013 

  1014 lemma reps'_expand: 

  1015   assumes h: "ks \<noteq> []"

  1016   shows "(EXS j. reps' i j ks) = reps' i (i + int (reps_len ks)) ks"

  1017 proof -

  1018   show ?thesis

  1019   proof(default+)

  1020     fix s

  1021     assume "(EXS j. reps' i j ks) s"

  1022     with h have "(EXS j. reps i (j - 1) ks \<and>* zero j) s" 

  1023       by (simp add:reps'_def)

  1024     hence "(reps i (i + int (reps_len ks) - 1) ks \<and>* zero (i + int (reps_len ks))) s"

  1025     proof(elim EXS_elim)

  1026       fix j

  1027       assume "(reps i (j - 1) ks \<and>* zero j) s"

  1028       then obtain s1 s2 where "s = s1 + s2" "s1 ## s2" "reps i (j - 1) ks s1" "zero j s2"

  1029         by (auto elim!:sep_conjE)

  1030       from reps_len_correct[OF this(3)]

  1031       have "j = i + int (reps_len ks)" by auto

  1032       with `reps i (j - 1) ks s1` have "reps i (i + int (reps_len ks) - 1) ks s1"

  1033         by simp

  1034       moreover from `j = i + int (reps_len ks)` and `zero j s2`

  1035       have "zero (i + int (reps_len ks)) s2" by auto

  1036       ultimately show "(reps i (i + int (reps_len ks) - 1) ks \<and>* zero (i + int (reps_len ks))) s"

  1037         using `s = s1 + s2` `s1 ## s2` by (auto intro!:sep_conjI)

  1038     qed

  1039     thus "reps' i (i + int (reps_len ks)) ks s"

  1040       by (simp add:h reps'_def)

  1041   next

  1042     fix s 

  1043     assume "reps' i (i + int (reps_len ks)) ks s"

  1044     thus "(EXS j. reps' i j ks) s"

  1045       by (auto intro!:EXS_intro)

  1046   qed

  1047 qed

  1048 

  1049 lemma reps'_len_correct: 

  1050   assumes h: "(reps' i j ks) s"

  1051   and h1: "ks \<noteq> []"

  1052   shows "(j = i + int (reps_len ks))"

  1053 proof -

  1054   from h1 have "reps' i j ks s = (reps i (j - 1) ks \<and>* zero j) s" by (simp add:reps'_def)

  1055   from h[unfolded this]

  1056   obtain s' where "reps i (j - 1) ks s'"

  1057     by (auto elim!:sep_conjE)

  1058   from reps_len_correct[OF this]

  1059   show ?thesis by simp

  1060 qed

  1061 

  1062 lemma reps'_append:

  1063   "reps' i j (ks1 @ ks2) = (EXS m. (reps' i (m - 1) ks1 \<and>* reps' m j ks2))"

  1064 proof(cases "ks1 = []")

  1065   case True

  1066   thus ?thesis

  1067     by (auto simp:reps'_def pred_ex_def pasrt_def set_ins_def sep_conj_def)

  1068 next

  1069   case False

  1070   show ?thesis

  1071   proof(cases "ks2 = []")

  1072     case False

  1073     from `ks1 \<noteq> []` and `ks2 \<noteq> []` 

  1074     have "splited (ks1 @ ks2) ks1 ks2" by (auto simp:splited_def)

  1075     from reps_splited[OF this, of i "j - 1"]

  1076     have eq_1: "reps i (j - 1) (ks1 @ ks2) =

  1077            (reps i (i + int (reps_len ks1) - 1) ks1 \<and>*

  1078            zero (i + int (reps_len ks1)) \<and>* 

  1079            reps (i + int (reps_len ks1) + 1) (j - 1) ks2)" .

  1080     from `ks1 \<noteq> []`

  1081     have eq_2: "reps' i j (ks1 @ ks2) = (reps i (j - 1) (ks1 @ ks2) \<and>* zero j)"

  1082       by (unfold reps'_def, simp)

  1083     show ?thesis

  1084     proof(default+)

  1085       fix s

  1086       assume "reps' i j (ks1 @ ks2) s"

  1087       show "(EXS m. reps' i (m - 1) ks1 \<and>* reps' m j ks2) s"

  1088       proof(rule EXS_intro[where x = "i + int(reps_len ks1) + 1"])

  1089         from `reps' i j (ks1 @ ks2) s`[unfolded eq_2 eq_1]

  1090         and `ks1 \<noteq> []` `ks2 \<noteq> []`

  1091         show "(reps' i (i + int (reps_len ks1) + 1 - 1) ks1 \<and>* 

  1092                          reps' (i + int (reps_len ks1) + 1) j ks2) s"

  1093           by (unfold reps'_def, simp, sep_cancel+)

  1094       qed

  1095     next

  1096       fix s

  1097       assume "(EXS m. reps' i (m - 1) ks1 \<and>* reps' m j ks2) s"

  1098       thus "reps' i j (ks1 @ ks2) s"

  1099       proof(elim EXS_elim)

  1100         fix m

  1101         assume "(reps' i (m - 1) ks1 \<and>* reps' m j ks2) s"

  1102         then obtain s1 s2 where h: 

  1103           "s = s1 + s2" "s1 ## s2" "reps' i (m - 1) ks1 s1"

  1104           " reps' m j ks2 s2" by (auto elim!:sep_conjE)

  1105         from reps'_len_correct[OF this(3) `ks1 \<noteq> []`]

  1106         have eq_m: "m = i + int (reps_len ks1) + 1" by simp

  1107         have "((reps i (i + int (reps_len ks1) - 1) ks1 \<and>* zero (i + int (reps_len ks1))) \<and>* 

  1108                ((reps (i + int (reps_len ks1) + 1) (j - 1) ks2) \<and>* zero j)) s"

  1109           (is "(?P \<and>* ?Q) s") 

  1110         proof(rule sep_conjI)

  1111           from h(3) eq_m `ks1 \<noteq> []` show "?P s1"

  1112             by (simp add:reps'_def)

  1113         next

  1114           from h(4) eq_m `ks2 \<noteq> []` show "?Q s2"

  1115             by (simp add:reps'_def)

  1116         next

  1117           from h(2) show "s1 ## s2" .

  1118         next

  1119           from h(1) show "s = s1 + s2" .

  1120         qed

  1121         thus "reps' i j (ks1 @ ks2) s"

  1122           by (unfold eq_2 eq_1, auto simp:sep_conj_ac)

  1123       qed

  1124     qed

  1125   next

  1126     case True

  1127     have "-1 + j = j - 1" by auto

  1128     with `ks1 \<noteq> []` True

  1129     show ?thesis

  1130       apply (auto simp:reps'_def pred_ex_def pasrt_def)

  1131       apply (unfold `-1 + j = j - 1`)

  1132       by (fold sep_empty_def, simp only:sep_conj_empty)

  1133   qed

  1134 qed

  1135