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

src/HOL/Library/List_Prefix.thy

changeset 10408 | d8b3613158b1 |

parent 10389 | c7d8901ab269 |

child 10512 | d34192966cd8 |

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