src/HOL/Record.thy
author wenzelm
Wed Oct 17 20:24:37 2001 +0200 (2001-10-17)
changeset 11821 ad32c92435db
parent 11489 1fd5469c195e
child 11826 2203c7f9ec40
permissions -rw-r--r--
abstract product types;
     1 (*  Title:      HOL/Record.thy
     2     ID:         $Id$
     3     Author:     Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
     4 *)
     5 
     6 header {* Extensible records with structural subtyping *}
     7 
     8 theory Record = Datatype
     9 files ("Tools/record_package.ML"):
    10 
    11 
    12 subsection {* Abstract product types *}
    13 
    14 constdefs
    15   product_type :: "('p => 'a * 'b) => ('a * 'b => 'p) =>
    16     ('a => 'b => 'p) => (('a => 'b => 'c) => 'p => 'c) => bool"
    17   "product_type Rep Abs intro elim ==
    18     type_definition Rep Abs UNIV \<and>
    19     intro = (\<lambda>a b. Abs (a, b)) \<and>
    20     elim = (\<lambda>f. prod_case f o Rep)"
    21 
    22 lemma product_typeI:
    23   "type_definition Rep Abs A ==> A == UNIV ==>
    24     intro == \<lambda>a b. Abs (a, b) ==> elim == \<lambda>f. prod_case f o Rep ==>
    25     product_type Rep Abs intro elim"
    26   by (simp add: product_type_def)
    27 
    28 lemma product_type_typedef:
    29     "product_type Rep Abs intro elim ==> type_definition Rep Abs UNIV"
    30   by (unfold product_type_def) blast
    31 
    32 lemma product_type_intro:
    33     "product_type Rep Abs intro elim ==> intro = (\<lambda>a b. Abs (a, b))"
    34   by (unfold product_type_def) blast
    35 
    36 lemma product_type_elim:
    37     "product_type Rep Abs intro elim ==> elim = (\<lambda>f. prod_case f o Rep)"
    38   by (unfold product_type_def) fast  (* FIXME blast fails!? *)
    39 
    40 lemma product_type_inject:
    41   "product_type Rep Abs intro elim ==>
    42     (intro x y = intro x' y') = (x = x' \<and> y = y')"
    43 proof -
    44   case rule_context
    45   show ?thesis
    46     by (simp add: product_type_intro [OF rule_context]
    47       Abs_inject [OF product_type_typedef [OF rule_context]])
    48 qed
    49 
    50 lemma product_type_surject:
    51   "product_type Rep Abs intro elim ==>
    52     elim f (intro x y) = f x y"
    53 proof -
    54   case rule_context
    55   show ?thesis
    56     by (simp add: product_type_intro [OF rule_context]
    57       product_type_elim [OF rule_context]
    58       Abs_inverse [OF product_type_typedef [OF rule_context]])
    59 qed
    60 
    61 lemma product_type_induct:
    62   "product_type Rep Abs intro elim ==>
    63     (!!x y. P (intro x y)) ==> P p"
    64 proof -
    65   assume hyp: "!!x y. P (intro x y)"
    66   assume prod_type: "product_type Rep Abs intro elim"
    67   show "P p"
    68   proof (rule Abs_induct [OF product_type_typedef [OF prod_type]])
    69     fix pair show "P (Abs pair)"
    70     proof (rule prod.induct)
    71       fix x y from hyp show "P (Abs (x, y))"
    72 	by (simp only: product_type_intro [OF prod_type])
    73     qed
    74   qed
    75 qed
    76 
    77 
    78 text {* \medskip Type class for record extensions. *}
    79 
    80 axclass more < "term"
    81 instance unit :: more ..
    82 
    83 
    84 subsection {* Concrete syntax of records *}
    85 
    86 nonterminals
    87   ident field_type field_types field fields update updates
    88 
    89 syntax
    90   "_constify"           :: "id => ident"                        ("_")
    91   "_constify"           :: "longid => ident"                    ("_")
    92 
    93   "_field_type"         :: "[ident, type] => field_type"        ("(2_ ::/ _)")
    94   ""                    :: "field_type => field_types"          ("_")
    95   "_field_types"        :: "[field_type, field_types] => field_types"    ("_,/ _")
    96   "_record_type"        :: "field_types => type"                ("(3'(| _ |'))")
    97   "_record_type_scheme" :: "[field_types, type] => type"        ("(3'(| _,/ (2... ::/ _) |'))")
    98 
    99   "_field"              :: "[ident, 'a] => field"               ("(2_ =/ _)")
   100   ""                    :: "field => fields"                    ("_")
   101   "_fields"             :: "[field, fields] => fields"          ("_,/ _")
   102   "_record"             :: "fields => 'a"                       ("(3'(| _ |'))")
   103   "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3'(| _,/ (2... =/ _) |'))")
   104 
   105   "_update_name"        :: idt
   106   "_update"             :: "[ident, 'a] => update"              ("(2_ :=/ _)")
   107   ""                    :: "update => updates"                  ("_")
   108   "_updates"            :: "[update, updates] => updates"       ("_,/ _")
   109   "_record_update"      :: "['a, updates] => 'b"                ("_/(3'(| _ |'))" [900,0] 900)
   110 
   111 syntax (xsymbols)
   112   "_record_type"        :: "field_types => type"                ("(3\<lparr>_\<rparr>)")
   113   "_record_type_scheme" :: "[field_types, type] => type"        ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
   114   "_record"             :: "fields => 'a"                               ("(3\<lparr>_\<rparr>)")
   115   "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
   116   "_record_update"      :: "['a, updates] => 'b"                ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
   117 
   118 
   119 subsection {* Package setup *}
   120 
   121 use "Tools/record_package.ML"
   122 
   123 parse_translation {*
   124   let
   125     fun update_name_tr (Free (x, T) :: ts) =
   126           Term.list_comb (Free (suffix RecordPackage.updateN x, T), ts)
   127       | update_name_tr (Const (x, T) :: ts) =
   128           Term.list_comb (Const (suffix RecordPackage.updateN x, T), ts)
   129       | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
   130           Term.list_comb (c $ update_name_tr [t] $
   131             (Syntax.const "fun" $ ty $ Syntax.const "dummy"), ts)
   132       | update_name_tr ts = raise TERM ("update_name_tr", ts);
   133   in [("_update_name", update_name_tr)] end
   134 *}
   135 
   136 setup RecordPackage.setup
   137 
   138 end