made split-rule tactic go beyond constructors with 20 arguments
authorblanchet
Sun May 03 18:14:11 2015 +0200 (2015-05-03)
changeset 6025198754695b421
parent 60250 baf2c8fddaa4
child 60252 2c468c062589
made split-rule tactic go beyond constructors with 20 arguments
src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Sun May 03 20:21:25 2015 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Sun May 03 18:14:11 2015 +0200
     1.3 @@ -37,6 +37,8 @@
     1.4  val split_connectI = @{thms allI impI conjI};
     1.5  val unfold_lets = @{thms Let_def[abs_def] split_beta}
     1.6  
     1.7 +fun clean_blast_tac ctxt = blast_tac (put_claset (claset_of @{theory_context HOL}) ctxt);
     1.8 +
     1.9  fun exhaust_inst_as_projs ctxt frees thm =
    1.10    let
    1.11      val num_frees = length frees;
     2.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Sun May 03 20:21:25 2015 +0200
     2.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Sun May 03 18:14:11 2015 +0200
     2.3 @@ -751,7 +751,7 @@
     2.4  
     2.5          fun prove_split selss goal =
     2.6            Goal.prove_sorry lthy [] [] goal (fn _ =>
     2.7 -            mk_split_tac lthy uexhaust_thm case_thms selss inject_thmss distinct_thmsss)
     2.8 +            mk_split_tac lthy ms uexhaust_thm case_thms selss inject_thmss distinct_thmsss)
     2.9            |> singleton (Proof_Context.export names_lthy lthy)
    2.10            |> Thm.close_derivation;
    2.11  
     3.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML	Sun May 03 20:21:25 2015 +0200
     3.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML	Sun May 03 18:14:11 2015 +0200
     3.3 @@ -7,7 +7,6 @@
     3.4  
     3.5  signature CTR_SUGAR_GENERAL_TACTICS =
     3.6  sig
     3.7 -  val clean_blast_tac: Proof.context -> int -> tactic
     3.8    val select_prem_tac: int -> (int -> tactic) -> int -> int -> tactic
     3.9    val unfold_thms_tac: Proof.context -> thm list -> tactic
    3.10  end;
    3.11 @@ -32,8 +31,8 @@
    3.12    val mk_half_distinct_disc_tac: Proof.context -> int -> thm -> thm -> tactic
    3.13    val mk_nchotomy_tac: int -> thm -> tactic
    3.14    val mk_other_half_distinct_disc_tac: thm -> tactic
    3.15 -  val mk_split_tac: Proof.context -> thm -> thm list -> thm list list -> thm list list ->
    3.16 -    thm list list list -> tactic
    3.17 +  val mk_split_tac: Proof.context -> int list -> thm -> thm list -> thm list list ->
    3.18 +    thm list list -> thm list list list -> tactic
    3.19    val mk_split_asm_tac: Proof.context -> thm -> tactic
    3.20    val mk_unique_disc_def_tac: int -> thm -> tactic
    3.21  end;
    3.22 @@ -45,7 +44,8 @@
    3.23  
    3.24  val meta_mp = @{thm meta_mp};
    3.25  
    3.26 -fun clean_blast_tac ctxt = blast_tac (put_claset (claset_of @{theory_context HOL}) ctxt);
    3.27 +fun clean_blast_depth_tac ctxt depth =
    3.28 +  depth_tac (put_claset (claset_of @{theory_context HOL}) ctxt) depth;
    3.29  
    3.30  fun select_prem_tac n tac k = DETERM o (EVERY' [REPEAT_DETERM_N (k - 1) o etac thin_rl,
    3.31    tac, REPEAT_DETERM_N (n - k) o etac thin_rl]);
    3.32 @@ -170,12 +170,14 @@
    3.33            rtac casex])
    3.34        cases (map2 (seq_conds if_P_or_not_P_OF n) (1 upto n) discss') selss));
    3.35  
    3.36 -fun mk_split_tac ctxt uexhaust cases selss injectss distinctsss =
    3.37 -  HEADGOAL (rtac uexhaust) THEN
    3.38 -  ALLGOALS (fn k => (hyp_subst_tac ctxt THEN'
    3.39 -     simp_tac (ss_only (@{thms simp_thms} @ cases @ nth selss (k - 1) @ nth injectss (k - 1) @
    3.40 -       flat (nth distinctsss (k - 1))) ctxt)) k) THEN
    3.41 -  ALLGOALS (clean_blast_tac ctxt);
    3.42 +fun mk_split_tac ctxt ms uexhaust cases selss injectss distinctsss =
    3.43 +  let val depth = fold Integer.max ms 0 in
    3.44 +    HEADGOAL (rtac uexhaust) THEN
    3.45 +    ALLGOALS (fn k => (hyp_subst_tac ctxt THEN'
    3.46 +       simp_tac (ss_only (@{thms simp_thms} @ cases @ nth selss (k - 1) @ nth injectss (k - 1) @
    3.47 +         flat (nth distinctsss (k - 1))) ctxt)) k) THEN
    3.48 +    ALLGOALS (clean_blast_depth_tac ctxt depth)
    3.49 +  end;
    3.50  
    3.51  val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex};
    3.52