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 -value "aval (Plus (V ''x'') (N 5)) (lookup [(''x'',7)])"
1.13 +text {* A little syntax magic to write larger states compactly: *}
1.14
1.15 -value "aval (Plus (V ''x'') (N 5)) (lookup [(''y'',7)])"
1.16 +nonterminal funlets and funlet
1.17 +
1.18 +syntax
1.19 + "_funlet" :: "['a, 'a] => funlet" ("_ /->/ _")
1.20 + "" :: "funlet => funlets" ("_")
1.21 + "_Funlets" :: "[funlet, funlets] => funlets" ("_,/ _")
1.22 + "_Fun" :: "funlets => 'a => 'b" ("(1[_])")
1.23 + "_FunUpd" :: "['a => 'b, funlets] => 'a => 'b" ("_/'(_')" [900,0]900)
1.24 +
1.25 +syntax (xsymbols)
1.26 + "_funlet" :: "['a, 'a] => funlet" ("_ /\<rightarrow>/ _")
1.27 +
1.28 +translations
1.29 + "_FunUpd m (_Funlets xy ms)" == "_FunUpd (_FunUpd m xy) ms"
1.30 + "_FunUpd m (_funlet x y)" == "m(x := y)"
1.31 + "_Fun ms" == "_FunUpd (%_. 0) ms"
1.32 + "_Fun (_Funlets ms1 ms2)" <= "_FunUpd (_Fun ms1) ms2"
1.33 + "_Funlets ms1 (_Funlets ms2 ms3)" <= "_Funlets (_Funlets ms1 ms2) ms3"
1.34 +
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