--- a/IntEx.thy Sat Nov 28 03:07:38 2009 +0100
+++ b/IntEx.thy Sat Nov 28 04:37:04 2009 +0100
@@ -161,7 +161,7 @@
apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
-apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) (***)
apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
@@ -236,49 +236,3 @@
done
-(*
-
-ML {*
-fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms =
- (REPEAT1 o FIRST1)
- [(K (print_tac "start")) THEN' (K no_tac),
- DT ctxt "1" (rtac trans_thm),
- DT ctxt "2" (LAMBDA_RES_TAC ctxt),
- DT ctxt "3" (ball_rsp_tac ctxt),
- DT ctxt "4" (bex_rsp_tac ctxt),
- DT ctxt "5" (FIRST' (map rtac rsp_thms)),
- DT ctxt "6" (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),
- DT ctxt "7" (rtac refl),
- DT ctxt "8" (APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])),
- DT ctxt "9" (Cong_Tac.cong_tac @{thm cong}),
- DT ctxt "A" (rtac @{thm ext}),
- DT ctxt "B" (rtac reflex_thm),
- DT ctxt "C" (atac),
- DT ctxt "D" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),
- DT ctxt "E" (WEAK_LAMBDA_RES_TAC ctxt),
- DT ctxt "F" (CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))]
-*}
-
-ML {*
-inj_repabs_trm @{context} (reg_atrm, aqtrm)
- |> Syntax.check_term @{context}
-*}
-
-
-ML {* val my_goal = cterm_of @{theory} (mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm)) *}
-ML {* val yr_goal = cterm_of @{theory} (build_repabs_goal @{context} (@{thm testtest} OF [arthm]) consts rty qty) *}
-
-prove {* mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm) *}
-apply(tactic {* ObjectLogic.full_atomize_tac 1 *})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *})
-done
-
-ML {*
-inj_repabs_trm @{context} (reg_atrm, aqtrm)
-|> Syntax.string_of_term @{context}
-|> writeln
-*}
-
-*)
-
-
--- a/QuotMain.thy Sat Nov 28 03:07:38 2009 +0100
+++ b/QuotMain.thy Sat Nov 28 04:37:04 2009 +0100
@@ -746,23 +746,20 @@
using a by (simp add: FUN_REL.simps)
ML {*
-val LAMBDA_RES_TAC =
- SUBGOAL (fn (goal, i) =>
- case goal of
- (_ $ (_ $ (Abs _) $ (Abs _))) => rtac @{thm FUN_REL_I} i
+val LAMBDA_RES_TAC2 =
+ 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_TAC2 =
+ 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 *)
@@ -776,14 +773,14 @@
ML {*
fun APPLY_RSP_TAC rty =
- CSUBGOAL (fn (concl, i) =>
+ 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}) i
+ if needs_lift rty (type_of f) then
+ rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1
else no_tac
end
handle _ => no_tac)
@@ -822,7 +819,7 @@
ML {*
fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
(FIRST' [resolve_tac trans2,
- LAMBDA_RES_TAC,
+ LAMBDA_RES_TAC2 ctxt,
rtac @{thm RES_FORALL_RSP},
ball_rsp_tac ctxt,
rtac @{thm RES_EXISTS_RSP},
@@ -831,14 +828,14 @@
rtac @{thm refl},
(instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN'
(RANGE [SOLVES' (quotient_tac quot_thms)])),
- (APPLY_RSP_TAC rty 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},
resolve_tac rel_refl,
atac,
SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})),
- WEAK_LAMBDA_RES_TAC ctxt,
+ WEAK_LAMBDA_RES_TAC2 ctxt,
CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))])
fun all_r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
@@ -878,7 +875,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_TAC2 ctxt),
(* R (Ball\<dots>) (Ball\<dots>) \<Longrightarrow> R (\<dots>) (\<dots>) *)
DT ctxt "3" (rtac @{thm RES_FORALL_RSP}),
@@ -899,7 +896,7 @@
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 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 *)
@@ -915,7 +912,7 @@
DT ctxt "E" (atac),
DT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),
- DT ctxt "G" (WEAK_LAMBDA_RES_TAC ctxt),
+ DT ctxt "G" (WEAK_LAMBDA_RES_TAC2 ctxt),
DT ctxt "H" (CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))])
fun all_r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms =