Now Datatype.occs_in_prems prints the necessary warning ITSELF.
authorpaulson
Wed Jul 23 11:52:22 1997 +0200 (1997-07-23)
changeset 3564f886dbd91ee5
parent 3563 c4f13747489f
child 3565 c64410e701fb
Now Datatype.occs_in_prems prints the necessary warning ITSELF.

It is also easier to invoke and even works if the induction variable
is a parameter (rather than a free variable).
src/HOL/datatype.ML
     1.1 --- a/src/HOL/datatype.ML	Wed Jul 23 11:50:26 1997 +0200
     1.2 +++ b/src/HOL/datatype.ML	Wed Jul 23 11:52:22 1997 +0200
     1.3 @@ -429,12 +429,15 @@
     1.4             |> add_axioms rules, add_primrec, size_eqns)
     1.5      end
     1.6  
     1.7 -(*Check if the (induction) variable occurs among the premises, which
     1.8 -  usually signals a mistake *)
     1.9 -fun occs_in_prems a i state =
    1.10 -  let val (_, _, Bi, _) = dest_state(state,i)
    1.11 -      val prems = Logic.strip_assums_hyp Bi
    1.12 -  in a  mem  map (#1 o dest_Free) (foldr add_term_frees (prems,[])) end;
    1.13 +(*Warn if the (induction) variable occurs Free among the premises, which
    1.14 +  usually signals a mistake.  But calls the tactic either way!*)
    1.15 +fun occs_in_prems tacf a = 
    1.16 +  SUBGOAL (fn (Bi,i) =>
    1.17 +	   (if  exists (fn Free(a',_) => a=a')
    1.18 +	              (foldr add_term_frees (#2 (strip_context Bi), []))
    1.19 +	     then warning "Induction variable occurs also among premises!"
    1.20 +	     else ();
    1.21 +	    tacf a i));
    1.22  
    1.23  end;
    1.24  
    1.25 @@ -879,11 +882,7 @@
    1.26       fun exhaust_tac a =
    1.27             ALLNEWSUBGOALS (res_inst_tac [(exh_var,a)] exhaustion)
    1.28                            (rotate_tac ~1);
    1.29 -     fun induct_tac a i st = st |>
    1.30 -             (if Datatype.occs_in_prems a i st
    1.31 -              then warning "Induction variable occurs also among premises!"
    1.32 -              else ();
    1.33 -              itac a i)
    1.34 +     val induct_tac = Datatype.occs_in_prems itac 
    1.35   in
    1.36    (ty, {constructors = map(fn s => const s handle _ => const("op "^s)) cl,
    1.37          case_const = const (ty^"_case"),