Session PLM

Theory TAO_1_Embedding

(*<*)
theory TAO_1_Embedding
imports Main
begin
(*>*)

section‹Representation Layer›
text‹\label{TAO_Embedding}›

subsection‹Primitives›
text‹\label{TAO_Embedding_Primitives}›

typedecl i ― ‹possible worlds›
typedecl j ― ‹states›

consts dw :: i ― ‹actual world›
consts dj :: j ― ‹actual state›

typedecl ω ― ‹ordinary objects›
typedecl σ ― ‹special urelements›
datatype υ = ωυ ω | συ σ ― ‹urelements›

subsection‹Derived Types›
text‹\label{TAO_Embedding_Derived_Types}›

typedef 𝗈 = "UNIV::(jibool) set"
  morphisms eval𝗈 make𝗈 .. ― ‹truth values›

type_synonym Π0 = 𝗈 ― ‹zero place relations›
typedef Π1 = "UNIV::(υjibool) set"
  morphisms evalΠ1 makeΠ1 .. ― ‹one place relations›
typedef Π2 = "UNIV::(υυjibool) set"
  morphisms evalΠ2 makeΠ2 .. ― ‹two place relations›
typedef Π3 = "UNIV::(υυυjibool) set"
  morphisms evalΠ3 makeΠ3 .. ― ‹three place relations›

type_synonym α = 1 set" ― ‹abstract objects›

datatype ν = ων ω | αν α ― ‹individuals›

typedef κ = "UNIV::(ν option) set"
  morphisms evalκ makeκ .. ― ‹individual terms›

setup_lifting type_definition_𝗈
setup_lifting type_definition_κ
setup_lifting type_definition_Π1
setup_lifting type_definition_Π2
setup_lifting type_definition_Π3

subsection‹Individual Terms and Definite Descriptions›
text‹\label{TAO_Embedding_IndividualTerms}›

lift_definition νκ :: κ" ("_P" [90] 90) is Some .
lift_definition proper :: bool" is "(≠) None" .
lift_definition rep :: ν" is the .

lift_definition that::"(ν𝗈)κ" (binder "ι" [8] 9) is
  "λ φ . if (∃! x . (φ x) dj dw)
         then Some (THE x . (φ x) dj dw)
         else None" .

subsection‹Mapping from Individuals to Urelements›
text‹\label{TAO_Embedding_AbstractObjectsToSpecialUrelements}›

consts ασ :: σ"
axiomatization where ασ_surj: "surj ασ"
definition νυ :: υ" where "νυ  case_ν ωυ (συ  ασ)"

subsection‹Exemplification of n-place-Relations.›
text‹\label{TAO_Embedding_Exemplification}›

lift_definition exe0::0𝗈" ("_") is id .
lift_definition exe1::1κ𝗈" ("_,_") is
  "λ F x s w . (proper x)  F (νυ (rep x)) s w" .
lift_definition exe2::2κκ𝗈" ("_,_,_") is
  "λ F x y s w . (proper x)  (proper y) 
     F (νυ (rep x)) (νυ (rep y)) s w" .
lift_definition exe3::3κκκ𝗈" ("_,_,_,_") is
"λ F x y z s w . (proper x)  (proper y)  (proper z) 
   F (νυ (rep x)) (νυ (rep y)) (νυ (rep z)) s w" .

subsection‹Encoding›
text‹\label{TAO_Embedding_Encoding}›

lift_definition enc :: Π1𝗈" ("_,_") is
  "λ x F s w . (proper x)  case_ν (λ ω . False) (λ α . F  α) (rep x)" .

subsection‹Connectives and Quantifiers›
text‹\label{TAO_Embedding_Connectives}›

consts I_NOT :: "j(ibool)ibool"
consts I_IMPL :: "j(ibool)(ibool)(ibool)"

lift_definition not :: "𝗈𝗈" ("¬_" [54] 70) is
  "λ p s w . s = dj  ¬p dj w  s  dj  (I_NOT s (p s) w)" .
lift_definition impl :: "𝗈𝗈𝗈" (infixl "" 51) is
  "λ p q s w . s = dj  (p dj w  q dj w)  s  dj  (I_IMPL s (p s) (q s) w)" .
lift_definition forallν :: "(ν𝗈)𝗈" (binder "ν" [8] 9) is
  "λ φ s w .  x :: ν . (φ x) s w" .
lift_definition forall0 :: "(Π0𝗈)𝗈" (binder "0" [8] 9) is
  "λ φ s w .  x :: Π0 . (φ x) s w" .
lift_definition forall1 :: "(Π1𝗈)𝗈" (binder "1" [8] 9) is
  "λ φ s w .  x :: Π1  . (φ x) s w" .
lift_definition forall2 :: "(Π2𝗈)𝗈" (binder "2" [8] 9) is
  "λ φ s w .  x :: Π2  . (φ x) s w" .
lift_definition forall3 :: "(Π3𝗈)𝗈" (binder "3" [8] 9) is
  "λ φ s w .  x :: Π3  . (φ x) s w" .
lift_definition forall𝗈 :: "(𝗈𝗈)𝗈" (binder "𝗈" [8] 9) is
  "λ φ s w .  x :: 𝗈  . (φ x) s w" .
lift_definition box :: "𝗈𝗈" ("_" [62] 63) is
  "λ p s w .  v . p s v" .
lift_definition actual :: "𝗈𝗈" ("𝒜_" [64] 65) is
  "λ p s w . p s dw" .

text‹
\begin{remark}
  The connectives behave classically if evaluated for the actual state @{term "dj"},
  whereas their behavior is governed by uninterpreted constants for any
  other state.
\end{remark}
›

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

text‹
\begin{remark}
  Lambda expressions have to convert maps from individuals to propositions to
  relations that are represented by maps from urelements to truth values.
\end{remark}
›

lift_definition lambdabinder0 :: "𝗈Π0" ("λ0") is id .
lift_definition lambdabinder1 :: "(ν𝗈)Π1" (binder "λ" [8] 9) is
  "λ φ u s w .  x . νυ x = u  φ x s w" .
lift_definition lambdabinder2 :: "(νν𝗈)Π2" ("λ2") is
  "λ φ u v s w .  x y . νυ x = u  νυ y = v  φ x y s w" .
lift_definition lambdabinder3 :: "(ννν𝗈)Π3" ("λ3") is
  "λ φ u v r s w .  x y z . νυ x = u  νυ y = v  νυ z = r  φ x y z s w" .

subsection‹Proper Maps›
text‹\label{TAO_Embedding_Proper}›

text‹
\begin{remark}
  The embedding introduces the notion of \emph{proper} maps from
  individual terms to propositions.

  Such a map is proper if and only if for all proper individual terms its truth evaluation in the
  actual state only depends on the urelements corresponding to the individuals the terms denote.

  Proper maps are exactly those maps that - when used as matrix of a lambda-expression - unconditionally
  allow beta-reduction.
\end{remark}
›

lift_definition IsProperInX :: "(κ𝗈)bool" is
  "λ φ .  x v . ( a . νυ a = νυ x  (φ (aP) dj v)) = (φ (xP) dj v)" .
lift_definition IsProperInXY :: "(κκ𝗈)bool" is
  "λ φ .  x y v . ( a b . νυ a = νυ x  νυ b = νυ y
                     (φ (aP) (bP) dj v)) = (φ (xP) (yP) dj v)" .
lift_definition IsProperInXYZ :: "(κκκ𝗈)bool" is
  "λ φ .  x y z v . ( a b c . νυ a = νυ x  νυ b = νυ y  νυ c = νυ z
                       (φ (aP) (bP) (cP) dj v)) = (φ (xP) (yP) (zP) dj v)" .


subsection‹Validity› 
text‹\label{TAO_Embedding_Validity}›

lift_definition valid_in :: "i𝗈bool" (infixl "" 5) is
  "λ v φ . φ dj v" .

text‹
\begin{remark}
  A formula is considered semantically valid for a possible world,
  if it evaluates to @{term "True"} for the actual state @{term "dj"}
  and the given possible world.
\end{remark}
›

subsection‹Concreteness›
text‹\label{TAO_Embedding_Concreteness}›

consts ConcreteInWorld :: ibool"

abbreviation (input) OrdinaryObjectsPossiblyConcrete where
  "OrdinaryObjectsPossiblyConcrete   x .  v . ConcreteInWorld x v"
abbreviation (input) PossiblyContingentObjectExists where
  "PossiblyContingentObjectExists   x v . ConcreteInWorld x v
                                         ( w . ¬ ConcreteInWorld x w)"
abbreviation (input) PossiblyNoContingentObjectExists where
  "PossiblyNoContingentObjectExists   w .  x . ConcreteInWorld x w
                                         ( v . ConcreteInWorld x v)"
axiomatization where
  OrdinaryObjectsPossiblyConcreteAxiom:
    "OrdinaryObjectsPossiblyConcrete"
  and PossiblyContingentObjectExistsAxiom:
    "PossiblyContingentObjectExists"
  and PossiblyNoContingentObjectExistsAxiom:
    "PossiblyNoContingentObjectExists"

text‹
\begin{remark}
  Care has to be taken that the defined notion of concreteness
  coincides with the meta-logical distinction between
  abstract objects and ordinary objects. Furthermore the axioms about
  concreteness have to be satisfied. This is achieved by introducing an
  uninterpreted constant @{term "ConcreteInWorld"} that determines whether
  an ordinary object is concrete in a given possible world. This constant is
  axiomatized, such that all ordinary objects are possibly concrete, contingent
  objects possibly exist and possibly no contingent objects exist.
\end{remark}
›


lift_definition Concrete::1" ("E!") is
  "λ u s w . case u of ωυ x  ConcreteInWorld x w | _  False" .

text‹
\begin{remark}
  Concreteness of ordinary objects is now defined using this
  axiomatized uninterpreted constant. Abstract objects on the other
  hand are never concrete.
\end{remark}
›

subsection‹Collection of Meta-Definitions›
text‹\label{TAO_Embedding_meta_defs}›

named_theorems meta_defs

declare not_def[meta_defs] impl_def[meta_defs] forallν_def[meta_defs]
        forall0_def[meta_defs] forall1_def[meta_defs]
        forall2_def[meta_defs] forall3_def[meta_defs] forall𝗈_def[meta_defs]
        box_def[meta_defs] actual_def[meta_defs] that_def[meta_defs]
        lambdabinder0_def[meta_defs] lambdabinder1_def[meta_defs]
        lambdabinder2_def[meta_defs] lambdabinder3_def[meta_defs]
        exe0_def[meta_defs] exe1_def[meta_defs] exe2_def[meta_defs]
        exe3_def[meta_defs] enc_def[meta_defs] inv_def[meta_defs]
        that_def[meta_defs] valid_in_def[meta_defs] Concrete_def[meta_defs]

declare [[smt_solver = cvc4]]
declare [[simp_depth_limit = 10]] (* prevent the simplifier from running forever *)
declare [[unify_search_bound = 40]] (* prevent unification bound errors *)

subsection‹Auxiliary Lemmata›
text‹\label{TAO_Embedding_Aux}›
  
named_theorems meta_aux

declare makeκ_inverse[meta_aux] evalκ_inverse[meta_aux]
        make𝗈_inverse[meta_aux] eval𝗈_inverse[meta_aux]
        makeΠ1_inverse[meta_aux] evalΠ1_inverse[meta_aux]
        makeΠ2_inverse[meta_aux] evalΠ2_inverse[meta_aux]
        makeΠ3_inverse[meta_aux] evalΠ3_inverse[meta_aux]
lemma νυ_ων_is_ωυ[meta_aux]: "νυ (ων x) = ωυ x" by (simp add: νυ_def)
lemma rep_proper_id[meta_aux]: "rep (xP) = x"
  by (simp add: meta_aux νκ_def rep_def)
lemma νκ_proper[meta_aux]: "proper (xP)"
  by (simp add: meta_aux νκ_def proper_def)
lemma no_αω[meta_aux]: "¬(νυ (αν x) = ωυ y)" by (simp add: νυ_def)
lemma no_σω[meta_aux]: "¬(συ x = ωυ y)" by blast
lemma νυ_surj[meta_aux]: "surj νυ"
  using ασ_surj unfolding νυ_def surj_def
  by (metis ν.simps(5) ν.simps(6) υ.exhaust comp_apply)
lemma lambdaΠ1_aux[meta_aux]:
  "makeΠ1 (λu s w. x. νυ x = u  evalΠ1 F (νυ x) s w) = F"
  proof -
    have " u s w φ . ( x . νυ x = u  φ (νυ x) (s::j) (w::i))  φ u s w"
      using νυ_surj unfolding surj_def by metis
    thus ?thesis apply transfer by simp
  qed
lemma lambdaΠ2_aux[meta_aux]:
  "makeΠ2 (λu v s w. x . νυ x = u  ( y . νυ y = v  evalΠ2 F (νυ x) (νυ y) s w)) = F"
  proof -
    have " u v (s ::j) (w::i) φ .
      ( x . νυ x = u  ( y . νυ y = v  φ (νυ x) (νυ y) s w))
       φ u v s w"
      using νυ_surj unfolding surj_def by metis
    thus ?thesis apply transfer by simp
  qed
lemma lambdaΠ3_aux[meta_aux]:
  "makeΠ3 (λu v r s w. x. νυ x = u  (y. νυ y = v 
   (z. νυ z = r  evalΠ3 F (νυ x) (νυ y) (νυ z) s w))) = F"
  proof -
    have " u v r (s::j) (w::i) φ . x. νυ x = u  (y. νυ y = v
           (z. νυ z = r  φ (νυ x) (νυ y) (νυ z) s w)) = φ u v r s w"
      using νυ_surj unfolding surj_def by metis
    thus ?thesis apply transfer apply (rule ext)+ by metis
  qed
(*<*)
end
(*>*)

Theory TAO_2_Semantics

(*<*)
theory TAO_2_Semantics
imports 
  TAO_1_Embedding 
  "HOL-Eisbach.Eisbach"
begin
(*>*)

section‹Semantic Abstraction›
text‹\label{TAO_Semantics}›

subsection‹Semantics›
text‹\label{TAO_Semantics_Semantics}›

