src/HOL/IMP/Hoare_Total_EX.thy
author paulson <lp15@cam.ac.uk>
Mon May 23 15:33:24 2016 +0100 (2016-05-23)
changeset 63114 27afe7af7379
parent 63070 952714a20087
child 63538 d7b5e2a222c2
permissions -rw-r--r--
Lots of new material for multivariate analysis
nipkow@63070
     1
(* Author: Tobias Nipkow *)
nipkow@63070
     2
nipkow@63070
     3
theory Hoare_Total_EX imports Hoare_Sound_Complete Hoare_Examples begin
nipkow@63070
     4
nipkow@63070
     5
subsection "Hoare Logic for Total Correctness"
nipkow@63070
     6
nipkow@63070
     7
text{* This is the standard set of rules that you find in many publications.
nipkow@63070
     8
The While-rule is different from the one in Concrete Semantics in that the
nipkow@63070
     9
invariant is indexed by natural numbers and goes down by 1 with
nipkow@63070
    10
every iteration. The completeness proof is easier but the rule is harder
nipkow@63070
    11
to apply in program proofs. *}
nipkow@63070
    12
nipkow@63070
    13
definition hoare_tvalid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool"
nipkow@63070
    14
  ("\<Turnstile>\<^sub>t {(1_)}/ (_)/ {(1_)}" 50) where
nipkow@63070
    15
"\<Turnstile>\<^sub>t {P}c{Q}  \<longleftrightarrow>  (\<forall>s. P s \<longrightarrow> (\<exists>t. (c,s) \<Rightarrow> t \<and> Q t))"
nipkow@63070
    16
nipkow@63070
    17
inductive
nipkow@63070
    18
  hoaret :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<turnstile>\<^sub>t ({(1_)}/ (_)/ {(1_)})" 50)
nipkow@63070
    19
where
nipkow@63070
    20
nipkow@63070
    21
Skip:  "\<turnstile>\<^sub>t {P} SKIP {P}"  |
nipkow@63070
    22
nipkow@63070
    23
Assign:  "\<turnstile>\<^sub>t {\<lambda>s. P(s[a/x])} x::=a {P}"  |
nipkow@63070
    24
nipkow@63070
    25
Seq: "\<lbrakk> \<turnstile>\<^sub>t {P\<^sub>1} c\<^sub>1 {P\<^sub>2}; \<turnstile>\<^sub>t {P\<^sub>2} c\<^sub>2 {P\<^sub>3} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P\<^sub>1} c\<^sub>1;;c\<^sub>2 {P\<^sub>3}"  |
nipkow@63070
    26
nipkow@63070
    27
If: "\<lbrakk> \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s} c\<^sub>1 {Q}; \<turnstile>\<^sub>t {\<lambda>s. P s \<and> \<not> bval b s} c\<^sub>2 {Q} \<rbrakk>
nipkow@63070
    28
  \<Longrightarrow> \<turnstile>\<^sub>t {P} IF b THEN c\<^sub>1 ELSE c\<^sub>2 {Q}"  |
nipkow@63070
    29
nipkow@63070
    30
While:
nipkow@63070
    31
  "\<lbrakk> \<And>n::nat. \<turnstile>\<^sub>t {P (Suc n)} c {P n};
nipkow@63070
    32
     \<forall>n s. P (Suc n) s \<longrightarrow> bval b s;  \<forall>s. P 0 s \<longrightarrow> \<not> bval b s \<rbrakk>
nipkow@63070
    33
   \<Longrightarrow> \<turnstile>\<^sub>t {\<lambda>s. \<exists>n. P n s} WHILE b DO c {P 0}"  |
nipkow@63070
    34
nipkow@63070
    35
conseq: "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile>\<^sub>t {P}c{Q}; \<forall>s. Q s \<longrightarrow> Q' s  \<rbrakk> \<Longrightarrow>
nipkow@63070
    36
           \<turnstile>\<^sub>t {P'}c{Q'}"
nipkow@63070
    37
nipkow@63070
    38
text{* Building in the consequence rule: *}
nipkow@63070
    39
nipkow@63070
    40
