# HG changeset patch # User haftmann # Date 1433177960 -7200 # Node ID 063698416239cb621b8c870a0fbf4126a383fa19 # Parent df9b153d866b2c47ec8a4159876f0f85ac44b9fd correct sort constraints for abbreviations in type classes * * * yet another bunch of corrections diff -r df9b153d866b -r 063698416239 src/HOL/Library/Extended.thy --- a/src/HOL/Library/Extended.thy Mon Jun 01 18:59:20 2015 +0200 +++ b/src/HOL/Library/Extended.thy Mon Jun 01 18:59:20 2015 +0200 @@ -25,7 +25,7 @@ case_of_simps less_eq_extended_case: less_eq_extended.simps definition less_extended :: "'a extended \ 'a extended \ bool" where -"((x::'a extended) < y) = (x \ y & \ x \ y)" +"((x::'a extended) < y) = (x \ y & \ y \ x)" instance by intro_classes (auto simp: less_extended_def less_eq_extended_case split: extended.splits) diff -r df9b153d866b -r 063698416239 src/HOL/Parity.thy --- a/src/HOL/Parity.thy Mon Jun 01 18:59:20 2015 +0200 +++ b/src/HOL/Parity.thy Mon Jun 01 18:59:20 2015 +0200 @@ -118,75 +118,60 @@ subsection {* Instances for @{typ nat} and @{typ int} *} lemma even_Suc_Suc_iff [simp]: - "even (Suc (Suc n)) \ even n" + "2 dvd Suc (Suc n) \ 2 dvd n" using dvd_add_triv_right_iff [of 2 n] by simp lemma even_Suc [simp]: - "even (Suc n) \ odd n" + "2 dvd Suc n \ \ 2 dvd n" by (induct n) auto lemma even_diff_nat [simp]: fixes m n :: nat - shows "even (m - n) \ m < n \ even (m + n)" + shows "2 dvd (m - n) \ m < n \ 2 dvd (m + n)" proof (cases "n \ m") case True then have "m - n + n * 2 = m + n" by (simp add: mult_2_right) - moreover have "even (m - n) \ even (m - n + n * 2)" by simp - ultimately have "even (m - n) \ even (m + n)" by (simp only:) + moreover have "2 dvd (m - n) \ 2 dvd (m - n + n * 2)" by simp + ultimately have "2 dvd (m - n) \ 2 dvd (m + n)" by (simp only:) then show ?thesis by auto next case False then show ?thesis by simp qed -lemma even_diff_iff [simp]: - fixes k l :: int - shows "even (k - l) \ even (k + l)" - using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right) - -lemma even_abs_add_iff [simp]: - fixes k l :: int - shows "even (\k\ + l) \ even (k + l)" - by (cases "k \ 0") (simp_all add: ac_simps) - -lemma even_add_abs_iff [simp]: - fixes k l :: int - shows "even (k + \l\) \ even (k + l)" - using even_abs_add_iff [of l k] by (simp add: ac_simps) - instance nat :: semiring_parity proof - show "odd (1 :: nat)" + show "\ 2 dvd (1 :: nat)" by (rule notI, erule dvdE) simp next fix m n :: nat - assume "odd m" - moreover assume "odd n" - ultimately have *: "even (Suc m) \ even (Suc n)" + assume "\ 2 dvd m" + moreover assume "\ 2 dvd n" + ultimately have *: "2 dvd Suc m \ 2 dvd Suc n" by simp - then have "even (Suc m + Suc n)" + then have "2 dvd (Suc m + Suc n)" by (blast intro: dvd_add) also have "Suc m + Suc n = m + n + 2" by simp - finally show "even (m + n)" + finally show "2 dvd (m + n)" using dvd_add_triv_right_iff [of 2 "m + n"] by simp next fix m n :: nat - assume *: "even (m * n)" - show "even m \ even n" + assume *: "2 dvd (m * n)" + show "2 dvd m \ 2 dvd n" proof (rule disjCI) - assume "odd n" - then have "even (Suc n)" by simp + assume "\ 2 dvd n" + then have "2 dvd (Suc n)" by simp then obtain r where "Suc n = 2 * r" .. moreover from * obtain s where "m * n = 2 * s" .. then have "2 * s + m = m * Suc n" by simp ultimately have " 2 * s + m = 2 * (m * r)" by (simp add: algebra_simps) then have "m = 2 * (m * r - s)" by simp - then show "even m" .. + then show "2 dvd m" .. qed next fix n :: nat - assume "odd n" + assume "\ 2 dvd n" then show "\m. n = m + 1" by (cases n) simp_all qed @@ -194,23 +179,38 @@ lemma odd_pos: "odd (n :: nat) \ 0 < n" by (auto elim: oddE) - + +lemma even_diff_iff [simp]: + fixes k l :: int + shows "2 dvd (k - l) \ 2 dvd (k + l)" + using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right) + +lemma even_abs_add_iff [simp]: + fixes k l :: int + shows "2 dvd (\k\ + l) \ 2 dvd (k + l)" + by (cases "k \ 0") (simp_all add: ac_simps) + +lemma even_add_abs_iff [simp]: + fixes k l :: int + shows "2 dvd (k + \l\) \ 2 dvd (k + l)" + using even_abs_add_iff [of l k] by (simp add: ac_simps) + instance int :: ring_parity proof - show "odd (1 :: int)" by (simp add: dvd_int_unfold_dvd_nat) + show "\ 2 dvd (1 :: int)" by (simp add: dvd_int_unfold_dvd_nat) fix k l :: int - assume "odd k" - moreover assume "odd l" - ultimately have "even (nat \k\ + nat \l\)" + assume "\ 2 dvd k" + moreover assume "\ 2 dvd l" + ultimately have "2 dvd (nat \k\ + nat \l\)" by (auto simp add: dvd_int_unfold_dvd_nat intro: odd_even_add) - then have "even (\k\ + \l\)" + then have "2 dvd (\k\ + \l\)" by (simp add: dvd_int_unfold_dvd_nat nat_add_distrib) - then show "even (k + l)" + then show "2 dvd (k + l)" by simp next fix k l :: int - assume "even (k * l)" - then show "even k \ even l" + assume "2 dvd (k * l)" + then show "2 dvd k \ 2 dvd l" by (simp add: dvd_int_unfold_dvd_nat even_multD nat_abs_mult_distrib) next fix k :: int @@ -352,4 +352,3 @@ ] end - diff -r df9b153d866b -r 063698416239 src/HOL/ex/FinFunPred.thy --- a/src/HOL/ex/FinFunPred.thy Mon Jun 01 18:59:20 2015 +0200 +++ b/src/HOL/ex/FinFunPred.thy Mon Jun 01 18:59:20 2015 +0200 @@ -15,7 +15,7 @@ definition le_finfun_def [code del]: "f \ g \ (\x. f $ x \ g $ x)" -definition [code del]: "(f\'a \f 'b) < g \ f \ g \ \ f \ g" +definition [code del]: "(f\'a \f 'b) < g \ f \ g \ \ g \ f" instance ..