# HG changeset patch # User Christian Urban # Date 1259379424 -3600 # Node ID f62d59cd8e1b8dc32afb4e15fc939614230f6e7a # Parent 12fc780ff0e8fff594fed6678ebd7d620140093b fixed previous commit diff -r 12fc780ff0e8 -r f62d59cd8e1b IntEx.thy --- 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 -*} - -*) - - diff -r 12fc780ff0e8 -r f62d59cd8e1b QuotMain.thy --- 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) (\x\) (\\) \ \R1 x y\ \ R2 (\x) (\y) *) - DT ctxt "2" (LAMBDA_RES_TAC), + DT ctxt "2" (LAMBDA_RES_TAC2 ctxt), (* R (Ball\) (Ball\) \ R (\) (\) *) DT ctxt "3" (rtac @{thm RES_FORALL_RSP}), @@ -899,7 +896,7 @@ THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))), (* R (t $ \) (t' $ \) \ 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 $ \) (t' $ \) \ 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 =