# HG changeset patch
# User nipkow
# Date 1306962484 -7200
# Node ID faba4800b00bc2d60fdc34a964723806b055757f
# Parent  9ed5d8ad8fa048565682eea48bbc7d2ba6a18bac# Parent  631dd866b2847aff408d59ec75a43feb545905cb
merged

diff -r 9ed5d8ad8fa0 -r faba4800b00b src/HOL/HOLCF/IMP/Denotational.thy
--- a/src/HOL/HOLCF/IMP/Denotational.thy	Wed Jun 01 19:50:59 2011 +0200
+++ b/src/HOL/HOLCF/IMP/Denotational.thy	Wed Jun 01 23:08:04 2011 +0200
@@ -5,17 +5,7 @@
 
 header "Denotational Semantics of Commands in HOLCF"
 
-theory Denotational imports HOLCF "~~/src/HOL/IMP/Natural" begin
-
-text {* Disable conflicting syntax from HOL Map theory. *}
-
-no_syntax
-  "_maplet"  :: "['a, 'a] => maplet"             ("_ /|->/ _")
-  "_maplets" :: "['a, 'a] => maplet"             ("_ /[|->]/ _")
-  ""         :: "maplet => maplets"             ("_")
-  "_Maplets" :: "[maplet, maplets] => maplets" ("_,/ _")
-  "_MapUpd"  :: "['a ~=> 'b, maplets] => 'a ~=> 'b" ("_/'(_')" [900,0]900)
-  "_Map"     :: "maplets => 'a ~=> 'b"            ("(1[_])")
+theory Denotational imports HOLCF "~~/src/HOL/IMP/Big_Step" begin
 
 subsection "Definition"
 
@@ -25,13 +15,13 @@
 
 primrec D :: "com => state discr -> state lift"
 where
-  "D(\<SKIP>) = (LAM s. Def(undiscr s))"
-| "D(X :== a) = (LAM s. Def((undiscr s)[X \<mapsto> a(undiscr s)]))"
+  "D(SKIP) = (LAM s. Def(undiscr s))"
+| "D(X ::= a) = (LAM s. Def((undiscr s)(X := aval a (undiscr s))))"
 | "D(c0 ; c1) = (dlift(D c1) oo (D c0))"
