1 header {* 

     2  {\em abacus} a kind of register machine

     3 *}

     4 

     5 theory abacus

     6 imports Main "~~/src/HOL/Algebra/IntRing" 

     7 begin

     8 

     9 text {*

    10   {\em Abacus} instructions:

    11 *}

    12 

    13 datatype abc_inst =

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

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

    16      *}

    17      Inc nat

    18   -- {*

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

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

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

    22      *}

    23    | Dec nat nat

    24   -- {*

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

    26   *}

    27    | Goto nat

    28 

    29 definition "stimes p q = {s . \<exists> u v. u \<in> p \<and> v \<in> q \<and> (u \<union> v = s) \<and> (u \<inter> v = {})}"

    30 

    31 no_notation times (infixl "*" 70)

    32 

    33 notation stimes (infixl "*" 70)

    34 

    35 lemma stimes_comm: "p * q = q * p"

    36   by (unfold stimes_def, auto)

    37 

    38 lemma stimes_assoc: "(p * q) * r = p * (q * r)"

    39   by (unfold stimes_def, blast)

    40 

    41 definition

    42   "emp = {{}}"

    43 

    44 lemma emp_unit_r [simp]: "p * emp = p"

    45   by (unfold stimes_def emp_def, auto)

    46 

    47 lemma emp_unit_l [simp]: "emp * p = p"

    48   by (metis emp_unit_r stimes_comm)

    49 

    50 lemma stimes_mono: "p \<subseteq> q \<Longrightarrow> p * r \<subseteq> q * r"

    51   by (unfold stimes_def, auto)

    52 

    53 thm mult_cancel_left

    54 

    55 lemma stimes_left_commute:

    56   "(p * (q * r)) = (q * (p * r))"

    57 by (metis stimes_assoc stimes_comm)

    58 

    59 lemmas stimes_ac = stimes_comm stimes_assoc stimes_left_commute

    60 

    61 definition pasrt :: "bool \<Rightarrow> ('a set set)" ("<_>" [71] 71)

    62 where "pasrt b = {s . s = {} \<and> b}"

    63 

    64 datatype apg = 

    65    Instr abc_inst

    66  | Label nat

    67  | Seq apg apg

    68  | Local "(nat \<Rightarrow> apg)"

    69 

    70 abbreviation prog_instr :: "abc_inst \<Rightarrow> apg" ("\<guillemotright>_" [61] 61)

    71 where "\<guillemotright>i \<equiv> Instr i"

    72 

    73 abbreviation prog_seq :: "apg \<Rightarrow> apg \<Rightarrow> apg" (infixl ";" 52)

    74 where "c1 ; c2 \<equiv> Seq c1 c2"

    75 

    76 type_synonym aconf = "((nat \<rightharpoonup> abc_inst) \<times> nat \<times> (nat \<rightharpoonup> nat) \<times> nat)"

    77 

    78 fun astep :: "aconf \<Rightarrow> aconf"

    79   where "astep (prog, pc, m, faults) = 

    80               (case (prog pc) of

    81                   Some (Inc i) \<Rightarrow> 

    82                          case m(i) of

    83                            Some n \<Rightarrow> (prog, pc + 1, m(i:= Some (n + 1)), faults)

    84                          | None \<Rightarrow> (prog, pc, m, faults + 1)

    85                 | Some (Dec i e) \<Rightarrow> 

    86                          case m(i) of

    87                            Some n \<Rightarrow> if (n = 0) then (prog, e, m, faults)

    88                                      else (prog, pc + 1, m(i:= Some (n - 1)), faults)

    89                          | None \<Rightarrow> (prog, pc, m, faults + 1)

    90                 | Some (Goto pc') \<Rightarrow> (prog, pc', m, faults)

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

    92 

    93 definition "run n = astep ^^ n"

    94 

    95 datatype aresource = 

    96     M nat nat

    97   | C nat abc_inst

    98   | At nat

    99   | Faults nat

   100 

   101 fun rset_of :: "aconf \<Rightarrow> aresource set"

   102   where "rset_of (prog, pc, m, faults) = 

   103                {M i n | i n. m (i) = Some n} \<union> {At pc} \<union>

   104                {C i inst | i inst. prog i = Some inst} \<union> {Faults faults}"

   105 

   106 type_synonym assert = "aresource set set"

   107 

   108 primrec assemble_to :: "apg \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> assert" 

   109   where 

   110   "assemble_to (Instr ai) i j = ({{C i ai}} * <(j = i + 1)>)" |

   111   "assemble_to (Seq p1 p2) i j = (\<Union> j'. (assemble_to p1 i j') * (assemble_to p2 j' j))" |

   112   "assemble_to (Local fp) i j  = (\<Union> l. (assemble_to (fp l) i j))" |

   113   "assemble_to (Label l) i j = <(i = j \<and> j = l)>"

   114 

   115 abbreviation asmb_to :: "nat \<Rightarrow> apg \<Rightarrow> nat \<Rightarrow> assert" ("_ :[ _ ]: _" [60, 60, 60] 60)

   116 where "i :[ apg ]: j \<equiv> assemble_to apg i j"

   117 

   118 definition

   119   Hoare_abc :: "assert \<Rightarrow> assert  \<Rightarrow> assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" 50)

   120 where

   121   "{p} c {q} \<equiv> (\<forall> s r. (rset_of s) \<in> (p*c*r) \<longrightarrow> (\<exists> k. ((rset_of (run k s)) \<in> (q*c*r))))" 

   122 

   123 definition "pc l = {{At l}}"

   124 

   125 definition "m a v = {{M a v}}"

   126 

   127 lemma hoare_dec_suc: "{pc i * m a v * <(v > 0)>} 

   128                           i:[ \<guillemotright>(Dec a e) ]:j  

   129                       {pc (i+1) * m a (v - 1)}"

   130   sorry

   131 

   132 lemma hoare_dec_fail: "{pc i * m a 0} 

   133                           i:[ \<guillemotright>(Dec a e) ]:j   

   134                        {pc e * m a 0}"

   135   sorry

   136 

   137 lemma hoare_inc: "{pc i * m a v} 

   138                       i:[ \<guillemotright>(Inc a) ]:j   

   139                   {pc (i+1) * m a (v + 1)}"

   140   sorry

   141 

   142 

   143 interpretation foo: comm_monoid_mult "op * :: 'a set set => 'a set set => 'a set set" "{{}}::'a set set"

   144 apply(default)

   145 apply(simp add: stimes_assoc)

   146 apply(simp add: stimes_comm)

   147 apply(simp add: emp_def[symmetric])

   148 done

   149 

   150 

   151 (*used by simplifier for numbers *)

   152 thm mult_cancel_left

   153 

   154 (*

   155 interpretation foo: comm_ring_1 "op * :: 'a set set => 'a set set => 'a set set" "{{}}::'a set set" 

   156 apply(default)

   157 *)

   158 

   159 lemma frame: "{p} c {q} \<Longrightarrow> \<forall> r. {p * r} c {q * r}"

   160 apply (unfold Hoare_abc_def, clarify)

   161 apply (erule_tac x = "(a, aa, ab, b)" in allE)

   162 apply (erule_tac x = "r*ra" in allE) 

   163 apply(simp add: stimes_ac)

   164 done

   165 

   166 lemma code_extension: "\<lbrakk>{p} c {q}\<rbrakk> \<Longrightarrow> (\<forall> e. {p} c * e {q})"

   167   apply (unfold Hoare_abc_def, clarify)

   168   apply (erule_tac x = "(a, aa, ab, b)" in allE)

   169   apply (erule_tac x = "e * r" in allE)

   170   apply(simp add: stimes_ac)

   171   done

   172 

   173 lemma run_add: "run (n1 + n2) s = run n1 (run n2 s)"

   174 apply (unfold run_def)

   175 by (metis funpow_add o_apply)

   176 

   177 lemma composition: "\<lbrakk>{p} c1 {q}; {q} c2 {r}\<rbrakk> \<Longrightarrow> {p} c1 * c2 {r}"

   178 proof -

   179   assume h: "{p} c1 {q}" "{q} c2 {r}"

   180   from code_extension [OF h(1), rule_format, of "c2"] 

   181   have "{p} c1 * c2 {q}" .

   182   moreover from code_extension [OF h(2), rule_format, of "c1"] and stimes_comm

   183   have "{q} c1 * c2 {r}" by metis

   184   ultimately show "{p} c1 * c2 {r}"

   185     apply (unfold Hoare_abc_def, clarify)

   186     proof -

   187       fix a aa ab b ra

   188       assume h1: "\<forall>s r. rset_of s \<in> p * (c1 * c2) * r \<longrightarrow>

   189                        (\<exists>k. rset_of (run k s) \<in> q * (c1 * c2) * r)"

   190         and h2: "\<forall>s ra. rset_of s \<in> q * (c1 * c2) * ra \<longrightarrow>

   191                        (\<exists>k. rset_of (run k s) \<in> r * (c1 * c2) * ra)"

   192         and h3: "rset_of (a, aa, ab, b) \<in> p * (c1 * c2) * ra"

   193       show "\<exists>k. rset_of (run k (a, aa, ab, b)) \<in> r * (c1 * c2) * ra"

   194       proof -

   195         let ?s = "(a, aa, ab, b)"

   196         from h1 [rule_format, of ?s, OF h3]

   197         obtain n1 where "rset_of (run n1 ?s) \<in> q * (c1 * c2) * ra" by blast

   198         from h2 [rule_format, OF this]

   199         obtain n2 where "rset_of (run n2 (run n1 ?s)) \<in> r * (c1 * c2) * ra" by blast

   200         with run_add show ?thesis by metis

   201       qed

   202     qed

   203 qed

   204 

   205 lemma asm_end_unique: "\<lbrakk>s \<in> (i:[c]:j1); s' \<in> (i:[c]:j2)\<rbrakk> \<Longrightarrow> j1 = j2"

   206 (* proof(induct c arbitrary:i j1 j2 s s') *) sorry

   207 

   208 lemma union_unique: "(\<forall> j. j \<noteq> i \<longrightarrow> c(j) = {}) \<Longrightarrow> (\<Union> j. c(j)) = (c i)"

   209   by auto

   210 

   211 lemma asm_consist: "i:[c1]:j \<noteq> {}"

   212   sorry

   213 

   214 lemma seq_comp: "\<lbrakk>{p} i:[c1]:j {q}; 

   215                   {q} j:[c2]:k {r}\<rbrakk> \<Longrightarrow> {p} i:[(c1 ; c2)]:k {r}"

   216 apply (unfold assemble_to.simps)

   217 proof -

   218   assume h: "{p} i :[ c1 ]: j {q}" "{q} j :[ c2 ]: k {r}"

   219   have " (\<Union>j'. (i :[ c1 ]: j') * (j' :[ c2 ]: k)) = 

   220              (i :[ c1 ]: j) * (j :[ c2 ]: k)"

   221   proof -

   222     { fix j' 

   223       assume "j' \<noteq> j"

   224       have "(i :[ c1 ]: j') * (j' :[ c2 ]: k) = {}" (is "?X * ?Y = {}")

   225       proof -

   226         { fix s 

   227           assume "s \<in> ?X*?Y"

   228           then obtain s1 s2 where h1: "s1 \<in> ?X" by (unfold stimes_def, auto)

   229           

   230         }

   231       qed

   232     } thus ?thesis by (auto intro!:union_unique)

   233   qed

   234   moreover have "{p} \<dots> {r}" by (rule composition [OF h])

   235   ultimately show "{p} \<Union>j'. (i :[ c1 ]: j') * (j' :[ c2 ]: k) {r}" by metis

   236 qed

   237   

   238 

   239  

   240 end