equal
deleted
inserted
replaced
139 section {* type definition for the quotient type *} |
139 section {* type definition for the quotient type *} |
140 |
140 |
141 (* the auxiliary data for the quotient types *) |
141 (* the auxiliary data for the quotient types *) |
142 use "quotient_info.ML" |
142 use "quotient_info.ML" |
143 |
143 |
144 declare [[map list = (map, LIST_REL)]] |
144 declare [[map list = (map, list_rel)]] |
145 declare [[map * = (prod_fun, prod_rel)]] |
145 declare [[map * = (prod_fun, prod_rel)]] |
146 declare [[map "fun" = (fun_map, fun_rel)]] |
146 declare [[map "fun" = (fun_map, fun_rel)]] |
147 |
147 |
148 lemmas [quotient_thm] = |
148 lemmas [quotient_thm] = |
149 FUN_Quotient LIST_Quotient |
149 fun_quotient list_quotient |
150 |
150 |
151 ML {* maps_lookup @{theory} "List.list" *} |
151 ML {* maps_lookup @{theory} "List.list" *} |
152 ML {* maps_lookup @{theory} "*" *} |
152 ML {* maps_lookup @{theory} "*" *} |
153 ML {* maps_lookup @{theory} "fun" *} |
153 ML {* maps_lookup @{theory} "fun" *} |
154 |
154 |
212 apply (rule_tac list="x" in list.induct) |
212 apply (rule_tac list="x" in list.induct) |
213 apply (simp_all) |
213 apply (simp_all) |
214 done |
214 done |
215 |
215 |
216 lemmas id_simps = |
216 lemmas id_simps = |
217 FUN_MAP_I[THEN eq_reflection] |
217 fun_map_id[THEN eq_reflection] |
218 id_apply[THEN eq_reflection] |
218 id_apply[THEN eq_reflection] |
219 id_def[THEN eq_reflection,symmetric] |
219 id_def[THEN eq_reflection,symmetric] |
220 prod_fun_id map_id |
220 prod_fun_id map_id |
221 |
221 |
222 ML {* |
222 ML {* |
608 val simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc rel_eqvs)) |
608 val simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc rel_eqvs)) |
609 val simproc2 = Simplifier.simproc_i thy "" pat2 (K (bex_reg_eqv_simproc rel_eqvs)) |
609 val simproc2 = Simplifier.simproc_i thy "" pat2 (K (bex_reg_eqv_simproc rel_eqvs)) |
610 val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc rel_eqvs)) |
610 val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc rel_eqvs)) |
611 val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc rel_eqvs)) |
611 val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc rel_eqvs)) |
612 val simp_ctxt = (Simplifier.context ctxt empty_ss) addsimprocs [simproc1, simproc2, simproc3, simproc4] |
612 val simp_ctxt = (Simplifier.context ctxt empty_ss) addsimprocs [simproc1, simproc2, simproc3, simproc4] |
613 (* TODO: Make sure that there are no LIST_REL, PAIR_REL etc involved *) |
613 (* TODO: Make sure that there are no list_rel, pair_rel etc involved *) |
614 val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) rel_eqvs |
614 val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) rel_eqvs |
615 in |
615 in |
616 ObjectLogic.full_atomize_tac THEN' |
616 ObjectLogic.full_atomize_tac THEN' |
617 simp_tac simp_ctxt THEN' |
617 simp_tac simp_ctxt THEN' |
618 REPEAT_ALL_NEW (FIRST' [ |
618 REPEAT_ALL_NEW (FIRST' [ |