merged
authornipkow
Fri Mar 12 15:48:37 2010 +0100 (2010-03-12)
changeset 3575041267aebfa5f
parent 35748 5f35613d9a65
parent 35749 bc8637ae91ab
child 35753 b4d818b0d7c4
child 35754 8e7dba5f00f5
merged
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/IMP/Hoare_Op.thy	Fri Mar 12 15:48:37 2010 +0100
     1.3 @@ -0,0 +1,130 @@
     1.4 +(*  Title:      HOL/IMP/Hoare_Op.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Tobias Nipkow
     1.7 +*)
     1.8 +
     1.9 +header "Hoare Logic (justified wrt operational semantics)"
    1.10 +
    1.11 +theory Hoare_Op imports Natural begin
    1.12 +
    1.13 +types assn = "state => bool"
    1.14 +
    1.15 +definition
    1.16 +  hoare_valid :: "[assn,com,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50) where
    1.17 +  "|= {P}c{Q} = (!s t. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t --> P s --> Q t)"
    1.18 +
    1.19 +inductive
    1.20 +  hoare :: "assn => com => assn => bool" ("|- ({(1_)}/ (_)/ {(1_)})" 50)
    1.21 +where
    1.22 +  skip: "|- {P}\<SKIP>{P}"
    1.23 +| ass:  "|- {%s. P(s[x\<mapsto>a s])} x:==a {P}"
    1.24 +| semi: "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}"
    1.25 +| If: "[| |- {%s. P s & b s}c{Q}; |- {%s. P s & ~b s}d{Q} |] ==>
    1.26 +      |- {P} \<IF> b \<THEN> c \<ELSE> d {Q}"
    1.27 +| While: "|- {%s. P s & b s} c {P} ==>
    1.28 +         |- {P} \<WHILE> b \<DO> c {%s. P s & ~b s}"
    1.29 +| conseq: "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==>
    1.30 +          |- {P'}c{Q'}"
    1.31 +
    1.32 +lemmas [simp] = skip ass semi If
    1.33 +
    1.34 +lemma strengthen_pre: "[| !s. P' s --> P s; |- {P}c{Q} |] ==> |- {P'}c{Q}"
    1.35 +by (blast intro: conseq)
    1.36 +
    1.37 +lemma weaken_post: "[| |- {P}c{Q}; !s. Q s --> Q' s |] ==> |- {P}c{Q'}"
    1.38 +by (blast intro: conseq)
    1.39 +
    1.40 +lemma hoare_sound: "|- {P}c{Q} ==> |= {P}c{Q}"
    1.41 +proof(induct rule: hoare.induct)
    1.42 +  case (While P b c)
    1.43 +  { fix s t
    1.44 +    assume "\<langle>WHILE b DO c,s\<rangle> \<longrightarrow>\<^sub>c t"
    1.45 +    hence "P s \<longrightarrow> P t \<and> \<not> b t"
    1.46 +    proof(induct "WHILE b DO c" s t)
    1.47 +      case WhileFalse thus ?case by blast
    1.48 +    next
    1.49 +      case WhileTrue thus ?case
    1.50 +        using While(2) unfolding hoare_valid_def by blast
    1.51 +    qed
    1.52 +
    1.53 +  }
    1.54 +  thus ?case unfolding hoare_valid_def by blast
    1.55 +qed (auto simp: hoare_valid_def)
    1.56 +
    1.57 +
    1.58 +definition
    1.59 +  wp :: "com => assn => assn" where
    1.60 +  "wp c Q = (%s. !t. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t --> Q t)"
    1.61 +
    1.62 +lemma wp_SKIP: "wp \<SKIP> Q = Q"
    1.63 +by (simp add: wp_def)
    1.64 +
    1.65 +lemma wp_Ass: "wp (x:==a) Q = (%s. Q(s[x\<mapsto>a s]))"
    1.66 +by (simp add: wp_def)
    1.67 +
    1.68 +lemma wp_Semi: "wp (c;d) Q = wp c (wp d Q)"
    1.69 +by (rule ext) (auto simp: wp_def)
    1.70 +
    1.71 +lemma wp_If:
    1.72 + "wp (\<IF> b \<THEN> c \<ELSE> d) Q = (%s. (b s --> wp c Q s) &  (~b s --> wp d Q s))"
    1.73 +by (rule ext) (auto simp: wp_def)
    1.74 +
    1.75 +lemma wp_While_If:
    1.76 + "wp (\<WHILE> b \<DO> c) Q s =
    1.77 +  wp (IF b THEN c;\<WHILE> b \<DO> c ELSE SKIP) Q s"
    1.78 +unfolding wp_def by (metis equivD1 equivD2 unfold_while)
    1.79 +
    1.80 +lemma wp_While_True: "b s ==>
    1.81 +  wp (\<WHILE> b \<DO> c) Q s = wp (c;\<WHILE> b \<DO> c) Q s"
    1.82 +by(simp add: wp_While_If wp_If wp_SKIP)
    1.83 +
    1.84 +lemma wp_While_False: "~b s ==> wp (\<WHILE> b \<DO> c) Q s = Q s"
    1.85 +by(simp add: wp_While_If wp_If wp_SKIP)
    1.86 +
    1.87 +lemmas [simp] = wp_SKIP wp_Ass wp_Semi wp_If wp_While_True wp_While_False
    1.88 +
    1.89 +lemma wp_is_pre: "|- {wp c Q} c {Q}"
    1.90 +proof(induct c arbitrary: Q)
    1.91 +  case SKIP show ?case by auto
    1.92 +next
    1.93 +  case Assign show ?case by auto
    1.94 +next
    1.95 +  case Semi thus ?case by(auto intro: semi)
    1.96 +next
    1.97 +  case (Cond b c1 c2)
    1.98 +  let ?If = "IF b THEN c1 ELSE c2"
    1.99 +  show ?case
   1.100 +  proof(rule If)
   1.101 +    show "|- {\<lambda>s. wp ?If Q s \<and> b s} c1 {Q}"
   1.102 +    proof(rule strengthen_pre[OF _ Cond(1)])
   1.103 +      show "\<forall>s. wp ?If Q s \<and> b s \<longrightarrow> wp c1 Q s" by auto
   1.104 +    qed
   1.105 +    show "|- {\<lambda>s. wp ?If Q s \<and> \<not> b s} c2 {Q}"
   1.106 +    proof(rule strengthen_pre[OF _ Cond(2)])
   1.107 +      show "\<forall>s. wp ?If Q s \<and> \<not> b s \<longrightarrow> wp c2 Q s" by auto
   1.108 +    qed
   1.109 +  qed
   1.110 +next
   1.111 +  case (While b c)
   1.112 +  let ?w = "WHILE b DO c"
   1.113 +  have "|- {wp ?w Q} ?w {\<lambda>s. wp ?w Q s \<and> \<not> b s}"
   1.114 +  proof(rule hoare.While)
   1.115 +    show "|- {\<lambda>s. wp ?w Q s \<and> b s} c {wp ?w Q}"
   1.116 +    proof(rule strengthen_pre[OF _ While(1)])
   1.117 +      show "\<forall>s. wp ?w Q s \<and> b s \<longrightarrow> wp c (wp ?w Q) s" by auto
   1.118 +    qed
   1.119 +  qed
   1.120 +  thus ?case
   1.121 +  proof(rule weaken_post)
   1.122 +    show "\<forall>s. wp ?w Q s \<and> \<not> b s \<longrightarrow> Q s" by auto
   1.123 +  qed
   1.124 +qed
   1.125 +
   1.126 +lemma hoare_relative_complete: assumes "|= {P}c{Q}" shows "|- {P}c{Q}"
   1.127 +proof(rule strengthen_pre)
   1.128 +  show "\<forall>s. P s \<longrightarrow> wp c Q s" using assms
   1.129 +    by (auto simp: hoare_valid_def wp_def)
   1.130 +  show "|- {wp c Q} c {Q}" by(rule wp_is_pre)
   1.131 +qed
   1.132 +
   1.133 +end
     2.1 --- a/src/HOL/IMP/ROOT.ML	Fri Mar 12 15:35:41 2010 +0100
     2.2 +++ b/src/HOL/IMP/ROOT.ML	Fri Mar 12 15:48:37 2010 +0100
     2.3 @@ -6,4 +6,4 @@
     2.4  Caveat: HOLCF/IMP depends on HOL/IMP
     2.5  *)
     2.6  
     2.7 -use_thys ["Expr", "Transition", "VC", "Examples", "Compiler0", "Compiler", "Live"];
     2.8 +use_thys ["Expr", "Transition", "Hoare_Op", "VC", "Examples", "Compiler0", "Compiler", "Live"];