src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML
changeset 60251 98754695b421
parent 59498 50b60f501b05
child 60279 351536745704
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML	Sun May 03 20:21:25 2015 +0200
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML	Sun May 03 18:14:11 2015 +0200
     1.3 @@ -7,7 +7,6 @@
     1.4  
     1.5  signature CTR_SUGAR_GENERAL_TACTICS =
     1.6  sig
     1.7 -  val clean_blast_tac: Proof.context -> int -> tactic
     1.8    val select_prem_tac: int -> (int -> tactic) -> int -> int -> tactic
     1.9    val unfold_thms_tac: Proof.context -> thm list -> tactic
    1.10  end;
    1.11 @@ -32,8 +31,8 @@
    1.12    val mk_half_distinct_disc_tac: Proof.context -> int -> thm -> thm -> tactic
    1.13    val mk_nchotomy_tac: int -> thm -> tactic
    1.14    val mk_other_half_distinct_disc_tac: thm -> tactic
    1.15 -  val mk_split_tac: Proof.context -> thm -> thm list -> thm list list -> thm list list ->
    1.16 -    thm list list list -> tactic
    1.17 +  val mk_split_tac: Proof.context -> int list -> thm -> thm list -> thm list list ->
    1.18 +    thm list list -> thm list list list -> tactic
    1.19    val mk_split_asm_tac: Proof.context -> thm -> tactic
    1.20    val mk_unique_disc_def_tac: int -> thm -> tactic
    1.21  end;
    1.22 @@ -45,7 +44,8 @@
    1.23  
    1.24  val meta_mp = @{thm meta_mp};
    1.25  
    1.26 -fun clean_blast_tac ctxt = blast_tac (put_claset (claset_of @{theory_context HOL}) ctxt);
    1.27 +fun clean_blast_depth_tac ctxt depth =
    1.28 +  depth_tac (put_claset (claset_of @{theory_context HOL}) ctxt) depth;
    1.29  
    1.30  fun select_prem_tac n tac k = DETERM o (EVERY' [REPEAT_DETERM_N (k - 1) o etac thin_rl,
    1.31    tac, REPEAT_DETERM_N (n - k) o etac thin_rl]);
    1.32 @@ -170,12 +170,14 @@
    1.33            rtac casex])
    1.34        cases (map2 (seq_conds if_P_or_not_P_OF n) (1 upto n) discss') selss));
    1.35  
    1.36 -fun mk_split_tac ctxt uexhaust cases selss injectss distinctsss =
    1.37 -  HEADGOAL (rtac uexhaust) THEN
    1.38 -  ALLGOALS (fn k => (hyp_subst_tac ctxt THEN'
    1.39 -     simp_tac (ss_only (@{thms simp_thms} @ cases @ nth selss (k - 1) @ nth injectss (k - 1) @
    1.40 -       flat (nth distinctsss (k - 1))) ctxt)) k) THEN
    1.41 -  ALLGOALS (clean_blast_tac ctxt);
    1.42 +fun mk_split_tac ctxt ms uexhaust cases selss injectss distinctsss =
    1.43 +  let val depth = fold Integer.max ms 0 in
    1.44 +    HEADGOAL (rtac uexhaust) THEN
    1.45 +    ALLGOALS (fn k => (hyp_subst_tac ctxt THEN'
    1.46 +       simp_tac (ss_only (@{thms simp_thms} @ cases @ nth selss (k - 1) @ nth injectss (k - 1) @
    1.47 +         flat (nth distinctsss (k - 1))) ctxt)) k) THEN
    1.48 +    ALLGOALS (clean_blast_depth_tac ctxt depth)
    1.49 +  end;
    1.50  
    1.51  val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex};
    1.52