author  wenzelm 
Sat, 30 Dec 2006 16:08:04 +0100  
changeset 21964  df2e82888a66 
parent 21646  c07b5b0e8492 
child 22086  cf6019fece63 
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 
17930
e7160d70be1f
added thm(s) retrieval functions (from goals.ML);
wenzelm
parents:
17703
diff
changeset

18 
val thm: xstring > thm 
e7160d70be1f
added thm(s) retrieval functions (from goals.ML);
wenzelm
parents:
17703
diff
changeset

19 
val thms: xstring > thm list 
5091  20 
structure ProtoPure: 
21 
sig 

22 
val thy: theory 

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

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

28 

3987  29 
signature PURE_THY = 
30 
sig 

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

31 
include BASIC_PURE_THY 
18801  32 
val tag_rule: tag > thm > thm 
33 
val untag_rule: string > thm > thm 

34 
val tag: tag > attribute 

35 
val untag: string > attribute 

21964  36 
val has_name_hint: thm > bool 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

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

38 
val put_name_hint: string > thm > thm 
18801  39 
val get_kind: thm > string 
40 
val kind_rule: string > thm > thm 

41 
val kind: string > attribute 

42 
val kind_internal: attribute 

43 
val has_internal: tag list > bool 

44 
val is_internal: thm > bool 

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

45 
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

46 
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

47 
val get_thms_closure: theory > thmref > thm list 
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 
54 
val theorem_space: theory > NameSpace.T 

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

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

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

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

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

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

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

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

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

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

72 
val smart_store_thms_open: (bstring * thm list) > thm list 
7899  73 
val forall_elim_var: int > thm > thm 
74 
val forall_elim_vars: int > thm > thm 

18728  75 
val add_thms: ((bstring * thm) * attribute list) list > theory > thm list * theory 
76 
val add_thmss: ((bstring * thm list) * attribute list) list > theory > thm list list * theory 

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

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

18728  82 
(thm list * attribute list) list) list > theory > (bstring * thm list) list * theory 
83 
val add_axioms: ((bstring * string) * attribute list) list > theory > thm list * theory 

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

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

86 
theory > thm list list * theory 

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

88 
theory > thm list list * theory 

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 

18728  97 
val add_defss: bool > ((bstring * string list) * attribute list) list > 
18377  98 
theory > thm list list * theory 
18728  99 
val add_defss_i: bool > ((bstring * term list) * attribute list) list > 
18358  100 
theory > thm list list * theory 
18666
f37a43cec547
generic_setup: optional argument, defaults to Context.setup();
wenzelm
parents:
18614
diff
changeset

101 
val generic_setup: string option > theory > theory 
17342
92504e2f6c07
added generic_setup, add_oracle (from isar_thy.ML);
wenzelm
parents:
17221
diff
changeset

102 
val add_oracle: bstring * string * string > theory > theory 
3987  103 
end; 
104 

105 
structure PureThy: PURE_THY = 

106 
struct 

107 

108 

18801  109 
(*** theorem tags ***) 
110 

111 
(* add / delete tags *) 

112 

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

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

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

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

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

118 

119 
fun simple_tag name x = tag (name, []) x; 

120 

121 

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

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

123 

21964  124 
fun has_name_hint thm = AList.defined (op =) (Thm.get_tags thm) "name"; 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

125 

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

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

127 
(case AList.lookup (op =) (Thm.get_tags thm) "name" of 
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

128 
SOME (k :: _) => k 
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

129 
 _ => "??.unknown"); 
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

130 

21964  131 
fun put_name_hint name = untag_rule "name" #> tag_rule ("name", [name]); 
132 

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

133 

18801  134 
(* theorem kinds *) 
135 

136 
fun get_kind thm = 

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

137 
(case AList.lookup (op =) (Thm.get_tags thm) "kind" of 
18801  138 
SOME (k :: _) => k 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21606
diff
changeset

139 
 _ => "??.unknown"); 
