# Theory AOT_model

```(*<*)
theory AOT_model
imports Main "HOL-Cardinals.Cardinals"
begin

(*>*)

section‹References›

text‹
A full description of this formalization including references can be found
at @{url ‹http://dx.doi.org/10.17169/refubium-35141›}.

The version of Principia Logico-Metaphysica (PLM) implemented in this formalization
can be found at @{url ‹http://mally.stanford.edu/principia-2021-10-13.pdf›}, while

›

section‹Model for the Logic of AOT›

text‹We introduce a primitive type for hyperintensional propositions.›
typedecl 𝗈

text‹To be able to model modal operators following Kripke semantics,
we introduce a primitive type for possible worlds and assert, by axiom,
that there is a surjective function mapping propositions to the
boolean-valued functions acting on possible worlds. We call the result
of applying this function to a proposition the Montague intension
of the proposition.›
typedecl w ―‹The primtive type of possible worlds.›
axiomatization AOT_model_d𝗈 :: ‹𝗈⇒(w⇒bool)› where
d𝗈_surj: ‹surj AOT_model_d𝗈›

text‹The axioms of PLM require the existence of a non-actual world.›
consts w⇩0 :: w ―‹The designated actual world.›
axiomatization where AOT_model_nonactual_world: ‹∃w . w ≠ w⇩0›

text‹Validity of a proposition in a given world can now be modelled as the result
of applying that world to the Montague intension of the proposition.›
definition AOT_model_valid_in :: ‹w⇒𝗈⇒bool› where
‹AOT_model_valid_in w φ ≡ AOT_model_d𝗈 φ w›

text‹By construction, we can choose a proposition for any given Montague intension,
s.t. the proposition is valid in a possible world iff the Montague intension
evaluates to true at that world.›
definition AOT_model_proposition_choice :: ‹(w⇒bool) ⇒ 𝗈› (binder ‹ε⇩𝗈 › 8)
where ‹ε⇩𝗈 w. φ w ≡ (inv AOT_model_d𝗈) φ›
lemma AOT_model_proposition_choice_simp: ‹AOT_model_valid_in w (ε⇩𝗈 w. φ w) = φ w›
by (simp add: surj_f_inv_f[OF d𝗈_surj] AOT_model_valid_in_def
AOT_model_proposition_choice_def)

text‹Nitpick can trivially show that there are models for the axioms above.›
lemma ‹True› nitpick[satisfy, user_axioms, expect = genuine] ..

typedecl ω ―‹The primtive type of ordinary objects/urelements.›

text‹Validating extended relation comprehension requires a large set of
special urelements. For simple models that do not validate extended
relation comprehension (and consequently the predecessor axiom in the
theory of natural numbers), it suffices to use a primitive type as @{text σ},
i.e. @{theory_text ‹typedecl σ›}.›
typedecl σ'
typedef σ = ‹UNIV::((ω ⇒ w ⇒ bool) set × (ω ⇒ w ⇒ bool) set × σ') set› ..

typedecl null ― ‹Null-urelements representing non-denoting terms.›

datatype υ = ωυ ω | συ σ | is_nullυ: nullυ null ― ‹Type of urelements›

text‹Urrelations are proposition-valued functions on urelements.
Urrelations are required to evaluate to necessarily false propositions for
null-urelements (note that there may be several distinct necessarily false
propositions).›
typedef urrel = ‹{ φ . ∀ x w . ¬AOT_model_valid_in w (φ (nullυ x)) }›
by (rule exI[where x=‹λ x . (ε⇩𝗈 w . ¬is_nullυ x)›])
(auto simp: AOT_model_proposition_choice_simp)

text‹Abstract objects will be modelled as sets of urrelations and will
have to be mapped surjectively into the set of special urelements.
We show that any mapping from abstract objects to special urelements
has to involve at least one large set of collapsed abstract objects.
We will use this fact to extend arbitrary mappings from abstract objects
to special urelements to surjective mappings.›
lemma ασ_pigeonhole:
― ‹For any arbitrary mapping @{term ασ} from sets of urrelations to special
urelements, there exists an abstract object x, s.t. the cardinal of the set
of special urelements is strictly smaller than the cardinal of the set of
abstract objects that are mapped to the same urelement as x under @{term ασ}.›
‹∃x . |UNIV::σ set| <o |{y . ασ x = ασ y}|›
for ασ :: ‹urrel set ⇒ σ›
proof(rule ccontr)
have card_σ_set_set_bound: ‹|UNIV::σ set set| ≤o |UNIV::urrel set|›
proof -
let ?pick = ‹λu s . ε⇩𝗈 w . case u of (συ s') ⇒ s' ∈ s | _ ⇒ False›
have ‹∃f :: σ set ⇒ urrel . inj f›
proof
show ‹inj (λs . Abs_urrel (λu . ?pick u s))›
proof(rule injI)
fix x y
assume ‹Abs_urrel (λu. ?pick u x) = Abs_urrel (λu. ?pick u y)›
hence ‹(λu. ?pick u x) = (λu. ?pick u y)›
by (auto intro!: Abs_urrel_inject[THEN iffD1]
simp: AOT_model_proposition_choice_simp)
hence ‹AOT_model_valid_in w⇩0 (?pick (συ s) x) =
AOT_model_valid_in w⇩0 (?pick (συ s) y)›
for s by metis
hence ‹(s ∈ x) = (s ∈ y)› for s
by (auto simp: AOT_model_proposition_choice_simp)
thus ‹x = y›
by blast
qed
qed
thus ?thesis
by (metis card_of_image inj_imp_surj_inv)
qed

text‹Assume, for a proof by contradiction, that there is no large collapsed set.›
assume ‹∄x . |UNIV::σ set| <o |{y . ασ x = ασ y}|›
hence A: ‹∀x . |{y . ασ x = ασ y}| ≤o |UNIV::σ set|›
by auto
have union_univ: ‹(⋃x ∈ range(inv ασ) . {y . ασ x = ασ y}) = UNIV›
by auto (meson f_inv_into_f range_eqI)

text‹We refute by case distinction: there is either finitely many or
infinitely many special urelements and in both cases we can derive
a contradiction from the assumption above.›
{
text‹Finite case.›
assume finite_σ_set: ‹finite (UNIV::σ set)›
hence finite_collapsed: ‹finite {y . ασ x = ασ y}› for x
using A card_of_ordLeq_infinite by blast
hence 0: ‹∀x . card {y . ασ x = ασ y} ≤ card (UNIV::σ set)›
by (metis A finite_σ_set card_of_ordLeq inj_on_iff_card_le)
have 1: ‹card (range (inv ασ)) ≤ card (UNIV::σ set)›
using finite_σ_set card_image_le by blast
hence 2: ‹finite (range (inv ασ))›
using finite_σ_set by blast

define n where ‹n = card (UNIV::urrel set set)›
define m where ‹m = card (UNIV::σ set)›

have ‹n = card (⋃x ∈ range(inv ασ) . {y . ασ x = ασ y})›
unfolding n_def using union_univ by argo
also have ‹… ≤ (∑i∈range (inv ασ). card {y. ασ i = ασ y})›
using card_UN_le 2 by blast
also have ‹… ≤ (∑i∈range (inv ασ). card (UNIV::σ set))›
by (metis (no_types, lifting) 0 sum_mono)
also have ‹… ≤ card (range (inv ασ)) * card (UNIV::σ set)›
using sum_bounded_above by auto
also have ‹… ≤ card (UNIV::σ set) * card (UNIV::σ set)›
using 1 by force
also have ‹… = m*m›
unfolding m_def by blast
finally have n_upper: ‹n ≤ m*m›.

have ‹finite (⋃x ∈ range(inv ασ) . {y . ασ x = ασ y})›
using 2 finite_collapsed by blast
hence finite_αset: ‹finite (UNIV::urrel set set)›
using union_univ by argo

have ‹2^2^m = (2::nat)^(card (UNIV::σ set set))›
by (metis Pow_UNIV card_Pow finite_σ_set m_def)
moreover have ‹card (UNIV::σ set set) ≤ (card (UNIV::urrel set))›
using card_σ_set_set_bound
by (meson Finite_Set.finite_set card_of_ordLeq finite_αset
finite_σ_set inj_on_iff_card_le)
ultimately have ‹2^2^m ≤ (2::nat)^(card (UNIV:: urrel set))›
by simp
also have ‹… = n›
unfolding n_def
by (metis Finite_Set.finite_set Pow_UNIV card_Pow finite_αset)
finally have ‹2^2^m ≤ n› by blast
hence ‹2^2^m ≤ m*m› using n_upper by linarith
moreover {
have ‹(2::nat)^(2^m) ≥ (2^(m + 1))›
by (metis Suc_eq_plus1 Suc_leI less_exp one_le_numeral power_increasing)
also have ‹(2^(m + 1)) = (2::nat) * 2^m›
by auto
have ‹m < 2^m›
hence ‹m*m < (2^m)*(2^m)›
moreover have ‹… = 2^(m+m)›
ultimately have ‹m*m < 2 ^ (m + m)› by presburger
moreover have ‹m+m ≤ 2^m›
proof (induct m)
case 0
thus ?case by auto
next
case (Suc m)
thus ?case
by (metis Suc_leI less_exp mult_2 mult_le_mono2 power_Suc)
qed
ultimately have ‹m*m < 2^2^m›
by (meson less_le_trans one_le_numeral power_increasing)
}
ultimately have False by auto
}
moreover {
text‹Infinite case.›
assume ‹infinite (UNIV::σ set)›
hence Cinfσ: ‹Cinfinite |UNIV::σ set|›
have 1: ‹|range (inv ασ)| ≤o |UNIV::σ set|›
by auto
have 2: ‹∀i∈range (inv ασ). |{y . ασ i = ασ y}| ≤o |UNIV::σ set|›
proof
fix i :: ‹urrel set›
assume ‹i ∈ range (inv ασ)›
show ‹|{y . ασ i = ασ y}| ≤o |UNIV::σ set|›
using A by blast
qed
have ‹|⋃ ((λi. {y. ασ i = ασ y}) ` (range (inv ασ)))| ≤o
|Sigma (range (inv ασ)) (λi. {y. ασ i = ασ y})|›
using card_of_UNION_Sigma by blast
hence ‹|UNIV::urrel set set| ≤o
|Sigma (range (inv ασ)) (λi. {y. ασ i = ασ y})|›
using union_univ by argo
moreover have ‹|Sigma (range (inv ασ)) (λi. {y. ασ i = ασ y})| ≤o |UNIV::σ set|›
using card_of_Sigma_ordLeq_Cinfinite[OF Cinfσ, OF 1, OF 2] by blast
ultimately have ‹|UNIV::urrel set set| ≤o |UNIV::σ set|›
using ordLeq_transitive by blast
moreover {
have ‹|UNIV::σ set| <o |UNIV::σ set set|›
by auto
moreover have ‹|UNIV::σ set set| ≤o |UNIV::urrel set|›
using card_σ_set_set_bound by blast
moreover have ‹|UNIV::urrel set| <o |UNIV::urrel set set|›
by auto
ultimately have ‹|UNIV::σ set| <o |UNIV::urrel set set|›
by (metis ordLess_imp_ordLeq ordLess_ordLeq_trans)
}
ultimately have False
using not_ordLeq_ordLess by blast
}
ultimately show False by blast
qed

