(*<*)
theory TAO_99_SanityTests
imports TAO_7_Axioms
begin
(*>*)

section‹Sanity Tests›
text‹\label{TAO_SanityTests}›

locale SanityTests
begin
  interpretation MetaSolver.
  interpretation Semantics.

subsection‹Consistency›
text‹\label{TAO_SanityTests_Consistency}›

  lemma "True"
    nitpick[expect=genuine, user_axioms, satisfy]
    by auto

subsection‹Intensionality›
text‹\label{TAO_SanityTests_Intensionality}›

  lemma "[(\<lambda>y. (q \<or> \<not>q)) = (\<lambda>y. (p \<or> \<not>p)) in v]"
    unfolding identity_Π₁_def conn_defs
    apply (rule Eq₁I) apply (simp add: meta_defs)
    nitpick[expect = genuine, user_axioms=true, card i = 2,
            card j = 2, card ψ = 1, card σ = 1,
            sat_solver = MiniSat, verbose, show_all]
    oops ― ‹Countermodel by Nitpick›
  lemma "[(\<lambda>y. (p \<or> q)) = (\<lambda>y. (q \<or> p)) in v]"
    unfolding identity_Π₁_def
    apply (rule Eq₁I) apply (simp add: meta_defs)
    nitpick[expect = genuine, user_axioms=true,
            sat_solver = MiniSat, card i = 2,
            card j = 2, card σ = 1, card ψ = 1,
            card υ = 2, verbose, show_all]
    oops ― ‹Countermodel by Nitpick›

subsection‹Concreteness coindices with Object Domains›
text‹\label{TAO_SanityTests_Concreteness}›

  lemma OrdCheck:
    "[(\<lambda> x . \<not>\<box>(\<not>(E!, x^P)), x) in v] ⟷
     (proper x) ∧ (case (rep x) of ψν y → True | _ → False)"
    using OrdinaryObjectsPossiblyConcreteAxiom
    apply (simp add: meta_defs meta_aux split: ν.split υ.split)
    using νυ_ψν_is_ψυ by fastforce
  lemma AbsCheck:
    "[(\<lambda> x . \<box>(\<not>(E!, x^P)), x) in v] ⟷
     (proper x) ∧ (case (rep x) of αν y → True | _ → False)"
    using OrdinaryObjectsPossiblyConcreteAxiom
    apply (simp add: meta_defs meta_aux split: ν.split υ.split)
    using no_αψ by blast

subsection‹Justification for Meta-Logical Axioms›
text‹\label{TAO_SanityTests_MetaAxioms}›

text‹
 begin{remark}
 OrdinaryObjectsPossiblyConcreteAxiom is equivalent to "all ordinary objects are
 possibly concrete".
 end{remark}
 ›
  lemma OrdAxiomCheck:
    "OrdinaryObjectsPossiblyConcrete ⟷
      (∀ x. ([(\<lambda> x . \<not>\<box>(\<not>(E!, x^P)), x^P) in v]
       ⟷ (case x of ψν y → True | _ → False)))"
    unfolding Concrete_def
    apply (simp add: meta_defs meta_aux split: ν.split υ.split)
    using νυ_ψν_is_ψυ by fastforce

text‹
 begin{remark}
 OrdinaryObjectsPossiblyConcreteAxiom is equivalent to "all abstract objects are
 necessarily not concrete".
 end{remark}
 ›

  lemma AbsAxiomCheck:
    "OrdinaryObjectsPossiblyConcrete ⟷
      (∀ x. ([(\<lambda> x . \<box>(\<not>(E!, x^P)), x^P) in v]
       ⟷ (case x of αν y → True | _ → False)))"
    apply (simp add: meta_defs meta_aux split: ν.split υ.split)
    using νυ_ψν_is_ψυ no_αψ by fastforce
  
text‹
 begin{remark}
 PossiblyContingentObjectExistsAxiom is equivalent to the corresponding statement
 in the embedded logic.
 end{remark}
 ›

  lemma PossiblyContingentObjectExistsCheck:
    "PossiblyContingentObjectExists ⟷ [\<not>(\<box>(\<forall> x. (E!,x^P) \<rightarrow> \<box>(E!,x^P))) in v]"
     apply (simp add: meta_defs forall_ν_def meta_aux split: ν.split υ.split)
     by (metis ν.simps(5) νυ_def υ.simps(1) no_σψ υ.exhaust)

text‹
 begin{remark}
 PossiblyNoContingentObjectExistsAxiom is equivalent to the corresponding statement
 in the embedded logic.
 end{remark}
 ›

  lemma PossiblyNoContingentObjectExistsCheck:
    "PossiblyNoContingentObjectExists ⟷ [\<not>(\<box>(\<not>(\<forall> x. (E!,x^P) \<rightarrow> \<box>(E!,x^P)))) in v]"
    apply (simp add: meta_defs forall_ν_def meta_aux split: ν.split υ.split)
    using νυ_ψν_is_ψυ by blast

subsection‹Relations in the Meta-Logic›
text‹\label{TAO_SanityTests_MetaRelations}›

