moved theories Parity, GCD, Binomial to Library;
authorwenzelm
Wed Nov 08 23:11:13 2006 +0100 (2006-11-08)
changeset 2125647195501ecf7
parent 21255 617fdb08abe9
child 21257 b7f090c5057d
moved theories Parity, GCD, Binomial to Library;
NEWS
src/HOL/Algebra/Exponent.thy
src/HOL/Algebra/ROOT.ML
src/HOL/Binomial.thy
src/HOL/Complex/ROOT.ML
src/HOL/GCD.thy
src/HOL/Hyperreal/HyperPow.thy
src/HOL/Import/HOL/ROOT.ML
src/HOL/Integ/Parity.thy
src/HOL/IsaMakefile
src/HOL/Library/Binomial.thy
src/HOL/Library/Commutative_Ring.thy
src/HOL/Library/GCD.thy
src/HOL/Library/Infinite_Set.thy
src/HOL/Library/Library.thy
src/HOL/Library/Parity.thy
src/HOL/Library/Primes.thy
src/HOL/PreList.thy
src/HOL/Real/Float.thy
src/HOL/ex/NatSum.thy
src/HOL/ex/ROOT.ML
src/HOL/ex/Reflected_Presburger.thy
     1.1 --- a/NEWS	Wed Nov 08 22:24:54 2006 +0100
     1.2 +++ b/NEWS	Wed Nov 08 23:11:13 2006 +0100
     1.3 @@ -615,9 +615,9 @@
     1.4  * inductive and datatype: provide projections of mutual rules, bundled
     1.5  as foo_bar.inducts;
     1.6  
     1.7 -* Library: theory Infinite_Set has been moved to the library.
     1.8 -
     1.9 -* Library: theory Accessible_Part has been move to main HOL.
    1.10 +* Library: moved theories Parity, GCD, Binomial, Infinite_Set to Library.
    1.11 +
    1.12 +* Library: moved theory Accessible_Part to main HOL.
    1.13  
    1.14  * Library: added theory Coinductive_List of potentially infinite lists
    1.15  as greatest fixed-point.
     2.1 --- a/src/HOL/Algebra/Exponent.thy	Wed Nov 08 22:24:54 2006 +0100
     2.2 +++ b/src/HOL/Algebra/Exponent.thy	Wed Nov 08 23:11:13 2006 +0100
     2.3 @@ -5,7 +5,7 @@
     2.4      exponent p s   yields the greatest power of p that divides s.
     2.5  *)
     2.6  
     2.7 -theory Exponent imports Main Primes begin
     2.8 +theory Exponent imports Main Primes Binomial begin
     2.9  
    2.10  
    2.11  section {*The Combinatorial Argument Underlying the First Sylow Theorem*}
     3.1 --- a/src/HOL/Algebra/ROOT.ML	Wed Nov 08 22:24:54 2006 +0100
     3.2 +++ b/src/HOL/Algebra/ROOT.ML	Wed Nov 08 23:11:13 2006 +0100
     3.3 @@ -10,6 +10,8 @@
     3.4  
     3.5  no_document use_thy "FuncSet";
     3.6  no_document use_thy "Primes";
     3.7 +no_document use_thy "Binomial";
     3.8 +
     3.9  
    3.10  (* Groups *)
    3.11  
     4.1 --- a/src/HOL/Binomial.thy	Wed Nov 08 22:24:54 2006 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,189 +0,0 @@
     4.4 -(*  Title:      HOL/Binomial.thy
     4.5 -    ID:         $Id$
     4.6 -    Author:     Lawrence C Paulson
     4.7 -    Copyright   1997  University of Cambridge
     4.8 -*)
     4.9 -
    4.10 -header{*Binomial Coefficients*}
    4.11 -
    4.12 -theory Binomial
    4.13 -imports GCD
    4.14 -begin
    4.15 -
    4.16 -text{*This development is based on the work of Andy Gordon and
    4.17 -Florian Kammueller*}
    4.18 -
    4.19 -consts
    4.20 -  binomial :: "nat \<Rightarrow> nat \<Rightarrow> nat"      (infixl "choose" 65)
    4.21 -
    4.22 -primrec
    4.23 -  binomial_0:   "(0     choose k) = (if k = 0 then 1 else 0)"
    4.24 -
    4.25 -  binomial_Suc: "(Suc n choose k) =
    4.26 -                 (if k = 0 then 1 else (n choose (k - 1)) + (n choose k))"
    4.27 -
    4.28 -lemma binomial_n_0 [simp]: "(n choose 0) = 1"
    4.29 -by (cases n) simp_all
    4.30 -
    4.31 -lemma binomial_0_Suc [simp]: "(0 choose Suc k) = 0"
    4.32 -by simp
    4.33 -
    4.34 -lemma binomial_Suc_Suc [simp]:
    4.35 -     "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)"
    4.36 -by simp
    4.37 -
    4.38 -lemma binomial_eq_0 [rule_format]: "\<forall>k. n < k --> (n choose k) = 0"
    4.39 -apply (induct "n")
    4.40 -apply auto
    4.41 -done
    4.42 -
    4.43 -declare binomial_0 [simp del] binomial_Suc [simp del]
    4.44 -
    4.45 -lemma binomial_n_n [simp]: "(n choose n) = 1"
    4.46 -apply (induct "n")
    4.47 -apply (simp_all add: binomial_eq_0)
    4.48 -done
    4.49 -
    4.50 -lemma binomial_Suc_n [simp]: "(Suc n choose n) = Suc n"
    4.51 -by (induct "n", simp_all)
    4.52 -
    4.53 -lemma binomial_1 [simp]: "(n choose Suc 0) = n"
    4.54 -by (induct "n", simp_all)
    4.55 -
    4.56 -lemma zero_less_binomial [rule_format]: "k \<le> n --> 0 < (n choose k)"
    4.57 -by (rule_tac m = n and n = k in diff_induct, simp_all)
    4.58 -
    4.59 -lemma binomial_eq_0_iff: "(n choose k = 0) = (n<k)"
    4.60 -apply (safe intro!: binomial_eq_0)
    4.61 -apply (erule contrapos_pp)
    4.62 -apply (simp add: zero_less_binomial)
    4.63 -done
    4.64 -
    4.65 -lemma zero_less_binomial_iff: "(0 < n choose k) = (k\<le>n)"
    4.66 -by (simp add: linorder_not_less [symmetric] binomial_eq_0_iff [symmetric])
    4.67 -
    4.68 -(*Might be more useful if re-oriented*)
    4.69 -lemma Suc_times_binomial_eq [rule_format]:
    4.70 -     "\<forall>k. k \<le> n --> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k"
    4.71 -apply (induct "n")
    4.72 -apply (simp add: binomial_0, clarify)
    4.73 -apply (case_tac "k")
    4.74 -apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq
    4.75 -                      binomial_eq_0)
    4.76 -done
    4.77 -
    4.78 -text{*This is the well-known version, but it's harder to use because of the
    4.79 -  need to reason about division.*}
    4.80 -lemma binomial_Suc_Suc_eq_times:
    4.81 -     "k \<le> n ==> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k"
    4.82 -by (simp add: Suc_times_binomial_eq div_mult_self_is_m zero_less_Suc
    4.83 -        del: mult_Suc mult_Suc_right)
    4.84 -
    4.85 -text{*Another version, with -1 instead of Suc.*}
    4.86 -lemma times_binomial_minus1_eq:
    4.87 -     "[|k \<le> n;  0<k|] ==> (n choose k) * k = n * ((n - 1) choose (k - 1))"
    4.88 -apply (cut_tac n = "n - 1" and k = "k - 1" in Suc_times_binomial_eq)
    4.89 -apply (simp split add: nat_diff_split, auto)
    4.90 -done
    4.91 -
    4.92 -subsubsection {* Theorems about @{text "choose"} *}
    4.93 -
    4.94 -text {*
    4.95 -  \medskip Basic theorem about @{text "choose"}.  By Florian
    4.96 -  Kamm\"uller, tidied by LCP.
    4.97 -*}
    4.98 -
    4.99 -lemma card_s_0_eq_empty:
   4.100 -    "finite A ==> card {B. B \<subseteq> A & card B = 0} = 1"
   4.101 -  apply (simp cong add: conj_cong add: finite_subset [THEN card_0_eq])
   4.102 -  apply (simp cong add: rev_conj_cong)
   4.103 -  done
   4.104 -
   4.105 -lemma choose_deconstruct: "finite M ==> x \<notin> M
   4.106 -  ==> {s. s <= insert x M & card(s) = Suc k}
   4.107 -       = {s. s <= M & card(s) = Suc k} Un
   4.108 -         {s. EX t. t <= M & card(t) = k & s = insert x t}"
   4.109 -  apply safe
   4.110 -   apply (auto intro: finite_subset [THEN card_insert_disjoint])
   4.111 -  apply (drule_tac x = "xa - {x}" in spec)
   4.112 -  apply (subgoal_tac "x \<notin> xa", auto)
   4.113 -  apply (erule rev_mp, subst card_Diff_singleton)
   4.114 -  apply (auto intro: finite_subset)
   4.115 -  done
   4.116 -
   4.117 -text{*There are as many subsets of @{term A} having cardinality @{term k}
   4.118 - as there are sets obtained from the former by inserting a fixed element
   4.119 - @{term x} into each.*}
   4.120 -lemma constr_bij:
   4.121 -   "[|finite A; x \<notin> A|] ==>
   4.122 -    card {B. EX C. C <= A & card(C) = k & B = insert x C} =
   4.123 -    card {B. B <= A & card(B) = k}"
   4.124 -  apply (rule_tac f = "%s. s - {x}" and g = "insert x" in card_bij_eq)
   4.125 -       apply (auto elim!: equalityE simp add: inj_on_def)
   4.126 -    apply (subst Diff_insert0, auto)
   4.127 -   txt {* finiteness of the two sets *}
   4.128 -   apply (rule_tac [2] B = "Pow (A)" in finite_subset)
   4.129 -   apply (rule_tac B = "Pow (insert x A)" in finite_subset)
   4.130 -   apply fast+
   4.131 -  done
   4.132 -
   4.133 -text {*
   4.134 -  Main theorem: combinatorial statement about number of subsets of a set.
   4.135 -*}
   4.136 -
   4.137 -lemma n_sub_lemma:
   4.138 -  "!!A. finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
   4.139 -  apply (induct k)
   4.140 -   apply (simp add: card_s_0_eq_empty, atomize)
   4.141 -  apply (rotate_tac -1, erule finite_induct)
   4.142 -   apply (simp_all (no_asm_simp) cong add: conj_cong
   4.143 -     add: card_s_0_eq_empty choose_deconstruct)
   4.144 -  apply (subst card_Un_disjoint)
   4.145 -     prefer 4 apply (force simp add: constr_bij)
   4.146 -    prefer 3 apply force
   4.147 -   prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2]
   4.148 -     finite_subset [of _ "Pow (insert x F)", standard])
   4.149 -  apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset])
   4.150 -  done
   4.151 -
   4.152 -theorem n_subsets:
   4.153 -    "finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
   4.154 -  by (simp add: n_sub_lemma)
   4.155 -
   4.156 -
   4.157 -text{* The binomial theorem (courtesy of Tobias Nipkow): *}
   4.158 -
   4.159 -theorem binomial: "(a+b::nat)^n = (\<Sum>k=0..n. (n choose k) * a^k * b^(n-k))"
   4.160 -proof (induct n)
   4.161 -  case 0 thus ?case by simp
   4.162 -next
   4.163 -  case (Suc n)
   4.164 -  have decomp: "{0..n+1} = {0} \<union> {n+1} \<union> {1..n}"
   4.165 -    by (auto simp add:atLeastAtMost_def atLeast_def atMost_def)
   4.166 -  have decomp2: "{0..n} = {0} \<union> {1..n}"
   4.167 -    by (auto simp add:atLeastAtMost_def atLeast_def atMost_def)
   4.168 -  have "(a+b::nat)^(n+1) = (a+b) * (\<Sum>k=0..n. (n choose k) * a^k * b^(n-k))"
   4.169 -    using Suc by simp
   4.170 -  also have "\<dots> =  a*(\<Sum>k=0..n. (n choose k) * a^k * b^(n-k)) +
   4.171 -                   b*(\<Sum>k=0..n. (n choose k) * a^k * b^(n-k))"
   4.172 -    by(rule nat_distrib)
   4.173 -  also have "\<dots> = (\<Sum>k=0..n. (n choose k) * a^(k+1) * b^(n-k)) +
   4.174 -                  (\<Sum>k=0..n. (n choose k) * a^k * b^(n-k+1))"
   4.175 -    by(simp add: setsum_right_distrib mult_ac)
   4.176 -  also have "\<dots> = (\<Sum>k=0..n. (n choose k) * a^k * b^(n+1-k)) +
   4.177 -                  (\<Sum>k=1..n+1. (n choose (k - 1)) * a^k * b^(n+1-k))"
   4.178 -    by (simp add:setsum_shift_bounds_cl_Suc_ivl Suc_diff_le
   4.179 -             del:setsum_cl_ivl_Suc)
   4.180 -  also have "\<dots> = a^(n+1) + b^(n+1) +
   4.181 -                  (\<Sum>k=1..n. (n choose (k - 1)) * a^k * b^(n+1-k)) +
   4.182 -                  (\<Sum>k=1..n. (n choose k) * a^k * b^(n+1-k))"
   4.183 -    by(simp add: decomp2)
   4.184 -  also have
   4.185 -    "\<dots> = a^(n+1) + b^(n+1) + (\<Sum>k=1..n. (n+1 choose k) * a^k * b^(n+1-k))"
   4.186 -    by(simp add: nat_distrib setsum_addf binomial.simps)
   4.187 -  also have "\<dots> = (\<Sum>k=0..n+1. (n+1 choose k) * a^k * b^(n+1-k))"
   4.188 -    using decomp by simp
   4.189 -  finally show ?case by simp
   4.190 -qed
   4.191 -
   4.192 -end
     5.1 --- a/src/HOL/Complex/ROOT.ML	Wed Nov 08 22:24:54 2006 +0100
     5.2 +++ b/src/HOL/Complex/ROOT.ML	Wed Nov 08 23:11:13 2006 +0100
     5.3 @@ -6,6 +6,8 @@
     5.4  *)
     5.5  
     5.6  no_document use_thy "Infinite_Set";
     5.7 -with_path "../Real"      use_thy "Float";
     5.8 +no_document use_thy "Parity";
     5.9 +
    5.10 +with_path "../Real" use_thy "Float";
    5.11  with_path "../Hyperreal" use_thy "Hyperreal";
    5.12  time_use_thy "Complex_Main";
     6.1 --- a/src/HOL/GCD.thy	Wed Nov 08 22:24:54 2006 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,210 +0,0 @@
     6.4 -(*  Title:      HOL/GCD.thy
     6.5 -    ID:         $Id$
     6.6 -    Author:     Christophe Tabacznyj and Lawrence C Paulson
     6.7 -    Copyright   1996  University of Cambridge
     6.8 -
     6.9 -Builds on Integ/Parity mainly because that contains recdef, which we
    6.10 -need, but also because we may want to include gcd on integers in here
    6.11 -as well in the future.
    6.12 -*)
    6.13 -
    6.14 -header {* The Greatest Common Divisor *}
    6.15 -
    6.16 -theory GCD
    6.17 -imports Parity
    6.18 -begin
    6.19 -
    6.20 -text {*
    6.21 -  See \cite{davenport92}.
    6.22 -  \bigskip
    6.23 -*}
    6.24 -
    6.25 -consts
    6.26 -  gcd  :: "nat \<times> nat => nat"  -- {* Euclid's algorithm *}
    6.27 -
    6.28 -recdef gcd  "measure ((\<lambda>(m, n). n) :: nat \<times> nat => nat)"
    6.29 -  "gcd (m, n) = (if n = 0 then m else gcd (n, m mod n))"
    6.30 -
    6.31 -constdefs
    6.32 -  is_gcd :: "nat => nat => nat => bool"  -- {* @{term gcd} as a relation *}
    6.33 -  "is_gcd p m n == p dvd m \<and> p dvd n \<and>
    6.34 -    (\<forall>d. d dvd m \<and> d dvd n --> d dvd p)"
    6.35 -
    6.36 -
    6.37 -lemma gcd_induct:
    6.38 -  "(!!m. P m 0) ==>
    6.39 -    (!!m n. 0 < n ==> P n (m mod n) ==> P m n)
    6.40 -  ==> P (m::nat) (n::nat)"
    6.41 -  apply (induct m n rule: gcd.induct)
    6.42 -  apply (case_tac "n = 0")
    6.43 -   apply simp_all
    6.44 -  done
    6.45 -
    6.46 -
    6.47 -lemma gcd_0 [simp]: "gcd (m, 0) = m"
    6.48 -  apply simp
    6.49 -  done
    6.50 -
    6.51 -lemma gcd_non_0: "0 < n ==> gcd (m, n) = gcd (n, m mod n)"
    6.52 -  apply simp
    6.53 -  done
    6.54 -
    6.55 -declare gcd.simps [simp del]
    6.56 -
    6.57 -lemma gcd_1 [simp]: "gcd (m, Suc 0) = 1"
    6.58 -  apply (simp add: gcd_non_0)
    6.59 -  done
    6.60 -
    6.61 -text {*
    6.62 -  \medskip @{term "gcd (m, n)"} divides @{text m} and @{text n}.  The
    6.63 -  conjunctions don't seem provable separately.
    6.64 -*}
    6.65 -
    6.66 -lemma gcd_dvd1 [iff]: "gcd (m, n) dvd m"
    6.67 -  and gcd_dvd2 [iff]: "gcd (m, n) dvd n"
    6.68 -  apply (induct m n rule: gcd_induct)
    6.69 -   apply (simp_all add: gcd_non_0)
    6.70 -  apply (blast dest: dvd_mod_imp_dvd)
    6.71 -  done
    6.72 -
    6.73 -text {*
    6.74 -  \medskip Maximality: for all @{term m}, @{term n}, @{term k}
    6.75 -  naturals, if @{term k} divides @{term m} and @{term k} divides
    6.76 -  @{term n} then @{term k} divides @{term "gcd (m, n)"}.
    6.77 -*}
    6.78 -
    6.79 -lemma gcd_greatest: "k dvd m ==> k dvd n ==> k dvd gcd (m, n)"
    6.80 -  apply (induct m n rule: gcd_induct)
    6.81 -   apply (simp_all add: gcd_non_0 dvd_mod)
    6.82 -  done
    6.83 -
    6.84 -lemma gcd_greatest_iff [iff]: "(k dvd gcd (m, n)) = (k dvd m \<and> k dvd n)"
    6.85 -  apply (blast intro!: gcd_greatest intro: dvd_trans)
    6.86 -  done
    6.87 -
    6.88 -lemma gcd_zero: "(gcd (m, n) = 0) = (m = 0 \<and> n = 0)"
    6.89 -  by (simp only: dvd_0_left_iff [THEN sym] gcd_greatest_iff)
    6.90 -
    6.91 -
    6.92 -text {*
    6.93 -  \medskip Function gcd yields the Greatest Common Divisor.
    6.94 -*}
    6.95 -
    6.96 -lemma is_gcd: "is_gcd (gcd (m, n)) m n"
    6.97 -  apply (simp add: is_gcd_def gcd_greatest)
    6.98 -  done
    6.99 -
   6.100 -text {*
   6.101 -  \medskip Uniqueness of GCDs.
   6.102 -*}
   6.103 -
   6.104 -lemma is_gcd_unique: "is_gcd m a b ==> is_gcd n a b ==> m = n"
   6.105 -  apply (simp add: is_gcd_def)
   6.106 -  apply (blast intro: dvd_anti_sym)
   6.107 -  done
   6.108 -
   6.109 -lemma is_gcd_dvd: "is_gcd m a b ==> k dvd a ==> k dvd b ==> k dvd m"
   6.110 -  apply (auto simp add: is_gcd_def)
   6.111 -  done
   6.112 -
   6.113 -
   6.114 -text {*
   6.115 -  \medskip Commutativity
   6.116 -*}
   6.117 -
   6.118 -lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m"
   6.119 -  apply (auto simp add: is_gcd_def)
   6.120 -  done
   6.121 -
   6.122 -lemma gcd_commute: "gcd (m, n) = gcd (n, m)"
   6.123 -  apply (rule is_gcd_unique)
   6.124 -   apply (rule is_gcd)
   6.125 -  apply (subst is_gcd_commute)
   6.126 -  apply (simp add: is_gcd)
   6.127 -  done
   6.128 -
   6.129 -lemma gcd_assoc: "gcd (gcd (k, m), n) = gcd (k, gcd (m, n))"
   6.130 -  apply (rule is_gcd_unique)
   6.131 -   apply (rule is_gcd)
   6.132 -  apply (simp add: is_gcd_def)
   6.133 -  apply (blast intro: dvd_trans)
   6.134 -  done
   6.135 -
   6.136 -lemma gcd_0_left [simp]: "gcd (0, m) = m"
   6.137 -  apply (simp add: gcd_commute [of 0])
   6.138 -  done
   6.139 -
   6.140 -lemma gcd_1_left [simp]: "gcd (Suc 0, m) = 1"
   6.141 -  apply (simp add: gcd_commute [of "Suc 0"])
   6.142 -  done
   6.143 -
   6.144 -
   6.145 -text {*
   6.146 -  \medskip Multiplication laws
   6.147 -*}
   6.148 -
   6.149 -lemma gcd_mult_distrib2: "k * gcd (m, n) = gcd (k * m, k * n)"
   6.150 -    -- {* \cite[page 27]{davenport92} *}
   6.151 -  apply (induct m n rule: gcd_induct)
   6.152 -   apply simp
   6.153 -  apply (case_tac "k = 0")
   6.154 -   apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2)
   6.155 -  done
   6.156 -
   6.157 -lemma gcd_mult [simp]: "gcd (k, k * n) = k"
   6.158 -  apply (rule gcd_mult_distrib2 [of k 1 n, simplified, symmetric])
   6.159 -  done
   6.160 -
   6.161 -lemma gcd_self [simp]: "gcd (k, k) = k"
   6.162 -  apply (rule gcd_mult [of k 1, simplified])
   6.163 -  done
   6.164 -
   6.165 -lemma relprime_dvd_mult: "gcd (k, n) = 1 ==> k dvd m * n ==> k dvd m"
   6.166 -  apply (insert gcd_mult_distrib2 [of m k n])
   6.167 -  apply simp
   6.168 -  apply (erule_tac t = m in ssubst)
   6.169 -  apply simp
   6.170 -  done
   6.171 -
   6.172 -lemma relprime_dvd_mult_iff: "gcd (k, n) = 1 ==> (k dvd m * n) = (k dvd m)"
   6.173 -  apply (blast intro: relprime_dvd_mult dvd_trans)
   6.174 -  done
   6.175 -
   6.176 -lemma gcd_mult_cancel: "gcd (k, n) = 1 ==> gcd (k * m, n) = gcd (m, n)"
   6.177 -  apply (rule dvd_anti_sym)
   6.178 -   apply (rule gcd_greatest)
   6.179 -    apply (rule_tac n = k in relprime_dvd_mult)
   6.180 -     apply (simp add: gcd_assoc)
   6.181 -     apply (simp add: gcd_commute)
   6.182 -    apply (simp_all add: mult_commute)
   6.183 -  apply (blast intro: dvd_trans)
   6.184 -  done
   6.185 -
   6.186 -
   6.187 -text {* \medskip Addition laws *}
   6.188 -
   6.189 -lemma gcd_add1 [simp]: "gcd (m + n, n) = gcd (m, n)"
   6.190 -  apply (case_tac "n = 0")
   6.191 -   apply (simp_all add: gcd_non_0)
   6.192 -  done
   6.193 -
   6.194 -lemma gcd_add2 [simp]: "gcd (m, m + n) = gcd (m, n)"
   6.195 -proof -
   6.196 -  have "gcd (m, m + n) = gcd (m + n, m)" by (rule gcd_commute) 
   6.197 -  also have "... = gcd (n + m, m)" by (simp add: add_commute)
   6.198 -  also have "... = gcd (n, m)" by simp
   6.199 -  also have  "... = gcd (m, n)" by (rule gcd_commute) 
   6.200 -  finally show ?thesis .
   6.201 -qed
   6.202 -
   6.203 -lemma gcd_add2' [simp]: "gcd (m, n + m) = gcd (m, n)"
   6.204 -  apply (subst add_commute)
   6.205 -  apply (rule gcd_add2)
   6.206 -  done
   6.207 -
   6.208 -lemma gcd_add_mult: "gcd (m, k * m + n) = gcd (m, n)"
   6.209 -  apply (induct k)
   6.210 -   apply (simp_all add: add_assoc)
   6.211 -  done
   6.212 -
   6.213 -end
     7.1 --- a/src/HOL/Hyperreal/HyperPow.thy	Wed Nov 08 22:24:54 2006 +0100
     7.2 +++ b/src/HOL/Hyperreal/HyperPow.thy	Wed Nov 08 23:11:13 2006 +0100
     7.3 @@ -7,7 +7,7 @@
     7.4  header{*Exponentials on the Hyperreals*}
     7.5  
     7.6  theory HyperPow
     7.7 -imports HyperArith HyperNat
     7.8 +imports HyperArith HyperNat Parity
     7.9  begin
    7.10  
    7.11  (* consts hpowr :: "[hypreal,nat] => hypreal" *)
     8.1 --- a/src/HOL/Import/HOL/ROOT.ML	Wed Nov 08 22:24:54 2006 +0100
     8.2 +++ b/src/HOL/Import/HOL/ROOT.ML	Wed Nov 08 23:11:13 2006 +0100
     8.3 @@ -3,5 +3,6 @@
     8.4      Author:     Sebastian Skalberg (TU Muenchen)
     8.5  *)
     8.6  
     8.7 +use_thy "Primes";
     8.8  setmp quick_and_dirty true use_thy "HOL4Prob";
     8.9  setmp quick_and_dirty true use_thy "HOL4";
     9.1 --- a/src/HOL/Integ/Parity.thy	Wed Nov 08 22:24:54 2006 +0100
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,451 +0,0 @@
     9.4 -(*  Title:      Parity.thy
     9.5 -    ID:         $Id$
     9.6 -    Author:     Jeremy Avigad
     9.7 -*)
     9.8 -
     9.9 -header {* Even and Odd for ints and nats*}
    9.10 -
    9.11 -theory Parity
    9.12 -imports Divides IntDiv NatSimprocs
    9.13 -begin
    9.14 -
    9.15 -axclass even_odd < type
    9.16 -
    9.17 -consts
    9.18 -  even :: "'a::even_odd => bool"
    9.19 -
    9.20 -instance int :: even_odd ..
    9.21 -instance nat :: even_odd ..
    9.22 -
    9.23 -defs (overloaded)
    9.24 -  even_def: "even (x::int) == x mod 2 = 0"
    9.25 -  even_nat_def: "even (x::nat) == even (int x)"
    9.26 -
    9.27 -abbreviation
    9.28 -  odd :: "'a::even_odd => bool"
    9.29 -  "odd x == \<not> even x"
    9.30 -
    9.31 -
    9.32 -subsection {* Even and odd are mutually exclusive *}
    9.33 -
    9.34 -lemma int_pos_lt_two_imp_zero_or_one: 
    9.35 -    "0 <= x ==> (x::int) < 2 ==> x = 0 | x = 1"
    9.36 -  by auto
    9.37 -
    9.38 -lemma neq_one_mod_two [simp]: "((x::int) mod 2 ~= 0) = (x mod 2 = 1)"
    9.39 -  apply (subgoal_tac "x mod 2 = 0 | x mod 2 = 1", force)
    9.40 -  apply (rule int_pos_lt_two_imp_zero_or_one, auto)
    9.41 -  done
    9.42 -
    9.43 -subsection {* Behavior under integer arithmetic operations *}
    9.44 -
    9.45 -lemma even_times_anything: "even (x::int) ==> even (x * y)"
    9.46 -  by (simp add: even_def zmod_zmult1_eq')
    9.47 -
    9.48 -lemma anything_times_even: "even (y::int) ==> even (x * y)"
    9.49 -  by (simp add: even_def zmod_zmult1_eq)
    9.50 -
    9.51 -lemma odd_times_odd: "odd (x::int) ==> odd y ==> odd (x * y)"
    9.52 -  by (simp add: even_def zmod_zmult1_eq)
    9.53 -
    9.54 -lemma even_product: "even((x::int) * y) = (even x | even y)"
    9.55 -  apply (auto simp add: even_times_anything anything_times_even) 
    9.56 -  apply (rule ccontr)
    9.57 -  apply (auto simp add: odd_times_odd)
    9.58 -  done
    9.59 -
    9.60 -lemma even_plus_even: "even (x::int) ==> even y ==> even (x + y)"
    9.61 -  by (simp add: even_def zmod_zadd1_eq)
    9.62 -
    9.63 -lemma even_plus_odd: "even (x::int) ==> odd y ==> odd (x + y)"
    9.64 -  by (simp add: even_def zmod_zadd1_eq)
    9.65 -
    9.66 -lemma odd_plus_even: "odd (x::int) ==> even y ==> odd (x + y)"
    9.67 -  by (simp add: even_def zmod_zadd1_eq)
    9.68 -
    9.69 -lemma odd_plus_odd: "odd (x::int) ==> odd y ==> even (x + y)"
    9.70 -  by (simp add: even_def zmod_zadd1_eq)
    9.71 -
    9.72 -lemma even_sum: "even ((x::int) + y) = ((even x & even y) | (odd x & odd y))"
    9.73 -  apply (auto intro: even_plus_even odd_plus_odd)
    9.74 -  apply (rule ccontr, simp add: even_plus_odd)
    9.75 -  apply (rule ccontr, simp add: odd_plus_even)
    9.76 -  done
    9.77 -
    9.78 -lemma even_neg: "even (-(x::int)) = even x"
    9.79 -  by (auto simp add: even_def zmod_zminus1_eq_if)
    9.80 -
    9.81 -lemma even_difference: 
    9.82 -  "even ((x::int) - y) = ((even x & even y) | (odd x & odd y))"
    9.83 -  by (simp only: diff_minus even_sum even_neg)
    9.84 -
    9.85 -lemma even_pow_gt_zero [rule_format]: 
    9.86 -    "even (x::int) ==> 0 < n --> even (x^n)"
    9.87 -  apply (induct n)
    9.88 -  apply (auto simp add: even_product)
    9.89 -  done
    9.90 -
    9.91 -lemma odd_pow: "odd x ==> odd((x::int)^n)"
    9.92 -  apply (induct n)
    9.93 -  apply (simp add: even_def)
    9.94 -  apply (simp add: even_product)
    9.95 -  done
    9.96 -
    9.97 -lemma even_power: "even ((x::int)^n) = (even x & 0 < n)"
    9.98 -  apply (auto simp add: even_pow_gt_zero) 
    9.99 -  apply (erule contrapos_pp, erule odd_pow)
   9.100 -  apply (erule contrapos_pp, simp add: even_def)
   9.101 -  done
   9.102 -
   9.103 -lemma even_zero: "even (0::int)"
   9.104 -  by (simp add: even_def)
   9.105 -
   9.106 -lemma odd_one: "odd (1::int)"
   9.107 -  by (simp add: even_def)
   9.108 -
   9.109 -lemmas even_odd_simps [simp] = even_def[of "number_of v",standard] even_zero 
   9.110 -  odd_one even_product even_sum even_neg even_difference even_power
   9.111 -
   9.112 -
   9.113 -subsection {* Equivalent definitions *}
   9.114 -
   9.115 -lemma two_times_even_div_two: "even (x::int) ==> 2 * (x div 2) = x" 
   9.116 -  by (auto simp add: even_def)
   9.117 -
   9.118 -lemma two_times_odd_div_two_plus_one: "odd (x::int) ==> 
   9.119 -    2 * (x div 2) + 1 = x"
   9.120 -  apply (insert zmod_zdiv_equality [of x 2, THEN sym])
   9.121 -  by (simp add: even_def)
   9.122 -
   9.123 -lemma even_equiv_def: "even (x::int) = (EX y. x = 2 * y)"
   9.124 -  apply auto
   9.125 -  apply (rule exI)
   9.126 -  by (erule two_times_even_div_two [THEN sym])
   9.127 -
   9.128 -lemma odd_equiv_def: "odd (x::int) = (EX y. x = 2 * y + 1)"
   9.129 -  apply auto
   9.130 -  apply (rule exI)
   9.131 -  by (erule two_times_odd_div_two_plus_one [THEN sym])
   9.132 -
   9.133 -
   9.134 -subsection {* even and odd for nats *}
   9.135 -
   9.136 -lemma pos_int_even_equiv_nat_even: "0 \<le> x ==> even x = even (nat x)"
   9.137 -  by (simp add: even_nat_def)
   9.138 -
   9.139 -lemma even_nat_product: "even((x::nat) * y) = (even x | even y)"
   9.140 -  by (simp add: even_nat_def int_mult)
   9.141 -
   9.142 -lemma even_nat_sum: "even ((x::nat) + y) = 
   9.143 -    ((even x & even y) | (odd x & odd y))"
   9.144 -  by (unfold even_nat_def, simp)
   9.145 -
   9.146 -lemma even_nat_difference: 
   9.147 -    "even ((x::nat) - y) = (x < y | (even x & even y) | (odd x & odd y))"
   9.148 -  apply (auto simp add: even_nat_def zdiff_int [THEN sym])
   9.149 -  apply (case_tac "x < y", auto simp add: zdiff_int [THEN sym])
   9.150 -  apply (case_tac "x < y", auto simp add: zdiff_int [THEN sym])
   9.151 -  done
   9.152 -
   9.153 -lemma even_nat_Suc: "even (Suc x) = odd x"
   9.154 -  by (simp add: even_nat_def)
   9.155 -
   9.156 -lemma even_nat_power: "even ((x::nat)^y) = (even x & 0 < y)"
   9.157 -  by (simp add: even_nat_def int_power)
   9.158 -
   9.159 -lemma even_nat_zero: "even (0::nat)"
   9.160 -  by (simp add: even_nat_def)
   9.161 -
   9.162 -lemmas even_odd_nat_simps [simp] = even_nat_def[of "number_of v",standard] 
   9.163 -  even_nat_zero even_nat_Suc even_nat_product even_nat_sum even_nat_power
   9.164 -
   9.165 -
   9.166 -subsection {* Equivalent definitions *}
   9.167 -
   9.168 -lemma nat_lt_two_imp_zero_or_one: "(x::nat) < Suc (Suc 0) ==> 
   9.169 -    x = 0 | x = Suc 0"
   9.170 -  by auto
   9.171 -
   9.172 -lemma even_nat_mod_two_eq_zero: "even (x::nat) ==> x mod (Suc (Suc 0)) = 0"
   9.173 -  apply (insert mod_div_equality [of x "Suc (Suc 0)", THEN sym])
   9.174 -  apply (drule subst, assumption)
   9.175 -  apply (subgoal_tac "x mod Suc (Suc 0) = 0 | x mod Suc (Suc 0) = Suc 0")
   9.176 -  apply force
   9.177 -  apply (subgoal_tac "0 < Suc (Suc 0)")
   9.178 -  apply (frule mod_less_divisor [of "Suc (Suc 0)" x])
   9.179 -  apply (erule nat_lt_two_imp_zero_or_one, auto)
   9.180 -  done
   9.181 -
   9.182 -lemma odd_nat_mod_two_eq_one: "odd (x::nat) ==> x mod (Suc (Suc 0)) = Suc 0"
   9.183 -  apply (insert mod_div_equality [of x "Suc (Suc 0)", THEN sym])
   9.184 -  apply (drule subst, assumption)
   9.185 -  apply (subgoal_tac "x mod Suc (Suc 0) = 0 | x mod Suc (Suc 0) = Suc 0")
   9.186 -  apply force 
   9.187 -  apply (subgoal_tac "0 < Suc (Suc 0)")
   9.188 -  apply (frule mod_less_divisor [of "Suc (Suc 0)" x])
   9.189 -  apply (erule nat_lt_two_imp_zero_or_one, auto)
   9.190 -  done
   9.191 -
   9.192 -lemma even_nat_equiv_def: "even (x::nat) = (x mod Suc (Suc 0) = 0)" 
   9.193 -  apply (rule iffI)
   9.194 -  apply (erule even_nat_mod_two_eq_zero)
   9.195 -  apply (insert odd_nat_mod_two_eq_one [of x], auto)
   9.196 -  done
   9.197 -
   9.198 -lemma odd_nat_equiv_def: "odd (x::nat) = (x mod Suc (Suc 0) = Suc 0)"
   9.199 -  apply (auto simp add: even_nat_equiv_def)
   9.200 -  apply (subgoal_tac "x mod (Suc (Suc 0)) < Suc (Suc 0)")
   9.201 -  apply (frule nat_lt_two_imp_zero_or_one, auto)
   9.202 -  done
   9.203 -
   9.204 -lemma even_nat_div_two_times_two: "even (x::nat) ==> 
   9.205 -    Suc (Suc 0) * (x div Suc (Suc 0)) = x"
   9.206 -  apply (insert mod_div_equality [of x "Suc (Suc 0)", THEN sym])
   9.207 -  apply (drule even_nat_mod_two_eq_zero, simp)
   9.208 -  done
   9.209 -
   9.210 -lemma odd_nat_div_two_times_two_plus_one: "odd (x::nat) ==> 
   9.211 -    Suc( Suc (Suc 0) * (x div Suc (Suc 0))) = x"  
   9.212 -  apply (insert mod_div_equality [of x "Suc (Suc 0)", THEN sym])
   9.213 -  apply (drule odd_nat_mod_two_eq_one, simp)
   9.214 -  done
   9.215 -
   9.216 -lemma even_nat_equiv_def2: "even (x::nat) = (EX y. x = Suc (Suc 0) * y)"
   9.217 -  apply (rule iffI, rule exI)
   9.218 -  apply (erule even_nat_div_two_times_two [THEN sym], auto)
   9.219 -  done
   9.220 -
   9.221 -lemma odd_nat_equiv_def2: "odd (x::nat) = (EX y. x = Suc(Suc (Suc 0) * y))"
   9.222 -  apply (rule iffI, rule exI)
   9.223 -  apply (erule odd_nat_div_two_times_two_plus_one [THEN sym], auto)
   9.224 -  done
   9.225 -
   9.226 -subsection {* Parity and powers *}
   9.227 -
   9.228 -lemma minus_one_even_odd_power:
   9.229 -     "(even x --> (- 1::'a::{comm_ring_1,recpower})^x = 1) & 
   9.230 -      (odd x --> (- 1::'a)^x = - 1)"
   9.231 -  apply (induct x)
   9.232 -  apply (rule conjI)
   9.233 -  apply simp
   9.234 -  apply (insert even_nat_zero, blast)
   9.235 -  apply (simp add: power_Suc)
   9.236 -done
   9.237 -
   9.238 -lemma minus_one_even_power [simp]:
   9.239 -     "even x ==> (- 1::'a::{comm_ring_1,recpower})^x = 1"
   9.240 -  by (rule minus_one_even_odd_power [THEN conjunct1, THEN mp], assumption)
   9.241 -
   9.242 -lemma minus_one_odd_power [simp]:
   9.243 -     "odd x ==> (- 1::'a::{comm_ring_1,recpower})^x = - 1"
   9.244 -  by (rule minus_one_even_odd_power [THEN conjunct2, THEN mp], assumption)
   9.245 -
   9.246 -lemma neg_one_even_odd_power:
   9.247 -     "(even x --> (-1::'a::{number_ring,recpower})^x = 1) & 
   9.248 -      (odd x --> (-1::'a)^x = -1)"
   9.249 -  apply (induct x)
   9.250 -  apply (simp, simp add: power_Suc)
   9.251 -  done
   9.252 -
   9.253 -lemma neg_one_even_power [simp]:
   9.254 -     "even x ==> (-1::'a::{number_ring,recpower})^x = 1"
   9.255 -  by (rule neg_one_even_odd_power [THEN conjunct1, THEN mp], assumption)
   9.256 -
   9.257 -lemma neg_one_odd_power [simp]:
   9.258 -     "odd x ==> (-1::'a::{number_ring,recpower})^x = -1"
   9.259 -  by (rule neg_one_even_odd_power [THEN conjunct2, THEN mp], assumption)
   9.260 -
   9.261 -lemma neg_power_if:
   9.262 -     "(-x::'a::{comm_ring_1,recpower}) ^ n = 
   9.263 -      (if even n then (x ^ n) else -(x ^ n))"
   9.264 -  by (induct n, simp_all split: split_if_asm add: power_Suc) 
   9.265 -
   9.266 -lemma zero_le_even_power: "even n ==> 
   9.267 -    0 <= (x::'a::{recpower,ordered_ring_strict}) ^ n"
   9.268 -  apply (simp add: even_nat_equiv_def2)
   9.269 -  apply (erule exE)
   9.270 -  apply (erule ssubst)
   9.271 -  apply (subst power_add)
   9.272 -  apply (rule zero_le_square)
   9.273 -  done
   9.274 -
   9.275 -lemma zero_le_odd_power: "odd n ==> 
   9.276 -    (0 <= (x::'a::{recpower,ordered_idom}) ^ n) = (0 <= x)"
   9.277 -  apply (simp add: odd_nat_equiv_def2)
   9.278 -  apply (erule exE)
   9.279 -  apply (erule ssubst)
   9.280 -  apply (subst power_Suc)
   9.281 -  apply (subst power_add)
   9.282 -  apply (subst zero_le_mult_iff)
   9.283 -  apply auto
   9.284 -  apply (subgoal_tac "x = 0 & 0 < y")
   9.285 -  apply (erule conjE, assumption)
   9.286 -  apply (subst power_eq_0_iff [THEN sym])
   9.287 -  apply (subgoal_tac "0 <= x^y * x^y")
   9.288 -  apply simp
   9.289 -  apply (rule zero_le_square)+
   9.290 -done
   9.291 -
   9.292 -lemma zero_le_power_eq: "(0 <= (x::'a::{recpower,ordered_idom}) ^ n) = 
   9.293 -    (even n | (odd n & 0 <= x))"
   9.294 -  apply auto
   9.295 -  apply (subst zero_le_odd_power [THEN sym])
   9.296 -  apply assumption+
   9.297 -  apply (erule zero_le_even_power)
   9.298 -  apply (subst zero_le_odd_power) 
   9.299 -  apply assumption+
   9.300 -done
   9.301 -
   9.302 -lemma zero_less_power_eq: "(0 < (x::'a::{recpower,ordered_idom}) ^ n) = 
   9.303 -    (n = 0 | (even n & x ~= 0) | (odd n & 0 < x))"
   9.304 -  apply (rule iffI)
   9.305 -  apply clarsimp
   9.306 -  apply (rule conjI)
   9.307 -  apply clarsimp
   9.308 -  apply (rule ccontr)
   9.309 -  apply (subgoal_tac "~ (0 <= x^n)")
   9.310 -  apply simp
   9.311 -  apply (subst zero_le_odd_power)
   9.312 -  apply assumption 
   9.313 -  apply simp
   9.314 -  apply (rule notI)
   9.315 -  apply (simp add: power_0_left)
   9.316 -  apply (rule notI)
   9.317 -  apply (simp add: power_0_left)
   9.318 -  apply auto
   9.319 -  apply (subgoal_tac "0 <= x^n")
   9.320 -  apply (frule order_le_imp_less_or_eq)
   9.321 -  apply simp
   9.322 -  apply (erule zero_le_even_power)
   9.323 -  apply (subgoal_tac "0 <= x^n")
   9.324 -  apply (frule order_le_imp_less_or_eq)
   9.325 -  apply auto
   9.326 -  apply (subst zero_le_odd_power)
   9.327 -  apply assumption
   9.328 -  apply (erule order_less_imp_le)
   9.329 -done
   9.330 -
   9.331 -lemma power_less_zero_eq: "((x::'a::{recpower,ordered_idom}) ^ n < 0) =
   9.332 -    (odd n & x < 0)" 
   9.333 -  apply (subst linorder_not_le [THEN sym])+
   9.334 -  apply (subst zero_le_power_eq)
   9.335 -  apply auto
   9.336 -done
   9.337 -
   9.338 -lemma power_le_zero_eq: "((x::'a::{recpower,ordered_idom}) ^ n <= 0) =
   9.339 -    (n ~= 0 & ((odd n & x <= 0) | (even n & x = 0)))"
   9.340 -  apply (subst linorder_not_less [THEN sym])+
   9.341 -  apply (subst zero_less_power_eq)
   9.342 -  apply auto
   9.343 -done
   9.344 -
   9.345 -lemma power_even_abs: "even n ==> 
   9.346 -    (abs (x::'a::{recpower,ordered_idom}))^n = x^n"
   9.347 -  apply (subst power_abs [THEN sym])
   9.348 -  apply (simp add: zero_le_even_power)
   9.349 -done
   9.350 -
   9.351 -lemma zero_less_power_nat_eq: "(0 < (x::nat) ^ n) = (n = 0 | 0 < x)"
   9.352 -  by (induct n, auto)
   9.353 -
   9.354 -lemma power_minus_even [simp]: "even n ==> 
   9.355 -    (- x)^n = (x^n::'a::{recpower,comm_ring_1})"
   9.356 -  apply (subst power_minus)
   9.357 -  apply simp
   9.358 -done
   9.359 -
   9.360 -lemma power_minus_odd [simp]: "odd n ==> 
   9.361 -    (- x)^n = - (x^n::'a::{recpower,comm_ring_1})"
   9.362 -  apply (subst power_minus)
   9.363 -  apply simp
   9.364 -done
   9.365 -
   9.366 -(* Simplify, when the exponent is a numeral *)
   9.367 -
   9.368 -lemmas power_0_left_number_of = power_0_left [of "number_of w", standard]
   9.369 -declare power_0_left_number_of [simp]
   9.370 -
   9.371 -lemmas zero_le_power_eq_number_of =
   9.372 -    zero_le_power_eq [of _ "number_of w", standard]
   9.373 -declare zero_le_power_eq_number_of [simp]
   9.374 -
   9.375 -lemmas zero_less_power_eq_number_of =
   9.376 -    zero_less_power_eq [of _ "number_of w", standard]
   9.377 -declare zero_less_power_eq_number_of [simp]
   9.378 -
   9.379 -lemmas power_le_zero_eq_number_of =
   9.380 -    power_le_zero_eq [of _ "number_of w", standard]
   9.381 -declare power_le_zero_eq_number_of [simp]
   9.382 -
   9.383 -lemmas power_less_zero_eq_number_of =
   9.384 -    power_less_zero_eq [of _ "number_of w", standard]
   9.385 -declare power_less_zero_eq_number_of [simp]
   9.386 -
   9.387 -lemmas zero_less_power_nat_eq_number_of =
   9.388 -    zero_less_power_nat_eq [of _ "number_of w", standard]
   9.389 -declare zero_less_power_nat_eq_number_of [simp]
   9.390 -
   9.391 -lemmas power_eq_0_iff_number_of = power_eq_0_iff [of _ "number_of w", standard]
   9.392 -declare power_eq_0_iff_number_of [simp]
   9.393 -
   9.394 -lemmas power_even_abs_number_of = power_even_abs [of "number_of w" _, standard]
   9.395 -declare power_even_abs_number_of [simp]
   9.396 -
   9.397 -
   9.398 -subsection {* An Equivalence for @{term [source] "0 \<le> a^n"} *}
   9.399 -
   9.400 -lemma even_power_le_0_imp_0:
   9.401 -     "a ^ (2*k) \<le> (0::'a::{ordered_idom,recpower}) ==> a=0"
   9.402 -apply (induct k) 
   9.403 -apply (auto simp add: zero_le_mult_iff mult_le_0_iff power_Suc)  
   9.404 -done
   9.405 -
   9.406 -lemma zero_le_power_iff:
   9.407 -     "(0 \<le> a^n) = (0 \<le> (a::'a::{ordered_idom,recpower}) | even n)"
   9.408 -      (is "?P n")
   9.409 -proof cases
   9.410 -  assume even: "even n"
   9.411 -  then obtain k where "n = 2*k"
   9.412 -    by (auto simp add: even_nat_equiv_def2 numeral_2_eq_2)
   9.413 -  thus ?thesis by (simp add: zero_le_even_power even) 
   9.414 -next
   9.415 -  assume odd: "odd n"
   9.416 -  then obtain k where "n = Suc(2*k)"
   9.417 -    by (auto simp add: odd_nat_equiv_def2 numeral_2_eq_2)
   9.418 -  thus ?thesis
   9.419 -    by (auto simp add: power_Suc zero_le_mult_iff zero_le_even_power 
   9.420 -             dest!: even_power_le_0_imp_0) 
   9.421 -qed 
   9.422 -
   9.423 -subsection {* Miscellaneous *}
   9.424 -
   9.425 -lemma even_plus_one_div_two: "even (x::int) ==> (x + 1) div 2 = x div 2"
   9.426 -  apply (subst zdiv_zadd1_eq)
   9.427 -  apply (simp add: even_def)
   9.428 -  done
   9.429 -
   9.430 -lemma odd_plus_one_div_two: "odd (x::int) ==> (x + 1) div 2 = x div 2 + 1"
   9.431 -  apply (subst zdiv_zadd1_eq)
   9.432 -  apply (simp add: even_def)
   9.433 -  done
   9.434 -
   9.435 -lemma div_Suc: "Suc a div c = a div c + Suc 0 div c + 
   9.436 -    (a mod c + Suc 0 mod c) div c"
   9.437 -  apply (subgoal_tac "Suc a = a + Suc 0")
   9.438 -  apply (erule ssubst)
   9.439 -  apply (rule div_add1_eq, simp)
   9.440 -  done
   9.441 -
   9.442 -lemma even_nat_plus_one_div_two: "even (x::nat) ==> 
   9.443 -   (Suc x) div Suc (Suc 0) = x div Suc (Suc 0)"
   9.444 -  apply (subst div_Suc)
   9.445 -  apply (simp add: even_nat_equiv_def)
   9.446 -  done
   9.447 -
   9.448 -lemma odd_nat_plus_one_div_two: "odd (x::nat) ==> 
   9.449 -    (Suc x) div Suc (Suc 0) = Suc (x div Suc (Suc 0))"
   9.450 -  apply (subst div_Suc)
   9.451 -  apply (simp add: odd_nat_equiv_def)
   9.452 -  done
   9.453 -
   9.454 -end
    10.1 --- a/src/HOL/IsaMakefile	Wed Nov 08 22:24:54 2006 +0100
    10.2 +++ b/src/HOL/IsaMakefile	Wed Nov 08 23:11:13 2006 +0100
    10.3 @@ -84,13 +84,13 @@
    10.4    $(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML			\
    10.5    $(SRC)/TFL/thry.ML $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML			\
    10.6    Tools/res_atpset.ML \
    10.7 -  Binomial.thy Code_Generator.thy Datatype.ML Datatype.thy			\
    10.8 +  Code_Generator.thy Datatype.ML Datatype.thy			\
    10.9    Divides.thy						\
   10.10    Equiv_Relations.thy Extraction.thy Finite_Set.ML Finite_Set.thy		\
   10.11    FixedPoint.thy Fun.thy HOL.ML HOL.thy Hilbert_Choice.thy Inductive.thy	\
   10.12    Integ/IntArith.thy Integ/IntDef.thy Integ/IntDiv.thy				\
   10.13    Integ/NatBin.thy Integ/NatSimprocs.thy Integ/Numeral.thy			\
   10.14 -  Integ/Parity.thy Integ/Presburger.thy Integ/cooper_dec.ML			\
   10.15 +  Integ/Presburger.thy Integ/cooper_dec.ML			\
   10.16    Integ/cooper_proof.ML Integ/reflected_presburger.ML				\
   10.17    Integ/reflected_cooper.ML Integ/int_arith1.ML Integ/int_factor_simprocs.ML	\
   10.18    Integ/nat_simprocs.ML Integ/presburger.ML Integ/qelim.ML LOrder.thy		\
   10.19 @@ -182,7 +182,7 @@
   10.20    Complex/Complex_Main.thy Complex/CLim.thy Complex/CSeries.thy			\
   10.21    Complex/CStar.thy Complex/Complex.thy Complex/ComplexBin.thy			\
   10.22    Complex/NSCA.thy Complex/NSComplex.thy Complex/document/root.tex 		\
   10.23 -  Library/Infinite_Set.thy
   10.24 +  Library/Infinite_Set.thy Library/Parity.thy
   10.25  	@cd Complex; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-Complex
   10.26  
   10.27  
   10.28 @@ -215,7 +215,8 @@
   10.29    Library/Library/document/root.bib Library/While_Combinator.thy \
   10.30    Library/Product_ord.thy Library/Char_ord.thy \
   10.31    Library/List_lexord.thy Library/Commutative_Ring.thy Library/comm_ring.ML \
   10.32 -  Library/Coinductive_List.thy Library/AssocList.thy
   10.33 +  Library/Coinductive_List.thy Library/AssocList.thy \
   10.34 +  Library/Parity.thy Library/GCD.thy Library/Binomial.thy
   10.35  	@cd Library; $(ISATOOL) usedir $(OUT)/HOL Library
   10.36  
   10.37  
   10.38 @@ -656,7 +657,7 @@
   10.39    ex/SAT_Examples.thy ex/svc_oracle.ML ex/SVC_Oracle.thy 			\
   10.40    ex/Sudoku.thy ex/Tarski.thy ex/document/root.bib ex/document/root.tex		\
   10.41    ex/mesontest2.ML ex/mesontest2.thy ex/reflection.ML ex/set.thy		\
   10.42 -  ex/svc_funcs.ML ex/svc_test.thy
   10.43 +  ex/svc_funcs.ML ex/svc_test.thy Library/Parity.thy Library/GCD.thy
   10.44  	@$(ISATOOL) usedir $(OUT)/HOL ex
   10.45  
   10.46  
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/Library/Binomial.thy	Wed Nov 08 23:11:13 2006 +0100
    11.3 @@ -0,0 +1,189 @@
    11.4 +(*  Title:      HOL/Binomial.thy
    11.5 +    ID:         $Id$
    11.6 +    Author:     Lawrence C Paulson
    11.7 +    Copyright   1997  University of Cambridge
    11.8 +*)
    11.9 +
   11.10 +header{*Binomial Coefficients*}
   11.11 +
   11.12 +theory Binomial
   11.13 +imports Main
   11.14 +begin
   11.15 +
   11.16 +text{*This development is based on the work of Andy Gordon and
   11.17 +Florian Kammueller*}
   11.18 +
   11.19 +consts
   11.20 +  binomial :: "nat \<Rightarrow> nat \<Rightarrow> nat"      (infixl "choose" 65)
   11.21 +
   11.22 +primrec
   11.23 +  binomial_0:   "(0     choose k) = (if k = 0 then 1 else 0)"
   11.24 +
   11.25 +  binomial_Suc: "(Suc n choose k) =
   11.26 +                 (if k = 0 then 1 else (n choose (k - 1)) + (n choose k))"
   11.27 +
   11.28 +lemma binomial_n_0 [simp]: "(n choose 0) = 1"
   11.29 +by (cases n) simp_all
   11.30 +
   11.31 +lemma binomial_0_Suc [simp]: "(0 choose Suc k) = 0"
   11.32 +by simp
   11.33 +
   11.34 +lemma binomial_Suc_Suc [simp]:
   11.35 +     "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)"
   11.36 +by simp
   11.37 +
   11.38 +lemma binomial_eq_0 [rule_format]: "\<forall>k. n < k --> (n choose k) = 0"
   11.39 +apply (induct "n")
   11.40 +apply auto
   11.41 +done
   11.42 +
   11.43 +declare binomial_0 [simp del] binomial_Suc [simp del]
   11.44 +
   11.45 +lemma binomial_n_n [simp]: "(n choose n) = 1"
   11.46 +apply (induct "n")
   11.47 +apply (simp_all add: binomial_eq_0)
   11.48 +done
   11.49 +
   11.50 +lemma binomial_Suc_n [simp]: "(Suc n choose n) = Suc n"
   11.51 +by (induct "n", simp_all)
   11.52 +
   11.53 +lemma binomial_1 [simp]: "(n choose Suc 0) = n"
   11.54 +by (induct "n", simp_all)
   11.55 +
   11.56 +lemma zero_less_binomial [rule_format]: "k \<le> n --> 0 < (n choose k)"
   11.57 +by (rule_tac m = n and n = k in diff_induct, simp_all)
   11.58 +
   11.59 +lemma binomial_eq_0_iff: "(n choose k = 0) = (n<k)"
   11.60 +apply (safe intro!: binomial_eq_0)
   11.61 +apply (erule contrapos_pp)
   11.62 +apply (simp add: zero_less_binomial)
   11.63 +done
   11.64 +
   11.65 +lemma zero_less_binomial_iff: "(0 < n choose k) = (k\<le>n)"
   11.66 +by (simp add: linorder_not_less [symmetric] binomial_eq_0_iff [symmetric])
   11.67 +
   11.68 +(*Might be more useful if re-oriented*)
   11.69 +lemma Suc_times_binomial_eq [rule_format]:
   11.70 +     "\<forall>k. k \<le> n --> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k"
   11.71 +apply (induct "n")
   11.72 +apply (simp add: binomial_0, clarify)
   11.73 +apply (case_tac "k")
   11.74 +apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq
   11.75 +                      binomial_eq_0)
   11.76 +done
   11.77 +
   11.78 +text{*This is the well-known version, but it's harder to use because of the
   11.79 +  need to reason about division.*}
   11.80 +lemma binomial_Suc_Suc_eq_times:
   11.81 +     "k \<le> n ==> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k"
   11.82 +by (simp add: Suc_times_binomial_eq div_mult_self_is_m zero_less_Suc
   11.83 +        del: mult_Suc mult_Suc_right)
   11.84 +
   11.85 +text{*Another version, with -1 instead of Suc.*}
   11.86 +lemma times_binomial_minus1_eq:
   11.87 +     "[|k \<le> n;  0<k|] ==> (n choose k) * k = n * ((n - 1) choose (k - 1))"
   11.88 +apply (cut_tac n = "n - 1" and k = "k - 1" in Suc_times_binomial_eq)
   11.89 +apply (simp split add: nat_diff_split, auto)
   11.90 +done
   11.91 +
   11.92 +subsubsection {* Theorems about @{text "choose"} *}
   11.93 +
   11.94 +text {*
   11.95 +  \medskip Basic theorem about @{text "choose"}.  By Florian
   11.96 +  Kamm\"uller, tidied by LCP.
   11.97 +*}
   11.98 +
   11.99 +lemma card_s_0_eq_empty:
  11.100 +    "finite A ==> card {B. B \<subseteq> A & card B = 0} = 1"
  11.101 +  apply (simp cong add: conj_cong add: finite_subset [THEN card_0_eq])
  11.102 +  apply (simp cong add: rev_conj_cong)
  11.103 +  done
  11.104 +
  11.105 +lemma choose_deconstruct: "finite M ==> x \<notin> M
  11.106 +  ==> {s. s <= insert x M & card(s) = Suc k}
  11.107 +       = {s. s <= M & card(s) = Suc k} Un
  11.108 +         {s. EX t. t <= M & card(t) = k & s = insert x t}"
  11.109 +  apply safe
  11.110 +   apply (auto intro: finite_subset [THEN card_insert_disjoint])
  11.111 +  apply (drule_tac x = "xa - {x}" in spec)
  11.112 +  apply (subgoal_tac "x \<notin> xa", auto)
  11.113 +  apply (erule rev_mp, subst card_Diff_singleton)
  11.114 +  apply (auto intro: finite_subset)
  11.115 +  done
  11.116 +
  11.117 +text{*There are as many subsets of @{term A} having cardinality @{term k}
  11.118 + as there are sets obtained from the former by inserting a fixed element
  11.119 + @{term x} into each.*}
  11.120 +lemma constr_bij:
  11.121 +   "[|finite A; x \<notin> A|] ==>
  11.122 +    card {B. EX C. C <= A & card(C) = k & B = insert x C} =
  11.123 +    card {B. B <= A & card(B) = k}"
  11.124 +  apply (rule_tac f = "%s. s - {x}" and g = "insert x" in card_bij_eq)
  11.125 +       apply (auto elim!: equalityE simp add: inj_on_def)
  11.126 +    apply (subst Diff_insert0, auto)
  11.127 +   txt {* finiteness of the two sets *}
  11.128 +   apply (rule_tac [2] B = "Pow (A)" in finite_subset)
  11.129 +   apply (rule_tac B = "Pow (insert x A)" in finite_subset)
  11.130 +   apply fast+
  11.131 +  done
  11.132 +
  11.133 +text {*
  11.134 +  Main theorem: combinatorial statement about number of subsets of a set.
  11.135 +*}
  11.136 +
  11.137 +lemma n_sub_lemma:
  11.138 +  "!!A. finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
  11.139 +  apply (induct k)
  11.140 +   apply (simp add: card_s_0_eq_empty, atomize)
  11.141 +  apply (rotate_tac -1, erule finite_induct)
  11.142 +   apply (simp_all (no_asm_simp) cong add: conj_cong
  11.143 +     add: card_s_0_eq_empty choose_deconstruct)
  11.144 +  apply (subst card_Un_disjoint)
  11.145 +     prefer 4 apply (force simp add: constr_bij)
  11.146 +    prefer 3 apply force
  11.147 +   prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2]
  11.148 +     finite_subset [of _ "Pow (insert x F)", standard])
  11.149 +  apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset])
  11.150 +  done
  11.151 +
  11.152 +theorem n_subsets:
  11.153 +    "finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
  11.154 +  by (simp add: n_sub_lemma)
  11.155 +
  11.156 +
  11.157 +text{* The binomial theorem (courtesy of Tobias Nipkow): *}
  11.158 +
  11.159 +theorem binomial: "(a+b::nat)^n = (\<Sum>k=0..n. (n choose k) * a^k * b^(n-k))"
  11.160 +proof (induct n)
  11.161 +  case 0 thus ?case by simp
  11.162 +next
  11.163 +  case (Suc n)
  11.164 +  have decomp: "{0..n+1} = {0} \<union> {n+1} \<union> {1..n}"
  11.165 +    by (auto simp add:atLeastAtMost_def atLeast_def atMost_def)
  11.166 +  have decomp2: "{0..n} = {0} \<union> {1..n}"
  11.167 +    by (auto simp add:atLeastAtMost_def atLeast_def atMost_def)
  11.168 +  have "(a+b::nat)^(n+1) = (a+b) * (\<Sum>k=0..n. (n choose k) * a^k * b^(n-k))"
  11.169 +    using Suc by simp
  11.170 +  also have "\<dots> =  a*(\<Sum>k=0..n. (n choose k) * a^k * b^(n-k)) +
  11.171 +                   b*(\<Sum>k=0..n. (n choose k) * a^k * b^(n-k))"
  11.172 +    by(rule nat_distrib)
  11.173 +  also have "\<dots> = (\<Sum>k=0..n. (n choose k) * a^(k+1) * b^(n-k)) +
  11.174 +                  (\<Sum>k=0..n. (n choose k) * a^k * b^(n-k+1))"
  11.175 +    by(simp add: setsum_right_distrib mult_ac)
  11.176 +  also have "\<dots> = (\<Sum>k=0..n. (n choose k) * a^k * b^(n+1-k)) +
  11.177 +                  (\<Sum>k=1..n+1. (n choose (k - 1)) * a^k * b^(n+1-k))"
  11.178 +    by (simp add:setsum_shift_bounds_cl_Suc_ivl Suc_diff_le
  11.179 +             del:setsum_cl_ivl_Suc)
  11.180 +  also have "\<dots> = a^(n+1) + b^(n+1) +
  11.181 +                  (\<Sum>k=1..n. (n choose (k - 1)) * a^k * b^(n+1-k)) +
  11.182 +                  (\<Sum>k=1..n. (n choose k) * a^k * b^(n+1-k))"
  11.183 +    by(simp add: decomp2)
  11.184 +  also have
  11.185 +    "\<dots> = a^(n+1) + b^(n+1) + (\<Sum>k=1..n. (n+1 choose k) * a^k * b^(n+1-k))"
  11.186 +    by(simp add: nat_distrib setsum_addf binomial.simps)
  11.187 +  also have "\<dots> = (\<Sum>k=0..n+1. (n+1 choose k) * a^k * b^(n+1-k))"
  11.188 +    using decomp by simp
  11.189 +  finally show ?case by simp
  11.190 +qed
  11.191 +
  11.192 +end
    12.1 --- a/src/HOL/Library/Commutative_Ring.thy	Wed Nov 08 22:24:54 2006 +0100
    12.2 +++ b/src/HOL/Library/Commutative_Ring.thy	Wed Nov 08 23:11:13 2006 +0100
    12.3 @@ -7,7 +7,7 @@
    12.4  header {* Proving equalities in commutative rings *}
    12.5  
    12.6  theory Commutative_Ring
    12.7 -imports Main
    12.8 +imports Main Parity
    12.9  uses ("comm_ring.ML")
   12.10  begin
   12.11  
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/HOL/Library/GCD.thy	Wed Nov 08 23:11:13 2006 +0100
    13.3 @@ -0,0 +1,206 @@
    13.4 +(*  Title:      HOL/GCD.thy
    13.5 +    ID:         $Id$
    13.6 +    Author:     Christophe Tabacznyj and Lawrence C Paulson
    13.7 +    Copyright   1996  University of Cambridge
    13.8 +*)
    13.9 +
   13.10 +header {* The Greatest Common Divisor *}
   13.11 +
   13.12 +theory GCD
   13.13 +imports Main
   13.14 +begin
   13.15 +
   13.16 +text {*
   13.17 +  See \cite{davenport92}.
   13.18 +  \bigskip
   13.19 +*}
   13.20 +
   13.21 +consts
   13.22 +  gcd  :: "nat \<times> nat => nat"  -- {* Euclid's algorithm *}
   13.23 +
   13.24 +recdef gcd  "measure ((\<lambda>(m, n). n) :: nat \<times> nat => nat)"
   13.25 +  "gcd (m, n) = (if n = 0 then m else gcd (n, m mod n))"
   13.26 +
   13.27 +constdefs
   13.28 +  is_gcd :: "nat => nat => nat => bool"  -- {* @{term gcd} as a relation *}
   13.29 +  "is_gcd p m n == p dvd m \<and> p dvd n \<and>
   13.30 +    (\<forall>d. d dvd m \<and> d dvd n --> d dvd p)"
   13.31 +
   13.32 +
   13.33 +lemma gcd_induct:
   13.34 +  "(!!m. P m 0) ==>
   13.35 +    (!!m n. 0 < n ==> P n (m mod n) ==> P m n)
   13.36 +  ==> P (m::nat) (n::nat)"
   13.37 +  apply (induct m n rule: gcd.induct)
   13.38 +  apply (case_tac "n = 0")
   13.39 +   apply simp_all
   13.40 +  done
   13.41 +
   13.42 +
   13.43 +lemma gcd_0 [simp]: "gcd (m, 0) = m"
   13.44 +  apply simp
   13.45 +  done
   13.46 +
   13.47 +lemma gcd_non_0: "0 < n ==> gcd (m, n) = gcd (n, m mod n)"
   13.48 +  apply simp
   13.49 +  done
   13.50 +
   13.51 +declare gcd.simps [simp del]
   13.52 +
   13.53 +lemma gcd_1 [simp]: "gcd (m, Suc 0) = 1"
   13.54 +  apply (simp add: gcd_non_0)
   13.55 +  done
   13.56 +
   13.57 +text {*
   13.58 +  \medskip @{term "gcd (m, n)"} divides @{text m} and @{text n}.  The
   13.59 +  conjunctions don't seem provable separately.
   13.60 +*}
   13.61 +
   13.62 +lemma gcd_dvd1 [iff]: "gcd (m, n) dvd m"
   13.63 +  and gcd_dvd2 [iff]: "gcd (m, n) dvd n"
   13.64 +  apply (induct m n rule: gcd_induct)
   13.65 +   apply (simp_all add: gcd_non_0)
   13.66 +  apply (blast dest: dvd_mod_imp_dvd)
   13.67 +  done
   13.68 +
   13.69 +text {*
   13.70 +  \medskip Maximality: for all @{term m}, @{term n}, @{term k}
   13.71 +  naturals, if @{term k} divides @{term m} and @{term k} divides
   13.72 +  @{term n} then @{term k} divides @{term "gcd (m, n)"}.
   13.73 +*}
   13.74 +
   13.75 +lemma gcd_greatest: "k dvd m ==> k dvd n ==> k dvd gcd (m, n)"
   13.76 +  apply (induct m n rule: gcd_induct)
   13.77 +   apply (simp_all add: gcd_non_0 dvd_mod)
   13.78 +  done
   13.79 +
   13.80 +lemma gcd_greatest_iff [iff]: "(k dvd gcd (m, n)) = (k dvd m \<and> k dvd n)"
   13.81 +  apply (blast intro!: gcd_greatest intro: dvd_trans)
   13.82 +  done
   13.83 +
   13.84 +lemma gcd_zero: "(gcd (m, n) = 0) = (m = 0 \<and> n = 0)"
   13.85 +  by (simp only: dvd_0_left_iff [THEN sym] gcd_greatest_iff)
   13.86 +
   13.87 +
   13.88 +text {*
   13.89 +  \medskip Function gcd yields the Greatest Common Divisor.
   13.90 +*}
   13.91 +
   13.92 +lemma is_gcd: "is_gcd (gcd (m, n)) m n"
   13.93 +  apply (simp add: is_gcd_def gcd_greatest)
   13.94 +  done
   13.95 +
   13.96 +text {*
   13.97 +  \medskip Uniqueness of GCDs.
   13.98 +*}
   13.99 +
  13.100 +lemma is_gcd_unique: "is_gcd m a b ==> is_gcd n a b ==> m = n"
  13.101 +  apply (simp add: is_gcd_def)
  13.102 +  apply (blast intro: dvd_anti_sym)
  13.103 +  done
  13.104 +
  13.105 +lemma is_gcd_dvd: "is_gcd m a b ==> k dvd a ==> k dvd b ==> k dvd m"
  13.106 +  apply (auto simp add: is_gcd_def)
  13.107 +  done
  13.108 +
  13.109 +
  13.110 +text {*
  13.111 +  \medskip Commutativity
  13.112 +*}
  13.113 +
  13.114 +lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m"
  13.115 +  apply (auto simp add: is_gcd_def)
  13.116 +  done
  13.117 +
  13.118 +lemma gcd_commute: "gcd (m, n) = gcd (n, m)"
  13.119 +  apply (rule is_gcd_unique)
  13.120 +   apply (rule is_gcd)
  13.121 +  apply (subst is_gcd_commute)
  13.122 +  apply (simp add: is_gcd)
  13.123 +  done
  13.124 +
  13.125 +lemma gcd_assoc: "gcd (gcd (k, m), n) = gcd (k, gcd (m, n))"
  13.126 +  apply (rule is_gcd_unique)
  13.127 +   apply (rule is_gcd)
  13.128 +  apply (simp add: is_gcd_def)
  13.129 +  apply (blast intro: dvd_trans)
  13.130 +  done
  13.131 +
  13.132 +lemma gcd_0_left [simp]: "gcd (0, m) = m"
  13.133 +  apply (simp add: gcd_commute [of 0])
  13.134 +  done
  13.135 +
  13.136 +lemma gcd_1_left [simp]: "gcd (Suc 0, m) = 1"
  13.137 +  apply (simp add: gcd_commute [of "Suc 0"])
  13.138 +  done
  13.139 +
  13.140 +
  13.141 +text {*
  13.142 +  \medskip Multiplication laws
  13.143 +*}
  13.144 +
  13.145 +lemma gcd_mult_distrib2: "k * gcd (m, n) = gcd (k * m, k * n)"
  13.146 +    -- {* \cite[page 27]{davenport92} *}
  13.147 +  apply (induct m n rule: gcd_induct)
  13.148 +   apply simp
  13.149 +  apply (case_tac "k = 0")
  13.150 +   apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2)
  13.151 +  done
  13.152 +
  13.153 +lemma gcd_mult [simp]: "gcd (k, k * n) = k"
  13.154 +  apply (rule gcd_mult_distrib2 [of k 1 n, simplified, symmetric])
  13.155 +  done
  13.156 +
  13.157 +lemma gcd_self [simp]: "gcd (k, k) = k"
  13.158 +  apply (rule gcd_mult [of k 1, simplified])
  13.159 +  done
  13.160 +
  13.161 +lemma relprime_dvd_mult: "gcd (k, n) = 1 ==> k dvd m * n ==> k dvd m"
  13.162 +  apply (insert gcd_mult_distrib2 [of m k n])
  13.163 +  apply simp
  13.164 +  apply (erule_tac t = m in ssubst)
  13.165 +  apply simp
  13.166 +  done
  13.167 +
  13.168 +lemma relprime_dvd_mult_iff: "gcd (k, n) = 1 ==> (k dvd m * n) = (k dvd m)"
  13.169 +  apply (blast intro: relprime_dvd_mult dvd_trans)
  13.170 +  done
  13.171 +
  13.172 +lemma gcd_mult_cancel: "gcd (k, n) = 1 ==> gcd (k * m, n) = gcd (m, n)"
  13.173 +  apply (rule dvd_anti_sym)
  13.174 +   apply (rule gcd_greatest)
  13.175 +    apply (rule_tac n = k in relprime_dvd_mult)
  13.176 +     apply (simp add: gcd_assoc)
  13.177 +     apply (simp add: gcd_commute)
  13.178 +    apply (simp_all add: mult_commute)
  13.179 +  apply (blast intro: dvd_trans)
  13.180 +  done
  13.181 +
  13.182 +
  13.183 +text {* \medskip Addition laws *}
  13.184 +
  13.185 +lemma gcd_add1 [simp]: "gcd (m + n, n) = gcd (m, n)"
  13.186 +  apply (case_tac "n = 0")
  13.187 +   apply (simp_all add: gcd_non_0)
  13.188 +  done
  13.189 +
  13.190 +lemma gcd_add2 [simp]: "gcd (m, m + n) = gcd (m, n)"
  13.191 +proof -
  13.192 +  have "gcd (m, m + n) = gcd (m + n, m)" by (rule gcd_commute) 
  13.193 +  also have "... = gcd (n + m, m)" by (simp add: add_commute)
  13.194 +  also have "... = gcd (n, m)" by simp
  13.195 +  also have  "... = gcd (m, n)" by (rule gcd_commute) 
  13.196 +  finally show ?thesis .
  13.197 +qed
  13.198 +
  13.199 +lemma gcd_add2' [simp]: "gcd (m, n + m) = gcd (m, n)"
  13.200 +  apply (subst add_commute)
  13.201 +  apply (rule gcd_add2)
  13.202 +  done
  13.203 +
  13.204 +lemma gcd_add_mult: "gcd (m, k * m + n) = gcd (m, n)"
  13.205 +  apply (induct k)
  13.206 +   apply (simp_all add: add_assoc)
  13.207 +  done
  13.208 +
  13.209 +end
    14.1 --- a/src/HOL/Library/Infinite_Set.thy	Wed Nov 08 22:24:54 2006 +0100
    14.2 +++ b/src/HOL/Library/Infinite_Set.thy	Wed Nov 08 23:11:13 2006 +0100
    14.3 @@ -6,7 +6,7 @@
    14.4  header {* Infinite Sets and Related Concepts *}
    14.5  
    14.6  theory Infinite_Set
    14.7 -imports Hilbert_Choice Binomial
    14.8 +imports Main
    14.9  begin
   14.10  
   14.11  subsection "Infinite Sets"
    15.1 --- a/src/HOL/Library/Library.thy	Wed Nov 08 22:24:54 2006 +0100
    15.2 +++ b/src/HOL/Library/Library.thy	Wed Nov 08 23:11:13 2006 +0100
    15.3 @@ -2,30 +2,33 @@
    15.4  (*<*)
    15.5  theory Library
    15.6  imports
    15.7 +  AssocList
    15.8    BigO
    15.9 +  Binomial
   15.10 +  Char_ord
   15.11 +  Coinductive_List
   15.12 +  Commutative_Ring
   15.13    Continuity
   15.14    EfficientNat
   15.15 +  ExecutableRat
   15.16    ExecutableSet
   15.17 -  ExecutableRat
   15.18 +  FuncSet
   15.19 +  GCD
   15.20 +  Infinite_Set
   15.21    MLString
   15.22 -  FuncSet
   15.23    Multiset
   15.24    NatPair
   15.25    Nat_Infinity
   15.26    Nested_Environment
   15.27    OptionalSugar
   15.28 +  Parity
   15.29    Permutation
   15.30    Primes
   15.31    Quotient
   15.32 +  State_Monad
   15.33    While_Combinator
   15.34    Word
   15.35    Zorn
   15.36 -  Char_ord
   15.37 -  Commutative_Ring
   15.38 -  Coinductive_List
   15.39 -  AssocList
   15.40 -  Infinite_Set
   15.41 -  State_Monad
   15.42  begin
   15.43  end
   15.44  (*>*)
    16.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.2 +++ b/src/HOL/Library/Parity.thy	Wed Nov 08 23:11:13 2006 +0100
    16.3 @@ -0,0 +1,451 @@
    16.4 +(*  Title:      Parity.thy
    16.5 +    ID:         $Id$
    16.6 +    Author:     Jeremy Avigad
    16.7 +*)
    16.8 +
    16.9 +header {* Even and Odd for int and nat *}
   16.10 +
   16.11 +theory Parity
   16.12 +imports Main
   16.13 +begin
   16.14 +
   16.15 +axclass even_odd < type
   16.16 +
   16.17 +consts
   16.18 +  even :: "'a::even_odd => bool"
   16.19 +
   16.20 +instance int :: even_odd ..
   16.21 +instance nat :: even_odd ..
   16.22 +
   16.23 +defs (overloaded)
   16.24 +  even_def: "even (x::int) == x mod 2 = 0"
   16.25 +  even_nat_def: "even (x::nat) == even (int x)"
   16.26 +
   16.27 +abbreviation
   16.28 +  odd :: "'a::even_odd => bool"
   16.29 +  "odd x == \<not> even x"
   16.30 +
   16.31 +
   16.32 +subsection {* Even and odd are mutually exclusive *}
   16.33 +
   16.34 +lemma int_pos_lt_two_imp_zero_or_one: 
   16.35 +    "0 <= x ==> (x::int) < 2 ==> x = 0 | x = 1"
   16.36 +  by auto
   16.37 +
   16.38 +lemma neq_one_mod_two [simp]: "((x::int) mod 2 ~= 0) = (x mod 2 = 1)"
   16.39 +  apply (subgoal_tac "x mod 2 = 0 | x mod 2 = 1", force)
   16.40 +  apply (rule int_pos_lt_two_imp_zero_or_one, auto)
   16.41 +  done
   16.42 +
   16.43 +subsection {* Behavior under integer arithmetic operations *}
   16.44 +
   16.45 +lemma even_times_anything: "even (x::int) ==> even (x * y)"
   16.46 +  by (simp add: even_def zmod_zmult1_eq')
   16.47 +
   16.48 +lemma anything_times_even: "even (y::int) ==> even (x * y)"
   16.49 +  by (simp add: even_def zmod_zmult1_eq)
   16.50 +
   16.51 +lemma odd_times_odd: "odd (x::int) ==> odd y ==> odd (x * y)"
   16.52 +  by (simp add: even_def zmod_zmult1_eq)
   16.53 +
   16.54 +lemma even_product: "even((x::int) * y) = (even x | even y)"
   16.55 +  apply (auto simp add: even_times_anything anything_times_even) 
   16.56 +  apply (rule ccontr)
   16.57 +  apply (auto simp add: odd_times_odd)
   16.58 +  done
   16.59 +
   16.60 +lemma even_plus_even: "even (x::int) ==> even y ==> even (x + y)"
   16.61 +  by (simp add: even_def zmod_zadd1_eq)
   16.62 +
   16.63 +lemma even_plus_odd: "even (x::int) ==> odd y ==> odd (x + y)"
   16.64 +  by (simp add: even_def zmod_zadd1_eq)
   16.65 +
   16.66 +lemma odd_plus_even: "odd (x::int) ==> even y ==> odd (x + y)"
   16.67 +  by (simp add: even_def zmod_zadd1_eq)
   16.68 +
   16.69 +lemma odd_plus_odd: "odd (x::int) ==> odd y ==> even (x + y)"
   16.70 +  by (simp add: even_def zmod_zadd1_eq)
   16.71 +
   16.72 +lemma even_sum: "even ((x::int) + y) = ((even x & even y) | (odd x & odd y))"
   16.73 +  apply (auto intro: even_plus_even odd_plus_odd)
   16.74 +  apply (rule ccontr, simp add: even_plus_odd)
   16.75 +  apply (rule ccontr, simp add: odd_plus_even)
   16.76 +  done
   16.77 +
   16.78 +lemma even_neg: "even (-(x::int)) = even x"
   16.79 +  by (auto simp add: even_def zmod_zminus1_eq_if)
   16.80 +
   16.81 +lemma even_difference: 
   16.82 +  "even ((x::int) - y) = ((even x & even y) | (odd x & odd y))"
   16.83 +  by (simp only: diff_minus even_sum even_neg)
   16.84 +
   16.85 +lemma even_pow_gt_zero [rule_format]: 
   16.86 +    "even (x::int) ==> 0 < n --> even (x^n)"
   16.87 +  apply (induct n)
   16.88 +  apply (auto simp add: even_product)
   16.89 +  done
   16.90 +
   16.91 +lemma odd_pow: "odd x ==> odd((x::int)^n)"
   16.92 +  apply (induct n)
   16.93 +  apply (simp add: even_def)
   16.94 +  apply (simp add: even_product)
   16.95 +  done
   16.96 +
   16.97 +lemma even_power: "even ((x::int)^n) = (even x & 0 < n)"
   16.98 +  apply (auto simp add: even_pow_gt_zero) 
   16.99 +  apply (erule contrapos_pp, erule odd_pow)
  16.100 +  apply (erule contrapos_pp, simp add: even_def)
  16.101 +  done
  16.102 +
  16.103 +lemma even_zero: "even (0::int)"
  16.104 +  by (simp add: even_def)
  16.105 +
  16.106 +lemma odd_one: "odd (1::int)"
  16.107 +  by (simp add: even_def)
  16.108 +
  16.109 +lemmas even_odd_simps [simp] = even_def[of "number_of v",standard] even_zero 
  16.110 +  odd_one even_product even_sum even_neg even_difference even_power
  16.111 +
  16.112 +
  16.113 +subsection {* Equivalent definitions *}
  16.114 +
  16.115 +lemma two_times_even_div_two: "even (x::int) ==> 2 * (x div 2) = x" 
  16.116 +  by (auto simp add: even_def)
  16.117 +
  16.118 +lemma two_times_odd_div_two_plus_one: "odd (x::int) ==> 
  16.119 +    2 * (x div 2) + 1 = x"
  16.120 +  apply (insert zmod_zdiv_equality [of x 2, THEN sym])
  16.121 +  by (simp add: even_def)
  16.122 +
  16.123 +lemma even_equiv_def: "even (x::int) = (EX y. x = 2 * y)"
  16.124 +  apply auto
  16.125 +  apply (rule exI)
  16.126 +  by (erule two_times_even_div_two [THEN sym])
  16.127 +
  16.128 +lemma odd_equiv_def: "odd (x::int) = (EX y. x = 2 * y + 1)"
  16.129 +  apply auto
  16.130 +  apply (rule exI)
  16.131 +  by (erule two_times_odd_div_two_plus_one [THEN sym])
  16.132 +
  16.133 +
  16.134 +subsection {* even and odd for nats *}
  16.135 +
  16.136 +lemma pos_int_even_equiv_nat_even: "0 \<le> x ==> even x = even (nat x)"
  16.137 +  by (simp add: even_nat_def)
  16.138 +
  16.139 +lemma even_nat_product: "even((x::nat) * y) = (even x | even y)"
  16.140 +  by (simp add: even_nat_def int_mult)
  16.141 +
  16.142 +lemma even_nat_sum: "even ((x::nat) + y) = 
  16.143 +    ((even x & even y) | (odd x & odd y))"
  16.144 +  by (unfold even_nat_def, simp)
  16.145 +
  16.146 +lemma even_nat_difference: 
  16.147 +    "even ((x::nat) - y) = (x < y | (even x & even y) | (odd x & odd y))"
  16.148 +  apply (auto simp add: even_nat_def zdiff_int [THEN sym])
  16.149 +  apply (case_tac "x < y", auto simp add: zdiff_int [THEN sym])
  16.150 +  apply (case_tac "x < y", auto simp add: zdiff_int [THEN sym])
  16.151 +  done
  16.152 +
  16.153 +lemma even_nat_Suc: "even (Suc x) = odd x"
  16.154 +  by (simp add: even_nat_def)
  16.155 +
  16.156 +lemma even_nat_power: "even ((x::nat)^y) = (even x & 0 < y)"
  16.157 +  by (simp add: even_nat_def int_power)
  16.158 +
  16.159 +lemma even_nat_zero: "even (0::nat)"
  16.160 +  by (simp add: even_nat_def)
  16.161 +
  16.162 +lemmas even_odd_nat_simps [simp] = even_nat_def[of "number_of v",standard] 
  16.163 +  even_nat_zero even_nat_Suc even_nat_product even_nat_sum even_nat_power
  16.164 +
  16.165 +
  16.166 +subsection {* Equivalent definitions *}
  16.167 +
  16.168 +lemma nat_lt_two_imp_zero_or_one: "(x::nat) < Suc (Suc 0) ==> 
  16.169 +    x = 0 | x = Suc 0"
  16.170 +  by auto
  16.171 +
  16.172 +lemma even_nat_mod_two_eq_zero: "even (x::nat) ==> x mod (Suc (Suc 0)) = 0"
  16.173 +  apply (insert mod_div_equality [of x "Suc (Suc 0)", THEN sym])
  16.174 +  apply (drule subst, assumption)
  16.175 +  apply (subgoal_tac "x mod Suc (Suc 0) = 0 | x mod Suc (Suc 0) = Suc 0")
  16.176 +  apply force
  16.177 +  apply (subgoal_tac "0 < Suc (Suc 0)")
  16.178 +  apply (frule mod_less_divisor [of "Suc (Suc 0)" x])
  16.179 +  apply (erule nat_lt_two_imp_zero_or_one, auto)
  16.180 +  done
  16.181 +
  16.182 +lemma odd_nat_mod_two_eq_one: "odd (x::nat) ==> x mod (Suc (Suc 0)) = Suc 0"
  16.183 +  apply (insert mod_div_equality [of x "Suc (Suc 0)", THEN sym])
  16.184 +  apply (drule subst, assumption)
  16.185 +  apply (subgoal_tac "x mod Suc (Suc 0) = 0 | x mod Suc (Suc 0) = Suc 0")
  16.186 +  apply force 
  16.187 +  apply (subgoal_tac "0 < Suc (Suc 0)")
  16.188 +  apply (frule mod_less_divisor [of "Suc (Suc 0)" x])
  16.189 +  apply (erule nat_lt_two_imp_zero_or_one, auto)
  16.190 +  done
  16.191 +
  16.192 +lemma even_nat_equiv_def: "even (x::nat) = (x mod Suc (Suc 0) = 0)" 
  16.193 +  apply (rule iffI)
  16.194 +  apply (erule even_nat_mod_two_eq_zero)
  16.195 +  apply (insert odd_nat_mod_two_eq_one [of x], auto)
  16.196 +  done
  16.197 +
  16.198 +lemma odd_nat_equiv_def: "odd (x::nat) = (x mod Suc (Suc 0) = Suc 0)"
  16.199 +  apply (auto simp add: even_nat_equiv_def)
  16.200 +  apply (subgoal_tac "x mod (Suc (Suc 0)) < Suc (Suc 0)")
  16.201 +  apply (frule nat_lt_two_imp_zero_or_one, auto)
  16.202 +  done
  16.203 +
  16.204 +lemma even_nat_div_two_times_two: "even (x::nat) ==> 
  16.205 +    Suc (Suc 0) * (x div Suc (Suc 0)) = x"
  16.206 +  apply (insert mod_div_equality [of x "Suc (Suc 0)", THEN sym])
  16.207 +  apply (drule even_nat_mod_two_eq_zero, simp)
  16.208 +  done
  16.209 +
  16.210 +lemma odd_nat_div_two_times_two_plus_one: "odd (x::nat) ==> 
  16.211 +    Suc( Suc (Suc 0) * (x div Suc (Suc 0))) = x"  
  16.212 +  apply (insert mod_div_equality [of x "Suc (Suc 0)", THEN sym])
  16.213 +  apply (drule odd_nat_mod_two_eq_one, simp)
  16.214 +  done
  16.215 +
  16.216 +lemma even_nat_equiv_def2: "even (x::nat) = (EX y. x = Suc (Suc 0) * y)"
  16.217 +  apply (rule iffI, rule exI)
  16.218 +  apply (erule even_nat_div_two_times_two [THEN sym], auto)
  16.219 +  done
  16.220 +
  16.221 +lemma odd_nat_equiv_def2: "odd (x::nat) = (EX y. x = Suc(Suc (Suc 0) * y))"
  16.222 +  apply (rule iffI, rule exI)
  16.223 +  apply (erule odd_nat_div_two_times_two_plus_one [THEN sym], auto)
  16.224 +  done
  16.225 +
  16.226 +subsection {* Parity and powers *}
  16.227 +
  16.228 +lemma minus_one_even_odd_power:
  16.229 +     "(even x --> (- 1::'a::{comm_ring_1,recpower})^x = 1) & 
  16.230 +      (odd x --> (- 1::'a)^x = - 1)"
  16.231 +  apply (induct x)
  16.232 +  apply (rule conjI)
  16.233 +  apply simp
  16.234 +  apply (insert even_nat_zero, blast)
  16.235 +  apply (simp add: power_Suc)
  16.236 +done
  16.237 +
  16.238 +lemma minus_one_even_power [simp]:
  16.239 +     "even x ==> (- 1::'a::{comm_ring_1,recpower})^x = 1"
  16.240 +  by (rule minus_one_even_odd_power [THEN conjunct1, THEN mp], assumption)
  16.241 +
  16.242 +lemma minus_one_odd_power [simp]:
  16.243 +     "odd x ==> (- 1::'a::{comm_ring_1,recpower})^x = - 1"
  16.244 +  by (rule minus_one_even_odd_power [THEN conjunct2, THEN mp], assumption)
  16.245 +
  16.246 +lemma neg_one_even_odd_power:
  16.247 +     "(even x --> (-1::'a::{number_ring,recpower})^x = 1) & 
  16.248 +      (odd x --> (-1::'a)^x = -1)"
  16.249 +  apply (induct x)
  16.250 +  apply (simp, simp add: power_Suc)
  16.251 +  done
  16.252 +
  16.253 +lemma neg_one_even_power [simp]:
  16.254 +     "even x ==> (-1::'a::{number_ring,recpower})^x = 1"
  16.255 +  by (rule neg_one_even_odd_power [THEN conjunct1, THEN mp], assumption)
  16.256 +
  16.257 +lemma neg_one_odd_power [simp]:
  16.258 +     "odd x ==> (-1::'a::{number_ring,recpower})^x = -1"
  16.259 +  by (rule neg_one_even_odd_power [THEN conjunct2, THEN mp], assumption)
  16.260 +
  16.261 +lemma neg_power_if:
  16.262 +     "(-x::'a::{comm_ring_1,recpower}) ^ n = 
  16.263 +      (if even n then (x ^ n) else -(x ^ n))"
  16.264 +  by (induct n, simp_all split: split_if_asm add: power_Suc) 
  16.265 +
  16.266 +lemma zero_le_even_power: "even n ==> 
  16.267 +    0 <= (x::'a::{recpower,ordered_ring_strict}) ^ n"
  16.268 +  apply (simp add: even_nat_equiv_def2)
  16.269 +  apply (erule exE)
  16.270 +  apply (erule ssubst)
  16.271 +  apply (subst power_add)
  16.272 +  apply (rule zero_le_square)
  16.273 +  done
  16.274 +
  16.275 +lemma zero_le_odd_power: "odd n ==> 
  16.276 +    (0 <= (x::'a::{recpower,ordered_idom}) ^ n) = (0 <= x)"
  16.277 +  apply (simp add: odd_nat_equiv_def2)
  16.278 +  apply (erule exE)
  16.279 +  apply (erule ssubst)
  16.280 +  apply (subst power_Suc)
  16.281 +  apply (subst power_add)
  16.282 +  apply (subst zero_le_mult_iff)
  16.283 +  apply auto
  16.284 +  apply (subgoal_tac "x = 0 & 0 < y")
  16.285 +  apply (erule conjE, assumption)
  16.286 +  apply (subst power_eq_0_iff [THEN sym])
  16.287 +  apply (subgoal_tac "0 <= x^y * x^y")
  16.288 +  apply simp
  16.289 +  apply (rule zero_le_square)+
  16.290 +done
  16.291 +
  16.292 +lemma zero_le_power_eq: "(0 <= (x::'a::{recpower,ordered_idom}) ^ n) = 
  16.293 +    (even n | (odd n & 0 <= x))"
  16.294 +  apply auto
  16.295 +  apply (subst zero_le_odd_power [THEN sym])
  16.296 +  apply assumption+
  16.297 +  apply (erule zero_le_even_power)
  16.298 +  apply (subst zero_le_odd_power) 
  16.299 +  apply assumption+
  16.300 +done
  16.301 +
  16.302 +lemma zero_less_power_eq: "(0 < (x::'a::{recpower,ordered_idom}) ^ n) = 
  16.303 +    (n = 0 | (even n & x ~= 0) | (odd n & 0 < x))"
  16.304 +  apply (rule iffI)
  16.305 +  apply clarsimp
  16.306 +  apply (rule conjI)
  16.307 +  apply clarsimp
  16.308 +  apply (rule ccontr)
  16.309 +  apply (subgoal_tac "~ (0 <= x^n)")
  16.310 +  apply simp
  16.311 +  apply (subst zero_le_odd_power)
  16.312 +  apply assumption 
  16.313 +  apply simp
  16.314 +  apply (rule notI)
  16.315 +  apply (simp add: power_0_left)
  16.316 +  apply (rule notI)
  16.317 +  apply (simp add: power_0_left)
  16.318 +  apply auto
  16.319 +  apply (subgoal_tac "0 <= x^n")
  16.320 +  apply (frule order_le_imp_less_or_eq)
  16.321 +  apply simp
  16.322 +  apply (erule zero_le_even_power)
  16.323 +  apply (subgoal_tac "0 <= x^n")
  16.324 +  apply (frule order_le_imp_less_or_eq)
  16.325 +  apply auto
  16.326 +  apply (subst zero_le_odd_power)
  16.327 +  apply assumption
  16.328 +  apply (erule order_less_imp_le)
  16.329 +done
  16.330 +
  16.331 +lemma power_less_zero_eq: "((x::'a::{recpower,ordered_idom}) ^ n < 0) =
  16.332 +    (odd n & x < 0)" 
  16.333 +  apply (subst linorder_not_le [THEN sym])+
  16.334 +  apply (subst zero_le_power_eq)
  16.335 +  apply auto
  16.336 +done
  16.337 +
  16.338 +lemma power_le_zero_eq: "((x::'a::{recpower,ordered_idom}) ^ n <= 0) =
  16.339 +    (n ~= 0 & ((odd n & x <= 0) | (even n & x = 0)))"
  16.340 +  apply (subst linorder_not_less [THEN sym])+
  16.341 +  apply (subst zero_less_power_eq)
  16.342 +  apply auto
  16.343 +done
  16.344 +
  16.345 +lemma power_even_abs: "even n ==> 
  16.346 +    (abs (x::'a::{recpower,ordered_idom}))^n = x^n"
  16.347 +  apply (subst power_abs [THEN sym])
  16.348 +  apply (simp add: zero_le_even_power)
  16.349 +done
  16.350 +
  16.351 +lemma zero_less_power_nat_eq: "(0 < (x::nat) ^ n) = (n = 0 | 0 < x)"
  16.352 +  by (induct n, auto)
  16.353 +
  16.354 +lemma power_minus_even [simp]: "even n ==> 
  16.355 +    (- x)^n = (x^n::'a::{recpower,comm_ring_1})"
  16.356 +  apply (subst power_minus)
  16.357 +  apply simp
  16.358 +done
  16.359 +
  16.360 +lemma power_minus_odd [simp]: "odd n ==> 
  16.361 +    (- x)^n = - (x^n::'a::{recpower,comm_ring_1})"
  16.362 +  apply (subst power_minus)
  16.363 +  apply simp
  16.364 +done
  16.365 +
  16.366 +(* Simplify, when the exponent is a numeral *)
  16.367 +
  16.368 +lemmas power_0_left_number_of = power_0_left [of "number_of w", standard]
  16.369 +declare power_0_left_number_of [simp]
  16.370 +
  16.371 +lemmas zero_le_power_eq_number_of =
  16.372 +    zero_le_power_eq [of _ "number_of w", standard]
  16.373 +declare zero_le_power_eq_number_of [simp]
  16.374 +
  16.375 +lemmas zero_less_power_eq_number_of =
  16.376 +    zero_less_power_eq [of _ "number_of w", standard]
  16.377 +declare zero_less_power_eq_number_of [simp]
  16.378 +
  16.379 +lemmas power_le_zero_eq_number_of =
  16.380 +    power_le_zero_eq [of _ "number_of w", standard]
  16.381 +declare power_le_zero_eq_number_of [simp]
  16.382 +
  16.383 +lemmas power_less_zero_eq_number_of =
  16.384 +    power_less_zero_eq [of _ "number_of w", standard]
  16.385 +declare power_less_zero_eq_number_of [simp]
  16.386 +
  16.387 +lemmas zero_less_power_nat_eq_number_of =
  16.388 +    zero_less_power_nat_eq [of _ "number_of w", standard]
  16.389 +declare zero_less_power_nat_eq_number_of [simp]
  16.390 +
  16.391 +lemmas power_eq_0_iff_number_of = power_eq_0_iff [of _ "number_of w", standard]
  16.392 +declare power_eq_0_iff_number_of [simp]
  16.393 +
  16.394 +lemmas power_even_abs_number_of = power_even_abs [of "number_of w" _, standard]
  16.395 +declare power_even_abs_number_of [simp]
  16.396 +
  16.397 +
  16.398 +subsection {* An Equivalence for @{term [source] "0 \<le> a^n"} *}
  16.399 +
  16.400 +lemma even_power_le_0_imp_0:
  16.401 +     "a ^ (2*k) \<le> (0::'a::{ordered_idom,recpower}) ==> a=0"
  16.402 +apply (induct k) 
  16.403 +apply (auto simp add: zero_le_mult_iff mult_le_0_iff power_Suc)  
  16.404 +done
  16.405 +
  16.406 +lemma zero_le_power_iff:
  16.407 +     "(0 \<le> a^n) = (0 \<le> (a::'a::{ordered_idom,recpower}) | even n)"
  16.408 +      (is "?P n")
  16.409 +proof cases
  16.410 +  assume even: "even n"
  16.411 +  then obtain k where "n = 2*k"
  16.412 +    by (auto simp add: even_nat_equiv_def2 numeral_2_eq_2)
  16.413 +  thus ?thesis by (simp add: zero_le_even_power even) 
  16.414 +next
  16.415 +  assume odd: "odd n"
  16.416 +  then obtain k where "n = Suc(2*k)"
  16.417 +    by (auto simp add: odd_nat_equiv_def2 numeral_2_eq_2)
  16.418 +  thus ?thesis
  16.419 +    by (auto simp add: power_Suc zero_le_mult_iff zero_le_even_power 
  16.420 +             dest!: even_power_le_0_imp_0) 
  16.421 +qed 
  16.422 +
  16.423 +subsection {* Miscellaneous *}
  16.424 +
  16.425 +lemma even_plus_one_div_two: "even (x::int) ==> (x + 1) div 2 = x div 2"
  16.426 +  apply (subst zdiv_zadd1_eq)
  16.427 +  apply (simp add: even_def)
  16.428 +  done
  16.429 +
  16.430 +lemma odd_plus_one_div_two: "odd (x::int) ==> (x + 1) div 2 = x div 2 + 1"
  16.431 +  apply (subst zdiv_zadd1_eq)
  16.432 +  apply (simp add: even_def)
  16.433 +  done
  16.434 +
  16.435 +lemma div_Suc: "Suc a div c = a div c + Suc 0 div c + 
  16.436 +    (a mod c + Suc 0 mod c) div c"
  16.437 +  apply (subgoal_tac "Suc a = a + Suc 0")
  16.438 +  apply (erule ssubst)
  16.439 +  apply (rule div_add1_eq, simp)
  16.440 +  done
  16.441 +
  16.442 +lemma even_nat_plus_one_div_two: "even (x::nat) ==> 
  16.443 +   (Suc x) div Suc (Suc 0) = x div Suc (Suc 0)"
  16.444 +  apply (subst div_Suc)
  16.445 +  apply (simp add: even_nat_equiv_def)
  16.446 +  done
  16.447 +
  16.448 +lemma odd_nat_plus_one_div_two: "odd (x::nat) ==> 
  16.449 +    (Suc x) div Suc (Suc 0) = Suc (x div Suc (Suc 0))"
  16.450 +  apply (subst div_Suc)
  16.451 +  apply (simp add: odd_nat_equiv_def)
  16.452 +  done
  16.453 +
  16.454 +end
    17.1 --- a/src/HOL/Library/Primes.thy	Wed Nov 08 22:24:54 2006 +0100
    17.2 +++ b/src/HOL/Library/Primes.thy	Wed Nov 08 23:11:13 2006 +0100
    17.3 @@ -7,7 +7,7 @@
    17.4  header {* Primality on nat *}
    17.5  
    17.6  theory Primes
    17.7 -imports Main
    17.8 +imports GCD
    17.9  begin
   17.10  
   17.11  definition
    18.1 --- a/src/HOL/PreList.thy	Wed Nov 08 22:24:54 2006 +0100
    18.2 +++ b/src/HOL/PreList.thy	Wed Nov 08 23:11:13 2006 +0100
    18.3 @@ -7,7 +7,7 @@
    18.4  header {* A Basis for Building the Theory of Lists *}
    18.5  
    18.6  theory PreList
    18.7 -imports Wellfounded_Relations Presburger Relation_Power Binomial
    18.8 +imports Wellfounded_Relations Presburger Relation_Power
    18.9  begin
   18.10  
   18.11  text {*
    19.1 --- a/src/HOL/Real/Float.thy	Wed Nov 08 22:24:54 2006 +0100
    19.2 +++ b/src/HOL/Real/Float.thy	Wed Nov 08 23:11:13 2006 +0100
    19.3 @@ -6,7 +6,7 @@
    19.4  header {* Floating Point Representation of the Reals *}
    19.5  
    19.6  theory Float
    19.7 -imports Real
    19.8 +imports Real Parity
    19.9  uses ("float.ML")
   19.10  begin
   19.11  
    20.1 --- a/src/HOL/ex/NatSum.thy	Wed Nov 08 22:24:54 2006 +0100
    20.2 +++ b/src/HOL/ex/NatSum.thy	Wed Nov 08 23:11:13 2006 +0100
    20.3 @@ -5,7 +5,7 @@
    20.4  
    20.5  header {* Summing natural numbers *}
    20.6  
    20.7 -theory NatSum imports Main begin
    20.8 +theory NatSum imports Main Parity begin
    20.9  
   20.10  text {*
   20.11    Summing natural numbers, squares, cubes, etc.
    21.1 --- a/src/HOL/ex/ROOT.ML	Wed Nov 08 22:24:54 2006 +0100
    21.2 +++ b/src/HOL/ex/ROOT.ML	Wed Nov 08 23:11:13 2006 +0100
    21.3 @@ -4,6 +4,9 @@
    21.4  Miscellaneous examples for Higher-Order Logic.
    21.5  *)
    21.6  
    21.7 +no_document use_thy "Parity";
    21.8 +no_document use_thy "GCD";
    21.9 +
   21.10  no_document time_use_thy "Classpackage";
   21.11  no_document time_use_thy "Codegenerator";
   21.12  no_document time_use_thy "CodeCollections";
    22.1 --- a/src/HOL/ex/Reflected_Presburger.thy	Wed Nov 08 22:24:54 2006 +0100
    22.2 +++ b/src/HOL/ex/Reflected_Presburger.thy	Wed Nov 08 23:11:13 2006 +0100
    22.3 @@ -9,7 +9,7 @@
    22.4  header {* Quantifier elimination for Presburger arithmetic *}
    22.5  
    22.6  theory Reflected_Presburger
    22.7 -imports Main
    22.8 +imports Main GCD
    22.9  begin
   22.10  
   22.11  (* Shadow syntax for integer terms *)