src/HOL/List.thy
changeset 47841 179b5e7c9803
parent 47640 62bfba15b212
child 48619 558e4e77ce69
equal deleted inserted replaced
47840:732ea1f08e3f 47841:179b5e7c9803
  4481 lemma sorted_list_of_set [simp]:
  4481 lemma sorted_list_of_set [simp]:
  4482   "finite A \<Longrightarrow> set (sorted_list_of_set A) = A \<and> sorted (sorted_list_of_set A) 
  4482   "finite A \<Longrightarrow> set (sorted_list_of_set A) = A \<and> sorted (sorted_list_of_set A) 
  4483     \<and> distinct (sorted_list_of_set A)"
  4483     \<and> distinct (sorted_list_of_set A)"
  4484   by (induct A rule: finite_induct) (simp_all add: set_insort sorted_insort distinct_insort)
  4484   by (induct A rule: finite_induct) (simp_all add: set_insort sorted_insort distinct_insort)
  4485 
  4485 
  4486 lemma sorted_list_of_set_sort_remdups:
  4486 lemma sorted_list_of_set_sort_remdups [code]:
  4487   "sorted_list_of_set (set xs) = sort (remdups xs)"
  4487   "sorted_list_of_set (set xs) = sort (remdups xs)"
  4488 proof -
  4488 proof -
  4489   interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
  4489   interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
  4490   show ?thesis by (simp add: sorted_list_of_set_def sort_conv_fold fold_set_fold_remdups)
  4490   show ?thesis by (simp add: sorted_list_of_set_def sort_conv_fold fold_set_fold_remdups)
  4491 qed
  4491 qed