src/Pure/global_theory.ML
author wenzelm
Sun, 22 Jul 2012 12:26:41 +0200
changeset 48423 0ccf143a2a69
parent 47337 bd24e466bef9
child 48992 0518bf89c777
permissions -rw-r--r--
maintain set of source digests, including relevant parts of session entry;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39507
diff changeset
     1
(*  Title:      Pure/global_theory.ML
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39507
diff changeset
     2
    Author:     Makarius
3987
22f5291012df Init 'theorems' data. The Pure theories.
wenzelm
parents:
diff changeset
     3
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39507
diff changeset
     4
Global theory content: stored facts.
3987
22f5291012df Init 'theorems' data. The Pure theories.
wenzelm
parents:
diff changeset
     5
*)
22f5291012df Init 'theorems' data. The Pure theories.
wenzelm
parents:
diff changeset
     6
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39507
diff changeset
     7
signature GLOBAL_THEORY =
3987
22f5291012df Init 'theorems' data. The Pure theories.
wenzelm
parents:
diff changeset
     8
sig
27198
79e9bf691aed removed old theorem database;
wenzelm
parents: 26959
diff changeset
     9
  val facts_of: theory -> Facts.T
26666
433b165b0a8c added intern_fact, check_fact, hide_fact;
wenzelm
parents: 26655
diff changeset
    10
  val intern_fact: theory -> xstring -> string
26693
90d0b86644ac renamed check_fact to defined_fact;
wenzelm
parents: 26683
diff changeset
    11
  val defined_fact: theory -> string -> bool
27198
79e9bf691aed removed old theorem database;
wenzelm
parents: 26959
diff changeset
    12
  val hide_fact: bool -> string -> theory -> theory
44304
7ee000ce5390 maintain recent future proofs at transaction boundaries;
wenzelm
parents: 42471
diff changeset
    13
  val begin_recent_proofs: theory -> theory
7ee000ce5390 maintain recent future proofs at transaction boundaries;
wenzelm
parents: 42471
diff changeset
    14
  val join_recent_proofs: theory -> unit
32105
da419b0c1c1d join_proofs: implicit exception;
wenzelm
parents: 32060
diff changeset
    15
  val join_proofs: theory -> unit
26683
849281658859 removed obsolete get_fact_silent;
wenzelm
parents: 26666
diff changeset
    16
  val get_fact: Context.generic -> theory -> Facts.ref -> thm list
26344
04dacc6809b6 simplified get_thm(s): back to plain name argument;
wenzelm
parents: 26336
diff changeset
    17
  val get_thms: theory -> xstring -> thm list
04dacc6809b6 simplified get_thm(s): back to plain name argument;
wenzelm
parents: 26336
diff changeset
    18
  val get_thm: theory -> xstring -> thm
16336
e3892698c57d thms_of no longer global;
wenzelm
parents: 16132
diff changeset
    19
  val all_thms_of: theory -> (string * thm) list
21580
ff8062cd41e9 added map/burrow_facts;
wenzelm
parents: 21567
diff changeset
    20
  val map_facts: ('a -> 'b) -> ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list
21567
c097a926ba78 added burrow_fact;
wenzelm
parents: 21524
diff changeset
    21
  val burrow_fact: ('a list -> 'b list) -> ('a list * 'c) list -> ('b list * 'c) list
21580
ff8062cd41e9 added map/burrow_facts;
wenzelm
parents: 21567
diff changeset
    22
  val burrow_facts: ('a list -> 'b list) ->
ff8062cd41e9 added map/burrow_facts;
wenzelm
parents: 21567
diff changeset
    23
    ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list
ff8062cd41e9 added map/burrow_facts;
wenzelm
parents: 21567
diff changeset
    24
  val name_multi: string -> 'a list -> (string * 'a) list
33700
768d14a67256 eliminated obsolete thm position tags;
wenzelm
parents: 33522
diff changeset
    25
  val name_thm: bool -> bool -> string -> thm -> thm
768d14a67256 eliminated obsolete thm position tags;
wenzelm
parents: 33522
diff changeset
    26
  val name_thms: bool -> bool -> string -> thm list -> thm list
768d14a67256 eliminated obsolete thm position tags;
wenzelm
parents: 33522
diff changeset
    27
  val name_thmss: bool -> string -> (thm list * 'a) list -> (thm list * 'a) list
