src/Pure/assumption.ML
author wenzelm
Sun, 29 Nov 2020 23:23:32 +0100
changeset 72786 21ff9c1a4644
parent 71177 71467e35fc3c
permissions -rw-r--r--
more Isabelle fonts, notably for PanelWindowContainer buttons with Windows L&F;
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
35716
9dd4747d9591 tuned signature;
wenzelm
parents: 33957
diff changeset
     9
  type export = bool -> cterm list -> (thm -> thm) * (term -> term)
20222
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
54883
dd04a8b654fc proper context for norm_hhf and derived operations;
wenzelm
parents: 54740
diff changeset
    12
  val assume: Proof.context -> cterm -> thm
54984
da70ab8531f4 more elementary management of declared hyps, below structure Assumption;
wenzelm
parents: 54883
diff changeset
    13
  val assume_hyps: cterm -> Proof.context -> thm * Proof.context
30471
178de3995e91 renamed assms_of to all_assms_of, and prems_of to all_prems_of;
wenzelm
parents: 29605
diff changeset
    14
  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
    15
  val all_prems_of: Proof.context -> thm list
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
  --------
67721
5348bea4accd eliminated ASCII syntax from Pure bootstrap;
wenzelm
parents: 59150
diff changeset
    37
  #A \<Longrightarrow> B
20222
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
  -------
67721
5348bea4accd eliminated ASCII syntax from Pure bootstrap;
wenzelm
parents: 59150
diff changeset
    47
  A \<Longrightarrow> B
20222
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
54984
da70ab8531f4 more elementary management of declared hyps, below structure Assumption;
wenzelm
parents: 54883
diff changeset
    51
54883
dd04a8b654fc proper context for norm_hhf and derived operations;
wenzelm
parents: 54740
diff changeset
    52
fun assume ctxt = Raw_Simplifier.norm_hhf ctxt o Thm.assume;
20222
e2b876cd9e29 Local assumptions, parameterized by export rules.
wenzelm
parents:
diff changeset
    53
54984
da70ab8531f4 more elementary management of declared hyps, below structure Assumption;
wenzelm
parents: 54883
diff changeset
    54
fun assume_hyps ct ctxt =
da70ab8531f4 more elementary management of declared hyps, below structure Assumption;
wenzelm
parents: 54883
diff changeset
    55
  let val (th, ctxt') = Thm.assume_hyps ct ctxt
da70ab8531f4 more elementary management of declared hyps, below structure Assumption;
wenzelm
parents: 54883
diff changeset
    56
  in (Raw_Simplifier.norm_hhf ctxt' th, ctxt') end;
da70ab8531f4 more elementary management of declared hyps, below structure Assumption;
wenzelm
parents: 54883
diff changeset
    57
20222
e2b876cd9e29 Local assumptions, parameterized by export rules.
wenzelm
parents:
diff changeset
    58
e2b876cd9e29 Local assumptions, parameterized by export rules.
wenzelm
parents:
diff changeset
    59
e2b876cd9e29 Local assumptions, parameterized by export rules.
wenzelm
parents:
diff changeset
    60
(** local context data **)
e2b876cd9e29 Local assumptions, parameterized by export rules.
wenzelm
parents:
diff changeset
    61
e2b876cd9e29 Local assumptions, parameterized by export rules.
wenzelm
parents:
diff changeset
    62
datatype data = Data of
67721
5348bea4accd eliminated ASCII syntax from Pure bootstrap;
wenzelm
parents: 59150
diff changeset
    63
 {assms: (export * cterm list) list,    (*assumes: A \<Longrightarrow> _*)
47236
973ab740a25d tuned comment;
wenzelm
parents: 46493
diff changeset
    64
  prems: thm list};                     (*prems: A |- norm_hhf A*)
20222
e2b876cd9e29 Local assumptions, parameterized by export rules.
wenzelm
parents:
diff changeset
    65
e2b876cd9e29 Local assumptions, parameterized by export rules.
wenzelm
parents:
diff changeset
    66
fun make_data (assms, prems) = Data {assms = assms, prems = prems};
59150
wenzelm
parents: 54984
diff changeset
    67
val empty_data = make_data ([], []);
20222
e2b876cd9e29 Local assumptions, parameterized by export rules.
wenzelm
parents:
diff changeset
    68
33519
e31a85f92ce9 adapted Generic_Data, Proof_Data;
wenzelm
parents: 30479
diff changeset
    69
structure Data = Proof_Data
20222
e2b876cd9e29 Local assumptions, parameterized by export rules.
wenzelm
parents:
diff changeset
    70
(
e2b876cd9e29 Local assumptions, parameterized by export rules.
wenzelm
parents:
diff changeset
    71
  type T = data;
59150
wenzelm
parents: 54984
diff changeset
    72
  fun init _ = empty_data;
20222
e2b876cd9e29 Local assumptions, parameterized by export rules.
wenzelm
parents:
diff changeset
    73
);
e2b876cd9e29 Local assumptions, parameterized by export rules.
wenzelm
parents:
diff changeset
    74
e2b876cd9e29 Local assumptions, parameterized by export rules.
wenzelm
parents:
diff changeset
    75
fun map_data f = Data.map (fn Data {assms, prems} => make_data (f (assms, prems)));
45650
wenzelm
parents: 45289
diff changeset
    76
fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep);
20222
e2b876cd9e29 Local assumptions, parameterized by export rules.
wenzelm
parents:
diff changeset
    77
