author  wenzelm 
Thu, 27 Mar 2008 14:41:18 +0100  
changeset 26430  8ddb2e7c5a1e 
parent 26395  9e0e4ce51313 
child 26436  dfd6947ab5c2 
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 

24243  75 
val appl_syntax: (string * typ * mixfix) list 
76 
val applC_syntax: (string * typ * mixfix) list 

3987  77 
end; 
78 

79 
structure PureThy: PURE_THY = 

80 
struct 

81 

82 

18801  83 
(*** theorem tags ***) 
84 

85 
(* add / delete tags *) 

86 

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

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

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

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

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

92 

93 

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

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

95 

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

98 
val has_name_hint = can the_name_hint; 

99 
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

100 

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

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

103 

25981  104 
(* theorem groups *) 
105 

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

107 

108 
fun put_group name = 

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

110 

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

112 

113 

18801  114 
(* theorem kinds *) 
115 

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

118 
val has_kind = can the_kind; 

25981  119 
val get_kind = the_default "" o try the_kind; 
18801  120 

23657  121 
fun kind_rule k = tag_rule (Markup.kindN, k) o untag_rule Markup.kindN; 
18801  122 
fun kind k x = if k = "" then x else Thm.rule_attribute (K (kind_rule k)) x; 
22363  123 
fun kind_internal x = kind Thm.internalK x; 
23657  124 
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

125 
val is_internal = has_internal o Thm.get_tags; 
18801  126 

127 

128 

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

129 
(*** theorem database ***) 
3987  130 

16441  131 
(** dataype theorems **) 
3987  132 

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

133 
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

