equal
deleted
inserted
replaced
1 (* Title: quotient_tacs.thy |
1 (* Title: HOL/Tools/Quotient/quotient_tacs.thy |
2 Author: Cezary Kaliszyk and Christian Urban |
2 Author: Cezary Kaliszyk and Christian Urban |
3 |
3 |
4 Tactics for solving goal arising from lifting |
4 Tactics for solving goal arising from lifting theorems to quotient |
5 theorems to quotient types. |
5 types. |
6 *) |
6 *) |
7 |
7 |
8 signature QUOTIENT_TACS = |
8 signature QUOTIENT_TACS = |
9 sig |
9 sig |
10 val regularize_tac: Proof.context -> int -> tactic |
10 val regularize_tac: Proof.context -> int -> tactic |
87 (ctyp_of thy (TVar (x, S)), ctyp_of thy ty) |
87 (ctyp_of thy (TVar (x, S)), ctyp_of thy ty) |
88 |
88 |
89 fun get_match_inst thy pat trm = |
89 fun get_match_inst thy pat trm = |
90 let |
90 let |
91 val univ = Unify.matchers thy [(pat, trm)] |
91 val univ = Unify.matchers thy [(pat, trm)] |
92 val SOME (env, _) = Seq.pull univ (* raises BIND, if no unifier *) |
92 val SOME (env, _) = Seq.pull univ (* raises Bind, if no unifier *) (* FIXME fragile *) |
93 val tenv = Vartab.dest (Envir.term_env env) |
93 val tenv = Vartab.dest (Envir.term_env env) |
94 val tyenv = Vartab.dest (Envir.type_env env) |
94 val tyenv = Vartab.dest (Envir.type_env env) |
95 in |
95 in |
96 (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) |
96 (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) |
97 end |
97 end |