--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Fri Mar 06 23:53:52 2015 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Fri Mar 06 23:54:05 2015 +0100
@@ -100,8 +100,8 @@
let
val thy = Proof_Context.theory_of ctxt
fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm))
- val ty_inst = map (SOME o Thm.global_ctyp_of thy) [domain_type (fastype_of R2)]
- val trm_inst = map (SOME o Thm.global_cterm_of thy) [R2, R1]
+ val ty_inst = map (SOME o Thm.ctyp_of ctxt) [domain_type (fastype_of R2)]
+ val trm_inst = map (SOME o Thm.cterm_of ctxt) [R2, R1]
in
(case try (Drule.instantiate' ty_inst trm_inst) ball_bex_thm of
NONE => NONE
@@ -198,11 +198,10 @@
(Const (@{const_name Quot_True}, _) $ x) =>
let
val fx = fnctn x;
- val thy = Proof_Context.theory_of ctxt;
- val cx = Thm.global_cterm_of thy x;
- val cfx = Thm.global_cterm_of thy fx;
- val cxt = Thm.global_ctyp_of thy (fastype_of x);
- val cfxt = Thm.global_ctyp_of thy (fastype_of fx);
+ val cx = Thm.cterm_of ctxt x;
+ val cfx = Thm.cterm_of ctxt fx;
+ val cxt = Thm.ctyp_of ctxt (fastype_of x);
+ val cfxt = Thm.ctyp_of ctxt (fastype_of fx);
val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QT_imp}
in
Conv.rewr_conv thm ctrm
@@ -236,7 +235,7 @@
assumption is different from the corresponding type in the goal.
*)
val apply_rsp_tac =
- Subgoal.FOCUS (fn {concl, asms, context,...} =>
+ Subgoal.FOCUS (fn {concl, asms, context = ctxt,...} =>
let
val bare_concl = HOLogic.dest_Trueprop (Thm.term_of concl)
val qt_asm = find_qt_asm (map Thm.term_of asms)
@@ -250,13 +249,12 @@
val ty_x = fastype_of x
val ty_b = fastype_of qt_arg
val ty_f = range_type (fastype_of f)
- val thy = Proof_Context.theory_of context
- val ty_inst = map (SOME o Thm.global_ctyp_of thy) [ty_x, ty_b, ty_f]
- val t_inst = map (SOME o Thm.global_cterm_of thy) [R2, f, g, x, y];
+ val ty_inst = map (SOME o Thm.ctyp_of ctxt) [ty_x, ty_b, ty_f]
+ val t_inst = map (SOME o Thm.cterm_of ctxt) [R2, f, g, x, y];
val inst_thm = Drule.instantiate' ty_inst
([NONE, NONE, NONE] @ t_inst) @{thm apply_rspQ3}
in
- (rtac inst_thm THEN' SOLVED' (quotient_tac context)) 1
+ (rtac inst_thm THEN' SOLVED' (quotient_tac ctxt)) 1
end
| _ => no_tac
end)
@@ -265,32 +263,27 @@
complex we rely on instantiation to tell us if it applies
*)
fun equals_rsp_tac R ctxt =
- let
- val thy = Proof_Context.theory_of ctxt
- in
- case try (Thm.global_cterm_of thy) R of (* There can be loose bounds in R *)
- SOME ctm =>
- let
- val ty = domain_type (fastype_of R)
- in
- case try (Drule.instantiate' [SOME (Thm.global_ctyp_of thy ty)]
- [SOME (Thm.global_cterm_of thy R)]) @{thm equals_rsp} of
- SOME thm => rtac thm THEN' quotient_tac ctxt
- | NONE => K no_tac
- end
- | _ => K no_tac
- end
+ case try (Thm.cterm_of ctxt) R of (* There can be loose bounds in R *) (* FIXME fragile *)
+ SOME ctm =>
+ let
+ val ty = domain_type (fastype_of R)
+ in
+ case try (Drule.instantiate' [SOME (Thm.ctyp_of ctxt ty)]
+ [SOME (Thm.cterm_of ctxt R)]) @{thm equals_rsp} of
+ SOME thm => rtac thm THEN' quotient_tac ctxt
+ | NONE => K no_tac
+ end
+ | _ => K no_tac
fun rep_abs_rsp_tac ctxt =
SUBGOAL (fn (goal, i) =>
(case try bare_concl goal of
SOME (rel $ _ $ (rep $ (abs $ _))) =>
(let
- val thy = Proof_Context.theory_of ctxt;
val (ty_a, ty_b) = dest_funT (fastype_of abs);
- val ty_inst = map (SOME o Thm.global_ctyp_of thy) [ty_a, ty_b];
+ val ty_inst = map (SOME o Thm.ctyp_of ctxt) [ty_a, ty_b];
in
- case try (map (SOME o Thm.global_cterm_of thy)) [rel, abs, rep] of
+ case try (map (SOME o Thm.cterm_of ctxt)) [rel, abs, rep] of
SOME t_inst =>
(case try (Drule.instantiate' ty_inst t_inst) @{thm rep_abs_rsp} of
SOME inst_thm => (rtac inst_thm THEN' quotient_tac ctxt) i
@@ -475,11 +468,10 @@
(case Thm.term_of ctrm of
(Const (@{const_name map_fun}, _) $ r1 $ a2) $ (Abs _) =>
let
- val thy = Proof_Context.theory_of ctxt
val (ty_b, ty_a) = dest_funT (fastype_of r1)
val (ty_c, ty_d) = dest_funT (fastype_of a2)
- val tyinst = map (SOME o Thm.global_ctyp_of thy) [ty_a, ty_b, ty_c, ty_d]
- val tinst = [NONE, NONE, SOME (Thm.global_cterm_of thy r1), NONE, SOME (Thm.global_cterm_of thy a2)]
+ val tyinst = map (SOME o Thm.ctyp_of ctxt) [ty_a, ty_b, ty_c, ty_d]
+ val tinst = [NONE, NONE, SOME (Thm.cterm_of ctxt r1), NONE, SOME (Thm.cterm_of ctxt a2)]
val thm1 = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]}
val thm2 = solve_quotient_assm ctxt (solve_quotient_assm ctxt thm1)
val thm3 = rewrite_rule ctxt @{thms id_apply[THEN eq_reflection]} thm2
@@ -488,7 +480,7 @@
then make_inst_id (Thm.term_of (Thm.lhs_of thm3)) (Thm.term_of ctrm)
else make_inst (Thm.term_of (Thm.lhs_of thm3)) (Thm.term_of ctrm)
val thm4 =
- Drule.instantiate_normalize ([], [(Thm.global_cterm_of thy insp, Thm.global_cterm_of thy inst)]) thm3
+ Drule.instantiate_normalize ([], [(Thm.cterm_of ctxt insp, Thm.cterm_of ctxt inst)]) thm3
in
Conv.rewr_conv thm4 ctrm
end
@@ -555,9 +547,8 @@
fun gen_frees_tac ctxt =
SUBGOAL (fn (concl, i) =>
let
- val thy = Proof_Context.theory_of ctxt
val vrs = Term.add_frees concl []
- val cvrs = map (Thm.global_cterm_of thy o Free) vrs
+ val cvrs = map (Thm.cterm_of ctxt o Free) vrs
val concl' = apply_under_Trueprop (all_list vrs) concl
val goal = Logic.mk_implies (concl', concl)
val rule = Goal.prove ctxt [] [] goal
@@ -608,7 +599,6 @@
fun procedure_inst ctxt rtrm qtrm =
let
- val thy = Proof_Context.theory_of ctxt
val rtrm' = HOLogic.dest_Trueprop rtrm
val qtrm' = HOLogic.dest_Trueprop qtrm
val reg_goal = Quotient_Term.regularize_trm_chk ctxt (rtrm', qtrm')
@@ -617,10 +607,10 @@
handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
in
Drule.instantiate' []
- [SOME (Thm.global_cterm_of thy rtrm'),
- SOME (Thm.global_cterm_of thy reg_goal),
+ [SOME (Thm.cterm_of ctxt rtrm'),
+ SOME (Thm.cterm_of ctxt reg_goal),
NONE,
- SOME (Thm.global_cterm_of thy inj_goal)] procedure_thm
+ SOME (Thm.cterm_of ctxt inj_goal)] procedure_thm
end
@@ -668,7 +658,6 @@
fun partiality_procedure_inst ctxt rtrm qtrm =
let
- val thy = Proof_Context.theory_of ctxt
val rtrm' = HOLogic.dest_Trueprop rtrm
val qtrm' = HOLogic.dest_Trueprop qtrm
val reg_goal = Quotient_Term.regularize_trm_chk ctxt (rtrm', qtrm')
@@ -677,9 +666,9 @@
handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
in
Drule.instantiate' []
- [SOME (Thm.global_cterm_of thy reg_goal),
+ [SOME (Thm.cterm_of ctxt reg_goal),
NONE,
- SOME (Thm.global_cterm_of thy inj_goal)] partiality_procedure_thm
+ SOME (Thm.cterm_of ctxt inj_goal)] partiality_procedure_thm
end