src/HOL/SetInterval.thy
changeset 14577 dbb95b825244
parent 14485 ea2707645af8
child 14692 b8d6c395c9e2
     1.1 --- a/src/HOL/SetInterval.thy	Fri Apr 16 04:06:52 2004 +0200
     1.2 +++ b/src/HOL/SetInterval.thy	Fri Apr 16 04:07:10 2004 +0200
     1.3 @@ -7,6 +7,8 @@
     1.4  lessThan, greaterThan, atLeast, atMost and two-sided intervals
     1.5  *)
     1.6  
     1.7 +header {* Set intervals *}
     1.8 +
     1.9  theory SetInterval = IntArith:
    1.10  
    1.11  constdefs
    1.12 @@ -145,33 +147,33 @@
    1.13  
    1.14  subsection {*Two-sided intervals*}
    1.15  
    1.16 -(* greaterThanLessThan *)
    1.17 +text {* @{text greaterThanLessThan} *}
    1.18  
    1.19  lemma greaterThanLessThan_iff [simp]:
    1.20    "(i : {)l..u(}) = (l < i & i < u)"
    1.21  by (simp add: greaterThanLessThan_def)
    1.22  
    1.23 -(* atLeastLessThan *)
    1.24 +text {* @{text atLeastLessThan} *}
    1.25  
    1.26  lemma atLeastLessThan_iff [simp]:
    1.27    "(i : {l..u(}) = (l <= i & i < u)"
    1.28  by (simp add: atLeastLessThan_def)
    1.29  
    1.30 -(* greaterThanAtMost *)
    1.31 +text {* @{text greaterThanAtMost} *}
    1.32  
    1.33  lemma greaterThanAtMost_iff [simp]:
    1.34    "(i : {)l..u}) = (l < i & i <= u)"
    1.35  by (simp add: greaterThanAtMost_def)
    1.36  
    1.37 -(* atLeastAtMost *)
    1.38 +text {* @{text atLeastAtMost} *}
    1.39  
    1.40  lemma atLeastAtMost_iff [simp]:
    1.41    "(i : {l..u}) = (l <= i & i <= u)"
    1.42  by (simp add: atLeastAtMost_def)
    1.43  
    1.44 -(* The above four lemmas could be declared as iffs.
    1.45 -   If we do so, a call to blast in Hyperreal/Star.ML, lemma STAR_Int
    1.46 -   seems to take forever (more than one hour). *)
    1.47 +text {* The above four lemmas could be declared as iffs.
    1.48 +  If we do so, a call to blast in Hyperreal/Star.ML, lemma @{text STAR_Int}
    1.49 +  seems to take forever (more than one hour). *}
    1.50  
    1.51  
    1.52  subsection {* Intervals of natural numbers *}
    1.53 @@ -227,7 +229,7 @@
    1.54  lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"
    1.55  by blast
    1.56  
    1.57 -(* Intervals of nats with Suc *)
    1.58 +text {* Intervals of nats with @{text Suc} *}
    1.59  
    1.60  lemma atLeastLessThanSuc_atLeastAtMost: "{l..Suc u(} = {l..u}"
    1.61    by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def)
    1.62 @@ -391,11 +393,11 @@
    1.63  
    1.64  subsection {*Lemmas useful with the summation operator setsum*}
    1.65  
    1.66 -(* For examples, see Algebra/poly/UnivPoly.thy *)
    1.67 +text {* For examples, see Algebra/poly/UnivPoly.thy *}
    1.68  
    1.69 -(** Disjoint Unions **)
    1.70 +subsubsection {* Disjoint Unions *}
    1.71  
    1.72 -(* Singletons and open intervals *)
    1.73 +text {* Singletons and open intervals *}
    1.74  
    1.75  lemma ivl_disj_un_singleton:
    1.76    "{l::'a::linorder} Un {)l..} = {l..}"
    1.77 @@ -406,7 +408,7 @@
    1.78    "(l::'a::linorder) <= u ==> {l..u(} Un {u} = {l..u}"
    1.79  by auto
    1.80  
    1.81 -(* One- and two-sided intervals *)
    1.82 +text {* One- and two-sided intervals *}
    1.83  
    1.84  lemma ivl_disj_un_one:
    1.85    "(l::'a::linorder) < u ==> {..l} Un {)l..u(} = {..u(}"
    1.86 @@ -419,7 +421,7 @@
    1.87    "(l::'a::linorder) <= u ==> {l..u(} Un {u..} = {l..}"
    1.88  by auto
    1.89  
    1.90 -(* Two- and two-sided intervals *)
    1.91 +text {* Two- and two-sided intervals *}
    1.92  
    1.93  lemma ivl_disj_un_two:
    1.94    "[| (l::'a::linorder) < m; m <= u |] ==> {)l..m(} Un {m..u(} = {)l..u(}"
    1.95 @@ -434,9 +436,9 @@
    1.96  
    1.97  lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two
    1.98  
    1.99 -(** Disjoint Intersections **)
   1.100 +subsubsection {* Disjoint Intersections *}
   1.101  
   1.102 -(* Singletons and open intervals *)
   1.103 +text {* Singletons and open intervals *}
   1.104  
   1.105  lemma ivl_disj_int_singleton:
   1.106    "{l::'a::order} Int {)l..} = {}"
   1.107 @@ -447,7 +449,7 @@
   1.108    "{l..u(} Int {u} = {}"
   1.109    by simp+
   1.110  
   1.111 -(* One- and two-sided intervals *)
   1.112 +text {* One- and two-sided intervals *}
   1.113  
   1.114  lemma ivl_disj_int_one:
   1.115    "{..l::'a::order} Int {)l..u(} = {}"
   1.116 @@ -460,7 +462,7 @@
   1.117    "{l..u(} Int {u..} = {}"
   1.118    by auto
   1.119  
   1.120 -(* Two- and two-sided intervals *)
   1.121 +text {* Two- and two-sided intervals *}
   1.122  
   1.123  lemma ivl_disj_int_two:
   1.124    "{)l::'a::order..m(} Int {m..u(} = {}"