29579
cb520b766e00 binding replaces bstring
haftmann
parents: 29433
diff changeset
    28
  val store_thms: binding * thm list -> theory -> thm list * theory
cb520b766e00 binding replaces bstring
haftmann
parents: 29433
diff changeset
    29
  val store_thm: binding * thm -> theory -> thm * theory
cb520b766e00 binding replaces bstring
haftmann
parents: 29433
diff changeset
    30
  val store_thm_open: binding * thm -> theory -> thm * theory
cb520b766e00 binding replaces bstring
haftmann
parents: 29433
diff changeset
    31
  val add_thms: ((binding * thm) * attribute list) list -> theory -> thm list * theory
cb520b766e00 binding replaces bstring
haftmann
parents: 29433
diff changeset
    32
  val add_thm: (binding * thm) * attribute list -> theory -> thm * theory
cb520b766e00 binding replaces bstring
haftmann
parents: 29433
diff changeset
    33
  val add_thmss: ((binding * thm list) * attribute list) list -> theory -> thm list list * theory
cb520b766e00 binding replaces bstring
haftmann
parents: 29433
diff changeset
    34
  val add_thms_dynamic: binding * (Context.generic -> thm list) -> theory -> theory
30853
6c6b7a72fa34 tuned signature;
wenzelm
parents: 30344
diff changeset
    35
  val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list
6c6b7a72fa34 tuned signature;
wenzelm
parents: 30344
diff changeset
    36
    -> theory -> (string * thm list) list * theory
29579
cb520b766e00 binding replaces bstring
haftmann
parents: 29433
diff changeset
    37
  val add_defs: bool -> ((binding * term) * attribute list) list ->
18377
0e1d025d57b3 oriented result pairs in PureThy
haftmann
parents: 18358
diff changeset
    38
    theory -> thm list * theory
29579
cb520b766e00 binding replaces bstring
haftmann
parents: 29433
diff changeset
    39
  val add_defs_unchecked: bool -> ((binding * term) * attribute list) list ->
cb520b766e00 binding replaces bstring
haftmann
parents: 29433
diff changeset
    40
    theory -> thm list * theory
30337
eb189f7e43a1 Theory.add_axioms/add_defs: replaced old bstring by binding;
wenzelm
parents: 30242
diff changeset
    41
  val add_defs_cmd: bool -> ((binding * string) * attribute list) list ->
18377
0e1d025d57b3 oriented result pairs in PureThy
haftmann
parents: 18358
diff changeset
    42
    theory -> thm list * theory
30337
eb189f7e43a1 Theory.add_axioms/add_defs: replaced old bstring by binding;
wenzelm
parents: 30242
diff changeset
    43
  val add_defs_unchecked_cmd: bool -> ((binding * string) * attribute list) list ->
19629
c107e7a79559 added add_defs_unchecked(_i);
wenzelm
parents: 19577
diff changeset
    44
    theory -> thm list * theory
3987
22f5291012df Init 'theorems' data. The Pure theories.
wenzelm
parents:
diff changeset
    45
end;
22f5291012df Init 'theorems' data. The Pure theories.
wenzelm
parents:
diff changeset
    46
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39507
diff changeset
    47
structure Global_Theory: GLOBAL_THEORY =
3987
22f5291012df Init 'theorems' data. The Pure theories.
wenzelm
parents:
diff changeset
    48
struct
22f5291012df Init 'theorems' data. The Pure theories.
wenzelm
parents:
diff changeset
    49
27198
79e9bf691aed removed old theorem database;
wenzelm
parents: 26959
diff changeset
    50
(** theory data **)
26282
305d5ca4fa9d replaced obsolete FactIndex.T by Facts.T (cumulative version, assumes that facts are only added to unfinished theories);
wenzelm
parents: 26050
diff changeset
    51
47337
bd24e466bef9 tuned comments;
wenzelm
parents: 47007
diff changeset
    52
type proofs = thm list * unit lazy;  (*accumulated thms, persistent join*)
45643
9e49cfe7015d memoing of forked proofs;
wenzelm
parents: 44304
diff changeset
    53
9e49cfe7015d memoing of forked proofs;
wenzelm
parents: 44304
diff changeset
    54
