(*<*)
theory TAO_5_MetaSolver
imports 
  TAO_4_BasicDefinitions 
  "HOL-Eisbach.Eisbach"
begin
(*>*)

section‹MetaSolver›
text‹\label{TAO_MetaSolver}›

text‹
 begin{remark}
 ‹meta_solver› is a resolution prover that translates
 expressions in the embedded logic to expressions in the meta-logic,
 resp. semantic expressions.
 The rules for connectives, quantifiers, exemplification
 and encoding are straightforward.
 Furthermore, rules for the defined identities are derived.
 The defined identities in the embedded logic coincide with the
 meta-logical equality.
 end{remark}
 ›

locale MetaSolver
begin
  interpretation Semantics .

  named_theorems meta_intro
  named_theorems meta_elim
  named_theorems meta_subst
  named_theorems meta_cong

  method meta_solver = (assumption | rule meta_intro
      | erule meta_elim | drule meta_elim |  subst meta_subst
      | subst (asm) meta_subst | (erule notE; (meta_solver; fail))
      )+

subsection‹Rules for Implication›
text‹\label{TAO_MetaSolver_Implication}›

  lemma ImplI[meta_intro]: "([φ in v] ==> [ψ in v]) ==> ([φ \<rightarrow> ψ in v])"
    by (simp add: Semantics.T5)
  lemma ImplE[meta_elim]: "([φ \<rightarrow> ψ in v]) ==> ([φ in v] ⟶ [ψ in v])"
    by (simp add: Semantics.T5)
  lemma ImplS[meta_subst]: "([φ \<rightarrow> ψ in v]) = ([φ in v] ⟶ [ψ in v])"
    by (simp add: Semantics.T5)

subsection‹Rules for Negation›
text‹\label{TAO_MetaSolver_Negation}›

  lemma NotI[meta_intro]: "¬[φ in v] ==> [\<not>φ in v]"
    by (simp add: Semantics.T4)
  lemma NotE[meta_elim]: "[\<not>φ in v] ==> ¬[φ in v]"
    by (simp add: Semantics.T4)
  lemma NotS[meta_subst]: "[\<not>φ in v] = (¬[φ in v])"
    by (simp add: Semantics.T4)

subsection‹Rules for Conjunction›
text‹\label{TAO_MetaSolver_Conjunction}›

  lemma ConjI[meta_intro]: "([φ in v] ∧ [ψ in v]) ==> [φ & ψ in v]"
    by (simp add: conj_def NotS ImplS)
  lemma ConjE[meta_elim]: "[φ & ψ in v] ==> ([φ in v] ∧ [ψ in v])"
    by (simp add: conj_def NotS ImplS)
  lemma ConjS[meta_subst]: "[φ & ψ in v] = ([φ in v] ∧ [ψ in v])"
    by (simp add: conj_def NotS ImplS)

subsection‹Rules for Equivalence›
text‹\label{TAO_MetaSolver_Equivalence}›

  lemma EquivI[meta_intro]: "([φ in v] ⟷ [ψ in v]) ==> [φ \<equiv> ψ in v]"
    by (simp add: equiv_def NotS ImplS ConjS)
  lemma EquivE[meta_elim]: "[φ \<equiv> ψ in v] ==> ([φ in v] ⟷ [ψ in v])"
    by (auto simp: equiv_def NotS ImplS ConjS)
  lemma EquivS[meta_subst]: "[φ \<equiv> ψ in v] = ([φ in v] ⟷ [ψ in v])"
    by (auto simp: equiv_def NotS ImplS ConjS)

subsection‹Rules for Disjunction›
text‹\label{TAO_MetaSolver_Disjunction}›

  lemma DisjI[meta_intro]: "([φ in v] ∨ [ψ in v]) ==> [φ \<or> ψ in v]"
    by (auto simp: disj_def NotS ImplS)
  lemma DisjE[meta_elim]: "[φ \<or> ψ in v] ==> ([φ in v] ∨ [ψ in v])"
    by (auto simp: disj_def NotS ImplS)
  lemma DisjS[meta_subst]: "[φ \<or> ψ in v] = ([φ in v] ∨ [ψ in v])"
    by (auto simp: disj_def NotS ImplS)

