summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Wed, 27 May 1998 12:22:32 +0200 | |

changeset 4971 | 09b8945cac07 |

parent 4970 | 8b65444edbb0 |

child 4972 | 7fe1d30c1374 |

more tracing

src/HOL/indrule.ML | file | annotate | diff | comparison | revisions | |

src/ZF/indrule.ML | file | annotate | diff | comparison | revisions |

--- a/src/HOL/indrule.ML Wed May 27 12:21:39 1998 +0200 +++ b/src/HOL/indrule.ML Wed May 27 12:22:32 1998 +0200 @@ -108,6 +108,11 @@ ind_tac (rev prems) (length prems)]) handle e => print_sign_exn sign e; +val _ = if !Ind_Syntax.trace then + (writeln "quant_induct = "; print_thm quant_induct) + else (); + + (*** Prove the simultaneous induction rule ***) (*Make distinct predicates for each inductive set. @@ -150,6 +155,14 @@ and mutual_induct_concl = Ind_Syntax.mk_Trueprop (fold_bal (app Ind_Syntax.conj) qconcls); +val _ = if !Ind_Syntax.trace then + (writeln ("induct_concl = " ^ + Sign.string_of_term sign induct_concl); + writeln ("mutual_induct_concl = " ^ + Sign.string_of_term sign mutual_induct_concl)) + else (); + + val lemma_tac = FIRST' [eresolve_tac [asm_rl, conjE, PartE, mp], resolve_tac [allI, impI, conjI, Part_eqI, refl], dresolve_tac [spec, mp, splitD]]; @@ -170,6 +183,11 @@ else (writeln " [ No mutual induction rule needed ]"; TrueI); +val _ = if !Ind_Syntax.trace then + (writeln "lemma = "; print_thm lemma) + else (); + + (*Mutual induction follows by freeness of Inl/Inr.*) (*Simplification largely reduces the mutual induction rule to the

--- a/src/ZF/indrule.ML Wed May 27 12:21:39 1998 +0200 +++ b/src/ZF/indrule.ML Wed May 27 12:22:32 1998 +0200 @@ -108,6 +108,11 @@ ORELSE' hyp_subst_tac)), ind_tac (rev prems) (length prems) ]); +val _ = if !Ind_Syntax.trace then + (writeln "quant_induct = "; print_thm quant_induct) + else (); + + (*** Prove the simultaneous induction rule ***) (*Make distinct predicates for each inductive set*) @@ -155,6 +160,14 @@ and mutual_induct_concl = FOLogic.mk_Trueprop(fold_bal (app FOLogic.conj) qconcls); +val _ = if !Ind_Syntax.trace then + (writeln ("induct_concl = " ^ + Sign.string_of_term sign induct_concl); + writeln ("mutual_induct_concl = " ^ + Sign.string_of_term sign mutual_induct_concl)) + else (); + + val lemma_tac = FIRST' [eresolve_tac [asm_rl, conjE, PartE, mp], resolve_tac [allI, impI, conjI, Part_eqI], dresolve_tac [spec, mp, Pr.fsplitD]]; @@ -174,6 +187,11 @@ else (writeln " [ No mutual induction rule needed ]"; TrueI); +val _ = if !Ind_Syntax.trace then + (writeln "lemma = "; print_thm lemma) + else (); + + (*Mutual induction follows by freeness of Inl/Inr.*) (*Simplification largely reduces the mutual induction rule to the @@ -189,7 +207,8 @@ where t==Part(tf,Inl) and f==Part(tf,Inr) to list({v: tf. P_t(v)}). Instead the following rules extract the relevant conjunct. *) -val cmonos = [subset_refl RS Collect_mono] RL Inductive.monos RLN (2,[rev_subsetD]); +val cmonos = [subset_refl RS Collect_mono] RL Inductive.monos + RLN (2,[rev_subsetD]); (*Minimizes backtracking by delivering the correct premise to each goal*) fun mutual_ind_tac [] 0 = all_tac