author  hoelzl 
Fri, 07 Dec 2012 14:28:57 +0100  
changeset 50417  f18b92f91818 
parent 47988  e4b69e10b990 
child 50999  3de230ed0547 
permissions  rwrr 
47317
432b29a96f61
modernized obsolete oldstyle theory name with proper newstyle underscore
huffman
parents:
47222
diff
changeset

1 
(* Title: HOL/Set_Interval.thy 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32596
diff
changeset

2 
Author: Tobias Nipkow 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32596
diff
changeset

3 
Author: Clemens Ballarin 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32596
diff
changeset

4 
Author: Jeremy Avigad 
8924  5 

13735  6 
lessThan, greaterThan, atLeast, atMost and twosided intervals 
8924  7 
*) 
8 

14577  9 
header {* Set intervals *} 
10 

47317
432b29a96f61
modernized obsolete oldstyle theory name with proper newstyle underscore
huffman
parents:
47222
diff
changeset

11 
theory Set_Interval 
33318
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33044
diff
changeset

12 
imports Int Nat_Transfer 
15131  13 
begin 
8924  14 

24691  15 
context ord 
16 
begin 

44008  17 

24691  18 
definition 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32596
diff
changeset

19 
lessThan :: "'a => 'a set" ("(1{..<_})") where 
25062  20 
"{..<u} == {x. x < u}" 
24691  21 

22 
definition 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32596
diff
changeset

23 
atMost :: "'a => 'a set" ("(1{.._})") where 
25062  24 
"{..u} == {x. x \<le> u}" 
24691  25 

26 
definition 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32596
diff
changeset

27 
greaterThan :: "'a => 'a set" ("(1{_<..})") where 
25062  28 
"{l<..} == {x. l<x}" 
24691  29 

30 
definition 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32596
diff
changeset

31 
atLeast :: "'a => 'a set" ("(1{_..})") where 
25062  32 
"{l..} == {x. l\<le>x}" 
24691  33 

34 
definition 

25062  35 
greaterThanLessThan :: "'a => 'a => 'a set" ("(1{_<..<_})") where 
36 
"{l<..<u} == {l<..} Int {..<u}" 

24691  37 

38 
definition 

25062  39 
atLeastLessThan :: "'a => 'a => 'a set" ("(1{_..<_})") where 
40 
"{l..<u} == {l..} Int {..<u}" 

24691  41 

42 
definition 

25062  43 
greaterThanAtMost :: "'a => 'a => 'a set" ("(1{_<.._})") where 
44 
"{l<..u} == {l<..} Int {..u}" 

24691  45 

46 
definition 

25062  47 
atLeastAtMost :: "'a => 'a => 'a set" ("(1{_.._})") where 
48 
"{l..u} == {l..} Int {..u}" 

24691  49 

50 
end 

8924  51 

13735  52 

15048  53 
text{* A note of warning when using @{term"{..<n}"} on type @{typ 
54 
nat}: it is equivalent to @{term"{0::nat..<n}"} but some lemmas involving 

15052  55 
@{term"{m..<n}"} may not exist in @{term"{..<n}"}form as well. *} 
15048  56 

14418  57 
syntax 
36364
0e2679025aeb
fix syntax precedence declarations for UNION, INTER, SUP, INF
huffman
parents:
36307
diff
changeset

58 
"_UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3UN _<=_./ _)" [0, 0, 10] 10) 
0e2679025aeb
fix syntax precedence declarations for UNION, INTER, SUP, INF
huffman
parents:
36307
diff
changeset

59 
"_UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3UN _<_./ _)" [0, 0, 10] 10) 
0e2679025aeb
fix syntax precedence declarations for UNION, INTER, SUP, INF
huffman
parents:
36307
diff
changeset

60 
"_INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3INT _<=_./ _)" [0, 0, 10] 10) 
0e2679025aeb
fix syntax precedence declarations for UNION, INTER, SUP, INF
huffman
parents:
36307
diff
changeset

61 
"_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3INT _<_./ _)" [0, 0, 10] 10) 
14418  62 

30372  63 
syntax (xsymbols) 
36364
0e2679025aeb
fix syntax precedence declarations for UNION, INTER, SUP, INF
huffman
parents:
36307
diff
changeset

64 
"_UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3\<Union> _\<le>_./ _)" [0, 0, 10] 10) 
0e2679025aeb
fix syntax precedence declarations for UNION, INTER, SUP, INF
huffman
parents:
36307
diff
changeset

65 
"_UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3\<Union> _<_./ _)" [0, 0, 10] 10) 
0e2679025aeb
fix syntax precedence declarations for UNION, INTER, SUP, INF
huffman
parents:
36307
diff
changeset

66 
"_INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3\<Inter> _\<le>_./ _)" [0, 0, 10] 10) 
0e2679025aeb
fix syntax precedence declarations for UNION, INTER, SUP, INF
huffman
parents:
36307
diff
changeset

67 
"_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3\<Inter> _<_./ _)" [0, 0, 10] 10) 
14418  68 

30372  69 
syntax (latex output) 
36364
0e2679025aeb
fix syntax precedence declarations for UNION, INTER, SUP, INF
huffman
parents:
36307
diff
changeset

70 
"_UNION_le" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Union>(00_ \<le> _)/ _)" [0, 0, 10] 10) 
0e2679025aeb
fix syntax precedence declarations for UNION, INTER, SUP, INF
huffman
parents:
36307
diff
changeset

71 
"_UNION_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Union>(00_ < _)/ _)" [0, 0, 10] 10) 
0e2679025aeb
fix syntax precedence declarations for UNION, INTER, SUP, INF
huffman
parents:
36307
diff
changeset

72 
"_INTER_le" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Inter>(00_ \<le> _)/ _)" [0, 0, 10] 10) 
0e2679025aeb
fix syntax precedence declarations for UNION, INTER, SUP, INF
huffman
parents:
36307
diff
changeset

73 
"_INTER_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Inter>(00_ < _)/ _)" [0, 0, 10] 10) 
14418  74 

75 
translations 

76 
"UN i<=n. A" == "UN i:{..n}. A" 

15045  77 
"UN i<n. A" == "UN i:{..<n}. A" 
14418  78 
"INT i<=n. A" == "INT i:{..n}. A" 
15045  79 
"INT i<n. A" == "INT i:{..<n}. A" 
14418  80 

81 

14485  82 
subsection {* Various equivalences *} 
13735  83 

25062  84 
lemma (in ord) lessThan_iff [iff]: "(i: lessThan k) = (i<k)" 
13850  85 
by (simp add: lessThan_def) 
13735  86 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

87 
lemma Compl_lessThan [simp]: 
13735  88 
"!!k:: 'a::linorder. lessThan k = atLeast k" 
13850  89 
apply (auto simp add: lessThan_def atLeast_def) 
13735  90 
done 
91 

13850  92 
lemma single_Diff_lessThan [simp]: "!!k:: 'a::order. {k}  lessThan k = {k}" 
93 
by auto 

13735  94 

25062  95 
lemma (in ord) greaterThan_iff [iff]: "(i: greaterThan k) = (k<i)" 
13850  96 
by (simp add: greaterThan_def) 
13735  97 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

98 
lemma Compl_greaterThan [simp]: 
13735  99 
"!!k:: 'a::linorder. greaterThan k = atMost k" 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25919
diff
changeset

100 
by (auto simp add: greaterThan_def atMost_def) 
13735  101 

13850  102 
lemma Compl_atMost [simp]: "!!k:: 'a::linorder. atMost k = greaterThan k" 
103 
apply (subst Compl_greaterThan [symmetric]) 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

104 
apply (rule double_complement) 
13735  105 
done 
106 

25062  107 
lemma (in ord) atLeast_iff [iff]: "(i: atLeast k) = (k<=i)" 
13850  108 
by (simp add: atLeast_def) 
13735  109 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

110 
lemma Compl_atLeast [simp]: 
13735  111 
"!!k:: 'a::linorder. atLeast k = lessThan k" 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25919
diff
changeset

112 
by (auto simp add: lessThan_def atLeast_def) 
13735  113 

25062  114 
lemma (in ord) atMost_iff [iff]: "(i: atMost k) = (i<=k)" 
13850  115 
by (simp add: atMost_def) 
13735  116 

14485  117 
lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}" 
118 
by (blast intro: order_antisym) 

13850  119 

120 

14485  121 
subsection {* Logical Equivalences for Set Inclusion and Equality *} 
13850  122 

123 
lemma atLeast_subset_iff [iff]: 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

124 
"(atLeast x \<subseteq> atLeast y) = (y \<le> (x::'a::order))" 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

125 
by (blast intro: order_trans) 
13850  126 

127 
lemma atLeast_eq_iff [iff]: 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

128 
"(atLeast x = atLeast y) = (x = (y::'a::linorder))" 
13850  129 
by (blast intro: order_antisym order_trans) 
130 

131 
lemma greaterThan_subset_iff [iff]: 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

132 
"(greaterThan x \<subseteq> greaterThan y) = (y \<le> (x::'a::linorder))" 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

133 
apply (auto simp add: greaterThan_def) 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

134 
apply (subst linorder_not_less [symmetric], blast) 
13850  135 
done 
136 

137 
lemma greaterThan_eq_iff [iff]: 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

138 
"(greaterThan x = greaterThan y) = (x = (y::'a::linorder))" 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

139 
apply (rule iffI) 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

140 
apply (erule equalityE) 
29709  141 
apply simp_all 
13850  142 
done 
143 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

144 
lemma atMost_subset_iff [iff]: "(atMost x \<subseteq> atMost y) = (x \<le> (y::'a::order))" 
13850  145 
by (blast intro: order_trans) 
146 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

147 
lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))" 
13850  148 
by (blast intro: order_antisym order_trans) 
149 

150 
lemma lessThan_subset_iff [iff]: 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

151 
"(lessThan x \<subseteq> lessThan y) = (x \<le> (y::'a::linorder))" 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

152 
apply (auto simp add: lessThan_def) 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

153 
apply (subst linorder_not_less [symmetric], blast) 
13850  154 
done 
155 

156 
lemma lessThan_eq_iff [iff]: 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

157 
"(lessThan x = lessThan y) = (x = (y::'a::linorder))" 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

158 
apply (rule iffI) 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

159 
apply (erule equalityE) 
29709  160 
apply simp_all 
13735  161 
done 
162 

40703
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

163 
lemma lessThan_strict_subset_iff: 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

164 
fixes m n :: "'a::linorder" 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

165 
shows "{..<m} < {..<n} \<longleftrightarrow> m < n" 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

166 
by (metis leD lessThan_subset_iff linorder_linear not_less_iff_gr_or_eq psubset_eq) 
13735  167 

13850  168 
subsection {*Twosided intervals*} 
13735  169 

24691  170 
context ord 
171 
begin 

172 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35644
diff
changeset

173 
lemma greaterThanLessThan_iff [simp,no_atp]: 
25062  174 
"(i : {l<..<u}) = (l < i & i < u)" 
13735  175 
by (simp add: greaterThanLessThan_def) 
176 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35644
diff
changeset

177 
lemma atLeastLessThan_iff [simp,no_atp]: 
25062  178 
"(i : {l..<u}) = (l <= i & i < u)" 
13735  179 
by (simp add: atLeastLessThan_def) 
180 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35644
diff
changeset

181 
lemma greaterThanAtMost_iff [simp,no_atp]: 
25062  182 
"(i : {l<..u}) = (l < i & i <= u)" 
13735  183 
by (simp add: greaterThanAtMost_def) 
184 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35644
diff
changeset

185 
lemma atLeastAtMost_iff [simp,no_atp]: 
25062  186 
"(i : {l..u}) = (l <= i & i <= u)" 
13735  187 
by (simp add: atLeastAtMost_def) 
188 

32436
10cd49e0c067
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
nipkow
parents:
32408
diff
changeset

189 
text {* The above four lemmas could be declared as iffs. Unfortunately this 
10cd49e0c067
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
nipkow
parents:
32408
diff
changeset

190 
breaks many proofs. Since it only helps blast, it is better to leave well 
10cd49e0c067
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
nipkow
parents:
32408
diff
changeset

191 
alone *} 
10cd49e0c067
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
nipkow
parents:
32408
diff
changeset

192 

24691  193 
end 
13735  194 

32400  195 
subsubsection{* Emptyness, singletons, subset *} 
15554  196 

24691  197 
context order 
198 
begin 

15554  199 

32400  200 
lemma atLeastatMost_empty[simp]: 
201 
"b < a \<Longrightarrow> {a..b} = {}" 

202 
by(auto simp: atLeastAtMost_def atLeast_def atMost_def) 

203 

204 
lemma atLeastatMost_empty_iff[simp]: 

205 
"{a..b} = {} \<longleftrightarrow> (~ a <= b)" 

206 
by auto (blast intro: order_trans) 

207 

208 
lemma atLeastatMost_empty_iff2[simp]: 

209 
"{} = {a..b} \<longleftrightarrow> (~ a <= b)" 

210 
by auto (blast intro: order_trans) 

211 

212 
lemma atLeastLessThan_empty[simp]: 

213 
"b <= a \<Longrightarrow> {a..<b} = {}" 

214 
by(auto simp: atLeastLessThan_def) 

24691  215 

32400  216 
lemma atLeastLessThan_empty_iff[simp]: 
217 
"{a..<b} = {} \<longleftrightarrow> (~ a < b)" 

218 
by auto (blast intro: le_less_trans) 

219 

220 
lemma atLeastLessThan_empty_iff2[simp]: 

221 
"{} = {a..<b} \<longleftrightarrow> (~ a < b)" 

222 
by auto (blast intro: le_less_trans) 

15554  223 

32400  224 
lemma greaterThanAtMost_empty[simp]: "l \<le> k ==> {k<..l} = {}" 
17719  225 
by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def) 
226 

32400  227 
lemma greaterThanAtMost_empty_iff[simp]: "{k<..l} = {} \<longleftrightarrow> ~ k < l" 
228 
by auto (blast intro: less_le_trans) 

229 

230 
lemma greaterThanAtMost_empty_iff2[simp]: "{} = {k<..l} \<longleftrightarrow> ~ k < l" 

231 
by auto (blast intro: less_le_trans) 

232 

29709  233 
lemma greaterThanLessThan_empty[simp]:"l \<le> k ==> {k<..<l} = {}" 
17719  234 
by(auto simp:greaterThanLessThan_def greaterThan_def lessThan_def) 
235 

25062  236 
lemma atLeastAtMost_singleton [simp]: "{a..a} = {a}" 
24691  237 
by (auto simp add: atLeastAtMost_def atMost_def atLeast_def) 
238 

36846
0f67561ed5a6
Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
hoelzl
parents:
36755
diff
changeset

239 
lemma atLeastAtMost_singleton': "a = b \<Longrightarrow> {a .. b} = {a}" by simp 
0f67561ed5a6
Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
hoelzl
parents:
36755
diff
changeset

240 

32400  241 
lemma atLeastatMost_subset_iff[simp]: 
242 
"{a..b} <= {c..d} \<longleftrightarrow> (~ a <= b)  c <= a & b <= d" 

243 
unfolding atLeastAtMost_def atLeast_def atMost_def 

244 
by (blast intro: order_trans) 

245 

246 
lemma atLeastatMost_psubset_iff: 

247 
"{a..b} < {c..d} \<longleftrightarrow> 

248 
((~ a <= b)  c <= a & b <= d & (c < a  b < d)) & c <= d" 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

249 
by(simp add: psubset_eq set_eq_iff less_le_not_le)(blast intro: order_trans) 
32400  250 

36846
0f67561ed5a6
Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
hoelzl
parents:
36755
diff
changeset

251 
lemma atLeastAtMost_singleton_iff[simp]: 
0f67561ed5a6
Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
hoelzl
parents:
36755
diff
changeset

252 
"{a .. b} = {c} \<longleftrightarrow> a = b \<and> b = c" 
0f67561ed5a6
Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
hoelzl
parents:
36755
diff
changeset

253 
proof 
0f67561ed5a6
Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
hoelzl
parents:
36755
diff
changeset

254 
assume "{a..b} = {c}" 
0f67561ed5a6
Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
hoelzl
parents:
36755
diff
changeset

255 
hence "\<not> (\<not> a \<le> b)" unfolding atLeastatMost_empty_iff[symmetric] by simp 
0f67561ed5a6
Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
hoelzl
parents:
36755
diff
changeset

256 
moreover with `{a..b} = {c}` have "c \<le> a \<and> b \<le> c" by auto 
0f67561ed5a6
Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
hoelzl
parents:
36755
diff
changeset

257 
ultimately show "a = b \<and> b = c" by auto 
0f67561ed5a6
Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
hoelzl
parents:
36755
diff
changeset

258 
qed simp 
0f67561ed5a6
Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
hoelzl
parents:
36755
diff
changeset

259 

24691  260 
end 
14485  261 

42891
e2f473671937
simp rules for empty intervals on dense linear order
hoelzl
parents:
40703
diff
changeset

262 
context dense_linorder 
e2f473671937
simp rules for empty intervals on dense linear order
hoelzl
parents:
40703
diff
changeset

263 
begin 
e2f473671937
simp rules for empty intervals on dense linear order
hoelzl
parents:
40703
diff
changeset

264 

e2f473671937
simp rules for empty intervals on dense linear order
hoelzl
parents:
40703
diff
changeset

265 
lemma greaterThanLessThan_empty_iff[simp]: 
e2f473671937
simp rules for empty intervals on dense linear order
hoelzl
parents:
40703
diff
changeset

266 
"{ a <..< b } = {} \<longleftrightarrow> b \<le> a" 
e2f473671937
simp rules for empty intervals on dense linear order
hoelzl
parents:
40703
diff
changeset

267 
using dense[of a b] by (cases "a < b") auto 
e2f473671937
simp rules for empty intervals on dense linear order
hoelzl
parents:
40703
diff
changeset

268 

e2f473671937
simp rules for empty intervals on dense linear order
hoelzl
parents:
40703
diff
changeset

269 
lemma greaterThanLessThan_empty_iff2[simp]: 
e2f473671937
simp rules for empty intervals on dense linear order
hoelzl
parents:
40703
diff
changeset

270 
"{} = { a <..< b } \<longleftrightarrow> b \<le> a" 
e2f473671937
simp rules for empty intervals on dense linear order
hoelzl
parents:
40703
diff
changeset

271 
using dense[of a b] by (cases "a < b") auto 
e2f473671937
simp rules for empty intervals on dense linear order
hoelzl
parents:
40703
diff
changeset

272 

42901  273 
lemma atLeastLessThan_subseteq_atLeastAtMost_iff: 
274 
"{a ..< b} \<subseteq> { c .. d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b \<le> d)" 

275 
using dense[of "max a d" "b"] 

276 
by (force simp: subset_eq Ball_def not_less[symmetric]) 

277 

278 
lemma greaterThanAtMost_subseteq_atLeastAtMost_iff: 

279 
"{a <.. b} \<subseteq> { c .. d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b \<le> d)" 

280 
using dense[of "a" "min c b"] 

281 
by (force simp: subset_eq Ball_def not_less[symmetric]) 

282 

283 
lemma greaterThanLessThan_subseteq_atLeastAtMost_iff: 

284 
"{a <..< b} \<subseteq> { c .. d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b \<le> d)" 

285 
using dense[of "a" "min c b"] dense[of "max a d" "b"] 

286 
by (force simp: subset_eq Ball_def not_less[symmetric]) 

287 

43657  288 
lemma atLeastAtMost_subseteq_atLeastLessThan_iff: 
289 
"{a .. b} \<subseteq> { c ..< d } \<longleftrightarrow> (a \<le> b \<longrightarrow> c \<le> a \<and> b < d)" 

290 
using dense[of "max a d" "b"] 

291 
by (force simp: subset_eq Ball_def not_less[symmetric]) 

292 

293 
lemma greaterThanAtMost_subseteq_atLeastLessThan_iff: 

294 
"{a <.. b} \<subseteq> { c ..< d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b < d)" 

295 
using dense[of "a" "min c b"] 

