Theory AOT_Definitions
theory AOT_Definitions
imports AOT_semantics
begin
section‹Definitions of AOT›
AOT_theorem "conventions:1": ‹φ & ψ ≡⇩d⇩f ¬(φ → ¬ψ)›
using AOT_conj.
AOT_theorem "conventions:2": ‹φ ∨ ψ ≡⇩d⇩f ¬φ → ψ›
using AOT_disj.
AOT_theorem "conventions:3": ‹φ ≡ ψ ≡⇩d⇩f (φ → ψ) & (ψ → φ)›
using AOT_equiv.
AOT_theorem "conventions:4": ‹∃α φ{α} ≡⇩d⇩f ¬∀α ¬φ{α}›
using AOT_exists.
AOT_theorem "conventions:5": ‹◇φ ≡⇩d⇩f ¬□¬φ›
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+
end
AOT_theorem "existence:1": ‹κ↓ ≡⇩d⇩f ∃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": ‹Π↓ ≡⇩d⇩f ∃x⇩1...∃x⇩n x⇩1...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]": ‹Π↓ ≡⇩d⇩f ∃x x[Π]›
using "existence:2"[of Π] by simp
AOT_theorem "existence:2[2]": ‹Π↓ ≡⇩d⇩f ∃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]": ‹Π↓ ≡⇩d⇩f ∃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]": ‹Π↓ ≡⇩d⇩f ∃x⇩1∃x⇩2∃x⇩3∃x⇩4 x⇩1x⇩2x⇩3x⇩4[Π]›
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": ‹φ↓ ≡⇩d⇩f [λx φ]↓›
by (simp add: AOT_sem_denotes AOT_model_denotes_𝗈_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! =⇩d⇩f [λx ◇E!x]› using AOT_ordinary .
AOT_theorem "oa:2": ‹A! =⇩d⇩f [λx ¬◇E!x]› using AOT_abstract .
declare "oa:1"[AOT_defs] "oa:2"[AOT_defs]
AOT_theorem "identity:1":
‹x = y ≡⇩d⇩f ([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 ≡⇩d⇩f 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 ≡⇩d⇩f 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 ≡⇩d⇩f F↓ & G↓ & ∀y⇩1∀y⇩2([λz [F]zy⇩1y⇩2] = [λz [G]zy⇩1y⇩2] &
[λz [F]y⇩1zy⇩2] = [λz [G]y⇩1zy⇩2] &
[λz [F]y⇩1y⇩2z] = [λz [G]y⇩1y⇩2z])›
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 ≡⇩d⇩f F↓ & G↓ & ∀y⇩1∀y⇩2∀y⇩3([λz [F]zy⇩1y⇩2y⇩3] = [λz [G]zy⇩1y⇩2y⇩3] &
[λz [F]y⇩1zy⇩2y⇩3] = [λz [G]y⇩1zy⇩2y⇩3] &
[λz [F]y⇩1y⇩2zy⇩3] = [λz [G]y⇩1y⇩2zy⇩3] &
[λz [F]y⇩1y⇩2y⇩3z] = [λz [G]y⇩1y⇩2y⇩3z])›
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 ≡⇩d⇩f F↓ & G↓ & ∀x⇩1...∀x⇩n «AOT_sem_proj_id x⇩1x⇩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 ≡⇩d⇩f 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": ‹τ ≠ σ ≡⇩d⇩f ¬(τ = σ)›
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: ‹«(τ,τ')»↓ ≡⇩d⇩f τ↓ & τ'↓›
by (simp add: AOT_model_denotes_prod_def AOT_model_equiv_def
AOT_sem_conj AOT_sem_denotes)
AOT_theorem tuple_identity_1: ‹«(τ,τ')» = «(σ, σ')» ≡⇩d⇩f (τ = σ) & (τ' = σ')›
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} ≡⇩d⇩f ∀α⇩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} ≡⇩d⇩f ∃α⇩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