author  wenzelm 
Sun, 08 Nov 2009 18:43:42 +0100  
changeset 33522  737589bb9bb8 
parent 33384  1b5ba4e6a953 
child 33700  768d14a67256 
permissions  rwrr 
3987  1 
(* Title: Pure/pure_thy.ML 
2 
Author: Markus Wenzel, TU Muenchen 

3 

26430  4 
Theorem storage. Pure theory syntax and logical content. 
3987  5 
*) 
6 

7 
signature PURE_THY = 

8 
sig 

27198  9 
val facts_of: theory > Facts.T 
26666  10 
val intern_fact: theory > xstring > string 
26693  11 
val defined_fact: theory > string > bool 
27198  12 
val hide_fact: bool > string > theory > theory 
32105  13 
val join_proofs: theory > unit 
26683  14 
val get_fact: Context.generic > theory > Facts.ref > thm list 
26344
04dacc6809b6
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset

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

16 
val get_thm: theory > xstring > thm 
16336  17 
val all_thms_of: theory > (string * thm) list 
21580  18 
val map_facts: ('a > 'b) > ('c * ('a list * 'd) list) list > ('c * ('b list * 'd) list) list 
21567  19 
val burrow_fact: ('a list > 'b list) > ('a list * 'c) list > ('b list * 'c) list 
21580  20 
val burrow_facts: ('a list > 'b list) > 
21 
('c * ('a list * 'd) list) list > ('c * ('b list * 'd) list) list 

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

28076  23 
val name_thm: bool > bool > Position.T > string > thm > thm 
24 
val name_thms: bool > bool > Position.T > string > thm list > thm list 

25 
val name_thmss: bool > Position.T > string > (thm list * 'a) list > (thm list * 'a) list 

29579  26 
val store_thms: binding * thm list > theory > thm list * theory 
27 
val store_thm: binding * thm > theory > thm * theory 

28 
val store_thm_open: binding * thm > theory > thm * theory 

29 
val add_thms: ((binding * thm) * attribute list) list > theory > thm list * theory 

30 
val add_thm: (binding * thm) * attribute list > theory > thm * theory 

31 
val add_thmss: ((binding * thm list) * attribute list) list > theory > thm list list * theory 

32 
val add_thms_dynamic: binding * (Context.generic > thm list) > theory > theory 

30853  33 
val note_thmss: string > (Thm.binding * (thm list * attribute list) list) list 
34 
> theory > (string * thm list) list * theory 

29579  35 
val add_axioms: ((binding * term) * attribute list) list > theory > thm list * theory 
30337
eb189f7e43a1
Theory.add_axioms/add_defs: replaced old bstring by binding;
wenzelm
parents:
30242
diff
changeset

36 
val add_axioms_cmd: ((binding * string) * attribute list) list > theory > thm list * theory 
29579  37 
val add_defs: bool > ((binding * term) * attribute list) list > 
18377  38 
theory > thm list * theory 
29579  39 
val add_defs_unchecked: bool > ((binding * term) * attribute list) list > 
40 
theory > thm list * theory 

30337
eb189f7e43a1
Theory.add_axioms/add_defs: replaced old bstring by binding;
wenzelm
parents:
30242
diff
changeset

41 
val add_defs_cmd: bool > ((binding * string) * attribute list) list > 
18377  42 
theory > thm list * theory 
30337
eb189f7e43a1
Theory.add_axioms/add_defs: replaced old bstring by binding;
wenzelm
parents:
30242
diff
changeset

43 
val add_defs_unchecked_cmd: bool > ((binding * string) * attribute list) list > 
19629  44 
theory > thm list * theory 
26959
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset

45 
val old_appl_syntax: theory > bool 
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset

46 
val old_appl_syntax_setup: theory > theory 
3987  47 
end; 
48 

49 
structure PureThy: PURE_THY = 

50 
struct 

51 

52 

27198  53 
(*** stored facts ***) 
3987  54 

27198  55 
(** theory data **) 
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

56 

33522  57 
structure FactsData = Theory_Data 
24713  58 
( 
32105  59 
type T = Facts.T * thm list; 
60 
val empty = (Facts.empty, []); 

61 
fun extend (facts, _) = (facts, []); 

33522  62 
fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), []); 
24713  63 
); 
3987  64 

