src/HOL/List.thy

 
 text \<open>A sorted predicate w.r.t. a relation:\<close>
 
 fun sorted_wrt :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
 "sorted_wrt P [] = True" |
-"sorted_wrt P [x] = True" |
-"sorted_wrt P (x # y # zs) = (P x y \<and> sorted_wrt P (y # zs))"
+"sorted_wrt P (x # ys) = ((\<forall>y \<in> set ys. P x y) \<and> sorted_wrt P ys)"
 
 (* FIXME: define sorted in terms of sorted_wrt *)
 
 text \<open>A class-based sorted predicate:\<close>
 
 context linorder
 begin
 
 fun sorted :: "'a list \<Rightarrow> bool" where
 "sorted [] = True" |
-"sorted [x] = True" |
-"sorted (x # y # zs) = (x \<le> y \<and> sorted (y # zs))"
+"sorted (x # ys) = ((\<forall>y \<in> set ys. x \<le> y) \<and> sorted ys)"
 
 lemma sorted_sorted_wrt: "sorted = sorted_wrt (\<le>)"
 proof (rule ext)
   fix xs show "sorted xs = sorted_wrt (\<le>) xs"
     by(induction xs rule: sorted.induct) auto

 subsection \<open>Sorting\<close>
 
 
 subsubsection \<open>@{const sorted_wrt}\<close>
 
-lemma sorted_wrt_Cons:
-assumes "transp P"
-shows   "sorted_wrt P (x # xs) = ((\<forall>y \<in> set xs. P x y) \<and> sorted_wrt P xs)"
-by(induction xs arbitrary: x)(auto intro: transpD[OF assms])
-
 lemma sorted_wrt_ConsI:
   "\<lbrakk> \<And>y. y \<in> set xs \<Longrightarrow> P x y; sorted_wrt P xs \<rbrakk> \<Longrightarrow> sorted_wrt P (x # xs)"
-by (induction xs rule: induct_list012) simp_all
+by (induction xs) simp_all
 
 lemma sorted_wrt_append:
-assumes "transp P"
-shows "sorted_wrt P (xs @ ys) \<longleftrightarrow>
+  "sorted_wrt P (xs @ ys) \<longleftrightarrow>
   sorted_wrt P xs \<and> sorted_wrt P ys \<and> (\<forall>x\<in>set xs. \<forall>y\<in>set ys. P x y)"
-by (induction xs) (auto simp: sorted_wrt_Cons[OF assms])
-
-lemma sorted_wrt_backwards:
-  "sorted_wrt P (xs @ [y, z]) = (P y z \<and> sorted_wrt P (xs @ [y]))"
-by (induction xs rule: induct_list012) auto
+by (induction xs) auto
 
 lemma sorted_wrt_rev:
   "sorted_wrt P (rev xs) = sorted_wrt (\<lambda>x y. P y x) xs"
-by (induction xs rule: induct_list012) (simp_all add: sorted_wrt_backwards)
+by (induction xs) (auto simp add: sorted_wrt_append)
 
 lemma sorted_wrt_mono:
   "(\<And>x y. P x y \<Longrightarrow> Q x y) \<Longrightarrow> sorted_wrt P xs \<Longrightarrow> sorted_wrt Q xs"
-by(induction xs rule: induct_list012)(auto)
+by(induction xs)(auto)
 
 lemma sorted_wrt01: "length xs \<le> 1 \<Longrightarrow> sorted_wrt P xs"
 by(auto simp: le_Suc_eq length_Suc_conv)
 
 text \<open>Strictly Ascending Sequences of Natural Numbers\<close>

 subsubsection \<open>@{const sorted}\<close>
 
 context linorder
 begin
 
-lemma sorted_Cons: "sorted (x#xs) = (sorted xs \<and> (\<forall>y \<in> set xs. x \<le> y))"
-apply(induction xs arbitrary: x)
- apply simp
-by simp (blast intro: order_trans)
-(*
-lemma sorted_iff_wrt: "sorted xs = sorted_wrt (\<le>) xs"
-proof
-  assume "sorted xs" thus "sorted_wrt (\<le>) xs"
-  proof (induct xs rule: sorted.induct)
-    case (Cons xs x) thus ?case by (cases xs) simp_all
-  qed simp
-qed (induct xs rule: induct_list012, simp_all)
-*)
 lemma sorted_tl:
   "sorted xs \<Longrightarrow> sorted (tl xs)"
-by (cases xs) (simp_all add: sorted_Cons)
+by (cases xs) (simp_all)
 
 lemma sorted_append:
   "sorted (xs@ys) = (sorted xs \<and> sorted ys \<and> (\<forall>x \<in> set xs. \<forall>y \<in> set ys. x\<le>y))"
-by (induct xs) (auto simp add:sorted_Cons)
+by (induct xs) (auto)
 
 lemma sorted_nth_mono:
   "sorted xs \<Longrightarrow> i \<le> j \<Longrightarrow> j < length xs \<Longrightarrow> xs!i \<le> xs!j"
