src/Pure/assumption.ML
author wenzelm
Thu Aug 15 16:02:47 2019 +0200 (9 months ago)
changeset 70533 031620901fcd
parent 70313 9c19e15c8548
child 70735 561b11865cb5
permissions -rw-r--r--
support for (fully reconstructed) proof terms in Scala;
proper cache_typs;
wenzelm@20222
     1
(*  Title:      Pure/assumption.ML
wenzelm@20222
     2
    Author:     Makarius
wenzelm@20222
     3
wenzelm@30471
     4
Context assumptions, parameterized by export rules.
wenzelm@20222
     5
*)
wenzelm@20222
     6
wenzelm@20222
     7
signature ASSUMPTION =
wenzelm@20222
     8
sig
wenzelm@35716
     9
  type export = bool -> cterm list -> (thm -> thm) * (term -> term)
wenzelm@20222
    10
  val assume_export: export
wenzelm@20222
    11
  val presume_export: export
wenzelm@54883
    12
  val assume: Proof.context -> cterm -> thm
wenzelm@54984
    13
  val assume_hyps: cterm -> Proof.context -> thm * Proof.context
wenzelm@30471
    14
  val all_assms_of: Proof.context -> cterm list
wenzelm@30471
    15
  val all_prems_of: Proof.context -> thm list
wenzelm@30471
    16
  val local_assms_of: Proof.context -> Proof.context -> cterm list
wenzelm@30471
    17
  val local_prems_of: Proof.context -> Proof.context -> thm list
wenzelm@20296
    18
  val add_assms: export -> cterm list -> Proof.context -> thm list * Proof.context
wenzelm@20296
    19
  val add_assumes: cterm list -> Proof.context -> thm list * Proof.context
wenzelm@20296
    20
  val export: bool -> Proof.context -> Proof.context -> thm -> thm
wenzelm@21679
    21
  val export_term: Proof.context -> Proof.context -> term -> term
wenzelm@21517
    22
  val export_morphism: Proof.context -> Proof.context -> morphism
wenzelm@20222
    23
end;
wenzelm@20222
    24
wenzelm@20222
    25
structure Assumption: ASSUMPTION =
wenzelm@20222
    26
struct
wenzelm@20222
    27
wenzelm@20222
    28
(** basic rules **)
wenzelm@20222
    29
wenzelm@21679
    30
type export = bool -> cterm list -> (thm -> thm) * (term -> term);
wenzelm@20222
    31
wenzelm@20222
    32
(*
wenzelm@20222
    33
    [A]
wenzelm@20222
    34
     :
wenzelm@20222
    35
     B
wenzelm@20222
    36
  --------
wenzelm@67721
    37
  #A \<Longrightarrow> B
wenzelm@20222
    38
*)
wenzelm@21679
    39
fun assume_export is_goal asms =
wenzelm@21679
    40
  (if is_goal then Drule.implies_intr_protected asms else Drule.implies_intr_list asms, fn t => t);
wenzelm@20222
    41
wenzelm@20222
    42
(*
wenzelm@20222
    43
    [A]
wenzelm@20222
    44
     :
wenzelm@20222
    45
     B
wenzelm@20222
    46
  -------
wenzelm@67721
    47
  A \<Longrightarrow> B
wenzelm@20222
    48
*)
wenzelm@20222
    49
fun presume_export _ = assume_export false;
wenzelm@20222
    50
wenzelm@54984
    51
wenzelm@54883
    52
fun assume ctxt = Raw_Simplifier.norm_hhf ctxt o Thm.assume;
wenzelm@20222
    53
wenzelm@54984
    54
