# Theory Coincidence

theory Coincidence
imports Lib Static_Semantics
```theory "Coincidence"
imports
"Lib"
"Syntax"
"Denotational_Semantics"
"Static_Semantics"
"HOL.Finite_Set"
begin
section ‹Static Semantics Properties›

subsection Auxiliaries

text ‹The state interpolating ‹stateinterpol ν ω S› between ‹ν› and ‹ω› that is ‹ν› on ‹S› and ‹ω› elsewhere›

definition stateinterpol:: "state ⇒ state ⇒ variable set ⇒ state"
where
"stateinterpol ν ω S = (λx. if (x∈S) then ν(x) else ω(x))"

definition statediff:: "state ⇒ state ⇒ variable set"
where "statediff ν ω = {x. ν(x)≠ω(x)}"

lemma nostatediff: "x∉statediff ν ω ⟹ ν(x)=ω(x)"

lemma stateinterpol_empty: "stateinterpol ν ω {} = ω"
proof
fix x
have empty: "⋀x. ¬(x∈{})" by auto
show "⋀x. stateinterpol ν ω {} x = ω x" using empty by (simp add: stateinterpol_def)
qed

lemma stateinterpol_left [simp]: "x∈S ⟹ (stateinterpol ν ω S)(x)=ν(x)"

lemma stateinterpol_right [simp]: "x∉S ⟹ (stateinterpol ν ω S)(x)=ω(x)"

lemma Vagree_stateinterpol [simp]: "Vagree (stateinterpol ν ω S) ν S"
and "Vagree (stateinterpol ν ω S) ω (-S)"
unfolding Vagree_def by auto

lemma Vagree_ror: "Vagree ν ν' (V∩W) ⟹ (∃ω. (Vagree ν ω V ∧ Vagree ω ν' W))"
proof -
assume "Vagree ν ν' (V∩W)"
hence "∀x. x∈V∩W ⟶ ν(x)=ν'(x)" by (simp add: Vagree_def)
let ?w="stateinterpol ν ν' V"
have l: "Vagree ν ?w V" by (simp add: Vagree_def)
have r: "Vagree ?w ν' W ∧ Vagree ?w ν' W" by (simp add: Vagree_def stateinterpol_def ‹∀x. x∈V∩W ⟶ ν x = ν' x›)
have "Vagree ν ?w V ∧ Vagree ?w ν' W" using l and r by blast
thus ?thesis by auto
qed

text ‹Remark 8 🌐‹https://doi.org/10.1007/978-3-319-94205-6_15› about simple properties of projections›

lemma restrictto_extends [simp]: "restrictto X V ⊇ X"

lemma restrictto_compose [simp]: "restrictto (restrictto X V) W = restrictto X (V∩W)"
proof
show "restrictto (restrictto X V) W ⊆ restrictto X (V∩W)"
by (auto simp add: restrictto_def Vagree_def)
next
show "restrictto X (V∩W) ⊆ restrictto (restrictto X V) W"
(*by (smt Vagree_ror mem_Collect_eq restrictto_def subsetI)*)
proof - (* sledgehammer *)
obtain rr :: "(variable ⇒ real) set ⇒ (variable ⇒ real) set ⇒ variable ⇒ real" where
"∀x0 x1. (∃v2. v2 ∈ x1 ∧ v2 ∉ x0) = (rr x0 x1 ∈ x1 ∧ rr x0 x1 ∉ x0)"
by moura
then have f1: "∀F Fa. rr Fa F ∈ F ∧ rr Fa F ∉ Fa ∨ F ⊆ Fa"
by (meson subsetI)
obtain rra :: "(variable ⇒ real) ⇒ variable set ⇒ (variable ⇒ real) set ⇒ variable ⇒ real" where
"∀x0 x1 x2. (∃v3. v3 ∈ x2 ∧ Vagree v3 x0 x1) = (rra x0 x1 x2 ∈ x2 ∧ Vagree (rra x0 x1 x2) x0 x1)"
by moura
then have f2: "∀F V f. (f ∉ {f. ∃fa. fa ∈ F ∧ Vagree fa f V} ∨ rra f V F ∈ F ∧ Vagree (rra f V F) f V) ∧ (f ∈ {f. ∃fa. fa ∈ F ∧ Vagree fa f V} ∨ (∀fa. fa ∉ F ∨ ¬ Vagree fa f V))"
by blast
moreover
{ assume "∃f. f ∈ X ∧ Vagree f (v4_1 W V (rr {f. ∃fa. fa ∈ {f. ∃fa. fa ∈ X ∧ Vagree fa f V} ∧ Vagree fa f W} {f. ∃fa. fa ∈ X ∧ Vagree fa f (V ∩ W)}) (rra (rr {f. ∃fa. fa ∈ {f. ∃fa. fa ∈ X ∧ Vagree fa f V} ∧ Vagree fa f W} {f. ∃fa. fa ∈ X ∧ Vagree fa f (V ∩ W)}) (V ∩ W) X)) V"
moreover
{ assume "∃f. f ∈ {f. ∃fa. fa ∈ X ∧ Vagree fa f V} ∧ Vagree f (rr {f. ∃fa. fa ∈ {f. ∃fa. fa ∈ X ∧ Vagree fa f V} ∧ Vagree fa f W} {f. ∃fa. fa ∈ X ∧ Vagree fa f (V ∩ W)}) W"
then have "rr {f. ∃fa. fa ∈ {f. ∃fa. fa ∈ X ∧ Vagree fa f V} ∧ Vagree fa f W} {f. ∃fa. fa ∈ X ∧ Vagree fa f (V ∩ W)} ∉ {f. ∃fa. fa ∈ X ∧ Vagree fa f (V ∩ W)} ∨ rr {f. ∃fa. fa ∈ {f. ∃fa. fa ∈ X ∧ Vagree fa f V} ∧ Vagree fa f W} {f. ∃fa. fa ∈ X ∧ Vagree fa f (V ∩ W)} ∈ {f. ∃fa. fa ∈ {f. ∃fa. fa ∈ X ∧ Vagree fa f V} ∧ Vagree fa f W}"
by blast
then have "{f. ∃fa. fa ∈ X ∧ Vagree fa f (V ∩ W)} ⊆ {f. ∃fa. fa ∈ {f. ∃fa. fa ∈ X ∧ Vagree fa f V} ∧ Vagree fa f W}"
using f1 by meson }
ultimately have "(¬ Vagree (rra (rr {f. ∃fa. fa ∈ {f. ∃fa. fa ∈ X ∧ Vagree fa f V} ∧ Vagree fa f W} {f. ∃fa. fa ∈ X ∧ Vagree fa f (V ∩ W)}) (V ∩ W) X) (v4_1 W V (rr {f. ∃fa. fa ∈ {f. ∃fa. fa ∈ X ∧ Vagree fa f V} ∧ Vagree fa f W} {f. ∃fa. fa ∈ X ∧ Vagree fa f (V ∩ W)}) (rra (rr {f. ∃fa. fa ∈ {f. ∃fa. fa ∈ X ∧ Vagree fa f V} ∧ Vagree fa f W} {f. ∃fa. fa ∈ X ∧ Vagree fa f (V ∩ W)}) (V ∩ W) X)) V ∨ ¬ Vagree (v4_1 W V (rr {f. ∃fa. fa ∈ {f. ∃fa. fa ∈ X ∧ Vagree fa f V} ∧ Vagree fa f W} {f. ∃fa. fa ∈ X ∧ Vagree fa f (V ∩ W)}) (rra (rr {f. ∃fa. fa ∈ {f. ∃fa. fa ∈ X ∧ Vagree fa f V} ∧ Vagree fa f W} {f. ∃fa. fa ∈ X ∧ Vagree fa f (V ∩ W)}) (V ∩ W) X)) (rr {f. ∃fa. fa ∈ {f. ∃fa. fa ∈ X ∧ Vagree fa f V} ∧ Vagree fa f W} {f. ∃fa. fa ∈ X ∧ Vagree fa f (V ∩ W)}) W) ∨ {f. ∃fa. fa ∈ X ∧ Vagree fa f (V ∩ W)} ⊆ {f. ∃fa. fa ∈ {f. ∃fa. fa ∈ X ∧ Vagree fa f V} ∧ Vagree fa f W}"
using f2 by meson }
ultimately have "{f. ∃fa. fa ∈ X ∧ Vagree fa f (V ∩ W)} ⊆ {f. ∃fa. fa ∈ {f. ∃fa. fa ∈ X ∧ Vagree fa f V} ∧ Vagree fa f W}"
using f1 by (meson Vagree_ror)
then show ?thesis
using restrictto_def by presburger
qed
qed

lemma restrictto_antimon [simp]: "W⊇V ⟹ restrictto X W ⊆ restrictto X V"
proof -
assume "W⊇V"
then have "∃U. V=W∩U" by auto
then obtain U where "V=W∩U" by auto
hence "restrictto X V = restrictto (restrictto X W) U" by simp
hence "restrictto X V ⊇ restrictto X W" using restrictto_extends by blast
thus ?thesis by auto
qed

lemma restrictto_empty [simp]: "X≠{} ⟹ restrictto X {} = worlds"
by (auto simp add: restrictto_def worlds_def)

lemma selectlike_shrinks [simp]: "selectlike X ν V ⊆ X"

lemma selectlike_compose [simp]: "selectlike (selectlike X ν V) ν W = selectlike X ν (V∪W)"

lemma selectlike_antimon [simp]: "W⊇V ⟹ selectlike X ν W ⊆ selectlike X ν V"

lemma selectlike_empty [simp]: "selectlike X ν {} = X"

lemma selectlike_self [simp]: "(ν ∈ selectlike X ν V) = (ν∈X)"

lemma selectlike_complement [simp]: "selectlike (-X) ν V ⊆ -selectlike X ν V"

lemma selectlike_union: "selectlike (X∪Y) ν V = selectlike X ν V ∪ selectlike Y ν V"

lemma selectlike_Sup: "selectlike (Sup M) ν V = Sup {selectlike X ν V | X. X∈M}"
using selectlike_def by auto

lemma selectlike_equal_cond: "(selectlike X ν V = selectlike Y ν V) = (∀μ. Uvariation μ ν (-V) ⟶ (μ∈X) = (μ∈Y))"
unfolding selectlike_def using Uvariation_Vagree by auto

lemma selectlike_equal_cocond: "(selectlike X ν (-V) = selectlike Y ν (-V)) = (∀μ. Uvariation μ ν V ⟶ (μ∈X) = (μ∈Y))"
using selectlike_equal_cond[where V=‹-V›] by simp

lemma selectlike_equal_cocond_rule: "(⋀μ. Uvariation μ ν (-V) ⟹ (μ∈X) = (μ∈Y))
⟹ (selectlike X ν V = selectlike Y ν V)"
using selectlike_equal_cond[where V=‹V›] by simp

lemma selectlike_equal_cocond_corule: "(⋀μ. Uvariation μ ν V ⟹ (μ∈X) = (μ∈Y))
⟹ (selectlike X ν (-V) = selectlike Y ν (-V))"
using selectlike_equal_cond[where V=‹-V›] by simp

lemma co_selectlike: "-(selectlike X ν V) = (-X) ∪ {ω. ¬Vagree ω ν V}"
unfolding selectlike_def by auto

lemma selectlike_co_selectlike: "selectlike (-(selectlike X ν V)) ν V = selectlike (-X) ν V"
unfolding selectlike_def by auto

lemma selectlike_Vagree: "Vagree ν ω V ⟹ selectlike X ν V = selectlike X ω V"
using Vagree_def selectlike_def by auto

lemma similar_selectlike_mem: "Vagree ν ω V ⟹ (ν∈selectlike X ω V) = (ν∈X)"
unfolding selectlike_def using Vagree_sym_rel by blast

(* also see nonBVG_rule *)
lemma BVG_nonelem [simp] :"(x∉BVG α) = (∀I ω X. (ω ∈ game_sem I α X) = (ω ∈ game_sem I α (selectlike X ω {x})))"
using BVG_elem monotone selectlike_shrinks
by (metis subset_iff)

text ‹‹statediff› interoperability›

lemma Vagree_statediff [simp]: "Vagree ω ω' S ⟹ statediff ω ω' ⊆ -S"
by (auto simp add: Vagree_def statediff_def)

lemma stateinterpol_diff [simp]: "stateinterpol ν ω (statediff ν ω) = ν"
proof
fix x
show sp: "(stateinterpol ν ω (statediff ν ω))(x) = ν(x)"
proof (cases "x∈statediff ν ω")
case True
then show ?thesis by simp
next
case False
then show ?thesis by (simp add: stateinterpol_def nostatediff)
qed
qed

lemma stateinterpol_insert: "Vagree (stateinterpol v w S) (stateinterpol v w (insert z S)) (-{z})"

lemma stateinterpol_FVT [simp]: "z∉FVT(t) ⟹ term_sem I t (stateinterpol ω ω' S) = term_sem I t (stateinterpol ω ω' (insert z S))"
proof -
assume a: "z∉FVT(t)"
have fvc: "⋀v. ⋀w. Vagree v w (-{z}) ⟹ (term_sem I t v = term_sem I t w)" using a by (simp add: FVT_def)
then show "term_sem I t (stateinterpol ω ω' S) = term_sem I t (stateinterpol ω ω' (insert z S))"
using fvc and stateinterpol_insert by blast
qed

subsection ‹Coincidence Lemmas›

paragraph ‹Coincidence for Terms›

text ‹Lemma 10 🌐‹https://doi.org/10.1007/978-3-319-94205-6_15››

theorem coincidence_term: "Vagree ω ω' (FVT θ) ⟹ term_sem I θ ω = term_sem I θ ω'"
proof -
assume a: "Vagree ω ω' (FVT θ)"
have isS: "statediff ω ω' ⊆ -FVT(θ)" using a and Vagree_statediff by simp
have gen: "S⊆-FVT(θ) ⟹ (term_sem I θ ω' = term_sem I θ (stateinterpol ω ω' S))" if "finite S" for S
using that
proof (induction S)
case empty
show ?case by (simp add: stateinterpol_empty)
next
case (insert z S)
thus ?case by auto
qed
from isS have finS: "finite (statediff ω ω')" using allvars_finite by (metis FVT_finite UNIV_def finite_compl rev_finite_subset)
show ?thesis using gen[where S=‹statediff ω ω'›, OF finS, OF isS] by simp
qed

corollary coincidence_term_cor: "Uvariation ω ω' U ⟹ (FVT θ)∩U={} ⟹ term_sem I θ ω = term_sem I θ ω'"
using coincidence_term Uvariation_Vagree
by (metis Vagree_antimon disjoint_eq_subset_Compl double_compl)

lemma stateinterpol_FVF [simp]: "z∉FVF(e) ⟹
((stateinterpol ω ω' S) ∈ fml_sem I e ⟷ (stateinterpol ω ω' (insert z S)) ∈ fml_sem I e)"
proof -
assume a: "z∉FVF(e)"
have agr: "Vagree (stateinterpol ω ω' S) (stateinterpol ω ω' (insert z S)) (-{z})" by (simp add: Vagree_def stateinterpol_def)
have fvc: "⋀v. ⋀w. (Vagree v w (-{z}) ⟹ (v∈fml_sem I e ⟹ w∈fml_sem I e))" using a by (simp add: FVF_def)
then have fvce: "⋀v. ⋀w. (Vagree v w (-{z}) ⟹ ((v∈fml_sem I e) = (w∈fml_sem I e)))"  using Vagree_sym_rel by blast
then show "(stateinterpol ω ω' S) ∈ fml_sem I e ⟷ (stateinterpol ω ω' (insert z S)) ∈ fml_sem I e"
using agr by simp
qed

paragraph ‹Coincidence for Formulas›

text ‹Lemma 11 🌐‹https://doi.org/10.1007/978-3-319-94205-6_15››

theorem coincidence_formula: "Vagree ω ω' (FVF φ) ⟹ (ω ∈ fml_sem I φ ⟷ ω' ∈ fml_sem I φ)"
proof -
assume a: "Vagree ω ω' (FVF φ)"
have isS: "statediff ω ω' ⊆ -FVF(φ)" using a and Vagree_statediff by simp
have gen: "S⊆-FVF(φ) ⟹ (ω' ∈ fml_sem I φ ⟷ (stateinterpol ω ω' S) ∈ fml_sem I φ)" if "finite S" for S
using that
proof (induction S)
case empty
show ?case by (simp add: stateinterpol_empty)
next
case (insert z S)
thus ?case by auto
qed
from isS have finS: "finite (statediff ω ω')" using allvars_finite by (metis FVF_finite UNIV_def finite_compl rev_finite_subset)
show ?thesis using gen[where S=‹statediff ω ω'›, OF finS, OF isS] by simp
qed

corollary coincidence_formula_cor: "Uvariation ω ω' U ⟹ (FVF φ)∩U={} ⟹ (ω ∈ fml_sem I φ ⟷ ω' ∈ fml_sem I φ)"
using coincidence_formula Uvariation_Vagree
by (metis Uvariation_def disjoint_eq_subset_Compl inf.commute subsetCE)

paragraph ‹Coincidence for Games›

text ‹‹Cignorabimus α V› is the set of all sets of variables that can be ignored for the coincidence game lemma›
definition Cignorabimus:: "game ⇒ variable set ⇒ variable set set"
where
"Cignorabimus α V = {M. ∀I.∀ω.∀ω'.∀X. (Vagree ω ω' (-M) ⟶ (ω∈game_sem I α (restrictto X V)) ⟶ (ω'∈game_sem I α (restrictto X V)))}"

lemma Cignorabimus_finite [simp]: "finite (Cignorabimus α V)"
unfolding Cignorabimus_def using finite_powerset[OF allvars_finite] finite_subset using Finite_Set.finite_subset by fastforce

lemma Cignorabimus_equiv [simp]: "Cignorabimus α V = {M. ∀I.∀ω.∀ω'.∀X. (Vagree ω ω' (-M) ⟶ (ω∈game_sem I α (restrictto X V)) = (ω'∈game_sem I α (restrictto X V)))}"
unfolding Cignorabimus_def by (metis (no_types, lifting) Vagree_sym_rel)

lemma Cignorabimus_antimon [simp]: "M ∈ Cignorabimus α V ∧ N⊆M ⟹ N ∈ Cignorabimus α V"
unfolding Cignorabimus_def
using Vagree_antimon by blast

lemma coempty: "-{}=allvars"
by simp

lemma Cignorabimus_empty [simp]: "{} ∈ Cignorabimus α V"
unfolding Cignorabimus_def using coempty Vagree_univ
by simp

text ‹Cignorabimus contains nonfree variables›
lemma Cignorabimus_init: "V⊇FVG(α) ⟹ x∉V ⟹ {x}∈Cignorabimus α V"
proof-
assume "V⊇FVG(α)"
assume a0: "x∉V"
hence a1: "x∉FVG(α)" using ‹FVG α ⊆ V› by blast
hence "⋀I v w. Vagree v w (-{x}) ⟹ (v ∈ game_sem I α (restrictto X (-{x})) ⟷ w ∈ game_sem I α (restrictto X (-{x})))"
by (metis (mono_tags, lifting) CollectI FVG_def Vagree_sym_rel)
show "{x}∈Cignorabimus α V"
proof-
{
fix I ω ω' X
have "Vagree ω ω' (-{x}) ⟶ (ω∈game_sem I α (restrictto X V)) ⟶ (ω'∈game_sem I α (restrictto X V))"
proof
assume a2: "Vagree ω ω' (-{x})"
show "(ω∈game_sem I α (restrictto X V)) ⟶ (ω'∈game_sem I α (restrictto X V))"
proof
assume "ω∈game_sem I α (restrictto X V)"
hence "ω∈game_sem I α (restrictto (restrictto X V) (-{x}))" by (simp add: Int_absorb2 ‹x∉V›)
hence "ω'∈game_sem I α (restrictto (restrictto X V) (-{x}))" using FVG_def a1 a2 by blast
hence "ω'∈game_sem I α (restrictto X (V∩-{x}))" by simp
show "ω'∈game_sem I α (restrictto X V)" using a0
by (metis Int_absorb2 ‹ω' ∈ game_sem I α (restrictto X (V ∩ - {x}))› subset_Compl_singleton)
qed
qed
}
thus ?thesis
unfolding Cignorabimus_def
by auto
qed
qed

text ‹Cignorabimus is closed under union›
lemma Cignorabimus_union: "M∈Cignorabimus α V ⟹ N∈Cignorabimus α V ⟹ (M∪N)∈Cignorabimus α V"
proof-
assume a1: "M∈Cignorabimus α V"
assume a2: "N∈Cignorabimus α V"
show "(M∪N)∈Cignorabimus α V" (*using a1 a2 unfolding Cignorabimus_def *)
proof-
{
fix I ω ω' X
assume a3: "Vagree ω ω' (-(M∪N))"
have h1: "⋀I ω ω'.⋀X. (Vagree ω ω' (-M) ⟹  (ω∈game_sem I α (restrictto X V)) ⟹ (ω'∈game_sem I α (restrictto X V)))" using a1 by simp
have h2: "⋀I ω ω'.⋀X. (Vagree ω ω' (-N) ⟹  (ω∈game_sem I α (restrictto X V)) ⟹ (ω'∈game_sem I α (restrictto X V)))" using a2 by simp
let ?s = "stateinterpol ω' ω M"
have v1: "Vagree ω ?s (-(M∪N))" using a3 by (simp add: Vagree_def)
have v2: "Vagree ?s ω' (-(M∪N))" using a3 by (simp add: Vagree_def)
have r1: "ω∈game_sem I α (restrictto X V) ⟹ ?s∈game_sem I α (restrictto X V)"
by (metis ComplD Vagree_def h1 stateinterpol_right)
have r2: "?s∈game_sem I α (restrictto X V) ⟹ ω'∈game_sem I α (restrictto X V)"
by (metis Vagree_ror compl_sup h1 h2 v2)
have res: "ω∈game_sem I α (restrictto X V) ⟹ ω'∈game_sem I α (restrictto X V)" using r1 r2 by blast
}
thus ?thesis
unfolding Cignorabimus_def
by auto
qed
qed

lemma powersetup_induct [case_names Base Cup]:
"⋀C. (⋀M. M∈C ⟹ P M) ⟹
(⋀S. (⋀M. M∈S ⟹ P M) ⟹ P (⋃S)) ⟹
P (⋃C)"
by simp

lemma Union_insert: "⋃(insert x S) = x∪⋃S"
by simp

lemma powerset2up_induct [case_names Finite Nonempty Base Cup]:
"(finite C) ⟹ (C≠{}) ⟹ (⋀M. M∈C ⟹ P M) ⟹
(⋀M N. P M ⟹ P N ⟹ P (M∪N)) ⟹
P (⋃C)"
proof (induction rule: finite_induct)
case empty
then show ?case by simp
next
case (insert x F)
then show ?case by force
qed

lemma Cignorabimus_step: "(⋀M. M∈S ⟹ M∈Cignorabimus α V) ⟹ (⋃S)∈Cignorabimus α V"
proof (cases "S={}")
case True
then show ?thesis using Cignorabimus_empty by simp
next
case nonem: False
then show "⋃S∈Cignorabimus α V" if "⋀M. M∈S ⟹ M∈Cignorabimus α V" and nonemp:"S≠{}" for S
proof (induction rule: powerset2up_induct)
case Finite
then show ?case using Cignorabimus_finite by (meson infinite_super subset_eq that(1))
next
case Nonempty
then show ?case using nonemp by simp
next
case (Base M)
then show ?case using that by simp
next
case (Cup S)
then show ?case using that Cignorabimus_union by blast
qed
qed

text ‹Lemma 12 🌐‹https://doi.org/10.1007/978-3-319-94205-6_15››

theorem coincidence_game: "Vagree ω ω' V ⟹ V⊇FVG(α) ⟹ (ω ∈ game_sem I α (restrictto X V)) = (ω' ∈ game_sem I α (restrictto X V))"
proof-
assume a1: "Vagree ω ω' V"
assume a2: "V ⊇ FVG α"
have base: "{x}∈Cignorabimus α V" if a3: "x∉V" and a4: "V ⊇ FVG α" for x V
using a3 and a4 and Cignorabimus_init by simp
have h: "-V = ⋃{xx. ∃x. xx={x} ∧ x∉V}" by auto (* finite *)
have "(-V)∈Cignorabimus α V" using a2 base h using Cignorabimus_step
(*by (smt Cignorabimus_step mem_Collect_eq)*)
proof - (*sledgehammer*)
have f1: "∀v V. v ∈ V ∨ ¬ FVG α ⊆ V ∨ {v} ∈ Cignorabimus α V"
using base by satx
obtain VV :: "variable set ⇒ game ⇒ variable set set ⇒ variable set" where
f2: "∀x0 x1 x2. (∃v3. v3 ∈ x2 ∧ v3 ∉ Cignorabimus x1 x0) = (VV x0 x1 x2 ∈ x2 ∧ VV x0 x1 x2 ∉ Cignorabimus x1 x0)"
by moura
obtain vv :: "variable set ⇒ variable" where
f3: "((∄v. VV V α {{v} |v. v ∉ V} = {v} ∧ v ∉ V) ∨ VV V α {{v} |v. v ∉ V} = {vv (VV V α {{v} |v. v ∉ V})} ∧ vv (VV V α {{v} |v. v ∉ V}) ∉ V) ∧ ((∃v. VV V α {{v} |v. v ∉ V} = {v} ∧ v ∉ V) ∨ (∀v. VV V α {{v} |v. v ∉ V} ≠ {v} ∨ v ∈ V))"
by moura
moreover
{ assume "{vv (VV V α {{v} |v. v ∉ V})} ∈ Cignorabimus α V"
then have "(VV V α {{v} |v. v ∉ V} ≠ {vv (VV V α {{v} |v. v ∉ V})} ∨ vv (VV V α {{v} |v. v ∉ V}) ∈ V) ∨ VV V α {{v} |v. v ∉ V} ∉ {{v} |v. v ∉ V} ∨ VV V α {{v} |v. v ∉ V} ∈ Cignorabimus α V"
by metis
then have "(∃v. VV V α {{v} |v. v ∉ V} = {v} ∧ v ∉ V) ⟶ VV V α {{v} |v. v ∉ V} ∉ {{v} |v. v ∉ V} ∨ VV V α {{v} |v. v ∉ V} ∈ Cignorabimus α V"
using f3 by blast }
ultimately have "VV V α {{v} |v. v ∉ V} ∉ {{v} |v. v ∉ V} ∨ VV V α {{v} |v. v ∉ V} ∈ Cignorabimus α V"
using f1 a2 by blast
then have "⋃{{v} |v. v ∉ V} ∈ Cignorabimus α V"
using f2 by (meson Cignorabimus_step)
then show ?thesis
using h by presburger
qed
from this show ?thesis by (simp add: a1)
qed

corollary coincidence_game_cor: "Uvariation ω ω' U ⟹ U∩FVG(α)={} ⟹ (ω ∈ game_sem I α (restrictto X (-U))) = (ω' ∈ game_sem I α (restrictto X (-U)))"
using coincidence_game Uvariation_Vagree
by (metis Uvariation_Vagree coincidence_game compl_le_swap1 disjoint_eq_subset_Compl double_compl)

subsection ‹Bound Effect Lemmas›

text ‹‹Bignorabimus α V› is the set of all sets of variables that can be ignored for boundeffect›
definition Bignorabimus:: "game ⇒ variable set set"
where
"Bignorabimus α = {M. ∀I.∀ω.∀X. ω∈game_sem I α X ⟷ ω∈game_sem I α (selectlike X ω M)}"

lemma Bignorabimus_finite [simp]: "finite (Bignorabimus α)"
unfolding Bignorabimus_def using finite_powerset[OF allvars_finite] finite_subset using Finite_Set.finite_subset by fastforce

lemma Bignorabimus_single [simp]: "game_sem I α (selectlike X ω M) ⊆ game_sem I α X"
by (meson monotone selectlike_shrinks subsetCE)

lemma Bignorabimus_equiv [simp]: "Bignorabimus α = {M. ∀I.∀ω.∀X. (ω∈game_sem I α X ⟶ ω∈game_sem I α (selectlike X ω M))}"
(*by (smt Bignorabimus_def Bignorabimus_single Collect_cong subsetCE)*)
proof - (*sledgehammer transformed*)
obtain VV :: "(variable set ⇒ bool) ⇒ (variable set ⇒ bool) ⇒ variable set" where
f1: "∀p pa. (¬ p (VV pa p)) = pa (VV pa p) ∨ Collect p = Collect pa"
by (metis (no_types) Collect_cong)
obtain rr :: "variable set ⇒ game ⇒ variable ⇒ real" and ii :: "variable set ⇒ game ⇒ interp" and FF :: "variable set ⇒ game ⇒ (variable ⇒ real) set" where
f2: "∀x0 x1. (∃v2 v3 v4. (v3 ∈ game_sem v2 x1 v4) ≠ (v3 ∈ game_sem v2 x1 (selectlike v4 v3 x0))) = ((rr x0 x1 ∈ game_sem (ii x0 x1) x1 (FF x0 x1)) ≠ (rr x0 x1 ∈ game_sem (ii x0 x1) x1 (selectlike (FF x0 x1) (rr x0 x1) x0)))"
by moura
have fact: "{V. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))} = {V. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V)}"
using f1 by (metis (no_types, hide_lams) Bignorabimus_single subsetCE)
have f3: "rr (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α ∉ game_sem (ii (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α) α (selectlike (FF (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α) (rr (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α) (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V)))) ∨ rr (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α ∈ game_sem (ii (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α) α (FF (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α)"
using Bignorabimus_single by blast
have f4: "(¬ (∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V)))))) ∨ (∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))))))) ∧ ((∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V)))))) ∨ (rr (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α ∉ game_sem (ii (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α) α (FF (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α)) = (rr (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α ∈ game_sem (ii (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α) α (selectlike (FF (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α) (rr (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α) (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))))))"
using f2 by blast
have "rr (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α ∈ game_sem (ii (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α) α (FF (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α) ⟶ (∃i f F. f ∈ game_sem i α F ∧ f ∉ game_sem i α (selectlike F f (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))))) ∨ rr (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α ∈ game_sem (ii (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α) α (selectlike (FF (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α) (rr (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α) (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))))"
by blast
moreover
{ assume "∃i f F. f ∈ game_sem i α F ∧ f ∉ game_sem i α (selectlike F f (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))))"
then have "¬ (∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V)))))"
by blast
moreover
{ assume "(¬ (∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V)))))) ≠ (∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))))))"
then have "{V. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))} = {V. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V)}"
using fact by simp }
ultimately have "(∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V)))))) ∨ {V. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))} = {V. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V)}"
by satx }
moreover
{ assume "∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V)))))"
then have "(¬ (∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V)))))) ≠ (∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))))))"
by blast
then have "{V. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))} = {V. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V)}"
using fact by simp}
ultimately have "{V. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))} = {V. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V)}"
using f4 f3 by satx
then show ?thesis
using Bignorabimus_def by presburger
qed

lemma Bignorabimus_empty [simp]: "{} ∈ Bignorabimus α"
unfolding Bignorabimus_def using coempty selectlike_empty
by simp

lemma Bignorabimus_init: "x∉BVG(α) ⟹ {x}∈Bignorabimus α"
unfolding Bignorabimus_def BVG_def
proof-
assume "x ∉ {x. ∃I ω X. ω ∈ game_sem I α X ∧ ω ∉ game_sem I α (selectlike X ω {x})}"
hence "¬(∃I ω X. ω ∈ game_sem I α X ∧ ω ∉ game_sem I α (selectlike X ω {x}))" by simp
hence "∀I ω X. (ω ∈ game_sem I α X) = (ω ∈ game_sem I α (selectlike X ω {x}))" using Bignorabimus_single by blast
thus "{x} ∈ {M. ∀I ω X. (ω ∈ game_sem I α X) = (ω ∈ game_sem I α (selectlike X ω M))}" by simp
qed

text ‹Bignorabimus is closed under union›
lemma Bignorabimus_union: "M∈Bignorabimus α ⟹ N∈Bignorabimus α ⟹ (M∪N)∈Bignorabimus α"
proof -
assume a1: "M∈Bignorabimus α"
assume a2: "N∈Bignorabimus α"
have h1: "∀I.∀ω.∀X. (ω∈game_sem I α X) ⟷ (ω∈game_sem I α (selectlike X ω M))" using a1
using Bignorabimus_equiv Bignorabimus_single by blast
have h2: "∀I.∀ω.∀X. (ω∈game_sem I α X) ⟷ (ω∈game_sem I α (selectlike X ω N))" using a2
using Bignorabimus_equiv Bignorabimus_single by blast
have c: "∀I.∀ω.∀X. (ω∈game_sem I α X) ⟷ (ω∈game_sem I α (selectlike X ω (M∪N)))" by (metis h1 h2 selectlike_compose)
then show "(M∪N)∈Bignorabimus α" unfolding Bignorabimus_def using c by fastforce
qed

lemma Bignorabimus_step: "(⋀M. M∈S ⟹ M∈Bignorabimus α) ⟹ (⋃S)∈Bignorabimus α"
proof (cases "S={}")
case True
then show ?thesis using Bignorabimus_empty by simp
next
case nonem: False
then show "⋃S∈Bignorabimus α" if "⋀M. M∈S ⟹ M∈Bignorabimus α" and nonemp:"S≠{}" for S
proof (induction rule: powerset2up_induct)
case Finite
then show ?case using Bignorabimus_finite by (meson infinite_super subset_eq that(1))
next
case Nonempty
then show ?case using nonemp by simp
next
case (Base M)
then show ?case using that by simp
next
case (Cup S)
then show ?case using that Bignorabimus_union by blast
qed
qed

text ‹Lemma 13 🌐‹https://doi.org/10.1007/978-3-319-94205-6_15››

theorem boundeffect: "(ω ∈ game_sem I α X) = (ω ∈ game_sem I α (selectlike X ω (-BVG(α))))"
proof-
have base: "{x}∈Bignorabimus α" if a3: "x∉BVG α" for x using a3 and Bignorabimus_init by simp
have h: "-BVG α = ⋃{xx. ∃x. xx={x} ∧ x∉BVG α}" by blast (* finite *)
have "(-BVG α)∈Bignorabimus α" using base h
(*by (smt Bignorabimus_step mem_Collect_eq)*)
proof - (*sledgehammer*)
obtain VV :: "game ⇒ variable set set ⇒ variable set" where
f1: "∀x0 x1. (∃v2. v2 ∈ x1 ∧ v2 ∉ Bignorabimus x0) = (VV x0 x1 ∈ x1 ∧ VV x0 x1 ∉ Bignorabimus x0)"
by moura
have "VV α {{v} |v. v ∉ BVG α} ∉ {{v} |v. v ∉ BVG α} ∨ VV α {{v} |v. v ∉ BVG α} ∈ Bignorabimus α"
by fastforce
then have "⋃{{v} |v. v ∉ BVG α} ∈ Bignorabimus α"
using f1 by (meson Bignorabimus_step)
then show ?thesis
using h by presburger
qed
from this show ?thesis using Bignorabimus_def by blast
qed

corollary boundeffect_cor: "V∩BVG(α)={} ⟹ (ω ∈ game_sem I α X) = (ω ∈ game_sem I α (selectlike X ω V))"
using boundeffect
by (metis disjoint_eq_subset_Compl selectlike_compose sup.absorb_iff2)

subsection ‹Static Analysis Observations›

lemma BVG_equiv: "game_equiv α β ⟹ BVG(α) = BVG(β)"
proof-
assume a: "game_equiv α β"
show "BVG(α) = BVG(β)" unfolding BVG_def using game_equiv_subst_eq[OF a] by metis
qed

lemmas union_or = Set.Un_iff

lemma not_union_or: "(x∉A∪B) = (x∉A ∧ x∉B)"
by simp

lemma repv_selectlike_self: "(repv ω x d ∈ selectlike X ω {x}) = (d=ω(x) ∧ ω ∈ X)"
unfolding selectlike_def using Vagree_repv_self Vagree_sym
by (metis (no_types, lifting) mem_Collect_eq repv_self)

lemma repv_selectlike_other: "x≠y ⟹ (repv ω x d ∈ selectlike X ω {y}) = (repv ω x d ∈ X)"
proof
assume a: "x≠y"
then have h: "{y}⊆-{x}" by simp
show "(repv ω x d ∈ selectlike X ω {y}) ⟹ (repv ω x d ∈ X)" using a selectlike_def Vagree_repv[of ω x d]
by auto
show "(repv ω x d ∈ X) ⟹ (repv ω x d ∈ selectlike X ω {y})"
using selectlike_def[where X=X and ν=ω and V=‹-{x}›] Vagree_repv[where ω=ω and x=x and d=d]
selectlike_antimon[where X=X and ν=ω and V=‹{y}› and W=‹-{x}›, OF h] Vagree_sym[where ν=‹repv ω x d› and V=‹-{x}›]
by auto
qed

lemma repv_selectlike_other_converse: "x≠y ⟹ (repv ω x d ∈ X) = (repv ω x d ∈ selectlike X ω {y})"
using repv_selectlike_other HOL.eq_commute by blast

lemma BVG_assign_other: "x≠y ⟹ y∉BVG(Assign x θ)"
using repv_selectlike_other_converse[where x=x and y=y] by simp

lemma BVG_assign_meta: "(⋀I ω. term_sem I θ ω = ω(x)) ⟹ BVG(Assign x θ) = {}"
and "term_sem I θ ω ≠ ω(x) ⟹ BVG(Assign x θ) = {x}"
(*using repv_selectlike_self BVG_assign_other BVG_def BVG_elem*)
proof-
have fact: "BVG(Assign x θ) ⊆ {x}" using BVG_assign_other by (metis singleton_iff subsetI)
from fact show "(⋀I ω. term_sem I θ ω = ω(x)) ⟹ BVG(Assign x θ) = {}" using BVG_def by simp
have h2: "∃I ω. term_sem I θ ω ≠ ω(x) ⟹ x ∈ BVG(Assign x θ)" using repv_selectlike_self by auto
from fact show "term_sem I θ ω ≠ ω(x) ⟹ BVG(Assign x θ) = {x}" using BVG_elem h2 by blast
qed

lemma BVG_assign: "BVG(Assign x θ) = (if (∀I ω. term_sem I θ ω = ω(x)) then {} else {x})"
using repv_selectlike_self repv_selectlike_other BVG_assign_other
proof-
have c0: "BVG(Assign x θ) ⊆ {x}" using BVG_assign_other by (metis singletonI subsetI)
have c1: "∀I ω. term_sem I θ ω = ω(x) ⟹ BVG(Assign x θ) = {}" using BVG_assign_other by auto
have h2: "∃I ω. term_sem I θ ω ≠ ω(x) ⟹ x ∈ BVG(Assign x θ)" using repv_selectlike_self by auto
have c2: "∃I ω. term_sem I θ ω ≠ ω(x) ⟹ BVG(Assign x θ) = {x}" using c0 h2 by blast
from c1 and c2 show ?thesis by simp
qed

lemma BVG_ODE_other: "y≠RVar x ⟹ y≠DVar x ⟹ y∉BVG(ODE x θ)"
(*using nonBVG_rule selectlike_equal_cocond_rule solves_ODE_def*)
proof-
assume yx: "y≠RVar x"
assume yxp: "y≠DVar x"
show "y∉BVG(ODE x θ)"
proof (rule nonBVG_inc_rule)
fix I ω X
assume "ω ∈ game_sem I (ODE x θ) X"
then have "∃F T. Vagree ω (F(0)) (-{DVar x}) ∧ F(T) ∈ X ∧ solves_ODE I F x θ" by simp
then obtain F T where "Vagree ω (F(0)) (-{DVar x}) ∧ F(T) ∈ X ∧ solves_ODE I F x θ" by blast
then have "Vagree ω (F(0)) (-{DVar x}) ∧ F(T) ∈ (selectlike X ω {y}) ∧ solves_ODE I F x θ"
using yx yxp solves_Vagree Vagree_def similar_selectlike_mem by auto
then have "∃F T. Vagree ω (F(0)) (-{DVar x}) ∧ F(T) ∈ (selectlike X ω {y}) ∧ solves_ODE I F x θ" by blast
then show "ω ∈ game_sem I (ODE x θ) (selectlike X ω {y})" by simp
qed
qed

text ‹This result could be strengthened to a conditional equality based on the RHS values›

lemma BVG_ODE: "BVG(ODE x θ) ⊆ {RVar x,DVar x}"
using BVG_ODE_other by blast

lemma BVG_test: "BVG(Test φ) = {}"
unfolding BVG_def game_sem.simps by auto

lemma BVG_choice: "BVG(Choice α β) ⊆ BVG(α) ∪ BVG(β)"
unfolding BVG_def game_sem.simps using not_union_or by auto
(*proof-
have f1: "⋀ω I X. (ω ∈ game_sem I α X ∪ game_sem I β X) =
(ω ∈ game_sem I α X ∨ ω ∈ game_sem I β X)" by (rule union_or)
have f2: "⋀ω I X. (ω ∉ game_sem I α (selectlike X ω {x}) ∪ game_sem I β (selectlike X ω {x})) =
(ω ∉ game_sem I α (selectlike X ω {x}) ∧ ω ∉ game_sem I β (selectlike X ω {x}))" by (rule not_union_or)
let ?lhs = "{x. ∃I ω X.
ω ∈ game_sem I α X ∪ game_sem I β X ∧
ω ∉ game_sem I α (selectlike X ω {x}) ∪ game_sem I β (selectlike X ω {x})}"
let ?rhs = "{x. ∃I ω X. ω ∈ game_sem I α X ∧ ω ∉ game_sem I α (selectlike X ω {x})} ∪
{x. ∃I ω X. ω ∈ game_sem I β X ∧ ω ∉ game_sem I β (selectlike X ω {x})}"
show "?lhs⊆?rhs" using f1 f2 by auto
qed*)

lemma select_nonBV: "x∉BVG(α) ⟹ selectlike (game_sem I α (selectlike X ω {x})) ω {x} = selectlike (game_sem I α X) ω {x}"
proof
show "selectlike (game_sem I α (selectlike X ω {x})) ω {x} ⊆ selectlike (game_sem I α X) ω {x}"
using game_sem_mono selectlike_shrinks selectlike_antimon Bignorabimus_single
by (metis selectlike_union sup.absorb_iff1)
next
assume nonbound: "x∉BVG(α)"
then have fact: "{x}∩BVG(α)={}" by auto
show "selectlike (game_sem I α X) ω {x} ⊆ selectlike (game_sem I α (selectlike X ω {x})) ω {x}"
proof
fix μ
assume "μ ∈ selectlike (game_sem I α X) ω {x}"
(* "V∩BVG(α)={} ⟹ (ω ∈ game_sem I α X) = (ω ∈ game_sem I α (selectlike X ω V))" *)
then have "μ ∈ selectlike (game_sem I α (selectlike X μ {x})) ω {x}"
using boundeffect_cor[where ω=μ and V=‹{x}› and α=α, OF fact] nonbound
by (metis ComplD ComplI co_selectlike not_union_or)
then show "μ ∈ selectlike (game_sem I α (selectlike X ω {x})) ω {x}" using selectlike_Vagree selectlike_def by fastforce
qed
qed

lemma BVG_compose: "BVG(Compose α β) ⊆ BVG(α) ∪ BVG(β)"
(*unfolding BVG_def game_sem.simps using game_union union_or not_union_or selectlike_shrinks monotone selectlike_compose*)
proof
fix x
assume a: "x∈BVG(Compose α β)"
show "x ∈ BVG α ∪ BVG β"
proof (rule ccontr)
assume "x∉BVG α ∪ BVG(β)"
then have nβ: "x∉BVG(β)"
and nα: "x∉BVG(α)" by simp_all
from a have "∃I.∃ω.∃X. ω ∈ game_sem I (Compose α β) X ∧ ω ∉ game_sem I (Compose α β) (selectlike X ω {x})" by simp
then obtain I ω X where adef: "ω ∈ game_sem I (Compose α β) X ∧ ω ∉ game_sem I (Compose α β) (selectlike X ω {x})" by blast
from adef have a1: "ω ∈ game_sem I α (game_sem I β X)" by simp
from adef have a2: "ω ∉ game_sem I α (game_sem I β (selectlike X ω {x}))" by simp
let ?Y = "selectlike X ω {x}"
from nα have nαc: "⋀I ω X. (ω ∈ game_sem I α X) = (ω ∈ game_sem I α (selectlike X ω {x}))" using BVG_nonelem by simp
from nβ have nβc: "⋀I ω X. (ω ∈ game_sem I β X) = (ω ∈ game_sem I β (selectlike X ω {x}))" using BVG_nonelem by simp
have c1: "ω ∈ game_sem I α (selectlike (game_sem I β X) ω {x})" using a1 nαc[where I=I and ω=ω and X=‹game_sem I β X›] by blast
have c2: "ω ∉ game_sem I α (selectlike (game_sem I β ?Y) ω {x})" using a2 nαc[where I=I and ω=ω and X=‹game_sem I β ?Y›] by blast
from c2 have c3: "ω ∉ game_sem I α (selectlike (game_sem I β X) ω {x})" using nβ selectlike_Vagree
proof-
have "selectlike (game_sem I β ?Y) ω {x} = selectlike (game_sem I β X) ω {x}" using nβ by (rule select_nonBV)
thus ?thesis using c2 by simp
qed
show "False" using c1 c3 nβc[where I=I] by auto
qed
qed

text ‹The converse inclusion does not hold generally, because
‹BVG(x := x+1; x:= x-1) = {} ≠ BVG(x := x+1) ∪ BVG(x := x-1) = {x}››

lemma "BVG(Compose (Assign x (Plus (Var x) (Number 1))) (Assign x (Plus (Var x) (Number (-1)))))
≠ BVG(Assign x (Plus (Var x) (Number 1))) ∪ BVG(Assign x (Plus (Var x) (Number (-1))))"
unfolding BVG_def selectlike_def repv_def Vagree_def by auto

lemma BVG_loop: "BVG(Loop α) ⊆ BVG(α)"
proof
fix x
assume a: "x∈BVG(Loop α)"
show "x ∈ BVG(α)"
proof (rule ccontr)
assume "¬ (x ∈ BVG(α))"
then have nα: "x∉BVG α" by simp
from nα have nαc: "⋀I ω X. (ω ∈ game_sem I α X) = (ω ∈ game_sem I α (selectlike X ω {x}))" using BVG_nonelem by simp
have "x∉BVG(Loop α)" (*using BVG_nonelem*)
proof (rule nonBVG_rule)
fix I ω X
let ?f = "λZ. X ∪ game_sem I α Z"
let ?g = "λY. (selectlike X ω {x}) ∪ game_sem I α Y"
let ?R = "λZ Y. selectlike Z ω {x} = selectlike Y ω {x}"
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 IH: "selectlike A ω {x} = selectlike B ω {x}" by simp
then show ?case
(* using selectlike_union nα select_nonBV IH by (smt insert_absorb2 insert_def selectlike_compose singleton_conv smt_solver=cvc4)  *)
proof-
have "selectlike (X ∪ game_sem I α A) ω {x} = selectlike X ω {x} ∪ selectlike (game_sem I α A) ω {x}" using selectlike_union by simp
also have "... = selectlike X ω {x} ∪ selectlike (game_sem I α (selectlike A ω {x})) ω {x}" using nα select_nonBV by blast
also have "... = selectlike X ω {x} ∪ selectlike (game_sem I α (selectlike B ω {x})) ω {x}" using IH by simp
also have "... = selectlike (selectlike X ω {x} ∪ game_sem I α B) ω {x}" using selectlike_union nα select_nonBV by auto
finally show "selectlike (X ∪ game_sem I α A) ω {x} = selectlike (selectlike X ω {x} ∪ game_sem I α B) ω {x}" .
qed
next
case (union M)
then have IH: "∀(A,B)∈M. selectlike A ω {x} = selectlike B ω {x}" .
then show ?case
using fst_proj_mem[where M=M] snd_proj_mem[where M=M]
selectlike_Sup[where ν=ω and V=‹{x}›] sup_corr_eq_chain by simp
(*proof-
have "selectlike (⋃fst_proj M) ω {x} = ⋃{selectlike A ω {x} | A. A∈fst_proj M}" using selectlike_Sup by simp
also have "... = ⋃{selectlike B ω {x} | B. B∈snd_proj M}" using sup_corr_eq_chain[OF IH] by simp
also have "... = selectlike (⋃snd_proj M) ω {x}" using selectlike_Sup by simp
finally show "selectlike (⋃fst_proj M) ω {x} = selectlike (⋃snd_proj M) ω {x}" .
qed*)
qed
from this show "(ω ∈ game_sem I (Loop α) X) = (ω ∈ game_sem I (Loop α) (selectlike X ω {x}))"
by (metis (mono_tags) game_sem.simps(6) lfp_def selectlike_self)
qed
then show "False" using a by blast
qed
qed

lemma BVG_dual: "BVG(Dual α) ⊆ BVG(α)"
(*unfolding game_sem.simps using BVG_elem selectlike_co_selectlike co_selectlike selectlike_complement selectlike_antimon*)
proof
fix x
assume a: "x∈BVG(Dual α)"
show "x∈BVG α"
proof-
from a have "∃I.∃ω.∃X. ω ∈ game_sem I (Dual α) X ∧ ω ∉ game_sem I (Dual α) (selectlike X ω {x})" by simp
then obtain I ω X where adef: "ω ∈ game_sem I (Dual α) X ∧ ω ∉ game_sem I (Dual α) (selectlike X ω {x})" by blast
from adef have a1: "ω ∉ game_sem I α (- X)" by simp
from adef have a2: "ω ∈ game_sem I α (- selectlike X ω {x})" by simp
let ?Y = "- selectlike X ω {x}"
have f1: "ω ∈ game_sem I α ?Y" by (rule a2)
have f2: "ω ∉ game_sem I α (selectlike ?Y ω {x})" using a1 selectlike_co_selectlike
by (metis (no_types, lifting) selectlike_shrinks monotone dual_order.trans subset_Compl_singleton)
show "x∈BVG(α)" using f1 f2 by auto
qed
qed

end
```