1198 lthy2 |
1198 lthy2 |
1199 end |
1199 end |
1200 *} |
1200 *} |
1201 |
1201 |
1202 (******************************************) |
1202 (******************************************) |
|
1203 (******************************************) |
1203 (* version with explicit qtrm *) |
1204 (* version with explicit qtrm *) |
|
1205 (******************************************) |
1204 (******************************************) |
1206 (******************************************) |
1205 |
1207 |
1206 ML {* |
1208 ML {* |
1207 fun mk_resp_arg lthy (rty, qty) = |
1209 fun mk_resp_arg lthy (rty, qty) = |
1208 let |
1210 let |
1236 ML {* |
1238 ML {* |
1237 fun trm_lift_error lthy rtrm qtrm = |
1239 fun trm_lift_error lthy rtrm qtrm = |
1238 let |
1240 let |
1239 val rtrm_str = quote (Syntax.string_of_term lthy rtrm) |
1241 val rtrm_str = quote (Syntax.string_of_term lthy rtrm) |
1240 val qtrm_str = quote (Syntax.string_of_term lthy qtrm) |
1242 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."] |
1243 val msg = ["The quotient theorem", qtrm_str, "and lifted theorem", rtrm_str, "do not match."] |
1242 in |
1244 in |
1243 raise LIFT_MATCH (space_implode " " msg) |
1245 raise LIFT_MATCH (space_implode " " msg) |
1244 end |
1246 end |
1245 *} |
1247 *} |
1246 |
1248 |
1272 *) |
1274 *) |
1273 |
1275 |
1274 ML {* |
1276 ML {* |
1275 fun REGULARIZE_trm lthy rtrm qtrm = |
1277 fun REGULARIZE_trm lthy rtrm qtrm = |
1276 case (rtrm, qtrm) of |
1278 case (rtrm, qtrm) of |
1277 (Abs (x, T, t), Abs (x', T', t')) => |
1279 (Abs (x, ty, t), Abs (x', ty', t')) => |
1278 let |
1280 let |
1279 val subtrm = REGULARIZE_trm lthy t t' |
1281 val subtrm = REGULARIZE_trm lthy t t' |
1280 in |
1282 in |
1281 if T = T' |
1283 if ty = ty' |
1282 then Abs (x, T, subtrm) |
1284 then Abs (x, ty, subtrm) |
1283 else mk_babs $ (mk_resp $ mk_resp_arg lthy (T, T')) $ subtrm |
1285 else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm |
1284 end |
1286 end |
1285 | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => |
1287 | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => |
1286 let |
1288 let |
1287 val subtrm = apply_subt (REGULARIZE_trm lthy) t t' |
1289 val subtrm = apply_subt (REGULARIZE_trm lthy) t t' |
1288 in |
1290 in |
1296 in |
1298 in |
1297 if ty = ty' |
1299 if ty = ty' |
1298 then Const (@{const_name "Ex"}, ty) $ subtrm |
1300 then Const (@{const_name "Ex"}, ty) $ subtrm |
1299 else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm |
1301 else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm |
1300 end |
1302 end |
1301 (* FIXME: why is there a case for equality? is it correct? *) |
1303 (* FIXME: Why is there a case for equality? Is it correct? *) |
1302 | (Const (@{const_name "op ="}, ty) $ t, Const (@{const_name "op ="}, ty') $ t') => |
1304 | (Const (@{const_name "op ="}, ty) $ t, Const (@{const_name "op ="}, ty') $ t') => |
1303 let |
1305 let |
1304 val subtrm = REGULARIZE_trm lthy t t' |
1306 val subtrm = REGULARIZE_trm lthy t t' |
1305 in |
1307 in |
1306 if ty = ty' |
1308 if ty = ty' |
1359 apply(rule b) |
1361 apply(rule b) |
1360 done |
1362 done |
1361 |
1363 |
1362 ML {* |
1364 ML {* |
1363 fun REGULARIZE_tac lthy rel_refl rel_eqv = |
1365 fun REGULARIZE_tac lthy rel_refl rel_eqv = |
1364 ObjectLogic.full_atomize_tac THEN' |
1366 (REPEAT1 o FIRST1) |
1365 REPEAT_ALL_NEW (FIRST' |
|
1366 [rtac rel_refl, |
1367 [rtac rel_refl, |
1367 atac, |
1368 atac, |
1368 rtac @{thm universal_twice}, |
1369 rtac @{thm universal_twice}, |
1369 rtac @{thm impI} THEN' atac, |
1370 rtac @{thm impI} THEN' atac, |
1370 rtac @{thm implication_twice}, |
1371 rtac @{thm implication_twice}, |
1371 rtac @{thm my_equiv_res_forall2}, |
1372 rtac @{thm my_equiv_res_forall2}, |
1372 rtac (rel_eqv RS @{thm my_equiv_res_exists}), |
1373 rtac (rel_eqv RS @{thm my_equiv_res_exists}), |
1373 (* For a = b \<longrightarrow> a \<approx> b *) |
1374 (* For a = b \<longrightarrow> a \<approx> b *) |
1374 rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl, |
1375 rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl, |
1375 rtac @{thm RIGHT_RES_FORALL_REGULAR}]) |
1376 rtac @{thm RIGHT_RES_FORALL_REGULAR}] |
1376 *} |
1377 *} |
1377 |
1378 |
1378 (* same version including debugging information *) |
1379 (* same version including debugging information *) |
1379 ML {* |
1380 ML {* |
1380 fun my_print_tac ctxt s thm = |
1381 fun my_print_tac ctxt s thm = |