summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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: