1(*
2    Author:      Norbert Schirmer
3    Maintainer:  Norbert Schirmer, norbert.schirmer at web de
4    License:     LGPL
5*)
6
7(*  Title:      Hoare.thy
8    Author:     Norbert Schirmer, TU Muenchen
9
10Copyright (C) 2004-2008 Norbert Schirmer
11Some rights reserved, TU Muenchen
12
13This library is free software; you can redistribute it and/or modify
14it under the terms of the GNU Lesser General Public License as
15published by the Free Software Foundation; either version 2.1 of the
16License, or (at your option) any later version.
17
18This library is distributed in the hope that it will be useful, but
19WITHOUT ANY WARRANTY; without even the implied warranty of
20MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
21Lesser General Public License for more details.
22
23You should have received a copy of the GNU Lesser General Public
24License along with this library; if not, write to the Free Software
25Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
26USA
27*)
28
29section \<open>Auxiliary Definitions/Lemmas to Facilitate Hoare Logic\<close>
30theory Hoare imports HoarePartial HoareTotal begin
31
32
33syntax
34
35"_hoarep_emptyFaults"::
36"[('s,'p,'f) body,('s,'p) quadruple set,
37   'f set,'s assn,('s,'p,'f) com, 's assn,'s assn] => bool"
38    ("(3_,_/\<turnstile> (_/ (_)/ _,/_))" [61,60,1000,20,1000,1000]60)
39
40"_hoarep_emptyCtx"::
41"[('s,'p,'f) body,'f set,'s assn,('s,'p,'f) com, 's assn,'s assn] => bool"
42    ("(3_/\<turnstile>\<^bsub>'/_\<^esub> (_/ (_)/ _,/_))" [61,60,1000,20,1000,1000]60)
43
44"_hoarep_emptyCtx_emptyFaults"::
45"[('s,'p,'f) body,'s assn,('s,'p,'f) com, 's assn,'s assn] => bool"
46    ("(3_/\<turnstile> (_/ (_)/ _,/_))" [61,1000,20,1000,1000]60)
47
48"_hoarep_noAbr"::
49"[('s,'p,'f) body,('s,'p) quadruple set,'f set,
50    's assn,('s,'p,'f) com, 's assn] => bool"
51    ("(3_,_/\<turnstile>\<^bsub>'/_\<^esub> (_/ (_)/ _))" [61,60,60,1000,20,1000]60)
52
53"_hoarep_noAbr_emptyFaults"::
54"[('s,'p,'f) body,('s,'p) quadruple set,'s assn,('s,'p,'f) com, 's assn] => bool"
55    ("(3_,_/\<turnstile> (_/ (_)/ _))" [61,60,1000,20,1000]60)
56
57"_hoarep_emptyCtx_noAbr"::
58"[('s,'p,'f) body,'f set,'s assn,('s,'p,'f) com, 's assn] => bool"
59    ("(3_/\<turnstile>\<^bsub>'/_\<^esub> (_/ (_)/ _))" [61,60,1000,20,1000]60)
60
61"_hoarep_emptyCtx_noAbr_emptyFaults"::
62"[('s,'p,'f) body,'s assn,('s,'p,'f) com, 's assn] => bool"
63    ("(3_/\<turnstile> (_/ (_)/ _))" [61,1000,20,1000]60)
64
65
66
67"_hoaret_emptyFaults"::
68"[('s,'p,'f) body,('s,'p) quadruple set,
69    's assn,('s,'p,'f) com, 's assn,'s assn] => bool"
70    ("(3_,_/\<turnstile>\<^sub>t (_/ (_)/ _,/_))" [61,60,1000,20,1000,1000]60)
71
72"_hoaret_emptyCtx"::
73"[('s,'p,'f) body,'f set,'s assn,('s,'p,'f) com, 's assn,'s assn] => bool"
74    ("(3_/\<turnstile>\<^sub>t\<^bsub>'/_\<^esub> (_/ (_)/ _,/_))" [61,60,1000,20,1000,1000]60)
75
76"_hoaret_emptyCtx_emptyFaults"::
77"[('s,'p,'f) body,'s assn,('s,'p,'f) com, 's assn,'s assn] => bool"
78    ("(3_/\<turnstile>\<^sub>t (_/ (_)/ _,/_))" [61,1000,20,1000,1000]60)
79
80"_hoaret_noAbr"::
81"[('s,'p,'f) body,'f set, ('s,'p) quadruple set,
82    's assn,('s,'p,'f) com, 's assn] => bool"
83    ("(3_,_/\<turnstile>\<^sub>t\<^bsub>'/_\<^esub> (_/ (_)/ _))" [61,60,60,1000,20,1000]60)
84
85"_hoaret_noAbr_emptyFaults"::
86"[('s,'p,'f) body,('s,'p) quadruple set,'s assn,('s,'p,'f) com, 's assn] => bool"
87    ("(3_,_/\<turnstile>\<^sub>t (_/ (_)/ _))" [61,60,1000,20,1000]60)
88
89"_hoaret_emptyCtx_noAbr"::
90"[('s,'p,'f) body,'f set,'s assn,('s,'p,'f) com, 's assn] => bool"
91    ("(3_/\<turnstile>\<^sub>t\<^bsub>'/_\<^esub> (_/ (_)/ _))" [61,60,1000,20,1000]60)
92
93"_hoaret_emptyCtx_noAbr_emptyFaults"::
94"[('s,'p,'f) body,'s assn,('s,'p,'f) com, 's assn] => bool"
95    ("(3_/\<turnstile>\<^sub>t (_/ (_)/ _))" [61,1000,20,1000]60)
96
97
98syntax (ASCII)
99
100"_hoarep_emptyFaults"::
101"[('s,'p,'f) body,('s,'p) quadruple set,
102     's assn,('s,'p,'f) com, 's assn,'s assn] \<Rightarrow> bool"
103   ("(3_,_/|- (_/ (_)/ _,/_))" [61,60,1000,20,1000,1000]60)
104
105"_hoarep_emptyCtx"::
106"[('s,'p,'f) body,'f set,'s assn,('s,'p,'f) com, 's assn,'s assn] => bool"
107   ("(3_/|-'/_ (_/ (_)/ _,/_))" [61,60,1000,20,1000,1000]60)
108
109"_hoarep_emptyCtx_emptyFaults"::
110"[('s,'p,'f) body,'s assn,('s,'p,'f) com, 's assn,'s assn] => bool"
111   ("(3_/|-(_/ (_)/ _,/_))" [61,1000,20,1000,1000]60)
112
113"_hoarep_noAbr"::
114"[('s,'p,'f) body,('s,'p) quadruple set,'f set,
115   's assn,('s,'p,'f) com, 's assn] => bool"
116   ("(3_,_/|-'/_ (_/ (_)/ _))" [61,60,60,1000,20,1000]60)
117
118"_hoarep_noAbr_emptyFaults"::
119"[('s,'p,'f) body,('s,'p) quadruple set,'s assn,('s,'p,'f) com, 's assn] => bool"
120   ("(3_,_/|-(_/ (_)/ _))" [61,60,1000,20,1000]60)
121
122"_hoarep_emptyCtx_noAbr"::
123"[('s,'p,'f) body,'f set,'s assn,('s,'p,'f) com, 's assn] => bool"
124   ("(3_/|-'/_ (_/ (_)/ _))" [61,60,1000,20,1000]60)
125
126"_hoarep_emptyCtx_noAbr_emptyFaults"::
127"[('s,'p,'f) body,'s assn,('s,'p,'f) com, 's assn] => bool"
128   ("(3_/|-(_/ (_)/ _))" [61,1000,20,1000]60)
129
130"_hoaret_emptyFault"::
131"[('s,'p,'f) body,('s,'p) quadruple set,
132     's assn,('s,'p,'f) com, 's assn,'s assn] => bool"
133   ("(3_,_/|-t (_/ (_)/ _,/_))" [61,60,1000,20,1000,1000]60)
134
135"_hoaret_emptyCtx"::
136"[('s,'p,'f) body,'f set,'s assn,('s,'p,'f) com, 's assn,'s assn] => bool"
137   ("(3_/|-t'/_ (_/ (_)/ _,/_))" [61,60,1000,20,1000,1000]60)
138
139"_hoaret_emptyCtx_emptyFaults"::
140"[('s,'p,'f) body,'s assn,('s,'p,'f) com, 's assn,'s assn] => bool"
141   ("(3_/|-t(_/ (_)/ _,/_))" [61,1000,20,1000,1000]60)
142
143"_hoaret_noAbr"::
144"[('s,'p,'f) body,('s,'p) quadruple set,'f set,
145   's assn,('s,'p,'f) com, 's assn] => bool"
146   ("(3_,_/|-t'/_ (_/ (_)/ _))" [61,60,60,1000,20,1000]60)
147
148"_hoaret_noAbr_emptyFaults"::
149"[('s,'p,'f) body,('s,'p) quadruple set,'s assn,('s,'p,'f) com, 's assn] => bool"
150   ("(3_,_/|-t(_/ (_)/ _))" [61,60,1000,20,1000]60)
151
152"_hoaret_emptyCtx_noAbr"::
153"[('s,'p,'f) body,'f set,'s assn,('s,'p,'f) com, 's assn] => bool"
154   ("(3_/|-t'/_ (_/ (_)/ _))" [61,60,1000,20,1000]60)
155
156"_hoaret_emptyCtx_noAbr_emptyFaults"::
157"[('s,'p,'f) body,'s assn,('s,'p,'f) com, 's assn] => bool"
158   ("(3_/|-t(_/ (_)/ _))" [61,1000,20,1000]60)
159
160translations
161
162
163 "\<Gamma>\<turnstile> P c Q,A"  == "\<Gamma>\<turnstile>\<^bsub>/{}\<^esub> P c Q,A"
164 "\<Gamma>\<turnstile>\<^bsub>/F\<^esub> P c Q,A"  == "\<Gamma>,{}\<turnstile>\<^bsub>/F\<^esub> P c Q,A"
165
166 "\<Gamma>,\<Theta>\<turnstile> P c Q"  == "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/{}\<^esub> P c Q"
167 "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q"  == "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,{}"
168 "\<Gamma>,\<Theta>\<turnstile> P c Q,A" == "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/{}\<^esub> P c Q,A"
169
170 "\<Gamma>\<turnstile> P c Q"    ==  "\<Gamma>\<turnstile>\<^bsub>/{}\<^esub> P c Q"
171 "\<Gamma>\<turnstile>\<^bsub>/F\<^esub> P c Q"  == "\<Gamma>,{}\<turnstile>\<^bsub>/F\<^esub> P c Q"
172 "\<Gamma>\<turnstile>\<^bsub>/F\<^esub> P c Q"  <=  "\<Gamma>\<turnstile>\<^bsub>/F\<^esub> P c Q,{}"
173 "\<Gamma>\<turnstile> P c Q"    <=  "\<Gamma>\<turnstile> P c Q,{}"
174
175
176
177
178 "\<Gamma>\<turnstile>\<^sub>t P c Q,A"   == "\<Gamma>\<turnstile>\<^sub>t\<^bsub>/{}\<^esub> P c Q,A"
179 "\<Gamma>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"  == "\<Gamma>,{}\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
180
181 "\<Gamma>,\<Theta>\<turnstile>\<^sub>t P c Q"   == "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/{}\<^esub> P c Q"
182 "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q" == "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,{}"
183 "\<Gamma>,\<Theta>\<turnstile>\<^sub>t P c Q,A"   == "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/{}\<^esub> P c Q,A"
184
185 "\<Gamma>\<turnstile>\<^sub>t P c Q"    == "\<Gamma>\<turnstile>\<^sub>t\<^bsub>/{}\<^esub> P c Q"
186 "\<Gamma>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q"  == "\<Gamma>,{}\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q"
187 "\<Gamma>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q"  <=  "\<Gamma>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,{}"
188 "\<Gamma>\<turnstile>\<^sub>t P c Q"    <=  "\<Gamma>\<turnstile>\<^sub>t P c Q,{}"
189
190
191term "\<Gamma>\<turnstile> P c Q"
192term "\<Gamma>\<turnstile> P c Q,A"
193
194term "\<Gamma>\<turnstile>\<^bsub>/F\<^esub> P c Q"
195term "\<Gamma>\<turnstile>\<^bsub>/F\<^esub> P c Q,A"
196
197term "\<Gamma>,\<Theta>\<turnstile> P c Q"
198term "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q"
199
200term "\<Gamma>,\<Theta>\<turnstile> P c Q,A"
201term "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A"
202
203
204term "\<Gamma>\<turnstile>\<^sub>t P c Q"
205term "\<Gamma>\<turnstile>\<^sub>t P c Q,A"
206
207term "\<Gamma>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q"
208term "\<Gamma>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
209
210term "\<Gamma>,\<Theta>\<turnstile> P c Q"
211term "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q"
212
213term "\<Gamma>,\<Theta>\<turnstile> P c Q,A"
214term "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
215
216
217locale hoare =
218  fixes \<Gamma>::"('s,'p,'f) body"
219
220
221primrec assoc:: "('a \<times>'b) list \<Rightarrow> 'a \<Rightarrow> 'b "
222where
223"assoc [] x = undefined" |
224"assoc (p#ps) x = (if fst p = x then (snd p) else assoc ps x)"
225
226lemma conjE_simp: "(P \<and> Q \<Longrightarrow> PROP R) \<equiv> (P \<Longrightarrow> Q \<Longrightarrow> PROP R)"
227  by rule simp_all
228
229lemma CollectInt_iff: "{s. P s} \<inter> {s. Q s} = {s. P s \<and> Q s}"
230  by auto
231
232lemma Compl_Collect:"-(Collect b) = {x. \<not>(b x)}"
233  by fastforce
234
235lemma Collect_False: "{s. False} = {}"
236  by simp
237
238lemma Collect_True: "{s. True} = UNIV"
239  by simp
240
241lemma triv_All_eq: "\<forall>x. P \<equiv> P"
242  by simp
243
244lemma triv_Ex_eq: "\<exists>x. P \<equiv> P"
245  by simp
246
247lemma Ex_True: "\<exists>b. b"
248   by blast
249
250lemma Ex_False: "\<exists>b. \<not>b"
251  by blast
252
253definition mex::"('a \<Rightarrow> bool) \<Rightarrow> bool"
254  where "mex P = Ex P"
255
256definition meq::"'a \<Rightarrow> 'a \<Rightarrow> bool"
257  where "meq s Z = (s = Z)"
258
259lemma subset_unI1: "A \<subseteq> B \<Longrightarrow> A \<subseteq> B \<union> C"
260  by blast
261
262lemma subset_unI2: "A \<subseteq> C \<Longrightarrow> A \<subseteq> B \<union> C"
263  by blast
264
265lemma split_paired_UN: "(\<Union>p. (P p)) = (\<Union>a b. (P (a,b)))"
266  by auto
267
268lemma in_insert_hd: "f \<in> insert f X"
269  by simp
270
271lemma lookup_Some_in_dom: "\<Gamma> p = Some bdy \<Longrightarrow> p \<in> dom \<Gamma>"
272  by auto
273
274lemma unit_object: "(\<forall>u::unit. P u) = P ()"
275  by auto
276
277lemma unit_ex: "(\<exists>u::unit. P u) = P ()"
278  by auto
279
280lemma unit_meta: "(\<And>(u::unit). PROP P u) \<equiv> PROP P ()"
281  by auto
282
283lemma unit_UN: "(\<Union>z::unit. P z) = P ()"
284  by auto
285
286lemma subset_singleton_insert1: "y = x \<Longrightarrow> {y} \<subseteq> insert x A"
287  by auto
288
289lemma subset_singleton_insert2: "{y} \<subseteq> A \<Longrightarrow> {y} \<subseteq> insert x A"
290  by auto
291
292lemma in_Specs_simp: "(\<forall>x\<in>\<Union>Z. {(P Z, p, Q Z, A Z)}. Prop x) =
293       (\<forall>Z. Prop (P Z,p,Q Z,A Z))"
294  by auto
295
296lemma in_set_Un_simp: "(\<forall>x\<in>A \<union> B. P x) = ((\<forall>x \<in> A. P x) \<and> (\<forall>x \<in> B. P x))"
297  by auto
298
299lemma split_all_conj: "(\<forall>x. P x \<and> Q x) = ((\<forall>x. P x) \<and> (\<forall>x. Q x))"
300  by blast
301
302lemma image_Un_single_simp: "f ` (\<Union>Z. {P Z}) = (\<Union>Z. {f (P Z)}) "
303  by auto
304
305
306
307lemma measure_lex_prod_def':
308  "f <*mlex*> r \<equiv> ({(x,y). (x,y) \<in> measure f \<or> f x=f y \<and> (x,y) \<in>  r})"
309  by (auto simp add: mlex_prod_def inv_image_def)
310
311lemma in_measure_iff: "(x,y) \<in> measure f = (f x < f y)"
312  by (simp add: measure_def inv_image_def)
313
314lemma in_lex_iff:
315  "((a,b),(x,y)) \<in> r <*lex*> s = ((a,x) \<in> r \<or> (a=x \<and> (b,y)\<in>s))"
316  by (simp add: lex_prod_def)
317
318lemma in_mlex_iff:
319  "(x,y) \<in> f <*mlex*> r = (f x < f y \<or> (f x=f y \<and> (x,y) \<in> r))"
320  by (simp add: measure_lex_prod_def' in_measure_iff)
321
322lemma in_inv_image_iff: "(x,y) \<in> inv_image r f = ((f x, f y) \<in> r)"
323  by (simp add: inv_image_def)
324
325text \<open>This is actually the same as @{thm [source] wf_mlex}. However, this basic
326proof took me so long that I'm not willing to delete it.
327\<close>
328lemma wf_measure_lex_prod [simp,intro]:
329  assumes wf_r: "wf r"
330  shows "wf (f <*mlex*> r)"
331proof (rule ccontr)
332  assume " \<not> wf (f <*mlex*> r)"
333  then
334  obtain g where "\<forall>i. (g (Suc i), g i) \<in> f <*mlex*> r"
335    by (auto simp add: wf_iff_no_infinite_down_chain)
336  hence g: "\<forall>i. (g (Suc i), g i) \<in> measure f \<or>
337    f (g (Suc i)) = f (g i) \<and> (g (Suc i), g i) \<in> r"
338    by (simp add: measure_lex_prod_def')
339  hence le_g: "\<forall>i. f (g (Suc i)) \<le> f (g i)"
340    by (auto simp add: in_measure_iff order_le_less)
341  have "wf (measure f)"
342    by simp
343  hence " \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> measure f \<longrightarrow> y \<notin> Q)"
344    by (simp add: wf_eq_minimal)
345  from this [rule_format, of "g ` UNIV"]
346  have "\<exists>z. z \<in> range g \<and> (\<forall>y. (y, z) \<in> measure f \<longrightarrow> y \<notin> range g)"
347    by auto
348  then obtain z where
349    z: "z \<in> range g" and
350    min_z: "\<forall>y. f y < f z \<longrightarrow> y \<notin> range g"
351    by (auto simp add: in_measure_iff)
352  from z obtain k where
353    k: "z = g k"
354    by auto
355  have "\<forall>i. k \<le> i \<longrightarrow> f (g i) = f (g k)"
356  proof (intro allI impI)
357    fix i
358    assume "k \<le> i" then show "f (g i) = f (g k)"
359    proof (induct i)
360      case 0
361      have "k \<le> 0" by fact hence "k = 0" by simp
362      thus "f (g 0) = f (g k)"
363        by simp
364    next
365      case (Suc n)
366      have k_Suc_n: "k \<le> Suc n" by fact
367      then show "f (g (Suc n)) = f (g k)"
368      proof (cases "k = Suc n")
369        case True
370        thus ?thesis by simp
371      next
372        case False
373        with k_Suc_n
374        have "k \<le> n"
375          by simp
376        with Suc.hyps
377        have n_k: "f (g n) = f (g k)" by simp
378        from le_g have le: "f (g (Suc n)) \<le> f (g n)"
379          by simp
380        show ?thesis
381        proof (cases "f (g (Suc n)) = f (g n)")
382          case True with n_k show ?thesis by simp
383        next
384          case False
385          with le have "f (g (Suc n)) < f (g n)"
386            by simp
387          with n_k k have "f (g (Suc n)) < f z"
388            by simp
389          with min_z have "g (Suc n) \<notin> range g"
390            by blast
391          hence False by simp
392          thus ?thesis
393            by simp
394        qed
395      qed
396    qed
397  qed
398  with k [symmetric] have "\<forall>i. k \<le> i \<longrightarrow> f (g i) = f z"
399    by simp
400  hence "\<forall>i. k \<le> i \<longrightarrow> f (g (Suc i)) = f (g i)"
401    by simp
402  with g have "\<forall>i. k \<le> i \<longrightarrow> (g (Suc i),(g i)) \<in> r"
403    by (auto simp add: in_measure_iff order_less_le )
404  hence "\<forall>i. (g (Suc (i+k)),(g (i+k))) \<in> r"
405    by simp
406  then
407  have "\<exists>f. \<forall>i. (f (Suc i), f i) \<in> r"
408    by - (rule exI [where x="\<lambda>i. g (i+k)"],simp)
409  with wf_r show False
410    by (simp add: wf_iff_no_infinite_down_chain)
411qed
412
413lemmas all_imp_to_ex = all_simps (5)
414(*"\<And>P Q. (\<forall>x. P x \<longrightarrow> Q) = ((\<exists>x. P x) \<longrightarrow> Q)"
415
416 Avoid introduction of existential quantification of states on negative
417 position.
418*)
419
420lemma all_imp_eq_triv: "(\<forall>x. x = k \<longrightarrow> Q) = Q"
421                       "(\<forall>x. k = x \<longrightarrow> Q) = Q"
422  by auto
423
424end
425