tuned proofs and augmented lemmas
authorhaftmann
Thu Dec 24 09:42:49 2015 +0100 (2015-12-24)
changeset 61929b8e242e52c97
parent 61928 8796d5edd29c
child 61930 380cbe15cca5
tuned proofs and augmented lemmas
src/HOL/GCD.thy
     1.1 --- a/src/HOL/GCD.thy	Thu Dec 24 12:50:12 2015 +0100
     1.2 +++ b/src/HOL/GCD.thy	Thu Dec 24 09:42:49 2015 +0100
     1.3 @@ -445,17 +445,6 @@
     1.4    "Gcd (set as) = foldr gcd as 0"
     1.5    by (induct as) simp_all
     1.6  
     1.7 -end  
     1.8 -
     1.9 -class semiring_Lcm = semiring_Gcd +
    1.10 -  assumes Lcm_Gcd: "Lcm A = Gcd {b. \<forall>a\<in>A. a dvd b}"
    1.11 -begin
    1.12 -
    1.13 -lemma dvd_Lcm:
    1.14 -  assumes "a \<in> A"
    1.15 -  shows "a dvd Lcm A"
    1.16 -  using assms by (auto intro: Gcd_greatest simp add: Lcm_Gcd)
    1.17 -
    1.18  lemma Gcd_image_normalize [simp]:
    1.19    "Gcd (normalize ` A) = Gcd A"
    1.20  proof -
    1.21 @@ -473,6 +462,17 @@
    1.22      by (auto intro: associated_eqI)
    1.23  qed
    1.24  
    1.25 +end  
    1.26 +
    1.27 +class semiring_Lcm = semiring_Gcd +
    1.28 +  assumes Lcm_Gcd: "Lcm A = Gcd {b. \<forall>a\<in>A. a dvd b}"
    1.29 +begin
    1.30 +
    1.31 +lemma dvd_Lcm:
    1.32 +  assumes "a \<in> A"
    1.33 +  shows "a dvd Lcm A"
    1.34 +  using assms by (auto intro: Gcd_greatest simp add: Lcm_Gcd)
    1.35 +
    1.36  lemma Lcm_least:
    1.37    assumes "\<And>b. b \<in> A \<Longrightarrow> b dvd a"
    1.38    shows "Lcm A dvd a"
    1.39 @@ -493,11 +493,38 @@
    1.40    with False show ?thesis
    1.41      by simp
    1.42  qed
    1.43 -  
    1.44 +
    1.45 +lemma Gcd_Lcm:
    1.46 +  "Gcd A = Lcm {b. \<forall>a\<in>A. b dvd a}"
    1.47 +  by (rule associated_eqI) (auto intro: Gcd_dvd dvd_Lcm Gcd_greatest Lcm_least)
    1.48 + 
    1.49  lemma Lcm_empty [simp]:
    1.50    "Lcm {} = 1"
    1.51    by (simp add: Lcm_Gcd)
    1.52  
    1.53 +lemma Lcm_insert [simp]:
    1.54 +  "Lcm (insert a A) = lcm a (Lcm A)"
    1.55 +proof (rule sym)
    1.56 +  have "lcm a (Lcm A) dvd Lcm (insert a A)"
    1.57 +    by (auto intro: dvd_Lcm Lcm_least)
    1.58 +  moreover have "Lcm (insert a A) dvd lcm a (Lcm A)"
    1.59 +  proof (rule Lcm_least)
    1.60 +    fix b
    1.61 +    assume "b \<in> insert a A"
    1.62 +    then show "b dvd lcm a (Lcm A)"
    1.63 +    proof
    1.64 +      assume "b = a" then show ?thesis by simp
    1.65 +    next
    1.66 +      assume "b \<in> A"
    1.67 +      then have "b dvd Lcm A" by (rule dvd_Lcm)
    1.68 +      moreover have "Lcm A dvd lcm a (Lcm A)" by simp
    1.69 +      ultimately show ?thesis by (blast intro: dvd_trans)
    1.70 +    qed
    1.71 +  qed
    1.72 +  ultimately show "lcm a (Lcm A) = Lcm (insert a A)"
    1.73 +    by (rule associated_eqI) (simp_all add: lcm_eq_0_iff)
    1.74 +qed
    1.75 +
    1.76  lemma Lcm_1_iff [simp]:
    1.77    "Lcm A = 1 \<longleftrightarrow> (\<forall>a\<in>A. is_unit a)" (is "?P \<longleftrightarrow> ?Q")
    1.78  proof
    1.79 @@ -521,15 +548,6 @@
    1.80      by simp
    1.81  qed
    1.82  
    1.83 -lemma Lcm_UNIV [simp]:
    1.84 -  "Lcm UNIV = 0"
    1.85 -proof -
    1.86 -  have "0 dvd Lcm UNIV"
    1.87 -    by (rule dvd_Lcm) simp
    1.88 -  then show ?thesis
    1.89 -    by simp
    1.90 -qed
    1.91 -
    1.92  lemma Lcm_eq_0_I:
    1.93    assumes "0 \<in> A"
    1.94    shows "Lcm A = 0"
    1.95 @@ -540,34 +558,21 @@
    1.96      by simp
    1.97  qed
    1.98  
    1.99 -lemma Gcd_Lcm:
   1.100 -  "Gcd A = Lcm {b. \<forall>a\<in>A. b dvd a}"
   1.101 -  by (rule associated_eqI) (auto intro: associatedI Gcd_dvd dvd_Lcm Gcd_greatest Lcm_least
   1.102 -    simp add: unit_factor_Gcd unit_factor_Lcm)
   1.103 +lemma Lcm_UNIV [simp]:
   1.104 +  "Lcm UNIV = 0"
   1.105 +  by (rule Lcm_eq_0_I) simp
   1.106  
   1.107 -lemma Lcm_insert [simp]:
   1.108 -  "Lcm (insert a A) = lcm a (Lcm A)"
   1.109 -proof (rule sym)
   1.110 -  have "lcm a (Lcm A) dvd Lcm (insert a A)"
   1.111 -    by (auto intro: dvd_Lcm Lcm_least)
   1.112 -  moreover have "Lcm (insert a A) dvd lcm a (Lcm A)"
   1.113 -  proof (rule Lcm_least)
   1.114 -    fix b
   1.115 -    assume "b \<in> insert a A"
   1.116 -    then show "b dvd lcm a (Lcm A)"
   1.117 -    proof
   1.118 -      assume "b = a" then show ?thesis by simp
   1.119 -    next
   1.120 -      assume "b \<in> A"
   1.121 -      then have "b dvd Lcm A" by (rule dvd_Lcm)
   1.122 -      moreover have "Lcm A dvd lcm a (Lcm A)" by simp
   1.123 -      ultimately show ?thesis by (blast intro: dvd_trans)
   1.124 -    qed
   1.125 -  qed
   1.126 -  ultimately show "lcm a (Lcm A) = Lcm (insert a A)"
   1.127 -    by (rule associated_eqI) (simp_all add: lcm_eq_0_iff)
   1.128 +lemma Lcm_0_iff:
   1.129 +  assumes "finite A"
   1.130 +  shows "Lcm A = 0 \<longleftrightarrow> 0 \<in> A"
   1.131 +proof (cases "A = {}")
   1.132 +  case True then show ?thesis by simp
   1.133 +next
   1.134 +  case False with assms show ?thesis
   1.135 +    by (induct A rule: finite_ne_induct)
   1.136 +      (auto simp add: lcm_eq_0_iff)
   1.137  qed
   1.138 -  
   1.139 +
   1.140  lemma Lcm_set [code_unfold]:
   1.141    "Lcm (set as) = foldr lcm as 1"
   1.142    by (induct as) simp_all
   1.143 @@ -1940,14 +1945,10 @@
   1.144  instantiation nat :: Gcd
   1.145  begin
   1.146  
   1.147 -definition
   1.148 -  "Lcm (M::nat set) = (if finite M then semilattice_neutr_set.F lcm 1 M else 0)"
   1.149 -
   1.150  interpretation semilattice_neutr_set lcm "1::nat" ..
   1.151  
   1.152 -lemma Lcm_nat_infinite:
   1.153 -  "\<not> finite M \<Longrightarrow> Lcm M = (0::nat)"
   1.154 -  by (simp add: Lcm_nat_def)
   1.155 +definition
   1.156 +  "Lcm (M::nat set) = (if finite M then F M else 0)"
   1.157  
   1.158  lemma Lcm_nat_empty:
   1.159    "Lcm {} = (1::nat)"
   1.160 @@ -1955,7 +1956,36 @@
   1.161  
   1.162  lemma Lcm_nat_insert:
   1.163    "Lcm (insert n M) = lcm (n::nat) (Lcm M)"
   1.164 -  by (cases "finite M") (simp_all add: Lcm_nat_def Lcm_nat_infinite del: One_nat_def)
   1.165 +  by (cases "finite M") (auto simp add: Lcm_nat_def simp del: One_nat_def)
   1.166 +
   1.167 +lemma Lcm_nat_infinite:
   1.168 +  "infinite M \<Longrightarrow> Lcm M = (0::nat)"
   1.169 +  by (simp add: Lcm_nat_def)
   1.170 +
   1.171 +lemma dvd_Lcm_nat [simp]:
   1.172 +  fixes M :: "nat set"
   1.173 +  assumes "m \<in> M"
   1.174 +  shows "m dvd Lcm M"
   1.175 +proof -
   1.176 +  from assms have "insert m M = M" by auto
   1.177 +  moreover have "m dvd Lcm (insert m M)"
   1.178 +    by (simp add: Lcm_nat_insert)
   1.179 +  ultimately show ?thesis by simp
   1.180 +qed
   1.181 +
   1.182 +lemma Lcm_dvd_nat [simp]:
   1.183 +  fixes M :: "nat set"
   1.184 +  assumes "\<forall>m\<in>M. m dvd n"
   1.185 +  shows "Lcm M dvd n"
   1.186 +proof (cases "n = 0")
   1.187 +  case True then show ?thesis by simp
   1.188 +next
   1.189 +  case False
   1.190 +  then have "finite {d. d dvd n}" by (rule finite_divisors_nat)
   1.191 +  moreover have "M \<subseteq> {d. d dvd n}" using assms by fast
   1.192 +  ultimately have "finite M" by (rule rev_finite_subset)
   1.193 +  then show ?thesis using assms by (induct M) (simp_all add: Lcm_nat_empty Lcm_nat_insert)
   1.194 +qed
   1.195  
   1.196  definition
   1.197    "Gcd (M::nat set) = Lcm {d. \<forall>m\<in>M. d dvd m}"
   1.198 @@ -1964,27 +1994,21 @@
   1.199  
   1.200  end
   1.201  
   1.202 -lemma dvd_Lcm_nat [simp]:
   1.203 -  fixes M :: "nat set"
   1.204 -  assumes "m \<in> M"
   1.205 -  shows "m dvd Lcm M"
   1.206 -proof (cases "finite M")
   1.207 -  case False then show ?thesis by (simp add: Lcm_nat_infinite)
   1.208 -next
   1.209 -  case True then show ?thesis using assms by (induct M) (auto simp add: Lcm_nat_insert)
   1.210 -qed
   1.211 +instance nat :: semiring_Gcd
   1.212 +proof
   1.213 +  show "Gcd N dvd n" if "n \<in> N" for N and n :: nat
   1.214 +  using that by (induct N rule: infinite_finite_induct)
   1.215 +    (auto simp add: Gcd_nat_def)
   1.216 +  show "n dvd Gcd N" if "\<And>m. m \<in> N \<Longrightarrow> n dvd m" for N and n :: nat
   1.217 +  using that by (induct N rule: infinite_finite_induct)
   1.218 +    (auto simp add: Gcd_nat_def)
   1.219 +qed simp
   1.220  
   1.221 -lemma Lcm_dvd_nat [simp]:
   1.222 -  fixes M :: "nat set"
   1.223 -  assumes "\<forall>m\<in>M. m dvd n"
   1.224 -  shows "Lcm M dvd n"
   1.225 -proof (cases "n = 0")
   1.226 -  assume "n \<noteq> 0"
   1.227 -  hence "finite {d. d dvd n}" by (rule finite_divisors_nat)
   1.228 -  moreover have "M \<subseteq> {d. d dvd n}" using assms by fast
   1.229 -  ultimately have "finite M" by (rule rev_finite_subset)
   1.230 -  then show ?thesis using assms by (induct M) (simp_all add: Lcm_nat_empty Lcm_nat_insert)
   1.231 -qed simp
   1.232 +instance nat :: semiring_Lcm
   1.233 +proof
   1.234 +  show "Lcm N = Gcd {m. \<forall>n\<in>N. n dvd m}" for N :: "nat set"
   1.235 +    by (rule associated_eqI) (auto intro!: Gcd_dvd Gcd_greatest)
   1.236 +qed
   1.237  
   1.238  interpretation gcd_lcm_complete_lattice_nat:
   1.239    complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat"
   1.240 @@ -2002,42 +2026,6 @@
   1.241  declare gcd_lcm_complete_lattice_nat.Inf_image_eq [simp del]
   1.242  declare gcd_lcm_complete_lattice_nat.Sup_image_eq [simp del]
   1.243  
   1.244 -instance nat :: semiring_Gcd
   1.245 -proof
   1.246 -  show "Gcd N dvd n" if "n \<in> N" for N and n :: nat
   1.247 -    using that by (fact gcd_lcm_complete_lattice_nat.Inf_lower)
   1.248 -next
   1.249 -  show "n dvd Gcd N" if "\<And>m. m \<in> N \<Longrightarrow> n dvd m" for N and n :: nat
   1.250 -    using that by (simp only: gcd_lcm_complete_lattice_nat.Inf_greatest)
   1.251 -next
   1.252 -  show "normalize (Gcd N) = Gcd N" for N :: "nat set"
   1.253 -    by simp
   1.254 -qed
   1.255 -
   1.256 -instance nat :: semiring_Lcm
   1.257 -proof
   1.258 -  have uf: "unit_factor (Lcm N) = 1" if "0 < Lcm N" for N :: "nat set"
   1.259 -  proof (cases "finite N")
   1.260 -    case False with that show ?thesis by (simp add: Lcm_nat_infinite)
   1.261 -  next
   1.262 -    case True then show ?thesis
   1.263 -    using that proof (induct N)
   1.264 -      case empty then show ?case by simp
   1.265 -    next
   1.266 -      case (insert n N)
   1.267 -      have "lcm n (Lcm N) \<noteq> 0 \<longleftrightarrow> n \<noteq> 0 \<and> Lcm N \<noteq> 0"
   1.268 -        using lcm_eq_0_iff [of n "Lcm N"] by simp
   1.269 -      then have "lcm n (Lcm N) > 0 \<longleftrightarrow> n > 0 \<and> Lcm N > 0"
   1.270 -        unfolding neq0_conv .
   1.271 -      with insert show ?case
   1.272 -        by (simp add: Lcm_nat_insert unit_factor_lcm)
   1.273 -    qed
   1.274 -  qed
   1.275 -  show "Lcm N = Gcd {m. \<forall>n\<in>N. n dvd m}" for N :: "nat set"
   1.276 -    by (rule associated_eqI) (auto intro!: associatedI Gcd_dvd Gcd_greatest
   1.277 -      simp add: unit_factor_Gcd uf)
   1.278 -qed
   1.279 -
   1.280  lemma Lcm_empty_nat:
   1.281    "Lcm {} = (1::nat)"
   1.282    by (fact Lcm_empty)
   1.283 @@ -2051,8 +2039,10 @@
   1.284    by (rule Lcm_eq_0_I)
   1.285  
   1.286  lemma Lcm0_iff [simp]:
   1.287 -  "finite (M::nat set) \<Longrightarrow> M \<noteq> {} \<Longrightarrow> Lcm M = 0 \<longleftrightarrow> 0 \<in> M"
   1.288 -  by (induct rule: finite_ne_induct) auto
   1.289 +  fixes M :: "nat set"
   1.290 +  assumes "finite M" and "M \<noteq> {}"
   1.291 +  shows "Lcm M = 0 \<longleftrightarrow> 0 \<in> M"
   1.292 +  using assms by (simp add: Lcm_0_iff)
   1.293  
   1.294  text\<open>Alternative characterizations of Gcd:\<close>
   1.295