-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathCoincidence.thy
1700 lines (1666 loc) · 110 KB
/
Coincidence.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 "Coincidence"
imports
Ordinary_Differential_Equations.ODE_Analysis
"Ids"
"Lib"
"Syntax"
"Denotational_Semantics"
"Frechet_Correctness"
"Static_Semantics"
begin
section \<open>Coincidence Theorems and Corollaries\<close>
text \<open>This section proves coincidence: semantics of terms, odes, formulas and programs depend only
on the free variables. This is one of the major lemmas for the correctness of uniform substitutions.
Along the way, we also prove the equivalence between two similar, but different semantics for ODE programs:
It does not matter whether the semantics of ODE's insist on the existence of a solution that agrees
with the start state on all variables vs. one that agrees only on the variables that are actually
relevant to the ODE. This is proven here by simultaneous induction with the coincidence theorem
for the following reason:
The reason for having two different semantics is that some proofs are easier with one semantics
and other proofs are easier with the other definition. The coincidence proof is either with the
more complicated definition, which should not be used as the main definition because it would make
the specification for the dL semantics significantly larger, effectively increasing the size of
the trusted core. However, that the proof of equivalence between the semantics using the coincidence
lemma for formulas. In order to use the coincidence proof in the equivalence proof and the equivalence
proof in the coincidence proof, they are proved by simultaneous induction.
\<close>
subsection \<open>Term Coincidence Theorems\<close>
lemma coincidence_sterm:"Vagree \<nu> \<nu>' (FVT \<theta>) \<Longrightarrow> sterm_sem I \<theta> (fst \<nu>) = sterm_sem I \<theta> (fst \<nu>')"
apply(induct "\<theta>") (* 7 subgoals *)
apply(auto simp add: Vagree_def)
by (meson rangeI)
lemma coincidence_sterm':"dfree \<theta> \<Longrightarrow> Vagree \<nu> \<nu>' (FVT \<theta>) \<Longrightarrow> Iagree I J {Inl x |x. x \<in> SIGT \<theta>} \<Longrightarrow> sterm_sem I \<theta> (fst \<nu>) = sterm_sem J \<theta> (fst \<nu>')"
proof (induction rule: dfree.induct)
case (dfree_Fun i args )
then show ?case
proof (auto)
from dfree_Fun.IH have free:"(\<And>i. dfree (args i))"
and IH:"(\<And>i. Vagree \<nu> \<nu>' (FVT (args i)) \<Longrightarrow> Iagree I J {Inl x |x. x \<in> SIGT (args i)} \<Longrightarrow> sterm_sem I (args i) (fst \<nu>) = sterm_sem J (args i) (fst \<nu>'))"
by auto
from dfree_Fun.prems have VA:"Vagree \<nu> \<nu>' (\<Union>i. FVT (args i))"
and IA:"Iagree I J {Inl x |x. x = i \<or> (\<exists>xa. x \<in> SIGT (args xa))}" by auto
from IA have IAorig:"Iagree I J {Inl x |x. x \<in> SIGT (Function i args)}" by auto
from Iagree_Func[OF IAorig] have eqF:"Functions I i = Functions J i" by auto
have Vsubs:"\<And>i. FVT (args i) \<subseteq> (\<Union>i. FVT (args i))" by auto
from VA
have VAs:"\<And>i. Vagree \<nu> \<nu>' (FVT (args i))"
using agree_sub[OF Vsubs] by auto
have Isubs:"\<And>j. {Inl x |x. x \<in> SIGT (args j)} \<subseteq> {Inl x |x. x \<in> SIGT (Function i args)}"
by auto
from IA
have IAs:"\<And>i. Iagree I J {Inl x |x. x \<in> SIGT (args i)}"
using Iagree_sub[OF Isubs] by auto
show "Functions I i (\<chi> i. sterm_sem I (args i) (fst \<nu>)) = Functions J i (\<chi> i. sterm_sem J (args i) (fst \<nu>'))"
using IH[OF VAs IAs] eqF by auto
qed
next
case (dfree_Plus \<theta>\<^sub>1 \<theta>\<^sub>2)
then show ?case
proof (auto)
assume "dfree \<theta>\<^sub>1" "dfree \<theta>\<^sub>2"
and IH1:"(Vagree \<nu> \<nu>' (FVT \<theta>\<^sub>1) \<Longrightarrow> Iagree I J {Inl x |x. x \<in> SIGT \<theta>\<^sub>1} \<Longrightarrow> sterm_sem I \<theta>\<^sub>1 (fst \<nu>) = sterm_sem J \<theta>\<^sub>1 (fst \<nu>'))"
and IH2:"(Vagree \<nu> \<nu>' (FVT \<theta>\<^sub>2) \<Longrightarrow> Iagree I J {Inl x |x. x \<in> SIGT \<theta>\<^sub>2} \<Longrightarrow> sterm_sem I \<theta>\<^sub>2 (fst \<nu>) = sterm_sem J \<theta>\<^sub>2 (fst \<nu>'))"
and VA:"Vagree \<nu> \<nu>' (FVT \<theta>\<^sub>1 \<union> FVT \<theta>\<^sub>2)"
and IA:"Iagree I J {Inl x |x. x \<in> SIGT \<theta>\<^sub>1 \<or> x \<in> SIGT \<theta>\<^sub>2}"
from VA
have VAs:"Vagree \<nu> \<nu>' (FVT \<theta>\<^sub>1)" "Vagree \<nu> \<nu>' (FVT \<theta>\<^sub>2)"
unfolding Vagree_def by auto
have Isubs:"{Inl x |x. x \<in> SIGT \<theta>\<^sub>1} \<subseteq> {Inl x |x. x \<in> SIGT (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)}"
"{Inl x |x. x \<in> SIGT \<theta>\<^sub>2} \<subseteq> {Inl x |x. x \<in> SIGT (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)}"
by auto
from IA
have IAs:"Iagree I J {Inl x |x. x \<in> SIGT \<theta>\<^sub>1}"
"Iagree I J {Inl x |x. x \<in> SIGT \<theta>\<^sub>2}"
using Iagree_sub[OF Isubs(1)] Iagree_sub[OF Isubs(2)] by auto
show "sterm_sem I \<theta>\<^sub>1 (fst \<nu>) + sterm_sem I \<theta>\<^sub>2 (fst \<nu>) = sterm_sem J \<theta>\<^sub>1 (fst \<nu>') + sterm_sem J \<theta>\<^sub>2 (fst \<nu>')"
using IH1[OF VAs(1) IAs(1)] IH2[OF VAs(2) IAs(2)] by auto
qed
next
case (dfree_Times \<theta>\<^sub>1 \<theta>\<^sub>2)
then show ?case
proof (auto)
assume "dfree \<theta>\<^sub>1" "dfree \<theta>\<^sub>2"
and IH1:"(Vagree \<nu> \<nu>' (FVT \<theta>\<^sub>1) \<Longrightarrow> Iagree I J {Inl x |x. x \<in> SIGT \<theta>\<^sub>1} \<Longrightarrow> sterm_sem I \<theta>\<^sub>1 (fst \<nu>) = sterm_sem J \<theta>\<^sub>1 (fst \<nu>'))"
and IH2:"(Vagree \<nu> \<nu>' (FVT \<theta>\<^sub>2) \<Longrightarrow> Iagree I J {Inl x |x. x \<in> SIGT \<theta>\<^sub>2} \<Longrightarrow> sterm_sem I \<theta>\<^sub>2 (fst \<nu>) = sterm_sem J \<theta>\<^sub>2 (fst \<nu>'))"
and VA:"Vagree \<nu> \<nu>' (FVT \<theta>\<^sub>1 \<union> FVT \<theta>\<^sub>2)"
and IA:"Iagree I J {Inl x |x. x \<in> SIGT \<theta>\<^sub>1 \<or> x \<in> SIGT \<theta>\<^sub>2}"
from VA
have VAs:"Vagree \<nu> \<nu>' (FVT \<theta>\<^sub>1)" "Vagree \<nu> \<nu>' (FVT \<theta>\<^sub>2)"
unfolding Vagree_def by auto
have Isubs:"{Inl x |x. x \<in> SIGT \<theta>\<^sub>1} \<subseteq> {Inl x |x. x \<in> SIGT (Times \<theta>\<^sub>1 \<theta>\<^sub>2)}"
"{Inl x |x. x \<in> SIGT \<theta>\<^sub>2} \<subseteq> {Inl x |x. x \<in> SIGT (Times \<theta>\<^sub>1 \<theta>\<^sub>2)}"
by auto
from IA
have IAs:"Iagree I J {Inl x |x. x \<in> SIGT \<theta>\<^sub>1}"
"Iagree I J {Inl x |x. x \<in> SIGT \<theta>\<^sub>2}"
using Iagree_sub[OF Isubs(1)] Iagree_sub[OF Isubs(2)] by auto
show "sterm_sem I \<theta>\<^sub>1 (fst \<nu>) * sterm_sem I \<theta>\<^sub>2 (fst \<nu>) = sterm_sem J \<theta>\<^sub>1 (fst \<nu>') * sterm_sem J \<theta>\<^sub>2 (fst \<nu>')"
using IH1[OF VAs(1) IAs(1)] IH2[OF VAs(2) IAs(2)] by auto
qed
qed (unfold Vagree_def Iagree_def, auto)
lemma coincidence_frechet :
fixes I :: "interp" and \<nu> :: "state" and \<nu>'::"state"
shows "dfree \<theta> \<Longrightarrow> Vagree \<nu> \<nu>' (FVDiff \<theta>) \<Longrightarrow> frechet I \<theta> (fst \<nu>) (snd \<nu>) = frechet I \<theta> (fst \<nu>') (snd \<nu>')"
proof (induction rule: dfree.induct)
case dfree_Var then show ?case
by (auto simp: inner_prod_eq Vagree_def)
next
case dfree_Const then show ?case
by auto
next
case (dfree_Fun var args)
have free:"(\<And>i. dfree (args i))"
and IH:"(\<And>i. Vagree \<nu> \<nu>' (FVDiff (args i)) \<Longrightarrow> frechet I (args i) (fst \<nu>) (snd \<nu>) = frechet I (args i) (fst \<nu>') (snd \<nu>'))"
and agree:"Vagree \<nu> \<nu>' (FVDiff ($f var args))"
using dfree_Fun.IH dfree_Fun.prems by auto
have frees:"(\<And>i. dfree (args i))" using free by (auto simp add: rangeI)
have agrees:"\<And>i. Vagree \<nu> \<nu>' (FVDiff (args i))" using agree agree_func by metis
have agrees':"\<And>i. Vagree \<nu> \<nu>' (FVT (args i))"
subgoal for i
using agrees[of i] FVDiff_sub[of "args i"] unfolding Vagree_def by blast
done
have sterms:"\<And>i. sterm_sem I (args i) (fst \<nu>) = sterm_sem I (args i) (fst \<nu>')"
by (rule coincidence_sterm[of "\<nu>" "\<nu>'", OF agrees'])
have frechets:"\<And>i. frechet I (args i) (fst \<nu>) (snd \<nu>) = frechet I (args i) (fst \<nu>') (snd \<nu>')" using IH agrees frees rangeI by blast
show "?case"
using agrees sterms frechets by (auto)
next
case (dfree_Neg t)
assume dfree1:"dfree t"
assume IH1:"(Vagree \<nu> \<nu>' (FVDiff t) \<Longrightarrow> frechet I t (fst \<nu>) (snd \<nu>) = frechet I t (fst \<nu>') (snd \<nu>'))"
assume agree:"Vagree \<nu> \<nu>' (FVDiff (Neg t))"
have agree1:"Vagree \<nu> \<nu>' (FVDiff t)" using agree agree_neg by (blast)
have IH1':"(frechet I t (fst \<nu>) (snd \<nu>) = frechet I t (fst \<nu>') (snd \<nu>'))"
using IH1 agree1 by (auto)
show "?case"
by (metis FVT.simps(4) IH1' UnCI Vagree_def coincidence_sterm frechet.simps(3) mem_Collect_eq)
next
case (dfree_Plus t1 t2)
assume dfree1:"dfree t1"
assume IH1:"(Vagree \<nu> \<nu>' (FVDiff t1) \<Longrightarrow> frechet I t1 (fst \<nu>) (snd \<nu>) = frechet I t1 (fst \<nu>') (snd \<nu>'))"
assume dfree2:"dfree t2"
assume IH2:"(Vagree \<nu> \<nu>' (FVDiff t2) \<Longrightarrow> frechet I t2 (fst \<nu>) (snd \<nu>) = frechet I t2 (fst \<nu>') (snd \<nu>'))"
assume agree:"Vagree \<nu> \<nu>' (FVDiff (Plus t1 t2))"
have agree1:"Vagree \<nu> \<nu>' (FVDiff t1)" using agree agree_plus1 by (blast)
have agree2:"Vagree \<nu> \<nu>' (FVDiff t2)" using agree agree_plus2 by (blast)
have IH1':"(frechet I t1 (fst \<nu>) (snd \<nu>) = frechet I t1 (fst \<nu>') (snd \<nu>'))"
using IH1 agree1 by (auto)
have IH2':"(frechet I t2 (fst \<nu>) (snd \<nu>) = frechet I t2 (fst \<nu>') (snd \<nu>'))"
using IH2 agree2 by (auto)
show "?case"
by(metis FVT_Plus IH1' IH2' UnCI Vagree_def coincidence_sterm Frechet_Plus mem_Collect_eq)
next
case (dfree_Times t1 t2)
assume dfree1:"dfree t1"
assume IH1:"(Vagree \<nu> \<nu>' (FVDiff t1) \<Longrightarrow> frechet I t1 (fst \<nu>) (snd \<nu>) = frechet I t1 (fst \<nu>') (snd \<nu>'))"
assume dfree2:"dfree t2"
assume IH2:"(Vagree \<nu> \<nu>' (FVDiff t2) \<Longrightarrow> frechet I t2 (fst \<nu>) (snd \<nu>) = frechet I t2 (fst \<nu>') (snd \<nu>'))"
assume agree:"Vagree \<nu> \<nu>' (FVDiff (Times t1 t2))"
have agree1:"Vagree \<nu> \<nu>' (FVDiff t1)" using agree agree_times1 by blast
have agree2:"Vagree \<nu> \<nu>' (FVDiff t2)" using agree agree_times2 by blast
have agree1':"Vagree \<nu> \<nu>' (FVT t1)"
using agree1 apply(auto simp add: Vagree_def)
using primify_contains by blast+
have agree2':"Vagree \<nu> \<nu>' (FVT t2)"
using agree2 apply(auto simp add: Vagree_def)
using primify_contains by blast+
have IH1':"(frechet I t1 (fst \<nu>) (snd \<nu>) = frechet I t1 (fst \<nu>') (snd \<nu>'))"
using IH1 agree1 by (auto)
have IH2':"(frechet I t2 (fst \<nu>) (snd \<nu>) = frechet I t2 (fst \<nu>') (snd \<nu>'))"
using IH2 agree2 by (auto)
have almost:"Vagree \<nu> \<nu>' (FVT (Times t1 t2)) \<Longrightarrow> frechet I (Times t1 t2) (fst \<nu>) (snd \<nu>) = frechet I (Times t1 t2) (fst \<nu>') (snd \<nu>')"
by (auto simp add: UnCI Vagree_def agree IH1' IH2' coincidence_sterm[OF agree1', of I] coincidence_sterm[OF agree2', of I])
show "?case"
using agree FVDiff_sub almost
by (metis agree_supset)
qed
lemma coincidence_frechet' :
fixes I J :: "interp" and \<nu> :: "state" and \<nu>'::"state"
shows "dfree \<theta> \<Longrightarrow> Vagree \<nu> \<nu>' (FVDiff \<theta>) \<Longrightarrow> Iagree I J {Inl x | x. x \<in> (SIGT \<theta>)} \<Longrightarrow> frechet I \<theta> (fst \<nu>) (snd \<nu>) = frechet J \<theta> (fst \<nu>') (snd \<nu>')"
proof (induction rule: dfree.induct)
case dfree_Var then show ?case
by (auto simp: inner_prod_eq Vagree_def)
next
case dfree_Const then show ?case
by auto
next
case (dfree_Fun var args)
have free:"(\<And>i. dfree (args i))"
and IH:"(\<And>i. Vagree \<nu> \<nu>' (FVDiff (args i)) \<Longrightarrow> Iagree I J {Inl x |x. x \<in> SIGT (args i)} \<Longrightarrow> frechet I (args i) (fst \<nu>) (snd \<nu>) = frechet J (args i) (fst \<nu>') (snd \<nu>'))"
and agree:"Vagree \<nu> \<nu>' (FVDiff ($f var args))"
and IA:"Iagree I J {Inl x |x. x \<in> SIGT ($f var args)}"
using dfree_Fun.IH dfree_Fun.prems by auto
have frees:"(\<And>i. dfree (args i))" using free by (auto simp add: rangeI)
have agrees:"\<And>i. Vagree \<nu> \<nu>' (FVDiff (args i))" using agree agree_func by metis
then have agrees':"\<And>i. Vagree \<nu> \<nu>' (FVT (args i))"
using agrees FVDiff_sub
by (metis agree_sub)
from Iagree_Func [OF IA ]have fEq:"Functions I var = Functions J var" by auto
have subs:"\<And>i.{Inl x |x. x \<in> SIGT (args i)} \<subseteq> {Inl x |x. x \<in> SIGT ($f var args)}"
by auto
from IA have IAs:"\<And>i. Iagree I J {Inl x |x. x \<in> SIGT (args i)}"
using Iagree_sub[OF subs] by auto
have sterms:"\<And>i. sterm_sem I (args i) (fst \<nu>) = sterm_sem J (args i) (fst \<nu>')"
subgoal for i
using frees agrees' coincidence_sterm'[of "args i" \<nu> \<nu>' I J] IAs
by (auto)
done
have frechets:"\<And>i. frechet I (args i) (fst \<nu>) (snd \<nu>) = frechet J (args i) (fst \<nu>') (snd \<nu>')"
using IH[OF agrees IAs] agrees frees rangeI by blast
show "?case"
using agrees agrees' sterms frechets fEq by auto
next
case (dfree_Neg t1)
assume dfree1:"dfree t1"
assume IH1:"(Vagree \<nu> \<nu>' (FVDiff t1) \<Longrightarrow> Iagree I J {Inl x |x. x \<in> SIGT t1} \<Longrightarrow> frechet I t1 (fst \<nu>) (snd \<nu>) = frechet J t1 (fst \<nu>') (snd \<nu>'))"
assume agree:"Vagree \<nu> \<nu>' (FVDiff (Neg t1))"
assume IA:"Iagree I J {Inl x |x. x \<in> SIGT (Neg t1)}"
have subs:"{Inl x |x. x \<in> SIGT t1} \<subseteq> {Inl x |x. x \<in> SIGT (Neg t1)}"
by auto
from IA
have IA1:"Iagree I J {Inl x |x. x \<in> SIGT t1}"
using Iagree_sub[OF subs(1)] by auto
have agree1:"Vagree \<nu> \<nu>' (FVDiff t1)" using agree agree_neg by (blast)
have agree1':"Vagree \<nu> \<nu>' (FVT t1)" using agree1 primify_contains by (auto simp add: Vagree_def, metis)
have IH1':"(frechet I t1 (fst \<nu>) (snd \<nu>) = frechet J t1 (fst \<nu>') (snd \<nu>'))"
using IH1 agree1 IA1 by (auto)
show "?case"
using coincidence_sterm[OF agree1'] coincidence_sterm[OF agree1']
by (auto simp add: IH1' UnCI Vagree_def)
next
case (dfree_Plus t1 t2)
assume dfree1:"dfree t1"
assume dfree2:"dfree t2"
assume IH1:"(Vagree \<nu> \<nu>' (FVDiff t1) \<Longrightarrow> Iagree I J {Inl x |x. x \<in> SIGT t1} \<Longrightarrow> frechet I t1 (fst \<nu>) (snd \<nu>) = frechet J t1 (fst \<nu>') (snd \<nu>'))"
assume IH2:"(Vagree \<nu> \<nu>' (FVDiff t2) \<Longrightarrow> Iagree I J {Inl x |x. x \<in> SIGT t2} \<Longrightarrow> frechet I t2 (fst \<nu>) (snd \<nu>) = frechet J t2 (fst \<nu>') (snd \<nu>'))"
assume agree:"Vagree \<nu> \<nu>' (FVDiff (Plus t1 t2))"
assume IA:"Iagree I J {Inl x |x. x \<in> SIGT (Plus t1 t2)}"
have subs:"{Inl x |x. x \<in> SIGT t1} \<subseteq> {Inl x |x. x \<in> SIGT (Plus t1 t2)}" "{Inl x |x. x \<in> SIGT t2} \<subseteq> {Inl x |x. x \<in> SIGT (Plus t1 t2)}"
by auto
from IA
have IA1:"Iagree I J {Inl x |x. x \<in> SIGT t1}"
and IA2:"Iagree I J {Inl x |x. x \<in> SIGT t2}"
using Iagree_sub[OF subs(1)] Iagree_sub[OF subs(2)] by auto
have agree1:"Vagree \<nu> \<nu>' (FVDiff t1)" using agree agree_plus1 by (blast)
have agree2:"Vagree \<nu> \<nu>' (FVDiff t2)" using agree agree_plus2 by (blast)
have agree1':"Vagree \<nu> \<nu>' (FVT t1)" using agree1 primify_contains by (auto simp add: Vagree_def, metis)
have agree2':"Vagree \<nu> \<nu>' (FVT t2)" using agree2 primify_contains by (auto simp add: Vagree_def, metis)
have IH1':"(frechet I t1 (fst \<nu>) (snd \<nu>) = frechet J t1 (fst \<nu>') (snd \<nu>'))"
using IH1 agree1 IA1 by (auto)
have IH2':"(frechet I t2 (fst \<nu>) (snd \<nu>) = frechet J t2 (fst \<nu>') (snd \<nu>'))"
using IH2 agree2 IA2 by (auto)
show "?case"
using coincidence_sterm[OF agree1'] coincidence_sterm[OF agree1'] coincidence_sterm[OF agree2']
by (auto simp add: IH1' IH2' UnCI Vagree_def)
next
case (dfree_Times t1 t2)
assume dfree1:"dfree t1"
assume dfree2:"dfree t2"
assume IH1:"(Vagree \<nu> \<nu>' (FVDiff t1) \<Longrightarrow> Iagree I J {Inl x |x. x \<in> SIGT t1} \<Longrightarrow> frechet I t1 (fst \<nu>) (snd \<nu>) = frechet J t1 (fst \<nu>') (snd \<nu>'))"
assume IH2:"(Vagree \<nu> \<nu>' (FVDiff t2) \<Longrightarrow> Iagree I J {Inl x |x. x \<in> SIGT t2} \<Longrightarrow> frechet I t2 (fst \<nu>) (snd \<nu>) = frechet J t2 (fst \<nu>') (snd \<nu>'))"
assume agree:"Vagree \<nu> \<nu>' (FVDiff (Times t1 t2))"
assume IA:"Iagree I J {Inl x |x. x \<in> SIGT (Times t1 t2)}"
have subs:"{Inl x |x. x \<in> SIGT t1} \<subseteq> {Inl x |x. x \<in> SIGT (Times t1 t2)}" "{Inl x |x. x \<in> SIGT t2} \<subseteq> {Inl x |x. x \<in> SIGT (Times t1 t2)}"
by auto
from IA
have IA1:"Iagree I J {Inl x |x. x \<in> SIGT t1}"
and IA2:"Iagree I J {Inl x |x. x \<in> SIGT t2}"
using Iagree_sub[OF subs(1)] Iagree_sub[OF subs(2)] by auto
have agree1:"Vagree \<nu> \<nu>' (FVDiff t1)" using agree agree_times1 by (blast)
then have agree1':"Vagree \<nu> \<nu>' (FVT t1)"
using agree1 primify_contains by (auto simp add: Vagree_def, metis)
have agree2:"Vagree \<nu> \<nu>' (FVDiff t2)" using agree agree_times2 by (blast)
then have agree2':"Vagree \<nu> \<nu>' (FVT t2)"
using agree2 primify_contains by (auto simp add: Vagree_def, metis)
have IH1':"(frechet I t1 (fst \<nu>) (snd \<nu>) = frechet J t1 (fst \<nu>') (snd \<nu>'))"
using IH1 agree1 IA1 by (auto)
have IH2':"(frechet I t2 (fst \<nu>) (snd \<nu>) = frechet J t2 (fst \<nu>') (snd \<nu>'))"
using IH2 agree2 IA2 by (auto)
note co1 = coincidence_sterm'[of "t1" \<nu> \<nu>' I J] and co2 = coincidence_sterm'[of "t2" \<nu> \<nu>' I J]
show "?case"
using co1 [OF dfree1 agree1' IA1] co2 [OF dfree2 agree2' IA2] IH1' IH2' by auto
qed
lemma coincidence_dterm:
fixes I :: "interp" and \<nu> :: "state" and \<nu>'::"state"
shows "dsafe \<theta> \<Longrightarrow> Vagree \<nu> \<nu>' (FVT \<theta>) \<Longrightarrow> dterm_sem I \<theta> \<nu> = dterm_sem I \<theta> \<nu>'"
proof (induction rule: dsafe.induct)
case (dsafe_Funl f)
assume "Vagree \<nu> \<nu>' (FVT ($$F f))"
then have agree:"Vagree \<nu> \<nu>' UNIV" by simp
then show "?case"
using agree_UNIV_eq[OF agree] by auto
next
case (dsafe_Fun f args)
have safe:"(\<And>i. dsafe (args i))"
and IH:"\<And>i. Vagree \<nu> \<nu>' (FVT (args i)) \<Longrightarrow> dterm_sem I (args i) \<nu> = dterm_sem I (args i) \<nu>'"
and agree:"Vagree \<nu> \<nu>' (FVT ($f f args))"
using dsafe_Fun.IH dsafe_Fun.prems by auto
then have "\<And>i. Vagree \<nu> \<nu>' (FVT (args i))"
using agree_func_fvt by (metis)
then show "?case"
using safe coincidence_sterm IH rangeI by (auto)
qed (auto simp: Vagree_def directional_derivative_def coincidence_frechet)
lemma coincidence_dterm':
fixes I J :: "interp" and \<nu> :: "state" and \<nu>'::"state"
shows "dsafe \<theta> \<Longrightarrow> Vagree \<nu> \<nu>' (FVT \<theta>) \<Longrightarrow> Iagree I J {Inl x | x. x \<in> (SIGT \<theta>)} \<Longrightarrow> dterm_sem I \<theta> \<nu> = dterm_sem J \<theta> \<nu>'"
proof (induction rule: dsafe.induct)
case (dsafe_Fun f args) then
have safe:"(\<And>i. dsafe (args i))"
and IH:"\<And>i. Vagree \<nu> \<nu>' (FVT (args i)) \<Longrightarrow> Iagree I J {Inl x | x. x \<in> (SIGT (args i))} \<Longrightarrow> dterm_sem I (args i) \<nu> = dterm_sem J (args i) \<nu>'"
and agree:"Vagree \<nu> \<nu>' (FVT ($f f args))"
and IA:"Iagree I J {Inl x |x. x \<in> SIGT ($f f args)}"
by auto
have subs:"\<And>i. {Inl x |x. x \<in> SIGT (args i)} \<subseteq> {Inl x |x. x \<in> SIGT ($f f args)}" by auto
from IA have IAs:
"\<And>i. Iagree I J {Inl x |x. x \<in> SIGT (args i)}"
using Iagree_sub [OF subs IA] by auto
from agree have agrees:"\<And>i. Vagree \<nu> \<nu>' (FVT (args i))"
using agree_func_fvt by (metis)
from Iagree_Func [OF IA] have fEq:"Functions I f = Functions J f" by auto
then show "?case"
using safe coincidence_sterm IH[OF agrees IAs] rangeI agrees fEq
by (auto)
next
case (dsafe_Funl f) then
have agree:"Vagree \<nu> \<nu>' (UNIV)"
and IA:"Iagree I J {Inl x |x. x \<in> SIGT ($$F f)}"
by auto
from Iagree_Funl [OF IA] have fEq:"Funls I f = Funls J f" by auto
then show "?case" using agree_UNIV_eq[OF agree] by auto
next
case (dsafe_Plus \<theta>\<^sub>1 \<theta>\<^sub>2) then
have safe:"dsafe \<theta>\<^sub>1" "dsafe \<theta>\<^sub>2"
and IH1:"Vagree \<nu> \<nu>' (FVT \<theta>\<^sub>1) \<Longrightarrow> Iagree I J {Inl x |x. x \<in> SIGT \<theta>\<^sub>1} \<Longrightarrow> dterm_sem I \<theta>\<^sub>1 \<nu> = dterm_sem J \<theta>\<^sub>1 \<nu>'"
and IH2:"Vagree \<nu> \<nu>' (FVT \<theta>\<^sub>2) \<Longrightarrow> Iagree I J {Inl x |x. x \<in> SIGT \<theta>\<^sub>2} \<Longrightarrow> dterm_sem I \<theta>\<^sub>2 \<nu> = dterm_sem J \<theta>\<^sub>2 \<nu>'"
and VA:"Vagree \<nu> \<nu>' (FVT (Plus \<theta>\<^sub>1 \<theta>\<^sub>2))"
and IA:"Iagree I J {Inl x |x. x \<in> SIGT (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)}"
by auto
from VA have VA1:"Vagree \<nu> \<nu>' (FVT \<theta>\<^sub>1)" and VA2:"Vagree \<nu> \<nu>' (FVT \<theta>\<^sub>2)"
unfolding Vagree_def by auto
have subs:"{Inl x |x. x \<in> SIGT \<theta>\<^sub>1} \<subseteq> {Inl x |x. x \<in> SIGT (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)}"
"{Inl x |x. x \<in> SIGT \<theta>\<^sub>2} \<subseteq> {Inl x |x. x \<in> SIGT (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)}"by auto
from IA have IA1:"Iagree I J {Inl x |x. x \<in> SIGT \<theta>\<^sub>1}" and IA2:"Iagree I J {Inl x |x. x \<in> SIGT \<theta>\<^sub>2}"
using Iagree_sub subs by auto
then show ?case
using IH1[OF VA1 IA1] IH2[OF VA2 IA2] by auto
next
case (dsafe_Times \<theta>\<^sub>1 \<theta>\<^sub>2) then
have safe:"dsafe \<theta>\<^sub>1" "dsafe \<theta>\<^sub>2"
and IH1:"Vagree \<nu> \<nu>' (FVT \<theta>\<^sub>1) \<Longrightarrow> Iagree I J {Inl x |x. x \<in> SIGT \<theta>\<^sub>1} \<Longrightarrow> dterm_sem I \<theta>\<^sub>1 \<nu> = dterm_sem J \<theta>\<^sub>1 \<nu>'"
and IH2:"Vagree \<nu> \<nu>' (FVT \<theta>\<^sub>2) \<Longrightarrow> Iagree I J {Inl x |x. x \<in> SIGT \<theta>\<^sub>2} \<Longrightarrow> dterm_sem I \<theta>\<^sub>2 \<nu> = dterm_sem J \<theta>\<^sub>2 \<nu>'"
and VA:"Vagree \<nu> \<nu>' (FVT (Times \<theta>\<^sub>1 \<theta>\<^sub>2))"
and IA:"Iagree I J {Inl x |x. x \<in> SIGT (Times \<theta>\<^sub>1 \<theta>\<^sub>2)}"
by auto
from VA have VA1:"Vagree \<nu> \<nu>' (FVT \<theta>\<^sub>1)" and VA2:"Vagree \<nu> \<nu>' (FVT \<theta>\<^sub>2)"
unfolding Vagree_def by auto
have subs:"{Inl x |x. x \<in> SIGT \<theta>\<^sub>1} \<subseteq> {Inl x |x. x \<in> SIGT (Times \<theta>\<^sub>1 \<theta>\<^sub>2)}"
"{Inl x |x. x \<in> SIGT \<theta>\<^sub>2} \<subseteq> {Inl x |x. x \<in> SIGT (Times \<theta>\<^sub>1 \<theta>\<^sub>2)}"by auto
from IA have IA1:"Iagree I J {Inl x |x. x \<in> SIGT \<theta>\<^sub>1}" and IA2:"Iagree I J {Inl x |x. x \<in> SIGT \<theta>\<^sub>2}"
using Iagree_sub subs by auto
then show ?case
using IH1[OF VA1 IA1] IH2[OF VA2 IA2] by auto
next
case (dsafe_Div \<theta>\<^sub>1 \<theta>\<^sub>2) then
have safe:"dsafe \<theta>\<^sub>1" "dsafe \<theta>\<^sub>2"
and IH1:"Vagree \<nu> \<nu>' (FVT \<theta>\<^sub>1) \<Longrightarrow> Iagree I J {Inl x |x. x \<in> SIGT \<theta>\<^sub>1} \<Longrightarrow> dterm_sem I \<theta>\<^sub>1 \<nu> = dterm_sem J \<theta>\<^sub>1 \<nu>'"
and IH2:"Vagree \<nu> \<nu>' (FVT \<theta>\<^sub>2) \<Longrightarrow> Iagree I J {Inl x |x. x \<in> SIGT \<theta>\<^sub>2} \<Longrightarrow> dterm_sem I \<theta>\<^sub>2 \<nu> = dterm_sem J \<theta>\<^sub>2 \<nu>'"
and VA:"Vagree \<nu> \<nu>' (FVT (Div \<theta>\<^sub>1 \<theta>\<^sub>2))"
and IA:"Iagree I J {Inl x |x. x \<in> SIGT (Div \<theta>\<^sub>1 \<theta>\<^sub>2)}"
by auto
from VA have VA1:"Vagree \<nu> \<nu>' (FVT \<theta>\<^sub>1)" and VA2:"Vagree \<nu> \<nu>' (FVT \<theta>\<^sub>2)"
unfolding Vagree_def by auto
have subs:"{Inl x |x. x \<in> SIGT \<theta>\<^sub>1} \<subseteq> {Inl x |x. x \<in> SIGT (Div \<theta>\<^sub>1 \<theta>\<^sub>2)}"
"{Inl x |x. x \<in> SIGT \<theta>\<^sub>2} \<subseteq> {Inl x |x. x \<in> SIGT (Div \<theta>\<^sub>1 \<theta>\<^sub>2)}"by auto
from IA have IA1:"Iagree I J {Inl x |x. x \<in> SIGT \<theta>\<^sub>1}" and IA2:"Iagree I J {Inl x |x. x \<in> SIGT \<theta>\<^sub>2}"
using Iagree_sub subs by auto
then show ?case
using IH1[OF VA1 IA1] IH2[OF VA2 IA2] by auto
next
case (dsafe_Max \<theta>\<^sub>1 \<theta>\<^sub>2) then
have safe:"dsafe \<theta>\<^sub>1" "dsafe \<theta>\<^sub>2"
and IH1:"Vagree \<nu> \<nu>' (FVT \<theta>\<^sub>1) \<Longrightarrow> Iagree I J {Inl x |x. x \<in> SIGT \<theta>\<^sub>1} \<Longrightarrow> dterm_sem I \<theta>\<^sub>1 \<nu> = dterm_sem J \<theta>\<^sub>1 \<nu>'"
and IH2:"Vagree \<nu> \<nu>' (FVT \<theta>\<^sub>2) \<Longrightarrow> Iagree I J {Inl x |x. x \<in> SIGT \<theta>\<^sub>2} \<Longrightarrow> dterm_sem I \<theta>\<^sub>2 \<nu> = dterm_sem J \<theta>\<^sub>2 \<nu>'"
and VA:"Vagree \<nu> \<nu>' (FVT (trm.Max \<theta>\<^sub>1 \<theta>\<^sub>2))"
and IA:"Iagree I J {Inl x |x. x \<in> SIGT (trm.Max \<theta>\<^sub>1 \<theta>\<^sub>2)}"
by auto
from VA have VA1:"Vagree \<nu> \<nu>' (FVT \<theta>\<^sub>1)" and VA2:"Vagree \<nu> \<nu>' (FVT \<theta>\<^sub>2)"
unfolding Vagree_def by auto
have subs:"{Inl x |x. x \<in> SIGT \<theta>\<^sub>1} \<subseteq> {Inl x |x. x \<in> SIGT (Max \<theta>\<^sub>1 \<theta>\<^sub>2)}"
"{Inl x |x. x \<in> SIGT \<theta>\<^sub>2} \<subseteq> {Inl x |x. x \<in> SIGT (Max \<theta>\<^sub>1 \<theta>\<^sub>2)}"by auto
from IA have IA1:"Iagree I J {Inl x |x. x \<in> SIGT \<theta>\<^sub>1}" and IA2:"Iagree I J {Inl x |x. x \<in> SIGT \<theta>\<^sub>2}"
using Iagree_sub subs by auto
then show ?case
using IH1[OF VA1 IA1] IH2[OF VA2 IA2] by auto
next
case (dsafe_Min \<theta>\<^sub>1 \<theta>\<^sub>2) then
have safe:"dsafe \<theta>\<^sub>1" "dsafe \<theta>\<^sub>2"
and IH1:"Vagree \<nu> \<nu>' (FVT \<theta>\<^sub>1) \<Longrightarrow> Iagree I J {Inl x |x. x \<in> SIGT \<theta>\<^sub>1} \<Longrightarrow> dterm_sem I \<theta>\<^sub>1 \<nu> = dterm_sem J \<theta>\<^sub>1 \<nu>'"
and IH2:"Vagree \<nu> \<nu>' (FVT \<theta>\<^sub>2) \<Longrightarrow> Iagree I J {Inl x |x. x \<in> SIGT \<theta>\<^sub>2} \<Longrightarrow> dterm_sem I \<theta>\<^sub>2 \<nu> = dterm_sem J \<theta>\<^sub>2 \<nu>'"
and VA:"Vagree \<nu> \<nu>' (FVT (trm.Min \<theta>\<^sub>1 \<theta>\<^sub>2))"
and IA:"Iagree I J {Inl x |x. x \<in> SIGT (trm.Min \<theta>\<^sub>1 \<theta>\<^sub>2)}"
by auto
from VA have VA1:"Vagree \<nu> \<nu>' (FVT \<theta>\<^sub>1)" and VA2:"Vagree \<nu> \<nu>' (FVT \<theta>\<^sub>2)"
unfolding Vagree_def by auto
have subs:"{Inl x |x. x \<in> SIGT \<theta>\<^sub>1} \<subseteq> {Inl x |x. x \<in> SIGT (Max \<theta>\<^sub>1 \<theta>\<^sub>2)}"
"{Inl x |x. x \<in> SIGT \<theta>\<^sub>2} \<subseteq> {Inl x |x. x \<in> SIGT (Max \<theta>\<^sub>1 \<theta>\<^sub>2)}"by auto
from IA have IA1:"Iagree I J {Inl x |x. x \<in> SIGT \<theta>\<^sub>1}" and IA2:"Iagree I J {Inl x |x. x \<in> SIGT \<theta>\<^sub>2}"
using Iagree_sub subs by auto
then show ?case
using IH1[OF VA1 IA1] IH2[OF VA2 IA2] by auto
next
case (dsafe_Abs \<theta>) then
have safe:"dsafe \<theta>"
and IH1:"Vagree \<nu> \<nu>' (FVT \<theta>) \<Longrightarrow> Iagree I J {Inl x |x. x \<in> SIGT \<theta>} \<Longrightarrow> dterm_sem I \<theta> \<nu> = dterm_sem J \<theta> \<nu>'"
and VA:"Vagree \<nu> \<nu>' (FVT (trm.Abs \<theta>))"
and IA:"Iagree I J {Inl x |x. x \<in> SIGT (trm.Abs \<theta>)}"
by auto
from VA have VA1:"Vagree \<nu> \<nu>' (FVT \<theta>)"
unfolding Vagree_def by auto
have subs:"{Inl x |x. x \<in> SIGT \<theta>} \<subseteq> {Inl x |x. x \<in> SIGT (Abs \<theta>)}" by auto
from IA have IA1:"Iagree I J {Inl x |x. x \<in> SIGT \<theta>}"
using Iagree_sub subs by auto
then show ?case
using IH1[OF VA1 IA1] by auto
qed (auto simp: Vagree_def directional_derivative_def coincidence_frechet')
subsection \<open>ODE Coincidence Theorems\<close>
lemma coincidence_ode:
fixes I J :: "interp" and \<nu> :: "state" and \<nu>'::"state"
assumes goodI:"is_interp I"
assumes goodJ:"is_interp J"
shows "osafe ODE \<Longrightarrow>
Vagree \<nu> \<nu>' (Inl ` FVO ODE) \<Longrightarrow>
Iagree I J ({Inl x | x. Inl x \<in> SIGO ODE} \<union> {Inr (Inr x) | x. Inr x \<in> SIGO ODE}) \<Longrightarrow>
ODE_sem I ODE (fst \<nu>) = ODE_sem J ODE (fst \<nu>')"
proof (induction rule: osafe.induct)
case (osafe_Var c sp)
then show ?case
proof (auto, cases sp, simp)
assume sp:"sp = None"
assume VA:"Vagree \<nu> \<nu>' (range Inl)"
have eqV:"(fst \<nu>) = (fst \<nu>')"
using agree_UNIV_fst[OF VA] by auto
assume IA:"Iagree I J {Inr (Inr c)}"
have eqIJ:"ODEs I c All = ODEs J c All"
using Iagree_ODE[OF IA] by auto
have eqbvIJ:"ODEBV I c All = ODEBV J c All"
using Iagree_ODEBV[OF IA] by auto
show "(\<lambda> i. if i \<in> ODEBV I c None then ODEs I c sp (fst \<nu>) $ i else 0)
= (\<lambda> i. if i \<in> ODEBV J c None then ODEs J c sp (fst \<nu>') $ i else 0)"
using sp eqV eqIJ eqbvIJ by (auto)
next
fix x
assume sp:"sp = Some x"
assume VA:"Vagree \<nu> \<nu>' (Inl ` FVO (OVar c sp))"
then have VA:"Vagree \<nu> \<nu>' (range Inl)" using sp by auto
have eqV:"(fst \<nu>) = (fst \<nu>')"
using agree_UNIV_fst[OF VA] by auto
assume IA:"Iagree I J {Inr (Inr c)}"
have eqIJ:"ODEs I c (NB x) = ODEs J c (NB x)"
using Iagree_ODE[OF IA] by auto
have eqbvIJ:"ODEBV I c (NB x) = ODEBV J c (NB x)"
using Iagree_ODEBV[OF IA] by auto
have iBound:"\<And>ode x. ODEBV I ode (NB x) \<subseteq> - {x}" using goodI unfolding is_interp_def by auto
have jBound:"\<And>ode x. ODEBV J ode (NB x) \<subseteq> - {x}" using goodJ unfolding is_interp_def by auto
show "(\<lambda> i. if i \<in> ODEBV I c sp then ODEs I c sp (fst \<nu>) $ i else 0) = (\<lambda> i. if i \<in> ODEBV J c sp then ODEs J c sp (fst \<nu>') $ i else 0)"
using sp eqV eqIJ eqbvIJ by(auto simp add: eqV eqIJ sp eqbvIJ)
qed
next
case (osafe_Sing \<theta> x)
then show ?case
proof (auto)
assume free:"dfree \<theta>"
and VA:"Vagree \<nu> \<nu>' (insert (Inl x) (Inl ` {x. Inl x \<in> FVT \<theta>}))"
and IA:"Iagree I J {Inl x |x. x \<in> SIGT \<theta>}"
from VA have VA':"Vagree \<nu> \<nu>' {Inl x | x. Inl x \<in> FVT \<theta>}" unfolding Vagree_def by auto
have agree_Lem:"\<And>\<theta>. dfree \<theta> \<Longrightarrow> Vagree \<nu> \<nu>' {Inl x | x. Inl x \<in> FVT \<theta>} \<Longrightarrow> Vagree \<nu> \<nu>' (FVT \<theta>)"
subgoal for \<theta>
apply(induction rule: dfree.induct)
by(auto simp add: Vagree_def)
done
have trm:"sterm_sem I \<theta> (fst \<nu>) = sterm_sem J \<theta> (fst \<nu>')"
using coincidence_sterm' free VA' IA agree_Lem[of \<theta>, OF free] by blast
show "(\<lambda> i. if i = x then sterm_sem I \<theta> (fst \<nu>) else 0) = (\<lambda> i. if i = x then sterm_sem J \<theta> (fst \<nu>') else 0)"
by (auto simp add: vec_eq_iff trm)
qed
next
case (osafe_Prod ODE1 ODE2)
then show ?case
proof (auto)
assume safe1:"osafe ODE1"
and safe2:"osafe ODE2"
and disjoint:"ODE_dom ODE1 \<inter> ODE_dom ODE2 = {}"
and IH1:"Vagree \<nu> \<nu>' (Inl ` FVO ODE1) \<Longrightarrow>
Iagree I J ({Inl x |x. Inl x \<in> SIGO ODE1} \<union> {Inr (Inr x) |x. Inr x \<in> SIGO ODE1}) \<Longrightarrow> ODE_sem I ODE1 (fst \<nu>) = ODE_sem J ODE1 (fst \<nu>')"
and IH2:"Vagree \<nu> \<nu>' (Inl ` FVO ODE2) \<Longrightarrow>
Iagree I J ({Inl x |x. Inl x \<in> SIGO ODE2} \<union> {Inr (Inr x) |x. Inr x \<in> SIGO ODE2}) \<Longrightarrow> ODE_sem I ODE2 (fst \<nu>) = ODE_sem J ODE2 (fst \<nu>')"
and VA:"Vagree \<nu> \<nu>' (Inl ` (FVO ODE1 \<union> FVO ODE2))"
and IA:"Iagree I J ({Inl x |x. Inl x \<in> SIGO ODE1 \<or> Inl x \<in> SIGO ODE2} \<union> {Inr (Inr x) |x. Inr x \<in> SIGO ODE1 \<or> Inr x \<in> SIGO ODE2})"
let ?IA = "({Inl x |x. Inl x \<in> SIGO ODE1 \<or> Inl x \<in> SIGO ODE2} \<union> {Inr (Inr x) |x. Inr x \<in> SIGO ODE1 \<or> Inr x \<in> SIGO ODE2})"
have FVsubs:
"Inl ` FVO ODE2 \<subseteq> Inl ` (FVO ODE1 \<union> FVO ODE2)"
"Inl ` FVO ODE1 \<subseteq> Inl ` (FVO ODE1 \<union> FVO ODE2)"
by auto
from VA
have VA1:"Vagree \<nu> \<nu>' (Inl ` FVO ODE1)"
and VA2:"Vagree \<nu> \<nu>' (Inl ` FVO ODE2)"
using agree_sub[OF FVsubs(1)] agree_sub[OF FVsubs(2)]
by (auto)
have SIGsubs:
"({Inl x |x. Inl x \<in> SIGO ODE1} \<union> {Inr (Inr x) |x. Inr x \<in> SIGO ODE1}) \<subseteq> ?IA"
"({Inl x |x. Inl x \<in> SIGO ODE2} \<union> {Inr (Inr x) |x. Inr x \<in> SIGO ODE2}) \<subseteq> ?IA"
by auto
from IA
have IA1:"Iagree I J ({Inl x |x. Inl x \<in> SIGO ODE1} \<union> {Inr (Inr x) |x. Inr x \<in> SIGO ODE1})"
and IA2:"Iagree I J ({Inl x |x. Inl x \<in> SIGO ODE2} \<union> {Inr (Inr x) |x. Inr x \<in> SIGO ODE2})"
using Iagree_sub[OF SIGsubs(1)] Iagree_sub[OF SIGsubs(2)] by auto
show "ODE_sem I ODE1 (fst \<nu>) + ODE_sem I ODE2 (fst \<nu>) = ODE_sem J ODE1 (fst \<nu>') + ODE_sem J ODE2 (fst \<nu>')"
using IH1[OF VA1 IA1] IH2[OF VA2 IA2] by auto
qed
qed
lemma coincidence_ode':
fixes I J :: "interp" and \<nu> :: "simple_state" and \<nu>'::"simple_state"
assumes goodI:"is_interp I"
assumes goodJ:"is_interp J"
shows "
osafe ODE \<Longrightarrow>
VSagree \<nu> \<nu>' (FVO ODE) \<Longrightarrow>
Iagree I J ({Inl x | x. Inl x \<in> SIGO ODE} \<union> {Inr (Inr x) | x. Inr x \<in> SIGO ODE}) \<Longrightarrow>
ODE_sem I ODE \<nu> = ODE_sem J ODE \<nu>'"
using coincidence_ode[of I J ODE "(\<nu>, \<chi> i. 0)" "(\<nu>', \<chi> i. 0)"] goodI goodJ
apply(auto)
unfolding VSagree_def Vagree_def apply auto
done
lemma alt_sem_lemma:"\<And> I::interp. \<And> ODE::ODE. \<And>sol. \<And>t::real. \<And> ab. osafe ODE \<Longrightarrow>
is_interp I \<Longrightarrow>
ODE_sem I ODE (sol t) = ODE_sem I ODE (\<chi> i. if i \<in> FVO ODE then sol t $ i else ab $ i)"
proof -
fix I::"interp"
and ODE::"ODE"
and sol
and t::real
and ab
assume safe:"osafe ODE"
assume good_interp:"is_interp I"
have VA:"VSagree (sol t) (\<chi> i. if i \<in> FVO ODE then sol t $ i else ab $ i) (FVO ODE)"
unfolding VSagree_def Vagree_def by auto
have IA: "Iagree I I ({Inl x | x. Inl x \<in> SIGO ODE} \<union> {Inr (Inr x) | x. Inr x \<in> SIGO ODE})" unfolding Iagree_def by auto
show "ODE_sem I ODE (sol t) = ODE_sem I ODE (\<chi> i. if i \<in> FVO ODE then sol t $ i else ab $ i)"
using coincidence_ode'[OF good_interp good_interp safe VA IA] by auto
qed
lemma bvo_to_fvo:"Inl x \<in> BVO ODE \<Longrightarrow> x \<in> FVO ODE"
proof (induction ODE)
case (OVar x1 x2)
then show ?case by(cases x2,auto)
next
case (OSing x1 x2)
then show ?case by auto
next
case (OProd ODE1 ODE2)
then show ?case by auto
qed
lemma ode_to_fvo:"x \<in> ODE_vars I ODE \<Longrightarrow> x \<in> FVO ODE"
proof (induction ODE)
case (OVar x1 x2)
then show ?case by(cases x2,auto)
next
case (OSing x1 x2)
then show ?case by auto
next
case (OProd ODE1 ODE2)
then show ?case by auto
qed
definition coincide_hp :: "hp \<Rightarrow> interp \<Rightarrow> interp \<Rightarrow> bool"
where "coincide_hp \<alpha> I J \<longleftrightarrow> (\<forall> \<nu> \<nu>' \<mu> V. Iagree I J (SIGP \<alpha>) \<longrightarrow> Vagree \<nu> \<nu>' V \<longrightarrow> V \<supseteq> (FVP \<alpha>) \<longrightarrow> (\<nu>, \<mu>) \<in> prog_sem I \<alpha> \<longrightarrow> (\<exists>\<mu>'. (\<nu>', \<mu>') \<in> prog_sem J \<alpha> \<and> Vagree \<mu> \<mu>' (MBV \<alpha> \<union> V)))"
definition ode_sem_equiv ::"hp \<Rightarrow> interp \<Rightarrow> bool"
where "ode_sem_equiv \<alpha> I \<longleftrightarrow>
(\<forall>ODE::ODE. \<forall>\<phi>::formula. osafe ODE \<longrightarrow> fsafe \<phi> \<longrightarrow>
(\<alpha> = EvolveODE ODE \<phi>) \<longrightarrow>
{(\<nu>, mk_v I ODE \<nu> (sol t)) | \<nu> sol t.
t \<ge> 0 \<and>
(sol solves_ode (\<lambda>_. ODE_sem I ODE)) {0..t} {x. mk_v I ODE \<nu> x \<in> fml_sem I \<phi>} \<and>
VSagree (sol 0) (fst \<nu>) {x | x. Inl x \<in> FVP (EvolveODE ODE \<phi>)}} =
{(\<nu>, mk_v I ODE \<nu> (sol t)) | \<nu> sol t.
t \<ge> 0 \<and>
(sol solves_ode (\<lambda>_. ODE_sem I ODE)) {0..t} {x. mk_v I ODE \<nu> x \<in> fml_sem I \<phi>} \<and>
sol 0 = fst \<nu>})"
definition coincide_hp' :: "hp \<Rightarrow> bool"
where "coincide_hp' \<alpha> \<longleftrightarrow> (\<forall> I J. is_interp I \<longrightarrow> is_interp J \<longrightarrow> (coincide_hp \<alpha> I J \<and> ode_sem_equiv \<alpha> I))"
definition coincide_fml :: "formula \<Rightarrow> bool"
where "coincide_fml \<phi> \<longleftrightarrow> (\<forall> \<nu> \<nu>' I J . is_interp I \<longrightarrow> is_interp J \<longrightarrow> Iagree I J (SIGF \<phi>) \<longrightarrow> Vagree \<nu> \<nu>' (FVF \<phi>) \<longrightarrow> \<nu> \<in> fml_sem I \<phi> \<longleftrightarrow> \<nu>' \<in> fml_sem J \<phi>)"
lemma coinc_fml [simp]: "coincide_fml \<phi> = (\<forall> \<nu> \<nu>' I J. is_interp I \<longrightarrow> is_interp J \<longrightarrow>Iagree I J (SIGF \<phi>) \<longrightarrow> Vagree \<nu> \<nu>' (FVF \<phi>) \<longrightarrow> \<nu> \<in> fml_sem I \<phi> \<longleftrightarrow> \<nu>' \<in> fml_sem J \<phi>)"
unfolding coincide_fml_def by auto
subsection \<open>Coincidence Theorems for Programs and Formulas\<close>
lemma coincidence_hp_fml:
fixes \<alpha>::hp
fixes \<phi>::formula
shows "(hpsafe \<alpha> \<longrightarrow> coincide_hp' \<alpha>) \<and> (fsafe \<phi> \<longrightarrow> coincide_fml \<phi>)"
proof (induction rule: hpsafe_fsafe.induct)
case (hpsafe_Pvar x)
thus "?case"
apply(unfold coincide_hp'_def | rule allI | rule conjI | rule impI)+
prefer 2 unfolding ode_sem_equiv_def subgoal by auto
unfolding coincide_hp_def apply(auto)
subgoal for I J a b aa ba ab bb V
proof -
assume IA:"Iagree I J {Inr (Inr x)}"
have Peq:"\<And>y. y \<in> Programs I x \<longleftrightarrow> y \<in> Programs J x" using Iagree_Prog[OF IA] by auto
assume agree:"Vagree (a, b) (aa, ba) V"
and sub:"UNIV \<subseteq> V"
and sem:"((a, b), ab, bb) \<in> Programs I x"
from agree_UNIV_eq[OF agree_sub [OF sub agree]]
have eq:"(a,b) = (aa,ba)" by auto
hence sem':"((aa,ba), (ab,bb)) \<in> Programs I x"
using sem by auto
have triv_sub:"V \<subseteq> UNIV" by auto
have VA:"Vagree (ab,bb) (ab,bb) V" using agree_sub[OF triv_sub agree_refl[of "(ab,bb)"]] eq
by auto
show "\<exists>a b. ((aa, ba), a, b) \<in> Programs J x \<and> Vagree (ab, bb) (a, b) V"
apply(rule exI[where x="ab"])
apply(rule exI[where x="bb"])
using sem eq VA by (auto simp add: Peq)
qed
done
next
case (hpsafe_Assign e x) then
show "?case"
proof (auto simp only: coincide_hp'_def ode_sem_equiv_def coincide_hp_def)
fix I J :: "interp"
and \<nu>1 \<nu>2 \<nu>'1 \<nu>'2 \<mu>1 \<mu>2 V
assume safe:"dsafe e"
and IA:"Iagree I J (SIGP (x := e))"
and VA:"Vagree (\<nu>1, \<nu>2) (\<nu>'1, \<nu>'2) V"
and sub:"FVP (x := e) \<subseteq> V"
and sem:"((\<nu>1, \<nu>2), (\<mu>1, \<mu>2)) \<in> prog_sem I (x := e)"
from VA have VA':"Vagree (\<nu>1, \<nu>2) (\<nu>'1, \<nu>'2) (FVT e)" unfolding FVP.simps Vagree_def using sub by auto
have Ssub:"{Inl x | x. x \<in> SIGT e} \<subseteq> (SIGP (x := e))" by auto
from IA have IA':"Iagree I J {Inl x | x. x \<in> SIGT e}" using Ssub unfolding SIGP.simps by auto
have "((\<nu>1, \<nu>2), repv (\<nu>1, \<nu>2) x (dterm_sem I e (\<nu>1, \<nu>2))) \<in> prog_sem I (x := e)" by auto
then have sem':"((\<nu>'1, \<nu>'2), repv (\<nu>'1, \<nu>'2) x (dterm_sem J e (\<nu>'1, \<nu>'2))) \<in> prog_sem J (x := e)"
using coincidence_dterm' safe VA' IA' by auto
from sem have eq:"(\<mu>1, \<mu>2) = (repv (\<nu>1, \<nu>2) x (dterm_sem I e (\<nu>1, \<nu>2)))" by auto
have VA'':"Vagree (\<mu>1, \<mu>2) (repv (\<nu>'1, \<nu>'2) x (dterm_sem J e (\<nu>'1, \<nu>'2))) (MBV (x := e) \<union> V)"
using coincidence_dterm'[of e "(\<nu>1,\<nu>2)" "(\<nu>'1,\<nu>'2)" I J] safe VA' IA' eq agree_refl VA unfolding MBV.simps Vagree_def
by auto
show "\<exists>\<mu>'. ((\<nu>'1, \<nu>'2), \<mu>') \<in> prog_sem J (x := e) \<and> Vagree (\<mu>1, \<mu>2) \<mu>' (MBV (x := e) \<union> V)"
using VA'' sem' by blast
qed
next
case (hpsafe_AssignAny x) then
show "?case"
proof (auto simp only: coincide_hp'_def ode_sem_equiv_def coincide_hp_def)
fix I J :: "interp"
and \<nu>1 \<nu>2 \<nu>'1 \<nu>'2 \<mu>1 \<mu>2 V
assume IA:"Iagree I J (SIGP (AssignAny x))"
and VA:"Vagree (\<nu>1, \<nu>2) (\<nu>'1, \<nu>'2) V"
and sub:"FVP (AssignAny x) \<subseteq> V"
and sem:"((\<nu>1, \<nu>2), (\<mu>1, \<mu>2)) \<in> prog_sem I (AssignAny x)"
show "\<exists>\<mu>'. ((\<nu>'1, \<nu>'2), \<mu>') \<in> prog_sem J (AssignAny x) \<and> Vagree (\<mu>1, \<mu>2) \<mu>' (MBV (AssignAny x) \<union> V)"
using IA VA sub sem apply auto subgoal for r
apply(rule exI[where x="fst (repv (\<nu>'1,\<nu>'2) x r)"])
apply(rule conjI)
subgoal apply(rule exI[where x=r])
apply(rule vec_extensionality)
using VA sub sem by(auto simp add: vec_eq_iff Vagree_def)
subgoal using VA sub sem by(auto simp add: vec_eq_iff Vagree_def) done done
qed
next
case (hpsafe_DiffAssign e x) then show "?case"
proof (auto simp only: coincide_hp'_def ode_sem_equiv_def coincide_hp_def)
fix I J::"interp"
and \<nu> \<nu>' \<mu> V
assume safe:"dsafe e"
and IA:"Iagree I J (SIGP (DiffAssign x e))"
and VA:"Vagree \<nu> \<nu>' V"
and sub:"FVP (DiffAssign x e) \<subseteq> V"
and sem:"(\<nu>, \<mu>) \<in> prog_sem I (DiffAssign x e)"
from VA have VA':"Vagree \<nu> \<nu>' (FVT e)" unfolding FVP.simps Vagree_def using sub by auto
have Ssub:"{Inl x | x. x \<in> SIGT e} \<subseteq> (SIGP (DiffAssign x e))" by auto
from IA have IA':"Iagree I J {Inl x | x. x \<in> SIGT e}" using Ssub unfolding SIGP.simps by auto
have "(\<nu>, repv \<nu> x (dterm_sem I e \<nu>)) \<in> prog_sem I (x := e)" by auto
then have sem':"(\<nu>', repd \<nu>' x (dterm_sem J e \<nu>')) \<in> prog_sem J (DiffAssign x e)"
using coincidence_dterm' safe VA' IA' by auto
from sem have eq:"\<mu> = (repd \<nu> x (dterm_sem I e \<nu>))" by auto
have VA':"Vagree \<mu> (repd \<nu>' x (dterm_sem J e \<nu>')) (MBV (DiffAssign x e) \<union> V)"
using coincidence_dterm'[OF safe VA', of I J, OF IA'] eq agree_refl VA unfolding MBV.simps Vagree_def
by auto
show "\<exists>\<mu>'. (\<nu>', \<mu>') \<in> prog_sem J (DiffAssign x e) \<and> Vagree \<mu> \<mu>' (MBV (DiffAssign x e) \<union> V)"
using VA' sem' by blast
qed
next
case (hpsafe_Test P) then
show "?case"
proof (auto simp add:coincide_hp'_def ode_sem_equiv_def coincide_hp_def)
fix I J::"interp" and \<nu> \<nu>' \<omega> \<omega>' ::"simple_state"
and V
assume safe:"fsafe P"
assume goodI:"is_interp I"
assume goodJ:"is_interp J"
assume "\<forall>a b aa ba I.
is_interp I \<longrightarrow>
(\<forall>J. is_interp J \<longrightarrow> Iagree I J (SIGF P) \<longrightarrow> Vagree (a, b) (aa, ba) (FVF P) \<longrightarrow> ((a, b) \<in> fml_sem I P) = ((aa, ba) \<in> fml_sem J P))"
hence IH:"Iagree I J (SIGF P) \<Longrightarrow> Vagree (\<nu>, \<nu>') (\<omega>, \<omega>') (FVF P) \<Longrightarrow> ((\<nu>, \<nu>') \<in> fml_sem I P) = ((\<omega>, \<omega>') \<in> fml_sem J P)"
using goodI goodJ by auto
assume IA:"Iagree I J (SIGF P)"
assume VA:"Vagree (\<nu>, \<nu>') (\<omega>, \<omega>') V"
assume sub:"FVF P \<subseteq> V"
hence VA':"Vagree (\<nu>, \<nu>') (\<omega>, \<omega>') (FVF P)" using agree_supset VA by auto
assume sem:"(\<nu>, \<nu>') \<in> fml_sem I P"
show "(\<omega>, \<omega>') \<in> fml_sem J P" using IH[OF IA VA'] sem by auto
qed
next
case (hpsafe_Evolve ODE P) then show "?case"
proof (unfold coincide_hp'_def)
assume osafe:"osafe ODE"
assume fsafe:"fsafe P"
assume IH:"coincide_fml P"
from IH have IHF:"\<And>\<nu> \<nu>' I J. Iagree I J (SIGF P) \<Longrightarrow> is_interp I \<Longrightarrow> is_interp J \<Longrightarrow> Vagree \<nu> \<nu>' (FVF P) \<Longrightarrow> (\<nu> \<in> fml_sem I P) = (\<nu>' \<in> fml_sem J P)"
unfolding coincide_fml_def by auto
have equiv:"\<And>I. is_interp I \<Longrightarrow> ode_sem_equiv (EvolveODE ODE P) I"
subgoal for I
apply(unfold ode_sem_equiv_def)
apply(rule allI)+
subgoal for ODE \<phi>
apply(rule impI)+
apply(auto) (* 2 subgoals *)
subgoal for aa ba ab bb sol t
apply(rule exI[where x="(\<lambda>t. \<chi> i. if i \<in> FVO ODE then sol t $ i else ab $ i)"])
apply(rule conjI)
subgoal using mk_v_agree[of I ODE "(ab,bb)" "sol t"] mk_v_agree[of I ODE "(ab,bb)" "(\<chi> i. if i \<in> FVO ODE then sol t $ i else ab $ i)"]
unfolding Vagree_def VSagree_def by (auto simp add: vec_eq_iff)
apply(rule exI[where x=t])
apply(rule conjI) (* 2 subgoals*)
subgoal
apply(rule agree_UNIV_eq)
using mk_v_agree[of I ODE "(ab,bb)" "sol t"]
mk_v_agree[of I ODE "(ab,bb)" "(\<chi> i. if i \<in> FVO ODE then sol t $ i else ab $ i)"]
mk_v_agree[of I ODE "(\<chi> i. if i \<in> FVO ODE then sol 0 $ i else ab $ i, bb)" "(\<chi> i. if i \<in> FVO ODE then sol t $ i else ab $ i)"]
unfolding Vagree_def VSagree_def
apply(auto) (* 2 subgoals *)
subgoal for i
apply(cases "Inl i \<in> BVO ODE")
subgoal
using bvo_to_fvo[of i ODE]
by (metis (no_types, lifting) image_eqI)
using bvo_to_fvo[of i ODE]
by (smt Inl_Inr_False Inl_inject image_iff ode_to_fvo)
using bvo_to_fvo[where ODE=ODE]
proof -
fix ia :: ident
assume good_interp:"is_interp I"
assume a1: "osafe ODE"
assume a2: "(aa, ba) = mk_v I ODE (ab, bb) (sol t)"
assume a3: "\<forall>i. (Inr i \<in> Inl ` ODE_vars I ODE \<longrightarrow> snd (mk_v I ODE (\<chi> i. if i \<in> FVO ODE then sol 0 $ i else ab $ i, bb) (\<chi> i. if i \<in> FVO ODE then sol t $ i else ab $ i)) $ i = ODE_sem I ODE (\<chi> i. if i \<in> FVO ODE then sol t $ i else ab $ i) $ i) \<and> ((Inr i::ident + ident) \<in> Inr ` ODE_vars I ODE \<longrightarrow> snd (mk_v I ODE (\<chi> i. if i \<in> FVO ODE then sol 0 $ i else ab $ i, bb) (\<chi> i. if i \<in> FVO ODE then sol t $ i else ab $ i)) $ i = ODE_sem I ODE (\<chi> i. if i \<in> FVO ODE then sol t $ i else ab $ i) $ i)"
assume a4: "\<forall>i. (Inr i \<in> Inl ` ODE_vars I ODE \<longrightarrow> snd (mk_v I ODE (ab, bb) (sol t)) $ i = ODE_sem I ODE (sol t) $ i) \<and> ((Inr i::ident + ident) \<in> Inr ` ODE_vars I ODE \<longrightarrow> snd (mk_v I ODE (ab, bb) (sol t)) $ i = ODE_sem I ODE (sol t) $ i)"
assume a5: "\<forall>i. Inr i \<notin> Inl ` ODE_vars I ODE \<and> (Inr i::ident + ident) \<notin> Inr ` ODE_vars I ODE \<longrightarrow> snd (mk_v I ODE (\<chi> i. if i \<in> FVO ODE then sol 0 $ i else ab $ i, bb) (\<chi> i. if i \<in> FVO ODE then sol t $ i else ab $ i)) $ i = bb $ i"
assume a6: "\<forall>i. Inr i \<notin> Inl ` ODE_vars I ODE \<and> (Inr i::ident + ident) \<notin> Inr ` ODE_vars I ODE \<longrightarrow> snd (mk_v I ODE (ab, bb) (sol t)) $ i = bb $ i"
have f7: "\<And>f r v. ODE_sem I ODE (\<chi> i. if i \<in> FVO ODE then f (r::real) $ i else v $ i) = ODE_sem I ODE (f r)"
(* using a1 good_interp alt_sem_lemma*)
subgoal for f r v
by (rule HOL.sym[OF alt_sem_lemma[OF a1 good_interp, of f r v]] )
done
{ assume "Inr ia \<notin> Inl ` ODE_vars I ODE"
{ assume "(Inr ia::(ident + ident)) \<notin> Inr ` ODE_vars I ODE \<and> Inr ia \<notin> Inl ` ODE_vars I ODE \<and> (Inr ia::(ident + ident)) \<notin> Inr ` ODE_vars I ODE \<and> Inr ia \<notin> Inl ` ODE_vars I ODE"
then have "snd (aa, ba) $ ia = bb $ ia \<and> (Inr ia::ident + ident) \<notin> Inr ` ODE_vars I ODE \<and> Inr ia \<notin> Inl ` ODE_vars I ODE"
using a6 a2 by presburger
then have "snd (mk_v I ODE (\<chi> c. if c \<in> FVO ODE then sol 0 $ c else ab $ c, bb) (\<chi> c. if c \<in> FVO ODE then sol t $ c else ab $ c)) $ ia = snd (aa, ba) $ ia"
using a5 by presburger }
then have "snd (mk_v I ODE (\<chi> c. if c \<in> FVO ODE then sol 0 $ c else ab $ c, bb) (\<chi> c. if c \<in> FVO ODE then sol t $ c else ab $ c)) $ ia = snd (aa, ba) $ ia"
using f7 a4 a3 a2 by force }
then show "snd (mk_v I ODE (ab, bb) (sol t)) $ ia = snd (mk_v I ODE (\<chi> c. if c \<in> FVO ODE then sol 0 $ c else ab $ c, bb) (\<chi> c. if c \<in> FVO ODE then sol t $ c else ab $ c)) $ ia"
using a2 by fastforce
qed
apply(rule conjI)
subgoal by auto
apply(auto simp only: solves_ode_def has_vderiv_on_def has_vector_derivative_def)
apply (rule has_derivative_vec[THEN has_derivative_eq_rhs])
defer
apply (rule ext)
apply (subst scaleR_vec_def)
apply (rule refl)
subgoal for x unfolding VSagree_def apply auto
proof -
assume osafe:"osafe ODE"
and fsafe:"fsafe \<phi>"
and eqP:"P = \<phi>"
and aaba: "(aa, ba) = mk_v I ODE (ab, bb) (sol t)"
and all:"\<forall>i. \<^cancel>\<open>(Inl i \<in> BVO ODE \<longrightarrow> sol 0 $ i = ab $ i) \<and>\<close> (Inl i \<in> Inl ` FVO ODE \<longrightarrow> sol 0 $ i = ab $ i) \<and> (Inl i \<in> FVF \<phi> \<longrightarrow> sol 0 $ i = ab $ i)"
and allSol:"\<forall>x\<in>{0..t}. (sol has_derivative (\<lambda>xa. xa *\<^sub>R ODE_sem I ODE (sol x))) (at x within {0..t})"
and mkV:"sol \<in> {0..t} \<rightarrow> {x. mk_v I ODE (ab, bb) x \<in> fml_sem I \<phi>}"
and x:"0 \<le> x"
and t:"x \<le> t"
and good_interp:"is_interp I"
from all have allT:"\<And>s. s \<ge> 0 \<Longrightarrow> s \<le> t \<Longrightarrow> mk_v I ODE (ab,bb) (sol s) \<in> fml_sem I \<phi>"
using mkV by auto
have VA:"\<And>x. Vagree (mk_v I ODE (ab, bb) (sol x)) (mk_v I ODE (ab, bb) (\<chi> i. if i \<in> FVO ODE then sol x $ i else ab $ i))
(FVF \<phi>)"
unfolding Vagree_def
apply(auto) (* 2 subgoals *)
subgoal for xa i
using mk_v_agree[of I ODE "(ab,bb)" "sol xa"]
mk_v_agree[of I ODE "(ab,bb)" "(\<chi> i. if i \<in> FVO ODE then sol xa $ i else ab $ i)"]
apply(cases "i \<in> ODE_vars I ODE")
using ode_to_fvo [of i I ODE] unfolding Vagree_def
apply auto
by fastforce
subgoal for xa i
using mk_v_agree[of I ODE "(ab,bb)" "sol xa"]
mk_v_agree[of I ODE "(ab,bb)" "(\<chi> i. if i \<in> FVO ODE then sol xa $ i else ab $ i)"]
ODE_vars_lr
using ode_to_fvo[of i I ODE] unfolding Vagree_def apply auto
using alt_sem_lemma osafe
subgoal
proof -
assume a1: "\<forall>i. Inr i \<notin> Inl ` ODE_vars I ODE \<and> (Inr i::ident + ident) \<notin> Inr ` ODE_vars I ODE \<longrightarrow> snd (mk_v I ODE (ab, bb) (sol xa)) $ i = bb $ i"
assume a2: "\<forall>i. Inr i \<notin> Inl ` ODE_vars I ODE \<and> (Inr i::ident + ident) \<notin> Inr ` ODE_vars I ODE \<longrightarrow> snd (mk_v I ODE (ab, bb) (\<chi> i. if i \<in> FVO ODE then sol xa $ i else ab $ i)) $ i = bb $ i"
assume a3: "\<forall>i. (Inr i \<in> Inl ` ODE_vars I ODE \<longrightarrow> snd (mk_v I ODE (ab, bb) (sol xa)) $ i = ODE_sem I ODE (sol xa) $ i) \<and> ((Inr i::ident + ident) \<in> Inr ` ODE_vars I ODE \<longrightarrow> snd (mk_v I ODE (ab, bb) (sol xa)) $ i = ODE_sem I ODE (sol xa) $ i)"
assume a4: "\<forall>i. (Inr i \<in> Inl ` ODE_vars I ODE \<longrightarrow> snd (mk_v I ODE (ab, bb) (\<chi> i. if i \<in> FVO ODE then sol xa $ i else ab $ i)) $ i = ODE_sem I ODE (\<chi> i. if i \<in> FVO ODE then sol xa $ i else ab $ i) $ i) \<and> ((Inr i::ident + ident) \<in> Inr ` ODE_vars I ODE \<longrightarrow> snd (mk_v I ODE (ab, bb) (\<chi> i. if i \<in> FVO ODE then sol xa $ i else ab $ i)) $ i = ODE_sem I ODE (\<chi> i. if i \<in> FVO ODE then sol xa $ i else ab $ i) $ i)"
have "ODE_sem I ODE (\<chi> c. if c \<in> FVO ODE then sol xa $ c else ab $ c) $ i = ODE_sem I ODE (sol xa) $ i"
using good_interp
by (metis (no_types) alt_sem_lemma osafe)
then have "Inr i \<notin> Inl ` ODE_vars I ODE \<and> (Inr i::ident + ident) \<notin> Inr ` ODE_vars I ODE \<or> snd (mk_v I ODE (ab, bb) (sol xa)) $ i = snd (mk_v I ODE (ab, bb) (\<chi> c. if c \<in> FVO ODE then sol xa $ c else ab $ c)) $ i"
using a4 a3 by fastforce
then show ?thesis
using a2 a1 by presburger
qed
done
done
note sem = IHF[OF Iagree_refl[of I]]
have VA1:"(\<forall>i. Inl i \<in> FVF \<phi> \<longrightarrow>
fst (mk_v I ODE ((\<chi> i. if i \<in> FVO ODE then sol 0 $ i else ab $ i), bb) (\<chi> i. if i \<in> FVO ODE then sol x $ i else ab $ i)) $ i
= fst (mk_v I ODE (ab, bb) (sol x)) $ i)"
and VA2: "(\<forall>i. Inr i \<in> FVF \<phi> \<longrightarrow>
snd (mk_v I ODE ((\<chi> i. if i \<in> FVO ODE then sol 0 $ i else ab $ i), bb) (\<chi> i. if i \<in> FVO ODE then sol x $ i else ab $ i)) $ i
= snd (mk_v I ODE (ab, bb) (sol x)) $ i)"
apply(auto) (* 2 subgoals *)
subgoal for i
using mk_v_agree[of I ODE "((\<chi> i. if i \<in> FVO ODE then sol 0 $ i else ab $ i),bb)" "(\<chi> i. if i \<in> FVO ODE then sol x $ i else ab $ i)"]
using mk_v_agree[of I ODE "(ab,bb)" "(sol x)"] ODE_vars_lr[of i I ODE]
unfolding Vagree_def apply (auto)
apply(erule allE[where x=i])+
apply(cases " i \<in> FVO ODE")
apply(auto)
apply(cases " i \<in> FVO ODE") (* 18 subgoals *)
apply(auto)
using ODE_vars_lr[of i I ODE] ode_to_fvo[of i I ODE]
apply auto
using all by meson
subgoal for i
using mk_v_agree[of I ODE "((\<chi> i. if i \<in> FVO ODE then sol 0 $ i else ab $ i),bb)" "(\<chi> i. if i \<in> FVO ODE then sol x $ i else ab $ i)"]
using mk_v_agree[of I ODE "(ab,bb)" "(sol x)"] ODE_vars_lr[of i I ODE]
unfolding Vagree_def apply (auto)
apply(erule allE[where x=i])+
apply(cases " i \<in> FVO ODE")
apply(auto) (* 32 subgoals *)
apply(cases " i \<in> FVO ODE")
apply(auto)
using ODE_vars_lr[of i I ODE] ode_to_fvo[of i I ODE]
apply(auto)
using alt_sem_lemma osafe
by (metis (no_types) alt_sem_lemma good_interp osafe)+
done
assume good:"is_interp I"
show "mk_v I ODE (\<chi> i. if i \<in> FVO ODE then sol 0 $ i else ab $ i, bb)
(\<chi> i. if i \<in> FVO ODE then sol x $ i else ab $ i) \<in> fml_sem I \<phi>"
using mk_v_agree[of I ODE "(\<chi> i. if i \<in> FVO ODE then sol 0 $ i else ab $ i, bb)"
"(\<chi> i. if i \<in> FVO ODE then sol x $ i else ab $ i)"]
mk_v_agree[of I ODE "(ab, bb)" "sol x"]
using sem[of "mk_v I ODE (\<chi> i. if i \<in> FVO ODE then sol 0 $ i else ab $ i, bb) (\<chi> i. if i \<in> FVO ODE then sol x $ i else ab $ i)"
"mk_v I ODE (ab, bb) (sol x)"]
VA1 VA2
allT[of x] allT[of 0]
unfolding Vagree_def
apply auto
using atLeastAtMost_iff mem_Collect_eq mkV t x
apply(auto)
using eqP VA sem good
by auto
qed
proof -
fix x i
assume
assms:"osafe ODE"
"fsafe \<phi>"
"0 \<le> t"
"(aa, ba) = mk_v I ODE (ab, bb) (sol t)"
"VSagree (sol 0) ab {x. \<^cancel>\<open>Inl x \<in> BVO ODE \<or> \<close>Inl x \<in> Inl ` FVO ODE \<or> Inl x \<in> FVF \<phi>}"
and deriv:"\<forall>x\<in>{0..t}. (sol has_derivative (\<lambda>xa. xa *\<^sub>R ODE_sem I ODE (sol x))) (at x within {0..t})"
and sol:"sol \<in> {0..t} \<rightarrow> {x. mk_v I ODE (ab, bb) x \<in> fml_sem I \<phi>}"
and mem:"x \<in> {0..t}"
and good_interp:"is_interp I"
from deriv
have xDeriv:"(sol has_derivative (\<lambda>xa. xa *\<^sub>R ODE_sem I ODE (sol x))) (at x within {0..t})"
using mem by blast
have silly1:"(\<lambda>x. \<chi> i. sol x $ i) = sol"
by (auto simp add: vec_eq_iff)
have silly2:"(\<lambda>h. \<chi> i. h * ODE_sem I ODE (sol x) $ i) = (\<lambda>xa. xa *\<^sub>R ODE_sem I ODE (sol x))"
by (auto simp add: vec_eq_iff)
from xDeriv have
xDeriv':"((\<lambda>x. \<chi> i. sol x $ i) has_derivative (\<lambda>h. \<chi> i. h * ODE_sem I ODE (sol x) $ i)) (at x within {0..t})"
using silly1 silly2 apply auto done
from xDeriv have xDerivs:"\<And>j. ((\<lambda>t. sol t $ j) has_derivative (\<lambda>xa. (xa *\<^sub>R ODE_sem I ODE (sol x)) $ j)) (at x within {0..t})"
subgoal for j
using silly1 silly2 has_derivative_proj[of "(\<lambda>i. \<lambda>t. sol t $ i)" "(\<lambda> i. \<lambda>xa. (xa *\<^sub>R ODE_sem I ODE (sol x)) $ i)" "(at x within {0..t})" j]
apply auto
done
done
have neato:"\<And>\<nu>. i \<notin> FVO ODE \<Longrightarrow> ODE_sem I ODE \<nu> $ i = 0"
proof (induction "ODE")
case (OVar x1 x2)
then show ?case by(cases x2,auto)
next
case (OSing x1 x2)
then show ?case by auto
next
case (OProd ODE1 ODE2)
then show ?case by auto
qed
show "((\<lambda>t. if i \<in> FVO ODE then sol t $ i else ab $ i) has_derivative
(\<lambda>h. h *\<^sub>R ODE_sem I ODE (\<chi> i. if i \<in> FVO ODE then sol x $ i else ab $ i) $ i))
(at x within {0..t})"
using assms sol mem
apply auto
apply (rule has_derivative_eq_rhs)
unfolding VSagree_def apply auto
apply(cases " i \<in> FVO ODE")
using xDerivs[of i] apply auto
using alt_sem_lemma neato[of "(\<chi> i. if i \<in> FVO ODE then sol x $ i else ab $ i)"] apply auto
proof -
assume a1: "((\<lambda>t. sol t $ i) has_derivative (\<lambda>xa. xa * ODE_sem I ODE (sol x) $ i)) (at x within {0..t})"
have "\<And> r. ODE_sem (I::interp) ODE (\<chi> c. if c \<in> FVO ODE then sol r $ c else ab $ c) = ODE_sem I ODE (sol r)"
by (metis (no_types) alt_sem_lemma good_interp assms(1))
then show "((\<lambda>r. sol r $ i) has_derivative (\<lambda>r. r * ODE_sem I ODE (\<chi> c. if c \<in> FVO ODE then sol x $ c else ab $ c) $ i)) (at x within {0..t})"
using a1 by presburger
qed
qed
proof -
fix aa ba bb sol t
assume osafe:"osafe ODE"
and fsafe:"fsafe \<phi>"
and t:"0 \<le> t"
and aaba:"(aa, ba) = mk_v I ODE (sol 0, bb) (sol t)"
and sol:"(sol solves_ode (\<lambda>a. ODE_sem I ODE)) {0..t} {x. mk_v I ODE (sol 0, bb) x \<in> fml_sem I \<phi>}"
show"\<exists>sola ta. mk_v I ODE (sol 0, bb) (sol t) = mk_v I ODE (sol 0, bb) (sola ta) \<and>
0 \<le> ta \<and>
(sola solves_ode (\<lambda>a. ODE_sem I ODE)) {0..ta} {x. mk_v I ODE (sol 0, bb) x \<in> fml_sem I \<phi>} \<and>
VSagree (sola 0) (sol 0) {x. Inl x \<in> Inl ` FVO ODE \<or> Inl x \<in> FVF \<phi>}"
apply(rule exI[where x=sol])
apply(rule exI[where x=t])
using fsafe t aaba sol apply auto
unfolding VSagree_def by auto
qed
done
done
show "\<forall>I J. is_interp I \<longrightarrow> is_interp J \<longrightarrow> coincide_hp (EvolveODE ODE P) I J \<and> ode_sem_equiv (EvolveODE ODE P) I"
proof (rule allI | rule impI)+
fix I J::"interp"
assume goodI:"is_interp I" assume goodJ:"is_interp J"
from equiv[of I]
have equivI:"
{(\<nu>, mk_v I ODE \<nu> (sol t)) | \<nu> sol t.
t \<ge> 0 \<and>
(sol solves_ode (\<lambda>_. ODE_sem I ODE)) {0..t} {x. mk_v I ODE \<nu> x \<in> fml_sem I P} \<and>
VSagree (sol 0) (fst \<nu>) {x | x. Inl x \<in> FVP (EvolveODE ODE P)}} =
{(\<nu>, mk_v I ODE \<nu> (sol t)) | \<nu> sol t.
t \<ge> 0 \<and>
(sol solves_ode (\<lambda>_. ODE_sem I ODE)) {0..t} {x. mk_v I ODE \<nu> x \<in> fml_sem I P} \<and>
(sol 0) = (fst \<nu>)}"
unfolding ode_sem_equiv_def using osafe fsafe goodI goodJ by blast
from equiv[of J]
have equivJ:"
{(\<nu>, mk_v J ODE \<nu> (sol t)) | \<nu> sol t.
t \<ge> 0 \<and>
(sol solves_ode (\<lambda>_. ODE_sem J ODE)) {0..t} {x. mk_v J ODE \<nu> x \<in> fml_sem J P} \<and>
VSagree (sol 0) (fst \<nu>) {x | x. Inl x \<in> FVP (EvolveODE ODE P)}} =
{(\<nu>, mk_v J ODE \<nu> (sol t)) | \<nu> sol t.
t \<ge> 0 \<and>