296 
by (force simp: subset_eq Ball_def not_less[symmetric]) 

297 

298 
lemma greaterThanLessThan_subseteq_atLeastLessThan_iff: 

299 
"{a <..< b} \<subseteq> { c ..< d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b \<le> d)" 

300 
using dense[of "a" "min c b"] dense[of "max a d" "b"] 

301 
by (force simp: subset_eq Ball_def not_less[symmetric]) 

302 

42891
e2f473671937
simp rules for empty intervals on dense linear order
hoelzl
parents:
40703
diff
changeset

303 
end 
e2f473671937
simp rules for empty intervals on dense linear order
hoelzl
parents:
40703
diff
changeset

304 

32408  305 
lemma (in linorder) atLeastLessThan_subset_iff: 
306 
"{a..<b} <= {c..<d} \<Longrightarrow> b <= a  c<=a & b<=d" 

307 
apply (auto simp:subset_eq Ball_def) 

308 
apply(frule_tac x=a in spec) 

309 
apply(erule_tac x=d in allE) 

310 
apply (simp add: less_imp_le) 

311 
done 

312 

40703
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

313 
lemma atLeastLessThan_inj: 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

314 
fixes a b c d :: "'a::linorder" 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

315 
assumes eq: "{a ..< b} = {c ..< d}" and "a < b" "c < d" 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

316 
shows "a = c" "b = d" 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

317 
using assms by (metis atLeastLessThan_subset_iff eq less_le_not_le linorder_antisym_conv2 subset_refl)+ 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

318 

d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

319 
lemma atLeastLessThan_eq_iff: 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

320 
fixes a b c d :: "'a::linorder" 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

321 
assumes "a < b" "c < d" 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

322 
shows "{a ..< b} = {c ..< d} \<longleftrightarrow> a = c \<and> b = d" 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

323 
using atLeastLessThan_inj assms by auto 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

324 

32456
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

325 
subsubsection {* Intersection *} 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

326 

341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

327 
context linorder 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

328 
begin 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

329 

341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

330 
lemma Int_atLeastAtMost[simp]: "{a..b} Int {c..d} = {max a c .. min b d}" 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

331 
by auto 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

332 

341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

333 
lemma Int_atLeastAtMostR1[simp]: "{..b} Int {c..d} = {c .. min b d}" 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

334 
by auto 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

335 

341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

336 
lemma Int_atLeastAtMostR2[simp]: "{a..} Int {c..d} = {max a c .. d}" 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

337 
by auto 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

338 

341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

339 
lemma Int_atLeastAtMostL1[simp]: "{a..b} Int {..d} = {a .. min b d}" 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

340 
by auto 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

341 

341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

342 
lemma Int_atLeastAtMostL2[simp]: "{a..b} Int {c..} = {max a c .. b}" 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

343 
by auto 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

344 

341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

345 
lemma Int_atLeastLessThan[simp]: "{a..<b} Int {c..<d} = {max a c ..< min b d}" 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

346 
by auto 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

347 

341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

348 
lemma Int_greaterThanAtMost[simp]: "{a<..b} Int {c<..d} = {max a c <.. min b d}" 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

349 
by auto 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

350 

341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

351 
lemma Int_greaterThanLessThan[simp]: "{a<..<b} Int {c<..<d} = {max a c <..< min b d}" 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

352 
by auto 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

353 

50417  354 
lemma Int_atMost[simp]: "{..a} \<inter> {..b} = {.. min a b}" 
355 
by (auto simp: min_def) 

356 

32456
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

357 
end 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

358 

341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

359 

14485  360 
subsection {* Intervals of natural numbers *} 
361 

15047  362 
subsubsection {* The Constant @{term lessThan} *} 
363 

14485  364 
lemma lessThan_0 [simp]: "lessThan (0::nat) = {}" 
365 
by (simp add: lessThan_def) 

366 

367 
lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)" 

368 
by (simp add: lessThan_def less_Suc_eq, blast) 

369 

43156  370 
text {* The following proof is convenient in induction proofs where 
39072  371 
new elements get indices at the beginning. So it is used to transform 
372 
@{term "{..<Suc n}"} to @{term "0::nat"} and @{term "{..< n}"}. *} 

373 

374 
lemma lessThan_Suc_eq_insert_0: "{..<Suc n} = insert 0 (Suc ` {..<n})" 

375 
proof safe 

376 
fix x assume "x < Suc n" "x \<notin> Suc ` {..<n}" 

377 
then have "x \<noteq> Suc (x  1)" by auto 

378 
with `x < Suc n` show "x = 0" by auto 

379 
qed 

380 

14485  381 
lemma lessThan_Suc_atMost: "lessThan (Suc k) = atMost k" 
382 
by (simp add: lessThan_def atMost_def less_Suc_eq_le) 

383 

384 
lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV" 

385 
by blast 

386 

15047  387 
subsubsection {* The Constant @{term greaterThan} *} 
388 

14485  389 
lemma greaterThan_0 [simp]: "greaterThan 0 = range Suc" 
390 
apply (simp add: greaterThan_def) 

391 
apply (blast dest: gr0_conv_Suc [THEN iffD1]) 

392 
done 

393 

394 
lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k  {Suc k}" 

395 
apply (simp add: greaterThan_def) 

396 
apply (auto elim: linorder_neqE) 

397 
done 

398 

399 
lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}" 

400 
by blast 

401 

15047  402 
subsubsection {* The Constant @{term atLeast} *} 
403 

14485  404 
lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV" 
405 
by (unfold atLeast_def UNIV_def, simp) 

406 

407 
lemma atLeast_Suc: "atLeast (Suc k) = atLeast k  {k}" 

408 
apply (simp add: atLeast_def) 

409 
apply (simp add: Suc_le_eq) 

410 
apply (simp add: order_le_less, blast) 

411 
done 

412 

413 
lemma atLeast_Suc_greaterThan: "atLeast (Suc k) = greaterThan k" 

414 
by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le) 

415 

416 
lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV" 

417 
by blast 

418 

15047  419 
subsubsection {* The Constant @{term atMost} *} 
420 

14485  421 
lemma atMost_0 [simp]: "atMost (0::nat) = {0}" 
422 
by (simp add: atMost_def) 

423 

424 
lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)" 

425 
apply (simp add: atMost_def) 

426 
apply (simp add: less_Suc_eq order_le_less, blast) 

427 
done 

428 

429 
lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV" 

430 
by blast 

431 

15047  432 
subsubsection {* The Constant @{term atLeastLessThan} *} 
433 

28068  434 
text{*The orientation of the following 2 rules is tricky. The lhs is 
24449  435 
defined in terms of the rhs. Hence the chosen orientation makes sense 
436 
in this theory  the reverse orientation complicates proofs (eg 

437 
nontermination). But outside, when the definition of the lhs is rarely 

438 
used, the opposite orientation seems preferable because it reduces a 

439 
specific concept to a more general one. *} 

28068  440 

15047  441 
lemma atLeast0LessThan: "{0::nat..<n} = {..<n}" 
15042  442 
by(simp add:lessThan_def atLeastLessThan_def) 
24449  443 

28068  444 
lemma atLeast0AtMost: "{0..n::nat} = {..n}" 
445 
by(simp add:atMost_def atLeastAtMost_def) 

446 

31998
2c7a24f74db9
code attributes use common underscore convention
haftmann
parents:
31509
diff
changeset

447 
declare atLeast0LessThan[symmetric, code_unfold] 
2c7a24f74db9
code attributes use common underscore convention
haftmann
parents:
31509
diff
changeset

448 
atLeast0AtMost[symmetric, code_unfold] 
24449  449 

450 
lemma atLeastLessThan0: "{m..<0::nat} = {}" 

15047  451 
by (simp add: atLeastLessThan_def) 
24449  452 

15047  453 
subsubsection {* Intervals of nats with @{term Suc} *} 
454 

455 
text{*Not a simprule because the RHS is too messy.*} 

456 
lemma atLeastLessThanSuc: 

457 
"{m..<Suc n} = (if m \<le> n then insert n {m..<n} else {})" 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

458 
by (auto simp add: atLeastLessThan_def) 
15047  459 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

460 
lemma atLeastLessThan_singleton [simp]: "{m..<Suc m} = {m}" 
15047  461 
by (auto simp add: atLeastLessThan_def) 
16041  462 
(* 
15047  463 
lemma atLeast_sum_LessThan [simp]: "{m + k..<k::nat} = {}" 
464 
by (induct k, simp_all add: atLeastLessThanSuc) 

465 

466 
lemma atLeastSucLessThan [simp]: "{Suc n..<n} = {}" 

467 
by (auto simp add: atLeastLessThan_def) 

16041  468 
*) 
15045  469 
lemma atLeastLessThanSuc_atLeastAtMost: "{l..<Suc u} = {l..u}" 
14485  470 
by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def) 
471 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

472 
lemma atLeastSucAtMost_greaterThanAtMost: "{Suc l..u} = {l<..u}" 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

473 
by (simp add: atLeast_Suc_greaterThan atLeastAtMost_def 
14485  474 
greaterThanAtMost_def) 
475 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

476 
lemma atLeastSucLessThan_greaterThanLessThan: "{Suc l..<u} = {l<..<u}" 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

477 
by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def 
14485  478 
greaterThanLessThan_def) 
479 

15554  480 
lemma atLeastAtMostSuc_conv: "m \<le> Suc n \<Longrightarrow> {m..Suc n} = insert (Suc n) {m..n}" 
481 
by (auto simp add: atLeastAtMost_def) 

482 

45932  483 
lemma atLeastAtMost_insertL: "m \<le> n \<Longrightarrow> insert m {Suc m..n} = {m ..n}" 
484 
by auto 

485 