subsection‹Rules for Necessity›
text‹\label{TAO_MetaSolver_Necessity}›

  lemma BoxI[meta_intro]: "(∧v.[φ in v]) ==> [\<box>φ in v]"
    by (simp add: Semantics.T6)
  lemma BoxE[meta_elim]: "[\<box>φ in v] ==> (∧v.[φ in v])"
    by (simp add: Semantics.T6)
  lemma BoxS[meta_subst]: "[\<box>φ in v] = (∀ v.[φ in v])"
    by (simp add: Semantics.T6)

subsection‹Rules for Possibility›
text‹\label{TAO_MetaSolver_Possibility}›

  lemma DiaI[meta_intro]: "(∃v.[φ in v]) ==> [\<diamond>φ in v]"
    by (metis BoxS NotS diamond_def)
  lemma DiaE[meta_elim]: "[\<diamond>φ in v] ==> (∃v.[φ in v])"
    by (metis BoxS NotS diamond_def)
  lemma DiaS[meta_subst]: "[\<diamond>φ in v] = (∃ v.[φ in v])"
    by (metis BoxS NotS diamond_def)

subsection‹Rules for Quantification›
text‹\label{TAO_MetaSolver_Quantification}›

  lemma AllI[meta_intro]: "(∧x. [φ x in v]) ==> [\<forall> x. φ x in v]"
    by (auto simp: T8)
  lemma AllE[meta_elim]: "[\<forall>x. φ x in v] ==> (∧x.[φ x in v])"
    by (auto simp: T8)
  lemma AllS[meta_subst]: "[\<forall>x. φ x in v] = (∀x.[φ x in v])"
    by (auto simp: T8)

subsubsection‹Rules for Existence›
  lemma ExIRule: "([φ y in v]) ==> [\<exists>x. φ x in v]"
    by (auto simp: exists_def Semantics.T8 Semantics.T4)
  lemma ExI[meta_intro]: "(∃ y . [φ y in v]) ==> [\<exists>x. φ x in v]"
    by (auto simp: exists_def Semantics.T8 Semantics.T4)
  lemma ExE[meta_elim]: "[\<exists>x. φ x in v] ==> (∃ y . [φ y in v])"
    by (auto simp: exists_def Semantics.T8 Semantics.T4)
  lemma ExS[meta_subst]: "[\<exists>x. φ x in v] = (∃ y . [φ y in v])"
    by (auto simp: exists_def Semantics.T8 Semantics.T4)
  lemma ExERule: assumes "[\<exists>x. φ x in v]" obtains x where "[φ x in v]" 
    using ExE assms by auto

subsection‹Rules for Actuality›
text‹\label{TAO_MetaSolver_Actuality}›

  lemma ActualI[meta_intro]: "[φ in dw] ==> [\<A>φ in v]"
    by (auto simp: Semantics.T7)
  lemma ActualE[meta_elim]: "[\<A>φ in v] ==> [φ in dw]"
    by (auto simp: Semantics.T7)
  lemma ActualS[meta_subst]: "[\<A>φ in v] = [φ in dw]"
    by (auto simp: Semantics.T7)

subsection ‹Rules for Encoding›
text‹\label{TAO_MetaSolver_Encoding}›

  lemma EncI[meta_intro]:
    assumes "∃ r o₁ . Some r = d₁ F ∧ Some o₁ = d_\<kappa> x ∧ o₁ ∈ en r"
    shows "[{x,F} in v]"
    using assms by (auto simp: Semantics.T2)
  lemma EncE[meta_elim]:
    assumes "[{x,F} in v]"
    shows "∃ r o₁ . Some r = d₁ F ∧ Some o₁ = d_\<kappa> x ∧ o₁ ∈ en r"
    using assms by (auto simp: Semantics.T2)
  lemma EncS[meta_subst]:
    "[{x,F} in v] = (∃ r o₁ . Some r = d₁ F ∧ Some o₁ = d_\<kappa> x ∧ o₁ ∈ en r)"
    by (auto simp: Semantics.T2)

subsection‹Rules for Exemplification›
text‹\label{TAO_MetaSolver_Exemplification}›

