# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1364390197 0
# Node ID 49dcc0b9b0b3fa5e3bc255620b2084d5f4707361
# Parent  d8e6f0798e235a171e1474160a69611e9d178c6e
adapted paper

diff -r d8e6f0798e23 -r 49dcc0b9b0b3 Paper/Paper.thy
--- a/Paper/Paper.thy	Wed Mar 27 09:47:02 2013 +0000
+++ b/Paper/Paper.thy	Wed Mar 27 13:16:37 2013 +0000
@@ -88,7 +88,7 @@
   Pr ("Pr\<^isup>_") and
   Cn ("Cn\<^isup>_") and
   Mn ("Mn\<^isup>_") and
-  rec_calc_rel ("eval") and 
+  rec_exec ("eval") and
   tm_of_rec ("translate") and
   listsum ("\<Sigma>")
 
@@ -103,9 +103,10 @@
 apply(case_tac [!] tp)
 by (auto)
 
+
 lemma inv1: 
-  shows "0 < n \<Longrightarrow> inv_begin0 n \<mapsto> inv_loop1 n"
-unfolding assert_imp_def
+  shows "0 < (n::nat) \<Longrightarrow> Turing_Hoare.assert_imp (inv_begin0 n) (inv_loop1 n)"
+unfolding Turing_Hoare.assert_imp_def
 unfolding inv_loop1.simps inv_begin0.simps
 apply(auto)
 apply(rule_tac x="1" in exI)
@@ -872,13 +873,13 @@
   \noindent
   whose three components are given in Figure~\ref{copy}. For our
   correctness proofs, we introduce the notion of total correctness
-  defined in terms of \emph{Hoare-triples}, written @{term "{P} p
+  defined in terms of \emph{Hoare-triples}, written @{term "{P} (p::tprog0)
   {Q}"}.  They implement the idea that a program @{term
   p} started in state @{term "1::nat"} with a tape satisfying @{term
   P} will after some @{text n} steps halt (have transitioned into the
   halting state) with a tape satisfying @{term Q}. This idea is very
   similar to the notion of \emph{realisability} in \cite{AspertiRicciotti12}. We
-  also have \emph{Hoare-pairs} of the form @{term "{P} p \<up>"}
+  also have \emph{Hoare-pairs} of the form @{term "{P} (p::tprog0) \<up>"}
   implementing the case that a program @{term p} started with a tape
   satisfying @{term P} will loop (never transition into the halting
   state). Both notion are formally defined as
@@ -911,7 +912,7 @@
 
   \noindent
   where
-  @{term "P' \<mapsto> P"} stands for the fact that for all tapes @{term "tp"},
+  @{term "Turing_Hoare.assert_imp P' P"} stands for the fact that for all tapes @{term "tp"},
   @{term "P' tp"} implies @{term "P tp"} (similarly for @{text "Q"} and @{text "Q'"}).
 
   Like Asperti and Ricciotti with their notion of realisability, we
@@ -1122,8 +1123,8 @@
   where we assume @{text "0 < n"} (similar reasoning is needed for
   the Hoare-triples for @{term tcopy_loop} and @{term tcopy_end}). Since the invariant of
   the halting state of @{term tcopy_begin} implies the invariant of
-  the starting state of @{term tcopy_loop}, that is @{term "inv_begin0
-  n \<mapsto> inv_loop1 n"} holds, and also @{term "inv_loop0 n = inv_end1
+  the starting state of @{term tcopy_loop}, that is @{term "Turing_Hoare.assert_imp (inv_begin0 n)
+  (inv_loop1 n)"} holds, and also @{term "inv_loop0 n = inv_end1
   n"}, we can derive the following Hoare-triple for the correctness 
   of @{term tcopy}:
 
@@ -1406,9 +1407,9 @@
             & @{text "|"}   & @{term "id n m"} & (projection)\\
   \end{tabular} &
   \begin{tabular}{cl@ {\hspace{4mm}}l}
-  @{text "|"} & @{term "Cn n r rs"} & (composition)\\
-  @{text "|"} & @{term "Pr n r\<^isub>1 r\<^isub>2"} & (primitive recursion)\\
-  @{text "|"} & @{term "Mn n r"} & (minimisation)\\
+  @{text "|"} & @{term "Cn n f fs"} & (composition)\\
+  @{text "|"} & @{term "Pr n f\<^isub>1 f\<^isub>2"} & (primitive recursion)\\
+  @{text "|"} & @{term "Mn n f"} & (minimisation)\\
   \end{tabular}
   \end{tabular}
   \end{center}
@@ -1416,29 +1417,32 @@
   \noindent 
   where @{text n} indicates the function expects @{term n} arguments
   (in \cite{Boolos87} both @{text z} and @{term s} expect one
-  argument), and @{text rs} stands for a list of recursive
+  argument), and @{text fs} stands for a list of recursive
   functions. Since we know in each case the arity, say @{term l}, we
-  can define an inductive evaluation relation that relates a recursive
-  function @{text r} and a list @{term ns} of natural numbers of
-  length @{text l}, to what the result of the recursive function is,
-  say @{text n}. We omit the definition of @{term "rec_calc_rel r ns
-  n"}. Because of space reasons, we also omit the definition of
+  can define an evaluation function, called @{term rec_exec}, that takes a recursive
+  function @{text f} and a list @{term ns} of natural numbers of
+  length @{text l} as arguments. Since this evaluation function uses 
+  the minimisation operator
+  from HOL, this function might not terminate always. As a result we also
+  need to inductively characterise when @{term rec_exec} terminates.
+  We omit the definitions for
+  @{term "rec_exec f ns"} and @{term "terminate f ns"}. Because of 
+  space reasons, we also omit the definition of
   translating recursive functions into abacus programs. We can prove,
   however, the following theorem about the translation: If @{thm (prem
-  1) recursive_compile_to_tm_correct3[where recf="r" and args="ns" and
-  r="n"]} holds for the recursive function @{text r}, then the
+  1) recursive_compile_to_tm_correct3[where recf="f" and args="ns"]} 
+  holds for the recursive function @{text f} and arguments @{term ns}, then the
   following Hoare-triple holds
 
   \begin{center}
-  @{thm (concl) recursive_compile_to_tm_correct3[where recf="r" and args="ns" and r="n"]}
+  @{thm (concl) recursive_compile_to_tm_correct3[where recf="f" and args="ns"]}
   \end{center}
 
   \noindent
-  for the translated Turing machine @{term "translate r"}. This
-  means that if the recursive function @{text r} with arguments @{text ns} evaluates
-  to @{text n}, then the translated Turing machine if started
+  for the Turing machine generated by @{term "translate f"}. This
+  means the translated Turing machine if started
   with the standard tape @{term "([Bk, Bk], <ns::nat list>)"} will terminate
-  with the standard tape @{term "(Bk \<up> k, <n::nat> @ Bk \<up> l)"} for some @{text k} and @{text l}.
+  with the standard tape @{term "(Bk \<up> k, <(rec_exec f ns)::nat> @ Bk \<up> l)"} for some @{text k} and @{text l}.
 
   Having recursive functions under our belt, we can construct a universal
   function, written @{text UF}. This universal function acts like an interpreter for Turing machines.
@@ -1560,12 +1564,13 @@
   If started with standard tape @{term "([], [Oc])"}, it halts with the
   non-standard tape @{term "([Oc], [])"} according to the definition in Chapter 3---so no
   result is calculated; but with the standard tape @{term "([], [Oc])"} according to the 
-  definition in Chapter 8. We solve this inconsitency in our formalisation by
+  definition in Chapter 8. 
+  We solve this inconsistency in our formalisation by
   setting up our definitions so that the @{text counter_example} Turing machine does not 
   produce any result by looping forever fetching @{term Nop}s in state @{text 0}. 
-  This solution is different from the definition in Chapter 3, but also 
-  different from the one in Chapter 8, where the instruction from state @{text 1} is 
-  fetched.
+  This solution implements essentially the definition in Chapter 3; it  
+  differs from the definition in Chapter 8, where perplexingly the instruction 
+  from state @{text 1} is fetched.
 *}
 
 (*
@@ -1676,7 +1681,7 @@
   functions and abacus machines, we agree, is not a project
   one wants to undertake too many times (our formalisation of abacus
   machines and their correct translation is approximately 4600 loc;
-  recursive functions 5000 loc and the universal Turing machine 10000 loc).
+  recursive functions 2800 loc and the universal Turing machine 10000 loc).
   
   Our work is also very much inspired by the formalisation of Turing
   machines of Asperti and Ricciotti \cite{AspertiRicciotti12} in the