fun assume_hyps ct ctxt =
wenzelm@54984
    55
  let val (th, ctxt') = Thm.assume_hyps ct ctxt
wenzelm@54984
    56
  in (Raw_Simplifier.norm_hhf ctxt' th, ctxt') end;
wenzelm@54984
    57
wenzelm@20222
    58
wenzelm@20222
    59
wenzelm@20222
    60
(** local context data **)
wenzelm@20222
    61
wenzelm@20222
    62
datatype data = Data of
wenzelm@67721
    63
 {assms: (export * cterm list) list,    (*assumes: A \<Longrightarrow> _*)
wenzelm@47236
    64
  prems: thm list};                     (*prems: A |- norm_hhf A*)
wenzelm@20222
    65
wenzelm@20222
    66
fun make_data (assms, prems) = Data {assms = assms, prems = prems};
wenzelm@59150
    67
val empty_data = make_data ([], []);
wenzelm@20222
    68
wenzelm@33519
    69
structure Data = Proof_Data
wenzelm@20222
    70
(
wenzelm@20222
    71
  type T = data;
wenzelm@59150
    72
  fun init _ = empty_data;
wenzelm@20222
    73
);
wenzelm@20222
    74
wenzelm@20222
    75
fun map_data f = Data.map (fn Data {assms, prems} => make_data (f (assms, prems)));
wenzelm@45650
    76
fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep);
wenzelm@20222
    77
wenzelm@30471
    78
wenzelm@30471
    79
(* all assumptions *)
wenzelm@30471
    80
wenzelm@30471
    81
val all_assumptions_of = #assms o rep_data;
wenzelm@30471
    82
val all_assms_of = maps #2 o all_assumptions_of;
wenzelm@30471
    83
val all_prems_of = #prems o rep_data;
wenzelm@20222
    84
wenzelm@20222
    85
wenzelm@30471
    86
(* local assumptions *)
wenzelm@30471
    87
wenzelm@30471
    88
fun local_assumptions_of inner outer =
haftmann@33957
    89
  drop (length (all_assumptions_of outer)) (all_assumptions_of inner);
wenzelm@26392
    90
wenzelm@30471
    91
val local_assms_of = maps #2 oo local_assumptions_of;
wenzelm@30471
    92
wenzelm@30471
    93
fun local_prems_of inner outer =
haftmann@33957
    94
  drop (length (all_prems_of outer)) (all_prems_of inner);
wenzelm@26392
    95
wenzelm@26392
    96
wenzelm@20222
    97
(* add assumptions *)
wenzelm@20222
    98
wenzelm@54883
    99
fun add_assms export new_asms ctxt =
wenzelm@54984
   100
  let val (new_prems, ctxt') = fold_map assume_hyps new_asms ctxt in
wenzelm@54984
   101
    ctxt'
wenzelm@54883
   102
    |> map_data (fn (asms, prems) => (asms @ [(export, new_asms)], prems @ new_prems))
wenzelm@54883
   103
    |> pair new_prems
wenzelm@20222
   104
  end;
wenzelm@20222
   105
wenzelm@20222
   106
val add_assumes = add_assms assume_export;
wenzelm@20222
   107
wenzelm@20222
   108
wenzelm@20296
   109
(* export *)
wenzelm@20222
   110
wenzelm@70313
   111
fun normalize ctxt0 th0 =
wenzelm@70313
   112
  let val (ctxt, th) = Thm.join_transfer_context (ctxt0, th0)
wenzelm@70313
   113
  in Raw_Simplifier.norm_hhf_protect ctxt th end;
wenzelm@70313
   114
wenzelm@20296
   115
fun export is_goal inner outer =
wenzelm@70313
   116
  normalize inner #>
wenzelm@30479
   117
  fold_rev (fn (e, As) => #1 (e is_goal As)) (local_assumptions_of inner outer) #>
wenzelm@70313
   118
  normalize outer;
wenzelm@20222
   119
wenzelm@21679
   120
fun export_term inner outer =
wenzelm@30471
   121
  fold_rev (fn (e, As) => #2 (e false As)) (local_assumptions_of inner outer);
wenzelm@21679
   122
wenzelm@21517
   123
fun export_morphism inner outer =
wenzelm@21517
   124
  let
wenzelm@21517
   125
    val thm = export false inner outer;
wenzelm@21679
   126
    val term = export_term inner outer;
wenzelm@21517
   127
    val typ = Logic.type_map term;
wenzelm@54740
   128
  in
wenzelm@70313
   129
    Morphism.transfer_morphism' inner $>
wenzelm@70313
   130
    Morphism.transfer_morphism' outer $>
wenzelm@54740
   131
    Morphism.morphism "Assumption.export"
wenzelm@54740
   132
      {binding = [], typ = [typ], term = [term], fact = [map thm]}
wenzelm@54740
   133
  end;
wenzelm@21517
   134
wenzelm@20222
   135
end;