linear arithmetic now takes "&" in assumptions apart.
authornipkow
Thu Jul 07 12:39:17 2005 +0200 (2005-07-07)
changeset 16733236dfafbeb63
parent 16732 1bbe526a552c
child 16734 2c76db916c51
linear arithmetic now takes "&" in assumptions apart.
src/HOL/Algebra/Exponent.thy
src/HOL/Divides.thy
src/HOL/Finite_Set.ML
src/HOL/Finite_Set.thy
src/HOL/Fun.thy
src/HOL/Hoare/Examples.thy
src/HOL/Hoare/ExamplesAbort.thy
src/HOL/HoareParallel/OG_Examples.thy
src/HOL/HoareParallel/RG_Examples.thy
src/HOL/Hyperreal/Series.thy
src/HOL/Infinite_Set.thy
src/HOL/Integ/IntDef.thy
src/HOL/Integ/IntDiv.thy
src/HOL/IsaMakefile
src/HOL/Matrix/Matrix.thy
src/HOL/Nat.thy
src/HOL/NumberTheory/Euler.thy
src/HOL/NumberTheory/EulerFermat.thy
src/HOL/NumberTheory/Gauss.thy
src/HOL/NumberTheory/Quadratic_Reciprocity.thy
src/HOL/Power.thy
src/HOL/SetInterval.thy
src/HOL/arith_data.ML
     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