# Theory TAO_5_MetaSolver

theory TAO_5_MetaSolver
imports TAO_4_BasicDefinitions
(*<*)
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 o⇩1 . Some r = d⇩1 F ∧ Some o⇩1 = d⇩κ x ∧ o⇩1 ∈ 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⇩1 . Some r = d⇩1 F ∧ Some o⇩1 = d⇩κ x ∧ o⇩1 ∈ en r"
using assms by (auto simp: Semantics.T2)
lemma EncS[meta_subst]:
"[⦃x,F⦄ in v] = (∃ r o⇩1 . Some r = d⇩1 F ∧ Some o⇩1 = d⇩κ x ∧ o⇩1 ∈ 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⇩0 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⇩0 p ∧ ex0 r v"
using assms by (auto simp: Semantics.T3)
lemma Exe0S[meta_subst]:
"[⦇p⦈ in v] = (∃ r . Some r = d⇩0 p ∧ ex0 r v)"
by (auto simp: Semantics.T3)

subsubsection‹One-Place Relations›

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

subsubsection‹Two-Place Relations›

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

subsubsection‹Three-Place Relations›

lemma Exe3I[meta_intro]:
assumes "∃ r o⇩1 o⇩2 o⇩3 . Some r = d⇩3 F ∧ Some o⇩1 = d⇩κ x
∧ Some o⇩2 = d⇩κ y ∧ Some o⇩3 = d⇩κ z
∧ (o⇩1, o⇩2, o⇩3) ∈ 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⇩1 o⇩2 o⇩3 . Some r = d⇩3 F ∧ Some o⇩1 = d⇩κ x
∧ Some o⇩2 = d⇩κ y ∧ Some o⇩3 = d⇩κ z
∧ (o⇩1, o⇩2, o⇩3) ∈ ex3 r v"
using assms by (auto simp: Semantics.T1_3)
lemma Exe3S[meta_subst]:
"[⦇F,x,y,z⦈ in v] = (∃ r o⇩1 o⇩2 o⇩3 . Some r = d⇩3 F ∧ Some o⇩1 = d⇩κ x
∧ Some o⇩2 = d⇩κ y ∧ Some o⇩3 = d⇩κ z
∧ (o⇩1, o⇩2, o⇩3) ∈ 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⇩1 y. Some o⇩1 = d⇩κ x ∧ o⇩1 = ων 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 propex⇩1 assms by fast
ultimately show "[⦇O!,x⦈ in v]"
unfolding Ordinary_def
using D5_1 propex⇩1 assms ConcretenessSemantics1 Exe1S
by blast
qed
lemma OrdE[meta_elim]:
assumes "[⦇O!,x⦈ in v]"
shows "∃ o⇩1 y. Some o⇩1 = d⇩κ x ∧ o⇩1 = ων y"
proof -
have "∃r o⇩1. Some r = d⇩1 O! ∧ Some o⇩1 = d⇩κ x ∧ o⇩1 ∈ 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] = (∃ o⇩1 y. Some o⇩1 = d⇩κ x ∧ o⇩1 = ων y)"
using OrdI OrdE by blast

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

lemma AbsI[meta_intro]:
assumes "∃ o⇩1 y. Some o⇩1 = d⇩κ x ∧ o⇩1 = αν 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 propex⇩1 assms
by (metis ν.distinct(1) option.sel)
ultimately show "[⦇A!,x⦈ in v]"
unfolding Abstract_def
using D5_1 propex⇩1 assms ConcretenessSemantics1 Exe1S
by blast
qed
lemma AbsE[meta_elim]:
assumes "[⦇A!,x⦈ in v]"
shows "∃ o⇩1 y. Some o⇩1 = d⇩κ x ∧ o⇩1 = αν y"
proof -
have 1: "IsProperInX (λx. ❙¬❙◇⦇E!,x⦈)"
by show_proper
have "∃r o⇩1. Some r = d⇩1 A! ∧ Some o⇩1 = d⇩κ x ∧ o⇩1 ∈ 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 propex⇩1
by (metis ν.exhaust)
qed
lemma AbsS[meta_cong]:
"[⦇A!,x⦈ in v] = (∃ o⇩1 y. Some o⇩1 = d⇩κ x ∧ o⇩1 = αν 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 w⇩0_def by simp
{
assume "∃ o⇩1 . Some o⇩1 = d⇩κ (❙ιx. φ x)"
hence ?thesis using 1 d⇩κ_inject by force
}
moreover {
assume "¬(∃ o⇩1 . Some o⇩1 = 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 Eq⇩EI[meta_intro]:
assumes "∃ o⇩1 o⇩2. Some (ων o⇩1) = d⇩κ x ∧ Some (ων o⇩2) = d⇩κ y ∧ o⇩1 = o⇩2"
shows "[x ❙=⇩E y in v]"
proof -
obtain o⇩1 o⇩2 where 1:
"Some (ων o⇩1) = d⇩κ x ∧ Some (ων o⇩2) = d⇩κ y ∧ o⇩1 = o⇩2"
using assms by auto
obtain r where 2:
"Some r = d⇩2 basic_identity⇩E"
using propex⇩2 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 "(ων o⇩1, ων o⇩2) ∈ 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⇩1 o⇩2. Some (ων o⇩1) = d⇩κ x ∧ Some (ων o⇩2) = d⇩κ y ∧ o⇩1 = o⇩2"
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_identity⇩E_def basic_identity⇩E_infix_def
using D4_2 T1_2 D5_2 by meson
hence 2: "∃ o⇩1 o⇩2 . Some (ων o⇩1) = d⇩κ x
∧ Some (ων o⇩2) = d⇩κ y"
apply (subst (asm) ConjS)
apply (subst (asm) ConjS)
using OrdE by auto
then obtain o⇩1 o⇩2 where 3:
"Some (ων o⇩1) = d⇩κ x ∧ Some (ων o⇩2) = d⇩κ y"
by auto
have "∃ r . Some r = d⇩1 (❙λ z . make𝗈 (λ w s . d⇩κ (z⇧P) = Some (ων o⇩1)))"
using propex⇩1 by auto
then obtain r where 4:
"Some r = d⇩1 (❙λ z . make𝗈 (λ w s . d⇩κ (z⇧P) = Some (ων o⇩1)))"
by auto
hence 5: "r = (λu s w. ∃ x . νυ x = u ∧ Some x = Some (ων o⇩1))"
unfolding lambdabinder1_def d⇩1_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 . ((ων o⇩1) ∈ ex1 r v) = ((ων o⇩2) ∈ ex1 r v)"
using 2 4 unfolding valid_in_def
by (metis "3" "6" d⇩1.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 "(ων o⇩1) ∈ ex1 r v"
unfolding 5 ex1_def by simp
ultimately have "(ων o⇩2) ∈ ex1 r v"
by auto
hence "o⇩1 = o⇩2" 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⇩1 o⇩2. Some (ων o⇩1) = d⇩κ x ∧ Some (ων o⇩2) = d⇩κ y
∧ o⇩1 = o⇩2)"
using Eq⇩EI Eq⇩EE by blast

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

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

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

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

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

lemma Eq⇩2I[meta_intro]: "F = G ⟹ [F ❙=⇩2 G in v]"
unfolding basic_identity⇩2_def
apply (rule AllI, rule ConjI, (subst Eq⇩1S)+)
by simp
lemma Eq⇩2E[meta_elim]: "[F ❙=⇩2 G in v] ⟹ F = G"
proof -
assume "[F ❙=⇩2 G in v]"
hence 1: "[❙∀ x. (❙λy. ⦇F,x⇧P,y⇧P⦈) ❙=⇩1 (❙λy. ⦇G,x⇧P,y⇧P⦈) in v]"
unfolding basic_identity⇩2_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, hide_lams) νυ_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 Eq⇩2S[meta_subst]: "[F ❙=⇩2 G in v] = (F = G)"
using Eq⇩2I Eq⇩2E by auto
lemma Eq⇩2_prop: "[F ❙=⇩2 G in v] ⟹ [φ F in v] = [φ G in v]"
using Eq⇩2E by blast

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

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

assume "[F ❙=⇩3 G in v]"
hence 1: "[❙∀ x y. (❙λz. ⦇F,x⇧P,y⇧P,z⇧P⦈) ❙=⇩1 (❙λz. ⦇G,x⇧P,y⇧P,z⇧P⦈) in v]"
unfolding basic_identity⇩3_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, hide_lams) νυ_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 Eq⇩3S[meta_subst]: "[F ❙=⇩3 G in v] = (F = G)"
using Eq⇩3I Eq⇩3E by auto
lemma Eq⇩3_prop: "[F ❙=⇩3 G in v] ⟹ [φ F in v] = [φ G in v]"
using Eq⇩3E by blast

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

lemma Eq⇩0I[meta_intro]: "x = y ⟹ [x ❙=⇩0 y in v]"
unfolding basic_identity⇩0_def by (simp add: Eq⇩1S)
lemma Eq⇩0E[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_identity⇩0_def by simp
hence "(❙λy. F) = (❙λy. G)"
using Eq⇩1S 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 Eq⇩0S[meta_subst]: "[F ❙=⇩0 G in v] = (F = G)"
using Eq⇩0I Eq⇩0E by auto
lemma Eq⇩0_prop: "[F ❙=⇩0 G in v] ⟹ [φ F in v] = [φ G in v]"
using Eq⇩0E by blast

end

(*<*)
end
(*>*)