-| "D(\<IF> b \<THEN> c1 \<ELSE> c2) =
-        (LAM s. if b (undiscr s) then (D c1)\<cdot>s else (D c2)\<cdot>s)"
-| "D(\<WHILE> b \<DO> c) =
-        fix\<cdot>(LAM w s. if b (undiscr s) then (dlift w)\<cdot>((D c)\<cdot>s)
+| "D(IF b THEN c1 ELSE c2) =
+        (LAM s. if bval b (undiscr s) then (D c1)\<cdot>s else (D c2)\<cdot>s)"
+| "D(WHILE b DO c) =
+        fix\<cdot>(LAM w s. if bval b (undiscr s) then (dlift w)\<cdot>((D c)\<cdot>s)
                       else Def(undiscr s))"
 
 subsection
@@ -47,32 +37,31 @@
     "(dlift f\<cdot>l = Def y) = (\<exists>x. l = Def x \<and> f\<cdot>(Discr x) = Def y)"
   by (simp add: dlift_def split: lift.split)
 
-lemma eval_implies_D: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t ==> D c\<cdot>(Discr s) = (Def t)"
-  apply (induct set: evalc)
-        apply simp_all
-   apply (subst fix_eq)
-   apply simp
-  apply (subst fix_eq)
-  apply simp
-  done
+lemma eval_implies_D: "(c,s) \<Rightarrow> t ==> D c\<cdot>(Discr s) = (Def t)"
+apply (induct rule: big_step_induct)
+      apply (auto)
+ apply (subst fix_eq)
+ apply simp
+apply (subst fix_eq)
+apply simp
+done
 
-lemma D_implies_eval: "!s t. D c\<cdot>(Discr s) = (Def t) --> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
-  apply (induct c)
-      apply simp
-     apply simp
-    apply force
-   apply (simp (no_asm))
-   apply force
-  apply (simp (no_asm))
-  apply (rule fix_ind)
-    apply (fast intro!: adm_lemmas adm_chfindom ax_flat)
-   apply (simp (no_asm))
-  apply (simp (no_asm))
-  apply safe
-  apply fast
-  done
+lemma D_implies_eval: "!s t. D c\<cdot>(Discr s) = (Def t) --> (c,s) \<Rightarrow> t"
+apply (induct c)
+    apply fastsimp
+   apply fastsimp
+  apply force
+ apply (simp (no_asm))
+ apply force
+apply (simp (no_asm))
+apply (rule fix_ind)
+  apply (fast intro!: adm_lemmas adm_chfindom ax_flat)
+ apply (simp (no_asm))
+apply (simp (no_asm))
+apply force
+done
 
-theorem D_is_eval: "(D c\<cdot>(Discr s) = (Def t)) = (\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t)"
-  by (fast elim!: D_implies_eval [rule_format] eval_implies_D)
+theorem D_is_eval: "(D c\<cdot>(Discr s) = (Def t)) = ((c,s) \<Rightarrow> t)"
+by (fast elim!: D_implies_eval [rule_format] eval_implies_D)
 
 end
diff -r 9ed5d8ad8fa0 -r faba4800b00b src/HOL/HOLCF/IMP/HoareEx.thy
--- a/src/HOL/HOLCF/IMP/HoareEx.thy	Wed Jun 01 19:50:59 2011 +0200
+++ b/src/HOL/HOLCF/IMP/HoareEx.thy	Wed Jun 01 23:08:04 2011 +0200
@@ -8,7 +8,7 @@
 theory HoareEx imports Denotational begin
 
 text {*
-  An example from the HOLCF paper by Müller, Nipkow, Oheimb, Slotosch
+  An example from the HOLCF paper by Mueller, Nipkow, Oheimb, Slotosch
   \cite{MuellerNvOS99}.  It demonstrates fixpoint reasoning by showing
   the correctness of the Hoare rule for while-loops.
 *}
@@ -17,10 +17,10 @@
 
 definition
   hoare_valid :: "[assn, com, assn] => bool"  ("|= {(1_)}/ (_)/ {(1_)}" 50) where
-  "|= {A} c {B} = (\<forall>s t. A s \<and> D c $(Discr s) = Def t --> B t)"
+  "|= {P} c {Q} = (\<forall>s t. P s \<and> D c $(Discr s) = Def t --> Q t)"
 
 lemma WHILE_rule_sound:
-    "|= {A} c {A} ==> |= {A} \<WHILE> b \<DO> c {\<lambda>s. A s \<and> \<not> b s}"
+    "|= {A} c {A} ==> |= {A} WHILE b DO c {\<lambda>s. A s \<and> \<not> bval b s}"
   apply (unfold hoare_valid_def)
   apply (simp (no_asm))
   apply (rule fix_ind)
diff -r 9ed5d8ad8fa0 -r faba4800b00b src/HOL/IMP/AExp.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/AExp.thy	Wed Jun 01 23:08:04 2011 +0200
@@ -0,0 +1,85 @@
+header "Arithmetic and Boolean Expressions"
+
+theory AExp imports Main begin
+
+subsection "Arithmetic Expressions"
+
+type_synonym name = string
+type_synonym val = int
+type_synonym state = "name \<Rightarrow> val"
+
+datatype aexp = N int | V name | Plus aexp aexp
+
+fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val" where
+"aval (N n) _ = n" |
+"aval (V x) s = s x" |
+"aval (Plus a1 a2) s = aval a1 s + aval a2 s"
+
+
+value "aval (Plus (V ''x'') (N 5)) (%x. if x = ''x'' then 7 else 0)"
+
+fun lookup :: "(string * val)list \<Rightarrow> string \<Rightarrow> val" where
+"lookup ((x,i)#xis) y = (if x=y then i else lookup xis y)"
+
+value "aval (Plus (V ''x'') (N 5)) (lookup [(''x'',7)])"
+
+value "aval (Plus (V ''x'') (N 5)) (lookup [(''y'',7)])"
+
+
+subsection "Optimization"
+
+text{* Evaluate constant subsexpressions: *}
+
+fun asimp_const :: "aexp \<Rightarrow> aexp" where
+"asimp_const (N n) = N n" |
+"asimp_const (V x) = V x" |
+"asimp_const (Plus a1 a2) =
+  (case (asimp_const a1, asimp_const a2) of
+    (N n1, N n2) \<Rightarrow> N(n1+n2) |
+    (a1',a2') \<Rightarrow> Plus a1' a2')"
+
+theorem aval_asimp_const[simp]:
+  "aval (asimp_const a) s = aval a s"
+apply(induct a)
+apply (auto split: aexp.split)
+done
+
+text{* Now we also eliminate all occurrences 0 in additions. The standard
+method: optimized versions of the constructors: *}
+
+fun plus :: "aexp \<Rightarrow> aexp \<Rightarrow> aexp" where
+"plus (N i1) (N i2) = N(i1+i2)" |
+"plus (N i) a = (if i=0 then a else Plus (N i) a)" |
+"plus a (N i) = (if i=0 then a else Plus a (N i))" |
+"plus a1 a2 = Plus a1 a2"
+
+text ""
+code_thms plus
+code_thms plus
+
+(* FIXME: dropping subsumed code eqns?? *)
+lemma aval_plus[simp]:
+  "aval (plus a1 a2) s = aval a1 s + aval a2 s"
+apply(induct a1 a2 rule: plus.induct)
+apply simp_all (* just for a change from auto *)
+done
+code_thms plus
+
+fun asimp :: "aexp \<Rightarrow> aexp" where
+"asimp (N n) = N n" |
+"asimp (V x) = V x" |
+"asimp (Plus a1 a2) = plus (asimp a1) (asimp a2)"
+
+text{* Note that in @{const asimp_const} the optimized constructor was
+inlined. Making it a separate function @{const plus} improves modularity of
+the code and the proofs. *}
+
+value "asimp (Plus (Plus (N 0) (N 0)) (Plus (V ''x'') (N 0)))"
+
+theorem aval_asimp[simp]:
+  "aval (asimp a) s = aval a s"
+apply(induct a)
+apply simp_all
+done
+
+end
diff -r 9ed5d8ad8fa0 -r faba4800b00b src/HOL/IMP/ASM.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/ASM.thy	Wed Jun 01 23:08:04 2011 +0200
@@ -0,0 +1,51 @@
+header "Arithmetic Stack Machine and Compilation"
+
+theory ASM imports AExp begin
+
+subsection "Arithmetic Stack Machine"
+
+datatype ainstr = LOADI val | LOAD string | ADD
+
+type_synonym stack = "val list"
+
+abbreviation "hd2 xs == hd(tl xs)"
+abbreviation "tl2 xs == tl(tl xs)"
+
+text{* \noindent Abbreviations are transparent: they are unfolded after
+parsing and folded back again before printing. Internally, they do not
+exist. *}
+
+fun aexec1 :: "ainstr \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack" where
+"aexec1 (LOADI n) _ stk  =  n # stk" |
+"aexec1 (LOAD n) s stk  =  s(n) # stk" |
+"aexec1  ADD _ stk  =  (hd2 stk + hd stk) # tl2 stk"
+
+fun aexec :: "ainstr list \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack" where
+"aexec [] _ stk = stk" |
+"aexec (i#is) s stk = aexec is s (aexec1 i s stk)"
+
+value "aexec [LOADI 5, LOAD ''y'', ADD]
+  (lookup[(''x'',42), (''y'',43)]) [50]"
+
+lemma aexec_append[simp]:
+  "aexec (is1@is2) s stk = aexec is2 s (aexec is1 s stk)"
+apply(induct is1 arbitrary: stk)
+apply (auto)
+done
+
+
+subsection "Compilation"
+
+fun acomp :: "aexp \<Rightarrow> ainstr list" where
+"acomp (N n) = [LOADI n]" |
+"acomp (V x) = [LOAD x]" |
+"acomp (Plus e1 e2) = acomp e1 @ acomp e2 @ [ADD]"
+
+value "acomp (Plus (Plus (V ''x'') (N 1)) (V ''z''))"
+
+theorem aexec_acomp[simp]: "aexec (acomp a) s stk = aval a s # stk"
+apply(induct a arbitrary: stk)
+apply (auto)
+done
+
+end
diff -r 9ed5d8ad8fa0 -r faba4800b00b src/HOL/IMP/BExp.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/BExp.thy	Wed Jun 01 23:08:04 2011 +0200
@@ -0,0 +1,69 @@
+theory BExp imports AExp begin
+
+subsection "Boolean Expressions"
+
+datatype bexp = B bool | Not bexp | And bexp bexp | Less aexp aexp
+
+fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where
+"bval (B bv) _ = bv" |
+"bval (Not b) s = (\<not> bval b s)" |
+"bval (And b1 b2) s = (if bval b1 s then bval b2 s else False)" |
+"bval (Less a1 a2) s = (aval a1 s < aval a2 s)"
+
+value "bval (Less (V ''x'') (Plus (N 3) (V ''y'')))
+  (lookup [(''x'',3),(''y'',1)])"
+
+
+subsection "Optimization"
+
+text{* Optimized constructors: *}
+
+fun less :: "aexp \<Rightarrow> aexp \<Rightarrow> bexp" where
+"less (N n1) (N n2) = B(n1 < n2)" |
+"less a1 a2 = Less a1 a2"
+
+lemma [simp]: "bval (less a1 a2) s = (aval a1 s < aval a2 s)"
+apply(induct a1 a2 rule: less.induct)
+apply simp_all
+done
+
+fun "and" :: "bexp \<Rightarrow> bexp \<Rightarrow> bexp" where
+"and (B True) b = b" |
+"and b (B True) = b" |
+"and (B False) b = B False" |
+"and b (B False) = B False" |
+"and b1 b2 = And b1 b2"
+
+lemma bval_and[simp]: "bval (and b1 b2) s = (bval b1 s \<and> bval b2 s)"
+apply(induct b1 b2 rule: and.induct)
+apply simp_all
+done
+
+fun not :: "bexp \<Rightarrow> bexp" where
+"not (B True) = B False" |
+"not (B False) = B True" |
+"not b = Not b"
+
+lemma bval_not[simp]: "bval (not b) s = (~bval b s)"
+apply(induct b rule: not.induct)
+apply simp_all
+done
+
+text{* Now the overall optimizer: *}
+
+fun bsimp :: "bexp \<Rightarrow> bexp" where
+"bsimp (Less a1 a2) = less (asimp a1) (asimp a2)" |
+"bsimp (And b1 b2) = and (bsimp b1) (bsimp b2)" |
+"bsimp (Not b) = not(bsimp b)" |
+"bsimp (B bv) = B bv"
+
+value "bsimp (And (Less (N 0) (N 1)) b)"
+
+value "bsimp (And (Less (N 1) (N 0)) (B True))"
+
+theorem "bval (bsimp b) s = bval b s"
+apply(induct b)
+apply simp_all
+done
+
+end
diff -r 9ed5d8ad8fa0 -r faba4800b00b src/HOL/IMP/Big_Step.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Big_Step.thy	Wed Jun 01 23:08:04 2011 +0200
@@ -0,0 +1,243 @@
+(* Author: Gerwin Klein, Tobias Nipkow *)
+
+theory Big_Step imports Com begin
+
+subsection "Big-Step Semantics of Commands"
+
+inductive
+  big_step :: "com \<times> state \<Rightarrow> state \<Rightarrow> bool" (infix "\<Rightarrow>" 55)
+where
+Skip:    "(SKIP,s) \<Rightarrow> s" |
+Assign:  "(x ::= a,s) \<Rightarrow> s(x := aval a s)" |
+Semi:    "\<lbrakk> (c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2;  (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>
+          (c\<^isub>1;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
+
+IfTrue:  "\<lbrakk> bval b s;  (c\<^isub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
+         (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
+IfFalse: "\<lbrakk> \<not>bval b s;  (c\<^isub>2,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
+         (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
+
+WhileFalse: "\<not>bval b s \<Longrightarrow> (WHILE b DO c,s) \<Rightarrow> s" |
+WhileTrue:  "\<lbrakk> bval b s\<^isub>1;  (c,s\<^isub>1) \<Rightarrow> s\<^isub>2;  (WHILE b DO c, s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>
+             (WHILE b DO c, s\<^isub>1) \<Rightarrow> s\<^isub>3"
+
+schematic_lemma ex: "(''x'' ::= N 5; ''y'' ::= V ''x'', s) \<Rightarrow> ?t"
+apply(rule Semi)
+apply(rule Assign)
+apply simp
+apply(rule Assign)
+done
+
+thm ex[simplified]
+
+text{* We want to execute the big-step rules: *}
+
+code_pred big_step .
+
+text{* For inductive definitions we need command
+       \texttt{values} instead of \texttt{value}. *}
+
+values "{t. (SKIP, lookup[]) \<Rightarrow> t}"
+
+text{* We need to translate the result state into a list
+to display it. *}
+
+values "{map t [''x''] |t. (SKIP, lookup [(''x'',42)]) \<Rightarrow> t}"
+
+values "{map t [''x''] |t. (''x'' ::= N 2, lookup [(''x'',42)]) \<Rightarrow> t}"
+
+values "{map t [''x'',''y''] |t.
+  (WHILE Less (V ''x'') (V ''y'') DO (''x'' ::= Plus (V ''x'') (N 5)),
+   lookup [(''x'',0),(''y'',13)]) \<Rightarrow> t}"
+
+
+text{* Proof automation: *}
+
+declare big_step.intros [intro]
+
+text{* The standard induction rule 
+@{thm [display] big_step.induct [no_vars]} *}
+
+thm big_step.induct
+
+text{* A customized induction rule for (c,s) pairs: *}
+
+lemmas big_step_induct = big_step.induct[split_format(complete)]
+thm big_step_induct
+text {*
+@{thm [display] big_step_induct [no_vars]}
+*}
+
+
+subsection "Rule inversion"
+
+text{* What can we deduce from @{prop "(SKIP,s) \<Rightarrow> t"} ?
+That @{prop "s = t"}. This is how we can automatically prove it: *}
+
+inductive_cases skipE[elim!]: "(SKIP,s) \<Rightarrow> t"
+thm skipE
+
+text{* This is an \emph{elimination rule}. The [elim] attribute tells auto,
+blast and friends (but not simp!) to use it automatically; [elim!] means that
+it is applied eagerly.
+
+Similarly for the other commands: *}
+
+inductive_cases AssignE[elim!]: "(x ::= a,s) \<Rightarrow> t"
+thm AssignE
+inductive_cases SemiE[elim!]: "(c1;c2,s1) \<Rightarrow> s3"
+thm SemiE
+inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) \<Rightarrow> t"
+thm IfE
+
+inductive_cases WhileE[elim]: "(WHILE b DO c,s) \<Rightarrow> t"
+thm WhileE
+text{* Only [elim]: [elim!] would not terminate. *}
+
+text{* An automatic example: *}
+
+lemma "(IF b THEN SKIP ELSE SKIP, s) \<Rightarrow> t \<Longrightarrow> t = s"
+by blast
+
+text{* Rule inversion by hand via the ``cases'' method: *}
+
+lemma assumes "(IF b THEN SKIP ELSE SKIP, s) \<Rightarrow> t"
+shows "t = s"
+proof-
+  from assms show ?thesis
+  proof cases  --"inverting assms"
+    case IfTrue thm IfTrue
+    thus ?thesis by blast
+  next
+    case IfFalse thus ?thesis by blast
+  qed
+qed
+
+
+subsection "Command Equivalence"
+
+text {*
+  We call two statements @{text c} and @{text c'} equivalent wrt.\ the
+  big-step semantics when \emph{@{text c} started in @{text s} terminates
+  in @{text s'} iff @{text c'} started in the same @{text s} also terminates
+  in the same @{text s'}}. Formally:
+*}
+abbreviation
+  equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" (infix "\<sim>" 50) where
+  "c \<sim> c' == (\<forall>s t. (c,s) \<Rightarrow> t  =  (c',s) \<Rightarrow> t)"
+
+text {*
+Warning: @{text"\<sim>"} is the symbol written \verb!\ < s i m >! (without spaces).
+
+  As an example, we show that loop unfolding is an equivalence
+  transformation on programs:
+*}
+lemma unfold_while:
+  "(WHILE b DO c) \<sim> (IF b THEN c; WHILE b DO c ELSE SKIP)" (is "?w \<sim> ?iw")
+proof -
+  -- "to show the equivalence, we look at the derivation tree for"
+  -- "each side and from that construct a derivation tree for the other side"
+  { fix s t assume "(?w, s) \<Rightarrow> t"
+    -- "as a first thing we note that, if @{text b} is @{text False} in state @{text s},"
+    -- "then both statements do nothing:"
+    { assume "\<not>bval b s"
+      hence "t = s" using `(?w,s) \<Rightarrow> t` by blast
+      hence "(?iw, s) \<Rightarrow> t" using `\<not>bval b s` by blast
+    }
+    moreover
+    -- "on the other hand, if @{text b} is @{text True} in state @{text s},"
+    -- {* then only the @{text WhileTrue} rule can have been used to derive @{text "(?w, s) \<Rightarrow> t"} *}
+    { assume "bval b s"
+      with `(?w, s) \<Rightarrow> t` obtain s' where
+        "(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto
+      -- "now we can build a derivation tree for the @{text IF}"
+      -- "first, the body of the True-branch:"
+      hence "(c; ?w, s) \<Rightarrow> t" by (rule Semi)
+      -- "then the whole @{text IF}"
+      with `bval b s` have "(?iw, s) \<Rightarrow> t" by (rule IfTrue)
+    }
+    ultimately
+    -- "both cases together give us what we want:"
+    have "(?iw, s) \<Rightarrow> t" by blast
+  }
+  moreover
+  -- "now the other direction:"
+  { fix s t assume "(?iw, s) \<Rightarrow> t"
+    -- "again, if @{text b} is @{text False} in state @{text s}, then the False-branch"
+    -- "of the @{text IF} is executed, and both statements do nothing:"
+    { assume "\<not>bval b s"
+      hence "s = t" using `(?iw, s) \<Rightarrow> t` by blast
+      hence "(?w, s) \<Rightarrow> t" using `\<not>bval b s` by blast
+    }
+    moreover
+    -- "on the other hand, if @{text b} is @{text True} in state @{text s},"
+    -- {* then this time only the @{text IfTrue} rule can have be used *}
+    { assume "bval b s"
+      with `(?iw, s) \<Rightarrow> t` have "(c; ?w, s) \<Rightarrow> t" by auto
+      -- "and for this, only the Semi-rule is applicable:"
+      then obtain s' where
+        "(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto
+      -- "with this information, we can build a derivation tree for the @{text WHILE}"
+      with `bval b s`
+      have "(?w, s) \<Rightarrow> t" by (rule WhileTrue)
+    }
+    ultimately
+    -- "both cases together again give us what we want:"
+    have "(?w, s) \<Rightarrow> t" by blast
+  }
+  ultimately
+  show ?thesis by blast
+qed
+
+text {* Luckily, such lengthy proofs are seldom necessary.  Isabelle can
+prove many such facts automatically.  *}
+
+lemma 
+  "(WHILE b DO c) \<sim> (IF b THEN c; WHILE b DO c ELSE SKIP)"
+by blast
+
+lemma triv_if:
+  "(IF b THEN c ELSE c) \<sim> c"
+by blast
+
+lemma commute_if:
+  "(IF b1 THEN (IF b2 THEN c11 ELSE c12) ELSE c2) 
+   \<sim> 
+   (IF b2 THEN (IF b1 THEN c11 ELSE c2) ELSE (IF b1 THEN c12 ELSE c2))"
+by blast
+
+
+subsection "Execution is deterministic"
+
+text {* This proof is automatic. *}
+theorem big_step_determ: "\<lbrakk> (c,s) \<Rightarrow> t; (c,s) \<Rightarrow> u \<rbrakk> \<Longrightarrow> u = t"
+apply (induct arbitrary: u rule: big_step.induct)
+apply blast+
+done
+
+text {*
+  This is the proof as you might present it in a lecture. The remaining
+  cases are simple enough to be proved automatically:
+*}
+theorem
+  "(c,s) \<Rightarrow> t  \<Longrightarrow>  (c,s) \<Rightarrow> t'  \<Longrightarrow>  t' = t"
+proof (induct arbitrary: t' rule: big_step.induct)
+  -- "the only interesting case, @{text WhileTrue}:"
+  fix b c s s1 t t'
+  -- "The assumptions of the rule:"
+  assume "bval b s" and "(c,s) \<Rightarrow> s1" and "(WHILE b DO c,s1) \<Rightarrow> t"
+  -- {* Ind.Hyp; note the @{text"\<And>"} because of arbitrary: *}
+  assume IHc: "\<And>t'. (c,s) \<Rightarrow> t' \<Longrightarrow> t' = s1"
+  assume IHw: "\<And>t'. (WHILE b DO c,s1) \<Rightarrow> t' \<Longrightarrow> t' = t"
+  -- "Premise of implication:"
+  assume "(WHILE b DO c,s) \<Rightarrow> t'"
+  with `bval b s` obtain s1' where
+      c: "(c,s) \<Rightarrow> s1'" and
+      w: "(WHILE b DO c,s1') \<Rightarrow> t'"
+    by auto
+  from c IHc have "s1' = s1" by blast
+  with w IHw show "t' = t" by blast
+qed blast+ -- "prove the rest automatically"
+
+
+end
diff -r 9ed5d8ad8fa0 -r faba4800b00b src/HOL/IMP/Com.thy
--- a/src/HOL/IMP/Com.thy	Wed Jun 01 19:50:59 2011 +0200
+++ b/src/HOL/IMP/Com.thy	Wed Jun 01 23:08:04 2011 +0200
@@ -1,33 +1,12 @@
-(*  Title:        HOL/IMP/Com.thy
-    Author:       Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
-    Author:       Gerwin Klein
-*)
-
-header "Syntax of Commands"
-
-theory Com imports Main begin
+header "IMP --- A Simple Imperative Language"
 
-typedecl loc 
-  -- "an unspecified (arbitrary) type of locations 
-      (adresses/names) for variables"
-      
-type_synonym val = nat -- "or anything else, @{text nat} used in examples"
-type_synonym state = "loc \<Rightarrow> val"
-type_synonym aexp = "state \<Rightarrow> val"
-type_synonym bexp = "state \<Rightarrow> bool"
-  -- "arithmetic and boolean expressions are not modelled explicitly here,"
-  -- "they are just functions on states"
+theory Com imports BExp begin
 
 datatype
-  com = SKIP                    
-      | Assign loc aexp         ("_ :== _ " 60)
-      | Semi   com com          ("_; _"  [60, 60] 10)
-      | Cond   bexp com com     ("IF _ THEN _ ELSE _"  60)
-      | While  bexp com         ("WHILE _ DO _"  60)
-
-notation (latex)
-  SKIP  ("\<SKIP>") and
-  Cond  ("\<IF> _ \<THEN> _ \<ELSE> _"  60) and
-  While  ("\<WHILE> _ \<DO> _"  60)
+  com = SKIP 
+      | Assign name aexp         ("_ ::= _" [1000, 61] 61)
+      | Semi   com  com          ("_;/ _"  [60, 61] 60)
+      | If     bexp com com     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61)
+      | While  bexp com         ("(WHILE _/ DO _)"  [0, 61] 61)
 
 end
diff -r 9ed5d8ad8fa0 -r faba4800b00b src/HOL/IMP/Compiler.thy
--- a/src/HOL/IMP/Compiler.thy	Wed Jun 01 19:50:59 2011 +0200
+++ b/src/HOL/IMP/Compiler.thy	Wed Jun 01 23:08:04 2011 +0200
@@ -1,298 +1,237 @@
-(*  Title:      HOL/IMP/Compiler.thy
-    Author:     Tobias Nipkow, TUM
-    Copyright   1996 TUM
-*)
+(* Author: Tobias Nipkow *)
+
+header "A Compiler for IMP"
 
-theory Compiler imports Machines begin
+theory Compiler imports Big_Step
+begin
 
-subsection "The compiler"
+subsection "Instructions and Stack Machine"
 
-primrec compile :: "com \<Rightarrow> instr list"
-where
-  "compile \<SKIP> = []"
-| "compile (x:==a) = [SET x a]"
-| "compile (c1;c2) = compile c1 @ compile c2"
-| "compile (\<IF> b \<THEN> c1 \<ELSE> c2) =
-    [JMPF b (length(compile c1) + 1)] @ compile c1 @
-    [JMPF (\<lambda>x. False) (length(compile c2))] @ compile c2"
-| "compile (\<WHILE> b \<DO> c) = [JMPF b (length(compile c) + 1)] @ compile c @
-    [JMPB (length(compile c)+1)]"
+datatype instr = 
+  LOADI int | LOAD string | ADD |
+  STORE string |
+  JMPF nat |
+  JMPB nat |
+  JMPFLESS nat |
+  JMPFGE nat
 
-subsection "Compiler correctness"
+type_synonym stack = "int list"
+type_synonym config = "nat\<times>state\<times>stack"
+
+abbreviation "hd2 xs == hd(tl xs)"
+abbreviation "tl2 xs == tl(tl xs)"
 
-theorem assumes A: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
-shows "\<And>p q. \<langle>compile c @ p,q,s\<rangle> -*\<rightarrow> \<langle>p,rev(compile c)@q,t\<rangle>"
-  (is "\<And>p q. ?P c s t p q")
-proof -
-  from A show "\<And>p q. ?thesis p q"
-  proof induct
-    case Skip thus ?case by simp
-  next
-    case Assign thus ?case by force
-  next
-    case Semi thus ?case by simp (blast intro:rtrancl_trans)
-  next
-    fix b c0 c1 s0 s1 p q
-    assume IH: "\<And>p q. ?P c0 s0 s1 p q"
-    assume "b s0"
-    thus "?P (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1 p q"
-      by(simp add: IH[THEN rtrancl_trans])
-  next
-    case IfFalse thus ?case by(simp)
-  next
-    case WhileFalse thus ?case by simp
-  next
-    fix b c and s0::state and s1 s2 p q
-    assume b: "b s0" and
-      IHc: "\<And>p q. ?P c s0 s1 p q" and
-      IHw: "\<And>p q. ?P (\<WHILE> b \<DO> c) s1 s2 p q"
-    show "?P (\<WHILE> b \<DO> c) s0 s2 p q"
-      using b  IHc[THEN rtrancl_trans] IHw by(simp)
-  qed
+inductive exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"
+    ("(_/ \<turnstile> (_ \<rightarrow>/ _))" [50,0,0] 50)
+  for P :: "instr list"
+where
+"\<lbrakk> i < size P;  P!i = LOADI n \<rbrakk> \<Longrightarrow>
+ P \<turnstile> (i,s,stk) \<rightarrow> (i+1,s, n#stk)" |
+"\<lbrakk> i < size P;  P!i = LOAD x \<rbrakk> \<Longrightarrow> 
+ P \<turnstile> (i,s,stk) \<rightarrow> (i+1,s, s x # stk)" |
+"\<lbrakk> i < size P;  P!i = ADD \<rbrakk> \<Longrightarrow> 
+ P \<turnstile> (i,s,stk) \<rightarrow> (i+1,s, (hd2 stk + hd stk) # tl2 stk)" |
+"\<lbrakk> i < size P;  P!i = STORE n \<rbrakk> \<Longrightarrow>
+ P \<turnstile> (i,s,stk) \<rightarrow> (i+1,s(n := hd stk),tl stk)" |
+"\<lbrakk> i < size P;  P!i = JMPF n \<rbrakk> \<Longrightarrow>
+ P \<turnstile> (i,s,stk) \<rightarrow> (i+1+n,s,stk)" |
+"\<lbrakk> i < size P;  P!i = JMPB n;  n \<le> i+1 \<rbrakk> \<Longrightarrow>
+ P \<turnstile> (i,s,stk) \<rightarrow> (i+1-n,s,stk)" |
+"\<lbrakk> i < size P;  P!i = JMPFLESS n \<rbrakk> \<Longrightarrow>
+ P \<turnstile> (i,s,stk) \<rightarrow> (if hd2 stk < hd stk then i+1+n else i+1,s,tl2 stk)" |
+"\<lbrakk> i < size P;  P!i = JMPFGE n \<rbrakk> \<Longrightarrow>
+ P \<turnstile> (i,s,stk) \<rightarrow> (if hd2 stk >= hd stk then i+1+n else i+1,s,tl2 stk)"
+
+code_pred exec1 .
+
+declare exec1.intros[intro]
+
+inductive exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("_/ \<turnstile> (_ \<rightarrow>*/ _)" 50)
+where
+refl: "P \<turnstile> c \<rightarrow>* c" |
+step: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P \<turnstile> c' \<rightarrow>* c'' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c''"
+
+declare exec.intros[intro]
+
+lemmas exec_induct = exec.induct[split_format(complete)]
+
+code_pred exec .
+
+values
+  "{(i,map t [''x'',''y''],stk) | i t stk.
+    [LOAD ''y'', STORE ''x''] \<turnstile>
+    (0,lookup[(''x'',3),(''y'',4)],[]) \<rightarrow>* (i,t,stk)}"
+
+
+subsection{* Verification infrastructure *}
+
+lemma exec_trans: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P \<turnstile> c' \<rightarrow>* c'' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c''"
+apply(induct rule: exec.induct)
+ apply blast
+by (metis exec.step)
+
+lemma exec1_subst: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> c' = c'' \<Longrightarrow> P \<turnstile> c \<rightarrow> c''"
+by auto
+
+lemmas exec1_simps = exec1.intros[THEN exec1_subst]
+
+text{* Below we need to argue about the execution of code that is embedded in
+larger programs. For this purpose we show that execution is preserved by
+appending code to the left or right of a program. *}
+
+lemma exec1_appendR: assumes "P \<turnstile> c \<rightarrow> c'" shows "P@P' \<turnstile> c \<rightarrow> c'"
+proof-
+  from assms show ?thesis
+  by cases (simp_all add: exec1_simps nth_append)
+  -- "All cases proved with the final simp-all"
 qed
 
-text {* The other direction! *}
-
-inductive_cases [elim!]: "(([],p,s),(is',p',s')) : stepa1"
-
-lemma [simp]: "(\<langle>[],q,s\<rangle> -n\<rightarrow> \<langle>p',q',t\<rangle>) = (n=0 \<and> p' = [] \<and> q' = q \<and> t = s)"
-apply(rule iffI)
- apply(erule rel_pow_E2, simp, fast)
-apply simp
-done
+lemma exec_appendR: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow>* c'"
+apply(induct rule: exec.induct)
+ apply blast
+by (metis exec1_appendR exec.step)
 
-lemma [simp]: "(\<langle>[],q,s\<rangle> -*\<rightarrow> \<langle>p',q',t\<rangle>) = (p' = [] \<and> q' = q \<and> t = s)"
-by(simp add: rtrancl_is_UN_rel_pow)
-
-definition
-  forws :: "instr \<Rightarrow> nat set" where
-  "forws instr = (case instr of
-     SET x a \<Rightarrow> {0} |
-     JMPF b n \<Rightarrow> {0,n} |
-     JMPB n \<Rightarrow> {})"
+lemma exec1_appendL:
+assumes "P \<turnstile> (i,s,stk) \<rightarrow> (i',s',stk')"
+shows "P' @ P \<turnstile> (size(P')+i,s,stk) \<rightarrow> (size(P')+i',s',stk')"
+proof-
+  from assms show ?thesis
+  by cases (simp_all add: exec1_simps)
+qed
 
-definition
-  backws :: "instr \<Rightarrow> nat set" where
-  "backws instr = (case instr of
-     SET x a \<Rightarrow> {} |
-     JMPF b n \<Rightarrow> {} |
-     JMPB n \<Rightarrow> {n})"
-
-primrec closed :: "nat \<Rightarrow> nat \<Rightarrow> instr list \<Rightarrow> bool"
-where
-  "closed m n [] = True"
-| "closed m n (instr#is) = ((\<forall>j \<in> forws instr. j \<le> size is+n) \<and>
-                          (\<forall>j \<in> backws instr. j \<le> m) \<and> closed (Suc m) n is)"
+lemma exec_appendL:
+ "P \<turnstile> (i,s,stk) \<rightarrow>* (i',s',stk')  \<Longrightarrow>
+  P' @ P \<turnstile> (size(P')+i,s,stk) \<rightarrow>* (size(P')+i',s',stk')"
+apply(induct rule: exec_induct)
+ apply blast
+by (blast intro: exec1_appendL exec.step)
 
-lemma [simp]:
- "\<And>m n. closed m n (C1@C2) =
-         (closed m (n+size C2) C1 \<and> closed (m+size C1) n C2)"
-by(induct C1) (simp, simp add:add_ac)
-
-theorem [simp]: "\<And>m n. closed m n (compile c)"
-by(induct c) (simp_all add:backws_def forws_def)
+text{* Now we specialise the above lemmas to enable automatic proofs of
+@{prop "P \<turnstile> c \<rightarrow>* c'"} where @{text P} is a mixture of concrete instructions and
+pieces of code that we already know how they execute (by induction), combined
+by @{text "@"} and @{text "#"}. Backward jumps are not supported.
+The details should be skipped on a first reading.
 
-lemma drop_lem: "n \<le> size(p1@p2)
- \<Longrightarrow> (p1' @ p2 = drop n p1 @ drop (n - size p1) p2) =
-    (n \<le> size p1 & p1' = drop n p1)"
-apply(rule iffI)
- defer apply simp
-apply(subgoal_tac "n \<le> size p1")
- apply simp
-apply(rule ccontr)
-apply(drule_tac f = length in arg_cong)
+If the pc points beyond the first instruction or part of the program, drop it: *}
+
+lemma exec_Cons_Suc[intro]:
+  "P \<turnstile> (i,s,stk) \<rightarrow>* (j,t,stk') \<Longrightarrow>
+  instr#P \<turnstile> (Suc i,s,stk) \<rightarrow>* (Suc j,t,stk')"
+apply(drule exec_appendL[where P'="[instr]"])
 apply simp
 done
 
-lemma reduce_exec1:
- "\<langle>i # p1 @ p2,q1 @ q2,s\<rangle> -1\<rightarrow> \<langle>p1' @ p2,q1' @ q2,s'\<rangle> \<Longrightarrow>
-  \<langle>i # p1,q1,s\<rangle> -1\<rightarrow> \<langle>p1',q1',s'\<rangle>"
-by(clarsimp simp add: drop_lem split:instr.split_asm split_if_asm)
-
-
-lemma closed_exec1:
- "\<lbrakk> closed 0 0 (rev q1 @ instr # p1);
-    \<langle>instr # p1 @ p2, q1 @ q2,r\<rangle> -1\<rightarrow> \<langle>p',q',r'\<rangle> \<rbrakk> \<Longrightarrow>
-  \<exists>p1' q1'. p' = p1'@p2 \<and> q' = q1'@q2 \<and> rev q1' @ p1' = rev q1 @ instr # p1"
-apply(clarsimp simp add:forws_def backws_def
-               split:instr.split_asm split_if_asm)
+lemma exec_appendL_if[intro]:
+ "size P' <= i
+  \<Longrightarrow> P \<turnstile> (i - size P',s,stk) \<rightarrow>* (i',s',stk')
+  \<Longrightarrow> P' @ P \<turnstile> (i,s,stk) \<rightarrow>* (size P' + i',s',stk')"
+apply(drule exec_appendL[where P'=P'])
+apply simp
 done
 
-theorem closed_execn_decomp: "\<And>C1 C2 r.
- \<lbrakk> closed 0 0 (rev C1 @ C2);
-   \<langle>C2 @ p1 @ p2, C1 @ q,r\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev C2 @ C1 @ q,t\<rangle> \<rbrakk>
- \<Longrightarrow> \<exists>s n1 n2. \<langle>C2,C1,r\<rangle> -n1\<rightarrow> \<langle>[],rev C2 @ C1,s\<rangle> \<and>
-     \<langle>p1@p2,rev C2 @ C1 @ q,s\<rangle> -n2\<rightarrow> \<langle>p2, rev p1 @ rev C2 @ C1 @ q,t\<rangle> \<and>
-         n = n1+n2"
-(is "\<And>C1 C2 r. \<lbrakk>?CL C1 C2; ?H C1 C2 r n\<rbrakk> \<Longrightarrow> ?P C1 C2 r n")
-proof(induct n)
-  fix C1 C2 r
-  assume "?H C1 C2 r 0"
-  thus "?P C1 C2 r 0" by simp
-next
-  fix C1 C2 r n
-  assume IH: "\<And>C1 C2 r. ?CL C1 C2 \<Longrightarrow> ?H C1 C2 r n \<Longrightarrow> ?P C1 C2 r n"
-  assume CL: "?CL C1 C2" and H: "?H C1 C2 r (Suc n)"
-  show "?P C1 C2 r (Suc n)"
-  proof (cases C2)
-    assume "C2 = []" with H show ?thesis by simp
-  next
-    fix instr tlC2
-    assume C2: "C2 = instr # tlC2"
-    from H C2 obtain p' q' r'
-      where 1: "\<langle>instr # tlC2 @ p1 @ p2, C1 @ q,r\<rangle> -1\<rightarrow> \<langle>p',q',r'\<rangle>"
-      and n: "\<langle>p',q',r'\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev C2 @ C1 @ q,t\<rangle>"
-      by(fastsimp simp add:rel_pow_commute)
-    from CL closed_exec1[OF _ 1] C2
-    obtain C2' C1' where pq': "p' = C2' @ p1 @ p2 \<and> q' = C1' @ q"
-      and same: "rev C1' @ C2' = rev C1 @ C2"
-      by fastsimp
-    have rev_same: "rev C2' @ C1' = rev C2 @ C1"
-    proof -
-      have "rev C2' @ C1' = rev(rev C1' @ C2')" by simp
-      also have "\<dots> = rev(rev C1 @ C2)" by(simp only:same)
-      also have "\<dots> =  rev C2 @ C1" by simp
-      finally show ?thesis .
-    qed
-    hence rev_same': "\<And>p. rev C2' @ C1' @ p = rev C2 @ C1 @ p" by simp
-    from n have n': "\<langle>C2' @ p1 @ p2,C1' @ q,r'\<rangle> -n\<rightarrow>
-                     \<langle>p2,rev p1 @ rev C2' @ C1' @ q,t\<rangle>"
-      by(simp add:pq' rev_same')
-    from IH[OF _ n'] CL
-    obtain s n1 n2 where n1: "\<langle>C2',C1',r'\<rangle> -n1\<rightarrow> \<langle>[],rev C2 @ C1,s\<rangle>" and
-      "\<langle>p1 @ p2,rev C2 @ C1 @ q,s\<rangle> -n2\<rightarrow> \<langle>p2,rev p1 @ rev C2 @ C1 @ q,t\<rangle> \<and>
-       n = n1 + n2"
-      by(fastsimp simp add: same rev_same rev_same')
-    moreover
-    from 1 n1 pq' C2 have "\<langle>C2,C1,r\<rangle> -Suc n1\<rightarrow> \<langle>[],rev C2 @ C1,s\<rangle>"
-      by (simp del:relpow.simps exec_simp) (fast dest:reduce_exec1)
-    ultimately show ?thesis by (fastsimp simp del:relpow.simps)
-  qed
-qed
+text{* Split the execution of a compound program up into the excution of its
+parts: *}
 
-lemma execn_decomp:
-"\<langle>compile c @ p1 @ p2,q,r\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev(compile c) @ q,t\<rangle>
- \<Longrightarrow> \<exists>s n1 n2. \<langle>compile c,[],r\<rangle> -n1\<rightarrow> \<langle>[],rev(compile c),s\<rangle> \<and>
-     \<langle>p1@p2,rev(compile c) @ q,s\<rangle> -n2\<rightarrow> \<langle>p2, rev p1 @ rev(compile c) @ q,t\<rangle> \<and>
-         n = n1+n2"
-using closed_execn_decomp[of "[]",simplified] by simp
+lemma exec_append_trans[intro]:
+"P \<turnstile> (0,s,stk) \<rightarrow>* (i',s',stk') \<Longrightarrow>
+ size P \<le> i' \<Longrightarrow>
+ P' \<turnstile>  (i' - size P,s',stk') \<rightarrow>* (i'',s'',stk'') \<Longrightarrow>
+ j'' = size P + i''
+ \<Longrightarrow>
+ P @ P' \<turnstile> (0,s,stk) \<rightarrow>* (j'',s'',stk'')"
+by(metis exec_trans[OF  exec_appendR exec_appendL_if])
 
-lemma exec_star_decomp:
-"\<langle>compile c @ p1 @ p2,q,r\<rangle> -*\<rightarrow> \<langle>p2,rev p1 @ rev(compile c) @ q,t\<rangle>
- \<Longrightarrow> \<exists>s. \<langle>compile c,[],r\<rangle> -*\<rightarrow> \<langle>[],rev(compile c),s\<rangle> \<and>
-     \<langle>p1@p2,rev(compile c) @ q,s\<rangle> -*\<rightarrow> \<langle>p2, rev p1 @ rev(compile c) @ q,t\<rangle>"
-by(simp add:rtrancl_is_UN_rel_pow)(fast dest: execn_decomp)
+
+declare Let_def[simp] eval_nat_numeral[simp]
 
 
-(* Alternative:
-lemma exec_comp_n:
-"\<And>p1 p2 q r t n.
- \<langle>compile c @ p1 @ p2,q,r\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev(compile c) @ q,t\<rangle>
- \<Longrightarrow> \<exists>s n1 n2. \<langle>compile c,[],r\<rangle> -n1\<rightarrow> \<langle>[],rev(compile c),s\<rangle> \<and>
-     \<langle>p1@p2,rev(compile c) @ q,s\<rangle> -n2\<rightarrow> \<langle>p2, rev p1 @ rev(compile c) @ q,t\<rangle> \<and>
-         n = n1+n2"
- (is "\<And>p1 p2 q r t n. ?H c p1 p2 q r t n \<Longrightarrow> ?P c p1 p2 q r t n")
-proof (induct c)
-*)
+subsection "Compilation"
 
-text{*Warning: 
-@{prop"\<langle>compile c @ p,q,s\<rangle> -*\<rightarrow> \<langle>p,rev(compile c)@q,t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"}
-is not true! *}
+fun acomp :: "aexp \<Rightarrow> instr list" where
+"acomp (N n) = [LOADI n]" |
+"acomp (V x) = [LOAD x]" |
+"acomp (Plus a1 a2) = acomp a1 @ acomp a2 @ [ADD]"
+
+lemma acomp_correct[intro]:
+  "acomp a \<turnstile> (0,s,stk) \<rightarrow>* (size(acomp a),s,aval a s#stk)"
+apply(induct a arbitrary: stk)
+apply(fastsimp)+
+done
 
-theorem "\<And>s t.
- \<langle>compile c,[],s\<rangle> -*\<rightarrow> \<langle>[],rev(compile c),t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
-proof (induct c)
-  fix s t
-  assume "\<langle>compile SKIP,[],s\<rangle> -*\<rightarrow> \<langle>[],rev(compile SKIP),t\<rangle>"
-  thus "\<langle>SKIP,s\<rangle> \<longrightarrow>\<^sub>c t" by simp
-next
-  fix s t v f
-  assume "\<langle>compile(v :== f),[],s\<rangle> -*\<rightarrow> \<langle>[],rev(compile(v :== f)),t\<rangle>"
-  thus "\<langle>v :== f,s\<rangle> \<longrightarrow>\<^sub>c t" by simp
-next
-  fix s1 s3 c1 c2
-  let ?C1 = "compile c1" let ?C2 = "compile c2"
-  assume IH1: "\<And>s t. \<langle>?C1,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C1,t\<rangle> \<Longrightarrow> \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c t"
-     and IH2: "\<And>s t. \<langle>?C2,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C2,t\<rangle> \<Longrightarrow> \<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c t"
-  assume "\<langle>compile(c1;c2),[],s1\<rangle> -*\<rightarrow> \<langle>[],rev(compile(c1;c2)),s3\<rangle>"
-  then obtain s2 where exec1: "\<langle>?C1,[],s1\<rangle> -*\<rightarrow> \<langle>[],rev ?C1,s2\<rangle>" and
-             exec2: "\<langle>?C2,rev ?C1,s2\<rangle> -*\<rightarrow> \<langle>[],rev(compile(c1;c2)),s3\<rangle>"
-    by(fastsimp dest:exec_star_decomp[of _ _ "[]" "[]",simplified])
-  from exec2 have exec2': "\<langle>?C2,[],s2\<rangle> -*\<rightarrow> \<langle>[],rev ?C2,s3\<rangle>"
-    using exec_star_decomp[of _ "[]" "[]"] by fastsimp
-  have "\<langle>c1,s1\<rangle> \<longrightarrow>\<^sub>c s2" using IH1 exec1 by simp
-  moreover have "\<langle>c2,s2\<rangle> \<longrightarrow>\<^sub>c s3" using IH2 exec2' by fastsimp
-  ultimately show "\<langle>c1;c2,s1\<rangle> \<longrightarrow>\<^sub>c s3" ..
+fun bcomp :: "bexp \<Rightarrow> bool \<Rightarrow> nat \<Rightarrow> instr list" where
+"bcomp (B bv) c n = (if bv=c then [JMPF n] else [])" |
+"bcomp (Not b) c n = bcomp b (\<not>c) n" |
+"bcomp (And b1 b2) c n =
+ (let cb2 = bcomp b2 c n;
+      m = (if c then size cb2 else size cb2+n);
+      cb1 = bcomp b1 False m
+  in cb1 @ cb2)" |
+"bcomp (Less a1 a2) c n =
+ acomp a1 @ acomp a2 @ (if c then [JMPFLESS n] else [JMPFGE n])"
+
+value
+  "bcomp (And (Less (V ''x'') (V ''y'')) (Not(Less (V ''u'') (V ''v''))))
+     False 3"
+
+lemma bcomp_correct[intro]:
+ "bcomp b c n \<turnstile>
+ (0,s,stk)  \<rightarrow>*  (size(bcomp b c n) + (if c = bval b s then n else 0),s,stk)"
+proof(induct b arbitrary: c n m)
+  case Not
+  from Not[of "~c"] show ?case by fastsimp
 next
-  fix s t b c1 c2
-  let ?if = "IF b THEN c1 ELSE c2" let ?C = "compile ?if"
-  let ?C1 = "compile c1" let ?C2 = "compile c2"
-  assume IH1: "\<And>s t. \<langle>?C1,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C1,t\<rangle> \<Longrightarrow> \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c t"
-     and IH2: "\<And>s t. \<langle>?C2,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C2,t\<rangle> \<Longrightarrow> \<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c t"
-     and H: "\<langle>?C,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C,t\<rangle>"
-  show "\<langle>?if,s\<rangle> \<longrightarrow>\<^sub>c t"
-  proof cases
-    assume b: "b s"
-    with H have "\<langle>?C1,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C1,t\<rangle>"
-      by (fastsimp dest:exec_star_decomp
-            [of _ "[JMPF (\<lambda>x. False) (size ?C2)]@?C2" "[]",simplified])
-    hence "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c t" by(rule IH1)
-    with b show ?thesis ..
-  next
-    assume b: "\<not> b s"
-    with H have "\<langle>?C2,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C2,t\<rangle>"
-      using exec_star_decomp[of _ "[]" "[]"] by simp
-    hence "\<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c t" by(rule IH2)
-    with b show ?thesis ..
-  qed
+  case (And b1 b2)
+  from And(1)[of "False"] And(2)[of "c"] show ?case by fastsimp
+qed fastsimp+
+
+
+fun ccomp :: "com \<Rightarrow> instr list" where
+"ccomp SKIP = []" |
+"ccomp (x ::= a) = acomp a @ [STORE x]" |
+"ccomp (c\<^isub>1;c\<^isub>2) = ccomp c\<^isub>1 @ ccomp c\<^isub>2" |
+"ccomp (IF b THEN c\<^isub>1 ELSE c\<^isub>2) =
+  (let cc\<^isub>1 = ccomp c\<^isub>1; cc\<^isub>2 = ccomp c\<^isub>2; cb = bcomp b False (size cc\<^isub>1 + 1)
+   in cb @ cc\<^isub>1 @ JMPF(size cc\<^isub>2) # cc\<^isub>2)" |
+"ccomp (WHILE b DO c) =
+ (let cc = ccomp c; cb = bcomp b False (size cc + 1)
+  in cb @ cc @ [JMPB (size cb + size cc + 1)])"
+
+value "ccomp
+ (IF Less (V ''u'') (N 1) THEN ''u'' ::= Plus (V ''u'') (N 1)
+  ELSE ''v'' ::= V ''u'')"
+
+value "ccomp (WHILE Less (V ''u'') (N 1) DO (''u'' ::= Plus (V ''u'') (N 1)))"
+
+
+subsection "Preservation of sematics"
+
+lemma ccomp_correct:
+  "(c,s) \<Rightarrow> t \<Longrightarrow> ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (size(ccomp c),t,stk)"
+proof(induct arbitrary: stk rule: big_step_induct)
+  case (Assign x a s)
+  show ?case by (fastsimp simp:fun_upd_def)
 next
-  fix b c s t
-  let ?w = "WHILE b DO c" let ?W = "compile ?w" let ?C = "compile c"
-  let ?j1 = "JMPF b (size ?C + 1)" let ?j2 = "JMPB (size ?C + 1)"
-  assume IHc: "\<And>s t. \<langle>?C,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C,t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
-     and H: "\<langle>?W,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
-  from H obtain k where ob:"\<langle>?W,[],s\<rangle> -k\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
-    by(simp add:rtrancl_is_UN_rel_pow) blast
-  { fix n have "\<And>s. \<langle>?W,[],s\<rangle> -n\<rightarrow> \<langle>[],rev ?W,t\<rangle> \<Longrightarrow> \<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c t"
-    proof (induct n rule: less_induct)
-      fix n
-      assume IHm: "\<And>m s. \<lbrakk>m < n; \<langle>?W,[],s\<rangle> -m\<rightarrow> \<langle>[],rev ?W,t\<rangle> \<rbrakk> \<Longrightarrow> \<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c t"
-      fix s
-      assume H: "\<langle>?W,[],s\<rangle> -n\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
-      show "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c t"
-      proof cases
-        assume b: "b s"
-        then obtain m where m: "n = Suc m"
-          and "\<langle>?C @ [?j2],[?j1],s\<rangle> -m\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
-          using H by fastsimp
-        then obtain r n1 n2 where n1: "\<langle>?C,[],s\<rangle> -n1\<rightarrow> \<langle>[],rev ?C,r\<rangle>"
-          and n2: "\<langle>[?j2],rev ?C @ [?j1],r\<rangle> -n2\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
-          and n12: "m = n1+n2"
-          using execn_decomp[of _ "[?j2]"]
-          by(simp del: execn_simp) fast
-        have n2n: "n2 - 1 < n" using m n12 by arith
-        note b
-        moreover
-        { from n1 have "\<langle>?C,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C,r\<rangle>"
-            by (simp add:rtrancl_is_UN_rel_pow) fast
-          hence "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c r" by(rule IHc)
-        }
-        moreover
-        { have "n2 - 1 < n" using m n12 by arith
-          moreover from n2 have "\<langle>?W,[],r\<rangle> -n2- 1\<rightarrow> \<langle>[],rev ?W,t\<rangle>" by fastsimp
-          ultimately have "\<langle>?w,r\<rangle> \<longrightarrow>\<^sub>c t" by(rule IHm)
-        }
-        ultimately show ?thesis ..
-      next
-        assume b: "\<not> b s"
-        hence "t = s" using H by simp
-        with b show ?thesis by simp
-      qed
-    qed
-  }
-  with ob show "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c t" by fast
-qed
-
-(* TODO: connect with Machine 0 using M_equiv *)
+  case (Semi c1 s1 s2 c2 s3)
+  let ?cc1 = "ccomp c1"  let ?cc2 = "ccomp c2"
+  have "?cc1 @ ?cc2 \<turnstile> (0,s1,stk) \<rightarrow>* (size ?cc1,s2,stk)"
+    using Semi.hyps(2) by (fastsimp)
+  moreover
+  have "?cc1 @ ?cc2 \<turnstile> (size ?cc1,s2,stk) \<rightarrow>* (size(?cc1 @ ?cc2),s3,stk)"
+    using Semi.hyps(4) by (fastsimp)
+  ultimately show ?case by simp (blast intro: exec_trans)
+next
+  case (WhileTrue b s1 c s2 s3)
+  let ?cc = "ccomp c"
+  let ?cb = "bcomp b False (size ?cc + 1)"
+  let ?cw = "ccomp(WHILE b DO c)"
+  have "?cw \<turnstile> (0,s1,stk) \<rightarrow>* (size ?cb + size ?cc,s2,stk)"
+    using WhileTrue(1,3) by fastsimp
+  moreover
+  have "?cw \<turnstile> (size ?cb + size ?cc,s2,stk) \<rightarrow>* (0,s2,stk)"
+    by (fastsimp)
+  moreover
+  have "?cw \<turnstile> (0,s2,stk) \<rightarrow>* (size ?cw,s3,stk)" by(rule WhileTrue(5))
+  ultimately show ?case by(blast intro: exec_trans)
+qed fastsimp+
 
 end
diff -r 9ed5d8ad8fa0 -r faba4800b00b src/HOL/IMP/Compiler0.thy
--- a/src/HOL/IMP/Compiler0.thy	Wed Jun 01 19:50:59 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,262 +0,0 @@
-(*  Title:      HOL/IMP/Compiler0.thy
-    Author:     Tobias Nipkow, TUM
-    Copyright   1996 TUM
-
-This is an early version of the compiler, where the abstract machine
-has an explicit pc. This turned out to be awkward, and a second
-development was started. See Machines.thy and Compiler.thy.
-*)
-
-header "A Simple Compiler"
-
-theory Compiler0 imports Natural begin
-
-subsection "An abstract, simplistic machine"
-
-text {* There are only three instructions: *}
-datatype instr = ASIN loc aexp | JMPF bexp nat | JMPB nat
-
-text {* We describe execution of programs in the machine by
-  an operational (small step) semantics:
-*}
-
-inductive_set
-  stepa1 :: "instr list \<Rightarrow> ((state\<times>nat) \<times> (state\<times>nat))set"
-  and stepa1' :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
-    ("_ \<turnstile> (3\<langle>_,_\<rangle>/ -1\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0] 50)
-  for P :: "instr list"
-where
-  "P \<turnstile> \<langle>s,m\<rangle> -1\<rightarrow> \<langle>t,n\<rangle> == ((s,m),t,n) : stepa1 P"
-| ASIN[simp]:
-  "\<lbrakk> n<size P; P!n = ASIN x a \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>s,n\<rangle> -1\<rightarrow> \<langle>s[x\<mapsto> a s],Suc n\<rangle>"
-| JMPFT[simp,intro]:
-  "\<lbrakk> n<size P; P!n = JMPF b i;  b s \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>s,n\<rangle> -1\<rightarrow> \<langle>s,Suc n\<rangle>"
-| JMPFF[simp,intro]:
-  "\<lbrakk> n<size P; P!n = JMPF b i; ~b s; m=n+i \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>s,n\<rangle> -1\<rightarrow> \<langle>s,m\<rangle>"
-| JMPB[simp]:
-  "\<lbrakk> n<size P; P!n = JMPB i; i <= n; j = n-i \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>s,n\<rangle> -1\<rightarrow> \<langle>s,j\<rangle>"
-
-abbreviation
-  stepa :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
-    ("_ \<turnstile>/ (3\<langle>_,_\<rangle>/ -*\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0] 50)  where
-  "P \<turnstile> \<langle>s,m\<rangle> -*\<rightarrow> \<langle>t,n\<rangle> == ((s,m),t,n) : ((stepa1 P)^*)"
-
-abbreviation
-  stepan :: "[instr list,state,nat,nat,state,nat] \<Rightarrow> bool"
-    ("_ \<turnstile>/ (3\<langle>_,_\<rangle>/ -(_)\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0,0] 50)  where
-  "P \<turnstile> \<langle>s,m\<rangle> -(i)\<rightarrow> \<langle>t,n\<rangle> == ((s,m),t,n) : (stepa1 P ^^ i)"
-
-subsection "The compiler"
-
-primrec compile :: "com \<Rightarrow> instr list" where
-"compile \<SKIP> = []" |
-"compile (x:==a) = [ASIN x a]" |
-"compile (c1;c2) = compile c1 @ compile c2" |
-"compile (\<IF> b \<THEN> c1 \<ELSE> c2) =
- [JMPF b (length(compile c1) + 2)] @ compile c1 @
- [JMPF (%x. False) (length(compile c2)+1)] @ compile c2" |
-"compile (\<WHILE> b \<DO> c) = [JMPF b (length(compile c) + 2)] @ compile c @
- [JMPB (length(compile c)+1)]"
-
-declare nth_append[simp]
-
-subsection "Context lifting lemmas"
-
-text {*
-  Some lemmas for lifting an execution into a prefix and suffix
-  of instructions; only needed for the first proof.
-*}
-lemma app_right_1:
-  assumes "is1 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
-  shows "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
-  using assms
-  by induct auto
-
-lemma app_left_1:
-  assumes "is2 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
-  shows "is1 @ is2 \<turnstile> \<langle>s1,size is1+i1\<rangle> -1\<rightarrow> \<langle>s2,size is1+i2\<rangle>"
-  using assms
-  by induct auto
-
-declare rtrancl_induct2 [induct set: rtrancl]
-
-lemma app_right:
-  assumes "is1 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
-  shows "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
-  using assms
-proof induct
-  show "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s1,i1\<rangle>" by simp
-next
-  fix s1' i1' s2 i2
-  assume "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s1',i1'\<rangle>"
-    and "is1 \<turnstile> \<langle>s1',i1'\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
-  thus "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
-    by (blast intro: app_right_1 rtrancl_trans)
-qed
-
-lemma app_left:
-  assumes "is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
-  shows "is1 @ is2 \<turnstile> \<langle>s1,size is1+i1\<rangle> -*\<rightarrow> \<langle>s2,size is1+i2\<rangle>"
-using assms
-proof induct
-  show "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s1,length is1 + i1\<rangle>" by simp
-next
-  fix s1' i1' s2 i2
-  assume "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s1',length is1 + i1'\<rangle>"
-    and "is2 \<turnstile> \<langle>s1',i1'\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
-  thus "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s2,length is1 + i2\<rangle>"
-    by (blast intro: app_left_1 rtrancl_trans)
-qed
-
-lemma app_left2:
-  "\<lbrakk> is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>; j1 = size is1+i1; j2 = size is1+i2 \<rbrakk> \<Longrightarrow>
-    is1 @ is2 \<turnstile> \<langle>s1,j1\<rangle> -*\<rightarrow> \<langle>s2,j2\<rangle>"
-  by (simp add: app_left)
-
-lemma app1_left:
-  assumes "is \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
-  shows "instr # is \<turnstile> \<langle>s1,Suc i1\<rangle> -*\<rightarrow> \<langle>s2,Suc i2\<rangle>"
-proof -
-  from app_left [OF assms, of "[instr]"]
-  show ?thesis by simp
-qed
-
-subsection "Compiler correctness"
-
-declare rtrancl_into_rtrancl[trans]
-        converse_rtrancl_into_rtrancl[trans]
-        rtrancl_trans[trans]
-
-text {*
-  The first proof; The statement is very intuitive,
-  but application of induction hypothesis requires the above lifting lemmas
-*}
-theorem
-  assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
-  shows "compile c \<turnstile> \<langle>s,0\<rangle> -*\<rightarrow> \<langle>t,length(compile c)\<rangle>" (is "?P c s t")
-  using assms
-proof induct
-  show "\<And>s. ?P \<SKIP> s s" by simp
-next
-  show "\<And>a s x. ?P (x :== a) s (s[x\<mapsto> a s])" by force
-next
-  fix c0 c1 s0 s1 s2
-  assume "?P c0 s0 s1"
-  hence "compile c0 @ compile c1 \<turnstile> \<langle>s0,0\<rangle> -*\<rightarrow> \<langle>s1,length(compile c0)\<rangle>"
-    by (rule app_right)
-  moreover assume "?P c1 s1 s2"
-  hence "compile c0 @ compile c1 \<turnstile> \<langle>s1,length(compile c0)\<rangle> -*\<rightarrow>
-    \<langle>s2,length(compile c0)+length(compile c1)\<rangle>"
-  proof -
-    show "\<And>is1 is2 s1 s2 i2.
-      is2 \<turnstile> \<langle>s1,0\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle> \<Longrightarrow>
-      is1 @ is2 \<turnstile> \<langle>s1,size is1\<rangle> -*\<rightarrow> \<langle>s2,size is1+i2\<rangle>"
-      using app_left[of _ 0] by simp
-  qed
-  ultimately have "compile c0 @ compile c1 \<turnstile> \<langle>s0,0\<rangle> -*\<rightarrow>
-      \<langle>s2,length(compile c0)+length(compile c1)\<rangle>"
-    by (rule rtrancl_trans)
-  thus "?P (c0; c1) s0 s2" by simp
-next
-  fix b c0 c1 s0 s1
-  let ?comp = "compile(\<IF> b \<THEN> c0 \<ELSE> c1)"
-  assume "b s0" and IH: "?P c0 s0 s1"
-  hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,1\<rangle>" by auto
-  also from IH
-  have "?comp \<turnstile> \<langle>s0,1\<rangle> -*\<rightarrow> \<langle>s1,length(compile c0)+1\<rangle>"
-    by(auto intro:app1_left app_right)
-  also have "?comp \<turnstile> \<langle>s1,length(compile c0)+1\<rangle> -1\<rightarrow> \<langle>s1,length ?comp\<rangle>"
-    by(auto)
-  finally show "?P (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1" .
-next
-  fix b c0 c1 s0 s1
-  let ?comp = "compile(\<IF> b \<THEN> c0 \<ELSE> c1)"
-  assume "\<not>b s0" and IH: "?P c1 s0 s1"
-  hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,length(compile c0) + 2\<rangle>" by auto
-  also from IH
-  have "?comp \<turnstile> \<langle>s0,length(compile c0)+2\<rangle> -*\<rightarrow> \<langle>s1,length ?comp\<rangle>"
-    by (force intro!: app_left2 app1_left)
-  finally show "?P (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1" .
-next
-  fix b c and s::state
-  assume "\<not>b s"
-  thus "?P (\<WHILE> b \<DO> c) s s" by force
-next
-  fix b c and s0::state and s1 s2
-  let ?comp = "compile(\<WHILE> b \<DO> c)"
-  assume "b s0" and
-    IHc: "?P c s0 s1" and IHw: "?P (\<WHILE> b \<DO> c) s1 s2"
-  hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,1\<rangle>" by auto
-  also from IHc
-  have "?comp \<turnstile> \<langle>s0,1\<rangle> -*\<rightarrow> \<langle>s1,length(compile c)+1\<rangle>"
-    by (auto intro: app1_left app_right)
-  also have "?comp \<turnstile> \<langle>s1,length(compile c)+1\<rangle> -1\<rightarrow> \<langle>s1,0\<rangle>" by simp
-  also note IHw
-  finally show "?P (\<WHILE> b \<DO> c) s0 s2".
-qed
-
-text {*
-  Second proof; statement is generalized to cater for prefixes and suffixes;
-  needs none of the lifting lemmas, but instantiations of pre/suffix.
-  *}
-(*
-theorem assumes A: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
-shows "\<And>a z. a@compile c@z \<turnstile> \<langle>s,size a\<rangle> -*\<rightarrow> \<langle>t,size a + size(compile c)\<rangle>"
-      (is "\<And>a z. ?P c s t a z")
-proof -
-  from A show "\<And>a z. ?thesis a z"
-  proof induct
-    case Skip thus ?case by simp
-  next
-    case Assign thus ?case by (force intro!: ASIN)
-  next
-    fix c1 c2 s s' s'' a z
-    assume IH1: "\<And>a z. ?P c1 s s' a z" and IH2: "\<And>a z. ?P c2 s' s'' a z"
-    from IH1 IH2[of "a@compile c1"]
-    show "?P (c1;c2) s s'' a z"
-      by(simp add:add_assoc[THEN sym])(blast intro:rtrancl_trans)
-  next
-(* at this point I gave up converting to structured proofs *)
-(* \<IF> b \<THEN> c0 \<ELSE> c1; case b is true *)
-   apply(intro strip)
-   (* instantiate assumption sufficiently for later: *)
-   apply(erule_tac x = "a@[?I]" in allE)
-   apply(simp)
-   (* execute JMPF: *)
-   apply(rule converse_rtrancl_into_rtrancl)
-    apply(force intro!: JMPFT)
-   (* execute compile c0: *)
-   apply(rule rtrancl_trans)
-    apply(erule allE)
-    apply assumption
-   (* execute JMPF: *)
-   apply(rule r_into_rtrancl)
-   apply(force intro!: JMPFF)
-(* end of case b is true *)
-  apply(intro strip)
-  apply(erule_tac x = "a@[?I]@compile c0@[?J]" in allE)
-  apply(simp add:add_assoc)
-  apply(rule converse_rtrancl_into_rtrancl)
-   apply(force intro!: JMPFF)
-  apply(blast)
- apply(force intro: JMPFF)
-apply(intro strip)
-apply(erule_tac x = "a@[?I]" in allE)
-apply(erule_tac x = a in allE)
-apply(simp)
-apply(rule converse_rtrancl_into_rtrancl)
- apply(force intro!: JMPFT)
-apply(rule rtrancl_trans)
- apply(erule allE)
- apply assumption
-apply(rule converse_rtrancl_into_rtrancl)
- apply(force intro!: JMPB)
-apply(simp)
-done
-*)
-text {* Missing: the other direction! I did much of it, and although
-the main lemma is very similar to the one in the new development, the
-lemmas surrounding it seemed much more complicated. In the end I gave
-up. *}
-
-end
diff -r 9ed5d8ad8fa0 -r faba4800b00b src/HOL/IMP/Denotation.thy
--- a/src/HOL/IMP/Denotation.thy	Wed Jun 01 19:50:59 2011 +0200
+++ b/src/HOL/IMP/Denotation.thy	Wed Jun 01 23:08:04 2011 +0200
@@ -1,44 +1,38 @@
-(*  Title:      HOL/IMP/Denotation.thy
-    Author:     Heiko Loetzbeyer & Robert Sandner, TUM
-*)
+(* Authors: Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow *)
 
 header "Denotational Semantics of Commands"
 
-theory Denotation imports Natural begin
+theory Denotation imports Big_Step begin
 
 type_synonym com_den = "(state \<times> state) set"
 
 definition
-  Gamma :: "[bexp,com_den] => (com_den => com_den)" where
-  "Gamma b cd = (\<lambda>phi. {(s,t). (s,t) \<in> (cd O phi) \<and> b s} \<union>
-                       {(s,t). s=t \<and> \<not>b s})"
+  Gamma :: "bexp \<Rightarrow> com_den \<Rightarrow> (com_den \<Rightarrow> com_den)" where
+  "Gamma b cd = (\<lambda>phi. {(s,t). (s,t) \<in> (cd O phi) \<and> bval b s} \<union>
+                       {(s,t). s=t \<and> \<not>bval b s})"
 
-primrec C :: "com => com_den"
-where
-  C_skip:   "C \<SKIP>   = Id"
-| C_assign: "C (x :== a) = {(s,t). t = s[x\<mapsto>a(s)]}"
-| C_comp:   "C (c0;c1)   = C(c0) O C(c1)"
-| C_if:     "C (\<IF> b \<THEN> c1 \<ELSE> c2) = {(s,t). (s,t) \<in> C c1 \<and> b s} \<union>
-                                                {(s,t). (s,t) \<in> C c2 \<and> \<not>b s}"
-| C_while:  "C(\<WHILE> b \<DO> c) = lfp (Gamma b (C c))"
+fun C :: "com \<Rightarrow> com_den" where
+"C SKIP   = Id" |
+"C (x ::= a) = {(s,t). t = s(x := aval a s)}" |
+"C (c0;c1)   = C(c0) O C(c1)" |
+"C (IF b THEN c1 ELSE c2) = {(s,t). (s,t) \<in> C c1 \<and> bval b s} \<union>
+                            {(s,t). (s,t) \<in> C c2 \<and> \<not>bval b s}" |
+"C(WHILE b DO c) = lfp (Gamma b (C c))"
 
 
-(**** mono (Gamma(b,c)) ****)
+lemma Gamma_mono: "mono (Gamma b c)"
+by (unfold Gamma_def mono_def) fast
 
-lemma Gamma_mono: "mono (Gamma b c)"
-  by (unfold Gamma_def mono_def) fast
-
-lemma C_While_If: "C(\<WHILE> b \<DO> c) = C(\<IF> b \<THEN> c;\<WHILE> b \<DO> c \<ELSE> \<SKIP>)"
+lemma C_While_If: "C(WHILE b DO c) = C(IF b THEN c;WHILE b DO c ELSE SKIP)"
 apply simp
 apply (subst lfp_unfold [OF Gamma_mono])  --{*lhs only*}
 apply (simp add: Gamma_def)
 done
 
-(* Operational Semantics implies Denotational Semantics *)
+text{* Equivalence of denotational and big-step semantics: *}
 
-lemma com1: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> (s,t) \<in> C(c)"
-(* start with rule induction *)
-apply (induct set: evalc)
+lemma com1: "(c,s) \<Rightarrow> t \<Longrightarrow> (s,t) \<in> C(c)"
+apply (induct rule: big_step_induct)
 apply auto
 (* while *)
 apply (unfold Gamma_def)
@@ -48,23 +42,17 @@
 apply auto 
 done
 
-(* Denotational Semantics implies Operational Semantics *)
-
-lemma com2: "(s,t) \<in> C(c) \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
+lemma com2: "(s,t) \<in> C(c) \<Longrightarrow> (c,s) \<Rightarrow> t"
 apply (induct c arbitrary: s t)
 apply auto 
 apply blast
-
 (* while *)
 apply (erule lfp_induct2 [OF _ Gamma_mono])
 apply (unfold Gamma_def)
 apply auto
 done
 
-
-(**** Proof of Equivalence ****)
-
-lemma denotational_is_natural: "(s,t) \<in> C(c)  =  (\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t)"
-  by (fast elim: com2 dest: com1)
+lemma denotational_is_big_step: "(s,t) \<in> C(c)  =  ((c,s) \<Rightarrow> t)"
+by (fast elim: com2 dest: com1)
 
 end
diff -r 9ed5d8ad8fa0 -r faba4800b00b src/HOL/IMP/Examples.thy
--- a/src/HOL/IMP/Examples.thy	Wed Jun 01 19:50:59 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,81 +0,0 @@
-(*  Title:      HOL/IMP/Examples.thy
-    Author:     David von Oheimb, TUM
-*)
-
-header "Examples"
-
-theory Examples imports Natural begin
-
-definition
-  factorial :: "loc => loc => com" where
-  "factorial a b = (b :== (%s. 1);
-                    \<WHILE> (%s. s a ~= 0) \<DO>
-                    (b :== (%s. s b * s a); a :== (%s. s a - 1)))"
-
-declare update_def [simp]
-
-subsection "An example due to Tony Hoare"
-
-lemma lemma1:
-  assumes 1: "!x. P x \<longrightarrow> Q x"
-    and 2: "\<langle>w,s\<rangle> \<longrightarrow>\<^sub>c t"
-  shows "w = While P c \<Longrightarrow> \<langle>While Q c,t\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> \<langle>While Q c,s\<rangle> \<longrightarrow>\<^sub>c u"
-  using 2 apply induct
-  using 1 apply auto
-  done
-
-lemma lemma2 [rule_format (no_asm)]:
-  "[| !x. P x \<longrightarrow> Q x; \<langle>w,s\<rangle> \<longrightarrow>\<^sub>c u |] ==>
-  !c. w = While Q c \<longrightarrow> \<langle>While P c; While Q c,s\<rangle> \<longrightarrow>\<^sub>c u"
-apply (erule evalc.induct)
-apply (simp_all (no_asm_simp))
-apply blast
-apply (case_tac "P s")
-apply auto
-done
-
-lemma Hoare_example: "!x. P x \<longrightarrow> Q x ==>
-  (\<langle>While P c; While Q c, s\<rangle> \<longrightarrow>\<^sub>c t) = (\<langle>While Q c, s\<rangle> \<longrightarrow>\<^sub>c t)"
-  by (blast intro: lemma1 lemma2 dest: semi [THEN iffD1])
-
-
-subsection "Factorial"
-
-lemma factorial_3: "a~=b ==>
-    \<langle>factorial a b, Mem(a:=3)\<rangle> \<longrightarrow>\<^sub>c Mem(b:=6, a:=0)"
-  by (simp add: factorial_def)
-
-text {* the same in single step mode: *}
-lemmas [simp del] = evalc_cases
-lemma  "a~=b \<Longrightarrow> \<langle>factorial a b, Mem(a:=3)\<rangle> \<longrightarrow>\<^sub>c Mem(b:=6, a:=0)"
-apply (unfold factorial_def)
-apply (frule not_sym)
-apply (rule evalc.intros)
-apply  (rule evalc.intros)
-apply simp
-apply (rule evalc.intros)
-apply   simp
-apply  (rule evalc.intros)
-apply   (rule evalc.intros)
-apply  simp
-apply  (rule evalc.intros)
-apply simp
-apply (rule evalc.intros)
-apply   simp
-apply  (rule evalc.intros)
-apply   (rule evalc.intros)
-apply  simp
-apply  (rule evalc.intros)
-apply simp
-apply (rule evalc.intros)
-apply   simp
-apply  (rule evalc.intros)
-apply   (rule evalc.intros)
-apply  simp
-apply  (rule evalc.intros)
-apply simp
-apply (rule evalc.intros)
-apply simp
-done
-
-end
diff -r 9ed5d8ad8fa0 -r faba4800b00b src/HOL/IMP/Expr.thy
--- a/src/HOL/IMP/Expr.thy	Wed Jun 01 19:50:59 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,106 +0,0 @@
-(*  Title:      HOL/IMP/Expr.thy
-    Author:     Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
-*)
-
-header "Expressions"
-
-theory Expr imports Main begin
-
-text {*
-  Arithmetic expressions and Boolean expressions.
-  Not used in the rest of the language, but included for completeness.
-*}
-
-subsection "Arithmetic expressions"
-typedecl loc
-
-type_synonym state = "loc => nat"
-
-datatype
-  aexp = N nat
-       | X loc
-       | Op1 "nat => nat" aexp
-       | Op2 "nat => nat => nat" aexp aexp
-
-subsection "Evaluation of arithmetic expressions"
-
-inductive
-  evala :: "[aexp*state,nat] => bool"  (infixl "-a->" 50)
-where
-  N:   "(N(n),s) -a-> n"
-| X:   "(X(x),s) -a-> s(x)"
-| Op1: "(e,s) -a-> n ==> (Op1 f e,s) -a-> f(n)"
-| Op2: "[| (e0,s) -a-> n0;  (e1,s)  -a-> n1 |]
-        ==> (Op2 f e0 e1,s) -a-> f n0 n1"
-
-lemmas [intro] = N X Op1 Op2
-
-
-subsection "Boolean expressions"
-
-datatype
-  bexp = true
-       | false
-       | ROp  "nat => nat => bool" aexp aexp
-       | noti bexp
-       | andi bexp bexp         (infixl "andi" 60)
-       | ori  bexp bexp         (infixl "ori" 60)
-
-subsection "Evaluation of boolean expressions"
-
-inductive
-  evalb :: "[bexp*state,bool] => bool"  (infixl "-b->" 50)
-  -- "avoid clash with ML constructors true, false"
-where
-  tru:   "(true,s) -b-> True"
-| fls:   "(false,s) -b-> False"
-| ROp:   "[| (a0,s) -a-> n0; (a1,s) -a-> n1 |]
-          ==> (ROp f a0 a1,s) -b-> f n0 n1"
-| noti:  "(b,s) -b-> w ==> (noti(b),s) -b-> (~w)"
-| andi:  "[| (b0,s) -b-> w0; (b1,s) -b-> w1 |]
-          ==> (b0 andi b1,s) -b-> (w0 & w1)"
-| ori:   "[| (b0,s) -b-> w0; (b1,s) -b-> w1 |]
-          ==> (b0 ori b1,s) -b-> (w0 | w1)"
-
-lemmas [intro] = tru fls ROp noti andi ori
-
-subsection "Denotational semantics of arithmetic and boolean expressions"
-
-primrec A :: "aexp => state => nat"
-where
-  "A(N(n)) = (%s. n)"
-| "A(X(x)) = (%s. s(x))"
-| "A(Op1 f a) = (%s. f(A a s))"
-| "A(Op2 f a0 a1) = (%s. f (A a0 s) (A a1 s))"
-
-primrec B :: "bexp => state => bool"
-where
-  "B(true) = (%s. True)"
-| "B(false) = (%s. False)"
-| "B(ROp f a0 a1) = (%s. f (A a0 s) (A a1 s))"
-| "B(noti(b)) = (%s. ~(B b s))"
-| "B(b0 andi b1) = (%s. (B b0 s) & (B b1 s))"
-| "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))"
-
-inductive_simps
-  evala_simps [simp]:
-  "(N(n),s) -a-> n'" 
-  "(X(x),sigma) -a-> i"
-  "(Op1 f e,sigma) -a-> i"
-  "(Op2 f a1 a2,sigma) -a-> i"
-  "((true,sigma) -b-> w)"
-  "((false,sigma) -b-> w)"
-  "((ROp f a0 a1,sigma) -b-> w)"
-  "((noti(b),sigma) -b-> w)"
-  "((b0 andi b1,sigma) -b-> w)"
-  "((b0 ori b1,sigma) -b-> w)"
-
-
-lemma aexp_iff: "((a,s) -a-> n) = (A a s = n)"
-  by (induct a arbitrary: n) auto
-
-lemma bexp_iff:
-  "((b,s) -b-> w) = (B b s = w)"
-  by (induct b arbitrary: w) (auto simp add: aexp_iff)
-
-end
diff -r 9ed5d8ad8fa0 -r faba4800b00b src/HOL/IMP/Hoare.thy
--- a/src/HOL/IMP/Hoare.thy	Wed Jun 01 19:50:59 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-(*  Title:      HOL/IMP/Hoare.thy
-    Author:     Tobias Nipkow
-*)
-
-header "Inductive Definition of Hoare Logic"
-
-theory Hoare imports Natural begin
-
-type_synonym assn = "state => bool"
-
-inductive
-  hoare :: "assn => com => assn => bool" ("|- ({(1_)}/ (_)/ {(1_)})" 50)
-where
-  skip: "|- {P}\<SKIP>{P}"
-| ass:  "|- {%s. P(s[x\<mapsto>a s])} x:==a {P}"
-| semi: "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}"
-| If: "[| |- {%s. P s & b s}c{Q}; |- {%s. P s & ~b s}d{Q} |] ==>
-      |- {P} \<IF> b \<THEN> c \<ELSE> d {Q}"
-| While: "|- {%s. P s & b s} c {P} ==>
-         |- {P} \<WHILE> b \<DO> c {%s. P s & ~b s}"
-| conseq: "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==>
-          |- {P'}c{Q'}"
-
-lemma strengthen_pre: "[| !s. P' s --> P s; |- {P}c{Q} |] ==> |- {P'}c{Q}"
-by (blast intro: conseq)
-
-lemma weaken_post: "[| |- {P}c{Q}; !s. Q s --> Q' s |] ==> |- {P}c{Q'}"
-by (blast intro: conseq)
-
-lemma While':
-assumes "|- {%s. P s & b s} c {P}" and "ALL s. P s & \<not> b s \<longrightarrow> Q s"
-shows "|- {P} \<WHILE> b \<DO> c {Q}"
-by(rule weaken_post[OF While[OF assms(1)] assms(2)])
-
-
-lemmas [simp] = skip ass semi If
-
-lemmas [intro!] = hoare.skip hoare.ass hoare.semi hoare.If
-
-end
diff -r 9ed5d8ad8fa0 -r faba4800b00b src/HOL/IMP/Hoare_Den.thy
--- a/src/HOL/IMP/Hoare_Den.thy	Wed Jun 01 19:50:59 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,133 +0,0 @@
-(*  Title:      HOL/IMP/Hoare_Den.thy
-    Author:     Tobias Nipkow
-*)
-
-header "Soundness and Completeness wrt Denotational Semantics"
-
-theory Hoare_Den imports Hoare Denotation begin
-
-definition
-  hoare_valid :: "[assn,com,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50) where
-  "|= {P}c{Q} = (!s t. (s,t) : C(c) --> P s --> Q t)"
-
-
-lemma hoare_sound: "|- {P}c{Q} ==> |= {P}c{Q}"
-proof(induct rule: hoare.induct)
-  case (While P b c)
-  { fix s t
-    let ?G = "Gamma b (C c)"
-    assume "(s,t) \<in> lfp ?G"
-    hence "P s \<longrightarrow> P t \<and> \<not> b t"
-    proof(rule lfp_induct2)
-      show "mono ?G" by(rule Gamma_mono)
-    next
-      fix s t assume "(s,t) \<in> ?G (lfp ?G \<inter> {(s,t). P s \<longrightarrow> P t \<and> \<not> b t})"
-      thus "P s \<longrightarrow> P t \<and> \<not> b t" using While.hyps
-        by(auto simp: hoare_valid_def Gamma_def)
-    qed
-  }
-  thus ?case by(simp add:hoare_valid_def)
-qed (auto simp: hoare_valid_def)
-
-
-definition
-  wp :: "com => assn => assn" where
-  "wp c Q = (%s. !t. (s,t) : C(c) --> Q t)"
-
-lemma wp_SKIP: "wp \<SKIP> Q = Q"
-by (simp add: wp_def)
-
-lemma wp_Ass: "wp (x:==a) Q = (%s. Q(s[x\<mapsto>a s]))"
-by (simp add: wp_def)
-
-lemma wp_Semi: "wp (c;d) Q = wp c (wp d Q)"
-by (rule ext) (auto simp: wp_def)
-
-lemma wp_If:
- "wp (\<IF> b \<THEN> c \<ELSE> d) Q = (%s. (b s --> wp c Q s) &  (~b s --> wp d Q s))"
-by (rule ext) (auto simp: wp_def)
-
-lemma wp_While_If:
- "wp (\<WHILE> b \<DO> c) Q s =
-  wp (IF b THEN c;\<WHILE> b \<DO> c ELSE SKIP) Q s"
-by(simp only: wp_def C_While_If)
-
-(*Not suitable for rewriting: LOOPS!*)
-lemma wp_While_if:
-  "wp (\<WHILE> b \<DO> c) Q s = (if b s then wp (c;\<WHILE> b \<DO> c) Q s else Q s)"
-by(simp add:wp_While_If wp_If wp_SKIP)
-
-lemma wp_While_True: "b s ==>
-  wp (\<WHILE> b \<DO> c) Q s = wp (c;\<WHILE> b \<DO> c) Q s"
-by(simp add: wp_While_if)
-
-lemma wp_While_False: "~b s ==> wp (\<WHILE> b \<DO> c) Q s = Q s"
-by(simp add: wp_While_if)
-
-lemmas [simp] = wp_SKIP wp_Ass wp_Semi wp_If wp_While_True wp_While_False
-
-lemma wp_While: "wp (\<WHILE> b \<DO> c) Q s =
-   (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))"
-apply (simp (no_asm))
-apply (rule iffI)
- apply (rule weak_coinduct)
-  apply (erule CollectI)
- apply safe
-  apply simp
- apply simp
-apply (simp add: wp_def Gamma_def)
-apply (intro strip)
-apply (rule mp)
- prefer 2 apply (assumption)
-apply (erule lfp_induct2)
-apply (fast intro!: monoI)
-apply (subst gfp_unfold)
- apply (fast intro!: monoI)
-apply fast
-done
-
-declare C_while [simp del]
-
-lemma wp_is_pre: "|- {wp c Q} c {Q}"
-proof(induct c arbitrary: Q)
-  case SKIP show ?case by auto
-next
-  case Assign show ?case by auto
-next
-  case Semi thus ?case by auto
-next
-  case (Cond b c1 c2)
-  let ?If = "IF b THEN c1 ELSE c2"
-  show ?case
-  proof(rule If)
-    show "|- {\<lambda>s. wp ?If Q s \<and> b s} c1 {Q}"
-    proof(rule strengthen_pre[OF _ Cond(1)])
-      show "\<forall>s. wp ?If Q s \<and> b s \<longrightarrow> wp c1 Q s" by auto
-    qed
-    show "|- {\<lambda>s. wp ?If Q s \<and> \<not> b s} c2 {Q}"
-    proof(rule strengthen_pre[OF _ Cond(2)])
-      show "\<forall>s. wp ?If Q s \<and> \<not> b s \<longrightarrow> wp c2 Q s" by auto
-    qed
-  qed
-next
-  case (While b c)
-  let ?w = "WHILE b DO c"
-  show ?case
-  proof(rule While')
-    show "|- {\<lambda>s. wp ?w Q s \<and> b s} c {wp ?w Q}"
-    proof(rule strengthen_pre[OF _ While(1)])
-      show "\<forall>s. wp ?w Q s \<and> b s \<longrightarrow> wp c (wp ?w Q) s" by auto
-    qed
-    show "\<forall>s. wp ?w Q s \<and> \<not> b s \<longrightarrow> Q s" by auto
-  qed
-qed
-
-lemma hoare_relative_complete: assumes "|= {P}c{Q}" shows "|- {P}c{Q}"
-proof(rule conseq)
-  show "\<forall>s. P s \<longrightarrow> wp c Q s" using assms
-    by (auto simp: hoare_valid_def wp_def)
-  show "|- {wp c Q} c {Q}" by(rule wp_is_pre)
-  show "\<forall>s. Q s \<longrightarrow> Q s" by auto
-qed
-
-end
diff -r 9ed5d8ad8fa0 -r faba4800b00b src/HOL/IMP/Hoare_Op.thy
--- a/src/HOL/IMP/Hoare_Op.thy	Wed Jun 01 19:50:59 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,105 +0,0 @@
-(*  Title:      HOL/IMP/Hoare_Op.thy
-    Author:     Tobias Nipkow
-*)
-
-header "Soundness and Completeness wrt Operational Semantics"
-
-theory Hoare_Op imports Hoare begin
-
-definition
-  hoare_valid :: "[assn,com,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50) where
-  "|= {P}c{Q} = (!s t. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t --> P s --> Q t)"
-
-lemma hoare_sound: "|- {P}c{Q} ==> |= {P}c{Q}"
-proof(induct rule: hoare.induct)
-  case (While P b c)
-  { fix s t
-    assume "\<langle>WHILE b DO c,s\<rangle> \<longrightarrow>\<^sub>c t"
-    hence "P s \<longrightarrow> P t \<and> \<not> b t"
-    proof(induct "WHILE b DO c" s t)
-      case WhileFalse thus ?case by blast
-    next
-      case WhileTrue thus ?case
-        using While(2) unfolding hoare_valid_def by blast
-    qed
-
-  }
-  thus ?case unfolding hoare_valid_def by blast
-qed (auto simp: hoare_valid_def)
-
-definition
-  wp :: "com => assn => assn" where
-  "wp c Q = (%s. !t. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t --> Q t)"
-
-lemma wp_SKIP: "wp \<SKIP> Q = Q"
-by (simp add: wp_def)
-
-lemma wp_Ass: "wp (x:==a) Q = (%s. Q(s[x\<mapsto>a s]))"
-by (simp add: wp_def)
-
-lemma wp_Semi: "wp (c;d) Q = wp c (wp d Q)"
-by (rule ext) (auto simp: wp_def)
-
-lemma wp_If:
- "wp (\<IF> b \<THEN> c \<ELSE> d) Q = (%s. (b s --> wp c Q s) &  (~b s --> wp d Q s))"
-by (rule ext) (auto simp: wp_def)
-
-lemma wp_While_If:
- "wp (\<WHILE> b \<DO> c) Q s =
-  wp (IF b THEN c;\<WHILE> b \<DO> c ELSE SKIP) Q s"
-unfolding wp_def by (metis equivD1 equivD2 unfold_while)
-
-lemma wp_While_True: "b s ==>
-  wp (\<WHILE> b \<DO> c) Q s = wp (c;\<WHILE> b \<DO> c) Q s"
-by(simp add: wp_While_If wp_If wp_SKIP)
-
-lemma wp_While_False: "~b s ==> wp (\<WHILE> b \<DO> c) Q s = Q s"
-by(simp add: wp_While_If wp_If wp_SKIP)
-
-lemmas [simp] = wp_SKIP wp_Ass wp_Semi wp_If wp_While_True wp_While_False
-
-lemma wp_is_pre: "|- {wp c Q} c {Q}"
-proof(induct c arbitrary: Q)
-  case SKIP show ?case by auto
-next
-  case Assign show ?case by auto
-next
-  case Semi thus ?case by(auto intro: semi)
-next
-  case (Cond b c1 c2)
-  let ?If = "IF b THEN c1 ELSE c2"
-  show ?case
-  proof(rule If)
-    show "|- {\<lambda>s. wp ?If Q s \<and> b s} c1 {Q}"
-    proof(rule strengthen_pre[OF _ Cond(1)])
-      show "\<forall>s. wp ?If Q s \<and> b s \<longrightarrow> wp c1 Q s" by auto
-    qed
-    show "|- {\<lambda>s. wp ?If Q s \<and> \<not> b s} c2 {Q}"
-    proof(rule strengthen_pre[OF _ Cond(2)])
-      show "\<forall>s. wp ?If Q s \<and> \<not> b s \<longrightarrow> wp c2 Q s" by auto
-    qed
-  qed
-next
-  case (While b c)
-  let ?w = "WHILE b DO c"
-  have "|- {wp ?w Q} ?w {\<lambda>s. wp ?w Q s \<and> \<not> b s}"
-  proof(rule hoare.While)
-    show "|- {\<lambda>s. wp ?w Q s \<and> b s} c {wp ?w Q}"
-    proof(rule strengthen_pre[OF _ While(1)])
-      show "\<forall>s. wp ?w Q s \<and> b s \<longrightarrow> wp c (wp ?w Q) s" by auto
-    qed
-  qed
-  thus ?case
-  proof(rule weaken_post)
-    show "\<forall>s. wp ?w Q s \<and> \<not> b s \<longrightarrow> Q s" by auto
-  qed
-qed
-
-lemma hoare_relative_complete: assumes "|= {P}c{Q}" shows "|- {P}c{Q}"
-proof(rule strengthen_pre)
-  show "\<forall>s. P s \<longrightarrow> wp c Q s" using assms
-    by (auto simp: hoare_valid_def wp_def)
-  show "|- {wp c Q} c {Q}" by(rule wp_is_pre)
-qed
-
-end
diff -r 9ed5d8ad8fa0 -r faba4800b00b src/HOL/IMP/Live.thy
--- a/src/HOL/IMP/Live.thy	Wed Jun 01 19:50:59 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,212 +0,0 @@
-theory Live imports Natural
-begin
-
-text{* Which variables/locations does an expression depend on?
-Any set of variables that completely determine the value of the expression,
-in the worst case all locations: *}
-
-consts Dep :: "((loc \<Rightarrow> 'a) \<Rightarrow> 'b) \<Rightarrow> loc set"
-specification (Dep)
-dep_on: "(\<forall>x\<in>Dep e. s x = t x) \<Longrightarrow> e s = e t"
-by(rule_tac x="%x. UNIV" in exI)(simp add: fun_eq_iff[symmetric])
-
-text{* The following definition of @{const Dep} looks very tempting
-@{prop"Dep e = {a. EX s t. (ALL x. x\<noteq>a \<longrightarrow> s x = t x) \<and> e s \<noteq> e t}"}
-but does not work in case @{text e} depends on an infinite set of variables.
-For example, if @{term"e s"} tests if @{text s} is 0 at infinitely many locations. Then @{term"Dep e"} incorrectly yields the empty set!
-
-If we had a concrete representation of expressions, we would simply write
-a recursive free-variables function.
-*}
-
-primrec L :: "com \<Rightarrow> loc set \<Rightarrow> loc set" where
-"L SKIP A = A" |
-"L (x :== e) A = A-{x} \<union> Dep e" |
-"L (c1; c2) A = (L c1 \<circ> L c2) A" |
-"L (IF b THEN c1 ELSE c2) A = Dep b \<union> L c1 A \<union> L c2 A" |
-"L (WHILE b DO c) A = Dep b \<union> A \<union> L c A"
-
-primrec "kill" :: "com \<Rightarrow> loc set" where
-"kill SKIP = {}" |
-"kill (x :== e) = {x}" |
-"kill (c1; c2) = kill c1 \<union> kill c2" |
-"kill (IF b THEN c1 ELSE c2) = Dep b \<union> kill c1 \<inter>  kill c2" |
-"kill (WHILE b DO c) = {}"
-
-primrec gen :: "com \<Rightarrow> loc set" where
-"gen SKIP = {}" |
-"gen (x :== e) = Dep e" |
-"gen (c1; c2) = gen c1 \<union> (gen c2-kill c1)" |
-"gen (IF b THEN c1 ELSE c2) = Dep b \<union> gen c1 \<union> gen c2" |
-"gen (WHILE b DO c) = Dep b \<union> gen c"
-
-lemma L_gen_kill: "L c A = gen c \<union> (A - kill c)"
-by(induct c arbitrary:A) auto
-
-lemma L_idemp: "L c (L c A) \<subseteq> L c A"
-by(fastsimp simp add:L_gen_kill)
-
-theorem L_sound: "\<forall> x \<in> L c A. s x = t x \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>c,t\<rangle> \<longrightarrow>\<^sub>c t' \<Longrightarrow>
- \<forall>x\<in>A. s' x = t' x"
-proof (induct c arbitrary: A s t s' t')
-  case SKIP then show ?case by auto
-next
-  case (Assign x e) then show ?case
-    by (auto simp:update_def ball_Un dest!: dep_on)
-next
-  case (Semi c1 c2)
-  from Semi(4) obtain s'' where s1: "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s''" and s2: "\<langle>c2,s''\<rangle> \<longrightarrow>\<^sub>c s'"
-    by auto
-  from Semi(5) obtain t'' where t1: "\<langle>c1,t\<rangle> \<longrightarrow>\<^sub>c t''" and t2: "\<langle>c2,t''\<rangle> \<longrightarrow>\<^sub>c t'"
-    by auto
-  show ?case using Semi(1)[OF _ s1 t1] Semi(2)[OF _ s2 t2] Semi(3) by fastsimp
-next
-  case (Cond b c1 c2)
-  show ?case
-  proof cases
-    assume "b s"
-    hence s: "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s'" using Cond(4) by simp
-    have "b t" using `b s` Cond(3) by (simp add: ball_Un)(blast dest: dep_on)
-    hence t: "\<langle>c1,t\<rangle> \<longrightarrow>\<^sub>c t'" using Cond(5) by auto
-    show ?thesis using Cond(1)[OF _ s t] Cond(3) by fastsimp
-  next
-    assume "\<not> b s"
-    hence s: "\<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c s'" using Cond(4) by auto
-    have "\<not> b t" using `\<not> b s` Cond(3) by (simp add: ball_Un)(blast dest: dep_on)
-    hence t: "\<langle>c2,t\<rangle> \<longrightarrow>\<^sub>c t'" using Cond(5) by auto
-    show ?thesis using Cond(2)[OF _ s t] Cond(3) by fastsimp
-  qed
-next
-  case (While b c) note IH = this
-  { fix cw
-    have "\<langle>cw,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> cw = (While b c) \<Longrightarrow> \<langle>cw,t\<rangle> \<longrightarrow>\<^sub>c t' \<Longrightarrow>
-          \<forall> x \<in> L cw A. s x = t x \<Longrightarrow> \<forall>x\<in>A. s' x = t' x"
-    proof (induct arbitrary: t A pred:evalc)
-      case WhileFalse
-      have "\<not> b t" using WhileFalse by (simp add: ball_Un)(blast dest:dep_on)
-      then have "t' = t" using WhileFalse by auto
-      then show ?case using WhileFalse by auto
-    next
-      case (WhileTrue _ s _ s'' s')
-      have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''" using WhileTrue(2,6) by simp
-      have "b t" using WhileTrue by (simp add: ball_Un)(blast dest:dep_on)
-      then obtain t'' where "\<langle>c,t\<rangle> \<longrightarrow>\<^sub>c t''" and "\<langle>While b c,t''\<rangle> \<longrightarrow>\<^sub>c t'"
-        using WhileTrue(6,7) by auto
-      have "\<forall>x\<in>Dep b \<union> A \<union> L c A. s'' x = t'' x"
-        using IH(1)[OF _ `\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''` `\<langle>c,t\<rangle> \<longrightarrow>\<^sub>c t''`] WhileTrue(6,8)
-        by (auto simp:L_gen_kill)
-      then have "\<forall>x\<in>L (While b c) A. s'' x = t'' x" by auto
-      then show ?case using WhileTrue(5,6) `\<langle>While b c,t''\<rangle> \<longrightarrow>\<^sub>c t'` by metis
-    qed auto }
--- "a terser version"
-  { let ?w = "While b c"
-    have "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>?w,t\<rangle> \<longrightarrow>\<^sub>c t' \<Longrightarrow>
-          \<forall> x \<in> L ?w A. s x = t x \<Longrightarrow> \<forall>x\<in>A. s' x = t' x"
-    proof (induct ?w s s' arbitrary: t A pred:evalc)
-      case WhileFalse
-      have "\<not> b t" using WhileFalse by (simp add: ball_Un)(blast dest:dep_on)
-      then have "t' = t" using WhileFalse by auto
-      then show ?case using WhileFalse by simp
-    next
-      case (WhileTrue s s'' s')
-      have "b t" using WhileTrue by (simp add: ball_Un)(blast dest:dep_on)
-      then obtain t'' where "\<langle>c,t\<rangle> \<longrightarrow>\<^sub>c t''" and "\<langle>While b c,t''\<rangle> \<longrightarrow>\<^sub>c t'"
-        using WhileTrue(6,7) by auto
-      have "\<forall>x\<in>Dep b \<union> A \<union> L c A. s'' x = t'' x"
-        using IH(1)[OF _ `\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''` `\<langle>c,t\<rangle> \<longrightarrow>\<^sub>c t''`] WhileTrue(7)
-        by (auto simp:L_gen_kill)
-      then have "\<forall>x\<in>L (While b c) A. s'' x = t'' x" by auto
-      then show ?case using WhileTrue(5) `\<langle>While b c,t''\<rangle> \<longrightarrow>\<^sub>c t'` by metis
-    qed }
-  from this[OF IH(3) IH(4,2)] show ?case by metis
-qed
-
-
-primrec bury :: "com \<Rightarrow> loc set \<Rightarrow> com" where
-"bury SKIP _ = SKIP" |
-"bury (x :== e) A = (if x:A then x:== e else SKIP)" |
-"bury (c1; c2) A = (bury c1 (L c2 A); bury c2 A)" |
-"bury (IF b THEN c1 ELSE c2) A = (IF b THEN bury c1 A ELSE bury c2 A)" |
-"bury (WHILE b DO c) A = (WHILE b DO bury c (Dep b \<union> A \<union> L c A))"
-
-theorem bury_sound:
-  "\<forall> x \<in> L c A. s x = t x \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>bury c A,t\<rangle> \<longrightarrow>\<^sub>c t' \<Longrightarrow>
-   \<forall>x\<in>A. s' x = t' x"
-proof (induct c arbitrary: A s t s' t')
-  case SKIP then show ?case by auto
-next
-  case (Assign x e) then show ?case
-    by (auto simp:update_def ball_Un split:split_if_asm dest!: dep_on)
-next
-  case (Semi c1 c2)
-  from Semi(4) obtain s'' where s1: "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s''" and s2: "\<langle>c2,s''\<rangle> \<longrightarrow>\<^sub>c s'"
-    by auto
-  from Semi(5) obtain t'' where t1: "\<langle>bury c1 (L c2 A),t\<rangle> \<longrightarrow>\<^sub>c t''" and t2: "\<langle>bury c2 A,t''\<rangle> \<longrightarrow>\<^sub>c t'"
-    by auto
-  show ?case using Semi(1)[OF _ s1 t1] Semi(2)[OF _ s2 t2] Semi(3) by fastsimp
-next
-  case (Cond b c1 c2)
-  show ?case
-  proof cases
-    assume "b s"
-    hence s: "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s'" using Cond(4) by simp
-    have "b t" using `b s` Cond(3) by (simp add: ball_Un)(blast dest: dep_on)
-    hence t: "\<langle>bury c1 A,t\<rangle> \<longrightarrow>\<^sub>c t'" using Cond(5) by auto
-    show ?thesis using Cond(1)[OF _ s t] Cond(3) by fastsimp
-  next
-    assume "\<not> b s"
-    hence s: "\<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c s'" using Cond(4) by auto
-    have "\<not> b t" using `\<not> b s` Cond(3) by (simp add: ball_Un)(blast dest: dep_on)
-    hence t: "\<langle>bury c2 A,t\<rangle> \<longrightarrow>\<^sub>c t'" using Cond(5) by auto
-    show ?thesis using Cond(2)[OF _ s t] Cond(3) by fastsimp
-  qed
-next
-  case (While b c) note IH = this
-  { fix cw
-    have "\<langle>cw,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> cw = (While b c) \<Longrightarrow> \<langle>bury cw A,t\<rangle> \<longrightarrow>\<^sub>c t' \<Longrightarrow>
-          \<forall> x \<in> L cw A. s x = t x \<Longrightarrow> \<forall>x\<in>A. s' x = t' x"
-    proof (induct arbitrary: t A pred:evalc)
-      case WhileFalse
-      have "\<not> b t" using WhileFalse by (simp add: ball_Un)(blast dest:dep_on)
-      then have "t' = t" using WhileFalse by auto
-      then show ?case using WhileFalse by auto
-    next
-      case (WhileTrue _ s _ s'' s')
-      have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''" using WhileTrue(2,6) by simp
-      have "b t" using WhileTrue by (simp add: ball_Un)(blast dest:dep_on)
-      then obtain t'' where tt'': "\<langle>bury c (Dep b \<union> A \<union> L c A),t\<rangle> \<longrightarrow>\<^sub>c t''"
-        and "\<langle>bury (While b c) A,t''\<rangle> \<longrightarrow>\<^sub>c t'"
-        using WhileTrue(6,7) by auto
-      have "\<forall>x\<in>Dep b \<union> A \<union> L c A. s'' x = t'' x"
-        using IH(1)[OF _ `\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''` tt''] WhileTrue(6,8)
-        by (auto simp:L_gen_kill)
-      moreover then have "\<forall>x\<in>L (While b c) A. s'' x = t'' x" by auto
-      ultimately show ?case
-        using WhileTrue(5,6) `\<langle>bury (While b c) A,t''\<rangle> \<longrightarrow>\<^sub>c t'` by metis
-    qed auto }
-  { let ?w = "While b c"
-    have "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>bury ?w A,t\<rangle> \<longrightarrow>\<^sub>c t' \<Longrightarrow>
-          \<forall> x \<in> L ?w A. s x = t x \<Longrightarrow> \<forall>x\<in>A. s' x = t' x"
-    proof (induct ?w s s' arbitrary: t A pred:evalc)
-      case WhileFalse
-      have "\<not> b t" using WhileFalse by (simp add: ball_Un)(blast dest:dep_on)
-      then have "t' = t" using WhileFalse by auto
-      then show ?case using WhileFalse by simp
-    next
-      case (WhileTrue s s'' s')
-      have "b t" using WhileTrue by (simp add: ball_Un)(blast dest:dep_on)
-      then obtain t'' where tt'': "\<langle>bury c (Dep b \<union> A \<union> L c A),t\<rangle> \<longrightarrow>\<^sub>c t''"
-        and "\<langle>bury (While b c) A,t''\<rangle> \<longrightarrow>\<^sub>c t'"
-        using WhileTrue(6,7) by auto
-      have "\<forall>x\<in>Dep b \<union> A \<union> L c A. s'' x = t'' x"
-        using IH(1)[OF _ `\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''` tt''] WhileTrue(7)
-        by (auto simp:L_gen_kill)
-      then have "\<forall>x\<in>L (While b c) A. s'' x = t'' x" by auto
-      then show ?case
-        using WhileTrue(5) `\<langle>bury (While b c) A,t''\<rangle> \<longrightarrow>\<^sub>c t'` by metis
-    qed }
-  from this[OF IH(3) IH(4,2)] show ?case by metis
-qed
-
-
-end
\ No newline at end of file
diff -r 9ed5d8ad8fa0 -r faba4800b00b src/HOL/IMP/Machines.thy
--- a/src/HOL/IMP/Machines.thy	Wed Jun 01 19:50:59 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,182 +0,0 @@
-theory Machines
-imports Natural
-begin
-
-lemma converse_in_rel_pow_eq:
-  "((x,z) \<in> R ^^ n) = (n=0 \<and> z=x \<or> (\<exists>m y. n = Suc m \<and> (x,y) \<in> R \<and> (y,z) \<in> R ^^ m))"
-apply(rule iffI)
- apply(blast elim:rel_pow_E2)
-apply (auto simp: rel_pow_commute[symmetric])
-done
-
-subsection "Instructions"
-
-text {* There are only three instructions: *}
-datatype instr = SET loc aexp | JMPF bexp nat | JMPB nat
-
-type_synonym instrs = "instr list"
-
-subsection "M0 with PC"
-
-inductive_set
-  exec01 :: "instr list \<Rightarrow> ((nat\<times>state) \<times> (nat\<times>state))set"
-  and exec01' :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
-    ("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -1\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
-  for P :: "instr list"
-where
-  "p \<turnstile> \<langle>i,s\<rangle> -1\<rightarrow> \<langle>j,t\<rangle> == ((i,s),j,t) : (exec01 p)"
-| SET: "\<lbrakk> n<size P; P!n = SET x a \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>n,s\<rangle> -1\<rightarrow> \<langle>Suc n,s[x\<mapsto> a s]\<rangle>"
-| JMPFT: "\<lbrakk> n<size P; P!n = JMPF b i;  b s \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>n,s\<rangle> -1\<rightarrow> \<langle>Suc n,s\<rangle>"
-| JMPFF: "\<lbrakk> n<size P; P!n = JMPF b i; \<not>b s; m=n+i+1; m \<le> size P \<rbrakk>
-        \<Longrightarrow> P \<turnstile> \<langle>n,s\<rangle> -1\<rightarrow> \<langle>m,s\<rangle>"
-| JMPB:  "\<lbrakk> n<size P; P!n = JMPB i; i \<le> n; j = n-i \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>n,s\<rangle> -1\<rightarrow> \<langle>j,s\<rangle>"
-
-abbreviation
-  exec0s :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
-    ("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -*\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)  where
-  "p \<turnstile> \<langle>i,s\<rangle> -*\<rightarrow> \<langle>j,t\<rangle> == ((i,s),j,t) : (exec01 p)^*"
-
-abbreviation
-  exec0n :: "[instrs, nat,state, nat, nat,state] \<Rightarrow> bool"
-    ("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)  where
-  "p \<turnstile> \<langle>i,s\<rangle> -n\<rightarrow> \<langle>j,t\<rangle> == ((i,s),j,t) : (exec01 p)^^n"
-
-subsection "M0 with lists"
-
-text {* We describe execution of programs in the machine by
-  an operational (small step) semantics:
-*}
-
-type_synonym config = "instrs \<times> instrs \<times> state"
-
-
-inductive_set
-  stepa1 :: "(config \<times> config)set"
-  and stepa1' :: "[instrs,instrs,state, instrs,instrs,state] \<Rightarrow> bool"
-    ("((1\<langle>_,/_,/_\<rangle>)/ -1\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50)
-where
-  "\<langle>p,q,s\<rangle> -1\<rightarrow> \<langle>p',q',t\<rangle> == ((p,q,s),p',q',t) : stepa1"
-| "\<langle>SET x a#p,q,s\<rangle> -1\<rightarrow> \<langle>p,SET x a#q,s[x\<mapsto> a s]\<rangle>"
-| "b s \<Longrightarrow> \<langle>JMPF b i#p,q,s\<rangle> -1\<rightarrow> \<langle>p,JMPF b i#q,s\<rangle>"
-| "\<lbrakk> \<not> b s; i \<le> size p \<rbrakk>
-   \<Longrightarrow> \<langle>JMPF b i # p, q, s\<rangle> -1\<rightarrow> \<langle>drop i p, rev(take i p) @ JMPF b i # q, s\<rangle>"
-| "i \<le> size q
-   \<Longrightarrow> \<langle>JMPB i # p, q, s\<rangle> -1\<rightarrow> \<langle>rev(take i q) @ JMPB i # p, drop i q, s\<rangle>"
-
-abbreviation
-  stepa :: "[instrs,instrs,state, instrs,instrs,state] \<Rightarrow> bool"
-    ("((1\<langle>_,/_,/_\<rangle>)/ -*\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50)  where
-  "\<langle>p,q,s\<rangle> -*\<rightarrow> \<langle>p',q',t\<rangle> == ((p,q,s),p',q',t) : (stepa1^*)"
-
-abbreviation
-  stepan :: "[instrs,instrs,state, nat, instrs,instrs,state] \<Rightarrow> bool"
-    ("((1\<langle>_,/_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50) where
-  "\<langle>p,q,s\<rangle> -i\<rightarrow> \<langle>p',q',t\<rangle> == ((p,q,s),p',q',t) : (stepa1^^i)"
-
-inductive_cases execE: "((i#is,p,s), (is',p',s')) : stepa1"
-
-lemma exec_simp[simp]:
- "(\<langle>i#p,q,s\<rangle> -1\<rightarrow> \<langle>p',q',t\<rangle>) = (case i of
- SET x a \<Rightarrow> t = s[x\<mapsto> a s] \<and> p' = p \<and> q' = i#q |
- JMPF b n \<Rightarrow> t=s \<and> (if b s then p' = p \<and> q' = i#q
-            else n \<le> size p \<and> p' = drop n p \<and> q' = rev(take n p) @ i # q) |
- JMPB n \<Rightarrow> n \<le> size q \<and> t=s \<and> p' = rev(take n q) @ i # p \<and> q' = drop n q)"
-apply(rule iffI)
-defer
-apply(clarsimp simp add: stepa1.intros split: instr.split_asm split_if_asm)
-apply(erule execE)
-apply(simp_all)
-done
-
-lemma execn_simp[simp]:
-"(\<langle>i#p,q,s\<rangle> -n\<rightarrow> \<langle>p'',q'',u\<rangle>) =
- (n=0 \<and> p'' = i#p \<and> q'' = q \<and> u = s \<or>
-  ((\<exists>m p' q' t. n = Suc m \<and>
-                \<langle>i#p,q,s\<rangle> -1\<rightarrow> \<langle>p',q',t\<rangle> \<and> \<langle>p',q',t\<rangle> -m\<rightarrow> \<langle>p'',q'',u\<rangle>)))"
-by(subst converse_in_rel_pow_eq, simp)
-
-
-lemma exec_star_simp[simp]: "(\<langle>i#p,q,s\<rangle> -*\<rightarrow> \<langle>p'',q'',u\<rangle>) =
- (p'' = i#p & q''=q & u=s |
- (\<exists>p' q' t. \<langle>i#p,q,s\<rangle> -1\<rightarrow> \<langle>p',q',t\<rangle> \<and> \<langle>p',q',t\<rangle> -*\<rightarrow> \<langle>p'',q'',u\<rangle>))"
-apply(simp add: rtrancl_is_UN_rel_pow del:exec_simp)
-apply(blast)
-done
-
-declare nth_append[simp]
-
-lemma rev_revD: "rev xs = rev ys \<Longrightarrow> xs = ys"
-by simp
-
-lemma [simp]: "(rev xs @ rev ys = rev zs) = (ys @ xs = zs)"
-apply(rule iffI)
- apply(rule rev_revD, simp)
-apply fastsimp
-done
-
-lemma direction1:
- "\<langle>q,p,s\<rangle> -1\<rightarrow> \<langle>q',p',t\<rangle> \<Longrightarrow>
-  rev p' @ q' = rev p @ q \<and> rev p @ q \<turnstile> \<langle>size p,s\<rangle> -1\<rightarrow> \<langle>size p',t\<rangle>"
-apply(induct set: stepa1)
-   apply(simp add:exec01.SET)
-  apply(fastsimp intro:exec01.JMPFT)
- apply simp
- apply(rule exec01.JMPFF)
-     apply simp
-    apply fastsimp
-   apply simp
-  apply simp
- apply simp
-apply(fastsimp simp add:exec01.JMPB)
-done
-
-(*
-lemma rev_take: "\<And>i. rev (take i xs) = drop (length xs - i) (rev xs)"
-apply(induct xs)
- apply simp_all
-apply(case_tac i)
-apply simp_all
-done
-
-lemma rev_drop: "\<And>i. rev (drop i xs) = take (length xs - i) (rev xs)"
-apply(induct xs)
- apply simp_all
-apply(case_tac i)
-apply simp_all
-done
-*)
-
-lemma direction2:
- "rpq \<turnstile> \<langle>sp,s\<rangle> -1\<rightarrow> \<langle>sp',t\<rangle> \<Longrightarrow>
-  rpq = rev p @ q & sp = size p & sp' = size p' \<longrightarrow>
-          rev p' @ q' = rev p @ q \<longrightarrow> \<langle>q,p,s\<rangle> -1\<rightarrow> \<langle>q',p',t\<rangle>"
-apply(induct arbitrary: p q p' q' set: exec01)
-   apply(clarsimp simp add: neq_Nil_conv append_eq_conv_conj)
-   apply(drule sym)
-   apply simp
-   apply(rule rev_revD)
-   apply simp
-  apply(clarsimp simp add: neq_Nil_conv append_eq_conv_conj)
-  apply(drule sym)
-  apply simp
-  apply(rule rev_revD)
-  apply simp
- apply(simp (no_asm_use) add: neq_Nil_conv append_eq_conv_conj, clarify)+
- apply(drule sym)
- apply simp
- apply(rule rev_revD)
- apply simp
-apply(clarsimp simp add: neq_Nil_conv append_eq_conv_conj)
-apply(drule sym)
-apply(simp add:rev_take)
-apply(rule rev_revD)
-apply(simp add:rev_drop)
-done
-
-
-theorem M_eqiv:
-"(\<langle>q,p,s\<rangle> -1\<rightarrow> \<langle>q',p',t\<rangle>) =
- (rev p' @ q' = rev p @ q \<and> rev p @ q \<turnstile> \<langle>size p,s\<rangle> -1\<rightarrow> \<langle>size p',t\<rangle>)"
-  by (blast dest: direction1 direction2)
-
-end
diff -r 9ed5d8ad8fa0 -r faba4800b00b src/HOL/IMP/Natural.thy
--- a/src/HOL/IMP/Natural.thy	Wed Jun 01 19:50:59 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,354 +0,0 @@
-(*  Title:        HOL/IMP/Natural.thy
-    Author:       Tobias Nipkow & Robert Sandner, TUM
-    Isar Version: Gerwin Klein, 2001; additional proofs by Lawrence Paulson
-    Copyright     1996 TUM
-*)
-
-header "Natural Semantics of Commands"
-
-theory Natural imports Com begin
-
-subsection "Execution of commands"
-
-text {*
-  We write @{text "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"} for \emph{Statement @{text c}, started
-  in state @{text s}, terminates in state @{text s'}}. Formally,
-  @{text "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"} is just another form of saying \emph{the tuple
-  @{text "(c,s,s')"} is part of the relation @{text evalc}}:
-*}
-
-definition
-  update :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("_/[_ ::= /_]" [900,0,0] 900) where
-  "update = fun_upd"
-
-notation (xsymbols)
-  update  ("_/[_ \<mapsto> /_]" [900,0,0] 900)
-
-text {* Disable conflicting syntax from HOL Map theory. *}
-
-no_syntax
-  "_maplet"  :: "['a, 'a] => maplet"             ("_ /|->/ _")
-  "_maplets" :: "['a, 'a] => maplet"             ("_ /[|->]/ _")
-  ""         :: "maplet => maplets"             ("_")
-  "_Maplets" :: "[maplet, maplets] => maplets" ("_,/ _")
-  "_MapUpd"  :: "['a ~=> 'b, maplets] => 'a ~=> 'b" ("_/'(_')" [900,0]900)
-  "_Map"     :: "maplets => 'a ~=> 'b"            ("(1[_])")
-
-text {*
-  The big-step execution relation @{text evalc} is defined inductively:
-*}
-inductive
-  evalc :: "[com,state,state] \<Rightarrow> bool" ("\<langle>_,_\<rangle>/ \<longrightarrow>\<^sub>c _" [0,0,60] 60)
-where
-  Skip:    "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s"
-| Assign:  "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s[x\<mapsto>a s]"
-
-| Semi:    "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'' \<Longrightarrow> \<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>c0; c1, s\<rangle> \<longrightarrow>\<^sub>c s'"
-
-| IfTrue:  "b s \<Longrightarrow> \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s'"
-| IfFalse: "\<not>b s \<Longrightarrow> \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s'"
-
-| WhileFalse: "\<not>b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c s"
-| WhileTrue:  "b s \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'' \<Longrightarrow> \<langle>\<WHILE> b \<DO> c, s''\<rangle> \<longrightarrow>\<^sub>c s'
-               \<Longrightarrow> \<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>c s'"
-
-lemmas evalc.intros [intro] -- "use those rules in automatic proofs"
-
-text {*
-The induction principle induced by this definition looks like this:
-
-@{thm [display] evalc.induct [no_vars]}
-
-
-(@{text "\<And>"} and @{text "\<Longrightarrow>"} are Isabelle's
-  meta symbols for @{text "\<forall>"} and @{text "\<longrightarrow>"})
-*}
-
-text {*
-  The rules of @{text evalc} are syntax directed, i.e.~for each
-  syntactic category there is always only one rule applicable. That
-  means we can use the rules in both directions.  This property is called rule inversion.
-*}
-inductive_cases skipE [elim!]:   "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s'"
-inductive_cases semiE [elim!]:   "\<langle>c0; c1, s\<rangle> \<longrightarrow>\<^sub>c s'"
-inductive_cases assignE [elim!]: "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s'"
-inductive_cases ifE [elim!]:     "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s'"
-inductive_cases whileE [elim]:  "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c s'"
-
-text {* The next proofs are all trivial by rule inversion.
-*}
-
-inductive_simps
-  skip: "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s'"
-  and assign: "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s'"
-  and semi: "\<langle>c0; c1, s\<rangle> \<longrightarrow>\<^sub>c s'"
-
-lemma ifTrue:
-  "b s \<Longrightarrow> \<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'"
-  by auto
-
-lemma ifFalse:
-  "\<not>b s \<Longrightarrow> \<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s'"
-  by auto
-
-lemma whileFalse:
-  "\<not> b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c s' = (s' = s)"
-  by auto
-
-lemma whileTrue:
-  "b s \<Longrightarrow>
-  \<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>c s' =
-  (\<exists>s''. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'' \<and> \<langle>\<WHILE> b \<DO> c, s''\<rangle> \<longrightarrow>\<^sub>c s')"
-  by auto
-
-text "Again, Isabelle may use these rules in automatic proofs:"
-lemmas evalc_cases [simp] = skip assign ifTrue ifFalse whileFalse semi whileTrue
-
-subsection "Equivalence of statements"
-
-text {*
-  We call two statements @{text c} and @{text c'} equivalent wrt.~the
-  big-step semantics when \emph{@{text c} started in @{text s} terminates
-  in @{text s'} iff @{text c'} started in the same @{text s} also terminates
-  in the same @{text s'}}. Formally:
-*}
-definition
-  equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" ("_ \<sim> _" [56, 56] 55) where
-  "c \<sim> c' = (\<forall>s s'. \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s')"
-
-text {*
-  Proof rules telling Isabelle to unfold the definition
-  if there is something to be proved about equivalent
-  statements: *}
-lemma equivI [intro!]:
-  "(\<And>s s'. \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s') \<Longrightarrow> c \<sim> c'"
-  by (unfold equiv_c_def) blast
-
-lemma equivD1:
-  "c \<sim> c' \<Longrightarrow> \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s'"
-  by (unfold equiv_c_def) blast
-
-lemma equivD2:
-  "c \<sim> c' \<Longrightarrow> \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s'"
-  by (unfold equiv_c_def) blast
-
-text {*
-  As an example, we show that loop unfolding is an equivalence
-  transformation on programs:
-*}
-lemma unfold_while:
-  "(\<WHILE> b \<DO> c) \<sim> (\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>)" (is "?w \<sim> ?if")
-proof -
-  -- "to show the equivalence, we look at the derivation tree for"
-  -- "each side and from that construct a derivation tree for the other side"
-  { fix s s' assume w: "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'"
-    -- "as a first thing we note that, if @{text b} is @{text False} in state @{text s},"
-    -- "then both statements do nothing:"
-    hence "\<not>b s \<Longrightarrow> s = s'" by blast
-    hence "\<not>b s \<Longrightarrow> \<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
-    moreover
-    -- "on the other hand, if @{text b} is @{text True} in state @{text s},"
-    -- {* then only the @{text WhileTrue} rule can have been used to derive @{text "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'"} *}
-    { assume b: "b s"
-      with w obtain s'' where
-        "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s''" and "\<langle>?w, s''\<rangle> \<longrightarrow>\<^sub>c s'" by (cases set: evalc) auto
-      -- "now we can build a derivation tree for the @{text \<IF>}"
-      -- "first, the body of the True-branch:"
-      hence "\<langle>c; ?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by (rule Semi)
-      -- "then the whole @{text \<IF>}"
-      with b have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'" by (rule IfTrue)
-    }
-    ultimately
-    -- "both cases together give us what we want:"
-    have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
-  }
-  moreover
-  -- "now the other direction:"
-  { fix s s' assume "if": "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'"
-    -- "again, if @{text b} is @{text False} in state @{text s}, then the False-branch"
-    -- "of the @{text \<IF>} is executed, and both statements do nothing:"
-    hence "\<not>b s \<Longrightarrow> s = s'" by blast
-    hence "\<not>b s \<Longrightarrow> \<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
-    moreover
-    -- "on the other hand, if @{text b} is @{text True} in state @{text s},"
-    -- {* then this time only the @{text IfTrue} rule can have be used *}
-    { assume b: "b s"
-      with "if" have "\<langle>c; ?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by (cases set: evalc) auto
-      -- "and for this, only the Semi-rule is applicable:"
-      then obtain s'' where
-        "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s''" and "\<langle>?w, s''\<rangle> \<longrightarrow>\<^sub>c s'" by (cases set: evalc) auto
-      -- "with this information, we can build a derivation tree for the @{text \<WHILE>}"
-      with b
-      have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by (rule WhileTrue)
-    }
-    ultimately
-    -- "both cases together again give us what we want:"
-    have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
-  }
-  ultimately
-  show ?thesis by blast
-qed
-
-text {*
-   Happily, such lengthy proofs are seldom necessary.  Isabelle can prove many such facts automatically.
-*}
-
-lemma 
-  "(\<WHILE> b \<DO> c) \<sim> (\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>)"
-by blast
-
-lemma triv_if:
-  "(\<IF> b \<THEN> c \<ELSE> c) \<sim> c"
-by blast
-
-lemma commute_if:
-  "(\<IF> b1 \<THEN> (\<IF> b2 \<THEN> c11 \<ELSE> c12) \<ELSE> c2) 
-   \<sim> 
-   (\<IF> b2 \<THEN> (\<IF> b1 \<THEN> c11 \<ELSE> c2) \<ELSE> (\<IF> b1 \<THEN> c12 \<ELSE> c2))"
-by blast
-
-lemma while_equiv:
-  "\<langle>c0, s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> c \<sim> c' \<Longrightarrow> (c0 = \<WHILE> b \<DO> c) \<Longrightarrow> \<langle>\<WHILE> b \<DO> c', s\<rangle> \<longrightarrow>\<^sub>c u" 
-by (induct rule: evalc.induct) (auto simp add: equiv_c_def) 
-
-lemma equiv_while:
-  "c \<sim> c' \<Longrightarrow> (\<WHILE> b \<DO> c) \<sim> (\<WHILE> b \<DO> c')"
-by (simp add: equiv_c_def) (metis equiv_c_def while_equiv) 
-
-
-text {*
-    Program equivalence is an equivalence relation.
-*}
-
-lemma equiv_refl:
-  "c \<sim> c"
-by blast
-
-lemma equiv_sym:
-  "c1 \<sim> c2 \<Longrightarrow> c2 \<sim> c1"
-by (auto simp add: equiv_c_def) 
-
-lemma equiv_trans:
-  "c1 \<sim> c2 \<Longrightarrow> c2 \<sim> c3 \<Longrightarrow> c1 \<sim> c3"
-by (auto simp add: equiv_c_def) 
-
-text {*
-    Program constructions preserve equivalence.
-*}
-
-lemma equiv_semi:
-  "c1 \<sim> c1' \<Longrightarrow> c2 \<sim> c2' \<Longrightarrow> (c1; c2) \<sim> (c1'; c2')"
-by (force simp add: equiv_c_def) 
-
-lemma equiv_if:
-  "c1 \<sim> c1' \<Longrightarrow> c2 \<sim> c2' \<Longrightarrow> (\<IF> b \<THEN> c1 \<ELSE> c2) \<sim> (\<IF> b \<THEN> c1' \<ELSE> c2')"
-by (force simp add: equiv_c_def) 
-
-lemma while_never: "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> c \<noteq> \<WHILE> (\<lambda>s. True) \<DO> c1"
-apply (induct rule: evalc.induct)
-apply auto
-done
-
-lemma equiv_while_True:
-  "(\<WHILE> (\<lambda>s. True) \<DO> c1) \<sim> (\<WHILE> (\<lambda>s. True) \<DO> c2)" 
-by (blast dest: while_never) 
-
-
-subsection "Execution is deterministic"
-
-text {*
-This proof is automatic.
-*}
-theorem "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = t"
-by (induct arbitrary: u rule: evalc.induct) blast+
-
-
-text {*
-The following proof presents all the details:
-*}
-theorem com_det:
-  assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t" and "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u"
-  shows "u = t"
-  using assms
-proof (induct arbitrary: u set: evalc)
-  fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u"
-  thus "u = s" by blast
-next
-  fix a s x u assume "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c u"
-  thus "u = s[x \<mapsto> a s]" by blast
-next
-  fix c0 c1 s s1 s2 u
-  assume IH0: "\<And>u. \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2"
-  assume IH1: "\<And>u. \<langle>c1,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
-
-  assume "\<langle>c0;c1, s\<rangle> \<longrightarrow>\<^sub>c u"
-  then obtain s' where
-      c0: "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'" and
-      c1: "\<langle>c1,s'\<rangle> \<longrightarrow>\<^sub>c u"
-    by auto
-
-  from c0 IH0 have "s'=s2" by blast
-  with c1 IH1 show "u=s1" by blast
-next
-  fix b c0 c1 s s1 u
-  assume IH: "\<And>u. \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
-
-  assume "b s" and "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>c u"
-  hence "\<langle>c0, s\<rangle> \<longrightarrow>\<^sub>c u" by blast
-  with IH show "u = s1" by blast
-next
-  fix b c0 c1 s s1 u
-  assume IH: "\<And>u. \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
-
-  assume "\<not>b s" and "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>c u"
-  hence "\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>c u" by blast
-  with IH show "u = s1" by blast
-next
-  fix b c s u
-  assume "\<not>b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u"
-  thus "u = s" by blast
-next
-  fix b c s s1 s2 u
-  assume "IH\<^sub>c": "\<And>u. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2"
-  assume "IH\<^sub>w": "\<And>u. \<langle>\<WHILE> b \<DO> c,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
-
-  assume "b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u"
-  then obtain s' where
-      c: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" and
-      w: "\<langle>\<WHILE> b \<DO> c,s'\<rangle> \<longrightarrow>\<^sub>c u"
-    by auto
-
-  from c "IH\<^sub>c" have "s' = s2" by blast
-  with w "IH\<^sub>w" show "u = s1" by blast
-qed
-
-
-text {*
-  This is the proof as you might present it in a lecture. The remaining
-  cases are simple enough to be proved automatically:
-*}
-theorem
-  assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t" and "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u"
-  shows "u = t"
-  using assms
-proof (induct arbitrary: u)
-  -- "the simple @{text \<SKIP>} case for demonstration:"
-  fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u"
-  thus "u = s" by blast
-next
-  -- "and the only really interesting case, @{text \<WHILE>}:"
-  fix b c s s1 s2 u
-  assume "IH\<^sub>c": "\<And>u. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2"
-  assume "IH\<^sub>w": "\<And>u. \<langle>\<WHILE> b \<DO> c,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
-
-  assume "b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u"
-  then obtain s' where
-      c: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" and
-      w: "\<langle>\<WHILE> b \<DO> c,s'\<rangle> \<longrightarrow>\<^sub>c u"
-    by auto
-
-  from c "IH\<^sub>c" have "s' = s2" by blast
-  with w "IH\<^sub>w" show "u = s1" by blast
-qed blast+ -- "prove the rest automatically"
-
-end
diff -r 9ed5d8ad8fa0 -r faba4800b00b src/HOL/IMP/ROOT.ML
--- a/src/HOL/IMP/ROOT.ML	Wed Jun 01 19:50:59 2011 +0200
+++ b/src/HOL/IMP/ROOT.ML	Wed Jun 01 23:08:04 2011 +0200
@@ -1,7 +1,24 @@
-(*  Title:     HOL/IMP/ROOT.ML
-    Author:    Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow, David von Oheimb
-
-Caveat: HOLCF/IMP depends on HOL/IMP
+use_thys
+["BExp",
+ "ASM",
+ "Small_Step",
+ "Denotation",
+ "Compiler"(*,
+ "Poly_Types",
+ "Sec_Typing",
+ "Sec_TypingT",
+ "Def_Ass_Sound_Big",
+ "Def_Ass_Sound_Small",
+ "Def_Ass2_Sound_Small",
+ "Def_Ass2_Big0",
+ "Live",
+ "Hoare_Examples",
+ "VC",
+ "HoareT",
+ "Procs_Dyn_Vars_Dyn",
+ "Procs_Stat_Vars_Dyn",
+ "Procs_Stat_Vars_Stat",
+ "C_like",
+ "OO"
 *)
-
-use_thys ["Expr", "Transition", "VC", "Hoare_Den", "Examples", "Compiler0", "Compiler", "Live"];
+];
diff -r 9ed5d8ad8fa0 -r faba4800b00b src/HOL/IMP/Small_Step.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Small_Step.thy	Wed Jun 01 23:08:04 2011 +0200
@@ -0,0 +1,210 @@
+header "Small-Step Semantics of Commands"
+
+theory Small_Step imports Star Big_Step begin
+
+subsection "The transition relation"
+
+inductive
+  small_step :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>" 55)
+where
+Assign:  "(x ::= a, s) \<rightarrow> (SKIP, s(x := aval a s))" |
+
+Semi1:   "(SKIP;c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)" |
+Semi2:   "(c\<^isub>1,s) \<rightarrow> (c\<^isub>1',s') \<Longrightarrow> (c\<^isub>1;c\<^isub>2,s) \<rightarrow> (c\<^isub>1';c\<^isub>2,s')" |
+
+IfTrue:  "bval b s \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>1,s)" |
+IfFalse: "\<not>bval b s \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)" |
+
+While:   "(WHILE b DO c,s) \<rightarrow> (IF b THEN c; WHILE b DO c ELSE SKIP,s)"
+
+
+abbreviation small_steps :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>*" 55)
+where "x \<rightarrow>* y == star small_step x y"
+
+subsection{* Executability *}
+
+code_pred small_step .
+
+values "{(c',map t [''x'',''y'',''z'']) |c' t.
+   (''x'' ::= V ''z''; ''y'' ::= V ''x'',
+    lookup[(''x'',3),(''y'',7),(''z'',5)]) \<rightarrow>* (c',t)}"
+
+
+subsection{* Proof infrastructure *}
+
+subsubsection{* Induction rules *}
+
+text{* The default induction rule @{thm[source] small_step.induct} only works
+for lemmas of the form @{text"a \<rightarrow> b \<Longrightarrow> \<dots>"} where @{text a} and @{text b} are
+not already pairs @{text"(DUMMY,DUMMY)"}. We can generate a suitable variant
+of @{thm[source] small_step.induct} for pairs by ``splitting'' the arguments
+@{text"\<rightarrow>"} into pairs: *}
+lemmas small_step_induct = small_step.induct[split_format(complete)]
+
+
+subsubsection{* Proof automation *}
+
+declare small_step.intros[simp,intro]
+
+text{* So called transitivity rules. See below. *}
+
+declare step[trans] step1[trans]
+
+lemma step2[trans]:
+  "cs \<rightarrow> cs' \<Longrightarrow> cs' \<rightarrow> cs'' \<Longrightarrow> cs \<rightarrow>* cs''"
+by(metis refl step)
+
+declare star_trans[trans]
+
+text{* Rule inversion: *}
+
+inductive_cases SkipE[elim!]: "(SKIP,s) \<rightarrow> ct"
+thm SkipE
+inductive_cases AssignE[elim!]: "(x::=a,s) \<rightarrow> ct"
+thm AssignE
+inductive_cases SemiE[elim]: "(c1;c2,s) \<rightarrow> ct"
+thm SemiE
+inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) \<rightarrow> ct"
+inductive_cases WhileE[elim]: "(WHILE b DO c, s) \<rightarrow> ct"
+
+
+text{* A simple property: *}
+lemma deterministic:
+  "cs \<rightarrow> cs' \<Longrightarrow> cs \<rightarrow> cs'' \<Longrightarrow> cs'' = cs'"
+apply(induct arbitrary: cs'' rule: small_step.induct)
+apply blast+
+done
+
+
+subsection "Equivalence with big-step semantics"
+
+lemma star_semi2: "(c1,s) \<rightarrow>* (c1',s') \<Longrightarrow> (c1;c2,s) \<rightarrow>* (c1';c2,s')"
+proof(induct rule: star_induct)
+  case refl thus ?case by simp
+next
+  case step
+  thus ?case by (metis Semi2 star.step)
+qed
+
+lemma semi_comp:
+  "\<lbrakk> (c1,s1) \<rightarrow>* (SKIP,s2); (c2,s2) \<rightarrow>* (SKIP,s3) \<rbrakk>
+   \<Longrightarrow> (c1;c2, s1) \<rightarrow>* (SKIP,s3)"
+by(blast intro: star.step star_semi2 star_trans)
+
+text{* The following proof corresponds to one on the board where one would
+show chains of @{text "\<rightarrow>"} and @{text "\<rightarrow>*"} steps. This is what the
+also/finally proof steps do: they compose chains, implicitly using the rules
+declared with attribute [trans] above. *}
+
+lemma big_to_small:
+  "cs \<Rightarrow> t \<Longrightarrow> cs \<rightarrow>* (SKIP,t)"
+proof (induct rule: big_step.induct)
+  fix s show "(SKIP,s) \<rightarrow>* (SKIP,s)" by simp
+next
+  fix x a s show "(x ::= a,s) \<rightarrow>* (SKIP, s(x := aval a s))" by auto
+next
+  fix c1 c2 s1 s2 s3
+  assume "(c1,s1) \<rightarrow>* (SKIP,s2)" and "(c2,s2) \<rightarrow>* (SKIP,s3)"
+  thus "(c1;c2, s1) \<rightarrow>* (SKIP,s3)" by (rule semi_comp)
+next
+  fix s::state and b c0 c1 t
+  assume "bval b s"
+  hence "(IF b THEN c0 ELSE c1,s) \<rightarrow> (c0,s)" by simp
+  also assume "(c0,s) \<rightarrow>* (SKIP,t)"
+  finally show "(IF b THEN c0 ELSE c1,s) \<rightarrow>* (SKIP,t)" . --"= by assumption"
+next
+  fix s::state and b c0 c1 t
+  assume "\<not>bval b s"
+  hence "(IF b THEN c0 ELSE c1,s) \<rightarrow> (c1,s)" by simp
+  also assume "(c1,s) \<rightarrow>* (SKIP,t)"
+  finally show "(IF b THEN c0 ELSE c1,s) \<rightarrow>* (SKIP,t)" .
+next
+  fix b c and s::state
+  assume b: "\<not>bval b s"
+  let ?if = "IF b THEN c; WHILE b DO c ELSE SKIP"
+  have "(WHILE b DO c,s) \<rightarrow> (?if, s)" by blast
+  also have "(?if,s) \<rightarrow> (SKIP, s)" by (simp add: b)
+  finally show "(WHILE b DO c,s) \<rightarrow>* (SKIP,s)" by auto
+next
+  fix b c s s' t
+  let ?w  = "WHILE b DO c"
+  let ?if = "IF b THEN c; ?w ELSE SKIP"
+  assume w: "(?w,s') \<rightarrow>* (SKIP,t)"
+  assume c: "(c,s) \<rightarrow>* (SKIP,s')"
+  assume b: "bval b s"
+  have "(?w,s) \<rightarrow> (?if, s)" by blast
+  also have "(?if, s) \<rightarrow> (c; ?w, s)" by (simp add: b)
+  also have "(c; ?w,s) \<rightarrow>* (SKIP,t)" by(rule semi_comp[OF c w])
+  finally show "(WHILE b DO c,s) \<rightarrow>* (SKIP,t)" by auto
+qed
+
+text{* Each case of the induction can be proved automatically: *}
+lemma  "cs \<Rightarrow> t \<Longrightarrow> cs \<rightarrow>* (SKIP,t)"
+proof (induct rule: big_step.induct)
+  case Skip show ?case by blast
+next
+  case Assign show ?case by blast
+next
+  case Semi thus ?case by (blast intro: semi_comp)
+next
+  case IfTrue thus ?case by (blast intro: step)
+next
+  case IfFalse thus ?case by (blast intro: step)
+next
+  case WhileFalse thus ?case
+    by (metis step step1 small_step.IfFalse small_step.While)
+next
+  case WhileTrue
+  thus ?case
+    by(metis While semi_comp small_step.IfTrue step[of small_step])
+qed
+
+lemma small1_big_continue:
+  "cs \<rightarrow> cs' \<Longrightarrow> cs' \<Rightarrow> t \<Longrightarrow> cs \<Rightarrow> t"
+apply (induct arbitrary: t rule: small_step.induct)
+apply auto
+done
+
+lemma small_big_continue:
+  "cs \<rightarrow>* cs' \<Longrightarrow> cs' \<Rightarrow> t \<Longrightarrow> cs \<Rightarrow> t"
+apply (induct rule: star.induct)
+apply (auto intro: small1_big_continue)
+done
+
+lemma small_to_big: "cs \<rightarrow>* (SKIP,t) \<Longrightarrow> cs \<Rightarrow> t"
+by (metis small_big_continue Skip)
+
+text {*
+  Finally, the equivalence theorem:
+*}
+theorem big_iff_small:
+  "cs \<Rightarrow> t = cs \<rightarrow>* (SKIP,t)"
+by(metis big_to_small small_to_big)
+
+
+subsection "Final configurations and infinite reductions"
+
+definition "final cs \<longleftrightarrow> \<not>(EX cs'. cs \<rightarrow> cs')"
+
+lemma finalD: "final (c,s) \<Longrightarrow> c = SKIP"
+apply(simp add: final_def)
+apply(induct c)
+apply blast+
+done
+
+lemma final_iff_SKIP: "final (c,s) = (c = SKIP)"
+by (metis SkipE finalD final_def)
+
+text{* Now we can show that @{text"\<Rightarrow>"} yields a final state iff @{text"\<rightarrow>"}
+terminates: *}
+
+lemma big_iff_small_termination:
+  "(EX t. cs \<Rightarrow> t) \<longleftrightarrow> (EX cs'. cs \<rightarrow>* cs' \<and> final cs')"
+by(simp add: big_iff_small final_iff_SKIP)
+
+text{* This is the same as saying that the absence of a big step result is
+equivalent with absence of a terminating small step sequence, i.e.\ with
+nontermination.  Since @{text"\<rightarrow>"} is determininistic, there is no difference
+between may and must terminate. *}
+
+end
diff -r 9ed5d8ad8fa0 -r faba4800b00b src/HOL/IMP/Star.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Star.thy	Wed Jun 01 23:08:04 2011 +0200
@@ -0,0 +1,27 @@
+theory Star imports Main
+begin
+
+inductive
+  star :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+for r where
+refl:  "star r x x" |
+step:  "r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
+
+lemma star_trans:
+  "star r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
+proof(induct rule: star.induct)
+  case refl thus ?case .
+next
+  case step thus ?case by (metis star.step)
+qed
+
+lemmas star_induct = star.induct[of "r:: 'a*'b \<Rightarrow> 'a*'b \<Rightarrow> bool", split_format(complete)]
+
+declare star.refl[simp,intro]
+
+lemma step1[simp, intro]: "r x y \<Longrightarrow> star r x y"
+by(metis refl step)
+
+code_pred star .
+
+end
diff -r 9ed5d8ad8fa0 -r faba4800b00b src/HOL/IMP/Transition.thy
--- a/src/HOL/IMP/Transition.thy	Wed Jun 01 19:50:59 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,644 +0,0 @@
-(*  Title:        HOL/IMP/Transition.thy
-    Author:       Tobias Nipkow & Robert Sandner, TUM
-    Isar Version: Gerwin Klein, 2001
-    Copyright     1996 TUM
-*)
-
-header "Transition Semantics of Commands"
-
-theory Transition imports Natural begin
-
-subsection "The transition relation"
-
-text {*
-  We formalize the transition semantics as in \cite{Nielson}. This
-  makes some of the rules a bit more intuitive, but also requires
-  some more (internal) formal overhead.
-
-  Since configurations that have terminated are written without
-  a statement, the transition relation is not
-  @{typ "((com \<times> state) \<times> (com \<times> state)) set"}
-  but instead:
-  @{typ "((com option \<times> state) \<times> (com option \<times> state)) set"}
-
-  Some syntactic sugar that we will use to hide the
-  @{text option} part in configurations:
-*}
-abbreviation
-  angle :: "[com, state] \<Rightarrow> com option \<times> state" ("<_,_>") where
-  "<c,s> == (Some c, s)"
-abbreviation
-  angle2 :: "state \<Rightarrow> com option \<times> state"  ("<_>") where
-  "<s> == (None, s)"
-
-notation (xsymbols)
-  angle  ("\<langle>_,_\<rangle>") and
-  angle2  ("\<langle>_\<rangle>")
-
-notation (HTML output)
-  angle  ("\<langle>_,_\<rangle>") and
-  angle2  ("\<langle>_\<rangle>")
-
-text {*
-  Now, finally, we are set to write down the rules for our small step semantics:
-*}
-inductive_set
-  evalc1 :: "((com option \<times> state) \<times> (com option \<times> state)) set"
-  and evalc1' :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
-    ("_ \<longrightarrow>\<^sub>1 _" [60,60] 61)
-where
-  "cs \<longrightarrow>\<^sub>1 cs' == (cs,cs') \<in> evalc1"
-| Skip:    "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s\<rangle>"
-| Assign:  "\<langle>x :== a, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s[x \<mapsto> a s]\<rangle>"
-
-| Semi1:   "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> \<langle>c0;c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1,s'\<rangle>"
-| Semi2:   "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c0',s'\<rangle> \<Longrightarrow> \<langle>c0;c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c0';c1,s'\<rangle>"
-
-| IfTrue:  "b s \<Longrightarrow> \<langle>\<IF> b \<THEN> c1 \<ELSE> c2,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1,s\<rangle>"
-| IfFalse: "\<not>b s \<Longrightarrow> \<langle>\<IF> b \<THEN> c1 \<ELSE> c2,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c2,s\<rangle>"
-
-| While:   "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>,s\<rangle>"
-
-lemmas [intro] = evalc1.intros -- "again, use these rules in automatic proofs"
-
-text {*
-  More syntactic sugar for the transition relation, and its
-  iteration.
-*}
-abbreviation
-  evalcn :: "[(com option\<times>state),nat,(com option\<times>state)] \<Rightarrow> bool"
-    ("_ -_\<rightarrow>\<^sub>1 _" [60,60,60] 60)  where
-  "cs -n\<rightarrow>\<^sub>1 cs' == (cs,cs') \<in> evalc1^^n"
-
-abbreviation
-  evalc' :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
-    ("_ \<longrightarrow>\<^sub>1\<^sup>* _" [60,60] 60)  where
-  "cs \<longrightarrow>\<^sub>1\<^sup>* cs' == (cs,cs') \<in> evalc1^*"
-
-(*<*)
-declare rel_pow_Suc_E2 [elim!]
-(*>*)
-
-text {*
-  As for the big step semantics you can read these rules in a
-  syntax directed way:
-*}
-lemma SKIP_1: "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 y = (y = \<langle>s\<rangle>)"
-  by (induct y, rule, cases set: evalc1, auto)
-
-lemma Assign_1: "\<langle>x :== a, s\<rangle> \<longrightarrow>\<^sub>1 y = (y = \<langle>s[x \<mapsto> a s]\<rangle>)"
-  by (induct y, rule, cases set: evalc1, auto)
-
-lemma Cond_1:
-  "\<langle>\<IF> b \<THEN> c1 \<ELSE> c2, s\<rangle> \<longrightarrow>\<^sub>1 y = ((b s \<longrightarrow> y = \<langle>c1, s\<rangle>) \<and> (\<not>b s \<longrightarrow> y = \<langle>c2, s\<rangle>))"
-  by (induct y, rule, cases set: evalc1, auto)
-
-lemma While_1:
-  "\<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>1 y = (y = \<langle>\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>, s\<rangle>)"
-  by (induct y, rule, cases set: evalc1, auto)
-
-lemmas [simp] = SKIP_1 Assign_1 Cond_1 While_1
-
-
-subsection "Examples"
-
-lemma
-  "s x = 0 \<Longrightarrow> \<langle>\<WHILE> \<lambda>s. s x \<noteq> 1 \<DO> (x:== \<lambda>s. s x+1), s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s[x \<mapsto> 1]\<rangle>"
-  (is "_ \<Longrightarrow> \<langle>?w, _\<rangle> \<longrightarrow>\<^sub>1\<^sup>* _")
-proof -
-  let ?c  = "x:== \<lambda>s. s x+1"
-  let ?if = "\<IF> \<lambda>s. s x \<noteq> 1 \<THEN> ?c; ?w \<ELSE> \<SKIP>"
-  assume [simp]: "s x = 0"
-  have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1  \<langle>?if, s\<rangle>" ..
-  also have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?c; ?w, s\<rangle>" by simp
-  also have "\<langle>?c; ?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 1]\<rangle>" by (rule Semi1) simp
-  also have "\<langle>?w, s[x \<mapsto> 1]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s[x \<mapsto> 1]\<rangle>" ..
-  also have "\<langle>?if, s[x \<mapsto> 1]\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<SKIP>, s[x \<mapsto> 1]\<rangle>" by (simp add: update_def)
-  also have "\<langle>\<SKIP>, s[x \<mapsto> 1]\<rangle> \<longrightarrow>\<^sub>1 \<langle>s[x \<mapsto> 1]\<rangle>" ..
-  finally show ?thesis ..
-qed
-
-lemma
-  "s x = 2 \<Longrightarrow> \<langle>\<WHILE> \<lambda>s. s x \<noteq> 1 \<DO> (x:== \<lambda>s. s x+1), s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* s'"
-  (is "_ \<Longrightarrow> \<langle>?w, _\<rangle> \<longrightarrow>\<^sub>1\<^sup>* s'")
-proof -
-  let ?c = "x:== \<lambda>s. s x+1"
-  let ?if = "\<IF> \<lambda>s. s x \<noteq> 1 \<THEN> ?c; ?w \<ELSE> \<SKIP>"
-  assume [simp]: "s x = 2"
-  note update_def [simp]
-  have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1  \<langle>?if, s\<rangle>" ..
-  also have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?c; ?w, s\<rangle>" by simp
-  also have "\<langle>?c; ?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 3]\<rangle>" by (rule Semi1) simp
-  also have "\<langle>?w, s[x \<mapsto> 3]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s[x \<mapsto> 3]\<rangle>" ..
-  also have "\<langle>?if, s[x \<mapsto> 3]\<rangle> \<longrightarrow>\<^sub>1  \<langle>?c; ?w, s[x \<mapsto> 3]\<rangle>" by simp
-  also have "\<langle>?c; ?w, s[x \<mapsto> 3]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 4]\<rangle>" by (rule Semi1) simp
-  also have "\<langle>?w, s[x \<mapsto> 4]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s[x \<mapsto> 4]\<rangle>" ..
-  also have "\<langle>?if, s[x \<mapsto> 4]\<rangle> \<longrightarrow>\<^sub>1  \<langle>?c; ?w, s[x \<mapsto> 4]\<rangle>" by simp
-  also have "\<langle>?c; ?w, s[x \<mapsto> 4]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 5]\<rangle>" by (rule Semi1) simp
-  oops
-
-subsection "Basic properties"
-
-text {*
-  There are no \emph{stuck} programs:
-*}
-lemma no_stuck: "\<exists>y. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1 y"
-proof (induct c)
-  -- "case Semi:"
-  fix c1 c2 assume "\<exists>y. \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 y"
-  then obtain y where "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 y" ..
-  then obtain c1' s' where "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'\<rangle> \<or> \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1',s'\<rangle>"
-    by (cases y, cases "fst y") auto
-  thus "\<exists>s'. \<langle>c1;c2,s\<rangle> \<longrightarrow>\<^sub>1 s'" by auto
-next
-  -- "case If:"
-  fix b c1 c2 assume "\<exists>y. \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 y" and "\<exists>y. \<langle>c2,s\<rangle> \<longrightarrow>\<^sub>1 y"
-  thus "\<exists>y. \<langle>\<IF> b \<THEN> c1 \<ELSE> c2, s\<rangle> \<longrightarrow>\<^sub>1 y" by (cases "b s") auto
-qed auto -- "the rest is trivial"
-
-text {*
-  If a configuration does not contain a statement, the program
-  has terminated and there is no next configuration:
-*}
-lemma stuck [elim!]: "\<langle>s\<rangle> \<longrightarrow>\<^sub>1 y \<Longrightarrow> P"
-  by (induct y, auto elim: evalc1.cases)
-
-lemma evalc_None_retrancl [simp, dest!]: "\<langle>s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* s' \<Longrightarrow> s' = \<langle>s\<rangle>"
-  by (induct set: rtrancl) auto
-
-(*<*)
-(* FIXME: relpow.simps don't work *)
-lemmas [simp del] = relpow.simps
-lemma rel_pow_0 [simp]: "!!R::('a*'a) set. R ^^ 0 = Id" by (simp add: relpow.simps)
-lemma rel_pow_Suc_0 [simp]: "!!R::('a*'a) set. R ^^ Suc 0 = R" by (simp add: relpow.simps)
-
-(*>*)
-lemma evalc1_None_0 [simp]: "\<langle>s\<rangle> -n\<rightarrow>\<^sub>1 y = (n = 0 \<and> y = \<langle>s\<rangle>)"
-  by (cases n) auto
-
-lemma SKIP_n: "\<langle>\<SKIP>, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> s' = s \<and> n=1"
-  by (cases n) auto
-
-subsection "Equivalence to natural semantics (after Nielson and Nielson)"
-
-text {*
-  We first need two lemmas about semicolon statements:
-  decomposition and composition.
-*}
-lemma semiD:
-  "\<langle>c1; c2, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<Longrightarrow>
-  \<exists>i j s'. \<langle>c1, s\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<and> \<langle>c2, s'\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<and> n = i+j"
-proof (induct n arbitrary: c1 c2 s s'')
-  case 0
-  then show ?case by simp
-next
-  case (Suc n)
-
-  from `\<langle>c1; c2, s\<rangle> -Suc n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>`
-  obtain co s''' where
-      1: "\<langle>c1; c2, s\<rangle> \<longrightarrow>\<^sub>1 (co, s''')" and
-      n: "(co, s''') -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>"
-    by auto
-
-  from 1
-  show "\<exists>i j s'. \<langle>c1, s\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<and> \<langle>c2, s'\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<and> Suc n = i+j"
-    (is "\<exists>i j s'. ?Q i j s'")
-  proof (cases set: evalc1)
-    case Semi1
-    from `co = Some c2` and `\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'''\<rangle>` and 1 n
-    have "?Q 1 n s'''" by simp
-    thus ?thesis by blast
-  next
-    case (Semi2 c1')
-    note c1 = `\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1', s'''\<rangle>`
-    with `co = Some (c1'; c2)` and n
-    have "\<langle>c1'; c2, s'''\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by simp
-    with Suc.hyps obtain i j s0 where
-        c1': "\<langle>c1',s'''\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s0\<rangle>" and
-        c2:  "\<langle>c2,s0\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" and
-        i:   "n = i+j"
-      by fast
-
-    from c1 c1'
-    have "\<langle>c1,s\<rangle> -(i+1)\<rightarrow>\<^sub>1 \<langle>s0\<rangle>" by (auto intro: rel_pow_Suc_I2)
-    with c2 i
-    have "?Q (i+1) j s0" by simp
-    thus ?thesis by blast
-  qed
-qed
-
-
-lemma semiI:
-  "\<langle>c0,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<Longrightarrow> \<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle> \<Longrightarrow> \<langle>c0; c1, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
-proof (induct n arbitrary: c0 s s'')
-  case 0
-  from `\<langle>c0,s\<rangle> -(0::nat)\<rightarrow>\<^sub>1 \<langle>s''\<rangle>`
-  have False by simp
-  thus ?case ..
-next
-  case (Suc n)
-  note c0 = `\<langle>c0,s\<rangle> -Suc n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>`
-  note c1 = `\<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>`
-  note IH = `\<And>c0 s s''.
-    \<langle>c0,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<Longrightarrow> \<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle> \<Longrightarrow> \<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>`
-  from c0 obtain y where
-    1: "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1 y" and n: "y -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by blast
-  from 1 obtain c0' s0' where
-      "y = \<langle>s0'\<rangle> \<or> y = \<langle>c0', s0'\<rangle>"
-    by (cases y, cases "fst y") auto
-  moreover
-  { assume y: "y = \<langle>s0'\<rangle>"
-    with n have "s'' = s0'" by simp
-    with y 1 have "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1, s''\<rangle>" by blast
-    with c1 have "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (blast intro: rtrancl_trans)
-  }
-  moreover
-  { assume y: "y = \<langle>c0', s0'\<rangle>"
-    with n have "\<langle>c0', s0'\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by blast
-    with IH c1 have "\<langle>c0'; c1,s0'\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by blast
-    moreover
-    from y 1 have "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c0'; c1,s0'\<rangle>" by blast
-    hence "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c0'; c1,s0'\<rangle>" by blast
-    ultimately
-    have "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (blast intro: rtrancl_trans)
-  }
-  ultimately
-  show "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by blast
-qed
-
-text {*
-  The easy direction of the equivalence proof:
-*}
-lemma evalc_imp_evalc1:
-  assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
-  shows "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
-  using assms
-proof induct
-  fix s show "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" by auto
-next
-  fix x a s show "\<langle>x :== a ,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s[x\<mapsto>a s]\<rangle>" by auto
-next
-  fix c0 c1 s s'' s'
-  assume "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s''\<rangle>"
-  then obtain n where "\<langle>c0,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by (blast dest: rtrancl_imp_rel_pow)
-  moreover
-  assume "\<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
-  ultimately
-  show "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (rule semiI)
-next
-  fix s::state and b c0 c1 s'
-  assume "b s"
-  hence "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c0,s\<rangle>" by simp
-  also assume "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
-  finally show "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" .
-next
-  fix s::state and b c0 c1 s'
-  assume "\<not>b s"
-  hence "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1,s\<rangle>" by simp
-  also assume "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
-  finally show "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" .
-next
-  fix b c and s::state
-  assume b: "\<not>b s"
-  let ?if = "\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>"
-  have "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s\<rangle>" by blast
-  also have "\<langle>?if,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<SKIP>, s\<rangle>" by (simp add: b)
-  also have "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s\<rangle>" by blast
-  finally show "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" ..
-next
-  fix b c s s'' s'
-  let ?w  = "\<WHILE> b \<DO> c"
-  let ?if = "\<IF> b \<THEN> c; ?w \<ELSE> \<SKIP>"
-  assume w: "\<langle>?w,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
-  assume c: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s''\<rangle>"
-  assume b: "b s"
-  have "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s\<rangle>" by blast
-  also have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c; ?w, s\<rangle>" by (simp add: b)
-  also
-  from c obtain n where "\<langle>c,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by (blast dest: rtrancl_imp_rel_pow)
-  with w have "\<langle>c; ?w,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by - (rule semiI)
-  finally show "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" ..
-qed
-
-text {*
-  Finally, the equivalence theorem:
-*}
-theorem evalc_equiv_evalc1:
-  "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
-proof
-  assume "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
-  then show "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (rule evalc_imp_evalc1)
-next
-  assume "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
-  then obtain n where "\<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by (blast dest: rtrancl_imp_rel_pow)
-  moreover
-  have "\<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
-  proof (induct arbitrary: c s s' rule: less_induct)
-    fix n
-    assume IH: "\<And>m c s s'. m < n \<Longrightarrow> \<langle>c,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
-    fix c s s'
-    assume c:  "\<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle>"
-    then obtain m where n: "n = Suc m" by (cases n) auto
-    with c obtain y where
-      c': "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1 y" and m: "y -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by blast
-    show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
-    proof (cases c)
-      case SKIP
-      with c n show ?thesis by auto
-    next
-      case Assign
-      with c n show ?thesis by auto
-    next
-      fix c1 c2 assume semi: "c = (c1; c2)"
-      with c obtain i j s'' where
-          c1: "\<langle>c1, s\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" and
-          c2: "\<langle>c2, s''\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" and
-          ij: "n = i+j"
-        by (blast dest: semiD)
-      from c1 c2 obtain
-        "0 < i" and "0 < j" by (cases i, auto, cases j, auto)
-      with ij obtain
-        i: "i < n" and j: "j < n" by simp
-      from IH i c1
-      have "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s''" .
-      moreover
-      from IH j c2
-      have "\<langle>c2,s''\<rangle> \<longrightarrow>\<^sub>c s'" .
-      moreover
-      note semi
-      ultimately
-      show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
-    next
-      fix b c1 c2 assume If: "c = \<IF> b \<THEN> c1 \<ELSE> c2"
-      { assume True: "b s = True"
-        with If c n
-        have "\<langle>c1,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by auto
-        with n IH
-        have "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
-        with If True
-        have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
-      }
-      moreover
-      { assume False: "b s = False"
-        with If c n
-        have "\<langle>c2,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by auto
-        with n IH
-        have "\<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
-        with If False
-        have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
-      }
-      ultimately
-      show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by (cases "b s") auto
-    next
-      fix b c' assume w: "c = \<WHILE> b \<DO> c'"
-      with c n
-      have "\<langle>\<IF> b \<THEN> c'; \<WHILE> b \<DO> c' \<ELSE> \<SKIP>,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>"
-        (is "\<langle>?if,_\<rangle> -m\<rightarrow>\<^sub>1 _") by auto
-      with n IH
-      have "\<langle>\<IF> b \<THEN> c'; \<WHILE> b \<DO> c' \<ELSE> \<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
-      moreover note unfold_while [of b c']
-      -- {* @{thm unfold_while [of b c']} *}
-      ultimately
-      have "\<langle>\<WHILE> b \<DO> c',s\<rangle> \<longrightarrow>\<^sub>c s'" by (blast dest: equivD2)
-      with w show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by simp
-    qed
-  qed
-  ultimately
-  show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
-qed
-
-
-subsection "Winskel's Proof"
-
-declare rel_pow_0_E [elim!]
-
-text {*
-  Winskel's small step rules are a bit different \cite{Winskel};
-  we introduce their equivalents as derived rules:
-*}
-lemma whileFalse1 [intro]:
-  "\<not> b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" (is "_ \<Longrightarrow> \<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>")
-proof -
-  assume "\<not>b s"
-  have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle>" ..
-  also from `\<not>b s` have "\<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<SKIP>, s\<rangle>" ..
-  also have "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s\<rangle>" ..
-  finally show "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" ..
-qed
-
-lemma whileTrue1 [intro]:
-  "b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;\<WHILE> b \<DO> c, s\<rangle>"
-  (is "_ \<Longrightarrow> \<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;?w,s\<rangle>")
-proof -
-  assume "b s"
-  have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle>" ..
-  also from `b s` have "\<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c;?w, s\<rangle>" ..
-  finally show "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;?w,s\<rangle>" ..
-qed
-
-inductive_cases evalc1_SEs:
-  "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>1 (co, s')"
-  "\<langle>x:==a,s\<rangle> \<longrightarrow>\<^sub>1 (co, s')"
-  "\<langle>c1;c2, s\<rangle> \<longrightarrow>\<^sub>1 (co, s')"
-  "\<langle>\<IF> b \<THEN> c1 \<ELSE> c2, s\<rangle> \<longrightarrow>\<^sub>1 (co, s')"
-  "\<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>1 (co, s')"
-
-inductive_cases evalc1_E: "\<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>1 (co, s')"
-
-declare evalc1_SEs [elim!]
-
-lemma evalc_impl_evalc1: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s1 \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s1\<rangle>"
-apply (induct set: evalc)
-
--- SKIP
-apply blast
-
--- ASSIGN
-apply fast
-
--- SEMI
-apply (fast dest: rtrancl_imp_UN_rel_pow intro: semiI)
-
--- IF
-apply (fast intro: converse_rtrancl_into_rtrancl)
-apply (fast intro: converse_rtrancl_into_rtrancl)
-
--- WHILE
-apply blast
-apply (blast dest: rtrancl_imp_UN_rel_pow intro: converse_rtrancl_into_rtrancl semiI)
-
-done
-
-
-lemma lemma2:
-  "\<langle>c;d,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>u\<rangle> \<Longrightarrow> \<exists>t m. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<and> \<langle>d,t\<rangle> -m\<rightarrow>\<^sub>1 \<langle>u\<rangle> \<and> m \<le> n"
-apply (induct n arbitrary: c d s u)
- -- "case n = 0"
- apply fastsimp
--- "induction step"
-apply (fast intro!: le_SucI le_refl dest!: rel_pow_Suc_D2
-            elim!: rel_pow_imp_rtrancl converse_rtrancl_into_rtrancl)
-done
-
-lemma evalc1_impl_evalc:
-  "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
-apply (induct c arbitrary: s t)
-apply (safe dest!: rtrancl_imp_UN_rel_pow)
-
--- SKIP
-apply (simp add: SKIP_n)
-
--- ASSIGN
-apply (fastsimp elim: rel_pow_E2)
-
--- SEMI
-apply (fast dest!: rel_pow_imp_rtrancl lemma2)
-
--- IF
-apply (erule rel_pow_E2)
-apply simp
-apply (fast dest!: rel_pow_imp_rtrancl)
-
--- "WHILE, induction on the length of the computation"
-apply (rename_tac b c s t n)
-apply (erule_tac P = "?X -n\<rightarrow>\<^sub>1 ?Y" in rev_mp)
-apply (rule_tac x = "s" in spec)
-apply (induct_tac n rule: nat_less_induct)
-apply (intro strip)
-apply (erule rel_pow_E2)
- apply simp
-apply (simp only: split_paired_all)
-apply (erule evalc1_E)
-
-apply simp
-apply (case_tac "b x")
- -- WhileTrue
- apply (erule rel_pow_E2)
-  apply simp
- apply (clarify dest!: lemma2)
- apply atomize
- apply (erule allE, erule allE, erule impE, assumption)
- apply (erule_tac x=mb in allE, erule impE, fastsimp)
- apply blast
--- WhileFalse
-apply (erule rel_pow_E2)
- apply simp
-apply (simp add: SKIP_n)
-done
-
-
-text {* proof of the equivalence of evalc and evalc1 *}
-lemma evalc1_eq_evalc: "(\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle>) = (\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t)"
-  by (fast elim!: evalc1_impl_evalc evalc_impl_evalc1)
-
-
-subsection "A proof without n"
-
-text {*
-  The inductions are a bit awkward to write in this section,
-  because @{text None} as result statement in the small step
-  semantics doesn't have a direct counterpart in the big step
-  semantics.
-
-  Winskel's small step rule set (using the @{text "\<SKIP>"} statement
-  to indicate termination) is better suited for this proof.
-*}
-
-lemma my_lemma1:
-  assumes "\<langle>c1,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s2\<rangle>"
-    and "\<langle>c2,s2\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
-  shows "\<langle>c1;c2,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
-proof -
-  -- {* The induction rule needs @{text P} to be a function of @{term "Some c1"} *}
-  from assms
-  have "\<langle>(\<lambda>c. if c = None then c2 else the c; c2) (Some c1),s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
-    apply (induct rule: converse_rtrancl_induct2)
-     apply simp
-    apply (rename_tac c s')
-    apply simp
-    apply (rule conjI)
-     apply fast
-    apply clarify
-    apply (case_tac c)
-    apply (auto intro: converse_rtrancl_into_rtrancl)
-    done
-  then show ?thesis by simp
-qed
-
-lemma evalc_impl_evalc1': "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s1 \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s1\<rangle>"
-apply (induct set: evalc)
-
--- SKIP
-apply fast
-
--- ASSIGN
-apply fast
-
--- SEMI
-apply (fast intro: my_lemma1)
-
--- IF
-apply (fast intro: converse_rtrancl_into_rtrancl)
-apply (fast intro: converse_rtrancl_into_rtrancl)
-
--- WHILE
-apply fast
-apply (fast intro: converse_rtrancl_into_rtrancl my_lemma1)
-
-done
-
-text {*
-  The opposite direction is based on a Coq proof done by Ranan Fraer and
-  Yves Bertot. The following sketch is from an email by Ranan Fraer.
-
-\begin{verbatim}
-First we've broke it into 2 lemmas:
-
-Lemma 1
-((c,s) --> (SKIP,t)) => (<c,s> -c-> t)
-
-This is a quick one, dealing with the cases skip, assignment
-and while_false.
-
-Lemma 2
-((c,s) -*-> (c',s')) /\ <c',s'> -c'-> t
-  =>
-<c,s> -c-> t
-
-This is proved by rule induction on the  -*-> relation
-and the induction step makes use of a third lemma:
-
-Lemma 3
-((c,s) --> (c',s')) /\ <c',s'> -c'-> t
-  =>
-<c,s> -c-> t
-
-This captures the essence of the proof, as it shows that <c',s'>
-behaves as the continuation of <c,s> with respect to the natural
-semantics.
-The proof of Lemma 3 goes by rule induction on the --> relation,
-dealing with the cases sequence1, sequence2, if_true, if_false and
-while_true. In particular in the case (sequence1) we make use again
-of Lemma 1.
-\end{verbatim}
-*}
-
-inductive_cases evalc1_term_cases: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'\<rangle>"
-
-lemma FB_lemma3:
-  "(c,s) \<longrightarrow>\<^sub>1 (c',s') \<Longrightarrow> c \<noteq> None \<Longrightarrow>
-  \<langle>if c'=None then \<SKIP> else the c',s'\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> \<langle>the c,s\<rangle> \<longrightarrow>\<^sub>c t"
-  by (induct arbitrary: t set: evalc1)
-    (auto elim!: evalc1_term_cases equivD2 [OF unfold_while])
-
-lemma FB_lemma2:
-  "(c,s) \<longrightarrow>\<^sub>1\<^sup>* (c',s') \<Longrightarrow> c \<noteq> None \<Longrightarrow>
-   \<langle>if c' = None then \<SKIP> else the c',s'\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> \<langle>the c,s\<rangle> \<longrightarrow>\<^sub>c t"
-  apply (induct rule: converse_rtrancl_induct2, force)
-  apply (fastsimp elim!: evalc1_term_cases intro: FB_lemma3)
-  done
-
-lemma evalc1_impl_evalc': "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
-  by (fastsimp dest: FB_lemma2)
-
-end
diff -r 9ed5d8ad8fa0 -r faba4800b00b src/HOL/IMP/VC.thy
--- a/src/HOL/IMP/VC.thy	Wed Jun 01 19:50:59 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,137 +0,0 @@
-(*  Title:      HOL/IMP/VC.thy
-    Author:     Tobias Nipkow
-
-acom: annotated commands
-vc:   verification-conditions
-awp:   weakest (liberal) precondition
-*)
-
-header "Verification Conditions"
-
-theory VC imports Hoare_Op begin
-
-datatype  acom = Askip
-               | Aass   loc aexp
-               | Asemi  acom acom
-               | Aif    bexp acom acom
-               | Awhile bexp assn acom
-
-primrec awp :: "acom => assn => assn"
-where
-  "awp Askip Q = Q"
-| "awp (Aass x a) Q = (\<lambda>s. Q(s[x\<mapsto>a s]))"
-| "awp (Asemi c d) Q = awp c (awp d Q)"
-| "awp (Aif b c d) Q = (\<lambda>s. (b s-->awp c Q s) & (~b s-->awp d Q s))"
-| "awp (Awhile b I c) Q = I"
-
-primrec vc :: "acom => assn => assn"
-where
-  "vc Askip Q = (\<lambda>s. True)"
-| "vc (Aass x a) Q = (\<lambda>s. True)"
-| "vc (Asemi c d) Q = (\<lambda>s. vc c (awp d Q) s & vc d Q s)"
-| "vc (Aif b c d) Q = (\<lambda>s. vc c Q s & vc d Q s)"
-| "vc (Awhile b I c) Q = (\<lambda>s. (I s & ~b s --> Q s) &
-                              (I s & b s --> awp c I s) & vc c I s)"
-
-primrec astrip :: "acom => com"
-where
-  "astrip Askip = SKIP"
-| "astrip (Aass x a) = (x:==a)"
-| "astrip (Asemi c d) = (astrip c;astrip d)"
-| "astrip (Aif b c d) = (\<IF> b \<THEN> astrip c \<ELSE> astrip d)"
-| "astrip (Awhile b I c) = (\<WHILE> b \<DO> astrip c)"
-
-(* simultaneous computation of vc and awp: *)
-primrec vcawp :: "acom => assn => assn \<times> assn"
-where
-  "vcawp Askip Q = (\<lambda>s. True, Q)"
-| "vcawp (Aass x a) Q = (\<lambda>s. True, \<lambda>s. Q(s[x\<mapsto>a s]))"
-| "vcawp (Asemi c d) Q = (let (vcd,wpd) = vcawp d Q;
-                              (vcc,wpc) = vcawp c wpd
-                          in (\<lambda>s. vcc s & vcd s, wpc))"
-| "vcawp (Aif b c d) Q = (let (vcd,wpd) = vcawp d Q;
-                              (vcc,wpc) = vcawp c Q
-                          in (\<lambda>s. vcc s & vcd s,
-                              \<lambda>s.(b s --> wpc s) & (~b s --> wpd s)))"
-| "vcawp (Awhile b I c) Q = (let (vcc,wpc) = vcawp c I
-                             in (\<lambda>s. (I s & ~b s --> Q s) &
-                                     (I s & b s --> wpc s) & vcc s, I))"
-
-(*
-Soundness and completeness of vc
-*)
-
-declare hoare.conseq [intro]
-
-
-lemma vc_sound: "(ALL s. vc c Q s) \<Longrightarrow> |- {awp c Q} astrip c {Q}"
-proof(induct c arbitrary: Q)
-  case (Awhile b I c)
-  show ?case
-  proof(simp, rule While')
-    from `\<forall>s. vc (Awhile b I c) Q s`
-    have vc: "ALL s. vc c I s" and IQ: "ALL s. I s \<and> \<not> b s \<longrightarrow> Q s" and
-         awp: "ALL s. I s & b s --> awp c I s" by simp_all
-    from vc have "|- {awp c I} astrip c {I}" using Awhile.hyps by blast
-    with awp show "|- {\<lambda>s. I s \<and> b s} astrip c {I}"
-      by(rule strengthen_pre)
-    show "\<forall>s. I s \<and> \<not> b s \<longrightarrow> Q s" by(rule IQ)
-  qed
-qed auto
-
-
-lemma awp_mono:
-  "(!s. P s --> Q s) ==> awp c P s ==> awp c Q s"
-proof (induct c arbitrary: P Q s)
-  case Asemi thus ?case by simp metis
-qed simp_all
-
-lemma vc_mono:
-  "(!s. P s --> Q s) ==> vc c P s ==> vc c Q s"
-proof(induct c arbitrary: P Q)
-  case Asemi thus ?case by simp (metis awp_mono)
-qed simp_all
-
-lemma vc_complete: assumes der: "|- {P}c{Q}"
-  shows "(\<exists>ac. astrip ac = c & (\<forall>s. vc ac Q s) & (\<forall>s. P s --> awp ac Q s))"
-  (is "? ac. ?Eq P c Q ac")
-using der
-proof induct
-  case skip
-  show ?case (is "? ac. ?C ac")
-  proof show "?C Askip" by simp qed
-next
-  case (ass P x a)
-  show ?case (is "? ac. ?C ac")
-  proof show "?C(Aass x a)" by simp qed
-next
-  case (semi P c1 Q c2 R)
-  from semi.hyps obtain ac1 where ih1: "?Eq P c1 Q ac1" by fast
-  from semi.hyps obtain ac2 where ih2: "?Eq Q c2 R ac2" by fast
-  show ?case (is "? ac. ?C ac")
-  proof
-    show "?C(Asemi ac1 ac2)"
-      using ih1 ih2 by simp (fast elim!: awp_mono vc_mono)
-  qed
-next
-  case (If P b c1 Q c2)
-  from If.hyps obtain ac1 where ih1: "?Eq (%s. P s & b s) c1 Q ac1" by fast
-  from If.hyps obtain ac2 where ih2: "?Eq (%s. P s & ~b s) c2 Q ac2" by fast
-  show ?case (is "? ac. ?C ac")
-  proof
-    show "?C(Aif b ac1 ac2)"
-      using ih1 ih2 by simp
-  qed
-next
-  case (While P b c)
-  from While.hyps obtain ac where ih: "?Eq (%s. P s & b s) c P ac" by fast
-  show ?case (is "? ac. ?C ac")
-  proof show "?C(Awhile b P ac)" using ih by simp qed
-next
-  case conseq thus ?case by(fast elim!: awp_mono vc_mono)
-qed
-
-lemma vcawp_vc_awp: "vcawp c Q = (vc c Q, awp c Q)"
-  by (induct c arbitrary: Q) (simp_all add: Let_def)
-
-end
diff -r 9ed5d8ad8fa0 -r faba4800b00b src/HOL/IMP/document/root.tex
--- a/src/HOL/IMP/document/root.tex	Wed Jun 01 19:50:59 2011 +0200
+++ b/src/HOL/IMP/document/root.tex	Wed Jun 01 23:08:04 2011 +0200
@@ -1,13 +1,38 @@
+\documentclass[11pt,a4paper]{article}
+\usepackage{isabelle,isabellesym}
 
-\documentclass[a4wide]{article}
-\usepackage{graphicx,isabelle,isabellesym}
+% further packages required for unusual symbols (see also
+% isabellesym.sty), use only when needed
+
+%\usepackage{amssymb}
+  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
+  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
+  %\<triangleq>, \<yen>, \<lozenge>
+
+%\usepackage[greek,english]{babel}
+  %option greek for \<euro>
+  %option english (default language) for \<guillemotleft>, \<guillemotright>
+
+%\usepackage[latin1]{inputenc}
+  %for \<onesuperior>, \<onequarter>, \<twosuperior>, \<onehalf>,
+  %\<threesuperior>, \<threequarters>, \<degree>
+
+%\usepackage[only,bigsqcap]{stmaryrd}
+  %for \<Sqinter>
+
+%\usepackage{eufrak}
+  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
+
+%\usepackage{textcomp}
+  %for \<cent>, \<currency>
+
+% this should be the last package used
 \usepackage{pdfsetup}
 
+% urls in roman style, theory text in math-similar italics
 \urlstyle{rm}
-\renewcommand{\isachardoublequote}{}
+\isabellestyle{it}
 
-% pretty printing for the Com language
-%\newcommand{\CMD}[1]{\isatext{\bf\sffamily#1}}
 \newcommand{\CMD}[1]{\isatext{\rm\sffamily#1}}
 \newcommand{\isasymSKIP}{\CMD{skip}}
 \newcommand{\isasymIF}{\CMD{if}}
@@ -16,37 +41,26 @@
 \newcommand{\isasymWHILE}{\CMD{while}}
 \newcommand{\isasymDO}{\CMD{do}}
 
-\addtolength{\hoffset}{-1cm}
-\addtolength{\textwidth}{2cm}
+% for uniform font size
+\renewcommand{\isastyle}{\isastyleminor}
+
 
 \begin{document}
 
-\title{IMP --- A {\tt WHILE}-language and its Semantics}
-\author{Gerwin Klein, Heiko Loetzbeyer, Tobias Nipkow, Robert Sandner}
+\title{Concrete Semantics}
+\author{TN \& GK}
 \maketitle
 
-\parindent 0pt\parskip 0.5ex
+\tableofcontents
+\newpage
 
-\begin{abstract}\noindent
-  The denotational, operational, and axiomatic semantics, a verification
-  condition generator, and all the necessary soundness, completeness and
-  equivalence proofs. Essentially a formalization of the first 100 pages of
-  \cite{Winskel}.
-  
-  An eminently readable description of this theory is found in \cite{Nipkow}.
-  See also HOLCF/IMP for a denotational semantics.
-\end{abstract}
-
-\tableofcontents
-
-\begin{center}
-  \includegraphics[scale=0.7]{session_graph}
-\end{center}
-
-\parindent 0pt\parskip 0.5ex
+% generated text of all theories
 \input{session}
 
-\bibliographystyle{plain}
+\nocite{Nipkow}
+
+% optional bibliography
+\bibliographystyle{abbrv}
 \bibliography{root}
 
 \end{document}
diff -r 9ed5d8ad8fa0 -r faba4800b00b src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Jun 01 19:50:59 2011 +0200
+++ b/src/HOL/IsaMakefile	Wed Jun 01 23:08:04 2011 +0200
@@ -525,9 +525,9 @@
 
 HOL-IMP: HOL $(LOG)/HOL-IMP.gz
 
-$(LOG)/HOL-IMP.gz: $(OUT)/HOL IMP/Com.thy IMP/Compiler0.thy		\
-  IMP/Compiler.thy IMP/Denotation.thy IMP/Expr.thy IMP/Hoare.thy	\
-  IMP/Natural.thy IMP/Examples.thy IMP/Transition.thy IMP/VC.thy	\
+$(LOG)/HOL-IMP.gz: $(OUT)/HOL IMP/ASM.thy IMP/AExp.thy IMP/BExp.thy	\
+  IMP/Big_Step.thy IMP/Com.thy IMP/Compiler.thy IMP/Denotation.thy 	\
+  IMP/Small_Step.thy IMP/Star.thy					\
   IMP/ROOT.ML IMP/document/root.tex IMP/document/root.bib
 	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL IMP
 
diff -r 9ed5d8ad8fa0 -r faba4800b00b src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Wed Jun 01 19:50:59 2011 +0200
+++ b/src/HOL/Wellfounded.thy	Wed Jun 01 23:08:04 2011 +0200
@@ -864,7 +864,7 @@
 
 lemma wf_bounded_measure:
 fixes ub :: "'a \<Rightarrow> nat" and f :: "'a \<Rightarrow> nat"
-assumes "!!a b. (b,a) : r \<Longrightarrow> ub b \<le> ub a & ub a > f b & f b > f a"
+assumes "!!a b. (b,a) : r \<Longrightarrow> ub b \<le> ub a & ub a \<ge> f b & f b > f a"
 shows "wf r"
 apply(rule wf_subset[OF wf_measure[of "%a. ub a - f a"]])
 apply (auto dest: assms)
@@ -873,11 +873,11 @@
 lemma wf_bounded_set:
 fixes ub :: "'a \<Rightarrow> 'b set" and f :: "'a \<Rightarrow> 'b set"
 assumes "!!a b. (b,a) : r \<Longrightarrow>
-  finite(ub a) & ub b \<subseteq> ub a & ub a \<supset> f b & f b \<supset> f a"
+  finite(ub a) & ub b \<subseteq> ub a & ub a \<supseteq> f b & f b \<supset> f a"
 shows "wf r"
 apply(rule wf_bounded_measure[of r "%a. card(ub a)" "%a. card(f a)"])
 apply(drule assms)
-apply (blast intro: card_mono finite_subset  psubset_card_mono dest: psubset_eq[THEN iffD2])
+apply (blast intro: card_mono finite_subset psubset_card_mono dest: psubset_eq[THEN iffD2])
 done