# HG changeset patch
# User paulson
# Date 820148380 -3600
# Node ID 7b61bcfeaa950ece5ce81b2b3521ad275e06be31
# Parent  ccb3c5ff6707e20bfb7da8af12c5bcf09a46a77e
Removed unfold:thm from signature INTR_ELIM and from the
functor result.  It is never used outside, is easily recovered using
bnd_mono and def_lfp_Tarski, and takes up considerable store.

diff -r ccb3c5ff6707 -r 7b61bcfeaa95 src/HOL/intr_elim.ML
--- a/src/HOL/intr_elim.ML	Thu Dec 28 11:59:15 1995 +0100
+++ b/src/HOL/intr_elim.ML	Thu Dec 28 11:59:40 1995 +0100
@@ -13,8 +13,8 @@
   val con_defs   : thm list		(*definitions of the constructors*)
   end;
 
-(*internal items*)
-signature INDUCTIVE_I =
+
+signature INDUCTIVE_I =	(** Terms read from the theory section **)
   sig
   val rec_tms    : term list		(*the recursive sets*)
   val intr_tms   : term list		(*terms for the introduction rules*)
@@ -25,51 +25,54 @@
   val thy        : theory               (*copy of input theory*)
   val defs	 : thm list		(*definitions made in thy*)
   val mono	 : thm			(*monotonicity for the lfp definition*)
-  val unfold     : thm			(*fixed-point equation*)
   val intrs      : thm list		(*introduction rules*)
   val elim       : thm			(*case analysis theorem*)
+  val mk_cases   : thm list -> string -> thm	(*generates case theorems*)
+  end;
+
+signature INTR_ELIM_AUX =	(** Used to make induction rules **)
+  sig
   val raw_induct : thm			(*raw induction rule from Fp.induct*)
-  val mk_cases : thm list -> string -> thm	(*generates case theorems*)
   val rec_names  : string list		(*names of recursive sets*)
   end;
 
 (*prove intr/elim rules for a fixedpoint definition*)
 functor Intr_elim_Fun
     (structure Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end  
-     and Fp: FP) : INTR_ELIM =
-struct
-open Logic Inductive Ind_Syntax;
-
-val rec_names = map (#1 o dest_Const o head_of) rec_tms;
+     and Fp: FP) 
+    : sig include INTR_ELIM INTR_ELIM_AUX end =
+let
+val rec_names = map (#1 o dest_Const o head_of) Inductive.rec_tms;
 val big_rec_name = space_implode "_" rec_names;
 
-val _ = deny (big_rec_name  mem  map ! (stamps_of_thy thy))
+val _ = deny (big_rec_name  mem  map ! (stamps_of_thy Inductive.thy))
              ("Definition " ^ big_rec_name ^ 
 	      " would clash with the theory of the same name!");
 
 (*fetch fp definitions from the theory*)
 val big_rec_def::part_rec_defs = 
-  map (get_def thy)
+  map (get_def Inductive.thy)
       (case rec_names of [_] => rec_names | _ => big_rec_name::rec_names);
 
 
-val sign = sign_of thy;
+val sign = sign_of Inductive.thy;
 
 (********)
 val _ = writeln "  Proving monotonicity...";
 
 val Const("==",_) $ _ $ (Const(_,fpT) $ fp_abs) =
-    big_rec_def |> rep_thm |> #prop |> unvarify;
+    big_rec_def |> rep_thm |> #prop |> Logic.unvarify;
 
 (*For the type of the argument of mono*)
 val [monoT] = binder_types fpT;
 
 val mono = 
     prove_goalw_cterm [] 
-      (cterm_of sign (mk_Trueprop (Const("mono", monoT-->boolT) $ fp_abs)))
+      (cterm_of sign (Ind_Syntax.mk_Trueprop 
+		      (Const("mono", monoT --> Ind_Syntax.boolT) $ fp_abs)))
       (fn _ =>
        [rtac monoI 1,
-	REPEAT (ares_tac (basic_monos @ monos) 1)]);
+	REPEAT (ares_tac (basic_monos @ Inductive.monos) 1)]);
 
 val unfold = standard (mono RS (big_rec_def RS Fp.Tarski));
 