43157  486 
text {* The analogous result is useful on @{typ int}: *} 
487 
(* here, because we don't have an own int section *) 

488 
lemma atLeastAtMostPlus1_int_conv: 

489 
"m <= 1+n \<Longrightarrow> {m..1+n} = insert (1+n) {m..n::int}" 

490 
by (auto intro: set_eqI) 

491 

33044  492 
lemma atLeastLessThan_add_Un: "i \<le> j \<Longrightarrow> {i..<j+k} = {i..<j} \<union> {j..<j+k::nat}" 
493 
apply (induct k) 

494 
apply (simp_all add: atLeastLessThanSuc) 

495 
done 

496 

16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

497 
subsubsection {* Image *} 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

498 

236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

499 
lemma image_add_atLeastAtMost: 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

500 
"(%n::nat. n+k) ` {i..j} = {i+k..j+k}" (is "?A = ?B") 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

501 
proof 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

502 
show "?A \<subseteq> ?B" by auto 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

503 
next 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

504 
show "?B \<subseteq> ?A" 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

505 
proof 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

506 
fix n assume a: "n : ?B" 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19538
diff
changeset

507 
hence "n  k : {i..j}" by auto 
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

508 
moreover have "n = (n  k) + k" using a by auto 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

509 
ultimately show "n : ?A" by blast 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

510 
qed 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

511 
qed 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

512 

236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

513 
lemma image_add_atLeastLessThan: 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

514 
"(%n::nat. n+k) ` {i..<j} = {i+k..<j+k}" (is "?A = ?B") 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

515 
proof 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

516 
show "?A \<subseteq> ?B" by auto 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

517 
next 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

518 
show "?B \<subseteq> ?A" 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

519 
proof 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

520 
fix n assume a: "n : ?B" 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19538
diff
changeset

521 
hence "n  k : {i..<j}" by auto 
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

522 
moreover have "n = (n  k) + k" using a by auto 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

523 
ultimately show "n : ?A" by blast 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

524 
qed 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

525 
qed 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

526 

236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

527 
corollary image_Suc_atLeastAtMost[simp]: 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

528 
"Suc ` {i..j} = {Suc i..Suc j}" 
30079
293b896b9c25
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
huffman
parents:
29960
diff
changeset

529 
using image_add_atLeastAtMost[where k="Suc 0"] by simp 
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

530 

236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

531 
corollary image_Suc_atLeastLessThan[simp]: 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

532 
"Suc ` {i..<j} = {Suc i..<Suc j}" 
30079
293b896b9c25
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
huffman
parents:
29960
diff
changeset

533 
using image_add_atLeastLessThan[where k="Suc 0"] by simp 
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

534 

236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

535 
lemma image_add_int_atLeastLessThan: 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

536 
"(%x. x + (l::int)) ` {0..<ul} = {l..<u}" 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

537 
apply (auto simp add: image_def) 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

538 
apply (rule_tac x = "x  l" in bexI) 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

539 
apply auto 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

540 
done 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

541 

37664  542 
lemma image_minus_const_atLeastLessThan_nat: 
543 
fixes c :: nat 

544 
shows "(\<lambda>i. i  c) ` {x ..< y} = 

545 
(if c < y then {x  c ..< y  c} else if x < y then {0} else {})" 

546 
(is "_ = ?right") 

547 
proof safe 

548 
fix a assume a: "a \<in> ?right" 

549 
show "a \<in> (\<lambda>i. i  c) ` {x ..< y}" 

550 
proof cases 

551 
assume "c < y" with a show ?thesis 

552 
by (auto intro!: image_eqI[of _ _ "a + c"]) 

553 
next 

554 
assume "\<not> c < y" with a show ?thesis 

555 
by (auto intro!: image_eqI[of _ _ x] split: split_if_asm) 

556 
qed 

557 
qed auto 

558 

35580  559 
context ordered_ab_group_add 
560 
begin 

561 

562 
lemma 

563 
fixes x :: 'a 

564 
shows image_uminus_greaterThan[simp]: "uminus ` {x<..} = {..<x}" 

565 
and image_uminus_atLeast[simp]: "uminus ` {x..} = {..x}" 

566 
proof safe 

567 
fix y assume "y < x" 

568 
hence *: "x < y" using neg_less_iff_less[of "y" x] by simp 

569 
have " (y) \<in> uminus ` {x<..}" 

570 
by (rule imageI) (simp add: *) 

571 
thus "y \<in> uminus ` {x<..}" by simp 

572 
next 

573 
fix y assume "y \<le> x" 

574 
have " (y) \<in> uminus ` {x..}" 

575 
by (rule imageI) (insert `y \<le> x`[THEN le_imp_neg_le], simp) 

576 
thus "y \<in> uminus ` {x..}" by simp 

577 
qed simp_all 

578 

579 
lemma 

580 
fixes x :: 'a 

581 
shows image_uminus_lessThan[simp]: "uminus ` {..<x} = {x<..}" 

582 
and image_uminus_atMost[simp]: "uminus ` {..x} = {x..}" 

583 
proof  

584 
have "uminus ` {..<x} = uminus ` uminus ` {x<..}" 

585 
and "uminus ` {..x} = uminus ` uminus ` {x..}" by simp_all 

586 
thus "uminus ` {..<x} = {x<..}" and "uminus ` {..x} = {x..}" 

587 
by (simp_all add: image_image 

588 
del: image_uminus_greaterThan image_uminus_atLeast) 

589 
qed 

590 

591 
lemma 

592 
fixes x :: 'a 

593 
shows image_uminus_atLeastAtMost[simp]: "uminus ` {x..y} = {y..x}" 

594 
and image_uminus_greaterThanAtMost[simp]: "uminus ` {x<..y} = {y..<x}" 

595 
and image_uminus_atLeastLessThan[simp]: "uminus ` {x..<y} = {y<..x}" 

596 
and image_uminus_greaterThanLessThan[simp]: "uminus ` {x<..<y} = {y<..<x}" 

597 
by (simp_all add: atLeastAtMost_def greaterThanAtMost_def atLeastLessThan_def 

598 
greaterThanLessThan_def image_Int[OF inj_uminus] Int_commute) 

599 
end 

16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

600 

14485  601 
subsubsection {* Finiteness *} 
602 

15045  603 
lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..<k}" 
14485  604 
by (induct k) (simp_all add: lessThan_Suc) 
605 

606 
lemma finite_atMost [iff]: fixes k :: nat shows "finite {..k}" 

607 
by (induct k) (simp_all add: atMost_Suc) 

608 

609 
lemma finite_greaterThanLessThan [iff]: 

15045  610 
fixes l :: nat shows "finite {l<..<u}" 
14485  611 
by (simp add: greaterThanLessThan_def) 
612 

613 
lemma finite_atLeastLessThan [iff]: 

15045  614 
fixes l :: nat shows "finite {l..<u}" 
14485  615 
by (simp add: atLeastLessThan_def) 
616 

617 
lemma finite_greaterThanAtMost [iff]: 

15045  618 
fixes l :: nat shows "finite {l<..u}" 
14485  619 
by (simp add: greaterThanAtMost_def) 
620 

621 
lemma finite_atLeastAtMost [iff]: 

622 
fixes l :: nat shows "finite {l..u}" 

623 
by (simp add: atLeastAtMost_def) 

624 

28068  625 
text {* A bounded set of natural numbers is finite. *} 
14485  626 
lemma bounded_nat_set_is_finite: 
24853  627 
"(ALL i:N. i < (n::nat)) ==> finite N" 
28068  628 
apply (rule finite_subset) 
629 
apply (rule_tac [2] finite_lessThan, auto) 

630 
done 

631 

31044  632 
text {* A set of natural numbers is finite iff it is bounded. *} 
633 
lemma finite_nat_set_iff_bounded: 

634 
"finite(N::nat set) = (EX m. ALL n:N. n<m)" (is "?F = ?B") 

635 
proof 

636 
assume f:?F show ?B 

637 
using Max_ge[OF `?F`, simplified less_Suc_eq_le[symmetric]] by blast 

638 
next 

639 
assume ?B show ?F using `?B` by(blast intro:bounded_nat_set_is_finite) 

640 
qed 

641 

642 
lemma finite_nat_set_iff_bounded_le: 

643 
"finite(N::nat set) = (EX m. ALL n:N. n<=m)" 

644 
apply(simp add:finite_nat_set_iff_bounded) 

645 
apply(blast dest:less_imp_le_nat le_imp_less_Suc) 

646 
done 

647 

28068  648 
lemma finite_less_ub: 
649 
"!!f::nat=>nat. (!!n. n \<le> f n) ==> finite {n. f n \<le> u}" 

650 
by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans) 

14485  651 

24853  652 
text{* Any subset of an interval of natural numbers the size of the 
653 
subset is exactly that interval. *} 

654 

655 
lemma subset_card_intvl_is_intvl: 

656 
"A <= {k..<k+card A} \<Longrightarrow> A = {k..<k+card A}" (is "PROP ?P") 

657 
proof cases 

658 
assume "finite A" 

659 
thus "PROP ?P" 

32006  660 
proof(induct A rule:finite_linorder_max_induct) 
24853  661 
case empty thus ?case by auto 
662 
next 

33434  663 
case (insert b A) 
24853  664 
moreover hence "b ~: A" by auto 
665 
moreover have "A <= {k..<k+card A}" and "b = k+card A" 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44008
diff
changeset

666 
using `b ~: A` insert by fastforce+ 
24853  667 
ultimately show ?case by auto 
668 
qed 

669 
next 

670 
assume "~finite A" thus "PROP ?P" by simp 

671 
qed 

672 

673 

32596
bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset

674 
subsubsection {* Proving Inclusions and Equalities between Unions *} 
bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset

675 

36755  676 
lemma UN_le_eq_Un0: 
677 
"(\<Union>i\<le>n::nat. M i) = (\<Union>i\<in>{1..n}. M i) \<union> M 0" (is "?A = ?B") 

678 
proof 

679 
show "?A <= ?B" 

680 
proof 

681 
fix x assume "x : ?A" 

682 
then obtain i where i: "i\<le>n" "x : M i" by auto 

683 
show "x : ?B" 

684 
proof(cases i) 

685 
case 0 with i show ?thesis by simp 

686 
next 

687 
case (Suc j) with i show ?thesis by auto 

688 
qed 

689 
qed 

690 
next 

691 
show "?B <= ?A" by auto 

692 
qed 

693 

694 
lemma UN_le_add_shift: 

