src/HOL/List.thy
 changeset 54868 bab6cade3cc5 parent 54863 82acc20ded73 child 54885 3a478d0a0e87
```     1.1 --- a/src/HOL/List.thy	Thu Dec 26 22:47:49 2013 +0100
1.2 +++ b/src/HOL/List.thy	Fri Dec 27 14:35:14 2013 +0100
1.3 @@ -5018,10 +5018,13 @@
1.4  sets to lists but one should convert in the other direction (via
1.5  @{const set}). *}
1.6
1.7 -definition (in linorder) sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
1.8 +context linorder
1.9 +begin
1.10 +
1.11 +definition sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
1.12    "sorted_list_of_set = folding.F insort []"
1.13
1.14 -sublocale linorder < sorted_list_of_set!: folding insort Nil
1.15 +sublocale sorted_list_of_set!: folding insort Nil
1.16  where
1.17    "folding.F insort [] = sorted_list_of_set"
1.18  proof -
1.19 @@ -5030,21 +5033,17 @@
1.20    show "folding.F insort [] = sorted_list_of_set" by (simp only: sorted_list_of_set_def)
1.21  qed
1.22
1.23 -context linorder
1.24 -begin
1.25 -
1.26  lemma sorted_list_of_set_empty:
1.27    "sorted_list_of_set {} = []"
1.28    by (fact sorted_list_of_set.empty)
1.29
1.30  lemma sorted_list_of_set_insert [simp]:
1.31 -  assumes "finite A"
1.32 -  shows "sorted_list_of_set (insert x A) = insort x (sorted_list_of_set (A - {x}))"
1.33 -  using assms by (fact sorted_list_of_set.insert_remove)
1.34 +  "finite A \<Longrightarrow> sorted_list_of_set (insert x A) = insort x (sorted_list_of_set (A - {x}))"
1.35 +  by (fact sorted_list_of_set.insert_remove)
1.36
1.37  lemma sorted_list_of_set_eq_Nil_iff [simp]:
1.38    "finite A \<Longrightarrow> sorted_list_of_set A = [] \<longleftrightarrow> A = {}"
1.39 -  using assms by (auto simp: sorted_list_of_set.remove)
1.40 +  by (auto simp: sorted_list_of_set.remove)
1.41
1.42  lemma sorted_list_of_set [simp]:
1.43    "finite A \<Longrightarrow> set (sorted_list_of_set A) = A \<and> sorted (sorted_list_of_set A)
```