author  paulson 
Fri, 05 Oct 2007 09:59:03 +0200  
changeset 24854  0ebcd575d3c6 
parent 24817  636b23afee76 
child 24965  8b4a02947721 
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 
16493  10 
datatype interval = FromTo of int * int  From of int  Single of int 
18031  11 
datatype thmref = 
12 
Name of string  

13 
NameSelection of string * interval list  

14 
Fact of string 

15456
956d6acacf89
Specific theorems in a named list of theorems can now be referred to
berghofe
parents:
15387
diff
changeset

15 
val get_thm: theory > thmref > thm 
956d6acacf89
Specific theorems in a named list of theorems can now be referred to
berghofe
parents:
15387
diff
changeset

16 
val get_thms: theory > thmref > thm list 
956d6acacf89
Specific theorems in a named list of theorems can now be referred to
berghofe
parents:
15387
diff
changeset

17 
val get_thmss: theory > thmref list > thm list 
5091  18 
structure ProtoPure: 
19 
sig 

20 
val thy: theory 

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

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

26 

3987  27 
signature PURE_THY = 
28 
sig 

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

29 
include BASIC_PURE_THY 
23657  30 
val tag_rule: Markup.property > thm > thm 
18801  31 
val untag_rule: string > thm > thm 
23657  32 
val tag: Markup.property > attribute 
18801  33 
val untag: string > attribute 
21964  34 
val has_name_hint: thm > bool 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

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

36 
val put_name_hint: string > thm > thm 
22251  37 
val has_kind: thm > bool 
18801  38 
val get_kind: thm > string 
39 
val kind_rule: string > thm > thm 

40 
val kind: string > attribute 

41 
val kind_internal: attribute 

23657  42 
val has_internal: Markup.property list > bool 
18801  43 
val is_internal: thm > bool 
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset

44 
val string_of_thmref: thmref > string 
15456
956d6acacf89
Specific theorems in a named list of theorems can now be referred to
berghofe
parents:
15387
diff
changeset

45 
val get_thm_closure: theory > thmref > thm 
956d6acacf89
Specific theorems in a named list of theorems can now be referred to
berghofe
parents:
15387
diff
changeset

46 
val get_thms_closure: theory > thmref > thm list 
9564  47 
val single_thm: string > thm list > thm 
16493  48 
val name_of_thmref: thmref > string 
49 
val map_name_of_thmref: (string > string) > thmref > thmref 

15456
956d6acacf89
Specific theorems in a named list of theorems can now be referred to
berghofe
parents:
15387
diff
changeset

50 
val select_thm: thmref > thm list > thm list 
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset

51 
val selections: string * thm list > (thmref * thm) list 
17162  52 
val theorems_of: theory > thm list NameSpace.table 
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset

53 
val fact_index_of: theory > FactIndex.T 
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset

54 
val valid_thms: theory > thmref * thm list > bool 
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset

55 
val thms_containing: theory > FactIndex.spec > (string * thm list) list 
13646  56 
val thms_containing_consts: theory > string list > (string * thm) list 
16336  57 
val thms_of: theory > (string * thm) list 
58 
val all_thms_of: theory > (string * thm) list 

12695  59 
val hide_thms: bool > string list > theory > theory 
21580  60 
val map_facts: ('a > 'b) > ('c * ('a list * 'd) list) list > ('c * ('b list * 'd) list) list 
21567  61 
val burrow_fact: ('a list > 'b list) > ('a list * 'c) list > ('b list * 'c) list 
21580  62 
val burrow_facts: ('a list > 'b list) > 
63 
('c * ('a list * 'd) list) list > ('c * ('b list * 'd) list) list 

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

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

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

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

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

70 
val smart_store_thms_open: (bstring * thm list) > thm list 
7899  71 
val forall_elim_var: int > thm > thm 
72 
val forall_elim_vars: int > thm > thm 

18728  73 
val add_thms: ((bstring * thm) * attribute list) list > theory > thm list * theory 
74 
val add_thmss: ((bstring * thm list) * attribute list) list > theory > thm list list * theory 

18801  75 
val note_thmss: string > ((bstring * attribute list) * 
18728  76 
(thmref * attribute list) list) list > theory > (bstring * thm list) list * theory 
18801  77 
val note_thmss_i: string > ((bstring * attribute list) * 
78 
(thm list * attribute list) list) list > theory > (bstring * thm list) list * theory 

79 
val note_thmss_qualified: string > string > ((bstring * attribute list) * 

18728  80 
(thm list * attribute list) list) list > theory > (bstring * thm list) list * theory 
81 
val add_axioms: ((bstring * string) * attribute list) list > theory > thm list * theory 

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

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

