src/Pure/assumption.ML
author haftmann
Wed Jan 21 16:47:04 2009 +0100 (2009-01-21)
changeset 29579 cb520b766e00
parent 28965 1de908189869
child 29605 f2924219125e
permissions -rw-r--r--
binding replaces bstring
     1 (*  Title:      Pure/assumption.ML
     2     Author:     Makarius
     3 
     4 Local assumptions, parameterized by export rules.
     5 *)
     6 
     7 signature ASSUMPTION =
     8 sig
     9   type export
    10   val assume_export: export
    11   val presume_export: export
    12   val assume: cterm -> thm
    13   val assms_of: Proof.context -> cterm list
    14   val prems_of: Proof.context -> thm list
    15   val extra_hyps: Proof.context -> thm -> term list
    16   val add_assms: export -> cterm list -> Proof.context -> thm list * Proof.context
    17   val add_assumes: cterm list -> Proof.context -> thm list * Proof.context
    18   val add_view: Proof.context -> cterm list -> Proof.context -> Proof.context
    19   val export: bool -> Proof.context -> Proof.context -> thm -> thm
    20   val export_term: Proof.context -> Proof.context -> term -> term
    21   val export_morphism: Proof.context -> Proof.context -> morphism
    22 end;
    23 
    24 structure Assumption: ASSUMPTION =
    25 struct
    26 
    27 (** basic rules **)
    28 
    29 type export = bool -> cterm list -> (thm -> thm) * (term -> term);
    30 
    31 (*
    32     [A]
    33      :
    34      B
    35   --------
    36   #A ==> B
    37 *)
    38 fun assume_export is_goal asms =
    39   (if is_goal then Drule.implies_intr_protected asms else Drule.implies_intr_list asms, fn t => t);
    40 
    41 (*
    42     [A]
    43      :
    44      B
    45   -------
    46   A ==> B
    47 *)
    48 fun presume_export _ = assume_export false;
    49 
    50 val assume = MetaSimplifier.norm_hhf o Thm.assume;
    51 
    52 
    53 
    54 (** local context data **)
    55 
    56 datatype data = Data of
    57  {assms: (export * cterm list) list,    (*assumes and views: A ==> _*)
    58   prems: thm list};                     (*prems: A |- A*)
    59 
    60 fun make_data (assms, prems) = Data {assms = assms, prems = prems};
    61 
    62 structure Data = ProofDataFun
    63 (
    64   type T = data;
    65   fun init _ = make_data ([], []);
    66 );
    67 
    68 fun map_data f = Data.map (fn Data {assms, prems} => make_data (f (assms, prems)));
    69 fun rep_data ctxt = Data.get ctxt |> (fn Data args => args);
    70 
    71 val assumptions_of = #assms o rep_data;
    72 val assms_of = maps #2 o assumptions_of;
    73 val prems_of = #prems o rep_data;
    74 
    75 fun extra_hyps ctxt th = subtract (op aconv) (map Thm.term_of (assms_of ctxt)) (Thm.hyps_of th);
    76 
    77 
    78 (* named prems -- legacy feature *)
    79 
    80 val _ = Context.>>
    81   (Context.map_theory (PureThy.add_thms_dynamic (Binding.name "prems",
    82     fn Context.Theory _ => [] | Context.Proof ctxt => prems_of ctxt)));
    83 
    84 
    85 (* add assumptions *)
    86 
    87 fun add_assms export new_asms =
    88   let val new_prems = map assume new_asms in
    89     map_data (fn (asms, prems) => (asms @ [(export, new_asms)], prems @ new_prems)) #>
    90     pair new_prems
    91   end;
    92 
    93 val add_assumes = add_assms assume_export;
    94 
    95 fun add_view outer view = map_data (fn (asms, prems) =>
    96   let
    97     val (asms1, asms2) = chop (length (assumptions_of outer)) asms;
    98     val asms' = asms1 @ [(assume_export, view)] @ asms2;
    99   in (asms', prems) end);
   100 
   101 
   102 (* export *)
   103 
   104 fun diff_assms inner outer =
   105   Library.drop (length (assumptions_of outer), assumptions_of inner);
   106 
   107 fun export is_goal inner outer =
   108   let val asms = diff_assms inner outer in
   109     MetaSimplifier.norm_hhf_protect
   110     #> fold_rev (fn (e, As) => #1 (e is_goal As)) asms
   111     #> MetaSimplifier.norm_hhf_protect
   112   end;
   113 
   114 fun export_term inner outer =
   115   fold_rev (fn (e, As) => #2 (e false As)) (diff_assms inner outer);
   116 
   117 fun export_morphism inner outer =
   118   let
   119     val thm = export false inner outer;
   120     val term = export_term inner outer;
   121     val typ = Logic.type_map term;
   122   in Morphism.morphism {binding = I, var = I, typ = typ, term = term, fact = map thm} end;
   123 
   124 end;