--- a/src/HOL/Isar_Examples/Hoare.thy Fri Feb 21 17:06:48 2014 +0100
+++ b/src/HOL/Isar_Examples/Hoare.thy Fri Feb 21 18:23:11 2014 +0100
@@ -22,41 +22,39 @@
type_synonym 'a assn = "'a set"
datatype 'a com =
- Basic "'a => 'a"
+ Basic "'a \<Rightarrow> 'a"
| Seq "'a com" "'a com" ("(_;/ _)" [60, 61] 60)
| Cond "'a bexp" "'a com" "'a com"
| While "'a bexp" "'a assn" "'a com"
abbreviation Skip ("SKIP")
- where "SKIP == Basic id"
-
-type_synonym 'a sem = "'a => 'a => bool"
+ where "SKIP \<equiv> Basic id"
-primrec iter :: "nat => 'a bexp => 'a sem => 'a sem"
-where
- "iter 0 b S s s' = (s ~: b & s = s')"
-| "iter (Suc n) b S s s' = (s : b & (EX s''. S s s'' & iter n b S s'' s'))"
+type_synonym 'a sem = "'a \<Rightarrow> 'a \<Rightarrow> bool"
-primrec Sem :: "'a com => 'a sem"
+primrec iter :: "nat \<Rightarrow> 'a bexp \<Rightarrow> 'a sem \<Rightarrow> 'a sem"
where
- "Sem (Basic f) s s' = (s' = f s)"
-| "Sem (c1; c2) s s' = (EX s''. Sem c1 s s'' & Sem c2 s'' s')"
-| "Sem (Cond b c1 c2) s s' =
- (if s : b then Sem c1 s s' else Sem c2 s s')"
-| "Sem (While b x c) s s' = (EX n. iter n b (Sem c) s s')"
+ "iter 0 b S s s' \<longleftrightarrow> s \<notin> b \<and> s = s'"
+| "iter (Suc n) b S s s' \<longleftrightarrow> s \<in> b \<and> (\<exists>s''. S s s'' \<and> iter n b S s'' s')"
-definition Valid :: "'a bexp => 'a com => 'a bexp => bool"
- ("(3|- _/ (2_)/ _)" [100, 55, 100] 50)
- where "|- P c Q \<longleftrightarrow> (\<forall>s s'. Sem c s s' --> s : P --> s' : Q)"
+primrec Sem :: "'a com \<Rightarrow> 'a sem"
+where
+ "Sem (Basic f) s s' \<longleftrightarrow> s' = f s"
+| "Sem (c1; c2) s s' \<longleftrightarrow> (\<exists>s''. Sem c1 s s'' \<and> Sem c2 s'' s')"
+| "Sem (Cond b c1 c2) s s' \<longleftrightarrow>
+ (if s \<in> b then Sem c1 s s' else Sem c2 s s')"
+| "Sem (While b x c) s s' \<longleftrightarrow> (\<exists>n. iter n b (Sem c) s s')"
-notation (xsymbols) Valid ("(3\<turnstile> _/ (2_)/ _)" [100, 55, 100] 50)
+definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
+ ("(3\<turnstile> _/ (2_)/ _)" [100, 55, 100] 50)
+ where "\<turnstile> P c Q \<longleftrightarrow> (\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> P \<longrightarrow> s' \<in> Q)"
lemma ValidI [intro?]:
- "(!!s s'. Sem c s s' ==> s : P ==> s' : Q) ==> |- P c Q"
+ "(\<And>s s'. Sem c s s' \<Longrightarrow> s \<in> P \<Longrightarrow> s' \<in> Q) \<Longrightarrow> \<turnstile> P c Q"
by (simp add: Valid_def)
lemma ValidD [dest?]:
- "|- P c Q ==> Sem c s s' ==> s : P ==> s' : Q"
+ "\<turnstile> P c Q \<Longrightarrow> Sem c s s' \<Longrightarrow> s \<in> P \<Longrightarrow> s' \<in> Q"
by (simp add: Valid_def)
@@ -71,12 +69,13 @@
to the state space. This subsumes the common rules of \name{skip}
and \name{assign}, as formulated in \S\ref{sec:hoare-isar}. *}
-theorem basic: "|- {s. f s : P} (Basic f) P"
+theorem basic: "\<turnstile> {s. f s \<in> P} (Basic f) P"
proof
- fix s s' assume s: "s : {s. f s : P}"
+ fix s s'
+ assume s: "s \<in> {s. f s \<in> P}"
assume "Sem (Basic f) s s'"
then have "s' = f s" by simp
- with s show "s' : P" by simp
+ with s show "s' \<in> P" by simp
qed
text {*
@@ -84,26 +83,27 @@
established in a straight forward manner as follows.
*}
-theorem seq: "|- P c1 Q ==> |- Q c2 R ==> |- P (c1; c2) R"
+theorem seq: "\<turnstile> P c1 Q \<Longrightarrow> \<turnstile> Q c2 R \<Longrightarrow> \<turnstile> P (c1; c2) R"
proof
- assume cmd1: "|- P c1 Q" and cmd2: "|- Q c2 R"
- fix s s' assume s: "s : P"
+ assume cmd1: "\<turnstile> P c1 Q" and cmd2: "\<turnstile> Q c2 R"
+ fix s s'
+ assume s: "s \<in> P"
assume "Sem (c1; c2) s s'"
then obtain s'' where sem1: "Sem c1 s s''" and sem2: "Sem c2 s'' s'"
by auto
- from cmd1 sem1 s have "s'' : Q" ..
- with cmd2 sem2 show "s' : R" ..
+ from cmd1 sem1 s have "s'' \<in> Q" ..
+ with cmd2 sem2 show "s' \<in> R" ..
qed
-theorem conseq: "P' <= P ==> |- P c Q ==> Q <= Q' ==> |- P' c Q'"
+theorem conseq: "P' \<subseteq> P \<Longrightarrow> \<turnstile> P c Q \<Longrightarrow> Q \<subseteq> Q' \<Longrightarrow> \<turnstile> P' c Q'"
proof
- assume P'P: "P' <= P" and QQ': "Q <= Q'"
- assume cmd: "|- P c Q"
+ assume P'P: "P' \<subseteq> P" and QQ': "Q \<subseteq> Q'"
+ assume cmd: "\<turnstile> P c Q"
fix s s' :: 'a
assume sem: "Sem c s s'"
- assume "s : P'" with P'P have "s : P" ..
- with cmd sem have "s' : Q" ..
- with QQ' show "s' : Q'" ..
+ assume "s : P'" with P'P have "s \<in> P" ..
+ with cmd sem have "s' \<in> Q" ..
+ with QQ' show "s' \<in> Q'" ..
qed
text {* The rule for conditional commands is directly reflected by the
@@ -111,26 +111,27 @@
which cases apply. *}
theorem cond:
- assumes case_b: "|- (P Int b) c1 Q"
- and case_nb: "|- (P Int -b) c2 Q"
- shows "|- P (Cond b c1 c2) Q"
+ assumes case_b: "\<turnstile> (P \<inter> b) c1 Q"
+ and case_nb: "\<turnstile> (P \<inter> -b) c2 Q"
+ shows "\<turnstile> P (Cond b c1 c2) Q"
proof
- fix s s' assume s: "s : P"
+ fix s s'
+ assume s: "s \<in> P"
assume sem: "Sem (Cond b c1 c2) s s'"
- show "s' : Q"
+ show "s' \<in> Q"
proof cases
- assume b: "s : b"
+ assume b: "s \<in> b"
from case_b show ?thesis
proof
from sem b show "Sem c1 s s'" by simp
- from s b show "s : P Int b" by simp
+ from s b show "s \<in> P \<inter> b" by simp
qed
next
- assume nb: "s ~: b"
+ assume nb: "s \<notin> b"
from case_nb show ?thesis
proof
from sem nb show "Sem c2 s s'" by simp
- from s nb show "s : P Int -b" by simp
+ from s nb show "s : P \<inter> -b" by simp
qed
qed
qed
@@ -143,22 +144,22 @@
of the semantics of \texttt{WHILE}. *}
theorem while:
- assumes body: "|- (P Int b) c P"
- shows "|- P (While b X c) (P Int -b)"
+ assumes body: "\<turnstile> (P \<inter> b) c P"
+ shows "\<turnstile> P (While b X c) (P \<inter> -b)"
proof
- fix s s' assume s: "s : P"
+ fix s s' assume s: "s \<in> P"
assume "Sem (While b X c) s s'"
then obtain n where "iter n b (Sem c) s s'" by auto
- from this and s show "s' : P Int -b"
+ from this and s show "s' \<in> P \<inter> -b"
proof (induct n arbitrary: s)
case 0
then show ?case by auto
next
case (Suc n)
- then obtain s'' where b: "s : b" and sem: "Sem c s s''"
+ then obtain s'' where b: "s \<in> b" and sem: "Sem c s s''"
and iter: "iter n b (Sem c) s'' s'" by auto
- from Suc and b have "s : P Int b" by simp
- with body sem have "s'' : P" ..
+ from Suc and b have "s \<in> P \<inter> b" by simp
+ with body sem have "s'' \<in> P" ..
with iter show ?case by (rule Suc)
qed
qed
@@ -188,29 +189,26 @@
@{ML Syntax_Trans.quote_tr'},). *}
syntax
- "_quote" :: "'b => ('a => 'b)" ("(.'(_').)" [0] 1000)
- "_antiquote" :: "('a => 'b) => 'b" ("\<acute>_" [1000] 1000)
+ "_quote" :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("(.'(_').)" [0] 1000)
+ "_antiquote" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b" ("\<acute>_" [1000] 1000)
"_Subst" :: "'a bexp \<Rightarrow> 'b \<Rightarrow> idt \<Rightarrow> 'a bexp"
("_[_'/\<acute>_]" [1000] 999)
- "_Assert" :: "'a => 'a set" ("(.{_}.)" [0] 1000)
- "_Assign" :: "idt => 'b => 'a com" ("(\<acute>_ :=/ _)" [70, 65] 61)
- "_Cond" :: "'a bexp => 'a com => 'a com => 'a com"
+ "_Assert" :: "'a \<Rightarrow> 'a set" ("(\<lbrace>_\<rbrace>)" [0] 1000)
+ "_Assign" :: "idt \<Rightarrow> 'b \<Rightarrow> 'a com" ("(\<acute>_ :=/ _)" [70, 65] 61)
+ "_Cond" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com \<Rightarrow> 'a com"
("(0IF _/ THEN _/ ELSE _/ FI)" [0, 0, 0] 61)
- "_While_inv" :: "'a bexp => 'a assn => 'a com => 'a com"
+ "_While_inv" :: "'a bexp \<Rightarrow> 'a assn \<Rightarrow> 'a com \<Rightarrow> 'a com"
("(0WHILE _/ INV _ //DO _ /OD)" [0, 0, 0] 61)
- "_While" :: "'a bexp => 'a com => 'a com"
+ "_While" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com"
("(0WHILE _ //DO _ /OD)" [0, 0] 61)
-syntax (xsymbols)
- "_Assert" :: "'a => 'a set" ("(\<lbrace>_\<rbrace>)" [0] 1000)
-
translations
- ".{b}." => "CONST Collect .(b)."
- "B [a/\<acute>x]" => ".{\<acute>(_update_name x (\<lambda>_. a)) \<in> B}."
- "\<acute>x := a" => "CONST Basic .(\<acute>(_update_name x (\<lambda>_. a)))."
- "IF b THEN c1 ELSE c2 FI" => "CONST Cond .{b}. c1 c2"
- "WHILE b INV i DO c OD" => "CONST While .{b}. i c"
- "WHILE b DO c OD" == "WHILE b INV CONST undefined DO c OD"
+ "\<lbrace>b\<rbrace>" \<rightharpoonup> "CONST Collect .(b)."
+ "B [a/\<acute>x]" \<rightharpoonup> "\<lbrace>\<acute>(_update_name x (\<lambda>_. a)) \<in> B\<rbrace>"
+ "\<acute>x := a" \<rightharpoonup> "CONST Basic .(\<acute>(_update_name x (\<lambda>_. a)))."
+ "IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "CONST Cond \<lbrace>b\<rbrace> c1 c2"
+ "WHILE b INV i DO c OD" \<rightharpoonup> "CONST While \<lbrace>b\<rbrace> i c"
+ "WHILE b DO c OD" \<rightleftharpoons> "WHILE b INV CONST undefined DO c OD"
parse_translation {*
let
@@ -259,28 +257,28 @@
calculational proofs, with the inclusion expressed in terms of sets
or predicates. Reversed order is supported as well. *}
-lemma [trans]: "|- P c Q ==> P' <= P ==> |- P' c Q"
+lemma [trans]: "\<turnstile> P c Q \<Longrightarrow> P' \<subseteq> P \<Longrightarrow> \<turnstile> P' c Q"
by (unfold Valid_def) blast
-lemma [trans] : "P' <= P ==> |- P c Q ==> |- P' c Q"
+lemma [trans] : "P' \<subseteq> P \<Longrightarrow> \<turnstile> P c Q \<Longrightarrow> \<turnstile> P' c Q"
by (unfold Valid_def) blast
-lemma [trans]: "Q <= Q' ==> |- P c Q ==> |- P c Q'"
+lemma [trans]: "Q \<subseteq> Q' \<Longrightarrow> \<turnstile> P c Q \<Longrightarrow> \<turnstile> P c Q'"
by (unfold Valid_def) blast
-lemma [trans]: "|- P c Q ==> Q <= Q' ==> |- P c Q'"
+lemma [trans]: "\<turnstile> P c Q \<Longrightarrow> Q \<subseteq> Q' \<Longrightarrow> \<turnstile> P c Q'"
by (unfold Valid_def) blast
lemma [trans]:
- "|- .{\<acute>P}. c Q ==> (!!s. P' s --> P s) ==> |- .{\<acute>P'}. c Q"
+ "\<turnstile> \<lbrace>\<acute>P\<rbrace> c Q \<Longrightarrow> (\<And>s. P' s \<longrightarrow> P s) \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P'\<rbrace> c Q"
by (simp add: Valid_def)
lemma [trans]:
- "(!!s. P' s --> P s) ==> |- .{\<acute>P}. c Q ==> |- .{\<acute>P'}. c Q"
+ "(\<And>s. P' s \<longrightarrow> P s) \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P\<rbrace> c Q \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P'\<rbrace> c Q"
by (simp add: Valid_def)
lemma [trans]:
- "|- P c .{\<acute>Q}. ==> (!!s. Q s --> Q' s) ==> |- P c .{\<acute>Q'}."
+ "\<turnstile> P c \<lbrace>\<acute>Q\<rbrace> \<Longrightarrow> (\<And>s. Q s \<longrightarrow> Q' s) \<Longrightarrow> \<turnstile> P c \<lbrace>\<acute>Q'\<rbrace>"
by (simp add: Valid_def)
lemma [trans]:
- "(!!s. Q s --> Q' s) ==> |- P c .{\<acute>Q}. ==> |- P c .{\<acute>Q'}."
+ "(\<And>s. Q s \<longrightarrow> Q' s) \<Longrightarrow> \<turnstile> P c \<lbrace>\<acute>Q\<rbrace> \<Longrightarrow> \<turnstile> P c \<lbrace>\<acute>Q'\<rbrace>"
by (simp add: Valid_def)
@@ -289,13 +287,13 @@
instances for any number of basic assignments, without producing
additional verification conditions.} *}
-lemma skip [intro?]: "|- P SKIP P"
+lemma skip [intro?]: "\<turnstile> P SKIP P"
proof -
- have "|- {s. id s : P} SKIP P" by (rule basic)
+ have "\<turnstile> {s. id s \<in> P} SKIP P" by (rule basic)
then show ?thesis by simp
qed
-lemma assign: "|- P [\<acute>a/\<acute>x::'a] \<acute>x := \<acute>a P"
+lemma assign: "\<turnstile> P [\<acute>a/\<acute>x::'a] \<acute>x := \<acute>a P"
by (rule basic)
text {* Note that above formulation of assignment corresponds to our
@@ -315,7 +313,7 @@
lemmas [trans, intro?] = seq
-lemma seq_assoc [simp]: "( |- P c1;(c2;c3) Q) = ( |- P (c1;c2);c3 Q)"
+lemma seq_assoc [simp]: "\<turnstile> P c1;(c2;c3) Q \<longleftrightarrow> \<turnstile> P (c1;c2);c3 Q"
by (auto simp add: Valid_def)
text {* Conditional statements. *}
@@ -323,30 +321,30 @@
lemmas [trans, intro?] = cond
lemma [trans, intro?]:
- "|- .{\<acute>P & \<acute>b}. c1 Q
- ==> |- .{\<acute>P & ~ \<acute>b}. c2 Q
- ==> |- .{\<acute>P}. IF \<acute>b THEN c1 ELSE c2 FI Q"
+ "\<turnstile> \<lbrace>\<acute>P \<and> \<acute>b\<rbrace> c1 Q
+ \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P \<and> \<not> \<acute>b\<rbrace> c2 Q
+ \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P\<rbrace> IF \<acute>b THEN c1 ELSE c2 FI Q"
by (rule cond) (simp_all add: Valid_def)
text {* While statements --- with optional invariant. *}
lemma [intro?]:
- "|- (P Int b) c P ==> |- P (While b P c) (P Int -b)"
+ "\<turnstile> (P \<inter> b) c P \<Longrightarrow> \<turnstile> P (While b P c) (P \<inter> -b)"
by (rule while)
lemma [intro?]:
- "|- (P Int b) c P ==> |- P (While b undefined c) (P Int -b)"
+ "\<turnstile> (P \<inter> b) c P \<Longrightarrow> \<turnstile> P (While b undefined c) (P \<inter> -b)"
by (rule while)
lemma [intro?]:
- "|- .{\<acute>P & \<acute>b}. c .{\<acute>P}.
- ==> |- .{\<acute>P}. WHILE \<acute>b INV .{\<acute>P}. DO c OD .{\<acute>P & ~ \<acute>b}."
+ "\<turnstile> \<lbrace>\<acute>P \<and> \<acute>b\<rbrace> c \<lbrace>\<acute>P\<rbrace>
+ \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P\<rbrace> WHILE \<acute>b INV \<lbrace>\<acute>P\<rbrace> DO c OD \<lbrace>\<acute>P \<and> \<not> \<acute>b\<rbrace>"
by (simp add: while Collect_conj_eq Collect_neg_eq)
lemma [intro?]:
- "|- .{\<acute>P & \<acute>b}. c .{\<acute>P}.
- ==> |- .{\<acute>P}. WHILE \<acute>b DO c OD .{\<acute>P & ~ \<acute>b}."
+ "\<turnstile> \<lbrace>\<acute>P \<and> \<acute>b\<rbrace> c \<lbrace>\<acute>P\<rbrace>
+ \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P\<rbrace> WHILE \<acute>b DO c OD \<lbrace>\<acute>P \<and> \<not> \<acute>b\<rbrace>"
by (simp add: while Collect_conj_eq Collect_neg_eq)
@@ -378,13 +376,9 @@
by (auto simp: Valid_def)
lemma iter_aux:
- "\<forall>s s'. Sem c s s' --> s : I & s : b --> s' : I ==>
- (\<And>s s'. s : I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' : I & s' ~: b)"
- apply(induct n)
- apply clarsimp
- apply (simp (no_asm_use))
- apply blast
- done
+ "\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> I \<and> s \<in> b \<longrightarrow> s' \<in> I \<Longrightarrow>
+ (\<And>s s'. s \<in> I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' \<in> I \<and> s' \<notin> b)"
+ by (induct n) auto
lemma WhileRule:
"p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i c) q"