37 in |
37 in |
38 Proof.theorem_i NONE after_qed' [goals'] ctxt |
38 Proof.theorem_i NONE after_qed' [goals'] ctxt |
39 end |
39 end |
40 |
40 |
41 |
41 |
42 (********************************) |
42 |
43 (* definition of quotient types *) |
43 (*** definition of quotient types ***) |
44 (********************************) |
|
45 |
44 |
46 val mem_def1 = @{lemma "y : S ==> S y" by (simp add: mem_def)} |
45 val mem_def1 = @{lemma "y : S ==> S y" by (simp add: mem_def)} |
47 val mem_def2 = @{lemma "S y ==> y : S" by (simp add: mem_def)} |
46 val mem_def2 = @{lemma "S y ==> y : S" by (simp add: mem_def)} |
48 |
47 |
49 (* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *) |
48 (* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *) |
222 else warning ("No map function defined for " ^ (commas warns) ^ |
221 else warning ("No map function defined for " ^ (commas warns) ^ |
223 ". This will cause problems later on.") |
222 ". This will cause problems later on.") |
224 end |
223 end |
225 |
224 |
226 |
225 |
227 (******************************) |
226 |
228 (* interface and syntax setup *) |
227 (*** interface and syntax setup ***) |
229 (******************************) |
228 |
230 |
229 |
231 (* the ML-interface takes a list of 5-tuples consisting of *) |
230 (* the ML-interface takes a list of 5-tuples consisting of |
232 (* *) |
231 |
233 (* - the name of the quotient type *) |
232 - the name of the quotient type |
234 (* - its free type variables (first argument) *) |
233 - its free type variables (first argument) |
235 (* - its mixfix annotation *) |
234 - its mixfix annotation |
236 (* - the type to be quotient *) |
235 - the type to be quotient |
237 (* - the relation according to which the type is quotient *) |
236 - the relation according to which the type is quotient |
238 (* *) |
237 |
239 (* it opens a proof-state in which one has to show that the *) |
238 it opens a proof-state in which one has to show that the |
240 (* relations are equivalence relations *) |
239 relations are equivalence relations |
|
240 *) |
241 |
241 |
242 fun quotient_type quot_list lthy = |
242 fun quotient_type quot_list lthy = |
243 let |
243 let |
244 (* sanity check *) |
244 (* sanity check *) |
245 val _ = map sanity_check quot_list |
245 val _ = List.app sanity_check quot_list |
246 val _ = map (map_check lthy) quot_list |
246 val _ = List.app (map_check lthy) quot_list |
247 |
247 |
248 fun mk_goal (rty, rel) = |
248 fun mk_goal (rty, rel) = |
249 let |
249 let |
250 val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} |
250 val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} |
251 in |
251 in |