--- a/src/FOL/ex/NewLocaleTest.thy Thu Nov 27 21:25:34 2008 +0100
+++ b/src/FOL/ex/NewLocaleTest.thy Fri Nov 28 11:14:13 2008 +0100
@@ -217,9 +217,47 @@
print_locale! lgrp
+(* Duality *)
+
+locale order =
+ fixes less :: "'a => 'a => o" (infix "<<" 50)
+ assumes refl: "x << x"
+ and trans: "[| x << y; y << z |] ==> x << z"
+
+sublocale order < dual: order "%x y. y << x"
+ apply (rule order.intro) apply (rule refl) apply (blast intro: trans)
+ done
+
+print_locale! order (* Only two instances of order. *)
+
+locale order' =
+ fixes less :: "'a => 'a => o" (infix "<<" 50)
+ assumes refl: "x << x"
+ and trans: "[| x << y; y << z |] ==> x << z"
+
+locale order_with_def = order'
+begin
+
+definition greater :: "'a => 'a => o" (infix ">>" 50) where
+ "x >> y <-> y << x"
+
+end
+
+sublocale order_with_def < dual: order' "op >>"
+ apply (intro order'.intro)
+ unfolding greater_def
+ apply (rule refl) apply (blast intro: trans)
+ done
+
+print_locale! order_with_def
+(* Note that decls come after theorems that make use of them.
+ Appears to be harmless at least in this example. *)
+
+
(* locale with many parameters ---
interpretations generate alternating group A5 *)
+
locale A5 =
fixes A and B and C and D and E
assumes eq: "A <-> B <-> C <-> D <-> E"
@@ -259,4 +297,9 @@
context trivial begin thm x.Q [where ?x = True] end
+sublocale trivial < y: trivial Q Q
+ apply (intro trivial.intro) using Q by fast
+
+print_locale! trivial (* No instance for y created (subsumed). *)
+
end