Theory TAO_5_MetaSolver

(*<*)
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]) ⟹ ([φ → ψ in v])"
    by (simp add: Semantics.T5)
  lemma ImplE[meta_elim]: "([φ → ψ in v]) ⟹ ([φ in v] ⟶ [ψ in v])"
    by (simp add: Semantics.T5)
  lemma ImplS[meta_subst]: "([φ → ψ 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] ⟹ [¬φ in v]"
    by (simp add: Semantics.T4)
  lemma NotE[meta_elim]: "[¬φ in v] ⟹ ¬[φ in v]"
    by (simp add: Semantics.T4)
  lemma NotS[meta_subst]: "[¬φ 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]) ⟹ [φ ≡ ψ in v]"
    by (simp add: equiv_def NotS ImplS ConjS)
  lemma EquivE[meta_elim]: "[φ ≡ ψ in v] ⟹ ([φ in v] ⟷ [ψ in v])"
    by (auto simp: equiv_def NotS ImplS ConjS)
  lemma EquivS[meta_subst]: "[φ ≡ ψ 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]) ⟹ [φ ∨ ψ in v]"
    by (auto simp: disj_def NotS ImplS)
  lemma DisjE[meta_elim]: "[φ ∨ ψ in v] ⟹ ([φ in v] ∨ [ψ in v])"
    by (auto simp: disj_def NotS ImplS)
  lemma DisjS[meta_subst]: "[φ ∨ ψ 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]) ⟹ [□φ in v]"
    by (simp add: Semantics.T6)
  lemma BoxE[meta_elim]: "[□φ in v] ⟹ (⋀v.[φ in v])"
    by (simp add: Semantics.T6)
  lemma BoxS[meta_subst]: "[□φ 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]) ⟹ [◇φ in v]"
    by (metis BoxS NotS diamond_def)
  lemma DiaE[meta_elim]: "[◇φ in v] ⟹ (∃v.[φ in v])"
    by (metis BoxS NotS diamond_def)
  lemma DiaS[meta_subst]: "[◇φ 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]) ⟹ [∀ x. φ x in v]"
    by (auto simp: T8)
  lemma AllE[meta_elim]: "[∀x. φ x in v] ⟹ (⋀x.[φ x in v])"
    by (auto simp: T8)
  lemma AllS[meta_subst]: "[∀x. φ x in v] = (∀x.[φ x in v])"
    by (auto simp: T8)

subsubsection‹Rules for Existence›
  lemma ExIRule: "([φ y in v]) ⟹ [∃x. φ x in v]"
    by (auto simp: exists_def Semantics.T8 Semantics.T4)
  lemma ExI[meta_intro]: "(∃ y . [φ y in v]) ⟹ [∃x. φ x in v]"
    by (auto simp: exists_def Semantics.T8 Semantics.T4)
  lemma ExE[meta_elim]: "[∃x. φ x in v] ⟹ (∃ y . [φ y in v])"
    by (auto simp: exists_def Semantics.T8 Semantics.T4)
  lemma ExS[meta_subst]: "[∃x. φ x in v] = (∃ y . [φ y in v])"
    by (auto simp: exists_def Semantics.T8 Semantics.T4)
  lemma ExERule: assumes "[∃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] ⟹ [𝒜φ in v]"
    by (auto simp: Semantics.T7)
  lemma ActualE[meta_elim]: "[𝒜φ in v] ⟹ [φ in dw]"
    by (auto simp: Semantics.T7)
  lemma ActualS[meta_subst]: "[𝒜φ in v] = [φ in dw]"
    by (auto simp: Semantics.T7)

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

  lemma EncI[meta_intro]:
    assumes "∃ r o1 . Some r = d1 F ∧ Some o1 = dκ x ∧ o1 ∈ 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 o1 . Some r = d1 F ∧ Some o1 = dκ x ∧ o1 ∈ en r"
    using assms by (auto simp: Semantics.T2)
  lemma EncS[meta_subst]:
    "[⦃x,F⦄ in v] = (∃ r o1 . Some r = d1 F ∧ Some o1 = dκ x ∧ o1 ∈ 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 = d0 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 = d0 p ∧ ex0 r v"
    using assms by (auto simp: Semantics.T3)
  lemma Exe0S[meta_subst]:
    "[⦇p⦈ in v] = (∃ r . Some r = d0 p ∧ ex0 r v)"
    by (auto simp: Semantics.T3)

