# HG changeset patch
# User kleing
# Date 1307370578 -7200
# Node ID 686fa0a0696e9975d562ed8d4266f24e81bd4135
# Parent  b505be6f029a4f21a737a5dae55b80e91a3267bd
imported rest of new IMP

diff -r b505be6f029a -r 686fa0a0696e src/HOL/IMP/AExp.thy
--- a/src/HOL/IMP/AExp.thy	Mon Jun 06 16:29:13 2011 +0200
+++ b/src/HOL/IMP/AExp.thy	Mon Jun 06 16:29:38 2011 +0200
@@ -18,12 +18,42 @@
 
 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)"
+text {* The same state more concisely: *}
+value "aval (Plus (V ''x'') (N 5)) ((%x. 0) (''x'':= 7))"
+
+text {* A little syntax magic to write larger states compactly: *}
+
+nonterminal funlets and funlet
+
+syntax
+  "_funlet"  :: "['a, 'a] => funlet"             ("_ /->/ _")
+   ""         :: "funlet => funlets"             ("_")
+  "_Funlets" :: "[funlet, funlets] => funlets"   ("_,/ _")
+  "_Fun"     :: "funlets => 'a => 'b"            ("(1[_])")
+  "_FunUpd"  :: "['a => 'b, funlets] => 'a => 'b" ("_/'(_')" [900,0]900)
+
+syntax (xsymbols)
+  "_funlet"  :: "['a, 'a] => funlet"             ("_ /\<rightarrow>/ _")
 
-value "aval (Plus (V ''x'') (N 5)) (lookup [(''x'',7)])"
+translations
+  "_FunUpd m (_Funlets xy ms)"  == "_FunUpd (_FunUpd m xy) ms"
+  "_FunUpd m (_funlet  x y)"    == "m(x := y)"
+  "_Fun ms"                     == "_FunUpd (%_. 0) ms"
+  "_Fun (_Funlets ms1 ms2)"     <= "_FunUpd (_Fun ms1) ms2"
+  "_Funlets ms1 (_Funlets ms2 ms3)" <= "_Funlets (_Funlets ms1 ms2) ms3"
 
-value "aval (Plus (V ''x'') (N 5)) (lookup [(''y'',7)])"
+text {* 
+  We can now write a series of updates to the function @{text "\<lambda>x. 0"} compactly:
+*}
+lemma "[a \<rightarrow> Suc 0, b \<rightarrow> 2] = ((%_. 0) (a := Suc 0)) (b := 2)"
+  by (rule refl)
+
+value "aval (Plus (V ''x'') (N 5)) [''x'' \<rightarrow> 7]"
+
+text {* Variables that are not mentioned in the state are 0 by default in 
+  the @{term "[a \<rightarrow> b::int]"} syntax: 
+*}   
+value "aval (Plus (V ''x'') (N 5)) [''y'' \<rightarrow> 7]"
 
 
 subsection "Optimization"
@@ -53,7 +83,6 @@
 "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
 
diff -r b505be6f029a -r 686fa0a0696e src/HOL/IMP/ASM.thy
--- a/src/HOL/IMP/ASM.thy	Mon Jun 06 16:29:13 2011 +0200
+++ b/src/HOL/IMP/ASM.thy	Mon Jun 06 16:29:38 2011 +0200
@@ -25,7 +25,7 @@
 "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]"
+ [''x'' \<rightarrow> 42, ''y'' \<rightarrow> 43] [50]"
 
 lemma aexec_append[simp]:
   "aexec (is1@is2) s stk = aexec is2 s (aexec is1 s stk)"
diff -r b505be6f029a -r 686fa0a0696e src/HOL/IMP/BExp.thy
--- a/src/HOL/IMP/BExp.thy	Mon Jun 06 16:29:13 2011 +0200
+++ b/src/HOL/IMP/BExp.thy	Mon Jun 06 16:29:38 2011 +0200
@@ -11,7 +11,7 @@
 "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)])"
+            [''x'' \<rightarrow> 3, ''y'' \<rightarrow> 1]"
 
 
 subsection "Optimization"
diff -r b505be6f029a -r 686fa0a0696e src/HOL/IMP/Big_Step.thy
--- a/src/HOL/IMP/Big_Step.thy	Mon Jun 06 16:29:13 2011 +0200
+++ b/src/HOL/IMP/Big_Step.thy	Mon Jun 06 16:29:38 2011 +0200
@@ -37,18 +37,18 @@
 text{* For inductive definitions we need command
        \texttt{values} instead of \texttt{value}. *}
 
-values "{t. (SKIP, lookup[]) \<Rightarrow> t}"
+values "{t. (SKIP, %_. 0) \<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. (SKIP, [''x'' \<rightarrow> 42]) \<Rightarrow> t}"
 
-values "{map t [''x''] |t. (''x'' ::= N 2, lookup [(''x'',42)]) \<Rightarrow> t}"
+values "{map t [''x''] |t. (''x'' ::= N 2, [''x'' \<rightarrow> 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}"
+   [''x'' \<rightarrow> 0, ''y'' \<rightarrow> 13]) \<Rightarrow> t}"
 
 
 text{* Proof automation: *}
diff -r b505be6f029a -r 686fa0a0696e src/HOL/IMP/C_like.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/C_like.thy	Mon Jun 06 16:29:38 2011 +0200
@@ -0,0 +1,95 @@
+theory C_like imports Main begin
+
+subsection "A C-like Language"
+
+type_synonym state = "nat \<Rightarrow> nat"
+
+datatype aexp = N nat | Deref aexp ("!") | Plus aexp aexp
+
+fun aval :: "aexp \<Rightarrow> state \<Rightarrow> nat" where
+"aval (N n) s = n" |
+"aval (!a) s = s(aval a s)" |
+"aval (Plus a\<^isub>1 a\<^isub>2) s = aval a\<^isub>1 s + aval a\<^isub>2 s"
+
+datatype bexp = B bool | Not bexp | And bexp bexp | Less aexp aexp
+
+primrec bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where
+"bval (B bv) _ = bv" |
+"bval (Not b) s = (\<not> bval b s)" |
+"bval (And b\<^isub>1 b\<^isub>2) s = (if bval b\<^isub>1 s then bval b\<^isub>2 s else False)" |
+"bval (Less a\<^isub>1 a\<^isub>2) s = (aval a\<^isub>1 s < aval a\<^isub>2 s)"
+
+
+datatype
+  com = SKIP 
+      | Assign aexp aexp         ("_ ::= _" [61, 61] 61)
+      | New    aexp aexp
+      | 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)
+
+inductive
+  big_step :: "com \<times> state \<times> nat \<Rightarrow> state \<times> nat \<Rightarrow> bool"  (infix "\<Rightarrow>" 55)
+where
+Skip:    "(SKIP,sn) \<Rightarrow> sn" |
+Assign:  "(lhs ::= a,s,n) \<Rightarrow> (s(aval lhs s := aval a s),n)" |
+New:     "(New lhs a,s,n) \<Rightarrow> (s(aval lhs s := n), n+aval a s)"  |
+Semi:    "\<lbrakk> (c\<^isub>1,sn\<^isub>1) \<Rightarrow> sn\<^isub>2;  (c\<^isub>2,sn\<^isub>2) \<Rightarrow> sn\<^isub>3 \<rbrakk> \<Longrightarrow>
+          (c\<^isub>1;c\<^isub>2, sn\<^isub>1) \<Rightarrow> sn\<^isub>3" |
+
+IfTrue:  "\<lbrakk> bval b s;  (c\<^isub>1,s,n) \<Rightarrow> tn \<rbrakk> \<Longrightarrow>
+         (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s,n) \<Rightarrow> tn" |
+IfFalse: "\<lbrakk> \<not>bval b s;  (c\<^isub>2,s,n) \<Rightarrow> tn \<rbrakk> \<Longrightarrow>
+         (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s,n) \<Rightarrow> tn" |
+
+WhileFalse: "\<not>bval b s \<Longrightarrow> (WHILE b DO c,s,n) \<Rightarrow> (s,n)" |
+WhileTrue:
+  "\<lbrakk> bval b s\<^isub>1;  (c,s\<^isub>1,n) \<Rightarrow> sn\<^isub>2;  (WHILE b DO c, sn\<^isub>2) \<Rightarrow> sn\<^isub>3 \<rbrakk> \<Longrightarrow>
+   (WHILE b DO c, s\<^isub>1,n) \<Rightarrow> sn\<^isub>3"
+
+code_pred big_step .
+
+
+text{* Examples: *}
+
+definition
+"array_sum =
+ WHILE Less (!(N 0)) (Plus (!(N 1)) (N 1))
+ DO ( N 2 ::= Plus (!(N 2)) (!(!(N 0)));
+      N 0 ::= Plus (!(N 0)) (N 1) )"
+
+text {* To show the first n variables in a @{typ "nat \<Rightarrow> nat"} state: *}
+definition 
+  "list t n = map t [0 ..< n]"
+
+values "{list t n |t n. (array_sum, nth[3,4,0,3,7],5) \<Rightarrow> (t,n)}"
+
+definition
+"linked_list_sum =
+ WHILE Less (N 0) (!(N 0))
+ DO ( N 1 ::= Plus(!(N 1)) (!(!(N 0)));
+      N 0 ::= !(Plus(!(N 0))(N 1)) )"
+
+values "{list t n |t n. (linked_list_sum, nth[4,0,3,0,7,2],6) \<Rightarrow> (t,n)}"
+
+definition
+"array_init =
+ New (N 0) (!(N 1)); N 2 ::= !(N 0);
+ WHILE Less (!(N 2)) (Plus (!(N 0)) (!(N 1)))
+ DO ( !(N 2) ::= !(N 2);
+      N 2 ::= Plus (!(N 2)) (N 1) )"
+
+values "{list t n |t n. (array_init, nth[5,2,7],3) \<Rightarrow> (t,n)}"
+
+definition
+"linked_list_init =
+ WHILE Less (!(N 1)) (!(N 0))
+ DO ( New (N 3) (N 2);
+      N 1 ::=  Plus (!(N 1)) (N 1);
+      !(N 3) ::= !(N 1);
+      Plus (!(N 3)) (N 1) ::= !(N 2);
+      N 2 ::= !(N 3) )"
+
+values "{list t n |t n. (linked_list_init, nth[2,0,0,0],4) \<Rightarrow> (t,n)}"
+
+end
diff -r b505be6f029a -r 686fa0a0696e src/HOL/IMP/Compiler.thy
--- a/src/HOL/IMP/Compiler.thy	Mon Jun 06 16:29:13 2011 +0200
+++ b/src/HOL/IMP/Compiler.thy	Mon Jun 06 16:29:38 2011 +0200
@@ -60,7 +60,7 @@
 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)}"
+    (0, [''x'' \<rightarrow> 3, ''y'' \<rightarrow> 4], []) \<rightarrow>* (i,t,stk)}"
 
 
 subsection{* Verification infrastructure *}