84 
theory > thm list list * theory 

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

86 
theory > thm list list * theory 

24434  87 
val simple_def: bstring * attribute list > 
88 
((bstring * typ * mixfix) * term list) * term > theory > (string * thm) * theory 

18728  89 
val add_defs: bool > ((bstring * string) * attribute list) list > 
18377  90 
theory > thm list * theory 
18728  91 
val add_defs_i: bool > ((bstring * term) * attribute list) list > 
18377  92 
theory > thm list * theory 
19629  93 
val add_defs_unchecked: bool > ((bstring * string) * attribute list) list > 
94 
theory > thm list * theory 

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

96 
theory > thm list * theory 

24243  97 
val appl_syntax: (string * typ * mixfix) list 
98 
val applC_syntax: (string * typ * mixfix) list 

3987  99 
end; 
100 

101 
structure PureThy: PURE_THY = 

102 
struct 

103 

104 

18801  105 
(*** theorem tags ***) 
106 

107 
(* add / delete tags *) 

108 

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

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

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

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

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

114 

115 

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

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

117 

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

120 
val has_name_hint = can the_name_hint; 

121 
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

122 

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

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

125 

18801  126 
(* theorem kinds *) 
127 

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

130 
val has_kind = can the_kind; 

131 
val get_kind = the_default "??.unknown" o try the_kind; 

18801  132 

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

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

139 

140 

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

141 
(*** theorem database ***) 
3987  142 

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

16441  145 
structure TheoremsData = TheoryDataFun 
24713  146 
( 
5005  147 
type T = 
16441  148 
{theorems: thm list NameSpace.table, 
149 
index: FactIndex.T} ref; 

3987  150 

4853  151 
fun mk_empty _ = 
16336  152 
ref {theorems = NameSpace.empty_table, index = FactIndex.empty}: T; 
3987  153 

5005  154 
val empty = mk_empty (); 
6547  155 
fun copy (ref x) = ref x; 
16441  156 
val extend = mk_empty; 
157 
fun merge _ = mk_empty; 

24713  158 
); 
3987  159 

16493  160 
val get_theorems_ref = TheoremsData.get; 
161 
val get_theorems = ! o get_theorems_ref; 

17162  162 
val theorems_of = #theorems o get_theorems; 
16493  163 
val fact_index_of = #index o get_theorems; 
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset

164 

6367  165 

3987  166 

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

167 
(** retrieve theorems **) 
3987  168 

15531  169 
fun the_thms _ (SOME thms) = thms 
170 
 the_thms name NONE = error ("Unknown theorem(s) " ^ quote name); 

4037  171 

9564  172 
fun single_thm _ [thm] = thm 
173 
 single_thm name _ = error ("Single theorem expected " ^ quote name); 

174 

15703  175 

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

176 
(* datatype interval *) 
15703  177 

178 
datatype interval = 

179 
FromTo of int * int  

180 
From of int  

181 
Single of int; 

182 

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

183 
fun string_of_interval (FromTo (i, j)) = string_of_int i ^ "" ^ string_of_int j 
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset

184 
 string_of_interval (From i) = string_of_int i ^ "" 
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset

185 
 string_of_interval (Single i) = string_of_int i; 
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset

186 

24793  187 
fun interval n iv = 
188 
let fun err () = raise Fail ("Bad interval specification " ^ string_of_interval iv) in 

189 
(case iv of 

190 
FromTo (i, j) => if i <= j then i upto j else err () 

191 
 From i => if i <= n then i upto n else err () 

192 
 Single i => [i]) 

193 
end; 

194 

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

195 

16493  196 
(* datatype thmref *) 
197 

198 
datatype thmref = 

199 
Name of string  

18031  200 
NameSelection of string * interval list  
201 
Fact of string; 

15703  202 

16493  203 
fun name_of_thmref (Name name) = name 
18031  204 
 name_of_thmref (NameSelection (name, _)) = name 
18678  205 
 name_of_thmref (Fact _) = error "Illegal literal fact"; 
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset

206 

16493  207 
fun map_name_of_thmref f (Name name) = Name (f name) 
18031  208 
 map_name_of_thmref f (NameSelection (name, is)) = NameSelection (f name, is) 
209 
 map_name_of_thmref _ thmref = thmref; 

16493  210 

211 
fun string_of_thmref (Name name) = name 

212 
 string_of_thmref (NameSelection (name, is)) = 

