src/HOL/Library/List_Prefix.thy
 changeset 23254 99644a53f16d parent 22178 29b95968272b child 23394 474ff28210c0
```     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"
```