src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML
changeset 57983 6edc3529bb4e
parent 57525 f9dd8a33f820
child 58634 9f10d82e8188
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML	Mon Aug 18 15:03:25 2014 +0200
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML	Mon Aug 18 17:19:58 2014 +0200
     1.3 @@ -22,13 +22,13 @@
     1.4    val mk_case_eq_if_tac: Proof.context -> int -> thm -> thm list -> thm list list ->
     1.5      thm list list -> tactic
     1.6    val mk_collapse_tac: Proof.context -> int -> thm -> thm list -> tactic
     1.7 -  val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic
     1.8 +  val mk_exhaust_disc_tac: int -> thm -> thm list -> tactic
     1.9 +  val mk_exhaust_sel_tac: int -> thm -> thm list -> tactic
    1.10    val mk_expand_tac: Proof.context -> int -> int list -> thm -> thm -> thm list ->
    1.11      thm list list list -> thm list list list -> tactic
    1.12 -  val mk_half_disc_exclude_tac: Proof.context -> int -> thm -> thm -> tactic
    1.13 +  val mk_half_distinct_disc_tac: Proof.context -> int -> thm -> thm -> tactic
    1.14    val mk_nchotomy_tac: int -> thm -> tactic
    1.15 -  val mk_other_half_disc_exclude_tac: thm -> tactic
    1.16 -  val mk_sel_exhaust_tac: int -> thm -> thm list -> tactic
    1.17 +  val mk_other_half_distinct_disc_tac: thm -> tactic
    1.18    val mk_split_tac: Proof.context -> thm -> thm list -> thm list list -> thm list list ->
    1.19      thm list list list -> tactic
    1.20    val mk_split_asm_tac: Proof.context -> thm -> tactic
    1.21 @@ -67,21 +67,21 @@
    1.22      (([etac notE, REPEAT_DETERM o rtac exI, atac], [REPEAT_DETERM o rtac exI, atac])
    1.23       |> k = 1 ? swap |> op @)));
    1.24  
    1.25 -fun mk_half_disc_exclude_tac ctxt m discD disc' =
    1.26 +fun mk_half_distinct_disc_tac ctxt m discD disc' =
    1.27    HEADGOAL (dtac discD THEN' REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac ctxt THEN'
    1.28      rtac disc');
    1.29  
    1.30 -fun mk_other_half_disc_exclude_tac half = HEADGOAL (etac @{thm contrapos_pn} THEN' etac half);
    1.31 +fun mk_other_half_distinct_disc_tac half = HEADGOAL (etac @{thm contrapos_pn} THEN' etac half);
    1.32  
    1.33 -fun mk_disc_or_sel_exhaust_tac n exhaust destIs =
    1.34 +fun mk_exhaust_disc_or_sel_tac n exhaust destIs =
    1.35    HEADGOAL (rtac exhaust THEN'
    1.36      EVERY' (map2 (fn k => fn destI => dtac destI THEN'
    1.37        select_prem_tac n (etac meta_mp) k THEN' atac) (1 upto n) destIs));
    1.38  
    1.39 -val mk_disc_exhaust_tac = mk_disc_or_sel_exhaust_tac;
    1.40 +val mk_exhaust_disc_tac = mk_exhaust_disc_or_sel_tac;
    1.41  
    1.42 -fun mk_sel_exhaust_tac n disc_exhaust collapses =
    1.43 -  mk_disc_or_sel_exhaust_tac n disc_exhaust collapses ORELSE
    1.44 +fun mk_exhaust_sel_tac n exhaust_disc collapses =
    1.45 +  mk_exhaust_disc_or_sel_tac n exhaust_disc collapses ORELSE
    1.46    HEADGOAL (etac meta_mp THEN' resolve_tac collapses);
    1.47  
    1.48  fun mk_collapse_tac ctxt m discD sels =
    1.49 @@ -92,17 +92,17 @@
    1.50         REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac ctxt THEN'
    1.51         SELECT_GOAL (unfold_thms_tac ctxt sels) THEN' rtac refl));
    1.52  
    1.53 -fun mk_expand_tac ctxt n ms udisc_exhaust vdisc_exhaust uncollapses disc_excludesss
    1.54 -    disc_excludesss' =
    1.55 +fun mk_expand_tac ctxt n ms uexhaust_disc vexhaust_disc uncollapses distinct_discsss
    1.56 +    distinct_discsss' =
    1.57    if ms = [0] then
    1.58      HEADGOAL (rtac (@{thm trans_sym} OF (replicate 2 (the_single uncollapses))) THEN'
    1.59 -      TRY o EVERY' [rtac udisc_exhaust, atac, rtac vdisc_exhaust, atac])
    1.60 +      TRY o EVERY' [rtac uexhaust_disc, atac, rtac vexhaust_disc, atac])
    1.61    else
    1.62      let val ks = 1 upto n in
    1.63 -      HEADGOAL (rtac udisc_exhaust THEN'
    1.64 -        EVERY' (map5 (fn k => fn m => fn disc_excludess => fn disc_excludess' => fn uuncollapse =>
    1.65 -          EVERY' [rtac (uuncollapse RS trans) THEN' TRY o atac, rtac sym, rtac vdisc_exhaust,
    1.66 -            EVERY' (map4 (fn k' => fn disc_excludes => fn disc_excludes' => fn vuncollapse =>
    1.67 +      HEADGOAL (rtac uexhaust_disc THEN'
    1.68 +        EVERY' (map5 (fn k => fn m => fn distinct_discss => fn distinct_discss' => fn uuncollapse =>
    1.69 +          EVERY' [rtac (uuncollapse RS trans) THEN' TRY o atac, rtac sym, rtac vexhaust_disc,
    1.70 +            EVERY' (map4 (fn k' => fn distinct_discs => fn distinct_discs' => fn vuncollapse =>
    1.71                EVERY'
    1.72                  (if k' = k then
    1.73                     [rtac (vuncollapse RS trans), TRY o atac] @
    1.74 @@ -113,11 +113,11 @@
    1.75                         REPEAT_DETERM_N (Int.max (0, m - 1)) o etac conjE,
    1.76                         asm_simp_tac (ss_only [] ctxt)])
    1.77                   else
    1.78 -                   [dtac (the_single (if k = n then disc_excludes else disc_excludes')),
    1.79 +                   [dtac (the_single (if k = n then distinct_discs else distinct_discs')),
    1.80                      etac (if k = n then @{thm iff_contradict(1)} else @{thm iff_contradict(2)}),
    1.81                      atac, atac]))
    1.82 -              ks disc_excludess disc_excludess' uncollapses)])
    1.83 -          ks ms disc_excludesss disc_excludesss' uncollapses))
    1.84 +              ks distinct_discss distinct_discss' uncollapses)])
    1.85 +          ks ms distinct_discsss distinct_discsss' uncollapses))
    1.86      end;
    1.87  
    1.88  fun mk_case_same_ctr_tac ctxt injects =