subsubsection‹Zero-place Relations›

  lemma Exe0I[meta_intro]:
    assumes "∃ r . Some r = d₀ p ∧ ex0 r v"
    shows "[(p) in v]"
    using assms by (auto simp: Semantics.T3)
  lemma Exe0E[meta_elim]:
    assumes "[(p) in v]"
    shows "∃ r . Some r = d₀ p ∧ ex0 r v"
    using assms by (auto simp: Semantics.T3)
  lemma Exe0S[meta_subst]:
    "[(p) in v] = (∃ r . Some r = d₀ p ∧ ex0 r v)"
    by (auto simp: Semantics.T3)

subsubsection‹One-Place Relations›

  lemma Exe1I[meta_intro]:
    assumes "∃ r o₁ . Some r = d₁ F ∧ Some o₁ = d_\<kappa> x ∧ o₁ ∈ ex1 r v"
    shows "[(F,x) in v]"
    using assms by (auto simp: Semantics.T1_1)
  lemma Exe1E[meta_elim]:
    assumes "[(F,x) in v]"
    shows "∃ r o₁ . Some r = d₁ F ∧ Some o₁ = d_\<kappa> x ∧ o₁ ∈ ex1 r v"
    using assms by (auto simp: Semantics.T1_1)
  lemma Exe1S[meta_subst]:
    "[(F,x) in v] = (∃ r o₁ . Some r = d₁ F ∧ Some o₁ = d_\<kappa> x ∧ o₁ ∈ ex1 r v)"
    by (auto simp: Semantics.T1_1)

subsubsection‹Two-Place Relations›

  lemma Exe2I[meta_intro]:
    assumes "∃ r o₁ o₂ . Some r = d₂ F ∧ Some o₁ = d_\<kappa> x
                      ∧ Some o₂ = d_\<kappa> y ∧ (o₁, o₂) ∈ ex2 r v"
    shows "[(F,x,y) in v]"
    using assms by (auto simp: Semantics.T1_2)
  lemma Exe2E[meta_elim]:
    assumes "[(F,x,y) in v]"
    shows "∃ r o₁ o₂ . Some r = d₂ F ∧ Some o₁ = d_\<kappa> x
                    ∧ Some o₂ = d_\<kappa> y ∧ (o₁, o₂) ∈ ex2 r v"
    using assms by (auto simp: Semantics.T1_2)
  lemma Exe2S[meta_subst]:
    "[(F,x,y) in v] = (∃ r o₁ o₂ . Some r = d₂ F ∧ Some o₁ = d_\<kappa> x
                      ∧ Some o₂ = d_\<kappa> y ∧ (o₁, o₂) ∈ ex2 r v)"
    by (auto simp: Semantics.T1_2)


subsubsection‹Three-Place Relations›

  lemma Exe3I[meta_intro]:
    assumes "∃ r o₁ o₂ o₃ . Some r = d₃ F ∧ Some o₁ = d_\<kappa> x
                         ∧ Some o₂ = d_\<kappa> y ∧ Some o₃ = d_\<kappa> z
                         ∧ (o₁, o₂, o₃) ∈ ex3 r v"
    shows "[(F,x,y,z) in v]"
    using assms by (auto simp: Semantics.T1_3)
  lemma Exe3E[meta_elim]:
    assumes "[(F,x,y,z) in v]"
    shows "∃ r o₁ o₂ o₃ . Some r = d₃ F ∧ Some o₁ = d_\<kappa> x
                       ∧ Some o₂ = d_\<kappa> y ∧ Some o₃ = d_\<kappa> z
                       ∧ (o₁, o₂, o₃) ∈ ex3 r v"
    using assms by (auto simp: Semantics.T1_3)
  lemma Exe3S[meta_subst]:
    "[(F,x,y,z) in v] = (∃ r o₁ o₂ o₃ . Some r = d₃ F ∧ Some o₁ = d_\<kappa> x
                                     ∧ Some o₂ = d_\<kappa> y ∧ Some o₃ = d_\<kappa> z
                                     ∧ (o₁, o₂, o₃) ∈ ex3 r v)"
    by (auto simp: Semantics.T1_3)

