src/ZF/indrule.ML
 changeset 516 1957113f0d7d parent 366 5b6e4340085b child 543 e961b2092869
```--- a/src/ZF/indrule.ML	Fri Aug 12 12:28:46 1994 +0200
+++ b/src/ZF/indrule.ML	Fri Aug 12 12:51:34 1994 +0200
@@ -1,7 +1,7 @@
(*  Title: 	ZF/indrule.ML
ID:         \$Id\$
Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1993  University of Cambridge
+    Copyright   1994  University of Cambridge

Induction rule module -- for Inductive/Coinductive Definitions

@@ -15,19 +15,25 @@
end;

-functor Indrule_Fun (structure Ind: INDUCTIVE and
-		     Pr: PR and Intr_elim: INTR_ELIM) : INDRULE  =
+functor Indrule_Fun
+    (structure Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end
+     and Pr: PR and Intr_elim: INTR_ELIM) : INDRULE  =
struct
-open Logic Ind Intr_elim;
+open Logic Ind_Syntax Inductive Intr_elim;
+
+val sign = sign_of thy;

-val dummy = writeln "Proving the induction rules...";
+val (Const(_,recT),rec_params) = strip_comb (hd rec_tms);
+
+val big_rec_name = space_implode "_" rec_names;
+val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
+
+val _ = writeln "  Proving the induction rules...";

(*** Prove the main induction rule ***)

val pred_name = "P";		(*name for predicate variables*)

-val prove = prove_term (sign_of Intr_elim.thy);
-
val big_rec_def::part_rec_defs = Intr_elim.defs;

(*Used to make induction rules;
@@ -63,7 +69,7 @@
val ind_prems = map (induct_prem (map (rpair pred) rec_tms)) intr_tms;

val quant_induct =
-    prove part_rec_defs
+    prove_term sign part_rec_defs
(list_implies (ind_prems, mk_tprop (mk_all_imp(big_rec_tm,pred))),
fn prems =>
[rtac (impI RS allI) 1,
@@ -112,7 +118,7 @@
and mutual_induct_concl = mk_tprop(fold_bal (app conj) qconcls);

val lemma = (*makes the link between the two induction rules*)
-    prove part_rec_defs
+    prove_term sign part_rec_defs
(mk_implies (induct_concl,mutual_induct_concl),
fn prems =>
[cut_facts_tac prems 1,
@@ -139,7 +145,7 @@
i  THEN mutual_ind_tac prems (i-1);

val mutual_induct_fsplit =
-    prove []
+    prove_term sign []
(list_implies (map (induct_prem (rec_tms~~preds)) intr_tms,
mutual_induct_concl),
fn prems =>```