src/HOL/Set_Interval.thy
author paulson <lp15@cam.ac.uk>
Thu, 29 May 2014 14:39:19 +0100
changeset 57113 7e95523302e6
parent 56949 d1a937cbf858
child 57129 7edb7550663e
permissions -rw-r--r--
New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
47317
432b29a96f61 modernized obsolete old-style theory name with proper new-style underscore
huffman
parents: 47222
diff changeset
     1
(*  Title:      HOL/Set_Interval.thy
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32596
diff changeset
     2
    Author:     Tobias Nipkow
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32596
diff changeset
     3
    Author:     Clemens Ballarin
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32596
diff changeset
     4
    Author:     Jeremy Avigad
8924
c434283b4cfa Added SetInterval
nipkow
parents:
diff changeset
     5
13735
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
     6
lessThan, greaterThan, atLeast, atMost and two-sided intervals
51334
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
     7
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
     8
Modern convention: Ixy stands for an interval where x and y
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
     9
describe the lower and upper bound and x,y : {c,o,i}
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
    10
where c = closed, o = open, i = infinite.
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
    11
Examples: Ico = {_ ..< _} and Ici = {_ ..}
8924
c434283b4cfa Added SetInterval
nipkow
parents:
diff changeset
    12
*)
c434283b4cfa Added SetInterval
nipkow
parents:
diff changeset
    13
14577
dbb95b825244 tuned document;
wenzelm
parents: 14485
diff changeset
    14
header {* Set intervals *}
dbb95b825244 tuned document;
wenzelm
parents: 14485
diff changeset
    15
47317
432b29a96f61 modernized obsolete old-style theory name with proper new-style underscore
huffman
parents: 47222
diff changeset
    16
theory Set_Interval
55088
57c82e01022b moved 'bacc' back to 'Enum' (cf. 744934b818c7) -- reduces baggage loaded by 'Hilbert_Choice'
blanchet
parents: 55085
diff changeset
    17
imports Lattices_Big Nat_Transfer
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15056
diff changeset
    18
begin
8924
c434283b4cfa Added SetInterval
nipkow
parents:
diff changeset
    19
24691
e7f46ee04809 localized { .. } (but only a few thms)
nipkow
parents: 24449
diff changeset
    20
context ord
e7f46ee04809 localized { .. } (but only a few thms)
nipkow
parents: 24449
diff changeset
    21
begin
44008
2e09299ce807 tuned proofs
haftmann
parents: 43657
diff changeset
    22
24691
e7f46ee04809 localized { .. } (but only a few thms)
nipkow
parents: 24449
diff changeset
    23
definition
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32596
diff changeset
    24
  lessThan    :: "'a => 'a set" ("(1{..<_})") where
25062
af5ef0d4d655 global class syntax
haftmann
parents: 24853
diff changeset
    25
  "{..<u} == {x. x < u}"
24691
e7f46ee04809 localized { .. } (but only a few thms)
nipkow
parents: 24449
diff changeset
    26
e7f46ee04809 localized { .. } (but only a few thms)
nipkow
parents: 24449
diff changeset
    27
definition
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32596
diff changeset
    28
  atMost      :: "'a => 'a set" ("(1{.._})") where
25062
af5ef0d4d655 global class syntax
haftmann
parents: 24853
diff changeset
    29
  "{..u} == {x. x \<le> u}"
24691
e7f46ee04809 localized { .. } (but only a few thms)
nipkow
parents: 24449
diff changeset
    30
e7f46ee04809 localized { .. } (but only a few thms)
nipkow
parents: 24449
diff changeset
    31
definition
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32596
diff changeset
    32
  greaterThan :: "'a => 'a set" ("(1{_<..})") where
25062
af5ef0d4d655 global class syntax
haftmann
parents: 24853
diff changeset
    33
  "{l<..} == {x. l<x}"
24691
e7f46ee04809 localized { .. } (but only a few thms)
nipkow
parents: 24449
diff changeset
    34
e7f46ee04809 localized { .. } (but only a few thms)
nipkow
parents: 24449
diff changeset
    35
definition
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32596
diff changeset
    36
  atLeast     :: "'a => 'a set" ("(1{_..})") where
25062
af5ef0d4d655 global class syntax
haftmann
parents: 24853
diff changeset
    37
  "{l..} == {x. l\<le>x}"
24691
e7f46ee04809 localized { .. } (but only a few thms)
nipkow
parents: 24449
diff changeset
    38
e7f46ee04809 localized { .. } (but only a few thms)
nipkow
parents: 24449
diff changeset
    39
definition
25062
af5ef0d4d655 global class syntax
haftmann
parents: 24853
diff changeset
    40
  greaterThanLessThan :: "'a => 'a => 'a set"  ("(1{_<..<_})") where
af5ef0d4d655 global class syntax
haftmann
parents: 24853
diff changeset
    41
  "{l<..<u} == {l<..} Int {..<u}"
24691
e7f46ee04809 localized { .. } (but only a few thms)
nipkow
parents: 24449
diff changeset
    42
e7f46ee04809 localized { .. } (but only a few thms)
nipkow
parents: 24449
diff changeset
    43
definition
25062
af5ef0d4d655 global class syntax
haftmann
parents: 24853
diff changeset
    44
  atLeastLessThan :: "'a => 'a => 'a set"      ("(1{_..<_})") where
af5ef0d4d655 global class syntax
haftmann
parents: 24853
diff changeset
    45
  "{l..<u} == {l..} Int {..<u}"
24691
e7f46ee04809 localized { .. } (but only a few thms)
nipkow
parents: 24449
diff changeset
    46
e7f46ee04809 localized { .. } (but only a few thms)
nipkow
parents: 24449
diff changeset
    47
definition
25062
af5ef0d4d655 global class syntax
haftmann
parents: 24853
diff changeset
    48
  greaterThanAtMost :: "'a => 'a => 'a set"    ("(1{_<.._})") where
af5ef0d4d655 global class syntax
haftmann
parents: 24853
diff changeset
    49
  "{l<..u} == {l<..} Int {..u}"
24691
e7f46ee04809 localized { .. } (but only a few thms)
nipkow
parents: 24449
diff changeset
    50
e7f46ee04809 localized { .. } (but only a few thms)
nipkow
parents: 24449
diff changeset
    51
definition
25062
af5ef0d4d655 global class syntax
haftmann
parents: 24853
diff changeset
    52
  atLeastAtMost :: "'a => 'a => 'a set"        ("(1{_.._})") where
af5ef0d4d655 global class syntax
haftmann
parents: 24853
diff changeset
    53
  "{l..u} == {l..} Int {..u}"
24691
e7f46ee04809 localized { .. } (but only a few thms)
nipkow
parents: 24449
diff changeset
    54
e7f46ee04809 localized { .. } (but only a few thms)
nipkow
parents: 24449
diff changeset
    55
end
8924
c434283b4cfa Added SetInterval
nipkow
parents:
diff changeset
    56
13735
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
    57
15048
11b4dce71d73 more syntax
nipkow
parents: 15047
diff changeset
    58
text{* A note of warning when using @{term"{..<n}"} on type @{typ
11b4dce71d73 more syntax
nipkow
parents: 15047
diff changeset
    59
nat}: it is equivalent to @{term"{0::nat..<n}"} but some lemmas involving
15052
cc562a263609 Added nice latex syntax.
nipkow
parents: 15048
diff changeset
    60
@{term"{m..<n}"} may not exist in @{term"{..<n}"}-form as well. *}
15048
11b4dce71d73 more syntax
nipkow
parents: 15047
diff changeset
    61
14418
b62323c85134 union/intersection over intervals
kleing
parents: 14398
diff changeset
    62
syntax
36364
0e2679025aeb fix syntax precedence declarations for UNION, INTER, SUP, INF
huffman
parents: 36307
diff changeset
    63
  "_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
    64
  "_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
    65
  "_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
    66
  "_INTER_less" :: "'a => 'a => 'b set => 'b set"       ("(3INT _<_./ _)" [0, 0, 10] 10)
14418
b62323c85134 union/intersection over intervals
kleing
parents: 14398
diff changeset
    67
30372
96d508968153 UN syntax fix
nipkow
parents: 30242
diff changeset
    68
syntax (xsymbols)
36364
0e2679025aeb fix syntax precedence declarations for UNION, INTER, SUP, INF
huffman
parents: 36307
diff changeset
    69
  "_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
    70
  "_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
    71
  "_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
    72
  "_INTER_less" :: "'a => 'a => 'b set => 'b set"       ("(3\<Inter> _<_./ _)" [0, 0, 10] 10)
14418
b62323c85134 union/intersection over intervals
kleing
parents: 14398
diff changeset
    73
30372
96d508968153 UN syntax fix
nipkow
parents: 30242
diff changeset
    74
syntax (latex output)
36364
0e2679025aeb fix syntax precedence declarations for UNION, INTER, SUP, INF
huffman
parents: 36307
diff changeset
    75
  "_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
    76
  "_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
    77
  "_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
    78
  "_INTER_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Inter>(00_ < _)/ _)" [0, 0, 10] 10)
14418
b62323c85134 union/intersection over intervals
kleing
parents: 14398
diff changeset
    79
b62323c85134 union/intersection over intervals
kleing
parents: 14398
diff changeset
    80
translations
b62323c85134 union/intersection over intervals
kleing
parents: 14398
diff changeset
    81
  "UN i<=n. A"  == "UN i:{..n}. A"
15045
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
    82
  "UN i<n. A"   == "UN i:{..<n}. A"
14418
b62323c85134 union/intersection over intervals
kleing
parents: 14398
diff changeset
    83
  "INT i<=n. A" == "INT i:{..n}. A"
15045
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
    84
  "INT i<n. A"  == "INT i:{..<n}. A"
14418
b62323c85134 union/intersection over intervals
kleing
parents: 14398
diff changeset
    85
b62323c85134 union/intersection over intervals
kleing
parents: 14398
diff changeset
    86
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
    87
subsection {* Various equivalences *}
13735
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
    88
25062
af5ef0d4d655 global class syntax
haftmann
parents: 24853
diff changeset
    89
lemma (in ord) lessThan_iff [iff]: "(i: lessThan k) = (i<k)"
13850
6d1bb3059818 new logical equivalences
paulson
parents: 13735
diff changeset
    90
by (simp add: lessThan_def)
13735
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
    91
15418
e28853da5df5 removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents: 15402
diff changeset
    92
lemma Compl_lessThan [simp]:
13735
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
    93
    "!!k:: 'a::linorder. -lessThan k = atLeast k"
13850
6d1bb3059818 new logical equivalences
paulson
parents: 13735
diff changeset
    94
apply (auto simp add: lessThan_def atLeast_def)
13735
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
    95
done
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
    96
13850
6d1bb3059818 new logical equivalences
paulson
parents: 13735
diff changeset
    97
lemma single_Diff_lessThan [simp]: "!!k:: 'a::order. {k} - lessThan k = {k}"
6d1bb3059818 new logical equivalences
paulson
parents: 13735
diff changeset
    98
by auto
13735
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
    99
25062
af5ef0d4d655 global class syntax
haftmann
parents: 24853
diff changeset
   100
lemma (in ord) greaterThan_iff [iff]: "(i: greaterThan k) = (k<i)"
13850
6d1bb3059818 new logical equivalences
paulson
parents: 13735
diff changeset
   101
by (simp add: greaterThan_def)
13735
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
   102
15418
e28853da5df5 removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents: 15402
diff changeset
   103
lemma Compl_greaterThan [simp]:
13735
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
   104
    "!!k:: 'a::linorder. -greaterThan k = atMost k"
26072
f65a7fa2da6c <= and < on nat no longer depend on wellfounded relations
haftmann
parents: 25919
diff changeset
   105
  by (auto simp add: greaterThan_def atMost_def)
13735
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
   106
13850
6d1bb3059818 new logical equivalences
paulson
parents: 13735
diff changeset
   107
lemma Compl_atMost [simp]: "!!k:: 'a::linorder. -atMost k = greaterThan k"
6d1bb3059818 new logical equivalences
paulson
parents: 13735
diff changeset
   108
apply (subst Compl_greaterThan [symmetric])
15418
e28853da5df5 removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents: 15402
diff changeset
   109
apply (rule double_complement)
13735
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
   110
done
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
   111
25062
af5ef0d4d655 global class syntax
haftmann
parents: 24853
diff changeset
   112
lemma (in ord) atLeast_iff [iff]: "(i: atLeast k) = (k<=i)"
13850
6d1bb3059818 new logical equivalences
paulson
parents: 13735
diff changeset
   113
by (simp add: atLeast_def)
13735
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
   114
15418
e28853da5df5 removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents: 15402
diff changeset
   115
lemma Compl_atLeast [simp]:
13735
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
   116
    "!!k:: 'a::linorder. -atLeast k = lessThan k"
26072
f65a7fa2da6c <= and < on nat no longer depend on wellfounded relations
haftmann
parents: 25919
diff changeset
   117
  by (auto simp add: lessThan_def atLeast_def)
13735
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
   118
25062
af5ef0d4d655 global class syntax
haftmann
parents: 24853
diff changeset
   119
lemma (in ord) atMost_iff [iff]: "(i: atMost k) = (i<=k)"
13850
6d1bb3059818 new logical equivalences
paulson
parents: 13735
diff changeset
   120
by (simp add: atMost_def)
13735
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
   121
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   122
lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}"
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   123
by (blast intro: order_antisym)
13850
6d1bb3059818 new logical equivalences
paulson
parents: 13735
diff changeset
   124
50999
3de230ed0547 introduce order topology
hoelzl
parents: 50417
diff changeset
   125
lemma (in linorder) lessThan_Int_lessThan: "{ a <..} \<inter> { b <..} = { max a b <..}"
3de230ed0547 introduce order topology
hoelzl
parents: 50417
diff changeset
   126
  by auto
3de230ed0547 introduce order topology
hoelzl
parents: 50417
diff changeset
   127
3de230ed0547 introduce order topology
hoelzl
parents: 50417
diff changeset
   128
lemma (in linorder) greaterThan_Int_greaterThan: "{..< a} \<inter> {..< b} = {..< min a b}"
3de230ed0547 introduce order topology
hoelzl
parents: 50417
diff changeset
   129
  by auto
13850
6d1bb3059818 new logical equivalences
paulson
parents: 13735
diff changeset
   130
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   131
subsection {* Logical Equivalences for Set Inclusion and Equality *}
13850
6d1bb3059818 new logical equivalences
paulson
parents: 13735
diff changeset
   132
6d1bb3059818 new logical equivalences
paulson
parents: 13735
diff changeset
   133
lemma atLeast_subset_iff [iff]:
15418
e28853da5df5 removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents: 15402
diff changeset
   134
     "(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
   135
by (blast intro: order_trans)
13850
6d1bb3059818 new logical equivalences
paulson
parents: 13735
diff changeset
   136
6d1bb3059818 new logical equivalences
paulson
parents: 13735
diff changeset
   137
lemma atLeast_eq_iff [iff]:
15418
e28853da5df5 removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents: 15402
diff changeset
   138
     "(atLeast x = atLeast y) = (x = (y::'a::linorder))"
13850
6d1bb3059818 new logical equivalences
paulson
parents: 13735
diff changeset
   139
