author  wenzelm 
Thu, 27 Mar 2008 15:32:19 +0100  
changeset 26436  dfd6947ab5c2 
parent 26430  8ddb2e7c5a1e 
child 26457  9385d441cec6 
permissions  rwrr 
3987  1 
(* Title: Pure/pure_thy.ML 
2 
ID: $Id$ 

3 
Author: Markus Wenzel, TU Muenchen 

4 

26430  5 
Theorem storage. Pure theory syntax and logical content. 
3987  6 
*) 
7 

8 
signature PURE_THY = 

9 
sig 

23657  10 
val tag_rule: Markup.property > thm > thm 
18801  11 
val untag_rule: string > thm > thm 
23657  12 
val tag: Markup.property > attribute 
18801  13 
val untag: string > attribute 
21964  14 
val has_name_hint: thm > bool 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

15 
val get_name_hint: thm > string 
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

16 
val put_name_hint: string > thm > thm 
25981  17 
val get_group: thm > string option 
18 
val put_group: string > thm > thm 

19 
val group: string > attribute 

22251  20 
val has_kind: thm > bool 
18801  21 
val get_kind: thm > string 
22 
val kind_rule: string > thm > thm 

23 
val kind: string > attribute 

24 
val kind_internal: attribute 

23657  25 
val has_internal: Markup.property list > bool 
18801  26 
val is_internal: thm > bool 
26344
04dacc6809b6
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset

27 
val get_fact: theory > Facts.ref > thm list 
04dacc6809b6
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset

28 
val get_fact_silent: theory > Facts.ref > thm list 
04dacc6809b6
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset

29 
val get_thms: theory > xstring > thm list 
04dacc6809b6
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset

30 
val get_thm: theory > xstring > thm 
17162  31 
val theorems_of: theory > thm list NameSpace.table 
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

32 
val all_facts_of: theory > Facts.T 
16336  33 
val thms_of: theory > (string * thm) list 
34 
val all_thms_of: theory > (string * thm) list 

12695  35 
val hide_thms: bool > string list > theory > theory 
21580  36 
val map_facts: ('a > 'b) > ('c * ('a list * 'd) list) list > ('c * ('b list * 'd) list) list 
21567  37 
val burrow_fact: ('a list > 'b list) > ('a list * 'c) list > ('b list * 'c) list 
21580  38 
val burrow_facts: ('a list > 'b list) > 
39 
('c * ('a list * 'd) list) list > ('c * ('b list * 'd) list) list 

40 
val name_multi: string > 'a list > (string * 'a) list 

21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

41 
val name_thm: bool > bool > string > thm > thm 
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

42 
val name_thms: bool > bool > string > thm list > thm list 
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

43 
val name_thmss: bool > string > (thm list * 'a) list > (thm list * 'a) list 
18728  44 
val store_thm: (bstring * thm) * attribute list > theory > thm * theory 
7405  45 
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

46 
val smart_store_thms_open: (bstring * thm list) > thm list 
7899  47 
val forall_elim_var: int > thm > thm 
48 
val forall_elim_vars: int > thm > thm 

26393  49 
val add_thms_dynamic: bstring * (Context.generic > thm list) > theory > theory 
18728  50 
val add_thms: ((bstring * thm) * attribute list) list > theory > thm list * theory 
24965  51 
val add_thmss: ((bstring * thm list) * attribute list) list > theory > thm list list * theory 
25598  52 
val note: string > string * thm > theory > thm * theory 
18801  53 
val note_thmss: string > ((bstring * attribute list) * 
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26320
diff
changeset

54 
(Facts.ref * attribute list) list) list > theory > (bstring * thm list) list * theory 
18801  55 
val note_thmss_i: string > ((bstring * attribute list) * 
56 
(thm list * attribute list) list) list > theory > (bstring * thm list) list * theory 

25981  57 
val note_thmss_grouped: string > string > ((bstring * attribute list) * 
58 
(thm list * attribute list) list) list > theory > (bstring * thm list) list * theory 

18801  59 
val note_thmss_qualified: string > string > ((bstring * attribute list) * 
18728  60 
(thm list * attribute list) list) list > theory > (bstring * thm list) list * theory 
61 
val add_axioms: ((bstring * string) * attribute list) list > theory > thm list * theory 

62 
val add_axioms_i: ((bstring * term) * attribute list) list > theory > thm list * theory 

63 
val add_axiomss: ((bstring * string list) * attribute list) list > 

64 
theory > thm list list * theory 

65 
val add_axiomss_i: ((bstring * term list) * attribute list) list > 

66 
theory > thm list list * theory 

67 
val add_defs: bool > ((bstring * string) * attribute list) list > 

18377  68 
theory > thm list * theory 
18728  69 
val add_defs_i: bool > ((bstring * term) * attribute list) list > 
18377  70 
theory > thm list * theory 
19629  71 
val add_defs_unchecked: bool > ((bstring * string) * attribute list) list > 
72 
theory > thm list * theory 

