diff -r d682591c63e1 -r db6ba2232945 Tests/abacus.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Tests/abacus.thy	Thu Mar 14 18:02:26 2013 +0000
@@ -0,0 +1,240 @@
+header {* 
+ {\em abacus} a kind of register machine
+*}
+
+theory abacus
+imports Main "~~/src/HOL/Algebra/IntRing" 
+begin
+
+text {*
+  {\em Abacus} instructions:
+*}
+
+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
+
+definition "stimes p q = {s . \<exists> u v. u \<in> p \<and> v \<in> q \<and> (u \<union> v = s) \<and> (u \<inter> v = {})}"
+
+no_notation times (infixl "*" 70)
+
+notation stimes (infixl "*" 70)
+
+lemma stimes_comm: "p * q = q * p"
+  by (unfold stimes_def, auto)
+
+lemma stimes_assoc: "(p * q) * r = p * (q * r)"
+  by (unfold stimes_def, blast)
+
+definition
+  "emp = {{}}"
+
+lemma emp_unit_r [simp]: "p * emp = p"
+  by (unfold stimes_def emp_def, auto)
+
+lemma emp_unit_l [simp]: "emp * p = p"
+  by (metis emp_unit_r stimes_comm)
+
+lemma stimes_mono: "p \<subseteq> q \<Longrightarrow> p * r \<subseteq> q * r"
+  by (unfold stimes_def, auto)
+
+thm mult_cancel_left
+
+lemma stimes_left_commute:
+  "(p * (q * r)) = (q * (p * r))"
+by (metis stimes_assoc stimes_comm)
+
+lemmas stimes_ac = stimes_comm stimes_assoc stimes_left_commute
+
+definition pasrt :: "bool \<Rightarrow> ('a set set)" ("<_>" [71] 71)
+where "pasrt b = {s . s = {} \<and> b}"
+
+datatype apg = 
+   Instr abc_inst
+ | Label nat
+ | Seq apg apg
+ | Local "(nat \<Rightarrow> apg)"
+
+abbreviation prog_instr :: "abc_inst \<Rightarrow> apg" ("\<guillemotright>_" [61] 61)
+where "\<guillemotright>i \<equiv> Instr i"
+
+abbreviation prog_seq :: "apg \<Rightarrow> apg \<Rightarrow> apg" (infixl ";" 52)
+where "c1 ; c2 \<equiv> Seq c1 c2"
+
+type_synonym aconf = "((nat \<rightharpoonup> abc_inst) \<times> nat \<times> (nat \<rightharpoonup> nat) \<times> nat)"
+
+fun astep :: "aconf \<Rightarrow> aconf"
+  where "astep (prog, pc, m, faults) = 
+              (case (prog pc) of
+                  Some (Inc i) \<Rightarrow> 
+                         case m(i) of
+                           Some n \<Rightarrow> (prog, pc + 1, m(i:= Some (n + 1)), faults)
+                         | None \<Rightarrow> (prog, pc, m, faults + 1)
+                | Some (Dec i e) \<Rightarrow> 
+                         case m(i) of
+                           Some n \<Rightarrow> if (n = 0) then (prog, e, m, faults)
+                                     else (prog, pc + 1, m(i:= Some (n - 1)), faults)
+                         | None \<Rightarrow> (prog, pc, m, faults + 1)
+                | Some (Goto pc') \<Rightarrow> (prog, pc', m, faults)
+                | None \<Rightarrow> (prog, pc, m, faults + 1))"
+
+definition "run n = astep ^^ n"
+
+datatype aresource = 
+    M nat nat
+  | C nat abc_inst
+  | At nat
+  | Faults nat
+
+fun rset_of :: "aconf \<Rightarrow> aresource set"
+  where "rset_of (prog, pc, m, faults) = 
+               {M i n | i n. m (i) = Some n} \<union> {At pc} \<union>
+               {C i inst | i inst. prog i = Some inst} \<union> {Faults faults}"
+
+type_synonym assert = "aresource set set"
+
+primrec assemble_to :: "apg \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> assert" 
+  where 
+  "assemble_to (Instr ai) i j = ({{C i ai}} * <(j = i + 1)>)" |
+  "assemble_to (Seq p1 p2) i j = (\<Union> j'. (assemble_to p1 i j') * (assemble_to p2 j' j))" |
+  "assemble_to (Local fp) i j  = (\<Union> l. (assemble_to (fp l) i j))" |
+  "assemble_to (Label l) i j = <(i = j \<and> j = l)>"
+
+abbreviation asmb_to :: "nat \<Rightarrow> apg \<Rightarrow> nat \<Rightarrow> assert" ("_ :[ _ ]: _" [60, 60, 60] 60)
+where "i :[ apg ]: j \<equiv> assemble_to apg i j"
+
+definition
+  Hoare_abc :: "assert \<Rightarrow> assert  \<Rightarrow> assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" 50)
+where
+  "{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))))" 
+
+definition "pc l = {{At l}}"
+
+definition "m a v = {{M a v}}"
+
+lemma hoare_dec_suc: "{pc i * m a v * <(v > 0)>} 
+                          i:[ \<guillemotright>(Dec a e) ]:j  
+                      {pc (i+1) * m a (v - 1)}"
+  sorry
+
+lemma hoare_dec_fail: "{pc i * m a 0} 
+                          i:[ \<guillemotright>(Dec a e) ]:j   
+                       {pc e * m a 0}"
+  sorry
+
+lemma hoare_inc: "{pc i * m a v} 
+                      i:[ \<guillemotright>(Inc a) ]:j   
+                  {pc (i+1) * m a (v + 1)}"
+  sorry
+
+
+interpretation foo: comm_monoid_mult "op * :: 'a set set => 'a set set => 'a set set" "{{}}::'a set set"
+apply(default)
+apply(simp add: stimes_assoc)
+apply(simp add: stimes_comm)
+apply(simp add: emp_def[symmetric])
+done
+
+
+(*used by simplifier for numbers *)
+thm mult_cancel_left
+
+(*
+interpretation foo: comm_ring_1 "op * :: 'a set set => 'a set set => 'a set set" "{{}}::'a set set" 
+apply(default)
+*)
+
+lemma frame: "{p} c {q} \<Longrightarrow> \<forall> r. {p * r} c {q * r}"
+apply (unfold Hoare_abc_def, clarify)
+apply (erule_tac x = "(a, aa, ab, b)" in allE)
+apply (erule_tac x = "r*ra" in allE) 
+apply(simp add: stimes_ac)
+done
+
+lemma code_extension: "\<lbrakk>{p} c {q}\<rbrakk> \<Longrightarrow> (\<forall> e. {p} c * e {q})"
+  apply (unfold Hoare_abc_def, clarify)
+  apply (erule_tac x = "(a, aa, ab, b)" in allE)
+  apply (erule_tac x = "e * r" in allE)
+  apply(simp add: stimes_ac)
+  done
+
+lemma run_add: "run (n1 + n2) s = run n1 (run n2 s)"
+apply (unfold run_def)
+by (metis funpow_add o_apply)
+
+lemma composition: "\<lbrakk>{p} c1 {q}; {q} c2 {r}\<rbrakk> \<Longrightarrow> {p} c1 * c2 {r}"
+proof -
+  assume h: "{p} c1 {q}" "{q} c2 {r}"
+  from code_extension [OF h(1), rule_format, of "c2"] 
+  have "{p} c1 * c2 {q}" .
+  moreover from code_extension [OF h(2), rule_format, of "c1"] and stimes_comm
+  have "{q} c1 * c2 {r}" by metis
+  ultimately show "{p} c1 * c2 {r}"
+    apply (unfold Hoare_abc_def, clarify)
+    proof -
+      fix a aa ab b ra
+      assume h1: "\<forall>s r. rset_of s \<in> p * (c1 * c2) * r \<longrightarrow>
+                       (\<exists>k. rset_of (run k s) \<in> q * (c1 * c2) * r)"
+        and h2: "\<forall>s ra. rset_of s \<in> q * (c1 * c2) * ra \<longrightarrow>
+                       (\<exists>k. rset_of (run k s) \<in> r * (c1 * c2) * ra)"
+        and h3: "rset_of (a, aa, ab, b) \<in> p * (c1 * c2) * ra"
+      show "\<exists>k. rset_of (run k (a, aa, ab, b)) \<in> r * (c1 * c2) * ra"
+      proof -
+        let ?s = "(a, aa, ab, b)"
+        from h1 [rule_format, of ?s, OF h3]
+        obtain n1 where "rset_of (run n1 ?s) \<in> q * (c1 * c2) * ra" by blast
+        from h2 [rule_format, OF this]
+        obtain n2 where "rset_of (run n2 (run n1 ?s)) \<in> r * (c1 * c2) * ra" by blast
+        with run_add show ?thesis by metis
+      qed
+    qed
+qed
+
+lemma asm_end_unique: "\<lbrakk>s \<in> (i:[c]:j1); s' \<in> (i:[c]:j2)\<rbrakk> \<Longrightarrow> j1 = j2"
+(* proof(induct c arbitrary:i j1 j2 s s') *) sorry
+
+lemma union_unique: "(\<forall> j. j \<noteq> i \<longrightarrow> c(j) = {}) \<Longrightarrow> (\<Union> j. c(j)) = (c i)"
+  by auto
+
+lemma asm_consist: "i:[c1]:j \<noteq> {}"
+  sorry
+
+lemma seq_comp: "\<lbrakk>{p} i:[c1]:j {q}; 
+                  {q} j:[c2]:k {r}\<rbrakk> \<Longrightarrow> {p} i:[(c1 ; c2)]:k {r}"
+apply (unfold assemble_to.simps)
+proof -
+  assume h: "{p} i :[ c1 ]: j {q}" "{q} j :[ c2 ]: k {r}"
+  have " (\<Union>j'. (i :[ c1 ]: j') * (j' :[ c2 ]: k)) = 
+             (i :[ c1 ]: j) * (j :[ c2 ]: k)"
+  proof -
+    { fix j' 
+      assume "j' \<noteq> j"
+      have "(i :[ c1 ]: j') * (j' :[ c2 ]: k) = {}" (is "?X * ?Y = {}")
+      proof -
+        { fix s 
+          assume "s \<in> ?X*?Y"
+          then obtain s1 s2 where h1: "s1 \<in> ?X" by (unfold stimes_def, auto)
+          
+        }
+      qed
+    } thus ?thesis by (auto intro!:union_unique)
+  qed
+  moreover have "{p} \<dots> {r}" by (rule composition [OF h])
+  ultimately show "{p} \<Union>j'. (i :[ c1 ]: j') * (j' :[ c2 ]: k) {r}" by metis
+qed
+  
+
+ 
+end