58 lambda c |
58 lambda c |
59 (HOLogic.exists_const rty $ |
59 (HOLogic.exists_const rty $ |
60 lambda x (HOLogic.mk_eq (c, (rel $ x)))) |
60 lambda x (HOLogic.mk_eq (c, (rel $ x)))) |
61 end |
61 end |
62 |
62 |
63 (* makes the new type definitions and proves non-emptyness*) |
63 (* makes the new type definitions and proves non-emptyness *) |
64 fun typedef_make (vs, qty_name, mx, rel, rty) lthy = |
64 fun typedef_make (vs, qty_name, mx, rel, rty) lthy = |
65 let |
65 let |
66 val typedef_tac = |
66 val typedef_tac = |
67 EVERY1 [rtac @{thm exI}, |
67 EVERY1 [rtac @{thm exI}, |
68 rtac mem_def2, |
68 rtac mem_def2, |
165 lthy4 |
165 lthy4 |
166 |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add]) |
166 |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add]) |
167 ||>> note (equiv_thm_name, equiv_thm, [intern_attr equiv_rules_add]) |
167 ||>> note (equiv_thm_name, equiv_thm, [intern_attr equiv_rules_add]) |
168 end |
168 end |
169 |
169 |
|
170 (* sanity checks of the quotient type specifications *) |
|
171 fun sanity_check ((vs, qty_name, _), (rty, rel)) = |
|
172 let |
|
173 val rty_tfreesT = map fst (Term.add_tfreesT rty []) |
|
174 val rel_tfrees = map fst (Term.add_tfrees rel []) |
|
175 val rel_frees = map fst (Term.add_frees rel []) |
|
176 val rel_vars = Term.add_vars rel [] |
|
177 val rel_tvars = Term.add_tvars rel [] |
|
178 val qty_str = (Binding.str_of qty_name) ^ ": " |
|
179 |
|
180 val illegal_rel_vars = |
|
181 if null rel_vars andalso null rel_tvars then [] |
|
182 else [qty_str ^ "illegal schematic variable(s) in the relation."] |
|
183 |
|
184 val dup_vs = |
|
185 (case duplicates (op =) vs of |
|
186 [] => [] |
|
187 | dups => [qty_str ^ "duplicate type variable(s) on the lhs: " ^ commas_quote dups]) |
|
188 |
|
189 val extra_rty_tfrees = |
|
190 (case subtract (op =) vs rty_tfreesT of |
|
191 [] => [] |
|
192 | extras => [qty_str ^ "extra type variable(s) on the lhs: " ^ commas_quote extras]) |
|
193 |
|
194 val extra_rel_tfrees = |
|
195 (case subtract (op =) vs rel_tfrees of |
|
196 [] => [] |
|
197 | extras => [qty_str ^ "extra type variable(s) in the relation: " ^ commas_quote extras]) |
|
198 |
|
199 val illegal_rel_frees = |
|
200 (case rel_frees of |
|
201 [] => [] |
|
202 | xs => [qty_str ^ "illegal variable(s) in the relation: " ^ commas_quote xs]) |
|
203 |
|
204 val errs = illegal_rel_vars @ dup_vs @ extra_rty_tfrees @ extra_rel_tfrees @ illegal_rel_frees |
|
205 in |
|
206 if null errs then () else error (cat_lines errs) |
|
207 end |
170 |
208 |
171 (* interface and syntax setup *) |
209 (* interface and syntax setup *) |
172 |
210 |
173 (* the ML-interface takes a list of 4-tuples consisting of *) |
211 (* the ML-interface takes a list of 5-tuples consisting of *) |
174 (* *) |
212 (* *) |
175 (* - the name of the quotient type *) |
213 (* - the name of the quotient type *) |
|
214 (* - its free type variables (first argument) *) |
176 (* - its mixfix annotation *) |
215 (* - its mixfix annotation *) |
177 (* - the type to be quotient *) |
216 (* - the type to be quotient *) |
178 (* - the relation according to which the type is quotient *) |
217 (* - the relation according to which the type is quotient *) |
179 |
218 |
180 fun quotient_type quot_list lthy = |
219 fun quotient_type quot_list lthy = |
188 |
227 |
189 val goals = map (mk_goal o snd) quot_list |
228 val goals = map (mk_goal o snd) quot_list |
190 |
229 |
191 fun after_qed thms lthy = |
230 fun after_qed thms lthy = |
192 fold_map mk_typedef_main (quot_list ~~ thms) lthy |> snd |
231 fold_map mk_typedef_main (quot_list ~~ thms) lthy |> snd |
|
232 |
|
233 (* sanity check*) |
|
234 val _ = map sanity_check quot_list |
193 in |
235 in |
194 theorem after_qed goals lthy |
236 theorem after_qed goals lthy |
195 end |
237 end |
196 |
238 |
197 fun quotient_type_cmd spec lthy = |
239 fun quotient_type_cmd spec lthy = |