src/Pure/drule.ML
changeset 21600 222810ce6b05
parent 21596 486cae91868f
child 21603 0fa36ea9aaf5
     1.1 --- a/src/Pure/drule.ML	Wed Nov 29 23:28:13 2006 +0100
     1.2 +++ b/src/Pure/drule.ML	Wed Nov 29 23:33:09 2006 +0100
     1.3 @@ -38,7 +38,6 @@
     1.4    val implies_elim_list: thm -> thm list -> thm
     1.5    val implies_intr_list: cterm list -> thm -> thm
     1.6    val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
     1.7 -  val zero_var_indexes_list: thm list -> thm list
     1.8    val zero_var_indexes: thm -> thm
     1.9    val implies_intr_hyps: thm -> thm
    1.10    val standard: thm -> thm
    1.11 @@ -100,7 +99,6 @@
    1.12    val add_used: thm -> string list -> string list
    1.13    val flexflex_unique: thm -> thm
    1.14    val close_derivation: thm -> thm
    1.15 -  val local_standard': thm -> thm
    1.16    val local_standard: thm -> thm
    1.17    val store_thm: bstring -> thm -> thm
    1.18    val store_standard_thm: bstring -> thm -> thm
    1.19 @@ -399,17 +397,14 @@
    1.20  fun implies_elim_list impth ths = Library.foldl (uncurry implies_elim) (impth,ths);
    1.21  
    1.22  (*Reset Var indexes to zero, renaming to preserve distinctness*)
    1.23 -fun zero_var_indexes_list [] = []
    1.24 -  | zero_var_indexes_list ths =
    1.25 -      let
    1.26 -        val thy = Theory.merge_list (map Thm.theory_of_thm ths);
    1.27 -        val certT = Thm.ctyp_of thy and cert = Thm.cterm_of thy;
    1.28 -        val (instT, inst) = TermSubst.zero_var_indexes_inst (map Thm.full_prop_of ths);
    1.29 -        val cinstT = map (fn (v, T) => (certT (TVar v), certT T)) instT;
    1.30 -        val cinst = map (fn (v, t) => (cert (Var v), cert t)) inst;
    1.31 -      in map (Thm.adjust_maxidx_thm ~1 o Thm.instantiate (cinstT, cinst)) ths end;
    1.32 -
    1.33 -val zero_var_indexes = singleton zero_var_indexes_list;
    1.34 +fun zero_var_indexes th =
    1.35 +  let
    1.36 +    val thy = Thm.theory_of_thm th;
    1.37 +    val certT = Thm.ctyp_of thy and cert = Thm.cterm_of thy;
    1.38 +    val (instT, inst) = TermSubst.zero_var_indexes_inst (Thm.full_prop_of th);
    1.39 +    val cinstT = map (fn (v, T) => (certT (TVar v), certT T)) instT;
    1.40 +    val cinst = map (fn (v, t) => (cert (Var v), cert t)) inst;
    1.41 +  in Thm.adjust_maxidx_thm ~1 (Thm.instantiate (cinstT, cinst) th) end;
    1.42  
    1.43  
    1.44  (** Standard form of object-rule: no hypotheses, flexflex constraints,
    1.45 @@ -441,20 +436,17 @@
    1.46      #> Thm.strip_shyps
    1.47      #> zero_var_indexes
    1.48      #> Thm.varifyT
    1.49 -    #> Thm.compress);   (* FIXME !? *)
    1.50 +    #> Thm.compress);
    1.51  
    1.52  val standard =
    1.53 -  flexflex_unique       (* FIXME !? *)
    1.54 +  flexflex_unique
    1.55    #> standard'
    1.56    #> close_derivation;
    1.57  
    1.58 -val local_standard' =
    1.59 +val local_standard =
    1.60    flexflex_unique
    1.61    #> Thm.strip_shyps
    1.62 -  #> zero_var_indexes;
    1.63 -
    1.64 -val local_standard =
    1.65 -  local_standard'
    1.66 +  #> zero_var_indexes
    1.67    #> Thm.compress
    1.68    #> close_derivation;
    1.69  
    1.70 @@ -870,21 +862,11 @@
    1.71    else cterm_fun (Pattern.rewrite_term (Thm.theory_of_cterm ct) [norm_hhf_prop] []) ct;
    1.72  
    1.73  
    1.74 -(* var indexes *)
    1.75 -
    1.76 -fun incr_indexes th = Thm.incr_indexes (Thm.maxidx_of th + 1);
    1.77 -
    1.78 -fun incr_indexes2 th1 th2 =
    1.79 -  Thm.incr_indexes (Int.max (Thm.maxidx_of th1, Thm.maxidx_of th2) + 1);
    1.80 -
    1.81 -fun th1 INCR_COMP th2 = incr_indexes th2 th1 COMP th2;
    1.82 -fun th1 COMP_INCR th2 = th1 COMP incr_indexes th1 th2;
    1.83 -
    1.84  
    1.85  (*** Instantiate theorem th, reading instantiations in theory thy ****)
    1.86  
    1.87  (*Version that normalizes the result: Thm.instantiate no longer does that*)
    1.88 -fun instantiate instpair th = Thm.instantiate instpair th COMP_INCR asm_rl;
    1.89 +fun instantiate instpair th = Thm.instantiate instpair th  COMP   asm_rl;
    1.90  
    1.91  fun read_instantiate_sg' thy sinsts th =
    1.92      let val ts = types_sorts th;
    1.93 @@ -1070,6 +1052,17 @@
    1.94    end;
    1.95  
    1.96  
    1.97 +(* var indexes *)
    1.98 +
    1.99 +fun incr_indexes th = Thm.incr_indexes (Thm.maxidx_of th + 1);
   1.100 +
   1.101 +fun incr_indexes2 th1 th2 =
   1.102 +  Thm.incr_indexes (Int.max (Thm.maxidx_of th1, Thm.maxidx_of th2) + 1);
   1.103 +
   1.104 +fun th1 INCR_COMP th2 = incr_indexes th2 th1 COMP th2;
   1.105 +fun th1 COMP_INCR th2 = th1 COMP incr_indexes th1 th2;
   1.106 +
   1.107 +
   1.108  
   1.109  (** multi_resolve **)
   1.110