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