# HG changeset patch
# User nipkow
# Date 1251720582 -7200
# Node ID 341c83339aebd6fd411dac0b13c94f77d92ba89a
# Parent  375db037f4d26660a8b8ec9a78586b34b83c3613
tuned the simp rules for Int involving insert and intervals.

diff -r 375db037f4d2 -r 341c83339aeb src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Sat Aug 29 14:31:39 2009 +0200
+++ b/src/HOL/Algebra/Divisibility.thy	Mon Aug 31 14:09:42 2009 +0200
@@ -2656,25 +2656,7 @@
   shows "(x \<in> carrier G \<and> x gcdof a b) =
          greatest (division_rel G) x (Lower (division_rel G) {a, b})"
 unfolding isgcd_def greatest_def Lower_def elem_def
-proof (simp, safe)
-  fix xa
-  assume r1[rule_format]: "\<forall>x. (x = a \<or> x = b) \<and> x \<in> carrier G \<longrightarrow> xa divides x"
-  assume r2[rule_format]: "\<forall>y\<in>carrier G. y divides a \<and> y divides b \<longrightarrow> y divides x"
-
-  assume "xa \<in> carrier G"  "x divides a"  "x divides b"
-  with carr
-  show "xa divides x"
-      by (fast intro: r1 r2)
-next
-  fix a' y
-  assume r1[rule_format]:
-         "\<forall>xa\<in>{l. \<forall>x. (x = a \<or> x = b) \<and> x \<in> carrier G \<longrightarrow> l divides x} \<inter> carrier G.
-           xa divides x"
-  assume "y \<in> carrier G"  "y divides a"  "y divides b"
-  with carr
-       show "y divides x"
-       by (fast intro: r1)
-qed (simp, simp)
+by auto
 
 lemma lcmof_leastUpper:
   fixes G (structure)
@@ -2682,25 +2664,7 @@
   shows "(x \<in> carrier G \<and> x lcmof a b) =
          least (division_rel G) x (Upper (division_rel G) {a, b})"
 unfolding islcm_def least_def Upper_def elem_def
-proof (simp, safe)
-  fix xa
-  assume r1[rule_format]: "\<forall>x. (x = a \<or> x = b) \<and> x \<in> carrier G \<longrightarrow> x divides xa"
-  assume r2[rule_format]: "\<forall>y\<in>carrier G. a divides y \<and> b divides y \<longrightarrow> x divides y"
-
-  assume "xa \<in> carrier G"  "a divides x"  "b divides x"
-  with carr
-  show "x divides xa"
-      by (fast intro: r1 r2)
-next
-  fix a' y
-  assume r1[rule_format]:
-         "\<forall>xa\<in>{l. \<forall>x. (x = a \<or> x = b) \<and> x \<in> carrier G \<longrightarrow> x divides l} \<inter> carrier G.
-           x divides xa"
-  assume "y \<in> carrier G"  "a divides y"  "b divides y"
-  with carr
-       show "x divides y"
-       by (fast intro: r1)
-qed (simp, simp)
+by auto
 
 lemma somegcd_meet:
   fixes G (structure)
diff -r 375db037f4d2 -r 341c83339aeb src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Sat Aug 29 14:31:39 2009 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy	Mon Aug 31 14:09:42 2009 +0200
@@ -592,15 +592,14 @@
         proof (cases "n = k")
           case True
           then have "\<zero> = (\<Oplus>i \<in> {..<n} \<union> {n}. ?s i)"
-            by (simp cong: R.finsum_cong add: ivl_disj_int_singleton Pi_def)
+            by (simp cong: R.finsum_cong add: Pi_def)
           also from True have "... = (\<Oplus>i \<in> {..k}. ?s i)"
             by (simp only: ivl_disj_un_singleton)
           finally show ?thesis .
         next
           case False with n_le_k have n_less_k: "n < k" by arith
           with neq have "\<zero> = (\<Oplus>i \<in> {..<n} \<union> {n}. ?s i)"
-            by (simp add: R.finsum_Un_disjoint f1 f2
-              ivl_disj_int_singleton Pi_def del: Un_insert_right)
+            by (simp add: R.finsum_Un_disjoint f1 f2 Pi_def del: Un_insert_right)
           also have "... = (\<Oplus>i \<in> {..n}. ?s i)"
             by (simp only: ivl_disj_un_singleton)
           also from n_less_k neq have "... = (\<Oplus>i \<in> {..n} \<union> {n<..k}. ?s i)"
