796 |
796 |
797 section {* Interpretation of Defined Concepts *} |
797 section {* Interpretation of Defined Concepts *} |
798 |
798 |
799 text {* Naming convention for global objects: prefixes D and d *} |
799 text {* Naming convention for global objects: prefixes D and d *} |
800 |
800 |
|
801 |
|
802 subsection {* Simple examples *} |
|
803 |
801 locale Da = fixes a :: o |
804 locale Da = fixes a :: o |
802 assumes true: a |
805 assumes true: a |
803 |
806 |
804 text {* In the following examples, @{term "~ a"} is the defined concept. *} |
807 text {* In the following examples, @{term "~ a"} is the defined concept. *} |
805 |
808 |
806 lemma (in Da) not_false: "~ a <-> False" |
809 lemma (in Da) not_false: "~ a <-> False" |
807 apply simp apply (rule true) done |
810 apply simp apply (rule true) done |
808 |
811 |
809 interpretation D1: Da ["True"] |
812 interpretation D1: Da ["True"] |
810 where "~ True" = "False" |
813 where "~ True == False" |
811 apply - |
814 apply - |
812 apply unfold_locales [1] apply rule |
815 apply unfold_locales [1] apply rule |
813 by simp |
816 by simp |
814 |
817 |
815 thm D1.not_false |
818 thm D1.not_false |
816 lemma "False <-> False" apply (rule D1.not_false) done |
819 lemma "False <-> False" apply (rule D1.not_false) done |
817 |
820 |
818 interpretation D2: Da ["x | ~ x"] |
821 interpretation D2: Da ["x | ~ x"] |
819 where "~ (x | ~ x)" = "~ x & x" |
822 where "~ (x | ~ x) <-> ~ x & x" |
820 apply - |
823 apply - |
821 apply unfold_locales [1] apply fast |
824 apply unfold_locales [1] apply fast |
822 by simp |
825 by simp |
823 |
826 |
824 thm D2.not_false |
827 thm D2.not_false |