Added rotation to exhaust_tac.
authornipkow
Thu May 22 13:05:52 1997 +0200 (1997-05-22)
changeset 32928b143c196d42
parent 3291 cf322b5c59aa
child 3293 c05f73cf3227
Added rotation to exhaust_tac.
src/HOL/List.ML
src/HOL/NatDef.ML
src/HOL/datatype.ML
     1.1 --- a/src/HOL/List.ML	Thu May 22 12:59:08 1997 +0200
     1.2 +++ b/src/HOL/List.ML	Thu May 22 13:05:52 1997 +0200
     1.3 @@ -464,7 +464,7 @@
     1.4  by(exhaust_tac "n" 1);
     1.5   by(Blast_tac 1);
     1.6  by(exhaust_tac "i" 1);
     1.7 -by(ALLGOALS (hyp_subst_tac THEN' Asm_full_simp_tac));
     1.8 +by(ALLGOALS Asm_full_simp_tac);
     1.9  qed_spec_mp "nth_take";
    1.10  Addsimps [nth_take];
    1.11  
     2.1 --- a/src/HOL/NatDef.ML	Thu May 22 12:59:08 1997 +0200
     2.2 +++ b/src/HOL/NatDef.ML	Thu May 22 13:05:52 1997 +0200
     2.3 @@ -70,10 +70,12 @@
     2.4  qed "natE";
     2.5  
     2.6  (*Install 'automatic' induction tactic, pretending nat is a datatype *)
     2.7 -(*except for induct_tac, everything is dummy*)
     2.8 +(*except for induct_tac and exhaust_tac, everything is dummy*)
     2.9  datatypes := [("nat",{case_const = Bound 0, case_rewrites = [],
    2.10    constructors = [], induct_tac = nat_ind_tac,
    2.11 -  exhaustion = natE, exhaust_tac = fn v => res_inst_tac [("n",v)] natE,
    2.12 +  exhaustion = natE,
    2.13 +  exhaust_tac = fn v => ALLNEWSUBGOALS (res_inst_tac [("n",v)] natE)
    2.14 +                                       (rotate_tac ~1),
    2.15    nchotomy = flexpair_def, case_cong = flexpair_def})];
    2.16  
    2.17  
     3.1 --- a/src/HOL/datatype.ML	Thu May 22 12:59:08 1997 +0200
     3.2 +++ b/src/HOL/datatype.ML	Thu May 22 13:05:52 1997 +0200
     3.3 @@ -5,6 +5,11 @@
     3.4     Copyright 1995 TU Muenchen
     3.5  *)
     3.6  
     3.7 +(* should go into Pure *)
     3.8 +fun ALLNEWSUBGOALS tac tacf i =
     3.9 +  STATE (fn state0 => tac i THEN
    3.10 +  STATE (fn state1 => let val d = nprems_of state1 - nprems_of state0
    3.11 +                      in EVERY(map tacf ((i+d) downto i)) end));
    3.12  
    3.13  (*used for constructor parameters*)
    3.14  datatype dt_type = dtVar of string |
    3.15 @@ -858,7 +863,9 @@
    3.16       val {nchotomy,case_cong} = case_thms sign case_rewrites itac
    3.17       val exhaustion = mk_exhaust nchotomy
    3.18       val exh_var = exhaust_var exhaustion;
    3.19 -     fun exhaust_tac a = res_inst_tac [(exh_var,a)] exhaustion;
    3.20 +     fun exhaust_tac a =
    3.21 +           ALLNEWSUBGOALS (res_inst_tac [(exh_var,a)] exhaustion)
    3.22 +                          (rotate_tac ~1);
    3.23       fun induct_tac a i =
    3.24             STATE(fn st =>
    3.25               (if Datatype.occs_in_prems a i st