1 (* Title: HOL/Record.thy |
1 (* Title: HOL/Record.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Wolfgang Naraschewski and Markus Wenzel, TU Muenchen |
3 Author: Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, TU Muenchen |
4 *) |
4 *) |
5 |
|
6 header {* Extensible records with structural subtyping *} |
|
7 |
5 |
8 theory Record = Product_Type |
6 theory Record = Product_Type |
9 files ("Tools/record_package.ML"): |
7 files ("Tools/record_package.ML"): |
10 |
8 |
|
9 ML {* |
|
10 val [h1, h2] = Goal "PROP Goal (\<And>x. PROP P x) \<Longrightarrow> (PROP P x \<Longrightarrow> PROP Q) \<Longrightarrow> PROP Q"; |
|
11 by (rtac h2 1); |
|
12 by (rtac (gen_all (h1 RS Drule.rev_triv_goal)) 1); |
|
13 qed "meta_allE"; |
|
14 *} |
11 |
15 |
12 subsection {* Abstract product types *} |
16 lemma prop_subst: "s = t \<Longrightarrow> PROP P t \<Longrightarrow> PROP P s" |
|
17 by simp |
13 |
18 |
14 locale product_type = |
19 lemma rec_UNIV_I: "\<And>x. x\<in>UNIV \<equiv> True" |
15 fixes Rep and Abs and pair and dest1 and dest2 |
20 by simp |
16 assumes "typedef": "type_definition Rep Abs UNIV" |
|
17 and pair: "pair == (\<lambda>a b. Abs (a, b))" |
|
18 and dest1: "dest1 == (\<lambda>p. fst (Rep p))" |
|
19 and dest2: "dest2 == (\<lambda>p. snd (Rep p))" |
|
20 |
21 |
21 lemma (in product_type) |
22 lemma rec_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P" |
22 "inject": "(pair x y = pair x' y') = (x = x' \<and> y = y')" |
23 by simp |
23 by (simp add: pair type_definition.Abs_inject [OF "typedef"]) |
|
24 |
|
25 lemma (in product_type) conv1: "dest1 (pair x y) = x" |
|
26 by (simp add: pair dest1 type_definition.Abs_inverse [OF "typedef"]) |
|
27 |
|
28 lemma (in product_type) conv2: "dest2 (pair x y) = y" |
|
29 by (simp add: pair dest2 type_definition.Abs_inverse [OF "typedef"]) |
|
30 |
|
31 lemma (in product_type) induct [induct type]: |
|
32 assumes hyp: "!!x y. P (pair x y)" |
|
33 shows "P p" |
|
34 proof (rule type_definition.Abs_induct [OF "typedef"]) |
|
35 fix q show "P (Abs q)" |
|
36 proof (induct q) |
|
37 fix x y have "P (pair x y)" by (rule hyp) |
|
38 also have "pair x y = Abs (x, y)" by (simp only: pair) |
|
39 finally show "P (Abs (x, y))" . |
|
40 qed |
|
41 qed |
|
42 |
|
43 lemma (in product_type) cases [cases type]: |
|
44 "(!!x y. p = pair x y ==> C) ==> C" |
|
45 by (induct p) (auto simp add: "inject") |
|
46 |
|
47 lemma (in product_type) surjective_pairing: |
|
48 "p = pair (dest1 p) (dest2 p)" |
|
49 by (induct p) (simp only: conv1 conv2) |
|
50 |
|
51 lemma (in product_type) split_paired_all: |
|
52 "(!!x. PROP P x) == (!!a b. PROP P (pair a b))" |
|
53 proof |
|
54 fix a b |
|
55 assume "!!x. PROP P x" |
|
56 thus "PROP P (pair a b)" . |
|
57 next |
|
58 fix x |
|
59 assume "!!a b. PROP P (pair a b)" |
|
60 hence "PROP P (pair (dest1 x) (dest2 x))" . |
|
61 thus "PROP P x" by (simp only: surjective_pairing [symmetric]) |
|
62 qed |
|
63 |
|
64 lemma (in product_type) split_paired_All: |
|
65 "(ALL x. P x) = (ALL a b. P (pair a b))" |
|
66 proof |
|
67 fix a b |
|
68 assume "ALL x. P x" |
|
69 thus "ALL a b. P (pair a b)" by rules |
|
70 next |
|
71 assume P: "ALL a b. P (pair a b)" |
|
72 show "ALL x. P x" |
|
73 proof |
|
74 fix x |
|
75 from P have "P (pair (dest1 x) (dest2 x))" by rules |
|
76 thus "P x" by (simp only: surjective_pairing [symmetric]) |
|
77 qed |
|
78 qed |
|
79 |
24 |
80 |
25 |
81 subsection {* Concrete record syntax *} |
26 subsection {* Concrete record syntax *} |
82 |
27 |
83 nonterminals |
28 nonterminals |
84 ident field_type field_types field fields update updates |
29 ident field_type field_types field fields update updates |
85 |
|
86 syntax |
30 syntax |
87 "_constify" :: "id => ident" ("_") |
31 "_constify" :: "id => ident" ("_") |
88 "_constify" :: "longid => ident" ("_") |
32 "_constify" :: "longid => ident" ("_") |
89 |
33 |
90 "_field_type" :: "[ident, type] => field_type" ("(2_ ::/ _)") |
34 "_field_type" :: "[ident, type] => field_type" ("(2_ ::/ _)") |
110 "_record_type_scheme" :: "[field_types, type] => type" ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)") |
54 "_record_type_scheme" :: "[field_types, type] => type" ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)") |
111 "_record" :: "fields => 'a" ("(3\<lparr>_\<rparr>)") |
55 "_record" :: "fields => 'a" ("(3\<lparr>_\<rparr>)") |
112 "_record_scheme" :: "[fields, 'a] => 'a" ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)") |
56 "_record_scheme" :: "[fields, 'a] => 'a" ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)") |
113 "_record_update" :: "['a, updates] => 'b" ("_/(3\<lparr>_\<rparr>)" [900,0] 900) |
57 "_record_update" :: "['a, updates] => 'b" ("_/(3\<lparr>_\<rparr>)" [900,0] 900) |
114 |
58 |
|
59 (* |
115 |
60 |
116 subsection {* Package setup *} |
61 "_structure" :: "fields => 'a" ("(3{| _ |})") |
|
62 "_structure_scheme" :: "[fields, 'a] => 'a" ("(3{| _,/ (2... =/ _) |})") |
|
63 |
|
64 "_structure_update_name":: idt |
|
65 "_structure_update" :: "['a, updates] \<Rightarrow> 'b" ("_/(3{| _ |})" [900,0] 900) |
117 |
66 |
118 use "Tools/record_package.ML" |
67 "_structure_type" :: "field_types => type" ("(3{| _ |})") |
119 setup RecordPackage.setup |
68 "_structure_type_scheme" :: "[field_types, type] => type" |
|
69 ("(3{| _,/ (2... ::/ _) |})") |
|
70 syntax (xsymbols) |
|
71 |
|
72 "_structure_scheme" :: "[fields, 'a] => 'a" ("(3{|_,/ (2\<dots> =/ _)|})") |
|
73 |
|
74 "_structure_type_scheme" :: "[field_types, type] => type" |
|
75 ("(3{|_,/ (2\<dots> ::/ _)|})") |
|
76 |
|
77 *) |
|
78 use "Tools/record_package.ML"; |
|
79 setup RecordPackage.setup; |
120 |
80 |
121 end |
81 end |
|
82 |