text‹We introduce a mapping from abstract objects (i.e. sets of urrelations) to
special urelements @{text ‹ασ›} that is surjective and distinguishes all
abstract objects that are distinguished by a (not necessarily surjective)
mapping @{text ‹ασ'›}. @{text ‹ασ'›} will be used to model extended relation
comprehension.›
consts ασ' :: ‹urrel set ⇒ σ›
consts ασ :: ‹urrel set ⇒ σ›

specification(ασ)
ασ_surj: ‹surj ασ›
ασ_ασ': ‹ασ x = ασ y ⟹ ασ' x = ασ' y›
proof -
obtain x where x_prop: ‹|UNIV::σ set| <o |{y. ασ' x = ασ' y}|›
using ασ_pigeonhole by blast
have ‹∃f :: urrel set ⇒ σ . f ` {y. ασ' x = ασ' y} = UNIV ∧ f x = ασ' x›
proof -
have ‹∃f :: urrel set ⇒ σ . f ` {y. ασ' x = ασ' y} = UNIV›
by (simp add: x_prop card_of_ordLeq2 ordLess_imp_ordLeq)
then obtain f :: ‹urrel set ⇒ σ› where ‹f ` {y. ασ' x = ασ' y} = UNIV›
by presburger
moreover obtain a where ‹f a = ασ' x› and ‹ασ' a = ασ' x›
by (smt (verit, best) calculation UNIV_I image_iff mem_Collect_eq)
ultimately have ‹(f (a := f x, x := f a)) ` {y. ασ' x = ασ' y} = UNIV ∧
(f (a := f x, x := f a)) x = ασ' x›
by (auto simp: image_def)
thus ?thesis by blast
qed
then obtain f where fimage: ‹f ` {y. ασ' x = ασ' y} = UNIV›
and fx: ‹f x = ασ' x›
by blast

define ασ :: ‹urrel set ⇒ σ› where
‹ασ ≡ λ urrels . if ασ' urrels = ασ' x ∧ f urrels ∉ range ασ'
then f urrels
else ασ' urrels›
have ‹surj ασ›
proof -
{
fix s :: σ
{
assume ‹s ∈ range ασ'›
hence 0: ‹ασ' (inv ασ' s) = s›
by (meson f_inv_into_f)
{
assume ‹s = ασ' x›
hence ‹ασ x = s›
using ασ_def fx by presburger
hence ‹∃f . ασ (f s) = s›
by auto
}
moreover {
assume ‹s ≠ ασ' x›
hence ‹ασ (inv ασ' s) = s›
unfolding ασ_def 0 by presburger
hence ‹∃f . ασ (f s) = s›
by blast
}
ultimately have ‹∃f . ασ (f s) = s›
by blast
}
moreover {
assume ‹s ∉ range ασ'›
moreover obtain urrels where ‹f urrels = s› and ‹ασ' x = ασ' urrels›
by (smt (verit, best) UNIV_I fimage image_iff mem_Collect_eq)
ultimately have ‹ασ urrels = s›
using ασ_def by presburger
hence ‹∃f . ασ (f s) = s›
by (meson f_inv_into_f range_eqI)
}
ultimately have ‹∃f . ασ (f s) = s›
by blast
}
thus ?thesis
by (metis surj_def)
qed
moreover have ‹∀x y. ασ x = ασ y ⟶ ασ' x = ασ' y›
by (metis ασ_def rangeI)
ultimately show ?thesis
by blast
qed

text‹For extended models that validate extended relation comprehension
(and consequently the predecessor axiom), we specify which
abstract objects are distinguished by @{const ασ'}.›

definition urrel_to_ωrel :: ‹urrel ⇒ (ω ⇒ w ⇒ bool)› where
‹urrel_to_ωrel ≡ λ r u w . AOT_model_valid_in w (Rep_urrel r (ωυ u))›
definition ωrel_to_urrel :: ‹(ω ⇒ w ⇒ bool) ⇒ urrel› where
‹ωrel_to_urrel ≡ λ φ . Abs_urrel
(λ u . ε⇩𝗈 w . case u of ωυ x ⇒ φ x w | _ ⇒ False)›

definition AOT_urrel_ωequiv :: ‹urrel ⇒ urrel ⇒ bool› where
‹AOT_urrel_ωequiv ≡ λ r s . ∀ u v . AOT_model_valid_in v (Rep_urrel r (ωυ u)) =
AOT_model_valid_in v (Rep_urrel s (ωυ u))›

lemma urrel_ωrel_quot: ‹Quotient3 AOT_urrel_ωequiv urrel_to_ωrel ωrel_to_urrel›
proof(rule Quotient3I)
show ‹urrel_to_ωrel (ωrel_to_urrel a) = a› for a
unfolding ωrel_to_urrel_def urrel_to_ωrel_def
apply (rule ext)
apply (subst Abs_urrel_inverse)
by (auto simp: AOT_model_proposition_choice_simp)
next
show ‹AOT_urrel_ωequiv (ωrel_to_urrel a) (ωrel_to_urrel a)› for a
unfolding ωrel_to_urrel_def AOT_urrel_ωequiv_def
apply (subst (1 2) Abs_urrel_inverse)
by (auto simp: AOT_model_proposition_choice_simp)
next
show ‹AOT_urrel_ωequiv r s = (AOT_urrel_ωequiv r r ∧ AOT_urrel_ωequiv s s ∧
urrel_to_ωrel r = urrel_to_ωrel s)› for r s
proof
assume ‹AOT_urrel_ωequiv r s›
hence ‹AOT_model_valid_in v (Rep_urrel r (ωυ u)) =
AOT_model_valid_in v (Rep_urrel s (ωυ u))› for u v
using AOT_urrel_ωequiv_def by metis
hence ‹urrel_to_ωrel r = urrel_to_ωrel s›
unfolding urrel_to_ωrel_def
by simp
thus ‹AOT_urrel_ωequiv r r ∧ AOT_urrel_ωequiv s s ∧
urrel_to_ωrel r = urrel_to_ωrel s›
unfolding AOT_urrel_ωequiv_def
by auto
next
assume ‹AOT_urrel_ωequiv r r ∧ AOT_urrel_ωequiv s s ∧
urrel_to_ωrel r = urrel_to_ωrel s›
hence ‹AOT_model_valid_in v (Rep_urrel r (ωυ u)) =
AOT_model_valid_in v (Rep_urrel s (ωυ u))› for u v
by (metis urrel_to_ωrel_def)
thus ‹AOT_urrel_ωequiv r s›
using AOT_urrel_ωequiv_def by presburger
qed
qed

specification (ασ')
ασ_eq_ord_exts_all:
‹ασ' a = ασ' b ⟹ (⋀s . urrel_to_ωrel s = urrel_to_ωrel r ⟹ s ∈ a)
⟹ (⋀ s . urrel_to_ωrel s = urrel_to_ωrel r ⟹ s ∈ b)›
ασ_eq_ord_exts_ex:
‹ασ' a = ασ' b ⟹ (∃ s . s ∈ a ∧ urrel_to_ωrel s = urrel_to_ωrel r)
⟹ (∃s . s ∈ b ∧ urrel_to_ωrel s = urrel_to_ωrel r)›
proof -
define ασ_wit_intersection where
‹ασ_wit_intersection ≡ λ urrels .
{ordext . ∀urrel . urrel_to_ωrel urrel = ordext ⟶ urrel ∈ urrels}›
define ασ_wit_union where
‹ασ_wit_union ≡ λ urrels .
{ordext . ∃urrel∈urrels . urrel_to_ωrel urrel = ordext}›

let ?ασ_wit = ‹λ urrels .
let ordexts = ασ_wit_intersection urrels in
let ordexts' = ασ_wit_union urrels in
(ordexts, ordexts', undefined)›
define ασ_wit :: ‹urrel set ⇒ σ› where
‹ασ_wit ≡ λ urrels . Abs_σ (?ασ_wit urrels)›
{
fix a b :: ‹urrel set› and r s
assume ‹ασ_wit a = ασ_wit b›
hence 0: ‹{ordext. ∀urrel. urrel_to_ωrel urrel = ordext ⟶ urrel ∈ a} =
{ordext. ∀urrel. urrel_to_ωrel urrel = ordext ⟶ urrel ∈ b}›
unfolding ασ_wit_def Let_def
apply (subst (asm) Abs_σ_inject)
by (auto simp: ασ_wit_intersection_def ασ_wit_union_def)
assume ‹urrel_to_ωrel s = urrel_to_ωrel r ⟹ s ∈ a› for s
hence ‹urrel_to_ωrel r ∈
{ordext. ∀urrel. urrel_to_ωrel urrel = ordext ⟶ urrel ∈ a}›
by auto
hence ‹urrel_to_ωrel r ∈
{ordext. ∀urrel. urrel_to_ωrel urrel = ordext ⟶ urrel ∈ b}›
using 0 by blast
moreover assume ‹urrel_to_ωrel s = urrel_to_ωrel r›
ultimately have ‹s ∈ b›
by blast
}
moreover {
fix a b :: ‹urrel set› and s r
assume ‹ασ_wit a = ασ_wit b›
hence 0: ‹{ordext. ∃urrel ∈ a. urrel_to_ωrel urrel = ordext} =
{ordext. ∃urrel ∈ b. urrel_to_ωrel urrel = ordext}›
unfolding ασ_wit_def
using Abs_σ_inject ασ_wit_union_def by auto
assume ‹s ∈ a›
hence ‹urrel_to_ωrel s ∈ {ordext. ∃urrel ∈ a. urrel_to_ωrel urrel = ordext}›
by blast
moreover assume ‹urrel_to_ωrel s = urrel_to_ωrel r›
ultimately have ‹urrel_to_ωrel r ∈
{ordext. ∃urrel ∈ b. urrel_to_ωrel urrel = ordext}›
using "0" by argo
hence ‹∃s. s ∈ b ∧ urrel_to_ωrel s = urrel_to_ωrel r›
by blast
}
ultimately show ?thesis
by (safe intro!: exI[where x=ασ_wit]; metis)
qed

text‹We enable the extended model version.›
abbreviation (input) AOT_ExtendedModel where ‹AOT_ExtendedModel ≡ True›

text‹Individual terms are either ordinary objects, represented by ordinary urelements,
abstract objects, modelled as sets of urrelations, or null objects, used to
represent non-denoting definite descriptions.›
datatype κ = ωκ ω | ακ ‹urrel set› | is_nullκ: nullκ null

text‹The mapping from abstract objects to urelements can be naturally
lifted to a surjective mapping from individual terms to urelements.›
primrec κυ :: ‹κ⇒υ› where
‹κυ (ωκ x) = ωυ x›
| ‹κυ (ακ x) = συ (ασ x)›
| ‹κυ (nullκ x) = nullυ x›

lemma κυ_surj: ‹surj κυ›
using ασ_surj by (metis κυ.simps(1) κυ.simps(2) κυ.simps(3) υ.exhaust surj_def)

text‹By construction if the urelement of an individual term is exemplified by
an urrelation, it cannot be a null-object.›
lemma urrel_null_false:
assumes ‹AOT_model_valid_in w (Rep_urrel f (κυ x))›
shows ‹¬is_nullκ x›
by (metis (mono_tags, lifting) assms Rep_urrel κ.collapse(3) κυ.simps(3)
mem_Collect_eq)

text‹AOT requires any ordinary object to be @{emph ‹possibly concrete›} and that
there is an object that is not actually, but possibly concrete.›
consts AOT_model_concreteω :: ‹ω ⇒ w ⇒  bool›
specification (AOT_model_concreteω)
AOT_model_ω_concrete_in_some_world:
‹∃ w . AOT_model_concreteω x w›
AOT_model_contingent_object:
‹∃ x w . AOT_model_concreteω x w ∧ ¬AOT_model_concreteω x w⇩0›
by (rule exI[where x=‹λ_ w. w ≠ w⇩0›]) (auto simp: AOT_model_nonactual_world)

text‹We define a type class for AOT's terms specifying the conditions under which
objects of that type denote and require the set of denoting terms to be
non-empty.›
class AOT_Term =
fixes AOT_model_denotes :: ‹'a ⇒ bool›
assumes AOT_model_denoting_ex: ‹∃ x . AOT_model_denotes x›

text‹All types except the type of propositions involve non-denoting terms. We
define a refined type class for those.›
class AOT_IncompleteTerm = AOT_Term +
assumes AOT_model_nondenoting_ex: ‹∃ x . ¬AOT_model_denotes x›

text‹Generic non-denoting term.›
definition AOT_model_nondenoting :: ‹'a::AOT_IncompleteTerm› where
‹AOT_model_nondenoting ≡ SOME τ . ¬AOT_model_denotes τ›
lemma AOT_model_nondenoing: ‹¬AOT_model_denotes (AOT_model_nondenoting)›
using someI_ex[OF AOT_model_nondenoting_ex]
unfolding AOT_model_nondenoting_def by blast

text‹@{const AOT_model_denotes} can trivially be extended to products of types.›
instantiation prod :: (AOT_Term, AOT_Term) AOT_Term
begin
definition AOT_model_denotes_prod :: ‹'a×'b ⇒ bool› where
‹AOT_model_denotes_prod ≡ λ(x,y) . AOT_model_denotes x ∧ AOT_model_denotes y›
instance proof
show ‹∃x::'a×'b. AOT_model_denotes x›
qed
end

text‹We specify a transformation of proposition-valued functions on terms, s.t.
the result is fully determined by @{emph ‹regular›} terms. This will be required
for modelling n-ary relations as functions on tuples while preserving AOT's
definition of n-ary relation identity.›
locale AOT_model_irregular_spec =
fixes AOT_model_irregular :: ‹('a ⇒ 𝗈) ⇒ 'a ⇒ 𝗈›
and AOT_model_regular :: ‹'a ⇒ bool›
and AOT_model_term_equiv :: ‹'a ⇒ 'a ⇒ bool›
assumes AOT_model_irregular_false:
‹¬AOT_model_valid_in w (AOT_model_irregular φ x)›
assumes AOT_model_irregular_equiv:
‹AOT_model_term_equiv x y ⟹
AOT_model_irregular φ x = AOT_model_irregular φ y›
assumes AOT_model_irregular_eqI:
‹(⋀ x . AOT_model_regular x ⟹ φ x = ψ x) ⟹
AOT_model_irregular φ x = AOT_model_irregular ψ x›

text‹We introduce a type class for individual terms that specifies being regular,
being equivalent (i.e. conceptually @{emph ‹sharing urelements›}) and the
transformation on proposition-valued functions as specified above.›
class AOT_IndividualTerm = AOT_IncompleteTerm +
fixes AOT_model_regular :: ‹'a ⇒ bool›
fixes AOT_model_term_equiv :: ‹'a ⇒ 'a ⇒ bool›
fixes AOT_model_irregular :: ‹('a ⇒ 𝗈) ⇒ 'a ⇒ 𝗈›
assumes AOT_model_irregular_nondenoting:
‹¬AOT_model_regular x ⟹ ¬AOT_model_denotes x›
assumes AOT_model_term_equiv_part_equivp:
‹equivp AOT_model_term_equiv›
assumes AOT_model_term_equiv_denotes:
‹AOT_model_term_equiv x y ⟹ (AOT_model_denotes x = AOT_model_denotes y)›
assumes AOT_model_term_equiv_regular:
‹AOT_model_term_equiv x y ⟹ (AOT_model_regular x = AOT_model_regular y)›
assumes AOT_model_irregular:
‹AOT_model_irregular_spec AOT_model_irregular AOT_model_regular
AOT_model_term_equiv›

interpretation AOT_model_irregular_spec AOT_model_irregular AOT_model_regular
AOT_model_term_equiv
using AOT_model_irregular .

text‹Our concrete type for individual terms satisfies the type class of
individual terms.
Note that all unary individuals are regular. In general, an individual term
may be a tuple and is regular, if at most one tuple element does not denote.›
instantiation κ :: AOT_IndividualTerm
begin
definition AOT_model_term_equiv_κ :: ‹κ ⇒ κ ⇒ bool› where
‹AOT_model_term_equiv_κ ≡ λ x y . κυ x = κυ y›
definition AOT_model_denotes_κ :: ‹κ ⇒ bool› where
‹AOT_model_denotes_κ ≡ λ x . ¬is_nullκ x›
definition AOT_model_regular_κ :: ‹κ ⇒ bool› where
‹AOT_model_regular_κ ≡ λ x . True›
definition AOT_model_irregular_κ :: ‹(κ ⇒ 𝗈) ⇒ κ ⇒ 𝗈› where
‹AOT_model_irregular_κ ≡ SOME φ . AOT_model_irregular_spec φ
AOT_model_regular AOT_model_term_equiv›
instance proof
show ‹∃x :: κ. AOT_model_denotes x›
by (rule exI[where x=‹ωκ undefined›])
next
show ‹∃x :: κ. ¬AOT_model_denotes x›
by (rule exI[where x=‹nullκ undefined›])
next
show "¬AOT_model_regular x ⟹ ¬ AOT_model_denotes x" for x :: κ
next
show ‹equivp (AOT_model_term_equiv :: κ ⇒ κ ⇒ bool)›
by (rule equivpI; rule reflpI exI sympI transpI)
next
fix x y :: κ
show ‹AOT_model_term_equiv x y ⟹ AOT_model_denotes x = AOT_model_denotes y›
by (metis AOT_model_denotes_κ_def AOT_model_term_equiv_κ_def κ.exhaust_disc
κυ.simps υ.disc(1,3,5,6) is_ακ_def is_ωκ_def is_nullκ_def)
next
fix x y :: κ
show ‹AOT_model_term_equiv x y ⟹ AOT_model_regular x = AOT_model_regular y›
next
have "AOT_model_irregular_spec (λ φ (x::κ) .  ε⇩𝗈 w . False)
AOT_model_regular AOT_model_term_equiv"
by standard (auto simp: AOT_model_proposition_choice_simp)
thus ‹AOT_model_irregular_spec (AOT_model_irregular::(κ⇒𝗈) ⇒ κ ⇒ 𝗈)
AOT_model_regular AOT_model_term_equiv›
unfolding AOT_model_irregular_κ_def by (metis (no_types, lifting) someI_ex)
qed
end

text‹We define relations among individuals as proposition valued functions.
@{emph ‹Denoting›} unary relations (among @{typ κ}) will match the
urrelations introduced above.›
typedef 'a rel (‹<_>›) = ‹UNIV::('a::AOT_IndividualTerm ⇒ 𝗈) set› ..
setup_lifting type_definition_rel

text‹We will use the transformation specified above to "fix" the behaviour of
functions on irregular terms when defining @{text ‹λ›}-expressions.›
definition fix_irregular :: ‹('a::AOT_IndividualTerm ⇒ 𝗈) ⇒ ('a ⇒ 𝗈)› where
‹fix_irregular ≡ λ φ x . if AOT_model_regular x
then φ x else AOT_model_irregular φ x›
lemma fix_irregular_denoting:
‹AOT_model_denotes x ⟹ fix_irregular φ x = φ x›
by (meson AOT_model_irregular_nondenoting fix_irregular_def)
lemma fix_irregular_regular:
‹AOT_model_regular x ⟹ fix_irregular φ x = φ x›
by (meson AOT_model_irregular_nondenoting fix_irregular_def)
lemma fix_irregular_irregular:
‹¬AOT_model_regular x ⟹ fix_irregular φ x = AOT_model_irregular φ x›

text‹Relations among individual terms are (potentially non-denoting) terms.
A relation denotes, if it agrees on all equivalent terms (i.e. terms sharing
urelements), is necessarily false on all non-denoting terms and is
well-behaved on irregular terms.›
instantiation rel :: (AOT_IndividualTerm) AOT_IncompleteTerm
begin
text‹\linelabel{AOT_model_denotes_rel}›
lift_definition AOT_model_denotes_rel :: ‹<'a> ⇒ bool› is
‹λ φ . (∀ x y . AOT_model_term_equiv x y ⟶ φ x = φ y) ∧
(∀ w x . AOT_model_valid_in w (φ x) ⟶ AOT_model_denotes x) ∧
(∀ x . ¬AOT_model_regular x ⟶ φ x = AOT_model_irregular φ x)› .
instance proof
have ‹AOT_model_irregular (fix_irregular φ) x = AOT_model_irregular φ x›
for φ and x :: 'a
by (rule AOT_model_irregular_eqI) (simp add: fix_irregular_def)
thus ‹∃ x :: <'a> . AOT_model_denotes x›
by (safe intro!: exI[where x=‹Abs_rel (fix_irregular (λx. ε⇩𝗈 w . False))›])
(transfer; auto simp: AOT_model_proposition_choice_simp fix_irregular_def
AOT_model_irregular_equiv AOT_model_term_equiv_regular
AOT_model_irregular_false)
next
show ‹∃f :: <'a> . ¬AOT_model_denotes f›
by (rule exI[where x=‹Abs_rel (λx. ε⇩𝗈 w . True)›];
auto simp: AOT_model_denotes_rel.abs_eq AOT_model_nondenoting_ex
AOT_model_proposition_choice_simp)
qed
end

text‹Auxiliary lemmata.›

lemma AOT_model_term_equiv_eps:
shows ‹AOT_model_term_equiv (Eps (AOT_model_term_equiv κ)) κ›
and ‹AOT_model_term_equiv κ (Eps (AOT_model_term_equiv κ))›
and ‹AOT_model_term_equiv κ κ' ⟹
(Eps (AOT_model_term_equiv κ)) = (Eps (AOT_model_term_equiv κ'))›
apply (metis AOT_model_term_equiv_part_equivp equivp_def someI_ex)
apply (metis AOT_model_term_equiv_part_equivp equivp_def someI_ex)
by (metis AOT_model_term_equiv_part_equivp equivp_def)

lemma AOT_model_denotes_Abs_rel_fix_irregularI:
assumes ‹⋀ x y . AOT_model_term_equiv x y ⟹ φ x = φ y›
and ‹⋀ w x . AOT_model_valid_in w (φ x) ⟹ AOT_model_denotes x›
shows ‹AOT_model_denotes (Abs_rel (fix_irregular φ))›
proof -
have ‹AOT_model_irregular φ x = AOT_model_irregular
(λx. if AOT_model_regular x then φ x else AOT_model_irregular φ x) x›
if ‹¬ AOT_model_regular x›
for x
by (rule AOT_model_irregular_eqI) auto
thus ?thesis
unfolding AOT_model_denotes_rel.rep_eq
using assms by (auto simp: AOT_model_irregular_false Abs_rel_inverse
AOT_model_irregular_equiv fix_irregular_def
AOT_model_term_equiv_regular)
qed

lemma AOT_model_term_equiv_rel_equiv:
assumes ‹AOT_model_denotes x›
and ‹AOT_model_denotes y›
shows ‹AOT_model_term_equiv x y = (∀ Π w . AOT_model_denotes Π ⟶
AOT_model_valid_in w (Rep_rel Π x) = AOT_model_valid_in w (Rep_rel Π y))›
proof
assume ‹AOT_model_term_equiv x y›
thus ‹∀ Π w . AOT_model_denotes Π ⟶ AOT_model_valid_in w (Rep_rel Π x) =
AOT_model_valid_in w (Rep_rel Π y)›
next
have 0: ‹(AOT_model_denotes x' ∧ AOT_model_term_equiv x' y) =
(AOT_model_denotes y' ∧ AOT_model_term_equiv y' y)›
if ‹AOT_model_term_equiv x' y'› for x' y'
by (metis that AOT_model_term_equiv_denotes AOT_model_term_equiv_part_equivp
equivp_def)
assume ‹∀ Π w . AOT_model_denotes Π ⟶ AOT_model_valid_in w (Rep_rel Π x) =
AOT_model_valid_in w (Rep_rel Π y)›
moreover have ‹AOT_model_denotes (Abs_rel (fix_irregular
(λ x . ε⇩𝗈 w . AOT_model_denotes x ∧ AOT_model_term_equiv x y)))›
(is "AOT_model_denotes ?r")
by (rule AOT_model_denotes_Abs_rel_fix_irregularI)
(auto simp: 0 AOT_model_denotes_rel.rep_eq Abs_rel_inverse fix_irregular_def
AOT_model_proposition_choice_simp AOT_model_irregular_false)
ultimately have ‹AOT_model_valid_in w (Rep_rel ?r x) =
AOT_model_valid_in w (Rep_rel ?r y)› for w
by blast
thus ‹AOT_model_term_equiv x y›
fix_irregular_denoting[OF assms(1)] AOT_model_term_equiv_part_equivp
fix_irregular_denoting[OF assms(2)] assms equivp_reflp)
qed

text‹Denoting relations among terms of type @{typ κ} correspond to urrelations.›

definition rel_to_urrel :: ‹<κ> ⇒ urrel› where
‹rel_to_urrel ≡ λ Π . Abs_urrel (λ u . Rep_rel Π (SOME x . κυ x = u))›
definition urrel_to_rel :: ‹urrel ⇒ <κ>› where
‹urrel_to_rel ≡ λ φ . Abs_rel (λ x . Rep_urrel φ (κυ x))›
definition AOT_rel_equiv :: ‹<'a::AOT_IndividualTerm> ⇒ <'a> ⇒ bool› where
‹AOT_rel_equiv ≡ λ f g . AOT_model_denotes f ∧ AOT_model_denotes g ∧ f = g›

lemma urrel_quotient3: ‹Quotient3 AOT_rel_equiv rel_to_urrel urrel_to_rel›
proof (rule Quotient3I)
have ‹(λu. Rep_urrel a (κυ (SOME x. κυ x = u))) = (λu. Rep_urrel a u)› for a
by (rule ext) (metis (mono_tags, lifting) κυ_surj surj_f_inv_f verit_sko_ex')
thus ‹rel_to_urrel (urrel_to_rel a) = a› for a
by (simp add: Abs_rel_inverse rel_to_urrel_def urrel_to_rel_def
Rep_urrel_inverse)
next
show ‹AOT_rel_equiv (urrel_to_rel a) (urrel_to_rel a)› for a
unfolding AOT_rel_equiv_def urrel_to_rel_def
by transfer (simp add: AOT_model_regular_κ_def AOT_model_denotes_κ_def
AOT_model_term_equiv_κ_def urrel_null_false)
next
{
fix a
assume ‹∀w x. AOT_model_valid_in w (a x) ⟶ ¬ is_nullκ x›
hence ‹(λu. a (SOME x. κυ x = u)) ∈
{φ. ∀x w. ¬ AOT_model_valid_in w (φ (nullυ x))}›
by (simp; metis (mono_tags, lifting) κ.exhaust_disc κυ.simps υ.disc(1,3,5)
υ.disc(6) is_ακ_def is_ωκ_def someI_ex)
} note 1 = this
{
fix r s :: ‹κ ⇒ 𝗈›
assume A: ‹∀x y. AOT_model_term_equiv x y ⟶ r x = r y›
assume ‹∀w x. AOT_model_valid_in w (r x) ⟶ AOT_model_denotes x›
hence 2: ‹(λu. r (SOME x. κυ x = u)) ∈
{φ. ∀x w. ¬ AOT_model_valid_in w (φ (nullυ x))}›
using 1 AOT_model_denotes_κ_def by meson
assume B: ‹∀x y. AOT_model_term_equiv x y ⟶ s x = s y›
assume ‹∀w x. AOT_model_valid_in w (s x) ⟶ AOT_model_denotes x›
hence 3: ‹(λu. s (SOME x. κυ x = u)) ∈
{φ. ∀x w. ¬ AOT_model_valid_in w (φ (nullυ x))}›
using 1 AOT_model_denotes_κ_def by meson
assume ‹Abs_urrel (λu. r (SOME x. κυ x = u)) =
Abs_urrel (λu. s (SOME x. κυ x = u))›
hence 4: ‹r (SOME x. κυ x = u) = s (SOME x::κ. κυ x = u)› for u
unfolding Abs_urrel_inject[OF 2 3] by metis
have ‹r x = s x› for x
using 4[of ‹κυ x›]
by (metis (mono_tags, lifting) A B AOT_model_term_equiv_κ_def someI_ex)
hence ‹r = s› by auto
}
thus ‹AOT_rel_equiv r s = (AOT_rel_equiv r r ∧ AOT_rel_equiv s s ∧
rel_to_urrel r = rel_to_urrel s)› for r s
unfolding AOT_rel_equiv_def rel_to_urrel_def
by transfer auto
qed

lemma urrel_quotient:
‹Quotient AOT_rel_equiv rel_to_urrel urrel_to_rel
(λx y. AOT_rel_equiv x x ∧ rel_to_urrel x = y)›
using Quotient3_to_Quotient[OF urrel_quotient3] by auto

text‹Unary individual terms are always regular and equipped with encoding and
concreteness. The specification of the type class anticipates the required
properties for deriving the axiom system.›
class AOT_UnaryIndividualTerm =
fixes AOT_model_enc :: ‹'a ⇒ <'a::AOT_IndividualTerm> ⇒ bool›
and AOT_model_concrete :: ‹w ⇒ 'a ⇒ bool›
assumes AOT_model_unary_regular:
‹AOT_model_regular x› ― ‹All unary individual terms are regular.›
and AOT_model_enc_relid:
‹AOT_model_denotes F ⟹
AOT_model_denotes G ⟹
(⋀ x . AOT_model_enc x F ⟷ AOT_model_enc x G)
⟹ F = G›
and AOT_model_A_objects:
‹∃x . AOT_model_denotes x ∧
(∀w. ¬ AOT_model_concrete w x) ∧
(∀F. AOT_model_denotes F ⟶ AOT_model_enc x F = φ F)›
and AOT_model_contingent:
‹∃ x w. AOT_model_concrete w x ∧ ¬ AOT_model_concrete w⇩0 x›
and AOT_model_nocoder:
‹AOT_model_concrete w x ⟹ ¬AOT_model_enc x F›
and AOT_model_concrete_equiv:
‹AOT_model_term_equiv x y ⟹
AOT_model_concrete w x = AOT_model_concrete w y›
and AOT_model_concrete_denotes:
‹AOT_model_concrete w x ⟹ AOT_model_denotes x›
― ‹The following are properties that will only hold in the extended models.›
and AOT_model_enc_indistinguishable_all:
‹AOT_ExtendedModel ⟹
AOT_model_denotes a ⟹ ¬(∃ w . AOT_model_concrete w a) ⟹
AOT_model_denotes b ⟹ ¬(∃ w . AOT_model_concrete w b) ⟹
AOT_model_denotes Π ⟹
(⋀ Π' . AOT_model_denotes Π' ⟹
(⋀ v . AOT_model_valid_in v (Rep_rel Π' a) =
AOT_model_valid_in v (Rep_rel Π' b))) ⟹
(⋀ Π' . AOT_model_denotes Π' ⟹
(⋀ v x . ∃ w . AOT_model_concrete w x ⟹
AOT_model_valid_in v (Rep_rel Π' x) =
AOT_model_valid_in v (Rep_rel Π x)) ⟹
AOT_model_enc a Π') ⟹
(⋀ Π' . AOT_model_denotes Π' ⟹
(⋀ v x . ∃ w . AOT_model_concrete w x ⟹
AOT_model_valid_in v (Rep_rel Π' x) =
AOT_model_valid_in v (Rep_rel Π x)) ⟹
AOT_model_enc b Π')›
and AOT_model_enc_indistinguishable_ex:
‹AOT_ExtendedModel ⟹
AOT_model_denotes a ⟹ ¬(∃ w . AOT_model_concrete w a) ⟹
AOT_model_denotes b ⟹ ¬(∃ w . AOT_model_concrete w b) ⟹
AOT_model_denotes Π ⟹
(⋀ Π' . AOT_model_denotes Π' ⟹
(⋀ v . AOT_model_valid_in v (Rep_rel Π' a) =
AOT_model_valid_in v (Rep_rel Π' b))) ⟹
(∃ Π' . AOT_model_denotes Π' ∧ AOT_model_enc a Π' ∧
(∀ v x . (∃ w . AOT_model_concrete w x) ⟶
AOT_model_valid_in v (Rep_rel Π' x) =
AOT_model_valid_in v (Rep_rel Π x))) ⟹
(∃ Π' . AOT_model_denotes Π' ∧ AOT_model_enc b Π' ∧
(∀ v x . (∃ w . AOT_model_concrete w x) ⟶
AOT_model_valid_in v (Rep_rel Π' x) =
AOT_model_valid_in v (Rep_rel Π x)))›

text‹Instantiate the class of unary individual terms for our concrete type of
individual terms @{typ κ}.›
instantiation κ :: AOT_UnaryIndividualTerm
begin

definition AOT_model_enc_κ :: ‹κ ⇒ <κ> ⇒ bool› where
‹AOT_model_enc_κ ≡ λ x F .
case x of ακ a ⇒ AOT_model_denotes F ∧ rel_to_urrel F ∈ a
| _ ⇒ False›
primrec AOT_model_concrete_κ :: ‹w ⇒ κ ⇒ bool› where
‹AOT_model_concrete_κ w (ωκ x) = AOT_model_concreteω x w›
| ‹AOT_model_concrete_κ w (ακ x) = False›
| ‹AOT_model_concrete_κ w (nullκ x) = False›

lemma AOT_meta_A_objects_κ:
‹∃x :: κ. AOT_model_denotes x ∧
(∀w. ¬ AOT_model_concrete w x) ∧
(∀F. AOT_model_denotes F ⟶ AOT_model_enc x F = φ F)› for φ
apply (rule exI[where x=‹ακ {f . φ (urrel_to_rel f)}›])
by (metis (no_types, lifting) AOT_rel_equiv_def urrel_quotient
Quotient_rep_abs_fold_unmap)

instance proof
show ‹AOT_model_regular x› for x :: κ
next
fix F G :: ‹<κ>›
assume ‹AOT_model_denotes F›
moreover assume ‹AOT_model_denotes G›
moreover assume ‹⋀x. AOT_model_enc x F = AOT_model_enc x G›
moreover obtain x where ‹∀G. AOT_model_denotes G ⟶ AOT_model_enc x G = (F = G)›
using AOT_meta_A_objects_κ by blast
ultimately show ‹F = G› by blast
next
show ‹∃x :: κ. AOT_model_denotes x ∧
(∀w. ¬ AOT_model_concrete w x) ∧
(∀F. AOT_model_denotes F ⟶ AOT_model_enc x F = φ F)› for φ
using AOT_meta_A_objects_κ .
next
show ‹∃ (x::κ) w. AOT_model_concrete w x ∧ ¬ AOT_model_concrete w⇩0 x›
using AOT_model_concrete_κ.simps(1) AOT_model_contingent_object by blast
next
show ‹AOT_model_concrete w x ⟹ ¬ AOT_model_enc x F› for w and x :: κ and F
by (metis AOT_model_concrete_κ.simps(2) AOT_model_enc_κ_def κ.case_eq_if
κ.collapse(2))
next
show ‹AOT_model_concrete w x = AOT_model_concrete w y›
if ‹AOT_model_term_equiv x y›
for x y :: κ and w
using that by (induct x; induct y; auto simp: AOT_model_term_equiv_κ_def)
next
show ‹AOT_model_concrete w x ⟹ AOT_model_denotes x› for w and x :: κ
by (metis AOT_model_concrete_κ.simps(3) AOT_model_denotes_κ_def κ.collapse(3))
(* Extended models only *)
next
fix κ κ' :: κ and Π Π' :: ‹<κ>› and w :: w
assume ext: ‹AOT_ExtendedModel›
assume ‹AOT_model_denotes κ›
moreover assume ‹∄w. AOT_model_concrete w κ›
ultimately obtain a where a_def: ‹ακ a = κ›
by (metis AOT_model_ω_concrete_in_some_world AOT_model_concrete_κ.simps(1)
AOT_model_denotes_κ_def κ.discI(3) κ.exhaust_sel)
assume ‹AOT_model_denotes κ'›
moreover assume ‹∄w. AOT_model_concrete w κ'›
ultimately obtain b where b_def: ‹ακ b = κ'›
by (metis AOT_model_ω_concrete_in_some_world AOT_model_concrete_κ.simps(1)
AOT_model_denotes_κ_def κ.discI(3) κ.exhaust_sel)
assume ‹AOT_model_denotes Π' ⟹ AOT_model_valid_in w (Rep_rel Π' κ) =
AOT_model_valid_in w (Rep_rel Π' κ')› for Π' w
hence ‹AOT_model_valid_in w (Rep_urrel r (κυ κ)) =
AOT_model_valid_in w (Rep_urrel r (κυ κ'))› for r
by (metis AOT_rel_equiv_def Abs_rel_inverse Quotient3_rel_rep
iso_tuple_UNIV_I urrel_quotient3 urrel_to_rel_def)
hence ‹let r = (Abs_urrel (λ u . ε⇩𝗈 w . u = κυ κ)) in
AOT_model_valid_in w (Rep_urrel r (κυ κ)) =
AOT_model_valid_in w (Rep_urrel r (κυ κ'))›
by presburger
hence ασ_eq: ‹ασ a = ασ b›
unfolding Let_def
apply (subst (asm) (1 2) Abs_urrel_inverse)
using AOT_model_proposition_choice_simp a_def b_def by force+
assume Π_den: ‹AOT_model_denotes Π›
have ‹¬AOT_model_valid_in w (Rep_rel Π (SOME xa. κυ xa = nullυ x))› for x w
by (metis (mono_tags, lifting) AOT_model_denotes_κ_def
AOT_model_denotes_rel.rep_eq κ.exhaust_disc κυ.simps(1,2,3)
‹AOT_model_denotes Π› υ.disc(8,9) υ.distinct(3)
is_ακ_def is_ωκ_def verit_sko_ex')
moreover have ‹Rep_rel Π (ωκ x) = Rep_rel Π (SOME y. κυ y = ωυ x)› for x
by (metis (mono_tags, lifting) AOT_model_denotes_rel.rep_eq
AOT_model_term_equiv_κ_def κυ.simps(1) Π_den verit_sko_ex')
ultimately have ‹Rep_rel Π (ωκ x) = Rep_urrel (rel_to_urrel Π) (ωυ x)› for x
unfolding rel_to_urrel_def
by (subst Abs_urrel_inverse) auto
hence ‹∃r . ∀ x . Rep_rel Π (ωκ x) = Rep_urrel r (ωυ x)›
by (auto intro!: exI[where x=‹rel_to_urrel Π›])
then obtain r where r_prop: ‹Rep_rel Π (ωκ x) = Rep_urrel r (ωυ x)› for x
by blast
assume ‹AOT_model_denotes Π' ⟹
(⋀v x. ∃w. AOT_model_concrete w x ⟹
AOT_model_valid_in v (Rep_rel Π' x) =
AOT_model_valid_in v (Rep_rel Π x)) ⟹ AOT_model_enc κ Π'› for Π'
hence ‹AOT_model_denotes Π' ⟹
(⋀v x. AOT_model_valid_in v (Rep_rel Π' (ωκ x)) =
AOT_model_valid_in v (Rep_rel Π (ωκ x))) ⟹ AOT_model_enc κ Π'› for Π'
by (metis AOT_model_concrete_κ.simps(2) AOT_model_concrete_κ.simps(3)
κ.exhaust_disc is_ακ_def is_ωκ_def is_nullκ_def)
hence ‹(⋀v x. AOT_model_valid_in v (Rep_urrel r (ωυ x)) =
AOT_model_valid_in v (Rep_rel Π (ωκ x))) ⟹ r ∈ a› for r
unfolding a_def[symmetric] AOT_model_enc_κ_def apply simp
by (smt (verit, best) AOT_rel_equiv_def Abs_rel_inverse Quotient3_def
κυ.simps(1) iso_tuple_UNIV_I urrel_quotient3 urrel_to_rel_def)
hence ‹(⋀v x. AOT_model_valid_in v (Rep_urrel r' (ωυ x)) =
AOT_model_valid_in v (Rep_urrel r (ωυ x))) ⟹ r' ∈ a› for r'
unfolding r_prop.
hence ‹⋀s. urrel_to_ωrel s = urrel_to_ωrel r ⟹ s ∈ a›
by (metis urrel_to_ωrel_def)
hence 0: ‹⋀s. urrel_to_ωrel s = urrel_to_ωrel r ⟹ s ∈ b›
using ασ_eq_ord_exts_all ασ_eq ext ασ_ασ' by blast

assume Π'_den: ‹AOT_model_denotes Π'›
assume ‹∃w. AOT_model_concrete w x ⟹ AOT_model_valid_in v (Rep_rel Π' x) =
AOT_model_valid_in v (Rep_rel Π x)› for v x
hence ‹AOT_model_valid_in v (Rep_rel Π' (ωκ x)) =
AOT_model_valid_in v (Rep_rel Π (ωκ x))› for v x
using AOT_model_ω_concrete_in_some_world AOT_model_concrete_κ.simps(1)
by presburger
hence ‹AOT_model_valid_in v (Rep_urrel (rel_to_urrel Π') (ωυ x)) =
AOT_model_valid_in v (Rep_urrel r (ωυ x))› for v x
by (smt (verit, best) AOT_rel_equiv_def Abs_rel_inverse Quotient3_def
κυ.simps(1) iso_tuple_UNIV_I r_prop urrel_quotient3 urrel_to_rel_def Π'_den)
hence ‹urrel_to_ωrel (rel_to_urrel Π') = urrel_to_ωrel r›
by (metis (full_types) AOT_urrel_ωequiv_def Quotient3_def urrel_ωrel_quot)
hence ‹rel_to_urrel Π' ∈ b› using 0 by blast
thus ‹AOT_model_enc κ' Π'›
unfolding b_def[symmetric] AOT_model_enc_κ_def by (auto simp: Π'_den)
next
fix κ κ' :: κ and Π Π' :: ‹<κ>› and w :: w
assume ext: ‹AOT_ExtendedModel›
assume ‹AOT_model_denotes κ›
moreover assume ‹∄w. AOT_model_concrete w κ›
ultimately obtain a where a_def: ‹ακ a = κ›
by (metis AOT_model_ω_concrete_in_some_world AOT_model_concrete_κ.simps(1)
AOT_model_denotes_κ_def κ.discI(3) κ.exhaust_sel)
assume ‹AOT_model_denotes κ'›
moreover assume ‹∄w. AOT_model_concrete w κ'›
ultimately obtain b where b_def: ‹ακ b = κ'›
by (metis AOT_model_ω_concrete_in_some_world AOT_model_concrete_κ.simps(1)
AOT_model_denotes_κ_def κ.discI(3) κ.exhaust_sel)
assume ‹AOT_model_denotes Π' ⟹ AOT_model_valid_in w (Rep_rel Π' κ) =
AOT_model_valid_in w (Rep_rel Π' κ')› for Π' w
hence ‹AOT_model_valid_in w (Rep_urrel r (κυ κ)) =
AOT_model_valid_in w (Rep_urrel r (κυ κ'))› for r
by (metis AOT_rel_equiv_def Abs_rel_inverse Quotient3_rel_rep
iso_tuple_UNIV_I urrel_quotient3 urrel_to_rel_def)
hence ‹let r = (Abs_urrel (λ u . ε⇩𝗈 w . u = κυ κ)) in
AOT_model_valid_in w (Rep_urrel r (κυ κ)) =
AOT_model_valid_in w (Rep_urrel r (κυ κ'))›
by presburger
hence ασ_eq: ‹ασ a = ασ b›
unfolding Let_def
apply (subst (asm) (1 2) Abs_urrel_inverse)
using AOT_model_proposition_choice_simp a_def b_def by force+
assume Π_den: ‹AOT_model_denotes Π›
have ‹¬AOT_model_valid_in w (Rep_rel Π (SOME xa. κυ xa = nullυ x))› for x w
by (metis (mono_tags, lifting) AOT_model_denotes_κ_def
AOT_model_denotes_rel.rep_eq κ.exhaust_disc κυ.simps(1,2,3)
‹AOT_model_denotes Π› υ.disc(8) υ.disc(9) υ.distinct(3)
is_ακ_def is_ωκ_def verit_sko_ex')
moreover have ‹Rep_rel Π (ωκ x) = Rep_rel Π (SOME xa. κυ xa = ωυ x)› for x
by (metis (mono_tags, lifting) AOT_model_denotes_rel.rep_eq
AOT_model_term_equiv_κ_def κυ.simps(1) Π_den verit_sko_ex')
ultimately have ‹Rep_rel Π (ωκ x) = Rep_urrel (rel_to_urrel Π) (ωυ x)› for x
unfolding rel_to_urrel_def
by (subst Abs_urrel_inverse) auto
hence ‹∃r . ∀ x . Rep_rel Π (ωκ x) = Rep_urrel r (ωυ x)›
by (auto intro!: exI[where x=‹rel_to_urrel Π›])
then obtain r where r_prop: ‹Rep_rel Π (ωκ x) = Rep_urrel r (ωυ x)› for x
by blast

assume ‹∃Π'. AOT_model_denotes Π' ∧
AOT_model_enc κ Π' ∧
(∀v x. (∃w. AOT_model_concrete w x) ⟶ AOT_model_valid_in v (Rep_rel Π' x) =
AOT_model_valid_in v (Rep_rel Π x))›
then obtain Π' where
Π'_den: ‹AOT_model_denotes Π'› and
κ_enc_Π': ‹AOT_model_enc κ Π'› and
Π'_prop: ‹∃w. AOT_model_concrete w x ⟹
AOT_model_valid_in v (Rep_rel Π' x) =
AOT_model_valid_in v (Rep_rel Π x)› for v x
by blast
have ‹AOT_model_valid_in v (Rep_rel Π' (ωκ x)) =
AOT_model_valid_in v (Rep_rel Π (ωκ x))› for x v
hence 0: ‹AOT_urrel_ωequiv (rel_to_urrel Π') (rel_to_urrel Π)›
unfolding AOT_urrel_ωequiv_def
by (smt (verit) AOT_rel_equiv_def Abs_rel_inverse Quotient3_def
κυ.simps(1) iso_tuple_UNIV_I urrel_quotient3 urrel_to_rel_def
Π_den Π'_den)
have ‹rel_to_urrel Π' ∈ a›
and ‹urrel_to_ωrel (rel_to_urrel Π') = urrel_to_ωrel (rel_to_urrel Π)›
apply (metis AOT_model_enc_κ_def κ.simps(11) κ_enc_Π' a_def)
by (metis Quotient3_rel 0 urrel_ωrel_quot)
hence ‹∃s. s ∈ b ∧ urrel_to_ωrel s = urrel_to_ωrel (rel_to_urrel Π)›
using ασ_eq_ord_exts_ex ασ_eq ext ασ_ασ' by blast
then obtain s where
s_prop: ‹s ∈ b ∧ urrel_to_ωrel s = urrel_to_ωrel (rel_to_urrel Π)›
by blast
then obtain Π'' where
Π''_prop: ‹rel_to_urrel Π'' = s› and Π''_den: ‹AOT_model_denotes Π''›
by (metis AOT_rel_equiv_def Quotient3_def urrel_quotient3)
moreover have ‹AOT_model_enc κ' Π''›
by (metis AOT_model_enc_κ_def Π''_den Π''_prop κ.simps(11) b_def s_prop)
moreover have ‹AOT_model_valid_in v (Rep_rel Π'' x) =
AOT_model_valid_in v (Rep_rel Π x)›
if ‹∃w. AOT_model_concrete w x› for v x
proof(insert that)
assume ‹∃w. AOT_model_concrete w x›
then obtain u where x_def: ‹x = ωκ u›
by (metis AOT_model_concrete_κ.simps(2,3) κ.exhaust)
show ‹AOT_model_valid_in v (Rep_rel Π'' x) =
AOT_model_valid_in v (Rep_rel Π x)›
unfolding x_def
by (smt (verit, best) AOT_rel_equiv_def Abs_rel_inverse Quotient3_def
Π''_den Π''_prop Π_den κυ.simps(1) iso_tuple_UNIV_I s_prop
urrel_quotient3 urrel_to_ωrel_def urrel_to_rel_def)
qed
ultimately show ‹∃Π'. AOT_model_denotes Π' ∧ AOT_model_enc κ' Π' ∧
(∀v x. (∃w. AOT_model_concrete w x) ⟶ AOT_model_valid_in v (Rep_rel Π' x) =
AOT_model_valid_in v (Rep_rel Π x))›
apply (safe intro!: exI[where x=Π''])
by auto
qed
end

text‹Products of unary individual terms and individual terms are individual terms.
A tuple is regular, if at most one element does not denote. I.e. a pair is
regular, if the first (unary) element denotes and the second is regular (i.e.
at most one of its recursive tuple elements does not denote), or the first does
not denote, but the second denotes (i.e. all its recursive tuple elements
denote).›
instantiation prod :: (AOT_UnaryIndividualTerm, AOT_IndividualTerm) AOT_IndividualTerm
begin
definition AOT_model_regular_prod :: ‹'a×'b ⇒ bool› where
‹AOT_model_regular_prod ≡ λ (x,y) . AOT_model_denotes x ∧ AOT_model_regular y ∨
¬AOT_model_denotes x ∧ AOT_model_denotes y›
definition AOT_model_term_equiv_prod :: ‹'a×'b ⇒ 'a×'b ⇒ bool› where
‹AOT_model_term_equiv_prod ≡  λ (x⇩1,y⇩1) (x⇩2,y⇩2) .
AOT_model_term_equiv x⇩1 x⇩2 ∧ AOT_model_term_equiv y⇩1 y⇩2›
function AOT_model_irregular_prod :: ‹('a×'b ⇒ 𝗈) ⇒ 'a×'b ⇒ 𝗈› where
AOT_model_irregular_proj2: ‹AOT_model_denotes x ⟹
AOT_model_irregular φ (x,y) =
AOT_model_irregular (λy. φ (SOME x' . AOT_model_term_equiv x x', y)) y›
| AOT_model_irregular_proj1: ‹¬AOT_model_denotes x ∧ AOT_model_denotes y ⟹
AOT_model_irregular φ (x,y) =
AOT_model_irregular (λx. φ (x, SOME y' . AOT_model_term_equiv y y')) x›
| AOT_model_irregular_prod_generic: ‹¬AOT_model_denotes x ∧ ¬AOT_model_denotes y ⟹
AOT_model_irregular φ (x,y) =
(SOME Φ . AOT_model_irregular_spec Φ AOT_model_regular AOT_model_term_equiv)
φ (x,y)›
by auto blast
termination using "termination" by blast

instance proof
obtain x :: 'a and y :: 'b where
‹¬AOT_model_denotes x› and ‹¬AOT_model_denotes y›
by (meson AOT_model_nondenoting_ex AOT_model_denoting_ex)
thus ‹∃x::'a×'b. ¬AOT_model_denotes x›
by (auto simp: AOT_model_denotes_prod_def AOT_model_regular_prod_def)
next
show ‹equivp (AOT_model_term_equiv :: 'a×'b ⇒ 'a×'b ⇒ bool)›
by (rule equivpI; rule reflpI sympI transpI;
equivp_reflp prod.case_eq_if case_prod_unfold equivp_symp)
(metis equivp_transp[OF AOT_model_term_equiv_part_equivp])
next
show ‹¬AOT_model_regular x ⟹ ¬ AOT_model_denotes x› for x :: ‹'a×'b›
by (metis (mono_tags, lifting) AOT_model_denotes_prod_def case_prod_unfold
AOT_model_irregular_nondenoting AOT_model_regular_prod_def)
next
fix x y :: ‹'a×'b›
show ‹AOT_model_term_equiv x y ⟹ AOT_model_denotes x = AOT_model_denotes y›
by (metis (mono_tags, lifting) AOT_model_denotes_prod_def case_prod_beta
AOT_model_term_equiv_denotes AOT_model_term_equiv_prod_def )
next
fix x y :: ‹'a×'b›
show ‹AOT_model_term_equiv x y ⟹ AOT_model_regular x = AOT_model_regular y›
by (induct x; induct y;
(meson AOT_model_term_equiv_denotes AOT_model_term_equiv_regular)
next
interpret sp: AOT_model_irregular_spec ‹λφ (x::'a×'b) . ε⇩𝗈 w . False›
AOT_model_regular AOT_model_term_equiv
have ex_spec: ‹∃ φ :: ('a×'b ⇒ 𝗈) ⇒ 'a×'b ⇒ 𝗈 .
AOT_model_irregular_spec φ AOT_model_regular AOT_model_term_equiv›
using sp.AOT_model_irregular_spec_axioms by blast
have some_spec: ‹AOT_model_irregular_spec
(SOME φ :: ('a×'b ⇒ 𝗈) ⇒ 'a×'b ⇒ 𝗈 .
AOT_model_irregular_spec φ AOT_model_regular AOT_model_term_equiv)
AOT_model_regular AOT_model_term_equiv›
using someI_ex[OF ex_spec] by argo
interpret sp_some: AOT_model_irregular_spec
‹SOME φ :: ('a×'b ⇒ 𝗈) ⇒ 'a×'b ⇒ 𝗈 .
AOT_model_irregular_spec φ AOT_model_regular AOT_model_term_equiv›
AOT_model_regular AOT_model_term_equiv
using some_spec by blast
show ‹AOT_model_irregular_spec (AOT_model_irregular :: ('a×'b ⇒ 𝗈) ⇒ 'a×'b ⇒ 𝗈)
AOT_model_regular AOT_model_term_equiv›
proof
have ‹¬AOT_model_valid_in w (AOT_model_irregular φ (a, b))›
for w φ and a :: 'a and b :: 'b
by (induct arbitrary: φ rule: AOT_model_irregular_prod.induct)
(auto simp: AOT_model_irregular_false sp_some.AOT_model_irregular_false)
thus "¬AOT_model_valid_in w (AOT_model_irregular φ x)" for w φ and x :: ‹'a×'b›
by (induct x)
next
{
fix x⇩1 y⇩1 :: 'a and x⇩2 y⇩2 :: 'b and φ :: ‹'a×'b⇒𝗈›
assume x⇩1y⇩1_equiv: ‹AOT_model_term_equiv x⇩1 y⇩1›
moreover assume x⇩2y⇩2_equiv: ‹AOT_model_term_equiv x⇩2 y⇩2›
ultimately have xy_equiv: ‹AOT_model_term_equiv (x⇩1,x⇩2) (y⇩1,y⇩2)›
{
assume ‹AOT_model_denotes x⇩1›
moreover hence ‹AOT_model_denotes y⇩1›
using AOT_model_term_equiv_denotes AOT_model_term_equiv_regular
x⇩1y⇩1_equiv x⇩2y⇩2_equiv by blast
ultimately have ‹AOT_model_irregular φ (x⇩1,x⇩2) =
AOT_model_irregular φ (y⇩1,y⇩2)›
using AOT_model_irregular_equiv AOT_model_term_equiv_eps(3)
x⇩1y⇩1_equiv x⇩2y⇩2_equiv by fastforce
}
moreover {
assume ‹~AOT_model_denotes x⇩1 ∧ AOT_model_denotes x⇩2›
moreover hence ‹~AOT_model_denotes y⇩1 ∧ AOT_model_denotes y⇩2›
by (meson AOT_model_term_equiv_denotes x⇩1y⇩1_equiv x⇩2y⇩2_equiv)
ultimately have ‹AOT_model_irregular φ (x⇩1,x⇩2) =
AOT_model_irregular φ (y⇩1,y⇩2)›
using AOT_model_irregular_equiv AOT_model_term_equiv_eps(3)
x⇩1y⇩1_equiv x⇩2y⇩2_equiv by fastforce
}
moreover {
assume denotes_x: ‹(¬AOT_model_denotes x⇩1 ∧ ¬AOT_model_denotes x⇩2)›
hence denotes_y: ‹(¬AOT_model_denotes y⇩1 ∧ ¬AOT_model_denotes y⇩2)›
by (meson AOT_model_term_equiv_denotes AOT_model_term_equiv_regular
x⇩1y⇩1_equiv x⇩2y⇩2_equiv)
have eps_eq: ‹Eps (AOT_model_term_equiv x⇩1) = Eps (AOT_model_term_equiv y⇩1)›
have ‹AOT_model_irregular φ (x⇩1,x⇩2) = AOT_model_irregular φ (y⇩1,y⇩2)›
using denotes_x denotes_y
using sp_some.AOT_model_irregular_equiv xy_equiv by auto
}
moreover {
assume denotes_x: ‹¬AOT_model_denotes x⇩1 ∧ AOT_model_denotes x⇩2›
hence denotes_y: ‹¬AOT_model_denotes y⇩1 ∧ AOT_model_denotes y⇩2›
by (meson AOT_model_term_equiv_denotes x⇩1y⇩1_equiv x⇩2y⇩2_equiv)
have eps_eq: ‹Eps (AOT_model_term_equiv x⇩2) = Eps (AOT_model_term_equiv y⇩2)›
have ‹AOT_model_irregular φ (x⇩1,x⇩2) = AOT_model_irregular φ (y⇩1,y⇩2)›
using denotes_x denotes_y
using AOT_model_irregular_nondenoting calculation(2) by blast
}
ultimately have ‹AOT_model_irregular φ (x⇩1,x⇩2) = AOT_model_irregular φ (y⇩1,y⇩2)›
using AOT_model_term_equiv_denotes AOT_model_term_equiv_regular
sp_some.AOT_model_irregular_equiv x⇩1y⇩1_equiv x⇩2y⇩2_equiv xy_equiv
by blast
} note 0 = this
show ‹AOT_model_term_equiv x y ⟹
AOT_model_irregular φ x = AOT_model_irregular φ y›
for x y :: ‹'a×'b› and φ
by (induct x; induct y; simp add: AOT_model_term_equiv_prod_def 0)
next
fix φ ψ :: ‹'a×'b ⇒ 𝗈›
assume ‹AOT_model_regular x ⟹ φ x = ψ x› for x
hence ‹φ (x, y) = ψ (x, y)›
if ‹AOT_model_denotes x ∧ AOT_model_regular y ∨
¬AOT_model_denotes x ∧ AOT_model_denotes y› for x y
using that unfolding AOT_model_regular_prod_def by simp
hence ‹AOT_model_irregular φ (x,y) = AOT_model_irregular ψ (x,y)›
for x :: 'a and y :: 'b
proof (induct arbitrary: ψ φ rule: AOT_model_irregular_prod.induct)
case (1 x y φ)
thus ?case
apply simp
by (meson AOT_model_irregular_eqI AOT_model_irregular_nondenoting
AOT_model_term_equiv_denotes AOT_model_term_equiv_eps(1))
next
case (2 x y φ)
thus ?case
apply simp
by (meson AOT_model_irregular_nondenoting AOT_model_term_equiv_denotes
AOT_model_term_equiv_eps(1))
next
case (3 x y φ)
thus ?case
apply simp
by (metis (mono_tags, lifting) AOT_model_regular_prod_def case_prod_conv
sp_some.AOT_model_irregular_eqI surj_pair)
qed
thus ‹AOT_model_irregular φ x = AOT_model_irregular ψ x› for  x :: ‹'a×'b›
by (metis surjective_pairing)
qed
qed
end

text‹Introduction rules for term equivalence on tuple terms.›
lemma AOT_meta_prod_equivI:
shows "⋀ (a::'a::AOT_UnaryIndividualTerm) x (y :: 'b::AOT_IndividualTerm) .
AOT_model_term_equiv x y ⟹ AOT_model_term_equiv (a,x) (a,y)"
and "⋀ (x::'a::AOT_UnaryIndividualTerm) y (b :: 'b::AOT_IndividualTerm) .
AOT_model_term_equiv x y ⟹ AOT_model_term_equiv (x,b) (y,b)"
unfolding AOT_model_term_equiv_prod_def

text‹The type of propositions are trivial instances of terms.›

instantiation 𝗈 :: AOT_Term
begin
definition AOT_model_denotes_𝗈 :: ‹𝗈 ⇒ bool› where
‹AOT_model_denotes_𝗈 ≡ λ_. True›
instance proof
show ‹∃x::𝗈. AOT_model_denotes x›
qed
end

text‹AOT's variables are modelled by restricting the type of terms to those terms
that denote.›
typedef 'a AOT_var = ‹{ x :: 'a::AOT_Term . AOT_model_denotes x }›
morphisms AOT_term_of_var AOT_var_of_term

text‹Simplify automatically generated theorems and rules.›
declare AOT_var_of_term_induct[induct del]
AOT_var_of_term_cases[cases del]
AOT_term_of_var_induct[induct del]
AOT_term_of_var_cases[cases del]
lemmas AOT_var_of_term_inverse = AOT_var_of_term_inverse[simplified]
and AOT_var_of_term_inject = AOT_var_of_term_inject[simplified]
and AOT_var_of_term_induct =
AOT_var_of_term_induct[simplified, induct type: AOT_var]
and AOT_var_of_term_cases =
AOT_var_of_term_cases[simplified, cases type: AOT_var]
and AOT_term_of_var = AOT_term_of_var[simplified]
and AOT_term_of_var_cases =
AOT_term_of_var_cases[simplified, induct pred: AOT_term_of_var]
and AOT_term_of_var_induct =
AOT_term_of_var_induct[simplified, induct pred: AOT_term_of_var]
and AOT_term_of_var_inverse = AOT_term_of_var_inverse[simplified]
and AOT_term_of_var_inject = AOT_term_of_var_inject[simplified]

text‹Equivalence by definition is modelled as necessary equivalence.›
consts AOT_model_equiv_def :: ‹𝗈 ⇒ 𝗈 ⇒ bool›
specification(AOT_model_equiv_def)
AOT_model_equiv_def: ‹AOT_model_equiv_def φ ψ = (∀ v . AOT_model_valid_in v φ =
AOT_model_valid_in v ψ)›
by (rule exI[where x=‹λ φ ψ . ∀ v . AOT_model_valid_in v φ =
AOT_model_valid_in v ψ›]) simp

text‹Identity by definition is modelled as identity for denoting terms plus
co-denoting.›
consts AOT_model_id_def :: ‹('b ⇒ 'a::AOT_Term) ⇒ ('b ⇒ 'a) ⇒ bool›
specification(AOT_model_id_def)
AOT_model_id_def: ‹(AOT_model_id_def τ σ) = (∀ α . if AOT_model_denotes (σ α)
then τ α = σ α
else ¬AOT_model_denotes (τ α))›
by (rule exI[where x="λ τ σ . ∀ α . if AOT_model_denotes (σ α)
then τ α = σ α
else ¬AOT_model_denotes (τ α)"])
blast
text‹To reduce definitions by identity without free variables to definitions
by identity with free variables acting on the unit type, we give the unit type
a trivial instantiation to @{class AOT_Term}.›
instantiation unit :: AOT_Term
begin
definition AOT_model_denotes_unit :: ‹unit ⇒ bool› where
‹AOT_model_denotes_unit ≡ λ_. True›
end

text‹Modally-strict and modally-fragile axioms are as necessary,
resp. actually valid propositions.›
definition AOT_model_axiom where
‹AOT_model_axiom ≡ λ φ . ∀ v . AOT_model_valid_in v φ›
definition AOT_model_act_axiom where
‹AOT_model_act_axiom ≡ λ φ . AOT_model_valid_in w⇩0 φ›

lemma AOT_model_axiomI:
assumes ‹⋀v . AOT_model_valid_in v φ›
shows ‹AOT_model_axiom φ›
unfolding AOT_model_axiom_def using assms ..

lemma AOT_model_act_axiomI:
assumes ‹AOT_model_valid_in w⇩0 φ›
shows ‹AOT_model_act_axiom φ›
unfolding AOT_model_act_axiom_def using assms .

(*<*)
end
(*>*)```