# 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

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 ⊨ ψ))"

lemma T5[semantics]: "(w ⊨ ψ ❙→ χ) = (¬(w ⊨ ψ) ∨ (w ⊨ χ))"

lemma T6[semantics]: "(w ⊨ ❙□ψ) = (∀ v . (v ⊨ ψ))"

lemma T7[semantics]: "(w ⊨ ❙𝒜ψ) = (dw ⊨ ψ)"

lemma T8_ν[semantics]: "(w ⊨ ❙∀⇩ν x. ψ x) = (∀ x . (w ⊨ ψ x))"

lemma T8_0[semantics]: "(w ⊨ ❙∀⇩0 x. ψ x) = (∀ x . (w ⊨ ψ x))"

lemma T8_1[semantics]: "(w ⊨ ❙∀⇩1 x. ψ x) = (∀ x . (w ⊨ ψ x))"

lemma T8_2[semantics]: "(w ⊨ ❙∀⇩2 x. ψ x) = (∀ x . (w ⊨ ψ x))"

lemma T8_3[semantics]: "(w ⊨ ❙∀⇩3 x. ψ x) = (∀ x . (w ⊨ ψ x))"

lemma T8_𝗈[semantics]: "(w ⊨ ❙∀⇩𝗈 x. ψ x) = (∀ x . (w ⊨ ψ x))"

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"

lemma D4_2[semantics]: "d⇩2 (❙λ⇧2 (λ x y . ⦇F, x⇧P, y⇧P⦈)) = d⇩2 F"

lemma D4_3[semantics]: "d⇩3 (❙λ⇧3 (λ x y z . ⦇F, x⇧P, y⇧P, z⇧P⦈)) = d⇩3 F"

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
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 . χ
― ‹one place:› (λ F . ⦇F,x⦈)
― ‹two place:› (λ F . ⦇F,x,x⦈) (λ F a . ⦇F,x,a⦈) (λ F a . ⦇F,a,x⦈)
― ‹three place three ‹x›:› (λ F . ⦇F,x,x,x⦈)
― ‹three place two ‹x›:› (λ F a . ⦇F,x,x,a⦈) (λ F a . ⦇F,x,a,x⦈)
(λ F a . ⦇F,a,x,x⦈)
― ‹three place one ‹x›:› (λ F a b. ⦇F,x,a,b⦈) (λ F a b. ⦇F,a,x,b⦈)
(λ F a b . ⦇F,a,b,x⦈))"
unfolding IsProperInX_def
by (auto simp: meta_defs meta_aux)

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

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

method show_proper = (fast intro: IsProper_intros)

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

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

abbreviation validity_in :: "𝗈⇒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
(*>*)