src/HOL/ex/LocaleTest2.thy
equal inserted replaced
`   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 `
`   602     apply auto `
`   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 *}`