/
SingleInputTransactions.thy
1230 lines (1142 loc) · 67.3 KB
/
SingleInputTransactions.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
theory SingleInputTransactions
imports Main Semantics
begin
declare [[ smt_timeout = 300 ]]
fun inputsToTransactions :: "TimeInterval \<Rightarrow> Input list \<Rightarrow> Transaction list" where
"inputsToTransactions si Nil = Cons \<lparr> interval = si
, inputs = Nil \<rparr> Nil" |
"inputsToTransactions si (Cons inp1 Nil) = Cons \<lparr> interval = si
, inputs = Cons inp1 Nil \<rparr> Nil" |
"inputsToTransactions si (Cons inp1 rest) = Cons \<lparr> interval = si
, inputs = Cons inp1 Nil \<rparr>
(inputsToTransactions si rest)"
fun traceListToSingleInput :: "Transaction list \<Rightarrow> Transaction list" where
"traceListToSingleInput Nil = Nil" |
"traceListToSingleInput (Cons \<lparr> interval = si
, inputs = inps \<rparr> rest) = inputsToTransactions si inps @ (traceListToSingleInput rest)"
lemma reductionLoopIdempotent :
"reductionLoop reducedBefore env state contract wa pa = ContractQuiescent reducedAfter nwa npa nsta ncont \<Longrightarrow>
reductionLoop reducedBefore2 env nsta ncont [] [] = ContractQuiescent reducedBefore2 [] [] nsta ncont"
apply (induction reducedBefore env state contract wa pa rule:reductionLoop.induct)
subgoal for reducedBefore env state contract warnings payments
apply (cases "reduceContractStep env state contract")
apply (cases "reduceContractStep env nsta ncont")
apply (simp add:Let_def)
apply simp
apply simp
apply metis
apply simp
by simp
done
lemma reduceContractUntilQuiescentIdempotent :
"reduceContractUntilQuiescent env state contract = ContractQuiescent reducedAfter wa pa nsta ncont \<Longrightarrow>
reduceContractUntilQuiescent env nsta ncont = ContractQuiescent False [] [] nsta ncont"
apply (simp only:reduceContractUntilQuiescent.simps)
using reductionLoopIdempotent by blast
lemma applyAllLoopEmptyIdempotent :
"applyAllLoop reducedBefore env sta cont [] a b = ApplyAllSuccess reducedAfter wa pa nsta ncont \<Longrightarrow>
applyAllLoop reducedBefore2 env nsta ncont [] c d = ApplyAllSuccess reducedBefore2 c d nsta ncont"
apply (simp only:applyAllLoop.simps[of reducedBefore env sta cont])
apply (cases "reduceContractUntilQuiescent env sta cont")
using reduceContractUntilQuiescentIdempotent apply auto[1]
by simp
lemma applyAllLoopJustAppendsWarningsAndEffects :
"applyAllLoop reducedBefore env st c list (wa @ wt) (ef @ et) = ApplyAllSuccess reducedAfter (wa @ nwa) (ef @ nef) fsta fcont \<Longrightarrow>
applyAllLoop reducedBefore env st c list (wa2 @ wt) (ef2 @ et) = ApplyAllSuccess reducedAfter (wa2 @ nwa) (ef2 @ nef) fsta fcont"
apply (induction list arbitrary: reducedBefore env st c wa wt ef et wa2 ef2 nwa nef)
subgoal for reducedBefore env st c wa wt ef et wa2 ef2 nwa nef
apply (simp only:applyAllLoop.simps[of reducedBefore env st c])
apply (cases "reduceContractUntilQuiescent env st c")
by simp_all
subgoal for head tail reducedBefore env st c wa wt ef et wa2 ef2 nwa nef
apply (simp only:applyAllLoop.simps[of reducedBefore env st c "(head # tail)"])
apply (cases "reduceContractUntilQuiescent env st c")
subgoal for tempReducedAfter tempWa tempEf tempState tempContract
apply (simp only:ReduceResult.case)
apply (subst list.case(2)[of _ _ head tail])
apply (subst (asm) list.case(2)[of _ _ head tail])
apply (cases "applyInput env tempState head tempContract")
apply (metis ApplyResult.simps(4) append.assoc)
by simp
by simp
done
lemma applyAllLoop_preserves_reduced : "applyAllLoop True env state cont list warns pays = ApplyAllSuccess reduced fwarn fpays fstate fcont \<Longrightarrow> reduced"
apply (induction "True" env state cont list warns pays arbitrary:reduced fwarn fpays fstate fcont rule:applyAllLoop.induct)
subgoal for env state contract inputs warnings payments reduced fwarn fpays fstate fcont
apply (simp only:applyAllLoop.simps[of True env state])
apply (auto split:ReduceResult.splits list.splits ApplyResult.splits simp del:reduceContractUntilQuiescent.simps applyAllLoop.simps applyInput.simps simp add:Let_def refl)
by blast
done
lemma applyAllLoop_noNil_reduces : "applyAllLoop False env sta cont (h#t) wa ef = ApplyAllSuccess reduced nwa npa nsta ncont \<Longrightarrow> reduced"
apply (simp only:applyAllLoop.simps[of False env])
apply (auto split:ReduceResult.splits ApplyResult.splits simp del:reduceContractUntilQuiescent.simps applyInput.simps applyAllLoop.simps)
using applyAllLoop_preserves_reduced by blast
lemma sthOrInequality : "(reducedBefore \<or> a # list \<noteq> []) = True"
by simp
lemma applyLoopIdempotent_base_case :
"applyAllLoop reducedBefore env sta cont [] twa tef = ApplyAllSuccess reducedAfter wa pa nsta ncont \<Longrightarrow>
applyAllLoop reducedBefore env sta cont t twa tef = ApplyAllSuccess reducedAfter2 (wa @ nwa) (pa @ npa) fsta fcont \<Longrightarrow>
applyAllLoop reducedBefore2 env nsta ncont t [] [] = ApplyAllSuccess (reducedBefore2 \<or> (t \<noteq> [])) nwa npa fsta fcont"
apply (simp only:applyAllLoop.simps[of reducedBefore env sta cont])
apply (cases "reduceContractUntilQuiescent env sta cont")
apply (simp only:ReduceResult.case list.case)
apply (simp only:applyAllLoop.simps[of reducedBefore2 env nsta ncont])
apply (cases "reduceContractUntilQuiescent env nsta ncont")
apply (simp only:ReduceResult.case list.case)
apply (cases t)
apply (simp only:list.case)
using reduceContractUntilQuiescentIdempotent apply auto[1]
apply (simp only:list.case)
subgoal for x11 x12 x13 x14 x15 x11a x12a x13a x14a x15a a list
apply (cases "applyInput env x14a a x15a")
apply (cases "applyInput env x14 a x15")
apply (simp only:ApplyResult.case sthOrInequality)
apply (smt ApplyAllResult.inject ApplyResult.inject ReduceResult.inject append.right_neutral append_assoc applyAllLoopJustAppendsWarningsAndEffects applyAllLoop_preserves_reduced convertReduceWarnings.simps(1) reduceContractUntilQuiescentIdempotent self_append_conv2)
using reduceContractUntilQuiescentIdempotent apply auto[1]
using reduceContractUntilQuiescentIdempotent by auto
using reduceContractUntilQuiescentIdempotent apply auto[1]
by auto
lemma applyLoopIdempotent :
"applyAllLoop reducedBefore env sta cont [h] [] [] = ApplyAllSuccess reducedAfter wa pa nsta ncont \<Longrightarrow>
applyAllLoop reducedBefore env sta cont (h # t) [] [] = ApplyAllSuccess reducedAfter2 (wa @ nwa) (pa @ npa) fsta fcont \<Longrightarrow>
applyAllLoop reducedBefore env nsta ncont t [] [] = ApplyAllSuccess (reducedBefore \<or> (t \<noteq> [])) nwa npa fsta fcont"
apply (simp only:applyAllLoop.simps[of reducedBefore env sta cont])
apply (cases "reduceContractUntilQuiescent env sta cont")
apply (simp only:ReduceResult.case Let_def list.case)
subgoal for x11 x12 x13 x14 x15
apply (cases "applyInput env x14 h x15")
subgoal for x11a x12a x13a
apply (simp only:applyInput.simps refl ApplyResult.case)
using applyLoopIdempotent_base_case by auto
by simp
by simp
lemma applyLoopIdempotent_base_case2 :
"applyAllLoop reducedBefore env sta cont [] twa tef = ApplyAllSuccess reducedAfter wa pa nsta ncont \<Longrightarrow>
applyAllLoop reducedAfter env nsta ncont t [] [] = ApplyAllSuccess reducedAfter2 nwa npa fsta fcont \<Longrightarrow>
applyAllLoop reducedBefore env sta cont t twa tef = ApplyAllSuccess reducedAfter2 (wa @ nwa) (pa @ npa) fsta fcont"
apply (simp only:applyAllLoop.simps[of reducedBefore env sta cont])
apply (cases "reduceContractUntilQuiescent env sta cont")
apply (simp only:ReduceResult.case list.case)
apply (simp only:applyAllLoop.simps[of reducedAfter env nsta ncont])
apply (cases "reduceContractUntilQuiescent env nsta ncont")
apply (simp only:ReduceResult.case list.case)
apply (cases t)
using reduceContractUntilQuiescentIdempotent apply auto[1]
apply (simp only:list.case ApplyResult.case)
subgoal for x11 x12 x13 x14 x15 x11a x12a x13a x14a x15a a list
apply (cases "applyInput env x14a a x15a")
apply (cases "applyInput env x14 a x15")
apply (simp only:ApplyResult.case)
subgoal for x11b x12b x13b x11aa x12aa x13aa
proof -
assume a1: "ApplyAllSuccess (reducedBefore \<or> x11) (twa @ convertReduceWarnings x12) (tef @ x13) x14 x15 = ApplyAllSuccess reducedAfter wa pa nsta ncont"
assume a2: "reduceContractUntilQuiescent env sta cont = ContractQuiescent x11 x12 x13 x14 x15"
assume a3: "reduceContractUntilQuiescent env nsta ncont = ContractQuiescent x11a x12a x13a x14a x15a"
assume a4: "applyInput env x14a a x15a = Applied x11b x12b x13b"
assume a5: "applyInput env x14 a x15 = Applied x11aa x12aa x13aa"
assume a6: "applyAllLoop True env x12b x13b list ([] @ convertReduceWarnings x12a @ convertApplyWarning x11b) ([] @ x13a) = ApplyAllSuccess reducedAfter2 nwa npa fsta fcont"
have f7: "(\<not> reducedBefore \<and> \<not> x11) \<noteq> reducedAfter \<and> twa @ convertReduceWarnings x12 = wa \<and> tef @ x13 = pa \<and> x14 = nsta \<and> x15 = ncont"
using a1 by blast
have "reduceContractUntilQuiescent env x14 x15 = ContractQuiescent False [] [] x14 x15"
using a2 by (meson reduceContractUntilQuiescentIdempotent)
then have f8: "\<not> x11a \<and> [] = x12a \<and> [] = [] @ x13a \<and> nsta = x14a \<and> ncont = x15a"
using f7 a3 by simp
then have f9: "[] = convertReduceWarnings x12a"
using convertReduceWarnings.simps(1) by presburger
have f10: "wa @ [] @ convertReduceWarnings x12a @ convertApplyWarning x11b = twa @ convertReduceWarnings x12 @ convertApplyWarning x11aa"
using f8 f7 a5 a4 by simp
have f11: "applyAllLoop True env x12aa x13aa list (convertReduceWarnings x12a @ [] @ convertReduceWarnings x12a @ convertApplyWarning x11b) (([] @ x13a) @ [] @ x13a) = ApplyAllSuccess reducedAfter2 nwa npa fsta fcont"
using f8 f7 a6 a5 a4 by auto
have "convertReduceWarnings x12a @ [] @ nwa = nwa"
using f9 by auto
then show ?thesis
using f11 f10 f8 f7 by (metis (no_types) append.right_neutral applyAllLoopJustAppendsWarningsAndEffects self_append_conv2)
qed
using reduceContractUntilQuiescentIdempotent apply auto[1]
by simp
apply simp
by simp
lemma applyLoopIdempotent2 :
"applyAllLoop reducedBefore env sta cont [h] [] [] = ApplyAllSuccess reducedAfter wa pa nsta ncont \<Longrightarrow>
applyAllLoop reducedAfter env nsta ncont t [] [] = ApplyAllSuccess reducedAfter2 nwa npa fsta fcont \<Longrightarrow>
applyAllLoop reducedBefore env sta cont (h # t) [] [] = ApplyAllSuccess reducedAfter2 (wa @ nwa) (pa @ npa) fsta fcont"
apply (simp only:applyAllLoop.simps[of reducedBefore env sta cont])
apply (cases "reduceContractUntilQuiescent env sta cont")
apply (simp only:ReduceResult.case Let_def list.case)
subgoal for x11 x12 x13 x14 x15
apply (cases "applyInput env x14 h x15")
subgoal for x12a x13a x14a
apply (simp only:ApplyResult.case)
using applyLoopIdempotent_base_case2 by blast
using applyLoopIdempotent_base_case2 by auto
by simp
lemma applyAllIterative :
"applyAllInputs env sta cont [h] = ApplyAllSuccess reducedAfter wa pa nsta ncont \<Longrightarrow>
applyAllInputs env sta cont (h#t) = ApplyAllSuccess reducedAfter2 (wa @ nwa) (pa @ npa) fsta fcont \<Longrightarrow>
applyAllInputs env nsta ncont t = ApplyAllSuccess (t \<noteq> []) nwa npa fsta fcont"
apply (simp only:applyAllInputs.simps)
by (smt applyLoopIdempotent)
lemma applyAllIterative2_aux :
"applyAllInputs env sta cont [h] = ApplyAllSuccess True wa pa nsta ncont \<Longrightarrow>
applyAllInputs env nsta ncont t = ApplyAllSuccess reduceAfter2 nwa npa fsta fcont \<Longrightarrow>
applyAllInputs env sta cont (h#t) = ApplyAllSuccess True (wa @ nwa) (pa @ npa) fsta fcont"
apply (simp only:applyAllInputs.simps)
proof -
assume a1: "applyAllLoop False env sta cont [h] [] [] = ApplyAllSuccess True wa pa nsta ncont"
assume a2: "applyAllLoop False env nsta ncont t [] [] = ApplyAllSuccess reduceAfter2 nwa npa fsta fcont"
have f3: "\<forall>b e s c i ba ts ps sa ca is bb tsa psa sb cb. applyAllLoop b e s c [i] [] [] \<noteq> ApplyAllSuccess ba ts ps sa ca \<or> applyAllLoop b e s c (i # is) [] [] \<noteq> ApplyAllSuccess bb (ts @ tsa) (ps @ psa) sb cb \<or> applyAllLoop b e sa ca is [] [] = ApplyAllSuccess (b \<or> is \<noteq> []) tsa psa sb cb"
by (meson applyLoopIdempotent)
have "applyAllLoop False env sta cont [h] [] [] = ApplyAllSuccess True (wa @ []) (pa @ []) nsta ncont"
using a1 by simp
then have "applyAllLoop False env nsta ncont [] [] [] = ApplyAllSuccess False [] [] nsta ncont"
using f3 a1 by presburger
then show "applyAllLoop False env sta cont (h # t) [] [] = ApplyAllSuccess True (wa @ nwa) (pa @ npa) fsta fcont"
using a2 a1 applyLoopIdempotent2 applyLoopIdempotent_base_case by auto
qed
lemma applyAllIterative2 :
"applyAllInputs env sta cont [h] = ApplyAllSuccess reduceAfter1 wa pa nsta ncont \<Longrightarrow>
applyAllInputs env nsta ncont t = ApplyAllSuccess reduceAfter2 nwa npa fsta fcont \<Longrightarrow>
applyAllInputs env sta cont (h#t) = ApplyAllSuccess True (wa @ nwa) (pa @ npa) fsta fcont"
apply (rule mp[of "reduceAfter1 = True"])
using applyAllIterative2_aux apply blast
apply (simp only:applyAllInputs.simps[of env sta cont "[h]"])
using applyAllLoop_noNil_reduces by blast
lemma applyAllInputsPrefix1:
"applyAllLoop reduceBefore env sta cont l iwa ipa = ApplyAllSuccess reduceAfter fwa fpa nsta ncont \<Longrightarrow>
\<exists>nwa. fwa = iwa @ nwa"
apply (induction reduceBefore env sta cont l iwa ipa arbitrary:fwa fpa nsta ncont rule:applyAllLoop.induct)
subgoal for reduceBefore env state contract inputs warnings payments fwa fpa nsta ncont
apply (simp only:applyAllLoop.simps[of reduceBefore env state contract inputs warnings payments])
apply (cases "reduceContractUntilQuiescent env state contract")
subgoal for reduceReduced reduceWarns reducePays reduceState reduceCont
apply (simp only:ReduceResult.case)
apply (cases inputs)
apply (simp only:list.case)
apply blast
subgoal for h t
apply (simp only:list.case)
apply (cases "applyInput env reduceState h reduceCont")
subgoal for applyWarn applyState applyCont
apply (simp only:ApplyResult.case)
by fastforce
by simp
done
by simp
done
lemma applyAllInputsPrefix2:
"applyAllLoop reducedBefore env sta cont l iwa ipa = ApplyAllSuccess reducedAfter fwa fpa nsta ncont \<Longrightarrow>
\<exists>npa. fpa = ipa @ npa"
apply (induction reducedBefore env sta cont l iwa ipa arbitrary:reducedAfter fwa fpa nsta ncont rule:applyAllLoop.induct)
subgoal for reducedBefore env state contract inputs warnings payments reducedAfter fwa fpa nsta ncont
apply (simp only:applyAllLoop.simps[of reducedBefore env state contract inputs warnings payments])
apply (cases "reduceContractUntilQuiescent env state contract")
subgoal for reduceReduced reduceWarns reducePays reduceState reduceCont
apply (simp only:ReduceResult.case)
apply (cases inputs)
apply (simp only:list.case)
apply blast
subgoal for h t
apply (simp only:list.case)
apply (cases "applyInput env reduceState h reduceCont")
subgoal for applyWarn applyState applyCont
apply (simp only:ApplyResult.case)
by force
by simp
done
by simp
done
lemma beforeApplyAllLoopIsUseless:
"iwa @ convertReduceWarnings x11 = wa \<Longrightarrow>
ipa @ x12 = pa \<Longrightarrow>
applyAllLoop reducedBefore2 env applyState applyCont t iwa ipa = ApplyAllSuccess reducedAfter2 fwa fpa fsta fcont \<Longrightarrow>
reduceContractUntilQuiescent env applyState applyCont = ContractQuiescent reducedAfter x11 x12 nsta ncont \<Longrightarrow>
ApplyAllSuccess reducedAfter2 fwa fpa fsta fcont = applyAllLoop reducedAfter2 env nsta ncont t wa pa"
apply (simp only:applyAllLoop.simps[of reducedBefore2 env applyState])
apply (simp only:applyAllLoop.simps[of reducedAfter2 env nsta])
apply (cases "reduceContractUntilQuiescent env nsta ncont")
subgoal for x11a x12a x13 x14
apply (simp only:ReduceResult.case)
apply (cases t)
apply (simp only:list.case)
using reduceContractUntilQuiescentIdempotent apply auto[1]
subgoal for h t
apply (simp only:list.case)
apply (simp only:reduceContractUntilQuiescentIdempotent)
apply (cases "applyInput env nsta h ncont")
apply force
by simp
done
using reduceContractUntilQuiescentIdempotent by auto
lemma applyAllInputsPrefix_aux:
"applyAllLoop reducedBefore env sta cont [h] [] [] = ApplyAllSuccess reducedAfter wa pa nsta ncont \<Longrightarrow>
applyAllLoop reducedBefore2 env sta cont (h # t) [] [] = ApplyAllSuccess reducedAfter2 fwa fpa fsta fcont \<Longrightarrow>
(\<exists> applyReducedBefore twa x11 x12 x13 applyState applyCont reducePays reduceState reduceCont.
twa @ convertReduceWarnings x12 = wa \<and>
reducePays @ x13 = pa \<and>
applyAllLoop applyReducedBefore env applyState applyCont t twa reducePays = ApplyAllSuccess reducedAfter2 fwa fpa fsta fcont \<and>
reduceContractUntilQuiescent env applyState applyCont = ContractQuiescent x11 x12 x13 nsta ncont)"
apply (subst (asm) applyAllLoop.simps[of reducedBefore env sta cont "[h]"])
apply (cases "reduceContractUntilQuiescent env sta cont")
subgoal for reduceReduced reduceWarns reducePays reduceState reduceCont
apply (simp only:ReduceResult.case)
apply (simp only:list.case)
apply (cases "applyInput env reduceState h reduceCont")
subgoal for applyWarn applyState applyCont
apply (simp only:ApplyResult.case)
apply (subst (asm) applyAllLoop.simps[of reducedBefore2 env sta cont "(h # t)"])
apply (cases "reduceContractUntilQuiescent env sta cont")
subgoal for reduceWarns2 reducePays2 reduceState2 reduceCont2
apply (simp only:ReduceResult.case)
apply (simp only:list.case)
apply (cases "applyInput env reduceState h reduceCont")
subgoal for applyWarn2 applyState2 applyCont2
apply (simp only:ApplyResult.case)
apply (subst (asm) applyAllLoop.simps[of True env applyState applyCont "[]"])
apply (cases "reduceContractUntilQuiescent env applyState applyCont")
subgoal for x11 x12 x13 x14
apply (simp only:ReduceResult.case list.case)
apply (simp del:applyAllLoop.simps reduceContractUntilQuiescent.simps applyInput.simps)
using append_assoc by blast
by simp
by simp
by simp
by simp
by simp
lemma applyAllInputsPrefix1_aux2:
"applyAllLoop reducedBefore env sta cont [h] [] [] = ApplyAllSuccess reducedAfter wa pa nsta ncont \<Longrightarrow>
applyAllLoop reducedBefore2 env sta cont (h # t) [] [] = ApplyAllSuccess reducedAfter2 fwa fpa fsta fcont \<Longrightarrow>
\<exists>nwa. fwa = wa @ nwa"
apply (frule applyAllInputsPrefix_aux[of reducedBefore env sta cont h reducedAfter wa pa nsta ncont reducedBefore2 t reducedAfter2 fwa fpa fsta fcont])
apply simp
by (metis applyAllInputsPrefix1 beforeApplyAllLoopIsUseless)
lemma applyAllPrefix1:
"applyAllInputs env sta cont [h] = ApplyAllSuccess reducedAfter wa pa nsta ncont \<Longrightarrow>
applyAllInputs env sta cont (h#t) = ApplyAllSuccess reducedAfter2 fwa fpa fsta fcont \<Longrightarrow>
(\<exists> nwa. fwa = wa @ nwa)"
apply (simp only:applyAllInputs.simps)
by (simp add: applyAllInputsPrefix1_aux2)
lemma applyAllInputsPrefix2_aux2:
"applyAllLoop reducedBefore env sta cont [h] [] [] = ApplyAllSuccess reducedAfter wa pa nsta ncont \<Longrightarrow>
applyAllLoop reducedBefore2 env sta cont (h # t) [] [] = ApplyAllSuccess reducedAfter2 fwa fpa fsta fcont \<Longrightarrow>
\<exists>npa. fpa = pa @ npa"
apply (frule applyAllInputsPrefix_aux[of reducedBefore env sta cont h reducedAfter wa pa nsta ncont reducedBefore2 t reducedAfter2 fwa fpa fsta fcont])
apply simp
by (metis applyAllInputsPrefix2 beforeApplyAllLoopIsUseless)
lemma applyAllPrefix2:
"applyAllInputs env sta cont [h] = ApplyAllSuccess reduced wa pa nsta ncont \<Longrightarrow>
applyAllInputs env sta cont (h#t) = ApplyAllSuccess reduced2 fwa fpa fsta fcont \<Longrightarrow>
(\<exists> npa. fpa = pa @ npa)"
by (simp add: applyAllInputsPrefix2_aux2)
lemma computeAllPrefix1:
"computeTransaction \<lparr>interval = interv, inputs = [head]\<rparr> sta cont =
TransactionOutput \<lparr>txOutWarnings = wa, txOutPayments = pa, txOutState = nsta, txOutContract = ncont\<rparr> \<Longrightarrow>
computeTransaction \<lparr>interval = interv, inputs = head # tail\<rparr> sta cont =
TransactionOutput \<lparr>txOutWarnings = fwa, txOutPayments = fpa, txOutState = fsta, txOutContract = fcont\<rparr> \<Longrightarrow>
(\<exists> nwa. fwa = wa @ nwa)"
apply (simp only:computeTransaction.simps)
apply (cases "fixInterval (interval \<lparr>interval = interv, inputs = [head]\<rparr>) sta")
subgoal for env fixSta
apply (cases "applyAllInputs env fixSta cont [head]")
subgoal for warnings payments newState conta
apply (cases "applyAllInputs env fixSta cont (head # tail)")
subgoal for warnings2 payments2 newState2 conta2
apply (simp del:applyAllInputs.simps fixInterval.simps)
by (metis TransactionOutput.distinct(1) TransactionOutput.inject(1) TransactionOutputRecord.ext_inject applyAllPrefix1)
by simp_all
by simp_all
by simp
lemma computeAllPrefix2:
"computeTransaction \<lparr>interval = interv, inputs = [head]\<rparr> sta cont =
TransactionOutput \<lparr>txOutWarnings = wa, txOutPayments = pa, txOutState = nsta, txOutContract = ncont\<rparr> \<Longrightarrow>
computeTransaction \<lparr>interval = interv, inputs = head # tail\<rparr> sta cont =
TransactionOutput \<lparr>txOutWarnings = fwa, txOutPayments = fpa, txOutState = fsta, txOutContract = fcont\<rparr> \<Longrightarrow>
(\<exists> npa. fpa = pa @ npa)"
apply (simp only:computeTransaction.simps)
apply (cases "fixInterval (interval \<lparr>interval = interv, inputs = [head]\<rparr>) sta")
subgoal for env fixSta
apply (cases "applyAllInputs env fixSta cont [head]")
subgoal for warnings payments newState conta
apply (cases "applyAllInputs env fixSta cont (head # tail)")
subgoal for warnings2 payments2 newState2 conta2
apply (simp del:applyAllInputs.simps fixInterval.simps)
by (metis TransactionOutput.distinct(1) TransactionOutput.inject(1) TransactionOutputRecord.ext_inject applyAllPrefix2)
by simp_all
by simp_all
by simp
lemma fixIntervalOnlySummary :
"minTime state = low \<Longrightarrow> low \<le> high \<Longrightarrow>
IntervalTrimmed \<lparr> timeInterval = (low, high) \<rparr> state = fixInterval (low, high) state"
by simp
lemma fixIntervalOnlySummary2 :
"fixInterval (low, high) state = IntervalTrimmed \<lparr> timeInterval = (nlow, nhigh) \<rparr> nstate \<Longrightarrow>
nlow = minTime nstate \<and> low \<le> high"
apply (cases "high < low")
apply simp
apply (cases "high < minTime state")
by (auto simp add:Let_def)
lemma fixIntervalChecksInterval :
"fixInterval inte sta1 = IntervalTrimmed \<lparr>timeInterval = (low, high)\<rparr> sta2 \<Longrightarrow>
low \<le> high"
apply (cases inte)
apply (simp add:Let_def)
subgoal for low1 high1
apply (cases "high1 < low1")
apply simp_all
apply (cases "high1 < minTime sta1")
apply simp_all
by linarith
done
lemma fixIntervalIdempotentOnInterval :
"minTime sta4 = minTime sta2 \<Longrightarrow>
fixInterval (low1, high1) sta1 = IntervalTrimmed \<lparr>timeInterval = (low, high)\<rparr> sta2 \<Longrightarrow>
fixInterval (low1, high1) sta4 = fixInterval (low, high) sta4"
apply (cases "high1 < low1")
apply simp
apply (cases "high1 < minTime sta1")
by (auto simp add:Let_def)
lemma reductionContractStep_preserves_minTime :
"reduceContractStep env state contract = Reduced wa ef sta2 cont2 \<Longrightarrow>
minTime state = minTime sta2"
apply (cases contract)
apply (auto split:option.splits simp add:Let_def)
subgoal for x21 x22 x23 x24 x25
apply (cases "evalValue env state x24 \<le> 0")
apply simp
apply (auto split:prod.splits simp add:Let_def)
done
apply (auto split:prod.splits simp add:Let_def)
by (metis ReduceStepResult.distinct(1) ReduceStepResult.distinct(3) ReduceStepResult.inject)
lemma reductionLoop_preserves_minTime :
"reductionLoop reducedBefore env sta con wa pa = ContractQuiescent reducedAfter reduceWarns pays sta2 con2 \<Longrightarrow> minTime sta = minTime sta2"
apply (induction reducedBefore env sta con wa pa arbitrary:reducedAfter reduceWarns pays sta2 con2 rule:reductionLoop.induct)
subgoal for env state contract warnings payments reduceWarns pays sta2 con2
apply (simp only:reductionLoop.simps[of env state contract warnings payments])
apply (auto split:ReduceStepResult.splits simp del:reductionLoop.simps)
using reductionContractStep_preserves_minTime by auto
done
lemma reduceContractUntilQuiescent_preserves_minTime :
"reduceContractUntilQuiescent env sta con = ContractQuiescent reducedAfter reduceWarns pays sta2 con2 \<Longrightarrow> minTime sta = minTime sta2"
apply (simp only:reduceContractUntilQuiescent.simps)
by (simp add: reductionLoop_preserves_minTime)
lemma applyCases_preserves_minTime :
"applyCases env curState head x41 = Applied applyWarn newState newCont \<Longrightarrow>
minTime curState = minTime newState"
apply (induction env curState head x41 arbitrary:applyWarn newCont newState rule:applyCases.induct)
subgoal for env state accId1 party1 tok1 amount accId2 party2 tok2 val cont rest applyWarn newCont newState
apply (cases "accId1 = accId2 \<and> party1 = party2 \<and> tok1 = tok2 \<and> amount = evalValue env state val")
by auto
subgoal for env state choId1 choice choId2 bounds cont rest applyWarn newCont newState
apply (cases "choId1 = choId2 \<and> inBounds choice bounds")
by auto
subgoal for env state obs cont rest applyWarn newCont newState
apply (cases "evalObservation env state obs")
by auto
by auto
lemma applyInput_preserves_minTime :
"applyInput env curState head cont = Applied applyWarn newState newCont \<Longrightarrow> minTime curState = minTime newState"
apply (cases cont)
by (auto simp add:applyCases_preserves_minTime)
lemma applyAllLoop_preserves_minTime :
"applyAllLoop reducedBefore env sta con inp wa pa = ApplyAllSuccess reducedAfter wa2 pa2 sta2 con2 \<Longrightarrow> minTime sta = minTime sta2"
apply (induction inp arbitrary:reducedBefore env sta con wa pa reducedAfter wa2 pa2 sta2 con2)
subgoal for reducedBefore env sta con wa pa reducedAfter wa2 pa2 sta2 con2
apply (simp only:applyAllLoop.simps[of reducedBefore env sta con "[]" wa pa])
apply (cases "reduceContractUntilQuiescent env sta con")
subgoal for reduceWarns pays curState cont
apply (simp del:reduceContractUntilQuiescent.simps)
using reduceContractUntilQuiescent_preserves_minTime by blast
apply (simp del:reduceContractUntilQuiescent.simps)
done
subgoal for head tail reducedBefore env sta con wa pa reducedAfter wa2 pa2 sta2 con2
apply (simp only:applyAllLoop.simps[of reducedBefore env sta con "(head # tail)" wa pa])
apply (cases "reduceContractUntilQuiescent env sta con")
subgoal for reducedAfter reduceWarns pays curState cont
apply (cases "applyInput env curState head cont")
subgoal for applyWarn newState newCont
by (simp add: applyInput_preserves_minTime reduceContractUntilQuiescent_preserves_minTime)
by simp
by simp
done
lemma applyAllInputs_preserves_minTime :
"applyAllInputs env sta con inp = ApplyAllSuccess reducedAfter wa2 pa2 sta2 con2 \<Longrightarrow>
minTime sta = minTime sta2"
apply (simp only:applyAllInputs.simps)
using applyAllLoop_preserves_minTime by blast
lemma applyAllInputs_preserves_minTime_rev :
"applyAllInputs env sta con inp = ApplyAllSuccess reducedAfter wa2 pa2 sta2 con2 \<Longrightarrow>
minTime sta2 = minTime sta"
by (simp add: applyAllInputs_preserves_minTime)
lemma fixIntervalIdempotentThroughApplyAllInputs :
"fixInterval inte sta1 = IntervalTrimmed env2 sta2 \<Longrightarrow>
applyAllInputs env2 sta2 con3 inp1 = ApplyAllSuccess reducedAfter wa4 pa4 sta4 con4 \<Longrightarrow>
fixInterval inte sta4 = IntervalTrimmed env2 sta4"
apply (cases env2)
subgoal for timeInterval
apply (cases timeInterval)
subgoal for low high
apply (simp del:fixInterval.simps applyAllInputs.simps)
apply (subst fixIntervalOnlySummary)
apply (metis applyAllInputs_preserves_minTime eq_fst_iff fixIntervalOnlySummary2)
using fixIntervalChecksInterval apply blast
apply (cases inte)
subgoal for low1 high1
using applyAllInputs_preserves_minTime_rev fixIntervalIdempotentOnInterval by blast
done
done
done
lemma fixIntervalIdempotentThroughApplyAllInputs2 :
"fixInterval interv sta = IntervalTrimmed fIenv1 fIsta1 \<Longrightarrow>
applyAllInputs fIenv1 fIsta1 con [head] = ApplyAllSuccess reducedAfter iwa ipa ista con3 \<Longrightarrow>
fixInterval interv ista = IntervalTrimmed fIenv1 ista"
using fixIntervalIdempotentThroughApplyAllInputs by blast
lemma smallerSize_implies_different :
"size cont1 < size cont \<Longrightarrow> cont1 \<noteq> cont"
by blast
lemma reductionStep_only_makes_smaller :
"contract \<noteq> ncontract \<Longrightarrow>
reduceContractStep env state contract = Reduced warning effect newState ncontract \<Longrightarrow> size ncontract < size contract"
apply (cases contract)
apply simp
apply (cases "refundOne (accounts state)")
apply simp
apply (simp add: case_prod_beta)
subgoal for accountId payee token val contract
apply (simp add:Let_def)
apply (cases "evalValue env state val \<le> 0")
apply (simp only:if_True Let_def)
apply blast
apply (simp only:if_False Let_def)
apply (cases "giveMoney accountId payee token (min (moneyInAccount accountId token (accounts state)) (evalValue env state val))
(updateMoneyInAccount accountId token
(moneyInAccount accountId token (accounts state) -
min (moneyInAccount accountId token (accounts state)) (evalValue env state val))
(accounts state))")
apply simp
done
apply auto[1]
subgoal for cases timeout contract
apply simp
apply (cases "timeInterval env")
subgoal for low high
apply simp
apply (cases "high < timeout")
apply simp_all
apply (cases "timeout \<le> low")
by simp_all
done
apply(simp add:Let_def)
by simp
lemma reductionLoop_only_makes_smaller :
"cont1 \<noteq> cont \<Longrightarrow>
reductionLoop reducedBefore env state cont wa pa = ContractQuiescent reducedAfter nwa npa nsta cont1 \<Longrightarrow>
size cont1 < size cont"
apply (induction reducedBefore env state cont wa pa arbitrary:cont1 reducedAfter nwa npa nsta rule:reductionLoop.induct)
subgoal for reducedBefore env state contract warnings payments cont1 reducedAfter nwa npa nsta
apply (simp only:reductionLoop.simps[of reducedBefore env state contract warnings payments])
apply (cases "reduceContractStep env state contract")
subgoal for warning effect newState ncontract
apply (simp del:reduceContractStep.simps reductionLoop.simps)
by (metis dual_order.strict_trans reductionStep_only_makes_smaller)
apply simp
by simp
done
lemma reduceContractUntilQuiescent_only_makes_smaller :
"cont1 \<noteq> cont \<Longrightarrow>
reduceContractUntilQuiescent env state cont = ContractQuiescent reducedAfter wa pa nsta cont1 \<Longrightarrow>
size cont1 < size cont"
apply (simp only:reduceContractUntilQuiescent.simps)
by (simp add: reductionLoop_only_makes_smaller)
lemma applyCases_only_makes_smaller :
"applyCases env curState input cases = Applied applyWarn newState cont1 \<Longrightarrow>
size cont1 < size_list size cases"
apply (induction env curState input cases rule:applyCases.induct)
apply auto
apply (metis ApplyResult.inject less_SucI less_add_Suc1 trans_less_add2)
apply (metis ApplyResult.inject less_SucI less_add_Suc1 trans_less_add2)
apply (metis ApplyResult.inject less_SucI less_add_Suc1 trans_less_add2)
done
lemma applyInput_only_makes_smaller :
"cont1 \<noteq> cont \<Longrightarrow>
applyInput env curState input cont = Applied applyWarn newState cont1 \<Longrightarrow>
size cont1 < size cont"
apply (cases cont)
apply simp_all
subgoal for cases timeout contract
by (simp add: add.commute applyCases_only_makes_smaller less_SucI trans_less_add2)
done
lemma applyAllLoop_only_makes_smaller :
"cont1 \<noteq> cont \<Longrightarrow>
applyAllLoop reducedBefore env sta cont c wa ef = ApplyAllSuccess reducedAfter cwa1 pa1 sta1 cont1 \<Longrightarrow> cont1 \<noteq> cont \<Longrightarrow> size cont1 < size cont"
apply (induction reducedBefore env sta cont c wa ef rule:applyAllLoop.induct)
subgoal for reducedBefore env state contract inputs warnings payments
apply (simp only:applyAllLoop.simps[of reducedBefore env state contract inputs warnings payments])
apply (cases "reduceContractUntilQuiescent env state contract")
apply (simp only:ReduceResult.case)
subgoal for reducedAfter wa pa nsta cont1
apply (cases inputs)
apply (simp only:list.case)
apply (simp add:reduceContractUntilQuiescent_only_makes_smaller)
subgoal for head tail
apply (simp only:list.case)
apply (cases "applyInput env nsta head cont1")
subgoal for applyWarn newState cont2
apply (simp only:ApplyResult.case)
by (smt applyInput_only_makes_smaller le_trans less_imp_le_nat not_le reduceContractUntilQuiescent_only_makes_smaller)
by simp
done
by simp
done
lemma applyAllInputs_only_makes_smaller :
"applyAllInputs env sta cont c = ApplyAllSuccess reducedAfter cwa1 pa1 sta1 cont1 \<Longrightarrow>
cont1 \<noteq> cont \<Longrightarrow> size cont1 < size cont"
apply (simp only:applyAllInputs.simps)
using applyAllLoop_only_makes_smaller by blast
lemma applyAllLoop_longer_doesnt_grow :
"applyAllLoop reducedBefore env sta cont h wa pa = ApplyAllSuccess reducedAfter1 cwa1 pa1 sta1 cont1 \<Longrightarrow>
applyAllLoop reducedBefore env sta cont (h @ t) wa pa = ApplyAllSuccess reducedAfter2 cwa2 pa2 sta2 cont2 \<Longrightarrow> size cont2 \<le> size cont1"
apply (induction h arbitrary: reducedBefore env sta cont t wa pa reducedAfter1 cwa1 pa1 sta1 cont1 reducedAfter2 cwa2 pa2 sta2 cont2)
subgoal for reducedBefore env sta cont t wa pa reducedAfter1 cwa1 pa1 sta1 cont1 reducedAfter2 cwa2 pa2 sta2 cont2
apply (subst (asm) applyAllLoop.simps)
apply (subst (asm) applyAllLoop.simps[of reducedBefore env sta cont "[] @ t"])
apply (cases "reduceContractUntilQuiescent env sta cont")
apply (simp only:ReduceResult.case)
apply (simp only:list.case append_Nil)
subgoal for reducedAfter wa pa nsta ncont
apply (cases t)
apply (simp only:list.case)
apply blast
apply (simp only:list.case)
subgoal for head tail
apply (cases "applyInput env nsta head ncont")
apply (simp only:ApplyResult.case)
apply (metis ApplyAllResult.inject applyAllLoop_only_makes_smaller applyInput_only_makes_smaller less_le_trans not_le_imp_less order.asym)
by simp
done
by simp
subgoal for hh ht reducedBefore env sta cont t wa pa reducedAfter1 cwa1 pa1 sta1 cont1 reducedAfter2 cwa2 pa2 sta2 cont2
apply (subst (asm) applyAllLoop.simps[of reducedBefore env sta cont "(hh # ht)"])
apply (subst (asm) applyAllLoop.simps[of reducedBefore env sta cont "(hh # ht) @ t"])
apply (cases "reduceContractUntilQuiescent env sta cont")
apply (simp only:ReduceResult.case List.append.append_Cons)
apply (simp only:list.case)
subgoal for reducedAfter wa pa nsta ncont
apply (cases "applyInput env nsta hh ncont")
apply (simp only:ApplyResult.case)
by simp
by simp
done
lemma applyAllInputs_longer_doesnt_grow :
"applyAllInputs env sta cont h = ApplyAllSuccess reducedAfter1 cwa1 pa1 sta1 cont1 \<Longrightarrow>
applyAllInputs env sta cont (h @ t) = ApplyAllSuccess reducedAfter2 cwa2 pa2 sta2 cont2 \<Longrightarrow>
size cont2 \<le> size cont1"
apply (simp only:applyAllInputs.simps)
by (simp add: applyAllLoop_longer_doesnt_grow)
lemma applyAllInputs_once_modified_always_modified :
"applyAllInputs env sta cont [h] = ApplyAllSuccess reducedAfter1 cwa1 pa1 sta1 cont1 \<Longrightarrow>
cont1 \<noteq> cont \<Longrightarrow>
applyAllInputs env sta cont (h # t) = ApplyAllSuccess reducedAfter2 cwa2 pa2 sta2 cont2 \<Longrightarrow>
cont2 \<noteq> cont"
apply (rule smallerSize_implies_different)
by (metis append_Cons append_Nil applyAllInputs.simps applyAllLoop_longer_doesnt_grow applyAllLoop_only_makes_smaller not_le)
lemma computeTransactionIterative_aux :
"fixInterval inte osta = IntervalTrimmed env sta \<Longrightarrow>
applyAllInputs env sta cont [h] = ApplyAllSuccess reducedAfter wa pa tsta ncont \<Longrightarrow>
fixInterval inte tsta = IntervalTrimmed nenv nsta \<Longrightarrow>
applyAllInputs nenv nsta ncont t = ApplyAllSuccess reducedAfter2 nwa npa fsta fcont \<Longrightarrow>
applyAllInputs env sta cont (h # t) = ApplyAllSuccess True (wa @ nwa) (pa @ npa) fsta fcont"
using applyAllIterative2 fixIntervalIdempotentThroughApplyAllInputs by auto
lemma computeTransactionIterative_aux2 :
"fixInterval inte sta = IntervalTrimmed fIenv1 fIsta1 \<Longrightarrow>
applyAllInputs fIenv1 fIsta1 con [h] = ApplyAllSuccess reducedAfter1 cwa1 pa1 sta1 cont1 \<Longrightarrow>
\<not> (cont1 = con \<and> (con \<noteq> Close \<or> accounts sta = [])) \<Longrightarrow>
applyAllInputs fIenv1 fIsta1 con (h # t) = ApplyAllSuccess reducedAfter3 cwa3 pa3 sta3 cont3 \<Longrightarrow>
\<not> (cont3 = con \<and> (con \<noteq> Close \<or> accounts sta = []))"
using applyAllInputs_once_modified_always_modified by blast
lemma computeTransactionIterative :
"computeTransaction \<lparr> interval = inte
, inputs = [h] \<rparr> sta cont = TransactionOutput \<lparr> txOutWarnings = wa
, txOutPayments = pa
, txOutState = nsta
, txOutContract = ncont \<rparr> \<Longrightarrow>
computeTransaction \<lparr> interval = inte
, inputs = t \<rparr> nsta ncont = TransactionOutput \<lparr> txOutWarnings = nwa
, txOutPayments = npa
, txOutState = fsta
, txOutContract = fcont \<rparr> \<Longrightarrow>
computeTransaction \<lparr> interval = inte
, inputs = h#t \<rparr> sta cont = TransactionOutput \<lparr> txOutWarnings = wa @ nwa
, txOutPayments = pa @ npa
, txOutState = fsta
, txOutContract = fcont \<rparr>"
apply (simp only:computeTransaction.simps)
apply (cases "fixInterval (interval \<lparr>interval = inte, inputs = [h]\<rparr>) sta")
subgoal for fIenv1 fIsta1
apply (simp only:IntervalResult.case Let_def)
apply (cases "applyAllInputs fIenv1 fIsta1 cont (inputs \<lparr>interval = inte, inputs = [h]\<rparr>)")
apply (simp only:ApplyAllResult.case)
subgoal for reducedAfter1 cwa1 pa1 sta1 con1
apply (cases "\<not> reducedAfter1 \<and> (cont \<noteq> Close \<or> accounts sta = [])")
apply simp
apply (simp only:if_False)
apply (cases "fixInterval (interval \<lparr>interval = inte, inputs = t\<rparr>) nsta")
apply (simp only:IntervalResult.case Let_def)
subgoal for fIenv2 fIsta2
apply (cases "applyAllInputs fIenv2 fIsta2 ncont (inputs \<lparr>interval = inte, inputs = t\<rparr>)")
apply (simp only:ApplyAllResult.case)
subgoal for reducedAfter2 cwa2 pa2 sta2 con2
apply (cases "\<not> reducedAfter2 \<and> (ncont \<noteq> Close \<or> accounts nsta = [])")
apply simp
apply (simp only:if_False)
apply (cases "fixInterval (interval \<lparr>interval = inte, inputs = h # t\<rparr>) sta")
apply (simp only:IntervalResult.case Let_def)
subgoal for fIenv3 fIsta3
apply (cases "applyAllInputs fIenv3 fIsta3 cont (inputs \<lparr>interval = inte, inputs = h # t\<rparr>)")
apply (simp only:ApplyAllResult.case)
subgoal for reducedAfter3 cwa3 pa3 sta3 con3
apply (cases "\<not> reducedAfter3 \<and> (cont \<noteq> Close \<or> accounts sta = [])")
using applyAllIterative2 fixIntervalIdempotentThroughApplyAllInputs apply auto[1]
apply (simp only:if_False)
by (smt ApplyAllResult.inject IntervalResult.inject(1) Transaction.select_convs(1) Transaction.select_convs(2) TransactionOutput.inject(1) TransactionOutputRecord.ext_inject applyAllIterative applyAllPrefix1 applyAllPrefix2 fixIntervalIdempotentThroughApplyAllInputs)
apply (simp only:ApplyAllResult.case)
apply (smt ApplyAllResult.distinct(1) IntervalResult.inject(1) Transaction.select_convs(1) Transaction.select_convs(2) TransactionOutput.inject(1) TransactionOutputRecord.ext_inject applyAllIterative2 fixIntervalIdempotentThroughApplyAllInputs)
apply (simp only:ApplyAllResult.case)
by (smt ApplyAllResult.distinct(3) IntervalResult.inject(1) Transaction.select_convs(1) Transaction.select_convs(2) TransactionOutput.inject(1) TransactionOutputRecord.ext_inject applyAllIterative2 fixIntervalIdempotentThroughApplyAllInputs)
by simp
apply simp
by simp
by simp
by simp_all
by simp
lemma fixIntervalPreservesAccounts :
"fixInterval interv sta = IntervalTrimmed interv2 sta2 \<Longrightarrow> accounts sta = accounts sta2"
apply (cases "sta")
apply (cases "interv")
subgoal for accounts choices boundValues minTime low high
apply simp
apply (cases "high < low")
apply simp
apply (cases "high < minTime")
by (auto simp add:Let_def)
done
lemma applyInput_reducesContract :
"applyInput fIenv3 curState2 head cont3 = Applied applyWarna newState2 cont4 \<Longrightarrow> size cont3 > size cont4"
apply (cases cont3)
apply auto
by (simp add: add.commute applyCases_only_makes_smaller less_SucI trans_less_add2)
lemma computeTransactionEquivalence_aux3 :
"rest \<noteq> [] \<Longrightarrow>
applyAllInputs fIenv3 fIsta1 con [head] = ApplyAllSuccess iReducedAfter iwa ipa fIsta3 con3 \<Longrightarrow>
\<not> applyAllInputs fIenv3 fIsta1 con (head # rest) = ApplyAllSuccess iReducedAfter2 fwa fpa sta3 con3"
apply (simp only:applyAllInputs.simps)
apply (simp only:applyAllLoop.simps[of False fIenv3 fIsta1])
apply (cases "reduceContractUntilQuiescent fIenv3 fIsta1 con")
apply (simp only:ReduceResult.case list.case)
subgoal for reduceReduced reduceWarns pays curState cont
apply (cases "applyInput fIenv3 curState head cont")
subgoal for applyWarn newState cont2
apply (simp del:reduceContractUntilQuiescent.simps applyInput.simps applyAllLoop.simps)
apply (cases rest)
apply blast
subgoal for head tail
apply (simp del:reduceContractUntilQuiescent.simps applyInput.simps applyAllLoop.simps)
apply (simp only:applyAllLoop.simps[of True fIenv3 newState])
apply (cases "reduceContractUntilQuiescent fIenv3 newState cont2")
subgoal for reduceReduceda reduceWarnsa paysa curState2 cont3
apply (simp only:ReduceResult.case list.case)
apply (cases "applyInput fIenv3 curState2 head cont3")
apply (simp only:ApplyResult.case)
subgoal for applyWarna newState2 cont4
by (metis ApplyAllResult.inject applyAllLoop_only_makes_smaller applyInput_reducesContract order.asym)
by simp
by simp
done
by simp
by simp
lemma notFalseAndTrue : "\<not> False \<and> True = True"
by simp
lemma computeTransactionStepEquivalence :
"rest \<noteq> [] \<Longrightarrow>
computeTransaction \<lparr>interval = interv, inputs = [head]\<rparr> sta con
= TransactionOutput \<lparr> txOutWarnings = iwa
, txOutPayments = ipa
, txOutState = ista
, txOutContract = icont \<rparr> \<Longrightarrow>
computeTransaction \<lparr>interval = interv, inputs = head # rest\<rparr> sta con
= TransactionOutput \<lparr> txOutWarnings = iwa @ iwa2
, txOutPayments = ipa @ ipa2
, txOutState = ista2
, txOutContract = icont2 \<rparr> \<Longrightarrow>
computeTransaction \<lparr>interval = interv, inputs = rest\<rparr> ista icont
= TransactionOutput \<lparr> txOutWarnings = iwa2
, txOutPayments = ipa2
, txOutState = ista2
, txOutContract = icont2 \<rparr>"
apply (simp only:computeTransaction.simps)
apply (simp del:fixInterval.simps computeTransaction.simps applyAllInputs.simps)
apply (cases "fixInterval interv sta")
subgoal for fIenv1 fIsta1
apply (simp del:fixInterval.simps computeTransaction.simps applyAllInputs.simps)
apply (cases "applyAllInputs fIenv1 fIsta1 con [head]")
apply (simp only:ApplyAllResult.case)
subgoal for reducedAfter1 cwa1 pa1 sta1 con1
apply (cases "\<not> reducedAfter1 \<and> (con \<noteq> Close \<or> accounts sta = [])")
apply simp
apply (simp del:fixInterval.simps computeTransaction.simps applyAllInputs.simps only:refl if_False)
apply (cases "fixInterval interv ista2")
subgoal for fIenv2 fIsta2
apply (cases "applyAllInputs fIenv1 fIsta1 con (head # rest)")
apply (simp only:ApplyAllResult.case if_False)
subgoal for reducedAfter2 cwa2 pa2 sta2 con2
apply (cases "\<not> reducedAfter2 \<and> (con \<noteq> Close \<or> accounts sta = [])")
apply simp
apply (simp del:fixInterval.simps computeTransaction.simps applyAllInputs.simps only:refl if_False)
apply (cases "fixInterval interv ista")
apply (simp only:IntervalResult.case Let_def)
subgoal for fIenv3 fIsta3
apply (cases "applyAllInputs fIenv3 fIsta3 icont rest")
apply (simp only:ApplyAllResult.case)
subgoal for reducedAfter3 cwa3 pa3 sta3 con3
apply (cases "\<not> reducedAfter3 \<and> (icont \<noteq> Close \<or> accounts ista = [])")
apply (simp del:fixInterval.simps computeTransaction.simps applyAllInputs.simps only:refl if_False)
apply (smt ApplyAllResult.inject IntervalResult.inject(1) TransactionOutput.inject(1) TransactionOutputRecord.ext_inject applyAllIterative fixIntervalIdempotentThroughApplyAllInputs)
using computeTransactionIterative_aux by auto
apply (simp only:ApplyAllResult.case)
apply (metis ApplyAllResult.distinct(1) IntervalResult.inject(1) TransactionOutput.inject(1) TransactionOutputRecord.ext_inject applyAllIterative fixIntervalIdempotentThroughApplyAllInputs)
apply (simp only:ApplyAllResult.case)
by (metis ApplyAllResult.distinct(3) IntervalResult.inject(1) TransactionOutput.inject(1) TransactionOutputRecord.ext_inject applyAllIterative fixIntervalIdempotentThroughApplyAllInputs)
by (simp add: fixIntervalIdempotentThroughApplyAllInputs)
apply simp
by simp
subgoal for err2
apply (cases "applyAllInputs fIenv1 fIsta1 con (head # rest)")
apply (simp del:fixInterval.simps computeTransaction.simps applyAllInputs.simps)
apply (metis (no_types, lifting) IntervalResult.distinct(1) TransactionOutput.distinct(1) TransactionOutput.inject(1) TransactionOutputRecord.select_convs(3) fixIntervalIdempotentThroughApplyAllInputs)
apply simp
by simp
done
apply simp
by simp
by simp
lemma applyAllInputs_prefix_error :
"a = ApplyAllAmbiguousTimeIntervalError \<or> a = ApplyAllNoMatchError \<Longrightarrow>
applyAllInputs env fixSta txOutCont [head] = a \<Longrightarrow>
applyAllInputs env fixSta txOutCont (head # tail) = a"
apply (simp only:applyAllInputs.simps applyAllLoop.simps[of False env fixSta txOutCont])
apply (cases "reduceContractUntilQuiescent env fixSta txOutCont")
subgoal for reduceReduced reduceWarns pays curState cont
apply (simp only:ReduceResult.case list.case)
apply (cases "applyInput env curState head cont")
subgoal for applyWarn newState cont2
apply (simp only:ApplyResult.case)
apply (simp only:applyAllLoop.simps[of True env newState cont2])
apply (cases "reduceContractUntilQuiescent env newState cont2")
subgoal for reduceWarns3 pays3 curState3 cont3
apply (simp only:ReduceResult.case list.case)
by blast
by simp
by simp
by simp
lemma applyAllInputs_noEmpty_changes_contract :
"applyAllInputs env fixSta txOutCont (head # []) = ApplyAllSuccess reduced warnings payments newState cont \<Longrightarrow>
reduced"
apply (simp del:reduceContractUntilQuiescent.simps)
apply (cases "reduceContractUntilQuiescent env fixSta txOutCont")
subgoal for reduceReduced reduceWarns reducePays reduceState reduceCont
apply (simp only:ReduceResult.case list.case)
apply (cases "reduceCont = txOutCont")
apply (cases "applyInput env reduceState head reduceCont")
subgoal for applyWarn applyState applyCont
apply (simp only:ApplyResult.case)
using applyAllLoop_preserves_reduced by blast
apply simp
apply (cases "applyInput env reduceState head reduceCont")
subgoal for applyWarn applyState applyCont
apply (simp only:ApplyResult.case)
apply (drule reduceContractUntilQuiescent_only_makes_smaller[of reduceCont txOutCont env fixSta reduceReduced reduceWarns reducePays reduceState])
apply simp
using applyAllLoop_preserves_reduced by blast
by simp
by simp
lemma computeTransaction_prefix_error :
"computeTransaction \<lparr>interval = interv, inputs = [head]\<rparr> txOutStat txOutCont = TransactionError x \<Longrightarrow>
computeTransaction \<lparr>interval = interv, inputs = head # tail\<rparr> txOutStat txOutCont = TransactionError x"
apply (simp del:fixInterval.simps applyAllInputs.simps)
apply (cases "fixInterval interv txOutStat")
subgoal for env fixSta
apply (simp only:IntervalResult.case Let_def)
apply (cases "applyAllInputs env fixSta txOutCont [head]")
subgoal for reduced warnings payments newState cont
apply (simp only:ApplyAllResult.case)
apply (cases "applyAllInputs env fixSta txOutCont (head # tail)")
subgoal for reduced2 warnings2 payments2 newState2 cont2
apply (simp only:ApplyAllResult.case)
apply (cases "\<not> reduced \<and> (txOutCont \<noteq> Close \<or> accounts txOutStat = [])")
apply (cases "\<not> reduced2 \<and> (txOutCont \<noteq> Close \<or> accounts txOutStat = [])")
apply simp
apply (simp only:if_True bool_simps)
using applyAllInputs_noEmpty_changes_contract apply blast
by auto
apply (simp only:ApplyAllResult.case)
using applyAllInputs_noEmpty_changes_contract apply fastforce
using applyAllInputs_noEmpty_changes_contract by fastforce
apply (metis (no_types, lifting) applyAllInputs_prefix_error)
by (metis (no_types, lifting) applyAllInputs_prefix_error)
by simp
lemma fixInterval_doesnt_care_about_inputs :
"fixInterval (interval \<lparr>interval = interv, inputs = inp1\<rparr>) sta = IntervalTrimmed env fixSta \<Longrightarrow>
fixInterval (interval \<lparr>interval = interv, inputs = inp2\<rparr>) sta = IntervalTrimmed env fixSta"
by simp
lemma fixInterval_idemp_on_same_minTime :
"fixInterval interv sta = IntervalTrimmed env fixSta \<Longrightarrow>
minTime fixSta = minTime ista \<Longrightarrow>
fixInterval interv ista = IntervalTrimmed env ista"
apply (cases sta)
apply (cases ista)
apply (cases interv)
apply simp
by (smt IntervalResult.distinct(1) IntervalResult.inject(1) State.select_convs(4))
lemma fixInterval_idemp_after_computeTransaction :
"fixInterval interv sta = IntervalTrimmed env fixSta \<Longrightarrow>
reduceContractUntilQuiescent env fixSta con = ContractQuiescent reduceReduced reduceWarns pays curState cont \<Longrightarrow>
applyInput env curState head cont = Applied applyWarn newState cont2 \<Longrightarrow>
reduceContractUntilQuiescent env newState cont2 = ContractQuiescent reduceReduced2 reduceWarns2 pays2 ista icont \<Longrightarrow>
fixInterval interv ista = IntervalTrimmed env ista"
by (simp add: applyInput_preserves_minTime fixInterval_idemp_on_same_minTime reductionLoop_preserves_minTime)
lemma applyAllLoop_independent_of_acc_error1 :
"applyAllLoop reducedBefore env sta cont htail wa pa = ApplyAllNoMatchError \<Longrightarrow>
applyAllLoop reducedBefore env sta cont htail wa2 pa2 = ApplyAllNoMatchError"
apply (induction htail arbitrary: reducedBefore env sta cont wa pa wa2 pa2)
apply (force split:ReduceResult.split)
subgoal for head tail reducedBefore env sta cont wa pa wa2 pa2
apply (simp only:applyAllLoop.simps[of reducedBefore env sta cont "head # tail"])
by (auto split:ReduceResult.split ApplyResult.split simp del:applyAllLoop.simps)
done
lemma applyAllLoop_independent_of_acc_error2 :
"applyAllLoop reducedBefore env sta cont htail wa pa = ApplyAllAmbiguousTimeIntervalError \<Longrightarrow>
applyAllLoop reducedBefore env sta cont htail wa2 pa2 = ApplyAllAmbiguousTimeIntervalError"
apply (induction htail arbitrary: reducedBefore env sta cont wa pa wa2 pa2)
apply (force split:ReduceResult.split)
subgoal for head tail reducedBefore env sta cont wa pa wa2 pa2
apply (simp only:applyAllLoop.simps[of reducedBefore env sta cont "head # tail"])
by (auto split:ReduceResult.split ApplyResult.split simp del:applyAllLoop.simps)
done
lemma computeTransactionStepEquivalence_error :
"rest \<noteq> [] \<Longrightarrow>
computeTransaction \<lparr>interval = interv, inputs = [head]\<rparr> sta con
= TransactionOutput \<lparr> txOutWarnings = iwa