author  wenzelm 
Thu, 20 Mar 2008 17:38:54 +0100  
changeset 26367  06635166d211 
parent 26361  7946f459c6c8 
child 26393  42febbed5460 
permissions  rwrr 
3987  1 
(* Title: Pure/pure_thy.ML 
2 
ID: $Id$ 

3 
Author: Markus Wenzel, TU Muenchen 

4 

16441  5 
Theorem storage. 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 
5091  10 
structure ProtoPure: 
11 
sig 

12 
val thy: theory 

18031  13 
val prop_def: thm 
19775  14 
val term_def: thm 
19125
59b26248547b
simplified Pure conjunction, based on actual const;
wenzelm
parents:
19046
diff
changeset

15 
val conjunction_def: thm 
5091  16 
end 
4853  17 
end; 
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset

18 

3987  19 
signature PURE_THY = 
20 
sig 

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

21 
include BASIC_PURE_THY 
23657  22 
val tag_rule: Markup.property > thm > thm 
18801  23 
val untag_rule: string > thm > thm 
23657  24 
val tag: Markup.property > attribute 
18801  25 
val untag: string > attribute 
21964  26 
val has_name_hint: thm > bool 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

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

28 
val put_name_hint: string > thm > thm 
25981  29 
val get_group: thm > string option 
30 
val put_group: string > thm > thm 

31 
val group: string > attribute 

22251  32 
val has_kind: thm > bool 
18801  33 
val get_kind: thm > string 
34 
val kind_rule: string > thm > thm 

35 
val kind: string > attribute 

36 
val kind_internal: attribute 

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

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

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

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

42 
val get_thm: theory > xstring > thm 
17162  43 
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

44 
val all_facts_of: theory > Facts.T 
16336  45 
val thms_of: theory > (string * thm) list 
46 
val all_thms_of: theory > (string * thm) list 

12695  47 
val hide_thms: bool > string list > theory > theory 
21580  48 
val map_facts: ('a > 'b) > ('c * ('a list * 'd) list) list > ('c * ('b list * 'd) list) list 
21567  49 
val burrow_fact: ('a list > 'b list) > ('a list * 'c) list > ('b list * 'c) list 
21580  50 
val burrow_facts: ('a list > 'b list) > 
51 
('c * ('a list * 'd) list) list > ('c * ('b list * 'd) list) list 

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

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

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

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

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

58 
val smart_store_thms_open: (bstring * thm list) > thm list 
7899  59 
val forall_elim_var: int > thm > thm 
60 
val forall_elim_vars: int > thm > thm 

18728  61 
val add_thms: ((bstring * thm) * attribute list) list > theory > thm list * theory 
24965  62 
val add_thmss: ((bstring * thm list) * attribute list) list > theory > thm list list * theory 
25598  63 
val note: string > string * thm > theory > thm * theory 
18801  64 
val note_thmss: string > ((bstring * attribute list) * 
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26320
diff
changeset

65 
(Facts.ref * attribute list) list) list > theory > (bstring * thm list) list * theory 
18801  66 
val note_thmss_i: string > ((bstring * attribute list) * 
67 
(thm list * attribute list) list) list > theory > (bstring * thm list) list * theory 

25981  68 
val note_thmss_grouped: string > string > ((bstring * attribute list) * 
69 
(thm list * attribute list) list) list > theory > (bstring * thm list) list * theory 

18801  70 
val note_thmss_qualified: string > string > ((bstring * attribute list) * 
18728  71 
(thm list * attribute list) list) list > theory > (bstring * thm list) list * theory 
72 
val add_axioms: ((bstring * string) * attribute list) list > theory > thm list * theory 

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

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

75 
theory > thm list list * theory 

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

77 
theory > thm list list * theory 

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

18377  79 
theory > thm list * theory 
18728  80 
val add_defs_i: bool > ((bstring * term) * attribute list) list > 
18377  81 
theory > thm list * theory 
19629  82 
val add_defs_unchecked: bool > ((bstring * string) * attribute list) list > 
83 
theory > thm list * theory 

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

85 
theory > thm list * theory 

24243  86 
val appl_syntax: (string * typ * mixfix) list 
87 
val applC_syntax: (string * typ * mixfix) list 

3987  88 
end; 
89 

90 
structure PureThy: PURE_THY = 

91 
struct 

92 

93 

18801  94 
(*** theorem tags ***) 
95 

96 
(* add / delete tags *) 

97 

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

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

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

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

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

103 

104 

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

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

106 

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

109 
val has_name_hint = can the_name_hint; 

110 
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

111 

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

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

114 

25981  115 
(* theorem groups *) 
116 

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

118 

119 
fun put_group name = 

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

121 

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

123 

124 

18801  125 
(* theorem kinds *) 
126 

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

129 
val has_kind = can the_kind; 

25981  130 
val get_kind = the_default "" o try the_kind; 
18801  131 

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

136 
val is_internal = has_internal o Thm.get_tags; 
18801  137 

138 

139 

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

140 
(*** theorem database ***) 
3987  141 

16441  142 
(** dataype theorems **) 
3987  143 

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

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

146 
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

147 

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

149 

16441  150 
structure TheoremsData = TheoryDataFun 
24713  151 
( 
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 
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

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

155 
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

156 
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

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

158 
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

159 
ref (make_thms NameSpace.empty_table (Facts.merge (all_facts1, all_facts2))); 
24713  160 
); 
3987  161 

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

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

165 
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

166 

6367  167 

3987  168 

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

169 
(** retrieve theorems **) 
3987  170 

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

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

172 

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

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

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

177 
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

178 

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

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

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

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

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

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

184 

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

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

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

187 

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

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

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

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

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

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

193 
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

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

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

196 
(NONE, NONE) => true 
009e56d16080
get_thm(s): check facts lookup vs. old thm database;
wenzelm
parents:
26282
diff
changeset

197 
 (SOME (name1, ths1), SOME (name2, ths2)) => name1 = name2 andalso Thm.eq_thms (ths1, ths2) 
009e56d16080
get_thm(s): check facts lookup vs. old thm database;
wenzelm
parents:
26282
diff
changeset

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

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

201 
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

202 
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

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

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

205 
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

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

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

208 

26320  209 
in 
210 

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

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

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

213 

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

215 
fun get_thm thy name = Facts.the_single name (get_thms thy name); 
4783  216 

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

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

218 

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

219 

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

221 

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

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

224 
in map (`(get_name_hint)) (maps snd (Symtab.dest thms)) end; 
15703  225 

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

226 
fun all_thms_of thy = maps thms_of (thy :: Theory.ancestors_of thy); 
16336  227 

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

228 

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

229 

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

230 
(** store theorems **) (*DESTRUCTIVE*) 
3987  231 

16441  232 
(* hiding  affects current theory node only *) 
12695  233 

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

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

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

240 

21580  241 
(* fact specifications *) 
242 

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

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

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

246 

247 

4853  248 
(* naming *) 
249 

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

4853  252 

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

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

255 

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

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

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

260 

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

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

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

263 

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

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

265 
burrow_fact (name_thms true official name) fact; 
4853  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 

5091  422 
(*** the ProtoPure theory ***) 
3987  423 

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

426 
val prop = SimpleSyntax.read_prop; 

427 

428 
val appl_syntax = 

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

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

431 

432 
val applC_syntax = 

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

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

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

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

16441  437 

3987  438 
val proto_pure = 
16493  439 
Context.pre_pure_thy 
16987  440 
> Compress.init_data 
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset

441 
> TheoremsData.init 
22796  442 
> Sign.add_types 
4922
03b81b6e1baa
added thms_closure: theory > xstring > tthm list option;
wenzelm
parents:
4853
diff
changeset

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

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

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

446 
("dummy", 0, NoSyn)] 
22796  447 
> Sign.add_nonterminals Syntax.basic_nonterms 
24243  448 
> Sign.add_syntax_i 
449 
[("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3%_./ _)", [0, 3], 3)), 

450 
("_abs", typ "'a", NoSyn), 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

486 
> Sign.add_syntax_i appl_syntax 

487 
> Sign.add_modesyntax_i (Symbol.xsymbolsN, true) 

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

489 
("_bracket", typ "types => type => type", Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)), 

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

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

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

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

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

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

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

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

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

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

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

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

502 
> Sign.add_modesyntax_i ("", false) 

503 
[("prop", typ "prop => prop", Mixfix ("_", [0], 0)), 

504 
("ProtoPure.term", typ "'a => prop", Delimfix "TERM _"), 

505 
("ProtoPure.conjunction", typ "prop => prop => prop", InfixrName ("&&", 2))] 

506 
> Sign.add_modesyntax_i ("HTML", false) 

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

508 
> Sign.add_consts_i 

509 
[("==", typ "'a => 'a => prop", InfixrName ("==", 2)), 

510 
("==>", typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)), 

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

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

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

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

25018
fac2ceba75b4
replaced obsolete Theory.add_finals_i by Theory.add_deps;
wenzelm
parents:
24965
diff
changeset

515 
> Theory.add_deps "==" ("==", typ "'a => 'a => prop") [] 
fac2ceba75b4
replaced obsolete Theory.add_finals_i by Theory.add_deps;
wenzelm
parents:
24965
diff
changeset

516 
> Theory.add_deps "==>" ("==>", typ "prop => prop => prop") [] 
fac2ceba75b4
replaced obsolete Theory.add_finals_i by Theory.add_deps;
wenzelm
parents:
24965
diff
changeset

517 
> Theory.add_deps "all" ("all", typ "('a => prop) => prop") [] 
fac2ceba75b4
replaced obsolete Theory.add_finals_i by Theory.add_deps;
wenzelm
parents:
24965
diff
changeset

518 
> Theory.add_deps "TYPE" ("TYPE", typ "'a itself") [] 
fac2ceba75b4
replaced obsolete Theory.add_finals_i by Theory.add_deps;
wenzelm
parents:
24965
diff
changeset

519 
> Theory.add_deps Term.dummy_patternN (Term.dummy_patternN, typ "'a") [] 
22796  520 
> Sign.add_trfuns Syntax.pure_trfuns 
521 
> Sign.add_trfunsT Syntax.pure_trfunsT 

16441  522 
> Sign.local_path 
24243  523 
> Sign.add_consts_i 
524 
[("term", typ "'a => prop", NoSyn), 

525 
("conjunction", typ "prop => prop => prop", NoSyn)] 

526 
> (add_defs_i false o map Thm.no_attributes) 

527 
[("prop_def", prop "(CONST prop :: prop => prop) (A::prop) == A::prop"), 

528 
("term_def", prop "(CONST ProtoPure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"), 

529 
("conjunction_def", prop "(A && B) == (!!C::prop. (A ==> B ==> C) ==> C)")] > snd 

19775  530 
> Sign.hide_consts false ["conjunction", "term"] 
18377  531 
> add_thmss [(("nothing", []), [])] > snd 
11516
a0633bdcd015
Added equality axioms and initialization of proof term package.
berghofe
parents:
10667
diff
changeset

532 
> Theory.add_axioms_i Proofterm.equality_axms 
16493  533 
> Theory.end_theory; 
3987  534 

5091  535 
structure ProtoPure = 
536 
struct 

537 
val thy = proto_pure; 

18031  538 
val prop_def = get_axiom thy "prop_def"; 
19775  539 
val term_def = get_axiom thy "term_def"; 
19125
59b26248547b
simplified Pure conjunction, based on actual const;
wenzelm
parents:
19046
diff
changeset

540 
val conjunction_def = get_axiom thy "conjunction_def"; 
5091  541 
end; 
3987  542 

543 
end; 

544 

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

545 
structure BasicPureThy: BASIC_PURE_THY = PureThy; 
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset

546 
open BasicPureThy; 