src/HOL/IMP/Hoare_Den.thy
changeset 35754 8e7dba5f00f5
child 41589 bbd861837ebc
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/IMP/Hoare_Den.thy	Fri Mar 12 18:42:56 2010 +0100
     1.3 @@ -0,0 +1,134 @@
     1.4 +(*  Title:      HOL/IMP/Hoare_Def.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Tobias Nipkow
     1.7 +*)
     1.8 +
     1.9 +header "Soundness and Completeness wrt Denotational Semantics"
    1.10 +
    1.11 +theory Hoare_Den imports Hoare Denotation begin
    1.12 +
    1.13 +definition
    1.14 +  hoare_valid :: "[assn,com,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50) where
    1.15 +  "|= {P}c{Q} = (!s t. (s,t) : C(c) --> P s --> Q t)"
    1.16 +
    1.17 +
    1.18 +lemma hoare_sound: "|- {P}c{Q} ==> |= {P}c{Q}"
    1.19 +proof(induct rule: hoare.induct)
    1.20 +  case (While P b c)
    1.21 +  { fix s t
    1.22 +    let ?G = "Gamma b (C c)"
    1.23 +    assume "(s,t) \<in> lfp ?G"
    1.24 +    hence "P s \<longrightarrow> P t \<and> \<not> b t"
    1.25 +    proof(rule lfp_induct2)
    1.26 +      show "mono ?G" by(rule Gamma_mono)
    1.27 +    next
    1.28 +      fix s t assume "(s,t) \<in> ?G (lfp ?G \<inter> {(s,t). P s \<longrightarrow> P t \<and> \<not> b t})"
    1.29 +      thus "P s \<longrightarrow> P t \<and> \<not> b t" using While.hyps
    1.30 +        by(auto simp: hoare_valid_def Gamma_def)
    1.31 +    qed
    1.32 +  }
    1.33 +  thus ?case by(simp add:hoare_valid_def)
    1.34 +qed (auto simp: hoare_valid_def)
    1.35 +
    1.36 +
    1.37 +definition
    1.38 +  wp :: "com => assn => assn" where
    1.39 +  "wp c Q = (%s. !t. (s,t) : C(c) --> Q t)"
    1.40 +
    1.41 +lemma wp_SKIP: "wp \<SKIP> Q = Q"
    1.42 +by (simp add: wp_def)
    1.43 +
    1.44 +lemma wp_Ass: "wp (x:==a) Q = (%s. Q(s[x\<mapsto>a s]))"
    1.45 +by (simp add: wp_def)
    1.46 +
    1.47 +lemma wp_Semi: "wp (c;d) Q = wp c (wp d Q)"
    1.48 +by (rule ext) (auto simp: wp_def)
    1.49 +
    1.50 +lemma wp_If:
    1.51 + "wp (\<IF> b \<THEN> c \<ELSE> d) Q = (%s. (b s --> wp c Q s) &  (~b s --> wp d Q s))"
    1.52 +by (rule ext) (auto simp: wp_def)
    1.53 +
    1.54 +lemma wp_While_If:
    1.55 + "wp (\<WHILE> b \<DO> c) Q s =
    1.56 +  wp (IF b THEN c;\<WHILE> b \<DO> c ELSE SKIP) Q s"
    1.57 +by(simp only: wp_def C_While_If)
    1.58 +
    1.59 +(*Not suitable for rewriting: LOOPS!*)
    1.60 +lemma wp_While_if:
    1.61 +  "wp (\<WHILE> b \<DO> c) Q s = (if b s then wp (c;\<WHILE> b \<DO> c) Q s else Q s)"
    1.62 +by(simp add:wp_While_If wp_If wp_SKIP)
    1.63 +
    1.64 +lemma wp_While_True: "b s ==>
    1.65 +  wp (\<WHILE> b \<DO> c) Q s = wp (c;\<WHILE> b \<DO> c) Q s"
    1.66 +by(simp add: wp_While_if)
    1.67 +
    1.68 +lemma wp_While_False: "~b s ==> wp (\<WHILE> b \<DO> c) Q s = Q s"
    1.69 +by(simp add: wp_While_if)
    1.70 +
    1.71 +lemmas [simp] = wp_SKIP wp_Ass wp_Semi wp_If wp_While_True wp_While_False
    1.72 +
    1.73 +lemma wp_While: "wp (\<WHILE> b \<DO> c) Q s =
    1.74 +   (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))"
    1.75 +apply (simp (no_asm))
    1.76 +apply (rule iffI)
    1.77 + apply (rule weak_coinduct)
    1.78 +  apply (erule CollectI)
    1.79 + apply safe
    1.80 +  apply simp
    1.81 + apply simp
    1.82 +apply (simp add: wp_def Gamma_def)
    1.83 +apply (intro strip)
    1.84 +apply (rule mp)
    1.85 + prefer 2 apply (assumption)
    1.86 +apply (erule lfp_induct2)
    1.87 +apply (fast intro!: monoI)
    1.88 +apply (subst gfp_unfold)
    1.89 + apply (fast intro!: monoI)
    1.90 +apply fast
    1.91 +done
    1.92 +
    1.93 +declare C_while [simp del]
    1.94 +
    1.95 +lemma wp_is_pre: "|- {wp c Q} c {Q}"
    1.96 +proof(induct c arbitrary: Q)
    1.97 +  case SKIP show ?case by auto
    1.98 +next
    1.99 +  case Assign show ?case by auto
   1.100 +next
   1.101 +  case Semi thus ?case by auto
   1.102 +next
   1.103 +  case (Cond b c1 c2)
   1.104 +  let ?If = "IF b THEN c1 ELSE c2"
   1.105 +  show ?case
   1.106 +  proof(rule If)
   1.107 +    show "|- {\<lambda>s. wp ?If Q s \<and> b s} c1 {Q}"
   1.108 +    proof(rule strengthen_pre[OF _ Cond(1)])
   1.109 +      show "\<forall>s. wp ?If Q s \<and> b s \<longrightarrow> wp c1 Q s" by auto
   1.110 +    qed
   1.111 +    show "|- {\<lambda>s. wp ?If Q s \<and> \<not> b s} c2 {Q}"
   1.112 +    proof(rule strengthen_pre[OF _ Cond(2)])
   1.113 +      show "\<forall>s. wp ?If Q s \<and> \<not> b s \<longrightarrow> wp c2 Q s" by auto
   1.114 +    qed
   1.115 +  qed
   1.116 +next
   1.117 +  case (While b c)
   1.118 +  let ?w = "WHILE b DO c"
   1.119 +  show ?case
   1.120 +  proof(rule While')
   1.121 +    show "|- {\<lambda>s. wp ?w Q s \<and> b s} c {wp ?w Q}"
   1.122 +    proof(rule strengthen_pre[OF _ While(1)])
   1.123 +      show "\<forall>s. wp ?w Q s \<and> b s \<longrightarrow> wp c (wp ?w Q) s" by auto
   1.124 +    qed
   1.125 +    show "\<forall>s. wp ?w Q s \<and> \<not> b s \<longrightarrow> Q s" by auto
   1.126 +  qed
   1.127 +qed
   1.128 +
   1.129 +lemma hoare_relative_complete: assumes "|= {P}c{Q}" shows "|- {P}c{Q}"
   1.130 +proof(rule conseq)
   1.131 +  show "\<forall>s. P s \<longrightarrow> wp c Q s" using assms
   1.132 +    by (auto simp: hoare_valid_def wp_def)
   1.133 +  show "|- {wp c Q} c {Q}" by(rule wp_is_pre)
   1.134 +  show "\<forall>s. Q s \<longrightarrow> Q s" by auto
   1.135 +qed
   1.136 +
   1.137 +end