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)