@@ -939,8 +938,7 @@
     also have "...= (\<Oplus>i \<in> {deg R p} \<union> {deg R p <.. deg R p + deg R q}. ?s i)"
       by (simp only: ivl_disj_un_singleton)
     also have "... = coeff P p (deg R p) \<otimes> coeff P q (deg R q)"
-      by (simp cong: R.finsum_cong
-	add: ivl_disj_int_singleton deg_aboveD R Pi_def)
+      by (simp cong: R.finsum_cong add: deg_aboveD R Pi_def)
     finally have "(\<Oplus>i \<in> {.. deg R p + deg R q}. ?s i)
       = coeff P p (deg R p) \<otimes> coeff P q (deg R q)" .
     with nz show "(\<Oplus>i \<in> {.. deg R p + deg R q}. ?s i) ~= \<zero>"
@@ -983,8 +981,7 @@
     have "... = coeff P (\<Oplus>\<^bsub>P\<^esub> i \<in> {..<k} \<union> {k}. ?s i) k"
       by (simp only: ivl_disj_un_singleton)
     also have "... = coeff P p k"
-      by (simp cong: R.finsum_cong
-	add: ivl_disj_int_singleton coeff_finsum deg_aboveD R RR Pi_def)
+      by (simp cong: R.finsum_cong add: coeff_finsum deg_aboveD R RR Pi_def)
     finally show ?thesis .
   next
     case False
@@ -992,8 +989,7 @@
           coeff P (\<Oplus>\<^bsub>P\<^esub> i \<in> {..<deg R p} \<union> {deg R p}. ?s i) k"
       by (simp only: ivl_disj_un_singleton)
     also from False have "... = coeff P p k"
-      by (simp cong: R.finsum_cong
-	add: ivl_disj_int_singleton coeff_finsum deg_aboveD R Pi_def)
+      by (simp cong: R.finsum_cong add: coeff_finsum deg_aboveD R Pi_def)
     finally show ?thesis .
   qed
 qed (simp_all add: R Pi_def)
diff -r 375db037f4d2 -r 341c83339aeb src/HOL/Algebra/poly/UnivPoly2.thy
--- a/src/HOL/Algebra/poly/UnivPoly2.thy	Sat Aug 29 14:31:39 2009 +0200
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Mon Aug 31 14:09:42 2009 +0200
@@ -674,8 +674,7 @@
     also have "... = setsum ?s ({deg p} Un {deg p <.. deg p + deg q})"
       by (simp only: ivl_disj_un_singleton)
     also have "... = coeff p (deg p) * coeff q (deg q)" 
-      by (simp add: setsum_Un_disjoint ivl_disj_int_singleton 
-        setsum_0 deg_aboveD)
+      by (simp add: setsum_Un_disjoint setsum_0 deg_aboveD)
     finally have "setsum ?s {.. deg p + deg q} 
       = coeff p (deg p) * coeff q (deg q)" .
     with nz show "setsum ?s {.. deg p + deg q} ~= 0"
@@ -719,8 +718,7 @@
     have "... = coeff (setsum ?s ({..<k} Un {k})) k"
       by (simp only: ivl_disj_un_singleton)
     also have "... = coeff p k"
-      by (simp add: setsum_Un_disjoint ivl_disj_int_singleton 
-        setsum_0 coeff_natsum deg_aboveD)
+      by (simp add: setsum_Un_disjoint setsum_0 coeff_natsum deg_aboveD)
     finally show ?thesis .
   next
     case False
@@ -728,8 +726,7 @@
           coeff (setsum ?s ({..<deg p} Un {deg p})) k"
       by (simp only: ivl_disj_un_singleton)
     also from False have "... = coeff p k"
-      by (simp add: setsum_Un_disjoint ivl_disj_int_singleton 
-        setsum_0 coeff_natsum deg_aboveD)
+      by (simp add: setsum_Un_disjoint setsum_0 coeff_natsum deg_aboveD)
     finally show ?thesis .
   qed
 qed
