src/Pure/pure_thy.ML
changeset 26436 dfd6947ab5c2
parent 26430 8ddb2e7c5a1e
child 26457 9385d441cec6
equal deleted inserted replaced
26435:bdce320cd426 26436:dfd6947ab5c2
    70     theory -> thm list * theory
    70     theory -> thm list * theory
    71   val add_defs_unchecked: bool -> ((bstring * string) * attribute list) list ->
    71   val add_defs_unchecked: bool -> ((bstring * string) * attribute list) list ->
    72     theory -> thm list * theory
    72     theory -> thm list * theory
    73   val add_defs_unchecked_i: bool -> ((bstring * term) * attribute list) list ->
    73   val add_defs_unchecked_i: bool -> ((bstring * term) * attribute list) list ->
    74     theory -> thm list * theory
    74     theory -> thm list * theory
    75   val appl_syntax: (string * typ * mixfix) list
       
    76   val applC_syntax: (string * typ * mixfix) list
       
    77 end;
    75 end;
    78 
    76 
    79 structure PureThy: PURE_THY =
    77 structure PureThy: PURE_THY =
    80 struct
    78 struct
    81 
    79 
   425 
   423 
   426 val typ = SimpleSyntax.read_typ;
   424 val typ = SimpleSyntax.read_typ;
   427 val term = SimpleSyntax.read_term;
   425 val term = SimpleSyntax.read_term;
   428 val prop = SimpleSyntax.read_prop;
   426 val prop = SimpleSyntax.read_prop;
   429 
   427 
   430 val appl_syntax =
       
   431  [("_appl", typ "('b => 'a) => args => logic", Mixfix ("(1_/(1'(_')))", [1000, 0], 1000)),
       
   432   ("_appl", typ "('b => 'a) => args => aprop", Mixfix ("(1_/(1'(_')))", [1000, 0], 1000))];
       
   433 
       
   434 val applC_syntax =
       
   435  [("",       typ "'a => cargs",                  Delimfix "_"),
       
   436   ("_cargs", typ "'a => cargs => cargs",         Mixfix ("_/ _", [1000, 1000], 1000)),
       
   437   ("_applC", typ "('b => 'a) => cargs => logic", Mixfix ("(1_/ _)", [1000, 1000], 999)),
       
   438   ("_applC", typ "('b => 'a) => cargs => aprop", Mixfix ("(1_/ _)", [1000, 1000], 999))];
       
   439 
       
   440 val _ = Context.>>
   428 val _ = Context.>>
   441   (Sign.add_types
   429   (Sign.add_types
   442    [("fun", 2, NoSyn),
   430    [("fun", 2, NoSyn),
   443     ("prop", 0, NoSyn),
   431     ("prop", 0, NoSyn),
   444     ("itself", 1, NoSyn),
   432     ("itself", 1, NoSyn),
   445     ("dummy", 0, NoSyn)]
   433     ("dummy", 0, NoSyn)]
   446   #> Sign.add_nonterminals Syntax.basic_nonterms
   434   #> Sign.add_nonterminals Syntax.basic_nonterms
   447   #> Sign.add_syntax_i
   435   #> Sign.add_syntax_i
   448    [("_lambda",     typ "pttrns => 'a => logic",     Mixfix ("(3%_./ _)", [0, 3], 3)),
   436    [("_lambda",     typ "pttrns => 'a => logic",       Mixfix ("(3%_./ _)", [0, 3], 3)),
   449     ("_abs",        typ "'a",                        NoSyn),
   437     ("_abs",        typ "'a",                          NoSyn),
   450     ("",            typ "'a => args",                Delimfix "_"),
   438     ("",            typ "'a => args",                  Delimfix "_"),
   451     ("_args",       typ "'a => args => args",        Delimfix "_,/ _"),
   439     ("_args",       typ "'a => args => args",          Delimfix "_,/ _"),
   452     ("",            typ "id => idt",                 Delimfix "_"),
   440     ("",            typ "id => idt",                   Delimfix "_"),
   453     ("_idtdummy",   typ "idt",                       Delimfix "'_"),
   441     ("_idtdummy",   typ "idt",                         Delimfix "'_"),
   454     ("_idtyp",      typ "id => type => idt",         Mixfix ("_::_", [], 0)),
   442     ("_idtyp",      typ "id => type => idt",           Mixfix ("_::_", [], 0)),
   455     ("_idtypdummy", typ "type => idt",               Mixfix ("'_()::_", [], 0)),
   443     ("_idtypdummy", typ "type => idt",                 Mixfix ("'_()::_", [], 0)),
   456     ("",            typ "idt => idt",                Delimfix "'(_')"),
   444     ("",            typ "idt => idt",                  Delimfix "'(_')"),
   457     ("",            typ "idt => idts",               Delimfix "_"),
   445     ("",            typ "idt => idts",                 Delimfix "_"),
   458     ("_idts",       typ "idt => idts => idts",       Mixfix ("_/ _", [1, 0], 0)),
   446     ("_idts",       typ "idt => idts => idts",         Mixfix ("_/ _", [1, 0], 0)),
   459     ("",            typ "idt => pttrn",              Delimfix "_"),
   447     ("",            typ "idt => pttrn",                Delimfix "_"),
   460     ("",            typ "pttrn => pttrns",           Delimfix "_"),
   448     ("",            typ "pttrn => pttrns",             Delimfix "_"),
   461     ("_pttrns",     typ "pttrn => pttrns => pttrns", Mixfix ("_/ _", [1, 0], 0)),
   449     ("_pttrns",     typ "pttrn => pttrns => pttrns",   Mixfix ("_/ _", [1, 0], 0)),
   462     ("",            typ "id => aprop",               Delimfix "_"),
   450     ("",            typ "id => aprop",                 Delimfix "_"),
   463     ("",            typ "longid => aprop",           Delimfix "_"),
   451     ("",            typ "longid => aprop",             Delimfix "_"),
   464     ("",            typ "var => aprop",              Delimfix "_"),
   452     ("",            typ "var => aprop",                Delimfix "_"),
   465     ("_DDDOT",      typ "aprop",                     Delimfix "..."),
   453     ("_DDDOT",      typ "aprop",                       Delimfix "..."),
   466     ("_aprop",      typ "aprop => prop",             Delimfix "PROP _"),
   454     ("_aprop",      typ "aprop => prop",               Delimfix "PROP _"),
   467     ("_asm",        typ "prop => asms",              Delimfix "_"),
   455     ("_asm",        typ "prop => asms",                Delimfix "_"),
   468     ("_asms",       typ "prop => asms => asms",      Delimfix "_;/ _"),
   456     ("_asms",       typ "prop => asms => asms",        Delimfix "_;/ _"),
   469     ("_bigimpl",    typ "asms => prop => prop",      Mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)),
   457     ("_bigimpl",    typ "asms => prop => prop",        Mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)),
   470     ("_ofclass",    typ "type => logic => prop",     Delimfix "(1OFCLASS/(1'(_,/ _')))"),
   458     ("_ofclass",    typ "type => logic => prop",       Delimfix "(1OFCLASS/(1'(_,/ _')))"),
   471     ("_mk_ofclass", typ "dummy",                     NoSyn),
   459     ("_mk_ofclass", typ "dummy",                       NoSyn),
   472     ("_TYPE",       typ "type => logic",             Delimfix "(1TYPE/(1'(_')))"),
   460     ("_TYPE",       typ "type => logic",               Delimfix "(1TYPE/(1'(_')))"),
   473     ("",            typ "id => logic",               Delimfix "_"),
   461     ("",            typ "id => logic",                 Delimfix "_"),
   474     ("",            typ "longid => logic",           Delimfix "_"),
   462     ("",            typ "longid => logic",             Delimfix "_"),
   475     ("",            typ "var => logic",              Delimfix "_"),
   463     ("",            typ "var => logic",                Delimfix "_"),
   476     ("_DDDOT",      typ "logic",                     Delimfix "..."),
   464     ("_DDDOT",      typ "logic",                       Delimfix "..."),
   477     ("_constify",   typ "num => num_const",          Delimfix "_"),
   465     ("_constify",   typ "num => num_const",            Delimfix "_"),
   478     ("_indexnum",   typ "num_const => index",        Delimfix "\\<^sub>_"),
   466     ("_indexnum",   typ "num_const => index",          Delimfix "\\<^sub>_"),
   479     ("_index",      typ "logic => index",            Delimfix "(00\\<^bsub>_\\<^esub>)"),
   467     ("_index",      typ "logic => index",              Delimfix "(00\\<^bsub>_\\<^esub>)"),
   480     ("_indexdefault", typ "index",                   Delimfix ""),
   468     ("_indexdefault", typ "index",                     Delimfix ""),
   481     ("_indexvar",   typ "index",                     Delimfix "'\\<index>"),
   469     ("_indexvar",   typ "index",                       Delimfix "'\\<index>"),
   482     ("_struct",     typ "index => logic",            Mixfix ("\\<struct>_", [1000], 1000)),
   470     ("_struct",     typ "index => logic",              Mixfix ("\\<struct>_", [1000], 1000)),
   483     ("==>",         typ "prop => prop => prop",      Delimfix "op ==>"),
   471     ("==>",         typ "prop => prop => prop",        Delimfix "op ==>"),
   484     (Term.dummy_patternN, typ "aprop",               Delimfix "'_")]
   472     (Term.dummy_patternN, typ "aprop",                 Delimfix "'_"),
   485   #> Sign.add_syntax_i appl_syntax
   473     ("_appl",       typ "('b => 'a) => args => logic", Mixfix ("(1_/(1'(_')))", [1000, 0], 1000)),
       
   474     ("_appl",       typ "('b => 'a) => args => aprop", Mixfix ("(1_/(1'(_')))", [1000, 0], 1000))]
   486   #> Sign.add_modesyntax_i (Symbol.xsymbolsN, true)
   475   #> Sign.add_modesyntax_i (Symbol.xsymbolsN, true)
   487    [("fun",      typ "type => type => type",   Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
   476    [("fun",      typ "type => type => type",   Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
   488     ("_bracket", typ "types => type => type",  Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
   477     ("_bracket", typ "types => type => type",  Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
   489     ("_ofsort",  typ "tid => sort => type",    Mixfix ("_\\<Colon>_", [1000, 0], 1000)),
   478     ("_ofsort",  typ "tid => sort => type",    Mixfix ("_\\<Colon>_", [1000, 0], 1000)),
   490     ("_constrain", typ "'a => type => 'a",     Mixfix ("_\\<Colon>_", [4, 0], 3)),
   479     ("_constrain", typ "'a => type => 'a",     Mixfix ("_\\<Colon>_", [4, 0], 3)),