src/HOL/Imperative_HOL/ex/Sublist.thy

 
 lemma sublist'_back: "\<lbrakk> i < j; j \<le> length xs \<rbrakk> \<Longrightarrow> sublist' i j xs = sublist' i (j - 1) xs @ [xs ! (j - 1)]"
 apply (induct xs arbitrary: a i j)
 apply simp
 apply simp
-apply (case_tac j)
-apply simp
-apply auto
-apply (case_tac nat)
-apply auto
 done
 
 (* suffices that j \<le> length xs and length ys *) 
 lemma sublist'_eq_samelength_iff: "length xs = length ys \<Longrightarrow> (sublist' i j xs  = sublist' i j ys) = (\<forall>i'. i \<le> i' \<and> i' < j \<longrightarrow> xs ! i' = ys ! i')"
 proof (induct xs arbitrary: ys i j)

     apply simp
     apply auto
     apply (case_tac i', auto)
     apply (erule_tac x="Suc i'" in allE, auto)
     apply (erule_tac x="i' - 1" in allE, auto)
-    apply (case_tac i', auto)
     apply (erule_tac x="Suc i'" in allE, auto)
     done
 qed
 
 lemma sublist'_all[simp]: "sublist' 0 (length xs) xs = xs"

 lemma sublist'_append: "\<lbrakk> i \<le> j; j \<le> k \<rbrakk> \<Longrightarrow>(sublist' i j xs) @ (sublist' j k xs) = sublist' i k xs"
 by (induct xs arbitrary: i j k) auto
 
 lemma nth_sublist': "\<lbrakk> k < j - i; j \<le> length xs \<rbrakk> \<Longrightarrow> (sublist' i j xs) ! k = xs ! (i + k)"
 apply (induct xs arbitrary: i j k)
-apply auto
+apply simp
 apply (case_tac k)
-apply auto
-apply (case_tac i)
 apply auto
 done
 
 lemma set_sublist': "set (sublist' i j xs) = {x. \<exists>k. i \<le> k \<and> k < j \<and> k < List.length xs \<and> x = xs ! k}"
 apply (simp add: sublist'_sublist)