src/HOL/List.thy
 changeset 53374 a14d2a854c02 parent 53017 0f376701e83b child 53412 01b804df0a30
```--- a/src/HOL/List.thy	Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/List.thy	Tue Sep 03 01:12:40 2013 +0200
@@ -722,12 +722,18 @@
using `xs \<noteq> []` proof (induct xs)
case Nil then show ?case by simp
next
-  case (Cons x xs) show ?case proof (cases xs)
-    case Nil with single show ?thesis by simp
+  case (Cons x xs)
+  show ?case
+  proof (cases xs)
+    case Nil
+    with single show ?thesis by simp
next
-    case Cons then have "xs \<noteq> []" by simp
-    moreover with Cons.hyps have "P xs" .
-    ultimately show ?thesis by (rule cons)
+    case Cons
+    show ?thesis
+    proof (rule cons)
+      from Cons show "xs \<noteq> []" by simp
+      with Cons.hyps show "P xs" .
+    qed
qed
qed

@@ -1061,12 +1067,13 @@
lemma map_eq_imp_length_eq:
assumes "map f xs = map g ys"
shows "length xs = length ys"
-using assms proof (induct ys arbitrary: xs)
+  using assms
+proof (induct ys arbitrary: xs)
case Nil then show ?case by simp
next
case (Cons y ys) then obtain z zs where xs: "xs = z # zs" by auto
from Cons xs have "map f zs = map g ys" by simp
-  moreover with Cons have "length zs = length ys" by blast
+  with Cons have "length zs = length ys" by blast
with xs show ?case by simp
qed

@@ -1669,10 +1676,10 @@
hence n: "n < Suc (length xs)" by simp
moreover
{ assume "n < length xs"
-    with n obtain n' where "length xs - n = Suc n'"
+    with n obtain n' where n': "length xs - n = Suc n'"
by (cases "length xs - n", auto)
moreover
-    then have "length xs - Suc n = n'" by simp
+    from n' have "length xs - Suc n = n'" by simp
ultimately
have "xs ! (length xs - Suc n) = (x # xs) ! (length xs - n)" by simp
}
@@ -3801,14 +3808,12 @@
then have "\<exists>m n zs. concat (replicate m zs) = xs' \<and> concat (replicate n zs) = ws"
using False and `xs' \<noteq> []` and `ys' = xs' @ ws` and len
by (intro less.hyps) auto
-    then obtain m n zs where "concat (replicate m zs) = xs'"
+    then obtain m n zs where *: "concat (replicate m zs) = xs'"
and "concat (replicate n zs) = ws" by blast
-    moreover
then have "concat (replicate (m + n) zs) = ys'"
using `ys' = xs' @ ws`
by (simp add: replicate_add)
-    ultimately
-    show ?thesis by blast
+    with * show ?thesis by blast
qed
then show ?case
using xs'_def ys'_def by metis
@@ -4074,8 +4079,8 @@
case Nil thus ?case by simp
next
case (Cons a xs)
-  moreover hence "!x. x: set xs \<longrightarrow> x \<noteq> a" by auto
-  ultimately show ?case by(simp add: sublist_Cons cong:filter_cong)
+  then have "!x. x: set xs \<longrightarrow> x \<noteq> a" by auto
+  with Cons show ?case by(simp add: sublist_Cons cong:filter_cong)
qed

@@ -4195,8 +4200,8 @@
hence "foldr (\<lambda>xs. max (length xs)) xss 0 = 0"
proof (induct xss)
case (Cons x xs)
-    moreover hence "x = []" by (cases x) auto
-    ultimately show ?case by auto
+    then have "x = []" by (cases x) auto
+    with Cons show ?case by auto
qed simp
thus ?thesis using True by simp
next
@@ -4585,7 +4590,7 @@
proof -
from assms have "map f xs = map f ys"
by (simp add: sorted_distinct_set_unique)
-  moreover with `inj_on f (set xs \<union> set ys)` show "xs = ys"
+  with `inj_on f (set xs \<union> set ys)` show "xs = ys"
by (blast intro: map_inj_on)
qed

@@ -4620,11 +4625,12 @@
lemma foldr_max_sorted:
assumes "sorted (rev xs)"
shows "foldr max xs y = (if xs = [] then y else max (xs ! 0) y)"
-using assms proof (induct xs)
+  using assms
+proof (induct xs)
case (Cons x xs)
-  moreover hence "sorted (rev xs)" using sorted_append by auto
-  ultimately show ?case
-    by (cases xs, auto simp add: sorted_append max_def)
+  then have "sorted (rev xs)" using sorted_append by auto
+  with Cons show ?case
+    by (cases xs) (auto simp add: sorted_append max_def)
qed simp

lemma filter_equals_takeWhile_sorted_rev:```