134 
{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

135 
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

136 

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

137 
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

138 

16441  139 
structure TheoremsData = TheoryDataFun 
24713  140 
( 
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

141 
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

142 
val empty = ref (make_thms NameSpace.empty_table Facts.empty); 
6547  143 
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

144 
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

145 
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

146 
(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

147 
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

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

26430  151 
val _ = Context.>> TheoremsData.init; 
152 

16493  153 
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

154 
val get_theorems = (fn Thms args => args) o ! o get_theorems_ref; 
17162  155 
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

156 
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

157 

6367  158 

3987  159 

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

160 
(** retrieve theorems **) 
3987  161 

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

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

163 

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

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

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

168 
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

169 

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

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

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

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

173 
val name = NameSpace.intern (Facts.space_of facts) xname; 
26393  174 
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

175 

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

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

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

178 

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

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

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

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

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

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

184 
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

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

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

187 
(NONE, NONE) => true 
26395  188 
 (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

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

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

192 
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

193 
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

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

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

196 
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

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

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

199 

26320  200 
in 
201 

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

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

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

204 

26361  205 
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

206 
fun get_thm thy name = Facts.the_single name (get_thms thy name); 
4783  207 

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

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

209 

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

210 

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

212 

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

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

215 
in map (`(get_name_hint)) (maps snd (Symtab.dest thms)) end; 
15703  216 

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

217 
fun all_thms_of thy = maps thms_of (thy :: Theory.ancestors_of thy); 
16336  218 

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

219 

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

220 

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

221 
(** store theorems **) (*DESTRUCTIVE*) 
3987  222 

16441  223 
(* hiding  affects current theory node only *) 
12695  224 

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

227 
val r as ref (Thms {theorems = (space, thms), all_facts}) = get_theorems_ref thy; 
16132  228 
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

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

231 

21580  232 
(* fact specifications *) 
233 

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

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

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

237 

238 

4853  239 
(* naming *) 
240 

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

4853  243 

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

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

246 

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

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

248 
> (if Thm.get_name thm <> "" andalso pre orelse not official then I else Thm.put_name name) 
26050  249 
> (if has_name_hint thm andalso pre orelse name = "" then I else put_name_hint name) 
250 
> 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

251 

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

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

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

254 

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

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

256 
burrow_fact (name_thms true official name) fact; 
4853  257 

258 

26393  259 
(* add_thms_dynamic *) 
260 

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

262 
let 

263 
val name = Sign.full_name thy bname; 

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

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

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

267 
in thy end); 

268 

269 

11998  270 
(* enter_thms *) 
4853  271 

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

272 
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

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

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

275 
fun enter_thms _ _ app_att ("", thms) thy = app_att (thy, thms) > swap 
23933  276 
 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

277 
let 
16441  278 
val name = Sign.full_name thy bname; 
279 
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

280 
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

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

13274  289 
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

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

291 
(thms', thy') 
23933  292 
end); 
3987  293 

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

294 

6091  295 
(* add_thms(s) *) 
4853  296 

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

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

299 
(foldl_map (Thm.theory_attributes atts)) (bname, thms); 
4853  300 

18377  301 
fun gen_add_thmss pre_name = 
302 
fold_map (add_thms_atts pre_name); 

5907  303 

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

304 
fun gen_add_thms pre_name args = 
18377  305 
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

306 

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

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

308 
val add_thms = gen_add_thms (name_thms true true); 
5907  309 

310 

14564  311 
(* note_thmss(_i) *) 
5907  312 

9192  313 
local 
12711  314 

25981  315 
fun gen_note_thmss get tag = fold_map (fn ((bname, more_atts), ths_atts) => fn thy => 
12711  316 
let 
18728  317 
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

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

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

9192  323 
in 
12711  324 

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

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

12711  328 

21438  329 
end; 
330 

25598  331 
fun note kind (name, thm) = 
332 
note_thmss_i kind [((name, []), [([thm], [])])] 

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

334 

18801  335 
fun note_thmss_qualified k path facts thy = 
336 
thy 

22796  337 
> Sign.add_path path 
338 
> Sign.no_base_names 

18801  339 
> note_thmss_i k facts 
22796  340 
> Sign.restore_naming thy; 
18801  341 

5280  342 

6091  343 
(* store_thm *) 
5280  344 

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

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

349 

16441  350 
(* smart_store_thms(_open) *) 
3987  351 

16441  352 
local 
353 

354 
fun smart_store _ (name, []) = 

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

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

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

357 
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

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

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

360 
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

361 
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

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

363 

16441  364 
in 
365 

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

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

367 
val smart_store_thms_open = smart_store false; 
16441  368 

369 
end; 

3987  370 

371 

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

372 
(* forall_elim_var(s)  belongs to drule.ML *) 
7899  373 

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

374 
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

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

376 
val {thy, tpairs, prop, ...} = Thm.rep_thm th; 
16787  377 
val add_used = Term.fold_aterms 
20853  378 
(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

379 
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

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

381 
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

382 
> 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

383 
in fold Thm.forall_elim cvars th end; 
7899  384 

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

385 
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

386 

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

387 
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

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

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

391 

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

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

393 

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

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

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

7753  404 
let 
405 
val named_axs = name_multi name axs; 

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

410 
fun add_multis add = fold_map (add_multi add); 

4853  411 
in 
19629  412 
val add_axioms = add_singles Theory.add_axioms; 
413 
val add_axioms_i = add_singles Theory.add_axioms_i; 

414 
val add_axiomss = add_multis Theory.add_axioms; 

415 
val add_axiomss_i = add_multis Theory.add_axioms_i; 

22796  416 
val add_defs = add_singles o Theory.add_defs false; 
417 
val add_defs_i = add_singles o Theory.add_defs_i false; 

418 
val add_defs_unchecked = add_singles o Theory.add_defs true; 

419 
val add_defs_unchecked_i = add_singles o Theory.add_defs_i true; 

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

421 

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

422 

3987  423 

26430  424 
(*** Pure theory syntax and logical content ***) 
3987  425 

24243  426 
val typ = SimpleSyntax.read_typ; 
427 
val term = SimpleSyntax.read_term; 

428 
val prop = SimpleSyntax.read_prop; 

429 

430 
val appl_syntax = 

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

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

433 

434 
val applC_syntax = 

435 
[("", typ "'a => cargs", Delimfix "_"), 

436 
("_cargs", typ "'a => cargs => cargs", Mixfix ("_/ _", [1000, 1000], 1000)), 

437 
("_applC", typ "('b => 'a) => cargs => logic", Mixfix ("(1_/ _)", [1000, 1000], 999)), 

438 
("_applC", typ "('b => 'a) => cargs => aprop", Mixfix ("(1_/ _)", [1000, 1000], 999))]; 

16441  439 

26430  440 
val _ = Context.>> 
441 
(Sign.add_types 

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

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

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

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

445 
("dummy", 0, NoSyn)] 
26430  446 
#> Sign.add_nonterminals Syntax.basic_nonterms 
447 
#> Sign.add_syntax_i 

24243  448 
[("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3%_./ _)", [0, 3], 3)), 
449 
("_abs", typ "'a", NoSyn), 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

26430  485 
#> Sign.add_syntax_i appl_syntax 
486 
#> Sign.add_modesyntax_i (Symbol.xsymbolsN, true) 

24243  487 
[("fun", typ "type => type => type", Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)), 
488 
("_bracket", typ "types => type => type", Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)), 

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

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

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

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

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

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

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

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

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

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

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

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

26430  501 
#> Sign.add_modesyntax_i ("", false) 
24243  502 
[("prop", typ "prop => prop", Mixfix ("_", [0], 0)), 
26430  503 
("Pure.term", typ "'a => prop", Delimfix "TERM _"), 
504 
("Pure.conjunction", typ "prop => prop => prop", InfixrName ("&&", 2))] 

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

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

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

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

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

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

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

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

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

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

519 
#> Sign.add_trfuns Syntax.pure_trfuns 

520 
#> Sign.add_trfunsT Syntax.pure_trfunsT 

521 
#> Sign.local_path 

522 
#> Sign.add_consts_i 

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

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

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

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

531 
#> Theory.add_axioms_i Proofterm.equality_axms); 

3987  532 

533 
end; 

534 