--- a/src/HOL/Number_Theory/Binomial.thy Sat Sep 10 22:11:55 2011 +0200
+++ b/src/HOL/Number_Theory/Binomial.thy Sat Sep 10 23:27:32 2011 +0200
@@ -20,40 +20,35 @@
subsection {* Main definitions *}
class binomial =
-
-fixes
- binomial :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "choose" 65)
+ fixes binomial :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "choose" 65)
(* definitions for the natural numbers *)
instantiation nat :: binomial
-
begin
-fun
- binomial_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+fun binomial_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
where
"binomial_nat n k =
(if k = 0 then 1 else
if n = 0 then 0 else
(binomial (n - 1) k) + (binomial (n - 1) (k - 1)))"
-instance proof qed
+instance ..
end
(* definitions for the integers *)
instantiation int :: binomial
-
begin
-definition
- binomial_int :: "int => int \<Rightarrow> int"
-where
- "binomial_int n k = (if n \<ge> 0 \<and> k \<ge> 0 then int (binomial (nat n) (nat k))
- else 0)"
-instance proof qed
+definition binomial_int :: "int => int \<Rightarrow> int" where
+ "binomial_int n k =
+ (if n \<ge> 0 \<and> k \<ge> 0 then int (binomial (nat n) (nat k))
+ else 0)"
+
+instance ..
end
@@ -97,10 +92,11 @@
by (induct n rule: induct'_nat, auto)
lemma zero_choose_int [rule_format,simp]: "(k::int) > n \<Longrightarrow> n choose k = 0"
- unfolding binomial_int_def apply (case_tac "n < 0")
+ unfolding binomial_int_def
+ apply (cases "n < 0")
apply force
apply (simp del: binomial_nat.simps)
-done
+ done
lemma choose_reduce_nat: "(n::nat) > 0 \<Longrightarrow> 0 < k \<Longrightarrow>
(n choose k) = ((n - 1) choose k) + ((n - 1) choose (k - 1))"
@@ -108,10 +104,10 @@
lemma choose_reduce_int: "(n::int) > 0 \<Longrightarrow> 0 < k \<Longrightarrow>
(n choose k) = ((n - 1) choose k) + ((n - 1) choose (k - 1))"
- unfolding binomial_int_def apply (subst choose_reduce_nat)
- apply (auto simp del: binomial_nat.simps
- simp add: nat_diff_distrib)
-done
+ unfolding binomial_int_def
+ apply (subst choose_reduce_nat)
+ apply (auto simp del: binomial_nat.simps simp add: nat_diff_distrib)
+ done
lemma choose_plus_one_nat: "((n::nat) + 1) choose (k + 1) =
(n choose (k + 1)) + (n choose k)"
@@ -128,13 +124,13 @@
declare binomial_nat.simps [simp del]
lemma choose_self_nat [simp]: "((n::nat) choose n) = 1"
- by (induct n rule: induct'_nat, auto simp add: choose_plus_one_nat)
+ by (induct n rule: induct'_nat) (auto simp add: choose_plus_one_nat)
lemma choose_self_int [simp]: "n \<ge> 0 \<Longrightarrow> ((n::int) choose n) = 1"
by (auto simp add: binomial_int_def)
lemma choose_one_nat [simp]: "(n::nat) choose 1 = n"
- by (induct n rule: induct'_nat, auto simp add: choose_reduce_nat)
+ by (induct n rule: induct'_nat) (auto simp add: choose_reduce_nat)
lemma choose_one_int [simp]: "n \<ge> 0 \<Longrightarrow> (n::int) choose 1 = n"
by (auto simp add: binomial_int_def)
@@ -165,7 +161,7 @@
apply force
apply (subst choose_reduce_nat)
apply auto
-done
+ done
lemma choose_pos_int: "n \<ge> 0 \<Longrightarrow> k >= 0 \<Longrightarrow> k \<le> n \<Longrightarrow>
((n::int) choose k) > 0"
@@ -183,7 +179,7 @@
apply (drule_tac x = n in spec) back back
apply (drule_tac x = "k - 1" in spec) back back back
apply auto
-done
+ done
lemma choose_altdef_aux_nat: "(k::nat) \<le> n \<Longrightarrow>
fact k * fact (n - k) * (n choose k) = fact n"
@@ -193,10 +189,9 @@
fix k :: nat and n
assume less: "k < n"
assume ih1: "fact k * fact (n - k) * (n choose k) = fact n"
- hence one: "fact (k + 1) * fact (n - k) * (n choose k) = (k + 1) * fact n"
+ then have one: "fact (k + 1) * fact (n - k) * (n choose k) = (k + 1) * fact n"
by (subst fact_plus_one_nat, auto)
- assume ih2: "fact (k + 1) * fact (n - (k + 1)) * (n choose (k + 1)) =
- fact n"
+ assume ih2: "fact (k + 1) * fact (n - (k + 1)) * (n choose (k + 1)) = fact n"
with less have "fact (k + 1) * fact ((n - (k + 1)) + 1) *
(n choose (k + 1)) = (n - k) * fact n"
by (subst (2) fact_plus_one_nat, auto)
@@ -222,7 +217,7 @@
apply (frule choose_altdef_aux_nat)
apply (erule subst)
apply (simp add: mult_ac)
-done
+ done
lemma choose_altdef_int:
@@ -238,7 +233,7 @@
(* why don't blast and auto get this??? *)
apply (rule exI)
apply (erule sym)
-done
+ done
lemma choose_dvd_int:
assumes "(0::int) <= k" and "k <= n"
@@ -293,7 +288,8 @@
fixes S :: "'a set"
shows "finite S \<Longrightarrow> card {T. T \<le> S \<and> card T = k} = card S choose k"
proof (induct arbitrary: k set: finite)
- case empty show ?case by (auto simp add: Collect_conv_if)
+ case empty
+ show ?case by (auto simp add: Collect_conv_if)
next
case (insert x F)
note iassms = insert(1,2)
@@ -303,11 +299,11 @@
case zero
from iassms have "{T. T \<le> (insert x F) \<and> card T = 0} = {{}}"
by (auto simp: finite_subset)
- thus ?case by auto
+ then show ?case by auto
next
case (plus1 k)
from iassms have fin: "finite (insert x F)" by auto
- hence "{ T. T \<subseteq> insert x F \<and> card T = k + 1} =
+ then have "{ T. T \<subseteq> insert x F \<and> card T = k + 1} =
{T. T \<le> F & card T = k + 1} Un
{T. T \<le> insert x F & x : T & card T = k + 1}"
by auto
@@ -326,14 +322,14 @@
let ?f = "%T. T Un {x}"
from iassms have "inj_on ?f {T. T <= F & card T = k}"
unfolding inj_on_def by auto
- hence "card ({T. T <= F & card T = k}) =
+ then have "card ({T. T <= F & card T = k}) =
card(?f ` {T. T <= F & card T = k})"
by (rule card_image [symmetric])
also have "?f ` {T. T <= F & card T = k} =
{T. T \<subseteq> insert x F \<and> x : T \<and> card T = k + 1}" (is "?L=?R")
proof-
{ fix S assume "S \<subseteq> F"
- hence "card(insert x S) = card S +1"
+ then have "card(insert x S) = card S +1"
using iassms by (auto simp: finite_subset) }
moreover
{ fix T assume 1: "T \<subseteq> insert x F" "x : T" "card T = k+1"
@@ -353,5 +349,4 @@
qed
qed
-
end
--- a/src/HOL/Number_Theory/Cong.thy Sat Sep 10 22:11:55 2011 +0200
+++ b/src/HOL/Number_Theory/Cong.thy Sat Sep 10 23:27:32 2011 +0200
@@ -14,7 +14,7 @@
The original theory "IntPrimes" was by Thomas M. Rasmussen, and
extended gcd, lcm, primes to the integers. Amine Chaieb provided
another extension of the notions to the integers, and added a number
-of results to "Primes" and "GCD".
+of results to "Primes" and "GCD".
The original theory, "IntPrimes", by Thomas M. Rasmussen, defined and
developed the congruence relations on the integers. The notion was
@@ -29,34 +29,33 @@
imports Primes
begin
-subsection {* Turn off One_nat_def *}
+subsection {* Turn off @{text One_nat_def} *}
-lemma induct'_nat [case_names zero plus1, induct type: nat]:
- "\<lbrakk> P (0::nat); !!n. P n \<Longrightarrow> P (n + 1)\<rbrakk> \<Longrightarrow> P n"
-by (erule nat_induct) (simp add:One_nat_def)
+lemma induct'_nat [case_names zero plus1, induct type: nat]:
+ "P (0::nat) \<Longrightarrow> (\<And>n. P n \<Longrightarrow> P (n + 1)) \<Longrightarrow> P n"
+ by (induct n) (simp_all add: One_nat_def)
-lemma cases_nat [case_names zero plus1, cases type: nat]:
- "P (0::nat) \<Longrightarrow> (!!n. P (n + 1)) \<Longrightarrow> P n"
-by(metis induct'_nat)
+lemma cases_nat [case_names zero plus1, cases type: nat]:
+ "P (0::nat) \<Longrightarrow> (\<And>n. P (n + 1)) \<Longrightarrow> P n"
+ by (rule induct'_nat)
lemma power_plus_one [simp]: "(x::'a::power)^(n + 1) = x * x^n"
-by (simp add: One_nat_def)
+ by (simp add: One_nat_def)
-lemma power_eq_one_eq_nat [simp]:
- "((x::nat)^m = 1) = (m = 0 | x = 1)"
-by (induct m, auto)
+lemma power_eq_one_eq_nat [simp]: "((x::nat)^m = 1) = (m = 0 | x = 1)"
+ by (induct m) auto
lemma card_insert_if' [simp]: "finite A \<Longrightarrow>
- card (insert x A) = (if x \<in> A then (card A) else (card A) + 1)"
-by (auto simp add: insert_absorb)
+ card (insert x A) = (if x \<in> A then (card A) else (card A) + 1)"
+ by (auto simp add: insert_absorb)
lemma nat_1' [simp]: "nat 1 = 1"
-by simp
+ by simp
(* For those annoying moments where Suc reappears, use Suc_eq_plus1 *)
declare nat_1 [simp del]
-declare add_2_eq_Suc [simp del]
+declare add_2_eq_Suc [simp del]
declare add_2_eq_Suc' [simp del]
@@ -66,31 +65,23 @@
subsection {* Main definitions *}
class cong =
-
-fixes
- cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ = _] '(mod _'))")
-
+ fixes cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ = _] '(mod _'))")
begin
-abbreviation
- notcong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ \<noteq> _] '(mod _'))")
-where
- "notcong x y m == (~cong x y m)"
+abbreviation notcong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ \<noteq> _] '(mod _'))")
+ where "notcong x y m \<equiv> \<not> cong x y m"
end
(* definitions for the natural numbers *)
instantiation nat :: cong
-
-begin
+begin
-definition
- cong_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
-where
- "cong_nat x y m = ((x mod m) = (y mod m))"
+definition cong_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
+ where "cong_nat x y m = ((x mod m) = (y mod m))"
-instance proof qed
+instance ..
end
@@ -98,15 +89,12 @@
(* definitions for the integers *)
instantiation int :: cong
-
-begin
+begin
-definition
- cong_int :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool"
-where
- "cong_int x y m = ((x mod m) = (y mod m))"
+definition cong_int :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool"
+ where "cong_int x y m = ((x mod m) = (y mod m))"
-instance proof qed
+instance ..
end
@@ -115,25 +103,25 @@
lemma transfer_nat_int_cong:
- "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> m >= 0 \<Longrightarrow>
+ "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> m >= 0 \<Longrightarrow>
([(nat x) = (nat y)] (mod (nat m))) = ([x = y] (mod m))"
- unfolding cong_int_def cong_nat_def
+ unfolding cong_int_def cong_nat_def
apply (auto simp add: nat_mod_distrib [symmetric])
apply (subst (asm) eq_nat_nat_iff)
- apply (case_tac "m = 0", force, rule pos_mod_sign, force)+
+ apply (cases "m = 0", force, rule pos_mod_sign, force)+
apply assumption
-done
+ done
-declare transfer_morphism_nat_int[transfer add return:
+declare transfer_morphism_nat_int[transfer add return:
transfer_nat_int_cong]
lemma transfer_int_nat_cong:
"[(int x) = (int y)] (mod (int m)) = [x = y] (mod m)"
apply (auto simp add: cong_int_def cong_nat_def)
apply (auto simp add: zmod_int [symmetric])
-done
+ done
-declare transfer_morphism_int_nat[transfer add return:
+declare transfer_morphism_int_nat[transfer add return:
transfer_int_nat_cong]
@@ -141,52 +129,52 @@
(* was zcong_0, etc. *)
lemma cong_0_nat [simp, presburger]: "([(a::nat) = b] (mod 0)) = (a = b)"
- by (unfold cong_nat_def, auto)
+ unfolding cong_nat_def by auto
lemma cong_0_int [simp, presburger]: "([(a::int) = b] (mod 0)) = (a = b)"
- by (unfold cong_int_def, auto)
+ unfolding cong_int_def by auto
lemma cong_1_nat [simp, presburger]: "[(a::nat) = b] (mod 1)"
- by (unfold cong_nat_def, auto)
+ unfolding cong_nat_def by auto
lemma cong_Suc_0_nat [simp, presburger]: "[(a::nat) = b] (mod Suc 0)"
- by (unfold cong_nat_def, auto simp add: One_nat_def)
+ unfolding cong_nat_def by (auto simp add: One_nat_def)
lemma cong_1_int [simp, presburger]: "[(a::int) = b] (mod 1)"
- by (unfold cong_int_def, auto)
+ unfolding cong_int_def by auto
lemma cong_refl_nat [simp]: "[(k::nat) = k] (mod m)"
- by (unfold cong_nat_def, auto)
+ unfolding cong_nat_def by auto
lemma cong_refl_int [simp]: "[(k::int) = k] (mod m)"
- by (unfold cong_int_def, auto)
+ unfolding cong_int_def by auto
lemma cong_sym_nat: "[(a::nat) = b] (mod m) \<Longrightarrow> [b = a] (mod m)"
- by (unfold cong_nat_def, auto)
+ unfolding cong_nat_def by auto
lemma cong_sym_int: "[(a::int) = b] (mod m) \<Longrightarrow> [b = a] (mod m)"
- by (unfold cong_int_def, auto)
+ unfolding cong_int_def by auto
lemma cong_sym_eq_nat: "[(a::nat) = b] (mod m) = [b = a] (mod m)"
- by (unfold cong_nat_def, auto)
+ unfolding cong_nat_def by auto
lemma cong_sym_eq_int: "[(a::int) = b] (mod m) = [b = a] (mod m)"
- by (unfold cong_int_def, auto)
+ unfolding cong_int_def by auto
lemma cong_trans_nat [trans]:
"[(a::nat) = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)"
- by (unfold cong_nat_def, auto)
+ unfolding cong_nat_def by auto
lemma cong_trans_int [trans]:
"[(a::int) = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)"
- by (unfold cong_int_def, auto)
+ unfolding cong_int_def by auto
lemma cong_add_nat:
"[(a::nat) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a + c = b + d] (mod m)"
apply (unfold cong_nat_def)
apply (subst (1 2) mod_add_eq)
apply simp
-done
+ done
lemma cong_add_int:
"[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a + c = b + d] (mod m)"
@@ -194,21 +182,21 @@
apply (subst (1 2) mod_add_left_eq)
apply (subst (1 2) mod_add_right_eq)
apply simp
-done
+ done
lemma cong_diff_int:
"[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a - c = b - d] (mod m)"
apply (unfold cong_int_def)
apply (subst (1 2) mod_diff_eq)
apply simp
-done
+ done
lemma cong_diff_aux_int:
- "(a::int) >= c \<Longrightarrow> b >= d \<Longrightarrow> [(a::int) = b] (mod m) \<Longrightarrow>
+ "(a::int) >= c \<Longrightarrow> b >= d \<Longrightarrow> [(a::int) = b] (mod m) \<Longrightarrow>
[c = d] (mod m) \<Longrightarrow> [tsub a c = tsub b d] (mod m)"
apply (subst (1 2) tsub_eq)
apply (auto intro: cong_diff_int)
-done;
+ done
lemma cong_diff_nat:
assumes "(a::nat) >= c" and "b >= d" and "[a = b] (mod m)" and
@@ -221,7 +209,7 @@
apply (unfold cong_nat_def)
apply (subst (1 2) mod_mult_eq)
apply simp
-done
+ done
lemma cong_mult_int:
"[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)"
@@ -230,73 +218,69 @@
apply (subst (1 2) mult_commute)
apply (subst (1 2) zmod_zmult1_eq)
apply simp
-done
-
-lemma cong_exp_nat: "[(x::nat) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
- apply (induct k)
- apply (auto simp add: cong_mult_nat)
- done
-
-lemma cong_exp_int: "[(x::int) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
- apply (induct k)
- apply (auto simp add: cong_mult_int)
done
-lemma cong_setsum_nat [rule_format]:
- "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
+lemma cong_exp_nat: "[(x::nat) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
+ by (induct k) (auto simp add: cong_mult_nat)
+
+lemma cong_exp_int: "[(x::int) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
+ by (induct k) (auto simp add: cong_mult_int)
+
+lemma cong_setsum_nat [rule_format]:
+ "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
[(SUM x:A. f x) = (SUM x:A. g x)] (mod m)"
- apply (case_tac "finite A")
+ apply (cases "finite A")
apply (induct set: finite)
apply (auto intro: cong_add_nat)
-done
+ done
lemma cong_setsum_int [rule_format]:
- "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
+ "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
[(SUM x:A. f x) = (SUM x:A. g x)] (mod m)"
- apply (case_tac "finite A")
+ apply (cases "finite A")
apply (induct set: finite)
apply (auto intro: cong_add_int)
-done
+ done
-lemma cong_setprod_nat [rule_format]:
- "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
+lemma cong_setprod_nat [rule_format]:
+ "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
[(PROD x:A. f x) = (PROD x:A. g x)] (mod m)"
- apply (case_tac "finite A")
+ apply (cases "finite A")
apply (induct set: finite)
apply (auto intro: cong_mult_nat)
-done
+ done
-lemma cong_setprod_int [rule_format]:
- "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
+lemma cong_setprod_int [rule_format]:
+ "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
[(PROD x:A. f x) = (PROD x:A. g x)] (mod m)"
- apply (case_tac "finite A")
+ apply (cases "finite A")
apply (induct set: finite)
apply (auto intro: cong_mult_int)
-done
+ done
lemma cong_scalar_nat: "[(a::nat)= b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)"
- by (rule cong_mult_nat, simp_all)
+ by (rule cong_mult_nat) simp_all
lemma cong_scalar_int: "[(a::int)= b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)"
- by (rule cong_mult_int, simp_all)
+ by (rule cong_mult_int) simp_all
lemma cong_scalar2_nat: "[(a::nat)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)"
- by (rule cong_mult_nat, simp_all)
+ by (rule cong_mult_nat) simp_all
lemma cong_scalar2_int: "[(a::int)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)"
- by (rule cong_mult_int, simp_all)
+ by (rule cong_mult_int) simp_all
lemma cong_mult_self_nat: "[(a::nat) * m = 0] (mod m)"
- by (unfold cong_nat_def, auto)
+ unfolding cong_nat_def by auto
lemma cong_mult_self_int: "[(a::int) * m = 0] (mod m)"
- by (unfold cong_int_def, auto)
+ unfolding cong_int_def by auto
lemma cong_eq_diff_cong_0_int: "[(a::int) = b] (mod m) = [a - b = 0] (mod m)"
apply (rule iffI)
apply (erule cong_diff_int [of a b m b b, simplified])
apply (erule cong_add_int [of "a - b" 0 m b b, simplified])
-done
+ done
lemma cong_eq_diff_cong_0_aux_int: "a >= b \<Longrightarrow>
[(a::int) = b] (mod m) = [tsub a b = 0] (mod m)"
@@ -307,29 +291,29 @@
shows "[a = b] (mod m) = [a - b = 0] (mod m)"
using assms by (rule cong_eq_diff_cong_0_aux_int [transferred])
-lemma cong_diff_cong_0'_nat:
- "[(x::nat) = y] (mod n) \<longleftrightarrow>
+lemma cong_diff_cong_0'_nat:
+ "[(x::nat) = y] (mod n) \<longleftrightarrow>
(if x <= y then [y - x = 0] (mod n) else [x - y = 0] (mod n))"
- apply (case_tac "y <= x")
+ apply (cases "y <= x")
apply (frule cong_eq_diff_cong_0_nat [where m = n])
apply auto [1]
apply (subgoal_tac "x <= y")
apply (frule cong_eq_diff_cong_0_nat [where m = n])
apply (subst cong_sym_eq_nat)
apply auto
-done
+ done
lemma cong_altdef_nat: "(a::nat) >= b \<Longrightarrow> [a = b] (mod m) = (m dvd (a - b))"
apply (subst cong_eq_diff_cong_0_nat, assumption)
apply (unfold cong_nat_def)
apply (simp add: dvd_eq_mod_eq_0 [symmetric])
-done
+ done
lemma cong_altdef_int: "[(a::int) = b] (mod m) = (m dvd (a - b))"
apply (subst cong_eq_diff_cong_0_int)
apply (unfold cong_int_def)
apply (simp add: dvd_eq_mod_eq_0 [symmetric])
-done
+ done
lemma cong_abs_int: "[(x::int) = y] (mod abs m) = [x = y] (mod m)"
by (simp add: cong_altdef_int)
@@ -342,29 +326,29 @@
(* any way around this? *)
apply (subgoal_tac "a * a - 1 = (a - 1) * (a - -1)")
apply (auto simp add: field_simps)
-done
+ done
lemma cong_mult_rcancel_int:
- "coprime k (m::int) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
+ "coprime k (m::int) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
apply (subst (1 2) cong_altdef_int)
apply (subst left_diff_distrib [symmetric])
apply (rule coprime_dvd_mult_iff_int)
apply (subst gcd_commute_int, assumption)
-done
+ done
lemma cong_mult_rcancel_nat:
assumes "coprime k (m::nat)"
shows "[a * k = b * k] (mod m) = [a = b] (mod m)"
apply (rule cong_mult_rcancel_int [transferred])
using assms apply auto
-done
+ done
lemma cong_mult_lcancel_nat:
- "coprime k (m::nat) \<Longrightarrow> [k * a = k * b ] (mod m) = [a = b] (mod m)"
+ "coprime k (m::nat) \<Longrightarrow> [k * a = k * b ] (mod m) = [a = b] (mod m)"
by (simp add: mult_commute cong_mult_rcancel_nat)
lemma cong_mult_lcancel_int:
- "coprime k (m::int) \<Longrightarrow> [k * a = k * b] (mod m) = [a = b] (mod m)"
+ "coprime k (m::int) \<Longrightarrow> [k * a = k * b] (mod m) = [a = b] (mod m)"
by (simp add: mult_commute cong_mult_rcancel_int)
(* was zcong_zgcd_zmult_zmod *)
@@ -395,7 +379,7 @@
apply auto
apply (rule_tac x = "a mod m" in exI)
apply (unfold cong_nat_def, auto)
-done
+ done
lemma cong_less_unique_int:
"0 < (m::int) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
@@ -407,12 +391,12 @@
lemma cong_iff_lin_int: "([(a::int) = b] (mod m)) = (\<exists>k. b = a + m * k)"
apply (auto simp add: cong_altdef_int dvd_def field_simps)
apply (rule_tac [!] x = "-k" in exI, auto)
-done
+ done
-lemma cong_iff_lin_nat: "([(a::nat) = b] (mod m)) =
+lemma cong_iff_lin_nat: "([(a::nat) = b] (mod m)) =
(\<exists>k1 k2. b + k1 * m = a + k2 * m)"
apply (rule iffI)
- apply (case_tac "b <= a")
+ apply (cases "b <= a")
apply (subst (asm) cong_altdef_nat, assumption)
apply (unfold dvd_def, auto)
apply (rule_tac x = k in exI)
@@ -430,42 +414,40 @@
apply (erule ssubst)back
apply (erule subst)
apply auto
-done
+ done
lemma cong_gcd_eq_int: "[(a::int) = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
apply (subst (asm) cong_iff_lin_int, auto)
- apply (subst add_commute)
+ apply (subst add_commute)
apply (subst (2) gcd_commute_int)
apply (subst mult_commute)
apply (subst gcd_add_mult_int)
apply (rule gcd_commute_int)
done
-lemma cong_gcd_eq_nat:
+lemma cong_gcd_eq_nat:
assumes "[(a::nat) = b] (mod m)"
shows "gcd a m = gcd b m"
apply (rule cong_gcd_eq_int [transferred])
using assms apply auto
done
-lemma cong_imp_coprime_nat: "[(a::nat) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow>
- coprime b m"
+lemma cong_imp_coprime_nat: "[(a::nat) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
by (auto simp add: cong_gcd_eq_nat)
-lemma cong_imp_coprime_int: "[(a::int) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow>
- coprime b m"
+lemma cong_imp_coprime_int: "[(a::int) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
by (auto simp add: cong_gcd_eq_int)
-lemma cong_cong_mod_nat: "[(a::nat) = b] (mod m) =
- [a mod m = b mod m] (mod m)"
+lemma cong_cong_mod_nat: "[(a::nat) = b] (mod m) = [a mod m = b mod m] (mod m)"
by (auto simp add: cong_nat_def)
-lemma cong_cong_mod_int: "[(a::int) = b] (mod m) =
- [a mod m = b mod m] (mod m)"
+lemma cong_cong_mod_int: "[(a::int) = b] (mod m) = [a mod m = b mod m] (mod m)"
by (auto simp add: cong_int_def)
lemma cong_minus_int [iff]: "[(a::int) = b] (mod -m) = [a = b] (mod m)"
- by (subst (1 2) cong_altdef_int, auto)
+ apply (subst (1 2) cong_altdef_int)
+ apply auto
+ done
lemma cong_zero_nat: "[(a::nat) = b] (mod 0) = (a = b)"
by auto
@@ -479,7 +461,7 @@
apply (unfold dvd_def, auto)
apply (rule mod_mod_cancel)
apply auto
-done
+ done
lemma mod_dvd_mod:
assumes "0 < (m::nat)" and "m dvd b"
@@ -490,12 +472,12 @@
done
*)
-lemma cong_add_lcancel_nat:
- "[(a::nat) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
+lemma cong_add_lcancel_nat:
+ "[(a::nat) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
by (simp add: cong_iff_lin_nat)
-lemma cong_add_lcancel_int:
- "[(a::int) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
+lemma cong_add_lcancel_int:
+ "[(a::int) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
by (simp add: cong_iff_lin_int)
lemma cong_add_rcancel_nat: "[(x::nat) + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
@@ -504,43 +486,42 @@
lemma cong_add_rcancel_int: "[(x::int) + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
by (simp add: cong_iff_lin_int)
-lemma cong_add_lcancel_0_nat: "[(a::nat) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
+lemma cong_add_lcancel_0_nat: "[(a::nat) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
by (simp add: cong_iff_lin_nat)
-lemma cong_add_lcancel_0_int: "[(a::int) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
+lemma cong_add_lcancel_0_int: "[(a::int) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
by (simp add: cong_iff_lin_int)
-lemma cong_add_rcancel_0_nat: "[x + (a::nat) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
+lemma cong_add_rcancel_0_nat: "[x + (a::nat) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
by (simp add: cong_iff_lin_nat)
-lemma cong_add_rcancel_0_int: "[x + (a::int) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
+lemma cong_add_rcancel_0_int: "[x + (a::int) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
by (simp add: cong_iff_lin_int)
-lemma cong_dvd_modulus_nat: "[(x::nat) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow>
+lemma cong_dvd_modulus_nat: "[(x::nat) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow>
[x = y] (mod n)"
apply (auto simp add: cong_iff_lin_nat dvd_def)
apply (rule_tac x="k1 * k" in exI)
apply (rule_tac x="k2 * k" in exI)
apply (simp add: field_simps)
-done
+ done
-lemma cong_dvd_modulus_int: "[(x::int) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow>
- [x = y] (mod n)"
+lemma cong_dvd_modulus_int: "[(x::int) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> [x = y] (mod n)"
by (auto simp add: cong_altdef_int dvd_def)
lemma cong_dvd_eq_nat: "[(x::nat) = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y"
- by (unfold cong_nat_def, auto simp add: dvd_eq_mod_eq_0)
+ unfolding cong_nat_def by (auto simp add: dvd_eq_mod_eq_0)
lemma cong_dvd_eq_int: "[(x::int) = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y"
- by (unfold cong_int_def, auto simp add: dvd_eq_mod_eq_0)
+ unfolding cong_int_def by (auto simp add: dvd_eq_mod_eq_0)
-lemma cong_mod_nat: "(n::nat) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)"
+lemma cong_mod_nat: "(n::nat) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)"
by (simp add: cong_nat_def)
-lemma cong_mod_int: "(n::int) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)"
+lemma cong_mod_int: "(n::int) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)"
by (simp add: cong_int_def)
-lemma mod_mult_cong_nat: "(a::nat) ~= 0 \<Longrightarrow> b ~= 0
+lemma mod_mult_cong_nat: "(a::nat) ~= 0 \<Longrightarrow> b ~= 0
\<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)"
by (simp add: cong_nat_def mod_mult2_eq mod_add_left_eq)
@@ -548,43 +529,43 @@
apply (simp add: cong_altdef_int)
apply (subst dvd_minus_iff [symmetric])
apply (simp add: field_simps)
-done
+ done
lemma cong_modulus_neg_int: "([(a::int) = b] (mod m)) = ([a = b] (mod -m))"
by (auto simp add: cong_altdef_int)
-lemma mod_mult_cong_int: "(a::int) ~= 0 \<Longrightarrow> b ~= 0
+lemma mod_mult_cong_int: "(a::int) ~= 0 \<Longrightarrow> b ~= 0
\<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)"
- apply (case_tac "b > 0")
+ apply (cases "b > 0")
apply (simp add: cong_int_def mod_mod_cancel mod_add_left_eq)
apply (subst (1 2) cong_modulus_neg_int)
apply (unfold cong_int_def)
apply (subgoal_tac "a * b = (-a * -b)")
apply (erule ssubst)
apply (subst zmod_zmult2_eq)
- apply (auto simp add: mod_add_left_eq)
-done
+ apply (auto simp add: mod_add_left_eq)
+ done
lemma cong_to_1_nat: "([(a::nat) = 1] (mod n)) \<Longrightarrow> (n dvd (a - 1))"
- apply (case_tac "a = 0")
+ apply (cases "a = 0")
apply force
apply (subst (asm) cong_altdef_nat)
apply auto
-done
+ done
lemma cong_0_1_nat: "[(0::nat) = 1] (mod n) = (n = 1)"
- by (unfold cong_nat_def, auto)
+ unfolding cong_nat_def by auto
lemma cong_0_1_int: "[(0::int) = 1] (mod n) = ((n = 1) | (n = -1))"
- by (unfold cong_int_def, auto simp add: zmult_eq_1_iff)
+ unfolding cong_int_def by (auto simp add: zmult_eq_1_iff)
-lemma cong_to_1'_nat: "[(a::nat) = 1] (mod n) \<longleftrightarrow>
+lemma cong_to_1'_nat: "[(a::nat) = 1] (mod n) \<longleftrightarrow>
a = 0 \<and> n = 1 \<or> (\<exists>m. a = 1 + m * n)"
- apply (case_tac "n = 1")
+ apply (cases "n = 1")
apply auto [1]
apply (drule_tac x = "a - 1" in spec)
apply force
- apply (case_tac "a = 0")
+ apply (cases "a = 0")
apply (auto simp add: cong_0_1_nat) [1]
apply (rule iffI)
apply (drule cong_to_1_nat)
@@ -594,7 +575,7 @@
apply (auto simp add: field_simps) [1]
apply (subst cong_altdef_nat)
apply (auto simp add: dvd_def)
-done
+ done
lemma cong_le_nat: "(y::nat) <= x \<Longrightarrow> [x = y] (mod n) \<longleftrightarrow> (\<exists>q. x = q * n + y)"
apply (subst cong_altdef_nat)
@@ -602,10 +583,10 @@
apply (unfold dvd_def, auto simp add: field_simps)
apply (rule_tac x = k in exI)
apply auto
-done
+ done
lemma cong_solve_nat: "(a::nat) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)"
- apply (case_tac "n = 0")
+ apply (cases "n = 0")
apply force
apply (frule bezout_nat [of a n], auto)
apply (rule exI, erule ssubst)
@@ -617,11 +598,11 @@
apply simp
apply (rule cong_refl_nat)
apply (rule cong_refl_nat)
-done
+ done
lemma cong_solve_int: "(a::int) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)"
- apply (case_tac "n = 0")
- apply (case_tac "a \<ge> 0")
+ apply (cases "n = 0")
+ apply (cases "a \<ge> 0")
apply auto
apply (rule_tac x = "-1" in exI)
apply auto
@@ -637,16 +618,15 @@
apply simp
apply (subst mult_commute)
apply (rule cong_refl_int)
-done
-
-lemma cong_solve_dvd_nat:
+ done
+
+lemma cong_solve_dvd_nat:
assumes a: "(a::nat) \<noteq> 0" and b: "gcd a n dvd d"
shows "EX x. [a * x = d] (mod n)"
proof -
- from cong_solve_nat [OF a] obtain x where
- "[a * x = gcd a n](mod n)"
+ from cong_solve_nat [OF a] obtain x where "[a * x = gcd a n](mod n)"
by auto
- hence "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)"
+ then have "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)"
by (elim cong_scalar2_nat)
also from b have "(d div gcd a n) * gcd a n = d"
by (rule dvd_div_mult_self)
@@ -656,14 +636,13 @@
by auto
qed
-lemma cong_solve_dvd_int:
+lemma cong_solve_dvd_int:
assumes a: "(a::int) \<noteq> 0" and b: "gcd a n dvd d"
shows "EX x. [a * x = d] (mod n)"
proof -
- from cong_solve_int [OF a] obtain x where
- "[a * x = gcd a n](mod n)"
+ from cong_solve_int [OF a] obtain x where "[a * x = gcd a n](mod n)"
by auto
- hence "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)"
+ then have "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)"
by (elim cong_scalar2_int)
also from b have "(d div gcd a n) * gcd a n = d"
by (rule dvd_div_mult_self)
@@ -673,56 +652,52 @@
by auto
qed
-lemma cong_solve_coprime_nat: "coprime (a::nat) n \<Longrightarrow>
- EX x. [a * x = 1] (mod n)"
- apply (case_tac "a = 0")
+lemma cong_solve_coprime_nat: "coprime (a::nat) n \<Longrightarrow> EX x. [a * x = 1] (mod n)"
+ apply (cases "a = 0")
apply force
apply (frule cong_solve_nat [of a n])
apply auto
-done
+ done
-lemma cong_solve_coprime_int: "coprime (a::int) n \<Longrightarrow>
- EX x. [a * x = 1] (mod n)"
- apply (case_tac "a = 0")
+lemma cong_solve_coprime_int: "coprime (a::int) n \<Longrightarrow> EX x. [a * x = 1] (mod n)"
+ apply (cases "a = 0")
apply auto
- apply (case_tac "n \<ge> 0")
+ apply (cases "n \<ge> 0")
apply auto
apply (subst cong_int_def, auto)
apply (frule cong_solve_int [of a n])
apply auto
-done
+ done
-lemma coprime_iff_invertible_nat: "m > (1::nat) \<Longrightarrow> coprime a m =
- (EX x. [a * x = 1] (mod m))"
+lemma coprime_iff_invertible_nat: "m > (1::nat) \<Longrightarrow> coprime a m = (EX x. [a * x = 1] (mod m))"
apply (auto intro: cong_solve_coprime_nat)
apply (unfold cong_nat_def, auto intro: invertible_coprime_nat)
-done
+ done
-lemma coprime_iff_invertible_int: "m > (1::int) \<Longrightarrow> coprime a m =
- (EX x. [a * x = 1] (mod m))"
+lemma coprime_iff_invertible_int: "m > (1::int) \<Longrightarrow> coprime a m = (EX x. [a * x = 1] (mod m))"
apply (auto intro: cong_solve_coprime_int)
apply (unfold cong_int_def)
apply (auto intro: invertible_coprime_int)
-done
+ done
-lemma coprime_iff_invertible'_int: "m > (1::int) \<Longrightarrow> coprime a m =
+lemma coprime_iff_invertible'_int: "m > (1::int) \<Longrightarrow> coprime a m =
(EX x. 0 <= x & x < m & [a * x = 1] (mod m))"
apply (subst coprime_iff_invertible_int)
apply auto
apply (auto simp add: cong_int_def)
apply (rule_tac x = "x mod m" in exI)
apply (auto simp add: mod_mult_right_eq [symmetric])
-done
+ done
lemma cong_cong_lcm_nat: "[(x::nat) = y] (mod a) \<Longrightarrow>
[x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
- apply (case_tac "y \<le> x")
+ apply (cases "y \<le> x")
apply (auto simp add: cong_altdef_nat lcm_least_nat) [1]
apply (rule cong_sym_nat)
apply (subst (asm) (1 2) cong_sym_eq_nat)
apply (auto simp add: cong_altdef_nat lcm_least_nat)
-done
+ done
lemma cong_cong_lcm_int: "[(x::int) = y] (mod a) \<Longrightarrow>
[x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
@@ -730,15 +705,17 @@
lemma cong_cong_coprime_nat: "coprime a b \<Longrightarrow> [(x::nat) = y] (mod a) \<Longrightarrow>
[x = y] (mod b) \<Longrightarrow> [x = y] (mod a * b)"
- apply (frule (1) cong_cong_lcm_nat)back
+ apply (frule (1) cong_cong_lcm_nat)
+ back
apply (simp add: lcm_nat_def)
-done
+ done
lemma cong_cong_coprime_int: "coprime a b \<Longrightarrow> [(x::int) = y] (mod a) \<Longrightarrow>
[x = y] (mod b) \<Longrightarrow> [x = y] (mod a * b)"
- apply (frule (1) cong_cong_lcm_int)back
+ apply (frule (1) cong_cong_lcm_int)
+ back
apply (simp add: lcm_altdef_int cong_abs_int abs_mult [symmetric])
-done
+ done
lemma cong_cong_setprod_coprime_nat [rule_format]: "finite A \<Longrightarrow>
(ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
@@ -750,7 +727,7 @@
apply (subst gcd_commute_nat)
apply (rule setprod_coprime_nat)
apply auto
-done
+ done
lemma cong_cong_setprod_coprime_int [rule_format]: "finite A \<Longrightarrow>
(ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
@@ -762,20 +739,18 @@
apply (subst gcd_commute_int)
apply (rule setprod_coprime_int)
apply auto
-done
+ done
-lemma binary_chinese_remainder_aux_nat:
+lemma binary_chinese_remainder_aux_nat:
assumes a: "coprime (m1::nat) m2"
shows "EX b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and>
[b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)"
proof -
- from cong_solve_coprime_nat [OF a]
- obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
+ from cong_solve_coprime_nat [OF a] obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
by auto
- from a have b: "coprime m2 m1"
+ from a have b: "coprime m2 m1"
by (subst gcd_commute_nat)
- from cong_solve_coprime_nat [OF b]
- obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
+ from cong_solve_coprime_nat [OF b] obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
by auto
have "[m1 * x1 = 0] (mod m1)"
by (subst mult_commute, rule cong_mult_self_nat)
@@ -785,18 +760,16 @@
ultimately show ?thesis by blast
qed
-lemma binary_chinese_remainder_aux_int:
+lemma binary_chinese_remainder_aux_int:
assumes a: "coprime (m1::int) m2"
shows "EX b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and>
[b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)"
proof -
- from cong_solve_coprime_int [OF a]
- obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
+ from cong_solve_coprime_int [OF a] obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
by auto
- from a have b: "coprime m2 m1"
+ from a have b: "coprime m2 m1"
by (subst gcd_commute_int)
- from cong_solve_coprime_int [OF b]
- obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
+ from cong_solve_coprime_int [OF b] obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
by auto
have "[m1 * x1 = 0] (mod m1)"
by (subst mult_commute, rule cong_mult_self_int)
@@ -811,8 +784,8 @@
shows "EX x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
proof -
from binary_chinese_remainder_aux_nat [OF a] obtain b1 b2
- where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and
- "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)"
+ where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and
+ "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)"
by blast
let ?x = "u1 * b1 + u2 * b2"
have "[?x = u1 * 1 + u2 * 0] (mod m1)"
@@ -822,7 +795,7 @@
apply (rule cong_scalar2_nat)
apply (rule `[b2 = 0] (mod m1)`)
done
- hence "[?x = u1] (mod m1)" by simp
+ then have "[?x = u1] (mod m1)" by simp
have "[?x = u1 * 0 + u2 * 1] (mod m2)"
apply (rule cong_add_nat)
apply (rule cong_scalar2_nat)
@@ -830,7 +803,7 @@
apply (rule cong_scalar2_nat)
apply (rule `[b2 = 1] (mod m2)`)
done
- hence "[?x = u2] (mod m2)" by simp
+ then have "[?x = u2] (mod m2)" by simp
with `[?x = u1] (mod m1)` show ?thesis by blast
qed
@@ -850,7 +823,7 @@
apply (rule cong_scalar2_int)
apply (rule `[b2 = 0] (mod m1)`)
done
- hence "[?x = u1] (mod m1)" by simp
+ then have "[?x = u1] (mod m1)" by simp
have "[?x = u1 * 0 + u2 * 1] (mod m2)"
apply (rule cong_add_int)
apply (rule cong_scalar2_int)
@@ -858,42 +831,42 @@
apply (rule cong_scalar2_int)
apply (rule `[b2 = 1] (mod m2)`)
done
- hence "[?x = u2] (mod m2)" by simp
+ then have "[?x = u2] (mod m2)" by simp
with `[?x = u1] (mod m1)` show ?thesis by blast
qed
-lemma cong_modulus_mult_nat: "[(x::nat) = y] (mod m * n) \<Longrightarrow>
+lemma cong_modulus_mult_nat: "[(x::nat) = y] (mod m * n) \<Longrightarrow>
[x = y] (mod m)"
- apply (case_tac "y \<le> x")
+ apply (cases "y \<le> x")
apply (simp add: cong_altdef_nat)
apply (erule dvd_mult_left)
apply (rule cong_sym_nat)
apply (subst (asm) cong_sym_eq_nat)
- apply (simp add: cong_altdef_nat)
+ apply (simp add: cong_altdef_nat)
apply (erule dvd_mult_left)
-done
+ done
-lemma cong_modulus_mult_int: "[(x::int) = y] (mod m * n) \<Longrightarrow>
+lemma cong_modulus_mult_int: "[(x::int) = y] (mod m * n) \<Longrightarrow>
[x = y] (mod m)"
- apply (simp add: cong_altdef_int)
+ apply (simp add: cong_altdef_int)
apply (erule dvd_mult_left)
-done
+ done
-lemma cong_less_modulus_unique_nat:
+lemma cong_less_modulus_unique_nat:
"[(x::nat) = y] (mod m) \<Longrightarrow> x < m \<Longrightarrow> y < m \<Longrightarrow> x = y"
by (simp add: cong_nat_def)
lemma binary_chinese_remainder_unique_nat:
- assumes a: "coprime (m1::nat) m2" and
- nz: "m1 \<noteq> 0" "m2 \<noteq> 0"
+ assumes a: "coprime (m1::nat) m2"
+ and nz: "m1 \<noteq> 0" "m2 \<noteq> 0"
shows "EX! x. x < m1 * m2 \<and> [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
proof -
- from binary_chinese_remainder_nat [OF a] obtain y where
+ from binary_chinese_remainder_nat [OF a] obtain y where
"[y = u1] (mod m1)" and "[y = u2] (mod m2)"
by blast
let ?x = "y mod (m1 * m2)"
from nz have less: "?x < m1 * m2"
- by auto
+ by auto
have one: "[?x = u1] (mod m1)"
apply (rule cong_trans_nat)
prefer 2
@@ -911,9 +884,8 @@
apply (rule cong_mod_nat)
using nz apply auto
done
- have "ALL z. z < m1 * m2 \<and> [z = u1] (mod m1) \<and> [z = u2] (mod m2) \<longrightarrow>
- z = ?x"
- proof (clarify)
+ have "ALL z. z < m1 * m2 \<and> [z = u1] (mod m1) \<and> [z = u2] (mod m2) \<longrightarrow> z = ?x"
+ proof clarify
fix z
assume "z < m1 * m2"
assume "[z = u1] (mod m1)" and "[z = u2] (mod m2)"
@@ -935,46 +907,43 @@
apply (intro cong_less_modulus_unique_nat)
apply (auto, erule cong_sym_nat)
done
- qed
- with less one two show ?thesis
- by auto
+ qed
+ with less one two show ?thesis by auto
qed
lemma chinese_remainder_aux_nat:
- fixes A :: "'a set" and
- m :: "'a \<Rightarrow> nat"
- assumes fin: "finite A" and
- cop: "ALL i : A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
- shows "EX b. (ALL i : A.
- [b i = 1] (mod m i) \<and> [b i = 0] (mod (PROD j : A - {i}. m j)))"
+ fixes A :: "'a set"
+ and m :: "'a \<Rightarrow> nat"
+ assumes fin: "finite A"
+ and cop: "ALL i : A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
+ shows "EX b. (ALL i : A. [b i = 1] (mod m i) \<and> [b i = 0] (mod (PROD j : A - {i}. m j)))"
proof (rule finite_set_choice, rule fin, rule ballI)
fix i
assume "i : A"
with cop have "coprime (PROD j : A - {i}. m j) (m i)"
by (intro setprod_coprime_nat, auto)
- hence "EX x. [(PROD j : A - {i}. m j) * x = 1] (mod m i)"
+ then have "EX x. [(PROD j : A - {i}. m j) * x = 1] (mod m i)"
by (elim cong_solve_coprime_nat)
then obtain x where "[(PROD j : A - {i}. m j) * x = 1] (mod m i)"
by auto
- moreover have "[(PROD j : A - {i}. m j) * x = 0]
+ moreover have "[(PROD j : A - {i}. m j) * x = 0]
(mod (PROD j : A - {i}. m j))"
by (subst mult_commute, rule cong_mult_self_nat)
- ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0]
+ ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0]
(mod setprod m (A - {i}))"
by blast
qed
lemma chinese_remainder_nat:
- fixes A :: "'a set" and
- m :: "'a \<Rightarrow> nat" and
- u :: "'a \<Rightarrow> nat"
- assumes
- fin: "finite A" and
- cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
+ fixes A :: "'a set"
+ and m :: "'a \<Rightarrow> nat"
+ and u :: "'a \<Rightarrow> nat"
+ assumes fin: "finite A"
+ and cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
shows "EX x. (ALL i:A. [x = u i] (mod m i))"
proof -
from chinese_remainder_aux_nat [OF fin cop] obtain b where
- bprop: "ALL i:A. [b i = 1] (mod m i) \<and>
+ bprop: "ALL i:A. [b i = 1] (mod m i) \<and>
[b i = 0] (mod (PROD j : A - {i}. m j))"
by blast
let ?x = "SUM i:A. (u i) * (b i)"
@@ -982,12 +951,12 @@
proof (rule exI, clarify)
fix i
assume a: "i : A"
- show "[?x = u i] (mod m i)"
+ show "[?x = u i] (mod m i)"
proof -
- from fin a have "?x = (SUM j:{i}. u j * b j) +
+ from fin a have "?x = (SUM j:{i}. u j * b j) +
(SUM j:A-{i}. u j * b j)"
by (subst setsum_Un_disjoint [symmetric], auto intro: setsum_cong)
- hence "[?x = u i * b i + (SUM j:A-{i}. u j * b j)] (mod m i)"
+ then have "[?x = u i * b i + (SUM j:A-{i}. u j * b j)] (mod m i)"
by auto
also have "[u i * b i + (SUM j:A-{i}. u j * b j) =
u i * 1 + (SUM j:A-{i}. u j * 0)] (mod m i)"
@@ -1010,35 +979,34 @@
qed
qed
-lemma coprime_cong_prod_nat [rule_format]: "finite A \<Longrightarrow>
+lemma coprime_cong_prod_nat [rule_format]: "finite A \<Longrightarrow>
(ALL i: A. (ALL j: A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
(ALL i: A. [(x::nat) = y] (mod m i)) \<longrightarrow>
- [x = y] (mod (PROD i:A. m i))"
+ [x = y] (mod (PROD i:A. m i))"
apply (induct set: finite)
apply auto
apply (erule (1) coprime_cong_mult_nat)
apply (subst gcd_commute_nat)
apply (rule setprod_coprime_nat)
apply auto
-done
+ done
lemma chinese_remainder_unique_nat:
- fixes A :: "'a set" and
- m :: "'a \<Rightarrow> nat" and
- u :: "'a \<Rightarrow> nat"
- assumes
- fin: "finite A" and
- nz: "ALL i:A. m i \<noteq> 0" and
- cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
+ fixes A :: "'a set"
+ and m :: "'a \<Rightarrow> nat"
+ and u :: "'a \<Rightarrow> nat"
+ assumes fin: "finite A"
+ and nz: "ALL i:A. m i \<noteq> 0"
+ and cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
shows "EX! x. x < (PROD i:A. m i) \<and> (ALL i:A. [x = u i] (mod m i))"
proof -
- from chinese_remainder_nat [OF fin cop] obtain y where
- one: "(ALL i:A. [y = u i] (mod m i))"
+ from chinese_remainder_nat [OF fin cop]
+ obtain y where one: "(ALL i:A. [y = u i] (mod m i))"
by blast
let ?x = "y mod (PROD i:A. m i)"
from fin nz have prodnz: "(PROD i:A. m i) \<noteq> 0"
by auto
- hence less: "?x < (PROD i:A. m i)"
+ then have less: "?x < (PROD i:A. m i)"
by auto
have cong: "ALL i:A. [?x = u i] (mod m i)"
apply auto
@@ -1052,28 +1020,29 @@
apply (rule fin)
apply assumption
done
- have unique: "ALL z. z < (PROD i:A. m i) \<and>
+ have unique: "ALL z. z < (PROD i:A. m i) \<and>
(ALL i:A. [z = u i] (mod m i)) \<longrightarrow> z = ?x"
proof (clarify)
fix z
assume zless: "z < (PROD i:A. m i)"
assume zcong: "(ALL i:A. [z = u i] (mod m i))"
have "ALL i:A. [?x = z] (mod m i)"
- apply clarify
+ apply clarify
apply (rule cong_trans_nat)
using cong apply (erule bspec)
apply (rule cong_sym_nat)
using zcong apply auto
done
with fin cop have "[?x = z] (mod (PROD i:A. m i))"
- by (intro coprime_cong_prod_nat, auto)
+ apply (intro coprime_cong_prod_nat)
+ apply auto
+ done
with zless less show "z = ?x"
apply (intro cong_less_modulus_unique_nat)
apply (auto, erule cong_sym_nat)
done
- qed
- from less cong unique show ?thesis
- by blast
+ qed
+ from less cong unique show ?thesis by blast
qed
end
--- a/src/HOL/Number_Theory/Fib.thy Sat Sep 10 22:11:55 2011 +0200
+++ b/src/HOL/Number_Theory/Fib.thy Sat Sep 10 23:27:32 2011 +0200
@@ -18,48 +18,40 @@
subsection {* Main definitions *}
class fib =
-
-fixes
- fib :: "'a \<Rightarrow> 'a"
+ fixes fib :: "'a \<Rightarrow> 'a"
(* definition for the natural numbers *)
instantiation nat :: fib
-
-begin
+begin
-fun
- fib_nat :: "nat \<Rightarrow> nat"
+fun fib_nat :: "nat \<Rightarrow> nat"
where
"fib_nat n =
(if n = 0 then 0 else
(if n = 1 then 1 else
fib (n - 1) + fib (n - 2)))"
-instance proof qed
+instance ..
end
(* definition for the integers *)
instantiation int :: fib
-
-begin
+begin
-definition
- fib_int :: "int \<Rightarrow> int"
-where
- "fib_int n = (if n >= 0 then int (fib (nat n)) else 0)"
+definition fib_int :: "int \<Rightarrow> int"
+ where "fib_int n = (if n >= 0 then int (fib (nat n)) else 0)"
-instance proof qed
+instance ..
end
subsection {* Set up Transfer *}
-
lemma transfer_nat_int_fib:
"(x::int) >= 0 \<Longrightarrow> fib (nat x) = nat (fib x)"
unfolding fib_int_def by auto
@@ -68,18 +60,16 @@
"n >= (0::int) \<Longrightarrow> fib n >= 0"
by (auto simp add: fib_int_def)
-declare transfer_morphism_nat_int[transfer add return:
+declare transfer_morphism_nat_int[transfer add return:
transfer_nat_int_fib transfer_nat_int_fib_closure]
-lemma transfer_int_nat_fib:
- "fib (int n) = int (fib n)"
+lemma transfer_int_nat_fib: "fib (int n) = int (fib n)"
unfolding fib_int_def by auto
-lemma transfer_int_nat_fib_closure:
- "is_nat n \<Longrightarrow> fib n >= 0"
+lemma transfer_int_nat_fib_closure: "is_nat n \<Longrightarrow> fib n >= 0"
unfolding fib_int_def by auto
-declare transfer_morphism_int_nat[transfer add return:
+declare transfer_morphism_int_nat[transfer add return:
transfer_int_nat_fib transfer_int_nat_fib_closure]
@@ -123,7 +113,7 @@
(* the need for One_nat_def is due to the natdiff_cancel_numerals
procedure *)
-lemma fib_induct_nat: "P (0::nat) \<Longrightarrow> P (1::nat) \<Longrightarrow>
+lemma fib_induct_nat: "P (0::nat) \<Longrightarrow> P (1::nat) \<Longrightarrow>
(!!n. P n \<Longrightarrow> P (n + 1) \<Longrightarrow> P (n + 2)) \<Longrightarrow> P n"
apply (atomize, induct n rule: nat_less_induct)
apply auto
@@ -137,7 +127,7 @@
apply (auto simp add: One_nat_def) (* again, natdiff_cancel *)
done
-lemma fib_add_nat: "fib ((n::nat) + k + 1) = fib (k + 1) * fib (n + 1) +
+lemma fib_add_nat: "fib ((n::nat) + k + 1) = fib (k + 1) * fib (n + 1) +
fib k * fib n"
apply (induct n rule: fib_induct_nat)
apply auto
@@ -148,26 +138,24 @@
(* hmmm. Why doesn't "n + (1 + (1 + k))" simplify to "n + k + 2"? *)
apply (subgoal_tac "n + (k + 2) = n + (1 + (1 + k))")
apply (erule ssubst) back back
- apply (erule ssubst) back
+ apply (erule ssubst) back
apply auto
done
-lemma fib_add'_nat: "fib (n + Suc k) = fib (Suc k) * fib (Suc n) +
- fib k * fib n"
+lemma fib_add'_nat: "fib (n + Suc k) =
+ fib (Suc k) * fib (Suc n) + fib k * fib n"
using fib_add_nat by (auto simp add: One_nat_def)
(* transfer from nats to ints *)
-lemma fib_add_int [rule_format]: "(n::int) >= 0 \<Longrightarrow> k >= 0 \<Longrightarrow>
- fib (n + k + 1) = fib (k + 1) * fib (n + 1) +
- fib k * fib n "
-
+lemma fib_add_int: "(n::int) >= 0 \<Longrightarrow> k >= 0 \<Longrightarrow>
+ fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n "
by (rule fib_add_nat [transferred])
lemma fib_neq_0_nat: "(n::nat) > 0 \<Longrightarrow> fib n ~= 0"
apply (induct n rule: fib_induct_nat)
apply (auto simp add: fib_plus_2_nat)
-done
+ done
lemma fib_gr_0_nat: "(n::nat) > 0 \<Longrightarrow> fib n > 0"
by (frule fib_neq_0_nat, simp)
@@ -180,21 +168,20 @@
much easier using integers, not natural numbers!
*}
-lemma fib_Cassini_aux_int: "fib (int n + 2) * fib (int n) -
+lemma fib_Cassini_aux_int: "fib (int n + 2) * fib (int n) -
(fib (int n + 1))^2 = (-1)^(n + 1)"
apply (induct n)
- apply (auto simp add: field_simps power2_eq_square fib_reduce_int
- power_add)
-done
+ apply (auto simp add: field_simps power2_eq_square fib_reduce_int power_add)
+ done
-lemma fib_Cassini_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n -
+lemma fib_Cassini_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n -
(fib (n + 1))^2 = (-1)^(nat n + 1)"
by (insert fib_Cassini_aux_int [of "nat n"], auto)
(*
-lemma fib_Cassini'_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n =
+lemma fib_Cassini'_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n =
(fib (n + 1))^2 + (-1)^(nat n + 1)"
- by (frule fib_Cassini_int, simp)
+ by (frule fib_Cassini_int, simp)
*)
lemma fib_Cassini'_int: "n >= 0 \<Longrightarrow> fib ((n::int) + 2) * fib n =
@@ -204,12 +191,11 @@
apply (subst tsub_eq)
apply (insert fib_gr_0_int [of "n + 1"], force)
apply auto
-done
+ done
lemma fib_Cassini_nat: "fib ((n::nat) + 2) * fib n =
- (if even n then (fib (n + 1))^2 - 1
- else (fib (n + 1))^2 + 1)"
-
+ (if even n then (fib (n + 1))^2 - 1
+ else (fib (n + 1))^2 + 1)"
by (rule fib_Cassini'_int [transferred, of n], auto)
@@ -222,13 +208,12 @@
apply (auto simp add: Suc_eq_plus1) (* again, natdiff_cancel *)
apply (subst add_commute, auto)
apply (subst gcd_commute_nat, auto simp add: field_simps)
-done
+ done
lemma coprime_fib_Suc_nat: "coprime (fib n) (fib (Suc n))"
using coprime_fib_plus_1_nat by (simp add: One_nat_def)
-lemma coprime_fib_plus_1_int:
- "n >= 0 \<Longrightarrow> coprime (fib (n::int)) (fib (n + 1))"
+lemma coprime_fib_plus_1_int: "n >= 0 \<Longrightarrow> coprime (fib (n::int)) (fib (n + 1))"
by (erule coprime_fib_plus_1_nat [transferred])
lemma gcd_fib_add_nat: "gcd (fib (m::nat)) (fib (n + m)) = gcd (fib m) (fib n)"
@@ -243,51 +228,53 @@
apply (subst gcd_commute_nat)
apply (rule gcd_mult_cancel_nat)
apply (rule coprime_fib_plus_1_nat)
-done
+ done
-lemma gcd_fib_add_int [rule_format]: "m >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow>
+lemma gcd_fib_add_int [rule_format]: "m >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow>
gcd (fib (m::int)) (fib (n + m)) = gcd (fib m) (fib n)"
by (erule gcd_fib_add_nat [transferred])
-lemma gcd_fib_diff_nat: "(m::nat) \<le> n \<Longrightarrow>
+lemma gcd_fib_diff_nat: "(m::nat) \<le> n \<Longrightarrow>
gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
by (simp add: gcd_fib_add_nat [symmetric, of _ "n-m"])
-lemma gcd_fib_diff_int: "0 <= (m::int) \<Longrightarrow> m \<le> n \<Longrightarrow>
+lemma gcd_fib_diff_int: "0 <= (m::int) \<Longrightarrow> m \<le> n \<Longrightarrow>
gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
by (simp add: gcd_fib_add_int [symmetric, of _ "n-m"])
-lemma gcd_fib_mod_nat: "0 < (m::nat) \<Longrightarrow>
+lemma gcd_fib_mod_nat: "0 < (m::nat) \<Longrightarrow>
gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
proof (induct n rule: less_induct)
case (less n)
from less.prems have pos_m: "0 < m" .
show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
proof (cases "m < n")
- case True note m_n = True
- then have m_n': "m \<le> n" by auto
+ case True
+ then have "m \<le> n" by auto
with pos_m have pos_n: "0 < n" by auto
- with pos_m m_n have diff: "n - m < n" by auto
+ with pos_m `m < n` have diff: "n - m < n" by auto
have "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib ((n - m) mod m))"
- by (simp add: mod_if [of n]) (insert m_n, auto)
- also have "\<dots> = gcd (fib m) (fib (n - m))"
+ by (simp add: mod_if [of n]) (insert `m < n`, auto)
+ also have "\<dots> = gcd (fib m) (fib (n - m))"
by (simp add: less.hyps diff pos_m)
- also have "\<dots> = gcd (fib m) (fib n)" by (simp add: gcd_fib_diff_nat m_n')
+ also have "\<dots> = gcd (fib m) (fib n)"
+ by (simp add: gcd_fib_diff_nat `m \<le> n`)
finally show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" .
next
- case False then show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
- by (cases "m = n") auto
+ case False
+ then show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
+ by (cases "m = n") auto
qed
qed
-lemma gcd_fib_mod_int:
+lemma gcd_fib_mod_int:
assumes "0 < (m::int)" and "0 <= n"
shows "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
apply (rule gcd_fib_mod_nat [transferred])
using assms apply auto
done
-lemma fib_gcd_nat: "fib (gcd (m::nat) n) = gcd (fib m) (fib n)"
+lemma fib_gcd_nat: "fib (gcd (m::nat) n) = gcd (fib m) (fib n)"
-- {* Law 6.111 *}
apply (induct m n rule: gcd_nat_induct)
apply (simp_all add: gcd_non_0_nat gcd_commute_nat gcd_fib_mod_nat)
@@ -297,7 +284,7 @@
fib (gcd (m::int) n) = gcd (fib m) (fib n)"
by (erule fib_gcd_nat [transferred])
-lemma atMost_plus_one_nat: "{..(k::nat) + 1} = insert (k + 1) {..k}"
+lemma atMost_plus_one_nat: "{..(k::nat) + 1} = insert (k + 1) {..k}"
by auto
theorem fib_mult_eq_setsum_nat:
--- a/src/HOL/Number_Theory/MiscAlgebra.thy Sat Sep 10 22:11:55 2011 +0200
+++ b/src/HOL/Number_Theory/MiscAlgebra.thy Sat Sep 10 23:27:32 2011 +0200
@@ -12,7 +12,7 @@
(* finiteness stuff *)
-lemma bounded_set1_int [intro]: "finite {(x::int). a < x & x < b & P x}"
+lemma bounded_set1_int [intro]: "finite {(x::int). a < x & x < b & P x}"
apply (subgoal_tac "{x. a < x & x < b & P x} <= {a<..<b}")
apply (erule finite_subset)
apply auto
@@ -64,7 +64,7 @@
apply auto
apply (rule_tac x = "inv x" in bexI)
apply auto
-done
+ done
lemma (in comm_monoid) units_comm_group: "comm_group(units_of G)"
apply (rule group.group_comm_groupI)
@@ -75,15 +75,15 @@
done
lemma units_of_carrier: "carrier (units_of G) = Units G"
- by (unfold units_of_def, auto)
+ unfolding units_of_def by auto
lemma units_of_mult: "mult(units_of G) = mult G"
- by (unfold units_of_def, auto)
+ unfolding units_of_def by auto
lemma units_of_one: "one(units_of G) = one G"
- by (unfold units_of_def, auto)
+ unfolding units_of_def by auto
-lemma (in monoid) units_of_inv: "x : Units G ==>
+lemma (in monoid) units_of_inv: "x : Units G ==>
m_inv (units_of G) x = m_inv G x"
apply (rule sym)
apply (subst m_inv_def)
@@ -105,12 +105,12 @@
apply (erule group.l_inv, assumption)
done
-lemma (in group) inj_on_const_mult: "a: (carrier G) ==>
+lemma (in group) inj_on_const_mult: "a: (carrier G) ==>
inj_on (%x. a \<otimes> x) (carrier G)"
- by (unfold inj_on_def, auto)
+ unfolding inj_on_def by auto
lemma (in group) surj_const_mult: "a : (carrier G) ==>
- (%x. a \<otimes> x) ` (carrier G) = (carrier G)"
+ (%x. a \<otimes> x) ` (carrier G) = (carrier G)"
apply (auto simp add: image_def)
apply (rule_tac x = "(m_inv G a) \<otimes> x" in bexI)
apply auto
@@ -118,7 +118,7 @@
for mult_ac rewriting. *)
apply (subst m_assoc [symmetric])
apply auto
-done
+ done
lemma (in group) l_cancel_one [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
(x \<otimes> a = x) = (a = one G)"
@@ -127,7 +127,7 @@
prefer 4
apply (erule ssubst)
apply auto
-done
+ done
lemma (in group) r_cancel_one [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
(a \<otimes> x = x) = (a = one G)"
@@ -136,28 +136,32 @@
prefer 4
apply (erule ssubst)
apply auto
-done
+ done
(* Is there a better way to do this? *)
lemma (in group) l_cancel_one' [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
(x = x \<otimes> a) = (a = one G)"
- by (subst eq_commute, simp)
+ apply (subst eq_commute)
+ apply simp
+ done
lemma (in group) r_cancel_one' [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
(x = a \<otimes> x) = (a = one G)"
- by (subst eq_commute, simp)
+ apply (subst eq_commute)
+ apply simp
+ done
(* This should be generalized to arbitrary groups, not just commutative
ones, using Lagrange's theorem. *)
lemma (in comm_group) power_order_eq_one:
- assumes fin [simp]: "finite (carrier G)"
- and a [simp]: "a : carrier G"
- shows "a (^) card(carrier G) = one G"
+ assumes fin [simp]: "finite (carrier G)"
+ and a [simp]: "a : carrier G"
+ shows "a (^) card(carrier G) = one G"
proof -
have "(\<Otimes>x:carrier G. x) = (\<Otimes>x:carrier G. a \<otimes> x)"
- by (subst (2) finprod_reindex [symmetric],
+ by (subst (2) finprod_reindex [symmetric],
auto simp add: Pi_def inj_on_const_mult surj_const_mult)
also have "\<dots> = (\<Otimes>x:carrier G. a) \<otimes> (\<Otimes>x:carrier G. x)"
by (auto simp add: finprod_multf Pi_def)
@@ -178,7 +182,7 @@
apply (rule trans)
apply (subgoal_tac "a = (a \<otimes> b) \<otimes> inv b")
apply assumption
- apply (subst m_assoc)
+ apply (subst m_assoc)
apply auto
apply (unfold Units_def)
apply auto
@@ -200,20 +204,20 @@
x \<otimes> y = \<one> \<Longrightarrow> inv x = y"
apply (rule inv_char)
apply auto
- apply (subst m_comm, auto)
+ apply (subst m_comm, auto)
done
-lemma (in ring) inv_neg_one [simp]: "inv (\<ominus> \<one>) = \<ominus> \<one>"
+lemma (in ring) inv_neg_one [simp]: "inv (\<ominus> \<one>) = \<ominus> \<one>"
apply (rule inv_char)
apply (auto simp add: l_minus r_minus)
done
-lemma (in monoid) inv_eq_imp_eq: "x : Units G \<Longrightarrow> y : Units G \<Longrightarrow>
+lemma (in monoid) inv_eq_imp_eq: "x : Units G \<Longrightarrow> y : Units G \<Longrightarrow>
inv x = inv y \<Longrightarrow> x = y"
apply (subgoal_tac "inv(inv x) = inv(inv y)")
apply (subst (asm) Units_inv_inv)+
apply auto
-done
+ done
lemma (in ring) Units_minus_one_closed [intro]: "\<ominus> \<one> : Units R"
apply (unfold Units_def)
@@ -221,24 +225,24 @@
apply (rule_tac x = "\<ominus> \<one>" in bexI)
apply auto
apply (simp add: l_minus r_minus)
-done
+ done
lemma (in monoid) inv_one [simp]: "inv \<one> = \<one>"
apply (rule inv_char)
apply auto
-done
+ done
lemma (in ring) inv_eq_neg_one_eq: "x : Units R \<Longrightarrow> (inv x = \<ominus> \<one>) = (x = \<ominus> \<one>)"
apply auto
apply (subst Units_inv_inv [symmetric])
apply auto
-done
+ done
lemma (in monoid) inv_eq_one_eq: "x : Units G \<Longrightarrow> (inv x = \<one>) = (x = \<one>)"
apply auto
apply (subst Units_inv_inv [symmetric])
apply auto
-done
+ done
(* This goes in FiniteProduct *)
@@ -256,29 +260,28 @@
apply (erule finite_UN_I)
apply blast
apply (fastsimp)
- apply (auto intro!: funcsetI finprod_closed)
-done
+ apply (auto intro!: funcsetI finprod_closed)
+ done
lemma (in comm_monoid) finprod_Union_disjoint:
"[| finite C; (ALL A:C. finite A & (ALL x:A. f x : carrier G));
- (ALL A:C. ALL B:C. A ~= B --> A Int B = {}) |]
- ==> finprod G f (Union C) = finprod G (finprod G f) C"
+ (ALL A:C. ALL B:C. A ~= B --> A Int B = {}) |]
+ ==> finprod G f (Union C) = finprod G (finprod G f) C"
apply (frule finprod_UN_disjoint [of C id f])
apply (auto simp add: SUP_def)
-done
+ done
-lemma (in comm_monoid) finprod_one [rule_format]:
- "finite A \<Longrightarrow> (ALL x:A. f x = \<one>) \<longrightarrow>
- finprod G f A = \<one>"
-by (induct set: finite) auto
+lemma (in comm_monoid) finprod_one:
+ "finite A \<Longrightarrow> (\<And>x. x:A \<Longrightarrow> f x = \<one>) \<Longrightarrow> finprod G f A = \<one>"
+ by (induct set: finite) auto
(* need better simplification rules for rings *)
(* the next one holds more generally for abelian groups *)
lemma (in cring) sum_zero_eq_neg:
- "x : carrier R \<Longrightarrow> y : carrier R \<Longrightarrow> x \<oplus> y = \<zero> \<Longrightarrow> x = \<ominus> y"
- apply (subgoal_tac "\<ominus> y = \<zero> \<oplus> \<ominus> y")
+ "x : carrier R \<Longrightarrow> y : carrier R \<Longrightarrow> x \<oplus> y = \<zero> \<Longrightarrow> x = \<ominus> y"
+ apply (subgoal_tac "\<ominus> y = \<zero> \<oplus> \<ominus> y")
apply (erule ssubst)back
apply (erule subst)
apply (simp_all add: ring_simprules)
@@ -287,7 +290,7 @@
(* there's a name conflict -- maybe "domain" should be
"integral_domain" *)
-lemma (in Ring.domain) square_eq_one:
+lemma (in Ring.domain) square_eq_one:
fixes x
assumes [simp]: "x : carrier R" and
"x \<otimes> x = \<one>"
@@ -298,15 +301,15 @@
also with `x \<otimes> x = \<one>` have "\<dots> = \<zero>"
by (simp add: ring_simprules)
finally have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = \<zero>" .
- hence "(x \<oplus> \<one>) = \<zero> | (x \<oplus> \<ominus> \<one>) = \<zero>"
+ then have "(x \<oplus> \<one>) = \<zero> | (x \<oplus> \<ominus> \<one>) = \<zero>"
by (intro integral, auto)
- thus ?thesis
+ then show ?thesis
apply auto
apply (erule notE)
apply (rule sum_zero_eq_neg)
apply auto
apply (subgoal_tac "x = \<ominus> (\<ominus> \<one>)")
- apply (simp add: ring_simprules)
+ apply (simp add: ring_simprules)
apply (rule sum_zero_eq_neg)
apply auto
done
@@ -318,7 +321,7 @@
apply auto
apply (erule ssubst)back
apply (erule Units_r_inv)
-done
+ done
(*
@@ -327,15 +330,15 @@
needed.)
*)
-lemma (in ring) finite_ring_finite_units [intro]: "finite (carrier R) \<Longrightarrow>
- finite (Units R)"
- by (rule finite_subset, auto)
+lemma (in ring) finite_ring_finite_units [intro]:
+ "finite (carrier R) \<Longrightarrow> finite (Units R)"
+ by (rule finite_subset) auto
(* this belongs with MiscAlgebra.thy *)
-lemma (in monoid) units_of_pow:
+lemma (in monoid) units_of_pow:
"x : Units G \<Longrightarrow> x (^)\<^bsub>units_of G\<^esub> (n::nat) = x (^)\<^bsub>G\<^esub> n"
apply (induct n)
- apply (auto simp add: units_group group.is_monoid
+ apply (auto simp add: units_group group.is_monoid
monoid.nat_pow_0 monoid.nat_pow_Suc units_of_one units_of_mult)
done
--- a/src/HOL/Number_Theory/Primes.thy Sat Sep 10 22:11:55 2011 +0200
+++ b/src/HOL/Number_Theory/Primes.thy Sat Sep 10 23:27:32 2011 +0200
@@ -31,54 +31,41 @@
imports "~~/src/HOL/GCD"
begin
-declare One_nat_def [simp del]
-
class prime = one +
-
-fixes
- prime :: "'a \<Rightarrow> bool"
+ fixes prime :: "'a \<Rightarrow> bool"
instantiation nat :: prime
-
begin
-definition
- prime_nat :: "nat \<Rightarrow> bool"
-where
- "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
+definition prime_nat :: "nat \<Rightarrow> bool"
+ where "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
-instance proof qed
+instance ..
end
instantiation int :: prime
-
begin
-definition
- prime_int :: "int \<Rightarrow> bool"
-where
- "prime_int p = prime (nat p)"
+definition prime_int :: "int \<Rightarrow> bool"
+ where "prime_int p = prime (nat p)"
-instance proof qed
+instance ..
end
subsection {* Set up Transfer *}
-
lemma transfer_nat_int_prime:
"(x::int) >= 0 \<Longrightarrow> prime (nat x) = prime x"
- unfolding gcd_int_def lcm_int_def prime_int_def
- by auto
+ unfolding gcd_int_def lcm_int_def prime_int_def by auto
declare transfer_morphism_nat_int[transfer add return:
transfer_nat_int_prime]
-lemma transfer_int_nat_prime:
- "prime (int x) = prime x"
- by (unfold gcd_int_def lcm_int_def prime_int_def, auto)
+lemma transfer_int_nat_prime: "prime (int x) = prime x"
+ unfolding gcd_int_def lcm_int_def prime_int_def by auto
declare transfer_morphism_int_nat[transfer add return:
transfer_int_nat_prime]
@@ -94,52 +81,54 @@
unfolding prime_int_def
apply (frule prime_odd_nat)
apply (auto simp add: even_nat_def)
-done
+ done
(* FIXME Is there a better way to handle these, rather than making them elim rules? *)
lemma prime_ge_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 0"
- by (unfold prime_nat_def, auto)
+ unfolding prime_nat_def by auto
lemma prime_gt_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 0"
- by (unfold prime_nat_def, auto)
+ unfolding prime_nat_def by auto
lemma prime_ge_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 1"
- by (unfold prime_nat_def, auto)
+ unfolding prime_nat_def by auto
lemma prime_gt_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 1"
- by (unfold prime_nat_def, auto)
+ unfolding prime_nat_def by auto
lemma prime_ge_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= Suc 0"
- by (unfold prime_nat_def, auto)
+ unfolding prime_nat_def by auto
lemma prime_gt_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > Suc 0"
- by (unfold prime_nat_def, auto)
+ unfolding prime_nat_def by auto
lemma prime_ge_2_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 2"
- by (unfold prime_nat_def, auto)
+ unfolding prime_nat_def by auto
lemma prime_ge_0_int [elim]: "prime (p::int) \<Longrightarrow> p >= 0"
- by (unfold prime_int_def prime_nat_def) auto
+ unfolding prime_int_def prime_nat_def by auto
lemma prime_gt_0_int [elim]: "prime (p::int) \<Longrightarrow> p > 0"
- by (unfold prime_int_def prime_nat_def, auto)
+ unfolding prime_int_def prime_nat_def by auto
lemma prime_ge_1_int [elim]: "prime (p::int) \<Longrightarrow> p >= 1"
- by (unfold prime_int_def prime_nat_def, auto)
+ unfolding prime_int_def prime_nat_def by auto
lemma prime_gt_1_int [elim]: "prime (p::int) \<Longrightarrow> p > 1"
- by (unfold prime_int_def prime_nat_def, auto)
+ unfolding prime_int_def prime_nat_def by auto
lemma prime_ge_2_int [elim]: "prime (p::int) \<Longrightarrow> p >= 2"
- by (unfold prime_int_def prime_nat_def, auto)
+ unfolding prime_int_def prime_nat_def by auto
lemma prime_int_altdef: "prime (p::int) = (1 < p \<and> (\<forall>m \<ge> 0. m dvd p \<longrightarrow>
m = 1 \<or> m = p))"
using prime_nat_def [transferred]
- apply (case_tac "p >= 0")
- by (blast, auto simp add: prime_ge_0_int)
+ apply (cases "p >= 0")
+ apply blast
+ apply (auto simp add: prime_ge_0_int)
+ done
lemma prime_imp_coprime_nat: "prime (p::nat) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
apply (unfold prime_nat_def)
@@ -168,26 +157,29 @@
lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
unfolding prime_nat_def dvd_def apply auto
- 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)
+ 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)
lemma not_prime_eq_prod_int: "(n::int) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
unfolding prime_int_altdef dvd_def
apply auto
- 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)
+ 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)
lemma prime_dvd_power_nat [rule_format]: "prime (p::nat) -->
n > 0 --> (p dvd x^n --> p dvd x)"
- by (induct n rule: nat_induct, auto)
+ by (induct n rule: nat_induct) auto
lemma prime_dvd_power_int [rule_format]: "prime (p::int) -->
n > 0 --> (p dvd x^n --> p dvd x)"
- apply (induct n rule: nat_induct, auto)
+ apply (induct n rule: nat_induct)
+ apply auto
apply (frule prime_ge_0_int)
apply auto
-done
+ done
-subsubsection{* Make prime naively executable *}
+subsubsection {* Make prime naively executable *}
lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
by (simp add: prime_nat_def)
@@ -205,89 +197,87 @@
by (simp add: prime_int_def)
lemma prime_nat_code [code]:
- "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
-apply (simp add: Ball_def)
-apply (metis less_not_refl prime_nat_def dvd_triv_right not_prime_eq_prod_nat)
-done
+ "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
+ apply (simp add: Ball_def)
+ apply (metis less_not_refl prime_nat_def dvd_triv_right not_prime_eq_prod_nat)
+ done
lemma prime_nat_simp:
- "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
-by (auto simp add: prime_nat_code)
+ "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
+ by (auto simp add: prime_nat_code)
lemmas prime_nat_simp_number_of [simp] = prime_nat_simp [of "number_of m", standard]
lemma prime_int_code [code]:
"prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?L = ?R")
proof
- assume "?L" thus "?R"
+ assume "?L"
+ then show "?R"
by (clarsimp simp: prime_gt_1_int) (metis int_one_le_iff_zero_less prime_int_altdef less_le)
next
- assume "?R" thus "?L" by (clarsimp simp:Ball_def) (metis dvdI not_prime_eq_prod_int)
+ assume "?R"
+ then show "?L" by (clarsimp simp: Ball_def) (metis dvdI not_prime_eq_prod_int)
qed
-lemma prime_int_simp:
- "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..p - 1]. ~ n dvd p)"
-by (auto simp add: prime_int_code)
+lemma prime_int_simp: "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..p - 1]. ~ n dvd p)"
+ by (auto simp add: prime_int_code)
lemmas prime_int_simp_number_of [simp] = prime_int_simp [of "number_of m", standard]
lemma two_is_prime_nat [simp]: "prime (2::nat)"
-by simp
+ by simp
lemma two_is_prime_int [simp]: "prime (2::int)"
-by simp
+ by simp
text{* A bit of regression testing: *}
-lemma "prime(97::nat)"
-by simp
-
-lemma "prime(97::int)"
-by simp
-
-lemma "prime(997::nat)"
-by eval
-
-lemma "prime(997::int)"
-by eval
+lemma "prime(97::nat)" by simp
+lemma "prime(97::int)" by simp
+lemma "prime(997::nat)" by eval
+lemma "prime(997::int)" by eval
lemma prime_imp_power_coprime_nat: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
apply (rule coprime_exp_nat)
apply (subst gcd_commute_nat)
apply (erule (1) prime_imp_coprime_nat)
-done
+ done
lemma prime_imp_power_coprime_int: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
apply (rule coprime_exp_int)
apply (subst gcd_commute_int)
apply (erule (1) prime_imp_coprime_int)
-done
+ done
lemma primes_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
apply (rule prime_imp_coprime_nat, assumption)
- apply (unfold prime_nat_def, auto)
-done
+ apply (unfold prime_nat_def)
+ apply auto
+ done
lemma primes_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
apply (rule prime_imp_coprime_int, assumption)
apply (unfold prime_int_altdef)
apply (metis int_one_le_iff_zero_less less_le)
-done
+ done
-lemma primes_imp_powers_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
+lemma primes_imp_powers_coprime_nat:
+ "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
by (rule coprime_exp2_nat, rule primes_coprime_nat)
-lemma primes_imp_powers_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
+lemma primes_imp_powers_coprime_int:
+ "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
by (rule coprime_exp2_int, rule primes_coprime_int)
lemma prime_factor_nat: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n"
apply (induct n rule: nat_less_induct)
apply (case_tac "n = 0")
- using two_is_prime_nat apply blast
- apply (metis One_nat_def dvd.order_trans dvd_refl less_Suc0 linorder_neqE_nat nat_dvd_not_less
- neq0_conv prime_nat_def)
-done
+ using two_is_prime_nat
+ apply blast
+ apply (metis One_nat_def dvd.order_trans dvd_refl less_Suc0 linorder_neqE_nat
+ nat_dvd_not_less neq0_conv prime_nat_def)
+ done
(* An Isar version:
@@ -301,7 +291,7 @@
fix n :: nat
assume "n ~= 1" and
ih: "\<forall>m<n. m \<noteq> 1 \<longrightarrow> (\<exists>p. prime p \<and> p dvd m)"
- thus "\<exists>p. prime p \<and> p dvd n"
+ then show "\<exists>p. prime p \<and> p dvd n"
proof -
{
assume "n = 0"
@@ -312,7 +302,7 @@
moreover
{
assume "prime n"
- hence ?thesis by auto
+ then have ?thesis by auto
}
moreover
{
@@ -335,13 +325,14 @@
assumes p: "prime (p::nat)" and ab: "coprime a b" and pab: "p^n dvd a * b"
shows "p^n dvd a \<or> p^n dvd b"
proof-
- {assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis
+ { assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis
apply (cases "n=0", simp_all)
- apply (cases "a=1", simp_all) done}
+ apply (cases "a=1", simp_all)
+ done }
moreover
- {assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1"
- then obtain m where m: "n = Suc m" by (cases n, auto)
- from n have "p dvd p^n" by (intro dvd_power, auto)
+ { assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1"
+ then obtain m where m: "n = Suc m" by (cases n) auto
+ from n have "p dvd p^n" apply (intro dvd_power) apply auto done
also note pab
finally have pab': "p dvd a * b".
from prime_dvd_mult_nat[OF p pab']
@@ -351,7 +342,7 @@
from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto
with p have "coprime b p"
by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
- hence pnb: "coprime (p^n) b"
+ then have pnb: "coprime (p^n) b"
by (subst gcd_commute_nat, rule coprime_exp_nat)
from coprime_dvd_mult_nat[OF pnb pab] have ?thesis by blast }
moreover
@@ -361,39 +352,39 @@
by auto
with p have "coprime a p"
by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
- hence pna: "coprime (p^n) a"
+ then have pna: "coprime (p^n) a"
by (subst gcd_commute_nat, rule coprime_exp_nat)
from coprime_dvd_mult_nat[OF pna pnba] have ?thesis by blast }
- ultimately have ?thesis by blast}
+ ultimately have ?thesis by blast }
ultimately show ?thesis by blast
qed
+
subsection {* Infinitely many primes *}
lemma next_prime_bound: "\<exists>(p::nat). prime p \<and> n < p \<and> p <= fact n + 1"
proof-
have f1: "fact n + 1 \<noteq> 1" using fact_ge_one_nat [of n] by arith
from prime_factor_nat [OF f1]
- obtain p where "prime p" and "p dvd fact n + 1" by auto
- hence "p \<le> fact n + 1"
- by (intro dvd_imp_le, auto)
- {assume "p \<le> n"
+ obtain p where "prime p" and "p dvd fact n + 1" by auto
+ then have "p \<le> fact n + 1" apply (intro dvd_imp_le) apply auto done
+ { assume "p \<le> n"
from `prime p` have "p \<ge> 1"
by (cases p, simp_all)
with `p <= n` have "p dvd fact n"
by (intro dvd_fact_nat)
with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n"
by (rule dvd_diff_nat)
- hence "p dvd 1" by simp
- hence "p <= 1" by auto
+ then have "p dvd 1" by simp
+ then have "p <= 1" by auto
moreover from `prime p` have "p > 1" by auto
ultimately have False by auto}
- hence "n < p" by arith
+ then have "n < p" by presburger
with `prime p` and `p <= fact n + 1` show ?thesis by auto
qed
lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)"
-using next_prime_bound by auto
+ using next_prime_bound by auto
lemma primes_infinite: "\<not> (finite {(p::nat). prime p})"
proof
@@ -402,8 +393,8 @@
by auto
then obtain b where "ALL (x::nat). prime x \<longrightarrow> x <= b"
by auto
- with bigger_prime [of b] show False by auto
+ with bigger_prime [of b] show False
+ by auto
qed
-
end
--- a/src/HOL/Number_Theory/Residues.thy Sat Sep 10 22:11:55 2011 +0200
+++ b/src/HOL/Number_Theory/Residues.thy Sat Sep 10 23:27:32 2011 +0200
@@ -16,14 +16,14 @@
(*
-
+
A locale for residue rings
*)
definition residue_ring :: "int => int ring" where
- "residue_ring m == (|
- carrier = {0..m - 1},
+ "residue_ring m == (|
+ carrier = {0..m - 1},
mult = (%x y. (x * y) mod m),
one = 1,
zero = 0,
@@ -34,7 +34,8 @@
assumes m_gt_one: "m > 1"
defines "R == residue_ring m"
-context residues begin
+context residues
+begin
lemma abelian_group: "abelian_group R"
apply (insert m_gt_one)
@@ -79,23 +80,23 @@
context residues
begin
-(* These lemmas translate back and forth between internal and
+(* These lemmas translate back and forth between internal and
external concepts *)
lemma res_carrier_eq: "carrier R = {0..m - 1}"
- by (unfold R_def residue_ring_def, auto)
+ unfolding R_def residue_ring_def by auto
lemma res_add_eq: "x \<oplus> y = (x + y) mod m"
- by (unfold R_def residue_ring_def, auto)
+ unfolding R_def residue_ring_def by auto
lemma res_mult_eq: "x \<otimes> y = (x * y) mod m"
- by (unfold R_def residue_ring_def, auto)
+ unfolding R_def residue_ring_def by auto
lemma res_zero_eq: "\<zero> = 0"
- by (unfold R_def residue_ring_def, auto)
+ unfolding R_def residue_ring_def by auto
lemma res_one_eq: "\<one> = 1"
- by (unfold R_def residue_ring_def units_of_def, auto)
+ unfolding R_def residue_ring_def units_of_def by auto
lemma res_units_eq: "Units R = { x. 0 < x & x < m & coprime x m}"
apply (insert m_gt_one)
@@ -127,14 +128,14 @@
apply auto
done
-lemma finite [iff]: "finite(carrier R)"
+lemma finite [iff]: "finite (carrier R)"
by (subst res_carrier_eq, auto)
-lemma finite_Units [iff]: "finite(Units R)"
+lemma finite_Units [iff]: "finite (Units R)"
by (subst res_units_eq, auto)
-(* The function a -> a mod m maps the integers to the
- residue classes. The following lemmas show that this mapping
+(* The function a -> a mod m maps the integers to the
+ residue classes. The following lemmas show that this mapping
respects addition and multiplication on the integers. *)
lemma mod_in_carrier [iff]: "a mod m : carrier R"
@@ -143,7 +144,10 @@
done
lemma add_cong: "(x mod m) \<oplus> (y mod m) = (x + y) mod m"
- by (unfold R_def residue_ring_def, auto, arith)
+ unfolding R_def residue_ring_def
+ apply auto
+ apply presburger
+ done
lemma mult_cong: "(x mod m) \<otimes> (y mod m) = (x * y) mod m"
apply (unfold R_def residue_ring_def, auto)
@@ -155,13 +159,10 @@
done
lemma zero_cong: "\<zero> = 0"
- apply (unfold R_def residue_ring_def, auto)
- done
+ unfolding R_def residue_ring_def by auto
lemma one_cong: "\<one> = 1 mod m"
- apply (insert m_gt_one)
- apply (unfold R_def residue_ring_def, auto)
- done
+ using m_gt_one unfolding R_def residue_ring_def by auto
(* revise algebra library to use 1? *)
lemma pow_cong: "(x mod m) (^) n = x^n mod m"
@@ -181,19 +182,19 @@
apply auto
done
-lemma (in residues) prod_cong:
- "finite A \<Longrightarrow> (\<Otimes> i:A. (f i) mod m) = (PROD i:A. f i) mod m"
+lemma (in residues) prod_cong:
+ "finite A \<Longrightarrow> (\<Otimes> i:A. (f i) mod m) = (PROD i:A. f i) mod m"
apply (induct set: finite)
apply (auto simp: one_cong mult_cong)
done
lemma (in residues) sum_cong:
- "finite A \<Longrightarrow> (\<Oplus> i:A. (f i) mod m) = (SUM i: A. f i) mod m"
+ "finite A \<Longrightarrow> (\<Oplus> i:A. (f i) mod m) = (SUM i: A. f i) mod m"
apply (induct set: finite)
apply (auto simp: zero_cong add_cong)
done
-lemma mod_in_res_units [simp]: "1 < m \<Longrightarrow> coprime a m \<Longrightarrow>
+lemma mod_in_res_units [simp]: "1 < m \<Longrightarrow> coprime a m \<Longrightarrow>
a mod m : Units R"
apply (subst res_units_eq, auto)
apply (insert pos_mod_sign [of m a])
@@ -204,10 +205,10 @@
apply (subst gcd_commute_int, assumption)
done
-lemma res_eq_to_cong: "((a mod m) = (b mod m)) = [a = b] (mod (m::int))"
+lemma res_eq_to_cong: "((a mod m) = (b mod m)) = [a = b] (mod (m::int))"
unfolding cong_int_def by auto
-(* Simplifying with these will translate a ring equation in R to a
+(* Simplifying with these will translate a ring equation in R to a
congruence. *)
lemmas res_to_cong_simps = add_cong mult_cong pow_cong one_cong
@@ -243,13 +244,13 @@
using p_prime apply auto
done
-context residues_prime begin
+context residues_prime
+begin
lemma is_field: "field R"
apply (rule cring.field_intro2)
apply (rule cring)
- apply (auto simp add: res_carrier_eq res_one_eq res_zero_eq
- res_units_eq)
+ apply (auto simp add: res_carrier_eq res_one_eq res_zero_eq res_units_eq)
apply (rule classical)
apply (erule notE)
apply (subst gcd_commute_int)
@@ -285,25 +286,24 @@
(* the definition of the phi function *)
-definition phi :: "int => nat" where
- "phi m == card({ x. 0 < x & x < m & gcd x m = 1})"
+definition phi :: "int => nat"
+ where "phi m = card({ x. 0 < x & x < m & gcd x m = 1})"
lemma phi_zero [simp]: "phi 0 = 0"
apply (subst phi_def)
-(* Auto hangs here. Once again, where is the simplification rule
+(* Auto hangs here. Once again, where is the simplification rule
1 == Suc 0 coming from? *)
apply (auto simp add: card_eq_0_iff)
(* Add card_eq_0_iff as a simp rule? delete card_empty_imp? *)
done
lemma phi_one [simp]: "phi 1 = 0"
- apply (auto simp add: phi_def card_eq_0_iff)
- done
+ by (auto simp add: phi_def card_eq_0_iff)
lemma (in residues) phi_eq: "phi m = card(Units R)"
by (simp add: phi_def res_units_eq)
-lemma (in residues) euler_theorem1:
+lemma (in residues) euler_theorem1:
assumes a: "gcd a m = 1"
shows "[a^phi m = 1] (mod m)"
proof -
@@ -311,7 +311,7 @@
by (intro mod_in_res_units)
from phi_eq have "(a mod m) (^) (phi m) = (a mod m) (^) (card (Units R))"
by simp
- also have "\<dots> = \<one>"
+ also have "\<dots> = \<one>"
by (intro units_power_order_eq_one, auto)
finally show ?thesis
by (simp add: res_to_cong_simps)
@@ -319,13 +319,13 @@
(* In fact, there is a two line proof!
-lemma (in residues) euler_theorem1:
+lemma (in residues) euler_theorem1:
assumes a: "gcd a m = 1"
shows "[a^phi m = 1] (mod m)"
proof -
have "(a mod m) (^) (phi m) = \<one>"
by (simp add: phi_eq units_power_order_eq_one a m_gt_one)
- thus ?thesis
+ then show ?thesis
by (simp add: res_to_cong_simps)
qed
@@ -338,7 +338,7 @@
shows "[a^phi m = 1] (mod m)"
proof (cases)
assume "m = 0 | m = 1"
- thus ?thesis by auto
+ then show ?thesis by auto
next
assume "~(m = 0 | m = 1)"
with assms show ?thesis
@@ -375,8 +375,8 @@
subsection {* Wilson's theorem *}
-lemma (in field) inv_pair_lemma: "x : Units R \<Longrightarrow> y : Units R \<Longrightarrow>
- {x, inv x} ~= {y, inv y} \<Longrightarrow> {x, inv x} Int {y, inv y} = {}"
+lemma (in field) inv_pair_lemma: "x : Units R \<Longrightarrow> y : Units R \<Longrightarrow>
+ {x, inv x} ~= {y, inv y} \<Longrightarrow> {x, inv x} Int {y, inv y} = {}"
apply auto
apply (erule notE)
apply (erule inv_eq_imp_eq)
@@ -390,10 +390,10 @@
assumes a: "p > 2"
shows "[fact (p - 1) = - 1] (mod p)"
proof -
- let ?InversePairs = "{ {x, inv x} | x. x : Units R - {\<one>, \<ominus> \<one>}}"
+ let ?InversePairs = "{ {x, inv x} | x. x : Units R - {\<one>, \<ominus> \<one>}}"
have UR: "Units R = {\<one>, \<ominus> \<one>} Un (Union ?InversePairs)"
by auto
- have "(\<Otimes>i: Units R. i) =
+ have "(\<Otimes>i: Units R. i) =
(\<Otimes>i: {\<one>, \<ominus> \<one>}. i) \<otimes> (\<Otimes>i: Union ?InversePairs. i)"
apply (subst UR)
apply (subst finprod_Un_disjoint)
@@ -409,7 +409,7 @@
apply (frule one_eq_neg_one)
apply (insert a, force)
done
- also have "(\<Otimes>i:(Union ?InversePairs). i) =
+ also have "(\<Otimes>i:(Union ?InversePairs). i) =
(\<Otimes>A: ?InversePairs. (\<Otimes>y:A. y))"
apply (subst finprod_Union_disjoint)
apply force
@@ -444,8 +444,7 @@
apply (subst res_prime_units_eq, rule refl)
done
finally have "fact (p - 1) mod p = \<ominus> \<one>".
- thus ?thesis
- by (simp add: res_to_cong_simps)
+ then show ?thesis by (simp add: res_to_cong_simps)
qed
lemma wilson_theorem: "prime (p::int) \<Longrightarrow> [fact (p - 1) = - 1] (mod p)"
@@ -457,7 +456,6 @@
apply (rule residues_prime.wilson_theorem1)
apply (rule residues_prime.intro)
apply auto
-done
-
+ done
end
--- a/src/HOL/Number_Theory/UniqueFactorization.thy Sat Sep 10 22:11:55 2011 +0200
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy Sat Sep 10 23:27:32 2011 +0200
@@ -42,7 +42,7 @@
apply auto
apply (subst setsum_Un_disjoint)
apply auto
-done
+ done
lemma setprod_Un2: "finite (A Un B) \<Longrightarrow>
setprod f (A Un B) = setprod f (A - B) * setprod f (B - A) *
@@ -53,7 +53,7 @@
apply auto
apply (subst setprod_Un_disjoint)
apply auto
-done
+ done
(* Here is a version of set product for multisets. Is it worth moving
to multiset.thy? If so, one should similarly define msetsum for abelian
@@ -71,12 +71,10 @@
translations
"PROD i :# A. b" == "CONST msetprod (%i. b) A"
-lemma msetprod_empty:
- "msetprod f {#} = 1"
+lemma msetprod_empty: "msetprod f {#} = 1"
by (simp add: msetprod_def)
-lemma msetprod_singleton:
- "msetprod f {#x#} = f x"
+lemma msetprod_singleton: "msetprod f {#x#} = f x"
by (simp add: msetprod_def)
lemma msetprod_Un: "msetprod f (A+B) = msetprod f A * msetprod f B"
@@ -105,7 +103,7 @@
apply (auto intro: setprod_cong)
apply (subst setprod_Un_disjoint [symmetric])
apply (auto intro: setprod_cong)
-done
+ done
subsection {* unique factorization: multiset version *}
@@ -119,27 +117,23 @@
assume "(n::nat) > 0"
then have "n = 1 | (n > 1 & prime n) | (n > 1 & ~ prime n)"
by arith
- moreover
- {
+ moreover {
assume "n = 1"
then have "(ALL p : set_of {#}. prime p) & n = (PROD i :# {#}. i)"
by (auto simp add: msetprod_def)
- }
- moreover
- {
+ } moreover {
assume "n > 1" and "prime n"
then have "(ALL p : set_of {# n #}. prime p) & n = (PROD i :# {# n #}. i)"
by (auto simp add: msetprod_def)
- }
- moreover
- {
+ } moreover {
assume "n > 1" and "~ prime n"
- with not_prime_eq_prod_nat obtain m k where n: "n = m * k & 1 < m & m < n & 1 < k & k < n"
- by blast
+ with not_prime_eq_prod_nat
+ obtain m k where n: "n = m * k & 1 < m & m < n & 1 < k & k < n"
+ by blast
with ih obtain Q R where "(ALL p : set_of Q. prime p) & m = (PROD i:#Q. i)"
and "(ALL p: set_of R. prime p) & k = (PROD i:#R. i)"
by blast
- hence "(ALL p: set_of (Q + R). prime p) & n = (PROD i :# Q + R. i)"
+ then have "(ALL p: set_of (Q + R). prime p) & n = (PROD i :# Q + R. i)"
by (auto simp add: n msetprod_Un)
then have "EX M. (ALL p : set_of M. prime p) & n = (PROD i :# M. i)"..
}
@@ -162,23 +156,21 @@
also have "... dvd (PROD i :# N. i)" by (rule assms)
also have "... = (PROD i : (set_of N). i ^ (count N i))"
by (simp add: msetprod_def)
- also have "... =
- a^(count N a) * (PROD i : (set_of N - {a}). i ^ (count N i))"
- proof (cases)
- assume "a : set_of N"
- hence b: "set_of N = {a} Un (set_of N - {a})"
- by auto
- thus ?thesis
- by (subst (1) b, subst setprod_Un_disjoint, auto)
- next
- assume "a ~: set_of N"
- thus ?thesis
- by auto
- qed
+ also have "... = a^(count N a) * (PROD i : (set_of N - {a}). i ^ (count N i))"
+ proof (cases)
+ assume "a : set_of N"
+ then have b: "set_of N = {a} Un (set_of N - {a})"
+ by auto
+ then show ?thesis
+ by (subst (1) b, subst setprod_Un_disjoint, auto)
+ next
+ assume "a ~: set_of N"
+ then show ?thesis by auto
+ qed
finally have "a ^ count M a dvd
a^(count N a) * (PROD i : (set_of N - {a}). i ^ (count N i))".
- moreover have "coprime (a ^ count M a)
- (PROD i : (set_of N - {a}). i ^ (count N i))"
+ moreover
+ have "coprime (a ^ count M a) (PROD i : (set_of N - {a}). i ^ (count N i))"
apply (subst gcd_commute_nat)
apply (rule setprod_coprime_nat)
apply (rule primes_imp_powers_coprime_nat)
@@ -188,10 +180,12 @@
ultimately have "a ^ count M a dvd a^(count N a)"
by (elim coprime_dvd_mult_nat)
with a show ?thesis
- by (intro power_dvd_imp_le, auto)
+ apply (intro power_dvd_imp_le)
+ apply auto
+ done
next
assume "a ~: set_of M"
- thus ?thesis by auto
+ then show ?thesis by auto
qed
lemma multiset_prime_factorization_unique:
@@ -210,10 +204,11 @@
ultimately have "count M a = count N a"
by auto
}
- thus ?thesis by (simp add:multiset_eq_iff)
+ then show ?thesis by (simp add:multiset_eq_iff)
qed
-definition multiset_prime_factorization :: "nat => nat multiset" where
+definition multiset_prime_factorization :: "nat => nat multiset"
+where
"multiset_prime_factorization n ==
if n > 0 then (THE M. ((ALL p : set_of M. prime p) &
n = (PROD i :# M. i)))
@@ -234,27 +229,21 @@
subsection {* Prime factors and multiplicity for nats and ints *}
class unique_factorization =
-
-fixes
- multiplicity :: "'a \<Rightarrow> 'a \<Rightarrow> nat" and
- prime_factors :: "'a \<Rightarrow> 'a set"
+ fixes multiplicity :: "'a \<Rightarrow> 'a \<Rightarrow> nat"
+ and prime_factors :: "'a \<Rightarrow> 'a set"
(* definitions for the natural numbers *)
instantiation nat :: unique_factorization
begin
-definition
- multiplicity_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-where
- "multiplicity_nat p n = count (multiset_prime_factorization n) p"
+definition multiplicity_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+ where "multiplicity_nat p n = count (multiset_prime_factorization n) p"
-definition
- prime_factors_nat :: "nat \<Rightarrow> nat set"
-where
- "prime_factors_nat n = set_of (multiset_prime_factorization n)"
+definition prime_factors_nat :: "nat \<Rightarrow> nat set"
+ where "prime_factors_nat n = set_of (multiset_prime_factorization n)"
-instance proof qed
+instance ..
end
@@ -263,34 +252,31 @@
instantiation int :: unique_factorization
begin
-definition
- multiplicity_int :: "int \<Rightarrow> int \<Rightarrow> nat"
-where
- "multiplicity_int p n = multiplicity (nat p) (nat n)"
+definition multiplicity_int :: "int \<Rightarrow> int \<Rightarrow> nat"
+ where "multiplicity_int p n = multiplicity (nat p) (nat n)"
-definition
- prime_factors_int :: "int \<Rightarrow> int set"
-where
- "prime_factors_int n = int ` (prime_factors (nat n))"
+definition prime_factors_int :: "int \<Rightarrow> int set"
+ where "prime_factors_int n = int ` (prime_factors (nat n))"
-instance proof qed
+instance ..
end
subsection {* Set up transfer *}
-lemma transfer_nat_int_prime_factors:
- "prime_factors (nat n) = nat ` prime_factors n"
- unfolding prime_factors_int_def apply auto
- by (subst transfer_int_nat_set_return_embed, assumption)
+lemma transfer_nat_int_prime_factors: "prime_factors (nat n) = nat ` prime_factors n"
+ unfolding prime_factors_int_def
+ apply auto
+ apply (subst transfer_int_nat_set_return_embed)
+ apply assumption
+ done
-lemma transfer_nat_int_prime_factors_closure: "n >= 0 \<Longrightarrow>
- nat_set (prime_factors n)"
+lemma transfer_nat_int_prime_factors_closure: "n >= 0 \<Longrightarrow> nat_set (prime_factors n)"
by (auto simp add: nat_set_def prime_factors_int_def)
lemma transfer_nat_int_multiplicity: "p >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow>
- multiplicity (nat p) (nat n) = multiplicity p n"
+ multiplicity (nat p) (nat n) = multiplicity p n"
by (auto simp add: multiplicity_int_def)
declare transfer_morphism_nat_int[transfer add return:
@@ -298,8 +284,7 @@
transfer_nat_int_multiplicity]
-lemma transfer_int_nat_prime_factors:
- "prime_factors (int n) = int ` prime_factors n"
+lemma transfer_int_nat_prime_factors: "prime_factors (int n) = int ` prime_factors n"
unfolding prime_factors_int_def by auto
lemma transfer_int_nat_prime_factors_closure: "is_nat n \<Longrightarrow>
@@ -318,10 +303,10 @@
subsection {* Properties of prime factors and multiplicity for nats and ints *}
lemma prime_factors_ge_0_int [elim]: "p : prime_factors (n::int) \<Longrightarrow> p >= 0"
- by (unfold prime_factors_int_def, auto)
+ unfolding prime_factors_int_def by auto
lemma prime_factors_prime_nat [intro]: "p : prime_factors (n::nat) \<Longrightarrow> prime p"
- apply (case_tac "n = 0")
+ apply (cases "n = 0")
apply (simp add: prime_factors_nat_def multiset_prime_factorization_def)
apply (auto simp add: prime_factors_nat_def multiset_prime_factorization)
done
@@ -334,17 +319,21 @@
done
lemma prime_factors_gt_0_nat [elim]: "p : prime_factors x \<Longrightarrow> p > (0::nat)"
- by (frule prime_factors_prime_nat, auto)
+ apply (frule prime_factors_prime_nat)
+ apply auto
+ done
lemma prime_factors_gt_0_int [elim]: "x >= 0 \<Longrightarrow> p : prime_factors x \<Longrightarrow>
p > (0::int)"
- by (frule (1) prime_factors_prime_int, auto)
+ apply (frule (1) prime_factors_prime_int)
+ apply auto
+ done
lemma prime_factors_finite_nat [iff]: "finite (prime_factors (n::nat))"
- by (unfold prime_factors_nat_def, auto)
+ unfolding prime_factors_nat_def by auto
lemma prime_factors_finite_int [iff]: "finite (prime_factors (n::int))"
- by (unfold prime_factors_int_def, auto)
+ unfolding prime_factors_int_def by auto
lemma prime_factors_altdef_nat: "prime_factors (n::nat) =
{p. multiplicity p n > 0}"
@@ -359,8 +348,9 @@
lemma prime_factorization_nat: "(n::nat) > 0 \<Longrightarrow>
n = (PROD p : prime_factors n. p^(multiplicity p n))"
- by (frule multiset_prime_factorization,
- simp add: prime_factors_nat_def multiplicity_nat_def msetprod_def)
+ apply (frule multiset_prime_factorization)
+ apply (simp add: prime_factors_nat_def multiplicity_nat_def msetprod_def)
+ done
lemma prime_factorization_int:
assumes "(n::int) > 0"
@@ -376,8 +366,7 @@
"S = { (p::nat) . f p > 0} \<Longrightarrow> finite S \<Longrightarrow> (ALL p : S. prime p) \<Longrightarrow>
n = (PROD p : S. p^(f p)) \<Longrightarrow>
S = prime_factors n & (ALL p. f p = multiplicity p n)"
- apply (subgoal_tac "multiset_prime_factorization n = Abs_multiset
- f")
+ apply (subgoal_tac "multiset_prime_factorization n = Abs_multiset f")
apply (unfold prime_factors_nat_def multiplicity_nat_def)
apply (simp add: set_of_def Abs_multiset_inverse multiset_def)
apply (unfold multiset_prime_factorization_def)
@@ -396,13 +385,14 @@
apply (subgoal_tac "f : multiset")
apply (auto simp only: Abs_multiset_inverse)
unfolding multiset_def apply force
-done
+ done
lemma prime_factors_characterization_nat: "S = {p. 0 < f (p::nat)} \<Longrightarrow>
finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
prime_factors n = S"
- by (rule prime_factorization_unique_nat [THEN conjunct1, symmetric],
- assumption+)
+ apply (rule prime_factorization_unique_nat [THEN conjunct1, symmetric])
+ apply assumption+
+ done
lemma prime_factors_characterization'_nat:
"finite {p. 0 < f (p::nat)} \<Longrightarrow>
@@ -410,7 +400,7 @@
prime_factors (PROD p | 0 < f p . p ^ f p) = {p. 0 < f p}"
apply (rule prime_factors_characterization_nat)
apply auto
-done
+ done
(* A minor glitch:*)
@@ -433,7 +423,7 @@
[where f = "%x. f (int (x::nat))",
transferred direction: nat "op <= (0::int)"])
apply auto
-done
+ done
lemma prime_factors_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow>
finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
@@ -444,32 +434,32 @@
apply (subst primes_characterization'_int)
apply auto
apply (auto simp add: prime_ge_0_int)
-done
+ done
lemma multiplicity_characterization_nat: "S = {p. 0 < f (p::nat)} \<Longrightarrow>
finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
multiplicity p n = f p"
- by (frule prime_factorization_unique_nat [THEN conjunct2, rule_format,
- symmetric], auto)
+ apply (frule prime_factorization_unique_nat [THEN conjunct2, rule_format, symmetric])
+ apply auto
+ done
lemma multiplicity_characterization'_nat: "finite {p. 0 < f (p::nat)} \<longrightarrow>
(ALL p. 0 < f p \<longrightarrow> prime p) \<longrightarrow>
multiplicity p (PROD p | 0 < f p . p ^ f p) = f p"
- apply (rule impI)+
+ apply (intro impI)
apply (rule multiplicity_characterization_nat)
apply auto
-done
+ done
lemma multiplicity_characterization'_int [rule_format]:
"finite {p. p >= 0 & 0 < f (p::int)} \<Longrightarrow>
(ALL p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> p >= 0 \<Longrightarrow>
multiplicity p (PROD p | p >= 0 & 0 < f p . p ^ f p) = f p"
-
apply (insert multiplicity_characterization'_nat
[where f = "%x. f (int (x::nat))",
transferred direction: nat "op <= (0::int)", rule_format])
apply auto
-done
+ done
lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow>
finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
@@ -480,7 +470,7 @@
apply (subst multiplicity_characterization'_int)
apply auto
apply (auto simp add: prime_ge_0_int)
-done
+ done
lemma multiplicity_zero_nat [simp]: "multiplicity (p::nat) 0 = 0"
by (simp add: multiplicity_nat_def multiset_prime_factorization_def)
@@ -495,51 +485,50 @@
by (simp add: multiplicity_int_def)
lemma multiplicity_prime_nat [simp]: "prime (p::nat) \<Longrightarrow> multiplicity p p = 1"
- apply (subst multiplicity_characterization_nat
- [where f = "(%q. if q = p then 1 else 0)"])
+ apply (subst multiplicity_characterization_nat [where f = "(%q. if q = p then 1 else 0)"])
apply auto
apply (case_tac "x = p")
apply auto
-done
+ done
lemma multiplicity_prime_int [simp]: "prime (p::int) \<Longrightarrow> multiplicity p p = 1"
unfolding prime_int_def multiplicity_int_def by auto
-lemma multiplicity_prime_power_nat [simp]: "prime (p::nat) \<Longrightarrow>
- multiplicity p (p^n) = n"
- apply (case_tac "n = 0")
+lemma multiplicity_prime_power_nat [simp]: "prime (p::nat) \<Longrightarrow> multiplicity p (p^n) = n"
+ apply (cases "n = 0")
apply auto
- apply (subst multiplicity_characterization_nat
- [where f = "(%q. if q = p then n else 0)"])
+ apply (subst multiplicity_characterization_nat [where f = "(%q. if q = p then n else 0)"])
apply auto
apply (case_tac "x = p")
apply auto
-done
+ done
-lemma multiplicity_prime_power_int [simp]: "prime (p::int) \<Longrightarrow>
- multiplicity p (p^n) = n"
+lemma multiplicity_prime_power_int [simp]: "prime (p::int) \<Longrightarrow> multiplicity p (p^n) = n"
apply (frule prime_ge_0_int)
apply (auto simp add: prime_int_def multiplicity_int_def nat_power_eq)
-done
+ done
-lemma multiplicity_nonprime_nat [simp]: "~ prime (p::nat) \<Longrightarrow>
- multiplicity p n = 0"
- apply (case_tac "n = 0")
+lemma multiplicity_nonprime_nat [simp]: "~ prime (p::nat) \<Longrightarrow> multiplicity p n = 0"
+ apply (cases "n = 0")
apply auto
apply (frule multiset_prime_factorization)
apply (auto simp add: set_of_def multiplicity_nat_def)
-done
+ done
lemma multiplicity_nonprime_int [simp]: "~ prime (p::int) \<Longrightarrow> multiplicity p n = 0"
- by (unfold multiplicity_int_def prime_int_def, auto)
+ unfolding multiplicity_int_def prime_int_def by auto
lemma multiplicity_not_factor_nat [simp]:
"p ~: prime_factors (n::nat) \<Longrightarrow> multiplicity p n = 0"
- by (subst (asm) prime_factors_altdef_nat, auto)
+ apply (subst (asm) prime_factors_altdef_nat)
+ apply auto
+ done
lemma multiplicity_not_factor_int [simp]:
"p >= 0 \<Longrightarrow> p ~: prime_factors (n::int) \<Longrightarrow> multiplicity p n = 0"
- by (subst (asm) prime_factors_altdef_int, auto)
+ apply (subst (asm) prime_factors_altdef_int)
+ apply auto
+ done
lemma multiplicity_product_aux_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow>
(prime_factors k) Un (prime_factors l) = prime_factors (k * l) &
@@ -572,7 +561,7 @@
apply (simp add: setprod_1)
apply (erule prime_factorization_nat)
apply (rule setprod_cong, auto)
-done
+ done
(* transfer doesn't have the same problem here with the right
choice of rules. *)
@@ -611,7 +600,7 @@
apply auto
apply (subst multiplicity_product_nat)
apply auto
-done
+ done
(* Transfer is delicate here for two reasons: first, because there is
an implicit quantifier over functions (f), and, second, because the
@@ -627,7 +616,7 @@
"(PROD x : A. int (f x)) >= 0"
apply (rule setsum_nonneg, auto)
apply (rule setprod_nonneg, auto)
-done
+ done
declare transfer_morphism_nat_int[transfer
add return: transfer_nat_int_sum_prod_closure3
@@ -648,7 +637,7 @@
apply auto
apply (rule setsum_cong)
apply auto
-done
+ done
declare transfer_morphism_nat_int[transfer
add return: transfer_nat_int_sum_prod2 (1)]
@@ -676,7 +665,6 @@
lemma multiplicity_prod_prime_powers_int:
"(p::int) >= 0 \<Longrightarrow> finite S \<Longrightarrow> (ALL p : S. prime p) \<Longrightarrow>
multiplicity p (PROD p : S. p ^ f p) = (if p : S then f p else 0)"
-
apply (subgoal_tac "int ` nat ` S = S")
apply (frule multiplicity_prod_prime_powers_nat [where f = "%x. f(int x)"
and S = "nat ` S", transferred])
@@ -684,7 +672,7 @@
apply (metis prime_int_def)
apply (metis prime_ge_0_int)
apply (metis nat_set_def prime_ge_0_int transfer_nat_int_set_return_embed)
-done
+ done
lemma multiplicity_distinct_prime_power_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow>
p ~= q \<Longrightarrow> multiplicity p (q^n) = 0"
@@ -692,7 +680,7 @@
apply (erule ssubst)
apply (subst multiplicity_prod_prime_powers_nat)
apply auto
-done
+ done
lemma multiplicity_distinct_prime_power_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow>
p ~= q \<Longrightarrow> multiplicity p (q^n) = 0"
@@ -701,41 +689,40 @@
prefer 4
apply assumption
apply auto
-done
+ done
-lemma dvd_multiplicity_nat:
+lemma dvd_multiplicity_nat:
"(0::nat) < y \<Longrightarrow> x dvd y \<Longrightarrow> multiplicity p x <= multiplicity p y"
- apply (case_tac "x = 0")
+ apply (cases "x = 0")
apply (auto simp add: dvd_def multiplicity_product_nat)
-done
+ done
lemma dvd_multiplicity_int:
"(0::int) < y \<Longrightarrow> 0 <= x \<Longrightarrow> x dvd y \<Longrightarrow> p >= 0 \<Longrightarrow>
multiplicity p x <= multiplicity p y"
- apply (case_tac "x = 0")
+ apply (cases "x = 0")
apply (auto simp add: dvd_def)
apply (subgoal_tac "0 < k")
apply (auto simp add: multiplicity_product_int)
apply (erule zero_less_mult_pos)
apply arith
-done
+ done
lemma dvd_prime_factors_nat [intro]:
"0 < (y::nat) \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x <= prime_factors y"
apply (simp only: prime_factors_altdef_nat)
apply auto
apply (metis dvd_multiplicity_nat le_0_eq neq_zero_eq_gt_zero_nat)
-done
+ done
lemma dvd_prime_factors_int [intro]:
"0 < (y::int) \<Longrightarrow> 0 <= x \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x <= prime_factors y"
apply (auto simp add: prime_factors_altdef_int)
apply (metis dvd_multiplicity_int le_0_eq neq_zero_eq_gt_zero_nat)
-done
+ done
lemma multiplicity_dvd_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow>
- ALL p. multiplicity p x <= multiplicity p y \<Longrightarrow>
- x dvd y"
+ ALL p. multiplicity p x <= multiplicity p y \<Longrightarrow> x dvd y"
apply (subst prime_factorization_nat [of x], assumption)
apply (subst prime_factorization_nat [of y], assumption)
apply (rule setprod_dvd_setprod_subset2)
@@ -744,11 +731,10 @@
apply auto
apply (metis gr0I le_0_eq less_not_refl)
apply (metis le_imp_power_dvd)
-done
+ done
lemma multiplicity_dvd_int: "0 < (x::int) \<Longrightarrow> 0 < y \<Longrightarrow>
- ALL p >= 0. multiplicity p x <= multiplicity p y \<Longrightarrow>
- x dvd y"
+ ALL p >= 0. multiplicity p x <= multiplicity p y \<Longrightarrow> x dvd y"
apply (subst prime_factorization_int [of x], assumption)
apply (subst prime_factorization_int [of y], assumption)
apply (rule setprod_dvd_setprod_subset2)
@@ -756,17 +742,18 @@
apply (subst prime_factors_altdef_int)+
apply auto
apply (metis le_imp_power_dvd prime_factors_ge_0_int)
-done
+ done
lemma multiplicity_dvd'_nat: "(0::nat) < x \<Longrightarrow>
\<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
-by (metis gcd_lcm_complete_lattice_nat.top_greatest le_refl multiplicity_dvd_nat
- multiplicity_nonprime_nat neq0_conv)
+ by (metis gcd_lcm_complete_lattice_nat.top_greatest le_refl multiplicity_dvd_nat
+ multiplicity_nonprime_nat neq0_conv)
lemma multiplicity_dvd'_int: "(0::int) < x \<Longrightarrow> 0 <= y \<Longrightarrow>
\<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
-by (metis eq_imp_le gcd_lcm_complete_lattice_nat.top_greatest int_eq_0_conv multiplicity_dvd_int
- multiplicity_nonprime_int nat_int transfer_nat_int_relations(4) less_le)
+ by (metis eq_imp_le gcd_lcm_complete_lattice_nat.top_greatest int_eq_0_conv
+ multiplicity_dvd_int multiplicity_nonprime_int nat_int transfer_nat_int_relations(4)
+ less_le)
lemma dvd_multiplicity_eq_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow>
(x dvd y) = (ALL p. multiplicity p x <= multiplicity p y)"
@@ -778,7 +765,7 @@
lemma prime_factors_altdef2_nat: "(n::nat) > 0 \<Longrightarrow>
(p : prime_factors n) = (prime p & p dvd n)"
- apply (case_tac "prime p")
+ apply (cases "prime p")
apply auto
apply (subst prime_factorization_nat [where n = n], assumption)
apply (rule dvd_trans)
@@ -787,13 +774,12 @@
apply (rule dvd_setprod)
apply auto
apply (metis One_nat_def Zero_not_Suc dvd_multiplicity_nat le0 le_antisym multiplicity_not_factor_nat multiplicity_prime_nat)
-done
+ done
lemma prime_factors_altdef2_int:
assumes "(n::int) > 0"
shows "(p : prime_factors n) = (prime p & p dvd n)"
-
- apply (case_tac "p >= 0")
+ apply (cases "p >= 0")
apply (rule prime_factors_altdef2_nat [transferred])
using assms apply auto
apply (auto simp add: prime_ge_0_int prime_factors_ge_0_int)
@@ -804,20 +790,18 @@
assumes [arith]: "x > 0" "y > 0" and
mult_eq [simp]: "!!p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
shows "x = y"
-
apply (rule dvd_antisym)
apply (auto intro: multiplicity_dvd'_nat)
-done
+ done
lemma multiplicity_eq_int:
fixes x and y::int
assumes [arith]: "x > 0" "y > 0" and
mult_eq [simp]: "!!p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
shows "x = y"
-
apply (rule dvd_antisym [transferred])
apply (auto intro: multiplicity_dvd'_int)
-done
+ done
subsection {* An application *}
@@ -850,7 +834,7 @@
done
ultimately have "z = gcd x y"
by (subst gcd_unique_nat [symmetric], blast)
- thus ?thesis
+ then show ?thesis
unfolding z_def by auto
qed
@@ -882,39 +866,34 @@
done
ultimately have "z = lcm x y"
by (subst lcm_unique_nat [symmetric], blast)
- thus ?thesis
+ then show ?thesis
unfolding z_def by auto
qed
lemma multiplicity_gcd_nat:
assumes [arith]: "x > 0" "y > 0"
- shows "multiplicity (p::nat) (gcd x y) =
- min (multiplicity p x) (multiplicity p y)"
-
+ shows "multiplicity (p::nat) (gcd x y) = min (multiplicity p x) (multiplicity p y)"
apply (subst gcd_eq_nat)
apply auto
apply (subst multiplicity_prod_prime_powers_nat)
apply auto
-done
+ done
lemma multiplicity_lcm_nat:
assumes [arith]: "x > 0" "y > 0"
- shows "multiplicity (p::nat) (lcm x y) =
- max (multiplicity p x) (multiplicity p y)"
-
+ shows "multiplicity (p::nat) (lcm x y) = max (multiplicity p x) (multiplicity p y)"
apply (subst lcm_eq_nat)
apply auto
apply (subst multiplicity_prod_prime_powers_nat)
apply auto
-done
+ done
lemma gcd_lcm_distrib_nat: "gcd (x::nat) (lcm y z) = lcm (gcd x y) (gcd x z)"
- apply (case_tac "x = 0 | y = 0 | z = 0")
+ apply (cases "x = 0 | y = 0 | z = 0")
apply auto
apply (rule multiplicity_eq_nat)
- apply (auto simp add: multiplicity_gcd_nat multiplicity_lcm_nat
- lcm_pos_nat)
-done
+ apply (auto simp add: multiplicity_gcd_nat multiplicity_lcm_nat lcm_pos_nat)
+ done
lemma gcd_lcm_distrib_int: "gcd (x::int) (lcm y z) = lcm (gcd x y) (gcd x z)"
apply (subst (1 2 3) gcd_abs_int)
@@ -923,6 +902,6 @@
apply force
apply (rule gcd_lcm_distrib_nat [transferred])
apply auto
-done
+ done
end