subsection‹Rules for Being Ordinary›
text‹\label{TAO_MetaSolver_Ordinary}›

  lemma OrdI[meta_intro]:
    assumes "∃ o₁ y. Some o₁ = d_\<kappa> x ∧ o₁ = ψν y"
    shows "[(O!,x) in v]"
    proof -
      have "IsProperInX (λx. \<diamond>(E!,x))"
        by show_proper
      moreover have "[\<diamond>(E!,x) in v]"
        apply meta_solver
        using ConcretenessSemantics1 propex₁ assms by fast
      ultimately show "[(O!,x) in v]"
        unfolding Ordinary_def
        using D5_1 propex₁ assms ConcretenessSemantics1 Exe1S
        by blast
    qed
  lemma OrdE[meta_elim]:
    assumes "[(O!,x) in v]"
    shows "∃ o₁ y. Some o₁ = d_\<kappa> x ∧ o₁ = ψν y"
    proof -
      have "∃r o₁. Some r = d₁ O! ∧ Some o₁ = d_\<kappa> x ∧ o₁ ∈ ex1 r v"
        using assms Exe1E by simp
      moreover have "IsProperInX (λx. \<diamond>(E!,x))"
        by show_proper
      ultimately have "[\<diamond>(E!,x) in v]"
        using D5_1 unfolding Ordinary_def by fast
      thus ?thesis
        apply - apply meta_solver
        using ConcretenessSemantics2 by blast
    qed
  lemma OrdS[meta_cong]:
    "[(O!,x) in v] = (∃ o₁ y. Some o₁ = d_\<kappa> x ∧ o₁ = ψν y)"
    using OrdI OrdE by blast

subsection‹Rules for Being Abstract›
text‹\label{TAO_MetaSolver_Abstract}›

  lemma AbsI[meta_intro]:
    assumes "∃ o₁ y. Some o₁ = d_\<kappa> x ∧ o₁ = αν y"
    shows "[(A!,x) in v]"
    proof -
      have "IsProperInX (λx. \<not>\<diamond>(E!,x))"
        by show_proper
      moreover have "[\<not>\<diamond>(E!,x) in v]"
        apply meta_solver
        using ConcretenessSemantics2 propex₁ assms
        by (metis ν.distinct(1) option.sel)
      ultimately show "[(A!,x) in v]"
        unfolding Abstract_def
        using D5_1 propex₁ assms ConcretenessSemantics1 Exe1S
        by blast
    qed
  lemma AbsE[meta_elim]:
    assumes "[(A!,x) in v]"
    shows "∃ o₁ y. Some o₁ = d_\<kappa> x ∧ o₁ = αν y"
    proof -
      have 1: "IsProperInX (λx. \<not>\<diamond>(E!,x))"
        by show_proper
      have "∃r o₁. Some r = d₁ A! ∧ Some o₁ = d_\<kappa> x ∧ o₁ ∈ ex1 r v"
        using assms Exe1E by simp
      moreover hence "[\<not>\<diamond>(E!,x) in v]"
        using D5_1[OF 1]
        unfolding Abstract_def by fast
      ultimately show ?thesis
        apply - apply meta_solver
        using ConcretenessSemantics1 propex₁
        by (metis ν.exhaust)
    qed
  lemma AbsS[meta_cong]:
    "[(A!,x) in v] = (∃ o₁ y. Some o₁ = d_\<kappa> x ∧ o₁ = αν y)"
    using AbsI AbsE by blast

subsection‹Rules for Definite Descriptions›
text‹\label{TAO_MetaSolver_DefiniteDescription}›

  lemma TheEqI:
    assumes "∧x. [φ x in dw] = [ψ x in dw]"
    shows "(\<iota>x. φ x) = (\<iota>x. ψ x)"
    proof -
      have 1: "d_\<kappa> (\<iota>x. φ x) = d_\<kappa> (\<iota>x. ψ x)"
        using assms D3 unfolding w₀_def by simp
      {
        assume "∃ o₁ . Some o₁ = d_\<kappa> (\<iota>x. φ x)"
        hence ?thesis using 1 d_\κ_inject by force
      }
      moreover {
        assume "¬(∃ o₁ . Some o₁ = d_\<kappa> (\<iota>x. φ x))"
        hence ?thesis using 1 D3
        by (metis d_\κ.rep_eq evalκ_inverse)
      }
      ultimately show ?thesis by blast
    qed

subsection‹Rules for Identity›
text‹\label{TAO_MetaSolver_Identity}›