by (blast intro: order_antisym order_trans)
6d1bb3059818 new logical equivalences
paulson
parents: 13735
diff changeset
   140
6d1bb3059818 new logical equivalences
paulson
parents: 13735
diff changeset
   141
lemma greaterThan_subset_iff [iff]:
15418
e28853da5df5 removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents: 15402
diff changeset
   142
     "(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
   143
apply (auto simp add: greaterThan_def)
e28853da5df5 removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents: 15402
diff changeset
   144
 apply (subst linorder_not_less [symmetric], blast)
13850
6d1bb3059818 new logical equivalences
paulson
parents: 13735
diff changeset
   145
done
6d1bb3059818 new logical equivalences
paulson
parents: 13735
diff changeset
   146
6d1bb3059818 new logical equivalences
paulson
parents: 13735
diff changeset
   147
lemma greaterThan_eq_iff [iff]:
15418
e28853da5df5 removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents: 15402
diff changeset
   148
     "(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
   149
apply (rule iffI)
e28853da5df5 removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents: 15402
diff changeset
   150
 apply (erule equalityE)
29709
cf8476cc440d fixed proposition slip
haftmann
parents: 29667
diff changeset
   151
 apply simp_all
13850
6d1bb3059818 new logical equivalences
paulson
parents: 13735
diff changeset
   152
done
6d1bb3059818 new logical equivalences
paulson
parents: 13735
diff changeset
   153
15418
e28853da5df5 removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents: 15402
diff changeset
   154
lemma atMost_subset_iff [iff]: "(atMost x \<subseteq> atMost y) = (x \<le> (y::'a::order))"
13850
6d1bb3059818 new logical equivalences
paulson
parents: 13735
diff changeset
   155
by (blast intro: order_trans)
6d1bb3059818 new logical equivalences
paulson
parents: 13735
diff changeset
   156
15418
e28853da5df5 removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents: 15402
diff changeset
   157
lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))"
13850
6d1bb3059818 new logical equivalences
paulson
parents: 13735
diff changeset
   158
by (blast intro: order_antisym order_trans)
6d1bb3059818 new logical equivalences
paulson
parents: 13735
diff changeset
   159
6d1bb3059818 new logical equivalences
paulson
parents: 13735
diff changeset
   160
lemma lessThan_subset_iff [iff]:
15418
e28853da5df5 removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents: 15402
diff changeset
   161
     "(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
   162
apply (auto simp add: lessThan_def)
e28853da5df5 removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents: 15402
diff changeset
   163
 apply (subst linorder_not_less [symmetric], blast)
13850
6d1bb3059818 new logical equivalences
paulson
parents: 13735
diff changeset
   164
done
6d1bb3059818 new logical equivalences
paulson
parents: 13735
diff changeset
   165
6d1bb3059818 new logical equivalences
paulson
parents: 13735
diff changeset
   166
lemma lessThan_eq_iff [iff]:
15418
e28853da5df5 removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents: 15402
diff changeset
   167
     "(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
   168
apply (rule iffI)
e28853da5df5 removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents: 15402
diff changeset
   169
 apply (erule equalityE)
29709
cf8476cc440d fixed proposition slip
haftmann
parents: 29667
diff changeset
   170
 apply simp_all
13735
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
   171
done
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
   172
40703
d1fc454d6735 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents: 39302
diff changeset
   173
lemma lessThan_strict_subset_iff:
d1fc454d6735 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents: 39302
diff changeset
   174
  fixes m n :: "'a::linorder"
d1fc454d6735 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents: 39302
diff changeset
   175
  shows "{..<m} < {..<n} \<longleftrightarrow> m < n"
d1fc454d6735 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents: 39302
diff changeset
   176
  by (metis leD lessThan_subset_iff linorder_linear not_less_iff_gr_or_eq psubset_eq)
13735
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
   177
13850
6d1bb3059818 new logical equivalences
paulson
parents: 13735
diff changeset
   178
subsection {*Two-sided intervals*}
13735
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
   179
24691
e7f46ee04809 localized { .. } (but only a few thms)
nipkow
parents: 24449
diff changeset
   180
context ord
e7f46ee04809 localized { .. } (but only a few thms)
nipkow
parents: 24449
diff changeset
   181
begin
e7f46ee04809 localized { .. } (but only a few thms)
nipkow
parents: 24449
diff changeset
   182
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 53374
diff changeset
   183
lemma greaterThanLessThan_iff [simp]:
25062
af5ef0d4d655 global class syntax
haftmann
parents: 24853
diff changeset
   184
  "(i : {l<..<u}) = (l < i & i < u)"
13735
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
   185
by (simp add: greaterThanLessThan_def)
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
   186
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 53374
diff changeset
   187
lemma atLeastLessThan_iff [simp]:
25062
af5ef0d4d655 global class syntax
haftmann
parents: 24853
diff changeset
   188
  "(i : {l..<u}) = (l <= i & i < u)"
13735
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
   189
by (simp add: atLeastLessThan_def)
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
   190
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 53374
diff changeset
   191
lemma greaterThanAtMost_iff [simp]:
25062
af5ef0d4d655 global class syntax
haftmann
parents: 24853
diff changeset
   192
  "(i : {l<..u}) = (l < i & i <= u)"
13735
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
   193
by (simp add: greaterThanAtMost_def)
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
   194
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 53374
diff changeset
   195
lemma atLeastAtMost_iff [simp]:
25062
af5ef0d4d655 global class syntax
haftmann
parents: 24853
diff changeset
   196
  "(i : {l..u}) = (l <= i & i <= u)"
13735
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
   197
by (simp add: atLeastAtMost_def)
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
   198
32436
10cd49e0c067 Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
nipkow
parents: 32408
diff changeset
   199
text {* The above four lemmas could be declared as iffs. Unfortunately this
52729
412c9e0381a1 factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents: 52380
diff changeset
   200
breaks many proofs. Since it only helps blast, it is better to leave them
412c9e0381a1 factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents: 52380
diff changeset
   201
alone. *}
32436
10cd49e0c067 Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
nipkow
parents: 32408
diff changeset
   202
50999
3de230ed0547 introduce order topology
hoelzl
parents: 50417
diff changeset
   203
lemma greaterThanLessThan_eq: "{ a <..< b} = { a <..} \<inter> {..< b }"
3de230ed0547 introduce order topology
hoelzl
parents: 50417
diff changeset
   204
  by auto
3de230ed0547 introduce order topology
hoelzl
parents: 50417
diff changeset
   205
24691
e7f46ee04809 localized { .. } (but only a few thms)
nipkow
parents: 24449
diff changeset
   206
end
13735
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
   207
32400
6c62363cf0d7 new lemmas
nipkow
parents: 32006
diff changeset
   208
subsubsection{* Emptyness, singletons, subset *}
15554
03d4347b071d integrated Jeremy's FiniteLib
nipkow
parents: 15542
diff changeset
   209
24691
e7f46ee04809 localized { .. } (but only a few thms)
nipkow
parents: 24449
diff changeset
   210
context order
e7f46ee04809 localized { .. } (but only a few thms)
nipkow
parents: 24449
diff changeset
   211
begin
15554
03d4347b071d integrated Jeremy's FiniteLib
nipkow
parents: 15542
diff changeset
   212
32400
6c62363cf0d7 new lemmas
nipkow
parents: 32006
diff changeset
   213
lemma atLeastatMost_empty[simp]:
6c62363cf0d7 new lemmas
nipkow
parents: 32006
diff changeset
   214
  "b < a \<Longrightarrow> {a..b} = {}"
6c62363cf0d7 new lemmas
nipkow
parents: 32006
diff changeset
   215
by(auto simp: atLeastAtMost_def atLeast_def atMost_def)
6c62363cf0d7 new lemmas
nipkow
parents: 32006
diff changeset
   216
6c62363cf0d7 new lemmas
nipkow
parents: 32006
diff changeset
   217
lemma atLeastatMost_empty_iff[simp]:
6c62363cf0d7 new lemmas
nipkow
parents: 32006
diff changeset
   218
  "{a..b} = {} \<longleftrightarrow> (~ a <= b)"
6c62363cf0d7 new lemmas
nipkow
parents: 32006
diff changeset
   219
by auto (blast intro: order_trans)
6c62363cf0d7 new lemmas
nipkow
parents: 32006
diff changeset
   220
6c62363cf0d7 new lemmas
nipkow
parents: 32006
diff changeset
   221
lemma atLeastatMost_empty_iff2[simp]:
6c62363cf0d7 new lemmas
nipkow
parents: 32006
diff changeset
   222
  "{} = {a..b} \<longleftrightarrow> (~ a <= b)"
6c62363cf0d7 new lemmas
nipkow
parents: 32006
diff changeset
   223
by auto (blast intro: order_trans)
6c62363cf0d7 new lemmas
nipkow
parents: 32006
diff changeset
   224
6c62363cf0d7 new lemmas
nipkow
parents: 32006
diff changeset
   225
lemma atLeastLessThan_empty[simp]:
6c62363cf0d7 new lemmas
nipkow
parents: 32006
diff changeset
   226
  "b <= a \<Longrightarrow> {a..<b} = {}"
6c62363cf0d7 new lemmas
nipkow
parents: 32006
diff changeset
   227
by(auto simp: atLeastLessThan_def)
24691
e7f46ee04809 localized { .. } (but only a few thms)
nipkow
parents: 24449
diff changeset
   228
32400
6c62363cf0d7 new lemmas
nipkow
parents: 32006
diff changeset
   229
lemma atLeastLessThan_empty_iff[simp]:
6c62363cf0d7 new lemmas
nipkow
parents: 32006
diff changeset
   230
  "{a..<b} = {} \<longleftrightarrow> (~ a < b)"
6c62363cf0d7 new lemmas
nipkow
parents: 32006
diff changeset
   231
by auto (blast intro: le_less_trans)
6c62363cf0d7 new lemmas
nipkow
parents: 32006
diff changeset
   232
6c62363cf0d7 new lemmas
nipkow
parents: 32006
diff changeset
   233
lemma atLeastLessThan_empty_iff2[simp]:
6c62363cf0d7 new lemmas
nipkow
parents: 32006
diff changeset
   234
  "{} = {a..<b} \<longleftrightarrow> (~ a < b)"
6c62363cf0d7 new lemmas
nipkow
parents: 32006
diff changeset
   235
by auto (blast intro: le_less_trans)
15554
03d4347b071d integrated Jeremy's FiniteLib
nipkow
parents: 15542
diff changeset
   236
32400
6c62363cf0d7 new lemmas
nipkow
parents: 32006
diff changeset
   237
lemma greaterThanAtMost_empty[simp]: "l \<le> k ==> {k<..l} = {}"
17719
2e75155c5ed5 Added a few lemmas
nipkow
parents: 17149
diff changeset
   238
by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def)
2e75155c5ed5 Added a few lemmas
nipkow
parents: 17149
diff changeset
   239
32400
6c62363cf0d7 new lemmas
nipkow
parents: 32006
diff changeset
   240
lemma greaterThanAtMost_empty_iff[simp]: "{k<..l} = {} \<longleftrightarrow> ~ k < l"
6c62363cf0d7 new lemmas
nipkow
parents: 32006
diff changeset
   241
by auto (blast intro: less_le_trans)
6c62363cf0d7 new lemmas
nipkow
parents: 32006
diff changeset
   242
6c62363cf0d7 new lemmas
nipkow
parents: 32006
diff changeset
   243
lemma greaterThanAtMost_empty_iff2[simp]: "{} = {k<..l} \<longleftrightarrow> ~ k < l"
6c62363cf0d7 new lemmas
nipkow
parents: 32006
diff changeset
   244
by auto (blast intro: less_le_trans)
6c62363cf0d7 new lemmas
nipkow
parents: 32006
diff changeset
   245
29709
cf8476cc440d fixed proposition slip
haftmann
parents: 29667
diff changeset
   246
lemma greaterThanLessThan_empty[simp]:"l \<le> k ==> {k<..<l} = {}"
17719
2e75155c5ed5 Added a few lemmas
nipkow
parents: 17149
diff changeset
   247
by(auto simp:greaterThanLessThan_def greaterThan_def lessThan_def)
2e75155c5ed5 Added a few lemmas
nipkow
parents: 17149
diff changeset
   248
25062
af5ef0d4d655 global class syntax
haftmann
parents: 24853
diff changeset
   249
lemma atLeastAtMost_singleton [simp]: "{a..a} = {a}"
24691
e7f46ee04809 localized { .. } (but only a few thms)
nipkow
parents: 24449
diff changeset
   250
by (auto simp add: atLeastAtMost_def atMost_def atLeast_def)
e7f46ee04809 localized { .. } (but only a few thms)
nipkow
parents: 24449
diff changeset
   251
36846
0f67561ed5a6 Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
hoelzl
parents: 36755
diff changeset
   252
lemma atLeastAtMost_singleton': "a = b \<Longrightarrow> {a .. b} = {a}" by simp
0f67561ed5a6 Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
hoelzl
parents: 36755
diff changeset
   253
32400
6c62363cf0d7 new lemmas
nipkow
parents: 32006
diff changeset
   254
lemma atLeastatMost_subset_iff[simp]:
6c62363cf0d7 new lemmas
nipkow
parents: 32006
diff changeset
   255
  "{a..b} <= {c..d} \<longleftrightarrow> (~ a <= b) | c <= a & b <= d"
6c62363cf0d7 new lemmas
nipkow
parents: 32006
diff changeset
   256
unfolding atLeastAtMost_def atLeast_def atMost_def
6c62363cf0d7 new lemmas
nipkow
parents: 32006
diff changeset
   257
by (blast intro: order_trans)
6c62363cf0d7 new lemmas
nipkow
parents: 32006
diff changeset
   258
6c62363cf0d7 new lemmas
nipkow
parents: 32006
diff changeset
   259
lemma atLeastatMost_psubset_iff:
6c62363cf0d7 new lemmas
nipkow
parents: 32006
diff changeset
   260
  "{a..b} < {c..d} \<longleftrightarrow>
