# HG changeset patch
# User wenzelm
# Date 1194551547 -3600
# Node ID 059c03630d6ef676afcda1e0d63a3209a568364e
# Parent  69c0a39ba028123a3889f615a26a291296d8dea1
tuned presentation;

diff -r 69c0a39ba028 -r 059c03630d6e src/HOL/Library/List_Prefix.thy
--- a/src/HOL/Library/List_Prefix.thy	Thu Nov 08 20:09:17 2007 +0100
+++ b/src/HOL/Library/List_Prefix.thy	Thu Nov 08 20:52:27 2007 +0100
@@ -190,12 +190,13 @@
 
 lemma not_prefix_cases:
   assumes pfx: "\<not> ps \<le> ls"
-  and c1: "\<lbrakk> ps \<noteq> []; ls = [] \<rbrakk> \<Longrightarrow> R"
-  and c2: "\<And>a as x xs. \<lbrakk> ps = a#as; ls = x#xs; x = a; \<not> as \<le> xs\<rbrakk> \<Longrightarrow> R"
-  and c3: "\<And>a as x xs. \<lbrakk> ps = a#as; ls = x#xs; x \<noteq> a\<rbrakk> \<Longrightarrow> R"
-  shows "R"
+  obtains
+    (c1) "ps \<noteq> []" and "ls = []"
+  | (c2) a as x xs where "ps = a#as" and "ls = x#xs" and "x = a" and "\<not> as \<le> xs"
+  | (c3) a as x xs where "ps = a#as" and "ls = x#xs" and "x \<noteq> a"
 proof (cases ps)
-  case Nil then show ?thesis using pfx by simp
+  case Nil
+  then show ?thesis using pfx by simp
 next
   case (Cons a as)
   then have c: "ps = a#as" .
@@ -221,11 +222,10 @@
 
 lemma not_prefix_induct [consumes 1, case_names Nil Neq Eq]:
   assumes np: "\<not> ps \<le> ls"
-  and base:   "\<And>x xs. P (x#xs) []"
-  and r1:     "\<And>x xs y ys. x \<noteq> y \<Longrightarrow> P (x#xs) (y#ys)"
-  and r2:     "\<And>x xs y ys. \<lbrakk> x = y; \<not> xs \<le> ys; P xs ys \<rbrakk> \<Longrightarrow> P (x#xs) (y#ys)"
-  shows "P ps ls"
-  using np
+    and base: "\<And>x xs. P (x#xs) []"
+    and r1: "\<And>x xs y ys. x \<noteq> y \<Longrightarrow> P (x#xs) (y#ys)"
+    and r2: "\<And>x xs y ys. \<lbrakk> x = y; \<not> xs \<le> ys; P xs ys \<rbrakk> \<Longrightarrow> P (x#xs) (y#ys)"
+  shows "P ps ls" using np
 proof (induct ls arbitrary: ps)
   case Nil then show ?case
     by (auto simp: neq_Nil_conv elim!: not_prefix_cases intro!: base)
@@ -242,6 +242,7 @@
     by (simp only: pv) (erule not_prefix_cases, auto intro: r1 r2 ih)
 qed
 
+
 subsection {* Parallel lists *}
 
 definition
@@ -310,10 +311,10 @@
   "\<lbrakk> xs \<parallel> ys; x = xs @ xs' ; y = ys @ ys' \<rbrakk> \<Longrightarrow> x \<parallel> y"
   by simp (rule parallel_append)
 
-lemma parallel_commute:
-  "(a \<parallel> b) = (b \<parallel> a)"
+lemma parallel_commute: "(a \<parallel> b) = (b \<parallel> a)"
   unfolding parallel_def by auto
 
+
 subsection {* Postfix order on lists *}
 
 definition
@@ -380,30 +381,29 @@
 qed
 
 lemma distinct_postfix:
-  assumes dx: "distinct xs"
-  and     pf: "xs >>= ys"
-  shows   "distinct ys"
-  using dx pf by (clarsimp elim!: postfixE)
+  assumes "distinct xs"
+    and "xs >>= ys"
+  shows "distinct ys"
+  using assms by (clarsimp elim!: postfixE)
 
 lemma postfix_map:
-  assumes pf: "xs >>= ys"
-  shows   "map f xs >>= map f ys"
-  using pf by (auto elim!: postfixE intro: postfixI)
+  assumes "xs >>= ys"
+  shows "map f xs >>= map f ys"
+  using assms by (auto elim!: postfixE intro: postfixI)
 
-lemma postfix_drop:
-  "as >>= drop n as"
+lemma postfix_drop: "as >>= drop n as"
   unfolding postfix_def
   by (rule exI [where x = "take n as"]) simp
 
 lemma postfix_take:
-  "xs >>= ys \<Longrightarrow> xs = take (length xs - length ys) xs @ ys"
+    "xs >>= ys \<Longrightarrow> xs = take (length xs - length ys) xs @ ys"
   by (clarsimp elim!: postfixE)
 
-lemma parallelD1:
-  "x \<parallel> y \<Longrightarrow> \<not> x \<le> y" by blast
+lemma parallelD1: "x \<parallel> y \<Longrightarrow> \<not> x \<le> y"
+  by blast
 
-lemma parallelD2:
-  "x \<parallel> y \<Longrightarrow> \<not> y \<le> x" by blast
+lemma parallelD2: "x \<parallel> y \<Longrightarrow> \<not> y \<le> x"
+  by blast
 
 lemma parallel_Nil1 [simp]: "\<not> x \<parallel> []"
   unfolding parallel_def by simp
@@ -426,11 +426,12 @@
 
 lemma not_equal_is_parallel:
   assumes neq: "xs \<noteq> ys"
-  and     len: "length xs = length ys"
-  shows   "xs \<parallel> ys"
+    and len: "length xs = length ys"
+  shows "xs \<parallel> ys"
   using len neq
 proof (induct rule: list_induct2)
-  case 1 then show ?case by simp
+  case 1
+  then show ?case by simp
 next
   case (2 a as b bs)
   have ih: "as \<noteq> bs \<Longrightarrow> as \<parallel> bs" by fact
@@ -447,18 +448,18 @@
 qed
 
 
-subsection {* Exeuctable code *}
+subsection {* Executable code *}
 
 lemma less_eq_code [code func]:
-  "([]\<Colon>'a\<Colon>{eq, ord} list) \<le> xs \<longleftrightarrow> True"
-  "(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> [] \<longleftrightarrow> False"
-  "(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> y # ys \<longleftrightarrow> x = y \<and> xs \<le> ys"
+    "([]\<Colon>'a\<Colon>{eq, ord} list) \<le> xs \<longleftrightarrow> True"
+    "(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> [] \<longleftrightarrow> False"
+    "(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> y # ys \<longleftrightarrow> x = y \<and> xs \<le> ys"
   by simp_all
 
 lemma less_code [code func]:
-  "xs < ([]\<Colon>'a\<Colon>{eq, ord} list) \<longleftrightarrow> False"
-  "[] < (x\<Colon>'a\<Colon>{eq, ord})# xs \<longleftrightarrow> True"
-  "(x\<Colon>'a\<Colon>{eq, ord}) # xs < y # ys \<longleftrightarrow> x = y \<and> xs < ys"
+    "xs < ([]\<Colon>'a\<Colon>{eq, ord} list) \<longleftrightarrow> False"
+    "[] < (x\<Colon>'a\<Colon>{eq, ord})# xs \<longleftrightarrow> True"
+    "(x\<Colon>'a\<Colon>{eq, ord}) # xs < y # ys \<longleftrightarrow> x = y \<and> xs < ys"
   unfolding strict_prefix_def by auto
 
 lemmas [code func] = postfix_to_prefix