[STATEMENT]
lemma adjoint_consequence:"(\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f') \<Longrightarrow> (\<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f') \<Longrightarrow> Vagree \<nu> \<omega> (FVS \<sigma>) \<Longrightarrow> adjoint I \<sigma> \<nu> = adjoint I \<sigma> \<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (FVS \<sigma>)\<rbrakk> \<Longrightarrow> local.adjoint I \<sigma> \<nu> = local.adjoint I \<sigma> \<omega>
[PROOF STEP]
apply(unfold FVS_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>)))\<rbrakk> \<Longrightarrow> local.adjoint I \<sigma> \<nu> = local.adjoint I \<sigma> \<omega>
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>)))\<rbrakk> \<Longrightarrow> local.adjoint I \<sigma> \<nu> = local.adjoint I \<sigma> \<omega>
[PROOF STEP]
apply(unfold adjoint_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>)))\<rbrakk> \<Longrightarrow> \<lparr>Functions = \<lambda>f. case SFunctions \<sigma> f of None \<Rightarrow> Functions I f | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<nu>, Predicates = \<lambda>p. case SPredicates \<sigma> p of None \<Rightarrow> Predicates I p | Some p' \<Rightarrow> \<lambda>R. \<nu> \<in> fml_sem (extendf I R) p', Contexts = \<lambda>c. case SContexts \<sigma> c of None \<Rightarrow> Contexts I c | Some c' \<Rightarrow> \<lambda>R. fml_sem (extendc I R) c', Programs = \<lambda>a. case SPrograms \<sigma> a of None \<Rightarrow> Programs I a | Some x \<Rightarrow> prog_sem I x, ODEs = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEs I ode | Some x \<Rightarrow> ODE_sem I x, ODEBV = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEBV I ode | Some x \<Rightarrow> ODE_vars I x\<rparr> = \<lparr>Functions = \<lambda>f. case SFunctions \<sigma> f of None \<Rightarrow> Functions I f | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<omega>, Predicates = \<lambda>p. case SPredicates \<sigma> p of None \<Rightarrow> Predicates I p | Some p' \<Rightarrow> \<lambda>R. \<omega> \<in> fml_sem (extendf I R) p', Contexts = \<lambda>c. case SContexts \<sigma> c of None \<Rightarrow> Contexts I c | Some c' \<Rightarrow> \<lambda>R. fml_sem (extendc I R) c', Programs = \<lambda>a. case SPrograms \<sigma> a of None \<Rightarrow> Programs I a | Some x \<Rightarrow> prog_sem I x, ODEs = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEs I ode | Some x \<Rightarrow> ODE_sem I x, ODEBV = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEBV I ode | Some x \<Rightarrow> ODE_vars I x\<rparr>
[PROOF STEP]
apply(rule interp_eq)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>)))\<rbrakk> \<Longrightarrow> (\<lambda>f. case SFunctions \<sigma> f of None \<Rightarrow> Functions I f | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<nu>) = (\<lambda>f. case SFunctions \<sigma> f of None \<Rightarrow> Functions I f | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<omega>)
 2. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>)))\<rbrakk> \<Longrightarrow> (\<lambda>p. case SPredicates \<sigma> p of None \<Rightarrow> Predicates I p | Some p' \<Rightarrow> \<lambda>R. \<nu> \<in> fml_sem (extendf I R) p') = (\<lambda>p. case SPredicates \<sigma> p of None \<Rightarrow> Predicates I p | Some p' \<Rightarrow> \<lambda>R. \<omega> \<in> fml_sem (extendf I R) p')
 3. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>)))\<rbrakk> \<Longrightarrow> (\<lambda>c. case SContexts \<sigma> c of None \<Rightarrow> Contexts I c | Some c' \<Rightarrow> \<lambda>R. fml_sem (extendc I R) c') = (\<lambda>c. case SContexts \<sigma> c of None \<Rightarrow> Contexts I c | Some c' \<Rightarrow> \<lambda>R. fml_sem (extendc I R) c')
 4. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>)))\<rbrakk> \<Longrightarrow> (\<lambda>a. case SPrograms \<sigma> a of None \<Rightarrow> Programs I a | Some x \<Rightarrow> prog_sem I x) = (\<lambda>a. case SPrograms \<sigma> a of None \<Rightarrow> Programs I a | Some x \<Rightarrow> prog_sem I x)
 5. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>)))\<rbrakk> \<Longrightarrow> (\<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEs I ode | Some x \<Rightarrow> ODE_sem I x) = (\<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEs I ode | Some x \<Rightarrow> ODE_sem I x)
 6. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>)))\<rbrakk> \<Longrightarrow> (\<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEBV I ode | Some x \<Rightarrow> ODE_vars I x) = (\<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEBV I ode | Some x \<Rightarrow> ODE_vars I x)
