imported rest of new IMP
authorkleing
Mon Jun 06 16:29:38 2011 +0200 (2011-06-06)
changeset 43158686fa0a0696e
parent 43157 b505be6f029a
child 43159 29b55f292e0b
imported rest of new IMP
src/HOL/IMP/AExp.thy
src/HOL/IMP/ASM.thy
src/HOL/IMP/BExp.thy
src/HOL/IMP/Big_Step.thy
src/HOL/IMP/C_like.thy
src/HOL/IMP/Compiler.thy
src/HOL/IMP/Def_Ass.thy
src/HOL/IMP/Def_Ass_Big.thy
src/HOL/IMP/Def_Ass_Exp.thy
src/HOL/IMP/Def_Ass_Small.thy
src/HOL/IMP/Def_Ass_Sound_Big.thy
src/HOL/IMP/Def_Ass_Sound_Small.thy
src/HOL/IMP/Hoare.thy
src/HOL/IMP/HoareT.thy
src/HOL/IMP/Hoare_Examples.thy
src/HOL/IMP/Hoare_Sound_Complete.thy
src/HOL/IMP/Live.thy
src/HOL/IMP/OO.thy
src/HOL/IMP/Procs.thy
src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy
src/HOL/IMP/Procs_Stat_Vars_Dyn.thy
src/HOL/IMP/Procs_Stat_Vars_Stat.thy
src/HOL/IMP/ROOT.ML
src/HOL/IMP/Sec_Type_Expr.thy
src/HOL/IMP/Sec_Typing.thy
src/HOL/IMP/Sec_TypingT.thy
src/HOL/IMP/Small_Step.thy
src/HOL/IMP/Util.thy
src/HOL/IMP/VC.thy
src/HOL/IMP/Vars.thy
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/IMP/AExp.thy	Mon Jun 06 16:29:13 2011 +0200
     1.2 +++ b/src/HOL/IMP/AExp.thy	Mon Jun 06 16:29:38 2011 +0200
     1.3 @@ -18,12 +18,42 @@
     1.4  
     1.5  value "aval (Plus (V ''x'') (N 5)) (%x. if x = ''x'' then 7 else 0)"
     1.6  
     1.7 -fun lookup :: "(string * val)list \<Rightarrow> string \<Rightarrow> val" where
     1.8 -"lookup ((x,i)#xis) y = (if x=y then i else lookup xis y)"
     1.9 +text {* The same state more concisely: *}
    1.10 +value "aval (Plus (V ''x'') (N 5)) ((%x. 0) (''x'':= 7))"
    1.11 +
    1.12 +text {* A little syntax magic to write larger states compactly: *}
    1.13 +
    1.14 +nonterminal funlets and funlet
    1.15 +
    1.16 +syntax
    1.17 +  "_funlet"  :: "['a, 'a] => funlet"             ("_ /->/ _")
    1.18 +   ""         :: "funlet => funlets"             ("_")
    1.19 +  "_Funlets" :: "[funlet, funlets] => funlets"   ("_,/ _")
    1.20 +  "_Fun"     :: "funlets => 'a => 'b"            ("(1[_])")
    1.21 +  "_FunUpd"  :: "['a => 'b, funlets] => 'a => 'b" ("_/'(_')" [900,0]900)
    1.22 +
    1.23 +syntax (xsymbols)
    1.24 +  "_funlet"  :: "['a, 'a] => funlet"             ("_ /\<rightarrow>/ _")
    1.25  
    1.26 -value "aval (Plus (V ''x'') (N 5)) (lookup [(''x'',7)])"
    1.27 +translations
    1.28 +  "_FunUpd m (_Funlets xy ms)"  == "_FunUpd (_FunUpd m xy) ms"
    1.29 +  "_FunUpd m (_funlet  x y)"    == "m(x := y)"
    1.30 +  "_Fun ms"                     == "_FunUpd (%_. 0) ms"
    1.31 +  "_Fun (_Funlets ms1 ms2)"     <= "_FunUpd (_Fun ms1) ms2"
    1.32 +  "_Funlets ms1 (_Funlets ms2 ms3)" <= "_Funlets (_Funlets ms1 ms2) ms3"
    1.33  
    1.34 -value "aval (Plus (V ''x'') (N 5)) (lookup [(''y'',7)])"
    1.35 +text {* 
    1.36 +  We can now write a series of updates to the function @{text "\<lambda>x. 0"} compactly:
    1.37 +*}
    1.38 +lemma "[a \<rightarrow> Suc 0, b \<rightarrow> 2] = ((%_. 0) (a := Suc 0)) (b := 2)"
    1.39 +  by (rule refl)
    1.40 +
    1.41 +value "aval (Plus (V ''x'') (N 5)) [''x'' \<rightarrow> 7]"
    1.42 +
    1.43 +text {* Variables that are not mentioned in the state are 0 by default in 
    1.44 +  the @{term "[a \<rightarrow> b::int]"} syntax: 
    1.45 +*}   
    1.46 +value "aval (Plus (V ''x'') (N 5)) [''y'' \<rightarrow> 7]"
    1.47  
    1.48  
    1.49  subsection "Optimization"
    1.50 @@ -53,7 +83,6 @@
    1.51  "plus a (N i) = (if i=0 then a else Plus a (N i))" |
    1.52  "plus a1 a2 = Plus a1 a2"
    1.53  
    1.54 -text ""
    1.55  code_thms plus
    1.56  code_thms plus
    1.57  
     2.1 --- a/src/HOL/IMP/ASM.thy	Mon Jun 06 16:29:13 2011 +0200
     2.2 +++ b/src/HOL/IMP/ASM.thy	Mon Jun 06 16:29:38 2011 +0200
     2.3 @@ -25,7 +25,7 @@
     2.4  "aexec (i#is) s stk = aexec is s (aexec1 i s stk)"
     2.5  
     2.6  value "aexec [LOADI 5, LOAD ''y'', ADD]
     2.7 -  (lookup[(''x'',42), (''y'',43)]) [50]"
     2.8 + [''x'' \<rightarrow> 42, ''y'' \<rightarrow> 43] [50]"
     2.9  
    2.10  lemma aexec_append[simp]:
    2.11    "aexec (is1@is2) s stk = aexec is2 s (aexec is1 s stk)"
     3.1 --- a/src/HOL/IMP/BExp.thy	Mon Jun 06 16:29:13 2011 +0200
     3.2 +++ b/src/HOL/IMP/BExp.thy	Mon Jun 06 16:29:38 2011 +0200
     3.3 @@ -11,7 +11,7 @@
     3.4  "bval (Less a1 a2) s = (aval a1 s < aval a2 s)"
     3.5  
     3.6  value "bval (Less (V ''x'') (Plus (N 3) (V ''y'')))
     3.7 -  (lookup [(''x'',3),(''y'',1)])"
     3.8 +            [''x'' \<rightarrow> 3, ''y'' \<rightarrow> 1]"
     3.9  
    3.10  
    3.11  subsection "Optimization"
     4.1 --- a/src/HOL/IMP/Big_Step.thy	Mon Jun 06 16:29:13 2011 +0200
     4.2 +++ b/src/HOL/IMP/Big_Step.thy	Mon Jun 06 16:29:38 2011 +0200
     4.3 @@ -37,18 +37,18 @@
     4.4  text{* For inductive definitions we need command
     4.5         \texttt{values} instead of \texttt{value}. *}
     4.6  
     4.7 -values "{t. (SKIP, lookup[]) \<Rightarrow> t}"
     4.8 +values "{t. (SKIP, %_. 0) \<Rightarrow> t}"
     4.9  
    4.10  text{* We need to translate the result state into a list
    4.11  to display it. *}
    4.12  
    4.13 -values "{map t [''x''] |t. (SKIP, lookup [(''x'',42)]) \<Rightarrow> t}"
    4.14 +values "{map t [''x''] |t. (SKIP, [''x'' \<rightarrow> 42]) \<Rightarrow> t}"
    4.15  
    4.16 -values "{map t [''x''] |t. (''x'' ::= N 2, lookup [(''x'',42)]) \<Rightarrow> t}"
    4.17 +values "{map t [''x''] |t. (''x'' ::= N 2, [''x'' \<rightarrow> 42]) \<Rightarrow> t}"
    4.18  
    4.19  values "{map t [''x'',''y''] |t.
    4.20    (WHILE Less (V ''x'') (V ''y'') DO (''x'' ::= Plus (V ''x'') (N 5)),
    4.21 -   lookup [(''x'',0),(''y'',13)]) \<Rightarrow> t}"
    4.22 +   [''x'' \<rightarrow> 0, ''y'' \<rightarrow> 13]) \<Rightarrow> t}"
    4.23  
    4.24  
    4.25  text{* Proof automation: *}
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/IMP/C_like.thy	Mon Jun 06 16:29:38 2011 +0200
     5.3 @@ -0,0 +1,95 @@
     5.4 +theory C_like imports Main begin
     5.5 +
     5.6 +subsection "A C-like Language"
     5.7 +
     5.8 +type_synonym state = "nat \<Rightarrow> nat"
     5.9 +
    5.10 +datatype aexp = N nat | Deref aexp ("!") | Plus aexp aexp
    5.11 +
    5.12 +fun aval :: "aexp \<Rightarrow> state \<Rightarrow> nat" where
    5.13 +"aval (N n) s = n" |
    5.14 +"aval (!a) s = s(aval a s)" |
    5.15 +"aval (Plus a\<^isub>1 a\<^isub>2) s = aval a\<^isub>1 s + aval a\<^isub>2 s"
    5.16 +
    5.17 +datatype bexp = B bool | Not bexp | And bexp bexp | Less aexp aexp
    5.18 +
    5.19 +primrec bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where
    5.20 +"bval (B bv) _ = bv" |
    5.21 +"bval (Not b) s = (\<not> bval b s)" |
    5.22 +"bval (And b\<^isub>1 b\<^isub>2) s = (if bval b\<^isub>1 s then bval b\<^isub>2 s else False)" |
    5.23 +"bval (Less a\<^isub>1 a\<^isub>2) s = (aval a\<^isub>1 s < aval a\<^isub>2 s)"
    5.24 +
    5.25 +
    5.26 +datatype
    5.27 +  com = SKIP 
    5.28 +      | Assign aexp aexp         ("_ ::= _" [61, 61] 61)
    5.29 +      | New    aexp aexp
    5.30 +      | Semi   com  com          ("_;/ _"  [60, 61] 60)
    5.31 +      | If     bexp com com     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61)
    5.32 +      | While  bexp com         ("(WHILE _/ DO _)"  [0, 61] 61)
    5.33 +
    5.34 +inductive
    5.35 +  big_step :: "com \<times> state \<times> nat \<Rightarrow> state \<times> nat \<Rightarrow> bool"  (infix "\<Rightarrow>" 55)
    5.36 +where
    5.37 +Skip:    "(SKIP,sn) \<Rightarrow> sn" |
    5.38 +Assign:  "(lhs ::= a,s,n) \<Rightarrow> (s(aval lhs s := aval a s),n)" |
    5.39 +New:     "(New lhs a,s,n) \<Rightarrow> (s(aval lhs s := n), n+aval a s)"  |
    5.40 +Semi:    "\<lbrakk> (c\<^isub>1,sn\<^isub>1) \<Rightarrow> sn\<^isub>2;  (c\<^isub>2,sn\<^isub>2) \<Rightarrow> sn\<^isub>3 \<rbrakk> \<Longrightarrow>
    5.41 +          (c\<^isub>1;c\<^isub>2, sn\<^isub>1) \<Rightarrow> sn\<^isub>3" |
    5.42 +
    5.43 +IfTrue:  "\<lbrakk> bval b s;  (c\<^isub>1,s,n) \<Rightarrow> tn \<rbrakk> \<Longrightarrow>
    5.44 +         (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s,n) \<Rightarrow> tn" |
    5.45 +IfFalse: "\<lbrakk> \<not>bval b s;  (c\<^isub>2,s,n) \<Rightarrow> tn \<rbrakk> \<Longrightarrow>
    5.46 +         (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s,n) \<Rightarrow> tn" |
    5.47 +
    5.48 +WhileFalse: "\<not>bval b s \<Longrightarrow> (WHILE b DO c,s,n) \<Rightarrow> (s,n)" |
    5.49 +WhileTrue:
    5.50 +  "\<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>
    5.51 +   (WHILE b DO c, s\<^isub>1,n) \<Rightarrow> sn\<^isub>3"
    5.52 +
    5.53 +code_pred big_step .
    5.54 +
    5.55 +
    5.56 +text{* Examples: *}
    5.57 +
    5.58 +definition
    5.59 +"array_sum =
    5.60 + WHILE Less (!(N 0)) (Plus (!(N 1)) (N 1))
    5.61 + DO ( N 2 ::= Plus (!(N 2)) (!(!(N 0)));
    5.62 +      N 0 ::= Plus (!(N 0)) (N 1) )"
    5.63 +
    5.64 +text {* To show the first n variables in a @{typ "nat \<Rightarrow> nat"} state: *}
    5.65 +definition 
    5.66 +  "list t n = map t [0 ..< n]"
    5.67 +
    5.68 +values "{list t n |t n. (array_sum, nth[3,4,0,3,7],5) \<Rightarrow> (t,n)}"
    5.69 +
    5.70 +definition
    5.71 +"linked_list_sum =
    5.72 + WHILE Less (N 0) (!(N 0))
    5.73 + DO ( N 1 ::= Plus(!(N 1)) (!(!(N 0)));
    5.74 +      N 0 ::= !(Plus(!(N 0))(N 1)) )"
    5.75 +
    5.76 +values "{list t n |t n. (linked_list_sum, nth[4,0,3,0,7,2],6) \<Rightarrow> (t,n)}"
    5.77 +
    5.78 +definition
    5.79 +"array_init =
    5.80 + New (N 0) (!(N 1)); N 2 ::= !(N 0);
    5.81 + WHILE Less (!(N 2)) (Plus (!(N 0)) (!(N 1)))
    5.82 + DO ( !(N 2) ::= !(N 2);
    5.83 +      N 2 ::= Plus (!(N 2)) (N 1) )"
    5.84 +
    5.85 +values "{list t n |t n. (array_init, nth[5,2,7],3) \<Rightarrow> (t,n)}"
    5.86 +
    5.87 +definition
    5.88 +"linked_list_init =
    5.89 + WHILE Less (!(N 1)) (!(N 0))
    5.90 + DO ( New (N 3) (N 2);
    5.91 +      N 1 ::=  Plus (!(N 1)) (N 1);
    5.92 +      !(N 3) ::= !(N 1);
    5.93 +      Plus (!(N 3)) (N 1) ::= !(N 2);
    5.94 +      N 2 ::= !(N 3) )"
    5.95 +
    5.96 +values "{list t n |t n. (linked_list_init, nth[2,0,0,0],4) \<Rightarrow> (t,n)}"
    5.97 +
    5.98 +end
     6.1 --- a/src/HOL/IMP/Compiler.thy	Mon Jun 06 16:29:13 2011 +0200
     6.2 +++ b/src/HOL/IMP/Compiler.thy	Mon Jun 06 16:29:38 2011 +0200
     6.3 @@ -60,7 +60,7 @@
     6.4  values
     6.5    "{(i,map t [''x'',''y''],stk) | i t stk.
     6.6      [LOAD ''y'', STORE ''x''] \<turnstile>
     6.7 -    (0,lookup[(''x'',3),(''y'',4)],[]) \<rightarrow>* (i,t,stk)}"
     6.8 +    (0, [''x'' \<rightarrow> 3, ''y'' \<rightarrow> 4], []) \<rightarrow>* (i,t,stk)}"
     6.9  
    6.10  
    6.11  subsection{* Verification infrastructure *}
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/IMP/Def_Ass.thy	Mon Jun 06 16:29:38 2011 +0200
     7.3 @@ -0,0 +1,25 @@
     7.4 +theory Def_Ass imports Vars Com
     7.5 +begin
     7.6 +
     7.7 +subsection "Definite Assignment Analysis"
     7.8 +
     7.9 +inductive D :: "name set \<Rightarrow> com \<Rightarrow> name set \<Rightarrow> bool" where
    7.10 +Skip: "D A SKIP A" |
    7.11 +Assign: "vars a \<subseteq> A \<Longrightarrow> D A (x ::= a) (insert x A)" |
    7.12 +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" |
    7.13 +If: "\<lbrakk> vars b \<subseteq> A;  D A c\<^isub>1 A\<^isub>1;  D A c\<^isub>2 A\<^isub>2 \<rbrakk> \<Longrightarrow>
    7.14 +  D A (IF b THEN c\<^isub>1 ELSE c\<^isub>2) (A\<^isub>1 Int A\<^isub>2)" |
    7.15 +While: "\<lbrakk> vars b \<subseteq> A;  D A c A' \<rbrakk> \<Longrightarrow> D A (WHILE b DO c) A"
    7.16 +
    7.17 +inductive_cases [elim!]:
    7.18 +"D A SKIP A'"
    7.19 +"D A (x ::= a) A'"
    7.20 +"D A (c1;c2) A'"
    7.21 +"D A (IF b THEN c1 ELSE c2) A'"
    7.22 +"D A (WHILE b DO c) A'"
    7.23 +
    7.24 +lemma D_incr: 
    7.25 +  "D A c A' \<Longrightarrow> A \<subseteq> A'"
    7.26 +by (induct rule: D.induct) auto
    7.27 +
    7.28 +end
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/IMP/Def_Ass_Big.thy	Mon Jun 06 16:29:38 2011 +0200
     8.3 @@ -0,0 +1,31 @@
     8.4 +(* Author: Tobias Nipkow *)
     8.5 +
     8.6 +theory Def_Ass_Big imports Com Def_Ass_Exp
     8.7 +begin
     8.8 +
     8.9 +subsection "Initialization-Sensitive Big Step Semantics"
    8.10 +
    8.11 +inductive
    8.12 +  big_step :: "(com \<times> state option) \<Rightarrow> state option \<Rightarrow> bool" (infix "\<Rightarrow>" 55)
    8.13 +where
    8.14 +None: "(c,None) \<Rightarrow> None" |
    8.15 +Skip: "(SKIP,s) \<Rightarrow> s" |
    8.16 +AssignNone: "aval a s = None \<Longrightarrow> (x ::= a, Some s) \<Rightarrow> None" |
    8.17 +Assign: "aval a s = Some i \<Longrightarrow> (x ::= a, Some s) \<Rightarrow> Some(s(x := Some i))" |
    8.18 +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" |
    8.19 +
    8.20 +IfNone:  "bval b s = None \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,Some s) \<Rightarrow> None" |
    8.21 +IfTrue:  "\<lbrakk> bval b s = Some True;  (c\<^isub>1,Some s) \<Rightarrow> s' \<rbrakk> \<Longrightarrow>
    8.22 +  (IF b THEN c\<^isub>1 ELSE c\<^isub>2,Some s) \<Rightarrow> s'" |
    8.23 +IfFalse: "\<lbrakk> bval b s = Some False;  (c\<^isub>2,Some s) \<Rightarrow> s' \<rbrakk> \<Longrightarrow>
    8.24 +  (IF b THEN c\<^isub>1 ELSE c\<^isub>2,Some s) \<Rightarrow> s'" |
    8.25 +
    8.26 +WhileNone: "bval b s = None \<Longrightarrow> (WHILE b DO c,Some s) \<Rightarrow> None" |
    8.27 +WhileFalse: "bval b s = Some False \<Longrightarrow> (WHILE b DO c,Some s) \<Rightarrow> Some s" |
    8.28 +WhileTrue:
    8.29 +  "\<lbrakk> bval b s = Some True;  (c,Some s) \<Rightarrow> s';  (WHILE b DO c,s') \<Rightarrow> s'' \<rbrakk> \<Longrightarrow>
    8.30 +  (WHILE b DO c,Some s) \<Rightarrow> s''"
    8.31 +
    8.32 +lemmas big_step_induct = big_step.induct[split_format(complete)]
    8.33 +
    8.34 +end
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/IMP/Def_Ass_Exp.thy	Mon Jun 06 16:29:38 2011 +0200
     9.3 @@ -0,0 +1,35 @@
     9.4 +(* Author: Tobias Nipkow *)
     9.5 +
     9.6 +theory Def_Ass_Exp imports Vars
     9.7 +begin
     9.8 +
     9.9 +subsection "Initialization-Sensitive Expressions Evaluation"
    9.10 +
    9.11 +type_synonym val = "int"
    9.12 +type_synonym state = "name \<Rightarrow> val option"
    9.13 +
    9.14 +
    9.15 +fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val option" where
    9.16 +"aval (N i) s = Some i" |
    9.17 +"aval (V x) s = s x" |
    9.18 +"aval (Plus a\<^isub>1 a\<^isub>2) s =
    9.19 +  (case (aval a\<^isub>1 s, aval a\<^isub>2 s) of
    9.20 +     (Some i\<^isub>1,Some i\<^isub>2) \<Rightarrow> Some(i\<^isub>1+i\<^isub>2) | _ \<Rightarrow> None)"
    9.21 +
    9.22 +
    9.23 +fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool option" where
    9.24 +"bval (B bv) s = Some bv" |
    9.25 +"bval (Not b) s = (case bval b s of None \<Rightarrow> None | Some bv \<Rightarrow> Some(\<not> bv))" |
    9.26 +"bval (And b\<^isub>1 b\<^isub>2) s = (case (bval b\<^isub>1 s, bval b\<^isub>2 s) of
    9.27 +  (Some bv\<^isub>1, Some bv\<^isub>2) \<Rightarrow> Some(bv\<^isub>1 & bv\<^isub>2) | _ \<Rightarrow> None)" |
    9.28 +"bval (Less a\<^isub>1 a\<^isub>2) s = (case (aval a\<^isub>1 s, aval a\<^isub>2 s) of
    9.29 + (Some i\<^isub>1, Some i\<^isub>2) \<Rightarrow> Some(i\<^isub>1 < i\<^isub>2) | _ \<Rightarrow> None)"
    9.30 +
    9.31 +
    9.32 +lemma aval_Some: "vars a \<subseteq> dom s \<Longrightarrow> \<exists> i. aval a s = Some i"
    9.33 +by (induct a) auto
    9.34 +
    9.35 +lemma bval_Some: "vars b \<subseteq> dom s \<Longrightarrow> \<exists> bv. bval b s = Some bv"
    9.36 +by (induct b) (auto dest!: aval_Some)
    9.37 +
    9.38 +end
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/IMP/Def_Ass_Small.thy	Mon Jun 06 16:29:38 2011 +0200
    10.3 @@ -0,0 +1,26 @@
    10.4 +(* Author: Tobias Nipkow *)
    10.5 +
    10.6 +theory Def_Ass_Small imports Star Com Def_Ass_Exp
    10.7 +begin
    10.8 +
    10.9 +subsection "Initialization-Sensitive Small Step Semantics"
   10.10 +
   10.11 +inductive
   10.12 +  small_step :: "(com \<times> state) \<Rightarrow> (com \<times> state) \<Rightarrow> bool" (infix "\<rightarrow>" 55)
   10.13 +where
   10.14 +Assign:  "aval a s = Some i \<Longrightarrow> (x ::= a, s) \<rightarrow> (SKIP, s(x := Some i))" |
   10.15 +
   10.16 +Semi1:   "(SKIP;c,s) \<rightarrow> (c,s)" |
   10.17 +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')" |
   10.18 +
   10.19 +IfTrue:  "bval b s = Some True \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>1,s)" |
   10.20 +IfFalse: "bval b s = Some False \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)" |
   10.21 +
   10.22 +While:   "(WHILE b DO c,s) \<rightarrow> (IF b THEN c; WHILE b DO c ELSE SKIP,s)"
   10.23 +
   10.24 +lemmas small_step_induct = small_step.induct[split_format(complete)]
   10.25 +
   10.26 +abbreviation small_steps :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>*" 55)
   10.27 +where "x \<rightarrow>* y == star small_step x y"
   10.28 +
   10.29 +end
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/IMP/Def_Ass_Sound_Big.thy	Mon Jun 06 16:29:38 2011 +0200
    11.3 @@ -0,0 +1,41 @@
    11.4 +(* Author: Tobias Nipkow *)
    11.5 +
    11.6 +theory Def_Ass_Sound_Big imports Def_Ass Def_Ass_Big
    11.7 +begin
    11.8 +
    11.9 +
   11.10 +subsection "Soundness wrt Big Steps"
   11.11 +
   11.12 +text{* Note the special form of the induction because one of the arguments
   11.13 +of the inductive predicate is not a variable but the term @{term"Some s"}: *}
   11.14 +
   11.15 +theorem Sound:
   11.16 +  "\<lbrakk> (c,Some s) \<Rightarrow> s';  D A c A';  A \<subseteq> dom s \<rbrakk>
   11.17 +  \<Longrightarrow> \<exists> t. s' = Some t \<and> A' \<subseteq> dom t"
   11.18 +proof (induct c "Some s" s' arbitrary: s A A' rule:big_step_induct)
   11.19 +  case AssignNone thus ?case
   11.20 +    by auto (metis aval_Some option.simps(3) subset_trans)
   11.21 +next
   11.22 +  case Semi thus ?case by auto metis
   11.23 +next
   11.24 +  case IfTrue thus ?case by auto blast
   11.25 +next
   11.26 +  case IfFalse thus ?case by auto blast
   11.27 +next
   11.28 +  case IfNone thus ?case
   11.29 +    by auto (metis bval_Some option.simps(3) order_trans)
   11.30 +next
   11.31 +  case WhileNone thus ?case
   11.32 +    by auto (metis bval_Some option.simps(3) order_trans)
   11.33 +next
   11.34 +  case (WhileTrue b s c s' s'')
   11.35 +  from `D A (WHILE b DO c) A'` obtain A' where "D A c A'" by blast
   11.36 +  then obtain t' where "s' = Some t'" "A \<subseteq> dom t'"
   11.37 +    by (metis D_incr WhileTrue(3,7) subset_trans)
   11.38 +  from WhileTrue(5)[OF this(1) WhileTrue(6) this(2)] show ?case .
   11.39 +qed auto
   11.40 +
   11.41 +corollary sound: "\<lbrakk>  D (dom s) c A';  (c,Some s) \<Rightarrow> s' \<rbrakk> \<Longrightarrow> s' \<noteq> None"
   11.42 +by (metis Sound not_Some_eq subset_refl)
   11.43 +
   11.44 +end
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/HOL/IMP/Def_Ass_Sound_Small.thy	Mon Jun 06 16:29:38 2011 +0200
    12.3 @@ -0,0 +1,56 @@
    12.4 +(* Author: Tobias Nipkow *)
    12.5 +
    12.6 +theory Def_Ass_Sound_Small imports Def_Ass Def_Ass_Small
    12.7 +begin
    12.8 +
    12.9 +subsection "Soundness wrt Small Steps"
   12.10 +
   12.11 +theorem progress:
   12.12 +  "D (dom s) c A' \<Longrightarrow> c \<noteq> SKIP \<Longrightarrow> EX cs'. (c,s) \<rightarrow> cs'"
   12.13 +proof (induct c arbitrary: s A')
   12.14 +  case Assign thus ?case by auto (metis aval_Some small_step.Assign)
   12.15 +next
   12.16 +  case (If b c1 c2)
   12.17 +  then obtain bv where "bval b s = Some bv" by (auto dest!:bval_Some)
   12.18 +  then show ?case
   12.19 +    by(cases bv)(auto intro: small_step.IfTrue small_step.IfFalse)
   12.20 +qed (fastsimp intro: small_step.intros)+
   12.21 +
   12.22 +lemma D_mono:  "D A c M \<Longrightarrow> A \<subseteq> A' \<Longrightarrow> EX M'. D A' c M' & M <= M'"
   12.23 +proof (induct c arbitrary: A A' M)
   12.24 +  case Semi thus ?case by auto (metis D.intros(3))
   12.25 +next
   12.26 +  case (If b c1 c2)
   12.27 +  then obtain M1 M2 where "vars b \<subseteq> A" "D A c1 M1" "D A c2 M2" "M = M1 \<inter> M2"
   12.28 +    by auto
   12.29 +  with If.hyps `A \<subseteq> A'` obtain M1' M2'
   12.30 +    where "D A' c1 M1'" "D A' c2 M2'" and "M1 \<subseteq> M1'" "M2 \<subseteq> M2'" by metis
   12.31 +  hence "D A' (IF b THEN c1 ELSE c2) (M1' \<inter> M2')" and "M \<subseteq> M1' \<inter> M2'"
   12.32 +    using `vars b \<subseteq> A` `A \<subseteq> A'` `M = M1 \<inter> M2` by(fastsimp intro: D.intros)+
   12.33 +  thus ?case by metis
   12.34 +next
   12.35 +  case While thus ?case by auto (metis D.intros(5) subset_trans)
   12.36 +qed (auto intro: D.intros)
   12.37 +
   12.38 +theorem D_preservation:
   12.39 +  "(c,s) \<rightarrow> (c',s') \<Longrightarrow> D (dom s) c A \<Longrightarrow> EX A'. D (dom s') c' A' & A <= A'"
   12.40 +proof (induct arbitrary: A rule: small_step_induct)
   12.41 +  case (While b c s)
   12.42 +  then obtain A' where "vars b \<subseteq> dom s" "A = dom s" "D (dom s) c A'" by blast
   12.43 +  moreover
   12.44 +  then obtain A'' where "D A' c A''" by (metis D_incr D_mono)
   12.45 +  ultimately have "D (dom s) (IF b THEN c; WHILE b DO c ELSE SKIP) (dom s)"
   12.46 +    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)
   12.47 +  thus ?case by (metis D_incr `A = dom s`)
   12.48 +next
   12.49 +  case Semi2 thus ?case by auto (metis D_mono D.intros(3))
   12.50 +qed (auto intro: D.intros)
   12.51 +
   12.52 +theorem D_sound:
   12.53 +  "(c,s) \<rightarrow>* (c',s') \<Longrightarrow> D (dom s) c A' \<Longrightarrow> c' \<noteq> SKIP
   12.54 +   \<Longrightarrow> \<exists>cs''. (c',s') \<rightarrow> cs''"
   12.55 +apply(induct arbitrary: A' rule:star_induct)
   12.56 +apply (metis progress)
   12.57 +by (metis D_preservation)
   12.58 +
   12.59 +end
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/HOL/IMP/Hoare.thy	Mon Jun 06 16:29:38 2011 +0200
    13.3 @@ -0,0 +1,59 @@
    13.4 +(* Author: Tobias Nipkow *)
    13.5 +
    13.6 +header "Hoare Logic"
    13.7 +
    13.8 +theory Hoare imports Big_Step begin
    13.9 +
   13.10 +subsection "Hoare Logic for Partial Correctness"
   13.11 +
   13.12 +type_synonym assn = "state \<Rightarrow> bool"
   13.13 +
   13.14 +abbreviation state_subst :: "state \<Rightarrow> aexp \<Rightarrow> name \<Rightarrow> state"
   13.15 +  ("_[_'/_]" [1000,0,0] 999)
   13.16 +where "s[a/x] == s(x := aval a s)"
   13.17 +
   13.18 +inductive
   13.19 +  hoare :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<turnstile> ({(1_)}/ (_)/ {(1_)})" 50)
   13.20 +where
   13.21 +Skip: "\<turnstile> {P} SKIP {P}"  |
   13.22 +
   13.23 +Assign:  "\<turnstile> {\<lambda>s. P(s[a/x])} x::=a {P}"  |
   13.24 +
   13.25 +Semi: "\<lbrakk> \<turnstile> {P} c\<^isub>1 {Q};  \<turnstile> {Q} c\<^isub>2 {R} \<rbrakk>
   13.26 +       \<Longrightarrow> \<turnstile> {P} c\<^isub>1;c\<^isub>2 {R}"  |
   13.27 +
   13.28 +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>
   13.29 +     \<Longrightarrow> \<turnstile> {P} IF b THEN c\<^isub>1 ELSE c\<^isub>2 {Q}"  |
   13.30 +
   13.31 +While: "\<turnstile> {\<lambda>s. P s \<and> bval b s} c {P} \<Longrightarrow>
   13.32 +        \<turnstile> {P} WHILE b DO c {\<lambda>s. P s \<and> \<not> bval b s}"  |
   13.33 +
   13.34 +conseq: "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s;  \<turnstile> {P} c {Q};  \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk>
   13.35 +        \<Longrightarrow> \<turnstile> {P'} c {Q'}"
   13.36 +
   13.37 +lemmas [simp] = hoare.Skip hoare.Assign hoare.Semi If
   13.38 +
   13.39 +lemmas [intro!] = hoare.Skip hoare.Assign hoare.Semi hoare.If
   13.40 +
   13.41 +lemma strengthen_pre:
   13.42 +  "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s;  \<turnstile> {P} c {Q} \<rbrakk> \<Longrightarrow> \<turnstile> {P'} c {Q}"
   13.43 +by (blast intro: conseq)
   13.44 +
   13.45 +lemma weaken_post:
   13.46 +  "\<lbrakk> \<turnstile> {P} c {Q};  \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk> \<Longrightarrow>  \<turnstile> {P} c {Q'}"
   13.47 +by (blast intro: conseq)
   13.48 +
   13.49 +text{* The assignment and While rule are awkward to use in actual proofs
   13.50 +because their pre and postcondition are of a very special form and the actual
   13.51 +goal would have to match this form exactly. Therefore we derive two variants
   13.52 +with arbitrary pre and postconditions. *}
   13.53 +
   13.54 +lemma Assign': "\<forall>s. P s \<longrightarrow> Q(s[a/x]) \<Longrightarrow> \<turnstile> {P} x ::= a {Q}"
   13.55 +by (simp add: strengthen_pre[OF _ Assign])
   13.56 +
   13.57 +lemma While':
   13.58 +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"
   13.59 +shows "\<turnstile> {P} WHILE b DO c {Q}"
   13.60 +by(rule weaken_post[OF While[OF assms(1)] assms(2)])
   13.61 +
   13.62 +end
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/HOL/IMP/HoareT.thy	Mon Jun 06 16:29:38 2011 +0200
    14.3 @@ -0,0 +1,215 @@
    14.4 +header{* Hoare Logic for Total Correctness *}
    14.5 +
    14.6 +theory HoareT imports Hoare_Sound_Complete Util begin
    14.7 +
    14.8 +text{*
    14.9 +Now that we have termination, we can define
   14.10 +total validity, @{text"\<Turnstile>\<^sub>t"}, as partial validity and guaranteed termination:*}
   14.11 +
   14.12 +definition hoare_tvalid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool"
   14.13 +  ("\<Turnstile>\<^sub>t {(1_)}/ (_)/ {(1_)}" 50) where
   14.14 +"\<Turnstile>\<^sub>t {P}c{Q}  \<equiv>  \<forall>s. P s \<longrightarrow> (\<exists>t. (c,s) \<Rightarrow> t \<and> Q t)"
   14.15 +
   14.16 +text{* Proveability of Hoare triples in the proof system for total
   14.17 +correctness is written @{text"\<turnstile>\<^sub>t {P}c{Q}"} and defined
   14.18 +inductively. The rules for @{text"\<turnstile>\<^sub>t"} differ from those for
   14.19 +@{text"\<turnstile>"} only in the one place where nontermination can arise: the
   14.20 +@{term While}-rule. *}
   14.21 +
   14.22 +inductive
   14.23 +  hoaret :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<turnstile>\<^sub>t ({(1_)}/ (_)/ {(1_)})" 50)
   14.24 +where
   14.25 +Skip:  "\<turnstile>\<^sub>t {P} SKIP {P}" |
   14.26 +Assign:  "\<turnstile>\<^sub>t {\<lambda>s. P(s[a/x])} x::=a {P}" |
   14.27 +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}" |
   14.28 +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>
   14.29 +  \<Longrightarrow> \<turnstile>\<^sub>t {P} IF b THEN c\<^isub>1 ELSE c\<^isub>2 {Q}" |
   14.30 +While:
   14.31 +  "\<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>
   14.32 +   \<Longrightarrow> \<turnstile>\<^sub>t {P} WHILE b DO c {\<lambda>s. P s \<and> \<not>bval b s}" |
   14.33 +conseq: "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile>\<^sub>t {P}c{Q}; \<forall>s. Q s \<longrightarrow> Q' s  \<rbrakk> \<Longrightarrow>
   14.34 +           \<turnstile>\<^sub>t {P'}c{Q'}"
   14.35 +
   14.36 +text{* The @{term While}-rule is like the one for partial correctness but it
   14.37 +requires additionally that with every execution of the loop body some measure
   14.38 +function @{term[source]"f :: state \<Rightarrow> nat"} decreases. *}
   14.39 +
   14.40 +lemma strengthen_pre:
   14.41 +  "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s;  \<turnstile>\<^sub>t {P} c {Q} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P'} c {Q}"
   14.42 +by (metis conseq)
   14.43 +
   14.44 +lemma weaken_post:
   14.45 +  "\<lbrakk> \<turnstile>\<^sub>t {P} c {Q};  \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk> \<Longrightarrow>  \<turnstile>\<^sub>t {P} c {Q'}"
   14.46 +by (metis conseq)
   14.47 +
   14.48 +lemma Assign': "\<forall>s. P s \<longrightarrow> Q(s[a/x]) \<Longrightarrow> \<turnstile>\<^sub>t {P} x ::= a {Q}"
   14.49 +by (simp add: strengthen_pre[OF _ Assign])
   14.50 +
   14.51 +lemma While':
   14.52 +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}"
   14.53 +    and "\<forall>s. P s \<and> \<not> bval b s \<longrightarrow> Q s"
   14.54 +shows "\<turnstile>\<^sub>t {P} WHILE b DO c {Q}"
   14.55 +by(blast intro: assms(1) weaken_post[OF While assms(2)])
   14.56 +
   14.57 +text{* Our standard example: *}
   14.58 +
   14.59 +abbreviation "w n ==
   14.60 +  WHILE Less (V ''y'') (N n)
   14.61 +  DO ( ''y'' ::= Plus (V ''y'') (N 1); ''x'' ::= Plus (V ''x'') (V ''y'') )"
   14.62 +
   14.63 +lemma "\<turnstile>\<^sub>t {\<lambda>s. 0 <= n} ''x'' ::= N 0; ''y'' ::= N 0; w n {\<lambda>s. s ''x'' = \<Sum> {1 .. n}}"
   14.64 +apply(rule Semi)
   14.65 +prefer 2
   14.66 +apply(rule While'
   14.67 +  [where P = "\<lambda>s. s ''x'' = \<Sum> {1..s ''y''} \<and> 0 <= n \<and> 0 <= s ''y'' \<and> s ''y'' \<le> n"
   14.68 +   and f = "\<lambda>s. nat n - nat (s ''y'')"])
   14.69 +apply(rule Semi)
   14.70 +prefer 2
   14.71 +apply(rule Assign)
   14.72 +apply(rule Assign')
   14.73 +apply (simp add: atLeastAtMostPlus1_int_conv algebra_simps)
   14.74 +apply clarsimp
   14.75 +apply arith
   14.76 +apply fastsimp
   14.77 +apply(rule Semi)
   14.78 +prefer 2
   14.79 +apply(rule Assign)
   14.80 +apply(rule Assign')
   14.81 +apply simp
   14.82 +done
   14.83 +
   14.84 +
   14.85 +text{* The soundness theorem: *}
   14.86 +
   14.87 +theorem hoaret_sound: "\<turnstile>\<^sub>t {P}c{Q}  \<Longrightarrow>  \<Turnstile>\<^sub>t {P}c{Q}"
   14.88 +proof(unfold hoare_tvalid_def, induct rule: hoaret.induct)
   14.89 +  case (While P b f c)
   14.90 +  show ?case
   14.91 +  proof
   14.92 +    fix s
   14.93 +    show "P s \<longrightarrow> (\<exists>t. (WHILE b DO c, s) \<Rightarrow> t \<and> P t \<and> \<not> bval b t)"
   14.94 +    proof(induct "f s" arbitrary: s rule: less_induct)
   14.95 +      case (less n)
   14.96 +      thus ?case by (metis While(2) WhileFalse WhileTrue)
   14.97 +    qed
   14.98 +  qed
   14.99 +next
  14.100 +  case If thus ?case by auto blast
  14.101 +qed fastsimp+
  14.102 +
  14.103 +
  14.104 +text{*
  14.105 +The completeness proof proceeds along the same lines as the one for partial
  14.106 +correctness. First we have to strengthen our notion of weakest precondition
  14.107 +to take termination into account: *}
  14.108 +
  14.109 +definition wpt :: "com \<Rightarrow> assn \<Rightarrow> assn" ("wp\<^sub>t") where
  14.110 +"wp\<^sub>t c Q  \<equiv>  \<lambda>s. \<exists>t. (c,s) \<Rightarrow> t \<and> Q t"
  14.111 +
  14.112 +lemma [simp]: "wp\<^sub>t SKIP Q = Q"
  14.113 +by(auto intro!: ext simp: wpt_def)
  14.114 +
  14.115 +lemma [simp]: "wp\<^sub>t (x ::= e) Q = (\<lambda>s. Q(s(x := aval e s)))"
  14.116 +by(auto intro!: ext simp: wpt_def)
  14.117 +
  14.118 +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)"
  14.119 +unfolding wpt_def
  14.120 +apply(rule ext)
  14.121 +apply auto
  14.122 +done
  14.123 +
  14.124 +lemma [simp]:
  14.125 + "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)"
  14.126 +apply(unfold wpt_def)
  14.127 +apply(rule ext)
  14.128 +apply auto
  14.129 +done
  14.130 +
  14.131 +
  14.132 +text{* Now we define the number of iterations @{term "WHILE b DO c"} needs to
  14.133 +terminate when started in state @{text s}. Because this is a truly partial
  14.134 +function, we define it as an (inductive) relation first: *}
  14.135 +
  14.136 +inductive Its :: "bexp \<Rightarrow> com \<Rightarrow> state \<Rightarrow> nat \<Rightarrow> bool" where
  14.137 +Its_0: "\<not> bval b s \<Longrightarrow> Its b c s 0" |
  14.138 +Its_Suc: "\<lbrakk> bval b s;  (c,s) \<Rightarrow> s';  Its b c s' n \<rbrakk> \<Longrightarrow> Its b c s (Suc n)"
  14.139 +
  14.140 +text{* The relation is in fact a function: *}
  14.141 +
  14.142 +lemma Its_fun: "Its b c s n \<Longrightarrow> Its b c s n' \<Longrightarrow> n=n'"
  14.143 +proof(induct arbitrary: n' rule:Its.induct)
  14.144 +(* new release:
  14.145 +  case Its_0 thus ?case by(metis Its.cases)
  14.146 +next
  14.147 +  case Its_Suc thus ?case by(metis Its.cases big_step_determ)
  14.148 +qed
  14.149 +*)
  14.150 +  case Its_0
  14.151 +  from this(1) Its.cases[OF this(2)] show ?case by metis
  14.152 +next
  14.153 +  case (Its_Suc b s c s' n n')
  14.154 +  note C = this
  14.155 +  from this(5) show ?case
  14.156 +  proof cases
  14.157 +    case Its_0 with Its_Suc(1) show ?thesis by blast
  14.158 +  next
  14.159 +    case Its_Suc with C show ?thesis by(metis big_step_determ)
  14.160 +  qed
  14.161 +qed
  14.162 +
  14.163 +text{* For all terminating loops, @{const Its} yields a result: *}
  14.164 +
  14.165 +lemma WHILE_Its: "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> \<exists>n. Its b c s n"
  14.166 +proof(induct "WHILE b DO c" s t rule: big_step_induct)
  14.167 +  case WhileFalse thus ?case by (metis Its_0)
  14.168 +next
  14.169 +  case WhileTrue thus ?case by (metis Its_Suc)
  14.170 +qed
  14.171 +
  14.172 +text{* Now the relation is turned into a function with the help of
  14.173 +the description operator @{text THE}: *}
  14.174 +
  14.175 +definition its :: "bexp \<Rightarrow> com \<Rightarrow> state \<Rightarrow> nat" where
  14.176 +"its b c s = (THE n. Its b c s n)"
  14.177 +
  14.178 +text{* The key property: every loop iteration increases @{const its} by 1. *}
  14.179 +
  14.180 +lemma its_Suc: "\<lbrakk> bval b s; (c, s) \<Rightarrow> s'; (WHILE b DO c, s') \<Rightarrow> t\<rbrakk>
  14.181 +       \<Longrightarrow> its b c s = Suc(its b c s')"
  14.182 +by (metis its_def WHILE_Its Its.intros(2) Its_fun the_equality)
  14.183 +
  14.184 +lemma wpt_is_pre: "\<turnstile>\<^sub>t {wp\<^sub>t c Q} c {Q}"
  14.185 +proof (induct c arbitrary: Q)
  14.186 +  case SKIP show ?case by simp (blast intro:hoaret.Skip)
  14.187 +next
  14.188 +  case Assign show ?case by simp (blast intro:hoaret.Assign)
  14.189 +next
  14.190 +  case Semi thus ?case by simp (blast intro:hoaret.Semi)
  14.191 +next
  14.192 +  case If thus ?case by simp (blast intro:hoaret.If hoaret.conseq)
  14.193 +next
  14.194 +  case (While b c)
  14.195 +  let ?w = "WHILE b DO c"
  14.196 +  { fix n
  14.197 +    have "\<forall>s. wp\<^sub>t ?w Q s \<and> bval b s \<and> its b c s = n \<longrightarrow>
  14.198 +              wp\<^sub>t c (\<lambda>s'. wp\<^sub>t ?w Q s' \<and> its b c s' < n) s"
  14.199 +      unfolding wpt_def by (metis WhileE its_Suc lessI)
  14.200 +    note strengthen_pre[OF this While]
  14.201 +  } note hoaret.While[OF this]
  14.202 +  moreover have "\<forall>s. wp\<^sub>t ?w Q s \<and> \<not> bval b s \<longrightarrow> Q s" by (auto simp add:wpt_def)
  14.203 +  ultimately show ?case by(rule weaken_post)
  14.204 +qed
  14.205 +
  14.206 +
  14.207 +text{*\noindent In the @{term While}-case, @{const its} provides the obvious
  14.208 +termination argument.
  14.209 +
  14.210 +The actual completeness theorem follows directly, in the same manner
  14.211 +as for partial correctness: *}
  14.212 +
  14.213 +theorem hoaret_complete: "\<Turnstile>\<^sub>t {P}c{Q} \<Longrightarrow> \<turnstile>\<^sub>t {P}c{Q}"
  14.214 +apply(rule strengthen_pre[OF _ wpt_is_pre])
  14.215 +apply(auto simp: hoare_tvalid_def hoare_valid_def wpt_def)
  14.216 +done
  14.217 +
  14.218 +end
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/src/HOL/IMP/Hoare_Examples.thy	Mon Jun 06 16:29:38 2011 +0200
    15.3 @@ -0,0 +1,78 @@
    15.4 +(* Author: Tobias Nipkow *)
    15.5 +
    15.6 +theory Hoare_Examples imports Hoare Util begin
    15.7 +
    15.8 +subsection{* Example: Sums *}
    15.9 +
   15.10 +text{* Summing up the first @{text n} natural numbers. The sum is accumulated
   15.11 +in variable @{text 0}, the loop counter is variable @{text 1}. *}
   15.12 +
   15.13 +abbreviation "w n ==
   15.14 +  WHILE Less (V ''y'') (N n)
   15.15 +  DO ( ''y'' ::= Plus (V ''y'') (N 1); ''x'' ::= Plus (V ''x'') (V ''y'') )"
   15.16 +
   15.17 +text{* For this example we make use of some predefined functions.  Function
   15.18 +@{const Setsum}, also written @{text"\<Sum>"}, sums up the elements of a set. The
   15.19 +set of numbers from @{text m} to @{text n} is written @{term "{m .. n}"}. *}
   15.20 +
   15.21 +subsubsection{* Proof by Operational Semantics *}
   15.22 +
   15.23 +text{* The behaviour of the loop is proved by induction: *}
   15.24 +
   15.25 +lemma setsum_head_plus_1:
   15.26 +  "m \<le> n \<Longrightarrow> setsum f {m..n} = f m + setsum f {m+1..n::int}"
   15.27 +by (subst simp_from_to) simp
   15.28 +  
   15.29 +lemma while_sum:
   15.30 +  "(w n, s) \<Rightarrow> t \<Longrightarrow> t ''x'' = s ''x'' + \<Sum> {s ''y'' + 1 .. n}"
   15.31 +apply(induct "w n" s t rule: big_step_induct)
   15.32 +apply(auto simp add: setsum_head_plus_1)
   15.33 +done
   15.34 +
   15.35 +text{* We were lucky that the proof was practically automatic, except for the
   15.36 +induction. In general, such proofs will not be so easy. The automation is
   15.37 +partly due to the right inversion rules that we set up as automatic
   15.38 +elimination rules that decompose big-step premises.
   15.39 +
   15.40 +Now we prefix the loop with the necessary initialization: *}
   15.41 +
   15.42 +lemma sum_via_bigstep:
   15.43 +assumes "(''x'' ::= N 0; ''y'' ::= N 0; w n, s) \<Rightarrow> t"
   15.44 +shows "t ''x'' = \<Sum> {1 .. n}"
   15.45 +proof -
   15.46 +  from assms have "(w n,s(''x'':=0,''y'':=0)) \<Rightarrow> t" by auto
   15.47 +  from while_sum[OF this] show ?thesis by simp
   15.48 +qed
   15.49 +
   15.50 +
   15.51 +subsubsection{* Proof by Hoare Logic *}
   15.52 +
   15.53 +text{* Note that we deal with sequences of commands from right to left,
   15.54 +pulling back the postcondition towards the precondition. *}
   15.55 +
   15.56 +lemma "\<turnstile> {\<lambda>s. 0 <= n} ''x'' ::= N 0; ''y'' ::= N 0; w n {\<lambda>s. s ''x'' = \<Sum> {1 .. n}}"
   15.57 +apply(rule hoare.Semi)
   15.58 +prefer 2
   15.59 +apply(rule While'
   15.60 +  [where P = "\<lambda>s. s ''x'' = \<Sum> {1..s ''y''} \<and> 0 \<le> s ''y'' \<and> s ''y'' \<le> n"])
   15.61 +apply(rule Semi)
   15.62 +prefer 2
   15.63 +apply(rule Assign)
   15.64 +apply(rule Assign')
   15.65 +apply(fastsimp simp: atLeastAtMostPlus1_int_conv algebra_simps)
   15.66 +apply(fastsimp)
   15.67 +apply(rule Semi)
   15.68 +prefer 2
   15.69 +apply(rule Assign)
   15.70 +apply(rule Assign')
   15.71 +apply simp
   15.72 +done
   15.73 +
   15.74 +text{* The proof is intentionally an apply skript because it merely composes
   15.75 +the rules of Hoare logic. Of course, in a few places side conditions have to
   15.76 +be proved. But since those proofs are 1-liners, a structured proof is
   15.77 +overkill. In fact, we shall learn later that the application of the Hoare
   15.78 +rules can be automated completely and all that is left for the user is to
   15.79 +provide the loop invariants and prove the side-conditions. *}
   15.80 +
   15.81 +end
    16.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.2 +++ b/src/HOL/IMP/Hoare_Sound_Complete.thy	Mon Jun 06 16:29:38 2011 +0200
    16.3 @@ -0,0 +1,101 @@
    16.4 +(* Author: Tobias Nipkow *)
    16.5 +
    16.6 +theory Hoare_Sound_Complete imports Hoare begin
    16.7 +
    16.8 +subsection "Soundness"
    16.9 +
   16.10 +definition
   16.11 +hoare_valid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<Turnstile> {(1_)}/ (_)/ {(1_)}" 50) where
   16.12 +"\<Turnstile> {P}c{Q} = (\<forall>s t. (c,s) \<Rightarrow> t  \<longrightarrow>  P s \<longrightarrow>  Q t)"
   16.13 +
   16.14 +lemma hoare_sound: "\<turnstile> {P}c{Q}  \<Longrightarrow>  \<Turnstile> {P}c{Q}"
   16.15 +proof(induct rule: hoare.induct)
   16.16 +  case (While P b c)
   16.17 +  { fix s t
   16.18 +    have "(WHILE b DO c,s) \<Rightarrow> t  \<Longrightarrow>  P s \<longrightarrow> P t \<and> \<not> bval b t"
   16.19 +    proof(induct "WHILE b DO c" s t rule: big_step_induct)
   16.20 +      case WhileFalse thus ?case by blast
   16.21 +    next
   16.22 +      case WhileTrue thus ?case
   16.23 +        using While(2) unfolding hoare_valid_def by blast
   16.24 +    qed
   16.25 +  }
   16.26 +  thus ?case unfolding hoare_valid_def by blast
   16.27 +qed (auto simp: hoare_valid_def)
   16.28 +
   16.29 +
   16.30 +subsection "Weakest Precondition"
   16.31 +
   16.32 +definition wp :: "com \<Rightarrow> assn \<Rightarrow> assn" where
   16.33 +"wp c Q = (\<lambda>s. \<forall>t. (c,s) \<Rightarrow> t  \<longrightarrow>  Q t)"
   16.34 +
   16.35 +lemma wp_SKIP[simp]: "wp SKIP Q = Q"
   16.36 +by (rule ext) (auto simp: wp_def)
   16.37 +
   16.38 +lemma wp_Ass[simp]: "wp (x::=a) Q = (\<lambda>s. Q(s[a/x]))"
   16.39 +by (rule ext) (auto simp: wp_def)
   16.40 +
   16.41 +lemma wp_Semi[simp]: "wp (c\<^isub>1;c\<^isub>2) Q = wp c\<^isub>1 (wp c\<^isub>2 Q)"
   16.42 +by (rule ext) (auto simp: wp_def)
   16.43 +
   16.44 +lemma wp_If[simp]:
   16.45 + "wp (IF b THEN c\<^isub>1 ELSE c\<^isub>2) Q =
   16.46 + (\<lambda>s. (bval b s \<longrightarrow> wp c\<^isub>1 Q s) \<and>  (\<not> bval b s \<longrightarrow> wp c\<^isub>2 Q s))"
   16.47 +by (rule ext) (auto simp: wp_def)
   16.48 +
   16.49 +lemma wp_While_If:
   16.50 + "wp (WHILE b DO c) Q s =
   16.51 +  wp (IF b THEN c;WHILE b DO c ELSE SKIP) Q s"
   16.52 +unfolding wp_def by (metis unfold_while)
   16.53 +
   16.54 +lemma wp_While_True[simp]: "bval b s \<Longrightarrow>
   16.55 +  wp (WHILE b DO c) Q s = wp (c; WHILE b DO c) Q s"
   16.56 +by(simp add: wp_While_If)
   16.57 +
   16.58 +lemma wp_While_False[simp]: "\<not> bval b s \<Longrightarrow> wp (WHILE b DO c) Q s = Q s"
   16.59 +by(simp add: wp_While_If)
   16.60 +
   16.61 +
   16.62 +subsection "Completeness"
   16.63 +
   16.64 +lemma wp_is_pre: "\<turnstile> {wp c Q} c {Q}"
   16.65 +proof(induct c arbitrary: Q)
   16.66 +  case Semi thus ?case by(auto intro: Semi)
   16.67 +next
   16.68 +  case (If b c1 c2)
   16.69 +  let ?If = "IF b THEN c1 ELSE c2"
   16.70 +  show ?case
   16.71 +  proof(rule hoare.If)
   16.72 +    show "\<turnstile> {\<lambda>s. wp ?If Q s \<and> bval b s} c1 {Q}"
   16.73 +    proof(rule strengthen_pre[OF _ If(1)])
   16.74 +      show "\<forall>s. wp ?If Q s \<and> bval b s \<longrightarrow> wp c1 Q s" by auto
   16.75 +    qed
   16.76 +    show "\<turnstile> {\<lambda>s. wp ?If Q s \<and> \<not> bval b s} c2 {Q}"
   16.77 +    proof(rule strengthen_pre[OF _ If(2)])
   16.78 +      show "\<forall>s. wp ?If Q s \<and> \<not> bval b s \<longrightarrow> wp c2 Q s" by auto
   16.79 +    qed
   16.80 +  qed
   16.81 +next
   16.82 +  case (While b c)
   16.83 +  let ?w = "WHILE b DO c"
   16.84 +  have "\<turnstile> {wp ?w Q} ?w {\<lambda>s. wp ?w Q s \<and> \<not> bval b s}"
   16.85 +  proof(rule hoare.While)
   16.86 +    show "\<turnstile> {\<lambda>s. wp ?w Q s \<and> bval b s} c {wp ?w Q}"
   16.87 +    proof(rule strengthen_pre[OF _ While(1)])
   16.88 +      show "\<forall>s. wp ?w Q s \<and> bval b s \<longrightarrow> wp c (wp ?w Q) s" by auto
   16.89 +    qed
   16.90 +  qed
   16.91 +  thus ?case
   16.92 +  proof(rule weaken_post)
   16.93 +    show "\<forall>s. wp ?w Q s \<and> \<not> bval b s \<longrightarrow> Q s" by auto
   16.94 +  qed
   16.95 +qed auto
   16.96 +
   16.97 +lemma hoare_relative_complete: assumes "\<Turnstile> {P}c{Q}" shows "\<turnstile> {P}c{Q}"
   16.98 +proof(rule strengthen_pre)
   16.99 +  show "\<forall>s. P s \<longrightarrow> wp c Q s" using assms
  16.100 +    by (auto simp: hoare_valid_def wp_def)
  16.101 +  show "\<turnstile> {wp c Q} c {Q}" by(rule wp_is_pre)
  16.102 +qed
  16.103 +
  16.104 +end
    17.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.2 +++ b/src/HOL/IMP/Live.thy	Mon Jun 06 16:29:38 2011 +0200
    17.3 @@ -0,0 +1,249 @@
    17.4 +(* Author: Tobias Nipkow *)
    17.5 +
    17.6 +header "Live Variable Analysis"
    17.7 +
    17.8 +theory Live imports Vars Big_Step
    17.9 +begin
   17.10 +
   17.11 +subsection "Liveness Analysis"
   17.12 +
   17.13 +fun L :: "com \<Rightarrow> name set \<Rightarrow> name set" where
   17.14 +"L SKIP X = X" |
   17.15 +"L (x ::= a) X = X-{x} \<union> vars a" |
   17.16 +"L (c\<^isub>1; c\<^isub>2) X = (L c\<^isub>1 \<circ> L c\<^isub>2) X" |
   17.17 +"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" |
   17.18 +"L (WHILE b DO c) X = vars b \<union> X \<union> L c X"
   17.19 +
   17.20 +value "show (L (''y'' ::= V ''z''; ''x'' ::= Plus (V ''y'') (V ''z'')) {''x''})"
   17.21 +
   17.22 +value "show (L (WHILE Less (V ''x'') (V ''x'') DO ''y'' ::= V ''z'') {''x''})"
   17.23 +
   17.24 +fun "kill" :: "com \<Rightarrow> name set" where
   17.25 +"kill SKIP = {}" |
   17.26 +"kill (x ::= a) = {x}" |
   17.27 +"kill (c\<^isub>1; c\<^isub>2) = kill c\<^isub>1 \<union> kill c\<^isub>2" |
   17.28 +"kill (IF b THEN c\<^isub>1 ELSE c\<^isub>2) = kill c\<^isub>1 \<inter> kill c\<^isub>2" |
   17.29 +"kill (WHILE b DO c) = {}"
   17.30 +
   17.31 +fun gen :: "com \<Rightarrow> name set" where
   17.32 +"gen SKIP = {}" |
   17.33 +"gen (x ::= a) = vars a" |
   17.34 +"gen (c\<^isub>1; c\<^isub>2) = gen c\<^isub>1 \<union> (gen c\<^isub>2 - kill c\<^isub>1)" |
   17.35 +"gen (IF b THEN c\<^isub>1 ELSE c\<^isub>2) = vars b \<union> gen c\<^isub>1 \<union> gen c\<^isub>2" |
   17.36 +"gen (WHILE b DO c) = vars b \<union> gen c"
   17.37 +
   17.38 +lemma L_gen_kill: "L c X = (X - kill c) \<union> gen c"
   17.39 +by(induct c arbitrary:X) auto
   17.40 +
   17.41 +lemma L_While_subset: "L c (L (WHILE b DO c) X) \<subseteq> L (WHILE b DO c) X"
   17.42 +by(auto simp add:L_gen_kill)
   17.43 +
   17.44 +
   17.45 +subsection "Soundness"
   17.46 +
   17.47 +theorem L_sound:
   17.48 +  "(c,s) \<Rightarrow> s'  \<Longrightarrow> s = t on L c X \<Longrightarrow>
   17.49 +  \<exists> t'. (c,t) \<Rightarrow> t' & s' = t' on X"
   17.50 +proof (induct arbitrary: X t rule: big_step_induct)
   17.51 +  case Skip then show ?case by auto
   17.52 +next
   17.53 +  case Assign then show ?case
   17.54 +    by (auto simp: ball_Un)
   17.55 +next
   17.56 +  case (Semi c1 s1 s2 c2 s3 X t1)
   17.57 +  from Semi(2,5) obtain t2 where
   17.58 +    t12: "(c1, t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X"
   17.59 +    by simp blast
   17.60 +  from Semi(4)[OF s2t2] obtain t3 where
   17.61 +    t23: "(c2, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
   17.62 +    by auto
   17.63 +  show ?case using t12 t23 s3t3 by auto
   17.64 +next
   17.65 +  case (IfTrue b s c1 s' c2)
   17.66 +  hence "s = t on vars b" "s = t on L c1 X" by auto
   17.67 +  from  bval_eq_if_eq_on_vars[OF this(1)] IfTrue(1) have "bval b t" by simp
   17.68 +  from IfTrue(3)[OF `s = t on L c1 X`] obtain t' where
   17.69 +    "(c1, t) \<Rightarrow> t'" "s' = t' on X" by auto
   17.70 +  thus ?case using `bval b t` by auto
   17.71 +next
   17.72 +  case (IfFalse b s c2 s' c1)
   17.73 +  hence "s = t on vars b" "s = t on L c2 X" by auto
   17.74 +  from  bval_eq_if_eq_on_vars[OF this(1)] IfFalse(1) have "~bval b t" by simp
   17.75 +  from IfFalse(3)[OF `s = t on L c2 X`] obtain t' where
   17.76 +    "(c2, t) \<Rightarrow> t'" "s' = t' on X" by auto
   17.77 +  thus ?case using `~bval b t` by auto
   17.78 +next
   17.79 +  case (WhileFalse b s c)
   17.80 +  hence "~ bval b t" by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
   17.81 +  thus ?case using WhileFalse(2) by auto
   17.82 +next
   17.83 +  case (WhileTrue b s1 c s2 s3 X t1)
   17.84 +  let ?w = "WHILE b DO c"
   17.85 +  from `bval b s1` WhileTrue(6) have "bval b t1"
   17.86 +    by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
   17.87 +  have "s1 = t1 on L c (L ?w X)" using  L_While_subset WhileTrue.prems
   17.88 +    by (blast)
   17.89 +  from WhileTrue(3)[OF this] obtain t2 where
   17.90 +    "(c, t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto
   17.91 +  from WhileTrue(5)[OF this(2)] obtain t3 where "(?w,t2) \<Rightarrow> t3" "s3 = t3 on X"
   17.92 +    by auto
   17.93 +  with `bval b t1` `(c, t1) \<Rightarrow> t2` show ?case by auto
   17.94 +qed
   17.95 +
   17.96 +
   17.97 +subsection "Program Optimization"
   17.98 +
   17.99 +text{* Burying assignments to dead variables: *}
  17.100 +fun bury :: "com \<Rightarrow> name set \<Rightarrow> com" where
  17.101 +"bury SKIP X = SKIP" |
  17.102 +"bury (x ::= a) X = (if x:X then x::= a else SKIP)" |
  17.103 +"bury (c\<^isub>1; c\<^isub>2) X = (bury c\<^isub>1 (L c\<^isub>2 X); bury c\<^isub>2 X)" |
  17.104 +"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" |
  17.105 +"bury (WHILE b DO c) X = WHILE b DO bury c (vars b \<union> X \<union> L c X)"
  17.106 +
  17.107 +text{* We could prove the analogous lemma to @{thm[source]L_sound}, and the
  17.108 +proof would be very similar. However, we phrase it as a semantics
  17.109 +preservation property: *}
  17.110 +
  17.111 +theorem bury_sound:
  17.112 +  "(c,s) \<Rightarrow> s'  \<Longrightarrow> s = t on L c X \<Longrightarrow>
  17.113 +  \<exists> t'. (bury c X,t) \<Rightarrow> t' & s' = t' on X"
  17.114 +proof (induct arbitrary: X t rule: big_step_induct)
  17.115 +  case Skip then show ?case by auto
  17.116 +next
  17.117 +  case Assign then show ?case
  17.118 +    by (auto simp: ball_Un)
  17.119 +next
  17.120 +  case (Semi c1 s1 s2 c2 s3 X t1)
  17.121 +  from Semi(2,5) obtain t2 where
  17.122 +    t12: "(bury c1 (L c2 X), t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X"
  17.123 +    by simp blast
  17.124 +  from Semi(4)[OF s2t2] obtain t3 where
  17.125 +    t23: "(bury c2 X, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
  17.126 +    by auto
  17.127 +  show ?case using t12 t23 s3t3 by auto
  17.128 +next
  17.129 +  case (IfTrue b s c1 s' c2)
  17.130 +  hence "s = t on vars b" "s = t on L c1 X" by auto
  17.131 +  from  bval_eq_if_eq_on_vars[OF this(1)] IfTrue(1) have "bval b t" by simp
  17.132 +  from IfTrue(3)[OF `s = t on L c1 X`] obtain t' where
  17.133 +    "(bury c1 X, t) \<Rightarrow> t'" "s' =t' on X" by auto
  17.134 +  thus ?case using `bval b t` by auto
  17.135 +next
  17.136 +  case (IfFalse b s c2 s' c1)
  17.137 +  hence "s = t on vars b" "s = t on L c2 X" by auto
  17.138 +  from  bval_eq_if_eq_on_vars[OF this(1)] IfFalse(1) have "~bval b t" by simp
  17.139 +  from IfFalse(3)[OF `s = t on L c2 X`] obtain t' where
  17.140 +    "(bury c2 X, t) \<Rightarrow> t'" "s' = t' on X" by auto
  17.141 +  thus ?case using `~bval b t` by auto
  17.142 +next
  17.143 +  case (WhileFalse b s c)
  17.144 +  hence "~ bval b t" by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
  17.145 +  thus ?case using WhileFalse(2) by auto
  17.146 +next
  17.147 +  case (WhileTrue b s1 c s2 s3 X t1)
  17.148 +  let ?w = "WHILE b DO c"
  17.149 +  from `bval b s1` WhileTrue(6) have "bval b t1"
  17.150 +    by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
  17.151 +  have "s1 = t1 on L c (L ?w X)"
  17.152 +    using L_While_subset WhileTrue.prems by blast
  17.153 +  from WhileTrue(3)[OF this] obtain t2 where
  17.154 +    "(bury c (L ?w X), t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto
  17.155 +  from WhileTrue(5)[OF this(2)] obtain t3
  17.156 +    where "(bury ?w X,t2) \<Rightarrow> t3" "s3 = t3 on X"
  17.157 +    by auto
  17.158 +  with `bval b t1` `(bury c (L ?w X), t1) \<Rightarrow> t2` show ?case by auto
  17.159 +    (* FIXME why does s/h fail here? *)
  17.160 +qed
  17.161 +
  17.162 +corollary final_bury_sound: "(c,s) \<Rightarrow> s' \<Longrightarrow> (bury c UNIV,s) \<Rightarrow> s'"
  17.163 +using bury_sound[of c s s' UNIV]
  17.164 +by (auto simp: fun_eq_iff[symmetric])
  17.165 +
  17.166 +text{* Now the opposite direction. *}
  17.167 +
  17.168 +lemma SKIP_bury[simp]:
  17.169 +  "SKIP = bury c X \<longleftrightarrow> c = SKIP | (EX x a. c = x::=a & x \<notin> X)"
  17.170 +by (cases c) auto
  17.171 +
  17.172 +lemma Assign_bury[simp]: "x::=a = bury c X \<longleftrightarrow> c = x::=a & x : X"
  17.173 +by (cases c) auto
  17.174 +
  17.175 +lemma Semi_bury[simp]: "bc\<^isub>1;bc\<^isub>2 = bury c X \<longleftrightarrow>
  17.176 +  (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))"
  17.177 +by (cases c) auto
  17.178 +
  17.179 +lemma If_bury[simp]: "IF b THEN bc1 ELSE bc2 = bury c X \<longleftrightarrow>
  17.180 +  (EX c1 c2. c = IF b THEN c1 ELSE c2 &
  17.181 +     bc1 = bury c1 X & bc2 = bury c2 X)"
  17.182 +by (cases c) auto
  17.183 +
  17.184 +lemma While_bury[simp]: "WHILE b DO bc' = bury c X \<longleftrightarrow>
  17.185 +  (EX c'. c = WHILE b DO c' & bc' = bury c' (vars b \<union> X \<union> L c X))"
  17.186 +by (cases c) auto
  17.187 +
  17.188 +theorem bury_sound2:
  17.189 +  "(bury c X,s) \<Rightarrow> s'  \<Longrightarrow> s = t on L c X \<Longrightarrow>
  17.190 +  \<exists> t'. (c,t) \<Rightarrow> t' & s' = t' on X"
  17.191 +proof (induct "bury c X" s s' arbitrary: c X t rule: big_step_induct)
  17.192 +  case Skip then show ?case by auto
  17.193 +next
  17.194 +  case Assign then show ?case
  17.195 +    by (auto simp: ball_Un)
  17.196 +next
  17.197 +  case (Semi bc1 s1 s2 bc2 s3 c X t1)
  17.198 +  then obtain c1 c2 where c: "c = c1;c2"
  17.199 +    and bc2: "bc2 = bury c2 X" and bc1: "bc1 = bury c1 (L c2 X)" by auto
  17.200 +  from Semi(2)[OF bc1, of t1] Semi.prems c obtain t2 where
  17.201 +    t12: "(c1, t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X" by auto
  17.202 +  from Semi(4)[OF bc2 s2t2] obtain t3 where
  17.203 +    t23: "(c2, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
  17.204 +    by auto
  17.205 +  show ?case using c t12 t23 s3t3 by auto
  17.206 +next
  17.207 +  case (IfTrue b s bc1 s' bc2)
  17.208 +  then obtain c1 c2 where c: "c = IF b THEN c1 ELSE c2"
  17.209 +    and bc1: "bc1 = bury c1 X" and bc2: "bc2 = bury c2 X" by auto
  17.210 +  have "s = t on vars b" "s = t on L c1 X" using IfTrue.prems c by auto
  17.211 +  from bval_eq_if_eq_on_vars[OF this(1)] IfTrue(1) have "bval b t" by simp
  17.212 +  from IfTrue(3)[OF bc1 `s = t on L c1 X`] obtain t' where
  17.213 +    "(c1, t) \<Rightarrow> t'" "s' =t' on X" by auto
  17.214 +  thus ?case using c `bval b t` by auto
  17.215 +next
  17.216 +  case (IfFalse b s bc2 s' bc1)
  17.217 +  then obtain c1 c2 where c: "c = IF b THEN c1 ELSE c2"
  17.218 +    and bc1: "bc1 = bury c1 X" and bc2: "bc2 = bury c2 X" by auto
  17.219 +  have "s = t on vars b" "s = t on L c2 X" using IfFalse.prems c by auto
  17.220 +  from bval_eq_if_eq_on_vars[OF this(1)] IfFalse(1) have "~bval b t" by simp
  17.221 +  from IfFalse(3)[OF bc2 `s = t on L c2 X`] obtain t' where
  17.222 +    "(c2, t) \<Rightarrow> t'" "s' =t' on X" by auto
  17.223 +  thus ?case using c `~bval b t` by auto
  17.224 +next
  17.225 +  case (WhileFalse b s c)
  17.226 +  hence "~ bval b t" by (auto simp: ball_Un dest: bval_eq_if_eq_on_vars)
  17.227 +  thus ?case using WhileFalse by auto
  17.228 +next
  17.229 +  case (WhileTrue b s1 bc' s2 s3 c X t1)
  17.230 +  then obtain c' where c: "c = WHILE b DO c'"
  17.231 +    and bc': "bc' = bury c' (vars b \<union> X \<union> L c' X)" by auto
  17.232 +  let ?w = "WHILE b DO c'"
  17.233 +  from `bval b s1` WhileTrue.prems c have "bval b t1"
  17.234 +    by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
  17.235 +  have "s1 = t1 on L c' (L ?w X)"
  17.236 +    using L_While_subset WhileTrue.prems c by blast
  17.237 +  with WhileTrue(3)[OF bc', of t1] obtain t2 where
  17.238 +    "(c', t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto
  17.239 +  from WhileTrue(5)[OF WhileTrue(6), of t2] c this(2) obtain t3
  17.240 +    where "(?w,t2) \<Rightarrow> t3" "s3 = t3 on X"
  17.241 +    by auto
  17.242 +  with `bval b t1` `(c', t1) \<Rightarrow> t2` c show ?case by auto
  17.243 +qed
  17.244 +
  17.245 +corollary final_bury_sound2: "(bury c UNIV,s) \<Rightarrow> s' \<Longrightarrow> (c,s) \<Rightarrow> s'"
  17.246 +using bury_sound2[of c UNIV]
  17.247 +by (auto simp: fun_eq_iff[symmetric])
  17.248 +
  17.249 +corollary bury_iff: "(bury c UNIV,s) \<Rightarrow> s' \<longleftrightarrow> (c,s) \<Rightarrow> s'"
  17.250 +by(metis final_bury_sound final_bury_sound2)
  17.251 +
  17.252 +end
    18.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.2 +++ b/src/HOL/IMP/OO.thy	Mon Jun 06 16:29:38 2011 +0200
    18.3 @@ -0,0 +1,114 @@
    18.4 +theory OO imports Main begin
    18.5 +
    18.6 +subsection "Towards an OO Language: A Language of Records"
    18.7 +
    18.8 +(* FIXME: move to HOL/Fun *)
    18.9 +abbreviation fun_upd2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c"
   18.10 +  ("_/'((2_,_ :=/ _)')" [1000,0,0,0] 900)
   18.11 +where "f(x,y := z) == f(x := (f x)(y := z))"
   18.12 +
   18.13 +type_synonym addr = nat
   18.14 +datatype ref = null | Ref addr
   18.15 +
   18.16 +type_synonym obj = "string \<Rightarrow> ref"
   18.17 +type_synonym venv = "string \<Rightarrow> ref"
   18.18 +type_synonym store = "addr \<Rightarrow> obj"
   18.19 +
   18.20 +datatype exp =
   18.21 +  Null |
   18.22 +  New |
   18.23 +  V string |
   18.24 +  Faccess exp string       ("_\<bullet>/_" [63,1000] 63) |
   18.25 +  Vassign string exp       ("(_ ::=/ _)" [1000,61] 62) |
   18.26 +  Fassign exp string exp   ("(_\<bullet>_ ::=/ _)" [63,0,62] 62) |
   18.27 +  Mcall exp string exp     ("(_\<bullet>/_<_>)" [63,0,0] 63) |
   18.28 +  Semi exp exp             ("_;/ _" [61,60] 60) |
   18.29 +  If bexp exp exp          ("IF _/ THEN (2_)/ ELSE (2_)" [0,0,61] 61)
   18.30 +and bexp = B bool | Not bexp | And bexp bexp | Eq exp exp
   18.31 +
   18.32 +type_synonym menv = "string \<Rightarrow> exp"
   18.33 +type_synonym config = "venv \<times> store \<times> addr"
   18.34 +
   18.35 +inductive
   18.36 +  big_step :: "menv \<Rightarrow> exp \<times> config \<Rightarrow> ref \<times> config \<Rightarrow> bool"
   18.37 +    ("(_ \<turnstile>/ (_/ \<Rightarrow> _))" [60,0,60] 55) and
   18.38 +  bval ::  "menv \<Rightarrow> bexp \<times> config \<Rightarrow> bool \<times> config \<Rightarrow> bool"
   18.39 +    ("_ \<turnstile> _ \<rightarrow> _" [60,0,60] 55)
   18.40 +where
   18.41 +Null:
   18.42 +"me \<turnstile> (Null,c) \<Rightarrow> (null,c)" |
   18.43 +New:
   18.44 +"me \<turnstile> (New,ve,s,n) \<Rightarrow> (Ref n,ve,s(n := (\<lambda>f. null)),n+1)" |
   18.45 +Vaccess:
   18.46 +"me \<turnstile> (V x,ve,sn) \<Rightarrow> (ve x,ve,sn)" |
   18.47 +Faccess:
   18.48 +"me \<turnstile> (e,c) \<Rightarrow> (Ref a,ve',s',n') \<Longrightarrow>
   18.49 + me \<turnstile> (e\<bullet>f,c) \<Rightarrow> (s' a f,ve',s',n')" |
   18.50 +Vassign:
   18.51 +"me \<turnstile> (e,c) \<Rightarrow> (r,ve',sn') \<Longrightarrow>
   18.52 + me \<turnstile> (x ::= e,c) \<Rightarrow> (r,ve'(x:=r),sn')" |
   18.53 +Fassign:
   18.54 +"\<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>
   18.55 + me \<turnstile> (oe\<bullet>f ::= e,c\<^isub>1) \<Rightarrow> (r,ve\<^isub>3,s\<^isub>3(a,f := r),n\<^isub>3)" |
   18.56 +Mcall:
   18.57 +"\<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);
   18.58 +   ve = (\<lambda>x. null)(''this'' := or, ''param'' := pr);
   18.59 +   me \<turnstile> (me m,ve,sn\<^isub>3) \<Rightarrow> (r,ve',sn\<^isub>4) \<rbrakk>
   18.60 +  \<Longrightarrow>
   18.61 + me \<turnstile> (oe\<bullet>m<pe>,c\<^isub>1) \<Rightarrow> (r,ve\<^isub>3,sn\<^isub>4)" |
   18.62 +Semi:
   18.63 +"\<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>
   18.64 + me \<turnstile> (e\<^isub>1; e\<^isub>2,c\<^isub>1) \<Rightarrow> c\<^isub>3" |
   18.65 +IfTrue:
   18.66 +"\<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>
   18.67 + me \<turnstile> (IF b THEN e\<^isub>1 ELSE e\<^isub>2,c\<^isub>1) \<Rightarrow> c\<^isub>3" |
   18.68 +IfFalse:
   18.69 +"\<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>
   18.70 + me \<turnstile> (IF b THEN e\<^isub>1 ELSE e\<^isub>2,c\<^isub>1) \<Rightarrow> c\<^isub>3" |
   18.71 +
   18.72 +"me \<turnstile> (B bv,c) \<rightarrow> (bv,c)" |
   18.73 +
   18.74 +"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)" |
   18.75 +
   18.76 +"\<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>
   18.77 + me \<turnstile> (And b\<^isub>1 b\<^isub>2,c\<^isub>1) \<rightarrow> (bv\<^isub>1\<and>bv\<^isub>2,c\<^isub>3)" |
   18.78 +
   18.79 +"\<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>
   18.80 + me \<turnstile> (Eq e\<^isub>1 e\<^isub>2,c\<^isub>1) \<rightarrow> (r\<^isub>1=r\<^isub>2,c\<^isub>3)"
   18.81 +
   18.82 +
   18.83 +code_pred (modes: i => i => o => bool) big_step .
   18.84 +
   18.85 +text{* Example: natural numbers encoded as objects with a predecessor
   18.86 +field. Null is zero. Method succ adds an object in front, method add
   18.87 +adds as many objects in front as the parameter specifies.
   18.88 +
   18.89 +First, the method bodies: *}
   18.90 +
   18.91 +definition
   18.92 +"m_succ  =  (''s'' ::= New)\<bullet>''pred'' ::= V ''this''; V ''s''"
   18.93 +
   18.94 +definition "m_add =
   18.95 +  IF Eq (V ''param'') Null
   18.96 +  THEN V ''this''
   18.97 +  ELSE V ''this''\<bullet>''succ''<Null>\<bullet>''add''<V ''param''\<bullet>''pred''>"
   18.98 +
   18.99 +text{* The method environment: *}
  18.100 +definition
  18.101 +"menv = (\<lambda>m. Null)(''succ'' := m_succ, ''add'' := m_add)"
  18.102 +
  18.103 +text{* The main code, adding 1 and 2: *}
  18.104 +definition "main =
  18.105 +  ''1'' ::= Null\<bullet>''succ''<Null>;
  18.106 +  ''2'' ::= V ''1''\<bullet>''succ''<Null>;
  18.107 +  V ''2'' \<bullet> ''add'' <V ''1''>"
  18.108 +
  18.109 +text{* Execution of semantics. The final variable environment and store are
  18.110 +converted into lists of references based on given lists of variable and field
  18.111 +names to extract. *}
  18.112 +
  18.113 +values
  18.114 + "{(r, map ve' [''1'',''2''], map (\<lambda>n. map (s' n)[''pred'']) [0..<n])|
  18.115 +    r ve' s' n. menv \<turnstile> (main, \<lambda>x. null, nth[], 0) \<Rightarrow> (r,ve',s',n)}"
  18.116 +
  18.117 +end
    19.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.2 +++ b/src/HOL/IMP/Procs.thy	Mon Jun 06 16:29:38 2011 +0200
    19.3 @@ -0,0 +1,27 @@
    19.4 +header "Extensions and Variations of IMP"
    19.5 +
    19.6 +theory Procs imports BExp begin
    19.7 +
    19.8 +subsection "Procedures and Local Variables"
    19.9 +
   19.10 +datatype
   19.11 +  com = SKIP 
   19.12 +      | Assign name aexp         ("_ ::= _" [1000, 61] 61)
   19.13 +      | Semi   com  com          ("_;/ _"  [60, 61] 60)
   19.14 +      | If     bexp com com     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61)
   19.15 +      | While  bexp com         ("(WHILE _/ DO _)"  [0, 61] 61)
   19.16 +      | Var    name com         ("(1{VAR _;;/ _})")
   19.17 +      | Proc   name com com     ("(1{PROC _ = _;;/ _})")
   19.18 +      | CALL   name
   19.19 +
   19.20 +definition "test_com =
   19.21 +{VAR ''x'';;
   19.22 + ''x'' ::= N 0;
   19.23 + {PROC ''p'' = ''x'' ::= Plus (V ''x'') (V ''x'');;
   19.24 +  {PROC ''q'' = CALL ''p'';;
   19.25 +   {VAR ''x'';;
   19.26 +    ''x'' ::= N 5;
   19.27 +    {PROC ''p'' = ''x'' ::= Plus (V ''x'') (N 1);;
   19.28 +     CALL ''q''; ''y'' ::= V ''x''}}}}}"
   19.29 +
   19.30 +end
    20.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.2 +++ b/src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy	Mon Jun 06 16:29:38 2011 +0200
    20.3 @@ -0,0 +1,40 @@
    20.4 +theory Procs_Dyn_Vars_Dyn imports Util Procs
    20.5 +begin
    20.6 +
    20.7 +subsubsection "Dynamic Scoping of Procedures and Variables"
    20.8 +
    20.9 +type_synonym penv = "name \<Rightarrow> com"
   20.10 +
   20.11 +inductive
   20.12 +  big_step :: "penv \<Rightarrow> com \<times> state \<Rightarrow> state \<Rightarrow> bool" ("_ \<turnstile> _ \<Rightarrow> _" [60,0,60] 55)
   20.13 +where
   20.14 +Skip:    "pe \<turnstile> (SKIP,s) \<Rightarrow> s" |
   20.15 +Assign:  "pe \<turnstile> (x ::= a,s) \<Rightarrow> s(x := aval a s)" |
   20.16 +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>
   20.17 +          pe \<turnstile> (c\<^isub>1;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
   20.18 +
   20.19 +IfTrue:  "\<lbrakk> bval b s;  pe \<turnstile> (c\<^isub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
   20.20 +         pe \<turnstile> (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
   20.21 +IfFalse: "\<lbrakk> \<not>bval b s;  pe \<turnstile> (c\<^isub>2,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
   20.22 +         pe \<turnstile> (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
   20.23 +
   20.24 +WhileFalse: "\<not>bval b s \<Longrightarrow> pe \<turnstile> (WHILE b DO c,s) \<Rightarrow> s" |
   20.25 +WhileTrue:
   20.26 +  "\<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>
   20.27 +   pe \<turnstile> (WHILE b DO c, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
   20.28 +
   20.29 +Var: "pe \<turnstile> (c,s) \<Rightarrow> t  \<Longrightarrow>  pe \<turnstile> ({VAR x;; c}, s) \<Rightarrow> t(x := s x)" |
   20.30 +
   20.31 +Call: "pe \<turnstile> (pe p, s) \<Rightarrow> t  \<Longrightarrow>  pe \<turnstile> (CALL p, s) \<Rightarrow> t" |
   20.32 +
   20.33 +Proc: "pe(p := cp) \<turnstile> (c,s) \<Rightarrow> t  \<Longrightarrow>  pe \<turnstile> ({PROC p = cp;; c}, s) \<Rightarrow> t"
   20.34 +
   20.35 +code_pred big_step .
   20.36 +
   20.37 +(* FIXME: example state syntax *)
   20.38 +values "{map t [''x'',''y'',''z''] |t. 
   20.39 +          (\<lambda>p. SKIP) \<turnstile> (CALL ''p'', (%_. 0)(''x'' := 42, ''y'' := 43)) \<Rightarrow> t}"
   20.40 +
   20.41 +values "{map t [''x'',''y'',''z''] |t. (\<lambda>p. SKIP) \<turnstile> (test_com, (%_. 0)) \<Rightarrow> t}"
   20.42 +
   20.43 +end
    21.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    21.2 +++ b/src/HOL/IMP/Procs_Stat_Vars_Dyn.thy	Mon Jun 06 16:29:38 2011 +0200
    21.3 @@ -0,0 +1,43 @@
    21.4 +theory Procs_Stat_Vars_Dyn imports Util Procs
    21.5 +begin
    21.6 +
    21.7 +subsubsection "Static Scoping of Procedures, Dynamic of Variables"
    21.8 +
    21.9 +type_synonym penv = "(name \<times> com) list"
   21.10 +
   21.11 +inductive
   21.12 +  big_step :: "penv \<Rightarrow> com \<times> state \<Rightarrow> state \<Rightarrow> bool" ("_ \<turnstile> _ \<Rightarrow> _" [60,0,60] 55)
   21.13 +where
   21.14 +Skip:    "pe \<turnstile> (SKIP,s) \<Rightarrow> s" |
   21.15 +Assign:  "pe \<turnstile> (x ::= a,s) \<Rightarrow> s(x := aval a s)" |
   21.16 +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>
   21.17 +          pe \<turnstile> (c\<^isub>1;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
   21.18 +
   21.19 +IfTrue:  "\<lbrakk> bval b s;  pe \<turnstile> (c\<^isub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
   21.20 +         pe \<turnstile> (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
   21.21 +IfFalse: "\<lbrakk> \<not>bval b s;  pe \<turnstile> (c\<^isub>2,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
   21.22 +         pe \<turnstile> (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
   21.23 +
   21.24 +WhileFalse: "\<not>bval b s \<Longrightarrow> pe \<turnstile> (WHILE b DO c,s) \<Rightarrow> s" |
   21.25 +WhileTrue:
   21.26 +  "\<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>
   21.27 +   pe \<turnstile> (WHILE b DO c, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
   21.28 +
   21.29 +Var: "pe \<turnstile> (c,s) \<Rightarrow> t  \<Longrightarrow>  pe \<turnstile> ({VAR x;; c}, s) \<Rightarrow> t(x := s x)" |
   21.30 +
   21.31 +Call1: "(p,c)#pe \<turnstile> (c, s) \<Rightarrow> t  \<Longrightarrow>  (p,c)#pe \<turnstile> (CALL p, s) \<Rightarrow> t" |
   21.32 +Call2: "\<lbrakk> p' \<noteq> p;  pe \<turnstile> (CALL p, s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
   21.33 +       (p',c)#pe \<turnstile> (CALL p, s) \<Rightarrow> t" |
   21.34 +
   21.35 +Proc: "(p,cp)#pe \<turnstile> (c,s) \<Rightarrow> t  \<Longrightarrow>  pe \<turnstile> ({PROC p = cp;; c}, s) \<Rightarrow> t"
   21.36 +
   21.37 +code_pred big_step .
   21.38 +
   21.39 +
   21.40 +(* FIXME: example state syntax *)
   21.41 +values "{map t [''x'', ''y'', ''z''] |t. 
   21.42 +            [] \<turnstile> (CALL ''p'', (%_. 0)(''x'' := 42, ''y'' := 43)) \<Rightarrow> t}"
   21.43 +
   21.44 +values "{map t [''x'', ''y'', ''z''] |t. [] \<turnstile> (test_com, (%_. 0) ) \<Rightarrow> t}"
   21.45 +
   21.46 +end
    22.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.2 +++ b/src/HOL/IMP/Procs_Stat_Vars_Stat.thy	Mon Jun 06 16:29:38 2011 +0200
    22.3 @@ -0,0 +1,53 @@
    22.4 +theory Procs_Stat_Vars_Stat imports Util Procs
    22.5 +begin
    22.6 +
    22.7 +subsubsection "Static Scoping of Procedures and Variables"
    22.8 +
    22.9 +type_synonym addr = nat
   22.10 +type_synonym venv = "name \<Rightarrow> addr"
   22.11 +type_synonym store = "addr \<Rightarrow> val"
   22.12 +type_synonym penv = "(name \<times> com \<times> venv) list"
   22.13 +
   22.14 +fun venv :: "penv \<times> venv \<times> nat \<Rightarrow> venv" where
   22.15 +"venv(_,ve,_) = ve"
   22.16 +
   22.17 +inductive
   22.18 +  big_step :: "penv \<times> venv \<times> nat \<Rightarrow> com \<times> store \<Rightarrow> store \<Rightarrow> bool"
   22.19 +  ("_ \<turnstile> _ \<Rightarrow> _" [60,0,60] 55)
   22.20 +where
   22.21 +Skip:    "e \<turnstile> (SKIP,s) \<Rightarrow> s" |
   22.22 +Assign:  "(pe,ve,f) \<turnstile> (x ::= a,s) \<Rightarrow> s(ve x := aval a (s o ve))" |
   22.23 +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>
   22.24 +          e \<turnstile> (c\<^isub>1;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
   22.25 +
   22.26 +IfTrue:  "\<lbrakk> bval b (s \<circ> venv e);  e \<turnstile> (c\<^isub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
   22.27 +         e \<turnstile> (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
   22.28 +IfFalse: "\<lbrakk> \<not>bval b (s \<circ> venv e);  e \<turnstile> (c\<^isub>2,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
   22.29 +         e \<turnstile> (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
   22.30 +
   22.31 +WhileFalse: "\<not>bval b (s \<circ> venv e) \<Longrightarrow> e \<turnstile> (WHILE b DO c,s) \<Rightarrow> s" |
   22.32 +WhileTrue:
   22.33 +  "\<lbrakk> bval b (s\<^isub>1 \<circ> venv e);  e \<turnstile> (c,s\<^isub>1) \<Rightarrow> s\<^isub>2;
   22.34 +     e \<turnstile> (WHILE b DO c, s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>
   22.35 +   e \<turnstile> (WHILE b DO c, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
   22.36 +
   22.37 +Var: "(pe,ve(x:=f),f+1) \<turnstile> (c,s) \<Rightarrow> t  \<Longrightarrow>
   22.38 +      (pe,ve,f) \<turnstile> ({VAR x;; c}, s) \<Rightarrow> t(f := s f)" |
   22.39 +
   22.40 +Call1: "((p,c,ve)#pe,ve,f) \<turnstile> (c, s) \<Rightarrow> t  \<Longrightarrow>
   22.41 +        ((p,c,ve)#pe,ve',f) \<turnstile> (CALL p, s) \<Rightarrow> t" |
   22.42 +Call2: "\<lbrakk> p' \<noteq> p;  (pe,ve,f) \<turnstile> (CALL p, s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
   22.43 +       ((p',c,ve')#pe,ve,f) \<turnstile> (CALL p, s) \<Rightarrow> t" |
   22.44 +
   22.45 +Proc: "((p,cp,ve)#pe,ve,f) \<turnstile> (c,s) \<Rightarrow> t
   22.46 +      \<Longrightarrow>  (pe,ve,f) \<turnstile> ({PROC p = cp;; c}, s) \<Rightarrow> t"
   22.47 +
   22.48 +code_pred big_step .
   22.49 +
   22.50 +values "{map t [0,1] |t. ([], \<lambda>n. 0, 0) \<turnstile> (CALL ''p'', nth [42, 43]) \<Rightarrow> t}"
   22.51 +
   22.52 +(* FIXME: syntax *)
   22.53 +values "{map t [0, 1, 2] |t. ([], (\<lambda>_. 3)(''x'' := 0, ''y'' := 1,''z'' := 2), 0) \<turnstile> (test_com, (%_. 0)) \<Rightarrow> t}"
   22.54 +
   22.55 +
   22.56 +end
    23.1 --- a/src/HOL/IMP/ROOT.ML	Mon Jun 06 16:29:13 2011 +0200
    23.2 +++ b/src/HOL/IMP/ROOT.ML	Mon Jun 06 16:29:38 2011 +0200
    23.3 @@ -4,13 +4,11 @@
    23.4   "Small_Step",
    23.5   "Denotation",
    23.6   "Compiler",
    23.7 - "Poly_Types"(*,
    23.8 + "Poly_Types",
    23.9   "Sec_Typing",
   23.10   "Sec_TypingT",
   23.11   "Def_Ass_Sound_Big",
   23.12   "Def_Ass_Sound_Small",
   23.13 - "Def_Ass2_Sound_Small",
   23.14 - "Def_Ass2_Big0",
   23.15   "Live",
   23.16   "Hoare_Examples",
   23.17   "VC",
   23.18 @@ -20,5 +18,4 @@
   23.19   "Procs_Stat_Vars_Stat",
   23.20   "C_like",
   23.21   "OO"
   23.22 -*)
   23.23  ];
    24.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    24.2 +++ b/src/HOL/IMP/Sec_Type_Expr.thy	Mon Jun 06 16:29:38 2011 +0200
    24.3 @@ -0,0 +1,45 @@
    24.4 +header "Security Type Systems"
    24.5 +
    24.6 +theory Sec_Type_Expr imports Big_Step
    24.7 +begin
    24.8 +
    24.9 +subsection "Security Levels and Expressions"
   24.10 +
   24.11 +type_synonym level = nat
   24.12 +
   24.13 +text{* The security/confidentiality level of each variable is globally fixed
   24.14 +for simplicity. For the sake of examples --- the general theory does not rely
   24.15 +on it! --- a variable of length @{text n} has security level @{text n}: *}
   24.16 +
   24.17 +definition sec :: "name \<Rightarrow> level" where 
   24.18 +  "sec n = size n"
   24.19 +
   24.20 +fun sec_aexp :: "aexp \<Rightarrow> level" where
   24.21 +"sec_aexp (N n) = 0" |
   24.22 +"sec_aexp (V x) = sec x" |
   24.23 +"sec_aexp (Plus a\<^isub>1 a\<^isub>2) = max (sec_aexp a\<^isub>1) (sec_aexp a\<^isub>2)"
   24.24 +
   24.25 +fun sec_bexp :: "bexp \<Rightarrow> level" where
   24.26 +"sec_bexp (B bv) = 0" |
   24.27 +"sec_bexp (Not b) = sec_bexp b" |
   24.28 +"sec_bexp (And b\<^isub>1 b\<^isub>2) = max (sec_bexp b\<^isub>1) (sec_bexp b\<^isub>2)" |
   24.29 +"sec_bexp (Less a\<^isub>1 a\<^isub>2) = max (sec_aexp a\<^isub>1) (sec_aexp a\<^isub>2)"
   24.30 +
   24.31 +
   24.32 +abbreviation eq_le :: "state \<Rightarrow> state \<Rightarrow> level \<Rightarrow> bool"
   24.33 +  ("(_ = _ '(\<le> _'))" [51,51,0] 50) where
   24.34 +"s = s' (\<le> l) == (\<forall> x. sec x \<le> l \<longrightarrow> s x = s' x)"
   24.35 +
   24.36 +abbreviation eq_less :: "state \<Rightarrow> state \<Rightarrow> level \<Rightarrow> bool"
   24.37 +  ("(_ = _ '(< _'))" [51,51,0] 50) where
   24.38 +"s = s' (< l) == (\<forall> x. sec x < l \<longrightarrow> s x = s' x)"
   24.39 +
   24.40 +lemma aval_eq_if_eq_le:
   24.41 +  "\<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"
   24.42 +by (induct a) auto
   24.43 +
   24.44 +lemma bval_eq_if_eq_le:
   24.45 +  "\<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"
   24.46 +by (induct b) (auto simp add: aval_eq_if_eq_le)
   24.47 +
   24.48 +end
    25.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    25.2 +++ b/src/HOL/IMP/Sec_Typing.thy	Mon Jun 06 16:29:38 2011 +0200
    25.3 @@ -0,0 +1,249 @@
    25.4 +(* Author: Tobias Nipkow *)
    25.5 +
    25.6 +theory Sec_Typing imports Sec_Type_Expr
    25.7 +begin
    25.8 +
    25.9 +subsection "Syntax Directed Typing"
   25.10 +
   25.11 +inductive sec_type :: "nat \<Rightarrow> com \<Rightarrow> bool" ("(_/ \<turnstile> _)" [0,0] 50) where
   25.12 +Skip:
   25.13 +  "l \<turnstile> SKIP" |
   25.14 +Assign:
   25.15 +  "\<lbrakk> sec x \<ge> sec_aexp a;  sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile> x ::= a" |
   25.16 +Semi:
   25.17 +  "\<lbrakk> l \<turnstile> c\<^isub>1;  l \<turnstile> c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile> c\<^isub>1;c\<^isub>2" |
   25.18 +If:
   25.19 +  "\<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" |
   25.20 +While:
   25.21 +  "max (sec_bexp b) l \<turnstile> c \<Longrightarrow> l \<turnstile> WHILE b DO c"
   25.22 +
   25.23 +code_pred (expected_modes: i => i => bool) sec_type .
   25.24 +
   25.25 +value "0 \<turnstile> IF Less (V ''x1'') (V ''x'') THEN ''x1'' ::= N 0 ELSE SKIP"
   25.26 +value "1 \<turnstile> IF Less (V ''x1'') (V ''x'') THEN ''x''  ::= N 0 ELSE SKIP"
   25.27 +value "2 \<turnstile> IF Less (V ''x1'') (V ''x'') THEN ''x1'' ::= N 0 ELSE SKIP"
   25.28 +
   25.29 +inductive_cases [elim!]:
   25.30 +  "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"
   25.31 +
   25.32 +
   25.33 +text{* An important property: anti-monotonicity. *}
   25.34 +
   25.35 +lemma anti_mono: "\<lbrakk> l \<turnstile> c;  l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile> c"
   25.36 +apply(induct arbitrary: l' rule: sec_type.induct)
   25.37 +apply (metis sec_type.intros(1))
   25.38 +apply (metis le_trans sec_type.intros(2))
   25.39 +apply (metis sec_type.intros(3))
   25.40 +apply (metis If le_refl sup_mono sup_nat_def)
   25.41 +apply (metis While le_refl sup_mono sup_nat_def)
   25.42 +done
   25.43 +
   25.44 +lemma confinement: "\<lbrakk> (c,s) \<Rightarrow> t;  l \<turnstile> c \<rbrakk> \<Longrightarrow> s = t (< l)"
   25.45 +proof(induct rule: big_step_induct)
   25.46 +  case Skip thus ?case by simp
   25.47 +next
   25.48 +  case Assign thus ?case by auto
   25.49 +next
   25.50 +  case Semi thus ?case by auto
   25.51 +next
   25.52 +  case (IfTrue b s c1)
   25.53 +  hence "max (sec_bexp b) l \<turnstile> c1" by auto
   25.54 +  hence "l \<turnstile> c1" by (metis le_maxI2 anti_mono)
   25.55 +  thus ?case using IfTrue.hyps by metis
   25.56 +next
   25.57 +  case (IfFalse b s c2)
   25.58 +  hence "max (sec_bexp b) l \<turnstile> c2" by auto
   25.59 +  hence "l \<turnstile> c2" by (metis le_maxI2 anti_mono)
   25.60 +  thus ?case using IfFalse.hyps by metis
   25.61 +next
   25.62 +  case WhileFalse thus ?case by auto
   25.63 +next
   25.64 +  case (WhileTrue b s1 c)
   25.65 +  hence "max (sec_bexp b) l \<turnstile> c" by auto
   25.66 +  hence "l \<turnstile> c" by (metis le_maxI2 anti_mono)
   25.67 +  thus ?case using WhileTrue by metis
   25.68 +qed
   25.69 +
   25.70 +
   25.71 +theorem noninterference:
   25.72 +  "\<lbrakk> (c,s) \<Rightarrow> s'; (c,t) \<Rightarrow> t';  0 \<turnstile> c;  s = t (\<le> l) \<rbrakk>
   25.73 +   \<Longrightarrow> s' = t' (\<le> l)"
   25.74 +proof(induct arbitrary: t t' rule: big_step_induct)
   25.75 +  case Skip thus ?case by auto
   25.76 +next
   25.77 +  case (Assign x a s)
   25.78 +  have [simp]: "t' = t(x := aval a t)" using Assign by auto
   25.79 +  have "sec x >= sec_aexp a" using `0 \<turnstile> x ::= a` by auto
   25.80 +  show ?case
   25.81 +  proof auto
   25.82 +    assume "sec x \<le> l"
   25.83 +    with `sec x >= sec_aexp a` have "sec_aexp a \<le> l" by arith
   25.84 +    thus "aval a s = aval a t"
   25.85 +      by (rule aval_eq_if_eq_le[OF `s = t (\<le> l)`])
   25.86 +  next
   25.87 +    fix y assume "y \<noteq> x" "sec y \<le> l"
   25.88 +    thus "s y = t y" using `s = t (\<le> l)` by simp
   25.89 +  qed
   25.90 +next
   25.91 +  case Semi thus ?case by blast
   25.92 +next
   25.93 +  case (IfTrue b s c1 s' c2)
   25.94 +  have "sec_bexp b \<turnstile> c1" "sec_bexp b \<turnstile> c2" using IfTrue.prems(2) by auto
   25.95 +  show ?case
   25.96 +  proof cases
   25.97 +    assume "sec_bexp b \<le> l"
   25.98 +    hence "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto
   25.99 +    hence "bval b t" using `bval b s` by(simp add: bval_eq_if_eq_le)
  25.100 +    with IfTrue.hyps(3) IfTrue.prems(1,3) `sec_bexp b \<turnstile> c1`  anti_mono
  25.101 +    show ?thesis by auto
  25.102 +  next
  25.103 +    assume "\<not> sec_bexp b \<le> l"
  25.104 +    have 1: "sec_bexp b \<turnstile> IF b THEN c1 ELSE c2"
  25.105 +      by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c1` `sec_bexp b \<turnstile> c2`)
  25.106 +    from confinement[OF big_step.IfTrue[OF IfTrue(1,2)] 1] `\<not> sec_bexp b \<le> l`
  25.107 +    have "s = s' (\<le> l)" by auto
  25.108 +    moreover
  25.109 +    from confinement[OF IfTrue.prems(1) 1] `\<not> sec_bexp b \<le> l`
  25.110 +    have "t = t' (\<le> l)" by auto
  25.111 +    ultimately show "s' = t' (\<le> l)" using `s = t (\<le> l)` by auto
  25.112 +  qed
  25.113 +next
  25.114 +  case (IfFalse b s c2 s' c1)
  25.115 +  have "sec_bexp b \<turnstile> c1" "sec_bexp b \<turnstile> c2" using IfFalse.prems(2) by auto
  25.116 +  show ?case
  25.117 +  proof cases
  25.118 +    assume "sec_bexp b \<le> l"
  25.119 +    hence "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto
  25.120 +    hence "\<not> bval b t" using `\<not> bval b s` by(simp add: bval_eq_if_eq_le)
  25.121 +    with IfFalse.hyps(3) IfFalse.prems(1,3) `sec_bexp b \<turnstile> c2` anti_mono
  25.122 +    show ?thesis by auto
  25.123 +  next
  25.124 +    assume "\<not> sec_bexp b \<le> l"
  25.125 +    have 1: "sec_bexp b \<turnstile> IF b THEN c1 ELSE c2"
  25.126 +      by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c1` `sec_bexp b \<turnstile> c2`)
  25.127 +    from confinement[OF big_step.IfFalse[OF IfFalse(1,2)] 1] `\<not> sec_bexp b \<le> l`
  25.128 +    have "s = s' (\<le> l)" by auto
  25.129 +    moreover
  25.130 +    from confinement[OF IfFalse.prems(1) 1] `\<not> sec_bexp b \<le> l`
  25.131 +    have "t = t' (\<le> l)" by auto
  25.132 +    ultimately show "s' = t' (\<le> l)" using `s = t (\<le> l)` by auto
  25.133 +  qed
  25.134 +next
  25.135 +  case (WhileFalse b s c)
  25.136 +  have "sec_bexp b \<turnstile> c" using WhileFalse.prems(2) by auto
  25.137 +  show ?case
  25.138 +  proof cases
  25.139 +    assume "sec_bexp b \<le> l"
  25.140 +    hence "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto
  25.141 +    hence "\<not> bval b t" using `\<not> bval b s` by(simp add: bval_eq_if_eq_le)
  25.142 +    with WhileFalse.prems(1,3) show ?thesis by auto
  25.143 +  next
  25.144 +    assume "\<not> sec_bexp b \<le> l"
  25.145 +    have 1: "sec_bexp b \<turnstile> WHILE b DO c"
  25.146 +      by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c`)
  25.147 +    from confinement[OF WhileFalse.prems(1) 1] `\<not> sec_bexp b \<le> l`
  25.148 +    have "t = t' (\<le> l)" by auto
  25.149 +    thus "s = t' (\<le> l)" using `s = t (\<le> l)` by auto
  25.150 +  qed
  25.151 +next
  25.152 +  case (WhileTrue b s1 c s2 s3 t1 t3)
  25.153 +  let ?w = "WHILE b DO c"
  25.154 +  have "sec_bexp b \<turnstile> c" using WhileTrue.prems(2) by auto
  25.155 +  show ?case
  25.156 +  proof cases
  25.157 +    assume "sec_bexp b \<le> l"
  25.158 +    hence "s1 = t1 (\<le> sec_bexp b)" using `s1 = t1 (\<le> l)` by auto
  25.159 +    hence "bval b t1"
  25.160 +      using `bval b s1` by(simp add: bval_eq_if_eq_le)
  25.161 +    then obtain t2 where "(c,t1) \<Rightarrow> t2" "(?w,t2) \<Rightarrow> t3"
  25.162 +      using `(?w,t1) \<Rightarrow> t3` by auto
  25.163 +    from WhileTrue.hyps(5)[OF `(?w,t2) \<Rightarrow> t3` `0 \<turnstile> ?w`
  25.164 +      WhileTrue.hyps(3)[OF `(c,t1) \<Rightarrow> t2` anti_mono[OF `sec_bexp b \<turnstile> c`]
  25.165 +        `s1 = t1 (\<le> l)`]]
  25.166 +    show ?thesis by simp
  25.167 +  next
  25.168 +    assume "\<not> sec_bexp b \<le> l"
  25.169 +    have 1: "sec_bexp b \<turnstile> ?w" by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c`)
  25.170 +    from confinement[OF big_step.WhileTrue[OF WhileTrue(1,2,4)] 1] `\<not> sec_bexp b \<le> l`
  25.171 +    have "s1 = s3 (\<le> l)" by auto
  25.172 +    moreover
  25.173 +    from confinement[OF WhileTrue.prems(1) 1] `\<not> sec_bexp b \<le> l`
  25.174 +    have "t1 = t3 (\<le> l)" by auto
  25.175 +    ultimately show "s3 = t3 (\<le> l)" using `s1 = t1 (\<le> l)` by auto
  25.176 +  qed
  25.177 +qed
  25.178 +
  25.179 +
  25.180 +subsection "The Standard Typing System"
  25.181 +
  25.182 +text{* The predicate @{prop"l \<turnstile> c"} is nicely intuitive and executable. The
  25.183 +standard formulation, however, is slightly different, replacing the maximum
  25.184 +computation by an antimonotonicity rule. We introduce the standard system now
  25.185 +and show the equivalence with our formulation. *}
  25.186 +
  25.187 +inductive sec_type' :: "nat \<Rightarrow> com \<Rightarrow> bool" ("(_/ \<turnstile>'' _)" [0,0] 50) where
  25.188 +Skip':
  25.189 +  "l \<turnstile>' SKIP" |
  25.190 +Assign':
  25.191 +  "\<lbrakk> sec x \<ge> sec_aexp a; sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile>' x ::= a" |
  25.192 +Semi':
  25.193 +  "\<lbrakk> l \<turnstile>' c\<^isub>1;  l \<turnstile>' c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile>' c\<^isub>1;c\<^isub>2" |
  25.194 +If':
  25.195 +  "\<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" |
  25.196 +While':
  25.197 +  "\<lbrakk> sec_bexp b \<le> l;  l \<turnstile>' c \<rbrakk> \<Longrightarrow> l \<turnstile>' WHILE b DO c" |
  25.198 +anti_mono':
  25.199 +  "\<lbrakk> l \<turnstile>' c;  l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile>' c"
  25.200 +
  25.201 +lemma sec_type_sec_type': "l \<turnstile> c \<Longrightarrow> l \<turnstile>' c"
  25.202 +apply(induct rule: sec_type.induct)
  25.203 +apply (metis Skip')
  25.204 +apply (metis Assign')
  25.205 +apply (metis Semi')
  25.206 +apply (metis min_max.inf_sup_ord(3) min_max.sup_absorb2 nat_le_linear If' anti_mono')
  25.207 +by (metis less_or_eq_imp_le min_max.sup_absorb1 min_max.sup_absorb2 nat_le_linear While' anti_mono')
  25.208 +
  25.209 +
  25.210 +lemma sec_type'_sec_type: "l \<turnstile>' c \<Longrightarrow> l \<turnstile> c"
  25.211 +apply(induct rule: sec_type'.induct)
  25.212 +apply (metis Skip)
  25.213 +apply (metis Assign)
  25.214 +apply (metis Semi)
  25.215 +apply (metis min_max.sup_absorb2 If)
  25.216 +apply (metis min_max.sup_absorb2 While)
  25.217 +by (metis anti_mono)
  25.218 +
  25.219 +subsection "A Bottom-Up Typing System"
  25.220 +
  25.221 +inductive sec_type2 :: "com \<Rightarrow> level \<Rightarrow> bool" ("(\<turnstile> _ : _)" [0,0] 50) where
  25.222 +Skip2:
  25.223 +  "\<turnstile> SKIP : l" |
  25.224 +Assign2:
  25.225 +  "sec x \<ge> sec_aexp a \<Longrightarrow> \<turnstile> x ::= a : sec x" |
  25.226 +Semi2:
  25.227 +  "\<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 " |
  25.228 +If2:
  25.229 +  "\<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>
  25.230 +  \<Longrightarrow> \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2 : min l\<^isub>1 l\<^isub>2" |
  25.231 +While2:
  25.232 +  "\<lbrakk> sec_bexp b \<le> l;  \<turnstile> c : l \<rbrakk> \<Longrightarrow> \<turnstile> WHILE b DO c : l"
  25.233 +
  25.234 +
  25.235 +lemma sec_type2_sec_type': "\<turnstile> c : l \<Longrightarrow> l \<turnstile>' c"
  25.236 +apply(induct rule: sec_type2.induct)
  25.237 +apply (metis Skip')
  25.238 +apply (metis Assign' eq_imp_le)
  25.239 +apply (metis Semi' anti_mono' min_max.inf.commute min_max.inf_le2)
  25.240 +apply (metis If' anti_mono' min_max.inf_absorb2 min_max.le_iff_inf nat_le_linear)
  25.241 +by (metis While')
  25.242 +
  25.243 +lemma sec_type'_sec_type2: "l \<turnstile>' c \<Longrightarrow> \<exists> l' \<ge> l. \<turnstile> c : l'"
  25.244 +apply(induct rule: sec_type'.induct)
  25.245 +apply (metis Skip2 le_refl)
  25.246 +apply (metis Assign2)
  25.247 +apply (metis Semi2 min_max.inf_greatest)
  25.248 +apply (metis If2 inf_greatest inf_nat_def le_trans)
  25.249 +apply (metis While2 le_trans)
  25.250 +by (metis le_trans)
  25.251 +
  25.252 +end
    26.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    26.2 +++ b/src/HOL/IMP/Sec_TypingT.thy	Mon Jun 06 16:29:38 2011 +0200
    26.3 @@ -0,0 +1,205 @@
    26.4 +theory Sec_TypingT imports Sec_Type_Expr
    26.5 +begin
    26.6 +
    26.7 +subsection "A Termination-Sensitive Syntax Directed System"
    26.8 +
    26.9 +inductive sec_type :: "nat \<Rightarrow> com \<Rightarrow> bool" ("(_/ \<turnstile> _)" [0,0] 50) where
   26.10 +Skip:
   26.11 +  "l \<turnstile> SKIP"  |
   26.12 +Assign:
   26.13 +  "\<lbrakk> sec x \<ge> sec_aexp a;  sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile> x ::= a"  |
   26.14 +Semi:
   26.15 +  "l \<turnstile> c\<^isub>1 \<Longrightarrow> l \<turnstile> c\<^isub>2 \<Longrightarrow> l \<turnstile> c\<^isub>1;c\<^isub>2"  |
   26.16 +If:
   26.17 +  "\<lbrakk> max (sec_bexp b) l \<turnstile> c\<^isub>1;  max (sec_bexp b) l \<turnstile> c\<^isub>2 \<rbrakk>
   26.18 +   \<Longrightarrow> l \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2"  |
   26.19 +While:
   26.20 +  "sec_bexp b = 0 \<Longrightarrow> 0 \<turnstile> c \<Longrightarrow> 0 \<turnstile> WHILE b DO c"
   26.21 +
   26.22 +code_pred (expected_modes: i => i => bool) sec_type .
   26.23 +
   26.24 +inductive_cases [elim!]:
   26.25 +  "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"
   26.26 +
   26.27 +
   26.28 +lemma anti_mono: "l \<turnstile> c \<Longrightarrow> l' \<le> l \<Longrightarrow> l' \<turnstile> c"
   26.29 +apply(induct arbitrary: l' rule: sec_type.induct)
   26.30 +apply (metis sec_type.intros(1))
   26.31 +apply (metis le_trans sec_type.intros(2))
   26.32 +apply (metis sec_type.intros(3))
   26.33 +apply (metis If le_refl sup_mono sup_nat_def)
   26.34 +by (metis While le_0_eq)
   26.35 +
   26.36 +
   26.37 +lemma confinement: "(c,s) \<Rightarrow> t \<Longrightarrow> l \<turnstile> c \<Longrightarrow> s = t (< l)"
   26.38 +proof(induct rule: big_step_induct)
   26.39 +  case Skip thus ?case by simp
   26.40 +next
   26.41 +  case Assign thus ?case by auto
   26.42 +next
   26.43 +  case Semi thus ?case by auto
   26.44 +next
   26.45 +  case (IfTrue b s c1)
   26.46 +  hence "max (sec_bexp b) l \<turnstile> c1" by auto
   26.47 +  hence "l \<turnstile> c1" by (metis le_maxI2 anti_mono)
   26.48 +  thus ?case using IfTrue.hyps by metis
   26.49 +next
   26.50 +  case (IfFalse b s c2)
   26.51 +  hence "max (sec_bexp b) l \<turnstile> c2" by auto
   26.52 +  hence "l \<turnstile> c2" by (metis le_maxI2 anti_mono)
   26.53 +  thus ?case using IfFalse.hyps by metis
   26.54 +next
   26.55 +  case WhileFalse thus ?case by auto
   26.56 +next
   26.57 +  case (WhileTrue b s1 c)
   26.58 +  hence "l \<turnstile> c" by auto
   26.59 +  thus ?case using WhileTrue by metis
   26.60 +qed
   26.61 +
   26.62 +lemma termi_if_non0: "l \<turnstile> c \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> \<exists> t. (c,s) \<Rightarrow> t"
   26.63 +apply(induct arbitrary: s rule: sec_type.induct)
   26.64 +apply (metis big_step.Skip)
   26.65 +apply (metis big_step.Assign)
   26.66 +apply (metis big_step.Semi)
   26.67 +apply (metis IfFalse IfTrue le0 le_antisym le_maxI2)
   26.68 +apply simp
   26.69 +done
   26.70 +
   26.71 +theorem noninterference: "(c,s) \<Rightarrow> s' \<Longrightarrow> 0 \<turnstile> c \<Longrightarrow>  s = t (\<le> l)
   26.72 +  \<Longrightarrow> \<exists> t'. (c,t) \<Rightarrow> t' \<and> s' = t' (\<le> l)"
   26.73 +proof(induct arbitrary: t rule: big_step_induct)
   26.74 +  case Skip thus ?case by auto
   26.75 +next
   26.76 +  case (Assign x a s)
   26.77 +  have "sec x >= sec_aexp a" using `0 \<turnstile> x ::= a` by auto
   26.78 +  have "(x ::= a,t) \<Rightarrow> t(x := aval a t)" by auto
   26.79 +  moreover
   26.80 +  have "s(x := aval a s) = t(x := aval a t) (\<le> l)"
   26.81 +  proof auto
   26.82 +    assume "sec x \<le> l"
   26.83 +    with `sec x \<ge> sec_aexp a` have "sec_aexp a \<le> l" by arith
   26.84 +    thus "aval a s = aval a t"
   26.85 +      by (rule aval_eq_if_eq_le[OF `s = t (\<le> l)`])
   26.86 +  next
   26.87 +    fix y assume "y \<noteq> x" "sec y \<le> l"
   26.88 +    thus "s y = t y" using `s = t (\<le> l)` by simp
   26.89 +  qed
   26.90 +  ultimately show ?case by blast
   26.91 +next
   26.92 +  case Semi thus ?case by blast
   26.93 +next
   26.94 +  case (IfTrue b s c1 s' c2)
   26.95 +  have "sec_bexp b \<turnstile> c1" "sec_bexp b \<turnstile> c2" using IfTrue.prems by auto
   26.96 +  obtain t' where t': "(c1, t) \<Rightarrow> t'" "s' = t' (\<le> l)"
   26.97 +    using IfTrue(3)[OF anti_mono[OF `sec_bexp b \<turnstile> c1`] IfTrue.prems(2)] by blast
   26.98 +  show ?case
   26.99 +  proof cases
  26.100 +    assume "sec_bexp b \<le> l"
  26.101 +    hence "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto
  26.102 +    hence "bval b t" using `bval b s` by(simp add: bval_eq_if_eq_le)
  26.103 +    thus ?thesis by (metis t' big_step.IfTrue)
  26.104 +  next
  26.105 +    assume "\<not> sec_bexp b \<le> l"
  26.106 +    hence 0: "sec_bexp b \<noteq> 0" by arith
  26.107 +    have 1: "sec_bexp b \<turnstile> IF b THEN c1 ELSE c2"
  26.108 +      by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c1` `sec_bexp b \<turnstile> c2`)
  26.109 +    from confinement[OF big_step.IfTrue[OF IfTrue(1,2)] 1] `\<not> sec_bexp b \<le> l`
  26.110 +    have "s = s' (\<le> l)" by auto
  26.111 +    moreover
  26.112 +    from termi_if_non0[OF 1 0, of t] obtain t' where
  26.113 +      "(IF b THEN c1 ELSE c2,t) \<Rightarrow> t'" ..
  26.114 +    moreover
  26.115 +    from confinement[OF this 1] `\<not> sec_bexp b \<le> l`
  26.116 +    have "t = t' (\<le> l)" by auto
  26.117 +    ultimately
  26.118 +    show ?case using `s = t (\<le> l)` by auto
  26.119 +  qed
  26.120 +next
  26.121 +  case (IfFalse b s c2 s' c1)
  26.122 +  have "sec_bexp b \<turnstile> c1" "sec_bexp b \<turnstile> c2" using IfFalse.prems by auto
  26.123 +  obtain t' where t': "(c2, t) \<Rightarrow> t'" "s' = t' (\<le> l)"
  26.124 +    using IfFalse(3)[OF anti_mono[OF `sec_bexp b \<turnstile> c2`] IfFalse.prems(2)] by blast
  26.125 +  show ?case
  26.126 +  proof cases
  26.127 +    assume "sec_bexp b \<le> l"
  26.128 +    hence "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto
  26.129 +    hence "\<not> bval b t" using `\<not> bval b s` by(simp add: bval_eq_if_eq_le)
  26.130 +    thus ?thesis by (metis t' big_step.IfFalse)
  26.131 +  next
  26.132 +    assume "\<not> sec_bexp b \<le> l"
  26.133 +    hence 0: "sec_bexp b \<noteq> 0" by arith
  26.134 +    have 1: "sec_bexp b \<turnstile> IF b THEN c1 ELSE c2"
  26.135 +      by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c1` `sec_bexp b \<turnstile> c2`)
  26.136 +    from confinement[OF big_step.IfFalse[OF IfFalse(1,2)] 1] `\<not> sec_bexp b \<le> l`
  26.137 +    have "s = s' (\<le> l)" by auto
  26.138 +    moreover
  26.139 +    from termi_if_non0[OF 1 0, of t] obtain t' where
  26.140 +      "(IF b THEN c1 ELSE c2,t) \<Rightarrow> t'" ..
  26.141 +    moreover
  26.142 +    from confinement[OF this 1] `\<not> sec_bexp b \<le> l`
  26.143 +    have "t = t' (\<le> l)" by auto
  26.144 +    ultimately
  26.145 +    show ?case using `s = t (\<le> l)` by auto
  26.146 +  qed
  26.147 +next
  26.148 +  case (WhileFalse b s c)
  26.149 +  hence [simp]: "sec_bexp b = 0" by auto
  26.150 +  have "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto
  26.151 +  hence "\<not> bval b t" using `\<not> bval b s` by (metis bval_eq_if_eq_le le_refl)
  26.152 +  with WhileFalse.prems(2) show ?case by auto
  26.153 +next
  26.154 +  case (WhileTrue b s c s'' s')
  26.155 +  let ?w = "WHILE b DO c"
  26.156 +  from `0 \<turnstile> ?w` have [simp]: "sec_bexp b = 0" by auto
  26.157 +  have "0 \<turnstile> c" using WhileTrue.prems(1) by auto
  26.158 +  from WhileTrue(3)[OF this WhileTrue.prems(2)]
  26.159 +  obtain t'' where "(c,t) \<Rightarrow> t''" and "s'' = t'' (\<le>l)" by blast
  26.160 +  from WhileTrue(5)[OF `0 \<turnstile> ?w` this(2)]
  26.161 +  obtain t' where "(?w,t'') \<Rightarrow> t'" and "s' = t' (\<le>l)" by blast
  26.162 +  from `bval b s` have "bval b t"
  26.163 +    using bval_eq_if_eq_le[OF `s = t (\<le>l)`] by auto
  26.164 +  show ?case
  26.165 +    using big_step.WhileTrue[OF `bval b t` `(c,t) \<Rightarrow> t''` `(?w,t'') \<Rightarrow> t'`]
  26.166 +    by (metis `s' = t' (\<le> l)`)
  26.167 +qed
  26.168 +
  26.169 +subsection "The Standard Termination-Sensitive System"
  26.170 +
  26.171 +text{* The predicate @{prop"l \<turnstile> c"} is nicely intuitive and executable. The
  26.172 +standard formulation, however, is slightly different, replacing the maximum
  26.173 +computation by an antimonotonicity rule. We introduce the standard system now
  26.174 +and show the equivalence with our formulation. *}
  26.175 +
  26.176 +inductive sec_type' :: "nat \<Rightarrow> com \<Rightarrow> bool" ("(_/ \<turnstile>'' _)" [0,0] 50) where
  26.177 +Skip':
  26.178 +  "l \<turnstile>' SKIP"  |
  26.179 +Assign':
  26.180 +  "\<lbrakk> sec x \<ge> sec_aexp a;  sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile>' x ::= a"  |
  26.181 +Semi':
  26.182 +  "l \<turnstile>' c\<^isub>1 \<Longrightarrow> l \<turnstile>' c\<^isub>2 \<Longrightarrow> l \<turnstile>' c\<^isub>1;c\<^isub>2"  |
  26.183 +If':
  26.184 +  "\<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"  |
  26.185 +While':
  26.186 +  "\<lbrakk> sec_bexp b = 0;  0 \<turnstile>' c \<rbrakk> \<Longrightarrow> 0 \<turnstile>' WHILE b DO c"  |
  26.187 +anti_mono':
  26.188 +  "\<lbrakk> l \<turnstile>' c;  l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile>' c"
  26.189 +
  26.190 +lemma "l \<turnstile> c \<Longrightarrow> l \<turnstile>' c"
  26.191 +apply(induct rule: sec_type.induct)
  26.192 +apply (metis Skip')
  26.193 +apply (metis Assign')
  26.194 +apply (metis Semi')
  26.195 +apply (metis min_max.inf_sup_ord(3) min_max.sup_absorb2 nat_le_linear If' anti_mono')
  26.196 +by (metis While')
  26.197 +
  26.198 +
  26.199 +lemma "l \<turnstile>' c \<Longrightarrow> l \<turnstile> c"
  26.200 +apply(induct rule: sec_type'.induct)
  26.201 +apply (metis Skip)
  26.202 +apply (metis Assign)
  26.203 +apply (metis Semi)
  26.204 +apply (metis min_max.sup_absorb2 If)
  26.205 +apply (metis While)
  26.206 +by (metis anti_mono)
  26.207 +
  26.208 +end
    27.1 --- a/src/HOL/IMP/Small_Step.thy	Mon Jun 06 16:29:13 2011 +0200
    27.2 +++ b/src/HOL/IMP/Small_Step.thy	Mon Jun 06 16:29:38 2011 +0200
    27.3 @@ -27,7 +27,7 @@
    27.4  
    27.5  values "{(c',map t [''x'',''y'',''z'']) |c' t.
    27.6     (''x'' ::= V ''z''; ''y'' ::= V ''x'',
    27.7 -    lookup[(''x'',3),(''y'',7),(''z'',5)]) \<rightarrow>* (c',t)}"
    27.8 +    [''x'' \<rightarrow> 3, ''y'' \<rightarrow> 7, ''z'' \<rightarrow> 5]) \<rightarrow>* (c',t)}"
    27.9  
   27.10  
   27.11  subsection{* Proof infrastructure *}
    28.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    28.2 +++ b/src/HOL/IMP/Util.thy	Mon Jun 06 16:29:38 2011 +0200
    28.3 @@ -0,0 +1,29 @@
    28.4 +(* Author: Tobias Nipkow *)
    28.5 +
    28.6 +theory Util imports Main
    28.7 +begin
    28.8 +
    28.9 +subsection "Show sets of variables as lists"
   28.10 +
   28.11 +text {* Sets are functions and are not displayed by element if
   28.12 +computed as values: *}
   28.13 +value "{''x'', ''y''}"
   28.14 +
   28.15 +text {* Lists do not have this problem *}
   28.16 +value "[''x'', ''y'']"
   28.17 +
   28.18 +text {* We define a function @{text show} that converts a set of
   28.19 +  variable names into a list. To keep things simple, we rely on
   28.20 +  the convention that we only use single letter names.
   28.21 +*}
   28.22 +definition 
   28.23 +  letters :: "string list" where
   28.24 +  "letters = map (\<lambda>c. [c]) chars"
   28.25 +
   28.26 +definition 
   28.27 +  "show" :: "string set \<Rightarrow> string list" where
   28.28 +  "show S = filter S letters" 
   28.29 +
   28.30 +value "show {''x'', ''z''}"
   28.31 +
   28.32 +end
    29.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    29.2 +++ b/src/HOL/IMP/VC.thy	Mon Jun 06 16:29:38 2011 +0200
    29.3 @@ -0,0 +1,146 @@
    29.4 +header "Verification Conditions"
    29.5 +
    29.6 +theory VC imports Hoare begin
    29.7 +
    29.8 +subsection "VCG via Weakest Preconditions"
    29.9 +
   29.10 +text{* Annotated commands: commands where loops are annotated with
   29.11 +invariants. *}
   29.12 +
   29.13 +datatype acom = Askip
   29.14 +              | Aassign name aexp
   29.15 +              | Asemi   acom acom
   29.16 +              | Aif     bexp acom acom
   29.17 +              | Awhile  bexp assn acom
   29.18 +
   29.19 +text{* Weakest precondition from annotated commands: *}
   29.20 +
   29.21 +fun pre :: "acom \<Rightarrow> assn \<Rightarrow> assn" where
   29.22 +"pre Askip Q = Q" |
   29.23 +"pre (Aassign x a) Q = (\<lambda>s. Q(s(x := aval a s)))" |
   29.24 +"pre (Asemi c\<^isub>1 c\<^isub>2) Q = pre c\<^isub>1 (pre c\<^isub>2 Q)" |
   29.25 +"pre (Aif b c\<^isub>1 c\<^isub>2) Q =
   29.26 +  (\<lambda>s. (bval b s \<longrightarrow> pre c\<^isub>1 Q s) \<and>
   29.27 +       (\<not> bval b s \<longrightarrow> pre c\<^isub>2 Q s))" |
   29.28 +"pre (Awhile b I c) Q = I"
   29.29 +
   29.30 +text{* Verification condition: *}
   29.31 +
   29.32 +fun vc :: "acom \<Rightarrow> assn \<Rightarrow> assn" where
   29.33 +"vc Askip Q = (\<lambda>s. True)" |
   29.34 +"vc (Aassign x a) Q = (\<lambda>s. True)" |
   29.35 +"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)" |
   29.36 +"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)" |
   29.37 +"vc (Awhile b I c) Q =
   29.38 +  (\<lambda>s. (I s \<and> \<not> bval b s \<longrightarrow> Q s) \<and>
   29.39 +       (I s \<and> bval b s \<longrightarrow> pre c I s) \<and>
   29.40 +       vc c I s)"
   29.41 +
   29.42 +text{* Strip annotations: *}
   29.43 +
   29.44 +fun astrip :: "acom \<Rightarrow> com" where
   29.45 +"astrip Askip = SKIP" |
   29.46 +"astrip (Aassign x a) = (x::=a)" |
   29.47 +"astrip (Asemi c\<^isub>1 c\<^isub>2) = (astrip c\<^isub>1; astrip c\<^isub>2)" |
   29.48 +"astrip (Aif b c\<^isub>1 c\<^isub>2) = (IF b THEN astrip c\<^isub>1 ELSE astrip c\<^isub>2)" |
   29.49 +"astrip (Awhile b I c) = (WHILE b DO astrip c)"
   29.50 +
   29.51 +
   29.52 +subsection "Soundness"
   29.53 +
   29.54 +lemma vc_sound: "\<forall>s. vc c Q s \<Longrightarrow> \<turnstile> {pre c Q} astrip c {Q}"
   29.55 +proof(induct c arbitrary: Q)
   29.56 +  case (Awhile b I c)
   29.57 +  show ?case
   29.58 +  proof(simp, rule While')
   29.59 +    from `\<forall>s. vc (Awhile b I c) Q s`
   29.60 +    have vc: "\<forall>s. vc c I s" and IQ: "\<forall>s. I s \<and> \<not> bval b s \<longrightarrow> Q s" and
   29.61 +         pre: "\<forall>s. I s \<and> bval b s \<longrightarrow> pre c I s" by simp_all
   29.62 +    have "\<turnstile> {pre c I} astrip c {I}" by(rule Awhile.hyps[OF vc])
   29.63 +    with pre show "\<turnstile> {\<lambda>s. I s \<and> bval b s} astrip c {I}"
   29.64 +      by(rule strengthen_pre)
   29.65 +    show "\<forall>s. I s \<and> \<not>bval b s \<longrightarrow> Q s" by(rule IQ)
   29.66 +  qed
   29.67 +qed (auto intro: hoare.conseq)
   29.68 +
   29.69 +corollary vc_sound':
   29.70 +  "(\<forall>s. vc c Q s) \<and> (\<forall>s. P s \<longrightarrow> pre c Q s) \<Longrightarrow> \<turnstile> {P} astrip c {Q}"
   29.71 +by (metis strengthen_pre vc_sound)
   29.72 +
   29.73 +
   29.74 +subsection "Completeness"
   29.75 +
   29.76 +lemma pre_mono:
   29.77 +  "\<forall>s. P s \<longrightarrow> P' s \<Longrightarrow> pre c P s \<Longrightarrow> pre c P' s"
   29.78 +proof (induct c arbitrary: P P' s)
   29.79 +  case Asemi thus ?case by simp metis
   29.80 +qed simp_all
   29.81 +
   29.82 +lemma vc_mono:
   29.83 +  "\<forall>s. P s \<longrightarrow> P' s \<Longrightarrow> vc c P s \<Longrightarrow> vc c P' s"
   29.84 +proof(induct c arbitrary: P P')
   29.85 +  case Asemi thus ?case by simp (metis pre_mono)
   29.86 +qed simp_all
   29.87 +
   29.88 +lemma vc_complete:
   29.89 + "\<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)"
   29.90 +  (is "_ \<Longrightarrow> \<exists>c'. ?G P c Q c'")
   29.91 +proof (induct rule: hoare.induct)
   29.92 +  case Skip
   29.93 +  show ?case (is "\<exists>ac. ?C ac")
   29.94 +  proof show "?C Askip" by simp qed
   29.95 +next
   29.96 +  case (Assign P a x)
   29.97 +  show ?case (is "\<exists>ac. ?C ac")
   29.98 +  proof show "?C(Aassign x a)" by simp qed
   29.99 +next
  29.100 +  case (Semi P c1 Q c2 R)
  29.101 +  from Semi.hyps obtain ac1 where ih1: "?G P c1 Q ac1" by blast
  29.102 +  from Semi.hyps obtain ac2 where ih2: "?G Q c2 R ac2" by blast
  29.103 +  show ?case (is "\<exists>ac. ?C ac")
  29.104 +  proof
  29.105 +    show "?C(Asemi ac1 ac2)"
  29.106 +      using ih1 ih2 by (fastsimp elim!: pre_mono vc_mono)
  29.107 +  qed
  29.108 +next
  29.109 +  case (If P b c1 Q c2)
  29.110 +  from If.hyps obtain ac1 where ih1: "?G (\<lambda>s. P s \<and> bval b s) c1 Q ac1"
  29.111 +    by blast
  29.112 +  from If.hyps obtain ac2 where ih2: "?G (\<lambda>s. P s \<and> \<not>bval b s) c2 Q ac2"
  29.113 +    by blast
  29.114 +  show ?case (is "\<exists>ac. ?C ac")
  29.115 +  proof
  29.116 +    show "?C(Aif b ac1 ac2)" using ih1 ih2 by simp
  29.117 +  qed
  29.118 +next
  29.119 +  case (While P b c)
  29.120 +  from While.hyps obtain ac where ih: "?G (\<lambda>s. P s \<and> bval b s) c P ac" by blast
  29.121 +  show ?case (is "\<exists>ac. ?C ac")
  29.122 +  proof show "?C(Awhile b P ac)" using ih by simp qed
  29.123 +next
  29.124 +  case conseq thus ?case by(fast elim!: pre_mono vc_mono)
  29.125 +qed
  29.126 +
  29.127 +
  29.128 +subsection "An Optimization"
  29.129 +
  29.130 +fun vcpre :: "acom \<Rightarrow> assn \<Rightarrow> assn \<times> assn" where
  29.131 +"vcpre Askip Q = (\<lambda>s. True, Q)" |
  29.132 +"vcpre (Aassign x a) Q = (\<lambda>s. True, \<lambda>s. Q(s[a/x]))" |
  29.133 +"vcpre (Asemi c\<^isub>1 c\<^isub>2) Q =
  29.134 +  (let (vc\<^isub>2,wp\<^isub>2) = vcpre c\<^isub>2 Q;
  29.135 +       (vc\<^isub>1,wp\<^isub>1) = vcpre c\<^isub>1 wp\<^isub>2
  29.136 +   in (\<lambda>s. vc\<^isub>1 s \<and> vc\<^isub>2 s, wp\<^isub>1))" |
  29.137 +"vcpre (Aif b c\<^isub>1 c\<^isub>2) Q =
  29.138 +  (let (vc\<^isub>2,wp\<^isub>2) = vcpre c\<^isub>2 Q;
  29.139 +       (vc\<^isub>1,wp\<^isub>1) = vcpre c\<^isub>1 Q
  29.140 +   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)))" |
  29.141 +"vcpre (Awhile b I c) Q =
  29.142 +  (let (vcc,wpc) = vcpre c I
  29.143 +   in (\<lambda>s. (I s \<and> \<not> bval b s \<longrightarrow> Q s) \<and>
  29.144 +           (I s \<and> bval b s \<longrightarrow> wpc s) \<and> vcc s, I))"
  29.145 +
  29.146 +lemma vcpre_vc_pre: "vcpre c Q = (vc c Q, pre c Q)"
  29.147 +by (induct c arbitrary: Q) (simp_all add: Let_def)
  29.148 +
  29.149 +end
    30.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    30.2 +++ b/src/HOL/IMP/Vars.thy	Mon Jun 06 16:29:38 2011 +0200
    30.3 @@ -0,0 +1,74 @@
    30.4 +(* Author: Tobias Nipkow *)
    30.5 +
    30.6 +header "Definite Assignment Analysis"
    30.7 +
    30.8 +theory Vars imports Util BExp
    30.9 +begin
   30.10 +
   30.11 +subsection "The Variables in an Expression"
   30.12 +
   30.13 +text{* We need to collect the variables in both arithmetic and boolean
   30.14 +expressions. For a change we do not introduce two functions, e.g.\ @{text
   30.15 +avars} and @{text bvars}, but we overload the name @{text vars}
   30.16 +via a \emph{type class}, a device that originated with Haskell: *}
   30.17 + 
   30.18 +class vars =
   30.19 +fixes vars :: "'a \<Rightarrow> name set"
   30.20 +
   30.21 +text{* This defines a type class ``vars'' with a single
   30.22 +function of (coincidentally) the same name. Then we define two separated
   30.23 +instances of the class, one for @{typ aexp} and one for @{typ bexp}: *}
   30.24 +
   30.25 +instantiation aexp :: vars
   30.26 +begin
   30.27 +
   30.28 +fun vars_aexp :: "aexp \<Rightarrow> name set" where
   30.29 +"vars_aexp (N n) = {}" |
   30.30 +"vars_aexp (V x) = {x}" |
   30.31 +"vars_aexp (Plus a\<^isub>1 a\<^isub>2) = vars_aexp a\<^isub>1 \<union> vars_aexp a\<^isub>2"
   30.32 +
   30.33 +instance ..
   30.34 +
   30.35 +end
   30.36 +
   30.37 +value "vars(Plus (V ''x'') (V ''y''))"
   30.38 +
   30.39 +text{* We need to convert functions to lists before we can view them: *}
   30.40 +
   30.41 +value "show  (vars(Plus (V ''x'') (V ''y'')))"
   30.42 +
   30.43 +instantiation bexp :: vars
   30.44 +begin
   30.45 +
   30.46 +fun vars_bexp :: "bexp \<Rightarrow> name set" where
   30.47 +"vars_bexp (B bv) = {}" |
   30.48 +"vars_bexp (Not b) = vars_bexp b" |
   30.49 +"vars_bexp (And b\<^isub>1 b\<^isub>2) = vars_bexp b\<^isub>1 \<union> vars_bexp b\<^isub>2" |
   30.50 +"vars_bexp (Less a\<^isub>1 a\<^isub>2) = vars a\<^isub>1 \<union> vars a\<^isub>2"
   30.51 +
   30.52 +instance ..
   30.53 +
   30.54 +end
   30.55 +
   30.56 +value "show  (vars(Less (Plus (V ''z'') (V ''y'')) (V ''x'')))"
   30.57 +
   30.58 +abbreviation
   30.59 +  eq_on :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> bool"
   30.60 + ("(_ =/ _/ on _)" [50,0,50] 50) where
   30.61 +"f = g on X == \<forall> x \<in> X. f x = g x"
   30.62 +
   30.63 +lemma aval_eq_if_eq_on_vars[simp]:
   30.64 +  "s\<^isub>1 = s\<^isub>2 on vars a \<Longrightarrow> aval a s\<^isub>1 = aval a s\<^isub>2"
   30.65 +apply(induct a)
   30.66 +apply simp_all
   30.67 +done
   30.68 +
   30.69 +lemma bval_eq_if_eq_on_vars:
   30.70 +  "s\<^isub>1 = s\<^isub>2 on vars b \<Longrightarrow> bval b s\<^isub>1 = bval b s\<^isub>2"
   30.71 +proof(induct b)
   30.72 +  case (Less a1 a2)
   30.73 +  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
   30.74 +  thus ?case by simp
   30.75 +qed simp_all
   30.76 +
   30.77 +end
    31.1 --- a/src/HOL/IsaMakefile	Mon Jun 06 16:29:13 2011 +0200
    31.2 +++ b/src/HOL/IsaMakefile	Mon Jun 06 16:29:38 2011 +0200
    31.3 @@ -527,8 +527,16 @@
    31.4  HOL-IMP: HOL $(LOG)/HOL-IMP.gz
    31.5  
    31.6  $(LOG)/HOL-IMP.gz: $(OUT)/HOL IMP/ASM.thy IMP/AExp.thy IMP/BExp.thy	\
    31.7 -  IMP/Big_Step.thy IMP/Com.thy IMP/Compiler.thy IMP/Denotation.thy 	\
    31.8 -  IMP/Poly_Types.thy IMP/Small_Step.thy IMP/Star.thy IMP/Types.thy	\
    31.9 +  IMP/Big_Step.thy IMP/C_like.thy IMP/Com.thy IMP/Compiler.thy \
   31.10 +  IMP/Def_Ass.thy IMP/Def_Ass_Big.thy IMP/Def_Ass_Exp.thy \
   31.11 +  IMP/Def_Ass_Small.thy IMP/Def_Ass_Sound_Big.thy \
   31.12 +  IMP/Def_Ass_Sound_Small.thy IMP/Denotation.thy IMP/Hoare.thy \
   31.13 +  IMP/HoareT.thy IMP/Hoare_Examples.thy IMP/Hoare_Sound_Complete.thy \
   31.14 +  IMP/Live.thy IMP/OO.thy IMP/Poly_Types.thy IMP/Procs.thy \
   31.15 +  IMP/Procs_Dyn_Vars_Dyn.thy IMP/Procs_Stat_Vars_Dyn.thy \
   31.16 +  IMP/Procs_Stat_Vars_Stat.thy IMP/Sec_Type_Expr.thy IMP/Sec_Typing.thy \
   31.17 +  IMP/Sec_TypingT.thy IMP/Small_Step.thy IMP/Star.thy IMP/Types.thy \
   31.18 +  IMP/Util.thy IMP/VC.thy IMP/Vars.thy \
   31.19    IMP/ROOT.ML IMP/document/root.tex IMP/document/root.bib
   31.20  	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL IMP
   31.21