# HG changeset patch
# User nipkow
# Date 1268415802 -3600
# Node ID bdfca0d37fee0ebae2ce19d2d585046944ea88e8
# Parent  b4d818b0d7c421543e3be8554d24e9d609ea5827# Parent  8e7dba5f00f5a246ba9a0380e2d4262b22af33f9
merged

diff -r b4d818b0d7c4 -r bdfca0d37fee src/HOL/IMP/Hoare.thy
--- 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
diff -r b4d818b0d7c4 -r bdfca0d37fee src/HOL/IMP/Hoare_Den.thy
--- /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
diff -r b4d818b0d7c4 -r bdfca0d37fee src/HOL/IMP/Hoare_Op.thy
--- 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)"
diff -r b4d818b0d7c4 -r bdfca0d37fee src/HOL/IMP/ROOT.ML
--- 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"];
diff -r b4d818b0d7c4 -r bdfca0d37fee src/HOL/IMP/VC.thy
--- 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))"