[PROOF STEP]
apply(auto simp add: fun_eq_iff)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>)))\<rbrakk> \<Longrightarrow> (case SFunctions \<sigma> x of None \<Rightarrow> Functions I x | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<nu>) xa = (case SFunctions \<sigma> x of None \<Rightarrow> Functions I x | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<omega>) xa
 2. \<And>x xa. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); (case SPredicates \<sigma> x of None \<Rightarrow> Predicates I x | Some p' \<Rightarrow> \<lambda>R. \<nu> \<in> fml_sem (extendf I R) p') xa\<rbrakk> \<Longrightarrow> (case SPredicates \<sigma> x of None \<Rightarrow> Predicates I x | Some p' \<Rightarrow> \<lambda>R. \<omega> \<in> fml_sem (extendf I R) p') xa
 3. \<And>x xa. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); (case SPredicates \<sigma> x of None \<Rightarrow> Predicates I x | Some p' \<Rightarrow> \<lambda>R. \<omega> \<in> fml_sem (extendf I R) p') xa\<rbrakk> \<Longrightarrow> (case SPredicates \<sigma> x of None \<Rightarrow> Predicates I x | Some p' \<Rightarrow> \<lambda>R. \<nu> \<in> fml_sem (extendf I R) p') xa
[PROOF STEP]
subgoal for xa xaa
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>)))\<rbrakk> \<Longrightarrow> (case SFunctions \<sigma> xa of None \<Rightarrow> Functions I xa | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<nu>) xaa = (case SFunctions \<sigma> xa of None \<Rightarrow> Functions I xa | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<omega>) xaa
[PROOF STEP]
apply(cases "SFunctions \<sigma> xa")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); SFunctions \<sigma> xa = None\<rbrakk> \<Longrightarrow> (case SFunctions \<sigma> xa of None \<Rightarrow> Functions I xa | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<nu>) xaa = (case SFunctions \<sigma> xa of None \<Rightarrow> Functions I xa | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<omega>) xaa
 2. \<And>a. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); SFunctions \<sigma> xa = Some a\<rbrakk> \<Longrightarrow> (case SFunctions \<sigma> xa of None \<Rightarrow> Functions I xa | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<nu>) xaa = (case SFunctions \<sigma> xa of None \<Rightarrow> Functions I xa | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<omega>) xaa
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); SFunctions \<sigma> xa = Some a\<rbrakk> \<Longrightarrow> dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a \<nu> = dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a \<omega>
[PROOF STEP]
subgoal for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); SFunctions \<sigma> xa = Some a\<rbrakk> \<Longrightarrow> dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a \<nu> = dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a \<omega>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); SFunctions \<sigma> xa = Some a\<rbrakk> \<Longrightarrow> dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a \<nu> = dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a \<omega>
[PROOF STEP]
assume safes:"(\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f')"
[PROOF STATE]
proof (state)
this:
SFunctions \<sigma> ?f7 = Some ?f'7 \<Longrightarrow> dsafe ?f'7

goal (1 subgoal):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); SFunctions \<sigma> xa = Some a\<rbrakk> \<Longrightarrow> dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a \<nu> = dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a \<omega>
[PROOF STEP]
assume agrees:"Vagree \<nu> \<omega> (\<Union>x. SFV \<sigma> x)"
[PROOF STATE]
proof (state)
this:
Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>)))

goal (1 subgoal):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); SFunctions \<sigma> xa = Some a\<rbrakk> \<Longrightarrow> dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a \<nu> = dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a \<omega>
[PROOF STEP]
assume some:"SFunctions \<sigma> xa = Some a"
[PROOF STATE]
proof (state)
this:
SFunctions \<sigma> xa = Some a

goal (1 subgoal):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); SFunctions \<sigma> xa = Some a\<rbrakk> \<Longrightarrow> dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a \<nu> = dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a \<omega>
[PROOF STEP]
from safes some
[PROOF STATE]
proof (chain)
picking this:
SFunctions \<sigma> ?f7 = Some ?f'7 \<Longrightarrow> dsafe ?f'7
SFunctions \<sigma> xa = Some a
[PROOF STEP]
have safe:"dsafe a"
[PROOF STATE]
proof (prove)
using this:
SFunctions \<sigma> ?f7 = Some ?f'7 \<Longrightarrow> dsafe ?f'7
SFunctions \<sigma> xa = Some a

