5753
|
1 |
(* Title: HOL/ex/Points.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
|
5741
|
4 |
|
5753
|
5 |
Basic use of extensible records in HOL, including the famous points
|
|
6 |
and coloured points.
|
|
7 |
*)
|
|
8 |
|
|
9 |
Points = Main +
|
5741
|
10 |
|
|
11 |
|
5753
|
12 |
(** points **)
|
5741
|
13 |
|
|
14 |
record point =
|
|
15 |
x :: nat
|
|
16 |
y :: nat
|
|
17 |
|
5753
|
18 |
(*
|
|
19 |
To find out, which theorems are produced by the record declaration,
|
|
20 |
type the following commands:
|
|
21 |
|
|
22 |
thms "point.simps";
|
|
23 |
thms "point.iffs";
|
|
24 |
thms "point.update_defs";
|
|
25 |
|
|
26 |
The set of theorems "point.simps" is added automatically to the
|
|
27 |
standard simpset, "point.iffs" is added to the claset and simpset.
|
|
28 |
*)
|
5741
|
29 |
|
|
30 |
|
5753
|
31 |
(*
|
|
32 |
Record declarations define new type abbreviations:
|
|
33 |
|
|
34 |
point = (| x :: nat, y :: nat |)
|
|
35 |
'a point_scheme = (| x :: nat, y :: nat, ... :: 'a |)
|
|
36 |
|
|
37 |
Extensions `...' must be in type class `more'!
|
|
38 |
*)
|
5741
|
39 |
|
|
40 |
consts foo1 :: point
|
|
41 |
consts foo2 :: "(| x :: nat, y :: nat |)"
|
|
42 |
consts foo3 :: 'a => ('a::more) point_scheme
|
|
43 |
consts foo4 :: "'a => (| x :: nat, y :: nat, ... :: 'a |)"
|
|
44 |
|
|
45 |
|
5753
|
46 |
(* Introducing concrete records and record schemes *)
|
5741
|
47 |
|
5753
|
48 |
defs
|
5741
|
49 |
foo1_def "foo1 == (| x = 1, y = 0 |)"
|
|
50 |
foo3_def "foo3 ext == (| x = 1, y = 0, ... = ext |)"
|
|
51 |
|
|
52 |
|
5753
|
53 |
(* Record selection and record update *)
|
5741
|
54 |
|
5753
|
55 |
constdefs
|
5741
|
56 |
getX :: ('a::more) point_scheme => nat
|
|
57 |
"getX r == x r"
|
|
58 |
setX :: ('a::more) point_scheme => nat => 'a point_scheme
|
|
59 |
"setX r n == r (| x := n |)"
|
|
60 |
|
|
61 |
|
5753
|
62 |
(* concrete records are type instances of record schemes *)
|
5741
|
63 |
|
|
64 |
constdefs
|
|
65 |
foo5 :: nat
|
5753
|
66 |
"foo5 == getX (| x = 1, y = 0 |)"
|
5741
|
67 |
|
|
68 |
|
5753
|
69 |
(* manipulating the `...' (more-part) *)
|
5741
|
70 |
|
|
71 |
constdefs
|
|
72 |
incX :: ('a::more) point_scheme => 'a point_scheme
|
5753
|
73 |
"incX r == (| x = Suc (x r), y = y r, ... = point.more r |)"
|
5741
|
74 |
|
5753
|
75 |
(*alternative definition*)
|
5741
|
76 |
constdefs
|
|
77 |
incX' :: ('a::more) point_scheme => 'a point_scheme
|
|
78 |
"incX' r == r (| x := Suc (x r) |)"
|
|
79 |
|
|
80 |
|
|
81 |
|
5753
|
82 |
(** coloured points: record extension **)
|
5741
|
83 |
|
|
84 |
datatype colour = Red | Green | Blue
|
|
85 |
|
|
86 |
record cpoint = point +
|
|
87 |
colour :: colour
|
|
88 |
|
|
89 |
|
5753
|
90 |
(*
|
|
91 |
The record declaration defines new type constructors:
|
5741
|
92 |
|
5753
|
93 |
cpoint = (| x :: nat, y :: nat, colour :: colour |)
|
|
94 |
'a cpoint_scheme = (| x :: nat, y :: nat, colour :: colour, ... :: 'a |)
|
|
95 |
*)
|
5741
|
96 |
|
|
97 |
consts foo6 :: cpoint
|
|
98 |
consts foo7 :: "(| x :: nat, y :: nat, colour :: colour |)"
|
|
99 |
consts foo8 :: ('a::more) cpoint_scheme
|
|
100 |
consts foo9 :: "(| x :: nat, y :: nat, colour :: colour, ... :: 'a |)"
|
|
101 |
|
|
102 |
|
5753
|
103 |
(* functions on point schemes work for cpoints as well *)
|
5741
|
104 |
|
5753
|
105 |
constdefs
|
5741
|
106 |
foo10 :: nat
|
|
107 |
"foo10 == getX (| x = 2, y = 0, colour = Blue |)"
|
|
108 |
|
|
109 |
|
5753
|
110 |
(* non-coercive structural subtyping *)
|
5741
|
111 |
|
5753
|
112 |
(*foo11 has type cpoint, not type point*) (*Great!*)
|
|
113 |
constdefs
|
5741
|
114 |
foo11 :: cpoint
|
5753
|
115 |
"foo11 == setX (| x = 2, y = 0, colour = Blue |) 0"
|
5741
|
116 |
|
|
117 |
|
|
118 |
|
5753
|
119 |
(** other features **)
|
|
120 |
|
|
121 |
(* field names contribute to record identity *)
|
5741
|
122 |
|
|
123 |
record point' =
|
|
124 |
x' :: nat
|
|
125 |
y' :: nat
|
|
126 |
|
|
127 |
consts
|
|
128 |
foo12 :: nat
|
5753
|
129 |
(*"foo12 == getX (| x' = 2, y' = 0 |)"*) (*invalid*)
|
5741
|
130 |
|
|
131 |
|
5753
|
132 |
(* polymorphic records *)
|
5741
|
133 |
|
|
134 |
record 'a point'' = point +
|
|
135 |
content :: 'a
|
|
136 |
|
|
137 |
types cpoint'' = colour point''
|
|
138 |
|
|
139 |
|
|
140 |
|
5753
|
141 |
(*Have a lot of fun!*)
|
5741
|
142 |
|
|
143 |
end
|