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" |
1060 fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver |
1060 fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver |
1061 in |
1061 in |
1062 EVERY' [lambda_prs_tac lthy, |
1062 EVERY' [lambda_prs_tac lthy, |
1063 simp_tac (simps thms1), |
1063 simp_tac (simps thms1), |
1064 simp_tac (simps thms2), |
1064 simp_tac (simps thms2), |
|
1065 lambda_prs_tac lthy, |
1065 TRY o rtac refl] |
1066 TRY o rtac refl] |
1066 end |
1067 end |
1067 *} |
1068 *} |
1068 |
1069 |
1069 section {* Tactic for genralisation of free variables in a goal *} |
1070 section {* Tactic for genralisation of free variables in a goal *} |
1182 THEN' RANGE_WARN [(regularize_tac ctxt, "Regularize proof failed."), |
1183 THEN' RANGE_WARN [(regularize_tac ctxt, "Regularize proof failed."), |
1183 (all_inj_repabs_tac ctxt, "Injection proof failed."), |
1184 (all_inj_repabs_tac ctxt, "Injection proof failed."), |
1184 (clean_tac ctxt, "Cleaning proof failed.")] |
1185 (clean_tac ctxt, "Cleaning proof failed.")] |
1185 *} |
1186 *} |
1186 |
1187 |
1187 ML {* |
1188 (* methods / interface *) |
1188 val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.thm |
1189 ML {* |
1189 |
|
1190 (* FIXME: if the argument order changes then this can be just one function *) |
1190 (* FIXME: if the argument order changes then this can be just one function *) |
1191 fun mk_method1 tac thm ctxt = |
1191 fun mk_method1 tac thm ctxt = |
1192 SIMPLE_METHOD (HEADGOAL (tac ctxt thm)) |
1192 SIMPLE_METHOD (HEADGOAL (tac ctxt thm)) |
1193 |
1193 |
1194 fun mk_method2 tac ctxt = |
1194 fun mk_method2 tac ctxt = |
1195 SIMPLE_METHOD (HEADGOAL (tac ctxt)) |
1195 SIMPLE_METHOD (HEADGOAL (tac ctxt)) |
1196 *} |
1196 *} |
1197 |
1197 |
1198 method_setup lifting = |
1198 method_setup lifting = |
1199 {* rule_spec >> (mk_method1 lift_tac) *} |
1199 {* Attrib.thm >> (mk_method1 lift_tac) *} |
1200 {* Lifting of theorems to quotient types. *} |
1200 {* Lifting of theorems to quotient types. *} |
1201 |
1201 |
1202 method_setup lifting_setup = |
1202 method_setup lifting_setup = |
1203 {* rule_spec >> (mk_method1 procedure_tac) *} |
1203 {* Attrib.thm >> (mk_method1 procedure_tac) *} |
1204 {* Sets up the three goals for the lifting procedure. *} |
1204 {* Sets up the three goals for the lifting procedure. *} |
1205 |
1205 |
1206 method_setup regularize = |
1206 method_setup regularize = |
1207 {* Scan.succeed (mk_method2 regularize_tac) *} |
1207 {* Scan.succeed (mk_method2 regularize_tac) *} |
1208 {* Proves automatically the regularization goals from the lifting procedure. *} |
1208 {* Proves automatically the regularization goals from the lifting procedure. *} |