author | wenzelm |
Sun, 01 Mar 2009 14:45:23 +0100 | |
changeset 30186 | 1f836e949ac2 |
parent 25705 | 45a2ffc5911e |
child 31723 | f5cafe803b55 |
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$ |
16114 | 3 |
Author: Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, TU Muenchen |
4870
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 |
|
22817 | 6 |
header {* Extensible records with structural subtyping *} |
7 |
||
15131 | 8 |
theory Record |
15140 | 9 |
imports Product_Type |
16417 | 10 |
uses ("Tools/record_package.ML") |
15131 | 11 |
begin |
4870
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
12 |
|
14700
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
14080
diff
changeset
|
13 |
lemma prop_subst: "s = t \<Longrightarrow> PROP P t \<Longrightarrow> PROP P s" |
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
14080
diff
changeset
|
14 |
by simp |
11826 | 15 |
|
14700
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
14080
diff
changeset
|
16 |
lemma rec_UNIV_I: "\<And>x. x\<in>UNIV \<equiv> True" |
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
14080
diff
changeset
|
17 |
by simp |
11826 | 18 |
|
14700
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
14080
diff
changeset
|
19 |
lemma rec_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P" |
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
14080
diff
changeset
|
20 |
by simp |
14080
9a50427d7165
Added split_paired_All rule for splitting variables bound by
berghofe
parents:
13421
diff
changeset
|
21 |
|
25705 | 22 |
lemma K_record_comp: "(\<lambda>x. c) \<circ> f = (\<lambda>x. c)" |
23 |
by (simp add: comp_def) |
|
11821 | 24 |
|
22817 | 25 |
|
11833 | 26 |
subsection {* Concrete record syntax *} |
4870
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
27 |
|
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
28 |
nonterminals |
5198 | 29 |
ident field_type field_types field fields update updates |
4870
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
30 |
syntax |
11821 | 31 |
"_constify" :: "id => ident" ("_") |
32 |
"_constify" :: "longid => ident" ("_") |
|
5198 | 33 |
|
11821 | 34 |
"_field_type" :: "[ident, type] => field_type" ("(2_ ::/ _)") |
35 |
"" :: "field_type => field_types" ("_") |
|
36 |
"_field_types" :: "[field_type, field_types] => field_types" ("_,/ _") |
|
37 |
"_record_type" :: "field_types => type" ("(3'(| _ |'))") |
|
10093 | 38 |
"_record_type_scheme" :: "[field_types, type] => type" ("(3'(| _,/ (2... ::/ _) |'))") |
5198 | 39 |
|
11821 | 40 |
"_field" :: "[ident, 'a] => field" ("(2_ =/ _)") |
41 |
"" :: "field => fields" ("_") |
|
42 |
"_fields" :: "[field, fields] => fields" ("_,/ _") |
|
43 |
"_record" :: "fields => 'a" ("(3'(| _ |'))") |
|
10093 | 44 |
"_record_scheme" :: "[fields, 'a] => 'a" ("(3'(| _,/ (2... =/ _) |'))") |
5198 | 45 |
|
10641 | 46 |
"_update_name" :: idt |
11821 | 47 |
"_update" :: "[ident, 'a] => update" ("(2_ :=/ _)") |
48 |
"" :: "update => updates" ("_") |
|
49 |
"_updates" :: "[update, updates] => updates" ("_,/ _") |
|
10093 | 50 |
"_record_update" :: "['a, updates] => 'b" ("_/(3'(| _ |'))" [900,0] 900) |
4870
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
51 |
|
10331 | 52 |
syntax (xsymbols) |
11821 | 53 |
"_record_type" :: "field_types => type" ("(3\<lparr>_\<rparr>)") |
10093 | 54 |
"_record_type_scheme" :: "[field_types, type] => type" ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)") |
55 |
"_record" :: "fields => 'a" ("(3\<lparr>_\<rparr>)") |
|
56 |
"_record_scheme" :: "[fields, 'a] => 'a" ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)") |
|
57 |
"_record_update" :: "['a, updates] => 'b" ("_/(3\<lparr>_\<rparr>)" [900,0] 900) |
|
9729 | 58 |
|
16114 | 59 |
use "Tools/record_package.ML" |
60 |
setup RecordPackage.setup |
|
10641 | 61 |
|
4870
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
62 |
end |