locale Semantics
begin
  named_theorems semantics

  subsubsection‹Semantic Domains›
  text‹\label{TAO_Semantics_Semantics_Domains}›
  type_synonym Rκ = "ν"
  type_synonym R0 = "jibool"
  type_synonym R1 = R0"
  type_synonym R2 = υR0"
  type_synonym R3 = υυR0"
  type_synonym W = i

  subsubsection‹Denotation Functions›
  text‹\label{TAO_Semantics_Semantics_Denotations}›

  lift_definition dκ :: Rκ option" is id .
  lift_definition d0 :: 0R0 option" is Some .
  lift_definition d1 :: 1R1 option" is Some .
  lift_definition d2 :: 2R2 option" is Some .
  lift_definition d3 :: 3R3 option" is Some .

  subsubsection‹Actual World›
  text‹\label{TAO_Semantics_Semantics_Actual_World}›
  definition w0 where "w0  dw"

  subsubsection‹Exemplification Extensions›
  text‹\label{TAO_Semantics_Semantics_Exemplification_Extensions}›

  definition ex0 :: "R0Wbool"
    where "ex0  λ F . F dj"
  definition ex1 :: "R1W(Rκ set)"
    where "ex1  λ F w . { x . F (νυ x) dj w }"
  definition ex2 :: "R2W((Rκ×Rκ) set)"
    where "ex2  λ F w . { (x,y) . F (νυ x) (νυ y) dj w }"
  definition ex3 :: "R3W((Rκ×Rκ×Rκ) set)"
    where "ex3  λ F w . { (x,y,z) . F (νυ x) (νυ y) (νυ z) dj w }"

  subsubsection‹Encoding Extensions›
  text‹\label{TAO_Semantics_Semantics_Encoding_Extension}›

  definition en :: "R1(Rκ set)"
    where "en  λ F . { x . case x of αν y  makeΠ1 (λ x . F x)  y
                                       | _  False }"

  subsubsection‹Collection of Semantic Definitions›
  text‹\label{TAO_Semantics_Semantics_Definitions}›

  named_theorems semantics_defs
  declare d0_def[semantics_defs] d1_def[semantics_defs]
          d2_def[semantics_defs] d3_def[semantics_defs]
          ex0_def[semantics_defs] ex1_def[semantics_defs]
          ex2_def[semantics_defs] ex3_def[semantics_defs]
          en_def[semantics_defs] dκ_def[semantics_defs]
          w0_def[semantics_defs]

  subsubsection‹Truth Conditions of Exemplification Formulas›
  text‹\label{TAO_Semantics_Semantics_Exemplification}›

  lemma T1_1[semantics]:
    "(w  F,x) = ( r o1 . Some r = d1 F  Some o1 = dκ x  o1  ex1 r w)"
    unfolding semantics_defs
    apply (simp add: meta_defs meta_aux rep_def proper_def)
    by (metis option.discI option.exhaust option.sel)

  lemma T1_2[semantics]:
    "(w  F,x,y) = ( r o1 o2 . Some r = d2 F  Some o1 = dκ x
                                Some o2 = dκ y  (o1, o2)  ex2 r w)"
    unfolding semantics_defs
    apply (simp add: meta_defs meta_aux rep_def proper_def)
    by (metis option.discI option.exhaust option.sel)

  lemma T1_3[semantics]:
    "(w  F,x,y,z) = ( 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 w)"
    unfolding semantics_defs
    apply (simp add: meta_defs meta_aux rep_def proper_def)
    by (metis option.discI option.exhaust option.sel)

  lemma T3[semantics]:
    "(w  F) = ( r . Some r = d0 F  ex0 r w)"
    unfolding semantics_defs
    by (simp add: meta_defs meta_aux)

  subsubsection‹Truth Conditions of Encoding Formulas›
  text‹\label{TAO_Semantics_Semantics_Encoding}›

  lemma T2[semantics]:
    "(w  x,F) = ( r o1 . Some r = d1 F  Some o1 = dκ x  o1  en r)"
    unfolding semantics_defs
    apply (simp add: meta_defs meta_aux rep_def proper_def split: ν.split)
    by (metis ν.exhaust ν.inject(2) ν.simps(4) νκ.rep_eq option.collapse
              option.discI rep.rep_eq rep_proper_id)

  subsubsection‹Truth Conditions of Complex Formulas›
  text‹\label{TAO_Semantics_Semantics_Complex_Formulas}›

  lemma T4[semantics]: "(w  ¬ψ) = (¬(w  ψ))"
    by (simp add: meta_defs meta_aux)

  lemma T5[semantics]: "(w  ψ  χ) = (¬(w  ψ)  (w  χ))"
    by (simp add: meta_defs meta_aux)

  lemma T6[semantics]: "(w  ψ) = ( v . (v  ψ))"
    by (simp add: meta_defs meta_aux)

  lemma T7[semantics]: "(w  𝒜ψ) = (dw  ψ)"
    by (simp add: meta_defs meta_aux)

  lemma T8_ν[semantics]: "(w  ν x. ψ x) = ( x . (w  ψ x))"
    by (simp add: meta_defs meta_aux)

  lemma T8_0[semantics]: "(w  0 x. ψ x) = ( x . (w  ψ x))"
    by (simp add: meta_defs meta_aux)

  lemma T8_1[semantics]: "(w  1 x. ψ x) = ( x . (w  ψ x))"
    by (simp add: meta_defs meta_aux)

  lemma T8_2[semantics]: "(w  2 x. ψ x) = ( x . (w  ψ x))"
    by (simp add: meta_defs meta_aux)

  lemma T8_3[semantics]: "(w  3 x. ψ x) = ( x . (w  ψ x))"
    by (simp add: meta_defs meta_aux)

  lemma T8_𝗈[semantics]: "(w  𝗈 x. ψ x) = ( x . (w  ψ x))"
    by (simp add: meta_defs meta_aux)

  subsubsection‹Denotations of Descriptions›
  text‹\label{TAO_Semantics_Semantics_Descriptions}›

  lemma D3[semantics]:
    "dκ (ιx . ψ x) = (if (x . (w0  ψ x)  ( y . (w0   ψ y)  y = x))
                      then (Some (THE x . (w0  ψ x))) else None)"
    unfolding semantics_defs
    by (auto simp: meta_defs meta_aux)

  subsubsection‹Denotations of Lambda Expressions›
  text‹\label{TAO_Semantics_Semantics_Lambda_Expressions}›

  lemma D4_1[semantics]: "d1 (λ x . F, xP) = d1 F"
    by (simp add: meta_defs meta_aux)

  lemma D4_2[semantics]: "d2 (λ2 (λ x y . F, xP, yP)) = d2 F"
    by (simp add: meta_defs meta_aux)

  lemma D4_3[semantics]: "d3 (λ3 (λ x y z . F, xP, yP, zP)) = d3 F"
    by (simp add: meta_defs meta_aux)

  lemma D5_1[semantics]:
    assumes "IsProperInX φ"
    shows " w o1 r . Some r = d1 (λ x . (φ (xP)))  Some o1 = dκ x
                       (o1  ex1 r w) = (w  φ x)"
    using assms unfolding IsProperInX_def semantics_defs
    by (auto simp: meta_defs meta_aux rep_def proper_def νκ.abs_eq)

  lemma D5_2[semantics]:
    assumes "IsProperInXY φ"
    shows " w o1 o2 r . Some r = d2 (λ2 (λ x y . φ (xP) (yP)))
                        Some o1 = dκ x  Some o2 = dκ y
                        ((o1,o2)  ex2 r w) = (w  φ x y)"
    using assms unfolding IsProperInXY_def semantics_defs
    by (auto simp: meta_defs meta_aux rep_def proper_def νκ.abs_eq)

  lemma D5_3[semantics]:
    assumes "IsProperInXYZ φ"
    shows " w o1 o2 o3 r . Some r = d3 (λ3 (λ x y z . φ (xP) (yP) (zP)))
                           Some o1 = dκ x  Some o2 = dκ y  Some o3 = dκ z
                           ((o1,o2,o3)  ex3 r w) = (w  φ x y z)"
    using assms unfolding IsProperInXYZ_def semantics_defs
    by (auto simp: meta_defs meta_aux rep_def proper_def νκ.abs_eq)

  lemma D6[semantics]: "( w r . Some r = d0 (λ0 φ)  ex0 r w = (w  φ))"
    by (auto simp: meta_defs meta_aux semantics_defs)

  subsubsection‹Auxiliary Lemmas›
  text‹\label{TAO_Semantics_Semantics_Auxiliary_Lemmata}›

  lemma propex0: " r . Some r = d0 F"
    unfolding d0_def by simp
  lemma propex1: " r . Some r = d1 F"
    unfolding d1_def by simp
  lemma propex2: " r . Some r = d2 F"
    unfolding d2_def by simp
  lemma propex3: " r . Some r = d3 F"
    unfolding d3_def by simp
  lemma dκ_proper: "dκ (uP) = Some u"
    unfolding dκ_def by (simp add: νκ_def meta_aux)
  lemma ConcretenessSemantics1:
    "Some r = d1 E!  ( w . ων x  ex1 r w)"
    unfolding semantics_defs apply transfer
    by (simp add: OrdinaryObjectsPossiblyConcreteAxiom νυ_ων_is_ωυ)
  lemma ConcretenessSemantics2:
    "Some r = d1 E!  (x  ex1 r w  (y. x = ων y))"
    unfolding semantics_defs apply transfer apply simp
    by (metis ν.exhaust υ.exhaust υ.simps(6) no_αω)
  lemma d0_inject: "x y. d0 x = d0 y  x = y"
    unfolding d0_def by (simp add: eval𝗈_inject)
  lemma d1_inject: "x y. d1 x = d1 y  x = y"
    unfolding d1_def by (simp add: evalΠ1_inject)
  lemma d2_inject: "x y. d2 x = d2 y  x = y"
    unfolding d2_def by (simp add: evalΠ2_inject)
  lemma d3_inject: "x y. d3 x = d3 y  x = y"
    unfolding d3_def by (simp add: evalΠ3_inject)
  lemma dκ_inject: "x y o1. Some o1 = dκ x  Some o1 = dκ y  x = y"
  proof -
    fix x :: κ and y :: κ and o1 :: ν
    assume "Some o1 = dκ x  Some o1 = dκ y"
    thus "x = y" apply transfer by auto
  qed
end

subsection‹Introduction Rules for Proper Maps›
text‹\label{TAO_Semantics_Proper}›

text‹
\begin{remark}
  Every map whose arguments only occur in exemplification
  expressions is proper.
\end{remark}
›

named_theorems IsProper_intros

lemma IsProperInX_intro[IsProper_intros]:
  "IsProperInX (λ x . χ
    ― ‹one place:› (λ F . F,x)
    ― ‹two place:› (λ F . F,x,x) (λ F a . F,x,a) (λ F a . F,a,x)
    ― ‹three place three x›:› (λ F . F,x,x,x)
    ― ‹three place two x›:› (λ F a . F,x,x,a) (λ F a . F,x,a,x)
                            (λ F a . F,a,x,x)
    ― ‹three place one x›:› (λ F a b. F,x,a,b) (λ F a b. F,a,x,b)
                            (λ F a b . F,a,b,x))"
  unfolding IsProperInX_def
  by (auto simp: meta_defs meta_aux)

lemma IsProperInXY_intro[IsProper_intros]:
  "IsProperInXY (λ x y . χ
    ― ‹only x›
      ― ‹one place:› (λ F . F,x)
      ― ‹two place:› (λ F . F,x,x) (λ F a . F,x,a) (λ F a . F,a,x)
      ― ‹three place three x›:› (λ F . F,x,x,x)
      ― ‹three place two x›:› (λ F a . F,x,x,a) (λ F a . F,x,a,x)
                              (λ F a . F,a,x,x)
      ― ‹three place one x›:› (λ F a b. F,x,a,b) (λ F a b. F,a,x,b)
                              (λ F a b . F,a,b,x)
    ― ‹only y›
      ― ‹one place:› (λ F . F,y)
      ― ‹two place:› (λ F . F,y,y) (λ F a . F,y,a) (λ F a . F,a,y)
      ― ‹three place three y›:› (λ F . F,y,y,y)
      ― ‹three place two y›:› (λ F a . F,y,y,a) (λ F a . F,y,a,y)
                              (λ F a . F,a,y,y)
      ― ‹three place one y›:› (λ F a b. F,y,a,b) (λ F a b. F,a,y,b)
                              (λ F a b . F,a,b,y)
    ― ‹x› and y›
      ― ‹two place:› (λ F . F,x,y) (λ F . F,y,x)
      ― ‹three place (x,y)›:› (λ F a . F,x,y,a) (λ F a . F,x,a,y)
                              (λ F a . F,a,x,y)
      ― ‹three place (y,x)›:› (λ F a . F,y,x,a) (λ F a . F,y,a,x)
                              (λ F a . F,a,y,x)
      ― ‹three place (x,x,y)›:› (λ F . F,x,x,y) (λ F . F,x,y,x)
                                (λ F . F,y,x,x)
      ― ‹three place (x,y,y)›:› (λ F . F,x,y,y) (λ F . F,y,x,y)
                                (λ F . F,y,y,x)
      ― ‹three place (x,x,x)›:› (λ F . F,x,x,x)
      ― ‹three place (y,y,y)›:› (λ F . F,y,y,y))"
  unfolding IsProperInXY_def by (auto simp: meta_defs meta_aux)

