src/FOL/ex/NewLocaleSetup.thy

Interpretation in theories: first version with equations.

(*  Title:      FOL/ex/NewLocaleSetup.thy
    Author:     Clemens Ballarin, TU Muenchen

Testing environment for locale expressions --- experimental.
*)

theory NewLocaleSetup
imports FOL
begin

ML {*

local

structure P = OuterParse and K = OuterKeyword;
val opt_bang = Scan.optional (P.$$$ "!" >> K true) false;

val locale_val =
  SpecParse.locale_expression --
    Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
  Scan.repeat1 SpecParse.context_element >> pair ([], []);

in

val _ =
  OuterSyntax.command "locale" "define named proof context" K.thy_decl
    (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (([], []), []) -- P.opt_begin
      >> (fn ((name, (expr, elems)), begin) =>
          (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
            (Expression.add_locale_cmd name name expr elems #>
              (fn ((target, notes), ctxt) => TheoryTarget.begin target ctxt |>
                fold (fn (kind, facts) => LocalTheory.notes kind facts #> snd) notes))));

val _ =
  OuterSyntax.improper_command "print_locales" "print locales of this theory" K.diag
    (Scan.succeed (Toplevel.no_timing o (Toplevel.unknown_theory o
  Toplevel.keep (NewLocale.print_locales o Toplevel.theory_of))));

val _ = OuterSyntax.improper_command "print_locale" "print named locale in this theory" K.diag
  (opt_bang -- P.xname >> (Toplevel.no_timing oo (fn (show_facts, name) =>
   Toplevel.unknown_theory o Toplevel.keep (fn state =>
     NewLocale.print_locale (Toplevel.theory_of state) show_facts name))));

val _ =
  OuterSyntax.command "interpretation"
    "prove interpretation of locale expression in theory" K.thy_goal
    (P.!!! SpecParse.locale_expression --
      Scan.optional (P.$$$ "where" |-- P.and_list1 (P.alt_string >> Facts.Fact ||
    P.position P.xname -- Scan.option Attrib.thm_sel >> Facts.Named)) []
        >> (fn (expr, mixin) => Toplevel.print o
            Toplevel.theory_to_proof (Expression.interpretation_cmd expr mixin)));

val _ =
  OuterSyntax.command "interpret"
    "prove interpretation of locale expression in proof context"
    (K.tag_proof K.prf_goal)
    (P.!!! SpecParse.locale_expression
        >> (fn expr => Toplevel.print o
            Toplevel.proof' (fn int => Expression.interpret_cmd expr int)));

end

*}

end