Quelle  AOT_model.thy

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

declare[[typedef_overloaded]]
(*>*)

section‹References›

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

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

 ›

section‹Model for the Logic of AOT›

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

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_do :: ‹o==>(w==>bool)› where
  do_surj: ‹surj AOT_model_do›

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

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==>o==>bool› where
  ‹AOT_model_valid_in w φ ≡ AOT_model_do φ 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) ==> o› (binder ‹ε_\o › 8)
  where ‹ε_\o w. φ w ≡ (inv AOT_model_do) φ›
lemma AOT_model_proposition_choice_simp: ‹AOT_model_valid_in w (ε_\o w. φ w) = φ w›
  by (simp add: surj_f_inv_f[OF do_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 . (ε_\o 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 . ε_\o 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₀ (?pick (συ s) x) =
 AOT_model_valid_in w₀ (?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›
        by (simp add: less_exp)
      hence ‹m*m < (2^m)*(2^m)›
        by (simp add: mult_strict_mono)
      moreover have ‹… = 2^(m+m)›
        by (simp add: power_add)
      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|›
      by (simp add: cinfinite_def)
    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 . ε_\o 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₀›
  by (rule exI[where x=‹λ_ w. w ≠ w₀›]) (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›
    by (simp add: AOT_model_denotes_prod_def AOT_model_denoting_ex)
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 ==> o) ==> 'a ==> o›
    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 ==> o) ==> 'a ==> o›
  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_κ :: ‹(κ ==> o) ==> κ ==> o› 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›])
       (simp add: AOT_model_denotes_κ_def)
next
  show ‹∃x :: κ. ¬AOT_model_denotes x›
    by (rule exI[where x=‹nullκ undefined›])
       (simp add: AOT_model_denotes_κ_def AOT_model_regular_κ_def)
next
  show "¬AOT_model_regular x ==> ¬ AOT_model_denotes x" for x :: κ
    by (simp add: AOT_model_regular_κ_def)
next
  show ‹equivp (AOT_model_term_equiv :: κ ==> κ ==> bool)›
    by (rule equivpI; rule reflpI exI sympI transpI)
       (simp_all add: AOT_model_term_equiv_κ_def)
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›
    by (simp add: AOT_model_regular_κ_def)
next
  have "AOT_model_irregular_spec (λ φ (x::κ) . ε_\<o> 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::(κ==>o) ==> κ ==> o)
 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 ==> o) 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 ==> o) ==> ('a ==> o)› 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›
  by (simp add: fix_irregular_def)

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. ε_\o 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. ε_\o 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)›
    by (simp add: AOT_model_denotes_rel.rep_eq)
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 . ε_\o 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›
    by (simp add: Abs_rel_inverse AOT_model_proposition_choice_simp
                  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 :: ‹<\<kappa>> ==> urrel› where
  ‹rel_to_urrel ≡ λ Π . Abs_urrel (λ u . Rep_rel Π (SOME x . κυ x = u))›
definition urrel_to_rel :: ‹urrel ==> <\<kappa>>› 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 :: ‹κ ==> o›
    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₀ 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_κ :: ‹κ ==> <\<kappa>> ==> 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)}›])
  apply (simp add: AOT_model_enc_κ_def AOT_model_denotes_κ_def)
  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 :: κ
    by (simp add: AOT_model_regular_κ_def)
next
  fix F G :: ‹<\<kappa>>›
  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₀ 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 Π Π' :: ‹<\<kappa>>› 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 . ε_\o 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 Π Π' :: ‹<\<kappa>>› 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 . ε_\o 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
    by (simp add: AOT_model_ψ_concrete_in_some_world Π'_prop)
  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₁,y₁) (x₂,y₂) .
 AOT_model_term_equiv x₁ x₂ ∧ AOT_model_term_equiv y₁ y₂›
function AOT_model_irregular_prod :: ‹('a×'b ==> o) ==> 'a×'b ==> o› 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;
        simp add: AOT_model_term_equiv_prod_def AOT_model_term_equiv_part_equivp
                  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;
        simp add: AOT_model_term_equiv_prod_def AOT_model_regular_prod_def)
       (meson AOT_model_term_equiv_denotes AOT_model_term_equiv_regular)
