1.1 --- a/src/HOL/Algebra/Exponent.thy Thu Jul 07 12:36:56 2005 +0200
1.2 +++ b/src/HOL/Algebra/Exponent.thy Thu Jul 07 12:39:17 2005 +0200
1.3 @@ -27,7 +27,7 @@
1.4 apply (case_tac "k=0", simp)
1.5 apply (drule_tac x = m in spec)
1.6 apply (drule_tac x = k in spec)
1.7 -apply (simp add: dvd_mult_cancel1 dvd_mult_cancel2, auto)
1.8 +apply (simp add: dvd_mult_cancel1 dvd_mult_cancel2)
1.9 done
1.10
1.11 lemma zero_less_prime_power: "prime p ==> 0 < p^a"
2.1 --- a/src/HOL/Divides.thy Thu Jul 07 12:36:56 2005 +0200
2.2 +++ b/src/HOL/Divides.thy Thu Jul 07 12:39:17 2005 +0200
2.3 @@ -242,7 +242,7 @@
2.4 subsection{*Proving facts about Quotient and Remainder*}
2.5
2.6 lemma unique_quotient_lemma:
2.7 - "[| b*q' + r' \<le> b*q + r; 0 < b; r < b |]
2.8 + "[| b*q' + r' \<le> b*q + r; x < b; r < b |]
2.9 ==> q' \<le> (q::nat)"
2.10 apply (rule leI)
2.11 apply (subst less_iff_Suc_add)
2.12 @@ -254,7 +254,7 @@
2.13 ==> q = q'"
2.14 apply (simp add: split_ifs quorem_def)
2.15 apply (blast intro: order_antisym
2.16 - dest: order_eq_refl [THEN unique_quotient_lemma] sym)+
2.17 + dest: order_eq_refl [THEN unique_quotient_lemma] sym)
2.18 done
2.19
2.20 lemma unique_remainder:
2.21 @@ -702,7 +702,9 @@
2.22 "0 < n \<Longrightarrow> (n * q \<le> m \<and> m < n * (Suc q)) = (q = ((m::nat) div n))"
2.23 apply (rule iffI)
2.24 apply (rule_tac a=m and r = "m - n * q" and r' = "m mod n" in unique_quotient)
2.25 - apply (simp_all add: quorem_def, arith)
2.26 +prefer 3; apply assumption
2.27 + apply (simp_all add: quorem_def)
2.28 + apply arith
2.29 apply (rule conjI)
2.30 apply (rule_tac P="%x. n * (m div n) \<le> x" in
2.31 subst [OF mod_div_equality [of _ n]])
3.1 --- a/src/HOL/Finite_Set.ML Thu Jul 07 12:36:56 2005 +0200
3.2 +++ b/src/HOL/Finite_Set.ML Thu Jul 07 12:39:17 2005 +0200
3.3 @@ -45,10 +45,7 @@
3.4 val card_insert_le = thm "card_insert_le";
3.5 val card_mono = thm "card_mono";
3.6 val card_psubset = thm "card_psubset";
3.7 -val card_s_0_eq_empty = thm "card_s_0_eq_empty";
3.8 val card_seteq = thm "card_seteq";
3.9 -val choose_deconstruct = thm "choose_deconstruct";
3.10 -val constr_bij = thm "constr_bij";
3.11 val Diff1_foldSet = thm "Diff1_foldSet";
3.12 val dvd_partition = thm "dvd_partition";
3.13 val empty_foldSetE = thm "empty_foldSetE";
3.14 @@ -89,8 +86,6 @@
3.15 val fold_insert = thm "ACf.fold_insert";
3.16 val fold_nest_Un_Int = thm "ACf.fold_nest_Un_Int";
3.17 val fold_nest_Un_disjoint = thm "ACf.fold_nest_Un_disjoint";
3.18 -val n_sub_lemma = thm "n_sub_lemma";
3.19 -val n_subsets = thm "n_subsets";
3.20 val psubset_card_mono = thm "psubset_card_mono";
3.21 val setsum_0 = thm "setsum_0";
3.22 val setsum_SucD = thm "setsum_SucD";
4.1 --- a/src/HOL/Finite_Set.thy Thu Jul 07 12:36:56 2005 +0200
4.2 +++ b/src/HOL/Finite_Set.thy Thu Jul 07 12:39:17 2005 +0200
4.3 @@ -891,8 +891,9 @@
4.4 "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
4.5 by(fastsimp simp: setsum_def intro: AC_add.fold_cong)
4.6
4.7 -lemma strong_setsum_cong:
4.8 - "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setsum f A = setsum g B"
4.9 +lemma strong_setsum_cong[cong]:
4.10 + "A = B ==> (!!x. x:B =simp=> f x = g x)
4.11 + ==> setsum (%x. f x) A = setsum (%x. g x) B"
4.12 by(fastsimp simp: simp_implies_def setsum_def intro: AC_add.fold_cong)
4.13
4.14 lemma setsum_cong2: "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setsum f A = setsum g A";
4.15 @@ -1704,71 +1705,6 @@
4.16 done
4.17
4.18
4.19 -subsubsection {* Theorems about @{text "choose"} *}
4.20 -
4.21 -text {*
4.22 - \medskip Basic theorem about @{text "choose"}. By Florian
4.23 - Kamm\"uller, tidied by LCP.
4.24 -*}
4.25 -
4.26 -lemma card_s_0_eq_empty:
4.27 - "finite A ==> card {B. B \<subseteq> A & card B = 0} = 1"
4.28 - apply (simp cong add: conj_cong add: finite_subset [THEN card_0_eq])
4.29 - apply (simp cong add: rev_conj_cong)
4.30 - done
4.31 -
4.32 -lemma choose_deconstruct: "finite M ==> x \<notin> M
4.33 - ==> {s. s <= insert x M & card(s) = Suc k}
4.34 - = {s. s <= M & card(s) = Suc k} Un
4.35 - {s. EX t. t <= M & card(t) = k & s = insert x t}"
4.36 - apply safe
4.37 - apply (auto intro: finite_subset [THEN card_insert_disjoint])
4.38 - apply (drule_tac x = "xa - {x}" in spec)
4.39 - apply (subgoal_tac "x \<notin> xa", auto)
4.40 - apply (erule rev_mp, subst card_Diff_singleton)
4.41 - apply (auto intro: finite_subset)
4.42 - done
4.43 -
4.44 -text{*There are as many subsets of @{term A} having cardinality @{term k}
4.45 - as there are sets obtained from the former by inserting a fixed element
4.46 - @{term x} into each.*}
4.47 -lemma constr_bij:
4.48 - "[|finite A; x \<notin> A|] ==>
4.49 - card {B. EX C. C <= A & card(C) = k & B = insert x C} =
4.50 - card {B. B <= A & card(B) = k}"
4.51 - apply (rule_tac f = "%s. s - {x}" and g = "insert x" in card_bij_eq)
4.52 - apply (auto elim!: equalityE simp add: inj_on_def)
4.53 - apply (subst Diff_insert0, auto)
4.54 - txt {* finiteness of the two sets *}
4.55 - apply (rule_tac [2] B = "Pow (A)" in finite_subset)
4.56 - apply (rule_tac B = "Pow (insert x A)" in finite_subset)
4.57 - apply fast+
4.58 - done
4.59 -
4.60 -text {*
4.61 - Main theorem: combinatorial statement about number of subsets of a set.
4.62 -*}
4.63 -
4.64 -lemma n_sub_lemma:
4.65 - "!!A. finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
4.66 - apply (induct k)
4.67 - apply (simp add: card_s_0_eq_empty, atomize)
4.68 - apply (rotate_tac -1, erule finite_induct)
4.69 - apply (simp_all (no_asm_simp) cong add: conj_cong
4.70 - add: card_s_0_eq_empty choose_deconstruct)
4.71 - apply (subst card_Un_disjoint)
4.72 - prefer 4 apply (force simp add: constr_bij)
4.73 - prefer 3 apply force
4.74 - prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2]
4.75 - finite_subset [of _ "Pow (insert x F)", standard])
4.76 - apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset])
4.77 - done
4.78 -
4.79 -theorem n_subsets:
4.80 - "finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
4.81 - by (simp add: n_sub_lemma)
4.82 -
4.83 -
4.84 subsection{* A fold functional for non-empty sets *}
4.85
4.86 text{* Does not require start value. *}
5.1 --- a/src/HOL/Fun.thy Thu Jul 07 12:36:56 2005 +0200
5.2 +++ b/src/HOL/Fun.thy Thu Jul 07 12:39:17 2005 +0200
5.3 @@ -92,13 +92,16 @@
5.4 lemma id_apply [simp]: "id x = x"
5.5 by (simp add: id_def)
5.6
5.7 -lemma inj_on_id: "inj_on id A"
5.8 +lemma inj_on_id[simp]: "inj_on id A"
5.9 by (simp add: inj_on_def)
5.10
5.11 -lemma surj_id: "surj id"
5.12 +lemma inj_on_id2[simp]: "inj_on (%x. x) A"
5.13 +by (simp add: inj_on_def)
5.14 +
5.15 +lemma surj_id[simp]: "surj id"
5.16 by (simp add: surj_def)
5.17
5.18 -lemma bij_id: "bij id"
5.19 +lemma bij_id[simp]: "bij id"
5.20 by (simp add: bij_def inj_on_id surj_id)
5.21
5.22
6.1 --- a/src/HOL/Hoare/Examples.thy Thu Jul 07 12:36:56 2005 +0200
6.2 +++ b/src/HOL/Hoare/Examples.thy Thu Jul 07 12:39:17 2005 +0200
6.3 @@ -73,7 +73,6 @@
6.4 apply vcg
6.5 apply simp
6.6 apply(simp add: distribs gcd_diff_r not_less_iff_le gcd_diff_l)
6.7 - apply arith
6.8 apply(simp add: distribs gcd_nnn)
6.9 done
6.10
6.11 @@ -136,7 +135,6 @@
6.12 DO r := r+1 OD
6.13 {r*r <= X & X < (r+1)*(r+1)}"
6.14 apply vcg_simp
6.15 -apply auto
6.16 done
6.17
6.18 (* without multiplication *)
6.19 @@ -149,7 +147,6 @@
6.20 DO r := r + 1; w := w + u + 2; u := u + 2 OD
6.21 {r*r <= X & X < (r+1)*(r+1)}"
6.22 apply vcg_simp
6.23 -apply auto
6.24 done
6.25
6.26
6.27 @@ -231,11 +228,10 @@
6.28 apply (simp);
6.29 apply (erule thin_rl)+
6.30 apply vcg_simp
6.31 - apply (force simp: neq_Nil_conv)
6.32 - apply (blast elim!: less_SucE intro: Suc_leI)
6.33 - apply (blast elim!: less_SucE intro: less_imp_diff_less dest: lem)
6.34 - apply (force simp: nth_list_update)
6.35 -apply (auto intro: order_antisym)
6.36 + apply (force simp: neq_Nil_conv)
6.37 + apply (blast elim!: less_SucE intro: Suc_leI)
6.38 + apply (blast elim!: less_SucE intro: less_imp_diff_less dest: lem)
6.39 +apply (force simp: nth_list_update)
6.40 done
6.41
6.42 end
6.43 \ No newline at end of file
7.1 --- a/src/HOL/Hoare/ExamplesAbort.thy Thu Jul 07 12:36:56 2005 +0200
7.2 +++ b/src/HOL/Hoare/ExamplesAbort.thy Thu Jul 07 12:39:17 2005 +0200
7.3 @@ -16,7 +16,6 @@
7.4 "VARS a i j
7.5 {k <= length a & i < k & j < k} j < length a \<rightarrow> a[i] := a!j {True}"
7.6 apply vcg_simp
7.7 -apply arith
7.8 done
7.9
7.10 lemma "VARS (a::int list) i
7.11 @@ -27,7 +26,6 @@
7.12 DO a[i] := 7; i := i+1 OD
7.13 {True}"
7.14 apply vcg_simp
7.15 -apply arith
7.16 done
7.17
7.18 end
8.1 --- a/src/HOL/HoareParallel/OG_Examples.thy Thu Jul 07 12:36:56 2005 +0200
8.2 +++ b/src/HOL/HoareParallel/OG_Examples.thy Thu Jul 07 12:39:17 2005 +0200
8.3 @@ -175,12 +175,11 @@
8.4 --{* 11 vc *}
8.5 apply simp_all
8.6 apply(tactic {* ALLGOALS Clarify_tac *})
8.7 ---{* 11 subgoals left *}
8.8 +--{* 10 subgoals left *}
8.9 apply(erule less_SucE)
8.10 apply simp
8.11 apply simp
8.12 ---{* 10 subgoals left *}
8.13 -apply force
8.14 +--{* 9 subgoals left *}
8.15 apply(case_tac "i=k")
8.16 apply force
8.17 apply simp
8.18 @@ -443,11 +442,11 @@
8.19 apply(simp_all (asm_lr) only:length_0_conv [THEN sym])
8.20 --{* 44 subgoals left *}
8.21 apply (simp_all (asm_lr) del:length_0_conv add: nth_list_update mod_less_divisor mod_lemma)
8.22 ---{* 33 subgoals left *}
8.23 +--{* 32 subgoals left *}
8.24 apply(tactic {* ALLGOALS Clarify_tac *})
8.25
8.26 apply(tactic {* TRYALL simple_arith_tac *})
8.27 ---{* 10 subgoals left *}
8.28 +--{* 9 subgoals left *}
8.29 apply (force simp add:less_Suc_eq)
8.30 apply(drule sym)
8.31 apply (force simp add:less_Suc_eq)+
8.32 @@ -525,10 +524,6 @@
8.33 apply simp_all
8.34 done
8.35
8.36 -lemma Example2_lemma3: "!!b. \<forall>i< n. b i = (Suc 0) \<Longrightarrow> (\<Sum>i=0..<n. b i)= n"
8.37 -apply (induct n)
8.38 -apply auto
8.39 -done
8.40
8.41 record Example2 =
8.42 c :: "nat \<Rightarrow> nat"
8.43 @@ -544,16 +539,13 @@
8.44 COEND
8.45 .{\<acute>x=n}."
8.46 apply oghoare
8.47 -apply simp_all
8.48 +apply (simp_all cong del: strong_setsum_cong)
8.49 apply (tactic {* ALLGOALS Clarify_tac *})
8.50 -apply simp_all
8.51 - apply(erule Example2_lemma2)
8.52 - apply simp
8.53 - apply(erule Example2_lemma2)
8.54 - apply simp
8.55 - apply(erule Example2_lemma2)
8.56 - apply simp
8.57 -apply(force intro: Example2_lemma3)
8.58 +apply (simp_all cong del: strong_setsum_cong)
8.59 + apply(erule (1) Example2_lemma2)
8.60 + apply(erule (1) Example2_lemma2)
8.61 + apply(erule (1) Example2_lemma2)
8.62 +apply(simp)
8.63 done
8.64
8.65 end
9.1 --- a/src/HOL/HoareParallel/RG_Examples.thy Thu Jul 07 12:36:56 2005 +0200
9.2 +++ b/src/HOL/HoareParallel/RG_Examples.thy Thu Jul 07 12:39:17 2005 +0200
9.3 @@ -228,7 +228,7 @@
9.4 apply simp
9.5 apply clarify
9.6 apply simp
9.7 -apply(force elim:Example2_lemma2_Suc0)
9.8 +apply(simp add:Example2_lemma2_Suc0 cong:if_cong)
9.9 apply simp+
9.10 done
9.11
10.1 --- a/src/HOL/Hyperreal/Series.thy Thu Jul 07 12:36:56 2005 +0200
10.2 +++ b/src/HOL/Hyperreal/Series.thy Thu Jul 07 12:39:17 2005 +0200
10.3 @@ -137,6 +137,10 @@
10.4 apply (induct "no", auto)
10.5 apply (drule_tac x = "Suc no" in spec)
10.6 apply (simp add: add_ac)
10.7 +(* FIXME why does simp require a separate step to prove the (pure arithmetic)
10.8 + left-over? With del cong: strong_setsum_cong it works!
10.9 +*)
10.10 +apply simp
10.11 done
10.12
10.13
11.1 --- a/src/HOL/Infinite_Set.thy Thu Jul 07 12:36:56 2005 +0200
11.2 +++ b/src/HOL/Infinite_Set.thy Thu Jul 07 12:39:17 2005 +0200
11.3 @@ -6,7 +6,7 @@
11.4 header {* Infnite Sets and Related Concepts*}
11.5
11.6 theory Infinite_Set
11.7 -imports Hilbert_Choice Finite_Set SetInterval
11.8 +imports Hilbert_Choice Binomial
11.9 begin
11.10
11.11 subsection "Infinite Sets"
12.1 --- a/src/HOL/Integ/IntDef.thy Thu Jul 07 12:36:56 2005 +0200
12.2 +++ b/src/HOL/Integ/IntDef.thy Thu Jul 07 12:39:17 2005 +0200
12.3 @@ -181,7 +181,7 @@
12.4 apply (simp add: congruent_def mult_ac)
12.5 apply (rename_tac u v w x y z)
12.6 apply (subgoal_tac "u*y + x*y = w*y + v*y & u*z + x*z = w*z + v*z")
12.7 -apply (simp add: mult_ac, arith)
12.8 +apply (simp add: mult_ac)
12.9 apply (simp add: add_mult_distrib [symmetric])
12.10 done
12.11
13.1 --- a/src/HOL/Integ/IntDiv.thy Thu Jul 07 12:36:56 2005 +0200
13.2 +++ b/src/HOL/Integ/IntDiv.thy Thu Jul 07 12:39:17 2005 +0200
13.3 @@ -102,7 +102,7 @@
13.4 subsection{*Uniqueness and Monotonicity of Quotients and Remainders*}
13.5
13.6 lemma unique_quotient_lemma:
13.7 - "[| b*q' + r' \<le> b*q + r; 0 \<le> r'; 0 < b; r < b |]
13.8 + "[| b*q' + r' \<le> b*q + r; 0 \<le> r'; r' < b; r < b |]
13.9 ==> q' \<le> (q::int)"
13.10 apply (subgoal_tac "r' + b * (q'-q) \<le> r")
13.11 prefer 2 apply (simp add: right_diff_distrib)
13.12 @@ -115,7 +115,7 @@
13.13 done
13.14
13.15 lemma unique_quotient_lemma_neg:
13.16 - "[| b*q' + r' \<le> b*q + r; r \<le> 0; b < 0; b < r' |]
13.17 + "[| b*q' + r' \<le> b*q + r; r \<le> 0; b < r; b < r' |]
13.18 ==> q \<le> (q'::int)"
13.19 by (rule_tac b = "-b" and r = "-r'" and r' = "-r" in unique_quotient_lemma,
13.20 auto)
14.1 --- a/src/HOL/IsaMakefile Thu Jul 07 12:36:56 2005 +0200
14.2 +++ b/src/HOL/IsaMakefile Thu Jul 07 12:39:17 2005 +0200
14.3 @@ -78,7 +78,7 @@
14.4 $(SRC)/TFL/casesplit.ML $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML \
14.5 $(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML \
14.6 $(SRC)/TFL/thry.ML $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML \
14.7 - Datatype.ML Datatype.thy Datatype_Universe.thy Divides.thy \
14.8 + Binomial.thy Datatype.ML Datatype.thy Datatype_Universe.thy Divides.thy \
14.9 Equiv_Relations.thy Extraction.thy Finite_Set.ML Finite_Set.thy \
14.10 Fun.thy Gfp.thy HOL.ML HOL.thy Hilbert_Choice.thy Inductive.thy \
14.11 Infinite_Set.thy Integ/IntArith.thy Integ/IntDef.thy Integ/IntDiv.thy \
15.1 --- a/src/HOL/Matrix/Matrix.thy Thu Jul 07 12:36:56 2005 +0200
15.2 +++ b/src/HOL/Matrix/Matrix.thy Thu Jul 07 12:39:17 2005 +0200
15.3 @@ -131,7 +131,7 @@
15.4 apply (simp add: one_matrix_def)
15.5 apply (simplesubst RepAbs_matrix)
15.6 apply (rule exI[of _ n], simp add: split_if)+
15.7 -by (simp add: split_if, arith)
15.8 +by (simp add: split_if)
15.9
15.10 lemma nrows_one_matrix[simp]: "nrows ((one_matrix n) :: ('a::axclass_0_neq_1)matrix) = n" (is "?r = _")
15.11 proof -
16.1 --- a/src/HOL/Nat.thy Thu Jul 07 12:36:56 2005 +0200
16.2 +++ b/src/HOL/Nat.thy Thu Jul 07 12:39:17 2005 +0200
16.3 @@ -93,7 +93,7 @@
16.4
16.5 text {* Injectiveness of @{term Suc} *}
16.6
16.7 -lemma inj_Suc: "inj_on Suc N"
16.8 +lemma inj_Suc[simp]: "inj_on Suc N"
16.9 by (simp add: Suc_def inj_on_def Abs_Nat_inject Rep_Nat Suc_RepI
16.10 inj_Suc_Rep [THEN inj_eq] Rep_Nat_inject)
16.11
16.12 @@ -665,6 +665,14 @@
16.13 done
16.14
16.15
16.16 +lemma inj_on_add_nat[simp]: "inj_on (%n::nat. n+k) N"
16.17 +apply(induct k)
16.18 + apply simp
16.19 +apply(drule comp_inj_on[OF _ inj_Suc])
16.20 +apply (simp add:o_def)
16.21 +done
16.22 +
16.23 +
16.24 subsection {* Multiplication *}
16.25
16.26 text {* right annihilation in product *}
17.1 --- a/src/HOL/NumberTheory/Euler.thy Thu Jul 07 12:36:56 2005 +0200
17.2 +++ b/src/HOL/NumberTheory/Euler.thy Thu Jul 07 12:39:17 2005 +0200
17.3 @@ -175,7 +175,7 @@
17.4 lemma SRStar_d22set_prop [rule_format]: "2 < p --> (SRStar p) = {1} \<union>
17.5 (d22set (p - 1))";
17.6 apply (induct p rule: d22set.induct, auto)
17.7 - apply (simp add: SRStar_def d22set.simps, arith)
17.8 + apply (simp add: SRStar_def d22set.simps)
17.9 apply (simp add: SRStar_def d22set.simps, clarify)
17.10 apply (frule aux1)
17.11 apply (frule aux2, auto)
18.1 --- a/src/HOL/NumberTheory/EulerFermat.thy Thu Jul 07 12:36:56 2005 +0200
18.2 +++ b/src/HOL/NumberTheory/EulerFermat.thy Thu Jul 07 12:39:17 2005 +0200
18.3 @@ -315,14 +315,11 @@
18.4 apply (rule Bnor_fin)
18.5 done
18.6
18.7 -lemma Bnor_prime [rule_format (no_asm)]:
18.8 - "zprime p ==>
18.9 - a < p --> (\<forall>b. 0 < b \<and> b \<le> a --> zgcd (b, p) = 1)
18.10 - --> card (BnorRset (a, p)) = nat a"
18.11 - apply (auto simp add: zless_zprime_imp_zrelprime)
18.12 +lemma Bnor_prime:
18.13 + "\<lbrakk> zprime p; a < p \<rbrakk> \<Longrightarrow> card (BnorRset (a, p)) = nat a"
18.14 apply (induct a p rule: BnorRset.induct)
18.15 apply (subst BnorRset.simps)
18.16 - apply (unfold Let_def, auto)
18.17 + apply (unfold Let_def, auto simp add:zless_zprime_imp_zrelprime)
18.18 apply (subgoal_tac "finite (BnorRset (a - 1,m))")
18.19 apply (subgoal_tac "a ~: BnorRset (a - 1,m)")
18.20 apply (auto simp add: card_insert_disjoint Suc_nat_eq_nat_zadd1)
18.21 @@ -333,7 +330,6 @@
18.22 lemma phi_prime: "zprime p ==> phi p = nat (p - 1)"
18.23 apply (unfold phi_def norRRset_def)
18.24 apply (rule Bnor_prime, auto)
18.25 - apply (erule zless_zprime_imp_zrelprime, simp_all)
18.26 done
18.27
18.28 theorem Little_Fermat:
19.1 --- a/src/HOL/NumberTheory/Gauss.thy Thu Jul 07 12:36:56 2005 +0200
19.2 +++ b/src/HOL/NumberTheory/Gauss.thy Thu Jul 07 12:39:17 2005 +0200
19.3 @@ -459,8 +459,7 @@
19.4 by (simp add: B_def)
19.5 then have "[setprod id A = ((-1)^(card E) * (setprod (%x. x * a) A))]
19.6 (mod p)"
19.7 - apply (rule zcong_trans)
19.8 - by (simp add: finite_A inj_on_xa_A setprod_reindex_id zcong_scalar2)
19.9 + by(simp add:finite_A inj_on_xa_A setprod_reindex_id[symmetric])
19.10 moreover have "setprod (%x. x * a) A =
19.11 setprod (%x. a) A * setprod id A"
19.12 by (insert finite_A, induct set: Finites, auto)
20.1 --- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Thu Jul 07 12:36:56 2005 +0200
20.2 +++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Thu Jul 07 12:39:17 2005 +0200
20.3 @@ -24,15 +24,13 @@
20.4 also have "setsum (%x. a * x) = setsum (%x. x * a)"
20.5 by (auto simp add: zmult_commute)
20.6 also have "setsum (%x. x * a) A = setsum id B"
20.7 - by (auto simp add: B_def setsum_reindex_id finite_A inj_on_xa_A)
20.8 + by (simp add: B_def setsum_reindex_id[OF inj_on_xa_A])
20.9 also have "... = setsum (%x. p * (x div p) + StandardRes p x) B"
20.10 - apply (rule setsum_cong)
20.11 - by (auto simp add: finite_B StandardRes_def zmod_zdiv_equality)
20.12 + by (auto simp add: StandardRes_def zmod_zdiv_equality)
20.13 also have "... = setsum (%x. p * (x div p)) B + setsum (StandardRes p) B"
20.14 by (rule setsum_addf)
20.15 also have "setsum (StandardRes p) B = setsum id C"
20.16 - by (auto simp add: C_def setsum_reindex_id [THEN sym] finite_B
20.17 - SR_B_inj)
20.18 + by (auto simp add: C_def setsum_reindex_id[OF SR_B_inj])
20.19 also from C_eq have "... = setsum id (D \<union> E)"
20.20 by auto
20.21 also from finite_D finite_E have "... = setsum id D + setsum id E"
20.22 @@ -40,7 +38,7 @@
20.23 by (auto simp add: D_def E_def)
20.24 also have "setsum (%x. p * (x div p)) B =
20.25 setsum ((%x. p * (x div p)) o (%x. (x * a))) A"
20.26 - by (auto simp add: B_def setsum_reindex finite_A inj_on_xa_A)
20.27 + by (auto simp add: B_def setsum_reindex inj_on_xa_A)
20.28 also have "... = setsum (%x. p * ((x * a) div p)) A"
20.29 by (auto simp add: o_def)
20.30 also from finite_A have "setsum (%x. p * ((x * a) div p)) A =
20.31 @@ -588,7 +586,7 @@
20.32 from prems have "~([q = 0] (mod p))"
20.33 apply (rule_tac p = q and q = p in pq_prime_neq)
20.34 apply (simp add: QRTEMP_def)+
20.35 - by arith
20.36 + done
20.37 with prems have a2: "(Legendre q p) =
20.38 (-1::int) ^ nat(setsum (%x. ((x * q) div p)) P_set)"
20.39 apply (rule_tac p = p in MainQRLemma)
21.1 --- a/src/HOL/Power.thy Thu Jul 07 12:36:56 2005 +0200
21.2 +++ b/src/HOL/Power.thy Thu Jul 07 12:39:17 2005 +0200
21.3 @@ -5,7 +5,7 @@
21.4
21.5 *)
21.6
21.7 -header{*Exponentiation and Binomial Coefficients*}
21.8 +header{*Exponentiation*}
21.9
21.10 theory Power
21.11 imports Divides
21.12 @@ -345,86 +345,6 @@
21.13 apply (erule dvd_imp_le, simp)
21.14 done
21.15
21.16 -
21.17 -subsection{*Binomial Coefficients*}
21.18 -
21.19 -text{*This development is based on the work of Andy Gordon and
21.20 -Florian Kammueller*}
21.21 -
21.22 -consts
21.23 - binomial :: "[nat,nat] => nat" (infixl "choose" 65)
21.24 -
21.25 -primrec
21.26 - binomial_0: "(0 choose k) = (if k = 0 then 1 else 0)"
21.27 -
21.28 - binomial_Suc: "(Suc n choose k) =
21.29 - (if k = 0 then 1 else (n choose (k - 1)) + (n choose k))"
21.30 -
21.31 -lemma binomial_n_0 [simp]: "(n choose 0) = 1"
21.32 -by (case_tac "n", simp_all)
21.33 -
21.34 -lemma binomial_0_Suc [simp]: "(0 choose Suc k) = 0"
21.35 -by simp
21.36 -
21.37 -lemma binomial_Suc_Suc [simp]:
21.38 - "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)"
21.39 -by simp
21.40 -
21.41 -lemma binomial_eq_0 [rule_format]: "\<forall>k. n < k --> (n choose k) = 0"
21.42 -apply (induct "n", auto)
21.43 -apply (erule allE)
21.44 -apply (erule mp, arith)
21.45 -done
21.46 -
21.47 -declare binomial_0 [simp del] binomial_Suc [simp del]
21.48 -
21.49 -lemma binomial_n_n [simp]: "(n choose n) = 1"
21.50 -apply (induct "n")
21.51 -apply (simp_all add: binomial_eq_0)
21.52 -done
21.53 -
21.54 -lemma binomial_Suc_n [simp]: "(Suc n choose n) = Suc n"
21.55 -by (induct "n", simp_all)
21.56 -
21.57 -lemma binomial_1 [simp]: "(n choose Suc 0) = n"
21.58 -by (induct "n", simp_all)
21.59 -
21.60 -lemma zero_less_binomial [rule_format]: "k \<le> n --> 0 < (n choose k)"
21.61 -by (rule_tac m = n and n = k in diff_induct, simp_all)
21.62 -
21.63 -lemma binomial_eq_0_iff: "(n choose k = 0) = (n<k)"
21.64 -apply (safe intro!: binomial_eq_0)
21.65 -apply (erule contrapos_pp)
21.66 -apply (simp add: zero_less_binomial)
21.67 -done
21.68 -
21.69 -lemma zero_less_binomial_iff: "(0 < n choose k) = (k\<le>n)"
21.70 -by (simp add: linorder_not_less [symmetric] binomial_eq_0_iff [symmetric])
21.71 -
21.72 -(*Might be more useful if re-oriented*)
21.73 -lemma Suc_times_binomial_eq [rule_format]:
21.74 - "\<forall>k. k \<le> n --> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k"
21.75 -apply (induct "n")
21.76 -apply (simp add: binomial_0, clarify)
21.77 -apply (case_tac "k")
21.78 -apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq
21.79 - binomial_eq_0)
21.80 -done
21.81 -
21.82 -text{*This is the well-known version, but it's harder to use because of the
21.83 - need to reason about division.*}
21.84 -lemma binomial_Suc_Suc_eq_times:
21.85 - "k \<le> n ==> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k"
21.86 -by (simp add: Suc_times_binomial_eq div_mult_self_is_m zero_less_Suc
21.87 - del: mult_Suc mult_Suc_right)
21.88 -
21.89 -text{*Another version, with -1 instead of Suc.*}
21.90 -lemma times_binomial_minus1_eq:
21.91 - "[|k \<le> n; 0<k|] ==> (n choose k) * k = n * ((n - 1) choose (k - 1))"
21.92 -apply (cut_tac n = "n - 1" and k = "k - 1" in Suc_times_binomial_eq)
21.93 -apply (simp split add: nat_diff_split, auto)
21.94 -done
21.95 -
21.96 text{*ML bindings for the general exponentiation theorems*}
21.97 ML
21.98 {*
21.99 @@ -477,19 +397,6 @@
21.100 val nat_zero_less_power_iff = thm"nat_zero_less_power_iff";
21.101 val power_le_dvd = thm"power_le_dvd";
21.102 val power_dvd_imp_le = thm"power_dvd_imp_le";
21.103 -val binomial_n_0 = thm"binomial_n_0";
21.104 -val binomial_0_Suc = thm"binomial_0_Suc";
21.105 -val binomial_Suc_Suc = thm"binomial_Suc_Suc";
21.106 -val binomial_eq_0 = thm"binomial_eq_0";
21.107 -val binomial_n_n = thm"binomial_n_n";
21.108 -val binomial_Suc_n = thm"binomial_Suc_n";
21.109 -val binomial_1 = thm"binomial_1";
21.110 -val zero_less_binomial = thm"zero_less_binomial";
21.111 -val binomial_eq_0_iff = thm"binomial_eq_0_iff";
21.112 -val zero_less_binomial_iff = thm"zero_less_binomial_iff";
21.113 -val Suc_times_binomial_eq = thm"Suc_times_binomial_eq";
21.114 -val binomial_Suc_Suc_eq_times = thm"binomial_Suc_Suc_eq_times";
21.115 -val times_binomial_minus1_eq = thm"times_binomial_minus1_eq";
21.116 *}
21.117
21.118 end
22.1 --- a/src/HOL/SetInterval.thy Thu Jul 07 12:36:56 2005 +0200
22.2 +++ b/src/HOL/SetInterval.thy Thu Jul 07 12:39:17 2005 +0200
22.3 @@ -300,6 +300,52 @@
22.4 lemma atLeastAtMostSuc_conv: "m \<le> Suc n \<Longrightarrow> {m..Suc n} = insert (Suc n) {m..n}"
22.5 by (auto simp add: atLeastAtMost_def)
22.6
22.7 +subsubsection {* Image *}
22.8 +
22.9 +lemma image_add_atLeastAtMost:
22.10 + "(%n::nat. n+k) ` {i..j} = {i+k..j+k}" (is "?A = ?B")
22.11 +proof
22.12 + show "?A \<subseteq> ?B" by auto
22.13 +next
22.14 + show "?B \<subseteq> ?A"
22.15 + proof
22.16 + fix n assume a: "n : ?B"
22.17 + hence "n - k : {i..j}" by auto arith+
22.18 + moreover have "n = (n - k) + k" using a by auto
22.19 + ultimately show "n : ?A" by blast
22.20 + qed
22.21 +qed
22.22 +
22.23 +lemma image_add_atLeastLessThan:
22.24 + "(%n::nat. n+k) ` {i..<j} = {i+k..<j+k}" (is "?A = ?B")
22.25 +proof
22.26 + show "?A \<subseteq> ?B" by auto
22.27 +next
22.28 + show "?B \<subseteq> ?A"
22.29 + proof
22.30 + fix n assume a: "n : ?B"
22.31 + hence "n - k : {i..<j}" by auto arith+
22.32 + moreover have "n = (n - k) + k" using a by auto
22.33 + ultimately show "n : ?A" by blast
22.34 + qed
22.35 +qed
22.36 +
22.37 +corollary image_Suc_atLeastAtMost[simp]:
22.38 + "Suc ` {i..j} = {Suc i..Suc j}"
22.39 +using image_add_atLeastAtMost[where k=1] by simp
22.40 +
22.41 +corollary image_Suc_atLeastLessThan[simp]:
22.42 + "Suc ` {i..<j} = {Suc i..<Suc j}"
22.43 +using image_add_atLeastLessThan[where k=1] by simp
22.44 +
22.45 +lemma image_add_int_atLeastLessThan:
22.46 + "(%x. x + (l::int)) ` {0..<u-l} = {l..<u}"
22.47 + apply (auto simp add: image_def)
22.48 + apply (rule_tac x = "x - l" in bexI)
22.49 + apply auto
22.50 + done
22.51 +
22.52 +
22.53 subsubsection {* Finiteness *}
22.54
22.55 lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..<k}"
22.56 @@ -390,19 +436,12 @@
22.57 apply auto
22.58 done
22.59
22.60 -lemma image_atLeastLessThan_int_shift:
22.61 - "(%x. x + (l::int)) ` {0..<u-l} = {l..<u}"
22.62 - apply (auto simp add: image_def)
22.63 - apply (rule_tac x = "x - l" in bexI)
22.64 - apply auto
22.65 - done
22.66 -
22.67 lemma finite_atLeastLessThan_int [iff]: "finite {l..<u::int}"
22.68 apply (subgoal_tac "(%x. x + l) ` {0..<u-l} = {l..<u}")
22.69 apply (erule subst)
22.70 apply (rule finite_imageI)
22.71 apply (rule finite_atLeastZeroLessThan_int)
22.72 - apply (rule image_atLeastLessThan_int_shift)
22.73 + apply (rule image_add_int_atLeastLessThan)
22.74 done
22.75
22.76 lemma finite_atLeastAtMost_int [iff]: "finite {l..(u::int)}"
22.77 @@ -430,7 +469,7 @@
22.78 apply (erule subst)
22.79 apply (rule card_image)
22.80 apply (simp add: inj_on_def)
22.81 - apply (rule image_atLeastLessThan_int_shift)
22.82 + apply (rule image_add_int_atLeastLessThan)
22.83 done
22.84
22.85 lemma card_atLeastAtMost_int [simp]: "card {l..u} = nat (u - l + 1)"
22.86 @@ -607,8 +646,6 @@
22.87 not provide all lemmas available for @{term"{m..<n}"} also in the
22.88 special form for @{term"{..<n}"}. *}
22.89
22.90 -(* FIXME change the simplifier's treatment of congruence rules?? *)
22.91 -
22.92 text{* This congruence rule should be used for sums over intervals as
22.93 the standard theorem @{text[source]setsum_cong} does not work well
22.94 with the simplifier who adds the unsimplified premise @{term"x:B"} to
22.95 @@ -652,10 +689,26 @@
22.96 apply (simp add: add_ac)
22.97 done
22.98
22.99 +subsection{* Shifting bounds *}
22.100 +
22.101 lemma setsum_shift_bounds_nat_ivl:
22.102 "setsum f {m+k..<n+k} = setsum (%i. f(i + k)){m..<n::nat}"
22.103 by (induct "n", auto simp:atLeastLessThanSuc)
22.104
22.105 +lemma setsum_shift_bounds_cl_nat_ivl:
22.106 + "setsum f {m+k..n+k} = setsum (%i. f(i + k)){m..n::nat}"
22.107 +apply (insert setsum_reindex[OF inj_on_add_nat, where h=f and B = "{m..n}"])
22.108 +apply (simp add:image_add_atLeastAtMost o_def)
22.109 +done
22.110 +
22.111 +corollary setsum_shift_bounds_cl_Suc_ivl:
22.112 + "setsum f {Suc m..Suc n} = setsum (%i. f(Suc i)){m..n}"
22.113 +by (simp add:setsum_shift_bounds_cl_nat_ivl[where k=1,simplified])
22.114 +
22.115 +corollary setsum_shift_bounds_Suc_ivl:
22.116 + "setsum f {Suc m..<Suc n} = setsum (%i. f(Suc i)){m..<n}"
22.117 +by (simp add:setsum_shift_bounds_nat_ivl[where k=1,simplified])
22.118 +
22.119
22.120 ML
22.121 {*
23.1 --- a/src/HOL/arith_data.ML Thu Jul 07 12:36:56 2005 +0200
23.2 +++ b/src/HOL/arith_data.ML Thu Jul 07 12:39:17 2005 +0200
23.3 @@ -183,6 +183,11 @@
23.4
23.5 val mk_Trueprop = HOLogic.mk_Trueprop;
23.6
23.7 +fun atomize thm = case #prop(rep_thm thm) of
23.8 + Const("Trueprop",_) $ (Const("op &",_) $ _ $ _) =>
23.9 + atomize(thm RS conjunct1) @ atomize(thm RS conjunct2)
23.10 + | _ => [thm];
23.11 +
23.12 fun neg_prop(TP$(Const("Not",_)$t)) = TP$t
23.13 | neg_prop(TP$t) = TP $ (Const("Not",HOLogic.boolT-->HOLogic.boolT)$t);
23.14