subsubsection‹Ordinary Objects›
text‹\label{TAO_MetaSolver_Identity_Ordinary}›

  lemma Eq_EI[meta_intro]:
    assumes "∃ o₁ o₂. Some (ψν o₁) = d_\<kappa> x ∧ Some (ψν o₂) = d_\<kappa> y ∧ o₁ = o₂"
    shows "[x =_E y in v]"
    proof -
      obtain o₁ o₂ where 1:
        "Some (ψν o₁) = d_\<kappa> x ∧ Some (ψν o₂) = d_\<kappa> y ∧ o₁ = o₂"
        using assms by auto
      obtain r where 2:
        "Some r = d₂ basic_identity_E"
        using propex₂ by auto
      have "[(O!,x) & (O!,y) & \<box>(\<forall>F. (F,x) \<equiv> (F,y)) in v]"
        proof -
          have "[(O!,x) in v] ∧ [(O!,y) in v]"
            using OrdI 1 by blast
          moreover have "[\<box>(\<forall>F. (F,x) \<equiv> (F,y)) in v]"
            apply meta_solver using 1 by force
          ultimately show ?thesis using ConjI by simp
        qed
      moreover have "IsProperInXY (λ x y . (O!,x) & (O!,y) & \<box>(\<forall>F. (F,x) \<equiv> (F,y)))"
        by show_proper
      ultimately have "(ψν o₁, ψν o₂) ∈ ex2 r v"
        using D5_2 1 2
        unfolding basic_identity_{E_def} by fast
      thus "[x =_E y in v]"
        using Exe2I 1 2
        unfolding basic_identity_{E_infix_def} basic_identity_{E_def}
        by blast
    qed
  lemma Eq_EE[meta_elim]:
    assumes "[x =_E y in v]"
    shows "∃ o₁ o₂. Some (ψν o₁) = d_\<kappa> x ∧ Some (ψν o₂) = d_\<kappa> y ∧ o₁ = o₂"
  proof -
    have "IsProperInXY (λ x y . (O!,x) & (O!,y) & \<box>(\<forall>F. (F,x) \<equiv> (F,y)))"
      by show_proper
    hence 1: "[(O!,x) & (O!,y) & \<box>(\<forall> F. (F,x) \<equiv> (F,y)) in v]"
      using assms unfolding basic_identity_{E_def} basic_identity_{E_infix_def}
      using D4_2 T1_2 D5_2 by meson
    hence 2: "∃ o₁ o₂ . Some (ψν o₁) = d_\<kappa> x
                     ∧ Some (ψν o₂) = d_\<kappa> y"
      apply (subst (asm) ConjS)
      apply (subst (asm) ConjS)
      using OrdE by auto
    then obtain o₁ o₂ where 3:
      "Some (ψν o₁) = d_\<kappa> x ∧ Some (ψν o₂) = d_\<kappa> y"
      by auto
    have "∃ r . Some r = d₁ (\<lambda> z . makeo (λ w s . d_\<kappa> (z^P) = Some (ψν o₁)))"
      using propex₁ by auto
    then obtain r where 4:
      "Some r = d₁ (\<lambda> z . makeo (λ w s . d_\<kappa> (z^P) = Some (ψν o₁)))"
      by auto
    hence 5: "r = (λu s w. ∃ x . νυ x = u ∧ Some x = Some (ψν o₁))"
      unfolding lambdabinder1_def d₁_def d_\κ_proper
      apply transfer
      by simp
    have "[\<box>(\<forall> F. (F,x) \<equiv> (F,y)) in v]"
      using 1 using ConjE by blast
    hence 6: "∀ v F . [(F,x) in v] ⟷ [(F,y) in v]"
      using BoxE EquivE AllE by fast
    hence "∀ v . ((ψν o₁) ∈ ex1 r v) = ((ψν o₂) ∈ ex1 r v)"
      using 2 4 unfolding valid_in_def
      by (metis "3" "6" d₁.rep_eq d_\κ_inject d_\κ_proper ex1_def evalo_inverse exe1.rep_eq
          mem_Collect_eq option.sel rep_proper_id νκ_proper valid_in.abs_eq)
    moreover have "(ψν o₁) ∈ ex1 r v"
      unfolding 5 ex1_def by simp
    ultimately have "(ψν o₂) ∈ ex1 r v"
      by auto
    hence "o₁ = o₂" unfolding 5 ex1_def by (auto simp: meta_aux)
    thus ?thesis
      using 3 by auto
  qed
  lemma Eq_ES[meta_subst]:
    "[x =_E y in v] = (∃ o₁ o₂. Some (ψν o₁) = d_\<kappa> x ∧ Some (ψν o₂) = d_\<kappa> y
                                ∧ o₁ = o₂)"
    using Eq_EI Eq_EE by blast