val empty_proofs: proofs = ([], Lazy.value ());
9e49cfe7015d memoing of forked proofs;
wenzelm
parents: 44304
diff changeset
    55
9e49cfe7015d memoing of forked proofs;
wenzelm
parents: 44304
diff changeset
    56
fun add_proofs more_thms ((thms, _): proofs) =
9e49cfe7015d memoing of forked proofs;
wenzelm
parents: 44304
diff changeset
    57
  let val thms' = fold cons more_thms thms
9e49cfe7015d memoing of forked proofs;
wenzelm
parents: 44304
diff changeset
    58
  in (thms', Lazy.lazy (fn () => Thm.join_proofs (rev thms'))) end;
9e49cfe7015d memoing of forked proofs;
wenzelm
parents: 44304
diff changeset
    59
9e49cfe7015d memoing of forked proofs;
wenzelm
parents: 44304
diff changeset
    60
fun force_proofs ((_, prfs): proofs) = Lazy.force prfs;
9e49cfe7015d memoing of forked proofs;
wenzelm
parents: 44304
diff changeset
    61
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39507
diff changeset
    62
structure Data = Theory_Data
24713
8b3b6d09ef40 tuned functor application;
wenzelm
parents: 24434
diff changeset
    63
(
47337
bd24e466bef9 tuned comments;
wenzelm
parents: 47007
diff changeset
    64
  type T = Facts.T * (proofs * proofs);  (*facts, recent proofs, all proofs of theory node*)
45643
9e49cfe7015d memoing of forked proofs;
wenzelm
parents: 44304
diff changeset
    65
  val empty = (Facts.empty, (empty_proofs, empty_proofs));
9e49cfe7015d memoing of forked proofs;
wenzelm
parents: 44304
diff changeset
    66
  fun extend (facts, _) = (facts, snd empty);
9e49cfe7015d memoing of forked proofs;
wenzelm
parents: 44304
diff changeset
    67
  fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), snd empty);
24713
8b3b6d09ef40 tuned functor application;
wenzelm
parents: 24434
diff changeset
    68
);
3987
22f5291012df Init 'theorems' data. The Pure theories.
wenzelm
parents:
diff changeset
    69
28841
5556c7976837 added force_proofs (based on thms ever passed through enter_thms);
wenzelm
parents: 28674
diff changeset
    70
5556c7976837 added force_proofs (based on thms ever passed through enter_thms);
wenzelm
parents: 28674
diff changeset
    71
(* facts *)
5556c7976837 added force_proofs (based on thms ever passed through enter_thms);
wenzelm
parents: 28674
diff changeset
    72
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39507
diff changeset
    73
val facts_of = #1 o Data.get;
26666
433b165b0a8c added intern_fact, check_fact, hide_fact;
wenzelm
parents: 26655
diff changeset
    74
433b165b0a8c added intern_fact, check_fact, hide_fact;
wenzelm
parents: 26655
diff changeset
    75
val intern_fact = Facts.intern o facts_of;
26693
90d0b86644ac renamed check_fact to defined_fact;
wenzelm
parents: 26683
diff changeset
    76
val defined_fact = Facts.defined o facts_of;
16023
66561f6814bd added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents: 15975
diff changeset
    77
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39507
diff changeset
    78
fun hide_fact fully name = Data.map (apfst (Facts.hide fully name));
28841
5556c7976837 added force_proofs (based on thms ever passed through enter_thms);
wenzelm
parents: 28674
diff changeset
    79
5556c7976837 added force_proofs (based on thms ever passed through enter_thms);
wenzelm
parents: 28674
diff changeset
    80
45643
9e49cfe7015d memoing of forked proofs;
wenzelm
parents: 44304
diff changeset
    81
(* forked proofs *)
28841
5556c7976837 added force_proofs (based on thms ever passed through enter_thms);
wenzelm
parents: 28674
diff changeset
    82
46775
6287653e63ec canonical argument order for attribute application;
wenzelm
parents: 45666
diff changeset
    83
fun register_proofs thms thy = (thms, Data.map (apsnd (pairself (add_proofs thms))) thy);
28977
08990d02211f renamed type Lazy.T to lazy;
wenzelm
parents: 28941
diff changeset
    84
45643
9e49cfe7015d memoing of forked proofs;
wenzelm
parents: 44304
diff changeset
    85
