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
typedecl j
consts dw :: i
consts dj :: j
typedecl ω
typedecl σ
datatype υ = ωυ ω | συ σ
subsection‹Derived Types›
text‹\label{TAO_Embedding_Derived_Types}›
typedef 𝗈 = "UNIV::(j⇒i⇒bool) set"
morphisms eval𝗈 make𝗈 ..
type_synonym Π⇩0 = 𝗈
typedef Π⇩1 = "UNIV::(υ⇒j⇒i⇒bool) set"
morphisms evalΠ⇩1 makeΠ⇩1 ..
typedef Π⇩2 = "UNIV::(υ⇒υ⇒j⇒i⇒bool) set"
morphisms evalΠ⇩2 makeΠ⇩2 ..
typedef Π⇩3 = "UNIV::(υ⇒υ⇒υ⇒j⇒i⇒bool) set"
morphisms evalΠ⇩3 makeΠ⇩3 ..
type_synonym α = "Π⇩1 set"
datatype ν = ων ω | αν α
typedef κ = "UNIV::(ν option) set"
morphisms evalκ makeκ ..
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⇒(i⇒bool)⇒i⇒bool"
consts I_IMPL :: "j⇒(i⇒bool)⇒(i⇒bool)⇒(i⇒bool)"
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 forall⇩0 :: "(Π⇩0⇒𝗈)⇒𝗈" (binder "❙∀⇩0" [8] 9) is
"λ φ s w . ∀ x :: Π⇩0 . (φ x) s w" .
lift_definition forall⇩1 :: "(Π⇩1⇒𝗈)⇒𝗈" (binder "❙∀⇩1" [8] 9) is
"λ φ s w . ∀ x :: Π⇩1 . (φ x) s w" .
lift_definition forall⇩2 :: "(Π⇩2⇒𝗈)⇒𝗈" (binder "❙∀⇩2" [8] 9) is
"λ φ s w . ∀ x :: Π⇩2 . (φ x) s w" .
lift_definition forall⇩3 :: "(Π⇩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 ∧ (φ (a⇧P) dj v)) = (φ (x⇧P) dj v)" .
lift_definition IsProperInXY :: "(κ⇒κ⇒𝗈)⇒bool" is
"λ φ . ∀ x y v . (∃ a b . νυ a = νυ x ∧ νυ b = νυ y
∧ (φ (a⇧P) (b⇧P) dj v)) = (φ (x⇧P) (y⇧P) dj v)" .
lift_definition IsProperInXYZ :: "(κ⇒κ⇒κ⇒𝗈)⇒bool" is
"λ φ . ∀ x y z v . (∃ a b c . νυ a = νυ x ∧ νυ b = νυ y ∧ νυ c = νυ z
∧ (φ (a⇧P) (b⇧P) (c⇧P) dj v)) = (φ (x⇧P) (y⇧P) (z⇧P) 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 :: "ω⇒i⇒bool"
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]
forall⇩0_def[meta_defs] forall⇩1_def[meta_defs]
forall⇩2_def[meta_defs] forall⇩3_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]]
declare [[unify_search_bound = 40]]
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 (x⇧P) = x"
by (simp add: meta_aux νκ_def rep_def)
lemma νκ_proper[meta_aux]: "proper (x⇧P)"
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 R⇩0 = "j⇒i⇒bool"
type_synonym R⇩1 = "υ⇒R⇩0"
type_synonym R⇩2 = "υ⇒υ⇒R⇩0"
type_synonym R⇩3 = "υ⇒υ⇒υ⇒R⇩0"
type_synonym W = i
subsubsection‹Denotation Functions›
text‹\label{TAO_Semantics_Semantics_Denotations}›
lift_definition d⇩κ :: "κ⇒R⇩κ option" is id .
lift_definition d⇩0 :: "Π⇩0⇒R⇩0 option" is Some .
lift_definition d⇩1 :: "Π⇩1⇒R⇩1 option" is Some .
lift_definition d⇩2 :: "Π⇩2⇒R⇩2 option" is Some .
lift_definition d⇩3 :: "Π⇩3⇒R⇩3 option" is Some .
subsubsection‹Actual World›
text‹\label{TAO_Semantics_Semantics_Actual_World}›
definition w⇩0 where "w⇩0 ≡ dw"
subsubsection‹Exemplification Extensions›
text‹\label{TAO_Semantics_Semantics_Exemplification_Extensions}›
definition ex0 :: "R⇩0⇒W⇒bool"
where "ex0 ≡ λ F . F dj"
definition ex1 :: "R⇩1⇒W⇒(R⇩κ set)"
where "ex1 ≡ λ F w . { x . F (νυ x) dj w }"
definition ex2 :: "R⇩2⇒W⇒((R⇩κ×R⇩κ) set)"
where "ex2 ≡ λ F w . { (x,y) . F (νυ x) (νυ y) dj w }"
definition ex3 :: "R⇩3⇒W⇒((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 :: "R⇩1⇒(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 d⇩0_def[semantics_defs] d⇩1_def[semantics_defs]
d⇩2_def[semantics_defs] d⇩3_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]
w⇩0_def[semantics_defs]
subsubsection‹Truth Conditions of Exemplification Formulas›
text‹\label{TAO_Semantics_Semantics_Exemplification}›
lemma T1_1[semantics]:
"(w ⊨ ⦇F,x⦈) = (∃ r o⇩1 . Some r = d⇩1 F ∧ Some o⇩1 = d⇩κ x ∧ o⇩1 ∈ 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 o⇩1 o⇩2 . Some r = d⇩2 F ∧ Some o⇩1 = d⇩κ x
∧ Some o⇩2 = d⇩κ y ∧ (o⇩1, o⇩2) ∈ ex2 r 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 o⇩1 o⇩2 o⇩3 . Some r = d⇩3 F ∧ Some o⇩1 = d⇩κ x
∧ Some o⇩2 = d⇩κ y ∧ Some o⇩3 = d⇩κ z
∧ (o⇩1, o⇩2, o⇩3) ∈ ex3 r 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 = d⇩0 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 o⇩1 . Some r = d⇩1 F ∧ Some o⇩1 = d⇩κ x ∧ o⇩1 ∈ 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 . (w⇩0 ⊨ ψ x) ∧ (∀ y . (w⇩0 ⊨ ψ y) ⟶ y = x))
then (Some (THE x . (w⇩0 ⊨ ψ 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]: "d⇩1 (❙λ x . ⦇F, x⇧P⦈) = d⇩1 F"
by (simp add: meta_defs meta_aux)
lemma D4_2[semantics]: "d⇩2 (❙λ⇧2 (λ x y . ⦇F, x⇧P, y⇧P⦈)) = d⇩2 F"
by (simp add: meta_defs meta_aux)
lemma D4_3[semantics]: "d⇩3 (❙λ⇧3 (λ x y z . ⦇F, x⇧P, y⇧P, z⇧P⦈)) = d⇩3 F"
by (simp add: meta_defs meta_aux)
lemma D5_1[semantics]:
assumes "IsProperInX φ"
shows "⋀ w o⇩1 r . Some r = d⇩1 (❙λ x . (φ (x⇧P))) ∧ Some o⇩1 = d⇩κ x
⟶ (o⇩1 ∈ 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 o⇩1 o⇩2 r . Some r = d⇩2 (❙λ⇧2 (λ x y . φ (x⇧P) (y⇧P)))
∧ Some o⇩1 = d⇩κ x ∧ Some o⇩2 = d⇩κ y
⟶ ((o⇩1,o⇩2) ∈ 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 o⇩1 o⇩2 o⇩3 r . Some r = d⇩3 (❙λ⇧3 (λ x y z . φ (x⇧P) (y⇧P) (z⇧P)))
∧ Some o⇩1 = d⇩κ x ∧ Some o⇩2 = d⇩κ y ∧ Some o⇩3 = d⇩κ z
⟶ ((o⇩1,o⇩2,o⇩3) ∈ 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 = d⇩0 (❙λ⇧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 propex⇩0: "∃ r . Some r = d⇩0 F"
unfolding d⇩0_def by simp
lemma propex⇩1: "∃ r . Some r = d⇩1 F"
unfolding d⇩1_def by simp
lemma propex⇩2: "∃ r . Some r = d⇩2 F"
unfolding d⇩2_def by simp
lemma propex⇩3: "∃ r . Some r = d⇩3 F"
unfolding d⇩3_def by simp
lemma d⇩κ_proper: "d⇩κ (u⇧P) = Some u"
unfolding d⇩κ_def by (simp add: νκ_def meta_aux)
lemma ConcretenessSemantics1:
"Some r = d⇩1 E! ⟹ (∃ w . ων x ∈ ex1 r w)"
unfolding semantics_defs apply transfer
by (simp add: OrdinaryObjectsPossiblyConcreteAxiom νυ_ων_is_ωυ)
lemma ConcretenessSemantics2:
"Some r = d⇩1 E! ⟹ (x ∈ ex1 r w ⟶ (∃y. x = ων y))"
unfolding semantics_defs apply transfer apply simp
by (metis ν.exhaust υ.exhaust υ.simps(6) no_αω)
lemma d⇩0_inject: "⋀x y. d⇩0 x = d⇩0 y ⟹ x = y"
unfolding d⇩0_def by (simp add: eval𝗈_inject)
lemma d⇩1_inject: "⋀x y. d⇩1 x = d⇩1 y ⟹ x = y"
unfolding d⇩1_def by (simp add: evalΠ⇩1_inject)
lemma d⇩2_inject: "⋀x y. d⇩2 x = d⇩2 y ⟹ x = y"
unfolding d⇩2_def by (simp add: evalΠ⇩2_inject)
lemma d⇩3_inject: "⋀x y. d⇩3 x = d⇩3 y ⟹ x = y"
unfolding d⇩3_def by (simp add: evalΠ⇩3_inject)
lemma d⇩κ_inject: "⋀x y o⇩1. Some o⇩1 = d⇩κ x ∧ Some o⇩1 = d⇩κ y ⟹ x = y"
proof -
fix x :: κ and y :: κ and o⇩1 :: ν
assume "Some o⇩1 = d⇩κ x ∧ Some o⇩1 = 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 . χ
(λ F . ⦇F,x⦈)
(λ F . ⦇F,x,x⦈) (λ F a . ⦇F,x,a⦈) (λ F a . ⦇F,a,x⦈)
(λ F . ⦇F,x,x,x⦈)
(λ F a . ⦇F,x,x,a⦈) (λ F a . ⦇F,x,a,x⦈)
(λ F a . ⦇F,a,x,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 . χ
(λ F . ⦇F,x⦈)
(λ F . ⦇F,x,x⦈) (λ F a . ⦇F,x,a⦈) (λ F a . ⦇F,a,x⦈)
(λ F . ⦇F,x,x,x⦈)
(λ F a . ⦇F,x,x,a⦈) (λ F a . ⦇F,x,a,x⦈)
(λ F a . ⦇F,a,x,x⦈)
(λ F a b. ⦇F,x,a,b⦈) (λ F a b. ⦇F,a,x,b⦈)
(λ F a b . ⦇F,a,b,x⦈)
(λ F . ⦇F,y⦈)
(λ F . ⦇F,y,y⦈) (λ F a . ⦇F,y,a⦈) (λ F a . ⦇F,a,y⦈)
(λ F . ⦇F,y,y,y⦈)
(λ F a . ⦇F,y,y,a⦈) (λ F a . ⦇F,y,a,y⦈)
(λ F a . ⦇F,a,y,y⦈)
(λ F a b. ⦇F,y,a,b⦈) (λ F a b. ⦇F,a,y,b⦈)
(λ F a b . ⦇F,a,b,y⦈)
(λ F . ⦇F,x,y⦈) (λ F . ⦇F,y,x⦈)
(λ F a . ⦇F,x,y,a⦈) (λ F a . ⦇F,x,a,y⦈)
(λ F a . ⦇F,a,x,y⦈)
(λ F a . ⦇F,y,x,a⦈) (λ F a . ⦇F,y,a,x⦈)
(λ F a . ⦇F,a,y,x⦈)
(λ F . ⦇F,x,x,y⦈) (λ F . ⦇F,x,y,x⦈)
(λ F . ⦇F,y,x,x⦈)
(λ F . ⦇F,x,y,y⦈) (λ F . ⦇F,y,x,y⦈)
(λ F . ⦇F,y,y,x⦈)
(λ F . ⦇F,x,x,x⦈)
(λ F . ⦇F,y,y,y⦈))"
unfolding IsProperInXY_def by (auto simp: meta_defs meta_aux)
lemma IsProperInXYZ_intro[IsProper_intros]:
"IsProperInXYZ (λ x y z . χ
(λ F . ⦇F,x⦈)
(λ F . ⦇F,x,x⦈) (λ F a . ⦇F,x,a⦈) (λ F a . ⦇F,a,x⦈)
(λ F . ⦇F,x,x,x⦈)
(λ F a . ⦇F,x,x,a⦈) (λ F a . ⦇F,x,a,x⦈)
(λ F a . ⦇F,a,x,x⦈)
(λ F a b. ⦇F,x,a,b⦈) (λ F a b. ⦇F,a,x,b⦈)
(λ F a b . ⦇F,a,b,x⦈)
(λ F . ⦇F,y⦈)
(λ F . ⦇F,y,y⦈) (λ F a . ⦇F,y,a⦈) (λ F a . ⦇F,a,y⦈)
(λ F . ⦇F,y,y,y⦈)
(λ F a . ⦇F,y,y,a⦈) (λ F a . ⦇F,y,a,y⦈)
(λ F a . ⦇F,a,y,y⦈)
(λ F a b. ⦇F,y,a,b⦈) (λ F a b. ⦇F,a,y,b⦈)
(λ F a b . ⦇F,a,b,y⦈)
(λ F . ⦇F,z⦈)
(λ F . ⦇F,z,z⦈) (λ F a . ⦇F,z,a⦈) (λ F a . ⦇F,a,z⦈)
(λ F . ⦇F,z,z,z⦈)
(λ F a . ⦇F,z,z,a⦈) (λ F a . ⦇F,z,a,z⦈)
(λ F a . ⦇F,a,z,z⦈)
(λ F a b. ⦇F,z,a,b⦈) (λ F a b. ⦇F,a,z,b⦈)
(λ F a b . ⦇F,a,b,z⦈)
(λ F . ⦇F,x,y⦈) (λ F . ⦇F,y,x⦈)
(λ F a . ⦇F,x,y,a⦈) (λ F a . ⦇F,x,a,y⦈)
(λ F a . ⦇F,a,x,y⦈)
(λ F a . ⦇F,y,x,a⦈) (λ F a . ⦇F,y,a,x⦈)
(λ F a . ⦇F,a,y,x⦈)
(λ F . ⦇F,x,x,y⦈) (λ F . ⦇F,x,y,x⦈)
(λ F . ⦇F,y,x,x⦈)
(λ F . ⦇F,x,y,y⦈) (λ F . ⦇F,y,x,y⦈)
(λ F . ⦇F,y,y,x⦈)
(λ F . ⦇F,x,x,x⦈)
(λ F . ⦇F,y,y,y⦈)
(λ F . ⦇F,x,z⦈) (λ F . ⦇F,z,x⦈)
(λ F a . ⦇F,x,z,a⦈) (λ F a . ⦇F,x,a,z⦈)
(λ F a . ⦇F,a,x,z⦈)
(λ F a . ⦇F,z,x,a⦈) (λ F a . ⦇F,z,a,x⦈)
(λ F a . ⦇F,a,z,x⦈)
(λ F . ⦇F,x,x,z⦈) (λ F . ⦇F,x,z,x⦈)
(λ F . ⦇F,z,x,x⦈)
(λ F . ⦇F,x,z,z⦈) (λ F . ⦇F,z,x,z⦈)
(λ F . ⦇F,z,z,x⦈)
(λ F . ⦇F,x,x,x⦈)
(λ F . ⦇F,z,z,z⦈)
(λ F . ⦇F,y,z⦈) (λ F . ⦇F,z,y⦈)
(λ F a . ⦇F,y,z,a⦈) (λ F a . ⦇F,y,a,z⦈)
(λ F a . ⦇F,a,y,z⦈)
(λ F a . ⦇F,z,y,a⦈) (λ F a . ⦇F,z,a,y⦈)
(λ F a . ⦇F,a,z,y⦈)
(λ F . ⦇F,y,y,z⦈) (λ F . ⦇F,y,z,y⦈)
(λ F . ⦇F,z,y,y⦈)
(λ F . ⦇F,y,z,z⦈) (λ F . ⦇F,z,y,z⦈)
(λ F . ⦇F,z,z,y⦈)
(λ F . ⦇F,y,y,y⦈)
(λ F . ⦇F,z,z,z⦈)
(λ F . ⦇F,x,y,z⦈) (λ F . ⦇F,x,z,y⦈)
(λ F . ⦇F,y,x,z⦈) (λ F . ⦇F,y,z,x⦈)
(λ 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}›
no_syntax "_list" :: "args ⇒ 'a list" ("[(_)]")
no_syntax "__listcompr" :: "args ⇒ 'a list" ("[(_)]")
abbreviation validity_in :: "𝗈⇒i⇒bool" ("[_ 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 ≡ forall⇩1"
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 ≡ forall⇩2"
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 ≡ forall⇩3"
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!,x⇧P⦈"
definition Abstract :: "Π⇩1" ("A!") where "Abstract ≡ ❙λx. ❙¬❙◇⦇E!,x⇧P⦈"
subsection‹Identity Definitions›
text‹\label{TAO_BasicDefinitions_Identity}›
definition basic_identity⇩E::"Π⇩2" where
"basic_identity⇩E ≡ ❙λ⇧2 (λ x y . ⦇O!,x⇧P⦈ ❙& ⦇O!,y⇧P⦈
❙& ❙□(❙∀ F. ⦇F,x⇧P⦈ ❙≡ ⦇F,y⇧P⦈))"
definition basic_identity⇩E_infix::"κ⇒κ⇒𝗈" (infixl "❙=⇩E" 63) where
"x ❙=⇩E y ≡ ⦇basic_identity⇩E, 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_identity⇩1 (infixl "❙=⇩1" 63) where
"basic_identity⇩1 ≡ λ F G . ❙□(❙∀ x. ⦃x⇧P,F⦄ ❙≡ ⦃x⇧P,G⦄)"
definition basic_identity⇩2 :: "Π⇩2⇒Π⇩2⇒𝗈" (infixl "❙=⇩2" 63) where
"basic_identity⇩2 ≡ λ F G . ❙∀ x. ((❙λy. ⦇F,x⇧P,y⇧P⦈) ❙=⇩1 (❙λy. ⦇G,x⇧P,y⇧P⦈))
❙& ((❙λy. ⦇F,y⇧P,x⇧P⦈) ❙=⇩1 (❙λy. ⦇G,y⇧P,x⇧P⦈))"
definition basic_identity⇩3::"Π⇩3⇒Π⇩3⇒𝗈" (infixl "❙=⇩3" 63) where
"basic_identity⇩3 ≡ λ F G . ❙∀ x y. (❙λz. ⦇F,z⇧P,x⇧P,y⇧P⦈) ❙=⇩1 (❙λz. ⦇G,z⇧P,x⇧P,y⇧P⦈)
❙& (❙λz. ⦇F,x⇧P,z⇧P,y⇧P⦈) ❙=⇩1 (❙λz. ⦇G,x⇧P,z⇧P,y⇧P⦈)
❙& (❙λz. ⦇F,x⇧P,y⇧P,z⇧P⦈) ❙=⇩1 (❙λz. ⦇G,x⇧P,y⇧P,z⇧P⦈)"
definition basic_identity⇩0::"𝗈⇒𝗈⇒𝗈" (infixl "❙=⇩0" 63) where
"basic_identity⇩0 ≡ λ 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 o⇩1 . Some r = d⇩1 F ∧ Some o⇩1 = d⇩κ x ∧ o⇩1 ∈ en r"
shows "[⦃x,F⦄ in v]"
using assms by (auto simp: Semantics.T2)
lemma EncE[meta_elim]:
assumes "[⦃x,F⦄ in v]"
shows "∃ r o⇩1 . Some r = d⇩1 F ∧ Some o⇩1 = d⇩κ x ∧ o⇩1 ∈ en r"
using assms by (auto simp: Semantics.T2)
lemma EncS[meta_subst]:
"[⦃x,F⦄ in v] = (∃ r o⇩1 . Some r = d⇩1 F ∧ Some o⇩1 = d⇩κ x ∧ o⇩1 ∈ en r)"
by (auto simp: Semantics.T2)
subsection‹Rules for Exemplification›
text‹\label{TAO_MetaSolver_Exemplification}›
subsubsection‹Zero-place Relations›
lemma Exe0I[meta_intro]:
assumes "∃ r . Some r = d⇩0 p ∧ ex0 r v"
shows "[⦇p⦈ in v]"
using assms by (auto simp: Semantics.T3)
lemma Exe0E[meta_elim]:
assumes "[⦇p⦈ in v]"
shows "∃ r . Some r = d⇩0 p ∧ ex0 r v"
using assms by (auto simp: Semantics.T3)
lemma Exe0S[meta_subst]:
"[⦇p⦈ in v] = (∃ r . Some r = d⇩0 p ∧ ex0 r v)"
by (auto simp: Semantics.T3)
subsubsection‹One-Place Relations›
lemma Exe1I[meta_intro]:
assumes "∃ r o⇩1 . Some r = d⇩1 F ∧ Some o⇩1 = d⇩κ x ∧ o⇩1 ∈ ex1 r v"
shows "[⦇F,x⦈ in v]"
using assms by (auto simp: Semantics.T1_1)
lemma Exe1E[meta_elim]:
assumes "[⦇F,x⦈ in v]"
shows "∃ r o⇩1 . Some r = d⇩1 F ∧ Some o⇩1 = d⇩κ x ∧ o⇩1 ∈ ex1 r v"
using assms by (auto simp: Semantics.T1_1)
lemma Exe1S[meta_subst]:
"[⦇F,x⦈ in v] = (∃ r o⇩1 . Some r = d⇩1 F ∧ Some o⇩1 = d⇩κ x ∧ o⇩1 ∈ ex1 r v)"
by (auto simp: Semantics.T1_1)
subsubsection‹Two-Place Relations›
lemma Exe2I[meta_intro]:
assumes "∃ r o⇩1 o⇩2 . Some r = d⇩2 F ∧ Some o⇩1 = d⇩κ x
∧ Some o⇩2 = d⇩κ y ∧ (o⇩1, o⇩2) ∈ ex2 r v"
shows "[⦇F,x,y⦈ in v]"
using assms by (auto simp: Semantics.T1_2)
lemma Exe2E[meta_elim]:
assumes "[⦇F,x,y⦈ in v]"
shows "∃ r o⇩1 o⇩2 . Some r = d⇩2 F ∧ Some o⇩1 = d⇩κ x
∧ Some o⇩2 = d⇩κ y ∧ (o⇩1, o⇩2) ∈ ex2 r v"
using assms by (auto simp: Semantics.T1_2)
lemma Exe2S[meta_subst]:
"[⦇F,x,y⦈ in v] = (∃ r o⇩1 o⇩2 . Some r = d⇩2 F ∧ Some o⇩1 = d⇩κ x
∧ Some o⇩2 = d⇩κ y ∧ (o⇩1, o⇩2) ∈ ex2 r v)"
by (auto simp: Semantics.T1_2)
subsubsection‹Three-Place Relations›
lemma Exe3I[meta_intro]:
assumes "∃ r o⇩1 o⇩2 o⇩3 . Some r = d⇩3 F ∧ Some o⇩1 = d⇩κ x
∧ Some o⇩2 = d⇩κ y ∧ Some o⇩3 = d⇩κ z
∧ (o⇩1, o⇩2, o⇩3) ∈ ex3 r v"
shows "[⦇F,x,y,z⦈ in v]"
using assms by (auto simp: Semantics.T1_3)
lemma Exe3E[meta_elim]:
assumes "[⦇F,x,y,z⦈ in v]"
shows "∃ r o⇩1 o⇩2 o⇩3 . Some r = d⇩3 F ∧ Some o⇩1 = d⇩κ x
∧ Some o⇩2 = d⇩κ y ∧ Some o⇩3 = d⇩κ z
∧ (o⇩1, o⇩2, o⇩3) ∈ ex3 r v"
using assms by (auto simp: Semantics.T1_3)
lemma Exe3S[meta_subst]:
"[⦇F,x,y,z⦈ in v] = (∃ r o⇩1 o⇩2 o⇩3 . Some r = d⇩3 F ∧ Some o⇩1 = d⇩κ x
∧ Some o⇩2 = d⇩κ y ∧ Some o⇩3 = d⇩κ z
∧ (o⇩1, o⇩2, o⇩3) ∈ ex3 r v)"
by (auto simp: Semantics.T1_3)
subsection‹Rules for Being Ordinary›
text‹\label{TAO_MetaSolver_Ordinary}›
lemma OrdI[meta_intro]:
assumes "∃ o⇩1 y. Some o⇩1 = d⇩κ x ∧ o⇩1 = ων y"
shows "[⦇O!,x⦈ in v]"
proof -
have "IsProperInX (λx. ❙◇⦇E!,x⦈)"
by show_proper
moreover have "[❙◇⦇E!,x⦈ in v]"
apply meta_solver
using ConcretenessSemantics1 propex⇩1 assms by fast
ultimately show "[⦇O!,x⦈ in v]"
unfolding Ordinary_def
using D5_1 propex⇩1 assms ConcretenessSemantics1 Exe1S
by blast
qed
lemma OrdE[meta_elim]:
assumes "[⦇O!,x⦈ in v]"
shows "∃ o⇩1 y. Some o⇩1 = d⇩κ x ∧ o⇩1 = ων y"
proof -
have "∃r o⇩1. Some r = d⇩1 O! ∧ Some o⇩1 = d⇩κ x ∧ o⇩1 ∈ ex1 r v"
using assms Exe1E by simp
moreover have "IsProperInX (λx. ❙◇⦇E!,x⦈)"
by show_proper
ultimately have "[❙◇⦇E!,x⦈ in v]"
using D5_1 unfolding Ordinary_def by fast
thus ?thesis
apply - apply meta_solver
using ConcretenessSemantics2 by blast
qed
lemma OrdS[meta_cong]:
"[⦇O!,x⦈ in v] = (∃ o⇩1 y. Some o⇩1 = d⇩κ x ∧ o⇩1 = ων y)"
using OrdI OrdE by blast
subsection‹Rules for Being Abstract›
text‹\label{TAO_MetaSolver_Abstract}›
lemma AbsI[meta_intro]:
assumes "∃ o⇩1 y. Some o⇩1 = d⇩κ x ∧ o⇩1 = αν y"
shows "[⦇A!,x⦈ in v]"
proof -
have "IsProperInX (λx. ❙¬❙◇⦇E!,x⦈)"
by show_proper
moreover have "[❙¬❙◇⦇E!,x⦈ in v]"
apply meta_solver
using ConcretenessSemantics2 propex⇩1 assms
by (metis ν.distinct(1) option.sel)
ultimately show "[⦇A!,x⦈ in v]"
unfolding Abstract_def
using D5_1 propex⇩1 assms ConcretenessSemantics1 Exe1S
by blast
qed
lemma AbsE[meta_elim]:
assumes "[⦇A!,x⦈ in v]"
shows "∃ o⇩1 y. Some o⇩1 = d⇩κ x ∧ o⇩1 = αν y"
proof -
have 1: "IsProperInX (λx. ❙¬❙◇⦇E!,x⦈)"
by show_proper
have "∃r o⇩1. Some r = d⇩1 A! ∧ Some o⇩1 = d⇩κ x ∧ o⇩1 ∈ ex1 r v"
using assms Exe1E by simp
moreover hence "[❙¬❙◇⦇E!,x⦈ in v]"
using D5_1[OF 1]
unfolding Abstract_def by fast
ultimately show ?thesis
apply - apply meta_solver
using ConcretenessSemantics1 propex⇩1
by (metis ν.exhaust)
qed
lemma AbsS[meta_cong]:
"[⦇A!,x⦈ in v] = (∃ o⇩1 y. Some o⇩1 = d⇩κ x ∧ o⇩1 = αν y)"
using AbsI AbsE by blast
subsection‹Rules for Definite Descriptions›
text‹\label{TAO_MetaSolver_DefiniteDescription}›
lemma TheEqI:
assumes "⋀x. [φ x in dw] = [ψ x in dw]"
shows "(❙ιx. φ x) = (❙ιx. ψ x)"
proof -
have 1: "d⇩κ (❙ιx. φ x) = d⇩κ (❙ιx. ψ x)"
using assms D3 unfolding w⇩0_def by simp
{
assume "∃ o⇩1 . Some o⇩1 = d⇩κ (❙ιx. φ x)"
hence ?thesis using 1 d⇩κ_inject by force
}
moreover {
assume "¬(∃ o⇩1 . Some o⇩1 = d⇩κ (❙ιx. φ x))"
hence ?thesis using 1 D3
by (metis d⇩κ.rep_eq evalκ_inverse)
}
ultimately show ?thesis by blast
qed
subsection‹Rules for Identity›
text‹\label{TAO_MetaSolver_Identity}›
subsubsection‹Ordinary Objects›
text‹\label{TAO_MetaSolver_Identity_Ordinary}›
lemma Eq⇩EI[meta_intro]:
assumes "∃ o⇩1 o⇩2. Some (ων o⇩1) = d⇩κ x ∧ Some (ων o⇩2) = d⇩κ y ∧ o⇩1 = o⇩2"
shows "[x ❙=⇩E y in v]"
proof -
obtain o⇩1 o⇩2 where 1:
"Some (ων o⇩1) = d⇩κ x ∧ Some (ων o⇩2) = d⇩κ y ∧ o⇩1 = o⇩2"
using assms by auto
obtain r where 2:
"Some r = d⇩2 basic_identity⇩E"
using propex⇩2 by auto
have "[⦇O!,x⦈ ❙& ⦇O!,y⦈ ❙& ❙□(❙∀F. ⦇F,x⦈ ❙≡ ⦇F,y⦈) in v]"
proof -
have "[⦇O!,x⦈ in v] ∧ [⦇O!,y⦈ in v]"
using OrdI 1 by blast
moreover have "[❙□(❙∀F. ⦇F,x⦈ ❙≡ ⦇F,y⦈) in v]"
apply meta_solver using 1 by force
ultimately show ?thesis using ConjI by simp
qed
moreover have "IsProperInXY (λ x y . ⦇O!,x⦈ ❙& ⦇O!,y⦈ ❙& ❙□(❙∀F. ⦇F,x⦈ ❙≡ ⦇F,y⦈))"
by show_proper
ultimately have "(ων o⇩1, ων o⇩2) ∈ ex2 r v"
using D5_2 1 2
unfolding basic_identity⇩E_def by fast
thus "[x ❙=⇩E y in v]"
using Exe2I 1 2
unfolding basic_identity⇩E_infix_def basic_identity⇩E_def
by blast
qed
lemma Eq⇩EE[meta_elim]:
assumes "[x ❙=⇩E y in v]"
shows "∃ o⇩1 o⇩2. Some (ων o⇩1) = d⇩κ x ∧ Some (ων o⇩2) = d⇩κ y ∧ o⇩1 = o⇩2"
proof -
have "IsProperInXY (λ x y . ⦇O!,x⦈ ❙& ⦇O!,y⦈ ❙& ❙□(❙∀F. ⦇F,x⦈ ❙≡ ⦇F,y⦈))"
by show_proper
hence 1: "[⦇O!,x⦈ ❙& ⦇O!,y⦈ ❙& ❙□(❙∀ F. ⦇F,x⦈ ❙≡ ⦇F,y⦈) in v]"
using assms unfolding basic_identity⇩E_def basic_identity⇩E_infix_def
using D4_2 T1_2 D5_2 by meson
hence 2: "∃ o⇩1 o⇩2 . Some (ων o⇩1) = d⇩κ x
∧ Some (ων o⇩2) = d⇩κ y"
apply (subst (asm) ConjS)
apply (subst (asm) ConjS)
using OrdE by auto
then obtain o⇩1 o⇩2 where 3:
"Some (ων o⇩1) = d⇩κ x ∧ Some (ων o⇩2) = d⇩κ y"
by auto
have "∃ r . Some r = d⇩1 (❙λ z . make𝗈 (λ w s . d⇩κ (z⇧P) = Some (ων o⇩1)))"
using propex⇩1 by auto
then obtain r where 4:
"Some r = d⇩1 (❙λ z . make𝗈 (λ w s . d⇩κ (z⇧P) = Some (ων o⇩1)))"
by auto
hence 5: "r = (λu s w. ∃ x . νυ x = u ∧ Some x = Some (ων o⇩1))"
unfolding lambdabinder1_def d⇩1_def d⇩κ_proper
apply transfer
by simp
have "[❙□(❙∀ F. ⦇F,x⦈ ❙≡ ⦇F,y⦈) in v]"
using 1 using ConjE by blast
hence 6: "∀ v F . [⦇F,x⦈ in v] ⟷ [⦇F,y⦈ in v]"
using BoxE EquivE AllE by fast
hence "∀ v . ((ων o⇩1) ∈ ex1 r v) = ((ων o⇩2) ∈ ex1 r v)"
using 2 4 unfolding valid_in_def
by (metis "3" "6" d⇩1.rep_eq d⇩κ_inject d⇩κ_proper ex1_def eval𝗈_inverse exe1.rep_eq
mem_Collect_eq option.sel rep_proper_id νκ_proper valid_in.abs_eq)
moreover have "(ων o⇩1) ∈ ex1 r v"
unfolding 5 ex1_def by simp
ultimately have "(ων o⇩2) ∈ ex1 r v"
by auto
hence "o⇩1 = o⇩2" unfolding 5 ex1_def by (auto simp: meta_aux)
thus ?thesis
using 3 by auto
qed
lemma Eq⇩ES[meta_subst]:
"[x ❙=⇩E y in v] = (∃ o⇩1 o⇩2. Some (ων o⇩1) = d⇩κ x ∧ Some (ων o⇩2) = d⇩κ y
∧ o⇩1 = o⇩2)"
using Eq⇩EI Eq⇩EE by blast
subsubsection‹Individuals›
text‹\label{TAO_MetaSolver_Identity_Individual}›
lemma EqκI[meta_intro]:
assumes "∃ o⇩1 o⇩2. Some o⇩1 = d⇩κ x ∧ Some o⇩2 = d⇩κ y ∧ o⇩1 = o⇩2"
shows "[x ❙=⇩κ y in v]"
proof -
have "x = y" using assms d⇩κ_inject by meson
moreover have "[x ❙=⇩κ x in v]"
unfolding basic_identity⇩κ_def
apply meta_solver
by (metis (no_types, lifting) assms AbsI Exe1E ν.exhaust)
ultimately show ?thesis by auto
qed
lemma Eqκ_prop:
assumes "[x ❙=⇩κ y in v]"
shows "[φ x in v] = [φ y in v]"
proof -
have "[x ❙=⇩E y ❙∨ ⦇A!,x⦈ ❙& ⦇A!,y⦈ ❙& ❙□(❙∀ F. ⦃x,F⦄ ❙≡ ⦃y,F⦄) in v]"
using assms unfolding basic_identity⇩κ_def by simp
moreover {
assume "[x ❙=⇩E y in v]"
hence "(∃ o⇩1 o⇩2. Some o⇩1 = d⇩κ x ∧ Some o⇩2 = d⇩κ y ∧ o⇩1 = o⇩2)"
using Eq⇩EE by fast
}
moreover {
assume 1: "[⦇A!,x⦈ ❙& ⦇A!,y⦈ ❙& ❙□(❙∀ F. ⦃x,F⦄ ❙≡ ⦃y,F⦄) in v]"
hence 2: "(∃ o⇩1 o⇩2 X Y. Some o⇩1 = d⇩κ x ∧ Some o⇩2 = d⇩κ y
∧ o⇩1 = αν X ∧ o⇩2 = αν Y)"
using AbsE ConjE by meson
moreover then obtain o⇩1 o⇩2 X Y where 3:
"Some o⇩1 = d⇩κ x ∧ Some o⇩2 = d⇩κ y ∧ o⇩1 = αν X ∧ o⇩2 = αν Y"
by auto
moreover have 4: "[❙□(❙∀ F. ⦃x,F⦄ ❙≡ ⦃y,F⦄) in v]"
using 1 ConjE by blast
hence 6: "∀ v F . [⦃x,F⦄ in v] ⟷ [⦃y,F⦄ in v]"
using BoxE AllE EquivE by fast
hence 7: "∀v r. (∃ o⇩1. Some o⇩1 = d⇩κ x ∧ o⇩1 ∈ en r)
= (∃ o⇩1. Some o⇩1 = d⇩κ y ∧ o⇩1 ∈ en r)"
apply - apply meta_solver
using propex⇩1 d⇩1_inject apply simp
apply transfer by simp
hence 8: "∀ r. (o⇩1 ∈ en r) = (o⇩2 ∈ en r)"
using 3 d⇩κ_inject d⇩κ_proper apply simp
by (metis option.inject)
hence "∀r. (o⇩1 ∈ r) = (o⇩2 ∈ r)"
unfolding en_def using 3
by (metis Collect_cong Collect_mem_eq ν.simps(6)
mem_Collect_eq makeΠ⇩1_cases)
hence "(o⇩1 ∈ { x . o⇩1 = x }) = (o⇩2 ∈ { x . o⇩1 = x })"
by metis
hence "o⇩1 = o⇩2" by simp
hence "(∃ o⇩1 o⇩2. Some o⇩1 = d⇩κ x ∧ Some o⇩2 = d⇩κ y ∧ o⇩1 = o⇩2)"
using 3 by auto
}
ultimately have "x = y"
using DisjS using Semantics.d⇩κ_inject by auto
thus "(v ⊨ (φ x)) = (v ⊨ (φ y))" by simp
qed
lemma EqκE[meta_elim]:
assumes "[x ❙=⇩κ y in v]"
shows "∃ o⇩1 o⇩2. Some o⇩1 = d⇩κ x ∧ Some o⇩2 = d⇩κ y ∧ o⇩1 = o⇩2"
proof -
have "∀ φ . (v ⊨ φ x) = (v ⊨ φ y)"
using assms Eqκ_prop by blast
moreover obtain φ where φ_prop:
"φ = (λ α . make𝗈 (λ w s . (∃ o⇩1 o⇩2. Some o⇩1 = d⇩κ x
∧ Some o⇩2 = d⇩κ α ∧ o⇩1 = o⇩2)))"
by auto
ultimately have "(v ⊨ φ x) = (v ⊨ φ y)" by metis
moreover have "(v ⊨ φ x)"
using assms unfolding φ_prop basic_identity⇩κ_def
by (metis (mono_tags, lifting) AbsS ConjE DisjS
Eq⇩ES valid_in.abs_eq)
ultimately have "(v ⊨ φ y)" by auto
thus ?thesis
unfolding φ_prop
by (simp add: valid_in_def meta_aux)
qed
lemma EqκS[meta_subst]:
"[x ❙=⇩κ y in v] = (∃ o⇩1 o⇩2. Some o⇩1 = d⇩κ x ∧ Some o⇩2 = d⇩κ y ∧ o⇩1 = o⇩2)"
using EqκI EqκE by blast
subsubsection‹One-Place Relations›
text‹\label{TAO_MetaSolver_Identity_OnePlaceRelation}›
lemma Eq⇩1I[meta_intro]: "F = G ⟹ [F ❙=⇩1 G in v]"
unfolding basic_identity⇩1_def
apply (rule BoxI, rule AllI, rule EquivI)
by simp
lemma Eq⇩1E[meta_elim]: "[F ❙=⇩1 G in v] ⟹ F = G"
unfolding basic_identity⇩1_def
apply (drule BoxE, drule_tac x="(αν { F })" in AllE, drule EquivE)
apply (simp add: Semantics.T2)
unfolding en_def d⇩κ_def d⇩1_def
using νκ_proper rep_proper_id
by (simp add: rep_def proper_def meta_aux νκ.rep_eq)
lemma Eq⇩1S[meta_subst]: "[F ❙=⇩1 G in v] = (F = G)"
using Eq⇩1I Eq⇩1E by auto
lemma Eq⇩1_prop: "[F ❙=⇩1 G in v] ⟹ [φ F in v] = [φ G in v]"
using Eq⇩1E by blast
subsubsection‹Two-Place Relations›
text‹\label{TAO_MetaSolver_Identity_TwoPlaceRelation}›
lemma Eq⇩2I[meta_intro]: "F = G ⟹ [F ❙=⇩2 G in v]"
unfolding basic_identity⇩2_def
apply (rule AllI, rule ConjI, (subst Eq⇩1S)+)
by simp
lemma Eq⇩2E[meta_elim]: "[F ❙=⇩2 G in v] ⟹ F = G"
proof -
assume "[F ❙=⇩2 G in v]"
hence 1: "[❙∀ x. (❙λy. ⦇F,x⇧P,y⇧P⦈) ❙=⇩1 (❙λy. ⦇G,x⇧P,y⇧P⦈) in v]"
unfolding basic_identity⇩2_def
apply - apply meta_solver by auto
{
fix u v s w
obtain x where x_def: "νυ x = v" by (metis νυ_surj surj_def)
obtain a where a_def:
"a = (λu s w. ∃xa. νυ xa = u ∧ evalΠ⇩2 F (νυ x) (νυ xa) s w)"
by auto
obtain b where b_def:
"b = (λu s w. ∃xa. νυ xa = u ∧ evalΠ⇩2 G (νυ x) (νυ xa) s w)"
by auto
have "a = b" unfolding a_def b_def
using 1 apply - apply meta_solver
by (auto simp: meta_defs meta_aux makeΠ⇩1_inject)
hence "a u s w = b u s w" by auto
hence "(evalΠ⇩2 F (νυ x) u s w) = (evalΠ⇩2 G (νυ x) u s w)"
unfolding a_def b_def
by (metis (no_types, hide_lams) νυ_surj surj_def)
hence "(evalΠ⇩2 F v u s w) = (evalΠ⇩2 G v u s w)"
unfolding x_def by auto
}
hence "(evalΠ⇩2 F) = (evalΠ⇩2 G)" by blast
thus "F = G" by (simp add: evalΠ⇩2_inject)
qed
lemma Eq⇩2S[meta_subst]: "[F ❙=⇩2 G in v] = (F = G)"
using Eq⇩2I Eq⇩2E by auto
lemma Eq⇩2_prop: "[F ❙=⇩2 G in v] ⟹ [φ F in v] = [φ G in v]"
using Eq⇩2E by blast
subsubsection‹Three-Place Relations›
text‹\label{TAO_MetaSolver_Identity_ThreePlaceRelation}›
lemma Eq⇩3I[meta_intro]: "F = G ⟹ [F ❙=⇩3 G in v]"
apply (simp add: meta_defs meta_aux conn_defs forall_ν_def basic_identity⇩3_def)
using MetaSolver.Eq⇩1I valid_in.rep_eq by auto
lemma Eq⇩3E[meta_elim]: "[F ❙=⇩3 G in v] ⟹ F = G"
proof -
assume "[F ❙=⇩3 G in v]"
hence 1: "[❙∀ x y. (❙λz. ⦇F,x⇧P,y⇧P,z⇧P⦈) ❙=⇩1 (❙λz. ⦇G,x⇧P,y⇧P,z⇧P⦈) in v]"
unfolding basic_identity⇩3_def
apply - apply meta_solver by auto
{
fix u v r s w
obtain x where x_def: "νυ x = v" by (metis νυ_surj surj_def)
obtain y where y_def: "νυ y = r" by (metis νυ_surj surj_def)
obtain a where a_def:
"a = (λu s w. ∃xa. νυ xa = u ∧ evalΠ⇩3 F (νυ x) (νυ y) (νυ xa) s w)"
by auto
obtain b where b_def:
"b = (λu s w. ∃xa. νυ xa = u ∧ evalΠ⇩3 G (νυ x) (νυ y) (νυ xa) s w)"
by auto
have "a = b" unfolding a_def b_def
using 1 apply - apply meta_solver
by (auto simp: meta_defs meta_aux makeΠ⇩1_inject)
hence "a u s w = b u s w" by auto
hence "(evalΠ⇩3 F (νυ x) (νυ y) u s w) = (evalΠ⇩3 G (νυ x) (νυ y) u s w)"
unfolding a_def b_def
by (metis (no_types, hide_lams) νυ_surj surj_def)
hence "(evalΠ⇩3 F v r u s w) = (evalΠ⇩3 G v r u s w)"
unfolding x_def y_def by auto
}
hence "(evalΠ⇩3 F) = (evalΠ⇩3 G)" by blast
thus "F = G" by (simp add: evalΠ⇩3_inject)
qed
lemma Eq⇩3S[meta_subst]: "[F ❙=⇩3 G in v] = (F = G)"
using Eq⇩3I Eq⇩3E by auto
lemma Eq⇩3_prop: "[F ❙=⇩3 G in v] ⟹ [φ F in v] = [φ G in v]"
using Eq⇩3E by blast
subsubsection‹Propositions›
text‹\label{TAO_MetaSolver_Identity_Proposition}›
lemma Eq⇩0I[meta_intro]: "x = y ⟹ [x ❙=⇩0 y in v]"
unfolding basic_identity⇩0_def by (simp add: Eq⇩1S)
lemma Eq⇩0E[meta_elim]: "[F ❙=⇩0 G in v] ⟹ F = G"
proof -
assume "[F ❙=⇩0 G in v]"
hence "[(❙λy. F) ❙=⇩1 (❙λy. G) in v]"
unfolding basic_identity⇩0_def by simp
hence "(❙λy. F) = (❙λy. G)"
using Eq⇩1S by simp
hence "(λu s w. (∃x. νυ x = u) ∧ eval𝗈 F s w)
= (λu s w. (∃x. νυ x = u) ∧ eval𝗈 G s w)"
apply (simp add: meta_defs meta_aux)
by (metis (no_types, lifting) UNIV_I makeΠ⇩1_inverse)
hence "⋀s w.(eval𝗈 F s w) = (eval𝗈 G s w)"
by metis
hence "(eval𝗈 F) = (eval𝗈 G)" by blast
thus "F = G"
by (metis eval𝗈_inverse)
qed
lemma Eq⇩0S[meta_subst]: "[F ❙=⇩0 G in v] = (F = G)"
using Eq⇩0I Eq⇩0E by auto
lemma Eq⇩0_prop: "[F ❙=⇩0 G in v] ⟹ [φ F in v] = [φ G in v]"
using Eq⇩0E by blast
end
end
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 . x⇧P ❙= y⇧P"
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_identity⇩1"
instance proof
fix F G :: Π⇩1 and w φ
show "(w ⊨ F ❙= G) ⟹ (w ⊨ φ F) ⟹ (w ⊨ φ G)"
unfolding identity_Π⇩1_def using MetaSolver.Eq⇩1_prop ..
qed
end
instantiation Π⇩2 :: identifiable
begin
definition identity_Π⇩2 where "identity_Π⇩2 ≡ basic_identity⇩2"
instance proof
fix F G :: Π⇩2 and w φ
show "(w ⊨ F ❙= G) ⟹ (w ⊨ φ F) ⟹ (w ⊨ φ G)"
unfolding identity_Π⇩2_def using MetaSolver.Eq⇩2_prop ..
qed
end
instantiation Π⇩3 :: identifiable
begin
definition identity_Π⇩3 where "identity_Π⇩3 ≡ basic_identity⇩3"
instance proof
fix F G :: Π⇩3 and w φ
show "(w ⊨ F ❙= G) ⟹ (w ⊨ φ F) ⟹ (w ⊨ φ G)"
unfolding identity_Π⇩3_def using MetaSolver.Eq⇩3_prop ..
qed
end
instantiation 𝗈 :: identifiable
begin
definition identity_𝗈 where "identity_𝗈 ≡ basic_identity⇩0"
instance proof
fix F G :: 𝗈 and w φ
show "(w ⊨ F ❙= G) ⟹ (w ⊨ φ F) ⟹ (w ⊨ φ G)"
unfolding identity_𝗈_def using MetaSolver.Eq⇩0_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 identity⇩E_def[identity_defs]:
"basic_identity⇩E ≡ ❙λ⇧2 (λx y. ⦇O!,x⇧P⦈ ❙& ⦇O!,y⇧P⦈ ❙& ❙□(❙∀F. ⦇F,x⇧P⦈ ❙≡ ⦇F,y⇧P⦈))"
unfolding basic_identity⇩E_def forall_Π⇩1_def by simp
lemma identity⇩E_infix_def[identity_defs]:
"x ❙=⇩E y ≡ ⦇basic_identity⇩E,x,y⦈" using basic_identity⇩E_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. (x⇧P) ❙=⇩E (y⇧P) ❙∨ ⦇A!,x⇧P⦈ ❙& ⦇A!,y⇧P⦈ ❙& ❙□(❙∀ F. ⦃x⇧P,F⦄ ❙≡ ⦃y⇧P,F⦄)"
unfolding identity_ν_def identity⇩κ_def by simp
lemma identity⇩1_def[identity_defs]:
"(❙=) ≡ λF G. ❙□(❙∀ x . ⦃x⇧P,F⦄ ❙≡ ⦃x⇧P,G⦄)"
unfolding identity_Π⇩1_def basic_identity⇩1_def forall_ν_def by simp
lemma identity⇩2_def[identity_defs]:
"(❙=) ≡ λF G. ❙∀ x. (❙λy. ⦇F,x⇧P,y⇧P⦈) ❙= (❙λy. ⦇G,x⇧P,y⇧P⦈)
❙& (❙λy. ⦇F,y⇧P,x⇧P⦈) ❙= (❙λy. ⦇G,y⇧P,x⇧P⦈)"
unfolding identity_Π⇩2_def identity_Π⇩1_def basic_identity⇩2_def forall_ν_def by simp
lemma identity⇩3_def[identity_defs]:
"(❙=) ≡ λF G. ❙∀ x y. (❙λz. ⦇F,z⇧P,x⇧P,y⇧P⦈) ❙= (❙λz. ⦇G,z⇧P,x⇧P,y⇧P⦈)
❙& (❙λz. ⦇F,x⇧P,z⇧P,y⇧P⦈) ❙= (❙λz. ⦇G,x⇧P,z⇧P,y⇧P⦈)
❙& (❙λz. ⦇F,x⇧P,y⇧P,z⇧P⦈) ❙= (❙λz. ⦇G,x⇧P,y⇧P,z⇧P⦈)"
unfolding identity_Π⇩3_def identity_Π⇩1_def basic_identity⇩3_def forall_ν_def by simp
lemma identity⇩𝗈_def[identity_defs]: "(❙=) ≡ λF G. (❙λy. F) ❙= (❙λy. G)"
unfolding identity_𝗈_def identity_Π⇩1_def basic_identity⇩0_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}
›
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] ⟶ (∃ o⇩1 . Some o⇩1 = 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] ⟶ (∃ o⇩1 . Some o⇩1 = 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
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!,x⇧P⦈ ❙& ❙◇❙¬⦇E!,x⇧P⦈) ❙& ❙◇❙¬(❙∃x. ⦇E!,x⇧P⦈ ❙& ❙◇❙¬⦇E!,x⇧P⦈)]]"
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]:
"[[x⇧P ❙= (❙ιx. φ x) ❙≡ (❙∀z.(❙𝒜(φ z) ❙≡ z ❙= x))]]"
unfolding axiom_def
proof (rule allI, rule EquivI; rule)
fix v
assume "[x⇧P ❙= (❙ιx. φ x) in v]"
moreover hence 1:
"∃o⇩1 o⇩2. Some o⇩1 = d⇩κ (x⇧P) ∧ Some o⇩2 = d⇩κ (❙ιx. φ x) ∧ o⇩1 = o⇩2"
apply - unfolding identity_κ_def by meta_solver
then obtain o⇩1 o⇩2 where 2:
"Some o⇩1 = d⇩κ (x⇧P) ∧ Some o⇩2 = d⇩κ (❙ιx. φ x) ∧ o⇩1 = o⇩2"
by auto
hence 3:
"(∃ x .((w⇩0 ⊨ φ x) ∧ (∀y. (w⇩0 ⊨ φ y) ⟶ y = x)))
∧ d⇩κ (❙ιx. φ x) = Some (THE x. (w⇩0 ⊨ φ x))"
using D3 by (metis option.distinct(1))
then obtain X where 4:
"((w⇩0 ⊨ φ X) ∧ (∀y. (w⇩0 ⊨ φ y) ⟶ y = X))"
by auto
moreover have "o⇩1 = (THE x. (w⇩0 ⊨ φ x))"
using 2 3 by auto
ultimately have 5: "X = o⇩1"
by (metis (mono_tags) theI)
have "∀ z . [❙𝒜φ z in v] = [(z⇧P) ❙= (x⇧P) in v]"
proof
fix z
have "[❙𝒜φ z in v] ⟹ [(z⇧P) ❙= (x⇧P) in v]"
unfolding identity_κ_def apply meta_solver
using 4 5 2 d⇩κ_proper w⇩0_def by auto
moreover have "[(z⇧P) ❙= (x⇧P) in v] ⟹ [❙𝒜φ z in v]"
unfolding identity_κ_def apply meta_solver
using 2 4 5
by (simp add: d⇩κ_proper w⇩0_def)
ultimately show "[❙𝒜φ z in v] = [(z⇧P) ❙= (x⇧P) 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) = (∃o⇩1 o⇩2. Some o⇩1 = d⇩κ (z⇧P)
∧ Some o⇩2 = d⇩κ (x⇧P) ∧ o⇩1 = o⇩2)"
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 "x⇧P = (❙ιx. φ x)"
using D3 d⇩κ_inject d⇩κ_proper w⇩0_def by presburger
thus "[x⇧P ❙= (❙ι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 . φ (x⇧P), x⇧P⦈ ❙≡ φ (x⇧P)]]"
apply axiom_meta_solver
using D5_1[OF assms] d⇩κ_proper propex⇩1
by metis
lemma lambda_predicates_2_2[axiom]:
assumes "IsProperInXY φ"
shows "[[⦇(❙λ⇧2 (λ x y . φ (x⇧P) (y⇧P))), x⇧P, y⇧P⦈ ❙≡ φ (x⇧P) (y⇧P)]]"
apply axiom_meta_solver
using D5_2[OF assms] d⇩κ_proper propex⇩2
by metis
lemma lambda_predicates_2_3[axiom]:
assumes "IsProperInXYZ φ"
shows "[[⦇(❙λ⇧3 (λ x y z . φ (x⇧P) (y⇧P) (z⇧P))),x⇧P,y⇧P,z⇧P⦈ ❙≡ φ (x⇧P) (y⇧P) (z⇧P)]]"
proof -
have "[[⦇(❙λ⇧3 (λ x y z . φ (x⇧P) (y⇧P) (z⇧P))),x⇧P,y⇧P,z⇧P⦈ ❙→ φ (x⇧P) (y⇧P) (z⇧P)]]"
apply axiom_meta_solver using D5_3[OF assms] by auto
moreover have
"[[φ (x⇧P) (y⇧P) (z⇧P) ❙→ ⦇(❙λ⇧3 (λ x y z . φ (x⇧P) (y⇧P) (z⇧P))),x⇧P,y⇧P,z⇧P⦈]]"
apply axiom_meta_solver
using D5_3[OF assms] d⇩κ_proper propex⇩3
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, x⇧P⦈) ❙= F]]"
unfolding axiom_def
apply (rule allI)
unfolding identity_Π⇩1_def apply (rule Eq⇩1I)
using D4_1 d⇩1_inject by simp
lemma lambda_predicates_3_2[axiom]:
"[[(❙λ⇧2 (λ x y . ⦇F, x⇧P, y⇧P⦈)) ❙= F]]"
unfolding axiom_def
apply (rule allI)
unfolding identity_Π⇩2_def apply (rule Eq⇩2I)
using D4_2 d⇩2_inject by simp
lemma lambda_predicates_3_3[axiom]:
"[[(❙λ⇧3 (λ x y z . ⦇F, x⇧P, y⇧P, z⇧P⦈)) ❙= F]]"
unfolding axiom_def
apply (rule allI)
unfolding identity_Π⇩3_def apply (rule Eq⇩3I)
using D4_3 d⇩3_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 Eq⇩0I)
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 Eq⇩1I)
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 Eq⇩2I)
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 Eq⇩3I)
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!,x⇧P⦈ ❙& (❙∀ F . (⦃x⇧P,F⦄ ❙≡ φ F))]]"
unfolding axiom_def
proof (rule allI, rule ExIRule)
fix v
let ?x = "αν { F . [φ F in v]}"
have "[⦇A!,?x⇧P⦈ in v]" by (simp add: AbsS d⇩κ_proper)
moreover have "[(❙∀F. ⦃?x⇧P,F⦄ ❙≡ φ F) in v]"
apply meta_solver unfolding en_def
using d⇩1.rep_eq d⇩κ_def d⇩κ_proper evalΠ⇩1_inverse by auto
ultimately show "[⦇A!,?x⇧P⦈ ❙& (❙∀F. ⦃?x⇧P,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 propnot⇩0 ≡ "propnot :: Π⇩0⇒Π⇩0"
propnot⇩1 ≡ "propnot :: Π⇩1⇒Π⇩1"
propnot⇩2 ≡ "propnot :: Π⇩2⇒Π⇩2"
propnot⇩3 ≡ "propnot :: Π⇩3⇒Π⇩3"
begin
definition propnot⇩0 :: "Π⇩0⇒Π⇩0" where
"propnot⇩0 ≡ λ p . ❙λ⇧0 (❙¬p)"
definition propnot⇩1 where
"propnot⇩1 ≡ λ F . ❙λ x . ❙¬⦇F, x⇧P⦈"
definition propnot⇩2 where
"propnot⇩2 ≡ λ F . ❙λ⇧2 (λ x y . ❙¬⦇F, x⇧P, y⇧P⦈)"
definition propnot⇩3 where
"propnot⇩3 ≡ λ F . ❙λ⇧3 (λ x y z . ❙¬⦇F, x⇧P, y⇧P, z⇧P⦈)"
end
named_theorems propnot_defs
declare propnot⇩0_def[propnot_defs] propnot⇩1_def[propnot_defs]
propnot⇩2_def[propnot_defs] propnot⇩3_def[propnot_defs]
subsection‹Noncontingent and Contingent Relations›
consts Necessary :: "'a⇒𝗈"
overloading Necessary⇩0 ≡ "Necessary :: Π⇩0⇒𝗈"
Necessary⇩1 ≡ "Necessary :: Π⇩1⇒𝗈"
Necessary⇩2 ≡ "Necessary :: Π⇩2⇒𝗈"
Necessary⇩3 ≡ "Necessary :: Π⇩3⇒𝗈"
begin
definition Necessary⇩0 where
"Necessary⇩0 ≡ λ p . ❙□p"
definition Necessary⇩1 :: "Π⇩1⇒𝗈" where
"Necessary⇩1 ≡ λ F . ❙□(❙∀ x . ⦇F,x⇧P⦈)"
definition Necessary⇩2 where
"Necessary⇩2 ≡ λ F . ❙□(❙∀ x y . ⦇F,x⇧P,y⇧P⦈)"
definition Necessary⇩3 where
"Necessary⇩3 ≡ λ F . ❙□(❙∀ x y z . ⦇F,x⇧P,y⇧P,z⇧P⦈)"
end
named_theorems Necessary_defs
declare Necessary⇩0_def[Necessary_defs] Necessary⇩1_def[Necessary_defs]
Necessary⇩2_def[Necessary_defs] Necessary⇩3_def[Necessary_defs]
consts Impossible :: "'a⇒𝗈"
overloading Impossible⇩0 ≡ "Impossible :: Π⇩0⇒𝗈"
Impossible⇩1 ≡ "Impossible :: Π⇩1⇒𝗈"
Impossible⇩2 ≡ "Impossible :: Π⇩2⇒𝗈"
Impossible⇩3 ≡ "Impossible :: Π⇩3⇒𝗈"
begin
definition Impossible⇩0 where
"Impossible⇩0 ≡ λ p . ❙□❙¬p"
definition Impossible⇩1 where
"Impossible⇩1 ≡ λ F . ❙□(❙∀ x. ❙¬⦇F,x⇧P⦈)"
definition Impossible⇩2 where
"Impossible⇩2 ≡ λ F . ❙□(❙∀ x y. ❙¬⦇F,x⇧P,y⇧P⦈)"
definition Impossible⇩3 where
"Impossible⇩3 ≡ λ F . ❙□(❙∀ x y z. ❙¬⦇F,x⇧P,y⇧P,z⇧P⦈)"
end
named_theorems Impossible_defs
declare Impossible⇩0_def[Impossible_defs] Impossible⇩1_def[Impossible_defs]
Impossible⇩2_def[Impossible_defs] Impossible⇩3_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,x⇧P⦈ ❙→ ❙□⦇F,x⇧P⦈)"
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 (x⇧P))"
definition UniversalObject :: "κ" ("❙a⇩V") where
"UniversalObject ≡ (❙ιx . Universal (x⇧P))"
subsection‹Propositional Properties›
definition Propositional where
"Propositional F ≡ ❙∃ p . F ❙= (❙λ x . p)"
subsection‹Indiscriminate Properties›
definition Indiscriminate :: "Π⇩1⇒𝗈" where
"Indiscriminate ≡ λ F . ❙□((❙∃ x . ⦇F,x⇧P⦈) ❙→ (❙∀ x . ⦇F,x⇧P⦈))"
subsection‹Miscellaneous›
definition not_identical⇩E :: "κ⇒κ⇒𝗈" (infixl "❙≠⇩E" 63)
where "not_identical⇩E ≡ λ x y . ⦇(❙λ⇧2 (λ x y . x⇧P ❙=⇩E y⇧P))⇧-, 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 . ((x⇧P) ❙=⇩E (y⇧P)) ❙≡ (⦇O!,x⇧P⦈ ❙& ⦇O!,y⇧P⦈
❙& ❙□(❙∀F . ⦇F,x⇧P⦈ ❙≡ ⦇F,y⇧P⦈)) in v]"
unfolding identity⇩E_infix_def identity⇩E_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 identity⇩E_infix_def
apply (rule SimpleExOrEnc.intros)
using 1 unfolding identity⇩E_infix_def by auto
moreover have "[❙∃ β . (β⇧P) ❙= y in v]"
apply (rule cqt_5_mod[where ψ="λ y . x ❙=⇩E y",axiom_instance,deduction])
unfolding identity⇩E_infix_def
apply (rule SimpleExOrEnc.intros) using 1
unfolding identity⇩E_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 . ((x⇧P) ❙=⇩E (y⇧P)) ❙≡ (⦇O!,x⇧P⦈ ❙& ⦇O!,y⇧P⦈
❙& ❙□(❙∀F . ⦇F,x⇧P⦈ ❙≡ ⦇F,y⇧P⦈)) in v]"
unfolding identity⇩E_def identity⇩E_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]: "[(x⇧P) ❙= (x⇧P) in v]"
proof -
have "[(❙◇⦇E!, x⇧P⦈) ❙∨ (❙¬❙◇⦇E!, x⇧P⦈) in v]"
using PLM.oth_class_taut_2 by simp
hence "[(❙◇⦇E!, x⇧P⦈) in v] ∨ [(❙¬❙◇⦇E!, x⇧P⦈) in v]"
using CP "❙∨E"(1) by blast
moreover {
assume "[(❙◇⦇E!, x⇧P⦈) in v]"
hence "[⦇❙λx. ❙◇⦇E!,x⇧P⦈,x⇧P⦈ in v]"
apply (rule lambda_predicates_2_1[axiom_instance, equiv_rl, rotated])
by show_proper
hence "[⦇❙λx. ❙◇⦇E!,x⇧P⦈,x⇧P⦈ ❙& ⦇❙λx. ❙◇⦇E!,x⇧P⦈,x⇧P⦈
❙& ❙□(❙∀F. ⦇F,x⇧P⦈ ❙≡ ⦇F,x⇧P⦈) in v]"
apply - by PLM_solver
hence "[(x⇧P) ❙=⇩E (x⇧P) in v]"
using eq_E_simple_1[equiv_rl] unfolding Ordinary_def by fast
}
moreover {
assume "[(❙¬❙◇⦇E!, x⇧P⦈) in v]"
hence "[⦇❙λx. ❙¬❙◇⦇E!,x⇧P⦈,x⇧P⦈ in v]"
apply (rule lambda_predicates_2_1[axiom_instance, equiv_rl, rotated])
by show_proper
hence "[⦇❙λx. ❙¬❙◇⦇E!,x⇧P⦈,x⇧P⦈ ❙& ⦇❙λx. ❙¬❙◇⦇E!,x⇧P⦈,x⇧P⦈
❙& ❙□(❙∀F. ⦃x⇧P,F⦄ ❙≡ ⦃x⇧P,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]:
"[((x⇧P) ❙= (y⇧P)) ❙→ ((y⇧P) ❙= (x⇧P)) in v]"
by (meson l_identity[axiom_instance] id_eq_obj_1 CP ded_thm_cor_3)
lemma id_eq_obj_3[PLM]:
"[((x⇧P) ❙= (y⇧P)) ❙& ((y⇧P) ❙= (z⇧P)) ❙→ ((x⇧P) ❙= (z⇧P)) 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 identity⇩E_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]:
"[