Binary file Literature/logics/1_sepAlgTactics.pdf has changed
Binary file Literature/logics/Tuer09.pdf has changed
Binary file Literature/logics/asl-short.pdf has changed
Binary file Literature/logics/septacs.pdf has changed
--- a/Paper/Paper.thy Wed Mar 27 13:24:41 2013 +0000
+++ b/Paper/Paper.thy Fri Mar 29 01:36:45 2013 +0000
@@ -3,7 +3,9 @@
imports "../thys/UTM" "../thys/Abacus_Defs"
begin
-
+(*
+value "map (steps (1,[],[Oc]) ([(L,0),(L,2),(R,2),(R,0)],0)) [0 ..< 4]"
+*)
hide_const (open) s
@@ -69,7 +71,7 @@
exponent ("_\<^bsup>_\<^esup>") and
tcopy ("copy") and
tape_of ("\<langle>_\<rangle>") and
- tm_comp ("_ \<oplus> _") and
+ tm_comp ("_ ; _") and
DUMMY ("\<^raw:\mbox{$\_\!\_\,$}>") and
inv_begin0 ("I\<^isub>0") and
inv_begin1 ("I\<^isub>1") and
@@ -530,7 +532,7 @@
blank cell to the right list; otherwise we have to remove the
head from the left-list and prepend it to the right list. Similarly
in the fourth clause for a right move action. The @{term Nop} operation
- leaves the the tape unchanged.
+ leaves the tape unchanged.
%Note that our treatment of the tape is rather ``unsymmetric''---we
%have the convention that the head of the right list is where the
@@ -599,12 +601,12 @@
The @{text 0}-state is special in that it will be used as the
``halting state''. There are no instructions for the @{text
0}-state, but it will always perform a @{term Nop}-operation and
- remain in the @{text 0}-state. Unlike Asperti and Riccioti
- \cite{AspertiRicciotti12}, we have chosen a very concrete
+ remain in the @{text 0}-state.
+ We have chosen a very concrete
representation for Turing machine programs, because when constructing a universal
Turing machine, we need to define a coding function for programs.
- This can be directly done for our programs-as-lists, but is
- slightly more difficult for the functions used by Asperti and Ricciotti.
+ %This can be directly done for our programs-as-lists, but is
+ %slightly more difficult for the functions used by Asperti and Ricciotti.
Given a program @{term p}, a state
and the cell being scanned by the head, we need to fetch
@@ -639,38 +641,7 @@
state, and the third that every next-state is one of the states mentioned in
the program or being the @{text 0}-state.
- We need to be able to sequentially compose Turing machine programs. Given our
- concrete representation, this is relatively straightforward, if
- slightly fiddly. We use the following two auxiliary functions:
-
- \begin{center}
- \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
- @{thm (lhs) shift.simps} @{text "\<equiv>"} @{thm (rhs) shift.simps}\\
- @{thm (lhs) adjust_simps} @{text "\<equiv>"} @{thm (rhs) adjust_simps}\\
- \end{tabular}
- \end{center}
-
- \noindent
- The first adds @{text n} to all states, except the @{text 0}-state,
- thus moving all ``regular'' states to the segment starting at @{text
- n}; the second adds @{term "Suc(length p div 2)"} to the @{text
- 0}-state, thus redirecting all references to the ``halting state''
- to the first state after the program @{text p}. With these two
- functions in place, we can define the \emph{sequential composition}
- of two Turing machine programs @{text "p\<^isub>1"} and @{text "p\<^isub>2"} as
-
- \begin{center}
- @{thm tm_comp.simps[where ?p1.0="p\<^isub>1" and ?p2.0="p\<^isub>2", THEN eq_reflection]}
- \end{center}
-
- \noindent
- %This means @{text "p\<^isub>1"} is executed first. Whenever it originally
- %transitioned to the @{text 0}-state, it will in the composed program transition to the starting
- %state of @{text "p\<^isub>2"} instead. All the states of @{text "p\<^isub>2"}
- %have been shifted in order to make sure that the states of the composed
- %program @{text "p\<^isub>1 \<oplus> p\<^isub>2"} still only ``occupy''
- %an initial segment of the natural numbers.
-
+
A \emph{configuration} @{term c} of a Turing machine is a state
together with a tape. This is written as @{text "(s, (l, r))"}. We
say a configuration \emph{is final} if @{term "s = (0::nat)"} and we
@@ -714,6 +685,65 @@
actually halt, but rather transitions to the @{text 0}-state (the
final state) and remains there performing @{text Nop}-actions until
@{text n} is reached.
+
+
+ We often need to restrict tapes to be in standard form, which means
+ the left list of the tape is either empty or only contains @{text "Bk"}s, and
+ the right list contains some ``clusters'' of @{text "Oc"}s separated by single
+ blanks. To make this formal we define the following overloaded function
+ encoding natural numbers into lists of @{term "Oc"}s and @{term Bk}s.
+ %
+ \begin{equation}
+ \mbox{\begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
+ @{thm (lhs) nats2tape(6)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(6)}\\
+ @{thm (lhs) nats2tape(4)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(4)}\\
+ \end{tabular}\hspace{6mm}
+ \begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
+ @{thm (lhs) nats2tape(1)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(1)}\\
+ @{thm (lhs) nats2tape(2)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(2)}\\
+ @{thm (lhs) nats2tape(3)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(3)}
+ \end{tabular}}\label{standard}
+ \end{equation}
+ %
+ \noindent
+ A \emph{standard tape} is then of the form @{text "(Bk\<^isup>k,\<langle>[n\<^isub>1,...,n\<^isub>m]\<rangle> @ Bk\<^isup>l)"} for some @{text k},
+ @{text l}
+ and @{text "n\<^bsub>1...m\<^esub>"}. Note that the head in a standard tape ``points'' to the
+ leftmost @{term "Oc"} on the tape. Note also that the natural number @{text 0}
+ is represented by a single filled cell on a standard tape, @{text 1} by two filled cells and so on.
+
+
+ We need to be able to sequentially compose Turing machine programs. Given our
+ concrete representation, this is relatively straightforward, if
+ slightly fiddly. We use the following two auxiliary functions:
+
+ \begin{center}
+ \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
+ @{thm (lhs) shift.simps} @{text "\<equiv>"} @{thm (rhs) shift.simps}\\
+ @{thm (lhs) adjust_simps} @{text "\<equiv>"} @{thm (rhs) adjust_simps}\\
+ \end{tabular}
+ \end{center}
+
+ \noindent
+ The first adds @{text n} to all states, except the @{text 0}-state,
+ thus moving all ``regular'' states to the segment starting at @{text
+ n}; the second adds @{term "Suc(length p div 2)"} to the @{text
+ 0}-state, thus redirecting all references to the ``halting state''
+ to the first state after the program @{text p}. With these two
+ functions in place, we can define the \emph{sequential composition}
+ of two Turing machine programs @{text "p\<^isub>1"} and @{text "p\<^isub>2"} as
+
+ \begin{center}
+ @{thm tm_comp.simps[where ?p1.0="p\<^isub>1" and ?p2.0="p\<^isub>2", THEN eq_reflection]}
+ \end{center}
+
+ \noindent
+ %This means @{text "p\<^isub>1"} is executed first. Whenever it originally
+ %transitioned to the @{text 0}-state, it will in the composed program transition to the starting
+ %state of @{text "p\<^isub>2"} instead. All the states of @{text "p\<^isub>2"}
+ %have been shifted in order to make sure that the states of the composed
+ %program @{text "p\<^isub>1 \<oplus> p\<^isub>2"} still only ``occupy''
+ %an initial segment of the natural numbers.
\begin{figure}[t]
\begin{center}
@@ -830,30 +860,7 @@
\end{figure}
- We often need to restrict tapes to be in standard form, which means
- the left list of the tape is either empty or only contains @{text "Bk"}s, and
- the right list contains some ``clusters'' of @{text "Oc"}s separated by single
- blanks. To make this formal we define the following overloaded function
- encoding natural numbers into lists of @{term "Oc"}s and @{term Bk}s.
- %
- \begin{equation}
- \mbox{\begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
- @{thm (lhs) nats2tape(6)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(6)}\\
- @{thm (lhs) nats2tape(4)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(4)}\\
- \end{tabular}\hspace{6mm}
- \begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
- @{thm (lhs) nats2tape(1)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(1)}\\
- @{thm (lhs) nats2tape(2)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(2)}\\
- @{thm (lhs) nats2tape(3)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(3)}
- \end{tabular}}\label{standard}
- \end{equation}
- %
- \noindent
- A \emph{standard tape} is then of the form @{text "(Bk\<^isup>k,\<langle>[n\<^isub>1,...,n\<^isub>m]\<rangle> @ Bk\<^isup>l)"} for some @{text k},
- @{text l}
- and @{text "n\<^bsub>1...m\<^esub>"}. Note that the head in a standard tape ``points'' to the
- leftmost @{term "Oc"} on the tape. Note also that the natural number @{text 0}
- is represented by a single filled cell on a standard tape, @{text 1} by two filled cells and so on.
+
Before we can prove the undecidability of the halting problem for
our Turing machines working on standard tapes, we have to analyse
@@ -1061,7 +1068,7 @@
\end{center}
\caption{The invariants @{term inv_begin0},\ldots,@{term inv_begin4} are for the states of
@{term tcopy_begin}. Below, the invariants only for the starting and halting states of
- @{term tcopy_loop} and @{term tcopy_end} are shown. In each invariant the parameter
+ @{term tcopy_loop} and @{term tcopy_end} are shown. In each invariant, the parameter
@{term n} stands for the number
of @{term Oc}s with which the Turing machine is started.}\label{invbegin}
\end{figure}
@@ -1392,7 +1399,7 @@
The main point of recursive functions is that we can relatively
easily construct a universal Turing machine via a universal
function. This is different from Norrish \cite{Norrish11} who gives a universal
- function for Church numbers, and also from Asperti and Ricciotti
+ function for the lambda-calculus, and also from Asperti and Ricciotti
\cite{AspertiRicciotti12} who construct a universal Turing machine
directly, but for simulating Turing machines with a more restricted alphabet.
Unlike Norrish \cite{Norrish11}, we need to represent recursive functions
@@ -1514,7 +1521,7 @@
containing the inconsistency was introduced in the fourth edition
\cite{BoolosFourth}). The central
idea about Turing machines is that when started with standard tapes
- they compute a partial arithmetic function. The inconsitency arises
+ they compute a partial arithmetic function. The inconsistency arises
when they define the case when this function should \emph{not} return a
result. Boolos at al write in Chapter 3, Page 32:
@@ -1538,7 +1545,7 @@
simulated Turing machine, and @{text "nstd(conf(m, x, t))"} returns @{text 1}
if the tape content is non-standard. If either one evaluates to
something that is not zero, then @{text "stdh(m, x, t)"} will be not zero, because of
- the $+$-operation. One the same page, a function @{text "halt(m, x)"} is defined
+ the $+$-operation. On the same page, a function @{text "halt(m, x)"} is defined
in terms of @{text stdh} for computing the steps the Turing machine needs to
execute before it halts (in case it halts at all). According to this definition, the simulated
Turing machine will continue to run after entering the @{text 0}-state
@@ -1562,9 +1569,9 @@
\noindent
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
+ non-standard tape @{term "([Oc, Bk], [])"} 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.
+ 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}.
@@ -1641,9 +1648,11 @@
\<or> \<not>P"}. For reasoning about computability we need to formalise a
concrete model of computations. We could have followed Norrish
\cite{Norrish11} using the $\lambda$-calculus as the starting point for computability theory,
- but then we would have to reimplement his infrastructure for
- reducing $\lambda$-terms on the ML-level. We would still need to
- connect his work to Turing machines for proofs that make essential use of them
+ but then we would still have
+ %to reimplement his infrastructure for
+ %reducing $\lambda$-terms on the ML-level.
+ %We would still need
+ to connect his work to Turing machines for proofs that make essential use of them
(for example the undecidability proof for Wang's tiling problem \cite{Robinson71}).
We therefore have formalised Turing machines in the first place and the main
@@ -1724,7 +1733,7 @@
introduced a more primitive specification logic, on which
Hoare-rules can be provided for special cases. It remains to be
seen whether their specification logic for assembly code can make it
- easier to reason about our Turing programs. That would be an
+ easier to reason about our Turing programs. Myreen ??? That would be an
attractive result, because Turing machine programs are very much
like assembly programs and it would connect some very classic work on
Turing machines to very cutting-edge work on machine code
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Tests/abacus-1.thy Fri Mar 29 01:36:45 2013 +0000
@@ -0,0 +1,757 @@
+header {*
+ {\em abacus} a kind of register machine
+*}
+
+theory abacus
+imports Main StateMonad
+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
+
+
+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 = {})"
+
+declare splits.simps [simp del]
+
+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]
+
+notation stimes (infixr "*" 70)
+
+lemma stimes_comm: "(p::('a set set)) * q = q * p"
+ by (unfold st_def, auto)
+
+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 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 st_def, auto)
+
+lemma stimes_left_commute:
+ "(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}"
+
+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" (infixr ";" 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
+
+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) =
+ 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"
+
+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"
+
+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))))"
+
+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)
+
+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)
+
+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 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}"
+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 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
+
+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)
+apply(simp add: emp_def[symmetric])
+done
+
+
+notation stimes (infixr "*" 70)
+
+(*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(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(metis 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 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 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: "\<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 -
+ 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 (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
+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 code_exI: "\<lbrakk>\<And>l. {p} c l * c' {q}\<rbrakk> \<Longrightarrow> {p} (\<Union> l. c l) * c' {q}"
+proof(unfold Hoare_abc_def, default, clarify)
+ fix prog i' mem ft r
+ assume h: "\<And>l. \<forall>s r. rset_of s \<in> p * (c l * c') * r \<longrightarrow> (\<exists>k. rset_of (run k s) \<in> q * (c l * c') * r)"
+ "rset_of (prog, i', mem, ft) \<in> p * (UNION UNIV c * c') * r"
+ show " \<exists>k. rset_of (run k (prog, i', mem, ft)) \<in> q * (UNION UNIV c * c') * r"
+ proof -
+ from h(2) obtain l where "rset_of (prog, i', mem, ft) \<in> p * (c l * c') * r"
+ apply (unfold st_def, auto)
+ by metis
+ from h(1)[rule_format, OF this]
+ obtain k where " rset_of (run k (prog, i', mem, ft)) \<in> q * (c l * c') * r" by blast
+ thus ?thesis by (unfold st_def, auto, metis)
+ qed
+qed
+
+lemma code_exIe: "\<lbrakk>\<And>l. {p} c l{q}\<rbrakk> \<Longrightarrow> {p} \<Union> l. (c l) {q}"
+proof -
+ assume "\<And>l. {p} c l {q}"
+ thus "{p} \<Union>l. c l {q}"
+ by(rule code_exI[where c'= "emp", unfolded emp_unit_r])
+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
+
+definition "clear a =
+ Local (\<lambda> start. (Local (\<lambda> exit. Label start; \<guillemotright>Dec a exit; \<guillemotright> Goto start; Label exit)))"
+
+lemma "{pc i * m a v} i:[clear a]:j {pc j*m a 0}"
+proof (unfold clear_def, rule hoare_local, default+)
+ fix l i j
+ show "{pc i * m a v} i :[ Local (\<lambda>exit. Label l ; \<guillemotright>Dec a exit ; \<guillemotright>Goto l ; Label exit) ]: j
+ {pc j * m a 0}"
+ proof(rule hoare_local, default+)
+ fix la i j
+ show "{pc i * m a v} i :[ (Label l ; \<guillemotright>Dec a la ; \<guillemotright>Goto l ; Label la) ]: j {pc j * m a 0}"
+ proof(subst assemble_to.simps, rule code_exIe)
+ have "\<And>j'. {pc i * m a v} (j' :[ (\<guillemotright>Dec a la ; \<guillemotright>Goto l ; Label la) ]: j) * (i :[ Label l ]: j')
+ {pc j * m a 0}"
+ proof(subst assemble_to.simps, rule code_exI)
+ fix j' j'a
+ show "{pc i * m a v}
+ ((j' :[ \<guillemotright>Dec a la ]: j'a) * (j'a :[ (\<guillemotright>Goto l ; Label la) ]: j)) * (i :[ Label l ]: j')
+ {pc j * m a 0}"
+ proof(unfold assemble_to.simps)
+ have "{pc i * m a v}
+ ((\<Union>j'. ({{C j'a (Goto l)}} * <(j' = j'a + 1)>) * ({{C j' (Dec a la)}} * <(j'a = j' + 1)>)
+ * <(j' = j \<and> j = la)>)) *
+ <(i = j' \<and> j' = l)>
+ {pc j * m a 0}"
+ proof(rule code_exI, fold assemble_to.simps)
+ qed
+ thus "{pc i * m a v}
+ (({{C j' (Dec a la)}} * <(j'a = j' + 1)>) *
+ (\<Union>j'. ({{C j'a (Goto l)}} * <(j' = j'a + 1)>) * <(j' = j \<and> j = la)>)) *
+ <(i = j' \<and> j' = l)>
+ {pc j * m a 0}" sorry
+ qed
+ qed
+ thus "\<And>j'. {pc i * m a v} (i :[ Label l ]: j') * (j' :[ (\<guillemotright>Dec a la ; \<guillemotright>Goto l ; Label la) ]: j)
+ {pc j * m a 0}" by (metis stimes_ac)
+ qed
+ qed
+qed
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Tests/abacus-2.thy Fri Mar 29 01:36:45 2013 +0000
@@ -0,0 +1,732 @@
+header {*
+ {\em abacus} a kind of register machine
+*}
+
+theory abacus
+imports Main "../Separation_Algebra/Sep_Tactics"
+begin
+
+instantiation set :: (type)sep_algebra
+begin
+
+definition set_zero_def: "0 = {}"
+
+definition plus_set_def: "s1 + s2 = s1 \<union> s2"
+
+definition sep_disj_set_def: "sep_disj s1 s2 = (s1 \<inter> s2 = {})"
+
+lemmas set_ins_def = sep_disj_set_def plus_set_def set_zero_def
+
+instance
+ apply(default)
+ apply(simp add:set_ins_def)
+ apply(simp add:sep_disj_set_def plus_set_def set_zero_def)
+ apply (metis inf_commute)
+ apply(simp add:sep_disj_set_def plus_set_def set_zero_def)
+ apply(simp add:sep_disj_set_def plus_set_def set_zero_def)
+ apply (metis sup_commute)
+ apply(simp add:sep_disj_set_def plus_set_def set_zero_def)
+ apply (metis (lifting) Un_assoc)
+ apply(simp add:sep_disj_set_def plus_set_def set_zero_def)
+ apply (metis (lifting) Int_Un_distrib Un_empty inf_sup_distrib1 sup_eq_bot_iff)
+ apply(simp add:sep_disj_set_def plus_set_def set_zero_def)
+ by (metis (lifting) Int_Un_distrib Int_Un_distrib2 sup_eq_bot_iff)
+end
+
+
+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
+
+datatype apg =
+ Instr abc_inst
+ | Label nat
+ | Seq apg apg
+ | Local "(nat \<Rightarrow> apg)"
+
+notation Local (binder "L " 10)
+
+abbreviation prog_instr :: "abc_inst \<Rightarrow> apg" ("\<guillemotright>_" [61] 61)
+where "\<guillemotright>i \<equiv> Instr i"
+
+abbreviation prog_seq :: "apg \<Rightarrow> apg \<Rightarrow> apg" (infixr ";" 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
+
+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) =
+ prog_set prog \<union> pc_set pc \<union> mem_set m \<union> faults_set faults"
+
+definition "sg e = (\<lambda> s. s = e)"
+
+definition "pc l = sg (pc_set l)"
+
+definition "m a v =sg ({M a v})"
+
+declare rset_of.simps[simp del]
+
+type_synonym assert = "aresource set \<Rightarrow> bool"
+
+primrec assemble_to :: "apg \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> assert"
+ where
+ "assemble_to (Instr ai) i j = (sg ({C i ai}) ** \<langle>(j = i + 1)\<rangle>)" |
+ "assemble_to (Seq p1 p2) i j = (EXS j'. (assemble_to p1 i j') ** (assemble_to p2 j' j))" |
+ "assemble_to (Local fp) i j = (EXS l. (assemble_to (fp l) i j))" |
+ "assemble_to (Label l) i j = \<langle>(i = j \<and> j = l)\<rangle>"
+
+abbreviation asmb_to :: "nat \<Rightarrow> apg \<Rightarrow> nat \<Rightarrow> assert" ("_ :[ _ ]: _" [60, 60, 60] 60)
+ where "i :[ apg ]: j \<equiv> assemble_to apg i j"
+
+lemma stimes_sgD: "(sg x ** q) s \<Longrightarrow> q (s - x) \<and> x \<subseteq> s"
+ apply(erule_tac sep_conjE)
+ apply(unfold set_ins_def sg_def)
+ by (metis Diff_Int2 Diff_Int_distrib2 Diff_Un Diff_cancel
+ Diff_empty Diff_idemp Diff_triv Int_Diff Un_Diff
+ Un_Diff_cancel inf_commute inf_idem sup_bot_right sup_commute sup_ge2)
+
+lemma pcD: "(pc i ** r) (rset_of (prog, i', mem, fault))
+ \<Longrightarrow> i' = i"
+proof -
+ assume "(pc i ** r) (rset_of (prog, i', mem, fault))"
+ 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: "(pc i ** sg {C i inst} ** r) (rset_of (prog, pos, mem, fault))
+ \<Longrightarrow> prog pos = Some inst"
+proof -
+ assume "(pc i ** sg {C i inst} ** r) (rset_of (prog, pos, mem, fault))"
+ thus ?thesis
+ apply(sep_subst pcD)
+ apply(unfold sep_conj_def set_ins_def sg_def rset_of.simps cpn_set_def)
+ by auto
+qed
+
+lemma memD: "((m a v) ** r) (rset_of (prog, pos, mem, fault)) \<Longrightarrow> mem a = Some v"
+proof -
+ assume "((m a v) ** r) (rset_of (prog, pos, mem, fault))"
+ 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. (p**c**r) (rset_of s) \<longrightarrow>
+ (\<exists> k. ((q ** c ** r) (rset_of (run k s)))))"
+
+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)
+
+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 smem_upd: "((m a v) ** r) (rset_of (x, y, mem, f)) \<Longrightarrow>
+ ((m a v') ** r) (rset_of (x, y, mem(a := Some v'), f))"
+proof -
+ have eq_s:"
+ (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)
+ assume "(m a v \<and>* r) (rset_of (x, y, mem, f))"
+ from this[unfolded rset_of.simps m_def]
+ have h: "(sg {M a v} \<and>* r) (prog_set x \<union> pc_set y \<union> mem_set mem \<union> faults_set f)" .
+ hence h0: "r (prog_set x \<union> pc_set y \<union> (mem_set mem - {M a v}) \<union> faults_set f)"
+ by(sep_drule stimes_sgD, clarify, unfold eq_s, auto)
+ from h M_in_simp have "{M a v} \<subseteq> mem_set mem"
+ by(sep_drule stimes_sgD, auto)
+ 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 "(m a v' ** r) (mem_set (mem(a \<mapsto> v')) \<union> prog_set x \<union> pc_set y \<union> faults_set f)"
+ proof(rule sep_conjI)
+ from h0 show "r (prog_set x \<union> pc_set y \<union> (mem_set mem - {M a v}) \<union> faults_set f)" .
+ next
+ show "m a v' ({M a v'})" by (unfold m_def sg_def, simp)
+ next
+ show "mem_set (mem(a \<mapsto> v')) \<union> prog_set x \<union> pc_set y \<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 h2(1) set_ins_def eq_s, auto)
+ next
+ from h2(2)
+ show " {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 set_ins_def, auto)
+ qed
+ thus ?thesis
+ apply (unfold rset_of.simps)
+ by (metis sup_commute sup_left_commute)
+ qed
+qed
+
+lemma pc_dest: "(pc i') (pc_set i) \<Longrightarrow> i = i'"
+ sorry
+
+lemma spc_upd: "(pc i' ** r) (rset_of (x, i, y, z)) \<Longrightarrow>
+ (pc i'' ** r) (rset_of (x, i'', y, z))"
+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}"
+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 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
+
+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)
+apply(simp add: emp_def[symmetric])
+done
+
+
+notation stimes (infixr "*" 70)
+
+(*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(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(metis 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 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 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: "\<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 -
+ 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 (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
+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 code_exI: "\<lbrakk>\<And>l. {p} c l * c' {q}\<rbrakk> \<Longrightarrow> {p} (\<Union> l. c l) * c' {q}"
+proof(unfold Hoare_abc_def, default, clarify)
+ fix prog i' mem ft r
+ assume h: "\<And>l. \<forall>s r. rset_of s \<in> p * (c l * c') * r \<longrightarrow> (\<exists>k. rset_of (run k s) \<in> q * (c l * c') * r)"
+ "rset_of (prog, i', mem, ft) \<in> p * (UNION UNIV c * c') * r"
+ show " \<exists>k. rset_of (run k (prog, i', mem, ft)) \<in> q * (UNION UNIV c * c') * r"
+ proof -
+ from h(2) obtain l where "rset_of (prog, i', mem, ft) \<in> p * (c l * c') * r"
+ apply (unfold st_def, auto)
+ by metis
+ from h(1)[rule_format, OF this]
+ obtain k where " rset_of (run k (prog, i', mem, ft)) \<in> q * (c l * c') * r" by blast
+ thus ?thesis by (unfold st_def, auto, metis)
+ qed
+qed
+
+lemma code_exIe: "\<lbrakk>\<And>l. {p} c l{q}\<rbrakk> \<Longrightarrow> {p} \<Union> l. (c l) {q}"
+proof -
+ assume "\<And>l. {p} c l {q}"
+ thus "{p} \<Union>l. c l {q}"
+ by(rule code_exI[where c'= "emp", unfolded emp_unit_r])
+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
+
+definition "clear a = (L start exit. Label start; \<guillemotright>Dec a exit; \<guillemotright> Goto start; Label exit)"
+
+lemma "{pc i * m a v} i:[clear a]:j {pc j*m a 0}"
+proof (unfold clear_def, rule hoare_local, default+)
+ fix l i j
+ show "{pc i * m a v} i :[ (L exit. Label l ; \<guillemotright>Dec a exit ; \<guillemotright>Goto l ; Label exit) ]: j
+ {pc j * m a 0}"
+ proof(rule hoare_local, default+)
+ fix la i j
+ show "{pc i * m a v} i :[ (Label l ; \<guillemotright>Dec a la ; \<guillemotright>Goto l ; Label la) ]: j {pc j * m a 0}"
+ proof(subst assemble_to.simps, rule code_exIe)
+ have "\<And>j'. {pc i * m a v} (j' :[ (\<guillemotright>Dec a la ; \<guillemotright>Goto l ; Label la) ]: j) * (i :[ Label l ]: j')
+ {pc j * m a 0}"
+ proof(subst assemble_to.simps, rule code_exI)
+ fix j' j'a
+ show "{pc i * m a v}
+ ((j' :[ \<guillemotright>Dec a la ]: j'a) * (j'a :[ (\<guillemotright>Goto l ; Label la) ]: j)) * (i :[ Label l ]: j')
+ {pc j * m a 0}"
+ proof(unfold assemble_to.simps)
+ have "{pc i * m a v}
+ ((\<Union>j'. ({{C j'a (Goto l)}} * <(j' = j'a + 1)>) * ({{C j' (Dec a la)}} * <(j'a = j' + 1)>)
+ * <(j' = j \<and> j = la)>)) *
+ <(i = j' \<and> j' = l)>
+ {pc j * m a 0}"
+ proof(rule code_exI, fold assemble_to.simps, unfold assemble_to.simps(4))
+ thm assemble_to.simps
+ qed
+ thus "{pc i * m a v}
+ (({{C j' (Dec a la)}} * <(j'a = j' + 1)>) *
+ (\<Union>j'. ({{C j'a (Goto l)}} * <(j' = j'a + 1)>) * <(j' = j \<and> j = la)>)) *
+ <(i = j' \<and> j' = l)>
+ {pc j * m a 0}" sorry
+ qed
+ qed
+ thus "\<And>j'. {pc i * m a v} (i :[ Label l ]: j') * (j' :[ (\<guillemotright>Dec a la ; \<guillemotright>Goto l ; Label la) ]: j)
+ {pc j * m a 0}" by (metis stimes_ac)
+ qed
+ qed
+qed
+
+end
Binary file paper.pdf has changed