equal
deleted
inserted
replaced
147 lemmas [quot_thm] = fun_quotient |
147 lemmas [quot_thm] = fun_quotient |
148 |
148 |
149 lemmas [quot_respect] = quot_rel_rsp |
149 lemmas [quot_respect] = quot_rel_rsp |
150 |
150 |
151 (* fun_map is not here since equivp is not true *) |
151 (* fun_map is not here since equivp is not true *) |
152 (* TODO: option, ... *) |
|
153 lemmas [quot_equiv] = identity_equivp |
152 lemmas [quot_equiv] = identity_equivp |
154 |
153 |
155 (* definition of the quotient types *) |
154 (* definition of the quotient types *) |
156 (* FIXME: should be called quotient_typ.ML *) |
155 (* FIXME: should be called quotient_typ.ML *) |
157 use "quotient.ML" |
156 use "quotient.ML" |
206 end |
205 end |
207 *} |
206 *} |
208 |
207 |
209 section {* Infrastructure about id *} |
208 section {* Infrastructure about id *} |
210 |
209 |
211 (* TODO: think where should this be *) |
210 lemmas [id_simps] = |
212 lemma prod_fun_id: "prod_fun id id \<equiv> id" |
|
213 by (rule eq_reflection) (simp add: prod_fun_def) |
|
214 |
|
215 lemmas [id_simps] = |
|
216 fun_map_id[THEN eq_reflection] |
211 fun_map_id[THEN eq_reflection] |
217 id_apply[THEN eq_reflection] |
212 id_apply[THEN eq_reflection] |
218 id_def[THEN eq_reflection,symmetric] |
213 id_def[THEN eq_reflection,symmetric] |
219 prod_fun_id |
|
220 |
214 |
221 section {* Debugging infrastructure for testing tactics *} |
215 section {* Debugging infrastructure for testing tactics *} |
222 |
216 |
223 ML {* |
217 ML {* |
224 fun my_print_tac ctxt s i thm = |
218 fun my_print_tac ctxt s i thm = |
646 val goal = hd (Drule.strip_imp_prems (cprop_of thm)) |
640 val goal = hd (Drule.strip_imp_prems (cprop_of thm)) |
647 in |
641 in |
648 thm OF [Goal.prove_internal [] goal (fn _ => quotient_tac ctxt 1)] |
642 thm OF [Goal.prove_internal [] goal (fn _ => quotient_tac ctxt 1)] |
649 end |
643 end |
650 handle _ => error "solve_quotient_assums failed. Maybe a quotient_thm is missing" |
644 handle _ => error "solve_quotient_assums failed. Maybe a quotient_thm is missing" |
651 *} |
|
652 |
|
653 (* Not used *) |
|
654 (* It proves the Quotient assumptions by calling quotient_tac *) |
|
655 ML {* |
|
656 fun solve_quotient_assum i ctxt thm = |
|
657 let |
|
658 val tac = |
|
659 (compose_tac (false, thm, i)) THEN_ALL_NEW |
|
660 (quotient_tac ctxt); |
|
661 val gc = Drule.strip_imp_concl (cprop_of thm); |
|
662 in |
|
663 Goal.prove_internal [] gc (fn _ => tac 1) |
|
664 end |
|
665 handle _ => error "solve_quotient_assum" |
|
666 *} |
645 *} |
667 |
646 |
668 definition |
647 definition |
669 "QUOT_TRUE x \<equiv> True" |
648 "QUOT_TRUE x \<equiv> True" |
670 |
649 |