18031  213 
name ^ enclose "(" ")" (commas (map string_of_interval is)) 
18678  214 
 string_of_thmref (Fact _) = error "Illegal literal fact"; 
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset

215 

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

216 

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

217 
(* select_thm *) 
15703  218 

16493  219 
fun select_thm (Name _) thms = thms 
18031  220 
 select_thm (Fact _) thms = thms 
24793  221 
 select_thm (NameSelection (name, ivs)) thms = 
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset

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

223 
val n = length thms; 
24793  224 
fun err msg = error (msg ^ " for " ^ quote name ^ " (length " ^ string_of_int n ^ ")"); 
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset

225 
fun select i = 
24793  226 
if i < 1 orelse i > n then err ("Bad subscript " ^ string_of_int i) 
227 
else nth thms (i  1); 

228 
val is = maps (interval n) ivs handle Fail msg => err msg; 

229 
in map select is end; 

15703  230 

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

231 

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

232 
(* selections *) 
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset

233 

16493  234 
fun selections (name, [thm]) = [(Name name, thm)] 
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset

235 
 selections (name, thms) = (1 upto length thms, thms) > ListPair.map (fn (i, thm) => 
16493  236 
(NameSelection (name, [Single i]), thm)); 
15456
956d6acacf89
Specific theorems in a named list of theorems can now be referred to
berghofe
parents:
15387
diff
changeset

237 

9564  238 

9808  239 
(* get_thm(s)_closure  statically scoped versions *) 
9564  240 

241 
(*beware of proper order of evaluation!*) 

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

242 

9564  243 
fun lookup_thms thy = 
244 
let 

16493  245 
val (space, thms) = #theorems (get_theorems thy); 
24137
8d7896398147
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
24029
diff
changeset

246 
val thy_ref = Theory.check_thy thy; 
9564  247 
in 
248 
fn name => 

17221  249 
Option.map (map (Thm.transfer (Theory.deref thy_ref))) (*dynamic identity*) 
17418  250 
(Symtab.lookup thms (NameSpace.intern space name)) (*static content*) 
9564  251 
end; 
3987  252 

9564  253 
fun get_thms_closure thy = 
16441  254 
let val closures = map lookup_thms (thy :: Theory.ancestors_of thy) in 
16493  255 
fn thmref => 
18031  256 
let val name = name_of_thmref thmref; 
16493  257 
in select_thm thmref (the_thms name (get_first (fn f => f name) closures)) end 
15456
956d6acacf89
Specific theorems in a named list of theorems can now be referred to
berghofe
parents:
15387
diff
changeset

258 
end; 
9564  259 

9808  260 
fun get_thm_closure thy = 
261 
let val get = get_thms_closure thy 

16493  262 
in fn thmref => single_thm (name_of_thmref thmref) (get thmref) end; 
9808  263 

9564  264 

16441  265 
(* get_thms etc. *) 
9564  266 

16493  267 
fun get_thms theory thmref = 
268 
let val name = name_of_thmref thmref in 

269 
get_first (fn thy => lookup_thms thy name) (theory :: Theory.ancestors_of theory) 

270 
> the_thms name > select_thm thmref > map (Thm.transfer theory) 

271 
end; 

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

272 

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

273 
fun get_thmss thy thmrefs = maps (get_thms thy) thmrefs; 
16493  274 
fun get_thm thy thmref = single_thm (name_of_thmref thmref) (get_thms thy thmref); 
4783  275 

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

276 

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

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

278 

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

279 
fun valid_thms thy (thmref, ths) = 
18678  280 
(case try (get_thms thy) thmref of 
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset

281 
NONE => false 
16132  282 
 SOME ths' => Thm.eq_thms (ths, ths')); 
3987  283 

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

284 
fun thms_containing theory spec = 
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset

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

286 
> maps (fn thy => 
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset

287 
FactIndex.find (fact_index_of thy) spec 
16493  288 
> List.filter (fn (name, ths) => valid_thms theory (Name name, ths)) 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19473
diff
changeset

289 
> distinct (eq_fst (op =))); 
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset

290 

13646  291 
fun thms_containing_consts thy consts = 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19473
diff
changeset

292 
thms_containing thy (consts, []) > maps #2 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

293 
> map (`(get_name_hint)); 
13646  294 

15882
a191d2bee3e1
new thms_containing that searches for patterns instead of constants
kleing
parents:
15801
diff
changeset

295 

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

297 

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

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

300 
in map (`(get_name_hint)) (maps snd (Symtab.dest thms)) end; 
15703  301 

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

302 
fun all_thms_of thy = maps thms_of (thy :: Theory.ancestors_of thy); 
16336  303 

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

