# 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'  \<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]])
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: "\<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. *}
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 \<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
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. \<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
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'  \<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)
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} \<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)
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 --> (\<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:
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 \<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)
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]: "\<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
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 \<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
 {*
diff -r 1bbe526a552c -r 236dfafbeb63 src/HOL/arith_data.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);