695 
"(\<Union>i\<le>n::nat. M(i+k)) = (\<Union>i\<in>{k..n+k}. M i)" (is "?A = ?B") 

696 
proof 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44008
diff
changeset

697 
show "?A <= ?B" by fastforce 
36755  698 
next 
699 
show "?B <= ?A" 

700 
proof 

701 
fix x assume "x : ?B" 

702 
then obtain i where i: "i : {k..n+k}" "x : M(i)" by auto 

703 
hence "ik\<le>n & x : M((ik)+k)" by auto 

704 
thus "x : ?A" by blast 

705 
qed 

706 
qed 

707 

32596
bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset

708 
lemma UN_UN_finite_eq: "(\<Union>n::nat. \<Union>i\<in>{0..<n}. A i) = (\<Union>n. A n)" 
bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset

709 
by (auto simp add: atLeast0LessThan) 
bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset

710 

bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset

711 
lemma UN_finite_subset: "(!!n::nat. (\<Union>i\<in>{0..<n}. A i) \<subseteq> C) \<Longrightarrow> (\<Union>n. A n) \<subseteq> C" 
bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset

712 
by (subst UN_UN_finite_eq [symmetric]) blast 
bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset

713 

33044  714 
lemma UN_finite2_subset: 
715 
"(!!n::nat. (\<Union>i\<in>{0..<n}. A i) \<subseteq> (\<Union>i\<in>{0..<n+k}. B i)) \<Longrightarrow> (\<Union>n. A n) \<subseteq> (\<Union>n. B n)" 

716 
apply (rule UN_finite_subset) 

717 
apply (subst UN_UN_finite_eq [symmetric, of B]) 

718 
apply blast 

719 
done 

32596
bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset

720 

bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset

721 
lemma UN_finite2_eq: 
33044  722 
"(!!n::nat. (\<Union>i\<in>{0..<n}. A i) = (\<Union>i\<in>{0..<n+k}. B i)) \<Longrightarrow> (\<Union>n. A n) = (\<Union>n. B n)" 
723 
apply (rule subset_antisym) 

724 
apply (rule UN_finite2_subset, blast) 

725 
apply (rule UN_finite2_subset [where k=k]) 

35216  726 
apply (force simp add: atLeastLessThan_add_Un [of 0]) 
33044  727 
done 
32596
bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset

728 

bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset

729 

14485  730 
subsubsection {* Cardinality *} 
731 

15045  732 
lemma card_lessThan [simp]: "card {..<u} = u" 
15251  733 
by (induct u, simp_all add: lessThan_Suc) 
14485  734 

735 
lemma card_atMost [simp]: "card {..u} = Suc u" 

736 
by (simp add: lessThan_Suc_atMost [THEN sym]) 

737 

15045  738 
lemma card_atLeastLessThan [simp]: "card {l..<u} = u  l" 
739 
apply (subgoal_tac "card {l..<u} = card {..<ul}") 

14485  740 
apply (erule ssubst, rule card_lessThan) 
15045  741 
apply (subgoal_tac "(%x. x + l) ` {..<ul} = {l..<u}") 
14485  742 
apply (erule subst) 
743 
apply (rule card_image) 

744 
apply (simp add: inj_on_def) 

745 
apply (auto simp add: image_def atLeastLessThan_def lessThan_def) 

746 
apply (rule_tac x = "x  l" in exI) 

747 
apply arith 

748 
done 

749 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

750 
lemma card_atLeastAtMost [simp]: "card {l..u} = Suc u  l" 
14485  751 
by (subst atLeastLessThanSuc_atLeastAtMost [THEN sym], simp) 
752 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

753 
lemma card_greaterThanAtMost [simp]: "card {l<..u} = u  l" 
14485  754 
by (subst atLeastSucAtMost_greaterThanAtMost [THEN sym], simp) 
755 

15045  756 
lemma card_greaterThanLessThan [simp]: "card {l<..<u} = u  Suc l" 
14485  757 
by (subst atLeastSucLessThan_greaterThanLessThan [THEN sym], simp) 
758 

26105
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset

759 
lemma ex_bij_betw_nat_finite: 
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset

760 
"finite M \<Longrightarrow> \<exists>h. bij_betw h {0..<card M} M" 
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset

761 
apply(drule finite_imp_nat_seg_image_inj_on) 
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset

762 
apply(auto simp:atLeast0LessThan[symmetric] lessThan_def[symmetric] card_image bij_betw_def) 
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset

763 
done 
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset

764 

ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset

765 
lemma ex_bij_betw_finite_nat: 
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset

766 
"finite M \<Longrightarrow> \<exists>h. bij_betw h M {0..<card M}" 
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset

767 
by (blast dest: ex_bij_betw_nat_finite bij_betw_inv) 
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset

768 

31438  769 
lemma finite_same_card_bij: 
770 
"finite A \<Longrightarrow> finite B \<Longrightarrow> card A = card B \<Longrightarrow> EX h. bij_betw h A B" 

771 
apply(drule ex_bij_betw_finite_nat) 

772 
apply(drule ex_bij_betw_nat_finite) 

773 
apply(auto intro!:bij_betw_trans) 

774 
done 

775 

776 
lemma ex_bij_betw_nat_finite_1: 

777 
"finite M \<Longrightarrow> \<exists>h. bij_betw h {1 .. card M} M" 

778 
by (rule finite_same_card_bij) auto 

779 

40703
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

780 
lemma bij_betw_iff_card: 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

781 
assumes FIN: "finite A" and FIN': "finite B" 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

782 
shows BIJ: "(\<exists>f. bij_betw f A B) \<longleftrightarrow> (card A = card B)" 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

783 
using assms 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

784 
proof(auto simp add: bij_betw_same_card) 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

785 
assume *: "card A = card B" 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

786 
obtain f where "bij_betw f A {0 ..< card A}" 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

787 
using FIN ex_bij_betw_finite_nat by blast 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

788 
moreover obtain g where "bij_betw g {0 ..< card B} B" 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

789 
using FIN' ex_bij_betw_nat_finite by blast 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

790 
ultimately have "bij_betw (g o f) A B" 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

791 
using * by (auto simp add: bij_betw_trans) 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

792 
thus "(\<exists>f. bij_betw f A B)" by blast 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

793 
qed 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

794 

d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

795 
lemma inj_on_iff_card_le: 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

796 
assumes FIN: "finite A" and FIN': "finite B" 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

797 
shows "(\<exists>f. inj_on f A \<and> f ` A \<le> B) = (card A \<le> card B)" 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

798 
proof (safe intro!: card_inj_on_le) 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

799 
assume *: "card A \<le> card B" 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

800 
obtain f where 1: "inj_on f A" and 2: "f ` A = {0 ..< card A}" 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

801 
using FIN ex_bij_betw_finite_nat unfolding bij_betw_def by force 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

802 
moreover obtain g where "inj_on g {0 ..< card B}" and 3: "g ` {0 ..< card B} = B" 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

803 
using FIN' ex_bij_betw_nat_finite unfolding bij_betw_def by force 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

804 
ultimately have "inj_on g (f ` A)" using subset_inj_on[of g _ "f ` A"] * by force 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

805 
hence "inj_on (g o f) A" using 1 comp_inj_on by blast 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

806 
moreover 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

807 
{have "{0 ..< card A} \<le> {0 ..< card B}" using * by force 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

808 
with 2 have "f ` A \<le> {0 ..< card B}" by blast 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

809 
hence "(g o f) ` A \<le> B" unfolding comp_def using 3 by force 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

810 
} 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

811 
ultimately show "(\<exists>f. inj_on f A \<and> f ` A \<le> B)" by blast 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

812 
qed (insert assms, auto) 
26105
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset

813 

14485  814 
subsection {* Intervals of integers *} 
815 

15045  816 
lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l..<u+1} = {l..(u::int)}" 
14485  817 
by (auto simp add: atLeastAtMost_def atLeastLessThan_def) 
818 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

819 
lemma atLeastPlusOneAtMost_greaterThanAtMost_int: "{l+1..u} = {l<..(u::int)}" 
14485  820 
by (auto simp add: atLeastAtMost_def greaterThanAtMost_def) 
821 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

822 
lemma atLeastPlusOneLessThan_greaterThanLessThan_int: 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

823 
"{l+1..<u} = {l<..<u::int}" 
14485  824 
by (auto simp add: atLeastLessThan_def greaterThanLessThan_def) 
825 

826 
subsubsection {* Finiteness *} 

827 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

828 
lemma image_atLeastZeroLessThan_int: "0 \<le> u ==> 
15045  829 
{(0::int)..<u} = int ` {..<nat u}" 
14485  830 
apply (unfold image_def lessThan_def) 
831 
apply auto 

832 
apply (rule_tac x = "nat x" in exI) 

35216  833 
apply (auto simp add: zless_nat_eq_int_zless [THEN sym]) 
14485  834 
done 
835 

15045  836 
lemma finite_atLeastZeroLessThan_int: "finite {(0::int)..<u}" 
47988  837 
apply (cases "0 \<le> u") 
14485  838 
apply (subst image_atLeastZeroLessThan_int, assumption) 
839 
apply (rule finite_imageI) 

840 
apply auto 

841 
done 

842 

15045  843 
lemma finite_atLeastLessThan_int [iff]: "finite {l..<u::int}" 
844 
apply (subgoal_tac "(%x. x + l) ` {0..<ul} = {l..<u}") 

14485  845 
apply (erule subst) 
846 
apply (rule finite_imageI) 

847 
apply (rule finite_atLeastZeroLessThan_int) 

16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

848 
apply (rule image_add_int_atLeastLessThan) 
14485  849 
done 
850 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

851 
lemma finite_atLeastAtMost_int [iff]: "finite {l..(u::int)}" 
14485  852 
by (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym], simp) 
853 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

854 
lemma finite_greaterThanAtMost_int [iff]: "finite {l<..(u::int)}" 
14485  855 
by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp) 
856 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

857 
lemma finite_greaterThanLessThan_int [iff]: "finite {l<..<u::int}" 
14485  858 
by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp) 
859 

24853  860 

14485  861 
subsubsection {* Cardinality *} 
862 