diff -r 375db037f4d2 -r 341c83339aeb src/HOL/Bali/Example.thy
--- a/src/HOL/Bali/Example.thy	Sat Aug 29 14:31:39 2009 +0200
+++ b/src/HOL/Bali/Example.thy	Mon Aug 31 14:09:42 2009 +0200
@@ -1167,7 +1167,6 @@
 apply    (simp,rule assigned.select_convs)
 apply   (simp)
 apply  simp
-apply  blast
 apply simp
 apply (simp add: intersect_ts_def)
 done
diff -r 375db037f4d2 -r 341c83339aeb src/HOL/Isar_examples/Mutilated_Checkerboard.thy
--- a/src/HOL/Isar_examples/Mutilated_Checkerboard.thy	Sat Aug 29 14:31:39 2009 +0200
+++ b/src/HOL/Isar_examples/Mutilated_Checkerboard.thy	Mon Aug 31 14:09:42 2009 +0200
@@ -113,7 +113,7 @@
 lemma evnodd_insert: "evnodd (insert (i, j) C) b =
     (if (i + j) mod 2 = b
       then insert (i, j) (evnodd C b) else evnodd C b)"
-  by (simp add: evnodd_def) blast
+  by (simp add: evnodd_def)
 
 
 subsection {* Dominoes *}
diff -r 375db037f4d2 -r 341c83339aeb src/HOL/Library/Abstract_Rat.thy
--- a/src/HOL/Library/Abstract_Rat.thy	Sat Aug 29 14:31:39 2009 +0200
+++ b/src/HOL/Library/Abstract_Rat.thy	Mon Aug 31 14:09:42 2009 +0200
@@ -189,14 +189,9 @@
   have "\<exists> a b a' b'. x = (a,b) \<and> y = (a',b')" by auto
   then obtain a b a' b' where xy[simp]: "x = (a,b)" "y=(a',b')" by blast
   assume H: ?lhs 
-  {assume "a = 0 \<or> b = 0 \<or> a' = 0 \<or> b' = 0" hence ?rhs
-      using na nb H
-      apply (simp add: INum_def split_def isnormNum_def)
-      apply (cases "a = 0", simp_all)
-      apply (cases "b = 0", simp_all)
-      apply (cases "a' = 0", simp_all)
-      apply (cases "a' = 0", simp_all add: of_int_eq_0_iff)
-      done}
+  {assume "a = 0 \<or> b = 0 \<or> a' = 0 \<or> b' = 0"
+    hence ?rhs using na nb H
+      by (simp add: INum_def split_def isnormNum_def split: split_if_asm)}
   moreover
   { assume az: "a \<noteq> 0" and bz: "b \<noteq> 0" and a'z: "a'\<noteq>0" and b'z: "b'\<noteq>0"
     from az bz a'z b'z na nb have pos: "b > 0" "b' > 0" by (simp_all add: isnormNum_def)
@@ -517,10 +512,7 @@
     have n0: "isnormNum 0\<^sub>N" by simp
     show ?thesis using nx ny 
       apply (simp only: isnormNum_unique[where ?'a = 'a, OF  Nmul_normN[OF nx ny] n0, symmetric] Nmul[where ?'a = 'a])
-      apply (simp add: INum_def split_def isnormNum_def fst_conv snd_conv)
-      apply (cases "a=0",simp_all)
-      apply (cases "a'=0",simp_all)
-      done
+      by (simp add: INum_def split_def isnormNum_def fst_conv snd_conv split: split_if_asm)
   }
 qed
 lemma Nneg_Nneg[simp]: "~\<^sub>N (~\<^sub>N c) = c"
diff -r 375db037f4d2 -r 341c83339aeb src/HOL/Library/Continuity.thy
--- a/src/HOL/Library/Continuity.thy	Sat Aug 29 14:31:39 2009 +0200
+++ b/src/HOL/Library/Continuity.thy	Mon Aug 31 14:09:42 2009 +0200
@@ -156,7 +156,7 @@
  apply (rule up_chainI)
  apply simp
 apply (drule Un_absorb1)
-apply (auto simp add: nat_not_singleton)
+apply (auto split:split_if_asm)
 done
 
 
@@ -184,8 +184,7 @@
  apply (rule down_chainI)
  apply simp
 apply (drule Int_absorb1)
-apply auto
-apply (auto simp add: nat_not_singleton)
+apply (auto split:split_if_asm)
 done
 
 
