nipkow@8924: (* Title: HOL/SetInterval.thy nipkow@8924: ID: $Id$ ballarin@13735: Author: Tobias Nipkow and Clemens Ballarin paulson@14485: Additions by Jeremy Avigad in March 2004 paulson@8957: Copyright 2000 TU Muenchen nipkow@8924: ballarin@13735: lessThan, greaterThan, atLeast, atMost and two-sided intervals nipkow@8924: *) nipkow@8924: wenzelm@14577: header {* Set intervals *} wenzelm@14577: nipkow@15131: theory SetInterval nipkow@15140: imports IntArith nipkow@15131: begin nipkow@8924: nipkow@8924: constdefs nipkow@15045: lessThan :: "('a::ord) => 'a set" ("(1{..<_})") nipkow@15045: "{.. 'a set" ("(1{.._})") wenzelm@11609: "{..u} == {x. x<=u}" nipkow@8924: nipkow@15045: greaterThan :: "('a::ord) => 'a set" ("(1{_<..})") nipkow@15045: "{l<..} == {x. l 'a set" ("(1{_..})") wenzelm@11609: "{l..} == {x. l<=x}" nipkow@8924: nipkow@15045: greaterThanLessThan :: "['a::ord, 'a] => 'a set" ("(1{_<..<_})") nipkow@15045: "{l<.. 'a set" ("(1{_..<_})") nipkow@15045: "{l.. 'a set" ("(1{_<.._})") nipkow@15045: "{l<..u} == {l<..} Int {..u}" ballarin@13735: ballarin@13735: atLeastAtMost :: "['a::ord, 'a] => 'a set" ("(1{_.._})") ballarin@13735: "{l..u} == {l..} Int {..u}" ballarin@13735: nipkow@15045: (* Old syntax, will disappear! *) nipkow@15045: syntax nipkow@15045: "_lessThan" :: "('a::ord) => 'a set" ("(1{.._'(})") nipkow@15045: "_greaterThan" :: "('a::ord) => 'a set" ("(1{')_..})") nipkow@15045: "_greaterThanLessThan" :: "['a::ord, 'a] => 'a set" ("(1{')_.._'(})") nipkow@15045: "_atLeastLessThan" :: "['a::ord, 'a] => 'a set" ("(1{_.._'(})") nipkow@15045: "_greaterThanAtMost" :: "['a::ord, 'a] => 'a set" ("(1{')_.._})") nipkow@15045: translations nipkow@15045: "{..m(}" => "{.. "{m<..}" nipkow@15045: "{)m..n(}" => "{m<.. "{m.. "{m<..n}" nipkow@15045: nipkow@15048: nipkow@15048: text{* A note of warning when using @{term"{.. nat => 'b set => 'b set" ("(3UN _<=_./ _)" 10) kleing@14418: "@UNION_less" :: "nat => nat => 'b set => 'b set" ("(3UN _<_./ _)" 10) kleing@14418: "@INTER_le" :: "nat => nat => 'b set => 'b set" ("(3INT _<=_./ _)" 10) kleing@14418: "@INTER_less" :: "nat => nat => 'b set => 'b set" ("(3INT _<_./ _)" 10) kleing@14418: kleing@14418: syntax (input) kleing@14418: "@UNION_le" :: "nat => nat => 'b set => 'b set" ("(3\ _\_./ _)" 10) kleing@14418: "@UNION_less" :: "nat => nat => 'b set => 'b set" ("(3\ _<_./ _)" 10) kleing@14418: "@INTER_le" :: "nat => nat => 'b set => 'b set" ("(3\ _\_./ _)" 10) kleing@14418: "@INTER_less" :: "nat => nat => 'b set => 'b set" ("(3\ _<_./ _)" 10) kleing@14418: kleing@14418: syntax (xsymbols) wenzelm@14846: "@UNION_le" :: "nat \ nat => 'b set => 'b set" ("(3\(00\<^bsub>_ \ _\<^esub>)/ _)" 10) wenzelm@14846: "@UNION_less" :: "nat \ nat => 'b set => 'b set" ("(3\(00\<^bsub>_ < _\<^esub>)/ _)" 10) wenzelm@14846: "@INTER_le" :: "nat \ nat => 'b set => 'b set" ("(3\(00\<^bsub>_ \ _\<^esub>)/ _)" 10) wenzelm@14846: "@INTER_less" :: "nat \ nat => 'b set => 'b set" ("(3\(00\<^bsub>_ < _\<^esub>)/ _)" 10) kleing@14418: kleing@14418: translations kleing@14418: "UN i<=n. A" == "UN i:{..n}. A" nipkow@15045: "UN i atLeast y) = (y \ (x::'a::order))" paulson@15418: by (blast intro: order_trans) paulson@13850: paulson@13850: lemma atLeast_eq_iff [iff]: paulson@15418: "(atLeast x = atLeast y) = (x = (y::'a::linorder))" paulson@13850: by (blast intro: order_antisym order_trans) paulson@13850: paulson@13850: lemma greaterThan_subset_iff [iff]: paulson@15418: "(greaterThan x \ greaterThan y) = (y \ (x::'a::linorder))" paulson@15418: apply (auto simp add: greaterThan_def) paulson@15418: apply (subst linorder_not_less [symmetric], blast) paulson@13850: done paulson@13850: paulson@13850: lemma greaterThan_eq_iff [iff]: paulson@15418: "(greaterThan x = greaterThan y) = (x = (y::'a::linorder))" paulson@15418: apply (rule iffI) paulson@15418: apply (erule equalityE) paulson@15418: apply (simp_all add: greaterThan_subset_iff) paulson@13850: done paulson@13850: paulson@15418: lemma atMost_subset_iff [iff]: "(atMost x \ atMost y) = (x \ (y::'a::order))" paulson@13850: by (blast intro: order_trans) paulson@13850: paulson@15418: lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))" paulson@13850: by (blast intro: order_antisym order_trans) paulson@13850: paulson@13850: lemma lessThan_subset_iff [iff]: paulson@15418: "(lessThan x \ lessThan y) = (x \ (y::'a::linorder))" paulson@15418: apply (auto simp add: lessThan_def) paulson@15418: apply (subst linorder_not_less [symmetric], blast) paulson@13850: done paulson@13850: paulson@13850: lemma lessThan_eq_iff [iff]: paulson@15418: "(lessThan x = lessThan y) = (x = (y::'a::linorder))" paulson@15418: apply (rule iffI) paulson@15418: apply (erule equalityE) paulson@15418: apply (simp_all add: lessThan_subset_iff) ballarin@13735: done ballarin@13735: ballarin@13735: paulson@13850: subsection {*Two-sided intervals*} ballarin@13735: ballarin@13735: lemma greaterThanLessThan_iff [simp]: nipkow@15045: "(i : {l<.. {m::'a::order..n} = {}"; nipkow@15554: by (auto simp add: atLeastAtMost_def atMost_def atLeast_def); nipkow@15554: nipkow@15554: lemma atLeastLessThan_empty[simp]: "n \ m ==> {m.. n then insert n {m.. Suc n \ {m..Suc n} = insert (Suc n) {m..n}" nipkow@15554: by (auto simp add: atLeastAtMost_def) nipkow@15554: paulson@14485: subsubsection {* Finiteness *} paulson@14485: nipkow@15045: lemma finite_lessThan [iff]: fixes k :: nat shows "finite {.. finite N" paulson@14485: -- {* A bounded set of natural numbers is finite. *} paulson@14485: apply (rule finite_subset) paulson@14485: apply (rule_tac [2] finite_lessThan, auto) paulson@14485: done paulson@14485: paulson@14485: subsubsection {* Cardinality *} paulson@14485: nipkow@15045: lemma card_lessThan [simp]: "card {.. u ==> nipkow@15045: {(0::int).. u") paulson@14485: apply (subst image_atLeastZeroLessThan_int, assumption) paulson@14485: apply (rule finite_imageI) paulson@14485: apply auto paulson@14485: done paulson@14485: paulson@15418: lemma image_atLeastLessThan_int_shift: nipkow@15045: "(%x. x + (l::int)) ` {0.. u") paulson@14485: apply (subst image_atLeastZeroLessThan_int, assumption) paulson@14485: apply (subst card_image) paulson@14485: apply (auto simp add: inj_on_def) paulson@14485: done paulson@14485: nipkow@15045: lemma card_atLeastLessThan_int [simp]: "card {l.. {l} Un {l<.. {l<.. {l} Un {l<..u} = {l..u}" nipkow@15045: "(l::'a::linorder) <= u ==> {l.. {..l} Un {l<.. {.. {..l} Un {l<..u} = {..u}" nipkow@15045: "(l::'a::linorder) <= u ==> {.. {l<..u} Un {u<..} = {l<..}" nipkow@15045: "(l::'a::linorder) < u ==> {l<.. {l..u} Un {u<..} = {l..}" nipkow@15045: "(l::'a::linorder) <= u ==> {l.. {l<.. {l<..m} Un {m<.. {l.. {l..m} Un {m<.. {l<.. {l<..m} Un {m<..u} = {l<..u}" nipkow@15045: "[| (l::'a::linorder) <= m; m <= u |] ==> {l.. {l..m} Un {m<..u} = {l..u}" ballarin@14398: by auto ballarin@13735: ballarin@13735: lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two ballarin@13735: wenzelm@14577: subsubsection {* Disjoint Intersections *} ballarin@13735: wenzelm@14577: text {* Singletons and open intervals *} ballarin@13735: ballarin@13735: lemma ivl_disj_int_singleton: nipkow@15045: "{l::'a::order} Int {l<..} = {}" nipkow@15045: "{.. n \ {i.. {m.. i | m \ i & j \ (n::'a::linorder))" nipkow@15542: apply(auto simp:linorder_not_le) nipkow@15542: apply(rule ccontr) nipkow@15542: apply(insert linorder_le_less_linear[of i n]) nipkow@15542: apply(clarsimp simp:linorder_not_le) nipkow@15542: apply(fastsimp) nipkow@15542: done nipkow@15542: nipkow@15041: nipkow@15042: subsection {* Summation indexed over intervals *} nipkow@15042: nipkow@15042: syntax nipkow@15042: "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10) nipkow@15048: "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10) nipkow@15048: "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<_./ _)" [0,0,10] 10) nipkow@15042: syntax (xsymbols) nipkow@15042: "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10) nipkow@15048: "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10) nipkow@15048: "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10) nipkow@15042: syntax (HTML output) nipkow@15042: "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10) nipkow@15048: "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10) nipkow@15048: "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10) nipkow@15056: syntax (latex_sum output) nipkow@15052: "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" nipkow@15052: ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10) nipkow@15052: "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" nipkow@15052: ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10) nipkow@15052: "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" nipkow@15052: ("(3\<^raw:$\sum_{>_ < _\<^raw:}$> _)" [0,0,10] 10) nipkow@15041: nipkow@15048: translations nipkow@15048: "\x=a..b. t" == "setsum (%x. t) {a..b}" nipkow@15048: "\x=a..ii. t) {..x\{a..b}. e"} & @{term"\x=a..b. e"} & @{term[mode=latex_sum]"\x=a..b. e"}\\ nipkow@15056: @{term[source]"\x\{a..x=a..x=a..x\{..xxx::nat=0..xa = c; b = d; !!x. \ c \ x; x < d \ \ f x = g x \ \ nipkow@15542: setsum f {a..i < Suc n. b i) = b n + (\i < n. b i)" nipkow@15041: by (simp add:lessThan_Suc) nipkow@15554: *) nipkow@15041: nipkow@15911: lemma setsum_cl_ivl_Suc[simp]: nipkow@15561: "setsum f {m..Suc n} = (if Suc n < m then 0 else setsum f {m..n} + f(Suc n))" nipkow@15561: by (auto simp:add_ac atLeastAtMostSuc_conv) nipkow@15561: nipkow@15911: lemma setsum_op_ivl_Suc[simp]: nipkow@15561: "setsum f {m.. nipkow@15561: (\i=n..m+1. f i) = (\i=n..m. f i) + f(m + 1)" nipkow@15561: by (auto simp:add_ac atLeastAtMostSuc_conv) nipkow@15561: nipkow@15539: lemma setsum_add_nat_ivl: "\ m \ n; n \ p \ \ nipkow@15539: setsum f {m.. 'a::ab_group_add" nipkow@15539: shows "\ m \ n; n \ p \ \ nipkow@15539: setsum f {m..