src/HOL/Record.thy
changeset 11821 ad32c92435db
parent 11489 1fd5469c195e
child 11826 2203c7f9ec40
     1.1 --- a/src/HOL/Record.thy	Wed Oct 17 20:24:03 2001 +0200
     1.2 +++ b/src/HOL/Record.thy	Wed Oct 17 20:24:37 2001 +0200
     1.3 @@ -1,53 +1,125 @@
     1.4  (*  Title:      HOL/Record.thy
     1.5      ID:         $Id$
     1.6      Author:     Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
     1.7 -
     1.8 -Extensible records with structural subtyping in HOL.  See
     1.9 -Tools/record_package.ML for the actual implementation.
    1.10  *)
    1.11  
    1.12 +header {* Extensible records with structural subtyping *}
    1.13 +
    1.14  theory Record = Datatype
    1.15 -files "Tools/record_package.ML":
    1.16 +files ("Tools/record_package.ML"):
    1.17  
    1.18  
    1.19 -(* concrete syntax *)
    1.20 +subsection {* Abstract product types *}
    1.21 +
    1.22 +constdefs
    1.23 +  product_type :: "('p => 'a * 'b) => ('a * 'b => 'p) =>
    1.24 +    ('a => 'b => 'p) => (('a => 'b => 'c) => 'p => 'c) => bool"
    1.25 +  "product_type Rep Abs intro elim ==
    1.26 +    type_definition Rep Abs UNIV \<and>
    1.27 +    intro = (\<lambda>a b. Abs (a, b)) \<and>
    1.28 +    elim = (\<lambda>f. prod_case f o Rep)"
    1.29 +
    1.30 +lemma product_typeI:
    1.31 +  "type_definition Rep Abs A ==> A == UNIV ==>
    1.32 +    intro == \<lambda>a b. Abs (a, b) ==> elim == \<lambda>f. prod_case f o Rep ==>
    1.33 +    product_type Rep Abs intro elim"
    1.34 +  by (simp add: product_type_def)
    1.35 +
    1.36 +lemma product_type_typedef:
    1.37 +    "product_type Rep Abs intro elim ==> type_definition Rep Abs UNIV"
    1.38 +  by (unfold product_type_def) blast
    1.39 +
    1.40 +lemma product_type_intro:
    1.41 +    "product_type Rep Abs intro elim ==> intro = (\<lambda>a b. Abs (a, b))"
    1.42 +  by (unfold product_type_def) blast
    1.43 +
    1.44 +lemma product_type_elim:
    1.45 +    "product_type Rep Abs intro elim ==> elim = (\<lambda>f. prod_case f o Rep)"
    1.46 +  by (unfold product_type_def) fast  (* FIXME blast fails!? *)
    1.47 +
    1.48 +lemma product_type_inject:
    1.49 +  "product_type Rep Abs intro elim ==>
    1.50 +    (intro x y = intro x' y') = (x = x' \<and> y = y')"
    1.51 +proof -
    1.52 +  case rule_context
    1.53 +  show ?thesis
    1.54 +    by (simp add: product_type_intro [OF rule_context]
    1.55 +      Abs_inject [OF product_type_typedef [OF rule_context]])
    1.56 +qed
    1.57 +
    1.58 +lemma product_type_surject:
    1.59 +  "product_type Rep Abs intro elim ==>
    1.60 +    elim f (intro x y) = f x y"
    1.61 +proof -
    1.62 +  case rule_context
    1.63 +  show ?thesis
    1.64 +    by (simp add: product_type_intro [OF rule_context]
    1.65 +      product_type_elim [OF rule_context]
    1.66 +      Abs_inverse [OF product_type_typedef [OF rule_context]])
    1.67 +qed
    1.68 +
    1.69 +lemma product_type_induct:
    1.70 +  "product_type Rep Abs intro elim ==>
    1.71 +    (!!x y. P (intro x y)) ==> P p"
    1.72 +proof -
    1.73 +  assume hyp: "!!x y. P (intro x y)"
    1.74 +  assume prod_type: "product_type Rep Abs intro elim"
    1.75 +  show "P p"
    1.76 +  proof (rule Abs_induct [OF product_type_typedef [OF prod_type]])
    1.77 +    fix pair show "P (Abs pair)"
    1.78 +    proof (rule prod.induct)
    1.79 +      fix x y from hyp show "P (Abs (x, y))"
    1.80 +	by (simp only: product_type_intro [OF prod_type])
    1.81 +    qed
    1.82 +  qed
    1.83 +qed
    1.84 +
    1.85 +
    1.86 +text {* \medskip Type class for record extensions. *}
    1.87 +
    1.88 +axclass more < "term"
    1.89 +instance unit :: more ..
    1.90 +
    1.91 +
    1.92 +subsection {* Concrete syntax of records *}
    1.93  
    1.94  nonterminals
    1.95    ident field_type field_types field fields update updates
    1.96  
    1.97  syntax
    1.98 -  (*field names*)
    1.99 -  "_constify"           :: "id => ident"                                ("_")
   1.100 -  "_constify"           :: "longid => ident"                            ("_")
   1.101 +  "_constify"           :: "id => ident"                        ("_")
   1.102 +  "_constify"           :: "longid => ident"                    ("_")
   1.103  
   1.104 -  (*record types*)
   1.105 -  "_field_type"         :: "[ident, type] => field_type"                ("(2_ ::/ _)")
   1.106 -  ""                    :: "field_type => field_types"                  ("_")
   1.107 -  "_field_types"        :: "[field_type, field_types] => field_types"   ("_,/ _")
   1.108 -  "_record_type"        :: "field_types => type"                        ("(3'(| _ |'))")
   1.109 +  "_field_type"         :: "[ident, type] => field_type"        ("(2_ ::/ _)")
   1.110 +  ""                    :: "field_type => field_types"          ("_")
   1.111 +  "_field_types"        :: "[field_type, field_types] => field_types"    ("_,/ _")
   1.112 +  "_record_type"        :: "field_types => type"                ("(3'(| _ |'))")
   1.113    "_record_type_scheme" :: "[field_types, type] => type"        ("(3'(| _,/ (2... ::/ _) |'))")
   1.114  
   1.115 -  (*records*)
   1.116 -  "_field"              :: "[ident, 'a] => field"                       ("(2_ =/ _)")
   1.117 -  ""                    :: "field => fields"                            ("_")
   1.118 -  "_fields"             :: "[field, fields] => fields"                  ("_,/ _")
   1.119 -  "_record"             :: "fields => 'a"                               ("(3'(| _ |'))")
   1.120 +  "_field"              :: "[ident, 'a] => field"               ("(2_ =/ _)")
   1.121 +  ""                    :: "field => fields"                    ("_")
   1.122 +  "_fields"             :: "[field, fields] => fields"          ("_,/ _")
   1.123 +  "_record"             :: "fields => 'a"                       ("(3'(| _ |'))")
   1.124    "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3'(| _,/ (2... =/ _) |'))")
   1.125  
   1.126 -  (*record updates*)
   1.127    "_update_name"        :: idt
   1.128 -  "_update"             :: "[ident, 'a] => update"                      ("(2_ :=/ _)")
   1.129 -  ""                    :: "update => updates"                          ("_")
   1.130 -  "_updates"            :: "[update, updates] => updates"               ("_,/ _")
   1.131 +  "_update"             :: "[ident, 'a] => update"              ("(2_ :=/ _)")
   1.132 +  ""                    :: "update => updates"                  ("_")
   1.133 +  "_updates"            :: "[update, updates] => updates"       ("_,/ _")
   1.134    "_record_update"      :: "['a, updates] => 'b"                ("_/(3'(| _ |'))" [900,0] 900)
   1.135  
   1.136  syntax (xsymbols)
   1.137 -  "_record_type"        :: "field_types => type"                        ("(3\<lparr>_\<rparr>)")
   1.138 +  "_record_type"        :: "field_types => type"                ("(3\<lparr>_\<rparr>)")
   1.139    "_record_type_scheme" :: "[field_types, type] => type"        ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
   1.140    "_record"             :: "fields => 'a"                               ("(3\<lparr>_\<rparr>)")
   1.141    "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
   1.142    "_record_update"      :: "['a, updates] => 'b"                ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
   1.143  
   1.144 +
   1.145 +subsection {* Package setup *}
   1.146 +
   1.147 +use "Tools/record_package.ML"
   1.148 +
   1.149  parse_translation {*
   1.150    let
   1.151      fun update_name_tr (Free (x, T) :: ts) =
   1.152 @@ -61,17 +133,6 @@
   1.153    in [("_update_name", update_name_tr)] end
   1.154  *}
   1.155  
   1.156 -
   1.157 -(* type class for record extensions *)
   1.158 -
   1.159 -axclass more < "term"
   1.160 -instance unit :: more ..
   1.161 -
   1.162 -
   1.163 -(* initialize the package *)
   1.164 -
   1.165 -setup
   1.166 -  RecordPackage.setup
   1.167 -
   1.168 +setup RecordPackage.setup
   1.169  
   1.170  end