175 end |
175 end |
176 *} |
176 *} |
177 |
177 |
178 ML {* |
178 ML {* |
179 (* tactic to prove the QUOT_TYPE theorem for the new type *) |
179 (* tactic to prove the QUOT_TYPE theorem for the new type *) |
180 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = |
180 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) lthy = |
181 let |
181 let |
182 val rep_thm = #Rep typedef_info |
182 val rep_thm = #Rep typedef_info |
183 val rep_inv = #Rep_inverse typedef_info |
183 val rep_inv = #Rep_inverse typedef_info |
184 val abs_inv = #Abs_inverse typedef_info |
184 val abs_inv = #Abs_inverse typedef_info |
185 val rep_inj = #Rep_inject typedef_info |
185 val rep_inj = #Rep_inject typedef_info |
190 in |
190 in |
191 EVERY1 [rtac @{thm QUOT_TYPE.intro}, |
191 EVERY1 [rtac @{thm QUOT_TYPE.intro}, |
192 rtac equiv_thm, |
192 rtac equiv_thm, |
193 rtac rep_thm_simpd, |
193 rtac rep_thm_simpd, |
194 rtac rep_inv, |
194 rtac rep_inv, |
195 rtac abs_inv_simpd, rtac @{thm exI}, rtac @{thm refl}, |
195 rtac abs_inv_simpd, |
|
196 rtac @{thm exI}, |
|
197 rtac @{thm refl}, |
196 rtac rep_inj] |
198 rtac rep_inj] |
197 end |
199 end |
198 |
|
199 |
200 |
200 fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy = |
201 fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy = |
201 let |
202 let |
202 val quot_type_const = Const (@{const_name "QUOT_TYPE"}, dummyT) |
203 val quot_type_const = Const (@{const_name "QUOT_TYPE"}, dummyT) |
203 val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep) |
204 val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep) |
204 |> Syntax.check_term lthy |
205 |> Syntax.check_term lthy |
|
206 val _ = goal |> Syntax.string_of_term lthy |> tracing |
205 in |
207 in |
206 Goal.prove lthy [] [] goal |
208 Goal.prove lthy [] [] goal |
207 (K (typedef_quot_type_tac equiv_thm typedef_info)) |
209 (K (typedef_quot_type_tac equiv_thm typedef_info lthy)) |
208 end |
210 end |
209 |
211 |
210 |
212 |
211 (* proves the quotient theorem *) |
213 (* proves the quotient theorem *) |
212 fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy = |
214 fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy = |
728 This function is needed to rewrite the right-hand |
730 This function is needed to rewrite the right-hand |
729 side to the left-hand side. |
731 side to the left-hand side. |
730 *} |
732 *} |
731 |
733 |
732 ML {* |
734 ML {* |
733 fun unlam_def_aux orig_ctxt ctxt t = |
735 fun unlam_def ctxt def = |
734 let val rhs = Thm.rhs_of t in |
736 let |
735 (case try (Thm.dest_abs NONE) rhs of |
737 val (lhs, rhs) = Thm.dest_equals (cprop_of def) |
736 SOME (v, vt) => |
738 val xs = strip_abs_vars (term_of rhs) |
737 let |
739 val (_, ctxt') = Variable.add_fixes (map fst xs) ctxt |
738 val (vname, vt) = Term.dest_Free (Thm.term_of v) |
740 |
739 val ([vnname], ctxt) = Variable.variant_fixes [vname] ctxt |
741 fun get_lhs [] = lhs |
740 val nv = Free(vnname, vt) |
742 | get_lhs (x::xs) = |
741 val t2 = Drule.fun_cong_rule t (Thm.cterm_of (ProofContext.theory_of ctxt) nv) |
743 let val cx = cterm_of (ProofContext.theory_of ctxt') (Free x) |
742 val tnorm = equal_elim (Drule.beta_eta_conversion (Thm.cprop_of t2)) t2 |
744 in Thm.capply (get_lhs xs) cx end |
743 in unlam_def_aux orig_ctxt ctxt tnorm end |
745 |
744 | NONE => singleton (ProofContext.export ctxt orig_ctxt) t) |
746 fun get_conv [] = Conv.rewr_conv def |
745 end; |
747 | get_conv (x::xs) = Conv.fun_conv (get_conv xs) |
746 |
748 |
747 fun unlam_def ctxt t = unlam_def_aux ctxt ctxt t |
749 in |
|
750 get_conv xs (get_lhs (rev xs)) |> |
|
751 singleton (ProofContext.export ctxt' ctxt) |
|
752 end |
748 *} |
753 *} |
749 |
754 |
750 local_setup {* |
755 local_setup {* |
751 make_const_def @{binding IN} @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
756 make_const_def @{binding IN} @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
752 *} |
757 *} |
753 |
758 |
754 term membship |
759 term membship |
755 term IN |
760 term IN |
756 thm IN_def |
761 thm IN_def |
|
762 ML {* (Conv.fun_conv (Conv.fun_conv (Conv.rewr_conv @{thm IN_def}))) @{cterm "IN x y"}*} |
|
763 ML {* MetaSimplifier.rewrite_rule @{thms IN_def} @{thm IN_def}*} |
|
764 |
757 ML {* unlam_def @{context} @{thm IN_def} *} |
765 ML {* unlam_def @{context} @{thm IN_def} *} |
758 |
766 |
759 lemmas a = QUOT_TYPE.ABS_def[OF QUOT_TYPE_fset] |
767 lemmas a = QUOT_TYPE.ABS_def[OF QUOT_TYPE_fset] |
760 thm QUOT_TYPE.thm11[OF QUOT_TYPE_fset, THEN iffD1, simplified a] |
768 thm QUOT_TYPE.thm11[OF QUOT_TYPE_fset, THEN iffD1, simplified a] |
761 |
769 |