equal
deleted
inserted
replaced
3212 upto.simps[of "- numeral m" "- numeral n"] for m n |
3212 upto.simps[of "- numeral m" "- numeral n"] for m n |
3213 |
3213 |
3214 lemma upto_empty[simp]: "j < i \<Longrightarrow> [i..j] = []" |
3214 lemma upto_empty[simp]: "j < i \<Longrightarrow> [i..j] = []" |
3215 by(simp add: upto.simps) |
3215 by(simp add: upto.simps) |
3216 |
3216 |
|
3217 lemma upto_single[simp]: "[i..i] = [i]" |
|
3218 by(simp add: upto.simps) |
|
3219 |
3217 lemma upto_Nil[simp]: "[i..j] = [] \<longleftrightarrow> j < i" |
3220 lemma upto_Nil[simp]: "[i..j] = [] \<longleftrightarrow> j < i" |
3218 by (simp add: upto.simps) |
3221 by (simp add: upto.simps) |
3219 |
3222 |
3220 lemma upto_Nil2[simp]: "[] = [i..j] \<longleftrightarrow> j < i" |
3223 lemma upto_Nil2[simp]: "[] = [i..j] \<longleftrightarrow> j < i" |
3221 by (simp add: upto.simps) |
3224 by (simp add: upto.simps) |