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 in Section 3).›
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 ‹A typed collection of non-empty domains with an application operator. BKK's
typing discipline ‹@ : D⇘α→β⇙ × D⇘α⇙ → D⇘β⇙› becomes a closure condition on the
one abstract operator. BKK's @{emph ‹frames›} (Definition 3.4, ‹D⇘α→β⇙ ⊆ F(D⇘α⇙; D⇘β⇙)›)
are a set-theoretic notion with no direct analogue over an abstract carrier; by BKK
Remark 3.6 every frame is functional, and it is @{emph ‹functionality›} (BKK
Definition 3.5; named property f in Definition 3.46) that all mathematical arguments consume, so
the model class below
is delineated by functionality.›
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); the update ‹ξ(x⇘σ⇙ := d)› is
BKK's ‹φ,[d/X]›.›
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: property f of BKK Definition 3.5.›
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 Section 1 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), (2), (4) and coincidence; the vehicle
for all abstraction reasoning below).›
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 (smt (verit, del_insts) asg_upd beta d fvs.simps(10) fvs_eq_fst_occ image_eqI prod.sel(1)
sigma_eval.ev_app sigma_eval.ev_beta sigma_eval.ev_coin sigma_eval.ev_var sigma_eval_axioms
upd_def wb wff_Fre 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); we fix a canonical assignment to name them.›
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 satisfying properties
q, f and b (with primitive equality, property q holds automatically, BKK
Definition 3.49 --- the q-witness at type ‹α› is the denotation ‹E(=⇘α⇙)›,
cf.\ the satisfaction lemma for Leibniz equality; with property b the
valuation is two-valued on ‹D⇘𝗈⇙›). This class
coincides with the ‹Σ›-Henkin models of BKK Definition 3.50 up to isomorphism
(BKK Lemma 3.67 and Theorem 3.68).›
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› in a model ‹⟨D,@,E,υ⟩› under 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"
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 ‹BKK Lemma 4.2: in a ‹Σ›-model with primitive equality (which gives property q with
witness ‹E(=⇘α⇙)›), Leibniz equality is satisfied exactly by equal denotations.›
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 ‹ℳ⇩*›; this development instantiates the most specialised one, the
class ‹ℳ⇩β⇩f⇩b› 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›}; equivalently, every wff denotes. A term model cannot be
full: with property b the domain ‹𝒟⇘ι❙⇒𝗈⇙› of a full frame over infinite ‹𝒟⇘ι⇙› would be
uncountable, whereas the term model 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_nonempty: "∃d. 𝒟⇘σ⇙ d"
and 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 ‹An assignment is @{emph ‹total›} (@{term resp}, respects the domains everywhere) if it
maps
every typed variable into the matching domain --- BKK's assignment @{emph ‹into›} the
structure.›
definition resp where "resp ξ ⟷ (∀(n::nat) τ. 𝒟⇘τ⇙ (ξ 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
end
subsection ‹Closed well-formed terms and simultaneous substitution›
text ‹A @{emph ‹closed›} well-formed term, BKK's ‹cwff⇘σ⇙› (BKK Section 2.2; BKK reserve
@{emph ‹sentence›} for closed formulae of type ‹𝗈› --- parameters are allowed,
they play the role of BKK's constants). These are the carriers of the term model.›
definition cwff :: "ty ⇒ 'p tm ⇒ bool" where "cwff σ A ⟷ wff⇘σ⇙(A) ∧ fvs A = {}"
lemma cwffI: "wff⇘σ⇙(A) ⟹ fvs A = {} ⟹ cwff σ A" by (simp add: cwff_def)
lemma cwff_wff: "cwff σ A ⟹ wff⇘σ⇙(A)" by (simp add: cwff_def)
lemma cwff_closed: "cwff σ A ⟹ fvs A = {}" by (simp add: cwff_def)
lemma cwff_lc: "cwff σ A ⟹ lc A" by (metis cwff_def wff_lc)
lemma cwff_Neg: "cwff (𝗈❙⇒𝗈) Neg"
and cwff_Dis: "cwff (𝗈❙⇒𝗈❙⇒𝗈) Dis"
and cwff_Pi: "cwff ((σ❙⇒𝗈)❙⇒𝗈) (Pi σ)"
and cwff_Iota: "cwff ((σ❙⇒𝗈)❙⇒σ) (Iota σ)"
and cwff_TrueB: "cwff 𝗈 ❙⊤"
and cwff_FalseB: "cwff 𝗈 ❙⊥"
by (auto simp: cwff_def wff_Neg wff_Dis wff_Pi wff_Iota)
lemma cwff_Eq: "cwff (σ❙⇒σ❙⇒𝗈) (Eq σ)" by (simp add: cwff_def wff_Eq)
lemma cwff_Par: "cwff σ (p⇧p⇘σ⇙)" by (simp add: cwff_def wff_Par)
lemma cwff_App: "cwff (σ❙⇒τ) s ⟹ cwff σ t ⟹ cwff τ (s ❙⋅ t)"
by (auto simp: cwff_def intro: wff.wff_App)
lemma cwff_opn: "cwff (σ❙⇒τ) (❙Λ⇘σ⇙ b) ⟹ cwff σ a ⟹ cwff τ (b❙⟨a❙⟩)"
by (metis (no_types, opaque_lifting) cwff_def fvs.simps(10) fvs_opn
subset_empty sup.idem wff_opn)
lemma cwff_unique: "cwff σ A ⟹ cwff τ A ⟹ σ = τ"
by (auto simp: cwff_def dest: wff_unique)
text ‹Converse of @{thm wff_Abs_open}: a body that is well-typed when opened with @{emph ‹one›}
fresh variable yields a well-typed abstraction (all fresh openings are ‹α›-variants).›
lemma wff_Abs_open_rev: "wff⇘τ⇙(b❙⟨x⇧f⇘σ⇙❙⟩) ⟹ x ∉ fvs b ⟹ wff⇘σ❙⇒τ⇙(❙Λ⇘σ⇙ b)"
by (metis fsub_intro wff_AbsI wff_Fre wff_fsub)
text ‹Simultaneous substitution of a (closed) term for every free variable --- the analogue of
the closing substitution ‹σ› in BKK's term evaluation (BKK Definition 3.35). Because the
replacements are closed, it commutes with opening --- the locally-nameless analogue of BKK's
parallel substitution, with no binder renaming.›
primrec msub :: "(nat ⇒ ty ⇒ 'p tm) ⇒ 'p tm ⇒ 'p tm" where
"msub ρ (Bnd i) = Bnd i"
| "msub ρ (n⇧f⇘τ⇙) = ρ n τ"
| "msub ρ (p⇧p⇘τ⇙) = p⇧p⇘τ⇙"
| "msub ρ Neg = Neg"
| "msub ρ Dis = Dis"
| "msub ρ (Pi τ) = Pi τ"
| "msub ρ (Iota τ) = Iota τ"
| "msub ρ (Eq τ) = Eq τ"
| "msub ρ (s ❙⋅ t) = (msub ρ s) ❙⋅ (msub ρ t)"
| "msub ρ (❙Λ⇘τ⇙ b) = ❙Λ⇘τ⇙ (msub ρ b)"
text ‹Parallel-substitution notation: ‹u❙⟦ρ❙⟧› applies the substitution ‹ρ›
to every free variable of ‹u›.›
syntax "_msub" :: "logic ⇒ logic ⇒ logic" (‹_❙⟦_❙⟧› [1000, 0] 1000)
syntax_consts "_msub" == "msub"
translations "u❙⟦ρ❙⟧" ⇌ "CONST msub ρ u"
lemma msub_opn: "(⋀n τ. lc (ρ n τ)) ⟹ msub ρ (opn k u t) = opn k (msub ρ u) (msub ρ t)"
by (induction t arbitrary: k) auto
lemma msub_cong: "(⋀n τ. (n, τ) ∈ occ t ⟹ ρ n τ = ρ' n τ) ⟹ msub ρ t = msub ρ' t"
by (induction t) auto
lemma fvs_msub: "(⋀n τ. fvs (ρ n τ) = {}) ⟹ fvs (msub ρ t) = {}"
by (induction t) auto
lemma wff_msub:
"wff⇘σ⇙(t) ⟹ (⋀n τ. wff⇘τ⇙(ρ n τ)) ⟹ wff⇘σ⇙(msub ρ t)"
proof (induction σ t arbitrary: ρ rule: wff.induct)
case (wff_Abs L τ b σ)
have lcr: "lc (ρ n τ')" for n τ' using wff_Abs.prems
by (rule wff_lc)
have "wff⇘σ❙⇒τ⇙(❙Λ⇘σ⇙ (msub ρ b))"
proof (rule wff.wff_Abs[of "L ∪ fvs b"])
fix y assume y: "y ∉ L ∪ fvs b"
let ?ρ = "ρ(y := (ρ y)(σ := y⇧f⇘σ⇙))"
have e: "msub ?ρ (b❙⟨y⇧f⇘σ⇙❙⟩) = (msub ρ b)❙⟨y⇧f⇘σ⇙❙⟩"
by (smt (verit, ccfv_SIG) Un_iff fun_upd_other fun_upd_same
fvs_eq_fst_occ image_eqI lc_Fre lcr msub.simps(2)
msub_cong msub_opn prod.sel(1) y)
have "wff⇘τ⇙(msub ?ρ (b❙⟨y⇧f⇘σ⇙❙⟩))"
using wff_Abs wff.wff_Fre y by (metis Un_iff fun_upd_other fun_upd_same)
thus "wff⇘τ⇙((msub ρ b)❙⟨y⇧f⇘σ⇙❙⟩)" using e by simp
qed (simp add: wff_Abs)
thus ?case by simp
qed(auto intro: wff.intros)
text ‹A well-formed term becomes a @{emph ‹closed›} well-formed term under a closed simultaneous
substitution --- the instance used to build the term model.›
lemma cwff_msub: "wff⇘σ⇙(t) ⟹ (⋀n τ. cwff τ (ρ n τ)) ⟹ cwff σ (msub ρ t)"
by (metis cwff_def wff_msub fvs_msub)
text ‹A closed term is untouched by simultaneous substitution.›
lemma msub_closed: "fvs t = {} ⟹ msub ρ t = t" by (induction t) auto
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::nat) τ. 𝒟⇘τ⇙ (ξ 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 τ)"
proof -
have "𝒟⇘τ⇙ (ξ n τ)" using assms[unfolded vresp_def] by blast
hence "∃t. cwff τ t ∧ ξ n τ = 𝒱 t" using v_dom by blast
thus ?thesis unfolding rep_of_def by (rule someI_ex)
qed
text ‹The valuation respects ‹β›-conversion under closing substitutions (BKK's quotient
of the term structure by ‹β›, Section 6): the abstraction case is pointwise by ‹v_beta›
and closed by ‹v_ext›.›
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 Ev :: "(nat ⇒ ty ⇒ 'u) ⇒ 'p tm ⇒ 'u" where "Ev ξ 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 α β f a) thus ?case using cwff_App v_dom valuation.v_app
valuation_axioms by fastforce
qed
sublocale valuation ⊆ bkkM: bkk_model Dv Vap Ev "λa. a = 𝒱 ❙⊤"
proof (unfold_locales, goal_cases)
case (1 τ A ξ) thus ?case
by (metis Ev_def bkkA.asg_def cwff_msub rep_of_spec v_domI vresp_def)
next case (2 ξ n σ) thus ?case
using Ev_def bkkA.asg_def rep_of_spec vresp_def by auto
next case (3 σ τ F A ξ) thus ?case
by (metis Ev_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 Ev_def by (simp cong: msub_cong)
next case 5 thus ?case using Ev_def beq_V bkkA.asg_def rep_of_spec vresp_def by auto
next case 6 thus ?case by (metis Ev_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: "Ev ξ Dis = 𝒱 Dis" by (simp add: Ev_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: "Ev ξ (Pi σ) = 𝒱 (Pi σ)" by (simp add: Ev_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 Ev_def v_dom v_eq by fastforce
next case 10 thus ?case by (smt (verit, best) Ev_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 ‹In a full frame every domain is inhabited (for ‹𝗈› by ‹Tv›, for ‹ι› by applying ‹Iv›
to a representable predicate, for function types by a constant function). 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): the abstraction case is immediate from
fullness.›
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)
end