src/HOL/IMP/Hoare_Sound_Complete.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 45015 fdac1e9880eb
child 47818 151d137f1095
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
     1 (* Author: Tobias Nipkow *)
     2 
     3 theory Hoare_Sound_Complete imports Hoare begin
     4 
     5 subsection "Soundness"
     6 
     7 definition
     8 hoare_valid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<Turnstile> {(1_)}/ (_)/ {(1_)}" 50) where
     9 "\<Turnstile> {P}c{Q} = (\<forall>s t. (c,s) \<Rightarrow> t  \<longrightarrow>  P s \<longrightarrow>  Q t)"
    10 
    11 lemma hoare_sound: "\<turnstile> {P}c{Q}  \<Longrightarrow>  \<Turnstile> {P}c{Q}"
    12 proof(induction rule: hoare.induct)
    13   case (While P b c)
    14   { fix s t
    15     have "(WHILE b DO c,s) \<Rightarrow> t  \<Longrightarrow>  P s \<longrightarrow> P t \<and> \<not> bval b t"
    16     proof(induction "WHILE b DO c" s t rule: big_step_induct)
    17       case WhileFalse thus ?case by blast
    18     next
    19       case WhileTrue thus ?case
    20         using While(2) unfolding hoare_valid_def by blast
    21     qed
    22   }
    23   thus ?case unfolding hoare_valid_def by blast
    24 qed (auto simp: hoare_valid_def)
    25 
    26 
    27 subsection "Weakest Precondition"
    28 
    29 definition wp :: "com \<Rightarrow> assn \<Rightarrow> assn" where
    30 "wp c Q = (\<lambda>s. \<forall>t. (c,s) \<Rightarrow> t  \<longrightarrow>  Q t)"
    31 
    32 lemma wp_SKIP[simp]: "wp SKIP Q = Q"
    33 by (rule ext) (auto simp: wp_def)
    34 
    35 lemma wp_Ass[simp]: "wp (x::=a) Q = (\<lambda>s. Q(s[a/x]))"
    36 by (rule ext) (auto simp: wp_def)
    37 
    38 lemma wp_Semi[simp]: "wp (c\<^isub>1;c\<^isub>2) Q = wp c\<^isub>1 (wp c\<^isub>2 Q)"
    39 by (rule ext) (auto simp: wp_def)
    40 
    41 lemma wp_If[simp]:
    42  "wp (IF b THEN c\<^isub>1 ELSE c\<^isub>2) Q =
    43  (\<lambda>s. (bval b s \<longrightarrow> wp c\<^isub>1 Q s) \<and>  (\<not> bval b s \<longrightarrow> wp c\<^isub>2 Q s))"
    44 by (rule ext) (auto simp: wp_def)
    45 
    46 lemma wp_While_If:
    47  "wp (WHILE b DO c) Q s =
    48   wp (IF b THEN c;WHILE b DO c ELSE SKIP) Q s"
    49 unfolding wp_def by (metis unfold_while)
    50 
    51 lemma wp_While_True[simp]: "bval b s \<Longrightarrow>
    52   wp (WHILE b DO c) Q s = wp (c; WHILE b DO c) Q s"
    53 by(simp add: wp_While_If)
    54 
    55 lemma wp_While_False[simp]: "\<not> bval b s \<Longrightarrow> wp (WHILE b DO c) Q s = Q s"
    56 by(simp add: wp_While_If)
    57 
    58 
    59 subsection "Completeness"
    60 
    61 lemma wp_is_pre: "\<turnstile> {wp c Q} c {Q}"
    62 proof(induction c arbitrary: Q)
    63   case Semi thus ?case by(auto intro: Semi)
    64 next
    65   case (If b c1 c2)
    66   let ?If = "IF b THEN c1 ELSE c2"
    67   show ?case
    68   proof(rule hoare.If)
    69     show "\<turnstile> {\<lambda>s. wp ?If Q s \<and> bval b s} c1 {Q}"
    70     proof(rule strengthen_pre[OF _ If(1)])
    71       show "\<forall>s. wp ?If Q s \<and> bval b s \<longrightarrow> wp c1 Q s" by auto
    72     qed
    73     show "\<turnstile> {\<lambda>s. wp ?If Q s \<and> \<not> bval b s} c2 {Q}"
    74     proof(rule strengthen_pre[OF _ If(2)])
    75       show "\<forall>s. wp ?If Q s \<and> \<not> bval b s \<longrightarrow> wp c2 Q s" by auto
    76     qed
    77   qed
    78 next
    79   case (While b c)
    80   let ?w = "WHILE b DO c"
    81   have "\<turnstile> {wp ?w Q} ?w {\<lambda>s. wp ?w Q s \<and> \<not> bval b s}"
    82   proof(rule hoare.While)
    83     show "\<turnstile> {\<lambda>s. wp ?w Q s \<and> bval b s} c {wp ?w Q}"
    84     proof(rule strengthen_pre[OF _ While(1)])
    85       show "\<forall>s. wp ?w Q s \<and> bval b s \<longrightarrow> wp c (wp ?w Q) s" by auto
    86     qed
    87   qed
    88   thus ?case
    89   proof(rule weaken_post)
    90     show "\<forall>s. wp ?w Q s \<and> \<not> bval b s \<longrightarrow> Q s" by auto
    91   qed
    92 qed auto
    93 
    94 lemma hoare_relative_complete: assumes "\<Turnstile> {P}c{Q}" shows "\<turnstile> {P}c{Q}"
    95 proof(rule strengthen_pre)
    96   show "\<forall>s. P s \<longrightarrow> wp c Q s" using assms
    97     by (auto simp: hoare_valid_def wp_def)
    98   show "\<turnstile> {wp c Q} c {Q}" by(rule wp_is_pre)
    99 qed
   100 
   101 end