src/HOL/Set_Interval.thy
 author nipkow Tue, 05 Mar 2013 10:16:15 +0100 changeset 51334 fd531bd984d8 parent 51329 4a3c453f99a1 child 52380 3cc46b8cca5e permissions -rw-r--r--
 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  33318 ddd97d9dfbfb moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly haftmann parents: 33044 diff changeset  17 imports Int 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  "{.. 'a set" ("(1{.._})") where  25062 af5ef0d4d655 global class syntax haftmann parents: 24853 diff changeset  29  "{..u} == {x. x \ 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 'a set" ("(1{_..})") where  25062 af5ef0d4d655 global class syntax haftmann parents: 24853 diff changeset  37  "{l..} == {x. l\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<.. 'a => 'a set" ("(1{_..<_})") where  af5ef0d4d655 global class syntax haftmann parents: 24853 diff changeset  45  "{l.. '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"{.. '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\ _\_./ _)" [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\ _<_./ _)" [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\ _\_./ _)" [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\ _<_./ _)" [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 \ 'a => 'b set => 'b set" ("(3\(00_ \ _)/ _)" [0, 0, 10] 10)  0e2679025aeb fix syntax precedence declarations for UNION, INTER, SUP, INF huffman parents: 36307 diff changeset  76  "_UNION_less" :: "'a \ 'a => 'b set => 'b set" ("(3\(00_ < _)/ _)" [0, 0, 10] 10)  0e2679025aeb fix syntax precedence declarations for UNION, INTER, SUP, INF huffman parents: 36307 diff changeset  77  "_INTER_le" :: "'a \ 'a => 'b set => 'b set" ("(3\(00_ \ _)/ _)" [0, 0, 10] 10)  0e2679025aeb fix syntax precedence declarations for UNION, INTER, SUP, INF huffman parents: 36307 diff changeset  78  "_INTER_less" :: "'a \ 'a => 'b set => 'b set" ("(3\(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<.. { 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} \ {..< 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 \ atLeast y) = (y \ (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 \ greaterThan y) = (y \ (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 \ atMost y) = (x \ (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 \ lessThan y) = (x \ (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"  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 35828 46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp" blanchet parents: 35644 diff changeset  183 lemma greaterThanLessThan_iff [simp,no_atp]:  25062 af5ef0d4d655 global class syntax haftmann parents: 24853 diff changeset  184  "(i : {l<.. 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  10cd49e0c067 Turned "x <= y ==> sup x y = y" (and relatives) into simp rules nipkow parents: 32408 diff changeset  200 breaks many proofs. Since it only helps blast, it is better to leave well  10cd49e0c067 Turned "x <= y ==> sup x y = y" (and relatives) into simp rules nipkow parents: 32408 diff changeset  201 alone *}  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 <..} \ {..< 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 \ {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} = {} \ (~ 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} \ (~ 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 \ {a.. (~ 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.. (~ 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 \ 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} = {} \ ~ 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} \ ~ 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 \ k ==> {k<.. {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} \ (~ 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} \  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' \ h=h' \ \ l\h \ \ l'\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} \ a = b \ 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}"  0f67561ed5a6 Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton' hoelzl parents: 36755 diff changeset  272  hence "\ (\ a \ b)" unfolding atLeastatMost_empty_iff[symmetric] by simp  0f67561ed5a6 Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton' hoelzl parents: 36755 diff changeset  273  moreover with {a..b} = {c} have "c \ a \ b \ c" by auto  0f67561ed5a6 Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton' hoelzl parents: 36755 diff changeset  274  ultimately show "a = b \ b = c" by auto  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} \ {l'..} = (~ l\h \ l\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} \ {..h'} = (~ l\h \ h\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..} \ {}"  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} \ {}"  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]: "\ UNIV \ {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]: "\ UNIV \ {..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]: "\ {l..} \ {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]: "\ {l..} \ {..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]: "\ UNIV \ {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]: "\ {..h} \ {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]: "\ {..h} \ {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]: "\ 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]: "\ 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]: "\ {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]: "\ {..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]: "\ 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]: "\ {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 51329 4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  376 context inner_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 } = {} \ b \ 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 } \ b \ 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} \ { c .. d } \ (a < b \ c \ a \ b \ 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} \ { c .. d } \ (a < b \ c \ a \ b \ 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} \ { c .. d } \ (a < b \ c \ a \ b \ 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} \ { c ..< d } \ (a \ b \ c \ a \ 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} \ { c ..< d } \ (a < b \ c \ a \ 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} \ { c ..< d } \ (a < b \ c \ a \ b \ 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 42891 e2f473671937 simp rules for empty intervals on dense linear order hoelzl parents: 40703 diff changeset  417 end  e2f473671937 simp rules for empty intervals on dense linear order hoelzl parents: 40703 diff changeset  418 51329 4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  419 context no_top  4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  420 begin  4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  421 51334 fd531bd984d8 more lemmas about intervals nipkow parents: 51329 diff changeset  422 lemma greaterThan_non_empty[simp]: "{x <..} \ {}"  51329 4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  423  using gt_ex[of x] by auto  4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  424 4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  425 end  4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  426 4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  427 context no_bot  4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  428 begin  4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  429 51334 fd531bd984d8 more lemmas about intervals nipkow parents: 51329 diff changeset  430 lemma lessThan_non_empty[simp]: "{..< x} \ {}"  51329 4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  431  using lt_ex[of x] by auto  4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  432 4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  433 end  4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  434 32408 a1a85b0a26f7 new interval lemma nipkow parents: 32400 diff changeset  435 lemma (in linorder) atLeastLessThan_subset_iff:  a1a85b0a26f7 new interval lemma nipkow parents: 32400 diff changeset  436  "{a.. b <= a | c<=a & b<=d"  a1a85b0a26f7 new interval lemma nipkow parents: 32400 diff changeset  437 apply (auto simp:subset_eq Ball_def)  a1a85b0a26f7 new interval lemma nipkow parents: 32400 diff changeset  438 apply(frule_tac x=a in spec)  a1a85b0a26f7 new interval lemma nipkow parents: 32400 diff changeset  439 apply(erule_tac x=d in allE)  a1a85b0a26f7 new interval lemma nipkow parents: 32400 diff changeset  440 apply (simp add: less_imp_le)  a1a85b0a26f7 new interval lemma nipkow parents: 32400 diff changeset  441 done  a1a85b0a26f7 new interval lemma nipkow parents: 32400 diff changeset  442 40703 d1fc454d6735 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image. hoelzl parents: 39302 diff changeset  443 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  444  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  445  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  446  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  447 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  448 d1fc454d6735 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image. hoelzl parents: 39302 diff changeset  449 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  450  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  451  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  452  shows "{a ..< b} = {c ..< d} \ 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  453  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  454 51334 fd531bd984d8 more lemmas about intervals nipkow parents: 51329 diff changeset  455 lemma (in bot) atLeast_eq_UNIV_iff: "{x..} = UNIV \ x = bot"  fd531bd984d8 more lemmas about intervals nipkow parents: 51329 diff changeset  456 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  457 51334 fd531bd984d8 more lemmas about intervals nipkow parents: 51329 diff changeset  458 lemma (in top) atMost_eq_UNIV_iff: "{..x} = UNIV \ x = top"  fd531bd984d8 more lemmas about intervals nipkow parents: 51329 diff changeset  459 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  460 51334 fd531bd984d8 more lemmas about intervals nipkow parents: 51329 diff changeset  461 lemma (in bounded_lattice) atLeastAtMost_eq_UNIV_iff:  fd531bd984d8 more lemmas about intervals nipkow parents: 51329 diff changeset  462  "{x..y} = UNIV \ (x = bot \ y = top)"  fd531bd984d8 more lemmas about intervals nipkow parents: 51329 diff changeset  463 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  464 d63ec23c9125 move auxiliary lemmas from Library/Extended_Reals to HOL image hoelzl parents: 51152 diff changeset  465 32456 341c83339aeb tuned the simp rules for Int involving insert and intervals. nipkow parents: 32436 diff changeset  466 subsubsection {* Intersection *}  341c83339aeb tuned the simp rules for Int involving insert and intervals. nipkow parents: 32436 diff changeset  467 341c83339aeb tuned the simp rules for Int involving insert and intervals. nipkow parents: 32436 diff changeset  468 context linorder  341c83339aeb tuned the simp rules for Int involving insert and intervals. nipkow parents: 32436 diff changeset  469 begin  341c83339aeb tuned the simp rules for Int involving insert and intervals. nipkow parents: 32436 diff changeset  470 341c83339aeb tuned the simp rules for Int involving insert and intervals. nipkow parents: 32436 diff changeset  471 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  472 by auto  341c83339aeb tuned the simp rules for Int involving insert and intervals. nipkow parents: 32436 diff changeset  473 341c83339aeb tuned the simp rules for Int involving insert and intervals. nipkow parents: 32436 diff changeset  474 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  475 by auto  341c83339aeb tuned the simp rules for Int involving insert and intervals. nipkow parents: 32436 diff changeset  476 341c83339aeb tuned the simp rules for Int involving insert and intervals. nipkow parents: 32436 diff changeset  477 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  478 by auto  341c83339aeb tuned the simp rules for Int involving insert and intervals. nipkow parents: 32436 diff changeset  479 341c83339aeb tuned the simp rules for Int involving insert and intervals. nipkow parents: 32436 diff changeset  480 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  481 by auto  341c83339aeb tuned the simp rules for Int involving insert and intervals. nipkow parents: 32436 diff changeset  482 341c83339aeb tuned the simp rules for Int involving insert and intervals. nipkow parents: 32436 diff changeset  483 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  484 by auto  341c83339aeb tuned the simp rules for Int involving insert and intervals. nipkow parents: 32436 diff changeset  485 341c83339aeb tuned the simp rules for Int involving insert and intervals. nipkow parents: 32436 diff changeset  486 lemma Int_atLeastLessThan[simp]: "{a.. {..b} = {.. min a b}"  f18b92f91818 add Int_atMost hoelzl parents: 47988 diff changeset  496  by (auto simp: min_def)  f18b92f91818 add Int_atMost hoelzl parents: 47988 diff changeset  497 32456 341c83339aeb tuned the simp rules for Int involving insert and intervals. nipkow parents: 32436 diff changeset  498 end  341c83339aeb tuned the simp rules for Int involving insert and intervals. nipkow parents: 32436 diff changeset  499 51329 4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  500 context complete_lattice  4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  501 begin  4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  502 4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  503 lemma  4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  504  shows Sup_atLeast[simp]: "Sup {x ..} = top"  4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  505  and Sup_greaterThanAtLeast[simp]: "x < top \ Sup {x <..} = top"  4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  506  and Sup_atMost[simp]: "Sup {.. y} = y"  4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  507  and Sup_atLeastAtMost[simp]: "x \ y \ Sup { x .. y} = y"  4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  508  and Sup_greaterThanAtMost[simp]: "x < y \ Sup { x <.. y} = y"  4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  509  by (auto intro!: Sup_eqI)  4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  510 4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  511 lemma  4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  512  shows Inf_atMost[simp]: "Inf {.. x} = bot"  4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  513  and Inf_atMostLessThan[simp]: "top < x \ Inf {..< x} = bot"  4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  514  and Inf_atLeast[simp]: "Inf {x ..} = x"  4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  515  and Inf_atLeastAtMost[simp]: "x \ y \ Inf { x .. y} = x"  4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  516  and Inf_atLeastLessThan[simp]: "x < y \ Inf { x ..< y} = x"  4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  517  by (auto intro!: Inf_eqI)  4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  518 4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  519 end  4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  520 4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  521 lemma  4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  522  fixes x y :: "'a :: {complete_lattice, inner_dense_linorder}"  4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  523  shows Sup_lessThan[simp]: "Sup {..< y} = y"  4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  524  and Sup_atLeastLessThan[simp]: "x < y \ Sup { x ..< y} = y"  4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  525  and Sup_greaterThanLessThan[simp]: "x < y \ Sup { x <..< y} = y"  4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  526  and Inf_greaterThan[simp]: "Inf {x <..} = x"  4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  527  and Inf_greaterThanAtMost[simp]: "x < y \ Inf { x <.. y} = x"  4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  528  and Inf_greaterThanLessThan[simp]: "x < y \ Inf { x <..< y} = x"  4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot hoelzl parents: 51328 diff changeset  529  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  530 14485 ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  531 subsection {* Intervals of natural numbers *}  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  532 15047 fa62de5862b9 redefining sumr to be a translation to setsum paulson parents: 15045 diff changeset  533 subsubsection {* The Constant @{term lessThan} *}  fa62de5862b9 redefining sumr to be a translation to setsum paulson parents: 15045 diff changeset  534 14485 ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  535 lemma lessThan_0 [simp]: "lessThan (0::nat) = {}"  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  536 by (simp add: lessThan_def)  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  537 ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  538 lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)"  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  539 by (simp add: lessThan_def less_Suc_eq, blast)  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  540 43156 04aaac80183f fixed typo kleing parents: 42901 diff changeset  541 text {* The following proof is convenient in induction proofs where  39072 1030b1a166ef Add lessThan_Suc_eq_insert_0 hoelzl parents: 37664 diff changeset  542 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  543 @{term "{.. Suc  {.. Suc (x - 1)" by auto  1030b1a166ef Add lessThan_Suc_eq_insert_0 hoelzl parents: 37664 diff changeset  549  with x < Suc n show "x = 0" by auto  1030b1a166ef Add lessThan_Suc_eq_insert_0 hoelzl parents: 37664 diff changeset  550 qed  1030b1a166ef Add lessThan_Suc_eq_insert_0 hoelzl parents: 37664 diff changeset  551 14485 ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  552 lemma lessThan_Suc_atMost: "lessThan (Suc k) = atMost k"  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  553 by (simp add: lessThan_def atMost_def less_Suc_eq_le)  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  554 ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  555 lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV"  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  556 by blast  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  557 15047 fa62de5862b9 redefining sumr to be a translation to setsum paulson parents: 15045 diff changeset  558 subsubsection {* The Constant @{term greaterThan} *}  fa62de5862b9 redefining sumr to be a translation to setsum paulson parents: 15045 diff changeset  559 14485 ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  560 lemma greaterThan_0 [simp]: "greaterThan 0 = range Suc"  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  561 apply (simp add: greaterThan_def)  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  562 apply (blast dest: gr0_conv_Suc [THEN iffD1])  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  563 done  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  564 ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  565 lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k - {Suc k}"  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  566 apply (simp add: greaterThan_def)  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  567 apply (auto elim: linorder_neqE)  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  568 done  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  569 ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  570 lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}"  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  571 by blast  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  572 15047 fa62de5862b9 redefining sumr to be a translation to setsum paulson parents: 15045 diff changeset  573 subsubsection {* The Constant @{term atLeast} *}  fa62de5862b9 redefining sumr to be a translation to setsum paulson parents: 15045 diff changeset  574 14485 ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  575 lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV"  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  576 by (unfold atLeast_def UNIV_def, simp)  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  577 ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  578 lemma atLeast_Suc: "atLeast (Suc k) = atLeast k - {k}"  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  579 apply (simp add: atLeast_def)  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  580 apply (simp add: Suc_le_eq)  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  581 apply (simp add: order_le_less, blast)  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  582 done  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  583 ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  584 lemma atLeast_Suc_greaterThan: "atLeast (Suc k) = greaterThan k"  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  585  by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le)  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  586 ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  587 lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV"  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  588 by blast  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  589 15047 fa62de5862b9 redefining sumr to be a translation to setsum paulson parents: 15045 diff changeset  590 subsubsection {* The Constant @{term atMost} *}  fa62de5862b9 redefining sumr to be a translation to setsum paulson parents: 15045 diff changeset  591 14485 ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  592 lemma atMost_0 [simp]: "atMost (0::nat) = {0}"  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  593 by (simp add: atMost_def)  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  594 ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  595 lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)"  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  596 apply (simp add: atMost_def)  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  597 apply (simp add: less_Suc_eq order_le_less, blast)  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  598 done  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  599 ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  600 lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  601 by blast  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  602 15047 fa62de5862b9 redefining sumr to be a translation to setsum paulson parents: 15045 diff changeset  603 subsubsection {* The Constant @{term atLeastLessThan} *}  fa62de5862b9 redefining sumr to be a translation to setsum paulson parents: 15045 diff changeset  604 28068 f6b2d1995171 cleaned up code generation for {.._} and {..<_} nipkow parents: 27656 diff changeset  605 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  606 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  607 in this theory --- the reverse orientation complicates proofs (eg  2f05cb7fed85 added (code) lemmas for setsum and foldl nipkow parents: 24286 diff changeset  608 nontermination). But outside, when the definition of the lhs is rarely  2f05cb7fed85 added (code) lemmas for setsum and foldl nipkow parents: 24286 diff changeset  609 used, the opposite orientation seems preferable because it reduces a  2f05cb7fed85 added (code) lemmas for setsum and foldl nipkow parents: 24286 diff changeset  610 specific concept to a more general one. *}  28068 f6b2d1995171 cleaned up code generation for {.._} and {..<_} nipkow parents: 27656 diff changeset  611 15047 fa62de5862b9 redefining sumr to be a translation to setsum paulson parents: 15045 diff changeset  612 lemma atLeast0LessThan: "{0::nat.. n then insert n {m.. Suc n \ {m..Suc n} = insert (Suc n) {m..n}"  03d4347b071d integrated Jeremy's FiniteLib nipkow parents: 15542 diff changeset  652 by (auto simp add: atLeastAtMost_def)  03d4347b071d integrated Jeremy's FiniteLib nipkow parents: 15542 diff changeset  653 45932 6f08f8fe9752 add lemmas noschinl parents: 44890 diff changeset  654 lemma atLeastAtMost_insertL: "m \ n \ insert m {Suc m..n} = {m ..n}"  6f08f8fe9752 add lemmas noschinl parents: 44890 diff changeset  655 by auto  6f08f8fe9752 add lemmas noschinl parents: 44890 diff changeset  656 43157 b505be6f029a atLeastAtMostSuc_conv on int kleing parents: 43156 diff changeset  657 text {* The analogous result is useful on @{typ int}: *}  b505be6f029a atLeastAtMostSuc_conv on int kleing parents: 43156 diff changeset  658 (* here, because we don't have an own int section *)  b505be6f029a atLeastAtMostSuc_conv on int kleing parents: 43156 diff changeset  659 lemma atLeastAtMostPlus1_int_conv:  b505be6f029a atLeastAtMostSuc_conv on int kleing parents: 43156 diff changeset  660  "m <= 1+n \ {m..1+n} = insert (1+n) {m..n::int}"  b505be6f029a atLeastAtMostSuc_conv on int kleing parents: 43156 diff changeset  661  by (auto intro: set_eqI)  b505be6f029a atLeastAtMostSuc_conv on int kleing parents: 43156 diff changeset  662 33044 fd0a9c794ec1 Some new lemmas concerning sets paulson parents: 32960 diff changeset  663 lemma atLeastLessThan_add_Un: "i \ j \ {i.. {j.. ?B" by auto  236dfafbeb63 linear arithmetic now takes "&" in assumptions apart. nipkow parents: 16102 diff changeset  674 next  236dfafbeb63 linear arithmetic now takes "&" in assumptions apart. nipkow parents: 16102 diff changeset  675  show "?B \ ?A"  236dfafbeb63 linear arithmetic now takes "&" in assumptions apart. nipkow parents: 16102 diff changeset  676  proof  236dfafbeb63 linear arithmetic now takes "&" in assumptions apart. nipkow parents: 16102 diff changeset  677  fix n assume a: "n : ?B"  20217 25b068a99d2b linear arithmetic splits certain operators (e.g. min, max, abs) webertj parents: 19538 diff changeset  678  hence "n - k : {i..j}" by auto  16733 236dfafbeb63 linear arithmetic now takes "&" in assumptions apart. nipkow parents: 16102 diff changeset  679  moreover have "n = (n - k) + k" using a by auto  236dfafbeb63 linear arithmetic now takes "&" in assumptions apart. nipkow parents: 16102 diff changeset  680  ultimately show "n : ?A" by blast  236dfafbeb63 linear arithmetic now takes "&" in assumptions apart. nipkow parents: 16102 diff changeset  681  qed  236dfafbeb63 linear arithmetic now takes "&" in assumptions apart. nipkow parents: 16102 diff changeset  682 qed  236dfafbeb63 linear arithmetic now takes "&" in assumptions apart. nipkow parents: 16102 diff changeset  683 236dfafbeb63 linear arithmetic now takes "&" in assumptions apart. nipkow parents: 16102 diff changeset  684 lemma image_add_atLeastLessThan:  236dfafbeb63 linear arithmetic now takes "&" in assumptions apart. nipkow parents: 16102 diff changeset  685  "(%n::nat. n+k)  {i.. ?B" by auto  236dfafbeb63 linear arithmetic now takes "&" in assumptions apart. nipkow parents: 16102 diff changeset  688 next  236dfafbeb63 linear arithmetic now takes "&" in assumptions apart. nipkow parents: 16102 diff changeset  689  show "?B \ ?A"  236dfafbeb63 linear arithmetic now takes "&" in assumptions apart. nipkow parents: 16102 diff changeset  690  proof  236dfafbeb63 linear arithmetic now takes "&" in assumptions apart. nipkow parents: 16102 diff changeset  691  fix n assume a: "n : ?B"  20217 25b068a99d2b linear arithmetic splits certain operators (e.g. min, max, abs) webertj parents: 19538 diff changeset  692  hence "n - k : {i..i. i - c)  {x ..< y} =  2946b8f057df Instantiate product type as euclidean space. hoelzl parents: 37388 diff changeset  716  (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  717  (is "_ = ?right")  2946b8f057df Instantiate product type as euclidean space. hoelzl parents: 37388 diff changeset  718 proof safe  2946b8f057df Instantiate product type as euclidean space. hoelzl parents: 37388 diff changeset  719  fix a assume a: "a \ ?right"  2946b8f057df Instantiate product type as euclidean space. hoelzl parents: 37388 diff changeset  720  show "a \ (\i. i - c)  {x ..< y}"  2946b8f057df Instantiate product type as euclidean space. hoelzl parents: 37388 diff changeset  721  proof cases  2946b8f057df Instantiate product type as euclidean space. hoelzl parents: 37388 diff changeset  722  assume "c < y" with a show ?thesis  2946b8f057df Instantiate product type as euclidean space. hoelzl parents: 37388 diff changeset  723  by (auto intro!: image_eqI[of _ _ "a + c"])  2946b8f057df Instantiate product type as euclidean space. hoelzl parents: 37388 diff changeset  724  next  2946b8f057df Instantiate product type as euclidean space. hoelzl parents: 37388 diff changeset  725  assume "\ c < y" with a show ?thesis  2946b8f057df Instantiate product type as euclidean space. hoelzl parents: 37388 diff changeset  726  by (auto intro!: image_eqI[of _ _ x] split: split_if_asm)  2946b8f057df Instantiate product type as euclidean space. hoelzl parents: 37388 diff changeset  727  qed  2946b8f057df Instantiate product type as euclidean space. hoelzl parents: 37388 diff changeset  728 qed auto  2946b8f057df Instantiate product type as euclidean space. hoelzl parents: 37388 diff changeset  729 51152 b52cc015429a added lemma Andreas Lochbihler parents: 50999 diff changeset  730 lemma image_int_atLeastLessThan: "int  {a.. uminus  {x<..}"  0f74806cab22 Rewrite rules for images of minus of intervals hoelzl parents: 35216 diff changeset  744  by (rule imageI) (simp add: *)  0f74806cab22 Rewrite rules for images of minus of intervals hoelzl parents: 35216 diff changeset  745  thus "y \ uminus  {x<..}" by simp  0f74806cab22 Rewrite rules for images of minus of intervals hoelzl parents: 35216 diff changeset  746 next  0f74806cab22 Rewrite rules for images of minus of intervals hoelzl parents: 35216 diff changeset  747  fix y assume "y \ -x"  0f74806cab22 Rewrite rules for images of minus of intervals hoelzl parents: 35216 diff changeset  748  have "- (-y) \ uminus  {x..}"  0f74806cab22 Rewrite rules for images of minus of intervals hoelzl parents: 35216 diff changeset  749  by (rule imageI) (insert y \ -x[THEN le_imp_neg_le], simp)  0f74806cab22 Rewrite rules for images of minus of intervals hoelzl parents: 35216 diff changeset  750  thus "y \ uminus  {x..}" by simp  0f74806cab22 Rewrite rules for images of minus of intervals hoelzl parents: 35216 diff changeset  751 qed simp_all  0f74806cab22 Rewrite rules for images of minus of intervals hoelzl parents: 35216 diff changeset  752 0f74806cab22 Rewrite rules for images of minus of intervals hoelzl parents: 35216 diff changeset  753 lemma  0f74806cab22 Rewrite rules for images of minus of intervals hoelzl parents: 35216 diff changeset  754  fixes x :: 'a  0f74806cab22 Rewrite rules for images of minus of intervals hoelzl parents: 35216 diff changeset  755  shows image_uminus_lessThan[simp]: "uminus  {.. finite N"  28068 f6b2d1995171 cleaned up code generation for {.._} and {..<_} nipkow parents: 27656 diff changeset  802 apply (rule finite_subset)  f6b2d1995171 cleaned up code generation for {.._} and {..<_} nipkow parents: 27656 diff changeset  803  apply (rule_tac [2] finite_lessThan, auto)  f6b2d1995171 cleaned up code generation for {.._} and {..<_} nipkow parents: 27656 diff changeset  804 done  f6b2d1995171 cleaned up code generation for {.._} and {..<_} nipkow parents: 27656 diff changeset  805 31044 6896c2498ac0 new lemmas nipkow parents: 31017 diff changeset  806 text {* A set of natural numbers is finite iff it is bounded. *}  6896c2498ac0 new lemmas nipkow parents: 31017 diff changeset  807 lemma finite_nat_set_iff_bounded:  6896c2498ac0 new lemmas nipkow parents: 31017 diff changeset  808  "finite(N::nat set) = (EX m. ALL n:N. nnat. (!!n. n \ f n) ==> finite {n. f n \ u}"  f6b2d1995171 cleaned up code generation for {.._} and {..<_} nipkow parents: 27656 diff changeset  824 by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans)  14485 ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  825 24853 aab5798e5a33 added lemmas nipkow parents: 24748 diff changeset  826 text{* Any subset of an interval of natural numbers the size of the  aab5798e5a33 added lemmas nipkow parents: 24748 diff changeset  827 subset is exactly that interval. *}  aab5798e5a33 added lemmas nipkow parents: 24748 diff changeset  828 aab5798e5a33 added lemmas nipkow parents: 24748 diff changeset  829 lemma subset_card_intvl_is_intvl:  aab5798e5a33 added lemmas nipkow parents: 24748 diff changeset  830  "A <= {k.. A = {k..i\n::nat. M i) = (\i\{1..n}. M i) \ M 0" (is "?A = ?B")  d1b498f2f50b added lemmas nipkow parents: 36365 diff changeset  852 proof  d1b498f2f50b added lemmas nipkow parents: 36365 diff changeset  853  show "?A <= ?B"  d1b498f2f50b added lemmas nipkow parents: 36365 diff changeset  854  proof  d1b498f2f50b added lemmas nipkow parents: 36365 diff changeset  855  fix x assume "x : ?A"  d1b498f2f50b added lemmas nipkow parents: 36365 diff changeset  856  then obtain i where i: "i\n" "x : M i" by auto  d1b498f2f50b added lemmas nipkow parents: 36365 diff changeset  857  show "x : ?B"  d1b498f2f50b added lemmas nipkow parents: 36365 diff changeset  858  proof(cases i)  d1b498f2f50b added lemmas nipkow parents: 36365 diff changeset  859  case 0 with i show ?thesis by simp  d1b498f2f50b added lemmas nipkow parents: 36365 diff changeset  860  next  d1b498f2f50b added lemmas nipkow parents: 36365 diff changeset  861  case (Suc j) with i show ?thesis by auto  d1b498f2f50b added lemmas nipkow parents: 36365 diff changeset  862  qed  d1b498f2f50b added lemmas nipkow parents: 36365 diff changeset  863  qed  d1b498f2f50b added lemmas nipkow parents: 36365 diff changeset  864 next  d1b498f2f50b added lemmas nipkow parents: 36365 diff changeset  865  show "?B <= ?A" by auto  d1b498f2f50b added lemmas nipkow parents: 36365 diff changeset  866 qed  d1b498f2f50b added lemmas nipkow parents: 36365 diff changeset  867 d1b498f2f50b added lemmas nipkow parents: 36365 diff changeset  868 lemma UN_le_add_shift:  d1b498f2f50b added lemmas nipkow parents: 36365 diff changeset  869  "(\i\n::nat. M(i+k)) = (\i\{k..n+k}. M i)" (is "?A = ?B")  d1b498f2f50b added lemmas nipkow parents: 36365 diff changeset  870 proof  44890 22f665a2e91c new fastforce replacing fastsimp - less confusing name nipkow parents: 44008 diff changeset  871  show "?A <= ?B" by fastforce  36755 d1b498f2f50b added lemmas nipkow parents: 36365 diff changeset  872 next  d1b498f2f50b added lemmas nipkow parents: 36365 diff changeset  873  show "?B <= ?A"  d1b498f2f50b added lemmas nipkow parents: 36365 diff changeset  874  proof  d1b498f2f50b added lemmas nipkow parents: 36365 diff changeset  875  fix x assume "x : ?B"  d1b498f2f50b added lemmas nipkow parents: 36365 diff changeset  876  then obtain i where i: "i : {k..n+k}" "x : M(i)" by auto  d1b498f2f50b added lemmas nipkow parents: 36365 diff changeset  877  hence "i-k\n & x : M((i-k)+k)" by auto  d1b498f2f50b added lemmas nipkow parents: 36365 diff changeset  878  thus "x : ?A" by blast  d1b498f2f50b added lemmas nipkow parents: 36365 diff changeset  879  qed  d1b498f2f50b added lemmas nipkow parents: 36365 diff changeset  880 qed  d1b498f2f50b added lemmas nipkow parents: 36365 diff changeset  881 32596 bd68c04dace1 New theorems for proving equalities and inclusions involving unions paulson parents: 32456 diff changeset  882 lemma UN_UN_finite_eq: "(\n::nat. \i\{0..n. A n)"  bd68c04dace1 New theorems for proving equalities and inclusions involving unions paulson parents: 32456 diff changeset  883  by (auto simp add: atLeast0LessThan)  bd68c04dace1 New theorems for proving equalities and inclusions involving unions paulson parents: 32456 diff changeset  884 bd68c04dace1 New theorems for proving equalities and inclusions involving unions paulson parents: 32456 diff changeset  885 lemma UN_finite_subset: "(!!n::nat. (\i\{0.. C) \ (\n. A n) \ C"  bd68c04dace1 New theorems for proving equalities and inclusions involving unions paulson parents: 32456 diff changeset  886  by (subst UN_UN_finite_eq [symmetric]) blast  bd68c04dace1 New theorems for proving equalities and inclusions involving unions paulson parents: 32456 diff changeset  887 33044 fd0a9c794ec1 Some new lemmas concerning sets paulson parents: 32960 diff changeset  888 lemma UN_finite2_subset:  fd0a9c794ec1 Some new lemmas concerning sets paulson parents: 32960 diff changeset  889  "(!!n::nat. (\i\{0.. (\i\{0.. (\n. A n) \ (\n. B n)"  fd0a9c794ec1 Some new lemmas concerning sets paulson parents: 32960 diff changeset  890  apply (rule UN_finite_subset)  fd0a9c794ec1 Some new lemmas concerning sets paulson parents: 32960 diff changeset  891  apply (subst UN_UN_finite_eq [symmetric, of B])  fd0a9c794ec1 Some new lemmas concerning sets paulson parents: 32960 diff changeset  892  apply blast  fd0a9c794ec1 Some new lemmas concerning sets paulson parents: 32960 diff changeset  893  done  32596 bd68c04dace1 New theorems for proving equalities and inclusions involving unions paulson parents: 32456 diff changeset  894 bd68c04dace1 New theorems for proving equalities and inclusions involving unions paulson parents: 32456 diff changeset  895 lemma UN_finite2_eq:  33044 fd0a9c794ec1 Some new lemmas concerning sets paulson parents: 32960 diff changeset  896  "(!!n::nat. (\i\{0..i\{0.. (\n. A n) = (\n. B n)"  fd0a9c794ec1 Some new lemmas concerning sets paulson parents: 32960 diff changeset  897  apply (rule subset_antisym)  fd0a9c794ec1 Some new lemmas concerning sets paulson parents: 32960 diff changeset  898  apply (rule UN_finite2_subset, blast)  fd0a9c794ec1 Some new lemmas concerning sets paulson parents: 32960 diff changeset  899  apply (rule UN_finite2_subset [where k=k])  35216 7641e8d831d2 get rid of many duplicate simp rule warnings huffman parents: 35171 diff changeset  900  apply (force simp add: atLeastLessThan_add_Un [of 0])  33044 fd0a9c794ec1 Some new lemmas concerning sets paulson parents: 32960 diff changeset  901  done  32596 bd68c04dace1 New theorems for proving equalities and inclusions involving unions paulson parents: 32456 diff changeset  902 bd68c04dace1 New theorems for proving equalities and inclusions involving unions paulson parents: 32456 diff changeset  903 14485 ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  904 subsubsection {* Cardinality *}  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  905 15045 d59f7e2e18d3 Moved to new m<.. \h. bij_betw h {0.. \h. bij_betw h M {0.. finite B \ card A = card B \ EX h. bij_betw h A B"  a1c4c1500abe A few finite lemmas nipkow parents: 31044 diff changeset  945 apply(drule ex_bij_betw_finite_nat)  a1c4c1500abe A few finite lemmas nipkow parents: 31044 diff changeset  946 apply(drule ex_bij_betw_nat_finite)  a1c4c1500abe A few finite lemmas nipkow parents: 31044 diff changeset  947 apply(auto intro!:bij_betw_trans)  a1c4c1500abe A few finite lemmas nipkow parents: 31044 diff changeset  948 done  a1c4c1500abe A few finite lemmas nipkow parents: 31044 diff changeset  949 a1c4c1500abe A few finite lemmas nipkow parents: 31044 diff changeset  950 lemma ex_bij_betw_nat_finite_1:  a1c4c1500abe A few finite lemmas nipkow parents: 31044 diff changeset  951  "finite M \ \h. bij_betw h {1 .. card M} M"  a1c4c1500abe A few finite lemmas nipkow parents: 31044 diff changeset  952 by (rule finite_same_card_bij) auto  a1c4c1500abe A few finite lemmas nipkow parents: 31044 diff changeset  953 40703 d1fc454d6735 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image. hoelzl parents: 39302 diff changeset  954 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  955  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  956  shows BIJ: "(\f. bij_betw f A B) \ (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  957 using assms  d1fc454d6735 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image. hoelzl parents: 39302 diff changeset  958 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  959  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  960  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  961  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  962  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  963  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  964  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  965  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  966  thus "(\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  967 qed  d1fc454d6735 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image. hoelzl parents: 39302 diff changeset  968 d1fc454d6735 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image. hoelzl parents: 39302 diff changeset  969 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  970  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  971  shows "(\f. inj_on f A \ f  A \ B) = (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  972 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  973  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  974  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  975  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  976  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  977  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  978  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  979  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  980  moreover  d1fc454d6735 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image. hoelzl parents: 39302 diff changeset  981  {have "{0 ..< card A} \ {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  982  with 2 have "f  A \ {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  983  hence "(g o f)  A \ 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  984  }  d1fc454d6735 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image. hoelzl parents: 39302 diff changeset  985  ultimately show "(\f. inj_on f A \ 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  986 qed (insert assms, auto)  26105 ae06618225ec moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and nipkow parents: 26072 diff changeset  987 14485 ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  988 subsection {* Intervals of integers *}  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  989 15045 d59f7e2e18d3 Moved to new m<.. u ==>  15045 d59f7e2e18d3 Moved to new m<.. u")  14485 ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  1012  apply (subst image_atLeastZeroLessThan_int, assumption)  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  1013  apply (rule finite_imageI)  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  1014  apply auto  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  1015  done  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  1016 15045 d59f7e2e18d3 Moved to new m<.. u")  14485 ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  1039  apply (subst image_atLeastZeroLessThan_int, assumption)  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  1040  apply (subst card_image)  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  1041  apply (auto simp add: inj_on_def)  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  1042  done  ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  1043 15045 d59f7e2e18d3 Moved to new m<.. k < (i::nat)}"  d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework bulwahn parents: 26105 diff changeset  1066 proof -  d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework bulwahn parents: 26105 diff changeset  1067  have "{k. P k \ k < i} \ {.. M"  d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework bulwahn parents: 26105 diff changeset  1073 shows "card {k \ M. k < Suc i} \ 0"  d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework bulwahn parents: 26105 diff changeset  1074 proof -  d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework bulwahn parents: 26105 diff changeset  1075  from zero_in_M have "{k \ M. k < Suc i} \ {}" by auto  d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework bulwahn parents: 26105 diff changeset  1076  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  1077 qed  d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework bulwahn parents: 26105 diff changeset  1078 d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework bulwahn parents: 26105 diff changeset  1079 lemma card_less_Suc2: "0 \ M \ card {k. Suc k \ M \ k < i} = card {k \ M. k < Suc i}"  37388 793618618f78 tuned quotes, antiquotations and whitespace haftmann parents: 36846 diff changeset  1080 apply (rule card_bij_eq [of Suc _ _ "\x. x - Suc 0"])  27656 d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework bulwahn parents: 26105 diff changeset  1081 apply simp  44890 22f665a2e91c new fastforce replacing fastsimp - less confusing name nipkow parents: 44008 diff changeset  1082 apply fastforce  27656 d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework bulwahn parents: 26105 diff changeset  1083 apply auto  d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework bulwahn parents: 26105 diff changeset  1084 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  1085 apply auto  d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework bulwahn parents: 26105 diff changeset  1086 apply (case_tac x)  d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework bulwahn parents: 26105 diff changeset  1087 apply auto  d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework bulwahn parents: 26105 diff changeset  1088 apply (case_tac xa)  d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework bulwahn parents: 26105 diff changeset  1089 apply auto  d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework bulwahn parents: 26105 diff changeset  1090 apply (case_tac xa)  d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework bulwahn parents: 26105 diff changeset  1091 apply auto  d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework bulwahn parents: 26105 diff changeset  1092 done  d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework bulwahn parents: 26105 diff changeset  1093 d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework bulwahn parents: 26105 diff changeset  1094 lemma card_less_Suc:  d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework bulwahn parents: 26105 diff changeset  1095  assumes zero_in_M: "0 \ M"  d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework bulwahn parents: 26105 diff changeset  1096  shows "Suc (card {k. Suc k \ M \ k < i}) = card {k \ M. k < Suc i}"  d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework bulwahn parents: 26105 diff changeset  1097 proof -  d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework bulwahn parents: 26105 diff changeset  1098  from assms have a: "0 \ {k \ 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  1099  hence c: "{k \ M. k < Suc i} = insert 0 ({k \ M. k < Suc i} - {0})"  d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework bulwahn parents: 26105 diff changeset  1100  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  1101  have b: "{k \ M. k < Suc i} - {0} = {k \ M - {0}. k < Suc i}" by auto  d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework bulwahn parents: 26105 diff changeset  1102  from finite_M_bounded_by_nat[of "\x. x \ M" "Suc i"] have "Suc (card {k. Suc k \ M \ k < i}) = card (insert 0 ({k \ M. k < Suc i} - {0}))"  d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework bulwahn parents: 26105 diff changeset  1103  apply (subst card_insert)  d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework bulwahn parents: 26105 diff changeset  1104  apply simp_all  d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework bulwahn parents: 26105 diff changeset  1105  apply (subst b)  d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework bulwahn parents: 26105 diff changeset  1106  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  1107  apply simp_all  d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework bulwahn parents: 26105 diff changeset  1108  done  d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework bulwahn parents: 26105 diff changeset  1109  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  1110 qed  d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework bulwahn parents: 26105 diff changeset  1111 14485 ea2707645af8 new material from Avigad paulson parents: 14478 diff changeset  1112 13850 6d1bb3059818 new logical equivalences paulson parents: 13735 diff changeset  1113 subsection {*Lemmas useful with the summation operator setsum*}  6d1bb3059818 new logical equivalences paulson parents: 13735 diff changeset  1114 16102 c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax. ballarin parents: 16052 diff changeset  1115 text {* For examples, see Algebra/poly/UnivPoly2.thy *}  13735 7de9342aca7a HOL-Algebra partially ported to Isar. ballarin parents: 11609 diff changeset  1116 14577 dbb95b825244 tuned document; wenzelm parents: 14485 diff changeset  1117 subsubsection {* Disjoint Unions *}  13735 7de9342aca7a HOL-Algebra partially ported to Isar. ballarin parents: 11609 diff changeset  1118 14577 dbb95b825244 tuned document; wenzelm parents: 14485 diff changeset  1119 text {* Singletons and open intervals *}  13735 7de9342aca7a HOL-Algebra partially ported to Isar. ballarin parents: 11609 diff changeset  1120 7de9342aca7a HOL-Algebra partially ported to Isar. ballarin parents: 11609 diff changeset  1121 lemma ivl_disj_un_singleton:  15045 d59f7e2e18d3 Moved to new m<.. {l} Un {l<.. {l<.. {l} Un {l<..u} = {l..u}"  d59f7e2e18d3 Moved to new m<.. {l.. {..l} Un {l<.. {.. {..l} Un {l<..u} = {..u}"  d59f7e2e18d3 Moved to new m<.. {.. {l<..u} Un {u<..} = {l<..}"  d59f7e2e18d3 Moved to new m<.. {l<.. {l..u} Un {u<..} = {l..}"  d59f7e2e18d3 Moved to new m<.. {l.. {l<.. {l<..m} Un {m<.. {l.. {l..m} Un {m<.. {l<.. {l<..m} Un {m<..u} = {l<..u}"  d59f7e2e18d3 Moved to new m<.. {l.. {l..m} Un {m<..u} = {l..u}"  14398 c5c47703f763 Efficient, graph-based reasoner for linear and partial orders. ballarin parents: 13850 diff changeset  1154 by auto  13735 7de9342aca7a HOL-Algebra partially ported to Isar. ballarin parents: 11609 diff changeset  1155 7de9342aca7a HOL-Algebra partially ported to Isar. ballarin parents: 11609 diff changeset  1156 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  1157 14577 dbb95b825244 tuned document; wenzelm parents: 14485 diff changeset  1158 subsubsection {* Disjoint Intersections *}  13735 7de9342aca7a HOL-Algebra partially ported to Isar. ballarin parents: 11609 diff changeset  1159 14577 dbb95b825244 tuned document; wenzelm parents: 14485 diff changeset  1160 text {* One- and two-sided intervals *}  13735 7de9342aca7a HOL-Algebra partially ported to Isar. ballarin parents: 11609 diff changeset  1161 7de9342aca7a HOL-Algebra partially ported to Isar. ballarin parents: 11609 diff changeset  1162 lemma ivl_disj_int_one:  15045 d59f7e2e18d3 Moved to new m<.. n \ {i.. {m.. i | m \ i & j \ (n::'a::linorder))"  ee6cd48cf840 more fine tuniung nipkow parents: 15539 diff changeset  1199 apply(auto simp:linorder_not_le)  ee6cd48cf840 more fine tuniung nipkow parents: 15539 diff changeset  1200 apply(rule ccontr)  ee6cd48cf840 more fine tuniung nipkow parents: 15539 diff changeset  1201 apply(insert linorder_le_less_linear[of i n])  ee6cd48cf840 more fine tuniung nipkow parents: 15539 diff changeset  1202 apply(clarsimp simp:linorder_not_le)  44890 22f665a2e91c new fastforce replacing fastsimp - less confusing name nipkow parents: 44008 diff changeset  1203 apply(fastforce)  15542 ee6cd48cf840 more fine tuniung nipkow parents: 15539 diff changeset  1204 done  ee6cd48cf840 more fine tuniung nipkow parents: 15539 diff changeset  1205 15041 a6b1f0cef7b3 Got rid of Summation and made it a translation into setsum instead. nipkow parents: 14846 diff changeset  1206 15042 fa7d27ef7e59 added {0::nat..n(} = {..n(} nipkow parents: 15041 diff changeset  1207 subsection {* Summation indexed over intervals *}  fa7d27ef7e59 added {0::nat..n(} = {..n(} nipkow parents: 15041 diff changeset  1208 fa7d27ef7e59 added {0::nat..n(} = {..n(} nipkow parents: 15041 diff changeset  1209 syntax  fa7d27ef7e59 added {0::nat..n(} = {..n(} nipkow parents: 15041 diff changeset  1210  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10)  15048 11b4dce71d73 more syntax nipkow parents: 15047 diff changeset  1211  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10)  16052 880b0e786c1b tuned setsum rewrites nipkow parents: 16041 diff changeset  1212  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<_./ _)" [0,0,10] 10)  880b0e786c1b tuned setsum rewrites nipkow parents: 16041 diff changeset  1213  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<=_./ _)" [0,0,10] 10)  15042 fa7d27ef7e59 added {0::nat..n(} = {..n(} nipkow parents: 15041 diff changeset  1214 syntax (xsymbols)  fa7d27ef7e59 added {0::nat..n(} = {..n(} nipkow parents: 15041 diff changeset  1215  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  15048 11b4dce71d73 more syntax nipkow parents: 15047 diff changeset  1216  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  16052 880b0e786c1b tuned setsum rewrites nipkow parents: 16041 diff changeset  1217  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  880b0e786c1b tuned setsum rewrites nipkow parents: 16041 diff changeset  1218  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  15042 fa7d27ef7e59 added {0::nat..n(} = {..n(} nipkow parents: 15041 diff changeset  1219 syntax (HTML output)  fa7d27ef7e59 added {0::nat..n(} = {..n(} nipkow parents: 15041 diff changeset  1220  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10)  15048 11b4dce71d73 more syntax nipkow parents: 15047 diff changeset  1221  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10)  16052 880b0e786c1b tuned setsum rewrites nipkow parents: 16041 diff changeset  1222  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10)  880b0e786c1b tuned setsum rewrites nipkow parents: 16041 diff changeset  1223  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10)  15056 b75073d90bff Fine-tuned sum syntax. nipkow parents: 15052 diff changeset  1224 syntax (latex_sum output)  15052 cc562a263609 Added nice latex syntax. nipkow parents: 15048 diff changeset  1225  "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b"  cc562a263609 Added nice latex syntax. nipkow parents: 15048 diff changeset  1226  ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)  cc562a263609 Added nice latex syntax. nipkow parents: 15048 diff changeset  1227  "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b"  cc562a263609 Added nice latex syntax. nipkow parents: 15048 diff changeset  1228  ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10)  16052 880b0e786c1b tuned setsum rewrites nipkow parents: 16041 diff changeset  1229  "_upt_setsum" :: "idt \ 'a \ 'b \ 'b"  880b0e786c1b tuned setsum rewrites nipkow parents: 16041 diff changeset  1230  ("(3\<^raw:$\sum_{>_ < _\<^raw:}$> _)" [0,0,10] 10)  15052 cc562a263609 Added nice latex syntax. nipkow parents: 15048 diff changeset  1231  "_upto_setsum" :: "idt \ 'a \ 'b \ 'b"  16052 880b0e786c1b tuned setsum rewrites nipkow parents: 16041 diff changeset  1232  ("(3\<^raw:$\sum_{>_ \ _\<^raw:}$> _)" [0,0,10] 10)  15041 a6b1f0cef7b3 Got rid of Summation and made it a translation into setsum instead. nipkow parents: 14846 diff changeset  1233 15048 11b4dce71d73 more syntax nipkow parents: 15047 diff changeset  1234 translations  28853 69eb69659bf3 Added new fold operator and renamed the old oe to fold_image. nipkow parents: 28068 diff changeset  1235  "\x=a..b. t" == "CONST setsum (%x. t) {a..b}"  69eb69659bf3 Added new fold operator and renamed the old oe to fold_image. nipkow parents: 28068 diff changeset  1236  "\x=a..i\n. t" == "CONST setsum (\i. t) {..n}"  69eb69659bf3 Added new fold operator and renamed the old oe to fold_image. nipkow parents: 28068 diff changeset  1238  "\ii. t) {..x\{a..b}. e"} & @{term"\x=a..b. e"} & @{term[mode=latex_sum]"\x=a..b. e"}\\  b75073d90bff Fine-tuned sum syntax. nipkow parents: 15052 diff changeset  1246 @{term[source]"\x\{a..x=a..x=a..x\{..b}. e"} & @{term"\x\b. e"} & @{term[mode=latex_sum]"\x\b. e"}\\  15056 b75073d90bff Fine-tuned sum syntax. nipkow parents: 15052 diff changeset  1248 @{term[source]"\x\{..xxx::nat=0..xa = c; b = d; !!x. \ c \ x; x < d \ \ f x = g x \ \  ee6cd48cf840 more fine tuniung nipkow parents: 15539 diff changeset  1271  setsum f {a..i \ Suc n. f i) = (\i \ n. f i) + f(Suc n)"  880b0e786c1b tuned setsum rewrites nipkow parents: 16041 diff changeset  1278 by (simp add:atMost_Suc add_ac)  880b0e786c1b tuned setsum rewrites nipkow parents: 16041 diff changeset  1279 16041 5a8736668ced simplifier trace info; Suc-intervals nipkow parents: 15911 diff changeset  1280 lemma setsum_lessThan_Suc[simp]: "(\i < Suc n. f i) = (\i < n. f i) + f n"  5a8736668ced simplifier trace info; Suc-intervals nipkow parents: 15911 diff changeset  1281 by (simp add:lessThan_Suc add_ac)  15041 a6b1f0cef7b3 Got rid of Summation and made it a translation into setsum instead. nipkow parents: 14846 diff changeset  1282 15911 b730b0edc085 turned 2 lemmas into simp rules nipkow parents: 15561 diff changeset  1283 lemma setsum_cl_ivl_Suc[simp]:  15561 045a07ac35a7 another reorganization of setsums and intervals nipkow parents: 15554 diff changeset  1284  "setsum f {m..Suc n} = (if Suc n < m then 0 else setsum f {m..n} + f(Suc n))"  045a07ac35a7 another reorganization of setsums and intervals nipkow parents: 15554 diff changeset  1285 by (auto simp:add_ac atLeastAtMostSuc_conv)  045a07ac35a7 another reorganization of setsums and intervals nipkow parents: 15554 diff changeset  1286 15911 b730b0edc085 turned 2 lemmas into simp rules nipkow parents: 15561 diff changeset  1287 lemma setsum_op_ivl_Suc[simp]:  15561 045a07ac35a7 another reorganization of setsums and intervals nipkow parents: 15554 diff changeset  1288  "setsum f {m..  045a07ac35a7 another reorganization of setsums and intervals nipkow parents: 15554 diff changeset  1292  (\i=n..m+1. f i) = (\i=n..m. f i) + f(m + 1)"  045a07ac35a7 another reorganization of setsums and intervals nipkow parents: 15554 diff changeset  1293 by (auto simp:add_ac atLeastAtMostSuc_conv)  16041 5a8736668ced simplifier trace info; Suc-intervals nipkow parents: 15911 diff changeset  1294 *)  28068 f6b2d1995171 cleaned up code generation for {.._} and {..<_} nipkow parents: 27656 diff changeset  1295 f6b2d1995171 cleaned up code generation for {.._} and {..<_} nipkow parents: 27656 diff changeset  1296 lemma setsum_head:  f6b2d1995171 cleaned up code generation for {.._} and {..<_} nipkow parents: 27656 diff changeset  1297  fixes n :: nat  f6b2d1995171 cleaned up code generation for {.._} and {..<_} nipkow parents: 27656 diff changeset  1298  assumes mn: "m <= n"  f6b2d1995171 cleaned up code generation for {.._} and {..<_} nipkow parents: 27656 diff changeset  1299  shows "(\x\{m..n}. P x) = P m + (\x\{m<..n}. P x)" (is "?lhs = ?rhs")