@@ -87,7 +90,7 @@
      backtracking may occur if the premises have extra variables!*)
    DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 1 ORELSE assume_tac 1),
    (*Now solve the equations like Inl 0 = Inl ?b2*)
-   rewrite_goals_tac con_defs,
+   rewrite_goals_tac Inductive.con_defs,
    REPEAT (rtac refl 1)];
 
 
@@ -98,25 +101,19 @@
     in  accesses_bal(f, g, asm_rl)  end;
 
 val intrs = map (uncurry (prove_goalw_cterm part_rec_defs))
-            (map (cterm_of sign) intr_tms ~~ 
-	     map intro_tacsf (mk_disj_rls(length intr_tms)));
+            (map (cterm_of sign) Inductive.intr_tms ~~ 
+	     map intro_tacsf (mk_disj_rls(length Inductive.intr_tms)));
 
 (********)
 val _ = writeln "  Proving the elimination rule...";
 
-(*Includes rules for Suc and Pair since they are common constructions*)
-val elim_rls = [asm_rl, FalseE, Suc_neq_Zero, Zero_neq_Suc,
-		make_elim Suc_inject, 
-		refl_thin, conjE, exE, disjE];
-
 (*Breaks down logical connectives in the monotonic function*)
 val basic_elim_tac =
-    REPEAT (SOMEGOAL (eresolve_tac (elim_rls@sumprod_free_SEs)
+    REPEAT (SOMEGOAL (eresolve_tac (Ind_Syntax.elim_rls @ 
+				    Ind_Syntax.sumprod_free_SEs)
 	      ORELSE' bound_hyp_subst_tac))
     THEN prune_params_tac;
 
-val elim = rule_by_tactic basic_elim_tac (unfold RS equals_CollectD);
-
 (*Applies freeness of the given constructors, which *must* be unfolded by
   the given defs.  Cannot simply use the local con_defs because con_defs=[] 
   for inference systems.
@@ -124,7 +121,8 @@
     rewrite_goals_tac defs THEN basic_elim_tac THEN fold_tac defs;
  *)
 fun con_elim_tac simps =
-  let val elim_tac = REPEAT o (eresolve_tac (elim_rls@sumprod_free_SEs))
+  let val elim_tac = REPEAT o (eresolve_tac (Ind_Syntax.elim_rls @ 
+					     Ind_Syntax.sumprod_free_SEs))
   in ALLGOALS(EVERY'[elim_tac,
                      asm_full_simp_tac (simpset_of "Nat" addsimps simps),
                      elim_tac,
@@ -133,13 +131,23 @@
   end;
 
 
-(*String s should have the form t:Si where Si is an inductive set*)
-fun mk_cases defs s = 
-    rule_by_tactic (con_elim_tac defs)
-      (assume_read thy s  RS  elim);
+in
+  struct
+  val thy   = Inductive.thy
+  and defs  = big_rec_def :: part_rec_defs
+  and mono  = mono
+  and intrs = intrs;
 
-val defs = big_rec_def::part_rec_defs;
+  val elim = rule_by_tactic basic_elim_tac 
+                  (unfold RS Ind_Syntax.equals_CollectD);
 
-val raw_induct = standard ([big_rec_def, mono] MRS Fp.induct);
+  (*String s should have the form t:Si where Si is an inductive set*)
+  fun mk_cases defs s = 
+      rule_by_tactic (con_elim_tac defs)
+	(assume_read Inductive.thy s  RS  elim);
+
+  val raw_induct = standard ([big_rec_def, mono] MRS Fp.induct)
+  and rec_names = rec_names
+  end
 end;