equal
deleted
inserted
replaced
147 |
147 |
148 lemmas [quotient_thm] = |
148 lemmas [quotient_thm] = |
149 fun_quotient list_quotient |
149 fun_quotient list_quotient |
150 |
150 |
151 lemmas [quotient_rsp] = |
151 lemmas [quotient_rsp] = |
152 quot_rel_rsp nil_rsp cons_rsp |
152 quot_rel_rsp nil_rsp cons_rsp foldl_rsp |
153 |
153 |
154 ML {* maps_lookup @{theory} "List.list" *} |
154 ML {* maps_lookup @{theory} "List.list" *} |
155 ML {* maps_lookup @{theory} "*" *} |
155 ML {* maps_lookup @{theory} "*" *} |
156 ML {* maps_lookup @{theory} "fun" *} |
156 ML {* maps_lookup @{theory} "fun" *} |
157 |
157 |
1108 |
1108 |
1109 ML {* |
1109 ML {* |
1110 fun clean_tac lthy = |
1110 fun clean_tac lthy = |
1111 let |
1111 let |
1112 val thy = ProofContext.theory_of lthy; |
1112 val thy = ProofContext.theory_of lthy; |
1113 val defs = map (Thm.varifyT o #def) (qconsts_dest thy) |
1113 val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) |
1114 val thms1 = @{thms all_prs ex_prs} |
1114 val thms1 = @{thms all_prs ex_prs} @ defs |
1115 val thms2 = @{thms eq_reflection[OF fun_map.simps]} |
1115 val thms2 = @{thms eq_reflection[OF fun_map.simps]} |
1116 @ @{thms id_simps Quotient_abs_rep Quotient_rel_rep} |
1116 @ @{thms id_simps Quotient_abs_rep Quotient_rel_rep} |
1117 @ defs |
|
1118 fun simp_ctxt thms = HOL_basic_ss addsimps thms addSolver quotient_solver |
1117 fun simp_ctxt thms = HOL_basic_ss addsimps thms addSolver quotient_solver |
1119 (* FIXME: use of someting smaller than HOL_basic_ss *) |
1118 (* FIXME: use of someting smaller than HOL_basic_ss *) |
1120 in |
1119 in |
1121 EVERY' [ |
1120 EVERY' [ |
1122 (* (rep1 ---> abs2) (\<lambda>x. rep2 (f (abs1 x))) ----> f *) |
1121 (* (rep1 ---> abs2) (\<lambda>x. rep2 (f (abs1 x))) ----> f *) |