src/Pure/Isar/isar_syn.ML
changeset 22299 a1293efe7ea5
parent 22239 9ddd3349d597
child 22321 e5cddafe2629
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Feb 10 09:26:17 2007 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Feb 10 09:26:18 2007 +0100
     1.3 @@ -402,6 +402,49 @@
     1.4        >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Locale.interpret Seq.single x y z)));
     1.5  
     1.6  
     1.7 +(* classes *)
     1.8 +
     1.9 +local
    1.10 +
    1.11 +val (classK, instanceK, print_classesK) = ("class", "instance", "print_classes")
    1.12 +
    1.13 +val class_subP = P.name -- Scan.repeat (P.$$$ "+" |-- P.name) >> (op ::);
    1.14 +val class_bodyP = P.!!! (Scan.repeat1 SpecParse.locale_element);
    1.15 +
    1.16 +val parse_arity =
    1.17 +  (P.xname --| P.$$$ "::" -- P.!!! P.arity)
    1.18 +    >> (fn (tyco, (asorts, sort)) => ((tyco, asorts), sort));
    1.19 +
    1.20 +in
    1.21 +
    1.22 +val classP =
    1.23 +  OuterSyntax.command classK "define type class" K.thy_decl (
    1.24 +    P.name --| P.$$$ "="
    1.25 +    -- (
    1.26 +      class_subP --| P.$$$ "+" -- class_bodyP
    1.27 +      || class_subP >> rpair []
    1.28 +      || class_bodyP >> pair [])
    1.29 +    -- P.opt_begin
    1.30 +    >> (fn ((bname, (supclasses, elems)), begin) =>
    1.31 +        Toplevel.begin_local_theory begin
    1.32 +          (ClassPackage.class_e bname supclasses elems #-> TheoryTarget.begin true)));
    1.33 +
    1.34 +val instanceP =
    1.35 +  OuterSyntax.command instanceK "prove type arity or subclass relation" K.thy_goal ((
    1.36 +      P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
    1.37 +           >> ClassPackage.instance_sort_e
    1.38 +      || P.and_list1 parse_arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
    1.39 +           >> (fn (arities, defs) => ClassPackage.instance_arity_e arities defs)
    1.40 +    ) >> (Toplevel.print oo Toplevel.theory_to_proof));
    1.41 +
    1.42 +val print_classesP =
    1.43 +  OuterSyntax.improper_command print_classesK "print classes of this theory" K.diag
    1.44 +    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory
    1.45 +      o Toplevel.keep (ClassPackage.print_classes o Toplevel.theory_of)));
    1.46 +
    1.47 +end;
    1.48 +
    1.49 +
    1.50  
    1.51  (** proof commands **)
    1.52  
    1.53 @@ -939,7 +982,7 @@
    1.54    simproc_setupP, parse_ast_translationP, parse_translationP,
    1.55    print_translationP, typed_print_translationP,
    1.56    print_ast_translationP, token_translationP, oracleP, contextP,
    1.57 -  localeP,
    1.58 +  localeP, classP, instanceP,
    1.59    (*proof commands*)
    1.60    theoremP, lemmaP, corollaryP, haveP, henceP, showP, thusP, fixP,
    1.61    assumeP, presumeP, defP, obtainP, guessP, letP, caseP, thenP, fromP,
    1.62 @@ -950,7 +993,7 @@
    1.63    cannot_undoP, redoP, undos_proofP, undoP, killP, interpretationP,
    1.64    interpretP,
    1.65    (*diagnostic commands*)
    1.66 -  pretty_setmarginP, helpP, print_commandsP, print_contextP,
    1.67 +  pretty_setmarginP, helpP, print_classesP, print_commandsP, print_contextP,
    1.68    print_theoryP, print_syntaxP, print_abbrevsP, print_factsP,
    1.69    print_theoremsP, print_localesP, print_localeP,
    1.70    print_registrationsP, print_attributesP, print_simpsetP,