lemma IsProperInXYZ_intro[IsProper_intros]:
  "IsProperInXYZ (λ x y z . χ
    ― ‹only x›
      ― ‹one place:› (λ F . F,x)
      ― ‹two place:› (λ F . F,x,x) (λ F a . F,x,a) (λ F a . F,a,x)
      ― ‹three place three x›:› (λ F . F,x,x,x)
      ― ‹three place two x›:› (λ F a . F,x,x,a) (λ F a . F,x,a,x)
                              (λ F a . F,a,x,x)
      ― ‹three place one x›:› (λ F a b. F,x,a,b) (λ F a b. F,a,x,b)
                              (λ F a b . F,a,b,x)
    ― ‹only y›
      ― ‹one place:› (λ F . F,y)
      ― ‹two place:› (λ F . F,y,y) (λ F a . F,y,a) (λ F a . F,a,y)
      ― ‹three place three y›:› (λ F . F,y,y,y)
      ― ‹three place two y›:› (λ F a . F,y,y,a) (λ F a . F,y,a,y)
                              (λ F a . F,a,y,y)
      ― ‹three place one y›:› (λ F a b. F,y,a,b) (λ F a b. F,a,y,b)
                              (λ F a b . F,a,b,y)
    ― ‹only z›
      ― ‹one place:› (λ F . F,z)
      ― ‹two place:› (λ F . F,z,z) (λ F a . F,z,a) (λ F a . F,a,z)
      ― ‹three place three z›:› (λ F . F,z,z,z)
      ― ‹three place two z›:› (λ F a . F,z,z,a) (λ F a . F,z,a,z)
                              (λ F a . F,a,z,z)
      ― ‹three place one z›:› (λ F a b. F,z,a,b) (λ F a b. F,a,z,b)
                              (λ F a b . F,a,b,z)
    ― ‹x› and y›
      ― ‹two place:› (λ F . F,x,y) (λ F . F,y,x)
      ― ‹three place (x,y)›:› (λ F a . F,x,y,a) (λ F a . F,x,a,y)
                              (λ F a . F,a,x,y)
      ― ‹three place (y,x)›:› (λ F a . F,y,x,a) (λ F a . F,y,a,x)
                              (λ F a . F,a,y,x)
      ― ‹three place (x,x,y)›:› (λ F . F,x,x,y) (λ F . F,x,y,x)
                                (λ F . F,y,x,x)
      ― ‹three place (x,y,y)›:› (λ F . F,x,y,y) (λ F . F,y,x,y)
                                (λ F . F,y,y,x)
      ― ‹three place (x,x,x)›:› (λ F . F,x,x,x)
      ― ‹three place (y,y,y)›:› (λ F . F,y,y,y)
    ― ‹x› and z›
      ― ‹two place:› (λ F . F,x,z) (λ F . F,z,x)
      ― ‹three place (x,z)›:› (λ F a . F,x,z,a) (λ F a . F,x,a,z)
                              (λ F a . F,a,x,z)
      ― ‹three place (z,x)›:› (λ F a . F,z,x,a) (λ F a . F,z,a,x)
                              (λ F a . F,a,z,x)
      ― ‹three place (x,x,z)›:› (λ F . F,x,x,z) (λ F . F,x,z,x)
                                (λ F . F,z,x,x)
      ― ‹three place (x,z,z)›:› (λ F . F,x,z,z) (λ F . F,z,x,z)
                                (λ F . F,z,z,x)
      ― ‹three place (x,x,x)›:› (λ F . F,x,x,x)
      ― ‹three place (z,z,z)›:› (λ F . F,z,z,z)
    ― ‹y› and z›
      ― ‹two place:› (λ F . F,y,z) (λ F . F,z,y)
      ― ‹three place (y,z)›:› (λ F a . F,y,z,a) (λ F a . F,y,a,z)
                              (λ F a . F,a,y,z)
      ― ‹three place (z,y)›:› (λ F a . F,z,y,a) (λ F a . F,z,a,y)
                              (λ F a . F,a,z,y)
      ― ‹three place (y,y,z)›:› (λ F . F,y,y,z) (λ F . F,y,z,y)
                                (λ F . F,z,y,y)
      ― ‹three place (y,z,z)›:› (λ F . F,y,z,z) (λ F . F,z,y,z)
                                (λ F . F,z,z,y)
      ― ‹three place (y,y,y)›:› (λ F . F,y,y,y)
      ― ‹three place (z,z,z)›:› (λ F . F,z,z,z)
    ― ‹x y z›
      ― ‹three place (x,…)›:› (λ F . F,x,y,z) (λ F . F,x,z,y)
      ― ‹three place (y,…)›:› (λ F . F,y,x,z) (λ F . F,y,z,x)
      ― ‹three place (z,…)›:› (λ F . F,z,x,y) (λ F . F,z,y,x))"
  unfolding IsProperInXYZ_def
  by (auto simp: meta_defs meta_aux)    

method show_proper = (fast intro: IsProper_intros)

subsection‹Validity Syntax›
text‹\label{TAO_Semantics_Validity}›

(* disable list syntax [] to replace it with truth evaluation *)
(*<*) no_syntax "_list" :: "args  'a list" ("[(_)]") (*>*) 
(*<*) no_syntax "__listcompr" :: "args  'a list" ("[(_)]") (*>*) 

abbreviation validity_in :: "𝗈ibool" ("[_ in _]" [1]) where
  "validity_in  λ φ v . v  φ"
definition actual_validity :: "𝗈bool" ("[_]" [1]) where
  "actual_validity  λ φ . dw  φ"
definition necessary_validity :: "𝗈bool" ("□[_]" [1]) where
  "necessary_validity  λ φ .  v . (v  φ)"

(*<*)
end
(*>*)

Theory TAO_3_Quantifiable

(*<*)
theory TAO_3_Quantifiable
imports TAO_2_Semantics
begin
(*>*)

section‹General Quantification›
text‹\label{TAO_Quantifiable}›

text‹
\begin{remark}
  In order to define general quantifiers that can act
  on individuals as well as relations a type class
  is introduced which assumes the semantics of the all quantifier.
  This type class is then instantiated for individuals and
  relations.
\end{remark}
›

subsection‹Type Class›
text‹\label{TAO_Quantifiable_Class}›

class quantifiable = fixes forall :: "('a𝗈)𝗈" (binder "" [8] 9)
  assumes quantifiable_T8: "(w  ( x . ψ x)) = ( x . (w  (ψ x)))"
begin
end

lemma (in Semantics) T8: shows "(w   x . ψ x) = ( x . (w  ψ x))"
  using quantifiable_T8 .

subsection‹Instantiations›
text‹\label{TAO_Quantifiable_Instantiations}›

instantiation ν :: quantifiable
begin
  definition forall_ν :: "(ν𝗈)𝗈" where "forall_ν  forallν"
  instance proof
    fix w :: i and ψ :: 𝗈"
    show "(w  x. ψ x) = (x. (w  ψ x))"
      unfolding forall_ν_def using Semantics.T8_ν .
  qed
end

instantiation 𝗈 :: quantifiable
begin
  definition forall_𝗈 :: "(𝗈𝗈)𝗈" where "forall_𝗈  forall𝗈"
  instance proof
    fix w :: i and ψ :: "𝗈𝗈"
    show "(w  x. ψ x) = (x. (w  ψ x))"
      unfolding forall_𝗈_def using Semantics.T8_𝗈 .
  qed
end

instantiation Π1 :: quantifiable
begin
  definition forall_Π1 :: "(Π1𝗈)𝗈" where "forall_Π1  forall1"
  instance proof
    fix w :: i and ψ :: 1𝗈"
    show "(w  x. ψ x) = (x. (w  ψ x))"
      unfolding forall_Π1_def using Semantics.T8_1 .
  qed
end

instantiation Π2 :: quantifiable
begin
  definition forall_Π2 :: "(Π2𝗈)𝗈" where "forall_Π2  forall2"
  instance proof
    fix w :: i and ψ :: 2𝗈"
    show "(w  x. ψ x) = (x. (w  ψ x))"
      unfolding forall_Π2_def using Semantics.T8_2 .
  qed
end

instantiation Π3 :: quantifiable
begin
  definition forall_Π3 :: "(Π3𝗈)𝗈" where "forall_Π3  forall3"
  instance proof
    fix w :: i and ψ :: 3𝗈"
    show "(w  x. ψ x) = (x. (w  ψ x))"
      unfolding forall_Π3_def using Semantics.T8_3 .
  qed
end

(*<*)
end
(*>*)

Theory TAO_4_BasicDefinitions

(*<*)
theory TAO_4_BasicDefinitions
imports TAO_3_Quantifiable
begin
(*>*)

section‹Basic Definitions›
text‹\label{TAO_BasicDefinitions}›

subsection‹Derived Connectives›
text‹\label{TAO_BasicDefinitions_DerivedConnectives}›

definition conj::"𝗈𝗈𝗈" (infixl "&" 53) where
  "conj  λ x y . ¬(x  ¬y)"
definition disj::"𝗈𝗈𝗈" (infixl "" 52) where
  "disj  λ x y . ¬x  y"
definition equiv::"𝗈𝗈𝗈" (infixl "" 51) where
  "equiv  λ x y . (x  y) & (y  x)"
definition diamond::"𝗈𝗈" ("_" [62] 63) where
  "diamond  λ φ . ¬¬φ"
definition (in quantifiable) exists :: "('a𝗈)𝗈" (binder "" [8] 9) where
    "exists  λ φ . ¬( x . ¬φ x)"

named_theorems conn_defs
declare diamond_def[conn_defs] conj_def[conn_defs]
        disj_def[conn_defs] equiv_def[conn_defs]
        exists_def[conn_defs]

subsection‹Abstract and Ordinary Objects›
text‹\label{TAO_BasicDefinitions_AbstractOrdinary}›

definition Ordinary :: 1" ("O!") where "Ordinary  λx. E!,xP"
definition Abstract :: 1" ("A!") where "Abstract  λx. ¬E!,xP"

subsection‹Identity Definitions›
text‹\label{TAO_BasicDefinitions_Identity}›

definition basic_identityE::2" where
  "basic_identityE  λ2 (λ x y . O!,xP & O!,yP
                         & ( F. F,xP  F,yP))"

definition basic_identityE_infix::κ𝗈" (infixl "=E" 63) where
  "x =E y  basic_identityE, x, y"

definition basic_identityκ (infixl "=κ" 63) where
  "basic_identityκ  λ x y . (x =E y)  A!,x & A!,y
                             & ( F. x,F  y,F)"

definition basic_identity1 (infixl "=1" 63) where
  "basic_identity1  λ F G . ( x. xP,F  xP,G)"

definition basic_identity2 :: 2Π2𝗈" (infixl "=2" 63) where
  "basic_identity2  λ F G .   x. ((λy. F,xP,yP) =1 (λy. G,xP,yP))
                                 & ((λy. F,yP,xP) =1 (λy. G,yP,xP))"

definition basic_identity3::3Π3𝗈" (infixl "=3" 63) where
  "basic_identity3  λ F G .  x y. (λz. F,zP,xP,yP) =1 (λz. G,zP,xP,yP)
                                  & (λz. F,xP,zP,yP) =1 (λz. G,xP,zP,yP)
                                  & (λz. F,xP,yP,zP) =1 (λz. G,xP,yP,zP)"

definition basic_identity0::"𝗈𝗈𝗈" (infixl "=0" 63) where
  "basic_identity0  λ F G . (λy. F) =1 (λy. G)"

(*<*)
end
(*>*)

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, 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 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, 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 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
(*>*)

Theory TAO_6_Identifiable

(*<*)
theory TAO_6_Identifiable
imports TAO_5_MetaSolver
begin
(*>*)

section‹General Identity›
text‹\label{TAO_Identifiable}›

text‹
\begin{remark}
  In order to define a general identity symbol that can act
  on all types of terms a type class is introduced
  which assumes the substitution property which
  is needed to derive the corresponding axiom.
  This type class is instantiated for all relation types, individual terms
  and individuals.
\end{remark}
›

subsection‹Type Classes›
text‹\label{TAO_Identifiable_Class}›

class identifiable =
fixes identity :: "'a'a𝗈" (infixl "=" 63)
assumes l_identity:
  "w  x = y  w  φ x  w  φ y"
begin
  abbreviation notequal (infixl "" 63) where
    "notequal  λ x y . ¬(x = y)"
end

class quantifiable_and_identifiable = quantifiable + identifiable
begin
  definition exists_unique::"('a𝗈)𝗈" (binder "!" [8] 9) where
    "exists_unique  λ φ .  α . φ α & (β. φ β  β = α)"
  
  declare exists_unique_def[conn_defs]
end

subsection‹Instantiations›
text‹\label{TAO_Identifiable_Instantiation}›

instantiation κ :: identifiable
begin
  definition identity_κ where "identity_κ  basic_identityκ"
  instance proof
    fix x y :: κ and w φ
    show "[x = y in w]  [φ x in w]  [φ y in w]"
      unfolding identity_κ_def
      using MetaSolver.Eqκ_prop ..
  qed
end

instantiation ν :: identifiable
begin
  definition identity_ν where "identity_ν  λ x y . xP = yP"
  instance proof
    fix α :: ν and β :: ν and v φ
    assume "v  α = β"
    hence "v  αP = βP"
      unfolding identity_ν_def by auto
    hence "φ.(v  φ (αP))  (v  φ (βP))"
      using l_identity by auto
    hence "(v  φ (rep (αP)))  (v  φ (rep (βP)))"
      by meson
    thus "(v  φ α)  (v  φ β)"
      by (simp only: rep_proper_id)
  qed
end

instantiation Π1 :: identifiable
begin
  definition identity_Π1 where "identity_Π1  basic_identity1"
  instance proof
    fix F G :: Π1 and w φ
    show "(w  F = G)  (w  φ F)  (w  φ G)"
      unfolding identity_Π1_def using MetaSolver.Eq1_prop ..
  qed
end

instantiation Π2 :: identifiable
begin
  definition identity_Π2 where "identity_Π2  basic_identity2"
  instance proof
    fix F G :: Π2 and w φ
    show "(w  F = G)  (w  φ F)  (w  φ G)"
      unfolding identity_Π2_def using MetaSolver.Eq2_prop ..
  qed
end

instantiation Π3 :: identifiable
begin
  definition identity_Π3 where "identity_Π3  basic_identity3"
  instance proof
    fix F G :: Π3 and w φ
    show "(w  F = G)  (w  φ F)  (w  φ G)"
      unfolding identity_Π3_def using MetaSolver.Eq3_prop ..
  qed
end

instantiation 𝗈 :: identifiable
begin
  definition identity_𝗈 where "identity_𝗈  basic_identity0"
  instance proof
    fix F G :: 𝗈 and w φ
    show "(w  F = G)  (w  φ F)  (w  φ G)"
      unfolding identity_𝗈_def using MetaSolver.Eq0_prop ..
  qed
end

instance ν :: quantifiable_and_identifiable ..
instance Π1 :: quantifiable_and_identifiable ..
instance Π2 :: quantifiable_and_identifiable ..
instance Π3 :: quantifiable_and_identifiable ..
instance 𝗈 :: quantifiable_and_identifiable ..

subsection‹New Identity Definitions›
text‹\label{TAO_Identifiable_Definitions}›

text‹
\begin{remark}
  The basic definitions of identity use type specific quantifiers
  and identity symbols. Equivalent definitions that
  use the general identity symbol and general quantifiers are provided.
\end{remark}
›

named_theorems identity_defs
lemma identityE_def[identity_defs]:
  "basic_identityE  λ2 (λx y. O!,xP & O!,yP & (F. F,xP  F,yP))"
  unfolding basic_identityE_def forall_Π1_def by simp
lemma identityE_infix_def[identity_defs]:
  "x =E y  basic_identityE,x,y" using basic_identityE_infix_def .
lemma identityκ_def[identity_defs]:
  "(=)  λx y. x =E y  A!,x & A!,y & ( F. x,F  y,F)"
  unfolding identity_κ_def basic_identityκ_def forall_Π1_def by simp
