(* Title: Pure/pure_thy.ML Author: Markus Wenzel, TU Muenchen Pure theory syntax and further logical content. signature PURE_THY =sig val old_appl_syntax: theory -> bool val old_appl_syntax_setup: theory -> theoryval token_markers: string list end ;structure Pure_Thy: PURE_THY =struct (* auxiliary *) val typ = Simple_Syntax.read_typ;val prop = Simple_Syntax.read_prop;val tycon = Lexicon.mark_type;val const = Lexicon.mark_const;val qualify = Binding.qualify true Context.PureN;fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range);fun infix_ (sy, p) = Infix (Input.string sy, p, Position.no_range);fun infixr_ (sy, p) = Infixr (Input.string sy, p, Position.no_range);fun binder (sy, p, q) = Binder (Input.string sy, p, q, Position.no_range);(* application syntax variants *) val appl_syntax ="_appl" , typ "('b \ 'a) \ args \ logic" ,"(\indent=1 notation=application\_/(1'(_')))" , [1000, 0], 1000)),"_appl" , typ "('b \ 'a) \ args \ aprop" ,"(\indent=1 notation=application\_/(1'(_')))" , [1000, 0], 1000))];val applC_syntax ="" , typ "'a \ cargs" , Mixfix.mixfix "_" ),"_cargs" , typ "'a \ cargs \ cargs" , mixfix ("_/ _" , [1000, 1000], 1000)),"_applC" , typ "('b \ 'a) \ cargs \ logic" ,"(\indent=1 notation=application\_/ _)" , [1000, 1000], 999)),"_applC" , typ "('b \ 'a) \ cargs \ aprop" ,"(\indent=1 notation=application\_/ _)" , [1000, 1000], 999))];structure Old_Appl_Syntax = Theory_Datatype T = bool ;val empty = false ;fun merge (b1, b2) : T =if b1 = b2 then b1else error "Cannot merge theories with different application syntax" ;val old_appl_syntax = Old_Appl_Syntax.get;val old_appl_syntax_setup =true #>false Syntax.mode_default applC_syntax #>true Syntax.mode_default appl_syntax;(* main content *) val token_markers ="_tfree" , "_tvar" , "_free" , "_bound" , "_loose" , "_var" , "_numeral" , "_inner_string" ];val _ = Theory.setupfalse #>"fun" , \<^here>), 2, NoSyn),"prop" , \<^here>), 0, NoSyn),"itself" , \<^here>), 1, NoSyn),"dummy" , \<^here>), 0, NoSyn),"proof" , \<^here>)), 0, NoSyn)]"fun" "prop" "itself" "dummy" "Pure.proof" map (fn name => Binding.make (name, \<^here>))"logic" , "type" , "types" , "sort" , "classes" ,"args" , "cargs" , "pttrn" , "pttrns" , "idt" , "idts" , "aprop" , "asms" ,"any" , "prop'" , "num_const" , "float_const" , "num_position" ,"float_position" , "index" , "struct" , "tid_position" ,"tvar_position" , "id_position" , "longid_position" , "var_position" ,"str_position" , "string_position" , "cartouche_position" , "type_name" ,"class_name" ]))true Syntax.mode_default (map (fn x => (x, typ "'a" , NoSyn)) token_markers)true Syntax.mode_default"" , typ "prop' \ prop" , Mixfix.mixfix "_" ),"" , typ "logic \ any" , Mixfix.mixfix "_" ),"" , typ "prop' \ any" , Mixfix.mixfix "_" ),"" , typ "logic \ logic" , Mixfix.mixfix "'(_')" ),"" , typ "prop' \ prop'" , Mixfix.mixfix "'(_')" ),"_constrain" , typ "logic \ type \ logic" , mixfix ("_::_" , [4, 0], 3)),"_constrain" , typ "prop' \ type \ prop'" , mixfix ("_::_" , [4, 0], 3)),"_ignore_type" , typ "'a" , NoSyn),"" , typ "tid_position \ type" , Mixfix.mixfix "_" ),"" , typ "tvar_position \ type" , Mixfix.mixfix "_" ),"" , typ "type_name \ type" , Mixfix.mixfix "_" ),"_type_name" , typ "id \ type_name" , Mixfix.mixfix "_" ),"_type_name" , typ "longid \ type_name" , Mixfix.mixfix "_" ),"_ofsort" , typ "tid_position \ sort \ type" , mixfix ("_::_" , [1000, 0], 1000)),"_ofsort" , typ "tvar_position \ sort \ type" , mixfix ("_::_" , [1000, 0], 1000)),"_dummy_ofsort" , typ "sort \ type" , mixfix ("'_' ::_" , [0], 1000)),"" , typ "class_name \ sort" , Mixfix.mixfix "_" ),"_class_name" , typ "id \ class_name" , Mixfix.mixfix "_" ),"_class_name" , typ "longid \ class_name" , Mixfix.mixfix "_" ),"_dummy_sort" , typ "sort" , Mixfix.mixfix "'_" ),"_topsort" , typ "sort" ,"(\open_block notation=\mixfix sort\\{})" ),"_sort" , typ "classes \ sort" ,"(\open_block notation=\mixfix sort\\{_})" ),"" , typ "class_name \ classes" , Mixfix.mixfix "_" ),"_classes" , typ "class_name \ classes \ classes" , Mixfix.mixfix "_,_" ),"_tapp" , typ "type \ type_name \ type" ,"(\open_block notation=\type_application\\_ _)" , [1000, 0], 1000)),"_tappl" , typ "type \ types \ type_name \ type" ,"(\notation=type_application\(1'(_,/ _')) _)" ),"" , typ "type \ types" , Mixfix.mixfix "_" ),"_types" , typ "type \ types \ types" , Mixfix.mixfix "_,/ _" ),"\<^type>fun" , typ "type \ type \ type" ,"(\notation=\infix \\\_/ \ _)" , [1, 0], 0)),"_bracket" , typ "types \ type \ type" ,"(\notation=\infix \\\[_]/ \ _)" , [0, 0], 0)),"" , typ "type \ type" , Mixfix.mixfix "'(_')" ),"\<^type>dummy" , typ "type" , Mixfix.mixfix "'_" ),"_type_prop" , typ "'a" , NoSyn),"_lambda" , typ "pttrns \ 'a \ logic" ,"(\indent=3 notation=abstraction\\_./ _)" , [0, 3], 3)),"_abs" , typ "'a" , NoSyn),"" , typ "'a \ args" , Mixfix.mixfix "_" ),"_args" , typ "'a \ args \ args" , Mixfix.mixfix "_,/ _" ),"" , typ "id_position \ idt" , Mixfix.mixfix "_" ),"_idtdummy" , typ "idt" , Mixfix.mixfix "'_" ),"_idtyp" , typ "id_position \ type \ idt" , mixfix ("_::_" , [], 0)),"_idtypdummy" , typ "type \ idt" , mixfix ("'_' ::_" , [], 0)),"" , typ "idt \ idt" , Mixfix.mixfix "'(_')" ),"" , typ "idt \ idts" , Mixfix.mixfix "_" ),"_idts" , typ "idt \ idts \ idts" , mixfix ("_/ _" , [1, 0], 0)),"" , typ "idt \ pttrn" , Mixfix.mixfix "_" ),"" , typ "pttrn \ pttrns" , Mixfix.mixfix "_" ),"_pttrns" , typ "pttrn \ pttrns \ pttrns" , mixfix ("_/ _" , [1, 0], 0)),"" , typ "aprop \ aprop" , Mixfix.mixfix "'(_')" ),"" , typ "id_position \ aprop" , Mixfix.mixfix "_" ),"" , typ "longid_position \ aprop" , Mixfix.mixfix "_" ),"" , typ "var_position \ aprop" , Mixfix.mixfix "_" ),"_DDDOT" , typ "aprop" , Mixfix.mixfix "\" ),"_aprop" , typ "aprop \ prop" ,"(\open_block notation=\prefix PROP\\PROP _)" ),"_asm" , typ "prop \ asms" , Mixfix.mixfix "_" ),"_asms" , typ "prop \ asms \ asms" , Mixfix.mixfix "_;/ _" ),"_bigimpl" , typ "asms \ prop \ prop" ,"(\notation=\infix \\\(1\_\)/ \ _)" , [0, 1], 1)),"_ofclass" , typ "type \ logic \ prop" ,"(\indent=1 notation=\mixfix OFCLASS\\OFCLASS/(1'(_,/ _')))" ),"_mk_ofclass" , typ "dummy" , NoSyn),"_TYPE" , typ "type \ logic" ,"(\indent=1 notation=\mixfix TYPE\\TYPE/(1'(_')))" ),"" , typ "id_position \ logic" , Mixfix.mixfix "_" ),"" , typ "longid_position \ logic" , Mixfix.mixfix "_" ),"" , typ "var_position \ logic" , Mixfix.mixfix "_" ),"_DDDOT" , typ "logic" , Mixfix.mixfix "\" ),"_strip_positions" , typ "'a" , NoSyn),"_position" , typ "num_token \ num_position" , Mixfix.mixfix "_" ),"_position" , typ "float_token \ float_position" , Mixfix.mixfix "_" ),"_constify" , typ "num_position \ num_const" , Mixfix.mixfix "_" ),"_constify" , typ "float_position \ float_const" , Mixfix.mixfix "_" ),"_index" , typ "logic \ index" , Mixfix.mixfix "(\unbreakable notation=\index\\\<^bsub>_\<^esub>)" ),"_indexdefault" , typ "index" , Mixfix.mixfix "" ),"_indexvar" , typ "index" , Mixfix.mixfix "'\" ),"_struct" , typ "index \ logic" , NoSyn),"_update_name" , typ "idt" , NoSyn),"_constrainAbs" , typ "'a" , NoSyn),"_position_sort" , typ "tid \ tid_position" , Mixfix.mixfix "_" ),"_position_sort" , typ "tvar \ tvar_position" , Mixfix.mixfix "_" ),"_position" , typ "id \ id_position" , Mixfix.mixfix "_" ),"_position" , typ "longid \ longid_position" , Mixfix.mixfix "_" ),"_position" , typ "var \ var_position" , Mixfix.mixfix "_" ),"_position" , typ "str_token \ str_position" , Mixfix.mixfix "_" ),"_position" , typ "string_token \ string_position" , Mixfix.mixfix "_" ),"_position" , typ "cartouche \ cartouche_position" , Mixfix.mixfix "_" ),"_type_constraint_" , typ "'a" , NoSyn),"_context_const" , typ "id_position \ logic" ,"(\open_block notation=\prefix CONST\\CONST _)" ),"_context_const" , typ "id_position \ aprop" ,"(\open_block notation=\prefix CONST\\CONST _)" ),"_context_const" , typ "longid_position \ logic" ,"(\open_block notation=\prefix CONST\\CONST _)" ),"_context_const" , typ "longid_position \ aprop" ,"(\open_block notation=\prefix CONST\\CONST _)" ),"_context_xconst" , typ "id_position \ logic" ,"(\open_block notation=\prefix XCONST\\XCONST _)" ),"_context_xconst" , typ "id_position \ aprop" ,"(\open_block notation=\prefix XCONST\\XCONST _)" ),"_context_xconst" , typ "longid_position \ logic" ,"(\open_block notation=\prefix XCONST\\XCONST _)" ),"_context_xconst" , typ "longid_position \ aprop" ,"(\open_block notation=\prefix XCONST\\XCONST _)" ),const "Pure.dummy_pattern" , typ "aprop" , Mixfix.mixfix "'_" ),"_sort_constraint" , typ "type \ prop" ,"(\indent=1 notation=\mixfix SORT_CONSTRAINT\\SORT'_CONSTRAINT/(1'(_')))" ),const "Pure.term" , typ "logic \ prop" ,"(\open_block notation=\prefix TERM\\TERM _)" ),const "Pure.conjunction" , typ "prop \ prop \ prop" , infixr_ ("&&&" , 2))]true Syntax.mode_default applC_syntaxtrue (Print_Mode.ASCII, true )"fun" , typ "type \ type \ type" ,"(\notation=\infix =>\\_/ => _)" , [1, 0], 0)),"_bracket" , typ "types \ type \ type" ,"(\notation=\infix =>\\[_]/ => _)" , [0, 0], 0)),"_lambda" , typ "pttrns \ 'a \ logic" ,"(\indent=3 notation=abstraction\%_./ _)" , [0, 3], 3)),const "Pure.eq" , typ "'a \ 'a \ prop" , infix_ ("==" , 2)),"Pure.all" , typ "idts \ prop \ prop" ,"(\indent=3 notation=\binder !!\\!!_./ _)" , [0, 0], 0)),const "Pure.imp" , typ "prop \ prop \ prop" , infixr_ ("==>" , 1)),"_DDDOT" , typ "aprop" , Mixfix.mixfix "..." ),"_bigimpl" , typ "asms \ prop \ prop" ,"(\notation=\infix \\\(3[| _ |])/ ==> _)" , [0, 1], 1)),"_DDDOT" , typ "logic" , Mixfix.mixfix "..." )]true ("" , false )const "Pure.prop" , typ "prop \ prop" , mixfix ("_" , [0], 0))]"eq" , \<^here>)), typ "'a \ 'a \ prop" , infix_ ("\" , 2)),"imp" , \<^here>)), typ "prop \ prop \ prop" , infixr_ ("\" , 1)),"all" , \<^here>)), typ "('a \ prop) \ prop" , binder ("\" , 0, 0)),"prop" , \<^here>)), typ "prop \ prop" , NoSyn),"type" , \<^here>)), typ "'a itself" , NoSyn),"dummy_pattern" , \<^here>)), typ "'a" , Mixfix.mixfix "'_" ),"Appt" , \<^here>)), typ "Pure.proof \ 'a \ Pure.proof" , NoSyn),"AppP" , \<^here>)), typ "Pure.proof \ Pure.proof \ Pure.proof" , NoSyn),"Abst" , \<^here>)), typ "('a \ Pure.proof) \ Pure.proof" , NoSyn),"AbsP" , \<^here>)), typ "prop \ (Pure.proof \ Pure.proof) \ Pure.proof" , NoSyn),"Hyp" , \<^here>)), typ "prop \ Pure.proof" , NoSyn),"Oracle" , \<^here>)), typ "prop \ Pure.proof" , NoSyn),"PClass" , \<^here>)), typ "('a itself \ prop) \ Pure.proof" , NoSyn),"MinProof" , \<^here>)), typ "Pure.proof" , NoSyn)]"Pure.eq" "Pure.imp" "Pure.all" "Pure.type" "Pure.dummy_pattern" "_bracket" , ["\<^type>fun" ]),"_bigimpl" , ["\<^const>Pure.imp" ]),"_TYPE" , ["\<^const>Pure.type" ]),"_TERM" , ["\<^const>Pure.term" ])]"term" , \<^here>)), typ "'a \ prop" , NoSyn),"sort_constraint" , \<^here>)), typ "'a itself \ prop" , NoSyn),"conjunction" , \<^here>)), typ "prop \ prop \ prop" , NoSyn)]"prop_def" , \<^here>),"(CONST Pure.prop :: prop \ prop) (A::prop) \ A::prop" ),"term_def" , \<^here>),"(CONST Pure.term :: 'a \ prop) (x::'a) \ (\A::prop. A \ A)" ),"sort_constraint_def" , \<^here>),"(CONST Pure.sort_constraint :: 'a itself \ prop) (CONST Pure.type :: 'a itself) \\ CONST Pure.term :: 'a itself \ prop) (CONST Pure.type :: ' a itself)"), "conjunction_def" , \<^here>),"(A &&& B) \ (\C::prop. (A \ B \ C) \ C)" )]end ;quality 100%
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
