src/ZF/indrule.ML

--- a/src/ZF/indrule.ML	Wed May 08 17:54:07 1996 +0200
+++ b/src/ZF/indrule.ML	Wed May 08 17:57:05 1996 +0200
@@ -17,7 +17,7 @@
 
 functor Indrule_Fun
     (structure Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end
-     and Pr: PR and Su : SU and 
+     and Pr: PR and CP: CARTPROD and Su : SU and 
      Intr_elim: sig include INTR_ELIM INTR_ELIM_AUX end) : INDRULE  =
 let
 
@@ -90,15 +90,11 @@
 
 (*Make distinct predicates for each inductive set*)
 
-(*Sigmas and Cartesian products may nest ONLY to the right!*)
-fun mk_pred_typ (t $ A $ Abs(_,_,B)) = 
-        if t = Pr.sigma  then  Ind_Syntax.iT --> mk_pred_typ B
-                         else  Ind_Syntax.iT --> Ind_Syntax.oT
-  | mk_pred_typ _           =  Ind_Syntax.iT --> Ind_Syntax.oT
-
-(*For testing whether the inductive set is a relation*)
-fun is_sigma (t$_$_) = (t = Pr.sigma)
-  | is_sigma _       =  false;
+(*The components of the element type, several if it is a product*)
+val elem_type = CP.pseudo_type Inductive.dom_sum;
+val elem_factors = CP.factors elem_type;
+val elem_frees = mk_frees "za" elem_factors;
+val elem_tuple = CP.mk_tuple Pr.pair elem_type elem_frees;
 
 (*Given a recursive set and its domain, return the "fsplit" predicate
   and a conclusion for the simultaneous induction rule.
@@ -107,17 +103,16 @@
   mutual recursion to invariably be a disjoint sum.*)
 fun mk_predpair rec_tm = 
   let val rec_name = (#1 o dest_Const o head_of) rec_tm
-      val T = mk_pred_typ Inductive.dom_sum
-      val pfree = Free(pred_name ^ "_" ^ rec_name, T)
-      val frees = mk_frees "za" (binder_types T)
+      val pfree = Free(pred_name ^ "_" ^ rec_name,
+		       elem_factors ---> Ind_Syntax.oT)
       val qconcl = 
-        foldr Ind_Syntax.mk_all (frees, 
-                        Ind_Syntax.imp $ 
-                          (Ind_Syntax.mem_const $ foldr1 (app Pr.pair) frees $
-                           rec_tm)
-                          $ (list_comb (pfree,frees)))
-  in  (Ind_Syntax.ap_split Pr.fsplit_const pfree (binder_types T), 
-      qconcl)  
+        foldr Ind_Syntax.mk_all 
+	  (elem_frees, 
+	   Ind_Syntax.imp $ 
+	   (Ind_Syntax.mem_const $ elem_tuple $ rec_tm)
+	         $ (list_comb (pfree, elem_frees)))
+  in  (CP.ap_split elem_type Ind_Syntax.oT pfree, 
+       qconcl)  
   end;
 
 val (preds,qconcls) = split_list (map mk_predpair Inductive.rec_tms);
@@ -129,21 +124,26 @@
 
 (*To instantiate the main induction rule*)
 val induct_concl = 
- Ind_Syntax.mk_tprop(Ind_Syntax.mk_all_imp(big_rec_tm,
-             Abs("z", Ind_Syntax.iT, 
-                 fold_bal (app Ind_Syntax.conj) 
-                 (map mk_rec_imp (Inductive.rec_tms~~preds)))))
+    Ind_Syntax.mk_tprop
+      (Ind_Syntax.mk_all_imp
+       (big_rec_tm,
+	Abs("z", Ind_Syntax.iT, 
+	    fold_bal (app Ind_Syntax.conj) 
+	    (map mk_rec_imp (Inductive.rec_tms~~preds)))))
 and mutual_induct_concl =
  Ind_Syntax.mk_tprop(fold_bal (app Ind_Syntax.conj) qconcls);
 
+val lemma_tac = FIRST' [eresolve_tac [asm_rl, conjE, PartE, mp],
+			resolve_tac [allI, impI, conjI, Part_eqI],
+			dresolve_tac [spec, mp, Pr.fsplitD]];
+
 val lemma = (*makes the link between the two induction rules*)
     prove_goalw_cterm part_rec_defs 
           (cterm_of sign (Logic.mk_implies (induct_concl,mutual_induct_concl)))
           (fn prems =>
            [cut_facts_tac prems 1, 
-            REPEAT (eresolve_tac [asm_rl, conjE, PartE, mp] 1
-             ORELSE resolve_tac [allI, impI, conjI, Part_eqI] 1
-             ORELSE dresolve_tac [spec, mp, Pr.fsplitD] 1)]);
+            REPEAT (rewrite_goals_tac [Pr.split_eq] THEN
+		    lemma_tac 1)]);
 
 (*Mutual induction follows by freeness of Inl/Inr.*)
 
@@ -197,25 +197,34 @@
            [rtac (quant_induct RS lemma) 1,
             mutual_ind_tac (rev prems) (length prems)]);
 
-(*Attempts to remove all occurrences of fsplit*)
-val fsplit_tac =
-    REPEAT (SOMEGOAL (FIRST' [rtac Pr.fsplitI, 
-                              dtac Pr.fsplitD,
-                              etac Pr.fsplitE,  (*apparently never used!*)
-                              bound_hyp_subst_tac]))
-    THEN prune_params_tac
+
+
+(** Uncurrying the predicate in the ordinary induction rule **)
+
+(*instantiate the variable to a tuple, if it is non-trivial, in order to
+  allow the predicate to be "opened up".
+  The name "x.1" comes from the "RS spec" !*)
+val inst = 
+    case elem_frees of [_] => I
+       | _ => instantiate ([], [(cterm_of sign (Var(("x",1), Ind_Syntax.iT)), 
+				 cterm_of sign elem_tuple)]);
+
+(*strip quantifier and the implication*)
+val induct0 = inst (quant_induct RS spec RSN (2,rev_mp));
+
 
 in
   struct
   (*strip quantifier*)
-  val induct = standard (quant_induct RS spec RSN (2,rev_mp));
+  val induct = standard 
+                  (CP.split_rule_var
+		    (Var((pred_name,2), elem_type --> Ind_Syntax.oT),
+		     induct0));
 
-  (*Just "True" unless significantly different from induct, with mutual
-    recursion or because it involves tuples.  This saves storage.*)
+  (*Just "True" unless there's true mutual recursion.  This saves storage.*)
   val mutual_induct = 
-      if length Intr_elim.rec_names > 1 orelse
-         is_sigma Inductive.dom_sum 
-      then rule_by_tactic fsplit_tac mutual_induct_fsplit
+      if length Intr_elim.rec_names > 1 
+      then CP.remove_split mutual_induct_fsplit
       else TrueI;
   end
 end;