diff -r 375db037f4d2 -r 341c83339aeb src/HOL/Library/Convex_Euclidean_Space.thy
--- a/src/HOL/Library/Convex_Euclidean_Space.thy	Sat Aug 29 14:31:39 2009 +0200
+++ b/src/HOL/Library/Convex_Euclidean_Space.thy	Mon Aug 31 14:09:42 2009 +0200
@@ -3355,9 +3355,8 @@
   qed(auto intro!:path_connected_singleton) next
   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)
     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)
-  have ***:"\<And>xa. (if xa = 0 then 0 else 1) \<noteq> 1 \<Longrightarrow> xa = 0" apply(rule ccontr) by auto
   have **:"{x::real^'n. norm x = 1} = (\<lambda>x. (1/norm x) *\<^sub>R x) ` (UNIV - {0})" apply(rule set_ext,rule)
-    unfolding image_iff apply(rule_tac x=x in bexI) unfolding mem_Collect_eq by(auto intro!: ***)
+    unfolding image_iff apply(rule_tac x=x in bexI) unfolding mem_Collect_eq by(auto split:split_if_asm)
   have "continuous_on (UNIV - {0}) (\<lambda>x::real^'n. 1 / norm x)" unfolding o_def continuous_on_eq_continuous_within
     apply(rule, rule continuous_at_within_inv[unfolded o_def inverse_eq_divide]) apply(rule continuous_at_within)
     apply(rule continuous_at_norm[unfolded o_def]) by auto
diff -r 375db037f4d2 -r 341c83339aeb src/HOL/Library/Euclidean_Space.thy
--- a/src/HOL/Library/Euclidean_Space.thy	Sat Aug 29 14:31:39 2009 +0200
+++ b/src/HOL/Library/Euclidean_Space.thy	Mon Aug 31 14:09:42 2009 +0200
@@ -1055,28 +1055,6 @@
 lemma norm_triangle_lt: "norm(x::real ^'n::finite) + norm(y) < e ==> norm(x + y) < e"
   by (metis basic_trans_rules(21) norm_triangle_ineq)
 
-lemma setsum_delta:
-  assumes fS: "finite S"
-  shows "setsum (\<lambda>k. if k=a then b k else 0) S = (if a \<in> S then b a else 0)"
-proof-
-  let ?f = "(\<lambda>k. if k=a then b k else 0)"
-  {assume a: "a \<notin> S"
-    hence "\<forall> k\<in> S. ?f k = 0" by simp
-    hence ?thesis  using a by simp}
-  moreover
-  {assume a: "a \<in> S"
-    let ?A = "S - {a}"
-    let ?B = "{a}"
-    have eq: "S = ?A \<union> ?B" using a by blast
-    have dj: "?A \<inter> ?B = {}" by simp
-    from fS have fAB: "finite ?A" "finite ?B" by auto
-    have "setsum ?f S = setsum ?f ?A + setsum ?f ?B"
-      using setsum_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
-      by simp
-    then have ?thesis  using a by simp}
-  ultimately show ?thesis by blast
-qed
-
 lemma component_le_norm: "\<bar>x$i\<bar> <= norm (x::real ^ 'n::finite)"
   apply (simp add: norm_vector_def)
   apply (rule member_le_setL2, simp_all)
@@ -2079,13 +2057,6 @@
 lemma matrix_add_ldistrib: "(A ** (B + C)) = (A \<star> B) + (A \<star> C)"
   by (vector matrix_matrix_mult_def setsum_addf[symmetric] ring_simps)
 
-lemma setsum_delta':
-  assumes fS: "finite S" shows
-  "setsum (\<lambda>k. if a = k then b k else 0) S =
-     (if a\<in> S then b a else 0)"
-  using setsum_delta[OF fS, of a b, symmetric]
-  by (auto intro: setsum_cong)
-
 lemma matrix_mul_lid:
   fixes A :: "'a::semiring_1 ^ 'm ^ 'n::finite"
   shows "mat 1 ** A = A"
diff -r 375db037f4d2 -r 341c83339aeb src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Sat Aug 29 14:31:39 2009 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy	Mon Aug 31 14:09:42 2009 +0200
@@ -633,8 +633,7 @@
 	    by (auto simp add: inverse_eq_divide power_divide)
 
 	  from k have kn: "k > n"
