*** bad commit -- reverted to previous version ***
authorwenzelm
Wed Nov 29 23:33:09 2006 +0100 (2006-11-29)
changeset 21600222810ce6b05
parent 21599 f424d328090c
child 21601 6588b947d631
*** bad commit -- reverted to previous version ***
src/Pure/Isar/locale.ML
src/Pure/Isar/proof_context.ML
src/Pure/drule.ML
src/Pure/pure_thy.ML
     1.1 --- a/src/Pure/Isar/locale.ML	Wed Nov 29 23:28:13 2006 +0100
     1.2 +++ b/src/Pure/Isar/locale.ML	Wed Nov 29 23:33:09 2006 +0100
     1.3 @@ -1809,7 +1809,7 @@
     1.4      val (ctxt, (_, facts)) = activate_facts true (K I)
     1.5        (ProofContext.init pred_thy, axiomify predicate_axioms elemss');
     1.6      val view_ctxt = Assumption.add_view thy_ctxt predicate_statement ctxt;
     1.7 -    val export = Drule.local_standard o singleton (ProofContext.export view_ctxt thy_ctxt);
     1.8 +    val export = singleton (ProofContext.export_standard view_ctxt thy_ctxt);
     1.9      val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])]));
    1.10      val elems' = maps #2 (filter (equal "" o #1 o #1) elemss');
    1.11      val elems'' = map_filter (fn (Fixes _) => NONE | e => SOME e) elems';
     2.1 --- a/src/Pure/Isar/proof_context.ML	Wed Nov 29 23:28:13 2006 +0100
     2.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Nov 29 23:33:09 2006 +0100
     2.3 @@ -70,6 +70,8 @@
     2.4    val read_const: Proof.context -> string -> term
     2.5    val goal_export: Proof.context -> Proof.context -> thm list -> thm list
     2.6    val export: Proof.context -> Proof.context -> thm list -> thm list
     2.7 +  val export_standard: Proof.context -> Proof.context -> thm list -> thm list
     2.8 +  val standard: Proof.context -> thm list -> thm list
     2.9    val export_morphism: Proof.context -> Proof.context -> morphism
    2.10    val add_binds: (indexname * string option) list -> Proof.context -> Proof.context
    2.11    val add_binds_i: (indexname * term option) list -> Proof.context -> Proof.context
    2.12 @@ -570,7 +572,9 @@
    2.13  
    2.14  
    2.15  
    2.16 -(** export results **)
    2.17 +(** export theorems **)
    2.18 +
    2.19 +(* rules *)
    2.20  
    2.21  fun common_export is_goal inner outer =
    2.22    map (Assumption.export is_goal inner outer) #>
    2.23 @@ -579,6 +583,14 @@
    2.24  val goal_export = common_export true;
    2.25  val export = common_export false;
    2.26  
    2.27 +fun export_standard inner outer =
    2.28 +  export inner outer #> map Drule.local_standard;
    2.29 +
    2.30 +fun standard ctxt = export_standard ctxt ctxt;
    2.31 +
    2.32 +
    2.33 +(* morphisms *)
    2.34 +
    2.35  fun export_morphism inner outer =
    2.36    Assumption.export_morphism inner outer $>
    2.37    Variable.export_morphism inner outer;
     3.1 --- a/src/Pure/drule.ML	Wed Nov 29 23:28:13 2006 +0100
     3.2 +++ b/src/Pure/drule.ML	Wed Nov 29 23:33:09 2006 +0100
     3.3 @@ -38,7 +38,6 @@
     3.4    val implies_elim_list: thm -> thm list -> thm
     3.5    val implies_intr_list: cterm list -> thm -> thm
     3.6    val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
     3.7 -  val zero_var_indexes_list: thm list -> thm list
     3.8    val zero_var_indexes: thm -> thm
     3.9    val implies_intr_hyps: thm -> thm
    3.10    val standard: thm -> thm
    3.11 @@ -100,7 +99,6 @@
    3.12    val add_used: thm -> string list -> string list
    3.13    val flexflex_unique: thm -> thm
    3.14    val close_derivation: thm -> thm
    3.15 -  val local_standard': thm -> thm
    3.16    val local_standard: thm -> thm
    3.17    val store_thm: bstring -> thm -> thm
    3.18    val store_standard_thm: bstring -> thm -> thm
    3.19 @@ -399,17 +397,14 @@
    3.20  fun implies_elim_list impth ths = Library.foldl (uncurry implies_elim) (impth,ths);
    3.21  
    3.22  (*Reset Var indexes to zero, renaming to preserve distinctness*)
    3.23 -fun zero_var_indexes_list [] = []
    3.24 -  | zero_var_indexes_list ths =
    3.25 -      let
    3.26 -        val thy = Theory.merge_list (map Thm.theory_of_thm ths);
    3.27 -        val certT = Thm.ctyp_of thy and cert = Thm.cterm_of thy;
    3.28 -        val (instT, inst) = TermSubst.zero_var_indexes_inst (map Thm.full_prop_of ths);
    3.29 -        val cinstT = map (fn (v, T) => (certT (TVar v), certT T)) instT;
    3.30 -        val cinst = map (fn (v, t) => (cert (Var v), cert t)) inst;
    3.31 -      in map (Thm.adjust_maxidx_thm ~1 o Thm.instantiate (cinstT, cinst)) ths end;
    3.32 -
    3.33 -val zero_var_indexes = singleton zero_var_indexes_list;
    3.34 +fun zero_var_indexes th =
    3.35 +  let
    3.36 +    val thy = Thm.theory_of_thm th;
    3.37 +    val certT = Thm.ctyp_of thy and cert = Thm.cterm_of thy;
    3.38 +    val (instT, inst) = TermSubst.zero_var_indexes_inst (Thm.full_prop_of th);
    3.39 +    val cinstT = map (fn (v, T) => (certT (TVar v), certT T)) instT;
    3.40 +    val cinst = map (fn (v, t) => (cert (Var v), cert t)) inst;
    3.41 +  in Thm.adjust_maxidx_thm ~1 (Thm.instantiate (cinstT, cinst) th) end;
    3.42  
    3.43  
    3.44  (** Standard form of object-rule: no hypotheses, flexflex constraints,
    3.45 @@ -441,20 +436,17 @@
    3.46      #> Thm.strip_shyps
    3.47      #> zero_var_indexes
    3.48      #> Thm.varifyT
    3.49 -    #> Thm.compress);   (* FIXME !? *)
    3.50 +    #> Thm.compress);
    3.51  
    3.52  val standard =
    3.53 -  flexflex_unique       (* FIXME !? *)
    3.54 +  flexflex_unique
    3.55    #> standard'
    3.56    #> close_derivation;
    3.57  
    3.58 -val local_standard' =
    3.59 +val local_standard =
    3.60    flexflex_unique
    3.61    #> Thm.strip_shyps
    3.62 -  #> zero_var_indexes;
    3.63 -
    3.64 -val local_standard =
    3.65 -  local_standard'
    3.66 +  #> zero_var_indexes
    3.67    #> Thm.compress
    3.68    #> close_derivation;
    3.69  
    3.70 @@ -870,21 +862,11 @@
    3.71    else cterm_fun (Pattern.rewrite_term (Thm.theory_of_cterm ct) [norm_hhf_prop] []) ct;
    3.72  
    3.73  
    3.74 -(* var indexes *)
    3.75 -
    3.76 -fun incr_indexes th = Thm.incr_indexes (Thm.maxidx_of th + 1);
    3.77 -
    3.78 -fun incr_indexes2 th1 th2 =
    3.79 -  Thm.incr_indexes (Int.max (Thm.maxidx_of th1, Thm.maxidx_of th2) + 1);
    3.80 -
    3.81 -fun th1 INCR_COMP th2 = incr_indexes th2 th1 COMP th2;
    3.82 -fun th1 COMP_INCR th2 = th1 COMP incr_indexes th1 th2;
    3.83 -
    3.84  
    3.85  (*** Instantiate theorem th, reading instantiations in theory thy ****)
    3.86  
    3.87  (*Version that normalizes the result: Thm.instantiate no longer does that*)
    3.88 -fun instantiate instpair th = Thm.instantiate instpair th COMP_INCR asm_rl;
    3.89 +fun instantiate instpair th = Thm.instantiate instpair th  COMP   asm_rl;
    3.90  
    3.91  fun read_instantiate_sg' thy sinsts th =
    3.92      let val ts = types_sorts th;
    3.93 @@ -1070,6 +1052,17 @@
    3.94    end;
    3.95  
    3.96  
    3.97 +(* var indexes *)
    3.98 +
    3.99 +fun incr_indexes th = Thm.incr_indexes (Thm.maxidx_of th + 1);
   3.100 +
   3.101 +fun incr_indexes2 th1 th2 =
   3.102 +  Thm.incr_indexes (Int.max (Thm.maxidx_of th1, Thm.maxidx_of th2) + 1);
   3.103 +
   3.104 +fun th1 INCR_COMP th2 = incr_indexes th2 th1 COMP th2;
   3.105 +fun th1 COMP_INCR th2 = th1 COMP incr_indexes th1 th2;
   3.106 +
   3.107 +
   3.108  
   3.109  (** multi_resolve **)
   3.110  
     4.1 --- a/src/Pure/pure_thy.ML	Wed Nov 29 23:28:13 2006 +0100
     4.2 +++ b/src/Pure/pure_thy.ML	Wed Nov 29 23:33:09 2006 +0100
     4.3 @@ -418,7 +418,10 @@
     4.4    | smart_store name_thm (name, [thm]) =
     4.5        fst (enter_thms (name_thm true) (name_thm false) I (name, [thm]) (Thm.theory_of_thm thm))
     4.6    | smart_store name_thm (name, thms) =
     4.7 -      let val thy = Theory.merge_list (map Thm.theory_of_thm thms)
     4.8 +      let
     4.9 +        fun merge th thy = Theory.merge (thy, Thm.theory_of_thm th)
    4.10 +          handle TERM (msg, _) => raise THM (msg, 0, [th]);
    4.11 +        val thy = fold merge (tl thms) (Thm.theory_of_thm (hd thms));
    4.12        in fst (enter_thms (name_thm true) (name_thm false) I (name, thms) thy) end;
    4.13  
    4.14  in