export: added explicit term operation;
authorwenzelm
Wed Dec 06 21:18:56 2006 +0100 (2006-12-06)
changeset 2167906715e253686
parent 21678 fcfc4afde6b9
child 21680 5d2230ad1261
export: added explicit term operation;
tuned export_morphism -- lean closure;
src/Pure/assumption.ML
     1.1 --- a/src/Pure/assumption.ML	Wed Dec 06 21:18:55 2006 +0100
     1.2 +++ b/src/Pure/assumption.ML	Wed Dec 06 21:18:56 2006 +0100
     1.3 @@ -18,6 +18,7 @@
     1.4    val add_assumes: cterm list -> Proof.context -> thm list * Proof.context
     1.5    val add_view: Proof.context -> cterm list -> Proof.context -> Proof.context
     1.6    val export: bool -> Proof.context -> Proof.context -> thm -> thm
     1.7 +  val export_term: Proof.context -> Proof.context -> term -> term
     1.8    val export_morphism: Proof.context -> Proof.context -> morphism
     1.9  end;
    1.10  
    1.11 @@ -26,7 +27,7 @@
    1.12  
    1.13  (** basic rules **)
    1.14  
    1.15 -type export = bool -> cterm list -> thm -> thm
    1.16 +type export = bool -> cterm list -> (thm -> thm) * (term -> term);
    1.17  
    1.18  (*
    1.19      [A]
    1.20 @@ -35,8 +36,8 @@
    1.21    --------
    1.22    #A ==> B
    1.23  *)
    1.24 -fun assume_export true = Drule.implies_intr_protected
    1.25 -  | assume_export false = Drule.implies_intr_list;
    1.26 +fun assume_export is_goal asms =
    1.27 +  (if is_goal then Drule.implies_intr_protected asms else Drule.implies_intr_list asms, fn t => t);
    1.28  
    1.29  (*
    1.30      [A]
    1.31 @@ -98,17 +99,23 @@
    1.32  
    1.33  (* export *)
    1.34  
    1.35 +fun diff_assms inner outer =
    1.36 +  Library.drop (length (assumptions_of outer), assumptions_of inner);
    1.37 +
    1.38  fun export is_goal inner outer =
    1.39 -  let val asms = Library.drop (length (assumptions_of outer), assumptions_of inner) in
    1.40 +  let val asms = diff_assms inner outer in
    1.41      MetaSimplifier.norm_hhf_protect
    1.42 -    #> fold_rev (fn (e, As) => e is_goal As) asms
    1.43 +    #> fold_rev (fn (e, As) => #1 (e is_goal As)) asms
    1.44      #> MetaSimplifier.norm_hhf_protect
    1.45    end;
    1.46  
    1.47 +fun export_term inner outer =
    1.48 +  fold_rev (fn (e, As) => #2 (e false As)) (diff_assms inner outer);
    1.49 +
    1.50  fun export_morphism inner outer =
    1.51    let
    1.52      val thm = export false inner outer;
    1.53 -    fun term t = Drule.term_rule (ProofContext.theory_of inner (*delayed until now*)) thm t;
    1.54 +    val term = export_term inner outer;
    1.55      val typ = Logic.type_map term;
    1.56    in Morphism.morphism {name = I, var = I, typ = typ, term = term, fact = map thm} end;
    1.57