subsubsection‹One-Place Relations›

  lemma Exe1I[meta_intro]:
    assumes "∃ r o1 . Some r = d1 F ∧ Some o1 = dκ x ∧ o1 ∈ 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 o1 . Some r = d1 F ∧ Some o1 = dκ x ∧ o1 ∈ ex1 r v"
    using assms by (auto simp: Semantics.T1_1)
  lemma Exe1S[meta_subst]:
    "[⦇F,x⦈ in v] = (∃ r o1 . Some r = d1 F ∧ Some o1 = dκ x ∧ o1 ∈ ex1 r v)"
    by (auto simp: Semantics.T1_1)

subsubsection‹Two-Place Relations›

  lemma Exe2I[meta_intro]:
    assumes "∃ r o1 o2 . Some r = d2 F ∧ Some o1 = dκ x
                      ∧ Some o2 = dκ y ∧ (o1, o2) ∈ 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 o1 o2 . Some r = d2 F ∧ Some o1 = dκ x
                    ∧ Some o2 = dκ y ∧ (o1, o2) ∈ ex2 r v"
    using assms by (auto simp: Semantics.T1_2)
  lemma Exe2S[meta_subst]:
    "[⦇F,x,y⦈ in v] = (∃ r o1 o2 . Some r = d2 F ∧ Some o1 = dκ x
                      ∧ Some o2 = dκ y ∧ (o1, o2) ∈ ex2 r v)"
    by (auto simp: Semantics.T1_2)