diff -r b505be6f029a -r 686fa0a0696e src/HOL/IMP/Def_Ass.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Def_Ass.thy	Mon Jun 06 16:29:38 2011 +0200
@@ -0,0 +1,25 @@
+theory Def_Ass imports Vars Com
+begin
+
+subsection "Definite Assignment Analysis"
+
+inductive D :: "name set \<Rightarrow> com \<Rightarrow> name set \<Rightarrow> bool" where
+Skip: "D A SKIP A" |
+Assign: "vars a \<subseteq> A \<Longrightarrow> D A (x ::= a) (insert x A)" |
+Semi: "\<lbrakk> D A\<^isub>1 c\<^isub>1 A\<^isub>2;  D A\<^isub>2 c\<^isub>2 A\<^isub>3 \<rbrakk> \<Longrightarrow> D A\<^isub>1 (c\<^isub>1; c\<^isub>2) A\<^isub>3" |
+If: "\<lbrakk> vars b \<subseteq> A;  D A c\<^isub>1 A\<^isub>1;  D A c\<^isub>2 A\<^isub>2 \<rbrakk> \<Longrightarrow>
+  D A (IF b THEN c\<^isub>1 ELSE c\<^isub>2) (A\<^isub>1 Int A\<^isub>2)" |
+While: "\<lbrakk> vars b \<subseteq> A;  D A c A' \<rbrakk> \<Longrightarrow> D A (WHILE b DO c) A"
+
+inductive_cases [elim!]:
+"D A SKIP A'"
+"D A (x ::= a) A'"
+"D A (c1;c2) A'"
+"D A (IF b THEN c1 ELSE c2) A'"
+"D A (WHILE b DO c) A'"
+
+lemma D_incr: 
+  "D A c A' \<Longrightarrow> A \<subseteq> A'"
+by (induct rule: D.induct) auto
+
+end
diff -r b505be6f029a -r 686fa0a0696e src/HOL/IMP/Def_Ass_Big.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Def_Ass_Big.thy	Mon Jun 06 16:29:38 2011 +0200
@@ -0,0 +1,31 @@
+(* Author: Tobias Nipkow *)
+
+theory Def_Ass_Big imports Com Def_Ass_Exp
+begin
+
+subsection "Initialization-Sensitive Big Step Semantics"
+
+inductive
+  big_step :: "(com \<times> state option) \<Rightarrow> state option \<Rightarrow> bool" (infix "\<Rightarrow>" 55)
+where
+None: "(c,None) \<Rightarrow> None" |
+Skip: "(SKIP,s) \<Rightarrow> s" |
+AssignNone: "aval a s = None \<Longrightarrow> (x ::= a, Some s) \<Rightarrow> None" |
+Assign: "aval a s = Some i \<Longrightarrow> (x ::= a, Some s) \<Rightarrow> Some(s(x := Some i))" |
+Semi:   "(c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2 \<Longrightarrow> (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3 \<Longrightarrow> (c\<^isub>1;c\<^isub>2,s\<^isub>1) \<Rightarrow> s\<^isub>3" |
+
+IfNone:  "bval b s = None \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,Some s) \<Rightarrow> None" |
+IfTrue:  "\<lbrakk> bval b s = Some True;  (c\<^isub>1,Some s) \<Rightarrow> s' \<rbrakk> \<Longrightarrow>
+  (IF b THEN c\<^isub>1 ELSE c\<^isub>2,Some s) \<Rightarrow> s'" |
+IfFalse: "\<lbrakk> bval b s = Some False;  (c\<^isub>2,Some s) \<Rightarrow> s' \<rbrakk> \<Longrightarrow>
+  (IF b THEN c\<^isub>1 ELSE c\<^isub>2,Some s) \<Rightarrow> s'" |
+
+WhileNone: "bval b s = None \<Longrightarrow> (WHILE b DO c,Some s) \<Rightarrow> None" |
+WhileFalse: "bval b s = Some False \<Longrightarrow> (WHILE b DO c,Some s) \<Rightarrow> Some s" |
+WhileTrue:
+  "\<lbrakk> bval b s = Some True;  (c,Some s) \<Rightarrow> s';  (WHILE b DO c,s') \<Rightarrow> s'' \<rbrakk> \<Longrightarrow>
+  (WHILE b DO c,Some s) \<Rightarrow> s''"
+
+lemmas big_step_induct = big_step.induct[split_format(complete)]
+
+end
diff -r b505be6f029a -r 686fa0a0696e src/HOL/IMP/Def_Ass_Exp.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Def_Ass_Exp.thy	Mon Jun 06 16:29:38 2011 +0200
@@ -0,0 +1,35 @@
+(* Author: Tobias Nipkow *)
+
+theory Def_Ass_Exp imports Vars
+begin
+
+subsection "Initialization-Sensitive Expressions Evaluation"
+
+type_synonym val = "int"
+type_synonym state = "name \<Rightarrow> val option"
+
+
+fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val option" where
+"aval (N i) s = Some i" |
+"aval (V x) s = s x" |
+"aval (Plus a\<^isub>1 a\<^isub>2) s =
+  (case (aval a\<^isub>1 s, aval a\<^isub>2 s) of
+     (Some i\<^isub>1,Some i\<^isub>2) \<Rightarrow> Some(i\<^isub>1+i\<^isub>2) | _ \<Rightarrow> None)"
+
+
+fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool option" where
+"bval (B bv) s = Some bv" |
+"bval (Not b) s = (case bval b s of None \<Rightarrow> None | Some bv \<Rightarrow> Some(\<not> bv))" |
+"bval (And b\<^isub>1 b\<^isub>2) s = (case (bval b\<^isub>1 s, bval b\<^isub>2 s) of
+  (Some bv\<^isub>1, Some bv\<^isub>2) \<Rightarrow> Some(bv\<^isub>1 & bv\<^isub>2) | _ \<Rightarrow> None)" |
+"bval (Less a\<^isub>1 a\<^isub>2) s = (case (aval a\<^isub>1 s, aval a\<^isub>2 s) of
+ (Some i\<^isub>1, Some i\<^isub>2) \<Rightarrow> Some(i\<^isub>1 < i\<^isub>2) | _ \<Rightarrow> None)"
+
+
+lemma aval_Some: "vars a \<subseteq> dom s \<Longrightarrow> \<exists> i. aval a s = Some i"
+by (induct a) auto
+
+lemma bval_Some: "vars b \<subseteq> dom s \<Longrightarrow> \<exists> bv. bval b s = Some bv"
+by (induct b) (auto dest!: aval_Some)
+
+end
diff -r b505be6f029a -r 686fa0a0696e src/HOL/IMP/Def_Ass_Small.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Def_Ass_Small.thy	Mon Jun 06 16:29:38 2011 +0200
@@ -0,0 +1,26 @@
+(* Author: Tobias Nipkow *)
+
+theory Def_Ass_Small imports Star Com Def_Ass_Exp
+begin
+
+subsection "Initialization-Sensitive Small Step Semantics"
+
+inductive
+  small_step :: "(com \<times> state) \<Rightarrow> (com \<times> state) \<Rightarrow> bool" (infix "\<rightarrow>" 55)
+where
+Assign:  "aval a s = Some i \<Longrightarrow> (x ::= a, s) \<rightarrow> (SKIP, s(x := Some i))" |
+
+Semi1:   "(SKIP;c,s) \<rightarrow> (c,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 = Some True \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>1,s)" |
+IfFalse: "bval b s = Some False \<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)"
+
+lemmas small_step_induct = small_step.induct[split_format(complete)]
+
+abbreviation small_steps :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>*" 55)
+where "x \<rightarrow>* y == star small_step x y"
+
+end
diff -r b505be6f029a -r 686fa0a0696e src/HOL/IMP/Def_Ass_Sound_Big.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Def_Ass_Sound_Big.thy	Mon Jun 06 16:29:38 2011 +0200
@@ -0,0 +1,41 @@
+(* Author: Tobias Nipkow *)
+
+theory Def_Ass_Sound_Big imports Def_Ass Def_Ass_Big
+begin
+
+
+subsection "Soundness wrt Big Steps"
+
+text{* Note the special form of the induction because one of the arguments
+of the inductive predicate is not a variable but the term @{term"Some s"}: *}
+
+theorem Sound:
+  "\<lbrakk> (c,Some s) \<Rightarrow> s';  D A c A';  A \<subseteq> dom s \<rbrakk>
+  \<Longrightarrow> \<exists> t. s' = Some t \<and> A' \<subseteq> dom t"
+proof (induct c "Some s" s' arbitrary: s A A' rule:big_step_induct)
+  case AssignNone thus ?case
+    by auto (metis aval_Some option.simps(3) subset_trans)
+next
+  case Semi thus ?case by auto metis
+next
+  case IfTrue thus ?case by auto blast
+next
+  case IfFalse thus ?case by auto blast
+next
+  case IfNone thus ?case
+    by auto (metis bval_Some option.simps(3) order_trans)
+next
+  case WhileNone thus ?case
+    by auto (metis bval_Some option.simps(3) order_trans)
+next
+  case (WhileTrue b s c s' s'')
+  from `D A (WHILE b DO c) A'` obtain A' where "D A c A'" by blast
+  then obtain t' where "s' = Some t'" "A \<subseteq> dom t'"
+    by (metis D_incr WhileTrue(3,7) subset_trans)
+  from WhileTrue(5)[OF this(1) WhileTrue(6) this(2)] show ?case .
+qed auto
+
+corollary sound: "\<lbrakk>  D (dom s) c A';  (c,Some s) \<Rightarrow> s' \<rbrakk> \<Longrightarrow> s' \<noteq> None"
+by (metis Sound not_Some_eq subset_refl)
+
+end
diff -r b505be6f029a -r 686fa0a0696e src/HOL/IMP/Def_Ass_Sound_Small.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Def_Ass_Sound_Small.thy	Mon Jun 06 16:29:38 2011 +0200
@@ -0,0 +1,56 @@
+(* Author: Tobias Nipkow *)
+
+theory Def_Ass_Sound_Small imports Def_Ass Def_Ass_Small
+begin
+
+subsection "Soundness wrt Small Steps"
+
+theorem progress:
+  "D (dom s) c A' \<Longrightarrow> c \<noteq> SKIP \<Longrightarrow> EX cs'. (c,s) \<rightarrow> cs'"
+proof (induct c arbitrary: s A')
+  case Assign thus ?case by auto (metis aval_Some small_step.Assign)
+next
+  case (If b c1 c2)
+  then obtain bv where "bval b s = Some bv" by (auto dest!:bval_Some)
+  then show ?case
+    by(cases bv)(auto intro: small_step.IfTrue small_step.IfFalse)
+qed (fastsimp intro: small_step.intros)+
+
+lemma D_mono:  "D A c M \<Longrightarrow> A \<subseteq> A' \<Longrightarrow> EX M'. D A' c M' & M <= M'"
+proof (induct c arbitrary: A A' M)
+  case Semi thus ?case by auto (metis D.intros(3))
+next
+  case (If b c1 c2)
+  then obtain M1 M2 where "vars b \<subseteq> A" "D A c1 M1" "D A c2 M2" "M = M1 \<inter> M2"
+    by auto
+  with If.hyps `A \<subseteq> A'` obtain M1' M2'
+    where "D A' c1 M1'" "D A' c2 M2'" and "M1 \<subseteq> M1'" "M2 \<subseteq> M2'" by metis
+  hence "D A' (IF b THEN c1 ELSE c2) (M1' \<inter> M2')" and "M \<subseteq> M1' \<inter> M2'"
+    using `vars b \<subseteq> A` `A \<subseteq> A'` `M = M1 \<inter> M2` by(fastsimp intro: D.intros)+
+  thus ?case by metis
+next
+  case While thus ?case by auto (metis D.intros(5) subset_trans)
+qed (auto intro: D.intros)
+
+theorem D_preservation:
+  "(c,s) \<rightarrow> (c',s') \<Longrightarrow> D (dom s) c A \<Longrightarrow> EX A'. D (dom s') c' A' & A <= A'"
+proof (induct arbitrary: A rule: small_step_induct)
+  case (While b c s)
+  then obtain A' where "vars b \<subseteq> dom s" "A = dom s" "D (dom s) c A'" by blast
+  moreover
+  then obtain A'' where "D A' c A''" by (metis D_incr D_mono)
+  ultimately have "D (dom s) (IF b THEN c; WHILE b DO c ELSE SKIP) (dom s)"
+    by (metis D.If[OF `vars b \<subseteq> dom s` D.Semi[OF `D (dom s) c A'` D.While[OF _ `D A' c A''`]] D.Skip] D_incr Int_absorb1 subset_trans)
+  thus ?case by (metis D_incr `A = dom s`)
+next
+  case Semi2 thus ?case by auto (metis D_mono D.intros(3))
+qed (auto intro: D.intros)
+
+theorem D_sound:
+  "(c,s) \<rightarrow>* (c',s') \<Longrightarrow> D (dom s) c A' \<Longrightarrow> c' \<noteq> SKIP
+   \<Longrightarrow> \<exists>cs''. (c',s') \<rightarrow> cs''"
+apply(induct arbitrary: A' rule:star_induct)
+apply (metis progress)
+by (metis D_preservation)
+
+end
diff -r b505be6f029a -r 686fa0a0696e src/HOL/IMP/Hoare.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Hoare.thy	Mon Jun 06 16:29:38 2011 +0200
@@ -0,0 +1,59 @@
+(* Author: Tobias Nipkow *)
+
+header "Hoare Logic"
+
+theory Hoare imports Big_Step begin
+
+subsection "Hoare Logic for Partial Correctness"
+
+type_synonym assn = "state \<Rightarrow> bool"
+
+abbreviation state_subst :: "state \<Rightarrow> aexp \<Rightarrow> name \<Rightarrow> state"
+  ("_[_'/_]" [1000,0,0] 999)
+where "s[a/x] == s(x := aval a s)"
+
+inductive
+  hoare :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<turnstile> ({(1_)}/ (_)/ {(1_)})" 50)
+where
+Skip: "\<turnstile> {P} SKIP {P}"  |
+
+Assign:  "\<turnstile> {\<lambda>s. P(s[a/x])} x::=a {P}"  |
+
+Semi: "\<lbrakk> \<turnstile> {P} c\<^isub>1 {Q};  \<turnstile> {Q} c\<^isub>2 {R} \<rbrakk>
+       \<Longrightarrow> \<turnstile> {P} c\<^isub>1;c\<^isub>2 {R}"  |
+
+If: "\<lbrakk> \<turnstile> {\<lambda>s. P s \<and> bval b s} c\<^isub>1 {Q};  \<turnstile> {\<lambda>s. P s \<and> \<not> bval b s} c\<^isub>2 {Q} \<rbrakk>
+     \<Longrightarrow> \<turnstile> {P} IF b THEN c\<^isub>1 ELSE c\<^isub>2 {Q}"  |
+
+While: "\<turnstile> {\<lambda>s. P s \<and> bval b s} c {P} \<Longrightarrow>
+        \<turnstile> {P} WHILE b DO c {\<lambda>s. P s \<and> \<not> bval b s}"  |
+
+conseq: "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s;  \<turnstile> {P} c {Q};  \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk>
+        \<Longrightarrow> \<turnstile> {P'} c {Q'}"
+
+lemmas [simp] = hoare.Skip hoare.Assign hoare.Semi If
+
+lemmas [intro!] = hoare.Skip hoare.Assign hoare.Semi hoare.If
+
+lemma strengthen_pre:
+  "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s;  \<turnstile> {P} c {Q} \<rbrakk> \<Longrightarrow> \<turnstile> {P'} c {Q}"
+by (blast intro: conseq)
+
+lemma weaken_post:
+  "\<lbrakk> \<turnstile> {P} c {Q};  \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk> \<Longrightarrow>  \<turnstile> {P} c {Q'}"
+by (blast intro: conseq)
+
+text{* The assignment and While rule are awkward to use in actual proofs
+because their pre and postcondition are of a very special form and the actual
+goal would have to match this form exactly. Therefore we derive two variants
+with arbitrary pre and postconditions. *}
+
+lemma Assign': "\<forall>s. P s \<longrightarrow> Q(s[a/x]) \<Longrightarrow> \<turnstile> {P} x ::= a {Q}"
+by (simp add: strengthen_pre[OF _ Assign])
+
+lemma While':
+assumes "\<turnstile> {\<lambda>s. P s \<and> bval b s} c {P}" and "\<forall>s. P s \<and> \<not> bval b s \<longrightarrow> Q s"
+shows "\<turnstile> {P} WHILE b DO c {Q}"
+by(rule weaken_post[OF While[OF assms(1)] assms(2)])
+
+end
diff -r b505be6f029a -r 686fa0a0696e src/HOL/IMP/HoareT.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/HoareT.thy	Mon Jun 06 16:29:38 2011 +0200
@@ -0,0 +1,215 @@
+header{* Hoare Logic for Total Correctness *}
+
+theory HoareT imports Hoare_Sound_Complete Util begin
+
+text{*
+Now that we have termination, we can define
+total validity, @{text"\<Turnstile>\<^sub>t"}, as partial validity and guaranteed termination:*}
+
+definition hoare_tvalid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool"
+  ("\<Turnstile>\<^sub>t {(1_)}/ (_)/ {(1_)}" 50) where
+"\<Turnstile>\<^sub>t {P}c{Q}  \<equiv>  \<forall>s. P s \<longrightarrow> (\<exists>t. (c,s) \<Rightarrow> t \<and> Q t)"
+
+text{* Proveability of Hoare triples in the proof system for total
+correctness is written @{text"\<turnstile>\<^sub>t {P}c{Q}"} and defined
+inductively. The rules for @{text"\<turnstile>\<^sub>t"} differ from those for
+@{text"\<turnstile>"} only in the one place where nontermination can arise: the
+@{term While}-rule. *}
+
+inductive
+  hoaret :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<turnstile>\<^sub>t ({(1_)}/ (_)/ {(1_)})" 50)
+where
+Skip:  "\<turnstile>\<^sub>t {P} SKIP {P}" |
+Assign:  "\<turnstile>\<^sub>t {\<lambda>s. P(s[a/x])} x::=a {P}" |
+Semi: "\<lbrakk> \<turnstile>\<^sub>t {P\<^isub>1} c\<^isub>1 {P\<^isub>2}; \<turnstile>\<^sub>t {P\<^isub>2} c\<^isub>2 {P\<^isub>3} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P\<^isub>1} c\<^isub>1;c\<^isub>2 {P\<^isub>3}" |
+If: "\<lbrakk> \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s} c\<^isub>1 {Q}; \<turnstile>\<^sub>t {\<lambda>s. P s \<and> \<not> bval b s} c\<^isub>2 {Q} \<rbrakk>
+  \<Longrightarrow> \<turnstile>\<^sub>t {P} IF b THEN c\<^isub>1 ELSE c\<^isub>2 {Q}" |
+While:
+  "\<lbrakk> \<And>n::nat. \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> f s = n} c {\<lambda>s. P s \<and> f s < n}\<rbrakk>
+   \<Longrightarrow> \<turnstile>\<^sub>t {P} WHILE b DO c {\<lambda>s. P s \<and> \<not>bval b s}" |
+conseq: "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile>\<^sub>t {P}c{Q}; \<forall>s. Q s \<longrightarrow> Q' s  \<rbrakk> \<Longrightarrow>
+           \<turnstile>\<^sub>t {P'}c{Q'}"
+
+text{* The @{term While}-rule is like the one for partial correctness but it
+requires additionally that with every execution of the loop body some measure
+function @{term[source]"f :: state \<Rightarrow> nat"} decreases. *}
+
+lemma strengthen_pre:
+  "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s;  \<turnstile>\<^sub>t {P} c {Q} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P'} c {Q}"
+by (metis conseq)
+
+lemma weaken_post:
+  "\<lbrakk> \<turnstile>\<^sub>t {P} c {Q};  \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk> \<Longrightarrow>  \<turnstile>\<^sub>t {P} c {Q'}"
+by (metis conseq)
+
+lemma Assign': "\<forall>s. P s \<longrightarrow> Q(s[a/x]) \<Longrightarrow> \<turnstile>\<^sub>t {P} x ::= a {Q}"
+by (simp add: strengthen_pre[OF _ Assign])
+
+lemma While':
+assumes "\<And>n::nat. \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> f s = n} c {\<lambda>s. P s \<and> f s < n}"
+    and "\<forall>s. P s \<and> \<not> bval b s \<longrightarrow> Q s"
+shows "\<turnstile>\<^sub>t {P} WHILE b DO c {Q}"
+by(blast intro: assms(1) weaken_post[OF While assms(2)])
+
+text{* Our standard example: *}
+
+abbreviation "w n ==
+  WHILE Less (V ''y'') (N n)
+  DO ( ''y'' ::= Plus (V ''y'') (N 1); ''x'' ::= Plus (V ''x'') (V ''y'') )"
+
+lemma "\<turnstile>\<^sub>t {\<lambda>s. 0 <= n} ''x'' ::= N 0; ''y'' ::= N 0; w n {\<lambda>s. s ''x'' = \<Sum> {1 .. n}}"
+apply(rule Semi)
+prefer 2
+apply(rule While'
+  [where P = "\<lambda>s. s ''x'' = \<Sum> {1..s ''y''} \<and> 0 <= n \<and> 0 <= s ''y'' \<and> s ''y'' \<le> n"
+   and f = "\<lambda>s. nat n - nat (s ''y'')"])
+apply(rule Semi)
+prefer 2
+apply(rule Assign)
+apply(rule Assign')
+apply (simp add: atLeastAtMostPlus1_int_conv algebra_simps)
+apply clarsimp
+apply arith
+apply fastsimp
+apply(rule Semi)
+prefer 2
+apply(rule Assign)
+apply(rule Assign')
+apply simp
+done
+
+
+text{* The soundness theorem: *}
+
+theorem hoaret_sound: "\<turnstile>\<^sub>t {P}c{Q}  \<Longrightarrow>  \<Turnstile>\<^sub>t {P}c{Q}"
+proof(unfold hoare_tvalid_def, induct rule: hoaret.induct)
+  case (While P b f c)
+  show ?case
+  proof
+    fix s
+    show "P s \<longrightarrow> (\<exists>t. (WHILE b DO c, s) \<Rightarrow> t \<and> P t \<and> \<not> bval b t)"
+    proof(induct "f s" arbitrary: s rule: less_induct)
+      case (less n)
+      thus ?case by (metis While(2) WhileFalse WhileTrue)
+    qed
+  qed
+next
+  case If thus ?case by auto blast
+qed fastsimp+
+
+
+text{*
+The completeness proof proceeds along the same lines as the one for partial
+correctness. First we have to strengthen our notion of weakest precondition
+to take termination into account: *}
+
+definition wpt :: "com \<Rightarrow> assn \<Rightarrow> assn" ("wp\<^sub>t") where
+"wp\<^sub>t c Q  \<equiv>  \<lambda>s. \<exists>t. (c,s) \<Rightarrow> t \<and> Q t"
+
+lemma [simp]: "wp\<^sub>t SKIP Q = Q"
+by(auto intro!: ext simp: wpt_def)
+
+lemma [simp]: "wp\<^sub>t (x ::= e) Q = (\<lambda>s. Q(s(x := aval e s)))"
+by(auto intro!: ext simp: wpt_def)
+
+lemma [simp]: "wp\<^sub>t (c\<^isub>1;c\<^isub>2) Q = wp\<^sub>t c\<^isub>1 (wp\<^sub>t c\<^isub>2 Q)"
+unfolding wpt_def
+apply(rule ext)
+apply auto
+done
+
+lemma [simp]:
+ "wp\<^sub>t (IF b THEN c\<^isub>1 ELSE c\<^isub>2) Q = (\<lambda>s. wp\<^sub>t (if bval b s then c\<^isub>1 else c\<^isub>2) Q s)"
+apply(unfold wpt_def)
+apply(rule ext)
+apply auto
+done
+
+
+text{* Now we define the number of iterations @{term "WHILE b DO c"} needs to
+terminate when started in state @{text s}. Because this is a truly partial
+function, we define it as an (inductive) relation first: *}
+
+inductive Its :: "bexp \<Rightarrow> com \<Rightarrow> state \<Rightarrow> nat \<Rightarrow> bool" where
+Its_0: "\<not> bval b s \<Longrightarrow> Its b c s 0" |
+Its_Suc: "\<lbrakk> bval b s;  (c,s) \<Rightarrow> s';  Its b c s' n \<rbrakk> \<Longrightarrow> Its b c s (Suc n)"
+
+text{* The relation is in fact a function: *}
+
+lemma Its_fun: "Its b c s n \<Longrightarrow> Its b c s n' \<Longrightarrow> n=n'"
+proof(induct arbitrary: n' rule:Its.induct)
+(* new release:
+  case Its_0 thus ?case by(metis Its.cases)
+next
+  case Its_Suc thus ?case by(metis Its.cases big_step_determ)
+qed
+*)
+  case Its_0
+  from this(1) Its.cases[OF this(2)] show ?case by metis
+next
+  case (Its_Suc b s c s' n n')
+  note C = this
+  from this(5) show ?case
+  proof cases
+    case Its_0 with Its_Suc(1) show ?thesis by blast
+  next
+    case Its_Suc with C show ?thesis by(metis big_step_determ)
+  qed
+qed
+
+text{* For all terminating loops, @{const Its} yields a result: *}
+
+lemma WHILE_Its: "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> \<exists>n. Its b c s n"
+proof(induct "WHILE b DO c" s t rule: big_step_induct)
+  case WhileFalse thus ?case by (metis Its_0)
+next
+  case WhileTrue thus ?case by (metis Its_Suc)
+qed
+
+text{* Now the relation is turned into a function with the help of
+the description operator @{text THE}: *}
+
+definition its :: "bexp \<Rightarrow> com \<Rightarrow> state \<Rightarrow> nat" where
+"its b c s = (THE n. Its b c s n)"
+
+text{* The key property: every loop iteration increases @{const its} by 1. *}
+
+lemma its_Suc: "\<lbrakk> bval b s; (c, s) \<Rightarrow> s'; (WHILE b DO c, s') \<Rightarrow> t\<rbrakk>
+       \<Longrightarrow> its b c s = Suc(its b c s')"
+by (metis its_def WHILE_Its Its.intros(2) Its_fun the_equality)
+
+lemma wpt_is_pre: "\<turnstile>\<^sub>t {wp\<^sub>t c Q} c {Q}"
+proof (induct c arbitrary: Q)
+  case SKIP show ?case by simp (blast intro:hoaret.Skip)
+next
+  case Assign show ?case by simp (blast intro:hoaret.Assign)
+next
+  case Semi thus ?case by simp (blast intro:hoaret.Semi)
+next
+  case If thus ?case by simp (blast intro:hoaret.If hoaret.conseq)
+next
+  case (While b c)
+  let ?w = "WHILE b DO c"
+  { fix n
+    have "\<forall>s. wp\<^sub>t ?w Q s \<and> bval b s \<and> its b c s = n \<longrightarrow>
+              wp\<^sub>t c (\<lambda>s'. wp\<^sub>t ?w Q s' \<and> its b c s' < n) s"
+      unfolding wpt_def by (metis WhileE its_Suc lessI)
+    note strengthen_pre[OF this While]
+  } note hoaret.While[OF this]
+  moreover have "\<forall>s. wp\<^sub>t ?w Q s \<and> \<not> bval b s \<longrightarrow> Q s" by (auto simp add:wpt_def)
+  ultimately show ?case by(rule weaken_post)
+qed
+
+
+text{*\noindent In the @{term While}-case, @{const its} provides the obvious
+termination argument.
+
+The actual completeness theorem follows directly, in the same manner
+as for partial correctness: *}
+
+theorem hoaret_complete: "\<Turnstile>\<^sub>t {P}c{Q} \<Longrightarrow> \<turnstile>\<^sub>t {P}c{Q}"
+apply(rule strengthen_pre[OF _ wpt_is_pre])
+apply(auto simp: hoare_tvalid_def hoare_valid_def wpt_def)
+done
+
+end
diff -r b505be6f029a -r 686fa0a0696e src/HOL/IMP/Hoare_Examples.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Hoare_Examples.thy	Mon Jun 06 16:29:38 2011 +0200
@@ -0,0 +1,78 @@
+(* Author: Tobias Nipkow *)
+
+theory Hoare_Examples imports Hoare Util begin
+
+subsection{* Example: Sums *}
+
+text{* Summing up the first @{text n} natural numbers. The sum is accumulated
+in variable @{text 0}, the loop counter is variable @{text 1}. *}
+
+abbreviation "w n ==
+  WHILE Less (V ''y'') (N n)
+  DO ( ''y'' ::= Plus (V ''y'') (N 1); ''x'' ::= Plus (V ''x'') (V ''y'') )"
+
+text{* For this example we make use of some predefined functions.  Function
+@{const Setsum}, also written @{text"\<Sum>"}, sums up the elements of a set. The
+set of numbers from @{text m} to @{text n} is written @{term "{m .. n}"}. *}
+
+subsubsection{* Proof by Operational Semantics *}
+
+text{* The behaviour of the loop is proved by induction: *}
+
+lemma setsum_head_plus_1:
+  "m \<le> n \<Longrightarrow> setsum f {m..n} = f m + setsum f {m+1..n::int}"
+by (subst simp_from_to) simp
+  
+lemma while_sum:
+  "(w n, s) \<Rightarrow> t \<Longrightarrow> t ''x'' = s ''x'' + \<Sum> {s ''y'' + 1 .. n}"
+apply(induct "w n" s t rule: big_step_induct)
+apply(auto simp add: setsum_head_plus_1)
+done
+
+text{* We were lucky that the proof was practically automatic, except for the
+induction. In general, such proofs will not be so easy. The automation is
+partly due to the right inversion rules that we set up as automatic
+elimination rules that decompose big-step premises.
+
+Now we prefix the loop with the necessary initialization: *}
+
+lemma sum_via_bigstep:
+assumes "(''x'' ::= N 0; ''y'' ::= N 0; w n, s) \<Rightarrow> t"
+shows "t ''x'' = \<Sum> {1 .. n}"
+proof -
+  from assms have "(w n,s(''x'':=0,''y'':=0)) \<Rightarrow> t" by auto
+  from while_sum[OF this] show ?thesis by simp
+qed
+
+
+subsubsection{* Proof by Hoare Logic *}
+
+text{* Note that we deal with sequences of commands from right to left,
+pulling back the postcondition towards the precondition. *}
+
+lemma "\<turnstile> {\<lambda>s. 0 <= n} ''x'' ::= N 0; ''y'' ::= N 0; w n {\<lambda>s. s ''x'' = \<Sum> {1 .. n}}"
+apply(rule hoare.Semi)
+prefer 2
+apply(rule While'
+  [where P = "\<lambda>s. s ''x'' = \<Sum> {1..s ''y''} \<and> 0 \<le> s ''y'' \<and> s ''y'' \<le> n"])
+apply(rule Semi)
+prefer 2
+apply(rule Assign)
+apply(rule Assign')
+apply(fastsimp simp: atLeastAtMostPlus1_int_conv algebra_simps)
+apply(fastsimp)
+apply(rule Semi)
+prefer 2
+apply(rule Assign)
+apply(rule Assign')
+apply simp
+done
+
+text{* The proof is intentionally an apply skript because it merely composes
+the rules of Hoare logic. Of course, in a few places side conditions have to
+be proved. But since those proofs are 1-liners, a structured proof is
+overkill. In fact, we shall learn later that the application of the Hoare
+rules can be automated completely and all that is left for the user is to
+provide the loop invariants and prove the side-conditions. *}
+
+end
diff -r b505be6f029a -r 686fa0a0696e src/HOL/IMP/Hoare_Sound_Complete.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Hoare_Sound_Complete.thy	Mon Jun 06 16:29:38 2011 +0200
@@ -0,0 +1,101 @@
+(* Author: Tobias Nipkow *)
+
+theory Hoare_Sound_Complete imports Hoare begin
+
+subsection "Soundness"
+
+definition
+hoare_valid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<Turnstile> {(1_)}/ (_)/ {(1_)}" 50) where
+"\<Turnstile> {P}c{Q} = (\<forall>s t. (c,s) \<Rightarrow> t  \<longrightarrow>  P s \<longrightarrow>  Q t)"
+
+lemma hoare_sound: "\<turnstile> {P}c{Q}  \<Longrightarrow>  \<Turnstile> {P}c{Q}"
+proof(induct rule: hoare.induct)
+  case (While P b c)
+  { fix s t
+    have "(WHILE b DO c,s) \<Rightarrow> t  \<Longrightarrow>  P s \<longrightarrow> P t \<and> \<not> bval b t"
+    proof(induct "WHILE b DO c" s t rule: big_step_induct)
+      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)
+
+
+subsection "Weakest Precondition"
+
+definition wp :: "com \<Rightarrow> assn \<Rightarrow> assn" where
+"wp c Q = (\<lambda>s. \<forall>t. (c,s) \<Rightarrow> t  \<longrightarrow>  Q t)"
+
+lemma wp_SKIP[simp]: "wp SKIP Q = Q"
+by (rule ext) (auto simp: wp_def)
+
+lemma wp_Ass[simp]: "wp (x::=a) Q = (\<lambda>s. Q(s[a/x]))"
+by (rule ext) (auto simp: wp_def)
+
+lemma wp_Semi[simp]: "wp (c\<^isub>1;c\<^isub>2) Q = wp c\<^isub>1 (wp c\<^isub>2 Q)"
+by (rule ext) (auto simp: wp_def)
+
+lemma wp_If[simp]:
+ "wp (IF b THEN c\<^isub>1 ELSE c\<^isub>2) Q =
+ (\<lambda>s. (bval b s \<longrightarrow> wp c\<^isub>1 Q s) \<and>  (\<not> bval b s \<longrightarrow> wp c\<^isub>2 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 unfold_while)
+
+lemma wp_While_True[simp]: "bval b s \<Longrightarrow>
+  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[simp]: "\<not> bval b s \<Longrightarrow> wp (WHILE b DO c) Q s = Q s"
+by(simp add: wp_While_If)
+
+
+subsection "Completeness"
+
+lemma wp_is_pre: "\<turnstile> {wp c Q} c {Q}"
+proof(induct c arbitrary: Q)
+  case Semi thus ?case by(auto intro: Semi)
+next
+  case (If b c1 c2)
+  let ?If = "IF b THEN c1 ELSE c2"
+  show ?case
+  proof(rule hoare.If)
+    show "\<turnstile> {\<lambda>s. wp ?If Q s \<and> bval b s} c1 {Q}"
+    proof(rule strengthen_pre[OF _ If(1)])
+      show "\<forall>s. wp ?If Q s \<and> bval b s \<longrightarrow> wp c1 Q s" by auto
+    qed
+    show "\<turnstile> {\<lambda>s. wp ?If Q s \<and> \<not> bval b s} c2 {Q}"
+    proof(rule strengthen_pre[OF _ If(2)])
+      show "\<forall>s. wp ?If Q s \<and> \<not> bval b s \<longrightarrow> wp c2 Q s" by auto
+    qed
+  qed
+next
+  case (While b c)
+  let ?w = "WHILE b DO c"
+  have "\<turnstile> {wp ?w Q} ?w {\<lambda>s. wp ?w Q s \<and> \<not> bval b s}"
+  proof(rule hoare.While)
+    show "\<turnstile> {\<lambda>s. wp ?w Q s \<and> bval b s} c {wp ?w Q}"
+    proof(rule strengthen_pre[OF _ While(1)])
+      show "\<forall>s. wp ?w Q s \<and> bval 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> bval b s \<longrightarrow> Q s" by auto
+  qed
+qed auto
+
+lemma hoare_relative_complete: assumes "\<Turnstile> {P}c{Q}" shows "\<turnstile> {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 "\<turnstile> {wp c Q} c {Q}" by(rule wp_is_pre)
+qed
+
+end
diff -r b505be6f029a -r 686fa0a0696e src/HOL/IMP/Live.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Live.thy	Mon Jun 06 16:29:38 2011 +0200
@@ -0,0 +1,249 @@
+(* Author: Tobias Nipkow *)
+
+header "Live Variable Analysis"
+
+theory Live imports Vars Big_Step
+begin
+
+subsection "Liveness Analysis"
+
+fun L :: "com \<Rightarrow> name set \<Rightarrow> name set" where
+"L SKIP X = X" |
+"L (x ::= a) X = X-{x} \<union> vars a" |
+"L (c\<^isub>1; c\<^isub>2) X = (L c\<^isub>1 \<circ> L c\<^isub>2) X" |
+"L (IF b THEN c\<^isub>1 ELSE c\<^isub>2) X = vars b \<union> L c\<^isub>1 X \<union> L c\<^isub>2 X" |
+"L (WHILE b DO c) X = vars b \<union> X \<union> L c X"
+
+value "show (L (''y'' ::= V ''z''; ''x'' ::= Plus (V ''y'') (V ''z'')) {''x''})"
+
+value "show (L (WHILE Less (V ''x'') (V ''x'') DO ''y'' ::= V ''z'') {''x''})"
+
+fun "kill" :: "com \<Rightarrow> name set" where
+"kill SKIP = {}" |
+"kill (x ::= a) = {x}" |
+"kill (c\<^isub>1; c\<^isub>2) = kill c\<^isub>1 \<union> kill c\<^isub>2" |
+"kill (IF b THEN c\<^isub>1 ELSE c\<^isub>2) = kill c\<^isub>1 \<inter> kill c\<^isub>2" |
+"kill (WHILE b DO c) = {}"
+
+fun gen :: "com \<Rightarrow> name set" where
+"gen SKIP = {}" |
+"gen (x ::= a) = vars a" |
+"gen (c\<^isub>1; c\<^isub>2) = gen c\<^isub>1 \<union> (gen c\<^isub>2 - kill c\<^isub>1)" |
+"gen (IF b THEN c\<^isub>1 ELSE c\<^isub>2) = vars b \<union> gen c\<^isub>1 \<union> gen c\<^isub>2" |
+"gen (WHILE b DO c) = vars b \<union> gen c"
+
+lemma L_gen_kill: "L c X = (X - kill c) \<union> gen c"
+by(induct c arbitrary:X) auto
+
+lemma L_While_subset: "L c (L (WHILE b DO c) X) \<subseteq> L (WHILE b DO c) X"
+by(auto simp add:L_gen_kill)
+
+
+subsection "Soundness"
+
+theorem L_sound:
+  "(c,s) \<Rightarrow> s'  \<Longrightarrow> s = t on L c X \<Longrightarrow>
+  \<exists> t'. (c,t) \<Rightarrow> t' & s' = t' on X"
+proof (induct arbitrary: X t rule: big_step_induct)
+  case Skip then show ?case by auto
+next
+  case Assign then show ?case
+    by (auto simp: ball_Un)
+next
+  case (Semi c1 s1 s2 c2 s3 X t1)
+  from Semi(2,5) obtain t2 where
+    t12: "(c1, t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X"
+    by simp blast
+  from Semi(4)[OF s2t2] obtain t3 where
+    t23: "(c2, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
+    by auto
+  show ?case using t12 t23 s3t3 by auto
+next
+  case (IfTrue b s c1 s' c2)
+  hence "s = t on vars b" "s = t on L c1 X" by auto
+  from  bval_eq_if_eq_on_vars[OF this(1)] IfTrue(1) have "bval b t" by simp
+  from IfTrue(3)[OF `s = t on L c1 X`] obtain t' where
+    "(c1, t) \<Rightarrow> t'" "s' = t' on X" by auto
+  thus ?case using `bval b t` by auto
+next
+  case (IfFalse b s c2 s' c1)
+  hence "s = t on vars b" "s = t on L c2 X" by auto
+  from  bval_eq_if_eq_on_vars[OF this(1)] IfFalse(1) have "~bval b t" by simp
+  from IfFalse(3)[OF `s = t on L c2 X`] obtain t' where
+    "(c2, t) \<Rightarrow> t'" "s' = t' on X" by auto
+  thus ?case using `~bval b t` by auto
+next
+  case (WhileFalse b s c)
+  hence "~ bval b t" by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
+  thus ?case using WhileFalse(2) by auto
+next
+  case (WhileTrue b s1 c s2 s3 X t1)
+  let ?w = "WHILE b DO c"
+  from `bval b s1` WhileTrue(6) have "bval b t1"
+    by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
+  have "s1 = t1 on L c (L ?w X)" using  L_While_subset WhileTrue.prems
+    by (blast)
+  from WhileTrue(3)[OF this] obtain t2 where
+    "(c, t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto
+  from WhileTrue(5)[OF this(2)] obtain t3 where "(?w,t2) \<Rightarrow> t3" "s3 = t3 on X"
+    by auto
+  with `bval b t1` `(c, t1) \<Rightarrow> t2` show ?case by auto
+qed
+
+
+subsection "Program Optimization"
+
+text{* Burying assignments to dead variables: *}
+fun bury :: "com \<Rightarrow> name set \<Rightarrow> com" where
+"bury SKIP X = SKIP" |
+"bury (x ::= a) X = (if x:X then x::= a else SKIP)" |
+"bury (c\<^isub>1; c\<^isub>2) X = (bury c\<^isub>1 (L c\<^isub>2 X); bury c\<^isub>2 X)" |
+"bury (IF b THEN c\<^isub>1 ELSE c\<^isub>2) X = IF b THEN bury c\<^isub>1 X ELSE bury c\<^isub>2 X" |
+"bury (WHILE b DO c) X = WHILE b DO bury c (vars b \<union> X \<union> L c X)"
+
+text{* We could prove the analogous lemma to @{thm[source]L_sound}, and the
+proof would be very similar. However, we phrase it as a semantics
+preservation property: *}
+
+theorem bury_sound:
+  "(c,s) \<Rightarrow> s'  \<Longrightarrow> s = t on L c X \<Longrightarrow>
+  \<exists> t'. (bury c X,t) \<Rightarrow> t' & s' = t' on X"
+proof (induct arbitrary: X t rule: big_step_induct)
+  case Skip then show ?case by auto
+next
+  case Assign then show ?case
+    by (auto simp: ball_Un)
+next
+  case (Semi c1 s1 s2 c2 s3 X t1)
+  from Semi(2,5) obtain t2 where
+    t12: "(bury c1 (L c2 X), t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X"
+    by simp blast
+  from Semi(4)[OF s2t2] obtain t3 where
+    t23: "(bury c2 X, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
+    by auto
+  show ?case using t12 t23 s3t3 by auto
+next
+  case (IfTrue b s c1 s' c2)
+  hence "s = t on vars b" "s = t on L c1 X" by auto
+  from  bval_eq_if_eq_on_vars[OF this(1)] IfTrue(1) have "bval b t" by simp
+  from IfTrue(3)[OF `s = t on L c1 X`] obtain t' where
+    "(bury c1 X, t) \<Rightarrow> t'" "s' =t' on X" by auto
+  thus ?case using `bval b t` by auto
+next
+  case (IfFalse b s c2 s' c1)
+  hence "s = t on vars b" "s = t on L c2 X" by auto
+  from  bval_eq_if_eq_on_vars[OF this(1)] IfFalse(1) have "~bval b t" by simp
+  from IfFalse(3)[OF `s = t on L c2 X`] obtain t' where
+    "(bury c2 X, t) \<Rightarrow> t'" "s' = t' on X" by auto
+  thus ?case using `~bval b t` by auto
+next
+  case (WhileFalse b s c)
+  hence "~ bval b t" by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
+  thus ?case using WhileFalse(2) by auto
+next
+  case (WhileTrue b s1 c s2 s3 X t1)
+  let ?w = "WHILE b DO c"
+  from `bval b s1` WhileTrue(6) have "bval b t1"
+    by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
+  have "s1 = t1 on L c (L ?w X)"
+    using L_While_subset WhileTrue.prems by blast
+  from WhileTrue(3)[OF this] obtain t2 where
+    "(bury c (L ?w X), t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto
+  from WhileTrue(5)[OF this(2)] obtain t3
+    where "(bury ?w X,t2) \<Rightarrow> t3" "s3 = t3 on X"
+    by auto
+  with `bval b t1` `(bury c (L ?w X), t1) \<Rightarrow> t2` show ?case by auto
+    (* FIXME why does s/h fail here? *)
+qed
+
+corollary final_bury_sound: "(c,s) \<Rightarrow> s' \<Longrightarrow> (bury c UNIV,s) \<Rightarrow> s'"
+using bury_sound[of c s s' UNIV]
+by (auto simp: fun_eq_iff[symmetric])
+
+text{* Now the opposite direction. *}
+
+lemma SKIP_bury[simp]:
+  "SKIP = bury c X \<longleftrightarrow> c = SKIP | (EX x a. c = x::=a & x \<notin> X)"
+by (cases c) auto
+
+lemma Assign_bury[simp]: "x::=a = bury c X \<longleftrightarrow> c = x::=a & x : X"
+by (cases c) auto
+
+lemma Semi_bury[simp]: "bc\<^isub>1;bc\<^isub>2 = bury c X \<longleftrightarrow>
+  (EX c\<^isub>1 c\<^isub>2. c = c\<^isub>1;c\<^isub>2 & bc\<^isub>2 = bury c\<^isub>2 X & bc\<^isub>1 = bury c\<^isub>1 (L c\<^isub>2 X))"
+by (cases c) auto
+
+lemma If_bury[simp]: "IF b THEN bc1 ELSE bc2 = bury c X \<longleftrightarrow>
+  (EX c1 c2. c = IF b THEN c1 ELSE c2 &
+     bc1 = bury c1 X & bc2 = bury c2 X)"
+by (cases c) auto
+
+lemma While_bury[simp]: "WHILE b DO bc' = bury c X \<longleftrightarrow>
+  (EX c'. c = WHILE b DO c' & bc' = bury c' (vars b \<union> X \<union> L c X))"
+by (cases c) auto
+
+theorem bury_sound2:
+  "(bury c X,s) \<Rightarrow> s'  \<Longrightarrow> s = t on L c X \<Longrightarrow>
+  \<exists> t'. (c,t) \<Rightarrow> t' & s' = t' on X"
+proof (induct "bury c X" s s' arbitrary: c X t rule: big_step_induct)
+  case Skip then show ?case by auto
+next
+  case Assign then show ?case
+    by (auto simp: ball_Un)
+next
+  case (Semi bc1 s1 s2 bc2 s3 c X t1)
+  then obtain c1 c2 where c: "c = c1;c2"
+    and bc2: "bc2 = bury c2 X" and bc1: "bc1 = bury c1 (L c2 X)" by auto
+  from Semi(2)[OF bc1, of t1] Semi.prems c obtain t2 where
+    t12: "(c1, t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X" by auto
+  from Semi(4)[OF bc2 s2t2] obtain t3 where
+    t23: "(c2, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
+    by auto
+  show ?case using c t12 t23 s3t3 by auto
+next
+  case (IfTrue b s bc1 s' bc2)
+  then obtain c1 c2 where c: "c = IF b THEN c1 ELSE c2"
+    and bc1: "bc1 = bury c1 X" and bc2: "bc2 = bury c2 X" by auto
+  have "s = t on vars b" "s = t on L c1 X" using IfTrue.prems c by auto
+  from bval_eq_if_eq_on_vars[OF this(1)] IfTrue(1) have "bval b t" by simp
+  from IfTrue(3)[OF bc1 `s = t on L c1 X`] obtain t' where
+    "(c1, t) \<Rightarrow> t'" "s' =t' on X" by auto
+  thus ?case using c `bval b t` by auto
+next
+  case (IfFalse b s bc2 s' bc1)
+  then obtain c1 c2 where c: "c = IF b THEN c1 ELSE c2"
+    and bc1: "bc1 = bury c1 X" and bc2: "bc2 = bury c2 X" by auto
+  have "s = t on vars b" "s = t on L c2 X" using IfFalse.prems c by auto
+  from bval_eq_if_eq_on_vars[OF this(1)] IfFalse(1) have "~bval b t" by simp
+  from IfFalse(3)[OF bc2 `s = t on L c2 X`] obtain t' where
+    "(c2, t) \<Rightarrow> t'" "s' =t' on X" by auto
+  thus ?case using c `~bval b t` by auto
+next
+  case (WhileFalse b s c)
+  hence "~ bval b t" by (auto simp: ball_Un dest: bval_eq_if_eq_on_vars)
+  thus ?case using WhileFalse by auto
+next
+  case (WhileTrue b s1 bc' s2 s3 c X t1)
+  then obtain c' where c: "c = WHILE b DO c'"
+    and bc': "bc' = bury c' (vars b \<union> X \<union> L c' X)" by auto
+  let ?w = "WHILE b DO c'"
+  from `bval b s1` WhileTrue.prems c have "bval b t1"
+    by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
+  have "s1 = t1 on L c' (L ?w X)"
+    using L_While_subset WhileTrue.prems c by blast
+  with WhileTrue(3)[OF bc', of t1] obtain t2 where
+    "(c', t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto
+  from WhileTrue(5)[OF WhileTrue(6), of t2] c this(2) obtain t3
+    where "(?w,t2) \<Rightarrow> t3" "s3 = t3 on X"
+    by auto
+  with `bval b t1` `(c', t1) \<Rightarrow> t2` c show ?case by auto
+qed
+
+corollary final_bury_sound2: "(bury c UNIV,s) \<Rightarrow> s' \<Longrightarrow> (c,s) \<Rightarrow> s'"
+using bury_sound2[of c UNIV]
+by (auto simp: fun_eq_iff[symmetric])
+
+corollary bury_iff: "(bury c UNIV,s) \<Rightarrow> s' \<longleftrightarrow> (c,s) \<Rightarrow> s'"
+by(metis final_bury_sound final_bury_sound2)
+
+end
diff -r b505be6f029a -r 686fa0a0696e src/HOL/IMP/OO.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/OO.thy	Mon Jun 06 16:29:38 2011 +0200
@@ -0,0 +1,114 @@
+theory OO imports Main begin
+
+subsection "Towards an OO Language: A Language of Records"
+
+(* FIXME: move to HOL/Fun *)
+abbreviation fun_upd2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c"
+  ("_/'((2_,_ :=/ _)')" [1000,0,0,0] 900)
+where "f(x,y := z) == f(x := (f x)(y := z))"
+
+type_synonym addr = nat
+datatype ref = null | Ref addr
+
+type_synonym obj = "string \<Rightarrow> ref"
+type_synonym venv = "string \<Rightarrow> ref"
+type_synonym store = "addr \<Rightarrow> obj"
+
+datatype exp =
+  Null |
+  New |
+  V string |
+  Faccess exp string       ("_\<bullet>/_" [63,1000] 63) |
+  Vassign string exp       ("(_ ::=/ _)" [1000,61] 62) |
+  Fassign exp string exp   ("(_\<bullet>_ ::=/ _)" [63,0,62] 62) |
+  Mcall exp string exp     ("(_\<bullet>/_<_>)" [63,0,0] 63) |
+  Semi exp exp             ("_;/ _" [61,60] 60) |
+  If bexp exp exp          ("IF _/ THEN (2_)/ ELSE (2_)" [0,0,61] 61)
+and bexp = B bool | Not bexp | And bexp bexp | Eq exp exp
+
+type_synonym menv = "string \<Rightarrow> exp"
+type_synonym config = "venv \<times> store \<times> addr"
+
+inductive
+  big_step :: "menv \<Rightarrow> exp \<times> config \<Rightarrow> ref \<times> config \<Rightarrow> bool"
+    ("(_ \<turnstile>/ (_/ \<Rightarrow> _))" [60,0,60] 55) and
+  bval ::  "menv \<Rightarrow> bexp \<times> config \<Rightarrow> bool \<times> config \<Rightarrow> bool"
+    ("_ \<turnstile> _ \<rightarrow> _" [60,0,60] 55)
+where
+Null:
+"me \<turnstile> (Null,c) \<Rightarrow> (null,c)" |
+New:
+"me \<turnstile> (New,ve,s,n) \<Rightarrow> (Ref n,ve,s(n := (\<lambda>f. null)),n+1)" |
+Vaccess:
+"me \<turnstile> (V x,ve,sn) \<Rightarrow> (ve x,ve,sn)" |
+Faccess:
+"me \<turnstile> (e,c) \<Rightarrow> (Ref a,ve',s',n') \<Longrightarrow>
+ me \<turnstile> (e\<bullet>f,c) \<Rightarrow> (s' a f,ve',s',n')" |
+Vassign:
+"me \<turnstile> (e,c) \<Rightarrow> (r,ve',sn') \<Longrightarrow>
+ me \<turnstile> (x ::= e,c) \<Rightarrow> (r,ve'(x:=r),sn')" |
+Fassign:
+"\<lbrakk> me \<turnstile> (oe,c\<^isub>1) \<Rightarrow> (Ref a,c\<^isub>2);  me \<turnstile> (e,c\<^isub>2) \<Rightarrow> (r,ve\<^isub>3,s\<^isub>3,n\<^isub>3) \<rbrakk> \<Longrightarrow>
+ me \<turnstile> (oe\<bullet>f ::= e,c\<^isub>1) \<Rightarrow> (r,ve\<^isub>3,s\<^isub>3(a,f := r),n\<^isub>3)" |
+Mcall:
+"\<lbrakk> me \<turnstile> (oe,c\<^isub>1) \<Rightarrow> (or,c\<^isub>2);  me \<turnstile> (pe,c\<^isub>2) \<Rightarrow> (pr,ve\<^isub>3,sn\<^isub>3);
+   ve = (\<lambda>x. null)(''this'' := or, ''param'' := pr);
+   me \<turnstile> (me m,ve,sn\<^isub>3) \<Rightarrow> (r,ve',sn\<^isub>4) \<rbrakk>
+  \<Longrightarrow>
+ me \<turnstile> (oe\<bullet>m<pe>,c\<^isub>1) \<Rightarrow> (r,ve\<^isub>3,sn\<^isub>4)" |
+Semi:
+"\<lbrakk> me \<turnstile> (e\<^isub>1,c\<^isub>1) \<Rightarrow> (r,c\<^isub>2);  me \<turnstile> (e\<^isub>2,c\<^isub>2) \<Rightarrow> c\<^isub>3 \<rbrakk> \<Longrightarrow>
+ me \<turnstile> (e\<^isub>1; e\<^isub>2,c\<^isub>1) \<Rightarrow> c\<^isub>3" |
+IfTrue:
+"\<lbrakk> me \<turnstile> (b,c\<^isub>1) \<rightarrow> (True,c\<^isub>2);  me \<turnstile> (e\<^isub>1,c\<^isub>2) \<Rightarrow> c\<^isub>3 \<rbrakk> \<Longrightarrow>
+ me \<turnstile> (IF b THEN e\<^isub>1 ELSE e\<^isub>2,c\<^isub>1) \<Rightarrow> c\<^isub>3" |
+IfFalse:
+"\<lbrakk> me \<turnstile> (b,c\<^isub>1) \<rightarrow> (False,c\<^isub>2);  me \<turnstile> (e\<^isub>2,c\<^isub>2) \<Rightarrow> c\<^isub>3 \<rbrakk> \<Longrightarrow>
+ me \<turnstile> (IF b THEN e\<^isub>1 ELSE e\<^isub>2,c\<^isub>1) \<Rightarrow> c\<^isub>3" |
+
+"me \<turnstile> (B bv,c) \<rightarrow> (bv,c)" |
+
+"me \<turnstile> (b,c\<^isub>1) \<rightarrow> (bv,c\<^isub>2) \<Longrightarrow> me \<turnstile> (Not b,c\<^isub>1) \<rightarrow> (\<not>bv,c\<^isub>2)" |
+
+"\<lbrakk> me \<turnstile> (b\<^isub>1,c\<^isub>1) \<rightarrow> (bv\<^isub>1,c\<^isub>2);  me \<turnstile> (b\<^isub>2,c\<^isub>2) \<rightarrow> (bv\<^isub>2,c\<^isub>3) \<rbrakk> \<Longrightarrow>
+ me \<turnstile> (And b\<^isub>1 b\<^isub>2,c\<^isub>1) \<rightarrow> (bv\<^isub>1\<and>bv\<^isub>2,c\<^isub>3)" |
+
+"\<lbrakk> me \<turnstile> (e\<^isub>1,c\<^isub>1) \<Rightarrow> (r\<^isub>1,c\<^isub>2);  me \<turnstile> (e\<^isub>2,c\<^isub>2) \<Rightarrow> (r\<^isub>2,c\<^isub>3) \<rbrakk> \<Longrightarrow>
+ me \<turnstile> (Eq e\<^isub>1 e\<^isub>2,c\<^isub>1) \<rightarrow> (r\<^isub>1=r\<^isub>2,c\<^isub>3)"
+
+
+code_pred (modes: i => i => o => bool) big_step .
+
+text{* Example: natural numbers encoded as objects with a predecessor
+field. Null is zero. Method succ adds an object in front, method add
+adds as many objects in front as the parameter specifies.
+
+First, the method bodies: *}
+
+definition
+"m_succ  =  (''s'' ::= New)\<bullet>''pred'' ::= V ''this''; V ''s''"
+
+definition "m_add =
+  IF Eq (V ''param'') Null
+  THEN V ''this''
+  ELSE V ''this''\<bullet>''succ''<Null>\<bullet>''add''<V ''param''\<bullet>''pred''>"
+
+text{* The method environment: *}
+definition
+"menv = (\<lambda>m. Null)(''succ'' := m_succ, ''add'' := m_add)"
+
+text{* The main code, adding 1 and 2: *}
+definition "main =
+  ''1'' ::= Null\<bullet>''succ''<Null>;
+  ''2'' ::= V ''1''\<bullet>''succ''<Null>;
+  V ''2'' \<bullet> ''add'' <V ''1''>"
+
+text{* Execution of semantics. The final variable environment and store are
+converted into lists of references based on given lists of variable and field
+names to extract. *}
+
+values
+ "{(r, map ve' [''1'',''2''], map (\<lambda>n. map (s' n)[''pred'']) [0..<n])|
+    r ve' s' n. menv \<turnstile> (main, \<lambda>x. null, nth[], 0) \<Rightarrow> (r,ve',s',n)}"
+
+end
diff -r b505be6f029a -r 686fa0a0696e src/HOL/IMP/Procs.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Procs.thy	Mon Jun 06 16:29:38 2011 +0200
@@ -0,0 +1,27 @@
+header "Extensions and Variations of IMP"
+
+theory Procs imports BExp begin
+
+subsection "Procedures and Local Variables"
+
+datatype
+  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)
+      | Var    name com         ("(1{VAR _;;/ _})")
+      | Proc   name com com     ("(1{PROC _ = _;;/ _})")
+      | CALL   name
+
+definition "test_com =
+{VAR ''x'';;
+ ''x'' ::= N 0;
+ {PROC ''p'' = ''x'' ::= Plus (V ''x'') (V ''x'');;
+  {PROC ''q'' = CALL ''p'';;
+   {VAR ''x'';;
+    ''x'' ::= N 5;
+    {PROC ''p'' = ''x'' ::= Plus (V ''x'') (N 1);;
+     CALL ''q''; ''y'' ::= V ''x''}}}}}"
+
+end
diff -r b505be6f029a -r 686fa0a0696e src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy	Mon Jun 06 16:29:38 2011 +0200
@@ -0,0 +1,40 @@
+theory Procs_Dyn_Vars_Dyn imports Util Procs
+begin
+
+subsubsection "Dynamic Scoping of Procedures and Variables"
+
+type_synonym penv = "name \<Rightarrow> com"
+
+inductive
+  big_step :: "penv \<Rightarrow> com \<times> state \<Rightarrow> state \<Rightarrow> bool" ("_ \<turnstile> _ \<Rightarrow> _" [60,0,60] 55)
+where
+Skip:    "pe \<turnstile> (SKIP,s) \<Rightarrow> s" |
+Assign:  "pe \<turnstile> (x ::= a,s) \<Rightarrow> s(x := aval a s)" |
+Semi:    "\<lbrakk> pe \<turnstile> (c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2;  pe \<turnstile> (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>
+          pe \<turnstile> (c\<^isub>1;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
+
+IfTrue:  "\<lbrakk> bval b s;  pe \<turnstile> (c\<^isub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
+         pe \<turnstile> (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
+IfFalse: "\<lbrakk> \<not>bval b s;  pe \<turnstile> (c\<^isub>2,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
+         pe \<turnstile> (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
+
+WhileFalse: "\<not>bval b s \<Longrightarrow> pe \<turnstile> (WHILE b DO c,s) \<Rightarrow> s" |
+WhileTrue:
+  "\<lbrakk> bval b s\<^isub>1;  pe \<turnstile> (c,s\<^isub>1) \<Rightarrow> s\<^isub>2;  pe \<turnstile> (WHILE b DO c, s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>
+   pe \<turnstile> (WHILE b DO c, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
+
+Var: "pe \<turnstile> (c,s) \<Rightarrow> t  \<Longrightarrow>  pe \<turnstile> ({VAR x;; c}, s) \<Rightarrow> t(x := s x)" |
+
+Call: "pe \<turnstile> (pe p, s) \<Rightarrow> t  \<Longrightarrow>  pe \<turnstile> (CALL p, s) \<Rightarrow> t" |
+
+Proc: "pe(p := cp) \<turnstile> (c,s) \<Rightarrow> t  \<Longrightarrow>  pe \<turnstile> ({PROC p = cp;; c}, s) \<Rightarrow> t"
+
+code_pred big_step .
+
+(* FIXME: example state syntax *)
+values "{map t [''x'',''y'',''z''] |t. 
+          (\<lambda>p. SKIP) \<turnstile> (CALL ''p'', (%_. 0)(''x'' := 42, ''y'' := 43)) \<Rightarrow> t}"
+
+values "{map t [''x'',''y'',''z''] |t. (\<lambda>p. SKIP) \<turnstile> (test_com, (%_. 0)) \<Rightarrow> t}"
+
+end
diff -r b505be6f029a -r 686fa0a0696e src/HOL/IMP/Procs_Stat_Vars_Dyn.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Procs_Stat_Vars_Dyn.thy	Mon Jun 06 16:29:38 2011 +0200
@@ -0,0 +1,43 @@
+theory Procs_Stat_Vars_Dyn imports Util Procs
+begin
+
+subsubsection "Static Scoping of Procedures, Dynamic of Variables"
+
+type_synonym penv = "(name \<times> com) list"
+
+inductive
+  big_step :: "penv \<Rightarrow> com \<times> state \<Rightarrow> state \<Rightarrow> bool" ("_ \<turnstile> _ \<Rightarrow> _" [60,0,60] 55)
+where
+Skip:    "pe \<turnstile> (SKIP,s) \<Rightarrow> s" |
+Assign:  "pe \<turnstile> (x ::= a,s) \<Rightarrow> s(x := aval a s)" |
+Semi:    "\<lbrakk> pe \<turnstile> (c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2;  pe \<turnstile> (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>
+          pe \<turnstile> (c\<^isub>1;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
+
+IfTrue:  "\<lbrakk> bval b s;  pe \<turnstile> (c\<^isub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
+         pe \<turnstile> (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
+IfFalse: "\<lbrakk> \<not>bval b s;  pe \<turnstile> (c\<^isub>2,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
+         pe \<turnstile> (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
+
+WhileFalse: "\<not>bval b s \<Longrightarrow> pe \<turnstile> (WHILE b DO c,s) \<Rightarrow> s" |
+WhileTrue:
+  "\<lbrakk> bval b s\<^isub>1;  pe \<turnstile> (c,s\<^isub>1) \<Rightarrow> s\<^isub>2;  pe \<turnstile> (WHILE b DO c, s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>
+   pe \<turnstile> (WHILE b DO c, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
+
+Var: "pe \<turnstile> (c,s) \<Rightarrow> t  \<Longrightarrow>  pe \<turnstile> ({VAR x;; c}, s) \<Rightarrow> t(x := s x)" |
+
+Call1: "(p,c)#pe \<turnstile> (c, s) \<Rightarrow> t  \<Longrightarrow>  (p,c)#pe \<turnstile> (CALL p, s) \<Rightarrow> t" |
+Call2: "\<lbrakk> p' \<noteq> p;  pe \<turnstile> (CALL p, s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
+       (p',c)#pe \<turnstile> (CALL p, s) \<Rightarrow> t" |
+
+Proc: "(p,cp)#pe \<turnstile> (c,s) \<Rightarrow> t  \<Longrightarrow>  pe \<turnstile> ({PROC p = cp;; c}, s) \<Rightarrow> t"
+
+code_pred big_step .
+
+
+(* FIXME: example state syntax *)
+values "{map t [''x'', ''y'', ''z''] |t. 
+            [] \<turnstile> (CALL ''p'', (%_. 0)(''x'' := 42, ''y'' := 43)) \<Rightarrow> t}"
+
+values "{map t [''x'', ''y'', ''z''] |t. [] \<turnstile> (test_com, (%_. 0) ) \<Rightarrow> t}"
+
+end
diff -r b505be6f029a -r 686fa0a0696e src/HOL/IMP/Procs_Stat_Vars_Stat.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Procs_Stat_Vars_Stat.thy	Mon Jun 06 16:29:38 2011 +0200
@@ -0,0 +1,53 @@
+theory Procs_Stat_Vars_Stat imports Util Procs
+begin
+
+subsubsection "Static Scoping of Procedures and Variables"
+
+type_synonym addr = nat
+type_synonym venv = "name \<Rightarrow> addr"
+type_synonym store = "addr \<Rightarrow> val"
+type_synonym penv = "(name \<times> com \<times> venv) list"
+
+fun venv :: "penv \<times> venv \<times> nat \<Rightarrow> venv" where
+"venv(_,ve,_) = ve"
+
+inductive
+  big_step :: "penv \<times> venv \<times> nat \<Rightarrow> com \<times> store \<Rightarrow> store \<Rightarrow> bool"
+  ("_ \<turnstile> _ \<Rightarrow> _" [60,0,60] 55)
+where
+Skip:    "e \<turnstile> (SKIP,s) \<Rightarrow> s" |
+Assign:  "(pe,ve,f) \<turnstile> (x ::= a,s) \<Rightarrow> s(ve x := aval a (s o ve))" |
+Semi:    "\<lbrakk> e \<turnstile> (c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2;  e \<turnstile> (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>
+          e \<turnstile> (c\<^isub>1;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
+
+IfTrue:  "\<lbrakk> bval b (s \<circ> venv e);  e \<turnstile> (c\<^isub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
+         e \<turnstile> (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
+IfFalse: "\<lbrakk> \<not>bval b (s \<circ> venv e);  e \<turnstile> (c\<^isub>2,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
+         e \<turnstile> (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
+
+WhileFalse: "\<not>bval b (s \<circ> venv e) \<Longrightarrow> e \<turnstile> (WHILE b DO c,s) \<Rightarrow> s" |
+WhileTrue:
+  "\<lbrakk> bval b (s\<^isub>1 \<circ> venv e);  e \<turnstile> (c,s\<^isub>1) \<Rightarrow> s\<^isub>2;
+     e \<turnstile> (WHILE b DO c, s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>
+   e \<turnstile> (WHILE b DO c, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
+
+Var: "(pe,ve(x:=f),f+1) \<turnstile> (c,s) \<Rightarrow> t  \<Longrightarrow>
+      (pe,ve,f) \<turnstile> ({VAR x;; c}, s) \<Rightarrow> t(f := s f)" |
+
+Call1: "((p,c,ve)#pe,ve,f) \<turnstile> (c, s) \<Rightarrow> t  \<Longrightarrow>
+        ((p,c,ve)#pe,ve',f) \<turnstile> (CALL p, s) \<Rightarrow> t" |
+Call2: "\<lbrakk> p' \<noteq> p;  (pe,ve,f) \<turnstile> (CALL p, s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
+       ((p',c,ve')#pe,ve,f) \<turnstile> (CALL p, s) \<Rightarrow> t" |
+
+Proc: "((p,cp,ve)#pe,ve,f) \<turnstile> (c,s) \<Rightarrow> t
+      \<Longrightarrow>  (pe,ve,f) \<turnstile> ({PROC p = cp;; c}, s) \<Rightarrow> t"
+
+code_pred big_step .
+
+values "{map t [0,1] |t. ([], \<lambda>n. 0, 0) \<turnstile> (CALL ''p'', nth [42, 43]) \<Rightarrow> t}"
+
+(* FIXME: syntax *)
+values "{map t [0, 1, 2] |t. ([], (\<lambda>_. 3)(''x'' := 0, ''y'' := 1,''z'' := 2), 0) \<turnstile> (test_com, (%_. 0)) \<Rightarrow> t}"
+
+
+end
diff -r b505be6f029a -r 686fa0a0696e src/HOL/IMP/ROOT.ML
--- a/src/HOL/IMP/ROOT.ML	Mon Jun 06 16:29:13 2011 +0200
+++ b/src/HOL/IMP/ROOT.ML	Mon Jun 06 16:29:38 2011 +0200
@@ -4,13 +4,11 @@
  "Small_Step",
  "Denotation",
  "Compiler",
- "Poly_Types"(*,
+ "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",
@@ -20,5 +18,4 @@
  "Procs_Stat_Vars_Stat",
  "C_like",
  "OO"
-*)
 ];
diff -r b505be6f029a -r 686fa0a0696e src/HOL/IMP/Sec_Type_Expr.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Sec_Type_Expr.thy	Mon Jun 06 16:29:38 2011 +0200
@@ -0,0 +1,45 @@
+header "Security Type Systems"
+
+theory Sec_Type_Expr imports Big_Step
+begin
+
+subsection "Security Levels and Expressions"
+
+type_synonym level = nat
+
+text{* The security/confidentiality level of each variable is globally fixed
+for simplicity. For the sake of examples --- the general theory does not rely
+on it! --- a variable of length @{text n} has security level @{text n}: *}
+
+definition sec :: "name \<Rightarrow> level" where 
+  "sec n = size n"
+
+fun sec_aexp :: "aexp \<Rightarrow> level" where
+"sec_aexp (N n) = 0" |
+"sec_aexp (V x) = sec x" |
+"sec_aexp (Plus a\<^isub>1 a\<^isub>2) = max (sec_aexp a\<^isub>1) (sec_aexp a\<^isub>2)"
+
+fun sec_bexp :: "bexp \<Rightarrow> level" where
+"sec_bexp (B bv) = 0" |
+"sec_bexp (Not b) = sec_bexp b" |
+"sec_bexp (And b\<^isub>1 b\<^isub>2) = max (sec_bexp b\<^isub>1) (sec_bexp b\<^isub>2)" |
+"sec_bexp (Less a\<^isub>1 a\<^isub>2) = max (sec_aexp a\<^isub>1) (sec_aexp a\<^isub>2)"
+
+
+abbreviation eq_le :: "state \<Rightarrow> state \<Rightarrow> level \<Rightarrow> bool"
+  ("(_ = _ '(\<le> _'))" [51,51,0] 50) where
+"s = s' (\<le> l) == (\<forall> x. sec x \<le> l \<longrightarrow> s x = s' x)"
+
+abbreviation eq_less :: "state \<Rightarrow> state \<Rightarrow> level \<Rightarrow> bool"
+  ("(_ = _ '(< _'))" [51,51,0] 50) where
+"s = s' (< l) == (\<forall> x. sec x < l \<longrightarrow> s x = s' x)"
+
+lemma aval_eq_if_eq_le:
+  "\<lbrakk> s\<^isub>1 = s\<^isub>2 (\<le> l);  sec_aexp a \<le> l \<rbrakk> \<Longrightarrow> aval a s\<^isub>1 = aval a s\<^isub>2"
+by (induct a) auto
+
+lemma bval_eq_if_eq_le:
+  "\<lbrakk> s\<^isub>1 = s\<^isub>2 (\<le> l);  sec_bexp b \<le> l \<rbrakk> \<Longrightarrow> bval b s\<^isub>1 = bval b s\<^isub>2"
+by (induct b) (auto simp add: aval_eq_if_eq_le)
+
+end
diff -r b505be6f029a -r 686fa0a0696e src/HOL/IMP/Sec_Typing.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Sec_Typing.thy	Mon Jun 06 16:29:38 2011 +0200
@@ -0,0 +1,249 @@
+(* Author: Tobias Nipkow *)
+
+theory Sec_Typing imports Sec_Type_Expr
+begin
+
+subsection "Syntax Directed Typing"
+
+inductive sec_type :: "nat \<Rightarrow> com \<Rightarrow> bool" ("(_/ \<turnstile> _)" [0,0] 50) where
+Skip:
+  "l \<turnstile> SKIP" |
+Assign:
+  "\<lbrakk> sec x \<ge> sec_aexp a;  sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile> x ::= a" |
+Semi:
+  "\<lbrakk> l \<turnstile> c\<^isub>1;  l \<turnstile> c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile> c\<^isub>1;c\<^isub>2" |
+If:
+  "\<lbrakk> max (sec_bexp b) l \<turnstile> c\<^isub>1;  max (sec_bexp b) l \<turnstile> c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2" |
+While:
+  "max (sec_bexp b) l \<turnstile> c \<Longrightarrow> l \<turnstile> WHILE b DO c"
+
+code_pred (expected_modes: i => i => bool) sec_type .
+
+value "0 \<turnstile> IF Less (V ''x1'') (V ''x'') THEN ''x1'' ::= N 0 ELSE SKIP"
+value "1 \<turnstile> IF Less (V ''x1'') (V ''x'') THEN ''x''  ::= N 0 ELSE SKIP"
+value "2 \<turnstile> IF Less (V ''x1'') (V ''x'') THEN ''x1'' ::= N 0 ELSE SKIP"
+
+inductive_cases [elim!]:
+  "l \<turnstile> x ::= a"  "l \<turnstile> c\<^isub>1;c\<^isub>2"  "l \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2"  "l \<turnstile> WHILE b DO c"
+
+
+text{* An important property: anti-monotonicity. *}
+
+lemma anti_mono: "\<lbrakk> l \<turnstile> c;  l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile> c"
+apply(induct arbitrary: l' rule: sec_type.induct)
+apply (metis sec_type.intros(1))
+apply (metis le_trans sec_type.intros(2))
+apply (metis sec_type.intros(3))
+apply (metis If le_refl sup_mono sup_nat_def)
+apply (metis While le_refl sup_mono sup_nat_def)
+done
+
+lemma confinement: "\<lbrakk> (c,s) \<Rightarrow> t;  l \<turnstile> c \<rbrakk> \<Longrightarrow> s = t (< l)"
+proof(induct rule: big_step_induct)
+  case Skip thus ?case by simp
+next
+  case Assign thus ?case by auto
+next
+  case Semi thus ?case by auto
+next
+  case (IfTrue b s c1)
+  hence "max (sec_bexp b) l \<turnstile> c1" by auto
+  hence "l \<turnstile> c1" by (metis le_maxI2 anti_mono)
+  thus ?case using IfTrue.hyps by metis
+next
+  case (IfFalse b s c2)
+  hence "max (sec_bexp b) l \<turnstile> c2" by auto
+  hence "l \<turnstile> c2" by (metis le_maxI2 anti_mono)
+  thus ?case using IfFalse.hyps by metis
+next
+  case WhileFalse thus ?case by auto
+next
+  case (WhileTrue b s1 c)
+  hence "max (sec_bexp b) l \<turnstile> c" by auto
+  hence "l \<turnstile> c" by (metis le_maxI2 anti_mono)
+  thus ?case using WhileTrue by metis
+qed
+
+
+theorem noninterference:
+  "\<lbrakk> (c,s) \<Rightarrow> s'; (c,t) \<Rightarrow> t';  0 \<turnstile> c;  s = t (\<le> l) \<rbrakk>
+   \<Longrightarrow> s' = t' (\<le> l)"
+proof(induct arbitrary: t t' rule: big_step_induct)
+  case Skip thus ?case by auto
+next
+  case (Assign x a s)
+  have [simp]: "t' = t(x := aval a t)" using Assign by auto
+  have "sec x >= sec_aexp a" using `0 \<turnstile> x ::= a` by auto
+  show ?case
+  proof auto
+    assume "sec x \<le> l"
+    with `sec x >= sec_aexp a` have "sec_aexp a \<le> l" by arith
+    thus "aval a s = aval a t"
+      by (rule aval_eq_if_eq_le[OF `s = t (\<le> l)`])
+  next
+    fix y assume "y \<noteq> x" "sec y \<le> l"
+    thus "s y = t y" using `s = t (\<le> l)` by simp
+  qed
+next
+  case Semi thus ?case by blast
+next
+  case (IfTrue b s c1 s' c2)
+  have "sec_bexp b \<turnstile> c1" "sec_bexp b \<turnstile> c2" using IfTrue.prems(2) by auto
+  show ?case
+  proof cases
+    assume "sec_bexp b \<le> l"
+    hence "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto
+    hence "bval b t" using `bval b s` by(simp add: bval_eq_if_eq_le)
+    with IfTrue.hyps(3) IfTrue.prems(1,3) `sec_bexp b \<turnstile> c1`  anti_mono
+    show ?thesis by auto
+  next
+    assume "\<not> sec_bexp b \<le> l"
+    have 1: "sec_bexp b \<turnstile> IF b THEN c1 ELSE c2"
+      by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c1` `sec_bexp b \<turnstile> c2`)
+    from confinement[OF big_step.IfTrue[OF IfTrue(1,2)] 1] `\<not> sec_bexp b \<le> l`
+    have "s = s' (\<le> l)" by auto
+    moreover
+    from confinement[OF IfTrue.prems(1) 1] `\<not> sec_bexp b \<le> l`
+    have "t = t' (\<le> l)" by auto
+    ultimately show "s' = t' (\<le> l)" using `s = t (\<le> l)` by auto
+  qed
+next
+  case (IfFalse b s c2 s' c1)
+  have "sec_bexp b \<turnstile> c1" "sec_bexp b \<turnstile> c2" using IfFalse.prems(2) by auto
+  show ?case
+  proof cases
+    assume "sec_bexp b \<le> l"
+    hence "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto
+    hence "\<not> bval b t" using `\<not> bval b s` by(simp add: bval_eq_if_eq_le)
+    with IfFalse.hyps(3) IfFalse.prems(1,3) `sec_bexp b \<turnstile> c2` anti_mono
+    show ?thesis by auto
+  next
+    assume "\<not> sec_bexp b \<le> l"
+    have 1: "sec_bexp b \<turnstile> IF b THEN c1 ELSE c2"
+      by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c1` `sec_bexp b \<turnstile> c2`)
+    from confinement[OF big_step.IfFalse[OF IfFalse(1,2)] 1] `\<not> sec_bexp b \<le> l`
+    have "s = s' (\<le> l)" by auto
+    moreover
+    from confinement[OF IfFalse.prems(1) 1] `\<not> sec_bexp b \<le> l`
+    have "t = t' (\<le> l)" by auto
+    ultimately show "s' = t' (\<le> l)" using `s = t (\<le> l)` by auto
+  qed
+next
+  case (WhileFalse b s c)
+  have "sec_bexp b \<turnstile> c" using WhileFalse.prems(2) by auto
+  show ?case
+  proof cases
+    assume "sec_bexp b \<le> l"
+    hence "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto
+    hence "\<not> bval b t" using `\<not> bval b s` by(simp add: bval_eq_if_eq_le)
+    with WhileFalse.prems(1,3) show ?thesis by auto
+  next
+    assume "\<not> sec_bexp b \<le> l"
+    have 1: "sec_bexp b \<turnstile> WHILE b DO c"
+      by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c`)
+    from confinement[OF WhileFalse.prems(1) 1] `\<not> sec_bexp b \<le> l`
+    have "t = t' (\<le> l)" by auto
+    thus "s = t' (\<le> l)" using `s = t (\<le> l)` by auto
+  qed
+next
+  case (WhileTrue b s1 c s2 s3 t1 t3)
+  let ?w = "WHILE b DO c"
+  have "sec_bexp b \<turnstile> c" using WhileTrue.prems(2) by auto
+  show ?case
+  proof cases
+    assume "sec_bexp b \<le> l"
+    hence "s1 = t1 (\<le> sec_bexp b)" using `s1 = t1 (\<le> l)` by auto
+    hence "bval b t1"
+      using `bval b s1` by(simp add: bval_eq_if_eq_le)
+    then obtain t2 where "(c,t1) \<Rightarrow> t2" "(?w,t2) \<Rightarrow> t3"
+      using `(?w,t1) \<Rightarrow> t3` by auto
+    from WhileTrue.hyps(5)[OF `(?w,t2) \<Rightarrow> t3` `0 \<turnstile> ?w`
+      WhileTrue.hyps(3)[OF `(c,t1) \<Rightarrow> t2` anti_mono[OF `sec_bexp b \<turnstile> c`]
+        `s1 = t1 (\<le> l)`]]
+    show ?thesis by simp
+  next
+    assume "\<not> sec_bexp b \<le> l"
+    have 1: "sec_bexp b \<turnstile> ?w" by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c`)
+    from confinement[OF big_step.WhileTrue[OF WhileTrue(1,2,4)] 1] `\<not> sec_bexp b \<le> l`
+    have "s1 = s3 (\<le> l)" by auto
+    moreover
+    from confinement[OF WhileTrue.prems(1) 1] `\<not> sec_bexp b \<le> l`
+    have "t1 = t3 (\<le> l)" by auto
+    ultimately show "s3 = t3 (\<le> l)" using `s1 = t1 (\<le> l)` by auto
+  qed
+qed
+
+
+subsection "The Standard Typing System"
+
+text{* The predicate @{prop"l \<turnstile> c"} is nicely intuitive and executable. The
+standard formulation, however, is slightly different, replacing the maximum
+computation by an antimonotonicity rule. We introduce the standard system now
+and show the equivalence with our formulation. *}
+
+inductive sec_type' :: "nat \<Rightarrow> com \<Rightarrow> bool" ("(_/ \<turnstile>'' _)" [0,0] 50) where
+Skip':
+  "l \<turnstile>' SKIP" |
+Assign':
+  "\<lbrakk> sec x \<ge> sec_aexp a; sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile>' x ::= a" |
+Semi':
+  "\<lbrakk> l \<turnstile>' c\<^isub>1;  l \<turnstile>' c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile>' c\<^isub>1;c\<^isub>2" |
+If':
+  "\<lbrakk> sec_bexp b \<le> l;  l \<turnstile>' c\<^isub>1;  l \<turnstile>' c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile>' IF b THEN c\<^isub>1 ELSE c\<^isub>2" |
+While':
+  "\<lbrakk> sec_bexp b \<le> l;  l \<turnstile>' c \<rbrakk> \<Longrightarrow> l \<turnstile>' WHILE b DO c" |
+anti_mono':
+  "\<lbrakk> l \<turnstile>' c;  l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile>' c"
+
+lemma sec_type_sec_type': "l \<turnstile> c \<Longrightarrow> l \<turnstile>' c"
+apply(induct rule: sec_type.induct)
+apply (metis Skip')
+apply (metis Assign')
+apply (metis Semi')
+apply (metis min_max.inf_sup_ord(3) min_max.sup_absorb2 nat_le_linear If' anti_mono')
+by (metis less_or_eq_imp_le min_max.sup_absorb1 min_max.sup_absorb2 nat_le_linear While' anti_mono')
+
+
+lemma sec_type'_sec_type: "l \<turnstile>' c \<Longrightarrow> l \<turnstile> c"
+apply(induct rule: sec_type'.induct)
+apply (metis Skip)
+apply (metis Assign)
+apply (metis Semi)
+apply (metis min_max.sup_absorb2 If)
+apply (metis min_max.sup_absorb2 While)
+by (metis anti_mono)
+
+subsection "A Bottom-Up Typing System"
+
+inductive sec_type2 :: "com \<Rightarrow> level \<Rightarrow> bool" ("(\<turnstile> _ : _)" [0,0] 50) where
+Skip2:
+  "\<turnstile> SKIP : l" |
+Assign2:
+  "sec x \<ge> sec_aexp a \<Longrightarrow> \<turnstile> x ::= a : sec x" |
+Semi2:
+  "\<lbrakk> \<turnstile> c\<^isub>1 : l\<^isub>1;  \<turnstile> c\<^isub>2 : l\<^isub>2 \<rbrakk> \<Longrightarrow> \<turnstile> c\<^isub>1;c\<^isub>2 : min l\<^isub>1 l\<^isub>2 " |
+If2:
+  "\<lbrakk> sec_bexp b \<le> min l\<^isub>1 l\<^isub>2;  \<turnstile> c\<^isub>1 : l\<^isub>1;  \<turnstile> c\<^isub>2 : l\<^isub>2 \<rbrakk>
+  \<Longrightarrow> \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2 : min l\<^isub>1 l\<^isub>2" |
+While2:
+  "\<lbrakk> sec_bexp b \<le> l;  \<turnstile> c : l \<rbrakk> \<Longrightarrow> \<turnstile> WHILE b DO c : l"
+
+
+lemma sec_type2_sec_type': "\<turnstile> c : l \<Longrightarrow> l \<turnstile>' c"
+apply(induct rule: sec_type2.induct)
+apply (metis Skip')
+apply (metis Assign' eq_imp_le)
+apply (metis Semi' anti_mono' min_max.inf.commute min_max.inf_le2)
+apply (metis If' anti_mono' min_max.inf_absorb2 min_max.le_iff_inf nat_le_linear)
+by (metis While')
+
+lemma sec_type'_sec_type2: "l \<turnstile>' c \<Longrightarrow> \<exists> l' \<ge> l. \<turnstile> c : l'"
+apply(induct rule: sec_type'.induct)
+apply (metis Skip2 le_refl)
+apply (metis Assign2)
+apply (metis Semi2 min_max.inf_greatest)
+apply (metis If2 inf_greatest inf_nat_def le_trans)
+apply (metis While2 le_trans)
+by (metis le_trans)
+
+end
diff -r b505be6f029a -r 686fa0a0696e src/HOL/IMP/Sec_TypingT.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Sec_TypingT.thy	Mon Jun 06 16:29:38 2011 +0200
@@ -0,0 +1,205 @@
+theory Sec_TypingT imports Sec_Type_Expr
+begin
+
+subsection "A Termination-Sensitive Syntax Directed System"
+
+inductive sec_type :: "nat \<Rightarrow> com \<Rightarrow> bool" ("(_/ \<turnstile> _)" [0,0] 50) where
+Skip:
+  "l \<turnstile> SKIP"  |
+Assign:
+  "\<lbrakk> sec x \<ge> sec_aexp a;  sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile> x ::= a"  |
+Semi:
+  "l \<turnstile> c\<^isub>1 \<Longrightarrow> l \<turnstile> c\<^isub>2 \<Longrightarrow> l \<turnstile> c\<^isub>1;c\<^isub>2"  |
+If:
+  "\<lbrakk> max (sec_bexp b) l \<turnstile> c\<^isub>1;  max (sec_bexp b) l \<turnstile> c\<^isub>2 \<rbrakk>
+   \<Longrightarrow> l \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2"  |
+While:
+  "sec_bexp b = 0 \<Longrightarrow> 0 \<turnstile> c \<Longrightarrow> 0 \<turnstile> WHILE b DO c"
+
+code_pred (expected_modes: i => i => bool) sec_type .
+
+inductive_cases [elim!]:
+  "l \<turnstile> x ::= a"  "l \<turnstile> c\<^isub>1;c\<^isub>2"  "l \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2"  "l \<turnstile> WHILE b DO c"
+
+
+lemma anti_mono: "l \<turnstile> c \<Longrightarrow> l' \<le> l \<Longrightarrow> l' \<turnstile> c"
+apply(induct arbitrary: l' rule: sec_type.induct)
+apply (metis sec_type.intros(1))
+apply (metis le_trans sec_type.intros(2))
+apply (metis sec_type.intros(3))
+apply (metis If le_refl sup_mono sup_nat_def)
+by (metis While le_0_eq)
+
+
+lemma confinement: "(c,s) \<Rightarrow> t \<Longrightarrow> l \<turnstile> c \<Longrightarrow> s = t (< l)"
+proof(induct rule: big_step_induct)
+  case Skip thus ?case by simp
+next
+  case Assign thus ?case by auto
+next
+  case Semi thus ?case by auto
+next
+  case (IfTrue b s c1)
+  hence "max (sec_bexp b) l \<turnstile> c1" by auto
+  hence "l \<turnstile> c1" by (metis le_maxI2 anti_mono)
+  thus ?case using IfTrue.hyps by metis
+next
+  case (IfFalse b s c2)
+  hence "max (sec_bexp b) l \<turnstile> c2" by auto
+  hence "l \<turnstile> c2" by (metis le_maxI2 anti_mono)
+  thus ?case using IfFalse.hyps by metis
+next
+  case WhileFalse thus ?case by auto
+next
+  case (WhileTrue b s1 c)
+  hence "l \<turnstile> c" by auto
+  thus ?case using WhileTrue by metis
+qed
+
+lemma termi_if_non0: "l \<turnstile> c \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> \<exists> t. (c,s) \<Rightarrow> t"
+apply(induct arbitrary: s rule: sec_type.induct)
+apply (metis big_step.Skip)
+apply (metis big_step.Assign)
+apply (metis big_step.Semi)
+apply (metis IfFalse IfTrue le0 le_antisym le_maxI2)
+apply simp
+done
+
+theorem noninterference: "(c,s) \<Rightarrow> s' \<Longrightarrow> 0 \<turnstile> c \<Longrightarrow>  s = t (\<le> l)
+  \<Longrightarrow> \<exists> t'. (c,t) \<Rightarrow> t' \<and> s' = t' (\<le> l)"
+proof(induct arbitrary: t rule: big_step_induct)
+  case Skip thus ?case by auto
+next
+  case (Assign x a s)
+  have "sec x >= sec_aexp a" using `0 \<turnstile> x ::= a` by auto
+  have "(x ::= a,t) \<Rightarrow> t(x := aval a t)" by auto
+  moreover
+  have "s(x := aval a s) = t(x := aval a t) (\<le> l)"
+  proof auto
+    assume "sec x \<le> l"
+    with `sec x \<ge> sec_aexp a` have "sec_aexp a \<le> l" by arith
+    thus "aval a s = aval a t"
+      by (rule aval_eq_if_eq_le[OF `s = t (\<le> l)`])
+  next
+    fix y assume "y \<noteq> x" "sec y \<le> l"
+    thus "s y = t y" using `s = t (\<le> l)` by simp
+  qed
+  ultimately show ?case by blast
+next
+  case Semi thus ?case by blast
+next
+  case (IfTrue b s c1 s' c2)
+  have "sec_bexp b \<turnstile> c1" "sec_bexp b \<turnstile> c2" using IfTrue.prems by auto
+  obtain t' where t': "(c1, t) \<Rightarrow> t'" "s' = t' (\<le> l)"
+    using IfTrue(3)[OF anti_mono[OF `sec_bexp b \<turnstile> c1`] IfTrue.prems(2)] by blast
+  show ?case
+  proof cases
+    assume "sec_bexp b \<le> l"
+    hence "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto
+    hence "bval b t" using `bval b s` by(simp add: bval_eq_if_eq_le)
+    thus ?thesis by (metis t' big_step.IfTrue)
+  next
+    assume "\<not> sec_bexp b \<le> l"
+    hence 0: "sec_bexp b \<noteq> 0" by arith
+    have 1: "sec_bexp b \<turnstile> IF b THEN c1 ELSE c2"
+      by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c1` `sec_bexp b \<turnstile> c2`)
+    from confinement[OF big_step.IfTrue[OF IfTrue(1,2)] 1] `\<not> sec_bexp b \<le> l`
+    have "s = s' (\<le> l)" by auto
+    moreover
+    from termi_if_non0[OF 1 0, of t] obtain t' where
+      "(IF b THEN c1 ELSE c2,t) \<Rightarrow> t'" ..
+    moreover
+    from confinement[OF this 1] `\<not> sec_bexp b \<le> l`
+    have "t = t' (\<le> l)" by auto
+    ultimately
+    show ?case using `s = t (\<le> l)` by auto
+  qed
+next
+  case (IfFalse b s c2 s' c1)
+  have "sec_bexp b \<turnstile> c1" "sec_bexp b \<turnstile> c2" using IfFalse.prems by auto
+  obtain t' where t': "(c2, t) \<Rightarrow> t'" "s' = t' (\<le> l)"
+    using IfFalse(3)[OF anti_mono[OF `sec_bexp b \<turnstile> c2`] IfFalse.prems(2)] by blast
+  show ?case
+  proof cases
+    assume "sec_bexp b \<le> l"
+    hence "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto
+    hence "\<not> bval b t" using `\<not> bval b s` by(simp add: bval_eq_if_eq_le)
+    thus ?thesis by (metis t' big_step.IfFalse)
+  next
+    assume "\<not> sec_bexp b \<le> l"
+    hence 0: "sec_bexp b \<noteq> 0" by arith
+    have 1: "sec_bexp b \<turnstile> IF b THEN c1 ELSE c2"
+      by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c1` `sec_bexp b \<turnstile> c2`)
+    from confinement[OF big_step.IfFalse[OF IfFalse(1,2)] 1] `\<not> sec_bexp b \<le> l`
+    have "s = s' (\<le> l)" by auto
+    moreover
+    from termi_if_non0[OF 1 0, of t] obtain t' where
+      "(IF b THEN c1 ELSE c2,t) \<Rightarrow> t'" ..
+    moreover
+    from confinement[OF this 1] `\<not> sec_bexp b \<le> l`
+    have "t = t' (\<le> l)" by auto
+    ultimately
+    show ?case using `s = t (\<le> l)` by auto
+  qed
+next
+  case (WhileFalse b s c)
+  hence [simp]: "sec_bexp b = 0" by auto
+  have "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto
+  hence "\<not> bval b t" using `\<not> bval b s` by (metis bval_eq_if_eq_le le_refl)
+  with WhileFalse.prems(2) show ?case by auto
+next
+  case (WhileTrue b s c s'' s')
+  let ?w = "WHILE b DO c"
+  from `0 \<turnstile> ?w` have [simp]: "sec_bexp b = 0" by auto
+  have "0 \<turnstile> c" using WhileTrue.prems(1) by auto
+  from WhileTrue(3)[OF this WhileTrue.prems(2)]
+  obtain t'' where "(c,t) \<Rightarrow> t''" and "s'' = t'' (\<le>l)" by blast
+  from WhileTrue(5)[OF `0 \<turnstile> ?w` this(2)]
+  obtain t' where "(?w,t'') \<Rightarrow> t'" and "s' = t' (\<le>l)" by blast
+  from `bval b s` have "bval b t"
+    using bval_eq_if_eq_le[OF `s = t (\<le>l)`] by auto
+  show ?case
+    using big_step.WhileTrue[OF `bval b t` `(c,t) \<Rightarrow> t''` `(?w,t'') \<Rightarrow> t'`]
+    by (metis `s' = t' (\<le> l)`)
+qed
+
+subsection "The Standard Termination-Sensitive System"
+
+text{* The predicate @{prop"l \<turnstile> c"} is nicely intuitive and executable. The
+standard formulation, however, is slightly different, replacing the maximum
+computation by an antimonotonicity rule. We introduce the standard system now
+and show the equivalence with our formulation. *}
+
+inductive sec_type' :: "nat \<Rightarrow> com \<Rightarrow> bool" ("(_/ \<turnstile>'' _)" [0,0] 50) where
+Skip':
+  "l \<turnstile>' SKIP"  |
+Assign':
+  "\<lbrakk> sec x \<ge> sec_aexp a;  sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile>' x ::= a"  |
+Semi':
+  "l \<turnstile>' c\<^isub>1 \<Longrightarrow> l \<turnstile>' c\<^isub>2 \<Longrightarrow> l \<turnstile>' c\<^isub>1;c\<^isub>2"  |
+If':
+  "\<lbrakk> sec_bexp b \<le> l;  l \<turnstile>' c\<^isub>1;  l \<turnstile>' c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile>' IF b THEN c\<^isub>1 ELSE c\<^isub>2"  |
+While':
+  "\<lbrakk> sec_bexp b = 0;  0 \<turnstile>' c \<rbrakk> \<Longrightarrow> 0 \<turnstile>' WHILE b DO c"  |
+anti_mono':
+  "\<lbrakk> l \<turnstile>' c;  l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile>' c"
+
+lemma "l \<turnstile> c \<Longrightarrow> l \<turnstile>' c"
+apply(induct rule: sec_type.induct)
+apply (metis Skip')
+apply (metis Assign')
+apply (metis Semi')
+apply (metis min_max.inf_sup_ord(3) min_max.sup_absorb2 nat_le_linear If' anti_mono')
+by (metis While')
+
+
+lemma "l \<turnstile>' c \<Longrightarrow> l \<turnstile> c"
+apply(induct rule: sec_type'.induct)
+apply (metis Skip)
+apply (metis Assign)
+apply (metis Semi)
+apply (metis min_max.sup_absorb2 If)
+apply (metis While)
+by (metis anti_mono)
+
+end
diff -r b505be6f029a -r 686fa0a0696e src/HOL/IMP/Small_Step.thy
--- a/src/HOL/IMP/Small_Step.thy	Mon Jun 06 16:29:13 2011 +0200
+++ b/src/HOL/IMP/Small_Step.thy	Mon Jun 06 16:29:38 2011 +0200
@@ -27,7 +27,7 @@
 
 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)}"
+    [''x'' \<rightarrow> 3, ''y'' \<rightarrow> 7, ''z'' \<rightarrow> 5]) \<rightarrow>* (c',t)}"
 
 
 subsection{* Proof infrastructure *}
diff -r b505be6f029a -r 686fa0a0696e src/HOL/IMP/Util.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Util.thy	Mon Jun 06 16:29:38 2011 +0200
@@ -0,0 +1,29 @@
+(* Author: Tobias Nipkow *)
+
+theory Util imports Main
+begin
+
+subsection "Show sets of variables as lists"
+
+text {* Sets are functions and are not displayed by element if
+computed as values: *}
+value "{''x'', ''y''}"
+
+text {* Lists do not have this problem *}
+value "[''x'', ''y'']"
+
+text {* We define a function @{text show} that converts a set of
+  variable names into a list. To keep things simple, we rely on
+  the convention that we only use single letter names.
+*}
+definition 
+  letters :: "string list" where
+  "letters = map (\<lambda>c. [c]) chars"
+
+definition 
+  "show" :: "string set \<Rightarrow> string list" where
+  "show S = filter S letters" 
+
+value "show {''x'', ''z''}"
+
+end
diff -r b505be6f029a -r 686fa0a0696e src/HOL/IMP/VC.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/VC.thy	Mon Jun 06 16:29:38 2011 +0200
@@ -0,0 +1,146 @@
+header "Verification Conditions"
+
+theory VC imports Hoare begin
+
+subsection "VCG via Weakest Preconditions"
+
+text{* Annotated commands: commands where loops are annotated with
+invariants. *}
+
+datatype acom = Askip
+              | Aassign name aexp
+              | Asemi   acom acom
+              | Aif     bexp acom acom
+              | Awhile  bexp assn acom
+
+text{* Weakest precondition from annotated commands: *}
+
+fun pre :: "acom \<Rightarrow> assn \<Rightarrow> assn" where
+"pre Askip Q = Q" |
+"pre (Aassign x a) Q = (\<lambda>s. Q(s(x := aval a s)))" |
+"pre (Asemi c\<^isub>1 c\<^isub>2) Q = pre c\<^isub>1 (pre c\<^isub>2 Q)" |
+"pre (Aif b c\<^isub>1 c\<^isub>2) Q =
+  (\<lambda>s. (bval b s \<longrightarrow> pre c\<^isub>1 Q s) \<and>
+       (\<not> bval b s \<longrightarrow> pre c\<^isub>2 Q s))" |
+"pre (Awhile b I c) Q = I"
+
+text{* Verification condition: *}
+
+fun vc :: "acom \<Rightarrow> assn \<Rightarrow> assn" where
+"vc Askip Q = (\<lambda>s. True)" |
+"vc (Aassign x a) Q = (\<lambda>s. True)" |
+"vc (Asemi c\<^isub>1 c\<^isub>2) Q = (\<lambda>s. vc c\<^isub>1 (pre c\<^isub>2 Q) s \<and> vc c\<^isub>2 Q s)" |
+"vc (Aif b c\<^isub>1 c\<^isub>2) Q = (\<lambda>s. vc c\<^isub>1 Q s \<and> vc c\<^isub>2 Q s)" |
+"vc (Awhile b I c) Q =
+  (\<lambda>s. (I s \<and> \<not> bval b s \<longrightarrow> Q s) \<and>
+       (I s \<and> bval b s \<longrightarrow> pre c I s) \<and>
+       vc c I s)"
+
+text{* Strip annotations: *}
+
+fun astrip :: "acom \<Rightarrow> com" where
+"astrip Askip = SKIP" |
+"astrip (Aassign x a) = (x::=a)" |
+"astrip (Asemi c\<^isub>1 c\<^isub>2) = (astrip c\<^isub>1; astrip c\<^isub>2)" |
+"astrip (Aif b c\<^isub>1 c\<^isub>2) = (IF b THEN astrip c\<^isub>1 ELSE astrip c\<^isub>2)" |
+"astrip (Awhile b I c) = (WHILE b DO astrip c)"
+
+
+subsection "Soundness"
+
+lemma vc_sound: "\<forall>s. vc c Q s \<Longrightarrow> \<turnstile> {pre 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: "\<forall>s. vc c I s" and IQ: "\<forall>s. I s \<and> \<not> bval b s \<longrightarrow> Q s" and
+         pre: "\<forall>s. I s \<and> bval b s \<longrightarrow> pre c I s" by simp_all
+    have "\<turnstile> {pre c I} astrip c {I}" by(rule Awhile.hyps[OF vc])
+    with pre show "\<turnstile> {\<lambda>s. I s \<and> bval b s} astrip c {I}"
+      by(rule strengthen_pre)
+    show "\<forall>s. I s \<and> \<not>bval b s \<longrightarrow> Q s" by(rule IQ)
+  qed
+qed (auto intro: hoare.conseq)
+
+corollary vc_sound':
+  "(\<forall>s. vc c Q s) \<and> (\<forall>s. P s \<longrightarrow> pre c Q s) \<Longrightarrow> \<turnstile> {P} astrip c {Q}"
+by (metis strengthen_pre vc_sound)
+
+
+subsection "Completeness"
+
+lemma pre_mono:
+  "\<forall>s. P s \<longrightarrow> P' s \<Longrightarrow> pre c P s \<Longrightarrow> pre c P' s"
+proof (induct c arbitrary: P P' s)
+  case Asemi thus ?case by simp metis
+qed simp_all
+
+lemma vc_mono:
+  "\<forall>s. P s \<longrightarrow> P' s \<Longrightarrow> vc c P s \<Longrightarrow> vc c P' s"
+proof(induct c arbitrary: P P')
+  case Asemi thus ?case by simp (metis pre_mono)
+qed simp_all
+
+lemma vc_complete:
+ "\<turnstile> {P}c{Q} \<Longrightarrow> \<exists>c'. astrip c' = c \<and> (\<forall>s. vc c' Q s) \<and> (\<forall>s. P s \<longrightarrow> pre c' Q s)"
+  (is "_ \<Longrightarrow> \<exists>c'. ?G P c Q c'")
+proof (induct rule: hoare.induct)
+  case Skip
+  show ?case (is "\<exists>ac. ?C ac")
+  proof show "?C Askip" by simp qed
+next
+  case (Assign P a x)
+  show ?case (is "\<exists>ac. ?C ac")
+  proof show "?C(Aassign x a)" by simp qed
+next
+  case (Semi P c1 Q c2 R)
+  from Semi.hyps obtain ac1 where ih1: "?G P c1 Q ac1" by blast
+  from Semi.hyps obtain ac2 where ih2: "?G Q c2 R ac2" by blast
+  show ?case (is "\<exists>ac. ?C ac")
+  proof
+    show "?C(Asemi ac1 ac2)"
+      using ih1 ih2 by (fastsimp elim!: pre_mono vc_mono)
+  qed
+next
+  case (If P b c1 Q c2)
+  from If.hyps obtain ac1 where ih1: "?G (\<lambda>s. P s \<and> bval b s) c1 Q ac1"
+    by blast
+  from If.hyps obtain ac2 where ih2: "?G (\<lambda>s. P s \<and> \<not>bval b s) c2 Q ac2"
+    by blast
+  show ?case (is "\<exists>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: "?G (\<lambda>s. P s \<and> bval b s) c P ac" by blast
+  show ?case (is "\<exists>ac. ?C ac")
+  proof show "?C(Awhile b P ac)" using ih by simp qed
+next
+  case conseq thus ?case by(fast elim!: pre_mono vc_mono)
+qed
+
+
+subsection "An Optimization"
+
+fun vcpre :: "acom \<Rightarrow> assn \<Rightarrow> assn \<times> assn" where
+"vcpre Askip Q = (\<lambda>s. True, Q)" |
+"vcpre (Aassign x a) Q = (\<lambda>s. True, \<lambda>s. Q(s[a/x]))" |
+"vcpre (Asemi c\<^isub>1 c\<^isub>2) Q =
+  (let (vc\<^isub>2,wp\<^isub>2) = vcpre c\<^isub>2 Q;
+       (vc\<^isub>1,wp\<^isub>1) = vcpre c\<^isub>1 wp\<^isub>2
+   in (\<lambda>s. vc\<^isub>1 s \<and> vc\<^isub>2 s, wp\<^isub>1))" |
+"vcpre (Aif b c\<^isub>1 c\<^isub>2) Q =
+  (let (vc\<^isub>2,wp\<^isub>2) = vcpre c\<^isub>2 Q;
+       (vc\<^isub>1,wp\<^isub>1) = vcpre c\<^isub>1 Q
+   in (\<lambda>s. vc\<^isub>1 s \<and> vc\<^isub>2 s, \<lambda>s. (bval b s \<longrightarrow> wp\<^isub>1 s) \<and> (\<not>bval b s \<longrightarrow> wp\<^isub>2 s)))" |
+"vcpre (Awhile b I c) Q =
+  (let (vcc,wpc) = vcpre c I
+   in (\<lambda>s. (I s \<and> \<not> bval b s \<longrightarrow> Q s) \<and>
+           (I s \<and> bval b s \<longrightarrow> wpc s) \<and> vcc s, I))"
+
+lemma vcpre_vc_pre: "vcpre c Q = (vc c Q, pre c Q)"
+by (induct c arbitrary: Q) (simp_all add: Let_def)
+
+end
diff -r b505be6f029a -r 686fa0a0696e src/HOL/IMP/Vars.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Vars.thy	Mon Jun 06 16:29:38 2011 +0200
@@ -0,0 +1,74 @@
+(* Author: Tobias Nipkow *)
+
+header "Definite Assignment Analysis"
+
+theory Vars imports Util BExp
+begin
+
+subsection "The Variables in an Expression"
+
+text{* We need to collect the variables in both arithmetic and boolean
+expressions. For a change we do not introduce two functions, e.g.\ @{text
+avars} and @{text bvars}, but we overload the name @{text vars}
+via a \emph{type class}, a device that originated with Haskell: *}
+ 
+class vars =
+fixes vars :: "'a \<Rightarrow> name set"
+
+text{* This defines a type class ``vars'' with a single
+function of (coincidentally) the same name. Then we define two separated
+instances of the class, one for @{typ aexp} and one for @{typ bexp}: *}
+
+instantiation aexp :: vars
+begin
+
+fun vars_aexp :: "aexp \<Rightarrow> name set" where
+"vars_aexp (N n) = {}" |
+"vars_aexp (V x) = {x}" |
+"vars_aexp (Plus a\<^isub>1 a\<^isub>2) = vars_aexp a\<^isub>1 \<union> vars_aexp a\<^isub>2"
+
+instance ..
+
+end
+
+value "vars(Plus (V ''x'') (V ''y''))"
+
+text{* We need to convert functions to lists before we can view them: *}
+
+value "show  (vars(Plus (V ''x'') (V ''y'')))"
+
+instantiation bexp :: vars
+begin
+
+fun vars_bexp :: "bexp \<Rightarrow> name set" where
+"vars_bexp (B bv) = {}" |
+"vars_bexp (Not b) = vars_bexp b" |
+"vars_bexp (And b\<^isub>1 b\<^isub>2) = vars_bexp b\<^isub>1 \<union> vars_bexp b\<^isub>2" |
+"vars_bexp (Less a\<^isub>1 a\<^isub>2) = vars a\<^isub>1 \<union> vars a\<^isub>2"
+
+instance ..
+
+end
+
+value "show  (vars(Less (Plus (V ''z'') (V ''y'')) (V ''x'')))"
+
+abbreviation
+  eq_on :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> bool"
+ ("(_ =/ _/ on _)" [50,0,50] 50) where
+"f = g on X == \<forall> x \<in> X. f x = g x"
+
+lemma aval_eq_if_eq_on_vars[simp]:
+  "s\<^isub>1 = s\<^isub>2 on vars a \<Longrightarrow> aval a s\<^isub>1 = aval a s\<^isub>2"
+apply(induct a)
+apply simp_all
+done
+
+lemma bval_eq_if_eq_on_vars:
+  "s\<^isub>1 = s\<^isub>2 on vars b \<Longrightarrow> bval b s\<^isub>1 = bval b s\<^isub>2"
+proof(induct b)
+  case (Less a1 a2)
+  hence "aval a1 s\<^isub>1 = aval a1 s\<^isub>2" and "aval a2 s\<^isub>1 = aval a2 s\<^isub>2" by simp_all
+  thus ?case by simp
+qed simp_all
+
+end
diff -r b505be6f029a -r 686fa0a0696e src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Jun 06 16:29:13 2011 +0200
+++ b/src/HOL/IsaMakefile	Mon Jun 06 16:29:38 2011 +0200
@@ -527,8 +527,16 @@
 HOL-IMP: HOL $(LOG)/HOL-IMP.gz
 
 $(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/Poly_Types.thy IMP/Small_Step.thy IMP/Star.thy IMP/Types.thy	\
+  IMP/Big_Step.thy IMP/C_like.thy IMP/Com.thy IMP/Compiler.thy \
+  IMP/Def_Ass.thy IMP/Def_Ass_Big.thy IMP/Def_Ass_Exp.thy \
+  IMP/Def_Ass_Small.thy IMP/Def_Ass_Sound_Big.thy \
+  IMP/Def_Ass_Sound_Small.thy IMP/Denotation.thy IMP/Hoare.thy \
+  IMP/HoareT.thy IMP/Hoare_Examples.thy IMP/Hoare_Sound_Complete.thy \
+  IMP/Live.thy IMP/OO.thy IMP/Poly_Types.thy IMP/Procs.thy \
+  IMP/Procs_Dyn_Vars_Dyn.thy IMP/Procs_Stat_Vars_Dyn.thy \
+  IMP/Procs_Stat_Vars_Stat.thy IMP/Sec_Type_Expr.thy IMP/Sec_Typing.thy \
+  IMP/Sec_TypingT.thy IMP/Small_Step.thy IMP/Star.thy IMP/Types.thy \
+  IMP/Util.thy IMP/VC.thy IMP/Vars.thy \
   IMP/ROOT.ML IMP/document/root.tex IMP/document/root.bib
 	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL IMP