30471
178de3995e91 renamed assms_of to all_assms_of, and prems_of to all_prems_of;
wenzelm
parents: 29605
diff changeset
    78
178de3995e91 renamed assms_of to all_assms_of, and prems_of to all_prems_of;
wenzelm
parents: 29605
diff changeset
    79
(* all assumptions *)
178de3995e91 renamed assms_of to all_assms_of, and prems_of to all_prems_of;
wenzelm
parents: 29605
diff changeset
    80
178de3995e91 renamed assms_of to all_assms_of, and prems_of to all_prems_of;
wenzelm
parents: 29605
diff changeset
    81
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
    82
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
    83
val all_prems_of = #prems o rep_data;
20222
e2b876cd9e29 Local assumptions, parameterized by export rules.
wenzelm
parents:
diff changeset
    84
e2b876cd9e29 Local assumptions, parameterized by export rules.
wenzelm
parents:
diff changeset
    85
30471
178de3995e91 renamed assms_of to all_assms_of, and prems_of to all_prems_of;
wenzelm
parents: 29605
diff changeset
    86
(* local assumptions *)
178de3995e91 renamed assms_of to all_assms_of, and prems_of to all_prems_of;
wenzelm
parents: 29605
diff changeset
    87
70735
561b11865cb5 explicit check of assumption prefix;
wenzelm
parents: 70313
diff changeset
    88
local
561b11865cb5 explicit check of assumption prefix;
wenzelm
parents: 70313
diff changeset
    89
561b11865cb5 explicit check of assumption prefix;
wenzelm
parents: 70313
diff changeset
    90
fun drop_prefix eq (args as (x :: xs, y :: ys)) =
561b11865cb5 explicit check of assumption prefix;
wenzelm
parents: 70313
diff changeset
    91
      if eq (x, y) then drop_prefix eq (xs, ys) else args
561b11865cb5 explicit check of assumption prefix;
wenzelm
parents: 70313
diff changeset
    92
  | drop_prefix _ args = args;
561b11865cb5 explicit check of assumption prefix;
wenzelm
parents: 70313
diff changeset
    93
561b11865cb5 explicit check of assumption prefix;
wenzelm
parents: 70313
diff changeset
    94
