-
Notifications
You must be signed in to change notification settings - Fork 0
/
ShortestPathCVerification.thy
1548 lines (1426 loc) · 67.3 KB
/
ShortestPathCVerification.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
(* uses Isabelle2017 and autocorres version 1.4 *)
theory ShortestPathCVerification
imports
"checker-verification/Library/Autocorres_Misc"
"checker-verification/Witness_Property/ShortestPath"
"HOL-Library.Option_ord"
begin
(* Parse the input file. *)
install_C_file "shortest_path_checker.c"
autocorres "shortest_path_checker.c"
context shortest_path_checker begin
(*Implementation Graph Types*)
type_synonym IVertex = "32 word"
type_synonym IEdge_Id = "32 word"
type_synonym IEdge = "IVertex \<times> IVertex"
type_synonym IPEdge = "IVertex \<Rightarrow> 32 word"
type_synonym IEInt = "IVertex \<Rightarrow> (32 word \<times> 32 word)"
type_synonym ICost = "IVertex \<Rightarrow> 32 word"
type_synonym IGraph = "32 word \<times> 32 word \<times> (IEdge_Id \<Rightarrow> IEdge)"
abbreviation ivertex_cnt ::
"IGraph \<Rightarrow> 32 word"
where
"ivertex_cnt G \<equiv> fst G"
abbreviation iedge_cnt ::
"IGraph \<Rightarrow> 32 word"
where
"iedge_cnt G \<equiv> fst (snd G)"
abbreviation iedges ::
"IGraph \<Rightarrow> IEdge_Id \<Rightarrow> IEdge"
where
"iedges G \<equiv> snd (snd G)"
abbreviation val ::
"IEInt \<Rightarrow> IVertex \<Rightarrow> 32 word"
where
"val f v \<equiv> fst (f v)"
fun bool ::
"32 word \<Rightarrow> bool"
where
"bool b = (if b=0 then False else True)"
abbreviation is_inf ::
"IEInt \<Rightarrow> IVertex \<Rightarrow> 32 word"
where
"is_inf f v \<equiv> (snd (f v))"
(* Make List - makes a list containing the result of a function *)
fun mk_list' ::
"nat \<Rightarrow> (32 word \<Rightarrow> 'b) \<Rightarrow> 'b list"
where
"mk_list' n f = map f (map of_nat [0..<n])"
fun mk_list'_temp ::
"nat \<Rightarrow> (32 word \<Rightarrow> 'b) \<Rightarrow> nat \<Rightarrow> 'b list"
where
"mk_list'_temp 0 _ _ = []" |
"mk_list'_temp (Suc x) f i = (f (of_nat i)) # mk_list'_temp x f (Suc i)"
(* Make graph lists *)
fun mk_iedge_list ::
"IGraph \<Rightarrow> IEdge list"
where
"mk_iedge_list G = mk_list' (unat (iedge_cnt G)) (iedges G)"
fun mk_inum_list ::
"IGraph \<Rightarrow> IEInt \<Rightarrow> (32 word \<times> 32 word) list"
where
"mk_inum_list G num = mk_list' (unat (ivertex_cnt G)) num"
fun mk_ipedge_list ::
"IGraph \<Rightarrow> IPEdge \<Rightarrow> 32 word list"
where
"mk_ipedge_list G pedge = mk_list' (unat (ivertex_cnt G)) pedge"
fun mk_idist_list ::
"IGraph \<Rightarrow> IEInt \<Rightarrow> (32 word \<times> 32 word) list"
where
"mk_idist_list G dis = mk_list' (unat (ivertex_cnt G)) dis"
fun mk_icost_list ::
"IGraph \<Rightarrow> ICost \<Rightarrow> 32 word list"
where
"mk_icost_list G cost = mk_list' (unat (iedge_cnt G)) cost"
(* Equate to Implementation *)
lemma sint_ucast:
"sint (ucast (x ::word32) :: sword32) = sint x"
by (clarsimp simp: sint_uint uint_up_ucast is_up)
lemma long_ucast:
"unat (ucast (x ::word32) :: word64) = unat x"
by (simp add: is_up uint_up_ucast unat_def)
fun to_edge ::
"IEdge \<Rightarrow> Edge_C"
where
"to_edge (u,v) = Edge_C u v"
lemma s_C_pte[simp]:
"first_C (to_edge e) = fst e"
by (cases e) auto
lemma t_C_pte[simp]:
"second_C (to_edge e) = snd e"
by (cases e) auto
fun cast_long ::
"32 word \<Rightarrow> 64 word"
where
"cast_long x = ucast x"
fun to_eint ::
"(32 word \<times> 32 word) \<Rightarrow> EInt_C"
where
"to_eint p = EInt_C (fst p) (snd p)"
lemma val_C_pte[simp]:
"val_C (to_eint p) = fst p"
by (case_tac "p") auto
lemma isInf_C_pte[simp]:
"isInf_C (to_eint p) = snd p"
by (cases p) auto
definition is_graph
where
"is_graph h iG p \<equiv>
is_valid_Graph_C h p \<and>
ivertex_cnt iG = num_vertices_C (heap_Graph_C h p) \<and>
iedge_cnt iG = num_edges_C (heap_Graph_C h p) \<and>
arrlist (heap_Edge_C h) (is_valid_Edge_C h)
(map to_edge (mk_iedge_list iG)) (arcs_C (heap_Graph_C h p))"
definition is_numm
where
"is_numm h iG iN p \<equiv>
arrlist (\<lambda>p. heap_EInt_C h p) (\<lambda>p. is_valid_EInt_C h p)
(map to_eint (mk_inum_list iG iN)) p"
definition is_pedge
where
"is_pedge h iG iP (p:: 32 signed word ptr) \<equiv> arrlist (\<lambda>p. heap_w32 h (ptr_coerce p))
(\<lambda>p. is_valid_w32 h (ptr_coerce p)) (mk_ipedge_list iG iP) p"
definition is_dist
where
"is_dist h iG iD p \<equiv>
arrlist (\<lambda>p. heap_EInt_C h p) (\<lambda>p. is_valid_EInt_C h p)
(map to_eint (mk_idist_list iG iD)) p"
definition is_cost
where
"is_cost h iG iC p \<equiv> arrlist (heap_w32 h) (is_valid_w32 h) (mk_icost_list iG iC) p"
(* Lemmas for unat and of_nat *)
lemma eq_of_nat_conv:
assumes "unat w1 = n"
shows "w2 = of_nat n \<longleftrightarrow> w2 = w1"
using assms by auto
(* More Lemmas for unat and of_nat *)
lemma less_unat_plus1:
assumes "a < unat (b + 1)"
shows "a < unat b \<or> a = unat b"
apply (subgoal_tac "b + 1 \<noteq> 0 ")
using assms unat_minus_one add_diff_cancel
by fastforce+
lemma unat_minus_plus1_less:
fixes a b
assumes "a < b"
shows "unat (b - (a + 1)) < unat (b - a)"
by (metis (no_types) ab_semigroup_add_class.add_ac(1) right_minus_eq measure_unat
add_diff_cancel2 assms is_num_normalize(1) zadd_diff_inverse linorder_neq_iff)
(* Abstract Graph *)
definition no_loops ::
"('a, 'b) pre_digraph \<Rightarrow> bool"
where
"no_loops G \<equiv> \<forall>e \<in> arcs G. tail G e \<noteq> head G e"
definition abs_IGraph ::
"IGraph \<Rightarrow> (32 word, 32 word) pre_digraph"
where
"abs_IGraph G \<equiv> \<lparr> verts = {0..<ivertex_cnt G}, arcs = {0..<iedge_cnt G},
tail = fst o iedges G, head = snd o iedges G \<rparr>"
lemma verts_absI[simp]: "verts (abs_IGraph G) = {0..<ivertex_cnt G}"
and edges_absI[simp]: "arcs (abs_IGraph G) = {0..<iedge_cnt G}"
and start_absI[simp]: "tail (abs_IGraph G) e = fst (iedges G e)"
and target_absI[simp]: "head (abs_IGraph G) e = snd (iedges G e)"
by (auto simp: abs_IGraph_def)
definition abs_ICost ::
"(IEdge_Id \<Rightarrow> 32 word) \<Rightarrow> IEdge_Id \<Rightarrow> real"
where
"abs_ICost c e \<equiv> real (unat (c e))"
definition abs_IDist ::
"(32 word \<Rightarrow> (32 word \<times> 32 word)) \<Rightarrow> 32 word \<Rightarrow> ereal"
where
"abs_IDist d v \<equiv> if snd (d v) \<noteq> 0 then PInfty else
real (unat (fst (d v)))"
definition abs_INum ::
"(32 word \<Rightarrow> (32 word \<times> 32 word)) \<Rightarrow> 32 word \<Rightarrow> enat"
where
"abs_INum n v \<equiv> if snd (n v) \<noteq> 0 then \<infinity> else unat (fst (n v))"
definition abs_IPedge ::
"(32 word \<Rightarrow> 32 word) \<Rightarrow> 32 word \<Rightarrow> 32 word option"
where
"abs_IPedge p v \<equiv> if msb (p v) then None else Some (p v)"
lemma None_abs_pedgeI[simp]:
"(abs_IPedge p v = None) = msb (p v)"
using abs_IPedge_def by auto
lemma Some_abs_pedgeI[simp]:
"(\<exists>e. abs_IPedge p v = Some e) = (~ (msb (p v)))"
using None_not_eq None_abs_pedgeI
by (metis abs_IPedge_def)
(*Helper Lemmas*)
lemma wellformed_iGraph:
assumes "wf_digraph (abs_IGraph G)"
shows "\<And>e. e < iedge_cnt G \<Longrightarrow>
fst (iedges G e) < ivertex_cnt G \<and>
snd (iedges G e) < ivertex_cnt G"
using assms unfolding wf_digraph_def by simp
lemma unat_image_upto:
fixes n :: "32 word"
shows "unat ` {0..<n} = {unat 0..<unat n}" (is "?A = ?B")
proof
show "?B \<subseteq> ?A"
proof
fix i assume a: "i \<in> ?B"
then obtain i':: "32 word" where ii: "i= unat i'"
by (metis atLeastLessThan_iff le_unat_uoi less_or_eq_imp_le)
then have "i' \<in> {0..<n}"
using a word_less_nat_alt by auto
thus "i \<in> ?A" using ii by fast
qed
next
show "?A \<subseteq> ?B"
proof
fix i assume a: "i \<in> ?A"
then obtain i':: "32 word" where ii: "i= unat i'" by blast
then have "i' \<in> {0..<n}" using a by force
thus "i \<in> ?B"
by (metis Un_iff atLeast0LessThan ii ivl_disj_un(8)
lessThan_iff unat_0 unat_mono word_zero_le)
qed
qed
lemma unat_simp:
"\<And>x y:: 32 word. unat (x + y) \<ge> unat x \<longleftrightarrow>
unat (x + y) = unat x + unat y"
using unat_plus_simple word_le_nat_alt by blast
lemma unat_simp_2:
"\<And>x y :: 32 word. unat (x + y) = unat x + unat y \<longrightarrow> unat x + unat y \<ge> unat x"
by simp
lemma unat_leq_plus:
fixes x y z :: "32 word"
assumes a1: "x \<le> y + z"
shows "unat x \<le> unat y + unat z"
by (simp add: assms word_unat_less_le)
lemma unat_leq_plus_64:
fixes x y z :: "64 word"
assumes a1: "x \<le> y + z"
shows "unat x \<le> unat y + unat z"
by (simp add: assms word_unat_less_le)
lemma real_unat_leq_plus:
fixes x y z :: "32 word"
assumes a1: "x \<le> y + z"
shows "real (unat x) \<le> real (unat y) + real (unat z)"
using assms unat_leq_plus by fastforce
lemma real_unat_leq_plus_64:
fixes x y z :: "64 word"
assumes a1: "x \<le> y + z"
shows "real (unat x) \<le> real (unat y) + real (unat z)"
using assms unat_leq_plus_64 by fastforce
lemma real_nat:
fixes x y z :: "nat"
assumes a1: "real x \<le> real y + real z"
shows "x \<le> y + z"
using assms by linarith
lemma unat_leq_trian_plus:
fixes x y z :: "32 word"
assumes a1: "unat x \<le> unat y + unat z"
assumes a2: "unat y + unat z \<ge> unat y"
assumes a3: "unat (y + z) \<ge> unat y"
shows "x \<le> y + z"
using a1 a3 unat_simp word_le_nat_alt by fastforce
lemma unat_leq_plus_unats:
fixes x y z :: "32 word"
assumes a1: "unat x \<le> unat (y + z)"
shows "x \<le> y + z"
proof -
have f1: "unat x \<le> unat y + unat z"
using a1 by (meson not_le unat_leq_plus word_less_nat_alt)
then show ?thesis
by (simp add: assms word_le_nat_alt)
qed
lemma unat_plus_leq_unats:
fixes y z :: "32 word"
assumes a1: "unat y + unat z \<le> unat (max_word :: 32 word)"
shows "unat y + unat z \<le> unat (y + z)"
using a1
by unat_arith
lemma trian_imp_valid:
fixes x y z :: "32 word"
assumes a1: "real (unat y) + real (unat z) \<le> real (unat (max_word :: 32 word)) \<and> real(unat x) \<le> real (unat y) + real (unat z)"
shows "unat y + unat z \<le> unat (max_word::32 word)"
using a1 by linarith
lemma c: "UCAST(32 \<rightarrow> 64) (x::word32) = cast_long x"
by simp
lemma cast_long_max: "unat (cast_long (x::32 word)) \<le> unat (max_word::word32)"
using word_le_nat_alt long_ucast by auto
lemma cast_long_max_extend: "unat (cast_long (x::32 word)) \<le> unat (max_word::word64)"
using word_le_nat_alt by blast
lemma trian_64_reverse:
fixes x y z :: "word32"
assumes a1: "UCAST(32 \<rightarrow> 64) x \<le> UCAST(32 \<rightarrow> 64) y + UCAST(32 \<rightarrow> 64) z"
shows "unat x \<le> unat y + unat z"
by (metis (no_types, hide_lams) assms is_up len_of_word_comparisons(2) unat_leq_plus_64
uint_up_ucast unat_def)
lemma unat_plus_less_two_power_length:
assumes len: "len_of TYPE('a::len) < len_of TYPE('b::len)"
shows "unat (C:: 'a word) + unat (D:: 'a word) < (2::nat) ^ LENGTH('b)"
proof -
have bounded: "uint C < 2 ^ LENGTH('a)" "uint D < (2 :: int) ^ LENGTH('a)"
by (insert uint_bounded)
have unat_bounded: "unat C < 2 ^ LENGTH('a)" "unat D < (2 :: nat) ^ LENGTH('a)"
by simp+
have suc_leq: "Suc (len_of (TYPE('a)::'a itself)) \<le> len_of (TYPE('b)::'b itself)"
using len Suc_leI by blast
then have two_power_suc_leq: "(2::nat) ^ (len_of (TYPE('a)::'a itself) + 1) \<le>
2 ^ len_of (TYPE('b)::'b itself)"
by (metis (no_types) One_nat_def add.right_neutral add_Suc_right
power_increasing_iff rel_simps(49) rel_simps(9))
have "(2::nat) ^ (LENGTH ('a) + 1) = (2 ^ LENGTH ('a)) + (2 ^ LENGTH ('a))"
by auto
then have "unat (C:: 'a word) + unat (D:: 'a word) < (2::nat) ^ (LENGTH ('a) + 1)"
using unat_bounded by linarith
thus ?thesis using two_power_suc_leq
by linarith
qed
lemma abstract_val_ucast_add_strict_upcast:
"\<lbrakk> len_of TYPE('a::len) < len_of TYPE('b::len);
abstract_val P C' unat C; abstract_val P D' unat D \<rbrakk>
\<Longrightarrow> abstract_val P (C' + D') unat
((ucast (C :: 'a word) :: 'b word) +
ucast (D :: 'a word) :: 'b word)"
apply (clarsimp simp: is_up unat_ucast_upcast ucast_def )
apply (clarsimp simp: word_of_int_def unat_word_ariths(1))
apply (frule unat_plus_less_two_power_length[where C=C and D=D])
by (metis Divides.mod_less add.right_neutral
unat_plus_less_two_power_length uint_inverse
uint_mod_same uint_nat unat_of_nat zero_less_numeral
zero_less_power)
lemmas word_add_strict_up_cast_no_overflow_32_64 =
abstract_val_ucast_add_strict_upcast
[unfolded abstract_val_def,
OF word_abs_base(18) impI, where P=True, simplified]
lemma word_add_cast_up_no_overflow:
"unat y + unat z = unat (UCAST(32 \<rightarrow> 64) y + UCAST(32 \<rightarrow> 64) z)"
using word_add_strict_up_cast_no_overflow_32_64 by blast
lemma add_ucast_no_overflow_64: (* add_ucast_no_overflow *)
fixes x y z :: "word32"
assumes a1: "unat x \<le> unat y + unat z"
shows "(UCAST(32 \<rightarrow> 64) x) \<le> (UCAST(32 \<rightarrow> 64) y + UCAST(32 \<rightarrow> 64) z)"
apply (insert a1)
apply (subgoal_tac "unat (UCAST(32 \<rightarrow> 64) x) \<le>
unat (UCAST(32 \<rightarrow> 64) y + UCAST(32 \<rightarrow> 64) z)")
using word_le_nat_alt apply blast
apply (subst word_add_cast_up_no_overflow[symmetric])
using long_ucast by auto
lemma add_ucast_no_overflow_unat:
fixes x y z :: "word32"
shows "(UCAST(32 \<rightarrow> 64) x = UCAST(32 \<rightarrow> 64) y + UCAST(32 \<rightarrow> 64) z) =
(unat x = unat y + unat z)"
proof -
have "(UCAST(32 \<rightarrow> 64) x = UCAST(32 \<rightarrow> 64) y + UCAST(32 \<rightarrow> 64) z) \<longrightarrow>
unat x = unat y + unat z"
by (metis (mono_tags, hide_lams) is_up le_add_same_cancel1
len_of_word_comparisons(2) add_ucast_no_overflow_64 uint_up_ucast unat_def
unat_plus_simple zero_le)
moreover
have "unat x = unat y + unat z \<longrightarrow>
(UCAST(32 \<rightarrow> 64) x = UCAST(32 \<rightarrow> 64) y + UCAST(32 \<rightarrow> 64) z)"
by (metis (mono_tags, hide_lams) is_up len_of_word_comparisons(2)
uint_up_ucast unat_def word_arith_nat_add word_unat.Rep_inverse)
ultimately show ?thesis by blast
qed
lemma path_length:
assumes "vpath p (abs_IGraph iG)"
shows "vwalk_length p < unat (ivertex_cnt iG)"
proof -
have pne: "p \<noteq> []" and dp: "distinct p" using assms by fast+
have "unat (ivertex_cnt iG) = card (unat ` {0..<(fst iG)})"
using unat_image_upto by simp
then have "unat (ivertex_cnt iG) = card ((verts (abs_IGraph iG)))"
by (simp add: inj_on_def card_image)
hence "length p \<le> unat (ivertex_cnt iG)"
by (metis finite_code card_mono vwalk_def
distinct_card[OF dp] vpath_def assms)
hence "length p - 1 < unat (ivertex_cnt iG)"
by (metis pne Nat.diff_le_self le_neq_implies_less
less_imp_diff_less minus_eq one_neq_zero length_0_conv)
thus "vwalk_length p < unat (fst iG)"
using assms
unfolding vpath_def vwalk_def by simp
qed
lemma ptr_coerce_ptr_add_uint[simp]:
"ptr_coerce (p +\<^sub>p uint x) = p +\<^sub>p (uint x)"
by auto
lemma heap_ptr_coerce:
"\<lbrakk>arrlist (\<lambda>p. h (ptr_coerce p)) (\<lambda>p. v (ptr_coerce p))
(map (iL \<circ> of_nat) [0..<unat n]) l; i < n; 0 \<le> i\<rbrakk> \<Longrightarrow>
iL i = h (ptr_coerce (l +\<^sub>p int (unat i)))"
apply (subgoal_tac
"h (ptr_coerce (l +\<^sub>p int (unat i))) = map (iL \<circ> of_nat) [0..<unat n] ! unat i")
apply (subgoal_tac "map (iL \<circ> of_nat) [0..<unat n] ! unat i = iL i")
apply fastforce
apply (metis (hide_lams, mono_tags) unat_mono word_unat.Rep_inverse
minus_nat.diff_0 nth_map_upt o_apply plus_nat.add_0)
apply (drule arrlist_nth_value[where i="int (unat i)"], (simp add:unat_mono)+)
done
lemma arrlist_heap:
"\<lbrakk>arrlist h v (map (iL \<circ> of_nat) [0..<unat n]) l;
i < n\<rbrakk> \<Longrightarrow>
iL i = h (l +\<^sub>p int (unat i))"
apply (subgoal_tac
"h (l +\<^sub>p int (unat i)) = map (iL \<circ> of_nat) [0..<unat n] ! unat i")
apply (subgoal_tac "map (iL \<circ> of_nat) [0..<unat n] ! unat i = iL i")
apply fastforce
apply (metis (hide_lams, mono_tags) unat_mono word_unat.Rep_inverse
minus_nat.diff_0 nth_map_upt o_apply plus_nat.add_0)
apply (simp add: arrlist_nth_value unat_mono)
done
lemma two_comp_arrlist_heap:
"\<lbrakk> arrlist h v (map (f \<circ> (iL \<circ> of_nat)) [0..<unat n]) l;
i < n\<rbrakk> \<Longrightarrow> f (iL i) = h (l +\<^sub>p (int (unat i)))"
using arrlist_heap
by (metis (no_types, hide_lams) comp_apply comp_assoc)
lemma two_comp_to_eint_arrlist_heap:
"\<lbrakk> arrlist h v (map (to_eint \<circ> (iL \<circ> of_nat)) [0..<unat n]) l;
i < n\<rbrakk> \<Longrightarrow> to_eint (iL i) = h (l +\<^sub>p (int (unat i)))"
using arrlist_heap
by (metis (no_types, hide_lams) comp_apply comp_assoc)
lemma two_comp_to_edge_arrlist_heap:
"\<lbrakk> arrlist h v (map (to_edge \<circ> (iL \<circ> of_nat)) [0..<unat n]) l;
i < n\<rbrakk> \<Longrightarrow> to_edge (iL i) = h (l +\<^sub>p (int (unat i)))"
using arrlist_heap
by (metis (no_types, hide_lams) comp_apply comp_assoc)
lemma head_heap:
"\<lbrakk>arrlist h v (map (to_edge \<circ> (iedges iG \<circ> of_nat)) [0..<unat m]) ep; e < m\<rbrakk> \<Longrightarrow>
snd ((iedges iG) e) = second_C (h (ep +\<^sub>p (uint e)))"
using two_comp_arrlist_heap to_edge.simps t_C_pte by (metis uint_nat)
lemma tail_heap:
"\<lbrakk>arrlist h v (map (to_edge \<circ> (iedges iG \<circ> of_nat)) [0..<unat m]) ep; e < m\<rbrakk> \<Longrightarrow>
fst ((iedges iG) e) = first_C (h (ep +\<^sub>p (uint e)))"
using two_comp_arrlist_heap to_edge.simps s_C_pte uint_nat by metis
lemma val_heap:
"\<lbrakk>arrlist h v (map (to_eint \<circ> (f \<circ> of_nat)) [0..<unat m]) ep; e < m\<rbrakk> \<Longrightarrow>
val f e = val_C (h (ep +\<^sub>p (uint e)))"
using two_comp_arrlist_heap to_eint.simps val_C_pte by (metis uint_nat)
lemma is_inf_heap:
"\<lbrakk>arrlist h v (map (to_eint \<circ> (f \<circ> of_nat)) [0..<unat m]) ep; e < m\<rbrakk> \<Longrightarrow>
is_inf f e = isInf_C (h (ep +\<^sub>p (uint e)))"
using two_comp_arrlist_heap to_eint.simps isInf_C_pte by (metis uint_nat)
definition is_wellformed_inv :: "IGraph \<Rightarrow> 32 word \<Rightarrow> bool" where
"is_wellformed_inv G i \<equiv> \<forall>k < i. ivertex_cnt G > fst (iedges G k)
\<and> ivertex_cnt G > snd (iedges G k)"
lemma is_wellformed_spc':
"\<lbrace> P and
(\<lambda>s. is_graph s iG g) \<rbrace>
is_wellformed' g
\<lbrace> (\<lambda>_ s. P s) And
(\<lambda>rr s. rr \<noteq> 0 \<longleftrightarrow> is_wellformed_inv iG (iedge_cnt iG)) \<rbrace>!"
apply (clarsimp simp: is_wellformed'_def)
apply (subst whileLoopE_add_inv [where
M="\<lambda>(ee, s). unat (iedge_cnt iG - ee)" and
I="\<lambda>ee s. P s \<and> is_wellformed_inv iG ee \<and>
ee \<le> iedge_cnt iG \<and>
is_graph s iG g"])
apply (simp add: skipE_def)
apply wp
unfolding is_graph_def is_wellformed_inv_def
apply (subst if_bool_eq_conj)+
apply (simp split: if_split_asm, safe, simp_all add: arrlist_nth)
apply (rule_tac x = "ee" in exI)
apply (subgoal_tac "num_vertices_C (heap_Graph_C s g) \<le> fst (snd (snd iG) ee)", force)
apply (subgoal_tac "first_C (heap_Edge_C s (arcs_C (heap_Graph_C s g) +\<^sub>p uint ee)) = fst (snd (snd iG) ee)", simp)
apply (subst tail_heap[where iG=iG], simp, blast+)
apply(rule_tac x = "ee" in exI)
apply (subgoal_tac "num_vertices_C (heap_Graph_C s g) \<le> snd (snd (snd iG) ee)", force)
apply (subgoal_tac "second_C (heap_Edge_C s (arcs_C (heap_Graph_C s g) +\<^sub>p uint ee)) = snd (snd (snd iG) ee)", simp)
apply (subst head_heap[where iG=iG], simp, blast+)
apply (metis two_comp_arrlist_heap s_C_pte le_cases le_step uint_nat word_le_less_eq)
apply (metis head_heap le_step not_less)
apply (metis le_step word_not_le)
apply (metis (mono_tags, hide_lams) diff_diff_add diff_self_eq_0 eq_iff_diff_eq_0 measure_unat not_less0 word_less_nat_alt zero_less_diff)
apply (rule arrlist_nth, (simp add: uint_nat unat_mono)+)
apply wp
apply fast
done
definition trian_inv :: "IGraph \<Rightarrow> IEInt \<Rightarrow> ICost \<Rightarrow> 32 word \<Rightarrow> bool" where
"trian_inv G d c m \<equiv>
\<forall>i < m. is_inf d (fst (iedges G i)) = 0 \<longrightarrow>
(is_inf d (snd (iedges G i)) = 0 \<and>
cast_long (val d (snd (iedges G i))) \<le> cast_long (val d (fst (iedges G i))) + cast_long (c i))"
lemma trian_inv_step:
assumes i_less_max: "i < (max_word::32 word)"
shows "trian_inv G d c (i + 1) \<longleftrightarrow> trian_inv G d c i \<and>
(is_inf d (fst (iedges G i)) = 0 \<longrightarrow> is_inf d (snd (iedges G i)) = 0 \<and>
cast_long (val d (snd (iedges G i))) \<le> cast_long (val d (fst (iedges G i))) + cast_long (c i))"
unfolding trian_inv_def
by (metis (no_types) i_less_max less_irrefl less_x_plus_1)
lemma trian_inv_le:
assumes leq: "j \<le> i"
assumes trian_i: "trian_inv G d c i"
shows "trian_inv G d c j"
using assms
by (induct j) (auto simp add: trian_inv_def)
lemma cost_abs_C_equiv:
fixes ee :: "32 word" and s :: lifted_globals
assumes a1: "arrlist (heap_w32 s) (is_valid_w32 s) (map (iC \<circ> of_nat) [0..<unat (num_edges_C (heap_Graph_C s g))]) c"
assumes a2: "fst (snd iG) = num_edges_C (heap_Graph_C s g)"
assumes a3: "ee < num_edges_C (heap_Graph_C s g)"
shows "iC ee = heap_w32 s (c +\<^sub>p int (unat (ee)))"
proof -
show ?thesis
using a1 a3 arrlist_heap by blast
qed
lemma enat_abs_C_equiv:
fixes ee :: "32 word" and s :: lifted_globals
assumes a1: "ee < num_edges_C (heap_Graph_C s g)"
assumes a2: "arrlist (heap_EInt_C s) (is_valid_EInt_C s) (map (to_eint \<circ> (iL \<circ> of_nat)) [0..<unat (num_vertices_C (heap_Graph_C s g))]) l"
assumes a3: "fst iG = num_vertices_C (heap_Graph_C s g)"
assumes a4: "fst (snd iG) = num_edges_C (heap_Graph_C s g)"
assumes a5: "arrlist (heap_Edge_C s) (is_valid_Edge_C s) (map (to_edge \<circ> (snd (snd iG) \<circ> of_nat)) [0..<unat (num_edges_C (heap_Graph_C s g))]) (arcs_C (heap_Graph_C s g))"
assumes a6: "\<forall>ee < num_edges_C (heap_Graph_C s g). fst (snd (snd iG) ee) < num_vertices_C (heap_Graph_C s g)"
shows "fst (iL (fst (snd (snd iG) ee))) = val_C (heap_EInt_C s (l +\<^sub>p int (unat (first_C (heap_Edge_C s (arcs_C (heap_Graph_C s g) +\<^sub>p int (unat ee)))))))"
proof -
show ?thesis using a6 a5 a4 a3 a2 a1 s_C_pte two_comp_to_edge_arrlist_heap two_comp_to_eint_arrlist_heap val_C_pte by metis
qed
declare if_bool_eq_conj [[simp add]]
lemma trian_spc':
"\<lbrace> P and
(\<lambda>s. wf_digraph (abs_IGraph iG) \<and>
is_graph s iG g \<and>
is_dist s iG iD d \<and>
is_cost s iG iC c)\<rbrace>
trian' g d c
\<lbrace> (\<lambda>_ s. P s) And
(\<lambda>rr s. rr \<noteq> 0 \<longleftrightarrow> trian_inv iG iD iC (iedge_cnt iG)) \<rbrace>!"
apply (clarsimp simp: trian'_def)
apply (subst whileLoopE_add_inv [where
M="\<lambda>(ee, s). unat (iedge_cnt iG - ee)" and
I="\<lambda>ee s. P s \<and> trian_inv iG iD iC ee \<and>
ee \<le> iedge_cnt iG \<and>
wf_digraph (abs_IGraph iG) \<and>
is_graph s iG g \<and>
is_dist s iG iD d \<and>
is_cost s iG iC c"])
apply (simp add: skipE_def)
apply wp
apply (subst if_bool_eq_conj)+
apply (simp split: if_split_asm, simp_all add: arrlist_nth)
apply (rule conjI, rule impI, rule conjI, rule impI, rule conjI)
apply fast
apply (unfold trian_inv_def is_dist_def is_cost_def is_graph_def)[1]
apply clarsimp
apply (rule_tac x=ee in exI)
apply safe[1]
apply (metis is_inf_heap s_C_pte two_comp_to_edge_arrlist_heap wellformed_iGraph uint_nat)
apply (subgoal_tac "snd (iD (snd (snd (snd iG) ee))) = isInf_C (heap_EInt_C s (d +\<^sub>p uint (second_C (heap_Edge_C s (arcs_C (heap_Graph_C s g) +\<^sub>p uint ee)))))")
apply argo
apply (subst is_inf_heap, fastforce)
apply (subst head_heap, fastforce, fastforce)
apply (metis head_heap wellformed_iGraph)
apply (subst head_heap, fastforce, fastforce)
apply fast
apply (rule conjI, rule impI, rule conjI, rule impI, rule conjI)
apply fast
apply (unfold trian_inv_def is_dist_def is_cost_def is_graph_def)[1]
apply clarsimp
apply (rule_tac x=ee in exI)
apply safe[1]
apply (subst is_inf_heap, fastforce)
apply (metis wellformed_iGraph)
apply (subst tail_heap, fastforce, fastforce)
apply blast
apply (subgoal_tac "UCAST(32 \<rightarrow> 64) (fst (iD (snd (snd (snd iG) ee)))) =
UCAST(32 \<rightarrow> 64)
(val_C (heap_EInt_C s
(d +\<^sub>p uint (second_C (heap_Edge_C s (arcs_C (heap_Graph_C s g) +\<^sub>p
uint ee))))))")
apply (subgoal_tac "UCAST(32 \<rightarrow> 64) (fst (iD (fst (snd (snd iG) ee)))) +
UCAST(32 \<rightarrow> 64) (iC ee) =
UCAST(32 \<rightarrow> 64)
(val_C (heap_EInt_C s
(d +\<^sub>p uint (first_C (heap_Edge_C s (arcs_C (heap_Graph_C s g) +\<^sub>p
uint ee)))))) + UCAST(32 \<rightarrow> 64) (heap_w32 s (c +\<^sub>p uint ee))")
apply fastforce
apply (subst tail_heap, fastforce, fastforce)
apply (subst val_heap, fastforce)
apply (metis s_C_pte two_comp_to_edge_arrlist_heap wellformed_iGraph uint_nat)
apply (simp add: cost_abs_C_equiv uint_nat)
apply (subst head_heap, fastforce, fastforce)
apply (subst val_heap, fastforce)
apply (metis t_C_pte two_comp_to_edge_arrlist_heap wellformed_iGraph uint_nat)
apply blast
apply (rule conjI, rule impI, rule conjI)
apply fastforce
apply (rule conjI)
apply (subgoal_tac " ee + 1 \<le> fst (snd iG)")
apply (subgoal_tac "ee < (max_word::32 word)")
apply (drule trian_inv_step[where d=iD and G=iG and c=iC])
apply clarsimp
apply (unfold trian_inv_def is_graph_def is_cost_def is_dist_def)[1]
apply clarsimp
apply (subst tail_heap, fastforce, fastforce)
apply (subst head_heap, fastforce, fastforce)
apply (simp add: cost_abs_C_equiv)
apply (subst is_inf_heap, fastforce)
apply (metis t_C_pte two_comp_to_edge_arrlist_heap wellformed_iGraph uint_nat)
apply (subst val_heap, fastforce)
apply (metis wellformed_iGraph)
apply (subst head_heap, fastforce, fastforce)
apply (subst val_heap, fastforce)
apply (metis s_C_pte two_comp_to_edge_arrlist_heap uint_nat wellformed_iGraph)
apply (rule conjI, blast, simp add: uint_nat)
apply (simp add:less_le not_le, meson less_le max_word_max not_le)
apply (simp add: inc_le is_graph_def, blast intro: inc_le)
apply (metis (mono_tags) inc_le is_graph_def unat_minus_plus1_less)
apply (rule conjI)
apply (unfold wf_digraph_def trian_inv_def is_graph_def is_cost_def is_dist_def)[1]
apply (clarsimp simp: if_bool_eq_conj)+
apply (rule arrlist_nth, (simp add: uint_nat unat_mono)+)
apply (metis s_C_pte two_comp_to_edge_arrlist_heap word_less_nat_alt)
apply (rule conjI)
apply (unfold trian_inv_def is_graph_def is_cost_def is_dist_def)[1]
apply (clarsimp simp: if_bool_eq_conj)+
apply (rule arrlist_nth, (simp add: uint_nat unat_mono)+)
apply (rule conjI)
apply (unfold wf_digraph_def trian_inv_def is_graph_def is_cost_def is_dist_def)[1]
apply (clarsimp simp: if_bool_eq_conj)+
apply (rule arrlist_nth, (simp add: uint_nat unat_mono)+)
apply (metis t_C_pte two_comp_to_edge_arrlist_heap word_less_nat_alt)
apply (unfold trian_inv_def is_graph_def is_cost_def is_dist_def)[1]
apply (clarsimp simp: if_bool_eq_conj)+
apply (rule arrlist_nth, (simp add: uint_nat unat_mono)+)
apply (unfold wf_digraph_def trian_inv_def is_graph_def is_cost_def is_dist_def)[1]
apply (clarsimp simp: if_bool_eq_conj)+
apply (rule arrlist_nth, (simp add: uint_nat unat_mono)+)
apply (metis t_C_pte two_comp_to_edge_arrlist_heap word_less_nat_alt)
apply (rule conjI, rule impI, rule conjI)
apply fastforce
apply (rule conjI)
apply (subgoal_tac " ee + 1 \<le> fst (snd iG)")
apply (subgoal_tac "ee < (max_word::32 word)")
apply (drule trian_inv_step[where d=iD and G=iG and c=iC])
apply clarsimp
apply (unfold trian_inv_def is_graph_def is_cost_def is_dist_def)[1]
apply clarsimp
apply (subst tail_heap, fastforce, fastforce)
apply (subst head_heap, fastforce, fastforce)
apply (simp add: cost_abs_C_equiv)
apply (subst is_inf_heap, fastforce)
apply (metis t_C_pte two_comp_to_edge_arrlist_heap wellformed_iGraph uint_nat)
apply (subst val_heap, fastforce)
apply (metis wellformed_iGraph)
apply (subst head_heap, fastforce, fastforce)
apply (subst val_heap, fastforce)
apply (metis s_C_pte two_comp_to_edge_arrlist_heap uint_nat wellformed_iGraph)
apply (rule conjI, metis is_inf_heap tail_heap wellformed_iGraph)
apply (metis is_inf_heap tail_heap wellformed_iGraph)
apply (simp add:less_le not_le, meson less_le max_word_max not_le)
apply (simp add: inc_le is_graph_def, blast intro: inc_le)
apply (metis (mono_tags) inc_le is_graph_def unat_minus_plus1_less)
apply (rule conjI)
apply (unfold wf_digraph_def trian_inv_def is_graph_def is_cost_def is_dist_def)[1]
apply (clarsimp simp: if_bool_eq_conj)+
apply (rule arrlist_nth, (simp add: uint_nat unat_mono)+)
apply (metis s_C_pte two_comp_to_edge_arrlist_heap word_less_nat_alt)
apply (rule conjI)
apply (unfold trian_inv_def is_graph_def is_cost_def is_dist_def)[1]
apply (clarsimp simp: if_bool_eq_conj)+
apply (rule arrlist_nth, (simp add: uint_nat unat_mono)+)
apply (unfold trian_inv_def is_graph_def is_cost_def is_dist_def)[1]
apply (clarsimp simp: if_bool_eq_conj)+
apply (simp add: is_graph_def)
apply wp
apply (unfold trian_inv_def is_graph_def is_cost_def is_dist_def)[1]
apply force
done
definition just_inv ::
"IGraph \<Rightarrow> IEInt \<Rightarrow> ICost \<Rightarrow> IVertex \<Rightarrow> IEInt \<Rightarrow> IPEdge \<Rightarrow> 32 word \<Rightarrow> bool" where
"just_inv G d c s n p k \<equiv>
\<forall>v < k. v \<noteq> s \<and> is_inf n v = 0 \<longrightarrow>
sint (p v) \<ge> 0 \<and>
(\<exists> e. e = p v \<and> e < iedge_cnt G \<and>
v = snd (iedges G e) \<and>
(is_inf d v = 0 \<longleftrightarrow> is_inf d (fst (iedges G e)) = 0) \<and>
(is_inf d v = 0 \<longrightarrow>
cast_long (val d v) = cast_long (val d (fst (iedges G e))) + cast_long (c e)) \<and>
is_inf n (fst (iedges G e)) = 0 \<and>
cast_long (val n v) = cast_long (val n (fst (iedges G e))) + 1)"
lemma just_inv_step:
assumes v_less_max: "v < (max_word::32 word)"
shows "just_inv G d c s n p (v + 1) \<longleftrightarrow> just_inv G d c s n p v
\<and> (v \<noteq> s \<and> is_inf n v = 0 \<longrightarrow>
sint (p v) \<ge> 0 \<and>
(\<exists> e. e = p v \<and> e < iedge_cnt G \<and>
v = snd (iedges G e) \<and>
(is_inf d v = 0 \<longleftrightarrow> is_inf d (fst (iedges G e)) = 0) \<and>
(is_inf d v = 0 \<longrightarrow>
cast_long (val d v) = cast_long (val d (fst (iedges G e))) + cast_long (c e)) \<and>
is_inf n (fst (iedges G e)) = 0 \<and>
cast_long (val n v) = cast_long (val n (fst (iedges G e))) + 1))"
unfolding just_inv_def using v_less_max
by (force simp: less_x_plus_1)
lemma just_inv_le:
assumes leq: "j \<le> i"
assumes just_i: "just_inv G d c s n p i"
shows "just_inv G d c s n p j"
using assms
by (induct j) (auto simp add: just_inv_def)
lemma pedge_abs_C_equiv:
fixes vv :: "32 word" and s :: lifted_globals
assumes a1: "arrlist (\<lambda>p. heap_w32 s (ptr_coerce p)) (\<lambda>p. is_valid_w32 s (ptr_coerce p)) (map (iP \<circ> of_nat) [0..<unat (num_vertices_C (heap_Graph_C s g))]) p"
assumes a2: "fst iG = num_vertices_C (heap_Graph_C s g)"
assumes a3: "vv < num_vertices_C (heap_Graph_C s g)"
shows "iP vv = heap_w32 s (ptr_coerce (p +\<^sub>p int (unat vv)))"
proof -
have "\<forall>w. heap_w32 s (ptr_coerce (p +\<^sub>p int (unat w))) = iP w \<or> \<not> w < fst iG"
using a2 a1 heap_ptr_coerce unat_0 by fastforce
show ?thesis
using a1 a3 arrlist_heap by blast
qed
lemma word32_minus_comm: "(x:: 32 word) - y - z = x - z - y" by simp
lemma just_spc':
"\<lbrace> P and
(\<lambda>s. wf_digraph (abs_IGraph iG) \<and>
is_graph s iG g \<and>
is_dist s iG iD d \<and>
is_cost s iG iC c \<and>
is_numm s iG iN n \<and>
is_pedge s iG iP p)\<rbrace>
just' g d c sc n p
\<lbrace> (\<lambda>_ s. P s) And
(\<lambda>rr s. rr \<noteq> 0 \<longleftrightarrow> just_inv iG iD iC sc iN iP (ivertex_cnt iG)) \<rbrace>!"
apply (clarsimp simp: just'_def)
apply (subst whileLoopE_add_inv [where
M="\<lambda>(vv, s). unat (ivertex_cnt iG - vv)" and
I="\<lambda>vv s. P s \<and> just_inv iG iD iC sc iN iP vv \<and>
vv \<le> ivertex_cnt iG \<and>
wf_digraph (abs_IGraph iG) \<and>
is_graph s iG g \<and>
is_dist s iG iD d \<and>
is_cost s iG iC c \<and>
is_numm s iG iN n \<and>
is_pedge s iG iP p"])
apply (simp add: skipE_def)
apply wp
apply (subst if_bool_eq_conj)+
apply (simp split: if_split_asm, simp_all add: arrlist_nth)
apply (rule conjI, rule impI, rule conjI, rule impI, rule conjI, rule impI)
apply (unfold just_inv_def is_graph_def is_dist_def is_cost_def is_numm_def is_pedge_def wf_digraph_def)[1]
apply (clarsimp, rule_tac x=vv in exI, simp add: uint_nat)
apply (metis isInf_C_pte sint_ucast two_comp_to_eint_arrlist_heap not_le heap_ptr_coerce word_zero_le)
apply (rule impI, rule conjI)
apply (unfold just_inv_def is_graph_def is_dist_def is_cost_def is_numm_def is_pedge_def wf_digraph_def)[1]
apply (clarsimp, rule_tac x=vv in exI, simp add: uint_nat)
apply (metis isInf_C_pte two_comp_to_eint_arrlist_heap not_le heap_ptr_coerce word_zero_le)
apply (rule conjI, rule impI, rule conjI)
apply (unfold just_inv_def is_graph_def is_dist_def is_cost_def is_numm_def is_pedge_def wf_digraph_def)[1]
apply (clarsimp, rule_tac x=vv in exI, simp add: uint_nat)
apply (metis (no_types) isInf_C_pte two_comp_to_eint_arrlist_heap
heap_ptr_coerce word_zero_le two_comp_to_edge_arrlist_heap t_C_pte)
apply (rule conjI, rule impI, rule conjI, rule impI, rule conjI)
apply (unfold just_inv_def is_graph_def is_dist_def is_cost_def is_numm_def is_pedge_def wf_digraph_def)[1]
apply meson
apply (unfold just_inv_def is_graph_def is_dist_def is_cost_def is_numm_def is_pedge_def wf_digraph_def)[1]
apply (clarsimp, rule_tac x=vv in exI, simp add: uint_nat)
apply (subgoal_tac "heap_w32 s (ptr_coerce (p +\<^sub>p int (unat vv))) = iP vv")
apply (metis (no_types, hide_lams) is_inf_heap tail_heap uint_nat)
apply (metis heap_ptr_coerce word_zero_le)
apply (rule conjI, rule impI, rule conjI)
apply (unfold just_inv_def is_graph_def is_dist_def is_cost_def is_numm_def is_pedge_def wf_digraph_def)[1]
apply (clarsimp, rule_tac x=vv in exI, simp add: uint_nat)
apply (subgoal_tac "heap_w32 s (ptr_coerce (p +\<^sub>p int (unat vv))) = iP vv")
apply (subgoal_tac "snd (iN vv) = 0")
apply (subgoal_tac "\<And>w. w < fst iG \<Longrightarrow> heap_EInt_C s (d +\<^sub>p int (unat w)) = to_eint (iD w)")
apply (metis (no_types, hide_lams) cost_abs_C_equiv isInf_C_pte tail_heap val_C_pte uint_nat)
apply (metis two_comp_to_eint_arrlist_heap)
apply (metis isInf_C_pte two_comp_to_eint_arrlist_heap)
apply (metis (no_types) heap_ptr_coerce word_zero_le)
apply (rule conjI, rule impI, rule conjI)
apply (unfold just_inv_def is_graph_def is_dist_def is_cost_def is_numm_def is_pedge_def wf_digraph_def)[1]
apply (clarsimp, rule_tac x=vv in exI, simp add: uint_nat)
apply (rule conjI)
apply (metis isInf_C_pte two_comp_to_eint_arrlist_heap)
apply (rule impI)+
apply (simp add: pedge_abs_C_equiv)
apply (simp add: enat_abs_C_equiv)
apply (simp add: cost_abs_C_equiv)
apply (subgoal_tac "isInf_C
(heap_EInt_C s (n +\<^sub>p int (unat (fst (snd (snd iG)
(heap_w32 s (ptr_coerce (p +\<^sub>p int (unat vv))))))))) \<noteq> 0")
apply (metis isInf_C_pte two_comp_to_eint_arrlist_heap)
apply (metis tail_heap uint_nat)
apply (rule conjI, rule impI, rule conjI)
apply (unfold just_inv_def is_graph_def is_dist_def is_cost_def
is_numm_def is_pedge_def wf_digraph_def)[1]
apply (clarsimp, rule_tac x=vv in exI, simp add: uint_nat)
apply (rule conjI)
apply (subst is_inf_heap, blast, blast)
apply (simp add: pedge_abs_C_equiv)
apply (simp add: uint_nat)
apply (rule impI)+
apply (simp add: pedge_abs_C_equiv enat_abs_C_equiv cost_abs_C_equiv)
apply (subst val_heap, blast, blast, simp add: uint_nat)
apply (metis two_comp_to_eint_arrlist_heap val_C_pte)
apply (rule conjI, rule impI, rule conjI)
apply blast
apply clarsimp
apply (unfold is_graph_def)[1]
apply (rule conjI)
apply (subst just_inv_step)
apply (metis max_word_max not_le word_le_less_eq)
apply clarsimp
apply (unfold is_graph_def is_dist_def is_cost_def
is_numm_def is_pedge_def wf_digraph_def)[1]
apply clarsimp
apply (frule_tac e="iP vv" in head_heap;
simp add: pedge_abs_C_equiv sint_ucast
enat_abs_C_equiv uint_nat cost_abs_C_equiv)
apply (frule_tac e="iP vv" in tail_heap;
simp add: pedge_abs_C_equiv)
apply (rule conjI, simp)
apply (rule conjI)
apply (metis (no_types, hide_lams) not_le isInf_C_pte
two_comp_to_eint_arrlist_heap uint_nat)
apply (rule conjI, clarsimp)
apply (subst val_heap, fastforce, fast)
apply (subst val_heap, fastforce, metis not_le)
apply (simp add: uint_nat)
apply (rule conjI)
apply (metis (no_types, hide_lams) not_le isInf_C_pte
two_comp_to_eint_arrlist_heap uint_nat)
apply (subst val_heap, fastforce, fast)
apply (subst val_heap, fastforce, metis not_le)
apply (simp add: uint_nat)
apply (metis le_step not_le unat_minus_plus1_less)
apply (rule conjI)
apply (unfold is_graph_def just_inv_def is_dist_def is_cost_def is_numm_def is_pedge_def wf_digraph_def)[1]
apply (clarsimp simp: if_bool_eq_conj)+
apply (rule arrlist_nth, (simp add: uint_nat unat_mono)+)
apply (rule conjI)
apply (unfold is_graph_def just_inv_def is_dist_def is_cost_def is_numm_def is_pedge_def wf_digraph_def)[1]
apply (clarsimp simp: if_bool_eq_conj)+
apply (rule arrlist_nth, (simp add: uint_nat unat_mono)+)
apply (metis s_C_pte two_comp_to_edge_arrlist_heap word_less_nat_alt not_le)
apply (rule conjI)
apply (unfold is_graph_def just_inv_def is_dist_def is_cost_def is_numm_def is_pedge_def wf_digraph_def)[1]
apply (clarsimp simp: if_bool_eq_conj)+
apply (rule arrlist_nth, (simp add: uint_nat unat_mono)+)
apply (simp add: is_graph_def word_less_nat_alt not_le, blast+)
apply (rule conjI)
apply (unfold is_graph_def just_inv_def is_dist_def is_cost_def is_numm_def is_pedge_def wf_digraph_def)[1]
apply (clarsimp simp: if_bool_eq_conj)+
apply (rule arrlist_nth, (simp add: uint_nat unat_mono)+)
apply (metis s_C_pte two_comp_to_edge_arrlist_heap word_less_nat_alt not_le)
apply (rule conjI)
apply (unfold is_pedge_def is_graph_def)[1]
apply (clarsimp simp: if_bool_eq_conj)+
apply (rule arrlist_nth, (simp add: uint_nat unat_mono)+)
apply (simp add: is_graph_def word_less_nat_alt not_le, blast+)
apply (rule conjI)
apply (unfold is_dist_def is_pedge_def is_graph_def)[1]
apply (clarsimp simp: if_bool_eq_conj)+
apply (rule arrlist_nth, (simp add: uint_nat unat_mono)+)
apply (metis (no_types, hide_lams) not_le s_C_pte two_comp_to_edge_arrlist_heap wellformed_iGraph word_less_nat_alt)
apply (rule conjI)
apply (unfold is_cost_def is_pedge_def is_graph_def)[1]
apply (clarsimp simp: if_bool_eq_conj)+
apply (rule arrlist_nth, (simp add: uint_nat unat_mono)+)
apply (unfold is_graph_def just_inv_def is_dist_def is_cost_def is_numm_def is_pedge_def wf_digraph_def)[1]
apply (clarsimp simp: if_bool_eq_conj)+
apply (rule conjI; rule arrlist_nth, (simp add: uint_nat unat_mono)+)
apply clarsimp
apply (subgoal_tac " vv + 1 \<le> fst iG")
apply (subgoal_tac "vv < (max_word::32 word)")
apply (rule conjI, rule impI)
apply (rule conjI, rule impI, clarsimp)
apply (drule_tac j="vv + 1" in just_inv_le, assumption)
apply (clarsimp simp: is_graph_def)
apply (simp add: just_inv_step)
apply (subgoal_tac "snd (iN vv) = 0")
apply clarsimp
apply (subgoal_tac "snd (iN (fst (snd (snd iG) (iP vv)))) \<noteq> 0")
apply simp
apply (subst is_inf_heap, force simp: is_numm_def, metis wellformed_iGraph)
apply (subst tail_heap, fastforce, fastforce)
apply (unfold is_pedge_def enat_abs_C_equiv)[]
apply (subst pedge_abs_C_equiv[where iP=iP], fastforce+)
apply (simp add: uint_nat)
apply (subst is_inf_heap, force simp: is_numm_def, fast+)
prefer 3 apply (metis max_word_max not_le word_le_less_eq)
prefer 3 apply (clarsimp simp: is_graph_def, metis not_le plus_one_helper)
apply (rule conjI; clarsimp)
apply (rule conjI, clarsimp)
apply (drule_tac j="vv + 1" in just_inv_le, assumption)
apply (clarsimp simp: is_graph_def)
apply (simp add: just_inv_step)
apply (subgoal_tac "snd (iN vv) = 0")
apply (clarsimp simp:
add_ucast_no_overflow_unat[where z=1, simplified ucast_1 unat_1])
apply (unfold is_numm_def)[]
apply clarsimp
apply (simp add: val_heap)
apply (subst notE[where P = " fst x = val_C y " for x y], assumption)
apply (subst val_heap, fast, metis wellformed_iGraph)
apply (subst tail_heap, fastforce, fastforce)
apply (unfold is_pedge_def enat_abs_C_equiv)[]
apply (subst pedge_abs_C_equiv[where iP=iP], fastforce+)
apply (simp add: uint_nat)
apply simp
apply (subst is_inf_heap, force simp: is_numm_def, fast+)
apply (rule conjI, clarsimp)
apply (rule conjI)
apply (subst just_inv_step, assumption)
apply clarsimp