src/HOL/SetInterval.thy
changeset 15047 fa62de5862b9
parent 15045 d59f7e2e18d3
child 15048 11b4dce71d73
     1.1 --- a/src/HOL/SetInterval.thy	Thu Jul 15 13:24:45 2004 +0200
     1.2 +++ b/src/HOL/SetInterval.thy	Thu Jul 15 15:32:32 2004 +0200
     1.3 @@ -192,6 +192,8 @@
     1.4  
     1.5  subsection {* Intervals of natural numbers *}
     1.6  
     1.7 +subsubsection {* The Constant @{term lessThan} *}
     1.8 +
     1.9  lemma lessThan_0 [simp]: "lessThan (0::nat) = {}"
    1.10  by (simp add: lessThan_def)
    1.11  
    1.12 @@ -204,6 +206,8 @@
    1.13  lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV"
    1.14  by blast
    1.15  
    1.16 +subsubsection {* The Constant @{term greaterThan} *}
    1.17 +
    1.18  lemma greaterThan_0 [simp]: "greaterThan 0 = range Suc"
    1.19  apply (simp add: greaterThan_def)
    1.20  apply (blast dest: gr0_conv_Suc [THEN iffD1])
    1.21 @@ -217,6 +221,8 @@
    1.22  lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}"
    1.23  by blast
    1.24  
    1.25 +subsubsection {* The Constant @{term atLeast} *}
    1.26 +
    1.27  lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV"
    1.28  by (unfold atLeast_def UNIV_def, simp)
    1.29  
    1.30 @@ -232,6 +238,8 @@
    1.31  lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV"
    1.32  by blast
    1.33  
    1.34 +subsubsection {* The Constant @{term atMost} *}
    1.35 +
    1.36  lemma atMost_0 [simp]: "atMost (0::nat) = {0}"
    1.37  by (simp add: atMost_def)
    1.38  
    1.39 @@ -243,10 +251,37 @@
    1.40  lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"
    1.41  by blast
    1.42  
    1.43 -lemma atLeast0LessThan [simp]: "{0::nat..<n} = {..<n}"
    1.44 +subsubsection {* The Constant @{term atLeastLessThan} *}
    1.45 +
    1.46 +text{*But not a simprule because some concepts are better left in terms
    1.47 +  of @{term atLeastLessThan}*}
    1.48 +lemma atLeast0LessThan: "{0::nat..<n} = {..<n}"
    1.49  by(simp add:lessThan_def atLeastLessThan_def)
    1.50  
    1.51 -text {* Intervals of nats with @{text Suc} *}
    1.52 +lemma atLeastLessThan0 [simp]: "{m..<0::nat} = {}"
    1.53 +by (simp add: atLeastLessThan_def)
    1.54 +
    1.55 +lemma atLeastLessThan_self [simp]: "{n::'a::order..<n} = {}"
    1.56 +by (auto simp add: atLeastLessThan_def)
    1.57 +
    1.58 +lemma atLeastLessThan_empty: "n \<le> m ==> {m..<n::'a::order} = {}"
    1.59 +by (auto simp add: atLeastLessThan_def)
    1.60 +
    1.61 +subsubsection {* Intervals of nats with @{term Suc} *}
    1.62 +
    1.63 +text{*Not a simprule because the RHS is too messy.*}
    1.64 +lemma atLeastLessThanSuc:
    1.65 +    "{m..<Suc n} = (if m \<le> n then insert n {m..<n} else {})"
    1.66 +by (auto simp add: atLeastLessThan_def) 
    1.67 +
    1.68 +lemma atLeastLessThan_singleton [simp]: "{m..<Suc m} = {m}" 
    1.69 +by (auto simp add: atLeastLessThan_def)
    1.70 +
    1.71 +lemma atLeast_sum_LessThan [simp]: "{m + k..<k::nat} = {}"
    1.72 +by (induct k, simp_all add: atLeastLessThanSuc)
    1.73 +
    1.74 +lemma atLeastSucLessThan [simp]: "{Suc n..<n} = {}"
    1.75 +by (auto simp add: atLeastLessThan_def)
    1.76  
    1.77  lemma atLeastLessThanSuc_atLeastAtMost: "{l..<Suc u} = {l..u}"
    1.78    by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def)
    1.79 @@ -312,7 +347,7 @@
    1.80    apply arith
    1.81    done
    1.82  
    1.83 -lemma card_atLeastAtMost [simp]: "card {l..u} = Suc u - l"
    1.84 +lemma card_atLeastAtMost [simp]: "card {l..u} = Suc u - l"  
    1.85    by (subst atLeastLessThanSuc_atLeastAtMost [THEN sym], simp)
    1.86  
    1.87  lemma card_greaterThanAtMost [simp]: "card {l<..u} = u - l"