author wenzelm Sat Sep 10 23:27:32 2011 +0200 (2011-09-10) changeset 44872 a98ef45122f3 parent 44871 fbfdc5ac86be child 44874 cd60c421b029
misc tuning;
 src/HOL/Number_Theory/Binomial.thy file | annotate | diff | revisions src/HOL/Number_Theory/Cong.thy file | annotate | diff | revisions src/HOL/Number_Theory/Fib.thy file | annotate | diff | revisions src/HOL/Number_Theory/MiscAlgebra.thy file | annotate | diff | revisions src/HOL/Number_Theory/Primes.thy file | annotate | diff | revisions src/HOL/Number_Theory/Residues.thy file | annotate | diff | revisions src/HOL/Number_Theory/UniqueFactorization.thy file | annotate | diff | revisions
```     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.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.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.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.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 -
2.85 -begin
2.86 +begin
2.87
2.88 -definition
2.89 -  cong_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
2.90 -where
2.91 -  "cong_nat x y m = ((x mod m) = (y mod m))"
2.92 +definition cong_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
2.93 +  where "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 -
2.105 -begin
2.106 +begin
2.107
2.108 -definition
2.109 -  cong_int :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool"
2.110 -where
2.111 -  "cong_int x y m = ((x mod m) = (y mod m))"
2.112 +definition cong_int :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool"
2.113 +  where "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.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.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.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.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 -
2.261 -lemma cong_exp_nat: "[(x::nat) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
2.262 -  apply (induct k)
2.263 -  apply (auto simp add: cong_mult_nat)
2.264 -  done
2.265 -
2.266 -lemma cong_exp_int: "[(x::int) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
2.267 -  apply (induct k)
2.268 -  apply (auto simp add: cong_mult_int)
2.269    done
2.270
2.271 -lemma cong_setsum_nat [rule_format]:
2.272 -    "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
2.273 +lemma cong_exp_nat: "[(x::nat) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
2.274 +  by (induct k) (auto simp add: cong_mult_nat)
2.275 +
2.276 +lemma cong_exp_int: "[(x::int) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
2.277 +  by (induct k) (auto simp add: cong_mult_int)
2.278 +
2.279 +lemma cong_setsum_nat [rule_format]:
2.280 +    "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
2.281        [(SUM x:A. f x) = (SUM x:A. g x)] (mod m)"
2.282 -  apply (case_tac "finite A")
2.283 +  apply (cases "finite A")
2.284    apply (induct set: finite)
2.286 -done
2.287 +  done
2.288
2.289  lemma cong_setsum_int [rule_format]:
2.290 -    "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
2.291 +    "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
2.292        [(SUM x:A. f x) = (SUM x:A. g x)] (mod m)"
2.293 -  apply (case_tac "finite A")
2.294 +  apply (cases "finite A")
2.295    apply (induct set: finite)
2.297 -done
2.298 +  done
2.299
2.300 -lemma cong_setprod_nat [rule_format]:
2.301 -    "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
2.302 +lemma cong_setprod_nat [rule_format]:
2.303 +    "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
2.304        [(PROD x:A. f x) = (PROD x:A. g x)] (mod m)"
2.305 -  apply (case_tac "finite A")
2.306 +  apply (cases "finite A")
2.307    apply (induct set: finite)
2.308    apply (auto intro: cong_mult_nat)
2.309 -done
2.310 +  done
2.311
2.312 -lemma cong_setprod_int [rule_format]:
2.313 -    "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
2.314 +lemma cong_setprod_int [rule_format]:
2.315 +    "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
2.316        [(PROD x:A. f x) = (PROD x:A. g x)] (mod m)"
2.317 -  apply (case_tac "finite A")
2.318 +  apply (cases "finite A")
2.319    apply (induct set: finite)
2.320    apply (auto intro: cong_mult_int)
2.321 -done
2.322 +  done
2.323
2.324  lemma cong_scalar_nat: "[(a::nat)= b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)"
2.325 -  by (rule cong_mult_nat, simp_all)
2.326 +  by (rule cong_mult_nat) simp_all
2.327
2.328  lemma cong_scalar_int: "[(a::int)= b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)"
2.329 -  by (rule cong_mult_int, simp_all)
2.330 +  by (rule cong_mult_int) simp_all
2.331
2.332  lemma cong_scalar2_nat: "[(a::nat)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)"
2.333 -  by (rule cong_mult_nat, simp_all)
2.334 +  by (rule cong_mult_nat) simp_all
2.335
2.336  lemma cong_scalar2_int: "[(a::int)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)"
2.337 -  by (rule cong_mult_int, simp_all)
2.338 +  by (rule cong_mult_int) simp_all
2.339
2.340  lemma cong_mult_self_nat: "[(a::nat) * m = 0] (mod m)"
2.341 -  by (unfold cong_nat_def, auto)
2.342 +  unfolding cong_nat_def by auto
2.343
2.344  lemma cong_mult_self_int: "[(a::int) * m = 0] (mod m)"
2.345 -  by (unfold cong_int_def, auto)
2.346 +  unfolding cong_int_def by auto
2.347
2.348  lemma cong_eq_diff_cong_0_int: "[(a::int) = b] (mod m) = [a - b = 0] (mod m)"
2.349    apply (rule iffI)
2.350    apply (erule cong_diff_int [of a b m b b, simplified])
2.351    apply (erule cong_add_int [of "a - b" 0 m b b, simplified])
2.352 -done
2.353 +  done
2.354
2.355  lemma cong_eq_diff_cong_0_aux_int: "a >= b \<Longrightarrow>
2.356      [(a::int) = b] (mod m) = [tsub a b = 0] (mod m)"
2.357 @@ -307,29 +291,29 @@
2.358    shows "[a = b] (mod m) = [a - b = 0] (mod m)"
2.359    using assms by (rule cong_eq_diff_cong_0_aux_int [transferred])
2.360
2.361 -lemma cong_diff_cong_0'_nat:
2.362 -  "[(x::nat) = y] (mod n) \<longleftrightarrow>
2.363 +lemma cong_diff_cong_0'_nat:
2.364 +  "[(x::nat) = y] (mod n) \<longleftrightarrow>
2.365      (if x <= y then [y - x = 0] (mod n) else [x - y = 0] (mod n))"
2.366 -  apply (case_tac "y <= x")
2.367 +  apply (cases "y <= x")
2.368    apply (frule cong_eq_diff_cong_0_nat [where m = n])
2.369    apply auto [1]
2.370    apply (subgoal_tac "x <= y")
2.371    apply (frule cong_eq_diff_cong_0_nat [where m = n])
2.372    apply (subst cong_sym_eq_nat)
2.373    apply auto
2.374 -done
2.375 +  done
2.376
2.377  lemma cong_altdef_nat: "(a::nat) >= b \<Longrightarrow> [a = b] (mod m) = (m dvd (a - b))"
2.378    apply (subst cong_eq_diff_cong_0_nat, assumption)
2.379    apply (unfold cong_nat_def)
2.380    apply (simp add: dvd_eq_mod_eq_0 [symmetric])
2.381 -done
2.382 +  done
2.383
2.384  lemma cong_altdef_int: "[(a::int) = b] (mod m) = (m dvd (a - b))"
2.385    apply (subst cong_eq_diff_cong_0_int)
2.386    apply (unfold cong_int_def)
2.387    apply (simp add: dvd_eq_mod_eq_0 [symmetric])
2.388 -done
2.389 +  done
2.390
2.391  lemma cong_abs_int: "[(x::int) = y] (mod abs m) = [x = y] (mod m)"
2.393 @@ -342,29 +326,29 @@
2.394    (* any way around this? *)
2.395    apply (subgoal_tac "a * a - 1 = (a - 1) * (a - -1)")
2.396    apply (auto simp add: field_simps)
2.397 -done
2.398 +  done
2.399
2.400  lemma cong_mult_rcancel_int:
2.401 -  "coprime k (m::int) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
2.402 +    "coprime k (m::int) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
2.403    apply (subst (1 2) cong_altdef_int)
2.404    apply (subst left_diff_distrib [symmetric])
2.405    apply (rule coprime_dvd_mult_iff_int)
2.406    apply (subst gcd_commute_int, assumption)
2.407 -done
2.408 +  done
2.409
2.410  lemma cong_mult_rcancel_nat:
2.411    assumes  "coprime k (m::nat)"
2.412    shows "[a * k = b * k] (mod m) = [a = b] (mod m)"
2.413    apply (rule cong_mult_rcancel_int [transferred])
2.414    using assms apply auto
2.415 -done
2.416 +  done
2.417
2.418  lemma cong_mult_lcancel_nat:
2.419 -  "coprime k (m::nat) \<Longrightarrow> [k * a = k * b ] (mod m) = [a = b] (mod m)"
2.420 +    "coprime k (m::nat) \<Longrightarrow> [k * a = k * b ] (mod m) = [a = b] (mod m)"
2.421    by (simp add: mult_commute cong_mult_rcancel_nat)
2.422
2.423  lemma cong_mult_lcancel_int:
2.424 -  "coprime k (m::int) \<Longrightarrow> [k * a = k * b] (mod m) = [a = b] (mod m)"
2.425 +    "coprime k (m::int) \<Longrightarrow> [k * a = k * b] (mod m) = [a = b] (mod m)"
2.426    by (simp add: mult_commute cong_mult_rcancel_int)
2.427
2.428  (* was zcong_zgcd_zmult_zmod *)
2.429 @@ -395,7 +379,7 @@
2.430    apply auto
2.431    apply (rule_tac x = "a mod m" in exI)
2.432    apply (unfold cong_nat_def, auto)
2.433 -done
2.434 +  done
2.435
2.436  lemma cong_less_unique_int:
2.437      "0 < (m::int) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
2.438 @@ -407,12 +391,12 @@
2.439  lemma cong_iff_lin_int: "([(a::int) = b] (mod m)) = (\<exists>k. b = a + m * k)"
2.440    apply (auto simp add: cong_altdef_int dvd_def field_simps)
2.441    apply (rule_tac [!] x = "-k" in exI, auto)
2.442 -done
2.443 +  done
2.444
2.445 -lemma cong_iff_lin_nat: "([(a::nat) = b] (mod m)) =
2.446 +lemma cong_iff_lin_nat: "([(a::nat) = b] (mod m)) =
2.447      (\<exists>k1 k2. b + k1 * m = a + k2 * m)"
2.448    apply (rule iffI)
2.449 -  apply (case_tac "b <= a")
2.450 +  apply (cases "b <= a")
2.451    apply (subst (asm) cong_altdef_nat, assumption)
2.452    apply (unfold dvd_def, auto)
2.453    apply (rule_tac x = k in exI)
2.454 @@ -430,42 +414,40 @@
2.455    apply (erule ssubst)back
2.456    apply (erule subst)
2.457    apply auto
2.458 -done
2.459 +  done
2.460
2.461  lemma cong_gcd_eq_int: "[(a::int) = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
2.462    apply (subst (asm) cong_iff_lin_int, auto)
2.465    apply (subst (2) gcd_commute_int)
2.466    apply (subst mult_commute)
2.468    apply (rule gcd_commute_int)
2.469    done
2.470
2.471 -lemma cong_gcd_eq_nat:
2.472 +lemma cong_gcd_eq_nat:
2.473    assumes "[(a::nat) = b] (mod m)"
2.474    shows "gcd a m = gcd b m"
2.475    apply (rule cong_gcd_eq_int [transferred])
2.476    using assms apply auto
2.477    done
2.478
2.479 -lemma cong_imp_coprime_nat: "[(a::nat) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow>
2.480 -    coprime b m"
2.481 +lemma cong_imp_coprime_nat: "[(a::nat) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
2.482    by (auto simp add: cong_gcd_eq_nat)
2.483
2.484 -lemma cong_imp_coprime_int: "[(a::int) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow>
2.485 -    coprime b m"
2.486 +lemma cong_imp_coprime_int: "[(a::int) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
2.487    by (auto simp add: cong_gcd_eq_int)
2.488
2.489 -lemma cong_cong_mod_nat: "[(a::nat) = b] (mod m) =
2.490 -    [a mod m = b mod m] (mod m)"
2.491 +lemma cong_cong_mod_nat: "[(a::nat) = b] (mod m) = [a mod m = b mod m] (mod m)"
2.492    by (auto simp add: cong_nat_def)
2.493
2.494 -lemma cong_cong_mod_int: "[(a::int) = b] (mod m) =
2.495 -    [a mod m = b mod m] (mod m)"
2.496 +lemma cong_cong_mod_int: "[(a::int) = b] (mod m) = [a mod m = b mod m] (mod m)"
2.497    by (auto simp add: cong_int_def)
2.498
2.499  lemma cong_minus_int [iff]: "[(a::int) = b] (mod -m) = [a = b] (mod m)"
2.500 -  by (subst (1 2) cong_altdef_int, auto)
2.501 +  apply (subst (1 2) cong_altdef_int)
2.502 +  apply auto
2.503 +  done
2.504
2.505  lemma cong_zero_nat: "[(a::nat) = b] (mod 0) = (a = b)"
2.506    by auto
2.507 @@ -479,7 +461,7 @@
2.508    apply (unfold dvd_def, auto)
2.509    apply (rule mod_mod_cancel)
2.510    apply auto
2.511 -done
2.512 +  done
2.513
2.514  lemma mod_dvd_mod:
2.515    assumes "0 < (m::nat)" and "m dvd b"
2.516 @@ -490,12 +472,12 @@
2.517    done
2.518  *)
2.519
2.521 -    "[(a::nat) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
2.523 +    "[(a::nat) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
2.525
2.527 -    "[(a::int) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
2.529 +    "[(a::int) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
2.531
2.532  lemma cong_add_rcancel_nat: "[(x::nat) + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
2.533 @@ -504,43 +486,42 @@
2.534  lemma cong_add_rcancel_int: "[(x::int) + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
2.536
2.537 -lemma cong_add_lcancel_0_nat: "[(a::nat) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
2.538 +lemma cong_add_lcancel_0_nat: "[(a::nat) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
2.540
2.541 -lemma cong_add_lcancel_0_int: "[(a::int) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
2.542 +lemma cong_add_lcancel_0_int: "[(a::int) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
2.544
2.545 -lemma cong_add_rcancel_0_nat: "[x + (a::nat) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
2.546 +lemma cong_add_rcancel_0_nat: "[x + (a::nat) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
2.548
2.549 -lemma cong_add_rcancel_0_int: "[x + (a::int) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
2.550 +lemma cong_add_rcancel_0_int: "[x + (a::int) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
2.552
2.553 -lemma cong_dvd_modulus_nat: "[(x::nat) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow>
2.554 +lemma cong_dvd_modulus_nat: "[(x::nat) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow>
2.555      [x = y] (mod n)"
2.556    apply (auto simp add: cong_iff_lin_nat dvd_def)
2.557    apply (rule_tac x="k1 * k" in exI)
2.558    apply (rule_tac x="k2 * k" in exI)
2.560 -done
2.561 +  done
2.562
2.563 -lemma cong_dvd_modulus_int: "[(x::int) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow>
2.564 -    [x = y] (mod n)"
2.565 +lemma cong_dvd_modulus_int: "[(x::int) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> [x = y] (mod n)"
2.566    by (auto simp add: cong_altdef_int dvd_def)
2.567
2.568  lemma cong_dvd_eq_nat: "[(x::nat) = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y"
2.569 -  by (unfold cong_nat_def, auto simp add: dvd_eq_mod_eq_0)
2.570 +  unfolding cong_nat_def by (auto simp add: dvd_eq_mod_eq_0)
2.571
2.572  lemma cong_dvd_eq_int: "[(x::int) = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y"
2.573 -  by (unfold cong_int_def, auto simp add: dvd_eq_mod_eq_0)
2.574 +  unfolding cong_int_def by (auto simp add: dvd_eq_mod_eq_0)
2.575
2.576 -lemma cong_mod_nat: "(n::nat) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)"
2.577 +lemma cong_mod_nat: "(n::nat) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)"
2.579
2.580 -lemma cong_mod_int: "(n::int) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)"
2.581 +lemma cong_mod_int: "(n::int) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)"
2.583
2.584 -lemma mod_mult_cong_nat: "(a::nat) ~= 0 \<Longrightarrow> b ~= 0
2.585 +lemma mod_mult_cong_nat: "(a::nat) ~= 0 \<Longrightarrow> b ~= 0
2.586      \<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)"
2.588
2.589 @@ -548,43 +529,43 @@
2.591    apply (subst dvd_minus_iff [symmetric])
2.593 -done
2.594 +  done
2.595
2.596  lemma cong_modulus_neg_int: "([(a::int) = b] (mod m)) = ([a = b] (mod -m))"
2.597    by (auto simp add: cong_altdef_int)
2.598
2.599 -lemma mod_mult_cong_int: "(a::int) ~= 0 \<Longrightarrow> b ~= 0
2.600 +lemma mod_mult_cong_int: "(a::int) ~= 0 \<Longrightarrow> b ~= 0
2.601      \<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)"
2.602 -  apply (case_tac "b > 0")
2.603 +  apply (cases "b > 0")
2.605    apply (subst (1 2) cong_modulus_neg_int)
2.606    apply (unfold cong_int_def)
2.607    apply (subgoal_tac "a * b = (-a * -b)")
2.608    apply (erule ssubst)
2.609    apply (subst zmod_zmult2_eq)
2.611 -done
2.613 +  done
2.614
2.615  lemma cong_to_1_nat: "([(a::nat) = 1] (mod n)) \<Longrightarrow> (n dvd (a - 1))"
2.616 -  apply (case_tac "a = 0")
2.617 +  apply (cases "a = 0")
2.618    apply force
2.619    apply (subst (asm) cong_altdef_nat)
2.620    apply auto
2.621 -done
2.622 +  done
2.623
2.624  lemma cong_0_1_nat: "[(0::nat) = 1] (mod n) = (n = 1)"
2.625 -  by (unfold cong_nat_def, auto)
2.626 +  unfolding cong_nat_def by auto
2.627
2.628  lemma cong_0_1_int: "[(0::int) = 1] (mod n) = ((n = 1) | (n = -1))"
2.629 -  by (unfold cong_int_def, auto simp add: zmult_eq_1_iff)
2.630 +  unfolding cong_int_def by (auto simp add: zmult_eq_1_iff)
2.631
2.632 -lemma cong_to_1'_nat: "[(a::nat) = 1] (mod n) \<longleftrightarrow>
2.633 +lemma cong_to_1'_nat: "[(a::nat) = 1] (mod n) \<longleftrightarrow>
2.634      a = 0 \<and> n = 1 \<or> (\<exists>m. a = 1 + m * n)"
2.635 -  apply (case_tac "n = 1")
2.636 +  apply (cases "n = 1")
2.637    apply auto [1]
2.638    apply (drule_tac x = "a - 1" in spec)
2.639    apply force
2.640 -  apply (case_tac "a = 0")
2.641 +  apply (cases "a = 0")
2.642    apply (auto simp add: cong_0_1_nat) [1]
2.643    apply (rule iffI)
2.644    apply (drule cong_to_1_nat)
2.645 @@ -594,7 +575,7 @@
2.646    apply (auto simp add: field_simps) [1]
2.647    apply (subst cong_altdef_nat)
2.648    apply (auto simp add: dvd_def)
2.649 -done
2.650 +  done
2.651
2.652  lemma cong_le_nat: "(y::nat) <= x \<Longrightarrow> [x = y] (mod n) \<longleftrightarrow> (\<exists>q. x = q * n + y)"
2.653    apply (subst cong_altdef_nat)
2.654 @@ -602,10 +583,10 @@
2.655    apply (unfold dvd_def, auto simp add: field_simps)
2.656    apply (rule_tac x = k in exI)
2.657    apply auto
2.658 -done
2.659 +  done
2.660
2.661  lemma cong_solve_nat: "(a::nat) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)"
2.662 -  apply (case_tac "n = 0")
2.663 +  apply (cases "n = 0")
2.664    apply force
2.665    apply (frule bezout_nat [of a n], auto)
2.666    apply (rule exI, erule ssubst)
2.667 @@ -617,11 +598,11 @@
2.668    apply simp
2.669    apply (rule cong_refl_nat)
2.670    apply (rule cong_refl_nat)
2.671 -done
2.672 +  done
2.673
2.674  lemma cong_solve_int: "(a::int) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)"
2.675 -  apply (case_tac "n = 0")
2.676 -  apply (case_tac "a \<ge> 0")
2.677 +  apply (cases "n = 0")
2.678 +  apply (cases "a \<ge> 0")
2.679    apply auto
2.680    apply (rule_tac x = "-1" in exI)
2.681    apply auto
2.682 @@ -637,16 +618,15 @@
2.683    apply simp
2.684    apply (subst mult_commute)
2.685    apply (rule cong_refl_int)
2.686 -done
2.687 -
2.688 -lemma cong_solve_dvd_nat:
2.689 +  done
2.690 +
2.691 +lemma cong_solve_dvd_nat:
2.692    assumes a: "(a::nat) \<noteq> 0" and b: "gcd a n dvd d"
2.693    shows "EX x. [a * x = d] (mod n)"
2.694  proof -
2.695 -  from cong_solve_nat [OF a] obtain x where
2.696 -      "[a * x = gcd a n](mod n)"
2.697 +  from cong_solve_nat [OF a] obtain x where "[a * x = gcd a n](mod n)"
2.698      by auto
2.699 -  hence "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)"
2.700 +  then have "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)"
2.701      by (elim cong_scalar2_nat)
2.702    also from b have "(d div gcd a n) * gcd a n = d"
2.703      by (rule dvd_div_mult_self)
2.704 @@ -656,14 +636,13 @@
2.705      by auto
2.706  qed
2.707
2.708 -lemma cong_solve_dvd_int:
2.709 +lemma cong_solve_dvd_int:
2.710    assumes a: "(a::int) \<noteq> 0" and b: "gcd a n dvd d"
2.711    shows "EX x. [a * x = d] (mod n)"
2.712  proof -
2.713 -  from cong_solve_int [OF a] obtain x where
2.714 -      "[a * x = gcd a n](mod n)"
2.715 +  from cong_solve_int [OF a] obtain x where "[a * x = gcd a n](mod n)"
2.716      by auto
2.717 -  hence "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)"
2.718 +  then have "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)"
2.719      by (elim cong_scalar2_int)
2.720    also from b have "(d div gcd a n) * gcd a n = d"
2.721      by (rule dvd_div_mult_self)
2.722 @@ -673,56 +652,52 @@
2.723      by auto
2.724  qed
2.725
2.726 -lemma cong_solve_coprime_nat: "coprime (a::nat) n \<Longrightarrow>
2.727 -    EX x. [a * x = 1] (mod n)"
2.728 -  apply (case_tac "a = 0")
2.729 +lemma cong_solve_coprime_nat: "coprime (a::nat) n \<Longrightarrow> EX x. [a * x = 1] (mod n)"
2.730 +  apply (cases "a = 0")
2.731    apply force
2.732    apply (frule cong_solve_nat [of a n])
2.733    apply auto
2.734 -done
2.735 +  done
2.736
2.737 -lemma cong_solve_coprime_int: "coprime (a::int) n \<Longrightarrow>
2.738 -    EX x. [a * x = 1] (mod n)"
2.739 -  apply (case_tac "a = 0")
2.740 +lemma cong_solve_coprime_int: "coprime (a::int) n \<Longrightarrow> EX x. [a * x = 1] (mod n)"
2.741 +  apply (cases "a = 0")
2.742    apply auto
2.743 -  apply (case_tac "n \<ge> 0")
2.744 +  apply (cases "n \<ge> 0")
2.745    apply auto
2.746    apply (subst cong_int_def, auto)
2.747    apply (frule cong_solve_int [of a n])
2.748    apply auto
2.749 -done
2.750 +  done
2.751
2.752 -lemma coprime_iff_invertible_nat: "m > (1::nat) \<Longrightarrow> coprime a m =
2.753 -    (EX x. [a * x = 1] (mod m))"
2.754 +lemma coprime_iff_invertible_nat: "m > (1::nat) \<Longrightarrow> coprime a m = (EX x. [a * x = 1] (mod m))"
2.755    apply (auto intro: cong_solve_coprime_nat)
2.756    apply (unfold cong_nat_def, auto intro: invertible_coprime_nat)
2.757 -done
2.758 +  done
2.759
2.760 -lemma coprime_iff_invertible_int: "m > (1::int) \<Longrightarrow> coprime a m =
2.761 -    (EX x. [a * x = 1] (mod m))"
2.762 +lemma coprime_iff_invertible_int: "m > (1::int) \<Longrightarrow> coprime a m = (EX x. [a * x = 1] (mod m))"
2.763    apply (auto intro: cong_solve_coprime_int)
2.764    apply (unfold cong_int_def)
2.765    apply (auto intro: invertible_coprime_int)
2.766 -done
2.767 +  done
2.768
2.769 -lemma coprime_iff_invertible'_int: "m > (1::int) \<Longrightarrow> coprime a m =
2.770 +lemma coprime_iff_invertible'_int: "m > (1::int) \<Longrightarrow> coprime a m =
2.771      (EX x. 0 <= x & x < m & [a * x = 1] (mod m))"
2.772    apply (subst coprime_iff_invertible_int)
2.773    apply auto
2.774    apply (auto simp add: cong_int_def)
2.775    apply (rule_tac x = "x mod m" in exI)
2.776    apply (auto simp add: mod_mult_right_eq [symmetric])
2.777 -done
2.778 +  done
2.779
2.780
2.781  lemma cong_cong_lcm_nat: "[(x::nat) = y] (mod a) \<Longrightarrow>
2.782      [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
2.783 -  apply (case_tac "y \<le> x")
2.784 +  apply (cases "y \<le> x")
2.785    apply (auto simp add: cong_altdef_nat lcm_least_nat) [1]
2.786    apply (rule cong_sym_nat)
2.787    apply (subst (asm) (1 2) cong_sym_eq_nat)
2.788    apply (auto simp add: cong_altdef_nat lcm_least_nat)
2.789 -done
2.790 +  done
2.791
2.792  lemma cong_cong_lcm_int: "[(x::int) = y] (mod a) \<Longrightarrow>
2.793      [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
2.794 @@ -730,15 +705,17 @@
2.795
2.796  lemma cong_cong_coprime_nat: "coprime a b \<Longrightarrow> [(x::nat) = y] (mod a) \<Longrightarrow>
2.797      [x = y] (mod b) \<Longrightarrow> [x = y] (mod a * b)"
2.798 -  apply (frule (1) cong_cong_lcm_nat)back
2.799 +  apply (frule (1) cong_cong_lcm_nat)
2.800 +  back
2.802 -done
2.803 +  done
2.804
2.805  lemma cong_cong_coprime_int: "coprime a b \<Longrightarrow> [(x::int) = y] (mod a) \<Longrightarrow>
2.806      [x = y] (mod b) \<Longrightarrow> [x = y] (mod a * b)"
2.807 -  apply (frule (1) cong_cong_lcm_int)back
2.808 +  apply (frule (1) cong_cong_lcm_int)
2.809 +  back
2.810    apply (simp add: lcm_altdef_int cong_abs_int abs_mult [symmetric])
2.811 -done
2.812 +  done
2.813
2.814  lemma cong_cong_setprod_coprime_nat [rule_format]: "finite A \<Longrightarrow>
2.815      (ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
2.816 @@ -750,7 +727,7 @@
2.817    apply (subst gcd_commute_nat)
2.818    apply (rule setprod_coprime_nat)
2.819    apply auto
2.820 -done
2.821 +  done
2.822
2.823  lemma cong_cong_setprod_coprime_int [rule_format]: "finite A \<Longrightarrow>
2.824      (ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
2.825 @@ -762,20 +739,18 @@
2.826    apply (subst gcd_commute_int)
2.827    apply (rule setprod_coprime_int)
2.828    apply auto
2.829 -done
2.830 +  done
2.831
2.832 -lemma binary_chinese_remainder_aux_nat:
2.833 +lemma binary_chinese_remainder_aux_nat:
2.834    assumes a: "coprime (m1::nat) m2"
2.835    shows "EX b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and>
2.836      [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)"
2.837  proof -
2.838 -  from cong_solve_coprime_nat [OF a]
2.839 -      obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
2.840 +  from cong_solve_coprime_nat [OF a] obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
2.841      by auto
2.842 -  from a have b: "coprime m2 m1"
2.843 +  from a have b: "coprime m2 m1"
2.844      by (subst gcd_commute_nat)
2.845 -  from cong_solve_coprime_nat [OF b]
2.846 -      obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
2.847 +  from cong_solve_coprime_nat [OF b] obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
2.848      by auto
2.849    have "[m1 * x1 = 0] (mod m1)"
2.850      by (subst mult_commute, rule cong_mult_self_nat)
2.851 @@ -785,18 +760,16 @@
2.852    ultimately show ?thesis by blast
2.853  qed
2.854
2.855 -lemma binary_chinese_remainder_aux_int:
2.856 +lemma binary_chinese_remainder_aux_int:
2.857    assumes a: "coprime (m1::int) m2"
2.858    shows "EX b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and>
2.859      [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)"
2.860  proof -
2.861 -  from cong_solve_coprime_int [OF a]
2.862 -      obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
2.863 +  from cong_solve_coprime_int [OF a] obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
2.864      by auto
2.865 -  from a have b: "coprime m2 m1"
2.866 +  from a have b: "coprime m2 m1"
2.867      by (subst gcd_commute_int)
2.868 -  from cong_solve_coprime_int [OF b]
2.869 -      obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
2.870 +  from cong_solve_coprime_int [OF b] obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
2.871      by auto
2.872    have "[m1 * x1 = 0] (mod m1)"
2.873      by (subst mult_commute, rule cong_mult_self_int)
2.874 @@ -811,8 +784,8 @@
2.875    shows "EX x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
2.876  proof -
2.877    from binary_chinese_remainder_aux_nat [OF a] obtain b1 b2
2.878 -    where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and
2.879 -          "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)"
2.880 +      where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and
2.881 +            "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)"
2.882      by blast
2.883    let ?x = "u1 * b1 + u2 * b2"
2.884    have "[?x = u1 * 1 + u2 * 0] (mod m1)"
2.885 @@ -822,7 +795,7 @@
2.886      apply (rule cong_scalar2_nat)
2.887      apply (rule `[b2 = 0] (mod m1)`)
2.888      done
2.889 -  hence "[?x = u1] (mod m1)" by simp
2.890 +  then have "[?x = u1] (mod m1)" by simp
2.891    have "[?x = u1 * 0 + u2 * 1] (mod m2)"
2.893      apply (rule cong_scalar2_nat)
2.894 @@ -830,7 +803,7 @@
2.895      apply (rule cong_scalar2_nat)
2.896      apply (rule `[b2 = 1] (mod m2)`)
2.897      done
2.898 -  hence "[?x = u2] (mod m2)" by simp
2.899 +  then have "[?x = u2] (mod m2)" by simp
2.900    with `[?x = u1] (mod m1)` show ?thesis by blast
2.901  qed
2.902
2.903 @@ -850,7 +823,7 @@
2.904      apply (rule cong_scalar2_int)
2.905      apply (rule `[b2 = 0] (mod m1)`)
2.906      done
2.907 -  hence "[?x = u1] (mod m1)" by simp
2.908 +  then have "[?x = u1] (mod m1)" by simp
2.909    have "[?x = u1 * 0 + u2 * 1] (mod m2)"
2.911      apply (rule cong_scalar2_int)
2.912 @@ -858,42 +831,42 @@
2.913      apply (rule cong_scalar2_int)
2.914      apply (rule `[b2 = 1] (mod m2)`)
2.915      done
2.916 -  hence "[?x = u2] (mod m2)" by simp
2.917 +  then have "[?x = u2] (mod m2)" by simp
2.918    with `[?x = u1] (mod m1)` show ?thesis by blast
2.919  qed
2.920
2.921 -lemma cong_modulus_mult_nat: "[(x::nat) = y] (mod m * n) \<Longrightarrow>
2.922 +lemma cong_modulus_mult_nat: "[(x::nat) = y] (mod m * n) \<Longrightarrow>
2.923      [x = y] (mod m)"
2.924 -  apply (case_tac "y \<le> x")
2.925 +  apply (cases "y \<le> x")
2.927    apply (erule dvd_mult_left)
2.928    apply (rule cong_sym_nat)
2.929    apply (subst (asm) cong_sym_eq_nat)
2.930 -  apply (simp add: cong_altdef_nat)
2.931 +  apply (simp add: cong_altdef_nat)
2.932    apply (erule dvd_mult_left)
2.933 -done
2.934 +  done
2.935
2.936 -lemma cong_modulus_mult_int: "[(x::int) = y] (mod m * n) \<Longrightarrow>
2.937 +lemma cong_modulus_mult_int: "[(x::int) = y] (mod m * n) \<Longrightarrow>
2.938      [x = y] (mod m)"
2.939 -  apply (simp add: cong_altdef_int)
2.940 +  apply (simp add: cong_altdef_int)
2.941    apply (erule dvd_mult_left)
2.942 -done
2.943 +  done
2.944
2.945 -lemma cong_less_modulus_unique_nat:
2.946 +lemma cong_less_modulus_unique_nat:
2.947      "[(x::nat) = y] (mod m) \<Longrightarrow> x < m \<Longrightarrow> y < m \<Longrightarrow> x = y"
2.949
2.950  lemma binary_chinese_remainder_unique_nat:
2.951 -  assumes a: "coprime (m1::nat) m2" and
2.952 -         nz: "m1 \<noteq> 0" "m2 \<noteq> 0"
2.953 +  assumes a: "coprime (m1::nat) m2"
2.954 +    and nz: "m1 \<noteq> 0" "m2 \<noteq> 0"
2.955    shows "EX! x. x < m1 * m2 \<and> [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
2.956  proof -
2.957 -  from binary_chinese_remainder_nat [OF a] obtain y where
2.958 +  from binary_chinese_remainder_nat [OF a] obtain y where
2.959        "[y = u1] (mod m1)" and "[y = u2] (mod m2)"
2.960      by blast
2.961    let ?x = "y mod (m1 * m2)"
2.962    from nz have less: "?x < m1 * m2"
2.963 -    by auto
2.964 +    by auto
2.965    have one: "[?x = u1] (mod m1)"
2.966      apply (rule cong_trans_nat)
2.967      prefer 2
2.968 @@ -911,9 +884,8 @@
2.969      apply (rule cong_mod_nat)
2.970      using nz apply auto
2.971      done
2.972 -  have "ALL z. z < m1 * m2 \<and> [z = u1] (mod m1) \<and> [z = u2] (mod m2) \<longrightarrow>
2.973 -      z = ?x"
2.974 -  proof (clarify)
2.975 +  have "ALL z. z < m1 * m2 \<and> [z = u1] (mod m1) \<and> [z = u2] (mod m2) \<longrightarrow> z = ?x"
2.976 +  proof clarify
2.977      fix z
2.978      assume "z < m1 * m2"
2.979      assume "[z = u1] (mod m1)" and  "[z = u2] (mod m2)"
2.980 @@ -935,46 +907,43 @@
2.981        apply (intro cong_less_modulus_unique_nat)
2.982        apply (auto, erule cong_sym_nat)
2.983        done
2.984 -  qed
2.985 -  with less one two show ?thesis
2.986 -    by auto
2.987 +  qed
2.988 +  with less one two show ?thesis by auto
2.989   qed
2.990
2.991  lemma chinese_remainder_aux_nat:
2.992 -  fixes A :: "'a set" and
2.993 -        m :: "'a \<Rightarrow> nat"
2.994 -  assumes fin: "finite A" and
2.995 -          cop: "ALL i : A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
2.996 -  shows "EX b. (ALL i : A.
2.997 -      [b i = 1] (mod m i) \<and> [b i = 0] (mod (PROD j : A - {i}. m j)))"
2.998 +  fixes A :: "'a set"
2.999 +    and m :: "'a \<Rightarrow> nat"
2.1000 +  assumes fin: "finite A"
2.1001 +    and cop: "ALL i : A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
2.1002 +  shows "EX b. (ALL i : A. [b i = 1] (mod m i) \<and> [b i = 0] (mod (PROD j : A - {i}. m j)))"
2.1003  proof (rule finite_set_choice, rule fin, rule ballI)
2.1004    fix i
2.1005    assume "i : A"
2.1006    with cop have "coprime (PROD j : A - {i}. m j) (m i)"
2.1007      by (intro setprod_coprime_nat, auto)
2.1008 -  hence "EX x. [(PROD j : A - {i}. m j) * x = 1] (mod m i)"
2.1009 +  then have "EX x. [(PROD j : A - {i}. m j) * x = 1] (mod m i)"
2.1010      by (elim cong_solve_coprime_nat)
2.1011    then obtain x where "[(PROD j : A - {i}. m j) * x = 1] (mod m i)"
2.1012      by auto
2.1013 -  moreover have "[(PROD j : A - {i}. m j) * x = 0]
2.1014 +  moreover have "[(PROD j : A - {i}. m j) * x = 0]
2.1015      (mod (PROD j : A - {i}. m j))"
2.1016      by (subst mult_commute, rule cong_mult_self_nat)
2.1017 -  ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0]
2.1018 +  ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0]
2.1019        (mod setprod m (A - {i}))"
2.1020      by blast
2.1021  qed
2.1022
2.1023  lemma chinese_remainder_nat:
2.1024 -  fixes A :: "'a set" and
2.1025 -        m :: "'a \<Rightarrow> nat" and
2.1026 -        u :: "'a \<Rightarrow> nat"
2.1027 -  assumes
2.1028 -        fin: "finite A" and
2.1029 -        cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
2.1030 +  fixes A :: "'a set"
2.1031 +    and m :: "'a \<Rightarrow> nat"
2.1032 +    and u :: "'a \<Rightarrow> nat"
2.1033 +  assumes fin: "finite A"
2.1034 +    and cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
2.1035    shows "EX x. (ALL i:A. [x = u i] (mod m i))"
2.1036  proof -
2.1037    from chinese_remainder_aux_nat [OF fin cop] obtain b where
2.1038 -    bprop: "ALL i:A. [b i = 1] (mod m i) \<and>
2.1039 +    bprop: "ALL i:A. [b i = 1] (mod m i) \<and>
2.1040        [b i = 0] (mod (PROD j : A - {i}. m j))"
2.1041      by blast
2.1042    let ?x = "SUM i:A. (u i) * (b i)"
2.1043 @@ -982,12 +951,12 @@
2.1044    proof (rule exI, clarify)
2.1045      fix i
2.1046      assume a: "i : A"
2.1047 -    show "[?x = u i] (mod m i)"
2.1048 +    show "[?x = u i] (mod m i)"
2.1049      proof -
2.1050 -      from fin a have "?x = (SUM j:{i}. u j * b j) +
2.1051 +      from fin a have "?x = (SUM j:{i}. u j * b j) +
2.1052            (SUM j:A-{i}. u j * b j)"
2.1053          by (subst setsum_Un_disjoint [symmetric], auto intro: setsum_cong)
2.1054 -      hence "[?x = u i * b i + (SUM j:A-{i}. u j * b j)] (mod m i)"
2.1055 +      then have "[?x = u i * b i + (SUM j:A-{i}. u j * b j)] (mod m i)"
2.1056          by auto
2.1057        also have "[u i * b i + (SUM j:A-{i}. u j * b j) =
2.1058                    u i * 1 + (SUM j:A-{i}. u j * 0)] (mod m i)"
2.1059 @@ -1010,35 +979,34 @@
2.1060    qed
2.1061  qed
2.1062
2.1063 -lemma coprime_cong_prod_nat [rule_format]: "finite A \<Longrightarrow>
2.1064 +lemma coprime_cong_prod_nat [rule_format]: "finite A \<Longrightarrow>
2.1065      (ALL i: A. (ALL j: A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
2.1066        (ALL i: A. [(x::nat) = y] (mod m i)) \<longrightarrow>
2.1067 -         [x = y] (mod (PROD i:A. m i))"
2.1068 +         [x = y] (mod (PROD i:A. m i))"
2.1069    apply (induct set: finite)
2.1070    apply auto
2.1071    apply (erule (1) coprime_cong_mult_nat)
2.1072    apply (subst gcd_commute_nat)
2.1073    apply (rule setprod_coprime_nat)
2.1074    apply auto
2.1075 -done
2.1076 +  done
2.1077
2.1078  lemma chinese_remainder_unique_nat:
2.1079 -  fixes A :: "'a set" and
2.1080 -        m :: "'a \<Rightarrow> nat" and
2.1081 -        u :: "'a \<Rightarrow> nat"
2.1082 -  assumes
2.1083 -        fin: "finite A" and
2.1084 -         nz: "ALL i:A. m i \<noteq> 0" and
2.1085 -        cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
2.1086 +  fixes A :: "'a set"
2.1087 +    and m :: "'a \<Rightarrow> nat"
2.1088 +    and u :: "'a \<Rightarrow> nat"
2.1089 +  assumes fin: "finite A"
2.1090 +    and nz: "ALL i:A. m i \<noteq> 0"
2.1091 +    and cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
2.1092    shows "EX! x. x < (PROD i:A. m i) \<and> (ALL i:A. [x = u i] (mod m i))"
2.1093  proof -
2.1094 -  from chinese_remainder_nat [OF fin cop] obtain y where
2.1095 -      one: "(ALL i:A. [y = u i] (mod m i))"
2.1096 +  from chinese_remainder_nat [OF fin cop]
2.1097 +  obtain y where one: "(ALL i:A. [y = u i] (mod m i))"
2.1098      by blast
2.1099    let ?x = "y mod (PROD i:A. m i)"
2.1100    from fin nz have prodnz: "(PROD i:A. m i) \<noteq> 0"
2.1101      by auto
2.1102 -  hence less: "?x < (PROD i:A. m i)"
2.1103 +  then have less: "?x < (PROD i:A. m i)"
2.1104      by auto
2.1105    have cong: "ALL i:A. [?x = u i] (mod m i)"
2.1106      apply auto
2.1107 @@ -1052,28 +1020,29 @@
2.1108      apply (rule fin)
2.1109      apply assumption
2.1110      done
2.1111 -  have unique: "ALL z. z < (PROD i:A. m i) \<and>
2.1112 +  have unique: "ALL z. z < (PROD i:A. m i) \<and>
2.1113        (ALL i:A. [z = u i] (mod m i)) \<longrightarrow> z = ?x"
2.1114    proof (clarify)
2.1115      fix z
2.1116      assume zless: "z < (PROD i:A. m i)"
2.1117      assume zcong: "(ALL i:A. [z = u i] (mod m i))"
2.1118      have "ALL i:A. [?x = z] (mod m i)"
2.1119 -      apply clarify
2.1120 +      apply clarify
2.1121        apply (rule cong_trans_nat)
2.1122        using cong apply (erule bspec)
2.1123        apply (rule cong_sym_nat)
2.1124        using zcong apply auto
2.1125        done
2.1126      with fin cop have "[?x = z] (mod (PROD i:A. m i))"
2.1127 -      by (intro coprime_cong_prod_nat, auto)
2.1128 +      apply (intro coprime_cong_prod_nat)
2.1129 +      apply auto
2.1130 +      done
2.1131      with zless less show "z = ?x"
2.1132        apply (intro cong_less_modulus_unique_nat)
2.1133        apply (auto, erule cong_sym_nat)
2.1134        done
2.1135 -  qed
2.1136 -  from less cong unique show ?thesis
2.1137 -    by blast
2.1138 +  qed
2.1139 +  from less cong unique show ?thesis by blast
2.1140  qed
2.1141
2.1142  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 -
3.17 -begin
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 -
3.38 -begin
3.39 +begin
3.40
3.41 -definition
3.42 -  fib_int :: "int \<Rightarrow> int"
3.43 -where
3.44 -  "fib_int n = (if n >= 0 then int (fib (nat n)) else 0)"
3.45 +definition fib_int :: "int \<Rightarrow> int"
3.46 +  where "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.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.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.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.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.144 -done
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.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.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.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.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.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.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.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.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.174 @@ -205,89 +197,87 @@
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.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.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.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.29
7.30 -lemma msetprod_singleton:
7.31 -  "msetprod f {#x#} = f x"
7.32 +lemma msetprod_singleton: "msetprod f {#x#} = f x"
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.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.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.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.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.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.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
```