6c62363cf0d7 new lemmas
nipkow
parents: 32006
diff changeset
   261
   ((~ 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
   262
by(simp add: psubset_eq set_eq_iff less_le_not_le)(blast intro: order_trans)
32400
6c62363cf0d7 new lemmas
nipkow
parents: 32006
diff changeset
   263
51334
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   264
lemma Icc_eq_Icc[simp]:
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   265
  "{l..h} = {l'..h'} = (l=l' \<and> h=h' \<or> \<not> l\<le>h \<and> \<not> l'\<le>h')"
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   266
by(simp add: order_class.eq_iff)(auto intro: order_trans)
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   267
36846
0f67561ed5a6 Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
hoelzl
parents: 36755
diff changeset
   268
lemma atLeastAtMost_singleton_iff[simp]:
0f67561ed5a6 Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
hoelzl
parents: 36755
diff changeset
   269
  "{a .. b} = {c} \<longleftrightarrow> a = b \<and> b = c"
0f67561ed5a6 Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
hoelzl
parents: 36755
diff changeset
   270
proof
0f67561ed5a6 Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
hoelzl
parents: 36755
diff changeset
   271
  assume "{a..b} = {c}"
53374
a14d2a854c02 tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents: 53216
diff changeset
   272
  hence *: "\<not> (\<not> a \<le> b)" unfolding atLeastatMost_empty_iff[symmetric] by simp
a14d2a854c02 tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents: 53216
diff changeset
   273
  with `{a..b} = {c}` have "c \<le> a \<and> b \<le> c" by auto
a14d2a854c02 tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents: 53216
diff changeset
   274
  with * show "a = b \<and> b = c" by auto
36846
0f67561ed5a6 Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
hoelzl
parents: 36755
diff changeset
   275
qed simp
0f67561ed5a6 Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
hoelzl
parents: 36755
diff changeset
   276
51334
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   277
lemma Icc_subset_Ici_iff[simp]:
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   278
  "{l..h} \<subseteq> {l'..} = (~ l\<le>h \<or> l\<ge>l')"
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   279
by(auto simp: subset_eq intro: order_trans)
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   280
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   281
lemma Icc_subset_Iic_iff[simp]:
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   282
  "{l..h} \<subseteq> {..h'} = (~ l\<le>h \<or> h\<le>h')"
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   283
by(auto simp: subset_eq intro: order_trans)
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   284
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   285
lemma not_Ici_eq_empty[simp]: "{l..} \<noteq> {}"
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   286
by(auto simp: set_eq_iff)
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   287
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   288
lemma not_Iic_eq_empty[simp]: "{..h} \<noteq> {}"
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   289
by(auto simp: set_eq_iff)
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   290
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   291
lemmas not_empty_eq_Ici_eq_empty[simp] = not_Ici_eq_empty[symmetric]
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   292
lemmas not_empty_eq_Iic_eq_empty[simp] = not_Iic_eq_empty[symmetric]
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   293
24691
e7f46ee04809 localized { .. } (but only a few thms)
nipkow
parents: 24449
diff changeset
   294
end
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   295
51334
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   296
context no_top
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   297
begin
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   298
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   299
(* also holds for no_bot but no_top should suffice *)
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   300
lemma not_UNIV_le_Icc[simp]: "\<not> UNIV \<subseteq> {l..h}"
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   301
using gt_ex[of h] by(auto simp: subset_eq less_le_not_le)
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   302
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   303
lemma not_UNIV_le_Iic[simp]: "\<not> UNIV \<subseteq> {..h}"
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   304
using gt_ex[of h] by(auto simp: subset_eq less_le_not_le)
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   305
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   306
lemma not_Ici_le_Icc[simp]: "\<not> {l..} \<subseteq> {l'..h'}"
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   307
using gt_ex[of h']
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   308
by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans)
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   309
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   310
lemma not_Ici_le_Iic[simp]: "\<not> {l..} \<subseteq> {..h'}"
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   311
using gt_ex[of h']
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   312
by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans)
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   313
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   314
end
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   315
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   316
context no_bot
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   317
begin
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   318
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   319
lemma not_UNIV_le_Ici[simp]: "\<not> UNIV \<subseteq> {l..}"
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   320
using lt_ex[of l] by(auto simp: subset_eq less_le_not_le)
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   321
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   322
lemma not_Iic_le_Icc[simp]: "\<not> {..h} \<subseteq> {l'..h'}"
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   323
using lt_ex[of l']
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   324
by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans)
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   325
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   326
lemma not_Iic_le_Ici[simp]: "\<not> {..h} \<subseteq> {l'..}"
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   327
using lt_ex[of l']
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   328
by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans)
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   329
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   330
end
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   331
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   332
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   333
context no_top
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   334
begin
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   335
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   336
(* also holds for no_bot but no_top should suffice *)
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   337
lemma not_UNIV_eq_Icc[simp]: "\<not> UNIV = {l'..h'}"
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   338
using gt_ex[of h'] by(auto simp: set_eq_iff  less_le_not_le)
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   339
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   340
lemmas not_Icc_eq_UNIV[simp] = not_UNIV_eq_Icc[symmetric]
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   341
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   342
lemma not_UNIV_eq_Iic[simp]: "\<not> UNIV = {..h'}"
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   343
using gt_ex[of h'] by(auto simp: set_eq_iff  less_le_not_le)
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   344
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   345
lemmas not_Iic_eq_UNIV[simp] = not_UNIV_eq_Iic[symmetric]
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   346
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   347
lemma not_Icc_eq_Ici[simp]: "\<not> {l..h} = {l'..}"
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   348
unfolding atLeastAtMost_def using not_Ici_le_Iic[of l'] by blast
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   349
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   350
lemmas not_Ici_eq_Icc[simp] = not_Icc_eq_Ici[symmetric]
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   351
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   352
(* also holds for no_bot but no_top should suffice *)
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   353
lemma not_Iic_eq_Ici[simp]: "\<not> {..h} = {l'..}"
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   354
using not_Ici_le_Iic[of l' h] by blast
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   355
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   356
lemmas not_Ici_eq_Iic[simp] = not_Iic_eq_Ici[symmetric]
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   357
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   358
end
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   359
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   360
context no_bot
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   361
begin
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   362
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   363
lemma not_UNIV_eq_Ici[simp]: "\<not> UNIV = {l'..}"
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   364
using lt_ex[of l'] by(auto simp: set_eq_iff  less_le_not_le)
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   365
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   366
lemmas not_Ici_eq_UNIV[simp] = not_UNIV_eq_Ici[symmetric]
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   367
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   368
lemma not_Icc_eq_Iic[simp]: "\<not> {l..h} = {..h'}"
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   369
unfolding atLeastAtMost_def using not_Iic_le_Ici[of h'] by blast
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   370
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   371
lemmas not_Iic_eq_Icc[simp] = not_Icc_eq_Iic[symmetric]
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   372
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   373
end
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   374
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   375
53216
ad2e09c30aa8 renamed inner_dense_linorder to dense_linorder
hoelzl
parents: 52729
diff changeset
   376
context dense_linorder
42891
e2f473671937 simp rules for empty intervals on dense linear order
hoelzl
parents: 40703
diff changeset
   377
begin
e2f473671937 simp rules for empty intervals on dense linear order
hoelzl
parents: 40703
diff changeset
   378
e2f473671937 simp rules for empty intervals on dense linear order
hoelzl
parents: 40703
diff changeset
   379
lemma greaterThanLessThan_empty_iff[simp]:
e2f473671937 simp rules for empty intervals on dense linear order
hoelzl
parents: 40703
diff changeset
   380
  "{ a <..< b } = {} \<longleftrightarrow> b \<le> a"
e2f473671937 simp rules for empty intervals on dense linear order
hoelzl
parents: 40703
diff changeset
   381
  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
   382
e2f473671937 simp rules for empty intervals on dense linear order
hoelzl
parents: 40703
diff changeset
   383
lemma greaterThanLessThan_empty_iff2[simp]:
e2f473671937 simp rules for empty intervals on dense linear order
hoelzl
parents: 40703
diff changeset
   384
  "{} = { a <..< b } \<longleftrightarrow> b \<le> a"
e2f473671937 simp rules for empty intervals on dense linear order
hoelzl
parents: 40703
diff changeset
   385
  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
   386
42901
e35cf2b25f48 equations for subsets of atLeastAtMost
hoelzl
parents: 42891
diff changeset
   387
lemma atLeastLessThan_subseteq_atLeastAtMost_iff:
e35cf2b25f48 equations for subsets of atLeastAtMost
hoelzl
parents: 42891
diff changeset
   388
  "{a ..< b} \<subseteq> { c .. d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b \<le> d)"
e35cf2b25f48 equations for subsets of atLeastAtMost
hoelzl
parents: 42891
diff changeset
   389
  using dense[of "max a d" "b"]
e35cf2b25f48 equations for subsets of atLeastAtMost
hoelzl
parents: 42891
diff changeset
   390
  by (force simp: subset_eq Ball_def not_less[symmetric])
e35cf2b25f48 equations for subsets of atLeastAtMost
hoelzl
parents: 42891
diff changeset
   391
e35cf2b25f48 equations for subsets of atLeastAtMost
hoelzl
parents: 42891
diff changeset
   392
lemma greaterThanAtMost_subseteq_atLeastAtMost_iff:
e35cf2b25f48 equations for subsets of atLeastAtMost
hoelzl
parents: 42891
diff changeset
   393
  "{a <.. b} \<subseteq> { c .. d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b \<le> d)"
e35cf2b25f48 equations for subsets of atLeastAtMost
hoelzl
parents: 42891
diff changeset
   394
  using dense[of "a" "min c b"]
e35cf2b25f48 equations for subsets of atLeastAtMost
hoelzl
parents: 42891
diff changeset
   395
  by (force simp: subset_eq Ball_def not_less[symmetric])
e35cf2b25f48 equations for subsets of atLeastAtMost
hoelzl
parents: 42891
diff changeset
   396
e35cf2b25f48 equations for subsets of atLeastAtMost
hoelzl
parents: 42891
diff changeset
   397
lemma greaterThanLessThan_subseteq_atLeastAtMost_iff:
e35cf2b25f48 equations for subsets of atLeastAtMost
hoelzl
parents: 42891
diff changeset
   398
  "{a <..< b} \<subseteq> { c .. d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b \<le> d)"
e35cf2b25f48 equations for subsets of atLeastAtMost
hoelzl
parents: 42891
diff changeset
   399
  using dense[of "a" "min c b"] dense[of "max a d" "b"]
e35cf2b25f48 equations for subsets of atLeastAtMost
hoelzl
parents: 42891
diff changeset
   400
  by (force simp: subset_eq Ball_def not_less[symmetric])
e35cf2b25f48 equations for subsets of atLeastAtMost
hoelzl
parents: 42891
diff changeset
   401
43657
537ea3846f64 equalities of subsets of atLeastLessThan
hoelzl
parents: 43157
diff changeset
   402
lemma atLeastAtMost_subseteq_atLeastLessThan_iff:
537ea3846f64 equalities of subsets of atLeastLessThan
hoelzl
parents: 43157
diff changeset
   403
  "{a .. b} \<subseteq> { c ..< d } \<longleftrightarrow> (a \<le> b \<longrightarrow> c \<le> a \<and> b < d)"
537ea3846f64 equalities of subsets of atLeastLessThan
hoelzl
parents: 43157
diff changeset
   404
  using dense[of "max a d" "b"]
537ea3846f64 equalities of subsets of atLeastLessThan
hoelzl
parents: 43157
diff changeset
   405
  by (force simp: subset_eq Ball_def not_less[symmetric])
537ea3846f64 equalities of subsets of atLeastLessThan
hoelzl
parents: 43157
diff changeset
   406
537ea3846f64 equalities of subsets of atLeastLessThan
hoelzl
parents: 43157
diff changeset
   407
lemma greaterThanAtMost_subseteq_atLeastLessThan_iff:
537ea3846f64 equalities of subsets of atLeastLessThan
hoelzl
parents: 43157
diff changeset
   408
  "{a <.. b} \<subseteq> { c ..< d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b < d)"
537ea3846f64 equalities of subsets of atLeastLessThan
hoelzl
parents: 43157
diff changeset
   409
  using dense[of "a" "min c b"]
537ea3846f64 equalities of subsets of atLeastLessThan
hoelzl
parents: 43157
diff changeset
   410
  by (force simp: subset_eq Ball_def not_less[symmetric])
537ea3846f64 equalities of subsets of atLeastLessThan
hoelzl
parents: 43157
diff changeset
   411
537ea3846f64 equalities of subsets of atLeastLessThan
hoelzl
parents: 43157
diff changeset
   412
lemma greaterThanLessThan_subseteq_atLeastLessThan_iff:
537ea3846f64 equalities of subsets of atLeastLessThan
hoelzl
parents: 43157
diff changeset
   413
  "{a <..< b} \<subseteq> { c ..< d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b \<le> d)"
537ea3846f64 equalities of subsets of atLeastLessThan
hoelzl
parents: 43157
diff changeset
   414
  using dense[of "a" "min c b"] dense[of "max a d" "b"]
537ea3846f64 equalities of subsets of atLeastLessThan
hoelzl
parents: 43157
diff changeset
   415
  by (force simp: subset_eq Ball_def not_less[symmetric])
537ea3846f64 equalities of subsets of atLeastLessThan
hoelzl
parents: 43157
diff changeset
   416
56328
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   417
lemma greaterThanLessThan_subseteq_greaterThanAtMost_iff:
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   418
  "{a <..< b} \<subseteq> { c <.. d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b \<le> d)"
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   419
  using dense[of "a" "min c b"] dense[of "max a d" "b"]
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   420
  by (force simp: subset_eq Ball_def not_less[symmetric])
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   421
42891
e2f473671937 simp rules for empty intervals on dense linear order
hoelzl
parents: 40703
diff changeset
   422
end
e2f473671937 simp rules for empty intervals on dense linear order
hoelzl
parents: 40703
diff changeset
   423
51329
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   424
context no_top
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   425
begin
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   426
51334
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   427
lemma greaterThan_non_empty[simp]: "{x <..} \<noteq> {}"
51329
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   428
  using gt_ex[of x] by auto
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   429
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   430
end
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   431
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   432
context no_bot
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   433
begin
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   434
51334
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   435
lemma lessThan_non_empty[simp]: "{..< x} \<noteq> {}"
51329
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   436
  using lt_ex[of x] by auto
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   437
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   438
end
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   439
32408
a1a85b0a26f7 new interval lemma
nipkow
parents: 32400
diff changeset
   440
lemma (in linorder) atLeastLessThan_subset_iff:
a1a85b0a26f7 new interval lemma
nipkow
parents: 32400
diff changeset
   441
  "{a..<b} <= {c..<d} \<Longrightarrow> b <= a | c<=a & b<=d"
a1a85b0a26f7 new interval lemma
nipkow
parents: 32400
diff changeset
   442
apply (auto simp:subset_eq Ball_def)
a1a85b0a26f7 new interval lemma
nipkow
parents: 32400
diff changeset
   443
apply(frule_tac x=a in spec)
a1a85b0a26f7 new interval lemma
nipkow
parents: 32400
diff changeset
   444
apply(erule_tac x=d in allE)
a1a85b0a26f7 new interval lemma
nipkow
parents: 32400
diff changeset
   445
apply (simp add: less_imp_le)
a1a85b0a26f7 new interval lemma
nipkow
parents: 32400
diff changeset
   446
done
a1a85b0a26f7 new interval lemma
nipkow
parents: 32400
diff changeset
   447
40703
d1fc454d6735 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents: 39302
diff changeset
   448
lemma atLeastLessThan_inj:
d1fc454d6735 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents: 39302
diff changeset
   449
  fixes a b c d :: "'a::linorder"
d1fc454d6735 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents: 39302
diff changeset
   450
  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 HOL-image.
hoelzl
parents: 39302
diff changeset
   451
  shows "a = c" "b = d"
d1fc454d6735 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents: 39302
diff changeset
   452
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 HOL-image.
hoelzl
parents: 39302
diff changeset
   453
d1fc454d6735 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents: 39302
diff changeset
   454
lemma atLeastLessThan_eq_iff:
d1fc454d6735 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents: 39302
diff changeset
   455
  fixes a b c d :: "'a::linorder"
d1fc454d6735 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents: 39302
diff changeset
   456
  assumes "a < b" "c < d"
d1fc454d6735 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents: 39302
diff changeset
   457
  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 HOL-image.
hoelzl
parents: 39302
diff changeset
   458
  using atLeastLessThan_inj assms by auto
d1fc454d6735 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents: 39302
diff changeset
   459
52729
412c9e0381a1 factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents: 52380
diff changeset
   460
lemma (in order_bot) atLeast_eq_UNIV_iff: "{x..} = UNIV \<longleftrightarrow> x = bot"
51334
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   461
by (auto simp: set_eq_iff intro: le_bot)
51328
d63ec23c9125 move auxiliary lemmas from Library/Extended_Reals to HOL image
hoelzl
parents: 51152
diff changeset
   462
52729
412c9e0381a1 factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents: 52380
diff changeset
   463
lemma (in order_top) atMost_eq_UNIV_iff: "{..x} = UNIV \<longleftrightarrow> x = top"
51334
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   464
by (auto simp: set_eq_iff intro: top_le)
51328
d63ec23c9125 move auxiliary lemmas from Library/Extended_Reals to HOL image
hoelzl
parents: 51152
diff changeset
   465
51334
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   466
lemma (in bounded_lattice) atLeastAtMost_eq_UNIV_iff:
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   467
  "{x..y} = UNIV \<longleftrightarrow> (x = bot \<and> y = top)"
fd531bd984d8 more lemmas about intervals
nipkow
parents: 51329
diff changeset
   468
by (auto simp: set_eq_iff intro: top_le le_bot)
51328
d63ec23c9125 move auxiliary lemmas from Library/Extended_Reals to HOL image
hoelzl
parents: 51152
diff changeset
   469
56949
d1a937cbf858 clean up Lebesgue integration
hoelzl
parents: 56480
diff changeset
   470
lemma Iio_eq_empty_iff: "{..< n::'a::{linorder, order_bot}} = {} \<longleftrightarrow> n = bot"
d1a937cbf858 clean up Lebesgue integration
hoelzl
parents: 56480
diff changeset
   471
  by (auto simp: set_eq_iff not_less le_bot)
d1a937cbf858 clean up Lebesgue integration
hoelzl
parents: 56480
diff changeset
   472
d1a937cbf858 clean up Lebesgue integration
hoelzl
parents: 56480
diff changeset
   473
lemma Iio_eq_empty_iff_nat: "{..< n::nat} = {} \<longleftrightarrow> n = 0"
d1a937cbf858 clean up Lebesgue integration
hoelzl
parents: 56480
diff changeset
   474
  by (simp add: Iio_eq_empty_iff bot_nat_def)
d1a937cbf858 clean up Lebesgue integration
hoelzl
parents: 56480
diff changeset
   475
51328
d63ec23c9125 move auxiliary lemmas from Library/Extended_Reals to HOL image
hoelzl
parents: 51152
diff changeset
   476
56328
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   477
subsection {* Infinite intervals *}
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   478
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   479
context dense_linorder
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   480
begin
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   481
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   482
lemma infinite_Ioo:
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   483
  assumes "a < b"
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   484
  shows "\<not> finite {a<..<b}"
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   485
proof
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   486
  assume fin: "finite {a<..<b}"
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   487
  moreover have ne: "{a<..<b} \<noteq> {}"
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   488
    using `a < b` by auto
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   489
  ultimately have "a < Max {a <..< b}" "Max {a <..< b} < b"
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   490
    using Max_in[of "{a <..< b}"] by auto
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   491
  then obtain x where "Max {a <..< b} < x" "x < b"
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   492
    using dense[of "Max {a<..<b}" b] by auto
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   493
  then have "x \<in> {a <..< b}"
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   494
    using `a < Max {a <..< b}` by auto
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   495
  then have "x \<le> Max {a <..< b}"
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   496
    using fin by auto
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   497
  with `Max {a <..< b} < x` show False by auto
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   498
qed
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   499
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   500
lemma infinite_Icc: "a < b \<Longrightarrow> \<not> finite {a .. b}"
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   501
  using greaterThanLessThan_subseteq_atLeastAtMost_iff[of a b a b] infinite_Ioo[of a b]
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   502
  by (auto dest: finite_subset)
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   503
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   504
lemma infinite_Ico: "a < b \<Longrightarrow> \<not> finite {a ..< b}"
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   505
  using greaterThanLessThan_subseteq_atLeastLessThan_iff[of a b a b] infinite_Ioo[of a b]
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   506
  by (auto dest: finite_subset)
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   507
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   508
lemma infinite_Ioc: "a < b \<Longrightarrow> \<not> finite {a <.. b}"
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   509
  using greaterThanLessThan_subseteq_greaterThanAtMost_iff[of a b a b] infinite_Ioo[of a b]
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   510
  by (auto dest: finite_subset)
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   511
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   512
end
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   513
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   514
lemma infinite_Iio: "\<not> finite {..< a :: 'a :: {no_bot, linorder}}"
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   515
proof
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   516
  assume "finite {..< a}"
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   517
  then have *: "\<And>x. x < a \<Longrightarrow> Min {..< a} \<le> x"
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   518
    by auto
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   519
  obtain x where "x < a"
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   520
    using lt_ex by auto
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   521
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   522
  obtain y where "y < Min {..< a}"
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   523
    using lt_ex by auto
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   524
  also have "Min {..< a} \<le> x"
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   525
    using `x < a` by fact
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   526
  also note `x < a`
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   527
  finally have "Min {..< a} \<le> y"
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   528
    by fact
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   529
  with `y < Min {..< a}` show False by auto
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   530
qed
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   531
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   532
lemma infinite_Iic: "\<not> finite {.. a :: 'a :: {no_bot, linorder}}"
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   533
  using infinite_Iio[of a] finite_subset[of "{..< a}" "{.. a}"]
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   534
  by (auto simp: subset_eq less_imp_le)
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   535
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   536
lemma infinite_Ioi: "\<not> finite {a :: 'a :: {no_top, linorder} <..}"
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   537
proof
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   538
  assume "finite {a <..}"
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   539
  then have *: "\<And>x. a < x \<Longrightarrow> x \<le> Max {a <..}"
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   540
    by auto
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   541
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   542
  obtain y where "Max {a <..} < y"
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   543
    using gt_ex by auto
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   544
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   545
  obtain x where "a < x"
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   546
    using gt_ex by auto
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   547
  also then have "x \<le> Max {a <..}"
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   548
    by fact
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   549
  also note `Max {a <..} < y`
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   550
  finally have "y \<le> Max { a <..}"
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   551
    by fact
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   552
  with `Max {a <..} < y` show False by auto
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   553
qed
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   554
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   555
lemma infinite_Ici: "\<not> finite {a :: 'a :: {no_top, linorder} ..}"
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   556
  using infinite_Ioi[of a] finite_subset[of "{a <..}" "{a ..}"]
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   557
  by (auto simp: subset_eq less_imp_le)
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   558
32456
341c83339aeb tuned the simp rules for Int involving insert and intervals.
nipkow
parents: 32436
diff changeset
   559
subsubsection {* Intersection *}
341c83339aeb tuned the simp rules for Int involving insert and intervals.
nipkow
parents: 32436
diff changeset
   560
341c83339aeb tuned the simp rules for Int involving insert and intervals.
nipkow
parents: 32436
diff changeset
   561
context linorder
341c83339aeb tuned the simp rules for Int involving insert and intervals.
nipkow
parents: 32436
diff changeset
   562
begin
341c83339aeb tuned the simp rules for Int involving insert and intervals.
nipkow
parents: 32436
diff changeset
   563
341c83339aeb tuned the simp rules for Int involving insert and intervals.
nipkow
parents: 32436
diff changeset
   564
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
   565
by auto
341c83339aeb tuned the simp rules for Int involving insert and intervals.
nipkow
parents: 32436
diff changeset
   566
341c83339aeb tuned the simp rules for Int involving insert and intervals.
nipkow
parents: 32436
diff changeset
   567
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
   568
by auto
341c83339aeb tuned the simp rules for Int involving insert and intervals.
nipkow
parents: 32436
diff changeset
   569
341c83339aeb tuned the simp rules for Int involving insert and intervals.
nipkow
parents: 32436
diff changeset
   570
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
   571
by auto
341c83339aeb tuned the simp rules for Int involving insert and intervals.
nipkow
parents: 32436
diff changeset
   572
341c83339aeb tuned the simp rules for Int involving insert and intervals.
nipkow
parents: 32436
diff changeset
   573
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
   574
by auto
341c83339aeb tuned the simp rules for Int involving insert and intervals.
nipkow
parents: 32436
diff changeset
   575
341c83339aeb tuned the simp rules for Int involving insert and intervals.
nipkow
parents: 32436
diff changeset
   576
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
   577
by auto
341c83339aeb tuned the simp rules for Int involving insert and intervals.
nipkow
parents: 32436
diff changeset
   578
341c83339aeb tuned the simp rules for Int involving insert and intervals.
nipkow
parents: 32436
diff changeset
   579
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
   580
by auto
341c83339aeb tuned the simp rules for Int involving insert and intervals.
nipkow
parents: 32436
diff changeset
   581
341c83339aeb tuned the simp rules for Int involving insert and intervals.
nipkow
parents: 32436
diff changeset
   582
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
   583
by auto
341c83339aeb tuned the simp rules for Int involving insert and intervals.
nipkow
parents: 32436
diff changeset
   584
341c83339aeb tuned the simp rules for Int involving insert and intervals.
nipkow
parents: 32436
diff changeset
   585
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
   586
by auto
341c83339aeb tuned the simp rules for Int involving insert and intervals.
nipkow
parents: 32436
diff changeset
   587
50417
f18b92f91818 add Int_atMost
hoelzl
parents: 47988
diff changeset
   588
lemma Int_atMost[simp]: "{..a} \<inter> {..b} = {.. min a b}"
f18b92f91818 add Int_atMost
hoelzl
parents: 47988
diff changeset
   589
  by (auto simp: min_def)
f18b92f91818 add Int_atMost
hoelzl
parents: 47988
diff changeset
   590
32456
341c83339aeb tuned the simp rules for Int involving insert and intervals.
nipkow
parents: 32436
diff changeset
   591
end
341c83339aeb tuned the simp rules for Int involving insert and intervals.
nipkow
parents: 32436
diff changeset
   592
51329
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   593
context complete_lattice
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   594
begin
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   595
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   596
lemma
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   597
  shows Sup_atLeast[simp]: "Sup {x ..} = top"
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   598
    and Sup_greaterThanAtLeast[simp]: "x < top \<Longrightarrow> Sup {x <..} = top"
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   599
    and Sup_atMost[simp]: "Sup {.. y} = y"
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   600
    and Sup_atLeastAtMost[simp]: "x \<le> y \<Longrightarrow> Sup { x .. y} = y"
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   601
    and Sup_greaterThanAtMost[simp]: "x < y \<Longrightarrow> Sup { x <.. y} = y"
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   602
  by (auto intro!: Sup_eqI)
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   603
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   604
lemma
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   605
  shows Inf_atMost[simp]: "Inf {.. x} = bot"
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   606
    and Inf_atMostLessThan[simp]: "top < x \<Longrightarrow> Inf {..< x} = bot"
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   607
    and Inf_atLeast[simp]: "Inf {x ..} = x"
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   608
    and Inf_atLeastAtMost[simp]: "x \<le> y \<Longrightarrow> Inf { x .. y} = x"
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   609
    and Inf_atLeastLessThan[simp]: "x < y \<Longrightarrow> Inf { x ..< y} = x"
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   610
  by (auto intro!: Inf_eqI)
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   611
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   612
end
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   613
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   614
lemma
53216
ad2e09c30aa8 renamed inner_dense_linorder to dense_linorder
hoelzl
parents: 52729
diff changeset
   615
  fixes x y :: "'a :: {complete_lattice, dense_linorder}"
51329
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   616
  shows Sup_lessThan[simp]: "Sup {..< y} = y"
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   617
    and Sup_atLeastLessThan[simp]: "x < y \<Longrightarrow> Sup { x ..< y} = y"
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   618
    and Sup_greaterThanLessThan[simp]: "x < y \<Longrightarrow> Sup { x <..< y} = y"
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   619
    and Inf_greaterThan[simp]: "Inf {x <..} = x"
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   620
    and Inf_greaterThanAtMost[simp]: "x < y \<Longrightarrow> Inf { x <.. y} = x"
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   621
    and Inf_greaterThanLessThan[simp]: "x < y \<Longrightarrow> Inf { x <..< y} = x"
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51328
diff changeset
   622
  by (auto intro!: Inf_eqI Sup_eqI intro: dense_le dense_le_bounded dense_ge dense_ge_bounded)
32456
341c83339aeb tuned the simp rules for Int involving insert and intervals.
nipkow
parents: 32436
diff changeset
   623
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   624
subsection {* Intervals of natural numbers *}
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   625
15047
fa62de5862b9 redefining sumr to be a translation to setsum
paulson
parents: 15045
diff changeset
   626
subsubsection {* The Constant @{term lessThan} *}
fa62de5862b9 redefining sumr to be a translation to setsum
paulson
parents: 15045
diff changeset
   627
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   628
lemma lessThan_0 [simp]: "lessThan (0::nat) = {}"
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   629
by (simp add: lessThan_def)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   630
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   631
lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)"
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   632
by (simp add: lessThan_def less_Suc_eq, blast)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   633
43156
04aaac80183f fixed typo
kleing
parents: 42901
diff changeset
   634
text {* The following proof is convenient in induction proofs where
39072
1030b1a166ef Add lessThan_Suc_eq_insert_0
hoelzl
parents: 37664
diff changeset
   635
new elements get indices at the beginning. So it is used to transform
1030b1a166ef Add lessThan_Suc_eq_insert_0
hoelzl
parents: 37664
diff changeset
   636
@{term "{..<Suc n}"} to @{term "0::nat"} and @{term "{..< n}"}. *}
1030b1a166ef Add lessThan_Suc_eq_insert_0
hoelzl
parents: 37664
diff changeset
   637
1030b1a166ef Add lessThan_Suc_eq_insert_0
hoelzl
parents: 37664
diff changeset
   638
lemma lessThan_Suc_eq_insert_0: "{..<Suc n} = insert 0 (Suc ` {..<n})"
1030b1a166ef Add lessThan_Suc_eq_insert_0
hoelzl
parents: 37664
diff changeset
   639
proof safe
1030b1a166ef Add lessThan_Suc_eq_insert_0
hoelzl
parents: 37664
diff changeset
   640
  fix x assume "x < Suc n" "x \<notin> Suc ` {..<n}"
1030b1a166ef Add lessThan_Suc_eq_insert_0
hoelzl
parents: 37664
diff changeset
   641
  then have "x \<noteq> Suc (x - 1)" by auto
1030b1a166ef Add lessThan_Suc_eq_insert_0
hoelzl
parents: 37664
diff changeset
   642
  with `x < Suc n` show "x = 0" by auto
1030b1a166ef Add lessThan_Suc_eq_insert_0
hoelzl
parents: 37664
diff changeset
   643
qed
1030b1a166ef Add lessThan_Suc_eq_insert_0
hoelzl
parents: 37664
diff changeset
   644
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   645
lemma lessThan_Suc_atMost: "lessThan (Suc k) = atMost k"
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   646
by (simp add: lessThan_def atMost_def less_Suc_eq_le)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   647
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   648
lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV"
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   649
by blast
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   650
15047
fa62de5862b9 redefining sumr to be a translation to setsum
paulson
parents: 15045
diff changeset
   651
subsubsection {* The Constant @{term greaterThan} *}
fa62de5862b9 redefining sumr to be a translation to setsum
paulson
parents: 15045
diff changeset
   652
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   653
lemma greaterThan_0 [simp]: "greaterThan 0 = range Suc"
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   654
apply (simp add: greaterThan_def)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   655
apply (blast dest: gr0_conv_Suc [THEN iffD1])
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   656
done
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   657
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   658
lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k - {Suc k}"
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   659
apply (simp add: greaterThan_def)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   660
apply (auto elim: linorder_neqE)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   661
done
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   662
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   663
lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}"
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   664
by blast
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   665
15047
fa62de5862b9 redefining sumr to be a translation to setsum
paulson
parents: 15045
diff changeset
   666
subsubsection {* The Constant @{term atLeast} *}
fa62de5862b9 redefining sumr to be a translation to setsum
paulson
parents: 15045
diff changeset
   667
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   668
lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV"
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   669
by (unfold atLeast_def UNIV_def, simp)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   670
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   671
lemma atLeast_Suc: "atLeast (Suc k) = atLeast k - {k}"
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   672
apply (simp add: atLeast_def)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   673
apply (simp add: Suc_le_eq)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   674
apply (simp add: order_le_less, blast)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   675
done
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   676
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   677
lemma atLeast_Suc_greaterThan: "atLeast (Suc k) = greaterThan k"
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   678
  by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   679
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   680
lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV"
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   681
by blast
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   682
15047
fa62de5862b9 redefining sumr to be a translation to setsum
paulson
parents: 15045
diff changeset
   683
subsubsection {* The Constant @{term atMost} *}
fa62de5862b9 redefining sumr to be a translation to setsum
paulson
parents: 15045
diff changeset
   684
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   685
lemma atMost_0 [simp]: "atMost (0::nat) = {0}"
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   686
by (simp add: atMost_def)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   687
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   688
lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)"
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   689
apply (simp add: atMost_def)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   690
apply (simp add: less_Suc_eq order_le_less, blast)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   691
done
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   692
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   693
lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   694
by blast
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   695
15047
fa62de5862b9 redefining sumr to be a translation to setsum
paulson
parents: 15045
diff changeset
   696
subsubsection {* The Constant @{term atLeastLessThan} *}
fa62de5862b9 redefining sumr to be a translation to setsum
paulson
parents: 15045
diff changeset
   697
28068
f6b2d1995171 cleaned up code generation for {.._} and {..<_}
nipkow
parents: 27656
diff changeset
   698
text{*The orientation of the following 2 rules is tricky. The lhs is
24449
2f05cb7fed85 added (code) lemmas for setsum and foldl
nipkow
parents: 24286
diff changeset
   699
defined in terms of the rhs.  Hence the chosen orientation makes sense
2f05cb7fed85 added (code) lemmas for setsum and foldl
nipkow
parents: 24286
diff changeset
   700
in this theory --- the reverse orientation complicates proofs (eg
2f05cb7fed85 added (code) lemmas for setsum and foldl
nipkow
parents: 24286
diff changeset
   701
nontermination). But outside, when the definition of the lhs is rarely
2f05cb7fed85 added (code) lemmas for setsum and foldl
nipkow
parents: 24286
diff changeset
   702
used, the opposite orientation seems preferable because it reduces a
2f05cb7fed85 added (code) lemmas for setsum and foldl
nipkow
parents: 24286
diff changeset
   703
specific concept to a more general one. *}
28068
f6b2d1995171 cleaned up code generation for {.._} and {..<_}
nipkow
parents: 27656
diff changeset
   704
15047
fa62de5862b9 redefining sumr to be a translation to setsum
paulson
parents: 15045
diff changeset
   705
lemma atLeast0LessThan: "{0::nat..<n} = {..<n}"
15042
fa7d27ef7e59 added {0::nat..n(} = {..n(}
nipkow
parents: 15041
diff changeset
   706
by(simp add:lessThan_def atLeastLessThan_def)
24449
2f05cb7fed85 added (code) lemmas for setsum and foldl
nipkow
parents: 24286
diff changeset
   707
28068
f6b2d1995171 cleaned up code generation for {.._} and {..<_}
nipkow
parents: 27656
diff changeset
   708
lemma atLeast0AtMost: "{0..n::nat} = {..n}"
f6b2d1995171 cleaned up code generation for {.._} and {..<_}
nipkow
parents: 27656
diff changeset
   709
by(simp add:atMost_def atLeastAtMost_def)
f6b2d1995171 cleaned up code generation for {.._} and {..<_}
nipkow
parents: 27656
diff changeset
   710
31998
2c7a24f74db9 code attributes use common underscore convention
haftmann
parents: 31509
diff changeset
   711
declare atLeast0LessThan[symmetric, code_unfold]
2c7a24f74db9 code attributes use common underscore convention
haftmann
parents: 31509
diff changeset
   712
        atLeast0AtMost[symmetric, code_unfold]
24449
2f05cb7fed85 added (code) lemmas for setsum and foldl
nipkow
parents: 24286
diff changeset
   713
2f05cb7fed85 added (code) lemmas for setsum and foldl
nipkow
parents: 24286
diff changeset
   714
lemma atLeastLessThan0: "{m..<0::nat} = {}"
15047
fa62de5862b9 redefining sumr to be a translation to setsum
paulson
parents: 15045
diff changeset
   715
by (simp add: atLeastLessThan_def)
24449
2f05cb7fed85 added (code) lemmas for setsum and foldl
nipkow
parents: 24286
diff changeset
   716
15047
fa62de5862b9 redefining sumr to be a translation to setsum
paulson
parents: 15045
diff changeset
   717
subsubsection {* Intervals of nats with @{term Suc} *}
fa62de5862b9 redefining sumr to be a translation to setsum
paulson
parents: 15045
diff changeset
   718
fa62de5862b9 redefining sumr to be a translation to setsum
paulson
parents: 15045
diff changeset
   719
text{*Not a simprule because the RHS is too messy.*}
fa62de5862b9 redefining sumr to be a translation to setsum
paulson
parents: 15045
diff changeset
   720
lemma atLeastLessThanSuc:
fa62de5862b9 redefining sumr to be a translation to setsum
paulson
parents: 15045
diff changeset
   721
    "{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
   722
by (auto simp add: atLeastLessThan_def)
15047
fa62de5862b9 redefining sumr to be a translation to setsum
paulson
parents: 15045
diff changeset
   723
15418
e28853da5df5 removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents: 15402
diff changeset
   724
lemma atLeastLessThan_singleton [simp]: "{m..<Suc m} = {m}"
15047
fa62de5862b9 redefining sumr to be a translation to setsum
paulson
parents: 15045
diff changeset
   725
by (auto simp add: atLeastLessThan_def)
16041
5a8736668ced simplifier trace info; Suc-intervals
nipkow
parents: 15911
diff changeset
   726
(*
15047
fa62de5862b9 redefining sumr to be a translation to setsum
paulson
parents: 15045
diff changeset
   727
lemma atLeast_sum_LessThan [simp]: "{m + k..<k::nat} = {}"
fa62de5862b9 redefining sumr to be a translation to setsum
paulson
parents: 15045
diff changeset
   728
by (induct k, simp_all add: atLeastLessThanSuc)
fa62de5862b9 redefining sumr to be a translation to setsum
paulson
parents: 15045
diff changeset
   729
fa62de5862b9 redefining sumr to be a translation to setsum
paulson
parents: 15045
diff changeset
   730
lemma atLeastSucLessThan [simp]: "{Suc n..<n} = {}"
fa62de5862b9 redefining sumr to be a translation to setsum
paulson
parents: 15045
diff changeset
   731
by (auto simp add: atLeastLessThan_def)
16041
5a8736668ced simplifier trace info; Suc-intervals
nipkow
parents: 15911
diff changeset
   732
*)
15045
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
   733
lemma atLeastLessThanSuc_atLeastAtMost: "{l..<Suc u} = {l..u}"
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   734
  by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   735
15418
e28853da5df5 removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents: 15402
diff changeset
   736
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
   737
  by (simp add: atLeast_Suc_greaterThan atLeastAtMost_def
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   738
    greaterThanAtMost_def)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   739
15418
e28853da5df5 removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents: 15402
diff changeset
   740
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
   741
  by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   742
    greaterThanLessThan_def)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   743
15554
03d4347b071d integrated Jeremy's FiniteLib
nipkow
parents: 15542
diff changeset
   744
lemma atLeastAtMostSuc_conv: "m \<le> Suc n \<Longrightarrow> {m..Suc n} = insert (Suc n) {m..n}"
03d4347b071d integrated Jeremy's FiniteLib
nipkow
parents: 15542
diff changeset
   745
by (auto simp add: atLeastAtMost_def)
03d4347b071d integrated Jeremy's FiniteLib
nipkow
parents: 15542
diff changeset
   746
45932
6f08f8fe9752 add lemmas
noschinl
parents: 44890
diff changeset
   747
lemma atLeastAtMost_insertL: "m \<le> n \<Longrightarrow> insert m {Suc m..n} = {m ..n}"
6f08f8fe9752 add lemmas
noschinl
parents: 44890
diff changeset
   748
by auto
6f08f8fe9752 add lemmas
noschinl
parents: 44890
diff changeset
   749
43157
b505be6f029a atLeastAtMostSuc_conv on int
kleing
parents: 43156
diff changeset
   750
text {* The analogous result is useful on @{typ int}: *}
b505be6f029a atLeastAtMostSuc_conv on int
kleing
parents: 43156
diff changeset
   751
(* here, because we don't have an own int section *)
b505be6f029a atLeastAtMostSuc_conv on int
kleing
parents: 43156
diff changeset
   752
lemma atLeastAtMostPlus1_int_conv:
b505be6f029a atLeastAtMostSuc_conv on int
kleing
parents: 43156
diff changeset
   753
  "m <= 1+n \<Longrightarrow> {m..1+n} = insert (1+n) {m..n::int}"
b505be6f029a atLeastAtMostSuc_conv on int
kleing
parents: 43156
diff changeset
   754
  by (auto intro: set_eqI)
b505be6f029a atLeastAtMostSuc_conv on int
kleing
parents: 43156
diff changeset
   755
33044
fd0a9c794ec1 Some new lemmas concerning sets
paulson
parents: 32960
diff changeset
   756
lemma atLeastLessThan_add_Un: "i \<le> j \<Longrightarrow> {i..<j+k} = {i..<j} \<union> {j..<j+k::nat}"
fd0a9c794ec1 Some new lemmas concerning sets
paulson
parents: 32960
diff changeset
   757
  apply (induct k) 
fd0a9c794ec1 Some new lemmas concerning sets
paulson
parents: 32960
diff changeset
   758
  apply (simp_all add: atLeastLessThanSuc)   
fd0a9c794ec1 Some new lemmas concerning sets
paulson
parents: 32960
diff changeset
   759
  done
fd0a9c794ec1 Some new lemmas concerning sets
paulson
parents: 32960
diff changeset
   760
57113
7e95523302e6 New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents: 56949
diff changeset
   761
subsubsection {* Intervals and numerals *}
7e95523302e6 New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents: 56949
diff changeset
   762
7e95523302e6 New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents: 56949
diff changeset
   763
lemma lessThan_nat_numeral:  --{*Evaluation for specific numerals*}
7e95523302e6 New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents: 56949
diff changeset
   764
  "lessThan (numeral k :: nat) = insert (pred_numeral k) (lessThan (pred_numeral k))"
7e95523302e6 New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents: 56949
diff changeset
   765
  by (simp add: numeral_eq_Suc lessThan_Suc)
7e95523302e6 New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents: 56949
diff changeset
   766
7e95523302e6 New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents: 56949
diff changeset
   767
lemma atMost_nat_numeral:  --{*Evaluation for specific numerals*}
7e95523302e6 New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents: 56949
diff changeset
   768
  "atMost (numeral k :: nat) = insert (numeral k) (atMost (pred_numeral k))"
7e95523302e6 New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents: 56949
diff changeset
   769
  by (simp add: numeral_eq_Suc atMost_Suc)
7e95523302e6 New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents: 56949
diff changeset
   770
7e95523302e6 New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents: 56949
diff changeset
   771
lemma atLeastLessThan_nat_numeral:  --{*Evaluation for specific numerals*}
7e95523302e6 New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents: 56949
diff changeset
   772
  "atLeastLessThan m (numeral k :: nat) = 
7e95523302e6 New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents: 56949
diff changeset
   773
     (if m \<le> (pred_numeral k) then insert (pred_numeral k) (atLeastLessThan m (pred_numeral k))
7e95523302e6 New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents: 56949
diff changeset
   774
                 else {})"
7e95523302e6 New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents: 56949
diff changeset
   775
  by (simp add: numeral_eq_Suc atLeastLessThanSuc)
7e95523302e6 New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents: 56949
diff changeset
   776
16733
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
   777
subsubsection {* Image *}
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
   778
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
   779
lemma image_add_atLeastAtMost:
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
   780
  "(%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
   781
proof
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
   782
  show "?A \<subseteq> ?B" by auto
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
   783
next
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
   784
  show "?B \<subseteq> ?A"
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
   785
  proof
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
   786
    fix n assume a: "n : ?B"
20217
25b068a99d2b linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents: 19538
diff changeset
   787
    hence "n - k : {i..j}" by auto
16733
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
   788
    moreover have "n = (n - k) + k" using a by auto
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
   789
    ultimately show "n : ?A" by blast
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
   790
  qed
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
   791
qed
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
   792
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
   793
lemma image_add_atLeastLessThan:
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
   794
  "(%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
   795
proof
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
   796
  show "?A \<subseteq> ?B" by auto
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
   797
next
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
   798
  show "?B \<subseteq> ?A"
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
   799
  proof
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
   800
    fix n assume a: "n : ?B"
20217
25b068a99d2b linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents: 19538
diff changeset
   801
    hence "n - k : {i..<j}" by auto
16733
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
   802
    moreover have "n = (n - k) + k" using a by auto
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
   803
    ultimately show "n : ?A" by blast
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
   804
  qed
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
   805
qed
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
   806
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
   807
corollary image_Suc_atLeastAtMost[simp]:
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
   808
  "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
   809
using image_add_atLeastAtMost[where k="Suc 0"] by simp
16733
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
   810
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
   811
corollary image_Suc_atLeastLessThan[simp]:
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
   812
  "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
   813
using image_add_atLeastLessThan[where k="Suc 0"] by simp
16733
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
   814
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
   815
lemma image_add_int_atLeastLessThan:
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
   816
    "(%x. x + (l::int)) ` {0..<u-l} = {l..<u}"
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
   817
  apply (auto simp add: image_def)
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
   818
  apply (rule_tac x = "x - l" in bexI)
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
   819
  apply auto
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
   820
  done
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
   821
37664
2946b8f057df Instantiate product type as euclidean space.
hoelzl
parents: 37388
diff changeset
   822
lemma image_minus_const_atLeastLessThan_nat:
2946b8f057df Instantiate product type as euclidean space.
hoelzl
parents: 37388
diff changeset
   823
  fixes c :: nat
2946b8f057df Instantiate product type as euclidean space.
hoelzl
parents: 37388
diff changeset
   824
  shows "(\<lambda>i. i - c) ` {x ..< y} =
2946b8f057df Instantiate product type as euclidean space.
hoelzl
parents: 37388
diff changeset
   825
      (if c < y then {x - c ..< y - c} else if x < y then {0} else {})"
2946b8f057df Instantiate product type as euclidean space.
hoelzl
parents: 37388
diff changeset
   826
    (is "_ = ?right")
2946b8f057df Instantiate product type as euclidean space.
hoelzl
parents: 37388
diff changeset
   827
proof safe
2946b8f057df Instantiate product type as euclidean space.
hoelzl
parents: 37388
diff changeset
   828
  fix a assume a: "a \<in> ?right"
2946b8f057df Instantiate product type as euclidean space.
hoelzl
parents: 37388
diff changeset
   829
  show "a \<in> (\<lambda>i. i - c) ` {x ..< y}"
2946b8f057df Instantiate product type as euclidean space.
hoelzl
parents: 37388
diff changeset
   830
  proof cases
2946b8f057df Instantiate product type as euclidean space.
hoelzl
parents: 37388
diff changeset
   831
    assume "c < y" with a show ?thesis
2946b8f057df Instantiate product type as euclidean space.
hoelzl
parents: 37388
diff changeset
   832
      by (auto intro!: image_eqI[of _ _ "a + c"])
2946b8f057df Instantiate product type as euclidean space.
hoelzl
parents: 37388
diff changeset
   833
  next
2946b8f057df Instantiate product type as euclidean space.
hoelzl
parents: 37388
diff changeset
   834
    assume "\<not> c < y" with a show ?thesis
2946b8f057df Instantiate product type as euclidean space.
hoelzl
parents: 37388
diff changeset
   835
      by (auto intro!: image_eqI[of _ _ x] split: split_if_asm)
2946b8f057df Instantiate product type as euclidean space.
hoelzl
parents: 37388
diff changeset
   836
  qed
2946b8f057df Instantiate product type as euclidean space.
hoelzl
parents: 37388
diff changeset
   837
qed auto
2946b8f057df Instantiate product type as euclidean space.
hoelzl
parents: 37388
diff changeset
   838
51152
b52cc015429a added lemma
Andreas Lochbihler
parents: 50999
diff changeset
   839
lemma image_int_atLeastLessThan: "int ` {a..<b} = {int a..<int b}"
55143
04448228381d explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents: 55088
diff changeset
   840
  by (auto intro!: image_eqI [where x = "nat x" for x])
51152
b52cc015429a added lemma
Andreas Lochbihler
parents: 50999
diff changeset
   841
35580
0f74806cab22 Rewrite rules for images of minus of intervals
hoelzl
parents: 35216
diff changeset
   842
context ordered_ab_group_add
0f74806cab22 Rewrite rules for images of minus of intervals
hoelzl
parents: 35216
diff changeset
   843
begin
0f74806cab22 Rewrite rules for images of minus of intervals
hoelzl
parents: 35216
diff changeset
   844
0f74806cab22 Rewrite rules for images of minus of intervals
hoelzl
parents: 35216
diff changeset
   845
lemma
0f74806cab22 Rewrite rules for images of minus of intervals
hoelzl
parents: 35216
diff changeset
   846
  fixes x :: 'a
0f74806cab22 Rewrite rules for images of minus of intervals
hoelzl
parents: 35216
diff changeset
   847
  shows image_uminus_greaterThan[simp]: "uminus ` {x<..} = {..<-x}"
0f74806cab22 Rewrite rules for images of minus of intervals
hoelzl
parents: 35216
diff changeset
   848
  and image_uminus_atLeast[simp]: "uminus ` {x..} = {..-x}"
0f74806cab22 Rewrite rules for images of minus of intervals
hoelzl
parents: 35216
diff changeset
   849
proof safe
0f74806cab22 Rewrite rules for images of minus of intervals
hoelzl
parents: 35216
diff changeset
   850
  fix y assume "y < -x"
0f74806cab22 Rewrite rules for images of minus of intervals
hoelzl
parents: 35216
diff changeset
   851
  hence *:  "x < -y" using neg_less_iff_less[of "-y" x] by simp
0f74806cab22 Rewrite rules for images of minus of intervals
hoelzl
parents: 35216
diff changeset
   852
  have "- (-y) \<in> uminus ` {x<..}"
0f74806cab22 Rewrite rules for images of minus of intervals
hoelzl
parents: 35216
diff changeset
   853
    by (rule imageI) (simp add: *)
0f74806cab22 Rewrite rules for images of minus of intervals
hoelzl
parents: 35216
diff changeset
   854
  thus "y \<in> uminus ` {x<..}" by simp
0f74806cab22 Rewrite rules for images of minus of intervals
hoelzl
parents: 35216
diff changeset
   855
next
0f74806cab22 Rewrite rules for images of minus of intervals
hoelzl
parents: 35216
diff changeset
   856
  fix y assume "y \<le> -x"
0f74806cab22 Rewrite rules for images of minus of intervals
hoelzl
parents: 35216
diff changeset
   857
  have "- (-y) \<in> uminus ` {x..}"
0f74806cab22 Rewrite rules for images of minus of intervals
hoelzl
parents: 35216
diff changeset
   858
    by (rule imageI) (insert `y \<le> -x`[THEN le_imp_neg_le], simp)
0f74806cab22 Rewrite rules for images of minus of intervals
hoelzl
parents: 35216
diff changeset
   859
  thus "y \<in> uminus ` {x..}" by simp
0f74806cab22 Rewrite rules for images of minus of intervals
hoelzl
parents: 35216
diff changeset
   860
qed simp_all
0f74806cab22 Rewrite rules for images of minus of intervals
hoelzl
parents: 35216
diff changeset
   861
0f74806cab22 Rewrite rules for images of minus of intervals
hoelzl
parents: 35216
diff changeset
   862
lemma
0f74806cab22 Rewrite rules for images of minus of intervals
hoelzl
parents: 35216
diff changeset
   863
  fixes x :: 'a
0f74806cab22 Rewrite rules for images of minus of intervals
hoelzl
parents: 35216
diff changeset
   864
  shows image_uminus_lessThan[simp]: "uminus ` {..<x} = {-x<..}"
0f74806cab22 Rewrite rules for images of minus of intervals
hoelzl
parents: 35216
diff changeset
   865
  and image_uminus_atMost[simp]: "uminus ` {..x} = {-x..}"
0f74806cab22 Rewrite rules for images of minus of intervals
hoelzl
parents: 35216
diff changeset
   866
proof -
0f74806cab22 Rewrite rules for images of minus of intervals
hoelzl
parents: 35216
diff changeset
   867
  have "uminus ` {..<x} = uminus ` uminus ` {-x<..}"
0f74806cab22 Rewrite rules for images of minus of intervals
hoelzl
parents: 35216
diff changeset
   868
    and "uminus ` {..x} = uminus ` uminus ` {-x..}" by simp_all
0f74806cab22 Rewrite rules for images of minus of intervals
hoelzl
parents: 35216
diff changeset
   869
  thus "uminus ` {..<x} = {-x<..}" and "uminus ` {..x} = {-x..}"
0f74806cab22 Rewrite rules for images of minus of intervals
hoelzl
parents: 35216
diff changeset
   870
    by (simp_all add: image_image
0f74806cab22 Rewrite rules for images of minus of intervals
hoelzl
parents: 35216
diff changeset
   871
        del: image_uminus_greaterThan image_uminus_atLeast)
0f74806cab22 Rewrite rules for images of minus of intervals
hoelzl
parents: 35216
diff changeset
   872
qed
0f74806cab22 Rewrite rules for images of minus of intervals
hoelzl
parents: 35216
diff changeset
   873
0f74806cab22 Rewrite rules for images of minus of intervals
hoelzl
parents: 35216
diff changeset
   874
lemma
0f74806cab22 Rewrite rules for images of minus of intervals
hoelzl
parents: 35216
diff changeset
   875
  fixes x :: 'a
0f74806cab22 Rewrite rules for images of minus of intervals
hoelzl
parents: 35216
diff changeset
   876
  shows image_uminus_atLeastAtMost[simp]: "uminus ` {x..y} = {-y..-x}"
0f74806cab22 Rewrite rules for images of minus of intervals
hoelzl
parents: 35216
diff changeset
   877
  and image_uminus_greaterThanAtMost[simp]: "uminus ` {x<..y} = {-y..<-x}"
0f74806cab22 Rewrite rules for images of minus of intervals
hoelzl
parents: 35216
diff changeset
   878
  and image_uminus_atLeastLessThan[simp]: "uminus ` {x..<y} = {-y<..-x}"
0f74806cab22 Rewrite rules for images of minus of intervals
hoelzl
parents: 35216
diff changeset
   879
  and image_uminus_greaterThanLessThan[simp]: "uminus ` {x<..<y} = {-y<..<-x}"
0f74806cab22 Rewrite rules for images of minus of intervals
hoelzl
parents: 35216
diff changeset
   880
  by (simp_all add: atLeastAtMost_def greaterThanAtMost_def atLeastLessThan_def
0f74806cab22 Rewrite rules for images of minus of intervals
hoelzl
parents: 35216
diff changeset
   881
      greaterThanLessThan_def image_Int[OF inj_uminus] Int_commute)
0f74806cab22 Rewrite rules for images of minus of intervals
hoelzl
parents: 35216
diff changeset
   882
end
16733
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
   883
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   884
subsubsection {* Finiteness *}
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   885
15045
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
   886
lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..<k}"
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   887
  by (induct k) (simp_all add: lessThan_Suc)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   888
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   889
lemma finite_atMost [iff]: fixes k :: nat shows "finite {..k}"
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   890
  by (induct k) (simp_all add: atMost_Suc)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   891
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   892
lemma finite_greaterThanLessThan [iff]:
15045
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
   893
  fixes l :: nat shows "finite {l<..<u}"
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   894
by (simp add: greaterThanLessThan_def)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   895
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   896
lemma finite_atLeastLessThan [iff]:
15045
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
   897
  fixes l :: nat shows "finite {l..<u}"
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   898
by (simp add: atLeastLessThan_def)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   899
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   900
lemma finite_greaterThanAtMost [iff]:
15045
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
   901
  fixes l :: nat shows "finite {l<..u}"
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   902
by (simp add: greaterThanAtMost_def)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   903
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   904
lemma finite_atLeastAtMost [iff]:
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   905
  fixes l :: nat shows "finite {l..u}"
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   906
by (simp add: atLeastAtMost_def)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   907
28068
f6b2d1995171 cleaned up code generation for {.._} and {..<_}
nipkow
parents: 27656
diff changeset
   908
text {* A bounded set of natural numbers is finite. *}
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   909
lemma bounded_nat_set_is_finite:
24853
aab5798e5a33 added lemmas
nipkow
parents: 24748
diff changeset
   910
  "(ALL i:N. i < (n::nat)) ==> finite N"
28068
f6b2d1995171 cleaned up code generation for {.._} and {..<_}
nipkow
parents: 27656
diff changeset
   911
apply (rule finite_subset)
f6b2d1995171 cleaned up code generation for {.._} and {..<_}
nipkow
parents: 27656
diff changeset
   912
 apply (rule_tac [2] finite_lessThan, auto)
f6b2d1995171 cleaned up code generation for {.._} and {..<_}
nipkow
parents: 27656
diff changeset
   913
done
f6b2d1995171 cleaned up code generation for {.._} and {..<_}
nipkow
parents: 27656
diff changeset
   914
31044
6896c2498ac0 new lemmas
nipkow
parents: 31017
diff changeset
   915
text {* A set of natural numbers is finite iff it is bounded. *}
6896c2498ac0 new lemmas
nipkow
parents: 31017
diff changeset
   916
lemma finite_nat_set_iff_bounded:
6896c2498ac0 new lemmas
nipkow
parents: 31017
diff changeset
   917
  "finite(N::nat set) = (EX m. ALL n:N. n<m)" (is "?F = ?B")
6896c2498ac0 new lemmas
nipkow
parents: 31017
diff changeset
   918
proof
6896c2498ac0 new lemmas
nipkow
parents: 31017
diff changeset
   919
  assume f:?F  show ?B
6896c2498ac0 new lemmas
nipkow
parents: 31017
diff changeset
   920
    using Max_ge[OF `?F`, simplified less_Suc_eq_le[symmetric]] by blast
6896c2498ac0 new lemmas
nipkow
parents: 31017
diff changeset
   921
next
6896c2498ac0 new lemmas
nipkow
parents: 31017
diff changeset
   922
  assume ?B show ?F using `?B` by(blast intro:bounded_nat_set_is_finite)
6896c2498ac0 new lemmas
nipkow
parents: 31017
diff changeset
   923
qed
6896c2498ac0 new lemmas
nipkow
parents: 31017
diff changeset
   924
6896c2498ac0 new lemmas
nipkow
parents: 31017
diff changeset
   925
lemma finite_nat_set_iff_bounded_le:
6896c2498ac0 new lemmas
nipkow
parents: 31017
diff changeset
   926
  "finite(N::nat set) = (EX m. ALL n:N. n<=m)"
6896c2498ac0 new lemmas
nipkow
parents: 31017
diff changeset
   927
apply(simp add:finite_nat_set_iff_bounded)
6896c2498ac0 new lemmas
nipkow
parents: 31017
diff changeset
   928
apply(blast dest:less_imp_le_nat le_imp_less_Suc)
6896c2498ac0 new lemmas
nipkow
parents: 31017
diff changeset
   929
done
6896c2498ac0 new lemmas
nipkow
parents: 31017
diff changeset
   930
28068
f6b2d1995171 cleaned up code generation for {.._} and {..<_}
nipkow
parents: 27656
diff changeset
   931
lemma finite_less_ub:
f6b2d1995171 cleaned up code generation for {.._} and {..<_}
nipkow
parents: 27656
diff changeset
   932
     "!!f::nat=>nat. (!!n. n \<le> f n) ==> finite {n. f n \<le> u}"
f6b2d1995171 cleaned up code generation for {.._} and {..<_}
nipkow
parents: 27656
diff changeset
   933
by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans)
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
   934
56328
b3551501424e add rules about infinity of intervals
hoelzl
parents: 56238
diff changeset
   935
24853
aab5798e5a33 added lemmas
nipkow
parents: 24748
diff changeset
   936
text{* Any subset of an interval of natural numbers the size of the
aab5798e5a33 added lemmas
nipkow
parents: 24748
diff changeset
   937
subset is exactly that interval. *}
aab5798e5a33 added lemmas
nipkow
parents: 24748
diff changeset
   938
aab5798e5a33 added lemmas
nipkow
parents: 24748
diff changeset
   939
lemma subset_card_intvl_is_intvl:
55085
0e8e4dc55866 moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
blanchet
parents: 54606
diff changeset
   940
  assumes "A \<subseteq> {k..<k + card A}"
0e8e4dc55866 moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
blanchet
parents: 54606
diff changeset
   941
  shows "A = {k..<k + card A}"
53374
a14d2a854c02 tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents: 53216
diff changeset
   942
proof (cases "finite A")
a14d2a854c02 tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents: 53216
diff changeset
   943
  case True
a14d2a854c02 tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents: 53216
diff changeset
   944
  from this and assms show ?thesis
a14d2a854c02 tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents: 53216
diff changeset
   945
  proof (induct A rule: finite_linorder_max_induct)
24853
aab5798e5a33 added lemmas
nipkow
parents: 24748
diff changeset
   946
    case empty thus ?case by auto
aab5798e5a33 added lemmas
nipkow
parents: 24748
diff changeset
   947
  next
33434
e9de8d69c1b9 fixed order of parameters in induction rules
nipkow
parents: 33318
diff changeset
   948
    case (insert b A)
53374
a14d2a854c02 tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents: 53216
diff changeset
   949
    hence *: "b \<notin> A" by auto
55085
0e8e4dc55866 moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
blanchet
parents: 54606
diff changeset
   950
    with insert have "A <= {k..<k + card A}" and "b = k + card A"
53374
a14d2a854c02 tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents: 53216
diff changeset
   951
      by fastforce+
a14d2a854c02 tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents: 53216
diff changeset
   952
    with insert * show ?case by auto
24853
aab5798e5a33 added lemmas
nipkow
parents: 24748
diff changeset
   953
  qed
aab5798e5a33 added lemmas
nipkow
parents: 24748
diff changeset
   954
next
53374
a14d2a854c02 tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents: 53216
diff changeset
   955
  case False
a14d2a854c02 tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents: 53216
diff changeset
   956
  with assms show ?thesis by simp
24853
aab5798e5a33 added lemmas
nipkow
parents: 24748
diff changeset
   957
qed
aab5798e5a33 added lemmas
nipkow
parents: 24748
diff changeset
   958
aab5798e5a33 added lemmas
nipkow
parents: 24748
diff changeset
   959
32596
bd68c04dace1 New theorems for proving equalities and inclusions involving unions
paulson
parents: 32456
diff changeset
   960
subsubsection {* Proving Inclusions and Equalities between Unions *}
bd68c04dace1 New theorems for proving equalities and inclusions involving unions
paulson
parents: 32456
diff changeset
   961
36755
d1b498f2f50b added lemmas
nipkow
parents: 36365
diff changeset
   962
lemma UN_le_eq_Un0:
d1b498f2f50b added lemmas
nipkow
parents: 36365
diff changeset
   963
  "(\<Union>i\<le>n::nat. M i) = (\<Union>i\<in>{1..n}. M i) \<union> M 0" (is "?A = ?B")
d1b498f2f50b added lemmas
nipkow
parents: 36365
diff changeset
   964
proof
d1b498f2f50b added lemmas
nipkow
parents: 36365
diff changeset
   965
  show "?A <= ?B"
d1b498f2f50b added lemmas
nipkow
parents: 36365
diff changeset
   966
  proof
d1b498f2f50b added lemmas
nipkow
parents: 36365
diff changeset
   967
    fix x assume "x : ?A"
d1b498f2f50b added lemmas
nipkow
parents: 36365
diff changeset
   968
    then obtain i where i: "i\<le>n" "x : M i" by auto
d1b498f2f50b added lemmas
nipkow
parents: 36365
diff changeset
   969
    show "x : ?B"
d1b498f2f50b added lemmas
nipkow
parents: 36365
diff changeset
   970
    proof(cases i)
d1b498f2f50b added lemmas
nipkow
parents: 36365
diff changeset
   971
      case 0 with i show ?thesis by simp
d1b498f2f50b added lemmas
nipkow
parents: 36365
diff changeset
   972
    next
d1b498f2f50b added lemmas
nipkow
parents: 36365
diff changeset
   973
      case (Suc j) with i show ?thesis by auto
d1b498f2f50b added lemmas
nipkow
parents: 36365
diff changeset
   974
    qed
d1b498f2f50b added lemmas
nipkow
parents: 36365
diff changeset
   975
  qed
d1b498f2f50b added lemmas
nipkow
parents: 36365
diff changeset
   976
next
d1b498f2f50b added lemmas
nipkow
parents: 36365
diff changeset
   977
  show "?B <= ?A" by auto
d1b498f2f50b added lemmas
nipkow
parents: 36365
diff changeset
   978
qed
d1b498f2f50b added lemmas
nipkow
parents: 36365
diff changeset
   979
d1b498f2f50b added lemmas
nipkow
parents: 36365
diff changeset
   980
lemma UN_le_add_shift:
d1b498f2f50b added lemmas
nipkow
parents: 36365
diff changeset
   981
  "(\<Union>i\<le>n::nat. M(i+k)) = (\<Union>i\<in>{k..n+k}. M i)" (is "?A = ?B")
d1b498f2f50b added lemmas
nipkow
parents: 36365
diff changeset
   982
proof
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 44008
diff changeset
   983
  show "?A <= ?B" by fastforce
36755
d1b498f2f50b added lemmas
nipkow
parents: 36365
diff changeset
   984
next
d1b498f2f50b added lemmas
nipkow
parents: 36365
diff changeset
   985
  show "?B <= ?A"
d1b498f2f50b added lemmas
nipkow
parents: 36365
diff changeset
   986
  proof
d1b498f2f50b added lemmas
nipkow
parents: 36365
diff changeset
   987
    fix x assume "x : ?B"
d1b498f2f50b added lemmas
nipkow
parents: 36365
diff changeset
   988
    then obtain i where i: "i : {k..n+k}" "x : M(i)" by auto
d1b498f2f50b added lemmas
nipkow
parents: 36365
diff changeset
   989
    hence "i-k\<le>n & x : M((i-k)+k)" by auto
d1b498f2f50b added lemmas
nipkow
parents: 36365
diff changeset
   990
    thus "x : ?A" by blast
d1b498f2f50b added lemmas
nipkow
parents: 36365
diff changeset
   991
  qed
d1b498f2f50b added lemmas
nipkow
parents: 36365
diff changeset
   992
qed
d1b498f2f50b added lemmas
nipkow
parents: 36365
diff changeset
   993
32596
bd68c04dace1 New theorems for proving equalities and inclusions involving unions
paulson
parents: 32456
diff changeset
   994
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
   995
  by (auto simp add: atLeast0LessThan) 
bd68c04dace1 New theorems for proving equalities and inclusions involving unions
paulson
parents: 32456
diff changeset
   996
bd68c04dace1 New theorems for proving equalities and inclusions involving unions
paulson
parents: 32456
diff changeset
   997
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
   998
  by (subst UN_UN_finite_eq [symmetric]) blast
bd68c04dace1 New theorems for proving equalities and inclusions involving unions
paulson
parents: 32456
diff changeset
   999
33044
fd0a9c794ec1 Some new lemmas concerning sets
paulson
parents: 32960
diff changeset
  1000
lemma UN_finite2_subset: 
fd0a9c794ec1 Some new lemmas concerning sets
paulson
parents: 32960
diff changeset
  1001
     "(!!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)"
fd0a9c794ec1 Some new lemmas concerning sets
paulson
parents: 32960
diff changeset
  1002
  apply (rule UN_finite_subset)
fd0a9c794ec1 Some new lemmas concerning sets
paulson
parents: 32960
diff changeset
  1003
  apply (subst UN_UN_finite_eq [symmetric, of B]) 
fd0a9c794ec1 Some new lemmas concerning sets
paulson
parents: 32960
diff changeset
  1004
  apply blast
fd0a9c794ec1 Some new lemmas concerning sets
paulson
parents: 32960
diff changeset
  1005
  done
32596
bd68c04dace1 New theorems for proving equalities and inclusions involving unions
paulson
parents: 32456
diff changeset
  1006
bd68c04dace1 New theorems for proving equalities and inclusions involving unions
paulson
parents: 32456
diff changeset
  1007
lemma UN_finite2_eq:
33044
fd0a9c794ec1 Some new lemmas concerning sets
paulson
parents: 32960
diff changeset
  1008
  "(!!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)"
fd0a9c794ec1 Some new lemmas concerning sets
paulson
parents: 32960
diff changeset
  1009
  apply (rule subset_antisym)
fd0a9c794ec1 Some new lemmas concerning sets
paulson
parents: 32960
diff changeset
  1010
   apply (rule UN_finite2_subset, blast)
fd0a9c794ec1 Some new lemmas concerning sets
paulson
parents: 32960
diff changeset
  1011
 apply (rule UN_finite2_subset [where k=k])
35216
7641e8d831d2 get rid of many duplicate simp rule warnings
huffman
parents: 35171
diff changeset
  1012
 apply (force simp add: atLeastLessThan_add_Un [of 0])
33044
fd0a9c794ec1 Some new lemmas concerning sets
paulson
parents: 32960
diff changeset
  1013
 done
32596
bd68c04dace1 New theorems for proving equalities and inclusions involving unions
paulson
parents: 32456
diff changeset
  1014
bd68c04dace1 New theorems for proving equalities and inclusions involving unions
paulson
parents: 32456
diff changeset
  1015
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1016
subsubsection {* Cardinality *}
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1017
15045
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1018
lemma card_lessThan [simp]: "card {..<u} = u"
15251
bb6f072c8d10 converted some induct_tac to induct
paulson
parents: 15140
diff changeset
  1019
  by (induct u, simp_all add: lessThan_Suc)
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1020
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1021
lemma card_atMost [simp]: "card {..u} = Suc u"
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1022
  by (simp add: lessThan_Suc_atMost [THEN sym])
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1023
15045
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1024
lemma card_atLeastLessThan [simp]: "card {l..<u} = u - l"
57113
7e95523302e6 New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents: 56949
diff changeset
  1025
proof -
7e95523302e6 New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents: 56949
diff changeset
  1026
  have "{l..<u} = (%x. x + l) ` {..<u-l}"
7e95523302e6 New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents: 56949
diff changeset
  1027
    apply (auto simp add: image_def atLeastLessThan_def lessThan_def)
7e95523302e6 New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents: 56949
diff changeset
  1028
    apply (rule_tac x = "x - l" in exI)
7e95523302e6 New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents: 56949
diff changeset
  1029
    apply arith
7e95523302e6 New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents: 56949
diff changeset
  1030
    done
7e95523302e6 New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents: 56949
diff changeset
  1031
  then have "card {l..<u} = card {..<u-l}"
7e95523302e6 New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents: 56949
diff changeset
  1032
    by (simp add: card_image inj_on_def)
7e95523302e6 New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents: 56949
diff changeset
  1033
  then show ?thesis
7e95523302e6 New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents: 56949
diff changeset
  1034
    by simp
7e95523302e6 New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents: 56949
diff changeset
  1035
qed
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1036
15418
e28853da5df5 removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents: 15402
diff changeset
  1037
lemma card_atLeastAtMost [simp]: "card {l..u} = Suc u - l"
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1038
  by (subst atLeastLessThanSuc_atLeastAtMost [THEN sym], simp)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1039
15418
e28853da5df5 removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents: 15402
diff changeset
  1040
lemma card_greaterThanAtMost [simp]: "card {l<..u} = u - l"
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1041
  by (subst atLeastSucAtMost_greaterThanAtMost [THEN sym], simp)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1042
15045
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1043
lemma card_greaterThanLessThan [simp]: "card {l<..<u} = u - Suc l"
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1044
  by (subst atLeastSucLessThan_greaterThanLessThan [THEN sym], simp)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1045
26105
ae06618225ec moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents: 26072
diff changeset
  1046
lemma ex_bij_betw_nat_finite:
ae06618225ec moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents: 26072
diff changeset
  1047
  "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
  1048
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
  1049
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
  1050
done
ae06618225ec moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents: 26072
diff changeset
  1051
ae06618225ec moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents: 26072
diff changeset
  1052
lemma ex_bij_betw_finite_nat:
ae06618225ec moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents: 26072
diff changeset
  1053
  "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
  1054
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
  1055
31438
a1c4c1500abe A few finite lemmas
nipkow
parents: 31044
diff changeset
  1056
lemma finite_same_card_bij:
a1c4c1500abe A few finite lemmas
nipkow
parents: 31044
diff changeset
  1057
  "finite A \<Longrightarrow> finite B \<Longrightarrow> card A = card B \<Longrightarrow> EX h. bij_betw h A B"
a1c4c1500abe A few finite lemmas
nipkow
parents: 31044
diff changeset
  1058
apply(drule ex_bij_betw_finite_nat)
a1c4c1500abe A few finite lemmas
nipkow
parents: 31044
diff changeset
  1059
apply(drule ex_bij_betw_nat_finite)
a1c4c1500abe A few finite lemmas
nipkow
parents: 31044
diff changeset
  1060
apply(auto intro!:bij_betw_trans)
a1c4c1500abe A few finite lemmas
nipkow
parents: 31044
diff changeset
  1061
done
a1c4c1500abe A few finite lemmas
nipkow
parents: 31044
diff changeset
  1062
a1c4c1500abe A few finite lemmas
nipkow
parents: 31044
diff changeset
  1063
lemma ex_bij_betw_nat_finite_1:
a1c4c1500abe A few finite lemmas
nipkow
parents: 31044
diff changeset
  1064
  "finite M \<Longrightarrow> \<exists>h. bij_betw h {1 .. card M} M"
a1c4c1500abe A few finite lemmas
nipkow
parents: 31044
diff changeset
  1065
by (rule finite_same_card_bij) auto
a1c4c1500abe A few finite lemmas
nipkow
parents: 31044
diff changeset
  1066
40703
d1fc454d6735 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents: 39302
diff changeset
  1067
lemma bij_betw_iff_card:
d1fc454d6735 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents: 39302
diff changeset
  1068
  assumes FIN: "finite A" and FIN': "finite B"
d1fc454d6735 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents: 39302
diff changeset
  1069
  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 HOL-image.
hoelzl
parents: 39302
diff changeset
  1070
using assms
d1fc454d6735 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents: 39302
diff changeset
  1071
proof(auto simp add: bij_betw_same_card)
d1fc454d6735 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents: 39302
diff changeset
  1072
  assume *: "card A = card B"
d1fc454d6735 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents: 39302
diff changeset
  1073
  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 HOL-image.
hoelzl
parents: 39302
diff changeset
  1074
  using FIN ex_bij_betw_finite_nat by blast
d1fc454d6735 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents: 39302
diff changeset
  1075
  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 HOL-image.
hoelzl
parents: 39302
diff changeset
  1076
  using FIN' ex_bij_betw_nat_finite by blast
d1fc454d6735 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents: 39302
diff changeset
  1077
  ultimately have "bij_betw (g o f) A B"
d1fc454d6735 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents: 39302
diff changeset
  1078
  using * by (auto simp add: bij_betw_trans)
d1fc454d6735 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents: 39302
diff changeset
  1079
  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 HOL-image.
hoelzl
parents: 39302
diff changeset
  1080
qed
d1fc454d6735 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents: 39302
diff changeset
  1081
d1fc454d6735 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents: 39302
diff changeset
  1082
lemma inj_on_iff_card_le:
d1fc454d6735 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents: 39302
diff changeset
  1083
  assumes FIN: "finite A" and FIN': "finite B"
d1fc454d6735 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents: 39302
diff changeset
  1084
  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 HOL-image.
hoelzl
parents: 39302
diff changeset
  1085
proof (safe intro!: card_inj_on_le)
d1fc454d6735 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents: 39302
diff changeset
  1086
  assume *: "card A \<le> card B"
d1fc454d6735 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents: 39302
diff changeset
  1087
  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 HOL-image.
hoelzl
parents: 39302
diff changeset
  1088
  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 HOL-image.
hoelzl
parents: 39302
diff changeset
  1089
  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 HOL-image.
hoelzl
parents: 39302
diff changeset
  1090
  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 HOL-image.
hoelzl
parents: 39302
diff changeset
  1091
  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 HOL-image.
hoelzl
parents: 39302
diff changeset
  1092
  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 HOL-image.
hoelzl
parents: 39302
diff changeset
  1093
  moreover
d1fc454d6735 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents: 39302
diff changeset
  1094
  {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 HOL-image.
hoelzl
parents: 39302
diff changeset
  1095
   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 HOL-image.
hoelzl
parents: 39302
diff changeset
  1096
   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 HOL-image.
hoelzl
parents: 39302
diff changeset
  1097
  }
d1fc454d6735 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents: 39302
diff changeset
  1098
  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 HOL-image.
hoelzl
parents: 39302
diff changeset
  1099
qed (insert assms, auto)
26105
ae06618225ec moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents: 26072
diff changeset
  1100
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1101
subsection {* Intervals of integers *}
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1102
15045
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1103
lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l..<u+1} = {l..(u::int)}"
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1104
  by (auto simp add: atLeastAtMost_def atLeastLessThan_def)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1105
15418
e28853da5df5 removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents: 15402
diff changeset
  1106
lemma atLeastPlusOneAtMost_greaterThanAtMost_int: "{l+1..u} = {l<..(u::int)}"
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1107
  by (auto simp add: atLeastAtMost_def greaterThanAtMost_def)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1108
15418
e28853da5df5 removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents: 15402
diff changeset
  1109
lemma atLeastPlusOneLessThan_greaterThanLessThan_int:
e28853da5df5 removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents: 15402
diff changeset
  1110
    "{l+1..<u} = {l<..<u::int}"
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1111
  by (auto simp add: atLeastLessThan_def greaterThanLessThan_def)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1112
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1113
subsubsection {* Finiteness *}
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1114
15418
e28853da5df5 removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents: 15402
diff changeset
  1115
lemma image_atLeastZeroLessThan_int: "0 \<le> u ==>
15045
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1116
    {(0::int)..<u} = int ` {..<nat u}"
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1117
  apply (unfold image_def lessThan_def)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1118
  apply auto
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1119
  apply (rule_tac x = "nat x" in exI)
35216
7641e8d831d2 get rid of many duplicate simp rule warnings
huffman
parents: 35171
diff changeset
  1120
  apply (auto simp add: zless_nat_eq_int_zless [THEN sym])
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1121
  done
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1122
15045
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1123
lemma finite_atLeastZeroLessThan_int: "finite {(0::int)..<u}"
47988
e4b69e10b990 tuned proofs;
wenzelm
parents: 47317
diff changeset
  1124
  apply (cases "0 \<le> u")
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1125
  apply (subst image_atLeastZeroLessThan_int, assumption)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1126
  apply (rule finite_imageI)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1127
  apply auto
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1128
  done
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1129
15045
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1130
lemma finite_atLeastLessThan_int [iff]: "finite {l..<u::int}"
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1131
  apply (subgoal_tac "(%x. x + l) ` {0..<u-l} = {l..<u}")
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1132
  apply (erule subst)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1133
  apply (rule finite_imageI)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1134
  apply (rule finite_atLeastZeroLessThan_int)
16733
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
  1135
  apply (rule image_add_int_atLeastLessThan)
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1136
  done
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1137
15418
e28853da5df5 removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents: 15402
diff changeset
  1138
lemma finite_atLeastAtMost_int [iff]: "finite {l..(u::int)}"
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1139
  by (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym], simp)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1140
15418
e28853da5df5 removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents: 15402
diff changeset
  1141
lemma finite_greaterThanAtMost_int [iff]: "finite {l<..(u::int)}"
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1142
  by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1143
15418
e28853da5df5 removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents: 15402
diff changeset
  1144
lemma finite_greaterThanLessThan_int [iff]: "finite {l<..<u::int}"
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1145
  by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1146
24853
aab5798e5a33 added lemmas
nipkow
parents: 24748
diff changeset
  1147
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1148
subsubsection {* Cardinality *}
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1149
15045
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1150
lemma card_atLeastZeroLessThan_int: "card {(0::int)..<u} = nat u"
47988
e4b69e10b990 tuned proofs;
wenzelm
parents: 47317
diff changeset
  1151
  apply (cases "0 \<le> u")
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1152
  apply (subst image_atLeastZeroLessThan_int, assumption)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1153
  apply (subst card_image)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1154
  apply (auto simp add: inj_on_def)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1155
  done
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1156
15045
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1157
lemma card_atLeastLessThan_int [simp]: "card {l..<u} = nat (u - l)"
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1158
  apply (subgoal_tac "card {l..<u} = card {0..<u-l}")
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1159
  apply (erule ssubst, rule card_atLeastZeroLessThan_int)
15045
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1160
  apply (subgoal_tac "(%x. x + l) ` {0..<u-l} = {l..<u}")
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1161
  apply (erule subst)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1162
  apply (rule card_image)
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1163
  apply (simp add: inj_on_def)
16733
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16102
diff changeset
  1164
  apply (rule image_add_int_atLeastLessThan)
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1165
  done
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1166
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1167
lemma card_atLeastAtMost_int [simp]: "card {l..u} = nat (u - l + 1)"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 28853
diff changeset
  1168
apply (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym])
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 28853
diff changeset
  1169
apply (auto simp add: algebra_simps)
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 28853
diff changeset
  1170
done
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1171
15418
e28853da5df5 removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents: 15402
diff changeset
  1172
lemma card_greaterThanAtMost_int [simp]: "card {l<..u} = nat (u - l)"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 28853
diff changeset
  1173
by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp)
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1174
15045
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1175
lemma card_greaterThanLessThan_int [simp]: "card {l<..<u} = nat (u - (l + 1))"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 28853
diff changeset
  1176
by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp)
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1177
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents: 26105
diff changeset
  1178
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
  1179
proof -
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents: 26105
diff changeset
  1180
  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
  1181
  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
  1182
qed
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents: 26105
diff changeset
  1183
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents: 26105
diff changeset
  1184
lemma card_less:
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents: 26105
diff changeset
  1185
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
  1186
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
  1187
proof -
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents: 26105
diff changeset
  1188
  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
  1189
  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
  1190
qed
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents: 26105
diff changeset
  1191
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents: 26105
diff changeset
  1192
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
793618618f78 tuned quotes, antiquotations and whitespace
haftmann
parents: 36846
diff changeset
  1193
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
  1194
apply auto
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents: 26105
diff changeset
  1195
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
  1196
apply auto
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents: 26105
diff changeset
  1197
apply (case_tac x)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents: 26105
diff changeset
  1198
apply auto
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents: 26105
diff changeset
  1199
apply (case_tac xa)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents: 26105
diff changeset
  1200
apply auto
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents: 26105
diff changeset
  1201
apply (case_tac xa)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents: 26105
diff changeset
  1202
apply auto
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents: 26105
diff changeset
  1203
done
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents: 26105
diff changeset
  1204
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents: 26105
diff changeset
  1205
lemma card_less_Suc:
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents: 26105
diff changeset
  1206
  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
  1207
    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
  1208