fun check_result ctxt kind term_of res =
561b11865cb5 explicit check of assumption prefix;
wenzelm
parents: 70313
diff changeset
    95
  (case res of
561b11865cb5 explicit check of assumption prefix;
wenzelm
parents: 70313
diff changeset
    96
    ([], rest) => rest
561b11865cb5 explicit check of assumption prefix;
wenzelm
parents: 70313
diff changeset
    97
  | (bad :: _, _) =>
561b11865cb5 explicit check of assumption prefix;
wenzelm
parents: 70313
diff changeset
    98
      raise Fail ("Outer context disagrees on " ^ kind ^ ": " ^
561b11865cb5 explicit check of assumption prefix;
wenzelm
parents: 70313
diff changeset
    99
        Syntax.string_of_term ctxt (term_of bad)));
561b11865cb5 explicit check of assumption prefix;
wenzelm
parents: 70313
diff changeset
   100
561b11865cb5 explicit check of assumption prefix;
wenzelm
parents: 70313
diff changeset
   101
in
561b11865cb5 explicit check of assumption prefix;
wenzelm
parents: 70313
diff changeset
   102
30471
178de3995e91 renamed assms_of to all_assms_of, and prems_of to all_prems_of;
wenzelm
parents: 29605
diff changeset
   103
fun local_assumptions_of inner outer =
70735
561b11865cb5 explicit check of assumption prefix;
wenzelm
parents: 70313
diff changeset
   104
  drop_prefix (eq_snd (eq_list Thm.aconvc)) (apply2 all_assumptions_of (outer, inner))
561b11865cb5 explicit check of assumption prefix;
wenzelm
parents: 70313
diff changeset
   105
  |>> maps #2
561b11865cb5 explicit check of assumption prefix;
wenzelm
parents: 70313
diff changeset
   106
  |> check_result outer "assumption" Thm.term_of;
26392
748b263f0e40 setup for dynamic "prems" (legacy);
wenzelm
parents: 22846
diff changeset
   107
30471
178de3995e91 renamed assms_of to all_assms_of, and prems_of to all_prems_of;
wenzelm
parents: 29605
diff changeset
   108
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
   109
178de3995e91 renamed assms_of to all_assms_of, and prems_of to all_prems_of;
wenzelm
parents: 29605
diff changeset
   110
fun local_prems_of inner outer =
70735
561b11865cb5 explicit check of assumption prefix;
wenzelm
parents: 70313
diff changeset
   111
  drop_prefix Thm.eq_thm_prop (apply2 all_prems_of (outer, inner))
561b11865cb5 explicit check of assumption prefix;
wenzelm
parents: 70313
diff changeset
   112
  |> check_result outer "premise" Thm.prop_of;
561b11865cb5 explicit check of assumption prefix;
wenzelm
parents: 70313
diff changeset
   113
561b11865cb5 explicit check of assumption prefix;
wenzelm
parents: 70313
diff changeset
   114
end;
26392
748b263f0e40 setup for dynamic "prems" (legacy);
wenzelm
parents: 22846
diff changeset
   115
748b263f0e40 setup for dynamic "prems" (legacy);
wenzelm
parents: 22846
diff changeset
   116
20222
e2b876cd9e29 Local assumptions, parameterized by export rules.
wenzelm
parents:
diff changeset
   117
(* add assumptions *)
e2b876cd9e29 Local assumptions, parameterized by export rules.
wenzelm
parents:
diff changeset
   118
54883
dd04a8b654fc proper context for norm_hhf and derived operations;
wenzelm
parents: 54740
diff changeset
   119
