1 header {* 

     2   Separation logic for Turing Machines

     3 *}

     4 

     5 theory Hoare_tm3

     6 imports Hoare_gen My_block Data_slot FMap

     7 begin

     8 

     9 notation FMap.lookup (infixl "$" 999)

    10 

    11 ML {*

    12 fun pretty_terms ctxt trms =

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

    14 *}

    15 

    16 ML {*

    17 structure StepRules = Named_Thms

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

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

    20 *}

    21 

    22 ML {*

    23 structure FwdRules = Named_Thms

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

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

    26 *}

    27 

    28 setup {* StepRules.setup *}

    29 setup {* FwdRules.setup *}

    30 

    31 method_setup prune = 

    32   {* Scan.succeed (SIMPLE_METHOD' o (K (K prune_params_tac))) *} 

    33   "pruning parameters"

    34 

    35 lemma int_add_C: 

    36   "x + (y::int) = y + x"

    37   by simp

    38 

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

    40   by simp

    41 

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

    43   by simp

    44 

    45 lemmas int_add_ac = int_add_A int_add_C int_add_LC

    46 

    47 

    48 section {* Operational Semantics of TM *}

    49 

    50 datatype taction = W0 | W1 | L | R

    51 

    52 type_synonym tstate = nat

    53 

    54 datatype Block = Oc | Bk

    55 

    56 (* the successor state when tape symbol is Bk or Oc, respectively *)

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

    58 

    59 (* - number of faults (nat)

    60    - TM program (nat \<rightharpoonup> tm_inst)

    61    - current state (nat)

    62    - position of head (int)

    63    - tape (int \<rightharpoonup> Block)

    64 *)

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

    66 

    67 (* updates the position/tape according to an action *)

    68 fun 

    69   next_tape :: "taction \<Rightarrow> (int \<times>  (int f\<rightharpoonup> Block)) \<Rightarrow> (int \<times>  (int f\<rightharpoonup> Block))"

    70 where 

    71   "next_tape W0 (pos, m) = (pos, m(pos f\<mapsto> Bk))" |

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

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

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

    75 

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

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

    78               (case (prog $ pc) of

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

    80                      case (m $ pos) of

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

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

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

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

    85 

    86 lemma tstep_splits: 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   102                    )"

   103   by (cases s) (auto split: option.splits Block.splits)

   104 

   105 datatype tresource = 

   106     TM int Block      (* at the position int of the tape is a Bl or Oc *)

   107   | TC nat tm_inst    (* at the address nat is a certain instruction *)

   108   | TAt nat           (* TM is at state nat*)

   109   | TPos int          (* head of TM is at position int *)

   110   | TFaults nat       (* there are nat faults *)

   111 

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

   113 definition "tpc_set pc = {TAt pc}"

   114 definition "tmem_set m = {TM i n | i n. m $ i = Some n}"

   115 definition "tpos_set pos = {TPos pos}"

   116 definition "tfaults_set faults = {TFaults faults}"

   117 

   118 lemmas tpn_set_def = tprog_set_def tpc_set_def tmem_set_def tfaults_set_def tpos_set_def

   119 

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

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

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

   123 

   124 interpretation tm: sep_exec tstep trset_of .

   125 

   126 

   127 

   128 section {* Assembly language for TMs and its program logic *}

   129 

   130 subsection {* The assembly language *}

   131 

   132 datatype tpg = 

   133    TInstr tm_inst

   134  | TLabel nat

   135  | TSeq tpg tpg

   136  | TLocal "nat \<Rightarrow> tpg"

   137 

   138 notation TLocal (binder "TL " 10)

   139 

   140 abbreviation 

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

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

   143 

   144 abbreviation tprog_seq :: 

   145   "tpg \<Rightarrow> tpg \<Rightarrow> tpg" (infixr ";" 52)

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

   147 

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

   149 

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

   151 

   152 abbreviation 

   153   t_hoare :: "tassert \<Rightarrow> tassert  \<Rightarrow> tassert \<Rightarrow> bool" ("(\<lbrace>(1_)\<rbrace>/ (_)/ \<lbrace>(1_)\<rbrace>)" 50)

   154 where 

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

   156 

   157 abbreviation it_hoare ::

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

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

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

   161 

   162 (*

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

   164   "tpg_len (TInstr ai) = 1" |

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

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

   167   "tpg_len (TLabel l) = 0" 

   168 *)

   169 

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

   171   where 

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

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

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

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

   176 

   177 declare tassemble_to.simps [simp del]

   178 

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

   180 

   181 abbreviation 

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

   183   where 

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

   185 

   186 lemma EXS_intro: 

   187   assumes h: "(P x) s"

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

   189   by (smt h pred_ex_def sep_conj_impl)

   190 

   191 lemma EXS_elim: 

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

   193   obtains x where "P x s"

   194   by (metis assms pred_ex_def)

   195 

   196 lemma EXS_eq:

   197   fixes x

   198   assumes h: "Q (p x)" 

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

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

   201 proof

   202   fix s

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

   204   proof

   205     assume "p x s"

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

   207   next

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

   209     thus "p x s"

   210     proof(rule EXS_elim)

   211       fix y

   212       assume "p y s"

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

   214     qed

   215   qed

   216 qed

   217 

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

   219 

   220 lemma tpg_fold_sg: 

   221   "tpg_fold [tpg] = tpg"

   222   by (simp add:tpg_fold_def)

   223 

   224 lemma tpg_fold_cons: 

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

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

   227   using h

   228 proof(induct tpgs arbitrary:tpg)

   229   case (Cons tpg1 tpgs1)

   230   thus ?case

   231   proof(cases "tpgs1 = []")

   232     case True

   233     thus ?thesis by (simp add:tpg_fold_def)

   234   next

   235     case False

   236     show ?thesis

   237     proof -

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

   239         by simp

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

   241         by simp

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

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

   244         by simp

   245       show ?thesis

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

   247         by (fold tpg_fold_def, simp)

   248     qed

   249   qed

   250 qed auto

   251 

   252 lemmas tpg_fold_simps = tpg_fold_sg tpg_fold_cons

   253 

   254 lemma tpg_fold_app:

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

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

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

   258   using h1 h2

   259 proof(induct tpgs1 arbitrary: i j tpgs2)

   260   case (Cons tpg1' tpgs1')

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

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

   263     case False

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

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

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

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

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

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

   270     proof -

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

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

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

   274       proof(default+)

   275         fix s

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

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

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

   279         proof(elim EXS_elim)

   280           fix j'

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

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

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

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

   285           proof(elim sep_conjE EXS_elim)

   286             fix x y j'a xa ya

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

   288                       "x ## y" "s = x + y"

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

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

   291                       " xa ## ya" "y = xa + ya"

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

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

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

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

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

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

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

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

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

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

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

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

   304                   by (auto intro!:sep_conjI)

   305               qed

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

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

   308                 by (metis sep_disj_addI1 sep_disj_commuteI)

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

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

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

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

   313                 by (auto intro!:sep_conjI)

   314             qed

   315           qed

   316         qed

   317       next

   318         fix s

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

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

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

   322         proof(elim EXS_elim sep_conjE)

   323           fix j' x y j'a xa ya

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   341                   by (auto intro!:sep_conjI)

   342               qed

   343             qed

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

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

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

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

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

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

   350               by (auto intro!:sep_conjI)

   351           qed

   352         qed

   353       qed

   354       thus ?thesis 

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

   356              unfold tassemble_to.simps, simp)

   357     qed

   358     finally show ?thesis . 

   359   next

   360     case True

   361     thus ?thesis

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

   363   qed 

   364 qed auto

   365  

   366 

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

   368 

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

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

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

   372 definition "one i = tm i Oc"

   373 definition "zero i= tm i Bk"

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

   375 

   376 declare trset_of.simps[simp del]

   377 

   378 lemma stimes_sgD: 

   379   "(sg x \<and>* q) s \<Longrightarrow> q (s - x) \<and> x \<subseteq> s"

   380   apply(erule_tac sep_conjE)

   381   apply(unfold set_ins_def sg_def)

   382   by (metis Diff_Int Diff_cancel Diff_empty Un_Diff sup.cobounded1 sup_bot.left_neutral sup_commute)

   383   

   384 lemma stD: 

   385   "(st i \<and>* r) (trset_of (ft, prog, i', pos, mem)) \<Longrightarrow> i' = i"

   386 proof -

   387   assume "(st i \<and>* r) (trset_of (ft, prog, i', pos, mem))"

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

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

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

   391   thus ?thesis

   392     by (unfold tpn_set_def, auto)

   393 qed

   394 

   395 lemma psD: 

   396   "(ps p \<and>* r) (trset_of (ft, prog, i', pos, mem)) \<Longrightarrow> pos = p"

   397 proof -

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

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

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

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

   402     by simp

   403   thus ?thesis

   404     by (unfold tpn_set_def, auto)

   405 qed

   406 

   407 lemma codeD: "(st i \<and>* sg {TC i inst} \<and>* r) (trset_of (ft, prog, i', pos, mem))

   408        \<Longrightarrow> prog $ i = Some inst"

   409 proof -

   410   assume "(st i \<and>* sg {TC i inst} \<and>* r) (trset_of (ft, prog, i', pos, mem))"

   411   thus ?thesis

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

   413     by auto

   414 qed

   415 

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

   417 proof -

   418   assume "((tm a v) \<and>* r) (trset_of (ft, prog, i, pos, mem))"

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

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

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

   422   thus ?thesis by auto

   423 qed

   424 

   425 lemma t_hoare_seq: 

   426   assumes a1: "\<And> i j. \<lbrace>st i \<and>* p\<rbrace> i:[c1]:j \<lbrace>st j \<and>* q\<rbrace>"

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

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

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

   430   fix j'

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

   432   proof(rule tm.composition)

   433     from a1 show "\<lbrace>st i \<and>* p\<rbrace>  i:[ c1 ]:j' \<lbrace>st j' \<and>* q\<rbrace>" by auto

   434   next

   435     from a2 show "\<lbrace>st j' \<and>* q\<rbrace>  j':[ c2 ]:k \<lbrace>st k \<and>* r\<rbrace>" by auto

   436   qed

   437 qed

   438 

   439 

   440 lemma t_hoare_seq1:

   441   assumes a1: "\<And>j'. \<lbrace>st i \<and>* p\<rbrace> i:[c1]:j' \<lbrace>st j' \<and>* q\<rbrace>"

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

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

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

   445   fix j'

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

   447   proof(rule tm.composition)

   448     from a1 show "\<lbrace>st i \<and>* p\<rbrace>  i:[ c1 ]:j' \<lbrace>st j' \<and>* q\<rbrace>" by auto

   449   next

   450     from a2 show " \<lbrace>st j' \<and>* q\<rbrace>  j':[ c2 ]:k \<lbrace>st k' \<and>* r\<rbrace>" by auto

   451   qed

   452 qed

   453 

   454 lemma t_hoare_seq2:

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

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

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

   458   by (rule tm.code_extension, rule h)

   459 

   460 lemma t_hoare_local: 

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

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

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

   464 

   465 lemma t_hoare_label: 

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

   467   shows "\<lbrace>st i \<and>* p\<rbrace> i:[(TLabel l; c l)]:j \<lbrace>st k \<and>* q\<rbrace>"

   468 using assms

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

   470 

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

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

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

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

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

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

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

   478 

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

   480 

   481 declare t_last_cmd_def [simp]

   482 

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

   484 

   485 declare t_blast_cmd_def [simp]

   486 

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

   488   by simp

   489 

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

   491   by simp

   492 

   493 lemma t_split_cmd_eq:

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

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

   496   using assms

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

   498   case (TSeq cx cy)

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

   500   show ?case

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

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

   503     proof -

   504       fix a

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

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

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

   508         apply (simp add:sep_conj_ac)

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

   510     qed

   511 qed auto

   512 

   513 lemma t_hoare_label_last_pre: 

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

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

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

   517 by (unfold t_split_cmd_eq[OF h1], 

   518     simp only:tassemble_to.simps sep_conj_cond, 

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

   520 

   521 lemma t_hoare_label_last: 

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

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

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

   525 proof -

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

   527       by simp

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

   529   show ?thesis by auto

   530 qed

   531 

   532 

   533 subsection {* Basic assertions for TM *}

   534 

   535 (* ones between tape position i and j *)

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

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

   538                else (one i) \<and>* ones (i + 1) j)"

   539 by auto

   540 

   541 termination 

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

   543 

   544 lemma ones_base_simp: 

   545   "j < i \<Longrightarrow> ones i j = <(i = j + 1)>"

   546   by simp

   547 

   548 lemma ones_step_simp: 

   549   "\<not> j < i \<Longrightarrow> ones i j =  ((one i) \<and>* ones (i + 1) j)"

   550   by simp

   551 

   552 lemmas ones_simps = ones_base_simp ones_step_simp

   553 

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

   555 

   556 lemma ones_induct [case_names Base Step]:

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

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

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

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

   561   fix i j 

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

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

   564   proof(cases "j < i")

   565     case True

   566     with h1 [OF True]

   567     show ?thesis by auto

   568   next

   569     case False

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

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

   572     with False show ?thesis by auto

   573   qed

   574 qed

   575 

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

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

   578                 else ones' i (j - 1) \<and>* one j)"

   579 by auto

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

   581 

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

   583 proof(induct i j rule:ones_induct)

   584   case Base

   585   thus ?case by auto

   586 next

   587   case (Step i j)

   588   show ?case

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

   590     case True

   591     with Step show ?thesis

   592       by simp

   593   next

   594     case False

   595     with Step show ?thesis 

   596       by (auto simp:sep_conj_ac)

   597   qed

   598 qed

   599 

   600 lemma ones_rev_induct [case_names Base Step]:

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

   602   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)"

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

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

   605   fix i j 

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

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

   608   proof(cases "j < i")

   609     case True

   610     with h1 [OF True]

   611     show ?thesis by auto

   612   next

   613     case False

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

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

   616     with ones_rev and False

   617     show ?thesis

   618       by simp

   619   qed

   620 qed

   621 

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

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

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

   625 by auto

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

   627 

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

   629   by simp

   630 

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

   632   by simp

   633 

   634 declare zeros.simps [simp del]

   635 lemmas zeros_simps [simp] = zeros_base_simp zeros_step_simp

   636 

   637 lemma zeros_induct [case_names Base Step]:

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

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

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

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

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

   643   fix i j 

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

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

   646   proof(cases "j < i")

   647     case True

   648     with h1 [OF True]

   649     show ?thesis by auto

   650   next

   651     case False

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

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

   654     with False show ?thesis by auto

   655   qed

   656 qed

   657 

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

   659 proof(induct i j rule:zeros_induct)

   660   case (Base i j)

   661   thus ?case by auto

   662 next

   663   case (Step i j)

   664   show ?case

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

   666     case True

   667     with Step show ?thesis by auto

   668   next

   669     case False

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

   671   qed

   672 qed

   673 

   674 lemma zeros_rev_induct [case_names Base Step]:

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

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

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

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

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

   680   fix i j 

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

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

   683   proof(cases "j < i")

   684     case True

   685     with h1 [OF True]

   686     show ?thesis by auto

   687   next

   688     case False

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

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

   691     with zeros_rev and False

   692     show ?thesis by simp

   693   qed

   694 qed

   695 

   696 definition "rep i j k = ((ones i (i + (int k))) \<and>* <(j = i + int k)>)"

   697 

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

   699   where

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

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

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

   703 

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

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

   706   by (cases ks, auto)

   707 

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

   709 

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

   711 

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

   713 

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

   715 

   716 lemma list_split: 

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

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

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

   720 proof(cases ys)

   721   case Nil

   722   with h1 show ?thesis by auto

   723 next

   724   case (Cons y' ys')

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

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

   727   show ?thesis

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

   729     case False

   730     show ?thesis

   731     proof(rule disjI2)

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

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

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

   735       qed

   736     qed

   737   next

   738     case True

   739     show ?thesis

   740     proof(rule disjI1)

   741       from hh True Cons

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

   743     qed

   744   qed

   745 qed

   746 

   747 lemma splited_cons[elim_format]: 

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

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

   750 proof -

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

   752   from list_split[OF this]

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

   754   thus ?thesis

   755   proof

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

   757   next

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

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

   760     show ?thesis

   761     proof(rule disjI2)

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

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

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

   765         with hh(1) hh(3)

   766         have "splited ks ys' zs"

   767           by (unfold splited_def, auto)

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

   769       qed

   770     qed

   771   qed

   772 qed

   773 

   774 lemma splited_cons_elim:

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

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

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

   778   shows P

   779 proof(rule splited_cons[OF h])

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

   781   thus P

   782   proof

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

   784     show P

   785     proof(rule h1)

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

   787     next

   788       from hh show "zs = ks" by simp

   789     qed

   790   next

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

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

   793     from h2[OF this]

   794     show P .

   795   qed

   796 qed

   797 

   798 lemma list_nth_expand:

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

   800   by (metis Cons_eq_appendI append_take_drop_id drop_Suc_conv_tl eq_Nil_appendI)

   801 

   802 lemma reps_len_nil: "reps_len [] = 0"

   803    by (auto simp:reps_len_def reps_sep_len_def reps_ctnt_len_def)

   804 

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

   806   by (auto simp:reps_len_def reps_sep_len_def reps_ctnt_len_def)

   807 

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

   809 proof(induct ks arbitrary:k)

   810   case (Cons n ns)

   811   thus ?case

   812     by(cases "ns = []", 

   813       auto simp:reps_len_def reps_sep_len_def reps_ctnt_len_def)

   814 qed auto

   815 

   816 lemma reps_len_correct:

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

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

   819   using h

   820 proof(induct ks arbitrary:i j s)

   821   case Nil

   822   thus ?case

   823     by (auto simp:reps_len_nil pasrt_def)

   824 next

   825   case (Cons n ns)

   826   thus ?case

   827   proof(cases "ns = []")

   828     case False

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

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

   831       by (auto elim!:sep_conjE)

   832     from Cons.hyps[OF this]

   833     show ?thesis

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

   835   next

   836     case True

   837     with Cons(2)

   838     show ?thesis

   839       by (auto simp:reps_len_sg pasrt_def)

   840   qed

   841 qed

   842 

   843 lemma reps_len_expand: 

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

   845 proof(default+)

   846   fix s

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

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

   849     by (auto simp:pred_ex_def)

   850 next

   851   fix s

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

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

   854 qed

   855 

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

   857 by (metis reps_len_def reps_len_expand sep.mult_commute sep_conj_exists1)

   858 

   859 lemma reps_splited:

   860   assumes h: "splited xs ys zs"

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

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

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

   864   using h

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

   866   case Nil

   867   thus ?case

   868     by (unfold splited_def, auto)

   869 next

   870   case (Cons k ks)

   871   from Cons(2)

   872   show ?case

   873   proof(rule splited_cons_elim)

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

   875     with Cons(2)

   876     show ?thesis

   877     proof(cases "ks = []")

   878       case True

   879       with Cons(2) have False

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

   881       thus ?thesis by auto

   882     next

   883       case False

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

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

   886       show ?thesis

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

   888             reps_len_sg, auto simp:sep_conj_ac,

   889             unfold ss h(2), simp)

   890     qed

   891   next

   892     fix ys'

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

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

   895       by (unfold splited_def, auto)

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

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

   898     show ?thesis

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

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

   901                     reps_len_cons[OF h(1)]

   902                     sep_conj_ac, subst ss, simp)

   903   qed

   904 qed

   905 

   906 

   907 subsection {* A theory of list extension *}

   908 

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

   910 

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

   912   by (metis length_append length_replicate list_ext_def)

   913 

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

   915   by (unfold list_ext_len_eq, auto)

   916 

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

   918   by (smt append_Nil2 list_ext_def replicate_0)

   919 

   920 lemma list_ext_lt_get: 

   921   assumes h: "a' < length xs"

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

   923 proof(cases "a < length xs")

   924   case True

   925   with h

   926   show ?thesis by (auto simp:list_ext_lt)

   927 next

   928   case False

   929   with h show ?thesis

   930     apply (unfold list_ext_def)

   931     by (metis nth_append)

   932 qed

   933 

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

   935   by (metis list_ext_len nth_list_update_eq)

   936 

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

   938   by (metis not_less nth_append)

   939 

   940 

   941 lemma list_ext_tail:

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

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

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

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

   946 proof -

   947   from h1 h2

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

   949     by (metis diff_less_mono h3 le_imp_less_Suc length_replicate)

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

   951     by (smt empty_replicate)

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

   953     by (metis length_replicate nth_replicate)

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

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

   956     by (rule nth_app[OF h2])

   957   ultimately show ?thesis

   958     by (auto simp:list_ext_def)

   959 qed

   960 

   961 lemmas list_ext_simps = list_ext_lt_get list_ext_lt list_ext_len list_ext_len_eq

   962 

   963 lemma listsum_upd_suc:

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

   965 by (smt elem_le_listsum_nat 

   966      length_list_update list_ext_get_upd 

   967      list_update_overwrite listsum_update_nat map_update 

   968      nth_equalityI nth_list_update nth_map)

   969 

   970 lemma reps_len_suc:

   971   assumes "a < length ks"

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

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

   974   case True

   975   with `a < length ks` 

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

   977     by (smt length_0_conv length_Suc_conv)

   978   thus ?thesis

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

   980       by (unfold reps_len_def reps_sep_len_def reps_ctnt_len_def, auto)

   981 next

   982   case False

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

   984     by (default, auto)

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

   986   show ?thesis

   987      by (unfold reps_len_def reps_sep_len_def reps_ctnt_len_def, simp)

   988 qed

   989   

   990 lemma ks_suc_len:

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

   992   and h2: "ks!a = v"

   993   and h3: "a < length ks"

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

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

   996 proof -

   997   from reps_len_correct[OF h1, unfolded list_ext_len_eq]

   998        reps_len_correct[OF h4, unfolded list_ext_len_eq] 

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

  1000   show ?thesis

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

  1002 qed

  1003 

  1004 lemma ks_ext_len:

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

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

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

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

  1009 proof -

  1010   from reps_len_correct[OF h1, unfolded  list_ext_len_eq]

  1011     and reps_len_correct[OF h4, unfolded list_ext_len_eq]

  1012   h3

  1013   show ?thesis by auto

  1014 qed

  1015 

  1016 definition 

  1017   "reps' i j ks = 

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

  1019 

  1020 lemma reps'_expand: 

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

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

  1023 proof -

  1024   show ?thesis

  1025   proof(default+)

  1026     fix s

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

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

  1029       by (simp add:reps'_def)

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

  1031     proof(elim EXS_elim)

  1032       fix j

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

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

  1035         by (auto elim!:sep_conjE)

  1036       from reps_len_correct[OF this(3)]

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

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

  1039         by simp

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

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

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

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

  1044     qed

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

  1046       by (simp add:h reps'_def)

  1047   next

  1048     fix s 

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

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

  1051       by (auto intro!:EXS_intro)

  1052   qed

  1053 qed

  1054 

  1055 lemma reps'_len_correct: 

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

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

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

  1059 proof -

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

  1061   from h[unfolded this]

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

  1063     by (auto elim!:sep_conjE)

  1064   from reps_len_correct[OF this]

  1065   show ?thesis by simp

  1066 qed

  1067 

  1068 lemma reps'_append:

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

  1070 proof(cases "ks1 = []")

  1071   case True

  1072   thus ?thesis

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

  1074 next

  1075   case False

  1076   show ?thesis

  1077   proof(cases "ks2 = []")

  1078     case False

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

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

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

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

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

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

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

  1086     from `ks1 \<noteq> []`

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

  1088       by (unfold reps'_def, simp)

  1089     show ?thesis

  1090     proof(default+)

  1091       fix s

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

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

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

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

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

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

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

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

  1100       qed

  1101     next

  1102       fix s

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

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

  1105       proof(elim EXS_elim)

  1106         fix m

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

  1108         then obtain s1 s2 where h: 

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

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

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

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

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

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

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

  1116         proof(rule sep_conjI)

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

  1118             by (simp add:reps'_def)

  1119         next

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

  1121             by (simp add:reps'_def)

  1122         next

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

  1124         next

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

  1126         qed

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

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

  1129       qed

  1130     qed

  1131   next

  1132     case True

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

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

  1135     show ?thesis