1 (* Title: Pure/pure_thy.ML
2 Author: Markus Wenzel, TU Muenchen
4 Pure theory syntax and further logical content.
9 val old_appl_syntax: theory -> bool
10 val old_appl_syntax_setup: theory -> theory
13 structure Pure_Thy: PURE_THY =
16 val typ = Simple_Syntax.read_typ;
17 val prop = Simple_Syntax.read_prop;
19 val tycon = Lexicon.mark_type;
20 val const = Lexicon.mark_const;
23 (* application syntax variants *)
26 [("_appl", typ "('b => 'a) => args => logic", Mixfix ("(1_/(1'(_')))", [1000, 0], 1000)),
27 ("_appl", typ "('b => 'a) => args => aprop", Mixfix ("(1_/(1'(_')))", [1000, 0], 1000))];
30 [("", typ "'a => cargs", Delimfix "_"),
31 ("_cargs", typ "'a => cargs => cargs", Mixfix ("_/ _", [1000, 1000], 1000)),
32 ("_applC", typ "('b => 'a) => cargs => logic", Mixfix ("(1_/ _)", [1000, 1000], 999)),
33 ("_applC", typ "('b => 'a) => cargs => aprop", Mixfix ("(1_/ _)", [1000, 1000], 999))];
35 structure Old_Appl_Syntax = Theory_Data
40 fun merge (b1, b2) : T =
42 else error "Cannot merge theories with different application syntax";
45 val old_appl_syntax = Old_Appl_Syntax.get;
47 val old_appl_syntax_setup =
48 Old_Appl_Syntax.put true #>
49 Sign.del_modesyntax_i Syntax.mode_default applC_syntax #>
50 Sign.add_syntax_i appl_syntax;
55 val _ = Context.>> (Context.map_theory
56 (Sign.map_naming (Name_Space.set_theory_name Context.PureN) #>
57 Old_Appl_Syntax.put false #>
59 [(Binding.name "fun", 2, NoSyn),
60 (Binding.name "prop", 0, NoSyn),
61 (Binding.name "itself", 1, NoSyn),
62 (Binding.name "dummy", 0, NoSyn)]
63 #> Sign.add_nonterminals_global (map Binding.name Syntax.basic_nonterms)
64 #> Sign.add_syntax_i (map (fn x => (x, typ "'a", NoSyn)) Syntax.token_markers)
66 [("", typ "prop' => prop", Delimfix "_"),
67 ("", typ "logic => any", Delimfix "_"),
68 ("", typ "prop' => any", Delimfix "_"),
69 ("", typ "logic => logic", Delimfix "'(_')"),
70 ("", typ "prop' => prop'", Delimfix "'(_')"),
71 ("_constrain", typ "logic => type => logic", Mixfix ("_::_", [4, 0], 3)),
72 ("_constrain", typ "prop' => type => prop'", Mixfix ("_::_", [4, 0], 3)),
73 ("", typ "tid => type", Delimfix "_"),
74 ("", typ "tvar => type", Delimfix "_"),
75 ("", typ "type_name => type", Delimfix "_"),
76 ("_type_name", typ "id => type_name", Delimfix "_"),
77 ("_type_name", typ "longid => type_name", Delimfix "_"),
78 ("_ofsort", typ "tid => sort => type", Mixfix ("_::_", [1000, 0], 1000)),
79 ("_ofsort", typ "tvar => sort => type", Mixfix ("_::_", [1000, 0], 1000)),
80 ("_dummy_ofsort", typ "sort => type", Mixfix ("'_()::_", [0], 1000)),
81 ("", typ "class_name => sort", Delimfix "_"),
82 ("_class_name", typ "id => class_name", Delimfix "_"),
83 ("_class_name", typ "longid => class_name", Delimfix "_"),
84 ("_topsort", typ "sort", Delimfix "{}"),
85 ("_sort", typ "classes => sort", Delimfix "{_}"),
86 ("", typ "class_name => classes", Delimfix "_"),
87 ("_classes", typ "class_name => classes => classes", Delimfix "_,_"),
88 ("_tapp", typ "type => type_name => type", Mixfix ("_ _", [1000, 0], 1000)),
89 ("_tappl", typ "type => types => type_name => type", Delimfix "((1'(_,/ _')) _)"),
90 ("", typ "type => types", Delimfix "_"),
91 ("_types", typ "type => types => types", Delimfix "_,/ _"),
92 ("\\<^type>fun", typ "type => type => type", Mixfix ("(_/ => _)", [1, 0], 0)),
93 ("_bracket", typ "types => type => type", Mixfix ("([_]/ => _)", [0, 0], 0)),
94 ("", typ "type => type", Delimfix "'(_')"),
95 ("\\<^type>dummy", typ "type", Delimfix "'_"),
96 ("_type_prop", typ "'a", NoSyn),
97 ("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3%_./ _)", [0, 3], 3)),
98 ("_abs", typ "'a", NoSyn),
99 ("", typ "'a => args", Delimfix "_"),
100 ("_args", typ "'a => args => args", Delimfix "_,/ _"),
101 ("", typ "id_position => idt", Delimfix "_"),
102 ("_idtdummy", typ "idt", Delimfix "'_"),
103 ("_idtyp", typ "id_position => type => idt", Mixfix ("_::_", [], 0)),
104 ("_idtypdummy", typ "type => idt", Mixfix ("'_()::_", [], 0)),
105 ("", typ "idt => idt", Delimfix "'(_')"),
106 ("", typ "idt => idts", Delimfix "_"),
107 ("_idts", typ "idt => idts => idts", Mixfix ("_/ _", [1, 0], 0)),
108 ("", typ "idt => pttrn", Delimfix "_"),
109 ("", typ "pttrn => pttrns", Delimfix "_"),
110 ("_pttrns", typ "pttrn => pttrns => pttrns", Mixfix ("_/ _", [1, 0], 0)),
111 ("", typ "aprop => aprop", Delimfix "'(_')"),
112 ("", typ "id_position => aprop", Delimfix "_"),
113 ("", typ "longid_position => aprop", Delimfix "_"),
114 ("", typ "var => aprop", Delimfix "_"),
115 ("_DDDOT", typ "aprop", Delimfix "..."),
116 ("_aprop", typ "aprop => prop", Delimfix "PROP _"),
117 ("_asm", typ "prop => asms", Delimfix "_"),
118 ("_asms", typ "prop => asms => asms", Delimfix "_;/ _"),
119 ("_bigimpl", typ "asms => prop => prop", Mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)),
120 ("_ofclass", typ "type => logic => prop", Delimfix "(1OFCLASS/(1'(_,/ _')))"),
121 ("_mk_ofclass", typ "dummy", NoSyn),
122 ("_TYPE", typ "type => logic", Delimfix "(1TYPE/(1'(_')))"),
123 ("", typ "id_position => logic", Delimfix "_"),
124 ("", typ "longid_position => logic", Delimfix "_"),
125 ("", typ "var => logic", Delimfix "_"),
126 ("_DDDOT", typ "logic", Delimfix "..."),
127 ("_strip_positions", typ "'a", NoSyn),
128 ("_position", typ "num_token => num_position", Delimfix "_"),
129 ("_position", typ "float_token => float_position", Delimfix "_"),
130 ("_position", typ "xnum_token => xnum_position", Delimfix "_"),
131 ("_constify", typ "num_position => num_const", Delimfix "_"),
132 ("_constify", typ "float_position => float_const", Delimfix "_"),
133 ("_constify", typ "xnum_position => xnum_const", Delimfix "_"),
134 ("_index", typ "logic => index", Delimfix "(00\\<^bsub>_\\<^esub>)"),
135 ("_indexdefault", typ "index", Delimfix ""),
136 ("_indexvar", typ "index", Delimfix "'\\<index>"),
137 ("_struct", typ "index => logic", Mixfix ("\\<struct>_", [1000], 1000)),
138 ("_update_name", typ "idt", NoSyn),
139 ("_constrainAbs", typ "'a", NoSyn),
140 ("_position", typ "id => id_position", Delimfix "_"),
141 ("_position", typ "longid => longid_position", Delimfix "_"),
142 ("_position", typ "str_token => str_position", Delimfix "_"),
143 ("_type_constraint_", typ "'a", NoSyn),
144 ("_context_const", typ "id_position => logic", Delimfix "CONST _"),
145 ("_context_const", typ "id_position => aprop", Delimfix "CONST _"),
146 ("_context_const", typ "longid_position => logic", Delimfix "CONST _"),
147 ("_context_const", typ "longid_position => aprop", Delimfix "CONST _"),
148 ("_context_xconst", typ "id_position => logic", Delimfix "XCONST _"),
149 ("_context_xconst", typ "id_position => aprop", Delimfix "XCONST _"),
150 ("_context_xconst", typ "longid_position => logic", Delimfix "XCONST _"),
151 ("_context_xconst", typ "longid_position => aprop", Delimfix "XCONST _"),
152 (const "==>", typ "prop => prop => prop", Delimfix "op ==>"),
153 (const Term.dummy_patternN, typ "aprop", Delimfix "'_"),
154 ("_sort_constraint", typ "type => prop", Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),
155 (const "Pure.term", typ "logic => prop", Delimfix "TERM _"),
156 (const "Pure.conjunction", typ "prop => prop => prop", Infixr ("&&&", 2))]
157 #> Sign.add_syntax_i applC_syntax
158 #> Sign.add_modesyntax_i (Symbol.xsymbolsN, true)
159 [(tycon "fun", typ "type => type => type", Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
160 ("_bracket", typ "types => type => type", Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
161 ("_ofsort", typ "tid => sort => type", Mixfix ("_\\<Colon>_", [1000, 0], 1000)),
162 ("_constrain", typ "logic => type => logic", Mixfix ("_\\<Colon>_", [4, 0], 3)),
163 ("_constrain", typ "prop' => type => prop'", Mixfix ("_\\<Colon>_", [4, 0], 3)),
164 ("_idtyp", typ "id_position => type => idt", Mixfix ("_\\<Colon>_", [], 0)),
165 ("_idtypdummy", typ "type => idt", Mixfix ("'_()\\<Colon>_", [], 0)),
166 ("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
167 (const "==", typ "'a => 'a => prop", Infixr ("\\<equiv>", 2)),
168 (const "all_binder", typ "idts => prop => prop", Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
169 (const "==>", typ "prop => prop => prop", Infixr ("\\<Longrightarrow>", 1)),
170 ("_DDDOT", typ "aprop", Delimfix "\\<dots>"),
171 ("_bigimpl", typ "asms => prop => prop", Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
172 ("_DDDOT", typ "logic", Delimfix "\\<dots>")]
173 #> Sign.add_modesyntax_i ("", false)
174 [(const "prop", typ "prop => prop", Mixfix ("_", [0], 0))]
175 #> Sign.add_modesyntax_i ("HTML", false)
176 [("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3))]
178 [(Binding.name "==", typ "'a => 'a => prop", Infixr ("==", 2)),
179 (Binding.name "==>", typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
180 (Binding.name "all", typ "('a => prop) => prop", Binder ("!!", 0, 0)),
181 (Binding.name "prop", typ "prop => prop", NoSyn),
182 (Binding.name "TYPE", typ "'a itself", NoSyn),
183 (Binding.name Term.dummy_patternN, typ "'a", Delimfix "'_")]
184 #> Theory.add_deps_global "==" ("==", typ "'a => 'a => prop") []
185 #> Theory.add_deps_global "==>" ("==>", typ "prop => prop => prop") []
186 #> Theory.add_deps_global "all" ("all", typ "('a => prop) => prop") []
187 #> Theory.add_deps_global "TYPE" ("TYPE", typ "'a itself") []
188 #> Theory.add_deps_global Term.dummy_patternN (Term.dummy_patternN, typ "'a") []
189 #> Sign.add_trfuns Syntax_Trans.pure_trfuns
192 [(Binding.name "term", typ "'a => prop", NoSyn),
193 (Binding.name "sort_constraint", typ "'a itself => prop", NoSyn),
194 (Binding.name "conjunction", typ "prop => prop => prop", NoSyn)]
195 #> (Global_Theory.add_defs false o map Thm.no_attributes)
196 [(Binding.name "prop_def", prop "(CONST prop :: prop => prop) (A::prop) == A::prop"),
197 (Binding.name "term_def", prop "(CONST Pure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"),
198 (Binding.name "sort_constraint_def",
199 prop "(CONST Pure.sort_constraint :: 'a itself => prop) (CONST TYPE :: 'a itself) ==\
200 \ (CONST Pure.term :: 'a itself => prop) (CONST TYPE :: 'a itself)"),
201 (Binding.name "conjunction_def", prop "(A &&& B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd
202 #> Sign.hide_const false "Pure.term"
203 #> Sign.hide_const false "Pure.sort_constraint"
204 #> Sign.hide_const false "Pure.conjunction"
205 #> Global_Theory.add_thmss [((Binding.name "nothing", []), [])] #> snd
206 #> fold (fn (a, prop) =>
207 snd o Thm.add_axiom_global (Binding.name a, prop)) Proofterm.equality_axms));