lemma strengthen_pre:
nipkow@63070
    41
  "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s;  \<turnstile>\<^sub>t {P} c {Q} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P'} c {Q}"
nipkow@63070
    42
by (metis conseq)
nipkow@63070
    43
nipkow@63070
    44
lemma weaken_post:
nipkow@63070
    45
  "\<lbrakk> \<turnstile>\<^sub>t {P} c {Q};  \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk> \<Longrightarrow>  \<turnstile>\<^sub>t {P} c {Q'}"
nipkow@63070
    46
by (metis conseq)
nipkow@63070
    47
nipkow@63070
    48
lemma Assign': "\<forall>s. P s \<longrightarrow> Q(s[a/x]) \<Longrightarrow> \<turnstile>\<^sub>t {P} x ::= a {Q}"
nipkow@63070
    49
by (simp add: strengthen_pre[OF _ Assign])
nipkow@63070
    50
nipkow@63070
    51
text{* The soundness theorem: *}
nipkow@63070
    52
nipkow@63070
    53
theorem hoaret_sound: "\<turnstile>\<^sub>t {P}c{Q}  \<Longrightarrow>  \<Turnstile>\<^sub>t {P}c{Q}"
nipkow@63070
    54
proof(unfold hoare_tvalid_def, induction rule: hoaret.induct)
nipkow@63070
    55
  case (While P c b)
nipkow@63070
    56
  {
nipkow@63070
    57
    fix n s
nipkow@63070
    58
    have "\<lbrakk> P n s \<rbrakk> \<Longrightarrow> \<exists>t. (WHILE b DO c, s) \<Rightarrow> t \<and> P 0 t"
nipkow@63070
    59
    proof(induction "n" arbitrary: s)
nipkow@63070
    60
      case 0 thus ?case using While.hyps(3) WhileFalse by blast
nipkow@63070
    61
    next
nipkow@63070
    62
      case (Suc n)
nipkow@63070
    63
      thus ?case by (meson While.IH While.hyps(2) WhileTrue)
nipkow@63070
    64
    qed
nipkow@63070
    65
  }
nipkow@63070
    66
  thus ?case by auto
nipkow@63070
    67
next
nipkow@63070
    68
  case If thus ?case by auto blast
nipkow@63070
    69
qed fastforce+
nipkow@63070
    70
nipkow@63070
    71
nipkow@63070
    72
definition wpt :: "com \<Rightarrow> assn \<Rightarrow> assn" ("wp\<^sub>t") where
nipkow@63070
    73
"wp\<^sub>t c Q  =  (\<lambda>s. \<exists>t. (c,s) \<Rightarrow> t \<and> Q t)"
nipkow@63070
    74
nipkow@63070
    75
lemma [simp]: "wp\<^sub>t SKIP Q = Q"
nipkow@63070
    76
by(auto intro!: ext simp: wpt_def)
nipkow@63070
    77
nipkow@63070
    78
lemma [simp]: "wp\<^sub>t (x ::= e) Q = (\<lambda>s. Q(s(x := aval e s)))"
nipkow@63070
    79
by(auto intro!: ext simp: wpt_def)
nipkow@63070
    80
nipkow@63070
    81
lemma [simp]: "wp\<^sub>t (c\<^sub>1;;c\<^sub>2) Q = wp\<^sub>t c\<^sub>1 (wp\<^sub>t c\<^sub>2 Q)"
nipkow@63070
    82
unfolding wpt_def
nipkow@63070
    83
apply(rule ext)
nipkow@63070
    84
apply auto
nipkow@63070
    85
done
nipkow@63070
    86
nipkow@63070
    87
lemma [simp]:
nipkow@63070
    88
 "wp\<^sub>t (IF b THEN c\<^sub>1 ELSE c\<^sub>2) Q = (\<lambda>s. wp\<^sub>t (if bval b s then c\<^sub>1 else c\<^sub>2) Q s)"
nipkow@63070
    89
apply(unfold wpt_def)
nipkow@63070
    90
apply(rule ext)
nipkow@63070
    91
apply auto
nipkow@63070
    92
done
nipkow@63070
    93
nipkow@63070
    94
nipkow@63070
    95
