correct sort constraints for abbreviations in type classes
authorhaftmann
Mon Jun 01 18:59:20 2015 +0200 (2015-06-01)
changeset 60343063698416239
parent 60342 df9b153d866b
child 60344 a40369ea3ba5
correct sort constraints for abbreviations in type classes
* * *
yet another bunch of corrections
src/HOL/Library/Extended.thy
src/HOL/Parity.thy
src/HOL/ex/FinFunPred.thy
     1.1 --- a/src/HOL/Library/Extended.thy	Mon Jun 01 18:59:20 2015 +0200
     1.2 +++ b/src/HOL/Library/Extended.thy	Mon Jun 01 18:59:20 2015 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4  case_of_simps less_eq_extended_case: less_eq_extended.simps
     1.5  
     1.6  definition less_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> bool" where
     1.7 -"((x::'a extended) < y) = (x \<le> y & \<not> x \<ge> y)"
     1.8 +"((x::'a extended) < y) = (x \<le> y & \<not> y \<le> x)"
     1.9  
    1.10  instance
    1.11    by intro_classes (auto simp: less_extended_def less_eq_extended_case split: extended.splits)
     2.1 --- a/src/HOL/Parity.thy	Mon Jun 01 18:59:20 2015 +0200
     2.2 +++ b/src/HOL/Parity.thy	Mon Jun 01 18:59:20 2015 +0200
     2.3 @@ -118,75 +118,60 @@
     2.4  subsection {* Instances for @{typ nat} and @{typ int} *}
     2.5  
     2.6  lemma even_Suc_Suc_iff [simp]:
     2.7 -  "even (Suc (Suc n)) \<longleftrightarrow> even n"
     2.8 +  "2 dvd Suc (Suc n) \<longleftrightarrow> 2 dvd n"
     2.9    using dvd_add_triv_right_iff [of 2 n] by simp
    2.10  
    2.11  lemma even_Suc [simp]:
    2.12 -  "even (Suc n) \<longleftrightarrow> odd n"
    2.13 +  "2 dvd Suc n \<longleftrightarrow> \<not> 2 dvd n"
    2.14    by (induct n) auto
    2.15  
    2.16  lemma even_diff_nat [simp]:
    2.17    fixes m n :: nat
    2.18 -  shows "even (m - n) \<longleftrightarrow> m < n \<or> even (m + n)"
    2.19 +  shows "2 dvd (m - n) \<longleftrightarrow> m < n \<or> 2 dvd (m + n)"
    2.20  proof (cases "n \<le> m")
    2.21    case True
    2.22    then have "m - n + n * 2 = m + n" by (simp add: mult_2_right)
    2.23 -  moreover have "even (m - n) \<longleftrightarrow> even (m - n + n * 2)" by simp
    2.24 -  ultimately have "even (m - n) \<longleftrightarrow> even (m + n)" by (simp only:)
    2.25 +  moreover have "2 dvd (m - n) \<longleftrightarrow> 2 dvd (m - n + n * 2)" by simp
    2.26 +  ultimately have "2 dvd (m - n) \<longleftrightarrow> 2 dvd (m + n)" by (simp only:)
    2.27    then show ?thesis by auto
    2.28  next
    2.29    case False
    2.30    then show ?thesis by simp
    2.31  qed 
    2.32    
    2.33 -lemma even_diff_iff [simp]:
    2.34 -  fixes k l :: int
    2.35 -  shows "even (k - l) \<longleftrightarrow> even (k + l)"
    2.36 -  using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right)
    2.37 -
    2.38 -lemma even_abs_add_iff [simp]:
    2.39 -  fixes k l :: int
    2.40 -  shows "even (\<bar>k\<bar> + l) \<longleftrightarrow> even (k + l)"
    2.41 -  by (cases "k \<ge> 0") (simp_all add: ac_simps)
    2.42 -
    2.43 -lemma even_add_abs_iff [simp]:
    2.44 -  fixes k l :: int
    2.45 -  shows "even (k + \<bar>l\<bar>) \<longleftrightarrow> even (k + l)"
    2.46 -  using even_abs_add_iff [of l k] by (simp add: ac_simps)
    2.47 -
    2.48  instance nat :: semiring_parity
    2.49  proof
    2.50 -  show "odd (1 :: nat)"
    2.51 +  show "\<not> 2 dvd (1 :: nat)"
    2.52      by (rule notI, erule dvdE) simp
    2.53  next
    2.54    fix m n :: nat
    2.55 -  assume "odd m"
    2.56 -  moreover assume "odd n"
    2.57 -  ultimately have *: "even (Suc m) \<and> even (Suc n)"
    2.58 +  assume "\<not> 2 dvd m"
    2.59 +  moreover assume "\<not> 2 dvd n"
    2.60 +  ultimately have *: "2 dvd Suc m \<and> 2 dvd Suc n"
    2.61      by simp
    2.62 -  then have "even (Suc m + Suc n)"
    2.63 +  then have "2 dvd (Suc m + Suc n)"
    2.64      by (blast intro: dvd_add)
    2.65    also have "Suc m + Suc n = m + n + 2"
    2.66      by simp
    2.67 -  finally show "even (m + n)"
    2.68 +  finally show "2 dvd (m + n)"
    2.69      using dvd_add_triv_right_iff [of 2 "m + n"] by simp
    2.70  next
    2.71    fix m n :: nat
    2.72 -  assume *: "even (m * n)"
    2.73 -  show "even m \<or> even n"
    2.74 +  assume *: "2 dvd (m * n)"
    2.75 +  show "2 dvd m \<or> 2 dvd n"
    2.76    proof (rule disjCI)
    2.77 -    assume "odd n"
    2.78 -    then have "even (Suc n)" by simp
    2.79 +    assume "\<not> 2 dvd n"
    2.80 +    then have "2 dvd (Suc n)" by simp
    2.81      then obtain r where "Suc n = 2 * r" ..
    2.82      moreover from * obtain s where "m * n = 2 * s" ..
    2.83      then have "2 * s + m = m * Suc n" by simp
    2.84      ultimately have " 2 * s + m = 2 * (m * r)" by (simp add: algebra_simps)
    2.85      then have "m = 2 * (m * r - s)" by simp
    2.86 -    then show "even m" ..
    2.87 +    then show "2 dvd m" ..
    2.88    qed
    2.89  next
    2.90    fix n :: nat
    2.91 -  assume "odd n"
    2.92 +  assume "\<not> 2 dvd n"
    2.93    then show "\<exists>m. n = m + 1"
    2.94      by (cases n) simp_all
    2.95  qed
    2.96 @@ -194,23 +179,38 @@
    2.97  lemma odd_pos: 
    2.98    "odd (n :: nat) \<Longrightarrow> 0 < n"
    2.99    by (auto elim: oddE)
   2.100 -  
   2.101 +
   2.102 +lemma even_diff_iff [simp]:
   2.103 +  fixes k l :: int
   2.104 +  shows "2 dvd (k - l) \<longleftrightarrow> 2 dvd (k + l)"
   2.105 +  using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right)
   2.106 +
   2.107 +lemma even_abs_add_iff [simp]:
   2.108 +  fixes k l :: int
   2.109 +  shows "2 dvd (\<bar>k\<bar> + l) \<longleftrightarrow> 2 dvd (k + l)"
   2.110 +  by (cases "k \<ge> 0") (simp_all add: ac_simps)
   2.111 +
   2.112 +lemma even_add_abs_iff [simp]:
   2.113 +  fixes k l :: int
   2.114 +  shows "2 dvd (k + \<bar>l\<bar>) \<longleftrightarrow> 2 dvd (k + l)"
   2.115 +  using even_abs_add_iff [of l k] by (simp add: ac_simps)
   2.116 +
   2.117  instance int :: ring_parity
   2.118  proof
   2.119 -  show "odd (1 :: int)" by (simp add: dvd_int_unfold_dvd_nat)
   2.120 +  show "\<not> 2 dvd (1 :: int)" by (simp add: dvd_int_unfold_dvd_nat)
   2.121    fix k l :: int
   2.122 -  assume "odd k"
   2.123 -  moreover assume "odd l"
   2.124 -  ultimately have "even (nat \<bar>k\<bar> + nat \<bar>l\<bar>)" 
   2.125 +  assume "\<not> 2 dvd k"
   2.126 +  moreover assume "\<not> 2 dvd l"
   2.127 +  ultimately have "2 dvd (nat \<bar>k\<bar> + nat \<bar>l\<bar>)" 
   2.128      by (auto simp add: dvd_int_unfold_dvd_nat intro: odd_even_add)
   2.129 -  then have "even (\<bar>k\<bar> + \<bar>l\<bar>)"
   2.130 +  then have "2 dvd (\<bar>k\<bar> + \<bar>l\<bar>)"
   2.131      by (simp add: dvd_int_unfold_dvd_nat nat_add_distrib)
   2.132 -  then show "even (k + l)"
   2.133 +  then show "2 dvd (k + l)"
   2.134      by simp
   2.135  next
   2.136    fix k l :: int
   2.137 -  assume "even (k * l)"
   2.138 -  then show "even k \<or> even l"
   2.139 +  assume "2 dvd (k * l)"
   2.140 +  then show "2 dvd k \<or> 2 dvd l"
   2.141      by (simp add: dvd_int_unfold_dvd_nat even_multD nat_abs_mult_distrib)
   2.142  next
   2.143    fix k :: int
   2.144 @@ -352,4 +352,3 @@
   2.145  ]
   2.146  
   2.147  end
   2.148 -
     3.1 --- a/src/HOL/ex/FinFunPred.thy	Mon Jun 01 18:59:20 2015 +0200
     3.2 +++ b/src/HOL/ex/FinFunPred.thy	Mon Jun 01 18:59:20 2015 +0200
     3.3 @@ -15,7 +15,7 @@
     3.4  
     3.5  definition le_finfun_def [code del]: "f \<le> g \<longleftrightarrow> (\<forall>x. f $ x \<le> g $ x)"
     3.6  
     3.7 -definition [code del]: "(f\<Colon>'a \<Rightarrow>f 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> f \<ge> g"
     3.8 +definition [code del]: "(f\<Colon>'a \<Rightarrow>f 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> g \<le> f"
     3.9  
    3.10  instance ..
    3.11