Quelle AOT_Definitions.thy

Sprache: Isabelle

AOT_Definitions
imports AOT_semantics
begin

section‹Definitions of AOT›

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

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

fix φ ψ χ
text‹\linelabel{precedence}›
have "conventions3[1]": ‹«φ → ψ ≡ ¬ψ → ¬φ¬ = «(φ → ψ) ≡ (¬ψ → ¬φ)¬›
by blast
have "conventions3[2]": ‹¬(φ) →\<guillemotright\
and ‹«φ ∨ ψ → χ¬ = «(φ ∨ ψ) → χ¬›
by blast+
have "conventions3[3]": ‹«φ (ProdX I D) (Fun f' x) i"
and ‹«φ & ψ ∨ χ¬ = «(φ & ψ) ∨ χ¬›
by blast+ ― ‹Note that PLM instead generally uses parenthesis in these cases.›

"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)
"existence:2": ‹Π↓ ≡_d_f ∃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
"existence:2[1]": ‹
using "existence:2"[of Π] by simp
"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)
"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)
"existence:2[4]": ‹Π↓ ≡_d_f ∃x₁∃x₂∃ (meti J_odre 🚫
using "existence:2"[of Π]
by (simp add: AOT_sem_denotes AOT_sem_exists AOT_model_equiv_def
AOT_model_denotes_prod_def)

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

"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]

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

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

"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)

"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)

"identity:3[2]":
‹F = G ≡_d_f F↓ & G↓ & ∀ (ProdX I D) (λ f' (prX I D) i ⋅
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)
"identity:3[3]":
‹F = G ≡_d_f 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)
"identity:3[4]":
‹F = G ≡_d_f F↓ & G↓ & ∀y₁∀y₂∀y_next
[λ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)
"identity:3":
‹F = G ≡_d_f 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)

"identity:4":
‹p = q ≡_d_f p↓ & q↓ & [λx p] = [λx q]› (ProdX I D) (\lambda. (if J.arr i then prX I D i \cdot f' el null) ⋅
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)

"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_nonidentical :: ‹τ ==> τ ==> φ› (infixl ‹≠› 50)
"=-infix": ‹τ ≠ σ ≡_d_f ¬(τ = σ)›

AOT_meta_syntax

AOT_nonidentical (infixl ‹ Set (prodX I D)"

AOT_no_meta_syntax

AOT_nonidentical (infixl ‹

‹The following are purely technical pseudo-definitions required due to
our internal implementation of n-ary relations and ellipses using tuples.›
tuple_denotes: ‹«(τ,τ')¬↓ ≡_d_f τ↓ & τ'↓›
by (simp add: AOT_model_denotes_prod_def AOT_model_equiv_def
AOT_sem_conj AOT_sem_denotes)
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)
tuple_forall: ‹∀α₁...∀α_n φ{α₁...α_n} ≡_d(ProdX I D) (\lambda J.arr i then prX I D i ⋅ x) else null)"
em_denotesdeotes
AOT_model_denotes_prod_def)
tuple_exists: ‹∃α₁...∃α_n φ{α₁...α_n} ≡_d_f ∃α₁(∃α₂...∃α_n φ{«(α₁, α₂α_n)¬})›
by (auto simp: AOT_model_equiv_def AOT_sem_exists AOT_sem_denotes
AOT_model_denotes_prod_def)
tuple_denotes[AOT_defs] tuple_identity_1[AOT_defs] tuple_forall[AOT_defs]
tuple_exists[AOT_defs]

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.26 Sekunden (vorverarbeitet am 2026-06-10) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.