author  wenzelm 
Mon, 17 Mar 2008 20:51:16 +0100  
changeset 26308  73d68876ba46 
parent 26292  009e56d16080 
child 26319  f512d78e6687 
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 
25981  37 
val get_group: thm > string option 
38 
val put_group: string > thm > thm 

39 
val group: string > attribute 

22251  40 
val has_kind: thm > bool 
18801  41 
val get_kind: thm > string 
42 
val kind_rule: string > thm > thm 

43 
val kind: string > attribute 

44 
val kind_internal: attribute 

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

47 
val string_of_thmref: thmref > string 
9564  48 
val single_thm: string > thm list > thm 
16493  49 
val name_of_thmref: thmref > string 
50 
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

51 
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

52 
val selections: string * thm list > (thmref * thm) list 
17162  53 
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

54 
val all_facts_of: theory > Facts.T 
16336  55 
val thms_of: theory > (string * thm) list 
56 
val all_thms_of: theory > (string * thm) list 

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

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

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

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

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

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

68 
val smart_store_thms_open: (bstring * thm list) > thm list 
7899  69 
val forall_elim_var: int > thm > thm 
70 
val forall_elim_vars: int > thm > thm 

18728  71 
val add_thms: ((bstring * thm) * attribute list) list > theory > thm list * theory 
24965  72 
val add_thmss: ((bstring * thm list) * attribute list) list > theory > thm list list * theory 
25598  73 
val note: string > string * thm > theory > thm * theory 
18801  74 
val note_thmss: string > ((bstring * attribute list) * 
18728  75 
(thmref * attribute list) list) list > theory > (bstring * thm list) list * theory 
18801  76 
val note_thmss_i: string > ((bstring * attribute list) * 
77 
(thm list * attribute list) list) list > theory > (bstring * thm list) list * theory 

25981  78 
val note_thmss_grouped: string > string > ((bstring * attribute list) * 
79 
(thm list * attribute list) list) list > theory > (bstring * thm list) list * theory 

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

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

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

85 
theory > thm list list * theory 

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

87 
theory > thm list list * theory 

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

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

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

95 
theory > thm list * theory 

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

3987  98 
end; 
99 

100 
structure PureThy: PURE_THY = 

101 
struct 

102 

103 

18801  104 
(*** theorem tags ***) 
105 

106 
(* add / delete tags *) 

107 

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

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

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

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

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

113 

114 

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

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

116 

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

119 
val has_name_hint = can the_name_hint; 

120 
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

121 

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

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

124 

25981  125 
(* theorem groups *) 
126 

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

128 

129 
fun put_group name = 

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

131 

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

133 

134 

18801  135 
(* theorem kinds *) 
136 

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

139 
val has_kind = can the_kind; 

25981  140 
val get_kind = the_default "" o try the_kind; 
18801  141 

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

146 
val is_internal = has_internal o Thm.get_tags; 
18801  147 

148 

149 

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

150 
(*** theorem database ***) 
3987  151 

16441  152 
(** dataype theorems **) 
3987  153 

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

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

156 
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

157 

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

159 

16441  160 
structure TheoremsData = TheoryDataFun 
24713  161 
( 
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

162 
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

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

165 
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

166 
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

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

168 
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

169 
ref (make_thms NameSpace.empty_table (Facts.merge (all_facts1, all_facts2))); 
24713  170 
); 
3987  171 

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

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

175 
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

176 

6367  177 

3987  178 

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

179 
(** retrieve theorems **) 
3987  180 

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

4037  183 

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

186 

15703  187 

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

188 
(* datatype interval *) 
15703  189 

190 
datatype interval = 

191 
FromTo of int * int  

192 
From of int  

193 
Single of int; 

194 

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

195 
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

196 
 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

197 
 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

198 

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

201 
(case iv of 

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

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

204 
 Single i => [i]) 

205 
end; 

206 

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

207 

16493  208 
(* datatype thmref *) 
209 

210 
datatype thmref = 

211 
Name of string  

18031  212 
NameSelection of string * interval list  
213 
Fact of string; 

15703  214 

