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 [quotient_thm] = |
151 lemmas [quot_thm] = |
152 fun_quotient prod_quotient |
152 fun_quotient prod_quotient |
153 |
153 |
154 lemmas [quotient_rsp] = |
154 lemmas [quot_respect] = |
155 quot_rel_rsp pair_rsp |
155 quot_rel_rsp pair_rsp |
156 |
156 |
157 (* fun_map is not here since equivp is not true *) |
157 (* fun_map is not here since equivp is not true *) |
158 (* TODO: option, ... *) |
158 (* TODO: option, ... *) |
159 lemmas [quotient_equiv] = |
159 lemmas [quot_equiv] = |
160 identity_equivp prod_equivp |
160 identity_equivp prod_equivp |
161 |
161 |
162 (* definition of the quotient types *) |
162 (* definition of the quotient types *) |
163 (* FIXME: should be called quotient_typ.ML *) |
163 (* FIXME: should be called quotient_typ.ML *) |
164 use "quotient.ML" |
164 use "quotient.ML" |
1061 fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver |
1061 fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver |
1062 in |
1062 in |
1063 EVERY' [lambda_prs_tac lthy, |
1063 EVERY' [lambda_prs_tac lthy, |
1064 simp_tac (simps thms1), |
1064 simp_tac (simps thms1), |
1065 simp_tac (simps thms2), |
1065 simp_tac (simps thms2), |
|
1066 lambda_prs_tac lthy, |
1066 TRY o rtac refl] |
1067 TRY o rtac refl] |
1067 end |
1068 end |
1068 *} |
1069 *} |
1069 |
1070 |
1070 section {* Tactic for genralisation of free variables in a goal *} |
1071 section {* Tactic for genralisation of free variables in a goal *} |
1183 THEN' RANGE_WARN [(regularize_tac ctxt, "Regularize proof failed."), |
1184 THEN' RANGE_WARN [(regularize_tac ctxt, "Regularize proof failed."), |
1184 (all_inj_repabs_tac ctxt, "Injection proof failed."), |
1185 (all_inj_repabs_tac ctxt, "Injection proof failed."), |
1185 (clean_tac ctxt, "Cleaning proof failed.")] |
1186 (clean_tac ctxt, "Cleaning proof failed.")] |
1186 *} |
1187 *} |
1187 |
1188 |
|
1189 (* methods / interface *) |
1188 ML {* |
1190 ML {* |
1189 val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.thm |
1191 val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.thm |
1190 |
1192 |
1191 (* FIXME: if the argument order changes then this can be just one function *) |
1193 (* FIXME: if the argument order changes then this can be just one function *) |
1192 fun mk_method1 tac thm ctxt = |
1194 fun mk_method1 tac thm ctxt = |