-	    apply (simp add: leastP_def setge_def fps_sum_rep_nth)
-	    by (cases "k \<le> n", auto)
+	    by (simp add: leastP_def setge_def fps_sum_rep_nth split:split_if_asm)
 	  then have "dist (?s n) a < (1/2)^n" unfolding dth
 	    by (auto intro: power_strict_decreasing)
 	  also have "\<dots> <= (1/2)^n0" using nn0
@@ -1244,10 +1243,9 @@
     {assume n0: "n \<noteq> 0"
       then have u: "{0} \<union> ({1} \<union> {2..n}) = {0..n}" "{1}\<union>{2..n} = {1..n}"
 	"{0..n - 1}\<union>{n} = {0..n}"
-	apply (simp_all add: expand_set_eq) by presburger+
+	by (auto simp: expand_set_eq)
       have d: "{0} \<inter> ({1} \<union> {2..n}) = {}" "{1} \<inter> {2..n} = {}"
-	"{0..n - 1}\<inter>{n} ={}" using n0
-	by (simp_all add: expand_set_eq, presburger+)
+	"{0..n - 1}\<inter>{n} ={}" using n0 by simp_all
       have f: "finite {0}" "finite {1}" "finite {2 .. n}"
 	"finite {0 .. n - 1}" "finite {n}" by simp_all
     have "((1 - ?X) * ?sa) $ n = setsum (\<lambda>i. (1 - ?X)$ i * ?sa $ (n - i)) {0 .. n}"
diff -r 375db037f4d2 -r 341c83339aeb src/HOL/Library/Fundamental_Theorem_Algebra.thy
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sat Aug 29 14:31:39 2009 +0200
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Mon Aug 31 14:09:42 2009 +0200
@@ -577,11 +577,12 @@
 next
   case (pCons c cs)
   {assume c0: "c = 0"
-    from pCons.hyps pCons.prems c0 have ?case apply auto
+    from pCons.hyps pCons.prems c0 have ?case
+      apply (auto)
       apply (rule_tac x="k+1" in exI)
       apply (rule_tac x="a" in exI, clarsimp)
       apply (rule_tac x="q" in exI)
-      by (auto simp add: power_Suc)}
+      by (auto)}
   moreover
   {assume c0: "c\<noteq>0"
     hence ?case apply-
diff -r 375db037f4d2 -r 341c83339aeb src/HOL/Library/Permutations.thy
--- a/src/HOL/Library/Permutations.thy	Sat Aug 29 14:31:39 2009 +0200
+++ b/src/HOL/Library/Permutations.thy	Mon Aug 31 14:09:42 2009 +0200
@@ -843,9 +843,7 @@
 	unfolding permutes_def by metis+
       from eq have "(Fun.swap a b id o p) a  = (Fun.swap a c id o q) a" by simp
       hence bc: "b = c"
-	apply (simp add: permutes_def pa qa o_def fun_upd_def swap_def id_def cong del: if_weak_cong)
-	apply (cases "a = b", auto)
-	by (cases "b = c", auto)
+	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)
       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
       hence "p = q" unfolding o_assoc swap_id_idempotent
 	by (simp add: o_def)
diff -r 375db037f4d2 -r 341c83339aeb src/HOL/Library/Univ_Poly.thy
--- a/src/HOL/Library/Univ_Poly.thy	Sat Aug 29 14:31:39 2009 +0200
+++ b/src/HOL/Library/Univ_Poly.thy	Mon Aug 31 14:09:42 2009 +0200
@@ -820,37 +820,24 @@
     done
 qed
 
-lemma (in semiring_0) pnormalize_sing: "(pnormalize [x] = [x]) \<longleftrightarrow> x \<noteq> 0" by simp
+lemma (in semiring_0) pnormalize_sing: "(pnormalize [x] = [x]) \<longleftrightarrow> x \<noteq> 0"
+by simp
 lemma (in semiring_0) pnormalize_pair: "y \<noteq> 0 \<longleftrightarrow> (pnormalize [x, y] = [x, y])" by simp
 lemma (in semiring_0) pnormal_cons: "pnormal p \<Longrightarrow> pnormal (c#p)"
   unfolding pnormal_def by simp
 lemma (in semiring_0) pnormal_tail: "p\<noteq>[] \<Longrightarrow> pnormal (c#p) \<Longrightarrow> pnormal p"
