# HG changeset patch
# User wenzelm
# Date 1633199506 -7200
# Node ID 2cf4d6cf4c0d356d2bd38484bbec24e5ed1b29f9
# Parent  584c4db57f68061bbff96e8f7c772a2341317010
trim whitespace;

diff -r 584c4db57f68 -r 2cf4d6cf4c0d src/HOL/List.thy
--- a/src/HOL/List.thy	Sat Oct 02 20:28:30 2021 +0200
+++ b/src/HOL/List.thy	Sat Oct 02 20:31:46 2021 +0200
@@ -371,7 +371,7 @@
 begin
 
 abbreviation sorted :: "'a list \<Rightarrow> bool" where
-  "sorted \<equiv> sorted_wrt (\<le>)" 
+  "sorted \<equiv> sorted_wrt (\<le>)"
 
 lemma sorted_simps: "sorted [] = True" "sorted (x # ys) = ((\<forall>y \<in> set ys. x\<le>y) \<and> sorted ys)"
   by auto
@@ -1499,7 +1499,7 @@
   | len (Const(\<^const_name>\<open>rev\<close>,_) $ xs) acc = len xs acc
   | len (Const(\<^const_name>\<open>map\<close>,_) $ _ $ xs) acc = len xs acc
   | len (Const(\<^const_name>\<open>concat\<close>,T) $ (Const(\<^const_name>\<open>rev\<close>,_) $ xss)) acc
-    = len (Const(\<^const_name>\<open>concat\<close>,T) $ xss) acc 
+    = len (Const(\<^const_name>\<open>concat\<close>,T) $ xss) acc
   | len t (ts,n) = (t::ts,n);
 
 val ss = simpset_of \<^context>;
@@ -3128,7 +3128,7 @@
   assumes "set xs \<subseteq> S"
   shows "Finite_Set.fold f y (set xs) = fold f (remdups xs) y"
   by (rule sym, use assms in \<open>induct xs arbitrary: y\<close>)
-     (simp_all add: insert_absorb fold_fun_left_comm) 
+     (simp_all add: insert_absorb fold_fun_left_comm)
 
 lemma (in comp_fun_idem_on) fold_set_fold:
   assumes "set xs \<subseteq> S"
@@ -3510,7 +3510,7 @@
 
 lemma successively_append_iff:
   "successively P (xs @ ys) \<longleftrightarrow>
-     successively P xs \<and> successively P ys \<and> 
+     successively P xs \<and> successively P ys \<and>
      (xs = [] \<or> ys = [] \<or> P (last xs) (hd ys))"
 by (induction xs) (auto simp: successively_Cons)
 
@@ -4141,7 +4141,7 @@
       by (metis (full_types) dropWhile_eq_self_iff last_snoc remdups_adj_append_dropWhile)
     thus ?thesis by (simp add: xs)
   qed
-  thus ?thesis using assms 
+  thus ?thesis using assms
     by (cases "xs = []"; cases "ys = []") auto
 qed
 
@@ -4425,7 +4425,7 @@
   by (auto dest: length_filter_less simp add: removeAll_filter_not_eq)
 
 lemma distinct_concat_iff: "distinct (concat xs) \<longleftrightarrow>
-  distinct (removeAll [] xs) \<and> 
+  distinct (removeAll [] xs) \<and>
   (\<forall>ys. ys \<in> set xs \<longrightarrow> distinct ys) \<and>
   (\<forall>ys zs. ys \<in> set xs \<and> zs \<in> set xs \<and> ys \<noteq> zs \<longrightarrow> set ys \<inter> set zs = {})"
 apply (induct xs)
@@ -4993,7 +4993,7 @@
 lemma splice_replicate[simp]: "splice (replicate m x) (replicate n x) = replicate (m+n) x"
 proof (induction "replicate m x" "replicate n x" arbitrary: m n rule: splice.induct)
   case (2 x xs)
-  then show ?case 
+  then show ?case
     by (auto simp add: Cons_replicate_eq dest: gr0_implies_Suc)
 qed auto
 
@@ -5360,7 +5360,7 @@
 lemma infinite_UNIV_listI: "\<not> finite(UNIV::'a list set)"
   by (metis UNIV_I finite_maxlen length_replicate less_irrefl)
 
-lemma same_length_different: 
+lemma same_length_different:
   assumes "xs \<noteq> ys" and "length xs = length ys"
   shows "\<exists>pre x xs' y ys'. x\<noteq>y \<and> xs = pre @ [x] @ xs' \<and> ys = pre @ [y] @ ys'"
   using assms
@@ -5462,7 +5462,7 @@
 proof
   assume ?L
   thus ?R
-    by (simp add: sorted_wrt_iff_nth_less) 
+    by (simp add: sorted_wrt_iff_nth_less)
 next
   assume ?R
   have "i < j \<Longrightarrow> j < length xs \<Longrightarrow> P (xs ! i) (xs ! j)" for i j
