tuned the simp rules for Int involving insert and intervals.
authornipkow
Mon Aug 31 14:09:42 2009 +0200 (2009-08-31)
changeset 32456341c83339aeb
parent 32450 375db037f4d2
child 32457 4595ff1d1a1a
tuned the simp rules for Int involving insert and intervals.
src/HOL/Algebra/Divisibility.thy
src/HOL/Algebra/UnivPoly.thy
src/HOL/Algebra/poly/UnivPoly2.thy
src/HOL/Bali/Example.thy
src/HOL/Isar_examples/Mutilated_Checkerboard.thy
src/HOL/Library/Abstract_Rat.thy
src/HOL/Library/Continuity.thy
src/HOL/Library/Convex_Euclidean_Space.thy
src/HOL/Library/Euclidean_Space.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Library/Fundamental_Theorem_Algebra.thy
src/HOL/Library/Permutations.thy
src/HOL/Library/Univ_Poly.thy
src/HOL/Library/Word.thy
src/HOL/Nat.thy
src/HOL/Set.thy
src/HOL/SetInterval.thy
src/HOL/UNITY/Simple/Common.thy
     1.1 --- a/src/HOL/Algebra/Divisibility.thy	Sat Aug 29 14:31:39 2009 +0200
     1.2 +++ b/src/HOL/Algebra/Divisibility.thy	Mon Aug 31 14:09:42 2009 +0200
     1.3 @@ -2656,25 +2656,7 @@
     1.4    shows "(x \<in> carrier G \<and> x gcdof a b) =
     1.5           greatest (division_rel G) x (Lower (division_rel G) {a, b})"
     1.6  unfolding isgcd_def greatest_def Lower_def elem_def
     1.7 -proof (simp, safe)
     1.8 -  fix xa
     1.9 -  assume r1[rule_format]: "\<forall>x. (x = a \<or> x = b) \<and> x \<in> carrier G \<longrightarrow> xa divides x"
    1.10 -  assume r2[rule_format]: "\<forall>y\<in>carrier G. y divides a \<and> y divides b \<longrightarrow> y divides x"
    1.11 -
    1.12 -  assume "xa \<in> carrier G"  "x divides a"  "x divides b"
    1.13 -  with carr
    1.14 -  show "xa divides x"
    1.15 -      by (fast intro: r1 r2)
    1.16 -next
    1.17 -  fix a' y
    1.18 -  assume r1[rule_format]:
    1.19 -         "\<forall>xa\<in>{l. \<forall>x. (x = a \<or> x = b) \<and> x \<in> carrier G \<longrightarrow> l divides x} \<inter> carrier G.
    1.20 -           xa divides x"
    1.21 -  assume "y \<in> carrier G"  "y divides a"  "y divides b"
    1.22 -  with carr
    1.23 -       show "y divides x"
    1.24 -       by (fast intro: r1)
    1.25 -qed (simp, simp)
    1.26 +by auto
    1.27  
    1.28  lemma lcmof_leastUpper:
    1.29    fixes G (structure)
    1.30 @@ -2682,25 +2664,7 @@
    1.31    shows "(x \<in> carrier G \<and> x lcmof a b) =
    1.32           least (division_rel G) x (Upper (division_rel G) {a, b})"
    1.33  unfolding islcm_def least_def Upper_def elem_def
    1.34 -proof (simp, safe)
    1.35 -  fix xa
    1.36 -  assume r1[rule_format]: "\<forall>x. (x = a \<or> x = b) \<and> x \<in> carrier G \<longrightarrow> x divides xa"
    1.37 -  assume r2[rule_format]: "\<forall>y\<in>carrier G. a divides y \<and> b divides y \<longrightarrow> x divides y"
    1.38 -
    1.39 -  assume "xa \<in> carrier G"  "a divides x"  "b divides x"
    1.40 -  with carr
    1.41 -  show "x divides xa"
    1.42 -      by (fast intro: r1 r2)
    1.43 -next
    1.44 -  fix a' y
    1.45 -  assume r1[rule_format]:
    1.46 -         "\<forall>xa\<in>{l. \<forall>x. (x = a \<or> x = b) \<and> x \<in> carrier G \<longrightarrow> x divides l} \<inter> carrier G.
    1.47 -           x divides xa"
    1.48 -  assume "y \<in> carrier G"  "a divides y"  "b divides y"
    1.49 -  with carr
    1.50 -       show "x divides y"
    1.51 -       by (fast intro: r1)
    1.52 -qed (simp, simp)
    1.53 +by auto
    1.54  
    1.55  lemma somegcd_meet:
    1.56    fixes G (structure)
     2.1 --- a/src/HOL/Algebra/UnivPoly.thy	Sat Aug 29 14:31:39 2009 +0200
     2.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Mon Aug 31 14:09:42 2009 +0200
     2.3 @@ -592,15 +592,14 @@
     2.4          proof (cases "n = k")
     2.5            case True
     2.6            then have "\<zero> = (\<Oplus>i \<in> {..<n} \<union> {n}. ?s i)"
     2.7 -            by (simp cong: R.finsum_cong add: ivl_disj_int_singleton Pi_def)
     2.8 +            by (simp cong: R.finsum_cong add: Pi_def)
     2.9            also from True have "... = (\<Oplus>i \<in> {..k}. ?s i)"
    2.10              by (simp only: ivl_disj_un_singleton)
    2.11            finally show ?thesis .
    2.12          next
    2.13            case False with n_le_k have n_less_k: "n < k" by arith
    2.14            with neq have "\<zero> = (\<Oplus>i \<in> {..<n} \<union> {n}. ?s i)"
    2.15 -            by (simp add: R.finsum_Un_disjoint f1 f2
    2.16 -              ivl_disj_int_singleton Pi_def del: Un_insert_right)
    2.17 +            by (simp add: R.finsum_Un_disjoint f1 f2 Pi_def del: Un_insert_right)
    2.18            also have "... = (\<Oplus>i \<in> {..n}. ?s i)"
    2.19              by (simp only: ivl_disj_un_singleton)
    2.20            also from n_less_k neq have "... = (\<Oplus>i \<in> {..n} \<union> {n<..k}. ?s i)"
    2.21 @@ -939,8 +938,7 @@
    2.22      also have "...= (\<Oplus>i \<in> {deg R p} \<union> {deg R p <.. deg R p + deg R q}. ?s i)"
    2.23        by (simp only: ivl_disj_un_singleton)
    2.24      also have "... = coeff P p (deg R p) \<otimes> coeff P q (deg R q)"
    2.25 -      by (simp cong: R.finsum_cong
    2.26 -	add: ivl_disj_int_singleton deg_aboveD R Pi_def)
    2.27 +      by (simp cong: R.finsum_cong add: deg_aboveD R Pi_def)
    2.28      finally have "(\<Oplus>i \<in> {.. deg R p + deg R q}. ?s i)
    2.29        = coeff P p (deg R p) \<otimes> coeff P q (deg R q)" .
    2.30      with nz show "(\<Oplus>i \<in> {.. deg R p + deg R q}. ?s i) ~= \<zero>"
    2.31 @@ -983,8 +981,7 @@
    2.32      have "... = coeff P (\<Oplus>\<^bsub>P\<^esub> i \<in> {..<k} \<union> {k}. ?s i) k"
    2.33        by (simp only: ivl_disj_un_singleton)
    2.34      also have "... = coeff P p k"
    2.35 -      by (simp cong: R.finsum_cong
    2.36 -	add: ivl_disj_int_singleton coeff_finsum deg_aboveD R RR Pi_def)
    2.37 +      by (simp cong: R.finsum_cong add: coeff_finsum deg_aboveD R RR Pi_def)
    2.38      finally show ?thesis .
    2.39    next
    2.40      case False
    2.41 @@ -992,8 +989,7 @@
    2.42            coeff P (\<Oplus>\<^bsub>P\<^esub> i \<in> {..<deg R p} \<union> {deg R p}. ?s i) k"
    2.43        by (simp only: ivl_disj_un_singleton)
    2.44      also from False have "... = coeff P p k"
    2.45 -      by (simp cong: R.finsum_cong
    2.46 -	add: ivl_disj_int_singleton coeff_finsum deg_aboveD R Pi_def)
    2.47 +      by (simp cong: R.finsum_cong add: coeff_finsum deg_aboveD R Pi_def)
    2.48      finally show ?thesis .
    2.49    qed
    2.50  qed (simp_all add: R Pi_def)
     3.1 --- a/src/HOL/Algebra/poly/UnivPoly2.thy	Sat Aug 29 14:31:39 2009 +0200
     3.2 +++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Mon Aug 31 14:09:42 2009 +0200
     3.3 @@ -674,8 +674,7 @@
     3.4      also have "... = setsum ?s ({deg p} Un {deg p <.. deg p + deg q})"
     3.5        by (simp only: ivl_disj_un_singleton)
     3.6      also have "... = coeff p (deg p) * coeff q (deg q)" 
     3.7 -      by (simp add: setsum_Un_disjoint ivl_disj_int_singleton 
     3.8 -        setsum_0 deg_aboveD)
     3.9 +      by (simp add: setsum_Un_disjoint setsum_0 deg_aboveD)
    3.10      finally have "setsum ?s {.. deg p + deg q} 
    3.11        = coeff p (deg p) * coeff q (deg q)" .
    3.12      with nz show "setsum ?s {.. deg p + deg q} ~= 0"
    3.13 @@ -719,8 +718,7 @@
    3.14      have "... = coeff (setsum ?s ({..<k} Un {k})) k"
    3.15        by (simp only: ivl_disj_un_singleton)
    3.16      also have "... = coeff p k"
    3.17 -      by (simp add: setsum_Un_disjoint ivl_disj_int_singleton 
    3.18 -        setsum_0 coeff_natsum deg_aboveD)
    3.19 +      by (simp add: setsum_Un_disjoint setsum_0 coeff_natsum deg_aboveD)
    3.20      finally show ?thesis .
    3.21    next
    3.22      case False
    3.23 @@ -728,8 +726,7 @@
    3.24            coeff (setsum ?s ({..<deg p} Un {deg p})) k"
    3.25        by (simp only: ivl_disj_un_singleton)
    3.26      also from False have "... = coeff p k"
    3.27 -      by (simp add: setsum_Un_disjoint ivl_disj_int_singleton 
    3.28 -        setsum_0 coeff_natsum deg_aboveD)
    3.29 +      by (simp add: setsum_Un_disjoint setsum_0 coeff_natsum deg_aboveD)
    3.30      finally show ?thesis .
    3.31    qed
    3.32  qed
     4.1 --- a/src/HOL/Bali/Example.thy	Sat Aug 29 14:31:39 2009 +0200
     4.2 +++ b/src/HOL/Bali/Example.thy	Mon Aug 31 14:09:42 2009 +0200
     4.3 @@ -1167,7 +1167,6 @@
     4.4  apply    (simp,rule assigned.select_convs)
     4.5  apply   (simp)
     4.6  apply  simp
     4.7 -apply  blast
     4.8  apply simp
     4.9  apply (simp add: intersect_ts_def)
    4.10  done
     5.1 --- a/src/HOL/Isar_examples/Mutilated_Checkerboard.thy	Sat Aug 29 14:31:39 2009 +0200
     5.2 +++ b/src/HOL/Isar_examples/Mutilated_Checkerboard.thy	Mon Aug 31 14:09:42 2009 +0200
     5.3 @@ -113,7 +113,7 @@
     5.4  lemma evnodd_insert: "evnodd (insert (i, j) C) b =
     5.5      (if (i + j) mod 2 = b
     5.6        then insert (i, j) (evnodd C b) else evnodd C b)"
     5.7 -  by (simp add: evnodd_def) blast
     5.8 +  by (simp add: evnodd_def)
     5.9  
    5.10  
    5.11  subsection {* Dominoes *}
     6.1 --- a/src/HOL/Library/Abstract_Rat.thy	Sat Aug 29 14:31:39 2009 +0200
     6.2 +++ b/src/HOL/Library/Abstract_Rat.thy	Mon Aug 31 14:09:42 2009 +0200
     6.3 @@ -189,14 +189,9 @@
     6.4    have "\<exists> a b a' b'. x = (a,b) \<and> y = (a',b')" by auto
     6.5    then obtain a b a' b' where xy[simp]: "x = (a,b)" "y=(a',b')" by blast
     6.6    assume H: ?lhs 
     6.7 -  {assume "a = 0 \<or> b = 0 \<or> a' = 0 \<or> b' = 0" hence ?rhs
     6.8 -      using na nb H
     6.9 -      apply (simp add: INum_def split_def isnormNum_def)
    6.10 -      apply (cases "a = 0", simp_all)
    6.11 -      apply (cases "b = 0", simp_all)
    6.12 -      apply (cases "a' = 0", simp_all)
    6.13 -      apply (cases "a' = 0", simp_all add: of_int_eq_0_iff)
    6.14 -      done}
    6.15 +  {assume "a = 0 \<or> b = 0 \<or> a' = 0 \<or> b' = 0"
    6.16 +    hence ?rhs using na nb H
    6.17 +      by (simp add: INum_def split_def isnormNum_def split: split_if_asm)}
    6.18    moreover
    6.19    { assume az: "a \<noteq> 0" and bz: "b \<noteq> 0" and a'z: "a'\<noteq>0" and b'z: "b'\<noteq>0"
    6.20      from az bz a'z b'z na nb have pos: "b > 0" "b' > 0" by (simp_all add: isnormNum_def)
    6.21 @@ -517,10 +512,7 @@
    6.22      have n0: "isnormNum 0\<^sub>N" by simp
    6.23      show ?thesis using nx ny 
    6.24        apply (simp only: isnormNum_unique[where ?'a = 'a, OF  Nmul_normN[OF nx ny] n0, symmetric] Nmul[where ?'a = 'a])
    6.25 -      apply (simp add: INum_def split_def isnormNum_def fst_conv snd_conv)
    6.26 -      apply (cases "a=0",simp_all)
    6.27 -      apply (cases "a'=0",simp_all)
    6.28 -      done
    6.29 +      by (simp add: INum_def split_def isnormNum_def fst_conv snd_conv split: split_if_asm)
    6.30    }
    6.31  qed
    6.32  lemma Nneg_Nneg[simp]: "~\<^sub>N (~\<^sub>N c) = c"
     7.1 --- a/src/HOL/Library/Continuity.thy	Sat Aug 29 14:31:39 2009 +0200
     7.2 +++ b/src/HOL/Library/Continuity.thy	Mon Aug 31 14:09:42 2009 +0200
     7.3 @@ -156,7 +156,7 @@
     7.4   apply (rule up_chainI)
     7.5   apply simp
     7.6  apply (drule Un_absorb1)
     7.7 -apply (auto simp add: nat_not_singleton)
     7.8 +apply (auto split:split_if_asm)
     7.9  done
    7.10  
    7.11  
    7.12 @@ -184,8 +184,7 @@
    7.13   apply (rule down_chainI)
    7.14   apply simp
    7.15  apply (drule Int_absorb1)
    7.16 -apply auto
    7.17 -apply (auto simp add: nat_not_singleton)
    7.18 +apply (auto split:split_if_asm)
    7.19  done
    7.20  
    7.21  
     8.1 --- a/src/HOL/Library/Convex_Euclidean_Space.thy	Sat Aug 29 14:31:39 2009 +0200
     8.2 +++ b/src/HOL/Library/Convex_Euclidean_Space.thy	Mon Aug 31 14:09:42 2009 +0200
     8.3 @@ -3355,9 +3355,8 @@
     8.4    qed(auto intro!:path_connected_singleton) next
     8.5    case False hence *:"{x::real^'n. norm(x - a) = r} = (\<lambda>x. a + r *\<^sub>R x) ` {x. norm x = 1}" unfolding not_le apply -apply(rule set_ext,rule)
     8.6      unfolding image_iff apply(rule_tac x="(1/r) *\<^sub>R (x - a)" in bexI) unfolding mem_Collect_eq norm_scaleR by (auto simp add: scaleR_right_diff_distrib)
     8.7 -  have ***:"\<And>xa. (if xa = 0 then 0 else 1) \<noteq> 1 \<Longrightarrow> xa = 0" apply(rule ccontr) by auto
     8.8    have **:"{x::real^'n. norm x = 1} = (\<lambda>x. (1/norm x) *\<^sub>R x) ` (UNIV - {0})" apply(rule set_ext,rule)
     8.9 -    unfolding image_iff apply(rule_tac x=x in bexI) unfolding mem_Collect_eq by(auto intro!: ***)
    8.10 +    unfolding image_iff apply(rule_tac x=x in bexI) unfolding mem_Collect_eq by(auto split:split_if_asm)
    8.11    have "continuous_on (UNIV - {0}) (\<lambda>x::real^'n. 1 / norm x)" unfolding o_def continuous_on_eq_continuous_within
    8.12      apply(rule, rule continuous_at_within_inv[unfolded o_def inverse_eq_divide]) apply(rule continuous_at_within)
    8.13      apply(rule continuous_at_norm[unfolded o_def]) by auto
     9.1 --- a/src/HOL/Library/Euclidean_Space.thy	Sat Aug 29 14:31:39 2009 +0200
     9.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Mon Aug 31 14:09:42 2009 +0200
     9.3 @@ -1055,28 +1055,6 @@
     9.4  lemma norm_triangle_lt: "norm(x::real ^'n::finite) + norm(y) < e ==> norm(x + y) < e"
     9.5    by (metis basic_trans_rules(21) norm_triangle_ineq)
     9.6  
     9.7 -lemma setsum_delta:
     9.8 -  assumes fS: "finite S"
     9.9 -  shows "setsum (\<lambda>k. if k=a then b k else 0) S = (if a \<in> S then b a else 0)"
    9.10 -proof-
    9.11 -  let ?f = "(\<lambda>k. if k=a then b k else 0)"
    9.12 -  {assume a: "a \<notin> S"
    9.13 -    hence "\<forall> k\<in> S. ?f k = 0" by simp
    9.14 -    hence ?thesis  using a by simp}
    9.15 -  moreover
    9.16 -  {assume a: "a \<in> S"
    9.17 -    let ?A = "S - {a}"
    9.18 -    let ?B = "{a}"
    9.19 -    have eq: "S = ?A \<union> ?B" using a by blast
    9.20 -    have dj: "?A \<inter> ?B = {}" by simp
    9.21 -    from fS have fAB: "finite ?A" "finite ?B" by auto
    9.22 -    have "setsum ?f S = setsum ?f ?A + setsum ?f ?B"
    9.23 -      using setsum_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
    9.24 -      by simp
    9.25 -    then have ?thesis  using a by simp}
    9.26 -  ultimately show ?thesis by blast
    9.27 -qed
    9.28 -
    9.29  lemma component_le_norm: "\<bar>x$i\<bar> <= norm (x::real ^ 'n::finite)"
    9.30    apply (simp add: norm_vector_def)
    9.31    apply (rule member_le_setL2, simp_all)
    9.32 @@ -2079,13 +2057,6 @@
    9.33  lemma matrix_add_ldistrib: "(A ** (B + C)) = (A \<star> B) + (A \<star> C)"
    9.34    by (vector matrix_matrix_mult_def setsum_addf[symmetric] ring_simps)
    9.35  
    9.36 -lemma setsum_delta':
    9.37 -  assumes fS: "finite S" shows
    9.38 -  "setsum (\<lambda>k. if a = k then b k else 0) S =
    9.39 -     (if a\<in> S then b a else 0)"
    9.40 -  using setsum_delta[OF fS, of a b, symmetric]
    9.41 -  by (auto intro: setsum_cong)
    9.42 -
    9.43  lemma matrix_mul_lid:
    9.44    fixes A :: "'a::semiring_1 ^ 'm ^ 'n::finite"
    9.45    shows "mat 1 ** A = A"
    10.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Sat Aug 29 14:31:39 2009 +0200
    10.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Mon Aug 31 14:09:42 2009 +0200
    10.3 @@ -633,8 +633,7 @@
    10.4  	    by (auto simp add: inverse_eq_divide power_divide)
    10.5  
    10.6  	  from k have kn: "k > n"
    10.7 -	    apply (simp add: leastP_def setge_def fps_sum_rep_nth)
    10.8 -	    by (cases "k \<le> n", auto)
    10.9 +	    by (simp add: leastP_def setge_def fps_sum_rep_nth split:split_if_asm)
   10.10  	  then have "dist (?s n) a < (1/2)^n" unfolding dth
   10.11  	    by (auto intro: power_strict_decreasing)
   10.12  	  also have "\<dots> <= (1/2)^n0" using nn0
   10.13 @@ -1244,10 +1243,9 @@
   10.14      {assume n0: "n \<noteq> 0"
   10.15        then have u: "{0} \<union> ({1} \<union> {2..n}) = {0..n}" "{1}\<union>{2..n} = {1..n}"
   10.16  	"{0..n - 1}\<union>{n} = {0..n}"
   10.17 -	apply (simp_all add: expand_set_eq) by presburger+
   10.18 +	by (auto simp: expand_set_eq)
   10.19        have d: "{0} \<inter> ({1} \<union> {2..n}) = {}" "{1} \<inter> {2..n} = {}"
   10.20 -	"{0..n - 1}\<inter>{n} ={}" using n0
   10.21 -	by (simp_all add: expand_set_eq, presburger+)
   10.22 +	"{0..n - 1}\<inter>{n} ={}" using n0 by simp_all
   10.23        have f: "finite {0}" "finite {1}" "finite {2 .. n}"
   10.24  	"finite {0 .. n - 1}" "finite {n}" by simp_all
   10.25      have "((1 - ?X) * ?sa) $ n = setsum (\<lambda>i. (1 - ?X)$ i * ?sa $ (n - i)) {0 .. n}"
    11.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sat Aug 29 14:31:39 2009 +0200
    11.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Mon Aug 31 14:09:42 2009 +0200
    11.3 @@ -577,11 +577,12 @@
    11.4  next
    11.5    case (pCons c cs)
    11.6    {assume c0: "c = 0"
    11.7 -    from pCons.hyps pCons.prems c0 have ?case apply auto
    11.8 +    from pCons.hyps pCons.prems c0 have ?case
    11.9 +      apply (auto)
   11.10        apply (rule_tac x="k+1" in exI)
   11.11        apply (rule_tac x="a" in exI, clarsimp)
   11.12        apply (rule_tac x="q" in exI)
   11.13 -      by (auto simp add: power_Suc)}
   11.14 +      by (auto)}
   11.15    moreover
   11.16    {assume c0: "c\<noteq>0"
   11.17      hence ?case apply-
    12.1 --- a/src/HOL/Library/Permutations.thy	Sat Aug 29 14:31:39 2009 +0200
    12.2 +++ b/src/HOL/Library/Permutations.thy	Mon Aug 31 14:09:42 2009 +0200
    12.3 @@ -843,9 +843,7 @@
    12.4  	unfolding permutes_def by metis+
    12.5        from eq have "(Fun.swap a b id o p) a  = (Fun.swap a c id o q) a" by simp
    12.6        hence bc: "b = c"
    12.7 -	apply (simp add: permutes_def pa qa o_def fun_upd_def swap_def id_def cong del: if_weak_cong)
    12.8 -	apply (cases "a = b", auto)
    12.9 -	by (cases "b = c", auto)
   12.10 +	by (simp add: permutes_def pa qa o_def fun_upd_def swap_def id_def cong del: if_weak_cong split: split_if_asm)
   12.11        from eq[unfolded bc] have "(\<lambda>p. Fun.swap a c id o p) (Fun.swap a c id o p) = (\<lambda>p. Fun.swap a c id o p) (Fun.swap a c id o q)" by simp
   12.12        hence "p = q" unfolding o_assoc swap_id_idempotent
   12.13  	by (simp add: o_def)
    13.1 --- a/src/HOL/Library/Univ_Poly.thy	Sat Aug 29 14:31:39 2009 +0200
    13.2 +++ b/src/HOL/Library/Univ_Poly.thy	Mon Aug 31 14:09:42 2009 +0200
    13.3 @@ -820,37 +820,24 @@
    13.4      done
    13.5  qed
    13.6  
    13.7 -lemma (in semiring_0) pnormalize_sing: "(pnormalize [x] = [x]) \<longleftrightarrow> x \<noteq> 0" by simp
    13.8 +lemma (in semiring_0) pnormalize_sing: "(pnormalize [x] = [x]) \<longleftrightarrow> x \<noteq> 0"
    13.9 +by simp
   13.10  lemma (in semiring_0) pnormalize_pair: "y \<noteq> 0 \<longleftrightarrow> (pnormalize [x, y] = [x, y])" by simp
   13.11  lemma (in semiring_0) pnormal_cons: "pnormal p \<Longrightarrow> pnormal (c#p)"
   13.12    unfolding pnormal_def by simp
   13.13  lemma (in semiring_0) pnormal_tail: "p\<noteq>[] \<Longrightarrow> pnormal (c#p) \<Longrightarrow> pnormal p"
   13.14 -  unfolding pnormal_def
   13.15 -  apply (cases "pnormalize p = []", auto)
   13.16 -  by (cases "c = 0", auto)
   13.17 +  unfolding pnormal_def by(auto split: split_if_asm)
   13.18  
   13.19  
   13.20  lemma (in semiring_0) pnormal_last_nonzero: "pnormal p ==> last p \<noteq> 0"
   13.21 -proof(induct p)
   13.22 -  case Nil thus ?case by (simp add: pnormal_def)
   13.23 -next
   13.24 -  case (Cons a as) thus ?case
   13.25 -    apply (simp add: pnormal_def)
   13.26 -    apply (cases "pnormalize as = []", simp_all)
   13.27 -    apply (cases "as = []", simp_all)
   13.28 -    apply (cases "a=0", simp_all)
   13.29 -    apply (cases "a=0", simp_all)
   13.30 -    done
   13.31 -qed
   13.32 +by(induct p) (simp_all add: pnormal_def split: split_if_asm)
   13.33  
   13.34  lemma (in semiring_0) pnormal_length: "pnormal p \<Longrightarrow> 0 < length p"
   13.35    unfolding pnormal_def length_greater_0_conv by blast
   13.36  
   13.37  lemma (in semiring_0) pnormal_last_length: "\<lbrakk>0 < length p ; last p \<noteq> 0\<rbrakk> \<Longrightarrow> pnormal p"
   13.38 -  apply (induct p, auto)
   13.39 -  apply (case_tac "p = []", auto)
   13.40 -  apply (simp add: pnormal_def)
   13.41 -  by (rule pnormal_cons, auto)
   13.42 +by (induct p) (auto simp: pnormal_def  split: split_if_asm)
   13.43 +
   13.44  
   13.45  lemma (in semiring_0) pnormal_id: "pnormal p \<longleftrightarrow> (0 < length p \<and> last p \<noteq> 0)"
   13.46    using pnormal_last_length pnormal_length pnormal_last_nonzero by blast
   13.47 @@ -918,9 +905,7 @@
   13.48  qed
   13.49  
   13.50  lemma (in semiring_0) pnormalize_eq: "last p \<noteq> 0 \<Longrightarrow> pnormalize p = p"
   13.51 -  apply (induct p, auto)
   13.52 -  apply (case_tac p, auto)+
   13.53 -  done
   13.54 +by (induct p) (auto split: split_if_asm)
   13.55  
   13.56  lemma (in semiring_0) last_pnormalize: "pnormalize p \<noteq> [] \<Longrightarrow> last (pnormalize p) \<noteq> 0"
   13.57    by (induct p, auto)
    14.1 --- a/src/HOL/Library/Word.thy	Sat Aug 29 14:31:39 2009 +0200
    14.2 +++ b/src/HOL/Library/Word.thy	Mon Aug 31 14:09:42 2009 +0200
    14.3 @@ -1008,12 +1008,7 @@
    14.4    fix xs
    14.5    assume "length (norm_signed (\<zero>#xs)) = Suc (length xs)"
    14.6    thus "norm_signed (\<zero>#xs) = \<zero>#xs"
    14.7 -    apply (simp add: norm_signed_Cons)
    14.8 -    apply safe
    14.9 -    apply simp_all
   14.10 -    apply (rule norm_unsigned_equal)
   14.11 -    apply assumption
   14.12 -    done
   14.13 +    by (simp add: norm_signed_Cons norm_unsigned_equal split: split_if_asm)
   14.14  next
   14.15    fix xs
   14.16    assume "length (norm_signed (\<one>#xs)) = Suc (length xs)"
    15.1 --- a/src/HOL/Nat.thy	Sat Aug 29 14:31:39 2009 +0200
    15.2 +++ b/src/HOL/Nat.thy	Mon Aug 31 14:09:42 2009 +0200
    15.3 @@ -1588,9 +1588,6 @@
    15.4  lemma zero_induct: "P k ==> (!!n. P (Suc n) ==> P n) ==> P 0"
    15.5    using inc_induct[of 0 k P] by blast
    15.6  
    15.7 -lemma nat_not_singleton: "(\<forall>x. x = (0::nat)) = False"
    15.8 -  by auto
    15.9 -
   15.10  (*The others are
   15.11        i - j - k = i - (j + k),
   15.12        k \<le> j ==> j - k + i = j + i - k,
    16.1 --- a/src/HOL/Set.thy	Sat Aug 29 14:31:39 2009 +0200
    16.2 +++ b/src/HOL/Set.thy	Mon Aug 31 14:09:42 2009 +0200
    16.3 @@ -1268,10 +1268,26 @@
    16.4      "(insert a B) Int C = (if a \<in> C then insert a (B \<inter> C) else B \<inter> C)"
    16.5    by auto
    16.6  
    16.7 +lemma Int_insert_left_if0[simp]:
    16.8 +    "a \<notin> C \<Longrightarrow> (insert a B) Int C = B \<inter> C"
    16.9 +  by auto
   16.10 +
   16.11 +lemma Int_insert_left_if1[simp]:
   16.12 +    "a \<in> C \<Longrightarrow> (insert a B) Int C = insert a (B Int C)"
   16.13 +  by auto
   16.14 +
   16.15  lemma Int_insert_right:
   16.16      "A \<inter> (insert a B) = (if a \<in> A then insert a (A \<inter> B) else A \<inter> B)"
   16.17    by auto
   16.18  
   16.19 +lemma Int_insert_right_if0[simp]:
   16.20 +    "a \<notin> A \<Longrightarrow> A Int (insert a B) = A Int B"
   16.21 +  by auto
   16.22 +
   16.23 +lemma Int_insert_right_if1[simp]:
   16.24 +    "a \<in> A \<Longrightarrow> A Int (insert a B) = insert a (A Int B)"
   16.25 +  by auto
   16.26 +
   16.27  lemma Un_Int_distrib: "A \<union> (B \<inter> C) = (A \<union> B) \<inter> (A \<union> C)"
   16.28    by blast
   16.29  
    17.1 --- a/src/HOL/SetInterval.thy	Sat Aug 29 14:31:39 2009 +0200
    17.2 +++ b/src/HOL/SetInterval.thy	Mon Aug 31 14:09:42 2009 +0200
    17.3 @@ -251,6 +251,38 @@
    17.4  apply (simp add: less_imp_le)
    17.5  done
    17.6  
    17.7 +subsubsection {* Intersection *}
    17.8 +
    17.9 +context linorder
   17.10 +begin
   17.11 +
   17.12 +lemma Int_atLeastAtMost[simp]: "{a..b} Int {c..d} = {max a c .. min b d}"
   17.13 +by auto
   17.14 +
   17.15 +lemma Int_atLeastAtMostR1[simp]: "{..b} Int {c..d} = {c .. min b d}"
   17.16 +by auto
   17.17 +
   17.18 +lemma Int_atLeastAtMostR2[simp]: "{a..} Int {c..d} = {max a c .. d}"
   17.19 +by auto
   17.20 +
   17.21 +lemma Int_atLeastAtMostL1[simp]: "{a..b} Int {..d} = {a .. min b d}"
   17.22 +by auto
   17.23 +
   17.24 +lemma Int_atLeastAtMostL2[simp]: "{a..b} Int {c..} = {max a c .. b}"
   17.25 +by auto
   17.26 +
   17.27 +lemma Int_atLeastLessThan[simp]: "{a..<b} Int {c..<d} = {max a c ..< min b d}"
   17.28 +by auto
   17.29 +
   17.30 +lemma Int_greaterThanAtMost[simp]: "{a<..b} Int {c<..d} = {max a c <.. min b d}"
   17.31 +by auto
   17.32 +
   17.33 +lemma Int_greaterThanLessThan[simp]: "{a<..<b} Int {c<..<d} = {max a c <..< min b d}"
   17.34 +by auto
   17.35 +
   17.36 +end
   17.37 +
   17.38 +
   17.39  subsection {* Intervals of natural numbers *}
   17.40  
   17.41  subsubsection {* The Constant @{term lessThan} *}
   17.42 @@ -705,17 +737,6 @@
   17.43  
   17.44  subsubsection {* Disjoint Intersections *}
   17.45  
   17.46 -text {* Singletons and open intervals *}
   17.47 -
   17.48 -lemma ivl_disj_int_singleton:
   17.49 -  "{l::'a::order} Int {l<..} = {}"
   17.50 -  "{..<u} Int {u} = {}"
   17.51 -  "{l} Int {l<..<u} = {}"
   17.52 -  "{l<..<u} Int {u} = {}"
   17.53 -  "{l} Int {l<..u} = {}"
   17.54 -  "{l..<u} Int {u} = {}"
   17.55 -  by simp+
   17.56 -
   17.57  text {* One- and two-sided intervals *}
   17.58  
   17.59  lemma ivl_disj_int_one:
   17.60 @@ -742,7 +763,7 @@
   17.61    "{l..m} Int {m<..u} = {}"
   17.62    by auto
   17.63  
   17.64 -lemmas ivl_disj_int = ivl_disj_int_singleton ivl_disj_int_one ivl_disj_int_two
   17.65 +lemmas ivl_disj_int = ivl_disj_int_one ivl_disj_int_two
   17.66  
   17.67  subsubsection {* Some Differences *}
   17.68  
    18.1 --- a/src/HOL/UNITY/Simple/Common.thy	Sat Aug 29 14:31:39 2009 +0200
    18.2 +++ b/src/HOL/UNITY/Simple/Common.thy	Mon Aug 31 14:09:42 2009 +0200
    18.3 @@ -92,7 +92,7 @@
    18.4        ==> F \<in> (atMost n) LeadsTo common"
    18.5  apply (rule LeadsTo_weaken_R)
    18.6  apply (rule_tac f = id and l = n in GreaterThan_bounded_induct)
    18.7 -apply (simp_all (no_asm_simp))
    18.8 +apply (simp_all (no_asm_simp) del: Int_insert_right_if1)
    18.9  apply (rule_tac [2] subset_refl)
   18.10  apply (blast dest: PSP_Stable2 intro: common_stable LeadsTo_weaken_R)
   18.11  done