diff -r f04b33ce250f -r a4dc62a46ee4 intr_elim.ML
--- a/intr_elim.ML	Tue Oct 24 14:59:17 1995 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,141 +0,0 @@
-(*  Title: 	HOL/intr_elim.ML
-    ID:         $Id$
-    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1994  University of Cambridge
-
-Introduction/elimination rule module -- for Inductive/Coinductive Definitions
-*)
-
-signature INDUCTIVE_ARG =	(** Description of a (co)inductive def **)
-  sig
-  val thy        : theory               (*new theory with inductive defs*)
-  val monos      : thm list		(*monotonicity of each M operator*)
-  val con_defs   : thm list		(*definitions of the constructors*)
-  end;
-
-(*internal items*)
-signature INDUCTIVE_I =
-  sig
-  val rec_tms    : term list		(*the recursive sets*)
-  val intr_tms   : term list		(*terms for the introduction rules*)
-  end;
-
-signature INTR_ELIM =
-  sig
-  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 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;
-val big_rec_name = space_implode "_" rec_names;
-
-val _ = deny (big_rec_name  mem  map ! (stamps_of_thy 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)
-      (case rec_names of [_] => rec_names | _ => big_rec_name::rec_names);
-
-
-val sign = sign_of thy;
-
-(********)
-val _ = writeln "  Proving monotonicity...";
-
-val Const("==",_) $ _ $ (Const(_,fpT) $ fp_abs) =
-    big_rec_def |> rep_thm |> #prop |> 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)))
-      (fn _ =>
-       [rtac monoI 1,
-	REPEAT (ares_tac (basic_monos @ monos) 1)]);
-
-val unfold = standard (mono RS (big_rec_def RS Fp.Tarski));
-
-(********)
-val _ = writeln "  Proving the introduction rules...";
-
-fun intro_tacsf disjIn prems = 
-  [(*insert prems and underlying sets*)
-   cut_facts_tac prems 1,
-   rtac (unfold RS ssubst) 1,
-   REPEAT (resolve_tac [Part_eqI,CollectI] 1),
-   (*Now 1-2 subgoals: the disjunction, perhaps equality.*)
-   rtac disjIn 1,
-   (*Not ares_tac, since refl must be tried before any equality assumptions;
-     backtracking may occur if the premises have extra variables!*)
-   DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 1 ORELSE assume_tac 1)];
-
-(*combines disjI1 and disjI2 to access the corresponding nested disjunct...*)
-val mk_disj_rls = 
-    let fun f rl = rl RS disjI1
-	and g rl = rl RS disjI2
-    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)));
-
-(********)
-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)
-	      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.
-fun con_elim_tac defs =
-    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))
-  in ALLGOALS(EVERY'[elim_tac,
-                     asm_full_simp_tac (nat_ss addsimps simps),
-                     elim_tac,
-                     REPEAT o bound_hyp_subst_tac])
-     THEN prune_params_tac
-  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);
-
-val defs = big_rec_def::part_rec_defs;
-
-val raw_induct = standard ([big_rec_def, mono] MRS Fp.induct);
-end;
-