src/HOL/Record.thy

Fix unescaped expressions breaking latex output in Record.thy

Expressions containing _ and ^ need to be adjusted or antiquoted in
text comments for latex compatibility. This is in fact a little
annoying, since it makes the comment less readable in both source
and HTML form.

(*  Title:      HOL/Record.thy
    Authors:    Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, TU Muenchen
                Thomas Sewell, NICTA
*)

header {* Extensible records with structural subtyping *}

theory Record
imports Product_Type
uses ("Tools/record.ML")
begin

lemma prop_subst: "s = t \<Longrightarrow> PROP P t \<Longrightarrow> PROP P s"
  by simp

lemma K_record_comp: "(\<lambda>x. c) \<circ> f = (\<lambda>x. c)" 
  by (simp add: comp_def)

lemma meta_iffD2:
  "\<lbrakk> PROP P \<equiv> PROP Q; PROP Q \<rbrakk> \<Longrightarrow> PROP P"
  by simp

lemma o_eq_dest_lhs:
  "a o b = c \<Longrightarrow> a (b v) = c v"
  by clarsimp

lemma id_o_refl:
  "id o f = f o id"
  by simp

lemma o_eq_id_dest:
  "a o b = id o c \<Longrightarrow> a (b v) = c v"
  by clarsimp

subsection {* Concrete record syntax *}

nonterminals
  ident field_type field_types field fields update updates
syntax
  "_constify"           :: "id => ident"                        ("_")
  "_constify"           :: "longid => ident"                    ("_")

  "_field_type"         :: "[ident, type] => field_type"        ("(2_ ::/ _)")
  ""                    :: "field_type => field_types"          ("_")
  "_field_types"        :: "[field_type, field_types] => field_types"    ("_,/ _")
  "_record_type"        :: "field_types => type"                ("(3'(| _ |'))")
  "_record_type_scheme" :: "[field_types, type] => type"        ("(3'(| _,/ (2... ::/ _) |'))")

  "_field"              :: "[ident, 'a] => field"               ("(2_ =/ _)")
  ""                    :: "field => fields"                    ("_")
  "_fields"             :: "[field, fields] => fields"          ("_,/ _")
  "_record"             :: "fields => 'a"                       ("(3'(| _ |'))")
  "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3'(| _,/ (2... =/ _) |'))")

  "_update_name"        :: idt
  "_update"             :: "[ident, 'a] => update"              ("(2_ :=/ _)")
  ""                    :: "update => updates"                  ("_")
  "_updates"            :: "[update, updates] => updates"       ("_,/ _")
  "_record_update"      :: "['a, updates] => 'b"                ("_/(3'(| _ |'))" [900,0] 900)

syntax (xsymbols)
  "_record_type"        :: "field_types => type"                ("(3\<lparr>_\<rparr>)")
  "_record_type_scheme" :: "[field_types, type] => type"        ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
  "_record"             :: "fields => 'a"                               ("(3\<lparr>_\<rparr>)")
  "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
  "_record_update"      :: "['a, updates] => 'b"                ("_/(3\<lparr>_\<rparr>)" [900,0] 900)

subsection {* Operators and lemmas for types isomorphic to tuples *}

text {*
Records are isomorphic to compound tuple types. To implement efficient
records, we make this isomorphism explicit. Consider the record
access/update simplification @{text "alpha (beta_update f rec) = alpha rec"} for
distinct fields alpha and beta of some record rec with n fields. There
are @{text "n ^ 2"} such theorems, which prohibits storage of all of them for
large n. The rules can be proved on the fly by case decomposition and
simplification in O(n) time. By creating O(n) isomorphic-tuple types
while defining the record, however, we can prove the access/update
simplification in @{text "O(log(n)^2)"} time.

The O(n) cost of case decomposition is not because O(n) steps are taken,
but rather because the resulting rule must contain O(n) new variables and
an O(n) size concrete record construction. To sidestep this cost, we would
like to avoid case decomposition in proving access/update theorems.

Record types are defined as isomorphic to tuple types. For instance, a
record type with fields 'a, 'b, 'c and 'd might be introduced as
isomorphic to @{text "'a \<times> ('b \<times> ('c \<times> 'd))"}. If we balance the tuple tree to
@{text "('a \<times> 'b) \<times> ('c \<times> 'd)"} then accessors can be defined by converting to
the underlying type then using O(log(n)) fst or snd operations.
Updators can be defined similarly, if we introduce a @{text "fst_update"} and
@{text "snd_update"} function. Furthermore, we can prove the access/update
theorem in O(log(n)) steps by using simple rewrites on fst, snd,
@{text "fst_update"} and @{text "snd_update"}.

The catch is that, although O(log(n)) steps were taken, the underlying
type we converted to is a tuple tree of size O(n). Processing this term
type wastes performance. We avoid this for large n by taking each
subtree of size K and defining a new type isomorphic to that tuple
subtree. A record can now be defined as isomorphic to a tuple tree
of these O(n/K) new types, or, if @{text "n > K*K"}, we can repeat the process,
until the record can be defined in terms of a tuple tree of complexity
less than the constant K.

If we prove the access/update theorem on this type with the analagous
steps to the tuple tree, we consume @{text "O(log(n)^2)"} time as the intermediate
terms are O(log(n)) in size and the types needed have size bounded by K.
To enable this analagous traversal, we define the functions seen below:
@{text "istuple_fst"}, @{text "istuple_snd"}, @{text "istuple_fst_update"}
and @{text "istuple_snd_update"}. These functions generalise tuple
operations by taking a parameter that encapsulates a tuple isomorphism.
The rewrites needed on these functions now need an additional assumption
which is that the isomorphism works.

These rewrites are typically used in a structured way. They are here
presented as the introduction rule @{text "isomorphic_tuple.intros"} rather than
as a rewrite rule set. The introduction form is an optimisation, as net
matching can be performed at one term location for each step rather than
the simplifier searching the term for possible pattern matches. The rule
set is used as it is viewed outside the locale, with the locale assumption
(that the isomorphism is valid) left as a rule assumption. All rules are
structured to aid net matching, using either a point-free form or an
encapsulating predicate.
*}

typedef ('a, 'b, 'c) tuple_isomorphism
  = "UNIV :: (('a \<Rightarrow> ('b \<times> 'c)) \<times> (('b \<times> 'c) \<Rightarrow> 'a)) set"
  by simp

definition
  "TupleIsomorphism repr abst = Abs_tuple_isomorphism (repr, abst)"

definition
  istuple_fst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b"
where
 "istuple_fst isom \<equiv> let (repr, abst) = Rep_tuple_isomorphism isom in fst \<circ> repr"