Theory Semantics
theory Semantics
imports Syntax
begin
section ‹Semantics: applicative structures, Henkin models and standard models›
text ‹The semantics in BKK's own layered terminology, in their order: @{emph ‹applicative
structures›} ‹(D, @)› (BKK Definition 3.1), ‹Σ›-@{emph ‹evaluations›} ‹J = (D, @, E)›
(BKK Definition 3.18) with an @{emph ‹abstract›} evaluation function subject to BKK's four
conditions, ‹Σ›-@{emph ‹valuations›} and ‹Σ›-@{emph ‹models›} ‹M = (D, @, E, υ)› (BKK
Definitions 3.40 and 3.41), and the model class ‹ℳ⇘βfb⇙› (BKK Definition 3.49, the
‹Σ›-Henkin models of Definition 3.50). The signature ‹Σ› is a static parameter of the
whole development: the logical constants fixed by the term datatype plus the typed
parameters drawn from ‹'p›, exactly as BKK fix ‹Σ› at the start of their Section 3.
After the abstract notions, the recursive denotation ‹⦇t⦈⇘ξ⇙› is introduced as the
@{emph ‹canonical construction›} of an evaluation function over frame-like structures
(BKK's ‹Σ›-evaluations over frames); it is the vehicle for building concrete models
(the standard models here, and the term model of the completeness proof).›
subsection ‹Assignment update›
text ‹BKK's assignment update ‹φ,[a/X]› (BKK Definition 3.17), written in
function-update style with the variable's type subscripted: ‹ξ(x⇘σ⇙ := d)›.›
definition upd :: "(nat ⇒ ty ⇒ 'u) ⇒ nat ⇒ ty ⇒ 'u ⇒ (nat ⇒ ty ⇒ 'u)"
(‹_'(_⇘_⇙ := _')› [1000, 0, 0, 0] 1000) where
"ξ(x⇘σ⇙ := d) ≡ λn τ. if n = x ∧ τ = σ then d else ξ n τ"
lemma upd_same [simp]: "ξ(x⇘σ⇙ := d) x σ = d" by (simp add: upd_def)
lemma upd_comm: "(x, σ) ≠ (w, τ) ⟹ (ξ(x⇘σ⇙ := d))(w⇘τ⇙ := e) = (ξ(w⇘τ⇙ := e))(x⇘σ⇙ := d)"
by (auto simp: upd_def fun_eq_iff)
subsection ‹Applicative structures (BKK Definition 3.1)›
text ‹An applicative structure (BKK Definition 3.1) is a family of non-empty domains
‹D⇘τ⇙›, one per type, with an application operator. By BKK's Currying remark
(Remark 3.3) one binary operator suffices. The point of the
notion is its generality: a member of ‹D⇘α→β⇙› need not be a function, and distinct
members may behave identically under application. BKK's term structures
(Example 3.8), with well-formed formulae as domains and syntactic application, are the
guiding example --- their ‹βη›-quotient over a signature with a single constant even
fails functionality (Remark 3.15) --- and the term model of the completeness proof
below is such a quotient structure. A @{emph ‹frame›} (Definition 3.4) is the
set-theoretic special case in which the function domains consist of actual functions;
every frame is @{emph ‹functional›}: members of ‹D⇘α→β⇙› that agree on all arguments
are equal (Definition 3.5, Remark 3.6; property f of Definition 3.46). Functionality
is the one consequence of being a frame that the proofs use, so the abstract model
classes below are delineated by it; the frame-based construction of concrete models
follows later in this theory.›
locale app_struct = fixes Dm :: "ty ⇒ 'u ⇒ bool" and Ap :: "'u ⇒ 'u ⇒ 'u"
assumes as_nonempty: "∃a. Dm α a" and as_appTy: "Dm (α ❙⇒ β) f ⟹ Dm α a ⟹ Dm β (Ap f a)"
begin
text ‹Variable assignments into the structure (BKK Definition 3.17).›
definition asg :: "(nat ⇒ ty ⇒ 'u) ⇒ bool" where "asg ξ ≡ ∀n τ. Dm τ (ξ n τ)"
lemma asg_upd: "asg ξ ⟹ Dm σ d ⟹ asg (ξ(x⇘σ⇙ := d))"
by (auto simp: asg_def upd_def)
text ‹Functionality (BKK Definition 3.5), later property f of BKK Definition 3.46.›
definition functional :: bool where
"functional ≡ ∀α β f g. Dm (α ❙⇒ β) f ⟶ Dm (α ❙⇒ β) g ⟶
(∀a. Dm α a ⟶ Ap f a = Ap g a) ⟶ f = g"
end
subsection ‹‹Σ›-evaluations (BKK Definition 3.18)›
text ‹An evaluation function ‹E› maps assignments to typed functions from well-formed
formulae into the domains, subject to BKK's four conditions: (1) it extends the
assignment on variables, (2) it is homomorphic for application, (3) it depends only
on the assignment's values at the free variables (coincidence), and (4) it respects
‹β›-conversion (BKK state this via ‹β›-normal forms; over our typed ‹β›-equality
‹≈⇘τ⇙› of theory ‹Syntax› the two formulations coincide, cf.\ BKK Remark 3.19).
In addition ‹E› is typed: well-formed formulae of type ‹τ› denote in ‹D⇘τ⇙›.›
locale sigma_eval = app_struct Dm Ap for Dm :: "ty ⇒ 'u ⇒ bool" and Ap :: "'u ⇒ 'u ⇒ 'u" +
fixes Ee :: "(nat ⇒ ty ⇒ 'u) ⇒ 'p tm ⇒ 'u"
assumes ev_type: "wff⇘τ⇙(A) ⟹ asg ξ ⟹ Dm τ (Ee ξ A)"
and ev_var: "asg ξ ⟹ Ee ξ (n⇧f⇘σ⇙) = ξ n σ"
and ev_app: "wff⇘σ❙⇒τ⇙(F) ⟹ wff⇘σ⇙(A) ⟹ asg ξ ⟹ Ee ξ (F ❙⋅ A) = Ap (Ee ξ F) (Ee ξ A)"
and ev_coin: "wff⇘τ⇙(A) ⟹ asg ξ ⟹ asg ξ' ⟹ (⋀n σ. (n, σ) ∈ occ A ⟹ ξ n σ = ξ' n σ)
⟹ Ee ξ A = Ee ξ' A"
and ev_beta: "A ≈⇘τ⇙ B ⟹ asg ξ ⟹ Ee ξ A = Ee ξ B"
begin
text ‹The derived ‹β›-application law: the denotation of an abstraction is determined
applicatively by the openings of its body (from conditions (1)--(4);
the vehicle for all abstraction reasoning below). In the sharpened form the fresh-name
condition only concerns the typed occurrence ‹(x, σ)›, not the bare name (a name may
occur at several types).›
lemma ev_abs_app_occ:
assumes wb: "wff⇘σ❙⇒τ⇙(❙Λ⇘σ⇙ b)" and xi: "asg ξ"
and x: "(x, σ) ∉ occ b" and d: "Dm σ d"
shows "Ap (Ee ξ (❙Λ⇘σ⇙ b)) d = Ee (ξ(x⇘σ⇙ := d)) (b❙⟨x⇧f⇘σ⇙❙⟩)"
proof -
let ?ξ' = "ξ(x⇘σ⇙ := d)"
have xi': "asg ?ξ'" by (rule asg_upd[OF xi d])
have coin: "Ee ξ (❙Λ⇘σ⇙ b) = Ee ?ξ' (❙Λ⇘σ⇙ b)"
by (rule ev_coin[OF wb xi xi']) (use x in ‹auto simp: upd_def›)
have "Ap (Ee ξ (❙Λ⇘σ⇙ b)) d = Ap (Ee ?ξ' (❙Λ⇘σ⇙ b)) (Ee ?ξ' (x⇧f⇘σ⇙))"
by (simp add: coin ev_var[OF xi'])
also have "… = Ee ?ξ' ((❙Λ⇘σ⇙ b) ❙⋅ (x⇧f⇘σ⇙))"
by (rule ev_app[OF wb wff_Fre xi', symmetric])
also have "… = Ee ?ξ' (b❙⟨x⇧f⇘σ⇙❙⟩)"
by (rule ev_beta[OF beta[OF wb wff_Fre] xi'])
finally show ?thesis .
qed
lemma ev_abs_app:
assumes wb: "wff⇘σ❙⇒τ⇙(❙Λ⇘σ⇙ b)" and xi: "asg ξ" and x: "x ∉ fvs b" and d: "Dm σ d"
shows "Ap (Ee ξ (❙Λ⇘σ⇙ b)) d = Ee (ξ(x⇘σ⇙ := d)) (b❙⟨x⇧f⇘σ⇙❙⟩)"
by (metis d ev_abs_app_occ fst_conv fvs_eq_fst_occ image_eqI wb x xi)
end
subsection ‹‹Σ›-valuations and ‹Σ›-models (BKK Definitions 3.40 and 3.41)›
text ‹A ‹Σ›-valuation is a (total) function ‹υ : D⇘𝗈⇙ → {T, F}› --- rendered as a HOL
predicate --- satisfying the properties ‹L⇩¬(E(¬))›, ‹L⇩∨(E(∨))› and ‹L⇧α⇩∀(E(Π⇩α))› of
BKK's Figure 2. A ‹Σ›-evaluation together with such a valuation is a ‹Σ›-model.
Following BKK Definition 3.41 (and Remark 3.42) we include primitive equality
‹L⇧α⇩=(E(=⇩α))›, and --- extending BKK Definition 3.41, whose ‹Σ›-models have no
description operator --- a description property for ‹E(ι⇩α)›, matching ‹NK(ι)›. Since the logical
constants are closed, their denotations are assignment-independent (coincidence), so
the conditions are stated for an arbitrary assignment.›
locale sigma_model = sigma_eval Dm Ap Ee for
Dm :: "ty ⇒ 'u ⇒ bool" and Ap :: "'u ⇒ 'u ⇒ 'u" and Ee :: "(nat ⇒ ty ⇒ 'u) ⇒ 'p tm ⇒ 'u" +
fixes vl :: "'u ⇒ bool"
assumes vl_neg: "asg ξ ⟹ Dm 𝗈 a ⟹ vl (Ap (Ee ξ Neg) a) ⟷ ¬ vl a"
and vl_dis: "asg ξ ⟹ Dm 𝗈 a ⟹ Dm 𝗈 b ⟹ vl (Ap (Ap (Ee ξ Dis) a) b) ⟷ vl a ∨ vl b"
and vl_pi: "asg ξ ⟹ Dm (σ ❙⇒ 𝗈) f ⟹
vl (Ap (Ee ξ (Pi σ)) f) ⟷ (∀d. Dm σ d ⟶ vl (Ap f d))"
and vl_eq: "asg ξ ⟹ Dm σ a ⟹ Dm σ b ⟹ vl (Ap (Ap (Ee ξ (Eq σ)) a) b) ⟷ a = b"
and vl_iota: "asg ξ ⟹ Dm (σ ❙⇒ 𝗈) f ⟹ Dm σ a ⟹ (⋀b. Dm σ b ⟹ vl (Ap f b) ⟷ b = a)
⟹ Ap (Ee ξ (Iota σ)) f = a"
begin
text ‹Satisfaction and validity (BKK Definition 3.41): ‹M ⊨⇘φ⇙ A› iff ‹υ(E⇘φ⇙(A)) ≡ T›.›
definition satisfies :: "(nat ⇒ ty ⇒ 'u) ⇒ 'p tm ⇒ bool" (‹⊨⇘_⇙ _› [0, 40] 40) where
"⊨⇘ξ⇙ A ≡ vl (Ee ξ A)"
definition valid :: "'p tm ⇒ bool" (‹⊨ _› [40] 40) where
"⊨ A ≡ ∀ξ. asg ξ ⟶ ⊨⇘ξ⇙ A"
end
subsection ‹The model class ‹ℳ⇘βfb⇙› (BKK Definition 3.49)›
text ‹BKK's completeness class for ‹NK› is ‹ℳ⇘βfb⇙›: ‹Σ›-models with properties q, f
and b (BKK Definitions 3.46 and 3.49). With primitive equality, property q holds
automatically: its witness at type ‹α› is the denotation ‹E(=⇘α⇙)› (see ‹sat_Leib›
below). With property b the valuation is two-valued on ‹D⇘𝗈⇙›. By BKK Lemma 3.67
and Theorem 3.68, ‹ℳ⇘βfb⇙› is, up to isomorphism, the class of ‹Σ›-Henkin models of
BKK Definition 3.50; we call its members Henkin models.›
locale bkk_model = sigma_model Dm Ap Ee vl
for Dm :: "ty ⇒ 'u ⇒ bool" and Ap :: "'u ⇒ 'u ⇒ 'u"
and Ee :: "(nat ⇒ ty ⇒ 'u) ⇒ 'p tm ⇒ 'u" and vl :: "'u ⇒ bool" +
assumes prop_f: functional and prop_b: "Dm 𝗈 a ⟹ Dm 𝗈 b ⟹ vl a ⟷ vl b ⟹ a = b"
subsection ‹Truth values in a ‹Σ›-model (BKK Lemma 3.43)›
context sigma_model
begin
text ‹The canonical assignment, from non-emptiness of the domains.›
definition xi0 :: "nat ⇒ ty ⇒ 'u" where "xi0 ≡ λn τ. SOME a. Dm τ a"
lemma asg_xi0: "asg xi0" using as_nonempty by (auto simp: asg_def xi0_def intro: someI_ex)
text ‹Closed terms evaluate independently of the assignment; the canonical assignment serves as
the reference.›
lemma Ee_closed: "wff⇘τ⇙(A) ⟹ occ A = {} ⟹ asg ξ ⟹ Ee ξ A = Ee xi0 A"
using ev_coin asg_xi0 by blast
text ‹Evaluating ‹❙⊥ = ❙Π⇘𝗈⇙(Bnd 0)›: its truth means every boolean object is true.›
lemma vl_FalseB: assumes xi: "asg ξ" shows "vl (Ee ξ ❙⊥) ⟷ (∀d. Dm 𝗈 d ⟶ vl d)"
proof -
have wI: "wff⇘𝗈❙⇒𝗈⇙(❙Λ⇘𝗈⇙ (Bnd 0) :: 'p tm)"
by (rule wff_AbsI) (simp add: wff_Fre)
have e: "Ee ξ (❙⊥ :: 'p tm) = Ap (Ee ξ (Pi 𝗈)) (Ee ξ (❙Λ⇘𝗈⇙ (Bnd 0)))"
by (metis FalseB_def Forall_def ev_app wI wff_Pi xi)
have b: "Ap (Ee ξ (❙Λ⇘𝗈⇙ (Bnd 0))) d = d" if d: "Dm 𝗈 d" for d
using asg_upd ev_abs_app ev_var that wI xi by auto
show ?thesis unfolding e using vl_pi xi ev_type wI xi b by auto
qed
text ‹BKK Lemma 3.43: ‹υ(E(❙⊤)) ≡ T› and ‹υ(E(❙⊥)) ≡ F›; in particular ‹D⇘𝗈⇙› contains a
true and a false object (BKK Remark 3.44).›
lemma vl_TF: assumes xi: "asg ξ" shows "vl (Ee ξ ❙⊤) ∧ ¬ vl (Ee ξ ❙⊥)"
by (metis (mono_tags, lifting) TrueB_def sigma_eval.ev_app sigma_eval.ev_type
sigma_eval_axioms vl_FalseB vl_neg wff_FalseB wff_Neg wff_TrueB xi)
end
subsection ‹Model-relative truth and validity at a carrier›
text ‹Truth of ‹A› under the evaluation ‹Ee› and valuation ‹vl› of a model, at an assignment, and validity over
@{emph ‹all›} models of the class ‹ℳ⇘βfb⇙› at a given value carrier ‹'u› --- the
carrier appears explicitly in the notation ‹⊨('u) A›.›
definition rel_truth ::
"((nat ⇒ ty ⇒ 'u) ⇒ 'p tm ⇒ 'u) ⇒ ('u ⇒ bool) ⇒ (nat ⇒ ty ⇒ 'u) ⇒ 'p tm ⇒ bool"
(‹⟨_,_⟩,_ ⊨ _› [0, 0, 0, 61] 60) where
"⟨Ee,vl⟩,ξ ⊨ A ≡ vl (Ee ξ A)"
definition bkk_valid :: "'u itself ⇒ 'p tm ⇒ bool" where
"bkk_valid u A ≡ ∀Dm Ap Ee (vl :: 'u ⇒ bool) ξ.
bkk_model Dm Ap Ee vl ⟶ app_struct.asg Dm ξ ⟶ ⟨Ee,vl⟩,ξ ⊨ A"
syntax "_bkk_valid" :: "type ⇒ logic ⇒ logic" (‹⊨'(_') _› [1000, 61] 60)
syntax_consts "_bkk_valid" == bkk_valid
translations "_bkk_valid t A" == "CONST bkk_valid (_TYPE t) A"
definition bkk_consequence :: "'u itself ⇒ 'p tm set ⇒ 'p tm ⇒ bool" where
"bkk_consequence u Γ A ≡ ∀Dm Ap Ee (vl :: 'u ⇒ bool) ξ.
bkk_model Dm Ap Ee vl ⟶ app_struct.asg Dm ξ ⟶
(∀ B ∈ Γ . wff 𝗈 B ∧ ⟨Ee,vl⟩,ξ ⊨ B) ⟶ ⟨Ee,vl⟩,ξ ⊨ A"
syntax "_bkk_consequence" :: "logic ⇒ type ⇒ logic ⇒ logic" (‹_ ⊨'(_') _› [61, 1000, 61] 60)
syntax_consts "_bkk_consequence" == bkk_consequence
translations "_bkk_consequence Γ t A" == "CONST bkk_consequence (_TYPE t) Γ A"
text ‹Note the well-formedness conjunct in the antecedent: a context containing an
ill-formed member entails everything, vacuously. This is deliberate --- the relation is
only ever applied to well-formed contexts, and every exported theorem carries explicit
‹wff› hypotheses --- but it is worth stating.
Consequence is monotone in the hypotheses: enlarging the context only narrows the
models that must be checked.›
lemma bkk_consequence_mono: "Γ0 ⊨('u) A ⟹ Γ0 ⊆ Γ ⟹ Γ ⊨('u) A"
unfolding bkk_consequence_def by blast
subsection ‹‹Σ›-evaluations over frames: the canonical construction›
text ‹A @{emph ‹frame signature›} fixes the applicative structure (BKK Definition 3.1) and the
denotation objects of the logical constants and parameters. It carries no conditions; the
denotation and its purely semantic properties (coincidence, BKK Definition 3.18(3)) live here.›
locale frame_sig =
fixes Dm :: "ty ⇒ 'u ⇒ bool" (‹𝒟⇘_⇙›)
and Ap :: "'u ⇒ 'u ⇒ 'u" (infixl ‹❙@› 200)
and Lm :: "ty ⇒ ('u ⇒ 'u) ⇒ 'u" and Tv :: 'u and Fv :: 'u
and Ngv :: 'u and Dsv :: 'u and Iv :: "ty ⇒ 'u"
and Ev :: "ty ⇒ 'u" and Piv :: "ty ⇒ 'u" and Jv :: "'p ⇒ ty ⇒ 'u"
begin
text ‹The denotation ‹⦇A⦈⇘ξ⇙› of a term under an assignment ‹ξ› --- BKK's
evaluation function (BKK Definition 3.18).›
fun den :: "'p tm ⇒ (nat ⇒ ty ⇒ 'u) ⇒ 'u" (‹⦇_⦈⇘_⇙› [0,0] 1000) where
"⦇Bnd i⦈⇘ξ⇙ = Tv"
| "⦇n⇧f⇘σ⇙⦈⇘ξ⇙ = ξ n σ"
| "⦇p⇧p⇘σ⇙⦈⇘ξ⇙ = Jv p σ"
| "⦇Neg⦈⇘ξ⇙ = Ngv"
| "⦇Dis⦈⇘ξ⇙ = Dsv"
| "⦇Pi σ⦈⇘ξ⇙ = Piv σ"
| "⦇Iota σ⦈⇘ξ⇙ = Iv σ"
| "⦇s ❙⋅ t⦈⇘ξ⇙ = (⦇s⦈⇘ξ⇙) ❙@ (⦇t⦈⇘ξ⇙)"
| "⦇❙Λ⇘σ⇙ b⦈⇘ξ⇙ = Lm σ (λd. ⦇b❙⟨(fresh (fvs b))⇧f⇘σ⇙❙⟩⦈⇘ξ((fresh (fvs b))⇘σ⇙ := d)⇙)"
| "⦇Eq σ⦈⇘ξ⇙ = Ev σ"
text ‹The recursive equations must be kept out of the default simpset: the ‹Abs› equation
unfolds under a ‹λ› and would loop.›
declare den.simps(8,9) [simp del]
text ‹Coincidence (BKK Definition 3.18(3)): the denotation depends only on the assignment
at the (typed) free occurrences.›
lemma den_coincidence: "(⋀n τ. (n, τ) ∈ occ t ⟹ ξ n τ = ξ' n τ) ⟹ ⦇t⦈⇘ξ⇙ = ⦇t⦈⇘ξ'⇙"
proof (induct t arbitrary: ξ ξ' rule: size_induct)
case (App s1 t1)
hence "⦇s1⦈⇘ξ⇙ = ⦇s1⦈⇘ξ'⇙" using App by fastforce
moreover have "⦇t1⦈⇘ξ⇙ = ⦇t1⦈⇘ξ'⇙"
using App by fastforce
ultimately show ?case
by (simp add: den.simps(8))
next
case (Abs σ b)
let ?x = "fresh (fvs b)"
have xnb: "?x ∉ fvs b" by (rule fresh_notin) simp
have "⦇b❙⟨?x⇧f⇘σ⇙❙⟩⦈⇘ξ(?x⇘σ⇙ := d)⇙ = ⦇b❙⟨?x⇧f⇘σ⇙❙⟩⦈⇘ξ'(?x⇘σ⇙ := d)⇙" for d
by (auto intro!: Abs)
(smt (verit, best) Abs.prems Un_iff occ.simps(10,2) occ_opn prod.inject
singleton_iff subset_eq upd_def)
thus ?case by (simp only: Abs den.simps(9))
qed auto
text ‹‹α›-invariance: opening with either of two fresh free variables gives the same
denotation. This makes the fresh choice built into @{const den} irrelevant, and is the
key to the substitution-value lemma below. The abstraction case renames both internal
fresh choices to a common fresh ‹w› (inner induction hypothesis), commutes the openings
(@{thm opn_opn_comm}), then swaps the two names (outer induction hypothesis).›
lemma den_rename: "x ∉ fvs t ⟹ y ∉ fvs t ⟹ ⦇opn k (x⇧f⇘σ⇙) t⦈⇘ξ(x⇘σ⇙ := d)⇙
= ⦇opn k (y⇧f⇘σ⇙) t⦈⇘ξ(y⇘σ⇙ := d)⇙"
proof (induction t arbitrary: k ξ x y σ d rule: size_induct)
case (App s1 t1)
hence "⦇opn k (x⇧f⇘σ⇙) s1⦈⇘ξ(x⇘σ⇙ := d)⇙ = ⦇opn k (y⇧f⇘σ⇙) s1⦈⇘ξ(y⇘σ⇙ := d)⇙" and
"⦇opn k (x⇧f⇘σ⇙) t1⦈⇘ξ(x⇘σ⇙ := d)⇙ = ⦇opn k (y⇧f⇘σ⇙) t1⦈⇘ξ(y⇘σ⇙ := d)⇙"
by auto
thus ?case by (simp only: App opn.simps den.simps(8))
next
case (Abs τ c)
define w where "w = fresh (fvs c ∪ {x, y})"
have wc: "w ∉ fvs c" and wx: "w ≠ x" and wy: "w ≠ y"
using fresh_notin[of "fvs c ∪ {x, y}"] unfolding w_def by auto
have xc: "x ∉ fvs c" and yc: "y ∉ fvs c" using Abs by auto
let ?px = "fresh (fvs (opn (Suc k) (x⇧f⇘σ⇙) c))"
let ?py = "fresh (fvs (opn (Suc k) (y⇧f⇘σ⇙) c))"
have pxf: "?px ∉ fvs (opn (Suc k) (x⇧f⇘σ⇙) c)"
by (rule fresh_notin) simp
have pyf: "?py ∉ fvs (opn (Suc k) (y⇧f⇘σ⇙) c)"
by (rule fresh_notin) simp
have wnx: "w ∉ fvs (opn (Suc k) (x⇧f⇘σ⇙) c)"
using wc wx fvs_opn[of "Suc k" "x⇧f⇘σ⇙" c] by auto
have wny: "w ∉ fvs (opn (Suc k) (y⇧f⇘σ⇙) c)"
using wc wy fvs_opn[of "Suc k" "y⇧f⇘σ⇙" c] by auto
have cw: "(opn (Suc k) (z⇧f⇘σ⇙) c)❙⟨w⇧f⇘τ⇙❙⟩ = opn (Suc k) (z⇧f⇘σ⇙) (c❙⟨w⇧f⇘τ⇙❙⟩)" for z
by (rule opn_opn_comm) auto
have "⦇(opn (Suc k) (x⇧f⇘σ⇙) c)❙⟨?px⇧f⇘τ⇙❙⟩⦈⇘(ξ(x⇘σ⇙ := d))(?px⇘τ⇙ := e)⇙
= ⦇(opn (Suc k) (y⇧f⇘σ⇙) c)❙⟨?py⇧f⇘τ⇙❙⟩⦈⇘(ξ(y⇘σ⇙ := d))(?py⇘τ⇙ := e)⇙"
for e
proof -
have "⦇(opn (Suc k) (x⇧f⇘σ⇙)
c)❙⟨?px⇧f⇘τ⇙❙⟩⦈⇘(ξ(x⇘σ⇙ := d))(?px⇘τ⇙ := e)⇙
= ⦇(opn (Suc k) (x⇧f⇘σ⇙) c)❙⟨w⇧f⇘τ⇙❙⟩⦈⇘(ξ(x⇘σ⇙ := d))(w⇘τ⇙ := e)⇙"
using Abs pxf wnx by (metis nle_le size_opn_Fre)
also have "… = ⦇opn (Suc k) (x⇧f⇘σ⇙) (c❙⟨w⇧f⇘τ⇙❙⟩)⦈⇘(ξ(w⇘τ⇙ := e))(x⇘σ⇙ := d)⇙"
using wx by (simp add: cw upd_comm)
also have "… = ⦇opn (Suc k) (y⇧f⇘σ⇙) (c❙⟨w⇧f⇘τ⇙❙⟩)⦈⇘(ξ(w⇘τ⇙ := e))(y⇘σ⇙ := d)⇙"
using Abs xc yc wc wx wy fvs_opn[of 0 "w⇧f⇘τ⇙" c]
by (smt (verit, best) Un_insert_right dual_order.refl fvs.simps(2) insertE size_opn_Fre
subset_eq sup_bot.right_neutral)
also have "… = ⦇(opn (Suc k) (y⇧f⇘σ⇙) c)❙⟨w⇧f⇘τ⇙❙⟩⦈⇘(ξ(y⇘σ⇙ := d))(w⇘τ⇙ := e)⇙"
using wy by (simp add: cw upd_comm)
also have "… = ⦇(opn (Suc k) (y⇧f⇘σ⇙) c)❙⟨?py⇧f⇘τ⇙❙⟩⦈⇘(ξ(y⇘σ⇙ := d))(?py⇘τ⇙ := e)⇙"
using Abs pyf wny by (metis order_refl size_opn_Fre)
finally show ?thesis.
qed
thus ?case using Abs by (simp add: den.simps(9))
qed(auto simp: upd_def)
text ‹Any sufficiently fresh variable may be used to compute an abstraction's denotation.›
lemma den_Abs: "x ∉ fvs b ⟹ ⦇❙Λ⇘σ⇙ b⦈⇘ξ⇙ = Lm σ (λd. ⦇b❙⟨x⇧f⇘σ⇙❙⟩⦈⇘ξ(x⇘σ⇙ := d)⇙)"
by (metis (no_types, lifting) ext den.simps(9) finite_fvs frame_sig.den_rename fresh_notin)
text ‹The substitution-value lemma (BKK Lemma 3.20).›
lemma den_fsub: "lc u ⟹ ⦇fsub x σ u t⦈⇘ξ⇙ = ⦇t⦈⇘ξ(x⇘σ⇙ := ⦇u⦈⇘ξ⇙)⇙"
proof (induction t arbitrary: ξ rule: size_induct)
case (Fre n ρ) thus ?case by (auto simp: upd_def)
next
case (App s1 t1)
have "⦇fsub x σ u s1⦈⇘ξ⇙ = ⦇s1⦈⇘ξ(x⇘σ⇙ := ⦇u⦈⇘ξ⇙)⇙" and
"⦇fsub x σ u t1⦈⇘ξ⇙ = ⦇t1⦈⇘ξ(x⇘σ⇙ := ⦇u⦈⇘ξ⇙)⇙"
using App by auto
thus ?case by (simp only: App fsub.simps den.simps(8))
next
case (Abs τ b)
define w where "w = fresh (fvs b ∪ fvs u ∪ {x})"
have wb: "w ∉ fvs b" and wu: "w ∉ fvs u" and wx: "w ≠ x"
using fresh_notin[of "fvs b ∪ fvs u ∪ {x}"] unfolding w_def by auto
have wfsb: "w ∉ fvs (fsub x σ u b)"
using wb wu fvs_fsub[of x σ u b] by auto
have "⦇fsub x σ u (❙Λ⇘τ⇙ b)⦈⇘ξ⇙ = Lm τ (λd. ⦇(fsub x σ u
b)❙⟨w⇧f⇘τ⇙❙⟩⦈⇘ξ(w⇘τ⇙ := d)⇙)"
by (simp only: fsub.simps den_Abs[OF wfsb])
also have "… = Lm τ (λd. ⦇fsub x σ u (b❙⟨w⇧f⇘τ⇙❙⟩)⦈⇘ξ(w⇘τ⇙ := d)⇙)"
using Abs wx by (simp add: fsub_opn)
also have "… = Lm τ (λd. ⦇b❙⟨w⇧f⇘τ⇙❙⟩⦈⇘(ξ(w⇘τ⇙ := d))(x⇘σ⇙ := ⦇u⦈⇘ξ(w⇘τ⇙ := d)⇙)⇙)"
using Abs by auto
also have "… = Lm τ (λd. ⦇b❙⟨w⇧f⇘τ⇙❙⟩⦈⇘(ξ(x⇘σ⇙ := ⦇u⦈⇘ξ⇙))(w⇘τ⇙ := d)⇙)"
proof (rule arg_cong[where f = "Lm τ"], rule ext)
fix d
have "⦇u⦈⇘ξ(w⇘τ⇙ := d)⇙ = ⦇u⦈⇘ξ⇙"
using den_coincidence wu fvs_eq_fst_occ
by (smt (verit, ccfv_threshold) fst_conv image_eqI upd_def)
thus "⦇b❙⟨w⇧f⇘τ⇙❙⟩⦈⇘(ξ(w⇘τ⇙ := d))(x⇘σ⇙ := ⦇u⦈⇘ξ(w⇘τ⇙ := d)⇙)⇙
= ⦇b❙⟨w⇧f⇘τ⇙❙⟩⦈⇘(ξ(x⇘σ⇙ := ⦇u⦈⇘ξ⇙))(w⇘τ⇙ := d)⇙"
using wx by (simp add: upd_comm)
qed
also have "… = ⦇❙Λ⇘τ⇙ b⦈⇘ξ(x⇘σ⇙ := ⦇u⦈⇘ξ⇙)⇙"
by (rule den_Abs[OF wb, symmetric])
finally show ?case unfolding Abs .
qed auto
text ‹The ‹β› form of the substitution-value lemma (BKK Lemma 3.20): opening an
abstraction body with a (locally closed) argument ‹u› is computed by evaluating the
body under the assignment updated with the denotation of ‹u›. This is the semantic
counterpart of ‹β›-reduction and the workhorse of soundness.›
lemma den_beta: assumes u: "lc u" and x: "x ∉ fvs b"
shows "⦇b❙⟨u❙⟩⦈⇘ξ⇙ = ⦇b❙⟨x⇧f⇘σ⇙❙⟩⦈⇘ξ(x⇘σ⇙ := ⦇u⦈⇘ξ⇙)⇙"
by (metis den_fsub fsub_intro u x)
end
text ‹Satisfaction of the connectives (the ‹Σ›-valuation conditions of BKK
Definition 3.41 and Figure 2; for the @{emph ‹defined›} connectives cf.\ BKK
Remark 3.47 and Lemma 3.48): model-theoretic facts, stated here so that the
calculus can use them for soundness.›
context sigma_model
begin
lemma sat_Neg: assumes "wff⇘𝗈⇙(A)" and "asg ξ"
shows "vl (Ee ξ (❙¬ A)) ⟷ ¬ vl (Ee ξ A)"
using ev_app wff_Neg assms vl_neg ev_type by metis
lemma sat_Dis: assumes "wff⇘𝗈⇙(A)" and "wff⇘𝗈⇙(B)" and "asg ξ"
shows "vl (Ee ξ (A ❙∨ B)) ⟷ vl (Ee ξ A) ∨ vl (Ee ξ B)"
using ev_app wff_App wff_Dis assms vl_dis ev_type by (smt (verit, ccfv_SIG))
lemma sat_ImpB: assumes "wff⇘𝗈⇙(A)" and "wff⇘𝗈⇙(B)" and "asg ξ"
shows "vl (Ee ξ (A ❙⊃ B)) ⟷ (vl (Ee ξ A) ⟶ vl (Ee ξ B))"
unfolding ImpB_def using sat_Dis wff_Not assms sat_Neg by auto
lemma sat_Pi: assumes "wff⇘σ❙⇒𝗈⇙(G)" and "asg ξ"
shows "vl (Ee ξ (Pi σ ❙⋅ G)) ⟷ (∀d. Dm σ d ⟶ vl (Ap (Ee ξ G) d))"
using ev_app wff_Pi assms vl_pi ev_type by metis
lemma sat_Forall: assumes wA: "wff⇘σ❙⇒𝗈⇙(❙Λ⇘σ⇙ b)" and x: "x ∉ fvs b" and xi: "asg ξ"
shows "vl (Ee ξ (❙Π⇘σ⇙ b)) ⟷ (∀d. Dm σ d ⟶ vl (Ee (ξ(x⇘σ⇙ := d)) (b❙⟨x⇧f⇘σ⇙❙⟩)))"
unfolding Forall_def using sat_Pi wA xi ev_abs_app x by auto
text ‹Satisfaction of Leibniz equality (BKK Lemma 4.2): in a ‹Σ›-model with primitive
equality, Leibniz equality holds exactly at identical denotations.›
lemma sat_Leib: assumes wA: "wff⇘α⇙(A)" and wB: "wff⇘α⇙(B)" and xi: "asg ξ"
shows "vl (Ee ξ (A ❙≐⇘α⇙ B)) ⟷ Ee ξ A = Ee ξ B"
proof -
have lcA: "lc A" and lcB: "lc B" using wA wB by (auto intro: wff_lc)
define p where "p = fresh (fvs A ∪ fvs B)"
have p: "p ∉ fvs A" "p ∉ fvs B"
unfolding p_def using fresh_notin[of "fvs A ∪ fvs B"] by auto
let ?b = "(Bnd 0 ❙⋅ A) ❙⊃ (Bnd 0 ❙⋅ B)"
have wI: "wff⇘(α❙⇒𝗈)❙⇒𝗈⇙(❙Λ⇘α❙⇒𝗈⇙ ?b)"
by (smt (verit, del_insts) ImpB_def lcA lcB opn.simps(1,4,5,9) opn_lc wA wB
wff_AbsI wff_App wff_Fre wff_ImpB)
have pf: "p ∉ fvs ?b" using p by (auto simp: ImpB_def)
have unf: "vl (Ee ξ (A ❙≐⇘α⇙ B)) ⟷ (∀r. Dm (α ❙⇒ 𝗈) r
⟶ (vl (Ap r (Ee ξ A)) ⟶ vl (Ap r (Ee ξ B))))"
proof -
have "vl (Ee (ξ(p⇘α ❙⇒ 𝗈⇙ := r)) (?b❙⟨p⇧f⇘α ❙⇒ 𝗈⇙❙⟩))
⟷ (vl (Ap r (Ee ξ A)) ⟶ vl (Ap r (Ee ξ B)))"
if r: "Dm (α ❙⇒ 𝗈) r" for r
proof -
let ?ξ = "ξ(p⇘α ❙⇒ 𝗈⇙ := r)"
have ob: "?b❙⟨p⇧f⇘α ❙⇒ 𝗈⇙❙⟩ = (p⇧f⇘α ❙⇒ 𝗈⇙ ❙⋅ A) ❙⊃ (p⇧f⇘α ❙⇒ 𝗈⇙ ❙⋅ B)"
by (simp add: opn_lc[OF lcA] opn_lc[OF lcB])
have cA: "Ee ?ξ A = Ee ξ A"
using p ev_coin[OF wA asg_upd[OF xi r] xi]
unfolding upd_def fvs_eq_fst_occ image_iff by force
have cB: "Ee ?ξ B = Ee ξ B"
using p ev_coin[OF wB asg_upd[OF xi r] xi]
unfolding upd_def fvs_eq_fst_occ image_iff by force
show ?thesis unfolding ob
by (smt (verit, del_insts) asg_upd cA cB ev_app ev_var sat_ImpB that upd_same wA wB
wff_App wff_AppE wff_App_FreFre wff_FreE xi)
qed
thus ?thesis
unfolding ev_beta[OF Leib_beq[OF wA wB] xi] sat_Forall[OF wI pf xi]
by blast
qed
show ?thesis
proof
assume L: "vl (Ee ξ (A ❙≐⇘α⇙ B))"
let ?r = "Ap (Ee ξ (Eq α)) (Ee ξ A)"
have rA: "vl (Ap ?r (Ee ξ A))"
using vl_eq[OF xi ev_type[OF wA xi] ev_type[OF wA xi]] by simp
have "vl (Ap ?r (Ee ξ B))"
using unf L as_appTy[OF ev_type[OF wff_Eq xi] ev_type[OF wA xi]] rA by blast
thus "Ee ξ A = Ee ξ B"
using vl_eq[OF xi ev_type[OF wA xi] ev_type[OF wB xi]] by simp
qed(simp add: unf)
qed
end
subsection ‹‹Σ›-Henkin models: the general-model locale (BKK Definition 3.50)›
text ‹BKK's soundness and completeness theorems (BKK Theorem 7.3, Corollary 7.7) cover all
eight model classes ‹ℳ⇩*›; we instantiate the most specialised one, the
class ‹ℳ⇘βfb⇙› of @{emph ‹‹Σ›-Henkin models›} (BKK Definition 3.50): ‹Σ›-models (BKK
Definition 3.41) satisfying property b, property f (functionality), and property q (BKK
Definitions 3.46 and 3.49). Crucially the function domains need not be full (BKK
Definition 3.5): following Henkin --- in BKK's words, it is sufficient to require that ‹𝒟⇘α❙⇒β⇙›
``has enough members that any well-formed formula can be evaluated'' (BKK
Section 2.3.1). We therefore require the ‹λ›-conditions --- ‹λ›-comprehension ‹gm_lamTy› and
the ‹β›-condition ‹gm_beta› of the ‹Σ›-evaluation (BKK Definition 3.18) --- only for the
functions that are @{emph ‹denotations of ‹λ›-terms›}, so that every wff denotes.
A term model need not be full: with property b the domain ‹𝒟⇘ι❙⇒𝗈⇙› of a full frame over
infinite ‹𝒟⇘ι⇙› would be uncountable, whereas the term model over a countable signature
is countable.
(BKK avoid Andrews' term @{emph ‹general models›} for this notion; we keep it in the locale name
‹general_model›, in Andrews' sense.) Standard models --- the full case, BKK
Definition 3.51 --- appear at the end of this section as a sublocale. Beyond BKK, the locale
carries the description condition ‹gm_descB› for the typed description operators ‹Iota σ›
(Andrews 1972, BKK's reference [3]), matched by the rule ‹NK(ι)› of the calculus.
Note that we render the applicative structure abstractly (an application operation ‹❙@› on a
carrier ‹'u›) rather than literally over a frame of functions (BKK Definition 3.4); by
functionality and BKK Theorem 3.68 the two presentations describe the same class of models
up to isomorphism.›
locale general_model = frame_sig +
assumes gm_TF: "Tv ≠ Fv" and gm_boolean: "𝒟⇘𝗈⇙ a ⟷ a = Tv ∨ a = Fv"
and gm_appTy: "⟦𝒟⇘σ❙⇒τ⇙ f; 𝒟⇘σ⇙ a⟧ ⟹ 𝒟⇘τ⇙ (f ❙@ a)"
and gm_negTy: "𝒟⇘𝗈❙⇒𝗈⇙ Ngv" and gm_disTy: "𝒟⇘𝗈❙⇒𝗈❙⇒𝗈⇙ Dsv"
and gm_piTy: "𝒟⇘(σ❙⇒𝗈)❙⇒𝗈⇙ (Piv σ)"
and gm_iotaTy: "𝒟⇘(σ❙⇒𝗈)❙⇒σ⇙ (Iv σ)" and gm_parTy: "𝒟⇘σ⇙ (Jv p σ)"
and gm_negB: "𝒟⇘𝗈⇙ a ⟹ (Ngv ❙@ a = Tv) = (a ≠ Tv)"
and gm_disB: "⟦𝒟⇘𝗈⇙ a; 𝒟⇘𝗈⇙ b⟧ ⟹ (Dsv ❙@ a ❙@ b = Tv) = (a = Tv ∨ b = Tv)"
and gm_piB: "𝒟⇘σ❙⇒𝗈⇙ f ⟹ (Piv σ ❙@ f = Tv) = (∀d. 𝒟⇘σ⇙ d ⟶ f ❙@ d = Tv)"
and gm_funct: "⟦𝒟⇘σ❙⇒τ⇙ g; 𝒟⇘σ❙⇒τ⇙ k; ⋀a. 𝒟⇘σ⇙ a ⟹ g ❙@ a = k ❙@ a⟧ ⟹ g = k"
and gm_eqTy: "𝒟⇘σ❙⇒σ❙⇒𝗈⇙ (Ev σ)"
and gm_eqB: "⟦𝒟⇘σ⇙ a; 𝒟⇘σ⇙ b⟧ ⟹ (Ev σ ❙@ a ❙@ b = Tv) = (a = b)"
and gm_descB: "⟦𝒟⇘σ❙⇒𝗈⇙ f; 𝒟⇘σ⇙ a; ∀b. 𝒟⇘σ⇙ b ⟶ (f ❙@ b = Tv) = (b = a)⟧ ⟹ Iv σ ❙@ f = a"
and gm_lamTy: "⟦wff⇘σ❙⇒τ⇙(❙Λ⇘σ⇙ bd); ∀n ρ. 𝒟⇘ρ⇙ (ξ n ρ)⟧ ⟹ 𝒟⇘σ❙⇒τ⇙ (⦇❙Λ⇘σ⇙ bd⦈⇘ξ⇙)"
and gm_beta: "⟦wff⇘τ⇙(bd❙⟨x⇧f⇘σ⇙❙⟩); x ∉ fvs bd; ∀n ρ. 𝒟⇘ρ⇙ (ξ n ρ); 𝒟⇘σ⇙ a⟧
⟹ ⦇❙Λ⇘σ⇙ bd⦈⇘ξ⇙ ❙@ a = ⦇bd❙⟨x⇧f⇘σ⇙❙⟩⦈⇘ξ(x⇘σ⇙ := a)⇙"
begin
text ‹Every domain is inhabited (part of BKK Definition 3.1) --- not an axiom: the parameter
interpretation ‹Jv› already inhabits every domain.›
lemma gm_nonempty: "∃d. 𝒟⇘σ⇙ d" using gm_parTy by blast
text ‹An assignment is @{emph ‹type-respecting›} (@{term resp}) if it maps every typed variable
into the matching domain --- BKK's assignment @{emph ‹into›} the structure.›
definition resp where "resp ξ ≡ ∀n τ. 𝒟⇘τ⇙ (ξ n τ)"
lemma Tv_dom [simp]: "𝒟⇘𝗈⇙ Tv" and Fv_dom [simp]: "𝒟⇘𝗈⇙ Fv"
using gm_boolean by auto
text ‹Every well-formed term denotes in the domain of its type (BKK Definition 3.18): the
‹λ›-comprehension condition ‹gm_lamTy› is exactly what makes the abstraction case go through.›
lemma den_dom: "wff⇘σ⇙(t) ⟹ resp ξ ⟹ 𝒟⇘σ⇙ (⦇t⦈⇘ξ⇙)"
proof (induction arbitrary: ξ rule: wff.induct)
case wff_App thus ?case using den.simps(8) gm_appTy by fastforce
next
case wff_Abs thus ?case using gm_lamTy resp_def wff.wff_Abs by blast
qed(auto simp: resp_def gm_parTy gm_negTy gm_disTy gm_piTy gm_iotaTy gm_eqTy)
text ‹The semantic ‹β› rule at the term level (BKK Remark 3.19): applying an abstraction to a
well-formed argument evaluates the opened body.›
lemma den_App_Abs:
assumes wb: "wff⇘σ❙⇒τ⇙(❙Λ⇘σ⇙ b)" and wa: "wff⇘σ⇙(a)" and r: "resp ξ"
shows "⦇(❙Λ⇘σ⇙ b) ❙⋅ a⦈⇘ξ⇙ = ⦇b❙⟨a❙⟩⦈⇘ξ⇙"
proof -
define x where "x = fresh (fvs b)"
have xb: "x ∉ fvs b"
using fresh_notin unfolding x_def by simp
have da: "𝒟⇘σ⇙ (⦇a⦈⇘ξ⇙)" using wa r by (rule den_dom)
have "⦇(❙Λ⇘σ⇙ b) ❙⋅ a⦈⇘ξ⇙ = ⦇❙Λ⇘σ⇙ b⦈⇘ξ⇙ ❙@ ⦇a⦈⇘ξ⇙" by (simp add: den.simps(8))
also have "… = ⦇b❙⟨x⇧f⇘σ⇙❙⟩⦈⇘ξ(x⇘σ⇙ := ⦇a⦈⇘ξ⇙)⇙"
using da gm_beta r resp_def wff_Abs_open wb xb by blast
also have "… = ⦇b❙⟨a❙⟩⦈⇘ξ⇙" using den_beta wff_lc wa xb by metis
finally show ?thesis.
qed
text ‹‹β›-convertible terms denote the same object under any domain-respecting assignment
(BKK Remark 3.19); the abstraction-congruence case uses functionality (property f).›
lemma beq_den: "s ≈⇘ρ⇙ t ⟹ ∀n τ. 𝒟⇘τ⇙ (ξ n τ) ⟹ ⦇s⦈⇘ξ⇙ = ⦇t⦈⇘ξ⇙"
proof (induction arbitrary: ξ rule: beq.induct)
case beta thus ?case using den_App_Abs resp_def by blast
next
case (abs L b σ τ b')
define x where "x = fresh (L ∪ fvs b ∪ fvs b')"
have xL: "x ∉ L" and xb: "x ∉ fvs b" and xb': "x ∉ fvs b'"
using fresh_notin[of "L ∪ fvs b ∪ fvs b'"] abs unfolding x_def by auto
have wb: "wff⇘τ⇙(b❙⟨x⇧f⇘σ⇙❙⟩)" and wb': "wff⇘τ⇙(b'❙⟨x⇧f⇘σ⇙❙⟩)"
using beq_wffL beq_wffR abs xL by blast+
{
fix a
assume a: "𝒟⇘σ⇙ a"
hence tot: "∀n γ. 𝒟⇘γ⇙ (ξ(x⇘σ⇙ := a) n γ)"
using abs.prems by (auto simp: upd_def)
have "⦇❙Λ⇘σ⇙ b⦈⇘ξ⇙ ❙@ a = ⦇b❙⟨x⇧f⇘σ⇙❙⟩⦈⇘ξ(x⇘σ⇙ := a)⇙"
by (rule gm_beta[OF wb xb abs.prems a])
also have "… = ⦇b'❙⟨x⇧f⇘σ⇙❙⟩⦈⇘ξ(x⇘σ⇙ := a)⇙"
using abs.IH[OF xL, of "ξ(x⇘σ⇙ := a)"] tot by blast
also have "… = ⦇❙Λ⇘σ⇙ b'⦈⇘ξ⇙ ❙@ a"
using gm_beta wb' xb' abs.prems a by simp
finally have "⦇❙Λ⇘σ⇙ b⦈⇘ξ⇙ ❙@ a = ⦇❙Λ⇘σ⇙ b'⦈⇘ξ⇙ ❙@ a".
}
thus ?case
using gm_funct gm_lamTy wff_Abs_open_rev wb xb abs.prems wb' xb' by blast
qed(auto simp: den.simps(8))
end
text ‹Every ‹Σ›-Henkin general model --- the frame-based canonical construction --- is a
BKK model: take ‹E := den› and ‹υ := (λa. a = Tv)›. The four evaluation conditions are
the denotation lemmas, and the ‹L›-properties are the ‹gm›-conditions.›
sublocale general_model ⊆ bkkA: app_struct Dm Ap
by unfold_locales (use gm_nonempty gm_appTy in blast)+
sublocale general_model ⊆ bkk: bkk_model Dm Ap "λξ A. ⦇A⦈⇘ξ⇙" "λa. a = Tv"
by (unfold_locales;
auto simp: bkkA.functional_def general_model_axioms[unfolded general_model_def]
bkkA.asg_def frame_sig.den.simps(8) resp_def
intro: beq_den den_coincidence den_dom)
text ‹Reusable satisfaction facts for the defined connectives and the named binders,
holding in @{emph ‹any›} ‹Σ›-Henkin general model: they peel ‹❙Πx⇘σ⇙.›, ‹❙∃x⇘σ⇙.› and
the connectives down to the underlying domains, reducing satisfaction of a closed
formula to a first-order statement about the carrier's domains --- the model-side
counterparts of the syntactic derived rules in ‹Calculus›.›
context general_model
begin
lemma sat_NegB:
assumes "wff⇘𝗈⇙(A)" and "bkkA.asg ξ"
shows "(⦇❙¬ A⦈⇘ξ⇙ = Tv) ⟷ ¬ (⦇A⦈⇘ξ⇙ = Tv)"
using bkk.sat_Neg[OF assms] by simp
lemma sat_DisB:
assumes "wff⇘𝗈⇙(A)" and "wff⇘𝗈⇙(B)" and "bkkA.asg ξ"
shows "(⦇A ❙∨ B⦈⇘ξ⇙ = Tv) ⟷ (⦇A⦈⇘ξ⇙ = Tv) ∨ (⦇B⦈⇘ξ⇙ = Tv)"
using bkk.sat_Dis[OF assms] by simp
lemma sat_ImpBB:
assumes "wff⇘𝗈⇙(A)" and "wff⇘𝗈⇙(B)" and "bkkA.asg ξ"
shows "(⦇A ❙⊃ B⦈⇘ξ⇙ = Tv) ⟷ ((⦇A⦈⇘ξ⇙ = Tv) ⟶ (⦇B⦈⇘ξ⇙ = Tv))"
using bkk.sat_ImpB[OF assms] by simp
lemma sat_AndB:
assumes "wff⇘𝗈⇙(A)" and "wff⇘𝗈⇙(B)" and "bkkA.asg ξ"
shows "(⦇A ❙∧ B⦈⇘ξ⇙ = Tv) ⟷ (⦇A⦈⇘ξ⇙ = Tv) ∧ (⦇B⦈⇘ξ⇙ = Tv)"
unfolding AndB_def
using sat_NegB[OF wff_Or[OF wff_Not[OF assms(1)] wff_Not[OF assms(2)]] assms(3)]
sat_DisB[OF wff_Not[OF assms(1)] wff_Not[OF assms(2)] assms(3)]
sat_NegB[OF assms(1) assms(3)] sat_NegB[OF assms(2) assms(3)]
by blast
lemma sat_PEqB:
assumes wa: "wff⇘σ⇙(A)" and wb: "wff⇘σ⇙(B)" and xi: "bkkA.asg ξ"
shows "(⦇A ❙=⇘σ⇙ B⦈⇘ξ⇙ = Tv) ⟷ (⦇A⦈⇘ξ⇙ = ⦇B⦈⇘ξ⇙)"
proof -
have dA: "𝒟⇘σ⇙ (⦇A⦈⇘ξ⇙)" using bkk.ev_type[OF wa xi] by simp
have dB: "𝒟⇘σ⇙ (⦇B⦈⇘ξ⇙)" using bkk.ev_type[OF wb xi] by simp
have "⦇A ❙=⇘σ⇙ B⦈⇘ξ⇙ = (Ev σ) ❙@ (⦇A⦈⇘ξ⇙) ❙@ (⦇B⦈⇘ξ⇙)"
by (simp add: den.simps(8))
thus ?thesis using bkk.vl_eq[OF xi dA dB] by simp
qed
text ‹Peeling a defined quantifier down to the carrier.›
lemma sat_AllN:
assumes wb: "wff⇘𝗈⇙(b)" and xi: "bkkA.asg ξ"
shows "(⦇❙Πv⇘σ⇙. b⦈⇘ξ⇙ = Tv) ⟷ (∀d. 𝒟⇘σ⇙ d ⟶ ⦇b⦈⇘ξ(v⇘σ⇙ := d)⇙ = Tv)"
proof -
note lcb = wff_lc[OF wb]
define x where "x = fresh (fvs b)"
have xnb: "x ∉ fvs b" unfolding x_def by (rule fresh_notin[OF finite_fvs])
have wf: "wff⇘σ ❙⇒ 𝗈⇙(❙Λ⇘σ⇙ (clos 0 v σ b))" by (rule wff_LamN_clos[OF wb])
have xnc: "x ∉ fvs (clos 0 v σ b)" using xnb fvs_clos[of 0 v σ b] by blast
have sub: "(clos 0 v σ b)❙⟨x⇧f⇘σ⇙❙⟩ = fsub v σ (x⇧f⇘σ⇙) b"
by (rule opn_clos_sub[OF opn_lc[OF lcb]])
have ev: "⦇(clos 0 v σ b)❙⟨x⇧f⇘σ⇙❙⟩⦈⇘ξ(x⇘σ⇙ := d)⇙ = ⦇b⦈⇘ξ(v⇘σ⇙ := d)⇙" for d
proof -
have "⦇(clos 0 v σ b)❙⟨x⇧f⇘σ⇙❙⟩⦈⇘ξ(x⇘σ⇙ := d)⇙
= ⦇b⦈⇘(ξ(x⇘σ⇙ := d))(v⇘σ⇙ := ⦇x⇧f⇘σ⇙⦈⇘ξ(x⇘σ⇙ := d)⇙)⇙"
by (simp only: sub den_fsub[OF lc_Fre])
also have "… = ⦇b⦈⇘(ξ(x⇘σ⇙ := d))(v⇘σ⇙ := d)⇙" by simp
also have "… = ⦇b⦈⇘ξ(v⇘σ⇙ := d)⇙"
proof (rule den_coincidence)
fix n τ assume o: "(n, τ) ∈ occ b"
show "((ξ(x⇘σ⇙ := d))(v⇘σ⇙ := d)) n τ = (ξ(v⇘σ⇙ := d)) n τ"
proof (cases "n = x ∧ τ = σ")
case True thus ?thesis using o xnb by (auto simp: fvs_eq_fst_occ image_iff)
next
case False thus ?thesis by (auto simp: upd_def)
qed
qed
finally show ?thesis .
qed
have "(⦇❙Πv⇘σ⇙. b⦈⇘ξ⇙ = Tv)
= (∀d. 𝒟⇘σ⇙ d ⟶ ⦇(clos 0 v σ b)❙⟨x⇧f⇘σ⇙❙⟩⦈⇘ξ(x⇘σ⇙ := d)⇙ = Tv)"
unfolding AllN_def using bkk.sat_Forall[OF wf xnc xi] by simp
thus ?thesis using ev by simp
qed
lemma sat_ExN:
assumes wb: "wff⇘𝗈⇙(b)" and xi: "bkkA.asg ξ"
shows "(⦇❙∃v⇘σ⇙. b⦈⇘ξ⇙ = Tv) ⟷ (∃d. 𝒟⇘σ⇙ d ∧ ⦇b⦈⇘ξ(v⇘σ⇙ := d)⇙ = Tv)"
proof -
have e: "(❙∃v⇘σ⇙. b) = ❙¬ (❙Πv⇘σ⇙. (❙¬ b))"
by (simp add: ExN_def AllN_def)
have wnb: "wff⇘𝗈⇙(❙¬ b)" using wb by (rule wff_Not)
have wAll: "wff⇘𝗈⇙(❙Πv⇘σ⇙. (❙¬ b))" by (rule wff_AllN[OF wnb])
have negd: "(⦇❙¬ b⦈⇘ξ(v⇘σ⇙ := d)⇙ = Tv) = (¬ (⦇b⦈⇘ξ(v⇘σ⇙ := d)⇙ = Tv))"
if "𝒟⇘σ⇙ d" for d
using sat_NegB[OF wb bkkA.asg_upd[OF xi that]] .
have "(⦇❙∃v⇘σ⇙. b⦈⇘ξ⇙ = Tv) = (¬ (⦇❙Πv⇘σ⇙. (❙¬ b)⦈⇘ξ⇙ = Tv))"
unfolding e using sat_NegB[OF wAll xi] by simp
also have "… = (¬ (∀d. 𝒟⇘σ⇙ d ⟶ ⦇❙¬ b⦈⇘ξ(v⇘σ⇙ := d)⇙ = Tv))"
using sat_AllN[OF wnb xi] by simp
also have "… = (∃d. 𝒟⇘σ⇙ d ∧ ⦇b⦈⇘ξ(v⇘σ⇙ := d)⇙ = Tv)"
using negd by blast
finally show ?thesis .
qed
end
subsection ‹Substitution-value laws›
text ‹The substitution-value law for abstract ‹Σ›-evaluations (BKK Lemma 3.20 for a
single free variable): substituting @{emph ‹any›} well-formed term equals updating
the assignment with its value.›
context sigma_eval
begin
lemma ev_fsub_one:
assumes wA: "wff⇘τ⇙(A)" and wu: "wff⇘σ⇙(u)" and xi: "asg ξ"
shows "Ee ξ (fsub x σ u A) = Ee (ξ(x⇘σ⇙ := Ee ξ u)) A"
proof -
have opnA: "opn 0 v A = A" for v by (simp add: wff_lc[OF wA])
let ?B = "clos 0 x σ A"
have wAbs: "wff⇘σ❙⇒τ⇙(❙Λ⇘σ⇙ ?B)"
by (rule wff_AbsI) (simp add: opn_clos_sub[OF opnA] wff_fsub[OF wA
wff_Fre])
have du: "Dm σ (Ee ξ u)" by (rule ev_type[OF wu xi])
have "Ee ξ (fsub x σ u A) = Ee ξ ((❙Λ⇘σ⇙ ?B) ❙⋅ u)"
unfolding opn_clos_sub[OF opnA, symmetric]
by (rule ev_beta[OF beq.sym[OF beq.beta[OF wAbs wu]] xi])
also have "… = Ap (Ee ξ (❙Λ⇘σ⇙ ?B)) (Ee ξ u)"
by (rule ev_app[OF wAbs wu xi])
also have "… = Ee (ξ(x⇘σ⇙ := Ee ξ u)) (?B❙⟨x⇧f⇘σ⇙❙⟩)"
by (rule ev_abs_app_occ[OF wAbs xi occ_clos du])
also have "?B❙⟨x⇧f⇘σ⇙❙⟩ = A"
by (simp add: opn_clos_sub[OF opnA] fsub_id)
finally show ?thesis .
qed
text ‹The @{emph ‹simultaneous›} substitution-value law (the simultaneous form of BKK
Lemma 3.20), for replacements that are closed wherever they act: evaluating
‹msub ρ A› equals evaluating ‹A› under the assignment that sends each variable to the
value of its replacement.›
lemma asg_msub:
assumes xi: "asg ξ" and wr: "⋀n τ'. wff⇘τ'⇙(ρ n τ')"
shows "asg (λn τ'. Ee ξ (ρ n τ'))"
using ev_type[OF wr xi] by (auto simp: asg_def)
lemma ev_msub_aux:
shows "card {q ∈ occ A. ρ (fst q) (snd q) ≠ (fst q)⇧f⇘snd q⇙} ≤ m ⟹
wff⇘τ⇙(A) ⟹ asg ξ ⟹ (⋀n τ'. wff⇘τ'⇙(ρ n τ')) ⟹
(⋀n τ'. ρ n τ' ≠ n⇧f⇘τ'⇙ ⟹ fvs (ρ n τ') = {}) ⟹
Ee ξ (msub ρ A) = Ee (λn τ'. Ee ξ (ρ n τ')) A"
proof (induction m arbitrary: A ρ)
case (0 A ρ)
have fin: "finite {q ∈ occ A. ρ (fst q) (snd q) ≠ (fst q)⇧f⇘snd q⇙}"
by (rule finite_subset[OF _ finite_occ]) auto
hence e: "{q ∈ occ A. ρ (fst q) (snd q) ≠ (fst q)⇧f⇘snd q⇙} = {}"
using 0(1) by simp
have idA: "msub ρ A = A"
by (subst msub_cong[where ρ' = "λn τ'. n⇧f⇘τ'⇙"]) (use e in ‹auto simp: msub_id›)
have "Ee ξ A = Ee (λn τ'. Ee ξ (ρ n τ')) A"
by (rule ev_coin[OF 0(2) 0(3) asg_msub[OF 0(3) 0(4)]])
(use e ev_var[OF 0(3)] in fastforce)
thus ?case by (simp add: idA)
next
case (Suc m A ρ)
show ?case
proof (cases "{q ∈ occ A. ρ (fst q) (snd q) ≠ (fst q)⇧f⇘snd q⇙} = {}")
case True
have idA: "msub ρ A = A"
by (subst msub_cong[where ρ' = "λn τ'. n⇧f⇘τ'⇙"]) (use True in ‹auto simp: msub_id›)
have "Ee ξ A = Ee (λn τ'. Ee ξ (ρ n τ')) A"
by (rule ev_coin[OF Suc.prems(2) Suc.prems(3) asg_msub[OF Suc.prems(3) Suc.prems(4)]])
(use True ev_var[OF Suc.prems(3)] in fastforce)
thus ?thesis by (simp add: idA)
next
case False
then obtain x σ where xs: "(x, σ) ∈ occ A" and ne: "ρ x σ ≠ x⇧f⇘σ⇙" by auto
have cl: "fvs (ρ x σ) = {}" by (rule Suc.prems(5)[OF ne])
have occu: "occ (ρ x σ) = {}" using cl by (simp add: fvs_eq_fst_occ)
define A1 where "A1 = fsub x σ (ρ x σ) A"
define ρ1 where "ρ1 = (λn τ'. if n = x ∧ τ' = σ then n⇧f⇘τ'⇙ else ρ n τ')"
have wA1: "wff⇘τ⇙(A1)" unfolding A1_def by (rule wff_fsub[OF Suc.prems(2) Suc.prems(4)])
have wr1: "wff⇘τ'⇙(ρ1 n τ')" for n τ'
unfolding ρ1_def using Suc.prems(4) by (auto intro: wff_Fre)
have cr1: "ρ1 n τ' ≠ n⇧f⇘τ'⇙ ⟹ fvs (ρ1 n τ') = {}" for n τ'
unfolding ρ1_def using Suc.prems(5) by (auto split: if_splits)
have step: "msub ρ A = msub ρ1 A1"
unfolding A1_def ρ1_def by (rule msub_step[of ρ x σ]) (rule cl)
have occA1: "occ A1 = occ A - {(x, σ)}"
unfolding A1_def by (rule occ_fsub_closed[OF occu])
have card1: "card {q ∈ occ A1. ρ1 (fst q) (snd q) ≠ (fst q)⇧f⇘snd q⇙} ≤ m"
proof -
let ?S = "{q ∈ occ A. ρ (fst q) (snd q) ≠ (fst q)⇧f⇘snd q⇙}"
have finS: "finite ?S" by (rule finite_subset[OF _ finite_occ]) auto
have mem: "(x, σ) ∈ ?S" using xs ne by simp
have sub: "{q ∈ occ A1. ρ1 (fst q) (snd q) ≠ (fst q)⇧f⇘snd q⇙} ⊆ ?S - {(x, σ)}"
unfolding occA1 ρ1_def by (auto split: if_splits)
have "card {q ∈ occ A1. ρ1 (fst q) (snd q) ≠ (fst q)⇧f⇘snd q⇙}
≤ card (?S - {(x, σ)})"
by (rule card_mono[OF finite_Diff[OF finS] sub])
also have "… = card ?S - 1" by (rule card_Diff_singleton[OF mem])
also have "… ≤ m" using Suc.prems(1) by simp
finally show ?thesis .
qed
have a1: "asg (λn τ'. Ee ξ (ρ1 n τ'))" by (rule asg_msub[OF Suc.prems(3) wr1])
have "Ee ξ (msub ρ A) = Ee ξ (msub ρ1 A1)" by (simp add: step)
also have "… = Ee (λn τ'. Ee ξ (ρ1 n τ')) A1"
by (rule Suc.IH[OF card1 wA1 Suc.prems(3) wr1 cr1])
also have "… = Ee ((λn τ'. Ee ξ (ρ1 n τ'))(x⇘σ⇙ := Ee (λn τ'. Ee ξ (ρ1 n τ')) (ρ x σ))) A"
unfolding A1_def by (rule ev_fsub_one[OF Suc.prems(2) Suc.prems(4) a1])
also have "Ee (λn τ'. Ee ξ (ρ1 n τ')) (ρ x σ) = Ee ξ (ρ x σ)"
by (rule ev_coin[OF Suc.prems(4) a1 Suc.prems(3)]) (simp add: occu)
also have "(λn τ'. Ee ξ (ρ1 n τ'))(x⇘σ⇙ := Ee ξ (ρ x σ))
= (λn τ'. Ee ξ (ρ n τ'))"
unfolding ρ1_def by (auto simp: upd_def fun_eq_iff)
finally show ?thesis .
qed
qed
lemma ev_msub:
assumes "wff⇘τ⇙(A)" and "asg ξ"
and "⋀n τ'. wff⇘τ'⇙(ρ n τ')"
and "⋀n τ'. ρ n τ' ≠ n⇧f⇘τ'⇙ ⟹ fvs (ρ n τ') = {}"
shows "Ee ξ (msub ρ A) = Ee (λn τ'. Ee ξ (ρ n τ')) A"
by (rule ev_msub_aux[OF order_refl assms])
text ‹The parameter-valued instance: the simultaneous closure ‹vpar S π› evaluates like
the assignment that reads off the parameter values on ‹S›.›
lemma ev_vpar:
assumes wA: "wff⇘τ⇙(A)" and xi: "asg ξ"
shows "Ee ξ (vpar S π A) = Ee (λn σ. if (n, σ) ∈ S then Ee ξ ((π n σ)⇧p⇘σ⇙) else ξ n σ) A"
proof -
have "Ee ξ (vpar S π A)
= Ee (λn σ. Ee ξ (if (n, σ) ∈ S then (π n σ)⇧p⇘σ⇙ else n⇧f⇘σ⇙)) A"
unfolding vpar_def
by (rule ev_msub[OF wA xi]) (auto intro: wff_Par wff_Fre split: if_splits)
also have "(λn σ. Ee ξ (if (n, σ) ∈ S then (π n σ)⇧p⇘σ⇙ else n⇧f⇘σ⇙))
= (λn σ. if (n, σ) ∈ S then Ee ξ ((π n σ)⇧p⇘σ⇙) else ξ n σ)"
by (auto simp: fun_eq_iff ev_var[OF xi])
finally show ?thesis .
qed
end
subsection ‹Transport of consequence along renamings and closures›
text ‹On the semantic side, maps of parameter names need @{emph ‹no›} injectivity:
any ‹h :: 'p ⇒ 'q› turns a model for ‹'q› into a model for ‹'p› by
evaluating through ‹prn h› --- the value conditions ‹vl⇩¬, …, vl⇩ι› only
inspect ‹Ee› at the logical constants, which ‹prn› fixes.›
lemma bkk_model_reduct:
fixes Ee :: "(nat ⇒ ty ⇒ 'u) ⇒ 'q tm ⇒ 'u" and h :: "'p ⇒ 'q"
assumes "bkk_model Dm Ap Ee vl"
shows "bkk_model Dm Ap (λξ t. Ee ξ (prn h t)) vl"
proof -
interpret bkk_model Dm Ap Ee vl by (rule assms)
show ?thesis
proof (unfold_locales, goal_cases)
case 3 thus ?case using ev_app by fastforce
next case 4 thus ?case by (metis ev_coin prn_occ wff_prn)
next case 5 thus ?case using ev_beta by blast
qed(auto simp: vl_eq vl_pi vl_dis vl_neg vl_iota ev_var ev_type wff_prn prop_f prop_b)
qed
text ‹The next lemma, ‹bkk_valid_map›, keeps its statement from the initial release of this
entry (August 2026) (compatibility export); it is the empty-context instance of ‹bkk_consequence_map›
below.›
lemma bkk_valid_map:
fixes h :: "'p ⇒ 'q"
assumes v: "⊨('u) (A :: 'p tm)"
shows "⊨('u) (prn h A :: 'q tm)"
unfolding bkk_valid_def rel_truth_def
by (metis bkk_model_reduct bkk_valid_def rel_truth_def v)
text ‹Semantic consequence transports along an @{emph ‹arbitrary›} map of parameter names:
the reduct of a ‹'q›-model is a ‹'p›-model, and it satisfies a hypothesis iff the original
satisfies its renaming.›
lemma bkk_consequence_map:
fixes h :: "'p ⇒ 'q"
assumes v: "Φ ⊨('u) (A :: 'p tm)"
and wΦ: "⋀B. B ∈ Φ ⟹ wff⇘𝗈⇙(B)"
shows "prn h ` Φ ⊨('u) (prn h A :: 'q tm)"
unfolding bkk_consequence_def rel_truth_def
proof (intro allI impI)
fix Dm Ap and Ee :: "(nat ⇒ ty ⇒ 'u) ⇒ 'q tm ⇒ 'u" and vl :: "'u ⇒ bool" and ξ
assume bm: "bkk_model Dm Ap Ee vl" and xi: "app_struct.asg Dm ξ"
and sat: "∀B'∈prn h ` Φ. wff 𝗈 B' ∧ vl (Ee ξ B')"
have bm': "bkk_model Dm Ap (λξ t. Ee ξ (prn h t)) vl" by (rule bkk_model_reduct[OF bm])
have "∀B∈Φ. wff 𝗈 B ∧ vl (Ee ξ (prn h B))" using sat wΦ by blast
thus "vl (Ee ξ (prn h A))"
using v bm' xi unfolding bkk_consequence_def rel_truth_def by blast
qed
text ‹Semantic consequence transports along the simultaneous closure, exactly as it does
along parameter renamings (@{thm [source] bkk_consequence_map}): every assignment for the
closed image induces, via the parameter values, an assignment for the originals.›
lemma bkk_consequence_vpar:
assumes v: "Φ ⊨('u) (A :: 'p tm)"
and wΦ: "⋀B. B ∈ Φ ⟹ wff⇘𝗈⇙(B)" and wA: "wff⇘𝗈⇙(A)"
shows "vpar UNIV π ` Φ ⊨('u) vpar UNIV π A"
unfolding bkk_consequence_def rel_truth_def
proof (intro allI impI)
fix Dm Ap and Ee :: "(nat ⇒ ty ⇒ 'u) ⇒ 'p tm ⇒ 'u" and vl :: "'u ⇒ bool" and ξ
assume bm: "bkk_model Dm Ap Ee vl" and xi: "app_struct.asg Dm ξ"
and sat: "∀B'∈vpar UNIV π ` Φ. wff 𝗈 B' ∧ vl (Ee ξ B')"
interpret M: bkk_model Dm Ap Ee vl by (rule bm)
have asg': "app_struct.asg Dm (λn σ. Ee ξ ((π n σ)⇧p⇘σ⇙))"
using M.ev_type[OF wff_Par xi] by (simp add: M.asg_def)
have evA: "Ee ξ (vpar UNIV π A) = Ee (λn σ. Ee ξ ((π n σ)⇧p⇘σ⇙)) A"
using M.ev_vpar[where S = UNIV, OF wA xi] by simp
have sat': "∀B∈Φ. wff 𝗈 B ∧ vl (Ee (λn σ. Ee ξ ((π n σ)⇧p⇘σ⇙)) B)"
proof
fix B assume B: "B ∈ Φ"
have wB: "wff⇘𝗈⇙(B)" using wΦ B by blast
have "Ee ξ (vpar UNIV π B) = Ee (λn σ. Ee ξ ((π n σ)⇧p⇘σ⇙)) B"
using M.ev_vpar[where S = UNIV, OF wB xi] by simp
moreover have "vpar UNIV π B ∈ vpar UNIV π ` Φ" using B by blast
ultimately show "wff 𝗈 B ∧ vl (Ee (λn σ. Ee ξ ((π n σ)⇧p⇘σ⇙)) B)"
using sat wB by auto
qed
have "vl (Ee (λn σ. Ee ξ ((π n σ)⇧p⇘σ⇙)) A)"
by (rule v[unfolded bkk_consequence_def rel_truth_def, rule_format,
OF bm asg' sat'[rule_format]])
thus "vl (Ee ξ (vpar UNIV π A))" by (simp add: evA)
qed
subsection ‹The valuation locale›
text ‹The ‹valuation› locale axiomatises what a term model provides: a carrier ‹'u› with an
application ‹❙@› and an evaluation ‹𝒱› of closed well-formed terms. It abstracts the
@{emph ‹quotient›} of BKK's term evaluation (BKK Definition 3.35) by Leibniz equality, as
constructed in the model-existence proof (BKK Theorem 6.33) --- note that the bare term
evaluation ‹𝒯ℰ(Σ)⇧β› is @{emph ‹not›} functional (BKK Remark 3.37); functionality only holds
after the quotient. The axioms: ‹v_app›/‹v_beta› are the evaluation conditions (BKK
Definition 3.18(2),(4)); ‹v_neg›, ‹v_dis›, ‹v_pi› are ‹L⇘¬⇙›, ‹L⇘∨⇙›, ‹L⇧σ⇘∀⇙› (BKK Figure 2);
‹v_ext› is functionality (property f), ‹v_eq› is primitive equality ‹L⇧σ⇘=⇙› (whence
property q), ‹v_desc› the description condition, ‹v_type› type-disjointness of the
domains, and ‹v_TF›/‹v_bool› are property b (BKK Definition 3.46).›
locale valuation =
fixes Dv :: "ty ⇒ 'u ⇒ bool" (‹𝒟⇘_⇙›)
and Vap :: "'u ⇒ 'u ⇒ 'u" (infixl ‹❙@› 200)
and Val :: "'p tm ⇒ 'u" (‹𝒱›)
assumes v_dom: "𝒟⇘σ⇙ d ⟷ (∃t. cwff σ t ∧ d = 𝒱 t)"
and v_app: "cwff (σ❙⇒τ) s ⟹ cwff σ t ⟹ 𝒱 (s ❙⋅ t) = 𝒱 s ❙@ 𝒱 t"
and v_beta: "cwff (σ❙⇒τ) (❙Λ⇘σ⇙ b) ⟹ cwff σ a ⟹ 𝒱 (❙Λ⇘σ⇙ b) ❙@ 𝒱 a = 𝒱 (b❙⟨a❙⟩)"
and v_TF: "𝒱 ❙⊤ ≠ 𝒱 ❙⊥"
and v_bool: "cwff 𝗈 φ ⟹ 𝒱 φ = 𝒱 ❙⊤ ∨ 𝒱 φ = 𝒱 ❙⊥"
and v_neg: "cwff 𝗈 φ ⟹ 𝒱 (❙¬ φ) = (if 𝒱 φ = 𝒱 ❙⊤ then 𝒱 ❙⊥ else 𝒱 ❙⊤)"
and v_dis: "cwff 𝗈 φ ⟹ cwff 𝗈 ψ ⟹
𝒱 (φ ❙∨ ψ) = (if 𝒱 φ = 𝒱 ❙⊤ ∨ 𝒱 ψ = 𝒱 ❙⊤ then 𝒱 ❙⊤ else 𝒱 ❙⊥)"
and v_pi: "cwff (σ❙⇒𝗈) f ⟹ 𝒱 ((Pi σ) ❙⋅ f) =
(if (∀a. cwff σ a ⟶ 𝒱 f ❙@ 𝒱 a = 𝒱 ❙⊤) then 𝒱 ❙⊤ else 𝒱 ❙⊥)"
and v_ext: "cwff (σ❙⇒τ) g ⟹ cwff (σ❙⇒τ) h
⟹ (⋀a. cwff σ a ⟹ 𝒱 g ❙@ 𝒱 a = 𝒱 h ❙@ 𝒱 a) ⟹ 𝒱 g = 𝒱 h"
and v_eq: "cwff σ a ⟹ cwff σ b ⟹ (𝒱 (Eq σ) ❙@ 𝒱 a ❙@ 𝒱 b = 𝒱 ❙⊤) = (𝒱 a = 𝒱 b)"
and v_desc: "cwff (σ❙⇒𝗈) f ⟹ cwff σ a
⟹ (∀b. cwff σ b ⟶ (𝒱 f ❙@ 𝒱 b = 𝒱 ❙⊤) = (𝒱 b = 𝒱 a))
⟹ 𝒱 ((Iota σ) ❙⋅ f) = 𝒱 a"
and v_type: "cwff σ s ⟹ cwff τ t ⟹ 𝒱 s = 𝒱 t ⟹ σ = τ"
begin
lemma v_domI: "cwff σ t ⟹ 𝒟⇘σ⇙ (𝒱 t)" using v_dom by blast
end
subsection ‹The term evaluation (BKK Section 6)›
text ‹A valuation extends to an evaluation function by simultaneous substitution of
representatives: ‹E⇘ξ⇙(A) := 𝒱([ρ⇘ξ⇙]A)›, BKK's evaluation for the term structure.
‹β›-respect is inherited from ‹v_beta› under closing substitutions, functionality is
‹v_ext›, and the remaining valuation conditions supply the ‹L›-properties --- so every
valuation is directly a ‹Σ›-model in the class ‹ℳ⇘βfb⇙›, with no detour through the
recursive denotation.›
context valuation
begin
definition vresp where "vresp ξ ≡ ∀n τ. 𝒟⇘τ⇙ (ξ n τ)"
definition rep_of where "rep_of ξ (n::nat) τ = (SOME t. cwff τ t ∧ ξ n τ = 𝒱 t)"
lemma rep_of_spec:
assumes "vresp ξ" shows "cwff τ (rep_of ξ n τ) ∧ ξ n τ = 𝒱 (rep_of ξ n τ)"
by (smt (verit, del_insts) assms rep_of_def someI_ex v_dom valuation.vresp_def
valuation_axioms)
text ‹The valuation respects ‹β›-conversion under closing substitutions: ‹β›-equal closed
terms are identified in the quotient (BKK Section 6).›
lemma beq_V: "s ≈⇘ρ'⇙ t ⟹ (⋀n τ. cwff τ (ρ n τ)) ⟹ 𝒱 (msub ρ s) = 𝒱 (msub ρ t)"
proof (induction arbitrary: ρ rule: beq.induct)
case (beta σ ρ' b a)
have lcr: "lc (ρ n τ)" for n τ
using beta.prems by (auto intro: wff_lc cwff_wff)
have cw1: "cwff (σ❙⇒ρ') (❙Λ⇘σ⇙ (msub ρ b))"
using cwff_msub[OF beta.hyps(1) beta.prems] by simp
have "𝒱 (msub ρ ((❙Λ⇘σ⇙ b) ❙⋅ a)) = 𝒱 (❙Λ⇘σ⇙ (msub ρ b)) ❙@ 𝒱 (msub ρ a)"
by (simp add: v_app[OF cw1 cwff_msub[OF beta.hyps(2) beta.prems]])
also have "… = 𝒱 ((msub ρ b)❙⟨msub ρ a❙⟩)"
by (rule v_beta[OF cw1 cwff_msub[OF beta.hyps(2) beta.prems]])
also have "… = 𝒱 (msub ρ (b❙⟨a❙⟩))" by (simp add: msub_opn[OF lcr])
finally show ?case.
next case (appL s σ ρ' s' t) thus ?case
by (smt (verit, ccfv_SIG) beq_wff cwff_msub msub.simps(9) valuation.v_app valuation_axioms)
next case (appR t σ t' ρ' s)
have wt: "wff⇘σ⇙(t)" and wt': "wff⇘σ⇙(t')"
using beq_wff[OF appR.hyps(1)] by auto
thus ?case using appR cwff_msub by (metis msub.simps(9) v_app)
next case (abs L b σ τ b')
obtain x where x: "x ∉ L ∪ fvs b ∪ fvs b'"
by (meson abs.hyps(1) ex_new_if_finite finite_UnI finite_fvs infinite_UNIV_nat)
have wb: "wff⇘τ⇙(b❙⟨x⇧f⇘σ⇙❙⟩)" and wb': "wff⇘τ⇙(b'❙⟨x⇧f⇘σ⇙❙⟩)"
using beq_wff[OF abs.hyps(2)[of x]] x by auto
have wA: "wff⇘σ❙⇒τ⇙(❙Λ⇘σ⇙ b)" using wff_Abs_open_rev[OF wb] x by auto
have wA': "wff⇘σ❙⇒τ⇙(❙Λ⇘σ⇙ b')" using wff_Abs_open_rev[OF wb'] x by auto
have "cwff (σ❙⇒τ) (❙Λ⇘σ⇙ (msub ρ b))"
using cwff_msub[OF wA abs.prems] by simp
moreover have "cwff (σ❙⇒τ) (❙Λ⇘σ⇙ (msub ρ b'))"
using cwff_msub[OF wA' abs.prems] by simp
moreover have "𝒱 (❙Λ⇘σ⇙ (msub ρ b)) ❙@ 𝒱 a = 𝒱 (❙Λ⇘σ⇙ (msub ρ b')) ❙@ 𝒱 a" if a: "cwff σ a" for a
proof -
let ?ρ = "ρ(x := (ρ x)(σ := a))"
have cr: "cwff τ' (?ρ n τ')" for n τ' using abs.prems a by auto
have lcr: "lc (?ρ n τ')" for n τ' using cr
by (meson wff_lc cwff_wff)
have mb: "msub ?ρ b = msub ρ b"
using msub_cong x fvs_eq_fst_occ image_iff
by (smt (verit, best) UnCI fst_conv fun_upd_other)
have mb': "msub ?ρ b' = msub ρ b'"
using msub_cong fvs_eq_fst_occ image_iff x
by (smt (verit, ccfv_threshold) Un_iff fst_conv fun_upd_other)
have e2: "msub ?ρ ((x⇧f⇘σ⇙) :: 'p tm) = a" by simp
have ob: "msub ?ρ (b❙⟨x⇧f⇘σ⇙❙⟩) = (msub ρ b)❙⟨a❙⟩"
by (simp only: msub_opn[OF lcr] e2 mb)
have ob': "msub ?ρ (b'❙⟨x⇧f⇘σ⇙❙⟩) = (msub ρ b')❙⟨a❙⟩"
by (simp only: msub_opn[OF lcr] e2 mb')
have IH: "𝒱 (msub ?ρ (b❙⟨x⇧f⇘σ⇙❙⟩)) = 𝒱 (msub ?ρ (b'❙⟨x⇧f⇘σ⇙❙⟩))"
by (rule abs.IH) (use x cr in auto)
have "𝒱 ((msub ρ b)❙⟨a❙⟩) = 𝒱 ((msub ρ b')❙⟨a❙⟩)" using IH
by (simp only: ob ob')
thus ?thesis using v_beta calculation a by simp
qed
ultimately show ?case using v_ext by simp
qed auto
text ‹BKK's evaluation function for the term model.›
definition Eval :: "(nat ⇒ ty ⇒ 'u) ⇒ 'p tm ⇒ 'u" where "Eval ξ A = 𝒱 (msub (rep_of ξ) A)"
end
text ‹Every valuation is a ‹Σ›-model in the class ‹ℳ⇘βfb⇙› (the direct construction of
BKK Section 6).›
sublocale valuation ⊆ bkkA: app_struct Dv Vap
proof (unfold_locales, goal_cases)
case 1 show ?case using v_domI[OF cwff_Par] by blast
next case 2 thus ?case using cwff_App v_dom valuation.v_app
valuation_axioms by fastforce
qed
sublocale valuation ⊆ bkkM: bkk_model Dv Vap Eval "λa. a = 𝒱 ❙⊤"
proof (unfold_locales, goal_cases)
case 1 thus ?case
by (metis Eval_def bkkA.asg_def cwff_msub rep_of_spec v_domI vresp_def)
next case 2 thus ?case
using Eval_def bkkA.asg_def rep_of_spec vresp_def by (metis msub.simps(2))
next case 3 thus ?case
by (metis Eval_def bkkA.asg_def cwff_msub msub.simps(9) rep_of_spec v_app vresp_def)
next case (4 τ A ξ ξ')
hence "rep_of ξ n σ = rep_of ξ' n σ" if "(n, σ) ∈ occ A" for n σ
using that by (auto simp: rep_of_def)
thus ?case unfolding Eval_def by (simp cong: msub_cong)
next case 5 thus ?case using Eval_def beq_V bkkA.asg_def rep_of_spec vresp_def by metis
next case 6 thus ?case by (metis Eval_def cwff_Neg msub.simps(4) v_TF v_app v_dom v_neg)
next case (7 ξ a b)
then obtain φ ψ where ab: "a = 𝒱 φ" "b = 𝒱 ψ" and c: "cwff 𝗈 φ" "cwff 𝗈 ψ"
using v_dom by blast
have e: "Eval ξ Dis = 𝒱 Dis" by (simp add: Eval_def)
show ?case unfolding e ab using v_TF
by (metis c(1,2) cwff_App cwff_Dis v_app v_dis)
next case (8 ξ σ f)
then obtain g where fg: "f = 𝒱 g" and cg: "cwff (σ ❙⇒ 𝗈) g"
using v_dom by blast
have e: "Eval ξ (Pi σ) = 𝒱 (Pi σ)" by (simp add: Eval_def)
have q: "(∀d. 𝒟⇘σ⇙ d ⟶ 𝒱 g ❙@ d = 𝒱 ❙⊤) = (∀a. cwff σ a ⟶ 𝒱 g ❙@ 𝒱 a = 𝒱 ❙⊤)"
using v_dom by metis
show ?case unfolding e fg using v_TF
by (auto simp: v_app[OF cwff_Pi cg, symmetric] v_pi[OF cg] q)
next case 9 thus ?case using Eval_def v_dom v_eq by fastforce
next case 10 thus ?case
by (smt (verit, best) Eval_def cwff_Iota msub.simps(7) v_app v_desc v_dom)
next case 11 thus ?case by (smt (verit, ccfv_threshold) bkkA.functional_def v_dom v_ext)
next case 12 thus ?case by (metis v_bool v_dom)
qed
subsection ‹Standard models (BKK Definition 3.51)›
text ‹A @{emph ‹‹Σ›-standard model›} (BKK Definition 3.51) is a ‹Σ›-Henkin model over a
@{emph ‹full›} frame (BKK Definition 3.5): every set-function between domains has a
representative. We record fullness by the universal abstraction laws ‹Lm_dom› and
‹beta_Lm›, quantified over @{emph ‹all›} functions ‹h :: 'u ⇒ 'u› --- strictly stronger
than the Henkin conditions of @{locale general_model}. On top of the full frame we assume
the ‹Σ›-valuation conditions (BKK Definition 3.41, Figure 2) with property b, property f
(functionality) and property q (BKK Definition 3.46).›
locale standard_model = frame_sig +
assumes beta_Lm: "⟦⋀d. 𝒟⇘σ⇙ d ⟹ 𝒟⇘τ⇙ (h d); 𝒟⇘σ⇙ a⟧ ⟹ Lm σ h ❙@ a = h a"
and Lm_dom: "(⋀d. 𝒟⇘σ⇙ d ⟹ 𝒟⇘τ⇙ (h d)) ⟹ 𝒟⇘σ❙⇒τ⇙ (Lm σ h)"
and Ap_dom: "⟦𝒟⇘σ❙⇒τ⇙ f; 𝒟⇘σ⇙ a⟧ ⟹ 𝒟⇘τ⇙ (f ❙@ a)"
and Ngv_dom: "𝒟⇘𝗈❙⇒𝗈⇙ Ngv"
and Dsv_dom: "𝒟⇘𝗈❙⇒𝗈❙⇒𝗈⇙ Dsv"
and Piv_dom: "𝒟⇘(σ❙⇒𝗈)❙⇒𝗈⇙ (Piv σ)"
and Iv_dom: "𝒟⇘(σ❙⇒𝗈)❙⇒σ⇙ (Iv σ)"
and Ev_dom: "𝒟⇘σ❙⇒σ❙⇒𝗈⇙ (Ev σ)" and Jv_dom: "𝒟⇘σ⇙ (Jv p σ)"
and TF: "Tv ≠ Fv" and boolean: "𝒟⇘𝗈⇙ a ⟷ a = Tv ∨ a = Fv"
and Lneg: "𝒟⇘𝗈⇙ a ⟹ (Ngv ❙@ a = Tv) = (a ≠ Tv)"
and Ldis: "⟦𝒟⇘𝗈⇙ a; 𝒟⇘𝗈⇙ b⟧ ⟹ (Dsv ❙@ a ❙@ b = Tv) = (a = Tv ∨ b = Tv)"
and Lall: "𝒟⇘σ❙⇒𝗈⇙ f ⟹ (Piv σ ❙@ f = Tv) = (∀d. 𝒟⇘σ⇙ d ⟶ f ❙@ d = Tv)"
and Leq: "⟦𝒟⇘σ⇙ a; 𝒟⇘σ⇙ b⟧ ⟹ (Ev σ ❙@ a ❙@ b = Tv) = (a = b)"
and funct: "⟦𝒟⇘σ❙⇒τ⇙ g; 𝒟⇘σ❙⇒τ⇙ k; ⋀a. 𝒟⇘σ⇙ a ⟹ g ❙@ a = k ❙@ a⟧ ⟹ g = k"
and descB: "⟦𝒟⇘σ❙⇒𝗈⇙ f; 𝒟⇘σ⇙ a; ∀b. 𝒟⇘σ⇙ b ⟶ (f ❙@ b = Tv) = (b = a)⟧
⟹ Iv σ ❙@ f = a"
begin
text ‹As in @{locale general_model}, membership of the truth values follows from property b.›
lemma Tv_dom [simp]: "𝒟⇘𝗈⇙ Tv" and Fv_dom [simp]: "𝒟⇘𝗈⇙ Fv"
by (simp_all add: boolean)
text ‹Every domain is inhabited, as in @{locale general_model}: the interpretation ‹Jv› of a
parameter provides a witness at every type. BKK build non-emptiness into the applicative
structure (BKK Definition 3.1).›
lemma dom_nonempty: "∃d. 𝒟⇘τ⇙ d" by (metis Jv_dom)
text ‹In a full frame every well-formed term denotes in the domain of its type (the standard
homomorphic construction, BKK Section 2.3.1).›
lemma std_den_dom: "wff⇘σ⇙(t) ⟹ ∀n ρ. 𝒟⇘ρ⇙ (ξ n ρ) ⟹ 𝒟⇘σ⇙ (⦇t⦈⇘ξ⇙)"
proof (induction arbitrary: ξ rule: wff.induct)
case (wff_App σ τ s t) thus ?case
by (metis Ap_dom frame_sig.den.simps(8))
next
case (wff_Abs L τ b σ)
define x where "x = fresh (L ∪ fvs b)"
have xL: "x ∉ L" and xb: "x ∉ fvs b"
using fresh_notin[of "L ∪ fvs b"] wff_Abs unfolding x_def by auto
have "𝒟⇘σ❙⇒τ⇙ (Lm σ (λd. ⦇b❙⟨x⇧f⇘σ⇙❙⟩⦈⇘ξ(x⇘σ⇙ := d)⇙))"
by (simp add: Lm_dom upd_def wff_Abs.IH wff_Abs.prems xL)
thus ?case by (simp add: den_Abs[OF xb])
qed (simp_all add: Jv_dom Ngv_dom Dsv_dom Piv_dom Iv_dom Ev_dom)
end
text ‹Every standard model is a ‹Σ›-Henkin general model (BKK Definition 3.51 is a special
case of Definition 3.50): the universal abstraction laws specialise to the denotation
functions.›
sublocale standard_model ⊆ general_model Dm Ap Lm Tv Fv Ngv Dsv Iv Ev Piv Jv
proof
show "𝒟⇘𝗈⇙ a ⟷ a = Tv ∨ a = Fv" for a using boolean Tv_dom Fv_dom by blast
show "𝒟⇘σ❙⇒τ⇙ g ⟹ 𝒟⇘σ❙⇒τ⇙ k ⟹ (⋀a. 𝒟⇘σ⇙ a ⟹ g ❙@ a = k ❙@ a) ⟹ g = k" for σ τ g k
by (rule funct)
show "wff⇘σ❙⇒τ⇙(❙Λ⇘σ⇙ bd) ⟹ ∀n ρ. 𝒟⇘ρ⇙ (ξ n ρ) ⟹ 𝒟⇘σ❙⇒τ⇙ (⦇❙Λ⇘σ⇙ bd⦈⇘ξ⇙)" for σ τ bd ξ
using std_den_dom by blast
next
fix τ x σ and bd :: ‹'b tm› and ξ :: ‹nat ⇒ ty ⇒ 'a› and a
assume wb: "wff⇘τ⇙(bd❙⟨x⇧f⇘σ⇙❙⟩)" and xb: "x ∉ fvs bd"
and r: "∀n ρ. 𝒟⇘ρ⇙ (ξ n ρ)" and da: "𝒟⇘σ⇙ a"
have "⦇❙Λ⇘σ⇙ bd⦈⇘ξ⇙ = Lm σ (λd. ⦇bd❙⟨x⇧f⇘σ⇙❙⟩⦈⇘ξ(x⇘σ⇙ := d)⇙)"
by (rule den_Abs[OF xb])
moreover have "Lm σ (λd. ⦇bd❙⟨x⇧f⇘σ⇙❙⟩⦈⇘ξ(x⇘σ⇙ := d)⇙) ❙@ a = ⦇bd❙⟨x⇧f⇘σ⇙❙⟩⦈⇘ξ(x⇘σ⇙ := a)⇙"
using r std_den_dom wb by (auto intro!: beta_Lm[where τ=τ, OF _ da] simp: upd_def)
ultimately show ‹⦇❙Λ⇘σ⇙ bd⦈⇘ξ⇙ ❙@ a = ⦇bd❙⟨x⇧f⇘σ⇙❙⟩⦈⇘ξ(x⇘σ⇙ := a)⇙› by simp
qed(safe intro!: Lall Ldis Lneg Leq Jv_dom Ev_dom Iv_dom Piv_dom Dsv_dom Ngv_dom Ap_dom TF
descB dom_nonempty)
subsection ‹Constructing the logical constants over a ‹λ›-universe›
text ‹A ‹Σ›-standard model need not be @{emph ‹given›} its logical constants: over any
universe with full function spaces (‹β›-abstraction with its typing, extensionality),
booleans and a domain-respecting parameter interpretation, they can be
@{emph ‹constructed›} --- negation, disjunction, quantification and equality by
‹λ›-abstraction over the domains, description by definite description (‹THE›, not
Hilbert choice).›
locale lambda_universe =
fixes Dm :: "ty ⇒ 'u ⇒ bool" and Ap :: "'u ⇒ 'u ⇒ 'u"
and Lm :: "ty ⇒ ('u ⇒ 'u) ⇒ 'u" and Tv Fv :: 'u and Jv :: "'p ⇒ ty ⇒ 'u"
assumes beta_Lm: "⟦⋀d. Dm σ d ⟹ Dm τ (h d); Dm σ a⟧ ⟹ Ap (Lm σ h) a = h a"
and Lm_dom: "(⋀d. Dm σ d ⟹ Dm τ (h d)) ⟹ Dm (σ ❙⇒ τ) (Lm σ h)"
and Ap_dom: "⟦Dm (σ ❙⇒ τ) f; Dm σ a⟧ ⟹ Dm τ (Ap f a)"
and funct: "⟦Dm (σ ❙⇒ τ) g; Dm (σ ❙⇒ τ) k; ⋀a. Dm σ a ⟹ Ap g a = Ap k a⟧ ⟹ g = k"
and TF: "Tv ≠ Fv"
and boolean: "Dm 𝗈 a ⟷ a = Tv ∨ a = Fv"
and Jv_dom: "Dm σ (Jv p σ)"
begin
lemma bTv [simp]: "Dm 𝗈 Tv" and bFv [simp]: "Dm 𝗈 Fv" using boolean by auto
definition Ngv :: 'u where "Ngv = Lm 𝗈 (λa. if a = Tv then Fv else Tv)"
definition Dsv :: 'u where
"Dsv = Lm 𝗈 (λa. Lm 𝗈 (λb. if a = Tv ∨ b = Tv then Tv else Fv))"
definition Piv :: "ty ⇒ 'u" where
"Piv σ = Lm (σ ❙⇒ 𝗈) (λf. if ∀d. Dm σ d ⟶ Ap f d = Tv then Tv else Fv)"
definition Ev :: "ty ⇒ 'u" where
"Ev σ = Lm σ (λa. Lm σ (λb. if a = b then Tv else Fv))"
definition Iv :: "ty ⇒ 'u" where
"Iv σ = Lm (σ ❙⇒ 𝗈)
(λf. if ∃a. Dm σ a ∧ (∀b. Dm σ b ⟶ (Ap f b = Tv) = (b = a))
then THE a. Dm σ a ∧ (∀b. Dm σ b ⟶ (Ap f b = Tv) = (b = a))
else Jv undefined σ)"
lemma Ngv_dom: "Dm (𝗈 ❙⇒ 𝗈) Ngv" unfolding Ngv_def by (rule Lm_dom) simp
lemma Dsv_dom: "Dm (𝗈 ❙⇒ 𝗈 ❙⇒ 𝗈) Dsv" unfolding Dsv_def by (intro Lm_dom) simp
lemma Piv_dom: "Dm ((σ ❙⇒ 𝗈) ❙⇒ 𝗈) (Piv σ)" unfolding Piv_def by (rule Lm_dom) simp
lemma Ev_dom: "Dm (σ ❙⇒ σ ❙⇒ 𝗈) (Ev σ)" unfolding Ev_def by (intro Lm_dom) simp
lemma Ngv_app: "Dm 𝗈 a ⟹ Ap Ngv a = (if a = Tv then Fv else Tv)"
unfolding Ngv_def by (rule beta_Lm[where τ = 𝗈]) simp_all
lemma Piv_app: "Dm (σ ❙⇒ 𝗈) f ⟹ Ap (Piv σ) f = (if ∀d. Dm σ d ⟶ Ap f d = Tv then Tv else Fv)"
unfolding Piv_def by (rule beta_Lm[where τ = 𝗈]) simp_all
lemma Dsv_app: "⟦Dm 𝗈 a; Dm 𝗈 b⟧ ⟹ Ap (Ap Dsv a) b = (if a = Tv ∨ b = Tv then Tv else Fv)"
proof -
assume a: "Dm 𝗈 a" and b: "Dm 𝗈 b"
have "Ap Dsv a = Lm 𝗈 (λb. if a = Tv ∨ b = Tv then Tv else Fv)"
unfolding Dsv_def by (auto intro!: beta_Lm[where τ = "𝗈 ❙⇒ 𝗈", OF _ a] Lm_dom)
moreover have "Ap (Lm 𝗈 (λb. if a = Tv ∨ b = Tv then Tv else Fv)) b
= (if a = Tv ∨ b = Tv then Tv else Fv)"
by (rule beta_Lm[where τ = 𝗈, OF _ b]) simp
ultimately show ?thesis by simp
qed
lemma Ev_app: "⟦Dm σ a; Dm σ b⟧ ⟹ Ap (Ap (Ev σ) a) b = (if a = b then Tv else Fv)"
proof -
assume a: "Dm σ a" and b: "Dm σ b"
have "Ap (Ev σ) a = Lm σ (λb. if a = b then Tv else Fv)"
unfolding Ev_def by (auto intro!: beta_Lm[where τ = "σ ❙⇒ 𝗈", OF _ a] Lm_dom)
moreover have "Ap (Lm σ (λb. if a = b then Tv else Fv)) b = (if a = b then Tv else Fv)"
by (rule beta_Lm[where τ = 𝗈, OF _ b]) simp
ultimately show ?thesis by simp
qed
lemma Iv_body_dom: "Dm (σ ❙⇒ 𝗈) f ⟹
Dm σ (if ∃a. Dm σ a ∧ (∀b. Dm σ b ⟶ (Ap f b = Tv) = (b = a))
then THE a. Dm σ a ∧ (∀b. Dm σ b ⟶ (Ap f b = Tv) = (b = a))
else Jv undefined σ)"
by (smt (verit, ccfv_SIG) Jv_dom Uniq_I the1_equality')
lemma Iv_dom: "Dm ((σ ❙⇒ 𝗈) ❙⇒ σ) (Iv σ)"
unfolding Iv_def by (rule Lm_dom) (rule Iv_body_dom)
lemma Iv_app_desc:
assumes f: "Dm (σ ❙⇒ 𝗈) f" and a: "Dm σ a"
and s: "∀b. Dm σ b ⟶ (Ap f b = Tv) = (b = a)"
shows "Ap (Iv σ) f = a"
proof -
have "(THE a'. Dm σ a' ∧ (∀b. Dm σ b ⟶ (Ap f b = Tv) = (b = a'))) = a"
using a s by auto
moreover have "Ap (Iv σ) f
= (if ∃a'. Dm σ a' ∧ (∀b. Dm σ b ⟶ (Ap f b = Tv) = (b = a'))
then THE a'. Dm σ a' ∧ (∀b. Dm σ b ⟶ (Ap f b = Tv) = (b = a'))
else Jv undefined σ)"
unfolding Iv_def by (rule beta_Lm[OF Iv_body_dom f])
ultimately show ?thesis
by (metis a s)
qed
theorem is_standard_model: "standard_model Dm Ap Lm Tv Fv Ngv Dsv Iv Ev Piv Jv"
proof unfold_locales
show "⋀a. Dm 𝗈 a ⟹ (Ap Ngv a = Tv) = (a ≠ Tv)"
using Ngv_app TF by auto
show "⋀a b. Dm 𝗈 a ⟹ Dm 𝗈 b ⟹ (Ap (Ap Dsv a) b = Tv) = (a = Tv ∨ b = Tv)"
using Dsv_app TF by auto
show "⋀σ f. Dm (σ ❙⇒ 𝗈) f ⟹ (Ap (Piv σ) f = Tv) = (∀d. Dm σ d ⟶ Ap f d = Tv)"
using Piv_app TF by auto
show "⋀σ a b. Dm σ a ⟹ Dm σ b ⟹ (Ap (Ap (Ev σ) a) b = Tv) = (a = b)"
using Ev_app TF by auto
qed(auto intro: Iv_app_desc funct Jv_dom Ev_dom Iv_dom Piv_dom Lm_dom Ap_dom
beta_Lm Ngv_dom Dsv_dom
simp: TF boolean)
end
end