src/HOL/List.thy
changeset 32415 1dddf2f64266
parent 32078 1c14f77201d4
child 32417 e87d9c78910c
     1.1 --- a/src/HOL/List.thy	Wed Aug 26 16:41:37 2009 +0200
     1.2 +++ b/src/HOL/List.thy	Wed Aug 26 19:54:01 2009 +0200
     1.3 @@ -2394,6 +2394,30 @@
     1.4          nth_Cons_number_of [simp] 
     1.5  
     1.6  
     1.7 +subsubsection {* @{text upto}: interval-list on @{typ int} *}
     1.8 +
     1.9 +(* FIXME make upto tail recursive? *)
    1.10 +
    1.11 +function upto :: "int \<Rightarrow> int \<Rightarrow> int list" ("(1[_../_])") where
    1.12 +"upto i j = (if i \<le> j then i # [i+1..j] else [])"
    1.13 +by auto
    1.14 +termination
    1.15 +by(relation "measure(%(i::int,j). nat(j - i + 1))") auto
    1.16 +
    1.17 +declare upto.simps[code, simp del]
    1.18 +
    1.19 +lemmas upto_rec_number_of[simp] =
    1.20 +  upto.simps[of "number_of m" "number_of n", standard]
    1.21 +
    1.22 +lemma upto_empty[simp]: "j < i \<Longrightarrow> [i..j] = []"
    1.23 +by(simp add: upto.simps)
    1.24 +
    1.25 +lemma set_upto[simp]: "set[i..j] = {i..j}"
    1.26 +apply(induct i j rule:upto.induct)
    1.27 +apply(simp add: upto.simps simp_from_to)
    1.28 +done
    1.29 +
    1.30 +
    1.31  subsubsection {* @{text "distinct"} and @{text remdups} *}
    1.32  
    1.33  lemma distinct_append [simp]:
    1.34 @@ -2448,6 +2472,12 @@
    1.35  lemma distinct_upt[simp]: "distinct[i..<j]"
    1.36  by (induct j) auto
    1.37  
    1.38 +lemma distinct_upto[simp]: "distinct[i..j]"
    1.39 +apply(induct i j rule:upto.induct)
    1.40 +apply(subst upto.simps)
    1.41 +apply(simp)
    1.42 +done
    1.43 +
    1.44  lemma distinct_take[simp]: "distinct xs \<Longrightarrow> distinct (take i xs)"
    1.45  apply(induct xs arbitrary: i)
    1.46   apply simp
    1.47 @@ -3091,6 +3121,12 @@
    1.48  lemma sorted_upt[simp]: "sorted[i..<j]"
    1.49  by (induct j) (simp_all add:sorted_append)
    1.50  
    1.51 +lemma sorted_upto[simp]: "sorted[i..j]"
    1.52 +apply(induct i j rule:upto.induct)
    1.53 +apply(subst upto.simps)
    1.54 +apply(simp add:sorted_Cons)
    1.55 +done
    1.56 +
    1.57  
    1.58  subsubsection {* @{text sorted_list_of_set} *}
    1.59  
    1.60 @@ -3124,89 +3160,6 @@
    1.61  end
    1.62  
    1.63  
    1.64 -subsubsection {* @{text upto}: the generic interval-list *}
    1.65 -
    1.66 -class finite_intvl_succ = linorder +
    1.67 -fixes successor :: "'a \<Rightarrow> 'a"
    1.68 -assumes finite_intvl: "finite{a..b}"
    1.69 -and successor_incr: "a < successor a"
    1.70 -and ord_discrete: "\<not>(\<exists>x. a < x & x < successor a)"
    1.71 -
    1.72 -context finite_intvl_succ
    1.73 -begin
    1.74 -
    1.75 -definition
    1.76 - upto :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list" ("(1[_../_])") where
    1.77 -"upto i j == sorted_list_of_set {i..j}"
    1.78 -
    1.79 -lemma upto[simp]: "set[a..b] = {a..b} & sorted[a..b] & distinct[a..b]"
    1.80 -by(simp add:upto_def finite_intvl)
    1.81 -
    1.82 -lemma insert_intvl: "i \<le> j \<Longrightarrow> insert i {successor i..j} = {i..j}"
    1.83 -apply(insert successor_incr[of i])
    1.84 -apply(auto simp: atLeastAtMost_def atLeast_def atMost_def)
    1.85 -apply(metis ord_discrete less_le not_le)
    1.86 -done
    1.87 -
    1.88 -lemma sorted_list_of_set_rec: "i \<le> j \<Longrightarrow>
    1.89 -  sorted_list_of_set {i..j} = i # sorted_list_of_set {successor i..j}"
    1.90 -apply(simp add:sorted_list_of_set_def upto_def)
    1.91 -apply (rule the1_equality[OF finite_sorted_distinct_unique])
    1.92 - apply (simp add:finite_intvl)
    1.93 -apply(rule the1I2[OF finite_sorted_distinct_unique])
    1.94 - apply (simp add:finite_intvl)
    1.95 -apply (simp add: sorted_Cons insert_intvl Ball_def)
    1.96 -apply (metis successor_incr leD less_imp_le order_trans)
    1.97 -done
    1.98 -
    1.99 -lemma sorted_list_of_set_rec2: "i \<le> j \<Longrightarrow>
   1.100 -  sorted_list_of_set {i..successor j} =
   1.101 -  sorted_list_of_set {i..j} @ [successor j]"
   1.102 -apply(simp add:sorted_list_of_set_def upto_def)
   1.103 -apply (rule the1_equality[OF finite_sorted_distinct_unique])
   1.104 - apply (simp add:finite_intvl)
   1.105 -apply(rule the1I2[OF finite_sorted_distinct_unique])
   1.106 - apply (simp add:finite_intvl)
   1.107 -apply (simp add: sorted_append Ball_def expand_set_eq)
   1.108 -apply(rule conjI)
   1.109 -apply (metis eq_iff leD linear not_leE ord_discrete order_trans successor_incr)
   1.110 -apply (metis leD linear order_trans successor_incr)
   1.111 -done
   1.112 -
   1.113 -lemma upto_rec[code]: "[i..j] = (if i \<le> j then i # [successor i..j] else [])"
   1.114 -by(simp add: upto_def sorted_list_of_set_rec)
   1.115 -
   1.116 -lemma upto_empty[simp]: "j < i \<Longrightarrow> [i..j] = []"
   1.117 -by(simp add: upto_rec)
   1.118 -
   1.119 -lemma upto_rec2: "i \<le> j \<Longrightarrow> [i..successor j] = [i..j] @ [successor j]"
   1.120 -by(simp add: upto_def sorted_list_of_set_rec2)
   1.121 -
   1.122 -end
   1.123 -
   1.124 -text{* The integers are an instance of the above class: *}
   1.125 -
   1.126 -instantiation int:: finite_intvl_succ
   1.127 -begin
   1.128 -
   1.129 -definition
   1.130 -successor_int_def[simp]: "successor = (%i\<Colon>int. i+1)"
   1.131 -
   1.132 -instance
   1.133 -by intro_classes (simp_all add: successor_int_def)
   1.134 -
   1.135 -end
   1.136 -
   1.137 -text{* Now @{term"[i..j::int]"} is defined for integers. *}
   1.138 -
   1.139 -hide (open) const successor
   1.140 -
   1.141 -lemma upto_rec2_int: "(i::int) \<le> j \<Longrightarrow> [i..j+1] = [i..j] @ [j+1]"
   1.142 -by(rule upto_rec2[where 'a = int, simplified successor_int_def])
   1.143 -
   1.144 -lemmas upto_rec_number_of_int[simp] = upto_rec[of "number_of m :: int" "number_of n", standard]
   1.145 -
   1.146 -
   1.147  subsubsection {* @{text lists}: the list-forming operator over sets *}
   1.148  
   1.149  inductive_set
   1.150 @@ -3880,9 +3833,7 @@
   1.151    "{i<..j::int} = set [i+1..j]"
   1.152  by auto
   1.153  
   1.154 -lemma atLeastAtMost_upto [code_unfold]:
   1.155 -  "{i..j::int} = set [i..j]"
   1.156 -by auto
   1.157 +lemmas atLeastAtMost_upto [code_unfold] = set_upto[symmetric]
   1.158  
   1.159  lemma setsum_set_upto_conv_listsum [code_unfold]:
   1.160    "setsum f (set [i..j::int]) = listsum (map f [i..j])"