src/HOL/Library/List_Prefix.thy
changeset 10408 d8b3613158b1
parent 10389 c7d8901ab269
child 10512 d34192966cd8
--- a/src/HOL/Library/List_Prefix.thy	Mon Nov 06 22:54:13 2000 +0100
+++ b/src/HOL/Library/List_Prefix.thy	Mon Nov 06 22:56:07 2000 +0100
@@ -137,49 +137,44 @@
 
 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"
-  (concl is "?E xs")
-proof -
-  assume "xs \<parallel> ys"
-  have "?this --> ?E xs" (is "?P xs")
-  proof (induct (stripped) xs rule: rev_induct)
-    assume "[] \<parallel> ys" hence False by auto
-    thus "?E []" ..
-  next
-    fix x xs
-    assume hyp: "?P xs"
-    assume asm: "xs @ [x] \<parallel> ys"
-    show "?E (xs @ [x])"
-    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
-        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:)
-        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:)
-        ultimately show ?thesis by blast
-      qed
-    next
-      assume "ys \<le> xs" hence "ys \<le> xs @ [x]" by simp
-      with asm have False by blast
+  (is "PROP ?P xs" concl is "?E xs")
+proof (induct xs rule: rev_induct)
+  assume "[] \<parallel> ys" hence False by auto
+  thus "?E []" ..
+next
+  fix x xs
+  assume hyp: "PROP ?P xs"
+  assume asm: "xs @ [x] \<parallel> ys"
+  show "?E (xs @ [x])"
+  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
+      hence False by blast
       thus ?thesis ..
     next
-      assume "xs \<parallel> ys"
-      with hyp 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
-      with neq ys show ?thesis by blast
+      fix c cs assume ys': "ys' = c # cs"
+      with asm 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:)
+      ultimately show ?thesis by blast
     qed
+  next
+    assume "ys \<le> xs" hence "ys \<le> xs @ [x]" by simp
+    with asm 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"
+      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
+    with neq ys show ?thesis by blast
   qed
-  thus ?thesis ..
 qed
 
 end