goal (1 subgoal):
 1. dsafe a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dsafe a

goal (1 subgoal):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); SFunctions \<sigma> xa = Some a\<rbrakk> \<Longrightarrow> dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a \<nu> = dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a \<omega>
[PROOF STEP]
have sub:"SFV \<sigma> (Inl xa) \<subseteq> (\<Union>x. SFV \<sigma> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SFV \<sigma> (Inl xa) \<subseteq> \<Union> (range (SFV \<sigma>))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
SFV \<sigma> (Inl xa) \<subseteq> \<Union> (range (SFV \<sigma>))

goal (1 subgoal):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); SFunctions \<sigma> xa = Some a\<rbrakk> \<Longrightarrow> dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a \<nu> = dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a \<omega>
[PROOF STEP]
from agrees
[PROOF STATE]
proof (chain)
picking this:
Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>)))
[PROOF STEP]
have "Vagree \<nu> \<omega> (SFV \<sigma> (Inl xa))"
[PROOF STATE]
proof (prove)
using this:
Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>)))

goal (1 subgoal):
 1. Vagree \<nu> \<omega> (SFV \<sigma> (Inl xa))
[PROOF STEP]
using agree_sub[OF sub agrees]
[PROOF STATE]
proof (prove)
using this:
Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>)))
Vagree \<nu> \<omega> (SFV \<sigma> (Inl xa))

goal (1 subgoal):
 1. Vagree \<nu> \<omega> (SFV \<sigma> (Inl xa))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Vagree \<nu> \<omega> (SFV \<sigma> (Inl xa))

goal (1 subgoal):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); SFunctions \<sigma> xa = Some a\<rbrakk> \<Longrightarrow> dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a \<nu> = dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a \<omega>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Vagree \<nu> \<omega> (SFV \<sigma> (Inl xa))
[PROOF STEP]
have agree:"Vagree \<nu> \<omega> (FVT a)"
[PROOF STATE]
proof (prove)
using this:
Vagree \<nu> \<omega> (SFV \<sigma> (Inl xa))

goal (1 subgoal):
 1. Vagree \<nu> \<omega> (FVT a)
[PROOF STEP]
using some
[PROOF STATE]
proof (prove)
using this:
Vagree \<nu> \<omega> (SFV \<sigma> (Inl xa))
SFunctions \<sigma> xa = Some a

goal (1 subgoal):
 1. Vagree \<nu> \<omega> (FVT a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Vagree \<nu> \<omega> (FVT a)

goal (1 subgoal):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); SFunctions \<sigma> xa = Some a\<rbrakk> \<Longrightarrow> dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a \<nu> = dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a \<omega>
[PROOF STEP]
show "?thesis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a \<nu> = dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a \<omega>
[PROOF STEP]
using coincidence_dterm[of a, OF safes[of xa a, OF some] agree]
[PROOF STATE]
proof (prove)
using this:
dterm_sem ?I a \<nu> = dterm_sem ?I a \<omega>

goal (1 subgoal):
 1. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a \<nu> = dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a \<omega>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a \<nu> = dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a \<omega>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); (case SPredicates \<sigma> x of None \<Rightarrow> Predicates I x | Some p' \<Rightarrow> \<lambda>R. \<nu> \<in> fml_sem (extendf I R) p') xa\<rbrakk> \<Longrightarrow> (case SPredicates \<sigma> x of None \<Rightarrow> Predicates I x | Some p' \<Rightarrow> \<lambda>R. \<omega> \<in> fml_sem (extendf I R) p') xa
 2. \<And>x xa. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); (case SPredicates \<sigma> x of None \<Rightarrow> Predicates I x | Some p' \<Rightarrow> \<lambda>R. \<omega> \<in> fml_sem (extendf I R) p') xa\<rbrakk> \<Longrightarrow> (case SPredicates \<sigma> x of None \<Rightarrow> Predicates I x | Some p' \<Rightarrow> \<lambda>R. \<nu> \<in> fml_sem (extendf I R) p') xa
[PROOF STEP]
subgoal for xa xaa
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); (case SPredicates \<sigma> xa of None \<Rightarrow> Predicates I xa | Some p' \<Rightarrow> \<lambda>R. \<nu> \<in> fml_sem (extendf I R) p') xaa\<rbrakk> \<Longrightarrow> (case SPredicates \<sigma> xa of None \<Rightarrow> Predicates I xa | Some p' \<Rightarrow> \<lambda>R. \<omega> \<in> fml_sem (extendf I R) p') xaa
[PROOF STEP]
apply(cases "SPredicates \<sigma> xa")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); (case SPredicates \<sigma> xa of None \<Rightarrow> Predicates I xa | Some p' \<Rightarrow> \<lambda>R. \<nu> \<in> fml_sem (extendf I R) p') xaa; SPredicates \<sigma> xa = None\<rbrakk> \<Longrightarrow> (case SPredicates \<sigma> xa of None \<Rightarrow> Predicates I xa | Some p' \<Rightarrow> \<lambda>R. \<omega> \<in> fml_sem (extendf I R) p') xaa
 2. \<And>a. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); (case SPredicates \<sigma> xa of None \<Rightarrow> Predicates I xa | Some p' \<Rightarrow> \<lambda>R. \<nu> \<in> fml_sem (extendf I R) p') xaa; SPredicates \<sigma> xa = Some a\<rbrakk> \<Longrightarrow> (case SPredicates \<sigma> xa of None \<Rightarrow> Predicates I xa | Some p' \<Rightarrow> \<lambda>R. \<omega> \<in> fml_sem (extendf I R) p') xaa
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); \<nu> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a; SPredicates \<sigma> xa = Some a\<rbrakk> \<Longrightarrow> \<omega> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a
[PROOF STEP]
subgoal for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); \<nu> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a; SPredicates \<sigma> xa = Some a\<rbrakk> \<Longrightarrow> \<omega> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); \<nu> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a; SPredicates \<sigma> xa = Some a\<rbrakk> \<Longrightarrow> \<omega> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a
[PROOF STEP]
assume safes:"(\<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f')"
[PROOF STATE]
proof (state)
this:
SPredicates \<sigma> ?f7 = Some ?f'7 \<Longrightarrow> fsafe ?f'7

goal (1 subgoal):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); \<nu> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a; SPredicates \<sigma> xa = Some a\<rbrakk> \<Longrightarrow> \<omega> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a
[PROOF STEP]
assume agrees:"Vagree \<nu> \<omega> (\<Union>x. SFV \<sigma> x)"
[PROOF STATE]
proof (state)
this:
Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>)))

goal (1 subgoal):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); \<nu> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a; SPredicates \<sigma> xa = Some a\<rbrakk> \<Longrightarrow> \<omega> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a
[PROOF STEP]
assume some:"SPredicates \<sigma> xa = Some a"
[PROOF STATE]
proof (state)
this:
SPredicates \<sigma> xa = Some a

goal (1 subgoal):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); \<nu> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a; SPredicates \<sigma> xa = Some a\<rbrakk> \<Longrightarrow> \<omega> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a
[PROOF STEP]
assume sem:"\<nu> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I,
                  ODEs = ODEs I, ODEBV = ODEBV I\<rparr>
        a"
[PROOF STATE]
proof (state)
this:
\<nu> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a

goal (1 subgoal):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); \<nu> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a; SPredicates \<sigma> xa = Some a\<rbrakk> \<Longrightarrow> \<omega> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a
[PROOF STEP]
from safes some
[PROOF STATE]
proof (chain)
picking this:
SPredicates \<sigma> ?f7 = Some ?f'7 \<Longrightarrow> fsafe ?f'7
SPredicates \<sigma> xa = Some a
[PROOF STEP]
have safe:"fsafe a"
[PROOF STATE]
proof (prove)
using this:
SPredicates \<sigma> ?f7 = Some ?f'7 \<Longrightarrow> fsafe ?f'7
SPredicates \<sigma> xa = Some a

goal (1 subgoal):
 1. fsafe a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fsafe a

goal (1 subgoal):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); \<nu> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a; SPredicates \<sigma> xa = Some a\<rbrakk> \<Longrightarrow> \<omega> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a
[PROOF STEP]
have sub:"SFV \<sigma> (Inr (Inr xa)) \<subseteq> (\<Union>x. SFV \<sigma> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SFV \<sigma> (Inr (Inr xa)) \<subseteq> \<Union> (range (SFV \<sigma>))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
SFV \<sigma> (Inr (Inr xa)) \<subseteq> \<Union> (range (SFV \<sigma>))

