renamed assms_of to all_assms_of, and prems_of to all_prems_of;
authorwenzelm
Thu Mar 12 15:53:14 2009 +0100 (2009-03-12)
changeset 30471178de3995e91
parent 30470 9ae8f9d78cd3
child 30472 9dea0866021c
renamed assms_of to all_assms_of, and prems_of to all_prems_of;
added local_assms_of, local_prems_of;
removed unused add_view;
src/Pure/assumption.ML
     1.1 --- a/src/Pure/assumption.ML	Thu Mar 12 14:30:23 2009 +0100
     1.2 +++ b/src/Pure/assumption.ML	Thu Mar 12 15:53:14 2009 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4  (*  Title:      Pure/assumption.ML
     1.5      Author:     Makarius
     1.6  
     1.7 -Local assumptions, parameterized by export rules.
     1.8 +Context assumptions, parameterized by export rules.
     1.9  *)
    1.10  
    1.11  signature ASSUMPTION =
    1.12 @@ -10,12 +10,13 @@
    1.13    val assume_export: export
    1.14    val presume_export: export
    1.15    val assume: cterm -> thm
    1.16 -  val assms_of: Proof.context -> cterm list
    1.17 -  val prems_of: Proof.context -> thm list
    1.18 +  val all_assms_of: Proof.context -> cterm list
    1.19 +  val all_prems_of: Proof.context -> thm list
    1.20    val extra_hyps: Proof.context -> thm -> term list
    1.21 +  val local_assms_of: Proof.context -> Proof.context -> cterm list
    1.22 +  val local_prems_of: Proof.context -> Proof.context -> thm list
    1.23    val add_assms: export -> cterm list -> Proof.context -> thm list * Proof.context
    1.24    val add_assumes: cterm list -> Proof.context -> thm list * Proof.context
    1.25 -  val add_view: Proof.context -> cterm list -> Proof.context -> Proof.context
    1.26    val export: bool -> Proof.context -> Proof.context -> thm -> thm
    1.27    val export_term: Proof.context -> Proof.context -> term -> term
    1.28    val export_morphism: Proof.context -> Proof.context -> morphism
    1.29 @@ -68,18 +69,31 @@
    1.30  fun map_data f = Data.map (fn Data {assms, prems} => make_data (f (assms, prems)));
    1.31  fun rep_data ctxt = Data.get ctxt |> (fn Data args => args);
    1.32  
    1.33 -val assumptions_of = #assms o rep_data;
    1.34 -val assms_of = maps #2 o assumptions_of;
    1.35 -val prems_of = #prems o rep_data;
    1.36 +
    1.37 +(* all assumptions *)
    1.38 +
    1.39 +val all_assumptions_of = #assms o rep_data;
    1.40 +val all_assms_of = maps #2 o all_assumptions_of;
    1.41 +val all_prems_of = #prems o rep_data;
    1.42  
    1.43 -fun extra_hyps ctxt th = subtract (op aconv) (map Thm.term_of (assms_of ctxt)) (Thm.hyps_of th);
    1.44 +fun extra_hyps ctxt th =
    1.45 +  subtract (op aconv) (map Thm.term_of (all_assms_of ctxt)) (Thm.hyps_of th);
    1.46 +
    1.47 +(*named prems -- legacy feature*)
    1.48 +val _ = Context.>>
    1.49 +  (Context.map_theory (PureThy.add_thms_dynamic (Binding.name "prems",
    1.50 +    fn Context.Theory _ => [] | Context.Proof ctxt => all_prems_of ctxt)));
    1.51  
    1.52  
    1.53 -(* named prems -- legacy feature *)
    1.54 +(* local assumptions *)
    1.55 +
    1.56 +fun local_assumptions_of inner outer =
    1.57 +  Library.drop (length (all_assumptions_of outer), all_assumptions_of inner);
    1.58  
    1.59 -val _ = Context.>>
    1.60 -  (Context.map_theory (PureThy.add_thms_dynamic (Binding.name "prems",
    1.61 -    fn Context.Theory _ => [] | Context.Proof ctxt => prems_of ctxt)));
    1.62 +val local_assms_of = maps #2 oo local_assumptions_of;
    1.63 +
    1.64 +fun local_prems_of inner outer =
    1.65 +  Library.drop (length (all_prems_of outer), all_prems_of inner);
    1.66  
    1.67  
    1.68  (* add assumptions *)
    1.69 @@ -92,27 +106,18 @@
    1.70  
    1.71  val add_assumes = add_assms assume_export;
    1.72  
    1.73 -fun add_view outer view = map_data (fn (asms, prems) =>
    1.74 -  let
    1.75 -    val (asms1, asms2) = chop (length (assumptions_of outer)) asms;
    1.76 -    val asms' = asms1 @ [(assume_export, view)] @ asms2;
    1.77 -  in (asms', prems) end);
    1.78 -
    1.79  
    1.80  (* export *)
    1.81  
    1.82 -fun diff_assms inner outer =
    1.83 -  Library.drop (length (assumptions_of outer), assumptions_of inner);
    1.84 -
    1.85  fun export is_goal inner outer =
    1.86 -  let val asms = diff_assms inner outer in
    1.87 +  let val asms = local_assumptions_of inner outer in
    1.88      MetaSimplifier.norm_hhf_protect
    1.89      #> fold_rev (fn (e, As) => #1 (e is_goal As)) asms
    1.90      #> MetaSimplifier.norm_hhf_protect
    1.91    end;
    1.92  
    1.93  fun export_term inner outer =
    1.94 -  fold_rev (fn (e, As) => #2 (e false As)) (diff_assms inner outer);
    1.95 +  fold_rev (fn (e, As) => #2 (e false As)) (local_assumptions_of inner outer);
    1.96  
    1.97  fun export_morphism inner outer =
    1.98    let