src/HOL/Library/List_Prefix.thy
changeset 11987 bf31b35949ce
parent 11780 d17ee2241257
child 12338 de0f4a63baa5
--- a/src/HOL/Library/List_Prefix.thy	Tue Oct 30 17:33:56 2001 +0100
+++ b/src/HOL/Library/List_Prefix.thy	Tue Oct 30 17:37:25 2001 +0100
@@ -151,27 +151,25 @@
 
 theorem parallel_decomp:
   "xs \<parallel> ys ==> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs"
-  (is "PROP ?P xs" concl is "?E xs")
 proof (induct xs rule: rev_induct)
-  assume "[] \<parallel> ys" hence False by auto
-  thus "?E []" ..
+  case Nil
+  hence False by auto
+  thus ?case ..
 next
-  fix x xs
-  assume hyp: "PROP ?P xs"
-  assume asm: "xs @ [x] \<parallel> ys"
-  show "?E (xs @ [x])"
+  case (snoc x xs)
+  show ?case
   proof (rule prefix_cases)
     assume le: "xs \<le> ys"
     then obtain ys' where ys: "ys = xs @ ys'" ..
     show ?thesis
     proof (cases ys')
       assume "ys' = []" with ys have "xs = ys" by simp
-      with asm have "[x] \<parallel> []" by auto
+      with snoc have "[x] \<parallel> []" by auto
       hence False by blast
       thus ?thesis ..
     next
       fix c cs assume ys': "ys' = c # cs"
-      with asm ys have "xs @ [x] \<parallel> xs @ c # cs" by (simp only:)
+      with snoc ys have "xs @ [x] \<parallel> xs @ c # cs" by (simp only:)
       hence "x \<noteq> c" by auto
       moreover have "xs @ [x] = xs @ x # []" by simp
       moreover from ys ys' have "ys = xs @ c # cs" by (simp only:)
@@ -179,11 +177,11 @@
     qed
   next
     assume "ys < xs" hence "ys \<le> xs @ [x]" by (simp add: strict_prefix_def)
-    with asm have False by blast
+    with snoc have False by blast
     thus ?thesis ..
   next
     assume "xs \<parallel> ys"
-    with hyp obtain as b bs c cs where neq: "(b::'a) \<noteq> c"
+    with snoc obtain as b bs c cs where neq: "(b::'a) \<noteq> c"
       and xs: "xs = as @ b # bs" and ys: "ys = as @ c # cs"
       by blast
     from xs have "xs @ [x] = as @ b # (bs @ [x])" by simp