18801  140 

141 
fun kind_rule k = tag_rule ("kind", [k]) o untag_rule "kind"; 

142 
fun kind k x = if k = "" then x else Thm.rule_attribute (K (kind_rule k)) x; 

143 
fun kind_internal x = kind internalK x; 

144 
fun has_internal tags = exists (fn ("kind", [k]) => k = internalK  _ => false) tags; 

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

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

147 

148 

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

149 
(*** theorem database ***) 
3987  150 

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

16441  153 
structure TheoremsData = TheoryDataFun 
154 
(struct 

5005  155 
val name = "Pure/theorems"; 
156 
type T = 

16441  157 
{theorems: thm list NameSpace.table, 
158 
index: FactIndex.T} ref; 

3987  159 

4853  160 
fun mk_empty _ = 
16336  161 
ref {theorems = NameSpace.empty_table, index = FactIndex.empty}: T; 
3987  162 

5005  163 
val empty = mk_empty (); 
6547  164 
fun copy (ref x) = ref x; 
16441  165 
val extend = mk_empty; 
166 
fun merge _ = mk_empty; 

19426
b9289b560446
moved print_theorems/theory to Isar/proof_display.ML;
wenzelm
parents:
19391
diff
changeset

167 
fun print _ _ = (); 
16441  168 
end); 
3987  169 

16493  170 
val get_theorems_ref = TheoremsData.get; 
171 
val get_theorems = ! o get_theorems_ref; 

17162  172 
val theorems_of = #theorems o get_theorems; 
173 
val theorem_space = #1 o theorems_of; 

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

175 

6367  176 

3987  177 

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

178 
(** retrieve theorems **) 
3987  179 

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

4037  182 

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

185 

15703  186 

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

187 
(* datatype interval *) 
15703  188 

189 
datatype interval = 

190 
FromTo of int * int  

191 
From of int  

192 
Single of int; 

193 

194 
fun interval _ (FromTo (i, j)) = i upto j 

195 
 interval n (From i) = i upto n 

196 
 interval _ (Single i) = [i]; 

197 

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

198 
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

199 
 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

200 
 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

201 

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

202 

16493  203 
(* datatype thmref *) 
204 

205 
datatype thmref = 

206 
Name of string  

18031  207 
NameSelection of string * interval list  
208 
Fact of string; 

15703  209 

16493  210 
fun name_of_thmref (Name name) = name 
18031  211 
 name_of_thmref (NameSelection (name, _)) = name 
18678  212 
 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

213 

16493  214 
fun map_name_of_thmref f (Name name) = Name (f name) 
18031  215 
 map_name_of_thmref f (NameSelection (name, is)) = NameSelection (f name, is) 
216 
 map_name_of_thmref _ thmref = thmref; 

16493  217 

218 
fun string_of_thmref (Name name) = name 

219 
 string_of_thmref (NameSelection (name, is)) = 

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

222 

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

223 

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

224 
(* select_thm *) 
15703  225 

16493  226 
fun select_thm (Name _) thms = thms 
18031  227 
 select_thm (Fact _) thms = thms 
16493  228 
 select_thm (NameSelection (name, is)) thms = 
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset

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

230 
val n = length thms; 
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset

231 
fun select i = 
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset

232 
if i < 1 orelse i > n then 
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset

233 
error ("Bad subscript " ^ string_of_int i ^ " for " ^ 
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset

234 
quote name ^ " (length " ^ string_of_int n ^ ")") 
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset

235 
else List.nth (thms, i  1); 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19473
diff
changeset

236 
in map select (maps (interval n) is) end; 
15703  237 

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

238 

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

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

240 

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

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

244 

9564  245 

9808  246 
(* get_thm(s)_closure  statically scoped versions *) 
9564  247 

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

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

249 

9564  250 
fun lookup_thms thy = 
251 
let 

