-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathDifferential_Axioms.thy
3529 lines (3442 loc) · 222 KB
/
Differential_Axioms.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 "Differential_Axioms"
imports
Ordinary_Differential_Equations.ODE_Analysis
"./Ids"
"./Finite_String"
"./Lib"
"./Syntax"
"./Denotational_Semantics"
"./Frechet_Correctness"
"./Axioms"
"./Coincidence"
begin
unbundle no_funcset_notation
section \<open>Differential Axioms\<close>
text \<open>Differential axioms fall into two categories:
Axioms for computing the derivatives of terms and axioms for proving properties of ODEs.
The derivative axioms are all corollaries of the frechet correctness theorem. The ODE
axioms are more involved, often requiring extensive use of the ODE libraries.\<close>
subsection \<open>Derivative Axioms\<close>
definition diff_const_axiom :: "formula"
where [axiom_defs]:"diff_const_axiom \<equiv> Equals (Differential ($f Ix empty)) \<^bold>0"
definition diff_var_axiom :: "formula"
where [axiom_defs]:"diff_var_axiom \<equiv> Equals (Differential (Syntax.Var Ix)) (DiffVar Ix)"
definition state_fun ::"ident \<Rightarrow> trm"
where [axiom_defs]:"state_fun f = ($f f (\<lambda>i. Syntax.Var i))"
definition diff_plus_axiom :: "formula"
where [axiom_defs]:"diff_plus_axiom \<equiv> Equals (Differential (Plus (state_fun Ix) (state_fun Iy)))
(Plus (Differential (state_fun Ix)) (Differential (state_fun Iy)))"
definition dMinusAxiom::"formula"
where [axiom_defs]:"dMinusAxiom \<equiv>
Equals
(Differential (Syntax.Minus (DFunl Ix) (DFunl Iy)))
(Syntax.Minus (Differential (DFunl Ix)) (Differential(DFunl Iy)))"
definition diff_times_axiom :: "formula"
where [axiom_defs]:"diff_times_axiom \<equiv> Equals (Differential (Times (state_fun Ix) (state_fun Iy)))
(Plus (Times (Differential (state_fun Ix)) (state_fun Iy))
(Times (state_fun Ix) (Differential (state_fun Iy))))"
(* [y=g(x)][y'=1](f(g(x))' = f(y)')*)
definition diff_chain_axiom::"formula"
where [axiom_defs]:"diff_chain_axiom \<equiv> [[Syntax.Assign Iy (f1 Iy Ix)]]([[DiffAssign Iy \<^bold>1]]
(Equals (Differential ($f Ix (singleton (f1 Iy Ix)))) (Times (Differential (f1 Ix Iy)) (Differential (f1 Iy Ix)))))"
subsection \<open>ODE Axioms\<close>
definition DWaxiom :: "formula"
(*
[{c_&q_(||)}]p_(||) <-> ([{c_&q_(||)}](q_(||)->p_(||)))*)
where [axiom_defs]:"DWaxiom = Equiv([[EvolveODE (OVar Ix None) (Pc Iy)]]Pc Ix) (([[EvolveODE (OVar Ix None) (Pc Iy)]](Pc Iy \<rightarrow> Pc Ix)))"
definition DWaxiom' :: "formula"
where [axiom_defs]:"DWaxiom' = ([[EvolveODE (OSing Ix (Function Ix (singleton (Syntax.Var Ix)))) (Prop Iy (singleton (Syntax.Var Ix)))]](Prop Iy (singleton (Syntax.Var Ix))))"
(* ([{c&q(||)}]p(||) <-> [{c&(q(||)&r(||))}]p(||)) <- [{c&q(||)}]r(||)
[{c&q(||)}]r(||) \<rightarrow> ([{c&q(||)}]p(||) <-> [{c&(q(||)&r(||))}]p(||))
[1&2]3 \<rightarrow> ([1&2]1 <-> [1&(2&3)]1)
*)
definition DCaxiom :: "formula"
where [axiom_defs]:"DCaxiom = (
([[EvolveODE (OVar Ix None) (Pc Iy)]]Pc Iz) \<rightarrow>
(([[EvolveODE (OVar Ix None) (Pc Iy)]](Pc Ix))
\<leftrightarrow>
([[EvolveODE (OVar Ix None) (And (Pc Iy) (Pc Iz))]]Pc Ix)))"
definition DEaxiom :: "formula"
where [axiom_defs]:"DEaxiom =
(([[EvolveODE (OSing Ix (f1 Ix Ix)) (p1 Iy Ix)]] (P Ix))
\<leftrightarrow>
([[EvolveODE (OSing Ix (f1 Ix Ix)) (p1 Iy Ix)]]
[[DiffAssign Ix (f1 Ix Ix)]]P Ix))"
definition DSaxiom :: "formula"
where [axiom_defs]:"DSaxiom =
(([[EvolveODE (OSing Ix (f0 Ix)) (p1 Iy Ix)]]p1 Iz Ix)
\<leftrightarrow>
(Forall Iy
(Implies (Geq (Syntax.Var Iy) \<^bold>0)
(Implies
(Forall Iz
(Implies (And (Geq (Syntax.Var Iz) \<^bold>0) (Geq (Syntax.Var Iy) (Syntax.Var Iz)))
(Prop Iy (singleton (Plus (Syntax.Var Ix) (Times (f0 Ix) (Syntax.Var Iz)))))))
([[Syntax.Assign Ix (Plus (Syntax.Var Ix) (Times (f0 Ix) (Syntax.Var Iy)))]]p1 Iz Ix )))))"
(* TODO: Axiom + proof
[{x_'=f(||), c & q(||)}]p(||)
<-> [{c,x_'=f(||)&q(||)}][x_':=f(||);]p(||)
x_ = vid1
f\<lparr>\<rparr>= fid1
c = vid1
q\<lparr>\<rparr> = pid2
p\<lparr>\<rparr> = pid1
[{x_'=f(||),c&q(||)}]p(||) <-> [{c,x_'=f(||)&q(||)}][x_':=f(||);]p(||)
*)
(* TODO: fid1 \<rightarrow> fid2*)
definition DiffEffectSysAxiom::"formula"
where [axiom_defs]:"DiffEffectSysAxiom \<equiv>
([[EvolveODE (oprod (OSing Ix (DFunl Ix)) (OVar Ix (Some Ix))) (P Iy)]]P Ix)
\<leftrightarrow> ([[EvolveODE (oprod (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (P Iy)]]([[DiffAssign Ix (DFunl Ix)]]P Ix))"
lemma ODE_zero:"\<And>i. is_interp I \<Longrightarrow> Inl i \<notin> BVO ODE \<Longrightarrow> Inr i \<notin> BVO ODE \<Longrightarrow> ODE_sem I ODE \<nu> $ i= 0"
proof(induction ODE)
case (OVar x1 x2)
then show ?case apply(cases x2,auto)
proof -
assume Some:"x2 = Some i"
assume good:"is_interp I"
assume elem:"i \<in> ODEBV I x1 (Some i)"
have bv:"ODEBV I x1 (Some i) \<subseteq> - {i}" using good unfolding is_interp_def by auto
then show "ODEs I x1 (Some i) \<nu> $ i = 0"
using good elem unfolding is_interp_def using bv by(auto)
qed
next
case (OSing x1 x2)
then show ?case by auto
next
case (OProd ODE1 ODE2)
then show ?case by auto
qed
lemma ODE_unbound_zero:
fixes i
assumes good_interp:"is_interp I"
shows "i \<notin> ODE_vars I ODE \<Longrightarrow> ODE_sem I ODE x $ i = 0"
proof (induction ODE)
case (OVar x1 x2)
assume notin:"i \<notin> ODE_vars I (OVar x1 x2)"
have thing:"(\<And>ode x. ODEBV I ode (Some x) \<subseteq> - {x})" using good_interp unfolding is_interp_def by auto
show ?case
apply(cases x2)
subgoal using notin by auto
using thing[of "x1"] notin 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_bound_effect:
fixes s t sol ODE X b
assumes good_interp:"is_interp I"
assumes s:"s \<in> {0..t}"
assumes sol:"(sol solves_ode (\<lambda>_. ODE_sem I ODE)) {0..t} X"
shows "Vagree (sol 0,b) (sol s, b) (-(BVO ODE))"
proof -
have imp:"\<And>i. Inl i \<notin> BVO ODE \<Longrightarrow> i \<notin> ODE_vars I ODE"
subgoal for i
apply(induction ODE,auto)
subgoal for x1 x2
apply(cases x2,auto)
using good_interp unfolding is_interp_def by auto done done
have "\<And>i. Inl i \<notin> BVO ODE \<Longrightarrow> (\<forall> s. s \<in> {0..t} \<longrightarrow> sol s $ i = sol 0 $ i)"
apply auto
apply (rule constant_when_zero)
using s sol apply auto
using ODE_unbound_zero solves_ode_subset good_interp imp
by fastforce+
then show "Vagree (sol 0, b) (sol s, b) (- BVO ODE)"
unfolding Vagree_def
using s by (metis Compl_iff fst_conv snd_conv)
qed
lemma ODE_bound_effect_tight_left:
fixes s t sol ODE X b
assumes good_interp:"is_interp I"
assumes s:"s \<in> {0..t}"
assumes sol:"(sol solves_ode (\<lambda>_. ODE_sem I ODE)) {0..t} X"
shows "VSagree (sol 0) (sol s) (-(ODE_vars I ODE))"
proof -
have "\<And>i. i \<notin> ODE_vars I ODE \<Longrightarrow> (\<forall> s. s \<in> {0..t} \<longrightarrow> sol s $ i = sol 0 $ i)"
apply auto
apply (rule constant_when_zero)
using s sol apply auto
using ODE_unbound_zero solves_ode_subset good_interp
by fastforce+
then show "VSagree (sol 0) (sol s) (-(ODE_vars I ODE))"
apply(auto)
unfolding VSagree_def
using s Compl_iff fst_conv snd_conv
by (metis (full_types) atLeastAtMost_iff)
qed
lemma ODE_bound_effect_tight:
fixes s t sol ODE X b
assumes good_interp:"is_interp I"
assumes s:"s \<in> {0..t}"
assumes sol:"(sol solves_ode (\<lambda>_. ODE_sem I ODE)) {0..t} X"
shows "Vagree (sol 0,b) (sol s,b) (-(semBV I ODE))"
proof -
have "\<And>i. i \<notin> ODE_vars I ODE \<Longrightarrow> (\<forall> s. s \<in> {0..t} \<longrightarrow> sol s $ i = sol 0 $ i)"
apply auto
apply (rule constant_when_zero)
using s sol apply auto
using ODE_unbound_zero solves_ode_subset good_interp
by fastforce+
then show "Vagree (sol 0,b) (sol s,b) (-(semBV I ODE))"
using ODE_bound_effect_tight_left[OF good_interp s sol]
by(auto simp add: Vagree_def VSagree_def)
qed
theorem DiffEffectSys_valid:"valid DiffEffectSysAxiom"
proof (unfold DiffEffectSysAxiom_def, simp)
have invX:"Rep_ident (Abs_ident ''$x'') = ''$x''"
apply(rule Abs_ident_inverse)
by(auto simp add: max_str)
have invY:"Rep_ident (Abs_ident ''$y'') = ''$y''"
apply(rule Abs_ident_inverse)
by(auto simp add: max_str)
have dsafe:"dsafe ($f Ix (singleton (trm.Var Ix)))"
by(auto simp add: f1_def p1_def Ix_def ident_expose_def Abs_ident_inverse invX SSENT_def FSENT_def SSENTINEL_def FSENTINEL_def max_str ilength_def)
have osafe:"osafe(OSing Ix (f1 Ix Ix))"
by(auto simp add: f1_def p1_def Ix_def ident_expose_def Abs_ident_inverse invX SSENT_def FSENT_def SSENTINEL_def FSENTINEL_def max_str ilength_def)
have fsafe:"fsafe (p1 Iy Ix)"
by(auto simp add: p1_def Iy_def ident_expose_def Abs_ident_inverse invY SSENT_def FSENT_def SSENTINEL_def FSENTINEL_def)
have solves_ode_cong:"\<And> SOL ODE1 ODE2 T X1 X2.
ODE1 = ODE2 \<Longrightarrow> X1 = X2 \<Longrightarrow> (SOL solves_ode ODE1) T X1 \<Longrightarrow> (SOL solves_ode ODE2) T X2"
by(auto)
have comm_sem:"\<And>I. (\<lambda>_. ODE_sem I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))
= (\<lambda>_. ODE_sem I (OProd (OSing Ix (DFunl Ix)) (OVar Ix (Some Ix))))"
by(rule ext,auto)
have eq_mkv_weak:"\<And> I x y ODE1 ODE2.
(ODE_vars I ODE1) = UNIV \<Longrightarrow> (ODE_vars I ODE2) = UNIV \<Longrightarrow>
(ODE_sem I ODE1) = (ODE_sem I ODE2) \<Longrightarrow> mk_v I ODE1 x y = mk_v I ODE2 x y"
subgoal for I x y ODE1 ODE2
apply(rule agree_UNIV_eq)
using mk_v_agree[of I "ODE1" x y]
using mk_v_agree[of I "ODE2" x y]
by(auto simp add: Vagree_def) done
have eq_mkv:"\<And> I x y ODE1 ODE2.
(semBV I ODE1) = (semBV I ODE2) \<Longrightarrow>
(ODE_sem I ODE1) = (ODE_sem I ODE2) \<Longrightarrow> mk_v I ODE1 x y = mk_v I ODE2 x y"
subgoal for I x y ODE1 ODE2
apply(rule agree_UNIV_eq)
using mk_v_agree[of I "ODE1" x y]
using mk_v_agree[of I "ODE2" x y]
apply(auto simp add: Vagree_def)
subgoal for i
apply(erule allE[where x=i])+
apply(clarsimp)
by metis
subgoal for i
apply(erule allE[where x=i])+
apply(clarsimp)
by metis
done done
have obv:"\<And>I. is_interp I \<Longrightarrow> ODEBV I Ix (Some Ix) \<subseteq> -{Ix}"
unfolding is_interp_def by auto
have eq_mkv2:"\<And>I::interp. \<And>x y. is_interp I \<Longrightarrow>
mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) x y =
mk_v I (OProd (OSing Ix (DFunl Ix)) (OVar Ix (Some Ix))) x y"
proof -
fix I::"interp" and x y
assume good:"is_interp I"
show "mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) x y = mk_v I (OProd (OSing Ix (DFunl Ix)) (OVar Ix (Some Ix))) x y"
apply(rule eq_mkv)
by auto
qed
have comm_mkv:"\<And> I ab bb. is_interp I \<Longrightarrow> {x. mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) x \<in> fml_sem I (Pc Iy)}
= {x. mk_v I (OProd (OSing Ix (DFunl Ix)) (OVar Ix (Some Ix))) (ab, bb) x \<in> fml_sem I (Pc Iy)}"
subgoal for I x y using eq_mkv2[of I "(x,y)"] apply auto done done
show "valid (([[EvolveODE (OProd (OSing Ix (DFunl Ix)) (OVar Ix (Some Ix))) (P Iy)]] (P Ix)) \<leftrightarrow>
([[EvolveODE ((OProd (OVar Ix (Some Ix))(OSing Ix (DFunl Ix)))) (P Iy)]]
[[DiffAssign Ix (DFunl Ix)]]P Ix))"
apply(auto simp only: DEaxiom_def valid_def Let_def iff_sem impl_sem)
apply(auto simp only: fml_sem.simps prog_sem.simps mem_Collect_eq box_sem f1_def p1_def P_def expand_singleton)
proof -
fix I ::"interp"
and aa ba ab bb sol
and t::real
and ac bc
assume good:"is_interp I"
assume bigNone:"
\<forall>\<omega>. (\<exists>\<nu> sol t. ((ab, bb), \<omega>) = (\<nu>, mk_v I (OProd (OSing Ix (DFunl Ix)) (OVar Ix (Some Ix))) \<nu> (sol t)) \<and>
0 \<le> t \<and>
(sol solves_ode (\<lambda>_. ODE_sem I (OProd (OSing Ix (DFunl Ix)) (OVar Ix (Some Ix))))) {0..t}
{x. mk_v I (OProd (OSing Ix (DFunl Ix)) (OVar Ix (Some Ix))) \<nu> x \<in> fml_sem I (Pc Iy)} \<and>
sol 0 = fst \<nu>) \<longrightarrow>
\<omega> \<in> fml_sem I (Pc Ix)"
let ?my\<omega> = "mk_v I (OProd (OSing Ix (DFunl Ix)) (OVar Ix (Some Ix))) (ab,bb) (sol t)"
assume t:"0 \<le> t"
assume aaba:"(aa, ba) = mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)"
assume sol:"(sol solves_ode (\<lambda>_. ODE_sem I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))) {0..t}
{x. mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) x \<in> fml_sem I (Pc Iy)}"
assume sol0:"sol 0 = fst (ab, bb)"
assume acbc:"
(ac, bc) =
repd (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) Ix
(dterm_sem I (DFunl Ix) (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)))"
have bigEx:"(\<exists>\<nu> sol t. ((ab, bb), ?my\<omega>) = (\<nu>, mk_v I (OProd (OSing Ix (DFunl Ix)) (OVar Ix (Some Ix))) \<nu> (sol t)) \<and>
0 \<le> t \<and>
(sol solves_ode (\<lambda>_. ODE_sem I (OProd (OSing Ix (DFunl Ix)) (OVar Ix (Some Ix))))) {0..t}
{x. mk_v I (OProd (OSing Ix (DFunl Ix)) (OVar Ix (Some Ix))) \<nu> x \<in> fml_sem I (Pc Iy)} \<and>
sol 0 = fst \<nu>)"
apply(rule exI[where x="(ab, bb)"])
apply(rule exI[where x="sol"])
apply(rule exI[where x="t"])
apply(rule conjI)
apply(rule refl)
apply(rule conjI)
apply(rule t)
apply(rule conjI)
apply(rule solves_ode_cong[where ?ODE1.0="(\<lambda>_. ODE_sem I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix)) ))" ,
where ?X1.0="{x. mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) x \<in> fml_sem I (Pc Iy)}"])
subgoal apply auto by(rule ext,rule ext, rule vec_extensionality,auto)
subgoal using comm_mkv[OF good] by auto
apply(rule sol)
by (rule sol0)
have bigRes:"?my\<omega> \<in> fml_sem I (Pc Ix)" using bigNone bigEx by blast
have notin1:"Inl Ix \<notin> BVO (OVar Ix (Some Ix))" using obv by auto
have notin2:"Inr Ix \<notin> BVO (OVar Ix (Some Ix))" using obv by auto
(* todo: change, not quite true *)
have ODE_sem:"ODE_sem I (OVar Ix (Some Ix)) (sol t) $ Ix = 0"
using ODE_zero notin1 notin2 good
by blast
have tset:"t \<in> {0..t}" using t by auto
have sol_mkv_eq:"(sol t) = fst (mk_v I (OProd (OSing Ix (DFunl Ix)) (OVar Ix (Some Ix))) (ab, bb) (sol t))"
using mk_v_agree[of "I" "(OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix)))" "(ab, bb)" "(sol t)"]
using sol0 good obv DFunl_def eq_mkv2 good ODE_bound_effect_tight[OF good tset sol]
apply(simp add: Vagree_def)
apply(erule conjE)+
apply(erule allE[where x="Ix"])+
apply(cases "Ix \<in> ODEBV I Ix (Some Ix)")
using sol0 apply(auto simp add: DFunl_def ODE_sem sol0)
using good obv apply auto
(* TODO: stuff about if derivative is zero then value is constant*)
apply(rule vec_extensionality)
using sol0 good obv DFunl_def eq_mkv2 good ODE_bound_effect_tight[OF good tset sol]
unfolding Vagree_def apply auto
apply (smt Compl_iff DFunl_def Vagree_def \<open>Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (ab, bb) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix)))) \<and> Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (mk_xode I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (sol t)) (semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> \<open>\<And>b. Vagree (sol 0, b) (sol t, b) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> fst_conv mk_xode.simps)
apply(rule vec_extensionality)
using sol0 good obv DFunl_def eq_mkv2 good ODE_bound_effect_tight[OF good tset sol] unfolding Vagree_def
apply (smt Compl_iff DFunl_def Vagree_def \<open>Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (ab, bb) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix)))) \<and> Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (mk_xode I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (sol t)) (semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> \<open>\<And>b. Vagree (sol 0, b) (sol t, b) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> fst_conv mk_xode.simps)
apply(rule vec_extensionality)
using sol0 good obv DFunl_def eq_mkv2 good ODE_bound_effect_tight[OF good tset sol] unfolding Vagree_def
apply (smt Compl_iff DFunl_def Vagree_def \<open>Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (ab, bb) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix)))) \<and> Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (mk_xode I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (sol t)) (semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> \<open>\<And>b. Vagree (sol 0, b) (sol t, b) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> fst_conv mk_xode.simps)
apply(rule vec_extensionality)
using sol0 good obv DFunl_def eq_mkv2 good ODE_bound_effect_tight[OF good tset sol] unfolding Vagree_def
apply (smt Compl_iff DFunl_def Vagree_def \<open>Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (ab, bb) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix)))) \<and> Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (mk_xode I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (sol t)) (semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> \<open>\<And>b. Vagree (sol 0, b) (sol t, b) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> fst_conv mk_xode.simps)
apply(rule vec_extensionality)
using sol0 good obv DFunl_def eq_mkv2 good ODE_bound_effect_tight[OF good tset sol] unfolding Vagree_def
apply (smt Compl_iff DFunl_def Vagree_def \<open>Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (ab, bb) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix)))) \<and> Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (mk_xode I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (sol t)) (semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> \<open>\<And>b. Vagree (sol 0, b) (sol t, b) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> fst_conv mk_xode.simps)
apply(rule vec_extensionality)
using sol0 good obv DFunl_def eq_mkv2 good ODE_bound_effect_tight[OF good tset sol] unfolding Vagree_def
apply (smt Compl_iff DFunl_def Vagree_def \<open>Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (ab, bb) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix)))) \<and> Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (mk_xode I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (sol t)) (semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> \<open>\<And>b. Vagree (sol 0, b) (sol t, b) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> fst_conv mk_xode.simps)
apply(rule vec_extensionality)
using sol0 good obv DFunl_def eq_mkv2 good ODE_bound_effect_tight[OF good tset sol] unfolding Vagree_def
apply (smt Compl_iff DFunl_def Vagree_def \<open>Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (ab, bb) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix)))) \<and> Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (mk_xode I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (sol t)) (semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> \<open>\<And>b. Vagree (sol 0, b) (sol t, b) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> fst_conv mk_xode.simps)
apply(rule vec_extensionality)
using sol0 good obv DFunl_def eq_mkv2 good ODE_bound_effect_tight[OF good tset sol] unfolding Vagree_def
apply (smt Compl_iff DFunl_def Vagree_def \<open>Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (ab, bb) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix)))) \<and> Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (mk_xode I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (sol t)) (semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> \<open>\<And>b. Vagree (sol 0, b) (sol t, b) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> fst_conv mk_xode.simps)
apply(rule vec_extensionality)
using sol0 good obv DFunl_def eq_mkv2 good ODE_bound_effect_tight[OF good tset sol] unfolding Vagree_def
apply (smt Compl_iff DFunl_def Vagree_def \<open>Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (ab, bb) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix)))) \<and> Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (mk_xode I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (sol t)) (semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> \<open>\<And>b. Vagree (sol 0, b) (sol t, b) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> fst_conv mk_xode.simps)
apply(rule vec_extensionality)
using sol0 good obv DFunl_def eq_mkv2 good ODE_bound_effect_tight[OF good tset sol] unfolding Vagree_def
apply (smt Compl_iff DFunl_def Vagree_def \<open>Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (ab, bb) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix)))) \<and> Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (mk_xode I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (sol t)) (semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> \<open>\<And>b. Vagree (sol 0, b) (sol t, b) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> fst_conv mk_xode.simps)
apply(rule vec_extensionality)
using sol0 good obv DFunl_def eq_mkv2 good ODE_bound_effect_tight[OF good tset sol] unfolding Vagree_def
apply (smt Compl_iff DFunl_def Vagree_def \<open>Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (ab, bb) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix)))) \<and> Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (mk_xode I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (sol t)) (semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> \<open>\<And>b. Vagree (sol 0, b) (sol t, b) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> fst_conv mk_xode.simps)
apply(rule vec_extensionality)
using sol0 good obv DFunl_def eq_mkv2 good ODE_bound_effect_tight[OF good tset sol] unfolding Vagree_def
apply (smt Compl_iff DFunl_def Vagree_def \<open>Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (ab, bb) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix)))) \<and> Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (mk_xode I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (sol t)) (semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> \<open>\<And>b. Vagree (sol 0, b) (sol t, b) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> fst_conv mk_xode.simps)
apply(rule vec_extensionality)
using sol0 good obv DFunl_def eq_mkv2 good ODE_bound_effect_tight[OF good tset sol] unfolding Vagree_def
apply (smt Compl_iff DFunl_def Vagree_def \<open>Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (ab, bb) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix)))) \<and> Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (mk_xode I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (sol t)) (semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> \<open>\<And>b. Vagree (sol 0, b) (sol t, b) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> fst_conv mk_xode.simps)
apply(rule vec_extensionality)
using sol0 good obv DFunl_def eq_mkv2 good ODE_bound_effect_tight[OF good tset sol] unfolding Vagree_def
apply (smt Compl_iff DFunl_def Vagree_def \<open>Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (ab, bb) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix)))) \<and> Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (mk_xode I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (sol t)) (semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> \<open>\<And>b. Vagree (sol 0, b) (sol t, b) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> fst_conv mk_xode.simps)
apply(rule vec_extensionality)
using sol0 good obv DFunl_def eq_mkv2 good ODE_bound_effect_tight[OF good tset sol] unfolding Vagree_def
apply (smt Compl_iff DFunl_def Vagree_def \<open>Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (ab, bb) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix)))) \<and> Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (mk_xode I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (sol t)) (semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> \<open>\<And>b. Vagree (sol 0, b) (sol t, b) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> fst_conv mk_xode.simps)
apply(rule vec_extensionality)
using sol0 good obv DFunl_def eq_mkv2 good ODE_bound_effect_tight[OF good tset sol] unfolding Vagree_def
apply (smt Compl_iff DFunl_def Vagree_def \<open>Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (ab, bb) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix)))) \<and> Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (mk_xode I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (sol t)) (semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> \<open>\<And>b. Vagree (sol 0, b) (sol t, b) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> fst_conv mk_xode.simps)
done
have FVF_univ:"FVF (Pc Ix) = UNIV" by auto
have repd_eq:"\<And>\<nu> x r. (snd \<nu>) $ x = r \<Longrightarrow> \<nu> = repd \<nu> x r" subgoal for \<nu> x r
apply(cases "\<nu>", simp)
by(rule vec_extensionality, auto) done
have sem_eq':"
((mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) \<in> fml_sem I (Pc Ix)) =
(repd (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) Ix
(dterm_sem I (DFunl Ix) (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t))) \<in> fml_sem I (Pc Ix))"
apply(rule coincidence_formula)
subgoal using dsafe by auto
apply(rule good)
apply(rule good)
subgoal by (rule Iagree_refl)
using mk_v_agree[of "I" "(OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix)))" "(ab, bb)" "(sol t)"]
apply(simp add: Vagree_def)
apply(erule conjE)+
apply(erule allE[where x="Ix"])+
apply(auto simp add: DFunl_def ODE_sem)
apply (metis DFunl_def eq_mkv2 good sol_mkv_eq)
apply (metis DFunl_def eq_mkv2 good sol_mkv_eq)
apply (metis DFunl_def eq_mkv2 good sol_mkv_eq)
apply (metis DFunl_def eq_mkv2 good sol_mkv_eq)
apply (metis DFunl_def eq_mkv2 good sol_mkv_eq)
apply (metis DFunl_def eq_mkv2 good sol_mkv_eq)
apply (metis DFunl_def eq_mkv2 good sol_mkv_eq)
apply (metis DFunl_def eq_mkv2 good sol_mkv_eq)
apply (metis DFunl_def eq_mkv2 good sol_mkv_eq obv)
using DFunl_def eq_mkv2 good sol_mkv_eq obv apply blast
apply (metis DFunl_def eq_mkv2 good sol_mkv_eq obv)
apply (metis DFunl_def eq_mkv2 good sol_mkv_eq obv)
using DFunl_def eq_mkv2 good sol_mkv_eq obv apply blast
apply (metis DFunl_def eq_mkv2 good sol_mkv_eq obv)
apply (metis DFunl_def eq_mkv2 good sol_mkv_eq obv)
using DFunl_def eq_mkv2 good sol_mkv_eq obv apply blast
apply (metis DFunl_def eq_mkv2 good sol_mkv_eq obv)
apply (metis DFunl_def eq_mkv2 good sol_mkv_eq obv)
using DFunl_def eq_mkv2 good sol_mkv_eq obv apply blast
apply (metis DFunl_def eq_mkv2 good sol_mkv_eq obv) done
then have sem_eq:"
(?my\<omega> \<in> fml_sem I (Pc Ix)) =
(repd (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) Ix
(dterm_sem I (DFunl Ix) (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t))) \<in> fml_sem I (Pc Ix))"
using DFunl_def eq_mkv2 good sol_mkv_eq obv
by (auto,(presburger)+)
show "repd (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) Ix
(dterm_sem I (DFunl Ix) (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)))
\<in> fml_sem I (Pc Ix)"
using bigRes sem_eq by blast
next
fix I::"interp"
and aa ba ab bb sol
and t::real
assume good_interp:"is_interp I"
assume all:"\<forall>\<omega>. (\<exists>\<nu> sol t. ((ab, bb), \<omega>) = (\<nu>, mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) \<nu> (sol t)) \<and>
0 \<le> t \<and>
(sol solves_ode (\<lambda>_. ODE_sem I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))) {0..t}
{x. mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) \<nu> x \<in> fml_sem I (Pc Iy)} \<and>
sol 0 = fst \<nu>) \<longrightarrow>
(\<forall>\<omega>'. \<omega>' = repd \<omega> Ix (dterm_sem I (DFunl Ix) \<omega>) \<longrightarrow> \<omega>' \<in> fml_sem I (Pc Ix))"
let ?my\<omega> = "mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab,bb) (sol t)"
assume t:"0 \<le> t"
assume aaba:"(aa, ba) = mk_v I (OProd (OSing Ix (DFunl Ix)) (OVar Ix (Some Ix))) (ab, bb) (sol t)"
assume sol:"
(sol solves_ode (\<lambda>_. ODE_sem I (OProd (OSing Ix (DFunl Ix)) (OVar Ix (Some Ix))))) {0..t}
{x. mk_v I (OProd (OSing Ix (DFunl Ix)) (OVar Ix (Some Ix))) (ab, bb) x \<in> fml_sem I (Pc Iy)}"
assume sol0:"sol 0 = fst (ab, bb)"
have bigEx:"(\<exists>\<nu> sol t. ((ab, bb), ?my\<omega>) = (\<nu>, mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) \<nu> (sol t)) \<and>
0 \<le> t \<and>
(sol solves_ode (\<lambda>_. ODE_sem I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))) {0..t}
{x. mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) \<nu> x \<in> fml_sem I (Pc Iy)} \<and>
sol 0 = fst \<nu>)"
apply(rule exI[where x="(ab, bb)"])
apply(rule exI[where x=sol])
apply(rule exI[where x=t])
apply(rule conjI)
apply(rule refl)
apply(rule conjI)
apply(rule t)
apply(rule conjI)
apply(rule solves_ode_cong[where ?ODE1.0="(\<lambda>_. ODE_sem I (OProd (OSing Ix (DFunl Ix))(OVar Ix (Some Ix))))",
where ?X1.0=" {x. mk_v I (OProd (OSing Ix (DFunl Ix)) (OVar Ix (Some Ix))) (ab, bb) x \<in> fml_sem I (Pc Iy)}"])
subgoal apply auto by(rule ext,rule ext, rule vec_extensionality,auto)
subgoal using comm_mkv[OF good_interp] by auto
apply(rule sol)
by (rule sol0)
have notin1:"Inl Ix \<notin> BVO (OVar Ix (Some Ix))" using good_interp unfolding is_interp_def by auto
have notin2:"Inr Ix \<notin> BVO (OVar Ix (Some Ix))" using good_interp unfolding is_interp_def by auto
have ODE_sem:"ODE_sem I (OVar Ix (Some Ix)) (sol t) $ Ix = 0"
using good_interp unfolding is_interp_def by auto
note good = good_interp
have tset:"t \<in> {0..t}" using t by auto
have vas:"Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (ab, bb) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix)))) \<and> Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (mk_xode I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (sol t)) (semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))"
"\<And>b. Vagree (sol 0, b) (sol t, b) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))"
using mk_v_agree[of "I" "(OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix)))" "(ab, bb)" "(sol t)"]
using sol0 good obv DFunl_def eq_mkv2 good ODE_bound_effect_tight[OF good tset sol]
by(simp add: Vagree_def)+
have sol_mkv_eq:"(sol t) = fst (mk_v I (OProd (OSing Ix (DFunl Ix)) (OVar Ix (Some Ix))) (ab, bb) (sol t))"
using mk_v_agree[of "I" "(OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix)))" "(ab, bb)" "(sol t)"]
using sol0 good obv DFunl_def eq_mkv2 good ODE_bound_effect_tight[OF good tset sol]
apply(simp add: Vagree_def)
apply(erule conjE)+
apply(erule allE[where x="Ix"])+
apply(cases "Ix \<in> ODEBV I Ix (Some Ix)")
using sol0 apply(auto simp add: DFunl_def ODE_sem sol0)
using good obv apply auto
(* TODO: stuff about if derivative is zero then value is constant*)
apply(rule vec_extensionality)
using sol0 good obv DFunl_def eq_mkv2 good ODE_bound_effect_tight[OF good tset sol]
unfolding Vagree_def apply auto
apply (smt Compl_iff DFunl_def Vagree_def vas fst_conv mk_xode.simps)
apply(rule vec_extensionality)
using sol0 good obv DFunl_def eq_mkv2 good ODE_bound_effect_tight[OF good tset sol] unfolding Vagree_def
apply (smt Compl_iff DFunl_def Vagree_def \<open>Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (ab, bb) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix)))) \<and> Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (mk_xode I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (sol t)) (semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> \<open>\<And>b. Vagree (sol 0, b) (sol t, b) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> fst_conv mk_xode.simps)
apply(rule vec_extensionality)
using sol0 good obv DFunl_def eq_mkv2 good ODE_bound_effect_tight[OF good tset sol] unfolding Vagree_def
apply (smt Compl_iff DFunl_def Vagree_def \<open>Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (ab, bb) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix)))) \<and> Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (mk_xode I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (sol t)) (semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> \<open>\<And>b. Vagree (sol 0, b) (sol t, b) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> fst_conv mk_xode.simps)
apply(rule vec_extensionality)
using sol0 good obv DFunl_def eq_mkv2 good ODE_bound_effect_tight[OF good tset sol] unfolding Vagree_def
apply (smt Compl_iff DFunl_def Vagree_def \<open>Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (ab, bb) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix)))) \<and> Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (mk_xode I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (sol t)) (semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> \<open>\<And>b. Vagree (sol 0, b) (sol t, b) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> fst_conv mk_xode.simps)
apply(rule vec_extensionality)
using sol0 good obv DFunl_def eq_mkv2 good ODE_bound_effect_tight[OF good tset sol] unfolding Vagree_def
apply (smt Compl_iff DFunl_def Vagree_def \<open>Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (ab, bb) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix)))) \<and> Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (mk_xode I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (sol t)) (semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> \<open>\<And>b. Vagree (sol 0, b) (sol t, b) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> fst_conv mk_xode.simps)
apply(rule vec_extensionality)
using sol0 good obv DFunl_def eq_mkv2 good ODE_bound_effect_tight[OF good tset sol] unfolding Vagree_def
apply (smt Compl_iff DFunl_def Vagree_def \<open>Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (ab, bb) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix)))) \<and> Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (mk_xode I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (sol t)) (semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> \<open>\<And>b. Vagree (sol 0, b) (sol t, b) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> fst_conv mk_xode.simps)
apply(rule vec_extensionality)
using sol0 good obv DFunl_def eq_mkv2 good ODE_bound_effect_tight[OF good tset sol] unfolding Vagree_def
apply (smt Compl_iff DFunl_def Vagree_def \<open>Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (ab, bb) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix)))) \<and> Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (mk_xode I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (sol t)) (semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> \<open>\<And>b. Vagree (sol 0, b) (sol t, b) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> fst_conv mk_xode.simps)
apply(rule vec_extensionality)
using sol0 good obv DFunl_def eq_mkv2 good ODE_bound_effect_tight[OF good tset sol] unfolding Vagree_def
apply (smt Compl_iff DFunl_def Vagree_def \<open>Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (ab, bb) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix)))) \<and> Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (mk_xode I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (sol t)) (semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> \<open>\<And>b. Vagree (sol 0, b) (sol t, b) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> fst_conv mk_xode.simps)
apply(rule vec_extensionality)
using sol0 good obv DFunl_def eq_mkv2 good ODE_bound_effect_tight[OF good tset sol] unfolding Vagree_def
apply (smt Compl_iff DFunl_def Vagree_def \<open>Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (ab, bb) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix)))) \<and> Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (mk_xode I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (sol t)) (semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> \<open>\<And>b. Vagree (sol 0, b) (sol t, b) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> fst_conv mk_xode.simps)
apply(rule vec_extensionality)
using sol0 good obv DFunl_def eq_mkv2 good ODE_bound_effect_tight[OF good tset sol] unfolding Vagree_def
apply (smt Compl_iff DFunl_def Vagree_def \<open>Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (ab, bb) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix)))) \<and> Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (mk_xode I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (sol t)) (semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> \<open>\<And>b. Vagree (sol 0, b) (sol t, b) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> fst_conv mk_xode.simps)
apply(rule vec_extensionality)
using sol0 good obv DFunl_def eq_mkv2 good ODE_bound_effect_tight[OF good tset sol] unfolding Vagree_def
apply (smt Compl_iff DFunl_def Vagree_def \<open>Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (ab, bb) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix)))) \<and> Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (mk_xode I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (sol t)) (semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> \<open>\<And>b. Vagree (sol 0, b) (sol t, b) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> fst_conv mk_xode.simps)
apply(rule vec_extensionality)
using sol0 good obv DFunl_def eq_mkv2 good ODE_bound_effect_tight[OF good tset sol] unfolding Vagree_def
apply (smt Compl_iff DFunl_def Vagree_def \<open>Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (ab, bb) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix)))) \<and> Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (mk_xode I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (sol t)) (semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> \<open>\<And>b. Vagree (sol 0, b) (sol t, b) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> fst_conv mk_xode.simps)
apply(rule vec_extensionality)
using sol0 good obv DFunl_def eq_mkv2 good ODE_bound_effect_tight[OF good tset sol] unfolding Vagree_def
apply (smt Compl_iff DFunl_def Vagree_def \<open>Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (ab, bb) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix)))) \<and> Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (mk_xode I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (sol t)) (semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> \<open>\<And>b. Vagree (sol 0, b) (sol t, b) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> fst_conv mk_xode.simps)
apply(rule vec_extensionality)
using sol0 good obv DFunl_def eq_mkv2 good ODE_bound_effect_tight[OF good tset sol] unfolding Vagree_def
apply (smt Compl_iff DFunl_def Vagree_def \<open>Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (ab, bb) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix)))) \<and> Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (mk_xode I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (sol t)) (semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> \<open>\<And>b. Vagree (sol 0, b) (sol t, b) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> fst_conv mk_xode.simps)
apply(rule vec_extensionality)
using sol0 good obv DFunl_def eq_mkv2 good ODE_bound_effect_tight[OF good tset sol] unfolding Vagree_def
apply (smt Compl_iff DFunl_def Vagree_def \<open>Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (ab, bb) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix)))) \<and> Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (mk_xode I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (sol t)) (semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> \<open>\<And>b. Vagree (sol 0, b) (sol t, b) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> fst_conv mk_xode.simps)
apply(rule vec_extensionality)
using sol0 good obv DFunl_def eq_mkv2 good ODE_bound_effect_tight[OF good tset sol] unfolding Vagree_def
apply (smt Compl_iff DFunl_def Vagree_def \<open>Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (ab, bb) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix)))) \<and> Vagree (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) (mk_xode I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (sol t)) (semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> \<open>\<And>b. Vagree (sol 0, b) (sol t, b) (- semBV I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))))\<close> fst_conv mk_xode.simps)
done
have vec_eq:"
(\<chi> i. dterm_sem I (Syntax.Var i) (mk_v I (OProd (OSing Ix (DFunl Ix))(OVar Ix (Some Ix))) (ab, bb) (sol t))) =
(\<chi> i. sterm_sem I (Syntax.Var i) (sol t))"
apply(rule vec_extensionality)
using mk_v_agree[of I "(OProd (OSing Ix (DFunl Ix))(OVar Ix (Some Ix)))" "(ab, bb)" "(sol t)"]
apply (simp add: Vagree_def)
subgoal for i
apply(cases "i = Ix")
subgoal by(auto)
subgoal apply(clarsimp) apply(erule allE[where x=i])+
apply(auto)
using notin1 notin2 sol_mkv_eq by auto
done done
have rep_sem_eq:"repd (mk_v I (OProd (OSing Ix (DFunl Ix))(OVar Ix (Some Ix))) (ab, bb) (sol t)) Ix
(dterm_sem I (DFunl Ix)
(mk_v I (OProd (OSing Ix (DFunl Ix))(OVar Ix (Some Ix))) (ab, bb) (sol t))) \<in> fml_sem I (Pc Ix)
= (repd ?my\<omega> Ix (dterm_sem I (DFunl Ix) ?my\<omega>) \<in> fml_sem I (Pc Ix))"
apply(rule coincidence_formula)
subgoal using dsafe by auto
apply(rule good_interp) apply(rule good_interp)
subgoal by (rule Iagree_refl)
using mk_v_agree[of "I" "(OProd (OSing Ix (DFunl Ix))(OVar Ix (Some Ix)))" "(ab, bb)" "(sol t)"]
unfolding Vagree_def
apply simp
apply(erule conjE)+
apply(erule allE[where x="Ix"])+
apply(simp add: ODE_sem)
using vec_eq eq_mkv2
by (simp add: good_interp)
note good = good_interp
have sem_eq':"
((mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) \<in> fml_sem I (Pc Ix)) =
(repd (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) Ix
(dterm_sem I (DFunl Ix) (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t))) \<in> fml_sem I (Pc Ix))"
apply(rule coincidence_formula)
subgoal using dsafe by simp
apply(rule good)
apply(rule good)
subgoal by (rule Iagree_refl)
using mk_v_agree[of "I" "(OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix)))" "(ab, bb)" "(sol t)"]
apply(simp add: Vagree_def)
apply(erule conjE)+
apply(erule allE[where x="Ix"])+
apply(auto simp add: DFunl_def ODE_sem)
apply (metis DFunl_def eq_mkv2 good sol_mkv_eq)
apply (metis DFunl_def eq_mkv2 good sol_mkv_eq)
apply (metis DFunl_def eq_mkv2 good sol_mkv_eq)
apply (metis DFunl_def eq_mkv2 good sol_mkv_eq)
apply (metis DFunl_def eq_mkv2 good sol_mkv_eq)
apply (metis DFunl_def eq_mkv2 good sol_mkv_eq)
apply (metis DFunl_def eq_mkv2 good sol_mkv_eq)
apply (metis DFunl_def eq_mkv2 good sol_mkv_eq)
apply (metis DFunl_def eq_mkv2 good sol_mkv_eq obv)
using DFunl_def eq_mkv2 good sol_mkv_eq obv apply blast
apply (metis DFunl_def eq_mkv2 good sol_mkv_eq obv)
apply (metis DFunl_def eq_mkv2 good sol_mkv_eq obv)
using DFunl_def eq_mkv2 good sol_mkv_eq obv apply blast
apply (metis DFunl_def eq_mkv2 good sol_mkv_eq obv)
apply (metis DFunl_def eq_mkv2 good sol_mkv_eq obv)
using DFunl_def eq_mkv2 good sol_mkv_eq obv apply blast
apply (metis DFunl_def eq_mkv2 good sol_mkv_eq obv)
apply (metis DFunl_def eq_mkv2 good sol_mkv_eq obv)
using DFunl_def eq_mkv2 good sol_mkv_eq obv apply blast
apply (metis DFunl_def eq_mkv2 good sol_mkv_eq obv) done
then have sem_eq'':"
(?my\<omega> \<in> fml_sem I (Pc Ix)) =
(repd (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) Ix
(dterm_sem I (DFunl Ix) (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t))) \<in> fml_sem I (Pc Ix))"
using DFunl_def eq_mkv2 good sol_mkv_eq obv by (auto,(presburger)+)
have sem_eq:
"(repd ?my\<omega> Ix (dterm_sem I (DFunl Ix) ?my\<omega>) \<in> fml_sem I (Pc Ix))
= (mk_v I (OProd (OSing Ix (DFunl Ix))(OVar Ix (Some Ix))) (ab, bb) (sol t) \<in> fml_sem I (Pc Ix)) "
using sem_eq' sem_eq'' DFunl_def eq_mkv2 good sol_mkv_eq obv
apply auto
by presburger+
(* using notin1 by auto *)
have some_sem:"repd (mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t)) Ix
(dterm_sem I (DFunl Ix)
(mk_v I (OProd (OVar Ix (Some Ix)) (OSing Ix (DFunl Ix))) (ab, bb) (sol t))) \<in> fml_sem I (Pc Ix)"
using rep_sem_eq
using all bigEx by blast
have bigImp:"(\<forall>\<omega>'. \<omega>' = repd ?my\<omega> Ix (dterm_sem I (DFunl Ix) ?my\<omega>) \<longrightarrow> \<omega>' \<in> fml_sem I (Pc Ix))"
apply(rule allI)
apply(rule impI)
apply auto
using some_sem by auto
have fml_sem:"repd ?my\<omega> Ix (dterm_sem I (DFunl Ix) ?my\<omega>) \<in> fml_sem I (Pc Ix)"
using sem_eq bigImp by blast
show "mk_v I (OProd (OSing Ix (DFunl Ix))(OVar Ix (Some Ix))) (ab, bb) (sol t) \<in> fml_sem I (Pc Ix)"
using fml_sem sem_eq by blast
qed
qed
(*
(Q \<rightarrow> [c&Q](f(x)' \<ge> g(x)'))
\<rightarrow>
([c&Q](f(x) \<ge> g(x))) --> (Q \<rightarrow> (f(x) \<ge> g(x))
*)
(* in axiombase:
(q(||) -> [{c&q(||)}](p(||)'))
\<rightarrow>
([{c&q(||)}]p(||) <-> [?q(||);]p(||))
*)
definition DIGeqaxiom :: "ODE \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> formula"
where [axiom_defs]:"DIGeqaxiom ODE \<theta>1 \<theta>2 =
Implies
(Implies (DPredl Ix) (And (Geq \<theta>1 \<theta>2)
([[EvolveODE ODE (DPredl Ix)]](Geq (Differential \<theta>1) (Differential \<theta>2)))))
([[EvolveODE ODE (DPredl Ix)]](Geq \<theta>1 \<theta>2))
"
definition DIEqaxiom :: "ODE \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> formula"
where [axiom_defs]:"DIEqaxiom ODE \<theta>1 \<theta>2 =
Implies
(Implies (DPredl Ix) (And (Equals \<theta>1 \<theta>2)
([[EvolveODE ODE (DPredl Ix)]](Equals (Differential \<theta>1) (Differential \<theta>2)))))
([[EvolveODE ODE (DPredl Ix)]](Equals \<theta>1 \<theta>2))
"
(*
g(x) > h(x) \<rightarrow> [x'=f(x), c & p(x)](g(x)' \<ge> h(x)') \<rightarrow> [x'=f(x), c & p(x)]g(x) > h(x)
*)
(*
(Q \<rightarrow> [c&Q](f(x)' \<ge> g(x)'))
\<rightarrow>
([c&Q](f(x) > g(x))) <-> (Q \<rightarrow> (f(x) > g(x))
*)
definition DIGraxiom :: "ODE \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> formula"
where [axiom_defs]:"DIGraxiom ODE \<theta>1 \<theta>2 =
Implies
(Implies (DPredl Ix) (And (Greater \<theta>1 \<theta>2)
([[EvolveODE ODE (DPredl Ix)]](Geq (Differential \<theta>1) (Differential \<theta>2)))))
([[EvolveODE ODE (DPredl Ix)]](Greater \<theta>1 \<theta>2))"
(* [{1' = 1(1) & 1(1)}]2(1) <->
\<exists>2. [{1'=1(1), 2' = 2(1)*2 + 3(1) & 1(1)}]2(1)*)
definition DGaxiom :: "formula"
where [axiom_defs]:"DGaxiom = (([[EvolveODE (OSing Ix (f1 Ix Ix)) (p1 Ix Ix)]]p1 Iy Ix) \<leftrightarrow>
(Exists Iy
([[EvolveODE (oprod (OSing Ix (f1 Ix Ix)) (OSing Iy (Plus (Times (f1 Iy Ix) (Syntax.Var Iy )) (f1 Iz Ix)))) (p1 Ix Ix)]]
p1 Iy Ix)))"
subsection \<open>Proofs for Derivative Axioms\<close>
lemma frechet_empty[simp]: "frechet I (Syntax.empty i) = (\<lambda>_ _. 0)"
by (auto simp: Syntax.empty_def)
lemma constant_deriv_inner:
assumes interp:"\<forall>x i. (Functions I i has_derivative FunctionFrechet I i x) (at x)"
shows "FunctionFrechet I Ix (vec_lambda (\<lambda>i. sterm_sem I (empty i) (fst \<nu>))) (vec_lambda(\<lambda>i. frechet I (empty i) (fst \<nu>) (snd \<nu>)))= 0"
proof -
have empty_zero:"(vec_lambda(\<lambda>i. frechet I (empty i) (fst \<nu>) (snd \<nu>))) = 0"
using empty_def Cart_lambda_cong frechet.simps(5) zero_vec_def
by (simp add: vec_extensionality)
let ?x = "(vec_lambda (\<lambda>i. sterm_sem I (empty i) (fst \<nu>)))"
from interp
have has_deriv:"(Functions I Ix has_derivative FunctionFrechet I Ix ?x) (at ?x)"
by auto
then have f_linear:"linear (FunctionFrechet I Ix ?x)"
using Deriv.has_derivative_linear by auto
then show ?thesis using empty_zero f_linear linear_0 by auto
qed
lemma constant_deriv_innerY:
assumes interp:"\<forall>x i. (Functions I i has_derivative FunctionFrechet I i x) (at x)"
shows "FunctionFrechet I Iy (vec_lambda (\<lambda>i. sterm_sem I (empty i) (fst \<nu>))) (vec_lambda(\<lambda>i. frechet I (empty i) (fst \<nu>) (snd \<nu>)))= 0"
proof -
have empty_zero:"(vec_lambda(\<lambda>i. frechet I (empty i) (fst \<nu>) (snd \<nu>))) = 0"
using empty_def Cart_lambda_cong frechet.simps(5) zero_vec_def
apply auto
apply(rule vec_extensionality)
using empty_def Cart_lambda_cong frechet.simps(5) zero_vec_def
by (smt Frechet_Const)
let ?x = "(vec_lambda (\<lambda>i. sterm_sem I (empty i) (fst \<nu>)))"
from interp
have has_deriv:"(Functions I Iy has_derivative FunctionFrechet I Iy ?x) (at ?x)"
by auto
then have f_linear:"linear (FunctionFrechet I Iy ?x)"
using Deriv.has_derivative_linear by auto
then show ?thesis using empty_zero f_linear linear_0 by auto
qed
lemma constant_deriv_zero:"is_interp I \<Longrightarrow> directional_derivative I ($f Ix empty) \<nu> = 0"
apply(simp only: is_interp_def directional_derivative_def frechet.simps frechet_correctness)
apply(rule constant_deriv_inner)
apply(auto)
done
lemma constant_deriv_zeroY:"is_interp I \<Longrightarrow> directional_derivative I ($f Iy empty) \<nu> = 0"
apply(simp only: is_interp_def directional_derivative_def frechet.simps frechet_correctness)
apply(rule constant_deriv_innerY)
apply(auto)
done
theorem diff_const_axiom_valid: "valid diff_const_axiom"
apply(simp only: valid_def diff_const_axiom_def equals_sem)
apply(rule allI | rule impI)+
apply(simp only: dterm_sem.simps constant_deriv_zero sterm_sem.simps)
by(auto simp add: POS_INF_def NEG_INF_def Abs_bword_inverse bword_zero_def)
theorem diff_var_axiom_valid: "valid diff_var_axiom"
apply(auto simp add: diff_var_axiom_def valid_def directional_derivative_def)
by (metis inner_prod_eq)
theorem dMinusAxiom_valid: "valid dMinusAxiom"
apply(auto simp add: dMinusAxiom_def valid_def Minus_def)
subgoal for I a b
using frechet_correctness[of I "(Plus (state_fun Ix) (state_fun Iy))" b]
unfolding state_fun_def apply (auto intro: dfree.intros)
unfolding directional_derivative_def by auto
done
(* (c_()*f_(||))' = c_()*(f_(||))' *)
definition DiffLinearAxiom::"formula"
where [axiom_defs]:"DiffLinearAxiom \<equiv>
Equals
(Differential (Times (Function Iy empty) (DFunl Ix)))
(Times (Function Iy empty) (Differential (DFunl Ix)))"
theorem DiffLinear_valid:"valid DiffLinearAxiom"
apply(auto simp add: DiffLinearAxiom_def valid_def Minus_def DFunl_def empty_def)
subgoal for I a b
using frechet_correctness[of I "(Times ($f Iy (\<lambda>i. \<^bold>0)) ($f Ix trm.Var))" b]
using constant_deriv_zeroY
unfolding state_fun_def apply (auto intro: dfree.intros)
unfolding directional_derivative_def by(auto simp add: empty_def)
done
theorem diff_plus_axiom_valid: "valid diff_plus_axiom"
apply(auto simp add: diff_plus_axiom_def valid_def)
subgoal for I a b
using frechet_correctness[of I "(Plus (state_fun Ix) (state_fun Iy))" b]
unfolding state_fun_def apply (auto intro: dfree.intros)
unfolding directional_derivative_def by auto
done
theorem diff_times_axiom_valid: "valid diff_times_axiom"
apply(auto simp add: diff_times_axiom_def valid_def)
subgoal for I a b
using frechet_correctness[of I "(Times (state_fun Ix) (state_fun Iy))" b]
unfolding state_fun_def apply (auto intro: dfree.intros)
unfolding directional_derivative_def by auto
done
subsection \<open>Proofs for ODE Axioms\<close>
lemma DW_valid:"valid DWaxiom"
apply(unfold DWaxiom_def valid_def Let_def impl_sem )
apply(safe)
apply(auto simp only: fml_sem.simps prog_sem.simps box_sem iff_sem)
subgoal for I aa ba ab bb sol t
using mk_v_agree[of I "(OVar Ix None)" "(ab,bb)" "sol t"]
Vagree_univ[of "aa" "ba" "sol t" "ODEs I Ix None (sol t) "] solves_ode_domainD
by (fastforce)
subgoal for I aa ba ab bb sol t
using mk_v_agree[of I "(OVar Ix None)" "(ab,bb)" "sol t"]
Vagree_univ[of "aa" "ba" "sol t" "ODEs I Ix None (sol t) "] solves_ode_domainD
by (fastforce)
done
lemma DE_lemma:
fixes ab bb::"simple_state"
and sol::"real \<Rightarrow> simple_state"
and I::"interp"
shows
"repd (mk_v I (OSing Ix (f1 Ix Ix)) (ab, bb) (sol t)) Ix (dterm_sem I (f1 Ix Ix) (mk_v I (OSing Ix (f1 Ix Ix)) (ab, bb) (sol t)))
= mk_v I (OSing Ix (f1 Ix Ix)) (ab, bb) (sol t)"
proof
have set_eq:" {Inl Ix, Inr Ix} = {Inr Ix, Inl Ix}" by auto
have agree:"Vagree (mk_v I (OSing Ix (f1 Ix Ix)) (ab, bb) (sol t)) (mk_xode I (OSing Ix (f1 Ix Ix)) (sol t))
{Inl Ix, Inr Ix}"
using mk_v_agree[of I "(OSing Ix (f1 Ix Ix))" "(ab, bb)" "(sol t)"]
unfolding semBV.simps using set_eq by auto
have fact:"dterm_sem I (f1 Ix Ix) (mk_v I (OSing Ix (f1 Ix Ix)) (ab, bb) (sol t))
= snd (mk_v I (OSing Ix (f1 Ix Ix)) (ab, bb) (sol t)) $ Ix"
using agree apply(simp only: Vagree_def dterm_sem.simps f1_def mk_xode.simps)
proof -
assume alls:"(\<forall>i. Inl i \<in> {Inl Ix, Inr Ix} \<longrightarrow>
fst (mk_v I (OSing Ix ($f Ix (singleton (trm.Var Ix)))) (ab, bb) (sol t)) $ i =
fst (sol t, ODE_sem I (OSing Ix ($f Ix (singleton (trm.Var Ix)))) (sol t)) $ i) \<and>
(\<forall>i. Inr i \<in> {Inl Ix, Inr Ix} \<longrightarrow>
snd (mk_v I (OSing Ix ($f Ix (singleton (trm.Var Ix)))) (ab, bb) (sol t)) $ i =
snd (sol t, ODE_sem I (OSing Ix ($f Ix (singleton (trm.Var Ix)))) (sol t)) $ i)"
hence atVid'':"snd (mk_v I (OSing Ix ($f Ix (singleton (trm.Var Ix)))) (ab, bb) (sol t)) $ Ix = sterm_sem I ($f Ix (singleton (trm.Var Ix))) (sol t)"
by auto
have argsEq:"(\<chi> i. dterm_sem I (singleton (trm.Var Ix) i)
(mk_v I (OSing Ix ($f Ix (singleton (trm.Var Ix)))) (ab, bb) (sol t)))
= (\<chi> i. sterm_sem I (singleton (trm.Var Ix) i) (sol t))"
using agree by (simp add: ext Vagree_def f1_def)
thus "Functions I Ix (\<chi> i. dterm_sem I (singleton (trm.Var Ix) i)
(mk_v I (OSing Ix ($f Ix (singleton (trm.Var Ix)))) (ab, bb) (sol t)))
= snd (mk_v I (OSing Ix ($f Ix (singleton (trm.Var Ix)))) (ab, bb) (sol t)) $ Ix"
by (simp only: atVid'' ODE_sem.simps sterm_sem.simps dterm_sem.simps)
qed
have eqSnd:"(\<chi> y. if Ix = y then snd (mk_v I (OSing Ix (f1 Ix Ix)) (ab, bb) (sol t)) $ Ix
else snd (mk_v I (OSing Ix (f1 Ix Ix)) (ab, bb) (sol t)) $ y) = snd (mk_v I (OSing Ix (f1 Ix Ix)) (ab, bb) (sol t))"
by (simp add: vec_extensionality)
have truth:"repd (mk_v I (OSing Ix (f1 Ix Ix)) (ab, bb) (sol t)) Ix
(dterm_sem I (f1 Ix Ix) (mk_v I (OSing Ix (f1 Ix Ix)) (ab, bb) (sol t)))
= mk_v I (OSing Ix (f1 Ix Ix)) (ab, bb) (sol t)"
using fact by (auto simp only: eqSnd repd.simps fact prod.collapse split: if_split)
thus "fst (repd (mk_v I (OSing Ix (f1 Ix Ix)) (ab, bb) (sol t)) Ix
(dterm_sem I (f1 Ix Ix) (mk_v I (OSing Ix (f1 Ix Ix)) (ab, bb) (sol t)))) =
fst (mk_v I (OSing Ix (f1 Ix Ix)) (ab, bb) (sol t))"
"snd (repd (mk_v I (OSing Ix (f1 Ix Ix)) (ab, bb) (sol t)) Ix
(dterm_sem I (f1 Ix Ix) (mk_v I (OSing Ix (f1 Ix Ix)) (ab, bb) (sol t)))) =
snd (mk_v I (OSing Ix (f1 Ix Ix)) (ab, bb) (sol t)) "
by auto
qed
lemma DE_valid:"valid DEaxiom"
proof -
have invX:"Rep_ident (Abs_ident ''$x'') = ''$x''"
apply(rule Abs_ident_inverse)
by(auto simp add: max_str)
have invY:"Rep_ident (Abs_ident ''$y'') = ''$y''"
apply(rule Abs_ident_inverse)
by(auto simp add: max_str)
have dsafe:"dsafe ($f Ix (singleton (Syntax.Var Ix)))" by(auto simp add: f1_def p1_def Ix_def ident_expose_def Abs_ident_inverse invX SSENT_def FSENT_def SSENTINEL_def FSENTINEL_def max_str ilength_def)
have osafe:"osafe(OSing Ix (f1 Ix Ix))" by(auto simp add: f1_def p1_def Ix_def ident_expose_def Abs_ident_inverse invX SSENT_def FSENT_def SSENTINEL_def FSENTINEL_def max_str ilength_def)
have fsafe:"fsafe (p1 Iy Ix)" by(auto simp add: Iy_def f1_def p1_def Ix_def ident_expose_def Abs_ident_inverse invX SSENT_def FSENT_def SSENTINEL_def FSENTINEL_def max_str ilength_def)
show "valid DEaxiom"
apply(auto simp only: DEaxiom_def valid_def Let_def iff_sem impl_sem)
apply(auto simp only: fml_sem.simps prog_sem.simps mem_Collect_eq box_sem)
proof -
fix I::"interp"
and aa ba ab bb sol
and t::real
and ac bc
assume "is_interp I"
assume allw:"\<forall>\<omega>. (\<exists>\<nu> sol t.
((ab, bb), \<omega>) = (\<nu>, mk_v I (OSing Ix (f1 Ix Ix)) \<nu> (sol t)) \<and>
0 \<le> t \<and>
(sol solves_ode (\<lambda>_. ODE_sem I (OSing Ix (f1 Ix Ix)))) {0..t}
{x. mk_v I (OSing Ix (f1 Ix Ix)) \<nu> x \<in> fml_sem I (p1 Iy Ix)} \<and>
(sol 0) = (fst \<nu>) ) \<longrightarrow>
\<omega> \<in> fml_sem I (P Ix)"
assume t:"0 \<le> t"
assume aaba:"(aa, ba) = mk_v I (OSing Ix (f1 Ix Ix)) (ab, bb) (sol t)"
assume solve:" (sol solves_ode (\<lambda>_. ODE_sem I (OSing Ix (f1 Ix Ix)))) {0..t}
{x. mk_v I (OSing Ix (f1 Ix Ix)) (ab, bb) x \<in> fml_sem I (p1 Iy Ix)}"
assume sol0:" (sol 0) = (fst (ab, bb)) "
assume rep:" (ac, bc) =
repd (mk_v I (OSing Ix (f1 Ix Ix)) (ab, bb) (sol t)) Ix
(dterm_sem I (f1 Ix Ix) (mk_v I (OSing Ix (f1 Ix Ix)) (ab, bb) (sol t)))"
have aaba_sem:"(aa,ba) \<in> fml_sem I (P Ix)" using allw t aaba solve sol0 rep by blast
have truth:"repd (mk_v I (OSing Ix (f1 Ix Ix)) (ab, bb) (sol t)) Ix
(dterm_sem I (f1 Ix Ix) (mk_v I (OSing Ix (f1 Ix Ix)) (ab, bb) (sol t)))
= mk_v I (OSing Ix (f1 Ix Ix)) (ab, bb) (sol t)"
using DE_lemma by auto
show "
repd (mk_v I (OSing Ix (f1 Ix Ix)) (ab, bb) (sol t)) Ix
(dterm_sem I (f1 Ix Ix) (mk_v I (OSing Ix (f1 Ix Ix)) (ab, bb) (sol t)))
\<in> fml_sem I (P Ix)" using aaba aaba_sem truth by (auto)
next
fix I::"interp" and aa ba ab bb sol and t::real
assume "is_interp I"
assume all:"\<forall>\<omega>. (\<exists>\<nu> sol t.
((ab, bb), \<omega>) = (\<nu>, mk_v I (OSing Ix (f1 Ix Ix)) \<nu> (sol t)) \<and>
0 \<le> t \<and>
(sol solves_ode (\<lambda>_. ODE_sem I (OSing Ix (f1 Ix Ix)))) {0..t}
{x. mk_v I (OSing Ix (f1 Ix Ix)) \<nu> x \<in> fml_sem I (p1 Iy Ix)} \<and>
(sol 0) = (fst \<nu>) ) \<longrightarrow>
(\<forall>\<omega>'. \<omega>' = repd \<omega> Ix (dterm_sem I (f1 Ix Ix) \<omega>) \<longrightarrow> \<omega>' \<in> fml_sem I (P Ix))"
hence justW:"(\<exists>\<nu> sol t.
((ab, bb), (aa, ba)) = (\<nu>, mk_v I (OSing Ix (f1 Ix Ix)) \<nu> (sol t)) \<and>
0 \<le> t \<and>
(sol solves_ode (\<lambda>_. ODE_sem I (OSing Ix (f1 Ix Ix)))) {0..t}
{x. mk_v I (OSing Ix (f1 Ix Ix)) \<nu> x \<in> fml_sem I (p1 Iy Ix)} \<and>
(sol 0) = (fst \<nu>)) \<longrightarrow>
(\<forall>\<omega>'. \<omega>' = repd (aa, ba) Ix (dterm_sem I (f1 Ix Ix) (aa, ba)) \<longrightarrow> \<omega>' \<in> fml_sem I (P Ix))"
by (rule allE)
assume t:"0 \<le> t"
assume aaba:"(aa, ba) = mk_v I (OSing Ix (f1 Ix Ix)) (ab, bb) (sol t)"
assume sol:"(sol solves_ode (\<lambda>_. ODE_sem I (OSing Ix (f1 Ix Ix)))) {0..t}
{x. mk_v I (OSing Ix (f1 Ix Ix)) (ab, bb) x \<in> fml_sem I (p1 Iy Ix)}"
assume sol0:" (sol 0) = (fst (ab, bb))"
have "repd (aa, ba) Ix (dterm_sem I (f1 Ix Ix) (aa, ba)) \<in> fml_sem I (P Ix)"
using justW t aaba sol sol0 by auto
hence foo:"repd (mk_v I (OSing Ix (f1 Ix Ix)) (ab, bb) (sol t)) Ix (dterm_sem I (f1 Ix Ix) (mk_v I (OSing Ix (f1 Ix Ix)) (ab, bb) (sol t))) \<in> fml_sem I (P Ix)"
using aaba by auto
hence "repd (mk_v I (OSing Ix (f1 Ix Ix)) (ab, bb) (sol t)) Ix (dterm_sem I (f1 Ix Ix) (mk_v I (OSing Ix (f1 Ix Ix)) (ab, bb) (sol t)))
= mk_v I (OSing Ix (f1 Ix Ix)) (ab, bb) (sol t)" using DE_lemma by auto
thus "mk_v I (OSing Ix (f1 Ix Ix)) (ab, bb) (sol t) \<in> fml_sem I (P Ix)" using foo by auto
qed
qed
lemma DE_sys_valid:
assumes disj:"{Inl Ix, Inr Ix} \<inter> BVO ODE = {}"
shows "valid (([[EvolveODE (oprod (OSing Ix (f1 Ix Ix)) ODE) (p1 Iy Ix)]] (P Ix)) \<leftrightarrow>
([[EvolveODE ((oprod (OSing Ix (f1 Ix Ix))ODE)) (p1 Iy Ix)]]
[[DiffAssign Ix (f1 Ix Ix)]]P Ix))"
proof -
have invX:"Rep_ident (Abs_ident ''$x'') = ''$x''"
apply(rule Abs_ident_inverse)
by(auto simp add: max_str)
have invY:"Rep_ident (Abs_ident ''$y'') = ''$y''"
apply(rule Abs_ident_inverse)
by(auto simp add: max_str)
have dsafe:"dsafe ($f Ix (singleton (trm.Var Ix)))" by(auto simp add: Iy_def f1_def p1_def Ix_def ident_expose_def Abs_ident_inverse invX SSENT_def FSENT_def SSENTINEL_def FSENTINEL_def max_str ilength_def)
have osafe:"osafe(OSing Ix (f1 Ix Ix))" by(auto simp add: Iy_def f1_def p1_def Ix_def ident_expose_def Abs_ident_inverse invX SSENT_def FSENT_def SSENTINEL_def FSENTINEL_def max_str ilength_def)
have fsafe:"fsafe (p1 Iy Ix)" by(auto simp add: Iy_def f1_def p1_def Ix_def ident_expose_def Abs_ident_inverse invX SSENT_def FSENT_def SSENTINEL_def FSENTINEL_def max_str ilength_def)
show "valid (([[EvolveODE (oprod (OSing Ix (f1 Ix Ix)) ODE) (p1 Iy Ix)]] (P Ix)) \<leftrightarrow>
([[EvolveODE ((oprod (OSing Ix (f1 Ix Ix)) ODE)) (p1 Iy Ix)]]
[[DiffAssign Ix (f1 Ix Ix)]]P Ix))"
apply(auto simp only: DEaxiom_def valid_def Let_def iff_sem impl_sem)
apply(auto simp only: fml_sem.simps prog_sem.simps mem_Collect_eq box_sem f1_def p1_def P_def expand_singleton)
proof -
fix I ::"interp"
and aa ba ab bb sol
and t::real
and ac bc
assume good:"is_interp I"
assume bigNone:"
\<forall>\<omega>. (\<exists>\<nu> sol t. ((ab, bb), \<omega>) = (\<nu>, mk_v I (oprod (OSing Ix ($f Ix (\<lambda>i. if i = Ix then trm.Var Ix else \<^bold>0))) ODE) \<nu> (sol t)) \<and>
0 \<le> t \<and>
(sol solves_ode (\<lambda>_. ODE_sem I (oprod(OSing Ix ($f Ix (\<lambda>i. if i = Ix then trm.Var Ix else \<^bold>0))) ODE ))) {0..t}
{x. Predicates I Iy
(\<chi> i. dterm_sem I (if i = Ix then trm.Var Ix else \<^bold>0)
(mk_v I (oprod (OSing Ix ($f Ix (\<lambda>i. if i = Ix then trm.Var Ix else \<^bold>0)))ODE) \<nu> x))} \<and>
sol 0 = fst \<nu>) \<longrightarrow>
\<omega> \<in> fml_sem I (Pc Ix)"
let ?my\<omega> = "mk_v I (oprod (OSing Ix ($f Ix (\<lambda>i. if i = Ix then trm.Var Ix else \<^bold>0)))ODE) (ab,bb) (sol t)"
assume t:"0 \<le> t"
assume aaba:"(aa, ba) = mk_v I (oprod (OSing Ix ($f Ix (\<lambda>i. if i = Ix then trm.Var Ix else \<^bold>0)))ODE) (ab, bb) (sol t)"
assume sol:"(sol solves_ode (\<lambda>_. ODE_sem I (oprod (OSing Ix ($f Ix (\<lambda>i. if i = Ix then trm.Var Ix else \<^bold>0)))ODE))) {0..t}
{x. Predicates I Iy
(\<chi> i. dterm_sem I (if i = Ix then trm.Var Ix else \<^bold>0)
(mk_v I (oprod (OSing Ix ($f Ix (\<lambda>i. if i = Ix then trm.Var Ix else \<^bold>0)))ODE) (ab, bb) x))}"
assume sol0:"sol 0 = fst (ab, bb)"
assume acbc:"(ac, bc) =
repd (mk_v I (oprod (OSing Ix ($f Ix (\<lambda>i. if i = Ix then trm.Var Ix else \<^bold>0)))ODE) (ab, bb) (sol t)) Ix
(dterm_sem I ($f Ix (\<lambda>i. if i = Ix then trm.Var Ix else \<^bold>0))
(mk_v I (oprod (OSing Ix ($f Ix (\<lambda>i. if i = Ix then trm.Var Ix else \<^bold>0)))ODE) (ab, bb) (sol t)))"
have bigEx:"(\<exists>\<nu> sol t. ((ab, bb), ?my\<omega>) = (\<nu>, mk_v I (oprod (OSing Ix ($f Ix (\<lambda>i. if i = Ix then trm.Var Ix else \<^bold>0)))ODE) \<nu> (sol t)) \<and>
0 \<le> t \<and>
(sol solves_ode (\<lambda>_. ODE_sem I (oprod (OSing Ix ($f Ix (\<lambda>i. if i = Ix then trm.Var Ix else \<^bold>0)))ODE))) {0..t}
{x. Predicates I Iy
(\<chi> i. dterm_sem I (if i = Ix then trm.Var Ix else \<^bold>0)