diff -r d8e6f0798e23 -r 49dcc0b9b0b3 Tests/Rec_def2.thy
--- a/Tests/Rec_def2.thy	Wed Mar 27 09:47:02 2013 +0000
+++ b/Tests/Rec_def2.thy	Wed Mar 27 13:16:37 2013 +0000
@@ -9,6 +9,10 @@
               |  Pr nat recf recf
               |  Mn nat recf 
 
+definition pred_of_nl :: "nat list \<Rightarrow> nat list"
+  where
+  "pred_of_nl xs = butlast xs @ [last xs - 1]"
+
 function rec_exec :: "recf \<Rightarrow> nat list \<Rightarrow> nat"
   where
   "rec_exec z xs = 0" |
@@ -17,13 +21,13 @@
   "rec_exec (Cn n f gs) xs = 
      rec_exec f (map (\<lambda> a. rec_exec a xs) gs)" | 
   "rec_exec (Pr n f g) xs = 
-     (if hd xs = 0 then rec_exec f (tl xs)
-      else rec_exec g ((hd xs - 1) # (rec_exec (Pr n f g) ((hd xs - 1) # tl xs)) # tl xs))" |
-  "rec_exec (Mn n f) xs = (LEAST x. rec_exec f (x # xs) = 0)"
+     (if last xs = 0 then rec_exec f (butlast xs)
+      else rec_exec g (butlast xs @ (last xs - 1) # [rec_exec (Pr n f g) (butlast xs @ [last xs - 1])]))" |
+  "rec_exec (Mn n f) xs = (LEAST x. rec_exec f (xs @ [x]) = 0)"
 by pat_completeness auto
 
 termination
-apply(relation "measures [\<lambda> (r, xs). size r, (\<lambda> (r, xs). hd xs)]")
+apply(relation "measures [\<lambda> (r, xs). size r, (\<lambda> (r, xs). last xs)]")
 apply(auto simp add: less_Suc_eq_le intro: trans_le_add2 list_size_estimation')
 done
 
@@ -34,11 +38,11 @@
 | termi_id: "\<lbrakk>n < m; length xs = m\<rbrakk> \<Longrightarrow> terminate (id m n) xs"
 | termi_cn: "\<lbrakk>terminate f (map (\<lambda>g. rec_exec g xs) gs); 
               \<forall>g \<in> set gs. terminate g xs; length xs = n\<rbrakk> \<Longrightarrow> terminate (Cn n f gs) xs"
-| termi_pr_0: "\<lbrakk>terminate f xs; length xs = n\<rbrakk> \<Longrightarrow> terminate (Pr n f g) (0 # xs)"
-| termi_pr_suc: "\<lbrakk>terminate (Pr n f gs) (x # xs); length xs = n;
-                  terminate g (x # rec_exec (Pr n f gs) (x # xs) # xs)\<rbrakk> 
-                  \<Longrightarrow> terminate (Pr n f gs) (Suc x # xs)"
-| termi_mn: "\<lbrakk>length xs = n; rec_exec f (r # xs) = 0;
-              \<forall> i < r. terminate f (i # xs) \<and> rec_exec f (i # xs) > 0\<rbrakk> \<Longrightarrow> terminate (Mn n f) xs"
+| termi_pr: "\<lbrakk>\<forall> y < x. terminate g (xs @ y # [rec_exec (Pr n f g) (xs @ [y])]);
+              terminate f xs;
+              length xs = n\<rbrakk> 
+              \<Longrightarrow> terminate (Pr n f g) (xs @ [x])"
+| termi_mn: "\<lbrakk>length xs = n; rec_exec f (xs @ [r]) = 0;
+              \<forall> i < r. terminate f (xs @ [i]) \<and> rec_exec f (xs @ [i]) > 0\<rbrakk> \<Longrightarrow> terminate (Mn n f) xs"
 
 end
\ No newline at end of file
diff -r d8e6f0798e23 -r 49dcc0b9b0b3 Tests/abacus.thy
--- a/Tests/abacus.thy	Wed Mar 27 09:47:02 2013 +0000
+++ b/Tests/abacus.thy	Wed Mar 27 13:16:37 2013 +0000
@@ -3,7 +3,7 @@
 *}
 
 theory abacus
-imports Main
+imports Main (*StateMonad*)
 begin
 
 text {*
@@ -26,38 +26,48 @@
   *}
    | 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 = {})}"
+
+fun splits :: "'a set \<Rightarrow> ('a set \<times> 'a set) \<Rightarrow> bool"
+where "splits s (u, v) = (u \<union> v = s \<and> u \<inter> v = {})"
 
-no_notation times (infixl "*" 70)
+declare splits.simps [simp del]
 
-notation stimes (infixl "*" 70)
+definition "stimes p q = {s . \<exists> u v. u \<in> p \<and> v \<in> q \<and> splits s (u, v)}"
+lemmas st_def = stimes_def[unfolded splits.simps]
 
-lemma stimes_comm: "p * q = q * p"
-  by (unfold stimes_def, auto)
+notation stimes (infixr "*" 70)
+
+lemma stimes_comm: "(p::('a set set)) * q = q * p"
+  by (unfold st_def, auto)
 
-lemma stimes_assoc: "(p * q) * r = p * (q * r)"
-  by (unfold stimes_def, blast)
+lemma splits_simp: "splits s (u, v) = (v = (s - u) \<and> v \<subseteq> s \<and> u \<subseteq> s)"
+  by (unfold splits.simps, auto)
+
+lemma stimes_assoc: "p * q * r = (p * q) * (r::'a set set)"
+  by (unfold st_def, blast)
 
 definition
   "emp = {{}}"
 
 lemma emp_unit_r [simp]: "p * emp = p"
-  by (unfold stimes_def emp_def, auto)
+  by (unfold st_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
+  by (unfold st_def, auto)
 
 lemma stimes_left_commute:
-  "(p * (q * r)) = (q * (p * r))"
+  "(q * (p * r)) = ((p::'a set set) * (q * r))"
 by (metis stimes_assoc stimes_comm)
 
 lemmas stimes_ac = stimes_comm stimes_assoc stimes_left_commute
 
+lemma "x * y * z = z * y * (x::'a set set)"
+by (metis stimes_ac)
+
+
 definition pasrt :: "bool \<Rightarrow> ('a set set)" ("<_>" [71] 71)
 where "pasrt b = {s . s = {} \<and> b}"
 
@@ -67,6 +77,12 @@
  | Seq apg apg
  | Local "(nat \<Rightarrow> apg)"
 
+notation Local (binder "LOCAL " 10)
+
+term "LOCAL a b. Seq (Label a) (Label b)"
+
+
+
 abbreviation prog_instr :: "abc_inst \<Rightarrow> apg" ("\<guillemotright>_" [61] 61)
 where "\<guillemotright>i \<equiv> Instr i"
 
@@ -98,10 +114,24 @@
   | At nat
   | Faults nat
 
+definition "prog_set prog = {C i inst | i inst. prog i = Some inst}"
+definition "pc_set pc = {At pc}"
+definition "mem_set m = {M i n | i n. m (i) = Some n} "
+definition "faults_set faults = {Faults faults}"
+
+lemmas cpn_set_def = prog_set_def pc_set_def mem_set_def faults_set_def
+
 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}"
+               prog_set prog \<union> pc_set pc \<union> mem_set m \<union> faults_set faults"
+
+definition "pc l = {pc_set l}"
+
+
+definition "m a v = {{M a v}}"
+
+
+declare rset_of.simps[simp del]
 
 type_synonym assert = "aresource set set"
 
@@ -113,34 +143,328 @@
   "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"
+  where "i :[ apg ]: j \<equiv> assemble_to apg i j"
+
+lemma stimes_sgD: "s \<in> {x} * q \<Longrightarrow> (s - x) \<in> q \<and> x \<subseteq> s"
+  apply (unfold st_def, auto)
+by (smt Diff_disjoint Un_Diff_cancel2 Un_Int_distrib 
+     Un_commute Un_empty_right Un_left_absorb)
+
+lemma pcD: "rset_of (prog, i', mem, fault) \<in> pc i * r
+       \<Longrightarrow> i' = i"
+proof -
+  assume "rset_of (prog, i', mem, fault) \<in> pc i * r"
+  from stimes_sgD [OF this[unfolded pc_def], unfolded rset_of.simps]
+  have "pc_set i \<subseteq> prog_set prog \<union> pc_set i' \<union> mem_set mem \<union> faults_set fault" by auto
+  thus ?thesis 
+    by (unfold cpn_set_def, auto)
+qed
+
+lemma codeD: "rset_of (prog, pos, mem, fault) \<in>  pc i * {{C i inst}} * r
+       \<Longrightarrow> prog pos = Some inst"
+proof -
+  assume h: "rset_of (prog, pos, mem, fault) \<in>  pc i * {{C i inst}} * r" (is "?c \<in> ?X")
+  from pcD[OF this] have "i = pos" by simp
+  with h show ?thesis
+    by (unfold rset_of.simps st_def pc_def prog_set_def 
+      pc_set_def mem_set_def faults_set_def, auto)
+qed
+
+lemma memD: "rset_of (prog, pos, mem, fault) \<in>  (m a v)  * r \<Longrightarrow> mem a = Some v"
+proof -
+  assume "rset_of (prog, pos, mem, fault) \<in>  (m a v)  * r"
+  from stimes_sgD[OF this[unfolded rset_of.simps cpn_set_def m_def]]
+  have "{M a v} \<subseteq> {C i inst |i inst. prog i = Some inst} \<union> 
+            {At pos} \<union> {M i n |i n. mem i = Some n} \<union> {Faults fault}" by auto
+  thus ?thesis by auto
+qed
 
 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))))" 
+  "{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 "dec_fun v j e = (if (v = 0) then (e, v) else (j, v - 1))"
+
+lemma disj_Diff: "a \<inter> b = {} \<Longrightarrow> a \<union> b - b = a"
+by (metis (lifting) Diff_cancel Un_Diff Un_Diff_Int)
 
-definition "pc l = {{At l}}"
+lemma diff_pc_set: "prog_set aa \<union> pc_set i \<union> mem_set ab \<union> faults_set b - pc_set i = 
+         prog_set aa \<union> mem_set ab \<union> faults_set b"  (is "?L = ?R")
+proof -
+  have "?L = (prog_set aa \<union> mem_set ab \<union> faults_set b \<union> pc_set i)  - pc_set i"
+    by auto
+  also have "\<dots> = ?R"
+  proof(rule disj_Diff)
+    show " (prog_set aa \<union> mem_set ab \<union> faults_set b) \<inter> pc_set i = {}"
+      by (unfold cpn_set_def, auto)
+  qed
+  finally show ?thesis .
+qed
+
+lemma M_in_simp: "({M a v} \<subseteq> prog_set x \<union> pc_set y \<union> mem_set mem \<union> faults_set f) = 
+        ({M a v} \<subseteq> mem_set mem)"
+  by (unfold cpn_set_def, auto)
+
+lemma mem_set_upd: 
+  "{M a v} \<subseteq> mem_set mem \<Longrightarrow> mem_set (mem(a:=Some v')) = ((mem_set mem) - {M a v}) \<union> {M a v'}"
+  by (unfold cpn_set_def, auto)
+
+lemma mem_set_disj: "{M a v} \<subseteq> mem_set mem \<Longrightarrow> {M a v'} \<inter>  (mem_set mem - {M a v}) = {}"
+  by (unfold cpn_set_def, auto)
+
+lemma stimesE:
+  assumes h: "s \<in> x * y"
+  obtains s1 s2 where "s = s1 \<union> s2" and "s1 \<inter> s2 = {}" and "s1 \<in> x" and "s2 \<in> y"
+  by (insert h, auto simp:st_def)
+
+lemma stimesI: 
+  "\<lbrakk>s = s1 \<union> s2; s1 \<inter> s2 = {}; s1 \<in> x; s2 \<in> y\<rbrakk> \<Longrightarrow> s \<in> x * y"
+  by (auto simp:st_def)
 
-definition "m a v = {{M a v}}"
+lemma smem_upd: "(rset_of (x, y, mem, f)) \<in> (m a v)*r \<Longrightarrow> 
+                    (rset_of (x, y, mem(a := Some v'), f) \<in> (m a v')*r)"
+proof -
+  assume h: " rset_of (x, y, mem, f) \<in> m a v * r"
+  from h[unfolded rset_of.simps m_def]
+  have "prog_set x \<union> pc_set y \<union> mem_set mem \<union> faults_set f \<in> {{M a v}} * r" .
+  from stimes_sgD [OF this]
+  have h1: "prog_set x \<union> pc_set y \<union> mem_set mem \<union> faults_set f - {M a v} \<in> r"
+           "{M a v} \<subseteq> prog_set x \<union> pc_set y \<union> mem_set mem \<union> faults_set f" by auto
+  moreover have "prog_set x \<union> pc_set y \<union> mem_set mem \<union> faults_set f - {M a v} = 
+                 prog_set x \<union> pc_set y \<union> (mem_set mem  - {M a v}) \<union> faults_set f"
+    by (unfold cpn_set_def, auto)
+  ultimately have h0: "prog_set x \<union> pc_set y \<union> (mem_set mem - {M a v}) \<union> faults_set f \<in> r" 
+    by simp
+  from h1(2) and M_in_simp have "{M a v} \<subseteq> mem_set mem" by simp
+  from mem_set_upd [OF this] mem_set_disj[OF this]
+  have h2: "mem_set (mem(a \<mapsto> v')) = {M a v'} \<union> (mem_set mem - {M a v})" 
+           "{M a v'} \<inter> (mem_set mem - {M a v}) = {}" by auto
+  show ?thesis
+  proof -
+    have "mem_set (mem(a \<mapsto> v')) \<union>  prog_set x \<union> pc_set y \<union> faults_set f \<in> m a v' * r"
+    proof(rule stimesI[OF _ _ _ h0])
+      show "{M a v'} \<in> m a v'" by (unfold m_def, auto)
+    next
+      show "mem_set (mem(a \<mapsto> v')) \<union> prog_set x \<union> pc_set y \<union> faults_set f =
+             {M a v'} \<union> (prog_set x \<union> pc_set y \<union> (mem_set mem - {M a v}) \<union> faults_set f)"
+        apply (unfold h2(1))
+        by (smt Un_commute Un_insert_left Un_insert_right 
+             Un_left_commute 
+                  `prog_set x \<union> pc_set y \<union> mem_set mem \<union> 
+                  faults_set f - {M a v} =prog_set x \<union> pc_set y 
+                  \<union> (mem_set mem - {M a v}) \<union> faults_set f`)
+    next
+      from h2(2)
+      show "{M a v'} \<inter> (prog_set x \<union> pc_set y \<union> (mem_set mem - {M a v}) \<union> faults_set f) = {}"
+        by (unfold cpn_set_def, auto)
+    qed
+    thus ?thesis 
+      apply (unfold rset_of.simps)
+      by (metis `mem_set (mem(a \<mapsto> v')) 
+            \<union> prog_set x \<union> pc_set y \<union> faults_set f \<in> m a v' * r` 
+         stimes_comm sup_commute sup_left_commute)
+  qed
+qed
 
-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 spc_upd: "rset_of (x, i, y, z) \<in> pc i' * r \<Longrightarrow> 
+                rset_of (x, i'', y, z) \<in> pc i'' * r"
+proof -
+  assume h: "rset_of (x, i, y, z) \<in> pc i' * r"
+  from stimes_sgD [OF h[unfolded rset_of.simps pc_set_def pc_def]]
+  have h1: "prog_set x \<union> {At i} \<union> mem_set y \<union> faults_set z - {At i'} \<in> r" 
+           "{At i'} \<subseteq> prog_set x \<union> {At i} \<union> mem_set y \<union> faults_set z" by auto
+  from h1(2) have eq_i: "i' = i" by (unfold cpn_set_def, auto)
+  have "prog_set x \<union> {At i} \<union> mem_set y \<union> faults_set z - {At i'} =
+        prog_set x  \<union> mem_set y \<union> faults_set z "
+    apply (unfold eq_i)
+    by (metis (full_types) Un_insert_left Un_insert_right 
+         diff_pc_set faults_set_def insert_commute insert_is_Un 
+          pc_set_def sup_assoc sup_bot_left sup_commute)
+  with h1(1) have in_r: "prog_set x \<union>  mem_set y \<union> faults_set z \<in> r" by auto
+  show ?thesis
+  proof(unfold rset_of.simps, rule stimesI[OF _ _ _ in_r])
+    show "{At i''} \<in> pc i''" by (unfold pc_def pc_set_def, simp)
+  next
+    show "prog_set x \<union> pc_set i'' \<union> mem_set y \<union> faults_set z =
+    {At i''} \<union> (prog_set x \<union> mem_set y \<union> faults_set z)"
+      by (unfold pc_set_def, auto)
+  next
+    show "{At i''} \<inter> (prog_set x \<union> mem_set y \<union> faults_set z) = {}"
+      by (auto simp:cpn_set_def)
+  qed
+qed
+
+lemma condD: "s \<in> <b>*r \<Longrightarrow> b"
+  by (unfold st_def pasrt_def, auto)
+
+lemma condD1: "s \<in> <b>*r \<Longrightarrow> s \<in> r"
+  by (unfold st_def pasrt_def, auto)
+
+lemma hoare_dec_suc: "{(pc i * m a v) * <(v > 0)>} 
+                          i:[\<guillemotright>(Dec a e) ]:j  
+                      {pc j * m a (v - 1)}"
+proof(unfold Hoare_abc_def, clarify)
+  fix prog i' ab b r 
+  assume h: "rset_of (prog, i', ab, b) \<in> ((pc i * m a v) * <(0 < v)>) * (i :[ \<guillemotright>Dec a e ]: j) * r"
+                           (is "?r \<in> ?S")
+  show "\<exists>k. rset_of (run k (prog, i', ab, b)) \<in> (pc j * m a (v - 1)) * (i :[ \<guillemotright>Dec a e ]: j) * r"
+  proof -
+    from h [unfolded assemble_to.simps]
+    have h1: "?r \<in> pc i * {{C i (Dec a e)}} * m a v * <(0 < v)> *  <(j = i + 1)> * r"
+             "?r \<in>  m a v * pc i * {{C i (Dec a e)}} * <(0 < v)> *  <(j = i + 1)> * r"
+             "?r \<in>   <(0 < v)> *  <(j = i + 1)> * m a v * pc i * {{C i (Dec a e)}} * r"
+             "?r \<in>   <(j = i + 1)> * <(0 < v)> *   m a v * pc i * {{C i (Dec a e)}} * r"
+      by ((metis stimes_ac)+)
+    note h2 =  condD [OF h1(3)] condD[OF h1(4)] pcD[OF h1(1)] codeD[OF h1(1)] memD[OF h1(2)]
+    hence stp: "run 1 (prog, i', ab, b) = (prog, Suc i, ab(a \<mapsto> v - Suc 0), b)" (is "?x = ?y")
+      by (unfold run_def, auto)
+    have "rset_of ?x \<in> (pc j * m a (v - 1)) * (i :[ \<guillemotright>Dec a e ]: j) * r"
+    proof -
+      have "rset_of ?y \<in> (pc j * m a (v - 1)) * (i :[ \<guillemotright>Dec a e ]: j) * r"
+      proof -
+        from spc_upd[OF h1(1), of "Suc i"]
+        have "rset_of (prog, (Suc i), ab, b) \<in> 
+                m a v * pc (Suc i) * {{C i (Dec a e)}} * <(0 < v)> * <(j = i + 1)> * r" 
+          by (metis stimes_ac)
+        from smem_upd[OF this, of "v - (Suc 0)"]
+        have "rset_of ?y \<in> 
+           m a (v - Suc 0) * pc (Suc i) * {{C i (Dec a e)}} * <(0 < v)> * <(j = i + 1)> * r" .
+        hence "rset_of ?y \<in> <(0 < v)> *
+                (pc (Suc i) * m a (v - Suc 0)) * ({{C i (Dec a e)}} * <(j = i + 1)>) * r"
+          by (metis stimes_ac)
+        from condD1[OF this] 
+        have "rset_of ?y \<in> (pc (Suc i) * m a (v - Suc 0)) * ({{C i (Dec a e)}} * <(j = i + 1)>) * r" .
+        thus ?thesis
+          by (unfold h2(2) assemble_to.simps, simp)
+      qed
+      with stp show ?thesis by simp
+    qed
+    thus ?thesis by blast
+  qed
+qed
 
 lemma hoare_dec_fail: "{pc i * m a 0} 
                           i:[ \<guillemotright>(Dec a e) ]:j   
                        {pc e * m a 0}"
-  sorry
+proof(unfold Hoare_abc_def, clarify)
+  fix prog i' ab b r 
+  assume h: "rset_of (prog, i', ab, b) \<in> (pc i * m a 0) * (i :[ \<guillemotright>Dec a e ]: j) * r"
+                           (is "?r \<in> ?S")
+  show "\<exists>k. rset_of (run k (prog, i', ab, b)) \<in> (pc e * m a 0) * (i :[ \<guillemotright>Dec a e ]: j) * r"
+  proof -
+    from h [unfolded assemble_to.simps]
+    have h1: "?r \<in> pc i * {{C i (Dec a e)}} * m a 0  *  <(j = i + 1)> * r"
+             "?r \<in>  m a 0 * pc i * {{C i (Dec a e)}} *  <(j = i + 1)> * r"
+             "?r \<in> <(j = i + 1)> * m a 0 * pc i * {{C i (Dec a e)}} * r"
+      by ((metis stimes_ac)+)
+    note h2 =  condD [OF h1(3)]  pcD[OF h1(1)] codeD[OF h1(1)] memD[OF h1(2)]
+    hence stp: "run 1 (prog, i', ab, b) = (prog, e, ab, b)" (is "?x = ?y")
+      by (unfold run_def, auto)
+    have "rset_of ?x \<in> (pc e * m a 0) * (i :[ \<guillemotright>Dec a e ]: j) * r"
+    proof -
+      have "rset_of ?y \<in> (pc e * m a 0) * (i :[ \<guillemotright>Dec a e ]: j) * r"
+      proof -
+        from spc_upd[OF h1(1), of "e"]
+        have "rset_of ?y \<in> pc e * {{C i (Dec a e)}} * m a 0 * <(j = i + 1)> * r" .
+        thus ?thesis
+          by (unfold assemble_to.simps, metis stimes_ac)
+      qed
+      with stp show ?thesis by simp
+    qed
+    thus ?thesis by blast
+  qed
+qed
+
+lemma pasrtD_p: "\<lbrakk>{p*<b>} c {q}\<rbrakk> \<Longrightarrow> (b \<longrightarrow> {p} c {q})"
+  apply (unfold Hoare_abc_def pasrt_def, auto)
+  by (fold emp_def, simp add:emp_unit_r)
+
+lemma hoare_dec: "dec_fun v j e = (pc', v') \<Longrightarrow> 
+                    {pc i * m a v} 
+                       i:[ \<guillemotright>(Dec a e) ]:j   
+                    {pc pc' * m a v'}"
+proof -
+  assume "dec_fun v j e = (pc', v')"
+  thus  "{pc i * m a v} 
+                       i:[ \<guillemotright>(Dec a e) ]:j   
+                    {pc pc' * m a v'}"
+    apply (auto split:if_splits simp:dec_fun_def)
+    apply (insert hoare_dec_fail, auto)[1]
+    apply (insert hoare_dec_suc, auto)
+    apply (atomize)
+    apply (erule_tac x = i in allE, erule_tac x = a in allE,
+           erule_tac x = v in allE, erule_tac x = e in allE, erule_tac x = pc' in allE)
+    by (drule_tac pasrtD_p, clarify)
+qed
 
 lemma hoare_inc: "{pc i * m a v} 
                       i:[ \<guillemotright>(Inc a) ]:j   
-                  {pc (i+1) * m a (v + 1)}"
-  sorry
+                  {pc j * m a (v + 1)}"
+proof(unfold Hoare_abc_def, clarify)
+  fix prog i' ab b r 
+  assume h: "rset_of (prog, i', ab, b) \<in> (pc i * m a v) * (i :[ \<guillemotright>Inc a ]: j) * r"
+                           (is "?r \<in> ?S")
+  show "\<exists>k. rset_of (run k (prog, i', ab, b)) \<in> (pc j * m a (v + 1)) * (i :[ \<guillemotright>Inc a ]: j) * r"
+  proof -
+    from h [unfolded assemble_to.simps]
+    have h1: "?r \<in> pc i * {{C i (Inc a)}} * m a v *  <(j = i + 1)> * r"
+             "?r \<in>  m a v * pc i * {{C i (Inc a)}} * <(j = i + 1)> * r"
+             "?r \<in>   <(j = i + 1)> * m a v * pc i * {{C i (Inc a)}} * r"
+      by ((metis stimes_ac)+)
+    note h2 =  condD [OF h1(3)] pcD[OF h1(1)] codeD[OF h1(1)] memD[OF h1(2)]
+    hence stp: "run 1 (prog, i', ab, b) = (prog, Suc i, ab(a \<mapsto> Suc v), b)" (is "?x = ?y")
+      by (unfold run_def, auto)
+    have "rset_of ?x \<in> (pc j * m a (v + 1)) * (i :[ \<guillemotright>Inc a]: j) * r"
+    proof -
+      have "rset_of ?y \<in> (pc j * m a (v + 1)) * (i :[ \<guillemotright>Inc a ]: j) * r"
+      proof -
+        from spc_upd[OF h1(1), of "Suc i"]
+        have "rset_of (prog, (Suc i), ab, b) \<in> 
+                m a v * pc (Suc i) * {{C i (Inc a)}} * <(j = i + 1)> * r" 
+          by (metis stimes_ac)
+        from smem_upd[OF this, of "Suc v"]
+        have "rset_of ?y \<in> 
+           m a (v + 1) * pc (i + 1) * {{C i (Inc a)}} * <(j = i + 1)> * r" by simp
+        thus ?thesis
+          by (unfold h2(1) assemble_to.simps, metis stimes_ac)
+      qed
+      with stp show ?thesis by simp
+    qed
+    thus ?thesis by blast
+  qed
+qed
 
+lemma hoare_goto: "{pc i} 
+                      i:[ \<guillemotright>(Goto e) ]:j   
+                   {pc e}"
+proof(unfold Hoare_abc_def, clarify)
+  fix prog i' ab b r 
+  assume h: "rset_of (prog, i', ab, b) \<in> pc i * (i :[ \<guillemotright>Goto e ]: j) * r"
+                           (is "?r \<in> ?S")
+  show "\<exists>k. rset_of (run k (prog, i', ab, b)) \<in> pc e * (i :[ \<guillemotright>Goto e ]: j) * r"
+  proof -
+    from h [unfolded assemble_to.simps]
+    have h1: "?r \<in> pc i * {{C i (Goto e)}} *  <(j = i + 1)> * r"
+      by ((metis stimes_ac)+)
+    note h2 = pcD[OF h1(1)] codeD[OF h1(1)] 
+    hence stp: "run 1 (prog, i', ab, b) = (prog, e, ab, b)" (is "?x = ?y")
+      by (unfold run_def, auto)
+    have "rset_of ?x \<in> pc e * (i :[ \<guillemotright>Goto e]: j) * r"
+    proof -
+      from spc_upd[OF h1(1), of "e"] 
+      show ?thesis
+        by (unfold stp assemble_to.simps, metis stimes_ac)
+    qed
+    thus ?thesis by blast
+  qed
+qed
 
-interpretation foo: comm_monoid_mult "op * :: 'a set set => 'a set set => 'a set set" "{{}}::'a set set"
+no_notation stimes (infixr "*" 70)
+
+interpretation foo: comm_monoid_mult 
+  "stimes :: 'a set set => 'a set set => 'a set set" "emp::'a set set"
 apply(default)
 apply(simp add: stimes_assoc)
 apply(simp add: stimes_comm)
@@ -148,6 +472,8 @@
 done
 
 
+notation stimes (infixr "*" 70)
+
 (*used by simplifier for numbers *)
 thm mult_cancel_left
 
@@ -156,18 +482,18 @@
 apply(default)
 *)
 
-lemma frame: "{p} c {q} \<Longrightarrow> \<forall> r. {p * r} c {q * r}"
+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)
+apply(metis 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)
+  apply(metis stimes_ac)
   done
 
 lemma run_add: "run (n1 + n2) s = run n1 (run n2 s)"
@@ -202,39 +528,173 @@
     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 stimes_simp: "s \<in> x * y = (\<exists> s1 s2. (s = s1 \<union> s2 \<and> s1 \<inter> s2 = {} \<and> s1 \<in> x \<and> s2 \<in> y))"
+by (metis (lifting) stimesE stimesI)
 
-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)
+lemma hoare_seq: 
+  "\<lbrakk>\<forall> i j. {pc i * p} i:[c1]:j {pc j * q}; 
+    \<forall> j k. {pc j * q} j:[c2]:k {pc k * r}\<rbrakk> \<Longrightarrow>  {pc i * p} i:[(c1 ; c2)]:k {pc k *r}"
 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 = {}")
+  assume h: "\<forall>i j. {pc i * p} i :[ c1 ]: j {pc j * q}" "\<forall> j k. {pc j * q} j:[c2]:k {pc k * r}"
+  show "{pc i * p} i:[(c1 ; c2)]:k {pc k *r}"
+  proof(subst Hoare_abc_def, clarify)
+    fix a aa ab b ra
+    assume "rset_of (a, aa, ab, b) \<in> (pc i * p) * (i :[ (c1 ; c2) ]: k) * ra"
+    hence "rset_of (a, aa, ab, b) \<in> (i :[ (c1 ; c2) ]: k) * (pc i * p * ra)" (is "?s \<in> ?X * ?Y")
+      by (metis stimes_ac)
+    from stimesE[OF this] obtain s1 s2 where
+      sp: "rset_of(a, aa, ab, b) = s1 \<union> s2" "s1 \<inter> s2 = {}" "s1 \<in> ?X" "s2 \<in> ?Y" by blast
+    from sp (3) obtain j' where 
+      "s1 \<in> (i:[c1]:j') * (j':[c2]:k)" (is "s1 \<in> ?Z")
+      by (auto simp:assemble_to.simps)
+    from stimesI[OF sp(1, 2) this sp(4)]
+    have "?s \<in>  (pc i * p) * (i :[ c1 ]: j') * (j' :[ c2 ]: k) * ra" by (metis stimes_ac)
+    from h(1)[unfolded Hoare_abc_def, rule_format, OF this]
+    obtain ka where 
+      "rset_of (run ka (a, aa, ab, b)) \<in> (pc j' * q) * (j' :[ c2 ]: k) * ((i :[ c1 ]: j') * ra)" 
+      sorry
+    from h(2)[unfolded Hoare_abc_def, rule_format, OF this]
+    obtain kb where 
+      "rset_of (run kb (run ka (a, aa, ab, b)))
+      \<in>  (pc k * r) * (j' :[ c2 ]: k) * (i :[ c1 ]: j') * ra" by blast
+    hence h3: "rset_of (run (kb + ka) (a, aa, ab, b))
+      \<in> pc k * r * (j' :[ c2 ]: k) * ((i :[ c1 ]: j') * ra)" 
+      sorry
+    hence "rset_of (run (kb + ka) (a, aa, ab, b)) \<in> pc k * r * (i :[ (c1 ; c2) ]: k) * ra"
+    proof -
+      have "rset_of (run (kb + ka) (a, aa, ab, b)) \<in> (i :[ (c1 ; c2) ]: k) * (pc k * r * ra)"
       proof -
