-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathSnapshot.thy
5272 lines (5122 loc) · 251 KB
/
Snapshot.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 \<open>The Chandy--Lamport algorithm\<close>
theory Snapshot
imports
"HOL-Library.Sublist"
"HOL-Library.Permutation"
Distributed_System
Trace
Util
Swap
begin
subsection \<open>The computation locale\<close>
text \<open>We extend the distributed system locale presented
earlier: Now we are given a trace t of the distributed system between
two configurations, the initial and final configuartions of t. Our objective
is to show that the Chandy--Lamport algorithm terminated successfully and
exhibits the same properties as claimed in~\cite{chandy}. In the initial state
no snapshotting must have taken place yet, however the computation itself may
have progressed arbitrarily far already.
We assume that there exists at least one process, that the
total number of processes in the system is finite, and that there
are only finitely many channels between the processes. The process graph
is strongly connected. Finally there are Chandy and Lamport's core assumptions:
every process snapshots at some time and no marker may remain in a channel forever.\<close>
locale computation = distributed_system +
fixes
init final :: "('a, 'b, 'c) configuration"
assumes
finite_channels:
"finite {i. \<exists>p q. channel i = Some (p, q)}" and
strongly_connected_raw:
"\<forall>p q. (p \<noteq> q) \<longrightarrow>
(tranclp (\<lambda>p q. (\<exists>i. channel i = Some (p, q)))) p q" and
at_least_two_processes:
"card (UNIV :: 'a set) > 1" and
finite_processes:
"finite (UNIV :: 'a set)" and
no_initial_Marker:
"\<forall>i. (\<exists>p q. channel i = Some (p, q))
\<longrightarrow> Marker \<notin> set (msgs init i)" and
no_msgs_if_no_channel:
"\<forall>i. channel i = None \<longrightarrow> msgs init i = []" and
no_initial_process_snapshot:
"\<forall>p. ~ has_snapshotted init p" and
no_initial_channel_snapshot:
"\<forall>i. channel_snapshot init i = ([], NotStarted)" and
valid: "\<exists>t. trace init t final" and
l1: "\<forall>t i cid. trace init t final
\<and> Marker \<in> set (msgs (s init t i) cid)
\<longrightarrow> (\<exists>j. j \<ge> i \<and> Marker \<notin> set (msgs (s init t j) cid))" and
l2: "\<forall>t p. trace init t final
\<longrightarrow> (\<exists>i. has_snapshotted (s init t i) p \<and> i \<le> length t)"
begin
definition has_channel where
"has_channel p q \<longleftrightarrow> (\<exists>i. channel i = Some (p, q))"
lemmas strongly_connected = strongly_connected_raw[folded has_channel_def]
lemma exists_some_channel:
shows "\<exists>i p q. channel i = Some (p, q)"
proof -
obtain p q where "p : (UNIV :: 'a set) \<and> q : (UNIV :: 'a set) \<and> p \<noteq> q"
by (metis (mono_tags) One_nat_def UNIV_eq_I all_not_in_conv at_least_two_processes card_Suc_Diff1 card.empty finite_processes insert_iff iso_tuple_UNIV_I less_numeral_extra(4) n_not_Suc_n)
then have "(tranclp has_channel) p q" using strongly_connected by simp
then obtain r s where "has_channel r s"
by (meson tranclpD)
then show ?thesis using has_channel_def by auto
qed
abbreviation S where
"S \<equiv> s init"
lemma no_messages_if_no_channel:
assumes "trace init t final"
shows "channel cid = None \<Longrightarrow> msgs (s init t i) cid = []"
using no_messages_introduced_if_no_channel[OF assms no_msgs_if_no_channel] by blast
lemma S_induct [consumes 3, case_names S_init S_step]:
"\<lbrakk> trace init t final; i \<le> j; j \<le> length t;
\<And>i. P i i;
\<And>i j. i < j \<Longrightarrow> j \<le> length t \<Longrightarrow> (S t i) \<turnstile> (t ! i) \<mapsto> (S t (Suc i)) \<Longrightarrow> P (Suc i) j \<Longrightarrow> P i j
\<rbrakk> \<Longrightarrow> P i j"
proof (induct "j - i" arbitrary: i)
case 0
then show ?case by simp
next
case (Suc n)
then have "(S t i) \<turnstile> (t ! i) \<mapsto> (S t (Suc i))" using Suc step_Suc by simp
then show ?case using Suc by simp
qed
lemma exists_index:
assumes
"trace init t final" and
"ev \<in> set (take (j - i) (drop i t))"
shows
"\<exists>k. i \<le> k \<and> k < j \<and> ev = t ! k"
proof -
have "trace (S t i) (take (j - i) (drop i t)) (S t j)"
by (metis assms(1) assms(2) diff_is_0_eq' exists_trace_for_any_i_j list.distinct(1) list.set_cases nat_le_linear take_eq_Nil)
obtain l where "ev = (take (j - i) (drop i t)) ! l" "l < length (take (j - i) (drop i t))"
by (metis assms(2) in_set_conv_nth)
let ?k = "l + i"
have "(take (j - i) (drop i t)) ! l = drop i t ! l"
using \<open>l < length (take (j - i) (drop i t))\<close> by auto
also have "... = t ! ?k"
by (metis add.commute assms(2) drop_all empty_iff list.set(1) nat_le_linear nth_drop take_Nil)
finally have "ev = t ! ?k"
using \<open>ev = take (j - i) (drop i t) ! l\<close> by blast
moreover have "i \<le> ?k \<and> ?k < j"
using \<open>l < length (take (j - i) (drop i t))\<close> by auto
ultimately show ?thesis by blast
qed
lemma no_change_if_ge_length_t:
assumes
"trace init t final" and
"i \<ge> length t" and
"j \<ge> i"
shows
"S t i = S t j"
proof -
have "trace (S t i) (take (j - i) (drop i t)) (S t j)"
using assms(1) assms(3) exists_trace_for_any_i_j by blast
moreover have "(take (j - i) (drop i t)) = Nil"
by (simp add: assms(2))
ultimately show ?thesis
by (metis tr_init trace_and_start_determines_end)
qed
lemma no_marker_if_no_snapshot:
shows
"\<lbrakk> trace init t final; channel cid = Some (p, q);
~ has_snapshotted (S t i) p \<rbrakk>
\<Longrightarrow> Marker \<notin> set (msgs (S t i) cid)"
proof (induct i)
case 0
then show ?case
by (metis exists_trace_for_any_i no_initial_Marker take_eq_Nil tr_init trace_and_start_determines_end)
next
case (Suc n)
then have IH: "Marker \<notin> set (msgs (S t n) cid)"
by (meson distributed_system.exists_trace_for_any_i_j distributed_system.snapshot_stable_2 distributed_system_axioms eq_iff le_Suc_eq)
then obtain tr where decomp: "trace (S t n) tr (S t (Suc n))" "tr = take (Suc n - n) (drop n t)"
using Suc exists_trace_for_any_i_j le_Suc_eq by blast
have "Marker \<notin> set (msgs (S t (Suc n)) cid)"
proof (cases "tr = []")
case True
then show ?thesis
by (metis IH decomp(1) tr_init trace_and_start_determines_end)
next
case False
then obtain ev where step: "tr = [ev]" "(S t n) \<turnstile> ev \<mapsto> (S t (Suc n))"
by (metis One_nat_def Suc_eq_plus1 Suc_leI \<open>tr = take (Suc n - n) (drop n t)\<close> \<open>trace (S t n) tr (S t (Suc n))\<close> add_diff_cancel_left' append.simps(1) butlast_take cancel_comm_monoid_add_class.diff_cancel length_greater_0_conv list.distinct(1) list.sel(3) snoc_eq_iff_butlast take0 take_Nil trace.cases)
then show ?thesis
proof (cases ev)
case (Snapshot p')
then show ?thesis
by (metis IH Suc.prems(2) Suc.prems(3) local.step(2) new_Marker_in_set_implies_nonregular_occurence new_msg_in_set_implies_occurrence nonregular_event_induces_snapshot snapshot_state_unchanged)
next
case (RecvMarker cid' p' q')
have "p' \<noteq> p"
proof (rule ccontr)
assume asm: "~ p' \<noteq> p"
then have "has_snapshotted (S t (Suc n)) p"
proof -
have "~ regular_event ev" using RecvMarker by auto
moreover have "occurs_on ev = p" using asm RecvMarker by auto
ultimately show ?thesis using step(2) Suc.hyps Suc.prems
by (metis nonregular_event_induces_snapshot snapshot_state_unchanged)
qed
then show False using Suc.prems by blast
qed
moreover have "cid \<noteq> cid'"
proof (rule ccontr)
assume "~ cid \<noteq> cid'"
then have "hd (msgs (S t n) cid) = Marker \<and> length (msgs (S t n) cid) > 0"
using step RecvMarker can_occur_def by auto
then have "Marker : set (msgs (S t n) cid)"
using list.set_sel(1) by fastforce
then show False using IH by simp
qed
ultimately have "msgs (S t (Suc n)) cid = msgs (S t n) cid"
proof -
have "\<nexists>r. channel cid = Some (p', r)"
using Suc.prems(2) \<open>p' \<noteq> p\<close> by auto
with `cid \<noteq> cid'` RecvMarker step show ?thesis by (cases "has_snapshotted (S t n) p'", auto)
qed
then show ?thesis by (simp add: IH)
next
case (Trans p' s s')
then show ?thesis
using IH local.step(2) by force
next
case (Send cid' p' q' s s' m)
with step IH show ?thesis by (cases "cid' = cid", auto)
next
case (Recv cid' p' q' s s' m)
with step IH show ?thesis by (cases "cid' = cid", auto)
qed
qed
then show ?case by blast
qed
subsection \<open>Termination\<close>
text \<open>We prove that the snapshot algorithm terminates, as exhibited
by lemma \texttt{snapshot\_algorithm\_must\_terminate}. In the final configuration all
processes have snapshotted, and no markers remain in the channels.\<close>
lemma must_exist_snapshot:
assumes
"trace init t final"
shows
"\<exists>p i. Snapshot p = t ! i"
proof (rule ccontr)
assume "\<nexists>p i. Snapshot p = t ! i"
have "\<forall>i p. ~ has_snapshotted (S t i) p"
proof (rule allI)
fix i
show "\<forall>p. ~ has_snapshotted (S t i) p"
proof (induct i)
case 0
then show ?case
by (metis assms distributed_system.trace_and_start_determines_end distributed_system_axioms exists_trace_for_any_i computation.no_initial_process_snapshot computation_axioms take0 tr_init)
next
case (Suc n)
then have IH: "\<forall>p. ~ has_snapshotted (S t n) p" by auto
then obtain tr where "trace (S t n) tr (S t (Suc n))" "tr = take (Suc n - n) (drop n t)"
using assms exists_trace_for_any_i_j le_Suc_eq by blast
show "\<forall>p. ~ has_snapshotted (S t (Suc n)) p"
proof (cases "tr = []")
case True
then show ?thesis
by (metis IH \<open>trace (S t n) tr (S t (Suc n))\<close> tr_init trace_and_start_determines_end)
next
case False
then obtain ev where step: "tr = [ev]" "(S t n) \<turnstile> ev \<mapsto> (S t (Suc n))"
by (metis One_nat_def Suc_eq_plus1 Suc_leI \<open>tr = take (Suc n - n) (drop n t)\<close> \<open>trace (S t n) tr (S t (Suc n))\<close> add_diff_cancel_left' append.simps(1) butlast_take cancel_comm_monoid_add_class.diff_cancel length_greater_0_conv list.distinct(1) list.sel(3) snoc_eq_iff_butlast take0 take_Nil trace.cases)
then show ?thesis
using step Suc.hyps proof (cases ev)
case (Snapshot q)
then show ?thesis
by (metis \<open>\<nexists>p i. Snapshot p = t ! i\<close> \<open>tr = [ev]\<close> \<open>tr = take (Suc n - n) (drop n t)\<close> append_Cons append_take_drop_id nth_append_length)
next
case (RecvMarker cid' q r)
then have m: "Marker \<in> set (msgs (S t n) cid')"
using RecvMarker_implies_Marker_in_set step by blast
have "~ has_snapshotted (S t n) q" using Suc by auto
then have "Marker \<notin> set (msgs (S t n) cid')"
proof -
have "channel cid' = Some (r, q)" using step can_occur_def RecvMarker by auto
then show ?thesis
using IH assms no_marker_if_no_snapshot by blast
qed
then show ?thesis using m by auto
qed auto
qed
qed
qed
obtain j p where "has_snapshotted (S t j) p" using l2 assms by blast
then show False
using \<open>\<forall>i p. \<not> has_snapshotted (S t i) p\<close> by blast
qed
lemma recv_marker_means_snapshotted:
assumes
"trace init t final" and
"ev = RecvMarker cid p q" and
"(S t i) \<turnstile> ev \<mapsto> (S t (Suc i))"
shows
"has_snapshotted (S t i) q"
proof -
have "Marker = hd (msgs (S t i) cid) \<and> length (msgs (S t i) cid) > 0"
proof -
have "Marker # msgs (S t (Suc i)) cid = msgs (S t i) cid"
using assms(2) assms(3) next_recv_marker by blast
then show ?thesis
by (metis length_greater_0_conv list.discI list.sel(1))
qed
then have "Marker \<in> set (msgs (S t i) cid)"
using hd_in_set by fastforce
then show "has_snapshotted (S t i) q"
proof -
have "channel cid = Some (q, p)" using assms can_occur_def by auto
then show ?thesis
using \<open>Marker \<in> set (msgs (S t i) cid)\<close> assms(1) no_marker_if_no_snapshot by blast
qed
qed
lemma recv_marker_means_cs_Done:
assumes
"trace init t final" and
"t ! i = RecvMarker cid p q" and
"i < length t"
shows
"snd (cs (S t (i+1)) cid) = Done"
proof -
have "(S t i) \<turnstile> (t ! i) \<mapsto> (S t (i+1))"
using assms(1) assms(3) step_Suc by auto
then show ?thesis
by (simp add: assms(2))
qed
lemma snapshot_produces_marker:
assumes
"trace init t final" and
"~ has_snapshotted (S t i) p" and
"has_snapshotted (S t (Suc i)) p" and
"channel cid = Some (p, q)"
shows
"Marker : set (msgs (S t (Suc i)) cid) \<or> has_snapshotted (S t i) q"
proof -
obtain ev where ex_ev: "(S t i) \<turnstile> ev \<mapsto> (S t (Suc i))"
by (metis append_Nil2 append_take_drop_id assms(1) assms(2) assms(3) distributed_system.step_Suc distributed_system_axioms drop_eq_Nil less_Suc_eq_le nat_le_linear not_less_eq s_def)
then have "occurs_on ev = p"
using assms(2) assms(3) no_state_change_if_no_event by force
then show ?thesis
using assms ex_ev proof (cases ev)
case (Snapshot r)
then have "Marker \<in> set (msgs (S t (Suc i)) cid)"
using ex_ev assms(2) assms(3) assms(4) by fastforce
then show ?thesis by simp
next
case (RecvMarker cid' r s)
have "r = p" using `occurs_on ev = p`
by (simp add: RecvMarker)
then show ?thesis
proof (cases "cid = cid'")
case True
then have "has_snapshotted (S t i) q"
using RecvMarker RecvMarker_implies_Marker_in_set assms(1) assms(2) assms(4) ex_ev no_marker_if_no_snapshot by blast
then show ?thesis by simp
next
case False
then have "\<exists>s. channel cid = Some (r, s)" using RecvMarker assms can_occur_def `r = p` by simp
then have "msgs (S t (Suc i)) cid = msgs (S t i) cid @ [Marker]"
using RecvMarker assms ex_ev `r = p` False by simp
then show ?thesis by simp
qed
qed auto
qed
lemma exists_snapshot_for_all_p:
assumes
"trace init t final"
shows
"\<exists>i. ~ has_snapshotted (S t i) p \<and> has_snapshotted (S t (Suc i)) p" (is ?Q)
proof -
obtain i where "has_snapshotted (S t i) p" using l2 assms by blast
let ?j = "LEAST j. has_snapshotted (S t j) p"
have "?j \<noteq> 0"
proof -
have "~ has_snapshotted (S t 0) p"
by (metis exists_trace_for_any_i list.discI no_initial_process_snapshot s_def take_eq_Nil trace.simps)
then show ?thesis
by (metis (mono_tags, lifting) \<open>has_snapshotted (S t i) p\<close> wellorder_Least_lemma(1))
qed
have "?j \<le> i"
by (meson Least_le \<open>has_snapshotted (S t i) p\<close>)
have "\<not> has_snapshotted (S t (?j - 1)) p" (is ?P)
proof (rule ccontr)
assume "\<not> ?P"
then have "has_snapshotted (S t (?j - 1)) p" by simp
then have "\<exists>j. j < ?j \<and> has_snapshotted (S t j) p"
by (metis One_nat_def \<open>(LEAST j. ps (S t j) p \<noteq> None) \<noteq> 0\<close> diff_less lessI not_gr_zero)
then show False
using not_less_Least by blast
qed
show ?thesis
proof (rule ccontr)
assume "\<not> ?Q"
have "\<forall>i. \<not> has_snapshotted (S t i) p"
proof (rule allI)
fix i'
show "\<not> has_snapshotted (S t i') p"
proof (induct i')
case 0
then show ?case
using \<open>(LEAST j. ps (S t j) p \<noteq> None) \<noteq> 0\<close> by force
next
case (Suc i'')
then show ?case
using \<open>\<nexists>i. \<not> ps (S t i) p \<noteq> None \<and> ps (S t (Suc i)) p \<noteq> None\<close> by blast
qed
qed
then show False
using \<open>ps (S t i) p \<noteq> None\<close> by blast
qed
qed
lemma all_processes_snapshotted_in_final_state:
assumes
"trace init t final"
shows
"has_snapshotted final p"
proof -
obtain i where "has_snapshotted (S t i) p \<and> i \<le> length t"
using assms l2 by blast
moreover have "final = (S t (length t))"
by (metis (no_types, lifting) assms exists_trace_for_any_i le_Suc_eq length_Cons take_Nil take_all trace.simps trace_and_start_determines_end)
ultimately show ?thesis
using assms exists_trace_for_any_i_j snapshot_stable by blast
qed
definition next_marker_free_state where
"next_marker_free_state t i cid = (LEAST j. j \<ge> i \<and> Marker \<notin> set (msgs (S t j) cid))"
lemma exists_next_marker_free_state:
assumes
"channel cid = Some (p, q)"
"trace init t final"
shows
"\<exists>!j. next_marker_free_state t i cid = j \<and> j \<ge> i \<and> Marker \<notin> set (msgs (S t j) cid)"
proof (cases "Marker \<in> set (msgs (S t i) cid)")
case False
then have "next_marker_free_state t i cid = i" unfolding next_marker_free_state_def
by (metis (no_types, lifting) Least_equality order_refl)
then show ?thesis using False assms by blast
next
case True
then obtain j where "j \<ge> i" "Marker \<notin> set (msgs (S t j) cid)" using l1 assms by blast
then show ?thesis
by (metis (no_types, lifting) LeastI_ex next_marker_free_state_def)
qed
theorem snapshot_algorithm_must_terminate:
assumes
"trace init t final"
shows
"\<exists>phi. ((\<forall>p. has_snapshotted (S t phi) p)
\<and> (\<forall>cid. Marker \<notin> set (msgs (S t phi) cid)))"
proof -
let ?i = "{i. i \<le> length t \<and> (\<forall>p. has_snapshotted (S t i) p)}"
have fin_i: "finite ?i" by auto
moreover have "?i \<noteq> empty"
proof -
have "\<forall>p. has_snapshotted (S t (length t)) p"
by (meson assms exists_trace_for_any_i_j l2 snapshot_stable_2)
then show ?thesis by blast
qed
then obtain i where asm: "\<forall>p. has_snapshotted (S t i) p" by blast
have f: "\<forall>j. j \<ge> i \<longrightarrow> (\<forall>p. has_snapshotted (S t j) p)"
using snapshot_stable asm exists_trace_for_any_i_j valid assms by blast
let ?s = "(\<lambda>cid. (next_marker_free_state t i cid)) ` { cid. channel cid \<noteq> None }"
have "?s \<noteq> empty" using exists_some_channel by auto
have fin_s: "finite ?s" using finite_channels by simp
let ?phi = "Max ?s"
have "?phi \<ge> i"
proof (rule ccontr)
assume asm: "\<not> ?phi \<ge> i"
obtain cid p q where g: "channel cid = Some (p, q)" using exists_some_channel by auto
then have "next_marker_free_state t i cid \<ge> i" using exists_next_marker_free_state assms by blast
then have "Max ?s \<ge> i" using Max_ge_iff g fin_s by fast
then show False using asm by simp
qed
then have "\<And>cid. Marker \<notin> set (msgs (S t ?phi) cid)"
proof -
fix cid
show "Marker \<notin> set (msgs (S t ?phi) cid)"
proof (cases "Marker : set (msgs (S t i) cid)")
case False
then show ?thesis
using \<open>i \<le> Max ?s\<close> asm assms exists_trace_for_any_i_j no_markers_if_all_snapshotted by blast
next
case True
then have cpq: "channel cid \<noteq> None" using no_messages_if_no_channel assms by fastforce
then obtain p q where chan: "channel cid = Some (p, q)" by auto
then obtain j where i: "j = next_marker_free_state t i cid" "Marker \<notin> set (msgs (S t j) cid)"
using exists_next_marker_free_state assms by fast
have "j \<le> ?phi" using cpq fin_s i(1) pair_imageI by simp
then show "Marker \<notin> set (msgs (S t ?phi) cid)"
proof -
have "trace (S t j) (take (?phi - j) (drop j t)) (S t ?phi)"
using \<open>j \<le> ?phi\<close> assms exists_trace_for_any_i_j by blast
moreover have "\<forall>p. has_snapshotted (S t j) p"
by (metis assms chan f computation.exists_next_marker_free_state computation_axioms i(1))
ultimately show ?thesis
using i(2) no_markers_if_all_snapshotted by blast
qed
qed
qed
thus ?thesis using f `?phi \<ge> i` by blast
qed
subsection \<open>Correctness\<close>
text \<open>The greatest part of this work is spent on the correctness
of the Chandy-Lamport algorithm. We prove that the snapshot is
consistent, i.e.\ there exists a permutation $t'$ of the trace $t$ and an intermediate
configuration $c'$ of $t'$ such that the configuration recorded in the snapshot
corresponds to the snapshot taken during execution of $t$, which is given as Theorem 1
in~\cite{chandy}.\<close>
lemma snapshot_stable_ver_2:
shows "trace init t final \<Longrightarrow> has_snapshotted (S t i) p \<Longrightarrow> j \<ge> i \<Longrightarrow> has_snapshotted (S t j) p"
using exists_trace_for_any_i_j snapshot_stable by blast
lemma snapshot_stable_ver_3:
shows "trace init t final \<Longrightarrow> ~ has_snapshotted (S t i) p \<Longrightarrow> i \<ge> j \<Longrightarrow> ~ has_snapshotted (S t j) p"
using snapshot_stable_ver_2 by blast
lemma marker_must_stay_if_no_snapshot:
assumes
"trace init t final" and
"has_snapshotted (S t i) p" and
"~ has_snapshotted (S t i) q" and
"channel cid = Some (p, q)"
shows
"Marker : set (msgs (S t i) cid)"
proof -
obtain j where "~ has_snapshotted (S t j) p \<and> has_snapshotted (S t (Suc j)) p"
using exists_snapshot_for_all_p assms by blast
have "j \<le> i"
proof (rule ccontr)
assume asm: "~ j \<le> i"
then have "~ has_snapshotted (S t i) p"
using \<open>\<not> has_snapshotted (S t j) p \<and> has_snapshotted (S t (Suc j)) p\<close> assms(1) less_imp_le_nat snapshot_stable_ver_3
by (meson nat_le_linear)
then show False using assms(2) by simp
qed
have "i \<le> length t"
proof (rule ccontr)
assume "~ i \<le> length t"
then have "i > length t"
using not_less by blast
obtain i' where a: "\<forall>p. has_snapshotted (S t i') p" using assms snapshot_algorithm_must_terminate by blast
have "i' \<ge> i"
using \<open>\<forall>p. has_snapshotted (S t i') p\<close> assms(1) assms(3) nat_le_linear snapshot_stable_ver_3 by blast
have "(S t i') \<noteq> (S t i)" using assms a by force
then have "i \<le> length t"
using \<open>i \<le> i'\<close> assms(1) computation.no_change_if_ge_length_t computation_axioms nat_le_linear by fastforce
then show False using `~ i \<le> length t` by simp
qed
have marker_in_set: "Marker : set (msgs (S t (Suc j)) cid)"
using \<open>\<not> has_snapshotted (S t j) p \<and> has_snapshotted (S t (Suc j)) p\<close> \<open>j \<le> i\<close> assms(1) assms(3) assms(4) snapshot_produces_marker snapshot_stable_ver_3 by blast
show ?thesis
proof (rule ccontr)
assume asm: "Marker \<notin> set (msgs (S t i) cid)"
then have range: "(Suc j) < i"
by (metis Suc_lessI \<open>\<not> ps (S t j) p \<noteq> None \<and> ps (S t (Suc j)) p \<noteq> None\<close> \<open>j \<le> i\<close> assms(2) marker_in_set order.order_iff_strict)
let ?k = "LEAST k. k \<ge> (Suc j) \<and> Marker \<notin> set (msgs (S t k) cid)"
have range_k: "(Suc j) < ?k \<and> ?k \<le> i"
proof -
have "j < (LEAST n. Suc j \<le> n \<and> Marker \<notin> set (msgs (S t n) cid))"
by (metis (full_types) Suc_le_eq assms(1) assms(4) exists_next_marker_free_state next_marker_free_state_def)
then show ?thesis
proof -
assume a1: "j < (LEAST n. Suc j \<le> n \<and> Marker \<notin> set (msgs (S t n) cid))"
have "j < i"
using local.range by linarith (* 4 ms *)
then have "(Suc j \<le> i \<and> Marker \<notin> set (msgs (S t i) cid)) \<and> (LEAST n. Suc j \<le> n \<and> Marker \<notin> set (msgs (S t n) cid)) \<noteq> Suc j"
by (metis (lifting) Suc_leI asm marker_in_set wellorder_Least_lemma(1)) (* 64 ms *)
then show ?thesis
using a1 by (simp add: wellorder_Least_lemma(2)) (* 16 ms *)
qed
qed
have a: "Marker : set (msgs (S t (?k-1)) cid)"
proof -
obtain nn :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
"\<forall>x0 x1. (\<exists>v2. x0 = Suc (x1 + v2)) = (x0 = Suc (x1 + nn x0 x1))"
by moura
then have f1: "(LEAST n. Suc j \<le> n \<and> Marker \<notin> set (msgs (S t n) cid)) = Suc (Suc j + nn (LEAST n. Suc j \<le> n \<and> Marker \<notin> set (msgs (S t n) cid)) (Suc j))"
using \<open>Suc j < (LEAST k. Suc j \<le> k \<and> Marker \<notin> set (msgs (S t k) cid)) \<and> (LEAST k. Suc j \<le> k \<and> Marker \<notin> set (msgs (S t k) cid)) \<le> i\<close> less_iff_Suc_add by fastforce
have f2: "Suc j \<le> Suc j + nn (LEAST n. Suc j \<le> n \<and> Marker \<notin> set (msgs (S t n) cid)) (Suc j)"
by simp
have f3: "\<forall>p n. \<not> p (n::nat) \<or> Least p \<le> n"
by (meson wellorder_Least_lemma(2))
have "\<not> (LEAST n. Suc j \<le> n \<and> Marker \<notin> set (msgs (S t n) cid)) \<le> Suc j + nn (LEAST n. Suc j \<le> n \<and> Marker \<notin> set (msgs (S t n) cid)) (Suc j)"
using f1 by linarith
then have f4: "\<not> (Suc j \<le> Suc j + nn (LEAST n. Suc j \<le> n \<and> Marker \<notin> set (msgs (S t n) cid)) (Suc j) \<and> Marker \<notin> set (msgs (S t (Suc j + nn (LEAST n. Suc j \<le> n \<and> Marker \<notin> set (msgs (S t n) cid)) (Suc j))) cid))"
using f3 by force
have "Suc j + nn (LEAST n. Suc j \<le> n \<and> Marker \<notin> set (msgs (S t n) cid)) (Suc j) = (LEAST n. Suc j \<le> n \<and> Marker \<notin> set (msgs (S t n) cid)) - 1"
using f1 by linarith
then show ?thesis
using f4 f2 by presburger
qed
have b: "Marker \<notin> set (msgs (S t ?k) cid)"
using assms(1) assms(4) exists_next_marker_free_state next_marker_free_state_def by fastforce
have "?k - 1 < i" using range_k by auto
then obtain ev where step: "(S t (?k-1)) \<turnstile> ev \<mapsto> (S t (Suc (?k-1)))"
by (meson Suc_le_eq \<open>i \<le> length t\<close> assms(1) le_trans step_Suc)
then show False
using a assms(1) assms(3) assms(4) b computation.snapshot_stable_ver_3 computation_axioms less_iff_Suc_add range_k recv_marker_means_snapshotted_2 by fastforce
qed
qed
subsubsection \<open>Pre- and postrecording events\<close>
definition prerecording_event:
"prerecording_event t i \<equiv>
i < length t \<and> regular_event (t ! i)
\<and> ~ has_snapshotted (S t i) (occurs_on (t ! i))"
definition postrecording_event:
"postrecording_event t i \<equiv>
i < length t \<and> regular_event (t ! i)
\<and> has_snapshotted (S t i) (occurs_on (t ! i))"
abbreviation neighboring where
"neighboring t i j \<equiv> i < j \<and> j < length t \<and> regular_event (t ! i) \<and> regular_event (t ! j)
\<and> (\<forall>k. i < k \<and> k < j \<longrightarrow> ~ regular_event (t ! k))"
lemma pre_if_regular_and_not_post:
assumes
"regular_event (t ! i)" and
"~ postrecording_event t i" and
"i < length t"
shows
"prerecording_event t i"
using assms computation.postrecording_event computation_axioms prerecording_event by metis
lemma post_if_regular_and_not_pre:
assumes
"regular_event (t ! i)" and
"~ prerecording_event t i" and
"i < length t"
shows
"postrecording_event t i"
using assms computation.postrecording_event computation_axioms prerecording_event by metis
lemma post_before_pre_different_processes:
assumes
"i < j" and
"j < length t" and
neighboring: "\<forall>k. (i < k \<and> k < j) \<longrightarrow> ~ regular_event (t ! k)" and
post_ei: "postrecording_event t i" and
pre_ej: "prerecording_event t j" and
valid: "trace init t final"
shows
"occurs_on (t ! i) \<noteq> occurs_on (t ! j)"
proof -
let ?p = "occurs_on (t ! i)"
let ?q = "occurs_on (t ! j)"
have sp: "has_snapshotted (S t i) ?p"
using assms postrecording_event prerecording_event by blast
have nsq: "~ has_snapshotted (S t j) ?q"
using assms postrecording_event prerecording_event by blast
show "?p \<noteq> ?q"
proof -
have "~ has_snapshotted (S t i) ?q"
proof (rule ccontr)
assume sq: "~ ~ has_snapshotted (S t i) ?q"
from `i < j` have "i \<le> j" using less_imp_le by blast
then obtain tr where ex_trace: "trace (S t i) tr (S t j)"
using exists_trace_for_any_i_j valid by blast
then have "has_snapshotted (S t j) ?q" using ex_trace snapshot_stable sq by blast
then show False using nsq by simp
qed
then show ?thesis using sp by auto
qed
qed
lemma post_before_pre_neighbors:
assumes
"i < j" and
"j < length t" and
neighboring: "\<forall>k. (i < k \<and> k < j) \<longrightarrow> ~ regular_event (t ! k)" and
post_ei: "postrecording_event t i" and
pre_ej: "prerecording_event t j" and
valid: "trace init t final"
shows
"Ball (set (take (j - (i+1)) (drop (i+1) t))) (%ev. ~ regular_event ev \<and> ~ occurs_on ev = occurs_on (t ! j))"
proof -
let ?p = "occurs_on (t ! i)"
let ?q = "occurs_on (t ! j)"
let ?between = "take (j - (i+1)) (drop (i+1) t)"
show ?thesis
proof (unfold Ball_def, rule allI, rule impI)
fix ev
assume "ev : set ?between"
have len_nr: "length ?between = (j - (i+1))" using assms(2) by auto
then obtain l where "?between ! l = ev" and range_l: "0 \<le> l \<and> l < (j - (i+1))"
by (metis \<open>ev \<in> set (take (j - (i + 1)) (drop (i + 1) t))\<close> gr_zeroI in_set_conv_nth le_numeral_extra(3) less_le)
let ?k = "l + (i+1)"
have "?between ! l = (t ! ?k)"
proof -
have "j < length t"
by (metis assms(2))
then show ?thesis
by (metis (no_types) Suc_eq_plus1 Suc_leI add.commute assms(1) drop_take length_take less_diff_conv less_imp_le_nat min.absorb2 nth_drop nth_take range_l)
qed
have "~ regular_event ev"
by (metis (no_types, lifting) assms(3) range_l One_nat_def Suc_eq_plus1 \<open>take (j - (i + 1)) (drop (i + 1) t) ! l = ev\<close> \<open>take (j - (i + 1)) (drop (i + 1) t) ! l = t ! (l + (i + 1))\<close> add.left_commute add_lessD1 lessI less_add_same_cancel2 less_diff_conv order_le_less)
have step_ev: "(S t ?k) \<turnstile> ev \<mapsto> (S t (?k+1))"
proof -
have "j \<le> length t"
by (metis assms(2) less_or_eq_imp_le)
then have "l + (i + 1) < length t"
by (meson less_diff_conv less_le_trans range_l)
then show ?thesis
by (metis (no_types) Suc_eq_plus1 \<open>take (j - (i + 1)) (drop (i + 1) t) ! l = ev\<close> \<open>take (j - (i + 1)) (drop (i + 1) t) ! l = t ! (l + (i + 1))\<close> distributed_system.step_Suc distributed_system_axioms valid)
qed
obtain cid s r where f: "ev = RecvMarker cid s r \<or> ev = Snapshot r" using `~ regular_event ev`
by (meson isRecvMarker_def isSnapshot_def nonregular_event)
from f have "occurs_on ev \<noteq> ?q"
proof (elim disjE)
assume snapshot: "ev = Snapshot r"
show ?thesis
proof (rule ccontr)
assume occurs_on_q: "~ occurs_on ev \<noteq> ?q"
then have "?q = r" using snapshot by auto
then have q_snapshotted: "has_snapshotted (S t (?k+1)) ?q"
using snapshot step_ev by auto
then show False
proof -
have "l + (i + 1) < j"
by (meson less_diff_conv range_l)
then show ?thesis
by (metis (no_types) Suc_eq_plus1 Suc_le_eq computation.snapshot_stable_ver_2 computation_axioms pre_ej prerecording_event q_snapshotted valid)
qed
qed
next
assume RecvMarker: "ev = RecvMarker cid s r"
show ?thesis
proof (rule ccontr)
assume occurs_on_q: "~ occurs_on ev \<noteq> ?q"
then have "s = ?q" using RecvMarker by auto
then have q_snapshotted: "has_snapshotted (S t (?k+1)) ?q"
proof (cases "has_snapshotted (S t ?k) ?q")
case True
then show ?thesis using snapshot_stable_ver_2 step_Suc step_ev valid by auto
next
case False
then show "has_snapshotted (S t (?k+1)) ?q"
using \<open>s = ?q\<close> next_recv_marker RecvMarker step_ev by auto
qed
then show False
proof -
have "l + (i + 1) < j"
using less_diff_conv range_l by blast
then show ?thesis
by (metis (no_types) Suc_eq_plus1 Suc_le_eq computation.snapshot_stable_ver_2 computation_axioms pre_ej prerecording_event q_snapshotted valid)
qed
qed
qed
then show "\<not> regular_event ev \<and> occurs_on ev \<noteq> ?q"
using `~ regular_event ev` by simp
qed
qed
lemma can_swap_neighboring_pre_and_postrecording_events:
assumes
"i < j" and
"j < length t" and
"occurs_on (t ! i) = p" and
"occurs_on (t ! j) = q" and
neighboring: "\<forall>k. (i < k \<and> k < j)
\<longrightarrow> ~ regular_event (t ! k)" and
post_ei: "postrecording_event t i" and
pre_ej: "prerecording_event t j" and
valid: "trace init t final"
shows
"can_occur (t ! j) (S t i)"
proof -
have "p \<noteq> q" using post_before_pre_different_processes assms by auto
have sp: "has_snapshotted (S t i) p"
using assms(3) post_ei postrecording_event prerecording_event by blast
have nsq: "~ has_snapshotted (S t j) q"
using assms(4) pre_ej prerecording_event by auto
let ?nr = "take (j - (Suc i)) (drop (Suc i) t)"
have valid_subtrace: "trace (S t (Suc i)) ?nr (S t j)"
using assms(1) exists_trace_for_any_i_j valid by fastforce
have "Ball (set ?nr) (%ev. ~ occurs_on ev = q \<and> ~ regular_event ev)"
proof -
have "?nr = take (j - (i+1)) (drop (i+1) t)" by auto
then show ?thesis
by (metis assms(1) assms(2) assms(4) neighboring post_ei pre_ej valid post_before_pre_neighbors)
qed
then have la: "list_all (%ev. ~ occurs_on ev = q) ?nr"
by (meson list_all_length nth_mem)
have tj_to_tSi: "can_occur (t ! j) (S t (Suc i))"
proof -
have "list_all (%ev. ~ isSend ev) ?nr"
proof -
have "list_all (%ev. ~ regular_event ev) ?nr"
using \<open>\<forall>ev\<in>set (take (j - (Suc i)) (drop (Suc i) t)). occurs_on ev \<noteq> q \<and> \<not> regular_event ev\<close> \<open>list_all (\<lambda>ev. occurs_on ev \<noteq> q) (take (j - (Suc i)) (drop (Suc i) t))\<close> list.pred_mono_strong by fastforce
then show ?thesis
by (simp add: list.pred_mono_strong)
qed
moreover have "~ isRecvMarker (t ! j)" using prerecording_event assms by auto
moreover have "can_occur (t ! j) (S t j)"
proof -
have "(S t j) \<turnstile> (t ! j) \<mapsto> (S t (Suc j))"
using assms(2) step_Suc valid by auto
then show ?thesis
using happen_implies_can_occur by blast
qed
ultimately show "can_occur (t ! j) (S t (Suc i))"
using assms(4) event_can_go_back_if_no_sender_trace valid_subtrace la by blast
qed
show "can_occur (t ! j) (S t i)"
proof (cases "isSend (t ! i)")
case False
have "~ isRecvMarker (t ! j)" using assms prerecording_event by auto
moreover have "~ isSend (t ! i)" using False by simp
ultimately show ?thesis
by (metis \<open>p \<noteq> q\<close> assms(3) assms(4) event_can_go_back_if_no_sender post_ei postrecording_event step_Suc tj_to_tSi valid)
next
case True
obtain cid s u u' m where Send: "t ! i = Send cid p s u u' m"
by (metis True isSend_def assms(3) event.sel(2))
have chan: "channel cid = Some (p, s)"
proof -
have "can_occur (t ! i) (S t i)"
by (meson computation.postrecording_event computation_axioms happen_implies_can_occur post_ei step_Suc valid)
then show ?thesis using can_occur_def Send by simp
qed
have n: "(S t i) \<turnstile> (t ! i) \<mapsto> (S t (Suc i))"
using assms(1) assms(2) step_Suc valid True by auto
have st: "states (S t i) q = states (S t (Suc i)) q"
using Send \<open>p \<noteq> q\<close> n by auto
have "isTrans (t ! j) \<or> isSend (t ! j) \<or> isRecv (t ! j)"
using assms(7) computation.prerecording_event computation_axioms regular_event by blast
then show ?thesis
proof (elim disjE)
assume "isTrans (t ! j)"
then show ?thesis
by (metis (no_types, lifting) tj_to_tSi st can_occur_def assms(4) event.case(1) event.collapse(1))
next
assume "isSend (t ! j)"
then obtain cid' s' u'' u''' m' where Send: "t ! j = Send cid' q s' u'' u''' m'"
by (metis (no_types, lifting) assms(4) event.sel(2) isSend_def)
have co_tSi: "can_occur (Send cid' q s' u'' u''' m') (S t (Suc i))"
using Send tj_to_tSi by auto
then have "channel cid' = Some (q, s') \<and> send cid' q s' u'' u''' m'"
using Send can_occur_def by simp
then show ?thesis using can_occur_def st Send assms co_tSi by auto
next
assume "isRecv (t ! j)"
then obtain cid' s' u'' u''' m' where Recv: "t ! j = Recv cid' q s' u'' u''' m'"
by (metis assms(4) event.sel(3) isRecv_def)
have co_tSi: "can_occur (Recv cid' q s' u'' u''' m') (S t (Suc i))"
using Recv tj_to_tSi by auto
then have a: "channel cid' = Some (s', q) \<and> length (msgs (S t (Suc i)) cid') > 0
\<and> hd (msgs (S t (Suc i)) cid') = Msg m'"
using can_occur_def co_tSi by fastforce
show "can_occur (t ! j) (S t i)"
proof (cases "cid = cid'")
case False
with Send n have "msgs (S t (Suc i)) cid' = msgs (S t i) cid'" by auto
then have b: "length (msgs (S t i) cid') > 0 \<and> hd (msgs (S t i) cid') = Msg m'"
using a by simp
with can_occur_Recv co_tSi st a Recv show ?thesis
unfolding can_occur_def by auto
next
case True (* This is the interesting case *)
have stu: "states (S t i) q = u''"
using can_occur_Recv co_tSi st by blast
show ?thesis
proof (rule ccontr)
have marker_in_set: "Marker \<in> set (msgs (S t i) cid)"
proof -
have "(s', q) = (p, q)"
using True a chan by auto
then show ?thesis
by (metis (no_types, lifting) True \<open>p \<noteq> q\<close> a assms(3) marker_must_stay_if_no_snapshot n no_state_change_if_no_event nsq snapshot_stable_2 sp valid valid_subtrace)
qed
assume asm: "~ can_occur (t ! j) (S t i)"
then show False
proof (unfold can_occur_def, (auto simp add: marker_in_set True Recv stu))
assume "msgs (S t i) cid' = []"
then show False using marker_in_set
by (simp add: True)
next
assume "hd (msgs (S t i) cid') \<noteq> Msg m'"
have "msgs (S t i) cid \<noteq> []" using marker_in_set by auto
then have "msgs (S t (Suc i)) cid = msgs (S t i) cid @ [Msg m]"
using Send True n chan by auto
then have "hd (msgs (S t (Suc i)) cid) \<noteq> Msg m'"
using True \<open>hd (msgs (S t i) cid') \<noteq> Msg m'\<close> \<open>msgs (S t i) cid \<noteq> []\<close> by auto
then have "~ can_occur (t ! j) (S t (Suc i))"
using True a by blast
then show False
using tj_to_tSi by blast
next
assume "~ recv cid' q s' u'' u''' m'"
then show False
using can_occur_Recv co_tSi by blast
next
assume "channel cid' \<noteq> Some (s', q)"
then show False using can_occur_def tj_to_tSi Recv by simp
qed
qed
qed
qed
qed
qed
subsubsection \<open>Event swapping\<close>
lemma swap_events:
shows "\<lbrakk> i < j; j < length t;
\<forall>k. (i < k \<and> k < j) \<longrightarrow> ~ regular_event (t ! k);
postrecording_event t i; prerecording_event t j;
trace init t final \<rbrakk>
\<Longrightarrow> trace init (swap_events i j t) final
\<and> (\<forall>k. k \<ge> j + 1 \<longrightarrow> S (swap_events i j t) k = S t k)
\<and> (\<forall>k. k \<le> i \<longrightarrow> S (swap_events i j t) k = S t k)
\<and> prerecording_event (swap_events i j t) i
\<and> postrecording_event (swap_events i j t) (i+1)
\<and> (\<forall>k. k > i+1 \<and> k < j+1
\<longrightarrow> ~ regular_event ((swap_events i j t) ! k))"
proof (induct "j - (i+1)" arbitrary: j t)
case 0
let ?p = "occurs_on (t ! i)"
let ?q = "occurs_on (t ! j)"
have "j = (i+1)"
using "0.prems" "0.hyps" by linarith
let ?subt = "take (j - (i+1)) (drop (i+1) t)"
have "t = take i t @ [t ! i] @ ?subt @ [t ! j] @ drop (j+1) t"
proof -
have "take (Suc i) t = take i t @ [t ! i]"
using "0.prems"(2) \<open>j = i + 1\<close> add_lessD1 take_Suc_conv_app_nth by blast
then show ?thesis
by (metis (no_types) "0.hyps" "0.prems"(2) Suc_eq_plus1 \<open>j = i + 1\<close> append_assoc append_take_drop_id self_append_conv2 take_Suc_conv_app_nth take_eq_Nil)
qed
have sp: "has_snapshotted (S t i) ?p"
using "0.prems" postrecording_event prerecording_event by blast
have nsq: "~ has_snapshotted (S t j) ?q"
using "0.prems" postrecording_event prerecording_event by blast
have "?p \<noteq> ?q"
using "0.prems" computation.post_before_pre_different_processes computation_axioms by blast
have "?subt = Nil"
by (simp add: \<open>j = i + 1\<close>)
have reg_step_1: "(S t i) \<turnstile> (t ! i) \<mapsto> (S t j)"
by (metis "0.prems"(2) "0.prems"(6) Suc_eq_plus1 \<open>j = i + 1\<close> add_lessD1 step_Suc)
have reg_step_2: "(S t j) \<turnstile> (t ! j) \<mapsto> (S t (j+1))"
using "0.prems"(2) "0.prems"(6) step_Suc by auto
have "can_occur (t ! j) (S t i)"
using "0.prems" can_swap_neighboring_pre_and_postrecording_events by blast
then obtain d' where new_step1: "(S t i) \<turnstile> (t ! j) \<mapsto> d'"
using exists_next_if_can_occur by blast
have st: "states d' ?p = states (S t i) ?p"
using \<open>(S t i) \<turnstile> t ! j \<mapsto> d'\<close> \<open>occurs_on (t ! i) \<noteq> occurs_on (t ! j)\<close> no_state_change_if_no_event by auto
then have "can_occur (t ! i) d'"
using \<open>occurs_on (t ! i) \<noteq> occurs_on (t ! j)\<close> event_stays_valid_if_no_occurrence happen_implies_can_occur new_step1 reg_step_1 by auto
then obtain e where new_step2: "d' \<turnstile> (t ! i) \<mapsto> e"
using exists_next_if_can_occur by blast
have "states e = states (S t (j+1))"
proof (rule ext)
fix p
show "states e p = states (S t (j+1)) p"
proof (cases "p = ?p \<or> p = ?q")
case True
then show ?thesis
proof (elim disjE)
assume "p = ?p"
then have "states d' p = states (S t i) p"
by (simp add: st)
thm same_state_implies_same_result_state
then have "states e p = states (S t j) p"
using "0.prems"(2) "0.prems"(6) new_step2 reg_step_1 by (blast intro:same_state_implies_same_result_state[symmetric])
moreover have "states (S t j) p = states (S t (j+1)) p"
using \<open>occurs_on (t ! i) \<noteq> occurs_on (t ! j)\<close> \<open>p = occurs_on (t ! i)\<close> no_state_change_if_no_event reg_step_2 by auto
ultimately show ?thesis by simp
next
assume "p = ?q"
then have "states (S t j) p = states (S t i) p"
using reg_step_1 \<open>occurs_on (t ! i) \<noteq> occurs_on (t ! j)\<close> no_state_change_if_no_event by auto
then have "states d' p = states (S t (j+1)) p"
using "0.prems"(5) prerecording_event computation_axioms new_step1 reg_step_2 same_state_implies_same_result_state by blast
moreover have "states e p = states (S t (j+1)) p"
using \<open>occurs_on (t ! i) \<noteq> occurs_on (t ! j)\<close> \<open>p = occurs_on (t ! j)\<close> calculation new_step2 no_state_change_if_no_event by auto
ultimately show ?thesis by simp
qed
next
case False
then have "states (S t i) p = states (S t j) p"
using no_state_change_if_no_event reg_step_1 by auto
moreover have "... = states (S t (j+1)) p"
using False no_state_change_if_no_event reg_step_2 by auto
moreover have "... = states d' p"
using False calculation new_step1 no_state_change_if_no_event by auto
moreover have "... = states e p"
using False new_step2 no_state_change_if_no_event by auto
ultimately show ?thesis by simp
qed
qed
moreover have "msgs e = msgs (S t (j+1))"
proof (rule ext)
fix cid
have "isTrans (t ! i) \<or> isSend (t ! i) \<or> isRecv (t ! i)"
using "0.prems"(4) computation.postrecording_event computation_axioms regular_event by blast
moreover have "isTrans (t ! j) \<or> isSend (t ! j) \<or> isRecv (t ! j)"
using "0.prems"(5) computation.prerecording_event computation_axioms regular_event by blast
ultimately show "msgs e cid = msgs (S t (j+1)) cid"
proof (elim disjE, goal_cases)