Theory ListOrder

(*  Title:      HOL/Proofs/Lambda/ListOrder.thy
    Author:     Tobias Nipkow
    Copyright   1998 TU Muenchen
*)

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¯¯) = (step1 r)¯¯"
  apply (unfold step1_def)
  apply (blast intro!: order_antisym)
  done

lemma in_step1_converse [iff]: "(step1 (r¯¯) x y) = ((step1 r)¯¯ 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 (simp add: step1_def)
  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