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