equal
deleted
inserted
replaced
246 in |
246 in |
247 Seq.single thm |
247 Seq.single thm |
248 end |
248 end |
249 |
249 |
250 fun DT ctxt s tac = EVERY' [tac, K (my_print_tac ctxt ("after " ^ s))] |
250 fun DT ctxt s tac = EVERY' [tac, K (my_print_tac ctxt ("after " ^ s))] |
|
251 |
|
252 fun NDT ctxt s tac = tac |
251 *} |
253 *} |
252 |
254 |
253 section {* Infrastructure about definitions *} |
255 section {* Infrastructure about definitions *} |
254 |
256 |
255 (* Does the same as 'subst' in a given theorem *) |
257 (* Does the same as 'subst' in a given theorem *) |
831 ML {* |
833 ML {* |
832 val ball_rsp_tac = |
834 val ball_rsp_tac = |
833 Subgoal.FOCUS (fn {concl, ...} => |
835 Subgoal.FOCUS (fn {concl, ...} => |
834 case (term_of concl) of |
836 case (term_of concl) of |
835 (_ $ (_ $ (Const (@{const_name Ball}, _) $ _) |
837 (_ $ (_ $ (Const (@{const_name Ball}, _) $ _) |
836 $ (Const (@{const_name Ball}, _) $ _))) => |
838 $ (Const (@{const_name Ball}, _) $ _))) => rtac @{thm FUN_REL_I} 1 |
837 rtac @{thm FUN_REL_I} 1 |
|
838 |_ => no_tac) |
839 |_ => no_tac) |
839 *} |
840 *} |
840 |
841 |
841 ML {* |
842 ML {* |
842 val bex_rsp_tac = |
843 val bex_rsp_tac = |
843 Subgoal.FOCUS (fn {concl, context = ctxt, ...} => |
844 Subgoal.FOCUS (fn {concl, context = ctxt, ...} => |
844 case (term_of concl) of |
845 case (term_of concl) of |
845 (_ $ (_ $ (Const (@{const_name Bex}, _) $ _) |
846 (_ $ (_ $ (Const (@{const_name Bex}, _) $ _) |
846 $ (Const (@{const_name Bex}, _) $ _))) => |
847 $ (Const (@{const_name Bex}, _) $ _))) => rtac @{thm FUN_REL_I} 1 |
847 rtac @{thm FUN_REL_I} 1 |
|
848 | _ => no_tac) |
848 | _ => no_tac) |
849 *} |
849 *} |
850 |
850 |
851 ML {* (* Legacy *) |
851 ML {* (* Legacy *) |
852 fun needs_lift (rty as Type (rty_s, _)) ty = |
852 fun needs_lift (rty as Type (rty_s, _)) ty = |
963 |
963 |
964 (* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> APPLY_RSP provided type of t needs lifting *) |
964 (* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> APPLY_RSP provided type of t needs lifting *) |
965 DT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' |
965 DT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' |
966 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))), |
966 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))), |
967 |
967 |
968 (* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> Cong provided R = (op =) and t does not need lifting *) |
968 (* (op =) (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> Cong provided type of t does not need lifting *) |
|
969 (* merge with previous tactic *) |
969 DT ctxt "B" (Cong_Tac.cong_tac @{thm cong}), |
970 DT ctxt "B" (Cong_Tac.cong_tac @{thm cong}), |
970 |
971 |
971 (* (op =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
972 (* (op =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
972 DT ctxt "C" (rtac @{thm ext}), |
973 DT ctxt "C" (rtac @{thm ext}), |
973 |
974 |