--- a/src/HOL/Record.thy Wed Oct 17 20:24:03 2001 +0200
+++ b/src/HOL/Record.thy Wed Oct 17 20:24:37 2001 +0200
@@ -1,53 +1,125 @@
(* Title: HOL/Record.thy
ID: $Id$
Author: Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
-
-Extensible records with structural subtyping in HOL. See
-Tools/record_package.ML for the actual implementation.
*)
+header {* Extensible records with structural subtyping *}
+
theory Record = Datatype
-files "Tools/record_package.ML":
+files ("Tools/record_package.ML"):
-(* concrete syntax *)
+subsection {* Abstract product types *}
+
+constdefs
+ product_type :: "('p => 'a * 'b) => ('a * 'b => 'p) =>
+ ('a => 'b => 'p) => (('a => 'b => 'c) => 'p => 'c) => bool"
+ "product_type Rep Abs intro elim ==
+ type_definition Rep Abs UNIV \<and>
+ intro = (\<lambda>a b. Abs (a, b)) \<and>
+ elim = (\<lambda>f. prod_case f o Rep)"
+
+lemma product_typeI:
+ "type_definition Rep Abs A ==> A == UNIV ==>
+ intro == \<lambda>a b. Abs (a, b) ==> elim == \<lambda>f. prod_case f o Rep ==>
+ product_type Rep Abs intro elim"
+ by (simp add: product_type_def)
+
+lemma product_type_typedef:
+ "product_type Rep Abs intro elim ==> type_definition Rep Abs UNIV"
+ by (unfold product_type_def) blast
+
+lemma product_type_intro:
+ "product_type Rep Abs intro elim ==> intro = (\<lambda>a b. Abs (a, b))"
+ by (unfold product_type_def) blast
+
+lemma product_type_elim:
+ "product_type Rep Abs intro elim ==> elim = (\<lambda>f. prod_case f o Rep)"
+ by (unfold product_type_def) fast (* FIXME blast fails!? *)
+
+lemma product_type_inject:
+ "product_type Rep Abs intro elim ==>
+ (intro x y = intro x' y') = (x = x' \<and> y = y')"
+proof -
+ case rule_context
+ show ?thesis
+ by (simp add: product_type_intro [OF rule_context]
+ Abs_inject [OF product_type_typedef [OF rule_context]])
+qed
+
+lemma product_type_surject:
+ "product_type Rep Abs intro elim ==>
+ elim f (intro x y) = f x y"
+proof -
+ case rule_context
+ show ?thesis
+ by (simp add: product_type_intro [OF rule_context]
+ product_type_elim [OF rule_context]
+ Abs_inverse [OF product_type_typedef [OF rule_context]])
+qed
+
+lemma product_type_induct:
+ "product_type Rep Abs intro elim ==>
+ (!!x y. P (intro x y)) ==> P p"
+proof -
+ assume hyp: "!!x y. P (intro x y)"
+ assume prod_type: "product_type Rep Abs intro elim"
+ show "P p"
+ proof (rule Abs_induct [OF product_type_typedef [OF prod_type]])
+ fix pair show "P (Abs pair)"
+ proof (rule prod.induct)
+ fix x y from hyp show "P (Abs (x, y))"
+ by (simp only: product_type_intro [OF prod_type])
+ qed
+ qed
+qed
+
+
+text {* \medskip Type class for record extensions. *}
+
+axclass more < "term"
+instance unit :: more ..
+
+
+subsection {* Concrete syntax of records *}
nonterminals
ident field_type field_types field fields update updates
syntax
- (*field names*)
- "_constify" :: "id => ident" ("_")
- "_constify" :: "longid => ident" ("_")
+ "_constify" :: "id => ident" ("_")
+ "_constify" :: "longid => ident" ("_")
- (*record types*)
- "_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'(| _ |'))")
+ "_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... ::/ _) |'))")
- (*records*)
- "_field" :: "[ident, 'a] => field" ("(2_ =/ _)")
- "" :: "field => fields" ("_")
- "_fields" :: "[field, fields] => fields" ("_,/ _")
- "_record" :: "fields => 'a" ("(3'(| _ |'))")
+ "_field" :: "[ident, 'a] => field" ("(2_ =/ _)")
+ "" :: "field => fields" ("_")
+ "_fields" :: "[field, fields] => fields" ("_,/ _")
+ "_record" :: "fields => 'a" ("(3'(| _ |'))")
"_record_scheme" :: "[fields, 'a] => 'a" ("(3'(| _,/ (2... =/ _) |'))")
- (*record updates*)
"_update_name" :: idt
- "_update" :: "[ident, 'a] => update" ("(2_ :=/ _)")
- "" :: "update => updates" ("_")
- "_updates" :: "[update, updates] => updates" ("_,/ _")
+ "_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" :: "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 {* Package setup *}
+
+use "Tools/record_package.ML"
+
parse_translation {*
let
fun update_name_tr (Free (x, T) :: ts) =
@@ -61,17 +133,6 @@
in [("_update_name", update_name_tr)] end
*}
-
-(* type class for record extensions *)
-
-axclass more < "term"
-instance unit :: more ..
-
-
-(* initialize the package *)
-
-setup
- RecordPackage.setup
-
+setup RecordPackage.setup
end