src/Pure/assumption.ML
author wenzelm
Sun Nov 27 21:53:38 2011 +0100 (2011-11-27)
changeset 45650 d314a4e8038f
parent 45289 25e9e7f527b4
child 46493 7e69b9f3149f
permissions -rw-r--r--
tuned;
     1 (*  Title:      Pure/assumption.ML
     2     Author:     Makarius
     3 
     4 Context assumptions, parameterized by export rules.
     5 *)
     6 
     7 signature ASSUMPTION =
     8 sig
     9   type export = bool -> cterm list -> (thm -> thm) * (term -> term)
    10   val assume_export: export
    11   val presume_export: export
    12   val assume: cterm -> thm
    13   val all_assms_of: Proof.context -> cterm list
    14   val all_prems_of: Proof.context -> thm list
    15   val extra_hyps: Proof.context -> thm -> term list
    16   val local_assms_of: Proof.context -> Proof.context -> cterm list
    17   val local_prems_of: Proof.context -> Proof.context -> thm list
    18   val add_assms: export -> cterm list -> Proof.context -> thm list * Proof.context
    19   val add_assumes: cterm list -> Proof.context -> thm list * 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 = Raw_Simplifier.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: A ==> _*)
    59   prems: thm list};                     (*prems: A |- A*)
    60 
    61 fun make_data (assms, prems) = Data {assms = assms, prems = prems};
    62 
    63 structure Data = Proof_Data
    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 rep => rep);
    71 
    72 
    73 (* all assumptions *)
    74 
    75 val all_assumptions_of = #assms o rep_data;
    76 val all_assms_of = maps #2 o all_assumptions_of;
    77 val all_prems_of = #prems o rep_data;
    78 
    79 fun extra_hyps ctxt th =
    80   subtract (op aconv) (map Thm.term_of (all_assms_of ctxt)) (Thm.hyps_of th);
    81 
    82 val _ = Context.>>
    83   (Context.map_theory (Global_Theory.add_thms_dynamic (Binding.name "prems",
    84     fn Context.Theory _ => []
    85      | Context.Proof ctxt =>
    86         (legacy_feature ("Use of global prems" ^ Position.str_of (Position.thread_data ()));
    87           all_prems_of ctxt))));
    88 
    89 
    90 (* local assumptions *)
    91 
    92 fun local_assumptions_of inner outer =
    93   drop (length (all_assumptions_of outer)) (all_assumptions_of inner);
    94 
    95 val local_assms_of = maps #2 oo local_assumptions_of;
    96 
    97 fun local_prems_of inner outer =
    98   drop (length (all_prems_of outer)) (all_prems_of inner);
    99 
   100 
   101 (* add assumptions *)
   102 
   103 fun add_assms export new_asms =
   104   let val new_prems = map assume new_asms in
   105     map_data (fn (asms, prems) => (asms @ [(export, new_asms)], prems @ new_prems)) #>
   106     pair new_prems
   107   end;
   108 
   109 val add_assumes = add_assms assume_export;
   110 
   111 
   112 (* export *)
   113 
   114 fun export is_goal inner outer =
   115   Raw_Simplifier.norm_hhf_protect #>
   116   fold_rev (fn (e, As) => #1 (e is_goal As)) (local_assumptions_of inner outer) #>
   117   Raw_Simplifier.norm_hhf_protect;
   118 
   119 fun export_term inner outer =
   120   fold_rev (fn (e, As) => #2 (e false As)) (local_assumptions_of inner outer);
   121 
   122 fun export_morphism inner outer =
   123   let
   124     val thm = export false inner outer;
   125     val term = export_term inner outer;
   126     val typ = Logic.type_map term;
   127   in Morphism.morphism {binding = [], typ = [typ], term = [term], fact = [map thm]} end;
   128 
   129 end;