header {* 

 {\em Abacus} defined as macros of TM

 *}

theory Hoare_abc2

imports Hoare_tm2 Finite_Set

begin

text {*

  {\em Abacus} instructions

*}

(*

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

datatype abc_inst =

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

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

     *}

     Inc nat

  -- {*

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

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

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

     *}

   | Dec nat nat

  -- {*

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

  *}

   | Goto nat

*)

datatype aresource = 

    M nat nat

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

  | At nat

  | Faults nat

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

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

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

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

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

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

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

                                fam_conj ars (recse_map ks))"

section {* A virtually defined Abacus *}

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

definition "pc l = sg {At l}"

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

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

lemma tm_hoare_inc1:

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

  shows "

    \<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> 

    i :[Inc a ]: j

    \<lbrace>st j \<and>*

     ps u \<and>*

     zero (u - 2) \<and>*

     zero (u - 1) \<and>*

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

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

  using h

proof

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

  hence "a < length ks" by simp 

  from list_ext_lt [OF this] tm_hoare_inc00[OF hh]

  show ?thesis by simp

next

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

  from tm_hoare_inc01[OF this]

  show ?thesis by simp

qed

lemma tm_hoare_inc2: 

  assumes "mm a v sr"

  shows "

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

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

          i:[ (Inc a) ]:j   

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

           st j \<and>*

           ps 2 \<and>*

           zero 0 \<and>*

           zero 1 \<and>*

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

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

proof -

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

  from tm_hoare_inc1[where u = 2]

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

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

             i :[Inc a ]: j

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

           ps 2 \<and>*

           zero 0 \<and>*

           zero 1 \<and>*

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

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

  thus ?thesis

    apply (unfold eq_sr)

    apply (simp add:fam_conj_simps list_ext_get_upd list_ext_len)

    by (rule tm.pre_condI, blast)

qed

locale IA_disjoint = 

  fixes s s' s1 cnf

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

  and h_disj: "s ## s'"

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

begin

lemma at_disj1: 

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

  shows "At j \<notin> s'"

proof

  from h_IA[unfolded IA_def]

  obtain ks idx

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

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

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

    by (auto elim!:EXS_elim simp:sep_conj_ac)

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

    by (auto elim:sep_conjE)

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

  obtain tt1 tt2

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

            "(fam_conj s (recse_map ks)) tt1"

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

    by (auto elim:sep_conjE)

  assume "At j \<in> s'"

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

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

  have "TAt j \<in> trset_of cnf"

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

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

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

  have "TAt i \<in> trset_of cnf"

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

  ultimately have "i = j"

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

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

  show False 

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

qed

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

  by (metis at_disj1)

lemma m_disj1: 

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

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

proof

  from h_IA[unfolded IA_def]

  obtain ks idx

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

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

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

    by (auto elim!:EXS_elim simp:sep_conj_ac)

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

    by (auto elim:sep_conjE)

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

  obtain tt1 tt2

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

            "(fam_conj s (recse_map ks)) tt1"

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

    by (auto elim:sep_conjE)

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

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

        recse_map.simps]

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

    by (auto simp:pasrt_def)

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

                         recse_map.simps]

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

    by (auto simp:pasrt_def)

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

  ultimately show False

    by (auto simp:set_ins_def)

qed

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

  by (metis m_disj1)

end

lemma EXS_elim1: 

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

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

  by (metis EXS_elim assms sep_conj_exists1)

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

                        i:[ (Inc a) ]:j   

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

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

                        i:[ ?code ?e ]:j   

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

