-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathcrdt_specs.thy
1519 lines (1114 loc) · 65.2 KB
/
crdt_specs.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
section "Composable CRDT specifications"
theory crdt_specs
imports repliss_sem
unique_ids
"HOL-Library.Monad_Syntax"
begin
text "In this section we define the semantics of several conflict-free replicated data types (CRDTs)."
text_raw \<open>\DefineSnippet{crdtSpec}{\<close>
type_synonym ('op, 'res) crdtSpec = "'op \<Rightarrow> ('op, 'res) operationContext \<Rightarrow> 'res \<Rightarrow> bool"
text_raw \<open>}%EndSnippet\<close>
text "An operation context is well-formed if the happens-before relation is transitive and inversely well-founded."
definition
"operationContext_wf ctxt \<equiv>
trans (happensBefore ctxt)
\<and> irrefl (happensBefore ctxt)
\<and> Field (happensBefore ctxt) \<subseteq> dom (calls ctxt)
\<and> finite (dom (calls ctxt))"
lemma operationContext_wf_trans: "operationContext_wf ctxt \<Longrightarrow> trans (happensBefore ctxt)"
unfolding operationContext_wf_def by auto
lemma operationContext_wf_irrefl: "operationContext_wf ctxt \<Longrightarrow> irrefl (happensBefore ctxt)"
unfolding operationContext_wf_def by auto
lemma operationContext_wf_hb_field: "operationContext_wf ctxt \<Longrightarrow> Field (happensBefore ctxt) \<subseteq> dom (calls ctxt)"
unfolding operationContext_wf_def by auto
lemma operationContext_wf_finite: "operationContext_wf ctxt \<Longrightarrow> finite (dom (calls ctxt))"
unfolding operationContext_wf_def by auto
lemma operationContext_wf_finite_hb:
assumes "operationContext_wf ctxt"
shows "finite (happensBefore ctxt)"
proof (rule finite_subset)
show "happensBefore ctxt \<subseteq> dom (calls ctxt) \<times> dom (calls ctxt)"
using operationContext_wf_hb_field[OF assms]
by (auto simp add: Field_def)
show "finite (dom (calls ctxt) \<times> dom (calls ctxt))"
using operationContext_wf_finite[OF assms] by auto
qed
lemma operationContext_wf_wf:
assumes "operationContext_wf ctxt"
shows "wf ((happensBefore ctxt)\<inverse>)"
by (simp add: assms operationContext_wf_finite_hb operationContext_wf_irrefl operationContext_wf_trans wf_converse)
lemma operationContext_wf_exists_max:
assumes wf: "operationContext_wf ctxt"
and "P x"
shows "\<exists>x'. P x' \<and> (x = x' \<or> (x,x')\<in>happensBefore ctxt) \<and> (\<forall>y. P y \<longrightarrow> (x',y)\<notin>happensBefore ctxt)"
using assms by (simp add: exists_max_wf' operationContext_wf_trans operationContext_wf_wf)
text "Some helper functions for defining the specs:"
definition "cOp c_calls c \<equiv> map_option call_operation (c_calls c)"
abbreviation "Op ctxt \<equiv> cOp (calls ctxt)"
definition "Res ctxt c \<equiv> map_option call_res (calls ctxt c)"
definition map_map_values :: "('x \<Rightarrow> 'y) \<Rightarrow> ('k \<rightharpoonup> 'x) \<Rightarrow> ('k \<rightharpoonup> 'y)" where
"map_map_values f m \<equiv> \<lambda>x. case m x of Some a \<Rightarrow> Some (f a) | None \<Rightarrow> None"
definition fmap_map_values :: "('x \<rightharpoonup> 'y) \<Rightarrow> ('k \<rightharpoonup> 'x) \<Rightarrow> ('k \<rightharpoonup> 'y)" where
"fmap_map_values f m \<equiv> \<lambda>x. m x \<bind> f"
lemma fmap_map_values_def':
"fmap_map_values f m = (\<lambda>x. case m x of Some a \<Rightarrow> f a | None \<Rightarrow> None)"
by (auto simp add: fmap_map_values_def split: option.splits)
lemma fmap_map_values_eq_some:
"(fmap_map_values f g x \<triangleq> y) \<longleftrightarrow> (\<exists>a. g x \<triangleq> a \<and> f a \<triangleq> y) "
by (auto simp add: fmap_map_values_def' split: option.splits)
definition
"map_ctxt f c \<equiv> c\<lparr>calls := map_map_values f (calls c)\<rparr>"
definition restrict_hb :: "('op, 'res) operationContext \<Rightarrow> ('op, 'res) operationContext" where
"restrict_hb ctxt \<equiv> ctxt\<lparr>happensBefore := happensBefore ctxt |r dom (calls ctxt)\<rparr>"
lemma calls_restrict_hb[simp]: "calls (restrict_hb c) = calls c"
by (simp add: restrict_hb_def)
lemma happensBefore_restrict_hb[simp]: "happensBefore (restrict_hb c) = happensBefore c |r dom (calls c)"
by (simp add: restrict_hb_def)
definition
"restrict_ctxt f ctxt \<equiv> restrict_hb \<lparr>calls = fmap_map_values f (calls ctxt), happensBefore = happensBefore ctxt\<rparr>"
definition
"map_Call f c \<equiv> case c of Call op r \<Rightarrow> (case f op of None \<Rightarrow> None | Some op' \<Rightarrow> Some (Call op' r))"
text_raw \<open>\DefineSnippet{sub_contexts}{\<close>
definition restrict_ctxt_op :: "('op1 \<rightharpoonup> 'op2) \<Rightarrow> ('op1, 'r) operationContext \<Rightarrow> ('op2, 'r) operationContext" where
"restrict_ctxt_op f \<equiv>
restrict_ctxt (\<lambda>c.
map_option (\<lambda>op'. Call op' (call_res c)) (f (call_operation c)))"
definition ctxt_restrict_calls :: "callId set \<Rightarrow> ('op, 'r) operationContext \<Rightarrow> ('op, 'r) operationContext" where
"ctxt_restrict_calls Cs ctxt = \<lparr>
calls = calls ctxt |` Cs,
happensBefore = happensBefore ctxt |r Cs\<rparr>"
definition sub_context :: "('c \<Rightarrow> 'a option) \<Rightarrow> callId set \<Rightarrow> ('c, 'b) operationContext \<Rightarrow> ('a, 'b) operationContext" where
"sub_context C_in Cs ctxt \<equiv>
(restrict_ctxt_op C_in (ctxt_restrict_calls Cs ctxt))"
text_raw \<open>}%EndSnippet\<close>
lemma calls_restrict_ctxt_op1:
"calls (restrict_ctxt_op f ctxt) c = (case calls ctxt c of None \<Rightarrow> None | Some call \<Rightarrow> map_Call f call)"
by (auto simp add: restrict_ctxt_op_def restrict_ctxt_def fmap_map_values_def map_Call_def intro!: ext split: option.splits call.splits)
lemma Op_restrict_ctxt_op:
"Op (restrict_ctxt_op f ctxt) = (\<lambda>c. Op ctxt c \<bind> f)"
by (auto simp add: cOp_def option_bind_def restrict_ctxt_op_def restrict_ctxt_def fmap_map_values_def
intro!: ext split: option.splits call.splits)
(metis (no_types, lifting) call.sel(1) option.exhaust_sel option.simps(8) option.simps(9))
lemma Op_restrict_ctxt_op_eq:
"Op (restrict_ctxt_op f ctxt) c \<triangleq> X \<longleftrightarrow> (\<exists>Y. Op ctxt c \<triangleq> Y \<and> f Y \<triangleq> X)"
by (auto simp add: Op_restrict_ctxt_op option_bind_def split: option.splits)
lemma happensBefore_restrict_ctxt_op:
"(x,y) \<in> happensBefore (restrict_ctxt_op f ctxt)
\<longleftrightarrow> (x,y)\<in>happensBefore ctxt
\<and> (\<exists>op. (Op ctxt x \<bind> f) \<triangleq> op)
\<and> (\<exists>op. (Op ctxt y \<bind> f) \<triangleq> op)"
by (auto simp add: restrict_ctxt_op_def cOp_def restrict_ctxt_def fmap_map_values_def
restrict_relation_def option_bind_def
split: option.splits call.splits)
lemma happensBefore_restrict_ctxt_op':
"(x,y) \<in> happensBefore (restrict_ctxt_op f ctxt)
\<longleftrightarrow> (x,y)\<in>happensBefore ctxt
\<and> (\<exists>op. Op ctxt x \<triangleq> op \<and> f op \<noteq> None)
\<and> (\<exists>op. Op ctxt y \<triangleq> op \<and> f op \<noteq> None)"
by (auto simp add: happensBefore_restrict_ctxt_op option_bind_def split: option.splits)
text "To combine CRDT specifications, we need to distinguish updates from queries, which we can do using
the following typeclass:"
class crdt_op = valueType +
fixes is_update :: "'a \<Rightarrow> bool"
begin
end
abbreviation "is_query x \<equiv> \<not>is_update x"
text "To make it easier to simplify composed specifications, we define well-formedness of specifications:
A spec is well formed if it only uses happens-before information from existing calls."
definition crdt_spec_wf :: "('op, 'res) crdtSpec \<Rightarrow> bool" where
"crdt_spec_wf spec \<equiv>
\<forall>op c r. spec op (restrict_hb c) r = spec op c r"
lemma use_crdt_spec_wf:
assumes "crdt_spec_wf spec"
shows "spec op (restrict_hb c) = spec op c"
using assms by (auto simp add: crdt_spec_wf_def)
subsection "Counter"
text_raw \<open>\DefineSnippet{counterOp}{\<close>
datatype counterOp =
Increment int
| GetCount
text_raw \<open>}%EndSnippet\<close>
instance counterOp :: countable
by countable_datatype
instantiation counterOp :: crdt_op begin
definition "is_update_counterOp op \<equiv> op \<noteq> GetCount"
definition "uniqueIds_counterOp (op::counterOp) \<equiv> {}::uniqueId set"
definition "default_counterOp \<equiv> GetCount"
instance by standard (auto simp add: uniqueIds_counterOp_def)
end
class from_int = valueType +
fixes from_int :: "int \<Rightarrow> 'a"
assumes from_int_no_uniqueIds: "uniqueIds (from_int x) = {}"
text_raw \<open>\DefineSnippet{counter_spec}{\<close>
definition
"increments op \<equiv> case op of Increment i \<Rightarrow> i | _ \<Rightarrow> 0"
definition counter_spec :: "(counterOp, 'a::{default,from_int}) crdtSpec" where
"counter_spec oper ctxt res \<equiv>
case oper of
Increment i \<Rightarrow> res = default
| GetCount \<Rightarrow> res = from_int (\<Sum>(_,c)\<leftarrow>\<^sub>m calls ctxt. increments (call_operation c))"
text_raw \<open>}%EndSnippet\<close>
subsection "Register"
text_raw \<open>\DefineSnippet{registerOp}{\<close>
datatype 'a registerOp =
Assign 'a
| Read
text_raw \<open>}%EndSnippet\<close>
instance registerOp :: (countable) countable
by countable_datatype
instantiation registerOp :: (valueType) crdt_op begin
definition "uniqueIds_registerOp x \<equiv>
case x of
Assign x \<Rightarrow> uniqueIds x
| Read \<Rightarrow> {}"
definition [simp]: "default_registerOp \<equiv> Read"
definition [simp]: "is_update_registerOp x \<equiv> x \<noteq> Read"
lemma [simp]: "uniqueIds (Assign x) = uniqueIds x"
and [simp]: "uniqueIds Read = {}"
by (auto simp add: uniqueIds_registerOp_def)
instance by (standard, auto simp add: uniqueIds_registerOp_def)
end
text "The latest values are all assigned values that have not been overridden by another call to assign."
text_raw \<open>\DefineSnippet{register_spec}{\<close>
definition
"latestAssignments_h c_ops s_happensBefore \<equiv>
\<lambda>c. case c_ops c of
Some (Assign v) \<Rightarrow>
if \<exists>c' v'. c_ops c' \<triangleq> Assign v' \<and> (c,c')\<in>s_happensBefore then None else Some v
| _ \<Rightarrow> None"
definition latestAssignments :: "('a registerOp, 'r) operationContext \<Rightarrow> callId \<rightharpoonup> 'a" where
"latestAssignments ctxt \<equiv> latestAssignments_h (Op ctxt) (happensBefore ctxt)"
definition
"latestValues ctxt \<equiv> Map.ran (latestAssignments ctxt)"
definition register_spec :: "'a::default \<Rightarrow> ('a registerOp, 'a) crdtSpec" where
"register_spec initial oper ctxt res \<equiv>
case oper of
Assign x \<Rightarrow> res = default
| Read \<Rightarrow> if latestValues ctxt = {} then res = initial else res \<in> latestValues ctxt "
definition lww_register_spec :: "'a::default \<Rightarrow> ('a registerOp, 'a) crdtSpec" where
"lww_register_spec initial oper ctxt res \<equiv>
case oper of
Assign x \<Rightarrow> res = default
| Read \<Rightarrow> res = firstValue initial (latestAssignments ctxt)"
text_raw \<open>}%EndSnippet\<close>
lemma ctxt_spec_wf_latestAssignments[simp]:
"latestAssignments (restrict_hb c) = latestAssignments c"
by (auto simp add: restrict_hb_def latestAssignments_h_def
restrict_relation_def latestAssignments_def cOp_def
intro!: ext
split: option.splits if_splits registerOp.splits call.splits,
blast+)
lemma latestValues_def2:
"latestValues ctxt =
{v | c v. Op ctxt c \<triangleq> Assign v
\<and> (\<nexists>c' v'. Op ctxt c' \<triangleq> Assign v' \<and> (c,c')\<in>happensBefore ctxt)}"
proof (auto simp add: latestValues_def latestAssignments_def latestAssignments_h_def image_def ran_def
split: option.splits call.splits if_splits, fuzzy_goal_cases G)
case (G x a y)
then show ?case
by (auto simp add: cOp_def split: option.splits registerOp.splits if_splits)
qed
lemma ctxt_spec_wf_latestValues[simp]:
"latestValues (restrict_hb c) = latestValues c"
by (auto simp add: latestValues_def)
lemma latest_assignments_wf:
"latestAssignments_h c_calls (Restr c_happensBefore (dom c_calls))
= latestAssignments_h c_calls c_happensBefore"
by (auto simp add: latestAssignments_h_def intro!: ext split: call.splits option.splits registerOp.splits, auto)
lemma latest_assignments_wf2[simp]:
assumes "c_calls \<subseteq>\<^sub>m Op c"
shows "latestAssignments_h c_calls (happensBefore (restrict_hb c))
= latestAssignments_h c_calls (happensBefore c)"
using assms by (auto simp add: cOp_def map_option_case map_le_def latestAssignments_h_def restrict_hb_def restrict_relation_def intro!: ext split: call.splits option.splits registerOp.splits,
auto,
meson domExists_simp domIff)
lemma register_spec_restrict_hb[simp]:
"register_spec i op (restrict_hb c) r
\<longleftrightarrow> register_spec i op c r"
by (auto simp add: register_spec_def split: registerOp.splits)
lemma register_spec_wf: "crdt_spec_wf (register_spec i)"
by (auto simp add: crdt_spec_wf_def )
lemma lwwregister_restrict_hb[simp]:
"lww_register_spec i op (restrict_hb c) r
\<longleftrightarrow> lww_register_spec i op c r"
by (auto simp add: lww_register_spec_def split: registerOp.splits )
lemma lwwregister_spec_wf: "crdt_spec_wf (lww_register_spec i)"
by (simp add: crdt_spec_wf_def)
subsection "Multi-Value Register"
class is_set =
fixes is_set :: "'a \<Rightarrow> 'a set \<Rightarrow> bool"
text_raw \<open>\DefineSnippet{mv_register_spec}{\<close>
definition mv_register_spec :: "('a registerOp, 'a::{default,is_set}) crdtSpec" where
"mv_register_spec oper ctxt res \<equiv>
case oper of
Assign x \<Rightarrow> res = default
| Read \<Rightarrow> is_set res (latestValues ctxt)"
text_raw \<open>}%EndSnippet\<close>
lemma mv_register_spec_restrict_hb[simp]:
"mv_register_spec op (restrict_hb c) r
= mv_register_spec op c r"
by (auto simp add: mv_register_spec_def split: registerOp.splits)
lemma mv_register_spec_wf: "crdt_spec_wf mv_register_spec"
by (simp add: crdt_spec_wf_def)
subsection "Flags"
text_raw \<open>\DefineSnippet{flagOp}{\<close>
datatype flagOp = Enable | Disable | ReadFlag
text_raw \<open>}%EndSnippet\<close>
instance flagOp :: countable
by countable_datatype
instantiation flagOp :: crdt_op begin
definition [simp]: "is_update_flagOp op \<equiv> op \<noteq> ReadFlag"
definition "uniqueIds_flagOp (op::flagOp) \<equiv> {}::uniqueId set"
definition "default_flagOp \<equiv> ReadFlag"
instance by standard (auto simp add: uniqueIds_flagOp_def)
end
class from_bool = valueType +
fixes from_bool :: "bool \<Rightarrow> 'a"
assumes from_bool_no_uniqueIds[simp]: "uniqueIds (from_bool x) = {}"
and from_bool_inj: "(from_bool x = from_bool y) \<longleftrightarrow> x = y"
instantiation bool :: from_bool begin
definition from_bool_bool :: "bool\<Rightarrow>bool" where [simp]: "from_bool_bool = id"
instance
by standard auto
end
text_raw \<open>\DefineSnippet{flag_specs}{\<close>
definition
"latestOps ctxt \<equiv>
{op | c op.
Op ctxt c \<triangleq> op
\<and> is_update op
\<and> (\<nexists>c' op'. Op ctxt c' \<triangleq> op'
\<and> is_update op'
\<and> (c, c')\<in>happensBefore ctxt)}"
definition flag_dw_spec :: "(flagOp, 'a::{default,from_bool}) crdtSpec" where
"flag_dw_spec oper ctxt res \<equiv>
case oper of
ReadFlag \<Rightarrow> res = from_bool (Enable \<in> latestOps ctxt \<and> Disable \<notin> latestOps ctxt)
| _ \<Rightarrow> res = default"
definition flag_ew_spec :: "(flagOp, 'a::{default,from_bool}) crdtSpec" where
"flag_ew_spec oper ctxt res \<equiv>
case oper of
ReadFlag \<Rightarrow> res = from_bool (Enable \<in> latestOps ctxt)
| _ \<Rightarrow> res = default"
definition flag_sdw_spec :: "(flagOp, 'a::{default,from_bool}) crdtSpec" where
"flag_sdw_spec oper ctxt res \<equiv>
case oper of
ReadFlag \<Rightarrow> res = from_bool (\<exists>e. Op ctxt e \<triangleq> Enable
\<and> (\<forall>d. Op ctxt d \<triangleq> Disable \<longrightarrow> (d,e)\<in>happensBefore ctxt))
| _ \<Rightarrow> res = default"
definition flag_sew_spec :: "(flagOp, 'a::{default,from_bool}) crdtSpec" where
"flag_sew_spec oper ctxt res \<equiv>
case oper of
ReadFlag \<Rightarrow> res = from_bool ((\<exists>e. Op ctxt e \<triangleq> Enable)
\<and> (\<nexists>d. Op ctxt d \<triangleq> Disable
\<and> (\<forall>e. Op ctxt e \<triangleq> Enable \<longrightarrow> (e,d)\<in>happensBefore ctxt)))
| _ \<Rightarrow> res = default"
text_raw \<open>}%EndSnippet\<close>
text "Now we prove alternative specifications for the flags:"
lemma latestOps_alt:
assumes wf: "operationContext_wf ctxt"
shows "x \<in> latestOps ctxt \<longleftrightarrow> is_update x \<and>
(\<exists>c. Op ctxt c \<triangleq> x \<and> (\<forall>c' x'. Op ctxt c' \<triangleq> x' \<longrightarrow> is_update x' \<longrightarrow> (c, c')\<in>happensBefore ctxt \<longrightarrow> x' = x))"
proof safe
fix x
assume "x \<in> latestOps ctxt"
show "is_update x"
using \<open>x \<in> latestOps ctxt\<close> latestOps_def by blast
from `x \<in> latestOps ctxt`
obtain c
where a0: "Op ctxt c \<triangleq> x"
and a1: "is_update x"
and a2: "\<forall>c' op'. is_update op' \<longrightarrow> Op ctxt c' \<triangleq> op' \<longrightarrow> (c, c') \<notin> happensBefore ctxt"
by (auto simp add: latestOps_def)
show "\<exists>c. Op ctxt c \<triangleq> x \<and> (\<forall>c' x'. Op ctxt c' \<triangleq> x' \<longrightarrow> is_update x' \<longrightarrow> (c, c') \<in> happensBefore ctxt \<longrightarrow> x' = x)"
proof (intro exI conjI allI impI)
show "Op ctxt c \<triangleq> x"
by (simp add: a0)
show "x' = x"
if c0: "Op ctxt c' \<triangleq> x'"
and c1: "(c, c') \<in> happensBefore ctxt"
and c2: "is_update x'"
for c' x'
using a2 c0 c1 c2 by blast
qed
next
fix c
assume a0: "is_update x"
and a1: "Op ctxt c \<triangleq> x"
and a2: "\<forall>c' x'. Op ctxt c' \<triangleq> x' \<longrightarrow> is_update x' \<longrightarrow> (c, c') \<in> happensBefore ctxt \<longrightarrow> x' = x"
text "Obtain hb-maximal c:"
obtain cm
where "Op ctxt cm \<triangleq> x"
and "cm = c \<or> (c,cm)\<in>happensBefore ctxt"
and "\<forall>y. Op ctxt y \<triangleq> x \<longrightarrow> (cm, y) \<notin> happensBefore ctxt"
using operationContext_wf_exists_max[OF wf, where P="\<lambda>c. Op ctxt c \<triangleq> x", OF a1]
by auto
show "x \<in> latestOps ctxt"
proof (auto simp add: latestOps_def `Op ctxt cm \<triangleq> x` a0 intro!: exI[where x=cm])
fix c' op'
assume b0: "is_update op'"
and b1: "Op ctxt c' \<triangleq> op'"
and b2: "(cm, c') \<in> happensBefore ctxt"
have "(c, c') \<in> happensBefore ctxt"
by (metis \<open>cm = c \<or> (c, cm) \<in> happensBefore ctxt\<close> b2 local.wf operationContext_wf_trans transE)
from a2[rule_format, OF `Op ctxt c' \<triangleq> op'` `is_update op'` `(c, c') \<in> happensBefore ctxt`]
show "False"
using \<open>\<forall>y. Op ctxt y \<triangleq> x \<longrightarrow> (cm, y) \<notin> happensBefore ctxt\<close> b1 b2 by blast
qed
qed
lemma latestOps_Enable:
assumes wf: "operationContext_wf ctxt"
shows "Enable \<in> latestOps ctxt \<longleftrightarrow>
(\<exists>c. Op ctxt c \<triangleq> Enable \<and> (\<forall>c'. Op ctxt c' \<triangleq> Disable \<longrightarrow> (c, c')\<notin>happensBefore ctxt))"
using flagOp.exhaust by (auto simp add: latestOps_alt[OF wf])
lemma latestOps_Disable:
assumes wf: "operationContext_wf ctxt"
shows "Disable \<in> latestOps ctxt \<longleftrightarrow>
(\<exists>c. Op ctxt c \<triangleq> Disable \<and> (\<forall>c'. Op ctxt c' \<triangleq> Enable \<longrightarrow> (c, c')\<notin>happensBefore ctxt))"
using flagOp.exhaust by (auto simp add: latestOps_alt[OF wf])
lemma latestOps_Enable':
shows "Enable \<in> latestOps ctxt \<longleftrightarrow>
(\<exists>c. Op ctxt c \<triangleq> Enable \<and> (\<forall>c'. Op ctxt c' \<triangleq> Enable \<or> Op ctxt c' \<triangleq> Disable \<longrightarrow> (c, c')\<notin>happensBefore ctxt))"
by (auto simp add: latestOps_def)
(metis (mono_tags, lifting) flagOp.exhaust)
lemma latestOps_Disable':
shows "Disable \<in> latestOps ctxt \<longleftrightarrow>
(\<exists>c. Op ctxt c \<triangleq> Disable \<and> (\<forall>c'. Op ctxt c' \<triangleq> Enable \<or> Op ctxt c' \<triangleq> Disable \<longrightarrow> (c, c')\<notin>happensBefore ctxt))"
by (auto simp add: latestOps_def)
(metis (mono_tags, lifting) flagOp.exhaust)
lemma latestOps_Enable'':
assumes wf: "operationContext_wf ctxt"
and "\<exists>e. Op ctxt e \<triangleq> Enable"
and "\<forall>d. Op ctxt d \<triangleq> Disable \<longrightarrow> (\<exists>e. Op ctxt e \<triangleq> Enable \<and> (d, e) \<in> happensBefore ctxt)"
shows "Enable \<in> latestOps ctxt"
proof -
obtain e where e: "Op ctxt e \<triangleq> Enable \<or> Op ctxt e \<triangleq> Disable"
using assms(2) by blast
obtain em
where "Op ctxt em \<triangleq> Enable \<or> Op ctxt em \<triangleq> Disable"
and "\<forall>e'. (Op ctxt e' \<triangleq> Enable \<or> Op ctxt e' \<triangleq> Disable) \<longrightarrow> (em,e')\<notin>happensBefore ctxt"
using operationContext_wf_exists_max[OF wf, where P="\<lambda>e. Op ctxt e \<triangleq> Enable \<or> Op ctxt e \<triangleq> Disable", OF e]
by auto
show ?thesis
by (auto simp add: latestOps_alt[OF wf])
(metis (mono_tags, lifting) \<open>\<And>thesis. (\<And>em. \<lbrakk>Op ctxt em \<triangleq> Enable \<or> Op ctxt em \<triangleq> Disable; \<forall>e'. Op ctxt e' \<triangleq> Enable \<or> Op ctxt e' \<triangleq> Disable \<longrightarrow> (em, e') \<notin> happensBefore ctxt\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis\<close> assms(3) flagOp.exhaust)
qed
lemma latestOps_Disable'':
assumes wf: "operationContext_wf ctxt"
and "\<exists>e. Op ctxt e \<triangleq> Disable"
and "\<forall>d. Op ctxt d \<triangleq> Enable \<longrightarrow> (\<exists>e. Op ctxt e \<triangleq> Disable \<and> (d, e) \<in> happensBefore ctxt)"
shows "Disable \<in> latestOps ctxt"
proof -
obtain e where e: "Op ctxt e \<triangleq> Enable \<or> Op ctxt e \<triangleq> Disable"
using assms(2) by blast
obtain em
where "Op ctxt em \<triangleq> Enable \<or> Op ctxt em \<triangleq> Disable"
and "\<forall>e'. (Op ctxt e' \<triangleq> Enable \<or> Op ctxt e' \<triangleq> Disable) \<longrightarrow> (em,e')\<notin>happensBefore ctxt"
using operationContext_wf_exists_max[OF wf, where P="\<lambda>e. Op ctxt e \<triangleq> Enable \<or> Op ctxt e \<triangleq> Disable", OF e]
by auto
show ?thesis
by (auto simp add: latestOps_alt[OF wf])
(metis (full_types) \<open>Op ctxt em \<triangleq> Enable \<or> Op ctxt em \<triangleq> Disable\<close> \<open>\<forall>e'. Op ctxt e' \<triangleq> Enable \<or> Op ctxt e' \<triangleq> Disable \<longrightarrow> (em, e') \<notin> happensBefore ctxt\<close> assms(3) flagOp.exhaust)
qed
lemma flag_dw_ReadFlag:
assumes a1: "flag_dw_spec ReadFlag ctxt res"
and wf: "operationContext_wf ctxt"
shows "res = from_bool ((\<exists>e. Op ctxt e \<triangleq> Enable)
\<and> (\<forall>d. Op ctxt d \<triangleq> Disable \<longrightarrow> (\<exists>e. Op ctxt e \<triangleq> Enable \<and> (d,e) \<in> happensBefore ctxt)))
"
proof -
from a1
have res1: "res = from_bool (Enable \<in> latestOps ctxt \<and> Disable \<notin> latestOps ctxt)"
by (simp add: flag_dw_spec_def)
show ?thesis
unfolding res1
by (rule arg_cong[where f=from_bool])
(meson latestOps_Disable latestOps_Enable' latestOps_Enable'' local.wf)
qed
subsection "Sets"
text_raw \<open>\DefineSnippet{setOp}{\<close>
datatype 'v setOp =
Add 'v
| Remove 'v
| Contains 'v
text_raw \<open>}%EndSnippet\<close>
instance setOp :: (countable) countable
by countable_datatype
instantiation setOp :: (valueType) crdt_op begin
definition "uniqueIds_setOp x \<equiv>
case x of
Add v \<Rightarrow> uniqueIds v
| Remove v \<Rightarrow> uniqueIds v
| Contains v \<Rightarrow> uniqueIds v"
definition [simp]: "default_setOp \<equiv> Add default"
definition "is_update_setOp x \<equiv> case x of Add _ \<Rightarrow> True | Remove _ \<Rightarrow> True | Contains _ \<Rightarrow> False"
lemma [simp]: "uniqueIds (Add v) = uniqueIds v"
and [simp]:"uniqueIds (Remove v) = uniqueIds v"
and [simp]:"uniqueIds (Contains v) = uniqueIds v"
by (auto simp add: uniqueIds_setOp_def)
lemma [simp]: "is_update (Add v) = True"
and [simp]:"is_update (Remove v) = True"
and [simp]:"is_update (Contains v) = False"
by (auto simp add: is_update_setOp_def)
instance by (standard, auto simp add: uniqueIds_setOp_def)
end
text_raw \<open>\DefineSnippet{set_specs}{\<close>
definition set_to_flag where
"set_to_flag v op \<equiv> case op of
Add x \<Rightarrow> if x = v then Some Enable else None
| Remove x \<Rightarrow> if x = v then Some Disable else None
| _ \<Rightarrow> None
"
definition set_spec :: "(flagOp, 'r::{default,from_bool}) crdtSpec \<Rightarrow> ('v setOp, 'r) crdtSpec" where
"set_spec F op ctxt res \<equiv>
case op of
Add _ => res = default
| Remove _ \<Rightarrow> res = default
| Contains v \<Rightarrow> F ReadFlag (restrict_ctxt_op (set_to_flag v) ctxt) res"
definition "set_aw_spec \<equiv> set_spec flag_ew_spec"
definition "set_rw_spec \<equiv> set_spec flag_dw_spec"
text_raw \<open>}%EndSnippet\<close>
lemma set_aw_spec_Add[simp]:
"set_aw_spec (Add x) ctxt res \<longleftrightarrow> res = default"
by (auto simp add: set_aw_spec_def set_spec_def)
lemma set_aw_spec_Remove[simp]:
"set_aw_spec (Remove x) ctxt res \<longleftrightarrow> res = default"
by (auto simp add: set_aw_spec_def set_spec_def)
lemma set_rw_spec_Add[simp]:
"set_rw_spec (Add x) ctxt res \<longleftrightarrow> res = default"
by (auto simp add: set_rw_spec_def set_spec_def)
lemma set_rw_spec_Remove[simp]:
"set_rw_spec (Remove x) ctxt res \<longleftrightarrow> res = default"
by (auto simp add: set_rw_spec_def set_spec_def)
lemma from_bool_eq_simp:
assumes "res = from_bool True \<or> res = from_bool False"
shows "(res = from_bool a \<longleftrightarrow> res = from_bool b) \<longleftrightarrow> a = b"
using assms
by (metis from_bool_inj)
lemma from_bool_eq_simp':
assumes "a \<longleftrightarrow> b"
shows "(res = from_bool a \<longleftrightarrow> res = from_bool b)"
by (simp add: assms)
lemma set_to_flag_Enable:
"set_to_flag x y \<triangleq> Enable \<longleftrightarrow> y = Add x"
by (auto simp add: set_to_flag_def split: setOp.splits)
lemma set_to_flag_Disable:
"set_to_flag x y \<triangleq> Disable \<longleftrightarrow> y = Remove x"
by (auto simp add: set_to_flag_def split: setOp.splits)
lemma set_to_flag_None:
"set_to_flag x y = None \<longleftrightarrow> y \<noteq> Remove x \<and> y \<noteq> Add x"
by (auto simp add: set_to_flag_def split: setOp.splits)
lemma trans_restrict_ctxt_op:
assumes "trans (happensBefore ctxt)"
shows "trans (happensBefore (restrict_ctxt_op (set_to_flag x) ctxt))"
by (auto simp add: trans_def happensBefore_restrict_ctxt_op,
meson assms transE)
lemma wf_restrict_ctxt_op:
assumes "wf ((happensBefore ctxt)\<inverse>)"
shows "wf ((happensBefore (restrict_ctxt_op (set_to_flag x) ctxt))\<inverse>)"
using assms proof (rule wf_subset)
show "(happensBefore (restrict_ctxt_op (set_to_flag x) ctxt))\<inverse> \<subseteq> (happensBefore ctxt)\<inverse>"
by (auto simp add: happensBefore_restrict_ctxt_op)
qed
lemma Field_restrict_ctxt_op:
assumes "Field (happensBefore ctxt) \<subseteq> dom (calls ctxt)"
shows "Field (happensBefore (restrict_ctxt_op (set_to_flag x) ctxt)) \<subseteq> dom (calls (restrict_ctxt_op (set_to_flag x) ctxt))"
using assms by (auto simp add: Field_def happensBefore_restrict_ctxt_op)
(metis cOp_def Op_restrict_ctxt_op map_option_eq_Some)+
lemma operationContext_wf_restrict_ctxt_op:
assumes "operationContext_wf ctxt"
shows "operationContext_wf (restrict_ctxt_op (set_to_flag x) ctxt)"
unfolding operationContext_wf_def
proof (intro conjI)
show "trans (happensBefore (restrict_ctxt_op (set_to_flag x) ctxt))"
by (simp add: assms operationContext_wf_trans trans_restrict_ctxt_op)
show "Field (happensBefore (restrict_ctxt_op (set_to_flag x) ctxt)) \<subseteq> dom (calls (restrict_ctxt_op (set_to_flag x) ctxt))"
by (simp add: Field_restrict_ctxt_op assms operationContext_wf_hb_field)
show "irrefl (happensBefore (restrict_ctxt_op (set_to_flag x) ctxt))"
by (meson assms happensBefore_restrict_ctxt_op irrefl_def operationContext_wf_irrefl)
show "finite (dom (calls (restrict_ctxt_op (set_to_flag x) ctxt)))"
proof (rule finite_subset)
show "dom (calls (restrict_ctxt_op (set_to_flag x) ctxt)) \<subseteq> dom (calls ctxt)"
by (auto simp add: restrict_ctxt_op_def restrict_ctxt_def fmap_map_values_def option_bind_def split: option.splits)
show "finite (dom (calls ctxt))"
by (simp add: assms operationContext_wf_finite)
qed
qed
lemma set_aw_spec_Contains:
assumes spec: "set_aw_spec (Contains x) ctxt res"
and wf: "operationContext_wf ctxt"
shows "res = from_bool (\<exists>a. Op ctxt a \<triangleq> Add x
\<and> (\<nexists>r. Op ctxt r \<triangleq> Remove x
\<and> (a,r)\<in>happensBefore ctxt))"
using spec proof (auto simp add: set_aw_spec_def set_spec_def flag_ew_spec_def from_bool_inj)
assume a0: "res = from_bool True"
and a1: "Enable \<in> latestOps (restrict_ctxt_op (set_to_flag x) ctxt)"
have "\<exists>a. Op (restrict_ctxt_op (set_to_flag x) ctxt) a \<triangleq> Enable
\<and> (\<forall>r. Op (restrict_ctxt_op (set_to_flag x) ctxt) r \<triangleq> Disable
\<longrightarrow> (a, r) \<notin> happensBefore (restrict_ctxt_op (set_to_flag x) ctxt))"
using a1 latestOps_Enable' by blast
thus "\<exists>a. Op ctxt a \<triangleq> Add x \<and> (\<forall>r. Op ctxt r \<triangleq> Remove x \<longrightarrow> (a, r) \<notin> happensBefore ctxt)"
by (auto simp add: Op_restrict_ctxt_op option_bind_def happensBefore_restrict_ctxt_op
set_to_flag_Enable set_to_flag_Disable split: option.splits)
(auto simp add: set_to_flag_def)
next
fix a
assume a0: "res = from_bool (Enable \<in> latestOps (restrict_ctxt_op (set_to_flag x) ctxt))"
and a1: "Op ctxt a \<triangleq> Add x"
and a2: "\<forall>r. Op ctxt r \<triangleq> Remove x \<longrightarrow> (a, r) \<notin> happensBefore ctxt"
have a1': "Op (restrict_ctxt_op (set_to_flag x) ctxt) a \<triangleq> Enable"
by (simp add: Op_restrict_ctxt_op a1 set_to_flag_Enable)
have a2': "\<forall>r. Op (restrict_ctxt_op (set_to_flag x) ctxt) r \<triangleq> Disable
\<longrightarrow> (a, r) \<notin> happensBefore (restrict_ctxt_op (set_to_flag x) ctxt)"
by (simp add: Op_restrict_ctxt_op a2 bind_eq_Some_conv happensBefore_restrict_ctxt_op set_to_flag_Disable)
have wf'': "operationContext_wf (restrict_ctxt_op (set_to_flag x) ctxt)"
by (simp add: local.wf operationContext_wf_restrict_ctxt_op)
show "Enable \<in> latestOps (restrict_ctxt_op (set_to_flag x) ctxt)"
using a1' a2' latestOps_Enable operationContext_wf_def wf'' by blast
qed
lemma set_aw_spec_Contains2:
assumes spec: "res = from_bool (\<exists>a. Op ctxt a \<triangleq> Add x
\<and> (\<nexists>r. Op ctxt r \<triangleq> Remove x
\<and> (a,r)\<in>happensBefore ctxt))" (is "res = from_bool ?b")
and wf: "operationContext_wf ctxt"
shows "set_aw_spec (Contains x) ctxt res"
proof (auto simp add: set_aw_spec_def set_spec_def flag_ew_spec_def )
have owf: "operationContext_wf (restrict_ctxt_op (set_to_flag x) ctxt)"
by (simp add: local.wf operationContext_wf_restrict_ctxt_op)
show "res = from_bool (Enable \<in> latestOps (restrict_ctxt_op (set_to_flag x) ctxt))"
proof (cases "?b")
case True
from this obtain a where "Op ctxt a \<triangleq> Add x"
and "\<nexists>r. Op ctxt r \<triangleq> Remove x \<and> (a, r) \<in> happensBefore ctxt"
by blast
thm set_to_flag_Disable set_to_flag_Enable
hence "Enable \<in> latestOps (restrict_ctxt_op (set_to_flag x) ctxt)"
by (subst latestOps_Enable[OF owf])
(auto simp add: Op_restrict_ctxt_op option_bind_def set_to_flag_def happensBefore_restrict_ctxt_op' split: option.splits setOp.splits cong: conj_cong)
thus ?thesis
using True local.spec by auto
next
case False
hence "Enable \<notin> latestOps (restrict_ctxt_op (set_to_flag x) ctxt)"
by (subst latestOps_Enable[OF owf])
(auto simp add: Op_restrict_ctxt_op option_bind_def set_to_flag_def happensBefore_restrict_ctxt_op' split: option.splits setOp.splits cong: conj_cong,
fastforce)
then show ?thesis
by (smt False local.spec)
qed
qed
lemma set_aw_spec_contains:
assumes "operationContext_wf ctxt"
shows "set_aw_spec (Contains x) ctxt res \<longleftrightarrow>
res = from_bool (\<exists>a. Op ctxt a \<triangleq> Add x
\<and> (\<nexists>r. Op ctxt r \<triangleq> Remove x
\<and> (a,r)\<in>happensBefore ctxt))"
using assms set_aw_spec_Contains set_aw_spec_Contains2 by fastforce
text \<open>
\DefineSnippet{set_aw_spec_contains}{
@{thm [display] (concl) set_aw_spec_contains}
}%EndSnippet\<close>
lemma exists_skolem:
"(\<exists>f. \<forall>x. P x (f x)) \<longleftrightarrow> (\<forall>x. \<exists>y. P x y)"
by metis
lemma exists_skolem2a:
"(\<exists>f. \<forall>x y. P x y (f x y)) \<longleftrightarrow> (\<forall>x y. \<exists>z. P x y z)"
by metis
lemma exists_skolem2b:
"(\<exists>f. \<forall>y x. P x y (f x y)) \<longleftrightarrow> (\<forall>y x. \<exists>z. P x y z)"
by (subst all_comm, subst exists_skolem2a) auto
text_raw \<open>\DefineSnippet{set_rw_spec_Contains}{\<close>
lemma set_rw_spec_Contains:
assumes spec: "set_rw_spec (Contains x) ctxt res"
and wf: "operationContext_wf ctxt"
shows "res = from_bool ((\<exists>a. Op ctxt a \<triangleq> Add x)
\<and> (\<forall>r. Op ctxt r \<triangleq> Remove x
\<longrightarrow> (\<exists>a. Op ctxt a \<triangleq> Add x
\<and> (r,a)\<in>happensBefore ctxt)))"
text_raw \<open>}%EndSnippet\<close>
using spec proof (auto simp add: set_rw_spec_def set_spec_def flag_dw_spec_def from_bool_inj)
assume a0: "res = from_bool True"
and a1: "Enable \<in> latestOps (restrict_ctxt_op (set_to_flag x) ctxt)"
and a2: "Disable \<notin> latestOps (restrict_ctxt_op (set_to_flag x) ctxt)"
show "\<exists>a. Op ctxt a \<triangleq> Add x"
by (smt Op_restrict_ctxt_op a1 bind_eq_Some_conv latestOps_Enable' set_to_flag_Enable)
next
fix r
assume a0: "res = from_bool True"
and a1: "Enable \<in> latestOps (restrict_ctxt_op (set_to_flag x) ctxt)"
and a2: "Disable \<notin> latestOps (restrict_ctxt_op (set_to_flag x) ctxt)"
and a3: "Op ctxt r \<triangleq> Remove x"
show "\<exists>a. Op ctxt a \<triangleq> Add x \<and> (r, a) \<in> happensBefore ctxt"
proof -
obtain cc :: "callId \<Rightarrow> (flagOp, 'b) operationContext \<Rightarrow> callId" where
f1: "\<forall>x0 x1. (\<exists>v2. Op x1 v2 \<triangleq> Enable \<and> (x0, v2) \<in> happensBefore x1) = (Op x1 (cc x0 x1) \<triangleq> Enable \<and> (x0, cc x0 x1) \<in> happensBefore x1)"
by moura
obtain ss :: "flagOp \<Rightarrow> ('a setOp \<Rightarrow> flagOp option) \<Rightarrow> 'a setOp option \<Rightarrow> 'a setOp" where
"\<forall>x0 x1 x2. (\<exists>v3. x2 \<triangleq> v3 \<and> x1 v3 \<triangleq> x0) = (x2 \<triangleq> ss x0 x1 x2 \<and> x1 (ss x0 x1 x2) \<triangleq> x0)"
by moura
then have f2: "\<forall>z f fa. (z \<bind> f \<noteq> Some fa \<or> z \<triangleq> ss fa f z \<and> f (ss fa f z) \<triangleq> fa) \<and> ((z \<bind> f) \<triangleq> fa \<or> (\<forall>s. z \<noteq> Some s \<or> f s \<noteq> Some fa))"
by (meson bind_eq_Some_conv)
have "(Some (Remove x) \<bind> set_to_flag x) \<triangleq> Disable"
by (simp add: set_to_flag_Disable)
then have "Op (restrict_ctxt_op (set_to_flag x) ctxt) (cc r (restrict_ctxt_op (set_to_flag x) ctxt)) \<triangleq> Enable \<and> (r, cc r (restrict_ctxt_op (set_to_flag x) ctxt)) \<in> happensBefore (restrict_ctxt_op (set_to_flag x) ctxt)"
using f1
by (metis Op_restrict_ctxt_op a2 a3 latestOps_Disable local.wf operationContext_wf_restrict_ctxt_op)
then show ?thesis
using f2 by (metis (full_types) Op_restrict_ctxt_op happensBefore_restrict_ctxt_op set_to_flag_Enable)
qed
next
fix a
assume a0: "res = from_bool (Enable \<in> latestOps (restrict_ctxt_op (set_to_flag x) ctxt) \<and> Disable \<notin> latestOps (restrict_ctxt_op (set_to_flag x) ctxt))"
and a1: "\<forall>r. Op ctxt r \<triangleq> Remove x \<longrightarrow> (\<exists>a. Op ctxt a \<triangleq> Add x \<and> (r, a) \<in> happensBefore ctxt)"
and a2: "Op ctxt a \<triangleq> Add x"
show "Enable \<in> latestOps (restrict_ctxt_op (set_to_flag x) ctxt)"
proof (rule latestOps_Enable'')
show "operationContext_wf (restrict_ctxt_op (set_to_flag x) ctxt)"
by (simp add: local.wf operationContext_wf_restrict_ctxt_op)
show "\<exists>e. Op (restrict_ctxt_op (set_to_flag x) ctxt) e \<triangleq> Enable"
by (metis Op_restrict_ctxt_op a2 bind.bind_lunit set_to_flag_Enable)
show "\<forall>d. Op (restrict_ctxt_op (set_to_flag x) ctxt) d \<triangleq> Disable \<longrightarrow>
(\<exists>e. Op (restrict_ctxt_op (set_to_flag x) ctxt) e \<triangleq> Enable \<and>
(d, e) \<in> happensBefore (restrict_ctxt_op (set_to_flag x) ctxt))"
by (auto simp add: Op_restrict_ctxt_op happensBefore_restrict_ctxt_op)
(metis (no_types, lifting) a1 bind_eq_Some_conv set_to_flag_Disable set_to_flag_Enable)
qed
next
fix a
assume a0: "res = from_bool False"
and a1: "\<forall>r. Op ctxt r \<triangleq> Remove x \<longrightarrow> (\<exists>a. Op ctxt a \<triangleq> Add x \<and> (r, a) \<in> happensBefore ctxt)"
and a2: "Op ctxt a \<triangleq> Add x"
and a3: "Disable \<in> latestOps (restrict_ctxt_op (set_to_flag x) ctxt)"
have wf': "operationContext_wf (restrict_ctxt_op (set_to_flag x) ctxt)"
by (simp add: local.wf operationContext_wf_restrict_ctxt_op)
show "False"
proof -
obtain cc :: "callId \<Rightarrow> flagOp \<Rightarrow> (flagOp, 'b) operationContext \<Rightarrow> callId" and ff :: "callId \<Rightarrow> flagOp \<Rightarrow> (flagOp, 'b) operationContext \<Rightarrow> flagOp" where
f2: "\<forall>x0 x1 x2. (\<exists>v3 v4. (Op x2 v3 \<triangleq> v4 \<and> is_update v4 \<and> (x0, v3) \<in> happensBefore x2) \<and> v4 \<noteq> x1) = ((Op x2 (cc x0 x1 x2) \<triangleq> ff x0 x1 x2 \<and> is_update (ff x0 x1 x2) \<and> (x0, cc x0 x1 x2) \<in> happensBefore x2) \<and> ff x0 x1 x2 \<noteq> x1)"
by moura
obtain cca :: "flagOp \<Rightarrow> (flagOp, 'b) operationContext \<Rightarrow> callId" where
"\<forall>x0 x1. (\<exists>v2. Op x1 v2 \<triangleq> x0 \<and> (\<forall>v3 v4. (Op x1 v3 \<noteq> Some v4 \<or> is_query v4 \<or> (v2, v3) \<notin> happensBefore x1) \<or> v4 = x0)) = (Op x1 (cca x0 x1) \<triangleq> x0 \<and> (\<forall>v3 v4. (Op x1 v3 \<noteq> Some v4 \<or> is_query v4 \<or> (cca x0 x1, v3) \<notin> happensBefore x1) \<or> v4 = x0))"
by (atomize_elim, subst exists_skolem2a, auto, blast)
then have f3: "\<forall>f z. ((f \<in> latestOps z) = (is_update f \<and> (\<exists>c. Op z c \<triangleq> f \<and> (\<forall>ca fa. (Op z ca \<noteq> Some fa \<or> is_query fa \<or> (c, ca) \<notin> happensBefore z) \<or> fa = f)))) = ((f \<notin> latestOps z \<or> is_update f \<and> Op z (cca f z) \<triangleq> f \<and> (\<forall>c fa. (Op z c \<noteq> Some fa \<or> is_query fa \<or> (cca f z, c) \<notin> happensBefore z) \<or> fa = f)) \<and> (f \<in> latestOps z \<or> is_query f \<or> (\<forall>c. Op z c \<noteq> Some f \<or> (Op z (cc c f z) \<triangleq> ff c f z \<and> is_update (ff c f z) \<and> (c, cc c f z) \<in> happensBefore z) \<and> ff c f z \<noteq> f)))"
using f2 by blast
have f4: "wf ((happensBefore (restrict_ctxt_op (set_to_flag x) ctxt))\<inverse>)"
by (simp add: local.wf operationContext_wf_wf wf_restrict_ctxt_op)
have "trans (happensBefore (restrict_ctxt_op (set_to_flag x) ctxt))"
by (simp add: local.wf operationContext_wf_restrict_ctxt_op operationContext_wf_trans)
then have f5: "is_update Disable \<and> Op (restrict_ctxt_op (set_to_flag x) ctxt) (cca Disable (restrict_ctxt_op (set_to_flag x) ctxt)) \<triangleq> Disable \<and> (\<forall>c f. Op (restrict_ctxt_op (set_to_flag x) ctxt) c \<noteq> Some f \<or> is_query f \<or> (cca Disable (restrict_ctxt_op (set_to_flag x) ctxt), c) \<notin> happensBefore (restrict_ctxt_op (set_to_flag x) ctxt) \<or> f = Disable)"
by (metis (no_types, lifting) a3 f3 latestOps_alt wf')
obtain ccb :: "callId \<Rightarrow> callId" where
f6: "\<forall>c. Op ctxt c \<noteq> Some (Remove x) \<or> Op ctxt (ccb c) \<triangleq> Add x \<and> (c, ccb c) \<in> happensBefore ctxt"
using a1 by moura
obtain ss :: "flagOp \<Rightarrow> ('a setOp \<Rightarrow> flagOp option) \<Rightarrow> 'a setOp option \<Rightarrow> 'a setOp" where
"\<forall>x0 x1 x2. (\<exists>v3. x2 \<triangleq> v3 \<and> x1 v3 \<triangleq> x0) = (x2 \<triangleq> ss x0 x1 x2 \<and> x1 (ss x0 x1 x2) \<triangleq> x0)"
by moura
then have "Op ctxt (cca Disable (restrict_ctxt_op (set_to_flag x) ctxt)) \<triangleq> ss Disable (set_to_flag x) (Op ctxt (cca Disable (restrict_ctxt_op (set_to_flag x) ctxt))) \<and> set_to_flag x (ss Disable (set_to_flag x) (Op ctxt (cca Disable (restrict_ctxt_op (set_to_flag x) ctxt)))) \<triangleq> Disable"
using f5 by (simp add: Op_restrict_ctxt_op bind_eq_Some_conv)
then have "Op ctxt (cca Disable (restrict_ctxt_op (set_to_flag x) ctxt)) \<triangleq> Remove x"
by (metis set_to_flag_Disable)
then have "Op ctxt (ccb (cca Disable (restrict_ctxt_op (set_to_flag x) ctxt))) \<triangleq> Add x \<and> (cca Disable (restrict_ctxt_op (set_to_flag x) ctxt), ccb (cca Disable (restrict_ctxt_op (set_to_flag x) ctxt))) \<in> happensBefore ctxt"
using f6 by blast
then show ?thesis
using f5 by (metis (no_types) Op_restrict_ctxt_op bind.bind_lunit flagOp.distinct(1) flagOp.distinct(3) happensBefore_restrict_ctxt_op is_update_flagOp_def set_to_flag_Enable)
qed
qed
lemma set_rw_spec_Contains2:
assumes spec: "res = from_bool ((\<exists>a. Op ctxt a \<triangleq> Add x)
\<and> (\<forall>r. Op ctxt r \<triangleq> Remove x
\<longrightarrow> (\<exists>a. Op ctxt a \<triangleq> Add x
\<and> (r,a)\<in>happensBefore ctxt)))"
and wf: "operationContext_wf ctxt"
shows "set_rw_spec (Contains x) ctxt res"
proof (auto simp add: set_rw_spec_def set_spec_def flag_dw_spec_def spec intro!: arg_cong[where f=from_bool])
have wf': "operationContext_wf (restrict_ctxt_op (set_to_flag x) ctxt) "
by (simp add: local.wf operationContext_wf_restrict_ctxt_op)
show "Enable \<in> latestOps (restrict_ctxt_op (set_to_flag x) ctxt)"
if c0: "\<forall>r. Op ctxt r \<triangleq> Remove x \<longrightarrow> (\<exists>a. Op ctxt a \<triangleq> Add x \<and> (r, a) \<in> happensBefore ctxt)"
and c1: "Op ctxt a \<triangleq> Add x"
for a
by (rule latestOps_Enable''[OF wf'])
(use that in \<open>auto simp add: Op_restrict_ctxt_op_eq set_to_flag_Enable
set_to_flag_Disable happensBefore_restrict_ctxt_op' set_to_flag_None\<close>)
show "False"
if c0: "\<forall>r. Op ctxt r \<triangleq> Remove x \<longrightarrow> (\<exists>a. Op ctxt a \<triangleq> Add x \<and> (r, a) \<in> happensBefore ctxt)"
and c1: "Op ctxt a \<triangleq> Add x"
and c2: "Disable \<in> latestOps (restrict_ctxt_op (set_to_flag x) ctxt)"
for a
using that