Theory TAO_99_SanityTests

theory TAO_99_SanityTests
imports TAO_7_Axioms
(*<*)
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_Π1_def conn_defs
    apply (rule Eq1I) apply (simp add: meta_defs)
    nitpick[expect = genuine, user_axioms=true, card i = 2,
            card j = 2, card ω = 1, card σ = 1,
            sat_solver = MiniSat_JNI, verbose, show_all]
    oops ― ‹Countermodel by Nitpick›
  lemma "[(λy. (p  q)) = (λy. (q  p)) in v]"
    unfolding identity_Π1_def
    apply (rule Eq1I) apply (simp add: meta_defs)
    nitpick[expect = genuine, user_axioms=true,
            sat_solver = MiniSat_JNI, 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!, xP⦈), 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!, xP⦈), 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!, xP⦈), xP⦈ 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!, xP⦈), xP⦈ 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!,xP ⦇E!,xP⦈)) 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!,xP ⦇E!,xP⦈))) 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,xP ⦇G,xP⦈) in v] ⟷
     ((λ x . (evalΠ1 F) x dj) = (λ x . (evalΠ1 G) x dj))"
  proof
    assume 1: "[x. (⦇F,xP ⦇G,xP⦈) in v]"
    {
      fix v
      fix y
      obtain x where y_def: "y = νυ x"
        by (meson νυ_surj surj_def)
      have "(∃r o1. Some r = d1 F ∧ Some o1 = dκ (xP) ∧ o1 ∈ ex1 r v) =
            (∃r o1. Some r = d1 G ∧ Some o1 = dκ (xP) ∧ o1 ∈ ex1 r v)"
            using 1 apply - by meta_solver
      moreover obtain r where r_def: "Some r = d1 F"
        unfolding d1_def by auto
      moreover obtain s where s_def: "Some s = d1 G"
        unfolding d1_def by auto
      moreover have "Some x = dκ (xP)"
        using dκ_proper by simp
      ultimately have "(x ∈ ex1 r v) = (x ∈ ex1 s v)"
        by (metis option.inject)
      hence "(evalΠ1 F) y dj v = (evalΠ1 G) y dj v"
        using r_def s_def y_def by (simp add: d1.rep_eq ex1_def)
    }
    thus "(λx. evalΠ1 F x dj) = (λx. evalΠ1 G x dj)"
      by auto
  next
    assume 1: "(λx. evalΠ1 F x dj) = (λx. evalΠ1 G x dj)"
    {
      fix y v
      obtain x where x_def: "x = νυ y"
        by simp
      hence "evalΠ1 F x dj = evalΠ1 G x dj"
        using 1 by metis
      moreover obtain r where r_def: "Some r = d1 F"
        unfolding d1_def by auto
      moreover obtain s where s_def: "Some s = d1 G"
        unfolding d1_def by auto
      ultimately have "(y ∈ ex1 r v) = (y ∈ ex1 s v)"
        by (simp add: d1.rep_eq ex1_def νυ_surj x_def)
      hence "[⦇F,yP ⦇G,yP⦈ in v]"
        apply - apply meta_solver
        using r_def s_def by (metis Semantics.dκ_proper option.inject)
    }
    thus "[x. (⦇F,xP ⦇G,xP⦈) 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,xP ⦇G,xP⦈) in v]"
    shows "[F = G in v] ⟷
           (∀ s . s ≠ dj ⟶ (∀ x . (evalΠ1 F) x s = (evalΠ1 G) x s))"
    proof
      interpret MetaSolver .
      assume "[F = G in v]"
      hence "F = G"
        apply - unfolding identity_Π1_def by meta_solver
      thus "∀s. s ≠ dj ⟶ (∀x. evalΠ1 F x s = evalΠ1 G x s)"
        by auto
    next
      interpret MetaSolver .
      assume "∀s. s ≠ dj ⟶ (∀x. evalΠ1 F x s = evalΠ1 G x s)"
      moreover have "((λ x . (evalΠ1 F) x dj) = (λ x . (evalΠ1 G) x dj))"
        using assms mat_eq_is_eq_dj by auto
      ultimately have "∀s x. evalΠ1 F x s = evalΠ1 G x s"
        by metis
      hence "evalΠ1 F = evalΠ1 G"
        by blast
      hence "F = G"
        by (metis evalΠ1_inverse)
      thus "[F = G in v]"
        unfolding identity_Π1_def using Eq1I 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Π1 F) x s = (evalΠ1 F) x dj"
    shows "[ x . (⦇F,xP ⦇G,xP⦈) in v] ⟷ [F = G in v]"
    by (metis (no_types) MetaSolver.Eq1S assms identity_Π1_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,xP,a⦈) = (λx . ⦇R,xP, 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,yP⦈) in v]"
  shows "(λx. ⦇R,xP,a⦈) = (λx . ⦇R,xP, ιy. ⦇G,yP⦈⦈)"
  proof -
    have "a = (ιy. ⦇G,yP⦈)"
      using MetaSolver.EqκS Semantics.dκ_inject assms
            identity_κ_def by auto
    thus ?thesis by simp
  qed

end

(*<*)
end
(*>*)