src/HOL/SetInterval.thy
 author ballarin Thu Feb 19 15:57:34 2004 +0100 (2004-02-19) changeset 14398 c5c47703f763 parent 13850 6d1bb3059818 child 14418 b62323c85134 permissions -rw-r--r--
Efficient, graph-based reasoner for linear and partial orders.
+ Setup as solver in the HOL simplifier.
 nipkow@8924 ` 1` ```(* Title: HOL/SetInterval.thy ``` nipkow@8924 ` 2` ``` ID: \$Id\$ ``` ballarin@13735 ` 3` ``` Author: Tobias Nipkow and Clemens Ballarin ``` paulson@8957 ` 4` ``` Copyright 2000 TU Muenchen ``` nipkow@8924 ` 5` ballarin@13735 ` 6` ```lessThan, greaterThan, atLeast, atMost and two-sided intervals ``` nipkow@8924 ` 7` ```*) ``` nipkow@8924 ` 8` ballarin@13735 ` 9` ```theory SetInterval = NatArith: ``` nipkow@8924 ` 10` nipkow@8924 ` 11` ```constdefs ``` wenzelm@11609 ` 12` ``` lessThan :: "('a::ord) => 'a set" ("(1{.._'(})") ``` wenzelm@11609 ` 13` ``` "{..u(} == {x. x 'a set" ("(1{.._})") ``` wenzelm@11609 ` 16` ``` "{..u} == {x. x<=u}" ``` nipkow@8924 ` 17` wenzelm@11609 ` 18` ``` greaterThan :: "('a::ord) => 'a set" ("(1{')_..})") ``` wenzelm@11609 ` 19` ``` "{)l..} == {x. l 'a set" ("(1{_..})") ``` wenzelm@11609 ` 22` ``` "{l..} == {x. l<=x}" ``` nipkow@8924 ` 23` ballarin@13735 ` 24` ``` greaterThanLessThan :: "['a::ord, 'a] => 'a set" ("(1{')_.._'(})") ``` ballarin@13735 ` 25` ``` "{)l..u(} == {)l..} Int {..u(}" ``` ballarin@13735 ` 26` ballarin@13735 ` 27` ``` atLeastLessThan :: "['a::ord, 'a] => 'a set" ("(1{_.._'(})") ``` ballarin@13735 ` 28` ``` "{l..u(} == {l..} Int {..u(}" ``` ballarin@13735 ` 29` ballarin@13735 ` 30` ``` greaterThanAtMost :: "['a::ord, 'a] => 'a set" ("(1{')_.._})") ``` ballarin@13735 ` 31` ``` "{)l..u} == {)l..} Int {..u}" ``` ballarin@13735 ` 32` ballarin@13735 ` 33` ``` atLeastAtMost :: "['a::ord, 'a] => 'a set" ("(1{_.._})") ``` ballarin@13735 ` 34` ``` "{l..u} == {l..} Int {..u}" ``` ballarin@13735 ` 35` paulson@13850 ` 36` ```subsection {*lessThan*} ``` ballarin@13735 ` 37` paulson@13850 ` 38` ```lemma lessThan_iff [iff]: "(i: lessThan k) = (i atLeast y) = (y \ (x::'a::order))" ``` paulson@13850 ` 134` ```by (blast intro: order_trans) ``` paulson@13850 ` 135` paulson@13850 ` 136` ```lemma atLeast_eq_iff [iff]: ``` paulson@13850 ` 137` ``` "(atLeast x = atLeast y) = (x = (y::'a::linorder))" ``` paulson@13850 ` 138` ```by (blast intro: order_antisym order_trans) ``` paulson@13850 ` 139` paulson@13850 ` 140` ```lemma greaterThan_subset_iff [iff]: ``` paulson@13850 ` 141` ``` "(greaterThan x \ greaterThan y) = (y \ (x::'a::linorder))" ``` paulson@13850 ` 142` ```apply (auto simp add: greaterThan_def) ``` paulson@13850 ` 143` ``` apply (subst linorder_not_less [symmetric], blast) ``` paulson@13850 ` 144` ```done ``` paulson@13850 ` 145` paulson@13850 ` 146` ```lemma greaterThan_eq_iff [iff]: ``` paulson@13850 ` 147` ``` "(greaterThan x = greaterThan y) = (x = (y::'a::linorder))" ``` paulson@13850 ` 148` ```apply (rule iffI) ``` paulson@13850 ` 149` ``` apply (erule equalityE) ``` paulson@13850 ` 150` ``` apply (simp add: greaterThan_subset_iff order_antisym, simp) ``` paulson@13850 ` 151` ```done ``` paulson@13850 ` 152` paulson@13850 ` 153` ```lemma atMost_subset_iff [iff]: "(atMost x \ atMost y) = (x \ (y::'a::order))" ``` paulson@13850 ` 154` ```by (blast intro: order_trans) ``` paulson@13850 ` 155` paulson@13850 ` 156` ```lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))" ``` paulson@13850 ` 157` ```by (blast intro: order_antisym order_trans) ``` paulson@13850 ` 158` paulson@13850 ` 159` ```lemma lessThan_subset_iff [iff]: ``` paulson@13850 ` 160` ``` "(lessThan x \ lessThan y) = (x \ (y::'a::linorder))" ``` paulson@13850 ` 161` ```apply (auto simp add: lessThan_def) ``` paulson@13850 ` 162` ``` apply (subst linorder_not_less [symmetric], blast) ``` paulson@13850 ` 163` ```done ``` paulson@13850 ` 164` paulson@13850 ` 165` ```lemma lessThan_eq_iff [iff]: ``` paulson@13850 ` 166` ``` "(lessThan x = lessThan y) = (x = (y::'a::linorder))" ``` paulson@13850 ` 167` ```apply (rule iffI) ``` paulson@13850 ` 168` ``` apply (erule equalityE) ``` paulson@13850 ` 169` ``` apply (simp add: lessThan_subset_iff order_antisym, simp) ``` ballarin@13735 ` 170` ```done ``` ballarin@13735 ` 171` ballarin@13735 ` 172` paulson@13850 ` 173` ```subsection {*Combined properties*} ``` ballarin@13735 ` 174` ballarin@13735 ` 175` ```lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}" ``` paulson@13850 ` 176` ```by (blast intro: order_antisym) ``` ballarin@13735 ` 177` paulson@13850 ` 178` ```subsection {*Two-sided intervals*} ``` ballarin@13735 ` 179` ballarin@13735 ` 180` ```(* greaterThanLessThan *) ``` ballarin@13735 ` 181` ballarin@13735 ` 182` ```lemma greaterThanLessThan_iff [simp]: ``` ballarin@13735 ` 183` ``` "(i : {)l..u(}) = (l < i & i < u)" ``` ballarin@13735 ` 184` ```by (simp add: greaterThanLessThan_def) ``` ballarin@13735 ` 185` ballarin@13735 ` 186` ```(* atLeastLessThan *) ``` ballarin@13735 ` 187` ballarin@13735 ` 188` ```lemma atLeastLessThan_iff [simp]: ``` ballarin@13735 ` 189` ``` "(i : {l..u(}) = (l <= i & i < u)" ``` ballarin@13735 ` 190` ```by (simp add: atLeastLessThan_def) ``` ballarin@13735 ` 191` ballarin@13735 ` 192` ```(* greaterThanAtMost *) ``` ballarin@13735 ` 193` ballarin@13735 ` 194` ```lemma greaterThanAtMost_iff [simp]: ``` ballarin@13735 ` 195` ``` "(i : {)l..u}) = (l < i & i <= u)" ``` ballarin@13735 ` 196` ```by (simp add: greaterThanAtMost_def) ``` ballarin@13735 ` 197` ballarin@13735 ` 198` ```(* atLeastAtMost *) ``` ballarin@13735 ` 199` ballarin@13735 ` 200` ```lemma atLeastAtMost_iff [simp]: ``` ballarin@13735 ` 201` ``` "(i : {l..u}) = (l <= i & i <= u)" ``` ballarin@13735 ` 202` ```by (simp add: atLeastAtMost_def) ``` ballarin@13735 ` 203` ballarin@13735 ` 204` ```(* The above four lemmas could be declared as iffs. ``` ballarin@13735 ` 205` ``` If we do so, a call to blast in Hyperreal/Star.ML, lemma STAR_Int ``` ballarin@13735 ` 206` ``` seems to take forever (more than one hour). *) ``` ballarin@13735 ` 207` paulson@13850 ` 208` ```subsection {*Lemmas useful with the summation operator setsum*} ``` paulson@13850 ` 209` ballarin@13735 ` 210` ```(* For examples, see Algebra/poly/UnivPoly.thy *) ``` ballarin@13735 ` 211` ballarin@13735 ` 212` ```(** Disjoint Unions **) ``` ballarin@13735 ` 213` ballarin@13735 ` 214` ```(* Singletons and open intervals *) ``` ballarin@13735 ` 215` ballarin@13735 ` 216` ```lemma ivl_disj_un_singleton: ``` ballarin@13735 ` 217` ``` "{l::'a::linorder} Un {)l..} = {l..}" ``` ballarin@13735 ` 218` ``` "{..u(} Un {u::'a::linorder} = {..u}" ``` ballarin@13735 ` 219` ``` "(l::'a::linorder) < u ==> {l} Un {)l..u(} = {l..u(}" ``` ballarin@13735 ` 220` ``` "(l::'a::linorder) < u ==> {)l..u(} Un {u} = {)l..u}" ``` ballarin@13735 ` 221` ``` "(l::'a::linorder) <= u ==> {l} Un {)l..u} = {l..u}" ``` ballarin@13735 ` 222` ``` "(l::'a::linorder) <= u ==> {l..u(} Un {u} = {l..u}" ``` ballarin@14398 ` 223` ```by auto ``` ballarin@13735 ` 224` ballarin@13735 ` 225` ```(* One- and two-sided intervals *) ``` ballarin@13735 ` 226` ballarin@13735 ` 227` ```lemma ivl_disj_un_one: ``` ballarin@13735 ` 228` ``` "(l::'a::linorder) < u ==> {..l} Un {)l..u(} = {..u(}" ``` ballarin@13735 ` 229` ``` "(l::'a::linorder) <= u ==> {..l(} Un {l..u(} = {..u(}" ``` ballarin@13735 ` 230` ``` "(l::'a::linorder) <= u ==> {..l} Un {)l..u} = {..u}" ``` ballarin@13735 ` 231` ``` "(l::'a::linorder) <= u ==> {..l(} Un {l..u} = {..u}" ``` ballarin@13735 ` 232` ``` "(l::'a::linorder) <= u ==> {)l..u} Un {)u..} = {)l..}" ``` ballarin@13735 ` 233` ``` "(l::'a::linorder) < u ==> {)l..u(} Un {u..} = {)l..}" ``` ballarin@13735 ` 234` ``` "(l::'a::linorder) <= u ==> {l..u} Un {)u..} = {l..}" ``` ballarin@13735 ` 235` ``` "(l::'a::linorder) <= u ==> {l..u(} Un {u..} = {l..}" ``` ballarin@14398 ` 236` ```by auto ``` ballarin@13735 ` 237` ballarin@13735 ` 238` ```(* Two- and two-sided intervals *) ``` ballarin@13735 ` 239` ballarin@13735 ` 240` ```lemma ivl_disj_un_two: ``` ballarin@13735 ` 241` ``` "[| (l::'a::linorder) < m; m <= u |] ==> {)l..m(} Un {m..u(} = {)l..u(}" ``` ballarin@13735 ` 242` ``` "[| (l::'a::linorder) <= m; m < u |] ==> {)l..m} Un {)m..u(} = {)l..u(}" ``` ballarin@13735 ` 243` ``` "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m(} Un {m..u(} = {l..u(}" ``` ballarin@13735 ` 244` ``` "[| (l::'a::linorder) <= m; m < u |] ==> {l..m} Un {)m..u(} = {l..u(}" ``` ballarin@13735 ` 245` ``` "[| (l::'a::linorder) < m; m <= u |] ==> {)l..m(} Un {m..u} = {)l..u}" ``` ballarin@13735 ` 246` ``` "[| (l::'a::linorder) <= m; m <= u |] ==> {)l..m} Un {)m..u} = {)l..u}" ``` ballarin@13735 ` 247` ``` "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m(} Un {m..u} = {l..u}" ``` ballarin@13735 ` 248` ``` "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m} Un {)m..u} = {l..u}" ``` ballarin@14398 ` 249` ```by auto ``` ballarin@13735 ` 250` ballarin@13735 ` 251` ```lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two ``` ballarin@13735 ` 252` ballarin@13735 ` 253` ```(** Disjoint Intersections **) ``` ballarin@13735 ` 254` ballarin@13735 ` 255` ```(* Singletons and open intervals *) ``` ballarin@13735 ` 256` ballarin@13735 ` 257` ```lemma ivl_disj_int_singleton: ``` ballarin@13735 ` 258` ``` "{l::'a::order} Int {)l..} = {}" ``` ballarin@13735 ` 259` ``` "{..u(} Int {u} = {}" ``` ballarin@13735 ` 260` ``` "{l} Int {)l..u(} = {}" ``` ballarin@13735 ` 261` ``` "{)l..u(} Int {u} = {}" ``` ballarin@13735 ` 262` ``` "{l} Int {)l..u} = {}" ``` ballarin@13735 ` 263` ``` "{l..u(} Int {u} = {}" ``` ballarin@13735 ` 264` ``` by simp+ ``` ballarin@13735 ` 265` ballarin@13735 ` 266` ```(* One- and two-sided intervals *) ``` ballarin@13735 ` 267` ballarin@13735 ` 268` ```lemma ivl_disj_int_one: ``` ballarin@13735 ` 269` ``` "{..l::'a::order} Int {)l..u(} = {}" ``` ballarin@13735 ` 270` ``` "{..l(} Int {l..u(} = {}" ``` ballarin@13735 ` 271` ``` "{..l} Int {)l..u} = {}" ``` ballarin@13735 ` 272` ``` "{..l(} Int {l..u} = {}" ``` ballarin@13735 ` 273` ``` "{)l..u} Int {)u..} = {}" ``` ballarin@13735 ` 274` ``` "{)l..u(} Int {u..} = {}" ``` ballarin@13735 ` 275` ``` "{l..u} Int {)u..} = {}" ``` ballarin@13735 ` 276` ``` "{l..u(} Int {u..} = {}" ``` ballarin@14398 ` 277` ``` by auto ``` ballarin@13735 ` 278` ballarin@13735 ` 279` ```(* Two- and two-sided intervals *) ``` ballarin@13735 ` 280` ballarin@13735 ` 281` ```lemma ivl_disj_int_two: ``` ballarin@13735 ` 282` ``` "{)l::'a::order..m(} Int {m..u(} = {}" ``` ballarin@13735 ` 283` ``` "{)l..m} Int {)m..u(} = {}" ``` ballarin@13735 ` 284` ``` "{l..m(} Int {m..u(} = {}" ``` ballarin@13735 ` 285` ``` "{l..m} Int {)m..u(} = {}" ``` ballarin@13735 ` 286` ``` "{)l..m(} Int {m..u} = {}" ``` ballarin@13735 ` 287` ``` "{)l..m} Int {)m..u} = {}" ``` ballarin@13735 ` 288` ``` "{l..m(} Int {m..u} = {}" ``` ballarin@13735 ` 289` ``` "{l..m} Int {)m..u} = {}" ``` ballarin@14398 ` 290` ``` by auto ``` ballarin@13735 ` 291` ballarin@13735 ` 292` ```lemmas ivl_disj_int = ivl_disj_int_singleton ivl_disj_int_one ivl_disj_int_two ``` ballarin@13735 ` 293` nipkow@8924 ` 294` ```end ```