1186 (clean_tac ctxt, "Cleaning proof failed.")] |
1186 (clean_tac ctxt, "Cleaning proof failed.")] |
1187 *} |
1187 *} |
1188 |
1188 |
1189 (* methods / interface *) |
1189 (* methods / interface *) |
1190 ML {* |
1190 ML {* |
1191 val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.thm |
|
1192 |
|
1193 (* FIXME: if the argument order changes then this can be just one function *) |
1191 (* FIXME: if the argument order changes then this can be just one function *) |
1194 fun mk_method1 tac thm ctxt = |
1192 fun mk_method1 tac thm ctxt = |
1195 SIMPLE_METHOD (HEADGOAL (tac ctxt thm)) |
1193 SIMPLE_METHOD (HEADGOAL (tac ctxt thm)) |
1196 |
1194 |
1197 fun mk_method2 tac ctxt = |
1195 fun mk_method2 tac ctxt = |
1198 SIMPLE_METHOD (HEADGOAL (tac ctxt)) |
1196 SIMPLE_METHOD (HEADGOAL (tac ctxt)) |
1199 *} |
1197 *} |
1200 |
1198 |
1201 method_setup lifting = |
1199 method_setup lifting = |
1202 {* rule_spec >> (mk_method1 lift_tac) *} |
1200 {* Attrib.thm >> (mk_method1 lift_tac) *} |
1203 {* Lifting of theorems to quotient types. *} |
1201 {* Lifting of theorems to quotient types. *} |
1204 |
1202 |
1205 method_setup lifting_setup = |
1203 method_setup lifting_setup = |
1206 {* rule_spec >> (mk_method1 procedure_tac) *} |
1204 {* Attrib.thm >> (mk_method1 procedure_tac) *} |
1207 {* Sets up the three goals for the lifting procedure. *} |
1205 {* Sets up the three goals for the lifting procedure. *} |
1208 |
1206 |
1209 method_setup regularize = |
1207 method_setup regularize = |
1210 {* Scan.succeed (mk_method2 regularize_tac) *} |
1208 {* Scan.succeed (mk_method2 regularize_tac) *} |
1211 {* Proves automatically the regularization goals from the lifting procedure. *} |
1209 {* Proves automatically the regularization goals from the lifting procedure. *} |