text{* Function @{text wpw} computes the weakest precondition of a While-loop
nipkow@63070
    96
that is unfolded a fixed number of times. *}
nipkow@63070
    97
nipkow@63070
    98
fun wpw :: "bexp \<Rightarrow> com \<Rightarrow> nat \<Rightarrow> assn \<Rightarrow> assn" where
nipkow@63070
    99
"wpw b c 0 Q s = (\<not> bval b s \<and> Q s)" |
nipkow@63070
   100
"wpw b c (Suc n) Q s = (bval b s \<and> (\<exists>s'. (c,s) \<Rightarrow> s' \<and>  wpw b c n Q s'))"
nipkow@63070
   101
nipkow@63070
   102
lemma WHILE_Its: "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> Q t \<Longrightarrow> \<exists>n. wpw b c n Q s"
nipkow@63070
   103
proof(induction "WHILE b DO c" s t rule: big_step_induct)
nipkow@63070
   104
  case WhileFalse thus ?case using wpw.simps(1) by blast 
nipkow@63070
   105
next
nipkow@63070
   106
  case WhileTrue thus ?case using wpw.simps(2) by blast
nipkow@63070
   107
qed
nipkow@63070
   108
nipkow@63070
   109
lemma wpt_is_pre: "\<turnstile>\<^sub>t {wp\<^sub>t c Q} c {Q}"
nipkow@63070
   110
proof (induction c arbitrary: Q)
nipkow@63070
   111
  case SKIP show ?case by (auto intro:hoaret.Skip)
nipkow@63070
   112
next
nipkow@63070
   113
  case Assign show ?case by (auto intro:hoaret.Assign)
nipkow@63070
   114
next
nipkow@63070
   115
  case Seq thus ?case by (auto intro:hoaret.Seq)
nipkow@63070
   116
next
nipkow@63070
   117
  case If thus ?case by (auto intro:hoaret.If hoaret.conseq)
nipkow@63070
   118
next
nipkow@63070
   119
  case (While b c)
nipkow@63070
   120
  let ?w = "WHILE b DO c"
nipkow@63070
   121
  have c1: "\<forall>s. wp\<^sub>t ?w Q s \<longrightarrow> (\<exists>n. wpw b c n Q s)"
nipkow@63070
   122
    unfolding wpt_def by (metis WHILE_Its)
nipkow@63070
   123
  have c3: "\<forall>s. wpw b c 0 Q s \<longrightarrow> Q s" by simp
nipkow@63070
   124
  have w2: "\<forall>n s. wpw b c (Suc n) Q s \<longrightarrow> bval b s" by simp
nipkow@63070
   125
  have w3: "\<forall>s. wpw b c 0 Q s \<longrightarrow> \<not> bval b s" by simp
nipkow@63070
   126
  { fix n
nipkow@63070
   127
    have 1: "\<forall>s. wpw b c (Suc n) Q s \<longrightarrow> (\<exists>t. (c, s) \<Rightarrow> t \<and> wpw b c n Q t)"
nipkow@63070
   128
      by simp
nipkow@63070
   129
    note strengthen_pre[OF 1 While.IH[of "wpw b c n Q", unfolded wpt_def]]
nipkow@63070
   130
  }
nipkow@63070
   131
  from conseq[OF c1 hoaret.While[OF this w2 w3] c3]
nipkow@63070
   132
  show ?case .
nipkow@63070
   133
qed
nipkow@63070
   134
nipkow@63070
   135
theorem hoaret_complete: "\<Turnstile>\<^sub>t {P}c{Q} \<Longrightarrow> \<turnstile>\<^sub>t {P}c{Q}"
nipkow@63070
   136
apply(rule strengthen_pre[OF _ wpt_is_pre])
nipkow@63070
   137
apply(auto simp: hoare_tvalid_def wpt_def)
nipkow@63070
   138
done
nipkow@63070
   139
nipkow@63070
   140
corollary hoaret_sound_complete: "\<turnstile>\<^sub>t {P}c{Q} \<longleftrightarrow> \<Turnstile>\<^sub>t {P}c{Q}"
nipkow@63070
   141
by (metis hoaret_sound hoaret_complete)
nipkow@63070
   142
nipkow@63070
   143
end