# HG changeset patch
# User ballarin
# Date 1176451350 -7200
# Node ID f792579b6e59ae6a1d35295921670999622fc343
# Parent  263d42253f539a9970e1ca221b303212eb35be30
Experimental code for the interpretation of definitions.

diff -r 263d42253f53 -r f792579b6e59 src/FOL/ex/LocaleTest.thy
--- a/src/FOL/ex/LocaleTest.thy	Fri Apr 13 10:01:43 2007 +0200
+++ b/src/FOL/ex/LocaleTest.thy	Fri Apr 13 10:02:30 2007 +0200
@@ -794,4 +794,44 @@
 
 print_locale! Rc
 
+
+section {* Interpretation of Defined Concepts *}
+
+text {* Naming convention for global objects: prefixes D and d *}
+
+locale Da = fixes a :: o
+  assumes true: a
+
+lemma (in Da) not_false: "~ a <-> False"
+  apply simp apply (rule true) done
+
+interpretation D1: Da ["True"]
+  where "~ True" = "False"
+  apply -
+  apply unfold_locales [1] apply rule
+  by simp
+
+thm D1.not_false
+lemma "False <-> False" apply (rule D1.not_false) done
+
+interpretation D2: Da ["x | ~ x"]
+  where "~ (x | ~ x)" = "~ x & x"
+  apply -
+  apply unfold_locales [1] apply fast
+  by simp
+
+thm D2.not_false
+lemma "~ x & x <-> False" apply (rule D2.not_false) done
+
+print_interps! Da
+
+(* Subscriptions of interpretations *)
+
+lemma (in Da) not_false2: "~a <-> False"
+  apply simp apply (rule true) done
+
+thm D1.not_false2 D2.not_false2
+lemma "False <-> False" apply (rule D1.not_false2) done
+lemma "~x & x <-> False" apply (rule D2.not_false2) done
+
 end