tuned whitespace;

--- a/src/HOL/List.thy	Sun Jan 29 11:59:48 2017 +0100
+++ b/src/HOL/List.thy	Sun Jan 29 13:28:45 2017 +0100
@@ -871,7 +871,7 @@
   case (Cons x xs ys zs ws) then show ?case by ((cases ys, simp_all), (cases zs,simp_all)) (cases ws, simp_all)
 qed
 
-lemma list_induct2': 
+lemma list_induct2':
   "\<lbrakk> P [] [];
   \<And>x xs. P (x#xs) [];
   \<And>y ys. P [] (y#ys);
@@ -1045,19 +1045,19 @@
           (case xs of Const (@{const_name Nil}, _) => cons | _ => last xs)
       | last (Const(@{const_name append},_) $ _ $ ys) = last ys
       | last t = t;
-    
+
     fun list1 (Const(@{const_name Cons},_) $ _ $ Const(@{const_name Nil},_)) = true
       | list1 _ = false;
-    
+
     fun butlast ((cons as Const(@{const_name Cons},_) $ x) $ xs) =
           (case xs of Const (@{const_name Nil}, _) => xs | _ => cons $ butlast xs)
       | butlast ((app as Const (@{const_name append}, _) $ xs) $ ys) = app $ butlast ys
       | butlast xs = Const(@{const_name Nil}, fastype_of xs);
-    
+
     val rearr_ss =
       simpset_of (put_simpset HOL_basic_ss @{context}
         addsimps [@{thm append_assoc}, @{thm append_Nil}, @{thm append_Cons}]);
-    
+
     fun list_eq ctxt (F as (eq as Const(_,eqT)) $ lhs $ rhs) =
       let
         val lastl = last lhs and lastr = last rhs;
@@ -1148,7 +1148,7 @@
   with Cons have "length zs = length ys" by blast
   with xs show ?case by simp
 qed
-  
+
 lemma map_inj_on:
  "[| map f xs = map f ys; inj_on f (set xs Un set ys) |]
   ==> xs = ys"
@@ -1287,7 +1287,7 @@
 lemma set_subset_Cons: "set xs \<subseteq> set (x # xs)"
 by auto
 
-lemma set_ConsD: "y \<in> set (x # xs) \<Longrightarrow> y=x \<or> y \<in> set xs" 
+lemma set_ConsD: "y \<in> set (x # xs) \<Longrightarrow> y=x \<or> y \<in> set xs"
 by auto
 
 lemma set_empty [iff]: "(set xs = {}) = (xs = [])"
@@ -1458,7 +1458,7 @@
 lemma filter_False [simp]: "\<forall>x \<in> set xs. \<not> P x ==> filter P xs = []"
 by (induct xs) auto
 
-lemma filter_empty_conv: "(filter P xs = []) = (\<forall>x\<in>set xs. \<not> P x)" 
+lemma filter_empty_conv: "(filter P xs = []) = (\<forall>x\<in>set xs. \<not> P x)"
 by (induct xs) simp_all
 
 lemma filter_id_conv: "(filter P xs = xs) = (\<forall>x\<in>set xs. P x)"
@@ -1582,7 +1582,7 @@
 
 primrec partition :: "('a \<Rightarrow> bool) \<Rightarrow>'a list \<Rightarrow> 'a list \<times> 'a list" where
 "partition P [] = ([], [])" |
-"partition P (x # xs) = 
+"partition P (x # xs) =
   (let (yes, no) = partition P xs
    in if P x then (x # yes, no) else (yes, x # no))"
 
@@ -1607,7 +1607,7 @@
 proof -
   from assms have "yes = fst (partition P xs)" and "no = snd (partition P xs)"
     by simp_all
-  then show ?thesis by (auto simp add: partition_filter1 partition_filter2) 
+  then show ?thesis by (auto simp add: partition_filter1 partition_filter2)
 qed
 
 lemma partition_filter_conv[simp]:
@@ -1832,7 +1832,7 @@
 by (induct xs arbitrary: i)(auto split:nat.split)
 
 lemma list_update_append:
-  "(xs @ ys) [n:= x] = 
+  "(xs @ ys) [n:= x] =
   (if n < length xs then xs[n:= x] @ ys else xs @ (ys [n-length xs:= x]))"
 by (induct xs arbitrary: n) (auto split:nat.splits)
 
@@ -2169,7 +2169,7 @@
 done
 
 lemma take_add:  "take (i+j) xs = take i xs @ take j (drop i xs)"
-apply (induct xs arbitrary: i, auto) 
+apply (induct xs arbitrary: i, auto)
  apply (case_tac i, simp_all)
 done
 
@@ -2192,7 +2192,7 @@
 done
 
 lemma id_take_nth_drop:
-  "i < length xs \<Longrightarrow> xs = take i xs @ xs!i # drop (Suc i) xs" 
+  "i < length xs \<Longrightarrow> xs = take i xs @ xs!i # drop (Suc i) xs"
 proof -
   assume si: "i < length xs"
   hence "xs = take (Suc i) xs @ drop (Suc i) xs" by auto
@@ -2201,7 +2201,7 @@
     apply (rule_tac take_Suc_conv_app_nth) by arith
   ultimately show ?thesis by auto
 qed
-  
+
 lemma take_update_cancel[simp]: "n \<le> m \<Longrightarrow> take n (xs[m := y]) = take n xs"
 by(simp add: list_eq_iff_nth_eq)
 
@@ -2397,12 +2397,12 @@
 done
 
 lemma takeWhile_cong [fundef_cong]:
-  "[| l = k; !!x. x : set l ==> P x = Q x |] 
+  "[| l = k; !!x. x : set l ==> P x = Q x |]
   ==> takeWhile P l = takeWhile Q k"
 by (induct k arbitrary: l) (simp_all)
 
 lemma dropWhile_cong [fundef_cong]:
-  "[| l = k; !!x. x : set l ==> P x = Q x |] 
+  "[| l = k; !!x. x : set l ==> P x = Q x |]
   ==> dropWhile P l = dropWhile Q k"
 by (induct k arbitrary: l, simp_all)
 
@@ -2593,7 +2593,7 @@
 
 subsubsection \<open>@{const list_all2}\<close>
 
-lemma list_all2_lengthD [intro?]: 
+lemma list_all2_lengthD [intro?]:
   "list_all2 P xs ys ==> length xs = length ys"
 by (simp add: list_all2_iff)
 
@@ -2701,11 +2701,11 @@
   "\<lbrakk>list_all2 P xs ys; p < size ys\<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
 by (frule list_all2_lengthD) (auto intro: list_all2_nthD)
 
-lemma list_all2_map1: 
+lemma list_all2_map1:
   "list_all2 P (map f as) bs = list_all2 (\<lambda>x y. P (f x) y) as bs"
 by (simp add: list_all2_conv_all_nth)
 
-lemma list_all2_map2: 
+lemma list_all2_map2:
   "list_all2 P as (map f bs) = list_all2 (\<lambda>x y. P x (f y)) as bs"
 by (auto simp add: list_all2_conv_all_nth)
 
@@ -2789,7 +2789,7 @@
     by (auto simp add: nth_append not_less le_mod_geq le_div_geq)
 qed
 
-lemma in_set_product_lists_length: 
+lemma in_set_product_lists_length:
   "xs \<in> set (product_lists xss) \<Longrightarrow> length xs = length xss"
 by (induct xss arbitrary: xs) auto
 
@@ -2809,7 +2809,7 @@
 
 lemma fold_simps [code]: \<comment> \<open>eta-expanded variant for generated code -- enables tail-recursion optimisation in Scala\<close>
   "fold f [] s = s"
-  "fold f (x # xs) s = fold f xs (f x s)" 
+  "fold f (x # xs) s = fold f xs (f x s)"
 by simp_all
 
 lemma fold_remove1_split:
@@ -2838,7 +2838,7 @@
   then show ?thesis by (simp add: fun_eq_iff)
 qed
 
-lemma fold_invariant: 
+lemma fold_invariant:
   "\<lbrakk> \<And>x. x \<in> set xs \<Longrightarrow> Q x;  P s;  \<And>x s. Q x \<Longrightarrow> P s \<Longrightarrow> P (f x s) \<rbrakk>
   \<Longrightarrow> P (fold f xs s)"
 by (induct xs arbitrary: s) simp_all
@@ -2992,7 +2992,7 @@
 lemma foldr_filter:
   "foldr f (filter P xs) = foldr (\<lambda>x. if P x then f x else id) xs"
 by (simp add: foldr_conv_fold rev_filter fold_filter)
-  
+
 lemma foldl_map [code_unfold]:
   "foldl g a (map f xs) = foldl (\<lambda>a x. g a (f x)) a xs"
 by (simp add: foldl_conv_fold fold_map comp_def)
@@ -3084,7 +3084,7 @@
 lemma map_decr_upt: "map (\<lambda>n. n - Suc 0) [Suc m..<Suc n] = [m..<n]"
 by (induct n) simp_all
 
- 
+
 lemma nth_take_lemma:
   "k <= length xs ==> k <= length ys ==>
      (!!i. i < k --> xs!i = ys!i) ==> take k xs = take k ys"
@@ -3109,9 +3109,9 @@
 by (rule nth_equalityI, auto)
 
 lemma list_all2_antisym:
-  "\<lbrakk> (\<And>x y. \<lbrakk>P x y; Q y x\<rbrakk> \<Longrightarrow> x = y); list_all2 P xs ys; list_all2 Q ys xs \<rbrakk> 
+  "\<lbrakk> (\<And>x y. \<lbrakk>P x y; Q y x\<rbrakk> \<Longrightarrow> x = y); list_all2 P xs ys; list_all2 Q ys xs \<rbrakk>
   \<Longrightarrow> xs = ys"
-apply (simp add: list_all2_conv_all_nth) 
+apply (simp add: list_all2_conv_all_nth)
 apply (rule nth_equalityI, blast, simp)
 done
 
@@ -3326,7 +3326,7 @@
   "\<lbrakk> distinct xs; i < length xs; j < length xs \<rbrakk> \<Longrightarrow> (xs!i = xs!j) = (i = j)"
 by(auto simp: distinct_conv_nth)
 
-lemma distinct_Ex1: 
+lemma distinct_Ex1:
   "distinct xs \<Longrightarrow> x \<in> set xs \<Longrightarrow> (\<exists>!i. i < length xs \<and> xs ! i = x)"
   by (auto simp: in_set_conv_nth nth_eq_iff_index_eq)
 
@@ -3334,7 +3334,7 @@
 by (rule inj_onI) (simp add: nth_eq_iff_index_eq)
 
 lemma bij_betw_nth:
-  assumes "distinct xs" "A = {..<length xs}" "B = set xs" 
+  assumes "distinct xs" "A = {..<length xs}" "B = set xs"
   shows   "bij_betw (op ! xs) A B"
   using assms unfolding bij_betw_def
   by (auto intro!: inj_on_nth simp: set_conv_nth)
@@ -3422,7 +3422,7 @@
   proof (cases "product_lists xss")
     case Nil then show ?thesis by (induct xs) simp_all
   next
-    case (Cons ps pss) with * show ?thesis 
+    case (Cons ps pss) with * show ?thesis
       by (auto intro!: inj_onI distinct_concat simp add: distinct_map)
   qed
 qed simp
@@ -3664,7 +3664,7 @@
   (case remdups_adj xs of [] \<Rightarrow> [x] | y # xs \<Rightarrow> if x = y then y # xs else x # y # xs)"
 by (induct xs arbitrary: x) (auto split: list.splits)
 
-lemma remdups_adj_append_two: 
+lemma remdups_adj_append_two:
   "remdups_adj (xs @ [x,y]) = remdups_adj (xs @ [x]) @ (if x = y then [] else [y])"
 by (induct xs rule: remdups_adj.induct, simp_all)
 
@@ -3696,7 +3696,7 @@
 lemma remdups_adj_distinct: "distinct xs \<Longrightarrow> remdups_adj xs = xs"
 by (induct xs rule: remdups_adj.induct, simp_all)
 
-lemma remdups_adj_append: 
+lemma remdups_adj_append:
   "remdups_adj (xs\<^sub>1 @ x # xs\<^sub>2) = remdups_adj (xs\<^sub>1 @ [x]) @ tl (remdups_adj (x # xs\<^sub>2))"
 by (induct xs\<^sub>1 rule: remdups_adj.induct, simp_all)
 
@@ -3782,7 +3782,7 @@
 qed
 
 lemma find_cong[fundef_cong]:
-  assumes "xs = ys" and "\<And>x. x \<in> set ys \<Longrightarrow> P x = Q x" 
+  assumes "xs = ys" and "\<And>x. x \<in> set ys \<Longrightarrow> P x = Q x"
   shows "List.find P xs = List.find Q ys"
 proof (cases "List.find P xs")
   case None thus ?thesis by (metis find_None_iff assms)
@@ -3824,12 +3824,12 @@
 
 lemma extract_SomeE:
  "List.extract P xs = Some (ys, y, zs) \<Longrightarrow>
-  xs = ys @ y # zs \<and> P y \<and> \<not> (\<exists> y \<in> set ys. P y)" 
+  xs = ys @ y # zs \<and> P y \<and> \<not> (\<exists> y \<in> set ys. P y)"
 by(auto simp: extract_def dropWhile_eq_Cons_conv split: list.splits)
 
 lemma extract_Some_iff:
   "List.extract P xs = Some (ys, y, zs) \<longleftrightarrow>
-   xs = ys @ y # zs \<and> P y \<and> \<not> (\<exists> y \<in> set ys. P y)" 
+   xs = ys @ y # zs \<and> P y \<and> \<not> (\<exists> y \<in> set ys. P y)"
 by(auto simp: extract_def dropWhile_eq_Cons_conv dest: set_takeWhileD split: list.splits)
 
 lemma extract_Nil_code[code]: "List.extract P [] = None"
@@ -4183,7 +4183,7 @@
 lemma map_snd_enumerate [simp]:
   "map snd (enumerate n xs) = xs"
   by (simp add: enumerate_eq_zip)
-  
+
 lemma in_set_enumerate_eq:
   "p \<in> set (enumerate n xs) \<longleftrightarrow> n \<le> fst p \<and> fst p < length xs + n \<and> nth xs (fst p - n) = snd p"
 proof -
@@ -4227,7 +4227,7 @@
 lemma enumerate_map_upt:
   "enumerate n (map f [n..<m]) = map (\<lambda>k. (k, f k)) [n..<m]"
   by (cases "n \<le> m") (simp_all add: zip_map2 zip_same_conv_map enumerate_eq_zip)
-  
+
 
 subsubsection \<open>@{const rotate1} and @{const rotate}\<close>
 
@@ -4408,18 +4408,15 @@
 
 subsubsection \<open>@{const sublists} and @{const List.n_lists}\<close>
 
-lemma length_sublists:
-  "length (sublists xs) = 2 ^ length xs"
+lemma length_sublists: "length (sublists xs) = 2 ^ length xs"
   by (induct xs) (simp_all add: Let_def)
 
-lemma sublists_powset:
-  "set ` set (sublists xs) = Pow (set xs)"
+lemma sublists_powset: "set ` set (sublists xs) = Pow (set xs)"
 proof -
   have aux: "\<And>x A. set ` Cons x ` A = insert x ` set ` A"
     by (auto simp add: image_def)
   have "set (map set (sublists xs)) = Pow (set xs)"
-    by (induct xs)
-      (simp_all add: aux Let_def Pow_insert Un_commute comp_def del: map_map)
+    by (induct xs) (simp_all add: aux Let_def Pow_insert Un_commute comp_def del: map_map)
   then show ?thesis by simp
 qed
 
@@ -4427,10 +4424,11 @@
   assumes "distinct xs"
   shows "distinct (map set (sublists xs))"
 proof (rule card_distinct)
-  have "finite (set xs)" by rule
-  then have "card (Pow (set xs)) = 2 ^ card (set xs)" by (rule card_Pow)
-  with assms distinct_card [of xs]
-    have "card (Pow (set xs)) = 2 ^ length xs" by simp
+  have "finite (set xs)" ..
+  then have "card (Pow (set xs)) = 2 ^ card (set xs)"
+    by (rule card_Pow)
+  with assms distinct_card [of xs] have "card (Pow (set xs)) = 2 ^ length xs"
+    by simp
   then show "card (set (map set (sublists xs))) = length (map set (sublists xs))"
     by (simp add: sublists_powset length_sublists)
 qed
@@ -4457,17 +4455,16 @@
 qed
 
 lemma sublists_refl: "xs \<in> set (sublists xs)"
-by (induct xs) (simp_all add: Let_def)
+  by (induct xs) (simp_all add: Let_def)
 
 lemma subset_sublists: "X \<subseteq> set xs \<Longrightarrow> X \<in> set ` set (sublists xs)"
-unfolding sublists_powset by simp
-
-lemma Cons_in_sublistsD:
-  "y # ys \<in> set (sublists xs) \<Longrightarrow> ys \<in> set (sublists xs)"
-by (induct xs) (auto simp: Let_def)
+  unfolding sublists_powset by simp
+
+lemma Cons_in_sublistsD: "y # ys \<in> set (sublists xs) \<Longrightarrow> ys \<in> set (sublists xs)"
+  by (induct xs) (auto simp: Let_def)
 
 lemma sublists_distinctD: "\<lbrakk> ys \<in> set (sublists xs); distinct xs \<rbrakk> \<Longrightarrow> distinct ys"
-proof(induct xs arbitrary: ys)
+proof (induct xs arbitrary: ys)
   case (Cons x xs ys)
   then show ?case
     by (auto simp: Let_def) (metis Pow_iff contra_subsetD image_eqI sublists_powset)
@@ -4828,7 +4825,7 @@
   from \<open>xs \<noteq> []\<close> obtain ys y where "xs = ys @ [y]" by (cases xs rule: rev_cases) auto
   with \<open>sorted xs\<close> show ?thesis by (simp add: sorted_append)
 qed
-  
+
 lemma insort_not_Nil [simp]:
   "insort_key f a xs \<noteq> []"
   by (induct xs) simp_all
@@ -5269,7 +5266,7 @@
   by (auto simp: sorted_list_of_set.remove)
 
 lemma sorted_list_of_set [simp]:
-  "finite A \<Longrightarrow> set (sorted_list_of_set A) = A \<and> sorted (sorted_list_of_set A) 
+  "finite A \<Longrightarrow> set (sorted_list_of_set A) = A \<and> sorted (sorted_list_of_set A)
     \<and> distinct (sorted_list_of_set A)"
   by (induct A rule: finite_induct) (simp_all add: set_insort sorted_insort distinct_insort)
 
@@ -5419,9 +5416,9 @@
 
 subsubsection \<open>Length Lexicographic Ordering\<close>
 
-text\<open>These orderings preserve well-foundedness: shorter lists 
+text\<open>These orderings preserve well-foundedness: shorter lists
   precede longer lists. These ordering are not used in dictionaries.\<close>
-        
+
 primrec \<comment> \<open>The lexicographic ordering for lists of the specified length\<close>
   lexn :: "('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> ('a list \<times> 'a list) set" where
 "lexn r 0 = {}" |
@@ -5569,14 +5566,14 @@
 
 text \<open>Classical lexicographic ordering on lists, ie. "a" < "ab" < "b".
     This ordering does \emph{not} preserve well-foundedness.
-     Author: N. Voelker, March 2005.\<close> 
+     Author: N. Voelker, March 2005.\<close>
 
 definition lexord :: "('a \<times> 'a) set \<Rightarrow> ('a list \<times> 'a list) set" where
 "lexord r = {(x,y). \<exists> a v. y = x @ a # v \<or>
             (\<exists> u a b v w. (a,b) \<in> r \<and> x = u @ (a # v) \<and> y = u @ (b # w))}"
 
 lemma lexord_Nil_left[simp]:  "([],y) \<in> lexord r = (\<exists> a x. y = a # x)"
-by (unfold lexord_def, induct_tac y, auto) 
+by (unfold lexord_def, induct_tac y, auto)
 
 lemma lexord_Nil_right[simp]: "(x,[]) \<notin> lexord r"
 by (unfold lexord_def, induct_tac x, auto)
@@ -5592,7 +5589,7 @@
 lemmas lexord_simps = lexord_Nil_left lexord_Nil_right lexord_cons_cons
 
 lemma lexord_append_rightI: "\<exists> b z. y = b # z \<Longrightarrow> (x, x @ y) \<in> lexord r"
-by (induct_tac x, auto)  
+by (induct_tac x, auto)
 
 lemma lexord_append_left_rightI:
      "(a,b) \<in> r \<Longrightarrow> (u @ a # x, u @ b # y) \<in> lexord r"
@@ -5605,36 +5602,36 @@
      "\<lbrakk> (x @ u, x @ v) \<in> lexord r; (! a. (a,a) \<notin> r) \<rbrakk> \<Longrightarrow> (u,v) \<in> lexord r"
 by (erule rev_mp, induct_tac x, auto)
 
-lemma lexord_take_index_conv: 
-   "((x,y) : lexord r) = 
-    ((length x < length y \<and> take (length x) y = x) \<or> 
+lemma lexord_take_index_conv:
+   "((x,y) : lexord r) =
+    ((length x < length y \<and> take (length x) y = x) \<or>
      (\<exists>i. i < min(length x)(length y) & take i x = take i y & (x!i,y!i) \<in> r))"
-  apply (unfold lexord_def Let_def, clarsimp) 
+  apply (unfold lexord_def Let_def, clarsimp)
   apply (rule_tac f = "(% a b. a \<or> b)" in arg_cong2)
-  apply auto 
+  apply auto
   apply (rule_tac x="hd (drop (length x) y)" in exI)
   apply (rule_tac x="tl (drop (length x) y)" in exI)
-  apply (erule subst, simp add: min_def) 
-  apply (rule_tac x ="length u" in exI, simp) 
-  apply (rule_tac x ="take i x" in exI) 
-  apply (rule_tac x ="x ! i" in exI) 
-  apply (rule_tac x ="y ! i" in exI, safe) 
+  apply (erule subst, simp add: min_def)
+  apply (rule_tac x ="length u" in exI, simp)
+  apply (rule_tac x ="take i x" in exI)
+  apply (rule_tac x ="x ! i" in exI)
+  apply (rule_tac x ="y ! i" in exI, safe)
   apply (rule_tac x="drop (Suc i) x" in exI)
-  apply (drule sym, simp add: Cons_nth_drop_Suc) 
+  apply (drule sym, simp add: Cons_nth_drop_Suc)
   apply (rule_tac x="drop (Suc i) y" in exI)
-  by (simp add: Cons_nth_drop_Suc) 
-
-\<comment> \<open>lexord is extension of partial ordering List.lex\<close> 
+  by (simp add: Cons_nth_drop_Suc)
+
+\<comment> \<open>lexord is extension of partial ordering List.lex\<close>
 lemma lexord_lex: "(x,y) \<in> lex r = ((x,y) \<in> lexord r \<and> length x = length y)"
-  apply (rule_tac x = y in spec) 
-  apply (induct_tac x, clarsimp) 
+  apply (rule_tac x = y in spec)
+  apply (induct_tac x, clarsimp)
   by (clarify, case_tac x, simp, force)
 
 lemma lexord_irreflexive: "ALL x. (x,x) \<notin> r \<Longrightarrow> (xs,xs) \<notin> lexord r"
 by (induct xs) auto
 
 text\<open>By Ren\'e Thiemann:\<close>
-lemma lexord_partial_trans: 
+lemma lexord_partial_trans:
   "(\<And>x y z. x \<in> set xs \<Longrightarrow> (x,y) \<in> r \<Longrightarrow> (y,z) \<in> r \<Longrightarrow> (x,z) \<in> r)
    \<Longrightarrow>  (xs,ys) \<in> lexord r  \<Longrightarrow>  (ys,zs) \<in> lexord r \<Longrightarrow>  (xs,zs) \<in> lexord r"
 proof (induct xs arbitrary: ys zs)
@@ -5664,24 +5661,24 @@
   thus ?case unfolding zzs by auto
 qed
 
-lemma lexord_trans: 
+lemma lexord_trans:
     "\<lbrakk> (x, y) \<in> lexord r; (y, z) \<in> lexord r; trans r \<rbrakk> \<Longrightarrow> (x, z) \<in> lexord r"
 by(auto simp: trans_def intro:lexord_partial_trans)
 
 lemma lexord_transI:  "trans r \<Longrightarrow> trans (lexord r)"
-by (rule transI, drule lexord_trans, blast) 
+by (rule transI, drule lexord_trans, blast)
 
 lemma lexord_linear: "(! a b. (a,b)\<in> r | a = b | (b,a) \<in> r) \<Longrightarrow> (x,y) : lexord r | x = y | (y,x) : lexord r"
-  apply (rule_tac x = y in spec) 
-  apply (induct_tac x, rule allI) 
-  apply (case_tac x, simp, simp) 
-  apply (rule allI, case_tac x, simp, simp) 
+  apply (rule_tac x = y in spec)
+  apply (induct_tac x, rule allI)
+  apply (case_tac x, simp, simp)
+  apply (rule allI, case_tac x, simp, simp)
   by blast
 
 lemma lexord_irrefl:
   "irrefl R \<Longrightarrow> irrefl (lexord R)"
   by (simp add: irrefl_def lexord_irreflexive)
-  
+
 lemma lexord_asym:
   assumes "asym R"
   shows "asym (lexord R)"
@@ -5701,7 +5698,7 @@
     with assms Cons show ?case by (auto elim: asym.cases)
   qed
 qed
-   
+
 lemma lexord_asymmetric:
   assumes "asym R"
   assumes hyp: "(a, b) \<in> lexord R"
@@ -5766,7 +5763,7 @@
 lemma lexordp_append_leftD: "\<lbrakk> lexordp (xs @ us) (xs @ vs); \<forall>a. \<not> a < a \<rbrakk> \<Longrightarrow> lexordp us vs"
 by(induct xs) auto
 
-lemma lexordp_irreflexive: 
+lemma lexordp_irreflexive:
   assumes irrefl: "\<forall>x. \<not> x < x"
   shows "\<not> lexordp xs xs"
 proof
@@ -5834,8 +5831,8 @@
   "lexordp xs ys \<longleftrightarrow> (xs, ys) \<in> lexord {(x, y). x < y}"
 by(simp add: lexordp_iff lexord_def)
 
-lemma lexordp_eq_antisym: 
-  assumes "lexordp_eq xs ys" "lexordp_eq ys xs" 
+lemma lexordp_eq_antisym:
+  assumes "lexordp_eq xs ys" "lexordp_eq ys xs"
   shows "xs = ys"
 using assms by induct simp_all
 
@@ -5904,10 +5901,10 @@
 unfolding measures_def
 by blast
 
-lemma in_measures[simp]: 
+lemma in_measures[simp]:
   "(x, y) \<in> measures [] = False"
   "(x, y) \<in> measures (f # fs)
-         = (f x < f y \<or> (f x = f y \<and> (x, y) \<in> measures fs))"  
+         = (f x < f y \<or> (f x = f y \<and> (x, y) \<in> measures fs))"
 unfolding measures_def
 by auto
 
@@ -6081,39 +6078,39 @@
 
 
 lemma listrel_mono: "r \<subseteq> s \<Longrightarrow> listrel r \<subseteq> listrel s"
-apply clarify  
+apply clarify
 apply (erule listrel.induct)
 apply (blast intro: listrel.intros)+
 done
 
 lemma listrel_subset: "r \<subseteq> A \<times> A \<Longrightarrow> listrel r \<subseteq> lists A \<times> lists A"
-apply clarify 
-apply (erule listrel.induct, auto) 
+apply clarify
+apply (erule listrel.induct, auto)
 done
 
-lemma listrel_refl_on: "refl_on A r \<Longrightarrow> refl_on (lists A) (listrel r)" 
+lemma listrel_refl_on: "refl_on A r \<Longrightarrow> refl_on (lists A) (listrel r)"
 apply (simp add: refl_on_def listrel_subset Ball_def)
-apply (rule allI) 
-apply (induct_tac x) 
+apply (rule allI)
+apply (induct_tac x)
 apply (auto intro: listrel.intros)
 done
 
-lemma listrel_sym: "sym r \<Longrightarrow> sym (listrel r)" 
+lemma listrel_sym: "sym r \<Longrightarrow> sym (listrel r)"
 apply (auto simp add: sym_def)
-apply (erule listrel.induct) 
+apply (erule listrel.induct)
 apply (blast intro: listrel.intros)+
 done
 
-lemma listrel_trans: "trans r \<Longrightarrow> trans (listrel r)" 
+lemma listrel_trans: "trans r \<Longrightarrow> trans (listrel r)"
 apply (simp add: trans_def)
-apply (intro allI) 
-apply (rule impI) 
-apply (erule listrel.induct) 
+apply (intro allI)
+apply (rule impI)
+apply (erule listrel.induct)
 apply (blast intro: listrel.intros)+
 done
 
 theorem equiv_listrel: "equiv A r \<Longrightarrow> equiv (lists A) (listrel r)"
-by (simp add: equiv_def listrel_refl_on listrel_sym listrel_trans) 
+by (simp add: equiv_def listrel_refl_on listrel_sym listrel_trans)
 
 lemma listrel_rtrancl_refl[iff]: "(xs,xs) : listrel(r^*)"
 using listrel_refl_on[of UNIV, OF refl_rtrancl]
@@ -6161,7 +6158,7 @@
 lemma rtrancl_listrel1_ConsI2:
   "(x,y) \<in> r^* \<Longrightarrow> (xs, ys) \<in> (listrel1 r)^*
   \<Longrightarrow> (x # xs, y # ys) \<in> (listrel1 r)^*"
-  by (blast intro: rtrancl_trans rtrancl_listrel1_ConsI1 
+  by (blast intro: rtrancl_trans rtrancl_listrel1_ConsI1
     subsetD[OF listrel1_rtrancl_subset_rtrancl_listrel1 listrel1I1])
 
 lemma listrel1_subset_listrel:
@@ -6209,11 +6206,11 @@
 lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (size_option f)"
 by (rule is_measure_trivial)
 
-lemma size_list_estimation[termination_simp]: 
+lemma size_list_estimation[termination_simp]:
   "x \<in> set xs \<Longrightarrow> y < f x \<Longrightarrow> y < size_list f xs"
 by (induct xs) auto
 
-lemma size_list_estimation'[termination_simp]: 
+lemma size_list_estimation'[termination_simp]:
   "x \<in> set xs \<Longrightarrow> y \<le> f x \<Longrightarrow> y \<le> size_list f xs"
 by (induct xs) auto
 
@@ -6223,7 +6220,7 @@
 lemma size_list_append[simp]: "size_list f (xs @ ys) = size_list f xs + size_list f ys"
 by (induct xs, auto)
 
-lemma size_list_pointwise[termination_simp]: 
+lemma size_list_pointwise[termination_simp]:
   "(\<And>x. x \<in> set xs \<Longrightarrow> f x \<le> g x) \<Longrightarrow> size_list f xs \<le> size_list g xs"
 by (induct xs) force+
 
@@ -6250,7 +6247,7 @@
 qed
 
 lemma set_list_bind: "set (List.bind xs f) = (\<Union>x\<in>set xs. set (f x))"
-  by (induction xs) simp_all  
+  by (induction xs) simp_all
 
 
 subsection \<open>Transfer\<close>