-by (induct xs arbitrary: i j) (auto simp:nth_Cons' sorted_Cons)
+by (induct xs arbitrary: i j) (auto simp:nth_Cons')
 
 lemma sorted_rev_nth_mono:
   "sorted (rev xs) \<Longrightarrow> i \<le> j \<Longrightarrow> j < length xs \<Longrightarrow> xs!j \<le> xs!i"
 using sorted_nth_mono[ of "rev xs" "length xs - j - 1" "length xs - i - 1"]
       rev_nth[of "length xs - i - 1" "xs"] rev_nth[of "length xs - j - 1" "xs"]

   moreover
   {
     fix y assume "y \<in> set xs"
     then obtain j where "j < length xs" and "xs ! j = y"
       unfolding in_set_conv_nth by blast
-    with Cons.prems[of 0 "Suc j"]
-    have "x \<le> y"
-      by auto
+    with Cons.prems[of 0 "Suc j"] have "x \<le> y" by auto
   }
   ultimately
-  show ?case
-    unfolding sorted_Cons by auto
+  show ?case by auto
 qed simp
 
 lemma sorted_equals_nth_mono:
   "sorted xs = (\<forall>j < length xs. \<forall>i \<le> j. xs ! i \<le> xs ! j)"
 by (auto intro: sorted_nth_monoI sorted_nth_mono)
 
 lemma sorted_map_remove1:
   "sorted (map f xs) \<Longrightarrow> sorted (map f (remove1 x xs))"
-by (induct xs) (auto simp add: sorted_Cons)
+by (induct xs) (auto)
 
 lemma sorted_remove1: "sorted xs \<Longrightarrow> sorted (remove1 a xs)"
 using sorted_map_remove1 [of "\<lambda>x. x"] by simp
 
 lemma sorted_butlast:

     by (cases xs rule: rev_cases) auto
   with \<open>sorted xs\<close> show ?thesis by (simp add: sorted_append)
 qed
 
 lemma sorted_replicate [simp]: "sorted(replicate n x)"
-by(induction n) (auto simp: sorted_Cons)
+by(induction n) (auto)
 
 lemma sorted_remdups[simp]:
-  "sorted l \<Longrightarrow> sorted (remdups l)"
-by (induct l) (auto simp: sorted_Cons)
+  "sorted xs \<Longrightarrow> sorted (remdups xs)"
+by (induct xs) (auto)
 
 lemma sorted_remdups_adj[simp]:
   "sorted xs \<Longrightarrow> sorted (remdups_adj xs)"
-by (induct xs rule: remdups_adj.induct, simp_all split: if_split_asm add: sorted_Cons)
+by (induct xs rule: remdups_adj.induct, simp_all split: if_split_asm)
 
 lemma sorted_nths: "sorted xs \<Longrightarrow> sorted (nths xs I)"
-by(induction xs arbitrary: I)(auto simp: sorted_Cons nths_Cons)
+by(induction xs arbitrary: I)(auto simp: nths_Cons)
 
 lemma sorted_distinct_set_unique:
 assumes "sorted xs" "distinct xs" "sorted ys" "distinct ys" "set xs = set ys"
 shows "xs = ys"
 proof -
   from assms have 1: "length xs = length ys" by (auto dest!: distinct_card)
   from assms show ?thesis
   proof(induct rule:list_induct2[OF 1])
     case 1 show ?case by simp
   next
-    case 2 thus ?case by (simp add: sorted_Cons)
-       (metis Diff_insert_absorb antisym insertE insert_iff)
+    case 2 thus ?case by simp (metis Diff_insert_absorb antisym insertE insert_iff)
   qed
 qed
 
 lemma map_sorted_distinct_set_unique:
   assumes "inj_on f (set xs \<union> set ys)"

 lemma sorted_takeWhile: "sorted xs \<Longrightarrow> sorted (takeWhile P xs)"
   by (subst takeWhile_eq_take) (auto dest: sorted_take)
 
 lemma sorted_filter:
   "sorted (map f xs) \<Longrightarrow> sorted (map f (filter P xs))"
-  by (induct xs) (simp_all add: sorted_Cons)
+  by (induct xs) simp_all
 
 lemma foldr_max_sorted:
   assumes "sorted (rev xs)"
   shows "foldr max xs y = (if xs = [] then y else max (xs ! 0) y)"
   using assms

   case Nil then show ?case by simp
 next
   case (Cons x xs)
   then have "sorted (map f [y\<leftarrow>xs . f y = (\<lambda>xs. f x) xs])" .
   moreover from Cons have "sorted (map f [y\<leftarrow>xs . f y = (g \<circ> Cons x) xs])" .
-  ultimately show ?case by (simp_all add: sorted_Cons)
+  ultimately show ?case by simp_all
 qed
 
 lemma sorted_same:
   "sorted [x\<leftarrow>xs. x = g xs]"
 using sorted_map_same [of "\<lambda>x. x"] by simp

 
 lemma distinct_sort[simp]: "distinct (sort_key f xs) = distinct xs"
 by (induct xs) (simp_all add: distinct_insort)
 
 lemma sorted_insort_key: "sorted (map f (insort_key f x xs)) = sorted (map f xs)"
-by (induct xs) (auto simp: sorted_Cons set_insort_key)
+by (induct xs) (auto simp: set_insort_key)
 
 lemma sorted_insort: "sorted (insort x xs) = sorted xs"
 using sorted_insort_key [where f="\<lambda>x. x"] by simp
 
 theorem sorted_sort_key [simp]: "sorted (map f (sort_key f xs))"

 
 lemma insort_is_Cons: "\<forall>x\<in>set xs. f a \<le> f x \<Longrightarrow> insort_key f a xs = a # xs"
 by (cases xs) auto
 
 lemma sorted_sort_id: "sorted xs \<Longrightarrow> sort xs = xs"
-by (induct xs) (auto simp add: sorted_Cons insort_is_Cons)
+by (induct xs) (auto simp add: insort_is_Cons)
 
 lemma insort_key_remove1:
   assumes "a \<in> set xs" and "sorted (map f xs)" and "hd (filter (\<lambda>x. f a = f x) xs) = a"
   shows "insort_key f a (remove1 a xs) = xs"
 using assms proof (induct xs)
   case (Cons x xs)
   then show ?case
   proof (cases "x = a")
     case False
     then have "f x \<noteq> f a" using Cons.prems by auto
-    then have "f x < f a" using Cons.prems by (auto simp: sorted_Cons)
-    with \<open>f x \<noteq> f a\<close> show ?thesis using Cons by (auto simp: sorted_Cons insort_is_Cons)
-  qed (auto simp: sorted_Cons insort_is_Cons)
+    then have "f x < f a" using Cons.prems by auto
+    with \<open>f x \<noteq> f a\<close> show ?thesis using Cons by (auto simp: insort_is_Cons)
+  qed (auto simp: insort_is_Cons)
 qed simp
 
 lemma insort_remove1:
   assumes "a \<in> set xs" and "sorted xs"
   shows "insort a (remove1 a xs) = xs"

   "\<not> P x \<Longrightarrow> filter P (insort_key f x xs) = filter P xs"
   by (induct xs) simp_all
 
 lemma filter_insort:
   "sorted (map f xs) \<Longrightarrow> P x \<Longrightarrow> filter P (insort_key f x xs) = insort_key f x (filter P xs)"
-  by (induct xs) (auto simp add: sorted_Cons, subst insort_is_Cons, auto)
+  by (induct xs) (auto, subst insort_is_Cons, auto)
 
 lemma filter_sort:
   "filter P (sort_key f xs) = sort_key f (filter P xs)"
   by (induct xs) (simp_all add: filter_insort_triv filter_insort)
 

   by (rule sorted_sort_id) simp
 
 lemma sorted_upto[simp]: "sorted[i..j]"
 apply(induct i j rule:upto.induct)
 apply(subst upto.simps)
-apply(simp add:sorted_Cons)
+apply(simp)
 done
 
 lemma sorted_find_Min:
   "sorted xs \<Longrightarrow> \<exists>x \<in> set xs. P x \<Longrightarrow> List.find P xs = Some (Min {x\<in>set xs. P x})"
 proof (induct xs)
   case Nil then show ?case by simp
 next
   case (Cons x xs) show ?case proof (cases "P x")
     case True
-    with Cons show ?thesis by (auto simp: sorted_Cons intro: Min_eqI [symmetric])
+    with Cons show ?thesis by (auto intro: Min_eqI [symmetric])
   next
     case False then have "{y. (y = x \<or> y \<in> set xs) \<and> P y} = {y \<in> set xs. P y}"
       by auto
-    with Cons False show ?thesis by (simp_all add: sorted_Cons)
+    with Cons False show ?thesis by (simp_all)
   qed
 qed
 
 lemma sorted_enumerate [simp]: "sorted (map fst (enumerate n xs))"
 by (simp add: enumerate_eq_zip)

 by unfold_locales(auto simp add: lexordp_conv_lexordp_eq lexordp_eq_refl lexordp_eq_antisym intro: lexordp_eq_trans del: disjCI intro: lexordp_eq_linear)
 
 end
 
 lemma sorted_insort_is_snoc: "sorted xs \<Longrightarrow> \<forall>x \<in> set xs. a \<ge> x \<Longrightarrow> insort a xs = xs @ [a]"
- by (induct xs) (auto dest!: insort_is_Cons simp: sorted_Cons)
+ by (induct xs) (auto dest!: insort_is_Cons)
 
 
 subsubsection \<open>Lexicographic combination of measure functions\<close>
 
 text \<open>These are useful for termination proofs\<close>

       by (metis Cons Cons_eq_filter_iff in_set_conv_decomp set_sort)
     next
       fix y assume "y \<in> set xs \<and> P y"
       hence "y \<in> set (filter P xs)" by auto
       thus "x \<le> y"
-        by (metis Cons eq_iff filter_sort set_ConsD set_sort sorted_Cons sorted_sort)
+        by (metis Cons eq_iff filter_sort set_ConsD set_sort sorted.simps(2) sorted_sort)
   qed
   thus ?thesis using Cons by (simp add: Bleast_def)
 qed
 
 declare Bleast_def[symmetric, code_unfold]