took out unreliable 'blast' from tactic altogether
authorblanchet
Sat May 09 14:10:10 2015 +0200 (2015-05-09)
changeset 60279351536745704
parent 60278 2a9bc6447779
child 60280 05fe9bdc4f8f
took out unreliable 'blast' from tactic altogether
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri May 08 16:14:02 2015 +0200
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Sat May 09 14:10:10 2015 +0200
     1.3 @@ -397,7 +397,13 @@
     1.4  
     1.5      val ctrs0 = map (prep_term no_defs_lthy) raw_ctrs;
     1.6  
     1.7 -    val Type (fcT_name, As0) = body_type (fastype_of (hd ctrs0));
     1.8 +    val (fcT_name, As0) =
     1.9 +      (case body_type (fastype_of (hd ctrs0)) of
    1.10 +        Type T' => T'
    1.11 +      | _ => error "Expected type constructor in body type of constructor");
    1.12 +    val _ = forall ((fn Type (T_name, _) => T_name = fcT_name | _ => false) o body_type
    1.13 +      o fastype_of) (tl ctrs0) orelse error "Constructors not constructing same type";
    1.14 +
    1.15      val fc_b_name = Long_Name.base_name fcT_name;
    1.16      val fc_b = Binding.name fc_b_name;
    1.17  
    1.18 @@ -675,7 +681,7 @@
    1.19  
    1.20      val goalss = [exhaust_goal] :: inject_goalss @ half_distinct_goalss;
    1.21  
    1.22 -    fun after_qed (thmss0 as [exhaust_thm] :: thmss) lthy =
    1.23 +    fun after_qed ([exhaust_thm] :: thmss) lthy =
    1.24        let
    1.25          val ((inject_thms, inject_thmss), half_distinct_thmss) = chop n thmss |>> `flat;
    1.26  
     2.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML	Fri May 08 16:14:02 2015 +0200
     2.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML	Sat May 09 14:10:10 2015 +0200
     2.3 @@ -44,9 +44,6 @@
     2.4  
     2.5  val meta_mp = @{thm meta_mp};
     2.6  
     2.7 -fun clean_blast_depth_tac ctxt depth =
     2.8 -  depth_tac (put_claset (claset_of @{theory_context HOL}) ctxt) depth;
     2.9 -
    2.10  fun select_prem_tac n tac k = DETERM o (EVERY' [REPEAT_DETERM_N (k - 1) o etac thin_rl,
    2.11    tac, REPEAT_DETERM_N (n - k) o etac thin_rl]);
    2.12  
    2.13 @@ -176,7 +173,10 @@
    2.14      ALLGOALS (fn k => (hyp_subst_tac ctxt THEN'
    2.15         simp_tac (ss_only (@{thms simp_thms} @ cases @ nth selss (k - 1) @ nth injectss (k - 1) @
    2.16           flat (nth distinctsss (k - 1))) ctxt)) k) THEN
    2.17 -    ALLGOALS (clean_blast_depth_tac ctxt depth)
    2.18 +    ALLGOALS (etac thin_rl THEN' rtac iffI THEN'
    2.19 +      REPEAT_DETERM o rtac allI THEN' rtac impI THEN' REPEAT_DETERM o etac conjE THEN'
    2.20 +      hyp_subst_tac ctxt THEN' atac THEN' REPEAT_DETERM o etac allE THEN' etac impE THEN'
    2.21 +      REPEAT_DETERM o (rtac conjI THEN' rtac refl) THEN' rtac refl THEN' atac)
    2.22    end;
    2.23  
    2.24  val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex};