src/Pure/assumption.ML
author wenzelm
Fri Nov 24 22:05:13 2006 +0100 (2006-11-24)
changeset 21517 b165c9120702
parent 20296 753fad9f6e03
child 21577 3ff126ca39b4
permissions -rw-r--r--
added export_morphism;
     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 -> term 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_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
    30 
    31 (*
    32     [A]
    33      :
    34      B
    35   --------
    36   #A ==> B
    37 *)
    38 fun assume_export true = Drule.implies_intr_protected
    39   | assume_export false = Drule.implies_intr_list;
    40 
    41 (*
    42     [A]
    43      :
    44      B
    45   -------
    46   A ==> B
    47 *)
    48 fun presume_export _ = assume_export false;
    49 
    50 val assume = 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   val name = "Pure/assumption";
    65   type T = data;
    66   fun init _ = make_data ([], []);
    67   fun print _ _ = ();
    68 );
    69 
    70 val _ = Context.add_setup Data.init;
    71 
    72 fun map_data f = Data.map (fn Data {assms, prems} => make_data (f (assms, prems)));
    73 fun rep_data ctxt = Data.get ctxt |> (fn Data args => args);
    74 
    75 val assumptions_of = #assms o rep_data;
    76 val assms_of = map Thm.term_of o maps #2 o assumptions_of;
    77 val prems_of = #prems o rep_data;
    78 
    79 fun extra_hyps ctxt th = subtract (op aconv) (assms_of ctxt) (Thm.hyps_of th);
    80 
    81 
    82 (* add assumptions *)
    83 
    84 fun add_assms export new_asms =
    85   let val new_prems = map assume new_asms in
    86     map_data (fn (asms, prems) => (asms @ [(export, new_asms)], prems @ new_prems)) #>
    87     pair new_prems
    88   end;
    89 
    90 val add_assumes = add_assms assume_export;
    91 
    92 fun add_view outer view = map_data (fn (asms, prems) =>
    93   let
    94     val (asms1, asms2) = chop (length (assumptions_of outer)) asms;
    95     val asms' = asms1 @ [(assume_export, view)] @ asms2;
    96   in (asms', prems) end);
    97 
    98 
    99 (* export *)
   100 
   101 fun export is_goal inner outer =
   102   let val asms = Library.drop (length (assumptions_of outer), assumptions_of inner) in
   103     norm_hhf_protect
   104     #> fold_rev (fn (e, As) => e is_goal As) asms
   105     #> norm_hhf_protect
   106   end;
   107 
   108 fun export_morphism inner outer =
   109   let
   110     val thm = export false inner outer;
   111     fun term t = Drule.term_rule (ProofContext.theory_of inner (*delayed until now*)) thm t;
   112     val typ = Logic.type_map term;
   113   in Morphism.morphism {name = I, var = I, typ = typ, term = term, fact = map thm} end;
   114 
   115 end;