theory AOT_Definitions
  imports AOT_semantics
begin

section‹Definitions of AOT›

AOT_theorem "conventions:1": ‹φ & ψ ≡_df ¬(φ → ¬ψ)›
  using AOT_conj.
AOT_theorem "conventions:2": ‹φ ∨ ψ ≡_df ¬φ → ψ›
  using AOT_disj.
AOT_theorem "conventions:3": ‹φ ≡ ψ ≡_df (φ → ψ) & (ψ → φ)›
  using AOT_equiv.
AOT_theorem "conventions:4": ‹∃α φ{α} ≡_df ¬∀α ¬φ{α}›
  using AOT_exists.
AOT_theorem "conventions:5": ‹♢φ ≡_df ¬◻¬φ›
  using AOT_dia.

declare "conventions:1"[AOT_defs] "conventions:2"[AOT_defs]
        "conventions:3"[AOT_defs] "conventions:4"[AOT_defs]
        "conventions:5"[AOT_defs]

notepad
begin
  fix φ ψ χ
  text‹\linelabel{precedence}›
  have "conventions3[1]": ‹«φ → ψ ≡ ¬ψ → ¬φ¬ = «(φ → ψ) ≡ (¬ψ → ¬φ)¬›
    by blast
  have "conventions3[2]": ‹«φ & ψ → χ¬ = «(φ & ψ) → χ¬›
                   and ‹«φ ∨ ψ → χ¬ = «(φ ∨ ψ) → χ¬›
    by blast+
  have "conventions3[3]": ‹«φ ∨ ψ & χ¬ = «(φ ∨ ψ) & χ¬›
                   and ‹«φ & ψ ∨ χ¬ = «(φ & ψ) ∨ χ¬›
     by blast+ ― ‹Note that PLM instead generally uses parenthesis in these cases.›
end


AOT_theorem "existence:1": ‹κ↓ ≡_df ∃F [F]κ›
  by (simp add: AOT_sem_denotes AOT_sem_exists AOT_model_equiv_def)
     (metis AOT_sem_denotes AOT_sem_exe AOT_sem_lambda_beta AOT_sem_lambda_denotes)
AOT_theorem "existence:2": ‹Π↓ ≡_df ∃x₁...∃x_n x₁...x_n[Π]›
  using AOT_sem_denotes AOT_sem_enc_denotes AOT_sem_universal_encoder
  by (simp add: AOT_sem_denotes AOT_sem_exists AOT_model_equiv_def) blast
AOT_theorem "existence:2[1]": ‹Π↓ ≡_df ∃x x[Π]›
  using "existence:2"[of Π] by simp
AOT_theorem "existence:2[2]": ‹Π↓ ≡_df ∃x∃y xy[Π]›
  using "existence:2"[of Π]
  by (simp add: AOT_sem_denotes AOT_sem_exists AOT_model_equiv_def
                AOT_model_denotes_prod_def)
AOT_theorem "existence:2[3]": ‹Π↓ ≡_df ∃x∃y∃z xyz[Π]›
  using "existence:2"[of Π]
  by (simp add: AOT_sem_denotes AOT_sem_exists AOT_model_equiv_def
                AOT_model_denotes_prod_def)
AOT_theorem "existence:2[4]": ‹Π↓ ≡_df ∃x₁∃x₂∃x₃∃x₄ x₁x₂x₃x₄[Π]›
  using "existence:2"[of Π]
  by (simp add: AOT_sem_denotes AOT_sem_exists AOT_model_equiv_def
                AOT_model_denotes_prod_def)

AOT_theorem "existence:3": ‹φ↓ ≡_df [λx φ]↓›
  by (simp add: AOT_sem_denotes AOT_model_denotes_o_def AOT_model_equiv_def
                AOT_model_lambda_denotes)

declare "existence:1"[AOT_defs] "existence:2"[AOT_defs] "existence:2[1]"[AOT_defs]
        "existence:2[2]"[AOT_defs] "existence:2[3]"[AOT_defs]
        "existence:2[4]"[AOT_defs] "existence:3"[AOT_defs]


AOT_theorem "oa:1": ‹O! =_df [λx ♢E!x]› using AOT_ordinary .
AOT_theorem "oa:2": ‹A! =_df [λx ¬♢E!x]› using AOT_abstract .

declare "oa:1"[AOT_defs] "oa:2"[AOT_defs]

AOT_theorem "identity:1":
  ‹x = y ≡_df ([O!]x & [O!]y & ◻∀F ([F]x ≡ [F]y)) ∨
 ([A!]x & [A!]y & ◻∀F (x[F] ≡ y[F]))›
  unfolding AOT_model_equiv_def
  using AOT_sem_ind_eq[of _ x y]
  by (simp add: AOT_sem_ordinary AOT_sem_abstract AOT_sem_conj
                AOT_sem_box AOT_sem_equiv AOT_sem_forall AOT_sem_disj AOT_sem_eq
                AOT_sem_denotes)

AOT_theorem "identity:2":
  ‹F = G ≡_df F↓ & G↓ & ◻∀x(x[F] ≡ x[G])›
  using AOT_sem_enc_eq[of _ F G]
  by (auto simp: AOT_model_equiv_def AOT_sem_imp AOT_sem_denotes AOT_sem_eq
                 AOT_sem_conj AOT_sem_forall AOT_sem_box AOT_sem_equiv)

