src/HOL/indrule.ML
 changeset 1728 01beef6262aa parent 1653 1a2ffa2fbf7d child 1746 f0c6aabc6c02
```--- a/src/HOL/indrule.ML	Tue May 07 18:14:39 1996 +0200
+++ b/src/HOL/indrule.ML	Tue May 07 18:15:51 1996 +0200
@@ -99,23 +99,26 @@
(*** Prove the simultaneous induction rule ***)

(*Make distinct predicates for each inductive set.
-  Splits cartesian products in elem_type, IF nested to the right! *)
+  Splits cartesian products in elem_type, however nested*)
+
+(*The components of the element type, several if it is a product*)
+val elem_factors = Ind_Syntax.factors elem_type;
+val elem_frees = mk_frees "za" elem_factors;
+val elem_tuple = Ind_Syntax.mk_tuple elem_type elem_frees;

(*Given a recursive set, return the "split" predicate
and a conclusion for the simultaneous induction rule*)
fun mk_predpair rec_tm =
let val rec_name = (#1 o dest_Const o head_of) rec_tm
-      val T = Ind_Syntax.factors elem_type ---> Ind_Syntax.boolT
-      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.boolT)
val qconcl =
foldr Ind_Syntax.mk_all
-          (frees,
-           Ind_Syntax.imp \$ (Ind_Syntax.mk_mem
-                             (foldr1 Ind_Syntax.mk_Pair frees, rec_tm))
-                \$ (list_comb (pfree,frees)))
-  in  (Ind_Syntax.ap_split Ind_Syntax.boolT pfree (binder_types T),
-      qconcl)
+          (elem_frees,
+           Ind_Syntax.imp \$ (Ind_Syntax.mk_mem (elem_tuple, rec_tm))
+                \$ (list_comb (pfree, elem_frees)))
+  in  (Ind_Syntax.ap_split elem_type Ind_Syntax.boolT pfree,
+       qconcl)
end;

val (preds,qconcls) = split_list (map mk_predpair Inductive.rec_tms);
@@ -135,15 +138,18 @@
and mutual_induct_concl =
Ind_Syntax.mk_Trueprop (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, refl],
+			dresolve_tac [spec, mp, splitD]];
+
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, refl] 1
-             ORELSE dresolve_tac [spec, mp, splitD] 1)])
+            REPEAT (rewrite_goals_tac [split RS eq_reflection] THEN
+		    lemma_tac 1)])
handle e => print_sign_exn sign e;

(*Mutual induction follows by freeness of Inl/Inr.*)
@@ -151,9 +157,9 @@
(*Simplification largely reduces the mutual induction rule to the
standard rule*)
val mut_ss = simpset_of "Fun"
-             addsimps [Inl_Inr_eq, Inr_Inl_eq, Inl_eq, Inr_eq];
+             addsimps [Inl_Inr_eq, Inr_Inl_eq, Inl_eq, Inr_eq, split];

-val all_defs = Inductive.con_defs @ part_rec_defs;
+val all_defs = [split RS eq_reflection] @ Inductive.con_defs @ part_rec_defs;

(*Removes Collects caused by M-operators in the intro rules*)
val cmonos = [subset_refl RS Int_Collect_mono] RL Inductive.monos RLN
@@ -172,7 +178,7 @@
simp_tac (mut_ss addsimps [Part_def]) 1  THEN
IF_UNSOLVED (*simp_tac may have finished it off!*)
((*simplify assumptions, but don't accept new rewrite rules!*)
-              asm_full_simp_tac (mut_ss setmksimps K[]) 1  THEN
+              full_simp_tac mut_ss 1  THEN
(*unpackage and use "prem" in the corresponding place*)
REPEAT (rtac impI 1)  THEN
rtac (rewrite_rule all_defs prem) 1  THEN
@@ -195,23 +201,27 @@
mutual_ind_tac (rev prems) (length prems)])
handle e => print_sign_exn sign e;

-(*Attempts to remove all occurrences of split*)
-val split_tac =
-    REPEAT (SOMEGOAL (FIRST' [rtac splitI,
-                              dtac splitD,
-                              etac splitE,
-                              bound_hyp_subst_tac]))
-    THEN prune_params_tac;
+(** Uncurrying the predicate in the ordinary induction rule **)
+
+(*The name "x.1" comes from the "RS spec" !*)
+val xvar = cterm_of sign (Var(("x",1), elem_type));
+
+(*strip quantifier and instantiate the variable to a tuple*)
+val induct0 = quant_induct RS spec RSN (2,rev_mp) |>
+              freezeT |>     (*Because elem_type contains TFrees not TVars*)
+              instantiate ([], [(xvar, cterm_of sign elem_tuple)]);

in
struct
-  (*strip quantifier*)
-  val induct = standard (quant_induct RS spec RSN (2,rev_mp));
+  val induct = standard
+                  (Ind_Syntax.split_rule_var
+		    (Var((pred_name,2), elem_type --> Ind_Syntax.boolT),
+		     induct0));

+  (*Just "True" unless there's true mutual recursion.  This saves storage.*)
val mutual_induct =
-      if length Intr_elim.rec_names > 1 orelse
-         length (Ind_Syntax.factors elem_type) > 1
-      then rule_by_tactic split_tac mutual_induct_split
+      if length Intr_elim.rec_names > 1
+      then Ind_Syntax.remove_split mutual_induct_split
else TrueI;
end
end;```