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 ∃x1...∃xn x1...xn[Π]›
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 ∃x1∃x2∃x3∃x4 x1x2x3x4[Π]›
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↓ & ∀y1∀y2([λz [F]zy1y2] = [λz [G]zy1y2] &
[λz [F]y1zy2] = [λz [G]y1zy2] &
[λz [F]y1y2z] = [λz [G]y1y2z])›
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↓ & ∀y1∀y2∀y3([λz [F]zy1y2y3] = [λz [G]zy1y2y3] &
[λz [F]y1zy2y3] = [λz [G]y1zy2y3] &
[λz [F]y1y2zy3] = [λz [G]y1y2zy3] &
[λz [F]y1y2y3z] = [λz [G]y1y2y3z])›
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↓ & ∀x1...∀xn «AOT_sem_proj_id x1xn (λ τ . 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: ‹∀α1...∀αn φ{α1...αn} ≡df ∀α1(∀α2...∀αn φ{«(α1, α2αn)¬})›
by (auto simp: AOT_model_equiv_def AOT_sem_forall AOT_sem_denotes
AOT_model_denotes_prod_def)
AOT_theorem tuple_exists: ‹∃α1...∃αn φ{α1...αn} ≡df ∃α1(∃α2...∃αn φ{«(α1, α2α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
¤ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet am 2026-11-04)
¤
*© Formatika GbR, Deutschland
