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
wenzelm@20222
     1
(*  Title:      Pure/assumption.ML
wenzelm@20222
     2
    ID:         $Id$
wenzelm@20222
     3
    Author:     Makarius
wenzelm@20222
     4
wenzelm@20222
     5
Local assumptions, parameterized by export rules.
wenzelm@20222
     6
*)
wenzelm@20222
     7
wenzelm@20222
     8
signature ASSUMPTION =
wenzelm@20222
     9
sig
wenzelm@20222
    10
  type export
wenzelm@20222
    11
  val assume_export: export
wenzelm@20222
    12
  val presume_export: export
wenzelm@20222
    13
  val assume: cterm -> thm
wenzelm@20296
    14
  val assms_of: Proof.context -> term list
wenzelm@20296
    15
  val prems_of: Proof.context -> thm list
wenzelm@20296
    16
  val extra_hyps: Proof.context -> thm -> term list
wenzelm@20296
    17
  val add_assms: export -> cterm list -> Proof.context -> thm list * Proof.context
wenzelm@20296
    18
  val add_assumes: cterm list -> Proof.context -> thm list * Proof.context
wenzelm@20296
    19
  val add_view: Proof.context -> cterm list -> Proof.context -> Proof.context
wenzelm@20296
    20
  val export: bool -> Proof.context -> Proof.context -> thm -> thm
wenzelm@20222
    21
end;
wenzelm@20222
    22
wenzelm@20222
    23
structure Assumption: ASSUMPTION =
wenzelm@20222
    24
struct
wenzelm@20222
    25
wenzelm@20222
    26
(** basic rules **)
wenzelm@20222
    27
wenzelm@20296
    28
type export = bool -> cterm list -> thm -> thm
wenzelm@20222
    29
wenzelm@20222
    30
(*
wenzelm@20222
    31
    [A]
wenzelm@20222
    32
     :
wenzelm@20222
    33
     B
wenzelm@20222
    34
  --------
wenzelm@20222
    35
  #A ==> B
wenzelm@20222
    36
*)
wenzelm@20296
    37
fun assume_export true = Drule.implies_intr_protected
wenzelm@20296
    38
  | assume_export false = Drule.implies_intr_list;
wenzelm@20222
    39
wenzelm@20222
    40
(*
wenzelm@20222
    41
    [A]
wenzelm@20222
    42
     :
wenzelm@20222
    43
     B
wenzelm@20222
    44
  -------
wenzelm@20222
    45
  A ==> B
wenzelm@20222
    46
*)
wenzelm@20222
    47
fun presume_export _ = assume_export false;
wenzelm@20222
    48
wenzelm@20222
    49
val assume = norm_hhf o Thm.assume;
wenzelm@20222
    50
wenzelm@20222
    51
wenzelm@20222
    52
wenzelm@20222
    53
(** local context data **)
wenzelm@20222
    54
wenzelm@20222
    55
datatype data = Data of
wenzelm@20222
    56
 {assms: (export * cterm list) list,    (*assumes and views: A ==> _*)
wenzelm@20222
    57
  prems: thm list};                     (*prems: A |- A*)
wenzelm@20222
    58
wenzelm@20222
    59
fun make_data (assms, prems) = Data {assms = assms, prems = prems};
wenzelm@20222
    60
wenzelm@20222
    61
structure Data = ProofDataFun
wenzelm@20222
    62
(
wenzelm@20222
    63
  val name = "Pure/assumption";
wenzelm@20222
    64
  type T = data;
wenzelm@20222
    65
  fun init _ = make_data ([], []);
wenzelm@20222
    66
  fun print _ _ = ();
wenzelm@20222
    67
);
wenzelm@20222
    68
wenzelm@20222
    69
val _ = Context.add_setup Data.init;
wenzelm@20222
    70
wenzelm@20222
    71
fun map_data f = Data.map (fn Data {assms, prems} => make_data (f (assms, prems)));
wenzelm@20222
    72
fun rep_data ctxt = Data.get ctxt |> (fn Data args => args);
wenzelm@20222
    73
wenzelm@20222
    74
val assumptions_of = #assms o rep_data;
wenzelm@20222
    75
val assms_of = map Thm.term_of o maps #2 o assumptions_of;
wenzelm@20222
    76
val prems_of = #prems o rep_data;
wenzelm@20222
    77
wenzelm@20222
    78
fun extra_hyps ctxt th = subtract (op aconv) (assms_of ctxt) (Thm.hyps_of th);
wenzelm@20222
    79
wenzelm@20222
    80
wenzelm@20222
    81
(* add assumptions *)
wenzelm@20222
    82
wenzelm@20222
    83
fun add_assms export new_asms =
wenzelm@20222
    84
  let val new_prems = map assume new_asms in
wenzelm@20222
    85
    map_data (fn (asms, prems) => (asms @ [(export, new_asms)], prems @ new_prems)) #>
wenzelm@20222
    86
    pair new_prems
wenzelm@20222
    87
  end;
wenzelm@20222
    88
wenzelm@20222
    89
val add_assumes = add_assms assume_export;
wenzelm@20222
    90
wenzelm@20222
    91
fun add_view outer view = map_data (fn (asms, prems) =>
wenzelm@20222
    92
  let
wenzelm@20222
    93
    val (asms1, asms2) = chop (length (assumptions_of outer)) asms;
wenzelm@20222
    94
    val asms' = asms1 @ [(assume_export, view)] @ asms2;
wenzelm@20222
    95
  in (asms', prems) end);
wenzelm@20222
    96
wenzelm@20222
    97
wenzelm@20296
    98
(* export *)
wenzelm@20222
    99
wenzelm@20296
   100
fun export is_goal inner outer =
wenzelm@20296
   101
  let val asms = Library.drop (length (assumptions_of outer), assumptions_of inner) in
wenzelm@20296
   102
    norm_hhf_protect
wenzelm@20296
   103
    #> fold_rev (fn (e, As) => e is_goal As) asms
wenzelm@20296
   104
    #> norm_hhf_protect
wenzelm@20222
   105
  end;
wenzelm@20222
   106
wenzelm@20222
   107
end;