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"