(*<*)
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₀ = "j→i→bool"
  type_synonym R₁ = "υ→R₀"
  type_synonym R₂ = "υ→υ→R₀"
  type_synonym R₃ = "υ→υ→υ→R₀"
  type_synonym W = i

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

  lift_definition d_\κ :: "κ→R_\<kappa> option" is id .
  lift_definition d₀ :: "Π₀→R₀ option" is Some .
  lift_definition d₁ :: "Π₁→R₁ option" is Some .
  lift_definition d₂ :: "Π₂→R₂ option" is Some .
  lift_definition d₃ :: "Π₃→R₃ option" is Some .

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

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

  definition ex0 :: "R₀→W→bool"
    where "ex0 ≡ λ F . F dj"
  definition ex1 :: "R₁→W→(R_\<kappa> set)"
    where "ex1 ≡ λ F w . { x . F (νυ x) dj w }"
  definition ex2 :: "R₂→W→((R_\<kappa>×R_\<kappa>) set)"
    where "ex2 ≡ λ F w . { (x,y) . F (νυ x) (νυ y) dj w }"
  definition ex3 :: "R₃→W→((R_\<kappa>×R_\<kappa>×R_\<kappa>) 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₁→(R_\<kappa> set)"
    where "en ≡ λ F . { x . case x of αν y → makeΠ₁ (λ x . F x) ∈ y
                                       | _ → False }"

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

  named_theorems semantics_defs
  declare d₀_def[semantics_defs] d₁_def[semantics_defs]
          d₂_def[semantics_defs] d₃_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₀_def[semantics_defs]

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

  lemma T1_1[semantics]:
    "(w ⊨ (F,x)) = (∃ r o₁ . Some r = d₁ F ∧ Some o₁ = d_\<kappa> x ∧ o₁ ∈ 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₁ o₂ . Some r = d₂ F ∧ Some o₁ = d_\<kappa> x
                               ∧ Some o₂ = d_\<kappa> y ∧ (o₁, o₂) ∈ 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₁ o₂ o₃ . Some r = d₃ F ∧ Some o₁ = d_\<kappa> x
                                    ∧ Some o₂ = d_\<kappa> y ∧ Some o₃ = d_\<kappa> z
                                    ∧ (o₁, o₂, o₃) ∈ 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₀ 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₁ . Some r = d₁ F ∧ Some o₁ = d_\<kappa> x ∧ o₁ ∈ 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 ⊨ \<not>ψ) = (¬(w ⊨ ψ))"
    by (simp add: meta_defs meta_aux)

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

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

  lemma T7[semantics]: "(w ⊨ \<A>ψ) = (dw ⊨ ψ)"
    by (simp add: meta_defs meta_aux)

  lemma T8_ν[semantics]: "(w ⊨ \<forall>_\<nu> x. ψ x) = (∀ x . (w ⊨ ψ x))"
    by (simp add: meta_defs meta_aux)

  lemma T8_0[semantics]: "(w ⊨ \<forall>₀ x. ψ x) = (∀ x . (w ⊨ ψ x))"
    by (simp add: meta_defs meta_aux)

  lemma T8_1[semantics]: "(w ⊨ \<forall>₁ x. ψ x) = (∀ x . (w ⊨ ψ x))"
    by (simp add: meta_defs meta_aux)

  lemma T8_2[semantics]: "(w ⊨ \<forall>₂ x. ψ x) = (∀ x . (w ⊨ ψ x))"
    by (simp add: meta_defs meta_aux)

  lemma T8_3[semantics]: "(w ⊨ \<forall>₃ x. ψ x) = (∀ x . (w ⊨ ψ x))"
    by (simp add: meta_defs meta_aux)

  lemma T8_o[semantics]: "(w ⊨ \<forall>_\<o> 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_\<kappa> (\<iota>x . ψ x) = (if (∃x . (w₀ ⊨ ψ x) ∧ (∀ y . (w₀ ⊨ ψ y) ⟶ y = x))
                      then (Some (THE x . (w₀ ⊨ ψ 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₁ (\<lambda> x . (F, x^P)) = d₁ F"
    by (simp add: meta_defs meta_aux)

  lemma D4_2[semantics]: "d₂ (\<lambda>² (λ x y . (F, x^P, y^P))) = d₂ F"
    by (simp add: meta_defs meta_aux)

  lemma D4_3[semantics]: "d₃ (\<lambda>³ (λ x y z . (F, x^P, y^P, z^P))) = d₃ F"
    by (simp add: meta_defs meta_aux)

  lemma D5_1[semantics]:
    assumes "IsProperInX φ"
    shows "∧ w o₁ r . Some r = d₁ (\<lambda> x . (φ (x^P))) ∧ Some o₁ = d_\<kappa> x
                      ⟶ (o₁ ∈ 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₁ o₂ r . Some r = d₂ (\<lambda>² (λ x y . φ (x^P) (y^P)))
                       ∧ Some o₁ = d_\<kappa> x ∧ Some o₂ = d_\<kappa> y
                       ⟶ ((o₁,o₂) ∈ 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₁ o₂ o₃ r . Some r = d₃ (\<lambda>³ (λ x y z . φ (x^P) (y^P) (z^P)))
                          ∧ Some o₁ = d_\<kappa> x ∧ Some o₂ = d_\<kappa> y ∧ Some o₃ = d_\<kappa> z
                          ⟶ ((o₁,o₂,o₃) ∈ 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₀ (\<lambda>⁰ φ) ⟶ 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₀: "∃ r . Some r = d₀ F"
    unfolding d₀_def by simp
  lemma propex₁: "∃ r . Some r = d₁ F"
    unfolding d₁_def by simp
  lemma propex₂: "∃ r . Some r = d₂ F"
    unfolding d₂_def by simp
  lemma propex₃: "∃ r . Some r = d₃ F"
    unfolding d₃_def by simp
  lemma d_\κ_proper: "d_\<kappa> (u^P) = Some u"
    unfolding d_\κ_def by (simp add: νκ_def meta_aux)
  lemma ConcretenessSemantics1:
    "Some r = d₁ E! ==> (∃ w . ψν x ∈ ex1 r w)"
    unfolding semantics_defs apply transfer
    by (simp add: OrdinaryObjectsPossiblyConcreteAxiom νυ_ψν_is_ψυ)
  lemma ConcretenessSemantics2:
    "Some r = d₁ E! ==> (x ∈ ex1 r w ⟶ (∃y. x = ψν y))"
    unfolding semantics_defs apply transfer apply simp
    by (metis ν.exhaust υ.exhaust υ.simps(6) no_αψ)
  lemma d₀_inject: "∧x y. d₀ x = d₀ y ==> x = y"
    unfolding d₀_def by (simp add: evalo_inject)
  lemma d₁_inject: "∧x y. d₁ x = d₁ y ==> x = y"
    unfolding d₁_def by (simp add: evalΠ₁_inject)
  lemma d₂_inject: "∧x y. d₂ x = d₂ y ==> x = y"
    unfolding d₂_def by (simp add: evalΠ₂_inject)
  lemma d₃_inject: "∧x y. d₃ x = d₃ y ==> x = y"
    unfolding d₃_def by (simp add: evalΠ₃_inject)
  lemma d_\κ_inject: "∧x y o₁. Some o₁ = d_\<kappa> x ∧ Some o₁ = d_\<kappa> y ==> x = y"
  proof -
    fix x :: κ and y :: κ and o₁ :: ν
    assume "Some o₁ = d_\<kappa> x ∧ Some o₁ = d_\<kappa> 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 *)
(*<*) unbundle no list_enumeration_syntax and no list_comprehension_syntax (*>*) 

abbreviation validity_in :: "o→i→bool" (‹[_ in _]› [1]) where
  "validity_in ≡ λ φ v . v ⊨ φ"
definition actual_validity :: "o→bool" (‹[_]› [1]) where
  "actual_validity ≡ λ φ . dw ⊨ φ"
definition necessary_validity :: "o→bool" (‹◻[_]› [1]) where
  "necessary_validity ≡ λ φ . ∀ v . (v ⊨ φ)"

(*<*)
end
(*>*)