subsubsection‹Three-Place Relations›

  lemma Exe3I[meta_intro]:
    assumes "∃ r o1 o2 o3 . Some r = d3 F ∧ Some o1 = dκ x
                         ∧ Some o2 = dκ y ∧ Some o3 = dκ z
                         ∧ (o1, o2, o3) ∈ 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 o1 o2 o3 . Some r = d3 F ∧ Some o1 = dκ x
                       ∧ Some o2 = dκ y ∧ Some o3 = dκ z
                       ∧ (o1, o2, o3) ∈ ex3 r v"
    using assms by (auto simp: Semantics.T1_3)
  lemma Exe3S[meta_subst]:
    "[⦇F,x,y,z⦈ in v] = (∃ r o1 o2 o3 . Some r = d3 F ∧ Some o1 = dκ x
                                     ∧ Some o2 = dκ y ∧ Some o3 = dκ z
                                     ∧ (o1, o2, o3) ∈ ex3 r v)"
    by (auto simp: Semantics.T1_3)

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

  lemma OrdI[meta_intro]:
    assumes "∃ o1 y. Some o1 = dκ x ∧ o1 = ων y"
    shows "[⦇O!,x⦈ in v]"
    proof -
      have "IsProperInX (λx. ◇⦇E!,x⦈)"
        by show_proper
      moreover have "[◇⦇E!,x⦈ in v]"
        apply meta_solver
        using ConcretenessSemantics1 propex1 assms by fast
      ultimately show "[⦇O!,x⦈ in v]"
        unfolding Ordinary_def
        using D5_1 propex1 assms ConcretenessSemantics1 Exe1S
        by blast
    qed
  lemma OrdE[meta_elim]:
    assumes "[⦇O!,x⦈ in v]"
    shows "∃ o1 y. Some o1 = dκ x ∧ o1 = ων y"
    proof -
      have "∃r o1. Some r = d1 O! ∧ Some o1 = dκ x ∧ o1 ∈ ex1 r v"
        using assms Exe1E by simp
      moreover have "IsProperInX (λx. ◇⦇E!,x⦈)"
        by show_proper
      ultimately have "[◇⦇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] = (∃ o1 y. Some o1 = dκ x ∧ o1 = ων y)"
    using OrdI OrdE by blast

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

  lemma AbsI[meta_intro]:
    assumes "∃ o1 y. Some o1 = dκ x ∧ o1 = αν y"
    shows "[⦇A!,x⦈ in v]"
    proof -
      have "IsProperInX (λx. ¬◇⦇E!,x⦈)"
        by show_proper
      moreover have "[¬◇⦇E!,x⦈ in v]"
        apply meta_solver
        using ConcretenessSemantics2 propex1 assms
        by (metis ν.distinct(1) option.sel)
      ultimately show "[⦇A!,x⦈ in v]"
        unfolding Abstract_def
        using D5_1 propex1 assms ConcretenessSemantics1 Exe1S
        by blast
    qed
  lemma AbsE[meta_elim]:
    assumes "[⦇A!,x⦈ in v]"
    shows "∃ o1 y. Some o1 = dκ x ∧ o1 = αν y"
    proof -
      have 1: "IsProperInX (λx. ¬◇⦇E!,x⦈)"
        by show_proper
      have "∃r o1. Some r = d1 A! ∧ Some o1 = dκ x ∧ o1 ∈ ex1 r v"
        using assms Exe1E by simp
      moreover hence "[¬◇⦇E!,x⦈ in v]"
        using D5_1[OF 1]
        unfolding Abstract_def by fast
      ultimately show ?thesis
        apply - apply meta_solver
        using ConcretenessSemantics1 propex1
        by (metis ν.exhaust)
    qed
  lemma AbsS[meta_cong]:
    "[⦇A!,x⦈ in v] = (∃ o1 y. Some o1 = dκ x ∧ o1 = αν 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 "(ιx. φ x) = (ιx. ψ x)"
    proof -
      have 1: "dκ (ιx. φ x) = dκ (ιx. ψ x)"
        using assms D3 unfolding w0_def by simp
      {
        assume "∃ o1 . Some o1 = dκ (ιx. φ x)"
        hence ?thesis using 1 dκ_inject by force
      }
      moreover {
        assume "¬(∃ o1 . Some o1 = dκ (ι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 EqEI[meta_intro]:
    assumes "∃ o1 o2. Some (ων o1) = dκ x ∧ Some (ων o2) = dκ y ∧ o1 = o2"
    shows "[x =E y in v]"
    proof -
      obtain o1 o2 where 1:
        "Some (ων o1) = dκ x ∧ Some (ων o2) = dκ y ∧ o1 = o2"
        using assms by auto
      obtain r where 2:
        "Some r = d2 basic_identityE"
        using propex2 by auto
      have "[⦇O!,x⦈ & ⦇O!,y⦈ & □(∀F. ⦇F,x⦈ ≡ ⦇F,y⦈) in v]"
        proof -
          have "[⦇O!,x⦈ in v] ∧ [⦇O!,y⦈ in v]"
            using OrdI 1 by blast
          moreover have "[□(∀F. ⦇F,x⦈ ≡ ⦇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⦈ & □(∀F. ⦇F,x⦈ ≡ ⦇F,y⦈))"
        by show_proper
      ultimately have "(ων o1, ων o2) ∈ ex2 r v"
        using D5_2 1 2
        unfolding basic_identityE_def by fast
      thus "[x =E y in v]"
        using Exe2I 1 2
        unfolding basic_identityE_infix_def basic_identityE_def
        by blast
    qed
  lemma EqEE[meta_elim]:
    assumes "[x =E y in v]"
    shows "∃ o1 o2. Some (ων o1) = dκ x ∧ Some (ων o2) = dκ y ∧ o1 = o2"
  proof -
    have "IsProperInXY (λ x y . ⦇O!,x⦈ & ⦇O!,y⦈ & □(∀F. ⦇F,x⦈ ≡ ⦇F,y⦈))"
      by show_proper
    hence 1: "[⦇O!,x⦈ & ⦇O!,y⦈ & □(∀ F. ⦇F,x⦈ ≡ ⦇F,y⦈) in v]"
      using assms unfolding basic_identityE_def basic_identityE_infix_def
      using D4_2 T1_2 D5_2 by meson
    hence 2: "∃ o1 o2 . Some (ων o1) = dκ x
                     ∧ Some (ων o2) = dκ y"
      apply (subst (asm) ConjS)
      apply (subst (asm) ConjS)
      using OrdE by auto
    then obtain o1 o2 where 3:
      "Some (ων o1) = dκ x ∧ Some (ων o2) = dκ y"
      by auto
    have "∃ r . Some r = d1 (λ z . make𝗈 (λ w s . dκ (zP) = Some (ων o1)))"
      using propex1 by auto
    then obtain r where 4:
      "Some r = d1 (λ z . make𝗈 (λ w s . dκ (zP) = Some (ων o1)))"
      by auto
    hence 5: "r = (λu s w. ∃ x . νυ x = u ∧ Some x = Some (ων o1))"
      unfolding lambdabinder1_def d1_def dκ_proper
      apply transfer
      by simp
    have "[□(∀ F. ⦇F,x⦈ ≡ ⦇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 . ((ων o1) ∈ ex1 r v) = ((ων o2) ∈ ex1 r v)"
      using 2 4 unfolding valid_in_def
      by (metis "3" "6" d1.rep_eq dκ_inject dκ_proper ex1_def eval𝗈_inverse exe1.rep_eq
          mem_Collect_eq option.sel rep_proper_id νκ_proper valid_in.abs_eq)
    moreover have "(ων o1) ∈ ex1 r v"
      unfolding 5 ex1_def by simp
    ultimately have "(ων o2) ∈ ex1 r v"
      by auto
    hence "o1 = o2" unfolding 5 ex1_def by (auto simp: meta_aux)
    thus ?thesis
      using 3 by auto
  qed
  lemma EqES[meta_subst]:
    "[x =E y in v] = (∃ o1 o2. Some (ων o1) = dκ x ∧ Some (ων o2) = dκ y
                                ∧ o1 = o2)"
    using EqEI EqEE by blast

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

  lemma EqκI[meta_intro]:
    assumes "∃ o1 o2. Some o1 = dκ x ∧ Some o2 = dκ y ∧ o1 = o2"
    shows "[x =κ y in v]"
  proof -
    have "x = y" using assms dκ_inject by meson
    moreover have "[x =κ 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 =κ y in v]"
    shows "[φ x in v] = [φ y in v]"
  proof -
    have "[x =E y ∨ ⦇A!,x⦈ & ⦇A!,y⦈ & □(∀ F. ⦃x,F⦄ ≡ ⦃y,F⦄) in v]"
      using assms unfolding basic_identityκ_def by simp
    moreover {
      assume "[x =E y in v]"
      hence "(∃ o1 o2. Some o1 = dκ x ∧ Some o2 = dκ y ∧ o1 = o2)"
        using EqEE by fast
    }
    moreover {
      assume 1: "[⦇A!,x⦈ & ⦇A!,y⦈ & □(∀ F. ⦃x,F⦄ ≡ ⦃y,F⦄) in v]"
      hence 2: "(∃ o1 o2 X Y. Some o1 = dκ x ∧ Some o2 = dκ y
                              ∧ o1 = αν X ∧ o2 = αν Y)"
        using AbsE ConjE by meson
      moreover then obtain o1 o2 X Y where 3:
        "Some o1 = dκ x ∧ Some o2 = dκ y ∧ o1 = αν X ∧ o2 = αν Y"
        by auto
      moreover have 4: "[□(∀ F. ⦃x,F⦄ ≡ ⦃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. (∃ o1. Some o1 = dκ x ∧ o1 ∈ en r)
                    = (∃ o1. Some o1 = dκ y ∧ o1 ∈ en r)"
        apply - apply meta_solver
        using propex1 d1_inject apply simp
        apply transfer by simp
      hence 8: "∀ r. (o1 ∈ en r) = (o2 ∈ en r)"
        using 3 dκ_inject dκ_proper apply simp
        by (metis option.inject)
      hence "∀r. (o1 ∈ r) = (o2 ∈ r)"
        unfolding en_def using 3
        by (metis Collect_cong Collect_mem_eq ν.simps(6)
                  mem_Collect_eq makeΠ1_cases)
      hence "(o1 ∈ { x . o1 = x }) = (o2 ∈ { x . o1 = x })"
        by metis
      hence "o1 = o2" by simp
      hence "(∃ o1 o2. Some o1 = dκ x ∧ Some o2 = dκ y ∧ o1 = o2)"
        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 =κ y in v]"
    shows "∃ o1 o2. Some o1 = dκ x ∧ Some o2 = dκ y ∧ o1 = o2"
  proof -
    have "∀ φ . (v ⊨ φ x) = (v ⊨ φ y)"
      using assms Eqκ_prop by blast
    moreover obtain φ where φ_prop:
      "φ = (λ α . make𝗈 (λ w s . (∃ o1 o2. Some o1 = dκ x
                            ∧ Some o2 = dκ α ∧ o1 = o2)))"
      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
                EqES 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 =κ y in v] = (∃ o1 o2. Some o1 = dκ x ∧ Some o2 = dκ y ∧ o1 = o2)"
    using EqκI EqκE by blast

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

  lemma Eq1I[meta_intro]: "F = G ⟹ [F =1 G in v]"
    unfolding basic_identity1_def
    apply (rule BoxI, rule AllI, rule EquivI)
    by simp
  lemma Eq1E[meta_elim]: "[F =1 G in v] ⟹ F = G"
    unfolding basic_identity1_def
    apply (drule BoxE, drule_tac x="(αν { F })" in AllE, drule EquivE)
    apply (simp add: Semantics.T2)
    unfolding en_def dκ_def d1_def
    using νκ_proper rep_proper_id
    by (simp add: rep_def proper_def meta_aux νκ.rep_eq)
  lemma Eq1S[meta_subst]: "[F =1 G in v] = (F = G)"
    using Eq1I Eq1E by auto
  lemma Eq1_prop: "[F =1 G in v] ⟹ [φ F in v] = [φ G in v]"
    using Eq1E by blast

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

  lemma Eq2I[meta_intro]: "F = G ⟹ [F =2 G in v]"
    unfolding basic_identity2_def
    apply (rule AllI, rule ConjI, (subst Eq1S)+)
    by simp
  lemma Eq2E[meta_elim]: "[F =2 G in v] ⟹ F = G"
  proof -
    assume "[F =2 G in v]"
    hence 1: "[∀ x. (λy. ⦇F,xP,yP⦈) =1 (λy. ⦇G,xP,yP⦈) in v]"
      unfolding basic_identity2_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Π2 F (νυ x) (νυ xa) s w)"
        by auto
      obtain b where b_def:
        "b = (λu s w. ∃xa. νυ xa = u ∧ evalΠ2 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Π1_inject)
      hence "a u s w = b u s w" by auto
      hence "(evalΠ2 F (νυ x) u s w) = (evalΠ2 G (νυ x) u s w)"
        unfolding a_def b_def
        by (metis (no_types, opaque_lifting) νυ_surj surj_def)
      hence "(evalΠ2 F v u s w) = (evalΠ2 G v u s w)"
        unfolding x_def by auto
    }
    hence "(evalΠ2 F) = (evalΠ2 G)" by blast
    thus "F = G" by (simp add: evalΠ2_inject)
  qed
  lemma Eq2S[meta_subst]: "[F =2 G in v] = (F = G)"
    using Eq2I Eq2E by auto
  lemma Eq2_prop: "[F =2 G in v] ⟹ [φ F in v] = [φ G in v]"
    using Eq2E by blast

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

  lemma Eq3I[meta_intro]: "F = G ⟹ [F =3 G in v]"
    apply (simp add: meta_defs meta_aux conn_defs forall_ν_def basic_identity3_def)
    using MetaSolver.Eq1I valid_in.rep_eq by auto
  lemma Eq3E[meta_elim]: "[F =3 G in v] ⟹ F = G"
  proof -

    assume "[F =3 G in v]"
    hence 1: "[∀ x y. (λz. ⦇F,xP,yP,zP⦈) =1 (λz. ⦇G,xP,yP,zP⦈) in v]"
      unfolding basic_identity3_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Π3 F (νυ x) (νυ y) (νυ xa) s w)"
        by auto
      obtain b where b_def:
        "b = (λu s w. ∃xa. νυ xa = u ∧ evalΠ3 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Π1_inject)
      hence "a u s w = b u s w" by auto
      hence "(evalΠ3 F (νυ x) (νυ y) u s w) = (evalΠ3 G (νυ x) (νυ y) u s w)"
        unfolding a_def b_def
        by (metis (no_types, opaque_lifting) νυ_surj surj_def)
      hence "(evalΠ3 F v r u s w) = (evalΠ3 G v r u s w)"
        unfolding x_def y_def by auto
    }
    hence "(evalΠ3 F) = (evalΠ3 G)" by blast
    thus "F = G" by (simp add: evalΠ3_inject)
  qed
  lemma Eq3S[meta_subst]: "[F =3 G in v] = (F = G)"
    using Eq3I Eq3E by auto
  lemma Eq3_prop: "[F =3 G in v] ⟹ [φ F in v] = [φ G in v]"
    using Eq3E by blast

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

  lemma Eq0I[meta_intro]: "x = y ⟹ [x =0 y in v]"
    unfolding basic_identity0_def by (simp add: Eq1S)
  lemma Eq0E[meta_elim]: "[F =0 G in v] ⟹ F = G"
    proof -
      assume "[F =0 G in v]"
      hence "[(λy. F) =1 (λy. G) in v]"
        unfolding basic_identity0_def by simp
      hence "(λy. F) = (λy. G)"
        using Eq1S by simp
      hence "(λu s w. (∃x. νυ x = u) ∧ eval𝗈 F s w)
           = (λu s w. (∃x. νυ x = u) ∧ eval𝗈 G s w)"
        apply (simp add: meta_defs meta_aux)
        by (metis (no_types, lifting) UNIV_I makeΠ1_inverse)
      hence "⋀s w.(eval𝗈 F s w) = (eval𝗈 G s w)"
        by metis
      hence "(eval𝗈 F) = (eval𝗈 G)" by blast
      thus "F = G"
      by (metis eval𝗈_inverse)
    qed
  lemma Eq0S[meta_subst]: "[F =0 G in v] = (F = G)"
    using Eq0I Eq0E by auto
  lemma Eq0_prop: "[F =0 G in v] ⟹ [φ F in v] = [φ G in v]"
    using Eq0E by blast

end

(*<*)
end
(*>*)