lemma identityν_def[identity_defs]:
  "(=)  λx y. (xP) =E (yP)  A!,xP & A!,yP & ( F. xP,F  yP,F)"
  unfolding identity_ν_def identityκ_def by simp
lemma identity1_def[identity_defs]:
  "(=)  λF G. ( x . xP,F  xP,G)"
  unfolding identity_Π1_def basic_identity1_def forall_ν_def by simp
lemma identity2_def[identity_defs]:
  "(=)  λF G.  x. (λy. F,xP,yP) = (λy. G,xP,yP)
                    & (λy. F,yP,xP) = (λy. G,yP,xP)"
  unfolding identity_Π2_def identity_Π1_def basic_identity2_def forall_ν_def by simp
lemma identity3_def[identity_defs]:
  "(=)  λF G.  x y. (λz. F,zP,xP,yP) = (λz. G,zP,xP,yP)
                      & (λz. F,xP,zP,yP) = (λz. G,xP,zP,yP)
                      & (λz. F,xP,yP,zP) = (λz. G,xP,yP,zP)"
  unfolding identity_Π3_def identity_Π1_def basic_identity3_def forall_ν_def by simp
lemma identity𝗈_def[identity_defs]: "(=)  λF G. (λy. F) = (λy. G)"
  unfolding identity_𝗈_def identity_Π1_def basic_identity0_def by simp

(*<*)
end
(*>*)

Theory TAO_7_Axioms

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

section‹The Axioms of PLM›
text‹\label{TAO_Axioms}›

text‹
\begin{remark}
  The axioms of PLM can now be derived from the Semantics
  and the model structure.
\end{remark}
›

(* TODO: why is this needed again here? The syntax should already
         have been disabled in TAO_Semantics. *)
(* disable list syntax [] to replace it with truth evaluation *)
(*<*) no_syntax "_list" :: "args  'a list" ("[(_)]") (*>*) 
(*<*) no_syntax "__listcompr" :: "args  'a list" ("[(_)]") (*>*) 

locale Axioms
begin
  interpretation MetaSolver .
  interpretation Semantics .
  named_theorems axiom

text‹
\begin{remark}
  The special syntax [[_]]› is introduced for stating the axioms.
  Modally-fragile axioms are stated with the syntax for actual validity [_]›.
\end{remark}
›

  definition axiom :: "𝗈bool" ("[[_]]") where "axiom  λ φ .  v . [φ in v]"

  method axiom_meta_solver = ((((unfold axiom_def)?, rule allI) | (unfold actual_validity_def)?), meta_solver,
                              (simp | (auto; fail))?)

subsection‹Closures›
text‹\label{TAO_Axioms_Closures}›

  text‹
\begin{remark}
  Rules resembling the concepts of closures in PLM are derived. Theorem attributes are introduced
  to aid in the instantiation of the axioms.
\end{remark}
›

  lemma axiom_instance[axiom]: "[[φ]]  [φ in v]"
    unfolding axiom_def by simp
  lemma closures_universal[axiom]: "(x.[[φ x]])  [[ x. φ x]]"
    by axiom_meta_solver
  lemma closures_actualization[axiom]: "[[φ]]  [[𝒜 φ]]"
    by axiom_meta_solver
  lemma closures_necessitation[axiom]: "[[φ]]  [[ φ]]"
    by axiom_meta_solver
  lemma necessitation_averse_axiom_instance[axiom]: "[φ]  [φ in dw]"
    by axiom_meta_solver
  lemma necessitation_averse_closures_universal[axiom]: "(x.[φ x])  [ x. φ x]"
    by axiom_meta_solver

  attribute_setup axiom_instance = ‹
    Scan.succeed (Thm.rule_attribute [] 
      (fn _ => fn thm => thm RS @{thm axiom_instance}))

  attribute_setup necessitation_averse_axiom_instance = ‹
    Scan.succeed (Thm.rule_attribute [] 
      (fn _ => fn thm => thm RS @{thm necessitation_averse_axiom_instance}))

  attribute_setup axiom_necessitation = ‹
    Scan.succeed (Thm.rule_attribute [] 
      (fn _ => fn thm => thm RS @{thm closures_necessitation}))

  attribute_setup axiom_actualization = ‹
    Scan.succeed (Thm.rule_attribute [] 
      (fn _ => fn thm => thm RS @{thm closures_actualization}))

  attribute_setup axiom_universal = ‹
    Scan.succeed (Thm.rule_attribute [] 
      (fn _ => fn thm => thm RS @{thm closures_universal}))

subsection‹Axioms for Negations and Conditionals›
text‹\label{TAO_Axioms_NegationsAndConditionals}›

  lemma pl_1[axiom]:
    "[[φ  (ψ  φ)]]"
    by axiom_meta_solver
  lemma pl_2[axiom]:
    "[[(φ  (ψ  χ))  ((φ  ψ)  (φ  χ))]]"
    by axiom_meta_solver
  lemma pl_3[axiom]:
    "[[(¬φ  ¬ψ)  ((¬φ  ψ)  φ)]]"
    by axiom_meta_solver

subsection‹Axioms of Identity›
text‹\label{TAO_Axioms_Identity}›

  lemma l_identity[axiom]:
    "[[α = β  (φ α  φ β)]]"
    using l_identity apply - by axiom_meta_solver

subsection‹Axioms of Quantification›
text‹\label{TAO_Axioms_Quantification}›

  lemma cqt_1[axiom]:
    "[[( α. φ α)  φ α]]"
    by axiom_meta_solver
  lemma cqt_1_κ[axiom]:
    "[[( α. φ (αP))  (( β . (βP) = α)  φ α)]]"
    proof -
      {
        fix v
        assume 1: "[( α. φ (αP)) in v]"
        assume "[( β . (βP) = α) in v]"
        then obtain β where 2:
          "[(βP) = α in v]" by (rule ExERule)
        hence "[φ (βP) in v]" using 1 AllE by fast
        hence "[φ α in v]"
          using l_identity[where φ=φ, axiom_instance]
          ImplS 2 by simp
      }
      thus "[[( α. φ (αP))  (( β . (βP) = α)  φ α)]]"
        unfolding axiom_def using ImplI by blast
    qed
  lemma cqt_3[axiom]:
    "[[(α. φ α  ψ α)  ((α. φ α)  (α. ψ α))]]"
    by axiom_meta_solver
  lemma cqt_4[axiom]:
    "[[φ  (α. φ)]]"
    by axiom_meta_solver

  inductive SimpleExOrEnc
    where "SimpleExOrEnc (λ x . F,x)"
        | "SimpleExOrEnc (λ x . F,x,y)"
        | "SimpleExOrEnc (λ x . F,y,x)"
        | "SimpleExOrEnc (λ x . F,x,y,z)"
        | "SimpleExOrEnc (λ x . F,y,x,z)"
        | "SimpleExOrEnc (λ x . F,y,z,x)"
        | "SimpleExOrEnc (λ x . x,F)"

  lemma cqt_5[axiom]:
    assumes "SimpleExOrEnc ψ"
    shows "[[(ψ (ιx . φ x))  ( α. (αP) = (ιx . φ x))]]"
    proof -
      have " w . ([(ψ (ιx . φ x)) in w]  ( o1 . Some o1 = dκ (ιx . φ x)))"
        using assms apply induct by (meta_solver;metis)+
     thus ?thesis
      apply - unfolding identity_κ_def
      apply axiom_meta_solver
      using dκ_proper by auto
    qed

  lemma cqt_5_mod[axiom]:
    assumes "SimpleExOrEnc ψ"
    shows "[[ψ τ  ( α . (αP) = τ)]]"
    proof -
      have " w . ([(ψ τ) in w]  ( o1 . Some o1 = dκ τ))"
        using assms apply induct by (meta_solver;metis)+
      thus ?thesis
        apply - unfolding identity_κ_def
        apply axiom_meta_solver
        using dκ_proper by auto
    qed

subsection‹Axioms of Actuality›
text‹\label{TAO_Axioms_Actuality}›

  lemma logic_actual[axiom]: "[(𝒜φ)  φ]"
    by axiom_meta_solver
  lemma "[[(𝒜φ)  φ]]"
    nitpick[user_axioms, expect = genuine, card = 1, card i = 2]
    oops ― ‹Counter-model by nitpick›

  lemma logic_actual_nec_1[axiom]:
    "[[𝒜¬φ  ¬𝒜φ]]"
    by axiom_meta_solver
  lemma logic_actual_nec_2[axiom]:
    "[[(𝒜(φ  ψ))  (𝒜φ  𝒜ψ)]]"
    by axiom_meta_solver
  lemma logic_actual_nec_3[axiom]:
    "[[𝒜(α. φ α)  (α. 𝒜(φ α))]]"
    by axiom_meta_solver
  lemma logic_actual_nec_4[axiom]:
    "[[𝒜φ  𝒜𝒜φ]]"
    by axiom_meta_solver

subsection‹Axioms of Necessity›
text‹\label{TAO_Axioms_Necessity}›

  lemma qml_1[axiom]:
    "[[(φ  ψ)  (φ  ψ)]]"
    by axiom_meta_solver
  lemma qml_2[axiom]:
    "[[φ  φ]]"
    by axiom_meta_solver
  lemma qml_3[axiom]:
    "[[φ  φ]]"
    by axiom_meta_solver
  lemma qml_4[axiom]:
    "[[(x. E!,xP & ¬E!,xP) & ¬(x. E!,xP & ¬E!,xP)]]"
     unfolding axiom_def
     using PossiblyContingentObjectExistsAxiom
           PossiblyNoContingentObjectExistsAxiom
     apply (simp add: meta_defs meta_aux conn_defs forall_ν_def
                 split: ν.split υ.split)
     by (metis νυ_ων_is_ωυ υ.distinct(1) υ.inject(1))

subsection‹Axioms of Necessity and Actuality›
text‹\label{TAO_Axioms_NecessityAndActuality}›

  lemma qml_act_1[axiom]:
    "[[𝒜φ  𝒜φ]]"
    by axiom_meta_solver
  lemma qml_act_2[axiom]:
    "[[φ  𝒜(φ)]]"
    by axiom_meta_solver

subsection‹Axioms of Descriptions›
text‹\label{TAO_Axioms_Descriptions}›

  lemma descriptions[axiom]:
    "[[xP = (ιx. φ x)  (z.(𝒜(φ z)  z = x))]]"
    unfolding axiom_def
    proof (rule allI, rule EquivI; rule)
      fix v
      assume "[xP = (ιx. φ x) in v]"
      moreover hence 1:
        "o1 o2. Some o1 = dκ (xP)  Some o2 = dκ (ιx. φ x)  o1 = o2"
        apply - unfolding identity_κ_def by meta_solver
      then obtain o1 o2 where 2:
        "Some o1 = dκ (xP)  Some o2 = dκ (ιx. φ x)  o1 = o2"
        by auto
      hence 3:
        "( x .((w0  φ x)  (y. (w0  φ y)  y = x)))
          dκ (ιx. φ x) = Some (THE x. (w0  φ x))"
        using D3 by (metis option.distinct(1))
      then obtain X where 4:
        "((w0  φ X)  (y. (w0  φ y)  y = X))"
        by auto
      moreover have "o1 = (THE x. (w0  φ x))"
        using 2 3 by auto
      ultimately have 5: "X = o1"
        by (metis (mono_tags) theI)
      have " z . [𝒜φ z in v] = [(zP) = (xP) in v]"
      proof
        fix z
        have "[𝒜φ z in v]  [(zP) = (xP) in v]"
          unfolding identity_κ_def apply meta_solver
          using 4 5 2 dκ_proper w0_def by auto
        moreover have "[(zP) = (xP) in v]  [𝒜φ z in v]"
          unfolding identity_κ_def apply meta_solver
          using 2 4 5 
          by (simp add: dκ_proper w0_def)
        ultimately show "[𝒜φ z in v] = [(zP) = (xP) in v]"
          by auto
      qed
      thus "[z. 𝒜φ z  (z) = (x) in v]"
        unfolding identity_ν_def
        by (simp add: AllI EquivS)
    next
      fix v
      assume "[z. 𝒜φ z  (z) = (x) in v]"
      hence "z. (dw  φ z) = (o1 o2. Some o1 = dκ (zP)
                 Some o2 = dκ (xP)  o1 = o2)"
        apply - unfolding identity_ν_def identity_κ_def by meta_solver
      hence " z . (dw  φ z) = (z = x)"
        by (simp add: dκ_proper)
      moreover hence "x = (THE z . (dw  φ z))" by simp
      ultimately have "xP = (ιx. φ x)"
        using D3 dκ_inject dκ_proper w0_def by presburger
      thus "[xP = (ιx. φ x) in v]"
        using EqκS unfolding identity_κ_def by (metis dκ_proper)
    qed

