--- a/QuotMain.thy Sat Nov 28 05:29:30 2009 +0100
+++ b/QuotMain.thy Sat Nov 28 05:43:18 2009 +0100
@@ -812,22 +812,19 @@
ML {*
val LAMBDA_RES_TAC =
- SUBGOAL (fn (goal, i) =>
- case goal of
- (_ $ (_ $ (Abs _) $ (Abs _))) => rtac @{thm FUN_REL_I} i
+ Subgoal.FOCUS (fn {concl, ...} =>
+ case (term_of concl) of
+ (_ $ (_ $ (Abs _) $ (Abs _))) => rtac @{thm FUN_REL_I} 1
| _ => no_tac)
*}
ML {*
-fun WEAK_LAMBDA_RES_TAC ctxt i st =
- (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
- (_ $ (_ $ _ $ (Abs(_, _, _)))) =>
- (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
- (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
- | (_ $ (_ $ (Abs(_, _, _)) $ _)) =>
- (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
- (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
- | _ => fn _ => no_tac) i st
+val WEAK_LAMBDA_RES_TAC =
+ Subgoal.FOCUS (fn {concl, ...} =>
+ case (term_of concl) of
+ (_ $ (_ $ _ $ (Abs _))) => rtac @{thm FUN_REL_I} 1
+ | (_ $ (_ $ (Abs _) $ _)) => rtac @{thm FUN_REL_I} 1
+ | _ => no_tac)
*}
ML {* (* Legacy *)
@@ -839,48 +836,44 @@
*}
-(* Doesn't work *)
ML {*
-fun APPLY_RSP_TAC rty = Subgoal.FOCUS (fn {concl, ...} =>
- let
- val (_ $ (R $ (f $ _) $ (_ $ _))) = term_of concl;
- val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP});
- val insts = Thm.match (pat, concl)
- in
- if needs_lift rty (type_of f) then rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1
- else no_tac
- end
- handle _ => no_tac)
-*}
-
-
-
-ML {*
-val ball_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
- let
- val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $
- (Const (@{const_name Ball}, _) $ _)) = term_of concl
- in
- ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))
- THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
- THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN'
- (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
- end
- handle _ => no_tac)
+fun APPLY_RSP_TAC rty =
+ Subgoal.FOCUS (fn {concl, ...} =>
+ case (term_of concl) of
+ (_ $ (R $ (f $ _) $ (_ $ _))) =>
+ let
+ val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP});
+ val insts = Thm.match (pat, concl)
+ in
+ if needs_lift rty (fastype_of f)
+ then rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1
+ else no_tac
+ end
+ | _ => no_tac)
*}
ML {*
-val bex_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
- let
- val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $
- (Const (@{const_name Bex}, _) $ _)) = term_of concl
- in
- ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))
- THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
- THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN'
- (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
- end
- handle _ => no_tac)
+val ball_rsp_tac =
+ Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
+ case (term_of concl) of
+ (_ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ (Const (@{const_name Ball}, _) $ _))) =>
+ ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))
+ THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
+ THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN'
+ (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
+ |_ => no_tac)
+*}
+
+ML {*
+val bex_rsp_tac =
+ Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
+ case (term_of concl) of
+ (_ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ (Const (@{const_name Bex}, _) $ _))) =>
+ ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))
+ THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
+ THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN'
+ (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
+ | _ => no_tac)
*}
ML {*
@@ -890,16 +883,16 @@
ML {*
fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
(FIRST' [resolve_tac trans2,
- LAMBDA_RES_TAC,
+ LAMBDA_RES_TAC ctxt,
rtac @{thm RES_FORALL_RSP},
ball_rsp_tac ctxt,
rtac @{thm RES_EXISTS_RSP},
bex_rsp_tac ctxt,
resolve_tac rsp_thms,
rtac @{thm refl},
- (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN'
+ (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN'
(RANGE [SOLVES' (quotient_tac quot_thms)])),
- (APPLY_RSP_TAC rty ctxt THEN'
+ (APPLY_RSP_TAC rty ctxt THEN'
(RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)])),
Cong_Tac.cong_tac @{thm cong},
rtac @{thm ext},
@@ -946,7 +939,7 @@
DT ctxt "1" (resolve_tac trans2),
(* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>\<dots>) \<Longrightarrow> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *)
- DT ctxt "2" (LAMBDA_RES_TAC),
+ DT ctxt "2" (LAMBDA_RES_TAC ctxt),
(* R (Ball\<dots>) (Ball\<dots>) \<Longrightarrow> R (\<dots>) (\<dots>) *)
DT ctxt "3" (rtac @{thm RES_FORALL_RSP}),
@@ -963,11 +956,11 @@
(* R (\<dots>) (Rep (Abs \<dots>)) \<Longrightarrow> R (\<dots>) (\<dots>) *)
(* observe ---> *)
- DT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt
+ DT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt
THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))),
(* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> APPLY_RSP provided type of t needs lifting *)
- DT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN'
+ DT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN'
(RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))),
(* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> Cong provided R = (op =) and t does not need lifting *)