linear arithmetic now takes "&" in assumptions apart.
--- 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"
--- 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' \<le> b*q + r; 0 < b; r < b |]
+ "[| b*q' + r' \<le> b*q + r; x < b; r < b |]
==> q' \<le> (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 \<Longrightarrow> (n * q \<le> m \<and> 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) \<le> x" in
subst [OF mod_div_equality [of _ n]])
--- 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";
--- 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: "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> 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 \<subseteq> 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 \<notin> 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 \<notin> 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 \<notin> 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. *}
--- 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)
--- 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
--- 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 \<rightarrow> 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
--- 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. \<forall>i< n. b i = (Suc 0) \<Longrightarrow> (\<Sum>i=0..<n. b i)= n"
-apply (induct n)
-apply auto
-done
record Example2 =
c :: "nat \<Rightarrow> nat"
@@ -544,16 +539,13 @@
COEND
.{\<acute>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
--- 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
--- 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
--- 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"
--- 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
--- 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' \<le> b*q + r; 0 \<le> r'; 0 < b; r < b |]
+ "[| b*q' + r' \<le> b*q + r; 0 \<le> r'; r' < b; r < b |]
==> q' \<le> (q::int)"
apply (subgoal_tac "r' + b * (q'-q) \<le> r")
prefer 2 apply (simp add: right_diff_distrib)
@@ -115,7 +115,7 @@
done
lemma unique_quotient_lemma_neg:
- "[| b*q' + r' \<le> b*q + r; r \<le> 0; b < 0; b < r' |]
+ "[| b*q' + r' \<le> b*q + r; r \<le> 0; b < r; b < r' |]
==> q \<le> (q'::int)"
by (rule_tac b = "-b" and r = "-r'" and r' = "-r" in unique_quotient_lemma,
auto)
--- 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 \
--- 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 -
--- 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 *}
--- 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} \<union>
(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)
--- 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 --> (\<forall>b. 0 < b \<and> b \<le> a --> zgcd (b, p) = 1)
- --> card (BnorRset (a, p)) = nat a"
- apply (auto simp add: zless_zprime_imp_zrelprime)
+lemma Bnor_prime:
+ "\<lbrakk> zprime p; a < p \<rbrakk> \<Longrightarrow> 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:
--- 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)
--- 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 \<union> 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)
--- 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]: "\<forall>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 \<le> 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) = (n<k)"
-apply (safe intro!: binomial_eq_0)
-apply (erule contrapos_pp)
-apply (simp add: zero_less_binomial)
-done
-
-lemma zero_less_binomial_iff: "(0 < n choose k) = (k\<le>n)"
-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]:
- "\<forall>k. k \<le> 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 \<le> 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 \<le> n; 0<k|] ==> (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
--- 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 \<le> Suc n \<Longrightarrow> {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 \<subseteq> ?B" by auto
+next
+ show "?B \<subseteq> ?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..<j} = {i+k..<j+k}" (is "?A = ?B")
+proof
+ show "?A \<subseteq> ?B" by auto
+next
+ show "?B \<subseteq> ?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
+
+corollary image_Suc_atLeastAtMost[simp]:
+ "Suc ` {i..j} = {Suc i..Suc j}"
+using image_add_atLeastAtMost[where k=1] by simp
+
+corollary image_Suc_atLeastLessThan[simp]:
+ "Suc ` {i..<j} = {Suc i..<Suc j}"
+using image_add_atLeastLessThan[where k=1] by simp
+
+lemma image_add_int_atLeastLessThan:
+ "(%x. x + (l::int)) ` {0..<u-l} = {l..<u}"
+ apply (auto simp add: image_def)
+ apply (rule_tac x = "x - l" in bexI)
+ apply auto
+ done
+
+
subsubsection {* Finiteness *}
lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..<k}"
@@ -390,19 +436,12 @@
apply auto
done
-lemma image_atLeastLessThan_int_shift:
- "(%x. x + (l::int)) ` {0..<u-l} = {l..<u}"
- apply (auto simp add: image_def)
- apply (rule_tac x = "x - l" in bexI)
- apply auto
- done
-
lemma finite_atLeastLessThan_int [iff]: "finite {l..<u::int}"
apply (subgoal_tac "(%x. x + l) ` {0..<u-l} = {l..<u}")
apply (erule subst)
apply (rule finite_imageI)
apply (rule finite_atLeastZeroLessThan_int)
- apply (rule image_atLeastLessThan_int_shift)
+ apply (rule image_add_int_atLeastLessThan)
done
lemma finite_atLeastAtMost_int [iff]: "finite {l..(u::int)}"
@@ -430,7 +469,7 @@
apply (erule subst)
apply (rule card_image)
apply (simp add: inj_on_def)
- apply (rule image_atLeastLessThan_int_shift)
+ apply (rule image_add_int_atLeastLessThan)
done
lemma card_atLeastAtMost_int [simp]: "card {l..u} = nat (u - l + 1)"
@@ -607,8 +646,6 @@
not provide all lemmas available for @{term"{m..<n}"} also in the
special form for @{term"{..<n}"}. *}
-(* FIXME change the simplifier's treatment of congruence rules?? *)
-
text{* This congruence rule should be used for sums over intervals as
the standard theorem @{text[source]setsum_cong} does not work well
with the simplifier who adds the unsimplified premise @{term"x:B"} to
@@ -652,10 +689,26 @@
apply (simp add: add_ac)
done
+subsection{* Shifting bounds *}
+
lemma setsum_shift_bounds_nat_ivl:
"setsum f {m+k..<n+k} = setsum (%i. f(i + k)){m..<n::nat}"
by (induct "n", auto simp:atLeastLessThanSuc)
+lemma setsum_shift_bounds_cl_nat_ivl:
+ "setsum f {m+k..n+k} = setsum (%i. f(i + k)){m..n::nat}"
+apply (insert setsum_reindex[OF inj_on_add_nat, where h=f and B = "{m..n}"])
+apply (simp add:image_add_atLeastAtMost o_def)
+done
+
+corollary setsum_shift_bounds_cl_Suc_ivl:
+ "setsum f {Suc m..Suc n} = setsum (%i. f(Suc i)){m..n}"
+by (simp add:setsum_shift_bounds_cl_nat_ivl[where k=1,simplified])
+
+corollary setsum_shift_bounds_Suc_ivl:
+ "setsum f {Suc m..<Suc n} = setsum (%i. f(Suc i)){m..<n}"
+by (simp add:setsum_shift_bounds_nat_ivl[where k=1,simplified])
+
ML
{*
--- a/src/HOL/arith_data.ML Thu Jul 07 12:36:56 2005 +0200
+++ b/src/HOL/arith_data.ML Thu Jul 07 12:39:17 2005 +0200
@@ -183,6 +183,11 @@
val mk_Trueprop = HOLogic.mk_Trueprop;
+fun atomize thm = case #prop(rep_thm thm) of
+ Const("Trueprop",_) $ (Const("op &",_) $ _ $ _) =>
+ 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);