isabelle-record

name	isabelle-record
description	How to read constants and theorems generated by Isabelle record definitions

Reading Record Definitions

A record defines a named product type with named fields, selectors, updaters, and an extensible inheritance mechanism.

Constants

Example: record point = xcoord :: nat ycoord :: nat

Notation ⦇ xcoord = 3, ycoord = 5 ⦈ (written (| xcoord = 3, ycoord = 5 |) in ASCII) is a record literal — it constructs a point with the given field values.

• xcoord, ycoord — selectors (field accessors). xcoord ⦇ xcoord = 3, ycoord = 5 ⦈ = 3
• xcoord_update, ycoord_update — functional field updaters. xcoord_update f r returns a copy of r with the xcoord field replaced by f (xcoord r). Note: r ⦇ xcoord := 10 ⦈ is sugar for xcoord_update (λ_. 10) r.
• point.make — record constructor. point.make x y = ⦇ xcoord = x, ycoord = y ⦈

Theorems

• point.cases: (⋀xcoord ycoord. r = ⦇ xcoord = xcoord, ycoord = ycoord ⦈ ⟹ P) ⟹ P → For any point, there exist field values xcoord and ycoord such that the record is constructed from them (case analysis).

• point.induct: (⋀xcoord ycoord. P ⦇ xcoord = xcoord, ycoord = ycoord ⦈) ⟹ P r → To prove a property for all point records, it suffices to prove it for records constructed from arbitrary field values.

• point.splits: Elimination of quantifiers over records: (∀r. P r) = (∀xcoord ycoord. P ⦇ xcoord = xcoord, ycoord = ycoord ⦈) → A universal statement over all records can be replaced by a universal statement over all field values, which is useful to destruct a universally quantified record variable.

Record Inheritance

Example:

record point = xcoord :: nat  ycoord :: nat
record cpoint = point + color :: string

cpoint extends point: it has all parent fields (xcoord, ycoord) plus its own (color).

Inheritance works through a polymorphic extension slot called more, appended after the declared fields. A child record fills the parent's more slot with its own fields. Every record generates three types:

• 'm point_ext — a type that packages the fields together with a polymorphic more slot: 'm point_ext = ⦇ xcoord :: nat, ycoord :: nat, … :: 'm ⦈.

• 'm point_scheme abbreviates 'm point_ext

• point abbreviates unit point_ext — the concrete closed type, with more fixed to unit.

• 'm cpoint_ext holds only the new field: 'm cpoint_ext = ⦇ color :: string, … :: 'm ⦈.

• 'm cpoint_scheme abbreviates ('m cpoint_ext) point_ext — the full chain: xcoord, ycoord from point_ext, then color + open more from cpoint_ext, so cpoint can itself be further extended.

• cpoint abbreviates (unit cpoint_ext) point_ext — the closed version.

Parent selectors work on child records: xcoord can be applied to a cpoint because the types are compatible through the scheme mechanism.

Constants

• cpoint.make :: nat ⇒ nat ⇒ string ⇒ cpoint — construct from all fields (parent + own). cpoint.make x y c builds a cpoint with xcoord = x, ycoord = y, color = c
• cpoint.fields :: string ⇒ unit cpoint_ext — the extension fragment that cpoint adds on top of point, packaging only the fields declared by cpoint itself (here just color), excluding inherited fields.
• cpoint.extend :: cpoint ⇒ 'm ⇒ 'm cpoint_scheme — extend a cpoint with additional data via the more slot
• cpoint.truncate :: 'm cpoint_scheme ⇒ cpoint — strip the extension, closing the more slot with unit to yield a plain cpoint
• cpoint.more :: 'm cpoint_scheme ⇒ 'm — access the extension slot (the polymorphic "rest" of the record)
• cpoint.more_update :: ('m ⇒ 'm) ⇒ 'm cpoint_scheme ⇒ 'm cpoint_scheme — apply a function to the extension slot