Fixed bug in inductive sections to allow disjunctive premises;
authorpaulson
Fri Apr 10 13:15:28 1998 +0200 (1998-04-10 ago)
changeset 480402b7c759159b
parent 4803 8428d4699d58
child 4805 20d292c05e6c
Fixed bug in inductive sections to allow disjunctive premises;
added tracing flag trace_induct
src/ZF/add_ind_def.ML
src/ZF/ind_syntax.ML
src/ZF/indrule.ML
     1.1 --- a/src/ZF/add_ind_def.ML	Thu Apr 09 12:31:35 1998 +0200
     1.2 +++ b/src/ZF/add_ind_def.ML	Fri Apr 10 13:15:28 1998 +0200
     1.3 @@ -165,8 +165,11 @@
     1.4               | _ => rec_tms ~~          (*define the sets as Parts*)
     1.5                      map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts));
     1.6  
     1.7 -    val dummy = seq (writeln o Sign.string_of_term sign o #2) axpairs
     1.8 -  
     1.9 +    (*tracing: print the fixedpoint definition*)
    1.10 +    val _ = if !Ind_Syntax.trace then
    1.11 +		seq (writeln o Sign.string_of_term sign o #2) axpairs
    1.12 +            else ()
    1.13 +
    1.14    in  thy |> PureThy.add_store_defs_i axpairs  end
    1.15  
    1.16  
     2.1 --- a/src/ZF/ind_syntax.ML	Thu Apr 09 12:31:35 1998 +0200
     2.2 +++ b/src/ZF/ind_syntax.ML	Fri Apr 10 13:15:28 1998 +0200
     2.3 @@ -12,6 +12,9 @@
     2.4  structure Ind_Syntax =
     2.5  struct
     2.6  
     2.7 +(*Print tracing messages during processing of "inductive" theory sections*)
     2.8 +val trace = ref false;
     2.9 +
    2.10  (** Abstract syntax definitions for ZF **)
    2.11  
    2.12  val iT = Type("i",[]);
    2.13 @@ -124,3 +127,5 @@
    2.14  
    2.15  end;
    2.16  
    2.17 +
    2.18 +val trace_induct = Ind_Syntax.trace;
     3.1 --- a/src/ZF/indrule.ML	Thu Apr 09 12:31:35 1998 +0200
     3.2 +++ b/src/ZF/indrule.ML	Fri Apr 10 13:15:28 1998 +0200
     3.3 @@ -62,7 +62,7 @@
     3.4    in list_all_free (quantfrees, Logic.list_implies (iprems,concl)) end
     3.5    handle Bind => error"Recursion term not found in conclusion";
     3.6  
     3.7 -(*Reduces backtracking by delivering the correct premise to each goal.
     3.8 +(*Minimizes backtracking by delivering the correct premise to each goal.
     3.9    Intro rules with extra Vars in premises still cause some backtracking *)
    3.10  fun ind_tac [] 0 = all_tac
    3.11    | ind_tac(prem::prems) i = 
    3.12 @@ -74,13 +74,15 @@
    3.13  val ind_prems = map (induct_prem (map (rpair pred) Inductive.rec_tms)) 
    3.14                      Inductive.intr_tms;
    3.15  
    3.16 -(*Debugging code...
    3.17 -val _ = writeln "ind_prems = ";
    3.18 -val _ = seq (writeln o Sign.string_of_term sign) ind_prems;
    3.19 -*)
    3.20 +val _ = if !Ind_Syntax.trace then 
    3.21 +            (writeln "ind_prems = ";
    3.22 +	     seq (writeln o Sign.string_of_term sign) ind_prems;
    3.23 +	     writeln "raw_induct = "; print_thm Intr_elim.raw_induct)
    3.24 +        else ();
    3.25 +
    3.26  
    3.27  (*We use a MINIMAL simpset because others (such as FOL_ss) contain too many
    3.28 -  simplifications.  If the premises get simplified, then the proofs will 
    3.29 +  simplifications.  If the premises get simplified, then the proofs could 
    3.30    fail.  *)
    3.31  val min_ss = empty_ss
    3.32        setmksimps (map mk_meta_eq o ZF_atomize o gen_all)
    3.33 @@ -98,8 +100,12 @@
    3.34          DETERM (etac Intr_elim.raw_induct 1),
    3.35          (*Push Part inside Collect*)
    3.36          full_simp_tac (min_ss addsimps [Part_Collect]) 1,
    3.37 -        REPEAT (FIRSTGOAL (eresolve_tac [CollectE, exE, conjE, disjE] ORELSE'
    3.38 -                           hyp_subst_tac)),
    3.39 +        (*This CollectE and disjE separates out the introduction rules*)
    3.40 +	REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE])),
    3.41 +	(*Now break down the individual cases.  No disjE here in case
    3.42 +          some premise involves disjunction.*)
    3.43 +        REPEAT (FIRSTGOAL (eresolve_tac [CollectE, exE, conjE] 
    3.44 +                           ORELSE' hyp_subst_tac)),
    3.45          ind_tac (rev prems) (length prems) ]);
    3.46  
    3.47  (*** Prove the simultaneous induction rule ***)
    3.48 @@ -165,7 +171,8 @@
    3.49  	     [cut_facts_tac prems 1, 
    3.50  	      REPEAT (rewrite_goals_tac [Pr.split_eq] THEN
    3.51  		      lemma_tac 1)]))
    3.52 -  else TrueI;
    3.53 +  else (writeln "  [ No mutual induction rule needed ]";
    3.54 +        TrueI);
    3.55  
    3.56  (*Mutual induction follows by freeness of Inl/Inr.*)
    3.57  
    3.58 @@ -184,7 +191,7 @@
    3.59  *)
    3.60  val cmonos = [subset_refl RS Collect_mono] RL Inductive.monos RLN (2,[rev_subsetD]);
    3.61  
    3.62 -(*Avoids backtracking by delivering the correct premise to each goal*)
    3.63 +(*Minimizes backtracking by delivering the correct premise to each goal*)
    3.64  fun mutual_ind_tac [] 0 = all_tac
    3.65    | mutual_ind_tac(prem::prems) i = 
    3.66        DETERM