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.
--- 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;