--- a/src/HOL/Algebra/Exponent.thy Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Algebra/Exponent.thy Tue Oct 23 23:27:23 2007 +0200
@@ -100,7 +100,7 @@
done
(*An upper bound for the n such that p^n dvd a: needed for GREATEST to exist*)
-lemma power_dvd_bound: "[|p^n dvd a; Suc 0 < p; a \<noteq> 0|] ==> n < a"
+lemma power_dvd_bound: "[|p^n dvd a; Suc 0 < p; a > 0|] ==> n < a"
apply (drule dvd_imp_le)
apply (drule_tac [2] n = n in Suc_le_power, auto)
done
@@ -115,7 +115,7 @@
apply (blast dest: prime_imp_one_less power_dvd_bound)
done
-lemma power_exponent_dvd: "s\<noteq>0 ==> (p ^ exponent p s) dvd s"
+lemma power_exponent_dvd: "s>0 ==> (p ^ exponent p s) dvd s"
apply (simp add: exponent_def)
apply clarify
apply (rule_tac k = 0 in GreatestI)
@@ -145,7 +145,7 @@
(* exponent_mult_add, easy inclusion. Could weaken p \<in> prime to Suc 0 < p *)
-lemma exponent_mult_add1: "[| a \<noteq> 0; b \<noteq> 0 |]
+lemma exponent_mult_add1: "[| a > 0; b > 0 |]
==> (exponent p a) + (exponent p b) <= exponent p (a * b)"
apply (case_tac "prime p")
apply (rule exponent_ge)
@@ -154,7 +154,7 @@
done
(* exponent_mult_add, opposite inclusion *)
-lemma exponent_mult_add2: "[| a \<noteq> 0; b \<noteq> 0 |]
+lemma exponent_mult_add2: "[| a > 0; b > 0 |]
==> exponent p (a * b) <= (exponent p a) + (exponent p b)"
apply (case_tac "prime p")
apply (rule leI, clarify)
@@ -168,7 +168,7 @@
apply (blast dest: power_Suc_exponent_Not_dvd)
done
-lemma exponent_mult_add: "[| a \<noteq> 0; b \<noteq> 0 |]
+lemma exponent_mult_add: "[| a > 0; b > 0 |]
==> exponent p (a * b) = (exponent p a) + (exponent p b)"
by (blast intro: exponent_mult_add1 exponent_mult_add2 order_antisym)
@@ -188,14 +188,14 @@
subsection{*Main Combinatorial Argument*}
-lemma le_extend_mult: "[| c \<noteq> 0; a <= b |] ==> a <= b * (c::nat)"
+lemma le_extend_mult: "[| c > 0; a <= b |] ==> a <= b * (c::nat)"
apply (rule_tac P = "%x. x <= b * c" in subst)
apply (rule mult_1_right)
apply (rule mult_le_mono, auto)
done
lemma p_fac_forw_lemma:
- "[| (m::nat) \<noteq> 0; k \<noteq> 0; k < p^a; (p^r) dvd (p^a)* m - k |] ==> r <= a"
+ "[| (m::nat) > 0; k > 0; k < p^a; (p^r) dvd (p^a)* m - k |] ==> r <= a"
apply (rule notnotD)
apply (rule notI)
apply (drule contrapos_nn [OF _ leI, THEN notnotD], assumption)
@@ -205,7 +205,7 @@
apply(metis dvd_diffD1 dvd_triv_right le_extend_mult linorder_linear linorder_not_less mult_commute nat_dvd_not_less neq0_conv)
done
-lemma p_fac_forw: "[| (m::nat) \<noteq> 0; k\<noteq>0; k < p^a; (p^r) dvd (p^a)* m - k |]
+lemma p_fac_forw: "[| (m::nat) > 0; k>0; k < p^a; (p^r) dvd (p^a)* m - k |]
==> (p^r) dvd (p^a) - k"
apply (frule_tac k1 = k and i = p in p_fac_forw_lemma [THEN le_imp_power_dvd], auto)
apply (subgoal_tac "p^r dvd p^a*m")
@@ -213,15 +213,15 @@
apply (drule dvd_diffD1)
apply assumption
prefer 2 apply (blast intro: dvd_diff)
-apply (drule not0_implies_Suc, auto)
+apply (drule gr0_implies_Suc, auto)
done
lemma r_le_a_forw:
- "[| (k::nat) \<noteq> 0; k < p^a; p\<noteq>0; (p^r) dvd (p^a) - k |] ==> r <= a"
+ "[| (k::nat) > 0; k < p^a; p>0; (p^r) dvd (p^a) - k |] ==> r <= a"
by (rule_tac m = "Suc 0" in p_fac_forw_lemma, auto)
-lemma p_fac_backw: "[| m\<noteq>0; k\<noteq>0; (p::nat)\<noteq>0; k < p^a; (p^r) dvd p^a - k |]
+lemma p_fac_backw: "[| m>0; k>0; (p::nat)\<noteq>0; k < p^a; (p^r) dvd p^a - k |]
==> (p^r) dvd (p^a)*m - k"
apply (frule_tac k1 = k and i = p in r_le_a_forw [THEN le_imp_power_dvd], auto)
apply (subgoal_tac "p^r dvd p^a*m")
@@ -232,7 +232,7 @@
apply (drule less_imp_Suc_add, auto)
done
-lemma exponent_p_a_m_k_equation: "[| m\<noteq>0; k\<noteq>0; (p::nat)\<noteq>0; k < p^a |]
+lemma exponent_p_a_m_k_equation: "[| m>0; k>0; (p::nat)\<noteq>0; k < p^a |]
==> exponent p (p^a * m - k) = exponent p (p^a - k)"
apply (blast intro: exponent_equalityI p_fac_forw p_fac_backw)
done
@@ -249,7 +249,7 @@
apply (induct_tac "k")
apply (simp (no_asm))
(*induction step*)
-apply (subgoal_tac "(Suc (j+n) choose Suc n) \<noteq> 0")
+apply (subgoal_tac "(Suc (j+n) choose Suc n) > 0")
prefer 2 apply (simp add: zero_less_binomial_iff, clarify)
apply (subgoal_tac "exponent p ((Suc (j+n) choose Suc n) * Suc n) =
exponent p (Suc n)")
@@ -278,7 +278,7 @@
lemma const_p_fac_right:
- "m\<noteq>0 ==> exponent p ((p^a * m - Suc 0) choose (p^a - Suc 0)) = 0"
+ "m>0 ==> exponent p ((p^a * m - Suc 0) choose (p^a - Suc 0)) = 0"
apply (case_tac "prime p")
prefer 2 apply simp
apply (frule_tac a = a in zero_less_prime_power)
@@ -296,7 +296,7 @@
done
lemma const_p_fac:
- "m\<noteq>0 ==> exponent p (((p^a) * m) choose p^a) = exponent p m"
+ "m>0 ==> exponent p (((p^a) * m) choose p^a) = exponent p m"
apply (case_tac "prime p")
prefer 2 apply simp
apply (subgoal_tac "0 < p^a * m & p^a <= p^a * m")
--- a/src/HOL/Algebra/Sylow.thy Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Algebra/Sylow.thy Tue Oct 23 23:27:23 2007 +0200
@@ -126,7 +126,7 @@
apply (blast intro: one_closed zero_less_card_empty)
done
-lemma (in sylow) zero_less_m: "m \<noteq> 0"
+lemma (in sylow) zero_less_m: "m > 0"
apply (cut_tac zero_less_o_G)
apply (simp add: order_G)
done
@@ -134,7 +134,7 @@
lemma (in sylow) card_calM: "card(calM) = (p^a) * m choose p^a"
by (simp add: calM_def n_subsets order_G [symmetric] order_def)
-lemma (in sylow) zero_less_card_calM: "card calM \<noteq> 0"
+lemma (in sylow) zero_less_card_calM: "card calM > 0"
by (simp add: card_calM zero_less_binomial le_extend_mult zero_less_m)
lemma (in sylow) max_p_div_calM:
--- a/src/HOL/Complex/ex/HarmonicSeries.thy Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Complex/ex/HarmonicSeries.thy Tue Oct 23 23:27:23 2007 +0200
@@ -80,7 +80,7 @@
then have
"inverse (real x) = 1 / (real x)"
by (rule nonzero_inverse_eq_divide)
- moreover from mgt0 have "real tm \<noteq> 0" by (simp add: tmdef neq0_conv)
+ moreover from mgt0 have "real tm \<noteq> 0" by (simp add: tmdef)
then have
"inverse (real tm) = 1 / (real tm)"
by (rule nonzero_inverse_eq_divide)
--- a/src/HOL/Complex/ex/MIR.thy Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Complex/ex/MIR.thy Tue Oct 23 23:27:23 2007 +0200
@@ -268,7 +268,7 @@
| "fmsize (NDvd i t) = 2"
| "fmsize p = 1"
(* several lemmas about fmsize *)
-lemma fmsize_pos: "fmsize p \<noteq> 0"
+lemma fmsize_pos: "fmsize p > 0"
by (induct p rule: fmsize.induct) simp_all
(* Semantics of formulae (fm) *)
@@ -316,7 +316,7 @@
"prep (Imp p q) = prep (Or (NOT p) q)"
"prep (Iff p q) = Or (prep (And p q)) (prep (And (NOT p) (NOT q)))"
"prep p = p"
-(hints simp add: fmsize_pos neq0_conv[symmetric])
+(hints simp add: fmsize_pos)
lemma prep: "\<And> bs. Ifm bs (prep p) = Ifm bs p"
by (induct p rule: prep.induct, auto)
--- a/src/HOL/Complex/ex/ReflectedFerrack.thy Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Complex/ex/ReflectedFerrack.thy Tue Oct 23 23:27:23 2007 +0200
@@ -106,7 +106,7 @@
"fmsize (A p) = 4+ fmsize p"
"fmsize p = 1"
(* several lemmas about fmsize *)
-lemma fmsize_pos: "fmsize p \<noteq> 0"
+lemma fmsize_pos: "fmsize p > 0"
by (induct p rule: fmsize.induct) simp_all
(* Semantics of formulae (fm) *)
@@ -917,7 +917,7 @@
"prep (Imp p q) = prep (Or (NOT p) q)"
"prep (Iff p q) = disj (prep (And p q)) (prep (And (NOT p) (NOT q)))"
"prep p = p"
-(hints simp add: fmsize_pos neq0_conv[symmetric])
+(hints simp add: fmsize_pos)
lemma prep: "\<And> bs. Ifm bs (prep p) = Ifm bs p"
by (induct p rule: prep.induct, auto)
--- a/src/HOL/Divides.thy Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Divides.thy Tue Oct 23 23:27:23 2007 +0200
@@ -250,14 +250,14 @@
apply (simp add: quorem_def)
done
-lemma quorem_div_mod: "b \<noteq> 0 ==> quorem ((a, b), (a div b, a mod b))"
- unfolding quorem_def by simp
+lemma quorem_div_mod: "b > 0 ==> quorem ((a, b), (a div b, a mod b))"
+unfolding quorem_def by simp
-lemma quorem_div: "[| quorem((a,b),(q,r)); b \<noteq> 0 |] ==> a div b = q"
- by (simp add: quorem_div_mod [THEN unique_quotient])
+lemma quorem_div: "[| quorem((a,b),(q,r)); b > 0 |] ==> a div b = q"
+by (simp add: quorem_div_mod [THEN unique_quotient])
-lemma quorem_mod: "[| quorem((a,b),(q,r)); b \<noteq> 0 |] ==> a mod b = r"
- by (simp add: quorem_div_mod [THEN unique_remainder])
+lemma quorem_mod: "[| quorem((a,b),(q,r)); b > 0 |] ==> a mod b = r"
+by (simp add: quorem_div_mod [THEN unique_remainder])
(** A dividend of zero **)
@@ -270,9 +270,9 @@
(** proving (a*b) div c = a * (b div c) + a * (b mod c) **)
lemma quorem_mult1_eq:
- "[| quorem((b,c),(q,r)); c \<noteq> 0 |]
- ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))"
- by (auto simp add: split_ifs mult_ac quorem_def add_mult_distrib2)
+ "[| quorem((b,c),(q,r)); c > 0 |]
+ ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))"
+by (auto simp add: split_ifs mult_ac quorem_def add_mult_distrib2)
lemma div_mult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::nat)"
apply (cases "c = 0", simp)
@@ -291,17 +291,18 @@
apply (simp_all add: mult_commute)
done
-lemma mod_mult_distrib_mod: "(a*b) mod (c::nat) = ((a mod c) * (b mod c)) mod c"
- apply (rule mod_mult1_eq' [THEN trans])
- apply (rule mod_mult1_eq)
- done
+lemma mod_mult_distrib_mod:
+ "(a*b) mod (c::nat) = ((a mod c) * (b mod c)) mod c"
+apply (rule mod_mult1_eq' [THEN trans])
+apply (rule mod_mult1_eq)
+done
(** proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) **)
lemma quorem_add1_eq:
- "[| quorem((a,c),(aq,ar)); quorem((b,c),(bq,br)); c \<noteq> 0 |]
- ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))"
- by (auto simp add: split_ifs mult_ac quorem_def add_mult_distrib2)
+ "[| quorem((a,c),(aq,ar)); quorem((b,c),(bq,br)); c > 0 |]
+ ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))"
+by (auto simp add: split_ifs mult_ac quorem_def add_mult_distrib2)
(*NOT suitable for rewriting: the RHS has an instance of the LHS*)
lemma div_add1_eq:
@@ -621,7 +622,7 @@
apply (simp add: power_add)
done
-lemma nat_zero_less_power_iff [simp]: "(0 < x^n) = (x \<noteq> (0::nat) | n=0)"
+lemma nat_zero_less_power_iff [simp]: "(x^n > 0) = (x > (0::nat) | n=0)"
by (induct n) auto
lemma power_le_dvd [rule_format]: "k^j dvd n --> i\<le>j --> k^i dvd (n::nat)"
@@ -690,19 +691,20 @@
lemma split_div_lemma:
"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)
-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
+apply (rule iffI)
+ apply (rule_tac a=m and r = "m - n * q" and r' = "m mod n" in unique_quotient)
+ 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]])
- apply (simp only: add: mult_ac)
- apply (rule_tac P="%x. x < n + n * (m div n)" in
+ apply (simp only: add: mult_ac)
+ apply (rule_tac P="%x. x < n + n * (m div n)" in
subst [OF mod_div_equality [of _ n]])
- apply (simp only: add: mult_ac add_ac)
- apply (rule add_less_mono1, simp)
- done
+apply (simp only: add: mult_ac add_ac)
+apply (rule add_less_mono1, simp)
+done
theorem split_div':
"P ((m::nat) div n) = ((n = 0 \<and> P 0) \<or>
--- a/src/HOL/Finite_Set.thy Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Finite_Set.thy Tue Oct 23 23:27:23 2007 +0200
@@ -1652,16 +1652,6 @@
apply(subst card_insert)
apply(auto intro:ccontr)
done
-(*
-lemma card_1_eq:
- "(card A = Suc 0) = (\<exists>x. A = {x})"
-by (auto dest!: card_eq_SucD)
-
-lemma card_2_eq:
- "(card A = Suc(Suc 0)) = (\<exists>x y. x\<noteq>y & A = {x,y})"
-by (auto dest!: card_eq_SucD)
-*)
-
lemma setsum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat(card A) * y"
apply (cases "finite A")
@@ -1725,7 +1715,7 @@
by(simp add:card_def setsum_reindex o_def del:setsum_constant)
lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A"
- by (simp add: card_seteq card_image)
+by (simp add: card_seteq card_image)
lemma eq_card_imp_inj_on:
"[| finite A; card(f ` A) = card A |] ==> inj_on f A"
@@ -1806,6 +1796,32 @@
done
+subsubsection {* Relating injectivity and surjectivity *}
+
+lemma finite_surj_inj: "finite(A) \<Longrightarrow> A <= f`A \<Longrightarrow> inj_on f A"
+apply(rule eq_card_imp_inj_on, assumption)
+apply(frule finite_imageI)
+apply(drule (1) card_seteq)
+apply(erule card_image_le)
+apply simp
+done
+
+lemma finite_UNIV_surj_inj: fixes f :: "'a \<Rightarrow> 'a"
+shows "finite(UNIV:: 'a set) \<Longrightarrow> surj f \<Longrightarrow> inj f"
+by (blast intro: finite_surj_inj subset_UNIV dest:surj_range)
+
+lemma finite_UNIV_inj_surj: fixes f :: "'a \<Rightarrow> 'a"
+shows "finite(UNIV:: 'a set) \<Longrightarrow> inj f \<Longrightarrow> surj f"
+by(fastsimp simp:surj_def dest!: endo_inj_surj)
+
+corollary infinite_UNIV_nat: "~finite(UNIV::nat set)"
+proof
+ assume "finite(UNIV::nat set)"
+ with finite_UNIV_inj_surj[of Suc]
+ show False by simp (blast dest: Suc_neq_Zero surjD)
+qed
+
+
subsection{* A fold functional for non-empty sets *}
text{* Does not require start value. *}
--- a/src/HOL/Hyperreal/Fact.thy Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Hyperreal/Fact.thy Tue Oct 23 23:27:23 2007 +0200
@@ -20,7 +20,7 @@
by (induct n) auto
lemma fact_not_eq_zero [simp]: "fact n \<noteq> 0"
-by (simp add: neq0_conv)
+by simp
lemma real_of_nat_fact_not_zero [simp]: "real (fact n) \<noteq> 0"
by auto
--- a/src/HOL/Hyperreal/HyperNat.thy Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Hyperreal/HyperNat.thy Tue Oct 23 23:27:23 2007 +0200
@@ -331,7 +331,7 @@
"\<forall>N::nat. {n. f n \<noteq> N} \<in> FreeUltrafilterNat
==> {n. N < f n} \<in> FreeUltrafilterNat"
apply (induct_tac N)
-apply (drule_tac x = 0 in spec, simp add: neq0_conv)
+apply (drule_tac x = 0 in spec, simp)
apply (drule_tac x = "Suc n" in spec)
apply (elim ultra, auto)
done
--- a/src/HOL/Hyperreal/MacLaurin.thy Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Hyperreal/MacLaurin.thy Tue Oct 23 23:27:23 2007 +0200
@@ -114,7 +114,7 @@
done
lemma Maclaurin:
- "[| 0 < h; n \<noteq> 0; diff 0 = f;
+ "[| 0 < h; n > 0; diff 0 = f;
\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t |]
==> \<exists>t. 0 < t &
t < h &
@@ -185,7 +185,7 @@
done
lemma Maclaurin_objl:
- "0 < h & n\<noteq>0 & diff 0 = f &
+ "0 < h & n>0 & diff 0 = f &
(\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t)
--> (\<exists>t. 0 < t & t < h &
f h = (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
@@ -218,7 +218,7 @@
by (blast intro: Maclaurin2)
lemma Maclaurin_minus:
- "[| h < 0; n \<noteq> 0; diff 0 = f;
+ "[| h < 0; n > 0; diff 0 = f;
\<forall>m t. m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t |]
==> \<exists>t. h < t &
t < 0 &
@@ -245,7 +245,7 @@
done
lemma Maclaurin_minus_objl:
- "(h < 0 & n \<noteq> 0 & diff 0 = f &
+ "(h < 0 & n > 0 & diff 0 = f &
(\<forall>m t.
m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t))
--> (\<exists>t. h < t &
@@ -261,7 +261,7 @@
(* not good for PVS sin_approx, cos_approx *)
lemma Maclaurin_bi_le_lemma [rule_format]:
- "n\<noteq>0 \<longrightarrow>
+ "n>0 \<longrightarrow>
diff 0 0 =
(\<Sum>m = 0..<n. diff m 0 * 0 ^ m / real (fact m)) +
diff n 0 * 0 ^ n / real (fact n)"
@@ -294,7 +294,7 @@
lemma Maclaurin_all_lt:
"[| diff 0 = f;
\<forall>m x. DERIV (diff m) x :> diff(Suc m) x;
- x ~= 0; n \<noteq> 0
+ x ~= 0; n > 0
|] ==> \<exists>t. 0 < abs t & abs t < abs x &
f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
(diff n t / real (fact n)) * x ^ n"
@@ -308,7 +308,7 @@
lemma Maclaurin_all_lt_objl:
"diff 0 = f &
(\<forall>m x. DERIV (diff m) x :> diff(Suc m) x) &
- x ~= 0 & n \<noteq> 0
+ x ~= 0 & n > 0
--> (\<exists>t. 0 < abs t & abs t < abs x &
f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
(diff n t / real (fact n)) * x ^ n)"
@@ -346,7 +346,7 @@
subsection{*Version for Exponential Function*}
-lemma Maclaurin_exp_lt: "[| x ~= 0; n \<noteq> 0 |]
+lemma Maclaurin_exp_lt: "[| x ~= 0; n > 0 |]
==> (\<exists>t. 0 < abs t &
abs t < abs x &
exp x = (\<Sum>m=0..<n. (x ^ m) / real (fact m)) +
@@ -423,9 +423,8 @@
done
-
lemma Maclaurin_sin_expansion3:
- "[| n \<noteq> 0; 0 < x |] ==>
+ "[| n > 0; 0 < x |] ==>
\<exists>t. 0 < t & t < x &
sin x =
(\<Sum>m=0..<n. (if even m then 0
@@ -491,7 +490,7 @@
done
lemma Maclaurin_cos_expansion2:
- "[| 0 < x; n \<noteq> 0 |] ==>
+ "[| 0 < x; n > 0 |] ==>
\<exists>t. 0 < t & t < x &
cos x =
(\<Sum>m=0..<n. (if even m
@@ -510,7 +509,7 @@
done
lemma Maclaurin_minus_cos_expansion:
- "[| x < 0; n \<noteq> 0 |] ==>
+ "[| x < 0; n > 0 |] ==>
\<exists>t. x < t & t < 0 &
cos x =
(\<Sum>m=0..<n. (if even m
--- a/src/HOL/Hyperreal/Poly.thy Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Hyperreal/Poly.thy Tue Oct 23 23:27:23 2007 +0200
@@ -782,7 +782,7 @@
declare pexp_one [simp]
lemma lemma_order_root [rule_format]:
- "\<forall>p a. n \<noteq> 0 & [- a, 1] %^ n divides p & ~ [- a, 1] %^ (Suc n) divides p
+ "\<forall>p a. n > 0 & [- a, 1] %^ n divides p & ~ [- a, 1] %^ (Suc n) divides p
--> poly p a = 0"
apply (induct "n", blast)
apply (auto simp add: divides_def poly_mult simp del: pmult_Cons)
@@ -792,8 +792,9 @@
apply (case_tac "poly p = poly []", auto)
apply (simp add: poly_linear_divides del: pmult_Cons, safe)
apply (drule_tac [!] a = a in order2)
+apply (rule ccontr)
apply (simp add: divides_def poly_mult fun_eq del: pmult_Cons, blast)
-apply (metis gr0_conv lemma_order_root)
+apply (blast intro: lemma_order_root)
done
lemma order_divides: "(([-a, 1] %^ n) divides p) = ((poly p = poly []) | n \<le> order a p)"
@@ -842,7 +843,7 @@
(* FIXME: too too long! *)
lemma lemma_order_pderiv [rule_format]:
- "\<forall>p q a. n \<noteq> 0 &
+ "\<forall>p q a. n > 0 &
poly (pderiv p) \<noteq> poly [] &
poly p = poly ([- a, 1] %^ n *** q) & ~ [- a, 1] divides q
--> n = Suc (order a (pderiv p))"
--- a/src/HOL/Hyperreal/Taylor.thy Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Hyperreal/Taylor.thy Tue Oct 23 23:27:23 2007 +0200
@@ -15,7 +15,7 @@
*}
lemma taylor_up:
- assumes INIT: "n\<noteq>0" "diff 0 = f"
+ assumes INIT: "n>0" "diff 0 = f"
and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"
and INTERV: "a \<le> c" "c < b"
shows "\<exists> t. c < t & t < b &
@@ -24,9 +24,9 @@
proof -
from INTERV have "0 < b-c" by arith
moreover
- from INIT have "n\<noteq>0" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto
+ from INIT have "n>0" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto
moreover
- have "ALL m t. m < n & 0 <= t & t <= b - c --> DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)"
+ have "ALL m t. m < n & 0 <= t & t <= b - c --> DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)"
proof (intro strip)
fix m t
assume "m < n & 0 <= t & t <= b - c"
@@ -57,7 +57,7 @@
qed
lemma taylor_down:
- assumes INIT: "n\<noteq>0" "diff 0 = f"
+ assumes INIT: "n>0" "diff 0 = f"
and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"
and INTERV: "a < c" "c \<le> b"
shows "\<exists> t. a < t & t < c &
@@ -66,7 +66,7 @@
proof -
from INTERV have "a-c < 0" by arith
moreover
- from INIT have "n\<noteq>0" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto
+ from INIT have "n>0" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto
moreover
have "ALL m t. m < n & a-c <= t & t <= 0 --> DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)"
proof (rule allI impI)+
@@ -97,7 +97,7 @@
qed
lemma taylor:
- assumes INIT: "n\<noteq>0" "diff 0 = f"
+ assumes INIT: "n>0" "diff 0 = f"
and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"
and INTERV: "a \<le> c " "c \<le> b" "a \<le> x" "x \<le> b" "x \<noteq> c"
shows "\<exists> t. (if x<c then (x < t & t < c) else (c < t & t < x)) &
--- a/src/HOL/IntArith.thy Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/IntArith.thy Tue Oct 23 23:27:23 2007 +0200
@@ -398,6 +398,15 @@
apply (frule pos_zmult_eq_1_iff_lemma, auto)
done
+(* Could be simplified but Presburger only becomes available too late *)
+lemma infinite_UNIV_int: "~finite(UNIV::int set)"
+proof
+ assume "finite(UNIV::int set)"
+ moreover have "~(EX i::int. 2*i = 1)"
+ by (auto simp: pos_zmult_eq_1_iff)
+ ultimately show False using finite_UNIV_inj_surj[of "%n::int. n+n"]
+ by (simp add:inj_on_def surj_def) (blast intro:sym)
+qed
subsection {* Legacy ML bindings *}
--- a/src/HOL/Library/Binomial.thy Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Library/Binomial.thy Tue Oct 23 23:27:23 2007 +0200
@@ -44,7 +44,7 @@
lemma binomial_1 [simp]: "(n choose Suc 0) = n"
by (induct n) simp_all
-lemma zero_less_binomial: "k \<le> n ==> (n choose k) \<noteq> 0"
+lemma zero_less_binomial: "k \<le> n ==> (n choose k) > 0"
by (induct n k rule: diff_induct) simp_all
lemma binomial_eq_0_iff: "(n choose k = 0) = (n<k)"
@@ -53,8 +53,9 @@
apply (simp add: zero_less_binomial)
done
-lemma zero_less_binomial_iff: "(n choose k \<noteq> 0) = (k\<le>n)"
-by (simp add: linorder_not_less binomial_eq_0_iff)
+lemma zero_less_binomial_iff: "(n choose k > 0) = (k\<le>n)"
+by(simp add: linorder_not_less binomial_eq_0_iff neq0_conv[symmetric]
+ del:neq0_conv)
(*Might be more useful if re-oriented*)
lemma Suc_times_binomial_eq:
--- a/src/HOL/Library/Multiset.thy Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Library/Multiset.thy Tue Oct 23 23:27:23 2007 +0200
@@ -11,7 +11,7 @@
subsection {* The type of multisets *}
-typedef 'a multiset = "{f::'a => nat. finite {x . f x \<noteq> 0}}"
+typedef 'a multiset = "{f::'a => nat. finite {x . f x > 0}}"
proof
show "(\<lambda>x. 0::nat) \<in> ?multiset" by simp
qed
@@ -38,7 +38,7 @@
abbreviation
Melem :: "'a => 'a multiset => bool" ("(_/ :# _)" [50, 51] 50) where
- "a :# M == count M a \<noteq> 0"
+ "a :# M == count M a > 0"
syntax
"_MCollect" :: "pttrn => 'a multiset => bool => 'a multiset" ("(1{# _ : _./ _#})")
@@ -309,7 +309,7 @@
apply (rule ext, force, clarify)
apply (frule setsum_SucD, clarify)
apply (rename_tac a)
- apply (subgoal_tac "finite {x. (f (a := f a - 1)) x \<noteq> 0}")
+ apply (subgoal_tac "finite {x. (f (a := f a - 1)) x > 0}")
prefer 2
apply (rule finite_subset)
prefer 2
@@ -759,7 +759,7 @@
apply (rule_tac x = "x # xa" in exI, auto)
done
-lemma set_count_greater_0: "set x = {a. count (multiset_of x) a \<noteq> 0}"
+lemma set_count_greater_0: "set x = {a. count (multiset_of x) a > 0}"
by (induct x) auto
lemma distinct_count_atmost_1:
--- a/src/HOL/Library/Parity.thy Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Library/Parity.thy Tue Oct 23 23:27:23 2007 +0200
@@ -222,7 +222,7 @@
apply (subst power_add)
apply (subst zero_le_mult_iff)
apply auto
- apply (subgoal_tac "x = 0 & y \<noteq> 0")
+ apply (subgoal_tac "x = 0 & y > 0")
apply (erule conjE, assumption)
apply (subst power_eq_0_iff [symmetric])
apply (subgoal_tac "0 <= x^y * x^y")
--- a/src/HOL/Library/Word.thy Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Library/Word.thy Tue Oct 23 23:27:23 2007 +0200
@@ -479,7 +479,7 @@
with mod_div_equality [of n 2]
show "n div 2 * 2 = n" by simp
next
- assume "n mod 2 \<noteq> 0"
+ assume "n mod 2 = Suc 0"
with mod_div_equality [of n 2]
show "Suc (n div 2 * 2) = n" by arith
qed
--- a/src/HOL/List.thy Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/List.thy Tue Oct 23 23:27:23 2007 +0200
@@ -950,7 +950,7 @@
proof (cases)
assume "p x"
hence eq: "?S' = insert 0 (Suc ` ?S)"
- by(auto simp: nth_Cons image_def split:nat.split dest:not0_implies_Suc)
+ by(auto simp: image_def split:nat.split dest:gr0_implies_Suc)
have "length (filter p (x # xs)) = Suc(card ?S)"
using Cons `p x` by simp
also have "\<dots> = Suc(card(Suc ` ?S))" using fin
@@ -961,7 +961,7 @@
next
assume "\<not> p x"
hence eq: "?S' = Suc ` ?S"
- by(auto simp add: image_def neq0_conv split:nat.split elim:lessE)
+ by(auto simp add: image_def split:nat.split elim:lessE)
have "length (filter p (x # xs)) = card ?S"
using Cons `\<not> p x` by simp
also have "\<dots> = card(Suc ` ?S)" using fin
@@ -2456,7 +2456,7 @@
lemma set_sublist: "set(sublist xs I) = {xs!i|i. i<size xs \<and> i \<in> I}"
apply(induct xs arbitrary: I)
-apply(auto simp: sublist_Cons nth_Cons split:nat.split dest!: not0_implies_Suc)
+apply(auto simp: sublist_Cons nth_Cons split:nat.split dest!: gr0_implies_Suc)
done
lemma set_sublist_subset: "set(sublist xs I) \<subseteq> set xs"
--- a/src/HOL/Nat.thy Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Nat.thy Tue Oct 23 23:27:23 2007 +0200
@@ -100,22 +100,22 @@
text {* Injectiveness and distinctness lemmas *}
lemma Suc_neq_Zero: "Suc m = 0 ==> R"
- by (rule notE, rule Suc_not_Zero)
+by (rule notE, rule Suc_not_Zero)
lemma Zero_neq_Suc: "0 = Suc m ==> R"
- by (rule Suc_neq_Zero, erule sym)
+by (rule Suc_neq_Zero, erule sym)
lemma Suc_inject: "Suc x = Suc y ==> x = y"
- by (rule inj_Suc [THEN injD])
+by (rule inj_Suc [THEN injD])
lemma nat_not_singleton: "(\<forall>x. x = (0::nat)) = False"
- by auto
+by auto
lemma n_not_Suc_n: "n \<noteq> Suc n"
- by (induct n) simp_all
+by (induct n) simp_all
lemma Suc_n_not_n: "Suc t \<noteq> t"
- by (rule not_sym, rule n_not_Suc_n)
+by (rule not_sym, rule n_not_Suc_n)
text {* A special form of induction for reasoning
@@ -221,12 +221,12 @@
done
lemma less_irrefl [elim!]: "(n::nat) < n ==> R"
- by (rule notE, rule less_not_refl)
+by (rule notE, rule less_not_refl)
lemma less_not_refl2: "n < m ==> m \<noteq> (n::nat)" by blast
lemma less_not_refl3: "(s::nat) < t ==> s \<noteq> t"
- by (rule not_sym, rule less_not_refl2)
+by (rule not_sym, rule less_not_refl2)
lemma lessE:
assumes major: "i < k"
@@ -239,10 +239,10 @@
done
lemma not_less0 [iff]: "~ n < (0::nat)"
- by (blast elim: lessE)
+by (blast elim: lessE)
lemma less_zeroE: "(n::nat) < 0 ==> R"
- by (rule notE, rule not_less0)
+by (rule notE, rule not_less0)
lemma less_SucE: assumes major: "m < Suc n"
and less: "m < n ==> P" and eq: "m = n ==> P" shows P
@@ -252,16 +252,16 @@
done
lemma less_Suc_eq: "(m < Suc n) = (m < n | m = n)"
- by (blast elim!: less_SucE intro: less_trans)
+by (blast elim!: less_SucE intro: less_trans)
lemma less_one [iff,noatp]: "(n < (1::nat)) = (n = 0)"
- by (simp add: less_Suc_eq)
+by (simp add: less_Suc_eq)
lemma less_Suc0 [iff]: "(n < Suc 0) = (n = 0)"
- by (simp add: less_Suc_eq)
+by (simp add: less_Suc_eq)
lemma Suc_mono: "m < n ==> Suc m < Suc n"
- by (induct n) (fast elim: less_trans lessE)+
+by (induct n) (fast elim: less_trans lessE)+
text {* "Less than" is a linear ordering *}
lemma less_linear: "m < n | m = n | n < (m::nat)"
@@ -312,7 +312,7 @@
done
lemma Suc_less_SucD: "Suc m < Suc n ==> m < n"
- by (blast elim: lessE dest: Suc_lessD)
+by (blast elim: lessE dest: Suc_lessD)
lemma Suc_less_eq [iff, code]: "(Suc m < Suc n) = (m < n)"
apply (rule iffI)
@@ -333,7 +333,7 @@
text {* Can be used with @{text less_Suc_eq} to get @{term "n = m | n < m"} *}
lemma not_less_eq: "(~ m < n) = (n < Suc m)"
- by (induct m n rule: diff_induct) simp_all
+by (induct m n rule: diff_induct) simp_all
text {* Complete induction, aka course-of-values induction *}
lemma nat_less_induct:
@@ -353,22 +353,22 @@
unfolding le_def by (rule not_less_eq [symmetric])
lemma le_imp_less_Suc: "m \<le> n ==> m < Suc n"
- by (rule less_Suc_eq_le [THEN iffD2])
+by (rule less_Suc_eq_le [THEN iffD2])
lemma le0 [iff]: "(0::nat) \<le> n"
unfolding le_def by (rule not_less0)
lemma Suc_n_not_le_n: "~ Suc n \<le> n"
- by (simp add: le_def)
+by (simp add: le_def)
lemma le_0_eq [iff]: "((i::nat) \<le> 0) = (i = 0)"
- by (induct i) (simp_all add: le_def)
+by (induct i) (simp_all add: le_def)
lemma le_Suc_eq: "(m \<le> Suc n) = (m \<le> n | m = Suc n)"
- by (simp del: less_Suc_eq_le add: less_Suc_eq_le [symmetric] less_Suc_eq)
+by (simp del: less_Suc_eq_le add: less_Suc_eq_le [symmetric] less_Suc_eq)
lemma le_SucE: "m \<le> Suc n ==> (m \<le> n ==> R) ==> (m = Suc n ==> R) ==> R"
- by (drule le_Suc_eq [THEN iffD1], iprover+)
+by (drule le_Suc_eq [THEN iffD1], iprover+)
lemma Suc_leI: "m < n ==> Suc(m) \<le> n"
apply (simp add: le_def less_Suc_eq)
@@ -376,7 +376,7 @@
done -- {* formerly called lessD *}
lemma Suc_leD: "Suc(m) \<le> n ==> m \<le> n"
- by (simp add: le_def less_Suc_eq)
+by (simp add: le_def less_Suc_eq)
text {* Stronger version of @{text Suc_leD} *}
lemma Suc_le_lessD: "Suc m \<le> n ==> m < n"
@@ -386,13 +386,13 @@
done
lemma Suc_le_eq: "(Suc m \<le> n) = (m < n)"
- by (blast intro: Suc_leI Suc_le_lessD)
+by (blast intro: Suc_leI Suc_le_lessD)
lemma le_SucI: "m \<le> n ==> m \<le> Suc n"
- by (unfold le_def) (blast dest: Suc_lessD)
+by (unfold le_def) (blast dest: Suc_lessD)
lemma less_imp_le: "m < n ==> m \<le> (n::nat)"
- by (unfold le_def) (blast elim: less_asym)
+by (unfold le_def) (blast elim: less_asym)
text {* For instance, @{text "(Suc m < Suc n) = (Suc m \<le> n) = (m < n)"} *}
lemmas le_simps = less_imp_le less_Suc_eq_le Suc_le_eq
@@ -411,36 +411,36 @@
by (blast elim!: less_irrefl elim: less_asym)
lemma le_eq_less_or_eq: "(m \<le> (n::nat)) = (m < n | m=n)"
- by (iprover intro: less_or_eq_imp_le le_imp_less_or_eq)
+by (iprover intro: less_or_eq_imp_le le_imp_less_or_eq)
text {* Useful with @{text blast}. *}
lemma eq_imp_le: "(m::nat) = n ==> m \<le> n"
- by (rule less_or_eq_imp_le) (rule disjI2)
+by (rule less_or_eq_imp_le) (rule disjI2)
lemma le_refl: "n \<le> (n::nat)"
- by (simp add: le_eq_less_or_eq)
+by (simp add: le_eq_less_or_eq)
lemma le_less_trans: "[| i \<le> j; j < k |] ==> i < (k::nat)"
- by (blast dest!: le_imp_less_or_eq intro: less_trans)
+by (blast dest!: le_imp_less_or_eq intro: less_trans)
lemma less_le_trans: "[| i < j; j \<le> k |] ==> i < (k::nat)"
- by (blast dest!: le_imp_less_or_eq intro: less_trans)
+by (blast dest!: le_imp_less_or_eq intro: less_trans)
lemma le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::nat)"
- by (blast dest!: le_imp_less_or_eq intro: less_or_eq_imp_le less_trans)
+by (blast dest!: le_imp_less_or_eq intro: less_or_eq_imp_le less_trans)
lemma le_anti_sym: "[| m \<le> n; n \<le> m |] ==> m = (n::nat)"
- by (blast dest!: le_imp_less_or_eq elim!: less_irrefl elim: less_asym)
+by (blast dest!: le_imp_less_or_eq elim!: less_irrefl elim: less_asym)
lemma Suc_le_mono [iff]: "(Suc n \<le> Suc m) = (n \<le> m)"
- by (simp add: le_simps)
+by (simp add: le_simps)
text {* Axiom @{text order_less_le} of class @{text order}: *}
lemma nat_less_le: "((m::nat) < n) = (m \<le> n & m \<noteq> n)"
- by (simp add: le_def nat_neq_iff) (blast elim!: less_asym)
+by (simp add: le_def nat_neq_iff) (blast elim!: less_asym)
lemma le_neq_implies_less: "(m::nat) \<le> n ==> m \<noteq> n ==> m < n"
- by (rule iffD2, rule nat_less_le, rule conjI)
+by (rule iffD2, rule nat_less_le, rule conjI)
text {* Axiom @{text linorder_linear} of class @{text linorder}: *}
lemma nat_le_linear: "(m::nat) \<le> n | n \<le> m"
@@ -457,7 +457,7 @@
lemmas linorder_neqE_nat = linorder_neqE [where 'a = nat]
lemma not_less_less_Suc_eq: "~ n < m ==> (n < Suc m) = (n = m)"
- by (blast elim!: less_SucE)
+by (blast elim!: less_SucE)
text {*
Rewrite @{term "n < Suc m"} to @{term "n = m"}
@@ -465,7 +465,7 @@
Not suitable as default simprules because they often lead to looping
*}
lemma le_less_Suc_eq: "m \<le> n ==> (n < Suc m) = (n = m)"
- by (rule not_less_less_Suc_eq, rule leD)
+by (rule not_less_less_Suc_eq, rule leD)
lemmas not_less_simps = not_less_less_Suc_eq le_less_Suc_eq
@@ -478,46 +478,47 @@
text {* Polymorphic, not just for @{typ nat} *}
lemma zero_reorient: "(0 = x) = (x = 0)"
- by auto
+by auto
lemma one_reorient: "(1 = x) = (x = 1)"
- by auto
+by auto
text {* These two rules ease the use of primitive recursion.
NOTE USE OF @{text "=="} *}
lemma def_nat_rec_0: "(!!n. f n == nat_rec c h n) ==> f 0 = c"
- by simp
+by simp
lemma def_nat_rec_Suc: "(!!n. f n == nat_rec c h n) ==> f (Suc n) = h n (f n)"
- by simp
+by simp
lemma not0_implies_Suc: "n \<noteq> 0 ==> \<exists>m. n = Suc m"
- by (cases n) simp_all
+by (cases n) simp_all
+
+lemma gr0_implies_Suc: "n > 0 ==> \<exists>m. n = Suc m"
+by (cases n) simp_all
lemma gr_implies_not0: fixes n :: nat shows "m<n ==> n \<noteq> 0"
- by (cases n) simp_all
+by (cases n) simp_all
-lemma neq0_conv: fixes n :: nat shows "(n \<noteq> 0) = (0 < n)"
- by (cases n) simp_all
-
-lemmas gr0_conv = neq0_conv[symmetric]
+lemma neq0_conv[iff]: fixes n :: nat shows "(n \<noteq> 0) = (0 < n)"
+by (cases n) simp_all
text {* This theorem is useful with @{text blast} *}
lemma gr0I: "((n::nat) = 0 ==> False) ==> 0 < n"
- by (rule iffD1, rule neq0_conv, iprover)
+by (rule neq0_conv[THEN iffD1], iprover)
lemma gr0_conv_Suc: "(0 < n) = (\<exists>m. n = Suc m)"
- by (fast intro: not0_implies_Suc)
+by (fast intro: not0_implies_Suc)
lemma not_gr0 [iff,noatp]: "!!n::nat. (~ (0 < n)) = (n = 0)"
using neq0_conv by blast
lemma Suc_le_D: "(Suc n \<le> m') ==> (? m. m' = Suc m)"
- by (induct m') simp_all
+by (induct m') simp_all
text {* Useful in certain inductive arguments *}
lemma less_Suc_eq_0_disj: "(m < Suc n) = (m = 0 | (\<exists>j. m = Suc j & j < n))"
- by (cases m) simp_all
+by (cases m) simp_all
lemma nat_induct2: "[|P 0; P (Suc 0); !!k. P k ==> P (Suc (Suc k))|] ==> P n"
apply (rule nat_less_induct)
@@ -542,48 +543,48 @@
done
lemma Least_Suc2:
- "[|P n; Q m; ~P 0; !k. P (Suc k) = Q k|] ==> Least P = Suc (Least Q)"
- by (erule (1) Least_Suc [THEN ssubst], simp)
+ "[|P n; Q m; ~P 0; !k. P (Suc k) = Q k|] ==> Least P = Suc (Least Q)"
+by (erule (1) Least_Suc [THEN ssubst], simp)
subsection {* @{term min} and @{term max} *}
lemma mono_Suc: "mono Suc"
- by (rule monoI) simp
+by (rule monoI) simp
lemma min_0L [simp]: "min 0 n = (0::nat)"
- by (rule min_leastL) simp
+by (rule min_leastL) simp
lemma min_0R [simp]: "min n 0 = (0::nat)"
- by (rule min_leastR) simp
+by (rule min_leastR) simp
lemma min_Suc_Suc [simp]: "min (Suc m) (Suc n) = Suc (min m n)"
- by (simp add: mono_Suc min_of_mono)
+by (simp add: mono_Suc min_of_mono)
lemma min_Suc1:
"min (Suc n) m = (case m of 0 => 0 | Suc m' => Suc(min n m'))"
- by (simp split: nat.split)
+by (simp split: nat.split)
lemma min_Suc2:
"min m (Suc n) = (case m of 0 => 0 | Suc m' => Suc(min m' n))"
- by (simp split: nat.split)
+by (simp split: nat.split)
lemma max_0L [simp]: "max 0 n = (n::nat)"
- by (rule max_leastL) simp
+by (rule max_leastL) simp
lemma max_0R [simp]: "max n 0 = (n::nat)"
- by (rule max_leastR) simp
+by (rule max_leastR) simp
lemma max_Suc_Suc [simp]: "max (Suc m) (Suc n) = Suc(max m n)"
- by (simp add: mono_Suc max_of_mono)
+by (simp add: mono_Suc max_of_mono)
lemma max_Suc1:
"max (Suc n) m = (case m of 0 => Suc n | Suc m' => Suc(max n m'))"
- by (simp split: nat.split)
+by (simp split: nat.split)
lemma max_Suc2:
"max m (Suc n) = (case m of 0 => Suc n | Suc m' => Suc(max m' n))"
- by (simp split: nat.split)
+by (simp split: nat.split)
subsection {* Basic rewrite rules for the arithmetic operators *}
@@ -591,10 +592,10 @@
text {* Difference *}
lemma diff_0_eq_0 [simp, code]: "0 - n = (0::nat)"
- by (induct n) simp_all
+by (induct n) simp_all
lemma diff_Suc_Suc [simp, code]: "Suc(m) - Suc(n) = m - n"
- by (induct n) simp_all
+by (induct n) simp_all
text {*
@@ -602,7 +603,7 @@
However, none of the generalizations are currently in the simpset,
and I dread to think what happens if I put them in
*}
-lemma Suc_pred [simp]: "0 \<noteq> n ==> Suc (n - Suc 0) = n"
+lemma Suc_pred [simp]: "n>0 ==> Suc (n - Suc 0) = n"
by (simp split add: nat.split)
declare diff_Suc [simp del, code del]
@@ -611,22 +612,22 @@
subsection {* Addition *}
lemma add_0_right [simp]: "m + 0 = (m::nat)"
- by (induct m) simp_all
+by (induct m) simp_all
lemma add_Suc_right [simp]: "m + Suc n = Suc (m + n)"
- by (induct m) simp_all
+by (induct m) simp_all
lemma add_Suc_shift [code]: "Suc m + n = m + Suc n"
- by simp
+by simp
text {* Associative law for addition *}
lemma nat_add_assoc: "(m + n) + k = m + ((n + k)::nat)"
- by (induct m) simp_all
+by (induct m) simp_all
text {* Commutative law for addition *}
lemma nat_add_commute: "m + n = n + (m::nat)"
- by (induct m) simp_all
+by (induct m) simp_all
lemma nat_add_left_commute: "x + (y + z) = y + ((x + z)::nat)"
apply (rule mk_left_commute [of "op +"])
@@ -635,30 +636,30 @@
done
lemma nat_add_left_cancel [simp]: "(k + m = k + n) = (m = (n::nat))"
- by (induct k) simp_all
+by (induct k) simp_all
lemma nat_add_right_cancel [simp]: "(m + k = n + k) = (m=(n::nat))"
- by (induct k) simp_all
+by (induct k) simp_all
lemma nat_add_left_cancel_le [simp]: "(k + m \<le> k + n) = (m\<le>(n::nat))"
- by (induct k) simp_all
+by (induct k) simp_all
lemma nat_add_left_cancel_less [simp]: "(k + m < k + n) = (m<(n::nat))"
- by (induct k) simp_all
+by (induct k) simp_all
text {* Reasoning about @{text "m + 0 = 0"}, etc. *}
lemma add_is_0 [iff]: fixes m :: nat shows "(m + n = 0) = (m = 0 & n = 0)"
- by (cases m) simp_all
+by (cases m) simp_all
lemma add_is_1: "(m+n= Suc 0) = (m= Suc 0 & n=0 | m=0 & n= Suc 0)"
- by (cases m) simp_all
+by (cases m) simp_all
lemma one_is_add: "(Suc 0 = m + n) = (m = Suc 0 & n = 0 | m = 0 & n = Suc 0)"
- by (rule trans, rule eq_commute, rule add_is_1)
+by (rule trans, rule eq_commute, rule add_is_1)
-lemma add_gr_0 [iff]: "!!m::nat. (m + n > 0) = (m\<noteq>0 | n\<noteq>0)"
-by (simp add:gr0_conv)
+lemma add_gr_0 [iff]: "!!m::nat. (m + n > 0) = (m>0 | n>0)"
+by(auto dest:gr0_implies_Suc)
lemma add_eq_self_zero: "!!m::nat. m + n = m ==> n = 0"
apply (drule add_0_right [THEN ssubst])
@@ -677,26 +678,26 @@
text {* right annihilation in product *}
lemma mult_0_right [simp]: "(m::nat) * 0 = 0"
- by (induct m) simp_all
+by (induct m) simp_all
text {* right successor law for multiplication *}
lemma mult_Suc_right [simp]: "m * Suc n = m + (m * n)"
- by (induct m) (simp_all add: nat_add_left_commute)
+by (induct m) (simp_all add: nat_add_left_commute)
text {* Commutative law for multiplication *}
lemma nat_mult_commute: "m * n = n * (m::nat)"
- by (induct m) simp_all
+by (induct m) simp_all
text {* addition distributes over multiplication *}
lemma add_mult_distrib: "(m + n) * k = (m * k) + ((n * k)::nat)"
- by (induct m) (simp_all add: nat_add_assoc nat_add_left_commute)
+by (induct m) (simp_all add: nat_add_assoc nat_add_left_commute)
lemma add_mult_distrib2: "k * (m + n) = (k * m) + ((k * n)::nat)"
- by (induct m) (simp_all add: nat_add_assoc)
+by (induct m) (simp_all add: nat_add_assoc)
text {* Associative law for multiplication *}
lemma nat_mult_assoc: "(m * n) * k = m * ((n * k)::nat)"
- by (induct m) (simp_all add: add_mult_distrib)
+by (induct m) (simp_all add: add_mult_distrib)
text{*The naturals form a @{text comm_semiring_1_cancel}*}
@@ -725,7 +726,7 @@
text {* strict, in 1st argument *}
lemma add_less_mono1: "i < j ==> i + k < j + (k::nat)"
- by (induct k) simp_all
+by (induct k) simp_all
text {* strict, in both arguments *}
lemma add_less_mono: "[|i < j; k < l|] ==> i + k < j + (l::nat)"
@@ -759,10 +760,10 @@
qed
lemma nat_mult_1: "(1::nat) * n = n"
- by simp
+by simp
lemma nat_mult_1_right: "n * (1::nat) = n"
- by simp
+by simp
subsection {* Additional theorems about "less than" *}
@@ -1083,7 +1084,7 @@
by (simp add: linorder_not_less [symmetric], auto)
lemma mult_cancel2 [simp]: "(m * k = n * k) = (m = n | (k = (0::nat)))"
-apply (cut_tac less_linear, safe, auto simp add: neq0_conv)
+apply (cut_tac less_linear, safe, auto)
apply (drule mult_less_mono1, assumption, simp)+
done
@@ -1105,7 +1106,7 @@
apply (rule disjCI)
apply (rule nat_less_cases, erule_tac [2] _)
apply (drule_tac [2] mult_less_mono2)
- apply (auto simp add: neq0_conv)
+ apply (auto)
done
@@ -1119,7 +1120,7 @@
setup Size.setup
lemma nat_size [simp, code func]: "size (n\<Colon>nat) = n"
- by (induct n) simp_all
+by (induct n) simp_all
lemma size_bool [code func]:
"size (b\<Colon>bool) = 0" by (cases b) auto
@@ -1136,7 +1137,7 @@
"Suc n = Suc m \<longleftrightarrow> n = m"
"Suc n = 0 \<longleftrightarrow> False"
"0 = Suc m \<longleftrightarrow> False"
- by auto
+by auto
lemma [code func]:
"(0\<Colon>nat) \<le> m \<longleftrightarrow> True"
@@ -1186,7 +1187,7 @@
by (cases "a<b" rule: case_split) (auto simp add: diff_is_0_eq [THEN iffD2])
lemma nat_diff_split_asm:
- "P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))"
+ "P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))"
-- {* elimination of @{text -} on @{text nat} in assumptions *}
by (simp split: nat_diff_split)
@@ -1378,7 +1379,7 @@
done
lemma of_nat_less_iff [simp]:
- "(of_nat m < (of_nat n::'a::ordered_semidom)) = (m<n)"
+ "(of_nat m < (of_nat n::'a::ordered_semidom)) = (m<n)"
by (blast intro: of_nat_less_imp_less less_imp_of_nat_less)
text{*Special cases where either operand is zero*}
@@ -1390,7 +1391,7 @@
by (rule of_nat_less_iff [of _ 0, simplified])
lemma of_nat_le_iff [simp]:
- "(of_nat m \<le> (of_nat n::'a::ordered_semidom)) = (m \<le> n)"
+ "(of_nat m \<le> (of_nat n::'a::ordered_semidom)) = (m \<le> n)"
by (simp add: linorder_not_less [symmetric])
text{*Special cases where either operand is zero*}
@@ -1420,7 +1421,7 @@
by (simp add: inj_on_def)
lemma of_nat_diff:
- "n \<le> m ==> of_nat (m - n) = of_nat m - (of_nat n :: 'a::ring_1)"
+ "n \<le> m ==> of_nat (m - n) = of_nat m - (of_nat n :: 'a::ring_1)"
by (simp del: of_nat_add
add: compare_rls of_nat_add [symmetric] split add: nat_diff_split)
--- a/src/HOL/Power.thy Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Power.thy Tue Oct 23 23:27:23 2007 +0200
@@ -140,7 +140,7 @@
done
lemma power_eq_0_iff [simp]:
- "(a^n = 0) = (a = (0::'a::{ring_1_no_zero_divisors,recpower}) & n\<noteq>0)"
+ "(a^n = 0) = (a = (0::'a::{ring_1_no_zero_divisors,recpower}) & n>0)"
apply (induct "n")
apply (auto simp add: power_Suc zero_neq_one [THEN not_sym])
done
@@ -342,7 +342,7 @@
lemma nat_one_le_power [simp]: "1 \<le> i ==> Suc 0 \<le> i^n"
by (insert one_le_power [of i n], simp)
-lemma nat_zero_less_power_iff [simp]: "(x^n = 0) = (x = (0::nat) & n\<noteq>0)"
+lemma nat_zero_less_power_iff [simp]: "(x^n > 0) = (x > (0::nat) | n=0)"
by (induct "n", auto)
text{*Valid for the naturals, but what if @{text"0<i<1"}?
--- a/src/HOL/Real/RComplete.thy Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Real/RComplete.thy Tue Oct 23 23:27:23 2007 +0200
@@ -1208,10 +1208,10 @@
apply simp
done
-lemma natfloor_div_nat: "1 <= x ==> y \<noteq> 0 ==>
+lemma natfloor_div_nat: "1 <= x ==> y > 0 ==>
natfloor (x / real y) = natfloor x div y"
proof -
- assume "1 <= (x::real)" and "(y::nat) \<noteq> 0"
+ assume "1 <= (x::real)" and "(y::nat) > 0"
have "natfloor x = (natfloor x) div y * y + (natfloor x) mod y"
by simp
then have a: "real(natfloor x) = real ((natfloor x) div y) * real y +
--- a/src/HOL/Real/RealDef.thy Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Real/RealDef.thy Tue Oct 23 23:27:23 2007 +0200
@@ -746,7 +746,7 @@
lemma real_of_nat_diff: "n \<le> m ==> real (m - n) = real (m::nat) - real n"
by (simp add: add: real_of_nat_def of_nat_diff)
-lemma real_of_nat_gt_zero_cancel_iff [simp]: "(0 < real (n::nat)) = (n \<noteq> 0)"
+lemma real_of_nat_gt_zero_cancel_iff [simp]: "(0 < real (n::nat)) = (0 < n)"
by (auto simp: real_of_nat_def)
lemma real_of_nat_le_zero_cancel_iff [simp]: "(real (n::nat) \<le> 0) = (n = 0)"
--- a/src/HOL/ex/Reflected_Presburger.thy Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/ex/Reflected_Presburger.thy Tue Oct 23 23:27:23 2007 +0200
@@ -63,7 +63,7 @@
"fmsize (NDvd i t) = 2"
"fmsize p = 1"
(* several lemmas about fmsize *)
-lemma fmsize_pos: "fmsize p \<noteq> 0"
+lemma fmsize_pos: "fmsize p > 0"
by (induct p rule: fmsize.induct) simp_all
(* Semantics of formulae (fm) *)
@@ -114,7 +114,7 @@
"prep (Imp p q) = prep (Or (NOT p) q)"
"prep (Iff p q) = Or (prep (And p q)) (prep (And (NOT p) (NOT q)))"
"prep p = p"
-(hints simp add: fmsize_pos neq0_conv[symmetric])
+(hints simp add: fmsize_pos)
lemma prep: "Ifm bbs bs (prep p) = Ifm bbs bs p"
by (induct p arbitrary: bs rule: prep.induct, auto)
@@ -189,11 +189,11 @@
lemma numsubst0_I:
"Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b#bs) a)#bs) t"
-by (induct t rule: numsubst0.induct,auto dest: not0_implies_Suc)
+by (induct t rule: numsubst0.induct,auto simp:nth_Cons')
lemma numsubst0_I':
"numbound0 a \<Longrightarrow> Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b'#bs) a)#bs) t"
-by (induct t rule: numsubst0.induct, auto dest: not0_implies_Suc simp: numbound0_I[where b="b" and b'="b'"])
+by (induct t rule: numsubst0.induct, auto simp: nth_Cons' numbound0_I[where b="b" and b'="b'"])
primrec
"subst0 t T = T"