header {* 

  Separation logic for TM

*}

theory Hoare_tm_basis

imports Hoare_gen My_block Data_slot MLs Term_pat (* BaseSS *) Subgoal Sort_ops

        Thm_inst

begin

section {* Aux lemmas on seperation algebra *}

lemma cond_eq: "((<b> \<and>* p) s) = (b \<and> (p s))"

proof

  assume "(<b> \<and>* p) s"

  from condD[OF this] show " b \<and> p s" .

next

  assume "b \<and> p s"

  hence b and "p s" by auto

  from `b` have "(<b>) 0" by (auto simp:pasrt_def)

  moreover have "s = 0 + s" by auto

  moreover have "0 ## s" by auto

  moreover note `p s`

  ultimately show "(<b> \<and>* p) s" by (auto intro!:sep_conjI)

qed

lemma cond_eqI:

  assumes h: "b \<Longrightarrow> r = s"

  shows "(<b> ** r) = (<b> ** s)"

proof(cases b)

  case True

  from h[OF this] show ?thesis by simp

next

  case False

  thus ?thesis

    by (unfold sep_conj_def set_ins_def pasrt_def, auto)

qed

lemma EXS_intro: 

  assumes h: "(P x) s"

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

  by (smt h pred_ex_def sep_conj_impl)

lemma EXS_elim: 

  assumes "(EXS x. P x) s"

  obtains x where "P x s"

  by (metis assms pred_ex_def)

lemma EXS_eq:

  fixes x

  assumes h: "Q (p x)" 

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

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

proof

  fix s

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

  proof

    assume "p x s"

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

  next

    assume "(EXS x. p x) s"

    thus "p x s"

    proof(rule EXS_elim)

      fix y

      assume "p y s"

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

    qed

  qed

qed

section {* The TM assembly language *}

subsection {* The TM assembly language *}

datatype taction = W0 | W1 | L | R

datatype tstate = St nat

fun nat_of :: "tstate \<Rightarrow> nat"

where "nat_of (St n) = n"

declare [[coercion_enabled]]

declare [[coercion "St :: nat \<Rightarrow> tstate"]]

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

datatype Block = Oc | Bk

datatype tpg = 

   TInstr tm_inst

 | TLabel tstate

 | TSeq tpg tpg

 | TLocal "(tstate \<Rightarrow> tpg)"

notation TLocal (binder "TL " 10)

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

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

abbreviation tprog_seq :: "tpg \<Rightarrow> tpg \<Rightarrow> tpg" (infixr ";" 52)

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

subsection {* The notion of assembling *}

datatype tresource = 

    TM int Block

  | TC nat tm_inst

  | TAt nat

  | TPos int

  | TFaults nat

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

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

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

  where 

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

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

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

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

declare tassemble_to.simps [simp del]

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

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

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

section {* Automatic checking of assemblility *}

subsection {* Basic theories *}

text {* @{text cpg} is the type for skeleton assembly language. Every constructor

        corresponds to one in the definition of @{text tpg} *}

datatype cpg = 

   CInstr tm_inst

 | CLabel nat

 | CSeq cpg cpg

 | CLocal cpg

text {* Conversion from @{text cpg} to @{text tpg}*}

fun c2t :: "tstate list \<Rightarrow> cpg \<Rightarrow> tpg" where 

  "c2t env (CInstr ((act0, St st0), (act1, St st1))) = 

                         TInstr ((act0, env!st0), (act1, env!st1))" |

  "c2t env (CLabel l) = TLabel (env!l)" |

  "c2t env (CSeq cpg1 cpg2) = TSeq (c2t env cpg1) (c2t env cpg2)" |

  "c2t env (CLocal cpg) = TLocal (\<lambda> x. c2t (x#env) cpg)"

text {* Well formedness checking of @{text cpg} *}

datatype status = Free | Bound

text {* @{text wf_cpg_test} is the checking function *}

