1.1 --- a/src/HOL/Library/List_Prefix.thy	Tue Oct 30 17:33:56 2001 +0100
     1.2 +++ b/src/HOL/Library/List_Prefix.thy	Tue Oct 30 17:37:25 2001 +0100
     1.3 @@ -151,27 +151,25 @@
     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 -  (is "PROP ?P xs" concl is "?E xs")
     1.8  proof (induct xs rule: rev_induct)
     1.9 -  assume "[] \<parallel> ys" hence False by auto
    1.10 -  thus "?E []" ..
    1.11 +  case Nil
    1.12 +  hence False by auto
    1.13 +  thus ?case ..
    1.14  next
    1.15 -  fix x xs
    1.16 -  assume hyp: "PROP ?P xs"
    1.17 -  assume asm: "xs @ [x] \<parallel> ys"
    1.18 -  show "?E (xs @ [x])"
    1.19 +  case (snoc x xs)
    1.20 +  show ?case
    1.21    proof (rule prefix_cases)
    1.22      assume le: "xs \<le> ys"
    1.23      then obtain ys' where ys: "ys = xs @ ys'" ..
    1.24      show ?thesis
    1.25      proof (cases ys')
    1.26        assume "ys' = []" with ys have "xs = ys" by simp
    1.27 -      with asm have "[x] \<parallel> []" by auto
    1.28 +      with snoc have "[x] \<parallel> []" by auto
    1.29        hence False by blast
    1.30        thus ?thesis ..
    1.31      next
    1.32        fix c cs assume ys': "ys' = c # cs"
    1.33 -      with asm ys have "xs @ [x] \<parallel> xs @ c # cs" by (simp only:)
    1.34 +      with snoc ys have "xs @ [x] \<parallel> xs @ c # cs" by (simp only:)
    1.35        hence "x \<noteq> c" by auto
    1.36        moreover have "xs @ [x] = xs @ x # []" by simp
    1.37        moreover from ys ys' have "ys = xs @ c # cs" by (simp only:)
    1.38 @@ -179,11 +177,11 @@
    1.39      qed
    1.40    next
    1.41      assume "ys < xs" hence "ys \<le> xs @ [x]" by (simp add: strict_prefix_def)
    1.42 -    with asm have False by blast
    1.43 +    with snoc have False by blast
    1.44      thus ?thesis ..
    1.45    next
    1.46      assume "xs \<parallel> ys"
    1.47 -    with hyp obtain as b bs c cs where neq: "(b::'a) \<noteq> c"
    1.48 +    with snoc obtain as b bs c cs where neq: "(b::'a) \<noteq> c"
    1.49        and xs: "xs = as @ b # bs" and ys: "ys = as @ c # cs"
    1.50        by blast
    1.51      from xs have "xs @ [x] = as @ b # (bs @ [x])" by simp