src/HOL/List.thy
changeset 35608 db4045d1406e
parent 35603 c0db094d0d80
child 35827 f552152d7747
equal deleted inserted replaced
35607:896f01fe825b 35608:db4045d1406e
   288 "sort_key f xs = foldr (insort_key f) xs []"
   288 "sort_key f xs = foldr (insort_key f) xs []"
   289 
   289 
   290 abbreviation "sort \<equiv> sort_key (\<lambda>x. x)"
   290 abbreviation "sort \<equiv> sort_key (\<lambda>x. x)"
   291 abbreviation "insort \<equiv> insort_key (\<lambda>x. x)"
   291 abbreviation "insort \<equiv> insort_key (\<lambda>x. x)"
   292 
   292 
       
   293 definition insort_insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
       
   294   "insort_insert x xs = (if x \<in> set xs then xs else insort x xs)"
       
   295 
   293 end
   296 end
   294 
   297 
   295 
   298 
   296 subsubsection {* List comprehension *}
   299 subsubsection {* List comprehension *}
   297 
   300 
  3700   also have "... \<le> t"
  3703   also have "... \<le> t"
  3701     using hd_dropWhile[of "?P" xs] le0[THEN preorder_class.le_less_trans, OF i]
  3704     using hd_dropWhile[of "?P" xs] le0[THEN preorder_class.le_less_trans, OF i]
  3702     using hd_conv_nth[of "?dW"] by simp
  3705     using hd_conv_nth[of "?dW"] by simp
  3703   finally show "\<not> t < f x" by simp
  3706   finally show "\<not> t < f x" by simp
  3704 qed
  3707 qed
       
  3708 
       
  3709 lemma set_insort_insert:
       
  3710   "set (insort_insert x xs) = insert x (set xs)"
       
  3711   by (auto simp add: insort_insert_def set_insort)
       
  3712 
       
  3713 lemma distinct_insort_insert:
       
  3714   assumes "distinct xs"
       
  3715   shows "distinct (insort_insert x xs)"
       
  3716   using assms by (induct xs) (auto simp add: insort_insert_def set_insort)
       
  3717 
       
  3718 lemma sorted_insort_insert:
       
  3719   assumes "sorted xs"
       
  3720   shows "sorted (insort_insert x xs)"
       
  3721   using assms by (simp add: insort_insert_def sorted_insort)
  3705 
  3722 
  3706 end
  3723 end
  3707 
  3724 
  3708 lemma sorted_upt[simp]: "sorted[i..<j]"
  3725 lemma sorted_upt[simp]: "sorted[i..<j]"
  3709 by (induct j) (simp_all add:sorted_append)
  3726 by (induct j) (simp_all add:sorted_append)