author | nipkow |
Mon, 11 Oct 2021 21:55:21 +0200 | |
changeset 74500 | 40f03761f77f |
parent 69505 | cc2d676d5395 |
permissions | -rw-r--r-- |
67019
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
1 |
(* Author: Tobias Nipkow *) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
2 |
|
68776
403dd13cf6e9
avoid session qualification because no tex is generated when used;
nipkow
parents:
67406
diff
changeset
|
3 |
subsubsection "Hoare Logic for Total Correctness With Logical Variables" |
403dd13cf6e9
avoid session qualification because no tex is generated when used;
nipkow
parents:
67406
diff
changeset
|
4 |
|
67019
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
5 |
theory Hoare_Total_EX2 |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
6 |
imports Hoare |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
7 |
begin |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
8 |
|
67406 | 9 |
text\<open>This is the standard set of rules that you find in many publications. |
67019
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
10 |
In the while-rule, a logical variable is needed to remember the pre-value |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
11 |
of the variant (an expression that decreases by one with each iteration). |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
12 |
In this theory, logical variables are modeled explicitly. |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
13 |
A simpler (but not quite as flexible) approach is found in theory \<open>Hoare_Total_EX\<close>: |
67406 | 14 |
pre and post-condition are connected via a universally quantified HOL variable.\<close> |
67019
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
15 |
|
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
16 |
type_synonym lvname = string |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
17 |
type_synonym assn2 = "(lvname \<Rightarrow> nat) \<Rightarrow> state \<Rightarrow> bool" |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
18 |
|
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
19 |
definition hoare_tvalid :: "assn2 \<Rightarrow> com \<Rightarrow> assn2 \<Rightarrow> bool" |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
20 |
("\<Turnstile>\<^sub>t {(1_)}/ (_)/ {(1_)}" 50) where |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
21 |
"\<Turnstile>\<^sub>t {P}c{Q} \<longleftrightarrow> (\<forall>l s. P l s \<longrightarrow> (\<exists>t. (c,s) \<Rightarrow> t \<and> Q l t))" |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
22 |
|
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
23 |
inductive |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
24 |
hoaret :: "assn2 \<Rightarrow> com \<Rightarrow> assn2 \<Rightarrow> bool" ("\<turnstile>\<^sub>t ({(1_)}/ (_)/ {(1_)})" 50) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
25 |
where |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
26 |
|
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
27 |
Skip: "\<turnstile>\<^sub>t {P} SKIP {P}" | |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
28 |
|
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
29 |
Assign: "\<turnstile>\<^sub>t {\<lambda>l s. P l (s[a/x])} x::=a {P}" | |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
30 |
|
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
31 |
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}" | |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
32 |
|
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
33 |
If: "\<lbrakk> \<turnstile>\<^sub>t {\<lambda>l s. P l s \<and> bval b s} c\<^sub>1 {Q}; \<turnstile>\<^sub>t {\<lambda>l s. P l s \<and> \<not> bval b s} c\<^sub>2 {Q} \<rbrakk> |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
34 |
\<Longrightarrow> \<turnstile>\<^sub>t {P} IF b THEN c\<^sub>1 ELSE c\<^sub>2 {Q}" | |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
35 |
|
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
36 |
While: |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
37 |
"\<lbrakk> \<turnstile>\<^sub>t {\<lambda>l. P (l(x := Suc(l(x))))} c {P}; |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
38 |
\<forall>l s. l x > 0 \<and> P l s \<longrightarrow> bval b s; |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
39 |
\<forall>l s. l x = 0 \<and> P l s \<longrightarrow> \<not> bval b s \<rbrakk> |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
40 |
\<Longrightarrow> \<turnstile>\<^sub>t {\<lambda>l s. \<exists>n. P (l(x:=n)) s} WHILE b DO c {\<lambda>l s. P (l(x := 0)) s}" | |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
41 |
|
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
42 |
conseq: "\<lbrakk> \<forall>l s. P' l s \<longrightarrow> P l s; \<turnstile>\<^sub>t {P}c{Q}; \<forall>l s. Q l s \<longrightarrow> Q' l s \<rbrakk> \<Longrightarrow> |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
43 |
\<turnstile>\<^sub>t {P'}c{Q'}" |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
44 |
|
67406 | 45 |
text\<open>Building in the consequence rule:\<close> |
67019
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
46 |
|
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
47 |
lemma strengthen_pre: |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
48 |
"\<lbrakk> \<forall>l s. P' l s \<longrightarrow> P l s; \<turnstile>\<^sub>t {P} c {Q} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P'} c {Q}" |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
49 |
by (metis conseq) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
50 |
|
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
51 |
lemma weaken_post: |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
52 |
"\<lbrakk> \<turnstile>\<^sub>t {P} c {Q}; \<forall>l s. Q l s \<longrightarrow> Q' l s \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P} c {Q'}" |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
53 |
by (metis conseq) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
54 |
|
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
55 |
lemma Assign': "\<forall>l s. P l s \<longrightarrow> Q l (s[a/x]) \<Longrightarrow> \<turnstile>\<^sub>t {P} x ::= a {Q}" |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
56 |
by (simp add: strengthen_pre[OF _ Assign]) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
57 |
|
67406 | 58 |
text\<open>The soundness theorem:\<close> |
67019
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
59 |
|
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
60 |
theorem hoaret_sound: "\<turnstile>\<^sub>t {P}c{Q} \<Longrightarrow> \<Turnstile>\<^sub>t {P}c{Q}" |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
61 |
proof(unfold hoare_tvalid_def, induction rule: hoaret.induct) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
62 |
case (While P x c b) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
63 |
have "\<lbrakk> l x = n; P l s \<rbrakk> \<Longrightarrow> \<exists>t. (WHILE b DO c, s) \<Rightarrow> t \<and> P (l(x := 0)) t" for n l s |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
64 |
proof(induction "n" arbitrary: l s) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
65 |
case 0 thus ?case using While.hyps(3) WhileFalse |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
66 |
by (metis fun_upd_triv) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
67 |
next |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
68 |
case Suc |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
69 |
thus ?case using While.IH While.hyps(2) WhileTrue |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
70 |
by (metis fun_upd_same fun_upd_triv fun_upd_upd zero_less_Suc) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
71 |
qed |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
72 |
thus ?case by fastforce |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
73 |
next |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
74 |
case If thus ?case by auto blast |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
75 |
qed fastforce+ |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
76 |
|
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
77 |
|
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
78 |
definition wpt :: "com \<Rightarrow> assn2 \<Rightarrow> assn2" ("wp\<^sub>t") where |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
79 |
"wp\<^sub>t c Q = (\<lambda>l s. \<exists>t. (c,s) \<Rightarrow> t \<and> Q l t)" |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
80 |
|
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
81 |
lemma [simp]: "wp\<^sub>t SKIP Q = Q" |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
82 |
by(auto intro!: ext simp: wpt_def) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
83 |
|
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
84 |
lemma [simp]: "wp\<^sub>t (x ::= e) Q = (\<lambda>l s. Q l (s(x := aval e s)))" |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
85 |
by(auto intro!: ext simp: wpt_def) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
86 |
|
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
87 |
lemma wpt_Seq[simp]: "wp\<^sub>t (c\<^sub>1;;c\<^sub>2) Q = wp\<^sub>t c\<^sub>1 (wp\<^sub>t c\<^sub>2 Q)" |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
88 |
by (auto simp: wpt_def fun_eq_iff) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
89 |
|
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
90 |
lemma [simp]: |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
91 |
"wp\<^sub>t (IF b THEN c\<^sub>1 ELSE c\<^sub>2) Q = (\<lambda>l s. wp\<^sub>t (if bval b s then c\<^sub>1 else c\<^sub>2) Q l s)" |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
92 |
by (auto simp: wpt_def fun_eq_iff) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
93 |
|
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
94 |
|
69505 | 95 |
text\<open>Function \<open>wpw\<close> computes the weakest precondition of a While-loop |
67406 | 96 |
that is unfolded a fixed number of times.\<close> |
67019
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
97 |
|
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
98 |
fun wpw :: "bexp \<Rightarrow> com \<Rightarrow> nat \<Rightarrow> assn2 \<Rightarrow> assn2" where |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
99 |
"wpw b c 0 Q l s = (\<not> bval b s \<and> Q l s)" | |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
100 |
"wpw b c (Suc n) Q l s = (bval b s \<and> (\<exists>s'. (c,s) \<Rightarrow> s' \<and> wpw b c n Q l s'))" |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
101 |
|
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
102 |
lemma WHILE_Its: |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
103 |
"(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> Q l t \<Longrightarrow> \<exists>n. wpw b c n Q l s" |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
104 |
proof(induction "WHILE b DO c" s t arbitrary: l rule: big_step_induct) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
105 |
case WhileFalse thus ?case using wpw.simps(1) by blast |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
106 |
next |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
107 |
case WhileTrue show ?case |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
108 |
using wpw.simps(2) WhileTrue(1,2) WhileTrue(5)[OF WhileTrue(6)] by blast |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
109 |
qed |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
110 |
|
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
111 |
definition support :: "assn2 \<Rightarrow> string set" where |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
112 |
"support P = {x. \<exists>l1 l2 s. (\<forall>y. y \<noteq> x \<longrightarrow> l1 y = l2 y) \<and> P l1 s \<noteq> P l2 s}" |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
113 |
|
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
114 |
lemma support_wpt: "support (wp\<^sub>t c Q) \<subseteq> support Q" |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
115 |
by(simp add: support_def wpt_def) blast |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
116 |
|
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
117 |
|
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
118 |
lemma support_wpw0: "support (wpw b c n Q) \<subseteq> support Q" |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
119 |
proof(induction n) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
120 |
case 0 show ?case by (simp add: support_def) blast |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
121 |
next |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
122 |
case Suc |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
123 |
have 1: "support (\<lambda>l s. A s \<and> B l s) \<subseteq> support B" for A B |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
124 |
by(auto simp: support_def) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
125 |
have 2: "support (\<lambda>l s. \<exists>s'. A s s' \<and> B l s') \<subseteq> support B" for A B |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
126 |
by(auto simp: support_def) blast+ |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
127 |
from Suc 1 2 show ?case by simp (meson order_trans) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
128 |
qed |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
129 |
|
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
130 |
lemma support_wpw_Un: |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
131 |
"support (%l. wpw b c (l x) Q l) \<subseteq> insert x (UN n. support(wpw b c n Q))" |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
132 |
using support_wpw0[of b c _ Q] |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
133 |
apply(auto simp add: support_def subset_iff) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
134 |
apply metis |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
135 |
apply metis |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
136 |
done |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
137 |
|
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
138 |
lemma support_wpw: "support (%l. wpw b c (l x) Q l) \<subseteq> insert x (support Q)" |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
139 |
using support_wpw0[of b c _ Q] support_wpw_Un[of b c _ Q] |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
140 |
by blast |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
141 |
|
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
142 |
lemma assn2_lupd: "x \<notin> support Q \<Longrightarrow> Q (l(x:=n)) = Q l" |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
143 |
by(simp add: support_def fun_upd_other fun_eq_iff) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
144 |
(metis (no_types, lifting) fun_upd_def) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
145 |
|
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
146 |
abbreviation "new Q \<equiv> SOME x. x \<notin> support Q" |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
147 |
|
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
148 |
lemma wpw_lupd: "x \<notin> support Q \<Longrightarrow> wpw b c n Q (l(x := u)) = wpw b c n Q l" |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
149 |
by(induction n) (auto simp: assn2_lupd fun_eq_iff) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
150 |
|
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
151 |
lemma wpt_is_pre: "finite(support Q) \<Longrightarrow> \<turnstile>\<^sub>t {wp\<^sub>t c Q} c {Q}" |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
152 |
proof (induction c arbitrary: Q) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
153 |
case SKIP show ?case by (auto intro:hoaret.Skip) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
154 |
next |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
155 |
case Assign show ?case by (auto intro:hoaret.Assign) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
156 |
next |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
157 |
case (Seq c1 c2) show ?case |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
158 |
by (auto intro:hoaret.Seq Seq finite_subset[OF support_wpt]) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
159 |
next |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
160 |
case If thus ?case by (auto intro:hoaret.If hoaret.conseq) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
161 |
next |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
162 |
case (While b c) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
163 |
let ?x = "new Q" |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
164 |
have "\<exists>x. x \<notin> support Q" using While.prems infinite_UNIV_listI |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
165 |
using ex_new_if_finite by blast |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
166 |
hence [simp]: "?x \<notin> support Q" by (rule someI_ex) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
167 |
let ?w = "WHILE b DO c" |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
168 |
have fsup: "finite (support (\<lambda>l. wpw b c (l x) Q l))" for x |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
169 |
using finite_subset[OF support_wpw] While.prems by simp |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
170 |
have c1: "\<forall>l s. wp\<^sub>t ?w Q l s \<longrightarrow> (\<exists>n. wpw b c n Q l s)" |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
171 |
unfolding wpt_def by (metis WHILE_Its) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
172 |
have c2: "\<forall>l s. l ?x = 0 \<and> wpw b c (l ?x) Q l s \<longrightarrow> \<not> bval b s" |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
173 |
by (simp cong: conj_cong) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
174 |
have w2: "\<forall>l s. 0 < l ?x \<and> wpw b c (l ?x) Q l s \<longrightarrow> bval b s" |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
175 |
by (auto simp: gr0_conv_Suc cong: conj_cong) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
176 |
have 1: "\<forall>l s. wpw b c (Suc(l ?x)) Q l s \<longrightarrow> |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
177 |
(\<exists>t. (c, s) \<Rightarrow> t \<and> wpw b c (l ?x) Q l t)" |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
178 |
by simp |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
179 |
have *: "\<turnstile>\<^sub>t {\<lambda>l. wpw b c (Suc (l ?x)) Q l} c {\<lambda>l. wpw b c (l ?x) Q l}" |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
180 |
by(rule strengthen_pre[OF 1 |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
181 |
While.IH[of "\<lambda>l. wpw b c (l ?x) Q l", unfolded wpt_def, OF fsup]]) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
182 |
show ?case |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
183 |
apply(rule conseq[OF _ hoaret.While[OF _ w2 c2]]) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
184 |
apply (simp_all add: c1 * assn2_lupd wpw_lupd del: wpw.simps(2)) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
185 |
done |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
186 |
qed |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
187 |
|
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
188 |
theorem hoaret_complete: "finite(support Q) \<Longrightarrow> \<Turnstile>\<^sub>t {P}c{Q} \<Longrightarrow> \<turnstile>\<^sub>t {P}c{Q}" |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
189 |
apply(rule strengthen_pre[OF _ wpt_is_pre]) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
190 |
apply(auto simp: hoare_tvalid_def wpt_def) |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
191 |
done |
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
192 |
|
74500 | 193 |
|
194 |
text \<open>Two examples:\<close> |
|
195 |
||
196 |
lemma "\<turnstile>\<^sub>t |
|
197 |
{\<lambda>l s. l ''x'' = nat(s ''x'')} |
|
198 |
WHILE Less (N 0) (V ''x'') DO ''x'' ::= Plus (V ''x'') (N (-1)) |
|
199 |
{\<lambda>l s. s ''x'' \<le> 0}" |
|
200 |
apply(rule conseq) |
|
201 |
prefer 2 |
|
202 |
apply(rule While[where P = "\<lambda>l s. l ''x'' = nat(s ''x'')" and x = "''x''"]) |
|
203 |
apply(rule Assign') |
|
204 |
apply auto |
|
205 |
done |
|
206 |
||
207 |
lemma "\<turnstile>\<^sub>t |
|
208 |
{\<lambda>l s. l ''x'' = nat(s ''x'')} |
|
209 |
WHILE Less (N 0) (V ''x'') |
|
210 |
DO (''x'' ::= Plus (V ''x'') (N (-1));; |
|
211 |
(''y'' ::= V ''x'';; |
|
212 |
WHILE Less (N 0) (V ''y'') DO ''y'' ::= Plus (V ''y'') (N (-1)))) |
|
213 |
{\<lambda>l s. s ''x'' \<le> 0}" |
|
214 |
apply(rule conseq) |
|
215 |
prefer 2 |
|
216 |
apply(rule While[where P = "\<lambda>l s. l ''x'' = nat(s ''x'')" and x = "''x''"]) |
|
217 |
defer |
|
218 |
apply auto |
|
219 |
apply(rule Seq) |
|
220 |
prefer 2 |
|
221 |
apply(rule Seq) |
|
222 |
prefer 2 |
|
223 |
apply(rule weaken_post) |
|
224 |
apply(rule_tac P = "\<lambda>l s. l ''x'' = nat(s ''x'') \<and> l ''y'' = nat(s ''y'')" and x = "''y''" in While) |
|
225 |
apply(rule Assign') |
|
226 |
apply auto[4] |
|
227 |
apply(rule Assign) |
|
228 |
apply(rule Assign') |
|
229 |
apply auto |
|
230 |
done |
|
231 |
||
67019
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
diff
changeset
|
232 |
end |