src/HOL/IMP/HoareT.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 46304 ef5d8e94f66f
child 47818 151d137f1095
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     1
header{* Hoare Logic for Total Correctness *}
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     2
44177
b4b5cbca2519 IMP/Util distinguishes between sets and functions again; imported only where used.
kleing
parents: 43158
diff changeset
     3
theory HoareT imports Hoare_Sound_Complete begin
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     4
46203
nipkow
parents: 45114
diff changeset
     5
text{* Note that this definition of total validity @{text"\<Turnstile>\<^sub>t"} only
nipkow
parents: 45114
diff changeset
     6
works if execution is deterministic (which it is in our case). *}
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     7
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     8
definition hoare_tvalid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     9
  ("\<Turnstile>\<^sub>t {(1_)}/ (_)/ {(1_)}" 50) where
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    10
"\<Turnstile>\<^sub>t {P}c{Q}  \<equiv>  \<forall>s. P s \<longrightarrow> (\<exists>t. (c,s) \<Rightarrow> t \<and> Q t)"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    11
45114
fa3715b35370 fixed typos in IMP
Jean Pichon
parents: 45015
diff changeset
    12
text{* Provability of Hoare triples in the proof system for total
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    13
correctness is written @{text"\<turnstile>\<^sub>t {P}c{Q}"} and defined
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    14
inductively. The rules for @{text"\<turnstile>\<^sub>t"} differ from those for
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    15
@{text"\<turnstile>"} only in the one place where nontermination can arise: the
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    16
@{term While}-rule. *}
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    17
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    18
inductive
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    19
  hoaret :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<turnstile>\<^sub>t ({(1_)}/ (_)/ {(1_)})" 50)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    20
where
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    21
Skip:  "\<turnstile>\<^sub>t {P} SKIP {P}" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    22
Assign:  "\<turnstile>\<^sub>t {\<lambda>s. P(s[a/x])} x::=a {P}" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    23
Semi: "\<lbrakk> \<turnstile>\<^sub>t {P\<^isub>1} c\<^isub>1 {P\<^isub>2}; \<turnstile>\<^sub>t {P\<^isub>2} c\<^isub>2 {P\<^isub>3} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P\<^isub>1} c\<^isub>1;c\<^isub>2 {P\<^isub>3}" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    24
If: "\<lbrakk> \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s} c\<^isub>1 {Q}; \<turnstile>\<^sub>t {\<lambda>s. P s \<and> \<not> bval b s} c\<^isub>2 {Q} \<rbrakk>
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    25
  \<Longrightarrow> \<turnstile>\<^sub>t {P} IF b THEN c\<^isub>1 ELSE c\<^isub>2 {Q}" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    26
While:
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    27
  "\<lbrakk> \<And>n::nat. \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> f s = n} c {\<lambda>s. P s \<and> f s < n}\<rbrakk>
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    28
   \<Longrightarrow> \<turnstile>\<^sub>t {P} WHILE b DO c {\<lambda>s. P s \<and> \<not>bval b s}" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    29
conseq: "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile>\<^sub>t {P}c{Q}; \<forall>s. Q s \<longrightarrow> Q' s  \<rbrakk> \<Longrightarrow>
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    30
           \<turnstile>\<^sub>t {P'}c{Q'}"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    31
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    32
text{* The @{term While}-rule is like the one for partial correctness but it
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    33
requires additionally that with every execution of the loop body some measure
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    34
function @{term[source]"f :: state \<Rightarrow> nat"} decreases. *}
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    35
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    36
lemma strengthen_pre:
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    37
  "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s;  \<turnstile>\<^sub>t {P} c {Q} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P'} c {Q}"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    38
by (metis conseq)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    39
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    40
lemma weaken_post:
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    41
  "\<lbrakk> \<turnstile>\<^sub>t {P} c {Q};  \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk> \<Longrightarrow>  \<turnstile>\<^sub>t {P} c {Q'}"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    42
by (metis conseq)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    43
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    44
lemma Assign': "\<forall>s. P s \<longrightarrow> Q(s[a/x]) \<Longrightarrow> \<turnstile>\<^sub>t {P} x ::= a {Q}"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    45
by (simp add: strengthen_pre[OF _ Assign])
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    46
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    47
lemma While':
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    48
assumes "\<And>n::nat. \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> f s = n} c {\<lambda>s. P s \<and> f s < n}"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    49
    and "\<forall>s. P s \<and> \<not> bval b s \<longrightarrow> Q s"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    50