goal (1 subgoal):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); \<nu> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a; SPredicates \<sigma> xa = Some a\<rbrakk> \<Longrightarrow> \<omega> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a
[PROOF STEP]
from agrees
[PROOF STATE]
proof (chain)
picking this:
Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>)))
[PROOF STEP]
have "Vagree \<nu> \<omega> (SFV \<sigma> (Inr (Inr xa)))"
[PROOF STATE]
proof (prove)
using this:
Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>)))

goal (1 subgoal):
 1. Vagree \<nu> \<omega> (SFV \<sigma> (Inr (Inr xa)))
[PROOF STEP]
using agree_sub[OF sub agrees]
[PROOF STATE]
proof (prove)
using this:
Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>)))
Vagree \<nu> \<omega> (SFV \<sigma> (Inr (Inr xa)))

goal (1 subgoal):
 1. Vagree \<nu> \<omega> (SFV \<sigma> (Inr (Inr xa)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Vagree \<nu> \<omega> (SFV \<sigma> (Inr (Inr xa)))

goal (1 subgoal):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); \<nu> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a; SPredicates \<sigma> xa = Some a\<rbrakk> \<Longrightarrow> \<omega> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Vagree \<nu> \<omega> (SFV \<sigma> (Inr (Inr xa)))
[PROOF STEP]
have agree:"Vagree \<nu> \<omega> (FVF a)"
[PROOF STATE]
proof (prove)
using this:
Vagree \<nu> \<omega> (SFV \<sigma> (Inr (Inr xa)))

goal (1 subgoal):
 1. Vagree \<nu> \<omega> (FVF a)
[PROOF STEP]
using some
[PROOF STATE]
proof (prove)
using this:
Vagree \<nu> \<omega> (SFV \<sigma> (Inr (Inr xa)))
SPredicates \<sigma> xa = Some a

goal (1 subgoal):
 1. Vagree \<nu> \<omega> (FVF a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Vagree \<nu> \<omega> (FVF a)

goal (1 subgoal):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); \<nu> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a; SPredicates \<sigma> xa = Some a\<rbrakk> \<Longrightarrow> \<omega> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a
[PROOF STEP]
let ?I' = "\<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I,
                  ODEs = ODEs I, ODEBV = ODEBV I\<rparr>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); \<nu> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a; SPredicates \<sigma> xa = Some a\<rbrakk> \<Longrightarrow> \<omega> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a
[PROOF STEP]
have IA:"\<And>S. Iagree ?I' ?I' (SIGF a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S. Iagree \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (SIGF a)
[PROOF STEP]
using Iagree_refl
[PROOF STATE]
proof (prove)
using this:
Iagree ?I ?I ?A

goal (1 subgoal):
 1. \<And>S. Iagree \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (SIGF a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Iagree \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (SIGF a)

goal (1 subgoal):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); \<nu> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a; SPredicates \<sigma> xa = Some a\<rbrakk> \<Longrightarrow> \<omega> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a
[PROOF STEP]
show "?thesis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<omega> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a
[PROOF STEP]
using coincidence_formula[of a, OF safes[of xa a, OF some] IA agree] sem
[PROOF STATE]
proof (prove)
using this:
(\<nu> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a) = (\<omega> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a)
\<nu> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a

goal (1 subgoal):
 1. \<omega> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<omega> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); (case SPredicates \<sigma> x of None \<Rightarrow> Predicates I x | Some p' \<Rightarrow> \<lambda>R. \<omega> \<in> fml_sem (extendf I R) p') xa\<rbrakk> \<Longrightarrow> (case SPredicates \<sigma> x of None \<Rightarrow> Predicates I x | Some p' \<Rightarrow> \<lambda>R. \<nu> \<in> fml_sem (extendf I R) p') xa
[PROOF STEP]
subgoal for xa xaa
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); (case SPredicates \<sigma> xa of None \<Rightarrow> Predicates I xa | Some p' \<Rightarrow> \<lambda>R. \<omega> \<in> fml_sem (extendf I R) p') xaa\<rbrakk> \<Longrightarrow> (case SPredicates \<sigma> xa of None \<Rightarrow> Predicates I xa | Some p' \<Rightarrow> \<lambda>R. \<nu> \<in> fml_sem (extendf I R) p') xaa
[PROOF STEP]
apply(cases "SPredicates \<sigma> xa")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); (case SPredicates \<sigma> xa of None \<Rightarrow> Predicates I xa | Some p' \<Rightarrow> \<lambda>R. \<omega> \<in> fml_sem (extendf I R) p') xaa; SPredicates \<sigma> xa = None\<rbrakk> \<Longrightarrow> (case SPredicates \<sigma> xa of None \<Rightarrow> Predicates I xa | Some p' \<Rightarrow> \<lambda>R. \<nu> \<in> fml_sem (extendf I R) p') xaa
 2. \<And>a. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); (case SPredicates \<sigma> xa of None \<Rightarrow> Predicates I xa | Some p' \<Rightarrow> \<lambda>R. \<omega> \<in> fml_sem (extendf I R) p') xaa; SPredicates \<sigma> xa = Some a\<rbrakk> \<Longrightarrow> (case SPredicates \<sigma> xa of None \<Rightarrow> Predicates I xa | Some p' \<Rightarrow> \<lambda>R. \<nu> \<in> fml_sem (extendf I R) p') xaa
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); \<omega> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a; SPredicates \<sigma> xa = Some a\<rbrakk> \<Longrightarrow> \<nu> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a
[PROOF STEP]
subgoal for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); \<omega> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a; SPredicates \<sigma> xa = Some a\<rbrakk> \<Longrightarrow> \<nu> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); \<omega> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a; SPredicates \<sigma> xa = Some a\<rbrakk> \<Longrightarrow> \<nu> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a
[PROOF STEP]
assume safes:"(\<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f')"
[PROOF STATE]
proof (state)
this:
SPredicates \<sigma> ?f7 = Some ?f'7 \<Longrightarrow> fsafe ?f'7

goal (1 subgoal):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); \<omega> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a; SPredicates \<sigma> xa = Some a\<rbrakk> \<Longrightarrow> \<nu> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a
[PROOF STEP]
assume agrees:"Vagree \<nu> \<omega> (\<Union>x. SFV \<sigma> x)"
[PROOF STATE]
proof (state)
this:
Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>)))

goal (1 subgoal):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); \<omega> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a; SPredicates \<sigma> xa = Some a\<rbrakk> \<Longrightarrow> \<nu> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a
[PROOF STEP]
assume some:"SPredicates \<sigma> xa = Some a"
[PROOF STATE]
proof (state)
this:
SPredicates \<sigma> xa = Some a

goal (1 subgoal):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); \<omega> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a; SPredicates \<sigma> xa = Some a\<rbrakk> \<Longrightarrow> \<nu> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a
[PROOF STEP]
assume sem:"\<omega> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I,
                  ODEs = ODEs I, ODEBV = ODEBV I\<rparr>
        a"
[PROOF STATE]
proof (state)
this:
\<omega> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a

goal (1 subgoal):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); \<omega> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a; SPredicates \<sigma> xa = Some a\<rbrakk> \<Longrightarrow> \<nu> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a
[PROOF STEP]
from safes some
[PROOF STATE]
proof (chain)
picking this:
SPredicates \<sigma> ?f7 = Some ?f'7 \<Longrightarrow> fsafe ?f'7
SPredicates \<sigma> xa = Some a
[PROOF STEP]
have safe:"fsafe a"
[PROOF STATE]
proof (prove)
using this:
SPredicates \<sigma> ?f7 = Some ?f'7 \<Longrightarrow> fsafe ?f'7
SPredicates \<sigma> xa = Some a

goal (1 subgoal):
 1. fsafe a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fsafe a

goal (1 subgoal):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); \<omega> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a; SPredicates \<sigma> xa = Some a\<rbrakk> \<Longrightarrow> \<nu> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a
[PROOF STEP]
have sub:"SFV \<sigma> (Inr (Inr xa)) \<subseteq> (\<Union>x. SFV \<sigma> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SFV \<sigma> (Inr (Inr xa)) \<subseteq> \<Union> (range (SFV \<sigma>))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
SFV \<sigma> (Inr (Inr xa)) \<subseteq> \<Union> (range (SFV \<sigma>))

goal (1 subgoal):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); \<omega> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a; SPredicates \<sigma> xa = Some a\<rbrakk> \<Longrightarrow> \<nu> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a
[PROOF STEP]
from agrees
[PROOF STATE]
proof (chain)
picking this:
Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>)))
[PROOF STEP]
have "Vagree \<nu> \<omega> (SFV \<sigma> (Inr (Inr xa)))"
[PROOF STATE]
proof (prove)
using this:
Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>)))

goal (1 subgoal):
 1. Vagree \<nu> \<omega> (SFV \<sigma> (Inr (Inr xa)))
