src/HOL/Lambda/ListOrder.thy

   Lifting an order to lists of elements, relating exactly one
   element.
 *}
 
 definition
-  step1 :: "('a \<times> 'a) set => ('a list \<times> 'a list) set" where
+  step1 :: "('a => 'a => bool) => 'a list => 'a list => bool" where
   "step1 r =
-    {(ys, xs). \<exists>us z z' vs. xs = us @ z # vs \<and> (z', z) \<in> r \<and> ys =
-      us @ z' # vs}"
+    (\<lambda>ys xs. \<exists>us z z' vs. xs = us @ z # vs \<and> r z' z \<and> ys =
+      us @ z' # vs)"
 
 
-lemma step1_converse [simp]: "step1 (r^-1) = (step1 r)^-1"
+lemma step1_converse [simp]: "step1 (r^--1) = (step1 r)^--1"
+  apply (unfold step1_def)
+  apply (blast intro!: order_antisym)
+  done
+
+lemma in_step1_converse [iff]: "(step1 (r^--1) x y) = ((step1 r)^--1 x y)"
+  apply auto
+  done
+
+lemma not_Nil_step1 [iff]: "\<not> step1 r [] xs"
   apply (unfold step1_def)
   apply blast
   done
 
-lemma in_step1_converse [iff]: "(p \<in> step1 (r^-1)) = (p \<in> (step1 r)^-1)"
-  apply auto
-  done
-
-lemma not_Nil_step1 [iff]: "([], xs) \<notin> step1 r"
-  apply (unfold step1_def)
-  apply blast
-  done
-
-lemma not_step1_Nil [iff]: "(xs, []) \<notin> step1 r"
+lemma not_step1_Nil [iff]: "\<not> step1 r xs []"
   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)"
+    "(step1 r (y # ys) (x # xs)) =
+      (r y x \<and> xs = ys \<or> x = y \<and> step1 r ys xs)"
   apply (unfold step1_def)
-  apply simp
   apply (rule iffI)
    apply (erule exE)
    apply (rename_tac ts)
    apply (case_tac ts)
     apply fastsimp

    apply blast
   apply (blast intro: Cons_eq_appendI)
   done
 
 lemma append_step1I:
-  "(ys, xs) \<in> step1 r \<and> vs = us \<or> ys = xs \<and> (vs, us) \<in> step1 r
-    ==> (ys @ vs, xs @ us) : step1 r"
+  "step1 r ys xs \<and> vs = us \<or> ys = xs \<and> step1 r vs us
+    ==> step1 r (ys @ vs) (xs @ us)"
   apply (unfold step1_def)
   apply auto
    apply blast
   apply (blast intro: append_eq_appendI)
   done
 
 lemma Cons_step1E [elim!]:
-  assumes "(ys, x # xs) \<in> step1 r"
-    and "!!y. ys = y # xs \<Longrightarrow> (y, x) \<in> r \<Longrightarrow> R"
-    and "!!zs. ys = x # zs \<Longrightarrow> (zs, xs) \<in> step1 r \<Longrightarrow> R"
+  assumes "step1 r ys (x # xs)"
+    and "!!y. ys = y # xs \<Longrightarrow> r y x \<Longrightarrow> R"
+    and "!!zs. ys = x # zs \<Longrightarrow> step1 r zs xs \<Longrightarrow> R"
   shows R
   using prems
   apply (cases ys)
    apply (simp add: step1_def)
   apply blast
   done
 
 lemma Snoc_step1_SnocD:
-  "(ys @ [y], xs @ [x]) \<in> step1 r
-    ==> ((ys, xs) \<in> step1 r \<and> y = x \<or> ys = xs \<and> (y, x) \<in> r)"
+  "step1 r (ys @ [y]) (xs @ [x])
+    ==> (step1 r ys xs \<and> y = x \<or> ys = xs \<and> r y x)"
   apply (unfold step1_def)
-  apply simp
   apply (clarify del: disjCI)
   apply (rename_tac vs)
   apply (rule_tac xs = vs in rev_exhaust)
    apply force
   apply simp
   apply blast
   done
 
 lemma Cons_acc_step1I [intro!]:
-    "x \<in> acc r ==> xs \<in> acc (step1 r) \<Longrightarrow> x # xs \<in> acc (step1 r)"
+    "acc r x ==> acc (step1 r) xs \<Longrightarrow> acc (step1 r) (x # xs)"
   apply (induct arbitrary: xs set: acc)
   apply (erule thin_rl)
   apply (erule acc_induct)
   apply (rule accI)
   apply blast
   done
 
-lemma lists_accD: "xs \<in> lists (acc r) ==> xs \<in> acc (step1 r)"
-  apply (induct set: lists)
+lemma lists_accD: "listsp (acc r) xs ==> acc (step1 r) xs"
+  apply (induct set: listsp)
    apply (rule accI)
    apply simp
   apply (rule accI)
   apply (fast dest: acc_downward)
   done
 
 lemma ex_step1I:
-  "[| x \<in> set xs; (y, x) \<in> r |]
-    ==> \<exists>ys. (ys, xs) \<in> step1 r \<and> y \<in> set ys"
+  "[| x \<in> set xs; r y x |]
+    ==> \<exists>ys. step1 r ys xs \<and> y \<in> set ys"
   apply (unfold step1_def)
   apply (drule in_set_conv_decomp [THEN iffD1])
   apply force
   done
 
-lemma lists_accI: "xs \<in> acc (step1 r) ==> xs \<in> lists (acc r)"
+lemma lists_accI: "acc (step1 r) xs ==> listsp (acc r) xs"
   apply (induct set: acc)
   apply clarify
   apply (rule accI)
-  apply (drule ex_step1I, assumption)
+  apply (drule_tac r=r in ex_step1I, assumption)
   apply blast
   done
 
 end