140 section {* type definition for the quotient type *} |
140 section {* type definition for the quotient type *} |
141 |
141 |
142 (* the auxiliary data for the quotient types *) |
142 (* the auxiliary data for the quotient types *) |
143 use "quotient_info.ML" |
143 use "quotient_info.ML" |
144 |
144 |
145 declare [[map * = (prod_fun, prod_rel)]] |
145 |
146 declare [[map "fun" = (fun_map, fun_rel)]] |
146 declare [[map "fun" = (fun_map, fun_rel)]] |
147 |
147 |
148 (* Throws now an exception: *) |
148 (* Throws now an exception: *) |
149 (* declare [[map "option" = (bla, blu)]] *) |
149 (* declare [[map "option" = (bla, blu)]] *) |
150 |
150 |
151 lemmas [quot_thm] = |
151 lemmas [quot_thm] = fun_quotient |
152 fun_quotient prod_quotient |
152 |
153 |
153 lemmas [quot_respect] = quot_rel_rsp |
154 lemmas [quot_respect] = |
|
155 quot_rel_rsp pair_rsp |
|
156 |
154 |
157 (* fun_map is not here since equivp is not true *) |
155 (* fun_map is not here since equivp is not true *) |
158 (* TODO: option, ... *) |
156 (* TODO: option, ... *) |
159 lemmas [quot_equiv] = |
157 lemmas [quot_equiv] = identity_equivp |
160 identity_equivp prod_equivp |
|
161 |
158 |
162 (* definition of the quotient types *) |
159 (* definition of the quotient types *) |
163 (* FIXME: should be called quotient_typ.ML *) |
160 (* FIXME: should be called quotient_typ.ML *) |
164 use "quotient.ML" |
161 use "quotient.ML" |
165 |
162 |
1054 fun clean_tac lthy = |
1051 fun clean_tac lthy = |
1055 let |
1052 let |
1056 val thy = ProofContext.theory_of lthy; |
1053 val thy = ProofContext.theory_of lthy; |
1057 val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) |
1054 val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) |
1058 (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *) |
1055 (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *) |
1059 val thms1 = @{thms all_prs ex_prs} @ defs |
1056 val thms1 = defs @ (prs_rules_get lthy) |
1060 val thms2 = @{thms fun_map.simps Quotient_abs_rep Quotient_rel_rep} @ (id_simps_get lthy) |
1057 val thms2 = @{thms fun_map.simps Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs} |
|
1058 @ (id_simps_get lthy) |
1061 fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver |
1059 fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver |
1062 in |
1060 in |
1063 EVERY' [lambda_prs_tac lthy, |
1061 EVERY' [simp_tac (simps thms1), |
1064 simp_tac (simps thms1), |
1062 lambda_prs_tac lthy, |
1065 simp_tac (simps thms2), |
1063 simp_tac (simps thms2), |
1066 lambda_prs_tac lthy, |
1064 lambda_prs_tac lthy, |
1067 TRY o rtac refl] |
1065 TRY o rtac refl] |
1068 end |
1066 end |
1069 *} |
1067 *} |