subsubsection‹Individuals›
text‹\label{TAO_MetaSolver_Identity_Individual}›

  lemma EqκI[meta_intro]:
    assumes "∃ o₁ o₂. Some o₁ = d_\<kappa> x ∧ Some o₂ = d_\<kappa> y ∧ o₁ = o₂"
    shows "[x =_\<kappa> y in v]"
  proof -
    have "x = y" using assms d_\κ_inject by meson
    moreover have "[x =_\<kappa> x in v]"
      unfolding basic_identity_\κ_def
      apply meta_solver
      by (metis (no_types, lifting) assms AbsI Exe1E ν.exhaust)
    ultimately show ?thesis by auto
  qed
  lemma Eqκ_prop:
    assumes "[x =_\<kappa> y in v]"
    shows "[φ x in v] = [φ y in v]"
  proof -
    have "[x =_E y \<or> (A!,x) & (A!,y) & \<box>(\<forall> F. {x,F} \<equiv> {y,F}) in v]"
      using assms unfolding basic_identity_\κ_def by simp
    moreover {
      assume "[x =_E y in v]"
      hence "(∃ o₁ o₂. Some o₁ = d_\<kappa> x ∧ Some o₂ = d_\<kappa> y ∧ o₁ = o₂)"
        using Eq_EE by fast
    }
    moreover {
      assume 1: "[(A!,x) & (A!,y) & \<box>(\<forall> F. {x,F} \<equiv> {y,F}) in v]"
      hence 2: "(∃ o₁ o₂ X Y. Some o₁ = d_\<kappa> x ∧ Some o₂ = d_\<kappa> y
                              ∧ o₁ = αν X ∧ o₂ = αν Y)"
        using AbsE ConjE by meson
      moreover then obtain o₁ o₂ X Y where 3:
        "Some o₁ = d_\<kappa> x ∧ Some o₂ = d_\<kappa> y ∧ o₁ = αν X ∧ o₂ = αν Y"
        by auto
      moreover have 4: "[\<box>(\<forall> F. {x,F} \<equiv> {y,F}) in v]"
        using 1 ConjE by blast
      hence 6: "∀ v F . [{x,F} in v] ⟷ [{y,F} in v]"
        using BoxE AllE EquivE by fast
      hence 7: "∀v r. (∃ o₁. Some o₁ = d_\<kappa> x ∧ o₁ ∈ en r)
                    = (∃ o₁. Some o₁ = d_\<kappa> y ∧ o₁ ∈ en r)"
        apply - apply meta_solver
        using propex₁ d₁_inject apply simp
        apply transfer by simp
      hence 8: "∀ r. (o₁ ∈ en r) = (o₂ ∈ en r)"
        using 3 d_\κ_inject d_\κ_proper apply simp
        by (metis option.inject)
      hence "∀r. (o₁ ∈ r) = (o₂ ∈ r)"
        unfolding en_def using 3
        by (metis Collect_cong Collect_mem_eq ν.simps(6)
                  mem_Collect_eq makeΠ₁_cases)
      hence "(o₁ ∈ { x . o₁ = x }) = (o₂ ∈ { x . o₁ = x })"
        by metis
      hence "o₁ = o₂" by simp
      hence "(∃ o₁ o₂. Some o₁ = d_\<kappa> x ∧ Some o₂ = d_\<kappa> y ∧ o₁ = o₂)"
        using 3 by auto
    }
    ultimately have "x = y"
      using DisjS using Semantics.d_\κ_inject by auto
    thus "(v ⊨ (φ x)) = (v ⊨ (φ y))" by simp
  qed
  lemma EqκE[meta_elim]:
    assumes "[x =_\<kappa> y in v]"
    shows "∃ o₁ o₂. Some o₁ = d_\<kappa> x ∧ Some o₂ = d_\<kappa> y ∧ o₁ = o₂"
  proof -
    have "∀ φ . (v ⊨ φ x) = (v ⊨ φ y)"
      using assms Eqκ_prop by blast
    moreover obtain φ where φ_prop:
      "φ = (λ α . makeo (λ w s . (∃ o₁ o₂. Some o₁ = d_\<kappa> x
                            ∧ Some o₂ = d_\<kappa> α ∧ o₁ = o₂)))"
      by auto
    ultimately have "(v ⊨ φ x) = (v ⊨ φ y)" by metis
    moreover have "(v ⊨ φ x)"
      using assms unfolding φ_prop basic_identity_\κ_def
      by (metis (mono_tags, lifting) AbsS ConjE DisjS
                Eq_ES valid_in.abs_eq)
    ultimately have "(v ⊨ φ y)" by auto
    thus ?thesis
      unfolding φ_prop
      by (simp add: valid_in_def meta_aux)
  qed
  lemma EqκS[meta_subst]:
    "[x =_\<kappa> y in v] = (∃ o₁ o₂. Some o₁ = d_\<kappa> x ∧ Some o₂ = d_\<kappa> y ∧ o₁ = o₂)"
    using EqκI EqκE by blast

