author | wenzelm |

Tue Jun 05 16:26:07 2007 +0200 (2007-06-05) | |

changeset 23254 | 99644a53f16d |

parent 23253 | b1f3f53c60b5 |

child 23255 | 631bd424fd72 |

tuned proofs;

1.1 --- a/src/HOL/Library/List_Prefix.thy Tue Jun 05 16:26:06 2007 +0200 1.2 +++ b/src/HOL/Library/List_Prefix.thy Tue Jun 05 16:26:07 2007 +0200 1.3 @@ -66,24 +66,24 @@ 1.4 proof (cases zs rule: rev_cases) 1.5 assume "zs = []" 1.6 with zs have "xs = ys @ [y]" by simp 1.7 - thus ?thesis .. 1.8 + then show ?thesis .. 1.9 next 1.10 fix z zs' assume "zs = zs' @ [z]" 1.11 with zs have "ys = xs @ zs'" by simp 1.12 - hence "xs \<le> ys" .. 1.13 - thus ?thesis .. 1.14 + then have "xs \<le> ys" .. 1.15 + then show ?thesis .. 1.16 qed 1.17 next 1.18 assume "xs = ys @ [y] \<or> xs \<le> ys" 1.19 - thus "xs \<le> ys @ [y]" 1.20 + then show "xs \<le> ys @ [y]" 1.21 proof 1.22 assume "xs = ys @ [y]" 1.23 - thus ?thesis by simp 1.24 + then show ?thesis by simp 1.25 next 1.26 assume "xs \<le> ys" 1.27 then obtain zs where "ys = xs @ zs" .. 1.28 - hence "ys @ [y] = xs @ (zs @ [y])" by simp 1.29 - thus ?thesis .. 1.30 + then have "ys @ [y] = xs @ (zs @ [y])" by simp 1.31 + then show ?thesis .. 1.32 qed 1.33 qed 1.34 1.35 @@ -96,15 +96,15 @@ 1.36 lemma same_prefix_nil [iff]: "(xs @ ys \<le> xs) = (ys = [])" 1.37 proof - 1.38 have "(xs @ ys \<le> xs @ []) = (ys \<le> [])" by (rule same_prefix_prefix) 1.39 - thus ?thesis by simp 1.40 + then show ?thesis by simp 1.41 qed 1.42 1.43 lemma prefix_prefix [simp]: "xs \<le> ys ==> xs \<le> ys @ zs" 1.44 proof - 1.45 assume "xs \<le> ys" 1.46 then obtain us where "ys = xs @ us" .. 1.47 - hence "ys @ zs = xs @ (us @ zs)" by simp 1.48 - thus ?thesis .. 1.49 + then have "ys @ zs = xs @ (us @ zs)" by simp 1.50 + then show ?thesis .. 1.51 qed 1.52 1.53 lemma append_prefixD: "xs @ ys \<le> zs \<Longrightarrow> xs \<le> zs" 1.54 @@ -178,8 +178,8 @@ 1.55 "xs \<parallel> ys ==> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs" 1.56 proof (induct xs rule: rev_induct) 1.57 case Nil 1.58 - hence False by auto 1.59 - thus ?case .. 1.60 + then have False by auto 1.61 + then show ?case .. 1.62 next 1.63 case (snoc x xs) 1.64 show ?case 1.65 @@ -190,20 +190,20 @@ 1.66 proof (cases ys') 1.67 assume "ys' = []" with ys have "xs = ys" by simp 1.68 with snoc have "[x] \<parallel> []" by auto 1.69 - hence False by blast 1.70 - thus ?thesis .. 1.71 + then have False by blast 1.72 + then show ?thesis .. 1.73 next 1.74 fix c cs assume ys': "ys' = c # cs" 1.75 with snoc ys have "xs @ [x] \<parallel> xs @ c # cs" by (simp only:) 1.76 - hence "x \<noteq> c" by auto 1.77 + then have "x \<noteq> c" by auto 1.78 moreover have "xs @ [x] = xs @ x # []" by simp 1.79 moreover from ys ys' have "ys = xs @ c # cs" by (simp only:) 1.80 ultimately show ?thesis by blast 1.81 qed 1.82 next 1.83 - assume "ys < xs" hence "ys \<le> xs @ [x]" by (simp add: strict_prefix_def) 1.84 + assume "ys < xs" then have "ys \<le> xs @ [x]" by (simp add: strict_prefix_def) 1.85 with snoc have False by blast 1.86 - thus ?thesis .. 1.87 + then show ?thesis .. 1.88 next 1.89 assume "xs \<parallel> ys" 1.90 with snoc obtain as b bs c cs where neq: "(b::'a) \<noteq> c"