subsection‹Axioms for Complex Relation Terms›
text‹\label{TAO_Axioms_ComplexRelationTerms}›

  lemma lambda_predicates_1[axiom]:
    "(λ x . φ x) = (λ y . φ y)" ..

  lemma lambda_predicates_2_1[axiom]:
    assumes "IsProperInX φ"
    shows "[[λ x . φ (xP), xP  φ (xP)]]"
    apply axiom_meta_solver
    using D5_1[OF assms] dκ_proper propex1
    by metis

  lemma lambda_predicates_2_2[axiom]:
    assumes "IsProperInXY φ"
    shows "[[(λ2 (λ x y . φ (xP) (yP))), xP, yP  φ (xP) (yP)]]"
    apply axiom_meta_solver
    using D5_2[OF assms] dκ_proper propex2
    by metis

  lemma lambda_predicates_2_3[axiom]:
    assumes "IsProperInXYZ φ"
    shows "[[(λ3 (λ x y z . φ (xP) (yP) (zP))),xP,yP,zP  φ (xP) (yP) (zP)]]"
    proof -
      have "[[(λ3 (λ x y z . φ (xP) (yP) (zP))),xP,yP,zP  φ (xP) (yP) (zP)]]"
        apply axiom_meta_solver using D5_3[OF assms] by auto
      moreover have
        "[[φ (xP) (yP) (zP)  (λ3 (λ x y z . φ (xP) (yP) (zP))),xP,yP,zP]]"
        apply axiom_meta_solver
        using D5_3[OF assms] dκ_proper propex3
        by (metis (no_types, lifting))
      ultimately show ?thesis unfolding axiom_def equiv_def ConjS by blast
    qed

  lemma lambda_predicates_3_0[axiom]:
    "[[(λ0 φ) = φ]]"
    unfolding identity_defs
    apply axiom_meta_solver
    by (simp add: meta_defs meta_aux)

  lemma lambda_predicates_3_1[axiom]:
    "[[(λ x . F, xP) = F]]"
    unfolding axiom_def
    apply (rule allI)
    unfolding identity_Π1_def apply (rule Eq1I)
    using D4_1 d1_inject by simp

  lemma lambda_predicates_3_2[axiom]:
    "[[(λ2 (λ x y . F, xP, yP)) = F]]"
    unfolding axiom_def
    apply (rule allI)
    unfolding identity_Π2_def apply (rule Eq2I)
    using D4_2 d2_inject by simp

  lemma lambda_predicates_3_3[axiom]:
    "[[(λ3 (λ x y z . F, xP, yP, zP)) = F]]"
    unfolding axiom_def
    apply (rule allI)
    unfolding identity_Π3_def apply (rule Eq3I)
    using D4_3 d3_inject by simp

  lemma lambda_predicates_4_0[axiom]:
    assumes "x.[(𝒜(φ x  ψ x)) in v]"
    shows "[[(λ0 (χ (ιx. φ x)) = λ0 (χ (ιx. ψ x)))]]"
    unfolding axiom_def identity_𝗈_def apply - apply (rule allI; rule Eq0I)
    using TheEqI[OF assms[THEN ActualE, THEN EquivE]] by auto

  lemma lambda_predicates_4_1[axiom]:
    assumes "x.[(𝒜(φ x  ψ x)) in v]"
    shows "[[((λ x . χ (ιx. φ x) x) = (λ x . χ (ιx. ψ x) x))]]"
    unfolding axiom_def identity_Π1_def apply - apply (rule allI; rule Eq1I)
    using TheEqI[OF assms[THEN ActualE, THEN EquivE]] by auto

  lemma lambda_predicates_4_2[axiom]:
    assumes "x.[(𝒜(φ x  ψ x)) in v]"
    shows "[[((λ2 (λ x y . χ (ιx. φ x) x y)) = (λ2 (λ x y . χ (ιx. ψ x) x y)))]]"
    unfolding axiom_def identity_Π2_def apply - apply (rule allI; rule Eq2I)
    using TheEqI[OF assms[THEN ActualE, THEN EquivE]] by auto

  lemma lambda_predicates_4_3[axiom]:
    assumes "x.[(𝒜(φ x  ψ x)) in v]"
    shows "[[(λ3 (λ x y z . χ (ιx. φ x) x y z)) = (λ3 (λ x y z . χ (ιx. ψ x) x y z))]]"
    unfolding axiom_def identity_Π3_def apply - apply (rule allI; rule Eq3I)
    using TheEqI[OF assms[THEN ActualE, THEN EquivE]] by auto

subsection‹Axioms of Encoding›
text‹\label{TAO_Axioms_Encoding}›

  lemma encoding[axiom]:
    "[[x,F  x,F]]"
    by axiom_meta_solver
  lemma nocoder[axiom]:
    "[[O!,x  ¬( F . x,F)]]"
    unfolding axiom_def
    apply (rule allI, rule ImplI, subst (asm) OrdS)
    apply meta_solver unfolding en_def
    by (metis ν.simps(5) mem_Collect_eq option.sel)
  lemma A_objects[axiom]:
    "[[x. A!,xP & ( F . (xP,F  φ F))]]"
    unfolding axiom_def
    proof (rule allI, rule ExIRule)
      fix v
      let ?x = "αν { F . [φ F in v]}"
      have "[A!,?xP in v]" by (simp add: AbsS dκ_proper)
      moreover have "[(F. ?xP,F  φ F) in v]"
        apply meta_solver unfolding en_def
        using d1.rep_eq dκ_def dκ_proper evalΠ1_inverse by auto
      ultimately show "[A!,?xP & (F. ?xP,F  φ F) in v]"
        by (simp only: ConjS)
    qed

end

(*<*)
end
(*>*)

Theory TAO_8_Definitions

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

section‹Definitions›
text‹\label{TAO_Definitions}›

subsection‹Property Negations›

consts propnot :: "'a'a" ("_-" [90] 90)
overloading propnot0  "propnot :: Π0Π0"
            propnot1  "propnot :: Π1Π1"
            propnot2  "propnot :: Π2Π2"
            propnot3  "propnot :: Π3Π3"
begin
  definition propnot0 :: 0Π0" where
    "propnot0  λ p . λ0 (¬p)"
  definition propnot1 where
    "propnot1  λ F . λ x . ¬F, xP"
  definition propnot2 where
    "propnot2  λ F . λ2 (λ x y . ¬F, xP, yP)"
  definition propnot3 where
    "propnot3  λ F . λ3 (λ x y z . ¬F, xP, yP, zP)"
end

named_theorems propnot_defs
declare propnot0_def[propnot_defs] propnot1_def[propnot_defs]
        propnot2_def[propnot_defs] propnot3_def[propnot_defs]

subsection‹Noncontingent and Contingent Relations›

consts Necessary :: "'a𝗈"
overloading Necessary0  "Necessary :: Π0𝗈"
            Necessary1  "Necessary :: Π1𝗈"
            Necessary2  "Necessary :: Π2𝗈"
            Necessary3  "Necessary :: Π3𝗈"
begin
  definition Necessary0 where
    "Necessary0  λ p . p"
  definition Necessary1 :: 1𝗈" where
    "Necessary1  λ F . ( x . F,xP)"
  definition Necessary2 where
    "Necessary2  λ F . ( x y . F,xP,yP)"
  definition Necessary3 where
    "Necessary3  λ F . ( x y z . F,xP,yP,zP)"
end

named_theorems Necessary_defs
declare Necessary0_def[Necessary_defs] Necessary1_def[Necessary_defs]
        Necessary2_def[Necessary_defs] Necessary3_def[Necessary_defs]

consts Impossible :: "'a𝗈"
overloading Impossible0  "Impossible :: Π0𝗈"
            Impossible1  "Impossible :: Π1𝗈"
            Impossible2  "Impossible :: Π2𝗈"
            Impossible3  "Impossible :: Π3𝗈"
begin
  definition Impossible0 where
    "Impossible0  λ p . ¬p"
  definition Impossible1 where
    "Impossible1  λ F . ( x. ¬F,xP)"
  definition Impossible2 where
    "Impossible2  λ F . ( x y. ¬F,xP,yP)"
  definition Impossible3 where
    "Impossible3  λ F . ( x y z. ¬F,xP,yP,zP)"
end

named_theorems Impossible_defs
declare Impossible0_def[Impossible_defs] Impossible1_def[Impossible_defs]
        Impossible2_def[Impossible_defs] Impossible3_def[Impossible_defs]

definition NonContingent where
  "NonContingent  λ F . (Necessary F)  (Impossible F)"
definition Contingent where
  "Contingent  λ F .  ¬(Necessary F  Impossible F)"

definition ContingentlyTrue :: "𝗈𝗈" where
  "ContingentlyTrue  λ p . p & ¬p"
definition ContingentlyFalse :: "𝗈𝗈" where
  "ContingentlyFalse  λ p . ¬p & p"

definition WeaklyContingent where
  "WeaklyContingent  λ F . Contingent F & ( x. F,xP  F,xP)"

subsection‹Null and Universal Objects›

definition Null :: 𝗈" where
  "Null  λ x . A!,x & ¬( F . x, F)"
definition Universal :: 𝗈" where
  "Universal  λ x . A!,x & ( F . x, F)"

definition NullObject :: "κ" ("a") where
  "NullObject  (ιx . Null (xP))"
definition UniversalObject :: "κ" ("aV") where
  "UniversalObject  (ιx . Universal (xP))"

subsection‹Propositional Properties›

definition Propositional where
  "Propositional F    p . F = (λ x . p)"

subsection‹Indiscriminate Properties›

definition Indiscriminate :: 1𝗈" where
  "Indiscriminate  λ F . (( x . F,xP)  ( x . F,xP))"

subsection‹Miscellaneous›

definition not_identicalE :: κ𝗈" (infixl "E" 63)
  where "not_identicalE  λ x y . (λ2 (λ x y . xP =E yP))-, x, y"

(*<*)
end
(*>*)

Theory TAO_9_PLM

(*<*)
theory TAO_9_PLM
imports 
  TAO_8_Definitions 
  "HOL-Eisbach.Eisbach_Tools"
begin
(*>*)

section‹The Deductive System PLM›
text‹\label{TAO_PLM}›

declare meta_defs[no_atp] meta_aux[no_atp]

locale PLM = Axioms
begin

subsection‹Automatic Solver›
text‹\label{TAO_PLM_Solver}›

  named_theorems PLM
  named_theorems PLM_intro
  named_theorems PLM_elim
  named_theorems PLM_dest
  named_theorems PLM_subst

  method PLM_solver declares PLM_intro PLM_elim PLM_subst PLM_dest PLM
    = ((assumption | (match axiom in A: "[[φ]]" for φ  fact A[axiom_instance])
        | fact PLM | rule PLM_intro | subst PLM_subst | subst (asm) PLM_subst
        | fastforce | safe | drule PLM_dest | erule PLM_elim); (PLM_solver)?)

subsection‹Modus Ponens›
text‹\label{TAO_PLM_ModusPonens}›

  lemma modus_ponens[PLM]:
    "[φ in v]; [φ  ψ in v]  [ψ in v]"
    by (simp add: Semantics.T5)

subsection‹Axioms›
text‹\label{TAO_PLM_Axioms}›

  interpretation Axioms .
  declare axiom[PLM]
  declare conn_defs[PLM]

subsection‹(Modally Strict) Proofs and Derivations›
text‹\label{TAO_PLM_ProofsAndDerivations}›

  lemma vdash_properties_6[no_atp]:
    "[φ in v]; [φ  ψ in v]  [ψ in v]"
    using modus_ponens .
  lemma vdash_properties_9[PLM]:
    "[φ in v]  [ψ  φ in v]"
    using modus_ponens pl_1[axiom_instance] by blast
  lemma vdash_properties_10[PLM]:
    "[φ  ψ in v]  ([φ in v]  [ψ in v])"
    using vdash_properties_6 .

  attribute_setup deduction = ‹
    Scan.succeed (Thm.rule_attribute [] 
      (fn _ => fn thm => thm RS @{thm vdash_properties_10}))

subsection‹GEN and RN›
text‹\label{TAO_PLM_GEN_RN}›

  lemma rule_gen[PLM]:
    "α . [φ α in v]  [α . φ α in v]"
    by (simp add: Semantics.T8)

  lemma RN_2[PLM]:
    "( v . [ψ in v]  [φ in v])  ([ψ in v]  [φ in v])"
    by (simp add: Semantics.T6)

  lemma RN[PLM]:
    "( v . [φ in v])  [φ in v]"
    using qml_3[axiom_necessitation, axiom_instance] RN_2 by blast

subsection‹Negations and Conditionals›
text‹\label{TAO_PLM_NegationsAndConditionals}›

  lemma if_p_then_p[PLM]:
    "[φ  φ in v]"
    using pl_1 pl_2 vdash_properties_10 axiom_instance by blast

  lemma deduction_theorem[PLM,PLM_intro]:
    "[φ in v]  [ψ in v]  [φ  ψ in v]"
    by (simp add: Semantics.T5)
  lemmas CP = deduction_theorem

  lemma ded_thm_cor_3[PLM]:
    "[φ  ψ in v]; [ψ  χ in v]  [φ  χ in v]"
    by (meson pl_2 vdash_properties_10 vdash_properties_9 axiom_instance)
  lemma ded_thm_cor_4[PLM]:
    "[φ  (ψ  χ) in v]; [ψ in v]  [φ  χ in v]"
    by (meson pl_2 vdash_properties_10 vdash_properties_9 axiom_instance)

  lemma useful_tautologies_1[PLM]:
    "[¬¬φ  φ in v]"
    by (meson pl_1 pl_3 ded_thm_cor_3 ded_thm_cor_4 axiom_instance)
  lemma useful_tautologies_2[PLM]:
    "[φ  ¬¬φ in v]"
    by (meson pl_1 pl_3 ded_thm_cor_3 useful_tautologies_1
              vdash_properties_10 axiom_instance)
  lemma useful_tautologies_3[PLM]:
    "[¬φ  (φ  ψ) in v]"
    by (meson pl_1 pl_2 pl_3 ded_thm_cor_3 ded_thm_cor_4 axiom_instance)
  lemma useful_tautologies_4[PLM]:
    "[(¬ψ  ¬φ)  (φ  ψ) in v]"
    by (meson pl_1 pl_2 pl_3 ded_thm_cor_3 ded_thm_cor_4 axiom_instance)
  lemma useful_tautologies_5[PLM]:
    "[(φ  ψ)  (¬ψ  ¬φ) in v]"
    by (metis CP useful_tautologies_4 vdash_properties_10)
  lemma useful_tautologies_6[PLM]:
    "[(φ  ¬ψ)  (ψ  ¬φ) in v]"
    by (metis CP useful_tautologies_4 vdash_properties_10)
  lemma useful_tautologies_7[PLM]:
    "[(¬φ  ψ)  (¬ψ  φ) in v]"
    using ded_thm_cor_3 useful_tautologies_4 useful_tautologies_5
          useful_tautologies_6 by blast
  lemma useful_tautologies_8[PLM]:
    "[φ  (¬ψ  ¬(φ  ψ)) in v]"
    by (meson ded_thm_cor_3 CP useful_tautologies_5)
  lemma useful_tautologies_9[PLM]:
    "[(φ  ψ)  ((¬φ  ψ)  ψ) in v]"
    by (metis CP useful_tautologies_4 vdash_properties_10)
  lemma useful_tautologies_10[PLM]:
    "[(φ  ¬ψ)  ((φ  ψ)  ¬φ) in v]"
    by (metis ded_thm_cor_3 CP useful_tautologies_6)

  lemma modus_tollens_1[PLM]:
    "[φ  ψ in v]; [¬ψ in v]  [¬φ in v]"
    by (metis ded_thm_cor_3 ded_thm_cor_4 useful_tautologies_3
              useful_tautologies_7 vdash_properties_10)
  lemma modus_tollens_2[PLM]:
    "[φ  ¬ψ in v]; [ψ in v]  [¬φ in v]"
    using modus_tollens_1 useful_tautologies_2
          vdash_properties_10 by blast

  lemma contraposition_1[PLM]:
    "[φ  ψ in v] = [¬ψ  ¬φ in v]"
    using useful_tautologies_4 useful_tautologies_5
          vdash_properties_10 by blast
  lemma contraposition_2[PLM]:
    "[φ  ¬ψ in v] = [ψ  ¬φ in v]"
    using contraposition_1 ded_thm_cor_3
          useful_tautologies_1 by blast

  lemma reductio_aa_1[PLM]:
    "[¬φ in v]  [¬ψ in v]; [¬φ in v]  [ψ in v]  [φ in v]"
    using CP modus_tollens_2 useful_tautologies_1
          vdash_properties_10 by blast
  lemma reductio_aa_2[PLM]:
    "[φ in v]  [¬ψ in v]; [φ in v]  [ψ in v]  [¬φ in v]"
    by (meson contraposition_1 reductio_aa_1)
  lemma reductio_aa_3[PLM]:
    "[¬φ  ¬ψ in v]; [¬φ  ψ in v]  [φ in v]"
    using reductio_aa_1 vdash_properties_10 by blast
  lemma reductio_aa_4[PLM]:
    "[φ  ¬ψ in v]; [φ  ψ in v]  [¬φ in v]"
    using reductio_aa_2 vdash_properties_10 by blast

  lemma raa_cor_1[PLM]:
    "[φ in v]; [¬ψ in v]  [¬φ in v]  ([φ in v]  [ψ in v])"
    using reductio_aa_1 vdash_properties_9 by blast
  lemma raa_cor_2[PLM]:
    "[¬φ in v]; [¬ψ in v]  [φ in v]  ([¬φ in v]  [ψ in v])"
    using reductio_aa_1 vdash_properties_9 by blast
  lemma raa_cor_3[PLM]:
    "[φ in v]; [¬ψ  ¬φ in v]  ([φ in v]  [ψ in v])"
    using raa_cor_1 vdash_properties_10 by blast
  lemma raa_cor_4[PLM]:
    "[¬φ in v]; [¬ψ  φ in v]  ([¬φ in v]  [ψ in v])"
    using raa_cor_2 vdash_properties_10 by blast