val begin_recent_proofs = Data.map (apsnd (apfst (K empty_proofs)));
9e49cfe7015d memoing of forked proofs;
wenzelm
parents: 44304
diff changeset
    86
val join_recent_proofs = force_proofs o #1 o #2 o Data.get;
9e49cfe7015d memoing of forked proofs;
wenzelm
parents: 44304
diff changeset
    87
val join_proofs = force_proofs o #2 o #2 o Data.get;
6367
7f36b6fd3eb3 added cond_extern_thm_sg;
wenzelm
parents: 6350
diff changeset
    88
3987
22f5291012df Init 'theorems' data. The Pure theories.
wenzelm
parents:
diff changeset
    89
4022
0770a19c48d3 added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents: 4013
diff changeset
    90
(** retrieve theorems **)
3987
22f5291012df Init 'theorems' data. The Pure theories.
wenzelm
parents:
diff changeset
    91
27198
79e9bf691aed removed old theorem database;
wenzelm
parents: 26959
diff changeset
    92
fun get_fact context thy xthmref =
26683
849281658859 removed obsolete get_fact_silent;
wenzelm
parents: 26666
diff changeset
    93
  let
42378
d9fe47d21b41 markup facts via name space;
wenzelm
parents: 42376
diff changeset
    94
    val facts = facts_of thy;
26683
849281658859 removed obsolete get_fact_silent;
wenzelm
parents: 26666
diff changeset
    95
    val xname = Facts.name_of_ref xthmref;
849281658859 removed obsolete get_fact_silent;
wenzelm
parents: 26666
diff changeset
    96
    val pos = Facts.pos_of_ref xthmref;
27198
79e9bf691aed removed old theorem database;
wenzelm
parents: 26959
diff changeset
    97
42471
593289343c7d hardwired mapping "_" -> "Pure.asm_rl" avoids legacy binding;
wenzelm
parents: 42381
diff changeset
    98
    val name =
593289343c7d hardwired mapping "_" -> "Pure.asm_rl" avoids legacy binding;
wenzelm
parents: 42381
diff changeset
    99
      (case intern_fact thy xname of
593289343c7d hardwired mapping "_" -> "Pure.asm_rl" avoids legacy binding;
wenzelm
parents: 42381
diff changeset
   100
        "_" => "Pure.asm_rl"
593289343c7d hardwired mapping "_" -> "Pure.asm_rl" avoids legacy binding;
wenzelm
parents: 42381
diff changeset
   101
      | name => name);
42378
d9fe47d21b41 markup facts via name space;
wenzelm
parents: 42376
diff changeset
   102
    val res = Facts.lookup context facts name;
27198
79e9bf691aed removed old theorem database;
wenzelm
parents: 26959
diff changeset
   103
    val _ = Theory.check_thy thy;
26683
849281658859 removed obsolete get_fact_silent;
wenzelm
parents: 26666
diff changeset
   104
  in
27198
79e9bf691aed removed old theorem database;
wenzelm
parents: 26959
diff changeset
   105
    (case res of
79e9bf691aed removed old theorem database;
wenzelm
parents: 26959
diff changeset
   106
      NONE => error ("Unknown fact " ^ quote name ^ Position.str_of pos)
27739
cd1df29db620 get_fact: report position;
wenzelm
parents: 27728
diff changeset
   107
    | SOME (static, ths) =>
47007
wenzelm
parents: 47005
diff changeset
   108
        (Context_Position.report_generic context pos (Name_Space.markup (Facts.space_of facts) name);
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45643
diff changeset
   109
         if static then ()
47007
wenzelm
parents: 47005
diff changeset
   110
         else Context_Position.report_generic context pos (Isabelle_Markup.dynamic_fact name);
27739
cd1df29db620 get_fact: report position;
wenzelm
parents: 27728
diff changeset
   111
         Facts.select xthmref (map (Thm.transfer thy) ths)))
26683
849281658859 removed obsolete get_fact_silent;
wenzelm
parents: 26666
diff changeset
   112
  end;
26344
04dacc6809b6 simplified get_thm(s): back to plain name argument;
wenzelm
parents: 26336
diff changeset
   113
26683
849281658859 removed obsolete get_fact_silent;
wenzelm
parents: 26666
diff changeset
   114
