145 text {* Note that there is no symbol for strict divisibility. Instead, |
145 text {* Note that there is no symbol for strict divisibility. Instead, |
146 interpretation substitutes @{term "x dvd y \<and> x \<noteq> y"}. *} |
146 interpretation substitutes @{term "x dvd y \<and> x \<noteq> y"}. *} |
147 |
147 |
148 interpretation nat_dvd: lattice ["op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"] |
148 interpretation nat_dvd: lattice ["op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"] |
149 where nat_dvd_meet_eq: |
149 where nat_dvd_meet_eq: |
150 "lattice.meet op dvd (x::nat) y = gcd (x, y)" |
150 "lattice.meet op dvd = gcd" |
151 and nat_dvd_join_eq: |
151 and nat_dvd_join_eq: |
152 "lattice.join op dvd (x::nat) y = lcm (x, y)" |
152 "lattice.join op dvd = lcm" |
153 proof - |
153 proof - |
154 show "lattice (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool)" |
154 show "lattice (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool)" |
155 apply unfold_locales |
155 apply unfold_locales |
156 apply (unfold nat_dvd.is_inf_def nat_dvd.is_sup_def) |
156 apply (unfold nat_dvd.is_inf_def nat_dvd.is_sup_def) |
157 apply (rule_tac x = "gcd (x, y)" in exI) |
157 apply (rule_tac x = "gcd x y" in exI) |
158 apply auto [1] |
158 apply auto [1] |
159 apply (rule_tac x = "lcm (x, y)" in exI) |
159 apply (rule_tac x = "lcm x y" in exI) |
160 apply (auto intro: lcm_dvd1 lcm_dvd2 lcm_least) |
160 apply (auto intro: lcm_dvd1 lcm_dvd2 lcm_least) |
161 done |
161 done |
162 then interpret nat_dvd: lattice ["op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"] . |
162 then interpret nat_dvd: lattice ["op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"] . |
163 show "lattice.meet op dvd (x::nat) y = gcd (x, y)" |
163 show "lattice.meet op dvd = gcd" |
|
164 apply (auto simp add: expand_fun_eq) |
164 apply (unfold nat_dvd.meet_def) |
165 apply (unfold nat_dvd.meet_def) |
165 apply (rule the_equality) |
166 apply (rule the_equality) |
166 apply (unfold nat_dvd.is_inf_def) |
167 apply (unfold nat_dvd.is_inf_def) |
167 by auto |
168 by auto |
168 show "lattice.join op dvd (x::nat) y = lcm (x, y)" |
169 show "lattice.join op dvd = lcm" |
|
170 apply (auto simp add: expand_fun_eq) |
169 apply (unfold nat_dvd.join_def) |
171 apply (unfold nat_dvd.join_def) |
170 apply (rule the_equality) |
172 apply (rule the_equality) |
171 apply (unfold nat_dvd.is_sup_def) |
173 apply (unfold nat_dvd.is_sup_def) |
172 by (auto intro: lcm_dvd1 lcm_dvd2 lcm_least) |
174 by (auto intro: lcm_dvd1 lcm_dvd2 lcm_least) |
173 qed |
175 qed |
194 apply (blast intro: mult_is_0) |
196 apply (blast intro: mult_is_0) |
195 thm mult_is_0 [THEN iffD1] |
197 thm mult_is_0 [THEN iffD1] |
196 *) |
198 *) |
197 |
199 |
198 lemma %invisible gcd_lcm_distr: |
200 lemma %invisible gcd_lcm_distr: |
199 "gcd (x, lcm (y, z)) = lcm (gcd (x, y), gcd (x, z))" |
201 "gcd x (lcm y z) = lcm (gcd x y) (gcd x z)" sorry |
200 sorry |
|
201 |
202 |
202 ML %invisible {* reset quick_and_dirty *} |
203 ML %invisible {* reset quick_and_dirty *} |
203 |
204 |
204 interpretation %visible nat_dvd: |
205 interpretation %visible nat_dvd: |
205 distrib_lattice ["op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"] |
206 distrib_lattice ["op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"] |