fun  wf_cpg_test :: "status list \<Rightarrow> cpg \<Rightarrow> (bool \<times> status list)" where

  "wf_cpg_test sts (CInstr ((a0, l0), (a1, l1))) = ((l0 < length sts \<and> l1 < length sts), sts)" |

  "wf_cpg_test sts (CLabel l) = ((l < length sts) \<and> sts!l = Free, sts[l:=Bound])" |

  "wf_cpg_test sts (CSeq c1 c2) = (let (b1, sts1) = wf_cpg_test sts c1;

                                  (b2, sts2) = wf_cpg_test sts1 c2 in

                                     (b1 \<and> b2, sts2))" |

  "wf_cpg_test sts (CLocal body) = (let (b, sts') = (wf_cpg_test (Free#sts) body) in 

                                   (b, tl sts'))"

text {*

  The meaning the following @{text "c2p"} has to be understood together with 

  the following lemma @{text "wf_cpg_test_correct"}. The intended use of @{text "c2p"}

  is when the elements of @{text "sts"} are all @{text "Free"}, in which case, 

  the precondition on @{text "f"}, i.e. 

       @{text "\<forall> x. ((length x = length sts \<and> 

                                    (\<forall> k < length sts. sts!k = Bound \<longrightarrow> (x!k = f i k))"}

  is trivially true. 

*}

definition 

   "c2p sts i cpg j = 

           (\<exists> f. \<forall> x. ((length x = length sts \<and> 

                        (\<forall> k < length sts. sts!k = Bound \<longrightarrow> (x!k = f i k)))

                   \<longrightarrow> (\<exists> s. (i:[(c2t x cpg)]:j) s)))"

instantiation status :: order

begin

  definition less_eq_status_def: "((st1::status) \<le> st2) = (st1 = Free \<or> st2 = Bound)"

  definition less_status_def: "((st1::status) < st2) = (st1 \<le> st2 \<and> st1 \<noteq> st2)"

instance

proof

  fix x y 

  show "(x < (y::status)) = (x \<le> y \<and> \<not> y \<le> x)"

    by (metis less_eq_status_def less_status_def status.distinct(1))

next

  fix x show "x \<le> (x::status)"

    by (metis (full_types) less_eq_status_def status.exhaust)

next

  fix x y z

  assume "x \<le> y" "y \<le> (z::status)" show "x \<le> (z::status)"

    by (metis `x \<le> y` `y \<le> z` less_eq_status_def status.distinct(1))

next

  fix x y

  assume "x \<le> y" "y \<le> (x::status)" show "x = y"

    by (metis `x \<le> y` `y \<le> x` less_eq_status_def status.distinct(1))

qed

end

instantiation list :: (order)order

begin

  definition "((sts::('a::order) list)  \<le> sts') = 

                   ((length sts = length sts') \<and> (\<forall> i < length sts. sts!i \<le> sts'!i))"

  definition "((sts::('a::order) list)  < sts') = ((sts \<le> sts') \<and> sts \<noteq> sts')"

  lemma anti_sym: assumes h: "x \<le> (y::'a list)" "y \<le> x"

      shows "x = y"

  proof -

    from h have "length x = length y"

      by (metis less_eq_list_def)

    moreover from h have " (\<forall> i < length x. x!i = y!i)"

      by (metis (full_types) antisym_conv less_eq_list_def)

    ultimately show ?thesis

      by (metis nth_equalityI)

  qed

  lemma refl: "x \<le> (x::('a::order) list)"

    apply (unfold less_eq_list_def)

    by (metis order_refl)

  instance

  proof

    fix x y

    show "((x::('a::order) list) < y) = (x \<le> y \<and> \<not> y \<le> x)"

    proof

      assume h: "x \<le> y \<and> \<not> y \<le> x"

      have "x \<noteq> y"

      proof

        assume "x = y" with h have "\<not> (x \<le> x)" by simp

        with refl show False by auto

      qed

      moreover from h have "x \<le> y" by blast

      ultimately show "x < y" by (auto simp:less_list_def)

    next

      assume h: "x < y"

      hence hh: "x \<le> y"

        by (metis less_list_def)

      moreover have "\<not> y \<le> x"

      proof

        assume "y \<le> x"

        from anti_sym[OF hh this] have "x = y" .

        with h show False

          by (metis less_list_def) 

      qed

      ultimately show "x \<le> y \<and> \<not> y \<le> x" by auto

    qed

  next

    fix x from refl show "(x::'a list) \<le> x" .

  next

    fix x y assume "(x::'a list) \<le> y" "y \<le> x" 

    from anti_sym[OF this] show "x = y" .

  next

    fix x y z

    assume h: "(x::'a list) \<le> y" "y \<le> z"

    show "x \<le> z"

    proof -

      from h have "length x = length z" by (metis less_eq_list_def)

      moreover from h have "\<forall> i < length x. x!i \<le> z!i"

        by (metis less_eq_list_def order_trans)

      ultimately show "x \<le> z"

        by (metis less_eq_list_def)

    qed

  qed

end

lemma sts_bound_le: "sts \<le> sts[l := Bound]"

proof -

  have "length sts = length (sts[l := Bound])"

    by (metis length_list_update)

  moreover have "\<forall> i < length sts. sts!i \<le> (sts[l:=Bound])!i"

  proof -

    { fix i

      assume "i < length sts"

      have "sts ! i \<le> sts[l := Bound] ! i"

      proof(cases "l < length sts")

        case True

        note le_l = this

        show ?thesis

        proof(cases "l = i")

          case True with le_l

          have "sts[l := Bound] ! i = Bound" by auto

          thus ?thesis by (metis less_eq_status_def) 

        next

          case False

          with le_l have "sts[l := Bound] ! i = sts!i" by auto

          thus ?thesis by auto

        qed

      next

        case False

        hence "sts[l := Bound] = sts" by auto

        thus ?thesis by auto

      qed

    } thus ?thesis by auto

  qed

  ultimately show ?thesis by (metis less_eq_list_def) 

qed

lemma sts_tl_le:

  assumes "sts \<le> sts'"

  shows "tl sts \<le> tl sts'"

proof -

  from assms have "length (tl sts) = length (tl sts')"

    by (metis (hide_lams, no_types) length_tl less_eq_list_def)

  moreover from assms have "\<forall> i < length (tl sts). (tl sts)!i \<le> (tl sts')!i"

    by (smt calculation length_tl less_eq_list_def nth_tl)

  ultimately show ?thesis

    by (metis less_eq_list_def)

qed

lemma wf_cpg_test_le:

  assumes "wf_cpg_test sts cpg = (True, sts')"

  shows "sts \<le> sts'" using assms

proof(induct cpg arbitrary:sts sts')

  case (CInstr instr sts sts')

  obtain a0 l0 a1 l1 where eq_instr: "instr = ((a0, St l0), (a1, St l1))"

    by (metis surj_pair tstate.exhaust)

  from CInstr[unfolded this]

  show ?case by simp

next

  case (CLabel l sts sts')

  thus ?case by (auto simp:sts_bound_le)

next

  case (CLocal body sts sts')

  from this(2)

  obtain sts1 where h: "wf_cpg_test (Free # sts) body = (True, sts1)" "sts' = tl sts1"

    by (auto split:prod.splits)

  from CLocal(1)[OF this(1)] have "Free # sts \<le> sts1" .

  from sts_tl_le[OF this]

  have "sts \<le> tl sts1" by simp

  from this[folded h(2)]

  show ?case .

next

  case (CSeq cpg1 cpg2 sts sts')

  from this(3)

  show ?case

    by (auto split:prod.splits dest!:CSeq(1, 2))

qed

lemma c2p_assert:

  assumes "(c2p [] i cpg j)"

  shows "\<exists> s. (i :[(c2t [] cpg)]: j) s"

proof -

  from assms obtain f where

    h [rule_format]: 

    "\<forall> x. length x = length [] \<and> (\<forall>k<length []. [] ! k = Bound \<longrightarrow> (x ! k = f i k)) \<longrightarrow>

                        (\<exists> s. (i :[ c2t [] cpg ]: j) s)"

    by (unfold c2p_def, auto)

  have "length [] = length [] \<and> (\<forall>k<length []. [] ! k = Bound \<longrightarrow> ([] ! k = f i k))"

    by auto

  from h[OF this] obtain s where "(i :[ c2t [] cpg ]: j) s" by blast

  thus ?thesis by auto

qed

definition "sts_disj sts sts' = ((length sts = length sts') \<and> 

                                 (\<forall> i < length sts. \<not>(sts!i = Bound \<and> sts'!i = Bound)))"

instantiation list :: (plus)plus

begin

   fun plus_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where

     "plus_list [] ys = []" |

     "plus_list (x#xs) [] = []" |

     "plus_list (x#xs) (y#ys) = ((x + y)#plus_list xs ys)"

   instance ..

end

instantiation list :: (minus)minus

begin

   fun minus_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where

     "minus_list [] ys = []" |

     "minus_list (x#xs) [] = []" |

     "minus_list (x#xs) (y#ys) = ((x - y)#minus_list xs ys)"

   instance ..

end

instantiation status :: minus

begin

   fun minus_status :: "status \<Rightarrow> status \<Rightarrow> status" where

     "minus_status Bound Bound = Free" |

     "minus_status Bound Free = Bound" |

     "minus_status Free x = Free "

   instance ..

end

instantiation status :: plus

begin

   fun plus_status :: "status \<Rightarrow> status \<Rightarrow> status" where

     "plus_status Free x = x" |

     "plus_status Bound x = Bound"

   instance ..

end

lemma length_sts_plus:

  assumes "length (sts1 :: status list) = length sts2"

  shows "length (sts1 + sts2) = length sts1"

  using assms

proof(induct sts1 arbitrary: sts2)

  case Nil

  thus ?case

    by (metis plus_list.simps(1))

next

  case (Cons s' sts' sts2)

  thus ?case

  proof(cases "sts2 = []")

    case True

    with Cons show ?thesis by auto

  next

    case False

    then obtain s'' sts'' where eq_sts2: "sts2 = s''#sts''"

      by (metis neq_Nil_conv)

    with Cons

    show ?thesis

      by (metis length_Suc_conv list.inject plus_list.simps(3))

  qed

qed

lemma nth_sts_plus:

  assumes "i < length ((sts1::status list) + sts2)"

  shows "(sts1 + sts2)!i = sts1!i + sts2!i"

  using assms

proof(induct sts1 arbitrary:i sts2)

  case (Nil i sts2)

  thus ?case by auto

next

  case (Cons s' sts' i sts2)

  show ?case

  proof(cases "sts2 = []")

    case True

    with Cons show ?thesis by auto

  next

    case False

    then obtain s'' sts'' where eq_sts2: "sts2 = s''#sts''"

      by (metis neq_Nil_conv)

    with Cons

    show ?thesis

      by (smt list.size(4) nth_Cons' plus_list.simps(3))

  qed

qed

lemma nth_sts_minus:

  assumes "i < length ((sts1::status list) - sts2)"

  shows "(sts1 - sts2)!i = sts1!i - sts2!i"

  using assms

proof(induct  arbitrary:i rule:minus_list.induct)

  case (3 x xs y ys i)

  show ?case

  proof(cases i)

    case 0

    thus ?thesis by simp

  next

    case (Suc k)

    with 3(2) have "k < length (xs - ys)" by auto

    from 3(1)[OF this] and Suc

    show ?thesis

      by auto

  qed

qed auto

fun taddr :: "tresource \<Rightarrow> nat" where

   "taddr (TC i instr) = i"

lemma tassemble_to_range:

  assumes "(i :[tpg]: j) s"

  shows "(i \<le> j) \<and> (\<forall> r \<in> s. i \<le> taddr r \<and> taddr r < j)"

  using assms

proof(induct tpg arbitrary: i j s)

  case (TInstr instr i j s)

  obtain a0 l0 a1 l1 where "instr = ((a0, l0), (a1, l1))"

    by (metis pair_collapse)

  with TInstr

  show ?case

    apply (simp add:tassemble_to.simps sg_def)

    by (smt `instr = ((a0, l0), a1, l1)` cond_eq cond_true_eq1 

        empty_iff insert_iff le_refl lessI sep.mult_commute taddr.simps)

next

  case (TLabel l i j s)

  thus ?case

    apply (simp add:tassemble_to.simps)

    by (smt equals0D pasrt_def set_zero_def)

next

  case (TSeq c1 c2 i j s)

  from TSeq(3) obtain s1 s2 j' where 

    h: "(i :[ c1 ]: j') s1" "(j' :[ c2 ]: j) s2" "s1 ## s2" "s = s1 + s2"

    by (auto simp:tassemble_to.simps elim!:EXS_elim sep_conjE)

  show ?case

  proof -

    { fix r 

      assume "r \<in> s"

      with h (3, 4) have "r \<in> s1 \<or> r \<in> s2"

        by (auto simp:set_ins_def)

      hence "i \<le> j \<and> i \<le> taddr r \<and> taddr r < j" 

      proof

        assume " r \<in> s1"

        from TSeq(1)[OF h(1)]

        have "i \<le> j'" "(\<forall>r\<in>s1. i \<le> taddr r \<and> taddr r < j')" by auto

        from this(2)[rule_format, OF `r \<in> s1`]

        have "i \<le> taddr r" "taddr r < j'" by auto

        with TSeq(2)[OF h(2)]

        show ?thesis by auto

      next

        assume "r \<in> s2"

        from TSeq(2)[OF h(2)]

        have "j' \<le> j" "(\<forall>r\<in>s2. j' \<le> taddr r \<and> taddr r < j)" by auto

        from this(2)[rule_format, OF `r \<in> s2`]

        have "j' \<le> taddr r" "taddr r < j" by auto

        with TSeq(1)[OF h(1)]

        show ?thesis by auto

      qed

    } thus ?thesis

      by (smt TSeq.hyps(1) TSeq.hyps(2) h(1) h(2))

  qed

next

  case (TLocal body i j s)

  from this(2) obtain l s' where "(i :[ body l ]: j) s"

    by (simp add:tassemble_to.simps, auto elim!:EXS_elim)

  from TLocal(1)[OF this]

  show ?case by auto

qed

lemma c2p_seq:

  assumes "c2p sts1 i cpg1 j'"

          "c2p sts2 j' cpg2 j"

          "sts_disj sts1 sts2"

  shows "(c2p (sts1 + sts2) i (CSeq cpg1 cpg2) j)" 

proof -