Moved to new m<..<n syntax for set intervals.
--- a/src/HOL/Algebra/UnivPoly.thy Thu Jul 15 08:38:37 2004 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy Thu Jul 15 13:11:34 2004 +0200
@@ -646,13 +646,13 @@
"!!i. [| n < i; i <= n + m |] ==> n + m - i < m" by arith
from True have "coeff P (monom P \<one> (Suc n)) k = \<one>" by simp
also from True
- have "... = (\<Oplus>i \<in> {..n(} \<union> {n}. coeff P (monom P \<one> n) i \<otimes>
+ have "... = (\<Oplus>i \<in> {..<n} \<union> {n}. coeff P (monom P \<one> n) i \<otimes>
coeff P (monom P \<one> 1) (k - i))"
by (simp cong: finsum_cong add: finsum_Un_disjoint Pi_def)
also have "... = (\<Oplus>i \<in> {..n}. coeff P (monom P \<one> n) i \<otimes>
coeff P (monom P \<one> 1) (k - i))"
by (simp only: ivl_disj_un_singleton)
- also from True have "... = (\<Oplus>i \<in> {..n} \<union> {)n..k}. coeff P (monom P \<one> n) i \<otimes>
+ also from True have "... = (\<Oplus>i \<in> {..n} \<union> {n<..k}. coeff P (monom P \<one> n) i \<otimes>
coeff P (monom P \<one> 1) (k - i))"
by (simp cong: finsum_cong add: finsum_Un_disjoint ivl_disj_int_one
order_less_imp_not_eq Pi_def)
@@ -668,10 +668,10 @@
from neq have "coeff P (monom P \<one> (Suc n)) k = \<zero>" by simp
also have "... = (\<Oplus>i \<in> {..k}. ?s i)"
proof -
- have f1: "(\<Oplus>i \<in> {..n(}. ?s i) = \<zero>" by (simp cong: finsum_cong add: Pi_def)
+ have f1: "(\<Oplus>i \<in> {..<n}. ?s i) = \<zero>" by (simp cong: finsum_cong add: Pi_def)
from neq have f2: "(\<Oplus>i \<in> {n}. ?s i) = \<zero>"
by (simp cong: finsum_cong add: Pi_def) arith
- have f3: "n < k ==> (\<Oplus>i \<in> {)n..k}. ?s i) = \<zero>"
+ have f3: "n < k ==> (\<Oplus>i \<in> {n<..k}. ?s i) = \<zero>"
by (simp cong: finsum_cong add: order_less_imp_not_eq Pi_def)
show ?thesis
proof (cases "k < n")
@@ -681,7 +681,7 @@
show ?thesis
proof (cases "n = k")
case True
- then have "\<zero> = (\<Oplus>i \<in> {..n(} \<union> {n}. ?s i)"
+ then have "\<zero> = (\<Oplus>i \<in> {..<n} \<union> {n}. ?s i)"
by (simp cong: finsum_cong add: finsum_Un_disjoint
ivl_disj_int_singleton Pi_def)
also from True have "... = (\<Oplus>i \<in> {..k}. ?s i)"
@@ -689,12 +689,12 @@
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)"
+ with neq have "\<zero> = (\<Oplus>i \<in> {..<n} \<union> {n}. ?s i)"
by (simp add: finsum_Un_disjoint f1 f2
ivl_disj_int_singleton 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)"
+ also from n_less_k neq have "... = (\<Oplus>i \<in> {..n} \<union> {n<..k}. ?s i)"
by (simp add: finsum_Un_disjoint f3 ivl_disj_int_one Pi_def)
also from n_less_k have "... = (\<Oplus>i \<in> {..k}. ?s i)"
by (simp only: ivl_disj_un_one)
@@ -976,12 +976,12 @@
show "deg R p + deg R q <= deg R (p \<otimes>\<^sub>2 q)"
proof (rule deg_belowI, simp add: R)
have "finsum R ?s {.. deg R p + deg R q}
- = finsum R ?s ({.. deg R p(} Un {deg R p .. deg R p + deg R q})"
+ = finsum R ?s ({..< deg R p} Un {deg R p .. deg R p + deg R q})"
by (simp only: ivl_disj_un_one)
also have "... = finsum R ?s {deg R p .. deg R p + deg R q}"
by (simp cong: finsum_cong add: finsum_Un_disjoint ivl_disj_int_one
deg_aboveD less_add_diff R Pi_def)
- also have "...= finsum R ?s ({deg R p} Un {)deg R p .. deg R p + deg R q})"
+ also have "...= finsum R ?s ({deg R p} Un {deg R p <.. deg R p + deg R q})"
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: finsum_cong add: finsum_Un_disjoint
@@ -1015,14 +1015,14 @@
proof (cases "k <= deg R p")
case True
hence "coeff P (finsum P ?s {..deg R p}) k =
- coeff P (finsum P ?s ({..k} Un {)k..deg R p})) k"
+ coeff P (finsum P ?s ({..k} Un {k<..deg R p})) k"
by (simp only: ivl_disj_un_one)
also from True
have "... = coeff P (finsum P ?s {..k}) k"
by (simp cong: finsum_cong add: finsum_Un_disjoint
ivl_disj_int_one order_less_imp_not_eq2 coeff_finsum R RR Pi_def)
also
- have "... = coeff P (finsum P ?s ({..k(} Un {k})) k"
+ have "... = coeff P (finsum P ?s ({..<k} Un {k})) k"
by (simp only: ivl_disj_un_singleton)
also have "... = coeff P p k"
by (simp cong: finsum_cong add: setsum_Un_disjoint
@@ -1031,7 +1031,7 @@
next
case False
hence "coeff P (finsum P ?s {..deg R p}) k =
- coeff P (finsum P ?s ({..deg R p(} Un {deg R p})) k"
+ coeff P (finsum P ?s ({..<deg R p} Un {deg R p})) k"
by (simp only: ivl_disj_un_singleton)
also from False have "... = coeff P p k"
by (simp cong: finsum_cong add: setsum_Un_disjoint ivl_disj_int_singleton
@@ -1046,7 +1046,7 @@
proof -
let ?s = "(%i. monom P (coeff P p i) i)"
assume R: "p \<in> carrier P" and "deg R p <= n"
- then have "finsum P ?s {..n} = finsum P ?s ({..deg R p} Un {)deg R p..n})"
+ then have "finsum P ?s {..n} = finsum P ?s ({..deg R p} Un {deg R p<..n})"
by (simp only: ivl_disj_un_one)
also have "... = finsum P ?s {..deg R p}"
by (simp cong: UP_finsum_cong add: UP_finsum_Un_disjoint ivl_disj_int_one
@@ -1206,12 +1206,12 @@
from f g have "(\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k - i)) =
(\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..n + m - k}. f k \<otimes> g i)"
by (simp add: diagonal_sum Pi_def)
- also have "... = (\<Oplus>k \<in> {..n} \<union> {)n..n + m}. \<Oplus>i \<in> {..n + m - k}. f k \<otimes> g i)"
+ also have "... = (\<Oplus>k \<in> {..n} \<union> {n<..n + m}. \<Oplus>i \<in> {..n + m - k}. f k \<otimes> g i)"
by (simp only: ivl_disj_un_one)
also from f g have "... = (\<Oplus>k \<in> {..n}. \<Oplus>i \<in> {..n + m - k}. f k \<otimes> g i)"
by (simp cong: finsum_cong
add: bound.bound [OF bf] finsum_Un_disjoint ivl_disj_int_one Pi_def)
- also from f g have "... = (\<Oplus>k \<in> {..n}. \<Oplus>i \<in> {..m} \<union> {)m..n + m - k}. f k \<otimes> g i)"
+ also from f g have "... = (\<Oplus>k \<in> {..n}. \<Oplus>i \<in> {..m} \<union> {m<..n + m - k}. f k \<otimes> g i)"
by (simp cong: finsum_cong add: ivl_disj_un_one le_add_diff Pi_def)
also from f g have "... = (\<Oplus>k \<in> {..n}. \<Oplus>i \<in> {..m}. f k \<otimes> g i)"
by (simp cong: finsum_cong
@@ -1262,7 +1262,7 @@
proof (simp only: eval_on_carrier UP_mult_closed)
from RS have
"(\<Oplus>\<^sub>2 i \<in> {..deg R (p \<otimes>\<^sub>3 q)}. h (coeff P (p \<otimes>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) =
- (\<Oplus>\<^sub>2 i \<in> {..deg R (p \<otimes>\<^sub>3 q)} \<union> {)deg R (p \<otimes>\<^sub>3 q)..deg R p + deg R q}.
+ (\<Oplus>\<^sub>2 i \<in> {..deg R (p \<otimes>\<^sub>3 q)} \<union> {deg R (p \<otimes>\<^sub>3 q)<..deg R p + deg R q}.
h (coeff P (p \<otimes>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
by (simp cong: finsum_cong
add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def
@@ -1292,7 +1292,7 @@
proof (simp only: eval_on_carrier UP_a_closed)
from RS have
"(\<Oplus>\<^sub>2i \<in> {..deg R (p \<oplus>\<^sub>3 q)}. h (coeff P (p \<oplus>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) =
- (\<Oplus>\<^sub>2i \<in> {..deg R (p \<oplus>\<^sub>3 q)} \<union> {)deg R (p \<oplus>\<^sub>3 q)..max (deg R p) (deg R q)}.
+ (\<Oplus>\<^sub>2i \<in> {..deg R (p \<oplus>\<^sub>3 q)} \<union> {deg R (p \<oplus>\<^sub>3 q)<..max (deg R p) (deg R q)}.
h (coeff P (p \<oplus>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
by (simp cong: finsum_cong
add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def
@@ -1306,9 +1306,9 @@
by (simp cong: finsum_cong
add: l_distr deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def)
also have "... =
- (\<Oplus>\<^sub>2 i \<in> {..deg R p} \<union> {)deg R p..max (deg R p) (deg R q)}.
+ (\<Oplus>\<^sub>2 i \<in> {..deg R p} \<union> {deg R p<..max (deg R p) (deg R q)}.
h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) \<oplus>\<^sub>2
- (\<Oplus>\<^sub>2 i \<in> {..deg R q} \<union> {)deg R q..max (deg R p) (deg R q)}.
+ (\<Oplus>\<^sub>2 i \<in> {..deg R q} \<union> {deg R q<..max (deg R p) (deg R q)}.
h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
by (simp only: ivl_disj_un_one le_maxI1 le_maxI2)
also from RS have "... =
@@ -1392,7 +1392,7 @@
assume S: "s \<in> carrier S"
then have
"(\<Oplus>\<^sub>2 i \<in> {..deg R (monom P \<one> 1)}. h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) =
- (\<Oplus>\<^sub>2i\<in>{..deg R (monom P \<one> 1)} \<union> {)deg R (monom P \<one> 1)..1}.
+ (\<Oplus>\<^sub>2i\<in>{..deg R (monom P \<one> 1)} \<union> {deg R (monom P \<one> 1)<..1}.
h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
by (simp cong: finsum_cong del: coeff_monom
add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def)
--- a/src/HOL/Algebra/poly/UnivPoly2.thy Thu Jul 15 08:38:37 2004 +0200
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy Thu Jul 15 13:11:34 2004 +0200
@@ -643,12 +643,12 @@
show "deg p + deg q <= deg (p * q)"
proof (rule deg_belowI, simp)
have "setsum ?s {.. deg p + deg q}
- = setsum ?s ({.. deg p(} Un {deg p .. deg p + deg q})"
+ = setsum ?s ({..< deg p} Un {deg p .. deg p + deg q})"
by (simp only: ivl_disj_un_one)
also have "... = setsum ?s {deg p .. deg p + deg q}"
by (simp add: setsum_Un_disjoint ivl_disj_int_one
setsum_0 deg_aboveD less_add_diff)
- also have "... = setsum ?s ({deg p} Un {)deg p .. deg p + deg q})"
+ 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
@@ -686,14 +686,14 @@
proof (cases "k <= deg p")
case True
hence "coeff (setsum ?s {..deg p}) k =
- coeff (setsum ?s ({..k} Un {)k..deg p})) k"
+ coeff (setsum ?s ({..k} Un {k<..deg p})) k"
by (simp only: ivl_disj_un_one)
also from True
have "... = coeff (setsum ?s {..k}) k"
by (simp add: setsum_Un_disjoint ivl_disj_int_one order_less_imp_not_eq2
setsum_0 coeff_natsum )
also
- have "... = coeff (setsum ?s ({..k(} Un {k})) k"
+ 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
@@ -702,7 +702,7 @@
next
case False
hence "coeff (setsum ?s {..deg p}) k =
- coeff (setsum ?s ({..deg p(} Un {deg p})) k"
+ 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
@@ -716,7 +716,7 @@
proof -
let ?s = "(%i. monom (coeff p i) i)"
assume "deg p <= n"
- then have "setsum ?s {..n} = setsum ?s ({..deg p} Un {)deg p..n})"
+ then have "setsum ?s {..n} = setsum ?s ({..deg p} Un {deg p<..n})"
by (simp only: ivl_disj_un_one)
also have "... = setsum ?s {..deg p}"
by (simp add: setsum_Un_disjoint ivl_disj_int_one
--- a/src/HOL/HoareParallel/OG_Examples.thy Thu Jul 15 08:38:37 2004 +0200
+++ b/src/HOL/HoareParallel/OG_Examples.thy Thu Jul 15 13:11:34 2004 +0200
@@ -513,10 +513,10 @@
lemma Example2_lemma2:
"!!b. \<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow> Suc (\<Sum>i::nat< n. b i)=(\<Sum>i< n. (b (j := Suc 0)) i)"
apply(frule_tac b="(b (j:=(Suc 0)))" in Example2_lemma2_aux)
-apply(erule_tac t="setsum (b(j := (Suc 0))) {..n(}" in ssubst)
+apply(erule_tac t="setsum (b(j := (Suc 0))) {..<n}" in ssubst)
apply(frule_tac b=b in Example2_lemma2_aux)
-apply(erule_tac t="setsum b {..n(}" in ssubst)
-apply(subgoal_tac "Suc (setsum b {..j(} + b j + (\<Sum>i<n - Suc j. b (Suc j + i)))=(setsum b {..j(} + Suc (b j) + (\<Sum>i<n - Suc j. b (Suc j + i)))")
+apply(erule_tac t="setsum b {..<n}" in ssubst)
+apply(subgoal_tac "Suc (setsum b {..<j} + b j + (\<Sum>i<n - Suc j. b (Suc j + i)))=(setsum b {..<j} + Suc (b j) + (\<Sum>i<n - Suc j. b (Suc j + i)))")
apply(rotate_tac -1)
apply(erule ssubst)
apply(subgoal_tac "j\<le>j")
--- a/src/HOL/HoareParallel/RG_Examples.thy Thu Jul 15 08:38:37 2004 +0200
+++ b/src/HOL/HoareParallel/RG_Examples.thy Thu Jul 15 13:11:34 2004 +0200
@@ -212,10 +212,10 @@
lemma Example2_lemma2:
"!!b. \<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow> Suc (\<Sum>i::nat< n. b i)=(\<Sum>i< n. (b (j := Suc 0)) i)"
apply(frule_tac b="(b (j:=(Suc 0)))" in Example2_lemma2_aux)
-apply(erule_tac t="setsum (b(j := (Suc 0))) {..n(}" in ssubst)
+apply(erule_tac t="setsum (b(j := (Suc 0))) {..<n}" in ssubst)
apply(frule_tac b=b in Example2_lemma2_aux)
-apply(erule_tac t="setsum b {..n(}" in ssubst)
-apply(subgoal_tac "Suc (setsum b {..j(} + b j + (\<Sum>i<n - Suc j. b (Suc j + i)))=(setsum b {..j(} + Suc (b j) + (\<Sum>i<n - Suc j. b (Suc j + i)))")
+apply(erule_tac t="setsum b {..<n}" in ssubst)
+apply(subgoal_tac "Suc (setsum b {..<j} + b j + (\<Sum>i<n - Suc j. b (Suc j + i)))=(setsum b {..<j} + Suc (b j) + (\<Sum>i<n - Suc j. b (Suc j + i)))")
apply(rotate_tac -1)
apply(erule ssubst)
apply(subgoal_tac "j\<le>j")
--- a/src/HOL/Infinite_Set.thy Thu Jul 15 08:38:37 2004 +0200
+++ b/src/HOL/Infinite_Set.thy Thu Jul 15 13:11:34 2004 +0200
@@ -68,7 +68,7 @@
lemma finite_nat_bounded:
assumes S: "finite (S::nat set)"
- shows "\<exists>k. S \<subseteq> {..k(}" (is "\<exists>k. ?bounded S k")
+ shows "\<exists>k. S \<subseteq> {..<k}" (is "\<exists>k. ?bounded S k")
using S
proof (induct)
have "?bounded {} 0" by simp
@@ -89,13 +89,13 @@
qed
lemma finite_nat_iff_bounded:
- "finite (S::nat set) = (\<exists>k. S \<subseteq> {..k(})" (is "?lhs = ?rhs")
+ "finite (S::nat set) = (\<exists>k. S \<subseteq> {..<k})" (is "?lhs = ?rhs")
proof
assume ?lhs
thus ?rhs by (rule finite_nat_bounded)
next
assume ?rhs
- then obtain k where "S \<subseteq> {..k(}" ..
+ then obtain k where "S \<subseteq> {..<k}" ..
thus "finite S"
by (rule finite_subset, simp)
qed
@@ -104,7 +104,7 @@
"finite (S::nat set) = (\<exists>k. S \<subseteq> {..k})" (is "?lhs = ?rhs")
proof
assume ?lhs
- then obtain k where "S \<subseteq> {..k(}"
+ then obtain k where "S \<subseteq> {..<k}"
by (blast dest: finite_nat_bounded)
hence "S \<subseteq> {..k}" by auto
thus ?rhs ..
--- a/src/HOL/List.thy Thu Jul 15 08:38:37 2004 +0200
+++ b/src/HOL/List.thy Thu Jul 15 13:11:34 2004 +0200
@@ -1526,7 +1526,7 @@
lemma sublist_singleton [simp]: "sublist [x] A = (if 0 : A then [x] else [])"
by (simp add: sublist_Cons)
-lemma sublist_upt_eq_take [simp]: "sublist l {..n(} = take n l"
+lemma sublist_upt_eq_take [simp]: "sublist l {..<n} = take n l"
apply (induct l rule: rev_induct, simp)
apply (simp split: nat_diff_split add: sublist_append)
done
--- a/src/HOL/MicroJava/BV/BVExample.thy Thu Jul 15 08:38:37 2004 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy Thu Jul 15 13:11:34 2004 +0200
@@ -416,7 +416,7 @@
in kiljvm G mxs (1+size pTs+mxl) rT et instr start)"
lemma [code]:
- "unstables r step ss = (UN p:{..size ss(}. if \<not>stable r step ss p then {p} else {})"
+ "unstables r step ss = (UN p:{..<size ss}. if \<not>stable r step ss p then {p} else {})"
apply (unfold unstables_def)
apply (rule equalityI)
apply (rule subsetI)
--- a/src/HOL/SetInterval.thy Thu Jul 15 08:38:37 2004 +0200
+++ b/src/HOL/SetInterval.thy Thu Jul 15 13:11:34 2004 +0200
@@ -12,30 +12,44 @@
theory SetInterval = IntArith:
constdefs
- lessThan :: "('a::ord) => 'a set" ("(1{.._'(})")
- "{..u(} == {x. x<u}"
+ lessThan :: "('a::ord) => 'a set" ("(1{..<_})")
+ "{..<u} == {x. x<u}"
atMost :: "('a::ord) => 'a set" ("(1{.._})")
"{..u} == {x. x<=u}"
- greaterThan :: "('a::ord) => 'a set" ("(1{')_..})")
- "{)l..} == {x. l<x}"
+ greaterThan :: "('a::ord) => 'a set" ("(1{_<..})")
+ "{l<..} == {x. l<x}"
atLeast :: "('a::ord) => 'a set" ("(1{_..})")
"{l..} == {x. l<=x}"
- greaterThanLessThan :: "['a::ord, 'a] => 'a set" ("(1{')_.._'(})")
- "{)l..u(} == {)l..} Int {..u(}"
+ greaterThanLessThan :: "['a::ord, 'a] => 'a set" ("(1{_<..<_})")
+ "{l<..<u} == {l<..} Int {..<u}"
- atLeastLessThan :: "['a::ord, 'a] => 'a set" ("(1{_.._'(})")
- "{l..u(} == {l..} Int {..u(}"
+ atLeastLessThan :: "['a::ord, 'a] => 'a set" ("(1{_..<_})")
+ "{l..<u} == {l..} Int {..<u}"
- greaterThanAtMost :: "['a::ord, 'a] => 'a set" ("(1{')_.._})")
- "{)l..u} == {)l..} Int {..u}"
+ greaterThanAtMost :: "['a::ord, 'a] => 'a set" ("(1{_<.._})")
+ "{l<..u} == {l<..} Int {..u}"
atLeastAtMost :: "['a::ord, 'a] => 'a set" ("(1{_.._})")
"{l..u} == {l..} Int {..u}"
+(* Old syntax, will disappear! *)
+syntax
+ "_lessThan" :: "('a::ord) => 'a set" ("(1{.._'(})")
+ "_greaterThan" :: "('a::ord) => 'a set" ("(1{')_..})")
+ "_greaterThanLessThan" :: "['a::ord, 'a] => 'a set" ("(1{')_.._'(})")
+ "_atLeastLessThan" :: "['a::ord, 'a] => 'a set" ("(1{_.._'(})")
+ "_greaterThanAtMost" :: "['a::ord, 'a] => 'a set" ("(1{')_.._})")
+translations
+ "{..m(}" => "{..<m}"
+ "{)m..}" => "{m<..}"
+ "{)m..n(}" => "{m<..<n}"
+ "{m..n(}" => "{m..<n}"
+ "{)m..n}" => "{m<..n}"
+
syntax
"@UNION_le" :: "nat => nat => 'b set => 'b set" ("(3UN _<=_./ _)" 10)
"@UNION_less" :: "nat => nat => 'b set => 'b set" ("(3UN _<_./ _)" 10)
@@ -56,9 +70,9 @@
translations
"UN i<=n. A" == "UN i:{..n}. A"
- "UN i<n. A" == "UN i:{..n(}. A"
+ "UN i<n. A" == "UN i:{..<n}. A"
"INT i<=n. A" == "INT i:{..n}. A"
- "INT i<n. A" == "INT i:{..n(}. A"
+ "INT i<n. A" == "INT i:{..<n}. A"
subsection {* Various equivalences *}
@@ -150,19 +164,19 @@
text {* @{text greaterThanLessThan} *}
lemma greaterThanLessThan_iff [simp]:
- "(i : {)l..u(}) = (l < i & i < u)"
+ "(i : {l<..<u}) = (l < i & i < u)"
by (simp add: greaterThanLessThan_def)
text {* @{text atLeastLessThan} *}
lemma atLeastLessThan_iff [simp]:
- "(i : {l..u(}) = (l <= i & i < u)"
+ "(i : {l..<u}) = (l <= i & i < u)"
by (simp add: atLeastLessThan_def)
text {* @{text greaterThanAtMost} *}
lemma greaterThanAtMost_iff [simp]:
- "(i : {)l..u}) = (l < i & i <= u)"
+ "(i : {l<..u}) = (l < i & i <= u)"
by (simp add: greaterThanAtMost_def)
text {* @{text atLeastAtMost} *}
@@ -229,40 +243,40 @@
lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"
by blast
-lemma atLeast0LessThan [simp]: "{0::nat..n(} = {..n(}"
+lemma atLeast0LessThan [simp]: "{0::nat..<n} = {..<n}"
by(simp add:lessThan_def atLeastLessThan_def)
text {* Intervals of nats with @{text Suc} *}
-lemma atLeastLessThanSuc_atLeastAtMost: "{l..Suc u(} = {l..u}"
+lemma atLeastLessThanSuc_atLeastAtMost: "{l..<Suc u} = {l..u}"
by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def)
-lemma atLeastSucAtMost_greaterThanAtMost: "{Suc l..u} = {)l..u}"
+lemma atLeastSucAtMost_greaterThanAtMost: "{Suc l..u} = {l<..u}"
by (simp add: atLeast_Suc_greaterThan atLeastAtMost_def
greaterThanAtMost_def)
-lemma atLeastSucLessThan_greaterThanLessThan: "{Suc l..u(} = {)l..u(}"
+lemma atLeastSucLessThan_greaterThanLessThan: "{Suc l..<u} = {l<..<u}"
by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def
greaterThanLessThan_def)
subsubsection {* Finiteness *}
-lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..k(}"
+lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..<k}"
by (induct k) (simp_all add: lessThan_Suc)
lemma finite_atMost [iff]: fixes k :: nat shows "finite {..k}"
by (induct k) (simp_all add: atMost_Suc)
lemma finite_greaterThanLessThan [iff]:
- fixes l :: nat shows "finite {)l..u(}"
+ fixes l :: nat shows "finite {l<..<u}"
by (simp add: greaterThanLessThan_def)
lemma finite_atLeastLessThan [iff]:
- fixes l :: nat shows "finite {l..u(}"
+ fixes l :: nat shows "finite {l..<u}"
by (simp add: atLeastLessThan_def)
lemma finite_greaterThanAtMost [iff]:
- fixes l :: nat shows "finite {)l..u}"
+ fixes l :: nat shows "finite {l<..u}"
by (simp add: greaterThanAtMost_def)
lemma finite_atLeastAtMost [iff]:
@@ -278,16 +292,16 @@
subsubsection {* Cardinality *}
-lemma card_lessThan [simp]: "card {..u(} = u"
+lemma card_lessThan [simp]: "card {..<u} = u"
by (induct_tac u, simp_all add: lessThan_Suc)
lemma card_atMost [simp]: "card {..u} = Suc u"
by (simp add: lessThan_Suc_atMost [THEN sym])
-lemma card_atLeastLessThan [simp]: "card {l..u(} = u - l"
- apply (subgoal_tac "card {l..u(} = card {..u-l(}")
+lemma card_atLeastLessThan [simp]: "card {l..<u} = u - l"
+ apply (subgoal_tac "card {l..<u} = card {..<u-l}")
apply (erule ssubst, rule card_lessThan)
- apply (subgoal_tac "(%x. x + l) ` {..u-l(} = {l..u(}")
+ apply (subgoal_tac "(%x. x + l) ` {..<u-l} = {l..<u}")
apply (erule subst)
apply (rule card_image)
apply (rule finite_lessThan)
@@ -301,52 +315,52 @@
lemma card_atLeastAtMost [simp]: "card {l..u} = Suc u - l"
by (subst atLeastLessThanSuc_atLeastAtMost [THEN sym], simp)
-lemma card_greaterThanAtMost [simp]: "card {)l..u} = u - l"
+lemma card_greaterThanAtMost [simp]: "card {l<..u} = u - l"
by (subst atLeastSucAtMost_greaterThanAtMost [THEN sym], simp)
-lemma card_greaterThanLessThan [simp]: "card {)l..u(} = u - Suc l"
+lemma card_greaterThanLessThan [simp]: "card {l<..<u} = u - Suc l"
by (subst atLeastSucLessThan_greaterThanLessThan [THEN sym], simp)
subsection {* Intervals of integers *}
-lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l..u+1(} = {l..(u::int)}"
+lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l..<u+1} = {l..(u::int)}"
by (auto simp add: atLeastAtMost_def atLeastLessThan_def)
-lemma atLeastPlusOneAtMost_greaterThanAtMost_int: "{l+1..u} = {)l..(u::int)}"
+lemma atLeastPlusOneAtMost_greaterThanAtMost_int: "{l+1..u} = {l<..(u::int)}"
by (auto simp add: atLeastAtMost_def greaterThanAtMost_def)
lemma atLeastPlusOneLessThan_greaterThanLessThan_int:
- "{l+1..u(} = {)l..(u::int)(}"
+ "{l+1..<u} = {l<..<u::int}"
by (auto simp add: atLeastLessThan_def greaterThanLessThan_def)
subsubsection {* Finiteness *}
lemma image_atLeastZeroLessThan_int: "0 \<le> u ==>
- {(0::int)..u(} = int ` {..nat u(}"
+ {(0::int)..<u} = int ` {..<nat u}"
apply (unfold image_def lessThan_def)
apply auto
apply (rule_tac x = "nat x" in exI)
apply (auto simp add: zless_nat_conj zless_nat_eq_int_zless [THEN sym])
done
-lemma finite_atLeastZeroLessThan_int: "finite {(0::int)..u(}"
+lemma finite_atLeastZeroLessThan_int: "finite {(0::int)..<u}"
apply (case_tac "0 \<le> u")
apply (subst image_atLeastZeroLessThan_int, assumption)
apply (rule finite_imageI)
apply auto
- apply (subgoal_tac "{0..u(} = {}")
+ apply (subgoal_tac "{0..<u} = {}")
apply auto
done
lemma image_atLeastLessThan_int_shift:
- "(%x. x + (l::int)) ` {0..u-l(} = {l..u(}"
+ "(%x. x + (l::int)) ` {0..<u-l} = {l..<u}"
apply (auto simp add: image_def atLeastLessThan_iff)
apply (rule_tac x = "x - l" in bexI)
apply auto
done
-lemma finite_atLeastLessThan_int [iff]: "finite {l..(u::int)(}"
- apply (subgoal_tac "(%x. x + l) ` {0..u-l(} = {l..u(}")
+lemma finite_atLeastLessThan_int [iff]: "finite {l..<u::int}"
+ apply (subgoal_tac "(%x. x + l) ` {0..<u-l} = {l..<u}")
apply (erule subst)
apply (rule finite_imageI)
apply (rule finite_atLeastZeroLessThan_int)
@@ -356,25 +370,25 @@
lemma finite_atLeastAtMost_int [iff]: "finite {l..(u::int)}"
by (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym], simp)
-lemma finite_greaterThanAtMost_int [iff]: "finite {)l..(u::int)}"
+lemma finite_greaterThanAtMost_int [iff]: "finite {l<..(u::int)}"
by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp)
-lemma finite_greaterThanLessThan_int [iff]: "finite {)l..(u::int)(}"
+lemma finite_greaterThanLessThan_int [iff]: "finite {l<..<u::int}"
by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp)
subsubsection {* Cardinality *}
-lemma card_atLeastZeroLessThan_int: "card {(0::int)..u(} = nat u"
+lemma card_atLeastZeroLessThan_int: "card {(0::int)..<u} = nat u"
apply (case_tac "0 \<le> u")
apply (subst image_atLeastZeroLessThan_int, assumption)
apply (subst card_image)
apply (auto simp add: inj_on_def)
done
-lemma card_atLeastLessThan_int [simp]: "card {l..u(} = nat (u - l)"
- apply (subgoal_tac "card {l..u(} = card {0..u-l(}")
+lemma card_atLeastLessThan_int [simp]: "card {l..<u} = nat (u - l)"
+ apply (subgoal_tac "card {l..<u} = card {0..<u-l}")
apply (erule ssubst, rule card_atLeastZeroLessThan_int)
- apply (subgoal_tac "(%x. x + l) ` {0..u-l(} = {l..u(}")
+ apply (subgoal_tac "(%x. x + l) ` {0..<u-l} = {l..<u}")
apply (erule subst)
apply (rule card_image)
apply (rule finite_atLeastZeroLessThan_int)
@@ -387,10 +401,10 @@
apply (auto simp add: compare_rls)
done
-lemma card_greaterThanAtMost_int [simp]: "card {)l..u} = nat (u - l)"
+lemma card_greaterThanAtMost_int [simp]: "card {l<..u} = nat (u - l)"
by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp)
-lemma card_greaterThanLessThan_int [simp]: "card {)l..u(} = nat (u - (l + 1))"
+lemma card_greaterThanLessThan_int [simp]: "card {l<..<u} = nat (u - (l + 1))"
by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp)
@@ -403,38 +417,38 @@
text {* Singletons and open intervals *}
lemma ivl_disj_un_singleton:
- "{l::'a::linorder} Un {)l..} = {l..}"
- "{..u(} Un {u::'a::linorder} = {..u}"
- "(l::'a::linorder) < u ==> {l} Un {)l..u(} = {l..u(}"
- "(l::'a::linorder) < u ==> {)l..u(} Un {u} = {)l..u}"
- "(l::'a::linorder) <= u ==> {l} Un {)l..u} = {l..u}"
- "(l::'a::linorder) <= u ==> {l..u(} Un {u} = {l..u}"
+ "{l::'a::linorder} Un {l<..} = {l..}"
+ "{..<u} Un {u::'a::linorder} = {..u}"
+ "(l::'a::linorder) < u ==> {l} Un {l<..<u} = {l..<u}"
+ "(l::'a::linorder) < u ==> {l<..<u} Un {u} = {l<..u}"
+ "(l::'a::linorder) <= u ==> {l} Un {l<..u} = {l..u}"
+ "(l::'a::linorder) <= u ==> {l..<u} Un {u} = {l..u}"
by auto
text {* One- and two-sided intervals *}
lemma ivl_disj_un_one:
- "(l::'a::linorder) < u ==> {..l} Un {)l..u(} = {..u(}"
- "(l::'a::linorder) <= u ==> {..l(} Un {l..u(} = {..u(}"
- "(l::'a::linorder) <= u ==> {..l} Un {)l..u} = {..u}"
- "(l::'a::linorder) <= u ==> {..l(} Un {l..u} = {..u}"
- "(l::'a::linorder) <= u ==> {)l..u} Un {)u..} = {)l..}"
- "(l::'a::linorder) < u ==> {)l..u(} Un {u..} = {)l..}"
- "(l::'a::linorder) <= u ==> {l..u} Un {)u..} = {l..}"
- "(l::'a::linorder) <= u ==> {l..u(} Un {u..} = {l..}"
+ "(l::'a::linorder) < u ==> {..l} Un {l<..<u} = {..<u}"
+ "(l::'a::linorder) <= u ==> {..<l} Un {l..<u} = {..<u}"
+ "(l::'a::linorder) <= u ==> {..l} Un {l<..u} = {..u}"
+ "(l::'a::linorder) <= u ==> {..<l} Un {l..u} = {..u}"
+ "(l::'a::linorder) <= u ==> {l<..u} Un {u<..} = {l<..}"
+ "(l::'a::linorder) < u ==> {l<..<u} Un {u..} = {l<..}"
+ "(l::'a::linorder) <= u ==> {l..u} Un {u<..} = {l..}"
+ "(l::'a::linorder) <= u ==> {l..<u} Un {u..} = {l..}"
by auto
text {* Two- and two-sided intervals *}
lemma ivl_disj_un_two:
- "[| (l::'a::linorder) < m; m <= u |] ==> {)l..m(} Un {m..u(} = {)l..u(}"
- "[| (l::'a::linorder) <= m; m < u |] ==> {)l..m} Un {)m..u(} = {)l..u(}"
- "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m(} Un {m..u(} = {l..u(}"
- "[| (l::'a::linorder) <= m; m < u |] ==> {l..m} Un {)m..u(} = {l..u(}"
- "[| (l::'a::linorder) < m; m <= u |] ==> {)l..m(} Un {m..u} = {)l..u}"
- "[| (l::'a::linorder) <= m; m <= u |] ==> {)l..m} Un {)m..u} = {)l..u}"
- "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m(} Un {m..u} = {l..u}"
- "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m} Un {)m..u} = {l..u}"
+ "[| (l::'a::linorder) < m; m <= u |] ==> {l<..<m} Un {m..<u} = {l<..<u}"
+ "[| (l::'a::linorder) <= m; m < u |] ==> {l<..m} Un {m<..<u} = {l<..<u}"
+ "[| (l::'a::linorder) <= m; m <= u |] ==> {l..<m} Un {m..<u} = {l..<u}"
+ "[| (l::'a::linorder) <= m; m < u |] ==> {l..m} Un {m<..<u} = {l..<u}"
+ "[| (l::'a::linorder) < m; m <= u |] ==> {l<..<m} Un {m..u} = {l<..u}"
+ "[| (l::'a::linorder) <= m; m <= u |] ==> {l<..m} Un {m<..u} = {l<..u}"
+ "[| (l::'a::linorder) <= m; m <= u |] ==> {l..<m} Un {m..u} = {l..u}"
+ "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m} Un {m<..u} = {l..u}"
by auto
lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two
@@ -444,38 +458,38 @@
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} = {}"
+ "{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:
- "{..l::'a::order} Int {)l..u(} = {}"
- "{..l(} Int {l..u(} = {}"
- "{..l} Int {)l..u} = {}"
- "{..l(} Int {l..u} = {}"
- "{)l..u} Int {)u..} = {}"
- "{)l..u(} Int {u..} = {}"
- "{l..u} Int {)u..} = {}"
- "{l..u(} Int {u..} = {}"
+ "{..l::'a::order} Int {l<..<u} = {}"
+ "{..<l} Int {l..<u} = {}"
+ "{..l} Int {l<..u} = {}"
+ "{..<l} Int {l..u} = {}"
+ "{l<..u} Int {u<..} = {}"
+ "{l<..<u} Int {u..} = {}"
+ "{l..u} Int {u<..} = {}"
+ "{l..<u} Int {u..} = {}"
by auto
text {* Two- and two-sided intervals *}
lemma ivl_disj_int_two:
- "{)l::'a::order..m(} Int {m..u(} = {}"
- "{)l..m} Int {)m..u(} = {}"
- "{l..m(} Int {m..u(} = {}"
- "{l..m} Int {)m..u(} = {}"
- "{)l..m(} Int {m..u} = {}"
- "{)l..m} Int {)m..u} = {}"
- "{l..m(} Int {m..u} = {}"
- "{l..m} Int {)m..u} = {}"
+ "{l::'a::order<..<m} Int {m..<u} = {}"
+ "{l<..m} Int {m<..<u} = {}"
+ "{l..<m} Int {m..<u} = {}"
+ "{l..m} Int {m<..<u} = {}"
+ "{l<..<m} Int {m..u} = {}"
+ "{l<..m} Int {m<..u} = {}"
+ "{l..<m} Int {m..u} = {}"
+ "{l..m} Int {m<..u} = {}"
by auto
lemmas ivl_disj_int = ivl_disj_int_singleton ivl_disj_int_one ivl_disj_int_two
@@ -504,7 +518,7 @@
syntax
"_Summation" :: "idt => 'a => 'b => 'b" ("\<Sum>_<_. _" [0, 51, 10] 10)
translations
- "\<Sum>i < n. b" == "setsum (\<lambda>i. b) {..n(}"
+ "\<Sum>i < n. b" == "setsum (\<lambda>i. b) {..<n}"
lemma Summation_Suc[simp]: "(\<Sum>i < Suc n. b i) = b n + (\<Sum>i < n. b i)"
by (simp add:lessThan_Suc)
--- a/src/HOL/UNITY/Comp/AllocBase.thy Thu Jul 15 08:38:37 2004 +0200
+++ b/src/HOL/UNITY/Comp/AllocBase.thy Thu Jul 15 13:11:34 2004 +0200
@@ -87,8 +87,8 @@
lemma bag_of_sublist_Un_Int:
"bag_of (sublist l (A Un B)) + bag_of (sublist l (A Int B)) =
bag_of (sublist l A) + bag_of (sublist l B)"
-apply (subgoal_tac "A Int B Int {..length l (} =
- (A Int {..length l (}) Int (B Int {..length l (}) ")
+apply (subgoal_tac "A Int B Int {..<length l} =
+ (A Int {..<length l}) Int (B Int {..<length l}) ")
apply (simp add: bag_of_sublist Int_Un_distrib2 setsum_Un_Int, blast)
done
--- a/src/HOL/UNITY/WFair.thy Thu Jul 15 08:38:37 2004 +0200
+++ b/src/HOL/UNITY/WFair.thy Thu Jul 15 13:11:34 2004 +0200
@@ -470,7 +470,7 @@
(*Alternative proof is via the lemma F \<in> (A \<inter> f-`(lessThan m)) leadsTo B*)
lemma lessThan_induct:
- "[| !!m::nat. F \<in> (A \<inter> f-`{m}) leadsTo ((A \<inter> f-`{..m(}) \<union> B) |]
+ "[| !!m::nat. F \<in> (A \<inter> f-`{m}) leadsTo ((A \<inter> f-`{..<m}) \<union> B) |]
==> F \<in> A leadsTo B"
apply (rule wf_less_than [THEN leadsTo_wf_induct])
apply (simp (no_asm_simp))
--- a/src/HOL/ex/NatSum.thy Thu Jul 15 08:38:37 2004 +0200
+++ b/src/HOL/ex/NatSum.thy Thu Jul 15 13:11:34 2004 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/ex/NatSum.ML
+(* Title: HOL/ex/NatSum.ML
ID: $Id$
Author: Tobias Nipkow
*)
@@ -26,7 +26,7 @@
squared.
*}
-lemma sum_of_odds: "(\<Sum>i \<in> {..n(}. Suc (i + i)) = n * n"
+lemma sum_of_odds: "(\<Sum>i \<in> {..<n}. Suc (i + i)) = n * n"
apply (induct n)
apply auto
done
@@ -37,7 +37,7 @@
*}
lemma sum_of_odd_squares:
- "3 * (\<Sum>i \<in> {..n(}. Suc (2*i) * Suc (2*i)) =
+ "3 * (\<Sum>i \<in> {..<n}. Suc (2*i) * Suc (2*i)) =
n * (4 * n * n - 1)"
apply (induct n)
apply (auto split: nat_diff_split) (*eliminate the subtraction*)
@@ -51,7 +51,7 @@
lemma numeral_2_eq_2: "2 = Suc (Suc 0)" by (auto );
lemma sum_of_odd_cubes:
- "(\<Sum>i \<in> {..n(}. Suc (2*i) * Suc (2*i) * Suc (2*i)) =
+ "(\<Sum>i \<in> {..<n}. Suc (2*i) * Suc (2*i) * Suc (2*i)) =
n * n * (2 * n * n - 1)"
apply (induct n)
apply (auto split: nat_diff_split) (*eliminate the subtraction*)
@@ -105,7 +105,7 @@
zdiff_zmult_distrib2 [simp]
lemma int_sum_of_fourth_powers:
- "30 * int (\<Sum>i \<in> {..m(}. i * i * i * i) =
+ "30 * int (\<Sum>i \<in> {..<m}. i * i * i * i) =
int m * (int m - 1) * (int (2 * m) - 1) *
(int (3 * m * m) - int (3 * m) - 1)"
apply (induct m)
@@ -118,17 +118,17 @@
general case.
*}
-lemma sum_of_2_powers: "(\<Sum>i \<in> {..n(}. 2^i) = 2^n - (1::nat)"
+lemma sum_of_2_powers: "(\<Sum>i \<in> {..<n}. 2^i) = 2^n - (1::nat)"
apply (induct n)
apply (auto split: nat_diff_split)
done
-lemma sum_of_3_powers: "2 * (\<Sum>i \<in> {..n(}. 3^i) = 3^n - (1::nat)"
+lemma sum_of_3_powers: "2 * (\<Sum>i \<in> {..<n}. 3^i) = 3^n - (1::nat)"
apply (induct n)
apply auto
done
-lemma sum_of_powers: "0 < k ==> (k - 1) * (\<Sum>i \<in> {..n(}. k^i) = k^n - (1::nat)"
+lemma sum_of_powers: "0 < k ==> (k - 1) * (\<Sum>i \<in> {..<n}. k^i) = k^n - (1::nat)"
apply (induct n)
apply auto
done