author | Manuel Eberl <eberlm@in.tum.de> |
Fri, 29 Mar 2024 19:28:59 +0100 | |
changeset 80061 | 4c1347e172b1 |
parent 69913 | ca515cf61651 |
permissions | -rw-r--r-- |
67618
3107dcea3493
features and caveats of datatype_record
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
1 |
(* Title: HOL/Library/Datatype_Records.thy |
3107dcea3493
features and caveats of datatype_record
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
2 |
Author: Lars Hupel |
3107dcea3493
features and caveats of datatype_record
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
3 |
*) |
3107dcea3493
features and caveats of datatype_record
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
4 |
|
67611
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
5 |
section \<open>Records based on BNF/datatype machinery\<close> |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
6 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
7 |
theory Datatype_Records |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
8 |
imports Main |
69913 | 9 |
keywords "datatype_record" :: thy_defn |
67611
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
10 |
begin |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
11 |
|
67618
3107dcea3493
features and caveats of datatype_record
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
12 |
text \<open> |
3107dcea3493
features and caveats of datatype_record
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
13 |
This theory provides an alternative, stripped-down implementation of records based on the |
3107dcea3493
features and caveats of datatype_record
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
14 |
machinery of the @{command datatype} package. |
3107dcea3493
features and caveats of datatype_record
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
15 |
|
3107dcea3493
features and caveats of datatype_record
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
16 |
It supports: |
3107dcea3493
features and caveats of datatype_record
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
17 |
\<^item> similar declaration syntax as records |
3107dcea3493
features and caveats of datatype_record
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
18 |
\<^item> record creation and update syntax (using \<open>\<lparr> ... \<rparr>\<close> brackets) |
3107dcea3493
features and caveats of datatype_record
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
19 |
\<^item> regular datatype features (e.g. dead type variables etc.) |
3107dcea3493
features and caveats of datatype_record
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
20 |
\<^item> ``after-the-fact'' registration of single-free-constructor types as records |
3107dcea3493
features and caveats of datatype_record
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
21 |
\<close> |
3107dcea3493
features and caveats of datatype_record
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
22 |
|
3107dcea3493
features and caveats of datatype_record
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
23 |
text \<open> |
3107dcea3493
features and caveats of datatype_record
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
24 |
Caveats: |
3107dcea3493
features and caveats of datatype_record
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
25 |
\<^item> there is no compatibility layer; importing this theory will disrupt existing syntax |
3107dcea3493
features and caveats of datatype_record
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
26 |
\<^item> extensible records are not supported |
3107dcea3493
features and caveats of datatype_record
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
27 |
\<close> |
3107dcea3493
features and caveats of datatype_record
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
28 |
|
67611
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
29 |
no_syntax |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
30 |
"_constify" :: "id => ident" ("_") |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
31 |
"_constify" :: "longid => ident" ("_") |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
32 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
33 |
"_field_type" :: "ident => type => field_type" ("(2_ ::/ _)") |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
34 |
"" :: "field_type => field_types" ("_") |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
35 |
"_field_types" :: "field_type => field_types => field_types" ("_,/ _") |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
36 |
"_record_type" :: "field_types => type" ("(3\<lparr>_\<rparr>)") |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
37 |
"_record_type_scheme" :: "field_types => type => type" ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)") |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
38 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
39 |
"_field" :: "ident => 'a => field" ("(2_ =/ _)") |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
40 |
"" :: "field => fields" ("_") |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
41 |
"_fields" :: "field => fields => fields" ("_,/ _") |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
42 |
"_record" :: "fields => 'a" ("(3\<lparr>_\<rparr>)") |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
43 |
"_record_scheme" :: "fields => 'a => 'a" ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)") |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
44 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
45 |
"_field_update" :: "ident => 'a => field_update" ("(2_ :=/ _)") |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
46 |
"" :: "field_update => field_updates" ("_") |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
47 |
"_field_updates" :: "field_update => field_updates => field_updates" ("_,/ _") |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
48 |
"_record_update" :: "'a => field_updates => 'b" ("_/(3\<lparr>_\<rparr>)" [900, 0] 900) |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
49 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
50 |
no_syntax (ASCII) |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
51 |
"_record_type" :: "field_types => type" ("(3'(| _ |'))") |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
52 |
"_record_type_scheme" :: "field_types => type => type" ("(3'(| _,/ (2... ::/ _) |'))") |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
53 |
"_record" :: "fields => 'a" ("(3'(| _ |'))") |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
54 |
"_record_scheme" :: "fields => 'a => 'a" ("(3'(| _,/ (2... =/ _) |'))") |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
55 |
"_record_update" :: "'a => field_updates => 'b" ("_/(3'(| _ |'))" [900, 0] 900) |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
56 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
57 |
(* copied and adapted from Record.thy *) |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
58 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
59 |
nonterminal |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
60 |
field and |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
61 |
fields and |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
62 |
field_update and |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
63 |
field_updates |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
64 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
65 |
syntax |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
66 |
"_constify" :: "id => ident" ("_") |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
67 |
"_constify" :: "longid => ident" ("_") |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
68 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
69 |
"_datatype_field" :: "ident => 'a => field" ("(2_ =/ _)") |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
70 |
"" :: "field => fields" ("_") |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
71 |
"_datatype_fields" :: "field => fields => fields" ("_,/ _") |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
72 |
"_datatype_record" :: "fields => 'a" ("(3\<lparr>_\<rparr>)") |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
73 |
"_datatype_field_update" :: "ident => 'a => field_update" ("(2_ :=/ _)") |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
74 |
"" :: "field_update => field_updates" ("_") |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
75 |
"_datatype_field_updates" :: "field_update => field_updates => field_updates" ("_,/ _") |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
76 |
"_datatype_record_update" :: "'a => field_updates => 'b" ("_/(3\<lparr>_\<rparr>)" [900, 0] 900) |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
77 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
78 |
syntax (ASCII) |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
79 |
"_datatype_record" :: "fields => 'a" ("(3'(| _ |'))") |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
80 |
"_datatype_record_scheme" :: "fields => 'a => 'a" ("(3'(| _,/ (2... =/ _) |'))") |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
81 |
"_datatype_record_update" :: "'a => field_updates => 'b" ("_/(3'(| _ |'))" [900, 0] 900) |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
82 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
83 |
named_theorems datatype_record_update |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
84 |
|
69605 | 85 |
ML_file \<open>datatype_records.ML\<close> |
67611
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
86 |
setup \<open>Datatype_Records.setup\<close> |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
87 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
88 |
end |