--- a/src/HOL/Auth/Kerberos_BAN.thy Sat Oct 20 12:09:30 2007 +0200
+++ b/src/HOL/Auth/Kerberos_BAN.thy Sat Oct 20 12:09:33 2007 +0200
@@ -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)
+apply (possibility, simp_all (no_asm_simp) add: used_Cons neq0_conv)
done
subsection{*Lemmas for reasoning about predicate "Issues"*}
--- a/src/HOL/Complex/ex/HarmonicSeries.thy Sat Oct 20 12:09:30 2007 +0200
+++ b/src/HOL/Complex/ex/HarmonicSeries.thy Sat Oct 20 12:09:33 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)
+ moreover from mgt0 have "real tm \<noteq> 0" by (simp add: tmdef neq0_conv)
then have
"inverse (real tm) = 1 / (real tm)"
by (rule nonzero_inverse_eq_divide)
--- a/src/HOL/Divides.thy Sat Oct 20 12:09:30 2007 +0200
+++ b/src/HOL/Divides.thy Sat Oct 20 12:09:33 2007 +0200
@@ -275,12 +275,14 @@
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)
+ 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
lemma mod_mult1_eq: "(a*b) mod c = a*(b mod c) mod (c::nat)"
- apply (cases "c = 0", simp)
+ 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
@@ -307,11 +309,13 @@
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
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
--- a/src/HOL/HoareParallel/OG_Examples.thy Sat Oct 20 12:09:30 2007 +0200
+++ b/src/HOL/HoareParallel/OG_Examples.thy Sat Oct 20 12:09:33 2007 +0200
@@ -439,7 +439,7 @@
apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
apply(simp_all (asm_lr) only:length_0_conv [THEN sym])
--{* 44 subgoals left *}
-apply (simp_all (asm_lr) del:length_0_conv add: nth_list_update mod_less_divisor mod_lemma)
+apply (simp_all (asm_lr) del:length_0_conv add: neq0_conv nth_list_update mod_less_divisor mod_lemma)
--{* 32 subgoals left *}
apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
--- a/src/HOL/Hyperreal/Fact.thy Sat Oct 20 12:09:30 2007 +0200
+++ b/src/HOL/Hyperreal/Fact.thy Sat Oct 20 12:09:33 2007 +0200
@@ -20,7 +20,7 @@
by (induct n) auto
lemma fact_not_eq_zero [simp]: "fact n \<noteq> 0"
- by simp
+ by (simp add: neq0_conv)
lemma real_of_nat_fact_not_zero [simp]: "real (fact n) \<noteq> 0"
by auto
--- a/src/HOL/Hyperreal/HyperNat.thy Sat Oct 20 12:09:30 2007 +0200
+++ b/src/HOL/Hyperreal/HyperNat.thy Sat Oct 20 12:09:33 2007 +0200
@@ -331,8 +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)
-apply (rule ccontr, drule FreeUltrafilterNat.not_memD, drule FreeUltrafilterNat.Int, assumption, simp)
+apply (drule_tac x = 0 in spec, simp add: neq0_conv)
apply (drule_tac x = "Suc n" in spec)
apply (elim ultra, auto)
done
--- a/src/HOL/Hyperreal/Integration.thy Sat Oct 20 12:09:30 2007 +0200
+++ b/src/HOL/Hyperreal/Integration.thy Sat Oct 20 12:09:33 2007 +0200
@@ -149,12 +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)
+apply (frule partition_rhs, simp only: neq0_conv)
apply (drule partition_gt, assumption)
apply (simp (no_asm_simp))
done
--- a/src/HOL/Hyperreal/MacLaurin.thy Sat Oct 20 12:09:30 2007 +0200
+++ b/src/HOL/Hyperreal/MacLaurin.thy Sat Oct 20 12:09:33 2007 +0200
@@ -279,11 +279,11 @@
apply (case_tac "n = 0", force)
apply (case_tac "x = 0")
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)
+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)
+apply (simp add: abs_if neq0_conv)
apply (rule_tac x = t in exI)
apply (simp add: abs_if)
txt{*Case 2, where @{term "0 < x"}*}
--- a/src/HOL/Hyperreal/Poly.thy Sat Oct 20 12:09:30 2007 +0200
+++ b/src/HOL/Hyperreal/Poly.thy Sat Oct 20 12:09:33 2007 +0200
@@ -595,6 +595,7 @@
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) 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 (simp (no_asm_simp) del: pderiv_aux_iszero)
@@ -793,7 +794,8 @@
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 (simp add: divides_def poly_mult fun_eq neq0_conv del: pmult_Cons, blast)
+using neq0_conv
apply (blast intro: lemma_order_root)
done
@@ -883,7 +885,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 dest: pderiv_zero)
+apply (auto simp add: neq0_conv dest: pderiv_zero)
apply (drule_tac a = a and p = p in order_decomp)
apply (blast intro: lemma_order_pderiv)
done
@@ -951,7 +953,6 @@
apply (simp add: fun_eq)
apply (blast intro: order_poly)
apply (auto simp add: order_root order_pderiv2)
-apply (drule spec, auto)
done
lemma pmult_one: "[1] *** p = p"
--- a/src/HOL/IntDiv.thy Sat Oct 20 12:09:30 2007 +0200
+++ b/src/HOL/IntDiv.thy Sat Oct 20 12:09:33 2007 +0200
@@ -1339,7 +1339,7 @@
apply simp
apply (case_tac "0 \<le> k")
apply iprover
- apply (simp add: linorder_not_le)
+ 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)
--- a/src/HOL/Library/Binomial.thy Sat Oct 20 12:09:30 2007 +0200
+++ b/src/HOL/Library/Binomial.thy Sat Oct 20 12:09:33 2007 +0200
@@ -50,11 +50,11 @@
lemma binomial_eq_0_iff: "(n choose k = 0) = (n<k)"
apply (safe intro!: binomial_eq_0)
apply (erule contrapos_pp)
- apply (simp add: zero_less_binomial)
+ apply (simp add: neq0_conv zero_less_binomial)
done
lemma zero_less_binomial_iff: "(0 < n choose k) = (k\<le>n)"
- by (simp add: linorder_not_less [symmetric] binomial_eq_0_iff [symmetric])
+ by (simp add: neq0_conv linorder_not_less [symmetric] binomial_eq_0_iff [symmetric])
(*Might be more useful if re-oriented*)
lemma Suc_times_binomial_eq:
--- a/src/HOL/Library/GCD.thy Sat Oct 20 12:09:30 2007 +0200
+++ b/src/HOL/Library/GCD.thy Sat Oct 20 12:09:33 2007 +0200
@@ -396,7 +396,7 @@
assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
shows "igcd (a div (igcd a b)) (b div (igcd a b)) = 1"
proof -
- from nz have nz': "nat \<bar>a\<bar> \<noteq> 0 \<or> nat \<bar>b\<bar> \<noteq> 0" by simp
+ from nz have nz': "nat \<bar>a\<bar> \<noteq> 0 \<or> nat \<bar>b\<bar> \<noteq> 0" by arith
let ?g = "igcd a b"
let ?a' = "a div ?g"
let ?b' = "b div ?g"
--- a/src/HOL/Library/Nat_Infinity.thy Sat Oct 20 12:09:30 2007 +0200
+++ b/src/HOL/Library/Nat_Infinity.thy Sat Oct 20 12:09:33 2007 +0200
@@ -99,7 +99,7 @@
by (simp add: inat_defs split:inat_splits)
lemma i0_eq [simp]: "((0::inat) < n) = (n \<noteq> 0)"
- by (simp add: inat_defs split:inat_splits)
+ by (simp add: neq0_conv inat_defs split:inat_splits)
lemma i0_iless_iSuc [simp]: "0 < iSuc n"
by (simp add: inat_defs split:inat_splits)
--- a/src/HOL/Library/Word.thy Sat Oct 20 12:09:30 2007 +0200
+++ b/src/HOL/Library/Word.thy Sat Oct 20 12:09:33 2007 +0200
@@ -420,7 +420,7 @@
apply (simp only: nat_to_bv_helper.simps [of n])
apply (subst unfold_nat_to_bv_helper)
using prems
- apply simp
+ apply (simp add: neq0_conv)
apply (subst nat_to_bv_def [of "n div 2"])
apply auto
done
@@ -474,7 +474,7 @@
apply (fold nat_to_bv_def)
apply (simp add: ind' split del: split_if)
apply (cases "n mod 2 = 0")
- proof simp_all
+ proof (simp_all add: neq0_conv)
assume "n mod 2 = 0"
with mod_div_equality [of n 2]
show "n div 2 * 2 = n"
@@ -554,7 +554,7 @@
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
+ by (atomize (full), induct w rule: bit_list_induct) (simp_all add: neq0_conv)
lemma bv_to_nat_nzero_imp_nempty:
"bv_to_nat w \<noteq> 0 \<Longrightarrow> norm_unsigned w \<noteq> []"
--- a/src/HOL/List.thy Sat Oct 20 12:09:30 2007 +0200
+++ b/src/HOL/List.thy Sat Oct 20 12:09:33 2007 +0200
@@ -950,7 +950,9 @@
proof (cases)
assume "p x"
hence eq: "?S' = insert 0 (Suc ` ?S)"
- by(auto simp add: nth_Cons image_def split:nat.split elim:lessE)
+ 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
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 +963,9 @@
next
assume "\<not> p x"
hence eq: "?S' = Suc ` ?S"
- by(auto simp add: nth_Cons image_def split:nat.split elim:lessE)
+ apply(auto simp add: nth_Cons image_def split:nat.split elim:lessE)
+ apply (rule_tac x="xa - 1" in exI, auto)
+ done
have "length (filter p (x # xs)) = card ?S"
using Cons `\<not> p x` by simp
also have "\<dots> = card(Suc ` ?S)" using fin
@@ -2453,7 +2457,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:sublist_Cons nth_Cons split:nat.split elim: lessE)
+apply(auto simp add: neq0_conv sublist_Cons nth_Cons split:nat.split elim: lessE)
apply(erule lessE)
apply auto
apply(erule lessE)
--- a/src/HOL/Real/RealDef.thy Sat Oct 20 12:09:30 2007 +0200
+++ b/src/HOL/Real/RealDef.thy Sat Oct 20 12:09:33 2007 +0200
@@ -795,8 +795,8 @@
lemma real_of_nat_div2:
"0 <= real (n::nat) / real (x) - real (n div x)"
apply(case_tac "x = 0")
- apply simp
- apply (simp add: compare_rls)
+ apply (simp add: neq0_conv)
+ apply (simp add: neq0_conv compare_rls)
apply (subst real_of_nat_div_aux)
apply assumption
apply simp
@@ -807,8 +807,8 @@
lemma real_of_nat_div3:
"real (n::nat) / real (x) - real (n div x) <= 1"
apply(case_tac "x = 0")
- apply simp
- apply (simp add: compare_rls)
+ apply (simp add: neq0_conv )
+ apply (simp add: compare_rls neq0_conv )
apply (subst real_of_nat_div_aux)
apply assumption
apply simp
--- a/src/HOL/Word/BinBoolList.thy Sat Oct 20 12:09:30 2007 +0200
+++ b/src/HOL/Word/BinBoolList.thy Sat Oct 20 12:09:33 2007 +0200
@@ -1103,7 +1103,7 @@
(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 split: ls_splits)
+ apply (clarsimp simp: Let_def neq0_conv split: ls_splits )
apply (erule lrlem)
done
--- a/src/HOL/Word/BinOperations.thy Sat Oct 20 12:09:30 2007 +0200
+++ b/src/HOL/Word/BinOperations.thy Sat Oct 20 12:09:33 2007 +0200
@@ -353,7 +353,6 @@
"!!w m. m ~= n ==>
bin_sc m c (bin_sc n b w) = bin_sc n b (bin_sc m c w)"
apply (induct n)
- apply safe
apply (case_tac [!] m)
apply auto
done
--- a/src/HOL/Word/WordArith.thy Sat Oct 20 12:09:30 2007 +0200
+++ b/src/HOL/Word/WordArith.thy Sat Oct 20 12:09:33 2007 +0200
@@ -117,7 +117,7 @@
lemmas unat_eq_zero = unat_0_iff
lemma unat_gt_0: "(0 < unat x) = (x ~= 0)"
- by (simp add : unat_0_iff [symmetric])
+ by (simp add : neq0_conv unat_0_iff [symmetric])
lemma ucast_0 [simp] : "ucast 0 = 0"
unfolding ucast_def
@@ -1245,7 +1245,7 @@
apply (rule contrapos_np)
prefer 2
apply (erule card_infinite)
- apply (simp add : card_word)
+ apply (simp add : card_word neq0_conv)
done
lemma card_word_size:
--- a/src/HOL/ex/Reflected_Presburger.thy Sat Oct 20 12:09:30 2007 +0200
+++ b/src/HOL/ex/Reflected_Presburger.thy Sat Oct 20 12:09:33 2007 +0200
@@ -189,13 +189,13 @@
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)
+ by (induct t rule: numsubst0.induct,auto simp add: gr0_conv_Suc neq0_conv)
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: gr0_conv_Suc numbound0_I[where b="b" and b'="b'"])
+ by (induct t rule: numsubst0.induct, auto simp add: neq0_conv gr0_conv_Suc numbound0_I[where b="b" and b'="b'"])
primrec
"subst0 t T = T"