-        { fix s 
-          assume "s \<in> ?X*?Y"
-          then obtain s1 s2 where h1: "s1 \<in> ?X" by (unfold stimes_def, auto)
-          
-        }
+        from h3 have "rset_of (run (kb + ka) (a, aa, ab, b))
+          \<in> ((j' :[ c2 ]: k) * ((i :[ c1 ]: j'))) * (pc k * r *  ra)"
+          by (metis stimes_ac)
+        then obtain 
+          s1 s2 where h4: "rset_of (run (kb + ka) (a, aa, ab, b)) = s1 \<union> s2"
+          " s1 \<inter> s2 = {}" "s1 \<in> (j' :[ c2 ]: k) * (i :[ c1 ]: j')"
+          "s2 \<in>  pc k * r * ra" by (rule stimesE, blast)
+        from h4(3) have "s1 \<in> (i :[ (c1 ; c2) ]: k)"
+          sorry
+        from stimesI [OF h4(1, 2) this h4(4)]
+        show ?thesis .
       qed
-    } thus ?thesis by (auto intro!:union_unique)
+      thus ?thesis by (metis stimes_ac)
+    qed
+    thus "\<exists>ka. rset_of (run ka (a, aa, ab, b)) \<in> (pc k * r) * (i :[ (c1 ; c2) ]: k) * ra"
+      by (metis stimes_ac)
   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
   