proof -
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents: 26105
diff changeset
  1209
  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
  1210
  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
  1211
    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
  1212
  have b: "{k \<in> M. k < Suc i} - {0} = {k \<in> M - {0}. k < Suc i}"  by auto
57113
7e95523302e6 New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents: 56949
diff changeset
  1213
  from finite_M_bounded_by_nat[of "\<lambda>x. x \<in> M" "Suc i"] 
7e95523302e6 New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents: 56949
diff changeset
  1214
  have "Suc (card {k. Suc k \<in> M \<and> k < i}) = card (insert 0 ({k \<in> M. k < Suc i} - {0}))"
27656
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents: 26105
diff changeset
  1215
    apply (subst card_insert)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents: 26105
diff changeset
  1216
    apply simp_all
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents: 26105
diff changeset
  1217
    apply (subst b)
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents: 26105
diff changeset
  1218
    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
  1219
    apply simp_all
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents: 26105
diff changeset
  1220
    done
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents: 26105
diff changeset
  1221
  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
  1222
qed
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents: 26105
diff changeset
  1223
14485
ea2707645af8 new material from Avigad
paulson
parents: 14478
diff changeset
  1224
13850
6d1bb3059818 new logical equivalences
paulson
parents: 13735
diff changeset
  1225