73 
val add_defs_unchecked_i: bool > ((bstring * term) * attribute list) list > 

74 
theory > thm list * theory 

3987  75 
end; 
76 

77 
structure PureThy: PURE_THY = 

78 
struct 

79 

80 

18801  81 
(*** theorem tags ***) 
82 

83 
(* add / delete tags *) 

84 

21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

85 
fun tag_rule tg = Thm.map_tags (insert (op =) tg); 
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

86 
fun untag_rule s = Thm.map_tags (filter_out (fn (s', _) => s = s')); 
18801  87 

88 
fun tag tg x = Thm.rule_attribute (K (tag_rule tg)) x; 

89 
fun untag s x = Thm.rule_attribute (K (untag_rule s)) x; 

90 

91 

21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

92 
(* unofficial theorem names *) 
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

93 

23657  94 
fun the_name_hint thm = the (AList.lookup (op =) (Thm.get_tags thm) Markup.nameN); 
22251  95 

96 
val has_name_hint = can the_name_hint; 

97 
val get_name_hint = the_default "??.unknown" o try the_name_hint; 

21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

98 

23657  99 
fun put_name_hint name = untag_rule Markup.nameN #> tag_rule (Markup.nameN, name); 
21964  100 

21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

101 

25981  102 
(* theorem groups *) 
103 

104 
fun get_group thm = AList.lookup (op =) (Thm.get_tags thm) Markup.groupN; 

105 

106 
fun put_group name = 

107 
if name = "" then I else Thm.map_tags (AList.update (op =) (Markup.groupN, name)); 

108 

109 
fun group name = Thm.rule_attribute (K (put_group name)); 

110 

111 

18801  112 
(* theorem kinds *) 
113 

23657  114 
fun the_kind thm = the (AList.lookup (op =) (Thm.get_tags thm) Markup.kindN); 
22251  115 

116 
val has_kind = can the_kind; 

25981  117 
val get_kind = the_default "" o try the_kind; 
18801  118 

23657  119 
fun kind_rule k = tag_rule (Markup.kindN, k) o untag_rule Markup.kindN; 
18801  120 
fun kind k x = if k = "" then x else Thm.rule_attribute (K (kind_rule k)) x; 
22363  121 
fun kind_internal x = kind Thm.internalK x; 
23657  122 
fun has_internal tags = exists (fn tg => tg = (Markup.kindN, Thm.internalK)) tags; 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

123 
val is_internal = has_internal o Thm.get_tags; 
18801  124 

125 

126 

4922
03b81b6e1baa
added thms_closure: theory > xstring > tthm list option;
wenzelm
parents:
4853
diff
changeset

127 
(*** theorem database ***) 
3987  128 

16441  129 
(** dataype theorems **) 
3987  130 

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

131 
datatype thms = Thms of 
305d5ca4fa9d
replaced obsolete FactIndex.T by Facts.T (cumulative version, assumes that facts are only added to unfinished theories);
wenzelm
parents:
26050
diff
changeset

132 
{theorems: thm list NameSpace.table, (* FIXME legacy *) 
305d5ca4fa9d
replaced obsolete FactIndex.T by Facts.T (cumulative version, assumes that facts are only added to unfinished theories);
wenzelm
parents:
26050
diff
changeset

133 
all_facts: Facts.T}; 
305d5ca4fa9d
replaced obsolete FactIndex.T by Facts.T (cumulative version, assumes that facts are only added to unfinished theories);
wenzelm
parents:
26050
diff
changeset

134 

305d5ca4fa9d
replaced obsolete FactIndex.T by Facts.T (cumulative version, assumes that facts are only added to unfinished theories);
wenzelm
parents:
26050
diff
changeset

135 
fun make_thms theorems all_facts = Thms {theorems = theorems, all_facts = all_facts}; 
305d5ca4fa9d
replaced obsolete FactIndex.T by Facts.T (cumulative version, assumes that facts are only added to unfinished theories);
wenzelm
parents:
26050
diff
changeset

136 

16441  137 
structure TheoremsData = TheoryDataFun 
24713  138 
( 
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

139 
type T = thms ref; (* FIXME legacy *) 
305d5ca4fa9d
replaced obsolete FactIndex.T by Facts.T (cumulative version, assumes that facts are only added to unfinished theories);
wenzelm
parents:
26050
diff
changeset

140 
val empty = ref (make_thms NameSpace.empty_table Facts.empty); 
6547  141 
fun copy (ref x) = ref x; 
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

142 
fun extend (ref (Thms {theorems = _, all_facts})) = ref (make_thms NameSpace.empty_table all_facts); 
305d5ca4fa9d
replaced obsolete FactIndex.T by Facts.T (cumulative version, assumes that facts are only added to unfinished theories);
wenzelm
parents:
26050
diff
changeset

143 
fun merge _ 
305d5ca4fa9d
replaced obsolete FactIndex.T by Facts.T (cumulative version, assumes that facts are only added to unfinished theories);
wenzelm
parents:
26050
diff
changeset

144 
(ref (Thms {theorems = _, all_facts = all_facts1}), 
305d5ca4fa9d
replaced obsolete FactIndex.T by Facts.T (cumulative version, assumes that facts are only added to unfinished theories);
wenzelm
parents:
26050
diff
changeset

145 
ref (Thms {theorems = _, all_facts = all_facts2})) = 
305d5ca4fa9d
replaced obsolete FactIndex.T by Facts.T (cumulative version, assumes that facts are only added to unfinished theories);
wenzelm
parents:
26050
diff
changeset

146 
ref (make_thms NameSpace.empty_table (Facts.merge (all_facts1, all_facts2))); 
24713  147 
); 
3987  148 

26430  149 
val _ = Context.>> TheoremsData.init; 
150 

16493  151 
val get_theorems_ref = TheoremsData.get; 
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

152 
val get_theorems = (fn Thms args => args) o ! o get_theorems_ref; 
17162  153 
val theorems_of = #theorems o get_theorems; 
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

154 
val all_facts_of = #all_facts o get_theorems; 
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset

155 

6367  156 

3987  157 

4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset

158 
(** retrieve theorems **) 
3987  159 

26292
009e56d16080
get_thm(s): check facts lookup vs. old thm database;
wenzelm
parents:
26282
diff
changeset

160 
local 
009e56d16080
get_thm(s): check facts lookup vs. old thm database;
wenzelm
parents:
26282
diff
changeset

161 

009e56d16080
get_thm(s): check facts lookup vs. old thm database;
wenzelm
parents:
26282
diff
changeset

162 
fun lookup_thms thy xname = 
9564  163 
let 
16493  164 
val (space, thms) = #theorems (get_theorems thy); 
26292
009e56d16080
get_thm(s): check facts lookup vs. old thm database;
wenzelm
parents:
26282
diff
changeset

165 
val name = NameSpace.intern space xname; 
009e56d16080
get_thm(s): check facts lookup vs. old thm database;
wenzelm
parents:
26282
diff
changeset

166 
in Option.map (pair name) (Symtab.lookup thms name) end; 
009e56d16080
get_thm(s): check facts lookup vs. old thm database;
wenzelm
parents:
26282
diff
changeset

167 

009e56d16080
get_thm(s): check facts lookup vs. old thm database;
wenzelm
parents:
26282
diff
changeset

168 
fun lookup_fact thy xname = 
009e56d16080
get_thm(s): check facts lookup vs. old thm database;
wenzelm
parents:
26282
diff
changeset

169 
let 
009e56d16080
get_thm(s): check facts lookup vs. old thm database;
wenzelm
parents:
26282
diff
changeset

170 
val facts = all_facts_of thy; 
009e56d16080
get_thm(s): check facts lookup vs. old thm database;
wenzelm
parents:
26282
diff
changeset

171 
val name = NameSpace.intern (Facts.space_of facts) xname; 
26393  172 
in Option.map (pair name) (Facts.lookup (Context.Theory thy) facts name) end; 
26292
009e56d16080
get_thm(s): check facts lookup vs. old thm database;
wenzelm
parents:
26282
diff
changeset

173 

009e56d16080
get_thm(s): check facts lookup vs. old thm database;
wenzelm
parents:
26282
diff
changeset

174 
fun show_result NONE = "none" 
009e56d16080
get_thm(s): check facts lookup vs. old thm database;
wenzelm
parents:
26282
diff
changeset

175 
 show_result (SOME (name, _)) = quote name; 
009e56d16080
get_thm(s): check facts lookup vs. old thm database;
wenzelm
parents:
26282
diff
changeset

176 

26344
04dacc6809b6
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset

177 
fun get silent theory thmref = 
26292
009e56d16080
get_thm(s): check facts lookup vs. old thm database;
wenzelm
parents:
26282
diff
changeset

178 
let 
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26320
diff
changeset

179 
val name = Facts.name_of_ref thmref; 
26367
06635166d211
get_thms etc.: improved reporting of source position;
wenzelm
parents:
26361
diff
changeset

180 
val pos = Facts.pos_of_ref thmref; 
26292
009e56d16080
get_thm(s): check facts lookup vs. old thm database;
wenzelm
parents:
26282
diff
changeset

181 
val new_res = lookup_fact theory name; 
009e56d16080
get_thm(s): check facts lookup vs. old thm database;
wenzelm
parents:
26282
diff
changeset

182 
val old_res = get_first (fn thy => lookup_thms thy name) (theory :: Theory.ancestors_of theory); 
009e56d16080
get_thm(s): check facts lookup vs. old thm database;
wenzelm
parents:
26282
diff
changeset

183 
val is_same = 
009e56d16080
get_thm(s): check facts lookup vs. old thm database;
wenzelm
parents:
26282
diff
changeset

184 
(case (new_res, old_res) of 
009e56d16080
get_thm(s): check facts lookup vs. old thm database;
wenzelm
parents:
26282
diff
changeset

185 
(NONE, NONE) => true 
26395  186 
 (SOME (_, ths1), SOME (_, ths2)) => Thm.eq_thms (ths1, ths2) 
26292
009e56d16080
get_thm(s): check facts lookup vs. old thm database;
wenzelm
parents:
26282
diff
changeset

187 
 _ => false); 
009e56d16080
get_thm(s): check facts lookup vs. old thm database;
wenzelm
parents:
26282
diff
changeset

188 
val _ = 
26320  189 
if is_same orelse silent then () 
26292
009e56d16080
get_thm(s): check facts lookup vs. old thm database;
wenzelm
parents:
26282
diff
changeset

190 
else legacy_feature ("Fact lookup differs from oldstyle thm database:\n" ^ 
26367
06635166d211
get_thms etc.: improved reporting of source position;
wenzelm
parents:
26361
diff
changeset

191 
show_result new_res ^ " vs " ^ show_result old_res ^ Position.str_of pos); 
06635166d211
get_thms etc.: improved reporting of source position;
wenzelm
parents:
26361
diff
changeset

192 
in 
06635166d211
get_thms etc.: improved reporting of source position;
wenzelm
parents:
26361
diff
changeset

193 
(case old_res of 
06635166d211
get_thms etc.: improved reporting of source position;
wenzelm
parents:
26361
diff
changeset

194 
NONE => error ("Unknown theorem(s) " ^ quote name ^ Position.str_of pos) 
06635166d211
get_thms etc.: improved reporting of source position;
wenzelm
parents:
26361
diff
changeset

195 
 SOME (_, ths) => Facts.select thmref (map (Thm.transfer theory) ths)) 
06635166d211
get_thms etc.: improved reporting of source position;
wenzelm
parents:
26361
diff
changeset

196 
end; 
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset

197 

26320  198 
in 
199 

26344
04dacc6809b6
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset

200 
val get_fact_silent = get true; 
04dacc6809b6
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset

201 
val get_fact = get false; 
04dacc6809b6
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset

202 

26361  203 
fun get_thms thy = get_fact thy o Facts.named; 
26344
04dacc6809b6
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset

204 
fun get_thm thy name = Facts.the_single name (get_thms thy name); 
4783  205 

26292
009e56d16080
get_thm(s): check facts lookup vs. old thm database;
wenzelm
parents:
26282
diff
changeset

206 
end; 
009e56d16080
get_thm(s): check facts lookup vs. old thm database;
wenzelm
parents:
26282
diff
changeset

207 

4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset

208 

16336  209 
(* thms_of etc. *) 
15882
a191d2bee3e1
new thms_containing that searches for patterns instead of constants
kleing
parents:
15801
diff
changeset

210 

16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset

211 
fun thms_of thy = 
17162  212 
let val thms = #2 (theorems_of thy) 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

213 
in map (`(get_name_hint)) (maps snd (Symtab.dest thms)) end; 
15703  214 

19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19473
diff
changeset

215 
fun all_thms_of thy = maps thms_of (thy :: Theory.ancestors_of thy); 
16336  216 

4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset

217 

0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset

218 

0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset

219 
(** store theorems **) (*DESTRUCTIVE*) 
3987  220 

16441  221 
(* hiding  affects current theory node only *) 
12695  222 

23933  223 
fun hide_thms fully names thy = CRITICAL (fn () => 
12695  224 
let 
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

225 
val r as ref (Thms {theorems = (space, thms), all_facts}) = get_theorems_ref thy; 
16132  226 
val space' = fold (NameSpace.hide fully) names space; 
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

227 
in r := make_thms (space', thms) all_facts; thy end); 
12695  228 

229 

21580  230 
(* fact specifications *) 
231 

232 
fun map_facts f = map (apsnd (map (apfst (map f)))); 

233 
fun burrow_fact f = split_list #>> burrow f #> op ~~; 

234 
fun burrow_facts f = split_list ##> burrow (burrow_fact f) #> op ~~; 

235 

236 

4853  237 
(* naming *) 
238 

18614  239 
fun gen_names _ len "" = replicate len "" 
240 
 gen_names j len name = map (fn i => name ^ "_" ^ string_of_int i) (j + 1 upto j + len); 

4853  241 

18801  242 
fun name_multi name [x] = [(name, x)] 
243 
 name_multi name xs = gen_names 0 (length xs) name ~~ xs; 

12235
5fa04fc9b254
Further restructuring of theorem naming functions.
berghofe
parents:
12138
diff
changeset

244 

21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

245 
fun name_thm pre official name thm = thm 
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

246 
> (if Thm.get_name thm <> "" andalso pre orelse not official then I else Thm.put_name name) 
26050  247 
> (if has_name_hint thm andalso pre orelse name = "" then I else put_name_hint name) 
248 
> Thm.map_tags (Position.default_properties (Position.thread_data ())); 

12872
0855c3ab2047
Theorems are only "prenamed" if the do not already have names.
berghofe
parents:
12711
diff
changeset

249 

21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

250 
fun name_thms pre official name xs = 
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

251 
map (uncurry (name_thm pre official)) (name_multi name xs); 
12235
5fa04fc9b254
Further restructuring of theorem naming functions.
berghofe
parents:
12138
diff
changeset

252 

21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

253 
fun name_thmss official name fact = 
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

254 
burrow_fact (name_thms true official name) fact; 
4853  255 

256 

26393  257 
(* add_thms_dynamic *) 
258 

259 
fun add_thms_dynamic (bname, f) thy = CRITICAL (fn () => 

260 
let 

261 
val name = Sign.full_name thy bname; 

262 
val r as ref (Thms {theorems, all_facts}) = get_theorems_ref thy; 

263 
val all_facts' = Facts.add_dynamic (Sign.naming_of thy) (name, f) all_facts; 

264 
val _ = r := make_thms theorems all_facts'; 

265 
in thy end); 

266 

267 

11998  268 
(* enter_thms *) 
4853  269 

7470
9f67ca1e03dc
eliminated default_name (thms no longer stored for name "");
wenzelm
parents:
7405
diff
changeset

270 
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

271 
fun warn_same name = warning ("Theorem database already contains a copy of " ^ quote name); 
3987  272 

18418
bf448d999b7e
rearranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18377
diff
changeset

273 
fun enter_thms _ _ app_att ("", thms) thy = app_att (thy, thms) > swap 
23933  274 
 enter_thms pre_name post_name app_att (bname, thms) thy = CRITICAL (fn () => 
7470
9f67ca1e03dc
eliminated default_name (thms no longer stored for name "");
wenzelm
parents:
7405
diff
changeset

275 
let 
16441  276 
val name = Sign.full_name thy bname; 
277 
val (thy', thms') = apsnd (post_name name) (app_att (thy, pre_name name thms)); 

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

278 
val r as ref (Thms {theorems = (space, theorems), all_facts}) = get_theorems_ref thy'; 
16513
f38693aad717
enter_thms: use theorem database of thy *after* attribute application;
wenzelm
parents:
16493
diff
changeset

279 
val space' = Sign.declare_name thy' name space; 
17418  280 
val theorems' = Symtab.update (name, thms') theorems; 
26308  281 
val all_facts' = Facts.add_global (Sign.naming_of thy') (name, thms') all_facts; 
13274  282 
in 
17418  283 
(case Symtab.lookup theorems name of 
15531  284 
NONE => () 
16441  285 
 SOME thms'' => 
286 
if Thm.eq_thms (thms', thms'') then warn_same name 

13274  287 
else warn_overwrite name); 
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

288 
r := make_thms (space', theorems') all_facts'; 
18418
bf448d999b7e
rearranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18377
diff
changeset

289 
(thms', thy') 
23933  290 
end); 
3987  291 

16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset

292 

6091  293 
(* add_thms(s) *) 
4853  294 

16441  295 
fun add_thms_atts pre_name ((bname, thms), atts) = 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

296 
enter_thms pre_name (name_thms false true) 
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

297 
(foldl_map (Thm.theory_attributes atts)) (bname, thms); 
4853  298 

18377  299 
fun gen_add_thmss pre_name = 
300 
fold_map (add_thms_atts pre_name); 

5907  301 

12235
5fa04fc9b254
Further restructuring of theorem naming functions.
berghofe
parents:
12138
diff
changeset

302 
fun gen_add_thms pre_name args = 
18377  303 
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

304 

21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

305 
val add_thmss = gen_add_thmss (name_thms true true); 
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

306 
val add_thms = gen_add_thms (name_thms true true); 
5907  307 

308 

14564  309 
(* note_thmss(_i) *) 
5907  310 

9192  311 
local 
12711  312 

25981  313 
fun gen_note_thmss get tag = fold_map (fn ((bname, more_atts), ths_atts) => fn thy => 
12711  314 
let 
18728  315 
fun app (x, (ths, atts)) = foldl_map (Thm.theory_attributes atts) (x, ths); 
18418
bf448d999b7e
rearranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18377
diff
changeset

316 
val (thms, thy') = thy > enter_thms 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

317 
(name_thmss true) (name_thms false true) (apsnd flat o foldl_map app) 
25981  318 
(bname, map (fn (ths, atts) => (get thy ths, surround tag (atts @ more_atts))) ths_atts); 
18801  319 
in ((bname, thms), thy') end); 
12711  320 

9192  321 
in 
12711  322 

26344
04dacc6809b6
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset

323 
fun note_thmss k = gen_note_thmss get_fact (kind k); 
25981  324 
fun note_thmss_i k = gen_note_thmss (K I) (kind k); 
325 
fun note_thmss_grouped k g = gen_note_thmss (K I) (kind k #> group g); 

12711  326 

21438  327 
end; 
328 

25598  329 
fun note kind (name, thm) = 
330 
note_thmss_i kind [((name, []), [([thm], [])])] 

331 
#>> (fn [(_, [thm])] => thm); 

332 

18801  333 
fun note_thmss_qualified k path facts thy = 
334 
thy 

22796  335 
> Sign.add_path path 
336 
> Sign.no_base_names 

18801  337 
> note_thmss_i k facts 
22796  338 
> Sign.restore_naming thy; 
18801  339 

5280  340 

6091  341 
(* store_thm *) 
5280  342 

11998  343 
fun store_thm ((bname, thm), atts) thy = 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

344 
let val ([th'], thy') = add_thms_atts (name_thms true true) ((bname, [thm]), atts) thy 
18358  345 
in (th', thy') end; 
3987  346 

347 

16441  348 
(* smart_store_thms(_open) *) 
3987  349 

16441  350 
local 
351 

352 
fun smart_store _ (name, []) = 

11516
a0633bdcd015
Added equality axioms and initialization of proof term package.
berghofe
parents:
10667
diff
changeset

353 
error ("Cannot store empty list of theorems: " ^ quote name) 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

354 
 smart_store official (name, [thm]) = 
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

355 
fst (enter_thms (name_thms true official) (name_thms false official) I (name, [thm]) 
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

356 
(Thm.theory_of_thm thm)) 
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

357 
 smart_store official (name, thms) = 
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

358 
let val thy = Theory.merge_list (map Thm.theory_of_thm thms) in 
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

359 
fst (enter_thms (name_thms true official) (name_thms false official) I (name, thms) thy) 
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

360 
end; 
11516
a0633bdcd015
Added equality axioms and initialization of proof term package.
berghofe
parents:
10667
diff
changeset

361 

16441  362 
in 
363 

21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

364 
val smart_store_thms = smart_store true; 
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

365 
val smart_store_thms_open = smart_store false; 
16441  366 

367 
end; 

3987  368 

369 

16722
040728f6a103
tuned forall_elim_var(s): avoid expensive Term.add_vars;
wenzelm
parents:
16536
diff
changeset

370 
(* forall_elim_var(s)  belongs to drule.ML *) 
7899  371 

16722
040728f6a103
tuned forall_elim_var(s): avoid expensive Term.add_vars;
wenzelm
parents:
16536
diff
changeset

372 
fun forall_elim_vars_aux strip_vars i th = 
040728f6a103
tuned forall_elim_var(s): avoid expensive Term.add_vars;
wenzelm
parents:
16536
diff
changeset

373 
let 
040728f6a103
tuned forall_elim_var(s): avoid expensive Term.add_vars;
wenzelm
parents:
16536
diff
changeset

374 
val {thy, tpairs, prop, ...} = Thm.rep_thm th; 
16787  375 
val add_used = Term.fold_aterms 
20853  376 
(fn Var ((x, j), _) => if i = j then insert (op =) x else I  _ => I); 
16722
040728f6a103
tuned forall_elim_var(s): avoid expensive Term.add_vars;
wenzelm
parents:
16536
diff
changeset

377 
val used = fold (fn (t, u) => add_used t o add_used u) tpairs (add_used prop []); 
040728f6a103
tuned forall_elim_var(s): avoid expensive Term.add_vars;
wenzelm
parents:
16536
diff
changeset

378 
val vars = strip_vars prop; 
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
20057
diff
changeset

379 
val cvars = (Name.variant_list used (map #1 vars), vars) 
16722
040728f6a103
tuned forall_elim_var(s): avoid expensive Term.add_vars;
wenzelm
parents:
16536
diff
changeset

380 
> ListPair.map (fn (x, (_, T)) => Thm.cterm_of thy (Var ((x, i), T))); 
040728f6a103
tuned forall_elim_var(s): avoid expensive Term.add_vars;
wenzelm
parents:
16536
diff
changeset

381 
in fold Thm.forall_elim cvars th end; 
7899  382 

16722
040728f6a103
tuned forall_elim_var(s): avoid expensive Term.add_vars;
wenzelm
parents:
16536
diff
changeset

383 
val forall_elim_vars = forall_elim_vars_aux Term.strip_all_vars; 
040728f6a103
tuned forall_elim_var(s): avoid expensive Term.add_vars;
wenzelm
parents:
16536
diff
changeset

384 

040728f6a103
tuned forall_elim_var(s): avoid expensive Term.add_vars;
wenzelm
parents:
16536
diff
changeset

385 
fun forall_elim_var i th = forall_elim_vars_aux 
040728f6a103
tuned forall_elim_var(s): avoid expensive Term.add_vars;
wenzelm
parents:
16536
diff
changeset

386 
(fn Const ("all", _) $ Abs (a, T, _) => [(a, T)] 
040728f6a103
tuned forall_elim_var(s): avoid expensive Term.add_vars;
wenzelm
parents:
16536
diff
changeset

387 
 _ => raise THM ("forall_elim_vars", i, [th])) i th; 
7899  388 

389 

4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset

390 
(* store axioms as theorems *) 
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset

391 

4853  392 
local 
17418  393 
fun get_ax thy (name, _) = Thm.get_axiom_i thy (Sign.full_name thy name); 
394 
fun get_axs thy named_axs = map (forall_elim_vars 0 o get_ax thy) named_axs; 

18377  395 
fun add_single add ((name, ax), atts) thy = 
4853  396 
let 
11998  397 
val named_ax = [(name, ax)]; 
7753  398 
val thy' = add named_ax thy; 
399 
val thm = hd (get_axs thy' named_ax); 

18377  400 
in apfst hd (gen_add_thms (K I) [((name, thm), atts)] thy') end; 
401 
fun add_multi add ((name, axs), atts) thy = 

7753  402 
let 
403 
val named_axs = name_multi name axs; 

4853  404 
val thy' = add named_axs thy; 
7753  405 
val thms = get_axs thy' named_axs; 
18377  406 
in apfst hd (gen_add_thmss (K I) [((name, thms), atts)] thy') end; 
407 
fun add_singles add = fold_map (add_single add); 

408 
fun add_multis add = fold_map (add_multi add); 

4853  409 
in 
19629  410 
val add_axioms = add_singles Theory.add_axioms; 
411 
val add_axioms_i = add_singles Theory.add_axioms_i; 

412 
val add_axiomss = add_multis Theory.add_axioms; 

413 
val add_axiomss_i = add_multis Theory.add_axioms_i; 

22796  414 
val add_defs = add_singles o Theory.add_defs false; 
415 
val add_defs_i = add_singles o Theory.add_defs_i false; 

416 
val add_defs_unchecked = add_singles o Theory.add_defs true; 

417 
val add_defs_unchecked_i = add_singles o Theory.add_defs_i true; 

4853  418 
end; 
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset

419 

0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset

420 

3987  421 

26430  422 
(*** Pure theory syntax and logical content ***) 
3987  423 

24243  424 
val typ = SimpleSyntax.read_typ; 
425 
val term = SimpleSyntax.read_term; 

426 
val prop = SimpleSyntax.read_prop; 

427 

26430  428 
val _ = Context.>> 
429 
(Sign.add_types 

4922
03b81b6e1baa
added thms_closure: theory > xstring > tthm list option;
wenzelm
parents:
4853
diff
changeset

430 
[("fun", 2, NoSyn), 
03b81b6e1baa
added thms_closure: theory > xstring > tthm list option;
wenzelm
parents:
4853
diff
changeset

431 
("prop", 0, NoSyn), 
03b81b6e1baa
added thms_closure: theory > xstring > tthm list option;
wenzelm
parents:
4853
diff
changeset

432 
("itself", 1, NoSyn), 
03b81b6e1baa
added thms_closure: theory > xstring > tthm list option;
wenzelm
parents:
4853
diff
changeset

433 
("dummy", 0, NoSyn)] 
26430  434 
#> Sign.add_nonterminals Syntax.basic_nonterms 
435 
#> Sign.add_syntax_i 

26436  436 
[("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3%_./ _)", [0, 3], 3)), 
437 
("_abs", typ "'a", NoSyn), 

438 
("", typ "'a => args", Delimfix "_"), 

439 
("_args", typ "'a => args => args", Delimfix "_,/ _"), 

440 
("", typ "id => idt", Delimfix "_"), 

441 
("_idtdummy", typ "idt", Delimfix "'_"), 

442 
("_idtyp", typ "id => type => idt", Mixfix ("_::_", [], 0)), 

443 
("_idtypdummy", typ "type => idt", Mixfix ("'_()::_", [], 0)), 

444 
("", typ "idt => idt", Delimfix "'(_')"), 

445 
("", typ "idt => idts", Delimfix "_"), 

446 
("_idts", typ "idt => idts => idts", Mixfix ("_/ _", [1, 0], 0)), 

447 
("", typ "idt => pttrn", Delimfix "_"), 

448 
("", typ "pttrn => pttrns", Delimfix "_"), 

449 
("_pttrns", typ "pttrn => pttrns => pttrns", Mixfix ("_/ _", [1, 0], 0)), 

450 
("", typ "id => aprop", Delimfix "_"), 

451 
("", typ "longid => aprop", Delimfix "_"), 

452 
("", typ "var => aprop", Delimfix "_"), 

453 
("_DDDOT", typ "aprop", Delimfix "..."), 

454 
("_aprop", typ "aprop => prop", Delimfix "PROP _"), 

455 
("_asm", typ "prop => asms", Delimfix "_"), 

456 
("_asms", typ "prop => asms => asms", Delimfix "_;/ _"), 

457 
("_bigimpl", typ "asms => prop => prop", Mixfix ("((3[ _ ])/ ==> _)", [0, 1], 1)), 

458 
("_ofclass", typ "type => logic => prop", Delimfix "(1OFCLASS/(1'(_,/ _')))"), 

459 
("_mk_ofclass", typ "dummy", NoSyn), 

460 
("_TYPE", typ "type => logic", Delimfix "(1TYPE/(1'(_')))"), 

461 
("", typ "id => logic", Delimfix "_"), 

462 
("", typ "longid => logic", Delimfix "_"), 

463 
("", typ "var => logic", Delimfix "_"), 

464 
("_DDDOT", typ "logic", Delimfix "..."), 

465 
("_constify", typ "num => num_const", Delimfix "_"), 

466 
("_indexnum", typ "num_const => index", Delimfix "\\<^sub>_"), 

467 
("_index", typ "logic => index", Delimfix "(00\\<^bsub>_\\<^esub>)"), 

468 
("_indexdefault", typ "index", Delimfix ""), 

469 
("_indexvar", typ "index", Delimfix "'\\<index>"), 

470 
("_struct", typ "index => logic", Mixfix ("\\<struct>_", [1000], 1000)), 

471 
("==>", typ "prop => prop => prop", Delimfix "op ==>"), 

472 
(Term.dummy_patternN, typ "aprop", Delimfix "'_"), 

473 
("_appl", typ "('b => 'a) => args => logic", Mixfix ("(1_/(1'(_')))", [1000, 0], 1000)), 

474 
("_appl", typ "('b => 'a) => args => aprop", Mixfix ("(1_/(1'(_')))", [1000, 0], 1000))] 

26430  475 
#> Sign.add_modesyntax_i (Symbol.xsymbolsN, true) 
24243  476 
[("fun", typ "type => type => type", Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)), 
477 
("_bracket", typ "types => type => type", Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)), 

478 
("_ofsort", typ "tid => sort => type", Mixfix ("_\\<Colon>_", [1000, 0], 1000)), 

479 
("_constrain", typ "'a => type => 'a", Mixfix ("_\\<Colon>_", [4, 0], 3)), 

480 
("_idtyp", typ "id => type => idt", Mixfix ("_\\<Colon>_", [], 0)), 

481 
("_idtypdummy", typ "type => idt", Mixfix ("'_()\\<Colon>_", [], 0)), 

482 
("_type_constraint_", typ "'a", NoSyn), 

483 
("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)), 

484 
("==", typ "'a => 'a => prop", InfixrName ("\\<equiv>", 2)), 

485 
("all_binder", typ "idts => prop => prop", Mixfix ("(3\\<And>_./ _)", [0, 0], 0)), 

486 
("==>", typ "prop => prop => prop", InfixrName ("\\<Longrightarrow>", 1)), 

487 
("_DDDOT", typ "aprop", Delimfix "\\<dots>"), 

488 
("_bigimpl", typ "asms => prop => prop", Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)), 

489 
("_DDDOT", typ "logic", Delimfix "\\<dots>")] 

26430  490 
#> Sign.add_modesyntax_i ("", false) 
24243  491 
[("prop", typ "prop => prop", Mixfix ("_", [0], 0)), 
26430  492 
("Pure.term", typ "'a => prop", Delimfix "TERM _"), 
493 
("Pure.conjunction", typ "prop => prop => prop", InfixrName ("&&", 2))] 

494 
#> Sign.add_modesyntax_i ("HTML", false) 

24243  495 
[("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3))] 
26430  496 
#> Sign.add_consts_i 
24243  497 
[("==", typ "'a => 'a => prop", InfixrName ("==", 2)), 
498 
("==>", typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)), 

499 
("all", typ "('a => prop) => prop", Binder ("!!", 0, 0)), 

500 
("prop", typ "prop => prop", NoSyn), 

501 
("TYPE", typ "'a itself", NoSyn), 

502 
(Term.dummy_patternN, typ "'a", Delimfix "'_")] 

26430  503 
#> Theory.add_deps "==" ("==", typ "'a => 'a => prop") [] 
504 
#> Theory.add_deps "==>" ("==>", typ "prop => prop => prop") [] 

505 
#> Theory.add_deps "all" ("all", typ "('a => prop) => prop") [] 

506 
#> Theory.add_deps "TYPE" ("TYPE", typ "'a itself") [] 

507 
#> Theory.add_deps Term.dummy_patternN (Term.dummy_patternN, typ "'a") [] 

508 
#> Sign.add_trfuns Syntax.pure_trfuns 

509 
#> Sign.add_trfunsT Syntax.pure_trfunsT 

510 
#> Sign.local_path 

511 
#> Sign.add_consts_i 

24243  512 
[("term", typ "'a => prop", NoSyn), 
513 
("conjunction", typ "prop => prop => prop", NoSyn)] 

26430  514 
#> (add_defs_i false o map Thm.no_attributes) 
24243  515 
[("prop_def", prop "(CONST prop :: prop => prop) (A::prop) == A::prop"), 
26430  516 
("term_def", prop "(CONST Pure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"), 
517 
("conjunction_def", prop "(A && B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd 

518 
#> Sign.hide_consts false ["conjunction", "term"] 

519 
#> add_thmss [(("nothing", []), [])] #> snd 

520 
#> Theory.add_axioms_i Proofterm.equality_axms); 

3987  521 

522 
end; 

523 