text‹
\begin{remark}
  In contrast to PLM the classical introduction and elimination rules are proven
  before the tautologies. The statements proven so far are sufficient
  for the proofs and using the derived rules the tautologies can be derived
  automatically.
\end{remark}
›

  lemma intro_elim_1[PLM]:
    "[φ in v]; [ψ in v]  [φ & ψ in v]"
    unfolding conj_def using ded_thm_cor_4 if_p_then_p modus_tollens_2 by blast
  lemmas "&I" = intro_elim_1
  lemma intro_elim_2_a[PLM]:
    "[φ & ψ in v]  [φ in v]"
    unfolding conj_def using CP reductio_aa_1 by blast
  lemma intro_elim_2_b[PLM]:
    "[φ & ψ in v]  [ψ in v]"
    unfolding conj_def using pl_1 CP reductio_aa_1 axiom_instance by blast
  lemmas "&E" = intro_elim_2_a intro_elim_2_b
  lemma intro_elim_3_a[PLM]:
    "[φ in v]  [φ  ψ in v]"
    unfolding disj_def using ded_thm_cor_4 useful_tautologies_3 by blast
  lemma intro_elim_3_b[PLM]:
    "[ψ in v]  [φ  ψ in v]"
    by (simp only: disj_def vdash_properties_9)
  lemmas "I" = intro_elim_3_a intro_elim_3_b
  lemma intro_elim_4_a[PLM]:
    "[φ  ψ in v]; [φ  χ in v]; [ψ  χ in v]  [χ in v]"
    unfolding disj_def by (meson reductio_aa_2 vdash_properties_10)
  lemma intro_elim_4_b[PLM]:
    "[φ  ψ in v]; [¬φ in v]  [ψ in v]"
    unfolding disj_def using vdash_properties_10 by blast
  lemma intro_elim_4_c[PLM]:
    "[φ  ψ in v]; [¬ψ in v]  [φ in v]"
    unfolding disj_def using raa_cor_2 vdash_properties_10 by blast
  lemma intro_elim_4_d[PLM]:
    "[φ  ψ in v]; [φ  χ in v]; [ψ  Θ in v]  [χ  Θ in v]"
    unfolding disj_def using contraposition_1 ded_thm_cor_3 by blast
  lemma intro_elim_4_e[PLM]:
    "[φ  ψ in v]; [φ  χ in v]; [ψ  Θ in v]  [χ  Θ in v]"
    unfolding equiv_def using "&E"(1) intro_elim_4_d by blast
  lemmas "E" = intro_elim_4_a intro_elim_4_b intro_elim_4_c intro_elim_4_d
  lemma intro_elim_5[PLM]:
    "[φ  ψ in v]; [ψ  φ in v]  [φ  ψ in v]"
    by (simp only: equiv_def "&I")
  lemmas "I" = intro_elim_5
  lemma intro_elim_6_a[PLM]:
    "[φ  ψ in v]; [φ in v]  [ψ in v]"
    unfolding equiv_def using "&E"(1) vdash_properties_10 by blast
  lemma intro_elim_6_b[PLM]:
    "[φ  ψ in v]; [ψ in v]  [φ in v]"
    unfolding equiv_def using "&E"(2) vdash_properties_10 by blast
  lemma intro_elim_6_c[PLM]:
    "[φ  ψ in v]; [¬φ in v]  [¬ψ in v]"
    unfolding equiv_def using "&E"(2) modus_tollens_1 by blast
  lemma intro_elim_6_d[PLM]:
    "[φ  ψ in v]; [¬ψ in v]  [¬φ in v]"
    unfolding equiv_def using "&E"(1) modus_tollens_1 by blast
  lemma intro_elim_6_e[PLM]:
    "[φ  ψ in v]; [ψ  χ in v]  [φ  χ in v]"
    by (metis equiv_def ded_thm_cor_3 "&E" "I")
  lemma intro_elim_6_f[PLM]:
    "[φ  ψ in v]; [φ  χ in v]  [χ  ψ in v]"
    by (metis equiv_def ded_thm_cor_3 "&E" "I")
  lemmas "E" = intro_elim_6_a intro_elim_6_b intro_elim_6_c
                intro_elim_6_d intro_elim_6_e intro_elim_6_f
  lemma intro_elim_7[PLM]:
    "[φ in v]  [¬¬φ in v]"
    using if_p_then_p modus_tollens_2 by blast
  lemmas "¬¬I" = intro_elim_7
  lemma intro_elim_8[PLM]:
    "[¬¬φ in v]  [φ in v]"
    using if_p_then_p raa_cor_2 by blast
  lemmas "¬¬E" = intro_elim_8

  context
  begin
    private lemma NotNotI[PLM_intro]:
      "[φ in v]  [¬(¬φ) in v]"
      by (simp add: "¬¬I")
    private lemma NotNotD[PLM_dest]:
      "[¬(¬φ) in v]  [φ in v]"
      using "¬¬E" by blast

    private lemma ImplI[PLM_intro]:
      "([φ in v]  [ψ in v])  [φ  ψ in v]"
      using CP .
    private lemma ImplE[PLM_elim, PLM_dest]:
      "[φ  ψ in v]  ([φ in v]  [ψ in v])"
      using modus_ponens .
    private lemma ImplS[PLM_subst]:
      "[φ  ψ in v] = ([φ in v]  [ψ in v])"
      using ImplI ImplE by blast

    private lemma NotI[PLM_intro]:
      "([φ in v]  (ψ .[ψ in v]))  [¬φ in v]"
      using CP modus_tollens_2 by blast
    private lemma NotE[PLM_elim,PLM_dest]:
      "[¬φ in v]  ([φ in v]  (ψ .[ψ in v]))"
      using "I"(2) "E"(3) by blast
    private lemma NotS[PLM_subst]:
      "[¬φ in v] = ([φ in v]  (ψ .[ψ in v]))"
      using NotI NotE by blast

    private lemma ConjI[PLM_intro]:
      "[φ in v]; [ψ in v]  [φ & ψ in v]"
      using "&I" by blast
    private lemma ConjE[PLM_elim,PLM_dest]:
      "[φ & ψ in v]  (([φ in v]  [ψ in v]))"
      using CP "&E" by blast
    private lemma ConjS[PLM_subst]:
      "[φ & ψ in v] = (([φ in v]  [ψ in v]))"
      using ConjI ConjE by blast

    private lemma DisjI[PLM_intro]:
      "[φ in v]  [ψ in v]  [φ  ψ in v]"
      using "I" by blast
    private lemma DisjE[PLM_elim,PLM_dest]:
      "[φ  ψ in v]  [φ in v]  [ψ in v]"
      using CP "E"(1) by blast
    private lemma DisjS[PLM_subst]:
      "[φ  ψ in v] = ([φ in v]  [ψ in v])"
      using DisjI DisjE by blast

    private lemma EquivI[PLM_intro]:
      "[φ in v]  [ψ in v];[ψ in v]  [φ in v]  [φ  ψ in v]"
      using CP "I" by blast
    private lemma EquivE[PLM_elim,PLM_dest]:
      "[φ  ψ in v]  (([φ in v]  [ψ in v])  ([ψ in v]  [φ in v]))"
      using "E"(1) "E"(2) by blast
    private lemma EquivS[PLM_subst]:
      "[φ  ψ in v] = ([φ in v]  [ψ in v])"
      using EquivI EquivE by blast

    private lemma NotOrD[PLM_dest]:
      "¬[φ  ψ in v]  ¬[φ in v]  ¬[ψ in v]"
      using "I" by blast
    private lemma NotAndD[PLM_dest]:
      "¬[φ & ψ in v]  ¬[φ in v]  ¬[ψ in v]"
      using "&I" by blast
    private lemma NotEquivD[PLM_dest]:
      "¬[φ  ψ in v]  [φ in v]  [ψ in v]"
      by (meson NotI contraposition_1 "I" vdash_properties_9)

    private lemma BoxI[PLM_intro]:
      "( v . [φ in v])  [φ in v]"
      using RN by blast
    private lemma NotBoxD[PLM_dest]:
      "¬[φ in v]  ( v . ¬[φ in v])"
      using BoxI by blast

    private lemma AllI[PLM_intro]:
      "( x . [φ x in v])  [ x . φ x in v]"
      using rule_gen by blast
    lemma NotAllD[PLM_dest]:
      "¬[ x . φ x in v]  ( x . ¬[φ x in v])"
      using AllI by fastforce
  end

  lemma oth_class_taut_1_a[PLM]:
    "[¬(φ & ¬φ) in v]"
    by PLM_solver
  lemma oth_class_taut_1_b[PLM]:
    "[¬(φ  ¬φ) in v]"
    by PLM_solver
  lemma oth_class_taut_2[PLM]:
    "[φ  ¬φ in v]"
    by PLM_solver
  lemma oth_class_taut_3_a[PLM]:
    "[(φ & φ)  φ in v]"
    by PLM_solver
  lemma oth_class_taut_3_b[PLM]:
    "[(φ & ψ)  (ψ & φ) in v]"
    by PLM_solver
  lemma oth_class_taut_3_c[PLM]:
    "[(φ & (ψ & χ))  ((φ & ψ) & χ) in v]"
    by PLM_solver
  lemma oth_class_taut_3_d[PLM]:
    "[(φ  φ)  φ in v]"
    by PLM_solver
  lemma oth_class_taut_3_e[PLM]:
    "[(φ  ψ)  (ψ  φ) in v]"
    by PLM_solver
  lemma oth_class_taut_3_f[PLM]:
    "[(φ  (ψ  χ))  ((φ  ψ)  χ) in v]"
    by PLM_solver
  lemma oth_class_taut_3_g[PLM]:
    "[(φ  ψ)  (ψ  φ) in v]"
    by PLM_solver
  lemma oth_class_taut_3_i[PLM]:
    "[(φ  (ψ  χ))  ((φ  ψ)  χ) in v]"
    by PLM_solver
  lemma oth_class_taut_4_a[PLM]:
    "[φ  φ in v]"
    by PLM_solver
  lemma oth_class_taut_4_b[PLM]:
    "[φ  ¬¬φ in v]"
    by PLM_solver
  lemma oth_class_taut_5_a[PLM]:
    "[(φ  ψ)  ¬(φ & ¬ψ) in v]"
    by PLM_solver
  lemma oth_class_taut_5_b[PLM]:
    "[¬(φ  ψ)  (φ & ¬ψ) in v]"
    by PLM_solver
  lemma oth_class_taut_5_c[PLM]:
    "[(φ  ψ)  ((ψ  χ)  (φ  χ)) in v]"
    by PLM_solver
  lemma oth_class_taut_5_d[PLM]:
    "[(φ  ψ)  (¬φ  ¬ψ) in v]"
    by PLM_solver
  lemma oth_class_taut_5_e[PLM]:
    "[(φ  ψ)  ((φ  χ)  (ψ  χ)) in v]"
    by PLM_solver
  lemma oth_class_taut_5_f[PLM]:
    "[(φ  ψ)  ((χ  φ)  (χ  ψ)) in v]"
    by PLM_solver
  lemma oth_class_taut_5_g[PLM]:
    "[(φ  ψ)  ((φ  χ)  (ψ  χ)) in v]"
    by PLM_solver
  lemma oth_class_taut_5_h[PLM]:
    "[(φ  ψ)  ((χ  φ)  (χ  ψ)) in v]"
    by PLM_solver
  lemma oth_class_taut_5_i[PLM]:
    "[(φ  ψ)  ((φ & ψ)  (¬φ & ¬ψ)) in v]"
    by PLM_solver
  lemma oth_class_taut_5_j[PLM]:
    "[(¬(φ  ψ))  ((φ & ¬ψ)  (¬φ & ψ)) in v]"
    by PLM_solver
  lemma oth_class_taut_5_k[PLM]:
    "[(φ  ψ)  (¬φ  ψ) in v]"
    by PLM_solver

  lemma oth_class_taut_6_a[PLM]:
    "[(φ & ψ)  ¬(¬φ  ¬ψ) in v]"
    by PLM_solver
  lemma oth_class_taut_6_b[PLM]:
    "[(φ  ψ)  ¬(¬φ & ¬ψ) in v]"
    by PLM_solver
  lemma oth_class_taut_6_c[PLM]:
    "[¬(φ & ψ)  (¬φ  ¬ψ) in v]"
    by PLM_solver
  lemma oth_class_taut_6_d[PLM]:
    "[¬(φ  ψ)  (¬φ & ¬ψ) in v]"
    by PLM_solver

  lemma oth_class_taut_7_a[PLM]:
    "[(φ & (ψ  χ))  ((φ & ψ)  (φ & χ)) in v]"
    by PLM_solver
  lemma oth_class_taut_7_b[PLM]:
    "[(φ  (ψ & χ))  ((φ  ψ) & (φ  χ)) in v]"
    by PLM_solver

  lemma oth_class_taut_8_a[PLM]:
    "[((φ & ψ)  χ)  (φ  (ψ  χ)) in v]"
    by PLM_solver
  lemma oth_class_taut_8_b[PLM]:
    "[(φ  (ψ  χ))  ((φ & ψ)  χ) in v]"
    by PLM_solver

  lemma oth_class_taut_9_a[PLM]:
    "[(φ & ψ)  φ in v]"
    by PLM_solver
  lemma oth_class_taut_9_b[PLM]:
    "[(φ & ψ)  ψ in v]"
    by PLM_solver

  lemma oth_class_taut_10_a[PLM]:
    "[φ  (ψ  (φ & ψ)) in v]"
    by PLM_solver
  lemma oth_class_taut_10_b[PLM]:
    "[(φ  (ψ  χ))  (ψ  (φ  χ)) in v]"
    by PLM_solver
  lemma oth_class_taut_10_c[PLM]:
    "[(φ  ψ)  ((φ  χ)  (φ  (ψ & χ))) in v]"
    by PLM_solver
  lemma oth_class_taut_10_d[PLM]:
    "[(φ  χ)  ((ψ  χ)  ((φ  ψ)  χ)) in v]"
    by PLM_solver
  lemma oth_class_taut_10_e[PLM]:
    "[(φ  ψ)  ((χ  Θ)  ((φ & χ)  (ψ & Θ))) in v]"
    by PLM_solver
  lemma oth_class_taut_10_f[PLM]:
    "[((φ & ψ)  (φ & χ))  (φ  (ψ  χ)) in v]"
    by PLM_solver
  lemma oth_class_taut_10_g[PLM]:
    "[((φ & ψ)  (χ & ψ))  (ψ  (φ  χ)) in v]"
    by PLM_solver

  attribute_setup equiv_lr = ‹
    Scan.succeed (Thm.rule_attribute [] 
      (fn _ => fn thm => thm RS @{thm "E"(1)}))

  attribute_setup equiv_rl = ‹
    Scan.succeed (Thm.rule_attribute [] 
      (fn _ => fn thm => thm RS @{thm "E"(2)}))

  attribute_setup equiv_sym = ‹
    Scan.succeed (Thm.rule_attribute [] 
      (fn _ => fn thm => thm RS @{thm oth_class_taut_3_g[equiv_lr]}))

  attribute_setup conj1 = ‹
    Scan.succeed (Thm.rule_attribute [] 
      (fn _ => fn thm => thm RS @{thm "&E"(1)}))

  attribute_setup conj2 = ‹
    Scan.succeed (Thm.rule_attribute [] 
      (fn _ => fn thm => thm RS @{thm "&E"(2)}))

  attribute_setup conj_sym = ‹
    Scan.succeed (Thm.rule_attribute [] 
      (fn _ => fn thm => thm RS @{thm oth_class_taut_3_b[equiv_lr]}))

  