subsection {*Lemmas useful with the summation operator setsum*}
6d1bb3059818 new logical equivalences
paulson
parents: 13735
diff changeset
  1226
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16052
diff changeset
  1227
text {* For examples, see Algebra/poly/UnivPoly2.thy *}
13735
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
  1228
14577
dbb95b825244 tuned document;
wenzelm
parents: 14485
diff changeset
  1229
subsubsection {* Disjoint Unions *}
13735
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
  1230
14577
dbb95b825244 tuned document;
wenzelm
parents: 14485
diff changeset
  1231
text {* Singletons and open intervals *}
13735
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
  1232
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
  1233
lemma ivl_disj_un_singleton:
15045
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1234
  "{l::'a::linorder} Un {l<..} = {l..}"
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1235
  "{..<u} Un {u::'a::linorder} = {..u}"
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1236
  "(l::'a::linorder) < u ==> {l} Un {l<..<u} = {l..<u}"
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1237
  "(l::'a::linorder) < u ==> {l<..<u} Un {u} = {l<..u}"
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1238
  "(l::'a::linorder) <= u ==> {l} Un {l<..u} = {l..u}"
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1239
  "(l::'a::linorder) <= u ==> {l..<u} Un {u} = {l..u}"
14398
c5c47703f763 Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents: 13850
diff changeset
  1240
