# HG changeset patch # User ballarin # Date 1227286939 -3600 # Node ID 2058a6b0eb20b2fa850ddafb10facacd2ff1a3d9 # Parent 686963dbf6cd961aeaebc4b859908a6976ffd0d6 Regression tests for new locale implementation. diff -r 686963dbf6cd -r 2058a6b0eb20 src/FOL/IsaMakefile --- 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 \ diff -r 686963dbf6cd -r 2058a6b0eb20 src/FOL/ex/NewLocaleSetup.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 diff -r 686963dbf6cd -r 2058a6b0eb20 src/FOL/ex/NewLocaleTest.thy --- /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 diff -r 686963dbf6cd -r 2058a6b0eb20 src/FOL/ex/ROOT.ML --- 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"; +