proof(induct rule:tm.IHoareI)

  case (IPre s' s r cnf)

  let ?cnf = "(trset_of cnf)"

  from IPre

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

    by (metis condD)+

  from h(1) obtain sr where

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

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

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

  from h(3) obtain s1 s2 s3

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

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

              "IA (s + s') s1" 

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

              "r s3"

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

    by (metis sep_add_commute sep_disj_addD1 sep_disj_addD2 sep_disj_commuteI)

  interpret ia_disj: IA_disjoint s s' s1 cnf

  proof

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

  next

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

  next

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

  qed

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

  from hh(3)

  have "(EXS ks ia.

         ps 2 \<and>*

         zero 0 \<and>*

         zero 1 \<and>*

         reps 2 ia ks \<and>*

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

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

        s1"

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

    apply (unfold eq_s)

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

  then obtain ks ia

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

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

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

    by (unfold pred_ex_def, auto simp:sep_conj_ac)

  then obtain ss1 ss2 where pres:

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

        "?PP ss1"

        "?QQ ss2"

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

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

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

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

  proof

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

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

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

      apply (elim EXS_elim1)

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

             fam_conj_elm_simp[OF at_in])

      apply (erule_tac sep_conjE, unfold set_ins_def)+

      by (auto simp:sep_conj_ac fam_conj_simps st_def sg_def tpn_set_def)

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

      apply(erule_tac sep_conjE)

      apply(erule_tac sep_conjE)

      by (auto simp:st_def tpc_set_def sg_def set_ins_def)

    ultimately have "i = ?e"

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

    from eq_s[unfolded this] at_in

    show "False" by (auto simp:set_ins_def)

  qed

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

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

         (trset_of cnf)"

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

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

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

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

    by (auto simp:set_ins_def)

  (*****************************************************************************)

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

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

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

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

  (******************************************************************************)

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

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

        st ?e \<and>*

        ps 2 \<and>*

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

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

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

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

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

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

  proof -

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

  (******************************************************************************)

    moreover have "?Q (?elm_f sr)" 

      by (simp add:mm_def sg_def)

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

    moreover 

  (******************************************************************************)

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

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

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

  qed

  moreover 

  (******************************************************************************)

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

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

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

  with at_fresh_s' 

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

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

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

  proof -

    fix elm

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

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

    proof(cases elm)

      (*******************************************************************)

      case (M a' v')

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

      with elm_in ia_disj.m_disj1[OF this] M

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

      thus ?thesis

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

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

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

        by (metis (full_types) bot_nat_def 

              leI le_trans less_Suc_eq_le list_ext_lt_get list_ext_tail set_zero_def)

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

    qed auto

  qed

  ultimately show ?case 

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

    apply (unfold IA_def, intro condI, assumption+)

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

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

    apply (unfold fam_conj_disj_simp[OF fresh_atm])

    apply (auto simp:sep_conj_ac fam_conj_simps)

    (***************************************************************************)

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

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

    apply (sep_cancel)+

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

qed

lemma tm_hoare_dec_fail:

  assumes "mm a 0 sr"

  shows 

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

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

       i:[ (Dec a e) ]:j 

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

     st e \<and>*

     ps 2 \<and>*

     zero 0 \<and>*

     zero 1 \<and>*

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

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

proof - 

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

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

    from tm_hoare_dec_fail1[where u = 2, OF this]

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

                  i :[ Dec a e ]: j

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

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

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

    by (simp)

  }

  thus ?thesis

    apply (unfold eq_sr)

    apply (simp add:fam_conj_simps list_ext_get_upd list_ext_len)

    by (rule tm.pre_condI, blast)

qed

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

                              i:[ (Dec a e) ]:j   

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

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

                                i:[ ?code ?e]:j   

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

proof(induct rule:tm.IHoareI)

  case (IPre s' s r cnf)

  let ?cnf = "(trset_of cnf)"

  from IPre

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

    by (metis condD)+

  from h(1) obtain sr where

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

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

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

  from h(3) obtain s1 s2 s3

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

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

              "IA (s + s') s1" 

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

              "r s3"

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

    by (metis sep_add_commute sep_disj_addD1 sep_disj_addD2 sep_disj_commuteI)

  interpret ia_disj: IA_disjoint s s' s1 cnf

  proof

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

  next

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

  next

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

  qed

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

  from hh(3)

  have "(EXS ks ia.

         ps 2 \<and>*

         zero 0 \<and>*

         zero 1 \<and>*

         reps 2 ia ks \<and>*

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

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

        s1"

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

    apply (unfold eq_s)

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

  then obtain ks ia

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

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

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

    by (unfold pred_ex_def, auto simp:sep_conj_ac)

  then obtain ss1 ss2 where pres:

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

        "?PP ss1"

        "?QQ ss2"

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

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

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

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

  proof

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

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

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

      apply (elim EXS_elim1)

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

             fam_conj_elm_simp[OF at_in])

      apply (erule_tac sep_conjE, unfold set_ins_def)+

      by (auto simp:sep_conj_ac fam_conj_simps st_def sg_def tpn_set_def)

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

      apply(erule_tac sep_conjE)

      apply(erule_tac sep_conjE)

      by (auto simp:st_def tpc_set_def sg_def set_ins_def)

    ultimately have "i = ?e"

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

    from eq_s[unfolded this] at_in

    show "False" by (auto simp:set_ins_def)

  qed

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

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

         (trset_of cnf)"

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

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

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

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

    by (auto simp:set_ins_def)

  (*****************************************************************************)

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

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

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

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

  (******************************************************************************)

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

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

        st ?e \<and>*

        ps 2 \<and>*

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

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

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

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

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

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

  proof -

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

  (******************************************************************************)

    moreover have "?Q (?elm_f sr)" 

      by (simp add:mm_def sg_def)

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

    moreover 

  (******************************************************************************)

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

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

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

  qed

  moreover 

  (******************************************************************************)

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

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

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

  with at_fresh_s' 

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

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

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

  proof -

    fix elm

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

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

    proof(cases elm)

      (*******************************************************************)

      case (M a' v')

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

      with elm_in ia_disj.m_disj1[OF this] M

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

      thus ?thesis

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

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

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

        by (metis (full_types) bot_nat_def 

              leI le_trans less_Suc_eq_le list_ext_lt_get list_ext_tail set_zero_def)

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

    qed auto

  qed

  ultimately show ?case 

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

    apply (unfold IA_def, intro condI, assumption+)