# HG changeset patch # User haftmann # Date 1364332179 -3600 # Node ID 604d73671fa73ef0a9e8269bc4b198dd4f51baf0 # Parent 2e26df807dc724da57ead9b920813bf8c7b58fbd avoid odd foundational terms after interpretation; more uniform code setup diff -r 2e26df807dc7 -r 604d73671fa7 src/HOL/GCD.thy --- 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" "\m n::nat. m dvd n \ \ 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 "\m n. m dvd n \ \ 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 (\m n. m dvd n \ \ 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 "\m n. m dvd n \ \ 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 +