equal
deleted
inserted
replaced
164 |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add]) |
164 |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add]) |
165 ||>> note (equiv_thm_name, equiv_thm, [intern_attr equiv_rules_add]) |
165 ||>> note (equiv_thm_name, equiv_thm, [intern_attr equiv_rules_add]) |
166 end |
166 end |
167 |
167 |
168 |
168 |
169 (* sanity checks of the quotient type specifications *) |
169 (* sanity checks for the quotient type specifications *) |
170 fun sanity_check ((vs, qty_name, _), (rty, rel)) = |
170 fun sanity_check ((vs, qty_name, _), (rty, rel)) = |
171 let |
171 let |
172 val rty_tfreesT = map fst (Term.add_tfreesT rty []) |
172 val rty_tfreesT = map fst (Term.add_tfreesT rty []) |
173 val rel_tfrees = map fst (Term.add_tfrees rel []) |
173 val rel_tfrees = map fst (Term.add_tfrees rel []) |
174 val rel_frees = map fst (Term.add_frees rel []) |
174 val rel_frees = map fst (Term.add_frees rel []) |
201 | xs => [qty_str ^ "illegal variable(s) in the relation: " ^ commas_quote xs]) |
201 | xs => [qty_str ^ "illegal variable(s) in the relation: " ^ commas_quote xs]) |
202 |
202 |
203 val errs = illegal_rel_vars @ dup_vs @ extra_rty_tfrees @ extra_rel_tfrees @ illegal_rel_frees |
203 val errs = illegal_rel_vars @ dup_vs @ extra_rty_tfrees @ extra_rel_tfrees @ illegal_rel_frees |
204 in |
204 in |
205 if null errs then () else error (cat_lines errs) |
205 if null errs then () else error (cat_lines errs) |
|
206 end |
|
207 |
|
208 (* check for existence of map functions *) |
|
209 fun map_check ctxt (_, (rty, _)) = |
|
210 let |
|
211 val thy = ProofContext.theory_of ctxt |
|
212 |
|
213 fun map_check_aux rty warns = |
|
214 case rty of |
|
215 Type (_, []) => warns |
|
216 | Type (s, _) => if (maps_exists thy s) then warns else s::warns |
|
217 | _ => warns |
|
218 |
|
219 val warns = map_check_aux rty [] |
|
220 in |
|
221 if null warns then () |
|
222 else warning ("No map function defined for " ^ (commas warns) ^ |
|
223 ". This will cause problems later on.") |
206 end |
224 end |
207 |
225 |
208 |
226 |
209 (******************************) |
227 (******************************) |
210 (* interface and syntax setup *) |
228 (* interface and syntax setup *) |
223 |
241 |
224 fun quotient_type quot_list lthy = |
242 fun quotient_type quot_list lthy = |
225 let |
243 let |
226 (* sanity check *) |
244 (* sanity check *) |
227 val _ = map sanity_check quot_list |
245 val _ = map sanity_check quot_list |
|
246 val _ = map (map_check lthy) quot_list |
228 |
247 |
229 fun mk_goal (rty, rel) = |
248 fun mk_goal (rty, rel) = |
230 let |
249 let |
231 val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} |
250 val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} |
232 in |
251 in |