Theory TAO_2_Semantics

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

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

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

locale Semantics
begin
  named_theorems semantics

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

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

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

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

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

  definition ex0 :: "R0⇒W⇒bool"
    where "ex0 ≡ λ F . F dj"
  definition ex1 :: "R1⇒W⇒(Rκ set)"
    where "ex1 ≡ λ F w . { x . F (νυ x) dj w }"
  definition ex2 :: "R2⇒W⇒((Rκ×Rκ) set)"
    where "ex2 ≡ λ F w . { (x,y) . F (νυ x) (νυ y) dj w }"
  definition ex3 :: "R3⇒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 :: "R1⇒(Rκ set)"
    where "en ≡ λ F . { x . case x of αν y ⇒ makeΠ1 (λ x . F x) ∈ y
                                       | _ ⇒ False }"

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

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

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

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

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

  lemma T1_3[semantics]:
    "(w ⊨ ⦇F,x,y,z⦈) = (∃ r o1 o2 o3 . Some r = d3 F ∧ Some o1 = dκ x
                                    ∧ Some o2 = dκ y ∧ Some o3 = dκ z
                                    ∧ (o1, o2, o3) ∈ ex3 r w)"
    unfolding semantics_defs
    apply (simp add: meta_defs meta_aux rep_def proper_def)
    by (metis option.discI option.exhaust option.sel)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

named_theorems IsProper_intros

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

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

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

method show_proper = (fast intro: IsProper_intros)

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

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

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