src/HOL/Proofs/Lambda/ListOrder.thy
 author haftmann Sat, 05 Jul 2014 11:01:53 +0200 changeset 57514 bdc2c6b40bf2 parent 54295 45a5523d4a63 child 58372 bfd497f2f4c2 permissions -rw-r--r--
prefer ac_simps collections over separate name bindings for add and mult
```
(*  Title:      HOL/Proofs/Lambda/ListOrder.thy
Author:     Tobias Nipkow
*)

header {* Lifting an order to lists of elements *}

theory ListOrder imports Main begin

declare [[syntax_ambiguity_warning = false]]

text {*
Lifting an order to lists of elements, relating exactly one
element.
*}

definition
step1 :: "('a => 'a => bool) => 'a list => 'a list => bool" where
"step1 r =
(\<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"
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 not_step1_Nil [iff]: "\<not> step1 r xs []"
apply (unfold step1_def)
apply blast
done

lemma Cons_step1_Cons [iff]:
"(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 (rule iffI)
apply (erule exE)
apply (rename_tac ts)
apply (case_tac ts)
apply fastforce
apply force
apply (erule disjE)
apply blast
apply (blast intro: Cons_eq_appendI)
done

lemma append_step1I:
"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 "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 assms
apply (cases ys)
apply blast
done

lemma Snoc_step1_SnocD:
"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 (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!]:
"Wellfounded.accp r x ==> Wellfounded.accp (step1 r) xs \<Longrightarrow> Wellfounded.accp (step1 r) (x # xs)"
apply (induct arbitrary: xs set: Wellfounded.accp)
apply (erule thin_rl)
apply (erule accp_induct)
apply (rule accp.accI)
apply blast
done

lemma lists_accD: "listsp (Wellfounded.accp r) xs ==> Wellfounded.accp (step1 r) xs"
apply (induct set: listsp)
apply (rule accp.accI)
apply simp
apply (rule accp.accI)
apply (fast dest: accp_downward)
done

lemma ex_step1I:
"[| 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: "Wellfounded.accp (step1 r) xs ==> listsp (Wellfounded.accp r) xs"
apply (induct set: Wellfounded.accp)
apply clarify
apply (rule accp.accI)
apply (drule_tac r=r in ex_step1I, assumption)
apply blast
done

end
```