src/HOL/List.thy
changeset 53374 a14d2a854c02
parent 53017 0f376701e83b
child 53412 01b804df0a30
     1.1 --- a/src/HOL/List.thy	Tue Sep 03 00:51:08 2013 +0200
     1.2 +++ b/src/HOL/List.thy	Tue Sep 03 01:12:40 2013 +0200
     1.3 @@ -722,12 +722,18 @@
     1.4  using `xs \<noteq> []` proof (induct xs)
     1.5    case Nil then show ?case by simp
     1.6  next
     1.7 -  case (Cons x xs) show ?case proof (cases xs)
     1.8 -    case Nil with single show ?thesis by simp
     1.9 +  case (Cons x xs)
    1.10 +  show ?case
    1.11 +  proof (cases xs)
    1.12 +    case Nil
    1.13 +    with single show ?thesis by simp
    1.14    next
    1.15 -    case Cons then have "xs \<noteq> []" by simp
    1.16 -    moreover with Cons.hyps have "P xs" .
    1.17 -    ultimately show ?thesis by (rule cons)
    1.18 +    case Cons
    1.19 +    show ?thesis
    1.20 +    proof (rule cons)
    1.21 +      from Cons show "xs \<noteq> []" by simp
    1.22 +      with Cons.hyps show "P xs" .
    1.23 +    qed
    1.24    qed
    1.25  qed
    1.26  
    1.27 @@ -1061,12 +1067,13 @@
    1.28  lemma map_eq_imp_length_eq:
    1.29    assumes "map f xs = map g ys"
    1.30    shows "length xs = length ys"
    1.31 -using assms proof (induct ys arbitrary: xs)
    1.32 +  using assms
    1.33 +proof (induct ys arbitrary: xs)
    1.34    case Nil then show ?case by simp
    1.35  next
    1.36    case (Cons y ys) then obtain z zs where xs: "xs = z # zs" by auto
    1.37    from Cons xs have "map f zs = map g ys" by simp
    1.38 -  moreover with Cons have "length zs = length ys" by blast
    1.39 +  with Cons have "length zs = length ys" by blast
    1.40    with xs show ?case by simp
    1.41  qed
    1.42    
    1.43 @@ -1669,10 +1676,10 @@
    1.44    hence n: "n < Suc (length xs)" by simp
    1.45    moreover
    1.46    { assume "n < length xs"
    1.47 -    with n obtain n' where "length xs - n = Suc n'"
    1.48 +    with n obtain n' where n': "length xs - n = Suc n'"
    1.49        by (cases "length xs - n", auto)
    1.50      moreover
    1.51 -    then have "length xs - Suc n = n'" by simp
    1.52 +    from n' have "length xs - Suc n = n'" by simp
    1.53      ultimately
    1.54      have "xs ! (length xs - Suc n) = (x # xs) ! (length xs - n)" by simp
    1.55    }
    1.56 @@ -3801,14 +3808,12 @@
    1.57      then have "\<exists>m n zs. concat (replicate m zs) = xs' \<and> concat (replicate n zs) = ws"
    1.58        using False and `xs' \<noteq> []` and `ys' = xs' @ ws` and len
    1.59        by (intro less.hyps) auto
    1.60 -    then obtain m n zs where "concat (replicate m zs) = xs'"
    1.61 +    then obtain m n zs where *: "concat (replicate m zs) = xs'"
    1.62        and "concat (replicate n zs) = ws" by blast
    1.63 -    moreover
    1.64      then have "concat (replicate (m + n) zs) = ys'"
    1.65        using `ys' = xs' @ ws`
    1.66        by (simp add: replicate_add)
    1.67 -    ultimately
    1.68 -    show ?thesis by blast
    1.69 +    with * show ?thesis by blast
    1.70    qed
    1.71    then show ?case
    1.72      using xs'_def ys'_def by metis
    1.73 @@ -4074,8 +4079,8 @@
    1.74    case Nil thus ?case by simp
    1.75  next
    1.76    case (Cons a xs)
    1.77 -  moreover hence "!x. x: set xs \<longrightarrow> x \<noteq> a" by auto
    1.78 -  ultimately show ?case by(simp add: sublist_Cons cong:filter_cong)
    1.79 +  then have "!x. x: set xs \<longrightarrow> x \<noteq> a" by auto
    1.80 +  with Cons show ?case by(simp add: sublist_Cons cong:filter_cong)
    1.81  qed
    1.82  
    1.83  
    1.84 @@ -4195,8 +4200,8 @@
    1.85    hence "foldr (\<lambda>xs. max (length xs)) xss 0 = 0"
    1.86    proof (induct xss)
    1.87      case (Cons x xs)
    1.88 -    moreover hence "x = []" by (cases x) auto
    1.89 -    ultimately show ?case by auto
    1.90 +    then have "x = []" by (cases x) auto
    1.91 +    with Cons show ?case by auto
    1.92    qed simp
    1.93    thus ?thesis using True by simp
    1.94  next
    1.95 @@ -4585,7 +4590,7 @@
    1.96  proof -
    1.97    from assms have "map f xs = map f ys"
    1.98      by (simp add: sorted_distinct_set_unique)
    1.99 -  moreover with `inj_on f (set xs \<union> set ys)` show "xs = ys"
   1.100 +  with `inj_on f (set xs \<union> set ys)` show "xs = ys"
   1.101      by (blast intro: map_inj_on)
   1.102  qed
   1.103  
   1.104 @@ -4620,11 +4625,12 @@
   1.105  lemma foldr_max_sorted:
   1.106    assumes "sorted (rev xs)"
   1.107    shows "foldr max xs y = (if xs = [] then y else max (xs ! 0) y)"
   1.108 -using assms proof (induct xs)
   1.109 +  using assms
   1.110 +proof (induct xs)
   1.111    case (Cons x xs)
   1.112 -  moreover hence "sorted (rev xs)" using sorted_append by auto
   1.113 -  ultimately show ?case
   1.114 -    by (cases xs, auto simp add: sorted_append max_def)
   1.115 +  then have "sorted (rev xs)" using sorted_append by auto
   1.116 +  with Cons show ?case
   1.117 +    by (cases xs) (auto simp add: sorted_append max_def)
   1.118  qed simp
   1.119  
   1.120  lemma filter_equals_takeWhile_sorted_rev: