# Theory USubst

theory USubst
imports Coincidence
```theory "USubst"
imports
Complex_Main
"Syntax"
"Static_Semantics"
"Coincidence"
"Denotational_Semantics"
begin
section ‹Uniform Substitution›

text ‹uniform substitution representation as tuple of partial maps from identifiers to type-compatible replacements.›
type_synonym usubst =
"(ident ⇀ trm) × (ident ⇀ trm) × (ident ⇀ fml) × (ident ⇀ game)"

abbreviation SConst:: "usubst ⇒ (ident ⇀ trm)"
where "SConst ≡ (λ(F0, _, _, _). F0)"
abbreviation SFuncs:: "usubst ⇒ (ident ⇀ trm)"
where "SFuncs ≡ (λ(_, F, _, _). F)"
abbreviation SPreds:: "usubst ⇒ (ident ⇀ fml)"
where "SPreds ≡ (λ(_, _, P, _). P)"
abbreviation SGames:: "usubst ⇒ (ident ⇀ game)"
where "SGames ≡ (λ(_, _, _, G). G)"

text ‹crude approximation of size which is enough for termination arguments›
definition usubstsize:: "usubst ⇒ nat"
where "usubstsize σ = (if (dom (SFuncs σ) = {} ∧ dom (SPreds σ) = {}) then 1 else 2)"

text ‹dot is some fixed constant function symbol that is reserved for the purposes of the substitution›
definition dot:: "trm"
where "dot = Const (dotid)"

subsection ‹Strict Mechanism for Handling Substitution Partiality in Isabelle›

text ‹Optional terms that result from a substitution, either actually a term or just none to indicate that the substitution clashed›
type_synonym trmo = "trm option"

abbreviation undeft:: trmo where "undeft ≡ None"
abbreviation Aterm:: "trm ⇒ trmo" where "Aterm ≡ Some"

lemma undeft_None: "undeft=None" by simp
lemma Aterm_Some: "Aterm θ=Some θ" by simp

lemma undeft_equiv: "(θ≠undeft) = (∃t. θ=Aterm t)"
by simp

text ‹Plus on defined terms, strict undeft otherwise ›
fun Pluso :: "trmo ⇒ trmo ⇒ trmo"
where
"Pluso (Aterm θ) (Aterm η) = Aterm(Plus θ η)"
| "Pluso undeft η = undeft"
| "Pluso θ undeft = undeft"

text ‹Times on defined terms, strict undeft otherwise ›
fun Timeso :: "trmo ⇒ trmo ⇒ trmo"
where
"Timeso (Aterm θ) (Aterm η) = Aterm(Times θ η)"
| "Timeso undeft η = undeft"
| "Timeso θ undeft = undeft"

fun Differentialo :: "trmo ⇒ trmo"
where
"Differentialo (Aterm θ) = Aterm(Differential θ)"
| "Differentialo undeft = undeft"

lemma Pluso_undef: "(Pluso θ η = undeft) = (θ=undeft ∨ η=undeft)"    by (metis Pluso.elims option.distinct(1))
lemma Timeso_undef: "(Timeso θ η = undeft) = (θ=undeft ∨ η=undeft)"  by (metis Timeso.elims option.distinct(1))
lemma Differentialo_undef: "(Differentialo θ = undeft) = (θ=undeft)" by (metis Differentialo.elims option.distinct(1))

type_synonym fmlo = "fml option"

abbreviation undeff:: fmlo where "undeff ≡ None"
abbreviation Afml:: "fml ⇒ fmlo" where "Afml ≡ Some"

type_synonym gameo = "game option"

abbreviation undefg:: gameo where "undefg ≡ None"
abbreviation Agame:: "game ⇒ gameo" where "Agame ≡ Some"

lemma undeff_equiv: "(φ≠undeff) = (∃f. φ=Afml f)"
by simp

lemma undefg_equiv: "(α≠undefg) = (∃g. α=Agame g)"
by simp

text ‹Geq on defined terms, strict undeft otherwise ›
fun Geqo :: "trmo ⇒ trmo ⇒ fmlo"
where
"Geqo (Aterm θ) (Aterm η) = Afml(Geq θ η)"
| "Geqo undeft η = undeff"
| "Geqo θ undeft = undeff"

text ‹Not on defined formulas, strict undeft otherwise ›
fun Noto :: "fmlo ⇒ fmlo"
where
"Noto (Afml φ) = Afml(Not φ)"
| "Noto undeff = undeff"

text ‹And on defined formulas, strict undeft otherwise ›
fun Ando :: "fmlo ⇒ fmlo ⇒ fmlo"
where
"Ando (Afml φ) (Afml ψ) = Afml(And φ ψ)"
| "Ando undeff ψ = undeff"
| "Ando φ undeff = undeff"

text ‹Exists on defined formulas, strict undeft otherwise ›
fun Existso :: "variable ⇒ fmlo ⇒ fmlo"
where
"Existso x (Afml φ) = Afml(Exists x φ)"
| "Existso x undeff = undeff"

text ‹Diamond on defined games/formulas, strict undeft otherwise ›
fun Diamondo :: "gameo ⇒ fmlo ⇒ fmlo"
where
"Diamondo (Agame α) (Afml φ) = Afml(Diamond α φ)"
| "Diamondo undefg φ = undeff"
| "Diamondo α undeff = undeff"

lemma Geqo_undef: "(Geqo θ η = undeff) = (θ=undeft ∨ η=undeft)"
by (metis Geqo.elims option.distinct(1))
lemma Noto_undef: "(Noto φ = undeff) = (φ=undeff)"
by (metis Noto.elims option.distinct(1))
lemma Ando_undef: "(Ando φ ψ = undeff) = (φ=undeff ∨ ψ=undeff)"
by (metis Ando.elims option.distinct(1))
lemma Existso_undef: "(Existso x φ = undeff) = (φ=undeff)"
by (metis Existso.elims option.distinct(1))
lemma Diamondo_undef: "(Diamondo α φ = undeff) = (α=undefg ∨ φ=undeff)"
by (metis Diamondo.elims option.distinct(1))

text ‹Assign on defined terms, strict undefg otherwise ›
fun Assigno :: "variable ⇒ trmo ⇒ gameo"
where
"Assigno x (Aterm θ) = Agame(Assign x θ)"
| "Assigno x undeft = undefg"

fun ODEo :: "ident ⇒ trmo ⇒ gameo"
where
"ODEo x (Aterm θ) = Agame(ODE x θ)"
| "ODEo x undeft = undefg"

text ‹Test on defined formulas, strict undefg otherwise ›
fun Testo :: "fmlo ⇒ gameo"
where
"Testo (Afml φ) = Agame(Test φ)"
| "Testo undeff = undefg"

text ‹Choice on defined games, strict undefg otherwise ›
fun Choiceo :: "gameo ⇒ gameo ⇒ gameo"
where
"Choiceo (Agame α) (Agame β) = Agame(Choice α β)"
| "Choiceo α undefg = undefg"
| "Choiceo undefg β = undefg"

text ‹Compose on defined games, strict undefg otherwise ›
fun Composeo :: "gameo ⇒ gameo ⇒ gameo"
where
"Composeo (Agame α) (Agame β) = Agame(Compose α β)"
| "Composeo α undefg = undefg"
| "Composeo undefg β = undefg"

text ‹Loop on defined games, strict undefg otherwise ›
fun Loopo :: "gameo ⇒ gameo"
where
"Loopo (Agame α) = Agame(Loop α)"
| "Loopo undefg = undefg"

text ‹Dual on defined games, strict undefg otherwise ›
fun Dualo :: "gameo ⇒ gameo"
where
"Dualo (Agame α) = Agame(Dual α)"
| "Dualo undefg = undefg"

lemma Assigno_undef: "(Assigno x θ = undefg) = (θ=undeft)"  by (metis Assigno.elims option.distinct(1))
lemma ODEo_undef: "(ODEo x θ = undefg) = (θ=undeft)"        by (metis ODEo.elims option.distinct(1))
lemma Testo_undef: "(Testo φ = undefg) = (φ=undeff)"        by (metis Testo.elims option.distinct(1))
lemma Choiceo_undef: "(Choiceo α β = undefg) = (α=undefg ∨ β=undefg)"   by (metis Choiceo.elims option.distinct(1))
lemma Composeo_undef: "(Composeo α β = undefg) = (α=undefg ∨ β=undefg)" by (metis Composeo.elims option.distinct(1))
lemma Loopo_undef: "(Loopo α = undefg) = (α=undefg)"        by (metis Loopo.elims option.distinct(1))
lemma Dualo_undef: "(Dualo α = undefg) = (α=undefg)"        by (metis Dualo.elims option.distinct(1))

subsection ‹Recursive Application of One-Pass Uniform Substitution›

text ‹‹dotsubstt θ› is the dot substitution ‹{. ~> θ}› substituting a term for the . function symbol›
definition dotsubstt:: "trm ⇒ usubst"
where "dotsubstt θ = (
(λf. (if f=dotid then (Some(θ)) else None)),
(λ_. None),
(λ_. None),
(λ_. None)
)"

definition usappconst:: "usubst ⇒ variable set ⇒ ident ⇒ (trmo)"
where "usappconst σ U f ≡ (case SConst σ f of Some r ⇒ if FVT(r)∩U={} then Aterm(r) else undeft | None ⇒ Aterm(Const f))"

function usubstappt:: "usubst ⇒ variable set ⇒ (trm ⇒ trmo)"
where
"usubstappt σ U (Var x)     = Aterm (Var x)"
| "usubstappt σ U (Number r)  = Aterm (Number r)"
| "usubstappt σ U (Const f)   = usappconst σ U f"
| "usubstappt σ U (Func f θ)  =
(case usubstappt σ U θ of undeft   ⇒ undeft
| Aterm σθ ⇒ (case SFuncs σ f of Some r ⇒ if FVT(r)∩U={} then usubstappt(dotsubstt σθ) {} r else undeft | None ⇒ Aterm(Func f σθ)))"
| "usubstappt σ U (Plus θ η)  = Pluso (usubstappt σ U θ) (usubstappt σ U η)"
| "usubstappt σ U (Times θ η) = Timeso (usubstappt σ U θ) (usubstappt σ U η)"
| "usubstappt σ U (Differential θ) = Differentialo (usubstappt σ allvars θ)"
by pat_completeness auto
termination
by (relation "measures [λ(σ,U,θ). usubstsize σ , λ(σ,U,θ). size θ]")

(* Expand let constructs automatically *)
declare Let_def [simp]

function usubstappf:: "usubst ⇒ variable set ⇒ (fml ⇒ fmlo)"
and usubstappp:: "usubst ⇒ variable set ⇒ (game ⇒ variable set × gameo)"
where
"usubstappf σ U (Pred p θ)   =
(case usubstappt σ U θ of undeft   ⇒ undeff
| Aterm σθ ⇒ (case SPreds σ p of Some r ⇒ if FVF(r)∩U={} then usubstappf(dotsubstt σθ) {} r else undeff | None ⇒ Afml(Pred p σθ)))"
| "usubstappf σ U (Geq θ η)    = Geqo (usubstappt σ U θ) (usubstappt σ U η)"
| "usubstappf σ U (Not φ)      = Noto (usubstappf σ U φ)"
| "usubstappf σ U (And φ ψ)    = Ando (usubstappf σ U φ) (usubstappf σ U ψ)"
| "usubstappf σ U (Exists x φ) = Existso x (usubstappf σ (U∪{x}) φ)"
| "usubstappf σ U (Diamond α φ) = (let Vα = usubstappp σ U α in Diamondo (snd Vα) (usubstappf σ (fst Vα) φ))"

| "usubstappp σ U (Game a)   =
(case SGames σ a of Some r ⇒ (U∪BVG(r),Agame r)
| None   ⇒ (allvars,Agame(Game a)))"
| "usubstappp σ U (Assign x θ) = (U∪{x}, Assigno x (usubstappt σ U θ))"
| "usubstappp σ U (Test φ) = (U, Testo (usubstappf σ U φ))"
| "usubstappp σ U (Choice α β) =
(let Vα = usubstappp σ U α in
let Wβ = usubstappp σ U β in
(fst Vα∪fst Wβ, Choiceo (snd Vα) (snd Wβ)))"
| "usubstappp σ U (Compose α β) =
(let Vα = usubstappp σ U α in
let Wβ = usubstappp σ (fst Vα) β in
(fst Wβ, Composeo (snd Vα) (snd Wβ)))"
| "usubstappp σ U (Loop α) =
(let V = fst(usubstappp σ U α) in
(V, Loopo (snd(usubstappp σ V α))))"
| "usubstappp σ U (Dual α) =
(let Vα = usubstappp σ U α in (fst Vα, Dualo (snd Vα)))"
| "usubstappp σ U (ODE x θ) = (U∪{RVar x,DVar x}, ODEo x (usubstappt σ (U∪{RVar x,DVar x}) θ))"
by pat_completeness auto
termination
by (relation "measures [(λk. usubstsize (case k of Inl(σ,U,φ) ⇒ σ | Inr(σ,U,α) ⇒ σ)) , (λk. case k of Inl (σ,U,φ) ⇒ size φ | Inr (σ,U,α) ⇒ size α)]")

text ‹Induction Principles for Uniform Substitutions›
lemmas usubstappt_induct = usubstappt.induct [case_names Var Number Const FuncMatch Plus Times Differential]
lemmas usubstappfp_induct = usubstappf_usubstappp.induct [case_names Pred Geq Not And Exists Diamond  Game Assign Test Choice Compose Loop Dual ODE]

paragraph ‹Simple Observations for Automation›

text ‹More automation for Case›

lemma usappconst_simp [simp]: "SConst σ f = Some r ⟹ FVT(r)∩U={} ⟹ usappconst σ U f = Aterm(r)"
and "SConst σ f = None ⟹ usappconst σ U f = Aterm(Const f)"
and "SConst σ f = Some r ⟹ FVT(r)∩U≠{} ⟹ usappconst σ U f = undeft"
unfolding usappconst_def by auto

lemma usappconst_conv: "usappconst σ U f≠undeft ⟹
SConst σ f = None ∨ (∃r. SConst σ f = Some r ∧ FVT(r)∩U={})"
(*by (smt option.case_eq_if option.collapse usappconst_def)*)
proof-
assume as: "usappconst σ U f≠undeft"
show "SConst σ f = None ∨ (∃r. SConst σ f = Some r ∧ FVT(r)∩U={})"
proof (cases "SConst σ f")
case None
then show ?thesis
by auto
next
case (Some a)
then show ?thesis using as usappconst_def[where σ=σ and U=U and f=f] option.distinct(1) by fastforce
qed
qed

lemma usubstappt_const [simp]: "SConst σ f = Some r ⟹ FVT(r)∩U={} ⟹ usubstappt σ U (Const f) = Aterm(r)"
and "SConst σ f = None ⟹ usubstappt σ U (Const f) = Aterm(Const f)"
and "SConst σ f = Some r ⟹ FVT(r)∩U≠{} ⟹ usubstappt σ U (Const f) = undeft"

lemma usubstappt_const_conv: "usubstappt σ U (Const f)≠undeft ⟹
SConst σ f = None ∨ (∃r. SConst σ f = Some r ∧ FVT(r)∩U={})"
using usappconst_conv by auto

lemma usubstappt_func [simp]: "SFuncs σ f = Some r ⟹ FVT(r)∩U={} ⟹ usubstappt σ U θ = Aterm σθ ⟹
usubstappt σ U (Func f θ) = usubstappt (dotsubstt σθ) {} r"
and "SFuncs σ f=None ⟹  usubstappt σ U θ = Aterm σθ ⟹ usubstappt σ U (Func f θ) = Aterm(Func f σθ)"
and "usubstappt σ U θ = undeft ⟹ usubstappt σ U (Func f θ) = undeft"
by auto

lemma usubstappt_func2 [simp]: "SFuncs σ f = Some r ⟹ FVT(r)∩U≠{} ⟹ usubstappt σ U (Func f θ) = undeft"
by (cases "usubstappt σ U θ") (auto)

lemma usubstappt_func_conv: "usubstappt σ U (Func f θ) ≠ undeft ⟹
usubstappt σ U θ ≠ undeft ∧
(SFuncs σ f = None ∨ (∃r. SFuncs σ f = Some r ∧ FVT(r)∩U={}))"
by (metis (lifting) option.simps(4) undeft_equiv usubstappt.simps(4) usubstappt_func2)
(*by (cases "usubstappt σ U θ") (auto) *)

lemma usubstappt_plus_conv: "usubstappt σ U (Plus θ η) ≠ undeft ⟹
usubstappt σ U θ ≠ undeft ∧ usubstappt σ U η ≠ undeft"

lemma usubstappt_times_conv: "usubstappt σ U (Times θ η) ≠ undeft ⟹
usubstappt σ U θ ≠ undeft ∧ usubstappt σ U η ≠ undeft"

lemma usubstappt_differential_conv: "usubstappt σ U (Differential θ) ≠ undeft ⟹
usubstappt σ allvars θ ≠ undeft"

lemma usubstappf_pred [simp]: "SPreds σ p = Some r ⟹ FVF(r)∩U={} ⟹ usubstappt σ U θ = Aterm σθ ⟹
usubstappf σ U (Pred p θ) = usubstappf (dotsubstt σθ) {} r"
and "SPreds σ p = None ⟹ usubstappt σ U θ = Aterm σθ ⟹ usubstappf σ U (Pred p θ) = Afml(Pred p σθ)"
and "usubstappt σ U θ = undeft ⟹ usubstappf σ U (Pred p θ) = undeff"
by auto

lemma usubstappf_pred2 [simp]: "SPreds σ p = Some r ⟹ FVF(r)∩U≠{} ⟹ usubstappf σ U (Pred p θ) = undeff"
by (cases "usubstappt σ U θ") (auto)

lemma usubstappf_pred_conv: "usubstappf σ U (Pred p θ) ≠ undeff ⟹
usubstappt σ U θ ≠ undeft ∧
(SPreds σ p = None ∨ (∃r. SPreds σ p = Some r ∧ FVF(r)∩U={}))"
by (metis (lifting) option.simps(4) undeff_equiv usubstappf.simps(1) usubstappf_pred2)

lemma usubstappf_geq: "usubstappt σ U θ ≠ undeft ⟹ usubstappt σ U η ≠ undeft ⟹
usubstappf σ U (Geq θ η) = Afml(Geq (the (usubstappt σ U θ)) (the (usubstappt σ U η)))"
by fastforce

lemma usubstappf_geq_conv: "usubstappf σ U (Geq θ η) ≠ undeff ⟹
usubstappt σ U θ ≠ undeft ∧ usubstappt σ U η ≠ undeft"

lemma usubstappf_geqr: "usubstappf σ U (Geq θ η) ≠ undeff ⟹
usubstappf σ U (Geq θ η) = Afml(Geq (the (usubstappt σ U θ)) (the (usubstappt σ U η)))"
using usubstappf_geq usubstappf_geq_conv by blast

lemma usubstappf_exists: "usubstappf σ U (Exists x φ) ≠ undeff ⟹
usubstappf σ U (Exists x φ) = Afml(Exists x (the (usubstappf σ (U∪{x}) φ)))"
using Existso_undef by auto

lemma usubstappp_game [simp]: "SGames σ a = Some r ⟹ usubstappp σ U (Game a) = (U∪BVG(r),Agame(r))"
and "SGames σ a = None ⟹ usubstappp σ U (Game a) = (allvars,Agame(Game a))"
by auto

lemma usubstappp_choice [simp]: "usubstappp σ U (Choice α β) =
(fst(usubstappp σ U α)∪fst(usubstappp σ U β), Choiceo (snd(usubstappp σ U α)) (snd(usubstappp σ U β)))"
by auto

lemma usubstappp_choice_conv : "snd(usubstappp σ U (Choice α β)) ≠ undefg ⟹
snd(usubstappp σ U α) ≠ undefg ∧ snd(usubstappp σ U β) ≠ undefg"

lemma usubstappp_compose [simp]: "usubstappp σ U (Compose α β) =
(fst(usubstappp σ (fst(usubstappp σ U α)) β), Composeo (snd(usubstappp σ U α)) (snd(usubstappp σ (fst(usubstappp σ U α)) β)))"
by simp

lemma usubstappp_loop: "usubstappp σ U (Loop α) =
(fst(usubstappp σ U α), Loopo (snd(usubstappp σ (fst(usubstappp σ U α)) α)))"
by auto

lemma usubstappp_dual [simp]: "usubstappp σ U (Dual α) =
(fst(usubstappp σ U α), Dualo (snd (usubstappp σ U α)))"
by simp

section ‹Soundness of Uniform Substitution›

subsection ‹USubst Application is a Function of Deterministic Result›

lemma usubstappt_det: "usubstappt σ U θ ≠ undeft ⟹ usubstappt σ V θ ≠ undeft ⟹
usubstappt σ U θ = usubstappt σ V θ"
proof (induction θ)
case (Var x)
then show ?case by simp
next
case (Number x)
then show ?case by simp
next
case (Const f)
then show ?case
(*by (smt option.case_eq_if usappconst_def usubstappt.simps(3))*)
proof - (*sledgehammer*)
have f1: "usubstappt σ U (Const f) = (case SConst σ f of None ⇒ Aterm (Const f) | Some t ⇒ if FVT t ∩ U = {} then Aterm t else undeft)"
have f2: "∀z f za. if za = undeft then (case za of None ⇒ z::trm option | Some x ⇒ f x) = z else (case za of None ⇒ z | Some x ⇒ f x) = f (the za)"
by force
then have "SConst σ f ≠ undeft ⟶ (if FVT (the (SConst σ f)) ∩ U = {} then Aterm (the (SConst σ f)) else undeft) = usappconst σ U f"
then have f3: "SConst σ f ≠ undeft ⟶ FVT (the (SConst σ f)) ∩ U = {}"
by (metis Const.prems(1) usubstappt.simps(3))
have "SConst σ f ≠ undeft ⟶ (if FVT (the (SConst σ f)) ∩ V = {} then Aterm (the (SConst σ f)) else undeft) = usappconst σ V f"
using f2 usappconst_def by presburger
then have "SConst σ f ≠ undeft ⟶ FVT (the (SConst σ f)) ∩ V = {}"
by (metis (no_types) Const.prems(2) usubstappt.simps(3))
then have f4: "SConst σ f ≠ undeft ⟶ usubstappt σ U (Const f) = usappconst σ V f"
using f3 f2 f1 usappconst_def by presburger
{ assume "usubstappt σ U (Const f) ≠ usubstappt σ V (Const f)"
then have "usubstappt σ U (Const f) ≠ (case SConst σ f of None ⇒ Aterm (Const f) | Some t ⇒ if FVT t ∩ V = {} then Aterm t else undeft)"
then have "SConst σ f ≠ undeft"
using f2 f1 by (metis (no_types))
then have ?thesis
using f4 by simp }
then show ?thesis
by blast
qed
next
case (Func f θ)
then show ?case using usubstappt_func
(*by (cases "SFuncs σ f") (auto simp add: usubstappt_func)*)
(*by (smt option.case_eq_if usubstappt.simps(4))*)
proof - (*sledgehammer*)
have f1: "(case usubstappt σ U θ of None ⇒ undeft | Some t ⇒ (case SFuncs σ f of None ⇒ Aterm (trm.Func f t) | Some ta ⇒ if FVT ta ∩ U = {} then usubstappt (dotsubstt t) {} ta else undeft)) ≠ undeft"
using Func(2) by auto
have f2: "∀z f za. if za = undeft then (case za of None ⇒ z::trm option | Some x ⇒ f x) = z else (case za of None ⇒ z | Some x ⇒ f x) = f (the za)"
by force
then have f3: "usubstappt σ U θ ≠ undeft"
using f1 by meson
have "(case usubstappt σ V θ of None ⇒ undeft | Some t ⇒ (case SFuncs σ f of None ⇒ Aterm (trm.Func f t) | Some ta ⇒ if FVT ta ∩ V = {} then usubstappt (dotsubstt t) {} ta else undeft)) ≠ undeft"
using Func(3) by auto
then have f4: "usubstappt σ V θ ≠ undeft"
using f2 by meson
then have f5: "usubstappt σ U (trm.Func f θ) = (case SFuncs σ f of None ⇒ Aterm (trm.Func f (the (usubstappt σ V θ))) | Some t ⇒ if FVT t ∩ U = {} then usubstappt (dotsubstt (the (usubstappt σ V θ))) {} t else undeft)"
using f3 f2 Func(1) usubstappt.simps(4) by presburger
have "SFuncs σ f ≠ undeft ⟶ (if FVT (the (SFuncs σ f)) ∩ U = {} then usubstappt (dotsubstt (the (usubstappt σ V θ))) {} (the (SFuncs σ f)) else undeft) = usubstappt σ U (trm.Func f θ)"
using f4 f3 f2 Func(1) usubstappt.simps(4) by presburger
then have f6: "SFuncs σ f ≠ undeft ⟶ FVT (the (SFuncs σ f)) ∩ U = {}"
by (metis Func(2))
have f7: "(case usubstappt σ V θ of None ⇒ undeft | Some t ⇒ (case SFuncs σ f of None ⇒ Aterm (trm.Func f t) | Some ta ⇒ if FVT ta ∩ V = {} then usubstappt (dotsubstt t) {} ta else undeft)) = (case SFuncs σ f of None ⇒ Aterm (trm.Func f (the (usubstappt σ V θ))) | Some t ⇒ if FVT t ∩ V = {} then usubstappt (dotsubstt (the (usubstappt σ V θ))) {} t else undeft)"
using f4 f2 by presburger
then have "SFuncs σ f ≠ undeft ⟶ (if FVT (the (SFuncs σ f)) ∩ V = {} then usubstappt (dotsubstt (the (usubstappt σ V θ))) {} (the (SFuncs σ f)) else undeft) = usubstappt σ V (trm.Func f θ)"
using f2 by simp
then have f8: "SFuncs σ f ≠ undeft ⟶ FVT (the (SFuncs σ f)) ∩ V = {}"
by (metis (full_types) Func(3))
{ assume "usubstappt σ U (trm.Func f θ) ≠ usubstappt σ V (trm.Func f θ)"
moreover
{ assume "(case SFuncs σ f of None ⇒ Aterm (trm.Func f (the (usubstappt σ V θ))) | Some t ⇒ if FVT t ∩ V = {} then usubstappt (dotsubstt (the (usubstappt σ V θ))) {} t else undeft) ≠ Aterm (trm.Func f (the (usubstappt σ V θ)))"
then have "SFuncs σ f ≠ undeft"
using f2 by meson }
ultimately have "SFuncs σ f ≠ undeft"
using f7 f5 by fastforce
then have ?thesis
using f8 f7 f6 f5 f2 by simp }
then show ?thesis
by blast
qed
next
case (Plus θ1 θ2)
then show ?case using Pluso_undef by auto
next
case (Times θ1 θ2)
then show ?case using Timeso_undef by auto
next
case (Differential θ)
then show ?case using Differentialo_undef by auto
qed

lemma usubstappf_and_usubstappp_det:
shows "usubstappf σ U φ ≠ undeff ⟹ usubstappf σ V φ ≠ undeff ⟹ usubstappf σ U φ = usubstappf σ V φ"
and "snd(usubstappp σ U α) ≠ undefg ⟹ snd(usubstappp σ V α) ≠ undefg ⟹ snd(usubstappp σ U α) = snd(usubstappp σ V α)"
proof (induction φ and α arbitrary: U V and U V)
case (Pred p θ)
then show ?case using usubstappt_det usubstappf_pred
(*by (metis usubstappf.simps(1)) *)
(*by (smt option.case_eq_if usubstappf.simps(1)) *)
proof - (*sledgehammer*)
have f1: "(case usubstappt σ U θ of None ⇒ undeff | Some t ⇒ (case SPreds σ p of None ⇒ Afml (Pred p t) | Some f ⇒ if FVF f ∩ U = {} then usubstappf (dotsubstt t) {} f else undeff)) ≠ undeff"
using Pred.prems(1) by auto
have f2: "∀z f za. if za = undeft then (case za of None ⇒ z::fml option | Some x ⇒ f x) = z else (case za of None ⇒ z | Some x ⇒ f x) = f (the za)"
then have f3: "(case usubstappt σ U θ of None ⇒ undeff | Some t ⇒ (case SPreds σ p of None ⇒ Afml (Pred p t) | Some f ⇒ if FVF f ∩ U = {} then usubstappf (dotsubstt t) {} f else undeff)) = (case SPreds σ p of None ⇒ Afml (Pred p (the (usubstappt σ U θ))) | Some f ⇒ if FVF f ∩ U = {} then usubstappf (dotsubstt (the (usubstappt σ U θ))) {} f else undeff)"
using f1 by meson
have f4: "(case usubstappt σ V θ of None ⇒ undeff | Some t ⇒ (case SPreds σ p of None ⇒ Afml (Pred p t) | Some f ⇒ if FVF f ∩ V = {} then usubstappf (dotsubstt t) {} f else undeff)) ≠ undeff"
using Pred.prems(2) by auto
then have f5: "usubstappt σ U θ = usubstappt σ V θ"
using f2 f1 by (meson usubstappt_det)
then have f6: "usubstappf σ U (Pred p θ) = (case SPreds σ p of None ⇒ Afml (Pred p (the (usubstappt σ V θ))) | Some f ⇒ if FVF f ∩ U = {} then usubstappf (dotsubstt (the (usubstappt σ V θ))) {} f else undeff)"
using f3 usubstappf.simps(1) by presburger
have f7: "∀z f za. if za = undeff then (case za of None ⇒ z::fml option | Some x ⇒ f x) = z else (case za of None ⇒ z | Some x ⇒ f x) = f (the za)"
have f8: "(case usubstappt σ V θ of None ⇒ undeff | Some t ⇒ (case SPreds σ p of None ⇒ Afml (Pred p t) | Some f ⇒ if FVF f ∩ V = {} then usubstappf (dotsubstt t) {} f else undeff)) = (case SPreds σ p of None ⇒ Afml (Pred p (the (usubstappt σ V θ))) | Some f ⇒ if FVF f ∩ V = {} then usubstappf (dotsubstt (the (usubstappt σ V θ))) {} f else undeff)"
using f4 f2 by meson
then have f9: "SPreds σ p = undeff ⟶ usubstappf σ U (Pred p θ) = usubstappf σ V (Pred p θ)"
using f6 by fastforce
{ assume "usubstappf σ U (Pred p θ) ≠ usubstappf σ V (Pred p θ)"
then have "usubstappf σ U (Pred p θ) ≠ (case SPreds σ p of None ⇒ Afml (Pred p (the (usubstappt σ V θ))) | Some f ⇒ if FVF f ∩ V = {} then usubstappf (dotsubstt (the (usubstappt σ V θ))) {} f else undeff)"
using f8 by simp
moreover
{ assume "usubstappf σ U (Pred p θ) ≠ (if FVF (the (SPreds σ p)) ∩ V = {} then usubstappf (dotsubstt (the (usubstappt σ V θ))) {} (the (SPreds σ p)) else undeff)"
moreover
{ assume "usubstappf σ U (Pred p θ) ≠ usubstappf (dotsubstt (the (usubstappt σ V θ))) {} (the (SPreds σ p))"
moreover
{ assume "usubstappf σ U (Pred p θ) ≠ (if FVF (the (SPreds σ p)) ∩ U = {} then usubstappf (dotsubstt (the (usubstappt σ V θ))) {} (the (SPreds σ p)) else undeff)"
then have "(case SPreds σ p of None ⇒ Afml (Pred p (the (usubstappt σ V θ))) | Some f ⇒ if FVF f ∩ U = {} then usubstappf (dotsubstt (the (usubstappt σ V θ))) {} f else undeff) ≠ (if FVF (the (SPreds σ p)) ∩ U = {} then usubstappf (dotsubstt (the (usubstappt σ V θ))) {} (the (SPreds σ p)) else undeff)"
using f6 by force
then have "SPreds σ p = undeff"
using f7 by (metis (no_types, lifting) Pred.prems(1) calculation f5 option.collapse usubstappf_pred usubstappf_pred2 usubstappf_pred_conv) }
moreover
{ assume "(if FVF (the (SPreds σ p)) ∩ U = {} then usubstappf (dotsubstt (the (usubstappt σ V θ))) {} (the (SPreds σ p)) else undeff) ≠ usubstappf (dotsubstt (the (usubstappt σ V θ))) {} (the (SPreds σ p))"
then have "(if FVF (the (SPreds σ p)) ∩ U = {} then usubstappf (dotsubstt (the (usubstappt σ V θ))) {} (the (SPreds σ p)) else undeff) ≠ (case SPreds σ p of None ⇒ Afml (Pred p (the (usubstappt σ U θ))) | Some f ⇒ if FVF f ∩ U = {} then usubstappf (dotsubstt (the (usubstappt σ U θ))) {} f else undeff)"
using f3 Pred.prems(1) by auto
then have "(if FVF (the (SPreds σ p)) ∩ U = {} then usubstappf (dotsubstt (the (usubstappt σ V θ))) {} (the (SPreds σ p)) else undeff) ≠ (case SPreds σ p of None ⇒ Afml (Pred p (the (usubstappt σ V θ))) | Some f ⇒ if FVF f ∩ U = {} then usubstappf (dotsubstt (the (usubstappt σ V θ))) {} f else undeff)"
using f5 using Pred.prems(1) ‹(if FVF (the (SPreds σ p)) ∩ U = {} then usubstappf (dotsubstt (the (usubstappt σ V θ))) {} (the (SPreds σ p)) else undeff) ≠ usubstappf (dotsubstt (the (usubstappt σ V θ))) {} (the (SPreds σ p))› f6 by auto
then have "(case SPreds σ p of None ⇒ Afml (Pred p (the (usubstappt σ V θ))) | Some f ⇒ if FVF f ∩ U = {} then usubstappf (dotsubstt (the (usubstappt σ V θ))) {} f else undeff) ≠ (if FVF (the (SPreds σ p)) ∩ U = {} then usubstappf (dotsubstt (the (usubstappt σ V θ))) {} (the (SPreds σ p)) else undeff)"
by simp
then have "SPreds σ p = undeff"
using f7 proof -
show ?thesis
using ‹(case SPreds σ p of None ⇒ Afml (Pred p (the (usubstappt σ V θ))) | Some f ⇒ if FVF f ∩ U = {} then usubstappf (dotsubstt (the (usubstappt σ V θ))) {} f else undeff) ≠ (if FVF (the (SPreds σ p)) ∩ U = {} then usubstappf (dotsubstt (the (usubstappt σ V θ))) {} (the (SPreds σ p)) else undeff)› calculation(2) f6 by presburger
qed}
ultimately have "SPreds σ p = undeff"
by fastforce }
moreover
{ assume "(if FVF (the (SPreds σ p)) ∩ V = {} then usubstappf (dotsubstt (the (usubstappt σ V θ))) {} (the (SPreds σ p)) else undeff) ≠ usubstappf (dotsubstt (the (usubstappt σ V θ))) {} (the (SPreds σ p))"
then have "(case SPreds σ p of None ⇒ Afml (Pred p (the (usubstappt σ V θ))) | Some f ⇒ if FVF f ∩ V = {} then usubstappf (dotsubstt (the (usubstappt σ V θ))) {} f else undeff) ≠ (if FVF (the (SPreds σ p)) ∩ V = {} then usubstappf (dotsubstt (the (usubstappt σ V θ))) {} (the (SPreds σ p)) else undeff)"
using f8 Pred.prems(2) by auto
then have "SPreds σ p = undeff"
using f7 by (metis (no_types, lifting) Pred.prems(2) ‹(if FVF (the (SPreds σ p)) ∩ V = {} then usubstappf (dotsubstt (the (usubstappt σ V θ))) {} (the (SPreds σ p)) else undeff) ≠ usubstappf (dotsubstt (the (usubstappt σ V θ))) {} (the (SPreds σ p))› option.collapse usubstappf_pred2)}
ultimately have "SPreds σ p = undeff"
by fastforce }
moreover
{ assume "(case SPreds σ p of None ⇒ Afml (Pred p (the (usubstappt σ V θ))) | Some f ⇒ if FVF f ∩ V = {} then usubstappf (dotsubstt (the (usubstappt σ V θ))) {} f else undeff) ≠ (if FVF (the (SPreds σ p)) ∩ V = {} then usubstappf (dotsubstt (the (usubstappt σ V θ))) {} (the (SPreds σ p)) else undeff)"
then have "SPreds σ p = undeff"
using f7 by (metis (no_types, lifting) Pred.prems(1) Pred.prems(2) ‹usubstappf σ U (Pred p θ) ≠ usubstappf σ V (Pred p θ)› calculation(2) option.collapse usubstappf_pred usubstappf_pred_conv)}
ultimately have ?thesis
using f9 by fastforce }
then show ?thesis
by blast
qed
next
case (Geq θ η)
then show ?case using usubstappt_det by (metis Geqo_undef usubstappf.simps(2))
next
case (Not x)
then show ?case by (metis Noto.simps(2) usubstappf.simps(3))
next
case (And x1 x2)
then show ?case by (metis Ando_undef usubstappf.simps(4))
next
case (Exists x1 x2)
then show ?case by (metis Existso_undef usubstappf.simps(5))
next
case (Diamond x1 x2)
then show ?case by (metis Diamondo_undef usubstappf.simps(6))
next
case (Game a)
then show ?case by (cases "SGames σ a") (auto)
next
case (Assign x θ)
then show ?case using usubstappt_det by (metis Assigno_undef snd_conv usubstappp.simps(2))
next
case (ODE x θ)
then show ?case using usubstappt_det by (metis ODEo_undef snd_conv usubstappp.simps(8))
next
case (Test φ)
then show ?case by (metis Testo_undef snd_conv usubstappp.simps(3))
next
case (Choice α β)
then show ?case by (metis Choiceo_undef snd_conv usubstappp.simps(4))
next
case (Compose α β)
then show ?case by (metis Composeo_undef snd_conv usubstappp.simps(5))
next
case (Loop α)
then show ?case by (metis Loopo_undef snd_conv usubstappp.simps(6))
next
case (Dual α)
then show ?case by (metis Dualo_undef snd_conv usubstappp.simps(7))
qed

lemma usubstappf_det: "usubstappf σ U φ ≠ undeff ⟹ usubstappf σ V φ ≠ undeff ⟹ usubstappf σ U φ = usubstappf σ V φ"
using usubstappf_and_usubstappp_det by simp

lemma usubstappp_det: "snd(usubstappp σ U α) ≠ undefg ⟹ snd(usubstappp σ V α) ≠ undefg ⟹ snd(usubstappp σ U α) = snd(usubstappp σ V α)"
using usubstappf_and_usubstappp_det by simp

subsection ‹Uniform Substitutions are Antimonotone in Taboos›

lemma usubst_taboos_mon: "fst(usubstappp σ U α) ⊇ U"
proof (induction α arbitrary: U rule: game_induct)
case (Game a)
then show ?case by (cases "SGames σ a") (auto)
next
case (Assign x θ)
then show ?case by fastforce
next
case (ODE x θ)
then show ?case by fastforce
next
case (Test φ)
then show ?case by fastforce
next
case (Choice α β)
then show ?case by fastforce
next
case (Compose α β)
then show ?case by fastforce
next
case (Loop α)
then show ?case by fastforce
next
case (Dual α)
then show ?case by fastforce
qed

lemma fst_pair [simp]: "fst (a,b) = a"
by simp

lemma snd_pair [simp]: "snd (a,b) = b"
by simp

lemma usubstappt_antimon: "V⊆U ⟹ usubstappt σ U θ ≠ undeft ⟹
usubstappt σ U θ = usubstappt σ V θ"
proof (induction θ)
case (Var x)
then show ?case by simp
next
case (Number x)
then show ?case by simp
next
case (Const f)
then show ?case
(*by (smt disjoint_iff_not_equal option.case_eq_if set_rev_mp usappconst_def usubstappt.simps(3))*)
proof - (*sledgehammer*)
have f1: "usubstappt σ U (Const f) = (case SConst σ f of None ⇒ Aterm (Const f) | Some t ⇒ if FVT t ∩ U = {} then Aterm t else undeft)"
have f2: "∀z f za. if za = undeft then (case za of None ⇒ z::trm option | Some x ⇒ f x) = z else (case za of None ⇒ z | Some x ⇒ f x) = f (the za)"
by force
then have "SConst σ f ≠ undeft ⟶ (if FVT (the (SConst σ f)) ∩ U = {} then Aterm (the (SConst σ f)) else undeft) = usappconst σ U f"
using usappconst_def by presburger
then have f3: "SConst σ f ≠ undeft ⟶ FVT (the (SConst σ f)) ∩ U = {}"
by (metis (no_types) Const.prems(2) usubstappt.simps(3))
have f4: "∀V Va. (V ∩ Va = {}) = (∀v. (v::variable) ∈ V ⟶ (∀va. va ∈ Va ⟶ v ≠ va))"
by blast
{ assume "usubstappt σ U (Const f) ≠ usubstappt σ V (Const f)"
then have "usubstappt σ U (Const f) ≠ (case SConst σ f of None ⇒ Aterm (Const f) | Some t ⇒ if FVT t ∩ V = {} then Aterm t else undeft)"
then have "SConst σ f ≠ undeft"
using f2 f1 by metis
then have "SConst σ f ≠ undeft ∧ FVT (the (SConst σ f)) ∩ V = {}"
using f4 f3 by (meson Const.prems(1) subsetD)
then have ?thesis
using f3 f2 usappconst_def usubstappt.simps(3) by presburger }
then show ?thesis
by blast
qed
next
case (Func f θ)
then show ?case using usubstappt_func
(*by (smt disjoint_iff_not_equal option.case_eq_if subset_iff usubstappt.simps(4))*)
proof - (*sledgehammer*)
have f1: "(case usubstappt σ U θ of None ⇒ undeft | Some t ⇒ (case SFuncs σ f of None ⇒ Aterm (trm.Func f t) | Some ta ⇒ if FVT ta ∩ U = {} then usubstappt (dotsubstt t) {} ta else undeft)) ≠ undeft"
using Func.prems(2) by fastforce
have f2: "∀z f za. if za = undeft then (case za of None ⇒ z::trm option | Some x ⇒ f x) = z else (case za of None ⇒ z | Some x ⇒ f x) = f (the za)"
by fastforce
then have f3: "usubstappt σ U θ ≠ undeft"
using f1 by meson
then have f4: "(case usubstappt σ U θ of None ⇒ undeft | Some t ⇒ (case SFuncs σ f of None ⇒ Aterm (trm.Func f t) | Some ta ⇒ if FVT ta ∩ U = {} then usubstappt (dotsubstt t) {} ta else undeft)) = (case SFuncs σ f of None ⇒ Aterm (trm.Func f (the (usubstappt σ U θ))) | Some t ⇒ if FVT t ∩ U = {} then usubstappt (dotsubstt (the (usubstappt σ U θ))) {} t else undeft)"
using f2 by presburger
have f5: "usubstappt σ U θ = undeft ∨ usubstappt σ U θ = usubstappt σ V θ"
using Func.IH Func.prems(1) by fastforce
have "SFuncs σ f ≠ undeft ⟶ (if FVT (the (SFuncs σ f)) ∩ U = {} then usubstappt (dotsubstt (the (usubstappt σ V θ))) {} (the (SFuncs σ f)) else undeft) = (case SFuncs σ f of None ⇒ Aterm (trm.Func f (the (usubstappt σ V θ))) | Some t ⇒ if FVT t ∩ U = {} then usubstappt (dotsubstt (the (usubstappt σ V θ))) {} t else undeft)"
using f2 by presburger
then have "SFuncs σ f ≠ undeft ⟶ (if FVT (the (SFuncs σ f)) ∩ U = {} then usubstappt (dotsubstt (the (usubstappt σ V θ))) {} (the (SFuncs σ f)) else undeft) = usubstappt σ U (trm.Func f θ)"
using f5 f4 f3 usubstappt.simps(4) by presburger
then have f6: "SFuncs σ f ≠ undeft ⟶ FVT (the (SFuncs σ f)) ∩ U = {}"
by (metis (no_types) Func.prems(2))
then have f7: "SFuncs σ f ≠ undeft ⟶ V ⊆ - FVT (the (SFuncs σ f))"
using Func.prems(1) by blast
have f8: "(case usubstappt σ V θ of None ⇒ undeft | Some t ⇒ (case SFuncs σ f of None ⇒ Aterm (trm.Func f t) | Some ta ⇒ if FVT ta ∩ V = {} then usubstappt (dotsubstt t) {} ta else undeft)) = (case SFuncs σ f of None ⇒ Aterm (trm.Func f (the (usubstappt σ V θ))) | Some t ⇒ if FVT t ∩ V = {} then usubstappt (dotsubstt (the (usubstappt σ V θ))) {} t else undeft)"
using f5 f3 f2 by presburger
have "SFuncs σ f ≠ undeft ⟶ usubstappt (dotsubstt (the (usubstappt σ V θ))) {} (the (SFuncs σ f)) = (case SFuncs σ f of None ⇒ Aterm (trm.Func f (the (usubstappt σ V θ))) | Some t ⇒ if FVT t ∩ U = {} then usubstappt (dotsubstt (the (usubstappt σ V θ))) {} t else undeft)"
using f6 f2 by presburger
then have f9: "SFuncs σ f ≠ undeft ⟶ usubstappt (dotsubstt (the (usubstappt σ V θ))) {} (the (SFuncs σ f)) = usubstappt σ U (trm.Func f θ)"
using f5 f4 f3 usubstappt.simps(4) by presburger
{ assume "usubstappt σ U (trm.Func f θ) ≠ usubstappt σ V (trm.Func f θ)"
moreover
{ assume "(case SFuncs σ f of None ⇒ Aterm (trm.Func f (the (usubstappt σ V θ))) | Some t ⇒ if FVT t ∩ V = {} then usubstappt (dotsubstt (the (usubstappt σ V θ))) {} t else undeft) ≠ Aterm (trm.Func f (the (usubstappt σ V θ)))"
then have "SFuncs σ f ≠ undeft"
using f2 by meson }
ultimately have "SFuncs σ f ≠ undeft"
using f5 f3 by fastforce
then have ?thesis
using f9 f8 f7 f2 by (simp add: disjoint_eq_subset_Compl inf.commute) }
then show ?thesis
by blast
qed
next
case (Plus θ1 θ2)
then show ?case using Pluso_undef by auto
next
case (Times θ1 θ2)
then show ?case using Timeso_undef by auto
next
case (Differential θ)
then show ?case using Differentialo_undef by auto
qed

text ‹Uniform Substitutions of Games have monotone taboo output›

lemma usubstappp_fst_mon: "U⊆V ⟹ fst(usubstappp σ U α) ⊆ fst(usubstappp σ V α)"
proof (induction α arbitrary: U V rule: game_induct)
case (Game a)
then show ?case by (cases "SGames σ a") (auto)
next
case (Assign x θ)
then show ?case by auto
next
case (ODE x θ)
then show ?case by auto
next
case (Test φ)
then show ?case by auto
next
case (Choice α β)
then show ?case by (metis Un_mono fst_pair usubstappp_choice)
next
case (Compose α β)
then show ?case by (metis fst_pair usubstappp_compose)
next
case (Loop α)
then show ?case by (metis fst_pair usubstappp_loop)
next
case (Dual α)
then show ?case by (metis fst_pair usubstappp_dual)
qed

lemma usubstappf_and_usubstappp_antimon:
shows "V⊆U ⟹ usubstappf σ U φ ≠ undeff ⟹ usubstappf σ U φ = usubstappf σ V φ"
and "V⊆U ⟹ snd(usubstappp σ U α) ≠ undefg ⟹ snd(usubstappp σ U α) = snd(usubstappp σ V α)"
proof-
have "V⊆U ⟹ usubstappf σ U φ ≠ undeff ⟹ usubstappf σ V φ ≠ undeff"
and "V⊆U ⟹ snd(usubstappp σ U α) ≠ undefg ⟹ snd(usubstappp σ V α) ≠ undefg"
proof (induction φ and α arbitrary: U V and U V)
case (Pred p θ)
then show ?case using usubstappt_antimon usubstappf_pred
(*by (smt Un_mono disjoint_eq_subset_Compl empty_subsetI inf.commute option.case_eq_if sup.absorb_iff1 sup.absorb_iff2 usubstappf.simps(1)) *)
proof - (*sledgehammer*)
have f1: "∀v. v ∉ V ∨ v ∈ U"
using Pred.prems(1) by auto
have f2: "∀z f za. if za = undeff then (case za of None ⇒ z::fml option | Some x ⇒ f x) = z else (case za of None ⇒ z | Some x ⇒ f x) = f (the za)"
have f3: "(case usubstappt σ U θ of None ⇒ undeff | Some t ⇒ (case SPreds σ p of None ⇒ Afml (Pred p t) | Some f ⇒ if FVF f ∩ U = {} then usubstappf (dotsubstt t) {} f else undeff)) ≠ undeff"
using Pred.prems(2) by auto
have f4: "∀z f za. if za = undeft then (case za of None ⇒ z::fml option | Some x ⇒ f x) = z else (case za of None ⇒ z | Some x ⇒ f x) = f (the za)"
then have f5: "usubstappt σ U θ ≠ undeft"
using f3 by meson
then have f6: "(case usubstappt σ U θ of None ⇒ undeff | Some t ⇒ (case SPreds σ p of None ⇒ Afml (Pred p t) | Some f ⇒ if FVF f ∩ U = {} then usubstappf (dotsubstt t) {} f else undeff)) = (case SPreds σ p of None ⇒ Afml (Pred p (the (usubstappt σ U θ))) | Some f ⇒ if FVF f ∩ U = {} then usubstappf (dotsubstt (the (usubstappt σ U θ))) {} f else undeff)"
using f4 by presburger
have f7: "usubstappt σ U θ = usubstappt σ V θ"
using f5 by (meson Pred.prems(1) usubstappt_antimon)
then have f8: "SPreds σ p = undeff ⟶ usubstappf σ U (Pred p θ) = usubstappf σ V (Pred p θ)"
using f2 usubstappf.simps(1) by presburger
obtain vv :: "variable set ⇒ variable set ⇒ variable" where
"∀x0 x1. (∃v2. v2 ∈ x1 ∧ (∃v3. v3 ∈ x0 ∧ v2 = v3)) = (vv x0 x1 ∈ x1 ∧ (∃v3. v3 ∈ x0 ∧ vv x0 x1 = v3))"
by moura
then obtain vva :: "variable set ⇒ variable set ⇒ variable" where
f9: "∀V Va. (V ∩ Va ≠ {} ∨ (∀v. v ∉ V ∨ (∀va. va ∉ Va ∨ v ≠ va))) ∧ (V ∩ Va = {} ∨ vv Va V ∈ V ∧ vva Va V ∈ Va ∧ vv Va V = vva Va V)"
by moura
then have f10: "(FVF (the (SPreds σ p)) ∩ V ≠ {} ∨ (∀v. v ∉ FVF (the (SPreds σ p)) ∨ (∀va. va ∉ V ∨ v ≠ va))) ∧ (FVF (the (SPreds σ p)) ∩ V = {} ∨ vv V (FVF (the (SPreds σ p))) ∈ FVF (the (SPreds σ p)) ∧ vva V (FVF (the (SPreds σ p))) ∈ V ∧ vv V (FVF (the (SPreds σ p))) = vva V (FVF (the (SPreds σ p))))"
by presburger
{ assume "vv V (FVF (the (SPreds σ p))) ∉ FVF (the (SPreds σ p)) ∨ vva V (FVF (the (SPreds σ p))) ∉ V ∨ vv V (FVF (the (SPreds σ p))) ≠ vva V (FVF (the (SPreds σ p)))"
moreover
{ assume "(if FVF (the (SPreds σ p)) ∩ V = {} then usubstappf (dotsubstt (the (usubstappt σ V θ))) {} (the (SPreds σ p)) else undeff) ≠ undeff"
moreover
{ assume "(if FVF (the (SPreds σ p)) ∩ V = {} then usubstappf (dotsubstt (the (usubstappt σ V θ))) {} (the (SPreds σ p)) else undeff) ≠ usubstappf σ V (Pred p θ)"
then have "(case SPreds σ p of None ⇒ Afml (Pred p (the (usubstappt σ V θ))) | Some f ⇒ if FVF f ∩ V = {} then usubstappf (dotsubstt (the (usubstappt σ V θ))) {} f else undeff) ≠ (if FVF (the (SPreds σ p)) ∩ V = {} then usubstappf (dotsubstt (the (usubstappt σ V θ))) {} (the (SPreds σ p)) else undeff)"
using f7 f5 f4 by simp
then have "SPreds σ p = undeff"
using f2 by (metis (no_types, lifting) ‹(if FVF (the (SPreds σ p)) ∩ V = {} then usubstappf (dotsubstt (the (usubstappt σ V θ))) {} (the (SPreds σ p)) else undeff) ≠ usubstappf σ V (Pred p θ)› calculation f5 f7 option.collapse usubstappf_pred)}
ultimately have "usubstappf σ V (Pred p θ) = undeff ⟶ SPreds σ p = undeff"
by fastforce }
moreover
{ assume "usubstappf (dotsubstt (the (usubstappt σ V θ))) {} (the (SPreds σ p)) ≠ usubstappf σ U (Pred p θ)"
then have "usubstappf (dotsubstt (the (usubstappt σ V θ))) {} (the (SPreds σ p)) ≠ (case SPreds σ p of None ⇒ Afml (Pred p (the (usubstappt σ U θ))) | Some f ⇒ if FVF f ∩ U = {} then usubstappf (dotsubstt (the (usubstappt σ U θ))) {} f else undeff)"
using f6 by simp
then have "usubstappf (dotsubstt (the (usubstappt σ V θ))) {} (the (SPreds σ p)) ≠ (case SPreds σ p of None ⇒ Afml (Pred p (the (usubstappt σ V θ))) | Some f ⇒ if FVF f ∩ U = {} then usubstappf (dotsubstt (the (usubstappt σ V θ))) {} f else undeff)"
using f7 by (metis f7)
moreover
{ assume "(case SPreds σ p of None ⇒ Afml (Pred p (the (usubstappt σ V θ))) | Some f ⇒ if FVF f ∩ U = {} then usubstappf (dotsubstt (the (usubstappt σ V θ))) {} f else undeff) ≠ (if FVF (the (SPreds σ p)) ∩ U = {} then usubstappf (dotsubstt (the (usubstappt σ V θ))) {} (the (SPreds σ p)) else undeff)"
then have "SPreds σ p = undeff"
using f2  by (metis (no_types, lifting) Pred.prems(2) ‹usubstappf (dotsubstt (the (usubstappt σ V θ))) {} (the (SPreds σ p)) ≠ usubstappf σ U (Pred p θ)› f5 f7 option.collapse usubstappf_pred usubstappf_pred2)}
ultimately have "FVF (the (SPreds σ p)) ∩ U = {} ⟶ SPreds σ p = undeff"
by force }
ultimately have "FVF (the (SPreds σ p)) ∩ U = {} ∧ usubstappf σ V (Pred p θ) = undeff ⟶ SPreds σ p = undeff"
using f10 by (metis Pred.prems(2)) }
moreover
{ assume "FVF (the (SPreds σ p)) ∩ U ≠ {}"
then have "(if FVF (the (SPreds σ p)) ∩ U = {} then usubstappf (dotsubstt (the (usubstappt σ V θ))) {} (the (SPreds σ p)) else undeff) ≠ (case SPreds σ p of None ⇒ Afml (Pred p (the (usubstappt σ U θ))) | Some f ⇒ if FVF f ∩ U = {} then usubstappf (dotsubstt (the (usubstappt σ U θ))) {} f else undeff)"
using f6 Pred.prems(2) by auto
then have "(if FVF (the (SPreds σ p)) ∩ U = {} then usubstappf (dotsubstt (the (usubstappt σ V θ))) {} (the (SPreds σ p)) else undeff) ≠ (case SPreds σ p of None ⇒ Afml (Pred p (the (usubstappt σ V θ))) | Some f ⇒ if FVF f ∩ U = {} then usubstappf (dotsubstt (the (usubstappt σ V θ))) {} f else undeff)"
using f7 by (metis  ‹FVF (the (SPreds σ p)) ∩ U ≠ {}›)
then have "(case SPreds σ p of None ⇒ Afml (Pred p (the (usubstappt σ V θ))) | Some f ⇒ if FVF f ∩ U = {} then usubstappf (dotsubstt (the (usubstappt σ V θ))) {} f else undeff) ≠ (if FVF (the (SPreds σ p)) ∩ U = {} then usubstappf (dotsubstt (the (usubstappt σ V θ))) {} (the (SPreds σ p)) else undeff)"
by simp
then have "SPreds σ p = undeff"
using f2
proof -
show ?thesis
by (metis (no_types) Pred.prems(2) ‹FVF (the (SPreds σ p)) ∩ U ≠ {}› option.discI option.expand option.sel usubstappf_pred2)
qed }
ultimately have "usubstappf σ V (Pred p θ) = undeff ⟶ SPreds σ p = undeff"
using f9 f1 by meson
then show ?thesis
using f8 by (metis (full_types) Pred.prems(2))
qed

next
case (Geq θ η)
then show ?case using usubstappt_antimon using Geqo_undef by auto
next
case (Not x)
then show ?case using Noto_undef by auto
next
case (And x1 x2)
then show ?case using Ando_undef by auto
next
case (Exists x1 x2)
then show ?case using Existso_undef
by (metis (no_types, lifting) Un_mono subsetI usubstappf.simps(5))
next
case (Diamond x1 x2)
then show ?case using Diamondo_undef usubstappf.simps(6) usubstappp_fst_mon by metis
next
case (Game a)
then show ?case by (cases "SGames σ a") (auto)
next
case (Assign x θ)
then show ?case using usubstappt_antimon by (metis Assigno_undef snd_conv usubstappp.simps(2))
next
case (ODE x θ)
then show ?case using usubstappt_antimon ODEo_undef
by (metis (no_types, hide_lams) Un_mono order_refl snd_conv usubstappp.simps(8))
next
case (Test φ)
then show ?case by (metis Testo_undef snd_conv usubstappp.simps(3))
next
case (Choice α β)
then show ?case using Choiceo_undef by auto
next
case (Compose α β)
then show ?case
using usubstappp_compose[where σ=σ and U=U and α=α and β=β] usubstappp_compose[where σ=σ and U=V and α=α and β=β]
Composeo_undef[where α=‹snd (usubstappp σ U α)› and β=‹snd (usubstappp σ (fst (usubstappp σ U α)) β)›]
Composeo_undef[where α=‹snd (usubstappp σ V α)› and β=‹snd (usubstappp σ (fst (usubstappp σ V α)) β)›]
snd_conv usubstappp_fst_mon by metis
(*proof-
from Compose have ca: "snd (usubstappp σ U (α ;; β)) ≠ undefg" by simp
have decU: "snd (usubstappp σ U (α ;; β)) = Composeo (snd(usubstappp σ U α)) (snd(usubstappp σ (fst(usubstappp σ U α)) β))" using usubstappp_compose by simp
have decV: "snd (usubstappp σ V (α ;; β)) = Composeo (snd(usubstappp σ V α)) (snd(usubstappp σ (fst(usubstappp σ V α)) β))" using usubstappp_compose by simp
from Compose have fact1: "snd(usubstappp σ V α) ≠ undefg" using Composeo_undef by auto
from Compose have fact2: "snd(usubstappp σ (fst(usubstappp σ U α)) β) ≠ undefg" using Composeo_undef by auto
have rel: "fst(usubstappp σ V α) ⊆ fst(usubstappp σ U α)" using ‹V⊆U› usubstappp_fst_mon by auto
from Compose have fact3: "snd(usubstappp σ (fst(usubstappp σ V α)) β) ≠ undefg" using fact2 rel by auto
then show ?thesis by (simp add: Composeo_undef fact1)
qed*)
next
case (Loop α)
then show ?case using Loopo_undef snd_conv usubstappp.simps(6) usubstappp_fst_mon by metis
next
case (Dual α)
then show ?case by (metis Dualo_undef snd_conv usubstappp.simps(7))
qed
from this show "V⊆U ⟹ usubstappf σ U φ ≠ undeff ⟹ usubstappf σ U φ = usubstappf σ V φ"
and "V⊆U ⟹ snd(usubstappp σ U α) ≠ undefg ⟹ snd(usubstappp σ U α) = snd(usubstappp σ V α)" using usubstappf_and_usubstappp_det by auto
qed

lemma usubstappf_antimon: "V⊆U ⟹ usubstappf σ U φ ≠ undeff ⟹ usubstappf σ U φ = usubstappf σ V φ"
using usubstappf_and_usubstappp_antimon by simp

lemma usubstappp_antimon: "V⊆U ⟹ snd(usubstappp σ U α) ≠ undefg ⟹ snd(usubstappp σ U α) = snd(usubstappp σ V α)"
using usubstappf_and_usubstappp_antimon by simp

subsection ‹Taboo Lemmas›

lemma usubstappp_loop_conv: "snd (usubstappp σ U (Loop α)) ≠ undefg ⟹
snd(usubstappp σ U α) ≠ undefg ∧
snd(usubstappp σ (fst(usubstappp σ U α)) α) ≠ undefg"
(*using usubstappp_loop Loopo_undef*)
proof
assume a: "snd (usubstappp σ U (Loop α)) ≠ undefg"
have fact: "fst(usubstappp σ U α) ⊇ U" using usubst_taboos_mon by simp
show "snd(usubstappp σ (fst(usubstappp σ U α)) α) ≠ undefg" using a usubstappp_loop Loopo_undef by simp
then show "snd(usubstappp σ U α) ≠ undefg" using a usubstappp_loop Loopo_undef fact usubstappp_antimon by auto
qed

text ‹Lemma 13 of 🌐‹http://arxiv.org/abs/1902.07230››

lemma usubst_taboos: "snd(usubstappp σ U α)≠undefg ⟹ fst(usubstappp σ U α) ⊇ U ∪ BVG(the (snd(usubstappp σ U α)))"
proof (induction α arbitrary: U rule: game_induct)
case (Game a)
then show ?case by (cases "SGames σ a") (auto)
next
case (Assign x θ)
then show ?case
using BVG_assign Assigno_undef
by (metis (no_types, lifting) Assigno.elims BVG_assign_other fst_pair option.sel singletonI snd_pair subsetI union_or usubstappp.simps(2))
next
case (ODE x θ)
then show ?case
using BVG_ODE ODEo_undef
by (metis (no_types, lifting) ODEo.elims Un_least fst_pair option.sel snd_conv sup.coboundedI2 usubst_taboos_mon usubstappp.simps(8))
next
case (Test p)
then show ?case
using BVG_test Testo_undef usubst_taboos_mon by auto
next
case (Choice α β)
then show ?case (*using usubstappp.simps Product_Type.fst_conv Product_Type.snd_conv BVG_choice*)
proof-
from Choice have IHa: "fst(usubstappp σ U α) ⊇ U ∪ BVG(the (snd(usubstappp σ U α)))" by (simp add: Choiceo_undef)
from Choice have IHb: "fst(usubstappp σ U β) ⊇ U ∪ BVG(the (snd(usubstappp σ U β)))" by (simp add: Choiceo_undef)
have fact: "BVG(the (snd(usubstappp σ U α))) ∪ BVG(the (snd(usubstappp σ U β))) ⊇ BVG(the (snd(usubstappp σ U (Choice α β))))" using BVG_choice
(*by (smt Choice.prems Choiceo.simps(1) Choiceo_undef option.collapse option.sel snd_pair usubstappp_choice)*)
proof -
have "Agame (the (snd (usubstappp σ U α)) ∪∪ the (snd (usubstappp σ U β))) = Choiceo (snd (usubstappp σ U α)) (snd (usubstappp σ U β))"
by (metis (no_types) Choice.prems Choiceo.simps(1) option.collapse usubstappp_choice_conv)
then show ?thesis
by (metis (no_types) BVG_choice Choice.prems Pair_inject option.collapse option.inject surjective_pairing usubstappp.simps(4))
qed
from IHa and IHb have "fst(usubstappp σ U α) ∪ fst(usubstappp σ U β) ⊇ U ∪ BVG(the (snd(usubstappp σ U α))) ∪ BVG(the (snd(usubstappp σ U β)))" by auto
then have "fst(usubstappp σ U (Choice α β)) ⊇ U ∪ BVG(the (snd(usubstappp σ U α))) ∪ BVG(the (snd(usubstappp σ U β)))" using usubstappp.simps Let_def by auto
then show "fst(usubstappp σ U (Choice α β)) ⊇ U ∪ BVG(the (snd(usubstappp σ U (Choice α β))))" using usubstappp.simps fact by auto
qed
next
case (Compose α β)
then show ?case
proof-
let ?V = "fst(usubstappp σ U α)"
let ?W = "fst(usubstappp σ ?V β)"
from Compose have IHa: "?V ⊇ U ∪ BVG(the (snd(usubstappp σ U α)))" by (simp add: Composeo_undef)
from Compose have IHb: "?W ⊇ ?V ∪ BVG(the (snd(usubstappp σ ?V β)))" by (simp add: Composeo_undef)
have fact: "BVG(the (snd(usubstappp σ U α))) ∪ BVG(the (snd(usubstappp σ ?V β))) ⊇ BVG(the (snd(usubstappp σ U (Compose α β))))" using usubstappp.simps BVG_compose
(*by (smt Compose.prems Composeo.simps(1) Composeo_undef option.collapse option.sel snd_pair)*)
proof -
have f1: "∀z. z = undefg ∨ Agame (the z) = z"
using option.collapse by blast
then have "Agame (the (snd (usubstappp σ U α)) ;; the (snd (usubstappp σ (fst (usubstappp σ U α)) β))) = snd (usubstappp σ U (α ;; β))"
using Compose.prems Composeo_undef by auto
then show ?thesis
using f1 by (metis (no_types) BVG_compose Compose.prems option.inject)
qed
have "?W ⊇ U ∪ BVG(the (snd(usubstappp σ U α))) ∪ BVG(the (snd(usubstappp σ ?V β)))" using usubstappp.simps Let_def IHa IHb by auto
then have "?W ⊇ U ∪ BVG(the (snd(usubstappp σ U (Compose α β))))" using fact by auto
then show "fst(usubstappp σ U (Compose α β)) ⊇ U ∪ BVG(the (snd(usubstappp σ U (Compose α β))))" using usubstappp.simps Let_def by simp
qed
next
case (Loop α)
then show ?case
proof-
let ?V = "fst(usubstappp σ U α)"
let ?W = "fst(usubstappp σ ?V α)"
from Loop have defα: "snd(usubstappp σ U α) ≠ undefg" using usubstappp_loop_conv by simp
from Loop have IHdef: "?V ⊇ U ∪ BVG(the (snd(usubstappp σ U α)))"
using defα usubstappp_loop[where σ=σ and U=U and α=α] Loopo_undef[where α=‹snd (usubstappp σ (fst (usubstappp σ U α)) α)›]   by auto
from Loop have IH: "?W ⊇ ?V ∪ BVG(the (snd(usubstappp σ ?V α)))" by (simp add: Loopo_undef)
then have Vfix: "?V ⊇ BVG(the (snd(usubstappp σ ?V α)))"
using usubstappp_det by (metis IHdef Loop.prems le_sup_iff usubstappp_loop_conv)
then have "?V ⊇ U ∪ BVG(the (snd(usubstappp σ U (Loop α))))"
using usubstappp.simps Vfix IHdef BVG_loop usubst_taboos_mon usubstappp_loop_conv
(*by (smt Loop.prems Loopo.simps(1) Un_mono option.collapse option.sel snd_pair sup.absorb_iff1)*)
proof - (*sledgehammer*)
have f1: "∀z. z = undefg ∨ Agame (the z) = z"
using option.collapse by blast
have "snd (usubstappp σ U α) ≠ undefg ∧ snd (usubstappp σ (fst (usubstappp σ U α)) α) ≠ undefg"
using Loop.prems usubstappp_loop_conv by blast
then have "Agame (Loop (the (snd (usubstappp σ (fst (usubstappp σ U α)) α)))) = snd (usubstappp σ U (Loop α))"
by force
then show ?thesis
using f1 by (metis (no_types) BVG_loop Loop.prems Vfix option.inject sup.absorb_iff1 sup.mono usubst_taboos_mon)
qed
then show "fst(usubstappp σ U (Loop α)) ⊇ U ∪ BVG(the (snd(usubstappp σ U (Loop α))))" using usubstappp.simps Let_def by simp
qed
next
case (Dual α)
then show ?case
(*using BVG_dual usubstappp.simps Let_def by auto*)
proof-
let ?V = "fst(usubstappp σ U α)"
from Dual have IH: "?V ⊇ U ∪ BVG(the (snd(usubstappp σ U α)))" by (simp add: Dualo_undef)
have fact: "BVG(the (snd(usubstappp σ U α))) ⊇ BVG(the (snd(usubstappp σ U (Dual α))))" using usubstappp.simps BVG_dual
by (metis (no_types, lifting) Dual.prems Dualo.simps(1) Dualo.simps(2) option.collapse option.sel snd_pair)
then have "?V ⊇ U ∪ BVG(the (snd(usubstappp σ U (Dual α))))" using IH fact by auto
then show "fst(usubstappp σ U (Dual α)) ⊇ U ∪ BVG(the (snd(usubstappp σ U (Dual α))))" using usubstappp.simps Let_def by simp
qed
qed

text ‹Modified interpretation ‹repI I f d› replaces the interpretation of constant function ‹f› in the interpretation ‹I› with ‹d››
definition repc :: " interp ⇒ ident ⇒ real ⇒ interp"
where "repc I f d ≡  mkinterp((λc. if c = f then d else Consts I c), Funcs I, Preds I, Games I)"

lemma repc_consts [simp]: "Consts (repc I f d) c = (if (c=f) then d else Consts I c)"
unfolding repc_def by auto
lemma repc_funcs [simp]: "Funcs (repc I f d) = Funcs I"
unfolding repc_def by simp
lemma repc_preds [simp]: "Preds (repc I f d) = Preds I"
unfolding repc_def by simp
lemma repc_games [simp]: "Games (repc I f d) = Games I"
unfolding repc_def by (simp add: mon_mono)

lemma adjoint_stays_mon: "mono (case SGames σ a of None ⇒ Games I a | Some r ⇒ λX. game_sem I r X)"
using game_sem_mono game_sem.simps(1)
by (metis disjE_realizer2 option.case_distrib)
(*proof -
have "∀z p b i f. (mono (case z of None ⇒ f | Some x ⇒ game_sem i x) ∨ ¬ (case z of None ⇒ b | Some x ⇒ p x)) ∨ ¬ mono f"
by (metis (no_types) disjE_realizer2 game_sem_mono)
then show ?thesis
by (metis (no_types) game_sem.simps(1) game_sem_mono option.case_distrib)
qed*)

text ‹adjoint interpretation ‹adjoint σ I ω› to ‹σ› of interpretation ‹I› in state ‹ω››

definition adjoint:: "usubst ⇒ (interp ⇒ state ⇒ interp)"
where "adjoint σ I ω = mkinterp(
(λf. (case SConst σ f of None ⇒ Consts I f| Some r ⇒ term_sem I r ω)),
(λf. (case SFuncs σ f of None ⇒ Funcs I f | Some r ⇒ λd. term_sem (repc I dotid d) r ω)),
(λp. (case SPreds σ p of None ⇒ Preds I p | Some r ⇒ λd. ω∈fml_sem (repc I dotid d) r)),
(λa. (case SGames σ a of None ⇒ Games I a | Some r ⇒ λX. game_sem I r X))
)"

lemma adjoint_consts: "Consts (adjoint σ I ω) f = term_sem I (case SConst σ f of Some r ⇒ r | None ⇒ Const f) ω"
unfolding adjoint_def by (cases "SConst σ f=None") (auto)

lemma adjoint_funcs: "Funcs (adjoint σ I ω) f = (case SFuncs σ f of None ⇒ Funcs I f | Some r ⇒ λd. term_sem (repc I dotid d) r ω)"

lemma adjoint_funcs_match: "SFuncs σ f=Some r ⟹ Funcs (adjoint σ I ω) f = (λd. term_sem (repc I dotid d) r ω)"

lemma adjoint_funcs_skip: "SFuncs σ f=None ⟹ Funcs (adjoint σ I ω) f = Funcs I f"

lemma adjoint_preds: "Preds (adjoint σ I ω) p = (case SPreds σ p of None ⇒ Preds I p | Some r ⇒ λd. ω∈fml_sem (repc I dotid d) r)"

lemma adjoint_preds_skip: "SPreds σ p=None ⟹ Preds (adjoint σ I ω) p = Preds I p"

lemma adjoint_preds_match: "SPreds σ p=Some r ⟹ Preds (adjoint σ I ω) p = (λd. ω∈fml_sem (repc I dotid d) r)"

lemma adjoint_games [simp]: "Games (adjoint σ I ω) a = (case SGames σ a of None ⇒ Games I a | Some r ⇒ λX. game_sem I r X)"

lemma adjoint_dotsubstt: "adjoint (dotsubstt θ) I ω = repc I dotid (term_sem I θ ω)"
proof-
let ?lhs = "adjoint (dotsubstt θ) I ω"
let ?rhs = "repc I dotid (term_sem I θ ω)"
have feq: "Funcs ?lhs = Funcs ?rhs" using repc_funcs adjoint_funcs dotsubstt_def by auto
moreover have peq: "Preds ?lhs = Preds ?rhs" using repc_preds adjoint_preds dotsubstt_def by auto
moreover have geq: "Games ?lhs = Games ?rhs" using repc_games adjoint_games dotsubstt_def by auto
moreover have ceq: "Consts ?lhs = Consts ?rhs" using repc_consts  adjoint_consts dotsubstt_def by auto
show ?thesis using mkinterp_eq[where I=‹?lhs› and J=‹?rhs›] feq peq geq ceq by simp
qed

subsection ‹Uniform Substitution for Terms›

text ‹Lemma 15 of 🌐‹http://arxiv.org/abs/1902.07230››
theorem usubst_term: "Uvariation ν ω U ⟹ usubstappt σ U θ≠undeft ⟹
term_sem I (the (usubstappt σ U θ)) ν = term_sem (adjoint σ I ω) θ ν"
proof-
assume vaouter: "Uvariation ν ω U"
assume defouter: "usubstappt σ U θ≠undeft"
show "usubstappt σ U θ≠undeft ⟹ term_sem I (the (usubstappt σ U θ)) ν = term_sem (adjoint σ I ω) θ ν" for σ θ
using vaouter proof (induction arbitrary: ν ω rule: usubstappt_induct)
case (Var σ U x)
then show ?case by simp
next
case (Number σ U r)
then show ?case by simp
next
case (Const σ U f)
then show ?case
proof (cases "SConst σ f")
case None
next
case (Some r)
then have varcond: "FVT(r)∩U={}" using Const usubstappt_const usubstappt_const_conv by (metis option.inject option.simps(3))
from Some have "term_sem I (the (usubstappt σ U (Const f))) ν = term_sem I r ν" by (simp add: varcond)
also have "... = term_sem I r ω" using Const coincidence_term_cor[of ν ω U r] varcond by simp
also have "... = Consts (adjoint σ I ω) f" using Some adjoint_consts by simp
also have "... = term_sem (adjoint σ I ω) (Const f) ν" by auto
finally show "term_sem I (the (usubstappt σ U (Const f))) ν = term_sem (adjoint σ I ω) (Const f) ν" .
qed
next
case (FuncMatch σ U f θ)
then have va: "Uvariation ν ω U" by simp
then show ?case
proof (cases "SFuncs σ f")
case None
from FuncMatch and None have IHsubterm: "term_sem I (the (usubstappt σ U θ)) ν = term_sem (adjoint σ I ω) θ ν" using va
from None show ?thesis using usubstappt_func IHsubterm adjoint_funcs
by (metis (no_types, lifting) FuncMatch.prems(1) option.case_eq_if option.sel term_sem.simps(4) usubstappt.simps(4))
next
case (Some r)
then have varcond: "FVT(r)∩U={}" using FuncMatch usubstappt_func usubstappt_func2 usubstappt_func_conv by meson
from FuncMatch have subdef: "usubstappt σ U θ ≠ undeft" using usubstappt_func_conv by auto
from FuncMatch and Some
have IHsubterm: "term_sem I (the (usubstappt σ U θ)) ν = term_sem (adjoint σ I ω) θ ν" using va subdef by blast
from FuncMatch and Some
have IHsubsubst: "⋀ν ω. Uvariation ν ω {} ⟹ term_sem I (the (usubstappt (dotsubstt (the (usubstappt σ U θ))) {} r)) ν = term_sem (adjoint (dotsubstt (the (usubstappt σ U θ))) I ω) r ν"
using subdef varcond by fastforce

let ?d = "term_sem I (the (usubstappt σ U θ)) ν"
have deq: "?d = term_sem (adjoint σ I ω) θ ν" by (rule IHsubterm)
let ?dotIa = "adjoint (dotsubstt (the (usubstappt σ U θ))) I ν"

from Some
have "term_sem I (the (usubstappt σ U (Func f θ))) ν = term_sem I (the (usubstappt (dotsubstt (the (usubstappt σ U θ))) {} r)) ν" using subdef varcond by force
also have "... = term_sem ?dotIa r ν" using IHsubsubst[where ν=ν and ω=ν] Uvariation_empty by auto
also have "... = term_sem (repc I dotid ?d) r ν" using adjoint_dotsubstt[where θ=‹the (usubstappt σ U θ)› and I=I and ω=ν] by simp
also have "... = term_sem (repc I dotid ?d) r ω" using coincidence_term_cor[where ω=ν and ω'=ω and U=U and θ=r and I=‹repc I dotid ?d›] va varcond by simp
(*I.^dω⟦σf(⋅)⟧  also have "... = term_sem ?dotIa r ω" using coincidence_term_cor[of ν ω U r ?dotIa] uv varcond by simp*)
also have "... = (Funcs (adjoint σ I ω) f)(?d)" using adjoint_funcs_match Some by simp
also have "... = (Funcs (adjoint σ I ω) f)(term_sem (adjoint σ I ω) θ ν)" using deq by simp
also have "... = term_sem (adjoint σ I ω) (Func f θ) ν" by simp
finally show "term_sem I (the (usubstappt σ U (Func f θ))) ν = term_sem (adjoint σ I ω) (Func f θ) ν" .
qed
next
case (Plus σ U θ η)
then show ?case using Pluso_undef by auto
next
case (Times σ U θ η)
then show ?case using Timeso_undef by auto
next
case (Differential σ U θ)
from Differential have subdef: "usubstappt σ allvars θ ≠ undeft" using usubstappt_differential_conv by simp
from Differential have IH: "⋀ν. term_sem I (the (usubstappt σ allvars θ)) ν = term_sem (adjoint σ I ω) θ ν" using subdef Uvariation_univ by blast (*by auto*)

have "term_sem I (the (usubstappt σ U (Differential θ))) ν = term_sem I (Differential (the (usubstappt σ allvars θ))) ν" using subdef by force
also have "... = sum(λx. ν(DVar x)*deriv(λX. term_sem I (the (usubstappt σ allvars θ)) (repv ν (RVar x) X))(ν(RVar x)))(allidents)" by simp
also have "... = sum(λx. ν(DVar x)*deriv(λX. term_sem (adjoint σ I ω) θ (repv ν (RVar x) X))(ν(RVar x)))(allidents)" using IH by auto
also have "... = term_sem (adjoint σ I ω) (Differential θ) ν" by simp
finally show "term_sem I (the (usubstappt σ U (Differential θ))) ν = term_sem (adjoint σ I ω) (Differential θ) ν" .
qed
qed

subsection ‹Uniform Substitution for Formulas and Games›

paragraph ‹Separately Prove Crucial Ingredient for the ODE Case of ‹usubst_fml_game››

lemma same_ODE_same_sol:
"(⋀ν. Uvariation ν (F(0)) {RVar x,DVar x} ⟹ term_sem I θ ν = term_sem J η ν)
⟹ solves_ODE I F x θ = solves_ODE J F x η"
using Uvariation_Vagree Vagree_def solves_ODE_def
(*by (smt double_complement)*)
proof-
assume va: "⋀ν. Uvariation ν (F(0)) {RVar x,DVar x} ⟹ term_sem I θ ν = term_sem J η ν"
then have va2: "⋀ν. Uvariation ν (F(0)) {RVar x,DVar x} ⟹ term_sem J η ν = term_sem I θ ν" by simp
have one: "⋀I J θ η. (⋀ν. Uvariation ν (F(0)) {RVar x,DVar x} ⟹ term_sem I θ ν = term_sem J η ν)
⟹ solves_ODE I F x θ ⟹ solves_ODE J F x η"
proof-
fix I J θ η
assume vaflow: "⋀ν. Uvariation ν (F(0)) {RVar x,DVar x} ⟹ term_sem I θ ν = term_sem J η ν"
assume sol: "solves_ODE I F x θ"
from vaflow and sol show "solves_ODE J F x η" unfolding solves_ODE_def using Uvariation_Vagree coincidence_term
by (metis double_complement solves_Vagree sol)
qed
show "solves_ODE I F x θ = solves_ODE J F x η" using one[where θ=θ and η=η, OF va] one[where θ=η and η=θ, OF va2]
by force
qed

lemma usubst_ode:
assumes subdef: "usubstappt σ {RVar x,DVar x} θ ≠ undeft"
shows "solves_ODE I F x (the (usubstappt σ {RVar x,DVar x} θ)) = solves_ODE (adjoint σ I (F(0))) F x θ"
proof-
have vaflow: "⋀F θ ζ. solves_ODE I F x θ ⟹ Uvariation (F(ζ)) (F(0)) {RVar x,DVar x}" using solves_Vagree_trans by simp
from subdef have IH: "⋀ν. Uvariation ν (F(0)) {RVar x,DVar x} ⟹ term_sem I (the (usubstappt σ {RVar x,DVar x} θ)) ν = term_sem (adjoint σ I (F(0))) θ ν" by (simp add: usubst_term)
then show ?thesis using IH vaflow solves_ODE_def Uvariation_Vagree same_ODE_same_sol by blast
qed

lemma usubst_ode_ext:
assumes     uv: "Uvariation (F(0)) ω (U∪{RVar x,DVar x})"
assumes subdef: "usubstappt σ (U∪{RVar x,DVar x}) θ ≠ undeft"
shows "solves_ODE I F x (the (usubstappt σ (U∪{RVar x,DVar x}) θ)) = solves_ODE (adjoint σ I ω) F x θ"
(*using usubst_ode usubstappt_det usubstappt_antimon Uvariation_Vagree Uvariation_mon *)
proof-
have vaflow1: "⋀F θ ζ. solves_ODE I F x (the (usubstappt σ (U∪{RVar x,DVar x}) θ)) ⟹ Uvariation (F(ζ)) (F(0)) {RVar x,DVar x}" using solves_Vagree_trans by simp
have vaflow2: "⋀F θ ζ. solves_ODE (adjoint σ I ω) F x θ ⟹ Uvariation (F(ζ)) (F(0)) {RVar x,DVar x}" using solves_Vagree_trans by simp
from subdef have IH: "⋀ν. Uvariation ν (F(0)) (U∪{RVar x,DVar x}) ⟹ term_sem I (the (usubstappt σ (U∪{RVar x,DVar x}) θ)) ν = term_sem (adjoint σ I (F(0))) θ ν" using Uvariation_refl Uvariation_trans usubst_term by blast
have l2r: "solves_ODE I F x (the (usubstappt σ (U∪{RVar x,DVar x}) θ)) ⟹ solves_ODE (adjoint σ I ω) F x θ"
using vaflow1 subdef same_ODE_same_sol Uvariation_trans usubst_term uv
(*by (smt sup_commute sup_left_idem)*)
proof - (*sledgehammer*)
assume a1: "solves_ODE I F x (the (usubstappt σ (U ∪ {RVar x, DVar x}) θ))"
obtain rr :: "trm ⇒ interp ⇒ trm ⇒ interp ⇒ char ⇒ (real ⇒ variable ⇒ real) ⇒ variable ⇒ real" where
f2: "∀x0 x1 x2 x3 x4 x5. (∃v6. Uvariation v6 (x5 0) {RVar x4, DVar x4} ∧ term_sem x3 x2 v6 ≠ term_sem x1 x0 v6) = (Uvariation (rr x0 x1 x2 x3 x4 x5) (x5 0) {RVar x4, DVar x4} ∧ term_sem x3 x2 (rr x0 x1 x2 x3 x4 x5) ≠ term_sem x1 x0 (rr x0 x1 x2 x3 x4 x5))"
by moura
have f3: "Uvariation (F 0) ω (insert (RVar x) (U ∪ {DVar x}))"
using uv by auto
have f4: "{DVar x} ∪ {} ∪ {DVar x} = insert (DVar x) ({DVar x} ∪ {} ∪ {}) ⟶ {RVar x} ∪ {DVar x} ∪ insert (RVar x) (U ∪ {DVar x}) = insert (RVar x) (U ∪ {DVar x})"
by fastforce
{ assume "{DVar x} ∪ {} ∪ {DVar x} = insert (DVar x) ({DVar x} ∪ {} ∪ {}) ∧ Uvariation (rr (the (usubstappt σ (U ∪ {RVar x, DVar x}) θ)) I θ (USubst.adjoint σ I ω) x F) ω ({RVar x} ∪ {DVar x} ∪ insert (RVar x) (U ∪ {DVar x}))"
then have "¬ Uvariation (rr (the (usubstappt σ (U ∪ {RVar x, DVar x}) θ)) I θ (USubst.adjoint σ I ω) x F) (F 0) {RVar x, DVar x} ∨ term_sem (USubst.adjoint σ I ω) θ (rr (the (usubstappt σ (U ∪ {RVar x, DVar x}) θ)) I θ (USubst.adjoint σ I ω) x F) = term_sem I (the (usubstappt σ (U ∪ {RVar x, DVar x}) θ)) (rr (the (usubstappt σ (U ∪ {RVar x, DVar x}) θ)) I θ (USubst.adjoint σ I ω) x F)"
using f4 subdef usubst_term by auto }
then have "¬ Uvariation (rr (the (usubstappt σ (U ∪ {RVar x, DVar x}) θ)) I θ (USubst.adjoint σ I ω) x F) (F 0) {RVar x, DVar x} ∨ term_sem (USubst.adjoint σ I ω) θ (rr (the (usubstappt σ (U ∪ {RVar x, DVar x}) θ)) I θ (USubst.adjoint σ I ω) x F) = term_sem I (the (usubstappt σ (U ∪ {RVar x, DVar x}) θ)) (rr (the (usubstappt σ (U ∪ {RVar x, DVar x}) θ)) I θ (USubst.adjoint σ I ω) x F)"
using f3 by (metis (no_types) Uvariation_trans insert_is_Un)
then show ?thesis
using f2 a1 by (meson same_ODE_same_sol)
qed
have r2l: "solves_ODE (adjoint σ I ω) F x θ ⟹ solves_ODE I F x (the (usubstappt σ (U∪{RVar x,DVar x}) θ))"
using vaflow2 subdef same_ODE_same_sol Uvariation_trans usubst_term uv
(*by (smt sup_commute sup_left_idem)*)
proof - (*sledgehammer*)
assume a1: "solves_ODE (USubst.adjoint σ I ω) F x θ"
obtain rr :: "trm ⇒ interp ⇒ trm ⇒ interp ⇒ char ⇒ (real ⇒ variable ⇒ real) ⇒ variable ⇒ real" where
"∀x0 x1 x2 x3 x4 x5. (∃v6. Uvariation v6 (x5 0) {RVar x4, DVar x4} ∧ term_sem x3 x2 v6 ≠ term_sem x1 x0 v6) = (Uvariation (rr x0 x1 x2 x3 x4 x5) (x5 0) {RVar x4, DVar x4} ∧ term_sem x3 x2 (rr x0 x1 x2 x3 x4 x5) ≠ term_sem x1 x0 (rr x0 x1 x2 x3 x4 x5))"
by moura
then have f2: "∀f c i t ia ta. Uvariation (rr ta ia t i c f) (f 0) {RVar c, DVar c} ∧ term_sem i t (rr ta ia t i c f) ≠ term_sem ia ta (rr ta ia t i c f) ∨ solves_ODE i f c t = solves_ODE ia f c ta"
by (meson same_ODE_same_sol)
have f3: "Uvariation (F 0) ω ({RVar x, DVar x} ∪ U)"
using uv by force
have f4: "usubstappt σ ({RVar x, DVar x} ∪ U) θ ≠ undeft"
using subdef by auto
{ assume "Uvariation (rr θ (USubst.adjoint σ I ω) (the (usubstappt σ (U ∪ {RVar x, DVar x}) θ)) I x F) ω ({RVar x, DVar x} ∪ ({RVar x, DVar x} ∪ U))"
then have "¬ Uvariation (rr θ (USubst.adjoint σ I ω) (the (usubstappt σ (U ∪ {RVar x, DVar x}) θ)) I x F) (F 0) {RVar x, DVar x} ∨ term_sem I (the (usubstappt σ (U ∪ {RVar x, DVar x}) θ)) (rr θ (USubst.adjoint σ I ω) (the (usubstappt σ (U ∪ {RVar x, DVar x}) θ)) I x F) = term_sem (USubst.adjoint σ I ω) θ (rr θ (USubst.adjoint σ I ω) (the (usubstappt σ (U ∪ {RVar x, DVar x}) θ)) I x F)"
using f4 by (simp add: Un_commute usubst_term) }
then show ?thesis
using f3 f2 a1 by (meson Uvariation_trans)
qed
from l2r and r2l show ?thesis by auto
qed

lemma usubst_ode_ext2:
assumes subdef: "usubstappt σ (U∪{RVar x,DVar x}) θ ≠ undeft"
assumes     uv: "Uvariation (F(0)) ω (U∪{RVar x,DVar x})"
shows "solves_ODE I F x (the (usubstappt σ (U∪{RVar x,DVar x}) θ)) = solves_ODE (adjoint σ I ω) F x θ"
using usubst_ode_ext subdef uv by blast

paragraph ‹Separately Prove the Loop Case of ‹usubst_fml_game››

lemma union_comm: "A∪B=B∪A"
by auto

definition loopfpτ:: "game ⇒ interp ⇒ (state set ⇒ state set)"
where "loopfpτ α I X = lfp(λZ. X ∪ game_sem I α Z)"

lemma usubst_game_loop:
assumes  uv: "Uvariation ν ω U"
and  IHαrec: "⋀ν ω X. Uvariation ν ω (fst(usubstappp σ U α)) ⟹ snd (usubstappp σ (fst(usubstappp σ U α)) α)≠undefg ⟹
(ν ∈ game_sem I (the (snd (usubstappp σ (fst(usubstappp σ U α)) α))) X) = (ν ∈ game_sem (adjoint σ I ω) α X)"
shows "snd (usubstappp σ U (Loop α))≠undefg ⟹ (ν ∈ game_sem I (the (snd (usubstappp σ U (Loop α)))) X) = (ν ∈ game_sem (adjoint σ I ω) (Loop α) X)"
proof-
assume def: "snd (usubstappp σ U (Loop α))≠undefg"
have loopfix: "⋀α I X. loopfpτ α I X = game_sem I (Loop α) X" unfolding loopfpτ_def using game_sem_loop by metis
let ?σαloopoff = "the (snd (usubstappp σ U (Loop α)))"
let ?σα = "the (snd(usubstappp σ (fst(usubstappp σ U α)) α))"
let ?σαloop = "Loop ?σα"
have loopform: "?σαloopoff = ?σαloop" using usubstappp_loop
by (metis (mono_tags, lifting) Loopo.simps(1) def option.exhaust_sel option.inject snd_conv usubstappp_loop_conv)
let ?τ = "loopfpτ ?σαloop I"
let ?ρ = "loopfpτ α (adjoint σ I ω)"
let ?V = "fst(usubstappp σ U α)"
have fact1: "⋀V. snd(usubstappp σ V α)≠undefg ⟹  fst(usubstappp σ V α) ⊇ BVG(the (snd(usubstappp σ V α)))" using usubst_taboos by simp
have fact2: "⋀V W. snd(usubstappp σ V α)≠undefg ⟹ snd(usubstappp σ W α)≠undefg ⟹ (fst(usubstappp σ V α) ⊇ BVG(the (snd(usubstappp σ W α))))" using fact1 usubst_taboos usubstappp_det by metis
have VgeqBV: "?V ⊇ BVG(?σα)" using usubst_taboos fact2 def usubstappp_loop_conv by simp
have uvV: "Vagree ν ω (-?V)" using uv
by (metis Uvariation_Vagree Uvariation_mon double_compl usubst_taboos_mon)
have τeq: "?τ(X) = game_sem I ?σαloop X" using loopfix by auto
have ρeq: "?ρ(X) = game_sem (adjoint σ I ω) (Loop α) X"  using loopfix by auto
have τisρ: "selectlike (?τ(X)) ω (-?V)= selectlike (?ρ(X)) ω (-?V)"
proof-
let ?f = "λZ. X ∪ game_sem I ?σα Z"
let ?g = "λY. X ∪ game_sem (adjoint σ I ω) α Y"
let ?R = "λZ Y. selectlike Z ω (-?V) = selectlike Y ω (-?V)"
have "?R (lfp ?f) (lfp ?g)"
proof (induction rule: lfp_lockstep_induct[where f=‹?f› and g=‹?g› and R=‹?R›])
case monof
then show ?case using game_sem_loop_fixpoint_mono by simp
next
case monog
then show ?case using game_sem_loop_fixpoint_mono by simp
next
case (step A B)
then have IHfp: "selectlike A ω (-?V) = selectlike B ω (-?V)" by simp
show "selectlike (X ∪ game_sem I ?σα A) ω (-?V) = selectlike (X ∪ game_sem (adjoint σ I ω) α B) ω (-?V)"
proof (rule selectlike_equal_cocond_corule
(*[where ν=ω and V=‹?V› and X=‹X ∪ game_sem I ?σα A› and Y=‹X ∪ game_sem (adjoint σ I ω) α B›]*))
fix μ
assume muvar: "Uvariation μ ω ?V"
have forw: "(μ ∈ X ∪ game_sem I ?σα A) = (μ ∈ X ∪ game_sem I ?σα (selectlike A μ (-BVG(?σα))))" using boundeffect by auto

have "(μ ∈ X ∪ game_sem (adjoint σ I ω) α B) = (μ ∈ X ∪ game_sem I ?σα B)" using IHαrec[OF muvar]
using def usubstappp_loop_conv by auto
also have "... = (μ ∈ X ∪ game_sem I ?σα (selectlike B μ (-BVG(?σα))))" using boundeffect by simp
finally have backw: "(μ ∈  X ∪ game_sem (adjoint σ I ω) α B) =  (μ ∈ X ∪ game_sem I ?σα (selectlike B μ (-BVG(?σα))))" .

have samewin: "selectlike A μ (-BVG(?σα)) = selectlike B μ (-BVG(?σα))" using IHfp selectlike_antimon VgeqBV muvar Uvariation_trans selectlike_equal_cocond
(*by (smt le_iff_sup)*)
proof -
have "Vagree μ ω (- fst (usubstappp σ U α))"
by (metis Uvariation_Vagree double_complement muvar)
then have "selectlike A μ (- fst (usubstappp σ U α)) = selectlike B μ (- fst (usubstappp σ U α))"
using IHfp selectlike_Vagree by presburger
then show ?thesis
by (metis (no_types) Compl_subset_Compl_iff VgeqBV selectlike_compose sup.absorb_iff2)
qed
from forw and backw show "(μ ∈ X ∪ game_sem I ?σα A) = (μ ∈ X ∪ game_sem (adjoint σ I ω) α B)" using samewin by auto
qed

next
case (union M)
then show ?case using selectlike_Sup[where ν=ω and V=‹-?V›] fst_proj_def snd_proj_def by (simp) (blast)
qed
then show ?thesis
using τeq loopfix loopfpτ_def by auto
qed
show ?thesis using τeq ρeq τisρ similar_selectlike_mem[OF uvV] by (metis loopform)
qed

lemma usubst_fml_game:
assumes vaouter: "Uvariation ν ω U"
shows "usubstappf σ U φ≠undeff ⟹ (ν ∈ fml_sem I (the (usubstappf σ U φ))) = (ν ∈ fml_sem (adjoint σ I ω) φ)"
and "snd (usubstappp σ U α)≠undefg ⟹ (ν ∈ game_sem I (the (snd (usubstappp σ U α))) X) = (ν ∈ game_sem (adjoint σ I ω) α X)"
proof-
show "usubstappf σ U φ≠undeff ⟹ (ν ∈ fml_sem I (the (usubstappf σ U φ))) = (ν ∈ fml_sem (adjoint σ I ω) φ)"
and "snd (usubstappp σ U α)≠undefg ⟹ (ν ∈ game_sem I (the (snd (usubstappp σ U α))) X) = (ν ∈ game_sem (adjoint σ I ω) α X)" for σ φ α
using vaouter proof (induction φ and α arbitrary: ν ω and ν ω X rule: usubstappfp_induct)
case (Pred σ U p θ)
then have va: "Uvariation ν ω U" by simp
then show ?case
proof (cases "SPreds σ p")
case None
then show ?thesis using usubst_term[OF va] adjoint_preds_skip
(*by (smt Pred.prems(1) fml_sem.simps(1) mem_Collect_eq option.case_eq_if option.sel usubstappf.simps(1))*)
proof - (*sledgehammer*)
have "∀p V c t. usubstappf p V (Pred c t) = (if usubstappt p V t = undeft then undeff else case SPreds p c of None ⇒ Afml (Pred c (the (usubstappt p V t))) | Some f ⇒ if FVF f ∩ V = {} then usubstappf (dotsubstt (the (usubstappt p V t))) {} f else undeff)"
then have f1: "∀p V c t. if usubstappt p V t = undeft then usubstappf p V (Pred c t) = undeff else usubstappf p V (Pred c t) = (case SPreds p c of None ⇒ Afml (Pred c (the (usubstappt p V t))) | Some f ⇒ if FVF f ∩ V = {} then usubstappf (dotsubstt (the (usubstappt p V t))) {} f else undeff)"
by presburger
then have "usubstappt σ U θ ≠ undeft"
by (meson Pred.prems(1))
then have f2: "usubstappf σ U (Pred p θ) = Afml (Pred p (the (usubstappt σ U θ)))"
using None by force
have "usubstappt σ U θ ≠ undeft"
using f1 by (meson Pred.prems(1))
then show ?thesis
using f2 by (simp add: None ‹⋀θ σ I. usubstappt σ U θ ≠ undeft ⟹ term_sem I (the (usubstappt σ U θ)) ν = term_sem (USubst.adjoint σ I ω) θ ν› adjoint_preds_skip)
qed

next
case (Some r)
then have varcond: "FVF(r)∩U={}" using Pred usubstappf_pred usubstappf_pred2 usubstappf_pred_conv by meson
from Pred have subdef: "usubstappt σ U θ ≠ undeft" using usubstappf_pred_conv by auto
from Pred and Some
have IHsubsubst: "⋀ν ω. Uvariation ν ω {} ⟹ (ν ∈ fml_sem I (the (usubstappf (dotsubstt (the (usubstappt σ U θ))) {} r))) = (ν ∈ fml_sem (adjoint (dotsubstt (the (usubstappt σ U θ))) I ω) r)"
using subdef varcond by fastforce

let ?d = "term_sem I (the (usubstappt σ U θ)) ν"
have deq: "?d = term_sem (adjoint σ I ω) θ ν" by (rule usubst_term[OF va subdef])
let ?dotIa = "adjoint (dotsubstt (the (usubstappt σ U θ))) I ν"

from Some
have "(ν∈fml_sem I (the (usubstappf σ U (Pred p θ)))) = (ν∈fml_sem I (the (usubstappf (dotsubstt (the (usubstappt σ U θ))) {} r)))"
using subdef varcond by force
also have "... = (ν∈fml_sem ?dotIa r)" using IHsubsubst[where ν=ν and ω=ν] Uvariation_empty by auto
also have "... = (ν∈fml_sem (repc I dotid ?d) r)" using adjoint_dotsubstt[where θ=‹the (usubstappt σ U θ)› and I=I and ω=ν] by simp
also have "... = (ω∈fml_sem (repc I dotid ?d) r)" using coincidence_formula_cor[where ω=ν and ω'=ω and U=U and φ=r and I=‹repc I dotid ?d›] va varcond by simp
(*I.^dω⟦σf(⋅)⟧  also have "... = term_sem ?dotIa r ω" using coincidence_term_cor[of ν ω U r ?dotIa] uv varcond by simp*)
also have "... = (Preds (adjoint σ I ω) p)(?d)" using adjoint_preds_match Some by simp
also have "... = (Preds (adjoint σ I ω) p)(term_sem (adjoint σ I ω) θ ν)" using deq by simp
also have "... = (ν∈fml_sem (adjoint σ I ω) (Pred p θ))" by simp
finally show "(ν∈fml_sem I (the (usubstappf σ U (Pred p θ)))) = (ν∈fml_sem (adjoint σ I ω) (Pred p θ))" .
qed

next
case (Geq σ U θ η)
(* then show ?case using usubst_term usubstappf_geq usubstappf_geq_conv
by (smt fml_sem.simps(2) mem_Collect_eq option.sel)*)
then have def1: "usubstappt σ U θ ≠ undeft" using usubstappf_geq_conv by simp
moreover have def2: "usubstappt σ U η ≠ undeft" using usubstappf_geq_conv Geq.prems(1) by blast
show ?case
using usubst_term[OF ‹Uvariation ν ω U›, OF def1] usubst_term[OF ‹Uvariation ν ω U›,OF def2] usubstappf_geqr[OF ‹usubstappf σ U (Geq θ η) ≠ undeff›] by force
next
case (Not σ U φ)
then show ?case using Noto_undef by auto
next
case (And σ U φ ψ)
then show ?case using Ando_undef by auto

next
case (Exists σ U x φ)
then have IH: "⋀ν ω. Uvariation ν ω (U∪{x}) ⟹ (ν ∈ fml_sem I (the (usubstappf σ (U∪{x}) φ))) = (ν ∈ fml_sem (adjoint σ I ω) φ)" by force
from Exists have "Uvariation ν ω U" by simp
(*from Exists have subdef: "usubstappt σ (U∪{x}) θ ≠ undeft" by auto*)

then have Uvar: "⋀d. Uvariation (repv ν x d) ω (U∪{x})" using Uvariation_repv Uvariation_trans Uvariation_sym
using Exists.prems(2) Uvariation_def by auto
have "(ν∈fml_sem I (the (usubstappf σ U (Exists x φ)))) = (ν∈fml_sem I (Exists x (the (usubstappf σ (U∪{x}) φ))))"
using usubstappf_exists Exists.prems(1) by fastforce
also have "... = (∃d. (repv ν x d)∈fml_sem I (the (usubstappf σ (U∪{x}) φ)))" by simp
also have "... = (∃d. (repv ν x d)∈fml_sem (adjoint σ I ω) φ)" using IH Uvar by auto
also have "... = (ν∈fml_sem (adjoint σ I ω) (Exists x φ))" by auto
finally have "(ν∈fml_sem I (the (usubstappf σ U (Exists x φ)))) =  (ν∈fml_sem (adjoint σ I ω) (Exists x φ))" .
from this show ?case by simp

next
case (Diamond σ U α φ)
let ?V = "fst(usubstappp σ U α)"
from Diamond have IHα: "⋀X. Uvariation ν ω U ⟹ (ν ∈ game_sem I (the (snd (usubstappp σ U α))) X) = (ν ∈ game_sem (adjoint σ I ω) α X)" by fastforce
from Diamond have IHφ: "⋀ν ω. Uvariation ν ω (fst(usubstappp σ U α)) ⟹ (ν ∈ fml_sem I (the (usubstappf σ (fst(usubstappp σ U α)) φ))) = (ν ∈ fml_sem (adjoint σ I ω) φ)"
from Diamond have uv: "Uvariation ν ω U" by simp
have "(ν ∈ fml_sem I (the (usubstappf σ U (Diamond α φ)))) = (ν ∈ fml_sem I (let Vα = usubstappp σ U α in Diamond (the (snd Vα)) (the (usubstappf σ (fst Vα) φ))))"
by (metis Diamond.prems(1) Diamondo.elims option.sel usubstappf.simps(6))
also have "... = (ν ∈ fml_sem I (Diamond (the (snd(usubstappp σ U α))) (the (usubstappf σ (fst(usubstappp σ U α)) φ))))" by simp
also have "... = (ν ∈ game_sem I (the (snd(usubstappp σ U α))) (fml_sem I (the (usubstappf σ (fst(usubstappp σ U α)) φ))))" by simp
also have "... = (ν ∈ game_sem I (the (snd(usubstappp σ U α))) (selectlike (fml_sem I (the (usubstappf σ (fst(usubstappp σ U α)) φ))) ν (-BVG(the (snd(usubstappp σ U α))))))" using boundeffect by auto
finally have forw: "(ν ∈ fml_sem I (the (usubstappf σ U (Diamond α φ)))) = (ν ∈ game_sem I (the (snd(usubstappp σ U α))) (selectlike (fml_sem I (the (usubstappf σ (fst(usubstappp σ U α)) φ))) ν (-BVG(the (snd(usubstappp σ U α))))))" .

have "(ν ∈ fml_sem (adjoint σ I ω) (Diamond α φ)) = (ν ∈ game_sem (adjoint σ I ω) α (fml_sem (adjoint σ I ω) φ))" by simp
also have "... = (ν ∈ game_sem I (the (snd(usubstappp σ U α))) (fml_sem (adjoint σ I ω) φ))" using IHα uv by simp
also have "... = (ν ∈ game_sem I (the (snd(usubstappp σ U α))) (selectlike (fml_sem (adjoint σ I ω) φ) ν (-BVG(the (snd(usubstappp σ U α))))))" using boundeffect by auto
finally have backw: "(ν ∈ fml_sem (adjoint σ I ω) (Diamond α φ)) = (ν ∈ game_sem I (the (snd(usubstappp σ U α))) (selectlike (fml_sem (adjoint σ I ω) φ) ν (-BVG(the (snd(usubstappp σ U α))))))" .

have samewin: "selectlike (fml_sem I (the (usubstappf σ (fst(usubstappp σ U α)) φ))) ν (-BVG(the (snd(usubstappp σ U α)))) = selectlike (fml_sem (adjoint σ I ω) φ) ν (-BVG(the (snd(usubstappp σ U α))))"
proof (rule selectlike_equal_cocond_corule)
fix μ
assume muvar: "Uvariation μ ν (BVG(the (snd(usubstappp σ U α))))"
have Uμω: "Uvariation μ ω ?V" using muvar uv Uvariation_trans union_comm usubst_taboos Uvariation_mon
(*by (smt Diamond.prems(1) Diamondo.simps(2) usubstappf.simps(6))*)
proof-
have Uμν: "Uvariation μ ν (BVG(the (snd(usubstappp σ U α))))" by (rule muvar)
have Uνω: "Uvariation ν ω U" by (rule uv)
have "Uvariation μ ω (U ∪ BVG(the (snd(usubstappp σ U α))))" using Uvariation_trans[OF Uμν Uνω] union_comm by (rule HOL.back_subst)
thus ?thesis using usubst_taboos Uvariation_mon by (metis (mono_tags, lifting) Diamond.prems(1) Diamondo_undef Uvariation_mon usubst_taboos usubstappf.simps(6))
qed
have "(μ ∈ fml_sem (adjoint σ I ω) φ) = (μ ∈ fml_sem I (the (usubstappf σ (fst(usubstappp σ U α)) φ)))"
using muvar Uvariation_trans uv IHφ boundeffect Uvariation_mon usubst_taboos Uμω by auto
then show "(μ ∈ fml_sem I (the (usubstappf σ (fst (usubstappp σ U α)) φ))) = (μ ∈ fml_sem (adjoint σ I ω) φ)" by simp
qed
from forw and backw show "(ν ∈ fml_sem I (the (usubstappf σ U (Diamond α φ)))) = (ν ∈ fml_sem (adjoint σ I ω) (Diamond α φ))" using samewin by auto

next (* games *)

case (Game σ U a)
then show ?case using adjoint_games usubstappp_game by (cases "SGames σ a") auto

next
case (Assign σ U x θ)
then show ?case using usubst_term Assigno_undef
(*by (smt Assigno.elims game_sem.simps(2) mem_Collect_eq option.sel snd_pair usubstappp.simps(2))*)
proof - (*sledgehammer*)
have f1: "usubstappt σ U θ ≠ undeft"
using Assign.prems(1) Assigno_undef by auto
{ assume "repv ν x (term_sem (USubst.adjoint σ I ω) θ ν) ∈ X"
then have "repv ν x (term_sem I (the (usubstappt σ U θ)) ν) ∈ X"
using f1 Assign.prems(2) usubst_term by auto
then have "repv ν x (term_sem (USubst.adjoint σ I ω) θ ν) ∈ X ⟶ (ν ∈ game_sem I (the (snd (usubstappp σ U (x := θ)))) X) = (ν ∈ game_sem (USubst.adjoint σ I ω) (x := θ) X)"
using f1 by force }
moreover
{ assume "repv ν x (term_sem (USubst.adjoint σ I ω) θ ν) ∉ X"
then have "repv ν x (term_sem I (the (usubstappt σ U θ)) ν) ∉ X ∧ repv ν x (term_sem (USubst.adjoint σ I ω) θ ν) ∉ X"
using f1 Assign.prems(2) usubst_term by presburger
then have ?thesis
using f1 by force }
ultimately show ?thesis
by fastforce
qed

next
case (Test σ U φ)
then show ?case using Testo_undef by auto

next
case (Choice σ U α β)
from Choice have IHα: "⋀X. Uvariation ν ω U ⟹ (ν ∈ game_sem I (the (snd (usubstappp σ U α))) X) = (ν ∈ game_sem (adjoint σ I ω) α X)" by (simp add: Choiceo_undef)
from Choice have IHβ: "⋀X. Uvariation ν ω U ⟹ (ν ∈ game_sem I (the (snd (usubstappp σ U β))) X) = (ν ∈ game_sem (adjoint σ I ω) β X)" by (simp add: Choiceo_undef)
from Choice have uv: "Uvariation ν ω U" by simp
show ?case using IHα IHβ uv
(*by (smt Choice.prems(1) Choiceo.elims game_sem.simps(4) option.sel snd_pair union_or usubstappp_choice) *)
proof -
have f1: "Agame (the (snd (usubstappp σ U α))) = snd (usubstappp σ U α)"
by (meson Choice(3) option.collapse usubstappp_choice_conv)
have "Agame (the (snd (usubstappp σ U β))) = snd (usubstappp σ U β)"
by (meson Choice(3) option.collapse usubstappp_choice_conv)
then have "snd (usubstappp σ U (α ∪∪ β)) = Agame (the (snd (usubstappp σ U α)) ∪∪ the (snd (usubstappp σ U β)))"
using f1 by (metis Choiceo.simps(1) snd_conv usubstappp.simps(4))
then have f2: "game_sem I (the (snd (usubstappp σ U α))) X ∪ game_sem I (the (snd (usubstappp σ U β))) X = game_sem I (the (snd (usubstappp σ U (α ∪∪ β)))) X"
by simp
moreover
{ assume "ν ∉ game_sem I (the (snd (usubstappp σ U β))) X"
have "(ν ∉ game_sem I (the (snd (usubstappp σ U (α ∪∪ β)))) X) = (ν ∈ game_sem (adjoint σ I ω) (α ∪∪ β) X) ⟶ ν ∉ game_sem I (the (snd (usubstappp σ U β))) X ∧ ν ∉ game_sem (adjoint σ I ω) (α ∪∪ β) X"
using f2 Choice(4) IHα IHβ by auto
then have "(ν ∉ game_sem I (the (snd (usubstappp σ U (α ∪∪ β)))) X) ≠ (ν ∈ game_sem (adjoint σ I ω) (α ∪∪ β) X)"
using f2 Choice(4) IHα by auto }
ultimately show ?thesis
using Choice(4) IHβ by auto
qed

next
case (Compose σ U α β)
let ?V = "fst(usubstappp σ U α)"
from Compose have IHα: "⋀X. Uvariation ν ω U ⟹ (ν ∈ game_sem I (the (snd (usubstappp σ U α))) X) = (ν ∈ game_sem (adjoint σ I ω) α X)" by (simp add: Composeo_undef)
from Compose have IHβ: "⋀ν ω X. Uvariation ν ω ?V ⟹ (ν ∈ game_sem I (the (snd (usubstappp σ ?V β))) X) = (ν ∈ game_sem (adjoint σ I ω) β X)" by (simp add: Composeo_undef)
from Compose have uv: "Uvariation ν ω U" by simp
have "(ν ∈ game_sem I (the (snd (usubstappp σ U (Compose α β)))) X) = (ν ∈ game_sem I (Compose (the (snd(usubstappp σ U α))) (the (snd(usubstappp σ ?V β)))) X)"
by (metis (no_types, lifting) Compose.prems(1) Composeo.elims option.sel snd_pair usubstappp.simps(5))
also have "... = (ν ∈ game_sem I (the (snd(usubstappp σ U α))) (game_sem I (the (snd(usubstappp σ ?V β))) X))" by simp
also have "... = (ν ∈ game_sem I (the (snd(usubstappp σ U α))) (selectlike (game_sem I (the (snd(usubstappp σ ?V β))) X) ν (-BVG(the(snd(usubstappp σ U α))))))" using boundeffect by auto
finally have forw: "(ν ∈ game_sem I (the (snd (usubstappp σ U (Compose α β)))) X) = (ν ∈ game_sem I (the (snd(usubstappp σ U α))) (selectlike (game_sem I (the (snd(usubstappp σ ?V β))) X) ν (-BVG(the(snd(usubstappp σ U α))))))" .

have "(ν ∈ game_sem (adjoint σ I ω) (Compose α β) X) = (ν ∈ game_sem (adjoint σ I ω) α ((game_sem (adjoint σ I ω) β) X))" by simp
also have "... = (ν ∈ game_sem I (the (snd(usubstappp σ U α))) ((game_sem (adjoint σ I ω) β) X))" using IHα[OF uv] by auto
also have "... = (ν ∈ game_sem I (the (snd(usubstappp σ U α))) (selectlike ((game_sem (adjoint σ I ω) β) X) ν (-BVG(the(snd(usubstappp σ U α))))))" using boundeffect by auto
finally have backw: "(ν ∈ game_sem (adjoint σ I ω) (Compose α β) X) = (ν ∈ game_sem I (the (snd(usubstappp σ U α))) (selectlike ((game_sem (adjoint σ I ω) β) X) ν (-BVG(the(snd(usubstappp σ U α))))))" .

have samewin: "selectlike (game_sem I (the (snd(usubstappp σ ?V β))) X) ν (-BVG(the(snd(usubstappp σ U α)))) = selectlike ((game_sem (adjoint σ I ω) β) X) ν (-BVG(the(snd(usubstappp σ U α))))"
proof (rule selectlike_equal_cocond_corule)
fix μ
assume muvar: "Uvariation μ ν (BVG(the(snd(usubstappp σ U α))))"
have Uμω: "Uvariation μ ω ?V" using muvar uv Uvariation_trans union_comm usubst_taboos Uvariation_mon
(*by (smt Compose.prems(1) Composeo_undef snd_pair usubstappp.simps(5))*)
proof -
have "Uvariation μ ω (BVG (the (snd (usubstappp σ U α))) ∪ U)" by (meson Uvariation_trans muvar uv)
then show ?thesis using Uvariation_mon union_comm usubst_taboos
by (metis (no_types, lifting) Compose.prems(1) Composeo_undef Pair_inject prod.collapse usubstappp_compose)
(*by (metis (no_types) Uvariation_mon union_comm usubst_taboos)*)
qed
have "(μ ∈ game_sem I (the(snd(usubstappp σ ?V β))) X) = (μ ∈ game_sem (adjoint σ I ω) β X)"
using muvar Uvariation_trans uv IHβ boundeffect Uvariation_mon usubst_taboos Uμω by auto
then show "(μ ∈ game_sem I (the(snd(usubstappp σ ?V β))) X) = (μ ∈ game_sem (adjoint σ I ω) β X)" by simp
qed
from forw and backw show "(ν ∈ game_sem I (the(snd (usubstappp σ U (Compose α β)))) X) = (ν ∈ game_sem (adjoint σ I ω) (Compose α β) X)" using samewin by auto

next
case (Loop σ U α)
let ?V = "fst(usubstappp σ U α)"
from Loop have selfdef: "snd (usubstappp σ U (Loop α)) ≠ undefg" by auto
from Loop have IHαrec: "⋀ν ω X. Uvariation ν ω ?V ⟹ (ν ∈ game_sem I (the (snd (usubstappp σ ?V α))) X) = (ν ∈ game_sem (adjoint σ I ω) α X)" by fastforce
from Loop have uv: "Uvariation ν ω U" by simp
show "(ν ∈ game_sem I (the (snd (usubstappp σ U (Loop α)))) X) = (ν ∈ game_sem (adjoint σ I ω) (Loop α) X)"
using usubst_game_loop IHαrec Loop.prems(2) selfdef by blast
(*by (rule usubst_game_loop[OF uv (*IHα*) IHαrec])*)

next
case (Dual σ U α)
from Dual have IHα: "⋀X. Uvariation ν ω U ⟹ (ν ∈ game_sem I (the (snd (usubstappp σ U α))) X) = (ν ∈ game_sem (adjoint σ I ω) α X)" by force
from Dual have uv: "Uvariation ν ω U" by simp
from Dual have def: "snd (usubstappp σ U (α^d)) ≠ undefg" by simp
(*show ?case using IHα[OF uv]
by (smt Compl_iff Dual.prems(1) Dualo.elims game_sem.simps(7) option.sel snd_pair usubstappp.simps(7))*)
have "(ν ∈ -game_sem I (the (snd (usubstappp σ U α))) (-X)) = (ν ∈ -game_sem (adjoint σ I ω) α (-X))" using IHα[OF uv] by simp
then have "(ν ∈ game_sem I ((the (snd (usubstappp σ U α)))^d) X) = (ν ∈ game_sem (adjoint σ I ω) (α^d) X)" using game_sem.simps(7) by auto
then show ?case using usubstappp_dual Dualo_undef
proof -
have "⋀σ V α. snd (usubstappp σ U (α^d)) = Dualo (snd (usubstappp σ U α))"  by simp
then have "snd (usubstappp σ U α) ≠ undefg" using Dualo_undef def by presburger
then show ?thesis
using ‹(ν ∈ game_sem I ((the (snd (usubstappp σ U α)))^d) X) = (ν ∈ game_sem (USubst.adjoint σ I ω) (α^d) X)› by force
qed

next
case (ODE σ U x θ)
then have va: "Uvariation ν ω U" by simp
from ODE have subdef: "usubstappt σ (U∪{RVar x,DVar x}) θ ≠ undeft" by (simp add: ODEo_undef)
from ODE have IH: "term_sem I (the (usubstappt σ (U∪{RVar x,DVar x}) θ)) ν = term_sem (adjoint σ I ω) θ ν" using va
by (metis ODEo_undef fst_pair snd_conv usubst_taboos_mon usubst_term usubstappp.simps(8) usubstappt_antimon)
have "(ν ∈ game_sem I (the (snd (usubstappp σ U (ODE x θ)))) X) = (ν ∈ game_sem I (the (ODEo x (usubstappt σ (U∪{RVar x,DVar x}) θ))) X)" by simp
also have "... = (ν ∈ game_sem I (ODE x (the (usubstappt σ (U∪{RVar x,DVar x}) θ))) X)" using subdef by force
also have "... = (∃F T. Vagree ν (F(0)) (-{DVar x}) ∧ F(T) ∈ X ∧ solves_ODE I F x (the (usubstappt σ (U∪{RVar x,DVar x}) θ)))" by simp
also have "... = (∃F T. Uvariation ν (F(0)) {DVar x} ∧ F(T) ∈ X ∧ solves_ODE I F x (the (usubstappt σ (U∪{RVar x,DVar x}) θ)))" using Uvariation_Vagree by (metis double_compl)
also have "... = (∃F T. Uvariation ν (F(0)) {DVar x} ∧ F(T) ∈ X ∧ solves_ODE (adjoint σ I ω) F x θ)"
using usubst_ode_ext2[OF subdef] va solves_Vagree_trans Uvariation_trans Uvariation_sym_rel Uvariation_mon by (meson subset_insertI)
also have "... = (∃F T. Vagree ν (F(0)) (-{DVar x}) ∧ F(T) ∈ X ∧ solves_ODE (adjoint σ I ω) F x θ)" using Uvariation_Vagree by (metis double_compl)
also have "... = (ν ∈ game_sem (adjoint σ I ω) (ODE x θ) X)" using solves_ODE_def by simp
finally show "(ν ∈ game_sem I (the (snd (usubstappp σ U (ODE x θ)))) X) = (ν ∈ game_sem (adjoint σ I ω) (ODE x θ) X)" .
qed
qed

text ‹Lemma 16 of 🌐‹http://arxiv.org/abs/1902.07230››
theorem usubst_fml: "Uvariation ν ω U ⟹ usubstappf σ U φ ≠ undeff ⟹
(ν ∈ fml_sem I (the (usubstappf σ U φ))) = (ν ∈ fml_sem (adjoint σ I ω) φ)"
using usubst_fml_game by simp

text ‹Lemma 17 of 🌐‹http://arxiv.org/abs/1902.07230››
theorem usubst_game: "Uvariation ν ω U ⟹ snd (usubstappp σ U α) ≠ undefg ⟹
(ν ∈ game_sem I (the (snd (usubstappp σ U α))) X) = (ν ∈ game_sem (adjoint σ I ω) α X)"
using usubst_fml_game by simp

subsection ‹Soundness of Uniform Substitution of Formulas›

abbreviation usubsta:: "usubst ⇒ fml ⇒ fmlo"
where "usubsta σ φ ≡ usubstappf σ {} φ"

text ‹Theorem 18 of 🌐‹http://arxiv.org/abs/1902.07230››
theorem usubst_sound: "usubsta σ φ ≠ undeff ⟹ valid φ ⟹ valid (the (usubsta σ φ))"
proof-
assume def: "usubsta σ φ ≠ undeff"
assume prem: "valid φ"
from prem have premc: "⋀I ω. ω ∈ fml_sem I φ" using valid_def by auto
show "valid (the (usubsta σ φ))" unfolding valid_def
proof (clarify)
fix I ω
have "(ω ∈ fml_sem I (the (usubsta σ φ))) = (ω ∈ fml_sem (adjoint σ I ω) φ)" using usubst_fml by (simp add: usubst_fml def)
also have "... = True" using premc by simp
finally have "(ω ∈ fml_sem I (the (usubsta σ φ))) = True" .
from this show "ω ∈ fml_sem I (the (usubstappf σ {} φ))" by simp
qed
qed

subsection ‹Soundness of Uniform Substitution of Rules›

text ‹Uniform Substitution applied to a rule or inference›
definition usubstr:: "usubst ⇒ inference ⇒ inference option"
where "usubstr σ R ≡ if (usubstappf σ allvars (snd R) ≠ undeff ∧ (∀φ∈set (fst R). usubstappf σ allvars φ ≠ undeff)) then
Some(map(the o (usubstappf σ allvars))(fst R), the (usubstappf σ allvars (snd R)))
else
None"

text ‹Simple observations about applying uniform substitutions to a rule›

lemma usubstr_conv: "usubstr σ R ≠ None ⟹
usubstappf σ allvars (snd R) ≠ undeff ∧
(∀φ∈set (fst R). usubstappf σ allvars φ ≠ undeff)"
by (metis usubstr_def)

lemma usubstr_union_undef: "(usubstr σ ((append A B), C) ≠ None) = (usubstr σ (A, C) ≠ None ∧ usubstr σ (B, C) ≠ None)"
using usubstr_def by auto
lemma usubstr_union_undef2: "(usubstr σ ((append A B), C) ≠ None) ⟹ (usubstr σ (A, C) ≠ None ∧ usubstr σ (B, C) ≠ None)"
using usubstr_union_undef by blast

lemma usubstr_cons_undef: "(usubstr σ ((Cons A B), C) ≠ None) = (usubstr σ ([A], C) ≠ None ∧ usubstr σ (B, C) ≠ None)"
using usubstr_def by auto
lemma usubstr_cons_undef2: "(usubstr σ ((Cons A B), C) ≠ None) ⟹ (usubstr σ ([A], C) ≠ None ∧ usubstr σ (B, C) ≠ None)"
using usubstr_cons_undef by blast

lemma usubstr_cons: "(usubstr σ ((Cons A B), C) ≠ None) ⟹
the (usubstr σ ((Cons A B), C)) = (Cons (the (usubstappf σ allvars A)) (fst (the (usubstr σ (B, C)))), snd (the (usubstr σ ([A], C))))"
using usubstr_union_undef map_cons usubstr_def
proof-
assume def: "(usubstr σ ((Cons A B), C) ≠ None)"
let ?R = "((Cons A B), C)"
have "the (usubstr σ ?R) = (map(the o (usubstappf σ allvars))(fst ?R) , the (usubstappf σ allvars (snd ?R)))" using def usubstr_def by (metis option.sel)
also have "... = (Cons (the (usubstappf σ allvars A)) (map(the o (usubstappf σ allvars))(B)) , the (usubstappf σ allvars (snd ?R)))" using map_cons by auto
also have "... = (Cons (the (usubstappf σ allvars A)) (fst (the (usubstr σ (B, C)))) , the (usubstappf σ allvars (snd ?R)))" using usubstr_cons_undef2[OF def] usubstr_def by (metis (no_types, lifting) fst_conv option.sel)
also have "... = (Cons (the (usubstappf σ allvars A)) (fst (the (usubstr σ (B, C)))) , snd (the (usubstr σ ([A], C))))" using def usubstr_def by auto
ultimately show "the (usubstr σ ((Cons A B), C)) = (Cons (the (usubstappf σ allvars A)) (fst (the (usubstr σ (B, C)))) , snd (the (usubstr σ ([A], C))))" by simp
qed

lemma usubstr_union: "(usubstr σ ((append A B), C) ≠ None) ⟹
the (usubstr σ ((append A B), C)) = (append (fst (the (usubstr σ (A, C)))) (fst (the (usubstr σ (B, C)))), snd (the (usubstr σ (A, C))))"
using usubstr_union_undef2
(*by (smt fst_pair map_append option.sel snd_pair usubstr_def)*)
proof-
assume def: "(usubstr σ ((append A B), C) ≠ None)"
let ?R = "((append A B), C)"
have "the (usubstr σ ?R) = (map(the o (usubstappf σ allvars))(fst ?R) , the (usubstappf σ allvars (snd ?R)))" using def usubstr_def by (metis option.sel)
also have "... = (map(the o (usubstappf σ allvars))(fst ?R) , snd (the (usubstr σ (A, C))))" using usubstr_union_undef2[OF def] usubstr_def by (metis option.sel sndI)
also have "... = (append (map(the o (usubstappf σ allvars))(A)) (map(the o (usubstappf σ allvars))(B)) , snd (the (usubstr σ (A, C))))" using usubstr_union_undef2[OF def] map_append by simp
also have "... = (append (fst (the (usubstr σ (A, C)))) (fst (the (usubstr σ (B, C)))), snd (the (usubstr σ (A, C))))" using usubstr_union_undef2[OF def] usubstr_def by (metis (no_types, lifting) fst_conv option.sel)
ultimately show "the (usubstr σ ((append A B), C)) = (append (fst (the (usubstr σ (A, C)))) (fst (the (usubstr σ (B, C)))), snd (the (usubstr σ (A, C))))" by simp
qed

lemma usubstr_length: "usubstr σ R ≠ None ⟹ length (fst (the (usubstr σ R))) = length (fst R)"
by (metis fst_pair length_map option.sel usubstr_def)

lemma usubstr_nth: "usubstr σ R ≠ None ⟹ 0≤k ⟹ k<length (fst R) ⟹
nth (fst (the (usubstr σ R))) k = the (usubstappf σ allvars (nth (fst R) k))"
(*unfolding usubstr_def using usubstr_length
by (smt comp_apply fst_pair nth_map option.sel)*)
proof-
assume a1: "usubstr σ R ≠ None"
assume a2: "0≤k"
assume a3: "k<length (fst R)"
show "nth (fst (the (usubstr σ R))) k = the (usubstappf σ allvars (nth (fst R) k))"
using a1 a2 a3 proof (induction R arbitrary: k)
case (Pair A C)
then show ?case
proof (induction A arbitrary: k)
case Nil
then show ?case by simp
next
case (Cons D E)
then have IH: "⋀k. usubstr σ (E, C) ≠ None ⟹ 0 ≤ k ⟹ k < length E ⟹ nth (fst (the (usubstr σ (E, C)))) k = the (usubstappf σ allvars (nth E k))" by simp
then show ?case
proof (cases k)
case 0
then show ?thesis using Cons usubstr_cons by simp
next
case (Suc n)
then have smaller: "n<length E" using Cons.prems(3) by auto
have nati: "0≤n" by simp
have def: "usubstr σ (E, C) ≠ None" using usubstr_cons_undef2[OF Cons.prems(1)] by blast
have "nth (fst (the (usubstr σ (E, C)))) n = the (usubstappf σ allvars (nth (fst (E,C)) n))" using IH[OF def, OF nati, OF smaller] by simp
then show ?thesis using Cons usubstr_cons by (simp add: Suc)
qed
qed
qed
qed

text ‹Theorem 19 of 🌐‹http://arxiv.org/abs/1902.07230››

theorem usubst_rule_sound: "usubstr σ R ≠ None ⟹ locally_sound R ⟹ locally_sound (the (usubstr σ R))"
proof-
assume def: "usubstr σ R ≠ None"
assume prem: "locally_sound R"
let ?σD = "usubstr σ R"
fix ω
from usubst_fml have substeq: "⋀I ν φ. usubstappf σ allvars φ ≠ undeff ⟹ (ν ∈ fml_sem I (the (usubstappf σ allvars φ))) = (ν ∈ fml_sem (adjoint σ I ω) φ)" using Uvariation_univ by blast
then have substval: "⋀I. usubstappf σ allvars φ ≠ undeff ⟹ valid_in I (the (usubstappf σ allvars φ)) = valid_in (adjoint σ I ω) φ" unfolding valid_in_def by auto
show "locally_sound (the (usubstr σ R))" unfolding locally_sound_def
proof (clarify)
fix I
assume "∀k≥0. k < length (fst (the (usubstr σ R))) ⟶ valid_in I (nth (fst (the (usubstr σ R))) k)"
then have "∀k≥0. k < length (fst R) ⟶ valid_in (adjoint σ I ω) (nth (fst R) k)" using substval usubstr_nth usubstr_length substeq valid_in_def by (metis def nth_mem usubstr_def)
then have "valid_in (adjoint σ I ω) (snd R)" using prem unfolding locally_sound_def by simp
from this show "valid_in I (snd (the (usubstr σ R)))" using usubst_fml substeq usubstr_def valid_in_def by (metis def option.sel snd_conv)
qed
qed

end
```