1.1 --- a/src/HOL/List.thy	Thu Jul 31 09:49:21 2008 +0200
     1.2 +++ b/src/HOL/List.thy	Fri Aug 01 12:57:50 2008 +0200
     1.3 @@ -2926,9 +2926,29 @@
     1.4  apply (metis successor_incr leD less_imp_le order_trans)
     1.5  done
     1.6  
     1.7 +lemma sorted_list_of_set_rec2: "i \<le> j \<Longrightarrow>
     1.8 +  sorted_list_of_set {i..successor j} =
     1.9 +  sorted_list_of_set {i..j} @ [successor j]"
    1.10 +apply(simp add:sorted_list_of_set_def upto_def)
    1.11 +apply (rule the1_equality[OF finite_sorted_distinct_unique])
    1.12 + apply (simp add:finite_intvl)
    1.13 +apply(rule the1I2[OF finite_sorted_distinct_unique])
    1.14 + apply (simp add:finite_intvl)
    1.15 +apply (simp add: sorted_append Ball_def expand_set_eq)
    1.16 +apply(rule conjI)
    1.17 +apply (metis eq_iff leD linear not_leE ord_discrete order_trans successor_incr)
    1.18 +apply (metis leD linear order_trans successor_incr)
    1.19 +done
    1.20 +
    1.21  lemma upto_rec[code]: "[i..j] = (if i \<le> j then i # [successor i..j] else [])"
    1.22  by(simp add: upto_def sorted_list_of_set_rec)
    1.23  
    1.24 +lemma upto_empty[simp]: "j < i \<Longrightarrow> [i..j] = []"
    1.25 +by(simp add: upto_rec)
    1.26 +
    1.27 +lemma upto_rec2: "i \<le> j \<Longrightarrow> [i..successor j] = [i..j] @ [successor j]"
    1.28 +by(simp add: upto_def sorted_list_of_set_rec2)
    1.29 +
    1.30  end
    1.31  
    1.32  text{* The integers are an instance of the above class: *}
    1.33 @@ -2937,10 +2957,10 @@
    1.34  begin
    1.35  
    1.36  definition
    1.37 -  successor_int_def: "successor = (%i\<Colon>int. i+1)"
    1.38 +successor_int_def: "successor = (%i\<Colon>int. i+1)"
    1.39  
    1.40  instance
    1.41 -  by intro_classes (simp_all add: successor_int_def)
    1.42 +by intro_classes (simp_all add: successor_int_def)
    1.43  
    1.44  end
    1.45  
    1.46 @@ -2948,6 +2968,9 @@
    1.47  
    1.48  hide (open) const successor
    1.49  
    1.50 +lemma upto_rec2_int: "(i::int) \<le> j \<Longrightarrow> [i..j+1] = [i..j] @ [j+1]"
    1.51 +by(rule upto_rec2[where 'a = int, simplified successor_int_def])
    1.52 +
    1.53  
    1.54  subsubsection {* @{text lists}: the list-forming operator over sets *}
    1.55  
    1.56 @@ -2956,7 +2979,7 @@
    1.57    for A :: "'a set"
    1.58  where
    1.59      Nil [intro!]: "[]: lists A"
    1.60 -  | Cons [intro!,noatp]: "[| a: A;l: lists A|] ==> a#l : lists A"
    1.61 +  | Cons [intro!,noatp]: "[| a: A; l: lists A|] ==> a#l : lists A"
    1.62  
    1.63  inductive_cases listsE [elim!,noatp]: "x#l : lists A"
    1.64  inductive_cases listspE [elim!,noatp]: "listsp A (x # l)"
    1.65 @@ -3619,11 +3642,11 @@
    1.66    "{n..<m} = set [n..<m]"
    1.67  by auto
    1.68  
    1.69 -lemma greaterThanAtMost_upto [code unfold]:
    1.70 +lemma greaterThanAtMost_upt [code unfold]:
    1.71    "{n<..m} = set [Suc n..<Suc m]"
    1.72  by auto
    1.73  
    1.74 -lemma atLeastAtMost_upto [code unfold]:
    1.75 +lemma atLeastAtMost_upt [code unfold]:
    1.76    "{n..m} = set [n..<Suc m]"
    1.77  by auto
    1.78  
    1.79 @@ -3643,9 +3666,35 @@
    1.80    "(\<exists>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..n}. P m)"
    1.81  by auto
    1.82  
    1.83 +lemma setsum_set_distinct_conv_listsum:
    1.84 +  "distinct xs \<Longrightarrow> setsum f (set xs) = listsum (map f xs)"
    1.85 +by (induct xs) simp_all
    1.86 +
    1.87  lemma setsum_set_upt_conv_listsum [code unfold]:
    1.88 -  "setsum f (set [k..<n]) = listsum (map f [k..<n])"
    1.89 -apply(subst atLeastLessThan_upt[symmetric])
    1.90 -by (induct n) simp_all
    1.91 +  "setsum f (set [m..<n]) = listsum (map f [m..<n])"
    1.92 +by (rule setsum_set_distinct_conv_listsum) simp
    1.93 +
    1.94 +
    1.95 +text {* Code for summation over ints. *}
    1.96 +
    1.97 +lemma greaterThanLessThan_upto [code unfold]:
    1.98 +  "{i<..<j::int} = set [i+1..j - 1]"
    1.99 +by auto
   1.100 +
   1.101 +lemma atLeastLessThan_upto [code unfold]:
   1.102 +  "{i..<j::int} = set [i..j - 1]"
   1.103 +by auto
   1.104 +
   1.105 +lemma greaterThanAtMost_upto [code unfold]:
   1.106 +  "{i<..j::int} = set [i+1..j]"
   1.107 +by auto
   1.108 +
   1.109 +lemma atLeastAtMost_upto [code unfold]:
   1.110 +  "{i..j::int} = set [i..j]"
   1.111 +by auto
   1.112 +
   1.113 +lemma setsum_set_upto_conv_listsum [code unfold]:
   1.114 +  "setsum f (set [i..j::int]) = listsum (map f [i..j])"
   1.115 +by (rule setsum_set_distinct_conv_listsum) simp
   1.116  
   1.117  end