equal
deleted
inserted
replaced
474 by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def |
474 by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def |
475 greaterThanLessThan_def) |
475 greaterThanLessThan_def) |
476 |
476 |
477 lemma atLeastAtMostSuc_conv: "m \<le> Suc n \<Longrightarrow> {m..Suc n} = insert (Suc n) {m..n}" |
477 lemma atLeastAtMostSuc_conv: "m \<le> Suc n \<Longrightarrow> {m..Suc n} = insert (Suc n) {m..n}" |
478 by (auto simp add: atLeastAtMost_def) |
478 by (auto simp add: atLeastAtMost_def) |
|
479 |
|
480 lemma atLeastAtMost_insertL: "m \<le> n \<Longrightarrow> insert m {Suc m..n} = {m ..n}" |
|
481 by auto |
479 |
482 |
480 text {* The analogous result is useful on @{typ int}: *} |
483 text {* The analogous result is useful on @{typ int}: *} |
481 (* here, because we don't have an own int section *) |
484 (* here, because we don't have an own int section *) |
482 lemma atLeastAtMostPlus1_int_conv: |
485 lemma atLeastAtMostPlus1_int_conv: |
483 "m <= 1+n \<Longrightarrow> {m..1+n} = insert (1+n) {m..n::int}" |
486 "m <= 1+n \<Longrightarrow> {m..1+n} = insert (1+n) {m..n::int}" |