1.1 --- a/src/HOL/List.thy	Wed Oct 17 13:55:38 2007 +0200
     1.2 +++ b/src/HOL/List.thy	Wed Oct 17 18:09:38 2007 +0200
     1.3 @@ -2579,11 +2579,43 @@
     1.4  end
     1.5  
     1.6  
     1.7 +subsubsection {* @{text sorted_list_of_set} *}
     1.8 +
     1.9 +text{* This function maps (finite) linearly ordered sets to sorted
    1.10 +lists. Warning: in most cases it is not a good idea to convert from
    1.11 +sets to lists but one should convert in the other direction (via
    1.12 +@{const set}). *}
    1.13 +
    1.14 +
    1.15 +context linorder
    1.16 +begin
    1.17 +
    1.18 +definition
    1.19 + sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
    1.20 +"sorted_list_of_set A == THE xs. set xs = A & sorted xs & distinct xs"
    1.21 +
    1.22 +lemma sorted_list_of_set[simp]: "finite A \<Longrightarrow>
    1.23 +  set(sorted_list_of_set A) = A &
    1.24 +  sorted(sorted_list_of_set A) & distinct(sorted_list_of_set A)"
    1.25 +apply(simp add:sorted_list_of_set_def)
    1.26 +apply(rule the1I2)
    1.27 + apply(simp_all add: finite_sorted_distinct_unique)
    1.28 +done
    1.29 +
    1.30 +lemma sorted_list_of_empty[simp]: "sorted_list_of_set {} = []"
    1.31 +unfolding sorted_list_of_set_def
    1.32 +apply(subst the_equality[of _ "[]"])
    1.33 +apply simp_all
    1.34 +done
    1.35 +
    1.36 +end
    1.37 +
    1.38 +
    1.39  subsubsection {* @{text upto}: the generic interval-list *}
    1.40  
    1.41  class finite_intvl_succ = linorder +
    1.42  fixes successor :: "'a \<Rightarrow> 'a"
    1.43 -assumes finite_intvl: "finite(ord.atLeastAtMost (op \<le>) a b)" (* FIXME should be finite({a..b}) *)
    1.44 +assumes finite_intvl: "finite{a..b}"
    1.45  and successor_incr: "a < successor a"
    1.46  and ord_discrete: "\<not>(\<exists>x. a < x & x < successor a)"
    1.47  
    1.48 @@ -2592,13 +2624,10 @@
    1.49  
    1.50  definition
    1.51   upto :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list" ("(1[_../_])") where
    1.52 -"upto i j == THE is. set is = {i..j} & sorted is & distinct is"
    1.53 -
    1.54 -lemma set_upto[simp]: "set[a..b] = {a..b}"
    1.55 -apply(simp add:upto_def)
    1.56 -apply(rule the1I2)
    1.57 -apply(simp_all add: finite_sorted_distinct_unique finite_intvl)
    1.58 -done
    1.59 +"upto i j == sorted_list_of_set {i..j}"
    1.60 +
    1.61 +lemma upto[simp]: "set[a..b] = {a..b} & sorted[a..b] & distinct[a..b]"
    1.62 +by(simp add:upto_def finite_intvl)
    1.63  
    1.64  lemma insert_intvl: "i \<le> j \<Longrightarrow> insert i {successor i..j} = {i..j}"
    1.65  apply(insert successor_incr[of i])
    1.66 @@ -2606,21 +2635,19 @@
    1.67  apply (metis ord_discrete less_le not_le)
    1.68  done
    1.69  
    1.70 +lemma sorted_list_of_set_rec: "i \<le> j \<Longrightarrow>
    1.71 +  sorted_list_of_set {i..j} = i # sorted_list_of_set {successor i..j}"
    1.72 +apply(simp add:sorted_list_of_set_def upto_def)
    1.73 +apply (rule the1_equality[OF finite_sorted_distinct_unique])
    1.74 + apply (simp add:finite_intvl)
    1.75 +apply(rule the1I2[OF finite_sorted_distinct_unique])
    1.76 + apply (simp add:finite_intvl)
    1.77 +apply (simp add: sorted_Cons insert_intvl Ball_def)
    1.78 +apply (metis successor_incr leD less_imp_le order_trans)
    1.79 +done
    1.80 +
    1.81  lemma upto_rec[code]: "[i..j] = (if i \<le> j then i # [successor i..j] else [])"
    1.82 -proof cases
    1.83 -  assume "i \<le> j" thus ?thesis
    1.84 -    apply(simp add:upto_def)
    1.85 -    apply (rule the1_equality[OF finite_sorted_distinct_unique])
    1.86 -     apply (simp add:finite_intvl)
    1.87 -    apply(rule the1I2[OF finite_sorted_distinct_unique])
    1.88 -     apply (simp add:finite_intvl)
    1.89 -    apply (simp add: sorted_Cons insert_intvl Ball_def)
    1.90 -    apply (metis successor_incr leD less_imp_le order_trans)
    1.91 -    done
    1.92 -next
    1.93 -  assume "~ i \<le> j" thus ?thesis
    1.94 -    by(simp add:upto_def atLeastAtMost_empty cong:conj_cong)
    1.95 -qed
    1.96 +by(simp add: upto_def sorted_list_of_set_rec)
    1.97  
    1.98  end
    1.99