fixed proofs
authorchaieb
Sat Oct 20 12:09:33 2007 +0200 (2007-10-20)
changeset 2511298824cc791c0
parent 25111 d52a58b51f1f
child 25113 008c964dd47f
fixed proofs
src/HOL/Auth/Kerberos_BAN.thy
src/HOL/Complex/ex/HarmonicSeries.thy
src/HOL/Divides.thy
src/HOL/HoareParallel/OG_Examples.thy
src/HOL/Hyperreal/Fact.thy
src/HOL/Hyperreal/HyperNat.thy
src/HOL/Hyperreal/Integration.thy
src/HOL/Hyperreal/MacLaurin.thy
src/HOL/Hyperreal/Poly.thy
src/HOL/IntDiv.thy
src/HOL/Library/Binomial.thy
src/HOL/Library/GCD.thy
src/HOL/Library/Nat_Infinity.thy
src/HOL/Library/Word.thy
src/HOL/List.thy
src/HOL/Real/RealDef.thy
src/HOL/Word/BinBoolList.thy
src/HOL/Word/BinOperations.thy
src/HOL/Word/WordArith.thy
src/HOL/ex/Reflected_Presburger.thy
     1.1 --- a/src/HOL/Auth/Kerberos_BAN.thy	Sat Oct 20 12:09:30 2007 +0200
     1.2 +++ b/src/HOL/Auth/Kerberos_BAN.thy	Sat Oct 20 12:09:33 2007 +0200
     1.3 @@ -133,7 +133,7 @@
     1.4  apply (rule_tac [2]
     1.5             bankerberos.Nil [THEN bankerberos.BK1, THEN bankerberos.BK2,
     1.6                               THEN bankerberos.BK3, THEN bankerberos.BK4])
     1.7 -apply (possibility, simp_all (no_asm_simp) add: used_Cons)
     1.8 +apply (possibility, simp_all (no_asm_simp) add: used_Cons neq0_conv)
     1.9  done
    1.10  
    1.11  subsection{*Lemmas for reasoning about predicate "Issues"*}
     2.1 --- a/src/HOL/Complex/ex/HarmonicSeries.thy	Sat Oct 20 12:09:30 2007 +0200
     2.2 +++ b/src/HOL/Complex/ex/HarmonicSeries.thy	Sat Oct 20 12:09:33 2007 +0200
     2.3 @@ -80,7 +80,7 @@
     2.4        then have
     2.5          "inverse (real x) = 1 / (real x)"
     2.6          by (rule nonzero_inverse_eq_divide)
     2.7 -      moreover from mgt0 have "real tm \<noteq> 0" by (simp add: tmdef)
     2.8 +      moreover from mgt0 have "real tm \<noteq> 0" by (simp add: tmdef neq0_conv)
     2.9        then have
    2.10          "inverse (real tm) = 1 / (real tm)"
    2.11          by (rule nonzero_inverse_eq_divide)
     3.1 --- a/src/HOL/Divides.thy	Sat Oct 20 12:09:30 2007 +0200
     3.2 +++ b/src/HOL/Divides.thy	Sat Oct 20 12:09:33 2007 +0200
     3.3 @@ -275,12 +275,14 @@
     3.4    by (auto simp add: split_ifs mult_ac quorem_def add_mult_distrib2)
     3.5  
     3.6  lemma div_mult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::nat)"
     3.7 -  apply (cases "c = 0", simp)
     3.8 +  apply (cases "c = 0", simp  add: neq0_conv)
     3.9 +  using neq0_conv
    3.10    apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_div])
    3.11    done
    3.12  
    3.13  lemma mod_mult1_eq: "(a*b) mod c = a*(b mod c) mod (c::nat)"
    3.14 -  apply (cases "c = 0", simp)
    3.15 +  apply (cases "c = 0", simp add: neq0_conv)
    3.16 +  using neq0_conv
    3.17    apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_mod])
    3.18    done
    3.19  
    3.20 @@ -307,11 +309,13 @@
    3.21  lemma div_add1_eq:
    3.22       "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
    3.23    apply (cases "c = 0", simp)
    3.24 +  using neq0_conv
    3.25    apply (blast intro: quorem_add1_eq [THEN quorem_div] quorem_div_mod quorem_div_mod)
    3.26    done
    3.27  
    3.28  lemma mod_add1_eq: "(a+b) mod (c::nat) = (a mod c + b mod c) mod c"
    3.29    apply (cases "c = 0", simp)
    3.30 +  using neq0_conv
    3.31    apply (blast intro: quorem_div_mod quorem_div_mod quorem_add1_eq [THEN quorem_mod])
    3.32    done
    3.33  
     4.1 --- a/src/HOL/HoareParallel/OG_Examples.thy	Sat Oct 20 12:09:30 2007 +0200
     4.2 +++ b/src/HOL/HoareParallel/OG_Examples.thy	Sat Oct 20 12:09:33 2007 +0200
     4.3 @@ -439,7 +439,7 @@
     4.4  apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
     4.5  apply(simp_all (asm_lr) only:length_0_conv [THEN sym])
     4.6  --{* 44 subgoals left *}
     4.7 -apply (simp_all (asm_lr) del:length_0_conv add: nth_list_update mod_less_divisor mod_lemma)
     4.8 +apply (simp_all (asm_lr) del:length_0_conv add: neq0_conv nth_list_update mod_less_divisor mod_lemma)
     4.9  --{* 32 subgoals left *}
    4.10  apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
    4.11  
     5.1 --- a/src/HOL/Hyperreal/Fact.thy	Sat Oct 20 12:09:30 2007 +0200
     5.2 +++ b/src/HOL/Hyperreal/Fact.thy	Sat Oct 20 12:09:33 2007 +0200
     5.3 @@ -20,7 +20,7 @@
     5.4    by (induct n) auto
     5.5  
     5.6  lemma fact_not_eq_zero [simp]: "fact n \<noteq> 0"
     5.7 -  by simp
     5.8 +  by (simp add: neq0_conv)
     5.9  
    5.10  lemma real_of_nat_fact_not_zero [simp]: "real (fact n) \<noteq> 0"
    5.11    by auto
     6.1 --- a/src/HOL/Hyperreal/HyperNat.thy	Sat Oct 20 12:09:30 2007 +0200
     6.2 +++ b/src/HOL/Hyperreal/HyperNat.thy	Sat Oct 20 12:09:33 2007 +0200
     6.3 @@ -331,8 +331,7 @@
     6.4       "\<forall>N::nat. {n. f n \<noteq> N} \<in> FreeUltrafilterNat
     6.5        ==> {n. N < f n} \<in> FreeUltrafilterNat"
     6.6  apply (induct_tac N)
     6.7 -apply (drule_tac x = 0 in spec)
     6.8 -apply (rule ccontr, drule FreeUltrafilterNat.not_memD, drule FreeUltrafilterNat.Int, assumption, simp)
     6.9 +apply (drule_tac x = 0 in spec, simp add: neq0_conv)
    6.10  apply (drule_tac x = "Suc n" in spec)
    6.11  apply (elim ultra, auto)
    6.12  done
     7.1 --- a/src/HOL/Hyperreal/Integration.thy	Sat Oct 20 12:09:30 2007 +0200
     7.2 +++ b/src/HOL/Hyperreal/Integration.thy	Sat Oct 20 12:09:33 2007 +0200
     7.3 @@ -149,12 +149,13 @@
     7.4  apply (rule_tac t = a in partition_lhs [THEN subst], assumption)
     7.5  apply (cut_tac x = "Suc n" and y = "psize D" in linorder_le_less_linear)
     7.6  apply (frule partition [THEN iffD1], safe)
     7.7 +using neq0_conv
     7.8   apply (blast intro: partition_lt less_le_trans)
     7.9  apply (rotate_tac 3)
    7.10  apply (drule_tac x = "Suc n" in spec)
    7.11  apply (erule impE)
    7.12  apply (erule less_imp_le)
    7.13 -apply (frule partition_rhs)
    7.14 +apply (frule partition_rhs, simp only: neq0_conv)
    7.15  apply (drule partition_gt, assumption)
    7.16  apply (simp (no_asm_simp))
    7.17  done
     8.1 --- a/src/HOL/Hyperreal/MacLaurin.thy	Sat Oct 20 12:09:30 2007 +0200
     8.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Sat Oct 20 12:09:33 2007 +0200
     8.3 @@ -279,11 +279,11 @@
     8.4  apply (case_tac "n = 0", force)
     8.5  apply (case_tac "x = 0")
     8.6  apply (rule_tac x = 0 in exI)
     8.7 -apply (force simp add: Maclaurin_bi_le_lemma)
     8.8 -apply (cut_tac x = x and y = 0 in linorder_less_linear, auto)
     8.9 +apply (force simp add: neq0_conv Maclaurin_bi_le_lemma)
    8.10 +apply (cut_tac x = x and y = 0 in linorder_less_linear, auto simp add: neq0_conv)
    8.11  txt{*Case 1, where @{term "x < 0"}*}
    8.12  apply (cut_tac f = "diff 0" and diff = diff and h = x and n = n in Maclaurin_minus_objl, safe)
    8.13 -apply (simp add: abs_if)
    8.14 +apply (simp add: abs_if neq0_conv)
    8.15  apply (rule_tac x = t in exI)
    8.16  apply (simp add: abs_if)
    8.17  txt{*Case 2, where @{term "0 < x"}*}
     9.1 --- a/src/HOL/Hyperreal/Poly.thy	Sat Oct 20 12:09:30 2007 +0200
     9.2 +++ b/src/HOL/Hyperreal/Poly.thy	Sat Oct 20 12:09:33 2007 +0200
     9.3 @@ -595,6 +595,7 @@
     9.4  lemma pderiv_aux_iszero_num: "(number_of n :: nat) \<noteq> 0
     9.5        ==> (list_all (%c. c = 0) (pderiv_aux (number_of n) p) =
     9.6        list_all (%c. c = 0) p)"
     9.7 +unfolding neq0_conv
     9.8  apply (rule_tac n1 = "number_of n" and m1 = 0 in less_imp_Suc_add [THEN exE], force)
     9.9  apply (rule_tac n1 = "0 + x" in pderiv_aux_iszero [THEN subst])
    9.10  apply (simp (no_asm_simp) del: pderiv_aux_iszero)
    9.11 @@ -793,7 +794,8 @@
    9.12  apply (simp add: poly_linear_divides del: pmult_Cons, safe)
    9.13  apply (drule_tac [!] a = a in order2)
    9.14  apply (rule ccontr)
    9.15 -apply (simp add: divides_def poly_mult fun_eq del: pmult_Cons, blast)
    9.16 +apply (simp add: divides_def poly_mult fun_eq neq0_conv del: pmult_Cons, blast)
    9.17 +using neq0_conv 
    9.18  apply (blast intro: lemma_order_root)
    9.19  done
    9.20  
    9.21 @@ -883,7 +885,7 @@
    9.22  lemma order_pderiv: "[| poly (pderiv p) \<noteq> poly []; order a p \<noteq> 0 |]
    9.23        ==> (order a p = Suc (order a (pderiv p)))"
    9.24  apply (case_tac "poly p = poly []")
    9.25 -apply (auto dest: pderiv_zero)
    9.26 +apply (auto simp add: neq0_conv  dest: pderiv_zero)
    9.27  apply (drule_tac a = a and p = p in order_decomp)
    9.28  apply (blast intro: lemma_order_pderiv)
    9.29  done
    9.30 @@ -951,7 +953,6 @@
    9.31  apply (simp add: fun_eq)
    9.32  apply (blast intro: order_poly)
    9.33  apply (auto simp add: order_root order_pderiv2)
    9.34 -apply (drule spec, auto)
    9.35  done
    9.36  
    9.37  lemma pmult_one: "[1] *** p = p"
    10.1 --- a/src/HOL/IntDiv.thy	Sat Oct 20 12:09:30 2007 +0200
    10.2 +++ b/src/HOL/IntDiv.thy	Sat Oct 20 12:09:33 2007 +0200
    10.3 @@ -1339,7 +1339,7 @@
    10.4    apply simp
    10.5    apply (case_tac "0 \<le> k")
    10.6    apply iprover
    10.7 -  apply (simp add: linorder_not_le)
    10.8 +  apply (simp add: neq0_conv linorder_not_le)
    10.9    apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
   10.10    apply assumption
   10.11    apply (simp add: mult_ac)
    11.1 --- a/src/HOL/Library/Binomial.thy	Sat Oct 20 12:09:30 2007 +0200
    11.2 +++ b/src/HOL/Library/Binomial.thy	Sat Oct 20 12:09:33 2007 +0200
    11.3 @@ -50,11 +50,11 @@
    11.4  lemma binomial_eq_0_iff: "(n choose k = 0) = (n<k)"
    11.5    apply (safe intro!: binomial_eq_0)
    11.6    apply (erule contrapos_pp)
    11.7 -  apply (simp add: zero_less_binomial)
    11.8 +  apply (simp add: neq0_conv zero_less_binomial)
    11.9    done
   11.10  
   11.11  lemma zero_less_binomial_iff: "(0 < n choose k) = (k\<le>n)"
   11.12 -  by (simp add: linorder_not_less [symmetric] binomial_eq_0_iff [symmetric])
   11.13 +  by (simp add: neq0_conv  linorder_not_less [symmetric] binomial_eq_0_iff [symmetric])
   11.14  
   11.15  (*Might be more useful if re-oriented*)
   11.16  lemma Suc_times_binomial_eq:
    12.1 --- a/src/HOL/Library/GCD.thy	Sat Oct 20 12:09:30 2007 +0200
    12.2 +++ b/src/HOL/Library/GCD.thy	Sat Oct 20 12:09:33 2007 +0200
    12.3 @@ -396,7 +396,7 @@
    12.4    assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
    12.5    shows "igcd (a div (igcd a b)) (b div (igcd a b)) = 1"
    12.6  proof -
    12.7 -  from nz have nz': "nat \<bar>a\<bar> \<noteq> 0 \<or> nat \<bar>b\<bar> \<noteq> 0" by simp
    12.8 +  from nz have nz': "nat \<bar>a\<bar> \<noteq> 0 \<or> nat \<bar>b\<bar> \<noteq> 0" by arith 
    12.9    let ?g = "igcd a b"
   12.10    let ?a' = "a div ?g"
   12.11    let ?b' = "b div ?g"
    13.1 --- a/src/HOL/Library/Nat_Infinity.thy	Sat Oct 20 12:09:30 2007 +0200
    13.2 +++ b/src/HOL/Library/Nat_Infinity.thy	Sat Oct 20 12:09:33 2007 +0200
    13.3 @@ -99,7 +99,7 @@
    13.4    by (simp add: inat_defs split:inat_splits)
    13.5  
    13.6  lemma i0_eq [simp]: "((0::inat) < n) = (n \<noteq> 0)"
    13.7 -  by (simp add: inat_defs split:inat_splits)
    13.8 +  by (simp add: neq0_conv inat_defs split:inat_splits)
    13.9  
   13.10  lemma i0_iless_iSuc [simp]: "0 < iSuc n"
   13.11    by (simp add: inat_defs split:inat_splits)
    14.1 --- a/src/HOL/Library/Word.thy	Sat Oct 20 12:09:30 2007 +0200
    14.2 +++ b/src/HOL/Library/Word.thy	Sat Oct 20 12:09:33 2007 +0200
    14.3 @@ -420,7 +420,7 @@
    14.4      apply (simp only: nat_to_bv_helper.simps [of n])
    14.5      apply (subst unfold_nat_to_bv_helper)
    14.6      using prems
    14.7 -    apply simp
    14.8 +    apply (simp add: neq0_conv)
    14.9      apply (subst nat_to_bv_def [of "n div 2"])
   14.10      apply auto
   14.11      done
   14.12 @@ -474,7 +474,7 @@
   14.13        apply (fold nat_to_bv_def)
   14.14        apply (simp add: ind' split del: split_if)
   14.15        apply (cases "n mod 2 = 0")
   14.16 -      proof simp_all
   14.17 +      proof (simp_all add: neq0_conv)
   14.18          assume "n mod 2 = 0"
   14.19          with mod_div_equality [of n 2]
   14.20          show "n div 2 * 2 = n"
   14.21 @@ -554,7 +554,7 @@
   14.22  
   14.23  lemma bv_to_nat_zero_imp_empty:
   14.24      "bv_to_nat w = 0 \<Longrightarrow> norm_unsigned w = []"
   14.25 -  by (atomize (full), induct w rule: bit_list_induct) simp_all
   14.26 +  by (atomize (full), induct w rule: bit_list_induct) (simp_all add: neq0_conv)
   14.27  
   14.28  lemma bv_to_nat_nzero_imp_nempty:
   14.29    "bv_to_nat w \<noteq> 0 \<Longrightarrow> norm_unsigned w \<noteq> []"
    15.1 --- a/src/HOL/List.thy	Sat Oct 20 12:09:30 2007 +0200
    15.2 +++ b/src/HOL/List.thy	Sat Oct 20 12:09:33 2007 +0200
    15.3 @@ -950,7 +950,9 @@
    15.4    proof (cases)
    15.5      assume "p x"
    15.6      hence eq: "?S' = insert 0 (Suc ` ?S)"
    15.7 -      by(auto simp add: nth_Cons image_def split:nat.split elim:lessE)
    15.8 +      apply (auto simp add:  nth_Cons image_def neq0_conv split:nat.split elim:lessE)
    15.9 +      apply (rule_tac x="xa - 1" in exI, auto)
   15.10 +      done
   15.11      have "length (filter p (x # xs)) = Suc(card ?S)"
   15.12        using Cons `p x` by simp
   15.13      also have "\<dots> = Suc(card(Suc ` ?S))" using fin
   15.14 @@ -961,7 +963,9 @@
   15.15    next
   15.16      assume "\<not> p x"
   15.17      hence eq: "?S' = Suc ` ?S"
   15.18 -      by(auto simp add: nth_Cons image_def split:nat.split elim:lessE)
   15.19 +      apply(auto simp add: nth_Cons image_def split:nat.split elim:lessE)
   15.20 +      apply (rule_tac x="xa - 1" in exI, auto)
   15.21 +      done
   15.22      have "length (filter p (x # xs)) = card ?S"
   15.23        using Cons `\<not> p x` by simp
   15.24      also have "\<dots> = card(Suc ` ?S)" using fin
   15.25 @@ -2453,7 +2457,7 @@
   15.26  lemma set_sublist: "set(sublist xs I) = {xs!i|i. i<size xs \<and> i \<in> I}"
   15.27  apply(induct xs arbitrary: I)
   15.28   apply simp
   15.29 -apply(auto simp add:sublist_Cons nth_Cons split:nat.split elim: lessE)
   15.30 +apply(auto simp add: neq0_conv sublist_Cons nth_Cons split:nat.split elim: lessE)
   15.31   apply(erule lessE)
   15.32    apply auto
   15.33  apply(erule lessE)
    16.1 --- a/src/HOL/Real/RealDef.thy	Sat Oct 20 12:09:30 2007 +0200
    16.2 +++ b/src/HOL/Real/RealDef.thy	Sat Oct 20 12:09:33 2007 +0200
    16.3 @@ -795,8 +795,8 @@
    16.4  lemma real_of_nat_div2:
    16.5    "0 <= real (n::nat) / real (x) - real (n div x)"
    16.6    apply(case_tac "x = 0")
    16.7 -  apply simp
    16.8 -  apply (simp add: compare_rls)
    16.9 +  apply (simp add: neq0_conv)
   16.10 +  apply (simp add: neq0_conv  compare_rls)
   16.11    apply (subst real_of_nat_div_aux)
   16.12    apply assumption
   16.13    apply simp
   16.14 @@ -807,8 +807,8 @@
   16.15  lemma real_of_nat_div3:
   16.16    "real (n::nat) / real (x) - real (n div x) <= 1"
   16.17    apply(case_tac "x = 0")
   16.18 -  apply simp
   16.19 -  apply (simp add: compare_rls)
   16.20 +  apply (simp add: neq0_conv )
   16.21 +  apply (simp add: compare_rls neq0_conv )
   16.22    apply (subst real_of_nat_div_aux)
   16.23    apply assumption
   16.24    apply simp
    17.1 --- a/src/HOL/Word/BinBoolList.thy	Sat Oct 20 12:09:30 2007 +0200
    17.2 +++ b/src/HOL/Word/BinBoolList.thy	Sat Oct 20 12:09:33 2007 +0200
    17.3 @@ -1103,7 +1103,7 @@
    17.4      (length ws <= m) = (nw + length bs * n <= m * n)"
    17.5    apply (rule_tac u=n and v=bs and w=nw and x=w in bin_rsplit_aux.induct)
    17.6    apply (subst bin_rsplit_aux.simps)
    17.7 -  apply (clarsimp simp: Let_def split: ls_splits)
    17.8 +  apply (clarsimp simp: Let_def neq0_conv split: ls_splits )
    17.9    apply (erule lrlem)
   17.10    done
   17.11  
    18.1 --- a/src/HOL/Word/BinOperations.thy	Sat Oct 20 12:09:30 2007 +0200
    18.2 +++ b/src/HOL/Word/BinOperations.thy	Sat Oct 20 12:09:33 2007 +0200
    18.3 @@ -353,7 +353,6 @@
    18.4    "!!w m. m ~= n ==> 
    18.5      bin_sc m c (bin_sc n b w) = bin_sc n b (bin_sc m c w)"
    18.6    apply (induct n)
    18.7 -   apply safe
    18.8     apply (case_tac [!] m)
    18.9       apply auto
   18.10    done
    19.1 --- a/src/HOL/Word/WordArith.thy	Sat Oct 20 12:09:30 2007 +0200
    19.2 +++ b/src/HOL/Word/WordArith.thy	Sat Oct 20 12:09:33 2007 +0200
    19.3 @@ -117,7 +117,7 @@
    19.4  lemmas unat_eq_zero = unat_0_iff
    19.5  
    19.6  lemma unat_gt_0: "(0 < unat x) = (x ~= 0)"
    19.7 -  by (simp add : unat_0_iff [symmetric])
    19.8 +  by (simp add : neq0_conv unat_0_iff [symmetric])
    19.9  
   19.10  lemma ucast_0 [simp] : "ucast 0 = 0"
   19.11    unfolding ucast_def
   19.12 @@ -1245,7 +1245,7 @@
   19.13    apply (rule contrapos_np)
   19.14     prefer 2
   19.15     apply (erule card_infinite)
   19.16 -  apply (simp add : card_word)
   19.17 +  apply (simp add : card_word neq0_conv)
   19.18    done
   19.19  
   19.20  lemma card_word_size: 
    20.1 --- a/src/HOL/ex/Reflected_Presburger.thy	Sat Oct 20 12:09:30 2007 +0200
    20.2 +++ b/src/HOL/ex/Reflected_Presburger.thy	Sat Oct 20 12:09:33 2007 +0200
    20.3 @@ -189,13 +189,13 @@
    20.4  
    20.5  lemma numsubst0_I:
    20.6    shows "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b#bs) a)#bs) t"
    20.7 -  by (induct t rule: numsubst0.induct,auto simp add: gr0_conv_Suc)
    20.8 +  by (induct t rule: numsubst0.induct,auto simp add: gr0_conv_Suc neq0_conv)
    20.9  
   20.10  lemma numsubst0_I':
   20.11    assumes nb: "numbound0 a"
   20.12    shows "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b'#bs) a)#bs) t"
   20.13    using nb
   20.14 -  by (induct t rule: numsubst0.induct, auto simp add: gr0_conv_Suc numbound0_I[where b="b" and b'="b'"])
   20.15 +  by (induct t rule: numsubst0.induct, auto simp add: neq0_conv gr0_conv_Suc numbound0_I[where b="b" and b'="b'"])
   20.16  
   20.17  primrec
   20.18    "subst0 t T = T"