1201 |
1201 |
1202 (******************************************) |
1202 (******************************************) |
1203 (* version with explicit qtrm *) |
1203 (* version with explicit qtrm *) |
1204 (******************************************) |
1204 (******************************************) |
1205 |
1205 |
1206 (* exception for when qtrm and rtrm do not match *) |
|
1207 |
|
1208 ML {* |
1206 ML {* |
1209 fun mk_resp_arg lthy (rty, qty) = |
1207 fun mk_resp_arg lthy (rty, qty) = |
1210 let |
1208 let |
1211 val thy = ProofContext.theory_of lthy |
1209 val thy = ProofContext.theory_of lthy |
1212 in |
1210 in |
1231 ML {* |
1229 ML {* |
1232 val mk_babs = Const (@{const_name "Babs"}, dummyT) |
1230 val mk_babs = Const (@{const_name "Babs"}, dummyT) |
1233 val mk_ball = Const (@{const_name "Ball"}, dummyT) |
1231 val mk_ball = Const (@{const_name "Ball"}, dummyT) |
1234 val mk_bex = Const (@{const_name "Bex"}, dummyT) |
1232 val mk_bex = Const (@{const_name "Bex"}, dummyT) |
1235 val mk_resp = Const (@{const_name Respects}, dummyT) |
1233 val mk_resp = Const (@{const_name Respects}, dummyT) |
|
1234 *} |
|
1235 |
|
1236 ML {* |
|
1237 fun trm_lift_error lthy rtrm qtrm = |
|
1238 let |
|
1239 val rtrm_str = quote (Syntax.string_of_term lthy rtrm) |
|
1240 val qtrm_str = quote (Syntax.string_of_term lthy qtrm) |
|
1241 val msg = ["quotient theorem", qtrm_str, "and lifted theorem", rtrm_str, "do not match."] |
|
1242 in |
|
1243 raise LIFT_MATCH (space_implode " " msg) |
|
1244 end |
1236 *} |
1245 *} |
1237 |
1246 |
1238 ML {* |
1247 ML {* |
1239 (* applies f to the subterm of an abstractions, otherwise to the given term *) |
1248 (* applies f to the subterm of an abstractions, otherwise to the given term *) |
1240 (* abstracted variables do not have to be treated specially *) |
1249 (* abstracted variables do not have to be treated specially *) |
1301 | (t1 $ t2, t1' $ t2') => |
1310 | (t1 $ t2, t1' $ t2') => |
1302 (REGULARIZE_trm lthy t1 t1') $ (REGULARIZE_trm lthy t2 t2') |
1311 (REGULARIZE_trm lthy t1 t1') $ (REGULARIZE_trm lthy t2 t2') |
1303 | (Free (x, ty), Free (x', ty')) => |
1312 | (Free (x, ty), Free (x', ty')) => |
1304 if x = x' |
1313 if x = x' |
1305 then rtrm |
1314 then rtrm |
1306 else raise LIFT_MATCH "quotient and lifted theorem do not match" |
1315 else trm_lift_error lthy rtrm qtrm |
1307 | (Bound i, Bound i') => |
1316 | (Bound i, Bound i') => |
1308 if i = i' |
1317 if i = i' |
1309 then rtrm |
1318 then rtrm |
1310 else raise LIFT_MATCH "quotient and lifted theorem do not match" |
1319 else trm_lift_error lthy rtrm qtrm |
1311 | (Const (s, ty), Const (s', ty')) => |
1320 | (Const (s, ty), Const (s', ty')) => |
1312 if s = s' andalso ty = ty' |
1321 if s = s' andalso ty = ty' |
1313 then rtrm |
1322 then rtrm |
1314 else rtrm (* FIXME: check correspondence according to definitions *) |
1323 else rtrm (* FIXME: check correspondence according to definitions *) |
1315 | _ => raise LIFT_MATCH "quotient and lifted theorem do not match" |
1324 | _ => trm_lift_error lthy rtrm qtrm |
1316 *} |
1325 *} |
1317 |
1326 |
1318 ML {* |
1327 ML {* |
1319 fun mk_REGULARIZE_goal lthy rtrm qtrm = |
1328 fun mk_REGULARIZE_goal lthy rtrm qtrm = |
1320 Logic.mk_implies (rtrm, REGULARIZE_trm lthy rtrm qtrm |> Syntax.check_term lthy) |
1329 Logic.mk_implies (rtrm, REGULARIZE_trm lthy rtrm qtrm |> Syntax.check_term lthy) |