[PROOF STEP]
using agree_sub[OF sub agrees]
[PROOF STATE]
proof (prove)
using this:
Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>)))
Vagree \<nu> \<omega> (SFV \<sigma> (Inr (Inr xa)))

goal (1 subgoal):
 1. Vagree \<nu> \<omega> (SFV \<sigma> (Inr (Inr xa)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Vagree \<nu> \<omega> (SFV \<sigma> (Inr (Inr xa)))

goal (1 subgoal):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); \<omega> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a; SPredicates \<sigma> xa = Some a\<rbrakk> \<Longrightarrow> \<nu> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Vagree \<nu> \<omega> (SFV \<sigma> (Inr (Inr xa)))
[PROOF STEP]
have agree:"Vagree \<nu> \<omega> (FVF a)"
[PROOF STATE]
proof (prove)
using this:
Vagree \<nu> \<omega> (SFV \<sigma> (Inr (Inr xa)))

goal (1 subgoal):
 1. Vagree \<nu> \<omega> (FVF a)
[PROOF STEP]
using some
[PROOF STATE]
proof (prove)
using this:
Vagree \<nu> \<omega> (SFV \<sigma> (Inr (Inr xa)))
SPredicates \<sigma> xa = Some a

goal (1 subgoal):
 1. Vagree \<nu> \<omega> (FVF a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Vagree \<nu> \<omega> (FVF a)

goal (1 subgoal):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); \<omega> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a; SPredicates \<sigma> xa = Some a\<rbrakk> \<Longrightarrow> \<nu> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a
[PROOF STEP]
let ?I' = "\<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I,
                  ODEs = ODEs I, ODEBV = ODEBV I\<rparr>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); \<omega> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a; SPredicates \<sigma> xa = Some a\<rbrakk> \<Longrightarrow> \<nu> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a
[PROOF STEP]
have IA:"\<And>S. Iagree ?I' ?I' (SIGF a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S. Iagree \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (SIGF a)
[PROOF STEP]
using Iagree_refl
[PROOF STATE]
proof (prove)
using this:
Iagree ?I ?I ?A

