1590 fun allex_prs_tac lthy quot = |
1590 fun allex_prs_tac lthy quot = |
1591 (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]}) |
1591 (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]}) |
1592 THEN' (quotient_tac quot); |
1592 THEN' (quotient_tac quot); |
1593 *} |
1593 *} |
1594 |
1594 |
|
1595 ML {* |
|
1596 let |
|
1597 val parser = Args.context -- Scan.lift Args.name_source |
|
1598 fun term_pat (ctxt, str) = |
|
1599 str |> ProofContext.read_term_pattern ctxt |
|
1600 |> ML_Syntax.print_term |
|
1601 |> ML_Syntax.atomic |
|
1602 in |
|
1603 ML_Antiquote.inline "term_pat" (parser >> term_pat) |
|
1604 end |
|
1605 *} |
|
1606 |
1595 ML {* |
1607 ML {* |
1596 fun prep_trm thy (x, (T, t)) = |
1608 fun prep_trm thy (x, (T, t)) = |
1597 (cterm_of thy (Var (x, T)), cterm_of thy t) |
1609 (cterm_of thy (Var (x, T)), cterm_of thy t) |
1598 |
1610 |
1599 fun prep_ty thy (x, (S, ty)) = |
1611 fun prep_ty thy (x, (S, ty)) = |
1600 (ctyp_of thy (TVar (x, S)), ctyp_of thy ty) |
1612 (ctyp_of thy (TVar (x, S)), ctyp_of thy ty) |
1601 *} |
1613 *} |
1602 |
1614 |
1603 ML {* |
1615 ML {* |
1604 fun unify_prs thy pat trm = |
1616 fun matching_prs thy pat trm = |
1605 let |
1617 let |
1606 val init = Envir.empty 0 (* FIXME: get the max-index *) |
1618 val univ = Unify.matchers thy [(pat, trm)] |
1607 val univ = Unify.smash_unifiers thy [(pat, trm)] init |
|
1608 val SOME (env, _) = Seq.pull univ |
1619 val SOME (env, _) = Seq.pull univ |
1609 val tenv = Vartab.dest (Envir.term_env env) |
1620 val tenv = Vartab.dest (Envir.term_env env) |
1610 val tyenv = Vartab.dest (Envir.type_env env) |
1621 val tyenv = Vartab.dest (Envir.type_env env) |
1611 in |
1622 in |
1612 (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) |
1623 (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) |
1613 end |
1624 end |
1614 *} |
1625 *} |
1615 |
1626 |
1616 |
|
1617 ML {* |
1627 ML {* |
1618 fun lambda_prs_tac lthy quot = |
1628 fun lambda_prs_tac lthy quot = |
1619 (EqSubst.eqsubst_tac lthy [0] @{thms LAMBDA_PRS} |
1629 (EqSubst.eqsubst_tac lthy [0] @{thms LAMBDA_PRS} |
1620 THEN' (RANGE [quotient_tac quot, quotient_tac quot])); |
1630 THEN' (RANGE [quotient_tac quot, quotient_tac quot])); |
1621 *} |
1631 *} |