author | paulson <lp15@cam.ac.uk> |
Sun, 20 May 2018 18:37:34 +0100 | |
changeset 68239 | 0764ee22a4d1 |
parent 67721 | 5348bea4accd |
child 70388 | e31271559de8 |
permissions | -rw-r--r-- |
3987 | 1 |
(* Title: Pure/pure_thy.ML |
2 |
Author: Markus Wenzel, TU Muenchen |
|
3 |
||
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
39507
diff
changeset
|
4 |
Pure theory syntax and further logical content. |
3987 | 5 |
*) |
6 |
||
7 |
signature PURE_THY = |
|
8 |
sig |
|
26959
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset
|
9 |
val old_appl_syntax: theory -> bool |
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset
|
10 |
val old_appl_syntax_setup: theory -> theory |
52160 | 11 |
val token_markers: string list |
3987 | 12 |
end; |
13 |
||
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
39507
diff
changeset
|
14 |
structure Pure_Thy: PURE_THY = |
3987 | 15 |
struct |
16 |
||
33384 | 17 |
val typ = Simple_Syntax.read_typ; |
18 |
val prop = Simple_Syntax.read_prop; |
|
35429
afa8cf9e63d8
authentic syntax for classes and type constructors;
wenzelm
parents:
35262
diff
changeset
|
19 |
|
42290
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42288
diff
changeset
|
20 |
val tycon = Lexicon.mark_type; |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42288
diff
changeset
|
21 |
val const = Lexicon.mark_const; |
24243 | 22 |
|
56234 | 23 |
val qualify = Binding.qualify true Context.PureN; |
24 |
||
62752 | 25 |
fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range); |
26 |
fun infix_ (sy, p) = Infix (Input.string sy, p, Position.no_range); |
|
27 |
fun infixr_ (sy, p) = Infixr (Input.string sy, p, Position.no_range); |
|
28 |
fun binder (sy, p, q) = Binder (Input.string sy, p, q, Position.no_range); |
|
29 |
||
26959
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset
|
30 |
|
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset
|
31 |
(* application syntax variants *) |
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset
|
32 |
|
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset
|
33 |
val appl_syntax = |
67721 | 34 |
[("_appl", typ "('b \<Rightarrow> 'a) \<Rightarrow> args \<Rightarrow> logic", mixfix ("(1_/(1'(_')))", [1000, 0], 1000)), |
35 |
("_appl", typ "('b \<Rightarrow> 'a) \<Rightarrow> args \<Rightarrow> aprop", mixfix ("(1_/(1'(_')))", [1000, 0], 1000))]; |
|
26959
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset
|
36 |
|
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset
|
37 |
val applC_syntax = |
67721 | 38 |
[("", typ "'a \<Rightarrow> cargs", Mixfix.mixfix "_"), |
39 |
("_cargs", typ "'a \<Rightarrow> cargs \<Rightarrow> cargs", mixfix ("_/ _", [1000, 1000], 1000)), |
|
40 |
("_applC", typ "('b \<Rightarrow> 'a) \<Rightarrow> cargs \<Rightarrow> logic", mixfix ("(1_/ _)", [1000, 1000], 999)), |
|
41 |
("_applC", typ "('b \<Rightarrow> 'a) \<Rightarrow> cargs \<Rightarrow> aprop", mixfix ("(1_/ _)", [1000, 1000], 999))]; |
|
26959
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset
|
42 |
|
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36744
diff
changeset
|
43 |
structure Old_Appl_Syntax = Theory_Data |
26959
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset
|
44 |
( |
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset
|
45 |
type T = bool; |
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset
|
46 |
val empty = false; |
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset
|
47 |
val extend = I; |
33522 | 48 |
fun merge (b1, b2) : T = |
26959
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset
|
49 |
if b1 = b2 then b1 |
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset
|
50 |
else error "Cannot merge theories with different application syntax"; |
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset
|
51 |
); |
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset
|
52 |
|
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36744
diff
changeset
|
53 |
val old_appl_syntax = Old_Appl_Syntax.get; |
26959
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset
|
54 |
|
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset
|
55 |
val old_appl_syntax_setup = |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36744
diff
changeset
|
56 |
Old_Appl_Syntax.put true #> |
56240 | 57 |
Sign.del_syntax Syntax.mode_default applC_syntax #> |
58 |
Sign.add_syntax Syntax.mode_default appl_syntax; |
|
26959
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset
|
59 |
|
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset
|
60 |
|
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset
|
61 |
(* main content *) |
f8f2df3e4d83
theory Pure provides regular application syntax by default;
wenzelm
parents:
26693
diff
changeset
|
62 |
|
52160 | 63 |
val token_markers = |
64 |
["_tfree", "_tvar", "_free", "_bound", "_loose", "_var", "_numeral", "_inner_string"]; |
|
65 |
||
53171 | 66 |
val _ = Theory.setup |
33365 | 67 |
(Sign.map_naming (Name_Space.set_theory_name Context.PureN) #> |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36744
diff
changeset
|
68 |
Old_Appl_Syntax.put false #> |
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42297
diff
changeset
|
69 |
Sign.add_types_global |
64556 | 70 |
[(Binding.make ("fun", \<^here>), 2, NoSyn), |
71 |
(Binding.make ("prop", \<^here>), 0, NoSyn), |
|
72 |
(Binding.make ("itself", \<^here>), 1, NoSyn), |
|
73 |
(Binding.make ("dummy", \<^here>), 0, NoSyn)] |
|
61255
15865e0c5598
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents:
61246
diff
changeset
|
74 |
#> Theory.add_deps_global "fun" ((Defs.Type, "fun"), [typ "'a", typ "'b"]) [] |
15865e0c5598
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents:
61246
diff
changeset
|
75 |
#> Theory.add_deps_global "prop" ((Defs.Type, "prop"), []) [] |
15865e0c5598
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents:
61246
diff
changeset
|
76 |
#> Theory.add_deps_global "itself" ((Defs.Type, "itself"), [typ "'a"]) [] |
15865e0c5598
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents:
61246
diff
changeset
|
77 |
#> Theory.add_deps_global "dummy" ((Defs.Type, "dummy"), []) [] |
52160 | 78 |
#> Sign.add_nonterminals_global |
64556 | 79 |
(map (fn name => Binding.make (name, \<^here>)) |
52160 | 80 |
(Lexicon.terminals @ ["logic", "type", "types", "sort", "classes", |
81 |
"args", "cargs", "pttrn", "pttrns", "idt", "idts", "aprop", "asms", |
|
58421 | 82 |
"any", "prop'", "num_const", "float_const", "num_position", |
83 |
"float_position", "index", "struct", "tid_position", |
|
55108
0b7a0c1fdf7e
inner syntax token language allows regular quoted strings;
wenzelm
parents:
55033
diff
changeset
|
84 |
"tvar_position", "id_position", "longid_position", "var_position", |
0b7a0c1fdf7e
inner syntax token language allows regular quoted strings;
wenzelm
parents:
55033
diff
changeset
|
85 |
"str_position", "string_position", "cartouche_position", "type_name", |
0b7a0c1fdf7e
inner syntax token language allows regular quoted strings;
wenzelm
parents:
55033
diff
changeset
|
86 |
"class_name"])) |
56240 | 87 |
#> Sign.add_syntax Syntax.mode_default (map (fn x => (x, typ "'a", NoSyn)) token_markers) |
88 |
#> Sign.add_syntax Syntax.mode_default |
|
67721 | 89 |
[("", typ "prop' \<Rightarrow> prop", Mixfix.mixfix "_"), |
90 |
("", typ "logic \<Rightarrow> any", Mixfix.mixfix "_"), |
|
91 |
("", typ "prop' \<Rightarrow> any", Mixfix.mixfix "_"), |
|
92 |
("", typ "logic \<Rightarrow> logic", Mixfix.mixfix "'(_')"), |
|
93 |
("", typ "prop' \<Rightarrow> prop'", Mixfix.mixfix "'(_')"), |
|
94 |
("_constrain", typ "logic \<Rightarrow> type \<Rightarrow> logic", mixfix ("_::_", [4, 0], 3)), |
|
95 |
("_constrain", typ "prop' \<Rightarrow> type \<Rightarrow> prop'", mixfix ("_::_", [4, 0], 3)), |
|
52211
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
52161
diff
changeset
|
96 |
("_ignore_type", typ "'a", NoSyn), |
67721 | 97 |
("", typ "tid_position \<Rightarrow> type", Mixfix.mixfix "_"), |
98 |
("", typ "tvar_position \<Rightarrow> type", Mixfix.mixfix "_"), |
|
99 |
("", typ "type_name \<Rightarrow> type", Mixfix.mixfix "_"), |
|
100 |
("_type_name", typ "id \<Rightarrow> type_name", Mixfix.mixfix "_"), |
|
101 |
("_type_name", typ "longid \<Rightarrow> type_name", Mixfix.mixfix "_"), |
|
102 |
("_ofsort", typ "tid_position \<Rightarrow> sort \<Rightarrow> type", mixfix ("_::_", [1000, 0], 1000)), |
|
103 |
("_ofsort", typ "tvar_position \<Rightarrow> sort \<Rightarrow> type", mixfix ("_::_", [1000, 0], 1000)), |
|
104 |
("_dummy_ofsort", typ "sort \<Rightarrow> type", mixfix ("'_()::_", [0], 1000)), |
|
105 |
("", typ "class_name \<Rightarrow> sort", Mixfix.mixfix "_"), |
|
106 |
("_class_name", typ "id \<Rightarrow> class_name", Mixfix.mixfix "_"), |
|
107 |
("_class_name", typ "longid \<Rightarrow> class_name", Mixfix.mixfix "_"), |
|
67718 | 108 |
("_dummy_sort", typ "sort", Mixfix.mixfix "'_"), |
62761 | 109 |
("_topsort", typ "sort", Mixfix.mixfix "{}"), |
67721 | 110 |
("_sort", typ "classes \<Rightarrow> sort", Mixfix.mixfix "{_}"), |
111 |
("", typ "class_name \<Rightarrow> classes", Mixfix.mixfix "_"), |
|
112 |
("_classes", typ "class_name \<Rightarrow> classes \<Rightarrow> classes", Mixfix.mixfix "_,_"), |
|
113 |
("_tapp", typ "type \<Rightarrow> type_name \<Rightarrow> type", mixfix ("_ _", [1000, 0], 1000)), |
|
114 |
("_tappl", typ "type \<Rightarrow> types \<Rightarrow> type_name \<Rightarrow> type", Mixfix.mixfix "((1'(_,/ _')) _)"), |
|
115 |
("", typ "type \<Rightarrow> types", Mixfix.mixfix "_"), |
|
116 |
("_types", typ "type \<Rightarrow> types \<Rightarrow> types", Mixfix.mixfix "_,/ _"), |
|
117 |
("\<^type>fun", typ "type \<Rightarrow> type \<Rightarrow> type", mixfix ("(_/ \<Rightarrow> _)", [1, 0], 0)), |
|
118 |
("_bracket", typ "types \<Rightarrow> type \<Rightarrow> type", mixfix ("([_]/ \<Rightarrow> _)", [0, 0], 0)), |
|
119 |
("", typ "type \<Rightarrow> type", Mixfix.mixfix "'(_')"), |
|
62761 | 120 |
("\<^type>dummy", typ "type", Mixfix.mixfix "'_"), |
42263
49b1b8d0782f
type syntax as regular mixfix specification (type_ext for bootstrapping has been obsolete for many years);
wenzelm
parents:
42245
diff
changeset
|
121 |
("_type_prop", typ "'a", NoSyn), |
67721 | 122 |
("_lambda", typ "pttrns \<Rightarrow> 'a \<Rightarrow> logic", mixfix ("(3\<lambda>_./ _)", [0, 3], 3)), |
26436 | 123 |
("_abs", typ "'a", NoSyn), |
67721 | 124 |
("", typ "'a \<Rightarrow> args", Mixfix.mixfix "_"), |
125 |
("_args", typ "'a \<Rightarrow> args \<Rightarrow> args", Mixfix.mixfix "_,/ _"), |
|
126 |
("", typ "id_position \<Rightarrow> idt", Mixfix.mixfix "_"), |
|
62761 | 127 |
("_idtdummy", typ "idt", Mixfix.mixfix "'_"), |
67721 | 128 |
("_idtyp", typ "id_position \<Rightarrow> type \<Rightarrow> idt", mixfix ("_::_", [], 0)), |
129 |
("_idtypdummy", typ "type \<Rightarrow> idt", mixfix ("'_()::_", [], 0)), |
|
130 |
("", typ "idt \<Rightarrow> idt", Mixfix.mixfix "'(_')"), |
|
131 |
("", typ "idt \<Rightarrow> idts", Mixfix.mixfix "_"), |
|
132 |
("_idts", typ "idt \<Rightarrow> idts \<Rightarrow> idts", mixfix ("_/ _", [1, 0], 0)), |
|
133 |
("", typ "idt \<Rightarrow> pttrn", Mixfix.mixfix "_"), |
|
134 |
("", typ "pttrn \<Rightarrow> pttrns", Mixfix.mixfix "_"), |
|
135 |
("_pttrns", typ "pttrn \<Rightarrow> pttrns \<Rightarrow> pttrns", mixfix ("_/ _", [1, 0], 0)), |
|
136 |
("", typ "aprop \<Rightarrow> aprop", Mixfix.mixfix "'(_')"), |
|
137 |
("", typ "id_position \<Rightarrow> aprop", Mixfix.mixfix "_"), |
|
138 |
("", typ "longid_position \<Rightarrow> aprop", Mixfix.mixfix "_"), |
|
139 |
("", typ "var_position \<Rightarrow> aprop", Mixfix.mixfix "_"), |
|
62761 | 140 |
("_DDDOT", typ "aprop", Mixfix.mixfix "\<dots>"), |
67721 | 141 |
("_aprop", typ "aprop \<Rightarrow> prop", Mixfix.mixfix "PROP _"), |
142 |
("_asm", typ "prop \<Rightarrow> asms", Mixfix.mixfix "_"), |
|
143 |
("_asms", typ "prop \<Rightarrow> asms \<Rightarrow> asms", Mixfix.mixfix "_;/ _"), |
|
144 |
("_bigimpl", typ "asms \<Rightarrow> prop \<Rightarrow> prop", mixfix ("((1\<lbrakk>_\<rbrakk>)/ \<Longrightarrow> _)", [0, 1], 1)), |
|
145 |
("_ofclass", typ "type \<Rightarrow> logic \<Rightarrow> prop", Mixfix.mixfix "(1OFCLASS/(1'(_,/ _')))"), |
|
26436 | 146 |
("_mk_ofclass", typ "dummy", NoSyn), |
67721 | 147 |
("_TYPE", typ "type \<Rightarrow> logic", Mixfix.mixfix "(1TYPE/(1'(_')))"), |
148 |
("", typ "id_position \<Rightarrow> logic", Mixfix.mixfix "_"), |
|
149 |
("", typ "longid_position \<Rightarrow> logic", Mixfix.mixfix "_"), |
|
150 |
("", typ "var_position \<Rightarrow> logic", Mixfix.mixfix "_"), |
|
62761 | 151 |
("_DDDOT", typ "logic", Mixfix.mixfix "\<dots>"), |
42057
3eba96ff3d3e
more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
wenzelm
parents:
42048
diff
changeset
|
152 |
("_strip_positions", typ "'a", NoSyn), |
67721 | 153 |
("_position", typ "num_token \<Rightarrow> num_position", Mixfix.mixfix "_"), |
154 |
("_position", typ "float_token \<Rightarrow> float_position", Mixfix.mixfix "_"), |
|
155 |
("_constify", typ "num_position \<Rightarrow> num_const", Mixfix.mixfix "_"), |
|
156 |
("_constify", typ "float_position \<Rightarrow> float_const", Mixfix.mixfix "_"), |
|
157 |
("_index", typ "logic \<Rightarrow> index", Mixfix.mixfix "(\<open>unbreakable\<close>\<^bsub>_\<^esub>)"), |
|
62761 | 158 |
("_indexdefault", typ "index", Mixfix.mixfix ""), |
159 |
("_indexvar", typ "index", Mixfix.mixfix "'\<index>"), |
|
67721 | 160 |
("_struct", typ "index \<Rightarrow> logic", NoSyn), |
35145
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
35130
diff
changeset
|
161 |
("_update_name", typ "idt", NoSyn), |
42295
8fdbb3b10beb
moved CONST syntax/translations to their proper place;
wenzelm
parents:
42294
diff
changeset
|
162 |
("_constrainAbs", typ "'a", NoSyn), |
67721 | 163 |
("_position_sort", typ "tid \<Rightarrow> tid_position", Mixfix.mixfix "_"), |
164 |
("_position_sort", typ "tvar \<Rightarrow> tvar_position", Mixfix.mixfix "_"), |
|
165 |
("_position", typ "id \<Rightarrow> id_position", Mixfix.mixfix "_"), |
|
166 |
("_position", typ "longid \<Rightarrow> longid_position", Mixfix.mixfix "_"), |
|
167 |
("_position", typ "var \<Rightarrow> var_position", Mixfix.mixfix "_"), |
|
168 |
("_position", typ "str_token \<Rightarrow> str_position", Mixfix.mixfix "_"), |
|
169 |
("_position", typ "string_token \<Rightarrow> string_position", Mixfix.mixfix "_"), |
|
170 |
("_position", typ "cartouche \<Rightarrow> cartouche_position", Mixfix.mixfix "_"), |
|
42048
afd11ca8e018
support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
wenzelm
parents:
39557
diff
changeset
|
171 |
("_type_constraint_", typ "'a", NoSyn), |
67721 | 172 |
("_context_const", typ "id_position \<Rightarrow> logic", Mixfix.mixfix "CONST _"), |
173 |
("_context_const", typ "id_position \<Rightarrow> aprop", Mixfix.mixfix "CONST _"), |
|
174 |
("_context_const", typ "longid_position \<Rightarrow> logic", Mixfix.mixfix "CONST _"), |
|
175 |
("_context_const", typ "longid_position \<Rightarrow> aprop", Mixfix.mixfix "CONST _"), |
|
176 |
("_context_xconst", typ "id_position \<Rightarrow> logic", Mixfix.mixfix "XCONST _"), |
|
177 |
("_context_xconst", typ "id_position \<Rightarrow> aprop", Mixfix.mixfix "XCONST _"), |
|
178 |
("_context_xconst", typ "longid_position \<Rightarrow> logic", Mixfix.mixfix "XCONST _"), |
|
179 |
("_context_xconst", typ "longid_position \<Rightarrow> aprop", Mixfix.mixfix "XCONST _"), |
|
62761 | 180 |
(const "Pure.dummy_pattern", typ "aprop", Mixfix.mixfix "'_"), |
67721 | 181 |
("_sort_constraint", typ "type \<Rightarrow> prop", Mixfix.mixfix "(1SORT'_CONSTRAINT/(1'(_')))"), |
182 |
(const "Pure.term", typ "logic \<Rightarrow> prop", Mixfix.mixfix "TERM _"), |
|
183 |
(const "Pure.conjunction", typ "prop \<Rightarrow> prop \<Rightarrow> prop", infixr_ ("&&&", 2))] |
|
56240 | 184 |
#> Sign.add_syntax Syntax.mode_default applC_syntax |
61957
301833d9013a
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61256
diff
changeset
|
185 |
#> Sign.add_syntax (Print_Mode.ASCII, true) |
67721 | 186 |
[(tycon "fun", typ "type \<Rightarrow> type \<Rightarrow> type", mixfix ("(_/ => _)", [1, 0], 0)), |
187 |
("_bracket", typ "types \<Rightarrow> type \<Rightarrow> type", mixfix ("([_]/ => _)", [0, 0], 0)), |
|
188 |
("_lambda", typ "pttrns \<Rightarrow> 'a \<Rightarrow> logic", mixfix ("(3%_./ _)", [0, 3], 3)), |
|
189 |
(const "Pure.eq", typ "'a \<Rightarrow> 'a \<Rightarrow> prop", infix_ ("==", 2)), |
|
190 |
(const "Pure.all_binder", typ "idts \<Rightarrow> prop \<Rightarrow> prop", mixfix ("(3!!_./ _)", [0, 0], 0)), |
|
191 |
(const "Pure.imp", typ "prop \<Rightarrow> prop \<Rightarrow> prop", infixr_ ("==>", 1)), |
|
62761 | 192 |
("_DDDOT", typ "aprop", Mixfix.mixfix "..."), |
67721 | 193 |
("_bigimpl", typ "asms \<Rightarrow> prop \<Rightarrow> prop", mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)), |
62761 | 194 |
("_DDDOT", typ "logic", Mixfix.mixfix "...")] |
56240 | 195 |
#> Sign.add_syntax ("", false) |
67721 | 196 |
[(const "Pure.prop", typ "prop \<Rightarrow> prop", mixfix ("_", [0], 0))] |
56239 | 197 |
#> Sign.add_consts |
67721 | 198 |
[(qualify (Binding.make ("eq", \<^here>)), typ "'a \<Rightarrow> 'a \<Rightarrow> prop", infix_ ("\<equiv>", 2)), |
199 |
(qualify (Binding.make ("imp", \<^here>)), typ "prop \<Rightarrow> prop \<Rightarrow> prop", infixr_ ("\<Longrightarrow>", 1)), |
|
200 |
(qualify (Binding.make ("all", \<^here>)), typ "('a \<Rightarrow> prop) \<Rightarrow> prop", binder ("\<And>", 0, 0)), |
|
201 |
(qualify (Binding.make ("prop", \<^here>)), typ "prop \<Rightarrow> prop", NoSyn), |
|
64556 | 202 |
(qualify (Binding.make ("type", \<^here>)), typ "'a itself", NoSyn), |
203 |
(qualify (Binding.make ("dummy_pattern", \<^here>)), typ "'a", Mixfix.mixfix "'_")] |
|
61256 | 204 |
#> Theory.add_deps_global "Pure.eq" ((Defs.Const, "Pure.eq"), [typ "'a"]) [] |
205 |
#> Theory.add_deps_global "Pure.imp" ((Defs.Const, "Pure.imp"), []) [] |
|
206 |
#> Theory.add_deps_global "Pure.all" ((Defs.Const, "Pure.all"), [typ "'a"]) [] |
|
207 |
#> Theory.add_deps_global "Pure.type" ((Defs.Const, "Pure.type"), [typ "'a"]) [] |
|
208 |
#> Theory.add_deps_global "Pure.dummy_pattern" ((Defs.Const, "Pure.dummy_pattern"), [typ "'a"]) [] |
|
52143 | 209 |
#> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation |
210 |
#> Sign.parse_translation Syntax_Trans.pure_parse_translation |
|
211 |
#> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation |
|
56239 | 212 |
#> Sign.add_consts |
67721 | 213 |
[(qualify (Binding.make ("term", \<^here>)), typ "'a \<Rightarrow> prop", NoSyn), |
214 |
(qualify (Binding.make ("sort_constraint", \<^here>)), typ "'a itself \<Rightarrow> prop", NoSyn), |
|
215 |
(qualify (Binding.make ("conjunction", \<^here>)), typ "prop \<Rightarrow> prop \<Rightarrow> prop", NoSyn)] |
|
26430 | 216 |
#> Sign.local_path |
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
39507
diff
changeset
|
217 |
#> (Global_Theory.add_defs false o map Thm.no_attributes) |
64556 | 218 |
[(Binding.make ("prop_def", \<^here>), |
67721 | 219 |
prop "(CONST Pure.prop :: prop \<Rightarrow> prop) (A::prop) \<equiv> A::prop"), |
64556 | 220 |
(Binding.make ("term_def", \<^here>), |
67721 | 221 |
prop "(CONST Pure.term :: 'a \<Rightarrow> prop) (x::'a) \<equiv> (\<And>A::prop. A \<Longrightarrow> A)"), |
64556 | 222 |
(Binding.make ("sort_constraint_def", \<^here>), |
67721 | 223 |
prop "(CONST Pure.sort_constraint :: 'a itself \<Rightarrow> prop) (CONST Pure.type :: 'a itself) \<equiv>\ |
224 |
\ (CONST Pure.term :: 'a itself \<Rightarrow> prop) (CONST Pure.type :: 'a itself)"), |
|
64556 | 225 |
(Binding.make ("conjunction_def", \<^here>), |
67721 | 226 |
prop "(A &&& B) \<equiv> (\<And>C::prop. (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C)")] #> snd |
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42297
diff
changeset
|
227 |
#> fold (fn (a, prop) => |
64556 | 228 |
snd o Thm.add_axiom_global (Binding.make (a, \<^here>), prop)) Proofterm.equality_axms); |
3987 | 229 |
|
230 |
end; |