Theory USubst

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 θ]")
  (auto simp add: usubstsize_def dotsubstt_def)
  
(* 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 α)]") 
  (auto simp add: usubstsize_def dotsubstt_def)

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"
  by (auto simp add: usappconst_def)

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"
  by (simp add: Pluso_undef)
  
lemma usubstappt_times_conv: "usubstappt σ U (Times θ η) ≠ undeft ⟹
  usubstappt σ U θ ≠ undeft ∧ usubstappt σ U η ≠ undeft"
  by (simp add: Timeso_undef)

lemma usubstappt_differential_conv: "usubstappt σ U (Differential θ) ≠ undeft ⟹
  usubstappt σ allvars θ ≠ undeft"
  by (simp add: Differentialo_undef)
  

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"
  by (simp add: Geqo_undef) 

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"
  by (simp add: Choiceo_undef)

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)"
      by (simp add: usappconst_def)
    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"
      by (simp add: usappconst_def)
    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)"
        by (simp add: usappconst_def)
      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)"
    by (simp add: option.case_eq_if)
    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)"
    by (simp add: option.case_eq_if)
    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)"
      by (simp add: usappconst_def)
    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)"
        by (simp add: usappconst_def)
      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)"
      by (simp add: option.case_eq_if)
      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)"
      by (simp add: option.case_eq_if)
      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 auto
      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, opaque_lifting) 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



subsection ‹Substitution Adjoints›

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))
  )"


paragraph ‹Simple Observations about Adjoints›
  
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 ω)"
  unfolding adjoint_def by auto

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

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

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)"
  unfolding adjoint_def by auto

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

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

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

lemma adjoint_dotsubstt: "adjoint (dotsubstt θ) I ω = repc I dotid (term_sem I θ ω)"
  (*unfolding adjoint_def dotsubstt_def adjoint_consts adjoint_funcs_skip adjoint_preds adjoint_games*)
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
      then show ?thesis using adjoint_consts by (simp add: usappconst_def)
    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
        by (simp add: FuncMatch.IH(1) usubstappt_func_conv)
      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)"
          by (simp add: option.case_eq_if)
        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 ω) φ)"
      by (simp add: Diamondo_undef) 
    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