# HG changeset patch
# User chaieb
# Date 1192874973 -7200
# Node ID 98824cc791c02ada0f6996e42c531715fbb144e9
# Parent  d52a58b51f1ff5ed41b3cd71fcd23250c76844b4
fixed proofs

diff -r d52a58b51f1f -r 98824cc791c0 src/HOL/Auth/Kerberos_BAN.thy
--- 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"*}
diff -r d52a58b51f1f -r 98824cc791c0 src/HOL/Complex/ex/HarmonicSeries.thy
--- 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)
diff -r d52a58b51f1f -r 98824cc791c0 src/HOL/Divides.thy
--- 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
 
diff -r d52a58b51f1f -r 98824cc791c0 src/HOL/HoareParallel/OG_Examples.thy
--- 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}) *})
 
diff -r d52a58b51f1f -r 98824cc791c0 src/HOL/Hyperreal/Fact.thy
--- 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
diff -r d52a58b51f1f -r 98824cc791c0 src/HOL/Hyperreal/HyperNat.thy
--- 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
diff -r d52a58b51f1f -r 98824cc791c0 src/HOL/Hyperreal/Integration.thy
--- 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
diff -r d52a58b51f1f -r 98824cc791c0 src/HOL/Hyperreal/MacLaurin.thy
--- 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"}*}
diff -r d52a58b51f1f -r 98824cc791c0 src/HOL/Hyperreal/Poly.thy
--- 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"
diff -r d52a58b51f1f -r 98824cc791c0 src/HOL/IntDiv.thy
--- 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)
diff -r d52a58b51f1f -r 98824cc791c0 src/HOL/Library/Binomial.thy
--- 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:
diff -r d52a58b51f1f -r 98824cc791c0 src/HOL/Library/GCD.thy
--- 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"
diff -r d52a58b51f1f -r 98824cc791c0 src/HOL/Library/Nat_Infinity.thy
--- 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)
diff -r d52a58b51f1f -r 98824cc791c0 src/HOL/Library/Word.thy
--- 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> []"
diff -r d52a58b51f1f -r 98824cc791c0 src/HOL/List.thy
--- 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)
diff -r d52a58b51f1f -r 98824cc791c0 src/HOL/Real/RealDef.thy
--- 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
diff -r d52a58b51f1f -r 98824cc791c0 src/HOL/Word/BinBoolList.thy
--- 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
 
diff -r d52a58b51f1f -r 98824cc791c0 src/HOL/Word/BinOperations.thy
--- 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
diff -r d52a58b51f1f -r 98824cc791c0 src/HOL/Word/WordArith.thy
--- 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: 
diff -r d52a58b51f1f -r 98824cc791c0 src/HOL/ex/Reflected_Presburger.thy
--- 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"