src/FOL/ex/LocaleTest.thy
changeset 22659 f792579b6e59
parent 20469 bb75c1cdf913
child 22757 d3298d63b7b6
equal deleted inserted replaced
22658:263d42253f53 22659:f792579b6e59
   792 locale Rc = Rb +
   792 locale Rc = Rb +
   793   assumes Rc: "True"
   793   assumes Rc: "True"
   794 
   794 
   795 print_locale! Rc
   795 print_locale! Rc
   796 
   796 
       
   797 
       
   798 section {* Interpretation of Defined Concepts *}
       
   799 
       
   800 text {* Naming convention for global objects: prefixes D and d *}
       
   801 
       
   802 locale Da = fixes a :: o
       
   803   assumes true: a
       
   804 
       
   805 lemma (in Da) not_false: "~ a <-> False"
       
   806   apply simp apply (rule true) done
       
   807 
       
   808 interpretation D1: Da ["True"]
       
   809   where "~ True" = "False"
       
   810   apply -
       
   811   apply unfold_locales [1] apply rule
       
   812   by simp
       
   813 
       
   814 thm D1.not_false
       
   815 lemma "False <-> False" apply (rule D1.not_false) done
       
   816 
       
   817 interpretation D2: Da ["x | ~ x"]
       
   818   where "~ (x | ~ x)" = "~ x & x"
       
   819   apply -
       
   820   apply unfold_locales [1] apply fast
       
   821   by simp
       
   822 
       
   823 thm D2.not_false
       
   824 lemma "~ x & x <-> False" apply (rule D2.not_false) done
       
   825 
       
   826 print_interps! Da
       
   827 
       
   828 (* Subscriptions of interpretations *)
       
   829 
       
   830 lemma (in Da) not_false2: "~a <-> False"
       
   831   apply simp apply (rule true) done
       
   832 
       
   833 thm D1.not_false2 D2.not_false2
       
   834 lemma "False <-> False" apply (rule D1.not_false2) done
       
   835 lemma "~x & x <-> False" apply (rule D2.not_false2) done
       
   836 
   797 end
   837 end