@@ -5545,7 +5545,7 @@
   "sorted xs \<Longrightarrow> i \<le> j \<Longrightarrow> j < length xs \<Longrightarrow> xs!i \<le> xs!j"
   by (auto simp: sorted_iff_nth_mono)
 
-lemma sorted_iff_nth_Suc: 
+lemma sorted_iff_nth_Suc:
   "sorted xs \<longleftrightarrow> (\<forall>i.  Suc i < length xs \<longrightarrow> xs!i \<le> xs!(Suc i))"
   by(simp add: sorted_wrt_iff_nth_Suc_transp)
 
@@ -5573,13 +5573,13 @@
   thus ?L by (simp add: sorted_iff_nth_mono)
 qed
 
-lemma sorted_rev_iff_nth_Suc: 
+lemma sorted_rev_iff_nth_Suc:
   "sorted (rev xs) \<longleftrightarrow> (\<forall>i.  Suc i < length xs \<longrightarrow> xs!(Suc i) \<le> xs!i)"
 proof-
   interpret dual: linorder "(\<lambda>x y. y \<le> x)" "(\<lambda>x y. y < x)"
     using dual_linorder .
   show ?thesis
-    using dual_linorder dual.sorted_iff_nth_Suc dual.sorted_iff_nth_mono 
+    using dual_linorder dual.sorted_iff_nth_Suc dual.sorted_iff_nth_mono
     unfolding sorted_rev_iff_nth_mono by simp
 qed
 
@@ -6244,7 +6244,7 @@
   proof (cases ys)
     case Nil
     then show ?thesis
