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