Theory Coincidence
theory "Coincidence"
imports
Ordinary_Differential_Equations.ODE_Analysis
"Ids"
"Lib"
"Syntax"
"Denotational_Semantics"
"Frechet_Correctness"
"Static_Semantics"
begin
section ‹Coincidence Theorems and Corollaries›
text ‹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.
›
context ids begin
subsection ‹Term Coincidence Theorems›
lemma coincidence_sterm:"Vagree ν ν' (FVT θ) ⟹ sterm_sem I θ (fst ν) = sterm_sem I θ (fst ν')"
apply(induct "θ")
apply(auto simp add: Vagree_def)
by (meson rangeI)
lemma coincidence_sterm':"dfree θ ⟹ Vagree ν ν' (FVT θ) ⟹ Iagree I J {Inl x |x. x ∈ SIGT θ} ⟹ sterm_sem I θ (fst ν) = sterm_sem J θ (fst ν')"
proof (induction rule: dfree.induct)
case (dfree_Fun args i)
then show ?case
proof (auto)
assume free:"(⋀i. dfree (args i))"
and IH:"(⋀i. Vagree ν ν' (FVT (args i)) ⟹ Iagree I J {Inl x |x. x ∈ SIGT (args i)} ⟹ sterm_sem I (args i) (fst ν) = sterm_sem J (args i) (fst ν'))"
and VA:"Vagree ν ν' (⋃i. FVT (args i))"
and IA:"Iagree I J {Inl x |x. x = i ∨ (∃xa. x ∈ SIGT (args xa))}"
from IA have IAorig:"Iagree I J {Inl x |x. x ∈ SIGT (Function i args)}" by auto
from Iagree_Func[OF IAorig] have eqF:"Functions I i = Functions J i" by auto
have Vsubs:"⋀i. FVT (args i) ⊆ (⋃i. FVT (args i))" by auto
from VA
have VAs:"⋀i. Vagree ν ν' (FVT (args i))"
using agree_sub[OF Vsubs] by auto
have Isubs:"⋀j. {Inl x |x. x ∈ SIGT (args j)} ⊆ {Inl x |x. x ∈ SIGT (Function i args)}"
by auto
from IA
have IAs:"⋀i. Iagree I J {Inl x |x. x ∈ SIGT (args i)}"
using Iagree_sub[OF Isubs] by auto
show "Functions I i (χ i. sterm_sem I (args i) (fst ν)) = Functions J i (χ i. sterm_sem J (args i) (fst ν'))"
using IH[OF VAs IAs] eqF by auto
qed
next
case (dfree_Plus θ⇩1 θ⇩2)
then show ?case
proof (auto)
assume "dfree θ⇩1" "dfree θ⇩2"
and IH1:"(Vagree ν ν' (FVT θ⇩1) ⟹ Iagree I J {Inl x |x. x ∈ SIGT θ⇩1} ⟹ sterm_sem I θ⇩1 (fst ν) = sterm_sem J θ⇩1 (fst ν'))"
and IH2:"(Vagree ν ν' (FVT θ⇩2) ⟹ Iagree I J {Inl x |x. x ∈ SIGT θ⇩2} ⟹ sterm_sem I θ⇩2 (fst ν) = sterm_sem J θ⇩2 (fst ν'))"
and VA:"Vagree ν ν' (FVT θ⇩1 ∪ FVT θ⇩2)"
and IA:"Iagree I J {Inl x |x. x ∈ SIGT θ⇩1 ∨ x ∈ SIGT θ⇩2}"
from VA
have VAs:"Vagree ν ν' (FVT θ⇩1)" "Vagree ν ν' (FVT θ⇩2)"
unfolding Vagree_def by auto
have Isubs:"{Inl x |x. x ∈ SIGT θ⇩1} ⊆ {Inl x |x. x ∈ SIGT (Plus θ⇩1 θ⇩2)}"
"{Inl x |x. x ∈ SIGT θ⇩2} ⊆ {Inl x |x. x ∈ SIGT (Plus θ⇩1 θ⇩2)}"
by auto
from IA
have IAs:"Iagree I J {Inl x |x. x ∈ SIGT θ⇩1}"
"Iagree I J {Inl x |x. x ∈ SIGT θ⇩2}"
using Iagree_sub[OF Isubs(1)] Iagree_sub[OF Isubs(2)] by auto
show "sterm_sem I θ⇩1 (fst ν) + sterm_sem I θ⇩2 (fst ν) = sterm_sem J θ⇩1 (fst ν') + sterm_sem J θ⇩2 (fst ν')"
using IH1[OF VAs(1) IAs(1)] IH2[OF VAs(2) IAs(2)] by auto
qed
next
case (dfree_Times θ⇩1 θ⇩2)
then show ?case
proof (auto)
assume "dfree θ⇩1" "dfree θ⇩2"
and IH1:"(Vagree ν ν' (FVT θ⇩1) ⟹ Iagree I J {Inl x |x. x ∈ SIGT θ⇩1} ⟹ sterm_sem I θ⇩1 (fst ν) = sterm_sem J θ⇩1 (fst ν'))"
and IH2:"(Vagree ν ν' (FVT θ⇩2) ⟹ Iagree I J {Inl x |x. x ∈ SIGT θ⇩2} ⟹ sterm_sem I θ⇩2 (fst ν) = sterm_sem J θ⇩2 (fst ν'))"
and VA:"Vagree ν ν' (FVT θ⇩1 ∪ FVT θ⇩2)"
and IA:"Iagree I J {Inl x |x. x ∈ SIGT θ⇩1 ∨ x ∈ SIGT θ⇩2}"
from VA
have VAs:"Vagree ν ν' (FVT θ⇩1)" "Vagree ν ν' (FVT θ⇩2)"
unfolding Vagree_def by auto
have Isubs:"{Inl x |x. x ∈ SIGT θ⇩1} ⊆ {Inl x |x. x ∈ SIGT (Times θ⇩1 θ⇩2)}"
"{Inl x |x. x ∈ SIGT θ⇩2} ⊆ {Inl x |x. x ∈ SIGT (Times θ⇩1 θ⇩2)}"
by auto
from IA
have IAs:"Iagree I J {Inl x |x. x ∈ SIGT θ⇩1}"
"Iagree I J {Inl x |x. x ∈ SIGT θ⇩2}"
using Iagree_sub[OF Isubs(1)] Iagree_sub[OF Isubs(2)] by auto
show "sterm_sem I θ⇩1 (fst ν) * sterm_sem I θ⇩2 (fst ν) = sterm_sem J θ⇩1 (fst ν') * sterm_sem J θ⇩2 (fst ν')"
using IH1[OF VAs(1) IAs(1)] IH2[OF VAs(2) IAs(2)] by auto
qed
qed (unfold Vagree_def Iagree_def, auto)
lemma sum_unique_nonzero:
fixes i::"'sv::finite" and f::"'sv ⇒ real"
assumes restZero:"⋀j. j∈(UNIV::'sv set) ⟹ j ≠ i ⟹ f j = 0"
shows "(∑j∈(UNIV::'sv set). f j) = f i"
proof -
have "(∑j∈(UNIV::'sv set). f j) = (∑j∈{i}. f j)"
using restZero by (intro sum.mono_neutral_cong_right) auto
then show ?thesis
by simp
qed
lemma coincidence_frechet :
fixes I :: "('a::finite, 'b::finite, 'c::finite) interp" and ν :: "'c state" and ν'::"'c state"
shows "dfree θ ⟹ Vagree ν ν' (FVDiff θ) ⟹ frechet I θ (fst ν) (snd ν) = frechet I θ (fst ν') (snd ν')"
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 args var)
assume free:"(⋀i. dfree (args i))"
assume IH:"(⋀i. Vagree ν ν' (FVDiff (args i)) ⟹ frechet I (args i) (fst ν) (snd ν) = frechet I (args i) (fst ν') (snd ν'))"
have frees:"(⋀i. dfree (args i))" using free by (auto simp add: rangeI)
assume agree:"Vagree ν ν' (FVDiff ($f var args))"
have agrees:"⋀i. Vagree ν ν' (FVDiff (args i))" using agree agree_func by metis
have agrees':"⋀i. Vagree ν ν' (FVT (args i))"
subgoal for i
using agrees[of i] FVDiff_sub[of "args i"] unfolding Vagree_def by blast
done
have sterms:"⋀i. sterm_sem I (args i) (fst ν) = sterm_sem I (args i) (fst ν')"
by (rule coincidence_sterm[of "ν" "ν'", OF agrees'])
have frechets:"⋀i. frechet I (args i) (fst ν) (snd ν) = frechet I (args i) (fst ν') (snd ν')" using IH agrees frees rangeI by blast
show "?case"
using agrees sterms frechets by (auto)
next
case (dfree_Plus t1 t2)
assume dfree1:"dfree t1"
assume IH1:"(Vagree ν ν' (FVDiff t1) ⟹ frechet I t1 (fst ν) (snd ν) = frechet I t1 (fst ν') (snd ν'))"
assume dfree2:"dfree t2"
assume IH2:"(Vagree ν ν' (FVDiff t2) ⟹ frechet I t2 (fst ν) (snd ν) = frechet I t2 (fst ν') (snd ν'))"
assume agree:"Vagree ν ν' (FVDiff (Plus t1 t2))"
have agree1:"Vagree ν ν' (FVDiff t1)" using agree agree_plus1 by (blast)
have agree2:"Vagree ν ν' (FVDiff t2)" using agree agree_plus2 by (blast)
have IH1':"(frechet I t1 (fst ν) (snd ν) = frechet I t1 (fst ν') (snd ν'))"
using IH1 agree1 by (auto)
have IH2':"(frechet I t2 (fst ν) (snd ν) = frechet I t2 (fst ν') (snd ν'))"
using IH2 agree2 by (auto)
show "?case"
by (metis FVT.simps(4) IH1' IH2' UnCI Vagree_def coincidence_sterm frechet.simps(3) mem_Collect_eq)
next
case (dfree_Times t1 t2)
assume dfree1:"dfree t1"
assume IH1:"(Vagree ν ν' (FVDiff t1) ⟹ frechet I t1 (fst ν) (snd ν) = frechet I t1 (fst ν') (snd ν'))"
assume dfree2:"dfree t2"
assume IH2:"(Vagree ν ν' (FVDiff t2) ⟹ frechet I t2 (fst ν) (snd ν) = frechet I t2 (fst ν') (snd ν'))"
assume agree:"Vagree ν ν' (FVDiff (Times t1 t2))"
have agree1:"Vagree ν ν' (FVDiff t1)" using agree agree_times1 by blast
have agree2:"Vagree ν ν' (FVDiff t2)" using agree agree_times2 by blast
have agree1':"Vagree ν ν' (FVT t1)"
using agree1 apply(auto simp add: Vagree_def)
using primify_contains by blast+
have agree2':"Vagree ν ν' (FVT t2)"
using agree2 apply(auto simp add: Vagree_def)
using primify_contains by blast+
have IH1':"(frechet I t1 (fst ν) (snd ν) = frechet I t1 (fst ν') (snd ν'))"
using IH1 agree1 by (auto)
have IH2':"(frechet I t2 (fst ν) (snd ν) = frechet I t2 (fst ν') (snd ν'))"
using IH2 agree2 by (auto)
have almost:"Vagree ν ν' (FVT (Times t1 t2)) ⟹ frechet I (Times t1 t2) (fst ν) (snd ν) = frechet I (Times t1 t2) (fst ν') (snd ν')"
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 :: "('a::finite, 'b::finite, 'c::finite) interp" and ν :: "'c state" and ν'::"'c state"
shows "dfree θ ⟹ Vagree ν ν' (FVDiff θ) ⟹ Iagree I J {Inl x | x. x ∈ (SIGT θ)} ⟹ frechet I θ (fst ν) (snd ν) = frechet J θ (fst ν') (snd ν')"
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 args var)
assume free:"(⋀i. dfree (args i))"
assume IH:"(⋀i. Vagree ν ν' (FVDiff (args i)) ⟹ Iagree I J {Inl x |x. x ∈ SIGT (args i)} ⟹ frechet I (args i) (fst ν) (snd ν) = frechet J (args i) (fst ν') (snd ν'))"
have frees:"(⋀i. dfree (args i))" using free by (auto simp add: rangeI)
assume agree:"Vagree ν ν' (FVDiff ($f var args))"
assume IA:"Iagree I J {Inl x |x. x ∈ SIGT ($f var args)}"
have agrees:"⋀i. Vagree ν ν' (FVDiff (args i))" using agree agree_func by metis
then have agrees':"⋀i. Vagree ν ν' (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:"⋀i.{Inl x |x. x ∈ SIGT (args i)} ⊆ {Inl x |x. x ∈ SIGT ($f var args)}"
by auto
from IA have IAs:"⋀i. Iagree I J {Inl x |x. x ∈ SIGT (args i)}"
using Iagree_sub[OF subs] by auto
have sterms:"⋀i. sterm_sem I (args i) (fst ν) = sterm_sem J (args i) (fst ν')"
subgoal for i
using frees agrees' coincidence_sterm'[of "args i" ν ν' I J] IAs
by (auto)
done
have frechets:"⋀i. frechet I (args i) (fst ν) (snd ν) = frechet J (args i) (fst ν') (snd ν')"
using IH[OF agrees IAs] agrees frees rangeI by blast
show "?case"
using agrees agrees' sterms frechets fEq by auto
next
case (dfree_Plus t1 t2)
assume dfree1:"dfree t1"
assume dfree2:"dfree t2"
assume IH1:"(Vagree ν ν' (FVDiff t1) ⟹ Iagree I J {Inl x |x. x ∈ SIGT t1} ⟹ frechet I t1 (fst ν) (snd ν) = frechet J t1 (fst ν') (snd ν'))"
assume IH2:"(Vagree ν ν' (FVDiff t2) ⟹ Iagree I J {Inl x |x. x ∈ SIGT t2} ⟹ frechet I t2 (fst ν) (snd ν) = frechet J t2 (fst ν') (snd ν'))"
assume agree:"Vagree ν ν' (FVDiff (Plus t1 t2))"
assume IA:"Iagree I J {Inl x |x. x ∈ SIGT (Plus t1 t2)}"
have subs:"{Inl x |x. x ∈ SIGT t1} ⊆ {Inl x |x. x ∈ SIGT (Plus t1 t2)}" "{Inl x |x. x ∈ SIGT t2} ⊆ {Inl x |x. x ∈ SIGT (Plus t1 t2)}"
by auto
from IA
have IA1:"Iagree I J {Inl x |x. x ∈ SIGT t1}"
and IA2:"Iagree I J {Inl x |x. x ∈ SIGT t2}"
using Iagree_sub[OF subs(1)] Iagree_sub[OF subs(2)] by auto
have agree1:"Vagree ν ν' (FVDiff t1)" using agree agree_plus1 by (blast)
have agree2:"Vagree ν ν' (FVDiff t2)" using agree agree_plus2 by (blast)
have agree1':"Vagree ν ν' (FVT t1)" using agree1 primify_contains by (auto simp add: Vagree_def, metis)
have agree2':"Vagree ν ν' (FVT t2)" using agree2 primify_contains by (auto simp add: Vagree_def, metis)
have IH1':"(frechet I t1 (fst ν) (snd ν) = frechet J t1 (fst ν') (snd ν'))"
using IH1 agree1 IA1 by (auto)
have IH2':"(frechet I t2 (fst ν) (snd ν) = frechet J t2 (fst ν') (snd ν'))"
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 ν ν' (FVDiff t1) ⟹ Iagree I J {Inl x |x. x ∈ SIGT t1} ⟹ frechet I t1 (fst ν) (snd ν) = frechet J t1 (fst ν') (snd ν'))"
assume IH2:"(Vagree ν ν' (FVDiff t2) ⟹ Iagree I J {Inl x |x. x ∈ SIGT t2} ⟹ frechet I t2 (fst ν) (snd ν) = frechet J t2 (fst ν') (snd ν'))"
assume agree:"Vagree ν ν' (FVDiff (Times t1 t2))"
assume IA:"Iagree I J {Inl x |x. x ∈ SIGT (Times t1 t2)}"
have subs:"{Inl x |x. x ∈ SIGT t1} ⊆ {Inl x |x. x ∈ SIGT (Times t1 t2)}" "{Inl x |x. x ∈ SIGT t2} ⊆ {Inl x |x. x ∈ SIGT (Times t1 t2)}"
by auto
from IA
have IA1:"Iagree I J {Inl x |x. x ∈ SIGT t1}"
and IA2:"Iagree I J {Inl x |x. x ∈ SIGT t2}"
using Iagree_sub[OF subs(1)] Iagree_sub[OF subs(2)] by auto
have agree1:"Vagree ν ν' (FVDiff t1)" using agree agree_times1 by (blast)
then have agree1':"Vagree ν ν' (FVT t1)"
using agree1 primify_contains by (auto simp add: Vagree_def, metis)
have agree2:"Vagree ν ν' (FVDiff t2)" using agree agree_times2 by (blast)
then have agree2':"Vagree ν ν' (FVT t2)"
using agree2 primify_contains by (auto simp add: Vagree_def, metis)
have IH1':"(frechet I t1 (fst ν) (snd ν) = frechet J t1 (fst ν') (snd ν'))"
using IH1 agree1 IA1 by (auto)
have IH2':"(frechet I t2 (fst ν) (snd ν) = frechet J t2 (fst ν') (snd ν'))"
using IH2 agree2 IA2 by (auto)
note co1 = coincidence_sterm'[of "t1" ν ν' I J] and co2 = coincidence_sterm'[of "t2" ν ν' 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 :: "('a::finite, 'b::finite, 'c::finite) interp" and ν :: "'c state" and ν'::"'c state"
shows "dsafe θ ⟹ Vagree ν ν' (FVT θ) ⟹ dterm_sem I θ ν = dterm_sem I θ ν'"
proof (induction rule: dsafe.induct)
case (dsafe_Fun args f)
assume safe:"(⋀i. dsafe (args i))"
assume IH:"⋀i. Vagree ν ν' (FVT (args i)) ⟹ dterm_sem I (args i) ν = dterm_sem I (args i) ν'"
assume agree:"Vagree ν ν' (FVT ($f f args))"
then have "⋀i. Vagree ν ν' (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 :: "('a::finite, 'b::finite, 'c::finite) interp" and ν :: "'c::finite state" and ν'::"'c::finite state"
shows "dsafe θ ⟹ Vagree ν ν' (FVT θ) ⟹ Iagree I J {Inl x | x. x ∈ (SIGT θ)} ⟹ dterm_sem I θ ν = dterm_sem J θ ν'"
proof (induction rule: dsafe.induct)
case (dsafe_Fun args f) then
have safe:"(⋀i. dsafe (args i))"
and IH:"⋀i. Vagree ν ν' (FVT (args i)) ⟹ Iagree I J {Inl x | x. x ∈ (SIGT (args i))} ⟹ dterm_sem I (args i) ν = dterm_sem J (args i) ν'"
and agree:"Vagree ν ν' (FVT ($f f args))"
and IA:"Iagree I J {Inl x |x. x ∈ SIGT ($f f args)}"
by auto
have subs:"⋀i. {Inl x |x. x ∈ SIGT (args i)} ⊆ {Inl x |x. x ∈ SIGT ($f f args)}" by auto
from IA have IAs:
"⋀i. Iagree I J {Inl x |x. x ∈ SIGT (args i)}"
using Iagree_sub [OF subs IA] by auto
from agree have agrees:"⋀i. Vagree ν ν' (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_Plus θ⇩1 θ⇩2) then
have safe:"dsafe θ⇩1" "dsafe θ⇩2"
and IH1:"Vagree ν ν' (FVT θ⇩1) ⟹ Iagree I J {Inl x |x. x ∈ SIGT θ⇩1} ⟹ dterm_sem I θ⇩1 ν = dterm_sem J θ⇩1 ν'"
and IH2:"Vagree ν ν' (FVT θ⇩2) ⟹ Iagree I J {Inl x |x. x ∈ SIGT θ⇩2} ⟹ dterm_sem I θ⇩2 ν = dterm_sem J θ⇩2 ν'"
and VA:"Vagree ν ν' (FVT (Plus θ⇩1 θ⇩2))"
and IA:"Iagree I J {Inl x |x. x ∈ SIGT (Plus θ⇩1 θ⇩2)}"
by auto
from VA have VA1:"Vagree ν ν' (FVT θ⇩1)" and VA2:"Vagree ν ν' (FVT θ⇩2)"
unfolding Vagree_def by auto
have subs:"{Inl x |x. x ∈ SIGT θ⇩1} ⊆ {Inl x |x. x ∈ SIGT (Plus θ⇩1 θ⇩2)}"
"{Inl x |x. x ∈ SIGT θ⇩2} ⊆ {Inl x |x. x ∈ SIGT (Plus θ⇩1 θ⇩2)}"by auto
from IA have IA1:"Iagree I J {Inl x |x. x ∈ SIGT θ⇩1}" and IA2:"Iagree I J {Inl x |x. x ∈ SIGT θ⇩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 θ⇩1 θ⇩2) then
have safe:"dsafe θ⇩1" "dsafe θ⇩2"
and IH1:"Vagree ν ν' (FVT θ⇩1) ⟹ Iagree I J {Inl x |x. x ∈ SIGT θ⇩1} ⟹ dterm_sem I θ⇩1 ν = dterm_sem J θ⇩1 ν'"
and IH2:"Vagree ν ν' (FVT θ⇩2) ⟹ Iagree I J {Inl x |x. x ∈ SIGT θ⇩2} ⟹ dterm_sem I θ⇩2 ν = dterm_sem J θ⇩2 ν'"
and VA:"Vagree ν ν' (FVT (Times θ⇩1 θ⇩2))"
and IA:"Iagree I J {Inl x |x. x ∈ SIGT (Times θ⇩1 θ⇩2)}"
by auto
from VA have VA1:"Vagree ν ν' (FVT θ⇩1)" and VA2:"Vagree ν ν' (FVT θ⇩2)"
unfolding Vagree_def by auto
have subs:"{Inl x |x. x ∈ SIGT θ⇩1} ⊆ {Inl x |x. x ∈ SIGT (Times θ⇩1 θ⇩2)}"
"{Inl x |x. x ∈ SIGT θ⇩2} ⊆ {Inl x |x. x ∈ SIGT (Times θ⇩1 θ⇩2)}"by auto
from IA have IA1:"Iagree I J {Inl x |x. x ∈ SIGT θ⇩1}" and IA2:"Iagree I J {Inl x |x. x ∈ SIGT θ⇩2}"
using Iagree_sub subs by auto
then show ?case
using IH1[OF VA1 IA1] IH2[OF VA2 IA2] by auto
qed (auto simp: Vagree_def directional_derivative_def coincidence_frechet')
subsection ‹ODE Coincidence Theorems›
lemma coincidence_ode:
fixes I J :: "('a::finite, 'b::finite, 'c::finite) interp" and ν :: "'c::finite state" and ν'::"'c::finite state"
shows "osafe ODE ⟹
Vagree ν ν' (Inl ` FVO ODE) ⟹
Iagree I J ({Inl x | x. Inl x ∈ SIGO ODE} ∪ {Inr (Inr x) | x. Inr x ∈ SIGO ODE}) ⟹
ODE_sem I ODE (fst ν) = ODE_sem J ODE (fst ν')"
proof (induction rule: osafe.induct)
case (osafe_Var c)
then show ?case
proof (auto)
assume VA:"Vagree ν ν' (range Inl)"
have eqV:"(fst ν) = (fst ν')"
using agree_UNIV_fst[OF VA] by auto
assume IA:"Iagree I J {Inr (Inr c)}"
have eqIJ:"ODEs I c = ODEs J c"
using Iagree_ODE[OF IA] by auto
show "ODEs I c (fst ν) = ODEs J c (fst ν')"
by (auto simp add: eqV eqIJ)
qed
next
case (osafe_Sing θ x)
then show ?case
proof (auto)
assume free:"dfree θ"
and VA:"Vagree ν ν' (insert (Inl x) (Inl ` {x. Inl x ∈ FVT θ}))"
and IA:"Iagree I J {Inl x |x. x ∈ SIGT θ}"
from VA have VA':"Vagree ν ν' {Inl x | x. Inl x ∈ FVT θ}" unfolding Vagree_def by auto
have agree_Lem:"⋀θ. dfree θ ⟹ Vagree ν ν' {Inl x | x. Inl x ∈ FVT θ} ⟹ Vagree ν ν' (FVT θ)"
subgoal for θ
apply(induction rule: dfree.induct)
by(auto simp add: Vagree_def)
done
have trm:"sterm_sem I θ (fst ν) = sterm_sem J θ (fst ν')"
using coincidence_sterm' free VA' IA agree_Lem[of θ, OF free] by blast
show "(λi. if i = x then sterm_sem I θ (fst ν) else 0) =
(λi. if i = x then sterm_sem J θ (fst ν') 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 ∩ ODE_dom ODE2 = {}"
and IH1:"Vagree ν ν' (Inl ` FVO ODE1) ⟹
Iagree I J ({Inl x |x. Inl x ∈ SIGO ODE1} ∪ {Inr (Inr x) |x. Inr x ∈ SIGO ODE1}) ⟹ ODE_sem I ODE1 (fst ν) = ODE_sem J ODE1 (fst ν')"
and IH2:"Vagree ν ν' (Inl ` FVO ODE2) ⟹
Iagree I J ({Inl x |x. Inl x ∈ SIGO ODE2} ∪ {Inr (Inr x) |x. Inr x ∈ SIGO ODE2}) ⟹ ODE_sem I ODE2 (fst ν) = ODE_sem J ODE2 (fst ν')"
and VA:"Vagree ν ν' (Inl ` (FVO ODE1 ∪ FVO ODE2))"
and IA:"Iagree I J ({Inl x |x. Inl x ∈ SIGO ODE1 ∨ Inl x ∈ SIGO ODE2} ∪ {Inr (Inr x) |x. Inr x ∈ SIGO ODE1 ∨ Inr x ∈ SIGO ODE2})"
let ?IA = "({Inl x |x. Inl x ∈ SIGO ODE1 ∨ Inl x ∈ SIGO ODE2} ∪ {Inr (Inr x) |x. Inr x ∈ SIGO ODE1 ∨ Inr x ∈ SIGO ODE2})"
have FVsubs:
"Inl ` FVO ODE2 ⊆ Inl ` (FVO ODE1 ∪ FVO ODE2)"
"Inl ` FVO ODE1 ⊆ Inl ` (FVO ODE1 ∪ FVO ODE2)"
by auto
from VA
have VA1:"Vagree ν ν' (Inl ` FVO ODE1)"
and VA2:"Vagree ν ν' (Inl ` FVO ODE2)"
using agree_sub[OF FVsubs(1)] agree_sub[OF FVsubs(2)]
by (auto)
have SIGsubs:
"({Inl x |x. Inl x ∈ SIGO ODE1} ∪ {Inr (Inr x) |x. Inr x ∈ SIGO ODE1}) ⊆ ?IA"
"({Inl x |x. Inl x ∈ SIGO ODE2} ∪ {Inr (Inr x) |x. Inr x ∈ SIGO ODE2}) ⊆ ?IA"
by auto
from IA
have IA1:"Iagree I J ({Inl x |x. Inl x ∈ SIGO ODE1} ∪ {Inr (Inr x) |x. Inr x ∈ SIGO ODE1})"
and IA2:"Iagree I J ({Inl x |x. Inl x ∈ SIGO ODE2} ∪ {Inr (Inr x) |x. Inr x ∈ SIGO ODE2})"
using Iagree_sub[OF SIGsubs(1)] Iagree_sub[OF SIGsubs(2)] by auto
show "ODE_sem I ODE1 (fst ν) + ODE_sem I ODE2 (fst ν) = ODE_sem J ODE1 (fst ν') + ODE_sem J ODE2 (fst ν')"
using IH1[OF VA1 IA1] IH2[OF VA2 IA2] by auto
qed
qed
lemma coincidence_ode':
fixes I J :: "('a::finite, 'b::finite, 'c::finite) interp" and ν :: "'c simple_state" and ν'::"'c simple_state"
shows "osafe ODE ⟹
VSagree ν ν' (FVO ODE) ⟹
Iagree I J ({Inl x | x. Inl x ∈ SIGO ODE} ∪ {Inr (Inr x) | x. Inr x ∈ SIGO ODE}) ⟹
ODE_sem I ODE ν = ODE_sem J ODE ν'"
using coincidence_ode[of ODE "(ν, χ i. 0)" "(ν', χ i. 0)" I J]
apply(auto)
unfolding VSagree_def Vagree_def apply auto
done
lemma alt_sem_lemma:"⋀ I::('a::finite,'b::finite,'c::finite) interp. ⋀ ODE::('a::finite,'c::finite) ODE. ⋀sol. ⋀t::real. ⋀ ab. osafe ODE ⟹
ODE_sem I ODE (sol t) = ODE_sem I ODE (χ i. if i ∈ FVO ODE then sol t $ i else ab $ i)"
proof -
fix I::"('a,'b,'c) interp"
and ODE::"('a,'c) ODE"
and sol
and t::real
and ab
assume safe:"osafe ODE"
have VA:"VSagree (sol t) (χ i. if i ∈ 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 ∈ SIGO ODE} ∪ {Inr (Inr x) | x. Inr x ∈ SIGO ODE})" unfolding Iagree_def by auto
show "ODE_sem I ODE (sol t) = ODE_sem I ODE (χ i. if i ∈ FVO ODE then sol t $ i else ab $ i)"
using coincidence_ode'[OF safe VA IA] by auto
qed
lemma bvo_to_fvo:"Inl x ∈ BVO ODE ⟹ x ∈ FVO ODE"
proof (induction ODE)
qed auto
lemma ode_to_fvo:"x ∈ ODE_vars I ODE ⟹ x ∈ FVO ODE"
proof (induction ODE)
qed auto
definition coincide_hp :: "('a::finite, 'b::finite, 'c::finite) hp ⇒ ('a::finite, 'b::finite, 'c::finite) interp ⇒ ('a::finite, 'b::finite, 'c::finite) interp ⇒ bool"
where "coincide_hp α I J ⟷ (∀ ν ν' μ V. Iagree I J (SIGP α) ⟶ Vagree ν ν' V ⟶ V ⊇ (FVP α) ⟶ (ν, μ) ∈ prog_sem I α ⟶ (∃μ'. (ν', μ') ∈ prog_sem J α ∧ Vagree μ μ' (MBV α ∪ V)))"
definition ode_sem_equiv ::"('a::finite, 'b::finite, 'c::finite) hp ⇒ ('a::finite, 'b::finite, 'c::finite) interp ⇒ bool"
where "ode_sem_equiv α I ⟷
(∀ODE::('a::finite,'c::finite) ODE. ∀φ::('a::finite,'b::finite,'c::finite)formula. osafe ODE ⟶ fsafe φ ⟶
(α = EvolveODE ODE φ) ⟶
{(ν, mk_v I ODE ν (sol t)) | ν sol t.
t ≥ 0 ∧
(sol solves_ode (λ_. ODE_sem I ODE)) {0..t} {x. mk_v I ODE ν x ∈ fml_sem I φ} ∧
VSagree (sol 0) (fst ν) {x | x. Inl x ∈ FVP (EvolveODE ODE φ)}} =
{(ν, mk_v I ODE ν (sol t)) | ν sol t.
t ≥ 0 ∧
(sol solves_ode (λ_. ODE_sem I ODE)) {0..t} {x. mk_v I ODE ν x ∈ fml_sem I φ} ∧
sol 0 = fst ν})"
definition coincide_hp' :: "('a::finite, 'b::finite, 'c::finite) hp ⇒ bool"
where "coincide_hp' α ⟷ (∀ I J. coincide_hp α I J ∧ ode_sem_equiv α I)"
definition coincide_fml :: "('a::finite, 'b::finite, 'c::finite) formula ⇒ bool"
where "coincide_fml φ ⟷ (∀ ν ν' I J . Iagree I J (SIGF φ) ⟶ Vagree ν ν' (FVF φ) ⟶ ν ∈ fml_sem I φ ⟷ ν' ∈ fml_sem J φ)"
lemma coinc_fml [simp]: "coincide_fml φ = (∀ ν ν' I J. Iagree I J (SIGF φ) ⟶ Vagree ν ν' (FVF φ) ⟶ ν ∈ fml_sem I φ ⟷ ν' ∈ fml_sem J φ)"
unfolding coincide_fml_def by auto
subsection ‹Coincidence Theorems for Programs and Formulas›
lemma coincidence_hp_fml:
fixes α::"('a::finite, 'b::finite, 'c::finite) hp"
fixes φ::"('a::finite, 'b::finite, 'c::finite) formula"
shows "(hpsafe α ⟶ coincide_hp' α) ∧ (fsafe φ ⟶ coincide_fml φ)"
proof (induction rule: hpsafe_fsafe.induct)
case (hpsafe_Pvar x)
thus "?case"
apply(unfold coincide_hp'_def | rule allI | rule conjI)+
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:"⋀y. y ∈ Programs I x ⟷ y ∈ Programs J x" using Iagree_Prog[OF IA] by auto
assume agree:"Vagree (a, b) (aa, ba) V"
and sub:"UNIV ⊆ V"
and sem:"((a, b), ab, bb) ∈ 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)) ∈ Programs I x"
using sem by auto
have triv_sub:"V ⊆ 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 "∃a b. ((aa, ba), a, b) ∈ Programs J x ∧ 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 :: "('a::finite,'b::finite,'c::finite) interp"
and ν1 ν2 ν'1 ν'2 μ1 μ2 V
assume safe:"dsafe e"
and IA:"Iagree I J (SIGP (x := e))"
and VA:"Vagree (ν1, ν2) (ν'1, ν'2) V"
and sub:"FVP (x := e) ⊆ V"
and sem:"((ν1, ν2), (μ1, μ2)) ∈ prog_sem I (x := e)"
from VA have VA':"Vagree (ν1, ν2) (ν'1, ν'2) (FVT e)" unfolding FVP.simps Vagree_def using sub by auto
have Ssub:"{Inl x | x. x ∈ SIGT e} ⊆ (SIGP (x := e))" by auto
from IA have IA':"Iagree I J {Inl x | x. x ∈ SIGT e}" using Ssub unfolding SIGP.simps by auto
have "((ν1, ν2), repv (ν1, ν2) x (dterm_sem I e (ν1, ν2))) ∈ prog_sem I (x := e)" by auto
then have sem':"((ν'1, ν'2), repv (ν'1, ν'2) x (dterm_sem J e (ν'1, ν'2))) ∈ prog_sem J (x := e)"
using coincidence_dterm' safe VA' IA' by auto
from sem have eq:"(μ1, μ2) = (repv (ν1, ν2) x (dterm_sem I e (ν1, ν2)))" by auto
have VA'':"Vagree (μ1, μ2) (repv (ν'1, ν'2) x (dterm_sem J e (ν'1, ν'2))) (MBV (x := e) ∪ V)"
using coincidence_dterm'[of e "(ν1,ν2)" "(ν'1,ν'2)" I J] safe VA' IA' eq agree_refl VA unfolding MBV.simps Vagree_def
by auto
show "∃μ'. ((ν'1, ν'2), μ') ∈ prog_sem J (x := e) ∧ Vagree (μ1, μ2) μ' (MBV (x := e) ∪ V)"
using VA'' sem' by blast
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::"('a,'b,'c) interp"
and ν ν' μ V
assume safe:"dsafe e"
and IA:"Iagree I J (SIGP (DiffAssign x e))"
and VA:"Vagree ν ν' V"
and sub:"FVP (DiffAssign x e) ⊆ V"
and sem:"(ν, μ) ∈ prog_sem I (DiffAssign x e)"
from VA have VA':"Vagree ν ν' (FVT e)" unfolding FVP.simps Vagree_def using sub by auto
have Ssub:"{Inl x | x. x ∈ SIGT e} ⊆ (SIGP (DiffAssign x e))" by auto
from IA have IA':"Iagree I J {Inl x | x. x ∈ SIGT e}" using Ssub unfolding SIGP.simps by auto
have "(ν, repv ν x (dterm_sem I e ν)) ∈ prog_sem I (x := e)" by auto
then have sem':"(ν', repd ν' x (dterm_sem J e ν')) ∈ prog_sem J (DiffAssign x e)"
using coincidence_dterm' safe VA' IA' by auto
from sem have eq:"μ = (repd ν x (dterm_sem I e ν))" by auto
have VA':"Vagree μ (repd ν' x (dterm_sem J e ν')) (MBV (DiffAssign x e) ∪ V)"
using coincidence_dterm'[OF safe VA', of I J, OF IA'] eq agree_refl VA unfolding MBV.simps Vagree_def
by auto
show "∃μ'. (ν', μ') ∈ prog_sem J (DiffAssign x e) ∧ Vagree μ μ' (MBV (DiffAssign x e) ∪ 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::"('a,'b,'c) interp" and ν ν' ω ω' ::"'c simple_state"
and V
assume safe:"fsafe P"
assume "∀a b aa ba I J. (Iagree I J (SIGF P) ⟶ Vagree (a, b) (aa, ba) (FVF P) ⟶ ((a, b) ∈ fml_sem I P) = ((aa, ba) ∈ fml_sem J P))"
hence IH:"Iagree I J (SIGF P) ⟹ Vagree (ν, ν') (ω, ω') (FVF P) ⟹ ((ν, ν') ∈ fml_sem I P) = ((ω, ω') ∈ fml_sem J P)"
by auto
assume IA:"Iagree I J (SIGF P)"
assume VA:"Vagree (ν, ν') (ω, ω') V"
assume sub:"FVF P ⊆ V"
hence VA':"Vagree (ν, ν') (ω, ω') (FVF P)" using agree_supset VA by auto
assume sem:"(ν, ν') ∈ fml_sem I P"
show "(ω, ω') ∈ 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:"⋀ν ν' I J. Iagree I J (SIGF P) ⟹ Vagree ν ν' (FVF P) ⟹ (ν ∈ fml_sem I P) = (ν' ∈ fml_sem J P)"
unfolding coincide_fml_def by auto
have equiv:"⋀I. ode_sem_equiv (EvolveODE ODE P) I"
subgoal for I
apply(unfold ode_sem_equiv_def)
apply(rule allI)+
subgoal for ODE φ
apply(rule impI)+
apply(auto)
subgoal for aa ba ab bb sol t
apply(rule exI[where x="(λt. χ i. if i ∈ 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)" "(χ i. if i ∈ 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)
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)" "(χ i. if i ∈ FVO ODE then sol t $ i else ab $ i)"]
mk_v_agree[of I ODE "(χ i. if i ∈ FVO ODE then sol 0 $ i else ab $ i, bb)" "(χ i. if i ∈ FVO ODE then sol t $ i else ab $ i)"]
unfolding Vagree_def VSagree_def
apply(auto)
subgoal for i
apply(cases "Inl i ∈ BVO ODE")
using bvo_to_fvo[of i ODE] apply (metis (no_types, lifting))
apply(erule allE[where x=i])+
using Inl_Inr_False imageE ode_to_fvo
proof -
assume a1: "(aa, ba) = mk_v I ODE (ab, bb) (sol t)"
assume a2: "(Inl i ∈ BVO ODE ⟶ sol 0 $ i = ab $ i) ∧ ( Inl i ∈ Inl ` FVO ODE ⟶ sol 0 $ i = ab $ i) ∧ (Inl i ∈ FVF φ ⟶ sol 0 $ i = ab $ i)"
assume a3: "(Inl i::'c + 'c) ∉ Inl ` ODE_vars I ODE ∧ Inl i ∉ Inr ` ODE_vars I ODE ⟶ fst (mk_v I ODE (ab, bb) (sol t)) $ i = ab $ i"
assume a4: "(Inl i::'c + 'c) ∉ Inl ` ODE_vars I ODE ∧ Inl i ∉ Inr ` ODE_vars I ODE ⟶ fst (mk_v I ODE (χ i. if i ∈ FVO ODE then sol 0 $ i else ab $ i, bb) (χ i. if i ∈ FVO ODE then sol t $ i else ab $ i)) $ i = (if i ∈ FVO ODE then sol 0 $ i else ab $ i)"
assume a5: "((Inl i::'c + 'c) ∈ Inl ` ODE_vars I ODE ⟶ fst (mk_v I ODE (ab, bb) (sol t)) $ i = sol t $ i) ∧ (Inl i ∈ Inr ` ODE_vars I ODE ⟶ fst (mk_v I ODE (ab, bb) (sol t)) $ i = sol t $ i)"
assume a6: "((Inl i::'c + 'c) ∈ Inl ` ODE_vars I ODE ⟶ fst (mk_v I ODE (χ i. if i ∈ FVO ODE then sol 0 $ i else ab $ i, bb) (χ i. if i ∈ FVO ODE then sol t $ i else ab $ i)) $ i = (if i ∈ FVO ODE then sol t $ i else ab $ i)) ∧ (Inl i ∈ Inr ` ODE_vars I ODE ⟶ fst (mk_v I ODE (χ i. if i ∈ FVO ODE then sol 0 $ i else ab $ i, bb) (χ i. if i ∈ FVO ODE then sol t $ i else ab $ i)) $ i = (if i ∈ FVO ODE then sol t $ i else ab $ i))"
have f7: "fst (aa, ba) $ i = sol t $ i ∨ (Inl i::'c + 'c) ∉ Inl ` ODE_vars I ODE"
using a5 a1 by auto
have f8: "fst (aa, ba) $ i = ab $ i ∨ (Inl i::'c + 'c) ∈ Inl ` ODE_vars I ODE"
using a3 a1 by fastforce
moreover
{ assume "fst (mk_v I ODE (χ c. if c ∈ FVO ODE then sol 0 $ c else ab $ c, bb) (χ c. if c ∈ FVO ODE then sol t $ c else ab $ c)) $ i ≠ ab $ i"
{ assume "fst (mk_v I ODE (χ c. if c ∈ FVO ODE then sol 0 $ c else ab $ c, bb) (χ c. if c ∈ FVO ODE then sol t $ c else ab $ c)) $ i ≠ ab $ i ∧ Inl i ∉ Inr ` ODE_vars I ODE"
have " i ∈ FVO ODE ∧ fst (aa, ba) $ i = ab $ i ⟶ fst (mk_v I ODE (χ c. if c ∈ FVO ODE then sol 0 $ c else ab $ c, bb) (χ c. if c ∈ FVO ODE then sol t $ c else ab $ c)) $ i ≠ sol t $ i ∧ (Inl i::'c + 'c) ∈ Inl ` ODE_vars I ODE ∨ fst (mk_v I ODE (χ c. if c ∈ FVO ODE then sol 0 $ c else ab $ c, bb) (χ c. if c ∈ FVO ODE then sol t $ c else ab $ c)) $ i = ab $ i"
using f7 a4 a2 by force }
then have " i ∈ FVO ODE ∧ fst (aa, ba) $ i = ab $ i ⟶ fst (mk_v I ODE (χ c. if c ∈ FVO ODE then sol 0 $ c else ab $ c, bb) (χ c. if c ∈ FVO ODE then sol t $ c else ab $ c)) $ i ≠ sol t $ i ∧ (Inl i::'c + 'c) ∈ Inl ` ODE_vars I ODE ∨ fst (mk_v I ODE (χ c. if c ∈ FVO ODE then sol 0 $ c else ab $ c, bb) (χ c. if c ∈ FVO ODE then sol t $ c else ab $ c)) $ i = ab $ i"
by blast }
ultimately have " i ∈ FVO ODE ⟶ fst (mk_v I ODE (χ c. if c ∈ FVO ODE then sol 0 $ c else ab $ c, bb) (χ c. if c ∈ FVO ODE then sol t $ c else ab $ c)) $ i = fst (aa, ba) $ i"
using f7 a6 by fastforce
then have "fst (mk_v I ODE (χ c. if c ∈ FVO ODE then sol 0 $ c else ab $ c, bb) (χ c. if c ∈ FVO ODE then sol t $ c else ab $ c)) $ i = fst (aa, ba) $ i"
using f8 a4 ode_to_fvo by fastforce
then show ?thesis
using a1 by presburger
qed
proof -
fix i :: 'c
assume a1: "osafe ODE"
assume a2: "(aa, ba) = mk_v I ODE (ab, bb) (sol t)"
assume a3: "∀i. (Inr i ∈ Inl ` ODE_vars I ODE ⟶ snd (mk_v I ODE (χ i. if i ∈ FVO ODE then sol 0 $ i else ab $ i, bb) (χ i. if i ∈ FVO ODE then sol t $ i else ab $ i)) $ i = ODE_sem I ODE (χ i. if i ∈ FVO ODE then sol t $ i else ab $ i) $ i) ∧ ((Inr i::'c + 'c) ∈ Inr ` ODE_vars I ODE ⟶ snd (mk_v I ODE (χ i. if i ∈ FVO ODE then sol 0 $ i else ab $ i, bb) (χ i. if i ∈ FVO ODE then sol t $ i else ab $ i)) $ i = ODE_sem I ODE (χ i. if i ∈ FVO ODE then sol t $ i else ab $ i) $ i)"
assume a4: "∀i. (Inr i ∈ Inl ` ODE_vars I ODE ⟶ snd (mk_v I ODE (ab, bb) (sol t)) $ i = ODE_sem I ODE (sol t) $ i) ∧ ((Inr i::'c + 'c) ∈ Inr ` ODE_vars I ODE ⟶ snd (mk_v I ODE (ab, bb) (sol t)) $ i = ODE_sem I ODE (sol t) $ i)"
assume a5: "∀i. Inr i ∉ Inl ` ODE_vars I ODE ∧ (Inr i::'c + 'c) ∉ Inr ` ODE_vars I ODE ⟶ snd (mk_v I ODE (χ i. if i ∈ FVO ODE then sol 0 $ i else ab $ i, bb) (χ i. if i ∈ FVO ODE then sol t $ i else ab $ i)) $ i = bb $ i"
assume a6: "∀i. Inr i ∉ Inl ` ODE_vars I ODE ∧ (Inr i::'c + 'c) ∉ Inr ` ODE_vars I ODE ⟶ snd (mk_v I ODE (ab, bb) (sol t)) $ i = bb $ i"
have "⋀i f r v. ODE_sem (i::('a, 'b, 'c) interp) ODE (χ c. if c ∈ FVO ODE then f (r::real) $ c else v $ c) = ODE_sem i ODE (f r)"
using a1 by (metis (no_types) alt_sem_lemma)
moreover
{ assume "(Inr i::'c + 'c) ∉ Inr ` ODE_vars I ODE"
moreover
{ assume "(Inr i::'c + 'c) ∉ Inr ` ODE_vars I ODE ∧ Inr i ∉ Inl ` ODE_vars I ODE ∧ (Inr i::'c + 'c) ∉ Inr ` ODE_vars I ODE ∧ Inr i ∉ Inl ` ODE_vars I ODE"
then have "snd (aa, ba) $ i = bb $ i ∧ (Inr i::'c + 'c) ∉ Inr ` ODE_vars I ODE ∧ Inr i ∉ Inl ` ODE_vars I ODE"
using a6 a2 by presburger
then have "snd (mk_v I ODE (χ c. if c ∈ FVO ODE then sol 0 $ c else ab $ c, bb) (χ c. if c ∈ FVO ODE then sol t $ c else ab $ c)) $ i = snd (aa, ba) $ i"
using a5 by presburger }
ultimately have "snd (mk_v I ODE (χ c. if c ∈ FVO ODE then sol 0 $ c else ab $ c, bb) (χ c. if c ∈ FVO ODE then sol t $ c else ab $ c)) $ i = snd (aa, ba) $ i"
by blast }
ultimately show "snd (mk_v I ODE (ab, bb) (sol t)) $ i = snd (mk_v I ODE (χ c. if c ∈ FVO ODE then sol 0 $ c else ab $ c, bb) (χ c. if c ∈ FVO ODE then sol t $ c else ab $ c)) $ i"
using a4 a3 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 φ"
and eqP:"P = φ"
and aaba: "(aa, ba) = mk_v I ODE (ab, bb) (sol t)"
and all:"∀i. (Inl i ∈ BVO ODE ⟶ sol 0 $ i = ab $ i) ∧ (Inl i ∈ Inl ` FVO ODE ⟶ sol 0 $ i = ab $ i) ∧ (Inl i ∈ FVF φ ⟶ sol 0 $ i = ab $ i)"
and allSol:"∀x∈{0..t}. (sol has_derivative (λxa. xa *⇩R ODE_sem I ODE (sol x))) (at x within {0..t})"
and mkV:"sol ∈ {0..t} → {x. mk_v I ODE (ab, bb) x ∈ fml_sem I φ}"
and x:"0 ≤ x"
and t:"x ≤ t"
from all have allT:"⋀s. s ≥ 0 ⟹ s ≤ t ⟹ mk_v I ODE (ab,bb) (sol s) ∈ fml_sem I φ"
using mkV by auto
have VA:"⋀x. Vagree (mk_v I ODE (ab, bb) (sol x)) (mk_v I ODE (ab, bb) (χ i. if i ∈ FVO ODE then sol x $ i else ab $ i))
(FVF φ)"
unfolding Vagree_def
apply(auto)
subgoal for xa i
using mk_v_agree[of I ODE "(ab,bb)" "sol xa"]
mk_v_agree[of I ODE "(ab,bb)" "(χ i. if i ∈ FVO ODE then sol xa $ i else ab $ i)"]
apply(cases "i ∈ 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)" "(χ i. if i ∈ 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: "∀i. Inr i ∉ Inl ` ODE_vars I ODE ∧ (Inr i::'c + 'c) ∉ Inr ` ODE_vars I ODE ⟶ snd (mk_v I ODE (ab, bb) (sol xa)) $ i = bb $ i"
assume a2: "∀i. Inr i ∉ Inl ` ODE_vars I ODE ∧ (Inr i::'c + 'c) ∉ Inr ` ODE_vars I ODE ⟶ snd (mk_v I ODE (ab, bb) (χ i. if i ∈ FVO ODE then sol xa $ i else ab $ i)) $ i = bb $ i"
assume a3: "∀i. (Inr i ∈ Inl ` ODE_vars I ODE ⟶ snd (mk_v I ODE (ab, bb) (sol xa)) $ i = ODE_sem I ODE (sol xa) $ i) ∧ ((Inr i::'c + 'c) ∈ Inr ` ODE_vars I ODE ⟶ snd (mk_v I ODE (ab, bb) (sol xa)) $ i = ODE_sem I ODE (sol xa) $ i)"
assume a4: "∀i. (Inr i ∈ Inl ` ODE_vars I ODE ⟶ snd (mk_v I ODE (ab, bb) (χ i. if i ∈ FVO ODE then sol xa $ i else ab $ i)) $ i = ODE_sem I ODE (χ i. if i ∈ FVO ODE then sol xa $ i else ab $ i) $ i) ∧ ((Inr i::'c + 'c) ∈ Inr ` ODE_vars I ODE ⟶ snd (mk_v I ODE (ab, bb) (χ i. if i ∈ FVO ODE then sol xa $ i else ab $ i)) $ i = ODE_sem I ODE (χ i. if i ∈ FVO ODE then sol xa $ i else ab $ i) $ i)"
have "ODE_sem I ODE (χ c. if c ∈ FVO ODE then sol xa $ c else ab $ c) $ i = ODE_sem I ODE (sol xa) $ i"
by (metis (no_types) alt_sem_lemma osafe)
then have "Inr i ∉ Inl ` ODE_vars I ODE ∧ (Inr i::'c + 'c) ∉ Inr ` ODE_vars I ODE ∨ snd (mk_v I ODE (ab, bb) (sol xa)) $ i = snd (mk_v I ODE (ab, bb) (χ c. if c ∈ 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:"(∀i. Inl i ∈ FVF φ ⟶
fst (mk_v I ODE ((χ i. if i ∈ FVO ODE then sol 0 $ i else ab $ i), bb) (χ i. if i ∈ FVO ODE then sol x $ i else ab $ i)) $ i
= fst (mk_v I ODE (ab, bb) (sol x)) $ i)"
and VA2: "(∀i. Inr i ∈ FVF φ ⟶
snd (mk_v I ODE ((χ i. if i ∈ FVO ODE then sol 0 $ i else ab $ i), bb) (χ i. if i ∈ FVO ODE then sol x $ i else ab $ i)) $ i
= snd (mk_v I ODE (ab, bb) (sol x)) $ i)"
apply(auto)
subgoal for i
using mk_v_agree[of I ODE "((χ i. if i ∈ FVO ODE then sol 0 $ i else ab $ i),bb)" "(χ i. if i ∈ 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 ∈ FVO ODE")
apply(auto)
apply(cases " i ∈ FVO ODE")
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 "((χ i. if i ∈ FVO ODE then sol 0 $ i else ab $ i),bb)" "(χ i. if i ∈ 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 ∈ FVO ODE")
apply(auto)
apply(cases " i ∈ 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 osafe)+
done
show "mk_v I ODE (χ i. if i ∈ FVO ODE then sol 0 $ i else ab $ i, bb)
(χ i. if i ∈ FVO ODE then sol x $ i else ab $ i) ∈ fml_sem I φ"
using mk_v_agree[of I ODE "(χ i. if i ∈ FVO ODE then sol 0 $ i else ab $ i, bb)"
"(χ i. if i ∈ 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 (χ i. if i ∈ FVO ODE then sol 0 $ i else ab $ i, bb) (χ i. if i ∈ 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
by auto
qed
proof -
fix x i
assume
assms:"osafe ODE"
"fsafe φ"
"0 ≤ t"
"(aa, ba) = mk_v I ODE (ab, bb) (sol t)"
"VSagree (sol 0) ab {x. Inl x ∈ BVO ODE ∨ Inl x ∈ Inl ` FVO ODE ∨ Inl x ∈ FVF φ}"
and deriv:"∀x∈{0..t}. (sol has_derivative (λxa. xa *⇩R ODE_sem I ODE (sol x))) (at x within {0..t})"
and sol:"sol ∈ {0..t} → {x. mk_v I ODE (ab, bb) x ∈ fml_sem I φ}"
and mem:"x ∈ {0..t}"
from deriv
have xDeriv:"(sol has_derivative (λxa. xa *⇩R ODE_sem I ODE (sol x))) (at x within {0..t})"
using mem by blast
have silly1:"(λx. χ i. sol x $ i) = sol"
by (auto simp add: vec_eq_iff)
have silly2:"(λh. χ i. h * ODE_sem I ODE (sol x) $ i) = (λxa. xa *⇩R ODE_sem I ODE (sol x))"
by (auto simp add: vec_eq_iff)
from xDeriv have
xDeriv':"((λx. χ i. sol x $ i) has_derivative (λh. χ i. h * ODE_sem I ODE (sol x) $ i)) (at x within {0..t})"
using silly1 silly2 apply auto done
from xDeriv have xDerivs:"⋀j. ((λt. sol t $ j) has_derivative (λxa. (xa *⇩R ODE_sem I ODE (sol x)) $ j)) (at x within {0..t})"
subgoal for j
using silly1 silly2 has_derivative_proj[of "(λi. λt. sol t $ i)" "(λ i. λxa. (xa *⇩R ODE_sem I ODE (sol x)) $ i)" "(at x within {0..t})" j]
apply auto
done
done
have neato:"⋀ν. i ∉ FVO ODE ⟹ ODE_sem I ODE ν $ i = 0"
proof (induction "ODE")
qed auto
show "((λt. if i ∈ FVO ODE then sol t $ i else ab $ i) has_derivative
(λh. h *⇩R ODE_sem I ODE (χ i. if i ∈ 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 ∈ FVO ODE")
using xDerivs[of i] apply auto
using alt_sem_lemma neato[of "(χ i. if i ∈ FVO ODE then sol x $ i else ab $ i)"] apply auto
proof -
assume a1: "((λt. sol t $ i) has_derivative (λxa. xa * ODE_sem I ODE (sol x) $ i)) (at x within {0..t})"
have "⋀i r. ODE_sem (i::('a, 'b, 'c) interp) ODE (χ c. if c ∈ FVO ODE then sol r $ c else ab $ c) = ODE_sem i ODE (sol r)"
by (metis (no_types) alt_sem_lemma assms(1))
then show "((λr. sol r $ i) has_derivative (λr. r * ODE_sem I ODE (χ c. if c ∈ 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 φ"
and t:"0 ≤ t"
and aaba:"(aa, ba) = mk_v I ODE (sol 0, bb) (sol t)"
and sol:"(sol solves_ode (λa. ODE_sem I ODE)) {0..t} {x. mk_v I ODE (sol 0, bb) x ∈ fml_sem I φ}"
show"∃sola ta. mk_v I ODE (sol 0, bb) (sol t) = mk_v I ODE (sol 0, bb) (sola ta) ∧
0 ≤ ta ∧
(sola solves_ode (λa. ODE_sem I ODE)) {0..ta} {x. mk_v I ODE (sol 0, bb) x ∈ fml_sem I φ} ∧
VSagree (sola 0) (sol 0) {x. Inl x ∈ BVO ODE ∨ Inl x ∈ Inl ` FVO ODE ∨ Inl x ∈ FVF φ}"
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 "∀I J. coincide_hp (EvolveODE ODE P) I J ∧ ode_sem_equiv (EvolveODE ODE P) I"
proof (rule allI)+
fix I J::"('a,'b,'c) interp"
from equiv[of I]
have equivI:"
{(ν, mk_v I ODE ν (sol t)) | ν sol t.
t ≥ 0 ∧
(sol solves_ode (λ_. ODE_sem I ODE)) {0..t} {x. mk_v I ODE ν x ∈ fml_sem I P} ∧
VSagree (sol 0) (fst ν) {x | x. Inl x ∈ FVP (EvolveODE ODE P)}} =
{(ν, mk_v I ODE ν (sol t)) | ν sol t.
t ≥ 0 ∧
(sol solves_ode (λ_. ODE_sem I ODE)) {0..t} {x. mk_v I ODE ν x ∈ fml_sem I P} ∧
(sol 0) = (fst ν)}"
unfolding ode_sem_equiv_def using osafe fsafe by blast
from equiv[of J]
have equivJ:"
{(ν, mk_v J ODE ν (sol t)) | ν sol t.
t ≥ 0 ∧
(sol solves_ode (λ_. ODE_sem J ODE)) {0..t} {x. mk_v J ODE ν x ∈ fml_sem J P} ∧
VSagree (sol 0) (fst ν) {x | x. Inl x ∈ FVP (EvolveODE ODE P)}} =
{(ν, mk_v J ODE ν (sol t)) | ν sol t.
t ≥ 0 ∧
(sol solves_ode (λ_. ODE_sem J ODE)) {0..t} {x. mk_v J ODE ν x ∈ fml_sem J P} ∧
(sol 0) = (fst ν)}"
unfolding ode_sem_equiv_def using osafe fsafe by blast
from equivI
have alt_ode_semI:"prog_sem I (EvolveODE ODE P) =
{(ν, mk_v I ODE ν (sol t)) | ν sol t.
t ≥ 0 ∧
(sol solves_ode (λ_. ODE_sem I ODE)) {0..t} {x. mk_v I ODE ν x ∈ fml_sem I P} ∧
VSagree (sol 0) (fst ν) {x | x. Inl x ∈ FVP (EvolveODE ODE P)}}" by auto
from equivJ
have alt_ode_semJ:"prog_sem J (EvolveODE ODE P) =
{(ν, mk_v J ODE ν (sol t)) | ν sol t.
t ≥ 0 ∧
(sol solves_ode (λ_. ODE_sem J ODE)) {0..t} {x. mk_v J ODE ν x ∈ fml_sem J P} ∧
VSagree (sol 0) (fst ν) {x | x. Inl x ∈ FVP (EvolveODE ODE P)}}" by auto
have co_hp:"coincide_hp (EvolveODE ODE P) I J"
apply(unfold coincide_hp_def)
apply (auto simp del: prog_sem.simps(8) simp add: alt_ode_semI alt_ode_semJ)
proof -
fix a b aa ba ab bb V sol t
from IH have IHF:"∀a b aa ba . Iagree I J (SIGF P) ⟶ Vagree (a, b) (aa, ba) (FVF P) ⟶ ((a, b) ∈ fml_sem I P) = ((aa, ba) ∈ fml_sem J P)"
unfolding coincide_fml_def by blast
assume IA:"Iagree I J (SIGF P ∪ {Inl x |x. Inl x ∈ SIGO ODE} ∪ {Inr (Inr x) |x. Inr x ∈ SIGO ODE})"
and VA:"Vagree (a, b) (aa, ba) V"
and OVsub:"BVO ODE ⊆ V"
and Osub:"Inl ` FVO ODE ⊆ V"
and Fsub:"FVF P ⊆ V"
and veq:"(ab, bb) = mk_v I ODE (a, b) (sol t)"
and t:"0 ≤ t"
and sol:"(sol solves_ode (λa. ODE_sem I ODE)) {0..t} {x. mk_v I ODE (a, b) x ∈ fml_sem I P}"
and VSA:"VSagree (sol 0) a {uu. Inl uu ∈ BVO ODE ∨ Inl uu ∈ Inl ` FVO ODE ∨ Inl uu ∈ FVF P}"
have semBVsub:"(semBV I ODE) ⊆ BVO ODE"
by (induction ODE, auto)
then have OVsub'':"(semBV I ODE) ⊆ V" using OVsub by auto
have MBVBVsub:"(Inl ` ODE_dom ODE ∪ Inr ` ODE_dom ODE) ⊆ BVO ODE"
apply(induction ODE)
by auto
from OVsub and MBVBVsub have OVsub':"(Inl ` ODE_dom ODE ∪ Inr ` ODE_dom ODE) ⊆ V"
by auto
from sol
have solSem:"⋀x. 0 ≤ x ⟹ x ≤ t ⟹ mk_v I ODE (a, b) (sol x) ∈ fml_sem I P"
and solDeriv:"⋀x. 0 ≤ x ⟹ x ≤ t ⟹ (sol has_vector_derivative ODE_sem I ODE (sol x)) (at x within {0..t})"
unfolding solves_ode_def has_vderiv_on_def by auto
have SIGFsub:"(SIGF P) ⊆ (SIGF P ∪ {Inl x |x. Inl x ∈ SIGO ODE} ∪ {Inr (Inr x) |x. Inr x ∈ SIGO ODE})" by auto
from IA have IAP:"Iagree I J (SIGF P)"
using Iagree_sub[OF SIGFsub] by auto
from IHF have IH':
"∀a b aa ba. Vagree (a, b) (aa, ba) (FVF P) ⟶ ((a, b) ∈ fml_sem I P) = ((aa, ba) ∈ fml_sem J P)"
using IAP by blast
from VA
have VAOV:"Vagree (a,b) (aa,ba) (BVO ODE)"
using agree_sub[OF OVsub] by auto
have ag:"⋀s. Vagree (mk_v I ODE (a, b) (sol s)) (a, b) (- semBV I ODE)"
"⋀s. Vagree (mk_v I ODE (a, b) (sol s)) (mk_xode I ODE (sol s)) (semBV I ODE)"
"⋀s. Vagree (mk_v J ODE (aa, ba) (sol s)) (aa, ba) (- semBV J ODE)"
"⋀s. Vagree (mk_v J ODE (aa, ba) (sol s)) (mk_xode J ODE (sol s)) (semBV J ODE)"
subgoal for s using mk_v_agree[of I ODE "(a,b)" "sol s"] by auto
subgoal for s using mk_v_agree[of I ODE "(a,b)" "sol s"] by auto
subgoal for s using mk_v_agree[of J ODE "(aa,ba)" "sol s"] by auto
subgoal for s using mk_v_agree[of J ODE "(aa,ba)" "sol s"] by auto
done
have sem_sub_BVO:"⋀I. semBV I ODE ⊆ BVO ODE"
subgoal for I
apply(induction ODE)
by auto
done
have MBV_sub_sem:"⋀I. (Inl ` ODE_dom ODE ∪ Inr ` ODE_dom ODE) ⊆ semBV I ODE"
subgoal for I by (induction ODE, auto) done
have ag_BVO:
"⋀s. Vagree (mk_v I ODE (a, b) (sol s)) (a, b) (- BVO ODE)"
"⋀s. Vagree (mk_v J ODE (aa, ba) (sol s)) (aa, ba) (- BVO ODE)"
using ag(1) ag(3) sem_sub_BVO[of I] sem_sub_BVO[of J] agree_sub by blast+
have ag_semBV:
"⋀s. Vagree (mk_v I ODE (a, b) (sol s)) (mk_xode I ODE (sol s)) (Inl ` ODE_dom ODE ∪ Inr ` ODE_dom ODE)"
"⋀s. Vagree (mk_v J ODE (aa, ba) (sol s)) (mk_xode J ODE (sol s)) (Inl ` ODE_dom ODE ∪ Inr ` ODE_dom ODE)"
using ag(2) ag(4) MBV_sub_sem[of I] MBV_sub_sem[of J]
by (simp add: agree_sub)+
have IOsub:"({Inl x |x. Inl x ∈ SIGO ODE} ∪ {Inr (Inr x) |x. Inr x ∈ SIGO ODE}) ⊆ (SIGF P ∪ {Inl x |x. Inl x ∈ SIGO ODE} ∪ {Inr (Inr x) |x. Inr x ∈ SIGO ODE})"
by auto
from IA
have IAO:"Iagree I J ({Inl x |x. Inl x ∈ SIGO ODE} ∪ {Inr (Inr x) |x. Inr x ∈ SIGO ODE})"
using Iagree_sub[OF IOsub] by auto
have IOsub':"({Inr (Inr x) |x. Inr x ∈ SIGO ODE}) ⊆ ({Inl x |x. Inl x ∈ SIGO ODE} ∪ {Inr (Inr x) |x. Inr x ∈ SIGO ODE})"
by auto
from IAO
have IAO':"Iagree I J ({Inr (Inr x) |x. Inr x ∈ SIGO ODE})"
using Iagree_sub[OF IOsub'] by auto
have VAsol:"⋀s ν'. Vagree ((sol s), ν') ((sol s), ν') (Inl `FVO ODE)" unfolding Vagree_def by auto
have Osem:"⋀s. 0 ≤ s ⟹ s ≤ t ⟹ ODE_sem I ODE (sol s) = ODE_sem J ODE (sol s)"
subgoal for s
using coincidence_ode[OF osafe VAsol[of s] IAO] by auto
done
from Osem
have Oag:"⋀s. 0 ≤ s ⟹ s ≤ t ⟹ VSagree (ODE_sem I ODE (sol s)) (ODE_sem J ODE (sol s)) {x. Inr x ∈ BVO ODE}"
unfolding VSagree_def by auto
from Osem
have Oagsem:"⋀s. 0 ≤ s ⟹ s ≤ t ⟹ VSagree (ODE_sem I ODE (sol s)) (ODE_sem J ODE (sol s)) {x. Inr x ∈ (semBV I ODE)}"
unfolding VSagree_def by auto
from Osem
have halp:"⋀s. 0 ≤ s ⟹ s ≤ t ⟹ Vagree (mk_xode I ODE (sol s)) (mk_xode J ODE (sol s)) (semBV I ODE)"
apply(auto)
using Oag unfolding Vagree_def VSagree_def by blast
then have halpp:"⋀s. 0 ≤ s ⟹ s ≤ t ⟹ Vagree (sol s, ODE_sem I ODE (sol s)) (sol s, ODE_sem J ODE (sol s)) (semBV I ODE)"
by auto
have eqV:"V = ((semBV I ODE)) ∪ (V ∩ (-(semBV I ODE)))" using OVsub'' by auto
have neat:"⋀ODE. Iagree I J ({Inr (Inr x) |x. Inr x ∈ SIGO ODE}) ⟹ semBV I ODE = semBV J ODE"
subgoal for ODE
proof (induction ODE)
case (OVar x)
then show ?case unfolding Iagree_def by auto
next
case (OSing x1a x2)
then show ?case by auto
next
case (OProd ODE1 ODE2)
assume IH1:"Iagree I J {Inr (Inr x) |x. Inr x ∈ SIGO ODE1} ⟹ semBV I ODE1 = semBV J ODE1"
assume IH2:"Iagree I J {Inr (Inr x) |x. Inr x ∈ SIGO ODE2} ⟹ semBV I ODE2 = semBV J ODE2"
assume agree:"Iagree I J {Inr (Inr x) |x. Inr x ∈ SIGO (OProd ODE1 ODE2)}"
from agree have agree1:"Iagree I J {Inr (Inr x) |x. Inr x ∈ SIGO ( ODE1 )}" and agree2:"Iagree I J {Inr (Inr x) |x. Inr x ∈ SIGO ( ODE2)}"
unfolding Iagree_def by auto
show ?case using IH1[OF agree1] IH2[OF agree2] by auto
qed
done
note semBVeq = neat[OF IAO']
then have halpp':"⋀s. 0 ≤ s ⟹ s ≤ t ⟹ Vagree (mk_v I ODE (a, b) (sol s)) (mk_v J ODE (aa, ba) (sol s)) (semBV I ODE)"
subgoal for s using ag[of s] ag_semBV[of s] Oagsem agree_trans semBVeq
unfolding Vagree_def by (auto simp add: semBVeq Osem)
done
have VAbar:"⋀s. 0 ≤ s ⟹ s ≤ t ⟹ Vagree (mk_v I ODE (a, b) (sol s)) (mk_v J ODE (aa, ba) (sol s)) (V ∩ (-(semBV I ODE)))"
subgoal for s
apply(unfold Vagree_def)
apply(rule conjI | rule allI)+
subgoal for i
apply auto
using VA ag[of s] semBVeq unfolding Vagree_def apply auto
by (metis Un_iff)
apply(rule allI)+
subgoal for i
using VA ag[of s] semBVeq unfolding Vagree_def by auto
done
done
have VAfoo:"⋀s. 0 ≤ s ⟹ s ≤ t ⟹ Vagree (mk_v I ODE (a, b) (sol s)) (mk_v J ODE (aa, ba) (sol s)) V"
using agree_union[OF halpp' VAbar] eqV by auto
have duhSub:"FVF P ⊆ UNIV" by auto
from VAfoo
have VA'foo:"⋀s. 0 ≤ s ⟹ s ≤ t ⟹ Vagree (mk_v I ODE (a, b) (sol s)) (mk_v J ODE (aa, ba) (sol s)) V"
using agree_sub[OF duhSub] by auto
then have VA''foo:"⋀s. 0 ≤ s ⟹ s ≤ t ⟹ Vagree (mk_v I ODE (a, b) (sol s)) (mk_v J ODE (aa, ba) (sol s)) (FVF P)"
using agree_sub[OF Fsub] by auto
from VA''foo IH'
have fmlSem:"⋀s. 0 ≤ s ⟹ s ≤ t ⟹ (mk_v I ODE (a, b) (sol s)) ∈ fml_sem I P ⟷ (mk_v J ODE (aa, ba) (sol s)) ∈ fml_sem J P"
using IAP coincide_fml_def hpsafe_Evolve.IH by blast
from VA
have VAO:"Vagree (a, b) (aa, ba) (Inl `FVO ODE)"
using agree_sub[OF Osub] by auto
have sol':"(sol solves_ode (λ_. ODE_sem J ODE)) {0..t} {x. mk_v J ODE (aa, ba) x ∈ fml_sem J P}"
apply(auto simp add: solves_ode_def has_vderiv_on_def)
subgoal for s
using solDeriv[of s] Osem[of s] by auto
subgoal for s
using solSem[of s] fmlSem[of s] by auto
done
have VSA':"VSagree (sol 0) aa {uu. Inl uu ∈ BVO ODE ∨ Inl uu ∈ Inl `FVO ODE ∨ Inl uu ∈ FVF P}"
using VSA VA OVsub unfolding VSagree_def Vagree_def
apply auto
using Osub apply blast
using Fsub by blast
show
" ∃ab bb. (∃sol t. (ab, bb) = mk_v J ODE (aa, ba) (sol t) ∧
0 ≤ t ∧
(sol solves_ode (λa. ODE_sem J ODE)) {0..t} {x. mk_v J ODE (aa, ba) x ∈ fml_sem J P} ∧
VSagree (sol 0) aa {uu. Inl uu ∈ BVO ODE ∨ Inl uu ∈ Inl `FVO ODE ∨ Inl uu ∈ FVF P}) ∧
Vagree (mk_v I ODE (a, b) (sol t)) (ab, bb) (Inl ` ODE_dom ODE ∪ Inr ` ODE_dom ODE ∪ V) "
apply(rule exI[where x="fst (mk_v J ODE (aa, ba) (sol t))"])
apply(rule exI[where x="snd (mk_v J ODE (aa, ba) (sol t))"])
apply(rule conjI)
subgoal
apply(rule exI[where x="sol"])
apply(rule exI[where x=t])
apply(rule conjI)
subgoal
apply(auto)
done
subgoal
apply(rule conjI)
subgoal by (rule t)
subgoal
apply(rule conjI)
subgoal by (rule sol')
subgoal by (rule VSA')
done
done
done
apply(auto)
using mk_v_agree[of I ODE "(a,b)" "(sol t)"]
mk_v_agree[of J ODE "(aa,ba)" "(sol t)"]
using agree_refl t VA'foo
OVsub' Un_absorb1 by (auto simp add: OVsub' Un_absorb1)
qed
show "coincide_hp (EvolveODE ODE P) I J ∧ ode_sem_equiv (EvolveODE ODE P) I" using co_hp equiv[of I] by auto
qed
qed
next
case (hpsafe_Choice a b)
then show "?case"
proof (auto simp only: coincide_hp'_def coincide_hp_def)
fix I J::"('a,'b,'c) interp" and ν1 ν1' ν2 ν2' μ μ' V
assume safe:"hpsafe a"
"hpsafe b"
and IH1:"
∀ I J. (∀ν ν' μ V.
Iagree I J (SIGP a) ⟶
Vagree ν ν' V ⟶ FVP a ⊆ V ⟶ (ν, μ) ∈ prog_sem I a ⟶ (∃μ'. (ν', μ') ∈ prog_sem J a ∧ Vagree μ μ' (MBV a ∪ V)))
∧ ode_sem_equiv a I"
and IH2:"∀ I J. (∀ν ν' μ V.
Iagree I J (SIGP b) ⟶
Vagree ν ν' V ⟶ FVP b ⊆ V ⟶ (ν, μ) ∈ prog_sem I b ⟶ (∃μ'. (ν', μ') ∈ prog_sem J b ∧ Vagree μ μ' (MBV b ∪ V)))
∧ ode_sem_equiv b I"
and IA:"Iagree I J (SIGP (a ∪∪ b))"
and VA:"Vagree (ν1, ν1') (ν2, ν2') V"
and sub:"FVP (a ∪∪ b) ⊆ V"
and sem:"((ν1, ν1'), (μ, μ')) ∈ prog_sem I (a ∪∪ b)"
hence eitherSem:"((ν1, ν1'), (μ, μ')) ∈ prog_sem I a ∨ ((ν1, ν1'), (μ, μ')) ∈ prog_sem I b"
by auto
have Ssub:"(SIGP a) ⊆ SIGP (a ∪∪ b)" "(SIGP b) ⊆ SIGP (a ∪∪ b)"
unfolding SIGP.simps by auto
have IA1:"Iagree I J (SIGP a)" and IA2:"Iagree I J (SIGP b)"
using IA Iagree_sub[OF Ssub(1)] Iagree_sub[OF Ssub(2)] by auto
from sub have sub1:"FVP a ⊆ V" and sub2:"FVP b ⊆ V" by auto
then
show "∃μ''. ((ν2, ν2'), μ'') ∈ prog_sem J (a ∪∪ b) ∧ Vagree (μ, μ') μ'' (MBV (a ∪∪ b) ∪ V)"
proof (cases "((ν1, ν1'), (μ, μ')) ∈ prog_sem I a")
case True
then obtain μ'' where prog_sem:"((ν2,ν2'), μ'') ∈ prog_sem J a" and agree:"Vagree (μ, μ') μ'' (MBV a ∪ V)"
using IH1 VA sub1 IA1 by blast
from agree have agree':"Vagree (μ, μ') μ'' (MBV (a ∪∪ b) ∪ V)"
unfolding Vagree_def MBV.simps by auto
from prog_sem have prog_sem':"((ν2,ν2'), μ'') ∈ prog_sem J (a ∪∪ b)"
unfolding prog_sem.simps by blast
from agree' and prog_sem' show ?thesis by blast
next
case False
then have sem2:"((ν1, ν1'), (μ, μ')) ∈ prog_sem I b" using eitherSem by blast
then obtain μ'' where prog_sem:"((ν2,ν2'), μ'') ∈ prog_sem J b" and agree:"Vagree (μ, μ') μ'' (MBV b ∪ V)"
using IH2 VA sub2 IA2 by blast
from agree have agree':"Vagree (μ, μ') μ'' (MBV (a ∪∪ b) ∪ V)"
unfolding Vagree_def MBV.simps by auto
from prog_sem have prog_sem':"((ν2,ν2'), μ'') ∈ prog_sem J (a ∪∪ b)"
unfolding prog_sem.simps by blast
from agree' and prog_sem' show ?thesis by blast
qed
next
fix I
assume IHs:
"∀I J. (∀ν ν' μ V.
Iagree I J (SIGP a) ⟶
Vagree ν ν' V ⟶ FVP a ⊆ V ⟶ (ν, μ) ∈ prog_sem I a ⟶ (∃μ'. (ν', μ') ∈ prog_sem J a ∧ Vagree μ μ' (MBV a ∪ V))) ∧
ode_sem_equiv a I"
"∀I J. (∀ν ν' μ V.
Iagree I J (SIGP b) ⟶
Vagree ν ν' V ⟶ FVP b ⊆ V ⟶ (ν, μ) ∈ prog_sem I b ⟶ (∃μ'. (ν', μ') ∈ prog_sem J b ∧ Vagree μ μ' (MBV b ∪ V))) ∧
ode_sem_equiv b I"
show "ode_sem_equiv (a ∪∪ b) I"
unfolding ode_sem_equiv_def by auto
qed
next
case (hpsafe_Sequence a b) then show "?case"
apply (unfold coincide_hp'_def coincide_hp_def)
apply (rule allI)+
apply (rule conjI)
prefer 2 subgoal unfolding ode_sem_equiv_def by auto
apply(unfold prog_sem.simps SIGP.simps FVP.simps )
apply(rule allI)+
apply(auto)
subgoal for I J ν2 ν2' V ν1 ν1' μ μ' ω ω'
proof -
assume safe:"hpsafe a" "hpsafe b"
assume "(∀I. ((∀J. Iagree I J (SIGP a) ⟶ (∀aa b ab ba ac bb V.
Vagree (aa, b) (ab, ba) V ⟶
FVP a ⊆ V ⟶ ((aa, b), ac, bb) ∈ prog_sem I a ⟶ (∃aa b. ((ab, ba), aa, b) ∈ prog_sem J a ∧ Vagree (ac, bb) (aa, b) (MBV a ∪ V)))))
∧ ode_sem_equiv a I)"
hence IH1':"⋀aa b ab ba ac bb V.
Iagree I J (SIGP a) ⟹
Vagree (aa, b) (ab, ba) V ⟹
FVP a ⊆ V ⟹ ((aa, b), ac, bb) ∈ prog_sem I a ⟹ (∃aa b. ((ab, ba), aa, b) ∈ prog_sem J a ∧ Vagree (ac, bb) (aa, b) (MBV a ∪ V))"
by auto
note IH1 = IH1'[of ν1 ν1' ν2 ν2' V μ μ']
assume IH2'':"
∀I. (∀J. Iagree I J (SIGP b) ⟶ (∀a ba aa bb ab bc V.
Vagree (a, ba) (aa, bb) V ⟶
FVP b ⊆ V ⟶ ((a, ba), ab, bc) ∈ prog_sem I b ⟶ (∃a ba. ((aa, bb), a, ba) ∈ prog_sem J b ∧ Vagree (ab, bc) (a, ba) (MBV b ∪ V))))
∧ ode_sem_equiv b I"
assume IAab:"Iagree I J (SIGP a ∪ SIGP b)"
have IAsubs:"SIGP a ⊆ (SIGP a ∪ SIGP b)" "SIGP b ⊆ (SIGP a ∪ SIGP b)" by auto
from IAab have IA:"Iagree I J (SIGP a)" "Iagree I J (SIGP b)" using Iagree_sub[OF IAsubs(1)] Iagree_sub[OF IAsubs(2)] by auto
from IH2'' have IH2':"⋀a ba aa bb ab bc V .
Iagree I J (SIGP b) ⟹
Vagree (a, ba) (aa, bb) V ⟹
FVP b ⊆ V ⟹ ((a, ba), ab, bc) ∈ prog_sem I b ⟹ (∃a ba. ((aa, bb), a, ba) ∈ prog_sem J b ∧ Vagree (ab, bc) (a, ba) (MBV b ∪ V))"
using IA by auto
assume VA:"Vagree (ν1, ν1') (ν2, ν2') V"
assume sub:"FVP a ⊆ V" "FVP b - MBV a ⊆ V"
hence sub':"FVP a ⊆ V" by auto
assume sem:"((ν1, ν1'), (μ, μ')) ∈ prog_sem I a"
"((μ, μ'), (ω, ω')) ∈ prog_sem I b"
obtain ω1 ω1' where sem1:"((ν2, ν2'), (ω1, ω1')) ∈ prog_sem J a" and VA1:"Vagree (μ, μ') (ω1, ω1') (MBV a ∪ V)"
using IH1[OF IA(1) VA sub' sem(1)] by auto
note IH2 = IH2'[of μ μ' ω1 ω1' " MBV a ∪ V" ω ω']
have sub2:"FVP b ⊆ MBV a ∪ V" using sub by auto
obtain ω2 ω2' where sem2:"((ω1, ω1'), (ω2, ω2')) ∈ prog_sem J b" and VA2:"Vagree (ω, ω') (ω2, ω2') (MBV b ∪ (MBV a ∪ V))"
using IH2[OF IA(2) VA1 sub2 sem(2)] by auto
show "∃ab bb. ((ν2, ν2'), (ab, bb)) ∈ prog_sem J a O prog_sem J b ∧ Vagree (ω, ω') (ab, bb) (MBV a ∪ MBV b ∪ V)"
using sem1 sem2 VA1 VA2
by (metis (no_types, lifting) Un_assoc Un_left_commute relcomp.relcompI)
qed
done
next
case (hpsafe_Loop a) then show "?case"
apply(unfold coincide_hp'_def coincide_hp_def)
apply(rule allI)+
apply(rule conjI)
prefer 2 subgoal unfolding ode_sem_equiv_def by auto
apply(rule allI | rule impI)+
apply(unfold prog_sem.simps FVP.simps MBV.simps SIGP.simps)
subgoal for I J ν ν' μ V
proof -
assume safe:"hpsafe a"
assume IH:"(∀ I J. (∀ν ν' μ V.
Iagree I J (SIGP a) ⟶
Vagree ν ν' V ⟶ FVP a ⊆ V ⟶ (ν, μ) ∈ prog_sem I a ⟶ (∃μ'. (ν', μ') ∈ prog_sem J a ∧ Vagree μ μ' (MBV a ∪ V)))
∧ ode_sem_equiv a I)"
assume agree:"Iagree I J (SIGP a)"
assume VA:"Vagree ν ν' V"
assume sub:"FVP a ⊆ V"
have "(ν, μ) ∈ (prog_sem I a)⇧* ⟹ (⋀ν'. Vagree ν ν' V ⟹ ∃μ'. (ν', μ') ∈ (prog_sem J a)⇧* ∧ Vagree μ μ' ({} ∪ V))"
apply(induction rule: converse_rtrancl_induct)
apply(auto)
subgoal for ω ω' s s' v v'
proof -
assume sem1:"((ω, ω'), (s, s')) ∈ prog_sem I a"
and sem2:"((s, s'), μ) ∈ (prog_sem I a)⇧*"
and IH2:"⋀v v'. (Vagree (s, s') (v,v') V ⟹ ∃ab ba. ((v,v'), (ab, ba)) ∈ (prog_sem J a)⇧* ∧ Vagree μ (ab, ba) V)"
and VA:"Vagree (ω, ω') (v,v') V"
obtain s'' where sem'':"((v, v'), s'') ∈ prog_sem J a" and VA'':"Vagree (s,s') s'' (MBV a ∪ V)"
using IH agree VA sub sem1 agree_refl by blast
then obtain s'1 and s'2 where sem'':"((v, v'), (s'1, s'2)) ∈ prog_sem J a" and VA'':"Vagree (s,s') (s'1, s'2) (MBV a ∪ V)"
using IH agree VA sub sem1 agree_refl by (cases "s''", blast)
from VA'' have VA''V:"Vagree (s,s') (s'1, s'2) V"
using agree_sub by blast
note IH2' = IH2[of s'1 s'2]
note IH2'' = IH2'[OF VA''V]
then obtain ab and ba where sem''':"((s'1, s'2), (ab, ba)) ∈ (prog_sem J a)⇧*" and VA''':"Vagree μ (ab, ba) V"
using IH2'' by auto
from sem'' sem''' have sem:"((v, v'), (ab, ba)) ∈ (prog_sem J a)⇧*" by auto
show "∃μ'1 μ'2. ((v, v'), (μ'1, μ'2)) ∈ (prog_sem J a)⇧* ∧ Vagree μ (μ'1, μ'2) V"
using sem VA''' by blast
qed
done
then show "(ν, μ) ∈ (prog_sem I a)⇧* ⟹ Vagree ν ν' V ⟹ ∃μ'. (ν', μ') ∈ (prog_sem J a)⇧* ∧ Vagree μ μ' ({} ∪ V)"
by auto
qed
done
next
case (fsafe_Geq t1 t2)
then have safe:"dsafe t1" "dsafe t2" by auto
have almost:"⋀ν ν'. ⋀ I J :: ('a, 'b, 'c) interp. Iagree I J (SIGF (Geq t1 t2)) ⟹ Vagree ν ν' (FVF (Geq t1 t2)) ⟹ (ν ∈ fml_sem I (Geq t1 t2)) = (ν' ∈ fml_sem J (Geq t1 t2))"
proof -
fix ν ν' and I J :: "('a, 'b, 'c) interp"
assume IA:"Iagree I J (SIGF (Geq t1 t2))"
hence IAs:"Iagree I J {Inl x | x. x ∈ (SIGT t1)}"
"Iagree I J {Inl x | x. x ∈ (SIGT t2)}"
unfolding SIGF.simps Iagree_def by auto
assume VA:"Vagree ν ν' (FVF (Geq t1 t2))"
hence VAs:"Vagree ν ν' (FVT t1)" "Vagree ν ν' (FVT t2)"
unfolding FVF.simps Vagree_def by auto
have sem1:"dterm_sem I t1 ν = dterm_sem J t1 ν'"
by (auto simp add: coincidence_dterm'[OF safe(1) VAs(1) IAs(1)])
have sem2:"dterm_sem I t2 ν = dterm_sem J t2 ν'"
by (auto simp add: coincidence_dterm'[OF safe(2) VAs(2) IAs(2)])
show "(ν ∈ fml_sem I (Geq t1 t2)) = (ν' ∈ fml_sem J (Geq t1 t2))"
by (simp add: sem1 sem2)
qed
show "?case" using almost unfolding coincide_fml_def by blast
next
case (fsafe_Prop args p)
then have safes:"⋀arg. arg ∈ range args ⟹ dsafe arg" using dfree_is_dsafe by auto
have almost:"⋀ν ν'. ⋀ I J::('a, 'b, 'c) interp. Iagree I J (SIGF (Prop p args)) ⟹ Vagree ν ν' (FVF (Prop p args)) ⟹ (ν ∈ fml_sem I (Prop p args)) = (ν' ∈ fml_sem J (Prop p args))"
proof -
fix ν ν' and I J :: "('a, 'b, 'c) interp"
assume IA:"Iagree I J (SIGF (Prop p args))"
have subs:"⋀i. {Inl x | x. x ∈ SIGT (args i)} ⊆ (SIGF (Prop p args))"
by auto
have IAs:"⋀i. Iagree I J {Inl x | x. x ∈ SIGT (args i)}"
using IA apply(unfold SIGF.simps)
subgoal for i
using Iagree_sub[OF subs[of i]] by auto
done
have mem:"Inr (Inr p) ∈ {Inr (Inr p)} ∪ {Inl x |x. x ∈ (⋃i. SIGT (args i))}"
by auto
from IA have pSame:"Predicates I p = Predicates J p"
by (auto simp add: Iagree_Pred IA mem)
assume VA:"Vagree ν ν' (FVF (Prop p args))"
hence VAs:"⋀i. Vagree ν ν' (FVT (args i))"
unfolding FVF.simps Vagree_def by auto
have sems:"⋀i. dterm_sem I (args i) ν = dterm_sem J (args i) ν'"
using IAs VAs coincidence_dterm' rangeI safes
by (simp add: coincidence_dterm')
hence vecSem:"(χ i. dterm_sem I (args i) ν) = (χ i. dterm_sem J (args i) ν')"
by auto
show "(ν ∈ fml_sem I (Prop p args)) = (ν' ∈ fml_sem J (Prop p args))"
apply(unfold fml_sem.simps mem_Collect_eq)
using IA vecSem pSame by (auto)
qed
then show "?case" unfolding coincide_fml_def by blast
next
case fsafe_Not then show "?case" by auto
next
case (fsafe_And p1 p2)
then have safes:"fsafe p1" "fsafe p2"
and IH1:"∀ ν ν' I J. Iagree I J (SIGF p1) ⟶ Vagree ν ν' (FVF p1) ⟶ (ν ∈ fml_sem I p1) = (ν' ∈ fml_sem J p1)"
and IH2:"∀ ν ν' I J. Iagree I J (SIGF p2) ⟶ Vagree ν ν' (FVF p2) ⟶ (ν ∈ fml_sem I p2) = (ν' ∈ fml_sem J p2)"
by auto
have almost:"⋀ν ν' I J. Iagree I J (SIGF (And p1 p2)) ⟹ Vagree ν ν' (FVF (And p1 p2)) ⟹ (ν ∈ fml_sem I (And p1 p2)) = (ν' ∈ fml_sem J (And p1 p2))"
proof -
fix ν ν' I J
assume IA:"Iagree I J (SIGF (And p1 p2))"
have IAsubs:"(SIGF p1) ⊆ (SIGF (And p1 p2))" "(SIGF p2) ⊆ (SIGF (And p1 p2))" by auto
from IA have IAs:"Iagree I J (SIGF p1)" "Iagree I J (SIGF p2)"
using Iagree_sub[OF IAsubs(1)] Iagree_sub[OF IAsubs(2)] by auto
assume VA:"Vagree ν ν' (FVF (And p1 p2))"
hence VAs:"Vagree ν ν' (FVF p1)" "Vagree ν ν' (FVF p2)"
unfolding FVF.simps Vagree_def by auto
have eq1:"(ν ∈ fml_sem I p1) = (ν' ∈ fml_sem J p1)" using IH1 IAs VAs by blast
have eq2:"(ν ∈ fml_sem I p2) = (ν' ∈ fml_sem J p2)" using IH2 IAs VAs by blast
show "(ν ∈ fml_sem I (And p1 p2)) = (ν' ∈ fml_sem J (And p1 p2))"
using eq1 eq2 by auto
qed
then show "?case" unfolding coincide_fml_def by blast
next
case (fsafe_Exists p x)
then have safe:"fsafe p"
and IH:"∀ ν ν' I J. Iagree I J (SIGF p) ⟶ Vagree ν ν' (FVF p) ⟶ (ν ∈ fml_sem I p) = (ν' ∈ fml_sem J p)"
by auto
have almost:"⋀ν ν' I J. Iagree I J (SIGF (Exists x p)) ⟹ Vagree ν ν' (FVF (Exists x p)) ⟹ (ν ∈ fml_sem I (Exists x p)) = (ν' ∈ fml_sem J (Exists x p))"
proof -
fix ν ν' I J
assume IA:"Iagree I J (SIGF (Exists x p))"
hence IA':"Iagree I J (SIGF p)"
unfolding SIGF.simps Iagree_def by auto
assume VA:"Vagree ν ν' (FVF (Exists x p))"
hence VA':"Vagree ν ν' (FVF p - {Inl x})" by auto
hence VA'':"⋀r. Vagree (repv ν x r) (repv ν' x r) (FVF p)"
subgoal for r
unfolding Vagree_def FVF.simps repv.simps
by auto
done
have IH': "⋀r. Iagree I J (SIGF p) ⟹ Vagree (repv ν x r) (repv ν' x r) (FVF p) ⟹ ((repv ν x r) ∈ fml_sem I p) = ((repv ν' x r) ∈ fml_sem J p)"
subgoal for r
using IH apply(rule allE[where x = "repv ν x r"])
apply(erule allE[where x = "repv ν' x r"])
by (auto)
done
hence IH'':"⋀r. ((repv ν x r) ∈ fml_sem I p) = ((repv ν' x r) ∈ fml_sem J p)"
subgoal for r
using IA' VA'' by auto
done
have fact:"⋀r. (repv ν x r ∈ fml_sem I p) = (repv ν' x r ∈ fml_sem J p)"
subgoal for r
using IH'[OF IA' VA''] by auto
done
show "(ν ∈ fml_sem I (Exists x p)) = (ν' ∈ fml_sem J (Exists x p))"
apply(simp only: fml_sem.simps mem_Collect_eq)
using IH'' by auto
qed
then show "?case" unfolding coincide_fml_def by blast
next
case (fsafe_Diamond a p) then
have hsafe:"hpsafe a"
and psafe:"fsafe p"
and IH1:"∀ I J. (∀ν ν' μ V. Iagree I J (SIGP a) ⟶
Vagree ν ν' V ⟶
FVP a ⊆ V ⟶ (ν, μ) ∈ prog_sem I a ⟶ (∃μ'. (ν', μ') ∈ prog_sem J a ∧ Vagree μ μ' (MBV a ∪ V)))"
and IH2:"∀ν ν' I J. Iagree I J (SIGF p) ⟶ Vagree ν ν' (FVF p) ⟶ (ν ∈ fml_sem I p) = (ν' ∈ fml_sem J p)"
unfolding coincide_hp'_def coincide_hp_def coincide_fml_def apply auto done
have almost:"⋀ν ν' I J. Iagree I J (SIGF (Diamond a p)) ⟹ Vagree ν ν' (FVF (Diamond a p)) ⟹ (ν ∈ fml_sem I (Diamond a p)) = (ν' ∈ fml_sem J (Diamond a p))"
proof -
fix ν ν' I J
assume IA:"Iagree I J (SIGF (Diamond a p))"
have IAsubs:"(SIGP a) ⊆ (SIGF (Diamond a p))" "(SIGF p) ⊆ (SIGF (Diamond a p))" by auto
from IA have IAP:"Iagree I J (SIGP a)"
and IAF:"Iagree I J (SIGF p)" using Iagree_sub[OF IAsubs(1)] Iagree_sub[OF IAsubs(2)] by auto
from IAP have IAP':"Iagree J I (SIGP a)" by (rule Iagree_comm)
from IAF have IAF':"Iagree J I (SIGF p)" by (rule Iagree_comm)
assume VA:"Vagree ν ν' (FVF (Diamond a p))"
hence VA':"Vagree ν' ν (FVF (Diamond a p))" by (rule agree_comm)
have dir1:"ν ∈ fml_sem I (Diamond a p) ⟹ ν' ∈ fml_sem J (Diamond a p)"
proof -
assume sem:"ν ∈ fml_sem I (Diamond a p)"
let ?V = "FVF (Diamond a p)"
have Vsup:"FVP a ⊆ ?V" by auto
obtain μ where prog:"(ν, μ) ∈ prog_sem I a" and fml:"μ ∈ fml_sem I p"
using sem by auto
from IH1 have IH1':
"Iagree I J (SIGP a) ⟹
Vagree ν ν' ?V ⟹
FVP a ⊆ ?V ⟹ (ν, μ) ∈ prog_sem I a ⟹ (∃μ'. (ν', μ') ∈ prog_sem J a ∧ Vagree μ μ' (MBV a ∪ ?V))"
by blast
obtain μ' where prog':"(ν', μ') ∈ prog_sem J a" and agree:"Vagree μ μ' (MBV a ∪ ?V)"
using IH1'[OF IAP VA Vsup prog] by blast
from IH2
have IH2':"Iagree I J (SIGF p) ⟹ Vagree μ μ' (FVF p) ⟹ (μ ∈ fml_sem I p) = (μ' ∈ fml_sem J p)"
by blast
have VAF:"Vagree μ μ' (FVF p)"
using agree VA by (auto simp only: Vagree_def FVF.simps)
hence IH2'':"(μ ∈ fml_sem I p) = (μ' ∈ fml_sem J p)"
using IH2'[OF IAF VAF] by auto
have fml':"μ' ∈ fml_sem J p" using IH2'' fml by auto
have "∃ μ'. (ν', μ') ∈ prog_sem J a ∧ μ' ∈ fml_sem J p" using fml' prog' by blast
then show "ν' ∈ fml_sem J (Diamond a p)"
unfolding fml_sem.simps by (auto simp only: mem_Collect_eq)
qed
have dir2:"ν' ∈ fml_sem J (Diamond a p) ⟹ ν ∈ fml_sem I (Diamond a p)"
proof -
assume sem:"ν' ∈ fml_sem J (Diamond a p)"
let ?V = "FVF (Diamond a p)"
have Vsup:"FVP a ⊆ ?V" by auto
obtain μ where prog:"(ν', μ) ∈ prog_sem J a" and fml:"μ ∈ fml_sem J p"
using sem by auto
from IH1 have IH1':
"Iagree J I (SIGP a) ⟹
Vagree ν' ν ?V ⟹
FVP a ⊆ ?V ⟹ (ν', μ) ∈ prog_sem J a ⟹ (∃μ'. (ν, μ') ∈ prog_sem I a ∧ Vagree μ μ' (MBV a ∪ ?V))"
by blast
obtain μ' where prog':"(ν, μ') ∈ prog_sem I a" and agree:"Vagree μ μ' (MBV a ∪ ?V)"
using IH1'[OF IAP' VA' Vsup prog] by blast
from IH2
have IH2':"Iagree J I (SIGF p) ⟹ Vagree μ μ' (FVF p) ⟹ (μ ∈ fml_sem J p) = (μ' ∈ fml_sem I p)"
by blast
have VAF:"Vagree μ μ' (FVF p)"
using agree VA by (auto simp only: Vagree_def FVF.simps)
hence IH2'':"(μ ∈ fml_sem J p) = (μ' ∈ fml_sem I p)"
using IH2'[OF IAF' VAF] by auto
have fml':"μ' ∈ fml_sem I p" using IH2'' fml by auto
have "∃ μ'. (ν, μ') ∈ prog_sem I a ∧ μ' ∈ fml_sem I p" using fml' prog' by blast
then show "ν ∈ fml_sem I (Diamond a p)"
unfolding fml_sem.simps by (auto simp only: mem_Collect_eq)
qed
show "(ν ∈ fml_sem I (Diamond a p)) = (ν' ∈ fml_sem J (Diamond a p))"
using dir1 dir2 by auto
qed
then show "?case" unfolding coincide_fml_def by blast
next
case (fsafe_InContext φ) then
have safe:"fsafe φ"
and IH:"(∀ ν ν' I J. Iagree I J (SIGF φ) ⟶ Vagree ν ν' (FVF φ) ⟶ ν ∈ fml_sem I φ ⟷ ν' ∈ fml_sem J φ)"
by (unfold coincide_fml_def)
hence IH':"⋀ν ν' I J. Iagree I J (SIGF φ) ⟹ Vagree ν ν' (FVF φ) ⟹ ν ∈ fml_sem I φ ⟷ ν' ∈ fml_sem J φ"
by auto
hence sem_eq:"⋀I J. Iagree I J (SIGF φ) ⟹ fml_sem I φ = fml_sem J φ"
apply (auto simp: Collect_cong Collect_mem_eq agree_refl)
using agree_refl by blast+
have "(⋀ ν ν' I J C . Iagree I J (SIGF (InContext C φ)) ⟹ Vagree ν ν' (FVF (InContext C φ)) ⟹ ν ∈ fml_sem I (InContext C φ) ⟷ ν' ∈ fml_sem J (InContext C φ))"
proof -
fix ν ν' I J C
assume IA:"Iagree I J (SIGF (InContext C φ))"
then have IA':"Iagree I J (SIGF φ)" unfolding SIGF.simps Iagree_def by auto
assume VA:"Vagree ν ν' (FVF (InContext C φ))"
then have VAU:"Vagree ν ν' UNIV" unfolding FVF.simps Vagree_def by auto
then have VA':"Vagree ν ν' (FVF φ)" unfolding FVF.simps Vagree_def by auto
from VAU have eq:"ν = ν'" by (cases "ν", cases "ν'", auto simp add: vec_eq_iff Vagree_def)
from IA have Cmem:"Inr (Inl C) ∈ SIGF (InContext C φ)"
by simp
have Cagree:"Contexts I C = Contexts J C" by (rule Iagree_Contexts[OF IA Cmem])
show "ν ∈ fml_sem I (InContext C φ) ⟷ ν' ∈ fml_sem J (InContext C φ)"
using Cagree eq sem_eq IA' by (auto)
qed
then show "?case" by simp
qed
lemma coincidence_formula:"⋀ν ν' I J. fsafe (φ::('a::finite, 'b::finite, 'c::finite) formula) ⟹ Iagree I J (SIGF φ) ⟹ Vagree ν ν' (FVF φ) ⟹ (ν ∈ fml_sem I φ ⟷ ν' ∈ fml_sem J φ)"
using coincidence_hp_fml unfolding coincide_fml_def by blast
lemma coincidence_hp:
fixes ν ν' μ V I J
assumes safe:"hpsafe (α::('a::finite, 'b::finite, 'c::finite) hp)"
assumes IA:"Iagree I J (SIGP α)"
assumes VA:"Vagree ν ν' V"
assumes sub:"V ⊇ (FVP α)"
assumes sem:"(ν, μ) ∈ prog_sem I α"
shows "(∃μ'. (ν', μ') ∈ prog_sem J α ∧ Vagree μ μ' (MBV α ∪ V))"
proof -
have thing:"(∀I J. (∀ν ν' μ V.
Iagree I J (SIGP α) ⟶
Vagree ν ν' V ⟶ FVP α ⊆ V ⟶ (ν, μ) ∈ prog_sem I α ⟶ (∃μ'. (ν', μ') ∈ prog_sem J α ∧ Vagree μ μ' (MBV α ∪ V))) ∧
ode_sem_equiv α I)"
using coincidence_hp_fml unfolding coincide_hp_def coincide_hp'_def
using safe by blast
then have "(Iagree I J (SIGP α) ⟹
Vagree ν ν' V ⟹ FVP α ⊆ V ⟹ (ν, μ) ∈ prog_sem I α ⟹ (∃μ'. (ν', μ') ∈ prog_sem J α ∧ Vagree μ μ' (MBV α ∪ V)))"
using IA VA sub sem thing by blast
then show "(∃μ'. (ν', μ') ∈ prog_sem J α ∧ Vagree μ μ' (MBV α ∪ V))"
using IA VA sub sem by auto
qed
subsection ‹Corollaries: Alternate ODE semantics definition›
lemma ode_sem_eq:
fixes I::"('a::finite,'b::finite,'c::finite) interp" and ODE::"('a,'c) ODE" and φ::"('a,'b,'c) formula"
assumes osafe:"osafe ODE"
assumes fsafe:"fsafe φ"
shows
"({(ν, mk_v I ODE ν (sol t)) | ν sol t.
t ≥ 0 ∧
(sol solves_ode (λ_. ODE_sem I ODE)) {0..t} {x. mk_v I ODE ν x ∈ fml_sem I φ} ∧
VSagree (sol 0) (fst ν) {x | x. Inl x ∈ FVP (EvolveODE ODE φ)}}) =
({(ν, mk_v I ODE ν (sol t)) | ν sol t.
t ≥ 0 ∧
(sol solves_ode (λ_. ODE_sem I ODE)) {0..t} {x. mk_v I ODE ν x ∈ fml_sem I φ} ∧
(sol 0) = (fst ν)})"
proof -
have hpsafe:"hpsafe (EvolveODE ODE φ)" using osafe fsafe by (auto intro: hpsafe_fsafe.intros)
have "coincide_hp'(EvolveODE ODE φ)" using coincidence_hp_fml hpsafe by blast
hence "ode_sem_equiv (EvolveODE ODE φ) I" unfolding coincide_hp'_def by auto
then show "?thesis"
unfolding ode_sem_equiv_def using osafe fsafe by auto
qed
lemma ode_alt_sem:"⋀I::('a::finite,'b::finite,'c::finite) interp. ⋀ODE::('a,'c) ODE. ⋀φ::('a,'b,'c)formula. osafe ODE ⟹ fsafe φ ⟹
prog_sem I (EvolveODE ODE φ)
=
{(ν, mk_v I ODE ν (sol t)) | ν sol t.
t ≥ 0 ∧
(sol solves_ode (λ_. ODE_sem I ODE)) {0..t} {x. mk_v I ODE ν x ∈ fml_sem I φ} ∧
VSagree (sol 0) (fst ν) {x | x. Inl x ∈ FVP (EvolveODE ODE φ)}}
"
subgoal for I ODE φ
using ode_sem_eq[of ODE φ I] by auto
done
end
end