# Theory ListOrder

theory ListOrder
imports Main
```(*  Title:      HOL/Proofs/Lambda/ListOrder.thy
Author:     Tobias Nipkow
*)

section ‹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 =
(λys xs. ∃us z z' vs. xs = us @ z # vs ∧ r z' z ∧ 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]: "¬ step1 r [] xs"
apply (unfold step1_def)
apply blast
done

lemma not_step1_Nil [iff]: "¬ step1 r xs []"
apply (unfold step1_def)
apply blast
done

lemma Cons_step1_Cons [iff]:
"(step1 r (y # ys) (x # xs)) =
(r y x ∧ xs = ys ∨ x = y ∧ 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 ∧ vs = us ∨ ys = xs ∧ 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 ⟹ r y x ⟹ R"
and "!!zs. ys = x # zs ⟹ step1 r zs xs ⟹ 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 ∧ y = x ∨ ys = xs ∧ 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 ⟹ 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 ∈ set xs; r y x |]
==> ∃ys. step1 r ys xs ∧ y ∈ 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
```