Theory TAO_2_Semantics

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

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

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

locale Semantics
begin
  named_theorems semantics

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

named_theorems IsProper_intros

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

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

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

method show_proper = (fast intro: IsProper_intros)

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

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

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

(*<*)
end
(*>*)