1 header {* 

     2  {\em Abacus} defined as macros of TM

     3  *}

     4 

     5 theory Hoare_abc

     6 imports Hoare_tm Finite_Set

     7 begin

     8 

     9 

    10 text {*

    11   {\em Abacus} instructions

    12 *}

    13 

    14 (*

    15 text {* The following Abacus instructions will be replaced by TM macros. *}

    16 datatype abc_inst =

    17   -- {* @{text "Inc n"} increments the memory cell (or register) 

    18          with address @{text "n"} by one.

    19      *}

    20      Inc nat

    21   -- {*

    22      @{text "Dec n label"} decrements the memory cell with address @{text "n"} by one. 

    23       If cell @{text "n"} is already zero, no decrements happens and the executio jumps to

    24       the instruction labeled by @{text "label"}.

    25      *}

    26    | Dec nat nat

    27   -- {*

    28   @{text "Goto label"} unconditionally jumps to the instruction labeled by @{text "label"}.

    29   *}

    30    | Goto nat

    31 

    32 *)

    33 

    34 datatype aresource = 

    35     M nat nat

    36   (* | C nat abc_inst *) (* C resource is not needed because there is no Abacus code any more *)  

    37   | At nat

    38   | Faults nat

    39 

    40 

    41 section {* An interpretation from Abacus to Turing Machine *}

    42 

    43 fun recse_map :: "nat list \<Rightarrow> aresource \<Rightarrow> tassert" where

    44   "recse_map ks (M a v) = <(a < length ks \<and> ks!a = v \<or> a \<ge> length ks \<and> v = 0)>" |

    45   "recse_map ks (At l) = st l" |

    46   "recse_map ks (Faults n) = sg {TFaults n}"

    47 

    48 definition "IA ars = (EXS ks i. ps 2 \<and>* zero 0 \<and>* zero 1 \<and>* (reps 2 i ks) \<and>* 

    49                                      fam_conj {i<..} zero \<and>* 

    50                                 fam_conj ars (recse_map ks))"

    51 

    52 

    53 section {* A virtually defined Abacus *}

    54 

    55 text {* The following Abacus instructions are to be defined as TM macros *}

    56 

    57 definition "pc l = sg {At l}"

    58 

    59 definition "mm a v =sg ({M a v})"

    60 

    61 type_synonym assert = "aresource set \<Rightarrow> bool"

    62 

    63 lemma tm_hoare_inc1:

    64   assumes h: "a < length ks \<and> ks ! a = v \<or> length ks \<le> a \<and> v = 0"

    65   shows "

    66     \<lbrace>st i \<and>* ps u \<and>* zero (u - 2) \<and>* zero (u - 1) \<and>* reps u ia ks \<and>* fam_conj {ia<..} zero\<rbrace> 

    67     i :[Inc a ]: j

    68     \<lbrace>st j \<and>*

    69      ps u \<and>*

    70      zero (u - 2) \<and>*

    71      zero (u - 1) \<and>*

    72      reps u (ia + int (reps_len (list_ext a ks)) - int (reps_len ks) + 1) ((list_ext a ks)[a := Suc v]) \<and>*

    73      fam_conj {ia + int (reps_len (list_ext a ks)) - int (reps_len ks) + 1<..} zero\<rbrace>"

    74   using h

    75 proof

    76   assume hh: "a < length ks \<and> ks ! a = v"

    77   hence "a < length ks" by simp 

    78   from list_ext_lt [OF this] tm_hoare_inc00[OF hh]

    79   show ?thesis by simp

    80 next

    81   assume "length ks \<le> a \<and> v = 0"

    82   from tm_hoare_inc01[OF this]

    83   show ?thesis by simp

    84 qed

    85 

    86 lemma tm_hoare_inc2: 

    87   assumes "mm a v sr"

    88   shows "

    89     \<lbrace> (fam_conj sr (recse_map ks) \<and>*

    90        st i \<and>* ps 2 \<and>* zero 0 \<and>* zero 1 \<and>* reps 2 ia ks \<and>* fam_conj {ia<..} zero) \<rbrace> 

    91           i:[ (Inc a) ]:j   

    92     \<lbrace> (fam_conj {M a (Suc v)} (recse_map (list_ext a ks[a := Suc v])) \<and>*

    93            st j \<and>*

    94            ps 2 \<and>*

    95            zero 0 \<and>*

    96            zero 1 \<and>*

    97            reps 2 (ia + int (reps_len (list_ext a ks)) - int (reps_len ks) + 1) ((list_ext a ks)[a := Suc v]) \<and>*

    98            fam_conj {ia + int (reps_len (list_ext a ks)) - int (reps_len ks) + 1<..} zero)\<rbrace>"

    99 proof -

   100   from `mm a v sr` have eq_sr: "sr = {M a v}" by (auto simp:mm_def sg_def)

   101   from tm_hoare_inc1[where u = 2]

   102   have "a < length ks \<and> ks ! a = v \<or> length ks \<le> a \<and> v = 0 \<Longrightarrow>

   103         \<lbrace>st i \<and>* ps 2 \<and>* zero 0 \<and>* zero 1 \<and>* reps 2 ia ks \<and>* fam_conj {ia<..} zero\<rbrace> 

   104              i :[Inc a ]: j

   105         \<lbrace>(st j \<and>*

   106            ps 2 \<and>*

   107            zero 0 \<and>*

   108            zero 1 \<and>*

   109            reps 2 (ia + int (reps_len (list_ext a ks)) - int (reps_len ks) + 1) ((list_ext a ks)[a := Suc v]) \<and>*

   110            fam_conj {ia + int (reps_len (list_ext a ks)) - int (reps_len ks) + 1<..} zero)\<rbrace>" by simp

   111   thus ?thesis

   112     apply (unfold eq_sr)

   113     apply (simp add:fam_conj_simps list_ext_get_upd list_ext_len)

   114     by (rule tm.pre_condI, blast)

   115 qed

   116 

   117 locale IA_disjoint = 

   118   fixes s s' s1 cnf

   119   assumes h_IA: "IA (s + s') s1"

   120   and h_disj: "s ## s'"

   121   and h_conf: "s1 \<subseteq> trset_of cnf"

   122 begin

   123 

   124 lemma at_disj1: 

   125   assumes at_in: "At i \<in> s"

   126   shows "At j \<notin> s'"

   127 proof

   128   from h_IA[unfolded IA_def]

   129   obtain ks idx

   130     where "((ps 2 \<and>* zero 0 \<and>* zero 1 \<and>* 

   131               reps 2 idx ks \<and>* fam_conj {idx<..} zero) \<and>* 

   132               fam_conj (s + s') (recse_map ks)) s1" (is "(?P \<and>* ?Q) s1")

   133     by (auto elim!:EXS_elim simp:sep_conj_ac)

   134   then obtain ss1 ss2 where "s1 = ss1 + ss2" "ss1 ## ss2" "?P ss1" "?Q ss2"

   135     by (auto elim:sep_conjE)

   136   from `?Q ss2`[unfolded fam_conj_disj_simp[OF h_disj]]

   137   obtain tt1 tt2

   138     where "ss2 = tt1 + tt2" "tt1 ## tt2" 

   139             "(fam_conj s (recse_map ks)) tt1"

   140             "(fam_conj s' (recse_map ks)) tt2"

   141     by (auto elim:sep_conjE)

   142   assume "At j \<in> s'"

   143   from `(fam_conj s' (recse_map ks)) tt2` [unfolded fam_conj_elm_simp[OF this]]

   144        `ss2 = tt1 + tt2` `s1 = ss1 + ss2` h_conf

   145   have "TAt j \<in> trset_of cnf"

   146     by (auto elim!:sep_conjE simp: st_def sg_def tpn_set_def set_ins_def)

   147   moreover from `(fam_conj s (recse_map ks)) tt1` [unfolded fam_conj_elm_simp[OF at_in]]

   148                 `ss2 = tt1 + tt2` `s1 = ss1 + ss2` h_conf

   149   have "TAt i \<in> trset_of cnf"

   150     by (auto elim!:sep_conjE simp: st_def sg_def tpn_set_def set_ins_def)

   151   ultimately have "i = j"

   152     by (cases cnf, simp add:trset_of.simps tpn_set_def)

   153   from at_in `At j \<in> s'` h_disj

   154   show False 

   155     by (unfold `i = j`, auto simp:set_ins_def)

   156 qed

   157 

   158 lemma at_disj2: "At i \<in> s' \<Longrightarrow> At j \<notin> s"

   159   by (metis at_disj1)

   160 

   161 lemma m_disj1: 

   162   assumes m_in: "M a v \<in> s"

   163   shows "M a v' \<notin> s'"

   164 proof

   165   from h_IA[unfolded IA_def]

   166   obtain ks idx

   167     where "((ps 2 \<and>* zero 0 \<and>* zero 1 \<and>* 

   168               reps 2 idx ks \<and>* fam_conj {idx<..} zero) \<and>* 

   169               fam_conj (s + s') (recse_map ks)) s1" (is "(?P \<and>* ?Q) s1")

   170     by (auto elim!:EXS_elim simp:sep_conj_ac)

   171   then obtain ss1 ss2 where "s1 = ss1 + ss2" "ss1 ## ss2" "?P ss1" "?Q ss2"

   172     by (auto elim:sep_conjE)

   173   from `?Q ss2`[unfolded fam_conj_disj_simp[OF h_disj]]

   174   obtain tt1 tt2

   175     where "ss2 = tt1 + tt2" "tt1 ## tt2" 

   176             "(fam_conj s (recse_map ks)) tt1"

   177             "(fam_conj s' (recse_map ks)) tt2"

   178     by (auto elim:sep_conjE)

   179   assume "M a v' \<in> s'"

   180   from `(fam_conj s' (recse_map ks)) tt2` [unfolded fam_conj_elm_simp[OF this]

   181         recse_map.simps]

   182   have "(a < length ks \<and> ks ! a = v' \<or> length ks \<le> a \<and> v' = 0)"

   183     by (auto simp:pasrt_def)

   184   moreover from `(fam_conj s (recse_map ks)) tt1` [unfolded fam_conj_elm_simp[OF m_in]

   185                          recse_map.simps]

   186   have "a < length ks \<and> ks ! a = v \<or> length ks \<le> a \<and> v = 0"

   187     by (auto simp:pasrt_def)

   188   moreover note m_in `M a v' \<in> s'` h_disj

   189   ultimately show False

   190     by (auto simp:set_ins_def)

   191 qed

   192 

   193 lemma m_disj2: "M a v \<in> s' \<Longrightarrow> M a v' \<notin> s"

   194   by (metis m_disj1)

   195 

   196 end

   197 

   198 lemma EXS_elim1: 

   199   assumes "((EXS x. P(x)) \<and>* r) s"

   200   obtains x where "(P(x) \<and>* r) s"

   201   by (metis EXS_elim assms sep_conj_exists1)

   202 

   203 lemma hoare_inc[step]: "IA. \<lbrace> pc i ** mm a v \<rbrace> 

   204                         i:[ (Inc a) ]:j   

   205                       \<lbrace> pc j ** mm a (Suc v)\<rbrace>"

   206                       (is "IA. \<lbrace> pc i ** ?P \<rbrace> 

   207                         i:[ ?code ?e ]:j   

   208                       \<lbrace> pc ?e ** ?Q\<rbrace>")

   209 proof(induct rule:tm.IHoareI)

   210   case (IPre s' s r cnf)

   211   let ?cnf = "(trset_of cnf)"

   212   from IPre

   213   have h: "(pc i \<and>* ?P) s" "(s ## s')" "(IA (s + s') \<and>* i :[ ?code(?e) ]: j \<and>* r) ?cnf"

   214     by (metis condD)+

   215   from h(1) obtain sr where

   216       eq_s: "s = {At i} \<union>  sr" "{At i} ##  sr" "?P sr"

   217     by (auto dest!:sep_conjD simp:set_ins_def pc_def sg_def)

   218   hence "At i \<in> s" by auto

   219   from h(3) obtain s1 s2 s3

   220     where hh: "?cnf = s1 + s2 + s3"

   221               "s1 ## s2 \<and> s2 ## s3 \<and> s1 ## s3" 

   222               "IA (s + s') s1" 

   223               "(i :[ ?code ?e ]: j) s2"

   224               "r s3"

   225     apply (auto elim!:sep_conjE intro!:sep_conjI simp:sep_conj_ac)

   226     by (metis sep_add_commute sep_disj_addD1 sep_disj_addD2 sep_disj_commuteI)

   227   interpret ia_disj: IA_disjoint s s' s1 cnf

   228   proof

   229     from `IA (s + s') s1` show "IA (s + s') s1" .

   230   next

   231     from `s ## s'` show "s ## s'" .

   232   next

   233     from hh(1) show "s1 \<subseteq> ?cnf" by (auto simp:set_ins_def)

   234   qed

   235   from hh(1) have s1_belong: "s1 \<subseteq> ?cnf" by (auto simp:set_ins_def)

   236   from hh(3)

   237   have "(EXS ks ia.

   238          ps 2 \<and>*

   239          zero 0 \<and>*

   240          zero 1 \<and>*

   241          reps 2 ia ks \<and>*

   242          fam_conj {ia<..} zero \<and>*

   243          (st i \<and>* fam_conj sr (recse_map ks)) \<and>* fam_conj s' (recse_map ks))

   244         s1"

   245     apply (unfold IA_def fam_conj_disj_simp[OF h(2)])

   246     apply (unfold eq_s)

   247     by (insert eq_s(2), simp add: fam_conj_disj_simp[OF eq_s(2)] fam_conj_simps set_ins_def)

   248   then obtain ks ia

   249     where "((fam_conj sr (recse_map ks) \<and>* st i \<and>* ps 2 \<and>* zero 0 \<and>* zero 1 \<and>*

   250              reps 2 ia ks \<and>* fam_conj {ia<..} zero) \<and>* fam_conj s' (recse_map ks)) s1" 

   251     (is "(?PP \<and>* ?QQ) s1")

   252     by (unfold pred_ex_def, auto simp:sep_conj_ac)

   253   then obtain ss1 ss2 where pres:

   254         "s1 = ss1 + ss2" "ss1 ## ss2"

   255         "?PP ss1"

   256         "?QQ ss2"

   257     by (auto elim!:sep_conjE intro!:sep_conjI)

   258   from ia_disj.at_disj1 [OF `At i \<in> s`]

   259   have at_fresh_s': "At ?e \<notin>  s'" .

   260   have at_fresh_sr: "At ?e \<notin> sr"

   261   proof

   262     assume at_in: "At ?e \<in> sr"

   263     from h(3)[unfolded IA_def fam_conj_disj_simp[OF h(2)]]

   264     have "TAt ?e \<in> trset_of cnf"

   265       apply (elim EXS_elim1)

   266       apply (unfold eq_s fam_conj_disj_simp[OF eq_s(2), unfolded set_ins_def]

   267              fam_conj_elm_simp[OF at_in])

   268       apply (erule_tac sep_conjE, unfold set_ins_def)+

   269       by (auto simp:sep_conj_ac fam_conj_simps st_def sg_def tpn_set_def)

   270     moreover from pres(1, 3) hh(1) have "TAt i \<in> trset_of cnf" 

   271       apply(erule_tac sep_conjE)

   272       apply(erule_tac sep_conjE)

   273       by (auto simp:st_def tpc_set_def sg_def set_ins_def)

   274     ultimately have "i = ?e"

   275       by (cases cnf, auto simp:tpn_set_def trset_of.simps)

   276     from eq_s[unfolded this] at_in

   277     show "False" by (auto simp:set_ins_def)

   278   qed

   279   from pres(3) and hh(2, 4, 5) pres(2, 4)

   280   have pres1: "(?PP \<and>* i :[ ?code(?e)]: j \<and>*  (r \<and>* (fam_conj s' (recse_map ks))))

   281          (trset_of cnf)"

   282     apply (unfold hh(1) pres(1))

   283     apply (rule sep_conjI[where x=ss1 and y = "ss2 + s2 + s3"], assumption+)

   284     apply (rule sep_conjI[where x="s2" and y = "ss2 + s3"], assumption+)

   285     apply (rule sep_conjI[where x="s3" and y = ss2], assumption+)

   286     by (auto simp:set_ins_def)

   287   (*****************************************************************************)

   288   let ?ks_f = "\<lambda> sr ks. list_ext a ks[a := Suc v]"

   289   let ?elm_f = "\<lambda> sr. {M a (Suc v)}"

   290   let ?idx_f = "\<lambda> sr ks ia. (ia + int (reps_len (list_ext a ks)) - int (reps_len ks) + 1)"

   291   (*----------------------------------------------------------------------------*)

   292   (******************************************************************************)

   293   from tm_hoare_inc2 [OF eq_s(3), unfolded tm.Hoare_gen_def, rule_format, OF pres1]

   294   obtain k where "((fam_conj (?elm_f sr) (recse_map (?ks_f sr ks)) \<and>*

   295         st ?e \<and>*

   296         ps 2 \<and>*

   297         zero 0 \<and>* zero 1 \<and>* reps 2 (?idx_f sr ks ia) (?ks_f sr ks) \<and>* 

   298         fam_conj {?idx_f sr ks ia<..} zero) \<and>*

   299        i :[ ?code ?e ]: j \<and>* r \<and>* fam_conj s' (recse_map ks))

   300        (trset_of (sep_exec.run tstep (Suc k) cnf))" by blast

   301   (*----------------------------------------------------------------------------*)

   302   moreover have "(pc ?e \<and>* ?Q) ({At ?e} \<union> ?elm_f sr)"

   303   proof -

   304     have "pc ?e {At ?e}" by (simp add:pc_def sg_def)

   305   (******************************************************************************)

   306     moreover have "?Q (?elm_f sr)" 

   307       by (simp add:mm_def sg_def)

   308   (*----------------------------------------------------------------------------*)

   309     moreover 

   310   (******************************************************************************)

   311     have "{At ?e} ## ?elm_f sr" by (simp add:set_ins_def)

   312   (*----------------------------------------------------------------------------*)

   313     ultimately show ?thesis by (auto intro!:sep_conjI simp:set_ins_def)

   314   qed

   315   moreover 

   316   (******************************************************************************)

   317   from ia_disj.m_disj1 `?P sr` `s = {At i} \<union> sr` 

   318   have "?elm_f sr ## s'" by (auto simp:set_ins_def mm_def sg_def)

   319   (*----------------------------------------------------------------------------*)

   320   with at_fresh_s' 

   321   have fresh_atm: "{At ?e} \<union> ?elm_f sr ## s'" by (auto simp:set_ins_def)

   322   moreover have eq_map: "\<And> elm. elm \<in> s' \<Longrightarrow> 

   323                            (recse_map ks elm) = (recse_map (?ks_f sr ks) elm)"

   324   proof -

   325     fix elm

   326     assume elm_in: "elm \<in> s'"

   327     show "(recse_map ks elm) = (recse_map (?ks_f sr ks) elm)"

   328     proof(cases elm)

   329       (*******************************************************************)

   330       case (M a' v')

   331       from eq_s have "M a v \<in> s" by (auto simp:set_ins_def mm_def sg_def)

   332       with elm_in ia_disj.m_disj1[OF this] M

   333       have "a \<noteq> a'" by auto

   334       thus ?thesis

   335         apply (auto simp:M recse_map.simps pasrt_def list_ext_len)

   336         apply (case_tac "a < length ks", auto simp:list_ext_len_eq list_ext_lt)

   337         apply (case_tac "a' < Suc a", auto simp:list_ext_len_eq list_ext_lt)

   338         by (metis (full_types) bot_nat_def 

   339               leI le_trans less_Suc_eq_le list_ext_lt_get list_ext_tail set_zero_def)

   340       (*-----------------------------------------------------------------*)

   341     qed auto

   342   qed

   343   ultimately show ?case 

   344     apply (rule_tac x = k in exI, rule_tac x = "{At ?e} \<union> ?elm_f sr" in exI)

   345     apply (unfold IA_def, intro condI, assumption+)

   346     apply (rule_tac x = "?ks_f sr ks" in pred_exI)

   347     apply (rule_tac x = "?idx_f sr ks ia" in pred_exI)

   348     apply (unfold fam_conj_disj_simp[OF fresh_atm])

   349     apply (auto simp:sep_conj_ac fam_conj_simps)

   350     (***************************************************************************)

   351     (* apply (unfold fam_conj_insert_simp [OF h_fresh1[OF at_fresh_sr]], simp) *)

   352     (*-------------------------------------------------------------------------*)

   353     apply (sep_cancel)+

   354     by (simp add: fam_conj_ext_eq[where I = "s'", OF eq_map])

   355 qed

   356 

   357 lemma tm_hoare_dec_fail:

   358   assumes "mm a 0 sr"

   359   shows 

   360   "\<lbrace> fam_conj sr (recse_map ks) \<and>*

   361     st i \<and>* ps 2 \<and>* zero 0 \<and>* zero 1 \<and>* reps 2 ia ks \<and>* fam_conj {ia<..} zero \<rbrace> 

   362        i:[ (Dec a e) ]:j 

   363    \<lbrace> fam_conj {M a 0} (recse_map (list_ext a ks[a := 0])) \<and>*

   364      st e \<and>*

   365      ps 2 \<and>*

   366      zero 0 \<and>*

   367      zero 1 \<and>*

   368      reps 2 (ia + int (reps_len (list_ext a ks)) - int (reps_len ks)) (list_ext a ks[a := 0]) \<and>*

   369      fam_conj {ia + int (reps_len (list_ext a ks)) - int (reps_len ks) <..} zero\<rbrace>"

   370 proof - 

   371   from `mm a 0 sr` have eq_sr: "sr = {M a 0}" by (auto simp:mm_def sg_def)

   372   { assume h: "a < length ks \<and> ks ! a = 0 \<or> length ks \<le> a"

   373     from tm_hoare_dec_fail1[where u = 2, OF this]

   374     have "\<lbrace>st i \<and>* ps 2 \<and>* zero 0 \<and>* zero 1 \<and>* reps 2 ia ks \<and>* fam_conj {ia<..} zero\<rbrace>  

   375                   i :[ Dec a e ]: j

   376           \<lbrace>st e \<and>* ps 2 \<and>* zero 0 \<and>* zero 1 \<and>*

   377             reps 2 (ia + int (reps_len (list_ext a ks)) - int (reps_len ks)) (list_ext a ks[a := 0]) \<and>*

   378             fam_conj {ia + int (reps_len (list_ext a ks)) - int (reps_len ks)<..} zero\<rbrace>"

   379     by (simp)

   380   }

   381   thus ?thesis

   382     apply (unfold eq_sr)

   383     apply (simp add:fam_conj_simps list_ext_get_upd list_ext_len)

   384     by (rule tm.pre_condI, blast)

   385 qed

   386 

   387 lemma hoare_dec_fail: "IA. \<lbrace> pc i ** mm a 0 \<rbrace>

   388                               i:[ (Dec a e) ]:j   

   389                            \<lbrace> pc e ** mm a 0 \<rbrace>"

   390                       (is "IA. \<lbrace> pc i ** ?P \<rbrace> 

   391                                 i:[ ?code ?e]:j   

   392                                \<lbrace> pc ?e ** ?Q\<rbrace>")

   393 proof(induct rule:tm.IHoareI)

   394   case (IPre s' s r cnf)

   395   let ?cnf = "(trset_of cnf)"

   396   from IPre

   397   have h: "(pc i \<and>* ?P) s" "(s ## s')" "(IA (s + s') \<and>* i :[ ?code(?e) ]: j \<and>* r) ?cnf"

   398     by (metis condD)+

   399   from h(1) obtain sr where

   400       eq_s: "s = {At i} \<union>  sr" "{At i} ##  sr" "?P sr"

   401     by (auto dest!:sep_conjD simp:set_ins_def pc_def sg_def)

   402   hence "At i \<in> s" by auto

   403   from h(3) obtain s1 s2 s3

   404     where hh: "?cnf = s1 + s2 + s3"

   405               "s1 ## s2 \<and> s2 ## s3 \<and> s1 ## s3" 

   406               "IA (s + s') s1" 

   407               "(i :[ ?code ?e ]: j) s2"

   408               "r s3"

   409     apply (auto elim!:sep_conjE intro!:sep_conjI simp:sep_conj_ac)

   410     by (metis sep_add_commute sep_disj_addD1 sep_disj_addD2 sep_disj_commuteI)

   411   interpret ia_disj: IA_disjoint s s' s1 cnf

   412   proof

   413     from `IA (s + s') s1` show "IA (s + s') s1" .

   414   next

   415     from `s ## s'` show "s ## s'" .

   416   next

   417     from hh(1) show "s1 \<subseteq> ?cnf" by (auto simp:set_ins_def)

   418   qed

   419   from hh(1) have s1_belong: "s1 \<subseteq> ?cnf" by (auto simp:set_ins_def)

   420   from hh(3)

   421   have "(EXS ks ia.

   422          ps 2 \<and>*

   423          zero 0 \<and>*

   424          zero 1 \<and>*

   425          reps 2 ia ks \<and>*

   426          fam_conj {ia<..} zero \<and>*

   427          (st i \<and>* fam_conj sr (recse_map ks)) \<and>* fam_conj s' (recse_map ks))

   428         s1"

   429     apply (unfold IA_def fam_conj_disj_simp[OF h(2)])

   430     apply (unfold eq_s)

   431     by (insert eq_s(2), simp add: fam_conj_disj_simp[OF eq_s(2)] fam_conj_simps set_ins_def)

   432   then obtain ks ia

   433     where "((fam_conj sr (recse_map ks) \<and>* st i \<and>* ps 2 \<and>* zero 0 \<and>* zero 1 \<and>*

   434              reps 2 ia ks \<and>* fam_conj {ia<..} zero) \<and>* fam_conj s' (recse_map ks)) s1" 

   435     (is "(?PP \<and>* ?QQ) s1")

   436     by (unfold pred_ex_def, auto simp:sep_conj_ac)

   437   then obtain ss1 ss2 where pres:

   438         "s1 = ss1 + ss2" "ss1 ## ss2"

   439         "?PP ss1"

   440         "?QQ ss2"

   441     by (auto elim!:sep_conjE intro!:sep_conjI)

   442   from ia_disj.at_disj1 [OF `At i \<in> s`]

   443   have at_fresh_s': "At ?e \<notin>  s'" .

   444   have at_fresh_sr: "At ?e \<notin> sr"

   445   proof

   446     assume at_in: "At ?e \<in> sr"

   447     from h(3)[unfolded IA_def fam_conj_disj_simp[OF h(2)]]

   448     have "TAt ?e \<in> trset_of cnf"

   449       apply (elim EXS_elim1)

   450       apply (unfold eq_s fam_conj_disj_simp[OF eq_s(2), unfolded set_ins_def]

   451              fam_conj_elm_simp[OF at_in])

   452       apply (erule_tac sep_conjE, unfold set_ins_def)+

   453       by (auto simp:sep_conj_ac fam_conj_simps st_def sg_def tpn_set_def)

   454     moreover from pres(1, 3) hh(1) have "TAt i \<in> trset_of cnf" 

   455       apply(erule_tac sep_conjE)

   456       apply(erule_tac sep_conjE)

   457       by (auto simp:st_def tpc_set_def sg_def set_ins_def)

   458     ultimately have "i = ?e"

   459       by (cases cnf, auto simp:tpn_set_def trset_of.simps)

   460     from eq_s[unfolded this] at_in

   461     show "False" by (auto simp:set_ins_def)

   462   qed

   463   from pres(3) and hh(2, 4, 5) pres(2, 4)

   464   have pres1: "(?PP \<and>* i :[ ?code(?e)]: j \<and>*  (r \<and>* (fam_conj s' (recse_map ks))))

   465          (trset_of cnf)"

   466     apply (unfold hh(1) pres(1))

   467     apply (rule sep_conjI[where x=ss1 and y = "ss2 + s2 + s3"], assumption+)

   468     apply (rule sep_conjI[where x="s2" and y = "ss2 + s3"], assumption+)

   469     apply (rule sep_conjI[where x="s3" and y = ss2], assumption+)

   470     by (auto simp:set_ins_def)

   471   (*****************************************************************************)

   472   let ?ks_f = "\<lambda> sr ks. list_ext a ks[a:=0]"

   473   let ?elm_f = "\<lambda> sr. {M a 0}"

   474   let ?idx_f = "\<lambda> sr ks ia. (ia + int (reps_len (list_ext a ks)) - int (reps_len ks))"

   475   (*----------------------------------------------------------------------------*)

   476   (******************************************************************************)

   477   from tm_hoare_dec_fail[OF `?P sr`, unfolded tm.Hoare_gen_def, rule_format, OF pres1]

   478   obtain k where "((fam_conj (?elm_f sr) (recse_map (?ks_f sr ks)) \<and>*

   479         st ?e \<and>*

   480         ps 2 \<and>*

   481         zero 0 \<and>* zero 1 \<and>* reps 2 (?idx_f sr ks ia) (?ks_f sr ks) \<and>* 

   482         fam_conj {?idx_f sr ks ia<..} zero) \<and>*

   483        i :[ ?code ?e ]: j \<and>* r \<and>* fam_conj s' (recse_map ks))

   484        (trset_of (sep_exec.run tstep (Suc k) cnf))" by blast

   485   (*----------------------------------------------------------------------------*)

   486   moreover have "(pc ?e \<and>* ?Q) ({At ?e} \<union> ?elm_f sr)"

   487   proof -

   488     have "pc ?e {At ?e}" by (simp add:pc_def sg_def)

   489   (******************************************************************************)

   490     moreover have "?Q (?elm_f sr)" 

   491       by (simp add:mm_def sg_def)

   492   (*----------------------------------------------------------------------------*)

   493     moreover 

   494   (******************************************************************************)

   495     have "{At ?e} ## ?elm_f sr" by (simp add:set_ins_def)

   496   (*----------------------------------------------------------------------------*)

   497     ultimately show ?thesis by (auto intro!:sep_conjI simp:set_ins_def)

   498   qed

   499   moreover 

   500   (******************************************************************************)

   501   from ia_disj.m_disj1 `?P sr` `s = {At i} \<union> sr` 

   502   have "?elm_f sr ## s'" by (auto simp:set_ins_def mm_def sg_def)

   503   (*----------------------------------------------------------------------------*)

   504   with at_fresh_s' 

   505   have fresh_atm: "{At ?e} \<union> ?elm_f sr ## s'" by (auto simp:set_ins_def)

   506   moreover have eq_map: "\<And> elm. elm \<in> s' \<Longrightarrow> 

   507                            (recse_map ks elm) = (recse_map (?ks_f sr ks) elm)"

   508   proof -

   509     fix elm

   510     assume elm_in: "elm \<in> s'"

   511     show "(recse_map ks elm) = (recse_map (?ks_f sr ks) elm)"

   512     proof(cases elm)

   513       (*******************************************************************)

   514       case (M a' v')

   515       from eq_s have "M a 0 \<in> s" by (auto simp:set_ins_def mm_def sg_def)

   516       with elm_in ia_disj.m_disj1[OF this] M

   517       have "a \<noteq> a'" by auto

   518       thus ?thesis

   519         apply (auto simp:M recse_map.simps pasrt_def list_ext_len)

   520         apply (case_tac "a < length ks", auto simp:list_ext_len_eq list_ext_lt)

   521         apply (case_tac "a' < Suc a", auto simp:list_ext_len_eq list_ext_lt)

   522         by (metis (full_types) bot_nat_def 

   523               leI le_trans less_Suc_eq_le list_ext_lt_get list_ext_tail set_zero_def)

   524       (*-----------------------------------------------------------------*)

   525     qed auto

   526   qed

   527   ultimately show ?case 

   528     apply (rule_tac x = k in exI, rule_tac x = "{At ?e} \<union> ?elm_f sr" in exI)

   529     apply (unfold IA_def, intro condI, assumption+)

   530     apply (rule_tac x = "?ks_f sr ks" in pred_exI)

   531     apply (rule_tac x = "?idx_f sr ks ia" in pred_exI)

   532     apply (unfold fam_conj_disj_simp[OF fresh_atm])

   533     apply (auto simp:sep_conj_ac fam_conj_simps)

   534     (***************************************************************************)

   535     (* apply (unfold fam_conj_insert_simp [OF h_fresh1[OF at_fresh_sr]], simp) *)

   536     (*-------------------------------------------------------------------------*)

   537     apply (sep_cancel)+

   538     by (simp add: fam_conj_ext_eq[where I = "s'", OF eq_map])

   539 qed

   540 

   541 lemma hoare_dec_fail_gen[step]: 

   542   assumes "v = 0"

   543   shows 

   544   "IA. \<lbrace> pc i ** mm a v \<rbrace>

   545        i:[ (Dec a e) ]:j   

   546        \<lbrace> pc e ** mm a v \<rbrace>"

   547   by (unfold assms, rule hoare_dec_fail)

   548 

   549 

   550 lemma tm_hoare_dec_suc2:

   551   assumes "mm a (Suc v) sr"

   552   shows "\<lbrace> fam_conj sr (recse_map ks) \<and>*

   553            st i \<and>* ps 2 \<and>* zero 0 \<and>* zero 1 \<and>* reps 2 ia ks \<and>* fam_conj {ia<..} zero \<rbrace>

   554              i:[(Dec a e)]:j

   555          \<lbrace> fam_conj {M a v} (recse_map (list_ext a ks[a := v])) \<and>*

   556            st j \<and>*

   557            ps 2 \<and>*

   558            zero 0 \<and>*

   559            zero 1 \<and>*

   560            reps 2 (ia  - 1) (list_ext a ks[a := v]) \<and>*

   561            fam_conj {ia  - 1<..} zero\<rbrace>"

   562 proof -

   563   from `mm a (Suc v) sr` have eq_sr: "sr = {M a (Suc v)}" by (auto simp:mm_def sg_def)

   564   thus ?thesis

   565     apply (unfold eq_sr)

   566     apply (simp add:fam_conj_simps list_ext_get_upd list_ext_len)

   567     apply (rule tm.pre_condI)

   568     by (drule tm_hoare_dec_suc1[where u = "2"], simp)

   569 qed

   570 

   571 lemma hoare_dec_suc2: 

   572   "IA. \<lbrace>(pc i \<and>* mm a (Suc v))\<rbrace>  

   573           i :[ Dec a e ]: j 

   574        \<lbrace>pc j \<and>* mm a v\<rbrace>"

   575        (is "IA. \<lbrace> pc i ** ?P \<rbrace> 

   576                    i:[ ?code ?e]:j   

   577                 \<lbrace> pc ?e ** ?Q\<rbrace>")

   578 proof(induct rule:tm.IHoareI)

   579   case (IPre s' s r cnf)

   580   let ?cnf = "(trset_of cnf)"

   581   from IPre

   582   have h: "(pc i \<and>* ?P) s" "(s ## s')" "(IA (s + s') \<and>* i :[ ?code(?e) ]: j \<and>* r) ?cnf"

   583     by (metis condD)+

   584   from h(1) obtain sr where

   585       eq_s: "s = {At i} \<union>  sr" "{At i} ##  sr" "?P sr"

   586     by (auto dest!:sep_conjD simp:set_ins_def pc_def sg_def)

   587   hence "At i \<in> s" by auto

   588   from h(3) obtain s1 s2 s3

   589     where hh: "?cnf = s1 + s2 + s3"

   590               "s1 ## s2 \<and> s2 ## s3 \<and> s1 ## s3" 

   591               "IA (s + s') s1" 

   592               "(i :[ ?code ?e ]: j) s2"

   593               "r s3"

   594     apply (auto elim!:sep_conjE intro!:sep_conjI simp:sep_conj_ac)

   595     by (metis sep_add_commute sep_disj_addD1 sep_disj_addD2 sep_disj_commuteI)

   596   interpret ia_disj: IA_disjoint s s' s1 cnf

   597   proof

   598     from `IA (s + s') s1` show "IA (s + s') s1" .

   599   next

   600     from `s ## s'` show "s ## s'" .

   601   next

   602     from hh(1) show "s1 \<subseteq> ?cnf" by (auto simp:set_ins_def)

   603   qed

   604   from hh(1) have s1_belong: "s1 \<subseteq> ?cnf" by (auto simp:set_ins_def)

   605   from hh(3)

   606   have "(EXS ks ia.

   607          ps 2 \<and>*

   608          zero 0 \<and>*

   609          zero 1 \<and>*

   610          reps 2 ia ks \<and>*

   611          fam_conj {ia<..} zero \<and>*

   612          (st i \<and>* fam_conj sr (recse_map ks)) \<and>* fam_conj s' (recse_map ks))

   613         s1"

   614     apply (unfold IA_def fam_conj_disj_simp[OF h(2)])

   615     apply (unfold eq_s)

   616     by (insert eq_s(2), simp add: fam_conj_disj_simp[OF eq_s(2)] fam_conj_simps set_ins_def)

   617   then obtain ks ia

   618     where "((fam_conj sr (recse_map ks) \<and>* st i \<and>* ps 2 \<and>* zero 0 \<and>* zero 1 \<and>*

   619              reps 2 ia ks \<and>* fam_conj {ia<..} zero) \<and>* fam_conj s' (recse_map ks)) s1" 

   620     (is "(?PP \<and>* ?QQ) s1")

   621     by (unfold pred_ex_def, auto simp:sep_conj_ac)

   622   then obtain ss1 ss2 where pres:

   623         "s1 = ss1 + ss2" "ss1 ## ss2"

   624         "?PP ss1"

   625         "?QQ ss2"

   626     by (auto elim!:sep_conjE intro!:sep_conjI)

   627   from ia_disj.at_disj1 [OF `At i \<in> s`]

   628   have at_fresh_s': "At ?e \<notin>  s'" .

   629   have at_fresh_sr: "At ?e \<notin> sr"

   630   proof

   631     assume at_in: "At ?e \<in> sr"

   632     from h(3)[unfolded IA_def fam_conj_disj_simp[OF h(2)]]

   633     have "TAt ?e \<in> trset_of cnf"

   634       apply (elim EXS_elim1)

   635       apply (unfold eq_s fam_conj_disj_simp[OF eq_s(2), unfolded set_ins_def]

   636              fam_conj_elm_simp[OF at_in])

   637       apply (erule_tac sep_conjE, unfold set_ins_def)+

   638       by (auto simp:sep_conj_ac fam_conj_simps st_def sg_def tpn_set_def)

   639     moreover from pres(1, 3) hh(1) have "TAt i \<in> trset_of cnf" 

   640       apply(erule_tac sep_conjE)

   641       apply(erule_tac sep_conjE)

   642       by (auto simp:st_def tpc_set_def sg_def set_ins_def)

   643     ultimately have "i = ?e"

   644       by (cases cnf, auto simp:tpn_set_def trset_of.simps)

   645     from eq_s[unfolded this] at_in

   646     show "False" by (auto simp:set_ins_def)

   647   qed

   648   from pres(3) and hh(2, 4, 5) pres(2, 4)

   649   have pres1: "(?PP \<and>* i :[ ?code(?e)]: j \<and>*  (r \<and>* (fam_conj s' (recse_map ks))))

   650          (trset_of cnf)"

   651     apply (unfold hh(1) pres(1))

   652     apply (rule sep_conjI[where x=ss1 and y = "ss2 + s2 + s3"], assumption+)

   653     apply (rule sep_conjI[where x="s2" and y = "ss2 + s3"], assumption+)

   654     apply (rule sep_conjI[where x="s3" and y = ss2], assumption+)

   655     by (auto simp:set_ins_def)

   656   (*****************************************************************************)

   657   let ?ks_f = "\<lambda> sr ks. list_ext a ks[a:=v]"

   658   let ?elm_f = "\<lambda> sr. {M a v}"

   659   let ?idx_f = "\<lambda> sr ks ia. ia  - 1"

   660   (*----------------------------------------------------------------------------*)

   661   (******************************************************************************)

   662   from tm_hoare_dec_suc2[OF `?P sr`, unfolded tm.Hoare_gen_def, rule_format, OF pres1]

   663   obtain k where "((fam_conj (?elm_f sr) (recse_map (?ks_f sr ks)) \<and>*

   664         st ?e \<and>*

   665         ps 2 \<and>*

   666         zero 0 \<and>* zero 1 \<and>* reps 2 (?idx_f sr ks ia) (?ks_f sr ks) \<and>* 

   667         fam_conj {?idx_f sr ks ia<..} zero) \<and>*

   668        i :[ ?code ?e ]: j \<and>* r \<and>* fam_conj s' (recse_map ks))

   669        (trset_of (sep_exec.run tstep (Suc k) cnf))" by blast

   670   (*----------------------------------------------------------------------------*)

   671   moreover have "(pc ?e \<and>* ?Q) ({At ?e} \<union> ?elm_f sr)"

   672   proof -

   673     have "pc ?e {At ?e}" by (simp add:pc_def sg_def)

   674   (******************************************************************************)

   675     moreover have "?Q (?elm_f sr)" 

   676       by (simp add:mm_def sg_def)

   677   (*----------------------------------------------------------------------------*)

   678     moreover 

   679   (******************************************************************************)

   680     have "{At ?e} ## ?elm_f sr" by (simp add:set_ins_def)

   681   (*----------------------------------------------------------------------------*)

   682     ultimately show ?thesis by (auto intro!:sep_conjI simp:set_ins_def)

   683   qed

   684   moreover 

   685   (******************************************************************************)

   686   from ia_disj.m_disj1 `?P sr` `s = {At i} \<union> sr` 

   687   have "?elm_f sr ## s'" by (auto simp:set_ins_def mm_def sg_def)

   688   (*----------------------------------------------------------------------------*)

   689   with at_fresh_s' 

   690   have fresh_atm: "{At ?e} \<union> ?elm_f sr ## s'" by (auto simp:set_ins_def)

   691   moreover have eq_map: "\<And> elm. elm \<in> s' \<Longrightarrow> 

   692                            (recse_map ks elm) = (recse_map (?ks_f sr ks) elm)"

   693   proof -

   694     fix elm

   695     assume elm_in: "elm \<in> s'"

   696     show "(recse_map ks elm) = (recse_map (?ks_f sr ks) elm)"

   697     proof(cases elm)

   698       (*******************************************************************)

   699       case (M a' v')

   700       from eq_s have "M a (Suc v) \<in> s" by (auto simp:set_ins_def mm_def sg_def)

   701       with elm_in ia_disj.m_disj1[OF this] M

   702       have "a \<noteq> a'" by auto

   703       thus ?thesis

   704         apply (auto simp:M recse_map.simps pasrt_def list_ext_len)

   705         apply (case_tac "a < length ks", auto simp:list_ext_len_eq list_ext_lt)

   706         apply (case_tac "a' < Suc a", auto simp:list_ext_len_eq list_ext_lt)

   707         by (metis (full_types) bot_nat_def 

   708               leI le_trans less_Suc_eq_le list_ext_lt_get list_ext_tail set_zero_def)

   709       (*-----------------------------------------------------------------*)

   710     qed auto

   711   qed

   712   ultimately show ?case 

   713     apply (rule_tac x = k in exI, rule_tac x = "{At ?e} \<union> ?elm_f sr" in exI)

   714     apply (unfold IA_def, intro condI, assumption+)

   715     apply (rule_tac x = "?ks_f sr ks" in pred_exI)

   716     apply (rule_tac x = "?idx_f sr ks ia" in pred_exI)

   717     apply (unfold fam_conj_disj_simp[OF fresh_atm])

   718     apply (auto simp:sep_conj_ac fam_conj_simps)

   719     (***************************************************************************)

   720     (* apply (unfold fam_conj_insert_simp [OF h_fresh1[OF at_fresh_sr]], simp) *)

   721     (*-------------------------------------------------------------------------*)

   722     apply (sep_cancel)+

   723     by (simp add: fam_conj_ext_eq[where I = "s'", OF eq_map])

   724 qed

   725 

   726 lemma hoare_dec_suc2_gen[step]: 

   727   assumes "v > 0"

   728   shows 

   729   "IA. \<lbrace>pc i \<and>* mm a v\<rbrace>  

   730           i :[ Dec a e ]: j 

   731        \<lbrace>pc j \<and>* mm a (v - 1)\<rbrace>"

   732 proof -

   733   from assms obtain v' where "v = Suc v'"

   734     by (metis gr_implies_not0 nat.exhaust)

   735   show ?thesis

   736     apply (unfold `v = Suc v'`, simp)

   737     by (rule hoare_dec_suc2)

   738 qed

   739 

   740 definition "Goto e = jmp e"

   741 

   742 lemma hoare_jmp_reps2:

   743       "\<lbrace> st i \<and>* ps u \<and>* reps u v ks \<and>* tm (v + 1) x \<rbrace>

   744                  i:[(jmp e)]:j

   745        \<lbrace> st e \<and>* ps u \<and>* reps u v ks \<and>* tm (v + 1) x \<rbrace>"

   746 proof(cases "ks")

   747   case Nil

   748   thus ?thesis

   749     by (simp add:sep_conj_cond reps.simps, intro tm.pre_condI, simp, hsteps)

   750 next

   751   case (Cons k ks')

   752   thus ?thesis

   753   proof(cases "ks' = []")

   754     case True with Cons

   755     show ?thesis

   756       apply(simp add:sep_conj_cond reps.simps, intro tm.pre_condI, simp add:ones_simps)

   757       by (hgoto hoare_jmp[where p = u])

   758   next

   759     case False

   760     show ?thesis

   761       apply (unfold `ks = k#ks'` reps_simp3[OF False], simp add:ones_simps)

   762       by (hgoto hoare_jmp[where p = u])

   763   qed

   764 qed

   765 

   766 lemma tm_hoare_goto_pre: (* ccc *)

   767   assumes "(<True>) sr"

   768   shows "\<lbrace> fam_conj sr (recse_map ks) \<and>*

   769            st i \<and>* ps 2 \<and>* zero 0 \<and>* zero 1 \<and>* reps 2 ia ks \<and>* fam_conj {ia<..} zero \<rbrace>

   770              i:[(Goto e)]:j

   771          \<lbrace> fam_conj {} (recse_map ks) \<and>*

   772            st e \<and>* ps 2 \<and>* zero 0 \<and>* zero 1 \<and>* reps 2 ia ks \<and>* fam_conj {ia<..} zero \<rbrace>"

   773   apply (unfold Goto_def)

   774   apply (subst (1 2) fam_conj_interv_simp)

   775   apply (unfold zero_def)

   776   apply (hstep hoare_jmp_reps2)

   777   apply (simp add:sep_conj_ac)

   778   my_block

   779     from assms have "sr = {}"

   780       by (simp add:pasrt_def set_ins_def)

   781   my_block_end

   782   by (unfold this, sep_cancel+)

   783   

   784 lemma hoare_goto_pre: 

   785   "IA. \<lbrace> pc i \<and>* <True> \<rbrace> 

   786         i:[ (Goto e) ]:j   

   787        \<lbrace> pc e \<and>* <True> \<rbrace>"

   788   (is "IA. \<lbrace> pc i ** ?P \<rbrace> 

   789               i:[ ?code ?e]:j   

   790            \<lbrace> pc ?e ** ?Q\<rbrace>")

   791 proof(induct rule:tm.IHoareI)

   792   case (IPre s' s r cnf)

   793   let ?cnf = "(trset_of cnf)"

   794   from IPre

   795   have h: "(pc i \<and>* ?P) s" "(s ## s')" "(IA (s + s') \<and>* i :[ ?code(?e) ]: j \<and>* r) ?cnf"

   796     by (metis condD)+

   797   from h(1) obtain sr where

   798       eq_s: "s = {At i} \<union>  sr" "{At i} ##  sr" "?P sr"

   799     by (auto dest!:sep_conjD simp:set_ins_def pc_def sg_def pasrt_def)

   800   hence "At i \<in> s" by auto

   801   from h(3) obtain s1 s2 s3

   802     where hh: "?cnf = s1 + s2 + s3"

   803               "s1 ## s2 \<and> s2 ## s3 \<and> s1 ## s3" 

   804               "IA (s + s') s1" 

   805               "(i :[ ?code ?e ]: j) s2"

   806               "r s3"

   807     apply (auto elim!:sep_conjE intro!:sep_conjI simp:sep_conj_ac)

   808     by (metis sep_add_commute sep_disj_addD1 sep_disj_addD2 sep_disj_commuteI)

   809   interpret ia_disj: IA_disjoint s s' s1 cnf

   810   proof

   811     from `IA (s + s') s1` show "IA (s + s') s1" .

   812   next

   813     from `s ## s'` show "s ## s'" .

   814   next

   815     from hh(1) show "s1 \<subseteq> ?cnf" by (auto simp:set_ins_def)

   816   qed

   817   from hh(1) have s1_belong: "s1 \<subseteq> ?cnf" by (auto simp:set_ins_def)

   818   from hh(3)

   819   have "(EXS ks ia.

   820          ps 2 \<and>*

   821          zero 0 \<and>*

   822          zero 1 \<and>*

   823          reps 2 ia ks \<and>*

   824          fam_conj {ia<..} zero \<and>*

   825          (st i \<and>* fam_conj sr (recse_map ks)) \<and>* fam_conj s' (recse_map ks))

   826         s1"

   827     apply (unfold IA_def fam_conj_disj_simp[OF h(2)])

   828     apply (unfold eq_s)

   829     by (insert eq_s(2), simp add: fam_conj_disj_simp[OF eq_s(2)] fam_conj_simps set_ins_def)

   830   then obtain ks ia

   831     where "((fam_conj sr (recse_map ks) \<and>* st i \<and>* ps 2 \<and>* zero 0 \<and>* zero 1 \<and>*

   832              reps 2 ia ks \<and>* fam_conj {ia<..} zero) \<and>* fam_conj s' (recse_map ks)) s1" 

   833     (is "(?PP \<and>* ?QQ) s1")

   834     by (unfold pred_ex_def, auto simp:sep_conj_ac)

   835   then obtain ss1 ss2 where pres:

   836         "s1 = ss1 + ss2" "ss1 ## ss2"

   837         "?PP ss1"

   838         "?QQ ss2"

   839     by (auto elim!:sep_conjE intro!:sep_conjI)

   840   from ia_disj.at_disj1 [OF `At i \<in> s`]

   841   have at_fresh_s': "At ?e \<notin>  s'" .

   842   have at_fresh_sr: "At ?e \<notin> sr"

   843   proof

   844     assume at_in: "At ?e \<in> sr"

   845     from h(3)[unfolded IA_def fam_conj_disj_simp[OF h(2)]]

   846     have "TAt ?e \<in> trset_of cnf"

   847       apply (elim EXS_elim1)

   848       apply (unfold eq_s fam_conj_disj_simp[OF eq_s(2), unfolded set_ins_def]

   849              fam_conj_elm_simp[OF at_in])

   850       apply (erule_tac sep_conjE, unfold set_ins_def)+

   851       by (auto simp:sep_conj_ac fam_conj_simps st_def sg_def tpn_set_def)

   852     moreover from pres(1, 3) hh(1) have "TAt i \<in> trset_of cnf" 

   853       apply(erule_tac sep_conjE)

   854       apply(erule_tac sep_conjE)

   855       by (auto simp:st_def tpc_set_def sg_def set_ins_def)

   856     ultimately have "i = ?e"

   857       by (cases cnf, auto simp:tpn_set_def trset_of.simps)

   858     from eq_s[unfolded this] at_in

   859     show "False" by (auto simp:set_ins_def)

   860   qed

   861   from pres(3) and hh(2, 4, 5) pres(2, 4)

   862   have pres1: "(?PP \<and>* i :[ ?code(?e)]: j \<and>*  (r \<and>* (fam_conj s' (recse_map ks))))

   863          (trset_of cnf)"

   864     apply (unfold hh(1) pres(1))

   865     apply (rule sep_conjI[where x=ss1 and y = "ss2 + s2 + s3"], assumption+)

   866     apply (rule sep_conjI[where x="s2" and y = "ss2 + s3"], assumption+)

   867     apply (rule sep_conjI[where x="s3" and y = ss2], assumption+)

   868     by (auto simp:set_ins_def)

   869   (*****************************************************************************)

   870   let ?ks_f = "\<lambda> sr ks. ks"

   871   let ?elm_f = "\<lambda> sr. {}"

   872   let ?idx_f = "\<lambda> sr ks ia. ia"

   873   (*----------------------------------------------------------------------------*)

   874   (******************************************************************************)

   875   from tm_hoare_goto_pre[OF `?P sr`, unfolded tm.Hoare_gen_def, rule_format, OF pres1]

   876   obtain k where "((fam_conj (?elm_f sr) (recse_map (?ks_f sr ks)) \<and>*

   877         st ?e \<and>*

   878         ps 2 \<and>*

   879         zero 0 \<and>* zero 1 \<and>* reps 2 (?idx_f sr ks ia) (?ks_f sr ks) \<and>* 

   880         fam_conj {?idx_f sr ks ia<..} zero) \<and>*

   881        i :[ ?code ?e ]: j \<and>* r \<and>* fam_conj s' (recse_map ks))

   882        (trset_of (sep_exec.run tstep (Suc k) cnf))" by blast

   883   (*----------------------------------------------------------------------------*)

   884   moreover have "(pc ?e \<and>* ?Q) ({At ?e} \<union> ?elm_f sr)"

   885   proof -

   886     have "pc ?e {At ?e}" by (simp add:pc_def sg_def)

   887   (******************************************************************************)

   888     moreover have "?Q (?elm_f sr)" 

   889      by (simp add:pasrt_def set_ins_def)

   890   (*----------------------------------------------------------------------------*)

   891     moreover 

   892   (******************************************************************************)

   893     have "{At ?e} ## ?elm_f sr" by (simp add:set_ins_def)

   894   (*----------------------------------------------------------------------------*)

   895     ultimately show ?thesis by (auto intro!:sep_conjI simp:set_ins_def)

   896   qed

   897   moreover 

   898   (******************************************************************************)

   899   from ia_disj.m_disj1 `?P sr` `s = {At i} \<union> sr` 

   900   have "?elm_f sr ## s'" by (auto simp:set_ins_def mm_def sg_def)

   901   (*----------------------------------------------------------------------------*)

   902   with at_fresh_s' 

   903   have fresh_atm: "{At ?e} \<union> ?elm_f sr ## s'" by (auto simp:set_ins_def)

   904   moreover have eq_map: "\<And> elm. elm \<in> s' \<Longrightarrow> 

   905                            (recse_map ks elm) = (recse_map (?ks_f sr ks) elm)"

   906   proof -

   907     fix elm

   908     assume elm_in: "elm \<in> s'"

   909     show "(recse_map ks elm) = (recse_map (?ks_f sr ks) elm)" 

   910       by simp

   911   qed

   912   ultimately show ?case 

   913     apply (rule_tac x = k in exI, rule_tac x = "{At ?e} \<union> ?elm_f sr" in exI)

   914     apply (unfold IA_def, intro condI, assumption+)

   915     apply (rule_tac x = "?ks_f sr ks" in pred_exI)

   916     apply (rule_tac x = "?idx_f sr ks ia" in pred_exI)

   917     apply (unfold fam_conj_disj_simp[OF fresh_atm])

   918     by (auto simp:sep_conj_ac fam_conj_simps)

   919 qed

   920 

   921 lemma hoare_goto[step]: "IA. \<lbrace> pc i \<rbrace> 

   922                           i:[ (Goto e) ]:j   

   923                        \<lbrace> pc e \<rbrace>"

   924 proof(rule tm.I_hoare_adjust [OF hoare_goto_pre])

   925   fix s assume "pc i s" thus "(pc i \<and>* <True>) s"

   926     by (metis cond_true_eq2)

   927 next

   928   fix s assume "(pc e \<and>* <True>) s" thus "pc e s"

   929     by (metis cond_true_eq2)

   930 qed

   931 

   932 lemma I_hoare_sequence: 

   933   assumes h1: "\<And> i j. I. \<lbrace>pc i ** p\<rbrace> i:[c1]:j \<lbrace>pc j ** q\<rbrace>"

   934   and h2: "\<And> j k. I. \<lbrace>pc j ** q\<rbrace> j:[c2]:k \<lbrace>pc k ** r\<rbrace>"

   935   shows "I. \<lbrace>pc i ** p\<rbrace> i:[(c1 ; c2)]:k \<lbrace>pc k ** r\<rbrace>"

   936 proof(unfold tassemble_to.simps, intro tm.I_code_exI)

   937   fix j'

   938   show "I.\<lbrace>pc i \<and>* p\<rbrace>  i :[ c1 ]: j' \<and>* j' :[ c2 ]: k \<lbrace>pc k \<and>* r\<rbrace>"

   939   proof(rule tm.I_sequencing)

   940     from tm.I_code_extension[OF h1 [of i j'], of" j' :[ c2 ]: k"]

   941     show "I.\<lbrace>pc i \<and>* p\<rbrace>  i :[ c1 ]: j' \<and>* j' :[ c2 ]: k \<lbrace>pc j' \<and>* q\<rbrace>" .

   942   next

   943     from tm.I_code_extension[OF h2 [of j' k], of" i :[ c1 ]: j'"]

   944     show "I.\<lbrace>pc j' \<and>* q\<rbrace>  i :[ c1 ]: j' \<and>* j' :[ c2 ]: k \<lbrace>pc k \<and>* r\<rbrace>"

   945       by (auto simp:sep_conj_ac)

   946   qed

   947 qed

   948 

   949 lemma I_hoare_seq1:

   950   assumes h1: "\<And>j'. I. \<lbrace>pc i ** p\<rbrace> i:[c1]:j' \<lbrace>pc j' ** q\<rbrace>"

   951   and h2: "\<And>j' . I. \<lbrace>pc j' ** q\<rbrace> j':[c2]:k \<lbrace>pc k' ** r\<rbrace>"

   952   shows "I. \<lbrace>pc i ** p\<rbrace> i:[(c1 ; c2)]:k \<lbrace>pc k' ** r\<rbrace>"

   953 proof(unfold tassemble_to.simps, intro tm.I_code_exI)

   954   fix j'

   955   show "I.\<lbrace>pc i \<and>* p\<rbrace>  i :[ c1 ]: j' \<and>* j' :[ c2 ]: k \<lbrace>pc k' \<and>* r\<rbrace>"

   956   proof(rule tm.I_sequencing)

   957     from tm.I_code_extension[OF h1 [of j'], of "j' :[ c2 ]: k "]

   958     show "I.\<lbrace>pc i \<and>* p\<rbrace>  i :[ c1 ]: j' \<and>* j' :[ c2 ]: k \<lbrace>pc j' \<and>* q\<rbrace>" .

   959   next

   960     from tm.I_code_extension[OF h2 [of j'], of" i :[ c1 ]: j'"]

   961     show "I.\<lbrace>pc j' \<and>* q\<rbrace>  i :[ c1 ]: j' \<and>* j' :[ c2 ]: k \<lbrace>pc k' \<and>* r\<rbrace>"

   962       by (auto simp:sep_conj_ac)

   963   qed

   964 qed

   965 

   966 lemma t_hoare_local1: 

   967   "(\<And>l. \<lbrace>p\<rbrace>  i :[ c l ]: j \<lbrace>q\<rbrace>) \<Longrightarrow>

   968     \<lbrace>p\<rbrace> i:[TLocal c]:j \<lbrace>q\<rbrace>"

   969 by (unfold tassemble_to.simps, rule tm.code_exI, auto)

   970 

   971 lemma I_hoare_local:

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

   973   shows "I. \<lbrace>pc i ** p\<rbrace> i:[TLocal c]:j \<lbrace>pc k ** q\<rbrace>"

   974 proof(unfold tassemble_to.simps, rule tm.I_code_exI)

   975   fix l

   976   from h[of l]

   977   show " I.\<lbrace>pc i \<and>* p\<rbrace>  i :[ c l ]: j \<lbrace>pc k \<and>* q\<rbrace>" .

   978 qed

   979 

   980 lemma t_hoare_label1: 

   981       "(\<And>l. l = i \<Longrightarrow> \<lbrace>p\<rbrace>  l :[ c l ]: j \<lbrace>q\<rbrace>) \<Longrightarrow>

   982              \<lbrace>p \<rbrace> 

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

   984              \<lbrace>q\<rbrace>"

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

   986 

   987 lemma I_hoare_label: 

   988   assumes h:"\<And>l. l = i \<Longrightarrow> I. \<lbrace>pc l \<and>* p\<rbrace>  l :[ c l ]: j \<lbrace>pc k \<and>* q\<rbrace>"

   989   shows "I. \<lbrace>pc i \<and>* p \<rbrace> 

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

   991              \<lbrace>pc k \<and>* q\<rbrace>"

   992 proof(unfold tm.IHoare_def, default)

   993   fix s'

   994   show " \<lbrace>EXS s. <(pc i \<and>* p) s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>  i :[ (TLabel l ; c l) ]: j

   995          \<lbrace>EXS s. <(pc k \<and>* q) s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>"

   996   proof(rule t_hoare_label1)

   997     fix l assume "l = i"

   998     from h[OF this, unfolded tm.IHoare_def]

   999     show "\<lbrace>EXS s. <(pc i \<and>* p) s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>  l :[ c l ]: j

  1000           \<lbrace>EXS s. <(pc k \<and>* q) s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>" 

  1001       by (simp add:`l = i`)

  1002   qed

  1003 qed

  1004 

  1005 lemma I_hoare_label_last: 

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

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

  1008   shows "I. \<lbrace>p\<rbrace> i:[c]:j \<lbrace>q\<rbrace>"

  1009 proof(unfold tm.IHoare_def, default)

  1010   fix s'

  1011   show "\<lbrace>EXS s. <p s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>  i :[ c ]: j 

  1012         \<lbrace>EXS s. <q s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>"

  1013   proof(rule t_hoare_label_last[OF h1])

  1014     assume "l = j"

  1015     from h2[OF this, unfolded tm.IHoare_def]

  1016     show "\<lbrace>EXS s. <p s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>  i :[ t_blast_cmd c ]: j

  1017           \<lbrace>EXS s. <q s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>"

  1018       by fast

  1019   qed

  1020 qed

  1021 

  1022 lemma I_hoare_seq2:

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

  1024  shows "I. \<lbrace>pc i ** p\<rbrace> i:[(c1 ; c2)]:j \<lbrace>pc k' ** r\<rbrace>"

  1025   apply (unfold tassemble_to.simps, intro tm.I_code_exI)

  1026   apply (unfold tm.IHoare_def, default)

  1027   apply (rule tm.code_extension)

  1028   by (rule h[unfolded tm.IHoare_def, rule_format])

  1029 

  1030 lemma IA_pre_stren:

  1031   assumes h1: "IA. \<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"

  1032   and h2:  "\<And>s. r s \<Longrightarrow> p s"

  1033   shows "IA. \<lbrace>r\<rbrace> c \<lbrace>q\<rbrace>"

  1034   by (rule tm.I_pre_stren[OF assms], simp)

  1035 

  1036 lemma IA_post_weaken: 

  1037   assumes h1: "IA. \<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"

  1038     and h2: "\<And> s. q s \<Longrightarrow> r s"

  1039   shows "IA. \<lbrace>p\<rbrace> c \<lbrace>r\<rbrace>"

  1040   by (rule tm.I_post_weaken[OF assms], simp)

  1041 

  1042 section {* Making triple processor for IA *}

  1043 

  1044 ML {* (* Functions specific to Hoare triple: IA {P} c {Q} *)

  1045   fun get_pre ctxt t = 

  1046     let val pat = term_of @{cpat "IA. \<lbrace>?P\<rbrace> ?c \<lbrace>?Q\<rbrace>"} 

  1047         val env = match ctxt pat t 

  1048     in inst env (term_of @{cpat "?P::aresource set \<Rightarrow> bool"}) end

  1049 

  1050   fun can_process ctxt t = ((get_pre ctxt t; true) handle _ => false)

  1051 

  1052   fun get_post ctxt t = 

  1053     let val pat = term_of @{cpat "IA. \<lbrace>?P\<rbrace> ?c \<lbrace>?Q\<rbrace>"} 

  1054         val env = match ctxt pat t 

  1055     in inst env (term_of @{cpat "?Q::aresource set \<Rightarrow> bool"}) end;

  1056 

  1057   fun get_mid ctxt t = 

  1058     let val pat = term_of @{cpat "IA. \<lbrace>?P\<rbrace> ?c \<lbrace>?Q\<rbrace>"} 

  1059         val env = match ctxt pat t 

  1060     in inst env (term_of @{cpat "?c::tresource set \<Rightarrow> bool"}) end;

  1061 

  1062   fun is_pc_term (Const (@{const_name pc}, _) $ _) = true

  1063     | is_pc_term _ = false

  1064 

  1065   fun mk_pc_term x =

  1066      Const (@{const_name pc}, @{typ "nat \<Rightarrow> aresource set \<Rightarrow> bool"}) $ Free (x, @{typ "nat"})

  1067 

  1068   val sconj_term = term_of @{cterm "sep_conj::assert \<Rightarrow> assert \<Rightarrow> assert"}

  1069 

  1070   val abc_triple = {binding = @{binding "abc_triple"}, 

  1071                    can_process = can_process,

  1072                    get_pre = get_pre,

  1073                    get_mid = get_mid,

  1074                    get_post = get_post,

  1075                    is_pc_term = is_pc_term,

  1076                    mk_pc_term = mk_pc_term,

  1077                    sconj_term = sconj_term,

  1078                    sep_conj_ac_tac = sep_conj_ac_tac,

  1079                    hoare_seq1 = @{thm I_hoare_seq1},

  1080                    hoare_seq2 = @{thm I_hoare_seq2},

  1081                    pre_stren = @{thm IA_pre_stren},

  1082                    post_weaken = @{thm IA_post_weaken},

  1083                    frame_rule = @{thm tm.I_frame_rule}

  1084                   }:HoareTriple

  1085 

  1086   val _ = (HoareTriples_get ()) |> (fn orig => HoareTriples_store (abc_triple::orig))

  1087 *}

  1088 

  1089 section {* Example proofs *}

  1090 

  1091 definition "clear a = (TL start exit. TLabel start; Dec a exit; Goto start; TLabel exit)"

  1092 

  1093 lemma hoare_clear[step]: 

  1094   "IA. \<lbrace>pc i ** mm a v\<rbrace> 

  1095          i:[clear a]:j 

  1096        \<lbrace>pc j ** mm a 0\<rbrace>"

  1097 proof(unfold clear_def, intro I_hoare_local I_hoare_label, simp,

  1098       rule I_hoare_label_last, simp+, prune)

  1099   show "IA.\<lbrace>pc i \<and>* mm a v\<rbrace>  i :[ (Dec a j ; Goto i) ]: j \<lbrace>pc j \<and>* mm a 0\<rbrace>"

  1100   proof(induct v)

  1101     case 0

  1102     show ?case

  1103       by hgoto

  1104   next

  1105     case (Suc v)

  1106     show ?case

  1107       apply (rule_tac Q = "pc i \<and>* mm a v" in tm.I_sequencing)

  1108       by hsteps

  1109   qed

  1110 qed

  1111 

  1112 definition "dup a b c = 

  1113        (TL start exit. TLabel start; Dec a exit; Inc b; Inc c; Goto start; TLabel exit)"

  1114 

  1115 lemma hoare_dup[step]: 

  1116         "IA. \<lbrace>pc i ** mm a va ** mm b vb ** mm c vc \<rbrace> 

  1117                   i:[dup a b c]:j 

  1118              \<lbrace>pc j ** mm a 0 ** mm b (va + vb) ** mm c (va + vc)\<rbrace>"

  1119 proof(unfold dup_def, intro I_hoare_local I_hoare_label, clarsimp,

  1120      rule I_hoare_label_last, simp+, prune)

  1121   show "IA. \<lbrace>pc i \<and>* mm a va \<and>* mm b vb \<and>* mm c vc\<rbrace>  

  1122                i :[ (Dec a j ; Inc b ; Inc c ; Goto i) ]: j

  1123             \<lbrace>pc j \<and>* mm a 0 \<and>* mm b (va + vb) \<and>* mm c (va + vc)\<rbrace>"

  1124   proof(induct va arbitrary: vb vc)

  1125     case (0 vb vc)

  1126     show ?case

  1127       by hgoto

  1128   next

  1129     case (Suc va vb vc)

  1130     show ?case

  1131       apply (rule_tac Q = "pc i \<and>* mm a va \<and>* mm b (Suc vb) \<and>* mm c (Suc vc)" in tm.I_sequencing)

  1132       by (hsteps Suc)

  1133   qed

  1134 qed

  1135