Removed unfold:thm from signature INTR_ELIM and from the
authorpaulson
Thu Dec 28 11:59:40 1995 +0100 (1995-12-28)
changeset 14257b61bcfeaa95
parent 1424 ccb3c5ff6707
child 1426 c60e9e1a1a23
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.
src/HOL/intr_elim.ML
     1.1 --- a/src/HOL/intr_elim.ML	Thu Dec 28 11:59:15 1995 +0100
     1.2 +++ b/src/HOL/intr_elim.ML	Thu Dec 28 11:59:40 1995 +0100
     1.3 @@ -13,8 +13,8 @@
     1.4    val con_defs   : thm list		(*definitions of the constructors*)
     1.5    end;
     1.6  
     1.7 -(*internal items*)
     1.8 -signature INDUCTIVE_I =
     1.9 +
    1.10 +signature INDUCTIVE_I =	(** Terms read from the theory section **)
    1.11    sig
    1.12    val rec_tms    : term list		(*the recursive sets*)
    1.13    val intr_tms   : term list		(*terms for the introduction rules*)
    1.14 @@ -25,51 +25,54 @@
    1.15    val thy        : theory               (*copy of input theory*)
    1.16    val defs	 : thm list		(*definitions made in thy*)
    1.17    val mono	 : thm			(*monotonicity for the lfp definition*)
    1.18 -  val unfold     : thm			(*fixed-point equation*)
    1.19    val intrs      : thm list		(*introduction rules*)
    1.20    val elim       : thm			(*case analysis theorem*)
    1.21 +  val mk_cases   : thm list -> string -> thm	(*generates case theorems*)
    1.22 +  end;
    1.23 +
    1.24 +signature INTR_ELIM_AUX =	(** Used to make induction rules **)
    1.25 +  sig
    1.26    val raw_induct : thm			(*raw induction rule from Fp.induct*)
    1.27 -  val mk_cases : thm list -> string -> thm	(*generates case theorems*)
    1.28    val rec_names  : string list		(*names of recursive sets*)
    1.29    end;
    1.30  
    1.31  (*prove intr/elim rules for a fixedpoint definition*)
    1.32  functor Intr_elim_Fun
    1.33      (structure Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end  
    1.34 -     and Fp: FP) : INTR_ELIM =
    1.35 -struct
    1.36 -open Logic Inductive Ind_Syntax;
    1.37 -
    1.38 -val rec_names = map (#1 o dest_Const o head_of) rec_tms;
    1.39 +     and Fp: FP) 
    1.40 +    : sig include INTR_ELIM INTR_ELIM_AUX end =
    1.41 +let
    1.42 +val rec_names = map (#1 o dest_Const o head_of) Inductive.rec_tms;
    1.43  val big_rec_name = space_implode "_" rec_names;
    1.44  
    1.45 -val _ = deny (big_rec_name  mem  map ! (stamps_of_thy thy))
    1.46 +val _ = deny (big_rec_name  mem  map ! (stamps_of_thy Inductive.thy))
    1.47               ("Definition " ^ big_rec_name ^ 
    1.48  	      " would clash with the theory of the same name!");
    1.49  
    1.50  (*fetch fp definitions from the theory*)
    1.51  val big_rec_def::part_rec_defs = 
    1.52 -  map (get_def thy)
    1.53 +  map (get_def Inductive.thy)
    1.54        (case rec_names of [_] => rec_names | _ => big_rec_name::rec_names);
    1.55  
    1.56  
    1.57 -val sign = sign_of thy;
    1.58 +val sign = sign_of Inductive.thy;
    1.59  
    1.60  (********)
    1.61  val _ = writeln "  Proving monotonicity...";
    1.62  
    1.63  val Const("==",_) $ _ $ (Const(_,fpT) $ fp_abs) =
    1.64 -    big_rec_def |> rep_thm |> #prop |> unvarify;
    1.65 +    big_rec_def |> rep_thm |> #prop |> Logic.unvarify;
    1.66  
    1.67  (*For the type of the argument of mono*)
    1.68  val [monoT] = binder_types fpT;
    1.69  
    1.70  val mono = 
    1.71      prove_goalw_cterm [] 
    1.72 -      (cterm_of sign (mk_Trueprop (Const("mono", monoT-->boolT) $ fp_abs)))
    1.73 +      (cterm_of sign (Ind_Syntax.mk_Trueprop 
    1.74 +		      (Const("mono", monoT --> Ind_Syntax.boolT) $ fp_abs)))
    1.75        (fn _ =>
    1.76         [rtac monoI 1,
    1.77 -	REPEAT (ares_tac (basic_monos @ monos) 1)]);
    1.78 +	REPEAT (ares_tac (basic_monos @ Inductive.monos) 1)]);
    1.79  
    1.80  val unfold = standard (mono RS (big_rec_def RS Fp.Tarski));
    1.81  
    1.82 @@ -87,7 +90,7 @@
    1.83       backtracking may occur if the premises have extra variables!*)
    1.84     DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 1 ORELSE assume_tac 1),
    1.85     (*Now solve the equations like Inl 0 = Inl ?b2*)
    1.86 -   rewrite_goals_tac con_defs,
    1.87 +   rewrite_goals_tac Inductive.con_defs,
    1.88     REPEAT (rtac refl 1)];
    1.89  
    1.90  
    1.91 @@ -98,25 +101,19 @@
    1.92      in  accesses_bal(f, g, asm_rl)  end;
    1.93  
    1.94  val intrs = map (uncurry (prove_goalw_cterm part_rec_defs))
    1.95 -            (map (cterm_of sign) intr_tms ~~ 
    1.96 -	     map intro_tacsf (mk_disj_rls(length intr_tms)));
    1.97 +            (map (cterm_of sign) Inductive.intr_tms ~~ 
    1.98 +	     map intro_tacsf (mk_disj_rls(length Inductive.intr_tms)));
    1.99  
   1.100  (********)
   1.101  val _ = writeln "  Proving the elimination rule...";
   1.102  
   1.103 -(*Includes rules for Suc and Pair since they are common constructions*)
   1.104 -val elim_rls = [asm_rl, FalseE, Suc_neq_Zero, Zero_neq_Suc,
   1.105 -		make_elim Suc_inject, 
   1.106 -		refl_thin, conjE, exE, disjE];
   1.107 -
   1.108  (*Breaks down logical connectives in the monotonic function*)
   1.109  val basic_elim_tac =
   1.110 -    REPEAT (SOMEGOAL (eresolve_tac (elim_rls@sumprod_free_SEs)
   1.111 +    REPEAT (SOMEGOAL (eresolve_tac (Ind_Syntax.elim_rls @ 
   1.112 +				    Ind_Syntax.sumprod_free_SEs)
   1.113  	      ORELSE' bound_hyp_subst_tac))
   1.114      THEN prune_params_tac;
   1.115  
   1.116 -val elim = rule_by_tactic basic_elim_tac (unfold RS equals_CollectD);
   1.117 -
   1.118  (*Applies freeness of the given constructors, which *must* be unfolded by
   1.119    the given defs.  Cannot simply use the local con_defs because con_defs=[] 
   1.120    for inference systems.
   1.121 @@ -124,7 +121,8 @@
   1.122      rewrite_goals_tac defs THEN basic_elim_tac THEN fold_tac defs;
   1.123   *)
   1.124  fun con_elim_tac simps =
   1.125 -  let val elim_tac = REPEAT o (eresolve_tac (elim_rls@sumprod_free_SEs))
   1.126 +  let val elim_tac = REPEAT o (eresolve_tac (Ind_Syntax.elim_rls @ 
   1.127 +					     Ind_Syntax.sumprod_free_SEs))
   1.128    in ALLGOALS(EVERY'[elim_tac,
   1.129                       asm_full_simp_tac (simpset_of "Nat" addsimps simps),
   1.130                       elim_tac,
   1.131 @@ -133,13 +131,23 @@
   1.132    end;
   1.133  
   1.134  
   1.135 -(*String s should have the form t:Si where Si is an inductive set*)
   1.136 -fun mk_cases defs s = 
   1.137 -    rule_by_tactic (con_elim_tac defs)
   1.138 -      (assume_read thy s  RS  elim);
   1.139 +in
   1.140 +  struct
   1.141 +  val thy   = Inductive.thy
   1.142 +  and defs  = big_rec_def :: part_rec_defs
   1.143 +  and mono  = mono
   1.144 +  and intrs = intrs;
   1.145  
   1.146 -val defs = big_rec_def::part_rec_defs;
   1.147 +  val elim = rule_by_tactic basic_elim_tac 
   1.148 +                  (unfold RS Ind_Syntax.equals_CollectD);
   1.149  
   1.150 -val raw_induct = standard ([big_rec_def, mono] MRS Fp.induct);
   1.151 +  (*String s should have the form t:Si where Si is an inductive set*)
   1.152 +  fun mk_cases defs s = 
   1.153 +      rule_by_tactic (con_elim_tac defs)
   1.154 +	(assume_read Inductive.thy s  RS  elim);
   1.155 +
   1.156 +  val raw_induct = standard ([big_rec_def, mono] MRS Fp.induct)
   1.157 +  and rec_names = rec_names
   1.158 +  end
   1.159  end;
   1.160