summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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