1(* Title: Pure/pure_thy.ML 2 Author: Markus Wenzel, TU Muenchen 3 4Pure theory syntax and further logical content. 5*) 6 7signature PURE_THY = 8sig 9 val old_appl_syntax: theory -> bool 10 val old_appl_syntax_setup: theory -> theory 11 val token_markers: string list 12end; 13 14structure Pure_Thy: PURE_THY = 15struct 16 17(* auxiliary *) 18 19val typ = Simple_Syntax.read_typ; 20val prop = Simple_Syntax.read_prop; 21 22val tycon = Lexicon.mark_type; 23val const = Lexicon.mark_const; 24 25val qualify = Binding.qualify true Context.PureN; 26 27fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range); 28fun infix_ (sy, p) = Infix (Input.string sy, p, Position.no_range); 29fun infixr_ (sy, p) = Infixr (Input.string sy, p, Position.no_range); 30fun binder (sy, p, q) = Binder (Input.string sy, p, q, Position.no_range); 31 32fun add_deps_type c thy = 33 let 34 val n = Sign.arity_number thy c; 35 val typargs = map (fn a => TFree (a, [])) (Name.invent Name.context Name.aT n); 36 in thy |> Theory.add_deps_global "" ((Defs.Type, c), typargs) [] end 37 38fun add_deps_const c thy = 39 let 40 val T = Logic.unvarifyT_global (Sign.the_const_type thy c); 41 val typargs = Sign.const_typargs thy (c, T); 42 in thy |> Theory.add_deps_global "" ((Defs.Const, c), typargs) [] end; 43 44 45(* application syntax variants *) 46 47val appl_syntax = 48 [("_appl", typ "('b \<Rightarrow> 'a) \<Rightarrow> args \<Rightarrow> logic", mixfix ("(1_/(1'(_')))", [1000, 0], 1000)), 49 ("_appl", typ "('b \<Rightarrow> 'a) \<Rightarrow> args \<Rightarrow> aprop", mixfix ("(1_/(1'(_')))", [1000, 0], 1000))]; 50 51val applC_syntax = 52 [("", typ "'a \<Rightarrow> cargs", Mixfix.mixfix "_"), 53 ("_cargs", typ "'a \<Rightarrow> cargs \<Rightarrow> cargs", mixfix ("_/ _", [1000, 1000], 1000)), 54 ("_applC", typ "('b \<Rightarrow> 'a) \<Rightarrow> cargs \<Rightarrow> logic", mixfix ("(1_/ _)", [1000, 1000], 999)), 55 ("_applC", typ "('b \<Rightarrow> 'a) \<Rightarrow> cargs \<Rightarrow> aprop", mixfix ("(1_/ _)", [1000, 1000], 999))]; 56 57structure Old_Appl_Syntax = Theory_Data 58( 59 type T = bool; 60 val empty = false; 61 val extend = I; 62 fun merge (b1, b2) : T = 63 if b1 = b2 then b1 64 else error "Cannot merge theories with different application syntax"; 65); 66 67val old_appl_syntax = Old_Appl_Syntax.get; 68 69val old_appl_syntax_setup = 70 Old_Appl_Syntax.put true #> 71 Sign.del_syntax Syntax.mode_default applC_syntax #> 72 Sign.add_syntax Syntax.mode_default appl_syntax; 73 74 75(* main content *) 76 77val token_markers = 78 ["_tfree", "_tvar", "_free", "_bound", "_loose", "_var", "_numeral", "_inner_string"]; 79 80val _ = Theory.setup 81 (Sign.theory_naming #> 82 Old_Appl_Syntax.put false #> 83 Sign.add_types_global 84 [(Binding.make ("fun", \<^here>), 2, NoSyn), 85 (Binding.make ("prop", \<^here>), 0, NoSyn), 86 (Binding.make ("itself", \<^here>), 1, NoSyn), 87 (Binding.make ("dummy", \<^here>), 0, NoSyn), 88 (qualify (Binding.make ("proof", \<^here>)), 0, NoSyn)] 89 #> add_deps_type "fun" 90 #> add_deps_type "prop" 91 #> add_deps_type "itself" 92 #> add_deps_type "dummy" 93 #> add_deps_type "Pure.proof" 94 #> Sign.add_nonterminals_global 95 (map (fn name => Binding.make (name, \<^here>)) 96 (Lexicon.terminals @ ["logic", "type", "types", "sort", "classes", 97 "args", "cargs", "pttrn", "pttrns", "idt", "idts", "aprop", "asms", 98 "any", "prop'", "num_const", "float_const", "num_position", 99 "float_position", "index", "struct", "tid_position", 100 "tvar_position", "id_position", "longid_position", "var_position", 101 "str_position", "string_position", "cartouche_position", "type_name", 102 "class_name"])) 103 #> Sign.add_syntax Syntax.mode_default (map (fn x => (x, typ "'a", NoSyn)) token_markers) 104 #> Sign.add_syntax Syntax.mode_default 105 [("", typ "prop' \<Rightarrow> prop", Mixfix.mixfix "_"), 106 ("", typ "logic \<Rightarrow> any", Mixfix.mixfix "_"), 107 ("", typ "prop' \<Rightarrow> any", Mixfix.mixfix "_"), 108 ("", typ "logic \<Rightarrow> logic", Mixfix.mixfix "'(_')"), 109 ("", typ "prop' \<Rightarrow> prop'", Mixfix.mixfix "'(_')"), 110 ("_constrain", typ "logic \<Rightarrow> type \<Rightarrow> logic", mixfix ("_::_", [4, 0], 3)), 111 ("_constrain", typ "prop' \<Rightarrow> type \<Rightarrow> prop'", mixfix ("_::_", [4, 0], 3)), 112 ("_ignore_type", typ "'a", NoSyn), 113 ("", typ "tid_position \<Rightarrow> type", Mixfix.mixfix "_"), 114 ("", typ "tvar_position \<Rightarrow> type", Mixfix.mixfix "_"), 115 ("", typ "type_name \<Rightarrow> type", Mixfix.mixfix "_"), 116 ("_type_name", typ "id \<Rightarrow> type_name", Mixfix.mixfix "_"), 117 ("_type_name", typ "longid \<Rightarrow> type_name", Mixfix.mixfix "_"), 118 ("_ofsort", typ "tid_position \<Rightarrow> sort \<Rightarrow> type", mixfix ("_::_", [1000, 0], 1000)), 119 ("_ofsort", typ "tvar_position \<Rightarrow> sort \<Rightarrow> type", mixfix ("_::_", [1000, 0], 1000)), 120 ("_dummy_ofsort", typ "sort \<Rightarrow> type", mixfix ("'_' ::_", [0], 1000)), 121 ("", typ "class_name \<Rightarrow> sort", Mixfix.mixfix "_"), 122 ("_class_name", typ "id \<Rightarrow> class_name", Mixfix.mixfix "_"), 123 ("_class_name", typ "longid \<Rightarrow> class_name", Mixfix.mixfix "_"), 124 ("_dummy_sort", typ "sort", Mixfix.mixfix "'_"), 125 ("_topsort", typ "sort", Mixfix.mixfix "{}"), 126 ("_sort", typ "classes \<Rightarrow> sort", Mixfix.mixfix "{_}"), 127 ("", typ "class_name \<Rightarrow> classes", Mixfix.mixfix "_"), 128 ("_classes", typ "class_name \<Rightarrow> classes \<Rightarrow> classes", Mixfix.mixfix "_,_"), 129 ("_tapp", typ "type \<Rightarrow> type_name \<Rightarrow> type", mixfix ("_ _", [1000, 0], 1000)), 130 ("_tappl", typ "type \<Rightarrow> types \<Rightarrow> type_name \<Rightarrow> type", Mixfix.mixfix "((1'(_,/ _')) _)"), 131 ("", typ "type \<Rightarrow> types", Mixfix.mixfix "_"), 132 ("_types", typ "type \<Rightarrow> types \<Rightarrow> types", Mixfix.mixfix "_,/ _"), 133 ("\<^type>fun", typ "type \<Rightarrow> type \<Rightarrow> type", mixfix ("(_/ \<Rightarrow> _)", [1, 0], 0)), 134 ("_bracket", typ "types \<Rightarrow> type \<Rightarrow> type", mixfix ("([_]/ \<Rightarrow> _)", [0, 0], 0)), 135 ("", typ "type \<Rightarrow> type", Mixfix.mixfix "'(_')"), 136 ("\<^type>dummy", typ "type", Mixfix.mixfix "'_"), 137 ("_type_prop", typ "'a", NoSyn), 138 ("_lambda", typ "pttrns \<Rightarrow> 'a \<Rightarrow> logic", mixfix ("(3\<lambda>_./ _)", [0, 3], 3)), 139 ("_abs", typ "'a", NoSyn), 140 ("", typ "'a \<Rightarrow> args", Mixfix.mixfix "_"), 141 ("_args", typ "'a \<Rightarrow> args \<Rightarrow> args", Mixfix.mixfix "_,/ _"), 142 ("", typ "id_position \<Rightarrow> idt", Mixfix.mixfix "_"), 143 ("_idtdummy", typ "idt", Mixfix.mixfix "'_"), 144 ("_idtyp", typ "id_position \<Rightarrow> type \<Rightarrow> idt", mixfix ("_::_", [], 0)), 145 ("_idtypdummy", typ "type \<Rightarrow> idt", mixfix ("'_' ::_", [], 0)), 146 ("", typ "idt \<Rightarrow> idt", Mixfix.mixfix "'(_')"), 147 ("", typ "idt \<Rightarrow> idts", Mixfix.mixfix "_"), 148 ("_idts", typ "idt \<Rightarrow> idts \<Rightarrow> idts", mixfix ("_/ _", [1, 0], 0)), 149 ("", typ "idt \<Rightarrow> pttrn", Mixfix.mixfix "_"), 150 ("", typ "pttrn \<Rightarrow> pttrns", Mixfix.mixfix "_"), 151 ("_pttrns", typ "pttrn \<Rightarrow> pttrns \<Rightarrow> pttrns", mixfix ("_/ _", [1, 0], 0)), 152 ("", typ "aprop \<Rightarrow> aprop", Mixfix.mixfix "'(_')"), 153 ("", typ "id_position \<Rightarrow> aprop", Mixfix.mixfix "_"), 154 ("", typ "longid_position \<Rightarrow> aprop", Mixfix.mixfix "_"), 155 ("", typ "var_position \<Rightarrow> aprop", Mixfix.mixfix "_"), 156 ("_DDDOT", typ "aprop", Mixfix.mixfix "\<dots>"), 157 ("_aprop", typ "aprop \<Rightarrow> prop", Mixfix.mixfix "PROP _"), 158 ("_asm", typ "prop \<Rightarrow> asms", Mixfix.mixfix "_"), 159 ("_asms", typ "prop \<Rightarrow> asms \<Rightarrow> asms", Mixfix.mixfix "_;/ _"), 160 ("_bigimpl", typ "asms \<Rightarrow> prop \<Rightarrow> prop", mixfix ("((1\<lbrakk>_\<rbrakk>)/ \<Longrightarrow> _)", [0, 1], 1)), 161 ("_ofclass", typ "type \<Rightarrow> logic \<Rightarrow> prop", Mixfix.mixfix "(1OFCLASS/(1'(_,/ _')))"), 162 ("_mk_ofclass", typ "dummy", NoSyn), 163 ("_TYPE", typ "type \<Rightarrow> logic", Mixfix.mixfix "(1TYPE/(1'(_')))"), 164 ("", typ "id_position \<Rightarrow> logic", Mixfix.mixfix "_"), 165 ("", typ "longid_position \<Rightarrow> logic", Mixfix.mixfix "_"), 166 ("", typ "var_position \<Rightarrow> logic", Mixfix.mixfix "_"), 167 ("_DDDOT", typ "logic", Mixfix.mixfix "\<dots>"), 168 ("_strip_positions", typ "'a", NoSyn), 169 ("_position", typ "num_token \<Rightarrow> num_position", Mixfix.mixfix "_"), 170 ("_position", typ "float_token \<Rightarrow> float_position", Mixfix.mixfix "_"), 171 ("_constify", typ "num_position \<Rightarrow> num_const", Mixfix.mixfix "_"), 172 ("_constify", typ "float_position \<Rightarrow> float_const", Mixfix.mixfix "_"), 173 ("_index", typ "logic \<Rightarrow> index", Mixfix.mixfix "(\<open>unbreakable\<close>\<^bsub>_\<^esub>)"), 174 ("_indexdefault", typ "index", Mixfix.mixfix ""), 175 ("_indexvar", typ "index", Mixfix.mixfix "'\<index>"), 176 ("_struct", typ "index \<Rightarrow> logic", NoSyn), 177 ("_update_name", typ "idt", NoSyn), 178 ("_constrainAbs", typ "'a", NoSyn), 179 ("_position_sort", typ "tid \<Rightarrow> tid_position", Mixfix.mixfix "_"), 180 ("_position_sort", typ "tvar \<Rightarrow> tvar_position", Mixfix.mixfix "_"), 181 ("_position", typ "id \<Rightarrow> id_position", Mixfix.mixfix "_"), 182 ("_position", typ "longid \<Rightarrow> longid_position", Mixfix.mixfix "_"), 183 ("_position", typ "var \<Rightarrow> var_position", Mixfix.mixfix "_"), 184 ("_position", typ "str_token \<Rightarrow> str_position", Mixfix.mixfix "_"), 185 ("_position", typ "string_token \<Rightarrow> string_position", Mixfix.mixfix "_"), 186 ("_position", typ "cartouche \<Rightarrow> cartouche_position", Mixfix.mixfix "_"), 187 ("_type_constraint_", typ "'a", NoSyn), 188 ("_context_const", typ "id_position \<Rightarrow> logic", Mixfix.mixfix "CONST _"), 189 ("_context_const", typ "id_position \<Rightarrow> aprop", Mixfix.mixfix "CONST _"), 190 ("_context_const", typ "longid_position \<Rightarrow> logic", Mixfix.mixfix "CONST _"), 191 ("_context_const", typ "longid_position \<Rightarrow> aprop", Mixfix.mixfix "CONST _"), 192 ("_context_xconst", typ "id_position \<Rightarrow> logic", Mixfix.mixfix "XCONST _"), 193 ("_context_xconst", typ "id_position \<Rightarrow> aprop", Mixfix.mixfix "XCONST _"), 194 ("_context_xconst", typ "longid_position \<Rightarrow> logic", Mixfix.mixfix "XCONST _"), 195 ("_context_xconst", typ "longid_position \<Rightarrow> aprop", Mixfix.mixfix "XCONST _"), 196 (const "Pure.dummy_pattern", typ "aprop", Mixfix.mixfix "'_"), 197 ("_sort_constraint", typ "type \<Rightarrow> prop", Mixfix.mixfix "(1SORT'_CONSTRAINT/(1'(_')))"), 198 (const "Pure.term", typ "logic \<Rightarrow> prop", Mixfix.mixfix "TERM _"), 199 (const "Pure.conjunction", typ "prop \<Rightarrow> prop \<Rightarrow> prop", infixr_ ("&&&", 2))] 200 #> Sign.add_syntax Syntax.mode_default applC_syntax 201 #> Sign.add_syntax (Print_Mode.ASCII, true) 202 [(tycon "fun", typ "type \<Rightarrow> type \<Rightarrow> type", mixfix ("(_/ => _)", [1, 0], 0)), 203 ("_bracket", typ "types \<Rightarrow> type \<Rightarrow> type", mixfix ("([_]/ => _)", [0, 0], 0)), 204 ("_lambda", typ "pttrns \<Rightarrow> 'a \<Rightarrow> logic", mixfix ("(3%_./ _)", [0, 3], 3)), 205 (const "Pure.eq", typ "'a \<Rightarrow> 'a \<Rightarrow> prop", infix_ ("==", 2)), 206 (const "Pure.all_binder", typ "idts \<Rightarrow> prop \<Rightarrow> prop", mixfix ("(3!!_./ _)", [0, 0], 0)), 207 (const "Pure.imp", typ "prop \<Rightarrow> prop \<Rightarrow> prop", infixr_ ("==>", 1)), 208 ("_DDDOT", typ "aprop", Mixfix.mixfix "..."), 209 ("_bigimpl", typ "asms \<Rightarrow> prop \<Rightarrow> prop", mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)), 210 ("_DDDOT", typ "logic", Mixfix.mixfix "...")] 211 #> Sign.add_syntax ("", false) 212 [(const "Pure.prop", typ "prop \<Rightarrow> prop", mixfix ("_", [0], 0))] 213 #> Sign.add_consts 214 [(qualify (Binding.make ("eq", \<^here>)), typ "'a \<Rightarrow> 'a \<Rightarrow> prop", infix_ ("\<equiv>", 2)), 215 (qualify (Binding.make ("imp", \<^here>)), typ "prop \<Rightarrow> prop \<Rightarrow> prop", infixr_ ("\<Longrightarrow>", 1)), 216 (qualify (Binding.make ("all", \<^here>)), typ "('a \<Rightarrow> prop) \<Rightarrow> prop", binder ("\<And>", 0, 0)), 217 (qualify (Binding.make ("prop", \<^here>)), typ "prop \<Rightarrow> prop", NoSyn), 218 (qualify (Binding.make ("type", \<^here>)), typ "'a itself", NoSyn), 219 (qualify (Binding.make ("dummy_pattern", \<^here>)), typ "'a", Mixfix.mixfix "'_"), 220 (qualify (Binding.make ("Appt", \<^here>)), typ "Pure.proof \<Rightarrow> 'a \<Rightarrow> Pure.proof", NoSyn), 221 (qualify (Binding.make ("AppP", \<^here>)), typ "Pure.proof \<Rightarrow> Pure.proof \<Rightarrow> Pure.proof", NoSyn), 222 (qualify (Binding.make ("Abst", \<^here>)), typ "('a \<Rightarrow> Pure.proof) \<Rightarrow> Pure.proof", NoSyn), 223 (qualify (Binding.make ("AbsP", \<^here>)), typ "prop \<Rightarrow> (Pure.proof \<Rightarrow> Pure.proof) \<Rightarrow> Pure.proof", NoSyn), 224 (qualify (Binding.make ("Hyp", \<^here>)), typ "prop \<Rightarrow> Pure.proof", NoSyn), 225 (qualify (Binding.make ("Oracle", \<^here>)), typ "prop \<Rightarrow> Pure.proof", NoSyn), 226 (qualify (Binding.make ("OfClass", \<^here>)), typ "('a itself \<Rightarrow> prop) \<Rightarrow> Pure.proof", NoSyn), 227 (qualify (Binding.make ("MinProof", \<^here>)), typ "Pure.proof", NoSyn)] 228 #> add_deps_const "Pure.eq" 229 #> add_deps_const "Pure.imp" 230 #> add_deps_const "Pure.all" 231 #> add_deps_const "Pure.type" 232 #> add_deps_const "Pure.dummy_pattern" 233 #> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation 234 #> Sign.parse_translation Syntax_Trans.pure_parse_translation 235 #> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation 236 #> Sign.add_consts 237 [(qualify (Binding.make ("term", \<^here>)), typ "'a \<Rightarrow> prop", NoSyn), 238 (qualify (Binding.make ("sort_constraint", \<^here>)), typ "'a itself \<Rightarrow> prop", NoSyn), 239 (qualify (Binding.make ("conjunction", \<^here>)), typ "prop \<Rightarrow> prop \<Rightarrow> prop", NoSyn)] 240 #> Sign.local_path 241 #> (Global_Theory.add_defs false o map Thm.no_attributes) 242 [(Binding.make ("prop_def", \<^here>), 243 prop "(CONST Pure.prop :: prop \<Rightarrow> prop) (A::prop) \<equiv> A::prop"), 244 (Binding.make ("term_def", \<^here>), 245 prop "(CONST Pure.term :: 'a \<Rightarrow> prop) (x::'a) \<equiv> (\<And>A::prop. A \<Longrightarrow> A)"), 246 (Binding.make ("sort_constraint_def", \<^here>), 247 prop "(CONST Pure.sort_constraint :: 'a itself \<Rightarrow> prop) (CONST Pure.type :: 'a itself) \<equiv>\ 248 \ (CONST Pure.term :: 'a itself \<Rightarrow> prop) (CONST Pure.type :: 'a itself)"), 249 (Binding.make ("conjunction_def", \<^here>), 250 prop "(A &&& B) \<equiv> (\<And>C::prop. (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C)")] #> snd 251 #> fold (fn (a, prop) => 252 snd o Thm.add_axiom_global (Binding.make (a, \<^here>), prop)) Proofterm.equality_axms); 253 254end; 255