fun get_thms thy = get_fact (Context.Theory thy) thy o Facts.named;
26344
04dacc6809b6 simplified get_thm(s): back to plain name argument;
wenzelm
parents: 26336
diff changeset
   115
fun get_thm thy name = Facts.the_single name (get_thms thy name);
4783
ca29125de4af added get_tthm(s), store_tthms(s);
wenzelm
parents: 4590
diff changeset
   116
27198
79e9bf691aed removed old theorem database;
wenzelm
parents: 26959
diff changeset
   117
fun all_thms_of thy =
27865
27a8ad9612a3 moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
wenzelm
parents: 27739
diff changeset
   118
  Facts.fold_static (fn (_, ths) => append (map (`(Thm.get_name_hint)) ths)) (facts_of thy) [];
16336
e3892698c57d thms_of no longer global;
wenzelm
parents: 16132
diff changeset
   119
4022
0770a19c48d3 added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents: 4013
diff changeset
   120
0770a19c48d3 added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents: 4013
diff changeset
   121
26488
b497e3187ec7 eliminated destructive/critical theorem database;
wenzelm
parents: 26471
diff changeset
   122
(** store theorems **)
3987
22f5291012df Init 'theorems' data. The Pure theories.
wenzelm
parents:
diff changeset
   123
21580
ff8062cd41e9 added map/burrow_facts;
wenzelm
parents: 21567
diff changeset
   124
(* fact specifications *)
ff8062cd41e9 added map/burrow_facts;
wenzelm
parents: 21567
diff changeset
   125
ff8062cd41e9 added map/burrow_facts;
wenzelm
parents: 21567
diff changeset
   126
fun map_facts f = map (apsnd (map (apfst (map f))));
ff8062cd41e9 added map/burrow_facts;
wenzelm
parents: 21567
diff changeset
   127
fun burrow_fact f = split_list #>> burrow f #> op ~~;
ff8062cd41e9 added map/burrow_facts;
wenzelm
parents: 21567
diff changeset
   128
fun burrow_facts f = split_list ##> burrow (burrow_fact f) #> op ~~;
ff8062cd41e9 added map/burrow_facts;
wenzelm
parents: 21567
diff changeset
   129
ff8062cd41e9 added map/burrow_facts;
wenzelm
parents: 21567
diff changeset
   130
4853
67bcbb03c235 tuned names of (add_)store_XXX functions;
wenzelm
parents: 4792
diff changeset
   131
(* naming *)
67bcbb03c235 tuned names of (add_)store_XXX functions;
wenzelm
parents: 4792
diff changeset
   132
18801
b913ce69660c moved theorem tags from Drule to PureThy;
wenzelm
parents: 18778
diff changeset
   133
fun name_multi name [x] = [(name, x)]
26457
wenzelm
parents: 26436
diff changeset
   134
  | name_multi "" xs = map (pair "") xs
wenzelm
parents: 26436
diff changeset
   135
  | name_multi name xs = map_index (fn (i, x) => (name ^ "_" ^ string_of_int (i + 1), x)) xs;
12235
5fa04fc9b254 Further restructuring of theorem naming functions.
berghofe
parents: 12138
diff changeset
   136
33700
768d14a67256 eliminated obsolete thm position tags;
wenzelm
parents: 33522
diff changeset
   137
fun name_thm pre official name thm = thm
41696
f69bb9077b02 tuned odd conditional expression;
wenzelm
parents: 39557
diff changeset
   138
  |> (if not official orelse pre andalso Thm.derivation_name thm <> "" then I
f69bb9077b02 tuned odd conditional expression;
wenzelm
parents: 39557
diff changeset
   139
      else Thm.name_derivation name)
f69bb9077b02 tuned odd conditional expression;
wenzelm
parents: 39557
diff changeset
   140
  |> (if name = "" orelse pre andalso Thm.has_name_hint thm then I
f69bb9077b02 tuned odd conditional expression;
wenzelm
parents: 39557
diff changeset
   141
      else Thm.put_name_hint name);
12872
0855c3ab2047 Theorems are only "pre-named" if the do not already have names.
berghofe
parents: 12711
diff changeset
   142
33700
768d14a67256 eliminated obsolete thm position tags;
wenzelm
parents: 33522
diff changeset
   143
fun name_thms pre official name xs =
768d14a67256 eliminated obsolete thm position tags;
wenzelm
parents: 33522
diff changeset
   144
  map (uncurry (name_thm pre official)) (name_multi name xs);
12235
5fa04fc9b254 Further restructuring of theorem naming functions.
berghofe
parents: 12138
diff changeset
   145
33700
768d14a67256 eliminated obsolete thm position tags;
wenzelm
parents: 33522
diff changeset
   146
fun name_thmss official name fact =
768d14a67256 eliminated obsolete thm position tags;
wenzelm
parents: 33522
diff changeset
   147
  burrow_fact (name_thms true official name) fact;
4853
67bcbb03c235 tuned names of (add_)store_XXX functions;
wenzelm
parents: 4792
diff changeset
   148
67bcbb03c235 tuned names of (add_)store_XXX functions;
wenzelm
parents: 4792
diff changeset
   149
11998
b14e7686ce84 - enter_thmx -> enter_thms
berghofe
parents: 11631
diff changeset
   150
(* enter_thms *)
4853
67bcbb03c235 tuned names of (add_)store_XXX functions;
wenzelm
parents: 4792
diff changeset
   151
28861
f53abb0733ee using name bindings
haftmann
parents: 28856
diff changeset
   152
fun enter_thms pre_name post_name app_att (b, thms) thy =
28965
1de908189869 cleaned up binding module and related code
haftmann
parents: 28941
diff changeset
   153
  if Binding.is_empty b
46775
6287653e63ec canonical argument order for attribute application;
wenzelm
parents: 45666
diff changeset
   154
  then app_att thms thy |-> register_proofs
30211
556d1810cdad Thm.binding;
wenzelm
parents: 30190
diff changeset
   155
  else
556d1810cdad Thm.binding;
wenzelm
parents: 30190
diff changeset
   156
    let
47005
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 46775
diff changeset
   157
      val name = Sign.full_name thy b;
46775
6287653e63ec canonical argument order for attribute application;
wenzelm
parents: 45666
diff changeset
   158
      val (thms', thy') = app_att (pre_name name thms) thy |>> post_name name |-> register_proofs;
30211
556d1810cdad Thm.binding;
wenzelm
parents: 30190
diff changeset
   159
      val thms'' = map (Thm.transfer thy') thms';
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 41696
diff changeset
   160
      val thy'' = thy'
47005
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 46775
diff changeset
   161
        |> (Data.map o apfst) (Facts.add_global (Context.Theory thy') (b, thms'') #> snd);
30211
556d1810cdad Thm.binding;
wenzelm
parents: 30190
diff changeset
   162
    in (thms'', thy'') end;
26488
b497e3187ec7 eliminated destructive/critical theorem database;
wenzelm
parents: 26471
diff changeset
   163
b497e3187ec7 eliminated destructive/critical theorem database;
wenzelm
parents: 26471
diff changeset
   164
b497e3187ec7 eliminated destructive/critical theorem database;
wenzelm
parents: 26471
diff changeset
   165
(* store_thm(s) *)
b497e3187ec7 eliminated destructive/critical theorem database;
wenzelm
parents: 26471
diff changeset
   166
33700
768d14a67256 eliminated obsolete thm position tags;
wenzelm
parents: 33522
diff changeset
   167
fun store_thms (b, thms) =
46775
6287653e63ec canonical argument order for attribute application;
wenzelm
parents: 45666
diff changeset
   168
  enter_thms (name_thms true true) (name_thms false true) pair (b, thms);
28076
b2374a203b1c name_thm etc.: pass position;
wenzelm
parents: 27865
diff changeset
   169
29579
cb520b766e00 binding replaces bstring
haftmann
parents: 29433
diff changeset
   170
fun store_thm (b, th) = store_thms (b, [th]) #>> the_single;
26488
b497e3187ec7 eliminated destructive/critical theorem database;
wenzelm
parents: 26471
diff changeset
   171
29579
cb520b766e00 binding replaces bstring
haftmann
parents: 29433
diff changeset
   172
fun store_thm_open (b, th) =
46775
6287653e63ec canonical argument order for attribute application;
wenzelm
parents: 45666
diff changeset
   173
  enter_thms (name_thms true false) (name_thms false false) pair (b, [th]) #>> the_single;
3987
22f5291012df Init 'theorems' data. The Pure theories.
wenzelm
parents:
diff changeset
   174
16023
66561f6814bd added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents: 15975
diff changeset
   175
6091
e3cdbd929a24 eliminated tthm type and Attribute structure;
wenzelm
parents: 6027
diff changeset
   176
(* add_thms(s) *)
4853
67bcbb03c235 tuned names of (add_)store_XXX functions;
wenzelm
parents: 4792
diff changeset
   177
29579
cb520b766e00 binding replaces bstring
haftmann
parents: 29433
diff changeset
   178
fun add_thms_atts pre_name ((b, thms), atts) =
46775
6287653e63ec canonical argument order for attribute application;
wenzelm
parents: 45666
diff changeset
   179
  enter_thms pre_name (name_thms false true) (fold_map (Thm.theory_attributes atts)) (b, thms);
4853
67bcbb03c235 tuned names of (add_)store_XXX functions;
wenzelm
parents: 4792
diff changeset
   180
18377
0e1d025d57b3 oriented result pairs in PureThy
haftmann
parents: 18358
diff changeset
   181
fun gen_add_thmss pre_name =
0e1d025d57b3 oriented result pairs in PureThy
haftmann
parents: 18358
diff changeset
   182
  fold_map (add_thms_atts pre_name);
5907
4b9f4e310891 added default_name;
wenzelm
parents: 5871
diff changeset
   183
12235
5fa04fc9b254 Further restructuring of theorem naming functions.
berghofe
parents: 12138
diff changeset
   184
fun gen_add_thms pre_name args =
18377
0e1d025d57b3 oriented result pairs in PureThy
haftmann
parents: 18358
diff changeset
   185
  apfst (map hd) o gen_add_thmss pre_name (map (apfst (apsnd single)) args);
12235
5fa04fc9b254 Further restructuring of theorem naming functions.
berghofe
parents: 12138
diff changeset
   186
33700
768d14a67256 eliminated obsolete thm position tags;
wenzelm
parents: 33522
diff changeset
   187
val add_thmss = gen_add_thmss (name_thms true true);
768d14a67256 eliminated obsolete thm position tags;
wenzelm
parents: 33522
diff changeset
   188
val add_thms = gen_add_thms (name_thms true true);
27683
add9a605d562 dropped PureThy.note; added PureThy.add_thm
haftmann
parents: 27198
diff changeset
   189
val add_thm = yield_singleton add_thms;
5907
4b9f4e310891 added default_name;
wenzelm
parents: 5871
diff changeset
   190
4b9f4e310891 added default_name;
wenzelm
parents: 5871
diff changeset
   191
26488
b497e3187ec7 eliminated destructive/critical theorem database;
wenzelm
parents: 26471
diff changeset
   192
(* add_thms_dynamic *)
b497e3187ec7 eliminated destructive/critical theorem database;
wenzelm
parents: 26471
diff changeset
   193
29579
cb520b766e00 binding replaces bstring
haftmann
parents: 29433
diff changeset
   194
fun add_thms_dynamic (b, f) thy = thy
47005
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 46775
diff changeset
   195
  |> (Data.map o apfst) (Facts.add_dynamic (Context.Theory thy) (b, f) #> snd);
26488
b497e3187ec7 eliminated destructive/critical theorem database;
wenzelm
parents: 26471
diff changeset
   196
b497e3187ec7 eliminated destructive/critical theorem database;
wenzelm
parents: 26471
diff changeset
   197
27728
9a9e54042800 removed obsolete note_thms_cmd;
wenzelm
parents: 27691
diff changeset
   198
(* note_thmss *)
5907
4b9f4e310891 added default_name;
wenzelm
parents: 5871
diff changeset
   199
46775
6287653e63ec canonical argument order for attribute application;
wenzelm
parents: 45666
diff changeset
   200
fun note_thmss kind = fold_map (fn ((b, more_atts), facts) => fn thy =>
12711
6a9412dd7d24 have_thmss vs. have_thmss_i;
wenzelm
parents: 12695
diff changeset
   201
  let
28965
1de908189869 cleaned up binding module and related code
haftmann
parents: 28941
diff changeset
   202
    val name = Sign.full_name thy b;
46775
6287653e63ec canonical argument order for attribute application;
wenzelm
parents: 45666
diff changeset
   203
    fun app (ths, atts) =
6287653e63ec canonical argument order for attribute application;
wenzelm
parents: 45666
diff changeset
   204
      fold_map (Thm.theory_attributes (surround (Thm.kind kind) (atts @ more_atts))) ths;
6287653e63ec canonical argument order for attribute application;
wenzelm
parents: 45666
diff changeset
   205
    val (thms, thy') =
6287653e63ec canonical argument order for attribute application;
wenzelm
parents: 45666
diff changeset
   206
      enter_thms (name_thmss true) (name_thms false true) (apfst flat oo fold_map app)
6287653e63ec canonical argument order for attribute application;
wenzelm
parents: 45666
diff changeset
   207
        (b, facts) thy;
28076
b2374a203b1c name_thm etc.: pass position;
wenzelm
parents: 27865
diff changeset
   208
  in ((name, thms), thy') end);
12711
6a9412dd7d24 have_thmss vs. have_thmss_i;
wenzelm
parents: 12695
diff changeset
   209
5280
6055775a151b added store_tthm;
wenzelm
parents: 5210
diff changeset
   210
4022
0770a19c48d3 added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents: 4013
diff changeset
   211
(* store axioms as theorems *)
0770a19c48d3 added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents: 4013
diff changeset
   212
4853
67bcbb03c235 tuned names of (add_)store_XXX functions;
wenzelm
parents: 4792
diff changeset
   213
local
35985
0bbf0d2348f9 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents: 35856
diff changeset
   214
0bbf0d2348f9 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents: 35856
diff changeset
   215
fun no_read _ (_, t) = t;
0bbf0d2348f9 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents: 35856
diff changeset
   216
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 41696
diff changeset
   217
fun read ctxt (b, str) =
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 41696
diff changeset
   218
  Syntax.read_prop ctxt str handle ERROR msg =>
42381
309ec68442c6 added Binding.print convenience, which includes quote already;
wenzelm
parents: 42379
diff changeset
   219
    cat_error msg ("The error(s) above occurred in definition " ^ Binding.print b);
35985
0bbf0d2348f9 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents: 35856
diff changeset
   220
0bbf0d2348f9 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents: 35856
diff changeset
   221
fun add prep unchecked overloaded = fold_map (fn ((b, raw_prop), atts) => fn thy =>
0bbf0d2348f9 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents: 35856
diff changeset
   222
  let
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 41696
diff changeset
   223
    val ctxt = Syntax.init_pretty_global thy;
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 41696
diff changeset
   224
    val prop = prep ctxt (b, raw_prop);
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 41696
diff changeset
   225
    val ((_, def), thy') = Thm.add_def ctxt unchecked overloaded (b, prop) thy;
35985
0bbf0d2348f9 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents: 35856
diff changeset
   226
    val thm = def
0bbf0d2348f9 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents: 35856
diff changeset
   227
      |> Thm.forall_intr_frees
0bbf0d2348f9 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents: 35856
diff changeset
   228
      |> Thm.forall_elim_vars 0
0bbf0d2348f9 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents: 35856
diff changeset
   229
      |> Thm.varifyT_global;
0bbf0d2348f9 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents: 35856
diff changeset
   230
  in yield_singleton (gen_add_thms (K I)) ((b, thm), atts) thy' end);
0bbf0d2348f9 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents: 35856
diff changeset
   231
4853
67bcbb03c235 tuned names of (add_)store_XXX functions;
wenzelm
parents: 4792
diff changeset
   232
in
35985
0bbf0d2348f9 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents: 35856
diff changeset
   233
0bbf0d2348f9 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents: 35856
diff changeset
   234
val add_defs = add no_read false;
0bbf0d2348f9 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents: 35856
diff changeset
   235
val add_defs_unchecked = add no_read true;
0bbf0d2348f9 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents: 35856
diff changeset
   236
val add_defs_cmd = add read false;
0bbf0d2348f9 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents: 35856
diff changeset
   237
val add_defs_unchecked_cmd = add read true;
0bbf0d2348f9 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents: 35856
diff changeset
   238
4853
67bcbb03c235 tuned names of (add_)store_XXX functions;
wenzelm
parents: 4792
diff changeset
   239
end;
4022
0770a19c48d3 added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents: 4013
diff changeset
   240
3987
22f5291012df Init 'theorems' data. The Pure theories.
wenzelm
parents:
diff changeset
   241
end;