Regression tests for new locale implementation.

--- a/src/FOL/IsaMakefile	Fri Nov 21 18:01:39 2008 +0100
+++ b/src/FOL/IsaMakefile	Fri Nov 21 18:02:19 2008 +0100
@@ -47,6 +47,7 @@
 
 $(LOG)/FOL-ex.gz: $(OUT)/FOL ex/First_Order_Logic.thy ex/If.thy		\
   ex/IffOracle.thy ex/LocaleTest.thy ex/Nat.thy ex/Natural_Numbers.thy	\
+  ex/NewLocaleSetup.thy ex/NewLocaleTest.thy    \
   ex/Miniscope.thy ex/Prolog.thy ex/ROOT.ML ex/Classical.thy		\
   ex/document/root.tex ex/Foundation.thy ex/Intuitionistic.thy		\
   ex/Intro.thy ex/Propositional_Int.thy ex/Propositional_Cla.thy	\

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/ex/NewLocaleSetup.thy	Fri Nov 21 18:02:19 2008 +0100
@@ -0,0 +1,47 @@
+(*  Title:      FOL/ex/NewLocaleSetup.thy
+    ID:         $Id$
+    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 =
+  Expression.parse_expression --
+    Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
+  Scan.repeat1 SpecParse.context_element >> pair (Expression.empty_expr, []);
+
+in
+
+val _ =
+  OuterSyntax.command "locale" "define named proof context" K.thy_decl
+    (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) ((Expression.empty_expr, []), []) -- P.opt_begin
+      >> (fn ((name, (expr, elems)), begin) =>
+          (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
+            (Expression.add_locale name name expr elems #-> TheoryTarget.begin)));
+
+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))));
+
+end
+
+*}
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/ex/NewLocaleTest.thy	Fri Nov 21 18:02:19 2008 +0100
@@ -0,0 +1,139 @@
+(*  Title:      FOL/ex/NewLocaleTest.thy
+    ID:         $Id$
+    Author:     Clemens Ballarin, TU Muenchen
+
+Testing environment for locale expressions --- experimental.
+*)
+
+theory NewLocaleTest
+imports NewLocaleSetup
+begin
+
+ML_val {* set new_locales *}
+ML_val {* set Toplevel.debug *}
+ML_val {* set show_hyps *}
+
+
+typedecl int arities int :: "term"
+consts plus :: "int => int => int" (infixl "+" 60)
+  zero :: int ("0")
+  minus :: "int => int" ("- _")
+
+
+text {* Inference of parameter types *}
+
+locale param1 = fixes p
+print_locale! param1
+
+locale param2 = fixes p :: 'a
+print_locale! param2
+
+(*
+locale param_top = param2 r for r :: "'b :: {}"
+print_locale! param_top
+*)
+
+locale param3 = fixes p (infix ".." 50)
+print_locale! param3
+
+locale param4 = fixes p :: "'a => 'a => 'a" (infix ".." 50)
+print_locale! param4
+
+
+text {* Incremental type constraints *}
+
+locale constraint1 =
+  fixes  prod (infixl "**" 65)
+  assumes l_id: "x ** y = x"
+  assumes assoc: "(x ** y) ** z = x ** (y ** z)"
+print_locale! constraint1
+
+locale constraint2 =
+  fixes p and q
+  assumes "p = q"
+print_locale! constraint2
+
+
+text {* Groups *}
+
+locale semi =
+  fixes prod (infixl "**" 65)
+  assumes assoc: "(x ** y) ** z = x ** (y ** z)"
+    and comm: "x ** y = y ** x"
+print_locale! semi thm semi_def
+
+locale lgrp = semi +
+  fixes one and inv
+  assumes lone: "one ** x = x"
+    and linv: "inv(x) ** x = one"
+print_locale! lgrp thm lgrp_def lgrp_axioms_def
+
+locale add_lgrp = semi "op ++" for sum (infixl "++" 60) +
+  fixes zero and neg
+  assumes lzero: "zero ++ x = x"
+    and lneg: "neg(x) ++ x = zero"
+print_locale! add_lgrp thm add_lgrp_def add_lgrp_axioms_def
+
+locale rev_lgrp = semi "%x y. y ++ x" for sum (infixl "++" 60)
+print_locale! rev_lgrp thm rev_lgrp_def
+
+locale hom = f: semi f + g: semi g for f and g
+print_locale! hom thm hom_def
+
+locale perturbation = semi + d: semi "%x y. delta(x) ** delta(y)" for delta
+print_locale! perturbation thm perturbation_def
+
+locale pert_hom = d1: perturbation f d1 + d2: perturbation f d2 for f d1 d2
+print_locale! pert_hom thm pert_hom_def
+
+text {* Alternative expression, obtaining nicer names in @{text "semi f"}. *}
+locale pert_hom' = semi f + d1: perturbation f d1 + d2: perturbation f d2 for f d1 d2
+print_locale! pert_hom' thm pert_hom'_def
+
+
+text {* Logic *}
+
+locale logic =
+  fixes land (infixl "&&" 55)
+    and lnot ("-- _" [60] 60)
+  assumes assoc: "(x && y) && z = x && (y && z)"
+    and notnot: "-- (-- x) = x"
+begin
+
+definition lor (infixl "||" 50) where
+  "x || y = --(-- x && -- y)"
+
+end
+print_locale! logic
+
+locale use_decl = logic + semi "op ||"
+print_locale! use_decl thm use_decl_def
+
+(*
+lemma (in lgrp) lcancel:
+  "x ** y = x ** z <-> y = z"
+proof
+  assume "x ** y = x ** z"
+  then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc)
+  then show "y = z" by (simp add: lone linv)
+qed simp
+*)
+
+locale rgrp = semi +
+  fixes one and inv
+  assumes rone: "x ** one = x"
+    and rinv: "x ** inv(x) = one"
+
+(*
+lemma (in rgrp) rcancel:
+  "y ** x = z ** x <-> y = z"
+proof
+  assume "y ** x = z ** x"
+  then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"
+    by (simp add: assoc [symmetric])
+  then show "y = z" by (simp add: rone rinv)
+qed simp
+*)
+
+
+end

--- a/src/FOL/ex/ROOT.ML	Fri Nov 21 18:01:39 2008 +0100
+++ b/src/FOL/ex/ROOT.ML	Fri Nov 21 18:02:19 2008 +0100
@@ -30,3 +30,5 @@
 
 (*regression test for locales -- sets several global flags!*)
 no_document use_thy "LocaleTest";
+no_document use_thy "NewLocaleTest";
+