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