28841
5556c7976837
added force_proofs (based on thms ever passed through enter_thms);
wenzelm
parents:
28674
diff
changeset

65 

5556c7976837
added force_proofs (based on thms ever passed through enter_thms);
wenzelm
parents:
28674
diff
changeset

66 
(* facts *) 
5556c7976837
added force_proofs (based on thms ever passed through enter_thms);
wenzelm
parents:
28674
diff
changeset

67 

5556c7976837
added force_proofs (based on thms ever passed through enter_thms);
wenzelm
parents:
28674
diff
changeset

68 
val facts_of = #1 o FactsData.get; 
26666  69 

70 
val intern_fact = Facts.intern o facts_of; 

26693  71 
val defined_fact = Facts.defined o facts_of; 
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset

72 

28841
5556c7976837
added force_proofs (based on thms ever passed through enter_thms);
wenzelm
parents:
28674
diff
changeset

73 
fun hide_fact fully name = FactsData.map (apfst (Facts.hide fully name)); 
5556c7976837
added force_proofs (based on thms ever passed through enter_thms);
wenzelm
parents:
28674
diff
changeset

74 

5556c7976837
added force_proofs (based on thms ever passed through enter_thms);
wenzelm
parents:
28674
diff
changeset

75 

5556c7976837
added force_proofs (based on thms ever passed through enter_thms);
wenzelm
parents:
28674
diff
changeset

76 
(* proofs *) 
5556c7976837
added force_proofs (based on thms ever passed through enter_thms);
wenzelm
parents:
28674
diff
changeset

77 

32105  78 
fun register_proofs (thy, thms) = (FactsData.map (apsnd (append thms)) thy, thms); 
28977  79 