shows "\<turnstile>\<^sub>t {P} WHILE b DO c {Q}"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    51
by(blast intro: assms(1) weaken_post[OF While assms(2)])
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    52
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    53
text{* Our standard example: *}
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    54
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    55
abbreviation "w n ==
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    56
  WHILE Less (V ''y'') (N n)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    57
  DO ( ''y'' ::= Plus (V ''y'') (N 1); ''x'' ::= Plus (V ''x'') (V ''y'') )"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    58
46304
nipkow
parents: 46203
diff changeset
    59
lemma "\<turnstile>\<^sub>t {\<lambda>s. 0 \<le> n} ''x'' ::= N 0; ''y'' ::= N 0; w n {\<lambda>s. s ''x'' = \<Sum>{1..n}}"
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    60
apply(rule Semi)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    61
prefer 2
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    62
apply(rule While'
46203
nipkow
parents: 45114
diff changeset
    63
  [where P = "\<lambda>s. s ''x'' = \<Sum> {1..s ''y''} \<and> 0 \<le> s ''y'' \<and> s ''y'' \<le> n"
nipkow
parents: 45114
diff changeset
    64
   and f = "\<lambda>s. nat (n - s ''y'')"])
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    65
apply(rule Semi)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    66
prefer 2
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    67
apply(rule Assign)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    68
apply(rule Assign')
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    69
apply (simp add: atLeastAtMostPlus1_int_conv algebra_simps)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    70
apply clarsimp
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 44177
diff changeset
    71
apply fastforce
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    72
apply(rule Semi)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    73
prefer 2
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    74
apply(rule Assign)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    75
apply(rule Assign')
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    76
apply simp
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    77
done
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    78
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    79
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    80
text{* The soundness theorem: *}
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    81
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    82
theorem hoaret_sound: "\<turnstile>\<^sub>t {P}c{Q}  \<Longrightarrow>  \<Turnstile>\<^sub>t {P}c{Q}"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    83
proof(unfold hoare_tvalid_def, induct rule: hoaret.induct)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    84
  case (While P b f c)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    85
  show ?case
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    86
  proof
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    87
    fix s
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    88
    show "P s \<longrightarrow> (\<exists>t. (WHILE b DO c, s) \<Rightarrow> t \<and> P t \<and> \<not> bval b t)"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44890
diff changeset
    89
    proof(induction "f s" arbitrary: s rule: less_induct)
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    90
      case (less n)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    91
      thus ?case by (metis While(2) WhileFalse WhileTrue)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    92
    qed
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    93
  qed
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    94
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    95
  case If thus ?case by auto blast
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 44177
diff changeset
    96
qed fastforce+
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    97
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    98
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    99
text{*
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   100
The completeness proof proceeds along the same lines as the one for partial
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   101
correctness. First we have to strengthen our notion of weakest precondition
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   102
to take termination into account: *}
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   103
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   104
definition wpt :: "com \<Rightarrow> assn \<Rightarrow> assn" ("wp\<^sub>t") where
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   105
"wp\<^sub>t c Q  \<equiv>  \<lambda>s. \<exists>t. (c,s) \<Rightarrow> t \<and> Q t"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   106
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   107
lemma [simp]: "wp\<^sub>t SKIP Q = Q"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   108
by(auto intro!: ext simp: wpt_def)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   109
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   110
lemma [simp]: "wp\<^sub>t (x ::= e) Q = (\<lambda>s. Q(s(x := aval e s)))"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   111
by(auto intro!: ext simp: wpt_def)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   112
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   113
lemma [simp]: "wp\<^sub>t (c\<^isub>1;c\<^isub>2) Q = wp\<^sub>t c\<^isub>1 (wp\<^sub>t c\<^isub>2 Q)"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   114
unfolding wpt_def
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   115
apply(rule ext)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   116
apply auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   117
done
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   118
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   119
lemma [simp]:
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   120
 "wp\<^sub>t (IF b THEN c\<^isub>1 ELSE c\<^isub>2) Q = (\<lambda>s. wp\<^sub>t (if bval b s then c\<^isub>1 else c\<^isub>2) Q s)"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   121
apply(unfold wpt_def)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   122
apply(rule ext)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   123
apply auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   124
done
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   125
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   126
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   127
text{* Now we define the number of iterations @{term "WHILE b DO c"} needs to
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   128
terminate when started in state @{text s}. Because this is a truly partial
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   129
function, we define it as an (inductive) relation first: *}
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   130
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   131
inductive Its :: "bexp \<Rightarrow> com \<Rightarrow> state \<Rightarrow> nat \<Rightarrow> bool" where
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   132
Its_0: "\<not> bval b s \<Longrightarrow> Its b c s 0" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   133
Its_Suc: "\<lbrakk> bval b s;  (c,s) \<Rightarrow> s';  Its b c s' n \<rbrakk> \<Longrightarrow> Its b c s (Suc n)"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   134
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   135
text{* The relation is in fact a function: *}
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   136
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   137
lemma Its_fun: "Its b c s n \<Longrightarrow> Its b c s n' \<Longrightarrow> n=n'"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44890
diff changeset
   138
proof(induction arbitrary: n' rule:Its.induct)
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   139
(* new release:
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   140
  case Its_0 thus ?case by(metis Its.cases)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   141
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   142
  case Its_Suc thus ?case by(metis Its.cases big_step_determ)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   143
qed
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   144
*)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   145
  case Its_0
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   146
  from this(1) Its.cases[OF this(2)] show ?case by metis
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   147
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   148
  case (Its_Suc b s c s' n n')
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   149
  note C = this
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   150
  from this(5) show ?case
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   151
  proof cases
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   152
    case Its_0 with Its_Suc(1) show ?thesis by blast
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   153
  next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   154
    case Its_Suc with C show ?thesis by(metis big_step_determ)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   155
  qed
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   156
qed
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   157
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   158
text{* For all terminating loops, @{const Its} yields a result: *}
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   159
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   160
lemma WHILE_Its: "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> \<exists>n. Its b c s n"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44890
diff changeset
   161
proof(induction "WHILE b DO c" s t rule: big_step_induct)
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   162
  case WhileFalse thus ?case by (metis Its_0)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   163
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   164
  case WhileTrue thus ?case by (metis Its_Suc)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   165
qed
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   166
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   167
text{* Now the relation is turned into a function with the help of
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   168
the description operator @{text THE}: *}
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   169
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   170
definition its :: "bexp \<Rightarrow> com \<Rightarrow> state \<Rightarrow> nat" where
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   171
"its b c s = (THE n. Its b c s n)"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   172
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   173
text{* The key property: every loop iteration increases @{const its} by 1. *}
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   174
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   175
lemma its_Suc: "\<lbrakk> bval b s; (c, s) \<Rightarrow> s'; (WHILE b DO c, s') \<Rightarrow> t\<rbrakk>
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   176
       \<Longrightarrow> its b c s = Suc(its b c s')"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   177
by (metis its_def WHILE_Its Its.intros(2) Its_fun the_equality)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   178
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   179
lemma wpt_is_pre: "\<turnstile>\<^sub>t {wp\<^sub>t c Q} c {Q}"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44890
diff changeset
   180
proof (induction c arbitrary: Q)
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   181
  case SKIP show ?case by simp (blast intro:hoaret.Skip)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   182
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   183
  case Assign show ?case by simp (blast intro:hoaret.Assign)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   184
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   185
  case Semi thus ?case by simp (blast intro:hoaret.Semi)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   186
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   187
  case If thus ?case by simp (blast intro:hoaret.If hoaret.conseq)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   188
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   189
  case (While b c)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   190
  let ?w = "WHILE b DO c"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   191
  { fix n
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   192
    have "\<forall>s. wp\<^sub>t ?w Q s \<and> bval b s \<and> its b c s = n \<longrightarrow>
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   193
              wp\<^sub>t c (\<lambda>s'. wp\<^sub>t ?w Q s' \<and> its b c s' < n) s"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   194
      unfolding wpt_def by (metis WhileE its_Suc lessI)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   195
    note strengthen_pre[OF this While]
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   196
  } note hoaret.While[OF this]
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   197
  moreover have "\<forall>s. wp\<^sub>t ?w Q s \<and> \<not> bval b s \<longrightarrow> Q s" by (auto simp add:wpt_def)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   198
  ultimately show ?case by(rule weaken_post)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   199
qed
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   200
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   201
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   202
text{*\noindent In the @{term While}-case, @{const its} provides the obvious
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   203
termination argument.
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   204
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   205
The actual completeness theorem follows directly, in the same manner
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   206
as for partial correctness: *}
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   207
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   208
theorem hoaret_complete: "\<Turnstile>\<^sub>t {P}c{Q} \<Longrightarrow> \<turnstile>\<^sub>t {P}c{Q}"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   209
apply(rule strengthen_pre[OF _ wpt_is_pre])
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   210
apply(auto simp: hoare_tvalid_def hoare_valid_def wpt_def)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   211
done
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   212
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   213
end