1170 val mk_ball = Const (@{const_name "Ball"}, dummyT) |
1170 val mk_ball = Const (@{const_name "Ball"}, dummyT) |
1171 val mk_bex = Const (@{const_name "Bex"}, dummyT) |
1171 val mk_bex = Const (@{const_name "Bex"}, dummyT) |
1172 val mk_resp = Const (@{const_name Respects}, dummyT) |
1172 val mk_resp = Const (@{const_name Respects}, dummyT) |
1173 *} |
1173 *} |
1174 |
1174 |
1175 ML {* |
|
1176 fun trm_lift_error lthy rtrm qtrm = |
|
1177 let |
|
1178 val rtrm_str = quote (Syntax.string_of_term lthy rtrm) |
|
1179 val qtrm_str = quote (Syntax.string_of_term lthy qtrm) |
|
1180 val msg = ["The quotient theorem", qtrm_str, "and lifted theorem", rtrm_str, "do not match."] |
|
1181 in |
|
1182 raise error (space_implode " " msg) |
|
1183 end |
|
1184 *} |
|
1185 |
1175 |
1186 ML {* |
1176 ML {* |
1187 (* - applies f to the subterm of an abstraction, *) |
1177 (* - applies f to the subterm of an abstraction, *) |
1188 (* otherwise to the given term, *) |
1178 (* otherwise to the given term, *) |
1189 (* - used by REGULARIZE, therefore abstracted *) |
1179 (* - used by REGULARIZE, therefore abstracted *) |
1263 | (t1 $ t2, t1' $ t2') => |
1253 | (t1 $ t2, t1' $ t2') => |
1264 (REGULARIZE_trm lthy t1 t1') $ (REGULARIZE_trm lthy t2 t2') |
1254 (REGULARIZE_trm lthy t1 t1') $ (REGULARIZE_trm lthy t2 t2') |
1265 | (Free (x, ty), Free (x', ty')) => |
1255 | (Free (x, ty), Free (x', ty')) => |
1266 if x = x' |
1256 if x = x' |
1267 then rtrm (* FIXME: check whether types corresponds *) |
1257 then rtrm (* FIXME: check whether types corresponds *) |
1268 else trm_lift_error lthy rtrm qtrm |
1258 else raise (LIFT_MATCH "regularize (frees)") |
1269 | (Bound i, Bound i') => |
1259 | (Bound i, Bound i') => |
1270 if i = i' |
1260 if i = i' |
1271 then rtrm |
1261 then rtrm |
1272 else trm_lift_error lthy rtrm qtrm |
1262 else raise (LIFT_MATCH "regularize (bounds)") |
1273 | (Const (s, ty), Const (s', ty')) => |
1263 | (Const (s, ty), Const (s', ty')) => |
1274 if s = s' andalso ty = ty' |
1264 if s = s' andalso ty = ty' |
1275 then rtrm |
1265 then rtrm |
1276 else rtrm (* FIXME: check correspondence according to definitions *) |
1266 else rtrm (* FIXME: check correspondence according to definitions *) |
1277 | _ => trm_lift_error lthy rtrm qtrm |
1267 | (rt, qt) => |
|
1268 let |
|
1269 val _ = tracing "default execption" |
|
1270 val _ = tracing (PolyML.makestring rt) |
|
1271 val _ = tracing (PolyML.makestring qt) |
|
1272 in |
|
1273 raise (LIFT_MATCH "regularize (default)") |
|
1274 end |
1278 *} |
1275 *} |
1279 |
1276 |
1280 ML {* |
1277 ML {* |
1281 fun mk_REGULARIZE_goal lthy rtrm qtrm = |
1278 fun mk_REGULARIZE_goal lthy rtrm qtrm = |
1282 Logic.mk_implies (rtrm, Syntax.check_term lthy (REGULARIZE_trm lthy rtrm qtrm)) |
1279 Logic.mk_implies (rtrm, Syntax.check_term lthy (REGULARIZE_trm lthy rtrm qtrm)) |
1431 | (Const _, Const _, _) => mk_repabs lthy (rty, qty) (list_comb (rhead, rargs')) |
1428 | (Const _, Const _, _) => mk_repabs lthy (rty, qty) (list_comb (rhead, rargs')) |
1432 | (Free (x, T), Free (x', T'), _) => |
1429 | (Free (x, T), Free (x', T'), _) => |
1433 mk_repabs lthy (rty, qty) (list_comb (mk_repabs lthy (T, T') rhead, rargs')) |
1430 mk_repabs lthy (rty, qty) (list_comb (mk_repabs lthy (T, T') rhead, rargs')) |
1434 | (Abs _, Abs _, _ ) => |
1431 | (Abs _, Abs _, _ ) => |
1435 mk_repabs lthy (rty, qty) (list_comb (inj_REPABS lthy (rhead, qhead), rargs')) |
1432 mk_repabs lthy (rty, qty) (list_comb (inj_REPABS lthy (rhead, qhead), rargs')) |
1436 | _ => trm_lift_error lthy rtrm qtrm |
1433 | _ => raise (LIFT_MATCH "injection") |
1437 end |
1434 end |
1438 end |
1435 end |
1439 *} |
1436 *} |
1440 |
1437 |
1441 ML {* |
1438 ML {* |
1526 lthy2 |
1523 lthy2 |
1527 end |
1524 end |
1528 *} |
1525 *} |
1529 |
1526 |
1530 ML {* |
1527 ML {* |
1531 fun spec_frees_tac [] = [] |
1528 fun inst_spec ctrm = |
1532 | spec_frees_tac (x::xs) = |
1529 let |
1533 let |
1530 val cty = ctyp_of_term ctrm |
1534 val spec' = Drule.instantiate' [SOME (ctyp_of_term x)] [NONE, SOME x] @{thm spec} |
1531 in |
1535 in |
1532 Drule.instantiate' [SOME cty] [NONE, SOME ctrm] @{thm spec} |
1536 (rtac spec')::(spec_frees_tac xs) |
1533 end |
1537 end |
1534 |
1538 *} |
1535 fun inst_spec_tac ctrms = |
1539 |
1536 EVERY' (map (dtac o inst_spec) ctrms) |
1540 ML {* |
1537 |
1541 val prepare_tac = CSUBGOAL (fn (concl, i) => |
1538 fun abs_list (xs, t) = |
1542 let |
1539 fold (fn (x, T) => fn t' => HOLogic.all_const T $ (lambda (Free (x, T)) t')) xs t |
1543 val vrs = Thm.add_cterm_frees concl [] |
1540 |
1544 in |
1541 fun gen_frees_tac ctxt = |
1545 EVERY' (ObjectLogic.full_atomize_tac::spec_frees_tac vrs) i |
1542 SUBGOAL (fn (concl, i) => |
1546 end) |
1543 let |
|
1544 val thy = ProofContext.theory_of ctxt |
|
1545 val concl' = HOLogic.dest_Trueprop concl |
|
1546 val vrs = Term.add_frees concl' [] |
|
1547 val cvrs = map (cterm_of thy o Free) vrs |
|
1548 val concl'' = HOLogic.mk_Trueprop (abs_list (vrs, concl')) |
|
1549 val goal = Logic.mk_implies (concl'', concl) |
|
1550 val rule = Goal.prove ctxt [] [] goal |
|
1551 (K ((inst_spec_tac (rev cvrs) THEN' atac) 1)) |
|
1552 in |
|
1553 rtac rule i |
|
1554 end) |
1547 *} |
1555 *} |
1548 |
1556 |
1549 lemma procedure: |
1557 lemma procedure: |
1550 assumes a: "A" |
1558 assumes a: "A" |
1551 and b: "A \<Longrightarrow> B" |
1559 and b: "A \<Longrightarrow> B" |
1553 and d: "C = D" |
1561 and d: "C = D" |
1554 shows "D" |
1562 shows "D" |
1555 using a b c d |
1563 using a b c d |
1556 by simp |
1564 by simp |
1557 |
1565 |
|
1566 ML {* |
|
1567 fun lift_error ctxt fun_str rtrm qtrm = |
|
1568 let |
|
1569 val rtrm_str = Syntax.string_of_term ctxt rtrm |
|
1570 val qtrm_str = Syntax.string_of_term ctxt qtrm |
|
1571 val msg = [enclose "[" "]" fun_str, "The quotient theorem", qtrm_str, |
|
1572 "and the lifted theorem", rtrm_str, "do not match"] |
|
1573 in |
|
1574 error (space_implode " " msg) |
|
1575 end |
|
1576 *} |
|
1577 |
1558 ML {* |
1578 ML {* |
1559 fun procedure_inst ctxt rtrm qtrm = |
1579 fun procedure_inst ctxt rtrm qtrm = |
1560 let |
1580 let |
1561 val thy = ProofContext.theory_of ctxt |
1581 val thy = ProofContext.theory_of ctxt |
1562 val rtrm' = HOLogic.dest_Trueprop rtrm |
1582 val rtrm' = HOLogic.dest_Trueprop rtrm |
1563 val qtrm' = HOLogic.dest_Trueprop qtrm |
1583 val qtrm' = HOLogic.dest_Trueprop qtrm |
1564 val reg_goal = Syntax.check_term ctxt (REGULARIZE_trm ctxt rtrm' qtrm') |
1584 val reg_goal = Syntax.check_term ctxt (REGULARIZE_trm ctxt rtrm' qtrm') |
|
1585 handle (LIFT_MATCH s) => lift_error ctxt s rtrm qtrm |
1565 val inj_goal = Syntax.check_term ctxt (inj_REPABS ctxt (reg_goal, qtrm')) |
1586 val inj_goal = Syntax.check_term ctxt (inj_REPABS ctxt (reg_goal, qtrm')) |
|
1587 handle (LIFT_MATCH s) => lift_error ctxt s rtrm qtrm |
1566 in |
1588 in |
1567 Drule.instantiate' [] |
1589 Drule.instantiate' [] |
1568 [SOME (cterm_of thy rtrm'), |
1590 [SOME (cterm_of thy rtrm'), |
1569 SOME (cterm_of thy reg_goal), |
1591 SOME (cterm_of thy reg_goal), |
1570 SOME (cterm_of thy inj_goal)] |
1592 SOME (cterm_of thy inj_goal)] |
1572 end |
1594 end |
1573 *} |
1595 *} |
1574 |
1596 |
1575 ML {* |
1597 ML {* |
1576 fun procedure_tac rthm ctxt = |
1598 fun procedure_tac rthm ctxt = |
1577 prepare_tac THEN' |
1599 ObjectLogic.full_atomize_tac |
1578 Subgoal.FOCUS (fn {context, concl, ...} => |
1600 THEN' gen_frees_tac ctxt |
1579 let |
1601 THEN' Subgoal.FOCUS (fn {context, concl, ...} => |
1580 val rthm' = atomize_thm rthm |
1602 let |
1581 val rule = procedure_inst context (prop_of rthm') (term_of concl) |
1603 val rthm' = atomize_thm rthm |
1582 in |
1604 val rule = procedure_inst context (prop_of rthm') (Envir.beta_norm (term_of concl)) |
1583 EVERY1 [rtac rule, rtac rthm'] |
1605 in |
1584 end) ctxt |
1606 EVERY1 [rtac rule, rtac rthm'] |
1585 *} |
1607 end) ctxt |
|
1608 *} |
|
1609 |
1586 |
1610 |
1587 |
1611 |
1588 ML {* |
1612 ML {* |
1589 (* FIXME: allex_prs and lambda_prs can be one function *) |
1613 (* FIXME: allex_prs and lambda_prs can be one function *) |
1590 fun allex_prs_tac lthy quot = |
1614 fun allex_prs_tac lthy quot = |
1616 fun matching_prs thy pat trm = |
1640 fun matching_prs thy pat trm = |
1617 let |
1641 let |
1618 val univ = Unify.matchers thy [(pat, trm)] |
1642 val univ = Unify.matchers thy [(pat, trm)] |
1619 val SOME (env, _) = Seq.pull univ |
1643 val SOME (env, _) = Seq.pull univ |
1620 val tenv = Vartab.dest (Envir.term_env env) |
1644 val tenv = Vartab.dest (Envir.term_env env) |
1621 val tyenv = Vartab.dest (Envir.type_env env) |
1645 val tyenv = Vartab.dest (Envir.type_env env) |
1622 in |
1646 in |
1623 (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) |
1647 (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) |
1624 end |
1648 end |
1625 *} |
1649 *} |
1626 |
1650 |