src/FOL/ex/NewLocaleSetup.thy
author ballarin
Fri Dec 05 16:41:36 2008 +0100 (2008-12-05)
changeset 29018 17538bdef546
parent 28993 829e684b02ef
child 29028 b5dad96c755a
child 29033 721529248e31
permissions -rw-r--r--
Interpretation in proof contexts.
     1 (*  Title:      FOL/ex/NewLocaleSetup.thy
     2     Author:     Clemens Ballarin, TU Muenchen
     3 
     4 Testing environment for locale expressions --- experimental.
     5 *)
     6 
     7 theory NewLocaleSetup
     8 imports FOL
     9 begin
    10 
    11 ML {*
    12 
    13 local
    14 
    15 structure P = OuterParse and K = OuterKeyword;
    16 val opt_bang = Scan.optional (P.$$$ "!" >> K true) false;
    17 
    18 val locale_val =
    19   Expression.parse_expression --
    20     Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
    21   Scan.repeat1 SpecParse.context_element >> pair ([], []);
    22 
    23 in
    24 
    25 val _ =
    26   OuterSyntax.command "locale" "define named proof context" K.thy_decl
    27     (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (([], []), []) -- P.opt_begin
    28       >> (fn ((name, (expr, elems)), begin) =>
    29           (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
    30             (Expression.add_locale_cmd name name expr elems #-> TheoryTarget.begin)));
    31 
    32 val _ =
    33   OuterSyntax.improper_command "print_locales" "print locales of this theory" K.diag
    34     (Scan.succeed (Toplevel.no_timing o (Toplevel.unknown_theory o
    35   Toplevel.keep (NewLocale.print_locales o Toplevel.theory_of))));
    36 
    37 val _ = OuterSyntax.improper_command "print_locale" "print named locale in this theory" K.diag
    38   (opt_bang -- P.xname >> (Toplevel.no_timing oo (fn (show_facts, name) =>
    39    Toplevel.unknown_theory o Toplevel.keep (fn state =>
    40      NewLocale.print_locale (Toplevel.theory_of state) show_facts name))));
    41 
    42 val _ =
    43   OuterSyntax.command "interpretation"
    44     "prove interpretation of locale expression in theory" K.thy_goal
    45     (P.!!! Expression.parse_expression
    46         >> (fn expr => Toplevel.print o
    47             Toplevel.theory_to_proof (Expression.interpretation_cmd expr)));
    48 
    49 val _ =
    50   OuterSyntax.command "interpret"
    51     "prove interpretation of locale expression in proof context"
    52     (K.tag_proof K.prf_goal)
    53     (P.!!! Expression.parse_expression
    54         >> (fn expr => Toplevel.print o
    55             Toplevel.proof' (fn int => Expression.interpret_cmd expr int)));
    56 
    57 end
    58 
    59 *}
    60 
    61 end