16441  252 
val thy_ref = Theory.self_ref thy; 
16493  253 
val (space, thms) = #theorems (get_theorems thy); 
9564  254 
in 
255 
fn name => 

17221  256 
Option.map (map (Thm.transfer (Theory.deref thy_ref))) (*dynamic identity*) 
17418  257 
(Symtab.lookup thms (NameSpace.intern space name)) (*static content*) 
9564  258 
end; 
3987  259 

9564  260 
fun get_thms_closure thy = 
16441  261 
let val closures = map lookup_thms (thy :: Theory.ancestors_of thy) in 
16493  262 
fn thmref => 
18031  263 
let val name = name_of_thmref thmref; 
16493  264 
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

265 
end; 
9564  266 

9808  267 
fun get_thm_closure thy = 
268 
let val get = get_thms_closure thy 

16493  269 
in fn thmref => single_thm (name_of_thmref thmref) (get thmref) end; 
9808  270 

9564  271 

16441  272 
(* get_thms etc. *) 
9564  273 

16493  274 
fun get_thms theory thmref = 
275 
let val name = name_of_thmref thmref in 

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

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

278 
end; 

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

279 

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

280 
fun get_thmss thy thmrefs = maps (get_thms thy) thmrefs; 
16493  281 
fun get_thm thy thmref = single_thm (name_of_thmref thmref) (get_thms thy thmref); 
4783  282 

17930
e7160d70be1f
added thm(s) retrieval functions (from goals.ML);
wenzelm
parents:
17703
diff
changeset

283 
fun thm name = get_thm (the_context ()) (Name name); 
e7160d70be1f
added thm(s) retrieval functions (from goals.ML);
wenzelm
parents:
17703
diff
changeset

284 
fun thms name = get_thms (the_context ()) (Name name); 
e7160d70be1f
added thm(s) retrieval functions (from goals.ML);
wenzelm
parents:
17703
diff
changeset

285 

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

286 

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

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

288 

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

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

291 
NONE => false 
16132  292 
 SOME ths' => Thm.eq_thms (ths, ths')); 
3987  293 

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

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

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

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

297 
FactIndex.find (fact_index_of thy) spec 
16493  298 
> 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

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

300 

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

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

303 
> map (`(get_name_hint)); 
13646  304 

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

305 

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

307 

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

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

310 
in map (`(get_name_hint)) (maps snd (Symtab.dest thms)) end; 
15703  311 

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

312 
fun all_thms_of thy = maps thms_of (thy :: Theory.ancestors_of thy); 
16336  313 

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

314 

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

315 

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

316 
(** store theorems **) (*DESTRUCTIVE*) 
3987  317 

16441  318 
(* hiding  affects current theory node only *) 
12695  319 