subsection‹Identity›
text‹\label{TAO_PLM_Identity}›

  lemma id_eq_prop_prop_1[PLM]:
    "[(F::Π1) = F in v]"
    unfolding identity_defs by PLM_solver 
  lemma id_eq_prop_prop_2[PLM]:
    "[((F::Π1) = G)  (G = F) in v]"
    by (meson id_eq_prop_prop_1 CP ded_thm_cor_3 l_identity[axiom_instance])
  lemma id_eq_prop_prop_3[PLM]:
    "[(((F::Π1) = G) & (G = H))  (F = H) in v]"
    by (metis l_identity[axiom_instance] ded_thm_cor_4 CP "&E")
  lemma id_eq_prop_prop_4_a[PLM]:
    "[(F::Π2) = F in v]"
    unfolding identity_defs by PLM_solver
  lemma id_eq_prop_prop_4_b[PLM]:
    "[(F::Π3) = F in v]"
    unfolding identity_defs by PLM_solver
  lemma id_eq_prop_prop_5_a[PLM]:
    "[((F::Π2) = G)  (G = F) in v]"
    by (meson id_eq_prop_prop_4_a CP ded_thm_cor_3 l_identity[axiom_instance])
  lemma id_eq_prop_prop_5_b[PLM]:
    "[((F::Π3) = G)  (G = F) in v]"
    by (meson id_eq_prop_prop_4_b CP ded_thm_cor_3 l_identity[axiom_instance])
  lemma id_eq_prop_prop_6_a[PLM]:
    "[(((F::Π2) = G) & (G = H))  (F = H) in v]"
    by (metis l_identity[axiom_instance] ded_thm_cor_4 CP "&E")
  lemma id_eq_prop_prop_6_b[PLM]:
    "[(((F::Π3) = G) & (G = H))  (F = H) in v]"
    by (metis l_identity[axiom_instance] ded_thm_cor_4 CP "&E")
  lemma id_eq_prop_prop_7[PLM]:
    "[(p::Π0) = p in v]"
    unfolding identity_defs by PLM_solver
  lemma id_eq_prop_prop_7_b[PLM]:
    "[(p::𝗈) = p in v]"
    unfolding identity_defs by PLM_solver
  lemma id_eq_prop_prop_8[PLM]:
    "[((p::Π0) = q)  (q = p) in v]"
    by (meson id_eq_prop_prop_7 CP ded_thm_cor_3 l_identity[axiom_instance])
  lemma id_eq_prop_prop_8_b[PLM]:
    "[((p::𝗈) = q)  (q = p) in v]"
    by (meson id_eq_prop_prop_7_b CP ded_thm_cor_3 l_identity[axiom_instance])
  lemma id_eq_prop_prop_9[PLM]:
    "[(((p::Π0) = q) & (q = r))  (p = r) in v]"
    by (metis l_identity[axiom_instance] ded_thm_cor_4 CP "&E")
  lemma id_eq_prop_prop_9_b[PLM]:
    "[(((p::𝗈) = q) & (q = r))  (p = r) in v]"
    by (metis l_identity[axiom_instance] ded_thm_cor_4 CP "&E")

  lemma eq_E_simple_1[PLM]:
    "[(x =E y)  (O!,x & O!,y & (F . F,x  F,y)) in v]"
    proof (rule "I"; rule CP)
      assume 1: "[x =E y in v]"
      have "[ x y . ((xP) =E (yP))  (O!,xP & O!,yP
              & (F . F,xP  F,yP)) in v]"
        unfolding identityE_infix_def identityE_def
        apply (rule lambda_predicates_2_2[axiom_universal, axiom_universal, axiom_instance])
        by show_proper
      moreover have "[ α . (αP) = x in v]"
        apply (rule cqt_5_mod[where ψ="λ x . x =E y", axiom_instance,deduction])
        unfolding identityE_infix_def
        apply (rule SimpleExOrEnc.intros)
        using 1 unfolding identityE_infix_def by auto
      moreover have "[ β . (βP) = y in v]"
        apply (rule cqt_5_mod[where ψ="λ y . x =E y",axiom_instance,deduction])
        unfolding identityE_infix_def
        apply (rule SimpleExOrEnc.intros) using 1
        unfolding identityE_infix_def by auto
      ultimately have "[(x =E y)  (O!,x & O!,y
                        & (F . F,x  F,y)) in v]"
        using cqt_1_κ[axiom_instance,deduction, deduction] by meson
      thus "[(O!,x & O!,y & (F . F,x  F,y)) in v]"
        using 1 "E"(1) by blast
    next
      assume 1: "[O!,x & O!,y & (F. F,x  F,y) in v]"
      have "[ x y . ((xP) =E (yP))  (O!,xP & O!,yP
              & (F . F,xP  F,yP)) in v]"
        unfolding identityE_def identityE_infix_def
        apply (rule lambda_predicates_2_2[axiom_universal, axiom_universal, axiom_instance])
        by show_proper
      moreover have "[ α . (αP) = x in v]"
        apply (rule cqt_5_mod[where ψ="λ x . O!,x",axiom_instance,deduction])
        apply (rule SimpleExOrEnc.intros)
        using 1[conj1,conj1] by auto
      moreover have "[ β . (βP) = y in v]"
        apply (rule cqt_5_mod[where ψ="λ y . O!,y",axiom_instance,deduction])
         apply (rule SimpleExOrEnc.intros)
        using 1[conj1,conj2] by auto
      ultimately have "[(x =E y)  (O!,x & O!,y
                        & (F . F,x  F,y)) in v]"
      using cqt_1_κ[axiom_instance,deduction, deduction] by meson
      thus "[(x =E y) in v]" using 1 "E"(2) by blast
    qed
  lemma eq_E_simple_2[PLM]:
    "[(x =E y)  (x = y) in v]"
    unfolding identity_defs by PLM_solver
  lemma eq_E_simple_3[PLM]:
    "[(x = y)  ((O!,x & O!,y & (F . F,x  F,y))
                (A!,x & A!,y & (F. x,F  y,F))) in v]"
    using eq_E_simple_1
    apply - unfolding identity_defs
    by PLM_solver

  lemma id_eq_obj_1[PLM]: "[(xP) = (xP) in v]"
    proof -
      have "[(E!, xP)  (¬E!, xP) in v]"
        using PLM.oth_class_taut_2 by simp
      hence "[(E!, xP) in v]  [(¬E!, xP) in v]"
        using CP "E"(1) by blast
      moreover {
        assume "[(E!, xP) in v]"
        hence "[λx. E!,xP,xP in v]"
          apply (rule lambda_predicates_2_1[axiom_instance, equiv_rl, rotated])
          by show_proper
        hence "[λx. E!,xP,xP & λx. E!,xP,xP
                & (F. F,xP  F,xP) in v]"
          apply - by PLM_solver
        hence "[(xP) =E (xP) in v]"
          using eq_E_simple_1[equiv_rl] unfolding Ordinary_def by fast
      }
      moreover {
        assume "[(¬E!, xP) in v]"
        hence "[λx. ¬E!,xP,xP in v]"
          apply (rule lambda_predicates_2_1[axiom_instance, equiv_rl, rotated])
          by show_proper
        hence "[λx. ¬E!,xP,xP & λx. ¬E!,xP,xP
                & (F. xP,F  xP,F) in v]"
          apply - by PLM_solver
      }
      ultimately show ?thesis unfolding identity_defs Ordinary_def Abstract_def
        using "I" by blast
    qed
  lemma id_eq_obj_2[PLM]:
    "[((xP) = (yP))  ((yP) = (xP)) in v]"
    by (meson l_identity[axiom_instance] id_eq_obj_1 CP ded_thm_cor_3)
  lemma id_eq_obj_3[PLM]:
    "[((xP) = (yP)) & ((yP) = (zP))  ((xP) = (zP)) in v]"
    by (metis l_identity[axiom_instance] ded_thm_cor_4 CP "&E")
end

text‹
\begin{remark}
  To unify the statements of the properties of equality a type class is introduced.
\end{remark}
›

class id_eq = quantifiable_and_identifiable +
  assumes id_eq_1: "[(x :: 'a) = x in v]"
  assumes id_eq_2: "[((x :: 'a) = y)  (y = x) in v]"
  assumes id_eq_3: "[((x :: 'a) = y) & (y = z)  (x = z) in v]"

instantiation ν :: id_eq
begin
  instance proof
    fix x :: ν and v
    show "[x = x in v]"
      using PLM.id_eq_obj_1
      by (simp add: identity_ν_def)
  next
    fix x y::ν and v
    show "[x = y  y = x in v]"
      using PLM.id_eq_obj_2
      by (simp add: identity_ν_def)
  next
    fix x y z::ν and v
    show "[((x = y) & (y = z))  x = z in v]"
      using PLM.id_eq_obj_3
      by (simp add: identity_ν_def)
  qed
end

instantiation 𝗈 :: id_eq
begin
  instance proof
    fix x :: 𝗈 and v
    show "[x = x in v]"
      using PLM.id_eq_prop_prop_7 .
  next
    fix x y :: 𝗈 and v
    show "[x = y  y = x in v]"
      using PLM.id_eq_prop_prop_8 .
  next
    fix x y z :: 𝗈 and v
    show "[((x = y) & (y = z))  x = z in v]"
      using PLM.id_eq_prop_prop_9 .
  qed
end

instantiation Π1 :: id_eq
begin
  instance proof
    fix x :: Π1 and v
    show "[x = x in v]"
      using PLM.id_eq_prop_prop_1 .
  next
    fix x y :: Π1 and v
    show "[x = y  y = x in v]"
      using PLM.id_eq_prop_prop_2 .
  next
    fix x y z :: Π1 and v
    show "[((x = y) & (y = z))  x = z in v]"
      using PLM.id_eq_prop_prop_3 .
  qed
end

instantiation Π2 :: id_eq
begin
  instance proof
    fix x :: Π2 and v
    show "[x = x in v]"
      using PLM.id_eq_prop_prop_4_a .
  next
    fix x y :: Π2 and v
    show "[x = y  y = x in v]"
      using PLM.id_eq_prop_prop_5_a .
  next
    fix x y z :: Π2 and v
    show "[((x = y) & (y = z))  x = z in v]"
      using PLM.id_eq_prop_prop_6_a .
  qed
end

instantiation Π3 :: id_eq
begin
  instance proof
    fix x :: Π3 and v
    show "[x = x in v]"
      using PLM.id_eq_prop_prop_4_b .
  next
    fix x y :: Π3 and v
    show "[x = y  y = x in v]"
      using PLM.id_eq_prop_prop_5_b .
  next
    fix x y z :: Π3 and v
    show "[((x = y) & (y = z))  x = z in v]"
      using PLM.id_eq_prop_prop_6_b .
  qed
end