15045  863 
lemma card_atLeastZeroLessThan_int: "card {(0::int)..<u} = nat u" 
47988  864 
apply (cases "0 \<le> u") 
14485  865 
apply (subst image_atLeastZeroLessThan_int, assumption) 
866 
apply (subst card_image) 

867 
apply (auto simp add: inj_on_def) 

868 
done 

869 

15045  870 
lemma card_atLeastLessThan_int [simp]: "card {l..<u} = nat (u  l)" 
871 
apply (subgoal_tac "card {l..<u} = card {0..<ul}") 

14485  872 
apply (erule ssubst, rule card_atLeastZeroLessThan_int) 
15045  873 
apply (subgoal_tac "(%x. x + l) ` {0..<ul} = {l..<u}") 
14485  874 
apply (erule subst) 
875 
apply (rule card_image) 

876 
apply (simp add: inj_on_def) 

16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

877 
apply (rule image_add_int_atLeastLessThan) 
14485  878 
done 
879 

880 
lemma card_atLeastAtMost_int [simp]: "card {l..u} = nat (u  l + 1)" 

29667  881 
apply (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym]) 
882 
apply (auto simp add: algebra_simps) 

883 
done 

14485  884 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

885 
lemma card_greaterThanAtMost_int [simp]: "card {l<..u} = nat (u  l)" 
29667  886 
by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp) 
14485  887 

15045  888 
lemma card_greaterThanLessThan_int [simp]: "card {l<..<u} = nat (u  (l + 1))" 
29667  889 
by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp) 
14485  890 

27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

891 
lemma finite_M_bounded_by_nat: "finite {k. P k \<and> k < (i::nat)}" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

892 
proof  
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

893 
have "{k. P k \<and> k < i} \<subseteq> {..<i}" by auto 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

894 
with finite_lessThan[of "i"] show ?thesis by (simp add: finite_subset) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

895 
qed 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

896 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

897 
lemma card_less: 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

898 
assumes zero_in_M: "0 \<in> M" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

899 
shows "card {k \<in> M. k < Suc i} \<noteq> 0" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

900 
proof  
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

901 
from zero_in_M have "{k \<in> M. k < Suc i} \<noteq> {}" by auto 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

902 
with finite_M_bounded_by_nat show ?thesis by (auto simp add: card_eq_0_iff) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

903 
qed 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

904 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

905 
lemma card_less_Suc2: "0 \<notin> M \<Longrightarrow> card {k. Suc k \<in> M \<and> k < i} = card {k \<in> M. k < Suc i}" 
37388  906 
apply (rule card_bij_eq [of Suc _ _ "\<lambda>x. x  Suc 0"]) 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

907 
apply simp 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44008
diff
changeset

908 
apply fastforce 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

909 
apply auto 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

910 
apply (rule inj_on_diff_nat) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

911 
apply auto 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

912 
apply (case_tac x) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

913 
apply auto 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

914 
apply (case_tac xa) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

915 
apply auto 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

916 
apply (case_tac xa) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

917 
apply auto 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

918 
done 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

919 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

920 
lemma card_less_Suc: 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

921 
assumes zero_in_M: "0 \<in> M" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

922 
shows "Suc (card {k. Suc k \<in> M \<and> k < i}) = card {k \<in> M. k < Suc i}" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

923 
proof  
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

924 
from assms have a: "0 \<in> {k \<in> M. k < Suc i}" by simp 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

925 
hence c: "{k \<in> M. k < Suc i} = insert 0 ({k \<in> M. k < Suc i}  {0})" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

926 
by (auto simp only: insert_Diff) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

927 
have b: "{k \<in> M. k < Suc i}  {0} = {k \<in> M  {0}. k < Suc i}" by auto 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

928 
from finite_M_bounded_by_nat[of "\<lambda>x. x \<in> M" "Suc i"] have "Suc (card {k. Suc k \<in> M \<and> k < i}) = card (insert 0 ({k \<in> M. k < Suc i}  {0}))" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

929 
apply (subst card_insert) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

930 
apply simp_all 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

931 
apply (subst b) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

932 
apply (subst card_less_Suc2[symmetric]) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

933 
apply simp_all 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

934 
done 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

935 
with c show ?thesis by simp 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

936 
qed 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

937 

14485  938 

13850  939 
subsection {*Lemmas useful with the summation operator setsum*} 
940 

16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16052
diff
changeset

941 
text {* For examples, see Algebra/poly/UnivPoly2.thy *} 
13735  942 

14577  943 
subsubsection {* Disjoint Unions *} 
13735  944 

14577  945 
text {* Singletons and open intervals *} 
13735  946 

947 
lemma ivl_disj_un_singleton: 

15045  948 
"{l::'a::linorder} Un {l<..} = {l..}" 
949 
"{..<u} Un {u::'a::linorder} = {..u}" 

950 
"(l::'a::linorder) < u ==> {l} Un {l<..<u} = {l..<u}" 

951 
"(l::'a::linorder) < u ==> {l<..<u} Un {u} = {l<..u}" 

952 
"(l::'a::linorder) <= u ==> {l} Un {l<..u} = {l..u}" 

953 
"(l::'a::linorder) <= u ==> {l..<u} Un {u} = {l..u}" 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
13850
diff
changeset

954 
by auto 
13735  955 

14577  956 
text {* One and twosided intervals *} 
13735  957 

958 
lemma ivl_disj_un_one: 

15045  959 
"(l::'a::linorder) < u ==> {..l} Un {l<..<u} = {..<u}" 
960 
"(l::'a::linorder) <= u ==> {..<l} Un {l..<u} = {..<u}" 

961 
"(l::'a::linorder) <= u ==> {..l} Un {l<..u} = {..u}" 

962 
"(l::'a::linorder) <= u ==> {..<l} Un {l..u} = {..u}" 

963 
"(l::'a::linorder) <= u ==> {l<..u} Un {u<..} = {l<..}" 

964 
"(l::'a::linorder) < u ==> {l<..<u} Un {u..} = {l<..}" 

965 
"(l::'a::linorder) <= u ==> {l..u} Un {u<..} = {l..}" 

966 
"(l::'a::linorder) <= u ==> {l..<u} Un {u..} = {l..}" 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
13850
diff
changeset

967 
by auto 
13735  968 

14577  969 
text {* Two and twosided intervals *} 
13735  970 

971 
lemma ivl_disj_un_two: 

15045  972 
"[ (l::'a::linorder) < m; m <= u ] ==> {l<..<m} Un {m..<u} = {l<..<u}" 
973 
"[ (l::'a::linorder) <= m; m < u ] ==> {l<..m} Un {m<..<u} = {l<..<u}" 

974 
"[ (l::'a::linorder) <= m; m <= u ] ==> {l..<m} Un {m..<u} = {l..<u}" 

975 
"[ (l::'a::linorder) <= m; m < u ] ==> {l..m} Un {m<..<u} = {l..<u}" 

976 
"[ (l::'a::linorder) < m; m <= u ] ==> {l<..<m} Un {m..u} = {l<..u}" 

977 
"[ (l::'a::linorder) <= m; m <= u ] ==> {l<..m} Un {m<..u} = {l<..u}" 

978 
"[ (l::'a::linorder) <= m; m <= u ] ==> {l..<m} Un {m..u} = {l..u}" 

979 
"[ (l::'a::linorder) <= m; m <= u ] ==> {l..m} Un {m<..u} = {l..u}" 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
13850
diff
changeset

980 
by auto 
13735  981 

982 
lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two 

983 

14577  984 
subsubsection {* Disjoint Intersections *} 
13735  985 

14577  986 
text {* One and twosided intervals *} 
13735  987 

988 
lemma ivl_disj_int_one: 

15045  989 
"{..l::'a::order} Int {l<..<u} = {}" 
990 
"{..<l} Int {l..<u} = {}" 

991 
"{..l} Int {l<..u} = {}" 

992 
"{..<l} Int {l..u} = {}" 

993 
"{l<..u} Int {u<..} = {}" 

994 
"{l<..<u} Int {u..} = {}" 

995 
"{l..u} Int {u<..} = {}" 

996 
"{l..<u} Int {u..} = {}" 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
13850
diff
changeset

997 
by auto 
13735  998 

14577  999 
text {* Two and twosided intervals *} 
13735  1000 

1001 
lemma ivl_disj_int_two: 

15045  1002 
"{l::'a::order<..<m} Int {m..<u} = {}" 
1003 
"{l<..m} Int {m<..<u} = {}" 

1004 
"{l..<m} Int {m..<u} = {}" 

1005 
"{l..m} Int {m<..<u} = {}" 

1006 
"{l<..<m} Int {m..u} = {}" 

1007 
"{l<..m} Int {m<..u} = {}" 

1008 
"{l..<m} Int {m..u} = {}" 

1009 
"{l..m} Int {m<..u} = {}" 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
13850
diff
changeset

1010 
by auto 
13735  1011 

32456
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

1012 
lemmas ivl_disj_int = ivl_disj_int_one ivl_disj_int_two 
13735  1013 

15542  1014 
subsubsection {* Some Differences *} 
1015 

1016 
lemma ivl_diff[simp]: 

1017 
"i \<le> n \<Longrightarrow> {i..<m}  {i..<n} = {n..<(m::'a::linorder)}" 

1018 
by(auto) 

1019 

1020 

1021 
subsubsection {* Some Subset Conditions *} 

1022 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35644
diff
changeset

1023 
lemma ivl_subset [simp,no_atp]: 
15542  1024 
"({i..<j} \<subseteq> {m..<n}) = (j \<le> i  m \<le> i & j \<le> (n::'a::linorder))" 
1025 
apply(auto simp:linorder_not_le) 

1026 
apply(rule ccontr) 

1027 
apply(insert linorder_le_less_linear[of i n]) 

1028 
apply(clarsimp simp:linorder_not_le) 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44008
diff
changeset

1029 
apply(fastforce) 
15542  1030 
done 
1031 

15041
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14846
diff
changeset

1032 

15042  1033 
subsection {* Summation indexed over intervals *} 
1034 

1035 
syntax 

1036 
"_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10) 