16493  215 
fun name_of_thmref (Name name) = name 
18031  216 
 name_of_thmref (NameSelection (name, _)) = name 
18678  217 
 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

218 

16493  219 
fun map_name_of_thmref f (Name name) = Name (f name) 
18031  220 
 map_name_of_thmref f (NameSelection (name, is)) = NameSelection (f name, is) 
221 
 map_name_of_thmref _ thmref = thmref; 

16493  222 

223 
fun string_of_thmref (Name name) = name 

224 
 string_of_thmref (NameSelection (name, is)) = 

18031  225 
name ^ enclose "(" ")" (commas (map string_of_interval is)) 
18678  226 
 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

227 

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

228 

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

229 
(* select_thm *) 
15703  230 

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

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

235 
val n = length thms; 
24793  236 
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

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

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

241 
in map select is end; 

15703  242 

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

243 

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

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

245 

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

247 
 selections (name, thms) = (1 upto length thms, thms) > ListPair.map (fn (i, thm) => 
16493  248 
(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

249 

9564  250 

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

251 
(* lookup/get thms *) 
4922
03b81b6e1baa
added thms_closure: theory > xstring > tthm list option;
wenzelm
parents:
4853
diff
changeset

252 

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

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

254 

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

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

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

259 
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

260 

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

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

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

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

264 
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

265 
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

266 

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

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

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

269 

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

270 
in 
3987  271 

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

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

274 
val name = name_of_thmref thmref; 
009e56d16080
get_thm(s): check facts lookup vs. old thm database;
wenzelm
parents:
26282
diff
changeset

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

276 
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

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

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

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

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

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

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

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

284 
else legacy_feature ("Fact lookup differs from oldstyle thm database:\n" ^ 
009e56d16080
get_thm(s): check facts lookup vs. old thm database;
wenzelm
parents:
26282
diff
changeset

285 
show_result new_res ^ " vs " ^ show_result old_res ^ 
009e56d16080
get_thm(s): check facts lookup vs. old thm database;
wenzelm
parents:
26282
diff
changeset

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

287 
in Option.map #2 old_res > the_thms name > select_thm thmref > map (Thm.transfer theory) end; 
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset

288 

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

289 
fun get_thmss thy thmrefs = maps (get_thms thy) thmrefs; 
16493  290 
fun get_thm thy thmref = single_thm (name_of_thmref thmref) (get_thms thy thmref); 
4783  291 

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

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

293 

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

294 

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

296 

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

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

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

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

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

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

303 

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 
(** store theorems **) (*DESTRUCTIVE*) 
3987  306 

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

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

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

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

315 

21580  316 
(* fact specifications *) 
317 

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

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

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

321 

322 

4853  323 
(* naming *) 
324 

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

4853  327 

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

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

330 

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

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

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

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

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

353 
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

354 
val space' = Sign.declare_name thy' name space; 
17418  355 
val theorems' = Symtab.update (name, thms') theorems; 
26308  356 
val all_facts' = Facts.add_global (Sign.naming_of thy') (name, thms') all_facts; 
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); 
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

363 
r := make_thms (space', theorems') all_facts'; 
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 

25981  388 
fun gen_note_thmss get tag = 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) 
25981  393 
(bname, map (fn (ths, atts) => (get thy ths, surround tag (atts @ more_atts))) ths_atts); 
18801  394 
in ((bname, thms), thy') end); 
12711  395 

9192  396 
in 
12711  397 

25981  398 
fun note_thmss k = gen_note_thmss get_thms (kind k); 
399 
fun note_thmss_i k = gen_note_thmss (K I) (kind k); 

400 
fun note_thmss_grouped k g = gen_note_thmss (K I) (kind k #> group g); 

12711  401 

21438  402 
end; 
403 

25598  404 
fun note kind (name, thm) = 
405 
note_thmss_i kind [((name, []), [([thm], [])])] 

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

407 

18801  408 
fun note_thmss_qualified k path facts thy = 
409 
thy 

22796  410 
> Sign.add_path path 
411 
> Sign.no_base_names 

18801  412 
> note_thmss_i k facts 
22796  413 
> Sign.restore_naming thy; 
18801  414 

5280  415 

6091  416 
(* store_thm *) 
5280  417 

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

419 
let val ([th'], thy') = add_thms_atts (name_thms true true) ((bname, [thm]), atts) thy 
18358  420 
in (th', thy') end; 
3987  421 

422 

16441  423 
(* smart_store_thms(_open) *) 
3987  424 

16441  425 
local 
426 

427 
fun smart_store _ (name, []) = 

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

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

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

430 
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

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

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

433 
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

434 
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

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

436 

16441  437 
in 
438 

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

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

440 
val smart_store_thms_open = smart_store false; 
16441  441 

442 
end; 

3987  443 

444 

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

445 
(* forall_elim_var(s)  belongs to drule.ML *) 
7899  446 

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

447 
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

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

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

452 
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

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

454 
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

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

456 
in fold Thm.forall_elim cvars th end; 
7899  457 

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

458 
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

459 

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

460 
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

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

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

464 

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

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

466 

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

18377  470 
fun add_single add ((name, ax), atts) thy = 
4853  471 
let 
11998  472 
val named_ax = [(name, ax)]; 
7753  473 
val thy' = add named_ax thy; 
474 
val thm = hd (get_axs thy' named_ax); 

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

7753  477 
let 
478 
val named_axs = name_multi name axs; 

4853  479 
val thy' = add named_axs thy; 
7753  480 
val thms = get_axs thy' named_axs; 
18377  481 
in apfst hd (gen_add_thmss (K I) [((name, thms), atts)] thy') end; 
482 
fun add_singles add = fold_map (add_single add); 

483 
fun add_multis add = fold_map (add_multi add); 

4853  484 
in 
19629  485 
val add_axioms = add_singles Theory.add_axioms; 
486 
val add_axioms_i = add_singles Theory.add_axioms_i; 

487 
val add_axiomss = add_multis Theory.add_axioms; 

488 
val add_axiomss_i = add_multis Theory.add_axioms_i; 

22796  489 
val add_defs = add_singles o Theory.add_defs false; 
490 
val add_defs_i = add_singles o Theory.add_defs_i false; 

491 
val add_defs_unchecked = add_singles o Theory.add_defs true; 

492 
val add_defs_unchecked_i = add_singles o Theory.add_defs_i true; 

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

494 

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

495 

3987  496 

5091  497 
(*** the ProtoPure theory ***) 
3987  498 

24243  499 
val typ = SimpleSyntax.read_typ; 
500 
val term = SimpleSyntax.read_term; 

501 
val prop = SimpleSyntax.read_prop; 

502 

503 
val appl_syntax = 

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

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

506 

507 
val applC_syntax = 

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

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

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

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

16441  512 

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

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

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

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

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

521 
("dummy", 0, NoSyn)] 
22796  522 
> Sign.add_nonterminals Syntax.basic_nonterms 
24243  523 
> Sign.add_syntax_i 
524 
[("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3%_./ _)", [0, 3], 3)), 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

561 
> Sign.add_syntax_i appl_syntax 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

577 
> Sign.add_modesyntax_i ("", false) 

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

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

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

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

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

583 
> Sign.add_consts_i 

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

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

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

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

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

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

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

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

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

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

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

594 
> Theory.add_deps Term.dummy_patternN (Term.dummy_patternN, typ "'a") [] 
22796  595 
> Sign.add_trfuns Syntax.pure_trfuns 
596 
> Sign.add_trfunsT Syntax.pure_trfunsT 

16441  597 
> Sign.local_path 
24243  598 
> Sign.add_consts_i 
599 
[("term", typ "'a => prop", NoSyn), 

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

601 
> (add_defs_i false o map Thm.no_attributes) 

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

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

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

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

607 
> Theory.add_axioms_i Proofterm.equality_axms 
16493  608 
> Theory.end_theory; 
3987  609 

5091  610 
structure ProtoPure = 
611 
struct 

612 
val thy = proto_pure; 

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

615 
val conjunction_def = get_axiom thy "conjunction_def"; 
5091  616 
end; 
3987  617 

618 
end; 

619 

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

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

621 
open BasicPureThy; 