author nipkow Fri Mar 12 18:42:56 2010 +0100 (2010-03-12) changeset 35754 8e7dba5f00f5 parent 35750 41267aebfa5f child 35755 bdfca0d37fee
Reorganized Hoare logic theories; added Hoare_Den
 src/HOL/IMP/Hoare.thy file | annotate | diff | revisions src/HOL/IMP/Hoare_Den.thy file | annotate | diff | revisions src/HOL/IMP/Hoare_Op.thy file | annotate | diff | revisions src/HOL/IMP/ROOT.ML file | annotate | diff | revisions src/HOL/IMP/VC.thy file | annotate | diff | revisions
```     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.63 -
1.64 -lemma wp_Ass: "wp (x:==a) Q = (%s. Q(s[x\<mapsto>a s]))"
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.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.87 -
1.88 -lemma wp_While_False: "~b s ==> wp (\<WHILE> b \<DO> c) Q s = Q s"
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.43 +
2.44 +lemma wp_Ass: "wp (x:==a) Q = (%s. Q(s[x\<mapsto>a s]))"
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.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.67 +
2.68 +lemma wp_While_False: "~b s ==> wp (\<WHILE> b \<DO> c) Q s = Q s"
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.6
5.7 -theory VC imports Hoare begin
5.8 +theory VC imports Hoare_Op begin
5.9
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))"
```