by auto
13735
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
  1241
14577
dbb95b825244 tuned document;
wenzelm
parents: 14485
diff changeset
  1242
text {* One- and two-sided intervals *}
13735
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
  1243
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
  1244
lemma ivl_disj_un_one:
15045
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1245
  "(l::'a::linorder) < u ==> {..l} Un {l<..<u} = {..<u}"
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1246
  "(l::'a::linorder) <= u ==> {..<l} Un {l..<u} = {..<u}"
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1247
  "(l::'a::linorder) <= u ==> {..l} Un {l<..u} = {..u}"
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1248
  "(l::'a::linorder) <= u ==> {..<l} Un {l..u} = {..u}"
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1249
  "(l::'a::linorder) <= u ==> {l<..u} Un {u<..} = {l<..}"
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1250
  "(l::'a::linorder) < u ==> {l<..<u} Un {u..} = {l<..}"
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1251
  "(l::'a::linorder) <= u ==> {l..u} Un {u<..} = {l..}"
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1252
  "(l::'a::linorder) <= u ==> {l..<u} Un {u..} = {l..}"
14398
c5c47703f763 Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents: 13850
diff changeset
  1253
by auto
13735
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
  1254
14577
dbb95b825244 tuned document;
wenzelm
parents: 14485
diff changeset
  1255