next
  interpret sp: AOT_model_irregular_spec ‹λφ (x::'a×'b) . ε_\o w . False›
                    AOT_model_regular AOT_model_term_equiv
    by (simp add: AOT_model_irregular_spec_def AOT_model_proposition_choice_simp)
  have ex_spec: ‹∃ φ :: ('a×'b ==> o) ==> 'a×'b ==> o .
 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 ==> o) ==> 'a×'b ==> o .
 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 ==> o) ==> 'a×'b ==> o .
 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 ==> o) ==> 'a×'b ==> o)
 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₁ y₁ :: 'a and x₂ y₂ :: 'b and φ :: ‹'a×'b==>o›
      assume x₁y₁_equiv: ‹AOT_model_term_equiv x₁ y₁›
      moreover assume x₂y₂_equiv: ‹AOT_model_term_equiv x₂ y₂›
      ultimately have xy_equiv: ‹AOT_model_term_equiv (x₁,x₂) (y₁,y₂)›
        by (simp add: AOT_model_term_equiv_prod_def)
      {
        assume ‹AOT_model_denotes x₁›
        moreover hence ‹AOT_model_denotes y₁›
          using AOT_model_term_equiv_denotes AOT_model_term_equiv_regular
                x₁y₁_equiv x₂y₂_equiv by blast
        ultimately have ‹AOT_model_irregular φ (x₁,x₂) =
 AOT_model_irregular φ (y₁,y₂)›
          using AOT_model_irregular_equiv AOT_model_term_equiv_eps(3)
                x₁y₁_equiv x₂y₂_equiv by fastforce
      }
      moreover {
        assume ‹~AOT_model_denotes x₁ ∧ AOT_model_denotes x₂›
        moreover hence ‹~AOT_model_denotes y₁ ∧ AOT_model_denotes y₂›
          by (meson AOT_model_term_equiv_denotes x₁y₁_equiv x₂y₂_equiv)
        ultimately have ‹AOT_model_irregular φ (x₁,x₂) =
 AOT_model_irregular φ (y₁,y₂)›
          using AOT_model_irregular_equiv AOT_model_term_equiv_eps(3)
                x₁y₁_equiv x₂y₂_equiv by fastforce
      }
      moreover {
        assume denotes_x: ‹(¬AOT_model_denotes x₁ ∧ ¬AOT_model_denotes x₂)›
        hence denotes_y: ‹(¬AOT_model_denotes y₁ ∧ ¬AOT_model_denotes y₂)›
          by (meson AOT_model_term_equiv_denotes AOT_model_term_equiv_regular
                    x₁y₁_equiv x₂y₂_equiv)
        have eps_eq: ‹Eps (AOT_model_term_equiv x₁) = Eps (AOT_model_term_equiv y₁)›
          by (simp add: AOT_model_term_equiv_eps(3) x₁y₁_equiv)
        have ‹AOT_model_irregular φ (x₁,x₂) = AOT_model_irregular φ (y₁,y₂)›
          using denotes_x denotes_y
          using sp_some.AOT_model_irregular_equiv xy_equiv by auto
      }
      moreover {
        assume denotes_x: ‹¬AOT_model_denotes x₁ ∧ AOT_model_denotes x₂›
        hence denotes_y: ‹¬AOT_model_denotes y₁ ∧ AOT_model_denotes y₂›
          by (meson AOT_model_term_equiv_denotes x₁y₁_equiv x₂y₂_equiv)
        have eps_eq: ‹Eps (AOT_model_term_equiv x₂) = Eps (AOT_model_term_equiv y₂)›
          by (simp add: AOT_model_term_equiv_eps(3) x₂y₂_equiv)
        have ‹AOT_model_irregular φ (x₁,x₂) = AOT_model_irregular φ (y₁,y₂)›
          using denotes_x denotes_y
          using AOT_model_irregular_nondenoting calculation(2) by blast
      }
      ultimately have ‹AOT_model_irregular φ (x₁,x₂) = AOT_model_irregular φ (y₁,y₂)›
        using AOT_model_term_equiv_denotes AOT_model_term_equiv_regular
              sp_some.AOT_model_irregular_equiv x₁y₁_equiv x₂y₂_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 ==> o›
    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
    by (simp add: AOT_model_term_equiv_part_equivp equivp_reflp)+

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

instantiation o :: AOT_Term
begin
definition AOT_model_denotes_o :: ‹o ==> bool› where
  ‹AOT_model_denotes_o ≡ λ_. True›
instance proof
  show ‹∃x::o. AOT_model_denotes x›
    by (simp add: AOT_model_denotes_o_def)
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
  by (simp add: AOT_model_denoting_ex)

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 :: ‹o ==> o ==> 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›
instance proof qed(simp add: AOT_model_denotes_unit_def)
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₀ φ›

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₀ φ›
  shows ‹AOT_model_act_axiom φ›
  unfolding AOT_model_act_axiom_def using assms .

(*<*)
end
(*>*)