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
```