1.1 --- a/src/HOL/Library/List_Prefix.thy	Mon Nov 06 22:54:13 2000 +0100
     1.2 +++ b/src/HOL/Library/List_Prefix.thy	Mon Nov 06 22:56:07 2000 +0100
     1.3 @@ -137,49 +137,44 @@
     1.4  
     1.5  theorem parallel_decomp:
     1.6    "xs \<parallel> ys ==> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs"
     1.7 -  (concl is "?E xs")
     1.8 -proof -
     1.9 -  assume "xs \<parallel> ys"
    1.10 -  have "?this --> ?E xs" (is "?P xs")
    1.11 -  proof (induct (stripped) xs rule: rev_induct)
    1.12 -    assume "[] \<parallel> ys" hence False by auto
    1.13 -    thus "?E []" ..
    1.14 -  next
    1.15 -    fix x xs
    1.16 -    assume hyp: "?P xs"
    1.17 -    assume asm: "xs @ [x] \<parallel> ys"
    1.18 -    show "?E (xs @ [x])"
    1.19 -    proof (rule prefix_cases)
    1.20 -      assume le: "xs \<le> ys"
    1.21 -      then obtain ys' where ys: "ys = xs @ ys'" ..
    1.22 -      show ?thesis
    1.23 -      proof (cases ys')
    1.24 -        assume "ys' = []" with ys have "xs = ys" by simp
    1.25 -        with asm have "[x] \<parallel> []" by auto
    1.26 -        hence False by blast
    1.27 -        thus ?thesis ..
    1.28 -      next
    1.29 -        fix c cs assume ys': "ys' = c # cs"
    1.30 -        with asm ys have "xs @ [x] \<parallel> xs @ c # cs" by (simp only:)
    1.31 -        hence "x \<noteq> c" by auto
    1.32 -        moreover have "xs @ [x] = xs @ x # []" by simp
    1.33 -        moreover from ys ys' have "ys = xs @ c # cs" by (simp only:)
    1.34 -        ultimately show ?thesis by blast
    1.35 -      qed
    1.36 -    next
    1.37 -      assume "ys \<le> xs" hence "ys \<le> xs @ [x]" by simp
    1.38 -      with asm have False by blast
    1.39 +  (is "PROP ?P xs" concl is "?E xs")
    1.40 +proof (induct xs rule: rev_induct)
    1.41 +  assume "[] \<parallel> ys" hence False by auto
    1.42 +  thus "?E []" ..
    1.43 +next
    1.44 +  fix x xs
    1.45 +  assume hyp: "PROP ?P xs"
    1.46 +  assume asm: "xs @ [x] \<parallel> ys"
    1.47 +  show "?E (xs @ [x])"
    1.48 +  proof (rule prefix_cases)
    1.49 +    assume le: "xs \<le> ys"
    1.50 +    then obtain ys' where ys: "ys = xs @ ys'" ..
    1.51 +    show ?thesis
    1.52 +    proof (cases ys')
    1.53 +      assume "ys' = []" with ys have "xs = ys" by simp
    1.54 +      with asm have "[x] \<parallel> []" by auto
    1.55 +      hence False by blast
    1.56        thus ?thesis ..
    1.57      next
    1.58 -      assume "xs \<parallel> ys"
    1.59 -      with hyp obtain as b bs c cs where neq: "(b::'a) \<noteq> c"
    1.60 -          and xs: "xs = as @ b # bs" and ys: "ys = as @ c # cs"
    1.61 -	by blast
    1.62 -      from xs have "xs @ [x] = as @ b # (bs @ [x])" by simp
    1.63 -      with neq ys show ?thesis by blast
    1.64 +      fix c cs assume ys': "ys' = c # cs"
    1.65 +      with asm ys have "xs @ [x] \<parallel> xs @ c # cs" by (simp only:)
    1.66 +      hence "x \<noteq> c" by auto
    1.67 +      moreover have "xs @ [x] = xs @ x # []" by simp
    1.68 +      moreover from ys ys' have "ys = xs @ c # cs" by (simp only:)
    1.69 +      ultimately show ?thesis by blast
    1.70      qed
    1.71 +  next
    1.72 +    assume "ys \<le> xs" hence "ys \<le> xs @ [x]" by simp
    1.73 +    with asm have False by blast
    1.74 +    thus ?thesis ..
    1.75 +  next
    1.76 +    assume "xs \<parallel> ys"
    1.77 +    with hyp obtain as b bs c cs where neq: "(b::'a) \<noteq> c"
    1.78 +      and xs: "xs = as @ b # bs" and ys: "ys = as @ c # cs"
    1.79 +      by blast
    1.80 +    from xs have "xs @ [x] = as @ b # (bs @ [x])" by simp
    1.81 +    with neq ys show ?thesis by blast
    1.82    qed
    1.83 -  thus ?thesis ..
    1.84  qed
    1.85  
    1.86  end