author | kleing |
Fri, 27 May 2005 01:09:44 +0200 | |
changeset 16095 | f6af6b265d20 |
parent 16023 | 66561f6814bd |
child 16132 | afd2d32c7d94 |
permissions | -rw-r--r-- |
3987 | 1 |
(* Title: Pure/pure_thy.ML |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel, TU Muenchen |
|
4 |
||
5091 | 5 |
Theorem database, derived theory operations, and the ProtoPure theory. |
3987 | 6 |
*) |
7 |
||
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
8 |
signature BASIC_PURE_THY = |
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
9 |
sig |
15456
956d6acacf89
Specific theorems in a named list of theorems can now be referred to
berghofe
parents:
15387
diff
changeset
|
10 |
type thmref |
5000 | 11 |
val print_theorems: theory -> unit |
12 |
val print_theory: theory -> unit |
|
15456
956d6acacf89
Specific theorems in a named list of theorems can now be referred to
berghofe
parents:
15387
diff
changeset
|
13 |
val get_thm: theory -> thmref -> thm |
956d6acacf89
Specific theorems in a named list of theorems can now be referred to
berghofe
parents:
15387
diff
changeset
|
14 |
val get_thms: theory -> thmref -> thm list |
956d6acacf89
Specific theorems in a named list of theorems can now be referred to
berghofe
parents:
15387
diff
changeset
|
15 |
val get_thmss: theory -> thmref list -> thm list |
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
16 |
val thms_of: theory -> (string * thm) list |
5091 | 17 |
structure ProtoPure: |
18 |
sig |
|
19 |
val thy: theory |
|
20 |
val Goal_def: thm |
|
21 |
end |
|
4853 | 22 |
end; |
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
23 |
|
3987 | 24 |
signature PURE_THY = |
25 |
sig |
|
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
26 |
include BASIC_PURE_THY |
15703 | 27 |
datatype interval = FromTo of int * int | From of int | Single of int |
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
28 |
val string_of_thmref: thmref -> string |
15456
956d6acacf89
Specific theorems in a named list of theorems can now be referred to
berghofe
parents:
15387
diff
changeset
|
29 |
val get_thm_closure: theory -> thmref -> thm |
956d6acacf89
Specific theorems in a named list of theorems can now be referred to
berghofe
parents:
15387
diff
changeset
|
30 |
val get_thms_closure: theory -> thmref -> thm list |
9564 | 31 |
val single_thm: string -> thm list -> thm |
15456
956d6acacf89
Specific theorems in a named list of theorems can now be referred to
berghofe
parents:
15387
diff
changeset
|
32 |
val select_thm: thmref -> thm list -> thm list |
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
33 |
val selections: string * thm list -> (thmref * thm) list |
6367 | 34 |
val cond_extern_thm_sg: Sign.sg -> string -> xstring |
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
35 |
val fact_index_of: theory -> FactIndex.T |
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
36 |
val valid_thms: theory -> thmref * thm list -> bool |
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
37 |
val thms_containing: theory -> FactIndex.spec -> (string * thm list) list |
13646 | 38 |
val thms_containing_consts: theory -> string list -> (string * thm) list |
12695 | 39 |
val hide_thms: bool -> string list -> theory -> theory |
6091 | 40 |
val store_thm: (bstring * thm) * theory attribute list -> theory -> theory * thm |
7405 | 41 |
val smart_store_thms: (bstring * thm list) -> thm list |
12138
7cad58fbc866
renamed open_smart_store_thms to smart_store_thms_open;
wenzelm
parents:
12123
diff
changeset
|
42 |
val smart_store_thms_open: (bstring * thm list) -> thm list |
7899 | 43 |
val forall_elim_var: int -> thm -> thm |
44 |
val forall_elim_vars: int -> thm -> thm |
|
8419
4770b1a12a93
add_thms, add_axioms, add_defs: return theorems as well;
wenzelm
parents:
8039
diff
changeset
|
45 |
val add_thms: ((bstring * thm) * theory attribute list) list -> theory -> theory * thm list |
12711 | 46 |
val add_thmss: ((bstring * thm list) * theory attribute list) list -> theory |
47 |
-> theory * thm list list |
|
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15570
diff
changeset
|
48 |
val note_thmss: |
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15570
diff
changeset
|
49 |
theory attribute -> ((bstring * theory attribute list) * |
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15570
diff
changeset
|
50 |
(thmref * theory attribute list) list) list -> theory -> |
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15570
diff
changeset
|
51 |
theory * (bstring * thm list) list |
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15570
diff
changeset
|
52 |
val note_thmss_i: |
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15570
diff
changeset
|
53 |
theory attribute -> ((bstring * theory attribute list) * |
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15570
diff
changeset
|
54 |
(thm list * theory attribute list) list) list -> theory -> |
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15570
diff
changeset
|
55 |
theory * (bstring * thm list) list |
15696 | 56 |
val note_thmss_accesses: |
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15570
diff
changeset
|
57 |
(string -> string list) -> |
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15570
diff
changeset
|
58 |
theory attribute -> ((bstring * theory attribute list) * |
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15570
diff
changeset
|
59 |
(thmref * theory attribute list) list) list -> theory -> |
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15570
diff
changeset
|
60 |
theory * (bstring * thm list) list |
15696 | 61 |
val note_thmss_accesses_i: |
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15570
diff
changeset
|
62 |
(string -> string list) -> |
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15570
diff
changeset
|
63 |
theory attribute -> ((bstring * theory attribute list) * |
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15570
diff
changeset
|
64 |
(thm list * theory attribute list) list) list -> theory -> |
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15570
diff
changeset
|
65 |
theory * (bstring * thm list) list |
8419
4770b1a12a93
add_thms, add_axioms, add_defs: return theorems as well;
wenzelm
parents:
8039
diff
changeset
|
66 |
val add_axioms: ((bstring * string) * theory attribute list) list -> theory -> theory * thm list |
4770b1a12a93
add_thms, add_axioms, add_defs: return theorems as well;
wenzelm
parents:
8039
diff
changeset
|
67 |
val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory * thm list |
12711 | 68 |
val add_axiomss: ((bstring * string list) * theory attribute list) list -> theory |
69 |
-> theory * thm list list |
|
70 |
val add_axiomss_i: ((bstring * term list) * theory attribute list) list -> theory |
|
71 |
-> theory * thm list list |
|
9318 | 72 |
val add_defs: bool -> ((bstring * string) * theory attribute list) list |
73 |
-> theory -> theory * thm list |
|
74 |
val add_defs_i: bool -> ((bstring * term) * theory attribute list) list |
|
75 |
-> theory -> theory * thm list |
|
76 |
val add_defss: bool -> ((bstring * string list) * theory attribute list) list |
|
77 |
-> theory -> theory * thm list list |
|
78 |
val add_defss_i: bool -> ((bstring * term list) * theory attribute list) list |
|
79 |
-> theory -> theory * thm list list |
|
4963
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
80 |
val get_name: theory -> string |
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
81 |
val put_name: string -> theory -> theory |
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
82 |
val global_path: theory -> theory |
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
83 |
val local_path: theory -> theory |
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
84 |
val begin_theory: string -> theory list -> theory |
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
85 |
val end_theory: theory -> theory |
6682 | 86 |
val checkpoint: theory -> theory |
4922
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
87 |
val add_typedecls: (bstring * string list * mixfix) list -> theory -> theory |
3987 | 88 |
end; |
89 |
||
90 |
structure PureThy: PURE_THY = |
|
91 |
struct |
|
92 |
||
93 |
||
4922
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
94 |
(*** theorem database ***) |
3987 | 95 |
|
4922
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
96 |
(** data kind 'Pure/theorems' **) |
3987 | 97 |
|
5005 | 98 |
structure TheoremsDataArgs = |
99 |
struct |
|
100 |
val name = "Pure/theorems"; |
|
3987 | 101 |
|
5005 | 102 |
type T = |
103 |
{space: NameSpace.T, |
|
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
104 |
theorems: thm list Symtab.table, |
13274 | 105 |
index: FactIndex.T} ref; |
3987 | 106 |
|
4853 | 107 |
fun mk_empty _ = |
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
108 |
ref {space = NameSpace.empty, theorems = Symtab.empty, index = FactIndex.empty}: T; |
3987 | 109 |
|
5005 | 110 |
val empty = mk_empty (); |
6547 | 111 |
fun copy (ref x) = ref x; |
5005 | 112 |
val prep_ext = mk_empty; |
113 |
val merge = mk_empty; |
|
114 |
||
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
115 |
fun pretty sg (ref {space, theorems, index = _}) = |
4853 | 116 |
let |
10008 | 117 |
val prt_thm = Display.pretty_thm_sg sg; |
4853 | 118 |
fun prt_thms (name, [th]) = |
119 |
Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, prt_thm th] |
|
120 |
| prt_thms (name, ths) = Pretty.big_list (name ^ ":") (map prt_thm ths); |
|
3987 | 121 |
|
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
122 |
val thmss = NameSpace.cond_extern_table space theorems; |
9215 | 123 |
in Pretty.big_list "theorems:" (map prt_thms thmss) end; |
8720 | 124 |
|
9215 | 125 |
fun print sg data = Pretty.writeln (pretty sg data); |
3987 | 126 |
end; |
127 |
||
5005 | 128 |
structure TheoremsData = TheoryDataFun(TheoremsDataArgs); |
129 |
val get_theorems_sg = TheoremsData.get_sg; |
|
130 |
val get_theorems = TheoremsData.get; |
|
131 |
||
6367 | 132 |
val cond_extern_thm_sg = NameSpace.cond_extern o #space o ! o get_theorems_sg; |
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
133 |
val fact_index_of = #index o ! o get_theorems; |
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
134 |
|
6367 | 135 |
|
3987 | 136 |
|
5000 | 137 |
(* print theory *) |
3987 | 138 |
|
5005 | 139 |
val print_theorems = TheoremsData.print; |
8720 | 140 |
|
5000 | 141 |
fun print_theory thy = |
9215 | 142 |
Display.pretty_full_theory thy @ |
143 |
[TheoremsDataArgs.pretty (Theory.sign_of thy) (get_theorems thy)] |
|
8720 | 144 |
|> Pretty.chunks |> Pretty.writeln; |
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
145 |
|
3987 | 146 |
|
147 |
||
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
148 |
(** retrieve theorems **) |
3987 | 149 |
|
15531 | 150 |
fun the_thms _ (SOME thms) = thms |
151 |
| the_thms name NONE = error ("Unknown theorem(s) " ^ quote name); |
|
4037 | 152 |
|
9564 | 153 |
fun single_thm _ [thm] = thm |
154 |
| single_thm name _ = error ("Single theorem expected " ^ quote name); |
|
155 |
||
15703 | 156 |
|
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
157 |
(* datatype interval *) |
15703 | 158 |
|
159 |
datatype interval = |
|
160 |
FromTo of int * int | |
|
161 |
From of int | |
|
162 |
Single of int; |
|
163 |
||
164 |
fun interval _ (FromTo (i, j)) = i upto j |
|
165 |
| interval n (From i) = i upto n |
|
166 |
| interval _ (Single i) = [i]; |
|
167 |
||
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
168 |
fun string_of_interval (FromTo (i, j)) = string_of_int i ^ "-" ^ string_of_int j |
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
169 |
| string_of_interval (From i) = string_of_int i ^ "-" |
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
170 |
| string_of_interval (Single i) = string_of_int i; |
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
171 |
|
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
172 |
|
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
173 |
(* type thmref *) |
15703 | 174 |
|
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
175 |
type thmref = xstring * interval list option; |
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
176 |
|
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
177 |
fun string_of_thmref (name, NONE) = name |
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
178 |
| string_of_thmref (name, SOME is) = |
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
179 |
name ^ enclose "(" ")" (commas (map string_of_interval is)); |
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
180 |
|
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
181 |
|
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
182 |
(* select_thm *) |
15703 | 183 |
|
184 |
fun select_thm (_, NONE) thms = thms |
|
185 |
| select_thm (name, SOME is) thms = |
|
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
186 |
let |
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
187 |
val n = length thms; |
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
188 |
fun select i = |
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
189 |
if i < 1 orelse i > n then |
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
190 |
error ("Bad subscript " ^ string_of_int i ^ " for " ^ |
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
191 |
quote name ^ " (length " ^ string_of_int n ^ ")") |
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
192 |
else List.nth (thms, i - 1); |
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
193 |
in map select (List.concat (map (interval n) is)) end; |
15703 | 194 |
|
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
195 |
|
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
196 |
(* selections *) |
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
197 |
|
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
198 |
fun selections (name, [thm]) = [((name, NONE), thm)] |
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
199 |
| selections (name, thms) = (1 upto length thms, thms) |> ListPair.map (fn (i, thm) => |
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
200 |
((name, SOME [Single i]), thm)); |
15456
956d6acacf89
Specific theorems in a named list of theorems can now be referred to
berghofe
parents:
15387
diff
changeset
|
201 |
|
9564 | 202 |
|
9808 | 203 |
(* get_thm(s)_closure -- statically scoped versions *) |
9564 | 204 |
|
205 |
(*beware of proper order of evaluation!*) |
|
4922
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
206 |
|
9564 | 207 |
fun lookup_thms thy = |
208 |
let |
|
209 |
val sg_ref = Sign.self_ref (Theory.sign_of thy); |
|
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
210 |
val ref {space, theorems, ...} = get_theorems thy; |
9564 | 211 |
in |
212 |
fn name => |
|
15570 | 213 |
Option.map (map (Thm.transfer_sg (Sign.deref sg_ref))) (*semi-dynamic identity*) |
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
214 |
(Symtab.lookup (theorems, NameSpace.intern space name)) (*static content*) |
9564 | 215 |
end; |
3987 | 216 |
|
9564 | 217 |
fun get_thms_closure thy = |
218 |
let val closures = map lookup_thms (thy :: Theory.ancestors_of thy) |
|
15456
956d6acacf89
Specific theorems in a named list of theorems can now be referred to
berghofe
parents:
15387
diff
changeset
|
219 |
in fn namei as (name, _) => select_thm namei |
956d6acacf89
Specific theorems in a named list of theorems can now be referred to
berghofe
parents:
15387
diff
changeset
|
220 |
(the_thms name (get_first (fn f => f name) closures)) |
956d6acacf89
Specific theorems in a named list of theorems can now be referred to
berghofe
parents:
15387
diff
changeset
|
221 |
end; |
9564 | 222 |
|
9808 | 223 |
fun get_thm_closure thy = |
224 |
let val get = get_thms_closure thy |
|
15456
956d6acacf89
Specific theorems in a named list of theorems can now be referred to
berghofe
parents:
15387
diff
changeset
|
225 |
in fn namei as (name, _) => single_thm name (get namei) end; |
9808 | 226 |
|
9564 | 227 |
|
228 |
(* get_thm etc. *) |
|
229 |
||
15456
956d6acacf89
Specific theorems in a named list of theorems can now be referred to
berghofe
parents:
15387
diff
changeset
|
230 |
fun get_thms theory (namei as (name, _)) = |
9564 | 231 |
get_first (fn thy => lookup_thms thy name) (theory :: Theory.ancestors_of theory) |
15456
956d6acacf89
Specific theorems in a named list of theorems can now be referred to
berghofe
parents:
15387
diff
changeset
|
232 |
|> the_thms name |> select_thm namei |> map (Thm.transfer theory); |
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
233 |
|
15570 | 234 |
fun get_thmss thy names = List.concat (map (get_thms thy) names); |
15456
956d6acacf89
Specific theorems in a named list of theorems can now be referred to
berghofe
parents:
15387
diff
changeset
|
235 |
fun get_thm thy (namei as (name, _)) = single_thm name (get_thms thy namei); |
4783 | 236 |
|
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
237 |
|
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
238 |
(* thms_containing etc. *) |
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
239 |
|
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
240 |
fun valid_thms thy (thmref, ths) = |
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
241 |
(case try (transform_error (get_thms thy)) thmref of |
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
242 |
NONE => false |
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
243 |
| SOME ths' => Library.equal_lists Thm.eq_thm (ths, ths')); |
3987 | 244 |
|
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
245 |
fun thms_containing theory spec = |
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
246 |
(theory :: Theory.ancestors_of theory) |
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
247 |
|> map (fn thy => |
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
248 |
FactIndex.find (fact_index_of thy) spec |
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
249 |
|> List.filter (fn (name, ths) => valid_thms theory ((name, NONE), ths)) |
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
250 |
|> gen_distinct eq_fst) |
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
251 |
|> List.concat; |
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
252 |
|
13646 | 253 |
fun thms_containing_consts thy consts = |
15570 | 254 |
thms_containing thy (consts, []) |> map #2 |> List.concat |
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
255 |
|> map (fn th => (Thm.name_of_thm th, th)); |
13646 | 256 |
|
15882
a191d2bee3e1
new thms_containing that searches for patterns instead of constants
kleing
parents:
15801
diff
changeset
|
257 |
|
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
258 |
(* thms_of *) |
15882
a191d2bee3e1
new thms_containing that searches for patterns instead of constants
kleing
parents:
15801
diff
changeset
|
259 |
|
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
260 |
fun thms_of thy = |
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
261 |
let val ref {theorems, ...} = get_theorems thy in |
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
262 |
map (fn th => (Thm.name_of_thm th, th)) (List.concat (map snd (Symtab.dest theorems))) |
15882
a191d2bee3e1
new thms_containing that searches for patterns instead of constants
kleing
parents:
15801
diff
changeset
|
263 |
end; |
15703 | 264 |
|
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
265 |
|
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
266 |
|
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
267 |
(** store theorems **) (*DESTRUCTIVE*) |
3987 | 268 |
|
12695 | 269 |
(* hiding -- affects current theory node only! *) |
270 |
||
13424 | 271 |
fun hide_thms fully names thy = |
12695 | 272 |
let |
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
273 |
val r as ref {space, theorems, index} = get_theorems thy; |
13424 | 274 |
val space' = NameSpace.hide fully (space, names); |
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
275 |
in r := {space = space', theorems = theorems, index = index}; thy end; |
12695 | 276 |
|
277 |
||
4853 | 278 |
(* naming *) |
279 |
||
11998 | 280 |
fun gen_names j len name = |
281 |
map (fn i => name ^ "_" ^ string_of_int i) (j+1 upto j+len); |
|
4853 | 282 |
|
11998 | 283 |
fun name_multi name xs = gen_names 0 (length xs) name ~~ xs; |
12235
5fa04fc9b254
Further restructuring of theorem naming functions.
berghofe
parents:
12138
diff
changeset
|
284 |
|
12872
0855c3ab2047
Theorems are only "pre-named" if the do not already have names.
berghofe
parents:
12711
diff
changeset
|
285 |
fun name_thm pre (p as (_, thm)) = |
0855c3ab2047
Theorems are only "pre-named" if the do not already have names.
berghofe
parents:
12711
diff
changeset
|
286 |
if Thm.name_of_thm thm <> "" andalso pre then thm else Thm.name_thm p; |
0855c3ab2047
Theorems are only "pre-named" if the do not already have names.
berghofe
parents:
12711
diff
changeset
|
287 |
|
0855c3ab2047
Theorems are only "pre-named" if the do not already have names.
berghofe
parents:
12711
diff
changeset
|
288 |
fun name_thms pre name [x] = [name_thm pre (name, x)] |
0855c3ab2047
Theorems are only "pre-named" if the do not already have names.
berghofe
parents:
12711
diff
changeset
|
289 |
| name_thms pre name xs = map (name_thm pre) (name_multi name xs); |
12235
5fa04fc9b254
Further restructuring of theorem naming functions.
berghofe
parents:
12138
diff
changeset
|
290 |
|
5fa04fc9b254
Further restructuring of theorem naming functions.
berghofe
parents:
12138
diff
changeset
|
291 |
fun name_thmss name xs = (case filter_out (null o fst) xs of |
12872
0855c3ab2047
Theorems are only "pre-named" if the do not already have names.
berghofe
parents:
12711
diff
changeset
|
292 |
[([x], z)] => [([name_thm true (name, x)], z)] |
12235
5fa04fc9b254
Further restructuring of theorem naming functions.
berghofe
parents:
12138
diff
changeset
|
293 |
| _ => snd (foldl_map (fn (i, (ys, z)) => (i + length ys, |
12872
0855c3ab2047
Theorems are only "pre-named" if the do not already have names.
berghofe
parents:
12711
diff
changeset
|
294 |
(map (name_thm true) (gen_names i (length ys) name ~~ ys), z))) (0, xs))); |
4853 | 295 |
|
296 |
||
11998 | 297 |
(* enter_thms *) |
4853 | 298 |
|
7470
9f67ca1e03dc
eliminated default_name (thms no longer stored for name "");
wenzelm
parents:
7405
diff
changeset
|
299 |
fun warn_overwrite name = warning ("Replaced old copy of theorems " ^ quote name); |
9f67ca1e03dc
eliminated default_name (thms no longer stored for name "");
wenzelm
parents:
7405
diff
changeset
|
300 |
fun warn_same name = warning ("Theorem database already contains a copy of " ^ quote name); |
3987 | 301 |
|
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15570
diff
changeset
|
302 |
fun gen_enter_thms _ _ _ _ _ app_att thy ("", thms) = app_att (thy, thms) |
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15570
diff
changeset
|
303 |
| gen_enter_thms full acc sg pre_name post_name app_att thy (bname, thms) = |
7470
9f67ca1e03dc
eliminated default_name (thms no longer stored for name "");
wenzelm
parents:
7405
diff
changeset
|
304 |
let |
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15570
diff
changeset
|
305 |
val name = full sg bname; |
11998 | 306 |
val (thy', thms') = app_att (thy, pre_name name thms); |
307 |
val named_thms = post_name name thms'; |
|
3987 | 308 |
|
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
309 |
val r as ref {space, theorems, index} = get_theorems_sg sg; |
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15570
diff
changeset
|
310 |
val space' = NameSpace.extend' acc (space, [name]); |
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
311 |
val theorems' = Symtab.update ((name, named_thms), theorems); |
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
312 |
val index' = FactIndex.add (K false) (name, named_thms) index; |
13274 | 313 |
in |
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
314 |
(case Symtab.lookup (theorems, name) of |
15531 | 315 |
NONE => () |
316 |
| SOME thms' => |
|
13274 | 317 |
if Library.equal_lists Thm.eq_thm (thms', named_thms) then warn_same name |
318 |
else warn_overwrite name); |
|
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
319 |
r := {space = space', theorems = theorems', index = index'}; |
11998 | 320 |
(thy', named_thms) |
321 |
end; |
|
3987 | 322 |
|
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15570
diff
changeset
|
323 |
fun enter_thms sg = gen_enter_thms Sign.full_name NameSpace.accesses sg; |
4853 | 324 |
|
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
325 |
|
6091 | 326 |
(* add_thms(s) *) |
4853 | 327 |
|
12235
5fa04fc9b254
Further restructuring of theorem naming functions.
berghofe
parents:
12138
diff
changeset
|
328 |
fun add_thms_atts pre_name ((bname, thms), atts) thy = |
12872
0855c3ab2047
Theorems are only "pre-named" if the do not already have names.
berghofe
parents:
12711
diff
changeset
|
329 |
enter_thms (Theory.sign_of thy) pre_name (name_thms false) |
11998 | 330 |
(Thm.applys_attributes o rpair atts) thy (bname, thms); |
4853 | 331 |
|
12235
5fa04fc9b254
Further restructuring of theorem naming functions.
berghofe
parents:
12138
diff
changeset
|
332 |
fun gen_add_thmss pre_name args theory = |
5fa04fc9b254
Further restructuring of theorem naming functions.
berghofe
parents:
12138
diff
changeset
|
333 |
foldl_map (fn (thy, arg) => add_thms_atts pre_name arg thy) (theory, args); |
5907 | 334 |
|
12235
5fa04fc9b254
Further restructuring of theorem naming functions.
berghofe
parents:
12138
diff
changeset
|
335 |
fun gen_add_thms pre_name args = |
5fa04fc9b254
Further restructuring of theorem naming functions.
berghofe
parents:
12138
diff
changeset
|
336 |
apsnd (map hd) o gen_add_thmss pre_name (map (apfst (apsnd single)) args); |
5fa04fc9b254
Further restructuring of theorem naming functions.
berghofe
parents:
12138
diff
changeset
|
337 |
|
12872
0855c3ab2047
Theorems are only "pre-named" if the do not already have names.
berghofe
parents:
12711
diff
changeset
|
338 |
val add_thmss = gen_add_thmss (name_thms true); |
0855c3ab2047
Theorems are only "pre-named" if the do not already have names.
berghofe
parents:
12711
diff
changeset
|
339 |
val add_thms = gen_add_thms (name_thms true); |
5907 | 340 |
|
341 |
||
14564 | 342 |
(* note_thmss(_i) *) |
5907 | 343 |
|
9192 | 344 |
local |
12711 | 345 |
|
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15570
diff
changeset
|
346 |
fun gen_note_thss enter get kind_att (thy, ((bname, more_atts), ths_atts)) = |
12711 | 347 |
let |
348 |
fun app (x, (ths, atts)) = Thm.applys_attributes ((x, ths), atts); |
|
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15570
diff
changeset
|
349 |
val (thy', thms) = enter (Theory.sign_of thy) |
15570 | 350 |
name_thmss (name_thms false) (apsnd List.concat o foldl_map app) thy |
12711 | 351 |
(bname, map (fn (ths, atts) => (get thy ths, atts @ more_atts @ [kind_att])) ths_atts); |
352 |
in (thy', (bname, thms)) end; |
|
353 |
||
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15570
diff
changeset
|
354 |
fun gen_note_thmss enter get kind_att args thy = |
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15570
diff
changeset
|
355 |
foldl_map (gen_note_thss enter get kind_att) (thy, args); |
12711 | 356 |
|
9192 | 357 |
in |
12711 | 358 |
|
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
359 |
(*if path is set, only permit unqualified names*) |
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15570
diff
changeset
|
360 |
val note_thmss = gen_note_thmss enter_thms get_thms; |
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15570
diff
changeset
|
361 |
val note_thmss_i = gen_note_thmss enter_thms (K I); |
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15570
diff
changeset
|
362 |
|
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
363 |
(*always permit qualified names, clients may specify non-standard access policy*) |
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
364 |
fun note_thmss_accesses acc = gen_note_thmss (gen_enter_thms Sign.full_name' acc) get_thms; |
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
365 |
fun note_thmss_accesses_i acc = gen_note_thmss (gen_enter_thms Sign.full_name' acc) (K I); |
12711 | 366 |
|
9192 | 367 |
end; |
5280 | 368 |
|
369 |
||
6091 | 370 |
(* store_thm *) |
5280 | 371 |
|
11998 | 372 |
fun store_thm ((bname, thm), atts) thy = |
12872
0855c3ab2047
Theorems are only "pre-named" if the do not already have names.
berghofe
parents:
12711
diff
changeset
|
373 |
let val (thy', [th']) = add_thms_atts (name_thms true) ((bname, [thm]), atts) thy |
5280 | 374 |
in (thy', th') end; |
3987 | 375 |
|
376 |
||
7405 | 377 |
(* smart_store_thms *) |
3987 | 378 |
|
12235
5fa04fc9b254
Further restructuring of theorem naming functions.
berghofe
parents:
12138
diff
changeset
|
379 |
fun gen_smart_store_thms _ (name, []) = |
11516
a0633bdcd015
Added equality axioms and initialization of proof term package.
berghofe
parents:
10667
diff
changeset
|
380 |
error ("Cannot store empty list of theorems: " ^ quote name) |
12235
5fa04fc9b254
Further restructuring of theorem naming functions.
berghofe
parents:
12138
diff
changeset
|
381 |
| gen_smart_store_thms name_thm (name, [thm]) = |
12872
0855c3ab2047
Theorems are only "pre-named" if the do not already have names.
berghofe
parents:
12711
diff
changeset
|
382 |
snd (enter_thms (Thm.sign_of_thm thm) (name_thm true) (name_thm false) |
0855c3ab2047
Theorems are only "pre-named" if the do not already have names.
berghofe
parents:
12711
diff
changeset
|
383 |
I () (name, [thm])) |
12235
5fa04fc9b254
Further restructuring of theorem naming functions.
berghofe
parents:
12138
diff
changeset
|
384 |
| gen_smart_store_thms name_thm (name, thms) = |
7405 | 385 |
let |
386 |
val merge_sg = Sign.merge_refs o apsnd (Sign.self_ref o Thm.sign_of_thm); |
|
15570 | 387 |
val sg_ref = Library.foldl merge_sg (Sign.self_ref (Thm.sign_of_thm (hd thms)), tl thms); |
12872
0855c3ab2047
Theorems are only "pre-named" if the do not already have names.
berghofe
parents:
12711
diff
changeset
|
388 |
in snd (enter_thms (Sign.deref sg_ref) (name_thm true) (name_thm false) |
0855c3ab2047
Theorems are only "pre-named" if the do not already have names.
berghofe
parents:
12711
diff
changeset
|
389 |
I () (name, thms)) |
0855c3ab2047
Theorems are only "pre-named" if the do not already have names.
berghofe
parents:
12711
diff
changeset
|
390 |
end; |
11516
a0633bdcd015
Added equality axioms and initialization of proof term package.
berghofe
parents:
10667
diff
changeset
|
391 |
|
12235
5fa04fc9b254
Further restructuring of theorem naming functions.
berghofe
parents:
12138
diff
changeset
|
392 |
val smart_store_thms = gen_smart_store_thms name_thms; |
12872
0855c3ab2047
Theorems are only "pre-named" if the do not already have names.
berghofe
parents:
12711
diff
changeset
|
393 |
val smart_store_thms_open = gen_smart_store_thms (K (K I)); |
3987 | 394 |
|
395 |
||
7899 | 396 |
(* forall_elim_vars (belongs to drule.ML) *) |
397 |
||
13713 | 398 |
(*Replace outermost quantified variable by Var of given index.*) |
7899 | 399 |
fun forall_elim_var i th = |
400 |
let val {prop,sign,...} = rep_thm th |
|
401 |
in case prop of |
|
13713 | 402 |
Const ("all", _) $ Abs (a, T, _) => |
403 |
let val used = map (fst o fst) |
|
15570 | 404 |
(List.filter (equal i o snd o fst) (Term.add_vars ([], prop))) |
13713 | 405 |
in forall_elim (cterm_of sign (Var ((variant used a, i), T))) th end |
406 |
| _ => raise THM ("forall_elim_var", i, [th]) |
|
7899 | 407 |
end; |
408 |
||
409 |
(*Repeat forall_elim_var until all outer quantifiers are removed*) |
|
410 |
fun forall_elim_vars i th = |
|
411 |
forall_elim_vars i (forall_elim_var i th) |
|
412 |
handle THM _ => th; |
|
413 |
||
414 |
||
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
415 |
(* store axioms as theorems *) |
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
416 |
|
4853 | 417 |
local |
7899 | 418 |
fun get_axs thy named_axs = |
419 |
map (forall_elim_vars 0 o Thm.get_axiom thy o fst) named_axs; |
|
7753 | 420 |
|
8419
4770b1a12a93
add_thms, add_axioms, add_defs: return theorems as well;
wenzelm
parents:
8039
diff
changeset
|
421 |
fun add_single add (thy, ((name, ax), atts)) = |
4853 | 422 |
let |
11998 | 423 |
val named_ax = [(name, ax)]; |
7753 | 424 |
val thy' = add named_ax thy; |
425 |
val thm = hd (get_axs thy' named_ax); |
|
12235
5fa04fc9b254
Further restructuring of theorem naming functions.
berghofe
parents:
12138
diff
changeset
|
426 |
in apsnd hd (gen_add_thms (K I) [((name, thm), atts)] thy') end; |
7753 | 427 |
|
8419
4770b1a12a93
add_thms, add_axioms, add_defs: return theorems as well;
wenzelm
parents:
8039
diff
changeset
|
428 |
fun add_multi add (thy, ((name, axs), atts)) = |
7753 | 429 |
let |
430 |
val named_axs = name_multi name axs; |
|
4853 | 431 |
val thy' = add named_axs thy; |
7753 | 432 |
val thms = get_axs thy' named_axs; |
12235
5fa04fc9b254
Further restructuring of theorem naming functions.
berghofe
parents:
12138
diff
changeset
|
433 |
in apsnd hd (gen_add_thmss (K I) [((name, thms), atts)] thy') end; |
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
434 |
|
8419
4770b1a12a93
add_thms, add_axioms, add_defs: return theorems as well;
wenzelm
parents:
8039
diff
changeset
|
435 |
fun add_singles add args thy = foldl_map (add_single add) (thy, args); |
4770b1a12a93
add_thms, add_axioms, add_defs: return theorems as well;
wenzelm
parents:
8039
diff
changeset
|
436 |
fun add_multis add args thy = foldl_map (add_multi add) (thy, args); |
4853 | 437 |
in |
7753 | 438 |
val add_axioms = add_singles Theory.add_axioms; |
439 |
val add_axioms_i = add_singles Theory.add_axioms_i; |
|
440 |
val add_axiomss = add_multis Theory.add_axioms; |
|
441 |
val add_axiomss_i = add_multis Theory.add_axioms_i; |
|
9318 | 442 |
val add_defs = add_singles o Theory.add_defs; |
443 |
val add_defs_i = add_singles o Theory.add_defs_i; |
|
444 |
val add_defss = add_multis o Theory.add_defs; |
|
445 |
val add_defss_i = add_multis o Theory.add_defs_i; |
|
4853 | 446 |
end; |
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
447 |
|
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
448 |
|
3987 | 449 |
|
4963
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
450 |
(*** derived theory operations ***) |
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
451 |
|
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
452 |
(** theory management **) |
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
453 |
|
5005 | 454 |
(* data kind 'Pure/theory_management' *) |
4963
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
455 |
|
5005 | 456 |
structure TheoryManagementDataArgs = |
457 |
struct |
|
458 |
val name = "Pure/theory_management"; |
|
6660 | 459 |
type T = {name: string, version: int}; |
5000 | 460 |
|
6660 | 461 |
val empty = {name = "", version = 0}; |
6547 | 462 |
val copy = I; |
5005 | 463 |
val prep_ext = I; |
5000 | 464 |
fun merge _ = empty; |
5005 | 465 |
fun print _ _ = (); |
4963
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
466 |
end; |
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
467 |
|
5005 | 468 |
structure TheoryManagementData = TheoryDataFun(TheoryManagementDataArgs); |
469 |
val get_info = TheoryManagementData.get; |
|
470 |
val put_info = TheoryManagementData.put; |
|
471 |
||
4963
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
472 |
|
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
473 |
(* get / put name *) |
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
474 |
|
5000 | 475 |
val get_name = #name o get_info; |
6660 | 476 |
fun put_name name = put_info {name = name, version = 0}; |
4963
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
477 |
|
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
478 |
|
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
479 |
(* control prefixing of theory name *) |
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
480 |
|
5210 | 481 |
val global_path = Theory.root_path; |
4963
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
482 |
|
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
483 |
fun local_path thy = |
5210 | 484 |
thy |> Theory.root_path |> Theory.add_path (get_name thy); |
4963
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
485 |
|
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
486 |
|
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
487 |
(* begin / end theory *) |
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
488 |
|
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
489 |
fun begin_theory name thys = |
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
490 |
Theory.prep_ext_merge thys |
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
491 |
|> put_name name |
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
492 |
|> local_path; |
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
493 |
|
12123 | 494 |
fun end_theory thy = |
495 |
thy |
|
496 |
|> Theory.add_name (get_name thy); |
|
4963
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
497 |
|
6682 | 498 |
fun checkpoint thy = |
499 |
if is_draft thy then |
|
500 |
let val {name, version} = get_info thy in |
|
501 |
thy |
|
502 |
|> Theory.add_name (name ^ ":" ^ string_of_int version) |
|
503 |
|> put_info {name = name, version = version + 1} |
|
504 |
end |
|
505 |
else thy; |
|
5000 | 506 |
|
507 |
||
4963
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
508 |
|
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
509 |
(** add logical types **) |
4922
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
510 |
|
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
511 |
fun add_typedecls decls thy = |
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
512 |
let |
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
513 |
val full = Sign.full_name (Theory.sign_of thy); |
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
514 |
|
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
515 |
fun type_of (raw_name, vs, mx) = |
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
516 |
if null (duplicates vs) then (raw_name, length vs, mx) |
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
517 |
else error ("Duplicate parameters in type declaration: " ^ quote raw_name); |
14854 | 518 |
in thy |> Theory.add_types (map type_of decls) end; |
4922
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
519 |
|
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
520 |
|
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
521 |
|
5091 | 522 |
(*** the ProtoPure theory ***) |
3987 | 523 |
|
524 |
val proto_pure = |
|
525 |
Theory.pre_pure |
|
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
526 |
|> TheoryManagementData.init |> put_name "ProtoPure" |
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
527 |
|> TheoremsData.init |
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
528 |
|> Proofterm.init |
4963
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
529 |
|> global_path |
3987 | 530 |
|> Theory.add_types |
4922
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
531 |
[("fun", 2, NoSyn), |
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
532 |
("prop", 0, NoSyn), |
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
533 |
("itself", 1, NoSyn), |
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
534 |
("dummy", 0, NoSyn)] |
03b81b6e1baa
added thms_closure: theory -> xstring -> tthm list option;
wenzelm
parents:
4853
diff
changeset
|
535 |
|> Theory.add_nonterminals Syntax.pure_nonterms |
3987 | 536 |
|> Theory.add_syntax Syntax.pure_syntax |
15801 | 537 |
|> Theory.add_syntax Syntax.pure_appl_syntax |
6692 | 538 |
|> Theory.add_modesyntax (Symbol.xsymbolsN, true) Syntax.pure_xsym_syntax |
3987 | 539 |
|> Theory.add_syntax |
7949 | 540 |
[("==>", "[prop, prop] => prop", Delimfix "op ==>"), |
9534 | 541 |
(Term.dummy_patternN, "aprop", Delimfix "'_")] |
3987 | 542 |
|> Theory.add_consts |
14854 | 543 |
[("==", "['a, 'a] => prop", InfixrName ("==", 2)), |
3987 | 544 |
("==>", "[prop, prop] => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)), |
545 |
("all", "('a => prop) => prop", Binder ("!!", 0, 0)), |
|
10667 | 546 |
("Goal", "prop => prop", NoSyn), |
6547 | 547 |
("TYPE", "'a itself", NoSyn), |
9534 | 548 |
(Term.dummy_patternN, "'a", Delimfix "'_")] |
14223
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
13800
diff
changeset
|
549 |
|> Theory.add_finals_i false |
14854 | 550 |
[Const("==", [TFree ("'a", []), TFree ("'a", [])] ---> propT), |
551 |
Const("==>", [propT, propT] ---> propT), |
|
552 |
Const("all", (TFree("'a", []) --> propT) --> propT), |
|
553 |
Const("TYPE", a_itselfT)] |
|
5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
5026
diff
changeset
|
554 |
|> Theory.add_modesyntax ("", false) |
12138
7cad58fbc866
renamed open_smart_store_thms to smart_store_thms_open;
wenzelm
parents:
12123
diff
changeset
|
555 |
(Syntax.pure_syntax_output @ Syntax.pure_appl_syntax) |
12250 | 556 |
|> Theory.add_trfuns Syntax.pure_trfuns |
557 |
|> Theory.add_trfunsT Syntax.pure_trfunsT |
|
4963
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
558 |
|> local_path |
10667 | 559 |
|> (#1 oo (add_defs_i false o map Thm.no_attributes)) |
560 |
[("Goal_def", let val A = Free ("A", propT) in Logic.mk_equals (Logic.mk_goal A, A) end)] |
|
9238 | 561 |
|> (#1 o add_thmss [(("nothing", []), [])]) |
11516
a0633bdcd015
Added equality axioms and initialization of proof term package.
berghofe
parents:
10667
diff
changeset
|
562 |
|> Theory.add_axioms_i Proofterm.equality_axms |
4963
38aa2d56e28c
added get_name, put_name, global_path, local_path, begin_theory,
wenzelm
parents:
4933
diff
changeset
|
563 |
|> end_theory; |
3987 | 564 |
|
5091 | 565 |
structure ProtoPure = |
566 |
struct |
|
567 |
val thy = proto_pure; |
|
568 |
val Goal_def = get_axiom thy "Goal_def"; |
|
569 |
end; |
|
3987 | 570 |
|
571 |
end; |
|
572 |
||
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
573 |
structure BasicPureThy: BASIC_PURE_THY = PureThy; |
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
574 |
open BasicPureThy; |