304 

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

305 

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

306 
(** store theorems **) (*DESTRUCTIVE*) 
3987  307 

16441  308 
(* hiding  affects current theory node only *) 
12695  309 

23933  310 
fun hide_thms fully names thy = CRITICAL (fn () => 
12695  311 
let 
16493  312 
val r as ref {theorems = (space, thms), index} = get_theorems_ref thy; 
16132  313 
val space' = fold (NameSpace.hide fully) names space; 
23933  314 
in r := {theorems = (space', thms), index = index}; thy end); 
12695  315 

316 

21580  317 
(* fact specifications *) 
318 

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

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

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

322 

323 

4853  324 
(* naming *) 
325 

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

4853  328 

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

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

331 

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

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

333 
> (if Thm.get_name thm <> "" andalso pre orelse not official then I else Thm.put_name name) 
21964  334 
> (if has_name_hint thm andalso pre orelse name = "" then I else put_name_hint name); 
12872
0855c3ab2047
Theorems are only "prenamed" if the do not already have names.
berghofe
parents:
12711
diff
changeset

335 

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

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

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

338 

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

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

340 
burrow_fact (name_thms true official name) fact; 
4853  341 

342 

11998  343 
(* enter_thms *) 
4853  344 

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

345 
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

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

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

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

350 
let 
16441  351 
val name = Sign.full_name thy bname; 
352 
val (thy', thms') = apsnd (post_name name) (app_att (thy, pre_name name thms)); 

16513
f38693aad717
enter_thms: use theorem database of thy *after* attribute application;
wenzelm
parents:
16493
diff
changeset

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

354 
val space' = Sign.declare_name thy' name space; 
17418  355 
val theorems' = Symtab.update (name, thms') theorems; 
18031  356 
val index' = FactIndex.add_global (name, thms') index; 
13274  357 
in 
17418  358 
(case Symtab.lookup theorems name of 
15531  359 
NONE => () 
16441  360 
 SOME thms'' => 
361 
if Thm.eq_thms (thms', thms'') then warn_same name 

13274  362 
else warn_overwrite name); 
16336  363 
r := {theorems = (space', theorems'), index = index'}; 
18418
bf448d999b7e
rearranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18377
diff
changeset

364 
(thms', thy') 
23933  365 
end); 
3987  366 

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

367 

6091  368 
(* add_thms(s) *) 
4853  369 

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

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

372 
(foldl_map (Thm.theory_attributes atts)) (bname, thms); 
4853  373 

18377  374 
fun gen_add_thmss pre_name = 
375 
fold_map (add_thms_atts pre_name); 

5907  376 

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

377 
fun gen_add_thms pre_name args = 
18377  378 
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

379 

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

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

381 
val add_thms = gen_add_thms (name_thms true true); 
5907  382 

383 

14564  384 
(* note_thmss(_i) *) 
5907  385 

9192  386 
local 
12711  387 

18801  388 
fun gen_note_thmss get k = fold_map (fn ((bname, more_atts), ths_atts) => fn thy => 
12711  389 
let 
18728  390 
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

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

392 
(name_thmss true) (name_thms false true) (apsnd flat o foldl_map app) 
18801  393 
(bname, map (fn (ths, atts) => (get thy ths, atts @ more_atts @ [kind k])) ths_atts); 
394 
in ((bname, thms), thy') end); 

12711  395 

9192  396 
in 
12711  397 

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

398 
val note_thmss = gen_note_thmss get_thms; 
bf448d999b7e
rearranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18377
diff
changeset

399 
val note_thmss_i = gen_note_thmss (K I); 
12711  400 

21438  401 
end; 
402 

18801  403 
fun note_thmss_qualified k path facts thy = 
404 
thy 

22796  405 
> Sign.add_path path 
406 
> Sign.no_base_names 

18801  407 
> note_thmss_i k facts 
22796  408 
> Sign.restore_naming thy; 
18801  409 

5280  410 

6091  411 
(* store_thm *) 
5280  412 

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

414 
let val ([th'], thy') = add_thms_atts (name_thms true true) ((bname, [thm]), atts) thy 
18358  415 
in (th', thy') end; 
3987  416 

417 

16441  418 
(* smart_store_thms(_open) *) 
3987  419 

16441  420 
local 
421 

422 
fun smart_store _ (name, []) = 

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

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

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

425 
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

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

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

428 
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

429 
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

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

431 

16441  432 
in 
433 

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

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

435 
val smart_store_thms_open = smart_store false; 
16441  436 

437 
end; 

3987  438 

439 

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

440 
(* forall_elim_var(s)  belongs to drule.ML *) 
7899  441 

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

442 
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

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

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

447 
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

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

449 
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

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

451 
in fold Thm.forall_elim cvars th end; 
7899  452 

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

453 
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

454 

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

455 
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

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

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

459 

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

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

461 

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

18377  465 
fun add_single add ((name, ax), atts) thy = 
4853  466 
let 
11998  467 
val named_ax = [(name, ax)]; 
7753  468 
val thy' = add named_ax thy; 
469 
val thm = hd (get_axs thy' named_ax); 

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

7753  472 
let 
473 
val named_axs = name_multi name axs; 

4853  474 
val thy' = add named_axs thy; 
7753  475 
val thms = get_axs thy' named_axs; 
18377  476 
in apfst hd (gen_add_thmss (K I) [((name, thms), atts)] thy') end; 
477 
fun add_singles add = fold_map (add_single add); 

478 
fun add_multis add = fold_map (add_multi add); 

4853  479 
in 
19629  480 
val add_axioms = add_singles Theory.add_axioms; 
481 
val add_axioms_i = add_singles Theory.add_axioms_i; 

482 
val add_axiomss = add_multis Theory.add_axioms; 

483 
val add_axiomss_i = add_multis Theory.add_axioms_i; 

22796  484 
val add_defs = add_singles o Theory.add_defs false; 
485 
val add_defs_i = add_singles o Theory.add_defs_i false; 

486 
val add_defs_unchecked = add_singles o Theory.add_defs true; 

487 
val add_defs_unchecked_i = add_singles o Theory.add_defs_i true; 

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

489 

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

490 

24434  491 
(* simple interface for simple definitions *) 
492 

493 
fun simple_def (raw_name, atts) (((raw_c, ty, syn), ts), t) thy = 

494 
let 

495 
val c = Sign.full_name thy raw_c; 

496 
val name = if raw_name = "" then Thm.def_name raw_c else raw_name; 

497 
val def = Logic.mk_equals (list_comb (Const (c, ty), ts), t); 

498 
in 

499 
thy 

24770
695a8e087b9f
Sign.add_consts_authentic: tags (Markup.property list);
wenzelm
parents:
24713
diff
changeset

500 
> Sign.add_consts_authentic [] [(raw_c, ty, syn)] 
24434  501 
> add_defs_i false [((name, def), atts)] 
502 
> (fn [thm] => pair (c, thm)) 

503 
end; 

504 

505 

3987  506 

5091  507 
(*** the ProtoPure theory ***) 
3987  508 

24243  509 
val typ = SimpleSyntax.read_typ; 
510 
val term = SimpleSyntax.read_term; 

511 
val prop = SimpleSyntax.read_prop; 

512 

513 
val appl_syntax = 

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

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

516 

517 
val applC_syntax = 

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

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

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

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

16441  522 

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

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

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

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

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

531 
("dummy", 0, NoSyn)] 
22796  532 
> Sign.add_nonterminals Syntax.basic_nonterms 
24243  533 
> Sign.add_syntax_i 
534 
[("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3%_./ _)", [0, 3], 3)), 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

571 
> Sign.add_syntax_i appl_syntax 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

587 
> Sign.add_modesyntax_i ("", false) 

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

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

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

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

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

593 
> Sign.add_consts_i 

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

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

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

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

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

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

14223
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
13800
diff
changeset

600 
> Theory.add_finals_i false 
24243  601 
[Const ("==", typ "'a => 'a => prop"), 
602 
Const ("==>", typ "prop => prop => prop"), 

603 
Const ("all", typ "('a => prop) => prop"), 

604 
Const ("TYPE", typ "'a itself"), 

605 
Const (Term.dummy_patternN, typ "'a")] 

22796  606 
> Sign.add_trfuns Syntax.pure_trfuns 
607 
> Sign.add_trfunsT Syntax.pure_trfunsT 

16441  608 
> Sign.local_path 
24243  609 
> Sign.add_consts_i 
610 
[("term", typ "'a => prop", NoSyn), 

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

612 
> (add_defs_i false o map Thm.no_attributes) 

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

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

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

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

618 
> Theory.add_axioms_i Proofterm.equality_axms 
16493  619 
> Theory.end_theory; 
3987  620 

5091  621 
structure ProtoPure = 
622 
struct 

623 
val thy = proto_pure; 

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

626 
val conjunction_def = get_axiom thy "conjunction_def"; 
5091  627 
end; 
3987  628 

629 
end; 

630 

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

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

632 
open BasicPureThy; 