fun add_assms export new_asms ctxt =
54984
da70ab8531f4 more elementary management of declared hyps, below structure Assumption;
wenzelm
parents: 54883
diff changeset
   120
  let val (new_prems, ctxt') = fold_map assume_hyps new_asms ctxt in
da70ab8531f4 more elementary management of declared hyps, below structure Assumption;
wenzelm
parents: 54883
diff changeset
   121
    ctxt'
54883
dd04a8b654fc proper context for norm_hhf and derived operations;
wenzelm
parents: 54740
diff changeset
   122
    |> map_data (fn (asms, prems) => (asms @ [(export, new_asms)], prems @ new_prems))
dd04a8b654fc proper context for norm_hhf and derived operations;
wenzelm
parents: 54740
diff changeset
   123
    |> pair new_prems
20222
e2b876cd9e29 Local assumptions, parameterized by export rules.
wenzelm
parents:
diff changeset
   124
  end;
e2b876cd9e29 Local assumptions, parameterized by export rules.
wenzelm
parents:
diff changeset
   125
e2b876cd9e29 Local assumptions, parameterized by export rules.
wenzelm
parents:
diff changeset
   126
val add_assumes = add_assms assume_export;
e2b876cd9e29 Local assumptions, parameterized by export rules.
wenzelm
parents:
diff changeset
   127
e2b876cd9e29 Local assumptions, parameterized by export rules.
wenzelm
parents:
diff changeset
   128
20296
753fad9f6e03 simplified export: no Seq.seq;
wenzelm
parents: 20222
diff changeset
   129
(* export *)
20222
e2b876cd9e29 Local assumptions, parameterized by export rules.
wenzelm
parents:
diff changeset
   130
20296
753fad9f6e03 simplified export: no Seq.seq;
wenzelm
parents: 20222
diff changeset
   131
fun export is_goal inner outer =
71177
71467e35fc3c more structural integrity;
wenzelm
parents: 70735
diff changeset
   132
  Raw_Simplifier.norm_hhf_protect inner #>
30479
wenzelm
parents: 30471
diff changeset
   133
  fold_rev (fn (e, As) => #1 (e is_goal As)) (local_assumptions_of inner outer) #>
71177
71467e35fc3c more structural integrity;
wenzelm
parents: 70735
diff changeset
   134
  Raw_Simplifier.norm_hhf_protect outer;
20222
e2b876cd9e29 Local assumptions, parameterized by export rules.
wenzelm
parents:
diff changeset
   135
21679
06715e253686 export: added explicit term operation;
wenzelm
parents: 21605
diff changeset
   136
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
   137
  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
   138
21517
b165c9120702 added export_morphism;
wenzelm
parents: 20296
diff changeset
   139
fun export_morphism inner outer =
b165c9120702 added export_morphism;
wenzelm
parents: 20296
diff changeset
   140
  let
b165c9120702 added export_morphism;
wenzelm
parents: 20296
diff changeset
   141
    val thm = export false inner outer;
21679
06715e253686 export: added explicit term operation;
wenzelm
parents: 21605
diff changeset
   142
    val term = export_term inner outer;
21517
b165c9120702 added export_morphism;
wenzelm
parents: 20296
diff changeset
   143
    val typ = Logic.type_map term;
54740
91f54d386680 maintain morphism names for diagnostic purposes;
wenzelm
parents: 54567
diff changeset
   144
  in
70313
9c19e15c8548 more structural integrity;
wenzelm
parents: 67721
diff changeset
   145
    Morphism.transfer_morphism' inner $>
9c19e15c8548 more structural integrity;
wenzelm
parents: 67721
diff changeset
   146
    Morphism.transfer_morphism' outer $>
54740
91f54d386680 maintain morphism names for diagnostic purposes;
wenzelm
parents: 54567
diff changeset
   147
    Morphism.morphism "Assumption.export"
91f54d386680 maintain morphism names for diagnostic purposes;
wenzelm
parents: 54567
diff changeset
   148
      {binding = [], typ = [typ], term = [term], fact = [map thm]}
91f54d386680 maintain morphism names for diagnostic purposes;
wenzelm
parents: 54567
diff changeset
   149
  end;
21517
b165c9120702 added export_morphism;
wenzelm
parents: 20296
diff changeset
   150
20222
e2b876cd9e29 Local assumptions, parameterized by export rules.
wenzelm
parents:
diff changeset
   151
end;