-
Notifications
You must be signed in to change notification settings - Fork 0
/
Interval_Arithmetic.thy
5043 lines (4922 loc) · 255 KB
/
Interval_Arithmetic.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 Interval_Arithmetic
imports
Complex_Main
Word_Lib.Word_Lib
Word_Lib.Word_Lemmas
"./Syntax"
begin
unbundle word_notation
type_synonym word = "32 Word.word"
type_synonym rstate = "ident \<Rightarrow> real"
type_synonym wstate = "(ident + ident) \<Rightarrow> word"
definition word::"word \<Rightarrow> bool"
where word_def[simp]:"word w \<equiv> w \<in> {NEG_INF..POS_INF}"
definition wstate::"wstate \<Rightarrow> prop"
where wstate_def[simp]:"wstate \<nu> \<equiv> (\<And>i. word (\<nu> (Inl i)) \<and> word (\<nu> (Inr i)))"
named_theorems rep_simps "Simplifications for representation functions"
(* Note: 0x80000000 is never used. This way there's no awkward asymmetry but I can still use existing
* support for 2's complement *)
inductive repe ::"word \<Rightarrow> real \<Rightarrow> bool" (infix "\<equiv>\<^sub>E" 10)
where
repPOS_INF:"r \<ge> real_of_int (sint POS_INF) \<Longrightarrow> repe POS_INF r"
| repNEG_INF:"r \<le> real_of_int (sint NEG_INF) \<Longrightarrow> repe NEG_INF r"
| repINT: "(sint w) < real_of_int(sint POS_INF) \<Longrightarrow> (sint w) > real_of_int(sint NEG_INF) \<Longrightarrow> repe w (sint w)"
inductive_simps
repePos_simps[rep_simps]:"repe POS_INF r"
and repeNeg_simps[rep_simps]:"repe NEG_INF r"
and repeInt_simps[rep_simps]:"repe w (sint w)"
definition repU ::"word \<Rightarrow> real \<Rightarrow> bool" (infix "\<equiv>\<^sub>U" 10)
where "repU w r \<equiv> \<exists> r'. r' \<ge> r \<and> repe w r'"
lemma repU_leq:"repU w r \<Longrightarrow> r' \<le> r \<Longrightarrow> repU w r'"
unfolding repU_def
using order_trans by auto
definition repL ::"word \<Rightarrow> real \<Rightarrow> bool" (infix "\<equiv>\<^sub>L" 10)
where "repL w r \<equiv> \<exists> r'. r' \<le> r \<and> repe w r'"
lemma repL_geq:"repL w r \<Longrightarrow> r' \<ge> r \<Longrightarrow> repL w r'"
unfolding repL_def
using order_trans by auto
definition repP ::"word * word \<Rightarrow> real \<Rightarrow> bool" (infix "\<equiv>\<^sub>P" 10)
where "repP w r \<equiv> let (w1, w2) = w in repL w1 r \<and> repU w2 r"
inductive rtsem :: "trm \<Rightarrow> rstate \<Rightarrow> real \<Rightarrow> bool" ("([_]_ \<down> _)" 10)
where
rtsem_Const:"Rep_bword w \<equiv>\<^sub>E r \<Longrightarrow> ([Const w]\<nu> \<down> r)"
| rtsem_Var:"([Var x]\<nu> \<down> \<nu> x)"
| rtsem_Plus:"\<lbrakk>([\<theta>\<^sub>1]\<nu> \<down> r\<^sub>1); ([\<theta>\<^sub>2]\<nu> \<down> r\<^sub>2)\<rbrakk> \<Longrightarrow> ([Plus \<theta>\<^sub>1 \<theta>\<^sub>2]\<nu> \<down> (r\<^sub>1 + r\<^sub>2))"
| rtsem_Times:"\<lbrakk>([\<theta>\<^sub>1]\<nu> \<down> r\<^sub>1); ([\<theta>\<^sub>2]\<nu> \<down> r\<^sub>2)\<rbrakk> \<Longrightarrow> ([Times \<theta>\<^sub>1 \<theta>\<^sub>2]\<nu> \<down> (r\<^sub>1 * r\<^sub>2))"
| rtsem_Div:"\<lbrakk>([\<theta>\<^sub>1]\<nu> \<down> r\<^sub>1); ([\<theta>\<^sub>2]\<nu> \<down> r\<^sub>2)\<rbrakk> \<Longrightarrow> ([Div \<theta>\<^sub>1 \<theta>\<^sub>2]\<nu> \<down> (r\<^sub>1 / r\<^sub>2))"
| rtsem_Max:"\<lbrakk>([\<theta>\<^sub>1]\<nu> \<down> r\<^sub>1); ([\<theta>\<^sub>2]\<nu> \<down> r\<^sub>2)\<rbrakk> \<Longrightarrow> ([Max \<theta>\<^sub>1 \<theta>\<^sub>2]\<nu> \<down> (max r\<^sub>1 r\<^sub>2))"
| rtsem_Min:"\<lbrakk>([\<theta>\<^sub>1]\<nu> \<down> r\<^sub>1); ([\<theta>\<^sub>2]\<nu> \<down> r\<^sub>2)\<rbrakk> \<Longrightarrow> ([Min \<theta>\<^sub>1 \<theta>\<^sub>2]\<nu> \<down> (min r\<^sub>1 r\<^sub>2))"
| rtsem_Abs:"\<lbrakk>([\<theta>\<^sub>1]\<nu> \<down> r\<^sub>1)\<rbrakk> \<Longrightarrow> ([Abs \<theta>\<^sub>1]\<nu> \<down> (abs r\<^sub>1))"
| rtsem_Neg:"([\<theta>]\<nu> \<down> r) \<Longrightarrow> ([Neg \<theta>]\<nu> \<down> -r)"
inductive_simps
rtsem_Const_simps[simp] : "([(Const w)]\<nu> \<down> r)"
and rtsem_Var_simps[simp] : "([Var x]\<nu> \<down> r)"
and rtsem_PlusU_simps[simp] : "([Plus \<theta>\<^sub>1 \<theta>\<^sub>2]\<nu> \<down> r)"
and rtsem_TimesU_simps[simp] : "([Times \<theta>\<^sub>1 \<theta>\<^sub>2]\<nu> \<down> r)"
and rtsem_Abs_simps[simp] : "([Abs \<theta>] \<nu> \<down> r)"
and rtsem_Max_simps[simp] : "([Max \<theta>\<^sub>1 \<theta>\<^sub>2] \<nu> \<down> r)"
and rtsem_Min_simps[simp] : "([Min \<theta>\<^sub>1 \<theta>\<^sub>2] \<nu> \<down> r)"
and rtsem_Div_simps[simp] : "([Div \<theta>\<^sub>1 \<theta>\<^sub>2] \<nu> \<down> r)"
and rtsem_Neg_simps[simp] : "([Neg \<theta>] \<nu> \<down> r)"
definition set_less :: "real set \<Rightarrow> real set \<Rightarrow> bool" (infix "<\<^sub>S" 10)
where "set_less A B \<equiv> (\<forall> x y. x \<in> A \<and> y \<in> B \<longrightarrow> x < y)"
definition set_geq :: "real set \<Rightarrow> real set \<Rightarrow> bool" (infix "\<ge>\<^sub>S" 10)
where "set_geq A B \<equiv> (\<forall> x y. x \<in> A \<and> y \<in> B \<longrightarrow> x \<ge> y)"
inductive rfsem :: "formula \<Rightarrow> rstate \<Rightarrow> bool \<Rightarrow> bool" ("([_]_) \<downharpoonright> _" 20)
where
rLeT:"\<lbrakk>([\<theta>\<^sub>1]\<nu> \<down> r\<^sub>1); ([\<theta>\<^sub>2]\<nu> \<down> r\<^sub>2)\<rbrakk> \<Longrightarrow> r\<^sub>1 < r\<^sub>2 \<Longrightarrow> ([Le \<theta>\<^sub>1 \<theta>\<^sub>2] \<nu> \<downharpoonright> True)"
| rLeF:"\<lbrakk>([\<theta>\<^sub>1]\<nu> \<down> r\<^sub>1); ([\<theta>\<^sub>2]\<nu> \<down> r\<^sub>2)\<rbrakk> \<Longrightarrow> r\<^sub>1 \<ge> r\<^sub>2 \<Longrightarrow> ([Le \<theta>\<^sub>1 \<theta>\<^sub>2] \<nu> \<downharpoonright> False)"
| rLeqT:"\<lbrakk>([\<theta>\<^sub>1]\<nu> \<down> r\<^sub>1); ([\<theta>\<^sub>2]\<nu> \<down> r\<^sub>2)\<rbrakk> \<Longrightarrow> r\<^sub>1 \<le> r\<^sub>2 \<Longrightarrow> ([Leq \<theta>\<^sub>1 \<theta>\<^sub>2] \<nu> \<downharpoonright> True)"
| rLeqF:"\<lbrakk>([\<theta>\<^sub>1]\<nu> \<down> r\<^sub>1); ([\<theta>\<^sub>2]\<nu> \<down> r\<^sub>2)\<rbrakk> \<Longrightarrow> r\<^sub>1 > r\<^sub>2 \<Longrightarrow> ([Leq \<theta>\<^sub>1 \<theta>\<^sub>2] \<nu> \<downharpoonright> False)"
| rEqualsT:"\<lbrakk>([\<theta>\<^sub>1]\<nu> \<down> r\<^sub>1); ([\<theta>\<^sub>2]\<nu> \<down> r\<^sub>2)\<rbrakk> \<Longrightarrow> r\<^sub>1 = r\<^sub>2 \<Longrightarrow> ([Equals \<theta>\<^sub>1 \<theta>\<^sub>2] \<nu> \<downharpoonright> True)"
| rEqualsF:"\<lbrakk>([\<theta>\<^sub>1]\<nu> \<down> r\<^sub>1); ([\<theta>\<^sub>2]\<nu> \<down> r\<^sub>2)\<rbrakk> \<Longrightarrow> r\<^sub>1 \<noteq> r\<^sub>2 \<Longrightarrow> ([Equals \<theta>\<^sub>1 \<theta>\<^sub>2] \<nu> \<downharpoonright> False)"
| rAndT:"\<lbrakk>([\<phi>]\<nu> \<downharpoonright> True); ([\<psi>]\<nu> \<downharpoonright> True)\<rbrakk> \<Longrightarrow> ([And \<phi> \<psi>]\<nu> \<downharpoonright> True)"
| rAndF1:"([\<phi>]\<nu> \<downharpoonright> False) \<Longrightarrow> ([And \<phi> \<psi>]\<nu> \<downharpoonright> False)"
| rAndF2:"([\<psi>]\<nu> \<downharpoonright> False) \<Longrightarrow> ([And \<phi> \<psi>]\<nu> \<downharpoonright> False)"
| rOrT1:"([\<phi>]\<nu> \<downharpoonright> True) \<Longrightarrow> ([Or \<phi> \<psi>]\<nu> \<downharpoonright> True)"
| rOrT2:"([\<psi>]\<nu> \<downharpoonright> True) \<Longrightarrow> ([Or \<phi> \<psi>]\<nu> \<downharpoonright> True)"
| rOrF:"\<lbrakk>([\<phi>]\<nu> \<downharpoonright> False) ;([\<psi>]\<nu> \<downharpoonright> False)\<rbrakk> \<Longrightarrow> ([And \<phi> \<psi>]\<nu> \<downharpoonright> False)"
| rNotT:"([\<phi>]\<nu> \<downharpoonright> False) \<Longrightarrow> ([(Not \<phi>)]\<nu> \<downharpoonright> True)"
| rNotF:"([\<phi>]\<nu> \<downharpoonright> True) \<Longrightarrow> ([(Not \<phi>)]\<nu> \<downharpoonright> False)"
inductive_simps
rfsem_Gr_simps[simp]: "([Le \<theta>\<^sub>1 \<theta>\<^sub>2]\<nu> \<downharpoonright> b)"
and rfsem_Leq_simps[simp]: "([Leq \<theta>\<^sub>1 \<theta>\<^sub>2]\<nu> \<downharpoonright> b)"
and rfsem_Equals_simps[simp]: "([Equals \<theta>\<^sub>1 \<theta>\<^sub>2]\<nu> \<downharpoonright> b)"
and rfsem_And_simps[simp]: "([And \<phi> \<psi>]\<nu> \<downharpoonright> b)"
and rfsem_Or_simps[simp]: "([(Or \<phi> \<psi>)]\<nu> \<downharpoonright> b)"
and rfsem_Not_simps[simp]: "([Not \<phi>]\<nu> \<downharpoonright> b)"
inductive rpsem :: "hp \<Rightarrow> rstate \<Rightarrow> rstate \<Rightarrow> bool" ("([_]_) \<downharpoonleft> _" 20)
where
rTest[simp]:"\<lbrakk>([\<phi>]\<nu> \<downharpoonright> True); \<nu> = \<omega>\<rbrakk> \<Longrightarrow> ([? \<phi>]\<nu> \<downharpoonleft> \<omega>)"
| rSeq[simp]:"\<lbrakk>([\<alpha>]\<nu> \<downharpoonleft> \<mu>); ([\<beta>]\<mu> \<downharpoonleft> \<omega>)\<rbrakk> \<Longrightarrow> ([\<alpha>;; \<beta>]\<nu> \<downharpoonleft> \<omega>)"
| rAssign[simp]:"\<lbrakk>([\<theta>]\<nu> \<down> r); \<omega> = (\<nu> (x := r))\<rbrakk> \<Longrightarrow> ([Assign x \<theta>]\<nu> \<downharpoonleft> \<omega>)"
| rChoice1[simp]:"([\<alpha>]\<nu> \<downharpoonleft> \<omega>) \<Longrightarrow> ([Choice \<alpha> \<beta>]\<nu> \<downharpoonleft> \<omega>)"
| rChoice2[simp]:"([\<beta>]\<nu> \<downharpoonleft> \<omega>) \<Longrightarrow> ([Choice \<alpha> \<beta>]\<nu> \<downharpoonleft> \<omega>)"
inductive_simps
rpsem_Test_simps[simp]: "([? \<phi>]\<nu> \<downharpoonleft> b)"
and rpsem_Seq_simps[simp]: "([\<alpha>;; \<beta>]\<nu> \<downharpoonleft> b)"
and rpsem_Assign_simps[simp]: "([Assign x \<theta>]\<nu> \<downharpoonleft> b)"
and rpsem_Choice_simps[simp]: "([Choice \<alpha> \<beta>]\<nu> \<downharpoonleft> b)"
lemma int_not_posinf:
assumes b1:"real_of_int (sint ra) < real_of_int (sint POS_INF)"
assumes b2:"real_of_int (sint NEG_INF) < real_of_int (sint ra)"
shows "ra \<noteq> POS_INF"
using b1 b2 unfolding POS_INF_def NEG_INF_def by auto
lemma int_not_neginf:
assumes b1:" real_of_int (sint ra) < real_of_int (sint POS_INF)"
assumes b2:" real_of_int (sint NEG_INF) < real_of_int (sint ra)"
shows "ra \<noteq> NEG_INF"
using b1 b2 unfolding POS_INF_def NEG_INF_def by auto
lemma int_not_undef:
assumes b1:"real_of_int (sint ra) < real_of_int (sint POS_INF)"
assumes b2:"real_of_int (sint NEG_INF) < real_of_int (sint ra)"
shows "ra \<noteq> NEG_INF-1"
using b1 b2 unfolding POS_INF_def NEG_INF_def by auto
lemma sint_range:
assumes b1:"real_of_int (sint ra) < real_of_int (sint POS_INF)"
assumes b2:"real_of_int (sint NEG_INF) < real_of_int (sint ra)"
shows "sint ra \<in> {i. i > -((2^31)-1) \<and> i < (2^31)-1}"
using b1 b2 unfolding POS_INF_def NEG_INF_def by auto
lemma word_size_neg:
fixes w :: "32 Word.word"
shows "size (-w) = size w"
using Word.word_size[of w] Word.word_size[of "-w"] by auto
lemma uint_distinct:
fixes w1 w2
assumes foo:"w1 \<noteq> w2"
shows "uint w1 \<noteq> uint w2"
using foo by auto
fun pu :: "word \<Rightarrow> word \<Rightarrow> word"
where "pu w1 w2 =
(if w1 = POS_INF then POS_INF
else if w2 = POS_INF then POS_INF
else if w1 = NEG_INF then
(if w2 = NEG_INF then NEG_INF
else
(let sum::64 Word.word = ((scast w2)::64 Word.word) + ((scast NEG_INF)::64 Word.word) in
if (sum::64 Word.word) <=s ((scast NEG_INF)::64 Word.word) then NEG_INF
else scast sum))
else if w2 = NEG_INF then
(let sum::64 Word.word = ((scast w1)::64 Word.word) + ((scast NEG_INF)::64 Word.word) in
if (sum::64 Word.word) <=s ((scast NEG_INF)::64 Word.word) then NEG_INF
else scast sum)
else
(let sum::64 Word.word = ((scast w1)::64 Word.word) + ((scast w2)::64 Word.word) in
if ((scast POS_INF)::64 Word.word) <=s (sum::64 Word.word) then POS_INF
else if (sum::64 Word.word) <=s ((scast NEG_INF)::64 Word.word) then NEG_INF
else scast sum))"
lemma scast_down_range:
fixes w::"'a::len Word.word"
assumes "sint w \<in> sints (len_of (TYPE('b::len)))"
shows "sint w = sint ((scast w)::'b Word.word)"
unfolding scast_def
by (simp add: assms word_sint.Abs_inverse)
lemma pu_lemma:
assumes up1:"w\<^sub>1 \<equiv>\<^sub>U (r\<^sub>1::real)"
assumes up2:"w\<^sub>2 \<equiv>\<^sub>U (r\<^sub>2::real)"
shows "pu w\<^sub>1 w\<^sub>2 \<equiv>\<^sub>U (r\<^sub>1 + r\<^sub>2)"
apply(cases "w\<^sub>1 = POS_INF")
subgoal
apply (auto simp add: POS_INF_def repU_def repe.simps NEG_INF_def)
using linear by blast
apply(cases "w\<^sub>2 = POS_INF")
subgoal
apply (auto simp add: POS_INF_def repU_def repe.simps NEG_INF_def)
using linear by blast
apply(cases "w\<^sub>1 = NEG_INF")
subgoal
apply(cases "w\<^sub>2 = NEG_INF")
subgoal
using up1 up2
by (auto simp add: POS_INF_def NEG_INF_def repU_def repe.simps)
subgoal
apply(simp)
proof -
assume neq1:"w\<^sub>2 \<noteq> POS_INF"
assume eq2:"w\<^sub>1 = NEG_INF"
assume neq3:"w\<^sub>2 \<noteq> NEG_INF"
let ?sum = "(scast w\<^sub>2 + scast NEG_INF)::64 Word.word"
have scast_eq1:"sint((scast w\<^sub>1)::64 Word.word) = sint w\<^sub>1"
apply(rule Word.sint_up_scast)
unfolding Word.is_up by auto
have scast_eq3:"sint((scast w\<^sub>2)::64 Word.word) = sint w\<^sub>2"
apply(rule Word.sint_up_scast)
unfolding Word.is_up by auto
have scast_eq2:"sint((scast (0x80000001::word))::64 Word.word) = sint ((0x80000001::32 Word.word))"
by auto
have sints64:"sints 64 = {i. - (2 ^ 63) \<le> i \<and> i < 2 ^ 63}"
using sints_def[of 64] range_sbintrunc[of 63] by auto
have sints32:"sints 32 = {i. - (2 ^ 31) \<le> i \<and> i < 2 ^ 31}"
using sints_def[of 32] range_sbintrunc[of 31] by auto
have thing1:"0 \<le> 9223372034707292161 + ((-(2 ^ 31))::real)" by auto
have thing2:"sint ((scast w\<^sub>2)::64 Word.word) \<ge> - (2 ^ 31) "
using Word.word_sint.Rep[of "(w\<^sub>2)::32 Word.word"] sints32
Word.word_size[of "(scast w\<^sub>2)::64 Word.word"] scast_eq1 scast_eq2 scast_eq3 len32 mem_Collect_eq
by auto
have aLeq:"2 ^ 31 < (9223372039002259455::int)" by auto
have bLeq:"sint ((scast w\<^sub>2)::64 Word.word) \<le> 2 ^ 31"
apply ( auto simp add: Word.word_sint.Rep[of "(w\<^sub>2)::32 Word.word"] sints32
scast_eq3 len32)
using Word.word_sint.Rep[of "(w\<^sub>2)::32 Word.word"] len32[of "TYPE(32)"] sints32 by auto
have thing3:"sint ((scast w\<^sub>2)::64 Word.word) < 9223372039002259455"
using aLeq bLeq by auto
have truth:" - (2 ^ (size ((scast w\<^sub>2)::64 Word.word) - 1)) \<le> sint ((scast w\<^sub>2)::64 Word.word) + sint ((-0x7FFFFFFF)::64 Word.word) \<and> sint ((scast w\<^sub>2)::64 Word.word) + sint ((-0x7FFFFFFF)::64 Word.word) \<le> 2 ^ (size ((scast w\<^sub>2)::64 Word.word) - 1) - 1"
apply(auto simp add:
Word.word_size[of "(scast w\<^sub>2)::64 Word.word"] Word.word_size[of "(scast (-0x7FFFFFFF))::64 Word.word"]
scast_eq1 scast_eq2
Word.word_sint.Rep[of "(w\<^sub>2)::32 Word.word"]
Word.word_sint.Rep[of "0x80000001::32 Word.word"]
Word.word_sint.Rep[of "(scast w\<^sub>2)::64 Word.word"]
Word.word_sint.Rep[of "-0x7FFFFFFF::64 Word.word"]
sints64 sints32 thing2)
using thing1 thing2 thing3 by auto
have case1a:" sint (((scast w\<^sub>2)::64 Word.word) + (-0x7FFFFFFF::64 Word.word)) = sint ((scast w\<^sub>2)::64 Word.word) + sint (-0x7FFFFFFF::64 Word.word)"
by(rule signed_arith_sint(1)[OF truth])
have case1b:"sint ((0xFFFFFFFF80000001)::64 Word.word) < 0"
by auto
have case1:"?sum <=s ((scast NEG_INF)::64 Word.word) \<Longrightarrow> NEG_INF \<equiv>\<^sub>U r\<^sub>1 + r\<^sub>2"
using up1 up2 apply (simp add: repU_def NEG_INF_def repe.simps POS_INF_def word_sle_def)
apply(rule exI[where x= "r\<^sub>1 + r\<^sub>2"])
apply(auto)
using case1a case1b
apply (auto simp add: NEG_INF_def neq1 eq2 neq3 repINT repU_def repe.simps repeInt_simps up2 word_sless_alt)
using repINT repU_def repe.simps repeInt_simps up2 word_sless_alt POS_INF_def NEG_INF_def apply (auto simp add: POS_INF_def NEG_INF_def)
proof -
fix r'
assume a1:"sint ((scast w\<^sub>2)::64 Word.word) \<le> 0"
then have h3:"sint w\<^sub>2 \<le> 0" using scast_eq3 by auto
assume a2:"r\<^sub>1 \<le> r'"
assume a3:"r\<^sub>2 \<le> (real_of_int (sint w\<^sub>2))"
assume a4:"r' \<le> (- 2147483647)"
assume a5:"sint w\<^sub>2 < 2147483647"
assume a6:"- 2147483647 < real_of_int (sint w\<^sub>2)"
assume a7:"sint (scast w\<^sub>2 + 0xFFFFFFFF80000001) = sint (scast w\<^sub>2) - 2147483647"
from a2 a4 have h1:"r\<^sub>1 \<le> - 2147483647" by auto
from a1 a3 h3 have h2:"r\<^sub>2 \<le> 0"
using dual_order.trans of_int_le_0_iff by blast
show "r\<^sub>1 + r\<^sub>2 \<le> (- 2147483647)"
using h1 h2 add.right_neutral add_mono by fastforce
qed
obtain r'\<^sub>1 and r'\<^sub>2 where
geq1:"r'\<^sub>1\<ge>r\<^sub>1" and equiv1:"w\<^sub>1 \<equiv>\<^sub>E r'\<^sub>1"
and geq2:"r'\<^sub>2\<ge>r\<^sub>2" and equiv2:"w\<^sub>2 \<equiv>\<^sub>E r'\<^sub>2"
using up1 up2 unfolding repU_def by auto
have leq1:"r'\<^sub>1 \<le> (real_of_int (sint NEG_INF))"
using equiv1 unfolding repe.simps
using neq1 eq2 neq3 apply auto
subgoal unfolding NEG_INF_def POS_INF_def by auto
done
have leq2:"r'\<^sub>2 = (real_of_int (sint w\<^sub>2))"
using equiv2 unfolding repe.simps
using neq1 eq2 neq3 by auto
have case2:"\<not>(?sum <=s scast NEG_INF) \<Longrightarrow> scast ?sum \<equiv>\<^sub>U r\<^sub>1 + r\<^sub>2"
apply (simp add: repU_def NEG_INF_def repe.simps POS_INF_def word_sle_def up1 up2)
apply(rule exI[where x= "r'\<^sub>2 - 0x7FFFFFFF"]) (*r\<^sub>1 + r\<^sub>2*)
apply(rule conjI)
subgoal
proof -
assume " \<not> sint (scast w\<^sub>2 + 0xFFFFFFFF80000001) \<le> - 2147483647"
have bound1:"r\<^sub>1 \<le> - 2147483647"
using leq1 geq1 by (auto simp add: NEG_INF_def)
have bound2:"r\<^sub>2 \<le> r'\<^sub>2"
using leq2 geq2 by auto
show "r\<^sub>1 + r\<^sub>2 \<le> r'\<^sub>2 - 2147483647"
using bound1 bound2
by(linarith)
qed
apply(rule disjI2)
apply(rule disjI2)
apply(auto)
subgoal
proof -
have g:"(-0x7FFFFFFF::64 Word.word) = 0xFFFFFFFF80000001" by auto
assume a:"\<not> sint (((scast w\<^sub>2)::64 Word.word) + 0xFFFFFFFF80000001) \<le> - 2147483647"
then have sintw2_bound:"sint (((scast w\<^sub>2)::64 Word.word) + (-0x7FFFFFFF)) > - 2147483647"
unfolding g by auto
have case1a:" sint (((scast w\<^sub>2)::64 Word.word) + (-0x7FFFFFFF::64 Word.word)) = sint ((scast w\<^sub>2)::64 Word.word) + sint (-0x7FFFFFFF::64 Word.word)"
by(rule signed_arith_sint(1)[OF truth])
have a1:"sint (((scast w\<^sub>2)::64 Word.word) + (-0x7FFFFFFF)) = sint((scast w\<^sub>2)::64 Word.word) + sint((-0x7FFFFFFF)::64 Word.word)" using case1a by auto
have b1:"sint((scast w\<^sub>2)::64 Word.word) = sint w\<^sub>2"
apply(rule Word.sint_up_scast)
unfolding Word.is_up by auto
have c1:"sint((-0x7FFFFFFF)::64 Word.word) = -0x7FFFFFFF"
by auto
have "- 0x7FFFFFFF < sint w\<^sub>2 + (- 0x7FFFFFFF)"
using sintw2_bound case1a
using c1 scast_eq3 by linarith
then have w2bound:"0 < sint w\<^sub>2"
using less_add_same_cancel2 by blast
have rightSize:"sint (((scast w\<^sub>2)::64 Word.word) + - 0x7FFFFFFF) \<in> sints (len_of TYPE(32))"
unfolding case1a b1 c1
apply ( auto simp add: Word.word_sint.Rep[of "(w\<^sub>2)::32 Word.word"] sints32 len32[of "TYPE(32)"])
defer
subgoal using Word.word_sint.Rep[of "(w\<^sub>2)::32 Word.word"] by ( auto simp add: sints32 len32[of "TYPE(32)"])
using w2bound by auto
have arith:"\<And>x::int. x \<le> 2 ^ 31 - 1 \<Longrightarrow> x + (- 2147483647) < 2147483647"
by auto
have downcast:"sint ((scast (((scast w\<^sub>2)::64 Word.word) + ((- 0x7FFFFFFF))))::word) = sint (((scast w\<^sub>2)::64 Word.word) + ((- 0x7FFFFFFF)::64 Word.word)) "
using scast_down_range[OF rightSize]
by auto
then have b:"sint ((scast (((scast w\<^sub>2)::64 Word.word) + 0xFFFFFFFF80000001))::word) = sint (((scast w\<^sub>2)::64 Word.word) + 0xFFFFFFFF80000001)"
using g by auto
have c:"sint (((scast w\<^sub>2)::64 Word.word) + 0xFFFFFFFF80000001) = sint ((scast w\<^sub>2)::64 Word.word) + sint ((-0x7FFFFFFF)::64 Word.word)"
using g case1a by auto
have d:"sint ((-0x7FFFFFFF)::64 Word.word) = (-0x7FFFFFFF)" by auto
have e:"sint ((scast w\<^sub>2)::64 Word.word) = sint w\<^sub>2"
using scast_eq3 by blast
have f:"r'\<^sub>2 = (real_of_int (sint w\<^sub>2))"
by (simp add: leq2)
show "r'\<^sub>2 - 2147483647 = (real_of_int (sint ((scast (((scast w\<^sub>2)::64 Word.word) + 0xFFFFFFFF80000001))::word)))"
using a b c d e f
proof -
have " (real_of_int (sint ((scast w\<^sub>2)::64 Word.word ) - 2147483647)) = r'\<^sub>2 - (real_of_int 2147483647)"
by (simp add: e leq2)
then show ?thesis
using b c d by(auto)
qed
qed
subgoal
proof -
have truth2a:" - (2 ^ (size ((scast w\<^sub>2)::64 Word.word) - 1)) \<le> sint ((scast w\<^sub>2)::64 Word.word) + sint ((-0x7FFFFFFF)::64 Word.word) \<and> sint ((scast w\<^sub>2)::64 Word.word) + sint ((-0x7FFFFFFF)::64 Word.word) \<le> 2 ^ (size ((scast w\<^sub>2)::64 Word.word) - 1) - 1"
apply(auto simp add:
Word.word_size[of "(scast w\<^sub>2)::64 Word.word"] Word.word_size[of "(scast (-0x7FFFFFFF))::64 Word.word"]
scast_eq1 scast_eq2
Word.word_sint.Rep[of "(w\<^sub>2)::32 Word.word"]
Word.word_sint.Rep[of "0x80000001::32 Word.word"]
Word.word_sint.Rep[of "(scast w\<^sub>2)::64 Word.word"]
Word.word_sint.Rep[of "-0x7FFFFFFF::64 Word.word"]
sints64 sints32 thing2)
using thing1 thing2 thing3 by auto
have case2a:" sint (((scast w\<^sub>2)::64 Word.word) + (-0x7FFFFFFF::64 Word.word)) = sint ((scast w\<^sub>2)::64 Word.word) + sint (-0x7FFFFFFF::64 Word.word)"
by(rule signed_arith_sint(1)[OF truth2a])
have min_cast:"(0xFFFFFFFF80000001::64 Word.word) =((scast (-0x7FFFFFFF::word))::64 Word.word)"
by auto
have neg64:"(((scast w\<^sub>2)::64 Word.word) + 0xFFFFFFFF80000001) = ((scast w\<^sub>2)::64 Word.word) + (-0x7FFFFFFF)" by auto
assume "\<not> sint (((scast w\<^sub>2)::64 Word.word) + 0xFFFFFFFF80000001) \<le> - 2147483647"
then have sintw2_bound:"sint (((scast w\<^sub>2)::64 Word.word) + (-0x7FFFFFFF)) > - 2147483647"
unfolding neg64 by auto
have a:"sint (((scast w\<^sub>2)::64 Word.word) + (-0x7FFFFFFF)) = sint((scast w\<^sub>2)::64 Word.word) + sint((-0x7FFFFFFF)::64 Word.word)" using case2a by auto
have b:"sint((scast w\<^sub>2)::64 Word.word) = sint w\<^sub>2"
apply(rule Word.sint_up_scast)
unfolding Word.is_up by auto
have c:"sint((-0x7FFFFFFF)::64 Word.word) = -0x7FFFFFFF"
by auto
have d:"sint w\<^sub>2 \<le> 2^31 - 1"
using Word.word_sint.Rep[of "(w\<^sub>2)::32 Word.word"]
by ( auto simp add: sints32 len32[of "TYPE(32)"])
have "- 0x7FFFFFFF < sint w\<^sub>2 + (- 0x7FFFFFFF)"
using sintw2_bound case2a
using c scast_eq3 by linarith
then have w2bound:"0 < sint w\<^sub>2"
using less_add_same_cancel2 by blast
have rightSize:"sint (((scast w\<^sub>2)::64 Word.word) + - 0x7FFFFFFF) \<in> sints (len_of TYPE(32))"
unfolding case2a b c
apply ( auto simp add: Word.word_sint.Rep[of "(w\<^sub>2)::32 Word.word"] sints32 len32[of "TYPE(32)"])
defer
subgoal using Word.word_sint.Rep[of "(w\<^sub>2)::32 Word.word"] by ( auto simp add: sints32 len32[of "TYPE(32)"])
using w2bound by auto
have arith:"\<And>x::int. x \<le> 2 ^ 31 - 1 \<Longrightarrow> x + (- 2147483647) < 2147483647"
by auto
have downcast:"sint ((scast (((scast w\<^sub>2)::64 Word.word) + ((- 0x7FFFFFFF))))::word) = sint (((scast w\<^sub>2)::64 Word.word) + ((- 0x7FFFFFFF)::64 Word.word)) "
using scast_down_range[OF rightSize]
by auto
have "sint (scast (((scast w\<^sub>2)::64 Word.word) + (-0x7FFFFFFF))::word) < 2147483647"
unfolding downcast a b c
using arith[of "sint w\<^sub>2", OF d]
by auto
then show "sint (scast (((scast w\<^sub>2)::64 Word.word) + 0xFFFFFFFF80000001)::word) < 2147483647"
by auto
qed
subgoal proof -
assume notLeq:"\<not> sint (((scast w\<^sub>2)::64 Word.word) + 0xFFFFFFFF80000001) \<le> - 2147483647"
then have gr:"sint (((scast w\<^sub>2)::64 Word.word) + 0xFFFFFFFF80000001) > - 2147483647"
by auto
have case2a:" sint (((scast w\<^sub>2)::64 Word.word) + (-0x7FFFFFFF::64 Word.word)) = sint ((scast w\<^sub>2)::64 Word.word) + sint (-0x7FFFFFFF::64 Word.word)"
by(rule signed_arith_sint(1)[OF truth])
have min_cast:"(0xFFFFFFFF80000001::64 Word.word) =((scast (-0x7FFFFFFF::word))::64 Word.word)"
by auto
have neg64:"(((scast w\<^sub>2)::64 Word.word) + 0xFFFFFFFF80000001) = ((scast w\<^sub>2)::64 Word.word) + (-0x7FFFFFFF)" by auto
then have sintw2_bound:"sint (((scast w\<^sub>2)::64 Word.word) + (-0x7FFFFFFF)) > - 2147483647"
unfolding neg64 using notLeq by auto
have a:"sint (((scast w\<^sub>2)::64 Word.word) + (-0x7FFFFFFF)) = sint((scast w\<^sub>2)::64 Word.word) + sint((-0x7FFFFFFF)::64 Word.word)" using case2a by auto
have b:"sint((scast w\<^sub>2)::64 Word.word) = sint w\<^sub>2"
apply(rule Word.sint_up_scast)
unfolding Word.is_up by auto
have c:"sint((-0x7FFFFFFF)::64 Word.word) = -0x7FFFFFFF"
by auto
have d:"sint w\<^sub>2 \<le> 2^31 - 1"
using Word.word_sint.Rep[of "(w\<^sub>2)::32 Word.word"]
by ( auto simp add: sints32 len32[of "TYPE(32)"])
have "- 0x7FFFFFFF < sint w\<^sub>2 + (- 0x7FFFFFFF)"
using sintw2_bound case2a
using c scast_eq3 by linarith
then have w2bound:"0 < sint w\<^sub>2"
using less_add_same_cancel2 by blast
have rightSize:"sint (((scast w\<^sub>2)::64 Word.word) + - 0x7FFFFFFF) \<in> sints (len_of TYPE(32))"
unfolding case2a b c
apply ( auto simp add: Word.word_sint.Rep[of "(w\<^sub>2)::32 Word.word"] sints32 len32[of "TYPE(32)"])
defer
subgoal using Word.word_sint.Rep[of "(w\<^sub>2)::32 Word.word"] by ( auto simp add: sints32 len32[of "TYPE(32)"])
using w2bound by auto
have downcast:"sint ((scast (((scast w\<^sub>2)::64 Word.word) + ((- 0x7FFFFFFF))))::word) = sint (((scast w\<^sub>2)::64 Word.word) + ((- 0x7FFFFFFF)::64 Word.word)) "
using scast_down_range[OF rightSize]
by auto
have negEq:"(0xFFFFFFFF80000001:: 64 Word.word) = ((-0x7FFFFFFF)::64 Word.word)" by auto
have sintEq:" sint ((scast (((scast w\<^sub>2)::64 Word.word) + 0xFFFFFFFF80000001))::word) =
sint (((scast w\<^sub>2)::64 Word.word) + 0xFFFFFFFF80000001) "
using downcast by auto
show "- 2147483647 < real_of_int (sint ((scast (((scast w\<^sub>2)::64 Word.word) + 0xFFFFFFFF80000001))::word))"
unfolding sintEq
using gr of_int_less_iff of_int_minus of_int_numeral by linarith
qed
done
show "(let sum = ?sum in if sum <=s scast NEG_INF then NEG_INF else scast sum) \<equiv>\<^sub>U r\<^sub>1 + r\<^sub>2"
by (auto simp add: Let_def case1 case2)
qed
done
apply(cases "w\<^sub>2 = NEG_INF")
subgoal
apply(simp)
proof -
assume neq1:"w\<^sub>1 \<noteq> POS_INF"
assume eq2:"w\<^sub>2 = NEG_INF"
assume neq3:"w\<^sub>1 \<noteq> NEG_INF"
let ?sum = "(scast w\<^sub>1 + scast NEG_INF)::64 Word.word"
have scast_eq1:"sint((scast w\<^sub>2)::64 Word.word) = sint w\<^sub>2"
apply(rule Word.sint_up_scast)
unfolding Word.is_up by auto
have scast_eq3:"sint((scast w\<^sub>1)::64 Word.word) = sint w\<^sub>1"
apply(rule Word.sint_up_scast)
unfolding Word.is_up by auto
have scast_eq2:"sint((scast (0x80000001::word))::64 Word.word) = sint ((0x80000001::32 Word.word))"
by auto
have sints64:"sints 64 = {i. - (2 ^ 63) \<le> i \<and> i < 2 ^ 63}"
using sints_def[of 64] range_sbintrunc[of 63] by auto
have sints32:"sints 32 = {i. - (2 ^ 31) \<le> i \<and> i < 2 ^ 31}"
using sints_def[of 32] range_sbintrunc[of 31] by auto
have thing1:"0 \<le> 9223372034707292161 + ((-(2 ^ 31))::real)" by auto
have thing2:"sint ((scast w\<^sub>1)::64 Word.word) \<ge> - (2 ^ 31) "
using Word.word_sint.Rep[of "(w\<^sub>1)::32 Word.word"] sints32
Word.word_size[of "(scast w\<^sub>1)::64 Word.word"] scast_eq1 scast_eq2 scast_eq3 len32 mem_Collect_eq
by auto
have aLeq:"2 ^ 31 < (9223372039002259455::int)" by auto
have bLeq:"sint ((scast w\<^sub>1)::64 Word.word) \<le> 2 ^ 31"
apply ( auto simp add: Word.word_sint.Rep[of "(w\<^sub>1)::32 Word.word"] sints32
scast_eq3 len32)
using Word.word_sint.Rep[of "(w\<^sub>1)::32 Word.word"] len32[of "TYPE(32)"] sints32 by auto
have thing3:"sint ((scast w\<^sub>1)::64 Word.word) < 9223372039002259455"
using aLeq bLeq by auto
have truth:" - (2 ^ (size ((scast w\<^sub>1)::64 Word.word) - 1)) \<le> sint ((scast w\<^sub>1)::64 Word.word) + sint ((-0x7FFFFFFF)::64 Word.word)
\<and> sint ((scast w\<^sub>1)::64 Word.word) + sint ((-0x7FFFFFFF)::64 Word.word) \<le> 2 ^ (size ((scast w\<^sub>1)::64 Word.word) - 1) - 1"
apply(auto simp add:
Word.word_size[of "(scast w\<^sub>1)::64 Word.word"] Word.word_size[of "(scast (-0x7FFFFFFF))::64 Word.word"]
scast_eq1 scast_eq2
Word.word_sint.Rep[of "(w\<^sub>1)::32 Word.word"]
Word.word_sint.Rep[of "0x80000001::32 Word.word"]
Word.word_sint.Rep[of "(scast w\<^sub>1)::64 Word.word"]
Word.word_sint.Rep[of "-0x7FFFFFFF::64 Word.word"]
sints64 sints32 thing2)
using thing1 thing2 thing3 by auto
have case1a:" sint (((scast w\<^sub>1)::64 Word.word) + (-0x7FFFFFFF::64 Word.word)) = sint ((scast w\<^sub>1)::64 Word.word) + sint (-0x7FFFFFFF::64 Word.word)"
by (rule signed_arith_sint(1)[of "(scast w\<^sub>1)::64 Word.word" "(- 0x7FFFFFFF)", OF truth])
have case1b:"sint ((0xFFFFFFFF80000001)::64 Word.word) < 0"
by auto
have g:"(-0x7FFFFFFF::64 Word.word) = 0xFFFFFFFF80000001" by auto
have c:"sint (((scast w\<^sub>1)::64 Word.word) + 0xFFFFFFFF80000001) = sint ((scast w\<^sub>1)::64 Word.word) + sint ((-0x7FFFFFFF)::64 Word.word)"
using g case1a by auto
have d:"sint ((-0x7FFFFFFF)::64 Word.word) = (-0x7FFFFFFF)" by auto
have e:"sint ((scast w\<^sub>1)::64 Word.word) = sint w\<^sub>1"
using scast_eq3 by blast
have d2:"sint w\<^sub>1 \<le> 2^31 - 1"
using Word.word_sint.Rep[of "(w\<^sub>1)::32 Word.word"]
by ( auto simp add: sints32 len32[of "TYPE(32)"])
have case1:"?sum <=s ((scast NEG_INF)::64 Word.word) \<Longrightarrow> NEG_INF \<equiv>\<^sub>U r\<^sub>1 + r\<^sub>2"
using up1 up2 apply (simp add: repU_def NEG_INF_def repe.simps POS_INF_def word_sle_def)
apply(rule exI[where x= "r\<^sub>1 + r\<^sub>2"])
apply(auto)
using case1a case1b
apply (auto simp add: NEG_INF_def neq1 eq2 neq3 repINT repU_def repe.simps repeInt_simps up2 word_sless_alt)
using repINT repU_def repe.simps repeInt_simps up2 word_sless_alt
proof -
fix r'
assume a1:"sint ((scast w\<^sub>1)::64 Word.word) \<le> 0"
then have h3:"sint w\<^sub>1 \<le> 0" using scast_eq3 by auto
assume a2:"r\<^sub>2 \<le> r'"
assume a3:"r\<^sub>1 \<le> (real_of_int (sint w\<^sub>1))"
assume a4:"r' \<le> (- 2147483647)"
assume a5:"sint w\<^sub>1 < 2147483647"
assume a6:"- 2147483647 < real_of_int (sint w\<^sub>1)"
assume a7:"sint (scast w\<^sub>1 + 0xFFFFFFFF80000001) = sint (scast w\<^sub>1) - 2147483647"
from a2 a4 have h1:"r\<^sub>2 \<le> - 2147483647" by auto
from a1 a3 h3 have h2:"r\<^sub>1 \<le> 0"
using dual_order.trans of_int_le_0_iff by blast
show "r\<^sub>1 + r\<^sub>2 \<le> (- 2147483647)"
using h1 h2 add.right_neutral add_mono by fastforce
qed
obtain r'\<^sub>1 and r'\<^sub>2 where
geq1:"r'\<^sub>1\<ge>r\<^sub>1" and equiv1:"w\<^sub>1 \<equiv>\<^sub>E r'\<^sub>1"
and geq2:"r'\<^sub>2\<ge>r\<^sub>2" and equiv2:"w\<^sub>2 \<equiv>\<^sub>E r'\<^sub>2"
using up1 up2 unfolding repU_def by auto
have leq1:"r'\<^sub>2 \<le> (real_of_int (sint NEG_INF))" and leq2:"r'\<^sub>1 = (real_of_int (sint w\<^sub>1))"
using equiv1 equiv2 unfolding repe.simps
using neq1 eq2 neq3 by auto
have case1a:" sint (((scast w\<^sub>1)::64 Word.word) + (-0x7FFFFFFF::64 Word.word)) = sint ((scast w\<^sub>1)::64 Word.word) + sint (-0x7FFFFFFF::64 Word.word)"
by(rule signed_arith_sint(1)[OF truth])
have neg64:"(((scast w\<^sub>1)::64 Word.word) + 0xFFFFFFFF80000001) = ((scast w\<^sub>1)::64 Word.word) + (-0x7FFFFFFF)" by auto
have case2:"\<not>(?sum <=s scast NEG_INF) \<Longrightarrow> scast ?sum \<equiv>\<^sub>U r\<^sub>1 + r\<^sub>2"
apply (simp add: repU_def NEG_INF_def repe.simps POS_INF_def word_sle_def up1 up2)
apply(rule exI[where x= "r'\<^sub>1 - 0x7FFFFFFF"]) (*r\<^sub>1 + r\<^sub>2*)
apply(rule conjI)
subgoal using leq1 leq2 geq1 geq2 unfolding NEG_INF_def by auto
apply(rule disjI2)
apply(rule disjI2)
apply(auto)
subgoal
proof -
have f:"r'\<^sub>1 = (real_of_int (sint w\<^sub>1))"
by (simp add: leq1 leq2 )
assume a:"\<not> sint (((scast w\<^sub>1)::64 Word.word) + 0xFFFFFFFF80000001) \<le> - 2147483647"
then have sintw2_bound:"sint (((scast w\<^sub>1)::64 Word.word) + (-0x7FFFFFFF)) > - 2147483647"
unfolding g by auto
have "- 0x7FFFFFFF < sint w\<^sub>1 + (- 0x7FFFFFFF)"
using sintw2_bound case1a
using d scast_eq3 by linarith
then have w2bound:"0 < sint w\<^sub>1"
using less_add_same_cancel2 by blast
have rightSize:"sint (((scast w\<^sub>1)::64 Word.word) + - 0x7FFFFFFF) \<in> sints (len_of TYPE(32))"
unfolding case1a e
using w2bound Word.word_sint.Rep[of "(w\<^sub>1)::32 Word.word"]
by ( auto simp add: sints32 len32[of "TYPE(32)"] )
have arith:"\<And>x::int. x \<le> 2 ^ 31 - 1 \<Longrightarrow> x + (- 2147483647) < 2147483647"
by auto
have downcast:"sint ((scast (((scast w\<^sub>1)::64 Word.word) + ((- 0x7FFFFFFF))))::word) = sint (((scast w\<^sub>1)::64 Word.word) + ((- 0x7FFFFFFF)::64 Word.word)) "
using scast_down_range[OF rightSize]
by auto
then have b:"sint ((scast (((scast w\<^sub>1)::64 Word.word) + 0xFFFFFFFF80000001))::word) = sint (((scast w\<^sub>1)::64 Word.word) + 0xFFFFFFFF80000001)"
using g by auto
show "r'\<^sub>1 - 2147483647 = (real_of_int (sint ((scast (((scast w\<^sub>1)::64 Word.word) + 0xFFFFFFFF80000001))::word)))"
using a b c d e f
proof -
have " (real_of_int (sint ((scast w\<^sub>1)::64 Word.word ) - 2147483647)) = r'\<^sub>1 - (real_of_int 2147483647)"
by (simp add: e leq2)
then show ?thesis
by (metis b c d diff_minus_eq_add minus_minus of_int_numeral)
qed
qed
subgoal
proof -
assume "\<not> sint (((scast w\<^sub>1)::64 Word.word) + 0xFFFFFFFF80000001) \<le> - 2147483647"
then have sintw2_bound:"sint (((scast w\<^sub>1)::64 Word.word) + (-0x7FFFFFFF)) > - 2147483647"
unfolding neg64 by auto
have "- 0x7FFFFFFF < sint w\<^sub>1 + (- 0x7FFFFFFF)"
using sintw2_bound case1a
using d scast_eq3 by linarith
then have w2bound:"0 < sint w\<^sub>1"
using less_add_same_cancel2 by blast
have rightSize:"sint (((scast w\<^sub>1)::64 Word.word) + - 0x7FFFFFFF) \<in> sints (len_of TYPE(32))"
unfolding case1a e c
apply ( auto simp add: Word.word_sint.Rep[of "(w\<^sub>1)::32 Word.word"] sints32 len32[of "TYPE(32)"])
defer
subgoal using Word.word_sint.Rep[of "(w\<^sub>1)::32 Word.word"] by ( auto simp add: sints32 len32[of "TYPE(32)"])
using w2bound by auto
have arith:"\<And>x::int. x \<le> 2 ^ 31 - 1 \<Longrightarrow> x + (- 2147483647) < 2147483647"
by auto
have downcast:"sint ((scast (((scast w\<^sub>1)::64 Word.word) + ((- 0x7FFFFFFF))))::word) = sint (((scast w\<^sub>1)::64 Word.word) + ((- 0x7FFFFFFF)::64 Word.word)) "
using scast_down_range[OF rightSize]
by auto
show "sint (scast (((scast w\<^sub>1)::64 Word.word) + 0xFFFFFFFF80000001)::word) < 2147483647"
using downcast d e c arith[of "sint w\<^sub>1", OF d2]
by auto
qed
subgoal proof -
assume notLeq:"\<not> sint (((scast w\<^sub>1)::64 Word.word) + 0xFFFFFFFF80000001) \<le> - 2147483647"
then have gr:"sint (((scast w\<^sub>1)::64 Word.word) + 0xFFFFFFFF80000001) > - 2147483647"
by auto
then have sintw2_bound:"sint (((scast w\<^sub>1)::64 Word.word) + (-0x7FFFFFFF)) > - 2147483647"
unfolding neg64 using notLeq by auto
have "- 0x7FFFFFFF < sint w\<^sub>1 + (- 0x7FFFFFFF)"
using sintw2_bound case1a
using d scast_eq3 by linarith
then have w2bound:"0 < sint w\<^sub>1"
using less_add_same_cancel2 by blast
have rightSize:"sint (((scast w\<^sub>1)::64 Word.word) + - 0x7FFFFFFF) \<in> sints (len_of TYPE(32))"
unfolding case1a e c
apply ( auto simp add: Word.word_sint.Rep[of "(w\<^sub>1)::32 Word.word"] sints32 len32[of "TYPE(32)"])
defer
subgoal using Word.word_sint.Rep[of "(w\<^sub>1)::32 Word.word"] by ( auto simp add: sints32 len32[of "TYPE(32)"])
using w2bound by auto
show "- 2147483647 < real_of_int (sint ((scast (((scast w\<^sub>1)::64 Word.word) + 0xFFFFFFFF80000001))::word))"
using scast_down_range[OF rightSize] gr of_int_less_iff of_int_minus of_int_numeral by auto
qed
done
show "(let sum = ?sum in if sum <=s scast NEG_INF then NEG_INF else scast sum) \<equiv>\<^sub>U r\<^sub>1 + r\<^sub>2"
by (auto simp add: Let_def case1 case2)
qed
apply simp
proof -
assume notinf1:"w\<^sub>1 \<noteq> POS_INF"
assume notinf2:"w\<^sub>2 \<noteq> POS_INF"
assume notneginf1:"w\<^sub>1 \<noteq> NEG_INF"
assume notneginf2:"w\<^sub>2 \<noteq> NEG_INF"
let ?sum = "((scast w\<^sub>1)::64 Word.word) + ((scast w\<^sub>2):: 64 Word.word)"
have inf_case:"scast POS_INF <=s ?sum \<Longrightarrow> POS_INF \<equiv>\<^sub>U r\<^sub>1 + r\<^sub>2"
using repU_def repePos_simps
by (meson dual_order.strict_trans not_less order_refl)
have scast_eq1:"sint((scast w\<^sub>1)::64 Word.word) = sint w\<^sub>1"
apply(rule Word.sint_up_scast)
unfolding Word.is_up by auto
have scast_eq2:"sint((scast w\<^sub>2)::64 Word.word) = sint w\<^sub>2"
apply(rule Word.sint_up_scast)
unfolding Word.is_up by auto
have sints64:"sints 64 = {i. - (2 ^ 63) \<le> i \<and> i < 2 ^ 63}"
using sints_def[of 64] range_sbintrunc[of 63] by auto
have sints32:"sints 32 = {i. - (2 ^ 31) \<le> i \<and> i < 2 ^ 31}"
using sints_def[of 32] range_sbintrunc[of 31] by auto
have truth:" - (2 ^ (size ((scast w\<^sub>1)::64 Word.word) - 1)) \<le> sint ((scast w\<^sub>1)::64 Word.word) + sint ((scast w\<^sub>2)::64 Word.word) \<and> sint ((scast w\<^sub>1)::64 Word.word) + sint ((scast w\<^sub>2)::64 Word.word) \<le> 2 ^ (size ((scast w\<^sub>1)::64 Word.word) - 1) - 1"
using Word.word_size[of "(scast w\<^sub>2)::64 Word.word"] Word.word_size[of "(scast w\<^sub>1)::64 Word.word"]
using scast_eq1 scast_eq2
Word.word_sint.Rep[of "(w\<^sub>1)::32 Word.word"]
Word.word_sint.Rep[of "(w\<^sub>2)::32 Word.word"]
Word.word_sint.Rep[of "(scast w\<^sub>1)::64 Word.word"]
Word.word_sint.Rep[of "(scast w\<^sub>2)::64 Word.word"]
sints64 sints32 by auto
have sint_eq:"sint((scast w\<^sub>1 + scast w\<^sub>2)::64 Word.word) = sint w\<^sub>1 + sint w\<^sub>2"
using signed_arith_sint(1)[of "(scast w\<^sub>1)::64 Word.word" "(scast w\<^sub>2)::64 Word.word", OF truth]
using scast_eq1 scast_eq2
by auto
have bigOne:"scast w\<^sub>1 + scast w\<^sub>2 <=s ((- 0x7FFFFFFF)::64 Word.word) \<Longrightarrow> \<exists>r'\<ge>r\<^sub>1 + r\<^sub>2. r' \<le> (- 0x7FFFFFFF)"
proof -
assume "scast w\<^sub>1 + scast w\<^sub>2 <=s ((- 0x7FFFFFFF)::64 Word.word)"
then have sum_leq:"sint w\<^sub>1 + sint w\<^sub>2 \<le> - 0x7FFFFFFF"
and sum_leq':" (sint w\<^sub>1 + sint w\<^sub>2) \<le> (- 2147483647)"
using sint_eq unfolding Word.word_sle_def by auto
obtain r'\<^sub>1 r'\<^sub>2 ::real where
bound1:"r'\<^sub>1 \<ge> r\<^sub>1 \<and> (w\<^sub>1 \<equiv>\<^sub>E r'\<^sub>1)" and
bound2:"r'\<^sub>2 \<ge> r\<^sub>2 \<and> (w\<^sub>2 \<equiv>\<^sub>E r'\<^sub>2)"
using up1 up2 unfolding repU_def by auto
have somethingA:"r'\<^sub>1 \<le> sint w\<^sub>1" and somethingB:"r'\<^sub>2 \<le> sint w\<^sub>2"
using bound1 bound2 unfolding repe.simps POS_INF_def NEG_INF_def apply auto
using \<open>scast w\<^sub>1 + scast w\<^sub>2 <=s - 0x7FFFFFFF\<close> word_sle_def notinf1 notinf2 unfolding POS_INF_def
by auto
have something:"r'\<^sub>1 + r'\<^sub>2 \<le> sint w\<^sub>1 + sint w\<^sub>2"
using somethingA somethingB add_mono by fastforce
show "\<exists>r'\<ge>r\<^sub>1 + r\<^sub>2. r' \<le> (- 0x7FFFFFFF)"
apply(rule exI[where x = "r'\<^sub>1 + r'\<^sub>2"])
using bound1 bound2 add_mono something sum_leq' order.trans
by auto
qed
have anImp:"\<And>r'. (r'\<ge>r\<^sub>1 + r\<^sub>2 \<and> r' \<le> (- 2147483647)) \<Longrightarrow>
(\<exists>r. - (2 ^ 31 - 1) = - (2 ^ 31 - 1) \<and> r' = r \<and> r \<le> (real_of_int (sint ((- (2 ^ 31 - 1))::32 Word.word))))"
by auto
have anEq:"((scast ((- (2 ^ 31 - 1))::32 Word.word))::64 Word.word) = (- 0x7FFFFFFF)"
by auto
have bigTwo:
"\<not>(((scast POS_INF)::64 Word.word) <=s ?sum) \<Longrightarrow>
\<not>(?sum <=s ((scast NEG_INF)::64 Word.word)) \<Longrightarrow>
\<exists>r'\<ge>r\<^sub>1 + r\<^sub>2. r' = (real_of_int (sint (scast (((scast w\<^sub>1)::64 Word.word) + ((scast w\<^sub>2)::64 Word.word))::word))) \<and> (r' < 0x7FFFFFFF \<and> (-0x7FFFFFFF) < r')"
proof -
assume "\<not>(((scast POS_INF)::64 Word.word) <=s ?sum)"
then have sum_leq:"sint w\<^sub>1 + sint w\<^sub>2 < 0x7FFFFFFF"
unfolding Word.word_sle_def POS_INF_def using sint_eq by auto
then have sum_leq':" (sint w\<^sub>1 + sint w\<^sub>2) < (2147483647)"
by auto
assume "\<not>(?sum <=s ((scast NEG_INF)::64 Word.word))"
then have sum_geq:"(- 0x7FFFFFFF) < sint w\<^sub>1 + sint w\<^sub>2"
unfolding Word.word_sle_def NEG_INF_def using sint_eq by auto
then have sum_geq':" (- 2147483647) < (sint w\<^sub>1 + sint w\<^sub>2)"
by auto
obtain r'\<^sub>1 r'\<^sub>2 ::real where
bound1:"r'\<^sub>1 \<ge> r\<^sub>1 \<and> (w\<^sub>1 \<equiv>\<^sub>E r'\<^sub>1)" and
bound2:"r'\<^sub>2 \<ge> r\<^sub>2 \<and> (w\<^sub>2 \<equiv>\<^sub>E r'\<^sub>2)"
using up1 up2 unfolding repU_def by auto
have somethingA:"r'\<^sub>1 \<le> sint w\<^sub>1" and somethingB:"r'\<^sub>2 \<le> sint w\<^sub>2"
using bound1 bound2 unfolding repe.simps POS_INF_def NEG_INF_def apply auto
using word_sle_def notinf1 notinf2 unfolding POS_INF_def
by auto
have something:"r'\<^sub>1 + r'\<^sub>2 \<le> sint w\<^sub>1 + sint w\<^sub>2"
using somethingA somethingB add_mono by fastforce
have "(w\<^sub>1 \<equiv>\<^sub>E r'\<^sub>1)" using bound1 by auto
then have
r1w1:"r'\<^sub>1 = (real_of_int (sint w\<^sub>1))"
and w1U:" (real_of_int (sint w\<^sub>1)) < (real_of_int (sint POS_INF))"
and w1L:" (real_of_int (sint NEG_INF)) < (real_of_int (sint w\<^sub>1))"
unfolding repe.simps
using notinf1 notinf2 notneginf1 notneginf2 by (auto simp add: POS_INF_def NEG_INF_def)
have "(w\<^sub>2 \<equiv>\<^sub>E r'\<^sub>2)" using bound2 by auto
then have
r2w1:"r'\<^sub>2 = (real_of_int (sint w\<^sub>2))"
and w2U:" (real_of_int (sint w\<^sub>2)) < (real_of_int (sint POS_INF))"
and w2L:" (real_of_int (sint NEG_INF)) < (real_of_int (sint w\<^sub>2))"
unfolding repe.simps
using notinf1 notinf2 notneginf1 notneginf2 by (auto simp add: POS_INF_def NEG_INF_def)
have "sint (((scast w\<^sub>1)::64 Word.word) + ((scast w\<^sub>2)::64 Word.word)) = sint ((scast (((scast w\<^sub>1)::64 Word.word) + ((scast w\<^sub>2)::64 Word.word)))::word)"
apply(rule scast_down_range)
unfolding sint_eq using sints32 sum_geq sum_leq by auto
then have cast_eq:"(sint ((scast (((scast w\<^sub>1)::64 Word.word) + ((scast w\<^sub>2)::64 Word.word)))::word)) = sint w\<^sub>1 + sint w\<^sub>2"
using scast_down_range
unfolding sint_eq using sints32 sum_geq sum_leq
using sint_eq by auto
from something and cast_eq
have r12_sint_scast:"r'\<^sub>1 + r'\<^sub>2 = (sint ((scast (((scast w\<^sub>1)::64 Word.word) + ((scast w\<^sub>2)::64 Word.word)))::word))"
using r1w1 w1U w1L r2w1 w2U w2L by (simp)
show ?thesis
using bound1 bound2 add_mono r12_sint_scast cast_eq sum_leq sum_leq' sum_geq'
\<open>r'\<^sub>1 + r'\<^sub>2 = (real_of_int (sint (scast (scast w\<^sub>1 + scast w\<^sub>2))))\<close>
by auto
qed
have neg_inf_case:"?sum <=s ((scast ((NEG_INF)::word))::64 Word.word) \<Longrightarrow> NEG_INF \<equiv>\<^sub>U r\<^sub>1 + r\<^sub>2"
proof (unfold repU_def NEG_INF_def repe.simps)
assume "scast w\<^sub>1 + scast w\<^sub>2 <=s ((scast ((- (2 ^ 31 - 1))::word))::64 Word.word)"
then have "scast w\<^sub>1 + scast w\<^sub>2 <=s ((- 0x7FFFFFFF)::64 Word.word)"
by (metis anEq)
then obtain r' where geq:"(r' \<ge> r\<^sub>1 + r\<^sub>2)" and leq:"(r' \<le> (- 0x7FFFFFFF))"
using bigOne by auto
show " \<exists>r'\<ge>r\<^sub>1 + r\<^sub>2.
(\<exists>r. - (2 ^ 31 - 1) = POS_INF \<and> r' = r \<and> real_of_int (sint POS_INF) \<le> r) \<or>
(\<exists>r. - (2 ^ 31 - 1) = - (2 ^ 31 - 1) \<and> r' = r \<and> r \<le> real_of_int (sint (- (2 ^ 31 - 1)::word))) \<or>
(\<exists>w. - (2 ^ 31 - 1) = w \<and>
r' = real_of_int (sint w) \<and>
real_of_int (sint w) < real_of_int (sint POS_INF) \<and> real_of_int (sint (- (2 ^ 31 - 1))) < real_of_int (sint w))"
using leq anImp geq
by auto
qed
have int_case:"\<not>(((scast POS_INF)::64 Word.word) <=s ?sum) \<Longrightarrow> \<not> (?sum <=s ((scast NEG_INF)::64 Word.word)) \<Longrightarrow> ((scast ?sum)::word) \<equiv>\<^sub>U r\<^sub>1 + r\<^sub>2"
proof -
assume bound1:"\<not> ((scast POS_INF)::64 Word.word) <=s scast w\<^sub>1 + scast w\<^sub>2"
assume bound2:"\<not> scast w\<^sub>1 + scast w\<^sub>2 <=s ((scast NEG_INF)::64 Word.word)"
obtain r'::real
where
rDef:"r' = (real_of_int (sint ((scast (((scast w\<^sub>1)::64 Word.word) + ((scast w\<^sub>2)::64 Word.word)))::word)))"
and r12:"r'\<ge>r\<^sub>1 + r\<^sub>2"
and boundU:"r' < 0x7FFFFFFF"
and boundL:" (-0x7FFFFFFF) < r'"
using bigTwo[OF bound1 bound2] by auto
obtain w::word
where wdef:"w = (scast (((scast w\<^sub>1)::64 Word.word) + ((scast w\<^sub>2)::64 Word.word))::word)"
by auto
then have wr:"r' = (real_of_int (sint w))"
using r12 bound1 bound2 rDef by blast
show ?thesis
unfolding repU_def NEG_INF_def repe.simps POS_INF_def
using r12 wdef rDef boundU boundL wr
by auto
qed
show "(let sum::64 Word.word = scast w\<^sub>1 + scast w\<^sub>2 in if scast POS_INF <=s sum then POS_INF else if sum <=s scast NEG_INF then NEG_INF else scast sum) \<equiv>\<^sub>U r\<^sub>1 + r\<^sub>2"
apply(cases "((scast POS_INF)::64 Word.word) <=s ((?sum)::64 Word.word)")
subgoal using inf_case Let_def int_case neg_inf_case by auto
apply(cases "?sum <=s scast NEG_INF")
subgoal
using inf_case Let_def int_case neg_inf_case
proof -
assume "\<not> (scast POS_INF::64 Word.word) <=s scast w\<^sub>1 + scast w\<^sub>2"
then have "\<not> (scast w\<^sub>1::64 Word.word) + scast w\<^sub>2 <=s scast NEG_INF \<and> \<not> (scast POS_INF::64 Word.word) <=s scast w\<^sub>1 + scast w\<^sub>2 \<and> \<not> (scast w\<^sub>1::64 Word.word) + scast w\<^sub>2 <=s scast NEG_INF \<or> ((let w = scast w\<^sub>1 + scast w\<^sub>2 in if scast POS_INF <=s (w::64 Word.word) then POS_INF else if w <=s scast NEG_INF then NEG_INF else scast w) \<equiv>\<^sub>U r\<^sub>1 + r\<^sub>2)"
using neg_inf_case by presburger
then show ?thesis
using int_case by force
qed
subgoal using inf_case Let_def int_case neg_inf_case
proof -
assume a1: "\<not> (scast POS_INF::64 Word.word) <=s scast w\<^sub>1 + scast w\<^sub>2"
assume "\<not> (scast w\<^sub>1::64 Word.word) + scast w\<^sub>2 <=s scast NEG_INF"
have "\<not> (scast w\<^sub>1::64 Word.word) + scast w\<^sub>2 <=s scast NEG_INF \<and> \<not> (scast POS_INF::64 Word.word) <=s scast w\<^sub>1 + scast w\<^sub>2 \<or> ((let w = scast w\<^sub>1 + scast w\<^sub>2 in if scast POS_INF <=s (w::64 Word.word) then POS_INF else if w <=s scast NEG_INF then NEG_INF else scast w) \<equiv>\<^sub>U r\<^sub>1 + r\<^sub>2)"
using a1 neg_inf_case by presburger
then show ?thesis
using int_case by force
qed
done
qed
fun pl :: "word \<Rightarrow> word \<Rightarrow> word"
where "pl w1 w2 =
(if w1 = NEG_INF then NEG_INF
else if w2 = NEG_INF then NEG_INF
else if w1 = POS_INF then
(if w2 = POS_INF then POS_INF
else
(let sum::64 Word.word = ((scast w2)::64 Word.word) + ((scast POS_INF)::64 Word.word) in
if ((scast POS_INF)::64 Word.word) <=s(sum::64 Word.word) then POS_INF
else scast sum))
else if w2 = POS_INF then
(let sum::64 Word.word = ((scast w1)::64 Word.word) + ((scast POS_INF)::64 Word.word) in
if ((scast POS_INF)::64 Word.word) <=s(sum::64 Word.word) then POS_INF
else scast sum)
else
(let sum::64 Word.word = ((scast w1)::64 Word.word) + ((scast w2)::64 Word.word) in
if ((scast POS_INF)::64 Word.word) <=s (sum::64 Word.word) then POS_INF
else if (sum::64 Word.word) <=s ((scast NEG_INF)::64 Word.word) then NEG_INF
else scast sum))
"
lemma pl_lemma:
assumes lo1:"w\<^sub>1 \<equiv>\<^sub>L (r\<^sub>1::real)"
assumes lo2:"w\<^sub>2 \<equiv>\<^sub>L (r\<^sub>2::real)"
shows "pl w\<^sub>1 w\<^sub>2 \<equiv>\<^sub>L (r\<^sub>1 + r\<^sub>2)"
apply(cases "w\<^sub>1 = NEG_INF")
subgoal
apply (auto simp add: POS_INF_def repL_def repe.simps NEG_INF_def)
using linear by auto
apply(cases "w\<^sub>2 = NEG_INF")
subgoal
apply (auto simp add: POS_INF_def repL_def repe.simps NEG_INF_def)
using linear by auto
apply(cases "w\<^sub>1 = POS_INF")
subgoal
apply(cases "w\<^sub>2 = POS_INF")
subgoal
using lo1 lo2
by (auto simp add: POS_INF_def NEG_INF_def repL_def repe.simps)
subgoal
apply(simp)
proof -
assume neq1:"w\<^sub>2 \<noteq> POS_INF"
assume eq2:"w\<^sub>1 = POS_INF"
assume neq3:"w\<^sub>2 \<noteq> NEG_INF"
let ?sum = "(scast w\<^sub>2 + scast POS_INF)::64 Word.word"
have scast_eq1:"sint((scast w\<^sub>1)::64 Word.word) = sint w\<^sub>1"
apply(rule Word.sint_up_scast)
unfolding Word.is_up by auto
have scast_eq3:"sint((scast w\<^sub>2)::64 Word.word) = sint w\<^sub>2"
apply(rule Word.sint_up_scast)
unfolding Word.is_up by auto
have scast_eq2:"sint((scast (0x80000001::word))::64 Word.word) = sint ((0x80000001::32 Word.word))"
by auto
have sints64:"sints 64 = {i. - (2 ^ 63) \<le> i \<and> i < 2 ^ 63}"
using sints_def[of 64] range_sbintrunc[of 63] by auto
have sints32:"sints 32 = {i. - (2 ^ 31) \<le> i \<and> i < 2 ^ 31}"
using sints_def[of 32] range_sbintrunc[of 31] by auto
have thing1:"0 \<le> 9223372034707292161 + ((-(2 ^ 31))::real)" by auto
have "sint (( w\<^sub>2)) \<ge> (-(2 ^ 31))"
using Word.word_sint.Rep[of "(w\<^sub>2)::32 Word.word"] sints32
Word.word_size[of "(scast w\<^sub>2)::64 Word.word"] scast_eq1 scast_eq2 scast_eq3 len32 mem_Collect_eq
by auto
then have thing4:"sint ((scast w\<^sub>2)::64 Word.word) \<ge> (-(2 ^ 31))"
using scast_down_range sint_ge sints_num
using scast_eq3 by linarith
have aLeq2:"(-(2 ^ 31)::int) \<ge> -9223372039002259455" by auto
then have thing2:" (0::int) \<le> 9223372039002259455 + sint ((scast w\<^sub>2)::64 Word.word)"
using thing4 aLeq2
by (metis ab_group_add_class.ab_left_minus add.commute add_mono neg_le_iff_le)
have aLeq:"2 ^ 31 \<le> (9223372039002259455::int)" by auto
have bLeq:"sint ((scast w\<^sub>2)::64 Word.word) \<le> 2 ^ 31"
apply ( auto simp add: Word.word_sint.Rep[of "(w\<^sub>2)::32 Word.word"] sints32
scast_eq3 len32)
using Word.word_sint.Rep[of "(w\<^sub>2)::32 Word.word"] len32[of "TYPE(32)"] sints32 by auto
have thing3:" sint ((scast w\<^sub>2)::64 Word.word) \<le> 9223372034707292160 "
using aLeq bLeq by auto
have truth:" - (2 ^ (size ((scast w\<^sub>2)::64 Word.word) - 1)) \<le> sint ((scast w\<^sub>2)::64 Word.word) + sint ((0x7FFFFFFF)::64 Word.word) \<and> sint ((scast w\<^sub>2)::64 Word.word) + sint ((0x7FFFFFFF)::64 Word.word) \<le> 2 ^ (size ((scast w\<^sub>2)::64 Word.word) - 1) - 1"
by(auto simp add:
Word.word_size[of "(scast w\<^sub>2)::64 Word.word"] Word.word_size[of "(scast (0x7FFFFFFF))::64 Word.word"]
scast_eq1 scast_eq2
Word.word_sint.Rep[of "(w\<^sub>2)::32 Word.word"]
Word.word_sint.Rep[of "-0x80000001::32 Word.word"]
Word.word_sint.Rep[of "(scast w\<^sub>2)::64 Word.word"]
Word.word_sint.Rep[of "0x7FFFFFFF::64 Word.word"]
sints64 sints32 thing2 thing1 thing3)
have case1a:" sint (((scast w\<^sub>2)::64 Word.word) + (0x7FFFFFFF::64 Word.word)) = sint ((scast w\<^sub>2)::64 Word.word) + sint (0x7FFFFFFF::64 Word.word)"
by(rule signed_arith_sint(1)[OF truth])
have case1b:"sint ((0xFFFFFFFF80000001)::64 Word.word) < 0"
by auto
have case1:" (((scast POS_INF)::64 Word.word) <=s ?sum) \<Longrightarrow> POS_INF \<equiv>\<^sub>L r\<^sub>1 + r\<^sub>2"
using lo1 lo2 apply (simp add: repL_def NEG_INF_def repe.simps POS_INF_def word_sle_def)
apply(rule exI[where x= "r\<^sub>1 + r\<^sub>2"])
apply(auto)
using case1a case1b
apply (auto simp add: NEG_INF_def POS_INF_def neq1 eq2 neq3 repINT repL_def repe.simps repeInt_simps lo2 word_sless_alt)
using repINT repL_def repe.simps repeInt_simps lo2 word_sless_alt
NEG_INF_def POS_INF_def neq1 eq2 neq3 repINT repL_def repe.simps repeInt_simps lo2 word_sless_alt
apply (auto simp add: NEG_INF_def POS_INF_def)
proof -
fix r'
assume a1:"0 \<le> sint (((scast w\<^sub>2)::64 Word.word))"
from a1 have h3:"2147483647 \<le> sint w\<^sub>2 + 0x7FFFFFFF " using scast_eq3
by auto
assume a2:"r' \<le> r\<^sub>1"
assume a3:" (real_of_int (sint w\<^sub>2)) \<le> r\<^sub>2 "
assume a4:" ( 2147483647) \<le> r'"
assume a5:"sint w\<^sub>2 < 2147483647"
assume a6:"- 2147483647 < real_of_int (sint w\<^sub>2)"
assume a7:"sint (scast w\<^sub>2 + 0x7FFFFFFF) = sint (scast w\<^sub>2) + 2147483647"
from a2 a4 have h1:"2147483647 \<le> r\<^sub>1" by auto
from a1 a3 h3 have h2:"0 \<le> r\<^sub>2"
using dual_order.trans of_int_le_0_iff le_add_same_cancel2 by fastforce
show " (2147483647) \<le> r\<^sub>1 + r\<^sub>2 "
using h1 h2 h3 add.right_neutral add_mono
by fastforce
qed
obtain r'\<^sub>1 and r'\<^sub>2 where
geq1:"r'\<^sub>1\<le>r\<^sub>1" and equiv1:"w\<^sub>1 \<equiv>\<^sub>E r'\<^sub>1"
and geq2:"r'\<^sub>2\<le>r\<^sub>2" and equiv2:"w\<^sub>2 \<equiv>\<^sub>E r'\<^sub>2"
using lo1 lo2 unfolding repL_def by auto
have leq1:"r'\<^sub>1 \<ge> (real_of_int (sint POS_INF))"
using equiv1 unfolding repe.simps
using neq1 eq2 neq3 apply auto
subgoal unfolding NEG_INF_def POS_INF_def by auto
done
have leq2:"r'\<^sub>2 = (real_of_int (sint w\<^sub>2))"
using equiv2 unfolding repe.simps
using neq1 eq2 neq3 by auto
have case2:"\<not>(scast POS_INF <=s ?sum) \<Longrightarrow> scast ?sum \<equiv>\<^sub>L r\<^sub>1 + r\<^sub>2"
apply (simp add: repL_def NEG_INF_def repe.simps POS_INF_def word_sle_def lo1 lo2)
apply(rule exI[where x= "r'\<^sub>2 + 0x7FFFFFFF"]) (*r\<^sub>1 + r\<^sub>2*)
apply(rule conjI)
subgoal
proof -
assume " \<not> 2147483647 \<le> sint (scast w\<^sub>2 + 0x7FFFFFFF)"
have bound1:"2147483647 \<le> r\<^sub>1"
using leq1 geq1 by (auto simp add: POS_INF_def)
have bound2:"r'\<^sub>2 \<le> r\<^sub>2 "
using leq2 geq2 by auto
show "r'\<^sub>2 + 2147483647 \<le> r\<^sub>1 + r\<^sub>2"
using bound1 bound2
by linarith
qed
apply(rule disjI2)
apply(rule disjI2)
apply(auto)
subgoal
proof -
assume a:"\<not> 2147483647 \<le> sint (((scast w\<^sub>2)::64 Word.word) + 0x7FFFFFFF)"
then have sintw2_bound:"2147483647 > sint (((scast w\<^sub>2)::64 Word.word) + (0x7FFFFFFF))"
by auto
have case1a:" sint (((scast w\<^sub>2)::64 Word.word) + (0x7FFFFFFF::64 Word.word)) = sint ((scast w\<^sub>2)::64 Word.word) + sint (0x7FFFFFFF::64 Word.word)"
by(rule signed_arith_sint(1)[OF truth])
have a1:"sint (((scast w\<^sub>2)::64 Word.word) + (0x7FFFFFFF)) = sint((scast w\<^sub>2)::64 Word.word) + sint((0x7FFFFFFF)::64 Word.word)" using case1a by auto
have b1:"sint((scast w\<^sub>2)::64 Word.word) = sint w\<^sub>2"
apply(rule Word.sint_up_scast)
unfolding Word.is_up by auto
have c1:"sint((0x7FFFFFFF)::64 Word.word) = 0x7FFFFFFF"
by auto
have "sint w\<^sub>2 + ( 0x7FFFFFFF) < 0x7FFFFFFF"
using sintw2_bound case1a
using c1 scast_eq3 by linarith
then have w2bound:"sint w\<^sub>2 < 0"
using add_less_same_cancel2 by blast
have rightSize:"sint (((scast w\<^sub>2)::64 Word.word) + 0x7FFFFFFF) \<in> sints (len_of TYPE(32))"
unfolding case1a b1 c1
apply ( auto simp add: Word.word_sint.Rep[of "(w\<^sub>2)::32 Word.word"] sints32 len32[of "TYPE(32)"])
using Word.word_sint.Rep[of "(w\<^sub>2)::32 Word.word"] sints32 len32[of "TYPE(32)"]
using w2bound by auto
have arith:"\<And>x::int. x \<le> 2 ^ 31 - 1 \<Longrightarrow> x + (- 2147483647) < 2147483647"
by auto
have downcast:"sint ((scast (((scast w\<^sub>2)::64 Word.word) + (( 0x7FFFFFFF))))::word) = sint (((scast w\<^sub>2)::64 Word.word) + (( 0x7FFFFFFF)::64 Word.word)) "
using scast_down_range[OF rightSize]
by auto
then have b:"sint ((scast (((scast w\<^sub>2)::64 Word.word) + 0x7FFFFFFF))::word) = sint (((scast w\<^sub>2)::64 Word.word) + 0x7FFFFFFF)"
by auto
have c:"sint (((scast w\<^sub>2)::64 Word.word) + 0x7FFFFFFF) = sint ((scast w\<^sub>2)::64 Word.word) + sint ((0x7FFFFFFF)::64 Word.word)"
using case1a by auto
have d:"sint ((0x7FFFFFFF)::64 Word.word) = (0x7FFFFFFF)" by auto
have e:"sint ((scast w\<^sub>2)::64 Word.word) = sint w\<^sub>2"
using scast_eq3 by blast
have f:"r'\<^sub>2 = (real_of_int (sint w\<^sub>2))"
by (simp add: leq2)
show "r'\<^sub>2 + 2147483647 = (real_of_int (sint ((scast (((scast w\<^sub>2)::64 Word.word) + 0x7FFFFFFF))::word)))"
using a b c d e f
proof -
have " (real_of_int (sint ((scast w\<^sub>2)::64 Word.word ) + 2147483647)) = r'\<^sub>2 + (real_of_int 2147483647)"
using e leq2 by auto
then show ?thesis
by (metis b c d of_int_numeral)
qed
qed
subgoal
proof -
have truth2a:" - (2 ^ (size ((scast w\<^sub>2)::64 Word.word) - 1)) \<le> sint ((scast w\<^sub>2)::64 Word.word) + sint ((0x7FFFFFFF)::64 Word.word) \<and> sint ((scast w\<^sub>2)::64 Word.word) + sint ((0x7FFFFFFF)::64 Word.word) \<le> 2 ^ (size ((scast w\<^sub>2)::64 Word.word) - 1) - 1"
apply(auto simp add:
Word.word_size[of "(scast w\<^sub>2)::64 Word.word"] Word.word_size[of "(scast (0x7FFFFFFF))::64 Word.word"]
scast_eq1 scast_eq2