subsubsection‹One-Place Relations›
text‹\label{TAO_MetaSolver_Identity_OnePlaceRelation}›

  lemma Eq₁I[meta_intro]: "F = G ==> [F =₁ G in v]"
    unfolding basic_identity₁_def
    apply (rule BoxI, rule AllI, rule EquivI)
    by simp
  lemma Eq₁E[meta_elim]: "[F =₁ G in v] ==> F = G"
    unfolding basic_identity₁_def
    apply (drule BoxE, drule_tac x="(αν { F })" in AllE, drule EquivE)
    apply (simp add: Semantics.T2)
    unfolding en_def d_\κ_def d₁_def
    using νκ_proper rep_proper_id
    by (simp add: rep_def proper_def meta_aux νκ.rep_eq)
  lemma Eq₁S[meta_subst]: "[F =₁ G in v] = (F = G)"
    using Eq₁I Eq₁E by auto
  lemma Eq₁_prop: "[F =₁ G in v] ==> [φ F in v] = [φ G in v]"
    using Eq₁E by blast

subsubsection‹Two-Place Relations›
text‹\label{TAO_MetaSolver_Identity_TwoPlaceRelation}›

  lemma Eq₂I[meta_intro]: "F = G ==> [F =₂ G in v]"
    unfolding basic_identity₂_def
    apply (rule AllI, rule ConjI, (subst Eq₁S)+)
    by simp
  lemma Eq₂E[meta_elim]: "[F =₂ G in v] ==> F = G"
  proof -
    assume "[F =₂ G in v]"
    hence 1: "[\<forall> x. (\<lambda>y. (F,x^P,y^P)) =₁ (\<lambda>y. (G,x^P,y^P)) in v]"
      unfolding basic_identity₂_def
      apply - apply meta_solver by auto
    {
      fix u v s w
      obtain x where x_def: "νυ x = v" by (metis νυ_surj surj_def)
      obtain a where a_def:
        "a = (λu s w. ∃xa. νυ xa = u ∧ evalΠ₂ F (νυ x) (νυ xa) s w)"
        by auto
      obtain b where b_def:
        "b = (λu s w. ∃xa. νυ xa = u ∧ evalΠ₂ G (νυ x) (νυ xa) s w)"
        by auto
      have "a = b" unfolding a_def b_def
          using 1 apply - apply meta_solver
          by (auto simp: meta_defs meta_aux makeΠ₁_inject)
      hence "a u s w = b u s w" by auto
      hence "(evalΠ₂ F (νυ x) u s w) = (evalΠ₂ G (νυ x) u s w)"
        unfolding a_def b_def
        by (metis (no_types, opaque_lifting) νυ_surj surj_def)
      hence "(evalΠ₂ F v u s w) = (evalΠ₂ G v u s w)"
        unfolding x_def by auto
    }
    hence "(evalΠ₂ F) = (evalΠ₂ G)" by blast
    thus "F = G" by (simp add: evalΠ₂_inject)
  qed
  lemma Eq₂S[meta_subst]: "[F =₂ G in v] = (F = G)"
    using Eq₂I Eq₂E by auto
  lemma Eq₂_prop: "[F =₂ G in v] ==> [φ F in v] = [φ G in v]"
    using Eq₂E by blast

