-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathQuantitative_Separation_Connectives.thy
1158 lines (939 loc) · 47.3 KB
/
Quantitative_Separation_Connectives.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
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
\<^marker>\<open>creator "Maximilian P. L. Haslbeck"\<close>
\<^marker>\<open>contributor "Christoph Matheja"\<close>
\<^marker>\<open>contributor "Kevin Batz"\<close>
chapter \<open>Quantitative Separating Connectives\<close>
theory Quantitative_Separation_Connectives
imports
"Separation_Algebra.Separation_Algebra" "HOL-Library.Extended_Nat"
"HOL-Library.Extended_Nonnegative_Real"
QSL_Misc
begin
paragraph \<open>Summary\<close>
text \<open>In this theory we introduce the quantitative separating connectives for an arbitrary
separation algebra and an measurement quantale.
We define the quantitative separating conjunction, and magic wand.
Then we prove adjointness of that the operators
We follow the Paper by Batz et al. @{cite batzPOPL19}.
\<close>
term "class.complete_lattice"
subsection \<open>The Locale quant_sep_con\<close>
locale comm_quantale = complete_lattice Inf Sup inf le less sup bot top
+ comm_monoid oper neutr
for Inf :: "'b set \<Rightarrow> 'b" ("\<Sqinter>_" [900] 900)
and Sup ("\<Squnion>_" [900] 900)
and inf
and le (infix "\<le>" 50) and less (infix "<" 50)
and sup bot top
and oper :: "'b \<Rightarrow> 'b \<Rightarrow> 'b" (infixl "\<^bold>*" 70)
and neutr :: "'b" ("\<^bold>1") +
assumes
Sup_mult_left_distrib: "\<And>c A. c \<^bold>* Sup A = Sup (((\<^bold>*) c) ` A)"
begin
lemma mult_bot: "\<And>x. x \<^bold>* bot = bot"
using Sup_mult_left_distrib[where A="{}"] by simp
lemma Sup_mult_right_distrib: "Sup I \<^bold>* c = Sup ((\<lambda>i. i \<^bold>* c) ` I)"
by (auto simp add: commute Sup_mult_left_distrib)
lemma oper_left_mono: "(a::'b) \<le> b \<Longrightarrow> c \<^bold>* a \<le> c \<^bold>* b"
using Sup_mult_left_distrib[where A="{a,b}" and c=c]
by (simp add: sup.absorb_iff2)
lemma oper_right_mono: "\<And>a b c. a \<le> b \<Longrightarrow> a \<^bold>* c \<le> b \<^bold>* c"
using oper_left_mono by (auto simp add: commute)
lemma oper_mono: "\<And>a b c d. a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> a \<^bold>* c \<le> b \<^bold>* d"
apply (erule oper_right_mono [THEN order_trans])
by (erule oper_left_mono)
(* conjecture: there is a Galois Connection *)
lemma "\<exists>f. (\<forall>A B C. (A \<le> (f C) B) \<longleftrightarrow> ((\<^bold>*) C) A \<le> B)"
oops
text \<open>residual\<close>
definition residual where
"residual x z = Sup {y. x \<^bold>* y \<le> z}"
lemma residual_imp: "x \<^bold>* y \<le> z \<Longrightarrow> y \<le> residual x z"
unfolding residual_def
apply(rule Sup_upper) by simp
lemma residual_imp': "y \<le> residual x z \<Longrightarrow> x \<^bold>* y \<le> z"
proof -
assume "y \<le> residual x z"
then have "x \<^bold>* y \<le> x \<^bold>* residual x z" by(rule oper_left_mono)
also have "\<dots> = x \<^bold>* \<Squnion>{y. x \<^bold>* y \<le> z}" unfolding residual_def by simp
also have "\<dots> = \<Squnion>{x \<^bold>* y | y . x \<^bold>* y \<le> z}" apply(subst Sup_mult_left_distrib)
apply(rule arg_cong[where f=Sup]) by auto
also have "\<dots> \<le> \<Squnion>{k | k . k \<le> z}" apply(rule Sup_mono) by auto
also have "\<dots> \<le> z" apply(rule Sup_least) by auto
finally show ?thesis .
qed
lemma residual_adjoint: "x \<^bold>* y \<le> z \<longleftrightarrow> y \<le> residual x z"
using residual_imp residual_imp' by blast
(* indeed :) *)
lemma "\<exists>f. (\<forall>A B C. (A \<le> (f C) B) \<longleftrightarrow> ((\<^bold>*) C) A \<le> B)"
apply(rule exI[where x=residual])
using residual_adjoint by simp
end
locale quant_sep_con = comm_quantale Inf Sup inf le less sup bot top oper neutr
for Inf :: "'b set \<Rightarrow> 'b" ("\<Sqinter>_" [900] 900)
and Sup ("\<Squnion>_" [900] 900)
and inf
and le (infix "\<le>" 50) and less (infix "<" 50)
and sup bot top
and oper :: "'b \<Rightarrow> 'b \<Rightarrow> 'b" (infixl "\<^bold>*" 70)
and neutr :: "'b" ("\<^bold>1") +
fixes
divide :: "'b \<Rightarrow> 'b \<Rightarrow> 'b" (infixl "\<^bold>div" 70)
assumes
\<comment>\<open>Facts about div\<close>
divide_neutral: "\<And>x::'b. x \<^bold>div \<^bold>1 = x" (* maybe \<^bold>\<le> suffices *)
and divide_right_mono_general: "\<And>a b c. a \<le> b \<Longrightarrow> a \<^bold>div c \<le> b \<^bold>div c"
and divide_right_antimono_general: "\<And>a b c. c \<le> b \<Longrightarrow> a \<^bold>div b \<le> a \<^bold>div c"
\<comment> \<open>oper and divide are "adjoint" = The essence of equation 79\<close>
and div_mult_adjoint:
"\<And>A B C :: 'b. \<lbrakk>(bot < C \<or> bot < B ) ; (C < top \<or> B < top) \<rbrakk> \<Longrightarrow> (A \<le> B \<^bold>div C) \<longleftrightarrow> A \<^bold>* C \<le> B"
\<comment> \<open>bot is not neutral\<close>
and bot_not_neutral: "bot < \<^bold>1"
begin
subsection \<open>stuff about complete lattices:\<close>
lemma nn: "(\<not> x < (top)) = (x = top)"
using top.not_eq_extremum by blast
lemma nn_bot: "(\<not> bot < x) = (x = bot)"
using bot.not_eq_extremum by blast
lemma botnottop: "bot \<noteq> top"
using bot_not_neutral by auto
lemma gt_botI: "\<not> a \<le> bot \<Longrightarrow> bot < a"
using local.bot_less by blast
lemma lt_topI: "\<not> e \<le> A \<Longrightarrow> A < top"
using local.top.not_eq_extremum local.top_greatest by blast
lemma le_sideconditions:
fixes a b c :: 'b
shows "((bot < a \<or> bot < b) \<and> (a < top \<or> b < top) \<longrightarrow> a \<le> b) \<longleftrightarrow> (a \<le> b)"
by (auto simp: nn nn_bot mult_bot botnottop intro: gt_botI)
lemma l_Sup_cong: "\<And>S S'. S=S' \<Longrightarrow> Sup S = Sup S'"
by simp
abbreviation SUPR :: "'c set \<Rightarrow>('c \<Rightarrow> 'b) \<Rightarrow> 'b"
where "SUPR A f \<equiv> \<Squnion>(f ` A)"
abbreviation INFI :: "'c set \<Rightarrow>('c \<Rightarrow> 'b) \<Rightarrow> 'b"
where "INFI A f \<equiv> \<Sqinter>(f ` A)"
lemma INF_mono_strong: "(\<And>m. m \<in> B \<Longrightarrow> g m < top \<Longrightarrow> \<exists>n\<in>A. f n \<le> g m) \<Longrightarrow> (INFI A f) \<le> (INFI B g)"
using Inf_mono_strong [of "g ` B" "f ` A"] by auto
lemma SUP_UNION: "(SUPR (\<Union>y\<in>A. g y) (\<lambda>x. f x)) = (SUPR A (\<lambda>y. SUPR (g y) (\<lambda>x. f x )))"
apply (rule antisym)
by (blast intro: SUP_least SUP_upper2)+
lemma SUP_times_distrib2_general:
fixes g :: "_\<Rightarrow>_\<Rightarrow>'b"
shows "SUPR A (\<lambda>(x,y). f x y \<^bold>* g x y) \<le>
SUPR A (\<lambda>(x,y). f x y) \<^bold>* SUPR A (\<lambda>(x,y). g x y)"
by (auto intro!: SUP_least intro: SUP_upper2 oper_mono)
lemma SUP_mult_left_distrib: "\<And>c f. c \<^bold>* SUPR I (\<lambda>i. f i) = SUPR I (\<lambda>i. c \<^bold>* f i)"
by (simp add: image_image Sup_mult_left_distrib)
lemma SUP_mult_right_distrib: "SUPR I (\<lambda>i. f i) \<^bold>* c = SUPR I (\<lambda>i. f i \<^bold>* c)"
by (simp add: image_image Sup_mult_right_distrib)
lemma sup_times_distrib: "(a::'b) \<^bold>* sup b c = sup (a\<^bold>*b) (a\<^bold>*c)"
using Sup_mult_left_distrib[where A="{b,c}"] by simp
subsection \<open>Facts derived from @{thm div_mult_adjoint}}:\<close>
lemma top_divide: "\<And>x. x < top \<Longrightarrow> top \<^bold>div x = top"
using div_mult_adjoint
by (metis local.bot_less local.top_greatest local.top_unique)
lemma divide_bot: "\<And>x::'b. bot < x \<Longrightarrow> x \<^bold>div bot = top"
using div_mult_adjoint
by (metis bot.extremum mult_bot le_less_trans nn top.extremum_unique)
context
assumes "SORT_CONSTRAINT ('a::{sep_algebra})"
begin
subsection \<open>Quantitative Separating Conjunction\<close>
definition
sep_conj_q (infixr "**q" 35)
where
"P **q Q \<equiv> \<lambda>h. Sup { P x \<^bold>* Q y | x y. h=x+y \<and> x ## y}"
lemma sep_conj_q_alt :
"(P **q Q) = (\<lambda>h. SUPR {(x,y). h=x+y \<and> x ## y} (\<lambda>(x,y). P x \<^bold>* Q y))"
unfolding sep_conj_q_def
apply(rule ext) by (auto intro!: l_Sup_cong)
lemma sep_conj_q_SUP:
"(P **q Q) = (\<lambda>h. (SUPR {(x,y)| x y. h=x+y \<and> x ## y} (\<lambda>i. (\<lambda>(x,y). P x \<^bold>* Q y) i)))"
unfolding sep_conj_q_def
apply(rule ext) by (auto intro!: l_Sup_cong)
subsection \<open>Quantitative Separating Implication - Magic Wand\<close>
definition
sep_impl_qq :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b ) \<Rightarrow> 'a \<Rightarrow> 'b" (infixr "-*qq" 35)
where
"P -*qq Q \<equiv> \<lambda>h. INFI { h'. h ## h' \<and> (bot < P h' \<or> bot < Q (h+h') )
\<and> (P h' < top \<or> Q (h+h') < top)}
(\<lambda>h'. (Q (h + h')) \<^bold>div (P h'))"
subsection \<open>Embedding of SL into QSL\<close>
definition emb where "emb P = (\<lambda>h. if P h then \<^bold>1 else bot)"
lemma emb_range: "emb P x \<in> {bot,\<^bold>1}" unfolding emb_def by auto
lemma emb_squared: "emb P x = emb P x \<^bold>* emb P x"
apply (cases "emb P x = bot") using emb_range apply (auto simp: mult_bot) by fastforce
lemma emb_1: "emb P h = \<^bold>1 \<longleftrightarrow> P h"
apply (auto simp: emb_def) using bot_not_neutral by blast
definition sep_empty_q :: "'a \<Rightarrow> 'b" where
"sep_empty_q \<equiv> emb (\<lambda>h. h = 0)"
text \<open>The restricted wand with an predicate in the first component:\<close>
abbreviation sep_impl_q (infixr "-*q" 35) where "(P -*q Q) \<equiv> (emb P -*qq Q)"
lemma sep_impl_q_alt_general:
fixes Q :: "'a \<Rightarrow> 'b"
shows
"inf \<^bold>1 ((P -*q Q) h) = inf \<^bold>1 (INFI { h'. h ## h' \<and> P h'} (\<lambda>h'. Q (h + h')))"
proof -
have T: "{h'. h ## h' \<and> ((bot::'b) < emb P h' \<or> (bot::'b) < Q (h + h'))
\<and> (emb P h' < (top::'b) \<or> Q (h + h') < (top::'b))}
= {h'. h ## h' \<and> (bot::'b) < emb P h' \<and> (emb P h' < (top::'b) \<or> Q (h + h') < top)}
\<union> {h'. h ## h' \<and>(bot::'b) = emb P h' \<and> (bot::'b) < Q (h + h')
\<and> (emb P h' < (top::'b) \<or> Q (h + h') < (top::'b))}"
using bot.not_eq_extremum by fastforce
let ?A = "{h'. h ## h' \<and> Q (h + h') < top \<and> P h'}"
let ?B = "{h'. h ## h' \<and> (bot::'b) < emb P h' \<and> (emb P h' < (top::'b) \<or> Q (h + h') < (top::'b))}"
have AB: "?A \<subseteq> ?B" by (auto simp: emb_def bot_not_neutral)
have KK: "\<^bold>1 \<le> (INFI (?B-?A) (\<lambda>h'. Q (h + h') \<^bold>div emb P h'))"
by(auto simp: le_Inf_iff emb_def divide_neutral intro: lt_topI)
have 1: "inf \<^bold>1 (INFI ?B (\<lambda>h'. Q (h + h') \<^bold>div emb P h'))
= inf \<^bold>1 (INFI ?A (\<lambda>x. Q (h + x)))"
proof -
have B_decompose: "?B = (?B - ?A) \<union> (?A)" using AB by blast
have i: "(INFI ?A (\<lambda>h'. Q (h + h') \<^bold>div emb P h')) = (INFI ?A (\<lambda>h'. Q (h + h')))"
by (auto simp: emb_def divide_neutral)
have ii: "inf \<^bold>1 (INFI (?B-?A) (\<lambda>h'. Q (h + h') \<^bold>div emb P h')) = \<^bold>1"
using KK by (auto intro: antisym)
have "(INFI (?B) (\<lambda>h'. Q (h + h') \<^bold>div emb P h'))
= inf (INFI (?B - ?A) (\<lambda>h'. Q (h + h') \<^bold>div emb P h'))
(INFI (?A) (\<lambda>h'. Q (h + h') \<^bold>div emb P h'))"
apply(subst B_decompose) by(rule INF_union)
also have "\<dots> = inf (INFI (?B - ?A) (\<lambda>h'. Q (h + h') \<^bold>div emb P h'))
(INFI (?A) (\<lambda>h'. Q (h + h')))"
unfolding i by simp
finally
have iii: "(INFI (?B) (\<lambda>h'. Q (h + h') \<^bold>div emb P h'))
= inf (INFI (?B - ?A) (\<lambda>h'. Q (h + h') \<^bold>div emb P h')) (INFI (?A) (\<lambda>h'. Q (h + h')))" .
have "inf \<^bold>1 (INFI (?B) (\<lambda>h'. Q (h + h') \<^bold>div emb P h'))
= inf \<^bold>1 (inf (INFI (?B-?A) (\<lambda>h'. Q (h + h') \<^bold>div emb P h'))
(INFI (?A) (\<lambda>h'. Q (h + h'))))"
unfolding iii by simp
also have "\<dots> = inf (inf \<^bold>1 (INFI (?B-?A) (\<lambda>h'. Q (h+h') \<^bold>div emb P h')))
(INFI ?A (\<lambda>h'. Q (h+h')))"
by(simp add: inf.assoc)
also have "\<dots> = inf \<^bold>1 (INFI (?A) (\<lambda>h'. Q (h + h')))"
unfolding ii by simp
finally show ?thesis .
qed
have "(\<exists>h'. h ## h' \<and> (bot::'b) < top \<and> Q (h + h') < top \<and> P h')
\<Longrightarrow> (INFI { h'. h ## h' \<and> P h'} (\<lambda>h'. Q (h + h'))) < top"
apply safe subgoal for h'
apply(rule order.strict_trans1)
apply(rule INF_lower[where i=h']) by auto
done
have "~(\<exists>h'. h ## h' \<and> (bot::'b) < top \<and> Q (h + h') < top \<and> P h')
\<Longrightarrow> (INFI { h'. h ## h' \<and> P h'} (\<lambda>h'. Q (h + h'))) = top"
apply auto
by (metis Inf_UNIV Inf_top_conv(2) UNIV_I top.not_eq_extremum)
have 2: "(INFI {h'. h ## h' \<and> (bot::'b) = emb P h' \<and> (bot::'b) < Q (h + h')
\<and> (emb P h' < (top::'b) \<or> Q (h + h') < (top::'b))}
(\<lambda>h'. Q (h + h') \<^bold>div emb P h'))
= top"
by (simp_all add: divide_bot)
have F: "{ h'. h ## h' \<and> P h'} = { h'. h ## h' \<and> P h' \<and> Q (h + h') = top}
\<union> { h'. h ## h' \<and> P h' \<and> Q (h + h') < top}"
using top.not_eq_extremum by blast
have 3: "(INFI {h'. h ## h' \<and> P h' \<and> Q (h + h') = top} (\<lambda>h'. Q (h + h'))) = top"
by auto
have "inf \<^bold>1 ((P -*q Q) h)
= inf \<^bold>1 (inf (INFI {h'. h ## h' \<and> (bot::'b) < emb P h'
\<and> (emb P h' < (top::'b) \<or> Q (h + h') < (top::'b))}
(\<lambda>h'. Q (h + h') \<^bold>div emb P h'))
(INFI {h'. h ## h' \<and> (bot::'b) = emb P h'\<and> (bot::'b) < Q (h + h')
\<and> (emb P h' < (top::'b) \<or> Q (h + h') < (top::'b))}
(\<lambda>h'. Q (h + h') \<^bold>div emb P h')))"
unfolding sep_impl_qq_def T INF_union
by simp
also have "\<dots> = inf \<^bold>1 (inf (INFI {h'. h ## h' \<and> (bot::'b) < emb P h'
\<and> (emb P h' < (top::'b) \<or> Q (h + h') < (top::'b))}
(\<lambda>h'. Q (h + h') \<^bold>div emb P h'))
top)"
unfolding 2 by simp
also have "\<dots> = inf \<^bold>1 (INFI {h'. h ## h' \<and> (bot::'b) < emb P h'
\<and> (emb P h' < (top::'b) \<or> Q (h + h') < (top::'b))}
(\<lambda>h'. Q (h + h') \<^bold>div emb P h'))"
by simp
also have "\<dots> = inf \<^bold>1 (INFI {h'. h ## h' \<and> Q (h + h') < top \<and> P h'} (\<lambda>x. Q (h + x)))"
unfolding 1 by simp
also have "\<dots> = inf \<^bold>1 ( INFI { h'. h ## h' \<and> P h'} (\<lambda>h'. Q (h + h')))"
unfolding F INF_union 3
apply(rule arg_cong[where f="\<lambda>x. inf \<^bold>1 x"])
by (auto intro: INF_cong)
finally show "inf \<^bold>1 ((P -*q Q) h) = inf \<^bold>1 (INFI {h'. h ## h' \<and> P h'} (\<lambda>h'. Q (h + h')))" .
qed
lemma sep_impl_q_alt_general':
fixes Q :: "'a \<Rightarrow> 'b"
assumes "\<^bold>1 = top"
shows
"((P -*q Q) h) = (INFI { h'. h ## h' \<and> P h'} (\<lambda>h'. Q (h + h')))"
using assms sep_impl_q_alt_general by simp
subsubsection \<open>Conservativity of QSL as an assertion language\<close>
lemma Sup_zeroone: "P \<subseteq> {bot,\<^bold>1} \<Longrightarrow> Sup P \<in> {bot,\<^bold>1}"
proof -
assume " P \<subseteq> {bot,\<^bold>1}"
then consider "P = {}" | "P={bot}" | "P={\<^bold>1}" | "P={bot,\<^bold>1}" by auto
then show ?thesis apply(cases)
by auto
qed
lemma sep_conj_q_range: "((emb P) **q (emb Q)) h \<in> {bot,\<^bold>1}"
unfolding sep_conj_q_def
apply(rule Sup_zeroone)
apply (auto simp: emb_def) using divide_neutral divide_bot mult_bot by auto
lemma Inf_zeroone: "P \<noteq> {} \<Longrightarrow> P \<subseteq> {bot,\<^bold>1} \<Longrightarrow> Inf P \<in> {bot,\<^bold>1}"
proof -
assume "P \<noteq> {}" " P \<subseteq> {bot,\<^bold>1}"
then consider "P={bot}" | "P={\<^bold>1}" | "P={bot,\<^bold>1}" by auto
then show ?thesis apply(cases)
by auto
qed
lemma Inf_zeroonetop: " P \<subseteq> {bot,\<^bold>1,top} \<Longrightarrow> Inf P \<in> {bot,\<^bold>1,top}"
by (smt insertI2 insert_Diff insert_absorb2 insert_commute insert_not_empty
local.Inf_insert local.Inf_lower local.ccInf_empty local.inf_top.right_neutral
local.le_bot singleton_insert_inj_eq' subset_antisym subset_insert_iff)
(*
lemma Inf_zeroonetop: "P \<subseteq> {bot,\<^bold>1,top} \<Longrightarrow> Inf P \<in> {bot,\<^bold>1,top}"
proof -
assume " P \<subseteq> {bot,\<^bold>1,top}"
then consider "P = {}"
| "P={bot}" | "P={\<^bold>1}" | "P={top}"
| "P={bot,\<^bold>1}" | "P={bot,top}" | "P={top,\<^bold>1}"
| "P={bot,\<^bold>1,top}" by auto
then show ?thesis apply(cases)
by auto
qed *)
lemma sep_conj_q_leq1: "((emb P) **q (emb Q)) h \<le> \<^bold>1"
using sep_conj_q_range[of P Q h] by auto
lemma emb_not_bot: "bot < emb P h \<longleftrightarrow> emb P h = \<^bold>1"
using bot_not_neutral by (auto simp: emb_def)
lemma emb_not_bot2: "bot \<noteq> emb P h \<longleftrightarrow> emb P h = \<^bold>1"
"emb P h \<noteq> bot \<longleftrightarrow> emb P h = \<^bold>1"
using bot_not_neutral by (auto simp: emb_def)
lemma sep_impl_q_rangezeroonetop: "((P -*q (emb Q)) h) \<in> {bot,\<^bold>1,top}"
unfolding sep_impl_qq_def
apply(rule Inf_zeroonetop)
subgoal apply (auto simp: emb_not_bot emb_not_bot2 divide_neutral )
apply(auto simp: emb_def divide_neutral divide_bot bot_not_neutral)
done
done
lemma inf_1_cuts: "a \<in> {bot, \<^bold>1, top} \<Longrightarrow> inf \<^bold>1 a \<in> {bot, \<^bold>1}"
proof -
assume "a \<in> {bot, \<^bold>1, top}"
then have "inf \<^bold>1 a \<in> { \<^bold>1, bot}"
using inf_bot_right inf_idem inf_top_right by blast
then show ?thesis
using bot_ennreal by auto
qed
lemma sep_impl_q_range: "inf \<^bold>1 ((P -*q (emb Q)) h) \<in> {bot, \<^bold>1}"
apply(rule inf_1_cuts) by(rule sep_impl_q_rangezeroonetop)
lemma quant_wand_conservative:
fixes P :: "'a \<Rightarrow> bool"
shows "(P \<longrightarrow>* Q) h \<longleftrightarrow> inf \<^bold>1 (((emb P) -*qq (emb Q)) h) = \<^bold>1"
proof -
(* rather ugly proof, DB's fault ;) *)
fix h
have " ((inf \<^bold>1 ((P -*q (emb Q)) h)) = \<^bold>1)
\<longleftrightarrow> ((inf \<^bold>1 ((INFI {h'. h ## h' \<and> P h'} (\<lambda>h'. emb Q (h + h'))))) = \<^bold>1)"
unfolding sep_impl_q_alt_general by simp
also have "\<dots> \<longleftrightarrow> (\<forall>h'. h ## h' \<and> P h' \<longrightarrow> Q (h + h'))"
apply(rule iffI)
subgoal
apply(cases "{h'. h ## h' \<and> P h'} = {}")
subgoal by auto
subgoal proof (safe, goal_cases)
case (1 h' x)
from 1(2-4) have "inf \<^bold>1 (INFI {h'. h ## h' \<and> P h'} (\<lambda>h'. emb Q (h + h'))) \<le> bot"
apply(intro le_infI2)
apply(intro INF_lower2[where i=h']) by (auto simp: emb_def)
then show ?case using 1(1) bot_not_neutral by auto
qed
done
subgoal
by(auto simp add: emb_def INF_constant cong: INF_cong_simp )
done
also have "\<dots> \<longleftrightarrow> (P \<longrightarrow>* Q) h" unfolding sep_impl_def by auto
finally show "(P \<longrightarrow>* Q) h \<longleftrightarrow> inf \<^bold>1 ((P -*q (emb Q)) h) = \<^bold>1" by simp
qed
lemma quant_wand_conservative':
fixes P :: "'a \<Rightarrow> bool"
assumes "\<^bold>1 = top"
shows "(P \<longrightarrow>* Q) h \<longleftrightarrow> (((emb P) -*qq (emb Q)) h) = \<^bold>1"
using assms quant_wand_conservative by simp
lemma quant_star_conservative:
fixes P :: "'a \<Rightarrow> bool"
shows "(P ** Q) h \<longleftrightarrow> ((emb P) **q (emb Q)) h = \<^bold>1"
proof -
have "(P ** Q) h = (\<exists>xa y. xa ## y \<and> h = xa + y \<and> emb P xa = \<^bold>1 \<and> emb Q y = \<^bold>1)"
unfolding sep_conj_def emb_1 by auto
also have "\<dots> = (Sup { emb P x \<^bold>* emb Q y | x y. h=x+y \<and> x ## y} = \<^bold>1)"
apply rule
subgoal
apply(rule antisym)
subgoal apply(subst sep_conj_q_leq1[unfolded sep_conj_q_def] ) by simp
subgoal apply(rule Sup_upper) by force
done
subgoal
proof (rule ccontr, goal_cases)
case 1
from 1(2) have "\<And>x y. (x,y) \<in> {(x,y) | x y. h = x + y \<and> x ## y}
\<Longrightarrow> emb P x \<^bold>* emb Q y = bot"
by (auto simp: emb_def split: if_splits simp: mult_bot)
then have "Sup {emb P x \<^bold>* emb Q y |x y. h = x + y \<and> x ## y} \<le> bot"
by (auto intro: Sup_least)
with 1(1) show "False" using bot_not_neutral by simp
qed
done
also have "\<dots> = (((emb P) **q (emb Q)) h = \<^bold>1)" unfolding sep_conj_q_def by simp
finally show ?thesis .
qed
subsection \<open>Properties of Quantitative Separating Connectives\<close>
subsubsection \<open>Commutative monoid\<close>
lemma SUP_UNION_my: "(SUPR A (\<lambda>y. SUPR (g y) (\<lambda>x. f y x ))) = (SUPR (\<Union>y\<in>A. Pair y ` g y) (\<lambda>xy. f (fst xy) (snd xy)))"
apply (rule antisym)
subgoal
apply(rule SUP_least)
apply(rule SUP_least)
subgoal for x y
apply(rule SUP_upper2[where i="(x,y)"]) by auto
done
subgoal
apply(rule SUP_least)
apply auto subgoal for x y
apply(rule SUP_upper2[where i=x]) apply simp
apply(rule SUP_upper2[where i=y]) by auto
done
done
lemma pp: "(\<And>x. gg (g x) = x) \<Longrightarrow> SUPR S f = SUPR (g ` S) (f o gg)"
by (simp add: image_image)
lemma star_assoc:
fixes x y z :: "'a \<Rightarrow> 'b"
shows "(x **q (y **q z)) = ((x **q y) **q z) "
proof (rule ext)
fix h
have "(x **q (y **q z)) h
= (SUPR {(x, y) |x y. h = x + y \<and> x ## y} (\<lambda> (xa, ya).
x xa \<^bold>* (SUPR {(x, y) |x y. ya = x + y \<and> x ## y} (\<lambda> (x, ya). y x \<^bold>* z ya))))"
unfolding sep_conj_q_SUP by auto
also have "\<dots> = (SUPR {(x, y). h = x + y \<and> x ## y} (\<lambda>xa.
case xa of (xa, ya) \<Rightarrow> SUPR {(x, y). ya = x + y \<and> x ## y} (\<lambda>i.
(case i of (h21, h22) \<Rightarrow> x xa \<^bold>* y h21 \<^bold>* z h22))))"
by(simp add: SUP_mult_left_distrib prod.case_distrib assoc)
also have "\<dots> = (SUPR {(x, y). h = x + y \<and> x ## y} (\<lambda>xa.
SUPR {((fst xa),x, y)| x y . snd xa = x + y \<and> x ## y}
(\<lambda>i. (case i of (b, h21, h22) \<Rightarrow> x b \<^bold>* y h21 \<^bold>* z h22))))"
by(force intro!: arg_cong[where f=Sup])
also have "\<dots> = (SUPR {(h1, h2, h3). h = h1 + h2 + h3 \<and> h1 ## h2 + h3
\<and> h1 ## h2 \<and> h1 ## h3 \<and> h3 ## h2 }
(\<lambda>xa. case xa of (h1, h2, h3) \<Rightarrow> x h1 \<^bold>* y h2 \<^bold>* z h3))"
apply(subst SUP_UNION[symmetric])
apply(rule SUP_cong)
subgoal
apply safe
subgoal by (metis fstI sep_add_assoc sep_disj_addD1 sep_disj_addD2 sndI)
by (auto simp: sep_add_ac dest: sep_disj_addD)
subgoal by auto
done
also have "\<dots> = (SUPR {(x, y). h = x + y \<and> x ## y}
(\<lambda>xa. SUPR {(h1,h2,snd xa)| h1 h2. fst xa = h1 + h2 \<and> h1 ## h2}
(\<lambda>i. (case i of (h1, h2, h3) \<Rightarrow> x h1 \<^bold>* y h2 \<^bold>* z h3))))"
apply(subst SUP_UNION[symmetric])
apply(rule SUP_cong)
subgoal
by (auto simp: sep_add_ac dest: sep_disj_addD
intro: sep_disj_addI1 sep_disj_addI3 sep_disj_commuteI )
subgoal
by auto
done
also have "\<dots> = (SUPR {(h12, h3). h = h12 + h3 \<and> h12 ## h3} (\<lambda>xa.
case xa of (h12,h3) \<Rightarrow> SUPR {(x, y). h12 = x+y \<and> x ## y}
(\<lambda>h12. (case h12 of (h1, h2) \<Rightarrow> (x h1 \<^bold>* y h2 \<^bold>* z h3)))))"
apply(rule SUP_cong)
apply simp
apply safe
apply(rule l_Sup_cong) by force
also have "\<dots> = ((x **q y) **q z) h"
unfolding sep_conj_q_SUP apply(auto simp: SUP_mult_right_distrib)
apply(rule SUP_cong)
apply simp
apply safe
apply(rule SUP_cong) by (auto simp: mult.assoc)
finally show "(x **q (y **q z)) h = ((x **q y) **q z) h " .
qed
lemma star_comm:
fixes X Y :: "_ \<Rightarrow> 'b"
shows "(X **q Y) = (Y **q X)"
unfolding sep_conj_q_SUP
apply(rule ext)
apply(rule l_Sup_cong)
by (auto simp add: commute sep_add_ac)
lemma emp_neutral1:
"(X **q sep_empty_q) = X"
unfolding sep_conj_q_def sep_empty_q_def emb_def
apply(rule ext)
apply(rule antisym)
subgoal
by (auto intro!: Sup_least simp: mult_bot)
subgoal
by (auto intro: Sup_upper)
done
lemma emp_neutral2 :
"(sep_empty_q **q X) = X"
by (simp add: star_comm emp_neutral1)
lemmas emp_neutral = emp_neutral1 emp_neutral2
lemma sep_conj_q_left_commute:
fixes P Q R :: "'a \<Rightarrow> 'b"
shows "(P **q Q **q R) = (Q **q P **q R)"
apply(subst star_assoc)
apply(subst star_comm)
apply(subst star_assoc) by simp
lemmas sep_conj_q_c = star_comm sep_conj_q_left_commute
subsubsection \<open>(Sub)distributivity Laws\<close>
abbreviation "fsup Q R \<equiv> (\<lambda>x. sup (Q x) (R x))"
lemma theorem_3_6_general1:
fixes
P :: "'a \<Rightarrow> 'b"
shows
"(P **q (fsup Q R)) = fsup (P **q Q) (P **q R)"
proof
fix h
have "(P **q (fsup Q R)) h = Sup {P x \<^bold>* fsup Q R y |x y. h = x + y \<and> x ## y}"
unfolding sep_conj_q_def by simp
also have "\<dots> = Sup { sup (P x \<^bold>* Q y) (P x \<^bold>* R y) |x y. h = x + y \<and> x ## y}"
apply(subst sup_times_distrib) by simp
also have "\<dots> = (SUPR {(x, y). h = x + y \<and> x ## y} (\<lambda>x. case x of (x,y) \<Rightarrow> sup (P x \<^bold>* Q y) (P x \<^bold>* R y)))"
apply (rule arg_cong[where f=Sup]) by auto
also have "\<dots> = (SUPR {(x, y). h = x + y \<and> x ## y} (\<lambda>x. sup (P (fst x) \<^bold>* Q (snd x)) (P (fst x) \<^bold>* R (snd x))))"
apply (rule arg_cong[where f=Sup])
by (meson prod.case_eq_if)
also have "\<dots> = sup (SUPR {(x, y). h = x + y \<and> x ## y} (\<lambda>x. P (fst x) \<^bold>* Q (snd x)))
(SUPR {(x, y). h = x + y \<and> x ## y} (\<lambda>x. P (fst x) \<^bold>* R (snd x)))"
apply(subst SUP_sup_distrib[symmetric]) ..
also have "\<dots> = fsup (P **q Q) (P **q R) h"
unfolding sep_conj_q_alt apply simp
by (metis (mono_tags, lifting) SUP_cong prod.case_eq_if)
finally show "(P **q fsup Q R) h = fsup (P **q Q) (P **q R) h " .
qed
lemma theorem_3_6_general3:
fixes
Q :: "_ \<Rightarrow> 'b"
shows
"( (emb \<phi>) **q (\<lambda>h. Q h \<^bold>* R h)) h \<le> ((emb \<phi>) **q Q) h \<^bold>* ((emb \<phi>) **q R) h"
proof -
have "( (emb \<phi>) **q (\<lambda>h. Q h \<^bold>* R h)) h = (SUPR {(h1, h2). h = h1 + h2 \<and> h1 ## h2} (\<lambda> (h1, h2). emb \<phi> h1 \<^bold>* (\<lambda>h. Q h \<^bold>* R h) h2))"
unfolding sep_conj_q_alt by simp
also have "... = (SUPR {(h1, h2). h = h1 + h2 \<and> h1 ## h2} (\<lambda>(h1, h2). emb \<phi> h1 \<^bold>* Q h2 \<^bold>* R h2))" apply (rule SUP_cong)
by (auto simp: assoc)
also have "... = (SUPR {(h1, h2). h = h1 + h2 \<and> h1 ## h2} (\<lambda>(h1, h2). (emb \<phi> h1 \<^bold>* Q h2) \<^bold>* ( emb \<phi> h1 \<^bold>* R h2)))"
apply (subst (1) emb_squared)
by (simp add: ac_simps)
also have "... \<le> (SUPR {(h1, h2). h = h1 + h2 \<and> h1 ## h2} (\<lambda>(h1, h2). (emb \<phi> h1 \<^bold>* Q h2)))
\<^bold>* (SUPR {(h1, h2). h = h1 + h2 \<and> h1 ## h2} (\<lambda>(h1, h2). ( emb \<phi> h1 \<^bold>* R h2)))"
by (rule SUP_times_distrib2_general)
also have "... = ((emb \<phi>) **q Q) h \<^bold>* ((emb \<phi>) **q R) h"
by (simp add: local.sep_conj_q_alt)
finally show "( (emb \<phi>) **q (\<lambda>h. Q h \<^bold>* R h)) h \<le> ((emb \<phi>) **q Q) h \<^bold>* ((emb \<phi>) **q R) h".
qed
lemma theorem_3_6:
fixes
Q :: "'a \<Rightarrow> 'b"
shows
"(P **q (fsup Q R)) = fsup (P **q Q) (P **q R)"
"( (emb \<phi>) **q (\<lambda>h. Q h \<^bold>* R h)) h \<le> ((emb \<phi>) **q Q) h \<^bold>* ((emb \<phi>) **q R) h"
using theorem_3_6_general1 theorem_3_6_general3 by auto
subsubsection \<open>Or\<close>
lemma emb_or: "emb (X or Y) = (fsup (emb X) (emb Y))"
unfolding emb_def by auto
subsubsection \<open>monotonicity of @{term "(**q)"}\<close>
text \<open>theorem 3.7\<close>
lemma sep_conj_q_mono:
fixes X X' :: "_ \<Rightarrow> 'b"
shows
"(\<And>x. X x \<le> X' x) \<Longrightarrow> (\<And>y. Y y \<le> Y' y) \<Longrightarrow> (X **q Y) h \<le> (X' **q Y') h"
by (force intro: le_funI SUP_mono simp add: sep_conj_q_alt oper_mono le_funD)
lemma sep_conj_q_right_mono:
fixes P :: "_ \<Rightarrow> 'b"
assumes P: "\<And>h. P h \<le> I h"
shows "(P **q R) h \<le> (I **q R) h"
using sep_conj_q_mono assms by blast
lemma sep_conj_q_left_mono:
fixes P :: "_ \<Rightarrow> 'b"
assumes P: "\<And>h. P h \<le> I h"
shows "(P **q R) h \<le> (I **q R) h"
using sep_conj_q_mono assms by blast
subsubsection \<open>monotonicity of @{term "(-*qq)"}\<close>
lemma sep_impl_q_left_mono:
fixes P :: "_\<Rightarrow>'b"
shows "(\<And>y. Y y \<le> Y' y) \<Longrightarrow> (P -*qq Y) h \<le> (P -*qq Y') h"
unfolding sep_impl_qq_def
apply(rule INF_mono_strong)
subgoal for h'
apply(rule bexI[where x=h'])
subgoal by (auto intro!: divide_right_mono_general)
subgoal using local.less_le_not_le local.top.not_eq_extremum divide_bot local.bot_less
by (force intro!: divide_right_mono_general)
done
done
lemma sep_impl_q_left_mono':
fixes P :: "_\<Rightarrow>'b"
shows "(\<And>y. Y y \<le> Y' y) \<Longrightarrow> (P -*qq Y) h \<le> (P -*qq Y') h"
using sep_impl_q_left_mono by blast
lemma ennreal_inverse_antimono:
"(a::ennreal) \<le> b \<Longrightarrow> inverse b \<le> inverse a"
apply(cases a; cases b; cases "a=0"; cases "b=0")
apply simp_all
apply(simp add: inverse_ennreal)
using ennreal_neq_top top.extremum_uniqueI
by (simp add: le_ennreal_iff)
lemma sep_impl_q_right_antimono:
shows "(\<And>h. P' h \<le> P h) \<Longrightarrow> (P -*qq Y) h \<le> (P' -*qq Y) h"
unfolding sep_impl_qq_def
apply(rule INF_mono_strong)
subgoal for h'
apply(rule bexI[where x=h'])
by (auto intro!: divide_right_antimono_general simp: nn top_divide local.less_le_trans )
done
lemma sep_impl_q_mono:
shows "(\<And>x. P' x \<le> P x) \<Longrightarrow> (\<And>x. Y x \<le> Y' x) \<Longrightarrow> (P -*qq Y) h \<le> (P' -*qq Y') h"
apply(rule order.trans)
apply(rule sep_impl_q_left_mono[where Y'=Y']) apply simp
apply(rule sep_impl_q_right_antimono) by simp
subsubsection \<open>adjointness of star and magicwand\<close>
text \<open>theorem 3.9\<close>
lemma adjoint_general:
shows "(\<forall>h. (X **q P) h \<le> Y h) \<longleftrightarrow> (\<forall>h. X h \<le> (P -*qq Y) h)"
proof -
(* side condition *)
let ?sc = "\<lambda>a b. (bot < a \<or> bot < b ) \<and> (a < top \<or> b < top)"
have le_mult_sc: "\<And>a b c. (?sc a b \<longrightarrow> c \<^bold>* a \<le> b) \<longleftrightarrow> (c \<^bold>* a \<le> b)"
by (auto simp: nn nn_bot mult_bot botnottop intro: gt_botI)
have "(\<forall> h. X h \<le> (P -*qq Y) h)
\<longleftrightarrow> (\<forall>h. X h \<le> (INFI {h'. h ## h' \<and> ?sc (P h') (Y (h+h')) } (\<lambda>h'. Y (h + h') \<^bold>div P h')))"
unfolding sep_impl_qq_def by simp
also have "... \<longleftrightarrow> (\<forall>h h'. h ## h' \<longrightarrow> ?sc (P h') (Y (h+h')) \<longrightarrow> X h \<le> Y (h + h') \<^bold>div P h')"
by (auto simp: le_INF_iff)
also have "... \<longleftrightarrow> (\<forall>h h'. h ## h' \<longrightarrow> ?sc (P h') (Y (h+h')) \<longrightarrow> X h \<^bold>* P h' \<le> Y (h + h'))"
using div_mult_adjoint by auto
also have "... \<longleftrightarrow> (\<forall>a b. a ## b \<longrightarrow> X a \<^bold>* P b \<le> Y (a + b))"
by(auto simp: le_mult_sc)
also have "... \<longleftrightarrow> (\<forall>h. ((\<lambda>h. SUPR {(x, y). h = x + y \<and> x ## y} (\<lambda> (x, y). X x \<^bold>* P y)) h \<le> Y h))"
by (simp add: SUP_le_iff)
also have "... \<longleftrightarrow> (\<forall>h. (X **q P) h \<le> Y h)"
unfolding sep_conj_q_alt by simp
finally show ?thesis by simp
qed
lemma adjoint: "(\<forall>h. (X **q (emb P)) h \<le> Y h) \<longleftrightarrow> (\<forall>h. X h \<le> (P -*q Y) h)"
using adjoint_general by blast
subsubsection \<open>quantitative modus ponens\<close>
text \<open>theorem 3.8\<close>
lemma quant_modus_ponens:
"( (emb P) **q (P -*q X)) h \<le> X h"
proof -
have " (P -*q X) h \<le> (P -*q X) h" by simp
then have "(((P -*q X) **q emb P) h \<le> X h)"
using adjoint[symmetric, where X="(P -*q X)" and Y=X] by auto
then show ?thesis apply(subst star_comm) .
qed
lemma quant_modus_ponens_general:
shows "( P **q (P -*qq X)) h \<le> X h"
proof -
have " (P -*qq X) h \<le> (P -*qq X) h" by simp
then have "(((P -*qq X) **q P) h \<le> X h)"
using adjoint_general[symmetric, where X="(P -*qq X)" and Y=X] by auto
then show ?thesis apply(subst star_comm) .
qed
subsection \<open>Intuitionistic Expectations\<close>
text \<open>In SL, a predicate @{term \<phi>} is called @{term intuitionistic}, iff for all @{term h} and
@{term h'} with @{term "h \<preceq> h'"} , @{term "\<phi> h"} implies @{term "\<phi> h'"}.\<close>
term "intuitionistic"
term "sep_true"
definition intuitionistic_q :: "('a \<Rightarrow> 'b) \<Rightarrow> bool" where
"intuitionistic_q P = (\<forall>h h'. h \<preceq> h' \<longrightarrow> P h \<le> P h')"
lemma intuitionistic_q_emb_intuitionistic_iff:
"intuitionistic_q (emb P) \<longleftrightarrow> intuitionistic P"
unfolding intuitionistic_q_def intuitionistic_def emb_def
using bot_not_neutral less_le_not_le by fastforce
lemma intuitionistic_qI:
"(\<And>h h'. h \<preceq> h' \<Longrightarrow> P h \<le> P h') \<Longrightarrow> intuitionistic_q P"
by (unfold intuitionistic_q_def, fast)
lemma intuitionistic_qI2:
"(\<And>h h'. h ## h' \<Longrightarrow> P h \<le> P (h + h')) \<Longrightarrow> intuitionistic_q P"
apply (unfold intuitionistic_q_def sep_substate_def)
by auto
lemma intuitionistic_qD:
"intuitionistic_q X \<Longrightarrow> h ## z \<Longrightarrow> h' = h + z \<Longrightarrow> X h \<le> X h' "
by (unfold intuitionistic_q_def sep_substate_def, auto)
lemma intuitionistic_q_is_attained_at_h:
fixes
X :: "_ \<Rightarrow> 'b"
assumes "intuitionistic_q X"
shows "(SUPR {(x, y) |x y. h = x + y \<and> x ## y} (\<lambda>(h1, h2). X h1)) = X h"
apply(rule antisym)
subgoal
apply(rule SUP_least) using assms by(auto dest: intuitionistic_qD)
subgoal
apply(rule SUP_upper2[where i="(h,0)"]) by auto
done
text \<open>Tightest intuitionistic expectations\<close>
abbreviation sep_true_q ("1\<^sub>q") where "1\<^sub>q \<equiv> (emb sep_true)"
theorem tightest_intuitionistic_expectations_star:
fixes X :: "'a \<Rightarrow> 'b"
shows
"intuitionistic_q (X **q 1\<^sub>q)"
"\<And>h. X h \<le> (X **q 1\<^sub>q) h"
"\<And>X' h. intuitionistic_q X' \<Longrightarrow> (\<And>h. X h \<le> X' h) \<Longrightarrow> (X **q 1\<^sub>q) h \<le> X' h"
proof -
show "intuitionistic_q (X **q 1\<^sub>q)"
proof (rule intuitionistic_qI2)
fix h h' :: 'a
assume *: "h ## h'"
have "(X **q 1\<^sub>q) h = (SUPR {(x, y). h = x + y \<and> x ## y} (\<lambda>(h1, h2). X h1 \<^bold>* 1\<^sub>q h2))"
unfolding sep_conj_q_alt by simp
also have "\<dots> = (SUPR {(x, y). h = x + y \<and> x ## y} (\<lambda>(h1, h2). X h1 \<^bold>* 1\<^sub>q (h2+h')))"
by (auto simp: emb_def)
also have "\<dots> \<le> (SUPR {(x, y). h + h' = x + y \<and> x ## y} (\<lambda>(h1, h2). X h1 \<^bold>* 1\<^sub>q h2))"
apply(rule SUP_mono) apply safe
subgoal for h1 h2 apply(rule bexI[where x="(h1,h2 + h')"])
using * by (auto simp: sep_add_assoc dest: sep_add_disjD intro: sep_disj_addI3)
done
also have "\<dots> = (X **q 1\<^sub>q) (h + h')"
unfolding sep_conj_q_alt by simp
finally show "(X **q 1\<^sub>q) h \<le> (X **q 1\<^sub>q) (h + h')" .
qed
next
fix h
have "X h \<le> (SUPR {(x, y) |x y. h = x + y \<and> x ## y} (\<lambda> (x, y). X x \<^bold>* emb (\<lambda>s. True) y))"
by (rule Sup_upper) (auto intro!: image_eqI[where x="(h,0)"] simp: emb_def)
also have "\<dots> = (X **q 1\<^sub>q) h"
unfolding sep_conj_q_SUP by simp
finally show "X h \<le> (X **q 1\<^sub>q) h" .
next
fix X'
assume "intuitionistic_q X'" and Xmono: "\<And>h. X h \<le> X' h"
fix h
have "(X **q 1\<^sub>q) h \<le> (X' **q 1\<^sub>q) h"
using sep_conj_q_mono[OF Xmono] by fast
also have "\<dots> = (SUPR {(x, y) |x y. h = x + y \<and> x ## y} (\<lambda>(x, y). X' x \<^bold>* 1\<^sub>q y))"
unfolding sep_conj_q_SUP by simp
also have "\<dots> = (SUPR {(x, y) |x y. h = x + y \<and> x ## y} (\<lambda>(x, y). X' x))"
by (auto simp add: emb_def)
also have "\<dots> = X' h"
apply(rule intuitionistic_q_is_attained_at_h) by fact
finally show "(X **q 1\<^sub>q) h \<le> X' h" .
qed
lemma intuitionistic_q_is_attained_at_h_wand:
fixes
X :: "_ \<Rightarrow> 'b"
assumes "intuitionistic_q X"
shows "X h = (INFI {h'. h ## h' \<and> (\<^bold>1 < top \<or> X (h + h') < top) } (\<lambda>h'. X (h + h')) )"
apply(rule antisym)
subgoal
apply(rule Inf_greatest) using assms by(auto dest: intuitionistic_qD)
subgoal
apply(cases "X h<top")
subgoal apply(rule INF_lower2[where i=0]) by auto
subgoal by(auto simp: nn)
done
done
lemma tightest_intuitionistic_expectations_wand_general:
fixes X :: "'a \<Rightarrow> 'b"
shows
"intuitionistic_q (1\<^sub>q -*qq X)"
"\<And>h. (1\<^sub>q -*qq X) h \<le> X h"
"\<And>X' h. intuitionistic_q X' \<Longrightarrow> (\<And>h. X' h \<le> X h) \<Longrightarrow> X' h \<le> (1\<^sub>q -*qq X) h"
proof -
(* side condition *)
let ?sc = "\<lambda>a b. (bot < a \<or> bot < b ) \<and> (a < top \<or> b < top)"
show 1: "intuitionistic_q (1\<^sub>q -*qq X)"
proof (rule intuitionistic_qI2)
fix h h' :: 'a
assume *: "h ## h'"
have "(1\<^sub>q -*qq X) h = (INFI {h'. h ## h' \<and> ?sc (emb (\<lambda>s. True) h') (X (h + h')) }
(\<lambda>h'. X (h + h') \<^bold>div emb (\<lambda>s. True) h'))"
unfolding sep_impl_qq_def by simp
also have "\<dots> \<le> (INFI {h'a. h + h' ## h'a \<and> ?sc (emb (\<lambda>s. True) h'a) (X (h + h'+ h'a))}
(\<lambda>h'a. X (h + h' + h'a) \<^bold>div emb (\<lambda>s. True) h'a))"
apply(rule INF_mono)
subgoal for h'' apply(rule bexI[where x="h' + h''"])
using * bot_not_neutral
by (auto simp: sep_disj_addI3 emb_def sep_add_assoc dest: sep_add_disjD)
done
also have "\<dots> = (1\<^sub>q -*qq X) (h + h')"
unfolding sep_impl_qq_def by simp
finally show "(1\<^sub>q -*qq X) h \<le> (1\<^sub>q -*qq X) (h + h')" .
qed
next
fix h
have "(1\<^sub>q -*qq X) h = (INFI {h'. h ## h' \<and> (bot < emb (\<lambda>s. True) h' \<or> bot < X (h + h'))
\<and> (emb (\<lambda>s. True) h' < top \<or> X (h + h') < top)}
(\<lambda>h'. X (h + h') \<^bold>div emb (\<lambda>s. True) h'))"
unfolding sep_impl_qq_def by simp
also have "\<dots> \<le> X h"
apply(cases "X h<top")
subgoal by (rule INF_lower2[where i=0]) (auto simp: bot_not_neutral emb_def divide_neutral)
subgoal by (auto simp: nn)
done
finally show "(1\<^sub>q -*qq X) h \<le> X h" .
next
fix X'
assume "intuitionistic_q X'" and Xmono: "\<And>h. X' h \<le> X h"
fix h (* for arbitrary but fixed h *)
have "X' h = (INFI {h'. h ## h' \<and> (\<^bold>1 < top \<or> X' (h + h') < top) } (\<lambda>h'. X' (h + h')) )"
apply(rule intuitionistic_q_is_attained_at_h_wand) by fact
also have "\<dots> = (INFI {h'. h ## h' \<and> (bot < emb (\<lambda>s. True) h' \<or> bot < X' (h + h'))
\<and> (emb (\<lambda>s. True) h' < top \<or> X' (h + h') < top)}
(\<lambda>h'. X' (h + h') \<^bold>div emb (\<lambda>s. True) h'))"
using bot_not_neutral by (auto simp: emb_def divide_neutral )
also have "\<dots> = (1\<^sub>q -*qq X') h"
unfolding sep_impl_qq_def by simp
also have "\<dots> \<le> (1\<^sub>q -*qq X) h"
apply(rule sep_impl_q_left_mono') by fact
finally show "X' h \<le> (1\<^sub>q -*qq X) h" .
qed
lemma tightest_intuitionistic_expectations_wand:
fixes X :: "'a \<Rightarrow> 'b"
shows
"intuitionistic_q (sep_true -*q X)"
"\<And>h. (sep_true -*q X) h \<le> X h"
"\<And>X' h. intuitionistic_q X' \<Longrightarrow> (\<And>h. X' h \<le> X h) \<Longrightarrow> X' h \<le> (sep_true -*q X) h"
using tightest_intuitionistic_expectations_wand_general by auto
abbreviation (input)
pred_ex_q :: "('b \<Rightarrow> 'a \<Rightarrow> ennreal) \<Rightarrow> 'a \<Rightarrow> ennreal" (binder "EXSq " 10) where
"EXSq x. P x \<equiv> \<lambda>h. SUP x. P x h"
end
end
section \<open>Showing that quantitative separating connectives
instantiated for bool yield the boolean separating connectives\<close>
instantiation "bool" :: one
begin
definition "one_bool == True"
instance by standard
end
interpretation BOOL: quant_sep_con Inf Sup inf "(\<le>)" "(<)" sup bot top
"(\<and>)" "True" "\<lambda>x y. y \<longrightarrow> x"
unfolding quant_sep_con_def comm_quantale_def apply safe
subgoal by standard
subgoal apply standard by auto
subgoal apply standard by auto
subgoal apply standard by auto
done
thm BOOL.oper_left_mono