src/Pure/variable.ML
changeset 19926 feb4d150cfd8
parent 19911 300bc6ce970d
child 20003 aac2c0d29751
     1.1 --- a/src/Pure/variable.ML	Mon Jun 19 20:21:30 2006 +0200
     1.2 +++ b/src/Pure/variable.ML	Mon Jun 19 20:21:32 2006 +0200
     1.3 @@ -24,6 +24,8 @@
     1.4    val declare_type: typ -> Context.proof -> Context.proof
     1.5    val declare_syntax: term -> Context.proof -> Context.proof
     1.6    val declare_term: term -> Context.proof -> Context.proof
     1.7 +  val declare_thm: thm -> Context.proof -> Context.proof
     1.8 +  val thm_context: thm -> Context.proof
     1.9    val rename_wrt: Context.proof -> term list -> (string * 'a) list -> (string * 'a) list
    1.10    val add_fixes: string list -> Context.proof -> string list * Context.proof
    1.11    val invent_fixes: string list -> Context.proof -> string list * Context.proof
    1.12 @@ -41,6 +43,8 @@
    1.13    val import_terms: bool -> term list -> Context.proof -> term list * Context.proof
    1.14    val importT: thm list -> Context.proof -> thm list * Context.proof
    1.15    val import: bool -> thm list -> Context.proof -> thm list * Context.proof
    1.16 +  val tradeT: Context.proof -> (thm list -> thm list) -> thm list -> thm list
    1.17 +  val trade: Context.proof -> (thm list -> thm list) -> thm list -> thm list
    1.18    val warn_extra_tfrees: Context.proof -> Context.proof -> unit
    1.19    val monomorphic: Context.proof -> term list -> term list
    1.20    val polymorphic: Context.proof -> term list -> term list
    1.21 @@ -181,6 +185,9 @@
    1.22        used,
    1.23        ins_occs t occ));
    1.24  
    1.25 +fun declare_thm th = fold declare_term (Thm.full_prop_of th :: Thm.hyps_of th);
    1.26 +fun thm_context th = Context.init_proof (Thm.theory_of_thm th) |> declare_thm th;
    1.27 +
    1.28  end;
    1.29  
    1.30  
    1.31 @@ -263,9 +270,10 @@
    1.32  
    1.33  fun gen_export inst inner outer ths =
    1.34    let
    1.35 -    val maxidx = fold Thm.maxidx_thm ths ~1;
    1.36 -    val inner' = fold (declare_occs o Thm.full_prop_of) ths inner;
    1.37 -  in map (Thm.generalize (inst inner' outer) (maxidx + 1)) ths end;
    1.38 +    val ths' = map Thm.adjust_maxidx_thm ths;
    1.39 +    val maxidx = fold Thm.maxidx_thm ths' ~1;
    1.40 +    val inner' = fold (declare_occs o Thm.full_prop_of) ths' inner;
    1.41 +  in map (Thm.generalize (inst inner' outer) (maxidx + 1)) ths' end;
    1.42  
    1.43  val exportT = gen_export (rpair [] oo exportT_inst);
    1.44  val export = gen_export export_inst;
    1.45 @@ -318,6 +326,16 @@
    1.46    in (ths', ctxt') end;
    1.47  
    1.48  
    1.49 +(* import/export *)
    1.50 +
    1.51 +fun gen_trade imp exp ctxt f ths =
    1.52 +  let val (ths', ctxt') = imp ths ctxt
    1.53 +  in exp ctxt' ctxt (f ths') end;
    1.54 +
    1.55 +val tradeT = gen_trade importT exportT;
    1.56 +val trade = gen_trade (import true) export;
    1.57 +
    1.58 +
    1.59  
    1.60  (** implicit polymorphism **)
    1.61