author | wenzelm |
Fri, 26 Oct 2001 23:58:21 +0200 | |
changeset 11952 | b10f1e8862f4 |
parent 11833 | 475f772ab643 |
child 11956 | b814360b0267 |
permissions | -rw-r--r-- |
4870
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
1 |
(* Title: HOL/Record.thy |
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
3 |
Author: Wolfgang Naraschewski and Markus Wenzel, TU Muenchen |
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
4 |
*) |
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
5 |
|
11821 | 6 |
header {* Extensible records with structural subtyping *} |
7 |
||
11826 | 8 |
theory Record = Product_Type |
11821 | 9 |
files ("Tools/record_package.ML"): |
4870
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
10 |
|
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
11 |
|
11821 | 12 |
subsection {* Abstract product types *} |
13 |
||
14 |
constdefs |
|
15 |
product_type :: "('p => 'a * 'b) => ('a * 'b => 'p) => |
|
11833 | 16 |
('a => 'b => 'p) => ('p => 'a) => ('p => 'b) => bool" |
11826 | 17 |
"product_type Rep Abs pair dest1 dest2 == |
11821 | 18 |
type_definition Rep Abs UNIV \<and> |
11826 | 19 |
pair = (\<lambda>a b. Abs (a, b)) \<and> |
20 |
dest1 = (\<lambda>p. fst (Rep p)) \<and> |
|
21 |
dest2 = (\<lambda>p. snd (Rep p))" |
|
11821 | 22 |
|
23 |
lemma product_typeI: |
|
11826 | 24 |
"type_definition Rep Abs UNIV ==> |
25 |
pair == \<lambda>a b. Abs (a, b) ==> |
|
11833 | 26 |
dest1 == (\<lambda>p. fst (Rep p)) ==> |
27 |
dest2 == (\<lambda>p. snd (Rep p)) ==> |
|
11826 | 28 |
product_type Rep Abs pair dest1 dest2" |
11821 | 29 |
by (simp add: product_type_def) |
30 |
||
31 |
lemma product_type_typedef: |
|
11826 | 32 |
"product_type Rep Abs pair dest1 dest2 ==> type_definition Rep Abs UNIV" |
11821 | 33 |
by (unfold product_type_def) blast |
34 |
||
11826 | 35 |
lemma product_type_pair: |
36 |
"product_type Rep Abs pair dest1 dest2 ==> pair a b = Abs (a, b)" |
|
37 |
by (unfold product_type_def) blast |
|
38 |
||
39 |
lemma product_type_dest1: |
|
40 |
"product_type Rep Abs pair dest1 dest2 ==> dest1 p = fst (Rep p)" |
|
11821 | 41 |
by (unfold product_type_def) blast |
42 |
||
11826 | 43 |
lemma product_type_dest2: |
44 |
"product_type Rep Abs pair dest1 dest2 ==> dest2 p = snd (Rep p)" |
|
45 |
by (unfold product_type_def) blast |
|
46 |
||
11821 | 47 |
|
11826 | 48 |
theorem product_type_inject: |
49 |
"product_type Rep Abs pair dest1 dest2 ==> |
|
50 |
(pair x y = pair x' y') = (x = x' \<and> y = y')" |
|
51 |
proof - |
|
52 |
case rule_context |
|
53 |
show ?thesis |
|
54 |
by (simp add: product_type_pair [OF rule_context] |
|
55 |
Abs_inject [OF product_type_typedef [OF rule_context]]) |
|
56 |
qed |
|
57 |
||
58 |
theorem product_type_conv1: |
|
59 |
"product_type Rep Abs pair dest1 dest2 ==> dest1 (pair x y) = x" |
|
11821 | 60 |
proof - |
61 |
case rule_context |
|
62 |
show ?thesis |
|
11826 | 63 |
by (simp add: product_type_pair [OF rule_context] |
64 |
product_type_dest1 [OF rule_context] |
|
65 |
Abs_inverse [OF product_type_typedef [OF rule_context]]) |
|
11821 | 66 |
qed |
67 |
||
11826 | 68 |
theorem product_type_conv2: |
69 |
"product_type Rep Abs pair dest1 dest2 ==> dest2 (pair x y) = y" |
|
11821 | 70 |
proof - |
71 |
case rule_context |
|
72 |
show ?thesis |
|
11826 | 73 |
by (simp add: product_type_pair [OF rule_context] |
74 |
product_type_dest2 [OF rule_context] |
|
11821 | 75 |
Abs_inverse [OF product_type_typedef [OF rule_context]]) |
76 |
qed |
|
77 |
||
11826 | 78 |
theorem product_type_induct [induct set: product_type]: |
79 |
"product_type Rep Abs pair dest1 dest2 ==> |
|
80 |
(!!x y. P (pair x y)) ==> P p" |
|
11821 | 81 |
proof - |
11826 | 82 |
assume hyp: "!!x y. P (pair x y)" |
83 |
assume prod_type: "product_type Rep Abs pair dest1 dest2" |
|
11821 | 84 |
show "P p" |
85 |
proof (rule Abs_induct [OF product_type_typedef [OF prod_type]]) |
|
86 |
fix pair show "P (Abs pair)" |
|
11826 | 87 |
proof (rule prod_induct) |
11821 | 88 |
fix x y from hyp show "P (Abs (x, y))" |
11826 | 89 |
by (simp only: product_type_pair [OF prod_type]) |
11821 | 90 |
qed |
91 |
qed |
|
92 |
qed |
|
93 |
||
11826 | 94 |
theorem product_type_cases [cases set: product_type]: |
95 |
"product_type Rep Abs pair dest1 dest2 ==> |
|
11833 | 96 |
(!!x y. p = pair x y ==> C) ==> C" |
11826 | 97 |
proof - |
98 |
assume prod_type: "product_type Rep Abs pair dest1 dest2" |
|
11833 | 99 |
assume "!!x y. p = pair x y ==> C" |
11826 | 100 |
with prod_type show C |
101 |
by (induct p) (simp only: product_type_inject [OF prod_type], blast) |
|
102 |
qed |
|
103 |
||
104 |
theorem product_type_surjective_pairing: |
|
105 |
"product_type Rep Abs pair dest1 dest2 ==> |
|
106 |
p = pair (dest1 p) (dest2 p)" |
|
107 |
proof - |
|
108 |
case rule_context |
|
109 |
thus ?thesis by (induct p) |
|
110 |
(simp add: product_type_conv1 [OF rule_context] product_type_conv2 [OF rule_context]) |
|
111 |
qed |
|
112 |
||
113 |
theorem product_type_split_paired_all: |
|
114 |
"product_type Rep Abs pair dest1 dest2 ==> |
|
11833 | 115 |
(!!x. PROP P x) == (!!a b. PROP P (pair a b))" |
11826 | 116 |
proof |
117 |
fix a b |
|
118 |
assume "!!x. PROP P x" |
|
119 |
thus "PROP P (pair a b)" . |
|
120 |
next |
|
121 |
case rule_context |
|
122 |
fix x |
|
123 |
assume "!!a b. PROP P (pair a b)" |
|
124 |
hence "PROP P (pair (dest1 x) (dest2 x))" . |
|
125 |
thus "PROP P x" by (simp only: product_type_surjective_pairing [OF rule_context, symmetric]) |
|
126 |
qed |
|
127 |
||
11821 | 128 |
|
11833 | 129 |
subsection {* Type class for record extensions *} |
11821 | 130 |
|
131 |
axclass more < "term" |
|
132 |
instance unit :: more .. |
|
133 |
||
134 |
||
11833 | 135 |
subsection {* Concrete record syntax *} |
4870
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
136 |
|
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
137 |
nonterminals |
5198 | 138 |
ident field_type field_types field fields update updates |
4870
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
139 |
|
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
140 |
syntax |
11821 | 141 |
"_constify" :: "id => ident" ("_") |
142 |
"_constify" :: "longid => ident" ("_") |
|
5198 | 143 |
|
11821 | 144 |
"_field_type" :: "[ident, type] => field_type" ("(2_ ::/ _)") |
145 |
"" :: "field_type => field_types" ("_") |
|
146 |
"_field_types" :: "[field_type, field_types] => field_types" ("_,/ _") |
|
147 |
"_record_type" :: "field_types => type" ("(3'(| _ |'))") |
|
10093 | 148 |
"_record_type_scheme" :: "[field_types, type] => type" ("(3'(| _,/ (2... ::/ _) |'))") |
5198 | 149 |
|
11821 | 150 |
"_field" :: "[ident, 'a] => field" ("(2_ =/ _)") |
151 |
"" :: "field => fields" ("_") |
|
152 |
"_fields" :: "[field, fields] => fields" ("_,/ _") |
|
153 |
"_record" :: "fields => 'a" ("(3'(| _ |'))") |
|
10093 | 154 |
"_record_scheme" :: "[fields, 'a] => 'a" ("(3'(| _,/ (2... =/ _) |'))") |
5198 | 155 |
|
10641 | 156 |
"_update_name" :: idt |
11821 | 157 |
"_update" :: "[ident, 'a] => update" ("(2_ :=/ _)") |
158 |
"" :: "update => updates" ("_") |
|
159 |
"_updates" :: "[update, updates] => updates" ("_,/ _") |
|
10093 | 160 |
"_record_update" :: "['a, updates] => 'b" ("_/(3'(| _ |'))" [900,0] 900) |
4870
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
161 |
|
10331 | 162 |
syntax (xsymbols) |
11821 | 163 |
"_record_type" :: "field_types => type" ("(3\<lparr>_\<rparr>)") |
10093 | 164 |
"_record_type_scheme" :: "[field_types, type] => type" ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)") |
165 |
"_record" :: "fields => 'a" ("(3\<lparr>_\<rparr>)") |
|
166 |
"_record_scheme" :: "[fields, 'a] => 'a" ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)") |
|
167 |
"_record_update" :: "['a, updates] => 'b" ("_/(3\<lparr>_\<rparr>)" [900,0] 900) |
|
9729 | 168 |
|
11833 | 169 |
|
170 |
subsection {* Package setup *} |
|
171 |
||
172 |
use "Tools/record_package.ML" |
|
173 |
setup RecordPackage.setup |
|
10641 | 174 |
|
4870
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
175 |
end |