+lemma hoare_local: 
+  "\<forall> l i j. {pc i*p} i:[c(l)]:j {pc j * q} 
+  \<Longrightarrow> {pc i * p} i:[Local c]:j {pc j * q}"
+proof -
+  assume h: "\<forall> l i j. {pc i*p} i:[c(l)]:j {pc j * q} "
+  show "{pc i * p} i:[Local c]:j {pc j * q}"
+  proof(unfold assemble_to.simps Hoare_abc_def, clarify)
+    fix a aa ab b r
+    assume h1: "rset_of (a, aa, ab, b) \<in> (pc i * p) * (\<Union>l. i :[ c l ]: j) * r"
+    hence "rset_of (a, aa, ab, b) \<in> (\<Union>l. i :[ c l ]: j) * (pc i * p * r)" 
+      by (metis stimes_ac)
+    then obtain s1 s2 l 
+      where "rset_of (a, aa, ab, b) = s1 \<union> s2"
+                "s1 \<inter> s2 = {}"
+                "s1 \<in> (i :[ c l ]: j)"
+                "s2 \<in> pc i * p * r"
+      by (rule stimesE, auto)
+    from stimesI[OF this]
+    have "rset_of (a, aa, ab, b) \<in> (pc i * p) * (i :[ c l ]: j) * r" 
+      by (metis stimes_ac)
+    from h[unfolded Hoare_abc_def, rule_format, OF this]
+    obtain k where "rset_of (run k (a, aa, ab, b)) \<in> (i :[ c l ]: j) * (pc j * q * r)" 
+      sorry
+    then obtain s1 s2
+      where h3: "rset_of (run k (a, aa, ab, b)) = s1 \<union> s2"
+                " s1 \<inter> s2 = {}" "s1 \<in> (\<Union> l. (i :[ c l ]: j))" "s2 \<in> pc j * q * r" 
+      by(rule stimesE, auto)
+    from stimesI[OF this]
+    show "\<exists>k. rset_of (run k (a, aa, ab, b)) \<in> (pc j * q) * (\<Union>l. i :[ c l ]: j) * r"
+      by (metis stimes_ac)
+  qed
+qed
 
