# HG changeset patch # User nipkow # Date 1120732757 -7200 # Node ID 236dfafbeb63a14f37bcaa09b3f91e7ba2afe46b # Parent 1bbe526a552c9aaad3e28d74445f876acd291dd3 linear arithmetic now takes "&" in assumptions apart. diff -r 1bbe526a552c -r 236dfafbeb63 src/HOL/Algebra/Exponent.thy --- a/src/HOL/Algebra/Exponent.thy Thu Jul 07 12:36:56 2005 +0200 +++ b/src/HOL/Algebra/Exponent.thy Thu Jul 07 12:39:17 2005 +0200 @@ -27,7 +27,7 @@ apply (case_tac "k=0", simp) apply (drule_tac x = m in spec) apply (drule_tac x = k in spec) -apply (simp add: dvd_mult_cancel1 dvd_mult_cancel2, auto) +apply (simp add: dvd_mult_cancel1 dvd_mult_cancel2) done lemma zero_less_prime_power: "prime p ==> 0 < p^a" diff -r 1bbe526a552c -r 236dfafbeb63 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Thu Jul 07 12:36:56 2005 +0200 +++ b/src/HOL/Divides.thy Thu Jul 07 12:39:17 2005 +0200 @@ -242,7 +242,7 @@ subsection{*Proving facts about Quotient and Remainder*} lemma unique_quotient_lemma: - "[| b*q' + r' \ b*q + r; 0 < b; r < b |] + "[| b*q' + r' \ b*q + r; x < b; r < b |] ==> q' \ (q::nat)" apply (rule leI) apply (subst less_iff_Suc_add) @@ -254,7 +254,7 @@ ==> q = q'" apply (simp add: split_ifs quorem_def) apply (blast intro: order_antisym - dest: order_eq_refl [THEN unique_quotient_lemma] sym)+ + dest: order_eq_refl [THEN unique_quotient_lemma] sym) done lemma unique_remainder: @@ -702,7 +702,9 @@ "0 < n \ (n * q \ m \ m < n * (Suc q)) = (q = ((m::nat) div n))" apply (rule iffI) apply (rule_tac a=m and r = "m - n * q" and r' = "m mod n" in unique_quotient) - apply (simp_all add: quorem_def, arith) +prefer 3; apply assumption + apply (simp_all add: quorem_def) + apply arith apply (rule conjI) apply (rule_tac P="%x. n * (m div n) \ x" in subst [OF mod_div_equality [of _ n]]) diff -r 1bbe526a552c -r 236dfafbeb63 src/HOL/Finite_Set.ML --- a/src/HOL/Finite_Set.ML Thu Jul 07 12:36:56 2005 +0200 +++ b/src/HOL/Finite_Set.ML Thu Jul 07 12:39:17 2005 +0200 @@ -45,10 +45,7 @@ val card_insert_le = thm "card_insert_le"; val card_mono = thm "card_mono"; val card_psubset = thm "card_psubset"; -val card_s_0_eq_empty = thm "card_s_0_eq_empty"; val card_seteq = thm "card_seteq"; -val choose_deconstruct = thm "choose_deconstruct"; -val constr_bij = thm "constr_bij"; val Diff1_foldSet = thm "Diff1_foldSet"; val dvd_partition = thm "dvd_partition"; val empty_foldSetE = thm "empty_foldSetE"; @@ -89,8 +86,6 @@ val fold_insert = thm "ACf.fold_insert"; val fold_nest_Un_Int = thm "ACf.fold_nest_Un_Int"; val fold_nest_Un_disjoint = thm "ACf.fold_nest_Un_disjoint"; -val n_sub_lemma = thm "n_sub_lemma"; -val n_subsets = thm "n_subsets"; val psubset_card_mono = thm "psubset_card_mono"; val setsum_0 = thm "setsum_0"; val setsum_SucD = thm "setsum_SucD"; diff -r 1bbe526a552c -r 236dfafbeb63 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Thu Jul 07 12:36:56 2005 +0200 +++ b/src/HOL/Finite_Set.thy Thu Jul 07 12:39:17 2005 +0200 @@ -891,8 +891,9 @@ "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B" by(fastsimp simp: setsum_def intro: AC_add.fold_cong) -lemma strong_setsum_cong: - "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setsum f A = setsum g B" +lemma strong_setsum_cong[cong]: + "A = B ==> (!!x. x:B =simp=> f x = g x) + ==> setsum (%x. f x) A = setsum (%x. g x) B" by(fastsimp simp: simp_implies_def setsum_def intro: AC_add.fold_cong) lemma setsum_cong2: "\\x. x \ A \ f x = g x\ \ setsum f A = setsum g A"; @@ -1704,71 +1705,6 @@ 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) - - subsection{* A fold functional for non-empty sets *} text{* Does not require start value. *} diff -r 1bbe526a552c -r 236dfafbeb63 src/HOL/Fun.thy --- a/src/HOL/Fun.thy Thu Jul 07 12:36:56 2005 +0200 +++ b/src/HOL/Fun.thy Thu Jul 07 12:39:17 2005 +0200 @@ -92,13 +92,16 @@ lemma id_apply [simp]: "id x = x" by (simp add: id_def) -lemma inj_on_id: "inj_on id A" +lemma inj_on_id[simp]: "inj_on id A" by (simp add: inj_on_def) -lemma surj_id: "surj id" +lemma inj_on_id2[simp]: "inj_on (%x. x) A" +by (simp add: inj_on_def) + +lemma surj_id[simp]: "surj id" by (simp add: surj_def) -lemma bij_id: "bij id" +lemma bij_id[simp]: "bij id" by (simp add: bij_def inj_on_id surj_id) diff -r 1bbe526a552c -r 236dfafbeb63 src/HOL/Hoare/Examples.thy --- a/src/HOL/Hoare/Examples.thy Thu Jul 07 12:36:56 2005 +0200 +++ b/src/HOL/Hoare/Examples.thy Thu Jul 07 12:39:17 2005 +0200 @@ -73,7 +73,6 @@ apply vcg apply simp apply(simp add: distribs gcd_diff_r not_less_iff_le gcd_diff_l) - apply arith apply(simp add: distribs gcd_nnn) done @@ -136,7 +135,6 @@ DO r := r+1 OD {r*r <= X & X < (r+1)*(r+1)}" apply vcg_simp -apply auto done (* without multiplication *) @@ -149,7 +147,6 @@ DO r := r + 1; w := w + u + 2; u := u + 2 OD {r*r <= X & X < (r+1)*(r+1)}" apply vcg_simp -apply auto done @@ -231,11 +228,10 @@ apply (simp); apply (erule thin_rl)+ apply vcg_simp - apply (force simp: neq_Nil_conv) - apply (blast elim!: less_SucE intro: Suc_leI) - apply (blast elim!: less_SucE intro: less_imp_diff_less dest: lem) - apply (force simp: nth_list_update) -apply (auto intro: order_antisym) + apply (force simp: neq_Nil_conv) + apply (blast elim!: less_SucE intro: Suc_leI) + apply (blast elim!: less_SucE intro: less_imp_diff_less dest: lem) +apply (force simp: nth_list_update) done end \ No newline at end of file diff -r 1bbe526a552c -r 236dfafbeb63 src/HOL/Hoare/ExamplesAbort.thy --- a/src/HOL/Hoare/ExamplesAbort.thy Thu Jul 07 12:36:56 2005 +0200 +++ b/src/HOL/Hoare/ExamplesAbort.thy Thu Jul 07 12:39:17 2005 +0200 @@ -16,7 +16,6 @@ "VARS a i j {k <= length a & i < k & j < k} j < length a \ a[i] := a!j {True}" apply vcg_simp -apply arith done lemma "VARS (a::int list) i @@ -27,7 +26,6 @@ DO a[i] := 7; i := i+1 OD {True}" apply vcg_simp -apply arith done end diff -r 1bbe526a552c -r 236dfafbeb63 src/HOL/HoareParallel/OG_Examples.thy --- a/src/HOL/HoareParallel/OG_Examples.thy Thu Jul 07 12:36:56 2005 +0200 +++ b/src/HOL/HoareParallel/OG_Examples.thy Thu Jul 07 12:39:17 2005 +0200 @@ -175,12 +175,11 @@ --{* 11 vc *} apply simp_all apply(tactic {* ALLGOALS Clarify_tac *}) ---{* 11 subgoals left *} +--{* 10 subgoals left *} apply(erule less_SucE) apply simp apply simp ---{* 10 subgoals left *} -apply force +--{* 9 subgoals left *} apply(case_tac "i=k") apply force apply simp @@ -443,11 +442,11 @@ apply(simp_all (asm_lr) only:length_0_conv [THEN sym]) --{* 44 subgoals left *} apply (simp_all (asm_lr) del:length_0_conv add: nth_list_update mod_less_divisor mod_lemma) ---{* 33 subgoals left *} +--{* 32 subgoals left *} apply(tactic {* ALLGOALS Clarify_tac *}) apply(tactic {* TRYALL simple_arith_tac *}) ---{* 10 subgoals left *} +--{* 9 subgoals left *} apply (force simp add:less_Suc_eq) apply(drule sym) apply (force simp add:less_Suc_eq)+ @@ -525,10 +524,6 @@ apply simp_all done -lemma Example2_lemma3: "!!b. \i< n. b i = (Suc 0) \ (\i=0.. nat" @@ -544,16 +539,13 @@ COEND .{\x=n}." apply oghoare -apply simp_all +apply (simp_all cong del: strong_setsum_cong) apply (tactic {* ALLGOALS Clarify_tac *}) -apply simp_all - apply(erule Example2_lemma2) - apply simp - apply(erule Example2_lemma2) - apply simp - apply(erule Example2_lemma2) - apply simp -apply(force intro: Example2_lemma3) +apply (simp_all cong del: strong_setsum_cong) + apply(erule (1) Example2_lemma2) + apply(erule (1) Example2_lemma2) + apply(erule (1) Example2_lemma2) +apply(simp) done end diff -r 1bbe526a552c -r 236dfafbeb63 src/HOL/HoareParallel/RG_Examples.thy --- a/src/HOL/HoareParallel/RG_Examples.thy Thu Jul 07 12:36:56 2005 +0200 +++ b/src/HOL/HoareParallel/RG_Examples.thy Thu Jul 07 12:39:17 2005 +0200 @@ -228,7 +228,7 @@ apply simp apply clarify apply simp -apply(force elim:Example2_lemma2_Suc0) +apply(simp add:Example2_lemma2_Suc0 cong:if_cong) apply simp+ done diff -r 1bbe526a552c -r 236dfafbeb63 src/HOL/Hyperreal/Series.thy --- a/src/HOL/Hyperreal/Series.thy Thu Jul 07 12:36:56 2005 +0200 +++ b/src/HOL/Hyperreal/Series.thy Thu Jul 07 12:39:17 2005 +0200 @@ -137,6 +137,10 @@ apply (induct "no", auto) apply (drule_tac x = "Suc no" in spec) apply (simp add: add_ac) +(* FIXME why does simp require a separate step to prove the (pure arithmetic) + left-over? With del cong: strong_setsum_cong it works! +*) +apply simp done diff -r 1bbe526a552c -r 236dfafbeb63 src/HOL/Infinite_Set.thy --- a/src/HOL/Infinite_Set.thy Thu Jul 07 12:36:56 2005 +0200 +++ b/src/HOL/Infinite_Set.thy Thu Jul 07 12:39:17 2005 +0200 @@ -6,7 +6,7 @@ header {* Infnite Sets and Related Concepts*} theory Infinite_Set -imports Hilbert_Choice Finite_Set SetInterval +imports Hilbert_Choice Binomial begin subsection "Infinite Sets" diff -r 1bbe526a552c -r 236dfafbeb63 src/HOL/Integ/IntDef.thy --- a/src/HOL/Integ/IntDef.thy Thu Jul 07 12:36:56 2005 +0200 +++ b/src/HOL/Integ/IntDef.thy Thu Jul 07 12:39:17 2005 +0200 @@ -181,7 +181,7 @@ apply (simp add: congruent_def mult_ac) apply (rename_tac u v w x y z) apply (subgoal_tac "u*y + x*y = w*y + v*y & u*z + x*z = w*z + v*z") -apply (simp add: mult_ac, arith) +apply (simp add: mult_ac) apply (simp add: add_mult_distrib [symmetric]) done diff -r 1bbe526a552c -r 236dfafbeb63 src/HOL/Integ/IntDiv.thy --- a/src/HOL/Integ/IntDiv.thy Thu Jul 07 12:36:56 2005 +0200 +++ b/src/HOL/Integ/IntDiv.thy Thu Jul 07 12:39:17 2005 +0200 @@ -102,7 +102,7 @@ subsection{*Uniqueness and Monotonicity of Quotients and Remainders*} lemma unique_quotient_lemma: - "[| b*q' + r' \ b*q + r; 0 \ r'; 0 < b; r < b |] + "[| b*q' + r' \ b*q + r; 0 \ r'; r' < b; r < b |] ==> q' \ (q::int)" apply (subgoal_tac "r' + b * (q'-q) \ r") prefer 2 apply (simp add: right_diff_distrib) @@ -115,7 +115,7 @@ done lemma unique_quotient_lemma_neg: - "[| b*q' + r' \ b*q + r; r \ 0; b < 0; b < r' |] + "[| b*q' + r' \ b*q + r; r \ 0; b < r; b < r' |] ==> q \ (q'::int)" by (rule_tac b = "-b" and r = "-r'" and r' = "-r" in unique_quotient_lemma, auto) diff -r 1bbe526a552c -r 236dfafbeb63 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Jul 07 12:36:56 2005 +0200 +++ b/src/HOL/IsaMakefile Thu Jul 07 12:39:17 2005 +0200 @@ -78,7 +78,7 @@ $(SRC)/TFL/casesplit.ML $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML \ $(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML \ $(SRC)/TFL/thry.ML $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML \ - Datatype.ML Datatype.thy Datatype_Universe.thy Divides.thy \ + Binomial.thy Datatype.ML Datatype.thy Datatype_Universe.thy Divides.thy \ Equiv_Relations.thy Extraction.thy Finite_Set.ML Finite_Set.thy \ Fun.thy Gfp.thy HOL.ML HOL.thy Hilbert_Choice.thy Inductive.thy \ Infinite_Set.thy Integ/IntArith.thy Integ/IntDef.thy Integ/IntDiv.thy \ diff -r 1bbe526a552c -r 236dfafbeb63 src/HOL/Matrix/Matrix.thy --- a/src/HOL/Matrix/Matrix.thy Thu Jul 07 12:36:56 2005 +0200 +++ b/src/HOL/Matrix/Matrix.thy Thu Jul 07 12:39:17 2005 +0200 @@ -131,7 +131,7 @@ apply (simp add: one_matrix_def) apply (simplesubst RepAbs_matrix) apply (rule exI[of _ n], simp add: split_if)+ -by (simp add: split_if, arith) +by (simp add: split_if) lemma nrows_one_matrix[simp]: "nrows ((one_matrix n) :: ('a::axclass_0_neq_1)matrix) = n" (is "?r = _") proof - diff -r 1bbe526a552c -r 236dfafbeb63 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Thu Jul 07 12:36:56 2005 +0200 +++ b/src/HOL/Nat.thy Thu Jul 07 12:39:17 2005 +0200 @@ -93,7 +93,7 @@ text {* Injectiveness of @{term Suc} *} -lemma inj_Suc: "inj_on Suc N" +lemma inj_Suc[simp]: "inj_on Suc N" by (simp add: Suc_def inj_on_def Abs_Nat_inject Rep_Nat Suc_RepI inj_Suc_Rep [THEN inj_eq] Rep_Nat_inject) @@ -665,6 +665,14 @@ done +lemma inj_on_add_nat[simp]: "inj_on (%n::nat. n+k) N" +apply(induct k) + apply simp +apply(drule comp_inj_on[OF _ inj_Suc]) +apply (simp add:o_def) +done + + subsection {* Multiplication *} text {* right annihilation in product *} diff -r 1bbe526a552c -r 236dfafbeb63 src/HOL/NumberTheory/Euler.thy --- a/src/HOL/NumberTheory/Euler.thy Thu Jul 07 12:36:56 2005 +0200 +++ b/src/HOL/NumberTheory/Euler.thy Thu Jul 07 12:39:17 2005 +0200 @@ -175,7 +175,7 @@ lemma SRStar_d22set_prop [rule_format]: "2 < p --> (SRStar p) = {1} \ (d22set (p - 1))"; apply (induct p rule: d22set.induct, auto) - apply (simp add: SRStar_def d22set.simps, arith) + apply (simp add: SRStar_def d22set.simps) apply (simp add: SRStar_def d22set.simps, clarify) apply (frule aux1) apply (frule aux2, auto) diff -r 1bbe526a552c -r 236dfafbeb63 src/HOL/NumberTheory/EulerFermat.thy --- a/src/HOL/NumberTheory/EulerFermat.thy Thu Jul 07 12:36:56 2005 +0200 +++ b/src/HOL/NumberTheory/EulerFermat.thy Thu Jul 07 12:39:17 2005 +0200 @@ -315,14 +315,11 @@ apply (rule Bnor_fin) done -lemma Bnor_prime [rule_format (no_asm)]: - "zprime p ==> - a < p --> (\b. 0 < b \ b \ a --> zgcd (b, p) = 1) - --> card (BnorRset (a, p)) = nat a" - apply (auto simp add: zless_zprime_imp_zrelprime) +lemma Bnor_prime: + "\ zprime p; a < p \ \ card (BnorRset (a, p)) = nat a" apply (induct a p rule: BnorRset.induct) apply (subst BnorRset.simps) - apply (unfold Let_def, auto) + apply (unfold Let_def, auto simp add:zless_zprime_imp_zrelprime) apply (subgoal_tac "finite (BnorRset (a - 1,m))") apply (subgoal_tac "a ~: BnorRset (a - 1,m)") apply (auto simp add: card_insert_disjoint Suc_nat_eq_nat_zadd1) @@ -333,7 +330,6 @@ lemma phi_prime: "zprime p ==> phi p = nat (p - 1)" apply (unfold phi_def norRRset_def) apply (rule Bnor_prime, auto) - apply (erule zless_zprime_imp_zrelprime, simp_all) done theorem Little_Fermat: diff -r 1bbe526a552c -r 236dfafbeb63 src/HOL/NumberTheory/Gauss.thy --- a/src/HOL/NumberTheory/Gauss.thy Thu Jul 07 12:36:56 2005 +0200 +++ b/src/HOL/NumberTheory/Gauss.thy Thu Jul 07 12:39:17 2005 +0200 @@ -459,8 +459,7 @@ by (simp add: B_def) then have "[setprod id A = ((-1)^(card E) * (setprod (%x. x * a) A))] (mod p)" - apply (rule zcong_trans) - by (simp add: finite_A inj_on_xa_A setprod_reindex_id zcong_scalar2) + by(simp add:finite_A inj_on_xa_A setprod_reindex_id[symmetric]) moreover have "setprod (%x. x * a) A = setprod (%x. a) A * setprod id A" by (insert finite_A, induct set: Finites, auto) diff -r 1bbe526a552c -r 236dfafbeb63 src/HOL/NumberTheory/Quadratic_Reciprocity.thy --- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Thu Jul 07 12:36:56 2005 +0200 +++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Thu Jul 07 12:39:17 2005 +0200 @@ -24,15 +24,13 @@ also have "setsum (%x. a * x) = setsum (%x. x * a)" by (auto simp add: zmult_commute) also have "setsum (%x. x * a) A = setsum id B" - by (auto simp add: B_def setsum_reindex_id finite_A inj_on_xa_A) + by (simp add: B_def setsum_reindex_id[OF inj_on_xa_A]) also have "... = setsum (%x. p * (x div p) + StandardRes p x) B" - apply (rule setsum_cong) - by (auto simp add: finite_B StandardRes_def zmod_zdiv_equality) + by (auto simp add: StandardRes_def zmod_zdiv_equality) also have "... = setsum (%x. p * (x div p)) B + setsum (StandardRes p) B" by (rule setsum_addf) also have "setsum (StandardRes p) B = setsum id C" - by (auto simp add: C_def setsum_reindex_id [THEN sym] finite_B - SR_B_inj) + by (auto simp add: C_def setsum_reindex_id[OF SR_B_inj]) also from C_eq have "... = setsum id (D \ E)" by auto also from finite_D finite_E have "... = setsum id D + setsum id E" @@ -40,7 +38,7 @@ by (auto simp add: D_def E_def) also have "setsum (%x. p * (x div p)) B = setsum ((%x. p * (x div p)) o (%x. (x * a))) A" - by (auto simp add: B_def setsum_reindex finite_A inj_on_xa_A) + by (auto simp add: B_def setsum_reindex inj_on_xa_A) also have "... = setsum (%x. p * ((x * a) div p)) A" by (auto simp add: o_def) also from finite_A have "setsum (%x. p * ((x * a) div p)) A = @@ -588,7 +586,7 @@ from prems have "~([q = 0] (mod p))" apply (rule_tac p = q and q = p in pq_prime_neq) apply (simp add: QRTEMP_def)+ - by arith + done with prems have a2: "(Legendre q p) = (-1::int) ^ nat(setsum (%x. ((x * q) div p)) P_set)" apply (rule_tac p = p in MainQRLemma) diff -r 1bbe526a552c -r 236dfafbeb63 src/HOL/Power.thy --- a/src/HOL/Power.thy Thu Jul 07 12:36:56 2005 +0200 +++ b/src/HOL/Power.thy Thu Jul 07 12:39:17 2005 +0200 @@ -5,7 +5,7 @@ *) -header{*Exponentiation and Binomial Coefficients*} +header{*Exponentiation*} theory Power imports Divides @@ -345,86 +345,6 @@ apply (erule dvd_imp_le, simp) done - -subsection{*Binomial Coefficients*} - -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 (case_tac "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", auto) -apply (erule allE) -apply (erule mp, arith) -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 - text{*ML bindings for the general exponentiation theorems*} ML {* @@ -477,19 +397,6 @@ val nat_zero_less_power_iff = thm"nat_zero_less_power_iff"; val power_le_dvd = thm"power_le_dvd"; val power_dvd_imp_le = thm"power_dvd_imp_le"; -val binomial_n_0 = thm"binomial_n_0"; -val binomial_0_Suc = thm"binomial_0_Suc"; -val binomial_Suc_Suc = thm"binomial_Suc_Suc"; -val binomial_eq_0 = thm"binomial_eq_0"; -val binomial_n_n = thm"binomial_n_n"; -val binomial_Suc_n = thm"binomial_Suc_n"; -val binomial_1 = thm"binomial_1"; -val zero_less_binomial = thm"zero_less_binomial"; -val binomial_eq_0_iff = thm"binomial_eq_0_iff"; -val zero_less_binomial_iff = thm"zero_less_binomial_iff"; -val Suc_times_binomial_eq = thm"Suc_times_binomial_eq"; -val binomial_Suc_Suc_eq_times = thm"binomial_Suc_Suc_eq_times"; -val times_binomial_minus1_eq = thm"times_binomial_minus1_eq"; *} end diff -r 1bbe526a552c -r 236dfafbeb63 src/HOL/SetInterval.thy --- a/src/HOL/SetInterval.thy Thu Jul 07 12:36:56 2005 +0200 +++ b/src/HOL/SetInterval.thy Thu Jul 07 12:39:17 2005 +0200 @@ -300,6 +300,52 @@ lemma atLeastAtMostSuc_conv: "m \ Suc n \ {m..Suc n} = insert (Suc n) {m..n}" by (auto simp add: atLeastAtMost_def) +subsubsection {* Image *} + +lemma image_add_atLeastAtMost: + "(%n::nat. n+k) ` {i..j} = {i+k..j+k}" (is "?A = ?B") +proof + show "?A \ ?B" by auto +next + show "?B \ ?A" + proof + fix n assume a: "n : ?B" + hence "n - k : {i..j}" by auto arith+ + moreover have "n = (n - k) + k" using a by auto + ultimately show "n : ?A" by blast + qed +qed + +lemma image_add_atLeastLessThan: + "(%n::nat. n+k) ` {i.. ?B" by auto +next + show "?B \ ?A" + proof + fix n assume a: "n : ?B" + hence "n - k : {i.. + atomize(thm RS conjunct1) @ atomize(thm RS conjunct2) + | _ => [thm]; + fun neg_prop(TP$(Const("Not",_)$t)) = TP$t | neg_prop(TP$t) = TP $ (Const("Not",HOLogic.boolT-->HOLogic.boolT)$t);