# HG changeset patch # User wenzelm # Date 1163023873 -3600 # Node ID 47195501ecf7054b2a7278d8608610d81443c3aa # Parent 617fdb08abe94bc7057de2b756fcbbb7ec4d1683 moved theories Parity, GCD, Binomial to Library; diff -r 617fdb08abe9 -r 47195501ecf7 NEWS --- a/NEWS Wed Nov 08 22:24:54 2006 +0100 +++ b/NEWS Wed Nov 08 23:11:13 2006 +0100 @@ -615,9 +615,9 @@ * inductive and datatype: provide projections of mutual rules, bundled as foo_bar.inducts; -* Library: theory Infinite_Set has been moved to the library. - -* Library: theory Accessible_Part has been move to main HOL. +* Library: moved theories Parity, GCD, Binomial, Infinite_Set to Library. + +* Library: moved theory Accessible_Part to main HOL. * Library: added theory Coinductive_List of potentially infinite lists as greatest fixed-point. diff -r 617fdb08abe9 -r 47195501ecf7 src/HOL/Algebra/Exponent.thy --- a/src/HOL/Algebra/Exponent.thy Wed Nov 08 22:24:54 2006 +0100 +++ b/src/HOL/Algebra/Exponent.thy Wed Nov 08 23:11:13 2006 +0100 @@ -5,7 +5,7 @@ exponent p s yields the greatest power of p that divides s. *) -theory Exponent imports Main Primes begin +theory Exponent imports Main Primes Binomial begin section {*The Combinatorial Argument Underlying the First Sylow Theorem*} diff -r 617fdb08abe9 -r 47195501ecf7 src/HOL/Algebra/ROOT.ML --- a/src/HOL/Algebra/ROOT.ML Wed Nov 08 22:24:54 2006 +0100 +++ b/src/HOL/Algebra/ROOT.ML Wed Nov 08 23:11:13 2006 +0100 @@ -10,6 +10,8 @@ no_document use_thy "FuncSet"; no_document use_thy "Primes"; +no_document use_thy "Binomial"; + (* Groups *) diff -r 617fdb08abe9 -r 47195501ecf7 src/HOL/Binomial.thy --- a/src/HOL/Binomial.thy Wed Nov 08 22:24:54 2006 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,189 +0,0 @@ -(* Title: HOL/Binomial.thy - ID: $Id$ - Author: Lawrence C Paulson - Copyright 1997 University of Cambridge -*) - -header{*Binomial Coefficients*} - -theory Binomial -imports GCD -begin - -text{*This development is based on the work of Andy Gordon and -Florian Kammueller*} - -consts - binomial :: "nat \ nat \ nat" (infixl "choose" 65) - -primrec - binomial_0: "(0 choose k) = (if k = 0 then 1 else 0)" - - binomial_Suc: "(Suc n choose k) = - (if k = 0 then 1 else (n choose (k - 1)) + (n choose k))" - -lemma binomial_n_0 [simp]: "(n choose 0) = 1" -by (cases n) simp_all - -lemma binomial_0_Suc [simp]: "(0 choose Suc k) = 0" -by simp - -lemma binomial_Suc_Suc [simp]: - "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)" -by simp - -lemma binomial_eq_0 [rule_format]: "\k. n < k --> (n choose k) = 0" -apply (induct "n") -apply auto -done - -declare binomial_0 [simp del] binomial_Suc [simp del] - -lemma binomial_n_n [simp]: "(n choose n) = 1" -apply (induct "n") -apply (simp_all add: binomial_eq_0) -done - -lemma binomial_Suc_n [simp]: "(Suc n choose n) = Suc n" -by (induct "n", simp_all) - -lemma binomial_1 [simp]: "(n choose Suc 0) = n" -by (induct "n", simp_all) - -lemma zero_less_binomial [rule_format]: "k \ n --> 0 < (n choose k)" -by (rule_tac m = n and n = k in diff_induct, simp_all) - -lemma binomial_eq_0_iff: "(n choose k = 0) = (nn)" -by (simp add: linorder_not_less [symmetric] binomial_eq_0_iff [symmetric]) - -(*Might be more useful if re-oriented*) -lemma Suc_times_binomial_eq [rule_format]: - "\k. k \ n --> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k" -apply (induct "n") -apply (simp add: binomial_0, clarify) -apply (case_tac "k") -apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq - binomial_eq_0) -done - -text{*This is the well-known version, but it's harder to use because of the - need to reason about division.*} -lemma binomial_Suc_Suc_eq_times: - "k \ n ==> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k" -by (simp add: Suc_times_binomial_eq div_mult_self_is_m zero_less_Suc - del: mult_Suc mult_Suc_right) - -text{*Another version, with -1 instead of Suc.*} -lemma times_binomial_minus1_eq: - "[|k \ n; 0 (n choose k) * k = n * ((n - 1) choose (k - 1))" -apply (cut_tac n = "n - 1" and k = "k - 1" in Suc_times_binomial_eq) -apply (simp split add: nat_diff_split, auto) -done - -subsubsection {* Theorems about @{text "choose"} *} - -text {* - \medskip Basic theorem about @{text "choose"}. By Florian - Kamm\"uller, tidied by LCP. -*} - -lemma card_s_0_eq_empty: - "finite A ==> card {B. B \ A & card B = 0} = 1" - apply (simp cong add: conj_cong add: finite_subset [THEN card_0_eq]) - apply (simp cong add: rev_conj_cong) - done - -lemma choose_deconstruct: "finite M ==> x \ M - ==> {s. s <= insert x M & card(s) = Suc k} - = {s. s <= M & card(s) = Suc k} Un - {s. EX t. t <= M & card(t) = k & s = insert x t}" - apply safe - apply (auto intro: finite_subset [THEN card_insert_disjoint]) - apply (drule_tac x = "xa - {x}" in spec) - apply (subgoal_tac "x \ xa", auto) - apply (erule rev_mp, subst card_Diff_singleton) - apply (auto intro: finite_subset) - done - -text{*There are as many subsets of @{term A} having cardinality @{term k} - as there are sets obtained from the former by inserting a fixed element - @{term x} into each.*} -lemma constr_bij: - "[|finite A; x \ A|] ==> - card {B. EX C. C <= A & card(C) = k & B = insert x C} = - card {B. B <= A & card(B) = k}" - apply (rule_tac f = "%s. s - {x}" and g = "insert x" in card_bij_eq) - apply (auto elim!: equalityE simp add: inj_on_def) - apply (subst Diff_insert0, auto) - txt {* finiteness of the two sets *} - apply (rule_tac [2] B = "Pow (A)" in finite_subset) - apply (rule_tac B = "Pow (insert x A)" in finite_subset) - apply fast+ - done - -text {* - Main theorem: combinatorial statement about number of subsets of a set. -*} - -lemma n_sub_lemma: - "!!A. finite A ==> card {B. B <= A & card B = k} = (card A choose k)" - apply (induct k) - apply (simp add: card_s_0_eq_empty, atomize) - apply (rotate_tac -1, erule finite_induct) - apply (simp_all (no_asm_simp) cong add: conj_cong - add: card_s_0_eq_empty choose_deconstruct) - apply (subst card_Un_disjoint) - prefer 4 apply (force simp add: constr_bij) - prefer 3 apply force - prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2] - finite_subset [of _ "Pow (insert x F)", standard]) - apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset]) - done - -theorem n_subsets: - "finite A ==> card {B. B <= A & card B = k} = (card A choose k)" - by (simp add: n_sub_lemma) - - -text{* The binomial theorem (courtesy of Tobias Nipkow): *} - -theorem binomial: "(a+b::nat)^n = (\k=0..n. (n choose k) * a^k * b^(n-k))" -proof (induct n) - case 0 thus ?case by simp -next - case (Suc n) - have decomp: "{0..n+1} = {0} \ {n+1} \ {1..n}" - by (auto simp add:atLeastAtMost_def atLeast_def atMost_def) - have decomp2: "{0..n} = {0} \ {1..n}" - by (auto simp add:atLeastAtMost_def atLeast_def atMost_def) - have "(a+b::nat)^(n+1) = (a+b) * (\k=0..n. (n choose k) * a^k * b^(n-k))" - using Suc by simp - also have "\ = a*(\k=0..n. (n choose k) * a^k * b^(n-k)) + - b*(\k=0..n. (n choose k) * a^k * b^(n-k))" - by(rule nat_distrib) - also have "\ = (\k=0..n. (n choose k) * a^(k+1) * b^(n-k)) + - (\k=0..n. (n choose k) * a^k * b^(n-k+1))" - by(simp add: setsum_right_distrib mult_ac) - also have "\ = (\k=0..n. (n choose k) * a^k * b^(n+1-k)) + - (\k=1..n+1. (n choose (k - 1)) * a^k * b^(n+1-k))" - by (simp add:setsum_shift_bounds_cl_Suc_ivl Suc_diff_le - del:setsum_cl_ivl_Suc) - also have "\ = a^(n+1) + b^(n+1) + - (\k=1..n. (n choose (k - 1)) * a^k * b^(n+1-k)) + - (\k=1..n. (n choose k) * a^k * b^(n+1-k))" - by(simp add: decomp2) - also have - "\ = a^(n+1) + b^(n+1) + (\k=1..n. (n+1 choose k) * a^k * b^(n+1-k))" - by(simp add: nat_distrib setsum_addf binomial.simps) - also have "\ = (\k=0..n+1. (n+1 choose k) * a^k * b^(n+1-k))" - using decomp by simp - finally show ?case by simp -qed - -end diff -r 617fdb08abe9 -r 47195501ecf7 src/HOL/Complex/ROOT.ML --- a/src/HOL/Complex/ROOT.ML Wed Nov 08 22:24:54 2006 +0100 +++ b/src/HOL/Complex/ROOT.ML Wed Nov 08 23:11:13 2006 +0100 @@ -6,6 +6,8 @@ *) no_document use_thy "Infinite_Set"; -with_path "../Real" use_thy "Float"; +no_document use_thy "Parity"; + +with_path "../Real" use_thy "Float"; with_path "../Hyperreal" use_thy "Hyperreal"; time_use_thy "Complex_Main"; diff -r 617fdb08abe9 -r 47195501ecf7 src/HOL/GCD.thy --- a/src/HOL/GCD.thy Wed Nov 08 22:24:54 2006 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,210 +0,0 @@ -(* Title: HOL/GCD.thy - ID: $Id$ - Author: Christophe Tabacznyj and Lawrence C Paulson - Copyright 1996 University of Cambridge - -Builds on Integ/Parity mainly because that contains recdef, which we -need, but also because we may want to include gcd on integers in here -as well in the future. -*) - -header {* The Greatest Common Divisor *} - -theory GCD -imports Parity -begin - -text {* - See \cite{davenport92}. - \bigskip -*} - -consts - gcd :: "nat \ nat => nat" -- {* Euclid's algorithm *} - -recdef gcd "measure ((\(m, n). n) :: nat \ nat => nat)" - "gcd (m, n) = (if n = 0 then m else gcd (n, m mod n))" - -constdefs - is_gcd :: "nat => nat => nat => bool" -- {* @{term gcd} as a relation *} - "is_gcd p m n == p dvd m \ p dvd n \ - (\d. d dvd m \ d dvd n --> d dvd p)" - - -lemma gcd_induct: - "(!!m. P m 0) ==> - (!!m n. 0 < n ==> P n (m mod n) ==> P m n) - ==> P (m::nat) (n::nat)" - apply (induct m n rule: gcd.induct) - apply (case_tac "n = 0") - apply simp_all - done - - -lemma gcd_0 [simp]: "gcd (m, 0) = m" - apply simp - done - -lemma gcd_non_0: "0 < n ==> gcd (m, n) = gcd (n, m mod n)" - apply simp - done - -declare gcd.simps [simp del] - -lemma gcd_1 [simp]: "gcd (m, Suc 0) = 1" - apply (simp add: gcd_non_0) - done - -text {* - \medskip @{term "gcd (m, n)"} divides @{text m} and @{text n}. The - conjunctions don't seem provable separately. -*} - -lemma gcd_dvd1 [iff]: "gcd (m, n) dvd m" - and gcd_dvd2 [iff]: "gcd (m, n) dvd n" - apply (induct m n rule: gcd_induct) - apply (simp_all add: gcd_non_0) - apply (blast dest: dvd_mod_imp_dvd) - done - -text {* - \medskip Maximality: for all @{term m}, @{term n}, @{term k} - naturals, if @{term k} divides @{term m} and @{term k} divides - @{term n} then @{term k} divides @{term "gcd (m, n)"}. -*} - -lemma gcd_greatest: "k dvd m ==> k dvd n ==> k dvd gcd (m, n)" - apply (induct m n rule: gcd_induct) - apply (simp_all add: gcd_non_0 dvd_mod) - done - -lemma gcd_greatest_iff [iff]: "(k dvd gcd (m, n)) = (k dvd m \ k dvd n)" - apply (blast intro!: gcd_greatest intro: dvd_trans) - done - -lemma gcd_zero: "(gcd (m, n) = 0) = (m = 0 \ n = 0)" - by (simp only: dvd_0_left_iff [THEN sym] gcd_greatest_iff) - - -text {* - \medskip Function gcd yields the Greatest Common Divisor. -*} - -lemma is_gcd: "is_gcd (gcd (m, n)) m n" - apply (simp add: is_gcd_def gcd_greatest) - done - -text {* - \medskip Uniqueness of GCDs. -*} - -lemma is_gcd_unique: "is_gcd m a b ==> is_gcd n a b ==> m = n" - apply (simp add: is_gcd_def) - apply (blast intro: dvd_anti_sym) - done - -lemma is_gcd_dvd: "is_gcd m a b ==> k dvd a ==> k dvd b ==> k dvd m" - apply (auto simp add: is_gcd_def) - done - - -text {* - \medskip Commutativity -*} - -lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m" - apply (auto simp add: is_gcd_def) - done - -lemma gcd_commute: "gcd (m, n) = gcd (n, m)" - apply (rule is_gcd_unique) - apply (rule is_gcd) - apply (subst is_gcd_commute) - apply (simp add: is_gcd) - done - -lemma gcd_assoc: "gcd (gcd (k, m), n) = gcd (k, gcd (m, n))" - apply (rule is_gcd_unique) - apply (rule is_gcd) - apply (simp add: is_gcd_def) - apply (blast intro: dvd_trans) - done - -lemma gcd_0_left [simp]: "gcd (0, m) = m" - apply (simp add: gcd_commute [of 0]) - done - -lemma gcd_1_left [simp]: "gcd (Suc 0, m) = 1" - apply (simp add: gcd_commute [of "Suc 0"]) - done - - -text {* - \medskip Multiplication laws -*} - -lemma gcd_mult_distrib2: "k * gcd (m, n) = gcd (k * m, k * n)" - -- {* \cite[page 27]{davenport92} *} - apply (induct m n rule: gcd_induct) - apply simp - apply (case_tac "k = 0") - apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2) - done - -lemma gcd_mult [simp]: "gcd (k, k * n) = k" - apply (rule gcd_mult_distrib2 [of k 1 n, simplified, symmetric]) - done - -lemma gcd_self [simp]: "gcd (k, k) = k" - apply (rule gcd_mult [of k 1, simplified]) - done - -lemma relprime_dvd_mult: "gcd (k, n) = 1 ==> k dvd m * n ==> k dvd m" - apply (insert gcd_mult_distrib2 [of m k n]) - apply simp - apply (erule_tac t = m in ssubst) - apply simp - done - -lemma relprime_dvd_mult_iff: "gcd (k, n) = 1 ==> (k dvd m * n) = (k dvd m)" - apply (blast intro: relprime_dvd_mult dvd_trans) - done - -lemma gcd_mult_cancel: "gcd (k, n) = 1 ==> gcd (k * m, n) = gcd (m, n)" - apply (rule dvd_anti_sym) - apply (rule gcd_greatest) - apply (rule_tac n = k in relprime_dvd_mult) - apply (simp add: gcd_assoc) - apply (simp add: gcd_commute) - apply (simp_all add: mult_commute) - apply (blast intro: dvd_trans) - done - - -text {* \medskip Addition laws *} - -lemma gcd_add1 [simp]: "gcd (m + n, n) = gcd (m, n)" - apply (case_tac "n = 0") - apply (simp_all add: gcd_non_0) - done - -lemma gcd_add2 [simp]: "gcd (m, m + n) = gcd (m, n)" -proof - - have "gcd (m, m + n) = gcd (m + n, m)" by (rule gcd_commute) - also have "... = gcd (n + m, m)" by (simp add: add_commute) - also have "... = gcd (n, m)" by simp - also have "... = gcd (m, n)" by (rule gcd_commute) - finally show ?thesis . -qed - -lemma gcd_add2' [simp]: "gcd (m, n + m) = gcd (m, n)" - apply (subst add_commute) - apply (rule gcd_add2) - done - -lemma gcd_add_mult: "gcd (m, k * m + n) = gcd (m, n)" - apply (induct k) - apply (simp_all add: add_assoc) - done - -end diff -r 617fdb08abe9 -r 47195501ecf7 src/HOL/Hyperreal/HyperPow.thy --- a/src/HOL/Hyperreal/HyperPow.thy Wed Nov 08 22:24:54 2006 +0100 +++ b/src/HOL/Hyperreal/HyperPow.thy Wed Nov 08 23:11:13 2006 +0100 @@ -7,7 +7,7 @@ header{*Exponentials on the Hyperreals*} theory HyperPow -imports HyperArith HyperNat +imports HyperArith HyperNat Parity begin (* consts hpowr :: "[hypreal,nat] => hypreal" *) diff -r 617fdb08abe9 -r 47195501ecf7 src/HOL/Import/HOL/ROOT.ML --- a/src/HOL/Import/HOL/ROOT.ML Wed Nov 08 22:24:54 2006 +0100 +++ b/src/HOL/Import/HOL/ROOT.ML Wed Nov 08 23:11:13 2006 +0100 @@ -3,5 +3,6 @@ Author: Sebastian Skalberg (TU Muenchen) *) +use_thy "Primes"; setmp quick_and_dirty true use_thy "HOL4Prob"; setmp quick_and_dirty true use_thy "HOL4"; diff -r 617fdb08abe9 -r 47195501ecf7 src/HOL/Integ/Parity.thy --- a/src/HOL/Integ/Parity.thy Wed Nov 08 22:24:54 2006 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,451 +0,0 @@ -(* Title: Parity.thy - ID: $Id$ - Author: Jeremy Avigad -*) - -header {* Even and Odd for ints and nats*} - -theory Parity -imports Divides IntDiv NatSimprocs -begin - -axclass even_odd < type - -consts - even :: "'a::even_odd => bool" - -instance int :: even_odd .. -instance nat :: even_odd .. - -defs (overloaded) - even_def: "even (x::int) == x mod 2 = 0" - even_nat_def: "even (x::nat) == even (int x)" - -abbreviation - odd :: "'a::even_odd => bool" - "odd x == \ even x" - - -subsection {* Even and odd are mutually exclusive *} - -lemma int_pos_lt_two_imp_zero_or_one: - "0 <= x ==> (x::int) < 2 ==> x = 0 | x = 1" - by auto - -lemma neq_one_mod_two [simp]: "((x::int) mod 2 ~= 0) = (x mod 2 = 1)" - apply (subgoal_tac "x mod 2 = 0 | x mod 2 = 1", force) - apply (rule int_pos_lt_two_imp_zero_or_one, auto) - done - -subsection {* Behavior under integer arithmetic operations *} - -lemma even_times_anything: "even (x::int) ==> even (x * y)" - by (simp add: even_def zmod_zmult1_eq') - -lemma anything_times_even: "even (y::int) ==> even (x * y)" - by (simp add: even_def zmod_zmult1_eq) - -lemma odd_times_odd: "odd (x::int) ==> odd y ==> odd (x * y)" - by (simp add: even_def zmod_zmult1_eq) - -lemma even_product: "even((x::int) * y) = (even x | even y)" - apply (auto simp add: even_times_anything anything_times_even) - apply (rule ccontr) - apply (auto simp add: odd_times_odd) - done - -lemma even_plus_even: "even (x::int) ==> even y ==> even (x + y)" - by (simp add: even_def zmod_zadd1_eq) - -lemma even_plus_odd: "even (x::int) ==> odd y ==> odd (x + y)" - by (simp add: even_def zmod_zadd1_eq) - -lemma odd_plus_even: "odd (x::int) ==> even y ==> odd (x + y)" - by (simp add: even_def zmod_zadd1_eq) - -lemma odd_plus_odd: "odd (x::int) ==> odd y ==> even (x + y)" - by (simp add: even_def zmod_zadd1_eq) - -lemma even_sum: "even ((x::int) + y) = ((even x & even y) | (odd x & odd y))" - apply (auto intro: even_plus_even odd_plus_odd) - apply (rule ccontr, simp add: even_plus_odd) - apply (rule ccontr, simp add: odd_plus_even) - done - -lemma even_neg: "even (-(x::int)) = even x" - by (auto simp add: even_def zmod_zminus1_eq_if) - -lemma even_difference: - "even ((x::int) - y) = ((even x & even y) | (odd x & odd y))" - by (simp only: diff_minus even_sum even_neg) - -lemma even_pow_gt_zero [rule_format]: - "even (x::int) ==> 0 < n --> even (x^n)" - apply (induct n) - apply (auto simp add: even_product) - done - -lemma odd_pow: "odd x ==> odd((x::int)^n)" - apply (induct n) - apply (simp add: even_def) - apply (simp add: even_product) - done - -lemma even_power: "even ((x::int)^n) = (even x & 0 < n)" - apply (auto simp add: even_pow_gt_zero) - apply (erule contrapos_pp, erule odd_pow) - apply (erule contrapos_pp, simp add: even_def) - done - -lemma even_zero: "even (0::int)" - by (simp add: even_def) - -lemma odd_one: "odd (1::int)" - by (simp add: even_def) - -lemmas even_odd_simps [simp] = even_def[of "number_of v",standard] even_zero - odd_one even_product even_sum even_neg even_difference even_power - - -subsection {* Equivalent definitions *} - -lemma two_times_even_div_two: "even (x::int) ==> 2 * (x div 2) = x" - by (auto simp add: even_def) - -lemma two_times_odd_div_two_plus_one: "odd (x::int) ==> - 2 * (x div 2) + 1 = x" - apply (insert zmod_zdiv_equality [of x 2, THEN sym]) - by (simp add: even_def) - -lemma even_equiv_def: "even (x::int) = (EX y. x = 2 * y)" - apply auto - apply (rule exI) - by (erule two_times_even_div_two [THEN sym]) - -lemma odd_equiv_def: "odd (x::int) = (EX y. x = 2 * y + 1)" - apply auto - apply (rule exI) - by (erule two_times_odd_div_two_plus_one [THEN sym]) - - -subsection {* even and odd for nats *} - -lemma pos_int_even_equiv_nat_even: "0 \ x ==> even x = even (nat x)" - by (simp add: even_nat_def) - -lemma even_nat_product: "even((x::nat) * y) = (even x | even y)" - by (simp add: even_nat_def int_mult) - -lemma even_nat_sum: "even ((x::nat) + y) = - ((even x & even y) | (odd x & odd y))" - by (unfold even_nat_def, simp) - -lemma even_nat_difference: - "even ((x::nat) - y) = (x < y | (even x & even y) | (odd x & odd y))" - apply (auto simp add: even_nat_def zdiff_int [THEN sym]) - apply (case_tac "x < y", auto simp add: zdiff_int [THEN sym]) - apply (case_tac "x < y", auto simp add: zdiff_int [THEN sym]) - done - -lemma even_nat_Suc: "even (Suc x) = odd x" - by (simp add: even_nat_def) - -lemma even_nat_power: "even ((x::nat)^y) = (even x & 0 < y)" - by (simp add: even_nat_def int_power) - -lemma even_nat_zero: "even (0::nat)" - by (simp add: even_nat_def) - -lemmas even_odd_nat_simps [simp] = even_nat_def[of "number_of v",standard] - even_nat_zero even_nat_Suc even_nat_product even_nat_sum even_nat_power - - -subsection {* Equivalent definitions *} - -lemma nat_lt_two_imp_zero_or_one: "(x::nat) < Suc (Suc 0) ==> - x = 0 | x = Suc 0" - by auto - -lemma even_nat_mod_two_eq_zero: "even (x::nat) ==> x mod (Suc (Suc 0)) = 0" - apply (insert mod_div_equality [of x "Suc (Suc 0)", THEN sym]) - apply (drule subst, assumption) - apply (subgoal_tac "x mod Suc (Suc 0) = 0 | x mod Suc (Suc 0) = Suc 0") - apply force - apply (subgoal_tac "0 < Suc (Suc 0)") - apply (frule mod_less_divisor [of "Suc (Suc 0)" x]) - apply (erule nat_lt_two_imp_zero_or_one, auto) - done - -lemma odd_nat_mod_two_eq_one: "odd (x::nat) ==> x mod (Suc (Suc 0)) = Suc 0" - apply (insert mod_div_equality [of x "Suc (Suc 0)", THEN sym]) - apply (drule subst, assumption) - apply (subgoal_tac "x mod Suc (Suc 0) = 0 | x mod Suc (Suc 0) = Suc 0") - apply force - apply (subgoal_tac "0 < Suc (Suc 0)") - apply (frule mod_less_divisor [of "Suc (Suc 0)" x]) - apply (erule nat_lt_two_imp_zero_or_one, auto) - done - -lemma even_nat_equiv_def: "even (x::nat) = (x mod Suc (Suc 0) = 0)" - apply (rule iffI) - apply (erule even_nat_mod_two_eq_zero) - apply (insert odd_nat_mod_two_eq_one [of x], auto) - done - -lemma odd_nat_equiv_def: "odd (x::nat) = (x mod Suc (Suc 0) = Suc 0)" - apply (auto simp add: even_nat_equiv_def) - apply (subgoal_tac "x mod (Suc (Suc 0)) < Suc (Suc 0)") - apply (frule nat_lt_two_imp_zero_or_one, auto) - done - -lemma even_nat_div_two_times_two: "even (x::nat) ==> - Suc (Suc 0) * (x div Suc (Suc 0)) = x" - apply (insert mod_div_equality [of x "Suc (Suc 0)", THEN sym]) - apply (drule even_nat_mod_two_eq_zero, simp) - done - -lemma odd_nat_div_two_times_two_plus_one: "odd (x::nat) ==> - Suc( Suc (Suc 0) * (x div Suc (Suc 0))) = x" - apply (insert mod_div_equality [of x "Suc (Suc 0)", THEN sym]) - apply (drule odd_nat_mod_two_eq_one, simp) - done - -lemma even_nat_equiv_def2: "even (x::nat) = (EX y. x = Suc (Suc 0) * y)" - apply (rule iffI, rule exI) - apply (erule even_nat_div_two_times_two [THEN sym], auto) - done - -lemma odd_nat_equiv_def2: "odd (x::nat) = (EX y. x = Suc(Suc (Suc 0) * y))" - apply (rule iffI, rule exI) - apply (erule odd_nat_div_two_times_two_plus_one [THEN sym], auto) - done - -subsection {* Parity and powers *} - -lemma minus_one_even_odd_power: - "(even x --> (- 1::'a::{comm_ring_1,recpower})^x = 1) & - (odd x --> (- 1::'a)^x = - 1)" - apply (induct x) - apply (rule conjI) - apply simp - apply (insert even_nat_zero, blast) - apply (simp add: power_Suc) -done - -lemma minus_one_even_power [simp]: - "even x ==> (- 1::'a::{comm_ring_1,recpower})^x = 1" - by (rule minus_one_even_odd_power [THEN conjunct1, THEN mp], assumption) - -lemma minus_one_odd_power [simp]: - "odd x ==> (- 1::'a::{comm_ring_1,recpower})^x = - 1" - by (rule minus_one_even_odd_power [THEN conjunct2, THEN mp], assumption) - -lemma neg_one_even_odd_power: - "(even x --> (-1::'a::{number_ring,recpower})^x = 1) & - (odd x --> (-1::'a)^x = -1)" - apply (induct x) - apply (simp, simp add: power_Suc) - done - -lemma neg_one_even_power [simp]: - "even x ==> (-1::'a::{number_ring,recpower})^x = 1" - by (rule neg_one_even_odd_power [THEN conjunct1, THEN mp], assumption) - -lemma neg_one_odd_power [simp]: - "odd x ==> (-1::'a::{number_ring,recpower})^x = -1" - by (rule neg_one_even_odd_power [THEN conjunct2, THEN mp], assumption) - -lemma neg_power_if: - "(-x::'a::{comm_ring_1,recpower}) ^ n = - (if even n then (x ^ n) else -(x ^ n))" - by (induct n, simp_all split: split_if_asm add: power_Suc) - -lemma zero_le_even_power: "even n ==> - 0 <= (x::'a::{recpower,ordered_ring_strict}) ^ n" - apply (simp add: even_nat_equiv_def2) - apply (erule exE) - apply (erule ssubst) - apply (subst power_add) - apply (rule zero_le_square) - done - -lemma zero_le_odd_power: "odd n ==> - (0 <= (x::'a::{recpower,ordered_idom}) ^ n) = (0 <= x)" - apply (simp add: odd_nat_equiv_def2) - apply (erule exE) - apply (erule ssubst) - apply (subst power_Suc) - apply (subst power_add) - apply (subst zero_le_mult_iff) - apply auto - apply (subgoal_tac "x = 0 & 0 < y") - apply (erule conjE, assumption) - apply (subst power_eq_0_iff [THEN sym]) - apply (subgoal_tac "0 <= x^y * x^y") - apply simp - apply (rule zero_le_square)+ -done - -lemma zero_le_power_eq: "(0 <= (x::'a::{recpower,ordered_idom}) ^ n) = - (even n | (odd n & 0 <= x))" - apply auto - apply (subst zero_le_odd_power [THEN sym]) - apply assumption+ - apply (erule zero_le_even_power) - apply (subst zero_le_odd_power) - apply assumption+ -done - -lemma zero_less_power_eq: "(0 < (x::'a::{recpower,ordered_idom}) ^ n) = - (n = 0 | (even n & x ~= 0) | (odd n & 0 < x))" - apply (rule iffI) - apply clarsimp - apply (rule conjI) - apply clarsimp - apply (rule ccontr) - apply (subgoal_tac "~ (0 <= x^n)") - apply simp - apply (subst zero_le_odd_power) - apply assumption - apply simp - apply (rule notI) - apply (simp add: power_0_left) - apply (rule notI) - apply (simp add: power_0_left) - apply auto - apply (subgoal_tac "0 <= x^n") - apply (frule order_le_imp_less_or_eq) - apply simp - apply (erule zero_le_even_power) - apply (subgoal_tac "0 <= x^n") - apply (frule order_le_imp_less_or_eq) - apply auto - apply (subst zero_le_odd_power) - apply assumption - apply (erule order_less_imp_le) -done - -lemma power_less_zero_eq: "((x::'a::{recpower,ordered_idom}) ^ n < 0) = - (odd n & x < 0)" - apply (subst linorder_not_le [THEN sym])+ - apply (subst zero_le_power_eq) - apply auto -done - -lemma power_le_zero_eq: "((x::'a::{recpower,ordered_idom}) ^ n <= 0) = - (n ~= 0 & ((odd n & x <= 0) | (even n & x = 0)))" - apply (subst linorder_not_less [THEN sym])+ - apply (subst zero_less_power_eq) - apply auto -done - -lemma power_even_abs: "even n ==> - (abs (x::'a::{recpower,ordered_idom}))^n = x^n" - apply (subst power_abs [THEN sym]) - apply (simp add: zero_le_even_power) -done - -lemma zero_less_power_nat_eq: "(0 < (x::nat) ^ n) = (n = 0 | 0 < x)" - by (induct n, auto) - -lemma power_minus_even [simp]: "even n ==> - (- x)^n = (x^n::'a::{recpower,comm_ring_1})" - apply (subst power_minus) - apply simp -done - -lemma power_minus_odd [simp]: "odd n ==> - (- x)^n = - (x^n::'a::{recpower,comm_ring_1})" - apply (subst power_minus) - apply simp -done - -(* Simplify, when the exponent is a numeral *) - -lemmas power_0_left_number_of = power_0_left [of "number_of w", standard] -declare power_0_left_number_of [simp] - -lemmas zero_le_power_eq_number_of = - zero_le_power_eq [of _ "number_of w", standard] -declare zero_le_power_eq_number_of [simp] - -lemmas zero_less_power_eq_number_of = - zero_less_power_eq [of _ "number_of w", standard] -declare zero_less_power_eq_number_of [simp] - -lemmas power_le_zero_eq_number_of = - power_le_zero_eq [of _ "number_of w", standard] -declare power_le_zero_eq_number_of [simp] - -lemmas power_less_zero_eq_number_of = - power_less_zero_eq [of _ "number_of w", standard] -declare power_less_zero_eq_number_of [simp] - -lemmas zero_less_power_nat_eq_number_of = - zero_less_power_nat_eq [of _ "number_of w", standard] -declare zero_less_power_nat_eq_number_of [simp] - -lemmas power_eq_0_iff_number_of = power_eq_0_iff [of _ "number_of w", standard] -declare power_eq_0_iff_number_of [simp] - -lemmas power_even_abs_number_of = power_even_abs [of "number_of w" _, standard] -declare power_even_abs_number_of [simp] - - -subsection {* An Equivalence for @{term [source] "0 \ a^n"} *} - -lemma even_power_le_0_imp_0: - "a ^ (2*k) \ (0::'a::{ordered_idom,recpower}) ==> a=0" -apply (induct k) -apply (auto simp add: zero_le_mult_iff mult_le_0_iff power_Suc) -done - -lemma zero_le_power_iff: - "(0 \ a^n) = (0 \ (a::'a::{ordered_idom,recpower}) | even n)" - (is "?P n") -proof cases - assume even: "even n" - then obtain k where "n = 2*k" - by (auto simp add: even_nat_equiv_def2 numeral_2_eq_2) - thus ?thesis by (simp add: zero_le_even_power even) -next - assume odd: "odd n" - then obtain k where "n = Suc(2*k)" - by (auto simp add: odd_nat_equiv_def2 numeral_2_eq_2) - thus ?thesis - by (auto simp add: power_Suc zero_le_mult_iff zero_le_even_power - dest!: even_power_le_0_imp_0) -qed - -subsection {* Miscellaneous *} - -lemma even_plus_one_div_two: "even (x::int) ==> (x + 1) div 2 = x div 2" - apply (subst zdiv_zadd1_eq) - apply (simp add: even_def) - done - -lemma odd_plus_one_div_two: "odd (x::int) ==> (x + 1) div 2 = x div 2 + 1" - apply (subst zdiv_zadd1_eq) - apply (simp add: even_def) - done - -lemma div_Suc: "Suc a div c = a div c + Suc 0 div c + - (a mod c + Suc 0 mod c) div c" - apply (subgoal_tac "Suc a = a + Suc 0") - apply (erule ssubst) - apply (rule div_add1_eq, simp) - done - -lemma even_nat_plus_one_div_two: "even (x::nat) ==> - (Suc x) div Suc (Suc 0) = x div Suc (Suc 0)" - apply (subst div_Suc) - apply (simp add: even_nat_equiv_def) - done - -lemma odd_nat_plus_one_div_two: "odd (x::nat) ==> - (Suc x) div Suc (Suc 0) = Suc (x div Suc (Suc 0))" - apply (subst div_Suc) - apply (simp add: odd_nat_equiv_def) - done - -end diff -r 617fdb08abe9 -r 47195501ecf7 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Nov 08 22:24:54 2006 +0100 +++ b/src/HOL/IsaMakefile Wed Nov 08 23:11:13 2006 +0100 @@ -84,13 +84,13 @@ $(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML \ $(SRC)/TFL/thry.ML $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML \ Tools/res_atpset.ML \ - Binomial.thy Code_Generator.thy Datatype.ML Datatype.thy \ + Code_Generator.thy Datatype.ML Datatype.thy \ Divides.thy \ Equiv_Relations.thy Extraction.thy Finite_Set.ML Finite_Set.thy \ FixedPoint.thy Fun.thy HOL.ML HOL.thy Hilbert_Choice.thy Inductive.thy \ Integ/IntArith.thy Integ/IntDef.thy Integ/IntDiv.thy \ Integ/NatBin.thy Integ/NatSimprocs.thy Integ/Numeral.thy \ - Integ/Parity.thy Integ/Presburger.thy Integ/cooper_dec.ML \ + Integ/Presburger.thy Integ/cooper_dec.ML \ Integ/cooper_proof.ML Integ/reflected_presburger.ML \ Integ/reflected_cooper.ML Integ/int_arith1.ML Integ/int_factor_simprocs.ML \ Integ/nat_simprocs.ML Integ/presburger.ML Integ/qelim.ML LOrder.thy \ @@ -182,7 +182,7 @@ Complex/Complex_Main.thy Complex/CLim.thy Complex/CSeries.thy \ Complex/CStar.thy Complex/Complex.thy Complex/ComplexBin.thy \ Complex/NSCA.thy Complex/NSComplex.thy Complex/document/root.tex \ - Library/Infinite_Set.thy + Library/Infinite_Set.thy Library/Parity.thy @cd Complex; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-Complex @@ -215,7 +215,8 @@ Library/Library/document/root.bib Library/While_Combinator.thy \ Library/Product_ord.thy Library/Char_ord.thy \ Library/List_lexord.thy Library/Commutative_Ring.thy Library/comm_ring.ML \ - Library/Coinductive_List.thy Library/AssocList.thy + Library/Coinductive_List.thy Library/AssocList.thy \ + Library/Parity.thy Library/GCD.thy Library/Binomial.thy @cd Library; $(ISATOOL) usedir $(OUT)/HOL Library @@ -656,7 +657,7 @@ ex/SAT_Examples.thy ex/svc_oracle.ML ex/SVC_Oracle.thy \ ex/Sudoku.thy ex/Tarski.thy ex/document/root.bib ex/document/root.tex \ ex/mesontest2.ML ex/mesontest2.thy ex/reflection.ML ex/set.thy \ - ex/svc_funcs.ML ex/svc_test.thy + ex/svc_funcs.ML ex/svc_test.thy Library/Parity.thy Library/GCD.thy @$(ISATOOL) usedir $(OUT)/HOL ex diff -r 617fdb08abe9 -r 47195501ecf7 src/HOL/Library/Binomial.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Binomial.thy Wed Nov 08 23:11:13 2006 +0100 @@ -0,0 +1,189 @@ +(* Title: HOL/Binomial.thy + ID: $Id$ + Author: Lawrence C Paulson + Copyright 1997 University of Cambridge +*) + +header{*Binomial Coefficients*} + +theory Binomial +imports Main +begin + +text{*This development is based on the work of Andy Gordon and +Florian Kammueller*} + +consts + binomial :: "nat \ nat \ nat" (infixl "choose" 65) + +primrec + binomial_0: "(0 choose k) = (if k = 0 then 1 else 0)" + + binomial_Suc: "(Suc n choose k) = + (if k = 0 then 1 else (n choose (k - 1)) + (n choose k))" + +lemma binomial_n_0 [simp]: "(n choose 0) = 1" +by (cases n) simp_all + +lemma binomial_0_Suc [simp]: "(0 choose Suc k) = 0" +by simp + +lemma binomial_Suc_Suc [simp]: + "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)" +by simp + +lemma binomial_eq_0 [rule_format]: "\k. n < k --> (n choose k) = 0" +apply (induct "n") +apply auto +done + +declare binomial_0 [simp del] binomial_Suc [simp del] + +lemma binomial_n_n [simp]: "(n choose n) = 1" +apply (induct "n") +apply (simp_all add: binomial_eq_0) +done + +lemma binomial_Suc_n [simp]: "(Suc n choose n) = Suc n" +by (induct "n", simp_all) + +lemma binomial_1 [simp]: "(n choose Suc 0) = n" +by (induct "n", simp_all) + +lemma zero_less_binomial [rule_format]: "k \ n --> 0 < (n choose k)" +by (rule_tac m = n and n = k in diff_induct, simp_all) + +lemma binomial_eq_0_iff: "(n choose k = 0) = (nn)" +by (simp add: linorder_not_less [symmetric] binomial_eq_0_iff [symmetric]) + +(*Might be more useful if re-oriented*) +lemma Suc_times_binomial_eq [rule_format]: + "\k. k \ n --> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k" +apply (induct "n") +apply (simp add: binomial_0, clarify) +apply (case_tac "k") +apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq + binomial_eq_0) +done + +text{*This is the well-known version, but it's harder to use because of the + need to reason about division.*} +lemma binomial_Suc_Suc_eq_times: + "k \ n ==> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k" +by (simp add: Suc_times_binomial_eq div_mult_self_is_m zero_less_Suc + del: mult_Suc mult_Suc_right) + +text{*Another version, with -1 instead of Suc.*} +lemma times_binomial_minus1_eq: + "[|k \ n; 0 (n choose k) * k = n * ((n - 1) choose (k - 1))" +apply (cut_tac n = "n - 1" and k = "k - 1" in Suc_times_binomial_eq) +apply (simp split add: nat_diff_split, auto) +done + +subsubsection {* Theorems about @{text "choose"} *} + +text {* + \medskip Basic theorem about @{text "choose"}. By Florian + Kamm\"uller, tidied by LCP. +*} + +lemma card_s_0_eq_empty: + "finite A ==> card {B. B \ A & card B = 0} = 1" + apply (simp cong add: conj_cong add: finite_subset [THEN card_0_eq]) + apply (simp cong add: rev_conj_cong) + done + +lemma choose_deconstruct: "finite M ==> x \ M + ==> {s. s <= insert x M & card(s) = Suc k} + = {s. s <= M & card(s) = Suc k} Un + {s. EX t. t <= M & card(t) = k & s = insert x t}" + apply safe + apply (auto intro: finite_subset [THEN card_insert_disjoint]) + apply (drule_tac x = "xa - {x}" in spec) + apply (subgoal_tac "x \ xa", auto) + apply (erule rev_mp, subst card_Diff_singleton) + apply (auto intro: finite_subset) + done + +text{*There are as many subsets of @{term A} having cardinality @{term k} + as there are sets obtained from the former by inserting a fixed element + @{term x} into each.*} +lemma constr_bij: + "[|finite A; x \ A|] ==> + card {B. EX C. C <= A & card(C) = k & B = insert x C} = + card {B. B <= A & card(B) = k}" + apply (rule_tac f = "%s. s - {x}" and g = "insert x" in card_bij_eq) + apply (auto elim!: equalityE simp add: inj_on_def) + apply (subst Diff_insert0, auto) + txt {* finiteness of the two sets *} + apply (rule_tac [2] B = "Pow (A)" in finite_subset) + apply (rule_tac B = "Pow (insert x A)" in finite_subset) + apply fast+ + done + +text {* + Main theorem: combinatorial statement about number of subsets of a set. +*} + +lemma n_sub_lemma: + "!!A. finite A ==> card {B. B <= A & card B = k} = (card A choose k)" + apply (induct k) + apply (simp add: card_s_0_eq_empty, atomize) + apply (rotate_tac -1, erule finite_induct) + apply (simp_all (no_asm_simp) cong add: conj_cong + add: card_s_0_eq_empty choose_deconstruct) + apply (subst card_Un_disjoint) + prefer 4 apply (force simp add: constr_bij) + prefer 3 apply force + prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2] + finite_subset [of _ "Pow (insert x F)", standard]) + apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset]) + done + +theorem n_subsets: + "finite A ==> card {B. B <= A & card B = k} = (card A choose k)" + by (simp add: n_sub_lemma) + + +text{* The binomial theorem (courtesy of Tobias Nipkow): *} + +theorem binomial: "(a+b::nat)^n = (\k=0..n. (n choose k) * a^k * b^(n-k))" +proof (induct n) + case 0 thus ?case by simp +next + case (Suc n) + have decomp: "{0..n+1} = {0} \ {n+1} \ {1..n}" + by (auto simp add:atLeastAtMost_def atLeast_def atMost_def) + have decomp2: "{0..n} = {0} \ {1..n}" + by (auto simp add:atLeastAtMost_def atLeast_def atMost_def) + have "(a+b::nat)^(n+1) = (a+b) * (\k=0..n. (n choose k) * a^k * b^(n-k))" + using Suc by simp + also have "\ = a*(\k=0..n. (n choose k) * a^k * b^(n-k)) + + b*(\k=0..n. (n choose k) * a^k * b^(n-k))" + by(rule nat_distrib) + also have "\ = (\k=0..n. (n choose k) * a^(k+1) * b^(n-k)) + + (\k=0..n. (n choose k) * a^k * b^(n-k+1))" + by(simp add: setsum_right_distrib mult_ac) + also have "\ = (\k=0..n. (n choose k) * a^k * b^(n+1-k)) + + (\k=1..n+1. (n choose (k - 1)) * a^k * b^(n+1-k))" + by (simp add:setsum_shift_bounds_cl_Suc_ivl Suc_diff_le + del:setsum_cl_ivl_Suc) + also have "\ = a^(n+1) + b^(n+1) + + (\k=1..n. (n choose (k - 1)) * a^k * b^(n+1-k)) + + (\k=1..n. (n choose k) * a^k * b^(n+1-k))" + by(simp add: decomp2) + also have + "\ = a^(n+1) + b^(n+1) + (\k=1..n. (n+1 choose k) * a^k * b^(n+1-k))" + by(simp add: nat_distrib setsum_addf binomial.simps) + also have "\ = (\k=0..n+1. (n+1 choose k) * a^k * b^(n+1-k))" + using decomp by simp + finally show ?case by simp +qed + +end diff -r 617fdb08abe9 -r 47195501ecf7 src/HOL/Library/Commutative_Ring.thy --- a/src/HOL/Library/Commutative_Ring.thy Wed Nov 08 22:24:54 2006 +0100 +++ b/src/HOL/Library/Commutative_Ring.thy Wed Nov 08 23:11:13 2006 +0100 @@ -7,7 +7,7 @@ header {* Proving equalities in commutative rings *} theory Commutative_Ring -imports Main +imports Main Parity uses ("comm_ring.ML") begin diff -r 617fdb08abe9 -r 47195501ecf7 src/HOL/Library/GCD.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/GCD.thy Wed Nov 08 23:11:13 2006 +0100 @@ -0,0 +1,206 @@ +(* Title: HOL/GCD.thy + ID: $Id$ + Author: Christophe Tabacznyj and Lawrence C Paulson + Copyright 1996 University of Cambridge +*) + +header {* The Greatest Common Divisor *} + +theory GCD +imports Main +begin + +text {* + See \cite{davenport92}. + \bigskip +*} + +consts + gcd :: "nat \ nat => nat" -- {* Euclid's algorithm *} + +recdef gcd "measure ((\(m, n). n) :: nat \ nat => nat)" + "gcd (m, n) = (if n = 0 then m else gcd (n, m mod n))" + +constdefs + is_gcd :: "nat => nat => nat => bool" -- {* @{term gcd} as a relation *} + "is_gcd p m n == p dvd m \ p dvd n \ + (\d. d dvd m \ d dvd n --> d dvd p)" + + +lemma gcd_induct: + "(!!m. P m 0) ==> + (!!m n. 0 < n ==> P n (m mod n) ==> P m n) + ==> P (m::nat) (n::nat)" + apply (induct m n rule: gcd.induct) + apply (case_tac "n = 0") + apply simp_all + done + + +lemma gcd_0 [simp]: "gcd (m, 0) = m" + apply simp + done + +lemma gcd_non_0: "0 < n ==> gcd (m, n) = gcd (n, m mod n)" + apply simp + done + +declare gcd.simps [simp del] + +lemma gcd_1 [simp]: "gcd (m, Suc 0) = 1" + apply (simp add: gcd_non_0) + done + +text {* + \medskip @{term "gcd (m, n)"} divides @{text m} and @{text n}. The + conjunctions don't seem provable separately. +*} + +lemma gcd_dvd1 [iff]: "gcd (m, n) dvd m" + and gcd_dvd2 [iff]: "gcd (m, n) dvd n" + apply (induct m n rule: gcd_induct) + apply (simp_all add: gcd_non_0) + apply (blast dest: dvd_mod_imp_dvd) + done + +text {* + \medskip Maximality: for all @{term m}, @{term n}, @{term k} + naturals, if @{term k} divides @{term m} and @{term k} divides + @{term n} then @{term k} divides @{term "gcd (m, n)"}. +*} + +lemma gcd_greatest: "k dvd m ==> k dvd n ==> k dvd gcd (m, n)" + apply (induct m n rule: gcd_induct) + apply (simp_all add: gcd_non_0 dvd_mod) + done + +lemma gcd_greatest_iff [iff]: "(k dvd gcd (m, n)) = (k dvd m \ k dvd n)" + apply (blast intro!: gcd_greatest intro: dvd_trans) + done + +lemma gcd_zero: "(gcd (m, n) = 0) = (m = 0 \ n = 0)" + by (simp only: dvd_0_left_iff [THEN sym] gcd_greatest_iff) + + +text {* + \medskip Function gcd yields the Greatest Common Divisor. +*} + +lemma is_gcd: "is_gcd (gcd (m, n)) m n" + apply (simp add: is_gcd_def gcd_greatest) + done + +text {* + \medskip Uniqueness of GCDs. +*} + +lemma is_gcd_unique: "is_gcd m a b ==> is_gcd n a b ==> m = n" + apply (simp add: is_gcd_def) + apply (blast intro: dvd_anti_sym) + done + +lemma is_gcd_dvd: "is_gcd m a b ==> k dvd a ==> k dvd b ==> k dvd m" + apply (auto simp add: is_gcd_def) + done + + +text {* + \medskip Commutativity +*} + +lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m" + apply (auto simp add: is_gcd_def) + done + +lemma gcd_commute: "gcd (m, n) = gcd (n, m)" + apply (rule is_gcd_unique) + apply (rule is_gcd) + apply (subst is_gcd_commute) + apply (simp add: is_gcd) + done + +lemma gcd_assoc: "gcd (gcd (k, m), n) = gcd (k, gcd (m, n))" + apply (rule is_gcd_unique) + apply (rule is_gcd) + apply (simp add: is_gcd_def) + apply (blast intro: dvd_trans) + done + +lemma gcd_0_left [simp]: "gcd (0, m) = m" + apply (simp add: gcd_commute [of 0]) + done + +lemma gcd_1_left [simp]: "gcd (Suc 0, m) = 1" + apply (simp add: gcd_commute [of "Suc 0"]) + done + + +text {* + \medskip Multiplication laws +*} + +lemma gcd_mult_distrib2: "k * gcd (m, n) = gcd (k * m, k * n)" + -- {* \cite[page 27]{davenport92} *} + apply (induct m n rule: gcd_induct) + apply simp + apply (case_tac "k = 0") + apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2) + done + +lemma gcd_mult [simp]: "gcd (k, k * n) = k" + apply (rule gcd_mult_distrib2 [of k 1 n, simplified, symmetric]) + done + +lemma gcd_self [simp]: "gcd (k, k) = k" + apply (rule gcd_mult [of k 1, simplified]) + done + +lemma relprime_dvd_mult: "gcd (k, n) = 1 ==> k dvd m * n ==> k dvd m" + apply (insert gcd_mult_distrib2 [of m k n]) + apply simp + apply (erule_tac t = m in ssubst) + apply simp + done + +lemma relprime_dvd_mult_iff: "gcd (k, n) = 1 ==> (k dvd m * n) = (k dvd m)" + apply (blast intro: relprime_dvd_mult dvd_trans) + done + +lemma gcd_mult_cancel: "gcd (k, n) = 1 ==> gcd (k * m, n) = gcd (m, n)" + apply (rule dvd_anti_sym) + apply (rule gcd_greatest) + apply (rule_tac n = k in relprime_dvd_mult) + apply (simp add: gcd_assoc) + apply (simp add: gcd_commute) + apply (simp_all add: mult_commute) + apply (blast intro: dvd_trans) + done + + +text {* \medskip Addition laws *} + +lemma gcd_add1 [simp]: "gcd (m + n, n) = gcd (m, n)" + apply (case_tac "n = 0") + apply (simp_all add: gcd_non_0) + done + +lemma gcd_add2 [simp]: "gcd (m, m + n) = gcd (m, n)" +proof - + have "gcd (m, m + n) = gcd (m + n, m)" by (rule gcd_commute) + also have "... = gcd (n + m, m)" by (simp add: add_commute) + also have "... = gcd (n, m)" by simp + also have "... = gcd (m, n)" by (rule gcd_commute) + finally show ?thesis . +qed + +lemma gcd_add2' [simp]: "gcd (m, n + m) = gcd (m, n)" + apply (subst add_commute) + apply (rule gcd_add2) + done + +lemma gcd_add_mult: "gcd (m, k * m + n) = gcd (m, n)" + apply (induct k) + apply (simp_all add: add_assoc) + done + +end diff -r 617fdb08abe9 -r 47195501ecf7 src/HOL/Library/Infinite_Set.thy --- a/src/HOL/Library/Infinite_Set.thy Wed Nov 08 22:24:54 2006 +0100 +++ b/src/HOL/Library/Infinite_Set.thy Wed Nov 08 23:11:13 2006 +0100 @@ -6,7 +6,7 @@ header {* Infinite Sets and Related Concepts *} theory Infinite_Set -imports Hilbert_Choice Binomial +imports Main begin subsection "Infinite Sets" diff -r 617fdb08abe9 -r 47195501ecf7 src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Wed Nov 08 22:24:54 2006 +0100 +++ b/src/HOL/Library/Library.thy Wed Nov 08 23:11:13 2006 +0100 @@ -2,30 +2,33 @@ (*<*) theory Library imports + AssocList BigO + Binomial + Char_ord + Coinductive_List + Commutative_Ring Continuity EfficientNat + ExecutableRat ExecutableSet - ExecutableRat + FuncSet + GCD + Infinite_Set MLString - FuncSet Multiset NatPair Nat_Infinity Nested_Environment OptionalSugar + Parity Permutation Primes Quotient + State_Monad While_Combinator Word Zorn - Char_ord - Commutative_Ring - Coinductive_List - AssocList - Infinite_Set - State_Monad begin end (*>*) diff -r 617fdb08abe9 -r 47195501ecf7 src/HOL/Library/Parity.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Parity.thy Wed Nov 08 23:11:13 2006 +0100 @@ -0,0 +1,451 @@ +(* Title: Parity.thy + ID: $Id$ + Author: Jeremy Avigad +*) + +header {* Even and Odd for int and nat *} + +theory Parity +imports Main +begin + +axclass even_odd < type + +consts + even :: "'a::even_odd => bool" + +instance int :: even_odd .. +instance nat :: even_odd .. + +defs (overloaded) + even_def: "even (x::int) == x mod 2 = 0" + even_nat_def: "even (x::nat) == even (int x)" + +abbreviation + odd :: "'a::even_odd => bool" + "odd x == \ even x" + + +subsection {* Even and odd are mutually exclusive *} + +lemma int_pos_lt_two_imp_zero_or_one: + "0 <= x ==> (x::int) < 2 ==> x = 0 | x = 1" + by auto + +lemma neq_one_mod_two [simp]: "((x::int) mod 2 ~= 0) = (x mod 2 = 1)" + apply (subgoal_tac "x mod 2 = 0 | x mod 2 = 1", force) + apply (rule int_pos_lt_two_imp_zero_or_one, auto) + done + +subsection {* Behavior under integer arithmetic operations *} + +lemma even_times_anything: "even (x::int) ==> even (x * y)" + by (simp add: even_def zmod_zmult1_eq') + +lemma anything_times_even: "even (y::int) ==> even (x * y)" + by (simp add: even_def zmod_zmult1_eq) + +lemma odd_times_odd: "odd (x::int) ==> odd y ==> odd (x * y)" + by (simp add: even_def zmod_zmult1_eq) + +lemma even_product: "even((x::int) * y) = (even x | even y)" + apply (auto simp add: even_times_anything anything_times_even) + apply (rule ccontr) + apply (auto simp add: odd_times_odd) + done + +lemma even_plus_even: "even (x::int) ==> even y ==> even (x + y)" + by (simp add: even_def zmod_zadd1_eq) + +lemma even_plus_odd: "even (x::int) ==> odd y ==> odd (x + y)" + by (simp add: even_def zmod_zadd1_eq) + +lemma odd_plus_even: "odd (x::int) ==> even y ==> odd (x + y)" + by (simp add: even_def zmod_zadd1_eq) + +lemma odd_plus_odd: "odd (x::int) ==> odd y ==> even (x + y)" + by (simp add: even_def zmod_zadd1_eq) + +lemma even_sum: "even ((x::int) + y) = ((even x & even y) | (odd x & odd y))" + apply (auto intro: even_plus_even odd_plus_odd) + apply (rule ccontr, simp add: even_plus_odd) + apply (rule ccontr, simp add: odd_plus_even) + done + +lemma even_neg: "even (-(x::int)) = even x" + by (auto simp add: even_def zmod_zminus1_eq_if) + +lemma even_difference: + "even ((x::int) - y) = ((even x & even y) | (odd x & odd y))" + by (simp only: diff_minus even_sum even_neg) + +lemma even_pow_gt_zero [rule_format]: + "even (x::int) ==> 0 < n --> even (x^n)" + apply (induct n) + apply (auto simp add: even_product) + done + +lemma odd_pow: "odd x ==> odd((x::int)^n)" + apply (induct n) + apply (simp add: even_def) + apply (simp add: even_product) + done + +lemma even_power: "even ((x::int)^n) = (even x & 0 < n)" + apply (auto simp add: even_pow_gt_zero) + apply (erule contrapos_pp, erule odd_pow) + apply (erule contrapos_pp, simp add: even_def) + done + +lemma even_zero: "even (0::int)" + by (simp add: even_def) + +lemma odd_one: "odd (1::int)" + by (simp add: even_def) + +lemmas even_odd_simps [simp] = even_def[of "number_of v",standard] even_zero + odd_one even_product even_sum even_neg even_difference even_power + + +subsection {* Equivalent definitions *} + +lemma two_times_even_div_two: "even (x::int) ==> 2 * (x div 2) = x" + by (auto simp add: even_def) + +lemma two_times_odd_div_two_plus_one: "odd (x::int) ==> + 2 * (x div 2) + 1 = x" + apply (insert zmod_zdiv_equality [of x 2, THEN sym]) + by (simp add: even_def) + +lemma even_equiv_def: "even (x::int) = (EX y. x = 2 * y)" + apply auto + apply (rule exI) + by (erule two_times_even_div_two [THEN sym]) + +lemma odd_equiv_def: "odd (x::int) = (EX y. x = 2 * y + 1)" + apply auto + apply (rule exI) + by (erule two_times_odd_div_two_plus_one [THEN sym]) + + +subsection {* even and odd for nats *} + +lemma pos_int_even_equiv_nat_even: "0 \ x ==> even x = even (nat x)" + by (simp add: even_nat_def) + +lemma even_nat_product: "even((x::nat) * y) = (even x | even y)" + by (simp add: even_nat_def int_mult) + +lemma even_nat_sum: "even ((x::nat) + y) = + ((even x & even y) | (odd x & odd y))" + by (unfold even_nat_def, simp) + +lemma even_nat_difference: + "even ((x::nat) - y) = (x < y | (even x & even y) | (odd x & odd y))" + apply (auto simp add: even_nat_def zdiff_int [THEN sym]) + apply (case_tac "x < y", auto simp add: zdiff_int [THEN sym]) + apply (case_tac "x < y", auto simp add: zdiff_int [THEN sym]) + done + +lemma even_nat_Suc: "even (Suc x) = odd x" + by (simp add: even_nat_def) + +lemma even_nat_power: "even ((x::nat)^y) = (even x & 0 < y)" + by (simp add: even_nat_def int_power) + +lemma even_nat_zero: "even (0::nat)" + by (simp add: even_nat_def) + +lemmas even_odd_nat_simps [simp] = even_nat_def[of "number_of v",standard] + even_nat_zero even_nat_Suc even_nat_product even_nat_sum even_nat_power + + +subsection {* Equivalent definitions *} + +lemma nat_lt_two_imp_zero_or_one: "(x::nat) < Suc (Suc 0) ==> + x = 0 | x = Suc 0" + by auto + +lemma even_nat_mod_two_eq_zero: "even (x::nat) ==> x mod (Suc (Suc 0)) = 0" + apply (insert mod_div_equality [of x "Suc (Suc 0)", THEN sym]) + apply (drule subst, assumption) + apply (subgoal_tac "x mod Suc (Suc 0) = 0 | x mod Suc (Suc 0) = Suc 0") + apply force + apply (subgoal_tac "0 < Suc (Suc 0)") + apply (frule mod_less_divisor [of "Suc (Suc 0)" x]) + apply (erule nat_lt_two_imp_zero_or_one, auto) + done + +lemma odd_nat_mod_two_eq_one: "odd (x::nat) ==> x mod (Suc (Suc 0)) = Suc 0" + apply (insert mod_div_equality [of x "Suc (Suc 0)", THEN sym]) + apply (drule subst, assumption) + apply (subgoal_tac "x mod Suc (Suc 0) = 0 | x mod Suc (Suc 0) = Suc 0") + apply force + apply (subgoal_tac "0 < Suc (Suc 0)") + apply (frule mod_less_divisor [of "Suc (Suc 0)" x]) + apply (erule nat_lt_two_imp_zero_or_one, auto) + done + +lemma even_nat_equiv_def: "even (x::nat) = (x mod Suc (Suc 0) = 0)" + apply (rule iffI) + apply (erule even_nat_mod_two_eq_zero) + apply (insert odd_nat_mod_two_eq_one [of x], auto) + done + +lemma odd_nat_equiv_def: "odd (x::nat) = (x mod Suc (Suc 0) = Suc 0)" + apply (auto simp add: even_nat_equiv_def) + apply (subgoal_tac "x mod (Suc (Suc 0)) < Suc (Suc 0)") + apply (frule nat_lt_two_imp_zero_or_one, auto) + done + +lemma even_nat_div_two_times_two: "even (x::nat) ==> + Suc (Suc 0) * (x div Suc (Suc 0)) = x" + apply (insert mod_div_equality [of x "Suc (Suc 0)", THEN sym]) + apply (drule even_nat_mod_two_eq_zero, simp) + done + +lemma odd_nat_div_two_times_two_plus_one: "odd (x::nat) ==> + Suc( Suc (Suc 0) * (x div Suc (Suc 0))) = x" + apply (insert mod_div_equality [of x "Suc (Suc 0)", THEN sym]) + apply (drule odd_nat_mod_two_eq_one, simp) + done + +lemma even_nat_equiv_def2: "even (x::nat) = (EX y. x = Suc (Suc 0) * y)" + apply (rule iffI, rule exI) + apply (erule even_nat_div_two_times_two [THEN sym], auto) + done + +lemma odd_nat_equiv_def2: "odd (x::nat) = (EX y. x = Suc(Suc (Suc 0) * y))" + apply (rule iffI, rule exI) + apply (erule odd_nat_div_two_times_two_plus_one [THEN sym], auto) + done + +subsection {* Parity and powers *} + +lemma minus_one_even_odd_power: + "(even x --> (- 1::'a::{comm_ring_1,recpower})^x = 1) & + (odd x --> (- 1::'a)^x = - 1)" + apply (induct x) + apply (rule conjI) + apply simp + apply (insert even_nat_zero, blast) + apply (simp add: power_Suc) +done + +lemma minus_one_even_power [simp]: + "even x ==> (- 1::'a::{comm_ring_1,recpower})^x = 1" + by (rule minus_one_even_odd_power [THEN conjunct1, THEN mp], assumption) + +lemma minus_one_odd_power [simp]: + "odd x ==> (- 1::'a::{comm_ring_1,recpower})^x = - 1" + by (rule minus_one_even_odd_power [THEN conjunct2, THEN mp], assumption) + +lemma neg_one_even_odd_power: + "(even x --> (-1::'a::{number_ring,recpower})^x = 1) & + (odd x --> (-1::'a)^x = -1)" + apply (induct x) + apply (simp, simp add: power_Suc) + done + +lemma neg_one_even_power [simp]: + "even x ==> (-1::'a::{number_ring,recpower})^x = 1" + by (rule neg_one_even_odd_power [THEN conjunct1, THEN mp], assumption) + +lemma neg_one_odd_power [simp]: + "odd x ==> (-1::'a::{number_ring,recpower})^x = -1" + by (rule neg_one_even_odd_power [THEN conjunct2, THEN mp], assumption) + +lemma neg_power_if: + "(-x::'a::{comm_ring_1,recpower}) ^ n = + (if even n then (x ^ n) else -(x ^ n))" + by (induct n, simp_all split: split_if_asm add: power_Suc) + +lemma zero_le_even_power: "even n ==> + 0 <= (x::'a::{recpower,ordered_ring_strict}) ^ n" + apply (simp add: even_nat_equiv_def2) + apply (erule exE) + apply (erule ssubst) + apply (subst power_add) + apply (rule zero_le_square) + done + +lemma zero_le_odd_power: "odd n ==> + (0 <= (x::'a::{recpower,ordered_idom}) ^ n) = (0 <= x)" + apply (simp add: odd_nat_equiv_def2) + apply (erule exE) + apply (erule ssubst) + apply (subst power_Suc) + apply (subst power_add) + apply (subst zero_le_mult_iff) + apply auto + apply (subgoal_tac "x = 0 & 0 < y") + apply (erule conjE, assumption) + apply (subst power_eq_0_iff [THEN sym]) + apply (subgoal_tac "0 <= x^y * x^y") + apply simp + apply (rule zero_le_square)+ +done + +lemma zero_le_power_eq: "(0 <= (x::'a::{recpower,ordered_idom}) ^ n) = + (even n | (odd n & 0 <= x))" + apply auto + apply (subst zero_le_odd_power [THEN sym]) + apply assumption+ + apply (erule zero_le_even_power) + apply (subst zero_le_odd_power) + apply assumption+ +done + +lemma zero_less_power_eq: "(0 < (x::'a::{recpower,ordered_idom}) ^ n) = + (n = 0 | (even n & x ~= 0) | (odd n & 0 < x))" + apply (rule iffI) + apply clarsimp + apply (rule conjI) + apply clarsimp + apply (rule ccontr) + apply (subgoal_tac "~ (0 <= x^n)") + apply simp + apply (subst zero_le_odd_power) + apply assumption + apply simp + apply (rule notI) + apply (simp add: power_0_left) + apply (rule notI) + apply (simp add: power_0_left) + apply auto + apply (subgoal_tac "0 <= x^n") + apply (frule order_le_imp_less_or_eq) + apply simp + apply (erule zero_le_even_power) + apply (subgoal_tac "0 <= x^n") + apply (frule order_le_imp_less_or_eq) + apply auto + apply (subst zero_le_odd_power) + apply assumption + apply (erule order_less_imp_le) +done + +lemma power_less_zero_eq: "((x::'a::{recpower,ordered_idom}) ^ n < 0) = + (odd n & x < 0)" + apply (subst linorder_not_le [THEN sym])+ + apply (subst zero_le_power_eq) + apply auto +done + +lemma power_le_zero_eq: "((x::'a::{recpower,ordered_idom}) ^ n <= 0) = + (n ~= 0 & ((odd n & x <= 0) | (even n & x = 0)))" + apply (subst linorder_not_less [THEN sym])+ + apply (subst zero_less_power_eq) + apply auto +done + +lemma power_even_abs: "even n ==> + (abs (x::'a::{recpower,ordered_idom}))^n = x^n" + apply (subst power_abs [THEN sym]) + apply (simp add: zero_le_even_power) +done + +lemma zero_less_power_nat_eq: "(0 < (x::nat) ^ n) = (n = 0 | 0 < x)" + by (induct n, auto) + +lemma power_minus_even [simp]: "even n ==> + (- x)^n = (x^n::'a::{recpower,comm_ring_1})" + apply (subst power_minus) + apply simp +done + +lemma power_minus_odd [simp]: "odd n ==> + (- x)^n = - (x^n::'a::{recpower,comm_ring_1})" + apply (subst power_minus) + apply simp +done + +(* Simplify, when the exponent is a numeral *) + +lemmas power_0_left_number_of = power_0_left [of "number_of w", standard] +declare power_0_left_number_of [simp] + +lemmas zero_le_power_eq_number_of = + zero_le_power_eq [of _ "number_of w", standard] +declare zero_le_power_eq_number_of [simp] + +lemmas zero_less_power_eq_number_of = + zero_less_power_eq [of _ "number_of w", standard] +declare zero_less_power_eq_number_of [simp] + +lemmas power_le_zero_eq_number_of = + power_le_zero_eq [of _ "number_of w", standard] +declare power_le_zero_eq_number_of [simp] + +lemmas power_less_zero_eq_number_of = + power_less_zero_eq [of _ "number_of w", standard] +declare power_less_zero_eq_number_of [simp] + +lemmas zero_less_power_nat_eq_number_of = + zero_less_power_nat_eq [of _ "number_of w", standard] +declare zero_less_power_nat_eq_number_of [simp] + +lemmas power_eq_0_iff_number_of = power_eq_0_iff [of _ "number_of w", standard] +declare power_eq_0_iff_number_of [simp] + +lemmas power_even_abs_number_of = power_even_abs [of "number_of w" _, standard] +declare power_even_abs_number_of [simp] + + +subsection {* An Equivalence for @{term [source] "0 \ a^n"} *} + +lemma even_power_le_0_imp_0: + "a ^ (2*k) \ (0::'a::{ordered_idom,recpower}) ==> a=0" +apply (induct k) +apply (auto simp add: zero_le_mult_iff mult_le_0_iff power_Suc) +done + +lemma zero_le_power_iff: + "(0 \ a^n) = (0 \ (a::'a::{ordered_idom,recpower}) | even n)" + (is "?P n") +proof cases + assume even: "even n" + then obtain k where "n = 2*k" + by (auto simp add: even_nat_equiv_def2 numeral_2_eq_2) + thus ?thesis by (simp add: zero_le_even_power even) +next + assume odd: "odd n" + then obtain k where "n = Suc(2*k)" + by (auto simp add: odd_nat_equiv_def2 numeral_2_eq_2) + thus ?thesis + by (auto simp add: power_Suc zero_le_mult_iff zero_le_even_power + dest!: even_power_le_0_imp_0) +qed + +subsection {* Miscellaneous *} + +lemma even_plus_one_div_two: "even (x::int) ==> (x + 1) div 2 = x div 2" + apply (subst zdiv_zadd1_eq) + apply (simp add: even_def) + done + +lemma odd_plus_one_div_two: "odd (x::int) ==> (x + 1) div 2 = x div 2 + 1" + apply (subst zdiv_zadd1_eq) + apply (simp add: even_def) + done + +lemma div_Suc: "Suc a div c = a div c + Suc 0 div c + + (a mod c + Suc 0 mod c) div c" + apply (subgoal_tac "Suc a = a + Suc 0") + apply (erule ssubst) + apply (rule div_add1_eq, simp) + done + +lemma even_nat_plus_one_div_two: "even (x::nat) ==> + (Suc x) div Suc (Suc 0) = x div Suc (Suc 0)" + apply (subst div_Suc) + apply (simp add: even_nat_equiv_def) + done + +lemma odd_nat_plus_one_div_two: "odd (x::nat) ==> + (Suc x) div Suc (Suc 0) = Suc (x div Suc (Suc 0))" + apply (subst div_Suc) + apply (simp add: odd_nat_equiv_def) + done + +end diff -r 617fdb08abe9 -r 47195501ecf7 src/HOL/Library/Primes.thy --- a/src/HOL/Library/Primes.thy Wed Nov 08 22:24:54 2006 +0100 +++ b/src/HOL/Library/Primes.thy Wed Nov 08 23:11:13 2006 +0100 @@ -7,7 +7,7 @@ header {* Primality on nat *} theory Primes -imports Main +imports GCD begin definition diff -r 617fdb08abe9 -r 47195501ecf7 src/HOL/PreList.thy --- a/src/HOL/PreList.thy Wed Nov 08 22:24:54 2006 +0100 +++ b/src/HOL/PreList.thy Wed Nov 08 23:11:13 2006 +0100 @@ -7,7 +7,7 @@ header {* A Basis for Building the Theory of Lists *} theory PreList -imports Wellfounded_Relations Presburger Relation_Power Binomial +imports Wellfounded_Relations Presburger Relation_Power begin text {* diff -r 617fdb08abe9 -r 47195501ecf7 src/HOL/Real/Float.thy --- a/src/HOL/Real/Float.thy Wed Nov 08 22:24:54 2006 +0100 +++ b/src/HOL/Real/Float.thy Wed Nov 08 23:11:13 2006 +0100 @@ -6,7 +6,7 @@ header {* Floating Point Representation of the Reals *} theory Float -imports Real +imports Real Parity uses ("float.ML") begin diff -r 617fdb08abe9 -r 47195501ecf7 src/HOL/ex/NatSum.thy --- a/src/HOL/ex/NatSum.thy Wed Nov 08 22:24:54 2006 +0100 +++ b/src/HOL/ex/NatSum.thy Wed Nov 08 23:11:13 2006 +0100 @@ -5,7 +5,7 @@ header {* Summing natural numbers *} -theory NatSum imports Main begin +theory NatSum imports Main Parity begin text {* Summing natural numbers, squares, cubes, etc. diff -r 617fdb08abe9 -r 47195501ecf7 src/HOL/ex/ROOT.ML --- a/src/HOL/ex/ROOT.ML Wed Nov 08 22:24:54 2006 +0100 +++ b/src/HOL/ex/ROOT.ML Wed Nov 08 23:11:13 2006 +0100 @@ -4,6 +4,9 @@ Miscellaneous examples for Higher-Order Logic. *) +no_document use_thy "Parity"; +no_document use_thy "GCD"; + no_document time_use_thy "Classpackage"; no_document time_use_thy "Codegenerator"; no_document time_use_thy "CodeCollections"; diff -r 617fdb08abe9 -r 47195501ecf7 src/HOL/ex/Reflected_Presburger.thy --- a/src/HOL/ex/Reflected_Presburger.thy Wed Nov 08 22:24:54 2006 +0100 +++ b/src/HOL/ex/Reflected_Presburger.thy Wed Nov 08 23:11:13 2006 +0100 @@ -9,7 +9,7 @@ header {* Quantifier elimination for Presburger arithmetic *} theory Reflected_Presburger -imports Main +imports Main GCD begin (* Shadow syntax for integer terms *)