- 
+lemma move_pure: "{p*<b>} c {q} = (b \<longrightarrow> {p} c {q})"
+proof(unfold Hoare_abc_def, default, clarify)
+  fix prog i' mem ft r
+  assume h: "\<forall>s r. rset_of s \<in> (p * <b>) * c * r \<longrightarrow> (\<exists>k. rset_of (run k s) \<in> q * c * r)"
+            "b" "rset_of (prog, i', mem, ft) \<in> p * c * r"
+  show "\<exists>k. rset_of (run k (prog, i', mem, ft)) \<in> q * c * r"
+  proof(rule h(1)[rule_format])
+    have "(p * <b>) * c * r = <b> * p * c * r" by (metis stimes_ac)
+    moreover have "rset_of (prog, i', mem, ft) \<in> \<dots>"
+    proof(rule stimesI[OF _ _ _ h(3)])
+      from h(2) show "{} \<in> <b>" by (auto simp:pasrt_def)
+    qed auto
+    ultimately show "rset_of (prog, i', mem, ft) \<in> (p * <b>) * c * r"
+      by (simp)
+  qed
+next
+  assume h: "b \<longrightarrow> (\<forall>s r. rset_of s \<in> p * c * r \<longrightarrow> (\<exists>k. rset_of (run k s) \<in> q * c * r))"
+  show "\<forall>s r. rset_of s \<in> (p * <b>) * c * r \<longrightarrow> (\<exists>k. rset_of (run k s) \<in> q * c * r)"
+  proof -
+    { fix s r 
+      assume "rset_of s \<in> (p * <b>) * c * r"
+      hence h1: "rset_of s \<in> <b> * p * c * r" by (metis stimes_ac)
+      have "(\<exists>k. rset_of (run k s) \<in> q * c * r)"
+      proof(rule h[rule_format])
+        from condD[OF h1] show b .
+      next
+        from condD1[OF h1] show "rset_of s \<in> p * c * r" .
+      qed
+    } thus ?thesis by blast
+  qed
+qed
+
+lemma precond_ex: "{\<Union> x. p x} c {q} = (\<forall> x. {p x} c {q})"
+proof(unfold Hoare_abc_def, default, clarify)
+  fix x prog i' mem ft r
+  assume h: "\<forall>s r. rset_of s \<in> UNION UNIV p * c * r \<longrightarrow> (\<exists>k. rset_of (run k s) \<in> q * c * r)"
+            "rset_of (prog, i', mem, ft) \<in> p x * c * r"
+  show "\<exists>k. rset_of (run k (prog, i', mem, ft)) \<in> q * c * r"
+  proof(rule h[rule_format])
+    from h(2) show "rset_of (prog, i', mem, ft) \<in> UNION UNIV p * c * r" by (auto simp:stimes_def)
+  qed
+next
+  assume h: "\<forall>x s r. rset_of s \<in> p x * c * r \<longrightarrow> (\<exists>k. rset_of (run k s) \<in> q * c * r)"
+  show "\<forall>s r. rset_of s \<in> UNION UNIV p * c * r \<longrightarrow> (\<exists>k. rset_of (run k s) \<in> q * c * r)"
+  proof -
+    { fix s r
+      assume "rset_of s \<in> UNION UNIV p * c * r"
+      then obtain x where "rset_of s \<in> p x * c * r" 
+        by (unfold st_def, auto, metis)
+      hence "(\<exists>k. rset_of (run k s) \<in> q * c * r)"
+        by(rule h[rule_format])
+    } thus ?thesis by blast
+  qed
+qed
+
+lemma pre_stren: "\<lbrakk>{p} c {q}; r \<subseteq> p\<rbrakk> \<Longrightarrow> {r} c {q}"
+proof(unfold Hoare_abc_def, clarify)
+  fix prog i' mem ft r'
+  assume h: "\<forall>s r. rset_of s \<in> p * c * r \<longrightarrow> (\<exists>k. rset_of (run k s) \<in> q * c * r)"
+            " r \<subseteq> p" " rset_of (prog, i', mem, ft) \<in> r * c * r'"
+  show "\<exists>k. rset_of (run k (prog, i', mem, ft)) \<in> q * c * r'"
+  proof(rule h(1)[rule_format])
+    from stimes_mono[OF h(2), of "c * r'"] h(3)
+    show "rset_of (prog, i', mem, ft) \<in> p * c * r'" by auto
+  qed
+qed
+
+lemma post_weaken: "\<lbrakk>{p} c {q}; q \<subseteq> r\<rbrakk> \<Longrightarrow> {p} c {r}"
+proof(unfold Hoare_abc_def, clarify)
+  fix prog i' mem ft r'
+  assume h: "\<forall>s r. rset_of s \<in> p * c * r \<longrightarrow> (\<exists>k. rset_of (run k s) \<in> q * c * r)"
+            " q \<subseteq> r" "rset_of (prog, i', mem, ft) \<in> p * c * r'"
+  show "\<exists>k. rset_of (run k (prog, i', mem, ft)) \<in> r * c * r'"
+  proof -
+    from h(1)[rule_format, OF h(3)]
+    obtain k where "rset_of (run k (prog, i', mem, ft)) \<in> q * c * r'" by auto
+    moreover from h(2) have "\<dots> \<subseteq> r * c * r'" by (metis stimes_mono)
+    ultimately show ?thesis by auto
+  qed
+qed
+
 end
