152 in |
152 in |
153 lambda c |
153 lambda c |
154 (HOLogic.exists_const ty $ |
154 (HOLogic.exists_const ty $ |
155 lambda x (HOLogic.mk_eq (c, (rel $ x)))) |
155 lambda x (HOLogic.mk_eq (c, (rel $ x)))) |
156 end |
156 end |
157 |
157 *} |
158 |
158 |
|
159 ML {* |
159 (* makes the new type definitions and proves non-emptyness*) |
160 (* makes the new type definitions and proves non-emptyness*) |
160 fun typedef_make (qty_name, rel, ty) lthy = |
161 fun typedef_make (qty_name, mx, rel, ty) lthy = |
161 let |
162 let |
162 val typedef_tac = |
163 val typedef_tac = |
163 EVERY1 [rewrite_goal_tac @{thms mem_def}, |
164 EVERY1 [rewrite_goal_tac @{thms mem_def}, |
164 rtac @{thm exI}, |
165 rtac @{thm exI}, |
165 rtac @{thm exI}, |
166 rtac @{thm exI}, |
166 rtac @{thm refl}] |
167 rtac @{thm refl}] |
|
168 val tfrees = map fst (Term.add_tfreesT ty []) |
167 in |
169 in |
168 LocalTheory.theory_result |
170 LocalTheory.theory_result |
169 (Typedef.add_typedef false NONE |
171 (Typedef.add_typedef false NONE |
170 (qty_name, map fst (Term.add_tfreesT ty []), NoSyn) |
172 (qty_name, tfrees, mx) |
171 (typedef_term rel ty lthy) |
173 (typedef_term rel ty lthy) |
172 NONE typedef_tac) lthy |
174 NONE typedef_tac) lthy |
173 end |
175 end |
174 |
176 *} |
175 |
177 |
|
178 ML {* |
176 (* tactic to prove the QUOT_TYPE theorem for the new type *) |
179 (* tactic to prove the QUOT_TYPE theorem for the new type *) |
177 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = |
180 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = |
178 let |
181 let |
179 val rep_thm = #Rep typedef_info |
182 val rep_thm = #Rep typedef_info |
180 val rep_inv = #Rep_inverse typedef_info |
183 val rep_inv = #Rep_inverse typedef_info |
249 val ((_, [th']), _) = Variable.import true [th] ctxt; |
252 val ((_, [th']), _) = Variable.import true [th] ctxt; |
250 in th' end); |
253 in th' end); |
251 *} |
254 *} |
252 |
255 |
253 ML {* |
256 ML {* |
254 fun typedef_main (qty_name, rel, ty, equiv_thm) lthy = |
257 fun typedef_main (qty_name, mx, rel, ty, equiv_thm) lthy = |
255 let |
258 let |
256 (* generates typedef *) |
259 (* generates typedef *) |
257 val ((_, typedef_info), lthy1) = typedef_make (qty_name, rel, ty) lthy |
260 val ((_, typedef_info), lthy1) = typedef_make (qty_name, mx, rel, ty) lthy |
258 |
261 |
259 (* abs and rep functions *) |
262 (* abs and rep functions *) |
260 val abs_ty = #abs_type typedef_info |
263 val abs_ty = #abs_type typedef_info |
261 val rep_ty = #rep_type typedef_info |
264 val rep_ty = #rep_type typedef_info |
262 val abs_name = #Abs_name typedef_info |
265 val abs_name = #Abs_name typedef_info |
380 |
383 |
381 consts Rt :: "t \<Rightarrow> t \<Rightarrow> bool" |
384 consts Rt :: "t \<Rightarrow> t \<Rightarrow> bool" |
382 axioms t_eq: "EQUIV Rt" |
385 axioms t_eq: "EQUIV Rt" |
383 |
386 |
384 local_setup {* |
387 local_setup {* |
385 typedef_main (@{binding "qt"}, @{term "Rt"}, @{typ "t"}, @{thm t_eq}) #> snd |
388 typedef_main (@{binding "qt"}, NoSyn, @{term "Rt"}, @{typ "t"}, @{thm t_eq}) #> snd |
386 *} |
389 *} |
387 |
390 |
388 section {* lifting of constants *} |
391 section {* lifting of constants *} |
389 |
392 |
390 text {* information about map-functions for type-constructor *} |
393 text {* information about map-functions for type-constructor *} |
577 unfolding EQUIV_REFL_SYM_TRANS REFL_def SYM_def TRANS_def |
580 unfolding EQUIV_REFL_SYM_TRANS REFL_def SYM_def TRANS_def |
578 apply(auto intro: list_eq.intros list_eq_refl) |
581 apply(auto intro: list_eq.intros list_eq_refl) |
579 done |
582 done |
580 |
583 |
581 local_setup {* |
584 local_setup {* |
582 typedef_main (@{binding "fset"}, @{term "list_eq"}, @{typ "'a list"}, @{thm "equiv_list_eq"}) #> snd |
585 typedef_main (@{binding "fset"}, NoSyn, @{term "list_eq"}, @{typ "'a list"}, @{thm "equiv_list_eq"}) #> snd |
583 *} |
586 *} |
584 |
587 |
585 print_theorems |
588 print_theorems |
586 |
589 |
587 typ "'a fset" |
590 typ "'a fset" |