text {* Two- and two-sided intervals *}
13735
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
  1256
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
  1257
lemma ivl_disj_un_two:
15045
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1258
  "[| (l::'a::linorder) < m; m <= u |] ==> {l<..<m} Un {m..<u} = {l<..<u}"
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1259
  "[| (l::'a::linorder) <= m; m < u |] ==> {l<..m} Un {m<..<u} = {l<..<u}"
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1260
  "[| (l::'a::linorder) <= m; m <= u |] ==> {l..<m} Un {m..<u} = {l..<u}"
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1261
  "[| (l::'a::linorder) <= m; m < u |] ==> {l..m} Un {m<..<u} = {l..<u}"
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1262
  "[| (l::'a::linorder) < m; m <= u |] ==> {l<..<m} Un {m..u} = {l<..u}"
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1263
  "[| (l::'a::linorder) <= m; m <= u |] ==> {l<..m} Un {m<..u} = {l<..u}"
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1264
  "[| (l::'a::linorder) <= m; m <= u |] ==> {l..<m} Un {m..u} = {l..u}"
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1265
  "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m} Un {m<..u} = {l..u}"
14398
c5c47703f763 Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents: 13850
diff changeset
  1266
by auto
13735
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
  1267
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
  1268
lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
  1269
14577
dbb95b825244 tuned document;
wenzelm
parents: 14485
diff changeset
  1270
subsubsection {* Disjoint Intersections *}
13735
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
  1271
14577
dbb95b825244 tuned document;
wenzelm
parents: 14485
diff changeset
  1272
text {* One- and two-sided intervals *}
13735
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
  1273
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
  1274
lemma ivl_disj_int_one:
15045
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1275
  "{..l::'a::order} Int {l<..<u} = {}"
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1276
  "{..<l} Int {l..<u} = {}"
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1277
  "{..l} Int {l<..u} = {}"
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1278
  "{..<l} Int {l..u} = {}"
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1279
  "{l<..u} Int {u<..} = {}"
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1280
  "{l<..<u} Int {u..} = {}"
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1281
  "{l..u} Int {u<..} = {}"
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1282
  "{l..<u} Int {u..} = {}"
14398
c5c47703f763 Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents: 13850
diff changeset
  1283
  by auto
13735
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
  1284
14577
dbb95b825244 tuned document;
wenzelm
parents: 14485
diff changeset
  1285
text {* Two- and two-sided intervals *}
13735
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
  1286
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
  1287
lemma ivl_disj_int_two:
15045
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1288
  "{l::'a::order<..<m} Int {m..<u} = {}"
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1289
  "{l<..m} Int {m<..<u} = {}"
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1290
  "{l..<m} Int {m..<u} = {}"
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1291
  "{l..m} Int {m<..<u} = {}"
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1292
  "{l<..<m} Int {m..u} = {}"
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1293
  "{l<..m} Int {m<..u} = {}"
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1294
  "{l..<m} Int {m..u} = {}"
d59f7e2e18d3 Moved to new m<..<n syntax for set intervals.
nipkow
parents: 15042
diff changeset
  1295
  "{l..m} Int {m<..u} = {}"
14398
c5c47703f763 Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents: 13850
diff changeset
  1296
  by auto
13735
7de9342aca7a HOL-Algebra partially ported to Isar.
ballarin
parents: 11609
diff changeset
  1297
32456
341c83339aeb tuned the simp rules for Int involving insert and intervals.
nipkow
parents: 32436
diff changeset