--- a/src/HOL/Lambda/ListOrder.thy Wed Feb 07 17:39:49 2007 +0100
+++ b/src/HOL/Lambda/ListOrder.thy Wed Feb 07 17:41:11 2007 +0100
@@ -14,36 +14,35 @@
*}
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)
@@ -56,8 +55,8 @@
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
@@ -65,9 +64,9 @@
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)
@@ -76,10 +75,9 @@
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)
@@ -89,7 +87,7 @@
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)
@@ -97,8 +95,8 @@
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)
@@ -106,18 +104,18 @@
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