# HG changeset patch # User nipkow # Date 1247654681 -7200 # Node ID c369417be0552fbebb647b51d719e1d482a4ceec # Parent 6ef7056e5215cfc11cbf2c4c23f5a28c70aa4e26 made upt/upto executable on nat/int by simp diff -r 6ef7056e5215 -r c369417be055 src/HOL/List.thy --- a/src/HOL/List.thy Tue Jul 14 12:18:52 2009 +0200 +++ b/src/HOL/List.thy Wed Jul 15 12:44:41 2009 +0200 @@ -2268,6 +2268,8 @@ -- {* simp does not terminate! *} by (induct j) auto +lemmas upt_rec_number_of[simp] = upt_rec[of "number_of m" "number_of n", standard] + lemma upt_conv_Nil [simp]: "j <= i ==> [i.. j \ [i..j+1] = [i..j] @ [j+1]" by(rule upto_rec2[where 'a = int, simplified successor_int_def]) +lemmas upto_rec_number_of_int[simp] = upto_rec[of "number_of m :: int" "number_of n", standard] + subsubsection {* @{text lists}: the list-forming operator over sets *}