--- a/src/HOL/IsaMakefile Fri Jun 19 18:01:09 2009 +0200
+++ b/src/HOL/IsaMakefile Fri Jun 19 18:33:10 2009 +0200
@@ -34,6 +34,7 @@
HOL-Modelcheck \
HOL-NanoJava \
HOL-Nominal-Examples \
+ HOL-NewNumberTheory \
HOL-NumberTheory \
HOL-Prolog \
HOL-SET-Protocol \
@@ -489,6 +490,18 @@
@cd Import/HOLLight; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOLLight
+## HOL-NewNumberTheory
+
+HOL-NewNumberTheory: HOL $(LOG)/HOL-NewNumberTheory.gz
+
+$(LOG)/HOL-NewNumberTheory.gz: $(OUT)/HOL GCD.thy Library/Multiset.thy \
+ NewNumberTheory/Fib.thy NewNumberTheory/Binomial.thy \
+ NewNumberTheory/Residues.thy NewNumberTheory/UniqueFactorization.thy \
+ NewNumberTheory/Cong.thy NewNumberTheory/MiscAlgebra.thy \
+ NewNumberTheory/ROOT.ML
+ @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL NewNumberTheory
+
+
## HOL-NumberTheory
HOL-NumberTheory: HOL $(LOG)/HOL-NumberTheory.gz
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NewNumberTheory/Binomial.thy Fri Jun 19 18:33:10 2009 +0200
@@ -0,0 +1,540 @@
+(* Title: Binomial.thy
+ Authors: Lawrence C. Paulson, Jeremy Avigad, Tobias Nipkow
+
+
+Defines factorial and the "choose" function, and establishes basic properties.
+
+The original theory "Binomial" was by Lawrence C. Paulson, based on
+the work of Andy Gordon and Florian Kammueller. The approach here,
+which derives the definition of binomial coefficients in terms of the
+factorial function, is due to Jeremy Avigad. The binomial theorem was
+formalized by Tobias Nipkow.
+
+*)
+
+
+header {* Binomial *}
+
+theory Binomial
+imports Cong
+begin
+
+
+subsection {* Main definitions *}
+
+class binomial =
+
+fixes
+ fact :: "'a \<Rightarrow> 'a" and
+ binomial :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "choose" 65)
+
+(* definitions for the natural numbers *)
+
+instantiation nat :: binomial
+
+begin
+
+fun
+ fact_nat :: "nat \<Rightarrow> nat"
+where
+ "fact_nat x =
+ (if x = 0 then 1 else
+ x * fact(x - 1))"
+
+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
+
+end
+
+(* definitions for the integers *)
+
+instantiation int :: binomial
+
+begin
+
+definition
+ fact_int :: "int \<Rightarrow> int"
+where
+ "fact_int x = (if x >= 0 then int (fact (nat x)) else 0)"
+
+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
+
+end
+
+
+subsection {* Set up Transfer *}
+
+
+lemma transfer_nat_int_binomial:
+ "(x::int) >= 0 \<Longrightarrow> fact (nat x) = nat (fact x)"
+ "(n::int) >= 0 \<Longrightarrow> k >= 0 \<Longrightarrow> binomial (nat n) (nat k) =
+ nat (binomial n k)"
+ unfolding fact_int_def binomial_int_def
+ by auto
+
+
+lemma transfer_nat_int_binomial_closures:
+ "x >= (0::int) \<Longrightarrow> fact x >= 0"
+ "n >= (0::int) \<Longrightarrow> k >= 0 \<Longrightarrow> binomial n k >= 0"
+ by (auto simp add: fact_int_def binomial_int_def)
+
+declare TransferMorphism_nat_int[transfer add return:
+ transfer_nat_int_binomial transfer_nat_int_binomial_closures]
+
+lemma transfer_int_nat_binomial:
+ "fact (int x) = int (fact x)"
+ "binomial (int n) (int k) = int (binomial n k)"
+ unfolding fact_int_def binomial_int_def by auto
+
+lemma transfer_int_nat_binomial_closures:
+ "is_nat x \<Longrightarrow> fact x >= 0"
+ "is_nat n \<Longrightarrow> is_nat k \<Longrightarrow> binomial n k >= 0"
+ by (auto simp add: fact_int_def binomial_int_def)
+
+declare TransferMorphism_int_nat[transfer add return:
+ transfer_int_nat_binomial transfer_int_nat_binomial_closures]
+
+
+subsection {* Factorial *}
+
+lemma nat_fact_zero [simp]: "fact (0::nat) = 1"
+ by simp
+
+lemma int_fact_zero [simp]: "fact (0::int) = 1"
+ by (simp add: fact_int_def)
+
+lemma nat_fact_one [simp]: "fact (1::nat) = 1"
+ by simp
+
+lemma nat_fact_Suc_0 [simp]: "fact (Suc 0) = Suc 0"
+ by (simp add: One_nat_def)
+
+lemma int_fact_one [simp]: "fact (1::int) = 1"
+ by (simp add: fact_int_def)
+
+lemma nat_fact_plus_one: "fact ((n::nat) + 1) = (n + 1) * fact n"
+ by simp
+
+lemma nat_fact_Suc: "fact (Suc n) = (Suc n) * fact n"
+ by (simp add: One_nat_def)
+
+lemma int_fact_plus_one:
+ assumes "n >= 0"
+ shows "fact ((n::int) + 1) = (n + 1) * fact n"
+
+ using prems by (rule nat_fact_plus_one [transferred])
+
+lemma nat_fact_reduce: "(n::nat) > 0 \<Longrightarrow> fact n = n * fact (n - 1)"
+ by simp
+
+lemma int_fact_reduce:
+ assumes "(n::int) > 0"
+ shows "fact n = n * fact (n - 1)"
+
+ using prems apply (subst tsub_eq [symmetric], auto)
+ apply (rule nat_fact_reduce [transferred])
+ using prems apply auto
+done
+
+declare fact_nat.simps [simp del]
+
+lemma nat_fact_nonzero [simp]: "fact (n::nat) \<noteq> 0"
+ apply (induct n rule: nat_induct')
+ apply (auto simp add: nat_fact_plus_one)
+done
+
+lemma int_fact_nonzero [simp]: "n >= 0 \<Longrightarrow> fact (n::int) ~= 0"
+ by (simp add: fact_int_def)
+
+lemma nat_fact_gt_zero [simp]: "fact (n :: nat) > 0"
+ by (insert nat_fact_nonzero [of n], arith)
+
+lemma int_fact_gt_zero [simp]: "n >= 0 \<Longrightarrow> fact (n :: int) > 0"
+ by (auto simp add: fact_int_def)
+
+lemma nat_fact_ge_one [simp]: "fact (n :: nat) >= 1"
+ by (insert nat_fact_nonzero [of n], arith)
+
+lemma nat_fact_ge_Suc_0 [simp]: "fact (n :: nat) >= Suc 0"
+ by (insert nat_fact_nonzero [of n], arith)
+
+lemma int_fact_ge_one [simp]: "n >= 0 \<Longrightarrow> fact (n :: int) >= 1"
+ apply (auto simp add: fact_int_def)
+ apply (subgoal_tac "1 = int 1")
+ apply (erule ssubst)
+ apply (subst zle_int)
+ apply auto
+done
+
+lemma nat_dvd_fact [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::nat)"
+ apply (induct n rule: nat_induct')
+ apply (auto simp add: nat_fact_plus_one)
+ apply (subgoal_tac "m = n + 1")
+ apply auto
+done
+
+lemma int_dvd_fact [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::int)"
+ apply (case_tac "1 <= n")
+ apply (induct n rule: int_ge_induct)
+ apply (auto simp add: int_fact_plus_one)
+ apply (subgoal_tac "m = i + 1")
+ apply auto
+done
+
+lemma nat_interval_plus_one: "(i::nat) <= j + 1 \<Longrightarrow>
+ {i..j+1} = {i..j} Un {j+1}"
+ by auto
+
+lemma int_interval_plus_one: "(i::int) <= j + 1 \<Longrightarrow> {i..j+1} = {i..j} Un {j+1}"
+ by auto
+
+lemma nat_fact_altdef: "fact (n::nat) = (PROD i:{1..n}. i)"
+ apply (induct n rule: nat_induct')
+ apply force
+ apply (subst nat_fact_plus_one)
+ apply (subst nat_interval_plus_one)
+ apply auto
+done
+
+lemma int_fact_altdef: "n >= 0 \<Longrightarrow> fact (n::int) = (PROD i:{1..n}. i)"
+ apply (induct n rule: int_ge_induct)
+ apply force
+ apply (subst int_fact_plus_one, assumption)
+ apply (subst int_interval_plus_one)
+ apply auto
+done
+
+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 nat_fact_ge_one [of n] by arith
+ from nat_prime_factor [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"
+ from `prime p` have "p \<ge> 1"
+ by (cases p, simp_all)
+ with `p <= n` have "p dvd fact n"
+ by (intro nat_dvd_fact)
+ with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n"
+ by (rule nat_dvd_diff)
+ hence "p dvd 1" by simp
+ hence "p <= 1" by auto
+ moreover from `prime p` have "p > 1" by auto
+ ultimately have False by auto}
+ hence "n < p" by arith
+ 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
+
+lemma primes_infinite: "\<not> (finite {(p::nat). prime p})"
+proof
+ assume "finite {(p::nat). prime p}"
+ with Max_ge have "(EX b. (ALL x : {(p::nat). prime p}. x <= b))"
+ 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
+qed
+
+
+subsection {* Binomial coefficients *}
+
+lemma nat_choose_zero [simp]: "(n::nat) choose 0 = 1"
+ by simp
+
+lemma int_choose_zero [simp]: "n \<ge> 0 \<Longrightarrow> (n::int) choose 0 = 1"
+ by (simp add: binomial_int_def)
+
+lemma nat_zero_choose [rule_format,simp]: "ALL (k::nat) > n. n choose k = 0"
+ by (induct n rule: nat_induct', auto)
+
+lemma int_zero_choose [rule_format,simp]: "(k::int) > n \<Longrightarrow> n choose k = 0"
+ unfolding binomial_int_def apply (case_tac "n < 0")
+ apply force
+ apply (simp del: binomial_nat.simps)
+done
+
+lemma nat_choose_reduce: "(n::nat) > 0 \<Longrightarrow> 0 < k \<Longrightarrow>
+ (n choose k) = ((n - 1) choose k) + ((n - 1) choose (k - 1))"
+ by simp
+
+lemma int_choose_reduce: "(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 nat_choose_reduce)
+ apply (auto simp del: binomial_nat.simps
+ simp add: nat_diff_distrib)
+done
+
+lemma nat_choose_plus_one: "((n::nat) + 1) choose (k + 1) =
+ (n choose (k + 1)) + (n choose k)"
+ by (simp add: nat_choose_reduce)
+
+lemma nat_choose_Suc: "(Suc n) choose (Suc k) =
+ (n choose (Suc k)) + (n choose k)"
+ by (simp add: nat_choose_reduce One_nat_def)
+
+lemma int_choose_plus_one: "n \<ge> 0 \<Longrightarrow> k \<ge> 0 \<Longrightarrow> ((n::int) + 1) choose (k + 1) =
+ (n choose (k + 1)) + (n choose k)"
+ by (simp add: binomial_int_def nat_choose_plus_one nat_add_distrib
+ del: binomial_nat.simps)
+
+declare binomial_nat.simps [simp del]
+
+lemma nat_choose_self [simp]: "((n::nat) choose n) = 1"
+ by (induct n rule: nat_induct', auto simp add: nat_choose_plus_one)
+
+lemma int_choose_self [simp]: "n \<ge> 0 \<Longrightarrow> ((n::int) choose n) = 1"
+ by (auto simp add: binomial_int_def)
+
+lemma nat_choose_one [simp]: "(n::nat) choose 1 = n"
+ by (induct n rule: nat_induct', auto simp add: nat_choose_reduce)
+
+lemma int_choose_one [simp]: "n \<ge> 0 \<Longrightarrow> (n::int) choose 1 = n"
+ by (auto simp add: binomial_int_def)
+
+lemma nat_plus_one_choose_self [simp]: "(n::nat) + 1 choose n = n + 1"
+ apply (induct n rule: nat_induct', force)
+ apply (case_tac "n = 0")
+ apply auto
+ apply (subst nat_choose_reduce)
+ apply (auto simp add: One_nat_def)
+ (* natdiff_cancel_numerals introduces Suc *)
+done
+
+lemma nat_Suc_choose_self [simp]: "(Suc n) choose n = Suc n"
+ using nat_plus_one_choose_self by (simp add: One_nat_def)
+
+lemma int_plus_one_choose_self [rule_format, simp]:
+ "(n::int) \<ge> 0 \<longrightarrow> n + 1 choose n = n + 1"
+ by (auto simp add: binomial_int_def nat_add_distrib)
+
+(* bounded quantification doesn't work with the unicode characters? *)
+lemma nat_choose_pos [rule_format]: "ALL k <= (n::nat).
+ ((n::nat) choose k) > 0"
+ apply (induct n rule: nat_induct')
+ apply force
+ apply clarify
+ apply (case_tac "k = 0")
+ apply force
+ apply (subst nat_choose_reduce)
+ apply auto
+done
+
+lemma int_choose_pos: "n \<ge> 0 \<Longrightarrow> k >= 0 \<Longrightarrow> k \<le> n \<Longrightarrow>
+ ((n::int) choose k) > 0"
+ by (auto simp add: binomial_int_def nat_choose_pos)
+
+lemma binomial_induct [rule_format]: "(ALL (n::nat). P n n) \<longrightarrow>
+ (ALL n. P (n + 1) 0) \<longrightarrow> (ALL n. (ALL k < n. P n k \<longrightarrow> P n (k + 1) \<longrightarrow>
+ P (n + 1) (k + 1))) \<longrightarrow> (ALL k <= n. P n k)"
+ apply (induct n rule: nat_induct')
+ apply auto
+ apply (case_tac "k = 0")
+ apply auto
+ apply (case_tac "k = n + 1")
+ apply auto
+ apply (drule_tac x = n in spec) back back
+ apply (drule_tac x = "k - 1" in spec) back back back
+ apply auto
+done
+
+lemma nat_choose_altdef_aux: "(k::nat) \<le> n \<Longrightarrow>
+ fact k * fact (n - k) * (n choose k) = fact n"
+ apply (rule binomial_induct [of _ k n])
+ apply auto
+proof -
+ 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"
+ by (subst nat_fact_plus_one, auto)
+ 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) nat_fact_plus_one, auto)
+ with less have two: "fact (k + 1) * fact (n - k) * (n choose (k + 1)) =
+ (n - k) * fact n" by simp
+ have "fact (k + 1) * fact (n - k) * (n + 1 choose (k + 1)) =
+ fact (k + 1) * fact (n - k) * (n choose (k + 1)) +
+ fact (k + 1) * fact (n - k) * (n choose k)"
+ by (subst nat_choose_reduce, auto simp add: ring_simps)
+ also note one
+ also note two
+ also with less have "(n - k) * fact n + (k + 1) * fact n= fact (n + 1)"
+ apply (subst nat_fact_plus_one)
+ apply (subst left_distrib [symmetric])
+ apply simp
+ done
+ finally show "fact (k + 1) * fact (n - k) * (n + 1 choose (k + 1)) =
+ fact (n + 1)" .
+qed
+
+lemma nat_choose_altdef: "(k::nat) \<le> n \<Longrightarrow>
+ n choose k = fact n div (fact k * fact (n - k))"
+ apply (frule nat_choose_altdef_aux)
+ apply (erule subst)
+ apply (simp add: mult_ac)
+done
+
+
+lemma int_choose_altdef:
+ assumes "(0::int) <= k" and "k <= n"
+ shows "n choose k = fact n div (fact k * fact (n - k))"
+
+ apply (subst tsub_eq [symmetric], rule prems)
+ apply (rule nat_choose_altdef [transferred])
+ using prems apply auto
+done
+
+lemma nat_choose_dvd: "(k::nat) \<le> n \<Longrightarrow> fact k * fact (n - k) dvd fact n"
+ unfolding dvd_def apply (frule nat_choose_altdef_aux)
+ (* why don't blast and auto get this??? *)
+ apply (rule exI)
+ apply (erule sym)
+done
+
+lemma int_choose_dvd:
+ assumes "(0::int) <= k" and "k <= n"
+ shows "fact k * fact (n - k) dvd fact n"
+
+ apply (subst tsub_eq [symmetric], rule prems)
+ apply (rule nat_choose_dvd [transferred])
+ using prems apply auto
+done
+
+(* generalizes Tobias Nipkow's proof to any commutative semiring *)
+theorem binomial: "(a+b::'a::{comm_ring_1,power})^n =
+ (SUM k=0..n. (of_nat (n choose k)) * a^k * b^(n-k))" (is "?P n")
+proof (induct n rule: nat_induct')
+ show "?P 0" by simp
+next
+ fix n
+ assume ih: "?P n"
+ have decomp: "{0..n+1} = {0} Un {n+1} Un {1..n}"
+ by auto
+ have decomp2: "{0..n} = {0} Un {1..n}"
+ by auto
+ have decomp3: "{1..n+1} = {n+1} Un {1..n}"
+ by auto
+ have "(a+b)^(n+1) =
+ (a+b) * (SUM k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
+ using ih by (simp add: power_plus_one)
+ also have "... = a*(SUM k=0..n. of_nat (n choose k) * a^k * b^(n-k)) +
+ b*(SUM k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
+ by (rule distrib)
+ also have "... = (SUM k=0..n. of_nat (n choose k) * a^(k+1) * b^(n-k)) +
+ (SUM k=0..n. of_nat (n choose k) * a^k * b^(n-k+1))"
+ by (subst (1 2) power_plus_one, simp add: setsum_right_distrib mult_ac)
+ also have "... = (SUM k=0..n. of_nat (n choose k) * a^k * b^(n+1-k)) +
+ (SUM k=1..n+1. of_nat (n choose (k - 1)) * a^k * b^(n+1-k))"
+ by (simp add:setsum_shift_bounds_cl_Suc_ivl Suc_diff_le
+ power_Suc ring_simps One_nat_def del:setsum_cl_ivl_Suc)
+ also have "... = a^(n+1) + b^(n+1) +
+ (SUM k=1..n. of_nat (n choose (k - 1)) * a^k * b^(n+1-k)) +
+ (SUM k=1..n. of_nat (n choose k) * a^k * b^(n+1-k))"
+ by (simp add: decomp2 decomp3)
+ also have
+ "... = a^(n+1) + b^(n+1) +
+ (SUM k=1..n. of_nat(n+1 choose k) * a^k * b^(n+1-k))"
+ by (auto simp add: ring_simps setsum_addf [symmetric]
+ nat_choose_reduce)
+ also have "... = (SUM k=0..n+1. of_nat (n+1 choose k) * a^k * b^(n+1-k))"
+ using decomp by (simp add: ring_simps)
+ finally show "?P (n + 1)" by simp
+qed
+
+lemma set_explicit: "{S. S = T \<and> P S} = (if P T then {T} else {})"
+ by auto
+
+lemma nat_card_subsets [rule_format]:
+ fixes S :: "'a set"
+ assumes "finite S"
+ shows "ALL k. card {T. T \<le> S \<and> card T = k} = card S choose k"
+ (is "?P S")
+using `finite S`
+proof (induct set: finite)
+ show "?P {}" by (auto simp add: set_explicit)
+ next fix x :: "'a" and F
+ assume iassms: "finite F" "x ~: F"
+ assume ih: "?P F"
+ show "?P (insert x F)" (is "ALL k. ?Q k")
+ proof
+ fix k
+ show "card {T. T \<subseteq> (insert x F) \<and> card T = k} =
+ card (insert x F) choose k" (is "?Q k")
+ proof (induct k rule: nat_induct')
+ from iassms have "{T. T \<le> (insert x F) \<and> card T = 0} = {{}}"
+ apply auto
+ apply (subst (asm) card_0_eq)
+ apply (auto elim: finite_subset)
+ done
+ thus "?Q 0"
+ by auto
+ next fix k
+ show "?Q (k + 1)"
+ proof -
+ from iassms have fin: "finite (insert x F)" by auto
+ hence "{ 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 intro!: subsetI)
+ with iassms fin have "card ({T. T \<le> insert x F \<and> card T = k + 1}) =
+ card ({T. T \<subseteq> F \<and> card T = k + 1}) +
+ card ({T. T \<subseteq> insert x F \<and> x : T \<and> card T = k + 1})"
+ apply (subst card_Un_disjoint [symmetric])
+ apply auto
+ (* note: nice! Didn't have to say anything here *)
+ done
+ also from ih have "card ({T. T \<subseteq> F \<and> card T = k + 1}) =
+ card F choose (k+1)" by auto
+ also have "card ({T. T \<subseteq> insert x F \<and> x : T \<and> card T = k + 1}) =
+ card ({T. T <= F & card T = k})"
+ proof -
+ let ?f = "%T. T Un {x}"
+ from iassms have "inj_on ?f {T. T <= F & card T = k}"
+ unfolding inj_on_def by (auto intro!: subsetI)
+ hence "card ({T. T <= F & card T = k}) =
+ card(?f ` {T. T <= F & card T = k})"
+ by (rule card_image [symmetric])
+ also from iassms fin have "?f ` {T. T <= F & card T = k} =
+ {T. T \<subseteq> insert x F \<and> x : T \<and> card T = k + 1}"
+ unfolding image_def
+ (* I can't figure out why this next line takes so long *)
+ apply auto
+ apply (frule (1) finite_subset, force)
+ apply (rule_tac x = "xa - {x}" in exI)
+ apply (subst card_Diff_singleton)
+ apply (auto elim: finite_subset)
+ done
+ finally show ?thesis by (rule sym)
+ qed
+ also from ih have "card ({T. T <= F & card T = k}) = card F choose k"
+ by auto
+ finally have "card ({T. T \<le> insert x F \<and> card T = k + 1}) =
+ card F choose (k + 1) + (card F choose k)".
+ with iassms nat_choose_plus_one show ?thesis
+ by auto
+ qed
+ qed
+ qed
+qed
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NewNumberTheory/Cong.thy Fri Jun 19 18:33:10 2009 +0200
@@ -0,0 +1,1093 @@
+(* Title: HOL/Library/Cong.thy
+ ID:
+ Authors: Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb,
+ Thomas M. Rasmussen, Jeremy Avigad
+
+
+Defines congruence (notation: [x = y] (mod z)) for natural numbers and
+integers.
+
+This file combines and revises a number of prior developments.
+
+The original theories "GCD" and "Primes" were by Christophe Tabacznyj
+and Lawrence C. Paulson, based on \cite{davenport92}. They introduced
+gcd, lcm, and prime for the natural numbers.
+
+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".
+
+The original theory, "IntPrimes", by Thomas M. Rasmussen, defined and
+developed the congruence relations on the integers. The notion was
+extended to the natural numbers by Chiaeb. Jeremy Avigad combined
+these, revised and tidied them, made the development uniform for the
+natural numbers and the integers, and added a number of new theorems.
+
+*)
+
+
+header {* Congruence *}
+
+theory Cong
+imports GCD
+begin
+
+subsection {* Turn off One_nat_def *}
+
+lemma nat_induct' [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 nat_cases [case_names zero plus1, cases type: nat]:
+ "P (0::nat) \<Longrightarrow> (!!n. P (n + 1)) \<Longrightarrow> P n"
+by(metis nat_induct')
+
+lemma power_plus_one [simp]: "(x::'a::power)^(n + 1) = x * x^n"
+by (simp add: One_nat_def)
+
+lemma nat_power_eq_one_eq [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)
+
+(* why wasn't card_insert_if a simp rule? *)
+declare card_insert_disjoint [simp del]
+
+lemma nat_1' [simp]: "nat 1 = 1"
+by simp
+
+(* For those annoying moments where Suc reappears *)
+lemma Suc_remove: "Suc n = n + 1"
+by simp
+
+declare nat_1 [simp del]
+declare add_2_eq_Suc [simp del]
+declare add_2_eq_Suc' [simp del]
+
+
+declare mod_pos_pos_trivial [simp]
+
+
+subsection {* Main definitions *}
+
+class cong =
+
+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)"
+
+end
+
+(* definitions for the natural numbers *)
+
+instantiation nat :: cong
+
+begin
+
+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
+
+end
+
+
+(* definitions for the integers *)
+
+instantiation int :: cong
+
+begin
+
+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
+
+end
+
+
+subsection {* Set up Transfer *}
+
+
+lemma transfer_nat_int_cong:
+ "(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
+ 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 assumption
+done
+
+declare TransferMorphism_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
+
+declare TransferMorphism_int_nat[transfer add return:
+ transfer_int_nat_cong]
+
+
+subsection {* Congruence *}
+
+(* was zcong_0, etc. *)
+lemma nat_cong_0 [simp, presburger]: "([(a::nat) = b] (mod 0)) = (a = b)"
+ by (unfold cong_nat_def, auto)
+
+lemma int_cong_0 [simp, presburger]: "([(a::int) = b] (mod 0)) = (a = b)"
+ by (unfold cong_int_def, auto)
+
+lemma nat_cong_1 [simp, presburger]: "[(a::nat) = b] (mod 1)"
+ by (unfold cong_nat_def, auto)
+
+lemma nat_cong_Suc_0 [simp, presburger]: "[(a::nat) = b] (mod Suc 0)"
+ by (unfold cong_nat_def, auto simp add: One_nat_def)
+
+lemma int_cong_1 [simp, presburger]: "[(a::int) = b] (mod 1)"
+ by (unfold cong_int_def, auto)
+
+lemma nat_cong_refl [simp]: "[(k::nat) = k] (mod m)"
+ by (unfold cong_nat_def, auto)
+
+lemma int_cong_refl [simp]: "[(k::int) = k] (mod m)"
+ by (unfold cong_int_def, auto)
+
+lemma nat_cong_sym: "[(a::nat) = b] (mod m) \<Longrightarrow> [b = a] (mod m)"
+ by (unfold cong_nat_def, auto)
+
+lemma int_cong_sym: "[(a::int) = b] (mod m) \<Longrightarrow> [b = a] (mod m)"
+ by (unfold cong_int_def, auto)
+
+lemma nat_cong_sym_eq: "[(a::nat) = b] (mod m) = [b = a] (mod m)"
+ by (unfold cong_nat_def, auto)
+
+lemma int_cong_sym_eq: "[(a::int) = b] (mod m) = [b = a] (mod m)"
+ by (unfold cong_int_def, auto)
+
+lemma nat_cong_trans [trans]:
+ "[(a::nat) = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)"
+ by (unfold cong_nat_def, auto)
+
+lemma int_cong_trans [trans]:
+ "[(a::int) = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)"
+ by (unfold cong_int_def, auto)
+
+lemma nat_cong_add:
+ "[(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
+
+lemma int_cong_add:
+ "[(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_add_left_eq)
+ apply (subst (1 2) mod_add_right_eq)
+ apply simp
+done
+
+lemma int_cong_diff:
+ "[(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
+
+lemma int_cong_diff_aux:
+ "(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: int_cong_diff)
+done;
+
+lemma nat_cong_diff:
+ assumes "(a::nat) >= c" and "b >= d" and "[a = b] (mod m)" and
+ "[c = d] (mod m)"
+ shows "[a - c = b - d] (mod m)"
+
+ using prems by (rule int_cong_diff_aux [transferred]);
+
+lemma nat_cong_mult:
+ "[(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_mult_eq)
+ apply simp
+done
+
+lemma int_cong_mult:
+ "[(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) zmod_zmult1_eq)
+ apply (subst (1 2) mult_commute)
+ apply (subst (1 2) zmod_zmult1_eq)
+ apply simp
+done
+
+lemma nat_cong_exp: "[(x::nat) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
+ apply (induct k)
+ apply (auto simp add: nat_cong_refl nat_cong_mult)
+done
+
+lemma int_cong_exp: "[(x::int) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
+ apply (induct k)
+ apply (auto simp add: int_cong_refl int_cong_mult)
+done
+
+lemma nat_cong_setsum [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 (induct set: finite)
+ apply (auto intro: nat_cong_add)
+done
+
+lemma int_cong_setsum [rule_format]:
+ "(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 (induct set: finite)
+ apply (auto intro: int_cong_add)
+done
+
+lemma nat_cong_setprod [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 (induct set: finite)
+ apply (auto intro: nat_cong_mult)
+done
+
+lemma int_cong_setprod [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 (induct set: finite)
+ apply (auto intro: int_cong_mult)
+done
+
+lemma nat_cong_scalar: "[(a::nat)= b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)"
+ by (rule nat_cong_mult, simp_all)
+
+lemma int_cong_scalar: "[(a::int)= b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)"
+ by (rule int_cong_mult, simp_all)
+
+lemma nat_cong_scalar2: "[(a::nat)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)"
+ by (rule nat_cong_mult, simp_all)
+
+lemma int_cong_scalar2: "[(a::int)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)"
+ by (rule int_cong_mult, simp_all)
+
+lemma nat_cong_mult_self: "[(a::nat) * m = 0] (mod m)"
+ by (unfold cong_nat_def, auto)
+
+lemma int_cong_mult_self: "[(a::int) * m = 0] (mod m)"
+ by (unfold cong_int_def, auto)
+
+lemma int_cong_eq_diff_cong_0: "[(a::int) = b] (mod m) = [a - b = 0] (mod m)"
+ apply (rule iffI)
+ apply (erule int_cong_diff [of a b m b b, simplified])
+ apply (erule int_cong_add [of "a - b" 0 m b b, simplified])
+done
+
+lemma int_cong_eq_diff_cong_0_aux: "a >= b \<Longrightarrow>
+ [(a::int) = b] (mod m) = [tsub a b = 0] (mod m)"
+ by (subst tsub_eq, assumption, rule int_cong_eq_diff_cong_0)
+
+lemma nat_cong_eq_diff_cong_0:
+ assumes "(a::nat) >= b"
+ shows "[a = b] (mod m) = [a - b = 0] (mod m)"
+
+ using prems by (rule int_cong_eq_diff_cong_0_aux [transferred])
+
+lemma nat_cong_diff_cong_0':
+ "[(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 (frule nat_cong_eq_diff_cong_0 [where m = n])
+ apply auto [1]
+ apply (subgoal_tac "x <= y")
+ apply (frule nat_cong_eq_diff_cong_0 [where m = n])
+ apply (subst nat_cong_sym_eq)
+ apply auto
+done
+
+lemma nat_cong_altdef: "(a::nat) >= b \<Longrightarrow> [a = b] (mod m) = (m dvd (a - b))"
+ apply (subst nat_cong_eq_diff_cong_0, assumption)
+ apply (unfold cong_nat_def)
+ apply (simp add: dvd_eq_mod_eq_0 [symmetric])
+done
+
+lemma int_cong_altdef: "[(a::int) = b] (mod m) = (m dvd (a - b))"
+ apply (subst int_cong_eq_diff_cong_0)
+ apply (unfold cong_int_def)
+ apply (simp add: dvd_eq_mod_eq_0 [symmetric])
+done
+
+lemma int_cong_abs: "[(x::int) = y] (mod abs m) = [x = y] (mod m)"
+ by (simp add: int_cong_altdef)
+
+lemma int_cong_square:
+ "\<lbrakk> prime (p::int); 0 < a; [a * a = 1] (mod p) \<rbrakk>
+ \<Longrightarrow> [a = 1] (mod p) \<or> [a = - 1] (mod p)"
+ apply (simp only: int_cong_altdef)
+ apply (subst int_prime_dvd_mult_eq [symmetric], assumption)
+ (* any way around this? *)
+ apply (subgoal_tac "a * a - 1 = (a - 1) * (a - -1)")
+ apply (auto simp add: ring_simps)
+done
+
+lemma int_cong_mult_rcancel:
+ "coprime k (m::int) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
+ apply (subst (1 2) int_cong_altdef)
+ apply (subst left_diff_distrib [symmetric])
+ apply (rule int_coprime_dvd_mult_iff)
+ apply (subst int_gcd_commute, assumption)
+done
+
+lemma nat_cong_mult_rcancel:
+ assumes "coprime k (m::nat)"
+ shows "[a * k = b * k] (mod m) = [a = b] (mod m)"
+
+ apply (rule int_cong_mult_rcancel [transferred])
+ using prems apply auto
+done
+
+lemma nat_cong_mult_lcancel:
+ "coprime k (m::nat) \<Longrightarrow> [k * a = k * b ] (mod m) = [a = b] (mod m)"
+ by (simp add: mult_commute nat_cong_mult_rcancel)
+
+lemma int_cong_mult_lcancel:
+ "coprime k (m::int) \<Longrightarrow> [k * a = k * b] (mod m) = [a = b] (mod m)"
+ by (simp add: mult_commute int_cong_mult_rcancel)
+
+(* was zcong_zgcd_zmult_zmod *)
+lemma int_coprime_cong_mult:
+ "[(a::int) = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n
+ \<Longrightarrow> [a = b] (mod m * n)"
+ apply (simp only: int_cong_altdef)
+ apply (erule (2) int_divides_mult)
+done
+
+lemma nat_coprime_cong_mult:
+ assumes "[(a::nat) = b] (mod m)" and "[a = b] (mod n)" and "coprime m n"
+ shows "[a = b] (mod m * n)"
+
+ apply (rule int_coprime_cong_mult [transferred])
+ using prems apply auto
+done
+
+lemma nat_cong_less_imp_eq: "0 \<le> (a::nat) \<Longrightarrow>
+ a < m \<Longrightarrow> 0 \<le> b \<Longrightarrow> b < m \<Longrightarrow> [a = b] (mod m) \<Longrightarrow> a = b"
+ by (auto simp add: cong_nat_def mod_pos_pos_trivial)
+
+lemma int_cong_less_imp_eq: "0 \<le> (a::int) \<Longrightarrow>
+ a < m \<Longrightarrow> 0 \<le> b \<Longrightarrow> b < m \<Longrightarrow> [a = b] (mod m) \<Longrightarrow> a = b"
+ by (auto simp add: cong_int_def mod_pos_pos_trivial)
+
+lemma nat_cong_less_unique:
+ "0 < (m::nat) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
+ apply auto
+ apply (rule_tac x = "a mod m" in exI)
+ apply (unfold cong_nat_def, auto)
+done
+
+lemma int_cong_less_unique:
+ "0 < (m::int) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
+ apply auto
+ apply (rule_tac x = "a mod m" in exI)
+ apply (unfold cong_int_def, auto simp add: mod_pos_pos_trivial)
+done
+
+lemma int_cong_iff_lin: "([(a::int) = b] (mod m)) = (\<exists>k. b = a + m * k)"
+ apply (auto simp add: int_cong_altdef dvd_def ring_simps)
+ apply (rule_tac [!] x = "-k" in exI, auto)
+done
+
+lemma nat_cong_iff_lin: "([(a::nat) = b] (mod m)) =
+ (\<exists>k1 k2. b + k1 * m = a + k2 * m)"
+ apply (rule iffI)
+ apply (case_tac "b <= a")
+ apply (subst (asm) nat_cong_altdef, assumption)
+ apply (unfold dvd_def, auto)
+ apply (rule_tac x = k in exI)
+ apply (rule_tac x = 0 in exI)
+ apply (auto simp add: ring_simps)
+ apply (subst (asm) nat_cong_sym_eq)
+ apply (subst (asm) nat_cong_altdef)
+ apply force
+ apply (unfold dvd_def, auto)
+ apply (rule_tac x = 0 in exI)
+ apply (rule_tac x = k in exI)
+ apply (auto simp add: ring_simps)
+ apply (unfold cong_nat_def)
+ apply (subgoal_tac "a mod m = (a + k2 * m) mod m")
+ apply (erule ssubst)back
+ apply (erule subst)
+ apply auto
+done
+
+lemma int_cong_gcd_eq: "[(a::int) = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
+ apply (subst (asm) int_cong_iff_lin, auto)
+ apply (subst add_commute)
+ apply (subst (2) int_gcd_commute)
+ apply (subst mult_commute)
+ apply (subst int_gcd_add_mult)
+ apply (rule int_gcd_commute)
+done
+
+lemma nat_cong_gcd_eq:
+ assumes "[(a::nat) = b] (mod m)"
+ shows "gcd a m = gcd b m"
+
+ apply (rule int_cong_gcd_eq [transferred])
+ using prems apply auto
+done
+
+lemma nat_cong_imp_coprime: "[(a::nat) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow>
+ coprime b m"
+ by (auto simp add: nat_cong_gcd_eq)
+
+lemma int_cong_imp_coprime: "[(a::int) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow>
+ coprime b m"
+ by (auto simp add: int_cong_gcd_eq)
+
+lemma nat_cong_cong_mod: "[(a::nat) = b] (mod m) =
+ [a mod m = b mod m] (mod m)"
+ by (auto simp add: cong_nat_def)
+
+lemma int_cong_cong_mod: "[(a::int) = b] (mod m) =
+ [a mod m = b mod m] (mod m)"
+ by (auto simp add: cong_int_def)
+
+lemma int_cong_minus [iff]: "[(a::int) = b] (mod -m) = [a = b] (mod m)"
+ by (subst (1 2) int_cong_altdef, auto)
+
+lemma nat_cong_zero [iff]: "[(a::nat) = b] (mod 0) = (a = b)"
+ by (auto simp add: cong_nat_def)
+
+lemma int_cong_zero [iff]: "[(a::int) = b] (mod 0) = (a = b)"
+ by (auto simp add: cong_int_def)
+
+(*
+lemma int_mod_dvd_mod:
+ "0 < (m::int) \<Longrightarrow> m dvd b \<Longrightarrow> (a mod b mod m) = (a mod m)"
+ apply (unfold dvd_def, auto)
+ apply (rule mod_mod_cancel)
+ apply auto
+done
+
+lemma mod_dvd_mod:
+ assumes "0 < (m::nat)" and "m dvd b"
+ shows "(a mod b mod m) = (a mod m)"
+
+ apply (rule int_mod_dvd_mod [transferred])
+ using prems apply auto
+done
+*)
+
+lemma nat_cong_add_lcancel:
+ "[(a::nat) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
+ by (simp add: nat_cong_iff_lin)
+
+lemma int_cong_add_lcancel:
+ "[(a::int) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
+ by (simp add: int_cong_iff_lin)
+
+lemma nat_cong_add_rcancel: "[(x::nat) + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
+ by (simp add: nat_cong_iff_lin)
+
+lemma int_cong_add_rcancel: "[(x::int) + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
+ by (simp add: int_cong_iff_lin)
+
+lemma nat_cong_add_lcancel_0: "[(a::nat) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
+ by (simp add: nat_cong_iff_lin)
+
+lemma int_cong_add_lcancel_0: "[(a::int) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
+ by (simp add: int_cong_iff_lin)
+
+lemma nat_cong_add_rcancel_0: "[x + (a::nat) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
+ by (simp add: nat_cong_iff_lin)
+
+lemma int_cong_add_rcancel_0: "[x + (a::int) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
+ by (simp add: int_cong_iff_lin)
+
+lemma nat_cong_dvd_modulus: "[(x::nat) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow>
+ [x = y] (mod n)"
+ apply (auto simp add: nat_cong_iff_lin dvd_def)
+ apply (rule_tac x="k1 * k" in exI)
+ apply (rule_tac x="k2 * k" in exI)
+ apply (simp add: ring_simps)
+done
+
+lemma int_cong_dvd_modulus: "[(x::int) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow>
+ [x = y] (mod n)"
+ by (auto simp add: int_cong_altdef dvd_def)
+
+lemma nat_cong_dvd_eq: "[(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)
+
+lemma int_cong_dvd_eq: "[(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)
+
+lemma nat_cong_mod: "(n::nat) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)"
+ by (simp add: cong_nat_def)
+
+lemma int_cong_mod: "(n::int) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)"
+ by (simp add: cong_int_def)
+
+lemma nat_mod_mult_cong: "(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)
+
+lemma int_neg_cong: "([(a::int) = b] (mod m)) = ([-a = -b] (mod m))"
+ apply (simp add: int_cong_altdef)
+ apply (subst dvd_minus_iff [symmetric])
+ apply (simp add: ring_simps)
+done
+
+lemma int_cong_modulus_neg: "([(a::int) = b] (mod m)) = ([a = b] (mod -m))"
+ by (auto simp add: int_cong_altdef)
+
+lemma int_mod_mult_cong: "(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 (simp add: cong_int_def mod_mod_cancel mod_add_left_eq)
+ apply (subst (1 2) int_cong_modulus_neg)
+ 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
+
+lemma nat_cong_to_1: "([(a::nat) = 1] (mod n)) \<Longrightarrow> (n dvd (a - 1))"
+ apply (case_tac "a = 0")
+ apply force
+ apply (subst (asm) nat_cong_altdef)
+ apply auto
+done
+
+lemma nat_0_cong_1: "[(0::nat) = 1] (mod n) = (n = 1)"
+ by (unfold cong_nat_def, auto)
+
+lemma int_0_cong_1: "[(0::int) = 1] (mod n) = ((n = 1) | (n = -1))"
+ by (unfold cong_int_def, auto simp add: zmult_eq_1_iff)
+
+lemma nat_cong_to_1': "[(a::nat) = 1] (mod n) \<longleftrightarrow>
+ a = 0 \<and> n = 1 \<or> (\<exists>m. a = 1 + m * n)"
+ apply (case_tac "n = 1")
+ apply auto [1]
+ apply (drule_tac x = "a - 1" in spec)
+ apply force
+ apply (case_tac "a = 0")
+ apply (auto simp add: nat_0_cong_1) [1]
+ apply (rule iffI)
+ apply (drule nat_cong_to_1)
+ apply (unfold dvd_def)
+ apply auto [1]
+ apply (rule_tac x = k in exI)
+ apply (auto simp add: ring_simps) [1]
+ apply (subst nat_cong_altdef)
+ apply (auto simp add: dvd_def)
+done
+
+lemma nat_cong_le: "(y::nat) <= x \<Longrightarrow> [x = y] (mod n) \<longleftrightarrow> (\<exists>q. x = q * n + y)"
+ apply (subst nat_cong_altdef)
+ apply assumption
+ apply (unfold dvd_def, auto simp add: ring_simps)
+ apply (rule_tac x = k in exI)
+ apply auto
+done
+
+lemma nat_cong_solve: "(a::nat) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)"
+ apply (case_tac "n = 0")
+ apply force
+ apply (frule nat_bezout [of a n], auto)
+ apply (rule exI, erule ssubst)
+ apply (rule nat_cong_trans)
+ apply (rule nat_cong_add)
+ apply (subst mult_commute)
+ apply (rule nat_cong_mult_self)
+ prefer 2
+ apply simp
+ apply (rule nat_cong_refl)
+ apply (rule nat_cong_refl)
+done
+
+lemma int_cong_solve: "(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 auto
+ apply (rule_tac x = "-1" in exI)
+ apply auto
+ apply (insert int_bezout [of a n], auto)
+ apply (rule exI)
+ apply (erule subst)
+ apply (rule int_cong_trans)
+ prefer 2
+ apply (rule int_cong_add)
+ apply (rule int_cong_refl)
+ apply (rule int_cong_sym)
+ apply (rule int_cong_mult_self)
+ apply simp
+ apply (subst mult_commute)
+ apply (rule int_cong_refl)
+done
+
+lemma nat_cong_solve_dvd:
+ assumes a: "(a::nat) \<noteq> 0" and b: "gcd a n dvd d"
+ shows "EX x. [a * x = d] (mod n)"
+proof -
+ from nat_cong_solve [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)"
+ by (elim nat_cong_scalar2)
+ also from b have "(d div gcd a n) * gcd a n = d"
+ by (rule dvd_div_mult_self)
+ also have "(d div gcd a n) * (a * x) = a * (d div gcd a n * x)"
+ by auto
+ finally show ?thesis
+ by auto
+qed
+
+lemma int_cong_solve_dvd:
+ assumes a: "(a::int) \<noteq> 0" and b: "gcd a n dvd d"
+ shows "EX x. [a * x = d] (mod n)"
+proof -
+ from int_cong_solve [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)"
+ by (elim int_cong_scalar2)
+ also from b have "(d div gcd a n) * gcd a n = d"
+ by (rule dvd_div_mult_self)
+ also have "(d div gcd a n) * (a * x) = a * (d div gcd a n * x)"
+ by auto
+ finally show ?thesis
+ by auto
+qed
+
+lemma nat_cong_solve_coprime: "coprime (a::nat) n \<Longrightarrow>
+ EX x. [a * x = 1] (mod n)"
+ apply (case_tac "a = 0")
+ apply force
+ apply (frule nat_cong_solve [of a n])
+ apply auto
+done
+
+lemma int_cong_solve_coprime: "coprime (a::int) n \<Longrightarrow>
+ EX x. [a * x = 1] (mod n)"
+ apply (case_tac "a = 0")
+ apply auto
+ apply (case_tac "n \<ge> 0")
+ apply auto
+ apply (subst cong_int_def, auto)
+ apply (frule int_cong_solve [of a n])
+ apply auto
+done
+
+lemma nat_coprime_iff_invertible: "m > (1::nat) \<Longrightarrow> coprime a m =
+ (EX x. [a * x = 1] (mod m))"
+ apply (auto intro: nat_cong_solve_coprime)
+ apply (unfold cong_nat_def, auto intro: nat_invertible_coprime)
+done
+
+lemma int_coprime_iff_invertible: "m > (1::int) \<Longrightarrow> coprime a m =
+ (EX x. [a * x = 1] (mod m))"
+ apply (auto intro: int_cong_solve_coprime)
+ apply (unfold cong_int_def)
+ apply (auto intro: int_invertible_coprime)
+done
+
+lemma int_coprime_iff_invertible': "m > (1::int) \<Longrightarrow> coprime a m =
+ (EX x. 0 <= x & x < m & [a * x = 1] (mod m))"
+ apply (subst int_coprime_iff_invertible)
+ 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
+
+
+lemma nat_cong_cong_lcm: "[(x::nat) = y] (mod a) \<Longrightarrow>
+ [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
+ apply (case_tac "y \<le> x")
+ apply (auto simp add: nat_cong_altdef nat_lcm_least) [1]
+ apply (rule nat_cong_sym)
+ apply (subst (asm) (1 2) nat_cong_sym_eq)
+ apply (auto simp add: nat_cong_altdef nat_lcm_least)
+done
+
+lemma int_cong_cong_lcm: "[(x::int) = y] (mod a) \<Longrightarrow>
+ [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
+ by (auto simp add: int_cong_altdef int_lcm_least) [1]
+
+lemma nat_cong_cong_coprime: "coprime a b \<Longrightarrow> [(x::nat) = y] (mod a) \<Longrightarrow>
+ [x = y] (mod b) \<Longrightarrow> [x = y] (mod a * b)"
+ apply (frule (1) nat_cong_cong_lcm)back
+ apply (simp add: lcm_nat_def)
+done
+
+lemma int_cong_cong_coprime: "coprime a b \<Longrightarrow> [(x::int) = y] (mod a) \<Longrightarrow>
+ [x = y] (mod b) \<Longrightarrow> [x = y] (mod a * b)"
+ apply (frule (1) int_cong_cong_lcm)back
+ apply (simp add: int_lcm_altdef int_cong_abs abs_mult [symmetric])
+done
+
+lemma nat_cong_cong_setprod_coprime [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))"
+ apply (induct set: finite)
+ apply auto
+ apply (rule nat_cong_cong_coprime)
+ apply (subst nat_gcd_commute)
+ apply (rule nat_setprod_coprime)
+ apply auto
+done
+
+lemma int_cong_cong_setprod_coprime [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::int) = y] (mod m i)) \<longrightarrow>
+ [x = y] (mod (PROD i:A. m i))"
+ apply (induct set: finite)
+ apply auto
+ apply (rule int_cong_cong_coprime)
+ apply (subst int_gcd_commute)
+ apply (rule int_setprod_coprime)
+ apply auto
+done
+
+lemma nat_binary_chinese_remainder_aux:
+ 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 nat_cong_solve_coprime [OF a]
+ obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
+ by auto
+ from a have b: "coprime m2 m1"
+ by (subst nat_gcd_commute)
+ from nat_cong_solve_coprime [OF b]
+ obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
+ by auto
+ have "[m1 * x1 = 0] (mod m1)"
+ by (subst mult_commute, rule nat_cong_mult_self)
+ moreover have "[m2 * x2 = 0] (mod m2)"
+ by (subst mult_commute, rule nat_cong_mult_self)
+ moreover note one two
+ ultimately show ?thesis by blast
+qed
+
+lemma int_binary_chinese_remainder_aux:
+ 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 int_cong_solve_coprime [OF a]
+ obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
+ by auto
+ from a have b: "coprime m2 m1"
+ by (subst int_gcd_commute)
+ from int_cong_solve_coprime [OF b]
+ obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
+ by auto
+ have "[m1 * x1 = 0] (mod m1)"
+ by (subst mult_commute, rule int_cong_mult_self)
+ moreover have "[m2 * x2 = 0] (mod m2)"
+ by (subst mult_commute, rule int_cong_mult_self)
+ moreover note one two
+ ultimately show ?thesis by blast
+qed
+
+lemma nat_binary_chinese_remainder:
+ assumes a: "coprime (m1::nat) m2"
+ shows "EX x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
+proof -
+ from nat_binary_chinese_remainder_aux [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)"
+ by blast
+ let ?x = "u1 * b1 + u2 * b2"
+ have "[?x = u1 * 1 + u2 * 0] (mod m1)"
+ apply (rule nat_cong_add)
+ apply (rule nat_cong_scalar2)
+ apply (rule `[b1 = 1] (mod m1)`)
+ apply (rule nat_cong_scalar2)
+ apply (rule `[b2 = 0] (mod m1)`)
+ done
+ hence "[?x = u1] (mod m1)" by simp
+ have "[?x = u1 * 0 + u2 * 1] (mod m2)"
+ apply (rule nat_cong_add)
+ apply (rule nat_cong_scalar2)
+ apply (rule `[b1 = 0] (mod m2)`)
+ apply (rule nat_cong_scalar2)
+ apply (rule `[b2 = 1] (mod m2)`)
+ done
+ hence "[?x = u2] (mod m2)" by simp
+ with `[?x = u1] (mod m1)` show ?thesis by blast
+qed
+
+lemma int_binary_chinese_remainder:
+ assumes a: "coprime (m1::int) m2"
+ shows "EX x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
+proof -
+ from int_binary_chinese_remainder_aux [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)"
+ by blast
+ let ?x = "u1 * b1 + u2 * b2"
+ have "[?x = u1 * 1 + u2 * 0] (mod m1)"
+ apply (rule int_cong_add)
+ apply (rule int_cong_scalar2)
+ apply (rule `[b1 = 1] (mod m1)`)
+ apply (rule int_cong_scalar2)
+ apply (rule `[b2 = 0] (mod m1)`)
+ done
+ hence "[?x = u1] (mod m1)" by simp
+ have "[?x = u1 * 0 + u2 * 1] (mod m2)"
+ apply (rule int_cong_add)
+ apply (rule int_cong_scalar2)
+ apply (rule `[b1 = 0] (mod m2)`)
+ apply (rule int_cong_scalar2)
+ apply (rule `[b2 = 1] (mod m2)`)
+ done
+ hence "[?x = u2] (mod m2)" by simp
+ with `[?x = u1] (mod m1)` show ?thesis by blast
+qed
+
+lemma nat_cong_modulus_mult: "[(x::nat) = y] (mod m * n) \<Longrightarrow>
+ [x = y] (mod m)"
+ apply (case_tac "y \<le> x")
+ apply (simp add: nat_cong_altdef)
+ apply (erule dvd_mult_left)
+ apply (rule nat_cong_sym)
+ apply (subst (asm) nat_cong_sym_eq)
+ apply (simp add: nat_cong_altdef)
+ apply (erule dvd_mult_left)
+done
+
+lemma int_cong_modulus_mult: "[(x::int) = y] (mod m * n) \<Longrightarrow>
+ [x = y] (mod m)"
+ apply (simp add: int_cong_altdef)
+ apply (erule dvd_mult_left)
+done
+
+lemma nat_cong_less_modulus_unique:
+ "[(x::nat) = y] (mod m) \<Longrightarrow> x < m \<Longrightarrow> y < m \<Longrightarrow> x = y"
+ by (simp add: cong_nat_def)
+
+lemma nat_binary_chinese_remainder_unique:
+ 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 nat_binary_chinese_remainder [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
+ have one: "[?x = u1] (mod m1)"
+ apply (rule nat_cong_trans)
+ prefer 2
+ apply (rule `[y = u1] (mod m1)`)
+ apply (rule nat_cong_modulus_mult)
+ apply (rule nat_cong_mod)
+ using nz apply auto
+ done
+ have two: "[?x = u2] (mod m2)"
+ apply (rule nat_cong_trans)
+ prefer 2
+ apply (rule `[y = u2] (mod m2)`)
+ apply (subst mult_commute)
+ apply (rule nat_cong_modulus_mult)
+ apply (rule nat_cong_mod)
+ 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)
+ fix z
+ assume "z < m1 * m2"
+ assume "[z = u1] (mod m1)" and "[z = u2] (mod m2)"
+ have "[?x = z] (mod m1)"
+ apply (rule nat_cong_trans)
+ apply (rule `[?x = u1] (mod m1)`)
+ apply (rule nat_cong_sym)
+ apply (rule `[z = u1] (mod m1)`)
+ done
+ moreover have "[?x = z] (mod m2)"
+ apply (rule nat_cong_trans)
+ apply (rule `[?x = u2] (mod m2)`)
+ apply (rule nat_cong_sym)
+ apply (rule `[z = u2] (mod m2)`)
+ done
+ ultimately have "[?x = z] (mod m1 * m2)"
+ by (auto intro: nat_coprime_cong_mult a)
+ with `z < m1 * m2` `?x < m1 * m2` show "z = ?x"
+ apply (intro nat_cong_less_modulus_unique)
+ apply (auto, erule nat_cong_sym)
+ done
+ qed
+ with less one two show ?thesis
+ by auto
+ qed
+
+lemma nat_chinese_remainder_aux:
+ 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 nat_setprod_coprime, auto)
+ hence "EX x. [(PROD j : A - {i}. m j) * x = 1] (mod m i)"
+ by (elim nat_cong_solve_coprime)
+ 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]
+ (mod (PROD j : A - {i}. m j))"
+ by (subst mult_commute, rule nat_cong_mult_self)
+ ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0]
+ (mod setprod m (A - {i}))"
+ by blast
+qed
+
+lemma nat_chinese_remainder:
+ 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 nat_chinese_remainder_aux [OF fin cop] obtain b where
+ 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)"
+ show "?thesis"
+ proof (rule exI, clarify)
+ fix i
+ assume a: "i : A"
+ show "[?x = u i] (mod m i)"
+ proof -
+ 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)"
+ 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)"
+ apply (rule nat_cong_add)
+ apply (rule nat_cong_scalar2)
+ using bprop a apply blast
+ apply (rule nat_cong_setsum)
+ apply (rule nat_cong_scalar2)
+ using bprop apply auto
+ apply (rule nat_cong_dvd_modulus)
+ apply (drule (1) bspec)
+ apply (erule conjE)
+ apply assumption
+ apply (rule dvd_setprod)
+ using fin a apply auto
+ done
+ finally show ?thesis
+ by simp
+ qed
+ qed
+qed
+
+lemma nat_coprime_cong_prod [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))"
+ apply (induct set: finite)
+ apply auto
+ apply (erule (1) nat_coprime_cong_mult)
+ apply (subst nat_gcd_commute)
+ apply (rule nat_setprod_coprime)
+ apply auto
+done
+
+lemma nat_chinese_remainder_unique:
+ 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 nat_chinese_remainder [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)"
+ by auto
+ have cong: "ALL i:A. [?x = u i] (mod m i)"
+ apply auto
+ apply (rule nat_cong_trans)
+ prefer 2
+ using one apply auto
+ apply (rule nat_cong_dvd_modulus)
+ apply (rule nat_cong_mod)
+ using prodnz apply auto
+ apply (rule dvd_setprod)
+ apply (rule fin)
+ apply assumption
+ done
+ 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 (rule nat_cong_trans)
+ using cong apply (erule bspec)
+ apply (rule nat_cong_sym)
+ using zcong apply auto
+ done
+ with fin cop have "[?x = z] (mod (PROD i:A. m i))"
+ by (intro nat_coprime_cong_prod, auto)
+ with zless less show "z = ?x"
+ apply (intro nat_cong_less_modulus_unique)
+ apply (auto, erule nat_cong_sym)
+ done
+ qed
+ from less cong unique show ?thesis
+ by blast
+qed
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NewNumberTheory/Fib.thy Fri Jun 19 18:33:10 2009 +0200
@@ -0,0 +1,319 @@
+(* Title: Fib.thy
+ Authors: Lawrence C. Paulson, Jeremy Avigad
+
+
+Defines the fibonacci function.
+
+The original "Fib" is due to Lawrence C. Paulson, and was adapted by
+Jeremy Avigad.
+*)
+
+
+header {* Fib *}
+
+theory Fib
+imports Binomial
+begin
+
+
+subsection {* Main definitions *}
+
+class fib =
+
+fixes
+ fib :: "'a \<Rightarrow> 'a"
+
+
+(* definition for the natural numbers *)
+
+instantiation nat :: fib
+
+begin
+
+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
+
+end
+
+(* definition for the integers *)
+
+instantiation int :: fib
+
+begin
+
+definition
+ fib_int :: "int \<Rightarrow> int"
+where
+ "fib_int n = (if n >= 0 then int (fib (nat n)) else 0)"
+
+instance proof qed
+
+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
+
+lemma transfer_nat_int_fib_closure:
+ "n >= (0::int) \<Longrightarrow> fib n >= 0"
+ by (auto simp add: fib_int_def)
+
+declare TransferMorphism_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)"
+ unfolding fib_int_def by auto
+
+lemma transfer_int_nat_fib_closure:
+ "is_nat n \<Longrightarrow> fib n >= 0"
+ unfolding fib_int_def by auto
+
+declare TransferMorphism_int_nat[transfer add return:
+ transfer_int_nat_fib transfer_int_nat_fib_closure]
+
+
+subsection {* Fibonacci numbers *}
+
+lemma nat_fib_0 [simp]: "fib (0::nat) = 0"
+ by simp
+
+lemma int_fib_0 [simp]: "fib (0::int) = 0"
+ unfolding fib_int_def by simp
+
+lemma nat_fib_1 [simp]: "fib (1::nat) = 1"
+ by simp
+
+lemma nat_fib_Suc_0 [simp]: "fib (Suc 0) = Suc 0"
+ by simp
+
+lemma int_fib_1 [simp]: "fib (1::int) = 1"
+ unfolding fib_int_def by simp
+
+lemma nat_fib_reduce: "(n::nat) >= 2 \<Longrightarrow> fib n = fib (n - 1) + fib (n - 2)"
+ by simp
+
+declare fib_nat.simps [simp del]
+
+lemma int_fib_reduce: "(n::int) >= 2 \<Longrightarrow> fib n = fib (n - 1) + fib (n - 2)"
+ unfolding fib_int_def
+ by (auto simp add: nat_fib_reduce nat_diff_distrib)
+
+lemma int_fib_neg [simp]: "(n::int) < 0 \<Longrightarrow> fib n = 0"
+ unfolding fib_int_def by auto
+
+lemma nat_fib_2 [simp]: "fib (2::nat) = 1"
+ by (subst nat_fib_reduce, auto)
+
+lemma int_fib_2 [simp]: "fib (2::int) = 1"
+ by (subst int_fib_reduce, auto)
+
+lemma nat_fib_plus_2: "fib ((n::nat) + 2) = fib (n + 1) + fib n"
+ by (subst nat_fib_reduce, auto simp add: One_nat_def)
+(* the need for One_nat_def is due to the natdiff_cancel_numerals
+ procedure *)
+
+lemma nat_fib_induct: "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
+ apply (case_tac "n = 0", force)
+ apply (case_tac "n = 1", force)
+ apply (subgoal_tac "n >= 2")
+ apply (frule_tac x = "n - 1" in spec)
+ apply (drule_tac x = "n - 2" in spec)
+ apply (drule_tac x = "n - 2" in spec)
+ apply auto
+ apply (auto simp add: One_nat_def) (* again, natdiff_cancel *)
+done
+
+lemma nat_fib_add: "fib ((n::nat) + k + 1) = fib (k + 1) * fib (n + 1) +
+ fib k * fib n"
+ apply (induct n rule: nat_fib_induct)
+ apply auto
+ apply (subst nat_fib_reduce)
+ apply (auto simp add: ring_simps)
+ apply (subst (1 3 5) nat_fib_reduce)
+ apply (auto simp add: ring_simps Suc_remove)
+(* 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 auto
+done
+
+lemma nat_fib_add': "fib (n + Suc k) = fib (Suc k) * fib (Suc n) +
+ fib k * fib n"
+ using nat_fib_add by (auto simp add: One_nat_def)
+
+
+(* transfer from nats to ints *)
+lemma int_fib_add [rule_format]: "(n::int) >= 0 \<Longrightarrow> k >= 0 \<Longrightarrow>
+ fib (n + k + 1) = fib (k + 1) * fib (n + 1) +
+ fib k * fib n "
+
+ by (rule nat_fib_add [transferred])
+
+lemma nat_fib_neq_0: "(n::nat) > 0 \<Longrightarrow> fib n ~= 0"
+ apply (induct n rule: nat_fib_induct)
+ apply (auto simp add: nat_fib_plus_2)
+done
+
+lemma nat_fib_gr_0: "(n::nat) > 0 \<Longrightarrow> fib n > 0"
+ by (frule nat_fib_neq_0, simp)
+
+lemma int_fib_gr_0: "(n::int) > 0 \<Longrightarrow> fib n > 0"
+ unfolding fib_int_def by (simp add: nat_fib_gr_0)
+
+text {*
+ \medskip Concrete Mathematics, page 278: Cassini's identity. The proof is
+ much easier using integers, not natural numbers!
+*}
+
+lemma int_fib_Cassini_aux: "fib (int n + 2) * fib (int n) -
+ (fib (int n + 1))^2 = (-1)^(n + 1)"
+ apply (induct n)
+ apply (auto simp add: ring_simps power2_eq_square int_fib_reduce
+ power_add)
+done
+
+lemma int_fib_Cassini: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n -
+ (fib (n + 1))^2 = (-1)^(nat n + 1)"
+ by (insert int_fib_Cassini_aux [of "nat n"], auto)
+
+(*
+lemma int_fib_Cassini': "n >= 0 \<Longrightarrow> fib (n + 2) * fib n =
+ (fib (n + 1))^2 + (-1)^(nat n + 1)"
+ by (frule int_fib_Cassini, simp)
+*)
+
+lemma int_fib_Cassini': "n >= 0 \<Longrightarrow> fib ((n::int) + 2) * fib n =
+ (if even n then tsub ((fib (n + 1))^2) 1
+ else (fib (n + 1))^2 + 1)"
+ apply (frule int_fib_Cassini, auto simp add: pos_int_even_equiv_nat_even)
+ apply (subst tsub_eq)
+ apply (insert int_fib_gr_0 [of "n + 1"], force)
+ apply auto
+done
+
+lemma nat_fib_Cassini: "fib ((n::nat) + 2) * fib n =
+ (if even n then (fib (n + 1))^2 - 1
+ else (fib (n + 1))^2 + 1)"
+
+ by (rule int_fib_Cassini' [transferred, of n], auto)
+
+
+text {* \medskip Toward Law 6.111 of Concrete Mathematics *}
+
+lemma nat_coprime_fib_plus_1: "coprime (fib (n::nat)) (fib (n + 1))"
+ apply (induct n rule: nat_fib_induct)
+ apply auto
+ apply (subst (2) nat_fib_reduce)
+ apply (auto simp add: Suc_remove) (* again, natdiff_cancel *)
+ apply (subst add_commute, auto)
+ apply (subst nat_gcd_commute, auto simp add: ring_simps)
+done
+
+lemma nat_coprime_fib_Suc: "coprime (fib n) (fib (Suc n))"
+ using nat_coprime_fib_plus_1 by (simp add: One_nat_def)
+
+lemma int_coprime_fib_plus_1:
+ "n >= 0 \<Longrightarrow> coprime (fib (n::int)) (fib (n + 1))"
+ by (erule nat_coprime_fib_plus_1 [transferred])
+
+lemma nat_gcd_fib_add: "gcd (fib (m::nat)) (fib (n + m)) = gcd (fib m) (fib n)"
+ apply (simp add: nat_gcd_commute [of "fib m"])
+ apply (rule nat_cases [of _ m])
+ apply simp
+ apply (subst add_assoc [symmetric])
+ apply (simp add: nat_fib_add)
+ apply (subst nat_gcd_commute)
+ apply (subst mult_commute)
+ apply (subst nat_gcd_add_mult)
+ apply (subst nat_gcd_commute)
+ apply (rule nat_gcd_mult_cancel)
+ apply (rule nat_coprime_fib_plus_1)
+done
+
+lemma int_gcd_fib_add [rule_format]: "m >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow>
+ gcd (fib (m::int)) (fib (n + m)) = gcd (fib m) (fib n)"
+ by (erule nat_gcd_fib_add [transferred])
+
+lemma nat_gcd_fib_diff: "(m::nat) \<le> n \<Longrightarrow>
+ gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
+ by (simp add: nat_gcd_fib_add [symmetric, of _ "n-m"])
+
+lemma int_gcd_fib_diff: "0 <= (m::int) \<Longrightarrow> m \<le> n \<Longrightarrow>
+ gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
+ by (simp add: int_gcd_fib_add [symmetric, of _ "n-m"])
+
+lemma nat_gcd_fib_mod: "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
+ with pos_m have pos_n: "0 < 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: less.hyps diff pos_m)
+ also have "\<dots> = gcd (fib m) (fib n)" by (simp add: nat_gcd_fib_diff m_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
+ qed
+qed
+
+lemma int_gcd_fib_mod:
+ assumes "0 < (m::int)" and "0 <= n"
+ shows "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
+
+ apply (rule nat_gcd_fib_mod [transferred])
+ using prems apply auto
+done
+
+lemma nat_fib_gcd: "fib (gcd (m::nat) n) = gcd (fib m) (fib n)"
+ -- {* Law 6.111 *}
+ apply (induct m n rule: nat_gcd_induct)
+ apply (simp_all add: nat_gcd_non_0 nat_gcd_commute nat_gcd_fib_mod)
+done
+
+lemma int_fib_gcd: "m >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow>
+ fib (gcd (m::int) n) = gcd (fib m) (fib n)"
+ by (erule nat_fib_gcd [transferred])
+
+lemma nat_atMost_plus_one: "{..(k::nat) + 1} = insert (k + 1) {..k}"
+ by auto
+
+theorem nat_fib_mult_eq_setsum:
+ "fib ((n::nat) + 1) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
+ apply (induct n)
+ apply (auto simp add: nat_atMost_plus_one nat_fib_plus_2 ring_simps)
+done
+
+theorem nat_fib_mult_eq_setsum':
+ "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
+ using nat_fib_mult_eq_setsum by (simp add: One_nat_def)
+
+theorem int_fib_mult_eq_setsum [rule_format]:
+ "n >= 0 \<Longrightarrow> fib ((n::int) + 1) * fib n = (\<Sum>k \<in> {0..n}. fib k * fib k)"
+ by (erule nat_fib_mult_eq_setsum [transferred])
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NewNumberTheory/MiscAlgebra.thy Fri Jun 19 18:33:10 2009 +0200
@@ -0,0 +1,402 @@
+(* Title: MiscAlgebra.thy
+ ID:
+ Author: Jeremy Avigad
+
+ These are things that can be added to the Algebra library,
+ as well as a few things that could possibly go in Main.
+*)
+
+theory MiscAlgebra
+imports
+ "~~/src/HOL/Algebra/Ring"
+ "~~/src/HOL/Algebra/FiniteProduct"
+begin;
+
+declare One_nat_def [simp del]
+
+
+(* Some things for Main? *)
+
+(* finiteness stuff *)
+
+lemma int_bounded_set1 [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
+done
+
+lemma image_set_eq_image: "{ f x | x. P x} = f ` { x. P x}"
+ unfolding image_def apply auto
+done
+
+lemma finite_image_set [simp]: "finite {x. P x} \<Longrightarrow>
+ finite { f x | x. P x}"
+ apply (subst image_set_eq_image)
+ apply auto
+done
+
+(* Examples:
+
+lemma "finite {x. 0 < x & x < 100 & prime (x::int)}"
+ by auto
+
+lemma "finite { 3 * x | x. 0 < x & x < 100 & prime (x::int) }"
+ by auto
+
+*)
+
+(* This could go in Set.thy *)
+
+lemma UNION_empty: "(UNION F A = {}) = (ALL x: F. (A x) = {})"
+ by auto
+
+
+(* The rest is for the algebra libraries *)
+
+(* This goes in FuncSet.thy. Any reason not to make it a simp rule? *)
+
+lemma funcset_id [simp]: "(%x. x): A \<rightarrow> A"
+ by (auto simp add: Pi_def);
+
+(* These go in Group.thy. *)
+
+(*
+ Show that the units in any monoid give rise to a group.
+
+ The file Residues.thy provides some infrastructure to use
+ facts about the unit group within the ring locale.
+*)
+
+
+constdefs
+ units_of :: "('a, 'b) monoid_scheme => 'a monoid"
+ "units_of G == (| carrier = Units G,
+ Group.monoid.mult = Group.monoid.mult G,
+ one = one G |)";
+
+(*
+
+lemma (in monoid) Units_mult_closed [intro]:
+ "x : Units G ==> y : Units G ==> x \<otimes> y : Units G"
+ apply (unfold Units_def)
+ apply (clarsimp)
+ apply (rule_tac x = "xaa \<otimes> xa" in bexI)
+ apply auto
+ apply (subst m_assoc)
+ apply auto
+ apply (subst (2) m_assoc [symmetric])
+ apply auto
+ apply (subst m_assoc)
+ apply auto
+ apply (subst (2) m_assoc [symmetric])
+ apply auto
+done
+
+*)
+
+lemma (in monoid) units_group: "group(units_of G)"
+ apply (unfold units_of_def)
+ apply (rule groupI)
+ apply auto
+ apply (subst m_assoc)
+ apply auto
+ apply (rule_tac x = "inv x" in bexI)
+ apply auto
+done
+
+lemma (in comm_monoid) units_comm_group: "comm_group(units_of G)"
+ apply (rule group.group_comm_groupI)
+ apply (rule units_group)
+ apply (insert prems)
+ apply (unfold units_of_def Units_def comm_monoid_def comm_monoid_axioms_def)
+ apply auto;
+done;
+
+lemma units_of_carrier: "carrier (units_of G) = Units G"
+ by (unfold units_of_def, auto)
+
+lemma units_of_mult: "mult(units_of G) = mult G"
+ by (unfold units_of_def, auto)
+
+lemma units_of_one: "one(units_of G) = one G"
+ by (unfold units_of_def, auto)
+
+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)
+ apply (rule the1_equality)
+ apply (rule ex_ex1I)
+ apply (subst (asm) Units_def)
+ apply auto
+ apply (erule inv_unique)
+ apply auto
+ apply (rule Units_closed)
+ apply (simp_all only: units_of_carrier [symmetric])
+ apply (insert units_group)
+ apply auto
+ apply (subst units_of_mult [symmetric])
+ apply (subst units_of_one [symmetric])
+ apply (erule group.r_inv, assumption)
+ apply (subst units_of_mult [symmetric])
+ apply (subst units_of_one [symmetric])
+ apply (erule group.l_inv, assumption)
+done
+
+lemma (in group) inj_on_const_mult: "a: (carrier G) ==>
+ inj_on (%x. a \<otimes> x) (carrier G)"
+ by (unfold inj_on_def, auto)
+
+lemma (in group) surj_const_mult: "a : (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
+(* auto should get this. I suppose we need "comm_monoid_simprules"
+ for mult_ac rewriting. *)
+ apply (subst m_assoc [symmetric])
+ apply auto
+done
+
+lemma (in group) l_cancel_one [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
+ (x \<otimes> a = x) = (a = one G)"
+ apply auto
+ apply (subst l_cancel [symmetric])
+ prefer 4
+ apply (erule ssubst)
+ apply auto
+done
+
+lemma (in group) r_cancel_one [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
+ (a \<otimes> x = x) = (a = one G)"
+ apply auto
+ apply (subst r_cancel [symmetric])
+ prefer 4
+ apply (erule ssubst)
+ apply auto
+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)
+
+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)
+
+(* 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"
+proof -
+ have "(\<Otimes>x:carrier G. x) = (\<Otimes>x:carrier G. a \<otimes> x)"
+ 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)
+ also have "(\<Otimes>x:carrier G. a) = a (^) card(carrier G)"
+ by (auto simp add: finprod_const)
+ finally show ?thesis
+(* uses the preceeding lemma *)
+ by auto
+qed
+
+
+(* Miscellaneous *)
+
+lemma (in cring) field_intro2: "\<zero>\<^bsub>R\<^esub> ~= \<one>\<^bsub>R\<^esub> \<Longrightarrow> ALL x : carrier R - {\<zero>\<^bsub>R\<^esub>}.
+ x : Units R \<Longrightarrow> field R"
+ apply (unfold_locales)
+ apply (insert prems, auto)
+ apply (rule trans)
+ apply (subgoal_tac "a = (a \<otimes> b) \<otimes> inv b")
+ apply assumption
+ apply (subst m_assoc)
+ apply (auto simp add: Units_r_inv)
+ apply (unfold Units_def)
+ apply auto
+done
+
+lemma (in monoid) inv_char: "x : carrier G \<Longrightarrow> y : carrier G \<Longrightarrow>
+ x \<otimes> y = \<one> \<Longrightarrow> y \<otimes> x = \<one> \<Longrightarrow> inv x = y"
+ apply (subgoal_tac "x : Units G")
+ apply (subgoal_tac "y = inv x \<otimes> \<one>")
+ apply simp
+ apply (erule subst)
+ apply (subst m_assoc [symmetric])
+ apply auto
+ apply (unfold Units_def)
+ apply auto
+done
+
+lemma (in comm_monoid) comm_inv_char: "x : carrier G \<Longrightarrow> y : carrier G \<Longrightarrow>
+ x \<otimes> y = \<one> \<Longrightarrow> inv x = y"
+ apply (rule inv_char)
+ apply auto
+ apply (subst m_comm, auto)
+done
+
+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>
+ 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
+
+lemma (in ring) Units_minus_one_closed [intro]: "\<ominus> \<one> : Units R"
+ apply (unfold Units_def)
+ apply auto
+ apply (rule_tac x = "\<ominus> \<one>" in bexI)
+ apply auto
+ apply (simp add: l_minus r_minus)
+done
+
+lemma (in monoid) inv_one [simp]: "inv \<one> = \<one>"
+ apply (rule inv_char)
+ apply auto
+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
+
+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
+
+
+(* This goes in FiniteProduct *)
+
+lemma (in comm_monoid) finprod_UN_disjoint:
+ "finite I \<Longrightarrow> (ALL i:I. finite (A i)) \<longrightarrow> (ALL i:I. ALL j:I. i ~= j \<longrightarrow>
+ (A i) Int (A j) = {}) \<longrightarrow>
+ (ALL i:I. ALL x: (A i). g x : carrier G) \<longrightarrow>
+ finprod G g (UNION I A) = finprod G (%i. finprod G g (A i)) I"
+ apply (induct set: finite)
+ apply force
+ apply clarsimp
+ apply (subst finprod_Un_disjoint)
+ apply blast
+ apply (erule finite_UN_I)
+ apply blast
+ apply (subst Int_UN_distrib)
+ apply (subst UNION_empty)
+ apply clarsimp
+ apply (drule_tac x = xa in bspec)back
+ apply (assumption, force)
+ apply (auto intro!: funcsetI finprod_closed)
+ apply (subst finprod_insert)
+ 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"
+ apply (frule finprod_UN_disjoint [of C id f])
+ apply (unfold Union_def id_def, auto)
+done
+
+lemma (in comm_monoid) finprod_one [rule_format]:
+ "finite A \<Longrightarrow> (ALL x:A. f x = \<one>) \<longrightarrow>
+ finprod G f A = \<one>"
+ apply (induct set: finite)
+ apply auto
+ apply (subst finprod_insert)
+ apply (auto intro!: funcsetI)
+done
+
+
+(* 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")
+ apply (erule ssubst)back
+ apply (erule subst)
+ apply (simp add: ring_simprules)+
+done
+
+(* there's a name conflict -- maybe "domain" should be
+ "integral_domain" *)
+
+lemma (in Ring.domain) square_eq_one:
+ fixes x
+ assumes [simp]: "x : carrier R" and
+ "x \<otimes> x = \<one>"
+ shows "x = \<one> | x = \<ominus>\<one>"
+proof -
+ have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = x \<otimes> x \<oplus> \<ominus> \<one>"
+ by (simp add: ring_simprules)
+ 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>"
+ by (intro integral, auto)
+ thus ?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 (rule sum_zero_eq_neg)
+ apply auto
+ done
+qed
+
+lemma (in Ring.domain) inv_eq_self: "x : Units R \<Longrightarrow>
+ x = inv x \<Longrightarrow> x = \<one> | x = \<ominus> \<one>"
+ apply (rule square_eq_one)
+ apply auto
+ apply (erule ssubst)back
+ apply (erule Units_r_inv)
+done
+
+
+(*
+ The following translates theorems about groups to the facts about
+ the units of a ring. (The list should be expanded as more things are
+ needed.)
+*)
+
+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:
+ "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
+ monoid.nat_pow_0 monoid.nat_pow_Suc units_of_one units_of_mult
+ One_nat_def)
+done
+
+lemma (in cring) units_power_order_eq_one: "finite (Units R) \<Longrightarrow> a : Units R
+ \<Longrightarrow> a (^) card(Units R) = \<one>"
+ apply (subst units_of_carrier [symmetric])
+ apply (subst units_of_one [symmetric])
+ apply (subst units_of_pow [symmetric])
+ apply assumption
+ apply (rule comm_group.power_order_eq_one)
+ apply (rule units_comm_group)
+ apply (unfold units_of_def, auto)
+done
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NewNumberTheory/ROOT.ML Fri Jun 19 18:33:10 2009 +0200
@@ -0,0 +1,1 @@
+use_thys ["Fib","Residues"];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NewNumberTheory/Residues.thy Fri Jun 19 18:33:10 2009 +0200
@@ -0,0 +1,474 @@
+(* Title: HOL/Library/Residues.thy
+ ID:
+ Author: Jeremy Avigad
+
+ An algebraic treatment of residue rings, and resulting proofs of
+ Euler's theorem and Wilson's theorem.
+*)
+
+header {* Residue rings *}
+
+theory Residues
+imports
+ UniqueFactorization
+ Binomial
+ MiscAlgebra
+begin
+
+
+(*
+
+ A locale for residue rings
+
+*)
+
+constdefs
+ residue_ring :: "int => int ring"
+ "residue_ring m == (|
+ carrier = {0..m - 1},
+ mult = (%x y. (x * y) mod m),
+ one = 1,
+ zero = 0,
+ add = (%x y. (x + y) mod m) |)"
+
+locale residues =
+ fixes m :: int and R (structure)
+ assumes m_gt_one: "m > 1"
+ defines "R == residue_ring m"
+
+context residues begin
+
+lemma abelian_group: "abelian_group R"
+ apply (insert m_gt_one)
+ apply (rule abelian_groupI)
+ apply (unfold R_def residue_ring_def)
+ apply (auto simp add: mod_pos_pos_trivial mod_add_right_eq [symmetric]
+ add_ac)
+ apply (case_tac "x = 0")
+ apply force
+ apply (subgoal_tac "(x + (m - x)) mod m = 0")
+ apply (erule bexI)
+ apply auto
+done
+
+lemma comm_monoid: "comm_monoid R"
+ apply (insert m_gt_one)
+ apply (unfold R_def residue_ring_def)
+ apply (rule comm_monoidI)
+ apply auto
+ apply (subgoal_tac "x * y mod m * z mod m = z * (x * y mod m) mod m")
+ apply (erule ssubst)
+ apply (subst zmod_zmult1_eq [symmetric])+
+ apply (simp_all only: mult_ac)
+done
+
+lemma cring: "cring R"
+ apply (rule cringI)
+ apply (rule abelian_group)
+ apply (rule comm_monoid)
+ apply (unfold R_def residue_ring_def, auto)
+ apply (subst mod_add_eq [symmetric])
+ apply (subst mult_commute)
+ apply (subst zmod_zmult1_eq [symmetric])
+ apply (simp add: ring_simps)
+done
+
+end
+
+sublocale residues < cring
+ by (rule cring)
+
+
+context residues begin
+
+(* 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)
+
+lemma res_add_eq: "x \<oplus> y = (x + y) mod m"
+ by (unfold R_def residue_ring_def, auto)
+
+lemma res_mult_eq: "x \<otimes> y = (x * y) mod m"
+ by (unfold R_def residue_ring_def, auto)
+
+lemma res_zero_eq: "\<zero> = 0"
+ by (unfold R_def residue_ring_def, auto)
+
+lemma res_one_eq: "\<one> = 1"
+ by (unfold R_def residue_ring_def units_of_def residue_ring_def, auto)
+
+lemma res_units_eq: "Units R = { x. 0 < x & x < m & coprime x m}"
+ apply (insert m_gt_one)
+ apply (unfold Units_def R_def residue_ring_def)
+ apply auto
+ apply (subgoal_tac "x ~= 0")
+ apply auto
+ apply (rule int_invertible_coprime)
+ apply (subgoal_tac "x ~= 0")
+ apply auto
+ apply (subst (asm) int_coprime_iff_invertible')
+ apply (rule m_gt_one)
+ apply (auto simp add: cong_int_def mult_commute)
+done
+
+lemma res_neg_eq: "\<ominus> x = (- x) mod m"
+ apply (insert m_gt_one)
+ apply (unfold R_def a_inv_def m_inv_def residue_ring_def)
+ apply auto
+ apply (rule the_equality)
+ apply auto
+ apply (subst mod_add_right_eq [symmetric])
+ apply auto
+ apply (subst mod_add_left_eq [symmetric])
+ apply auto
+ apply (subgoal_tac "y mod m = - x mod m")
+ apply simp
+ apply (subst zmod_eq_dvd_iff)
+ apply auto
+done
+
+lemma finite [iff]: "finite(carrier R)"
+ by (subst res_carrier_eq, auto)
+
+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
+ respects addition and multiplication on the integers. *)
+
+lemma mod_in_carrier [iff]: "a mod m : carrier R"
+ apply (unfold res_carrier_eq)
+ apply (insert m_gt_one, auto)
+done
+
+lemma add_cong: "(x mod m) \<oplus> (y mod m) = (x + y) mod m"
+ by (unfold R_def residue_ring_def, auto, arith)
+
+lemma mult_cong: "(x mod m) \<otimes> (y mod m) = (x * y) mod m"
+ apply (unfold R_def residue_ring_def, auto)
+ apply (subst zmod_zmult1_eq [symmetric])
+ apply (subst mult_commute)
+ apply (subst zmod_zmult1_eq [symmetric])
+ apply (subst mult_commute)
+ apply auto
+done
+
+lemma zero_cong: "\<zero> = 0"
+ apply (unfold R_def residue_ring_def, auto)
+done
+
+lemma one_cong: "\<one> = 1 mod m"
+ apply (insert m_gt_one)
+ apply (unfold R_def residue_ring_def, auto)
+done
+
+(* revise algebra library to use 1? *)
+lemma pow_cong: "(x mod m) (^) n = x^n mod m"
+ apply (insert m_gt_one)
+ apply (induct n)
+ apply (auto simp add: nat_pow_def one_cong One_nat_def)
+ apply (subst mult_commute)
+ apply (rule mult_cong)
+done
+
+lemma neg_cong: "\<ominus> (x mod m) = (- x) mod m"
+ apply (rule sym)
+ apply (rule sum_zero_eq_neg)
+ apply auto
+ apply (subst add_cong)
+ apply (subst zero_cong)
+ 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"
+ apply (induct set: finite)
+ apply (auto simp add: one_cong)
+ apply (subst finprod_insert)
+ apply (auto intro!: funcsetI 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"
+ apply (induct set: finite)
+ apply (auto simp add: zero_cong)
+ apply (subst finsum_insert)
+ apply (auto intro!: funcsetI add_cong)
+done
+
+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])
+ apply (subgoal_tac "a mod m ~= 0")
+ apply arith
+ apply auto
+ apply (subst (asm) int_gcd_commute)
+ apply (subst (asm) int_gcd_mult)
+ apply auto
+ apply (subst (asm) int_gcd_red)
+ apply (subst int_gcd_commute, assumption)
+done
+
+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
+ congruence. *)
+
+lemmas res_to_cong_simps = add_cong mult_cong pow_cong one_cong
+ prod_cong sum_cong neg_cong res_eq_to_cong
+
+(* Other useful facts about the residue ring *)
+
+lemma one_eq_neg_one: "\<one> = \<ominus> \<one> \<Longrightarrow> m = 2"
+ apply (simp add: res_one_eq res_neg_eq)
+ apply (insert m_gt_one)
+ apply (subgoal_tac "~(m > 2)")
+ apply arith
+ apply (rule notI)
+ apply (subgoal_tac "-1 mod m = m - 1")
+ apply force
+ apply (subst mod_add_self2 [symmetric])
+ apply (subst mod_pos_pos_trivial)
+ apply auto
+done
+
+end
+
+
+(* prime residues *)
+
+locale residues_prime =
+ fixes p :: int and R (structure)
+ assumes p_prime [intro]: "prime p"
+ defines "R == residue_ring p"
+
+sublocale residues_prime < residues p
+ apply (unfold R_def residues_def)
+ using p_prime apply auto
+done
+
+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 (rule classical)
+ apply (erule notE)
+ apply (subst int_gcd_commute)
+ apply (rule int_prime_imp_coprime)
+ apply (rule p_prime)
+ apply (rule notI)
+ apply (frule zdvd_imp_le)
+ apply auto
+done
+
+lemma res_prime_units_eq: "Units R = {1..p - 1}"
+ apply (subst res_units_eq)
+ apply auto
+ apply (subst int_gcd_commute)
+ apply (rule int_prime_imp_coprime)
+ apply (rule p_prime)
+ apply (rule zdvd_not_zless)
+ apply auto
+done
+
+end
+
+sublocale residues_prime < field
+ by (rule is_field)
+
+
+(*
+ Test cases: Euler's theorem and Wilson's theorem.
+*)
+
+
+subsection{* Euler's theorem *}
+
+(* the definition of the phi function *)
+
+constdefs
+ phi :: "int => nat"
+ "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
+ 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
+
+lemma (in residues) phi_eq: "phi m = card(Units R)"
+ by (simp add: phi_def res_units_eq)
+
+lemma (in residues) euler_theorem1:
+ assumes a: "gcd a m = 1"
+ shows "[a^phi m = 1] (mod m)"
+proof -
+ from a m_gt_one have [simp]: "a mod m : Units R"
+ 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>"
+ by (intro units_power_order_eq_one, auto)
+ finally show ?thesis
+ by (simp add: res_to_cong_simps)
+qed
+
+(* In fact, there is a two line proof!
+
+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
+ by (simp add: res_to_cong_simps)
+qed
+
+*)
+
+(* outside the locale, we can relax the restriction m > 1 *)
+
+lemma euler_theorem:
+ assumes "m >= 0" and "gcd a m = 1"
+ shows "[a^phi m = 1] (mod m)"
+proof (cases)
+ assume "m = 0 | m = 1"
+ thus ?thesis by auto
+next
+ assume "~(m = 0 | m = 1)"
+ with prems show ?thesis
+ by (intro residues.euler_theorem1, unfold residues_def, auto)
+qed
+
+lemma (in residues_prime) phi_prime: "phi p = (nat p - 1)"
+ apply (subst phi_eq)
+ apply (subst res_prime_units_eq)
+ apply auto
+done
+
+lemma phi_prime: "prime p \<Longrightarrow> phi p = (nat p - 1)"
+ apply (rule residues_prime.phi_prime)
+ apply (erule residues_prime.intro)
+done
+
+lemma fermat_theorem:
+ assumes "prime p" and "~ (p dvd a)"
+ shows "[a^(nat p - 1) = 1] (mod p)"
+proof -
+ from prems have "[a^phi p = 1] (mod p)"
+ apply (intro euler_theorem)
+ (* auto should get this next part. matching across
+ substitutions is needed. *)
+ apply (frule int_prime_gt_1, arith)
+ apply (subst int_gcd_commute, erule int_prime_imp_coprime, assumption)
+ done
+ also have "phi p = nat p - 1"
+ by (rule phi_prime, rule prems)
+ finally show ?thesis .
+qed
+
+
+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} = {}"
+ apply auto
+ apply (erule notE)
+ apply (erule inv_eq_imp_eq)
+ apply auto
+ apply (erule notE)
+ apply (erule inv_eq_imp_eq)
+ apply auto
+done
+
+lemma (in residues_prime) wilson_theorem1:
+ assumes a: "p > 2"
+ shows "[fact (p - 1) = - 1] (mod p)"
+proof -
+ let ?InversePairs = "{ {x, inv x} | x. x : Units R - {\<one>, \<ominus> \<one>}}"
+ have "Units R = {\<one>, \<ominus> \<one>} Un (Union ?InversePairs)"
+ by auto
+ hence "(\<Otimes>i: Units R. i) =
+ (\<Otimes>i: {\<one>, \<ominus> \<one>}. i) \<otimes> (\<Otimes>i: Union ?InversePairs. i)"
+ apply (elim ssubst) back back
+ apply (subst finprod_Un_disjoint)
+ apply (auto intro!: funcsetI)
+ apply (drule sym, subst (asm) inv_eq_one_eq)
+ apply auto
+ apply (drule sym, subst (asm) inv_eq_neg_one_eq)
+ apply auto
+ done
+ also have "(\<Otimes>i: {\<one>, \<ominus> \<one>}. i) = \<ominus> \<one>"
+ apply (subst finprod_insert)
+ apply auto
+ apply (frule one_eq_neg_one)
+ apply (insert a, force)
+ apply (auto intro!: funcsetI)
+ done
+ also have "(\<Otimes>i:(Union ?InversePairs). i) =
+ (\<Otimes> A: ?InversePairs. (\<Otimes> y:A. y))"
+ apply (subst finprod_Union_disjoint)
+ apply force
+ apply force
+ apply clarify
+ apply (rule inv_pair_lemma)
+ apply auto
+ done
+ also have "\<dots> = \<one>"
+ apply (rule finprod_one)
+ apply auto
+ apply (subst finprod_insert)
+ apply auto
+ apply (frule inv_eq_self)
+ apply (auto intro!: funcsetI)
+ done
+ finally have "(\<Otimes>i: Units R. i) = \<ominus> \<one>"
+ by simp
+ also have "(\<Otimes>i: Units R. i) = (\<Otimes>i: Units R. i mod p)"
+ apply (rule finprod_cong')
+ apply (auto intro!: funcsetI)
+ apply (subst (asm) res_prime_units_eq)
+ apply auto
+ done
+ also have "\<dots> = (PROD i: Units R. i) mod p"
+ apply (rule prod_cong)
+ apply auto
+ done
+ also have "\<dots> = fact (p - 1) mod p"
+ apply (subst int_fact_altdef)
+ apply (insert prems, force)
+ 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)
+qed
+
+lemma wilson_theorem: "prime (p::int) \<Longrightarrow> [fact (p - 1) = - 1] (mod p)"
+ apply (frule int_prime_gt_1)
+ apply (case_tac "p = 2")
+ apply (subst int_fact_altdef, simp)
+ apply (subst cong_int_def)
+ apply simp
+ apply (rule residues_prime.wilson_theorem1)
+ apply (rule residues_prime.intro)
+ apply auto
+done
+
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NewNumberTheory/UniqueFactorization.thy Fri Jun 19 18:33:10 2009 +0200
@@ -0,0 +1,967 @@
+(* Title: UniqueFactorization.thy
+ ID:
+ Author: Jeremy Avigad
+
+
+ Unique factorization for the natural numbers and the integers.
+
+ Note: there were previous Isabelle formalizations of unique
+ factorization due to Thomas Marthedal Rasmussen, and, building on
+ that, by Jeremy Avigad and David Gray.
+*)
+
+header {* UniqueFactorization *}
+
+theory UniqueFactorization
+imports Cong Multiset
+begin
+
+(* inherited from Multiset *)
+declare One_nat_def [simp del]
+
+(* As a simp or intro rule,
+
+ prime p \<Longrightarrow> p > 0
+
+ wreaks havoc here. When the premise includes ALL x :# M. prime x, it
+ leads to the backchaining
+
+ x > 0
+ prime x
+ x :# M which is, unfortunately,
+ count M x > 0
+*)
+
+
+(* useful facts *)
+
+lemma setsum_Un2: "finite (A Un B) \<Longrightarrow>
+ setsum f (A Un B) = setsum f (A - B) + setsum f (B - A) +
+ setsum f (A Int B)"
+ apply (subgoal_tac "A Un B = (A - B) Un (B - A) Un (A Int B)")
+ apply (erule ssubst)
+ apply (subst setsum_Un_disjoint)
+ apply auto
+ apply (subst setsum_Un_disjoint)
+ apply auto
+done
+
+lemma setprod_Un2: "finite (A Un B) \<Longrightarrow>
+ setprod f (A Un B) = setprod f (A - B) * setprod f (B - A) *
+ setprod f (A Int B)"
+ apply (subgoal_tac "A Un B = (A - B) Un (B - A) Un (A Int B)")
+ apply (erule ssubst)
+ apply (subst setprod_Un_disjoint)
+ apply auto
+ apply (subst setprod_Un_disjoint)
+ apply auto
+done
+
+(* Should this go in Multiset.thy? *)
+(* TN: No longer an intro-rule; needed only once and might get in the way *)
+lemma multiset_eqI: "[| !!x. count M x = count N x |] ==> M = N"
+ by (subst multiset_eq_conv_count_eq, blast)
+
+(* 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
+ semirings, using of_nat. Also, is it worth developing bounded quantifiers
+ "ALL i :# M. P i"?
+*)
+
+constdefs
+ msetprod :: "('a => ('b::{power,comm_monoid_mult})) => 'a multiset => 'b"
+ "msetprod f M == setprod (%x. (f x)^(count M x)) (set_of M)"
+
+syntax
+ "_msetprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"
+ ("(3PROD _:#_. _)" [0, 51, 10] 10)
+
+translations
+ "PROD i :# A. b" == "msetprod (%i. b) A"
+
+lemma msetprod_Un: "msetprod f (A+B) = msetprod f A * msetprod f B"
+ apply (simp add: msetprod_def power_add)
+ apply (subst setprod_Un2)
+ apply auto
+ apply (subgoal_tac
+ "(PROD x:set_of A - set_of B. f x ^ count A x * f x ^ count B x) =
+ (PROD x:set_of A - set_of B. f x ^ count A x)")
+ apply (erule ssubst)
+ apply (subgoal_tac
+ "(PROD x:set_of B - set_of A. f x ^ count A x * f x ^ count B x) =
+ (PROD x:set_of B - set_of A. f x ^ count B x)")
+ apply (erule ssubst)
+ apply (subgoal_tac "(PROD x:set_of A. f x ^ count A x) =
+ (PROD x:set_of A - set_of B. f x ^ count A x) *
+ (PROD x:set_of A Int set_of B. f x ^ count A x)")
+ apply (erule ssubst)
+ apply (subgoal_tac "(PROD x:set_of B. f x ^ count B x) =
+ (PROD x:set_of B - set_of A. f x ^ count B x) *
+ (PROD x:set_of A Int set_of B. f x ^ count B x)")
+ apply (erule ssubst)
+ apply (subst setprod_timesf)
+ apply (force simp add: mult_ac)
+ apply (subst setprod_Un_disjoint [symmetric])
+ apply (auto intro: setprod_cong)
+ apply (subst setprod_Un_disjoint [symmetric])
+ apply (auto intro: setprod_cong)
+done
+
+
+subsection {* unique factorization: multiset version *}
+
+lemma multiset_prime_factorization_exists [rule_format]: "n > 0 -->
+ (EX M. (ALL (p::nat) : set_of M. prime p) & n = (PROD i :# M. i))"
+proof (rule nat_less_induct, clarify)
+ fix n :: nat
+ assume ih: "ALL m < n. 0 < m --> (EX M. (ALL p : set_of M. prime p) & m =
+ (PROD i :# M. i))"
+ assume "(n::nat) > 0"
+ then have "n = 1 | (n > 1 & prime n) | (n > 1 & ~ prime n)"
+ by arith
+ moreover
+ {
+ assume "n = 1"
+ then have "(ALL p : set_of {#}. prime p) & n = (PROD i :# {#}. i)"
+ by (auto simp add: msetprod_def)
+ }
+ 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
+ {
+ assume "n > 1" and "~ prime n"
+ from prems nat_not_prime_eq_prod
+ obtain m k where "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)"
+ by (auto simp add: prems msetprod_Un set_of_union)
+ then have "EX M. (ALL p : set_of M. prime p) & n = (PROD i :# M. i)"..
+ }
+ ultimately show "EX M. (ALL p : set_of M. prime p) & n = (PROD i::nat:#M. i)"
+ by blast
+qed
+
+lemma multiset_prime_factorization_unique_aux:
+ fixes a :: nat
+ assumes "(ALL p : set_of M. prime p)" and
+ "(ALL p : set_of N. prime p)" and
+ "(PROD i :# M. i) dvd (PROD i:# N. i)"
+ shows
+ "count M a <= count N a"
+proof cases
+ assume "a : set_of M"
+ with prems have a: "prime a"
+ by auto
+ with prems have "a ^ count M a dvd (PROD i :# M. i)"
+ by (auto intro: dvd_setprod simp add: msetprod_def)
+ also have "... dvd (PROD i :# N. i)"
+ by (rule prems)
+ 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
+ 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))"
+ apply (subst nat_gcd_commute)
+ apply (rule nat_setprod_coprime)
+ apply (rule nat_primes_imp_powers_coprime)
+ apply (insert prems, auto)
+ done
+ ultimately have "a ^ count M a dvd a^(count N a)"
+ by (elim nat_coprime_dvd_mult)
+ with a show ?thesis
+ by (intro power_dvd_imp_le, auto)
+next
+ assume "a ~: set_of M"
+ thus ?thesis by auto
+qed
+
+lemma multiset_prime_factorization_unique:
+ assumes "(ALL (p::nat) : set_of M. prime p)" and
+ "(ALL p : set_of N. prime p)" and
+ "(PROD i :# M. i) = (PROD i:# N. i)"
+ shows
+ "M = N"
+proof -
+ {
+ fix a
+ from prems have "count M a <= count N a"
+ by (intro multiset_prime_factorization_unique_aux, auto)
+ moreover from prems have "count N a <= count M a"
+ by (intro multiset_prime_factorization_unique_aux, auto)
+ ultimately have "count M a = count N a"
+ by auto
+ }
+ thus ?thesis by (simp add:multiset_eq_conv_count_eq)
+qed
+
+constdefs
+ multiset_prime_factorization :: "nat => nat multiset"
+ "multiset_prime_factorization n ==
+ if n > 0 then (THE M. ((ALL p : set_of M. prime p) &
+ n = (PROD i :# M. i)))
+ else {#}"
+
+lemma multiset_prime_factorization: "n > 0 ==>
+ (ALL p : set_of (multiset_prime_factorization n). prime p) &
+ n = (PROD i :# (multiset_prime_factorization n). i)"
+ apply (unfold multiset_prime_factorization_def)
+ apply clarsimp
+ apply (frule multiset_prime_factorization_exists)
+ apply clarify
+ apply (rule theI)
+ apply (insert multiset_prime_factorization_unique, blast)+
+done
+
+
+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"
+
+(* 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
+ prime_factors_nat :: "nat \<Rightarrow> nat set"
+where
+ "prime_factors_nat n = set_of (multiset_prime_factorization n)"
+
+instance proof qed
+
+end
+
+(* definitions for the integers *)
+
+instantiation int :: unique_factorization
+
+begin
+
+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))"
+
+instance proof qed
+
+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_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"
+ by (auto simp add: multiplicity_int_def)
+
+declare TransferMorphism_nat_int[transfer add return:
+ transfer_nat_int_prime_factors transfer_nat_int_prime_factors_closure
+ transfer_nat_int_multiplicity]
+
+
+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>
+ nat_set (prime_factors n)"
+ by (simp only: transfer_nat_int_prime_factors_closure is_nat_def)
+
+lemma transfer_int_nat_multiplicity:
+ "multiplicity (int p) (int n) = multiplicity p n"
+ by (auto simp add: multiplicity_int_def)
+
+declare TransferMorphism_int_nat[transfer add return:
+ transfer_int_nat_prime_factors transfer_int_nat_prime_factors_closure
+ transfer_int_nat_multiplicity]
+
+
+subsection {* Properties of prime factors and multiplicity for nats and ints *}
+
+lemma int_prime_factors_ge_0 [elim]: "p : prime_factors (n::int) \<Longrightarrow> p >= 0"
+ by (unfold prime_factors_int_def, auto)
+
+lemma nat_prime_factors_prime [intro]: "p : prime_factors (n::nat) \<Longrightarrow> prime p"
+ apply (case_tac "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
+
+lemma int_prime_factors_prime [intro]:
+ assumes "n >= 0" and "p : prime_factors (n::int)"
+ shows "prime p"
+
+ apply (rule nat_prime_factors_prime [transferred, of n p])
+ using prems apply auto
+done
+
+lemma nat_prime_factors_gt_0 [elim]: "p : prime_factors x \<Longrightarrow> p > (0::nat)"
+ by (frule nat_prime_factors_prime, auto)
+
+lemma int_prime_factors_gt_0 [elim]: "x >= 0 \<Longrightarrow> p : prime_factors x \<Longrightarrow>
+ p > (0::int)"
+ by (frule (1) int_prime_factors_prime, auto)
+
+lemma nat_prime_factors_finite [iff]: "finite (prime_factors (n::nat))"
+ by (unfold prime_factors_nat_def, auto)
+
+lemma int_prime_factors_finite [iff]: "finite (prime_factors (n::int))"
+ by (unfold prime_factors_int_def, auto)
+
+lemma nat_prime_factors_altdef: "prime_factors (n::nat) =
+ {p. multiplicity p n > 0}"
+ by (force simp add: prime_factors_nat_def multiplicity_nat_def)
+
+lemma int_prime_factors_altdef: "prime_factors (n::int) =
+ {p. p >= 0 & multiplicity p n > 0}"
+ apply (unfold prime_factors_int_def multiplicity_int_def)
+ apply (subst nat_prime_factors_altdef)
+ apply (auto simp add: image_def)
+done
+
+lemma nat_prime_factorization: "(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)
+
+thm nat_prime_factorization [transferred]
+
+lemma int_prime_factorization:
+ assumes "(n::int) > 0"
+ shows "n = (PROD p : prime_factors n. p^(multiplicity p n))"
+
+ apply (rule nat_prime_factorization [transferred, of n])
+ using prems apply auto
+done
+
+lemma nat_neq_zero_eq_gt_zero: "((x::nat) ~= 0) = (x > 0)"
+ by auto
+
+lemma nat_prime_factorization_unique:
+ "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 (unfold prime_factors_nat_def multiplicity_nat_def)
+ apply (simp add: set_of_def count_def Abs_multiset_inverse multiset_def)
+ apply (unfold multiset_prime_factorization_def)
+ apply (subgoal_tac "n > 0")
+ prefer 2
+ apply force
+ apply (subst if_P, assumption)
+ apply (rule the1_equality)
+ apply (rule ex_ex1I)
+ apply (rule multiset_prime_factorization_exists, assumption)
+ apply (rule multiset_prime_factorization_unique)
+ apply force
+ apply force
+ apply force
+ unfolding set_of_def count_def msetprod_def
+ apply (subgoal_tac "f : multiset")
+ apply (auto simp only: Abs_multiset_inverse)
+ unfolding multiset_def apply force
+done
+
+lemma nat_prime_factors_characterization: "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 nat_prime_factorization_unique [THEN conjunct1, symmetric],
+ assumption+)
+
+lemma nat_prime_factors_characterization':
+ "finite {p. 0 < f (p::nat)} \<Longrightarrow>
+ (ALL p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow>
+ prime_factors (PROD p | 0 < f p . p ^ f p) = {p. 0 < f p}"
+ apply (rule nat_prime_factors_characterization)
+ apply auto
+done
+
+(* A minor glitch:*)
+
+thm nat_prime_factors_characterization'
+ [where f = "%x. f (int (x::nat))",
+ transferred direction: nat "op <= (0::int)", rule_format]
+
+(*
+ Transfer isn't smart enough to know that the "0 < f p" should
+ remain a comparison between nats. But the transfer still works.
+*)
+
+lemma int_primes_characterization' [rule_format]:
+ "finite {p. p >= 0 & 0 < f (p::int)} \<Longrightarrow>
+ (ALL p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow>
+ prime_factors (PROD p | p >=0 & 0 < f p . p ^ f p) =
+ {p. p >= 0 & 0 < f p}"
+
+ apply (insert nat_prime_factors_characterization'
+ [where f = "%x. f (int (x::nat))",
+ transferred direction: nat "op <= (0::int)"])
+ apply auto
+done
+
+lemma int_prime_factors_characterization: "S = {p. 0 < f (p::int)} \<Longrightarrow>
+ finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
+ prime_factors n = S"
+ apply simp
+ apply (subgoal_tac "{p. 0 < f p} = {p. 0 <= p & 0 < f p}")
+ apply (simp only:)
+ apply (subst int_primes_characterization')
+ apply auto
+ apply (auto simp add: int_prime_ge_0)
+done
+
+lemma nat_multiplicity_characterization: "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 nat_prime_factorization_unique [THEN conjunct2, rule_format,
+ symmetric], auto)
+
+lemma nat_multiplicity_characterization': "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 (rule nat_multiplicity_characterization)
+ apply auto
+done
+
+lemma int_multiplicity_characterization' [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 nat_multiplicity_characterization'
+ [where f = "%x. f (int (x::nat))",
+ transferred direction: nat "op <= (0::int)", rule_format])
+ apply auto
+done
+
+lemma int_multiplicity_characterization: "S = {p. 0 < f (p::int)} \<Longrightarrow>
+ finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
+ p >= 0 \<Longrightarrow> multiplicity p n = f p"
+ apply simp
+ apply (subgoal_tac "{p. 0 < f p} = {p. 0 <= p & 0 < f p}")
+ apply (simp only:)
+ apply (subst int_multiplicity_characterization')
+ apply auto
+ apply (auto simp add: int_prime_ge_0)
+done
+
+lemma nat_multiplicity_zero [simp]: "multiplicity (p::nat) 0 = 0"
+ by (simp add: multiplicity_nat_def multiset_prime_factorization_def)
+
+lemma int_multiplicity_zero [simp]: "multiplicity (p::int) 0 = 0"
+ by (simp add: multiplicity_int_def)
+
+lemma nat_multiplicity_one [simp]: "multiplicity p (1::nat) = 0"
+ by (subst nat_multiplicity_characterization [where f = "%x. 0"], auto)
+
+lemma int_multiplicity_one [simp]: "multiplicity p (1::int) = 0"
+ by (simp add: multiplicity_int_def)
+
+lemma nat_multiplicity_prime [simp]: "prime (p::nat) \<Longrightarrow> multiplicity p p = 1"
+ apply (subst nat_multiplicity_characterization
+ [where f = "(%q. if q = p then 1 else 0)"])
+ apply auto
+ apply (case_tac "x = p")
+ apply auto
+done
+
+lemma int_multiplicity_prime [simp]: "prime (p::int) \<Longrightarrow> multiplicity p p = 1"
+ unfolding prime_int_def multiplicity_int_def by auto
+
+lemma nat_multiplicity_prime_power [simp]: "prime (p::nat) \<Longrightarrow>
+ multiplicity p (p^n) = n"
+ apply (case_tac "n = 0")
+ apply auto
+ apply (subst nat_multiplicity_characterization
+ [where f = "(%q. if q = p then n else 0)"])
+ apply auto
+ apply (case_tac "x = p")
+ apply auto
+done
+
+lemma int_multiplicity_prime_power [simp]: "prime (p::int) \<Longrightarrow>
+ multiplicity p (p^n) = n"
+ apply (frule int_prime_ge_0)
+ apply (auto simp add: prime_int_def multiplicity_int_def nat_power_eq)
+done
+
+lemma nat_multiplicity_nonprime [simp]: "~ prime (p::nat) \<Longrightarrow>
+ multiplicity p n = 0"
+ apply (case_tac "n = 0")
+ apply auto
+ apply (frule multiset_prime_factorization)
+ apply (auto simp add: set_of_def multiplicity_nat_def)
+done
+
+lemma int_multiplicity_nonprime [simp]: "~ prime (p::int) \<Longrightarrow> multiplicity p n = 0"
+ by (unfold multiplicity_int_def prime_int_def, auto)
+
+lemma nat_multiplicity_not_factor [simp]:
+ "p ~: prime_factors (n::nat) \<Longrightarrow> multiplicity p n = 0"
+ by (subst (asm) nat_prime_factors_altdef, auto)
+
+lemma int_multiplicity_not_factor [simp]:
+ "p >= 0 \<Longrightarrow> p ~: prime_factors (n::int) \<Longrightarrow> multiplicity p n = 0"
+ by (subst (asm) int_prime_factors_altdef, auto)
+
+lemma nat_multiplicity_product_aux: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow>
+ (prime_factors k) Un (prime_factors l) = prime_factors (k * l) &
+ (ALL p. multiplicity p k + multiplicity p l = multiplicity p (k * l))"
+ apply (rule nat_prime_factorization_unique)
+ apply (simp only: nat_prime_factors_altdef)
+ apply auto
+ apply (subst power_add)
+ apply (subst setprod_timesf)
+ apply (rule arg_cong2)back back
+ apply (subgoal_tac "prime_factors k Un prime_factors l = prime_factors k Un
+ (prime_factors l - prime_factors k)")
+ apply (erule ssubst)
+ apply (subst setprod_Un_disjoint)
+ apply auto
+ apply (subgoal_tac "(\<Prod>p\<in>prime_factors l - prime_factors k. p ^ multiplicity p k) =
+ (\<Prod>p\<in>prime_factors l - prime_factors k. 1)")
+ apply (erule ssubst)
+ apply (simp add: setprod_1)
+ apply (erule nat_prime_factorization)
+ apply (rule setprod_cong, auto)
+ apply (subgoal_tac "prime_factors k Un prime_factors l = prime_factors l Un
+ (prime_factors k - prime_factors l)")
+ apply (erule ssubst)
+ apply (subst setprod_Un_disjoint)
+ apply auto
+ apply (subgoal_tac "(\<Prod>p\<in>prime_factors k - prime_factors l. p ^ multiplicity p l) =
+ (\<Prod>p\<in>prime_factors k - prime_factors l. 1)")
+ apply (erule ssubst)
+ apply (simp add: setprod_1)
+ apply (erule nat_prime_factorization)
+ apply (rule setprod_cong, auto)
+done
+
+(* transfer doesn't have the same problem here with the right
+ choice of rules. *)
+
+lemma int_multiplicity_product_aux:
+ assumes "(k::int) > 0" and "l > 0"
+ shows
+ "(prime_factors k) Un (prime_factors l) = prime_factors (k * l) &
+ (ALL p >= 0. multiplicity p k + multiplicity p l = multiplicity p (k * l))"
+
+ apply (rule nat_multiplicity_product_aux [transferred, of l k])
+ using prems apply auto
+done
+
+lemma nat_prime_factors_product: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> prime_factors (k * l) =
+ prime_factors k Un prime_factors l"
+ by (rule nat_multiplicity_product_aux [THEN conjunct1, symmetric])
+
+lemma int_prime_factors_product: "(k::int) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> prime_factors (k * l) =
+ prime_factors k Un prime_factors l"
+ by (rule int_multiplicity_product_aux [THEN conjunct1, symmetric])
+
+lemma nat_multiplicity_product: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> multiplicity p (k * l) =
+ multiplicity p k + multiplicity p l"
+ by (rule nat_multiplicity_product_aux [THEN conjunct2, rule_format,
+ symmetric])
+
+lemma int_multiplicity_product: "(k::int) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> p >= 0 \<Longrightarrow>
+ multiplicity p (k * l) = multiplicity p k + multiplicity p l"
+ by (rule int_multiplicity_product_aux [THEN conjunct2, rule_format,
+ symmetric])
+
+lemma nat_multiplicity_setprod: "finite S \<Longrightarrow> (ALL x : S. f x > 0) \<Longrightarrow>
+ multiplicity (p::nat) (PROD x : S. f x) =
+ (SUM x : S. multiplicity p (f x))"
+ apply (induct set: finite)
+ apply auto
+ apply (subst nat_multiplicity_product)
+ apply auto
+done
+
+(* Transfer is delicate here for two reasons: first, because there is
+ an implicit quantifier over functions (f), and, second, because the
+ product over the multiplicity should not be translated to an integer
+ product.
+
+ The way to handle the first is to use quantifier rules for functions.
+ The way to handle the second is to turn off the offending rule.
+*)
+
+lemma transfer_nat_int_sum_prod_closure3:
+ "(SUM x : A. int (f x)) >= 0"
+ "(PROD x : A. int (f x)) >= 0"
+ apply (rule setsum_nonneg, auto)
+ apply (rule setprod_nonneg, auto)
+done
+
+declare TransferMorphism_nat_int[transfer
+ add return: transfer_nat_int_sum_prod_closure3
+ del: transfer_nat_int_sum_prod2 (1)]
+
+lemma int_multiplicity_setprod: "p >= 0 \<Longrightarrow> finite S \<Longrightarrow>
+ (ALL x : S. f x > 0) \<Longrightarrow>
+ multiplicity (p::int) (PROD x : S. f x) =
+ (SUM x : S. multiplicity p (f x))"
+
+ apply (frule nat_multiplicity_setprod
+ [where f = "%x. nat(int(nat(f x)))",
+ transferred direction: nat "op <= (0::int)"])
+ apply auto
+ apply (subst (asm) setprod_cong)
+ apply (rule refl)
+ apply (rule if_P)
+ apply auto
+ apply (rule setsum_cong)
+ apply auto
+done
+
+declare TransferMorphism_nat_int[transfer
+ add return: transfer_nat_int_sum_prod2 (1)]
+
+lemma nat_multiplicity_prod_prime_powers:
+ "finite S \<Longrightarrow> (ALL p : S. prime (p::nat)) \<Longrightarrow>
+ multiplicity p (PROD p : S. p ^ f p) = (if p : S then f p else 0)"
+ apply (subgoal_tac "(PROD p : S. p ^ f p) =
+ (PROD p : S. p ^ (%x. if x : S then f x else 0) p)")
+ apply (erule ssubst)
+ apply (subst nat_multiplicity_characterization)
+ prefer 5 apply (rule refl)
+ apply (rule refl)
+ apply auto
+ apply (subst setprod_mono_one_right)
+ apply assumption
+ prefer 3
+ apply (rule setprod_cong)
+ apply (rule refl)
+ apply auto
+done
+
+(* Here the issue with transfer is the implicit quantifier over S *)
+
+lemma int_multiplicity_prod_prime_powers:
+ "(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 nat_multiplicity_prod_prime_powers [where f = "%x. f(int x)"
+ and S = "nat ` S", transferred])
+ apply auto
+ apply (subst prime_int_def [symmetric])
+ apply auto
+ apply (subgoal_tac "xb >= 0")
+ apply force
+ apply (rule int_prime_ge_0)
+ apply force
+ apply (subst transfer_nat_int_set_return_embed)
+ apply (unfold nat_set_def, auto)
+done
+
+lemma nat_multiplicity_distinct_prime_power: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow>
+ p ~= q \<Longrightarrow> multiplicity p (q^n) = 0"
+ apply (subgoal_tac "q^n = setprod (%x. x^n) {q}")
+ apply (erule ssubst)
+ apply (subst nat_multiplicity_prod_prime_powers)
+ apply auto
+done
+
+lemma int_multiplicity_distinct_prime_power: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow>
+ p ~= q \<Longrightarrow> multiplicity p (q^n) = 0"
+ apply (frule int_prime_ge_0 [of q])
+ apply (frule nat_multiplicity_distinct_prime_power [transferred leaving: n])
+ prefer 4
+ apply assumption
+ apply auto
+done
+
+lemma nat_dvd_multiplicity:
+ "(0::nat) < y \<Longrightarrow> x dvd y \<Longrightarrow> multiplicity p x <= multiplicity p y"
+ apply (case_tac "x = 0")
+ apply (auto simp add: dvd_def nat_multiplicity_product)
+done
+
+lemma int_dvd_multiplicity:
+ "(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 (auto simp add: dvd_def)
+ apply (subgoal_tac "0 < k")
+ apply (auto simp add: int_multiplicity_product)
+ apply (erule zero_less_mult_pos)
+ apply arith
+done
+
+lemma nat_dvd_prime_factors [intro]:
+ "0 < (y::nat) \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x <= prime_factors y"
+ apply (simp only: nat_prime_factors_altdef)
+ apply auto
+ apply (frule nat_dvd_multiplicity)
+ apply auto
+(* It is a shame that auto and arith don't get this. *)
+ apply (erule order_less_le_trans)back
+ apply assumption
+done
+
+lemma int_dvd_prime_factors [intro]:
+ "0 < (y::int) \<Longrightarrow> 0 <= x \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x <= prime_factors y"
+ apply (auto simp add: int_prime_factors_altdef)
+ apply (erule order_less_le_trans)
+ apply (rule int_dvd_multiplicity)
+ apply auto
+done
+
+lemma nat_multiplicity_dvd: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow>
+ ALL p. multiplicity p x <= multiplicity p y \<Longrightarrow>
+ x dvd y"
+ apply (subst nat_prime_factorization [of x], assumption)
+ apply (subst nat_prime_factorization [of y], assumption)
+ apply (rule setprod_dvd_setprod_subset2)
+ apply force
+ apply (subst nat_prime_factors_altdef)+
+ apply auto
+(* Again, a shame that auto and arith don't get this. *)
+ apply (drule_tac x = xa in spec, auto)
+ apply (rule le_imp_power_dvd)
+ apply blast
+done
+
+lemma int_multiplicity_dvd: "0 < (x::int) \<Longrightarrow> 0 < y \<Longrightarrow>
+ ALL p >= 0. multiplicity p x <= multiplicity p y \<Longrightarrow>
+ x dvd y"
+ apply (subst int_prime_factorization [of x], assumption)
+ apply (subst int_prime_factorization [of y], assumption)
+ apply (rule setprod_dvd_setprod_subset2)
+ apply force
+ apply (subst int_prime_factors_altdef)+
+ apply auto
+ apply (rule dvd_power_le)
+ apply auto
+ apply (drule_tac x = xa in spec)
+ apply (erule impE)
+ apply auto
+done
+
+lemma nat_multiplicity_dvd': "(0::nat) < x \<Longrightarrow>
+ \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
+ apply (cases "y = 0")
+ apply auto
+ apply (rule nat_multiplicity_dvd, auto)
+ apply (case_tac "prime p")
+ apply auto
+done
+
+lemma int_multiplicity_dvd': "(0::int) < x \<Longrightarrow> 0 <= y \<Longrightarrow>
+ \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
+ apply (cases "y = 0")
+ apply auto
+ apply (rule int_multiplicity_dvd, auto)
+ apply (case_tac "prime p")
+ apply auto
+done
+
+lemma nat_dvd_multiplicity_eq: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow>
+ (x dvd y) = (ALL p. multiplicity p x <= multiplicity p y)"
+ by (auto intro: nat_dvd_multiplicity nat_multiplicity_dvd)
+
+lemma int_dvd_multiplicity_eq: "0 < (x::int) \<Longrightarrow> 0 < y \<Longrightarrow>
+ (x dvd y) = (ALL p >= 0. multiplicity p x <= multiplicity p y)"
+ by (auto intro: int_dvd_multiplicity int_multiplicity_dvd)
+
+lemma nat_prime_factors_altdef2: "(n::nat) > 0 \<Longrightarrow>
+ (p : prime_factors n) = (prime p & p dvd n)"
+ apply (case_tac "prime p")
+ apply auto
+ apply (subst nat_prime_factorization [where n = n], assumption)
+ apply (rule dvd_trans)
+ apply (rule dvd_power [where x = p and n = "multiplicity p n"])
+ apply (subst (asm) nat_prime_factors_altdef, force)
+ apply (rule dvd_setprod)
+ apply auto
+ apply (subst nat_prime_factors_altdef)
+ apply (subst (asm) nat_dvd_multiplicity_eq)
+ apply auto
+ apply (drule spec [where x = p])
+ apply auto
+done
+
+lemma int_prime_factors_altdef2:
+ assumes "(n::int) > 0"
+ shows "(p : prime_factors n) = (prime p & p dvd n)"
+
+ apply (case_tac "p >= 0")
+ apply (rule nat_prime_factors_altdef2 [transferred])
+ using prems apply auto
+ apply (auto simp add: int_prime_ge_0 int_prime_factors_ge_0)
+done
+
+lemma nat_multiplicity_eq:
+ fixes x and y::nat
+ 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_anti_sym)
+ apply (auto intro: nat_multiplicity_dvd')
+done
+
+lemma int_multiplicity_eq:
+ 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_anti_sym [transferred])
+ apply (auto intro: int_multiplicity_dvd')
+done
+
+
+subsection {* An application *}
+
+lemma nat_gcd_eq:
+ assumes pos [arith]: "x > 0" "y > 0"
+ shows "gcd (x::nat) y =
+ (PROD p: prime_factors x Un prime_factors y.
+ p ^ (min (multiplicity p x) (multiplicity p y)))"
+proof -
+ def z == "(PROD p: prime_factors (x::nat) Un prime_factors y.
+ p ^ (min (multiplicity p x) (multiplicity p y)))"
+ have [arith]: "z > 0"
+ unfolding z_def by (rule setprod_pos_nat, auto)
+ have aux: "!!p. prime p \<Longrightarrow> multiplicity p z =
+ min (multiplicity p x) (multiplicity p y)"
+ unfolding z_def
+ apply (subst nat_multiplicity_prod_prime_powers)
+ apply (auto simp add: nat_multiplicity_not_factor)
+ done
+ have "z dvd x"
+ by (intro nat_multiplicity_dvd', auto simp add: aux)
+ moreover have "z dvd y"
+ by (intro nat_multiplicity_dvd', auto simp add: aux)
+ moreover have "ALL w. w dvd x & w dvd y \<longrightarrow> w dvd z"
+ apply auto
+ apply (case_tac "w = 0", auto)
+ apply (erule nat_multiplicity_dvd')
+ apply (auto intro: nat_dvd_multiplicity simp add: aux)
+ done
+ ultimately have "z = gcd x y"
+ by (subst nat_gcd_unique [symmetric], blast)
+ thus ?thesis
+ unfolding z_def by auto
+qed
+
+lemma nat_lcm_eq:
+ assumes pos [arith]: "x > 0" "y > 0"
+ shows "lcm (x::nat) y =
+ (PROD p: prime_factors x Un prime_factors y.
+ p ^ (max (multiplicity p x) (multiplicity p y)))"
+proof -
+ def z == "(PROD p: prime_factors (x::nat) Un prime_factors y.
+ p ^ (max (multiplicity p x) (multiplicity p y)))"
+ have [arith]: "z > 0"
+ unfolding z_def by (rule setprod_pos_nat, auto)
+ have aux: "!!p. prime p \<Longrightarrow> multiplicity p z =
+ max (multiplicity p x) (multiplicity p y)"
+ unfolding z_def
+ apply (subst nat_multiplicity_prod_prime_powers)
+ apply (auto simp add: nat_multiplicity_not_factor)
+ done
+ have "x dvd z"
+ by (intro nat_multiplicity_dvd', auto simp add: aux)
+ moreover have "y dvd z"
+ by (intro nat_multiplicity_dvd', auto simp add: aux)
+ moreover have "ALL w. x dvd w & y dvd w \<longrightarrow> z dvd w"
+ apply auto
+ apply (case_tac "w = 0", auto)
+ apply (rule nat_multiplicity_dvd')
+ apply (auto intro: nat_dvd_multiplicity simp add: aux)
+ done
+ ultimately have "z = lcm x y"
+ by (subst nat_lcm_unique [symmetric], blast)
+ thus ?thesis
+ unfolding z_def by auto
+qed
+
+lemma nat_multiplicity_gcd:
+ assumes [arith]: "x > 0" "y > 0"
+ shows "multiplicity (p::nat) (gcd x y) =
+ min (multiplicity p x) (multiplicity p y)"
+
+ apply (subst nat_gcd_eq)
+ apply auto
+ apply (subst nat_multiplicity_prod_prime_powers)
+ apply auto
+done
+
+lemma nat_multiplicity_lcm:
+ assumes [arith]: "x > 0" "y > 0"
+ shows "multiplicity (p::nat) (lcm x y) =
+ max (multiplicity p x) (multiplicity p y)"
+
+ apply (subst nat_lcm_eq)
+ apply auto
+ apply (subst nat_multiplicity_prod_prime_powers)
+ apply auto
+done
+
+lemma nat_gcd_lcm_distrib: "gcd (x::nat) (lcm y z) = lcm (gcd x y) (gcd x z)"
+ apply (case_tac "x = 0 | y = 0 | z = 0")
+ apply auto
+ apply (rule nat_multiplicity_eq)
+ apply (auto simp add: nat_multiplicity_gcd nat_multiplicity_lcm
+ nat_lcm_pos)
+done
+
+lemma int_gcd_lcm_distrib: "gcd (x::int) (lcm y z) = lcm (gcd x y) (gcd x z)"
+ apply (subst (1 2 3) int_gcd_abs)
+ apply (subst int_lcm_abs)
+ apply (subst (2) abs_of_nonneg)
+ apply force
+ apply (rule nat_gcd_lcm_distrib [transferred])
+ apply auto
+done
+
+end