-  unfolding pnormal_def
-  apply (cases "pnormalize p = []", auto)
-  by (cases "c = 0", auto)
+  unfolding pnormal_def by(auto split: split_if_asm)
 
 
 lemma (in semiring_0) pnormal_last_nonzero: "pnormal p ==> last p \<noteq> 0"
-proof(induct p)
-  case Nil thus ?case by (simp add: pnormal_def)
-next
-  case (Cons a as) thus ?case
-    apply (simp add: pnormal_def)
-    apply (cases "pnormalize as = []", simp_all)
-    apply (cases "as = []", simp_all)
-    apply (cases "a=0", simp_all)
-    apply (cases "a=0", simp_all)
-    done
-qed
+by(induct p) (simp_all add: pnormal_def split: split_if_asm)
 
 lemma (in semiring_0) pnormal_length: "pnormal p \<Longrightarrow> 0 < length p"
   unfolding pnormal_def length_greater_0_conv by blast
 
 lemma (in semiring_0) pnormal_last_length: "\<lbrakk>0 < length p ; last p \<noteq> 0\<rbrakk> \<Longrightarrow> pnormal p"
-  apply (induct p, auto)
-  apply (case_tac "p = []", auto)
-  apply (simp add: pnormal_def)
-  by (rule pnormal_cons, auto)
+by (induct p) (auto simp: pnormal_def  split: split_if_asm)
+
 
 lemma (in semiring_0) pnormal_id: "pnormal p \<longleftrightarrow> (0 < length p \<and> last p \<noteq> 0)"
   using pnormal_last_length pnormal_length pnormal_last_nonzero by blast
@@ -918,9 +905,7 @@
 qed
 
 lemma (in semiring_0) pnormalize_eq: "last p \<noteq> 0 \<Longrightarrow> pnormalize p = p"
-  apply (induct p, auto)
-  apply (case_tac p, auto)+
-  done
+by (induct p) (auto split: split_if_asm)
 
 lemma (in semiring_0) last_pnormalize: "pnormalize p \<noteq> [] \<Longrightarrow> last (pnormalize p) \<noteq> 0"
   by (induct p, auto)
diff -r 375db037f4d2 -r 341c83339aeb src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Sat Aug 29 14:31:39 2009 +0200
+++ b/src/HOL/Library/Word.thy	Mon Aug 31 14:09:42 2009 +0200
@@ -1008,12 +1008,7 @@
   fix xs
   assume "length (norm_signed (\<zero>#xs)) = Suc (length xs)"
   thus "norm_signed (\<zero>#xs) = \<zero>#xs"
-    apply (simp add: norm_signed_Cons)
-    apply safe
-    apply simp_all
-    apply (rule norm_unsigned_equal)
-    apply assumption
-    done
+    by (simp add: norm_signed_Cons norm_unsigned_equal split: split_if_asm)
 next
   fix xs
   assume "length (norm_signed (\<one>#xs)) = Suc (length xs)"
diff -r 375db037f4d2 -r 341c83339aeb src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sat Aug 29 14:31:39 2009 +0200
+++ b/src/HOL/Nat.thy	Mon Aug 31 14:09:42 2009 +0200
@@ -1588,9 +1588,6 @@
 lemma zero_induct: "P k ==> (!!n. P (Suc n) ==> P n) ==> P 0"
   using inc_induct[of 0 k P] by blast
 
