Uses minimal simpset (min_ss) and full_simp_tac
authorpaulson
Mon Jul 15 14:54:37 1996 +0200 (1996-07-15)
changeset 1861505b104f675a
parent 1860 71bfeecfa96c
child 1862 74d4ae2f6fc3
Uses minimal simpset (min_ss) and full_simp_tac
instead of asm_full_simp_tac to prevent excessive simplification, which
can cause proofs to fail
src/HOL/indrule.ML
     1.1 --- a/src/HOL/indrule.ML	Mon Jul 15 12:36:56 1996 +0200
     1.2 +++ b/src/HOL/indrule.ML	Mon Jul 15 14:54:37 1996 +0200
     1.3 @@ -81,6 +81,15 @@
     1.4  val _ = seq (writeln o Sign.string_of_term sign) ind_prems;
     1.5  *)
     1.6  
     1.7 +(*We use a MINIMAL simpset because others (such as HOL_ss) contain too many
     1.8 +  simplifications.  If the premises get simplified, then the proofs will 
     1.9 +  fail.  This arose with a premise of the form {(F n,G n)|n . True}, which
    1.10 +  expanded to something containing ...&True. *)
    1.11 +val min_ss = empty_ss
    1.12 +      setmksimps (mksimps mksimps_pairs)
    1.13 +      setsolver (fn prems => resolve_tac (TrueI::refl::prems) ORELSE' atac
    1.14 +                             ORELSE' etac FalseE);
    1.15 +
    1.16  val quant_induct = 
    1.17      prove_goalw_cterm part_rec_defs 
    1.18        (cterm_of sign 
    1.19 @@ -90,7 +99,7 @@
    1.20        (fn prems =>
    1.21         [rtac (impI RS allI) 1,
    1.22          DETERM (etac Intr_elim.raw_induct 1),
    1.23 -        asm_full_simp_tac (HOL_ss addsimps [Part_Collect]) 1,
    1.24 +        full_simp_tac (min_ss addsimps [Part_Collect]) 1,
    1.25          REPEAT (FIRSTGOAL (eresolve_tac [IntE, CollectE, exE, conjE, disjE] 
    1.26                             ORELSE' hyp_subst_tac)),
    1.27          ind_tac (rev prems) (length prems)])
    1.28 @@ -156,8 +165,7 @@
    1.29  
    1.30  (*Simplification largely reduces the mutual induction rule to the 
    1.31    standard rule*)
    1.32 -val mut_ss = simpset_of "Fun"
    1.33 -             addsimps [Inl_Inr_eq, Inr_Inl_eq, Inl_eq, Inr_eq, split];
    1.34 +val mut_ss = min_ss addsimps [Inl_Inr_eq, Inr_Inl_eq, Inl_eq, Inr_eq, split];
    1.35  
    1.36  val all_defs = [split RS eq_reflection] @ Inductive.con_defs @ part_rec_defs;
    1.37