text‹
 begin{remark}
 Material equality in the embedded logic corresponds to
 equality in the actual state in the meta-logic.
 end{remark}
 ›

  lemma mat_eq_is_eq_dj:
    "[\<forall> x . \<box>((F,x^P) \<equiv> (G,x^P)) in v] ⟷
     ((λ x . (evalΠ₁ F) x dj) = (λ x . (evalΠ₁ G) x dj))"
  proof
    assume 1: "[\<forall>x. \<box>((F,x^P) \<equiv> (G,x^P)) in v]"
    {
      fix v
      fix y
      obtain x where y_def: "y = νυ x"
        by (meson νυ_surj surj_def)
      have "(∃r o₁. Some r = d₁ F ∧ Some o₁ = d_\<kappa> (x^P) ∧ o₁ ∈ ex1 r v) =
            (∃r o₁. Some r = d₁ G ∧ Some o₁ = d_\<kappa> (x^P) ∧ o₁ ∈ ex1 r v)"
            using 1 apply - by meta_solver
      moreover obtain r where r_def: "Some r = d₁ F"
        unfolding d₁_def by auto
      moreover obtain s where s_def: "Some s = d₁ G"
        unfolding d₁_def by auto
      moreover have "Some x = d_\<kappa> (x^P)"
        using d_\κ_proper by simp
      ultimately have "(x ∈ ex1 r v) = (x ∈ ex1 s v)"
        by (metis option.inject)
      hence "(evalΠ₁ F) y dj v = (evalΠ₁ G) y dj v"
        using r_def s_def y_def by (simp add: d₁.rep_eq ex1_def)
    }
    thus "(λx. evalΠ₁ F x dj) = (λx. evalΠ₁ G x dj)"
      by auto
  next
    assume 1: "(λx. evalΠ₁ F x dj) = (λx. evalΠ₁ G x dj)"
    {
      fix y v
      obtain x where x_def: "x = νυ y"
        by simp
      hence "evalΠ₁ F x dj = evalΠ₁ G x dj"
        using 1 by metis
      moreover obtain r where r_def: "Some r = d₁ F"
        unfolding d₁_def by auto
      moreover obtain s where s_def: "Some s = d₁ G"
        unfolding d₁_def by auto
      ultimately have "(y ∈ ex1 r v) = (y ∈ ex1 s v)"
        by (simp add: d₁.rep_eq ex1_def νυ_surj x_def)
      hence "[(F,y^P) \<equiv> (G,y^P) in v]"
        apply - apply meta_solver
        using r_def s_def by (metis Semantics.d_\κ_proper option.inject)
    }
    thus "[\<forall>x. \<box>((F,x^P) \<equiv> (G,x^P)) in v]"
      using T6 T8 by fast
  qed

text‹
 begin{remark}
 Materially equivalent relations are equal in the embedded logic
 if and only if they also coincide in all other states.
 end{remark}
 ›

  lemma mat_eq_is_eq_if_eq_forall_j:
    assumes "[\<forall> x . \<box>((F,x^P) \<equiv> (G,x^P)) in v]"
    shows "[F = G in v] ⟷
           (∀ s . s ≠ dj ⟶ (∀ x . (evalΠ₁ F) x s = (evalΠ₁ G) x s))"
    proof
      interpret MetaSolver .
      assume "[F = G in v]"
      hence "F = G"
        apply - unfolding identity_Π₁_def by meta_solver
      thus "∀s. s ≠ dj ⟶ (∀x. evalΠ₁ F x s = evalΠ₁ G x s)"
        by auto
    next
      interpret MetaSolver .
      assume "∀s. s ≠ dj ⟶ (∀x. evalΠ₁ F x s = evalΠ₁ G x s)"
      moreover have "((λ x . (evalΠ₁ F) x dj) = (λ x . (evalΠ₁ G) x dj))"
        using assms mat_eq_is_eq_dj by auto
      ultimately have "∀s x. evalΠ₁ F x s = evalΠ₁ G x s"
        by metis
      hence "evalΠ₁ F = evalΠ₁ G"
        by blast
      hence "F = G"
        by (metis evalΠ₁_inverse)
      thus "[F = G in v]"
        unfolding identity_Π₁_def using Eq₁I by auto
    qed

text‹
 begin{remark}
 Under the assumption that all properties behave in all states like in the actual state
 the defined equality degenerates to material equality.
 end{remark}
 ›

  lemma assumes "∀ F x s . (evalΠ₁ F) x s = (evalΠ₁ F) x dj"
    shows "[\<forall> x . \<box>((F,x^P) \<equiv> (G,x^P)) in v] ⟷ [F = G in v]"
    by (metis (no_types) MetaSolver.Eq₁S assms identity_Π₁_def
                         mat_eq_is_eq_dj mat_eq_is_eq_if_eq_forall_j)

subsection‹Lambda Expressions›
text‹\label{TAO_SanityTests_MetaLambda}›

  lemma lambda_interpret_1:
  assumes "[a = b in v]"
  shows "(\<lambda>x. (R,x^P,a)) = (\<lambda>x . (R,x^P, b))"
  proof -
    have "a = b"
      using MetaSolver.EqκS Semantics.d_\κ_inject assms
            identity_κ_def by auto
    thus ?thesis by simp
  qed

  lemma lambda_interpret_2:
  assumes "[a = (\<iota>y. (G,y^P)) in v]"
  shows "(\<lambda>x. (R,x^P,a)) = (\<lambda>x . (R,x^P, \<iota>y. (G,y^P)))"
  proof -
    have "a = (\<iota>y. (G,y^P))"
      using MetaSolver.EqκS Semantics.d_\κ_inject assms
            identity_κ_def by auto
    thus ?thesis by simp
  qed

end

(*<*)
end
(*>*)