AOT_theorem "identity:3[2]":
  ‹F = G ≡_df F↓ & G↓ & ∀y([λz [F]zy] = [λz [G]zy] & [λz [F]yz] = [λz [G]yz])›
  by (auto simp: AOT_model_equiv_def AOT_sem_proj_id_prop[of _ F G]
                 AOT_sem_proj_id_prod_def AOT_sem_conj AOT_sem_denotes
                 AOT_sem_forall AOT_sem_unary_proj_id AOT_model_denotes_prod_def)
AOT_theorem "identity:3[3]":
  ‹F = G ≡_df F↓ & G↓ & ∀y₁∀y₂([λz [F]zy₁y₂] = [λz [G]zy₁y₂] &
 [λz [F]y₁zy₂] = [λz [G]y₁zy₂] &
 [λz [F]y₁y₂z] = [λz [G]y₁y₂z])›
  by (auto simp: AOT_model_equiv_def AOT_sem_proj_id_prop[of _ F G]
                 AOT_sem_proj_id_prod_def AOT_sem_conj AOT_sem_denotes
                 AOT_sem_forall AOT_sem_unary_proj_id AOT_model_denotes_prod_def)
AOT_theorem "identity:3[4]":
  ‹F = G ≡_df F↓ & G↓ & ∀y₁∀y₂∀y₃([λz [F]zy₁y₂y₃] = [λz [G]zy₁y₂y₃] &
 [λz [F]y₁zy₂y₃] = [λz [G]y₁zy₂y₃] &
 [λz [F]y₁y₂zy₃] = [λz [G]y₁y₂zy₃] &
 [λz [F]y₁y₂y₃z] = [λz [G]y₁y₂y₃z])›
  by (auto simp: AOT_model_equiv_def AOT_sem_proj_id_prop[of _ F G]
                 AOT_sem_proj_id_prod_def AOT_sem_conj AOT_sem_denotes
                 AOT_sem_forall AOT_sem_unary_proj_id AOT_model_denotes_prod_def)
AOT_theorem "identity:3":
  ‹F = G ≡_df F↓ & G↓ & ∀x₁...∀x_n «AOT_sem_proj_id x₁x_n (λ τ . AOT_exe F τ)
 (λ τ . AOT_exe G τ)¬›
  by (auto simp: AOT_model_equiv_def AOT_sem_proj_id_prop[of _ F G]
                 AOT_sem_proj_id_prod_def AOT_sem_conj AOT_sem_denotes
                 AOT_sem_forall AOT_sem_unary_proj_id AOT_model_denotes_prod_def)

AOT_theorem "identity:4":
  ‹p = q ≡_df p↓ & q↓ & [λx p] = [λx q]›
  by (auto simp: AOT_model_equiv_def AOT_sem_eq AOT_sem_denotes AOT_sem_conj
                 AOT_model_lambda_denotes AOT_sem_lambda_eq_prop_eq)

declare "identity:1"[AOT_defs] "identity:2"[AOT_defs] "identity:3[2]"[AOT_defs]
        "identity:3[3]"[AOT_defs] "identity:3[4]"[AOT_defs] "identity:3"[AOT_defs]
        "identity:4"[AOT_defs]

AOT_define AOT_nonidentical :: ‹τ → τ → φ› (infixl ‹≠› 50)
  "=-infix": ‹τ ≠ σ ≡_df ¬(τ = σ)›

context AOT_meta_syntax
begin
notation AOT_nonidentical (infixl ‹\≠› 50)
end
context AOT_no_meta_syntax
begin
no_notation AOT_nonidentical (infixl ‹\≠› 50)
end


text‹The following are purely technical pseudo-definitions required due to
 our internal implementation of n-ary relations and ellipses using tuples.›
AOT_theorem tuple_denotes: ‹«(τ,τ')¬↓ ≡_df τ↓ & τ'↓›
  by (simp add: AOT_model_denotes_prod_def AOT_model_equiv_def
                AOT_sem_conj AOT_sem_denotes)
AOT_theorem tuple_identity_1: ‹«(τ,τ')¬ = «(σ, σ')¬ ≡_df (τ = σ) & (τ' = σ')›
  by (auto simp: AOT_model_equiv_def AOT_sem_conj AOT_sem_eq
                 AOT_model_denotes_prod_def AOT_sem_denotes)
AOT_theorem tuple_forall: ‹∀α₁...∀α_n φ{α₁...α_n} ≡_df ∀α₁(∀α₂...∀α_n φ{«(α₁, α₂α_n)¬})›
  by (auto simp: AOT_model_equiv_def AOT_sem_forall AOT_sem_denotes
                 AOT_model_denotes_prod_def)
AOT_theorem tuple_exists: ‹∃α₁...∃α_n φ{α₁...α_n} ≡_df ∃α₁(∃α₂...∃α_n φ{«(α₁, α₂α_n)¬})›
  by (auto simp: AOT_model_equiv_def AOT_sem_exists AOT_sem_denotes
                 AOT_model_denotes_prod_def)
declare tuple_denotes[AOT_defs] tuple_identity_1[AOT_defs] tuple_forall[AOT_defs]
        tuple_exists[AOT_defs]

end