# HG changeset patch # User haftmann # Date 1388094469 -3600 # Node ID c21a2465cac1875153e78afea017e3db414ee343 # Parent 7b9a67cbd48f189cf391a69b5f60ef0339b746e3 prefer ephemeral interpretation over interpretation in proof contexts; prefer context begin ... end blocks for often-occuring assumptions; slightly more complete interpretations into abstract algebraic structures for gcd/lcm diff -r 7b9a67cbd48f -r c21a2465cac1 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Wed Dec 25 22:35:29 2013 +0100 +++ b/src/HOL/Finite_Set.thy Thu Dec 26 22:47:49 2013 +0100 @@ -1085,6 +1085,9 @@ assumes comp_fun_commute: "f y \ f x = f x \ f y" begin +interpretation comp_fun_commute f + by default (insert comp_fun_commute, simp add: fun_eq_iff) + definition F :: "'a set \ 'b" where eq_fold: "F A = fold f z A" @@ -1101,8 +1104,6 @@ assumes "finite A" and "x \ A" shows "F (insert x A) = f x (F A)" proof - - interpret comp_fun_commute f - by default (insert comp_fun_commute, simp add: fun_eq_iff) from fold_insert assms have "fold f z (insert x A) = f x (fold f z A)" by simp with `finite A` show ?thesis by (simp add: eq_fold fun_eq_iff) @@ -1134,12 +1135,13 @@ declare insert [simp del] +interpretation comp_fun_idem f + by default (insert comp_fun_commute comp_fun_idem, simp add: fun_eq_iff) + lemma insert_idem [simp]: assumes "finite A" shows "F (insert x A) = f x (F A)" proof - - interpret comp_fun_idem f - by default (insert comp_fun_commute comp_fun_idem, simp add: fun_eq_iff) from fold_insert_idem assms have "fold f z (insert x A) = f x (fold f z A)" by simp with `finite A` show ?thesis by (simp add: eq_fold fun_eq_iff) diff -r 7b9a67cbd48f -r c21a2465cac1 src/HOL/GCD.thy --- a/src/HOL/GCD.thy Wed Dec 25 22:35:29 2013 +0100 +++ b/src/HOL/GCD.thy Thu Dec 26 22:47:49 2013 +0100 @@ -197,14 +197,14 @@ by (simp add: lcm_int_def) (* was gcd_0, etc. *) -lemma gcd_0_nat [simp]: "gcd (x::nat) 0 = x" +lemma gcd_0_nat: "gcd (x::nat) 0 = x" by simp (* was igcd_0, etc. *) lemma gcd_0_int [simp]: "gcd (x::int) 0 = abs x" by (unfold gcd_int_def, auto) -lemma gcd_0_left_nat [simp]: "gcd 0 (x::nat) = x" +lemma gcd_0_left_nat: "gcd 0 (x::nat) = x" by simp lemma gcd_0_left_int [simp]: "gcd 0 (x::int) = abs x" @@ -243,7 +243,7 @@ lemma gcd_dvd1_nat [iff]: "(gcd (m::nat)) n dvd m" and gcd_dvd2_nat [iff]: "(gcd m n) dvd n" apply (induct m n rule: gcd_nat_induct) - apply (simp_all add: gcd_non_0_nat) + apply (simp_all add: gcd_non_0_nat gcd_0_nat) apply (blast dest: dvd_mod_imp_dvd) done @@ -278,7 +278,7 @@ by (rule zdvd_imp_le, auto) lemma gcd_greatest_nat: "(k::nat) dvd m \ k dvd n \ k dvd gcd m n" -by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod) +by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod gcd_0_nat) lemma gcd_greatest_int: "(k::int) dvd m \ k dvd n \ k dvd gcd m n" @@ -307,25 +307,6 @@ lemma gcd_pos_int [simp]: "(gcd (m::int) n > 0) = (m ~= 0 | n ~= 0)" by (insert gcd_zero_int [of m n], insert gcd_ge_0_int [of m n], arith) -interpretation gcd_nat: abel_semigroup "gcd :: nat \ nat \ nat" -proof -qed (auto intro: dvd_antisym dvd_trans) - -interpretation gcd_int: abel_semigroup "gcd :: int \ int \ int" -proof -qed (simp_all add: gcd_int_def gcd_nat.assoc gcd_nat.commute gcd_nat.left_commute) - -lemmas gcd_assoc_nat = gcd_nat.assoc -lemmas gcd_commute_nat = gcd_nat.commute -lemmas gcd_left_commute_nat = gcd_nat.left_commute -lemmas gcd_assoc_int = gcd_int.assoc -lemmas gcd_commute_int = gcd_int.commute -lemmas gcd_left_commute_int = gcd_int.left_commute - -lemmas gcd_ac_nat = gcd_assoc_nat gcd_commute_nat gcd_left_commute_nat - -lemmas gcd_ac_int = gcd_assoc_int gcd_commute_int gcd_left_commute_int - lemma gcd_unique_nat: "(d::nat) dvd a \ d dvd b \ (\e. e dvd a \ e dvd b \ e dvd d) \ d = gcd a b" apply auto @@ -343,18 +324,40 @@ apply (auto intro: gcd_greatest_int) done +interpretation gcd_nat: abel_semigroup "gcd :: nat \ nat \ nat" + + gcd_nat: semilattice_neutr_order "gcd :: nat \ nat \ nat" 0 "op dvd" "(\m n. m dvd n \ \ n dvd m)" +apply default +apply (auto intro: dvd_antisym dvd_trans)[4] +apply (metis dvd.dual_order.refl gcd_unique_nat) +apply (auto intro: dvdI elim: dvdE) +done + +interpretation gcd_int: abel_semigroup "gcd :: int \ int \ int" +proof +qed (simp_all add: gcd_int_def gcd_nat.assoc gcd_nat.commute gcd_nat.left_commute) + +lemmas gcd_assoc_nat = gcd_nat.assoc +lemmas gcd_commute_nat = gcd_nat.commute +lemmas gcd_left_commute_nat = gcd_nat.left_commute +lemmas gcd_assoc_int = gcd_int.assoc +lemmas gcd_commute_int = gcd_int.commute +lemmas gcd_left_commute_int = gcd_int.left_commute + +lemmas gcd_ac_nat = gcd_assoc_nat gcd_commute_nat gcd_left_commute_nat + +lemmas gcd_ac_int = gcd_assoc_int gcd_commute_int gcd_left_commute_int + lemma gcd_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \ gcd x y = x" -by (metis dvd.eq_iff gcd_unique_nat) + by (fact gcd_nat.absorb1) lemma gcd_proj2_if_dvd_nat [simp]: "(y::nat) dvd x \ gcd x y = y" -by (metis dvd.eq_iff gcd_unique_nat) + by (fact gcd_nat.absorb2) -lemma gcd_proj1_if_dvd_int[simp]: "x dvd y \ gcd (x::int) y = abs x" -by (metis abs_dvd_iff abs_eq_0 gcd_0_left_int gcd_abs_int gcd_unique_int) +lemma gcd_proj1_if_dvd_int [simp]: "x dvd y \ gcd (x::int) y = abs x" + by (metis abs_dvd_iff gcd_0_left_int gcd_abs_int gcd_unique_int) -lemma gcd_proj2_if_dvd_int[simp]: "y dvd x \ gcd (x::int) y = abs y" -by (metis gcd_proj1_if_dvd_int gcd_commute_int) - +lemma gcd_proj2_if_dvd_int [simp]: "y dvd x \ gcd (x::int) y = abs y" + by (metis gcd_proj1_if_dvd_int gcd_commute_int) text {* \medskip Multiplication laws @@ -1391,12 +1394,17 @@ by (auto intro: dvd_antisym [transferred] lcm_least_int) interpretation lcm_nat: abel_semigroup "lcm :: nat \ nat \ nat" + + lcm_nat: semilattice_neutr "lcm :: nat \ nat \ nat" 1 proof fix n m p :: nat show "lcm (lcm n m) p = lcm n (lcm m p)" by (rule lcm_unique_nat [THEN iffD1]) (metis dvd.order_trans lcm_unique_nat) show "lcm m n = lcm n m" by (simp add: lcm_nat_def gcd_commute_nat field_simps) + show "lcm m m = m" + by (metis dvd.order_refl lcm_unique_nat) + show "lcm m 1 = m" + by (metis dvd.dual_order.refl lcm_unique_nat one_dvd) qed interpretation lcm_int: abel_semigroup "lcm :: int \ int \ int" @@ -1478,10 +1486,6 @@ subsection {* The complete divisibility lattice *} -lemma semilattice_neutr_set_lcm_one_nat: - "semilattice_neutr_set lcm (1::nat)" - by default simp_all - interpretation gcd_semilattice_nat: semilattice_inf gcd "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" proof case goal3 thus ?case by(metis gcd_unique_nat) @@ -1508,28 +1512,19 @@ definition "Lcm (M::nat set) = (if finite M then semilattice_neutr_set.F lcm 1 M else 0)" +interpretation semilattice_neutr_set lcm "1::nat" .. + lemma Lcm_nat_infinite: "\ finite M \ Lcm M = (0::nat)" by (simp add: Lcm_nat_def) lemma Lcm_nat_empty: "Lcm {} = (1::nat)" -proof - - interpret semilattice_neutr_set lcm "1::nat" - by (fact semilattice_neutr_set_lcm_one_nat) - show ?thesis by (simp add: Lcm_nat_def) -qed + by (simp add: Lcm_nat_def) lemma Lcm_nat_insert: "Lcm (insert n M) = lcm (n::nat) (Lcm M)" -proof (cases "finite M") - interpret semilattice_neutr_set lcm "1::nat" - by (fact semilattice_neutr_set_lcm_one_nat) - case True - then show ?thesis by (simp add: Lcm_nat_def) -next - case False then show ?thesis by (simp add: Lcm_nat_infinite) -qed + by (cases "finite M") (simp_all add: Lcm_nat_def Lcm_nat_infinite) definition "Gcd (M::nat set) = Lcm {d. \m\M. d dvd m}" @@ -1587,7 +1582,7 @@ qed lemma Lcm_empty_nat: "Lcm {} = (1::nat)" - by (fact gcd_lcm_complete_lattice_nat.Sup_empty) (* already simp *) + by (fact Lcm_nat_empty) lemma Gcd_empty_nat: "Gcd {} = (0::nat)" by (fact gcd_lcm_complete_lattice_nat.Inf_empty) (* already simp *) @@ -1688,6 +1683,7 @@ lemma lcm_eq_nitpick_lcm [nitpick_unfold]: "lcm x y = Nitpick.nat_lcm x y" by (simp only: lcm_nat_def Nitpick.nat_lcm_def gcd_eq_nitpick_gcd) + subsubsection {* Setwise gcd and lcm for integers *} instantiation int :: Gcd diff -r 7b9a67cbd48f -r c21a2465cac1 src/HOL/Quotient.thy --- a/src/HOL/Quotient.thy Wed Dec 25 22:35:29 2013 +0100 +++ b/src/HOL/Quotient.thy Thu Dec 26 22:47:49 2013 +0100 @@ -46,75 +46,94 @@ shows "Quotient3 R Abs Rep" using assms unfolding Quotient3_def by blast -lemma Quotient3_abs_rep: +context + fixes R Abs Rep assumes a: "Quotient3 R Abs Rep" - shows "Abs (Rep a) = a" +begin + +lemma Quotient3_abs_rep: + "Abs (Rep a) = a" using a unfolding Quotient3_def by simp lemma Quotient3_rep_reflp: - assumes a: "Quotient3 R Abs Rep" - shows "R (Rep a) (Rep a)" + "R (Rep a) (Rep a)" using a unfolding Quotient3_def by blast lemma Quotient3_rel: - assumes a: "Quotient3 R Abs Rep" - shows "R r r \ R s s \ Abs r = Abs s \ R r s" -- {* orientation does not loop on rewriting *} + "R r r \ R s s \ Abs r = Abs s \ R r s" -- {* orientation does not loop on rewriting *} using a unfolding Quotient3_def by blast lemma Quotient3_refl1: - assumes a: "Quotient3 R Abs Rep" - shows "R r s \ R r r" + "R r s \ R r r" using a unfolding Quotient3_def by fast lemma Quotient3_refl2: - assumes a: "Quotient3 R Abs Rep" - shows "R r s \ R s s" + "R r s \ R s s" using a unfolding Quotient3_def by fast lemma Quotient3_rel_rep: - assumes a: "Quotient3 R Abs Rep" - shows "R (Rep a) (Rep b) \ a = b" + "R (Rep a) (Rep b) \ a = b" using a unfolding Quotient3_def by metis lemma Quotient3_rep_abs: - assumes a: "Quotient3 R Abs Rep" - shows "R r r \ R (Rep (Abs r)) r" + "R r r \ R (Rep (Abs r)) r" using a unfolding Quotient3_def by blast lemma Quotient3_rel_abs: - assumes a: "Quotient3 R Abs Rep" - shows "R r s \ Abs r = Abs s" + "R r s \ Abs r = Abs s" using a unfolding Quotient3_def by blast lemma Quotient3_symp: - assumes a: "Quotient3 R Abs Rep" - shows "symp R" + "symp R" using a unfolding Quotient3_def using sympI by metis lemma Quotient3_transp: - assumes a: "Quotient3 R Abs Rep" - shows "transp R" + "transp R" using a unfolding Quotient3_def using transpI by (metis (full_types)) lemma Quotient3_part_equivp: - assumes a: "Quotient3 R Abs Rep" - shows "part_equivp R" -by (metis Quotient3_rep_reflp Quotient3_symp Quotient3_transp a part_equivpI) + "part_equivp R" + by (metis Quotient3_rep_reflp Quotient3_symp Quotient3_transp part_equivpI) + +lemma abs_o_rep: + "Abs o Rep = id" + unfolding fun_eq_iff + by (simp add: Quotient3_abs_rep) + +lemma equals_rsp: + assumes b: "R xa xb" "R ya yb" + shows "R xa ya = R xb yb" + using b Quotient3_symp Quotient3_transp + by (blast elim: sympE transpE) + +lemma rep_abs_rsp: + assumes b: "R x1 x2" + shows "R x1 (Rep (Abs x2))" + using b Quotient3_rel Quotient3_abs_rep Quotient3_rep_reflp + by metis + +lemma rep_abs_rsp_left: + assumes b: "R x1 x2" + shows "R (Rep (Abs x1)) x2" + using b Quotient3_rel Quotient3_abs_rep Quotient3_rep_reflp + by metis + +end lemma identity_quotient3: - shows "Quotient3 (op =) id id" + "Quotient3 (op =) id id" unfolding Quotient3_def id_def by blast @@ -157,19 +176,6 @@ ultimately show ?thesis by (intro Quotient3I) (assumption+) qed -lemma abs_o_rep: - assumes a: "Quotient3 R Abs Rep" - shows "Abs o Rep = id" - unfolding fun_eq_iff - by (simp add: Quotient3_abs_rep[OF a]) - -lemma equals_rsp: - assumes q: "Quotient3 R Abs Rep" - and a: "R xa xb" "R ya yb" - shows "R xa ya = R xb yb" - using a Quotient3_symp[OF q] Quotient3_transp[OF q] - by (blast elim: sympE transpE) - lemma lambda_prs: assumes q1: "Quotient3 R1 Abs1 Rep1" and q2: "Quotient3 R2 Abs2 Rep2" @@ -186,20 +192,6 @@ using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2] by simp -lemma rep_abs_rsp: - assumes q: "Quotient3 R Abs Rep" - and a: "R x1 x2" - shows "R x1 (Rep (Abs x2))" - using a Quotient3_rel[OF q] Quotient3_abs_rep[OF q] Quotient3_rep_reflp[OF q] - by metis - -lemma rep_abs_rsp_left: - assumes q: "Quotient3 R Abs Rep" - and a: "R x1 x2" - shows "R (Rep (Abs x1)) x2" - using a Quotient3_rel[OF q] Quotient3_abs_rep[OF q] Quotient3_rep_reflp[OF q] - by metis - text{* In the following theorem R1 can be instantiated with anything, but we know some of the types of the Rep and Abs functions;