1.1 --- a/src/HOL/Number_Theory/Binomial.thy Sat Sep 10 22:11:55 2011 +0200
1.2 +++ b/src/HOL/Number_Theory/Binomial.thy Sat Sep 10 23:27:32 2011 +0200
1.3 @@ -20,40 +20,35 @@
1.4 subsection {* Main definitions *}
1.5
1.6 class binomial =
1.7 -
1.8 -fixes
1.9 - binomial :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "choose" 65)
1.10 + fixes binomial :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "choose" 65)
1.11
1.12 (* definitions for the natural numbers *)
1.13
1.14 instantiation nat :: binomial
1.15 -
1.16 begin
1.17
1.18 -fun
1.19 - binomial_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
1.20 +fun binomial_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
1.21 where
1.22 "binomial_nat n k =
1.23 (if k = 0 then 1 else
1.24 if n = 0 then 0 else
1.25 (binomial (n - 1) k) + (binomial (n - 1) (k - 1)))"
1.26
1.27 -instance proof qed
1.28 +instance ..
1.29
1.30 end
1.31
1.32 (* definitions for the integers *)
1.33
1.34 instantiation int :: binomial
1.35 -
1.36 begin
1.37
1.38 -definition
1.39 - binomial_int :: "int => int \<Rightarrow> int"
1.40 -where
1.41 - "binomial_int n k = (if n \<ge> 0 \<and> k \<ge> 0 then int (binomial (nat n) (nat k))
1.42 - else 0)"
1.43 -instance proof qed
1.44 +definition binomial_int :: "int => int \<Rightarrow> int" where
1.45 + "binomial_int n k =
1.46 + (if n \<ge> 0 \<and> k \<ge> 0 then int (binomial (nat n) (nat k))
1.47 + else 0)"
1.48 +
1.49 +instance ..
1.50
1.51 end
1.52
1.53 @@ -97,10 +92,11 @@
1.54 by (induct n rule: induct'_nat, auto)
1.55
1.56 lemma zero_choose_int [rule_format,simp]: "(k::int) > n \<Longrightarrow> n choose k = 0"
1.57 - unfolding binomial_int_def apply (case_tac "n < 0")
1.58 + unfolding binomial_int_def
1.59 + apply (cases "n < 0")
1.60 apply force
1.61 apply (simp del: binomial_nat.simps)
1.62 -done
1.63 + done
1.64
1.65 lemma choose_reduce_nat: "(n::nat) > 0 \<Longrightarrow> 0 < k \<Longrightarrow>
1.66 (n choose k) = ((n - 1) choose k) + ((n - 1) choose (k - 1))"
1.67 @@ -108,10 +104,10 @@
1.68
1.69 lemma choose_reduce_int: "(n::int) > 0 \<Longrightarrow> 0 < k \<Longrightarrow>
1.70 (n choose k) = ((n - 1) choose k) + ((n - 1) choose (k - 1))"
1.71 - unfolding binomial_int_def apply (subst choose_reduce_nat)
1.72 - apply (auto simp del: binomial_nat.simps
1.73 - simp add: nat_diff_distrib)
1.74 -done
1.75 + unfolding binomial_int_def
1.76 + apply (subst choose_reduce_nat)
1.77 + apply (auto simp del: binomial_nat.simps simp add: nat_diff_distrib)
1.78 + done
1.79
1.80 lemma choose_plus_one_nat: "((n::nat) + 1) choose (k + 1) =
1.81 (n choose (k + 1)) + (n choose k)"
1.82 @@ -128,13 +124,13 @@
1.83 declare binomial_nat.simps [simp del]
1.84
1.85 lemma choose_self_nat [simp]: "((n::nat) choose n) = 1"
1.86 - by (induct n rule: induct'_nat, auto simp add: choose_plus_one_nat)
1.87 + by (induct n rule: induct'_nat) (auto simp add: choose_plus_one_nat)
1.88
1.89 lemma choose_self_int [simp]: "n \<ge> 0 \<Longrightarrow> ((n::int) choose n) = 1"
1.90 by (auto simp add: binomial_int_def)
1.91
1.92 lemma choose_one_nat [simp]: "(n::nat) choose 1 = n"
1.93 - by (induct n rule: induct'_nat, auto simp add: choose_reduce_nat)
1.94 + by (induct n rule: induct'_nat) (auto simp add: choose_reduce_nat)
1.95
1.96 lemma choose_one_int [simp]: "n \<ge> 0 \<Longrightarrow> (n::int) choose 1 = n"
1.97 by (auto simp add: binomial_int_def)
1.98 @@ -165,7 +161,7 @@
1.99 apply force
1.100 apply (subst choose_reduce_nat)
1.101 apply auto
1.102 -done
1.103 + done
1.104
1.105 lemma choose_pos_int: "n \<ge> 0 \<Longrightarrow> k >= 0 \<Longrightarrow> k \<le> n \<Longrightarrow>
1.106 ((n::int) choose k) > 0"
1.107 @@ -183,7 +179,7 @@
1.108 apply (drule_tac x = n in spec) back back
1.109 apply (drule_tac x = "k - 1" in spec) back back back
1.110 apply auto
1.111 -done
1.112 + done
1.113
1.114 lemma choose_altdef_aux_nat: "(k::nat) \<le> n \<Longrightarrow>
1.115 fact k * fact (n - k) * (n choose k) = fact n"
1.116 @@ -193,10 +189,9 @@
1.117 fix k :: nat and n
1.118 assume less: "k < n"
1.119 assume ih1: "fact k * fact (n - k) * (n choose k) = fact n"
1.120 - hence one: "fact (k + 1) * fact (n - k) * (n choose k) = (k + 1) * fact n"
1.121 + then have one: "fact (k + 1) * fact (n - k) * (n choose k) = (k + 1) * fact n"
1.122 by (subst fact_plus_one_nat, auto)
1.123 - assume ih2: "fact (k + 1) * fact (n - (k + 1)) * (n choose (k + 1)) =
1.124 - fact n"
1.125 + assume ih2: "fact (k + 1) * fact (n - (k + 1)) * (n choose (k + 1)) = fact n"
1.126 with less have "fact (k + 1) * fact ((n - (k + 1)) + 1) *
1.127 (n choose (k + 1)) = (n - k) * fact n"
1.128 by (subst (2) fact_plus_one_nat, auto)
1.129 @@ -222,7 +217,7 @@
1.130 apply (frule choose_altdef_aux_nat)
1.131 apply (erule subst)
1.132 apply (simp add: mult_ac)
1.133 -done
1.134 + done
1.135
1.136
1.137 lemma choose_altdef_int:
1.138 @@ -238,7 +233,7 @@
1.139 (* why don't blast and auto get this??? *)
1.140 apply (rule exI)
1.141 apply (erule sym)
1.142 -done
1.143 + done
1.144
1.145 lemma choose_dvd_int:
1.146 assumes "(0::int) <= k" and "k <= n"
1.147 @@ -293,7 +288,8 @@
1.148 fixes S :: "'a set"
1.149 shows "finite S \<Longrightarrow> card {T. T \<le> S \<and> card T = k} = card S choose k"
1.150 proof (induct arbitrary: k set: finite)
1.151 - case empty show ?case by (auto simp add: Collect_conv_if)
1.152 + case empty
1.153 + show ?case by (auto simp add: Collect_conv_if)
1.154 next
1.155 case (insert x F)
1.156 note iassms = insert(1,2)
1.157 @@ -303,11 +299,11 @@
1.158 case zero
1.159 from iassms have "{T. T \<le> (insert x F) \<and> card T = 0} = {{}}"
1.160 by (auto simp: finite_subset)
1.161 - thus ?case by auto
1.162 + then show ?case by auto
1.163 next
1.164 case (plus1 k)
1.165 from iassms have fin: "finite (insert x F)" by auto
1.166 - hence "{ T. T \<subseteq> insert x F \<and> card T = k + 1} =
1.167 + then have "{ T. T \<subseteq> insert x F \<and> card T = k + 1} =
1.168 {T. T \<le> F & card T = k + 1} Un
1.169 {T. T \<le> insert x F & x : T & card T = k + 1}"
1.170 by auto
1.171 @@ -326,14 +322,14 @@
1.172 let ?f = "%T. T Un {x}"
1.173 from iassms have "inj_on ?f {T. T <= F & card T = k}"
1.174 unfolding inj_on_def by auto
1.175 - hence "card ({T. T <= F & card T = k}) =
1.176 + then have "card ({T. T <= F & card T = k}) =
1.177 card(?f ` {T. T <= F & card T = k})"
1.178 by (rule card_image [symmetric])
1.179 also have "?f ` {T. T <= F & card T = k} =
1.180 {T. T \<subseteq> insert x F \<and> x : T \<and> card T = k + 1}" (is "?L=?R")
1.181 proof-
1.182 { fix S assume "S \<subseteq> F"
1.183 - hence "card(insert x S) = card S +1"
1.184 + then have "card(insert x S) = card S +1"
1.185 using iassms by (auto simp: finite_subset) }
1.186 moreover
1.187 { fix T assume 1: "T \<subseteq> insert x F" "x : T" "card T = k+1"
1.188 @@ -353,5 +349,4 @@
1.189 qed
1.190 qed
1.191
1.192 -
1.193 end
2.1 --- a/src/HOL/Number_Theory/Cong.thy Sat Sep 10 22:11:55 2011 +0200
2.2 +++ b/src/HOL/Number_Theory/Cong.thy Sat Sep 10 23:27:32 2011 +0200
2.3 @@ -14,7 +14,7 @@
2.4 The original theory "IntPrimes" was by Thomas M. Rasmussen, and
2.5 extended gcd, lcm, primes to the integers. Amine Chaieb provided
2.6 another extension of the notions to the integers, and added a number
2.7 -of results to "Primes" and "GCD".
2.8 +of results to "Primes" and "GCD".
2.9
2.10 The original theory, "IntPrimes", by Thomas M. Rasmussen, defined and
2.11 developed the congruence relations on the integers. The notion was
2.12 @@ -29,34 +29,33 @@
2.13 imports Primes
2.14 begin
2.15
2.16 -subsection {* Turn off One_nat_def *}
2.17 +subsection {* Turn off @{text One_nat_def} *}
2.18
2.19 -lemma induct'_nat [case_names zero plus1, induct type: nat]:
2.20 - "\<lbrakk> P (0::nat); !!n. P n \<Longrightarrow> P (n + 1)\<rbrakk> \<Longrightarrow> P n"
2.21 -by (erule nat_induct) (simp add:One_nat_def)
2.22 +lemma induct'_nat [case_names zero plus1, induct type: nat]:
2.23 + "P (0::nat) \<Longrightarrow> (\<And>n. P n \<Longrightarrow> P (n + 1)) \<Longrightarrow> P n"
2.24 + by (induct n) (simp_all add: One_nat_def)
2.25
2.26 -lemma cases_nat [case_names zero plus1, cases type: nat]:
2.27 - "P (0::nat) \<Longrightarrow> (!!n. P (n + 1)) \<Longrightarrow> P n"
2.28 -by(metis induct'_nat)
2.29 +lemma cases_nat [case_names zero plus1, cases type: nat]:
2.30 + "P (0::nat) \<Longrightarrow> (\<And>n. P (n + 1)) \<Longrightarrow> P n"
2.31 + by (rule induct'_nat)
2.32
2.33 lemma power_plus_one [simp]: "(x::'a::power)^(n + 1) = x * x^n"
2.34 -by (simp add: One_nat_def)
2.35 + by (simp add: One_nat_def)
2.36
2.37 -lemma power_eq_one_eq_nat [simp]:
2.38 - "((x::nat)^m = 1) = (m = 0 | x = 1)"
2.39 -by (induct m, auto)
2.40 +lemma power_eq_one_eq_nat [simp]: "((x::nat)^m = 1) = (m = 0 | x = 1)"
2.41 + by (induct m) auto
2.42
2.43 lemma card_insert_if' [simp]: "finite A \<Longrightarrow>
2.44 - card (insert x A) = (if x \<in> A then (card A) else (card A) + 1)"
2.45 -by (auto simp add: insert_absorb)
2.46 + card (insert x A) = (if x \<in> A then (card A) else (card A) + 1)"
2.47 + by (auto simp add: insert_absorb)
2.48
2.49 lemma nat_1' [simp]: "nat 1 = 1"
2.50 -by simp
2.51 + by simp
2.52
2.53 (* For those annoying moments where Suc reappears, use Suc_eq_plus1 *)
2.54
2.55 declare nat_1 [simp del]
2.56 -declare add_2_eq_Suc [simp del]
2.57 +declare add_2_eq_Suc [simp del]
2.58 declare add_2_eq_Suc' [simp del]
2.59
2.60
2.61 @@ -66,31 +65,23 @@
2.62 subsection {* Main definitions *}
2.63
2.64 class cong =
2.65 -
2.66 -fixes
2.67 - cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ = _] '(mod _'))")
2.68 -
2.69 + fixes cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ = _] '(mod _'))")
2.70 begin
2.71
2.72 -abbreviation
2.73 - notcong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ \<noteq> _] '(mod _'))")
2.74 -where
2.75 - "notcong x y m == (~cong x y m)"
2.76 +abbreviation notcong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ \<noteq> _] '(mod _'))")
2.77 + where "notcong x y m \<equiv> \<not> cong x y m"
2.78
2.79 end
2.80
2.81 (* definitions for the natural numbers *)
2.82
2.83 instantiation nat :: cong
2.84 +begin
2.85
2.86 -begin
2.87 +definition cong_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
2.88 + where "cong_nat x y m = ((x mod m) = (y mod m))"
2.89
2.90 -definition
2.91 - cong_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
2.92 -where
2.93 - "cong_nat x y m = ((x mod m) = (y mod m))"
2.94 -
2.95 -instance proof qed
2.96 +instance ..
2.97
2.98 end
2.99
2.100 @@ -98,15 +89,12 @@
2.101 (* definitions for the integers *)
2.102
2.103 instantiation int :: cong
2.104 +begin
2.105
2.106 -begin
2.107 +definition cong_int :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool"
2.108 + where "cong_int x y m = ((x mod m) = (y mod m))"
2.109
2.110 -definition
2.111 - cong_int :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool"
2.112 -where
2.113 - "cong_int x y m = ((x mod m) = (y mod m))"
2.114 -
2.115 -instance proof qed
2.116 +instance ..
2.117
2.118 end
2.119
2.120 @@ -115,25 +103,25 @@
2.121
2.122
2.123 lemma transfer_nat_int_cong:
2.124 - "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> m >= 0 \<Longrightarrow>
2.125 + "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> m >= 0 \<Longrightarrow>
2.126 ([(nat x) = (nat y)] (mod (nat m))) = ([x = y] (mod m))"
2.127 - unfolding cong_int_def cong_nat_def
2.128 + unfolding cong_int_def cong_nat_def
2.129 apply (auto simp add: nat_mod_distrib [symmetric])
2.130 apply (subst (asm) eq_nat_nat_iff)
2.131 - apply (case_tac "m = 0", force, rule pos_mod_sign, force)+
2.132 + apply (cases "m = 0", force, rule pos_mod_sign, force)+
2.133 apply assumption
2.134 -done
2.135 + done
2.136
2.137 -declare transfer_morphism_nat_int[transfer add return:
2.138 +declare transfer_morphism_nat_int[transfer add return:
2.139 transfer_nat_int_cong]
2.140
2.141 lemma transfer_int_nat_cong:
2.142 "[(int x) = (int y)] (mod (int m)) = [x = y] (mod m)"
2.143 apply (auto simp add: cong_int_def cong_nat_def)
2.144 apply (auto simp add: zmod_int [symmetric])
2.145 -done
2.146 + done
2.147
2.148 -declare transfer_morphism_int_nat[transfer add return:
2.149 +declare transfer_morphism_int_nat[transfer add return:
2.150 transfer_int_nat_cong]
2.151
2.152
2.153 @@ -141,52 +129,52 @@
2.154
2.155 (* was zcong_0, etc. *)
2.156 lemma cong_0_nat [simp, presburger]: "([(a::nat) = b] (mod 0)) = (a = b)"
2.157 - by (unfold cong_nat_def, auto)
2.158 + unfolding cong_nat_def by auto
2.159
2.160 lemma cong_0_int [simp, presburger]: "([(a::int) = b] (mod 0)) = (a = b)"
2.161 - by (unfold cong_int_def, auto)
2.162 + unfolding cong_int_def by auto
2.163
2.164 lemma cong_1_nat [simp, presburger]: "[(a::nat) = b] (mod 1)"
2.165 - by (unfold cong_nat_def, auto)
2.166 + unfolding cong_nat_def by auto
2.167
2.168 lemma cong_Suc_0_nat [simp, presburger]: "[(a::nat) = b] (mod Suc 0)"
2.169 - by (unfold cong_nat_def, auto simp add: One_nat_def)
2.170 + unfolding cong_nat_def by (auto simp add: One_nat_def)
2.171
2.172 lemma cong_1_int [simp, presburger]: "[(a::int) = b] (mod 1)"
2.173 - by (unfold cong_int_def, auto)
2.174 + unfolding cong_int_def by auto
2.175
2.176 lemma cong_refl_nat [simp]: "[(k::nat) = k] (mod m)"
2.177 - by (unfold cong_nat_def, auto)
2.178 + unfolding cong_nat_def by auto
2.179
2.180 lemma cong_refl_int [simp]: "[(k::int) = k] (mod m)"
2.181 - by (unfold cong_int_def, auto)
2.182 + unfolding cong_int_def by auto
2.183
2.184 lemma cong_sym_nat: "[(a::nat) = b] (mod m) \<Longrightarrow> [b = a] (mod m)"
2.185 - by (unfold cong_nat_def, auto)
2.186 + unfolding cong_nat_def by auto
2.187
2.188 lemma cong_sym_int: "[(a::int) = b] (mod m) \<Longrightarrow> [b = a] (mod m)"
2.189 - by (unfold cong_int_def, auto)
2.190 + unfolding cong_int_def by auto
2.191
2.192 lemma cong_sym_eq_nat: "[(a::nat) = b] (mod m) = [b = a] (mod m)"
2.193 - by (unfold cong_nat_def, auto)
2.194 + unfolding cong_nat_def by auto
2.195
2.196 lemma cong_sym_eq_int: "[(a::int) = b] (mod m) = [b = a] (mod m)"
2.197 - by (unfold cong_int_def, auto)
2.198 + unfolding cong_int_def by auto
2.199
2.200 lemma cong_trans_nat [trans]:
2.201 "[(a::nat) = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)"
2.202 - by (unfold cong_nat_def, auto)
2.203 + unfolding cong_nat_def by auto
2.204
2.205 lemma cong_trans_int [trans]:
2.206 "[(a::int) = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)"
2.207 - by (unfold cong_int_def, auto)
2.208 + unfolding cong_int_def by auto
2.209
2.210 lemma cong_add_nat:
2.211 "[(a::nat) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a + c = b + d] (mod m)"
2.212 apply (unfold cong_nat_def)
2.213 apply (subst (1 2) mod_add_eq)
2.214 apply simp
2.215 -done
2.216 + done
2.217
2.218 lemma cong_add_int:
2.219 "[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a + c = b + d] (mod m)"
2.220 @@ -194,21 +182,21 @@
2.221 apply (subst (1 2) mod_add_left_eq)
2.222 apply (subst (1 2) mod_add_right_eq)
2.223 apply simp
2.224 -done
2.225 + done
2.226
2.227 lemma cong_diff_int:
2.228 "[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a - c = b - d] (mod m)"
2.229 apply (unfold cong_int_def)
2.230 apply (subst (1 2) mod_diff_eq)
2.231 apply simp
2.232 -done
2.233 + done
2.234
2.235 lemma cong_diff_aux_int:
2.236 - "(a::int) >= c \<Longrightarrow> b >= d \<Longrightarrow> [(a::int) = b] (mod m) \<Longrightarrow>
2.237 + "(a::int) >= c \<Longrightarrow> b >= d \<Longrightarrow> [(a::int) = b] (mod m) \<Longrightarrow>
2.238 [c = d] (mod m) \<Longrightarrow> [tsub a c = tsub b d] (mod m)"
2.239 apply (subst (1 2) tsub_eq)
2.240 apply (auto intro: cong_diff_int)
2.241 -done;
2.242 + done
2.243
2.244 lemma cong_diff_nat:
2.245 assumes "(a::nat) >= c" and "b >= d" and "[a = b] (mod m)" and
2.246 @@ -221,7 +209,7 @@
2.247 apply (unfold cong_nat_def)
2.248 apply (subst (1 2) mod_mult_eq)
2.249 apply simp
2.250 -done
2.251 + done
2.252
2.253 lemma cong_mult_int:
2.254 "[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)"
2.255 @@ -230,73 +218,69 @@
2.256 apply (subst (1 2) mult_commute)
2.257 apply (subst (1 2) zmod_zmult1_eq)
2.258 apply simp
2.259 -done
2.260 + done
2.261
2.262 lemma cong_exp_nat: "[(x::nat) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
2.263 - apply (induct k)
2.264 - apply (auto simp add: cong_mult_nat)
2.265 + by (induct k) (auto simp add: cong_mult_nat)
2.266 +
2.267 +lemma cong_exp_int: "[(x::int) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
2.268 + by (induct k) (auto simp add: cong_mult_int)
2.269 +
2.270 +lemma cong_setsum_nat [rule_format]:
2.271 + "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
2.272 + [(SUM x:A. f x) = (SUM x:A. g x)] (mod m)"
2.273 + apply (cases "finite A")
2.274 + apply (induct set: finite)
2.275 + apply (auto intro: cong_add_nat)
2.276 done
2.277
2.278 -lemma cong_exp_int: "[(x::int) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
2.279 - apply (induct k)
2.280 - apply (auto simp add: cong_mult_int)
2.281 +lemma cong_setsum_int [rule_format]:
2.282 + "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
2.283 + [(SUM x:A. f x) = (SUM x:A. g x)] (mod m)"
2.284 + apply (cases "finite A")
2.285 + apply (induct set: finite)
2.286 + apply (auto intro: cong_add_int)
2.287 done
2.288
2.289 -lemma cong_setsum_nat [rule_format]:
2.290 - "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
2.291 - [(SUM x:A. f x) = (SUM x:A. g x)] (mod m)"
2.292 - apply (case_tac "finite A")
2.293 - apply (induct set: finite)
2.294 - apply (auto intro: cong_add_nat)
2.295 -done
2.296 -
2.297 -lemma cong_setsum_int [rule_format]:
2.298 - "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
2.299 - [(SUM x:A. f x) = (SUM x:A. g x)] (mod m)"
2.300 - apply (case_tac "finite A")
2.301 - apply (induct set: finite)
2.302 - apply (auto intro: cong_add_int)
2.303 -done
2.304 -
2.305 -lemma cong_setprod_nat [rule_format]:
2.306 - "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
2.307 +lemma cong_setprod_nat [rule_format]:
2.308 + "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
2.309 [(PROD x:A. f x) = (PROD x:A. g x)] (mod m)"
2.310 - apply (case_tac "finite A")
2.311 + apply (cases "finite A")
2.312 apply (induct set: finite)
2.313 apply (auto intro: cong_mult_nat)
2.314 -done
2.315 + done
2.316
2.317 -lemma cong_setprod_int [rule_format]:
2.318 - "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
2.319 +lemma cong_setprod_int [rule_format]:
2.320 + "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
2.321 [(PROD x:A. f x) = (PROD x:A. g x)] (mod m)"
2.322 - apply (case_tac "finite A")
2.323 + apply (cases "finite A")
2.324 apply (induct set: finite)
2.325 apply (auto intro: cong_mult_int)
2.326 -done
2.327 + done
2.328
2.329 lemma cong_scalar_nat: "[(a::nat)= b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)"
2.330 - by (rule cong_mult_nat, simp_all)
2.331 + by (rule cong_mult_nat) simp_all
2.332
2.333 lemma cong_scalar_int: "[(a::int)= b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)"
2.334 - by (rule cong_mult_int, simp_all)
2.335 + by (rule cong_mult_int) simp_all
2.336
2.337 lemma cong_scalar2_nat: "[(a::nat)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)"
2.338 - by (rule cong_mult_nat, simp_all)
2.339 + by (rule cong_mult_nat) simp_all
2.340
2.341 lemma cong_scalar2_int: "[(a::int)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)"
2.342 - by (rule cong_mult_int, simp_all)
2.343 + by (rule cong_mult_int) simp_all
2.344
2.345 lemma cong_mult_self_nat: "[(a::nat) * m = 0] (mod m)"
2.346 - by (unfold cong_nat_def, auto)
2.347 + unfolding cong_nat_def by auto
2.348
2.349 lemma cong_mult_self_int: "[(a::int) * m = 0] (mod m)"
2.350 - by (unfold cong_int_def, auto)
2.351 + unfolding cong_int_def by auto
2.352
2.353 lemma cong_eq_diff_cong_0_int: "[(a::int) = b] (mod m) = [a - b = 0] (mod m)"
2.354 apply (rule iffI)
2.355 apply (erule cong_diff_int [of a b m b b, simplified])
2.356 apply (erule cong_add_int [of "a - b" 0 m b b, simplified])
2.357 -done
2.358 + done
2.359
2.360 lemma cong_eq_diff_cong_0_aux_int: "a >= b \<Longrightarrow>
2.361 [(a::int) = b] (mod m) = [tsub a b = 0] (mod m)"
2.362 @@ -307,29 +291,29 @@
2.363 shows "[a = b] (mod m) = [a - b = 0] (mod m)"
2.364 using assms by (rule cong_eq_diff_cong_0_aux_int [transferred])
2.365
2.366 -lemma cong_diff_cong_0'_nat:
2.367 - "[(x::nat) = y] (mod n) \<longleftrightarrow>
2.368 +lemma cong_diff_cong_0'_nat:
2.369 + "[(x::nat) = y] (mod n) \<longleftrightarrow>
2.370 (if x <= y then [y - x = 0] (mod n) else [x - y = 0] (mod n))"
2.371 - apply (case_tac "y <= x")
2.372 + apply (cases "y <= x")
2.373 apply (frule cong_eq_diff_cong_0_nat [where m = n])
2.374 apply auto [1]
2.375 apply (subgoal_tac "x <= y")
2.376 apply (frule cong_eq_diff_cong_0_nat [where m = n])
2.377 apply (subst cong_sym_eq_nat)
2.378 apply auto
2.379 -done
2.380 + done
2.381
2.382 lemma cong_altdef_nat: "(a::nat) >= b \<Longrightarrow> [a = b] (mod m) = (m dvd (a - b))"
2.383 apply (subst cong_eq_diff_cong_0_nat, assumption)
2.384 apply (unfold cong_nat_def)
2.385 apply (simp add: dvd_eq_mod_eq_0 [symmetric])
2.386 -done
2.387 + done
2.388
2.389 lemma cong_altdef_int: "[(a::int) = b] (mod m) = (m dvd (a - b))"
2.390 apply (subst cong_eq_diff_cong_0_int)
2.391 apply (unfold cong_int_def)
2.392 apply (simp add: dvd_eq_mod_eq_0 [symmetric])
2.393 -done
2.394 + done
2.395
2.396 lemma cong_abs_int: "[(x::int) = y] (mod abs m) = [x = y] (mod m)"
2.397 by (simp add: cong_altdef_int)
2.398 @@ -342,29 +326,29 @@
2.399 (* any way around this? *)
2.400 apply (subgoal_tac "a * a - 1 = (a - 1) * (a - -1)")
2.401 apply (auto simp add: field_simps)
2.402 -done
2.403 + done
2.404
2.405 lemma cong_mult_rcancel_int:
2.406 - "coprime k (m::int) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
2.407 + "coprime k (m::int) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
2.408 apply (subst (1 2) cong_altdef_int)
2.409 apply (subst left_diff_distrib [symmetric])
2.410 apply (rule coprime_dvd_mult_iff_int)
2.411 apply (subst gcd_commute_int, assumption)
2.412 -done
2.413 + done
2.414
2.415 lemma cong_mult_rcancel_nat:
2.416 assumes "coprime k (m::nat)"
2.417 shows "[a * k = b * k] (mod m) = [a = b] (mod m)"
2.418 apply (rule cong_mult_rcancel_int [transferred])
2.419 using assms apply auto
2.420 -done
2.421 + done
2.422
2.423 lemma cong_mult_lcancel_nat:
2.424 - "coprime k (m::nat) \<Longrightarrow> [k * a = k * b ] (mod m) = [a = b] (mod m)"
2.425 + "coprime k (m::nat) \<Longrightarrow> [k * a = k * b ] (mod m) = [a = b] (mod m)"
2.426 by (simp add: mult_commute cong_mult_rcancel_nat)
2.427
2.428 lemma cong_mult_lcancel_int:
2.429 - "coprime k (m::int) \<Longrightarrow> [k * a = k * b] (mod m) = [a = b] (mod m)"
2.430 + "coprime k (m::int) \<Longrightarrow> [k * a = k * b] (mod m) = [a = b] (mod m)"
2.431 by (simp add: mult_commute cong_mult_rcancel_int)
2.432
2.433 (* was zcong_zgcd_zmult_zmod *)
2.434 @@ -395,7 +379,7 @@
2.435 apply auto
2.436 apply (rule_tac x = "a mod m" in exI)
2.437 apply (unfold cong_nat_def, auto)
2.438 -done
2.439 + done
2.440
2.441 lemma cong_less_unique_int:
2.442 "0 < (m::int) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
2.443 @@ -407,12 +391,12 @@
2.444 lemma cong_iff_lin_int: "([(a::int) = b] (mod m)) = (\<exists>k. b = a + m * k)"
2.445 apply (auto simp add: cong_altdef_int dvd_def field_simps)
2.446 apply (rule_tac [!] x = "-k" in exI, auto)
2.447 -done
2.448 + done
2.449
2.450 -lemma cong_iff_lin_nat: "([(a::nat) = b] (mod m)) =
2.451 +lemma cong_iff_lin_nat: "([(a::nat) = b] (mod m)) =
2.452 (\<exists>k1 k2. b + k1 * m = a + k2 * m)"
2.453 apply (rule iffI)
2.454 - apply (case_tac "b <= a")
2.455 + apply (cases "b <= a")
2.456 apply (subst (asm) cong_altdef_nat, assumption)
2.457 apply (unfold dvd_def, auto)
2.458 apply (rule_tac x = k in exI)
2.459 @@ -430,42 +414,40 @@
2.460 apply (erule ssubst)back
2.461 apply (erule subst)
2.462 apply auto
2.463 -done
2.464 + done
2.465
2.466 lemma cong_gcd_eq_int: "[(a::int) = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
2.467 apply (subst (asm) cong_iff_lin_int, auto)
2.468 - apply (subst add_commute)
2.469 + apply (subst add_commute)
2.470 apply (subst (2) gcd_commute_int)
2.471 apply (subst mult_commute)
2.472 apply (subst gcd_add_mult_int)
2.473 apply (rule gcd_commute_int)
2.474 done
2.475
2.476 -lemma cong_gcd_eq_nat:
2.477 +lemma cong_gcd_eq_nat:
2.478 assumes "[(a::nat) = b] (mod m)"
2.479 shows "gcd a m = gcd b m"
2.480 apply (rule cong_gcd_eq_int [transferred])
2.481 using assms apply auto
2.482 done
2.483
2.484 -lemma cong_imp_coprime_nat: "[(a::nat) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow>
2.485 - coprime b m"
2.486 +lemma cong_imp_coprime_nat: "[(a::nat) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
2.487 by (auto simp add: cong_gcd_eq_nat)
2.488
2.489 -lemma cong_imp_coprime_int: "[(a::int) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow>
2.490 - coprime b m"
2.491 +lemma cong_imp_coprime_int: "[(a::int) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
2.492 by (auto simp add: cong_gcd_eq_int)
2.493
2.494 -lemma cong_cong_mod_nat: "[(a::nat) = b] (mod m) =
2.495 - [a mod m = b mod m] (mod m)"
2.496 +lemma cong_cong_mod_nat: "[(a::nat) = b] (mod m) = [a mod m = b mod m] (mod m)"
2.497 by (auto simp add: cong_nat_def)
2.498
2.499 -lemma cong_cong_mod_int: "[(a::int) = b] (mod m) =
2.500 - [a mod m = b mod m] (mod m)"
2.501 +lemma cong_cong_mod_int: "[(a::int) = b] (mod m) = [a mod m = b mod m] (mod m)"
2.502 by (auto simp add: cong_int_def)
2.503
2.504 lemma cong_minus_int [iff]: "[(a::int) = b] (mod -m) = [a = b] (mod m)"
2.505 - by (subst (1 2) cong_altdef_int, auto)
2.506 + apply (subst (1 2) cong_altdef_int)
2.507 + apply auto
2.508 + done
2.509
2.510 lemma cong_zero_nat: "[(a::nat) = b] (mod 0) = (a = b)"
2.511 by auto
2.512 @@ -479,7 +461,7 @@
2.513 apply (unfold dvd_def, auto)
2.514 apply (rule mod_mod_cancel)
2.515 apply auto
2.516 -done
2.517 + done
2.518
2.519 lemma mod_dvd_mod:
2.520 assumes "0 < (m::nat)" and "m dvd b"
2.521 @@ -490,12 +472,12 @@
2.522 done
2.523 *)
2.524
2.525 -lemma cong_add_lcancel_nat:
2.526 - "[(a::nat) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
2.527 +lemma cong_add_lcancel_nat:
2.528 + "[(a::nat) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
2.529 by (simp add: cong_iff_lin_nat)
2.530
2.531 -lemma cong_add_lcancel_int:
2.532 - "[(a::int) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
2.533 +lemma cong_add_lcancel_int:
2.534 + "[(a::int) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
2.535 by (simp add: cong_iff_lin_int)
2.536
2.537 lemma cong_add_rcancel_nat: "[(x::nat) + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
2.538 @@ -504,43 +486,42 @@
2.539 lemma cong_add_rcancel_int: "[(x::int) + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
2.540 by (simp add: cong_iff_lin_int)
2.541
2.542 -lemma cong_add_lcancel_0_nat: "[(a::nat) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
2.543 +lemma cong_add_lcancel_0_nat: "[(a::nat) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
2.544 by (simp add: cong_iff_lin_nat)
2.545
2.546 -lemma cong_add_lcancel_0_int: "[(a::int) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
2.547 +lemma cong_add_lcancel_0_int: "[(a::int) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
2.548 by (simp add: cong_iff_lin_int)
2.549
2.550 -lemma cong_add_rcancel_0_nat: "[x + (a::nat) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
2.551 +lemma cong_add_rcancel_0_nat: "[x + (a::nat) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
2.552 by (simp add: cong_iff_lin_nat)
2.553
2.554 -lemma cong_add_rcancel_0_int: "[x + (a::int) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
2.555 +lemma cong_add_rcancel_0_int: "[x + (a::int) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
2.556 by (simp add: cong_iff_lin_int)
2.557
2.558 -lemma cong_dvd_modulus_nat: "[(x::nat) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow>
2.559 +lemma cong_dvd_modulus_nat: "[(x::nat) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow>
2.560 [x = y] (mod n)"
2.561 apply (auto simp add: cong_iff_lin_nat dvd_def)
2.562 apply (rule_tac x="k1 * k" in exI)
2.563 apply (rule_tac x="k2 * k" in exI)
2.564 apply (simp add: field_simps)
2.565 -done
2.566 + done
2.567
2.568 -lemma cong_dvd_modulus_int: "[(x::int) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow>
2.569 - [x = y] (mod n)"
2.570 +lemma cong_dvd_modulus_int: "[(x::int) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> [x = y] (mod n)"
2.571 by (auto simp add: cong_altdef_int dvd_def)
2.572
2.573 lemma cong_dvd_eq_nat: "[(x::nat) = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y"
2.574 - by (unfold cong_nat_def, auto simp add: dvd_eq_mod_eq_0)
2.575 + unfolding cong_nat_def by (auto simp add: dvd_eq_mod_eq_0)
2.576
2.577 lemma cong_dvd_eq_int: "[(x::int) = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y"
2.578 - by (unfold cong_int_def, auto simp add: dvd_eq_mod_eq_0)
2.579 + unfolding cong_int_def by (auto simp add: dvd_eq_mod_eq_0)
2.580
2.581 -lemma cong_mod_nat: "(n::nat) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)"
2.582 +lemma cong_mod_nat: "(n::nat) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)"
2.583 by (simp add: cong_nat_def)
2.584
2.585 -lemma cong_mod_int: "(n::int) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)"
2.586 +lemma cong_mod_int: "(n::int) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)"
2.587 by (simp add: cong_int_def)
2.588
2.589 -lemma mod_mult_cong_nat: "(a::nat) ~= 0 \<Longrightarrow> b ~= 0
2.590 +lemma mod_mult_cong_nat: "(a::nat) ~= 0 \<Longrightarrow> b ~= 0
2.591 \<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)"
2.592 by (simp add: cong_nat_def mod_mult2_eq mod_add_left_eq)
2.593
2.594 @@ -548,43 +529,43 @@
2.595 apply (simp add: cong_altdef_int)
2.596 apply (subst dvd_minus_iff [symmetric])
2.597 apply (simp add: field_simps)
2.598 -done
2.599 + done
2.600
2.601 lemma cong_modulus_neg_int: "([(a::int) = b] (mod m)) = ([a = b] (mod -m))"
2.602 by (auto simp add: cong_altdef_int)
2.603
2.604 -lemma mod_mult_cong_int: "(a::int) ~= 0 \<Longrightarrow> b ~= 0
2.605 +lemma mod_mult_cong_int: "(a::int) ~= 0 \<Longrightarrow> b ~= 0
2.606 \<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)"
2.607 - apply (case_tac "b > 0")
2.608 + apply (cases "b > 0")
2.609 apply (simp add: cong_int_def mod_mod_cancel mod_add_left_eq)
2.610 apply (subst (1 2) cong_modulus_neg_int)
2.611 apply (unfold cong_int_def)
2.612 apply (subgoal_tac "a * b = (-a * -b)")
2.613 apply (erule ssubst)
2.614 apply (subst zmod_zmult2_eq)
2.615 - apply (auto simp add: mod_add_left_eq)
2.616 -done
2.617 + apply (auto simp add: mod_add_left_eq)
2.618 + done
2.619
2.620 lemma cong_to_1_nat: "([(a::nat) = 1] (mod n)) \<Longrightarrow> (n dvd (a - 1))"
2.621 - apply (case_tac "a = 0")
2.622 + apply (cases "a = 0")
2.623 apply force
2.624 apply (subst (asm) cong_altdef_nat)
2.625 apply auto
2.626 -done
2.627 + done
2.628
2.629 lemma cong_0_1_nat: "[(0::nat) = 1] (mod n) = (n = 1)"
2.630 - by (unfold cong_nat_def, auto)
2.631 + unfolding cong_nat_def by auto
2.632
2.633 lemma cong_0_1_int: "[(0::int) = 1] (mod n) = ((n = 1) | (n = -1))"
2.634 - by (unfold cong_int_def, auto simp add: zmult_eq_1_iff)
2.635 + unfolding cong_int_def by (auto simp add: zmult_eq_1_iff)
2.636
2.637 -lemma cong_to_1'_nat: "[(a::nat) = 1] (mod n) \<longleftrightarrow>
2.638 +lemma cong_to_1'_nat: "[(a::nat) = 1] (mod n) \<longleftrightarrow>
2.639 a = 0 \<and> n = 1 \<or> (\<exists>m. a = 1 + m * n)"
2.640 - apply (case_tac "n = 1")
2.641 + apply (cases "n = 1")
2.642 apply auto [1]
2.643 apply (drule_tac x = "a - 1" in spec)
2.644 apply force
2.645 - apply (case_tac "a = 0")
2.646 + apply (cases "a = 0")
2.647 apply (auto simp add: cong_0_1_nat) [1]
2.648 apply (rule iffI)
2.649 apply (drule cong_to_1_nat)
2.650 @@ -594,7 +575,7 @@
2.651 apply (auto simp add: field_simps) [1]
2.652 apply (subst cong_altdef_nat)
2.653 apply (auto simp add: dvd_def)
2.654 -done
2.655 + done
2.656
2.657 lemma cong_le_nat: "(y::nat) <= x \<Longrightarrow> [x = y] (mod n) \<longleftrightarrow> (\<exists>q. x = q * n + y)"
2.658 apply (subst cong_altdef_nat)
2.659 @@ -602,10 +583,10 @@
2.660 apply (unfold dvd_def, auto simp add: field_simps)
2.661 apply (rule_tac x = k in exI)
2.662 apply auto
2.663 -done
2.664 + done
2.665
2.666 lemma cong_solve_nat: "(a::nat) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)"
2.667 - apply (case_tac "n = 0")
2.668 + apply (cases "n = 0")
2.669 apply force
2.670 apply (frule bezout_nat [of a n], auto)
2.671 apply (rule exI, erule ssubst)
2.672 @@ -617,11 +598,11 @@
2.673 apply simp
2.674 apply (rule cong_refl_nat)
2.675 apply (rule cong_refl_nat)
2.676 -done
2.677 + done
2.678
2.679 lemma cong_solve_int: "(a::int) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)"
2.680 - apply (case_tac "n = 0")
2.681 - apply (case_tac "a \<ge> 0")
2.682 + apply (cases "n = 0")
2.683 + apply (cases "a \<ge> 0")
2.684 apply auto
2.685 apply (rule_tac x = "-1" in exI)
2.686 apply auto
2.687 @@ -637,16 +618,15 @@
2.688 apply simp
2.689 apply (subst mult_commute)
2.690 apply (rule cong_refl_int)
2.691 -done
2.692 -
2.693 -lemma cong_solve_dvd_nat:
2.694 + done
2.695 +
2.696 +lemma cong_solve_dvd_nat:
2.697 assumes a: "(a::nat) \<noteq> 0" and b: "gcd a n dvd d"
2.698 shows "EX x. [a * x = d] (mod n)"
2.699 proof -
2.700 - from cong_solve_nat [OF a] obtain x where
2.701 - "[a * x = gcd a n](mod n)"
2.702 + from cong_solve_nat [OF a] obtain x where "[a * x = gcd a n](mod n)"
2.703 by auto
2.704 - hence "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)"
2.705 + then have "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)"
2.706 by (elim cong_scalar2_nat)
2.707 also from b have "(d div gcd a n) * gcd a n = d"
2.708 by (rule dvd_div_mult_self)
2.709 @@ -656,14 +636,13 @@
2.710 by auto
2.711 qed
2.712
2.713 -lemma cong_solve_dvd_int:
2.714 +lemma cong_solve_dvd_int:
2.715 assumes a: "(a::int) \<noteq> 0" and b: "gcd a n dvd d"
2.716 shows "EX x. [a * x = d] (mod n)"
2.717 proof -
2.718 - from cong_solve_int [OF a] obtain x where
2.719 - "[a * x = gcd a n](mod n)"
2.720 + from cong_solve_int [OF a] obtain x where "[a * x = gcd a n](mod n)"
2.721 by auto
2.722 - hence "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)"
2.723 + then have "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)"
2.724 by (elim cong_scalar2_int)
2.725 also from b have "(d div gcd a n) * gcd a n = d"
2.726 by (rule dvd_div_mult_self)
2.727 @@ -673,56 +652,52 @@
2.728 by auto
2.729 qed
2.730
2.731 -lemma cong_solve_coprime_nat: "coprime (a::nat) n \<Longrightarrow>
2.732 - EX x. [a * x = 1] (mod n)"
2.733 - apply (case_tac "a = 0")
2.734 +lemma cong_solve_coprime_nat: "coprime (a::nat) n \<Longrightarrow> EX x. [a * x = 1] (mod n)"
2.735 + apply (cases "a = 0")
2.736 apply force
2.737 apply (frule cong_solve_nat [of a n])
2.738 apply auto
2.739 -done
2.740 + done
2.741
2.742 -lemma cong_solve_coprime_int: "coprime (a::int) n \<Longrightarrow>
2.743 - EX x. [a * x = 1] (mod n)"
2.744 - apply (case_tac "a = 0")
2.745 +lemma cong_solve_coprime_int: "coprime (a::int) n \<Longrightarrow> EX x. [a * x = 1] (mod n)"
2.746 + apply (cases "a = 0")
2.747 apply auto
2.748 - apply (case_tac "n \<ge> 0")
2.749 + apply (cases "n \<ge> 0")
2.750 apply auto
2.751 apply (subst cong_int_def, auto)
2.752 apply (frule cong_solve_int [of a n])
2.753 apply auto
2.754 -done
2.755 + done
2.756
2.757 -lemma coprime_iff_invertible_nat: "m > (1::nat) \<Longrightarrow> coprime a m =
2.758 - (EX x. [a * x = 1] (mod m))"
2.759 +lemma coprime_iff_invertible_nat: "m > (1::nat) \<Longrightarrow> coprime a m = (EX x. [a * x = 1] (mod m))"
2.760 apply (auto intro: cong_solve_coprime_nat)
2.761 apply (unfold cong_nat_def, auto intro: invertible_coprime_nat)
2.762 -done
2.763 + done
2.764
2.765 -lemma coprime_iff_invertible_int: "m > (1::int) \<Longrightarrow> coprime a m =
2.766 - (EX x. [a * x = 1] (mod m))"
2.767 +lemma coprime_iff_invertible_int: "m > (1::int) \<Longrightarrow> coprime a m = (EX x. [a * x = 1] (mod m))"
2.768 apply (auto intro: cong_solve_coprime_int)
2.769 apply (unfold cong_int_def)
2.770 apply (auto intro: invertible_coprime_int)
2.771 -done
2.772 + done
2.773
2.774 -lemma coprime_iff_invertible'_int: "m > (1::int) \<Longrightarrow> coprime a m =
2.775 +lemma coprime_iff_invertible'_int: "m > (1::int) \<Longrightarrow> coprime a m =
2.776 (EX x. 0 <= x & x < m & [a * x = 1] (mod m))"
2.777 apply (subst coprime_iff_invertible_int)
2.778 apply auto
2.779 apply (auto simp add: cong_int_def)
2.780 apply (rule_tac x = "x mod m" in exI)
2.781 apply (auto simp add: mod_mult_right_eq [symmetric])
2.782 -done
2.783 + done
2.784
2.785
2.786 lemma cong_cong_lcm_nat: "[(x::nat) = y] (mod a) \<Longrightarrow>
2.787 [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
2.788 - apply (case_tac "y \<le> x")
2.789 + apply (cases "y \<le> x")
2.790 apply (auto simp add: cong_altdef_nat lcm_least_nat) [1]
2.791 apply (rule cong_sym_nat)
2.792 apply (subst (asm) (1 2) cong_sym_eq_nat)
2.793 apply (auto simp add: cong_altdef_nat lcm_least_nat)
2.794 -done
2.795 + done
2.796
2.797 lemma cong_cong_lcm_int: "[(x::int) = y] (mod a) \<Longrightarrow>
2.798 [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
2.799 @@ -730,15 +705,17 @@
2.800
2.801 lemma cong_cong_coprime_nat: "coprime a b \<Longrightarrow> [(x::nat) = y] (mod a) \<Longrightarrow>
2.802 [x = y] (mod b) \<Longrightarrow> [x = y] (mod a * b)"
2.803 - apply (frule (1) cong_cong_lcm_nat)back
2.804 + apply (frule (1) cong_cong_lcm_nat)
2.805 + back
2.806 apply (simp add: lcm_nat_def)
2.807 -done
2.808 + done
2.809
2.810 lemma cong_cong_coprime_int: "coprime a b \<Longrightarrow> [(x::int) = y] (mod a) \<Longrightarrow>
2.811 [x = y] (mod b) \<Longrightarrow> [x = y] (mod a * b)"
2.812 - apply (frule (1) cong_cong_lcm_int)back
2.813 + apply (frule (1) cong_cong_lcm_int)
2.814 + back
2.815 apply (simp add: lcm_altdef_int cong_abs_int abs_mult [symmetric])
2.816 -done
2.817 + done
2.818
2.819 lemma cong_cong_setprod_coprime_nat [rule_format]: "finite A \<Longrightarrow>
2.820 (ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
2.821 @@ -750,7 +727,7 @@
2.822 apply (subst gcd_commute_nat)
2.823 apply (rule setprod_coprime_nat)
2.824 apply auto
2.825 -done
2.826 + done
2.827
2.828 lemma cong_cong_setprod_coprime_int [rule_format]: "finite A \<Longrightarrow>
2.829 (ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
2.830 @@ -762,20 +739,18 @@
2.831 apply (subst gcd_commute_int)
2.832 apply (rule setprod_coprime_int)
2.833 apply auto
2.834 -done
2.835 + done
2.836
2.837 -lemma binary_chinese_remainder_aux_nat:
2.838 +lemma binary_chinese_remainder_aux_nat:
2.839 assumes a: "coprime (m1::nat) m2"
2.840 shows "EX b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and>
2.841 [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)"
2.842 proof -
2.843 - from cong_solve_coprime_nat [OF a]
2.844 - obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
2.845 + from cong_solve_coprime_nat [OF a] obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
2.846 by auto
2.847 - from a have b: "coprime m2 m1"
2.848 + from a have b: "coprime m2 m1"
2.849 by (subst gcd_commute_nat)
2.850 - from cong_solve_coprime_nat [OF b]
2.851 - obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
2.852 + from cong_solve_coprime_nat [OF b] obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
2.853 by auto
2.854 have "[m1 * x1 = 0] (mod m1)"
2.855 by (subst mult_commute, rule cong_mult_self_nat)
2.856 @@ -785,18 +760,16 @@
2.857 ultimately show ?thesis by blast
2.858 qed
2.859
2.860 -lemma binary_chinese_remainder_aux_int:
2.861 +lemma binary_chinese_remainder_aux_int:
2.862 assumes a: "coprime (m1::int) m2"
2.863 shows "EX b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and>
2.864 [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)"
2.865 proof -
2.866 - from cong_solve_coprime_int [OF a]
2.867 - obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
2.868 + from cong_solve_coprime_int [OF a] obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
2.869 by auto
2.870 - from a have b: "coprime m2 m1"
2.871 + from a have b: "coprime m2 m1"
2.872 by (subst gcd_commute_int)
2.873 - from cong_solve_coprime_int [OF b]
2.874 - obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
2.875 + from cong_solve_coprime_int [OF b] obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
2.876 by auto
2.877 have "[m1 * x1 = 0] (mod m1)"
2.878 by (subst mult_commute, rule cong_mult_self_int)
2.879 @@ -811,8 +784,8 @@
2.880 shows "EX x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
2.881 proof -
2.882 from binary_chinese_remainder_aux_nat [OF a] obtain b1 b2
2.883 - where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and
2.884 - "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)"
2.885 + where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and
2.886 + "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)"
2.887 by blast
2.888 let ?x = "u1 * b1 + u2 * b2"
2.889 have "[?x = u1 * 1 + u2 * 0] (mod m1)"
2.890 @@ -822,7 +795,7 @@
2.891 apply (rule cong_scalar2_nat)
2.892 apply (rule `[b2 = 0] (mod m1)`)
2.893 done
2.894 - hence "[?x = u1] (mod m1)" by simp
2.895 + then have "[?x = u1] (mod m1)" by simp
2.896 have "[?x = u1 * 0 + u2 * 1] (mod m2)"
2.897 apply (rule cong_add_nat)
2.898 apply (rule cong_scalar2_nat)
2.899 @@ -830,7 +803,7 @@
2.900 apply (rule cong_scalar2_nat)
2.901 apply (rule `[b2 = 1] (mod m2)`)
2.902 done
2.903 - hence "[?x = u2] (mod m2)" by simp
2.904 + then have "[?x = u2] (mod m2)" by simp
2.905 with `[?x = u1] (mod m1)` show ?thesis by blast
2.906 qed
2.907
2.908 @@ -850,7 +823,7 @@
2.909 apply (rule cong_scalar2_int)
2.910 apply (rule `[b2 = 0] (mod m1)`)
2.911 done
2.912 - hence "[?x = u1] (mod m1)" by simp
2.913 + then have "[?x = u1] (mod m1)" by simp
2.914 have "[?x = u1 * 0 + u2 * 1] (mod m2)"
2.915 apply (rule cong_add_int)
2.916 apply (rule cong_scalar2_int)
2.917 @@ -858,42 +831,42 @@
2.918 apply (rule cong_scalar2_int)
2.919 apply (rule `[b2 = 1] (mod m2)`)
2.920 done
2.921 - hence "[?x = u2] (mod m2)" by simp
2.922 + then have "[?x = u2] (mod m2)" by simp
2.923 with `[?x = u1] (mod m1)` show ?thesis by blast
2.924 qed
2.925
2.926 -lemma cong_modulus_mult_nat: "[(x::nat) = y] (mod m * n) \<Longrightarrow>
2.927 +lemma cong_modulus_mult_nat: "[(x::nat) = y] (mod m * n) \<Longrightarrow>
2.928 [x = y] (mod m)"
2.929 - apply (case_tac "y \<le> x")
2.930 + apply (cases "y \<le> x")
2.931 apply (simp add: cong_altdef_nat)
2.932 apply (erule dvd_mult_left)
2.933 apply (rule cong_sym_nat)
2.934 apply (subst (asm) cong_sym_eq_nat)
2.935 - apply (simp add: cong_altdef_nat)
2.936 + apply (simp add: cong_altdef_nat)
2.937 apply (erule dvd_mult_left)
2.938 -done
2.939 + done
2.940
2.941 -lemma cong_modulus_mult_int: "[(x::int) = y] (mod m * n) \<Longrightarrow>
2.942 +lemma cong_modulus_mult_int: "[(x::int) = y] (mod m * n) \<Longrightarrow>
2.943 [x = y] (mod m)"
2.944 - apply (simp add: cong_altdef_int)
2.945 + apply (simp add: cong_altdef_int)
2.946 apply (erule dvd_mult_left)
2.947 -done
2.948 + done
2.949
2.950 -lemma cong_less_modulus_unique_nat:
2.951 +lemma cong_less_modulus_unique_nat:
2.952 "[(x::nat) = y] (mod m) \<Longrightarrow> x < m \<Longrightarrow> y < m \<Longrightarrow> x = y"
2.953 by (simp add: cong_nat_def)
2.954
2.955 lemma binary_chinese_remainder_unique_nat:
2.956 - assumes a: "coprime (m1::nat) m2" and
2.957 - nz: "m1 \<noteq> 0" "m2 \<noteq> 0"
2.958 + assumes a: "coprime (m1::nat) m2"
2.959 + and nz: "m1 \<noteq> 0" "m2 \<noteq> 0"
2.960 shows "EX! x. x < m1 * m2 \<and> [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
2.961 proof -
2.962 - from binary_chinese_remainder_nat [OF a] obtain y where
2.963 + from binary_chinese_remainder_nat [OF a] obtain y where
2.964 "[y = u1] (mod m1)" and "[y = u2] (mod m2)"
2.965 by blast
2.966 let ?x = "y mod (m1 * m2)"
2.967 from nz have less: "?x < m1 * m2"
2.968 - by auto
2.969 + by auto
2.970 have one: "[?x = u1] (mod m1)"
2.971 apply (rule cong_trans_nat)
2.972 prefer 2
2.973 @@ -911,9 +884,8 @@
2.974 apply (rule cong_mod_nat)
2.975 using nz apply auto
2.976 done
2.977 - have "ALL z. z < m1 * m2 \<and> [z = u1] (mod m1) \<and> [z = u2] (mod m2) \<longrightarrow>
2.978 - z = ?x"
2.979 - proof (clarify)
2.980 + have "ALL z. z < m1 * m2 \<and> [z = u1] (mod m1) \<and> [z = u2] (mod m2) \<longrightarrow> z = ?x"
2.981 + proof clarify
2.982 fix z
2.983 assume "z < m1 * m2"
2.984 assume "[z = u1] (mod m1)" and "[z = u2] (mod m2)"
2.985 @@ -935,46 +907,43 @@
2.986 apply (intro cong_less_modulus_unique_nat)
2.987 apply (auto, erule cong_sym_nat)
2.988 done
2.989 - qed
2.990 - with less one two show ?thesis
2.991 - by auto
2.992 + qed
2.993 + with less one two show ?thesis by auto
2.994 qed
2.995
2.996 lemma chinese_remainder_aux_nat:
2.997 - fixes A :: "'a set" and
2.998 - m :: "'a \<Rightarrow> nat"
2.999 - assumes fin: "finite A" and
2.1000 - cop: "ALL i : A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
2.1001 - shows "EX b. (ALL i : A.
2.1002 - [b i = 1] (mod m i) \<and> [b i = 0] (mod (PROD j : A - {i}. m j)))"
2.1003 + fixes A :: "'a set"
2.1004 + and m :: "'a \<Rightarrow> nat"
2.1005 + assumes fin: "finite A"
2.1006 + and cop: "ALL i : A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
2.1007 + shows "EX b. (ALL i : A. [b i = 1] (mod m i) \<and> [b i = 0] (mod (PROD j : A - {i}. m j)))"
2.1008 proof (rule finite_set_choice, rule fin, rule ballI)
2.1009 fix i
2.1010 assume "i : A"
2.1011 with cop have "coprime (PROD j : A - {i}. m j) (m i)"
2.1012 by (intro setprod_coprime_nat, auto)
2.1013 - hence "EX x. [(PROD j : A - {i}. m j) * x = 1] (mod m i)"
2.1014 + then have "EX x. [(PROD j : A - {i}. m j) * x = 1] (mod m i)"
2.1015 by (elim cong_solve_coprime_nat)
2.1016 then obtain x where "[(PROD j : A - {i}. m j) * x = 1] (mod m i)"
2.1017 by auto
2.1018 - moreover have "[(PROD j : A - {i}. m j) * x = 0]
2.1019 + moreover have "[(PROD j : A - {i}. m j) * x = 0]
2.1020 (mod (PROD j : A - {i}. m j))"
2.1021 by (subst mult_commute, rule cong_mult_self_nat)
2.1022 - ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0]
2.1023 + ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0]
2.1024 (mod setprod m (A - {i}))"
2.1025 by blast
2.1026 qed
2.1027
2.1028 lemma chinese_remainder_nat:
2.1029 - fixes A :: "'a set" and
2.1030 - m :: "'a \<Rightarrow> nat" and
2.1031 - u :: "'a \<Rightarrow> nat"
2.1032 - assumes
2.1033 - fin: "finite A" and
2.1034 - cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
2.1035 + fixes A :: "'a set"
2.1036 + and m :: "'a \<Rightarrow> nat"
2.1037 + and u :: "'a \<Rightarrow> nat"
2.1038 + assumes fin: "finite A"
2.1039 + and cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
2.1040 shows "EX x. (ALL i:A. [x = u i] (mod m i))"
2.1041 proof -
2.1042 from chinese_remainder_aux_nat [OF fin cop] obtain b where
2.1043 - bprop: "ALL i:A. [b i = 1] (mod m i) \<and>
2.1044 + bprop: "ALL i:A. [b i = 1] (mod m i) \<and>
2.1045 [b i = 0] (mod (PROD j : A - {i}. m j))"
2.1046 by blast
2.1047 let ?x = "SUM i:A. (u i) * (b i)"
2.1048 @@ -982,12 +951,12 @@
2.1049 proof (rule exI, clarify)
2.1050 fix i
2.1051 assume a: "i : A"
2.1052 - show "[?x = u i] (mod m i)"
2.1053 + show "[?x = u i] (mod m i)"
2.1054 proof -
2.1055 - from fin a have "?x = (SUM j:{i}. u j * b j) +
2.1056 + from fin a have "?x = (SUM j:{i}. u j * b j) +
2.1057 (SUM j:A-{i}. u j * b j)"
2.1058 by (subst setsum_Un_disjoint [symmetric], auto intro: setsum_cong)
2.1059 - hence "[?x = u i * b i + (SUM j:A-{i}. u j * b j)] (mod m i)"
2.1060 + then have "[?x = u i * b i + (SUM j:A-{i}. u j * b j)] (mod m i)"
2.1061 by auto
2.1062 also have "[u i * b i + (SUM j:A-{i}. u j * b j) =
2.1063 u i * 1 + (SUM j:A-{i}. u j * 0)] (mod m i)"
2.1064 @@ -1010,35 +979,34 @@
2.1065 qed
2.1066 qed
2.1067
2.1068 -lemma coprime_cong_prod_nat [rule_format]: "finite A \<Longrightarrow>
2.1069 +lemma coprime_cong_prod_nat [rule_format]: "finite A \<Longrightarrow>
2.1070 (ALL i: A. (ALL j: A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
2.1071 (ALL i: A. [(x::nat) = y] (mod m i)) \<longrightarrow>
2.1072 - [x = y] (mod (PROD i:A. m i))"
2.1073 + [x = y] (mod (PROD i:A. m i))"
2.1074 apply (induct set: finite)
2.1075 apply auto
2.1076 apply (erule (1) coprime_cong_mult_nat)
2.1077 apply (subst gcd_commute_nat)
2.1078 apply (rule setprod_coprime_nat)
2.1079 apply auto
2.1080 -done
2.1081 + done
2.1082
2.1083 lemma chinese_remainder_unique_nat:
2.1084 - fixes A :: "'a set" and
2.1085 - m :: "'a \<Rightarrow> nat" and
2.1086 - u :: "'a \<Rightarrow> nat"
2.1087 - assumes
2.1088 - fin: "finite A" and
2.1089 - nz: "ALL i:A. m i \<noteq> 0" and
2.1090 - cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
2.1091 + fixes A :: "'a set"
2.1092 + and m :: "'a \<Rightarrow> nat"
2.1093 + and u :: "'a \<Rightarrow> nat"
2.1094 + assumes fin: "finite A"
2.1095 + and nz: "ALL i:A. m i \<noteq> 0"
2.1096 + and cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
2.1097 shows "EX! x. x < (PROD i:A. m i) \<and> (ALL i:A. [x = u i] (mod m i))"
2.1098 proof -
2.1099 - from chinese_remainder_nat [OF fin cop] obtain y where
2.1100 - one: "(ALL i:A. [y = u i] (mod m i))"
2.1101 + from chinese_remainder_nat [OF fin cop]
2.1102 + obtain y where one: "(ALL i:A. [y = u i] (mod m i))"
2.1103 by blast
2.1104 let ?x = "y mod (PROD i:A. m i)"
2.1105 from fin nz have prodnz: "(PROD i:A. m i) \<noteq> 0"
2.1106 by auto
2.1107 - hence less: "?x < (PROD i:A. m i)"
2.1108 + then have less: "?x < (PROD i:A. m i)"
2.1109 by auto
2.1110 have cong: "ALL i:A. [?x = u i] (mod m i)"
2.1111 apply auto
2.1112 @@ -1052,28 +1020,29 @@
2.1113 apply (rule fin)
2.1114 apply assumption
2.1115 done
2.1116 - have unique: "ALL z. z < (PROD i:A. m i) \<and>
2.1117 + have unique: "ALL z. z < (PROD i:A. m i) \<and>
2.1118 (ALL i:A. [z = u i] (mod m i)) \<longrightarrow> z = ?x"
2.1119 proof (clarify)
2.1120 fix z
2.1121 assume zless: "z < (PROD i:A. m i)"
2.1122 assume zcong: "(ALL i:A. [z = u i] (mod m i))"
2.1123 have "ALL i:A. [?x = z] (mod m i)"
2.1124 - apply clarify
2.1125 + apply clarify
2.1126 apply (rule cong_trans_nat)
2.1127 using cong apply (erule bspec)
2.1128 apply (rule cong_sym_nat)
2.1129 using zcong apply auto
2.1130 done
2.1131 with fin cop have "[?x = z] (mod (PROD i:A. m i))"
2.1132 - by (intro coprime_cong_prod_nat, auto)
2.1133 + apply (intro coprime_cong_prod_nat)
2.1134 + apply auto
2.1135 + done
2.1136 with zless less show "z = ?x"
2.1137 apply (intro cong_less_modulus_unique_nat)
2.1138 apply (auto, erule cong_sym_nat)
2.1139 done
2.1140 - qed
2.1141 - from less cong unique show ?thesis
2.1142 - by blast
2.1143 + qed
2.1144 + from less cong unique show ?thesis by blast
2.1145 qed
2.1146
2.1147 end
3.1 --- a/src/HOL/Number_Theory/Fib.thy Sat Sep 10 22:11:55 2011 +0200
3.2 +++ b/src/HOL/Number_Theory/Fib.thy Sat Sep 10 23:27:32 2011 +0200
3.3 @@ -18,48 +18,40 @@
3.4 subsection {* Main definitions *}
3.5
3.6 class fib =
3.7 -
3.8 -fixes
3.9 - fib :: "'a \<Rightarrow> 'a"
3.10 + fixes fib :: "'a \<Rightarrow> 'a"
3.11
3.12
3.13 (* definition for the natural numbers *)
3.14
3.15 instantiation nat :: fib
3.16 +begin
3.17
3.18 -begin
3.19 -
3.20 -fun
3.21 - fib_nat :: "nat \<Rightarrow> nat"
3.22 +fun fib_nat :: "nat \<Rightarrow> nat"
3.23 where
3.24 "fib_nat n =
3.25 (if n = 0 then 0 else
3.26 (if n = 1 then 1 else
3.27 fib (n - 1) + fib (n - 2)))"
3.28
3.29 -instance proof qed
3.30 +instance ..
3.31
3.32 end
3.33
3.34 (* definition for the integers *)
3.35
3.36 instantiation int :: fib
3.37 +begin
3.38
3.39 -begin
3.40 +definition fib_int :: "int \<Rightarrow> int"
3.41 + where "fib_int n = (if n >= 0 then int (fib (nat n)) else 0)"
3.42
3.43 -definition
3.44 - fib_int :: "int \<Rightarrow> int"
3.45 -where
3.46 - "fib_int n = (if n >= 0 then int (fib (nat n)) else 0)"
3.47 -
3.48 -instance proof qed
3.49 +instance ..
3.50
3.51 end
3.52
3.53
3.54 subsection {* Set up Transfer *}
3.55
3.56 -
3.57 lemma transfer_nat_int_fib:
3.58 "(x::int) >= 0 \<Longrightarrow> fib (nat x) = nat (fib x)"
3.59 unfolding fib_int_def by auto
3.60 @@ -68,18 +60,16 @@
3.61 "n >= (0::int) \<Longrightarrow> fib n >= 0"
3.62 by (auto simp add: fib_int_def)
3.63
3.64 -declare transfer_morphism_nat_int[transfer add return:
3.65 +declare transfer_morphism_nat_int[transfer add return:
3.66 transfer_nat_int_fib transfer_nat_int_fib_closure]
3.67
3.68 -lemma transfer_int_nat_fib:
3.69 - "fib (int n) = int (fib n)"
3.70 +lemma transfer_int_nat_fib: "fib (int n) = int (fib n)"
3.71 unfolding fib_int_def by auto
3.72
3.73 -lemma transfer_int_nat_fib_closure:
3.74 - "is_nat n \<Longrightarrow> fib n >= 0"
3.75 +lemma transfer_int_nat_fib_closure: "is_nat n \<Longrightarrow> fib n >= 0"
3.76 unfolding fib_int_def by auto
3.77
3.78 -declare transfer_morphism_int_nat[transfer add return:
3.79 +declare transfer_morphism_int_nat[transfer add return:
3.80 transfer_int_nat_fib transfer_int_nat_fib_closure]
3.81
3.82
3.83 @@ -123,7 +113,7 @@
3.84 (* the need for One_nat_def is due to the natdiff_cancel_numerals
3.85 procedure *)
3.86
3.87 -lemma fib_induct_nat: "P (0::nat) \<Longrightarrow> P (1::nat) \<Longrightarrow>
3.88 +lemma fib_induct_nat: "P (0::nat) \<Longrightarrow> P (1::nat) \<Longrightarrow>
3.89 (!!n. P n \<Longrightarrow> P (n + 1) \<Longrightarrow> P (n + 2)) \<Longrightarrow> P n"
3.90 apply (atomize, induct n rule: nat_less_induct)
3.91 apply auto
3.92 @@ -137,7 +127,7 @@
3.93 apply (auto simp add: One_nat_def) (* again, natdiff_cancel *)
3.94 done
3.95
3.96 -lemma fib_add_nat: "fib ((n::nat) + k + 1) = fib (k + 1) * fib (n + 1) +
3.97 +lemma fib_add_nat: "fib ((n::nat) + k + 1) = fib (k + 1) * fib (n + 1) +
3.98 fib k * fib n"
3.99 apply (induct n rule: fib_induct_nat)
3.100 apply auto
3.101 @@ -148,26 +138,24 @@
3.102 (* hmmm. Why doesn't "n + (1 + (1 + k))" simplify to "n + k + 2"? *)
3.103 apply (subgoal_tac "n + (k + 2) = n + (1 + (1 + k))")
3.104 apply (erule ssubst) back back
3.105 - apply (erule ssubst) back
3.106 + apply (erule ssubst) back
3.107 apply auto
3.108 done
3.109
3.110 -lemma fib_add'_nat: "fib (n + Suc k) = fib (Suc k) * fib (Suc n) +
3.111 - fib k * fib n"
3.112 +lemma fib_add'_nat: "fib (n + Suc k) =
3.113 + fib (Suc k) * fib (Suc n) + fib k * fib n"
3.114 using fib_add_nat by (auto simp add: One_nat_def)
3.115
3.116
3.117 (* transfer from nats to ints *)
3.118 -lemma fib_add_int [rule_format]: "(n::int) >= 0 \<Longrightarrow> k >= 0 \<Longrightarrow>
3.119 - fib (n + k + 1) = fib (k + 1) * fib (n + 1) +
3.120 - fib k * fib n "
3.121 -
3.122 +lemma fib_add_int: "(n::int) >= 0 \<Longrightarrow> k >= 0 \<Longrightarrow>
3.123 + fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n "
3.124 by (rule fib_add_nat [transferred])
3.125
3.126 lemma fib_neq_0_nat: "(n::nat) > 0 \<Longrightarrow> fib n ~= 0"
3.127 apply (induct n rule: fib_induct_nat)
3.128 apply (auto simp add: fib_plus_2_nat)
3.129 -done
3.130 + done
3.131
3.132 lemma fib_gr_0_nat: "(n::nat) > 0 \<Longrightarrow> fib n > 0"
3.133 by (frule fib_neq_0_nat, simp)
3.134 @@ -180,21 +168,20 @@
3.135 much easier using integers, not natural numbers!
3.136 *}
3.137
3.138 -lemma fib_Cassini_aux_int: "fib (int n + 2) * fib (int n) -
3.139 +lemma fib_Cassini_aux_int: "fib (int n + 2) * fib (int n) -
3.140 (fib (int n + 1))^2 = (-1)^(n + 1)"
3.141 apply (induct n)
3.142 - apply (auto simp add: field_simps power2_eq_square fib_reduce_int
3.143 - power_add)
3.144 -done
3.145 + apply (auto simp add: field_simps power2_eq_square fib_reduce_int power_add)
3.146 + done
3.147
3.148 -lemma fib_Cassini_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n -
3.149 +lemma fib_Cassini_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n -
3.150 (fib (n + 1))^2 = (-1)^(nat n + 1)"
3.151 by (insert fib_Cassini_aux_int [of "nat n"], auto)
3.152
3.153 (*
3.154 -lemma fib_Cassini'_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n =
3.155 +lemma fib_Cassini'_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n =
3.156 (fib (n + 1))^2 + (-1)^(nat n + 1)"
3.157 - by (frule fib_Cassini_int, simp)
3.158 + by (frule fib_Cassini_int, simp)
3.159 *)
3.160
3.161 lemma fib_Cassini'_int: "n >= 0 \<Longrightarrow> fib ((n::int) + 2) * fib n =
3.162 @@ -204,12 +191,11 @@
3.163 apply (subst tsub_eq)
3.164 apply (insert fib_gr_0_int [of "n + 1"], force)
3.165 apply auto
3.166 -done
3.167 + done
3.168
3.169 lemma fib_Cassini_nat: "fib ((n::nat) + 2) * fib n =
3.170 - (if even n then (fib (n + 1))^2 - 1
3.171 - else (fib (n + 1))^2 + 1)"
3.172 -
3.173 + (if even n then (fib (n + 1))^2 - 1
3.174 + else (fib (n + 1))^2 + 1)"
3.175 by (rule fib_Cassini'_int [transferred, of n], auto)
3.176
3.177
3.178 @@ -222,13 +208,12 @@
3.179 apply (auto simp add: Suc_eq_plus1) (* again, natdiff_cancel *)
3.180 apply (subst add_commute, auto)
3.181 apply (subst gcd_commute_nat, auto simp add: field_simps)
3.182 -done
3.183 + done
3.184
3.185 lemma coprime_fib_Suc_nat: "coprime (fib n) (fib (Suc n))"
3.186 using coprime_fib_plus_1_nat by (simp add: One_nat_def)
3.187
3.188 -lemma coprime_fib_plus_1_int:
3.189 - "n >= 0 \<Longrightarrow> coprime (fib (n::int)) (fib (n + 1))"
3.190 +lemma coprime_fib_plus_1_int: "n >= 0 \<Longrightarrow> coprime (fib (n::int)) (fib (n + 1))"
3.191 by (erule coprime_fib_plus_1_nat [transferred])
3.192
3.193 lemma gcd_fib_add_nat: "gcd (fib (m::nat)) (fib (n + m)) = gcd (fib m) (fib n)"
3.194 @@ -243,51 +228,53 @@
3.195 apply (subst gcd_commute_nat)
3.196 apply (rule gcd_mult_cancel_nat)
3.197 apply (rule coprime_fib_plus_1_nat)
3.198 -done
3.199 + done
3.200
3.201 -lemma gcd_fib_add_int [rule_format]: "m >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow>
3.202 +lemma gcd_fib_add_int [rule_format]: "m >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow>
3.203 gcd (fib (m::int)) (fib (n + m)) = gcd (fib m) (fib n)"
3.204 by (erule gcd_fib_add_nat [transferred])
3.205
3.206 -lemma gcd_fib_diff_nat: "(m::nat) \<le> n \<Longrightarrow>
3.207 +lemma gcd_fib_diff_nat: "(m::nat) \<le> n \<Longrightarrow>
3.208 gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
3.209 by (simp add: gcd_fib_add_nat [symmetric, of _ "n-m"])
3.210
3.211 -lemma gcd_fib_diff_int: "0 <= (m::int) \<Longrightarrow> m \<le> n \<Longrightarrow>
3.212 +lemma gcd_fib_diff_int: "0 <= (m::int) \<Longrightarrow> m \<le> n \<Longrightarrow>
3.213 gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
3.214 by (simp add: gcd_fib_add_int [symmetric, of _ "n-m"])
3.215
3.216 -lemma gcd_fib_mod_nat: "0 < (m::nat) \<Longrightarrow>
3.217 +lemma gcd_fib_mod_nat: "0 < (m::nat) \<Longrightarrow>
3.218 gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
3.219 proof (induct n rule: less_induct)
3.220 case (less n)
3.221 from less.prems have pos_m: "0 < m" .
3.222 show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
3.223 proof (cases "m < n")
3.224 - case True note m_n = True
3.225 - then have m_n': "m \<le> n" by auto
3.226 + case True
3.227 + then have "m \<le> n" by auto
3.228 with pos_m have pos_n: "0 < n" by auto
3.229 - with pos_m m_n have diff: "n - m < n" by auto
3.230 + with pos_m `m < n` have diff: "n - m < n" by auto
3.231 have "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib ((n - m) mod m))"
3.232 - by (simp add: mod_if [of n]) (insert m_n, auto)
3.233 - also have "\<dots> = gcd (fib m) (fib (n - m))"
3.234 + by (simp add: mod_if [of n]) (insert `m < n`, auto)
3.235 + also have "\<dots> = gcd (fib m) (fib (n - m))"
3.236 by (simp add: less.hyps diff pos_m)
3.237 - also have "\<dots> = gcd (fib m) (fib n)" by (simp add: gcd_fib_diff_nat m_n')
3.238 + also have "\<dots> = gcd (fib m) (fib n)"
3.239 + by (simp add: gcd_fib_diff_nat `m \<le> n`)
3.240 finally show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" .
3.241 next
3.242 - case False then show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
3.243 - by (cases "m = n") auto
3.244 + case False
3.245 + then show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
3.246 + by (cases "m = n") auto
3.247 qed
3.248 qed
3.249
3.250 -lemma gcd_fib_mod_int:
3.251 +lemma gcd_fib_mod_int:
3.252 assumes "0 < (m::int)" and "0 <= n"
3.253 shows "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
3.254 apply (rule gcd_fib_mod_nat [transferred])
3.255 using assms apply auto
3.256 done
3.257
3.258 -lemma fib_gcd_nat: "fib (gcd (m::nat) n) = gcd (fib m) (fib n)"
3.259 +lemma fib_gcd_nat: "fib (gcd (m::nat) n) = gcd (fib m) (fib n)"
3.260 -- {* Law 6.111 *}
3.261 apply (induct m n rule: gcd_nat_induct)
3.262 apply (simp_all add: gcd_non_0_nat gcd_commute_nat gcd_fib_mod_nat)
3.263 @@ -297,7 +284,7 @@
3.264 fib (gcd (m::int) n) = gcd (fib m) (fib n)"
3.265 by (erule fib_gcd_nat [transferred])
3.266
3.267 -lemma atMost_plus_one_nat: "{..(k::nat) + 1} = insert (k + 1) {..k}"
3.268 +lemma atMost_plus_one_nat: "{..(k::nat) + 1} = insert (k + 1) {..k}"
3.269 by auto
3.270
3.271 theorem fib_mult_eq_setsum_nat:
4.1 --- a/src/HOL/Number_Theory/MiscAlgebra.thy Sat Sep 10 22:11:55 2011 +0200
4.2 +++ b/src/HOL/Number_Theory/MiscAlgebra.thy Sat Sep 10 23:27:32 2011 +0200
4.3 @@ -12,7 +12,7 @@
4.4
4.5 (* finiteness stuff *)
4.6
4.7 -lemma bounded_set1_int [intro]: "finite {(x::int). a < x & x < b & P x}"
4.8 +lemma bounded_set1_int [intro]: "finite {(x::int). a < x & x < b & P x}"
4.9 apply (subgoal_tac "{x. a < x & x < b & P x} <= {a<..<b}")
4.10 apply (erule finite_subset)
4.11 apply auto
4.12 @@ -64,7 +64,7 @@
4.13 apply auto
4.14 apply (rule_tac x = "inv x" in bexI)
4.15 apply auto
4.16 -done
4.17 + done
4.18
4.19 lemma (in comm_monoid) units_comm_group: "comm_group(units_of G)"
4.20 apply (rule group.group_comm_groupI)
4.21 @@ -75,15 +75,15 @@
4.22 done
4.23
4.24 lemma units_of_carrier: "carrier (units_of G) = Units G"
4.25 - by (unfold units_of_def, auto)
4.26 + unfolding units_of_def by auto
4.27
4.28 lemma units_of_mult: "mult(units_of G) = mult G"
4.29 - by (unfold units_of_def, auto)
4.30 + unfolding units_of_def by auto
4.31
4.32 lemma units_of_one: "one(units_of G) = one G"
4.33 - by (unfold units_of_def, auto)
4.34 + unfolding units_of_def by auto
4.35
4.36 -lemma (in monoid) units_of_inv: "x : Units G ==>
4.37 +lemma (in monoid) units_of_inv: "x : Units G ==>
4.38 m_inv (units_of G) x = m_inv G x"
4.39 apply (rule sym)
4.40 apply (subst m_inv_def)
4.41 @@ -105,12 +105,12 @@
4.42 apply (erule group.l_inv, assumption)
4.43 done
4.44
4.45 -lemma (in group) inj_on_const_mult: "a: (carrier G) ==>
4.46 +lemma (in group) inj_on_const_mult: "a: (carrier G) ==>
4.47 inj_on (%x. a \<otimes> x) (carrier G)"
4.48 - by (unfold inj_on_def, auto)
4.49 + unfolding inj_on_def by auto
4.50
4.51 lemma (in group) surj_const_mult: "a : (carrier G) ==>
4.52 - (%x. a \<otimes> x) ` (carrier G) = (carrier G)"
4.53 + (%x. a \<otimes> x) ` (carrier G) = (carrier G)"
4.54 apply (auto simp add: image_def)
4.55 apply (rule_tac x = "(m_inv G a) \<otimes> x" in bexI)
4.56 apply auto
4.57 @@ -118,7 +118,7 @@
4.58 for mult_ac rewriting. *)
4.59 apply (subst m_assoc [symmetric])
4.60 apply auto
4.61 -done
4.62 + done
4.63
4.64 lemma (in group) l_cancel_one [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
4.65 (x \<otimes> a = x) = (a = one G)"
4.66 @@ -127,7 +127,7 @@
4.67 prefer 4
4.68 apply (erule ssubst)
4.69 apply auto
4.70 -done
4.71 + done
4.72
4.73 lemma (in group) r_cancel_one [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
4.74 (a \<otimes> x = x) = (a = one G)"
4.75 @@ -136,28 +136,32 @@
4.76 prefer 4
4.77 apply (erule ssubst)
4.78 apply auto
4.79 -done
4.80 + done
4.81
4.82 (* Is there a better way to do this? *)
4.83
4.84 lemma (in group) l_cancel_one' [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
4.85 (x = x \<otimes> a) = (a = one G)"
4.86 - by (subst eq_commute, simp)
4.87 + apply (subst eq_commute)
4.88 + apply simp
4.89 + done
4.90
4.91 lemma (in group) r_cancel_one' [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
4.92 (x = a \<otimes> x) = (a = one G)"
4.93 - by (subst eq_commute, simp)
4.94 + apply (subst eq_commute)
4.95 + apply simp
4.96 + done
4.97
4.98 (* This should be generalized to arbitrary groups, not just commutative
4.99 ones, using Lagrange's theorem. *)
4.100
4.101 lemma (in comm_group) power_order_eq_one:
4.102 - assumes fin [simp]: "finite (carrier G)"
4.103 - and a [simp]: "a : carrier G"
4.104 - shows "a (^) card(carrier G) = one G"
4.105 + assumes fin [simp]: "finite (carrier G)"
4.106 + and a [simp]: "a : carrier G"
4.107 + shows "a (^) card(carrier G) = one G"
4.108 proof -
4.109 have "(\<Otimes>x:carrier G. x) = (\<Otimes>x:carrier G. a \<otimes> x)"
4.110 - by (subst (2) finprod_reindex [symmetric],
4.111 + by (subst (2) finprod_reindex [symmetric],
4.112 auto simp add: Pi_def inj_on_const_mult surj_const_mult)
4.113 also have "\<dots> = (\<Otimes>x:carrier G. a) \<otimes> (\<Otimes>x:carrier G. x)"
4.114 by (auto simp add: finprod_multf Pi_def)
4.115 @@ -178,7 +182,7 @@
4.116 apply (rule trans)
4.117 apply (subgoal_tac "a = (a \<otimes> b) \<otimes> inv b")
4.118 apply assumption
4.119 - apply (subst m_assoc)
4.120 + apply (subst m_assoc)
4.121 apply auto
4.122 apply (unfold Units_def)
4.123 apply auto
4.124 @@ -200,20 +204,20 @@
4.125 x \<otimes> y = \<one> \<Longrightarrow> inv x = y"
4.126 apply (rule inv_char)
4.127 apply auto
4.128 - apply (subst m_comm, auto)
4.129 + apply (subst m_comm, auto)
4.130 done
4.131
4.132 -lemma (in ring) inv_neg_one [simp]: "inv (\<ominus> \<one>) = \<ominus> \<one>"
4.133 +lemma (in ring) inv_neg_one [simp]: "inv (\<ominus> \<one>) = \<ominus> \<one>"
4.134 apply (rule inv_char)
4.135 apply (auto simp add: l_minus r_minus)
4.136 done
4.137
4.138 -lemma (in monoid) inv_eq_imp_eq: "x : Units G \<Longrightarrow> y : Units G \<Longrightarrow>
4.139 +lemma (in monoid) inv_eq_imp_eq: "x : Units G \<Longrightarrow> y : Units G \<Longrightarrow>
4.140 inv x = inv y \<Longrightarrow> x = y"
4.141 apply (subgoal_tac "inv(inv x) = inv(inv y)")
4.142 apply (subst (asm) Units_inv_inv)+
4.143 apply auto
4.144 -done
4.145 + done
4.146
4.147 lemma (in ring) Units_minus_one_closed [intro]: "\<ominus> \<one> : Units R"
4.148 apply (unfold Units_def)
4.149 @@ -221,24 +225,24 @@
4.150 apply (rule_tac x = "\<ominus> \<one>" in bexI)
4.151 apply auto
4.152 apply (simp add: l_minus r_minus)
4.153 -done
4.154 + done
4.155
4.156 lemma (in monoid) inv_one [simp]: "inv \<one> = \<one>"
4.157 apply (rule inv_char)
4.158 apply auto
4.159 -done
4.160 + done
4.161
4.162 lemma (in ring) inv_eq_neg_one_eq: "x : Units R \<Longrightarrow> (inv x = \<ominus> \<one>) = (x = \<ominus> \<one>)"
4.163 apply auto
4.164 apply (subst Units_inv_inv [symmetric])
4.165 apply auto
4.166 -done
4.167 + done
4.168
4.169 lemma (in monoid) inv_eq_one_eq: "x : Units G \<Longrightarrow> (inv x = \<one>) = (x = \<one>)"
4.170 apply auto
4.171 apply (subst Units_inv_inv [symmetric])
4.172 apply auto
4.173 -done
4.174 + done
4.175
4.176
4.177 (* This goes in FiniteProduct *)
4.178 @@ -256,29 +260,28 @@
4.179 apply (erule finite_UN_I)
4.180 apply blast
4.181 apply (fastsimp)
4.182 - apply (auto intro!: funcsetI finprod_closed)
4.183 -done
4.184 + apply (auto intro!: funcsetI finprod_closed)
4.185 + done
4.186
4.187 lemma (in comm_monoid) finprod_Union_disjoint:
4.188 "[| finite C; (ALL A:C. finite A & (ALL x:A. f x : carrier G));
4.189 - (ALL A:C. ALL B:C. A ~= B --> A Int B = {}) |]
4.190 - ==> finprod G f (Union C) = finprod G (finprod G f) C"
4.191 + (ALL A:C. ALL B:C. A ~= B --> A Int B = {}) |]
4.192 + ==> finprod G f (Union C) = finprod G (finprod G f) C"
4.193 apply (frule finprod_UN_disjoint [of C id f])
4.194 apply (auto simp add: SUP_def)
4.195 -done
4.196 + done
4.197
4.198 -lemma (in comm_monoid) finprod_one [rule_format]:
4.199 - "finite A \<Longrightarrow> (ALL x:A. f x = \<one>) \<longrightarrow>
4.200 - finprod G f A = \<one>"
4.201 -by (induct set: finite) auto
4.202 +lemma (in comm_monoid) finprod_one:
4.203 + "finite A \<Longrightarrow> (\<And>x. x:A \<Longrightarrow> f x = \<one>) \<Longrightarrow> finprod G f A = \<one>"
4.204 + by (induct set: finite) auto
4.205
4.206
4.207 (* need better simplification rules for rings *)
4.208 (* the next one holds more generally for abelian groups *)
4.209
4.210 lemma (in cring) sum_zero_eq_neg:
4.211 - "x : carrier R \<Longrightarrow> y : carrier R \<Longrightarrow> x \<oplus> y = \<zero> \<Longrightarrow> x = \<ominus> y"
4.212 - apply (subgoal_tac "\<ominus> y = \<zero> \<oplus> \<ominus> y")
4.213 + "x : carrier R \<Longrightarrow> y : carrier R \<Longrightarrow> x \<oplus> y = \<zero> \<Longrightarrow> x = \<ominus> y"
4.214 + apply (subgoal_tac "\<ominus> y = \<zero> \<oplus> \<ominus> y")
4.215 apply (erule ssubst)back
4.216 apply (erule subst)
4.217 apply (simp_all add: ring_simprules)
4.218 @@ -287,7 +290,7 @@
4.219 (* there's a name conflict -- maybe "domain" should be
4.220 "integral_domain" *)
4.221
4.222 -lemma (in Ring.domain) square_eq_one:
4.223 +lemma (in Ring.domain) square_eq_one:
4.224 fixes x
4.225 assumes [simp]: "x : carrier R" and
4.226 "x \<otimes> x = \<one>"
4.227 @@ -298,15 +301,15 @@
4.228 also with `x \<otimes> x = \<one>` have "\<dots> = \<zero>"
4.229 by (simp add: ring_simprules)
4.230 finally have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = \<zero>" .
4.231 - hence "(x \<oplus> \<one>) = \<zero> | (x \<oplus> \<ominus> \<one>) = \<zero>"
4.232 + then have "(x \<oplus> \<one>) = \<zero> | (x \<oplus> \<ominus> \<one>) = \<zero>"
4.233 by (intro integral, auto)
4.234 - thus ?thesis
4.235 + then show ?thesis
4.236 apply auto
4.237 apply (erule notE)
4.238 apply (rule sum_zero_eq_neg)
4.239 apply auto
4.240 apply (subgoal_tac "x = \<ominus> (\<ominus> \<one>)")
4.241 - apply (simp add: ring_simprules)
4.242 + apply (simp add: ring_simprules)
4.243 apply (rule sum_zero_eq_neg)
4.244 apply auto
4.245 done
4.246 @@ -318,7 +321,7 @@
4.247 apply auto
4.248 apply (erule ssubst)back
4.249 apply (erule Units_r_inv)
4.250 -done
4.251 + done
4.252
4.253
4.254 (*
4.255 @@ -327,15 +330,15 @@
4.256 needed.)
4.257 *)
4.258
4.259 -lemma (in ring) finite_ring_finite_units [intro]: "finite (carrier R) \<Longrightarrow>
4.260 - finite (Units R)"
4.261 - by (rule finite_subset, auto)
4.262 +lemma (in ring) finite_ring_finite_units [intro]:
4.263 + "finite (carrier R) \<Longrightarrow> finite (Units R)"
4.264 + by (rule finite_subset) auto
4.265
4.266 (* this belongs with MiscAlgebra.thy *)
4.267 -lemma (in monoid) units_of_pow:
4.268 +lemma (in monoid) units_of_pow:
4.269 "x : Units G \<Longrightarrow> x (^)\<^bsub>units_of G\<^esub> (n::nat) = x (^)\<^bsub>G\<^esub> n"
4.270 apply (induct n)
4.271 - apply (auto simp add: units_group group.is_monoid
4.272 + apply (auto simp add: units_group group.is_monoid
4.273 monoid.nat_pow_0 monoid.nat_pow_Suc units_of_one units_of_mult)
4.274 done
4.275
5.1 --- a/src/HOL/Number_Theory/Primes.thy Sat Sep 10 22:11:55 2011 +0200
5.2 +++ b/src/HOL/Number_Theory/Primes.thy Sat Sep 10 23:27:32 2011 +0200
5.3 @@ -31,54 +31,41 @@
5.4 imports "~~/src/HOL/GCD"
5.5 begin
5.6
5.7 -declare One_nat_def [simp del]
5.8 -
5.9 class prime = one +
5.10 -
5.11 -fixes
5.12 - prime :: "'a \<Rightarrow> bool"
5.13 + fixes prime :: "'a \<Rightarrow> bool"
5.14
5.15 instantiation nat :: prime
5.16 -
5.17 begin
5.18
5.19 -definition
5.20 - prime_nat :: "nat \<Rightarrow> bool"
5.21 -where
5.22 - "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
5.23 +definition prime_nat :: "nat \<Rightarrow> bool"
5.24 + where "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
5.25
5.26 -instance proof qed
5.27 +instance ..
5.28
5.29 end
5.30
5.31 instantiation int :: prime
5.32 -
5.33 begin
5.34
5.35 -definition
5.36 - prime_int :: "int \<Rightarrow> bool"
5.37 -where
5.38 - "prime_int p = prime (nat p)"
5.39 +definition prime_int :: "int \<Rightarrow> bool"
5.40 + where "prime_int p = prime (nat p)"
5.41
5.42 -instance proof qed
5.43 +instance ..
5.44
5.45 end
5.46
5.47
5.48 subsection {* Set up Transfer *}
5.49
5.50 -
5.51 lemma transfer_nat_int_prime:
5.52 "(x::int) >= 0 \<Longrightarrow> prime (nat x) = prime x"
5.53 - unfolding gcd_int_def lcm_int_def prime_int_def
5.54 - by auto
5.55 + unfolding gcd_int_def lcm_int_def prime_int_def by auto
5.56
5.57 declare transfer_morphism_nat_int[transfer add return:
5.58 transfer_nat_int_prime]
5.59
5.60 -lemma transfer_int_nat_prime:
5.61 - "prime (int x) = prime x"
5.62 - by (unfold gcd_int_def lcm_int_def prime_int_def, auto)
5.63 +lemma transfer_int_nat_prime: "prime (int x) = prime x"
5.64 + unfolding gcd_int_def lcm_int_def prime_int_def by auto
5.65
5.66 declare transfer_morphism_int_nat[transfer add return:
5.67 transfer_int_nat_prime]
5.68 @@ -94,52 +81,54 @@
5.69 unfolding prime_int_def
5.70 apply (frule prime_odd_nat)
5.71 apply (auto simp add: even_nat_def)
5.72 -done
5.73 + done
5.74
5.75 (* FIXME Is there a better way to handle these, rather than making them elim rules? *)
5.76
5.77 lemma prime_ge_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 0"
5.78 - by (unfold prime_nat_def, auto)
5.79 + unfolding prime_nat_def by auto
5.80
5.81 lemma prime_gt_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 0"
5.82 - by (unfold prime_nat_def, auto)
5.83 + unfolding prime_nat_def by auto
5.84
5.85 lemma prime_ge_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 1"
5.86 - by (unfold prime_nat_def, auto)
5.87 + unfolding prime_nat_def by auto
5.88
5.89 lemma prime_gt_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 1"
5.90 - by (unfold prime_nat_def, auto)
5.91 + unfolding prime_nat_def by auto
5.92
5.93 lemma prime_ge_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= Suc 0"
5.94 - by (unfold prime_nat_def, auto)
5.95 + unfolding prime_nat_def by auto
5.96
5.97 lemma prime_gt_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > Suc 0"
5.98 - by (unfold prime_nat_def, auto)
5.99 + unfolding prime_nat_def by auto
5.100
5.101 lemma prime_ge_2_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 2"
5.102 - by (unfold prime_nat_def, auto)
5.103 + unfolding prime_nat_def by auto
5.104
5.105 lemma prime_ge_0_int [elim]: "prime (p::int) \<Longrightarrow> p >= 0"
5.106 - by (unfold prime_int_def prime_nat_def) auto
5.107 + unfolding prime_int_def prime_nat_def by auto
5.108
5.109 lemma prime_gt_0_int [elim]: "prime (p::int) \<Longrightarrow> p > 0"
5.110 - by (unfold prime_int_def prime_nat_def, auto)
5.111 + unfolding prime_int_def prime_nat_def by auto
5.112
5.113 lemma prime_ge_1_int [elim]: "prime (p::int) \<Longrightarrow> p >= 1"
5.114 - by (unfold prime_int_def prime_nat_def, auto)
5.115 + unfolding prime_int_def prime_nat_def by auto
5.116
5.117 lemma prime_gt_1_int [elim]: "prime (p::int) \<Longrightarrow> p > 1"
5.118 - by (unfold prime_int_def prime_nat_def, auto)
5.119 + unfolding prime_int_def prime_nat_def by auto
5.120
5.121 lemma prime_ge_2_int [elim]: "prime (p::int) \<Longrightarrow> p >= 2"
5.122 - by (unfold prime_int_def prime_nat_def, auto)
5.123 + unfolding prime_int_def prime_nat_def by auto
5.124
5.125
5.126 lemma prime_int_altdef: "prime (p::int) = (1 < p \<and> (\<forall>m \<ge> 0. m dvd p \<longrightarrow>
5.127 m = 1 \<or> m = p))"
5.128 using prime_nat_def [transferred]
5.129 - apply (case_tac "p >= 0")
5.130 - by (blast, auto simp add: prime_ge_0_int)
5.131 + apply (cases "p >= 0")
5.132 + apply blast
5.133 + apply (auto simp add: prime_ge_0_int)
5.134 + done
5.135
5.136 lemma prime_imp_coprime_nat: "prime (p::nat) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
5.137 apply (unfold prime_nat_def)
5.138 @@ -168,26 +157,29 @@
5.139 lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
5.140 EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
5.141 unfolding prime_nat_def dvd_def apply auto
5.142 - by(metis mult_commute linorder_neq_iff linorder_not_le mult_1 n_less_n_mult_m one_le_mult_iff less_imp_le_nat)
5.143 + by (metis mult_commute linorder_neq_iff linorder_not_le mult_1
5.144 + n_less_n_mult_m one_le_mult_iff less_imp_le_nat)
5.145
5.146 lemma not_prime_eq_prod_int: "(n::int) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
5.147 EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
5.148 unfolding prime_int_altdef dvd_def
5.149 apply auto
5.150 - by(metis div_mult_self1_is_id div_mult_self2_is_id int_div_less_self int_one_le_iff_zero_less zero_less_mult_pos less_le)
5.151 + by (metis div_mult_self1_is_id div_mult_self2_is_id
5.152 + int_div_less_self int_one_le_iff_zero_less zero_less_mult_pos less_le)
5.153
5.154 lemma prime_dvd_power_nat [rule_format]: "prime (p::nat) -->
5.155 n > 0 --> (p dvd x^n --> p dvd x)"
5.156 - by (induct n rule: nat_induct, auto)
5.157 + by (induct n rule: nat_induct) auto
5.158
5.159 lemma prime_dvd_power_int [rule_format]: "prime (p::int) -->
5.160 n > 0 --> (p dvd x^n --> p dvd x)"
5.161 - apply (induct n rule: nat_induct, auto)
5.162 + apply (induct n rule: nat_induct)
5.163 + apply auto
5.164 apply (frule prime_ge_0_int)
5.165 apply auto
5.166 -done
5.167 + done
5.168
5.169 -subsubsection{* Make prime naively executable *}
5.170 +subsubsection {* Make prime naively executable *}
5.171
5.172 lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
5.173 by (simp add: prime_nat_def)
5.174 @@ -205,89 +197,87 @@
5.175 by (simp add: prime_int_def)
5.176
5.177 lemma prime_nat_code [code]:
5.178 - "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
5.179 -apply (simp add: Ball_def)
5.180 -apply (metis less_not_refl prime_nat_def dvd_triv_right not_prime_eq_prod_nat)
5.181 -done
5.182 + "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
5.183 + apply (simp add: Ball_def)
5.184 + apply (metis less_not_refl prime_nat_def dvd_triv_right not_prime_eq_prod_nat)
5.185 + done
5.186
5.187 lemma prime_nat_simp:
5.188 - "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
5.189 -by (auto simp add: prime_nat_code)
5.190 + "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
5.191 + by (auto simp add: prime_nat_code)
5.192
5.193 lemmas prime_nat_simp_number_of [simp] = prime_nat_simp [of "number_of m", standard]
5.194
5.195 lemma prime_int_code [code]:
5.196 "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?L = ?R")
5.197 proof
5.198 - assume "?L" thus "?R"
5.199 + assume "?L"
5.200 + then show "?R"
5.201 by (clarsimp simp: prime_gt_1_int) (metis int_one_le_iff_zero_less prime_int_altdef less_le)
5.202 next
5.203 - assume "?R" thus "?L" by (clarsimp simp:Ball_def) (metis dvdI not_prime_eq_prod_int)
5.204 + assume "?R"
5.205 + then show "?L" by (clarsimp simp: Ball_def) (metis dvdI not_prime_eq_prod_int)
5.206 qed
5.207
5.208 -lemma prime_int_simp:
5.209 - "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..p - 1]. ~ n dvd p)"
5.210 -by (auto simp add: prime_int_code)
5.211 +lemma prime_int_simp: "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..p - 1]. ~ n dvd p)"
5.212 + by (auto simp add: prime_int_code)
5.213
5.214 lemmas prime_int_simp_number_of [simp] = prime_int_simp [of "number_of m", standard]
5.215
5.216 lemma two_is_prime_nat [simp]: "prime (2::nat)"
5.217 -by simp
5.218 + by simp
5.219
5.220 lemma two_is_prime_int [simp]: "prime (2::int)"
5.221 -by simp
5.222 + by simp
5.223
5.224 text{* A bit of regression testing: *}
5.225
5.226 -lemma "prime(97::nat)"
5.227 -by simp
5.228 -
5.229 -lemma "prime(97::int)"
5.230 -by simp
5.231 -
5.232 -lemma "prime(997::nat)"
5.233 -by eval
5.234 -
5.235 -lemma "prime(997::int)"
5.236 -by eval
5.237 +lemma "prime(97::nat)" by simp
5.238 +lemma "prime(97::int)" by simp
5.239 +lemma "prime(997::nat)" by eval
5.240 +lemma "prime(997::int)" by eval
5.241
5.242
5.243 lemma prime_imp_power_coprime_nat: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
5.244 apply (rule coprime_exp_nat)
5.245 apply (subst gcd_commute_nat)
5.246 apply (erule (1) prime_imp_coprime_nat)
5.247 -done
5.248 + done
5.249
5.250 lemma prime_imp_power_coprime_int: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
5.251 apply (rule coprime_exp_int)
5.252 apply (subst gcd_commute_int)
5.253 apply (erule (1) prime_imp_coprime_int)
5.254 -done
5.255 + done
5.256
5.257 lemma primes_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
5.258 apply (rule prime_imp_coprime_nat, assumption)
5.259 - apply (unfold prime_nat_def, auto)
5.260 -done
5.261 + apply (unfold prime_nat_def)
5.262 + apply auto
5.263 + done
5.264
5.265 lemma primes_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
5.266 apply (rule prime_imp_coprime_int, assumption)
5.267 apply (unfold prime_int_altdef)
5.268 apply (metis int_one_le_iff_zero_less less_le)
5.269 -done
5.270 + done
5.271
5.272 -lemma primes_imp_powers_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
5.273 +lemma primes_imp_powers_coprime_nat:
5.274 + "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
5.275 by (rule coprime_exp2_nat, rule primes_coprime_nat)
5.276
5.277 -lemma primes_imp_powers_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
5.278 +lemma primes_imp_powers_coprime_int:
5.279 + "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
5.280 by (rule coprime_exp2_int, rule primes_coprime_int)
5.281
5.282 lemma prime_factor_nat: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n"
5.283 apply (induct n rule: nat_less_induct)
5.284 apply (case_tac "n = 0")
5.285 - using two_is_prime_nat apply blast
5.286 - apply (metis One_nat_def dvd.order_trans dvd_refl less_Suc0 linorder_neqE_nat nat_dvd_not_less
5.287 - neq0_conv prime_nat_def)
5.288 -done
5.289 + using two_is_prime_nat
5.290 + apply blast
5.291 + apply (metis One_nat_def dvd.order_trans dvd_refl less_Suc0 linorder_neqE_nat
5.292 + nat_dvd_not_less neq0_conv prime_nat_def)
5.293 + done
5.294
5.295 (* An Isar version:
5.296
5.297 @@ -301,7 +291,7 @@
5.298 fix n :: nat
5.299 assume "n ~= 1" and
5.300 ih: "\<forall>m<n. m \<noteq> 1 \<longrightarrow> (\<exists>p. prime p \<and> p dvd m)"
5.301 - thus "\<exists>p. prime p \<and> p dvd n"
5.302 + then show "\<exists>p. prime p \<and> p dvd n"
5.303 proof -
5.304 {
5.305 assume "n = 0"
5.306 @@ -312,7 +302,7 @@
5.307 moreover
5.308 {
5.309 assume "prime n"
5.310 - hence ?thesis by auto
5.311 + then have ?thesis by auto
5.312 }
5.313 moreover
5.314 {
5.315 @@ -335,13 +325,14 @@
5.316 assumes p: "prime (p::nat)" and ab: "coprime a b" and pab: "p^n dvd a * b"
5.317 shows "p^n dvd a \<or> p^n dvd b"
5.318 proof-
5.319 - {assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis
5.320 + { assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis
5.321 apply (cases "n=0", simp_all)
5.322 - apply (cases "a=1", simp_all) done}
5.323 + apply (cases "a=1", simp_all)
5.324 + done }
5.325 moreover
5.326 - {assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1"
5.327 - then obtain m where m: "n = Suc m" by (cases n, auto)
5.328 - from n have "p dvd p^n" by (intro dvd_power, auto)
5.329 + { assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1"
5.330 + then obtain m where m: "n = Suc m" by (cases n) auto
5.331 + from n have "p dvd p^n" apply (intro dvd_power) apply auto done
5.332 also note pab
5.333 finally have pab': "p dvd a * b".
5.334 from prime_dvd_mult_nat[OF p pab']
5.335 @@ -351,7 +342,7 @@
5.336 from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto
5.337 with p have "coprime b p"
5.338 by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
5.339 - hence pnb: "coprime (p^n) b"
5.340 + then have pnb: "coprime (p^n) b"
5.341 by (subst gcd_commute_nat, rule coprime_exp_nat)
5.342 from coprime_dvd_mult_nat[OF pnb pab] have ?thesis by blast }
5.343 moreover
5.344 @@ -361,39 +352,39 @@
5.345 by auto
5.346 with p have "coprime a p"
5.347 by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
5.348 - hence pna: "coprime (p^n) a"
5.349 + then have pna: "coprime (p^n) a"
5.350 by (subst gcd_commute_nat, rule coprime_exp_nat)
5.351 from coprime_dvd_mult_nat[OF pna pnba] have ?thesis by blast }
5.352 - ultimately have ?thesis by blast}
5.353 + ultimately have ?thesis by blast }
5.354 ultimately show ?thesis by blast
5.355 qed
5.356
5.357 +
5.358 subsection {* Infinitely many primes *}
5.359
5.360 lemma next_prime_bound: "\<exists>(p::nat). prime p \<and> n < p \<and> p <= fact n + 1"
5.361 proof-
5.362 have f1: "fact n + 1 \<noteq> 1" using fact_ge_one_nat [of n] by arith
5.363 from prime_factor_nat [OF f1]
5.364 - obtain p where "prime p" and "p dvd fact n + 1" by auto
5.365 - hence "p \<le> fact n + 1"
5.366 - by (intro dvd_imp_le, auto)
5.367 - {assume "p \<le> n"
5.368 + obtain p where "prime p" and "p dvd fact n + 1" by auto
5.369 + then have "p \<le> fact n + 1" apply (intro dvd_imp_le) apply auto done
5.370 + { assume "p \<le> n"
5.371 from `prime p` have "p \<ge> 1"
5.372 by (cases p, simp_all)
5.373 with `p <= n` have "p dvd fact n"
5.374 by (intro dvd_fact_nat)
5.375 with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n"
5.376 by (rule dvd_diff_nat)
5.377 - hence "p dvd 1" by simp
5.378 - hence "p <= 1" by auto
5.379 + then have "p dvd 1" by simp
5.380 + then have "p <= 1" by auto
5.381 moreover from `prime p` have "p > 1" by auto
5.382 ultimately have False by auto}
5.383 - hence "n < p" by arith
5.384 + then have "n < p" by presburger
5.385 with `prime p` and `p <= fact n + 1` show ?thesis by auto
5.386 qed
5.387
5.388 lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)"
5.389 -using next_prime_bound by auto
5.390 + using next_prime_bound by auto
5.391
5.392 lemma primes_infinite: "\<not> (finite {(p::nat). prime p})"
5.393 proof
5.394 @@ -402,8 +393,8 @@
5.395 by auto
5.396 then obtain b where "ALL (x::nat). prime x \<longrightarrow> x <= b"
5.397 by auto
5.398 - with bigger_prime [of b] show False by auto
5.399 + with bigger_prime [of b] show False
5.400 + by auto
5.401 qed
5.402
5.403 -
5.404 end
6.1 --- a/src/HOL/Number_Theory/Residues.thy Sat Sep 10 22:11:55 2011 +0200
6.2 +++ b/src/HOL/Number_Theory/Residues.thy Sat Sep 10 23:27:32 2011 +0200
6.3 @@ -16,14 +16,14 @@
6.4
6.5
6.6 (*
6.7 -
6.8 +
6.9 A locale for residue rings
6.10
6.11 *)
6.12
6.13 definition residue_ring :: "int => int ring" where
6.14 - "residue_ring m == (|
6.15 - carrier = {0..m - 1},
6.16 + "residue_ring m == (|
6.17 + carrier = {0..m - 1},
6.18 mult = (%x y. (x * y) mod m),
6.19 one = 1,
6.20 zero = 0,
6.21 @@ -34,7 +34,8 @@
6.22 assumes m_gt_one: "m > 1"
6.23 defines "R == residue_ring m"
6.24
6.25 -context residues begin
6.26 +context residues
6.27 +begin
6.28
6.29 lemma abelian_group: "abelian_group R"
6.30 apply (insert m_gt_one)
6.31 @@ -79,23 +80,23 @@
6.32 context residues
6.33 begin
6.34
6.35 -(* These lemmas translate back and forth between internal and
6.36 +(* These lemmas translate back and forth between internal and
6.37 external concepts *)
6.38
6.39 lemma res_carrier_eq: "carrier R = {0..m - 1}"
6.40 - by (unfold R_def residue_ring_def, auto)
6.41 + unfolding R_def residue_ring_def by auto
6.42
6.43 lemma res_add_eq: "x \<oplus> y = (x + y) mod m"
6.44 - by (unfold R_def residue_ring_def, auto)
6.45 + unfolding R_def residue_ring_def by auto
6.46
6.47 lemma res_mult_eq: "x \<otimes> y = (x * y) mod m"
6.48 - by (unfold R_def residue_ring_def, auto)
6.49 + unfolding R_def residue_ring_def by auto
6.50
6.51 lemma res_zero_eq: "\<zero> = 0"
6.52 - by (unfold R_def residue_ring_def, auto)
6.53 + unfolding R_def residue_ring_def by auto
6.54
6.55 lemma res_one_eq: "\<one> = 1"
6.56 - by (unfold R_def residue_ring_def units_of_def, auto)
6.57 + unfolding R_def residue_ring_def units_of_def by auto
6.58
6.59 lemma res_units_eq: "Units R = { x. 0 < x & x < m & coprime x m}"
6.60 apply (insert m_gt_one)
6.61 @@ -127,14 +128,14 @@
6.62 apply auto
6.63 done
6.64
6.65 -lemma finite [iff]: "finite(carrier R)"
6.66 +lemma finite [iff]: "finite (carrier R)"
6.67 by (subst res_carrier_eq, auto)
6.68
6.69 -lemma finite_Units [iff]: "finite(Units R)"
6.70 +lemma finite_Units [iff]: "finite (Units R)"
6.71 by (subst res_units_eq, auto)
6.72
6.73 -(* The function a -> a mod m maps the integers to the
6.74 - residue classes. The following lemmas show that this mapping
6.75 +(* The function a -> a mod m maps the integers to the
6.76 + residue classes. The following lemmas show that this mapping
6.77 respects addition and multiplication on the integers. *)
6.78
6.79 lemma mod_in_carrier [iff]: "a mod m : carrier R"
6.80 @@ -143,7 +144,10 @@
6.81 done
6.82
6.83 lemma add_cong: "(x mod m) \<oplus> (y mod m) = (x + y) mod m"
6.84 - by (unfold R_def residue_ring_def, auto, arith)
6.85 + unfolding R_def residue_ring_def
6.86 + apply auto
6.87 + apply presburger
6.88 + done
6.89
6.90 lemma mult_cong: "(x mod m) \<otimes> (y mod m) = (x * y) mod m"
6.91 apply (unfold R_def residue_ring_def, auto)
6.92 @@ -155,13 +159,10 @@
6.93 done
6.94
6.95 lemma zero_cong: "\<zero> = 0"
6.96 - apply (unfold R_def residue_ring_def, auto)
6.97 - done
6.98 + unfolding R_def residue_ring_def by auto
6.99
6.100 lemma one_cong: "\<one> = 1 mod m"
6.101 - apply (insert m_gt_one)
6.102 - apply (unfold R_def residue_ring_def, auto)
6.103 - done
6.104 + using m_gt_one unfolding R_def residue_ring_def by auto
6.105
6.106 (* revise algebra library to use 1? *)
6.107 lemma pow_cong: "(x mod m) (^) n = x^n mod m"
6.108 @@ -181,19 +182,19 @@
6.109 apply auto
6.110 done
6.111
6.112 -lemma (in residues) prod_cong:
6.113 - "finite A \<Longrightarrow> (\<Otimes> i:A. (f i) mod m) = (PROD i:A. f i) mod m"
6.114 +lemma (in residues) prod_cong:
6.115 + "finite A \<Longrightarrow> (\<Otimes> i:A. (f i) mod m) = (PROD i:A. f i) mod m"
6.116 apply (induct set: finite)
6.117 apply (auto simp: one_cong mult_cong)
6.118 done
6.119
6.120 lemma (in residues) sum_cong:
6.121 - "finite A \<Longrightarrow> (\<Oplus> i:A. (f i) mod m) = (SUM i: A. f i) mod m"
6.122 + "finite A \<Longrightarrow> (\<Oplus> i:A. (f i) mod m) = (SUM i: A. f i) mod m"
6.123 apply (induct set: finite)
6.124 apply (auto simp: zero_cong add_cong)
6.125 done
6.126
6.127 -lemma mod_in_res_units [simp]: "1 < m \<Longrightarrow> coprime a m \<Longrightarrow>
6.128 +lemma mod_in_res_units [simp]: "1 < m \<Longrightarrow> coprime a m \<Longrightarrow>
6.129 a mod m : Units R"
6.130 apply (subst res_units_eq, auto)
6.131 apply (insert pos_mod_sign [of m a])
6.132 @@ -204,10 +205,10 @@
6.133 apply (subst gcd_commute_int, assumption)
6.134 done
6.135
6.136 -lemma res_eq_to_cong: "((a mod m) = (b mod m)) = [a = b] (mod (m::int))"
6.137 +lemma res_eq_to_cong: "((a mod m) = (b mod m)) = [a = b] (mod (m::int))"
6.138 unfolding cong_int_def by auto
6.139
6.140 -(* Simplifying with these will translate a ring equation in R to a
6.141 +(* Simplifying with these will translate a ring equation in R to a
6.142 congruence. *)
6.143
6.144 lemmas res_to_cong_simps = add_cong mult_cong pow_cong one_cong
6.145 @@ -243,13 +244,13 @@
6.146 using p_prime apply auto
6.147 done
6.148
6.149 -context residues_prime begin
6.150 +context residues_prime
6.151 +begin
6.152
6.153 lemma is_field: "field R"
6.154 apply (rule cring.field_intro2)
6.155 apply (rule cring)
6.156 - apply (auto simp add: res_carrier_eq res_one_eq res_zero_eq
6.157 - res_units_eq)
6.158 + apply (auto simp add: res_carrier_eq res_one_eq res_zero_eq res_units_eq)
6.159 apply (rule classical)
6.160 apply (erule notE)
6.161 apply (subst gcd_commute_int)
6.162 @@ -285,25 +286,24 @@
6.163
6.164 (* the definition of the phi function *)
6.165
6.166 -definition phi :: "int => nat" where
6.167 - "phi m == card({ x. 0 < x & x < m & gcd x m = 1})"
6.168 +definition phi :: "int => nat"
6.169 + where "phi m = card({ x. 0 < x & x < m & gcd x m = 1})"
6.170
6.171 lemma phi_zero [simp]: "phi 0 = 0"
6.172 apply (subst phi_def)
6.173 -(* Auto hangs here. Once again, where is the simplification rule
6.174 +(* Auto hangs here. Once again, where is the simplification rule
6.175 1 == Suc 0 coming from? *)
6.176 apply (auto simp add: card_eq_0_iff)
6.177 (* Add card_eq_0_iff as a simp rule? delete card_empty_imp? *)
6.178 done
6.179
6.180 lemma phi_one [simp]: "phi 1 = 0"
6.181 - apply (auto simp add: phi_def card_eq_0_iff)
6.182 - done
6.183 + by (auto simp add: phi_def card_eq_0_iff)
6.184
6.185 lemma (in residues) phi_eq: "phi m = card(Units R)"
6.186 by (simp add: phi_def res_units_eq)
6.187
6.188 -lemma (in residues) euler_theorem1:
6.189 +lemma (in residues) euler_theorem1:
6.190 assumes a: "gcd a m = 1"
6.191 shows "[a^phi m = 1] (mod m)"
6.192 proof -
6.193 @@ -311,7 +311,7 @@
6.194 by (intro mod_in_res_units)
6.195 from phi_eq have "(a mod m) (^) (phi m) = (a mod m) (^) (card (Units R))"
6.196 by simp
6.197 - also have "\<dots> = \<one>"
6.198 + also have "\<dots> = \<one>"
6.199 by (intro units_power_order_eq_one, auto)
6.200 finally show ?thesis
6.201 by (simp add: res_to_cong_simps)
6.202 @@ -319,13 +319,13 @@
6.203
6.204 (* In fact, there is a two line proof!
6.205
6.206 -lemma (in residues) euler_theorem1:
6.207 +lemma (in residues) euler_theorem1:
6.208 assumes a: "gcd a m = 1"
6.209 shows "[a^phi m = 1] (mod m)"
6.210 proof -
6.211 have "(a mod m) (^) (phi m) = \<one>"
6.212 by (simp add: phi_eq units_power_order_eq_one a m_gt_one)
6.213 - thus ?thesis
6.214 + then show ?thesis
6.215 by (simp add: res_to_cong_simps)
6.216 qed
6.217
6.218 @@ -338,7 +338,7 @@
6.219 shows "[a^phi m = 1] (mod m)"
6.220 proof (cases)
6.221 assume "m = 0 | m = 1"
6.222 - thus ?thesis by auto
6.223 + then show ?thesis by auto
6.224 next
6.225 assume "~(m = 0 | m = 1)"
6.226 with assms show ?thesis
6.227 @@ -375,8 +375,8 @@
6.228
6.229 subsection {* Wilson's theorem *}
6.230
6.231 -lemma (in field) inv_pair_lemma: "x : Units R \<Longrightarrow> y : Units R \<Longrightarrow>
6.232 - {x, inv x} ~= {y, inv y} \<Longrightarrow> {x, inv x} Int {y, inv y} = {}"
6.233 +lemma (in field) inv_pair_lemma: "x : Units R \<Longrightarrow> y : Units R \<Longrightarrow>
6.234 + {x, inv x} ~= {y, inv y} \<Longrightarrow> {x, inv x} Int {y, inv y} = {}"
6.235 apply auto
6.236 apply (erule notE)
6.237 apply (erule inv_eq_imp_eq)
6.238 @@ -390,10 +390,10 @@
6.239 assumes a: "p > 2"
6.240 shows "[fact (p - 1) = - 1] (mod p)"
6.241 proof -
6.242 - let ?InversePairs = "{ {x, inv x} | x. x : Units R - {\<one>, \<ominus> \<one>}}"
6.243 + let ?InversePairs = "{ {x, inv x} | x. x : Units R - {\<one>, \<ominus> \<one>}}"
6.244 have UR: "Units R = {\<one>, \<ominus> \<one>} Un (Union ?InversePairs)"
6.245 by auto
6.246 - have "(\<Otimes>i: Units R. i) =
6.247 + have "(\<Otimes>i: Units R. i) =
6.248 (\<Otimes>i: {\<one>, \<ominus> \<one>}. i) \<otimes> (\<Otimes>i: Union ?InversePairs. i)"
6.249 apply (subst UR)
6.250 apply (subst finprod_Un_disjoint)
6.251 @@ -409,7 +409,7 @@
6.252 apply (frule one_eq_neg_one)
6.253 apply (insert a, force)
6.254 done
6.255 - also have "(\<Otimes>i:(Union ?InversePairs). i) =
6.256 + also have "(\<Otimes>i:(Union ?InversePairs). i) =
6.257 (\<Otimes>A: ?InversePairs. (\<Otimes>y:A. y))"
6.258 apply (subst finprod_Union_disjoint)
6.259 apply force
6.260 @@ -444,8 +444,7 @@
6.261 apply (subst res_prime_units_eq, rule refl)
6.262 done
6.263 finally have "fact (p - 1) mod p = \<ominus> \<one>".
6.264 - thus ?thesis
6.265 - by (simp add: res_to_cong_simps)
6.266 + then show ?thesis by (simp add: res_to_cong_simps)
6.267 qed
6.268
6.269 lemma wilson_theorem: "prime (p::int) \<Longrightarrow> [fact (p - 1) = - 1] (mod p)"
6.270 @@ -457,7 +456,6 @@
6.271 apply (rule residues_prime.wilson_theorem1)
6.272 apply (rule residues_prime.intro)
6.273 apply auto
6.274 -done
6.275 -
6.276 + done
6.277
6.278 end
7.1 --- a/src/HOL/Number_Theory/UniqueFactorization.thy Sat Sep 10 22:11:55 2011 +0200
7.2 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy Sat Sep 10 23:27:32 2011 +0200
7.3 @@ -42,7 +42,7 @@
7.4 apply auto
7.5 apply (subst setsum_Un_disjoint)
7.6 apply auto
7.7 -done
7.8 + done
7.9
7.10 lemma setprod_Un2: "finite (A Un B) \<Longrightarrow>
7.11 setprod f (A Un B) = setprod f (A - B) * setprod f (B - A) *
7.12 @@ -53,7 +53,7 @@
7.13 apply auto
7.14 apply (subst setprod_Un_disjoint)
7.15 apply auto
7.16 -done
7.17 + done
7.18
7.19 (* Here is a version of set product for multisets. Is it worth moving
7.20 to multiset.thy? If so, one should similarly define msetsum for abelian
7.21 @@ -71,12 +71,10 @@
7.22 translations
7.23 "PROD i :# A. b" == "CONST msetprod (%i. b) A"
7.24
7.25 -lemma msetprod_empty:
7.26 - "msetprod f {#} = 1"
7.27 +lemma msetprod_empty: "msetprod f {#} = 1"
7.28 by (simp add: msetprod_def)
7.29
7.30 -lemma msetprod_singleton:
7.31 - "msetprod f {#x#} = f x"
7.32 +lemma msetprod_singleton: "msetprod f {#x#} = f x"
7.33 by (simp add: msetprod_def)
7.34
7.35 lemma msetprod_Un: "msetprod f (A+B) = msetprod f A * msetprod f B"
7.36 @@ -105,7 +103,7 @@
7.37 apply (auto intro: setprod_cong)
7.38 apply (subst setprod_Un_disjoint [symmetric])
7.39 apply (auto intro: setprod_cong)
7.40 -done
7.41 + done
7.42
7.43
7.44 subsection {* unique factorization: multiset version *}
7.45 @@ -119,27 +117,23 @@
7.46 assume "(n::nat) > 0"
7.47 then have "n = 1 | (n > 1 & prime n) | (n > 1 & ~ prime n)"
7.48 by arith
7.49 - moreover
7.50 - {
7.51 + moreover {
7.52 assume "n = 1"
7.53 then have "(ALL p : set_of {#}. prime p) & n = (PROD i :# {#}. i)"
7.54 by (auto simp add: msetprod_def)
7.55 - }
7.56 - moreover
7.57 - {
7.58 + } moreover {
7.59 assume "n > 1" and "prime n"
7.60 then have "(ALL p : set_of {# n #}. prime p) & n = (PROD i :# {# n #}. i)"
7.61 by (auto simp add: msetprod_def)
7.62 - }
7.63 - moreover
7.64 - {
7.65 + } moreover {
7.66 assume "n > 1" and "~ prime n"
7.67 - with not_prime_eq_prod_nat obtain m k where n: "n = m * k & 1 < m & m < n & 1 < k & k < n"
7.68 - by blast
7.69 + with not_prime_eq_prod_nat
7.70 + obtain m k where n: "n = m * k & 1 < m & m < n & 1 < k & k < n"
7.71 + by blast
7.72 with ih obtain Q R where "(ALL p : set_of Q. prime p) & m = (PROD i:#Q. i)"
7.73 and "(ALL p: set_of R. prime p) & k = (PROD i:#R. i)"
7.74 by blast
7.75 - hence "(ALL p: set_of (Q + R). prime p) & n = (PROD i :# Q + R. i)"
7.76 + then have "(ALL p: set_of (Q + R). prime p) & n = (PROD i :# Q + R. i)"
7.77 by (auto simp add: n msetprod_Un)
7.78 then have "EX M. (ALL p : set_of M. prime p) & n = (PROD i :# M. i)"..
7.79 }
7.80 @@ -162,23 +156,21 @@
7.81 also have "... dvd (PROD i :# N. i)" by (rule assms)
7.82 also have "... = (PROD i : (set_of N). i ^ (count N i))"
7.83 by (simp add: msetprod_def)
7.84 - also have "... =
7.85 - a^(count N a) * (PROD i : (set_of N - {a}). i ^ (count N i))"
7.86 - proof (cases)
7.87 - assume "a : set_of N"
7.88 - hence b: "set_of N = {a} Un (set_of N - {a})"
7.89 - by auto
7.90 - thus ?thesis
7.91 - by (subst (1) b, subst setprod_Un_disjoint, auto)
7.92 - next
7.93 - assume "a ~: set_of N"
7.94 - thus ?thesis
7.95 - by auto
7.96 - qed
7.97 + also have "... = a^(count N a) * (PROD i : (set_of N - {a}). i ^ (count N i))"
7.98 + proof (cases)
7.99 + assume "a : set_of N"
7.100 + then have b: "set_of N = {a} Un (set_of N - {a})"
7.101 + by auto
7.102 + then show ?thesis
7.103 + by (subst (1) b, subst setprod_Un_disjoint, auto)
7.104 + next
7.105 + assume "a ~: set_of N"
7.106 + then show ?thesis by auto
7.107 + qed
7.108 finally have "a ^ count M a dvd
7.109 a^(count N a) * (PROD i : (set_of N - {a}). i ^ (count N i))".
7.110 - moreover have "coprime (a ^ count M a)
7.111 - (PROD i : (set_of N - {a}). i ^ (count N i))"
7.112 + moreover
7.113 + have "coprime (a ^ count M a) (PROD i : (set_of N - {a}). i ^ (count N i))"
7.114 apply (subst gcd_commute_nat)
7.115 apply (rule setprod_coprime_nat)
7.116 apply (rule primes_imp_powers_coprime_nat)
7.117 @@ -188,10 +180,12 @@
7.118 ultimately have "a ^ count M a dvd a^(count N a)"
7.119 by (elim coprime_dvd_mult_nat)
7.120 with a show ?thesis
7.121 - by (intro power_dvd_imp_le, auto)
7.122 + apply (intro power_dvd_imp_le)
7.123 + apply auto
7.124 + done
7.125 next
7.126 assume "a ~: set_of M"
7.127 - thus ?thesis by auto
7.128 + then show ?thesis by auto
7.129 qed
7.130
7.131 lemma multiset_prime_factorization_unique:
7.132 @@ -210,10 +204,11 @@
7.133 ultimately have "count M a = count N a"
7.134 by auto
7.135 }
7.136 - thus ?thesis by (simp add:multiset_eq_iff)
7.137 + then show ?thesis by (simp add:multiset_eq_iff)
7.138 qed
7.139
7.140 -definition multiset_prime_factorization :: "nat => nat multiset" where
7.141 +definition multiset_prime_factorization :: "nat => nat multiset"
7.142 +where
7.143 "multiset_prime_factorization n ==
7.144 if n > 0 then (THE M. ((ALL p : set_of M. prime p) &
7.145 n = (PROD i :# M. i)))
7.146 @@ -234,27 +229,21 @@
7.147 subsection {* Prime factors and multiplicity for nats and ints *}
7.148
7.149 class unique_factorization =
7.150 -
7.151 -fixes
7.152 - multiplicity :: "'a \<Rightarrow> 'a \<Rightarrow> nat" and
7.153 - prime_factors :: "'a \<Rightarrow> 'a set"
7.154 + fixes multiplicity :: "'a \<Rightarrow> 'a \<Rightarrow> nat"
7.155 + and prime_factors :: "'a \<Rightarrow> 'a set"
7.156
7.157 (* definitions for the natural numbers *)
7.158
7.159 instantiation nat :: unique_factorization
7.160 begin
7.161
7.162 -definition
7.163 - multiplicity_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
7.164 -where
7.165 - "multiplicity_nat p n = count (multiset_prime_factorization n) p"
7.166 +definition multiplicity_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
7.167 + where "multiplicity_nat p n = count (multiset_prime_factorization n) p"
7.168
7.169 -definition
7.170 - prime_factors_nat :: "nat \<Rightarrow> nat set"
7.171 -where
7.172 - "prime_factors_nat n = set_of (multiset_prime_factorization n)"
7.173 +definition prime_factors_nat :: "nat \<Rightarrow> nat set"
7.174 + where "prime_factors_nat n = set_of (multiset_prime_factorization n)"
7.175
7.176 -instance proof qed
7.177 +instance ..
7.178
7.179 end
7.180
7.181 @@ -263,34 +252,31 @@
7.182 instantiation int :: unique_factorization
7.183 begin
7.184
7.185 -definition
7.186 - multiplicity_int :: "int \<Rightarrow> int \<Rightarrow> nat"
7.187 -where
7.188 - "multiplicity_int p n = multiplicity (nat p) (nat n)"
7.189 +definition multiplicity_int :: "int \<Rightarrow> int \<Rightarrow> nat"
7.190 + where "multiplicity_int p n = multiplicity (nat p) (nat n)"
7.191
7.192 -definition
7.193 - prime_factors_int :: "int \<Rightarrow> int set"
7.194 -where
7.195 - "prime_factors_int n = int ` (prime_factors (nat n))"
7.196 +definition prime_factors_int :: "int \<Rightarrow> int set"
7.197 + where "prime_factors_int n = int ` (prime_factors (nat n))"
7.198
7.199 -instance proof qed
7.200 +instance ..
7.201
7.202 end
7.203
7.204
7.205 subsection {* Set up transfer *}
7.206
7.207 -lemma transfer_nat_int_prime_factors:
7.208 - "prime_factors (nat n) = nat ` prime_factors n"
7.209 - unfolding prime_factors_int_def apply auto
7.210 - by (subst transfer_int_nat_set_return_embed, assumption)
7.211 +lemma transfer_nat_int_prime_factors: "prime_factors (nat n) = nat ` prime_factors n"
7.212 + unfolding prime_factors_int_def
7.213 + apply auto
7.214 + apply (subst transfer_int_nat_set_return_embed)
7.215 + apply assumption
7.216 + done
7.217
7.218 -lemma transfer_nat_int_prime_factors_closure: "n >= 0 \<Longrightarrow>
7.219 - nat_set (prime_factors n)"
7.220 +lemma transfer_nat_int_prime_factors_closure: "n >= 0 \<Longrightarrow> nat_set (prime_factors n)"
7.221 by (auto simp add: nat_set_def prime_factors_int_def)
7.222
7.223 lemma transfer_nat_int_multiplicity: "p >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow>
7.224 - multiplicity (nat p) (nat n) = multiplicity p n"
7.225 + multiplicity (nat p) (nat n) = multiplicity p n"
7.226 by (auto simp add: multiplicity_int_def)
7.227
7.228 declare transfer_morphism_nat_int[transfer add return:
7.229 @@ -298,8 +284,7 @@
7.230 transfer_nat_int_multiplicity]
7.231
7.232
7.233 -lemma transfer_int_nat_prime_factors:
7.234 - "prime_factors (int n) = int ` prime_factors n"
7.235 +lemma transfer_int_nat_prime_factors: "prime_factors (int n) = int ` prime_factors n"
7.236 unfolding prime_factors_int_def by auto
7.237
7.238 lemma transfer_int_nat_prime_factors_closure: "is_nat n \<Longrightarrow>
7.239 @@ -318,10 +303,10 @@
7.240 subsection {* Properties of prime factors and multiplicity for nats and ints *}
7.241
7.242 lemma prime_factors_ge_0_int [elim]: "p : prime_factors (n::int) \<Longrightarrow> p >= 0"
7.243 - by (unfold prime_factors_int_def, auto)
7.244 + unfolding prime_factors_int_def by auto
7.245
7.246 lemma prime_factors_prime_nat [intro]: "p : prime_factors (n::nat) \<Longrightarrow> prime p"
7.247 - apply (case_tac "n = 0")
7.248 + apply (cases "n = 0")
7.249 apply (simp add: prime_factors_nat_def multiset_prime_factorization_def)
7.250 apply (auto simp add: prime_factors_nat_def multiset_prime_factorization)
7.251 done
7.252 @@ -334,17 +319,21 @@
7.253 done
7.254
7.255 lemma prime_factors_gt_0_nat [elim]: "p : prime_factors x \<Longrightarrow> p > (0::nat)"
7.256 - by (frule prime_factors_prime_nat, auto)
7.257 + apply (frule prime_factors_prime_nat)
7.258 + apply auto
7.259 + done
7.260
7.261 lemma prime_factors_gt_0_int [elim]: "x >= 0 \<Longrightarrow> p : prime_factors x \<Longrightarrow>
7.262 p > (0::int)"
7.263 - by (frule (1) prime_factors_prime_int, auto)
7.264 + apply (frule (1) prime_factors_prime_int)
7.265 + apply auto
7.266 + done
7.267
7.268 lemma prime_factors_finite_nat [iff]: "finite (prime_factors (n::nat))"
7.269 - by (unfold prime_factors_nat_def, auto)
7.270 + unfolding prime_factors_nat_def by auto
7.271
7.272 lemma prime_factors_finite_int [iff]: "finite (prime_factors (n::int))"
7.273 - by (unfold prime_factors_int_def, auto)
7.274 + unfolding prime_factors_int_def by auto
7.275
7.276 lemma prime_factors_altdef_nat: "prime_factors (n::nat) =
7.277 {p. multiplicity p n > 0}"
7.278 @@ -359,8 +348,9 @@
7.279
7.280 lemma prime_factorization_nat: "(n::nat) > 0 \<Longrightarrow>
7.281 n = (PROD p : prime_factors n. p^(multiplicity p n))"
7.282 - by (frule multiset_prime_factorization,
7.283 - simp add: prime_factors_nat_def multiplicity_nat_def msetprod_def)
7.284 + apply (frule multiset_prime_factorization)
7.285 + apply (simp add: prime_factors_nat_def multiplicity_nat_def msetprod_def)
7.286 + done
7.287
7.288 lemma prime_factorization_int:
7.289 assumes "(n::int) > 0"
7.290 @@ -376,8 +366,7 @@
7.291 "S = { (p::nat) . f p > 0} \<Longrightarrow> finite S \<Longrightarrow> (ALL p : S. prime p) \<Longrightarrow>
7.292 n = (PROD p : S. p^(f p)) \<Longrightarrow>
7.293 S = prime_factors n & (ALL p. f p = multiplicity p n)"
7.294 - apply (subgoal_tac "multiset_prime_factorization n = Abs_multiset
7.295 - f")
7.296 + apply (subgoal_tac "multiset_prime_factorization n = Abs_multiset f")
7.297 apply (unfold prime_factors_nat_def multiplicity_nat_def)
7.298 apply (simp add: set_of_def Abs_multiset_inverse multiset_def)
7.299 apply (unfold multiset_prime_factorization_def)
7.300 @@ -396,13 +385,14 @@
7.301 apply (subgoal_tac "f : multiset")
7.302 apply (auto simp only: Abs_multiset_inverse)
7.303 unfolding multiset_def apply force
7.304 -done
7.305 + done
7.306
7.307 lemma prime_factors_characterization_nat: "S = {p. 0 < f (p::nat)} \<Longrightarrow>
7.308 finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
7.309 prime_factors n = S"
7.310 - by (rule prime_factorization_unique_nat [THEN conjunct1, symmetric],
7.311 - assumption+)
7.312 + apply (rule prime_factorization_unique_nat [THEN conjunct1, symmetric])
7.313 + apply assumption+
7.314 + done
7.315
7.316 lemma prime_factors_characterization'_nat:
7.317 "finite {p. 0 < f (p::nat)} \<Longrightarrow>
7.318 @@ -410,7 +400,7 @@
7.319 prime_factors (PROD p | 0 < f p . p ^ f p) = {p. 0 < f p}"
7.320 apply (rule prime_factors_characterization_nat)
7.321 apply auto
7.322 -done
7.323 + done
7.324
7.325 (* A minor glitch:*)
7.326
7.327 @@ -433,7 +423,7 @@
7.328 [where f = "%x. f (int (x::nat))",
7.329 transferred direction: nat "op <= (0::int)"])
7.330 apply auto
7.331 -done
7.332 + done
7.333
7.334 lemma prime_factors_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow>
7.335 finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
7.336 @@ -444,32 +434,32 @@
7.337 apply (subst primes_characterization'_int)
7.338 apply auto
7.339 apply (auto simp add: prime_ge_0_int)
7.340 -done
7.341 + done
7.342
7.343 lemma multiplicity_characterization_nat: "S = {p. 0 < f (p::nat)} \<Longrightarrow>
7.344 finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
7.345 multiplicity p n = f p"
7.346 - by (frule prime_factorization_unique_nat [THEN conjunct2, rule_format,
7.347 - symmetric], auto)
7.348 + apply (frule prime_factorization_unique_nat [THEN conjunct2, rule_format, symmetric])
7.349 + apply auto
7.350 + done
7.351
7.352 lemma multiplicity_characterization'_nat: "finite {p. 0 < f (p::nat)} \<longrightarrow>
7.353 (ALL p. 0 < f p \<longrightarrow> prime p) \<longrightarrow>
7.354 multiplicity p (PROD p | 0 < f p . p ^ f p) = f p"
7.355 - apply (rule impI)+
7.356 + apply (intro impI)
7.357 apply (rule multiplicity_characterization_nat)
7.358 apply auto
7.359 -done
7.360 + done
7.361
7.362 lemma multiplicity_characterization'_int [rule_format]:
7.363 "finite {p. p >= 0 & 0 < f (p::int)} \<Longrightarrow>
7.364 (ALL p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> p >= 0 \<Longrightarrow>
7.365 multiplicity p (PROD p | p >= 0 & 0 < f p . p ^ f p) = f p"
7.366 -
7.367 apply (insert multiplicity_characterization'_nat
7.368 [where f = "%x. f (int (x::nat))",
7.369 transferred direction: nat "op <= (0::int)", rule_format])
7.370 apply auto
7.371 -done
7.372 + done
7.373
7.374 lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow>
7.375 finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
7.376 @@ -480,7 +470,7 @@
7.377 apply (subst multiplicity_characterization'_int)
7.378 apply auto
7.379 apply (auto simp add: prime_ge_0_int)
7.380 -done
7.381 + done
7.382
7.383 lemma multiplicity_zero_nat [simp]: "multiplicity (p::nat) 0 = 0"
7.384 by (simp add: multiplicity_nat_def multiset_prime_factorization_def)
7.385 @@ -495,51 +485,50 @@
7.386 by (simp add: multiplicity_int_def)
7.387
7.388 lemma multiplicity_prime_nat [simp]: "prime (p::nat) \<Longrightarrow> multiplicity p p = 1"
7.389 - apply (subst multiplicity_characterization_nat
7.390 - [where f = "(%q. if q = p then 1 else 0)"])
7.391 + apply (subst multiplicity_characterization_nat [where f = "(%q. if q = p then 1 else 0)"])
7.392 apply auto
7.393 apply (case_tac "x = p")
7.394 apply auto
7.395 -done
7.396 + done
7.397
7.398 lemma multiplicity_prime_int [simp]: "prime (p::int) \<Longrightarrow> multiplicity p p = 1"
7.399 unfolding prime_int_def multiplicity_int_def by auto
7.400
7.401 -lemma multiplicity_prime_power_nat [simp]: "prime (p::nat) \<Longrightarrow>
7.402 - multiplicity p (p^n) = n"
7.403 - apply (case_tac "n = 0")
7.404 +lemma multiplicity_prime_power_nat [simp]: "prime (p::nat) \<Longrightarrow> multiplicity p (p^n) = n"
7.405 + apply (cases "n = 0")
7.406 apply auto
7.407 - apply (subst multiplicity_characterization_nat
7.408 - [where f = "(%q. if q = p then n else 0)"])
7.409 + apply (subst multiplicity_characterization_nat [where f = "(%q. if q = p then n else 0)"])
7.410 apply auto
7.411 apply (case_tac "x = p")
7.412 apply auto
7.413 -done
7.414 + done
7.415
7.416 -lemma multiplicity_prime_power_int [simp]: "prime (p::int) \<Longrightarrow>
7.417 - multiplicity p (p^n) = n"
7.418 +lemma multiplicity_prime_power_int [simp]: "prime (p::int) \<Longrightarrow> multiplicity p (p^n) = n"
7.419 apply (frule prime_ge_0_int)
7.420 apply (auto simp add: prime_int_def multiplicity_int_def nat_power_eq)
7.421 -done
7.422 + done
7.423
7.424 -lemma multiplicity_nonprime_nat [simp]: "~ prime (p::nat) \<Longrightarrow>
7.425 - multiplicity p n = 0"
7.426 - apply (case_tac "n = 0")
7.427 +lemma multiplicity_nonprime_nat [simp]: "~ prime (p::nat) \<Longrightarrow> multiplicity p n = 0"
7.428 + apply (cases "n = 0")
7.429 apply auto
7.430 apply (frule multiset_prime_factorization)
7.431 apply (auto simp add: set_of_def multiplicity_nat_def)
7.432 -done
7.433 + done
7.434
7.435 lemma multiplicity_nonprime_int [simp]: "~ prime (p::int) \<Longrightarrow> multiplicity p n = 0"
7.436 - by (unfold multiplicity_int_def prime_int_def, auto)
7.437 + unfolding multiplicity_int_def prime_int_def by auto
7.438
7.439 lemma multiplicity_not_factor_nat [simp]:
7.440 "p ~: prime_factors (n::nat) \<Longrightarrow> multiplicity p n = 0"
7.441 - by (subst (asm) prime_factors_altdef_nat, auto)
7.442 + apply (subst (asm) prime_factors_altdef_nat)
7.443 + apply auto
7.444 + done
7.445
7.446 lemma multiplicity_not_factor_int [simp]:
7.447 "p >= 0 \<Longrightarrow> p ~: prime_factors (n::int) \<Longrightarrow> multiplicity p n = 0"
7.448 - by (subst (asm) prime_factors_altdef_int, auto)
7.449 + apply (subst (asm) prime_factors_altdef_int)
7.450 + apply auto
7.451 + done
7.452
7.453 lemma multiplicity_product_aux_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow>
7.454 (prime_factors k) Un (prime_factors l) = prime_factors (k * l) &
7.455 @@ -572,7 +561,7 @@
7.456 apply (simp add: setprod_1)
7.457 apply (erule prime_factorization_nat)
7.458 apply (rule setprod_cong, auto)
7.459 -done
7.460 + done
7.461
7.462 (* transfer doesn't have the same problem here with the right
7.463 choice of rules. *)
7.464 @@ -611,7 +600,7 @@
7.465 apply auto
7.466 apply (subst multiplicity_product_nat)
7.467 apply auto
7.468 -done
7.469 + done
7.470
7.471 (* Transfer is delicate here for two reasons: first, because there is
7.472 an implicit quantifier over functions (f), and, second, because the
7.473 @@ -627,7 +616,7 @@
7.474 "(PROD x : A. int (f x)) >= 0"
7.475 apply (rule setsum_nonneg, auto)
7.476 apply (rule setprod_nonneg, auto)
7.477 -done
7.478 + done
7.479
7.480 declare transfer_morphism_nat_int[transfer
7.481 add return: transfer_nat_int_sum_prod_closure3
7.482 @@ -648,7 +637,7 @@
7.483 apply auto
7.484 apply (rule setsum_cong)
7.485 apply auto
7.486 -done
7.487 + done
7.488
7.489 declare transfer_morphism_nat_int[transfer
7.490 add return: transfer_nat_int_sum_prod2 (1)]
7.491 @@ -676,7 +665,6 @@
7.492 lemma multiplicity_prod_prime_powers_int:
7.493 "(p::int) >= 0 \<Longrightarrow> finite S \<Longrightarrow> (ALL p : S. prime p) \<Longrightarrow>
7.494 multiplicity p (PROD p : S. p ^ f p) = (if p : S then f p else 0)"
7.495 -
7.496 apply (subgoal_tac "int ` nat ` S = S")
7.497 apply (frule multiplicity_prod_prime_powers_nat [where f = "%x. f(int x)"
7.498 and S = "nat ` S", transferred])
7.499 @@ -684,7 +672,7 @@
7.500 apply (metis prime_int_def)
7.501 apply (metis prime_ge_0_int)
7.502 apply (metis nat_set_def prime_ge_0_int transfer_nat_int_set_return_embed)
7.503 -done
7.504 + done
7.505
7.506 lemma multiplicity_distinct_prime_power_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow>
7.507 p ~= q \<Longrightarrow> multiplicity p (q^n) = 0"
7.508 @@ -692,7 +680,7 @@
7.509 apply (erule ssubst)
7.510 apply (subst multiplicity_prod_prime_powers_nat)
7.511 apply auto
7.512 -done
7.513 + done
7.514
7.515 lemma multiplicity_distinct_prime_power_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow>
7.516 p ~= q \<Longrightarrow> multiplicity p (q^n) = 0"
7.517 @@ -701,41 +689,40 @@
7.518 prefer 4
7.519 apply assumption
7.520 apply auto
7.521 -done
7.522 + done
7.523
7.524 -lemma dvd_multiplicity_nat:
7.525 +lemma dvd_multiplicity_nat:
7.526 "(0::nat) < y \<Longrightarrow> x dvd y \<Longrightarrow> multiplicity p x <= multiplicity p y"
7.527 - apply (case_tac "x = 0")
7.528 + apply (cases "x = 0")
7.529 apply (auto simp add: dvd_def multiplicity_product_nat)
7.530 -done
7.531 + done
7.532
7.533 lemma dvd_multiplicity_int:
7.534 "(0::int) < y \<Longrightarrow> 0 <= x \<Longrightarrow> x dvd y \<Longrightarrow> p >= 0 \<Longrightarrow>
7.535 multiplicity p x <= multiplicity p y"
7.536 - apply (case_tac "x = 0")
7.537 + apply (cases "x = 0")
7.538 apply (auto simp add: dvd_def)
7.539 apply (subgoal_tac "0 < k")
7.540 apply (auto simp add: multiplicity_product_int)
7.541 apply (erule zero_less_mult_pos)
7.542 apply arith
7.543 -done
7.544 + done
7.545
7.546 lemma dvd_prime_factors_nat [intro]:
7.547 "0 < (y::nat) \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x <= prime_factors y"
7.548 apply (simp only: prime_factors_altdef_nat)
7.549 apply auto
7.550 apply (metis dvd_multiplicity_nat le_0_eq neq_zero_eq_gt_zero_nat)
7.551 -done
7.552 + done
7.553
7.554 lemma dvd_prime_factors_int [intro]:
7.555 "0 < (y::int) \<Longrightarrow> 0 <= x \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x <= prime_factors y"
7.556 apply (auto simp add: prime_factors_altdef_int)
7.557 apply (metis dvd_multiplicity_int le_0_eq neq_zero_eq_gt_zero_nat)
7.558 -done
7.559 + done
7.560
7.561 lemma multiplicity_dvd_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow>
7.562 - ALL p. multiplicity p x <= multiplicity p y \<Longrightarrow>
7.563 - x dvd y"
7.564 + ALL p. multiplicity p x <= multiplicity p y \<Longrightarrow> x dvd y"
7.565 apply (subst prime_factorization_nat [of x], assumption)
7.566 apply (subst prime_factorization_nat [of y], assumption)
7.567 apply (rule setprod_dvd_setprod_subset2)
7.568 @@ -744,11 +731,10 @@
7.569 apply auto
7.570 apply (metis gr0I le_0_eq less_not_refl)
7.571 apply (metis le_imp_power_dvd)
7.572 -done
7.573 + done
7.574
7.575 lemma multiplicity_dvd_int: "0 < (x::int) \<Longrightarrow> 0 < y \<Longrightarrow>
7.576 - ALL p >= 0. multiplicity p x <= multiplicity p y \<Longrightarrow>
7.577 - x dvd y"
7.578 + ALL p >= 0. multiplicity p x <= multiplicity p y \<Longrightarrow> x dvd y"
7.579 apply (subst prime_factorization_int [of x], assumption)
7.580 apply (subst prime_factorization_int [of y], assumption)
7.581 apply (rule setprod_dvd_setprod_subset2)
7.582 @@ -756,17 +742,18 @@
7.583 apply (subst prime_factors_altdef_int)+
7.584 apply auto
7.585 apply (metis le_imp_power_dvd prime_factors_ge_0_int)
7.586 -done
7.587 + done
7.588
7.589 lemma multiplicity_dvd'_nat: "(0::nat) < x \<Longrightarrow>
7.590 \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
7.591 -by (metis gcd_lcm_complete_lattice_nat.top_greatest le_refl multiplicity_dvd_nat
7.592 - multiplicity_nonprime_nat neq0_conv)
7.593 + by (metis gcd_lcm_complete_lattice_nat.top_greatest le_refl multiplicity_dvd_nat
7.594 + multiplicity_nonprime_nat neq0_conv)
7.595
7.596 lemma multiplicity_dvd'_int: "(0::int) < x \<Longrightarrow> 0 <= y \<Longrightarrow>
7.597 \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
7.598 -by (metis eq_imp_le gcd_lcm_complete_lattice_nat.top_greatest int_eq_0_conv multiplicity_dvd_int
7.599 - multiplicity_nonprime_int nat_int transfer_nat_int_relations(4) less_le)
7.600 + by (metis eq_imp_le gcd_lcm_complete_lattice_nat.top_greatest int_eq_0_conv
7.601 + multiplicity_dvd_int multiplicity_nonprime_int nat_int transfer_nat_int_relations(4)
7.602 + less_le)
7.603
7.604 lemma dvd_multiplicity_eq_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow>
7.605 (x dvd y) = (ALL p. multiplicity p x <= multiplicity p y)"
7.606 @@ -778,7 +765,7 @@
7.607
7.608 lemma prime_factors_altdef2_nat: "(n::nat) > 0 \<Longrightarrow>
7.609 (p : prime_factors n) = (prime p & p dvd n)"
7.610 - apply (case_tac "prime p")
7.611 + apply (cases "prime p")
7.612 apply auto
7.613 apply (subst prime_factorization_nat [where n = n], assumption)
7.614 apply (rule dvd_trans)
7.615 @@ -787,13 +774,12 @@
7.616 apply (rule dvd_setprod)
7.617 apply auto
7.618 apply (metis One_nat_def Zero_not_Suc dvd_multiplicity_nat le0 le_antisym multiplicity_not_factor_nat multiplicity_prime_nat)
7.619 -done
7.620 + done
7.621
7.622 lemma prime_factors_altdef2_int:
7.623 assumes "(n::int) > 0"
7.624 shows "(p : prime_factors n) = (prime p & p dvd n)"
7.625 -
7.626 - apply (case_tac "p >= 0")
7.627 + apply (cases "p >= 0")
7.628 apply (rule prime_factors_altdef2_nat [transferred])
7.629 using assms apply auto
7.630 apply (auto simp add: prime_ge_0_int prime_factors_ge_0_int)
7.631 @@ -804,20 +790,18 @@
7.632 assumes [arith]: "x > 0" "y > 0" and
7.633 mult_eq [simp]: "!!p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
7.634 shows "x = y"
7.635 -
7.636 apply (rule dvd_antisym)
7.637 apply (auto intro: multiplicity_dvd'_nat)
7.638 -done
7.639 + done
7.640
7.641 lemma multiplicity_eq_int:
7.642 fixes x and y::int
7.643 assumes [arith]: "x > 0" "y > 0" and
7.644 mult_eq [simp]: "!!p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
7.645 shows "x = y"
7.646 -
7.647 apply (rule dvd_antisym [transferred])
7.648 apply (auto intro: multiplicity_dvd'_int)
7.649 -done
7.650 + done
7.651
7.652
7.653 subsection {* An application *}
7.654 @@ -850,7 +834,7 @@
7.655 done
7.656 ultimately have "z = gcd x y"
7.657 by (subst gcd_unique_nat [symmetric], blast)
7.658 - thus ?thesis
7.659 + then show ?thesis
7.660 unfolding z_def by auto
7.661 qed
7.662
7.663 @@ -882,39 +866,34 @@
7.664 done
7.665 ultimately have "z = lcm x y"
7.666 by (subst lcm_unique_nat [symmetric], blast)
7.667 - thus ?thesis
7.668 + then show ?thesis
7.669 unfolding z_def by auto
7.670 qed
7.671
7.672 lemma multiplicity_gcd_nat:
7.673 assumes [arith]: "x > 0" "y > 0"
7.674 - shows "multiplicity (p::nat) (gcd x y) =
7.675 - min (multiplicity p x) (multiplicity p y)"
7.676 -
7.677 + shows "multiplicity (p::nat) (gcd x y) = min (multiplicity p x) (multiplicity p y)"
7.678 apply (subst gcd_eq_nat)
7.679 apply auto
7.680 apply (subst multiplicity_prod_prime_powers_nat)
7.681 apply auto
7.682 -done
7.683 + done
7.684
7.685 lemma multiplicity_lcm_nat:
7.686 assumes [arith]: "x > 0" "y > 0"
7.687 - shows "multiplicity (p::nat) (lcm x y) =
7.688 - max (multiplicity p x) (multiplicity p y)"
7.689 -
7.690 + shows "multiplicity (p::nat) (lcm x y) = max (multiplicity p x) (multiplicity p y)"
7.691 apply (subst lcm_eq_nat)
7.692 apply auto
7.693 apply (subst multiplicity_prod_prime_powers_nat)
7.694 apply auto
7.695 -done
7.696 + done
7.697
7.698 lemma gcd_lcm_distrib_nat: "gcd (x::nat) (lcm y z) = lcm (gcd x y) (gcd x z)"
7.699 - apply (case_tac "x = 0 | y = 0 | z = 0")
7.700 + apply (cases "x = 0 | y = 0 | z = 0")
7.701 apply auto
7.702 apply (rule multiplicity_eq_nat)
7.703 - apply (auto simp add: multiplicity_gcd_nat multiplicity_lcm_nat
7.704 - lcm_pos_nat)
7.705 -done
7.706 + apply (auto simp add: multiplicity_gcd_nat multiplicity_lcm_nat lcm_pos_nat)
7.707 + done
7.708
7.709 lemma gcd_lcm_distrib_int: "gcd (x::int) (lcm y z) = lcm (gcd x y) (gcd x z)"
7.710 apply (subst (1 2 3) gcd_abs_int)
7.711 @@ -923,6 +902,6 @@
7.712 apply force
7.713 apply (rule gcd_lcm_distrib_nat [transferred])
7.714 apply auto
7.715 -done
7.716 + done
7.717
7.718 end