-
Notifications
You must be signed in to change notification settings - Fork 0
/
Short_Theory_12_13.thy
224 lines (191 loc) · 10.7 KB
/
Short_Theory_12_13.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
theory Short_Theory_12_13
imports "HOL-IMP.BExp" "HOL-IMP.Star"
begin
datatype
com = SKIP
| Assign vname aexp ("_ ::= _" [1000, 61] 61)
| Seq com com ("_;;/ _" [60, 61] 60)
| If bexp com com ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61)
| While bexp com ("(WHILE _/ DO _)" [0, 61] 61)
| Or com com ("(_/ OR _)" [0, 61] 61)
inductive
big_step :: "com \<times> state \<Rightarrow> state \<Rightarrow> bool" (infix "\<Rightarrow>" 55)
where
Skip: "(SKIP, s) \<Rightarrow> s" |
Assign: "(x ::= a, s) \<Rightarrow> s(x := aval a s)" |
Seq: "\<lbrakk>(c\<^sub>1, s\<^sub>1) \<Rightarrow> s\<^sub>2; (c\<^sub>2, s\<^sub>2) \<Rightarrow> s\<^sub>3\<rbrakk> \<Longrightarrow> (c\<^sub>1;; c\<^sub>2, s\<^sub>1) \<Rightarrow> s\<^sub>3" |
IfTrue: "\<lbrakk>bval b s; (c\<^sub>1, s) \<Rightarrow> s'\<rbrakk> \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<Rightarrow> s'" |
IfFalse: "\<lbrakk>\<not>bval b s; (c\<^sub>2, s) \<Rightarrow> s'\<rbrakk> \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<Rightarrow> s'" |
WhileFalse: "\<not>bval b s \<Longrightarrow> (WHILE b DO c,s) \<Rightarrow> s" |
WhileTrue: "\<lbrakk>bval b s\<^sub>1; (c, s\<^sub>1) \<Rightarrow> s\<^sub>2; (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3 \<rbrakk>
\<Longrightarrow> (WHILE b DO c, s\<^sub>1) \<Rightarrow> s\<^sub>3" |
OrLeft: "(c\<^sub>1,s) \<Rightarrow> s' \<Longrightarrow> (c\<^sub>1 OR c\<^sub>2, s) \<Rightarrow> s'" |
OrRight: "(c\<^sub>2,s) \<Rightarrow> s' \<Longrightarrow> (c\<^sub>1 OR c\<^sub>2, s) \<Rightarrow> s'"
lemmas big_step_induct = big_step.induct[split_format(complete)]
declare big_step.intros [intro]
lemma BS_SkipE [elim!]: "\<lbrakk>(SKIP, s) \<Rightarrow> t; t = s \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
by (cases rule: big_step.cases) auto
lemma BS_AssignE [elim!]: "\<lbrakk>(x ::= a, s) \<Rightarrow> t; t = s(x := aval a s) \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
by (cases rule: big_step.cases) auto
lemma BS_SeqE [elim!]: "\<lbrakk>(c\<^sub>1;; c\<^sub>2, s\<^sub>1) \<Rightarrow> s\<^sub>3;
\<And>s\<^sub>2. \<lbrakk>(c\<^sub>1, s\<^sub>1) \<Rightarrow> s\<^sub>2; (c\<^sub>2, s\<^sub>2) \<Rightarrow> s\<^sub>3\<rbrakk> \<Longrightarrow> P\<rbrakk>
\<Longrightarrow> P"
by (cases rule: big_step.cases) auto
lemma BS_IfE [elim!]: "\<lbrakk>
(IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<Rightarrow> t;
\<lbrakk>bval b s; (c\<^sub>1, s) \<Rightarrow> t\<rbrakk> \<Longrightarrow> P;
\<lbrakk>\<not> bval b s; (c\<^sub>2, s) \<Rightarrow> t\<rbrakk> \<Longrightarrow> P
\<rbrakk> \<Longrightarrow> P"
by (cases rule: big_step.cases) auto
lemma BS_WhileE [elim]: "\<lbrakk>
(WHILE b DO c, s) \<Rightarrow> t;
\<lbrakk>\<not> bval b t; s = t\<rbrakk> \<Longrightarrow> P;
\<And>s\<^sub>2. \<lbrakk>bval b s; (c, s) \<Rightarrow> s\<^sub>2; (WHILE b DO c, s\<^sub>2) \<Rightarrow> t\<rbrakk> \<Longrightarrow> P
\<rbrakk> \<Longrightarrow> P"
by (cases rule: big_step.cases) auto
lemma BS_Or [elim!]: "\<lbrakk>(c\<^sub>1 OR c\<^sub>2, s) \<Rightarrow> t; (c\<^sub>1, s) \<Rightarrow> t \<Longrightarrow> P; (c\<^sub>2, s) \<Rightarrow> t \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
by (cases rule: big_step.cases) auto
abbreviation equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" (infix "\<sim>" 50) where
"c \<sim> c' \<equiv> (\<forall>s t. (c,s) \<Rightarrow> t = (c',s) \<Rightarrow> t)"
lemma "(c\<^sub>1 OR c\<^sub>2) \<sim> (c\<^sub>2 OR c\<^sub>1)" by blast
lemma unfold_while:
"(WHILE b DO c) \<sim> (IF b THEN c;; WHILE b DO c ELSE SKIP)" (is "?w \<sim> ?iw")
proof -
\<comment> \<open>to show the equivalence, we look at the derivation tree for\<close>
\<comment> \<open>each side and from that construct a derivation tree for the other side\<close>
have "(?iw, s) \<Rightarrow> t" if assm: "(?w, s) \<Rightarrow> t" for s t
proof -
from assm show ?thesis
proof cases \<comment> \<open>rule inversion on \<open>(?w, s) \<Rightarrow> t\<close>\<close>
case WhileFalse
thus ?thesis by blast
next
case WhileTrue
from \<open>bval b s\<close> \<open>(?w, s) \<Rightarrow> t\<close> obtain s' where
"(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto
\<comment> \<open>now we can build a derivation tree for the \<^text>\<open>IF\<close>\<close>
\<comment> \<open>first, the body of the True-branch:\<close>
hence "(c;; ?w, s) \<Rightarrow> t" by (rule Seq)
\<comment> \<open>then the whole \<^text>\<open>IF\<close>\<close>
with \<open>bval b s\<close> show ?thesis by (rule IfTrue)
qed
qed
moreover
\<comment> \<open>now the other direction:\<close>
have "(?w, s) \<Rightarrow> t" if assm: "(?iw, s) \<Rightarrow> t" for s t
proof -
from assm show ?thesis
proof cases \<comment> \<open>rule inversion on \<open>(?iw, s) \<Rightarrow> t\<close>\<close>
case IfFalse
hence "s = t" using \<open>(?iw, s) \<Rightarrow> t\<close> by blast
thus ?thesis using \<open>\<not>bval b s\<close> by blast
next
case IfTrue
\<comment> \<open>and for this, only the Seq-rule is applicable:\<close>
from \<open>(c;; ?w, s) \<Rightarrow> t\<close> obtain s' where
"(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto
\<comment> \<open>with this information, we can build a derivation tree for \<^text>\<open>WHILE\<close>\<close>
with \<open>bval b s\<close> show ?thesis by (rule WhileTrue)
qed
qed
ultimately
show ?thesis by blast
qed
type_synonym assn = "state \<Rightarrow> bool"
section "Hoare Logic"
definition hoare_valid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool"
("\<Turnstile> {(1_)}/ (_)/ {(1_)}" 50) where
"\<Turnstile> {P} c {Q} = (\<forall>s t. P s \<and> (c,s) \<Rightarrow> t \<longrightarrow> Q t)"
abbreviation state_subst :: "state \<Rightarrow> aexp \<Rightarrow> vname \<Rightarrow> state"
("_[_'/_]" [1000,0,0] 999) where
"s[a/x] == s(x := aval a s)"
inductive hoare :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool"
("\<turnstile> ({(1_)}/ (_)/ {(1_)})" 50) where
Skip: "\<turnstile> {P} SKIP {P}" |
Assign: "\<turnstile> {\<lambda>s. P(s[a/x])} x::=a {P}" |
Seq: "\<lbrakk> \<turnstile> {P} c\<^sub>1 {Q}; \<turnstile> {Q} c\<^sub>2 {R} \<rbrakk> \<Longrightarrow> \<turnstile> {P} c\<^sub>1;;c\<^sub>2 {R}" |
If: "\<lbrakk> \<turnstile> {\<lambda>s. P s \<and> bval b s} c\<^sub>1 {Q}; \<turnstile> {\<lambda>s. P s \<and> \<not> bval b s} c\<^sub>2 {Q} \<rbrakk>
\<Longrightarrow> \<turnstile> {P} IF b THEN c\<^sub>1 ELSE c\<^sub>2 {Q}" |
While: "\<turnstile> {\<lambda>s. P s \<and> bval b s} c {P} \<Longrightarrow>
\<turnstile> {P} WHILE b DO c {\<lambda>s. P s \<and> \<not> bval b s}" |
Or: "\<lbrakk> \<turnstile> {P} c\<^sub>1 {Q}; \<turnstile> {P} c\<^sub>2 {Q} \<rbrakk>
\<Longrightarrow> \<turnstile> {P} c\<^sub>1 OR c\<^sub>2 {Q}" |
conseq: "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile> {P} c {Q}; \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk>
\<Longrightarrow> \<turnstile> {P'} c {Q'}"
lemmas [simp] = hoare.Skip hoare.Assign hoare.Seq hoare.If hoare.Or
lemmas [intro!] = hoare.Skip hoare.Assign hoare.Seq hoare.If hoare.Or
lemma strengthen_pre: "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile> {P} c {Q} \<rbrakk> \<Longrightarrow> \<turnstile> {P'} c {Q}"
by (blast intro: conseq)
lemma weaken_post: "\<lbrakk> \<turnstile> {P} c {Q}; \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk> \<Longrightarrow> \<turnstile> {P} c {Q'}"
by (blast intro: conseq)
lemma Assign': "\<forall>s. P s \<longrightarrow> Q(s[a/x]) \<Longrightarrow> \<turnstile> {P} x ::= a {Q}"
by (simp add: strengthen_pre[OF _ Assign])
lemma While':
assumes "\<turnstile> {\<lambda>s. P s \<and> bval b s} c {P}"
and "\<forall>s. P s \<and> \<not> bval b s \<longrightarrow> Q s"
shows "\<turnstile> {P} WHILE b DO c {Q}"
by(rule weaken_post[OF While[OF assms(1)] assms(2)])
subsection \<open>Soundness and Completeness\<close>
lemma hoare_sound: "\<turnstile> {P}c{Q} \<Longrightarrow> \<Turnstile> {P}c{Q}"
proof(induction rule: hoare.induct)
case (While P b c)
have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> P s \<Longrightarrow> P t \<and> \<not> bval b t" for s t
proof(induction "WHILE b DO c" s t rule: big_step_induct)
case WhileFalse thus ?case by blast
next
case WhileTrue thus ?case
using While.IH unfolding hoare_valid_def by blast
qed
thus ?case unfolding hoare_valid_def by blast
qed (auto simp: hoare_valid_def)
definition wp :: "com \<Rightarrow> assn \<Rightarrow> assn" where
"wp c Q = (\<lambda>s. \<forall>t. (c,s) \<Rightarrow> t \<longrightarrow> Q t)"
lemma wp_SKIP[simp]: "wp SKIP Q = Q"
by (rule ext) (auto simp: wp_def)
lemma wp_Ass[simp]: "wp (x::=a) Q = (\<lambda>s. Q(s[a/x]))"
by (rule ext) (auto simp: wp_def)
lemma wp_Seq[simp]: "wp (c\<^sub>1;;c\<^sub>2) Q = wp c\<^sub>1 (wp c\<^sub>2 Q)"
by (rule ext) (auto simp: wp_def)
lemma wp_If[simp]:
"wp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) Q =
(\<lambda>s. if bval b s then wp c\<^sub>1 Q s else wp c\<^sub>2 Q s)"
by (rule ext) (auto simp: wp_def)
lemma wp_While_If:
"wp (WHILE b DO c) Q s =
wp (IF b THEN c;;WHILE b DO c ELSE SKIP) Q s"
unfolding wp_def by (metis unfold_while)
lemma wp_While_True[simp]: "bval b s \<Longrightarrow>
wp (WHILE b DO c) Q s = wp (c;; WHILE b DO c) Q s"
by(simp add: wp_While_If)
lemma wp_While_False[simp]: "\<not> bval b s \<Longrightarrow> wp (WHILE b DO c) Q s = Q s"
by(simp add: wp_While_If)
lemma wp_Or[simp]:
"wp (c\<^sub>1 OR c\<^sub>2) Q =
(\<lambda>s. wp c\<^sub>1 Q s \<and> wp c\<^sub>2 Q s)"
by (rule ext) (auto simp: wp_def)
lemma wp_is_pre: "\<turnstile> {wp c Q} c {Q}"
proof(induction c arbitrary: Q)
case If thus ?case by (auto intro: conseq)
next
case (While b c)
let ?w = "WHILE b DO c"
show "\<turnstile> {wp ?w Q} ?w {Q}"
proof(rule While')
show "\<turnstile> {\<lambda>s. wp ?w Q s \<and> bval b s} c {wp ?w Q}"
proof(rule strengthen_pre[OF _ While.IH])
show "\<forall>s. wp ?w Q s \<and> bval b s \<longrightarrow> wp c (wp ?w Q) s" by auto
qed
show "\<forall>s. wp ?w Q s \<and> \<not> bval b s \<longrightarrow> Q s" by auto
qed
next
case Or thus ?case by (auto intro: conseq)
qed auto
lemma hoare_complete: assumes "\<Turnstile> {P} c {Q}" shows "\<turnstile> {P} c {Q}"
proof(rule strengthen_pre)
show "\<forall>s. P s \<longrightarrow> wp c Q s" using assms
by (auto simp: hoare_valid_def wp_def)
show "\<turnstile> {wp c Q} c {Q}" by (rule wp_is_pre)
qed
corollary hoare_sound_complete: "\<turnstile> {P} c {Q} \<longleftrightarrow> \<Turnstile> {P} c {Q}"
by (metis hoare_complete hoare_sound)
end