context PLM
begin
  lemma id_eq_1[PLM]:
    "[(x::'a::id_eq) = x in v]"
    using id_eq_1 .
  lemma id_eq_2[PLM]:
    "[((x::'a::id_eq) = y)  (y = x) in v]"
    using id_eq_2 .
  lemma id_eq_3[PLM]:
    "[((x::'a::id_eq) = y) & (y = z)  (x = z) in v]"
    using id_eq_3 .

  attribute_setup eq_sym = ‹
    Scan.succeed (Thm.rule_attribute [] 
      (fn _ => fn thm => thm RS @{thm id_eq_2[deduction]}))


  lemma all_self_eq_1[PLM]:
    "[( α :: 'a::id_eq . α = α) in v]"
    by PLM_solver
  lemma all_self_eq_2[PLM]:
    "[α :: 'a::id_eq . (α = α) in v]"
    by PLM_solver

  lemma t_id_t_proper_1[PLM]:
    "[τ = τ'  ( β . (βP) = τ) in v]"
    proof (rule CP)
      assume "[τ = τ' in v]"
      moreover {
        assume "[τ =E τ' in v]"
        hence "[ β . (βP) = τ in v]"
          apply -
          apply (rule cqt_5_mod[where ψ="λ τ . τ =E τ'", axiom_instance, deduction])
           subgoal unfolding identity_defs by (rule SimpleExOrEnc.intros)
          by simp
      }
      moreover {
        assume "[A!,τ & A!,τ' & (F. τ,F  τ',F) in v]"
        hence "[ β . (βP) = τ in v]"
          apply -
          apply (rule cqt_5_mod[where ψ="λ τ . A!,τ", axiom_instance, deduction])
           subgoal unfolding identity_defs by (rule SimpleExOrEnc.intros)
          by PLM_solver
      }
      ultimately show "[ β . (βP) = τ in v]" unfolding identityκ_def
        using intro_elim_4_b reductio_aa_1 by blast
    qed

  lemma t_id_t_proper_2[PLM]: "[τ = τ'  ( β . (βP) = τ') in v]"
  proof (rule CP)
    assume "[τ = τ' in v]"
    moreover {
      assume "[τ =E τ' in v]"
      hence "[ β . (βP) = τ' in v]"
        apply -
        apply (rule cqt_5_mod[where ψ="λ τ' . τ =E τ'", axiom_instance, deduction])
         subgoal unfolding identity_defs by (rule SimpleExOrEnc.intros)
        by simp
    }
    moreover {
      assume "[A!,τ & A!,τ' & (F. τ,F  τ',F) in v]"
      hence "[ β . (βP) = τ' in v]"
        apply -
        apply (rule cqt_5_mod[where ψ="λ τ . A!,τ", axiom_instance, deduction])
         subgoal unfolding identity_defs by (rule SimpleExOrEnc.intros)
        by PLM_solver
    }
    ultimately show "[ β . (βP) = τ' in v]" unfolding identityκ_def
      using intro_elim_4_b reductio_aa_1 by blast
  qed

  lemma id_nec[PLM]: "[((α::'a::id_eq) = (β))  ((α) = (β)) in v]"
    apply (rule "I")
     using l_identity[where φ = "(λ β .  ((α) = (β)))", axiom_instance]
           id_eq_1 RN ded_thm_cor_4 unfolding identity_ν_def
     apply blast
    using qml_2[axiom_instance] by blast

  lemma id_nec_desc[PLM]:
    "[((ιx. φ x) = (ιx. ψ x))  ((ιx. φ x) = (ιx. ψ x)) in v]"
    proof (cases "[( α. (αP) = (ιx . φ x)) in v]  [( β. (βP) = (ιx . ψ x)) in v]")
      assume "[( α. (αP) = (ιx . φ x)) in v]  [( β. (βP) = (ιx . ψ x)) in v]"
      then obtain α and β where
        "[(αP) = (ιx . φ x) in v]  [(βP) = (ιx . ψ x) in v]"
        apply - unfolding conn_defs by PLM_solver
      moreover {
        moreover have "[(α) = (β)  ((α) = (β)) in v]" by PLM_solver
        ultimately have "[((ιx. φ x) = (βP)  ((ιx. φ x) = (βP))) in v]"
          using l_identity[where φ="λ α . (α) = (βP)  ((α) = (βP))", axiom_instance]
          modus_ponens unfolding identity_ν_def by metis
      }
      ultimately show ?thesis
        using l_identity[where φ="λ α . (ιx . φ x) = (α)
                                    ((ιx . φ x) = (α))", axiom_instance]
        modus_ponens by metis
    next
      assume "¬([( α. (αP) = (ιx . φ x)) in v]  [( β. (βP) = (ιx . ψ x)) in v])"
      hence "¬[A!,(ιx . φ x) in v]  ¬[(ιx . φ x) =E (ιx . ψ x) in v]
            ¬[A!,(ιx . ψ x) in v]  ¬[(ιx . φ x) =E (ιx . ψ x) in v]"
      unfolding identityE_infix_def
      using cqt_5[axiom_instance] PLM.contraposition_1 SimpleExOrEnc.intros
            vdash_properties_10 by meson
      hence "¬[(ιx . φ x) = (ιx . ψ x) in v]"
        apply - unfolding identity_defs by PLM_solver
      thus ?thesis apply - apply PLM_solver
        using qml_2[axiom_instance, deduction] by auto
    qed

subsection‹Quantification›
text‹\label{TAO_PLM_Quantification}›

  lemma rule_ui[PLM,PLM_elim,PLM_dest]:
    "[α . φ α in v]  [φ β in v]"
    by (meson cqt_1[axiom_instance, deduction])
  lemmas "E" = rule_ui

  lemma rule_ui_2[PLM,PLM_elim,PLM_dest]:
    "[α . φ (αP) in v]; [ α . (α)P = β in v]  [φ β in v]"
    using cqt_1_κ[axiom_instance, deduction, deduction] by blast

  lemma cqt_orig_1[PLM]:
    "[(α. φ α)  φ β in v]"
    by PLM_solver
  lemma cqt_orig_2[PLM]:
    "[(α. φ  ψ α)  (φ  (α. ψ α)) in v]"
    by PLM_solver

  lemma universal[PLM]:
    "(α . [φ α in v])  [ α . φ α in v]"
    using rule_gen .
  lemmas "I" = universal

  lemma cqt_basic_1[PLM]:
    "[(α. (β . φ α β))  (β. (α. φ α β)) in v]"
    by PLM_solver
  lemma cqt_basic_2[PLM]:
    "[(α. φ α  ψ α)  ((α. φ α  ψ α) & (α. ψ α  φ α)) in v]"
    by PLM_solver
  lemma cqt_basic_3[PLM]:
    "[(α. φ α  ψ α)  ((α. φ α)  (α. ψ α)) in v]"
    by PLM_solver
  lemma cqt_basic_4[PLM]:
    "[(α. φ α & ψ α)  ((α. φ α) & (α. ψ α)) in v]"
    by PLM_solver
  lemma cqt_basic_6[PLM]:
    "[(α. (α. φ α))  (α. φ α) in v]"
    by PLM_solver
  lemma cqt_basic_7[PLM]:
    "[(φ  (α . ψ α))  (α.(φ  ψ α)) in v]"
    by PLM_solver
  lemma cqt_basic_8[PLM]:
    "[((α. φ α)  (α. ψ α))  (α. (φ α  ψ α)) in v]"
    by PLM_solver
  lemma cqt_basic_9[PLM]:
    "[((α. φ α  ψ α) & (α. ψ α  χ α))  (α. φ α  χ α) in v]"
    by PLM_solver
  lemma cqt_basic_10[PLM]:
    "[((α. φ α  ψ α) & (α. ψ α  χ α))  (α. φ α  χ α) in v]"
    by PLM_solver
  lemma cqt_basic_11[PLM]:
    "[(α. φ α  ψ α)  (α. ψ α  φ α) in v]"
    by PLM_solver
  lemma cqt_basic_12[PLM]:
    "[(α. φ α)  (β. φ β) in v]"
    by PLM_solver

  lemma existential[PLM,PLM_intro]:
    "[φ α in v]  [ α. φ α in v]"
    unfolding exists_def by PLM_solver
  lemmas "I" = existential
  lemma instantiation_[PLM,PLM_elim,PLM_dest]:
    "[α . φ α in v]; (α.[φ α in v]  [ψ in v])  [ψ in v]"
    unfolding exists_def by PLM_solver

  lemma Instantiate:
    assumes "[ x . φ x  in v]"
    obtains x where "[φ x in v]"
    apply (insert assms) unfolding exists_def by PLM_solver
  lemmas "E" = Instantiate

  lemma cqt_further_1[PLM]:
    "[(α. φ α)  (α. φ α) in v]"
    by PLM_solver
  lemma cqt_further_2[PLM]:
    "[(¬(α. φ α))  (α. ¬φ α) in v]"
    unfolding exists_def by PLM_solver
  lemma cqt_further_3[PLM]:
    "[(α. φ α)  ¬(α. ¬φ α) in v]"
    unfolding exists_def by PLM_solver
  lemma cqt_further_4[PLM]:
    "[(¬(α. φ α))  (α. ¬φ α) in v]"
    unfolding exists_def by PLM_solver
  lemma cqt_further_5[PLM]:
    "[(α. φ α & ψ α)  ((α. φ α) & (α. ψ α)) in v]"
      unfolding exists_def by PLM_solver
  lemma cqt_further_6[PLM]:
    "[(α. φ α  ψ α)  ((α. φ α)  (α. ψ α)) in v]"
    unfolding exists_def by PLM_solver
  lemma cqt_further_10[PLM]:
    "[(φ (α::'a::id_eq) & ( β . φ β  β = α))  ( β . φ β  β = α) in v]"
    apply PLM_solver
     using l_identity[axiom_instance, deduction, deduction] id_eq_2[deduction]
     apply blast
    using id_eq_1 by auto
  lemma cqt_further_11[PLM]:
    "[((α. φ α) & (α. ψ α))  (α. φ α  ψ α) in v]"
    by PLM_solver
  lemma cqt_further_12[PLM]:
    "[((¬(α. φ α)) & (¬(α. ψ α)))  (α. φ α  ψ α) in v]"
    unfolding exists_def by PLM_solver
  lemma cqt_further_13[PLM]:
    "[((α. φ α) & (¬(α. ψ α)))  (¬(α. φ α  ψ α)) in v]"
    unfolding exists_def by PLM_solver
  lemma cqt_further_14[PLM]:
    "[(α. β. φ α β)  (β. α. φ α β) in v]"
    unfolding exists_def by PLM_solver

  lemma nec_exist_unique[PLM]:
    "[( x. φ x  (φ x))  ((!x. φ x)  (!x. (φ x))) in v]"
    proof (rule CP)
      assume a: "[x. φ x  φ x in v]"
      show "[(!x. φ x)  (!x. φ x) in v]"
      proof (rule CP)
        assume "[(!x. φ x) in v]"
        hence "[α. φ α & (β. φ β  β = α) in v]"
          by (simp only: exists_unique_def)
        then obtain α where 1:
          "[φ α & (β. φ β  β = α) in v]"
          by (rule "E")
        {
          fix β
          have "[φ β  β = α in v]"
            using 1 "&E"(2) qml_2[axiom_instance]
              ded_thm_cor_3 "E" by fastforce
        }
        hence "[β. φ β  β = α in v]" by (rule "I")
        moreover have "[(φ α) in v]"
          using 1 "&E"(1) a vdash_properties_10 cqt_orig_1[deduction]
          by fast
        ultimately have "[α. (φ α) & (β. φ β  β = α) in v]"
          using "&I" "I" by fast
        thus "[(!x. φ x) in v]"
          unfolding exists_unique_def by assumption
      qed
    qed


subsection‹Actuality and Descriptions›
text‹\label{TAO_PLM_ActualityAndDescriptions}›

  lemma nec_imp_act[PLM]: "[φ  𝒜φ in v]"
    apply (rule CP)
    using qml_act_2[axiom_instance, equiv_lr]
          qml_2[axiom_actualization, axiom_instance]
          logic_actual_nec_2[axiom_instance, equiv_lr, deduction]
    by blast
  lemma act_conj_act_1[PLM]:
    "[𝒜(𝒜φ  φ) in v]"
    using equiv_def logic_actual_nec_2[axiom_instance]
          logic_actual_nec_4[axiom_instance] "&E"(2) "E"(2)
    by metis
  lemma act_conj_act_2[PLM]:
    "[𝒜(φ  𝒜φ) in v]"
    using logic_actual_nec_2[axiom_instance] qml_act_1[axiom_instance]
          ded_thm_cor_3 "E"(2) nec_imp_act
    by blast
  lemma act_conj_act_3[PLM]:
    "[(𝒜φ & 𝒜ψ)  𝒜(φ & ψ) in v]"
    unfolding conn_defs
    by (metis logic_actual_nec_2[axiom_instance]
              logic_actual_nec_1[axiom_instance]
              "E"(2) CP "E"(4) reductio_aa_2
              vdash_properties_10)
  lemma act_conj_act_4[PLM]:
    "[𝒜(𝒜φ  φ) in v]"
    unfolding equiv_def
    by (PLM_solver PLM_intro: act_conj_act_3[where φ="𝒜φ  φ"
                                and ψ="φ  𝒜φ", deduction])
  lemma closure_act_1a[PLM]:
    "[𝒜𝒜(𝒜φ  φ) in v]"
    using logic_actual_nec_4[axiom_instance]
          act_conj_act_4 "E"(1)
    by blast
  lemma closure_act_1b[PLM]:
    "[𝒜𝒜𝒜(𝒜φ  φ) in v]"
    using logic_actual_nec_4[axiom_instance]
          act_conj_act_4 "E"(1)
    by blast
  lemma closure_act_1c[PLM]:
    "[𝒜𝒜𝒜𝒜(𝒜φ  φ) in v]"
    using logic_actual_nec_4[axiom_instance]
          act_conj_act_4 "E"(1)
    by blast
  lemma closure_act_2[PLM]:
    "[α. 𝒜(𝒜(φ α)  φ α) in v]"
    by PLM_solver

  lemma closure_act_3[PLM]:
    "[𝒜(α. 𝒜(φ α)  φ α) in v]"
    by (PLM_solver PLM_intro: logic_actual_nec_3[axiom_instance, equiv_rl])
  lemma closure_act_4[PLM]:
    "[𝒜(α1 α2. 𝒜(φ α1 α2)  φ α1 α2) in v]"
    by (PLM_solver PLM_intro: logic_actual_nec_3[axiom_instance, equiv_rl])
  lemma closure_act_4_b[PLM]:
    "[𝒜(α1 α2 α3. 𝒜(φ α1 α2 α3)  φ α1 α2 α3) in v]"
    by (PLM_solver PLM_intro: logic_actual_nec_3[axiom_instance, equiv_rl])
  lemma closure_act_4_c[PLM]:
    "[𝒜(α1 α2 α3 α4. 𝒜(φ α1 α2 α3 α4)  φ α1 α2 α3 α4) in v]"
    by (PLM_solver PLM_intro: logic_actual_nec_3[axiom_instance, equiv_rl])

  lemma RA[PLM,PLM_intro]:
    "([φ in dw])  [𝒜φ in dw]"
    using logic_actual[necessitation_averse_axiom_instance, equiv_rl] .

  lemma RA_2[PLM,PLM_intro]:
    "([ψ in dw]  [φ in dw])  ([𝒜ψ in dw]  [𝒜φ in dw])"
    using RA logic_actual[necessitation_averse_axiom_instance] intro_elim_6_a by blast

  context
  begin
    private lemma ActualE[PLM,PLM_elim,PLM_dest]:
      "[