1.1 --- a/src/ZF/indrule.ML Tue Jul 16 15:48:27 1996 +0200
1.2 +++ b/src/ZF/indrule.ML Tue Jul 16 15:49:46 1996 +0200
1.3 @@ -72,6 +72,20 @@
1.4 val ind_prems = map (induct_prem (map (rpair pred) Inductive.rec_tms))
1.5 Inductive.intr_tms;
1.6
1.7 +(*Debugging code...
1.8 +val _ = writeln "ind_prems = ";
1.9 +val _ = seq (writeln o Sign.string_of_term sign) ind_prems;
1.10 +*)
1.11 +
1.12 +(*We use a MINIMAL simpset because others (such as FOL_ss) contain too many
1.13 + simplifications. If the premises get simplified, then the proofs will
1.14 + fail. *)
1.15 +val min_ss = empty_ss
1.16 + setmksimps (map mk_meta_eq o ZF_atomize o gen_all)
1.17 + setsolver (fn prems => resolve_tac (triv_rls@prems)
1.18 + ORELSE' assume_tac
1.19 + ORELSE' etac FalseE);
1.20 +
1.21 val quant_induct =
1.22 prove_goalw_cterm part_rec_defs
1.23 (cterm_of sign
1.24 @@ -81,7 +95,7 @@
1.25 [rtac (impI RS allI) 1,
1.26 DETERM (etac Intr_elim.raw_induct 1),
1.27 (*Push Part inside Collect*)
1.28 - asm_full_simp_tac (FOL_ss addsimps [Part_Collect]) 1,
1.29 + full_simp_tac (min_ss addsimps [Part_Collect]) 1,
1.30 REPEAT (FIRSTGOAL (eresolve_tac [CollectE, exE, conjE, disjE] ORELSE'
1.31 hyp_subst_tac)),
1.32 ind_tac (rev prems) (length prems) ]);
1.33 @@ -150,7 +164,7 @@
1.34 (*Simplification largely reduces the mutual induction rule to the
1.35 standard rule*)
1.36 val mut_ss =
1.37 - FOL_ss addsimps [Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff];
1.38 + min_ss addsimps [Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff];
1.39
1.40 val all_defs = Inductive.con_defs @ part_rec_defs;
1.41
1.42 @@ -174,8 +188,11 @@
1.43 rewrite_goals_tac all_defs THEN
1.44 simp_tac (mut_ss addsimps [Part_iff]) 1 THEN
1.45 IF_UNSOLVED (*simp_tac may have finished it off!*)
1.46 - ((*simplify assumptions, but don't accept new rewrite rules!*)
1.47 - asm_full_simp_tac (mut_ss setmksimps (fn _=>[])) 1 THEN
1.48 + ((*simplify assumptions*)
1.49 + (*some risk of excessive simplification here -- might have
1.50 + to identify the bare minimum set of rewrites*)
1.51 + full_simp_tac
1.52 + (mut_ss addsimps (conj_rews @ imp_rews @ quant_rews)) 1 THEN
1.53 (*unpackage and use "prem" in the corresponding place*)
1.54 REPEAT (rtac impI 1) THEN
1.55 rtac (rewrite_rule all_defs prem) 1 THEN