src/HOL/ex/LocaleTest2.thy
changeset 23951 b188cac107ad
parent 23919 af871d13e320
child 24946 a7bcad413799
equal deleted inserted replaced
23950:f54c0e339061 23951:b188cac107ad
   599     apply unfold_locales
   599     apply unfold_locales
   600     apply (unfold nat_dvd.is_inf_def nat_dvd.is_sup_def)
   600     apply (unfold nat_dvd.is_inf_def nat_dvd.is_sup_def)
   601     apply (rule_tac x = "gcd (x, y)" in exI)
   601     apply (rule_tac x = "gcd (x, y)" in exI)
   602     apply auto [1]
   602     apply auto [1]
   603     apply (rule_tac x = "lcm (x, y)" in exI)
   603     apply (rule_tac x = "lcm (x, y)" in exI)
   604     apply (auto intro: lcm_dvd1 lcm_dvd2 lcm_lowest)
   604     apply (auto intro: lcm_dvd1 lcm_dvd2 lcm_least)
   605     done
   605     done
   606   then interpret nat_dvd: dlat ["op dvd :: [nat, nat] => bool"] .
   606   then interpret nat_dvd: dlat ["op dvd :: [nat, nat] => bool"] .
   607   txt {* Interpretation to ease use of definitions, which are
   607   txt {* Interpretation to ease use of definitions, which are
   608     conditional in general but unconditional after interpretation. *}
   608     conditional in general but unconditional after interpretation. *}
   609   show "dlat.meet (op dvd) (x::nat) y = gcd (x, y)"
   609   show "dlat.meet (op dvd) (x::nat) y = gcd (x, y)"
   613     by auto
   613     by auto
   614   show "dlat.join (op dvd) (x::nat) y = lcm (x, y)"
   614   show "dlat.join (op dvd) (x::nat) y = lcm (x, y)"
   615     apply (unfold nat_dvd.join_def)
   615     apply (unfold nat_dvd.join_def)
   616     apply (rule the_equality)
   616     apply (rule the_equality)
   617     apply (unfold nat_dvd.is_sup_def)
   617     apply (unfold nat_dvd.is_sup_def)
   618     by (auto intro: lcm_dvd1 lcm_dvd2 lcm_lowest)
   618     by (auto intro: lcm_dvd1 lcm_dvd2 lcm_least)
   619 qed
   619 qed
   620 
   620 
   621 text {* Interpreted theorems from the locales, involving defined terms. *}
   621 text {* Interpreted theorems from the locales, involving defined terms. *}
   622 
   622 
   623 thm nat_dvd.less_def text {* from dpo *}
   623 thm nat_dvd.less_def text {* from dpo *}