goal (1 subgoal):
 1. \<And>S. Iagree \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (SIGF a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Iagree \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (SIGF a)

goal (1 subgoal):
 1. \<lbrakk>\<And>f f'. SFunctions \<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates \<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree \<nu> \<omega> (\<Union> (range (SFV \<sigma>))); \<omega> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a; SPredicates \<sigma> xa = Some a\<rbrakk> \<Longrightarrow> \<nu> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a
[PROOF STEP]
show "?thesis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a
[PROOF STEP]
using coincidence_formula[of a, OF safes[of xa a, OF some] IA agree] sem
[PROOF STATE]
proof (prove)
using this:
(\<nu> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a) = (\<omega> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a)
\<omega> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a

goal (1 subgoal):
 1. \<nu> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<nu> \<in> fml_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma SIGT_plus1:"Vagree \<nu> \<omega> (\<Union>i\<in>SIGT (Plus t1 t2). case SFunctions \<sigma> i of Some x \<Rightarrow> FVT x | None \<Rightarrow> {})
  \<Longrightarrow> Vagree \<nu> \<omega> (\<Union>i\<in>SIGT t1. case SFunctions \<sigma> i of Some x \<Rightarrow> FVT x | None \<Rightarrow> {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Vagree \<nu> \<omega> (\<Union>i\<in>SIGT (Plus t1 t2). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<Longrightarrow> Vagree \<nu> \<omega> (\<Union>i\<in>SIGT t1. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)
[PROOF STEP]
unfolding Vagree_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>i. Inl i \<in> (\<Union>i\<in>SIGT (Plus t1 t2). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<longrightarrow> fst \<nu> $ i = fst \<omega> $ i) \<and> (\<forall>i. Inr i \<in> (\<Union>i\<in>SIGT (Plus t1 t2). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<longrightarrow> snd \<nu> $ i = snd \<omega> $ i) \<Longrightarrow> (\<forall>i. Inl i \<in> (\<Union>i\<in>SIGT t1. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<longrightarrow> fst \<nu> $ i = fst \<omega> $ i) \<and> (\<forall>i. Inr i \<in> (\<Union>i\<in>SIGT t1. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<longrightarrow> snd \<nu> $ i = snd \<omega> $ i)
[PROOF STEP]
by auto


[STATEMENT]
lemma SIGT_plus2:"Vagree \<nu> \<omega> (\<Union>i\<in>SIGT (Plus t1 t2). case SFunctions \<sigma> i of Some x \<Rightarrow> FVT x | None \<Rightarrow> {})
  \<Longrightarrow> Vagree \<nu> \<omega> (\<Union>i\<in>SIGT t2. case SFunctions \<sigma> i of Some x \<Rightarrow> FVT x | None \<Rightarrow> {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Vagree \<nu> \<omega> (\<Union>i\<in>SIGT (Plus t1 t2). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<Longrightarrow> Vagree \<nu> \<omega> (\<Union>i\<in>SIGT t2. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)
[PROOF STEP]
unfolding Vagree_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>i. Inl i \<in> (\<Union>i\<in>SIGT (Plus t1 t2). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<longrightarrow> fst \<nu> $ i = fst \<omega> $ i) \<and> (\<forall>i. Inr i \<in> (\<Union>i\<in>SIGT (Plus t1 t2). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<longrightarrow> snd \<nu> $ i = snd \<omega> $ i) \<Longrightarrow> (\<forall>i. Inl i \<in> (\<Union>i\<in>SIGT t2. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<longrightarrow> fst \<nu> $ i = fst \<omega> $ i) \<and> (\<forall>i. Inr i \<in> (\<Union>i\<in>SIGT t2. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<longrightarrow> snd \<nu> $ i = snd \<omega> $ i)
[PROOF STEP]
by auto


[STATEMENT]
lemma SIGT_times1:"Vagree \<nu> \<omega> (\<Union>i\<in>SIGT (Times t1 t2). case SFunctions \<sigma> i of Some x \<Rightarrow> FVT x | None \<Rightarrow> {})
  \<Longrightarrow> Vagree \<nu> \<omega> (\<Union>i\<in>SIGT t1. case SFunctions \<sigma> i of Some x \<Rightarrow> FVT x | None \<Rightarrow> {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Vagree \<nu> \<omega> (\<Union>i\<in>SIGT (Times t1 t2). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<Longrightarrow> Vagree \<nu> \<omega> (\<Union>i\<in>SIGT t1. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)
[PROOF STEP]
unfolding Vagree_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>i. Inl i \<in> (\<Union>i\<in>SIGT (Times t1 t2). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<longrightarrow> fst \<nu> $ i = fst \<omega> $ i) \<and> (\<forall>i. Inr i \<in> (\<Union>i\<in>SIGT (Times t1 t2). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<longrightarrow> snd \<nu> $ i = snd \<omega> $ i) \<Longrightarrow> (\<forall>i. Inl i \<in> (\<Union>i\<in>SIGT t1. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<longrightarrow> fst \<nu> $ i = fst \<omega> $ i) \<and> (\<forall>i. Inr i \<in> (\<Union>i\<in>SIGT t1. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<longrightarrow> snd \<nu> $ i = snd \<omega> $ i)
[PROOF STEP]
by auto


[STATEMENT]
lemma SIGT_times2:"Vagree \<nu> \<omega> (\<Union>i\<in>SIGT (Times t1 t2). case SFunctions \<sigma> i of Some x \<Rightarrow> FVT x | None \<Rightarrow> {})
  \<Longrightarrow> Vagree \<nu> \<omega> (\<Union>i\<in>SIGT t2. case SFunctions \<sigma> i of Some x \<Rightarrow> FVT x | None \<Rightarrow> {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Vagree \<nu> \<omega> (\<Union>i\<in>SIGT (Times t1 t2). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<Longrightarrow> Vagree \<nu> \<omega> (\<Union>i\<in>SIGT t2. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)
[PROOF STEP]
unfolding Vagree_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>i. Inl i \<in> (\<Union>i\<in>SIGT (Times t1 t2). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<longrightarrow> fst \<nu> $ i = fst \<omega> $ i) \<and> (\<forall>i. Inr i \<in> (\<Union>i\<in>SIGT (Times t1 t2). case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<longrightarrow> snd \<nu> $ i = snd \<omega> $ i) \<Longrightarrow> (\<forall>i. Inl i \<in> (\<Union>i\<in>SIGT t2. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<longrightarrow> fst \<nu> $ i = fst \<omega> $ i) \<and> (\<forall>i. Inr i \<in> (\<Union>i\<in>SIGT t2. case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x) \<longrightarrow> snd \<nu> $ i = snd \<omega> $ i)
[PROOF STEP]
by auto