1 (* Title: HOL/Tools/Quotient/quotient_typ.thy |
|
2 Author: Cezary Kaliszyk and Christian Urban |
|
3 |
|
4 Definition of a quotient type. |
|
5 |
|
6 *) |
|
7 |
|
8 signature QUOTIENT_TYPE = |
|
9 sig |
|
10 val add_quotient_type: ((string list * binding * mixfix) * (typ * term)) * thm |
|
11 -> Proof.context -> (thm * thm) * local_theory |
|
12 |
|
13 val quotient_type: ((string list * binding * mixfix) * (typ * term)) list |
|
14 -> Proof.context -> Proof.state |
|
15 |
|
16 val quotient_type_cmd: ((((string list * binding) * mixfix) * string) * string) list |
|
17 -> Proof.context -> Proof.state |
|
18 end; |
|
19 |
|
20 structure Quotient_Type: QUOTIENT_TYPE = |
|
21 struct |
|
22 |
|
23 open Quotient_Info; |
|
24 |
|
25 (* wrappers for define, note, Attrib.internal and theorem_i *) |
|
26 fun define (name, mx, rhs) lthy = |
|
27 let |
|
28 val ((rhs, (_ , thm)), lthy') = |
|
29 Local_Theory.define ((name, mx), (Attrib.empty_binding, rhs)) lthy |
|
30 in |
|
31 ((rhs, thm), lthy') |
|
32 end |
|
33 |
|
34 fun note (name, thm, attrs) lthy = |
|
35 let |
|
36 val ((_,[thm']), lthy') = Local_Theory.note ((name, attrs), [thm]) lthy |
|
37 in |
|
38 (thm', lthy') |
|
39 end |
|
40 |
|
41 fun intern_attr at = Attrib.internal (K at) |
|
42 |
|
43 fun theorem after_qed goals ctxt = |
|
44 let |
|
45 val goals' = map (rpair []) goals |
|
46 fun after_qed' thms = after_qed (the_single thms) |
|
47 in |
|
48 Proof.theorem_i NONE after_qed' [goals'] ctxt |
|
49 end |
|
50 |
|
51 |
|
52 |
|
53 (*** definition of quotient types ***) |
|
54 |
|
55 val mem_def1 = @{lemma "y : S ==> S y" by (simp add: mem_def)} |
|
56 val mem_def2 = @{lemma "S y ==> y : S" by (simp add: mem_def)} |
|
57 |
|
58 (* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *) |
|
59 fun typedef_term rel rty lthy = |
|
60 let |
|
61 val [x, c] = |
|
62 [("x", rty), ("c", HOLogic.mk_setT rty)] |
|
63 |> Variable.variant_frees lthy [rel] |
|
64 |> map Free |
|
65 in |
|
66 lambda c (HOLogic.exists_const rty $ |
|
67 lambda x (HOLogic.mk_eq (c, (rel $ x)))) |
|
68 end |
|
69 |
|
70 |
|
71 (* makes the new type definitions and proves non-emptyness *) |
|
72 fun typedef_make (vs, qty_name, mx, rel, rty) lthy = |
|
73 let |
|
74 val typedef_tac = |
|
75 EVERY1 (map rtac [@{thm exI}, mem_def2, @{thm exI}, @{thm refl}]) |
|
76 in |
|
77 Typedef.add_typedef false NONE (qty_name, vs, mx) |
|
78 (typedef_term rel rty lthy) NONE typedef_tac lthy |
|
79 end |
|
80 |
|
81 |
|
82 (* tactic to prove the quot_type theorem for the new type *) |
|
83 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = |
|
84 let |
|
85 val rep_thm = #Rep typedef_info RS mem_def1 |
|
86 val rep_inv = #Rep_inverse typedef_info |
|
87 val abs_inv = mem_def2 RS #Abs_inverse typedef_info |
|
88 val rep_inj = #Rep_inject typedef_info |
|
89 in |
|
90 (rtac @{thm quot_type.intro} THEN' RANGE [ |
|
91 rtac equiv_thm, |
|
92 rtac rep_thm, |
|
93 rtac rep_inv, |
|
94 EVERY' (map rtac [abs_inv, @{thm exI}, @{thm refl}]), |
|
95 rtac rep_inj]) 1 |
|
96 end |
|
97 |
|
98 |
|
99 (* proves the quot_type theorem for the new type *) |
|
100 fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy = |
|
101 let |
|
102 val quot_type_const = Const (@{const_name "quot_type"}, dummyT) |
|
103 val goal = |
|
104 HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep) |
|
105 |> Syntax.check_term lthy |
|
106 in |
|
107 Goal.prove lthy [] [] goal |
|
108 (K (typedef_quot_type_tac equiv_thm typedef_info)) |
|
109 end |
|
110 |
|
111 (* proves the quotient theorem for the new type *) |
|
112 fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy = |
|
113 let |
|
114 val quotient_const = Const (@{const_name "Quotient"}, dummyT) |
|
115 val goal = |
|
116 HOLogic.mk_Trueprop (quotient_const $ rel $ abs $ rep) |
|
117 |> Syntax.check_term lthy |
|
118 |
|
119 val typedef_quotient_thm_tac = |
|
120 EVERY1 [ |
|
121 K (rewrite_goals_tac [abs_def, rep_def]), |
|
122 rtac @{thm quot_type.Quotient}, |
|
123 rtac quot_type_thm] |
|
124 in |
|
125 Goal.prove lthy [] [] goal |
|
126 (K typedef_quotient_thm_tac) |
|
127 end |
|
128 |
|
129 |
|
130 (* main function for constructing a quotient type *) |
|
131 fun add_quotient_type (((vs, qty_name, mx), (rty, rel)), equiv_thm) lthy = |
|
132 let |
|
133 (* generates the typedef *) |
|
134 val ((qty_full_name, typedef_info), lthy1) = typedef_make (vs, qty_name, mx, rel, rty) lthy |
|
135 |
|
136 (* abs and rep functions from the typedef *) |
|
137 val Abs_ty = #abs_type typedef_info |
|
138 val Rep_ty = #rep_type typedef_info |
|
139 val Abs_name = #Abs_name typedef_info |
|
140 val Rep_name = #Rep_name typedef_info |
|
141 val Abs_const = Const (Abs_name, Rep_ty --> Abs_ty) |
|
142 val Rep_const = Const (Rep_name, Abs_ty --> Rep_ty) |
|
143 |
|
144 (* more useful abs and rep definitions *) |
|
145 val abs_const = Const (@{const_name "quot_type.abs"}, dummyT ) |
|
146 val rep_const = Const (@{const_name "quot_type.rep"}, dummyT ) |
|
147 val abs_trm = Syntax.check_term lthy1 (abs_const $ rel $ Abs_const) |
|
148 val rep_trm = Syntax.check_term lthy1 (rep_const $ Rep_const) |
|
149 val abs_name = Binding.prefix_name "abs_" qty_name |
|
150 val rep_name = Binding.prefix_name "rep_" qty_name |
|
151 |
|
152 val ((abs, abs_def), lthy2) = define (abs_name, NoSyn, abs_trm) lthy1 |
|
153 val ((rep, rep_def), lthy3) = define (rep_name, NoSyn, rep_trm) lthy2 |
|
154 |
|
155 (* quot_type theorem *) |
|
156 val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, equiv_thm, typedef_info) lthy3 |
|
157 |
|
158 (* quotient theorem *) |
|
159 val quotient_thm = typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_thm) lthy3 |
|
160 val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name |
|
161 |
|
162 (* name equivalence theorem *) |
|
163 val equiv_thm_name = Binding.suffix_name "_equivp" qty_name |
|
164 |
|
165 (* storing the quot-info *) |
|
166 fun qinfo phi = transform_quotdata phi |
|
167 {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm} |
|
168 val lthy4 = Local_Theory.declaration true |
|
169 (fn phi => quotdata_update_gen qty_full_name (qinfo phi)) lthy3 |
|
170 in |
|
171 lthy4 |
|
172 |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add]) |
|
173 ||>> note (equiv_thm_name, equiv_thm, [intern_attr equiv_rules_add]) |
|
174 end |
|
175 |
|
176 |
|
177 (* sanity checks for the quotient type specifications *) |
|
178 fun sanity_check ((vs, qty_name, _), (rty, rel)) = |
|
179 let |
|
180 val rty_tfreesT = map fst (Term.add_tfreesT rty []) |
|
181 val rel_tfrees = map fst (Term.add_tfrees rel []) |
|
182 val rel_frees = map fst (Term.add_frees rel []) |
|
183 val rel_vars = Term.add_vars rel [] |
|
184 val rel_tvars = Term.add_tvars rel [] |
|
185 val qty_str = Binding.str_of qty_name ^ ": " |
|
186 |
|
187 val illegal_rel_vars = |
|
188 if null rel_vars andalso null rel_tvars then [] |
|
189 else [qty_str ^ "illegal schematic variable(s) in the relation."] |
|
190 |
|
191 val dup_vs = |
|
192 (case duplicates (op =) vs of |
|
193 [] => [] |
|
194 | dups => [qty_str ^ "duplicate type variable(s) on the lhs: " ^ commas_quote dups]) |
|
195 |
|
196 val extra_rty_tfrees = |
|
197 (case subtract (op =) vs rty_tfreesT of |
|
198 [] => [] |
|
199 | extras => [qty_str ^ "extra type variable(s) on the lhs: " ^ commas_quote extras]) |
|
200 |
|
201 val extra_rel_tfrees = |
|
202 (case subtract (op =) vs rel_tfrees of |
|
203 [] => [] |
|
204 | extras => [qty_str ^ "extra type variable(s) in the relation: " ^ commas_quote extras]) |
|
205 |
|
206 val illegal_rel_frees = |
|
207 (case rel_frees of |
|
208 [] => [] |
|
209 | xs => [qty_str ^ "illegal variable(s) in the relation: " ^ commas_quote xs]) |
|
210 |
|
211 val errs = illegal_rel_vars @ dup_vs @ extra_rty_tfrees @ extra_rel_tfrees @ illegal_rel_frees |
|
212 in |
|
213 if null errs then () else error (cat_lines errs) |
|
214 end |
|
215 |
|
216 (* check for existence of map functions *) |
|
217 fun map_check ctxt (_, (rty, _)) = |
|
218 let |
|
219 val thy = ProofContext.theory_of ctxt |
|
220 |
|
221 fun map_check_aux rty warns = |
|
222 case rty of |
|
223 Type (_, []) => warns |
|
224 | Type (s, _) => if maps_defined thy s then warns else s::warns |
|
225 | _ => warns |
|
226 |
|
227 val warns = map_check_aux rty [] |
|
228 in |
|
229 if null warns then () |
|
230 else warning ("No map function defined for " ^ commas warns ^ |
|
231 ". This will cause problems later on.") |
|
232 end |
|
233 |
|
234 |
|
235 |
|
236 (*** interface and syntax setup ***) |
|
237 |
|
238 |
|
239 (* the ML-interface takes a list of 5-tuples consisting of: |
|
240 |
|
241 - the name of the quotient type |
|
242 - its free type variables (first argument) |
|
243 - its mixfix annotation |
|
244 - the type to be quotient |
|
245 - the relation according to which the type is quotient |
|
246 |
|
247 it opens a proof-state in which one has to show that the |
|
248 relations are equivalence relations |
|
249 *) |
|
250 |
|
251 fun quotient_type quot_list lthy = |
|
252 let |
|
253 (* sanity check *) |
|
254 val _ = List.app sanity_check quot_list |
|
255 val _ = List.app (map_check lthy) quot_list |
|
256 |
|
257 fun mk_goal (rty, rel) = |
|
258 let |
|
259 val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} |
|
260 in |
|
261 HOLogic.mk_Trueprop (Const (@{const_name equivp}, equivp_ty) $ rel) |
|
262 end |
|
263 |
|
264 val goals = map (mk_goal o snd) quot_list |
|
265 |
|
266 fun after_qed thms lthy = |
|
267 fold_map add_quotient_type (quot_list ~~ thms) lthy |> snd |
|
268 in |
|
269 theorem after_qed goals lthy |
|
270 end |
|
271 |
|
272 fun quotient_type_cmd specs lthy = |
|
273 let |
|
274 fun parse_spec ((((vs, qty_name), mx), rty_str), rel_str) lthy = |
|
275 let |
|
276 val rty = Syntax.read_typ lthy rty_str |
|
277 val lthy1 = Variable.declare_typ rty lthy |
|
278 val rel = |
|
279 Syntax.parse_term lthy1 rel_str |
|
280 |> Syntax.type_constraint (rty --> rty --> @{typ bool}) |
|
281 |> Syntax.check_term lthy1 |
|
282 val (newT, lthy2) = lthy1 |
|
283 |> Typedecl.typedecl_wrt [rel] (qty_name, vs, mx) |
|
284 ||> Variable.declare_term rel |
|
285 |
|
286 (*val Type (full_qty_name, type_args) = newT |
|
287 val vs' = map Term.dest_TFree type_args*) |
|
288 in |
|
289 (((vs, qty_name, mx), (rty, rel)), lthy2) |
|
290 end |
|
291 |
|
292 val (spec', lthy') = fold_map parse_spec specs lthy |
|
293 in |
|
294 quotient_type spec' lthy' |
|
295 end |
|
296 |
|
297 val quotspec_parser = |
|
298 OuterParse.and_list1 |
|
299 ((OuterParse.type_args -- OuterParse.binding) -- |
|
300 OuterParse.opt_mixfix -- (OuterParse.$$$ "=" |-- OuterParse.typ) -- |
|
301 (OuterParse.$$$ "/" |-- OuterParse.term)) |
|
302 |
|
303 val _ = OuterKeyword.keyword "/" |
|
304 |
|
305 val _ = |
|
306 OuterSyntax.local_theory_to_proof "quotient_type" |
|
307 "quotient type definitions (require equivalence proofs)" |
|
308 OuterKeyword.thy_goal (quotspec_parser >> quotient_type_cmd) |
|
309 |
|
310 end; (* structure *) |
|