-
Notifications
You must be signed in to change notification settings - Fork 108
/
Extended_Separation_Algebra.thy
639 lines (540 loc) · 25.4 KB
/
Extended_Separation_Algebra.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
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
(*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*)
(*
Adds positivity law to separation algebra, as well as defining
the septraction and sep-coimplication operators, providing lemmas
for each.
*)
theory Extended_Separation_Algebra
imports
Lib.Lib
"Sep_Tactics"
begin
no_notation pred_and (infixr "and" 35)
no_notation pred_or (infixr "or" 30)
no_notation pred_not ("not _" [40] 40)
no_notation pred_imp (infixr "imp" 25)
lemma sep_conj_exists_left[simp]: "((\<lambda>s. \<exists>x. (P x) s) \<and>* R) \<equiv> (EXS x. (P x \<and>* R)) "
apply (rule eq_reflection)
by (clarsimp simp: sep_conj_def, fastforce)
instantiation "bool" :: stronger_sep_algebra
begin
definition "zero_bool \<equiv> True"
definition "plus_bool \<equiv> \<lambda>(x :: bool) (y :: bool). x \<and> y"
definition "sep_disj_bool \<equiv> \<lambda>(x :: bool) (y :: bool). x \<or> y"
instance
by (intro_classes; fastforce simp: zero_bool_def plus_bool_def sep_disj_bool_def)
end
instantiation "prod" :: (stronger_sep_algebra, stronger_sep_algebra) stronger_sep_algebra
begin
definition "zero_prod \<equiv> (0,0)"
definition "plus_prod p p' \<equiv> (fst p + fst p', snd p + snd p')"
definition "sep_disj_prod p p' \<equiv> fst p ## fst p' \<and> snd p ## snd p'"
instance
apply (intro_classes; simp add: zero_prod_def plus_prod_def sep_disj_prod_def)
apply (simp add: sep_add_assoc | fastforce simp: sep_disj_commute sep_add_commute)+
done
end
instantiation "fun" :: (type, pre_sep_algebra) pre_sep_algebra
begin
definition "zero_fun = (\<lambda>x. 0)"
definition "plus_fun f f' \<equiv> (\<lambda>x. (f x) + (f' x) )"
definition "sep_disj_fun \<equiv> (\<lambda>f f'. \<forall>x. f x ## f' x ) :: ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool "
instance
apply (intro_classes)
apply (clarsimp simp: comp_def sep_disj_fun_def )
apply (clarsimp simp: zero_fun_def sep_disj_fun_def plus_fun_def )
apply (clarsimp simp: zero_fun_def comp_def sep_disj_fun_def plus_fun_def )
apply (simp add: sep_disj_commute)
apply (clarsimp simp: zero_fun_def sep_disj_commuteI sep_disj_fun_def plus_fun_def)
apply (clarsimp simp: zero_fun_def sep_disj_commuteI sep_disj_fun_def plus_fun_def sep_add_commute)
apply (clarsimp simp: zero_fun_def sep_disj_commuteI sep_disj_fun_def plus_fun_def sep_add_commute sep_add_assoc)
done
end
instantiation "fun" :: (type, sep_algebra) sep_algebra
begin
instance
apply (intro_classes)
apply (clarsimp simp: zero_fun_def sep_disj_fun_def plus_fun_def )
using sep_disj_addD apply blast
apply (clarsimp simp: zero_fun_def comp_def sep_disj_fun_def plus_fun_def )
by (simp add: sep_disj_addI1)
end
instantiation option :: (type) sep_algebra begin
definition "sep_disj_option (h :: 'a option) (h' :: 'a option) =
(case h of (Some x) \<Rightarrow> h' = None | _ \<Rightarrow> h = None)"
definition "plus_option (h :: 'a option) (h' :: 'a option) =
(case h of (Some x) \<Rightarrow> h | _ \<Rightarrow> h')"
definition "zero_option = None"
instance
apply (intro_classes)
by (clarsimp simp: sep_disj_option_def zero_option_def plus_option_def split: option.splits)+
end
instantiation option :: (type) cancellative_sep_algebra begin
instance
apply (intro_classes)
apply (simp add: option.case_eq_if plus_option_def sep_disj_option_def)
apply (clarsimp simp: zero_option_def option.case_eq_if plus_option_def sep_disj_option_def split: if_split_asm option.splits)
apply (clarsimp simp: zero_option_def option.case_eq_if plus_option_def sep_disj_option_def split: if_split_asm option.splits)
done
end
instantiation "fun" :: (type, cancellative_sep_algebra) cancellative_sep_algebra begin
instance
apply (intro_classes)
apply (clarsimp simp: plus_fun_def sep_disj_fun_def zero_fun_def)
apply (safe; fastforce)
apply (clarsimp simp: plus_fun_def sep_disj_fun_def zero_fun_def)
apply (rule ext)
apply (meson sep_disj_positive)
apply (rule ext)
apply (clarsimp simp: plus_fun_def sep_disj_fun_def zero_fun_def)
by (meson sep_add_cancel)
end
lemma sep_substate_antisym:
"x \<preceq> y \<Longrightarrow> y \<preceq> x \<Longrightarrow> x = (y :: 'a ::cancellative_sep_algebra)"
apply (clarsimp simp: sep_substate_def)
apply (rename_tac h' h)
apply (subgoal_tac "h' = 0")
apply (clarsimp)
apply (drule_tac trans[where s=x and t="x+0"])
apply (clarsimp)
apply (subgoal_tac "(x + h' + h = x + 0) \<longrightarrow> ((0 + x) = (h' + h) + x)")
apply (drule mp, clarsimp)
apply (metis sep_add_cancelD sep_add_disj_eq sep_disj_commuteI sep_disj_positive_zero sep_disj_zero)
by (metis sep_add_assoc sep_add_commute sep_add_zero sep_add_zero_sym sep_disj_commuteI)
context sep_algebra begin
definition
septraction :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)" (infix "-*" 25)
where
"septraction P Q = (not (P \<longrightarrow>* not Q))"
lemma septraction_impl1:
"(P -* Q) s \<Longrightarrow> (\<And>s. P s \<Longrightarrow> P' s) \<Longrightarrow> (P' -* Q) s "
apply (clarsimp simp: septraction_def pred_neg_def)
using sep_impl_def by auto
lemma septraction_impl2:
"(P -* Q) s \<Longrightarrow> (\<And>s. Q s \<Longrightarrow> Q' s) \<Longrightarrow> (P -* Q') s "
apply (clarsimp simp: septraction_def pred_neg_def)
using sep_impl_def by auto
definition
sep_coimpl :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)" (infix "\<leadsto>*" 24)
where
"sep_coimpl P Q \<equiv> \<lambda>s. \<not> (P \<and>* not Q) s"
lemma sep_septraction_snake:
"(P -* Q) s \<Longrightarrow> (\<And>s. Q s \<Longrightarrow> (P \<leadsto>* Q') s) \<Longrightarrow> Q' s"
apply (clarsimp simp: sep_coimpl_def septraction_def pred_neg_def sep_conj_def sep_impl_def)
using sep_add_commute sep_disj_commute by auto
lemma sep_snake_septraction:
"Q s \<Longrightarrow> (\<And>s. (P -* Q) s \<Longrightarrow> Q' s) \<Longrightarrow> (P \<leadsto>* Q') s "
apply (clarsimp simp: sep_coimpl_def septraction_def pred_neg_def sep_conj_def sep_impl_def)
using sep_add_commute sep_disj_commute by fastforce
lemma septraction_snake_trivial:
"(P -* (P \<leadsto>* R)) s \<Longrightarrow> R s" by (erule sep_septraction_snake)
end
lemma sep_impl_impl:
"(P \<longrightarrow>* Q) s\<Longrightarrow> (\<And>s. Q s \<Longrightarrow> Q' s) \<Longrightarrow> (P \<longrightarrow>* Q') s"
by (metis sep_implD sep_implI)
lemma disjointness_equiv:
"(\<forall>P (s :: 'a :: sep_algebra). strictly_exact P \<longrightarrow> \<not>P 0 \<longrightarrow> (P \<leadsto>* (P \<leadsto>* sep_false)) s) =
(\<forall>h :: 'a. h ## h \<longrightarrow> h = 0)"
apply (rule iffI)
apply (clarsimp)
apply (erule_tac x="(=) h" in allE)
apply (drule mp)
apply (clarsimp simp: strictly_exact_def)
apply (rule ccontr)
apply (drule mp)
apply (clarsimp)
apply (erule_tac x="h + h" in allE)
apply (clarsimp simp: sep_coimpl_def sep_conj_def pred_neg_def)
apply (erule_tac x=h in allE, clarsimp)
apply (erule_tac x=0 in allE, clarsimp)
apply (clarsimp)
apply (clarsimp simp: sep_coimpl_def sep_conj_def pred_neg_def strictly_exact_def)
apply (erule_tac x=x in allE, erule_tac x=xa in allE, clarsimp simp: sep_empty_def)
apply (erule_tac x=x in allE, clarsimp)
using sep_disj_addD1 by blast
definition
sep_min :: "(('a :: sep_algebra) \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)" where
"sep_min P \<equiv> P and (P \<leadsto>* \<box>)"
definition
sep_subtract :: "(('a :: sep_algebra) \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)" where
"sep_subtract P Q \<equiv> P and (Q \<leadsto>* \<box>)"
lemma sep_min_subtract_subtract:
"sep_min P = sep_subtract P P"
apply (clarsimp simp: sep_subtract_def sep_min_def)
done
lemma sep_subtract_distrib_disj:
"sep_subtract (P or Q) R = ((sep_subtract P R) or (sep_subtract Q R))"
apply (rule ext, rule iffI)
apply (clarsimp simp: pred_disj_def pred_conj_def sep_subtract_def)
apply (clarsimp simp: pred_disj_def pred_conj_def sep_subtract_def)
apply (safe)
done
lemma sep_snake_sep_impl:
"(P \<longrightarrow>* R) s \<Longrightarrow> (\<And> s. R s \<Longrightarrow> (P \<leadsto>* sep_false) s) \<Longrightarrow> (not P \<and>* (not (P -* R))) s"
apply (drule sep_impl_impl[where Q'="(P \<leadsto>* sep_false)"])
apply (atomize)
apply (erule allE, drule mp, assumption)
apply (assumption)
apply (erule contrapos_pp)
apply (clarsimp simp: sep_impl_def sep_coimpl_def sep_conj_def pred_neg_def septraction_def)
apply (erule_tac x=0 in allE)
apply (erule_tac x=s in allE)
apply (clarsimp)
apply (rule_tac x=0 in exI)
apply (clarsimp)
by (metis (full_types) disjoint_zero_sym sep_add_commute sep_add_zero_sym sep_disj_commuteI)
lemma sep_snake_mp:
"(P \<leadsto>* Q) s \<Longrightarrow> (P \<and>* sep_true) s \<Longrightarrow> (P \<and>* Q) s "
apply (clarsimp simp: sep_coimpl_def)
apply (clarsimp simp: sep_conj_def sep_coimpl_def pred_neg_def)
apply (fastforce)
done
lemma sep_coimpl_contrapos:
"(P \<leadsto>* Q) = ((not Q) \<leadsto>* (not P))"
by (rule ext, rule iffI; simp add: sep_coimpl_def pred_neg_def sep_conj_commute)
lemma sep_coimpl_def':
"(\<not> (P \<and>* Q) s) = ((P \<leadsto>* (not Q)) s)"
by (simp add: pred_neg_def sep_coimpl_def)
lemma rewrite_sp:
"(\<forall>R s. (P \<leadsto>* R) s \<longrightarrow> (Q \<and>* R) (f s)) \<longleftrightarrow> (\<forall>R s. R s \<longrightarrow> (Q \<and>* (P -* R)) (f s) )"
apply (rule iffI)
apply (clarsimp)
apply (erule_tac x="P -* R" in allE)
apply (erule_tac x=s in allE)
apply (drule mp)
apply (erule (1) sep_snake_septraction)
apply (assumption)
apply (clarsimp)
apply (erule_tac x="P \<leadsto>* R" in allE)
apply (erule_tac x=s in allE)
apply (clarsimp)
apply (sep_cancel)
apply (erule (1) sep_septraction_snake)
done
lemma sep_coimpl_weaken:
"(P \<leadsto>* Q) s \<Longrightarrow> (\<And>s. P' s \<Longrightarrow> P s) \<Longrightarrow> (P' \<leadsto>* Q) s"
apply (clarsimp simp: sep_coimpl_def sep_conj_def pred_neg_def)
apply (fastforce)
done
lemma sep_curry':
"R s \<Longrightarrow> (P \<longrightarrow>* (P \<and>* R)) s"
by (simp add: sep_wand_trivial)
lemma sep_coimpl_mp_gen:
"(P \<and>* Q) s \<Longrightarrow> (P' \<leadsto>* Q') s \<Longrightarrow> (\<And>s. P s \<Longrightarrow> P' s) \<Longrightarrow> ((P and P') \<and>* (Q and Q')) s"
apply (clarsimp simp: sep_coimpl_def sep_conj_def pred_conj_def pred_neg_def)
by (fastforce simp: sep_disj_commute sep_add_commute)
lemma ex_pull:
"\<exists>h s. P h s \<and> Q h \<Longrightarrow> \<exists>h. Q h \<and> (\<exists>s. P h s)"
apply (fastforce)
done
lemma sep_mp_snake_mp:
"(P \<and>* (P \<longrightarrow>* (P \<leadsto>* Q))) s \<Longrightarrow> (P \<and>* Q) s"
apply (clarsimp simp: sep_conj_def)
apply (rename_tac x y)
apply (rule_tac x=x in exI)
apply (rule_tac x=y in exI)
apply (clarsimp)
apply (clarsimp simp: sep_impl_def)
apply (erule_tac x=x in allE)
apply (clarsimp simp: sep_disj_commute)
apply (clarsimp simp: sep_conj_def sep_coimpl_def pred_neg_def)
by (fastforce simp: sep_disj_commute sep_add_commute)
lemma septract_cancel:
"(P -* Q) s \<Longrightarrow> (\<And>s. P s \<Longrightarrow> P' s) \<Longrightarrow> (\<And>s. Q s \<Longrightarrow> Q' s) \<Longrightarrow> (P' -* Q') s"
apply (clarsimp simp: septraction_def sep_impl_def pred_neg_def)
apply (fastforce)
done
lemma sep_coimpl_mp_zero:
"(P \<leadsto>* Q) s \<Longrightarrow> P s \<Longrightarrow> Q (0)"
by (clarsimp simp: sep_coimpl_def sep_conj_def)
lemma sep_neg_not:
"(P \<leadsto>* sep_false) s \<Longrightarrow> \<not>P s"
apply (cases "P s")
apply (drule(1) sep_coimpl_mp_zero)
apply (clarsimp)
apply (simp)
done
lemma sep_antimp':
"P s \<Longrightarrow> (Q \<leadsto>* (Q -* P)) s \<and> P s"
apply (clarsimp)
apply (erule sep_snake_septraction, assumption)
done
definition
sep_precise_conj :: "(('a :: sep_algebra) \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)" where
"sep_precise_conj P \<equiv> P and (ALLS R. (sep_true \<longrightarrow>* (P \<leadsto>* R)))"
notation sep_precise_conj (infix "\<and>@" 50)
definition
coprecise :: "(('a :: sep_algebra) \<Rightarrow> bool) \<Rightarrow> bool" where
"coprecise P = (\<forall>s h h'. P h \<longrightarrow> P h' \<longrightarrow> s \<preceq> h \<longrightarrow> s \<preceq> h' \<longrightarrow> s \<noteq> 0 \<longrightarrow> h = h')"
definition
cointuitionistic :: "(('a :: sep_algebra) \<Rightarrow> bool) \<Rightarrow> bool" where
"cointuitionistic P = (\<forall>h h'. P h \<and> h' \<preceq> h \<longrightarrow> P h')"
lemma intuitionistic_def':
"intuitionistic P = (\<forall>s R. (P \<and>* R) s \<longrightarrow> P s)"
apply (rule iffI)
apply (clarsimp simp: intuitionistic_def)
apply (clarsimp simp: sep_conj_def)
using sep_substate_disj_add apply blast
apply (clarsimp simp: intuitionistic_def)
apply (erule_tac x=h' in allE)
apply (drule mp)
apply (rule_tac x=sep_true in exI)
apply (clarsimp simp:sep_conj_def sep_substate_def, fastforce)
apply (assumption)
done
lemma cointuitionistic_def':
"cointuitionistic P = (\<forall>s R. P s \<longrightarrow> (R \<leadsto>* P) s)"
apply (rule iffI)
apply (clarsimp)
apply (clarsimp simp: sep_coimpl_def)
apply (clarsimp simp: sep_conj_def pred_neg_def cointuitionistic_def)
apply (rename_tac R x y)
apply (erule_tac x="x + y" in allE)
apply (erule_tac x=y in allE)
apply (clarsimp)
using sep_disj_commuteI sep_substate_disj_add' apply blast
apply (clarsimp simp: cointuitionistic_def)
apply (erule_tac x=h in allE)
apply (clarsimp)
apply (clarsimp simp: sep_substate_def)
apply (erule_tac x="\<lambda>s. s = z" in allE)
apply (clarsimp simp: sep_coimpl_def sep_conj_def pred_neg_def)
apply (fastforce simp: sep_disj_commute sep_add_commute)
done
lemma saturated_split:
"cointuitionistic P \<Longrightarrow> P s \<Longrightarrow> (Q \<and>* R) s \<Longrightarrow> ((P and Q) \<and>* (P and R)) s"
apply (clarsimp simp: cointuitionistic_def sep_conj_def pred_conj_def)
apply (rule_tac x=x in exI)
apply (rule_tac x=y in exI)
apply (clarsimp)
using sep_disj_commuteI sep_substate_disj_add sep_substate_disj_add' by blast
lemma sep_wand_dne:
"((P \<longrightarrow>* sep_false) \<longrightarrow>* sep_false) s \<Longrightarrow> \<exists>s. P s"
apply (clarsimp simp: septraction_def pred_neg_def sep_impl_def sep_conj_def sep_coimpl_def)
apply (erule_tac x=0 in allE)
apply (clarsimp)
done
lemma sep_snake_dne:
"(sep_true \<leadsto>* P) s \<Longrightarrow> ((P \<leadsto>* sep_false) \<leadsto>* sep_false) s"
apply (clarsimp simp: septraction_def pred_neg_def sep_impl_def sep_conj_def sep_coimpl_def)
apply (rename_tac x y)
apply (erule_tac x=y in allE)
apply (erule_tac x=x in allE)
apply (rule_tac x=x in exI)
apply (rule_tac x=0 in exI)
apply (clarsimp)
apply (fastforce simp: sep_disj_commute sep_add_commute)
done
lemma strictly_exactI:
"(\<And>P s. ((P -* R) -* R) s \<Longrightarrow> P (s :: 'a :: cancellative_sep_algebra)) \<Longrightarrow> strictly_exact R"
apply (atomize)
apply (clarsimp simp: strictly_exact_def)
apply (clarsimp simp: septraction_def pred_neg_def sep_impl_def sep_conj_def sep_coimpl_def strictly_exact_def)
apply (rename_tac h h')
apply (erule_tac x="\<lambda>s. s = h" in allE)
by (metis disjoint_zero_sym sep_add_commute sep_add_zero sep_disj_zero)
lemma strictly_exact_septractD:
"strictly_exact R \<Longrightarrow> ((P -* R) -* R) s \<Longrightarrow> P (s :: 'a :: cancellative_sep_algebra)"
apply (clarsimp simp: septraction_def pred_neg_def sep_impl_def sep_conj_def sep_coimpl_def
strictly_exact_def)
by (metis sep_add_cancel sep_add_commute sep_disj_commuteI)
lemma strictly_exact_def':
"(\<forall>P s. ((P -* R) -* R) s \<longrightarrow> P (s :: 'a :: cancellative_sep_algebra)) = strictly_exact R"
using strictly_exactI strictly_exact_septractD by auto
lemma copreciseI:
"(\<forall>(s ) R. (P -* R) s \<longrightarrow> (P \<longrightarrow>* R) s) \<Longrightarrow> coprecise P"
apply (clarsimp simp: coprecise_def)
apply (clarsimp simp: sep_substate_def)
apply (erule_tac x="0" in allE)
apply (rename_tac s h h')
apply (erule_tac x="\<lambda>s'. s' = s + h" in allE)
apply (drule mp)
apply (clarsimp simp: septraction_def pred_neg_def sep_impl_def)
apply (clarsimp simp: septraction_def pred_neg_def sep_impl_def)
done
lemma sep_implI':
"strictly_exact P \<Longrightarrow> (P -* R) s \<Longrightarrow> (P \<longrightarrow>* R) s"
apply (clarsimp simp: septraction_def pred_neg_def sep_impl_def coprecise_def strictly_exact_def)
apply (fastforce)
done
lemma
"\<forall>s P. (P -* R) s \<longrightarrow> (P \<longrightarrow>* R) s \<Longrightarrow> \<exists>s. R s \<Longrightarrow> R s"
apply (clarsimp simp: coprecise_def)
apply (clarsimp simp: septraction_def pred_neg_def sep_impl_def)
by (metis disjoint_zero_sym sep_add_zero_sym)
lemma strictly_exactI':
"\<forall>s R. (P -* R) s \<longrightarrow> (P \<longrightarrow>* R) s \<Longrightarrow> strictly_exact P"
apply (clarsimp simp: strictly_exact_def)
apply (erule_tac x="0" in allE)
apply (rename_tac h h')
apply (erule_tac x="\<lambda>h. h = h'" in allE)
apply (drule mp)
apply (clarsimp simp: septraction_def pred_neg_def sep_impl_def)
apply (clarsimp simp: septraction_def pred_neg_def sep_impl_def)
done
lemma strictly_exact_def'':
"(\<forall>s R. (P -* R) s \<longrightarrow> (P \<longrightarrow>* R) s) = strictly_exact P"
using sep_implI' strictly_exactI' by blast
lemma conj_coimpl_precise:
"(\<forall>s R. (P \<and>* R) s \<longrightarrow> (P \<leadsto>* R) s) \<Longrightarrow> precise P"
apply (clarsimp simp: precise_def)
apply (clarsimp simp: sep_substate_def)
apply (rename_tac h h' z z')
apply (erule_tac x="h + z" in allE)
apply (erule_tac x="\<lambda>s. s= z" in allE)
apply (drule mp)
apply (clarsimp simp: sep_conj_def)
apply (fastforce)
apply (clarsimp simp: sep_coimpl_def sep_conj_def pred_neg_def)
using sep_add_cancel by fastforce
lemma precise_conj_coimpl:
"precise P \<Longrightarrow> (\<forall>s R. (P \<and>* R) s \<longrightarrow> (P \<leadsto>* R) s)"
apply (clarsimp simp: precise_def)
apply (clarsimp simp: sep_conj_def sep_coimpl_def pred_neg_def)
by (metis cancellative_sep_algebra_class.sep_add_cancelD sep_add_commute
sep_disj_commuteI sep_substate_disj_add)
lemma septract_cancel_eq_precise:
"(\<forall>s. ((P -* (P \<and>* R)) s \<longrightarrow> R s)) = (\<forall>s. (P \<and>* R) s \<longrightarrow> (P \<leadsto>* R) s)"
apply (rule iffI)
apply (clarsimp)
apply (clarsimp simp: sep_conj_def sep_impl_def septraction_def pred_neg_def sep_coimpl_def)
apply (rule ccontr)
apply (rename_tac x y h h')
apply (erule_tac x=h' in allE)
apply (clarsimp)
apply (erule_tac x=h in allE)
apply (clarsimp simp: sep_disj_commute)
apply (erule_tac x=x in allE)
apply (clarsimp)
apply (erule_tac x=y in allE)
apply (clarsimp)
apply (fastforce simp: sep_disj_commute sep_add_commute)
apply (clarsimp simp: septraction_def pred_neg_def sep_impl_def)
by (metis pred_neg_def sep_coimpl_def sep_conjI sep_conj_commuteI)
lemma sep_coimpl_cancel:
"(P \<leadsto>* Q) s \<Longrightarrow> ((P \<and>* Q) s \<Longrightarrow> (P \<leadsto>* Q') s) \<Longrightarrow> (P \<leadsto>* Q') s"
apply (clarsimp simp: sep_coimpl_def pred_neg_def)
apply (clarsimp simp: sep_conj_def)
by blast
lemma sep_cases:
"R s \<Longrightarrow> (P \<and>* (P -* R)) s \<or> (P \<leadsto>* (sep_false)) s"
apply (safe)
apply (clarsimp simp: sep_coimpl_def)
apply (rule ccontr)
by (meson sep_antimp' sep_conj_sep_true_right sep_snake_mp)
lemma contra:
"(\<forall>s. P s \<longrightarrow> Q s) \<Longrightarrow> (\<forall>s. \<not> Q s \<longrightarrow> \<not> P s )"
apply (safe)
by (fastforce)
lemma
"(\<forall>R s. (P \<and>* R) (s) \<longrightarrow> (Q \<and>* R) (f s) ) = (\<forall>R s. (Q \<leadsto>* R) (f s) \<longrightarrow> (P \<leadsto>* R) ( s))"
apply (clarsimp simp: sep_coimpl_def)
apply (rule iffI)
apply (clarsimp)
apply (clarsimp)
by (meson sep_coimpl_def sep_coimpl_def')
lemma
"R s \<Longrightarrow> strictly_exact R \<Longrightarrow> (P \<longrightarrow>* R) s' \<Longrightarrow> (P -* R) s' \<Longrightarrow> s' \<preceq> s \<Longrightarrow> (P \<and>* sep_true) s"
apply (clarsimp simp: sep_conj_def sep_coimpl_def pred_neg_def septraction_def sep_impl_def)
by (metis sep_add_commute sep_disj_commuteI strictly_exact_def)
lemma sep_coimpl_comb:
" (R \<leadsto>* P) s \<Longrightarrow> (R \<leadsto>* Q) s \<Longrightarrow> (R \<leadsto>* (P and Q)) s"
apply (clarsimp simp: sep_coimpl_def sep_conj_def pred_neg_def pred_conj_def)
done
lemma sep_coimpl_contra:
"(R \<leadsto>* (not Q)) s \<Longrightarrow> (R \<leadsto>* Q) s \<Longrightarrow> (R \<leadsto>* sep_false) s"
apply (drule sep_coimpl_comb, assumption)
apply (clarsimp simp: pred_neg_def pred_conj_def)
done
lemma sep_comb':
"((not Q) \<leadsto>* P) s \<Longrightarrow> (Q \<leadsto>* R) s \<Longrightarrow> ((R or P) \<and>* sep_true) s"
apply (clarsimp simp: sep_coimpl_def sep_conj_def pred_neg_def)
by (metis (full_types) disjoint_zero_sym pred_disj_def sep_add_zero sep_add_zero_sym sep_disj_zero)
lemma sep_coimpl_dne:
"((R \<leadsto>* sep_false) \<leadsto>* sep_false) s \<Longrightarrow> (R \<and>* sep_true) s"
by (metis sep_coimpl_def sep_conj_sep_true_right sep_neg_not)
lemma sep_antimp_contrapos:
" (R) s \<Longrightarrow> ((P \<longrightarrow>* not R) \<leadsto>* (not P)) s "
by (metis pred_neg_def sep_coimpl_def' sep_mp_gen)
lemma sep_snake_trivial:
"(sep_true \<leadsto>* Q) s \<Longrightarrow> Q s"
by (metis pred_neg_def sep_coimpl_def sep_conj_sep_true')
lemma min_predD:
"(R \<leadsto>* \<box>) s \<Longrightarrow> (R \<and>* sep_true) s \<Longrightarrow> R s"
using Sep_Cancel_Set.sep_conj_empty' sep_coimpl_dne sep_snake_mp by blast
lemma septract_sep_wand:
"(P -* R) s \<Longrightarrow> (P \<longrightarrow>* Q) s \<Longrightarrow> (P -* (Q and R)) s"
apply (clarsimp simp: sep_impl_def septraction_def pred_neg_def)
by (fastforce simp: pred_conj_def)
lemma
"(P -* (P \<and>* R)) s \<Longrightarrow> (P \<longrightarrow>* Q) s \<Longrightarrow> (\<And>s. (Q and (P \<and>* R)) s \<Longrightarrow> (P \<leadsto>* R) s) \<Longrightarrow> R s"
using sep_septraction_snake septract_sep_wand by blast
lemma sep_elsewhereD:
"(P -* sep_true) s \<Longrightarrow> (P \<longrightarrow>* (P \<leadsto>* R)) s \<Longrightarrow> R s"
apply (drule (1) septract_sep_wand, simp add: pred_conj_def)
using sep_septraction_snake by blast
lemma sep_conj_coimplI:
"(Q \<leadsto>* R) s \<Longrightarrow> ((P \<and>* Q) \<leadsto>* (P -* R)) s "
by (metis sep_coimpl_def sep_coimpl_def' sep_conj_commuteI sep_mp_frame septraction_def)
lemma sep_conj_septract_curry:
"((P \<and>* Q) -* R) s \<Longrightarrow> (P -* (Q -* R)) s"
by (smt sep_antimp' sep_conj_coimplI sep_septraction_snake)
lemma sep_snake_boxI:
"Q s \<Longrightarrow> (\<box> \<leadsto>* Q) s"
by (simp add: pred_neg_def sep_coimpl_def)
lemma sep_snake_boxD:
"(Q \<leadsto>* \<box>) s \<Longrightarrow> ((Q \<leadsto>* sep_false) or Q) s"
apply (simp only: pred_disj_def)
apply (safe)
using Sep_Cancel_Set.sep_conj_empty' sep_coimpl_cancel by blast
lemma septract_wandD:
"(( R \<longrightarrow>* (not Q)) -* Q) s \<Longrightarrow> (not R) s"
apply (erule sep_septraction_snake)
using sep_antimp_contrapos by blast
lemma sep_impl_septractD:
"(P \<longrightarrow>* Q) s \<Longrightarrow> (R -* (not Q)) s \<Longrightarrow> ((R and not P) -* (not Q)) s"
apply (clarsimp simp: sep_impl_def pred_neg_def septraction_def)
apply (erule_tac x=h' in allE)
apply (clarsimp simp: pred_conj_def)
apply (fastforce)
done
lemma sep_neg_impl:
"(not (R \<longrightarrow>* Q)) = (R -* (not Q)) "
apply (clarsimp simp: pred_neg_def septraction_def)
done
lemma
"P s \<Longrightarrow> (R -* Q) s \<Longrightarrow> ((R and (P -* Q)) -* Q) s"
apply (clarsimp simp: septraction_def sep_impl_def pred_neg_def pred_conj_def)
by (fastforce simp: sep_add_commute sep_disj_commute)
lemma sep_coimpl_notempty:
"(Q \<leadsto>* (not \<box>)) s \<Longrightarrow> (not Q) s"
apply (clarsimp simp: sep_coimpl_def pred_neg_def)
done
method sep_subst uses add = (sep_frule (direct) add)
lemma septract_empty_empty:
"(P -* \<box>) s \<Longrightarrow> \<box> (s :: 'a :: cancellative_sep_algebra)"
apply (clarsimp simp: septraction_def pred_neg_def sep_impl_def sep_empty_def)
done
lemma septract_trivial:
"P s \<Longrightarrow> (sep_true -* P) s"
apply (clarsimp simp: septraction_def pred_neg_def sep_impl_def sep_empty_def)
using sep_disj_zero by fastforce
lemma sep_empty_and_conj:
"\<box> s \<Longrightarrow> (P \<and>* Q) s \<Longrightarrow> P (s :: 'a :: cancellative_sep_algebra)"
by (metis sep_conj_def sep_disj_positive_zero sep_empty_def)
lemma sep_conj_coimpl_mp:
"(P \<and>* R) s \<Longrightarrow> (P \<leadsto>* Q) s \<Longrightarrow> (P \<and>* (Q and R)) s"
apply (drule (2) sep_coimpl_mp_gen, clarsimp simp: pred_conj_def conj_commute)
done
lemma sep_conj_coimpl_contrapos_mp:
"(P \<and>* Q) s \<Longrightarrow> (R \<leadsto>* (not Q)) s \<Longrightarrow> (Q \<and>* (P and (not R))) s"
apply (subst (asm) sep_coimpl_contrapos)
apply (clarsimp simp: pred_neg_def)
apply (sep_drule (direct) sep_conj_coimpl_mp[where P=Q], assumption)
apply (clarsimp simp: pred_conj_def conj_commute)
done
end