15048  1037 
"_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10) 
16052  1038 
"_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _<_./ _)" [0,0,10] 10) 
1039 
"_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _<=_./ _)" [0,0,10] 10) 

15042  1040 
syntax (xsymbols) 
1041 
"_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10) 

15048  1042 
"_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10) 
16052  1043 
"_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10) 
1044 
"_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_\<le>_./ _)" [0,0,10] 10) 

15042  1045 
syntax (HTML output) 
1046 
"_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10) 

15048  1047 
"_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10) 
16052  1048 
"_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10) 
1049 
"_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_\<le>_./ _)" [0,0,10] 10) 

15056  1050 
syntax (latex_sum output) 
15052  1051 
"_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" 
1052 
("(3\<^raw:$\sum_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10) 

1053 
"_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" 

1054 
("(3\<^raw:$\sum_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10) 

16052  1055 
"_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" 
1056 
("(3\<^raw:$\sum_{>_ < _\<^raw:}$> _)" [0,0,10] 10) 

15052  1057 
"_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" 
16052  1058 
("(3\<^raw:$\sum_{>_ \<le> _\<^raw:}$> _)" [0,0,10] 10) 
15041
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14846
diff
changeset

1059 

15048  1060 
translations 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28068
diff
changeset

1061 
"\<Sum>x=a..b. t" == "CONST setsum (%x. t) {a..b}" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28068
diff
changeset

1062 
"\<Sum>x=a..<b. t" == "CONST setsum (%x. t) {a..<b}" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28068
diff
changeset

1063 
"\<Sum>i\<le>n. t" == "CONST setsum (\<lambda>i. t) {..n}" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28068
diff
changeset

1064 
"\<Sum>i<n. t" == "CONST setsum (\<lambda>i. t) {..<n}" 
15041
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14846
diff
changeset

1065 

15052  1066 
text{* The above introduces some pretty alternative syntaxes for 
15056  1067 
summation over intervals: 
15052  1068 
\begin{center} 
1069 
\begin{tabular}{lll} 

15056  1070 
Old & New & \LaTeX\\ 
1071 
@{term[source]"\<Sum>x\<in>{a..b}. e"} & @{term"\<Sum>x=a..b. e"} & @{term[mode=latex_sum]"\<Sum>x=a..b. e"}\\ 

1072 
@{term[source]"\<Sum>x\<in>{a..<b}. e"} & @{term"\<Sum>x=a..<b. e"} & @{term[mode=latex_sum]"\<Sum>x=a..<b. e"}\\ 

16052  1073 
@{term[source]"\<Sum>x\<in>{..b}. e"} & @{term"\<Sum>x\<le>b. e"} & @{term[mode=latex_sum]"\<Sum>x\<le>b. e"}\\ 
15056  1074 
@{term[source]"\<Sum>x\<in>{..<b}. e"} & @{term"\<Sum>x<b. e"} & @{term[mode=latex_sum]"\<Sum>x<b. e"} 
15052  1075 
\end{tabular} 
1076 
\end{center} 

15056  1077 
The left column shows the term before introduction of the new syntax, 
1078 
the middle column shows the new (default) syntax, and the right column 

1079 
shows a special syntax. The latter is only meaningful for latex output 

1080 
and has to be activated explicitly by setting the print mode to 

21502  1081 
@{text latex_sum} (e.g.\ via @{text "mode = latex_sum"} in 
15056  1082 
antiquotations). It is not the default \LaTeX\ output because it only 
1083 
works well with italicstyle formulae, not ttstyle. 

15052  1084 

1085 
Note that for uniformity on @{typ nat} it is better to use 

1086 
@{term"\<Sum>x::nat=0..<n. e"} rather than @{text"\<Sum>x<n. e"}: @{text setsum} may 

1087 
not provide all lemmas available for @{term"{m..<n}"} also in the 

1088 
special form for @{term"{..<n}"}. *} 

1089 

15542  1090 
text{* This congruence rule should be used for sums over intervals as 
1091 
the standard theorem @{text[source]setsum_cong} does not work well 

1092 
with the simplifier who adds the unsimplified premise @{term"x:B"} to 

1093 
the context. *} 

1094 

1095 
lemma setsum_ivl_cong: 

1096 
"\<lbrakk>a = c; b = d; !!x. \<lbrakk> c \<le> x; x < d \<rbrakk> \<Longrightarrow> f x = g x \<rbrakk> \<Longrightarrow> 

1097 
setsum f {a..<b} = setsum g {c..<d}" 

1098 
by(rule setsum_cong, simp_all) 

15041
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14846
diff
changeset

1099 

16041  1100 
(* FIXME why are the following simp rules but the corresponding eqns 
1101 
on intervals are not? *) 

1102 

16052  1103 
lemma setsum_atMost_Suc[simp]: "(\<Sum>i \<le> Suc n. f i) = (\<Sum>i \<le> n. f i) + f(Suc n)" 
1104 
by (simp add:atMost_Suc add_ac) 

1105 

16041  1106 
lemma setsum_lessThan_Suc[simp]: "(\<Sum>i < Suc n. f i) = (\<Sum>i < n. f i) + f n" 
1107 
by (simp add:lessThan_Suc add_ac) 

15041
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14846
diff
changeset

1108 

15911  1109 
lemma setsum_cl_ivl_Suc[simp]: 
15561  1110 
"setsum f {m..Suc n} = (if Suc n < m then 0 else setsum f {m..n} + f(Suc n))" 
1111 
by (auto simp:add_ac atLeastAtMostSuc_conv) 

1112 

15911  1113 
lemma setsum_op_ivl_Suc[simp]: 
15561  1114 
"setsum f {m..<Suc n} = (if n < m then 0 else setsum f {m..<n} + f(n))" 
1115 
by (auto simp:add_ac atLeastLessThanSuc) 

16041  1116 
(* 
15561  1117 
lemma setsum_cl_ivl_add_one_nat: "(n::nat) <= m + 1 ==> 
1118 
(\<Sum>i=n..m+1. f i) = (\<Sum>i=n..m. f i) + f(m + 1)" 

1119 
by (auto simp:add_ac atLeastAtMostSuc_conv) 

16041  1120 
*) 
28068  1121 

1122 
lemma setsum_head: 

1123 
fixes n :: nat 

1124 
assumes mn: "m <= n" 

1125 
shows "(\<Sum>x\<in>{m..n}. P x) = P m + (\<Sum>x\<in>{m<..n}. P x)" (is "?lhs = ?rhs") 

1126 
proof  

1127 
from mn 

1128 
have "{m..n} = {m} \<union> {m<..n}" 

1129 
by (auto intro: ivl_disj_un_singleton) 

1130 
hence "?lhs = (\<Sum>x\<in>{m} \<union> {m<..n}. P x)" 

1131 
by (simp add: atLeast0LessThan) 

1132 
also have "\<dots> = ?rhs" by simp 

1133 
finally show ?thesis . 

1134 
qed 

1135 

1136 
lemma setsum_head_Suc: 

1137 
"m \<le> n \<Longrightarrow> setsum f {m..n} = f m + setsum f {Suc m..n}" 

1138 
by (simp add: setsum_head atLeastSucAtMost_greaterThanAtMost) 

1139 

1140 
lemma setsum_head_upt_Suc: 

1141 
"m < n \<Longrightarrow> setsum f {m..<n} = f m + setsum f {Suc m..<n}" 

30079
293b896b9c25
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
huffman
parents:
29960
diff
changeset

1142 
apply(insert setsum_head_Suc[of m "n  Suc 0" f]) 
29667  1143 
apply (simp add: atLeastLessThanSuc_atLeastAtMost[symmetric] algebra_simps) 
28068  1144 
done 
1145 

31501  1146 
lemma setsum_ub_add_nat: assumes "(m::nat) \<le> n + 1" 
1147 
shows "setsum f {m..n + p} = setsum f {m..n} + setsum f {n + 1..n + p}" 

1148 
proof 

1149 
have "{m .. n+p} = {m..n} \<union> {n+1..n+p}" using `m \<le> n+1` by auto 

1150 
thus ?thesis by (auto simp: ivl_disj_int setsum_Un_disjoint 

1151 
atLeastSucAtMost_greaterThanAtMost) 

1152 
qed 

28068  1153 

15539  1154 
lemma setsum_add_nat_ivl: "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow> 
1155 
setsum f {m..<n} + setsum f {n..<p} = setsum f {m..<p::nat}" 

1156 
by (simp add:setsum_Un_disjoint[symmetric] ivl_disj_int ivl_disj_un) 

1157 

1158 
lemma setsum_diff_nat_ivl: 

1159 
fixes f :: "nat \<Rightarrow> 'a::ab_group_add" 

1160 
shows "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow> 

1161 
setsum f {m..<p}  setsum f {m..<n} = setsum f {n..<p}" 

1162 
using setsum_add_nat_ivl [of m n p f,symmetric] 

1163 
apply (simp add: add_ac) 

1164 
done 

1165 

31505  1166 
lemma setsum_natinterval_difff: 
1167 
fixes f:: "nat \<Rightarrow> ('a::ab_group_add)" 

1168 
shows "setsum (\<lambda>k. f k  f(k + 1)) {(m::nat) .. n} = 

1169 
(if m <= n then f m  f(n + 1) else 0)" 

1170 
by (induct n, auto simp add: algebra_simps not_le le_Suc_eq) 

1171 

44008  1172 
lemma setsum_restrict_set': 
1173 
"finite A \<Longrightarrow> setsum f {x \<in> A. x \<in> B} = (\<Sum>x\<in>A. if x \<in> B then f x else 0)" 

1174 
by (simp add: setsum_restrict_set [symmetric] Int_def) 

1175 

1176 
lemma setsum_restrict_set'': 

1177 
"finite A \<Longrightarrow> setsum f {x \<in> A. P x} = (\<Sum>x\<in>A. if P x then f x else 0)" 

1178 
by (simp add: setsum_restrict_set' [of A f "{x. P x}", simplified mem_Collect_eq]) 

31509  1179 

1180 
lemma setsum_setsum_restrict: 

44008  1181 
"finite S \<Longrightarrow> finite T \<Longrightarrow> 
1182 
setsum (\<lambda>x. setsum (\<lambda>y. f x y) {y. y \<in> T \<and> R x y}) S = setsum (\<lambda>y. setsum (\<lambda>x. f x y) {x. x \<in> S \<and> R x y}) T" 

1183 
by (simp add: setsum_restrict_set'') (rule setsum_commute) 

31509  1184 

1185 
lemma setsum_image_gen: assumes fS: "finite S" 

1186 
shows "setsum g S = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)" 

1187 
proof 

1188 
{ fix x assume "x \<in> S" then have "{y. y\<in> f`S \<and> f x = y} = {f x}" by auto } 

1189 
hence "setsum g S = setsum (\<lambda>x. setsum (\<lambda>y. g x) {y. y\<in> f`S \<and> f x = y}) S" 

1190 
by simp 

1191 
also have "\<dots> = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)" 

1192 
by (rule setsum_setsum_restrict[OF fS finite_imageI[OF fS]]) 

1193 
finally show ?thesis . 

1194 
qed 

1195 

35171
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1196 
lemma setsum_le_included: 
36307
1732232f9b27
sharpened constraint (c.f. 4e7f5b22dd7d); explicit is better than implicit
haftmann
parents:
35828
diff
changeset

1197 
fixes f :: "'a \<Rightarrow> 'b::ordered_comm_monoid_add" 
35171
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1198 
assumes "finite s" "finite t" 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1199 
and "\<forall>y\<in>t. 0 \<le> g y" "(\<forall>x\<in>s. \<exists>y\<in>t. i y = x \<and> f x \<le> g y)" 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1200 
shows "setsum f s \<le> setsum g t" 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1201 
proof  
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1202 
have "setsum f s \<le> setsum (\<lambda>y. setsum g {x. x\<in>t \<and> i x = y}) s" 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1203 
proof (rule setsum_mono) 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1204 
fix y assume "y \<in> s" 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1205 
with assms obtain z where z: "z \<in> t" "y = i z" "f y \<le> g z" by auto 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1206 
with assms show "f y \<le> setsum g {x \<in> t. i x = y}" (is "?A y \<le> ?B y") 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1207 
using order_trans[of "?A (i z)" "setsum g {z}" "?B (i z)", intro] 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1208 
by (auto intro!: setsum_mono2) 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1209 
qed 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1210 
also have "... \<le> setsum (\<lambda>y. setsum g {x. x\<in>t \<and> i x = y}) (i ` t)" 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1211 
using assms(24) by (auto intro!: setsum_mono2 setsum_nonneg) 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1212 
also have "... \<le> setsum g t" 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1213 
using assms by (auto simp: setsum_image_gen[symmetric]) 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1214 
finally show ?thesis . 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1215 
qed 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1216 

31509  1217 
lemma setsum_multicount_gen: 
1218 
assumes "finite s" "finite t" "\<forall>j\<in>t. (card {i\<in>s. R i j} = k j)" 

1219 
shows "setsum (\<lambda>i. (card {j\<in>t. R i j})) s = setsum k t" (is "?l = ?r") 

1220 
proof 

1221 
have "?l = setsum (\<lambda>i. setsum (\<lambda>x.1) {j\<in>t. R i j}) s" by auto 

1222 
also have "\<dots> = ?r" unfolding setsum_setsum_restrict[OF assms(12)] 

1223 
using assms(3) by auto 

1224 
finally show ?thesis . 

1225 
qed 

1226 

1227 
lemma setsum_multicount: 

1228 
assumes "finite S" "finite T" "\<forall>j\<in>T. (card {i\<in>S. R i j} = k)" 

1229 
shows "setsum (\<lambda>i. card {j\<in>T. R i j}) S = k * card T" (is "?l = ?r") 

1230 
proof 

1231 
have "?l = setsum (\<lambda>i. k) T" by(rule setsum_multicount_gen)(auto simp:assms) 

35216  1232 
also have "\<dots> = ?r" by(simp add: mult_commute) 
31509  1233 
finally show ?thesis by auto 
1234 
qed 

1235 

28068  1236 

16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

1237 
subsection{* Shifting bounds *} 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

1238 

15539  1239 
lemma setsum_shift_bounds_nat_ivl: 
1240 
"setsum f {m+k..<n+k} = setsum (%i. f(i + k)){m..<n::nat}" 

1241 
by (induct "n", auto simp:atLeastLessThanSuc) 

1242 

16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

1243 
lemma setsum_shift_bounds_cl_nat_ivl: 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

1244 
"setsum f {m+k..n+k} = setsum (%i. f(i + k)){m..n::nat}" 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

1245 
apply (insert setsum_reindex[OF inj_on_add_nat, where h=f and B = "{m..n}"]) 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

1246 
apply (simp add:image_add_atLeastAtMost o_def) 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

1247 
done 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

1248 

236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

1249 
corollary setsum_shift_bounds_cl_Suc_ivl: 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

1250 
"setsum f {Suc m..Suc n} = setsum (%i. f(Suc i)){m..n}" 
30079
293b896b9c25
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
huffman
parents:
29960
diff
changeset

1251 
by (simp add:setsum_shift_bounds_cl_nat_ivl[where k="Suc 0", simplified]) 
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

1252 

236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

1253 
corollary setsum_shift_bounds_Suc_ivl: 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

1254 
"setsum f {Suc m..<Suc n} = setsum (%i. f(Suc i)){m..<n}" 
30079
293b896b9c25
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
huffman
parents:
29960
diff
changeset

1255 
by (simp add:setsum_shift_bounds_nat_ivl[where k="Suc 0", simplified]) 
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

1256 

28068  1257 
lemma setsum_shift_lb_Suc0_0: 
1258 
"f(0::nat) = (0::nat) \<Longrightarrow> setsum f {Suc 0..k} = setsum f {0..k}" 

1259 
by(simp add:setsum_head_Suc) 

19106
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

1260 

28068  1261 
lemma setsum_shift_lb_Suc0_0_upt: 
1262 
"f(0::nat) = 0 \<Longrightarrow> setsum f {Suc 0..<k} = setsum f {0..<k}" 

1263 
apply(cases k)apply simp 

1264 
apply(simp add:setsum_head_upt_Suc) 

1265 
done 

19022
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

1266 

17149
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
16733
diff
changeset

1267 
subsection {* The formula for geometric sums *} 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
16733
diff
changeset

1268 

e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
16733
diff
changeset

1269 
lemma geometric_sum: 
36307
1732232f9b27
sharpened constraint (c.f. 4e7f5b22dd7d); explicit is better than implicit
haftmann
parents:
35828
diff
changeset

1270 
assumes "x \<noteq> 1" 
1732232f9b27
sharpened constraint (c.f. 4e7f5b22dd7d); explicit is better than implicit
haftmann
parents:
35828
diff
changeset

1271 
shows "(\<Sum>i=0..<n. x ^ i) = (x ^ n  1) / (x  1::'a::field)" 
1732232f9b27
sharpened constraint (c.f. 4e7f5b22dd7d); explicit is better than implicit
haftmann
parents:
35828
diff
changeset

1272 
proof  
1732232f9b27
sharpened constraint (c.f. 4e7f5b22dd7d); explicit is better than implicit
haftmann
parents:
35828
diff
changeset

1273 
from assms obtain y where "y = x  1" and "y \<noteq> 0" by simp_all 
1732232f9b27
sharpened constraint (c.f. 4e7f5b22dd7d); explicit is better than implicit
haftmann
parents:
35828
diff
changeset

1274 
moreover have "(\<Sum>i=0..<n. (y + 1) ^ i) = ((y + 1) ^ n  1) / y" 
1732232f9b27
sharpened constraint (c.f. 4e7f5b22dd7d); explicit is better than implicit
haftmann
parents:
35828
diff
changeset

1275 
proof (induct n) 
1732232f9b27
sharpened constraint (c.f. 4e7f5b22dd7d); explicit is better than implicit
haftmann
parents:
35828
diff
changeset

1276 
case 0 then show ?case by simp 
1732232f9b27
sharpened constraint (c.f. 4e7f5b22dd7d); explicit is better than implicit
haftmann
parents:
35828
diff
changeset

1277 
next 
1732232f9b27
sharpened constraint (c.f. 4e7f5b22dd7d); explicit is better than implicit
haftmann
parents:
35828
diff
changeset

1278 
case (Suc n) 
1732232f9b27
sharpened constraint (c.f. 4e7f5b22dd7d); explicit is better than implicit
haftmann
parents:
35828
diff
changeset

1279 
moreover with `y \<noteq> 0` have "(1 + y) ^ n = (y * inverse y) * (1 + y) ^ n" by simp 
36350  1280 
ultimately show ?case by (simp add: field_simps divide_inverse) 
36307
1732232f9b27
sharpened constraint (c.f. 4e7f5b22dd7d); explicit is better than implicit
haftmann
parents:
35828
diff
changeset

1281 
qed 
1732232f9b27
sharpened constraint (c.f. 4e7f5b22dd7d); explicit is better than implicit
haftmann
parents:
35828
diff
changeset

1282 
ultimately show ?thesis by simp 
1732232f9b27
sharpened constraint (c.f. 4e7f5b22dd7d); explicit is better than implicit
haftmann
parents:
35828
diff
changeset

1283 
qed 
1732232f9b27
sharpened constraint (c.f. 4e7f5b22dd7d); explicit is better than implicit
haftmann
parents:
35828
diff
changeset

1284 

17149
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
16733
diff
changeset

1285 

19469
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

1286 
subsection {* The formula for arithmetic sums *} 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

1287 

47222
1b7c909a6fad
rephrase lemmas about arithmetic series using numeral '2'
huffman
parents:
47108
diff
changeset

1288 
lemma gauss_sum: 
1b7c909a6fad
rephrase lemmas about arithmetic series using numeral '2'
huffman
parents:
47108
diff
changeset

1289 
"(2::'a::comm_semiring_1)*(\<Sum>i\<in>{1..n}. of_nat i) = 
19469
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

1290 
of_nat n*((of_nat n)+1)" 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

1291 
proof (induct n) 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

1292 
case 0 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

1293 
show ?case by simp 