diff -r d8e6f0798e23 -r 49dcc0b9b0b3 paper.pdf
Binary file paper.pdf has changed
diff -r d8e6f0798e23 -r 49dcc0b9b0b3 thys/Recursive.thy
--- a/thys/Recursive.thy	Wed Mar 27 09:47:02 2013 +0000
+++ b/thys/Recursive.thy	Wed Mar 27 13:16:37 2013 +0000
@@ -2519,23 +2519,32 @@
 qed
 
 lemma recursive_compile_to_tm_correct2: 
-  assumes  compile: "rec_ci recf = (ap, ary, fp)"
-  and termi: " terminate recf args"
+  assumes termi: " terminate recf args"
   shows "\<exists> stp m l. steps0 (Suc 0, [Bk, Bk], <args>) (tm_of_rec recf) stp = 
                      (0, Bk\<up>Suc (Suc m), Oc\<up>Suc (rec_exec recf args) @ Bk\<up>l)"
-using recursive_compile_to_tm_correct1[of recf ap ary fp args "tm_of (ap [+] dummy_abc (length args))" "[]" 0]
-assms param_pattern[of recf args ap ary fp]
-by(simp add: exp_suc replicate_Suc[THEN sym] del: replicate_Suc tm_of_rec_def)
+proof(case_tac "rec_ci recf", simp add: tm_of_rec.simps)
+  fix ap ar fp
+  assume "rec_ci recf = (ap, ar, fp)"
+  thus "\<exists>stp m l. steps0 (Suc 0, [Bk, Bk], <args>) 
+    (tm_of (ap [+] dummy_abc ar) @ shift (mopup ar) (listsum (layout_of (ap [+] dummy_abc ar)))) stp =
+    (0, Bk # Bk # Bk \<up> m, Oc # Oc \<up> rec_exec recf args @ Bk \<up> l)"
+    using recursive_compile_to_tm_correct1[of recf ap ar fp args "tm_of (ap [+] dummy_abc (length args))" "[]" 0]
+      assms param_pattern[of recf args ap ar fp]
+    by(simp add: replicate_Suc[THEN sym] replicate_Suc_iff_anywhere del: replicate_Suc tm_of_rec_def, 
+      simp add: exp_suc del: replicate_Suc)
+qed
 
 lemma recursive_compile_to_tm_correct3: 
-  assumes compile: "rec_ci recf = (ap, ary, fp)"
-  and termi: "terminate recf args"
-  shows "{\<lambda> (l, r). l = [Bk, Bk] \<and> r = <args>} (tm_of_rec recf) 
-         {\<lambda> (l, r). \<exists> m i. l = Bk\<up>(Suc (Suc m)) \<and> r = Oc\<up>Suc (rec_exec recf args) @ Bk \<up> i}"
-using recursive_compile_to_tm_correct2[of recf ap ary fp args] assms
-apply(simp add: Hoare_halt_def, auto)
-apply(rule_tac x = stp in exI, simp)
-done
+  assumes termi: "terminate recf args"
+  shows "{\<lambda> tp. tp =([Bk, Bk], <args>)} (tm_of_rec recf) 
+         {\<lambda> tp. \<exists> k l. tp = (Bk\<up> k, <rec_exec recf args> @ Bk \<up> l)}"
+using recursive_compile_to_tm_correct2[OF assms]
+apply(auto simp add: Hoare_halt_def)
+apply(rule_tac x = stp in exI)
+apply(auto simp add: tape_of_nat_abv)
+apply(rule_tac x = "Suc (Suc m)" in exI)
+apply(simp)
+done 
 
 lemma [simp]:
   "list_all (\<lambda>(acn, s). s \<le> Suc (Suc (Suc (Suc (Suc (Suc (2 * n))))))) xs \<Longrightarrow>