--- a/src/HOL/Algebra/Divisibility.thy Mon Aug 31 12:22:15 2009 +0200
+++ b/src/HOL/Algebra/Divisibility.thy Mon Aug 31 14:10:11 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)
--- a/src/HOL/Algebra/UnivPoly.thy Mon Aug 31 12:22:15 2009 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy Mon Aug 31 14:10:11 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)
--- a/src/HOL/Algebra/poly/UnivPoly2.thy Mon Aug 31 12:22:15 2009 +0200
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy Mon Aug 31 14:10:11 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
--- a/src/HOL/Bali/Example.thy Mon Aug 31 12:22:15 2009 +0200
+++ b/src/HOL/Bali/Example.thy Mon Aug 31 14:10:11 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
--- a/src/HOL/Isar_examples/Mutilated_Checkerboard.thy Mon Aug 31 12:22:15 2009 +0200
+++ b/src/HOL/Isar_examples/Mutilated_Checkerboard.thy Mon Aug 31 14:10:11 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 *}
--- a/src/HOL/Library/Abstract_Rat.thy Mon Aug 31 12:22:15 2009 +0200
+++ b/src/HOL/Library/Abstract_Rat.thy Mon Aug 31 14:10:11 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"
--- a/src/HOL/Library/Continuity.thy Mon Aug 31 12:22:15 2009 +0200
+++ b/src/HOL/Library/Continuity.thy Mon Aug 31 14:10:11 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
--- a/src/HOL/Library/Convex_Euclidean_Space.thy Mon Aug 31 12:22:15 2009 +0200
+++ b/src/HOL/Library/Convex_Euclidean_Space.thy Mon Aug 31 14:10:11 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
--- a/src/HOL/Library/Euclidean_Space.thy Mon Aug 31 12:22:15 2009 +0200
+++ b/src/HOL/Library/Euclidean_Space.thy Mon Aug 31 14:10:11 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"
--- a/src/HOL/Library/Formal_Power_Series.thy Mon Aug 31 12:22:15 2009 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Mon Aug 31 14:10:11 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}"
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Mon Aug 31 12:22:15 2009 +0200
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Mon Aug 31 14:10:11 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-
--- a/src/HOL/Library/Permutations.thy Mon Aug 31 12:22:15 2009 +0200
+++ b/src/HOL/Library/Permutations.thy Mon Aug 31 14:10:11 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)
--- a/src/HOL/Library/Univ_Poly.thy Mon Aug 31 12:22:15 2009 +0200
+++ b/src/HOL/Library/Univ_Poly.thy Mon Aug 31 14:10:11 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)
--- a/src/HOL/Library/Word.thy Mon Aug 31 12:22:15 2009 +0200
+++ b/src/HOL/Library/Word.thy Mon Aug 31 14:10:11 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)"
--- a/src/HOL/Nat.thy Mon Aug 31 12:22:15 2009 +0200
+++ b/src/HOL/Nat.thy Mon Aug 31 14:10:11 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,
--- a/src/HOL/Set.thy Mon Aug 31 12:22:15 2009 +0200
+++ b/src/HOL/Set.thy Mon Aug 31 14:10:11 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
--- a/src/HOL/SetInterval.thy Mon Aug 31 12:22:15 2009 +0200
+++ b/src/HOL/SetInterval.thy Mon Aug 31 14:10:11 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 *}
--- a/src/HOL/UNITY/Simple/Common.thy Mon Aug 31 12:22:15 2009 +0200
+++ b/src/HOL/UNITY/Simple/Common.thy Mon Aug 31 14:10:11 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