src/FOL/ex/NewLocaleTest.thy
 changeset 28899 7bf5d7f154b8 parent 28898 530c7d28a962 child 28903 b3fc3a62247a
```--- 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```