src/HOL/List.thy
changeset 68083 d730a8cfc6e0
parent 68028 1f9f973eed2a
child 68085 7fe53815cce9
equal deleted inserted replaced
68082:b25ccd85b1fd 68083:d730a8cfc6e0
  5605 
  5605 
  5606 lemma sorted_list_of_set_eq_Nil_iff [simp]:
  5606 lemma sorted_list_of_set_eq_Nil_iff [simp]:
  5607   "finite A \<Longrightarrow> sorted_list_of_set A = [] \<longleftrightarrow> A = {}"
  5607   "finite A \<Longrightarrow> sorted_list_of_set A = [] \<longleftrightarrow> A = {}"
  5608 by (auto simp: sorted_list_of_set.remove)
  5608 by (auto simp: sorted_list_of_set.remove)
  5609 
  5609 
  5610 lemma sorted_list_of_set [simp]:
  5610 lemma set_sorted_list_of_set [simp]:
  5611   "finite A \<Longrightarrow> set (sorted_list_of_set A) = A \<and> sorted (sorted_list_of_set A)
  5611   "finite A \<Longrightarrow> set (sorted_list_of_set A) = A"
  5612     \<and> distinct (sorted_list_of_set A)"
  5612 by(induct A rule: finite_induct) (simp_all add: set_insort_key)
  5613 by(induct A rule: finite_induct)
  5613 
  5614   (simp_all add: set_insort_key sorted_insort distinct_insort)
  5614 lemma sorted_sorted_list_of_set [simp]: "sorted (sorted_list_of_set A)"
  5615 
  5615 proof (cases "finite A")
  5616 lemma distinct_sorted_list_of_set:
  5616   case True thus ?thesis by(induction A) (simp_all add: sorted_insort)
  5617   "distinct (sorted_list_of_set A)"
  5617 next
  5618 using sorted_list_of_set by (cases "finite A") auto
  5618   case False thus ?thesis by simp
       
  5619 qed
       
  5620 
       
  5621 lemma distinct_sorted_list_of_set [simp]: "distinct (sorted_list_of_set A)"
       
  5622 proof (cases "finite A")
       
  5623   case True thus ?thesis by(induction A) (simp_all add: distinct_insort)
       
  5624 next
       
  5625   case False thus ?thesis by simp
       
  5626 qed
  5619 
  5627 
  5620 lemma sorted_list_of_set_sort_remdups [code]:
  5628 lemma sorted_list_of_set_sort_remdups [code]:
  5621   "sorted_list_of_set (set xs) = sort (remdups xs)"
  5629   "sorted_list_of_set (set xs) = sort (remdups xs)"
  5622 proof -
  5630 proof -
  5623   interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
  5631   interpret comp_fun_commute insort by (fact comp_fun_commute_insort)