13424  320 
fun hide_thms fully names thy = 
12695  321 
let 
16493  322 
val r as ref {theorems = (space, thms), index} = get_theorems_ref thy; 
16132  323 
val space' = fold (NameSpace.hide fully) names space; 
16336  324 
in r := {theorems = (space', thms), index = index}; thy end; 
12695  325 

326 

21580  327 
(* fact specifications *) 
328 

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

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

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

332 

333 

4853  334 
(* naming *) 
335 

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

4853  338 

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

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

341 

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

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

343 
> (if Thm.get_name thm <> "" andalso pre orelse not official then I else Thm.put_name name) 
21964  344 
> (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

345 

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

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

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

348 

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

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

350 
burrow_fact (name_thms true official name) fact; 
4853  351 

352 

11998  353 
(* enter_thms *) 
4853  354 

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

355 
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

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

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

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

360 
let 
16441  361 
val name = Sign.full_name thy bname; 
362 
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

363 
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

364 
val space' = Sign.declare_name thy' name space; 
17418  365 
val theorems' = Symtab.update (name, thms') theorems; 
18031  366 
val index' = FactIndex.add_global (name, thms') index; 
13274  367 
in 
17418  368 
(case Symtab.lookup theorems name of 
15531  369 
NONE => () 
16441  370 
 SOME thms'' => 
371 
if Thm.eq_thms (thms', thms'') then warn_same name 

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

374 
(thms', thy') 
11998  375 
end; 
3987  376 

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

377 

6091  378 
(* add_thms(s) *) 
4853  379 

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

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

382 
(foldl_map (Thm.theory_attributes atts)) (bname, thms); 
4853  383 

18377  384 
fun gen_add_thmss pre_name = 
385 
fold_map (add_thms_atts pre_name); 

5907  386 

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

387 
fun gen_add_thms pre_name args = 
18377  388 
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

389 

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

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

391 
val add_thms = gen_add_thms (name_thms true true); 
5907  392 

393 

14564  394 
(* note_thmss(_i) *) 
5907  395 

9192  396 
local 
12711  397 

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

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

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

12711  405 

9192  406 
in 
12711  407 

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

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

409 
val note_thmss_i = gen_note_thmss (K I); 
12711  410 

21438  411 
end; 
412 

18801  413 
fun note_thmss_qualified k path facts thy = 
414 
thy 

415 
> Theory.add_path path 

416 
> Theory.no_base_names 

417 
> note_thmss_i k facts 

418 
> Theory.restore_naming thy; 

419 

5280  420 

6091  421 
(* store_thm *) 
5280  422 

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

424 
let val ([th'], thy') = add_thms_atts (name_thms true true) ((bname, [thm]), atts) thy 
18358  425 
in (th', thy') end; 
3987  426 

427 

16441  428 
(* smart_store_thms(_open) *) 
3987  429 

16441  430 
local 
431 

432 
fun smart_store _ (name, []) = 

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

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

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

435 
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

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

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

438 
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

439 
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

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

441 

16441  442 
in 
443 

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

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

445 
val smart_store_thms_open = smart_store false; 
16441  446 

447 
end; 

3987  448 

449 

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

450 
(* forall_elim_var(s)  belongs to drule.ML *) 
7899  451 

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

452 
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

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

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

457 
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

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

459 
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

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

461 
in fold Thm.forall_elim cvars th end; 
7899  462 

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

463 
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

464 

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

465 
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

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

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

469 

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

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

471 

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

18377  475 
fun add_single add ((name, ax), atts) thy = 
4853  476 
let 
11998  477 
val named_ax = [(name, ax)]; 
7753  478 
val thy' = add named_ax thy; 
479 
val thm = hd (get_axs thy' named_ax); 

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

7753  482 
let 
483 
val named_axs = name_multi name axs; 

4853  484 
val thy' = add named_axs thy; 
7753  485 
val thms = get_axs thy' named_axs; 
18377  486 
in apfst hd (gen_add_thmss (K I) [((name, thms), atts)] thy') end; 
487 
fun add_singles add = fold_map (add_single add); 

488 
fun add_multis add = fold_map (add_multi add); 

4853  489 
in 
19629  490 
val add_axioms = add_singles Theory.add_axioms; 
491 
val add_axioms_i = add_singles Theory.add_axioms_i; 

492 
val add_axiomss = add_multis Theory.add_axioms; 

493 
val add_axiomss_i = add_multis Theory.add_axioms_i; 

494 
val add_defs = add_singles o (Theory.add_defs false); 

495 
val add_defs_i = add_singles o (Theory.add_defs_i false); 

496 
val add_defs_unchecked = add_singles o (Theory.add_defs true); 

497 
val add_defs_unchecked_i = add_singles o (Theory.add_defs_i true); 

498 
val add_defss = add_multis o (Theory.add_defs false); 

499 
val add_defss_i = add_multis o (Theory.add_defs_i false); 

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

501 

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

502 

3987  503 

17342
92504e2f6c07
added generic_setup, add_oracle (from isar_thy.ML);
wenzelm
parents:
17221
diff
changeset

504 
(*** ML setup ***) 
92504e2f6c07
added generic_setup, add_oracle (from isar_thy.ML);
wenzelm
parents:
17221
diff
changeset

505 

92504e2f6c07
added generic_setup, add_oracle (from isar_thy.ML);
wenzelm
parents:
17221
diff
changeset

506 
(* generic_setup *) 
92504e2f6c07
added generic_setup, add_oracle (from isar_thy.ML);
wenzelm
parents:
17221
diff
changeset

507 

18713  508 
fun generic_setup NONE = (fn thy => thy > Context.setup ()) 
509 
 generic_setup (SOME txt) = Context.use_let "val setup: theory > theory" "setup" txt; 

17342
92504e2f6c07
added generic_setup, add_oracle (from isar_thy.ML);
wenzelm
parents:
17221
diff
changeset

510 

92504e2f6c07
added generic_setup, add_oracle (from isar_thy.ML);
wenzelm
parents:
17221
diff
changeset

511 

92504e2f6c07
added generic_setup, add_oracle (from isar_thy.ML);
wenzelm
parents:
17221
diff
changeset

512 
(* add_oracle *) 
92504e2f6c07
added generic_setup, add_oracle (from isar_thy.ML);
wenzelm
parents:
17221
diff
changeset

513 

92504e2f6c07
added generic_setup, add_oracle (from isar_thy.ML);
wenzelm
parents:
17221
diff
changeset

514 
fun add_oracle (name, T, oracle) = 
92504e2f6c07
added generic_setup, add_oracle (from isar_thy.ML);
wenzelm
parents:
17221
diff
changeset

515 
let val txt = 
92504e2f6c07
added generic_setup, add_oracle (from isar_thy.ML);
wenzelm
parents:
17221
diff
changeset

516 
"local\n\ 
92504e2f6c07
added generic_setup, add_oracle (from isar_thy.ML);
wenzelm
parents:
17221
diff
changeset

517 
\ type T = " ^ T ^ ";\n\ 
92504e2f6c07
added generic_setup, add_oracle (from isar_thy.ML);
wenzelm
parents:
17221
diff
changeset

518 
\ val oracle: theory > T > term = " ^ oracle ^ ";\n\ 
92504e2f6c07
added generic_setup, add_oracle (from isar_thy.ML);
wenzelm
parents:
17221
diff
changeset

519 
\ val name = " ^ quote name ^ ";\n\ 
92504e2f6c07
added generic_setup, add_oracle (from isar_thy.ML);
wenzelm
parents:
17221
diff
changeset

520 
\ exception Arg of T;\n\ 
92504e2f6c07
added generic_setup, add_oracle (from isar_thy.ML);
wenzelm
parents:
17221
diff
changeset

521 
\ val _ = Context.>> (Theory.add_oracle (name, fn (thy, Arg x) => oracle thy x));\n\ 
92504e2f6c07
added generic_setup, add_oracle (from isar_thy.ML);
wenzelm
parents:
17221
diff
changeset

522 
\ val thy = Context.the_context ();\n\ 
92504e2f6c07
added generic_setup, add_oracle (from isar_thy.ML);
wenzelm
parents:
17221
diff
changeset

523 
\ val invoke_" ^ name ^ " = Thm.invoke_oracle_i thy (Sign.full_name thy name);\n\ 
92504e2f6c07
added generic_setup, add_oracle (from isar_thy.ML);
wenzelm
parents:
17221
diff
changeset

524 
\in\n\ 
92504e2f6c07
added generic_setup, add_oracle (from isar_thy.ML);
wenzelm
parents:
17221
diff
changeset

525 
\ fun " ^ name ^ " thy x = invoke_" ^ name ^ " (thy, Arg x);\n\ 
92504e2f6c07
added generic_setup, add_oracle (from isar_thy.ML);
wenzelm
parents:
17221
diff
changeset

526 
\end;\n"; 
92504e2f6c07
added generic_setup, add_oracle (from isar_thy.ML);
wenzelm
parents:
17221
diff
changeset

527 
in Context.use_mltext_theory txt false end; 
92504e2f6c07
added generic_setup, add_oracle (from isar_thy.ML);
wenzelm
parents:
17221
diff
changeset

528 

92504e2f6c07
added generic_setup, add_oracle (from isar_thy.ML);
wenzelm
parents:
17221
diff
changeset

529 

92504e2f6c07
added generic_setup, add_oracle (from isar_thy.ML);
wenzelm
parents:
17221
diff
changeset

530 

5091  531 
(*** the ProtoPure theory ***) 
3987  532 

16441  533 
val aT = TFree ("'a", []); 
534 
val A = Free ("A", propT); 

535 

3987  536 
val proto_pure = 
16493  537 
Context.pre_pure_thy 
16987  538 
> Compress.init_data 
16536  539 
> Sign.init_data 
540 
> Theory.init_data 

541 
> Proofterm.init_data 

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

542 
> TheoremsData.init 
3987  543 
> Theory.add_types 
4922
03b81b6e1baa
added thms_closure: theory > xstring > tthm list option;
wenzelm
parents:
4853
diff
changeset

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

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

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

547 
("dummy", 0, NoSyn)] 
18713  548 
> Theory.add_nonterminals Syntax.basic_nonterms 
3987  549 
> Theory.add_syntax 
18713  550 
[("_lambda", "[pttrns, 'a] => logic", Mixfix ("(3%_./ _)", [0, 3], 3)), 
551 
("_abs", "'a", NoSyn), 

552 
("", "'a => args", Delimfix "_"), 

553 
("_args", "['a, args] => args", Delimfix "_,/ _"), 

554 
("", "id => idt", Delimfix "_"), 

555 
("_idtdummy", "idt", Delimfix "'_"), 

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

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

558 
("", "idt => idt", Delimfix "'(_')"), 

559 
("", "idt => idts", Delimfix "_"), 

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

561 
("", "idt => pttrn", Delimfix "_"), 

562 
("", "pttrn => pttrns", Delimfix "_"), 

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

564 
("", "id => aprop", Delimfix "_"), 

565 
("", "longid => aprop", Delimfix "_"), 

566 
("", "var => aprop", Delimfix "_"), 

567 
("_DDDOT", "aprop", Delimfix "..."), 

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

569 
("_asm", "prop => asms", Delimfix "_"), 

570 
("_asms", "[prop, asms] => asms", Delimfix "_;/ _"), 

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

572 
("_ofclass", "[type, logic] => prop", Delimfix "(1OFCLASS/(1'(_,/ _')))"), 

573 
("_mk_ofclass", "_", NoSyn), 

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

575 
("", "id => logic", Delimfix "_"), 

576 
("", "longid => logic", Delimfix "_"), 

577 
("", "var => logic", Delimfix "_"), 

578 
("_DDDOT", "logic", Delimfix "..."), 

579 
("_constify", "num => num_const", Delimfix "_"), 

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

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

582 
("_indexdefault", "index", Delimfix ""), 

583 
("_indexvar", "index", Delimfix "'\\<index>"), 

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

585 
("==>", "prop => prop => prop", Delimfix "op ==>"), 

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

587 
> Theory.add_syntax Syntax.appl_syntax 

588 
> Theory.add_modesyntax (Symbol.xsymbolsN, true) 

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

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

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

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

21524  593 
("_idtyp", "[id, type] => idt", Mixfix ("_\\<Colon>_", [], 0)), 
18713  594 
("_idtypdummy", "type => idt", Mixfix ("'_()\\<Colon>_", [], 0)), 
19577  595 
("_type_constraint_", "'a", NoSyn), 
18713  596 
("_lambda", "[pttrns, 'a] => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)), 
597 
("==", "['a, 'a] => prop", InfixrName ("\\<equiv>", 2)), 

21524  598 
("all_binder", "[idts, prop] => prop", Mixfix ("(3\\<And>_./ _)", [0, 0], 0)), 
18713  599 
("==>", "[prop, prop] => prop", InfixrName ("\\<Longrightarrow>", 1)), 
600 
("_DDDOT", "aprop", Delimfix "\\<dots>"), 

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

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

603 
> Theory.add_modesyntax ("", false) 

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

19775  605 
("ProtoPure.term", "'a => prop", Delimfix "TERM _"), 
19125
59b26248547b
simplified Pure conjunction, based on actual const;
wenzelm
parents:
19046
diff
changeset

606 
("ProtoPure.conjunction", "prop => prop => prop", InfixrName ("&&", 2))] 
18713  607 
> Theory.add_modesyntax ("HTML", false) 
608 
[("_lambda", "[pttrns, 'a] => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3))] 

3987  609 
> Theory.add_consts 
16441  610 
[("==", "'a => 'a => prop", InfixrName ("==", 2)), 
611 
("==>", "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)), 

3987  612 
("all", "('a => prop) => prop", Binder ("!!", 0, 0)), 
18031  613 
("prop", "prop => prop", NoSyn), 
6547  614 
("TYPE", "'a itself", NoSyn), 
9534  615 
(Term.dummy_patternN, "'a", Delimfix "'_")] 
14223
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
13800
diff
changeset

616 
> Theory.add_finals_i false 
16441  617 
[Const ("==", [aT, aT] > propT), 
618 
Const ("==>", [propT, propT] > propT), 

619 
Const ("all", (aT > propT) > propT), 

19391  620 
Const ("TYPE", Term.a_itselfT), 
17703  621 
Const (Term.dummy_patternN, aT)] 
18838  622 
> Theory.add_trfuns Syntax.pure_trfuns 
623 
> Theory.add_trfunsT Syntax.pure_trfunsT 

16441  624 
> Sign.local_path 
19125
59b26248547b
simplified Pure conjunction, based on actual const;
wenzelm
parents:
19046
diff
changeset

625 
> Theory.add_consts 
19775  626 
[("term", "'a => prop", NoSyn), 
627 
("conjunction", "prop => prop => prop", NoSyn)] 

19125
59b26248547b
simplified Pure conjunction, based on actual const;
wenzelm
parents:
19046
diff
changeset

628 
> (add_defs false o map Thm.no_attributes) 
59b26248547b
simplified Pure conjunction, based on actual const;
wenzelm
parents:
19046
diff
changeset

629 
[("prop_def", "prop(A) == A"), 
19775  630 
("term_def", "term(x) == (!!A. PROP A ==> PROP A)"), 
19125
59b26248547b
simplified Pure conjunction, based on actual const;
wenzelm
parents:
19046
diff
changeset

631 
("conjunction_def", 
59b26248547b
simplified Pure conjunction, based on actual const;
wenzelm
parents:
19046
diff
changeset

632 
"conjunction(A, B) == (!!C. (PROP A ==> PROP B ==> PROP C) ==> PROP C)")] > snd 
19775  633 
> Sign.hide_consts false ["conjunction", "term"] 
18377  634 
> add_thmss [(("nothing", []), [])] > snd 
11516
a0633bdcd015
Added equality axioms and initialization of proof term package.
berghofe
parents:
10667
diff
changeset

635 
> Theory.add_axioms_i Proofterm.equality_axms 
16493  636 
> Theory.end_theory; 
3987  637 

5091  638 
structure ProtoPure = 
639 
struct 

640 
val thy = proto_pure; 

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

643 
val conjunction_def = get_axiom thy "conjunction_def"; 
5091  644 
end; 
3987  645 

646 
end; 

647 

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

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

649 
open BasicPureThy; 