Eliminated most of the neq0_conv occurrences. As a result, many
theorems had to be rephrased with ~= 0 instead of > 0.
--- a/src/HOL/Algebra/Exponent.thy Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Algebra/Exponent.thy Sun Oct 21 14:53:44 2007 +0200
@@ -9,9 +9,8 @@
section {*The Combinatorial Argument Underlying the First Sylow Theorem*}
-constdefs
- exponent :: "[nat, nat] => nat"
- "exponent p s == if prime p then (GREATEST r. p^r dvd s) else 0"
+definition exponent :: "nat => nat => nat" where
+"exponent p s == if prime p then (GREATEST r. p^r dvd s) else 0"
subsection{*Prime Theorems*}
@@ -20,7 +19,7 @@
by (unfold prime_def, force)
lemma prime_iff:
- "(prime p) = (Suc 0 < p & (\<forall>a b. p dvd a*b --> (p dvd a) | (p dvd b)))"
+ "(prime p) = (Suc 0 < p & (\<forall>a b. p dvd a*b --> (p dvd a) | (p dvd b)))"
apply (auto simp add: prime_imp_one_less)
apply (blast dest!: prime_dvd_mult)
apply (auto simp add: prime_def)
@@ -40,8 +39,8 @@
lemma prime_dvd_cases:
- "[| p*k dvd m*n; prime p |]
- ==> (\<exists>x. k dvd x*n & m = p*x) | (\<exists>y. k dvd m*y & n = p*y)"
+ "[| p*k dvd m*n; prime p |]
+ ==> (\<exists>x. k dvd x*n & m = p*x) | (\<exists>y. k dvd m*y & n = p*y)"
apply (simp add: prime_iff)
apply (frule dvd_mult_left)
apply (subgoal_tac "p dvd m | p dvd n")
@@ -55,8 +54,8 @@
lemma prime_power_dvd_cases [rule_format (no_asm)]: "prime p
- ==> \<forall>m n. p^c dvd m*n -->
- (\<forall>a b. a+b = Suc c --> p^a dvd m | p^b dvd n)"
+ ==> \<forall>m n. p^c dvd m*n -->
+ (\<forall>a b. a+b = Suc c --> p^a dvd m | p^b dvd n)"
apply (induct_tac "c")
apply clarify
apply (case_tac "a")
@@ -85,8 +84,8 @@
(*needed in this form in Sylow.ML*)
lemma div_combine:
- "[| prime p; ~ (p ^ (Suc r) dvd n); p^(a+r) dvd n*k |]
- ==> p ^ a dvd k"
+ "[| prime p; ~ (p ^ (Suc r) dvd n); p^(a+r) dvd n*k |]
+ ==> p ^ a dvd k"
by (drule_tac a = "Suc r" and b = a in prime_power_dvd_cases, assumption, auto)
(*Lemma for power_dvd_bound*)
@@ -96,15 +95,12 @@
apply simp
apply (subgoal_tac "2 * n + 2 <= p * p^n", simp)
apply (subgoal_tac "2 * p^n <= p * p^n")
-(*?arith_tac should handle all of this!*)
-apply (rule order_trans)
-prefer 2 apply assumption
+apply arith
apply (drule_tac k = 2 in mult_le_mono2, simp)
-apply (rule mult_le_mono1, simp)
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; 0 < a|] ==> n < a"
+lemma power_dvd_bound: "[|p^n dvd a; Suc 0 < p; a \<noteq> 0|] ==> n < a"
apply (drule dvd_imp_le)
apply (drule_tac [2] n = n in Suc_le_power, auto)
done
@@ -113,13 +109,13 @@
subsection{*Exponent Theorems*}
lemma exponent_ge [rule_format]:
- "[|p^k dvd n; prime p; 0<n|] ==> k <= exponent p n"
+ "[|p^k dvd n; prime p; 0<n|] ==> k <= exponent p n"
apply (simp add: exponent_def)
apply (erule Greatest_le)
apply (blast dest: prime_imp_one_less power_dvd_bound)
done
-lemma power_exponent_dvd: "0<s ==> (p ^ exponent p s) dvd s"
+lemma power_exponent_dvd: "s\<noteq>0 ==> (p ^ exponent p s) dvd s"
apply (simp add: exponent_def)
apply clarify
apply (rule_tac k = 0 in GreatestI)
@@ -127,7 +123,7 @@
done
lemma power_Suc_exponent_Not_dvd:
- "[|(p * p ^ exponent p s) dvd s; prime p |] ==> s=0"
+ "[|(p * p ^ exponent p s) dvd s; prime p |] ==> s=0"
apply (subgoal_tac "p ^ Suc (exponent p s) dvd s")
prefer 2 apply simp
apply (rule ccontr)
@@ -141,7 +137,7 @@
done
lemma exponent_equalityI:
- "!r::nat. (p^r dvd a) = (p^r dvd b) ==> exponent p a = exponent p b"
+ "!r::nat. (p^r dvd a) = (p^r dvd b) ==> exponent p a = exponent p b"
by (simp (no_asm_simp) add: exponent_def)
lemma exponent_eq_0 [simp]: "\<not> prime p ==> exponent p s = 0"
@@ -149,9 +145,8 @@
(* exponent_mult_add, easy inclusion. Could weaken p \<in> prime to Suc 0 < p *)
-lemma exponent_mult_add1:
- "[| 0 < a; 0 < b |]
- ==> (exponent p a) + (exponent p b) <= exponent p (a * b)"
+lemma exponent_mult_add1: "[| a \<noteq> 0; b \<noteq> 0 |]
+ ==> (exponent p a) + (exponent p b) <= exponent p (a * b)"
apply (case_tac "prime p")
apply (rule exponent_ge)
apply (auto simp add: power_add)
@@ -159,8 +154,8 @@
done
(* exponent_mult_add, opposite inclusion *)
-lemma exponent_mult_add2: "[| 0 < a; 0 < b |]
- ==> exponent p (a * b) <= (exponent p a) + (exponent p b)"
+lemma exponent_mult_add2: "[| a \<noteq> 0; b \<noteq> 0 |]
+ ==> exponent p (a * b) <= (exponent p a) + (exponent p b)"
apply (case_tac "prime p")
apply (rule leI, clarify)
apply (cut_tac p = p and s = "a*b" in power_exponent_dvd, auto)
@@ -173,9 +168,8 @@
apply (blast dest: power_Suc_exponent_Not_dvd)
done
-lemma exponent_mult_add:
- "[| 0 < a; 0 < b |]
- ==> exponent p (a * b) = (exponent p a) + (exponent p b)"
+lemma exponent_mult_add: "[| a \<noteq> 0; b \<noteq> 0 |]
+ ==> exponent p (a * b) = (exponent p a) + (exponent p b)"
by (blast intro: exponent_mult_add1 exponent_mult_add2 order_antisym)
@@ -194,40 +188,41 @@
subsection{*Main Combinatorial Argument*}
-lemma le_extend_mult: "[| 0 < c; a <= b |] ==> a <= b * (c::nat)"
+lemma le_extend_mult: "[| c \<noteq> 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:
- "[| 0 < (m::nat); 0<k; k < p^a; (p^r) dvd (p^a)* m - k |] ==> r <= a"
+ "[| (m::nat) \<noteq> 0; k \<noteq> 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)
apply (drule less_imp_le [of a])
apply (drule le_imp_power_dvd)
apply (drule_tac n = "p ^ r" in dvd_trans, assumption)
-apply (metis dvd_diffD1 dvd_triv_right le_extend_mult linorder_linear linorder_not_less mult_commute nat_dvd_not_less)
+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: "[| 0 < (m::nat); 0<k; k < p^a; (p^r) dvd (p^a)* m - k |]
- ==> (p^r) dvd (p^a) - k"
+lemma p_fac_forw: "[| (m::nat) \<noteq> 0; k\<noteq>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")
prefer 2 apply (blast intro: dvd_mult2)
apply (drule dvd_diffD1)
apply assumption
prefer 2 apply (blast intro: dvd_diff)
-apply (drule less_imp_Suc_add, auto)
+apply (drule not0_implies_Suc, auto)
done
-lemma r_le_a_forw: "[| 0 < (k::nat); k < p^a; 0 < p; (p^r) dvd (p^a) - k |] ==> r <= a"
+lemma r_le_a_forw:
+ "[| (k::nat) \<noteq> 0; k < p^a; p\<noteq>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: "[| 0<m; 0<k; 0 < (p::nat); k < p^a; (p^r) dvd p^a - k |]
- ==> (p^r) dvd (p^a)*m - k"
+lemma p_fac_backw: "[| m\<noteq>0; k\<noteq>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")
prefer 2 apply (blast intro: dvd_mult2)
@@ -237,8 +232,8 @@
apply (drule less_imp_Suc_add, auto)
done
-lemma exponent_p_a_m_k_equation: "[| 0<m; 0<k; 0 < (p::nat); k < p^a |]
- ==> exponent p (p^a * m - k) = exponent p (p^a - k)"
+lemma exponent_p_a_m_k_equation: "[| m\<noteq>0; k\<noteq>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
@@ -247,14 +242,14 @@
(*The bound K is needed; otherwise it's too weak to be used.*)
lemma p_not_div_choose_lemma [rule_format]:
- "[| \<forall>i. Suc i < K --> exponent p (Suc i) = exponent p (Suc(j+i))|]
- ==> k<K --> exponent p ((j+k) choose k) = 0"
+ "[| \<forall>i. Suc i < K --> exponent p (Suc i) = exponent p (Suc(j+i))|]
+ ==> k<K --> exponent p ((j+k) choose k) = 0"
apply (case_tac "prime p")
prefer 2 apply simp
apply (induct_tac "k")
apply (simp (no_asm))
(*induction step*)
-apply (subgoal_tac "0 < (Suc (j+n) choose Suc n) ")
+apply (subgoal_tac "(Suc (j+n) choose Suc n) \<noteq> 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)")
@@ -271,9 +266,9 @@
(*The lemma above, with two changes of variables*)
lemma p_not_div_choose:
- "[| k<K; k<=n;
- \<forall>j. 0<j & j<K --> exponent p (n - k + (K - j)) = exponent p (K - j)|]
- ==> exponent p (n choose k) = 0"
+ "[| k<K; k<=n;
+ \<forall>j. 0<j & j<K --> exponent p (n - k + (K - j)) = exponent p (K - j)|]
+ ==> exponent p (n choose k) = 0"
apply (cut_tac j = "n-k" and k = k and p = p in p_not_div_choose_lemma)
prefer 3 apply simp
prefer 2 apply assumption
@@ -283,7 +278,7 @@
lemma const_p_fac_right:
- "0 < m ==> exponent p ((p^a * m - Suc 0) choose (p^a - Suc 0)) = 0"
+ "m\<noteq>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)
@@ -301,7 +296,7 @@
done
lemma const_p_fac:
- "0 < m ==> exponent p (((p^a) * m) choose p^a) = exponent p m"
+ "m\<noteq>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 Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Algebra/Sylow.thy Sun Oct 21 14:53:44 2007 +0200
@@ -126,7 +126,7 @@
apply (blast intro: one_closed zero_less_card_empty)
done
-lemma (in sylow) zero_less_m: "0 < m"
+lemma (in sylow) zero_less_m: "m \<noteq> 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: "0 < card calM"
+lemma (in sylow) zero_less_card_calM: "card calM \<noteq> 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/Auth/Guard/Guard.thy Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Auth/Guard/Guard.thy Sun Oct 21 14:53:44 2007 +0200
@@ -187,7 +187,7 @@
subsection{*basic facts about @{term crypt_nb}*}
-lemma non_empty_crypt_msg: "Crypt K Y:parts {X} ==> 0 < crypt_nb X"
+lemma non_empty_crypt_msg: "Crypt K Y:parts {X} ==> crypt_nb X \<noteq> 0"
by (induct X, simp_all, safe, simp_all)
subsection{*number of Crypt's in a message list*}
@@ -216,7 +216,7 @@
cnb l = (cnb l - crypt_nb Z) + crypt_nb Z"
by (erule parts.induct, auto simp: in_set_conv_decomp)
-lemma non_empty_crypt: "Crypt K Y:parts (set l) ==> 0 < cnb l"
+lemma non_empty_crypt: "Crypt K Y:parts (set l) ==> cnb l \<noteq> 0"
by (induct l, auto dest: non_empty_crypt_msg parts_insert_substD)
subsection{*list of kparts*}
--- a/src/HOL/Auth/Guard/GuardK.thy Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Auth/Guard/GuardK.thy Sun Oct 21 14:53:44 2007 +0200
@@ -183,7 +183,7 @@
subsection{*basic facts about @{term crypt_nb}*}
-lemma non_empty_crypt_msg: "Crypt K Y:parts {X} ==> 0 < crypt_nb X"
+lemma non_empty_crypt_msg: "Crypt K Y:parts {X} ==> crypt_nb X \<noteq> 0"
by (induct X, simp_all, safe, simp_all)
subsection{*number of Crypt's in a message list*}
@@ -212,7 +212,7 @@
cnb l = (cnb l - crypt_nb Z) + crypt_nb Z"
by (erule parts.induct, auto simp: in_set_conv_decomp)
-lemma non_empty_crypt: "Crypt K Y:parts (set l) ==> 0 < cnb l"
+lemma non_empty_crypt: "Crypt K Y:parts (set l) ==> cnb l \<noteq> 0"
by (induct l, auto dest: non_empty_crypt_msg parts_insert_substD)
subsection{*list of kparts*}
--- a/src/HOL/Auth/Kerberos_BAN.thy Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Auth/Kerberos_BAN.thy Sun Oct 21 14:53:44 2007 +0200
@@ -35,7 +35,7 @@
text{*The authenticator only for one journey*}
specification (authlife)
- authlife_LB [iff]: "0 < authlife"
+ authlife_LB [iff]: "authlife \<noteq> 0"
by blast
abbreviation
@@ -133,7 +133,7 @@
apply (rule_tac [2]
bankerberos.Nil [THEN bankerberos.BK1, THEN bankerberos.BK2,
THEN bankerberos.BK3, THEN bankerberos.BK4])
-apply (possibility, simp_all (no_asm_simp) add: used_Cons neq0_conv)
+apply (possibility, simp_all (no_asm_simp) add: used_Cons)
done
subsection{*Lemmas for reasoning about predicate "Issues"*}
--- a/src/HOL/Complex/ex/MIR.thy Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Complex/ex/MIR.thy Sun Oct 21 14:53:44 2007 +0200
@@ -268,7 +268,7 @@
| "fmsize (NDvd i t) = 2"
| "fmsize p = 1"
(* several lemmas about fmsize *)
-lemma fmsize_pos: "fmsize p > 0"
+lemma fmsize_pos: "fmsize p \<noteq> 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)
+(hints simp add: fmsize_pos neq0_conv[symmetric])
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 Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Complex/ex/ReflectedFerrack.thy Sun Oct 21 14:53:44 2007 +0200
@@ -106,7 +106,7 @@
"fmsize (A p) = 4+ fmsize p"
"fmsize p = 1"
(* several lemmas about fmsize *)
-lemma fmsize_pos: "fmsize p > 0"
+lemma fmsize_pos: "fmsize p \<noteq> 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)
+(hints simp add: fmsize_pos neq0_conv[symmetric])
lemma prep: "\<And> bs. Ifm bs (prep p) = Ifm bs p"
by (induct p rule: prep.induct, auto)
--- a/src/HOL/Divides.thy Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Divides.thy Sun Oct 21 14:53:44 2007 +0200
@@ -250,13 +250,13 @@
apply (simp add: quorem_def)
done
-lemma quorem_div_mod: "0 < b ==> quorem ((a, b), (a div b, a mod b))"
+lemma quorem_div_mod: "b \<noteq> 0 ==> quorem ((a, b), (a div b, a mod b))"
unfolding quorem_def by simp
-lemma quorem_div: "[| quorem((a,b),(q,r)); 0 < b |] ==> a div b = q"
+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_mod: "[| quorem((a,b),(q,r)); 0 < b |] ==> a mod b = r"
+lemma quorem_mod: "[| quorem((a,b),(q,r)); b \<noteq> 0 |] ==> a mod b = r"
by (simp add: quorem_div_mod [THEN unique_remainder])
(** A dividend of zero **)
@@ -270,21 +270,19 @@
(** proving (a*b) div c = a * (b div c) + a * (b mod c) **)
lemma quorem_mult1_eq:
- "[| quorem((b,c),(q,r)); 0 < c |]
+ "[| 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)
lemma div_mult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::nat)"
- apply (cases "c = 0", simp add: neq0_conv)
- using neq0_conv
- apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_div])
- done
+apply (cases "c = 0", simp)
+apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_div])
+done
lemma mod_mult1_eq: "(a*b) mod c = a*(b mod c) mod (c::nat)"
- apply (cases "c = 0", simp add: neq0_conv)
- using neq0_conv
- apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_mod])
- done
+apply (cases "c = 0", simp)
+apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_mod])
+done
lemma mod_mult1_eq': "(a*b) mod (c::nat) = ((a mod c) * b) mod c"
apply (rule trans)
@@ -301,23 +299,21 @@
(** 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)); 0 < c |]
+ "[| 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)
(*NOT suitable for rewriting: the RHS has an instance of the LHS*)
lemma div_add1_eq:
- "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
- apply (cases "c = 0", simp)
- using neq0_conv
- apply (blast intro: quorem_add1_eq [THEN quorem_div] quorem_div_mod quorem_div_mod)
- done
+ "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
+apply (cases "c = 0", simp)
+apply (blast intro: quorem_add1_eq [THEN quorem_div] quorem_div_mod)
+done
lemma mod_add1_eq: "(a+b) mod (c::nat) = (a mod c + b mod c) mod c"
- apply (cases "c = 0", simp)
- using neq0_conv
- apply (blast intro: quorem_div_mod quorem_div_mod quorem_add1_eq [THEN quorem_mod])
- done
+apply (cases "c = 0", simp)
+apply (blast intro: quorem_div_mod quorem_add1_eq [THEN quorem_mod])
+done
subsection{*Proving @{term "a div (b*c) = (a div b) div c"}*}
--- a/src/HOL/Hyperreal/Fact.thy Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Hyperreal/Fact.thy Sun Oct 21 14:53:44 2007 +0200
@@ -17,60 +17,60 @@
lemma fact_gt_zero [simp]: "0 < fact n"
- by (induct n) auto
+by (induct n) auto
lemma fact_not_eq_zero [simp]: "fact n \<noteq> 0"
- by (simp add: neq0_conv)
+by (simp add: neq0_conv)
lemma real_of_nat_fact_not_zero [simp]: "real (fact n) \<noteq> 0"
- by auto
+by auto
lemma real_of_nat_fact_gt_zero [simp]: "0 < real(fact n)"
- by auto
+by auto
lemma real_of_nat_fact_ge_zero [simp]: "0 \<le> real(fact n)"
- by simp
+by simp
lemma fact_ge_one [simp]: "1 \<le> fact n"
- by (induct n) auto
+by (induct n) auto
lemma fact_mono: "m \<le> n ==> fact m \<le> fact n"
- apply (drule le_imp_less_or_eq)
- apply (auto dest!: less_imp_Suc_add)
- apply (induct_tac k, auto)
- done
+apply (drule le_imp_less_or_eq)
+apply (auto dest!: less_imp_Suc_add)
+apply (induct_tac k, auto)
+done
text{*Note that @{term "fact 0 = fact 1"}*}
lemma fact_less_mono: "[| 0 < m; m < n |] ==> fact m < fact n"
- apply (drule_tac m = m in less_imp_Suc_add, auto)
- apply (induct_tac k, auto)
- done
+apply (drule_tac m = m in less_imp_Suc_add, auto)
+apply (induct_tac k, auto)
+done
lemma inv_real_of_nat_fact_gt_zero [simp]: "0 < inverse (real (fact n))"
- by (auto simp add: positive_imp_inverse_positive)
+by (auto simp add: positive_imp_inverse_positive)
lemma inv_real_of_nat_fact_ge_zero [simp]: "0 \<le> inverse (real (fact n))"
- by (auto intro: order_less_imp_le)
+by (auto intro: order_less_imp_le)
lemma fact_diff_Suc [rule_format]:
- "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
- apply (induct n arbitrary: m)
- apply auto
- apply (drule_tac x = "m - 1" in meta_spec, auto)
- done
+ "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
+apply (induct n arbitrary: m)
+apply auto
+apply (drule_tac x = "m - 1" in meta_spec, auto)
+done
lemma fact_num0 [simp]: "fact 0 = 1"
- by auto
+by auto
lemma fact_num_eq_if: "fact m = (if m=0 then 1 else m * fact (m - 1))"
- by (cases m) auto
+by (cases m) auto
lemma fact_add_num_eq_if:
- "fact (m + n) = (if m + n = 0 then 1 else (m + n) * fact (m + n - 1))"
- by (cases "m + n") auto
+ "fact (m + n) = (if m + n = 0 then 1 else (m + n) * fact (m + n - 1))"
+by (cases "m + n") auto
lemma fact_add_num_eq_if2:
- "fact (m + n) = (if m = 0 then fact n else (m + n) * fact ((m - 1) + n))"
- by (cases m) auto
+ "fact (m + n) = (if m = 0 then fact n else (m + n) * fact ((m - 1) + n))"
+by (cases m) auto
end
--- a/src/HOL/Hyperreal/Integration.thy Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Hyperreal/Integration.thy Sun Oct 21 14:53:44 2007 +0200
@@ -149,14 +149,13 @@
apply (rule_tac t = a in partition_lhs [THEN subst], assumption)
apply (cut_tac x = "Suc n" and y = "psize D" in linorder_le_less_linear)
apply (frule partition [THEN iffD1], safe)
-using neq0_conv
apply (blast intro: partition_lt less_le_trans)
apply (rotate_tac 3)
apply (drule_tac x = "Suc n" in spec)
apply (erule impE)
apply (erule less_imp_le)
-apply (frule partition_rhs, simp only: neq0_conv)
-apply (drule partition_gt, assumption)
+apply (frule partition_rhs)
+apply (drule partition_gt[of _ _ _ 0], arith)
apply (simp (no_asm_simp))
done
--- a/src/HOL/Hyperreal/MacLaurin.thy Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Hyperreal/MacLaurin.thy Sun Oct 21 14:53:44 2007 +0200
@@ -114,7 +114,7 @@
done
lemma Maclaurin:
- "[| 0 < h; 0 < n; diff 0 = f;
+ "[| 0 < h; n \<noteq> 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,13 +185,11 @@
done
lemma Maclaurin_objl:
- "0 < h & 0 < n & 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) +
- diff n t / real (fact n) * h ^ n)"
+ "0 < h & n\<noteq>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) +
+ diff n t / real (fact n) * h ^ n)"
by (blast intro: Maclaurin)
@@ -220,7 +218,7 @@
by (blast intro: Maclaurin2)
lemma Maclaurin_minus:
- "[| h < 0; 0 < n; diff 0 = f;
+ "[| h < 0; n \<noteq> 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 &
@@ -247,7 +245,7 @@
done
lemma Maclaurin_minus_objl:
- "(h < 0 & 0 < n & diff 0 = f &
+ "(h < 0 & n \<noteq> 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 &
@@ -263,10 +261,10 @@
(* not good for PVS sin_approx, cos_approx *)
lemma Maclaurin_bi_le_lemma [rule_format]:
- "0 < n \<longrightarrow>
- diff 0 0 =
- (\<Sum>m = 0..<n. diff m 0 * 0 ^ m / real (fact m)) +
- diff n 0 * 0 ^ n / real (fact n)"
+ "n\<noteq>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)"
by (induct "n", auto)
lemma Maclaurin_bi_le:
@@ -278,17 +276,17 @@
diff n t / real (fact n) * x ^ n"
apply (case_tac "n = 0", force)
apply (case_tac "x = 0")
-apply (rule_tac x = 0 in exI)
-apply (force simp add: neq0_conv Maclaurin_bi_le_lemma)
-apply (cut_tac x = x and y = 0 in linorder_less_linear, auto simp add: neq0_conv)
-txt{*Case 1, where @{term "x < 0"}*}
-apply (cut_tac f = "diff 0" and diff = diff and h = x and n = n in Maclaurin_minus_objl, safe)
-apply (simp add: abs_if neq0_conv)
-apply (rule_tac x = t in exI)
-apply (simp add: abs_if)
+ apply (rule_tac x = 0 in exI)
+ apply (force simp add: Maclaurin_bi_le_lemma)
+apply (cut_tac x = x and y = 0 in linorder_less_linear, auto)
+ txt{*Case 1, where @{term "x < 0"}*}
+ apply (cut_tac f = "diff 0" and diff = diff and h = x and n = n in Maclaurin_minus_objl, safe)
+ apply (simp add: abs_if)
+ apply (rule_tac x = t in exI)
+ apply (simp add: abs_if)
txt{*Case 2, where @{term "0 < x"}*}
apply (cut_tac f = "diff 0" and diff = diff and h = x and n = n in Maclaurin_objl, safe)
-apply (simp add: abs_if)
+ apply (simp add: abs_if)
apply (rule_tac x = t in exI)
apply (simp add: abs_if)
done
@@ -296,7 +294,7 @@
lemma Maclaurin_all_lt:
"[| diff 0 = f;
\<forall>m x. DERIV (diff m) x :> diff(Suc m) x;
- x ~= 0; 0 < n
+ x ~= 0; n \<noteq> 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"
@@ -310,7 +308,7 @@
lemma Maclaurin_all_lt_objl:
"diff 0 = f &
(\<forall>m x. DERIV (diff m) x :> diff(Suc m) x) &
- x ~= 0 & 0 < n
+ x ~= 0 & n \<noteq> 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)"
@@ -318,7 +316,7 @@
lemma Maclaurin_zero [rule_format]:
"x = (0::real)
- ==> 0 < n -->
+ ==> n \<noteq> 0 -->
(\<Sum>m=0..<n. (diff m (0::real) / real (fact m)) * x ^ m) =
diff 0 0"
by (induct n, auto)
@@ -328,11 +326,11 @@
|] ==> \<exists>t. abs t \<le> abs x &
f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
(diff n t / real (fact n)) * x ^ n"
-apply (insert linorder_le_less_linear [of n 0])
-apply (erule disjE, force)
+apply(cases "n=0")
+apply (force)
apply (case_tac "x = 0")
apply (frule_tac diff = diff and n = n in Maclaurin_zero, assumption)
-apply (drule gr_implies_not0 [THEN not0_implies_Suc])
+apply (drule not0_implies_Suc)
apply (rule_tac x = 0 in exI, force)
apply (frule_tac diff = diff and n = n in Maclaurin_all_lt, auto)
apply (rule_tac x = t in exI, auto)
@@ -348,7 +346,7 @@
subsection{*Version for Exponential Function*}
-lemma Maclaurin_exp_lt: "[| x ~= 0; 0 < n |]
+lemma Maclaurin_exp_lt: "[| x ~= 0; n \<noteq> 0 |]
==> (\<exists>t. 0 < abs t &
abs t < abs x &
exp x = (\<Sum>m=0..<n. (x ^ m) / real (fact m)) +
@@ -375,19 +373,19 @@
done
lemma mod_exhaust_less_4:
- "m mod 4 = 0 | m mod 4 = 1 | m mod 4 = 2 | m mod 4 = (3::nat)"
+ "m mod 4 = 0 | m mod 4 = 1 | m mod 4 = 2 | m mod 4 = (3::nat)"
by auto
lemma Suc_Suc_mult_two_diff_two [rule_format, simp]:
- "0 < n --> Suc (Suc (2 * n - 2)) = 2*n"
+ "n\<noteq>0 --> Suc (Suc (2 * n - 2)) = 2*n"
by (induct "n", auto)
lemma lemma_Suc_Suc_4n_diff_2 [rule_format, simp]:
- "0 < n --> Suc (Suc (4*n - 2)) = 4*n"
+ "n\<noteq>0 --> Suc (Suc (4*n - 2)) = 4*n"
by (induct "n", auto)
lemma Suc_mult_two_diff_one [rule_format, simp]:
- "0 < n --> Suc (2 * n - 1) = 2*n"
+ "n\<noteq>0 --> Suc (2 * n - 1) = 2*n"
by (induct "n", auto)
@@ -427,7 +425,7 @@
lemma Maclaurin_sin_expansion3:
- "[| 0 < n; 0 < x |] ==>
+ "[| n \<noteq> 0; 0 < x |] ==>
\<exists>t. 0 < t & t < x &
sin x =
(\<Sum>m=0..<n. (if even m then 0
@@ -493,7 +491,7 @@
done
lemma Maclaurin_cos_expansion2:
- "[| 0 < x; 0 < n |] ==>
+ "[| 0 < x; n \<noteq> 0 |] ==>
\<exists>t. 0 < t & t < x &
cos x =
(\<Sum>m=0..<n. (if even m
@@ -512,7 +510,7 @@
done
lemma Maclaurin_minus_cos_expansion:
- "[| x < 0; 0 < n |] ==>
+ "[| x < 0; n \<noteq> 0 |] ==>
\<exists>t. x < t & t < 0 &
cos x =
(\<Sum>m=0..<n. (if even m
--- a/src/HOL/Hyperreal/Poly.thy Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Hyperreal/Poly.thy Sun Oct 21 14:53:44 2007 +0200
@@ -589,15 +589,14 @@
declare real_mult_zero_disj_iff [simp]
lemma pderiv_aux_iszero [rule_format, simp]:
- "\<forall>n. list_all (%c. c = 0) (pderiv_aux (Suc n) p) = list_all (%c. c = 0) p"
+ "\<forall>n. list_all (%c. c = 0) (pderiv_aux (Suc n) p) = list_all (%c. c = 0) p"
by (induct "p", auto)
lemma pderiv_aux_iszero_num: "(number_of n :: nat) \<noteq> 0
- ==> (list_all (%c. c = 0) (pderiv_aux (number_of n) p) =
+ ==> (list_all (%c. c = 0) (pderiv_aux (number_of n) p) =
list_all (%c. c = 0) p)"
-unfolding neq0_conv
-apply (rule_tac n1 = "number_of n" and m1 = 0 in less_imp_Suc_add [THEN exE], force)
-apply (rule_tac n1 = "0 + x" in pderiv_aux_iszero [THEN subst])
+apply(drule not0_implies_Suc, clarify)
+apply (rule_tac n1 = "m" in pderiv_aux_iszero [THEN subst])
apply (simp (no_asm_simp) del: pderiv_aux_iszero)
done
@@ -783,7 +782,7 @@
declare pexp_one [simp]
lemma lemma_order_root [rule_format]:
- "\<forall>p a. 0 < n & [- a, 1] %^ n divides p & ~ [- a, 1] %^ (Suc n) divides p
+ "\<forall>p a. n \<noteq> 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)
@@ -794,8 +793,7 @@
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 neq0_conv del: pmult_Cons, blast)
-using neq0_conv
+apply (simp add: divides_def poly_mult fun_eq del: pmult_Cons, blast)
apply (blast intro: lemma_order_root)
done
@@ -845,7 +843,7 @@
(* FIXME: too too long! *)
lemma lemma_order_pderiv [rule_format]:
- "\<forall>p q a. 0 < n &
+ "\<forall>p q a. n \<noteq> 0 &
poly (pderiv p) \<noteq> poly [] &
poly p = poly ([- a, 1] %^ n *** q) & ~ [- a, 1] divides q
--> n = Suc (order a (pderiv p))"
@@ -876,7 +874,7 @@
(poly qa xa + - poly (pderiv q) xa) *
(poly ([- a, 1] %^ n) xa *
((- a + xa) * (inverse (real (Suc n)) * real (Suc n))))")
-apply (simp only: mult_ac)
+apply (simp only: mult_ac)
apply (rotate_tac 2)
apply (drule_tac x = xa in spec)
apply (simp add: left_distrib mult_ac del: pmult_Cons)
@@ -885,7 +883,7 @@
lemma order_pderiv: "[| poly (pderiv p) \<noteq> poly []; order a p \<noteq> 0 |]
==> (order a p = Suc (order a (pderiv p)))"
apply (case_tac "poly p = poly []")
-apply (auto simp add: neq0_conv dest: pderiv_zero)
+apply (auto dest: pderiv_zero)
apply (drule_tac a = a and p = p in order_decomp)
apply (blast intro: lemma_order_pderiv)
done
--- a/src/HOL/Hyperreal/Taylor.thy Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Hyperreal/Taylor.thy Sun Oct 21 14:53:44 2007 +0200
@@ -15,7 +15,7 @@
*}
lemma taylor_up:
- assumes INIT: "0 < n" "diff 0 = f"
+ assumes INIT: "n\<noteq>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,7 +24,7 @@
proof -
from INTERV have "0 < b-c" by arith
moreover
- from INIT have "0<n" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto
+ from INIT have "n\<noteq>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)"
proof (intro strip)
@@ -57,7 +57,7 @@
qed
lemma taylor_down:
- assumes INIT: "0 < n" "diff 0 = f"
+ assumes INIT: "n\<noteq>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 "0<n" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto
+ from INIT have "n\<noteq>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: "0 < n" "diff 0 = f"
+ assumes INIT: "n\<noteq>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/IntDiv.thy Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/IntDiv.thy Sun Oct 21 14:53:44 2007 +0200
@@ -1316,34 +1316,34 @@
theorem ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
- apply (simp split add: split_nat)
- apply (rule iffI)
- apply (erule exE)
- apply (rule_tac x = "int x" in exI)
- apply simp
- apply (erule exE)
- apply (rule_tac x = "nat x" in exI)
- apply (erule conjE)
- apply (erule_tac x = "nat x" in allE)
- apply simp
- done
+apply (simp split add: split_nat)
+apply (rule iffI)
+apply (erule exE)
+apply (rule_tac x = "int x" in exI)
+apply simp
+apply (erule exE)
+apply (rule_tac x = "nat x" in exI)
+apply (erule conjE)
+apply (erule_tac x = "nat x" in allE)
+apply simp
+done
theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
- apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric]
+apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric]
nat_0_le cong add: conj_cong)
- apply (rule iffI)
- apply iprover
- apply (erule exE)
- apply (case_tac "x=0")
- apply (rule_tac x=0 in exI)
- apply simp
- apply (case_tac "0 \<le> k")
- apply iprover
- apply (simp add: neq0_conv linorder_not_le)
- apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
- apply assumption
- apply (simp add: mult_ac)
- done
+apply (rule iffI)
+apply iprover
+apply (erule exE)
+apply (case_tac "x=0")
+apply (rule_tac x=0 in exI)
+apply simp
+apply (case_tac "0 \<le> k")
+apply iprover
+apply (simp add: neq0_conv linorder_not_le)
+apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
+apply assumption
+apply (simp add: mult_ac)
+done
lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
proof
--- a/src/HOL/Library/Binomial.thy Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Library/Binomial.thy Sun Oct 21 14:53:44 2007 +0200
@@ -21,50 +21,50 @@
(if k = 0 then 1 else (n choose (k - 1)) + (n choose k))"
lemma binomial_n_0 [simp]: "(n choose 0) = 1"
- by (cases n) simp_all
+by (cases n) simp_all
lemma binomial_0_Suc [simp]: "(0 choose Suc k) = 0"
- by simp
+by simp
lemma binomial_Suc_Suc [simp]:
- "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)"
- by simp
+ "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)"
+by simp
lemma binomial_eq_0: "!!k. n < k ==> (n choose k) = 0"
- by (induct n) auto
+by (induct n) auto
declare binomial_0 [simp del] binomial_Suc [simp del]
lemma binomial_n_n [simp]: "(n choose n) = 1"
- by (induct n) (simp_all add: binomial_eq_0)
+by (induct n) (simp_all add: binomial_eq_0)
lemma binomial_Suc_n [simp]: "(Suc n choose n) = Suc n"
- by (induct n) simp_all
+by (induct n) simp_all
lemma binomial_1 [simp]: "(n choose Suc 0) = n"
- by (induct n) simp_all
+by (induct n) simp_all
-lemma zero_less_binomial: "k \<le> n ==> 0 < (n choose k)"
- by (induct n k rule: diff_induct) simp_all
+lemma zero_less_binomial: "k \<le> n ==> (n choose k) \<noteq> 0"
+by (induct n k rule: 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: neq0_conv zero_less_binomial)
- done
+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: neq0_conv linorder_not_less [symmetric] binomial_eq_0_iff [symmetric])
+lemma zero_less_binomial_iff: "(n choose k \<noteq> 0) = (k\<le>n)"
+by (simp add: linorder_not_less binomial_eq_0_iff)
(*Might be more useful if re-oriented*)
lemma Suc_times_binomial_eq:
- "!!k. k \<le> n ==> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k"
- apply (induct n)
- apply (simp add: binomial_0)
- apply (case_tac k)
- apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq
+ "!!k. k \<le> n ==> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k"
+apply (induct n)
+apply (simp add: binomial_0)
+apply (case_tac k)
+apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq
binomial_eq_0)
- done
+done
text{*This is the well-known version, but it's harder to use because of the
need to reason about division.*}
--- a/src/HOL/Library/Multiset.thy Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Library/Multiset.thy Sun Oct 21 14:53:44 2007 +0200
@@ -11,7 +11,7 @@
subsection {* The type of multisets *}
-typedef 'a multiset = "{f::'a => nat. finite {x . 0 < f x}}"
+typedef 'a multiset = "{f::'a => nat. finite {x . f x \<noteq> 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 == 0 < count M a"
+ "a :# M == count M a \<noteq> 0"
syntax
"_MCollect" :: "pttrn => 'a multiset => bool => 'a multiset" ("(1{# _ : _./ _#})")
@@ -300,7 +300,7 @@
lemma rep_multiset_induct_aux:
assumes 1: "P (\<lambda>a. (0::nat))"
and 2: "!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1))"
- shows "\<forall>f. f \<in> multiset --> setsum f {x. 0 < f x} = n --> P f"
+ shows "\<forall>f. f \<in> multiset --> setsum f {x. f x \<noteq> 0} = n --> P f"
apply (unfold multiset_def)
apply (induct_tac n, simp, clarify)
apply (subgoal_tac "f = (\<lambda>a.0)")
@@ -309,7 +309,7 @@
apply (rule ext, force, clarify)
apply (frule setsum_SucD, clarify)
apply (rename_tac a)
- apply (subgoal_tac "finite {x. 0 < (f (a := f a - 1)) x}")
+ apply (subgoal_tac "finite {x. (f (a := f a - 1)) x \<noteq> 0}")
prefer 2
apply (rule finite_subset)
prefer 2
@@ -323,10 +323,10 @@
apply (erule ssubst, rule 2 [unfolded multiset_def], blast)
apply (erule allE, erule impE, erule_tac [2] mp, blast)
apply (simp (no_asm_simp) add: setsum_decr del: fun_upd_apply One_nat_def)
- apply (subgoal_tac "{x. x \<noteq> a --> 0 < f x} = {x. 0 < f x}")
+ apply (subgoal_tac "{x. x \<noteq> a --> f x \<noteq> 0} = {x. f x \<noteq> 0}")
prefer 2
apply blast
- apply (subgoal_tac "{x. x \<noteq> a \<and> 0 < f x} = {x. 0 < f x} - {a}")
+ apply (subgoal_tac "{x. x \<noteq> a \<and> f x \<noteq> 0} = {x. f x \<noteq> 0} - {a}")
prefer 2
apply blast
apply (simp add: le_imp_diff_is_add setsum_diff1_nat cong: conj_cong)
--- a/src/HOL/Library/Nat_Infinity.thy Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Library/Nat_Infinity.thy Sun Oct 21 14:53:44 2007 +0200
@@ -51,132 +51,132 @@
subsection "Constructors"
lemma Fin_0: "Fin 0 = 0"
- by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
lemma Infty_ne_i0 [simp]: "\<infinity> \<noteq> 0"
- by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
lemma i0_ne_Infty [simp]: "0 \<noteq> \<infinity>"
- by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
lemma iSuc_Fin [simp]: "iSuc (Fin n) = Fin (Suc n)"
- by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
lemma iSuc_Infty [simp]: "iSuc \<infinity> = \<infinity>"
- by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
lemma iSuc_ne_0 [simp]: "iSuc n \<noteq> 0"
- by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
lemma iSuc_inject [simp]: "(iSuc x = iSuc y) = (x = y)"
- by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
subsection "Ordering relations"
lemma Infty_ilessE [elim!]: "\<infinity> < Fin m ==> R"
- by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
lemma iless_linear: "m < n \<or> m = n \<or> n < (m::inat)"
- by (simp add: inat_defs split:inat_splits, arith)
+by (simp add: inat_defs split:inat_splits, arith)
lemma iless_not_refl [simp]: "\<not> n < (n::inat)"
- by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
lemma iless_trans: "i < j ==> j < k ==> i < (k::inat)"
- by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
lemma iless_not_sym: "n < m ==> \<not> m < (n::inat)"
- by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
lemma Fin_iless_mono [simp]: "(Fin n < Fin m) = (n < m)"
- by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
lemma Fin_iless_Infty [simp]: "Fin n < \<infinity>"
- by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
lemma Infty_eq [simp]: "(n < \<infinity>) = (n \<noteq> \<infinity>)"
- by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
lemma i0_eq [simp]: "((0::inat) < n) = (n \<noteq> 0)"
- by (simp add: neq0_conv inat_defs split:inat_splits)
+by (fastsimp simp: inat_defs split:inat_splits)
lemma i0_iless_iSuc [simp]: "0 < iSuc n"
- by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
lemma not_ilessi0 [simp]: "\<not> n < (0::inat)"
- by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
lemma Fin_iless: "n < Fin m ==> \<exists>k. n = Fin k"
- by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
lemma iSuc_mono [simp]: "(iSuc n < iSuc m) = (n < m)"
- by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
lemma ile_def2: "(m \<le> n) = (m < n \<or> m = (n::inat))"
- by (simp add: inat_defs split:inat_splits, arith)
+by (simp add: inat_defs split:inat_splits, arith)
lemma ile_refl [simp]: "n \<le> (n::inat)"
- by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
lemma ile_trans: "i \<le> j ==> j \<le> k ==> i \<le> (k::inat)"
- by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
lemma ile_iless_trans: "i \<le> j ==> j < k ==> i < (k::inat)"
- by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
lemma iless_ile_trans: "i < j ==> j \<le> k ==> i < (k::inat)"
- by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
lemma Infty_ub [simp]: "n \<le> \<infinity>"
- by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
lemma i0_lb [simp]: "(0::inat) \<le> n"
- by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
lemma Infty_ileE [elim!]: "\<infinity> \<le> Fin m ==> R"
- by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
lemma Fin_ile_mono [simp]: "(Fin n \<le> Fin m) = (n \<le> m)"
- by (simp add: inat_defs split:inat_splits, arith)
+by (simp add: inat_defs split:inat_splits, arith)
lemma ilessI1: "n \<le> m ==> n \<noteq> m ==> n < (m::inat)"
- by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
lemma ileI1: "m < n ==> iSuc m \<le> n"
- by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
lemma Suc_ile_eq: "(Fin (Suc m) \<le> n) = (Fin m < n)"
- by (simp add: inat_defs split:inat_splits, arith)
+by (simp add: inat_defs split:inat_splits, arith)
lemma iSuc_ile_mono [simp]: "(iSuc n \<le> iSuc m) = (n \<le> m)"
- by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
lemma iless_Suc_eq [simp]: "(Fin m < iSuc n) = (Fin m \<le> n)"
- by (simp add: inat_defs split:inat_splits, arith)
+by (simp add: inat_defs split:inat_splits, arith)
lemma not_iSuc_ilei0 [simp]: "\<not> iSuc n \<le> 0"
- by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
lemma ile_iSuc [simp]: "n \<le> iSuc n"
- by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
lemma Fin_ile: "n \<le> Fin m ==> \<exists>k. n = Fin k"
- by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j ==> \<exists>j. Fin k < Y j"
- apply (induct_tac k)
- apply (simp (no_asm) only: Fin_0)
- apply (fast intro: ile_iless_trans i0_lb)
- apply (erule exE)
- apply (drule spec)
- apply (erule exE)
- apply (drule ileI1)
- apply (rule iSuc_Fin [THEN subst])
- apply (rule exI)
- apply (erule (1) ile_iless_trans)
- done
+apply (induct_tac k)
+ apply (simp (no_asm) only: Fin_0)
+ apply (fast intro: ile_iless_trans i0_lb)
+apply (erule exE)
+apply (drule spec)
+apply (erule exE)
+apply (drule ileI1)
+apply (rule iSuc_Fin [THEN subst])
+apply (rule exI)
+apply (erule (1) ile_iless_trans)
+done
end
--- a/src/HOL/Library/Parity.thy Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Library/Parity.thy Sun Oct 21 14:53:44 2007 +0200
@@ -222,7 +222,7 @@
apply (subst power_add)
apply (subst zero_le_mult_iff)
apply auto
- apply (subgoal_tac "x = 0 & 0 < y")
+ apply (subgoal_tac "x = 0 & y \<noteq> 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 Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Library/Word.thy Sun Oct 21 14:53:44 2007 +0200
@@ -412,21 +412,22 @@
thus ?thesis ..
qed
-lemma nat_to_bv_non0 [simp]: "0 < n ==> nat_to_bv n = nat_to_bv (n div 2) @ [if n mod 2 = 0 then \<zero> else \<one>]"
+lemma nat_to_bv_non0 [simp]: "n\<noteq>0 ==> nat_to_bv n = nat_to_bv (n div 2) @ [if n mod 2 = 0 then \<zero> else \<one>]"
proof -
- assume [simp]: "0 < n"
+ assume [simp]: "n\<noteq>0"
show ?thesis
apply (subst nat_to_bv_def [of n])
apply (simp only: nat_to_bv_helper.simps [of n])
apply (subst unfold_nat_to_bv_helper)
using prems
- apply (simp add: neq0_conv)
+ apply (simp)
apply (subst nat_to_bv_def [of "n div 2"])
apply auto
done
qed
-lemma bv_to_nat_dist_append: "bv_to_nat (l1 @ l2) = bv_to_nat l1 * 2 ^ length l2 + bv_to_nat l2"
+lemma bv_to_nat_dist_append:
+ "bv_to_nat (l1 @ l2) = bv_to_nat l1 * 2 ^ length l2 + bv_to_nat l2"
proof -
have "\<forall>l2. bv_to_nat (l1 @ l2) = bv_to_nat l1 * 2 ^ length l2 + bv_to_nat l2"
proof (induct l1,simp_all)
@@ -457,8 +458,7 @@
assume ind: "!!j. j < n \<Longrightarrow> bv_to_nat (nat_to_bv j) = j"
show "bv_to_nat (nat_to_bv n) = n"
proof (rule n_div_2_cases [of n])
- assume "n = 0"
- then show ?thesis by simp
+ assume "n = 0" then show ?thesis by simp
next
assume nn: "n div 2 < n"
assume n0: "0 < n"
@@ -474,16 +474,14 @@
apply (fold nat_to_bv_def)
apply (simp add: ind' split del: split_if)
apply (cases "n mod 2 = 0")
- proof (simp_all add: neq0_conv)
+ proof (simp_all)
assume "n mod 2 = 0"
with mod_div_equality [of n 2]
- show "n div 2 * 2 = n"
- by simp
+ show "n div 2 * 2 = n" by simp
next
- assume "n mod 2 = Suc 0"
+ assume "n mod 2 \<noteq> 0"
with mod_div_equality [of n 2]
- show "Suc (n div 2 * 2) = n"
- by simp
+ show "Suc (n div 2 * 2) = n" by arith
qed
qed
qed
@@ -536,29 +534,30 @@
lemmas [simp del] = nat_to_bv_non0
lemma norm_unsigned_length [intro!]: "length (norm_unsigned w) \<le> length w"
- by (subst norm_unsigned_def,rule rem_initial_length)
+by (subst norm_unsigned_def,rule rem_initial_length)
-lemma norm_unsigned_equal: "length (norm_unsigned w) = length w ==> norm_unsigned w = w"
- by (simp add: norm_unsigned_def,rule rem_initial_equal)
+lemma norm_unsigned_equal:
+ "length (norm_unsigned w) = length w ==> norm_unsigned w = w"
+by (simp add: norm_unsigned_def,rule rem_initial_equal)
lemma bv_extend_norm_unsigned: "bv_extend (length w) \<zero> (norm_unsigned w) = w"
- by (simp add: norm_unsigned_def,rule bv_extend_rem_initial)
+by (simp add: norm_unsigned_def,rule bv_extend_rem_initial)
lemma norm_unsigned_append1 [simp]:
- "norm_unsigned xs \<noteq> [] ==> norm_unsigned (xs @ ys) = norm_unsigned xs @ ys"
- by (simp add: norm_unsigned_def,rule rem_initial_append1)
+ "norm_unsigned xs \<noteq> [] ==> norm_unsigned (xs @ ys) = norm_unsigned xs @ ys"
+by (simp add: norm_unsigned_def,rule rem_initial_append1)
lemma norm_unsigned_append2 [simp]:
- "norm_unsigned xs = [] ==> norm_unsigned (xs @ ys) = norm_unsigned ys"
- by (simp add: norm_unsigned_def,rule rem_initial_append2)
+ "norm_unsigned xs = [] ==> norm_unsigned (xs @ ys) = norm_unsigned ys"
+by (simp add: norm_unsigned_def,rule rem_initial_append2)
lemma bv_to_nat_zero_imp_empty:
- "bv_to_nat w = 0 \<Longrightarrow> norm_unsigned w = []"
- by (atomize (full), induct w rule: bit_list_induct) (simp_all add: neq0_conv)
+ "bv_to_nat w = 0 \<Longrightarrow> norm_unsigned w = []"
+by (atomize (full), induct w rule: bit_list_induct) simp_all
lemma bv_to_nat_nzero_imp_nempty:
"bv_to_nat w \<noteq> 0 \<Longrightarrow> norm_unsigned w \<noteq> []"
- by (induct w rule: bit_list_induct) simp_all
+by (induct w rule: bit_list_induct) simp_all
lemma nat_helper1:
assumes ass: "nat_to_bv (bv_to_nat w) = norm_unsigned w"
@@ -1855,8 +1854,8 @@
qed
qed
-lemma bv_msb_one: "bv_msb w = \<one> ==> 0 < bv_to_nat w"
- by (cases w) simp_all
+lemma bv_msb_one: "bv_msb w = \<one> ==> bv_to_nat w \<noteq> 0"
+by (cases w) simp_all
lemma bv_smult_length_utos: "length (bv_smult (utos w1) w2) \<le> length w1 + length w2"
proof -
@@ -2064,7 +2063,7 @@
by (simp add: length_nat_def Least_equality)
lemma length_nat_non0:
- assumes n0: "0 < n"
+ assumes n0: "n \<noteq> 0"
shows "length_nat n = Suc (length_nat (n div 2))"
apply (simp add: length_nat [symmetric])
apply (subst nat_to_bv_non0 [of n])
--- a/src/HOL/List.thy Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/List.thy Sun Oct 21 14:53:44 2007 +0200
@@ -950,9 +950,7 @@
proof (cases)
assume "p x"
hence eq: "?S' = insert 0 (Suc ` ?S)"
- apply (auto simp add: nth_Cons image_def neq0_conv split:nat.split elim:lessE)
- apply (rule_tac x="xa - 1" in exI, auto)
- done
+ by(auto simp: nth_Cons image_def split:nat.split dest:not0_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
@@ -2460,12 +2458,7 @@
lemma set_sublist: "set(sublist xs I) = {xs!i|i. i<size xs \<and> i \<in> I}"
apply(induct xs arbitrary: I)
- apply simp
-apply(auto simp add: neq0_conv sublist_Cons nth_Cons split:nat.split elim: lessE)
- apply(erule lessE)
- apply auto
-apply(erule lessE)
-apply auto
+apply(auto simp: sublist_Cons nth_Cons split:nat.split dest!: not0_implies_Suc)
done
lemma set_sublist_subset: "set(sublist xs I) \<subseteq> set xs"
--- a/src/HOL/Nat.thy Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Nat.thy Sun Oct 21 14:53:44 2007 +0200
@@ -508,10 +508,7 @@
by (fast intro: not0_implies_Suc)
lemma not_gr0 [iff,noatp]: "!!n::nat. (~ (0 < n)) = (n = 0)"
- apply (rule iffI)
- apply (rule ccontr)
- apply (simp_all add: neq0_conv)
- done
+using neq0_conv by blast
lemma Suc_le_D: "(Suc n \<le> m') ==> (? m. m' = Suc m)"
by (induct m') simp_all
@@ -603,8 +600,8 @@
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 < n ==> Suc (n - Suc 0) = n"
- by (simp add: neq0_conv split add: nat.split)
+lemma Suc_pred [simp]: "0 \<noteq> n ==> Suc (n - Suc 0) = n"
+by (simp split add: nat.split)
declare diff_Suc [simp del, code del]
@@ -658,8 +655,8 @@
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)
-lemma add_gr_0 [iff]: "!!m::nat. (0 < m + n) = (0 < m | 0 < n)"
- by (simp del: neq0_conv add: neq0_conv [symmetric])
+lemma add_gr_0 [iff]: "!!m::nat. (m + n \<noteq> 0) = (m\<noteq>0 | n\<noteq>0)"
+by simp
lemma add_eq_self_zero: "!!m::nat. m + n = m ==> n = 0"
apply (drule add_0_right [THEN ssubst])
@@ -743,11 +740,11 @@
done
text {* strict, in 1st argument; proof is by induction on @{text "k > 0"} *}
-lemma mult_less_mono2: "(i::nat) < j ==> 0 < k ==> k * i < k * j"
- apply (erule_tac m1 = 0 in less_imp_Suc_add [THEN exE], simp)
- apply (induct_tac x)
- apply (simp_all add: add_less_mono)
- done
+lemma mult_less_mono2: "(i::nat) < j ==> 0<k ==> k * i < k * j"
+apply(auto simp: gr0_conv_Suc)
+apply (induct_tac m)
+apply (simp_all add: add_less_mono)
+done
text{*The naturals form an ordered @{text comm_semiring_1_cancel}*}
@@ -1084,9 +1081,9 @@
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 (drule mult_less_mono1, assumption, simp)+
- done
+apply (cut_tac less_linear, safe, auto simp add: neq0_conv)
+apply (drule mult_less_mono1, assumption, simp)+
+done
lemma mult_cancel1 [simp]: "(k * m = k * n) = (m = n | (k = (0::nat)))"
by (simp add: mult_commute [of k])
@@ -1105,8 +1102,8 @@
apply (drule sym)
apply (rule disjCI)
apply (rule nat_less_cases, erule_tac [2] _)
- apply (fastsimp simp add: neq0_conv elim!: less_SucE)
- apply (fastsimp simp add: neq0_conv dest: mult_less_mono2)
+ apply (fastsimp elim!: less_SucE)
+ apply (auto simp add: neq0_conv dest: mult_less_mono2)
done
--- a/src/HOL/Power.thy Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Power.thy Sun Oct 21 14:53:44 2007 +0200
@@ -140,16 +140,13 @@
done
lemma power_eq_0_iff [simp]:
- "(a^n = 0) = (a = (0::'a::{ring_1_no_zero_divisors,recpower}) & 0<n)"
+ "(a^n = 0) = (a = (0::'a::{ring_1_no_zero_divisors,recpower}) & n\<noteq>0)"
apply (induct "n")
apply (auto simp add: power_Suc zero_neq_one [THEN not_sym])
done
-lemma field_power_eq_0_iff:
- "(a^n = 0) = (a = (0::'a::{division_ring,recpower}) & 0<n)"
-by simp (* TODO: delete *)
-
-lemma field_power_not_zero: "a \<noteq> (0::'a::{ring_1_no_zero_divisors,recpower}) ==> a^n \<noteq> 0"
+lemma field_power_not_zero:
+ "a \<noteq> (0::'a::{ring_1_no_zero_divisors,recpower}) ==> a^n \<noteq> 0"
by force
lemma nonzero_power_inverse:
@@ -279,26 +276,26 @@
order_less_imp_le)
done
-lemma power_increasing_iff [simp]:
- "1 < (b::'a::{ordered_semidom,recpower}) ==> (b ^ x \<le> b ^ y) = (x \<le> y)"
- by (blast intro: power_le_imp_le_exp power_increasing order_less_imp_le)
+lemma power_increasing_iff [simp]:
+ "1 < (b::'a::{ordered_semidom,recpower}) ==> (b ^ x \<le> b ^ y) = (x \<le> y)"
+by (blast intro: power_le_imp_le_exp power_increasing order_less_imp_le)
lemma power_strict_increasing_iff [simp]:
- "1 < (b::'a::{ordered_semidom,recpower}) ==> (b ^ x < b ^ y) = (x < y)"
- by (blast intro: power_less_imp_less_exp power_strict_increasing)
+ "1 < (b::'a::{ordered_semidom,recpower}) ==> (b ^ x < b ^ y) = (x < y)"
+by (blast intro: power_less_imp_less_exp power_strict_increasing)
lemma power_le_imp_le_base:
- assumes le: "a ^ Suc n \<le> b ^ Suc n"
- and ynonneg: "(0::'a::{ordered_semidom,recpower}) \<le> b"
- shows "a \<le> b"
- proof (rule ccontr)
- assume "~ a \<le> b"
- then have "b < a" by (simp only: linorder_not_le)
- then have "b ^ Suc n < a ^ Suc n"
- by (simp only: prems power_strict_mono)
- from le and this show "False"
- by (simp add: linorder_not_less [symmetric])
- qed
+assumes le: "a ^ Suc n \<le> b ^ Suc n"
+ and ynonneg: "(0::'a::{ordered_semidom,recpower}) \<le> b"
+shows "a \<le> b"
+proof (rule ccontr)
+ assume "~ a \<le> b"
+ then have "b < a" by (simp only: linorder_not_le)
+ then have "b ^ Suc n < a ^ Suc n"
+ by (simp only: prems power_strict_mono)
+ from le and this show "False"
+ by (simp add: linorder_not_less [symmetric])
+qed
lemma power_less_imp_less_base:
fixes a b :: "'a::{ordered_semidom,recpower}"
@@ -345,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]: "(0 < x^n) = (x \<noteq> (0::nat) | n=0)"
+lemma nat_zero_less_power_iff [simp]: "(x^n = 0) = (x = (0::nat) & n\<noteq>0)"
by (induct "n", auto)
text{*Valid for the naturals, but what if @{text"0<i<1"}?
@@ -393,7 +390,7 @@
val power_mono = thm"power_mono";
val power_strict_mono = thm"power_strict_mono";
val power_eq_0_iff = thm"power_eq_0_iff";
-val field_power_eq_0_iff = thm"field_power_eq_0_iff";
+val field_power_eq_0_iff = thm"power_eq_0_iff";
val field_power_not_zero = thm"field_power_not_zero";
val power_inverse = thm"power_inverse";
val nonzero_power_divide = thm"nonzero_power_divide";
--- a/src/HOL/Real/RealDef.thy Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Real/RealDef.thy Sun Oct 21 14:53:44 2007 +0200
@@ -794,24 +794,24 @@
lemma real_of_nat_div2:
"0 <= real (n::nat) / real (x) - real (n div x)"
- apply(case_tac "x = 0")
- apply (simp add: neq0_conv)
- apply (simp add: neq0_conv compare_rls)
- apply (subst real_of_nat_div_aux)
- apply assumption
- apply simp
- apply (subst zero_le_divide_iff)
- apply simp
+apply(case_tac "x = 0")
+ apply (simp)
+apply (simp add: compare_rls)
+apply (subst real_of_nat_div_aux)
+ apply simp
+apply simp
+apply (subst zero_le_divide_iff)
+apply simp
done
lemma real_of_nat_div3:
"real (n::nat) / real (x) - real (n div x) <= 1"
- apply(case_tac "x = 0")
- apply (simp add: neq0_conv )
- apply (simp add: compare_rls neq0_conv )
- apply (subst real_of_nat_div_aux)
- apply assumption
- apply simp
+apply(case_tac "x = 0")
+apply (simp)
+apply (simp add: compare_rls)
+apply (subst real_of_nat_div_aux)
+ apply simp
+apply simp
done
lemma real_of_nat_div4: "real (n div x) <= real (n::nat) / real x"
--- a/src/HOL/Word/BinBoolList.thy Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Word/BinBoolList.thy Sun Oct 21 14:53:44 2007 +0200
@@ -1099,20 +1099,19 @@
done
lemma bin_rsplit_aux_len_le [rule_format] :
- "ALL ws m. n > 0 --> ws = bin_rsplit_aux (n, bs, nw, w) -->
+ "ALL ws m. n \<noteq> 0 --> ws = bin_rsplit_aux (n, bs, nw, w) -->
(length ws <= m) = (nw + length bs * n <= m * n)"
apply (rule_tac u=n and v=bs and w=nw and x=w in bin_rsplit_aux.induct)
apply (subst bin_rsplit_aux.simps)
- apply (clarsimp simp: Let_def neq0_conv split: ls_splits )
- apply (erule lrlem)
+ apply (simp add:lrlem Let_def split: ls_splits )
done
lemma bin_rsplit_len_le:
- "n > 0 --> ws = bin_rsplit n (nw, w) --> (length ws <= m) = (nw <= m * n)"
+ "n \<noteq> 0 --> ws = bin_rsplit n (nw, w) --> (length ws <= m) = (nw <= m * n)"
unfolding bin_rsplit_def by (clarsimp simp add : bin_rsplit_aux_len_le)
lemma bin_rsplit_aux_len [rule_format] :
- "0 < n --> length (bin_rsplit_aux (n, cs, nw, w)) =
+ "n\<noteq>0 --> length (bin_rsplit_aux (n, cs, nw, w)) =
(nw + n - 1) div n + length cs"
apply (rule_tac u=n and v=cs and w=nw and x=w in bin_rsplit_aux.induct)
apply (subst bin_rsplit_aux.simps)
@@ -1126,11 +1125,11 @@
done
lemma bin_rsplit_len:
- "0 < n ==> length (bin_rsplit n (nw, w)) = (nw + n - 1) div n"
+ "n\<noteq>0 ==> length (bin_rsplit n (nw, w)) = (nw + n - 1) div n"
unfolding bin_rsplit_def by (clarsimp simp add : bin_rsplit_aux_len)
lemma bin_rsplit_aux_len_indep [rule_format] :
- "0 < n ==> (ALL v bs. length bs = length cs -->
+ "n\<noteq>0 ==> (ALL v bs. length bs = length cs -->
length (bin_rsplit_aux (n, bs, nw, v)) =
length (bin_rsplit_aux (n, cs, nw, w)))"
apply (rule_tac u=n and v=cs and w=nw and x=w in bin_rsplit_aux.induct)
@@ -1148,7 +1147,7 @@
done
lemma bin_rsplit_len_indep:
- "0 < n ==> length (bin_rsplit n (nw, v)) = length (bin_rsplit n (nw, w))"
+ "n\<noteq>0 ==> length (bin_rsplit n (nw, v)) = length (bin_rsplit n (nw, w))"
apply (unfold bin_rsplit_def)
apply (erule bin_rsplit_aux_len_indep)
apply (rule refl)
--- a/src/HOL/Word/BinGeneral.thy Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Word/BinGeneral.thy Sun Oct 21 14:53:44 2007 +0200
@@ -457,7 +457,7 @@
we get a version for when the word length is given literally *)
lemmas nat_non0_gr =
- trans [OF iszero_def [THEN Not_eq_iff [THEN iffD2]] neq0_conv, standard]
+ trans [OF iszero_def [THEN Not_eq_iff [THEN iffD2]] refl, standard]
lemmas bintrunc_pred_simps [simp] =
bintrunc_minus_simps [of "number_of bin", simplified nobm1, standard]
--- a/src/HOL/Word/WordArith.thy Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Word/WordArith.thy Sun Oct 21 14:53:44 2007 +0200
@@ -117,28 +117,28 @@
lemmas unat_eq_zero = unat_0_iff
lemma unat_gt_0: "(0 < unat x) = (x ~= 0)"
- by (simp add : neq0_conv unat_0_iff [symmetric])
+by (auto simp: unat_0_iff [symmetric])
lemma ucast_0 [simp] : "ucast 0 = 0"
- unfolding ucast_def
- by simp (simp add: word_0_wi)
+unfolding ucast_def
+by simp (simp add: word_0_wi)
lemma sint_0 [simp] : "sint 0 = 0"
- unfolding sint_uint
- by (simp add: Pls_def [symmetric])
+unfolding sint_uint
+by (simp add: Pls_def [symmetric])
lemma scast_0 [simp] : "scast 0 = 0"
- apply (unfold scast_def)
- apply simp
- apply (simp add: word_0_wi)
- done
+apply (unfold scast_def)
+apply simp
+apply (simp add: word_0_wi)
+done
lemma sint_n1 [simp] : "sint -1 = -1"
- apply (unfold word_m1_wi_Min)
- apply (simp add: word_sbin.eq_norm)
- apply (unfold Min_def number_of_eq)
- apply simp
- done
+apply (unfold word_m1_wi_Min)
+apply (simp add: word_sbin.eq_norm)
+apply (unfold Min_def number_of_eq)
+apply simp
+done
lemma scast_n1 [simp] : "scast -1 = -1"
apply (unfold scast_def sint_n1)
@@ -1242,15 +1242,15 @@
lemmas card_word = trans [OF card_eq card_lessThan', standard]
lemma finite_word_UNIV: "finite (UNIV :: 'a :: len word set)"
- apply (rule contrapos_np)
- prefer 2
- apply (erule card_infinite)
- apply (simp add : card_word neq0_conv)
- done
+apply (rule contrapos_np)
+ prefer 2
+ apply (erule card_infinite)
+apply (simp add: card_word)
+done
lemma card_word_size:
"card (UNIV :: 'a :: len word set) = (2 ^ size (x :: 'a word))"
- unfolding word_size by (rule card_word)
+unfolding word_size by (rule card_word)
end
--- a/src/HOL/ex/Reflected_Presburger.thy Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/ex/Reflected_Presburger.thy Sun Oct 21 14:53:44 2007 +0200
@@ -63,7 +63,7 @@
"fmsize (NDvd i t) = 2"
"fmsize p = 1"
(* several lemmas about fmsize *)
-lemma fmsize_pos: "fmsize p > 0"
+lemma fmsize_pos: "fmsize p \<noteq> 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)
+(hints simp add: fmsize_pos neq0_conv[symmetric])
lemma prep: "Ifm bbs bs (prep p) = Ifm bbs bs p"
by (induct p arbitrary: bs rule: prep.induct, auto)
@@ -188,14 +188,12 @@
| "numsubst0 t (Mul i a) = Mul i (numsubst0 t a)"
lemma numsubst0_I:
- shows "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b#bs) a)#bs) t"
- by (induct t rule: numsubst0.induct,auto simp add: gr0_conv_Suc neq0_conv)
+ "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b#bs) a)#bs) t"
+by (induct t rule: numsubst0.induct,auto dest: not0_implies_Suc)
lemma numsubst0_I':
- assumes nb: "numbound0 a"
- shows "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b'#bs) a)#bs) t"
- using nb
- by (induct t rule: numsubst0.induct, auto simp add: neq0_conv gr0_conv_Suc numbound0_I[where b="b" and b'="b'"])
+ "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'"])
primrec
"subst0 t T = T"