src/HOL/SetInterval.thy
changeset 43157 b505be6f029a
parent 43156 04aaac80183f
child 43657 537ea3846f64
equal deleted inserted replaced
43156:04aaac80183f 43157:b505be6f029a
   458   by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def
   458   by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def
   459     greaterThanLessThan_def)
   459     greaterThanLessThan_def)
   460 
   460 
   461 lemma atLeastAtMostSuc_conv: "m \<le> Suc n \<Longrightarrow> {m..Suc n} = insert (Suc n) {m..n}"
   461 lemma atLeastAtMostSuc_conv: "m \<le> Suc n \<Longrightarrow> {m..Suc n} = insert (Suc n) {m..n}"
   462 by (auto simp add: atLeastAtMost_def)
   462 by (auto simp add: atLeastAtMost_def)
       
   463 
       
   464 text {* The analogous result is useful on @{typ int}: *}
       
   465 (* here, because we don't have an own int section *)
       
   466 lemma atLeastAtMostPlus1_int_conv:
       
   467   "m <= 1+n \<Longrightarrow> {m..1+n} = insert (1+n) {m..n::int}"
       
   468   by (auto intro: set_eqI)
   463 
   469 
   464 lemma atLeastLessThan_add_Un: "i \<le> j \<Longrightarrow> {i..<j+k} = {i..<j} \<union> {j..<j+k::nat}"
   470 lemma atLeastLessThan_add_Un: "i \<le> j \<Longrightarrow> {i..<j+k} = {i..<j} \<union> {j..<j+k::nat}"
   465   apply (induct k) 
   471   apply (induct k) 
   466   apply (simp_all add: atLeastLessThanSuc)   
   472   apply (simp_all add: atLeastLessThanSuc)   
   467   done
   473   done