summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Tue, 26 Mar 2013 22:09:39 +0100 | |

changeset 51547 | 604d73671fa7 |

parent 51546 | 2e26df807dc7 |

child 51548 | 757fa47af981 |

avoid odd foundational terms after interpretation;
more uniform code setup

src/HOL/GCD.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/GCD.thy Tue Mar 26 21:53:56 2013 +0100 +++ b/src/HOL/GCD.thy Tue Mar 26 22:09:39 2013 +0100 @@ -1545,24 +1545,30 @@ qed simp interpretation gcd_lcm_complete_lattice_nat: - complete_lattice Gcd Lcm gcd "op dvd" "\<lambda>m n::nat. m dvd n \<and> \<not> n dvd m" lcm 1 0 -proof - case goal1 show ?case by simp -next - case goal2 show ?case by simp -next - case goal5 thus ?case by (rule dvd_Lcm_nat) -next - case goal6 thus ?case by simp -next - case goal3 thus ?case by (simp add: Gcd_nat_def) -next - case goal4 thus ?case by (simp add: Gcd_nat_def) + complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat" +where + "complete_lattice.INFI Gcd A f = Gcd (f ` A :: nat set)" + and "complete_lattice.SUPR Lcm A f = Lcm (f ` A)" +proof - + show "class.complete_lattice Gcd Lcm gcd Rings.dvd (\<lambda>m n. m dvd n \<and> \<not> n dvd m) lcm 1 (0::nat)" + proof + case goal1 show ?case by simp + next + case goal2 show ?case by simp + next + case goal5 thus ?case by (rule dvd_Lcm_nat) + next + case goal6 thus ?case by simp + next + case goal3 thus ?case by (simp add: Gcd_nat_def) + next + case goal4 thus ?case by (simp add: Gcd_nat_def) + qed + then interpret gcd_lcm_complete_lattice_nat: + complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat" . + from gcd_lcm_complete_lattice_nat.INF_def show "complete_lattice.INFI Gcd A f = Gcd (f ` A)" . + from gcd_lcm_complete_lattice_nat.SUP_def show "complete_lattice.SUPR Lcm A f = Lcm (f ` A)" . qed -(* bh: This interpretation generates many lemmas about -"complete_lattice.SUPR Lcm" and "complete_lattice.INFI Gcd". -Should we define binder versions of LCM and GCD to correspond -with these? *) lemma Lcm_empty_nat: "Lcm {} = (1::nat)" by (fact gcd_lcm_complete_lattice_nat.Sup_empty) (* already simp *) @@ -1717,11 +1723,12 @@ using assms by (simp add: Gcd_int_def dvd_int_iff) lemma Lcm_set_int [code_unfold]: - "Lcm (set xs) = foldl lcm (1::int) xs" + "Lcm (set xs) = fold lcm xs (1::int)" by (induct xs rule: rev_induct, simp_all add: lcm_commute_int) lemma Gcd_set_int [code_unfold]: - "Gcd (set xs) = foldl gcd (0::int) xs" + "Gcd (set xs) = fold gcd xs (0::int)" by (induct xs rule: rev_induct, simp_all add: gcd_commute_int) end +