1 header {* 

     2   Separation logic for Turing Machines

     3 *}

     4 

     5 theory Hoare_tm

     6 imports Hoare_gen 

     7         My_block 

     8         Data_slot

     9         "~~/src/HOL/Library/FinFun_Syntax"

    10 begin

    11 

    12 

    13 ML {*

    14 fun pretty_terms ctxt trms =

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

    16 *}

    17 

    18 ML {*

    19 structure StepRules = Named_Thms

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

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

    22 *}

    23 

    24 ML {*

    25 structure FwdRules = Named_Thms

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

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

    28 *}

    29 

    30 setup {* StepRules.setup *}

    31 setup {* FwdRules.setup *}

    32 

    33 method_setup prune = 

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

    35   "pruning parameters"

    36 

    37 lemma int_add_C: 

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

    39   by simp

    40 

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

    42   by simp

    43 

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

    45   by simp

    46 

    47 lemmas int_add_ac = int_add_A int_add_C int_add_LC

    48 

    49 

    50 section {* Operational Semantics of TM *}

    51 

    52 datatype taction = W0 | W1 | L | R

    53 

    54 type_synonym tstate = nat

    55 

    56 datatype Block = Oc | Bk

    57 

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

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

    60 

    61 (* - number of faults (nat)

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

    63    - current state (nat)

    64    - position of head (int)

    65    - tape (int \<rightharpoonup> Block)

    66 *)

    67 type_synonym tconf = "nat \<times> (nat \<Rightarrow>f tm_inst option) \<times> nat \<times> int \<times> (int \<Rightarrow>f Block option)"

    68 

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

    70 fun 

    71   next_tape :: "taction \<Rightarrow> (int \<times>  (int \<Rightarrow>f Block option)) \<Rightarrow> (int \<times>  (int \<Rightarrow>f Block option))"

    72 where 

    73   "next_tape W0 (pos, m) = (pos, m(pos $:= Some Bk))" |

    74   "next_tape W1 (pos, m) = (pos, m(pos $:= Some Oc))" |

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

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

    77 

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

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

    80               (case (prog $ pc) of

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

    82                      case (m $ pos) of

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

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

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

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

    87 

    88 lemma tstep_splits: 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   104                    )"

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

   106 

   107 datatype tresource = 

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

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

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

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

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

   113 

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

   115 definition "tpc_set pc = {TAt pc}"

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

   117 definition "tpos_set pos = {TPos pos}"

   118 definition "tfaults_set faults = {TFaults faults}"

   119 

   120 lemmas tpn_set_def = tprog_set_def tpc_set_def tmem_set_def tfaults_set_def tpos_set_def

   121 

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

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

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

   125 

   126 interpretation tm: sep_exec tstep trset_of .

   127 

   128 

   129 

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

   131 

   132 subsection {* The assembly language *}

   133 

   134 datatype tpg = 

   135    TInstr tm_inst

   136  | TLabel nat

   137  | TSeq tpg tpg

   138  | TLocal "nat \<Rightarrow> tpg"

   139 

   140 notation TLocal (binder "TL " 10)

   141 

   142 abbreviation 

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

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

   145 

   146 abbreviation tprog_seq :: 

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

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

   149 

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

   151 

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

   153 

   154 abbreviation 

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

   156 where 

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

   158 

   159 abbreviation it_hoare ::

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

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

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

   163 

   164 (*

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

   166   "tpg_len (TInstr ai) = 1" |

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

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

   169   "tpg_len (TLabel l) = 0" 

   170 *)

   171 

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

   173   where 

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

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

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

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

   178 

   179 declare tassemble_to.simps [simp del]

   180 

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

   182 

   183 abbreviation 

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

   185   where 

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

   187 

   188 lemma EXS_intro: 

   189   assumes h: "(P x) s"

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

   191   by (smt h pred_ex_def sep_conj_impl)

   192 

   193 lemma EXS_elim: 

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

   195   obtains x where "P x s"

   196   by (metis assms pred_ex_def)

   197 

   198 lemma EXS_eq:

   199   fixes x

   200   assumes h: "Q (p x)" 

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

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

   203 proof

   204   fix s

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

   206   proof

   207     assume "p x s"

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

   209   next

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

   211     thus "p x s"

   212     proof(rule EXS_elim)

   213       fix y

   214       assume "p y s"

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

   216     qed

   217   qed

   218 qed

   219 

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

   221 

   222 lemma tpg_fold_sg: 

   223   "tpg_fold [tpg] = tpg"

   224   by (simp add:tpg_fold_def)

   225 

   226 lemma tpg_fold_cons: 

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

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

   229   using h

   230 proof(induct tpgs arbitrary:tpg)

   231   case (Cons tpg1 tpgs1)

   232   thus ?case

   233   proof(cases "tpgs1 = []")

   234     case True

   235     thus ?thesis by (simp add:tpg_fold_def)

   236   next

   237     case False

   238     show ?thesis

   239     proof -

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

   241         by simp

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

   243         by simp

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

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

   246         by simp

   247       show ?thesis

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

   249         by (fold tpg_fold_def, simp)

   250     qed

   251   qed

   252 qed auto

   253 

   254 lemmas tpg_fold_simps = tpg_fold_sg tpg_fold_cons

   255 

   256 lemma tpg_fold_app:

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

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

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

   260   using h1 h2

   261 proof(induct tpgs1 arbitrary: i j tpgs2)

   262   case (Cons tpg1' tpgs1')

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

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

   265     case False

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

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

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

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

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

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

   272     proof -

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

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

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

   276       proof(default+)

   277         fix s

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

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

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

   281         proof(elim EXS_elim)

   282           fix j'

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

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

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

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

   287           proof(elim sep_conjE EXS_elim)

   288             fix x y j'a xa ya

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

   290                       "x ## y" "s = x + y"

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

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

   293                       " xa ## ya" "y = xa + ya"

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

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

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

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

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

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

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

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

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

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

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

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

   306                   by (auto intro!:sep_conjI)

   307               qed

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

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

   310                 by (metis sep_disj_addI1 sep_disj_commuteI)

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

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

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

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

   315                 by (auto intro!:sep_conjI)

   316             qed

   317           qed

   318         qed

   319       next

   320         fix s

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

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

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

   324         proof(elim EXS_elim sep_conjE)

   325           fix j' x y j'a xa ya

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   343                   by (auto intro!:sep_conjI)

   344               qed

   345             qed

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

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

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

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

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

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

   352               by (auto intro!:sep_conjI)

   353           qed

   354         qed

   355       qed

   356       thus ?thesis 

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

   358              unfold tassemble_to.simps, simp)

   359     qed

   360     finally show ?thesis . 

   361   next

   362     case True

   363     thus ?thesis

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

   365   qed 

   366 qed auto

   367  

   368 

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

   370 

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

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

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

   374 definition "one i = tm i Oc"

   375 definition "zero i= tm i Bk"

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

   377 

   378 declare trset_of.simps[simp del]

   379 

   380 lemma stimes_sgD: 

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

   382   apply(erule_tac sep_conjE)

   383   apply(unfold set_ins_def sg_def)

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

   385   

   386 lemma stD: 

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

   388 proof -

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

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

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

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

   393   thus ?thesis

   394     by (unfold tpn_set_def, auto)

   395 qed

   396 

   397 lemma psD: 

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

   399 proof -

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

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

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

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

   404     by simp

   405   thus ?thesis

   406     by (unfold tpn_set_def, auto)

   407 qed

   408 

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

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

   411 proof -

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

   413   thus ?thesis

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

   415     

   416     by auto

   417 qed

   418 

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

   420 proof -

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

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

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

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

   425   thus ?thesis by auto

   426 qed

   427 

   428 lemma t_hoare_seq: 

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

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

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

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

   433   fix j'

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

   435   proof(rule tm.composition)

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

   437   next

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

   439   qed

   440 qed

   441 

   442 

   443 lemma t_hoare_seq1:

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

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

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

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

   448   fix j'

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

   450   proof(rule tm.composition)

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

   452   next

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

   454   qed

   455 qed

   456 

   457 lemma t_hoare_seq2:

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

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

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

   461   by (rule tm.code_extension, rule h)

   462 

   463 lemma t_hoare_local: 

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

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

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

   467 

   468 lemma t_hoare_label: 

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

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

   471 using assms

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

   473 

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

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

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

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

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

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

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

   481 

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

   483 

   484 declare t_last_cmd_def [simp]

   485 

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

   487 

   488 declare t_blast_cmd_def [simp]

   489 

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

   491   by simp

   492 

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

   494   by simp

   495 

   496 lemma t_split_cmd_eq:

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

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

   499   using assms

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

   501   case (TSeq cx cy)

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

   503   show ?case

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

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

   506     proof -

   507       fix a

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

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

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

   511         apply (simp add:sep_conj_ac)

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

   513     qed

   514 qed auto

   515 

   516 lemma t_hoare_label_last_pre: 

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

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

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

   520 by (unfold t_split_cmd_eq[OF h1], 

   521     simp only:tassemble_to.simps sep_conj_cond, 

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

   523 

   524 lemma t_hoare_label_last: 

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

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

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

   528 proof -

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

   530       by simp

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

   532   show ?thesis by auto

   533 qed

   534 

   535 

   536 subsection {* Basic assertions for TM *}

   537 

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

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

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

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

   542 by auto

   543 

   544 termination 

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

   546 

   547 lemma ones_base_simp: 

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

   549   by simp

   550 

   551 lemma ones_step_simp: 

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

   553   by simp

   554 

   555 lemmas ones_simps = ones_base_simp ones_step_simp

   556 

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

   558 

   559 lemma ones_induct [case_names Base Step]:

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

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

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

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

   564   fix i j 

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

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

   567   proof(cases "j < i")

   568     case True

   569     with h1 [OF True]

   570     show ?thesis by auto

   571   next

   572     case False

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

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

   575     with False show ?thesis by auto

   576   qed

   577 qed

   578 

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

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

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

   582 by auto

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

   584 

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

   586 proof(induct i j rule:ones_induct)

   587   case Base

   588   thus ?case by auto

   589 next

   590   case (Step i j)

   591   show ?case

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

   593     case True

   594     with Step show ?thesis

   595       by simp

   596   next

   597     case False

   598     with Step show ?thesis 

   599       by (auto simp:sep_conj_ac)

   600   qed

   601 qed

   602 

   603 lemma ones_rev_induct [case_names Base Step]:

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

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

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

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

   608   fix i j 

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

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

   611   proof(cases "j < i")

   612     case True

   613     with h1 [OF True]

   614     show ?thesis by auto

   615   next

   616     case False

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

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

   619     with ones_rev and False

   620     show ?thesis

   621       by simp

   622   qed

   623 qed

   624 

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

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

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

   628 by auto

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

   630 

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

   632   by simp

   633 

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

   635   by simp

   636 

   637 declare zeros.simps [simp del]

   638 lemmas zeros_simps [simp] = zeros_base_simp zeros_step_simp

   639 

   640 lemma zeros_induct [case_names Base Step]:

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

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

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

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

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

   646   fix i j 

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

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

   649   proof(cases "j < i")

   650     case True

   651     with h1 [OF True]

   652     show ?thesis by auto

   653   next

   654     case False

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

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

   657     with False show ?thesis by auto

   658   qed

   659 qed

   660 

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

   662 proof(induct i j rule:zeros_induct)

   663   case (Base i j)

   664   thus ?case by auto

   665 next

   666   case (Step i j)

   667   show ?case

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

   669     case True

   670     with Step show ?thesis by auto

   671   next

   672     case False

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

   674   qed

   675 qed

   676 

   677 lemma zeros_rev_induct [case_names Base Step]:

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

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

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

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

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

   683   fix i j 

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

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

   686   proof(cases "j < i")

   687     case True

   688     with h1 [OF True]

   689     show ?thesis by auto

   690   next

   691     case False

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

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

   694     with zeros_rev and False

   695     show ?thesis by simp

   696   qed

   697 qed

   698 

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

   700 

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

   702   where

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

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

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

   706 

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

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

   709   by (cases ks, auto)

   710 

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

   712 

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

   714 

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

   716 

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

   718 

   719 lemma list_split: 

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

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

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

   723 proof(cases ys)

   724   case Nil

   725   with h1 show ?thesis by auto

   726 next

   727   case (Cons y' ys')

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

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

   730   show ?thesis

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

   732     case False

   733     show ?thesis

   734     proof(rule disjI2)

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

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

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

   738       qed

   739     qed

   740   next

   741     case True

   742     show ?thesis

   743     proof(rule disjI1)

   744       from hh True Cons

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

   746     qed

   747   qed

   748 qed

   749 

   750 lemma splited_cons[elim_format]: 

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

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

   753 proof -

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

   755   from list_split[OF this]

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

   757   thus ?thesis

   758   proof

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

   760   next

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

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

   763     show ?thesis

   764     proof(rule disjI2)

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

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

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

   768         with hh(1) hh(3)

   769         have "splited ks ys' zs"

   770           by (unfold splited_def, auto)

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

   772       qed

   773     qed

   774   qed

   775 qed

   776 

   777 lemma splited_cons_elim:

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

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

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

   781   shows P

   782 proof(rule splited_cons[OF h])

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

   784   thus P

   785   proof

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

   787     show P

   788     proof(rule h1)

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

   790     next

   791       from hh show "zs = ks" by simp

   792     qed

   793   next

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

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

   796     from h2[OF this]

   797     show P .

   798   qed

   799 qed

   800 

   801 lemma list_nth_expand:

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

   803   by (metis Cons_eq_appendI append_take_drop_id drop_Suc_conv_tl eq_Nil_appendI)

   804 

   805 lemma reps_len_nil: "reps_len [] = 0"

   806    by (auto simp:reps_len_def reps_sep_len_def reps_ctnt_len_def)

   807 

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

   809   by (auto simp:reps_len_def reps_sep_len_def reps_ctnt_len_def)

   810 

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

   812 proof(induct ks arbitrary:k)

   813   case (Cons n ns)

   814   thus ?case

   815     by(cases "ns = []", 

   816       auto simp:reps_len_def reps_sep_len_def reps_ctnt_len_def)

   817 qed auto

   818 

   819 lemma reps_len_correct:

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

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

   822   using h

   823 proof(induct ks arbitrary:i j s)

   824   case Nil

   825   thus ?case

   826     by (auto simp:reps_len_nil pasrt_def)

   827 next

   828   case (Cons n ns)

   829   thus ?case

   830   proof(cases "ns = []")

   831     case False

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

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

   834       by (auto elim!:sep_conjE)

   835     from Cons.hyps[OF this]

   836     show ?thesis

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

   838   next

   839     case True

   840     with Cons(2)

   841     show ?thesis

   842       by (auto simp:reps_len_sg pasrt_def)

   843   qed

   844 qed

   845 

   846 lemma reps_len_expand: 

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

   848 proof(default+)

   849   fix s

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

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

   852     by (auto simp:pred_ex_def)

   853 next

   854   fix s

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

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

   857 qed

   858 

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

   860 by (metis reps_len_def reps_len_expand sep.mult_commute sep_conj_exists1)

   861 

   862 lemma reps_splited:

   863   assumes h: "splited xs ys zs"

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

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

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

   867   using h

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

   869   case Nil

   870   thus ?case

   871     by (unfold splited_def, auto)

   872 next

   873   case (Cons k ks)

   874   from Cons(2)

   875   show ?case

   876   proof(rule splited_cons_elim)

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

   878     with Cons(2)

   879     show ?thesis

   880     proof(cases "ks = []")

   881       case True

   882       with Cons(2) have False

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

   884       thus ?thesis by auto

   885     next

   886       case False

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

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

   889       show ?thesis

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

   891             reps_len_sg, auto simp:sep_conj_ac,

   892             unfold ss h(2), simp)

   893     qed

   894   next

   895     fix ys'

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

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

   898       by (unfold splited_def, auto)

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

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

   901     show ?thesis

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

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

   904                     reps_len_cons[OF h(1)]

   905                     sep_conj_ac, subst ss, simp)

   906   qed

   907 qed

   908 

   909 

   910 subsection {* A theory of list extension *}

   911 

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

   913 

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

   915   by (metis length_append length_replicate list_ext_def)

   916 

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

   918   by (unfold list_ext_len_eq, auto)

   919 

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

   921   by (smt append_Nil2 list_ext_def replicate_0)

   922 

   923 lemma list_ext_lt_get: 

   924   assumes h: "a' < length xs"

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

   926 proof(cases "a < length xs")

   927   case True

   928   with h

   929   show ?thesis by (auto simp:list_ext_lt)

   930 next

   931   case False

   932   with h show ?thesis

   933     apply (unfold list_ext_def)

   934     by (metis nth_append)

   935 qed

   936 

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

   938   by (metis list_ext_len nth_list_update_eq)

   939 

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

   941   by (metis not_less nth_append)

   942 

   943 

   944 lemma list_ext_tail:

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

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

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

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

   949 proof -

   950   from h1 h2

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

   952     by (metis diff_less_mono h3 le_imp_less_Suc length_replicate)

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

   954     by (smt empty_replicate)

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

   956     by (metis length_replicate nth_replicate)

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

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

   959     by (rule nth_app[OF h2])

   960   ultimately show ?thesis

   961     by (auto simp:list_ext_def)

   962 qed

   963 

   964 lemmas list_ext_simps = list_ext_lt_get list_ext_lt list_ext_len list_ext_len_eq

   965 

   966 lemma listsum_upd_suc:

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

   968 by (smt elem_le_listsum_nat 

   969      length_list_update list_ext_get_upd 

   970      list_update_overwrite listsum_update_nat map_update 

   971      nth_equalityI nth_list_update nth_map)

   972 

   973 lemma reps_len_suc:

   974   assumes "a < length ks"

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

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

   977   case True

   978   with `a < length ks` 

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

   980     by (smt length_0_conv length_Suc_conv)

   981   thus ?thesis

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

   983       by (unfold reps_len_def reps_sep_len_def reps_ctnt_len_def, auto)

   984 next

   985   case False

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

   987     by (default, auto)

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

   989   show ?thesis

   990      by (unfold reps_len_def reps_sep_len_def reps_ctnt_len_def, simp)

   991 qed

   992   

   993 lemma ks_suc_len:

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

   995   and h2: "ks!a = v"

   996   and h3: "a < length ks"

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

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

   999 proof -

  1000   from reps_len_correct[OF h1, unfolded list_ext_len_eq]

  1001        reps_len_correct[OF h4, unfolded list_ext_len_eq] 

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

  1003   show ?thesis

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

  1005 qed

  1006 

  1007 lemma ks_ext_len:

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

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

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

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

  1012 proof -

  1013   from reps_len_correct[OF h1, unfolded  list_ext_len_eq]

  1014     and reps_len_correct[OF h4, unfolded list_ext_len_eq]

  1015   h3

  1016   show ?thesis by auto

  1017 qed

  1018 

  1019 definition 

  1020   "reps' i j ks = 

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

  1022 

  1023 lemma reps'_expand: 

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

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

  1026 proof -

  1027   show ?thesis

  1028   proof(default+)

  1029     fix s

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

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

  1032       by (simp add:reps'_def)

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

  1034     proof(elim EXS_elim)

  1035       fix j

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

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

  1038         by (auto elim!:sep_conjE)

  1039       from reps_len_correct[OF this(3)]

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

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

  1042         by simp

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

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

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

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

  1047     qed

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

  1049       by (simp add:h reps'_def)

  1050   next

  1051     fix s 

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

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

  1054       by (auto intro!:EXS_intro)

  1055   qed

  1056 qed

  1057 

  1058 lemma reps'_len_correct: 

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

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

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

  1062 proof -

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

  1064   from h[unfolded this]

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

  1066     by (auto elim!:sep_conjE)

  1067   from reps_len_correct[OF this]

  1068   show ?thesis by simp

  1069 qed

  1070 

  1071 lemma reps'_append:

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

  1073 proof(cases "ks1 = []")

  1074   case True

  1075   thus ?thesis

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

  1077 next

  1078   case False

  1079   show ?thesis

  1080   proof(cases "ks2 = []")

  1081     case False

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

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

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

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

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

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

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

  1089     from `ks1 \<noteq> []`

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

  1091       by (unfold reps'_def, simp)

  1092     show ?thesis

  1093     proof(default+)

  1094       fix s

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

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

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

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

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

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

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

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

  1103       qed

  1104     next

  1105       fix s

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

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

  1108       proof(elim EXS_elim)

  1109         fix m

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

  1111         then obtain s1 s2 where h: 

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

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

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

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

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

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

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

  1119         proof(rule sep_conjI)

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

  1121             by (simp add:reps'_def)

  1122         next

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

  1124             by (simp add:reps'_def)

  1125         next

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

  1127         next

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

  1129         qed

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

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

  1132       qed

  1133     qed

  1134   next

  1135     case True