src/Pure/assumption.ML
author haftmann
Fri Nov 10 07:44:47 2006 +0100 (2006-11-10)
changeset 21286 b5e7b80caa6a
parent 20296 753fad9f6e03
child 21517 b165c9120702
permissions -rw-r--r--
introduces canonical AList functions for loop_tacs
     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 end;
    22 
    23 structure Assumption: ASSUMPTION =
    24 struct
    25 
    26 (** basic rules **)
    27 
    28 type export = bool -> cterm list -> thm -> thm
    29 
    30 (*
    31     [A]
    32      :
    33      B
    34   --------
    35   #A ==> B
    36 *)
    37 fun assume_export true = Drule.implies_intr_protected
    38   | assume_export false = Drule.implies_intr_list;
    39 
    40 (*
    41     [A]
    42      :
    43      B
    44   -------
    45   A ==> B
    46 *)
    47 fun presume_export _ = assume_export false;
    48 
    49 val assume = norm_hhf o Thm.assume;
    50 
    51 
    52 
    53 (** local context data **)
    54 
    55 datatype data = Data of
    56  {assms: (export * cterm list) list,    (*assumes and views: A ==> _*)
    57   prems: thm list};                     (*prems: A |- A*)
    58 
    59 fun make_data (assms, prems) = Data {assms = assms, prems = prems};
    60 
    61 structure Data = ProofDataFun
    62 (
    63   val name = "Pure/assumption";
    64   type T = data;
    65   fun init _ = make_data ([], []);
    66   fun print _ _ = ();
    67 );
    68 
    69 val _ = Context.add_setup Data.init;
    70 
    71 fun map_data f = Data.map (fn Data {assms, prems} => make_data (f (assms, prems)));
    72 fun rep_data ctxt = Data.get ctxt |> (fn Data args => args);
    73 
    74 val assumptions_of = #assms o rep_data;
    75 val assms_of = map Thm.term_of o maps #2 o assumptions_of;
    76 val prems_of = #prems o rep_data;
    77 
    78 fun extra_hyps ctxt th = subtract (op aconv) (assms_of ctxt) (Thm.hyps_of th);
    79 
    80 
    81 (* add assumptions *)
    82 
    83 fun add_assms export new_asms =
    84   let val new_prems = map assume new_asms in
    85     map_data (fn (asms, prems) => (asms @ [(export, new_asms)], prems @ new_prems)) #>
    86     pair new_prems
    87   end;
    88 
    89 val add_assumes = add_assms assume_export;
    90 
    91 fun add_view outer view = map_data (fn (asms, prems) =>
    92   let
    93     val (asms1, asms2) = chop (length (assumptions_of outer)) asms;
    94     val asms' = asms1 @ [(assume_export, view)] @ asms2;
    95   in (asms', prems) end);
    96 
    97 
    98 (* export *)
    99 
   100 fun export is_goal inner outer =
   101   let val asms = Library.drop (length (assumptions_of outer), assumptions_of inner) in
   102     norm_hhf_protect
   103     #> fold_rev (fn (e, As) => e is_goal As) asms
   104     #> norm_hhf_protect
   105   end;
   106 
   107 end;