1 header {* 

     2   Separation logic for TM

     3 *}

     4 

     5 theory Hoare_tm

     6 imports Hoare_tm_basis My_block Data_slot

     7 begin

     8 

     9 

    10 section {* Aux lemmas *}

    11 

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

    13   by simp

    14 

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

    16   by simp

    17 

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

    19   by simp

    20 

    21 lemmas int_add_ac = int_add_A int_add_C int_add_LC

    22 

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

    24                        "pruning parameters"

    25 

    26 ML {*

    27 structure StepRules = Named_Thms

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

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

    30 *}

    31 

    32 ML {*

    33 structure FwdRules = Named_Thms

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

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

    36 *}

    37 

    38 setup {* StepRules.setup *}

    39 

    40 setup {* FwdRules.setup *}

    41 

    42 section {* Operational Semantics of TM *}

    43 

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

    45 

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

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

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

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

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

    51 

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

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

    54               (case (prog pc) of

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

    56                      case (m pos) of

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

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

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

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

    61 

    62 (* lemma tstep_splits: 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    78                    )"

    79   apply (case_tac s, auto split:option.splits Block.splits)

    80 *)

    81 

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

    83 definition "tpc_set pc = {TAt pc}"

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

    85 definition "tpos_set pos = {TPos pos}"

    86 definition "tfaults_set faults = {TFaults faults}"

    87 

    88 lemmas tpn_set_def = tprog_set_def tpc_set_def tmem_set_def tfaults_set_def tpos_set_def

    89 

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

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

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

    93 

    94 interpretation tm: sep_exec tstep trset_of .

    95 

    96 section {* Hoare logic for TM *}

    97 

    98 abbreviation t_hoare :: 

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

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

   101 

   102 abbreviation it_hoare ::

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

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

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

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

   107 

   108 (*

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

   110   "tpg_len (TInstr ai) = 1" |

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

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

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

   114 

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

   116   by (simp add:tpg_fold_def)

   117 

   118 lemma tpg_fold_cons: 

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

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

   121   using h

   122 proof(induct tpgs arbitrary:tpg)

   123   case (Cons tpg1 tpgs1)

   124   thus ?case

   125   proof(cases "tpgs1 = []")

   126     case True

   127     thus ?thesis by (simp add:tpg_fold_def)

   128   next

   129     case False

   130     show ?thesis

   131     proof -

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

   133         by simp

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

   135         by simp

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

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

   138         by simp

   139       show ?thesis

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

   141         by (fold tpg_fold_def, simp)

   142     qed

   143   qed

   144 qed auto

   145 

   146 lemmas tpg_fold_simps = tpg_fold_sg tpg_fold_cons

   147 

   148 lemma tpg_fold_app:

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

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

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

   152   using h1 h2

   153 proof(induct tpgs1 arbitrary: i j tpgs2)

   154   case (Cons tpg1' tpgs1')

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

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

   157     case False

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

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

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

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

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

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

   164     proof -

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

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

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

   168       proof(default+)

   169         fix s

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

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

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

   173         proof(elim EXS_elim)

   174           fix j'

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

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

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

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

   179           proof(elim sep_conjE EXS_elim)

   180             fix x y j'a xa ya

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

   182                       "x ## y" "s = x + y"

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

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

   185                       " xa ## ya" "y = xa + ya"

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

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

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

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

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

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

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

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

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

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

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

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

   198                   by (auto intro!:sep_conjI)

   199               qed

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

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

   202                 by (metis sep_disj_addI1 sep_disj_commuteI)

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

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

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

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

   207                 by (auto intro!:sep_conjI)

   208             qed

   209           qed

   210         qed

   211       next

   212         fix s

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

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

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

   216         proof(elim EXS_elim sep_conjE)

   217           fix j' x y j'a xa ya

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   235                   by (auto intro!:sep_conjI)

   236               qed

   237             qed

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

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

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

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

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

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

   244               by (auto intro!:sep_conjI)

   245           qed

   246         qed

   247       qed

   248       thus ?thesis 

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

   250              unfold tassemble_to.simps, simp)

   251     qed

   252     finally show ?thesis . 

   253   next

   254     case True

   255     thus ?thesis

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

   257   qed 

   258 qed auto

   259  

   260 

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

   262 

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

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

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

   266 definition "one i = tm i Oc"

   267 definition "zero i= tm i Bk"

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

   269 

   270 declare trset_of.simps[simp del]

   271 

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

   273   apply(erule_tac sep_conjE)

   274   apply(unfold set_ins_def sg_def)

   275   by (metis Diff_Int2 Diff_Int_distrib2 Diff_Un Diff_cancel 

   276     Diff_empty Diff_idemp Diff_triv Int_Diff Un_Diff 

   277     Un_Diff_cancel inf_commute inf_idem sup_bot_right sup_commute sup_ge2)

   278 

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

   280        \<Longrightarrow> i' = i"

   281 proof -

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

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

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

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

   286   thus ?thesis

   287     by (unfold tpn_set_def, auto)

   288 qed

   289 

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

   291        \<Longrightarrow> pos = p"

   292 proof -

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

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

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

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

   297     by simp

   298   thus ?thesis

   299     by (unfold tpn_set_def, auto)

   300 qed

   301 

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

   303        \<Longrightarrow> prog i = Some inst"

   304 proof -

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

   306   thus ?thesis

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

   308     by auto

   309 qed

   310 

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

   312 proof -

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

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

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

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

   317   thus ?thesis by auto

   318 qed

   319 

   320 lemma t_hoare_seq: 

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

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

   323 proof -

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

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

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

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

   328     fix j'

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

   330     proof(rule tm.composition)

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

   332     next

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

   334     qed

   335   qed

   336 qed

   337 

   338 lemma t_hoare_seq1:

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

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

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

   342 proof -

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

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

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

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

   347     fix j'

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

   349     proof(rule tm.composition)

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

   351     next

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

   353     qed

   354   qed

   355 qed

   356 

   357 lemma t_hoare_seq2:

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

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

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

   361   by (rule tm.code_extension, rule h)

   362 

   363 lemma t_hoare_local: 

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

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

   366   by (unfold tassemble_to.simps, intro tm.code_exI, case_tac l, simp)

   367 

   368 lemma t_hoare_label: 

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

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

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

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

   373   by (cases l, unfold tassemble_to.simps, intro tm.code_exI tm.code_condI, clarify, auto)

   374 

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

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

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

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

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

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

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

   382 

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

   384 

   385 declare t_last_cmd_def [simp]

   386 

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

   388 

   389 declare t_blast_cmd_def [simp]

   390 

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

   392   by simp

   393 

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

   395   by simp

   396 

   397 lemma t_split_cmd_eq:

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

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

   400   using assms

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

   402   case (TSeq cx cy)

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

   404   show ?case

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

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

   407     proof -

   408       fix a

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

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

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

   412         apply (simp add:sep_conj_ac)

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

   414     qed

   415 qed auto

   416 

   417 lemma t_hoare_label_last_pre: 

   418   fixes l

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

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

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

   422 by (cases l, unfold t_split_cmd_eq[OF h1], 

   423     simp only:tassemble_to.simps sep_conj_cond, 

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

   425 

   426 lemma t_hoare_label_last: 

   427   fixes l

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

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

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

   431 proof -

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

   433       by simp

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

   435   show ?thesis by auto

   436 qed

   437 

   438 subsection {* Basic assertions for TM *}

   439 

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

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

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

   443 by auto

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

   445 

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

   447   by simp

   448 

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

   450   by simp

   451 

   452 lemmas ones_simps = ones_base_simp ones_step_simp

   453 

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

   455 

   456 lemma ones_induct [case_names Base Step]:

   457   fixes P i j

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

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

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

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

   462   fix i j 

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

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

   465   proof(cases "j < i")

   466     case True

   467     with h1 [OF True]

   468     show ?thesis by auto

   469   next

   470     case False

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

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

   473     with False show ?thesis by auto

   474   qed

   475 qed

   476 

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

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

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

   480 by auto

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

   482 

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

   484 proof(induct i j rule:ones_induct)

   485   case Base

   486   thus ?case by auto

   487 next

   488   case (Step i j)

   489   show ?case

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

   491     case True

   492     with Step show ?thesis

   493       by simp

   494   next

   495     case False

   496     with Step show ?thesis 

   497       by (auto simp:sep_conj_ac)

   498   qed

   499 qed

   500 

   501 lemma ones_rev_induct [case_names Base Step]:

   502   fixes P i j

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

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

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

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

   507   fix i j 

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

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

   510   proof(cases "j < i")

   511     case True

   512     with h1 [OF True]

   513     show ?thesis by auto

   514   next

   515     case False

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

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

   518     with ones_rev and False

   519     show ?thesis

   520       by simp

   521   qed

   522 qed

   523 

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

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

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

   527 by auto

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

   529 

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

   531   by simp

   532 

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

   534   by simp

   535 

   536 declare zeros.simps [simp del]

   537 lemmas zeros_simps [simp] = zeros_base_simp zeros_step_simp

   538 

   539 lemma zeros_induct [case_names Base Step]:

   540   fixes P i j

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

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

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

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

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

   546   fix i j 

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

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

   549   proof(cases "j < i")

   550     case True

   551     with h1 [OF True]

   552     show ?thesis by auto

   553   next

   554     case False

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

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

   557     with False show ?thesis by auto

   558   qed

   559 qed

   560 

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

   562 proof(induct i j rule:zeros_induct)

   563   case (Base i j)

   564   thus ?case by auto

   565 next

   566   case (Step i j)

   567   show ?case

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

   569     case True

   570     with Step show ?thesis by auto

   571   next

   572     case False

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

   574   qed

   575 qed

   576 

   577 lemma zeros_rev_induct [case_names Base Step]:

   578   fixes P i j

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

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

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

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

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

   584   fix i j 

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

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

   587   proof(cases "j < i")

   588     case True

   589     with h1 [OF True]

   590     show ?thesis by auto

   591   next

   592     case False

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

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

   595     with zeros_rev and False

   596     show ?thesis by simp

   597   qed

   598 qed

   599 

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

   601 

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

   603   where

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

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

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

   607 

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

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

   610   by (cases ks, auto)

   611 

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

   613 

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

   615 

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

   617 

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

   619 

   620 lemma list_split: 

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

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

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

   624 proof(cases ys)

   625   case Nil

   626   with h1 show ?thesis by auto

   627 next

   628   case (Cons y' ys')

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

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

   631   show ?thesis

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

   633     case False

   634     show ?thesis

   635     proof(rule disjI2)

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

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

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

   639       qed

   640     qed

   641   next

   642     case True

   643     show ?thesis

   644     proof(rule disjI1)

   645       from hh True Cons

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

   647     qed

   648   qed

   649 qed

   650 

   651 lemma splited_cons[elim_format]: 

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

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

   654 proof -

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

   656   from list_split[OF this]

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

   658   thus ?thesis

   659   proof

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

   661   next

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

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

   664     show ?thesis

   665     proof(rule disjI2)

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

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

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

   669         with hh(1) hh(3)

   670         have "splited ks ys' zs"

   671           by (unfold splited_def, auto)

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

   673       qed

   674     qed

   675   qed

   676 qed

   677 

   678 lemma splited_cons_elim:

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

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

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

   682   shows P

   683 proof(rule splited_cons[OF h])

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

   685   thus P

   686   proof

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

   688     show P

   689     proof(rule h1)

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

   691     next

   692       from hh show "zs = ks" by simp

   693     qed

   694   next

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

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

   697     from h2[OF this]

   698     show P .

   699   qed

   700 qed

   701 

   702 lemma list_nth_expand:

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

   704   by (metis Cons_eq_appendI append_take_drop_id drop_Suc_conv_tl eq_Nil_appendI)

   705 

   706 lemma reps_len_nil: "reps_len [] = 0"

   707    by (auto simp:reps_len_def reps_sep_len_def reps_ctnt_len_def)

   708 

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

   710   by (auto simp:reps_len_def reps_sep_len_def reps_ctnt_len_def)

   711 

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

   713 proof(induct ks arbitrary:k)

   714   case (Cons n ns)

   715   thus ?case

   716     by(cases "ns = []", 

   717       auto simp:reps_len_def reps_sep_len_def reps_ctnt_len_def)

   718 qed auto

   719 

   720 lemma reps_len_correct:

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

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

   723   using h

   724 proof(induct ks arbitrary:i j s)

   725   case Nil

   726   thus ?case

   727     by (auto simp:reps_len_nil pasrt_def)

   728 next

   729   case (Cons n ns)

   730   thus ?case

   731   proof(cases "ns = []")

   732     case False

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

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

   735       by (auto elim!:sep_conjE)

   736     from Cons.hyps[OF this]

   737     show ?thesis

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

   739   next

   740     case True

   741     with Cons(2)

   742     show ?thesis

   743       by (auto simp:reps_len_sg pasrt_def)

   744   qed

   745 qed

   746 

   747 lemma reps_len_expand: 

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

   749 proof(default+)

   750   fix s

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

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

   753     by (auto simp:pred_ex_def)

   754 next

   755   fix s

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

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

   758 qed

   759 

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

   761 by (metis reps_len_def reps_len_expand sep.mult_commute sep_conj_exists1)

   762 

   763 lemma reps_splited:

   764   assumes h: "splited xs ys zs"

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

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

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

   768   using h

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

   770   case Nil

   771   thus ?case

   772     by (unfold splited_def, auto)

   773 next

   774   case (Cons k ks)

   775   from Cons(2)

   776   show ?case

   777   proof(rule splited_cons_elim)

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

   779     with Cons(2)

   780     show ?thesis

   781     proof(cases "ks = []")

   782       case True

   783       with Cons(2) have False

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

   785       thus ?thesis by auto

   786     next

   787       case False

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

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

   790       show ?thesis

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

   792             reps_len_sg, auto simp:sep_conj_ac,

   793             unfold ss h(2), simp)

   794     qed

   795   next

   796     fix ys'

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

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

   799       by (unfold splited_def, auto)

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

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

   802     show ?thesis

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

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

   805                     reps_len_cons[OF h(1)]

   806                     sep_conj_ac, subst ss, simp)

   807   qed

   808 qed

   809 

   810 subsection {* A theory of list extension *}

   811 

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

   813 

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

   815   by (metis length_append length_replicate list_ext_def)

   816 

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

   818   by (unfold list_ext_len_eq, auto)

   819 

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

   821   by (smt append_Nil2 list_ext_def replicate_0)

   822 

   823 lemma list_ext_lt_get: 

   824   assumes h: "a' < length xs"

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

   826 proof(cases "a < length xs")

   827   case True

   828   with h

   829   show ?thesis by (auto simp:list_ext_lt)

   830 next

   831   case False

   832   with h show ?thesis

   833     apply (unfold list_ext_def)

   834     by (metis nth_append)

   835 qed

   836 

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

   838   by (metis list_ext_len nth_list_update_eq)

   839 

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

   841   by (metis not_less nth_append)

   842 

   843 lemma pred_exI: 

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

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

   846   by (metis assms pred_ex_def sep_globalise)

   847 

   848 lemma list_ext_tail:

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

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

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

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

   853 proof -

   854   from h1 h2

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

   856     by (metis diff_less_mono h3 le_imp_less_Suc length_replicate)

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

   858     by (smt empty_replicate)

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

   860     by (metis length_replicate nth_replicate)

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

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

   863     by (rule nth_app[OF h2])

   864   ultimately show ?thesis

   865     by (auto simp:list_ext_def)

   866 qed

   867 

   868 lemmas list_ext_simps = list_ext_lt_get list_ext_lt list_ext_len list_ext_len_eq

   869 

   870 lemma listsum_upd_suc:

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

   872 by (smt Ex_list_of_length Skolem_list_nth elem_le_listsum_nat 

   873      length_induct length_list_update length_map length_splice 

   874      list_eq_iff_nth_eq list_ext_get_upd list_ext_lt_get list_update_beyond 

   875      list_update_id list_update_overwrite list_update_same_conv list_update_swap 

   876      listsum_update_nat map_eq_imp_length_eq map_update neq_if_length_neq 

   877      nth_equalityI nth_list_update nth_list_update_eq nth_list_update_neq nth_map reps_sep_len_def)

   878 

   879 lemma reps_len_suc:

   880   assumes "a < length ks"

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

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

   883   case True

   884   with `a < length ks` 

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

   886     by (smt length_0_conv length_Suc_conv)

   887   thus ?thesis

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

   889       by (unfold reps_len_def reps_sep_len_def reps_ctnt_len_def, auto)

   890 next

   891   case False

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

   893     by (default, auto)

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

   895   show ?thesis

   896      by (unfold reps_len_def reps_sep_len_def reps_ctnt_len_def, simp)

   897 qed

   898   

   899 lemma ks_suc_len:

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

   901   and h2: "ks!a = v"

   902   and h3: "a < length ks"

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

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

   905 proof -

   906   from reps_len_correct[OF h1, unfolded list_ext_len_eq]

   907        reps_len_correct[OF h4, unfolded list_ext_len_eq] 

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

   909   show ?thesis

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

   911 qed

   912 

   913 lemma ks_ext_len:

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

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

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

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

   918 proof -

   919   from reps_len_correct[OF h1, unfolded  list_ext_len_eq]

   920     and reps_len_correct[OF h4, unfolded list_ext_len_eq]

   921   h3

   922   show ?thesis by auto

   923 qed

   924 

   925 definition 

   926   "reps' i j ks = 

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

   928 

   929 lemma reps'_expand: 

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

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

   932 proof -

   933   show ?thesis

   934   proof(default+)

   935     fix s

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

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

   938       by (simp add:reps'_def)

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

   940     proof(elim EXS_elim)

   941       fix j

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

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

   944         by (auto elim!:sep_conjE)

   945       from reps_len_correct[OF this(3)]

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

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

   948         by simp

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

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

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

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

   953     qed

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

   955       by (simp add:h reps'_def)

   956   next

   957     fix s 

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

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

   960       by (auto intro!:EXS_intro)

   961   qed

   962 qed

   963 

   964 lemma reps'_len_correct: 

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

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

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

   968 proof -

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

   970   from h[unfolded this]

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

   972     by (auto elim!:sep_conjE)

   973   from reps_len_correct[OF this]

   974   show ?thesis by simp

   975 qed

   976 

   977 lemma reps'_append:

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

   979 proof(cases "ks1 = []")

   980   case True

   981   thus ?thesis

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

   983 next

   984   case False

   985   show ?thesis

   986   proof(cases "ks2 = []")

   987     case False

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

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

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

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

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

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

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

   995     from `ks1 \<noteq> []`

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

   997       by (unfold reps'_def, simp)

   998     show ?thesis

   999     proof(default+)

  1000       fix s

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

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

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

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

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

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

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

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

  1009       qed

  1010     next

  1011       fix s

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

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

  1014       proof(elim EXS_elim)

  1015         fix m

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

  1017         then obtain s1 s2 where h: 

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

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

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

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

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

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

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

  1025         proof(rule sep_conjI)

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

  1027             by (simp add:reps'_def)

  1028         next

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

  1030             by (simp add:reps'_def)

  1031         next

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

  1033         next

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

  1035         qed

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

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

  1038       qed

  1039     qed

  1040   next

  1041     case True

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

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

  1044     show ?thesis

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

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

  1047       by (fold sep_empty_def, simp only:sep_conj_empty)

  1048   qed

  1049 qed

  1050 

  1051 lemma reps'_sg: 

  1052   "reps' i j [k] = 

  1053        (<(j = i + int k + 1)> \<and>* ones i (i + int k) \<and>* zero j)"

  1054   apply (unfold reps'_def, default, auto simp:sep_conj_ac)

  1055   by (sep_cancel+, simp add:pasrt_def)+

  1056 

  1057 

  1058 section {* Basic macros for TM *}

  1059 

  1060 lemma st_upd: 

  1061   assumes pre: "(st i' ** r) (trset_of (f, x, i, y, z))"

  1062   shows "(st i'' ** r) (trset_of (f, x,  i'', y, z))"

  1063 proof -

  1064   from stimes_sgD[OF pre[unfolded st_def], unfolded trset_of.simps, unfolded stD[OF pre]]

  1065   have "r (tprog_set x \<union> tpc_set i' \<union> tpos_set y \<union> tmem_set z \<union> tfaults_set f - tpc_set i')"

  1066     by blast

  1067   moreover have 

  1068     "(tprog_set x \<union> tpc_set i' \<union> tpos_set y \<union> tmem_set z \<union> tfaults_set f - tpc_set i') =

  1069      (tprog_set x \<union> tpos_set y \<union> tmem_set z \<union> tfaults_set f)"

  1070     by (unfold tpn_set_def, auto)

  1071   ultimately have r_rest: "r (tprog_set x \<union> tpos_set y \<union> tmem_set z \<union> tfaults_set f)"

  1072     by auto

  1073   show ?thesis

  1074   proof(rule sep_conjI[where Q = r, OF _ r_rest])

  1075     show "st i'' (tpc_set i'')" 

  1076       by (unfold st_def sg_def, simp)

  1077   next

  1078     show "tpc_set i'' ## tprog_set x \<union> tpos_set y \<union> tmem_set z \<union> tfaults_set f"

  1079       by (unfold tpn_set_def sep_disj_set_def, auto)

  1080   next

  1081     show "trset_of (f, x, i'', y, z) =

  1082              tpc_set i'' + (tprog_set x \<union> tpos_set y \<union> tmem_set z \<union> tfaults_set f)"

  1083       by (unfold trset_of.simps plus_set_def, auto)

  1084   qed

  1085 qed

  1086 

  1087 lemma pos_upd: 

  1088   assumes pre: "(ps i ** r) (trset_of (f, x, y, i', z))"

  1089   shows "(ps j ** r) (trset_of (f, x, y, j, z))"

  1090 proof -

  1091   from stimes_sgD[OF pre[unfolded ps_def], unfolded trset_of.simps, unfolded psD[OF pre]]

  1092   have "r (tprog_set x \<union> tpc_set y \<union> tpos_set i \<union> tmem_set z \<union> 

  1093               tfaults_set f - tpos_set i)" (is "r ?xs")

  1094     by blast

  1095   moreover have 

  1096     "?xs = tprog_set x \<union> tpc_set y  \<union> tmem_set z \<union> tfaults_set f"

  1097     by (unfold tpn_set_def, auto)

  1098   ultimately have r_rest: "r \<dots>"

  1099     by auto

  1100   show ?thesis

  1101   proof(rule sep_conjI[where Q = r, OF _ r_rest])

  1102     show "ps j (tpos_set j)" 

  1103       by (unfold ps_def sg_def, simp)

  1104   next

  1105     show "tpos_set j ## tprog_set x \<union> tpc_set y \<union> tmem_set z \<union> tfaults_set f"

  1106       by (unfold tpn_set_def sep_disj_set_def, auto)

  1107   next

  1108     show "trset_of (f, x, y, j, z) = 

  1109              tpos_set j + (tprog_set x \<union> tpc_set y \<union> tmem_set z \<union> tfaults_set f)"

  1110       by (unfold trset_of.simps plus_set_def, auto)

  1111   qed

  1112 qed

  1113 

  1114 lemma TM_in_simp: "({TM a v} \<subseteq> 

  1115                       tprog_set x \<union> tpc_set y \<union> tpos_set z \<union> tmem_set mem \<union> tfaults_set f) = 

  1116                              ({TM a v} \<subseteq> tmem_set mem)"

  1117   by (unfold tpn_set_def, auto)

  1118 

  1119 lemma tmem_set_upd: 

  1120   "{TM a v} \<subseteq> tmem_set mem \<Longrightarrow> 

  1121         tmem_set (mem(a:=Some v')) = ((tmem_set mem) - {TM a v}) \<union> {TM a v'}"

  1122   by (unfold tpn_set_def, auto)

  1123 

  1124 lemma tmem_set_disj: "{TM a v} \<subseteq> tmem_set mem \<Longrightarrow> 

  1125                             {TM a v'} \<inter>  (tmem_set mem - {TM a v}) = {}"

  1126   by (unfold tpn_set_def, auto)

  1127 

  1128 lemma smem_upd: "((tm a v) ** r) (trset_of (f, x, y, z, mem))  \<Longrightarrow> 

  1129                     ((tm a v') ** r) (trset_of (f, x, y, z, mem(a := Some v')))"

  1130 proof -

  1131   have eq_s: "(tprog_set x \<union> tpc_set y \<union> tpos_set z \<union> tmem_set mem \<union> tfaults_set f - {TM a v}) =

  1132     (tprog_set x \<union> tpc_set y \<union> tpos_set z \<union> (tmem_set mem - {TM a v}) \<union> tfaults_set f)"

  1133     by (unfold tpn_set_def, auto)

  1134   assume g: "(tm a v \<and>* r) (trset_of (f, x, y, z, mem))"

  1135   from this[unfolded trset_of.simps tm_def]