-
Notifications
You must be signed in to change notification settings - Fork 108
/
GraphRefine.thy
2164 lines (1929 loc) · 94.9 KB
/
GraphRefine.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
(*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*)
theory GraphRefine
imports
TailrecPre
GraphLangLemmas
Lib.Lib
"CParser.LemmaBucket_C"
ExtraSpecs
begin
type_synonym ('s, 'x, 'e) c_trace = "nat \<Rightarrow> (('s, 'x, 'e) com \<times> ('s, 'e) xstate) option"
definition
c_trace :: "('x \<Rightarrow> ('s, 'x, 'e) com option) \<Rightarrow> ('s, 'x, 'e) c_trace set"
where
"c_trace Gamma = nat_trace_rel (Not o final) {(cfg, cfg'). step Gamma cfg cfg'}"
definition
"exec_final_step cfg = (case cfg of (Throw, Normal xs) \<Rightarrow> Abrupt xs | _ \<Rightarrow> snd cfg)"
lemma exec_via_trace:
"Gamma \<turnstile> \<langle>com, Normal s\<rangle> \<Rightarrow> xs
= (\<exists>tr \<in> c_trace Gamma. tr 0 = Some (com, Normal s)
\<and> option_map exec_final_step (trace_end tr) = Some xs)"
proof -
have dom_If: "\<And>n f. dom (\<lambda>i. if i \<le> n then Some (f i) else None) = {..n}"
by (auto split: if_split_asm)
have end_If: "\<And>n f. trace_end (\<lambda>i. if i \<le> n then Some (f i) else None) = Some (f n)"
apply (simp add: trace_end_def dom_If)
apply (subst Max_eqI, simp+)
apply (rule_tac x="Suc n" in exI, simp)
done
show ?thesis unfolding c_trace_def
apply safe
apply (clarsimp simp: relpowp_fun_conv dest!: exec_impl_steps rtranclp_imp_relpowp)
apply (rule_tac x="\<lambda>i. if i \<le> n then Some (f i) else None" in bexI)
apply (simp add: end_If exec_final_step_def split: xstate.split_asm)
apply (simp add: nat_trace_rel_def)
apply (clarsimp simp: linorder_not_le less_Suc_eq)
apply (simp add: final_def split: xstate.split_asm)
apply (drule(1) trace_end_SomeD)
apply clarsimp
apply (subgoal_tac "rtranclp (step Gamma) (the (tr 0)) (the (tr n))")
apply (clarsimp simp: final_def)
apply (auto simp: exec_final_step_def dest: steps_Skip_impl_exec steps_Throw_impl_exec)[1]
apply (simp add: rtranclp_power relpowp_fun_conv)
apply (rule_tac x=n in exI)
apply (rule_tac x="the o tr" in exI)
apply (frule(1) trace_None_dom_eq)
apply (clarsimp simp: nat_trace_rel_def)
apply (subgoal_tac "i \<in> dom tr \<and> Suc i \<in> dom tr")
apply clarify
apply metis
apply (drule(1) eqset_imp_iff[THEN iffD1, rotated, OF domI])+
apply simp
done
qed
abbreviation
"extend_rel \<equiv> {((i :: nat, tr), (j, tr')).
j > i \<and> restrict_map tr {.. i} = restrict_map tr' {.. i}}"
definition
"suffix_tuple_closure_inter Ss
= (\<Inter>S \<in> Ss. {(y, tr). \<exists>k. (y, restrict_map tr {.. k}) \<in> S})"
lemma suffix_tuple_closure_prefixI:
"(y, restrict_map tr {.. (k :: nat)}) \<in> suffix_tuple_closure_inter Ss
\<Longrightarrow> (y, tr) \<in> suffix_tuple_closure_inter Ss"
by (auto simp add: suffix_tuple_closure_inter_def)
definition
trace_end_match :: "(state \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 's set
\<Rightarrow> stack option
\<Rightarrow> ((('s, 'x, 'e) com \<times> ('s, 'e) xstate) option)
\<Rightarrow> bool"
where
"trace_end_match out_eqs I e e' = ((\<exists>ft. e' = Some (com.Skip, Fault ft))
\<or> ((e = None) \<and> (e' = None))
\<or> (\<exists>sst' gst' gf'. e = Some [(Ret, gst', gf')]
\<and> e' = Some (com.Skip, Normal sst')
\<and> out_eqs gst' sst' \<and> sst' \<in> I))"
definition
simpl_to_graph :: "('x \<Rightarrow> ('s, 'x, 'e) com option)
\<Rightarrow> (string \<Rightarrow> graph_function option) \<Rightarrow> string
\<Rightarrow> next_node \<Rightarrow> ('s, 'x, 'e) com
\<Rightarrow> nat \<Rightarrow> (trace \<times> ('s, 'x, 'e) c_trace) set list
\<Rightarrow> 's set \<Rightarrow> 's set \<Rightarrow> (state \<Rightarrow> 's \<Rightarrow> bool)
\<Rightarrow> (state \<Rightarrow> 's \<Rightarrow> bool)
\<Rightarrow> bool"
where
"simpl_to_graph SGamma GGamma gf nn com n traces P I inp_eqs out_eqs
= (\<forall>tr gst sst n' gf' tr' n''. tr n' = Some [(nn, gst, gf')] \<and> sst \<in> P \<and> sst \<in> I
\<and> inp_eqs gst sst \<and> n' \<ge> n \<and> n'' \<ge> n
\<and> tr \<in> exec_trace GGamma gf
\<and> (tr, restrict_map tr' {.. n''}) \<in> suffix_tuple_closure_inter (set traces)
\<and> tr' \<in> nat_trace_rel (\<lambda>x. False) {(cfg, cfg'). step SGamma cfg cfg'}
\<and> tr' n'' = Some (com, Normal sst)
\<longrightarrow> (\<exists>tr''. tr'' \<in> c_trace SGamma \<and> restrict_map tr'' {.. n''} = restrict_map tr' {.. n''}
\<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'')))"
lemma simpl_to_graph_ge_subset:
"simpl_to_graph SGamma GGamma gf nn com n traces' P I inp_eqs out_eqs
\<Longrightarrow> n' \<ge> n \<and> set traces' \<subseteq> set traces
\<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com n' traces P I inp_eqs out_eqs"
apply (simp add: simpl_to_graph_def suffix_tuple_closure_inter_def Ball_def)
apply (erule mp[rotated], intro all_mono ex_mono imp_mono conj_mono imp_refl,
simp_all)
apply blast
done
lemmas simpl_to_graphI = simpl_to_graph_def[THEN iffD2, rule_format]
lemmas simpl_to_graphD = simpl_to_graph_def[THEN iffD1, rule_format]
lemma nat_trace_rel_split:
"tr n = Some v
\<Longrightarrow> tr' (Suc n) = Some v'
\<Longrightarrow> (v, v') \<in> R
\<Longrightarrow> tr \<in> nat_trace_rel cont' R
\<Longrightarrow> (\<lambda>i. tr' (Suc n + i)) \<in> nat_trace_rel cont R
\<Longrightarrow> (\<lambda>i. if i \<le> n then tr i else tr' i) \<in> nat_trace_rel cont R"
apply (frule(1) trace_Some_dom_superset)
apply (clarsimp simp: nat_trace_rel_def, safe)
apply (simp_all add: linorder_not_le less_Suc_eq_le subset_iff domIff)
apply (drule_tac x="na - Suc n" in spec | clarsimp)+
done
lemma nat_trace_rel_to_relpow:
"trace \<in> nat_trace_rel cont R
\<Longrightarrow> trace i = Some x
\<Longrightarrow> trace (i + j) = Some y
\<Longrightarrow> (x, y) \<in> R ^^ j"
apply (induct j arbitrary: y)
apply simp
apply atomize
apply (clarsimp simp: nat_trace_rel_def)
apply (drule_tac x="i + j" in spec, clarsimp)
apply auto
done
lemma exec_graph_trace_must_take_steps:
"trace \<in> exec_trace \<Gamma> fn
\<Longrightarrow> trace i = Some [(nn, st, fn)]
\<Longrightarrow> (exec_graph_step \<Gamma> ^^ j) `` {[(nn, st, fn)]} \<subseteq> {[(nn', st', fn)]}
\<Longrightarrow> \<forall>k < j. \<forall>st'. ([(nn, st, fn)], st') \<in> exec_graph_step \<Gamma> ^^ k
\<longrightarrow> continuing st'
\<Longrightarrow> trace (i + j) = Some [(nn', st', fn)]"
apply (case_tac "trace (i + j)")
apply (clarsimp simp add: exec_trace_def)
apply (drule(1) trace_None_dom_eq)
apply clarsimp
apply (drule sym[where s="dom trace"])
apply (frule_tac x=i in eqset_imp_iff)
apply (frule_tac x="n' - 1" in eqset_imp_iff)
apply (frule_tac x="n'" in eqset_imp_iff)
apply (simp(no_asm_use), clarsimp simp: domIff)
apply (frule_tac i="n' - 1" in trace_end_eq_Some, simp+)
apply (drule(1) trace_end_SomeD, clarsimp)
apply (drule_tac x="n' - 1 - i" in spec, simp)
apply (drule_tac i=i and j="n' - 1 - i" in nat_trace_rel_to_relpow, simp+)
apply (clarsimp simp add: exec_trace_def)
apply (drule_tac i=i and j=j in nat_trace_rel_to_relpow, simp+)
apply auto
done
lemma c_trace_may_extend:
"trace \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma> \<turnstile> x \<rightarrow> y}
\<Longrightarrow> trace i = Some (com, Normal st)
\<Longrightarrow> ((step \<Gamma>) ^^ j) (com, Normal st) (com', xst')
\<Longrightarrow> (y, restrict_map trace {..i}) \<in> suffix_tuple_closure_inter Ss
\<Longrightarrow> \<exists>trace'. trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma> \<turnstile> x \<rightarrow> y}
\<and> trace' (i + j) = Some (com', xst')
\<and> restrict_map trace' {.. i} = restrict_map trace {.. i}
\<and> (y, restrict_map trace' {.. i + j}) \<in> suffix_tuple_closure_inter Ss"
apply (cases "j = 0")
apply fastforce
apply (clarsimp simp: relpowp_fun_conv)
apply (rule_tac x="\<lambda>k. if k \<le> i then trace k else
if k \<le> i + j then Some (f (k - i))
else None"
in exI)
apply (intro conjI)
apply (erule nat_trace_rel_split, simp, simp_all)
apply (drule_tac x=0 in spec, simp)
apply (simp add: nat_trace_rel_def)
apply (simp add: restrict_map_def cong: if_cong)
apply (rule_tac k=i in suffix_tuple_closure_prefixI)
apply (simp add: restrict_map_def cong: if_cong)
done
lemma c_trace_may_extend_steps:
"trace \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma> \<turnstile> x \<rightarrow> y}
\<Longrightarrow> trace i = Some (com, Normal st)
\<Longrightarrow> \<Gamma> \<turnstile> (com, Normal st) \<rightarrow>\<^sup>* (com', xst')
\<Longrightarrow> (y, restrict_map trace {..i}) \<in> suffix_tuple_closure_inter Ss
\<Longrightarrow> \<exists>j trace'. trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma> \<turnstile> x \<rightarrow> y}
\<and> trace' (i + j) = Some (com', xst')
\<and> restrict_map trace' {.. i} = restrict_map trace {.. i}
\<and> (y, restrict_map trace' {.. i + j}) \<in> suffix_tuple_closure_inter Ss"
apply (clarsimp simp: rtranclp_power)
apply (blast intro: c_trace_may_extend)
done
lemma restrict_map_prefix_eq: "(restrict_map tr {..n} = restrict_map tr' {..n})
= (\<forall>i \<le> n. tr i = tr' i)"
by (auto simp add: fun_eq_iff restrict_map_def)
lemma restrict_map_eq_mono:
"i \<le> j \<Longrightarrow> restrict_map tr {..j} = restrict_map tr' {..j}
\<Longrightarrow> restrict_map tr {.. (i :: 'a :: linorder)} = restrict_map tr' {..i}"
unfolding restrict_map_prefix_eq
by clarsimp
lemma simpl_to_graph_step_general:
"(\<And>sst gst. sst \<in> P \<Longrightarrow> sst \<in> I \<Longrightarrow> inp_eqs gst sst
\<Longrightarrow> \<exists>sst' gst'. ((step SGamma) ^^ j) (com, Normal sst) (com', Normal sst')
\<and> (exec_graph_step GGamma ^^ i) `` {[(nn, gst, gf)]} \<subseteq> {[(nn', gst', gf)]}
\<and> (\<forall>k < i. \<forall>st'. ([(nn, gst, gf)], st') \<in> exec_graph_step GGamma ^^ k
\<longrightarrow> continuing st')
\<and> sst' \<in> P' \<and> sst' \<in> I \<and> inp_eqs' gst' sst')
\<Longrightarrow> simpl_to_graph SGamma GGamma gf nn' com' (n + min i j) traces P' I inp_eqs' out_eqs
\<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com n traces P I inp_eqs out_eqs"
apply (clarsimp intro!: simpl_to_graphI)
apply (erule_tac x=sst in meta_allE)
apply (erule_tac x=gst in meta_allE)
apply clarsimp
apply (frule(1) exec_trace_invariant)
apply (clarsimp simp: exec_graph_invariant_Cons)
apply (frule(2) exec_graph_trace_must_take_steps)
apply simp
apply (frule(3) c_trace_may_extend)
apply clarsimp
apply (drule_tac n''="n'' + j" in simpl_to_graphD,
(rule conjI | assumption | simp)+)
apply (metis restrict_map_eq_mono[OF le_add1[where m=j]])
done
lemma simpl_to_graph_step:
"(\<And>sst gst. sst \<in> P \<Longrightarrow> sst \<in> I \<Longrightarrow> inp_eqs gst sst
\<Longrightarrow> \<exists>sst' gst'. (step SGamma) (com, Normal sst) (com', Normal sst')
\<and> exec_graph_step GGamma `` {[(NextNode m, gst, gf)]} \<subseteq> {[(nn', gst', gf)]}
\<and> sst' \<in> P' \<and> sst' \<in> I \<and> inp_eqs' gst' sst')
\<Longrightarrow> simpl_to_graph SGamma GGamma gf nn' com' (Suc n) traces P' I inp_eqs' out_eqs
\<Longrightarrow> simpl_to_graph SGamma GGamma gf (NextNode m) com n traces P I inp_eqs out_eqs"
apply (rule simpl_to_graph_step_general[rotated, where i=1 and j=1])
apply simp+
apply (simp add: eq_OO)
done
lemma simpl_to_graph_step_R:
"(\<And>sst gst. sst \<in> P \<Longrightarrow> sst \<in> I \<Longrightarrow> inp_eqs gst sst
\<Longrightarrow> \<exists>sst'. (step SGamma) (com, Normal sst) (com', Normal sst')
\<and> sst' \<in> P' \<and> sst' \<in> I \<and> inp_eqs' gst sst')
\<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com' n traces P' I inp_eqs' out_eqs
\<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com n traces P I inp_eqs out_eqs"
apply (rule simpl_to_graph_step_general[rotated, where i=0 and j=1])
apply simp+
apply (simp add: eq_OO)
done
lemma simpl_to_graph_step_R_unchanged:
"(\<And>sst gst. sst \<in> P \<Longrightarrow> sst \<in> I \<Longrightarrow> inp_eqs gst sst
\<Longrightarrow> (step SGamma) (com, Normal sst) (com', Normal sst))
\<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com' n traces P I inp_eqs out_eqs
\<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com n traces P I inp_eqs out_eqs"
apply (erule simpl_to_graph_step_R[rotated])
apply blast
done
lemma simpl_to_graph_steps_Fault1:
"\<forall>s \<in> P \<inter> I. \<exists>com'. SGamma \<turnstile> (com, Normal s) \<rightarrow>\<^sup>* (com', Fault F)
\<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com n Q P I eqs out_eqs"
apply (clarsimp simp: simpl_to_graph_def)
apply (drule_tac x=sst in bspec, clarsimp+)
apply (cut_tac \<Gamma>=SGamma and c="com'" and f=F in steps_Fault)
apply (frule_tac c_trace_may_extend_steps, assumption)
apply (erule(1) rtranclp_trans)
apply assumption
apply (clarsimp simp: c_trace_def)
apply (rule exI, rule context_conjI)
apply (erule(1) nat_trace_rel_final, fastforce simp: final_def)
apply (simp add: trace_end_cut trace_end_match_def)
done
lemma extensible_traces_to_infinite_trace:
assumes step: "\<forall>x \<in> S. (trace x, trace (f x)) \<in> extend_rel
\<and> f x \<in> S \<and> m x < m (f x)"
and x: "x \<in> S"
shows "\<exists>tr. \<forall>i :: nat. \<exists>y \<in> S. \<exists>j. m y > i \<and> fst (trace y) > i
\<and> (trace y, (j, tr)) \<in> extend_rel"
proof -
let ?f = "\<lambda>i. (f ^^ i) x"
have f_induct: "\<And>i. m (?f i) \<ge> i \<and> fst (trace (?f i)) \<ge> i \<and> ?f i \<in> S"
apply (induct_tac i)
apply (simp add: x)
apply (auto dest: step[rule_format])
done
have f_eq: "\<forall>i j k. i \<le> fst (trace (?f j)) \<longrightarrow> j \<le> k
\<longrightarrow> fst (trace (?f j)) \<le> fst (trace (?f k)) \<and> snd (trace (?f k)) i = snd (trace (?f j)) i"
apply (intro allI, induct_tac k)
apply simp
apply clarsimp
apply (cut_tac i=n in f_induct[rule_format], clarsimp)
apply (frule_tac step[rule_format])
apply (clarsimp simp: fun_eq_iff restrict_map_def linorder_not_le split_def
split: if_split_asm)
apply (drule_tac x=i in spec)
apply (auto simp: le_Suc_eq)
done
have f_norm:
"\<forall>i j. j \<le> fst (trace (?f i)) \<longrightarrow> snd (trace (?f i)) j = snd (trace (?f j)) j"
apply clarsimp
apply (cut_tac i=j and j="min i j" and k="max i j" in f_eq[rule_format])
apply (simp add: min_def linorder_not_le f_induct)
apply simp
apply (simp add: min_def max_def split: if_split_asm)
done
show "?thesis"
apply (rule_tac x="\<lambda>i. snd (trace (?f i)) i" in exI)
apply (clarsimp simp: split_def)
apply (rule_tac x="?f (Suc i)" in bexI)
apply (cut_tac i="Suc i" in f_induct)
apply (clarsimp simp: fun_eq_iff restrict_map_def f_norm
simp del: funpow.simps)
apply (metis lessI)
apply (simp add: f_induct del: funpow.simps)
done
qed
lemma extensible_traces_to_infinite_trace_choice:
assumes step: "\<forall>x \<in> S. \<exists>y. (trace x, trace y) \<in> extend_rel
\<and> y \<in> S \<and> m x < m y"
and x: "x \<in> S"
shows "\<exists>tr. \<forall>i :: nat. \<exists>y \<in> S. \<exists>j. m y > i \<and> fst (trace y) > i
\<and> (trace y, (j, tr)) \<in> extend_rel"
proof -
let ?P = "\<lambda>i x. m x \<ge> i \<and> fst (trace x) \<ge> i \<and> x \<in> S"
let ?Q = "\<lambda>x y. m y > m x \<and> (trace x, trace y) \<in> extend_rel"
have induct:
"\<And>x n. ?P n x \<Longrightarrow> \<exists>y. ?P (Suc n) y \<and> ?Q x y"
apply clarsimp
apply (frule step[THEN bspec])
apply clarsimp
apply (rule_tac x=y in exI)
apply simp
done
obtain f where f: "\<forall>n. ?P n (f n) \<and> ?Q (f n) (f (Suc n))"
using x dependent_nat_choice[where P="?P" and Q="\<lambda>_. ?Q"]
by (simp only: induct, auto)
have f_induct: "\<And>i. m (f i) \<ge> i \<and> fst (trace (f i)) \<ge> i \<and> f i \<in> S"
apply (cut_tac n=i in f[rule_format], simp)
done
have f_eq: "\<forall>i j k. i \<le> fst (trace (f j)) \<longrightarrow> j \<le> k
\<longrightarrow> fst (trace (f j)) \<le> fst (trace (f k)) \<and> snd (trace (f k)) i = snd (trace (f j)) i"
apply (intro allI, induct_tac k)
apply simp
apply clarsimp
apply (cut_tac i=n in f_induct[rule_format], clarsimp)
apply (cut_tac n=n in f[rule_format], simp)
apply (clarsimp simp: fun_eq_iff restrict_map_def linorder_not_le split_def
split: if_split_asm)
apply (drule_tac x=i in spec)
apply (auto simp: le_Suc_eq)
done
have f_norm:
"\<forall>i j. j \<le> fst (trace (f i)) \<longrightarrow> snd (trace (f i)) j = snd (trace (f j)) j"
apply clarsimp
apply (cut_tac i=j and j="min i j" and k="max i j" in f_eq[rule_format])
apply (simp add: min_def linorder_not_le f_induct)
apply simp
apply (simp add: min_def max_def split: if_split_asm)
done
show "?thesis"
apply (rule_tac x="\<lambda>i. snd (trace (f i)) i" in exI)
apply (clarsimp simp: split_def)
apply (rule_tac x="f (Suc i)" in bexI)
apply (cut_tac i="Suc i" in f_induct)
apply (clarsimp simp: fun_eq_iff restrict_map_def f_norm
simp del: funpow.simps)
apply (metis lessI)
apply (simp add: f_induct del: funpow.simps)
done
qed
lemma trace_end_None_ge_seq:
"tr \<in> nat_trace_rel c R
\<Longrightarrow> \<forall>i. \<exists>j \<ge> i. tr j \<noteq> None
\<Longrightarrow> trace_end tr = None"
apply (clarsimp simp: trace_end_def)
apply (drule_tac x=n in spec)
apply (drule(1) trace_None_dom_subset)
apply auto
done
lemma restrict_map_eq_Some_le:
"(restrict_map tr {..n} = restrict_map tr' {..m})
\<Longrightarrow> tr' (m :: nat) = Some v
\<Longrightarrow> n \<ge> m \<and> (\<forall>k \<le> m. restrict_map tr {..k} = restrict_map tr' {..k})"
apply (frule_tac x=m in fun_cong, simp(no_asm_use) add: restrict_map_def)
apply (simp split: if_split_asm)
apply (auto simp: fun_eq_iff split: if_split_asm)
done
lemma trace_prefixes_to_trace:
assumes i: "\<forall>i. \<exists>j tr k. j \<ge> i \<and> tr j \<noteq> None
\<and> ((j, tr), (k, tr')) \<in> extend_rel \<and> tr \<in> nat_trace_rel c R"
shows "trace_end tr' = None \<and> tr' \<in> nat_trace_rel c' R"
proof (intro conjI)
have weak: "tr' \<in> nat_trace_rel (\<lambda>x. False) R"
apply (clarsimp simp: nat_trace_rel_def)
apply (cut_tac i="Suc n" in i[rule_format])
apply (clarsimp simp: nat_trace_rel_def)
apply (drule_tac x=n in spec, clarsimp)
apply (clarsimp simp: restrict_map_prefix_eq)
done
have inf: "\<forall>i. tr' i \<noteq> None"
apply (intro allI notI)
apply (cut_tac i=i in i[rule_format])
apply (clarsimp simp: restrict_map_prefix_eq)
apply (drule trace_None_dom_subset[OF _ weak])
apply auto
done
thus "trace_end tr' = None"
by (simp only: trace_end_def, simp)
show "tr' \<in> nat_trace_rel c' R" using weak
by (simp only: nat_trace_rel_def inf mem_Collect_eq, simp)
qed
lemma suffix_tuple_closure_inter_insert:
"(x, tr) \<in> suffix_tuple_closure_inter (insert S Ss)
= ((\<exists>k. (x, restrict_map tr {..k}) \<in> S) \<and> (x, tr) \<in> suffix_tuple_closure_inter Ss)"
by (simp add: suffix_tuple_closure_inter_def)
lemma simpl_to_graph_induct_proof:
assumes Suc: "\<And>S' n'. n' \<ge> n
\<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com (Suc n') (S' # S) P I inp_eqs out_eqs
\<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com n' (S' # S) P I inp_eqs out_eqs"
shows "simpl_to_graph SGamma GGamma gf nn com n (({tr} \<times> UNIV) # S) P I inp_eqs out_eqs"
proof -
obtain M where M_def:
"M = (\<lambda>n1 tr1. {(n', n'', tr'). tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}
\<and> (\<exists>sst gst gf'. tr' n'' = Some (com, Normal sst) \<and> tr n' = Some [(nn, gst, gf')]
\<and> inp_eqs gst sst \<and> sst \<in> P \<and> sst \<in> I
\<and> (tr, restrict_map tr' {..n''}) \<in> suffix_tuple_closure_inter (set S)
\<and> restrict_map tr' {..n1} = restrict_map tr1 {..n1}
\<and> n' \<ge> n \<and> n'' \<ge> n \<and> n'' \<ge> n1)})"
by auto
have induct_ge: "\<And>S' m n'. m \<ge> n \<longrightarrow> simpl_to_graph SGamma GGamma gf nn com m (S' # S) P I inp_eqs out_eqs
\<Longrightarrow> m \<ge> n'
\<Longrightarrow> n' \<ge> n \<longrightarrow> simpl_to_graph SGamma GGamma gf nn com n' (S' # S) P I inp_eqs out_eqs"
apply (erule(1) inc_induct)
apply clarsimp
apply (erule(1) Suc)
done
hence ge: "\<And>S' m n'. simpl_to_graph SGamma GGamma gf nn com m (S' # S) P I inp_eqs out_eqs
\<Longrightarrow> m \<ge> n' \<Longrightarrow> n' \<ge> n
\<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com n' (S' # S) P I inp_eqs out_eqs"
by auto
have terminating_case: "\<And>i j orig_tr' n1 tr1. (i, j, orig_tr') \<in> M n1 tr1
\<Longrightarrow> tr \<in> exec_trace GGamma gf
\<Longrightarrow> \<forall>v' \<in> M n1 tr1. fst v' > i \<longrightarrow> ((j, orig_tr'), snd v') \<notin> extend_rel
\<Longrightarrow> \<exists>tr'. tr' \<in> c_trace SGamma
\<and> restrict_map tr' {..j} = restrict_map orig_tr' {..j}
\<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr')"
apply (cut_tac n'="min i j" and m="Suc (max i j)"
and S'="{tr} \<times> {restrict_map orig_tr' {..j}}" in ge)
apply (clarsimp simp: M_def simpl_to_graph_def suffix_tuple_closure_inter_insert)
apply (erule_tac x=n' in allE, erule_tac x=n'' in allE, erule_tac x=tr' in allE)
apply (simp add: Suc_le_eq)
apply (drule(1) restrict_map_eq_Some_le)
apply simp
apply simp
apply (clarsimp simp: M_def)
apply (clarsimp simp: M_def)
apply (erule_tac n''=j and tr'=orig_tr' in simpl_to_graphD,
(rule conjI | assumption | simp)+)
apply (simp add: suffix_tuple_closure_inter_insert)
apply (metis min.idem)
apply simp
done
have infinite_case:
"\<And>v' n1 tr1. \<forall>v \<in> M n1 tr1. \<exists>v' \<in> M n1 tr1. fst v' > fst v \<and> (snd v, snd v') \<in> extend_rel
\<Longrightarrow> tr \<in> exec_trace GGamma gf
\<Longrightarrow> v' \<in> M n1 tr1
\<Longrightarrow> \<exists>tr'. trace_end tr = None
\<and> restrict_map tr' {.. n1} = restrict_map tr1 {.. n1}
\<and> trace_end tr' = None
\<and> tr' \<in> c_trace SGamma"
apply (drule extensible_traces_to_infinite_trace_choice[where
trace=snd and m=fst, rotated])
apply (rule ballI, drule(1) bspec)
apply fastforce
apply (erule exE, rename_tac tr')
apply (rule_tac x=tr' in exI)
apply (rule conjI)
apply (rule trace_end_None_ge_seq)
apply (auto simp add: exec_trace_def)[1]
apply clarsimp
apply (drule_tac x=i in spec)
apply (clarsimp simp: M_def)
apply (blast intro: less_imp_le)
apply (clarsimp simp: c_trace_def)
apply (rule conjI)
apply (drule_tac x=0 in spec)
apply (clarsimp simp: M_def)
apply (drule_tac i=n1 in restrict_map_eq_mono[rotated], assumption)+
apply simp
apply (rule trace_prefixes_to_trace)
apply clarsimp
apply (drule_tac x=i in spec)
apply (clarsimp simp: M_def)
apply (blast intro: less_imp_le)
done
show ?thesis
apply (clarsimp simp: simpl_to_graph_def suffix_tuple_closure_inter_insert)
apply (case_tac "(\<forall>v \<in> M n'' tr'. \<exists>v' \<in> M n'' tr'. fst v' > fst v \<and> (snd v, snd v') \<in> extend_rel)")
apply (drule(1) infinite_case)
apply (fastforce simp add: M_def)
apply (fastforce simp: trace_end_match_def)
apply clarsimp
apply (frule(1) terminating_case, simp)
apply (clarify, rename_tac soln_tr', rule_tac x=soln_tr' in exI)
apply (clarsimp simp: M_def)
apply (drule_tac i=n'' in restrict_map_eq_mono[rotated], assumption)+
apply simp
done
qed
lemma simpl_to_graph_induct:
assumes Suc: "\<And>S' k. simpl_to_graph SGamma GGamma gf nn com (Suc n + k) (S' # S) P I inp_eqs out_eqs
\<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com (n + k) (S' # S) P I inp_eqs out_eqs"
shows "simpl_to_graph SGamma GGamma gf nn com n S P I inp_eqs out_eqs"
apply (rule simpl_to_graphI)
apply (cut_tac tr=tr and n=n and S=S in simpl_to_graph_induct_proof)
apply (cut_tac S'=S' and k="n'a - n" in Suc)
apply simp+
apply (erule simpl_to_graphD)
apply (simp add: suffix_tuple_closure_inter_insert)
apply blast
done
definition
"eq_impl addr eqs eqs2 S = (\<forall>gst sst. eqs gst sst \<longrightarrow> sst \<in> S \<longrightarrow> eqs2 gst sst)"
lemma eq_implD:
"\<lbrakk> eq_impl addr eqs eqs2 S; eqs gst sst; sst \<in> S \<rbrakk>
\<Longrightarrow> eqs2 gst sst"
by (simp add: eq_impl_def)
lemma simpl_to_graph_cases:
"simpl_to_graph SGamma GGamma gf nn com n traces (P \<inter> S) I inp_eqs out_eqs
\<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com n traces (P \<inter> - S) I inp_eqs out_eqs
\<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com n traces P I inp_eqs out_eqs"
apply (rule simpl_to_graphI)
apply (case_tac "sst \<in> S")
apply (clarsimp simp only: simpl_to_graph_def[where P="P \<inter> S"] Compl_iff Int_iff)
apply (clarsimp simp only: simpl_to_graph_def[where P="P \<inter> - S"] Compl_iff Int_iff)
done
lemma exec_graph_step_image_node:
"GGamma f = Some gf \<Longrightarrow> function_graph gf n = Some node
\<Longrightarrow> exec_graph_step GGamma `` {[(NextNode n, gst, f)]}
= exec_node GGamma gst node [(NextNode n, gst, f)]"
by (cases gf, simp add: exec_graph_step_def)
definition
"add_cont com conts
= foldl (\<lambda>c d. case d of Inl d' \<Rightarrow> c ;; d' | Inr d' \<Rightarrow> com.Catch c d') com conts"
lemma add_cont_Cons:
"add_cont c (Inl d # cont) = add_cont (c ;; d) cont"
"add_cont c (Inr d # cont) = add_cont (com.Catch c d) cont"
by (simp_all add: add_cont_def)
lemma add_cont_Nil:
"add_cont c [] = c"
by (simp add: add_cont_def)
lemma add_cont_step:
"SGamma \<turnstile> (com, s) \<rightarrow> (com', s')
\<Longrightarrow> SGamma \<turnstile> (add_cont com con, s) \<rightarrow> (add_cont com' con, s')"
apply (induct con rule: rev_induct)
apply (simp add: add_cont_def)
apply (simp add: add_cont_def step.intros split: sum.split)
done
lemma simpl_to_graph_Cond:
"\<lbrakk> nn = NextNode m; GGamma gf = Some gfc; function_graph gfc m = Some (Cond l r cond);
eq_impl nn eqs (\<lambda>gst sst. l \<noteq> r \<longrightarrow> cond gst = (sst \<in> C)) (P \<inter> I);
eq_impl nn eqs eqs2 (P \<inter> I \<inter> C);
simpl_to_graph SGamma GGamma gf l (add_cont c con) (Suc n) Q (P \<inter> C) I eqs2 out_eqs;
eq_impl nn eqs eqs3 (P \<inter> I \<inter> (- C));
simpl_to_graph SGamma GGamma gf r (add_cont d con) (Suc n) Q (P \<inter> - C) I eqs3 out_eqs \<rbrakk>
\<Longrightarrow> simpl_to_graph SGamma GGamma gf nn (add_cont (com.Cond C c d) con) n Q P I eqs out_eqs"
apply clarsimp
apply (rule_tac S=C in simpl_to_graph_cases)
apply (erule_tac nn'=l in simpl_to_graph_step[rotated])
apply (simp add: exec_graph_step_image_node)
apply (fastforce dest: eq_implD intro: step.intros add_cont_step)[1]
apply (erule_tac nn'=r in simpl_to_graph_step[rotated])
apply (simp add: exec_graph_step_image_node)
apply (fastforce dest: eq_implD intro: step.intros add_cont_step)[1]
done
lemma simpl_to_graph_weaken[rotated]:
assumes eqs: "\<forall>gst sst. eqs gst sst \<and> sst \<in> P \<and> sst \<in> I
\<longrightarrow> eqs2 gst sst \<and> sst \<in> Q"
shows "simpl_to_graph SGamma GGamma gf nn com n tS Q I eqs2 out_eqs
\<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com n tS P I eqs out_eqs"
using eqs
apply (clarsimp simp add: simpl_to_graph_def)
apply blast
done
lemma simpl_to_graph_weaken_eq_impl:
"eq_impl nn eqs eqs2 (I \<inter> P)
\<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com n tS P I eqs2 out_eqs
\<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com n tS P I eqs out_eqs"
apply (erule simpl_to_graph_weaken)
apply (simp add: eq_impl_def)
done
lemma simpl_to_graph_While_lemma:
assumes ps: "GGamma f = Some gf" "nn = NextNode m" "function_graph gf m = Some (Cond l r cond)"
"eq_impl nn eqs (\<lambda>gst sst. cond gst = (sst \<in> C)) (I \<inter> P)"
assumes loop: "\<And>k S. \<lbrakk> simpl_to_graph SGamma GGamma f nn (add_cont (com.While C c) con) (Suc (n + k)) (S # tS) P I eqs out_eqs \<rbrakk>
\<Longrightarrow> simpl_to_graph SGamma GGamma f l (add_cont (c ;; com.While C c) con) (Suc (n + k)) (S # tS) (P \<inter> C) I eqs out_eqs"
assumes exitloop: "simpl_to_graph SGamma GGamma f r (add_cont com.Skip con) (Suc n) tS (P \<inter> (- C)) I eqs out_eqs"
shows "simpl_to_graph SGamma GGamma f nn (add_cont (com.While C c) con) n tS P I eqs out_eqs"
apply (rule simpl_to_graph_induct)
apply (simp add: ps)
apply (rule_tac S=C in simpl_to_graph_cases)
apply (rule simpl_to_graph_step[rotated])
apply (rule loop)
apply (simp add: ps)
apply (frule eq_implD[OF ps(4)], simp+)
apply (simp add: exec_graph_step_image_node ps)
apply (blast intro: step.intros add_cont_step)
apply (rule simpl_to_graph_step[rotated])
apply (rule simpl_to_graph_ge_subset)
apply (rule exitloop)
apply fastforce
apply (frule eq_implD[OF ps(4)], simp+)
apply (simp add: exec_graph_step_image_node ps)
apply (blast intro: step.intros add_cont_step)
done
lemma simpl_to_graph_While_inst:
assumes ps: "nn = NextNode m" "GGamma f = Some gf" "function_graph gf m = Some (Cond l r cond)"
"eq_impl nn eqs (\<lambda>gst sst. cond gst = (sst \<in> C)) (I \<inter> G)"
and ss_eq: "eq_impl nn eqs eqs2 (I \<inter> G \<inter> C)"
and ss: "\<And>k S. \<lbrakk> simpl_to_graph SGamma GGamma f nn (add_cont (com.While C c) con) (Suc (n + k)) (S # tS) G I eqs out_eqs \<rbrakk>
\<Longrightarrow> simpl_to_graph SGamma GGamma f l (add_cont (c ;; com.While C c) con) (Suc (n + k)) (S # tS) (G \<inter> C) I eqs2 out_eqs"
and ex_eq: "eq_impl nn eqs eqs3 (I \<inter> G \<inter> - C)"
and ex: "simpl_to_graph SGamma GGamma f r (add_cont com.Skip con) (Suc n) tS (G \<inter> (- C)) I eqs3 out_eqs"
and in_eq: "eq_impl nn eqs (\<lambda>gst sst. sst \<in> G) (I \<inter> G')"
shows "simpl_to_graph SGamma GGamma f nn (add_cont (com.While C c) con) n tS G' I eqs out_eqs"
apply (rule simpl_to_graph_weaken)
apply (rule simpl_to_graph_While_lemma[where P=G], (rule ps)+)
apply (rule simpl_to_graph_weaken, erule ss)
apply (clarsimp simp: ss_eq[THEN eq_implD])
apply (rule simpl_to_graph_weaken, rule ex)
apply (clarsimp simp: ex_eq[THEN eq_implD])
apply (clarsimp simp: in_eq[THEN eq_implD])
done
lemma use_simpl_to_graph_While_assum:
"\<lbrakk> simpl_to_graph SGamma GGamma f nn com n tS P I eqs out_eqs;
n \<le> n' \<and> set tS \<subseteq> set tS';
eq_impl nn eqs (\<lambda>gst sst. sst \<in> P) (Q \<inter> I) \<rbrakk>
\<Longrightarrow> simpl_to_graph SGamma GGamma f nn com n' tS' Q I eqs out_eqs"
apply (erule simpl_to_graph_ge_subset[rotated])
apply (erule simpl_to_graph_weaken)
apply (auto simp add: eq_impl_def)
done
lemma simpl_to_graph_Skip_immediate:
"simpl_to_graph SGamma GGamma f nn (add_cont c con) n tS P I eqs out_eqs
\<Longrightarrow> simpl_to_graph SGamma GGamma f nn (add_cont com.Skip (Inl c # con)) n tS P I eqs out_eqs"
"simpl_to_graph SGamma GGamma f nn (add_cont com.Skip con) n tS P I eqs out_eqs
\<Longrightarrow> simpl_to_graph SGamma GGamma f nn (add_cont com.Skip (Inr c # con)) n tS P I eqs out_eqs"
apply (safe elim!: simpl_to_graph_step_R_unchanged[rotated])
apply (auto simp: add_cont_Cons intro: add_cont_step step.intros)
done
lemmas simpl_to_graph_Skip
= simpl_to_graph_Skip_immediate[OF simpl_to_graph_weaken_eq_impl]
lemma simpl_to_graph_Throw_immediate:
"simpl_to_graph SGamma GGamma f nn (add_cont com.Throw con) n tS P I eqs out_eqs
\<Longrightarrow> simpl_to_graph SGamma GGamma f nn (add_cont com.Throw (Inl c # con)) n tS P I eqs out_eqs"
"simpl_to_graph SGamma GGamma f nn (add_cont c con) n tS P I eqs out_eqs
\<Longrightarrow> simpl_to_graph SGamma GGamma f nn (add_cont com.Throw (Inr c # con)) n tS P I eqs out_eqs"
apply (safe elim!: simpl_to_graph_step_R_unchanged[rotated])
apply (auto simp: add_cont_Cons intro: add_cont_step step.intros)
done
lemmas simpl_to_graph_Throw
= simpl_to_graph_Throw_immediate[OF simpl_to_graph_weaken_eq_impl]
lemma simpl_to_graph_Seq:
"simpl_to_graph SGamma GGamma f nn (add_cont (c ;; d) con) n tS P I eqs out_eqs
= simpl_to_graph SGamma GGamma f nn (add_cont c (Inl d # con)) n tS P I eqs out_eqs"
by (simp add: add_cont_Cons)
lemma simpl_to_graph_Catch:
"simpl_to_graph SGamma GGamma f nn (add_cont (com.Catch c d) con) n tS P I eqs out_eqs
= simpl_to_graph SGamma GGamma f nn (add_cont c (Inr d # con)) n tS P I eqs out_eqs"
by (simp add: add_cont_Cons)
lemma no_next_step: "eq_impl nn' eqs (\<lambda>gst' sst'.
((exec_graph_step GGamma) ^^ 0) `` {[(nn, gst', fn)]} \<subseteq> {[(nn, gst', fn)]}
\<and> (\<forall>k < (0 :: nat). \<forall>st'. ([(nn, gst', fn)], st') \<in> exec_graph_step GGamma ^^ k
\<longrightarrow> continuing st')) P"
by (simp add: eq_impl_def)
lemma basic_next_step: "GGamma fn = Some gf \<Longrightarrow> function_graph gf m = Some (Basic nn' upds)
\<Longrightarrow> eq_impl nn'' eqs (\<lambda>gst' sst'.
((exec_graph_step GGamma) ^^ 1) `` {[(NextNode m, gst', fn)]} \<subseteq> {[(nn', upd_vars upds gst', fn)]}
\<and> (\<forall>k < 1. \<forall>st'. ([(NextNode m, gst', fn)], st') \<in> exec_graph_step GGamma ^^ k
\<longrightarrow> continuing st')) P"
apply (clarsimp simp: eq_impl_def simp del: imp_disjL)
apply (clarsimp simp: exec_graph_step_def K_def split: graph_function.split_asm)
done
lemma simpl_to_graph_Basic_next_step:
assumes next_step: "eq_impl nn eqs (\<lambda>gst' sst'.
((exec_graph_step GGamma) ^^ steps) `` {[(nn, gst', fn)]} \<subseteq> {[(nn', f gst', fn)]}
\<and> (\<forall>k < steps. \<forall>st'. ([(nn, gst', fn)], st') \<in> exec_graph_step GGamma ^^ k
\<longrightarrow> continuing st')) (P \<inter> I)"
shows
"\<lbrakk> eq_impl nn eqs (\<lambda>gst sst. eqs2 (f gst) (f' sst) \<and> f' sst \<in> I \<and> f' sst \<in> Q) (P \<inter> I);
simpl_to_graph SGamma GGamma fn nn' (add_cont com.Skip con) (n + min steps 1) tS Q I eqs2 out_eqs \<rbrakk>
\<Longrightarrow> simpl_to_graph SGamma GGamma fn nn (add_cont (com.Basic f') con) n tS P I eqs out_eqs"
apply (rule simpl_to_graph_step_general[where j=1 and i=steps, rotated -1])
apply simp
apply (frule eq_implD[OF next_step], simp)
apply (simp add: eq_OO)
apply (rule exI, rule conjI, blast intro: add_cont_step step.intros)
apply (auto dest: eq_implD)
done
lemmas simpl_to_graph_Basic_triv'
= simpl_to_graph_Basic_next_step[OF no_next_step]
lemmas simpl_to_graph_Basic_triv = simpl_to_graph_Basic_triv'[where f'="\<lambda>x. x" and Q=UNIV]
lemmas simpl_to_graph_Basic
= simpl_to_graph_Basic_next_step[OF basic_next_step, where Q=UNIV]
definition
"upd_range upd_fun v = range (upd_fun (\<lambda>_. v))"
lemma simpl_to_graph_cbreak:
"eq_impl nn eqs (\<lambda>gst sst. eqs2 gst (exn_upd (\<lambda>_. Break) sst) \<and> exn_upd (\<lambda>_. Break) sst \<in> I) (P \<inter> I)
\<Longrightarrow> simpl_to_graph SGamma GGamma f nn
(add_cont com.Throw con) n tS (upd_range exn_upd Break) I eqs2 out_eqs
\<Longrightarrow> simpl_to_graph SGamma GGamma f nn
(add_cont (cbreak exn_upd) con) n tS P I eqs out_eqs"
apply (simp add: cbreak_def simpl_to_graph_Seq)
apply (rule_tac simpl_to_graph_Basic_triv'[rotated])
apply (rule simpl_to_graph_Skip_immediate)
apply simp
apply (simp add: upd_range_def)
done
lemma simpl_to_graph_ccatchbrk_Break:
"\<forall>f s. exn_var (exn_upd f s) = f (exn_var s)
\<Longrightarrow> eq_impl nn eqs eqs2 (upd_range exn_upd Break \<inter> I)
\<Longrightarrow> simpl_to_graph SGamma GGamma f nn
(add_cont com.Skip con) n tS (upd_range exn_upd Break) I eqs2 out_eqs
\<Longrightarrow> simpl_to_graph SGamma GGamma f nn
(add_cont (ccatchbrk exn_var) con) n tS (upd_range exn_upd Break) I eqs out_eqs"
apply (simp add: ccatchbrk_def)
apply (rule simpl_to_graph_step_R_unchanged)
apply (simp add: upd_range_def)
apply (blast intro: add_cont_step step.intros)
apply (erule simpl_to_graph_weaken, simp add: eq_impl_def)
done
lemma simpl_to_graph_ccatchbrk_Return:
"\<forall>f s. exn_var (exn_upd f s) = f (exn_var s)
\<Longrightarrow> eq_impl nn eqs eqs2 (upd_range exn_upd Return \<inter> I)
\<Longrightarrow> simpl_to_graph SGamma GGamma f nn
(add_cont com.Throw con) n tS (upd_range exn_upd Return) I eqs2 out_eqs
\<Longrightarrow> simpl_to_graph SGamma GGamma f nn
(add_cont (ccatchbrk exn_var) con) n tS (upd_range exn_upd Return) I eqs out_eqs"
apply (simp add: ccatchbrk_def)
apply (rule simpl_to_graph_step_R_unchanged)
apply (simp add: upd_range_def)
apply (rule add_cont_step step.CondFalse)+
apply clarsimp
apply (erule simpl_to_graph_weaken, simp add: eq_impl_def)
done
lemma simpl_to_graph_creturn_void:
"eq_impl nn eqs (\<lambda>gst sst. eqs2 gst (exn_upd (\<lambda>_. Return) sst) \<and> exn_upd (\<lambda>_. Return) sst \<in> I) (P \<inter> I)
\<Longrightarrow> simpl_to_graph SGamma GGamma f nn
(add_cont com.Throw con) n tS (upd_range exn_upd Return) I eqs2 out_eqs
\<Longrightarrow> simpl_to_graph SGamma GGamma f nn
(add_cont (creturn_void exn_upd) con) n tS P I eqs out_eqs"
apply (simp add: creturn_void_def simpl_to_graph_Seq)
apply (rule_tac simpl_to_graph_Basic_triv'[rotated])
apply (rule simpl_to_graph_Skip_immediate)
apply simp
apply (simp add: upd_range_def)
done
lemma rtranclp_respects_fun:
assumes respects: "\<And>x y. R x y \<Longrightarrow> R (f x) (f y)"
shows "R\<^sup>*\<^sup>* x y \<Longrightarrow> R\<^sup>*\<^sup>* (f x) (f y)"
apply (induct rule: rtranclp.induct)
apply (fastforce intro: respects elim: rtranclp_trans)+
done
lemma add_cont_steps:
"\<Gamma> \<turnstile> (com, xs) \<rightarrow>\<^sup>* (com', xs')
\<Longrightarrow> \<Gamma> \<turnstile> (add_cont com con, xs) \<rightarrow>\<^sup>* (add_cont com' con, xs')"
apply (drule_tac f="\<lambda>(a, b). (add_cont a con, b)" in rtranclp_respects_fun[rotated])
apply clarsimp
apply (erule add_cont_step)
apply simp
done
lemma simpl_to_graph_steps_Fault:
"\<forall>s \<in> P \<inter> I. \<exists>com'. SGamma \<turnstile> (com, Normal s) \<rightarrow>\<^sup>* (com', Fault F)
\<Longrightarrow> simpl_to_graph SGamma GGamma gf nn (add_cont com con) n Q P I eqs out_eqs"
apply (clarsimp intro!: simpl_to_graph_steps_Fault1)
apply (drule_tac x=s in bspec, clarsimp+)
apply (rule exI)
apply (erule add_cont_steps)
done
lemma simpl_to_graph_Guard:
"\<lbrakk> nn = NextNode m; eq_impl nn eqs eqs2 (P \<inter> I \<inter> G);
simpl_to_graph SGamma GGamma gf nn (add_cont c con) n Q (G \<inter> P) I eqs2 out_eqs \<rbrakk>
\<Longrightarrow> simpl_to_graph SGamma GGamma gf nn (add_cont (com.Guard F G c) con) n Q P I eqs out_eqs"
apply clarsimp
apply (rule_tac S=G in simpl_to_graph_cases)
apply (rule simpl_to_graph_step_R_unchanged[rotated])
apply (erule simpl_to_graph_weaken)
apply (simp add: eq_impl_def)
apply (rule add_cont_step)
apply (blast intro: step.Guard)
apply (rule simpl_to_graph_steps_Fault)
apply (blast intro: step.GuardFault)
done
lemma simpl_to_graph_done:
"\<lbrakk> eq_impl nn eqs out_eqs (P \<inter> I) \<rbrakk>
\<Longrightarrow> simpl_to_graph SGamma GGamma gf Ret (add_cont com.Skip []) n Q P I eqs out_eqs"
apply (clarsimp simp: c_trace_def add_cont_Nil intro!: simpl_to_graphI)
apply (frule_tac i=n' in exec_trace_step_cases)
apply (rule exI, rule context_conjI)
apply (erule(1) nat_trace_rel_final, simp add: final_def)
apply (clarsimp simp: trace_end_cut exec_graph_step_def)
apply (clarsimp simp: exec_trace_def trace_end_eq_Some
eq_impl_def trace_end_match_def)
done
lemma eq_impl_refl:
"eq_impl nn eqs eqs P"
by (simp add: eq_impl_def)
lemmas simpl_to_graph_done2 = simpl_to_graph_done[OF eq_impl_refl]
lemmas simpl_to_graph_creturn_void2 = simpl_to_graph_creturn_void[where nn=Ret, OF eq_impl_refl]
lemma simpl_to_graph_noop_Basic:
"\<lbrakk> GGamma gf = Some gfc; function_graph gfc m = Some (node.Basic nn upds);
eq_impl nn eqs (\<lambda>gst sst. eqs2 (upd_vars upds gst) sst) (P \<inter> I);
simpl_to_graph SGamma GGamma gf nn c n Q P I eqs2 out_eqs \<rbrakk>
\<Longrightarrow> simpl_to_graph SGamma GGamma gf (NextNode m) c n Q P I eqs out_eqs"
apply (rule simpl_to_graph_step_general[where i=1 and j=0, rotated])
apply simp+
apply (simp add: exec_graph_step_image_node eq_impl_def K_def)
done
lemma simpl_to_graph_noop:
"\<lbrakk> GGamma gf = Some gfc; function_graph gfc m = Some (node.Basic nn []);
simpl_to_graph SGamma GGamma gf nn c n Q P I eqs2 out_eqs;
eq_impl nn eqs eqs2 (P \<inter> I) \<rbrakk>
\<Longrightarrow> simpl_to_graph SGamma GGamma gf (NextNode m) c n Q P I eqs out_eqs"
apply (erule(1) simpl_to_graph_noop_Basic, simp_all)
apply (simp add: upd_vars_def save_vals_def eq_impl_def)
done
lemmas simpl_to_graph_nearly_done
= simpl_to_graph_noop[where c="add_cont com.Skip []"]
lemma eq_impl_triv: "eq_impl nn eqs eqs S"
by (simp add: eq_impl_def)
lemmas simpl_to_graph_noop_same_eqs
= simpl_to_graph_noop[OF _ _ _ eq_impl_triv]
definition
exec_trace_inputs :: "graph_function \<Rightarrow> trace \<Rightarrow> variable list"
where
"exec_trace_inputs gfun tr = (case tr 0 of Some [(nn, gst, _)]
=> acc_vars (function_inputs gfun) gst)"
definition
graph_fun_refines
where
"graph_fun_refines SGamma GGamma I inputs proc outputs fname
= (\<exists>gf. GGamma fname = Some gf \<and> length (function_inputs gf) = length inputs
\<and> length (function_outputs gf) = length outputs
\<and> distinct (function_inputs gf)
\<and> (\<forall>tr \<in> exec_trace GGamma fname.
\<forall>s. map (\<lambda>i. i s) inputs = exec_trace_inputs gf tr \<and> s \<in> I
\<longrightarrow> ((\<exists>ft. SGamma \<turnstile> \<langle>com.Call proc, Normal s\<rangle> \<Rightarrow> Fault ft)
\<or> (trace_end tr = None \<and> \<not> terminates SGamma (com.Call proc) (Normal s))
\<or> (\<exists>gst sst. SGamma \<turnstile> \<langle>com.Call proc, Normal s\<rangle> \<Rightarrow> Normal sst
\<and> trace_end tr = Some [(Ret, gst, fname)]
\<and> sst \<in> I \<and> map (\<lambda>j. j sst) outputs
= acc_vars (function_outputs gf) gst))))"
lemma var_acc_var_upd:
"var_acc nm (var_upd nm' v st) = (if nm = nm' then v else var_acc nm st)"
by (cases st, simp add: var_acc_def var_upd_def)
lemma var_acc_var_upd_same[simp]:
"var_acc nm (var_upd nm v st) = v"
by (simp add: var_acc_var_upd)
lemma var_acc_var_upd_diff:
"nm \<noteq> nm' \<Longrightarrow> var_acc nm (var_upd nm' v st) = var_acc nm st"
by (simp add: var_acc_var_upd)
lemma fetch_returned:
"\<lbrakk> distinct vs; length vs = length xs \<rbrakk>
\<Longrightarrow> acc_vars vs (save_vals vs xs st) = xs"
apply (induct vs arbitrary: xs st)
apply (simp add: acc_vars_def)
apply (case_tac xs, simp_all add: save_vals_def acc_vars_def)
apply (rule_tac P="\<lambda>st. var_acc a st = b" and Q="\<lambda>x. x \<in> set xs" for a b xs
in fold_invariant, simp)
apply simp
apply (clarsimp simp: var_acc_var_upd set_zip)
done
lemma c_trace_nontermination:
"tr \<in> c_trace \<Gamma>
\<Longrightarrow> trace_end tr = None
\<Longrightarrow> tr 0 = Some (com, st)
\<Longrightarrow> \<not> terminates \<Gamma> com st"
apply (frule trace_end_NoneD, simp add: c_trace_def)
apply (erule disjE)
apply (clarsimp simp: c_trace_def nat_trace_rel_def)+
apply (drule terminates_impl_no_infinite_trans_computation)
apply auto
done
lemma trace_end_Ret_Err:
"trace \<in> exec_trace Gamma fname
\<Longrightarrow> trace_end trace = Some v
\<Longrightarrow> \<exists>gst er. v = [(er, gst, fname)] \<and> er \<in> {Ret, Err}"
apply (frule trace_end_SomeD)
apply (clarsimp simp: exec_trace_def, assumption)
apply clarsimp
apply (frule(1) exec_trace_invariant)
apply (auto simp: continuing_def exec_graph_invariant_Cons
split: list.split_asm next_node.split_asm,
auto simp: exec_graph_invariant_def)
done
lemma graph_fun_refines_from_simpl_to_graph_with_refine:
"\<lbrakk> SGamma proc = Some com; GGamma fname = Some gf;
simple_simpl_refines SGamma com' com;
\<And>Q. simpl_to_graph SGamma GGamma fname (NextNode (entry_point gf)) (add_cont com' []) 0
[Q] UNIV I eqs
(\<lambda>s s'. map (\<lambda>i. var_acc i s) (function_outputs gf) = map (\<lambda>i. i s') outs);
eq_impl (NextNode (entry_point gf))