src/HOL/Lambda/ListOrder.thy

 (*  Title:      HOL/Lambda/ListOrder.thy
     ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   1998 TU Muenchen
-
-Lifting an order to lists of elements, relating exactly one element
 *)
 
+header {* Lifting an order to lists of elements *}
+
 theory ListOrder = Acc:
+
+text {*
+  Lifting an order to lists of elements, relating exactly one
+  element.
+*}
 
 constdefs
   step1 :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
   "step1 r ==
-    {(ys, xs). \<exists>us z z' vs. xs = us @ z # vs \<and> (z', z) \<in> r \<and> ys = us @ z' # vs}"
+    {(ys, xs). \<exists>us z z' vs. xs = us @ z # vs \<and> (z', z) \<in> r \<and> ys =
+      us @ z' # vs}"
 
 
 lemma step1_converse [simp]: "step1 (r^-1) = (step1 r)^-1"
   apply (unfold step1_def)
   apply blast

   apply (unfold step1_def)
   apply blast
   done
 
 lemma Cons_step1_Cons [iff]:
-  "((y # ys, x # xs) \<in> step1 r) = ((y, x) \<in> r \<and> xs = ys \<or> x = y \<and> (ys, xs) \<in> step1 r)"
+    "((y # ys, x # xs) \<in> step1 r) =
+      ((y, x) \<in> r \<and> xs = ys \<or> x = y \<and> (ys, xs) \<in> step1 r)"
   apply (unfold step1_def)
   apply simp
   apply (rule iffI)
    apply (erule exE)
    apply (rename_tac ts)

   apply (blast intro: append_eq_appendI)
   done
 
 lemma Cons_step1E [rulify_prems, elim!]:
   "[| (ys, x # xs) \<in> step1 r;
-      \<forall>y. ys = y # xs --> (y, x) \<in> r --> R;
-      \<forall>zs. ys = x # zs --> (zs, xs) : step1 r --> R
+    \<forall>y. ys = y # xs --> (y, x) \<in> r --> R;
+    \<forall>zs. ys = x # zs --> (zs, xs) \<in> step1 r --> R
    |] ==> R"
   apply (case_tac ys)
    apply (simp add: step1_def)
   apply blast
   done

    apply simp
   apply (rule accI)
   apply (fast dest: acc_downward)
   done
 
-lemma ex_step1I: "[| x \<in> set xs; (y, x) \<in> r |]
+lemma ex_step1I:
+  "[| x \<in> set xs; (y, x) \<in> r |]
     ==> \<exists>ys. (ys, xs) \<in> step1 r \<and> y \<in> set ys"
   apply (unfold step1_def)
   apply (drule in_set_conv_decomp [THEN iffD1])
   apply force
   done