src/HOL/Library/List_Prefix.thy
 changeset 11987 bf31b35949ce parent 11780 d17ee2241257 child 12338 de0f4a63baa5
```     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
```