Theory TAO_99_SanityTests

(*<*)
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 "[(❙λy. (q ❙∨ ❙¬q)) ❙= (❙λy. (p ❙∨ ❙¬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 "[(❙λy. (p ❙∨ q)) ❙= (❙λy. (q ❙∨ 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:
    "[⦇❙λ x . ❙¬❙□(❙¬⦇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:
    "[⦇❙λ x . ❙□(❙¬⦇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. ([⦇❙λ x . ❙¬❙□(❙¬⦇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. ([⦇❙λ x . ❙□(❙¬⦇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 ⟷ [❙¬(❙□(❙∀ x. ⦇E!,x⇧^P⦈ ❙→ ❙□⦇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 ⟷ [❙¬(❙□(❙¬(❙∀ x. ⦇E!,x⇧^P⦈ ❙→ ❙□⦇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:
    "[❙∀ x . ❙□(⦇F,x⇧^P⦈ ❙≡ ⦇G,x⇧^P⦈) in v] ⟷
     ((λ x . (evalΠ⇩₁ F) x dj) = (λ x . (evalΠ⇩₁ G) x dj))"
  proof
    assume 1: "[❙∀x. ❙□(⦇F,x⇧^P⦈ ❙≡ ⦇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⇩_κ (x⇧^P) ∧ o⇩₁ ∈ ex1 r v) =
            (∃r o⇩₁. Some r = d⇩₁ G ∧ Some o⇩₁ = d⇩_κ (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⇩_κ (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⦈ ❙≡ ⦇G,y⇧^P⦈ in v]"
        apply - apply meta_solver
        using r_def s_def by (metis Semantics.d⇩_κ_proper option.inject)
    }
    thus "[❙∀x. ❙□(⦇F,x⇧^P⦈ ❙≡ ⦇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 "[❙∀ x . ❙□(⦇F,x⇧^P⦈ ❙≡ ⦇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 "[❙∀ x . ❙□(⦇F,x⇧^P⦈ ❙≡ ⦇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 "(❙λx. ⦇R,x⇧^P,a⦈) = (❙λ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 ❙= (❙ιy. ⦇G,y⇧^P⦈) in v]"
  shows "(❙λx. ⦇R,x⇧^P,a⦈) = (❙λx . ⦇R,x⇧^P, ❙ιy. ⦇G,y⇧^P⦈⦈)"
  proof -
    have "a = (❙ιy. ⦇G,y⇧^P⦈)"
      using MetaSolver.EqκS Semantics.d⇩_κ_inject assms
            identity_κ_def by auto
    thus ?thesis by simp
  qed

end

(*<*)
end
(*>*)