Fixed bug involving inductive definitions having equalities in the premises,
authorpaulson
Fri Oct 04 15:23:12 2002 +0200 (2002-10-04 ago)
changeset 13626282fbabec862
parent 13625 ca86e84ce200
child 13627 67b0b7500a9d
Fixed bug involving inductive definitions having equalities in the premises,
e.g. n = Suc(m).
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Oct 04 09:56:48 2002 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Oct 04 15:23:12 2002 +0200
     1.3 @@ -31,6 +31,7 @@
     1.4  signature INDUCTIVE_PACKAGE =
     1.5  sig
     1.6    val quiet_mode: bool ref
     1.7 +  val trace: bool ref
     1.8    val unify_consts: Sign.sg -> term list -> term list -> term list * term list
     1.9    val split_rule_vars: term list -> thm -> thm
    1.10    val get_inductive: theory -> string -> ({names: string list, coind: bool} *
    1.11 @@ -165,6 +166,7 @@
    1.12  (** misc utilities **)
    1.13  
    1.14  val quiet_mode = ref false;
    1.15 +val trace = ref false;  (*for debugging*)
    1.16  fun message s = if ! quiet_mode then () else writeln s;
    1.17  fun clean_message s = if ! quick_and_dirty then () else message s;
    1.18  
    1.19 @@ -412,6 +414,7 @@
    1.20        end;
    1.21  
    1.22      val ind_prems = map mk_ind_prem intr_ts;
    1.23 +
    1.24      val factors = foldl (mg_prod_factors preds) ([], ind_prems);
    1.25  
    1.26      (* make conclusions for induction rules *)
    1.27 @@ -624,6 +627,11 @@
    1.28      val (preds, ind_prems, mutual_ind_concl, factors) =
    1.29        mk_indrule cs cTs params intr_ts;
    1.30  
    1.31 +    val dummy = if !trace then
    1.32 +		(writeln "ind_prems = ";
    1.33 +		 seq (writeln o Sign.string_of_term sign) ind_prems)
    1.34 +	    else ();
    1.35 +
    1.36      (* make predicate for instantiation of abstract induction rule *)
    1.37  
    1.38      fun mk_ind_pred _ [P] = P
    1.39 @@ -651,20 +659,27 @@
    1.40               nth_elem (find_index_eq c cs, preds)))))
    1.41          (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites, rtac refl 1])) cs;
    1.42  
    1.43 +    val raw_fp_induct = (mono RS (fp_def RS def_lfp_induct));
    1.44 +
    1.45 +    val dummy = if !trace then
    1.46 +		(writeln "raw_fp_induct = "; print_thm raw_fp_induct)
    1.47 +	    else ();
    1.48 +
    1.49      val induct = quick_and_dirty_prove_goalw_cterm thy [inductive_conj_def] (Thm.cterm_of sign
    1.50        (Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
    1.51          [rtac (impI RS allI) 1,
    1.52 -         DETERM (etac (mono RS (fp_def RS def_lfp_induct)) 1),
    1.53 +         DETERM (etac raw_fp_induct 1),
    1.54           rewrite_goals_tac (map mk_meta_eq (vimage_Int::Int_Collect::vimage_simps)),
    1.55           fold_goals_tac rec_sets_defs,
    1.56           (*This CollectE and disjE separates out the introduction rules*)
    1.57           REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE, exE])),
    1.58           (*Now break down the individual cases.  No disjE here in case
    1.59             some premise involves disjunction.*)
    1.60 -         REPEAT (FIRSTGOAL (etac conjE ORELSE' hyp_subst_tac)),
    1.61 -         rewrite_goals_tac sum_case_rewrites,
    1.62 +         REPEAT (FIRSTGOAL (etac conjE)),
    1.63 +         ALLGOALS (asm_simp_tac (HOL_basic_ss addsimps sum_case_rewrites)),
    1.64           EVERY (map (fn prem =>
    1.65 -           DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
    1.66 +			DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1 APPEND 
    1.67 +						hyp_subst_tac 1)) prems)]);
    1.68  
    1.69      val lemma = quick_and_dirty_prove_goalw_cterm thy rec_sets_defs (Thm.cterm_of sign
    1.70        (Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems =>