--- a/src/HOL/BNF/Tools/bnf_comp.ML Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML Wed Sep 26 10:00:59 2012 +0200
@@ -167,7 +167,7 @@
|> sort (rev_order o int_ord o pairself fst)
|> map snd) @ [map_id_of_bnf outer];
in
- (EVERY' (map (fn thm => subst_tac ctxt [thm]) thms) THEN' rtac refl) 1
+ (EVERY' (map (fn thm => subst_tac ctxt NONE [thm]) thms) THEN' rtac refl) 1
end;
fun map_comp_tac _ =
--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML Wed Sep 26 10:00:59 2012 +0200
@@ -106,7 +106,7 @@
fun mk_srel_Id_tac n srel_Gr map_id {context = ctxt, prems = _} =
unfold_thms_tac ctxt [srel_Gr, @{thm Id_alt}] THEN
- subst_tac ctxt [map_id] 1 THEN
+ subst_tac ctxt NONE [map_id] 1 THEN
(if n = 0 then rtac refl 1
else EVERY' [rtac @{thm arg_cong2[of _ _ _ _ Gr]},
rtac equalityI, rtac subset_UNIV, rtac subsetI, rtac CollectI,
--- a/src/HOL/BNF/Tools/bnf_fp_sugar_tactics.ML Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_sugar_tactics.ML Wed Sep 26 10:00:59 2012 +0200
@@ -95,10 +95,10 @@
fun mk_corec_like_tac corec_like_defs map_ids ctor_dtor_corec_like pre_map_def ctr_def ctxt =
unfold_thms_tac ctxt (ctr_def :: corec_like_defs) THEN
- subst_tac ctxt [ctor_dtor_corec_like] 1 THEN asm_simp_tac corec_like_ss 1 THEN
+ subst_tac ctxt NONE [ctor_dtor_corec_like] 1 THEN asm_simp_tac corec_like_ss 1 THEN
unfold_thms_tac ctxt (pre_map_def :: sum_prod_thms_map @ map_ids) THEN
unfold_thms_tac ctxt @{thms id_def} THEN
- TRY ((rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1);
+ TRY ((rtac refl ORELSE' subst_tac ctxt NONE @{thms unit_eq} THEN' rtac refl) 1);
fun mk_disc_corec_like_iff_tac case_splits' corec_likes discs ctxt =
EVERY (map3 (fn case_split_tac => fn corec_like_thm => fn disc =>
--- a/src/HOL/BNF/Tools/bnf_tactics.ML Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_tactics.ML Wed Sep 26 10:00:59 2012 +0200
@@ -13,8 +13,7 @@
val prefer_tac: int -> tactic
val select_prem_tac: int -> (int -> tactic) -> int -> int -> tactic
val fo_rtac: thm -> Proof.context -> int -> tactic
- val subst_asm_tac: Proof.context -> thm list -> int -> tactic
- val subst_tac: Proof.context -> thm list -> int -> tactic
+ val subst_tac: Proof.context -> int list option -> thm list -> int -> tactic
val substs_tac: Proof.context -> thm list -> int -> tactic
val unfold_thms_tac: Proof.context -> thm list -> tactic
val mk_unfold_thms_then_tac: Proof.context -> thm list -> ('a -> tactic) -> 'a -> tactic
@@ -61,10 +60,9 @@
fun mk_unfold_thms_then_tac lthy defs tac x = unfold_thms_tac lthy defs THEN tac x;
-(*unlike "unfold_thms_tac", succeeds when the RHS contains schematic variables not in the LHS*)
-fun subst_asm_tac ctxt = EqSubst.eqsubst_asm_tac ctxt [0];
-fun subst_tac ctxt = EqSubst.eqsubst_tac ctxt [0];
-fun substs_tac ctxt = REPEAT_DETERM oo subst_tac ctxt;
+(*unlike "unfold_thms_tac", these succeed when the RHS contains schematic variables not in the LHS*)
+fun subst_tac ctxt = EqSubst.eqsubst_tac ctxt o the_default [0];
+fun substs_tac ctxt = REPEAT_DETERM oo subst_tac ctxt NONE;
(* Theorems for open typedefs with UNIV as representing set *)
@@ -103,7 +101,7 @@
fun mk_ctor_or_dtor_rel_tac srel_def IJrel_defs IJsrel_defs dtor_srel {context = ctxt, prems = _} =
unfold_thms_tac ctxt IJrel_defs THEN
- subst_tac ctxt [unfold_thms ctxt (IJrel_defs @ IJsrel_defs @
+ subst_tac ctxt NONE [unfold_thms ctxt (IJrel_defs @ IJsrel_defs @
@{thms Collect_pair_mem_eq mem_Collect_eq fst_conv snd_conv}) dtor_srel] 1 THEN
unfold_thms_tac ctxt (srel_def ::
@{thms Collect_fst_snd_mem_eq mem_Collect_eq pair_mem_Collect_split fst_conv snd_conv
--- a/src/HOL/BNF/Tools/bnf_wrap.ML Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_wrap.ML Wed Sep 26 10:00:59 2012 +0200
@@ -493,9 +493,6 @@
mk_disc_exhaust_tac n exhaust_thm discI_thms)
end;
- val disc_exhaust_thms =
- if has_alternate_disc_def orelse no_discs_at_all then [] else [disc_exhaust_thm];
-
val (collapse_thms, collapse_thm_opts) =
let
fun mk_goal ctr udisc usels =
@@ -553,7 +550,7 @@
end;
in
(all_sel_thms, sel_thmss, disc_thmss, disc_thms, discI_thms, disc_exclude_thms,
- disc_exhaust_thms, collapse_thms, expand_thms, case_eq_thms)
+ [disc_exhaust_thm], collapse_thms, expand_thms, case_eq_thms)
end;
val (case_cong_thm, weak_case_cong_thm) =
--- a/src/HOL/BNF/Tools/bnf_wrap_tactics.ML Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_wrap_tactics.ML Wed Sep 26 10:00:59 2012 +0200
@@ -41,7 +41,7 @@
EVERY' [rtac iffI, rtac uexhaust, REPEAT_DETERM_N m o rtac exI, atac, rtac refl] 1;
fun mk_alternate_disc_def_tac ctxt k other_disc_def distinct uexhaust =
- EVERY' ([subst_tac ctxt [other_disc_def], rtac @{thm iffI_np}, REPEAT_DETERM o etac exE,
+ EVERY' ([subst_tac ctxt NONE [other_disc_def], rtac @{thm iffI_np}, REPEAT_DETERM o etac exE,
hyp_subst_tac, SELECT_GOAL (unfold_thms_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI,
rtac distinct, rtac uexhaust] @
(([etac notE, REPEAT_DETERM o rtac exI, atac], [REPEAT_DETERM o rtac exI, atac])
@@ -76,7 +76,7 @@
in
(rtac udisc_exhaust THEN'
EVERY' (map5 (fn k => fn m => fn disc_excludess => fn disc_excludess' => fn uuncollapse =>
- EVERY' [if m = 0 then K all_tac else subst_tac ctxt [uuncollapse] THEN' maybe_atac,
+ EVERY' [if m = 0 then K all_tac else subst_tac ctxt NONE [uuncollapse] THEN' maybe_atac,
rtac sym, rtac vdisc_exhaust,
EVERY' (map4 (fn k' => fn disc_excludes => fn disc_excludes' => fn vuncollapse =>
EVERY'
@@ -84,7 +84,7 @@
if m = 0 then
[hyp_subst_tac, rtac refl]
else
- [subst_tac ctxt [vuncollapse], maybe_atac,
+ [subst_tac ctxt NONE [vuncollapse], maybe_atac,
if n = 1 then K all_tac else EVERY' [dtac meta_mp, atac, dtac meta_mp, atac],
REPEAT_DETERM_N (Int.max (0, m - 1)) o etac conjE, asm_simp_tac (ss_only [])]
else
@@ -107,6 +107,7 @@
val naked_ctxt = Proof_Context.init_global @{theory HOL};
+(* TODO: More precise "simp_thms"; get rid of "blast_tac" *)
fun mk_split_tac uexhaust cases injectss distinctsss =
rtac uexhaust 1 THEN
ALLGOALS (fn k => (hyp_subst_tac THEN'