-lemma nat_not_singleton: "(\<forall>x. x = (0::nat)) = False"
-  by auto
-
 (*The others are
       i - j - k = i - (j + k),
       k \<le> j ==> j - k + i = j + i - k,
diff -r 375db037f4d2 -r 341c83339aeb src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sat Aug 29 14:31:39 2009 +0200
+++ b/src/HOL/Set.thy	Mon Aug 31 14:09:42 2009 +0200
@@ -1268,10 +1268,26 @@
     "(insert a B) Int C = (if a \<in> C then insert a (B \<inter> C) else B \<inter> C)"
   by auto
 
+lemma Int_insert_left_if0[simp]:
+    "a \<notin> C \<Longrightarrow> (insert a B) Int C = B \<inter> C"
+  by auto
+
+lemma Int_insert_left_if1[simp]:
+    "a \<in> C \<Longrightarrow> (insert a B) Int C = insert a (B Int C)"
+  by auto
+
 lemma Int_insert_right:
     "A \<inter> (insert a B) = (if a \<in> A then insert a (A \<inter> B) else A \<inter> B)"
   by auto
 
+lemma Int_insert_right_if0[simp]:
+    "a \<notin> A \<Longrightarrow> A Int (insert a B) = A Int B"
+  by auto
+
+lemma Int_insert_right_if1[simp]:
+    "a \<in> A \<Longrightarrow> A Int (insert a B) = insert a (A Int B)"
+  by auto
+
 lemma Un_Int_distrib: "A \<union> (B \<inter> C) = (A \<union> B) \<inter> (A \<union> C)"
   by blast
 
diff -r 375db037f4d2 -r 341c83339aeb src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Sat Aug 29 14:31:39 2009 +0200
+++ b/src/HOL/SetInterval.thy	Mon Aug 31 14:09:42 2009 +0200
@@ -251,6 +251,38 @@
 apply (simp add: less_imp_le)
 done
 
+subsubsection {* Intersection *}
+
+context linorder
+begin
+
+lemma Int_atLeastAtMost[simp]: "{a..b} Int {c..d} = {max a c .. min b d}"
+by auto
+
+lemma Int_atLeastAtMostR1[simp]: "{..b} Int {c..d} = {c .. min b d}"
+by auto
+
+lemma Int_atLeastAtMostR2[simp]: "{a..} Int {c..d} = {max a c .. d}"
+by auto
+
+lemma Int_atLeastAtMostL1[simp]: "{a..b} Int {..d} = {a .. min b d}"
+by auto
+
+lemma Int_atLeastAtMostL2[simp]: "{a..b} Int {c..} = {max a c .. b}"
+by auto
+
+lemma Int_atLeastLessThan[simp]: "{a..<b} Int {c..<d} = {max a c ..< min b d}"
+by auto
+
+lemma Int_greaterThanAtMost[simp]: "{a<..b} Int {c<..d} = {max a c <.. min b d}"
+by auto
+
+lemma Int_greaterThanLessThan[simp]: "{a<..<b} Int {c<..<d} = {max a c <..< min b d}"
+by auto
+
+end
+
+
 subsection {* Intervals of natural numbers *}
 
 subsubsection {* The Constant @{term lessThan} *}
@@ -705,17 +737,6 @@
 
 subsubsection {* Disjoint Intersections *}
 
-text {* Singletons and open intervals *}
-
-lemma ivl_disj_int_singleton:
-  "{l::'a::order} Int {l<..} = {}"
-  "{..<u} Int {u} = {}"
-  "{l} Int {l<..<u} = {}"
-  "{l<..<u} Int {u} = {}"
-  "{l} Int {l<..u} = {}"
-  "{l..<u} Int {u} = {}"
-  by simp+
-
 text {* One- and two-sided intervals *}
 
 lemma ivl_disj_int_one:
@@ -742,7 +763,7 @@
   "{l..m} Int {m<..u} = {}"
   by auto
 
-lemmas ivl_disj_int = ivl_disj_int_singleton ivl_disj_int_one ivl_disj_int_two
+lemmas ivl_disj_int = ivl_disj_int_one ivl_disj_int_two
 
 subsubsection {* Some Differences *}
 
diff -r 375db037f4d2 -r 341c83339aeb src/HOL/UNITY/Simple/Common.thy
--- a/src/HOL/UNITY/Simple/Common.thy	Sat Aug 29 14:31:39 2009 +0200
+++ b/src/HOL/UNITY/Simple/Common.thy	Mon Aug 31 14:09:42 2009 +0200
@@ -92,7 +92,7 @@
       ==> F \<in> (atMost n) LeadsTo common"
 apply (rule LeadsTo_weaken_R)
 apply (rule_tac f = id and l = n in GreaterThan_bounded_induct)
-apply (simp_all (no_asm_simp))
+apply (simp_all (no_asm_simp) del: Int_insert_right_if1)
 apply (rule_tac [2] subset_refl)
 apply (blast dest: PSP_Stable2 intro: common_stable LeadsTo_weaken_R)
 done