src/HOL/List.thy
changeset 44916 840d8c3d9113
parent 44890 22f665a2e91c
child 44921 58eef4843641
equal deleted inserted replaced
44914:f0fd38929d21 44916:840d8c3d9113
  3865   by (induct xs) simp_all
  3865   by (induct xs) simp_all
  3866 
  3866 
  3867 lemma insort_is_Cons: "\<forall>x\<in>set xs. f a \<le> f x \<Longrightarrow> insort_key f a xs = a # xs"
  3867 lemma insort_is_Cons: "\<forall>x\<in>set xs. f a \<le> f x \<Longrightarrow> insort_key f a xs = a # xs"
  3868 by (cases xs) auto
  3868 by (cases xs) auto
  3869 
  3869 
       
  3870 lemma sorted_sort_id: "sorted xs \<Longrightarrow> sort xs = xs"
       
  3871   by (induct xs) (auto simp add: sorted_Cons insort_is_Cons)
       
  3872 
  3870 lemma sorted_map_remove1:
  3873 lemma sorted_map_remove1:
  3871   "sorted (map f xs) \<Longrightarrow> sorted (map f (remove1 x xs))"
  3874   "sorted (map f xs) \<Longrightarrow> sorted (map f (remove1 x xs))"
  3872   by (induct xs) (auto simp add: sorted_Cons)
  3875   by (induct xs) (auto simp add: sorted_Cons)
  3873 
  3876 
  3874 lemma sorted_remove1: "sorted xs \<Longrightarrow> sorted (remove1 a xs)"
  3877 lemma sorted_remove1: "sorted xs \<Longrightarrow> sorted (remove1 a xs)"