--- a/src/HOL/IMP/Hoare.thy Fri Mar 12 16:02:42 2010 +0100
+++ b/src/HOL/IMP/Hoare.thy Fri Mar 12 18:43:22 2010 +0100
@@ -6,14 +6,10 @@
header "Inductive Definition of Hoare Logic"
-theory Hoare imports Denotation begin
+theory Hoare imports Natural begin
types assn = "state => bool"
-definition
- hoare_valid :: "[assn,com,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50) where
- "|= {P}c{Q} = (!s t. (s,t) : C(c) --> P s --> Q t)"
-
inductive
hoare :: "assn => com => assn => bool" ("|- ({(1_)}/ (_)/ {(1_)})" 50)
where
@@ -27,139 +23,20 @@
| conseq: "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==>
|- {P'}c{Q'}"
-definition
- wp :: "com => assn => assn" where
- "wp c Q = (%s. !t. (s,t) : C(c) --> Q t)"
-
-(*
-Soundness (and part of) relative completeness of Hoare rules
-wrt denotational semantics
-*)
-
lemma strengthen_pre: "[| !s. P' s --> P s; |- {P}c{Q} |] ==> |- {P'}c{Q}"
by (blast intro: conseq)
lemma weaken_post: "[| |- {P}c{Q}; !s. Q s --> Q' s |] ==> |- {P}c{Q'}"
by (blast intro: conseq)
-lemma hoare_sound: "|- {P}c{Q} ==> |= {P}c{Q}"
-proof(induct rule: hoare.induct)
- case (While P b c)
- { fix s t
- let ?G = "Gamma b (C c)"
- assume "(s,t) \<in> lfp ?G"
- hence "P s \<longrightarrow> P t \<and> \<not> b t"
- proof(rule lfp_induct2)
- show "mono ?G" by(rule Gamma_mono)
- next
- fix s t assume "(s,t) \<in> ?G (lfp ?G \<inter> {(s,t). P s \<longrightarrow> P t \<and> \<not> b t})"
- thus "P s \<longrightarrow> P t \<and> \<not> b t" using While.hyps
- by(auto simp: hoare_valid_def Gamma_def)
- qed
- }
- thus ?case by(simp add:hoare_valid_def)
-qed (auto simp: hoare_valid_def)
+lemma While':
+assumes "|- {%s. P s & b s} c {P}" and "ALL s. P s & \<not> b s \<longrightarrow> Q s"
+shows "|- {P} \<WHILE> b \<DO> c {Q}"
+by(rule weaken_post[OF While[OF assms(1)] assms(2)])
-lemma wp_SKIP: "wp \<SKIP> Q = Q"
-by (simp add: wp_def)
-
-lemma wp_Ass: "wp (x:==a) Q = (%s. Q(s[x\<mapsto>a s]))"
-by (simp add: wp_def)
-
-lemma wp_Semi: "wp (c;d) Q = wp c (wp d Q)"
-by (rule ext) (auto simp: wp_def)
-
-lemma wp_If:
- "wp (\<IF> b \<THEN> c \<ELSE> d) Q = (%s. (b s --> wp c Q s) & (~b s --> wp d Q s))"
-by (rule ext) (auto simp: wp_def)
-
-lemma wp_While_If:
- "wp (\<WHILE> b \<DO> c) Q s =
- wp (IF b THEN c;\<WHILE> b \<DO> c ELSE SKIP) Q s"
-by(simp only: wp_def C_While_If)
-
-(*Not suitable for rewriting: LOOPS!*)
-lemma wp_While_if:
- "wp (\<WHILE> b \<DO> c) Q s = (if b s then wp (c;\<WHILE> b \<DO> c) Q s else Q s)"
-by(simp add:wp_While_If wp_If wp_SKIP)
-
-lemma wp_While_True: "b s ==>
- wp (\<WHILE> b \<DO> c) Q s = wp (c;\<WHILE> b \<DO> c) Q s"
-by(simp add: wp_While_if)
-
-lemma wp_While_False: "~b s ==> wp (\<WHILE> b \<DO> c) Q s = Q s"
-by(simp add: wp_While_if)
-
-lemmas [simp] = wp_SKIP wp_Ass wp_Semi wp_If wp_While_True wp_While_False
-
-lemma wp_While: "wp (\<WHILE> b \<DO> c) Q s =
- (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))"
-apply (simp (no_asm))
-apply (rule iffI)
- apply (rule weak_coinduct)
- apply (erule CollectI)
- apply safe
- apply simp
- apply simp
-apply (simp add: wp_def Gamma_def)
-apply (intro strip)
-apply (rule mp)
- prefer 2 apply (assumption)
-apply (erule lfp_induct2)
-apply (fast intro!: monoI)
-apply (subst gfp_unfold)
- apply (fast intro!: monoI)
-apply fast
-done
-
-declare C_while [simp del]
+lemmas [simp] = skip ass semi If
lemmas [intro!] = hoare.skip hoare.ass hoare.semi hoare.If
-lemma wp_is_pre: "|- {wp c Q} c {Q}"
-proof(induct c arbitrary: Q)
- case SKIP show ?case by auto
-next
- case Assign show ?case by auto
-next
- case Semi thus ?case by auto
-next
- case (Cond b c1 c2)
- let ?If = "IF b THEN c1 ELSE c2"
- show ?case
- proof(rule If)
- show "|- {\<lambda>s. wp ?If Q s \<and> b s} c1 {Q}"
- proof(rule strengthen_pre[OF _ Cond(1)])
- show "\<forall>s. wp ?If Q s \<and> b s \<longrightarrow> wp c1 Q s" by auto
- qed
- show "|- {\<lambda>s. wp ?If Q s \<and> \<not> b s} c2 {Q}"
- proof(rule strengthen_pre[OF _ Cond(2)])
- show "\<forall>s. wp ?If Q s \<and> \<not> b s \<longrightarrow> wp c2 Q s" by auto
- qed
- qed
-next
- case (While b c)
- let ?w = "WHILE b DO c"
- have "|- {wp ?w Q} ?w {\<lambda>s. wp ?w Q s \<and> \<not> b s}"
- proof(rule hoare.While)
- show "|- {\<lambda>s. wp ?w Q s \<and> b s} c {wp ?w Q}"
- proof(rule strengthen_pre[OF _ While(1)])
- show "\<forall>s. wp ?w Q s \<and> b s \<longrightarrow> wp c (wp ?w Q) s" by auto
- qed
- qed
- thus ?case
- proof(rule weaken_post)
- show "\<forall>s. wp ?w Q s \<and> \<not> b s \<longrightarrow> Q s" by auto
- qed
-qed
-
-lemma hoare_relative_complete: assumes "|= {P}c{Q}" shows "|- {P}c{Q}"
-proof(rule conseq)
- show "\<forall>s. P s \<longrightarrow> wp c Q s" using assms
- by (auto simp: hoare_valid_def wp_def)
- show "|- {wp c Q} c {Q}" by(rule wp_is_pre)
- show "\<forall>s. Q s \<longrightarrow> Q s" by auto
-qed
-
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Hoare_Den.thy Fri Mar 12 18:43:22 2010 +0100
@@ -0,0 +1,134 @@
+(* Title: HOL/IMP/Hoare_Def.thy
+ ID: $Id$
+ Author: Tobias Nipkow
+*)
+
+header "Soundness and Completeness wrt Denotational Semantics"
+
+theory Hoare_Den imports Hoare Denotation begin
+
+definition
+ hoare_valid :: "[assn,com,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50) where
+ "|= {P}c{Q} = (!s t. (s,t) : C(c) --> P s --> Q t)"
+
+
+lemma hoare_sound: "|- {P}c{Q} ==> |= {P}c{Q}"
+proof(induct rule: hoare.induct)
+ case (While P b c)
+ { fix s t
+ let ?G = "Gamma b (C c)"
+ assume "(s,t) \<in> lfp ?G"
+ hence "P s \<longrightarrow> P t \<and> \<not> b t"
+ proof(rule lfp_induct2)
+ show "mono ?G" by(rule Gamma_mono)
+ next
+ fix s t assume "(s,t) \<in> ?G (lfp ?G \<inter> {(s,t). P s \<longrightarrow> P t \<and> \<not> b t})"
+ thus "P s \<longrightarrow> P t \<and> \<not> b t" using While.hyps
+ by(auto simp: hoare_valid_def Gamma_def)
+ qed
+ }
+ thus ?case by(simp add:hoare_valid_def)
+qed (auto simp: hoare_valid_def)
+
+
+definition
+ wp :: "com => assn => assn" where
+ "wp c Q = (%s. !t. (s,t) : C(c) --> Q t)"
+
+lemma wp_SKIP: "wp \<SKIP> Q = Q"
+by (simp add: wp_def)
+
+lemma wp_Ass: "wp (x:==a) Q = (%s. Q(s[x\<mapsto>a s]))"
+by (simp add: wp_def)
+
+lemma wp_Semi: "wp (c;d) Q = wp c (wp d Q)"
+by (rule ext) (auto simp: wp_def)
+
+lemma wp_If:
+ "wp (\<IF> b \<THEN> c \<ELSE> d) Q = (%s. (b s --> wp c Q s) & (~b s --> wp d Q s))"
+by (rule ext) (auto simp: wp_def)
+
+lemma wp_While_If:
+ "wp (\<WHILE> b \<DO> c) Q s =
+ wp (IF b THEN c;\<WHILE> b \<DO> c ELSE SKIP) Q s"
+by(simp only: wp_def C_While_If)
+
+(*Not suitable for rewriting: LOOPS!*)
+lemma wp_While_if:
+ "wp (\<WHILE> b \<DO> c) Q s = (if b s then wp (c;\<WHILE> b \<DO> c) Q s else Q s)"
+by(simp add:wp_While_If wp_If wp_SKIP)
+
+lemma wp_While_True: "b s ==>
+ wp (\<WHILE> b \<DO> c) Q s = wp (c;\<WHILE> b \<DO> c) Q s"
+by(simp add: wp_While_if)
+
+lemma wp_While_False: "~b s ==> wp (\<WHILE> b \<DO> c) Q s = Q s"
+by(simp add: wp_While_if)
+
+lemmas [simp] = wp_SKIP wp_Ass wp_Semi wp_If wp_While_True wp_While_False
+
+lemma wp_While: "wp (\<WHILE> b \<DO> c) Q s =
+ (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))"
+apply (simp (no_asm))
+apply (rule iffI)
+ apply (rule weak_coinduct)
+ apply (erule CollectI)
+ apply safe
+ apply simp
+ apply simp
+apply (simp add: wp_def Gamma_def)
+apply (intro strip)
+apply (rule mp)
+ prefer 2 apply (assumption)
+apply (erule lfp_induct2)
+apply (fast intro!: monoI)
+apply (subst gfp_unfold)
+ apply (fast intro!: monoI)
+apply fast
+done
+
+declare C_while [simp del]
+
+lemma wp_is_pre: "|- {wp c Q} c {Q}"
+proof(induct c arbitrary: Q)
+ case SKIP show ?case by auto
+next
+ case Assign show ?case by auto
+next
+ case Semi thus ?case by auto
+next
+ case (Cond b c1 c2)
+ let ?If = "IF b THEN c1 ELSE c2"
+ show ?case
+ proof(rule If)
+ show "|- {\<lambda>s. wp ?If Q s \<and> b s} c1 {Q}"
+ proof(rule strengthen_pre[OF _ Cond(1)])
+ show "\<forall>s. wp ?If Q s \<and> b s \<longrightarrow> wp c1 Q s" by auto
+ qed
+ show "|- {\<lambda>s. wp ?If Q s \<and> \<not> b s} c2 {Q}"
+ proof(rule strengthen_pre[OF _ Cond(2)])
+ show "\<forall>s. wp ?If Q s \<and> \<not> b s \<longrightarrow> wp c2 Q s" by auto
+ qed
+ qed
+next
+ case (While b c)
+ let ?w = "WHILE b DO c"
+ show ?case
+ proof(rule While')
+ show "|- {\<lambda>s. wp ?w Q s \<and> b s} c {wp ?w Q}"
+ proof(rule strengthen_pre[OF _ While(1)])
+ show "\<forall>s. wp ?w Q s \<and> b s \<longrightarrow> wp c (wp ?w Q) s" by auto
+ qed
+ show "\<forall>s. wp ?w Q s \<and> \<not> b s \<longrightarrow> Q s" by auto
+ qed
+qed
+
+lemma hoare_relative_complete: assumes "|= {P}c{Q}" shows "|- {P}c{Q}"
+proof(rule conseq)
+ show "\<forall>s. P s \<longrightarrow> wp c Q s" using assms
+ by (auto simp: hoare_valid_def wp_def)
+ show "|- {wp c Q} c {Q}" by(rule wp_is_pre)
+ show "\<forall>s. Q s \<longrightarrow> Q s" by auto
+qed
+
+end
--- a/src/HOL/IMP/Hoare_Op.thy Fri Mar 12 16:02:42 2010 +0100
+++ b/src/HOL/IMP/Hoare_Op.thy Fri Mar 12 18:43:22 2010 +0100
@@ -3,37 +3,14 @@
Author: Tobias Nipkow
*)
-header "Hoare Logic (justified wrt operational semantics)"
+header "Soundness and Completeness wrt Operational Semantics"
-theory Hoare_Op imports Natural begin
-
-types assn = "state => bool"
+theory Hoare_Op imports Hoare begin
definition
hoare_valid :: "[assn,com,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50) where
"|= {P}c{Q} = (!s t. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t --> P s --> Q t)"
-inductive
- hoare :: "assn => com => assn => bool" ("|- ({(1_)}/ (_)/ {(1_)})" 50)
-where
- skip: "|- {P}\<SKIP>{P}"
-| ass: "|- {%s. P(s[x\<mapsto>a s])} x:==a {P}"
-| semi: "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}"
-| If: "[| |- {%s. P s & b s}c{Q}; |- {%s. P s & ~b s}d{Q} |] ==>
- |- {P} \<IF> b \<THEN> c \<ELSE> d {Q}"
-| While: "|- {%s. P s & b s} c {P} ==>
- |- {P} \<WHILE> b \<DO> c {%s. P s & ~b s}"
-| conseq: "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==>
- |- {P'}c{Q'}"
-
-lemmas [simp] = skip ass semi If
-
-lemma strengthen_pre: "[| !s. P' s --> P s; |- {P}c{Q} |] ==> |- {P'}c{Q}"
-by (blast intro: conseq)
-
-lemma weaken_post: "[| |- {P}c{Q}; !s. Q s --> Q' s |] ==> |- {P}c{Q'}"
-by (blast intro: conseq)
-
lemma hoare_sound: "|- {P}c{Q} ==> |= {P}c{Q}"
proof(induct rule: hoare.induct)
case (While P b c)
@@ -51,7 +28,6 @@
thus ?case unfolding hoare_valid_def by blast
qed (auto simp: hoare_valid_def)
-
definition
wp :: "com => assn => assn" where
"wp c Q = (%s. !t. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t --> Q t)"
--- a/src/HOL/IMP/ROOT.ML Fri Mar 12 16:02:42 2010 +0100
+++ b/src/HOL/IMP/ROOT.ML Fri Mar 12 18:43:22 2010 +0100
@@ -6,4 +6,4 @@
Caveat: HOLCF/IMP depends on HOL/IMP
*)
-use_thys ["Expr", "Transition", "Hoare_Op", "VC", "Examples", "Compiler0", "Compiler", "Live"];
+use_thys ["Expr", "Transition", "VC", "Hoare_Den", "Examples", "Compiler0", "Compiler", "Live"];
--- a/src/HOL/IMP/VC.thy Fri Mar 12 16:02:42 2010 +0100
+++ b/src/HOL/IMP/VC.thy Fri Mar 12 18:43:22 2010 +0100
@@ -10,7 +10,7 @@
header "Verification Conditions"
-theory VC imports Hoare begin
+theory VC imports Hoare_Op begin
datatype acom = Askip
| Aass loc aexp
@@ -63,51 +63,36 @@
Soundness and completeness of vc
*)
-declare hoare.intros [intro]
+declare hoare.conseq [intro]
-lemma l: "!s. P s --> P s" by fast
-lemma vc_sound: "(!s. vc c Q s) --> |- {awp c Q} astrip c {Q}"
-apply (induct c arbitrary: Q)
- apply (simp_all (no_asm))
- apply fast
- apply fast
- apply fast
- (* if *)
- apply atomize
- apply (tactic "deepen_tac @{claset} 4 1")
-(* while *)
-apply atomize
-apply (intro allI impI)
-apply (rule conseq)
- apply (rule l)
- apply (rule While)
- defer
- apply fast
-apply (rule_tac P="awp c fun2" in conseq)
- apply fast
- apply fast
-apply fast
-done
+lemma vc_sound: "(ALL s. vc c Q s) \<Longrightarrow> |- {awp c Q} astrip c {Q}"
+proof(induct c arbitrary: Q)
+ case (Awhile b I c)
+ show ?case
+ proof(simp, rule While')
+ from `\<forall>s. vc (Awhile b I c) Q s`
+ have vc: "ALL s. vc c I s" and IQ: "ALL s. I s \<and> \<not> b s \<longrightarrow> Q s" and
+ awp: "ALL s. I s & b s --> awp c I s" by simp_all
+ from vc have "|- {awp c I} astrip c {I}" using Awhile.hyps by blast
+ with awp show "|- {\<lambda>s. I s \<and> b s} astrip c {I}"
+ by(rule strengthen_pre)
+ show "\<forall>s. I s \<and> \<not> b s \<longrightarrow> Q s" by(rule IQ)
+ qed
+qed auto
-lemma awp_mono [rule_format (no_asm)]:
- "!P Q. (!s. P s --> Q s) --> (!s. awp c P s --> awp c Q s)"
-apply (induct c)
- apply (simp_all (no_asm_simp))
-apply (rule allI, rule allI, rule impI)
-apply (erule allE, erule allE, erule mp)
-apply (erule allE, erule allE, erule mp, assumption)
-done
-lemma vc_mono [rule_format (no_asm)]:
- "!P Q. (!s. P s --> Q s) --> (!s. vc c P s --> vc c Q s)"
-apply (induct c)
- apply (simp_all (no_asm_simp))
-apply safe
-apply (erule allE,erule allE,erule impE,erule_tac [2] allE,erule_tac [2] mp)
-prefer 2 apply assumption
-apply (fast elim: awp_mono)
-done
+lemma awp_mono:
+ "(!s. P s --> Q s) ==> awp c P s ==> awp c Q s"
+proof (induct c arbitrary: P Q s)
+ case Asemi thus ?case by simp metis
+qed simp_all
+
+lemma vc_mono:
+ "(!s. P s --> Q s) ==> vc c P s ==> vc c Q s"
+proof(induct c arbitrary: P Q)
+ case Asemi thus ?case by simp (metis awp_mono)
+qed simp_all
lemma vc_complete: assumes der: "|- {P}c{Q}"
shows "(\<exists>ac. astrip ac = c & (\<forall>s. vc ac Q s) & (\<forall>s. P s --> awp ac Q s))"