subsubsection‹Three-Place Relations›
text‹\label{TAO_MetaSolver_Identity_ThreePlaceRelation}›

  lemma Eq₃I[meta_intro]: "F = G ==> [F =₃ G in v]"
    apply (simp add: meta_defs meta_aux conn_defs forall_ν_def basic_identity₃_def)
    using MetaSolver.Eq₁I valid_in.rep_eq by auto
  lemma Eq₃E[meta_elim]: "[F =₃ G in v] ==> F = G"
  proof -

    assume "[F =₃ G in v]"
    hence 1: "[\<forall> x y. (\<lambda>z. (F,x^P,y^P,z^P)) =₁ (\<lambda>z. (G,x^P,y^P,z^P)) in v]"
      unfolding basic_identity₃_def
      apply - apply meta_solver by auto
    {
      fix u v r s w
      obtain x where x_def: "νυ x = v" by (metis νυ_surj surj_def)
      obtain y where y_def: "νυ y = r" by (metis νυ_surj surj_def)
      obtain a where a_def:
        "a = (λu s w. ∃xa. νυ xa = u ∧ evalΠ₃ F (νυ x) (νυ y) (νυ xa) s w)"
        by auto
      obtain b where b_def:
        "b = (λu s w. ∃xa. νυ xa = u ∧ evalΠ₃ G (νυ x) (νυ y) (νυ xa) s w)"
        by auto
      have "a = b" unfolding a_def b_def
          using 1 apply - apply meta_solver
          by (auto simp: meta_defs meta_aux makeΠ₁_inject)
      hence "a u s w = b u s w" by auto
      hence "(evalΠ₃ F (νυ x) (νυ y) u s w) = (evalΠ₃ G (νυ x) (νυ y) u s w)"
        unfolding a_def b_def
        by (metis (no_types, opaque_lifting) νυ_surj surj_def)
      hence "(evalΠ₃ F v r u s w) = (evalΠ₃ G v r u s w)"
        unfolding x_def y_def by auto
    }
    hence "(evalΠ₃ F) = (evalΠ₃ G)" by blast
    thus "F = G" by (simp add: evalΠ₃_inject)
  qed
  lemma Eq₃S[meta_subst]: "[F =₃ G in v] = (F = G)"
    using Eq₃I Eq₃E by auto
  lemma Eq₃_prop: "[F =₃ G in v] ==> [φ F in v] = [φ G in v]"
    using Eq₃E by blast

subsubsection‹Propositions›
text‹\label{TAO_MetaSolver_Identity_Proposition}›

  lemma Eq₀I[meta_intro]: "x = y ==> [x =₀ y in v]"
    unfolding basic_identity₀_def by (simp add: Eq₁S)
  lemma Eq₀E[meta_elim]: "[F =₀ G in v] ==> F = G"
    proof -
      assume "[F =₀ G in v]"
      hence "[(\<lambda>y. F) =₁ (\<lambda>y. G) in v]"
        unfolding basic_identity₀_def by simp
      hence "(\<lambda>y. F) = (\<lambda>y. G)"
        using Eq₁S by simp
      hence "(λu s w. (∃x. νυ x = u) ∧ evalo F s w)
           = (λu s w. (∃x. νυ x = u) ∧ evalo G s w)"
        apply (simp add: meta_defs meta_aux)
        by (metis (no_types, lifting) UNIV_I makeΠ₁_inverse)
      hence "∧s w.(evalo F s w) = (evalo G s w)"
        by metis
      hence "(evalo F) = (evalo G)" by blast
      thus "F = G"
      by (metis evalo_inverse)
    qed
  lemma Eq₀S[meta_subst]: "[F =₀ G in v] = (F = G)"
    using Eq₀I Eq₀E by auto
  lemma Eq₀_prop: "[F =₀ G in v] ==> [φ F in v] = [φ G in v]"
    using Eq₀E by blast

end

(*<*)
end
(*>*)