-      using Cons.prems by auto 
+      using Cons.prems by auto
   next
     case (Cons y ys')
     then have "xs = ys'"
@@ -6255,13 +6255,13 @@
       using local.Cons by blast
   qed
 qed auto
-	
+
 lemma (in linorder) strict_sorted_equal_Uniq: "\<exists>\<^sub>\<le>\<^sub>1xs. sorted_wrt (<) xs \<and> set xs = A"
   by (simp add: Uniq_def strict_sorted_equal)
 
 lemma sorted_key_list_of_set_inject:
   assumes "A \<subseteq> S" "B \<subseteq> S"
-  assumes "sorted_key_list_of_set f A = sorted_key_list_of_set f B" "finite A" "finite B" 
+  assumes "sorted_key_list_of_set f A = sorted_key_list_of_set f B" "finite A" "finite B"
   shows "A = B"
   using assms set_sorted_key_list_of_set by metis
 
@@ -6326,7 +6326,7 @@
   "sorted_list_of_set {m..<n} = [m..<n]"
 by (rule sorted_distinct_set_unique) simp_all
 
-lemma sorted_list_of_set_lessThan_Suc [simp]: 
+lemma sorted_list_of_set_lessThan_Suc [simp]:
   "sorted_list_of_set {..<Suc k} = sorted_list_of_set {..<k} @ [k]"
   using le0 lessThan_atLeast0 sorted_list_of_set_range upt_Suc_append by presburger
 
@@ -6341,7 +6341,7 @@
   by (auto simp: less_le simp flip: sorted_list_of_set.sorted_key_list_of_set_unique intro: Min_in)
 
 lemma sorted_list_of_set_greaterThanLessThan:
-  assumes "Suc i < j" 
+  assumes "Suc i < j"
     shows "sorted_list_of_set {i<..<j} = Suc i # sorted_list_of_set {Suc i<..<j}"
 proof -
   have "{i<..<j} = insert (Suc i) {Suc i<..<j}"
@@ -6351,16 +6351,16 @@
 qed
 
 lemma sorted_list_of_set_greaterThanAtMost:
-  assumes "Suc i \<le> j" 
+  assumes "Suc i \<le> j"
     shows "sorted_list_of_set {i<..j} = Suc i # sorted_list_of_set {Suc i<..j}"
   using sorted_list_of_set_greaterThanLessThan [of i "Suc j"]
   by (metis assms greaterThanAtMost_def greaterThanLessThan_eq le_imp_less_Suc lessThan_Suc_atMost)
 
-lemma nth_sorted_list_of_set_greaterThanLessThan: 
+lemma nth_sorted_list_of_set_greaterThanLessThan:
   "n < j - Suc i \<Longrightarrow> sorted_list_of_set {i<..<j} ! n = Suc (i+n)"
   by (induction n arbitrary: i) (auto simp: sorted_list_of_set_greaterThanLessThan)
 
-lemma nth_sorted_list_of_set_greaterThanAtMost: 
+lemma nth_sorted_list_of_set_greaterThanAtMost:
   "n < j - i \<Longrightarrow> sorted_list_of_set {i<..j} ! n = Suc (i+n)"
   using nth_sorted_list_of_set_greaterThanLessThan [of n "Suc j" i]
   by (simp add: greaterThanAtMost_def greaterThanLessThan_eq lessThan_Suc_atMost)
@@ -6515,7 +6515,7 @@
   "(xs, ys) \<in> lexn r n \<Longrightarrow> length xs = n \<and> length ys = n"
   by (induct n arbitrary: xs ys) auto
 
-lemma wf_lex [intro!]: 
+lemma wf_lex [intro!]:
   assumes "wf r" shows "wf (lex r)"
   unfolding lex_def
 proof (rule wf_UN)
@@ -6631,7 +6631,7 @@
     if "xs \<noteq> ys" and len: "length xs = length ys" for xs ys
   proof -
     obtain pre x xs' y ys' where "x\<noteq>y" and xs: "xs = pre @ [x] @ xs'" and ys: "ys = pre @ [y] @ys'"
-      by (meson len \<open>xs \<noteq> ys\<close> same_length_different) 
+      by (meson len \<open>xs \<noteq> ys\<close> same_length_different)
     then consider "(x,y) \<in> r" | "(y,x) \<in> r"
       by (meson UNIV_I assms total_on_def)
     then show ?thesis
@@ -6662,14 +6662,14 @@
     by (simp add: lex_conv) (blast intro: Cons_eq_appendI)
 qed
 
-lemma Nil_lenlex_iff1 [simp]: "([], ns) \<in> lenlex r \<longleftrightarrow> ns \<noteq> []" 
+lemma Nil_lenlex_iff1 [simp]: "([], ns) \<in> lenlex r \<longleftrightarrow> ns \<noteq> []"
   and Nil_lenlex_iff2 [simp]: "(ns,[]) \<notin> lenlex r"
   by (auto simp: lenlex_def)
 
-lemma Cons_lenlex_iff: 
-  "((m # ms, n # ns) \<in> lenlex r) \<longleftrightarrow> 
-    length ms < length ns 
-  \<or> length ms = length ns \<and> (m,n) \<in> r 
+lemma Cons_lenlex_iff:
+  "((m # ms, n # ns) \<in> lenlex r) \<longleftrightarrow>
+    length ms < length ns
+  \<or> length ms = length ns \<and> (m,n) \<in> r
   \<or> (m = n \<and> (ms,ns) \<in> lenlex r)"
   by (auto simp: lenlex_def)
 
@@ -6797,19 +6797,19 @@
 proof-
   from leD[OF assms(2)] assms(1)[unfolded lexord_take_index_conv[of u w r] min_absorb2[OF assms(2)]]
   obtain i where "take i u = take i w" and "(u!i,w!i) \<in> r" and "i < length w"
-    by blast   
+    by blast
   hence "((u@v)!i, (w@z)!i) \<in> r"
     unfolding nth_append using less_le_trans[OF \<open>i < length w\<close> assms(2)] \<open>(u!i,w!i) \<in> r\<close>
     by presburger
   moreover have "i < min (length (u@v)) (length (w@z))"
     using assms(2) \<open>i < length w\<close> by simp
   moreover have "take i (u@v) = take i (w@z)"
-    using assms(2) \<open>i < length w\<close> \<open>take i u = take i w\<close> by simp 
+    using assms(2) \<open>i < length w\<close> \<open>take i u = take i w\<close> by simp
   ultimately show ?thesis
     using lexord_take_index_conv by blast
 qed
 
-lemma lexord_sufE: 
+lemma lexord_sufE:
   assumes "(xs@zs,ys@qs) \<in> lexord r" "xs \<noteq> ys" "length xs = length ys" "length zs = length qs"
   shows "(xs,ys) \<in> lexord r"
 proof-
@@ -6893,7 +6893,7 @@
 qed
 
 corollary lexord_linear: "(\<forall>a b. (a,b) \<in> r \<or> a = b \<or> (b,a) \<in> r) \<Longrightarrow> (x,y) \<in> lexord r \<or> x = y \<or> (y,x) \<in> lexord r"
-  using total_lexord by (metis UNIV_I total_on_def) 
+  using total_lexord by (metis UNIV_I total_on_def)
 
 lemma lexord_irrefl:
   "irrefl R \<Longrightarrow> irrefl (lexord R)"
@@ -6902,7 +6902,7 @@
 lemma lexord_asym:
   assumes "asym R"
   shows "asym (lexord R)"
-proof 
+proof
   fix xs ys
   assume "(xs, ys) \<in> lexord R"
   then show "(ys, xs) \<notin> lexord R"
@@ -6932,12 +6932,12 @@
   by (simp add: lenlex_def asym_inv_image asym_less_than asym_lex asym_lex_prod)
 
 lemma lenlex_append1:
-  assumes len: "(us,xs) \<in> lenlex R" and eq: "length vs = length ys" 
+  assumes len: "(us,xs) \<in> lenlex R" and eq: "length vs = length ys"
   shows "(us @ vs, xs @ ys) \<in> lenlex R"
   using len
 proof (induction us)
   case Nil
-  then show ?case 
+  then show ?case
     by (simp add: lenlex_def eq)
 next
   case (Cons u us)
@@ -6950,7 +6950,7 @@
   shows "(us @ xs, us @ ys) \<in> lenlex R \<longleftrightarrow> (xs, ys) \<in> lenlex R"
 proof (induction us)
   case Nil
-  then show ?case 
+  then show ?case
     by (simp add: lenlex_def)
 next
   case (Cons u us)