32105  80 
fun join_proofs thy = Thm.join_proofs (rev (#2 (FactsData.get thy))); 
27198  81 

6367  82 

3987  83 

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

84 
(** retrieve theorems **) 
3987  85 

27198  86 
fun get_fact context thy xthmref = 
26683  87 
let 
88 
val xname = Facts.name_of_ref xthmref; 

89 
val pos = Facts.pos_of_ref xthmref; 

27198  90 

91 
val name = intern_fact thy xname; 

92 
val res = Facts.lookup context (facts_of thy) name; 

93 
val _ = Theory.check_thy thy; 

26683  94 
in 
27198  95 
(case res of 
96 
NONE => error ("Unknown fact " ^ quote name ^ Position.str_of pos) 

27739  97 
 SOME (static, ths) => 
98 
(Position.report ((if static then Markup.fact else Markup.dynamic_fact) name) pos; 

99 
Facts.select xthmref (map (Thm.transfer thy) ths))) 

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

101 

26683  102 
fun get_thms thy = get_fact (Context.Theory thy) thy o Facts.named; 
26344
04dacc6809b6
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset

103 
fun get_thm thy name = Facts.the_single name (get_thms thy name); 
4783  104 

27198  105 
fun all_thms_of thy = 
27865
27a8ad9612a3
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
wenzelm
parents:
27739
diff
changeset

106 
Facts.fold_static (fn (_, ths) => append (map (`(Thm.get_name_hint)) ths)) (facts_of thy) []; 
16336  107 

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

108 

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

109 

26488
b497e3187ec7
eliminated destructive/critical theorem database;
wenzelm
parents:
26471
diff
changeset

110 
(** store theorems **) 
3987  111 

21580  112 
(* fact specifications *) 
113 

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

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

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

117 

118 

4853  119 
(* naming *) 
120 

18801  121 
fun name_multi name [x] = [(name, x)] 
26457  122 
 name_multi "" xs = map (pair "") xs 
123 
 name_multi name xs = map_index (fn (i, x) => (name ^ "_" ^ string_of_int (i + 1), x)) xs; 

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

124 

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

126 
> (if Thm.get_name thm <> "" andalso pre orelse not official then I else Thm.put_name name) 
27865
27a8ad9612a3
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
wenzelm
parents:
27739
diff
changeset

127 
> (if Thm.has_name_hint thm andalso pre orelse name = "" then I else Thm.put_name_hint name) 
28076  128 
> Thm.default_position pos 
27865
27a8ad9612a3
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
wenzelm
parents:
27739
diff
changeset

129 
> Thm.default_position (Position.thread_data ()); 
12872
0855c3ab2047
Theorems are only "prenamed" if the do not already have names.
berghofe
parents:
12711
diff
changeset

130 

28076  131 
fun name_thms pre official pos name xs = 
132 
map (uncurry (name_thm pre official pos)) (name_multi name xs); 

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

133 

28076  134 
fun name_thmss official pos name fact = 
135 
burrow_fact (name_thms true official pos name) fact; 

4853  136 

137 

11998  138 
(* enter_thms *) 
4853  139 

28861  140 
fun enter_thms pre_name post_name app_att (b, thms) thy = 
28965  141 
if Binding.is_empty b 
32105  142 
then swap (register_proofs (app_att (thy, thms))) 
30211  143 
else 
144 
let 

145 
val naming = Sign.naming_of thy; 

33095
bbd52d2f8696
renamed NameSpace to Name_Space  also to emphasize its subtle change in semantics;
wenzelm
parents:
32786
diff
changeset

146 
val name = Name_Space.full_name naming b; 
30211  147 
val (thy', thms') = 
32105  148 
register_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms))); 
30211  149 
val thms'' = map (Thm.transfer thy') thms'; 
150 
val thy'' = thy' > (FactsData.map o apfst) (Facts.add_global naming (b, thms'') #> snd); 

151 
in (thms'', thy'') end; 

26488
b497e3187ec7
eliminated destructive/critical theorem database;
wenzelm
parents:
26471
diff
changeset

152 

b497e3187ec7
eliminated destructive/critical theorem database;
wenzelm
parents:
26471
diff
changeset

153 

b497e3187ec7
eliminated destructive/critical theorem database;
wenzelm
parents:
26471
diff
changeset

154 
(* store_thm(s) *) 
b497e3187ec7
eliminated destructive/critical theorem database;
wenzelm
parents:
26471
diff
changeset

155 

29579  156 
fun store_thms (b, thms) = enter_thms (name_thms true true Position.none) 
157 
(name_thms false true Position.none) I (b, thms); 

28076  158 

29579  159 
fun store_thm (b, th) = store_thms (b, [th]) #>> the_single; 
26488
b497e3187ec7
eliminated destructive/critical theorem database;
wenzelm
parents:
26471
diff
changeset

160 

29579  161 
fun store_thm_open (b, th) = 
28076  162 
enter_thms (name_thms true false Position.none) (name_thms false false Position.none) I 
29579  163 
(b, [th]) #>> the_single; 
3987  164 

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

165 

6091  166 
(* add_thms(s) *) 
4853  167 

29579  168 
fun add_thms_atts pre_name ((b, thms), atts) = 
28076  169 
enter_thms pre_name (name_thms false true Position.none) 
30190  170 
(Library.foldl_map (Thm.theory_attributes atts)) (b, thms); 
4853  171 

18377  172 
fun gen_add_thmss pre_name = 
173 
fold_map (add_thms_atts pre_name); 

5907  174 

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

175 
fun gen_add_thms pre_name args = 
18377  176 
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

177 

28076  178 
val add_thmss = gen_add_thmss (name_thms true true Position.none); 
179 
val add_thms = gen_add_thms (name_thms true true Position.none); 

27683  180 
val add_thm = yield_singleton add_thms; 
5907  181 

182 

26488
b497e3187ec7
eliminated destructive/critical theorem database;
wenzelm
parents:
26471
diff
changeset

183 
(* add_thms_dynamic *) 
b497e3187ec7
eliminated destructive/critical theorem database;
wenzelm
parents:
26471
diff
changeset

184 

29579  185 
fun add_thms_dynamic (b, f) thy = thy 
28864  186 
> (FactsData.map o apfst) 
29579  187 
(Facts.add_dynamic (Sign.naming_of thy) (b, f) #> snd); 
26488
b497e3187ec7
eliminated destructive/critical theorem database;
wenzelm
parents:
26471
diff
changeset

188 

b497e3187ec7
eliminated destructive/critical theorem database;
wenzelm
parents:
26471
diff
changeset

189 

27728  190 
(* note_thmss *) 
5907  191 

33167  192 
fun note_thmss kind = fold_map (fn ((b, more_atts), ths_atts) => fn thy => 
12711  193 
let 
28941  194 
val pos = Binding.pos_of b; 
28965  195 
val name = Sign.full_name thy b; 
28076  196 
val _ = Position.report (Markup.fact_decl name) pos; 
197 

30190  198 
fun app (x, (ths, atts)) = Library.foldl_map (Thm.theory_attributes atts) (x, ths); 
18418
bf448d999b7e
rearranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18377
diff
changeset

199 
val (thms, thy') = thy > enter_thms 
30190  200 
(name_thmss true pos) (name_thms false true pos) (apsnd flat o Library.foldl_map app) 
33167  201 
(b, map (fn (ths, atts) => (ths, surround (Thm.kind kind) (atts @ more_atts))) ths_atts); 
28076  202 
in ((name, thms), thy') end); 
12711  203 

5280  204 

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

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

206 

4853  207 
local 
29579  208 
fun get_ax thy (b, _) = Thm.axiom thy (Sign.full_name thy b); 
26655  209 
fun get_axs thy named_axs = map (Thm.forall_elim_vars 0 o get_ax thy) named_axs; 
30337
eb189f7e43a1
Theory.add_axioms/add_defs: replaced old bstring by binding;
wenzelm
parents:
30242
diff
changeset

210 
fun add_axm add = fold_map (fn ((b, ax), atts) => fn thy => 
4853  211 
let 
29579  212 
val named_ax = [(b, ax)]; 
7753  213 
val thy' = add named_ax thy; 
30337
eb189f7e43a1
Theory.add_axioms/add_defs: replaced old bstring by binding;
wenzelm
parents:
30242
diff
changeset

214 
val thm = hd (get_axs thy' named_ax); 
eb189f7e43a1
Theory.add_axioms/add_defs: replaced old bstring by binding;
wenzelm
parents:
30242
diff
changeset

215 
in apfst hd (gen_add_thms (K I) [((b, thm), atts)] thy') end); 
4853  216 
in 
30337
eb189f7e43a1
Theory.add_axioms/add_defs: replaced old bstring by binding;
wenzelm
parents:
30242
diff
changeset

217 
val add_defs = add_axm o Theory.add_defs_i false; 
eb189f7e43a1
Theory.add_axioms/add_defs: replaced old bstring by binding;
wenzelm
parents:
30242
diff
changeset

218 
val add_defs_unchecked = add_axm o Theory.add_defs_i true; 
eb189f7e43a1
Theory.add_axioms/add_defs: replaced old bstring by binding;
wenzelm
parents:
30242
diff
changeset

219 
val add_axioms = add_axm Theory.add_axioms_i; 
eb189f7e43a1
Theory.add_axioms/add_defs: replaced old bstring by binding;
wenzelm
parents:
30242
diff
changeset

220 
val add_defs_cmd = add_axm o Theory.add_defs false; 
eb189f7e43a1
Theory.add_axioms/add_defs: replaced old bstring by binding;
wenzelm
parents:
30242
diff
changeset

221 
val add_defs_unchecked_cmd = add_axm o Theory.add_defs true; 
eb189f7e43a1
Theory.add_axioms/add_defs: replaced old bstring by binding;
wenzelm
parents:
30242
diff
changeset

222 
val add_axioms_cmd = add_axm Theory.add_axioms; 
4853  223 
end; 
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset

224 

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

225 

3987  226 

26430  227 
(*** Pure theory syntax and logical content ***) 
3987  228 

33384  229 
val typ = Simple_Syntax.read_typ; 
230 
val prop = Simple_Syntax.read_prop; 

24243  231 

28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28841
diff
changeset

232 
val typeT = Syntax.typeT; 
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28841
diff
changeset

233 
val spropT = Syntax.spropT; 
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28841
diff
changeset

234 

26959
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset

235 

f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset

236 
(* application syntax variants *) 
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset

237 

f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset

238 
val appl_syntax = 
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset

239 
[("_appl", typ "('b => 'a) => args => logic", Mixfix ("(1_/(1'(_')))", [1000, 0], 1000)), 
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset

240 
("_appl", typ "('b => 'a) => args => aprop", Mixfix ("(1_/(1'(_')))", [1000, 0], 1000))]; 
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset

241 

f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset

242 
val applC_syntax = 
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset

243 
[("", typ "'a => cargs", Delimfix "_"), 
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset

244 
("_cargs", typ "'a => cargs => cargs", Mixfix ("_/ _", [1000, 1000], 1000)), 
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset

245 
("_applC", typ "('b => 'a) => cargs => logic", Mixfix ("(1_/ _)", [1000, 1000], 999)), 
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset

246 
("_applC", typ "('b => 'a) => cargs => aprop", Mixfix ("(1_/ _)", [1000, 1000], 999))]; 
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset

247 

33522  248 
structure OldApplSyntax = Theory_Data 
26959
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset

249 
( 
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset

250 
type T = bool; 
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset

251 
val empty = false; 
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset

252 
val extend = I; 
33522  253 
fun merge (b1, b2) : T = 
26959
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset

254 
if b1 = b2 then b1 
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset

255 
else error "Cannot merge theories with different application syntax"; 
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset

256 
); 
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset

257 

f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset

258 
val old_appl_syntax = OldApplSyntax.get; 
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset

259 

f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset

260 
val old_appl_syntax_setup = 
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset

261 
OldApplSyntax.put true #> 
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset

262 
Sign.del_modesyntax_i Syntax.mode_default applC_syntax #> 
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset

263 
Sign.add_syntax_i appl_syntax; 
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset

264 

f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset

265 

f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset

266 
(* main content *) 
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset

267 

26463  268 
val _ = Context.>> (Context.map_theory 
33365  269 
(Sign.map_naming (Name_Space.set_theory_name Context.PureN) #> 
33522  270 
OldApplSyntax.put false #> 
26959
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset

271 
Sign.add_types 
30344
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
30337
diff
changeset

272 
[(Binding.name "fun", 2, NoSyn), 
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
30337
diff
changeset

273 
(Binding.name "prop", 0, NoSyn), 
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
30337
diff
changeset

274 
(Binding.name "itself", 1, NoSyn), 
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
30337
diff
changeset

275 
(Binding.name "dummy", 0, NoSyn)] 
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
30337
diff
changeset

276 
#> Sign.add_nonterminals (map Binding.name Syntax.basic_nonterms) 
26430  277 
#> Sign.add_syntax_i 
26436  278 
[("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3%_./ _)", [0, 3], 3)), 
279 
("_abs", typ "'a", NoSyn), 

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

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

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

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

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

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

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

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

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

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

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

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

28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28841
diff
changeset

292 
("", typ "aprop => aprop", Delimfix "'(_')"), 
26436  293 
("", typ "id => aprop", Delimfix "_"), 
294 
("", typ "longid => aprop", Delimfix "_"), 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

29156
89f76a58a378
renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents:
29002
diff
changeset

309 
("_constify", typ "float_token => float_const", Delimfix "_"), 
26436  310 
("_indexnum", typ "num_const => index", Delimfix "\\<^sub>_"), 
311 
("_index", typ "logic => index", Delimfix "(00\\<^bsub>_\\<^esub>)"), 

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

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

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

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

28622
1a0b845855ac
added const sort_constraint with syntax SORT_CONSTRAINT  logically vacous;
wenzelm
parents:
28076
diff
changeset

316 
(Term.dummy_patternN, typ "aprop", Delimfix "'_"), 
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28841
diff
changeset

317 
("_sort_constraint", typ "type => prop", Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"), 
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28841
diff
changeset

318 
("Pure.term", typ "logic => prop", Delimfix "TERM _"), 
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28841
diff
changeset

319 
("Pure.conjunction", typ "prop => prop => prop", InfixrName ("&&&", 2))] 
26959
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset

320 
#> Sign.add_syntax_i applC_syntax 
26430  321 
#> Sign.add_modesyntax_i (Symbol.xsymbolsN, true) 
24243  322 
[("fun", typ "type => type => type", Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)), 
323 
("_bracket", typ "types => type => type", Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)), 

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

28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28841
diff
changeset

325 
("_constrain", typ "logic => type => logic", Mixfix ("_\\<Colon>_", [4, 0], 3)), 
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28841
diff
changeset

326 
("_constrain", [spropT, typeT] > spropT, Mixfix ("_\\<Colon>_", [4, 0], 3)), 
24243  327 
("_idtyp", typ "id => type => idt", Mixfix ("_\\<Colon>_", [], 0)), 
328 
("_idtypdummy", typ "type => idt", Mixfix ("'_()\\<Colon>_", [], 0)), 

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

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

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

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

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

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

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

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

26430  337 
#> Sign.add_modesyntax_i ("", false) 
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28841
diff
changeset

338 
[("prop", typ "prop => prop", Mixfix ("_", [0], 0))] 
26430  339 
#> Sign.add_modesyntax_i ("HTML", false) 
24243  340 
[("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3))] 
26430  341 
#> Sign.add_consts_i 
30344
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
30337
diff
changeset

342 
[(Binding.name "==", typ "'a => 'a => prop", InfixrName ("==", 2)), 
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
30337
diff
changeset

343 
(Binding.name "==>", typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)), 
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
30337
diff
changeset

344 
(Binding.name "all", typ "('a => prop) => prop", Binder ("!!", 0, 0)), 
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
30337
diff
changeset

345 
(Binding.name "prop", typ "prop => prop", NoSyn), 
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
30337
diff
changeset

346 
(Binding.name "TYPE", typ "'a itself", NoSyn), 
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
30337
diff
changeset

347 
(Binding.name Term.dummy_patternN, typ "'a", Delimfix "'_")] 
26430  348 
#> Theory.add_deps "==" ("==", typ "'a => 'a => prop") [] 
349 
#> Theory.add_deps "==>" ("==>", typ "prop => prop => prop") [] 

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

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

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

353 
#> Sign.add_trfuns Syntax.pure_trfuns 

354 
#> Sign.add_trfunsT Syntax.pure_trfunsT 

355 
#> Sign.local_path 

356 
#> Sign.add_consts_i 

30344
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
30337
diff
changeset

357 
[(Binding.name "term", typ "'a => prop", NoSyn), 
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
30337
diff
changeset

358 
(Binding.name "sort_constraint", typ "'a itself => prop", NoSyn), 
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
30337
diff
changeset

359 
(Binding.name "conjunction", typ "prop => prop => prop", NoSyn)] 
27691
ce171cbd4b93
PureThy: dropped note_thmss_qualified, dropped _i suffix
haftmann
parents:
27683
diff
changeset

360 
#> (add_defs false o map Thm.no_attributes) 
29579  361 
[(Binding.name "prop_def", prop "(CONST prop :: prop => prop) (A::prop) == A::prop"), 
362 
(Binding.name "term_def", prop "(CONST Pure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"), 

363 
(Binding.name "sort_constraint_def", 

28622
1a0b845855ac
added const sort_constraint with syntax SORT_CONSTRAINT  logically vacous;
wenzelm
parents:
28076
diff
changeset

364 
prop "(CONST Pure.sort_constraint :: 'a itself => prop) (CONST TYPE :: 'a itself) ==\ 
1a0b845855ac
added const sort_constraint with syntax SORT_CONSTRAINT  logically vacous;
wenzelm
parents:
28076
diff
changeset

365 
\ (CONST Pure.term :: 'a itself => prop) (CONST TYPE :: 'a itself)"), 
29579  366 
(Binding.name "conjunction_def", prop "(A &&& B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd 
28622
1a0b845855ac
added const sort_constraint with syntax SORT_CONSTRAINT  logically vacous;
wenzelm
parents:
28076
diff
changeset

367 
#> Sign.hide_const false "Pure.term" 
1a0b845855ac
added const sort_constraint with syntax SORT_CONSTRAINT  logically vacous;
wenzelm
parents:
28076
diff
changeset

368 
#> Sign.hide_const false "Pure.sort_constraint" 
26666  369 
#> Sign.hide_const false "Pure.conjunction" 
29579  370 
#> add_thmss [((Binding.name "nothing", []), [])] #> snd 
30337
eb189f7e43a1
Theory.add_axioms/add_defs: replaced old bstring by binding;
wenzelm
parents:
30242
diff
changeset

371 
#> Theory.add_axioms_i (map (apfst Binding.name) Proofterm.equality_axms))); 
3987  372 

373 
end; 