Reorganized Hoare logic theories; added Hoare_Den
authornipkow
Fri Mar 12 18:42:56 2010 +0100 (2010-03-12)
changeset 357548e7dba5f00f5
parent 35750 41267aebfa5f
child 35755 bdfca0d37fee
Reorganized Hoare logic theories; added Hoare_Den
src/HOL/IMP/Hoare.thy
src/HOL/IMP/Hoare_Den.thy
src/HOL/IMP/Hoare_Op.thy
src/HOL/IMP/ROOT.ML
src/HOL/IMP/VC.thy
     1.1 --- a/src/HOL/IMP/Hoare.thy	Fri Mar 12 15:48:37 2010 +0100
     1.2 +++ b/src/HOL/IMP/Hoare.thy	Fri Mar 12 18:42:56 2010 +0100
     1.3 @@ -6,14 +6,10 @@
     1.4  
     1.5  header "Inductive Definition of Hoare Logic"
     1.6  
     1.7 -theory Hoare imports Denotation begin
     1.8 +theory Hoare imports Natural begin
     1.9  
    1.10  types assn = "state => bool"
    1.11  
    1.12 -definition
    1.13 -  hoare_valid :: "[assn,com,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50) where
    1.14 -  "|= {P}c{Q} = (!s t. (s,t) : C(c) --> P s --> Q t)"
    1.15 -
    1.16  inductive
    1.17    hoare :: "assn => com => assn => bool" ("|- ({(1_)}/ (_)/ {(1_)})" 50)
    1.18  where
    1.19 @@ -27,139 +23,20 @@
    1.20  | conseq: "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==>
    1.21            |- {P'}c{Q'}"
    1.22  
    1.23 -definition
    1.24 -  wp :: "com => assn => assn" where
    1.25 -  "wp c Q = (%s. !t. (s,t) : C(c) --> Q t)"
    1.26 -
    1.27 -(*
    1.28 -Soundness (and part of) relative completeness of Hoare rules
    1.29 -wrt denotational semantics
    1.30 -*)
    1.31 -
    1.32  lemma strengthen_pre: "[| !s. P' s --> P s; |- {P}c{Q} |] ==> |- {P'}c{Q}"
    1.33  by (blast intro: conseq)
    1.34  
    1.35  lemma weaken_post: "[| |- {P}c{Q}; !s. Q s --> Q' s |] ==> |- {P}c{Q'}"
    1.36  by (blast intro: conseq)
    1.37  
    1.38 -lemma hoare_sound: "|- {P}c{Q} ==> |= {P}c{Q}"
    1.39 -proof(induct rule: hoare.induct)
    1.40 -  case (While P b c)
    1.41 -  { fix s t
    1.42 -    let ?G = "Gamma b (C c)"
    1.43 -    assume "(s,t) \<in> lfp ?G"
    1.44 -    hence "P s \<longrightarrow> P t \<and> \<not> b t"
    1.45 -    proof(rule lfp_induct2)
    1.46 -      show "mono ?G" by(rule Gamma_mono)
    1.47 -    next
    1.48 -      fix s t assume "(s,t) \<in> ?G (lfp ?G \<inter> {(s,t). P s \<longrightarrow> P t \<and> \<not> b t})"
    1.49 -      thus "P s \<longrightarrow> P t \<and> \<not> b t" using While.hyps
    1.50 -        by(auto simp: hoare_valid_def Gamma_def)
    1.51 -    qed
    1.52 -  }
    1.53 -  thus ?case by(simp add:hoare_valid_def)
    1.54 -qed (auto simp: hoare_valid_def)
    1.55 +lemma While':
    1.56 +assumes "|- {%s. P s & b s} c {P}" and "ALL s. P s & \<not> b s \<longrightarrow> Q s"
    1.57 +shows "|- {P} \<WHILE> b \<DO> c {Q}"
    1.58 +by(rule weaken_post[OF While[OF assms(1)] assms(2)])
    1.59  
    1.60  
    1.61 -lemma wp_SKIP: "wp \<SKIP> Q = Q"
    1.62 -by (simp add: wp_def)
    1.63 -
    1.64 -lemma wp_Ass: "wp (x:==a) Q = (%s. Q(s[x\<mapsto>a s]))"
    1.65 -by (simp add: wp_def)
    1.66 -
    1.67 -lemma wp_Semi: "wp (c;d) Q = wp c (wp d Q)"
    1.68 -by (rule ext) (auto simp: wp_def)
    1.69 -
    1.70 -lemma wp_If:
    1.71 - "wp (\<IF> b \<THEN> c \<ELSE> d) Q = (%s. (b s --> wp c Q s) &  (~b s --> wp d Q s))"
    1.72 -by (rule ext) (auto simp: wp_def)
    1.73 -
    1.74 -lemma wp_While_If:
    1.75 - "wp (\<WHILE> b \<DO> c) Q s =
    1.76 -  wp (IF b THEN c;\<WHILE> b \<DO> c ELSE SKIP) Q s"
    1.77 -by(simp only: wp_def C_While_If)
    1.78 -
    1.79 -(*Not suitable for rewriting: LOOPS!*)
    1.80 -lemma wp_While_if:
    1.81 -  "wp (\<WHILE> b \<DO> c) Q s = (if b s then wp (c;\<WHILE> b \<DO> c) Q s else Q s)"
    1.82 -by(simp add:wp_While_If wp_If wp_SKIP)
    1.83 -
    1.84 -lemma wp_While_True: "b s ==>
    1.85 -  wp (\<WHILE> b \<DO> c) Q s = wp (c;\<WHILE> b \<DO> c) Q s"
    1.86 -by(simp add: wp_While_if)
    1.87 -
    1.88 -lemma wp_While_False: "~b s ==> wp (\<WHILE> b \<DO> c) Q s = Q s"
    1.89 -by(simp add: wp_While_if)
    1.90 -
    1.91 -lemmas [simp] = wp_SKIP wp_Ass wp_Semi wp_If wp_While_True wp_While_False
    1.92 -
    1.93 -lemma wp_While: "wp (\<WHILE> b \<DO> c) Q s =
    1.94 -   (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))"
    1.95 -apply (simp (no_asm))
    1.96 -apply (rule iffI)
    1.97 - apply (rule weak_coinduct)
    1.98 -  apply (erule CollectI)
    1.99 - apply safe
   1.100 -  apply simp
   1.101 - apply simp
   1.102 -apply (simp add: wp_def Gamma_def)
   1.103 -apply (intro strip)
   1.104 -apply (rule mp)
   1.105 - prefer 2 apply (assumption)
   1.106 -apply (erule lfp_induct2)
   1.107 -apply (fast intro!: monoI)
   1.108 -apply (subst gfp_unfold)
   1.109 - apply (fast intro!: monoI)
   1.110 -apply fast
   1.111 -done
   1.112 -
   1.113 -declare C_while [simp del]
   1.114 +lemmas [simp] = skip ass semi If
   1.115  
   1.116  lemmas [intro!] = hoare.skip hoare.ass hoare.semi hoare.If
   1.117  
   1.118 -lemma wp_is_pre: "|- {wp c Q} c {Q}"
   1.119 -proof(induct c arbitrary: Q)
   1.120 -  case SKIP show ?case by auto
   1.121 -next
   1.122 -  case Assign show ?case by auto
   1.123 -next
   1.124 -  case Semi thus ?case by auto
   1.125 -next
   1.126 -  case (Cond b c1 c2)
   1.127 -  let ?If = "IF b THEN c1 ELSE c2"
   1.128 -  show ?case
   1.129 -  proof(rule If)
   1.130 -    show "|- {\<lambda>s. wp ?If Q s \<and> b s} c1 {Q}"
   1.131 -    proof(rule strengthen_pre[OF _ Cond(1)])
   1.132 -      show "\<forall>s. wp ?If Q s \<and> b s \<longrightarrow> wp c1 Q s" by auto
   1.133 -    qed
   1.134 -    show "|- {\<lambda>s. wp ?If Q s \<and> \<not> b s} c2 {Q}"
   1.135 -    proof(rule strengthen_pre[OF _ Cond(2)])
   1.136 -      show "\<forall>s. wp ?If Q s \<and> \<not> b s \<longrightarrow> wp c2 Q s" by auto
   1.137 -    qed
   1.138 -  qed
   1.139 -next
   1.140 -  case (While b c)
   1.141 -  let ?w = "WHILE b DO c"
   1.142 -  have "|- {wp ?w Q} ?w {\<lambda>s. wp ?w Q s \<and> \<not> b s}"
   1.143 -  proof(rule hoare.While)
   1.144 -    show "|- {\<lambda>s. wp ?w Q s \<and> b s} c {wp ?w Q}"
   1.145 -    proof(rule strengthen_pre[OF _ While(1)])
   1.146 -      show "\<forall>s. wp ?w Q s \<and> b s \<longrightarrow> wp c (wp ?w Q) s" by auto
   1.147 -    qed
   1.148 -  qed
   1.149 -  thus ?case
   1.150 -  proof(rule weaken_post)
   1.151 -    show "\<forall>s. wp ?w Q s \<and> \<not> b s \<longrightarrow> Q s" by auto
   1.152 -  qed
   1.153 -qed
   1.154 -
   1.155 -lemma hoare_relative_complete: assumes "|= {P}c{Q}" shows "|- {P}c{Q}"
   1.156 -proof(rule conseq)
   1.157 -  show "\<forall>s. P s \<longrightarrow> wp c Q s" using assms
   1.158 -    by (auto simp: hoare_valid_def wp_def)
   1.159 -  show "|- {wp c Q} c {Q}" by(rule wp_is_pre)
   1.160 -  show "\<forall>s. Q s \<longrightarrow> Q s" by auto
   1.161 -qed
   1.162 -
   1.163  end
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/IMP/Hoare_Den.thy	Fri Mar 12 18:42:56 2010 +0100
     2.3 @@ -0,0 +1,134 @@
     2.4 +(*  Title:      HOL/IMP/Hoare_Def.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Tobias Nipkow
     2.7 +*)
     2.8 +
     2.9 +header "Soundness and Completeness wrt Denotational Semantics"
    2.10 +
    2.11 +theory Hoare_Den imports Hoare Denotation begin
    2.12 +
    2.13 +definition
    2.14 +  hoare_valid :: "[assn,com,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50) where
    2.15 +  "|= {P}c{Q} = (!s t. (s,t) : C(c) --> P s --> Q t)"
    2.16 +
    2.17 +
    2.18 +lemma hoare_sound: "|- {P}c{Q} ==> |= {P}c{Q}"
    2.19 +proof(induct rule: hoare.induct)
    2.20 +  case (While P b c)
    2.21 +  { fix s t
    2.22 +    let ?G = "Gamma b (C c)"
    2.23 +    assume "(s,t) \<in> lfp ?G"
    2.24 +    hence "P s \<longrightarrow> P t \<and> \<not> b t"
    2.25 +    proof(rule lfp_induct2)
    2.26 +      show "mono ?G" by(rule Gamma_mono)
    2.27 +    next
    2.28 +      fix s t assume "(s,t) \<in> ?G (lfp ?G \<inter> {(s,t). P s \<longrightarrow> P t \<and> \<not> b t})"
    2.29 +      thus "P s \<longrightarrow> P t \<and> \<not> b t" using While.hyps
    2.30 +        by(auto simp: hoare_valid_def Gamma_def)
    2.31 +    qed
    2.32 +  }
    2.33 +  thus ?case by(simp add:hoare_valid_def)
    2.34 +qed (auto simp: hoare_valid_def)
    2.35 +
    2.36 +
    2.37 +definition
    2.38 +  wp :: "com => assn => assn" where
    2.39 +  "wp c Q = (%s. !t. (s,t) : C(c) --> Q t)"
    2.40 +
    2.41 +lemma wp_SKIP: "wp \<SKIP> Q = Q"
    2.42 +by (simp add: wp_def)
    2.43 +
    2.44 +lemma wp_Ass: "wp (x:==a) Q = (%s. Q(s[x\<mapsto>a s]))"
    2.45 +by (simp add: wp_def)
    2.46 +
    2.47 +lemma wp_Semi: "wp (c;d) Q = wp c (wp d Q)"
    2.48 +by (rule ext) (auto simp: wp_def)
    2.49 +
    2.50 +lemma wp_If:
    2.51 + "wp (\<IF> b \<THEN> c \<ELSE> d) Q = (%s. (b s --> wp c Q s) &  (~b s --> wp d Q s))"
    2.52 +by (rule ext) (auto simp: wp_def)
    2.53 +
    2.54 +lemma wp_While_If:
    2.55 + "wp (\<WHILE> b \<DO> c) Q s =
    2.56 +  wp (IF b THEN c;\<WHILE> b \<DO> c ELSE SKIP) Q s"
    2.57 +by(simp only: wp_def C_While_If)
    2.58 +
    2.59 +(*Not suitable for rewriting: LOOPS!*)
    2.60 +lemma wp_While_if:
    2.61 +  "wp (\<WHILE> b \<DO> c) Q s = (if b s then wp (c;\<WHILE> b \<DO> c) Q s else Q s)"
    2.62 +by(simp add:wp_While_If wp_If wp_SKIP)
    2.63 +
    2.64 +lemma wp_While_True: "b s ==>
    2.65 +  wp (\<WHILE> b \<DO> c) Q s = wp (c;\<WHILE> b \<DO> c) Q s"
    2.66 +by(simp add: wp_While_if)
    2.67 +
    2.68 +lemma wp_While_False: "~b s ==> wp (\<WHILE> b \<DO> c) Q s = Q s"
    2.69 +by(simp add: wp_While_if)
    2.70 +
    2.71 +lemmas [simp] = wp_SKIP wp_Ass wp_Semi wp_If wp_While_True wp_While_False
    2.72 +
    2.73 +lemma wp_While: "wp (\<WHILE> b \<DO> c) Q s =
    2.74 +   (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))"
    2.75 +apply (simp (no_asm))
    2.76 +apply (rule iffI)
    2.77 + apply (rule weak_coinduct)
    2.78 +  apply (erule CollectI)
    2.79 + apply safe
    2.80 +  apply simp
    2.81 + apply simp
    2.82 +apply (simp add: wp_def Gamma_def)
    2.83 +apply (intro strip)
    2.84 +apply (rule mp)
    2.85 + prefer 2 apply (assumption)
    2.86 +apply (erule lfp_induct2)
    2.87 +apply (fast intro!: monoI)
    2.88 +apply (subst gfp_unfold)
    2.89 + apply (fast intro!: monoI)
    2.90 +apply fast
    2.91 +done
    2.92 +
    2.93 +declare C_while [simp del]
    2.94 +
    2.95 +lemma wp_is_pre: "|- {wp c Q} c {Q}"
    2.96 +proof(induct c arbitrary: Q)
    2.97 +  case SKIP show ?case by auto
    2.98 +next
    2.99 +  case Assign show ?case by auto
   2.100 +next
   2.101 +  case Semi thus ?case by auto
   2.102 +next
   2.103 +  case (Cond b c1 c2)
   2.104 +  let ?If = "IF b THEN c1 ELSE c2"
   2.105 +  show ?case
   2.106 +  proof(rule If)
   2.107 +    show "|- {\<lambda>s. wp ?If Q s \<and> b s} c1 {Q}"
   2.108 +    proof(rule strengthen_pre[OF _ Cond(1)])
   2.109 +      show "\<forall>s. wp ?If Q s \<and> b s \<longrightarrow> wp c1 Q s" by auto
   2.110 +    qed
   2.111 +    show "|- {\<lambda>s. wp ?If Q s \<and> \<not> b s} c2 {Q}"
   2.112 +    proof(rule strengthen_pre[OF _ Cond(2)])
   2.113 +      show "\<forall>s. wp ?If Q s \<and> \<not> b s \<longrightarrow> wp c2 Q s" by auto
   2.114 +    qed
   2.115 +  qed
   2.116 +next
   2.117 +  case (While b c)
   2.118 +  let ?w = "WHILE b DO c"
   2.119 +  show ?case
   2.120 +  proof(rule While')
   2.121 +    show "|- {\<lambda>s. wp ?w Q s \<and> b s} c {wp ?w Q}"
   2.122 +    proof(rule strengthen_pre[OF _ While(1)])
   2.123 +      show "\<forall>s. wp ?w Q s \<and> b s \<longrightarrow> wp c (wp ?w Q) s" by auto
   2.124 +    qed
   2.125 +    show "\<forall>s. wp ?w Q s \<and> \<not> b s \<longrightarrow> Q s" by auto
   2.126 +  qed
   2.127 +qed
   2.128 +
   2.129 +lemma hoare_relative_complete: assumes "|= {P}c{Q}" shows "|- {P}c{Q}"
   2.130 +proof(rule conseq)
   2.131 +  show "\<forall>s. P s \<longrightarrow> wp c Q s" using assms
   2.132 +    by (auto simp: hoare_valid_def wp_def)
   2.133 +  show "|- {wp c Q} c {Q}" by(rule wp_is_pre)
   2.134 +  show "\<forall>s. Q s \<longrightarrow> Q s" by auto
   2.135 +qed
   2.136 +
   2.137 +end
     3.1 --- a/src/HOL/IMP/Hoare_Op.thy	Fri Mar 12 15:48:37 2010 +0100
     3.2 +++ b/src/HOL/IMP/Hoare_Op.thy	Fri Mar 12 18:42:56 2010 +0100
     3.3 @@ -3,37 +3,14 @@
     3.4      Author:     Tobias Nipkow
     3.5  *)
     3.6  
     3.7 -header "Hoare Logic (justified wrt operational semantics)"
     3.8 +header "Soundness and Completeness wrt Operational Semantics"
     3.9  
    3.10 -theory Hoare_Op imports Natural begin
    3.11 -
    3.12 -types assn = "state => bool"
    3.13 +theory Hoare_Op imports Hoare begin
    3.14  
    3.15  definition
    3.16    hoare_valid :: "[assn,com,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50) where
    3.17    "|= {P}c{Q} = (!s t. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t --> P s --> Q t)"
    3.18  
    3.19 -inductive
    3.20 -  hoare :: "assn => com => assn => bool" ("|- ({(1_)}/ (_)/ {(1_)})" 50)
    3.21 -where
    3.22 -  skip: "|- {P}\<SKIP>{P}"
    3.23 -| ass:  "|- {%s. P(s[x\<mapsto>a s])} x:==a {P}"
    3.24 -| semi: "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}"
    3.25 -| If: "[| |- {%s. P s & b s}c{Q}; |- {%s. P s & ~b s}d{Q} |] ==>
    3.26 -      |- {P} \<IF> b \<THEN> c \<ELSE> d {Q}"
    3.27 -| While: "|- {%s. P s & b s} c {P} ==>
    3.28 -         |- {P} \<WHILE> b \<DO> c {%s. P s & ~b s}"
    3.29 -| conseq: "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==>
    3.30 -          |- {P'}c{Q'}"
    3.31 -
    3.32 -lemmas [simp] = skip ass semi If
    3.33 -
    3.34 -lemma strengthen_pre: "[| !s. P' s --> P s; |- {P}c{Q} |] ==> |- {P'}c{Q}"
    3.35 -by (blast intro: conseq)
    3.36 -
    3.37 -lemma weaken_post: "[| |- {P}c{Q}; !s. Q s --> Q' s |] ==> |- {P}c{Q'}"
    3.38 -by (blast intro: conseq)
    3.39 -
    3.40  lemma hoare_sound: "|- {P}c{Q} ==> |= {P}c{Q}"
    3.41  proof(induct rule: hoare.induct)
    3.42    case (While P b c)
    3.43 @@ -51,7 +28,6 @@
    3.44    thus ?case unfolding hoare_valid_def by blast
    3.45  qed (auto simp: hoare_valid_def)
    3.46  
    3.47 -
    3.48  definition
    3.49    wp :: "com => assn => assn" where
    3.50    "wp c Q = (%s. !t. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t --> Q t)"
     4.1 --- a/src/HOL/IMP/ROOT.ML	Fri Mar 12 15:48:37 2010 +0100
     4.2 +++ b/src/HOL/IMP/ROOT.ML	Fri Mar 12 18:42:56 2010 +0100
     4.3 @@ -6,4 +6,4 @@
     4.4  Caveat: HOLCF/IMP depends on HOL/IMP
     4.5  *)
     4.6  
     4.7 -use_thys ["Expr", "Transition", "Hoare_Op", "VC", "Examples", "Compiler0", "Compiler", "Live"];
     4.8 +use_thys ["Expr", "Transition", "VC", "Hoare_Den", "Examples", "Compiler0", "Compiler", "Live"];
     5.1 --- a/src/HOL/IMP/VC.thy	Fri Mar 12 15:48:37 2010 +0100
     5.2 +++ b/src/HOL/IMP/VC.thy	Fri Mar 12 18:42:56 2010 +0100
     5.3 @@ -10,7 +10,7 @@
     5.4  
     5.5  header "Verification Conditions"
     5.6  
     5.7 -theory VC imports Hoare begin
     5.8 +theory VC imports Hoare_Op begin
     5.9  
    5.10  datatype  acom = Askip
    5.11                 | Aass   loc aexp
    5.12 @@ -63,51 +63,36 @@
    5.13  Soundness and completeness of vc
    5.14  *)
    5.15  
    5.16 -declare hoare.intros [intro]
    5.17 +declare hoare.conseq [intro]
    5.18  
    5.19 -lemma l: "!s. P s --> P s" by fast
    5.20  
    5.21 -lemma vc_sound: "(!s. vc c Q s) --> |- {awp c Q} astrip c {Q}"
    5.22 -apply (induct c arbitrary: Q)
    5.23 -    apply (simp_all (no_asm))
    5.24 -    apply fast
    5.25 -   apply fast
    5.26 -  apply fast
    5.27 - (* if *)
    5.28 - apply atomize
    5.29 - apply (tactic "deepen_tac @{claset} 4 1")
    5.30 -(* while *)
    5.31 -apply atomize
    5.32 -apply (intro allI impI)
    5.33 -apply (rule conseq)
    5.34 -  apply (rule l)
    5.35 - apply (rule While)
    5.36 - defer
    5.37 - apply fast
    5.38 -apply (rule_tac P="awp c fun2" in conseq)
    5.39 -  apply fast
    5.40 - apply fast
    5.41 -apply fast
    5.42 -done
    5.43 +lemma vc_sound: "(ALL s. vc c Q s) \<Longrightarrow> |- {awp c Q} astrip c {Q}"
    5.44 +proof(induct c arbitrary: Q)
    5.45 +  case (Awhile b I c)
    5.46 +  show ?case
    5.47 +  proof(simp, rule While')
    5.48 +    from `\<forall>s. vc (Awhile b I c) Q s`
    5.49 +    have vc: "ALL s. vc c I s" and IQ: "ALL s. I s \<and> \<not> b s \<longrightarrow> Q s" and
    5.50 +         awp: "ALL s. I s & b s --> awp c I s" by simp_all
    5.51 +    from vc have "|- {awp c I} astrip c {I}" using Awhile.hyps by blast
    5.52 +    with awp show "|- {\<lambda>s. I s \<and> b s} astrip c {I}"
    5.53 +      by(rule strengthen_pre)
    5.54 +    show "\<forall>s. I s \<and> \<not> b s \<longrightarrow> Q s" by(rule IQ)
    5.55 +  qed
    5.56 +qed auto
    5.57  
    5.58 -lemma awp_mono [rule_format (no_asm)]:
    5.59 -  "!P Q. (!s. P s --> Q s) --> (!s. awp c P s --> awp c Q s)"
    5.60 -apply (induct c)
    5.61 -    apply (simp_all (no_asm_simp))
    5.62 -apply (rule allI, rule allI, rule impI)
    5.63 -apply (erule allE, erule allE, erule mp)
    5.64 -apply (erule allE, erule allE, erule mp, assumption)
    5.65 -done
    5.66  
    5.67 -lemma vc_mono [rule_format (no_asm)]:
    5.68 -  "!P Q. (!s. P s --> Q s) --> (!s. vc c P s --> vc c Q s)"
    5.69 -apply (induct c)
    5.70 -    apply (simp_all (no_asm_simp))
    5.71 -apply safe
    5.72 -apply (erule allE,erule allE,erule impE,erule_tac [2] allE,erule_tac [2] mp)
    5.73 -prefer 2 apply assumption
    5.74 -apply (fast elim: awp_mono)
    5.75 -done
    5.76 +lemma awp_mono:
    5.77 +  "(!s. P s --> Q s) ==> awp c P s ==> awp c Q s"
    5.78 +proof (induct c arbitrary: P Q s)
    5.79 +  case Asemi thus ?case by simp metis
    5.80 +qed simp_all
    5.81 +
    5.82 +lemma vc_mono:
    5.83 +  "(!s. P s --> Q s) ==> vc c P s ==> vc c Q s"
    5.84 +proof(induct c arbitrary: P Q)
    5.85 +  case Asemi thus ?case by simp (metis awp_mono)
    5.86 +qed simp_all
    5.87  
    5.88  lemma vc_complete: assumes der: "|- {P}c{Q}"
    5.89    shows "(\<exists>ac. astrip ac = c & (\<forall>s. vc ac Q s) & (\<forall>s. P s --> awp ac Q s))"