# Theory ListOrder

Up to index of Isabelle/HOL/Lambda

theory ListOrder
imports Accessible_Part
begin

    (*  Title:      HOL/Lambda/ListOrder.thy
        ID:         $Id: ListOrder.thy,v 1.10 2005/06/17 14:13:08 haftmann Exp $
        Author:     Tobias Nipkow
        Copyright   1998 TU Muenchen
    *)

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

    theory ListOrder imports Accessible_Part begin

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

    constdefs
      step1 :: "('a × 'a) set => ('a list × 'a list) set"
      "step1 r ==
        {(ys, xs). ∃us z z' vs. xs = us @ z # vs ∧ (z', z) ∈ r ∧ ys =
          us @ z' # vs}"

    lemma step1_converse [simp]: "step1 (r^-1) = (step1 r)^-1"
      apply (unfold step1_def)
      apply blast
      done

    lemma in_step1_converse [iff]: "(p ∈ step1 (r^-1)) = (p ∈ (step1 r)^-1)"
      apply auto
      done

    lemma not_Nil_step1 [iff]: "([], xs) ∉ step1 r"
      apply (unfold step1_def)
      apply blast
      done

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

    lemma Cons_step1_Cons [iff]:
        "((y # ys, x # xs) ∈ step1 r) =
          ((y, x) ∈ r ∧ xs = ys ∨ x = y ∧ (ys, xs) ∈ step1 r)"
      apply (unfold step1_def)
      apply simp
      apply (rule iffI)
       apply (erule exE)
       apply (rename_tac ts)
       apply (case_tac ts)
        apply fastsimp
       apply force
      apply (erule disjE)
       apply blast
      apply (blast intro: Cons_eq_appendI)
      done

    lemma append_step1I:
      "(ys, xs) ∈ step1 r ∧ vs = us ∨ ys = xs ∧ (vs, us) ∈ step1 r
        ==> (ys @ vs, xs @ us) : step1 r"
      apply (unfold step1_def)
      apply auto
       apply blast
      apply (blast intro: append_eq_appendI)
      done

    lemma Cons_step1E [rule_format, elim!]:
      "[| (ys, x # xs) ∈ step1 r;
        ∀y. ys = y # xs --> (y, x) ∈ r --> R;
        ∀zs. ys = x # zs --> (zs, xs) ∈ step1 r --> R
       |] ==> R"
      apply (case_tac ys)
       apply (simp add: step1_def)
      apply blast
      done

    lemma Snoc_step1_SnocD:
      "(ys @ [y], xs @ [x]) ∈ step1 r
        ==> ((ys, xs) ∈ step1 r ∧ y = x ∨ ys = xs ∧ (y, x) ∈ r)"
      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 [rule_format, intro!]:
        "x ∈ acc r ==> ∀xs. xs ∈ acc (step1 r) --> x # xs ∈ acc (step1 r)"
      apply (erule acc_induct)
      apply (erule thin_rl)
      apply clarify
      apply (erule acc_induct)
      apply (rule accI)
      apply blast
      done

    lemma lists_accD: "xs ∈ lists (acc r) ==> xs ∈ acc (step1 r)"
      apply (erule lists.induct)
       apply (rule accI)
       apply simp
      apply (rule accI)
      apply (fast dest: acc_downward)
      done

    lemma ex_step1I:
      "[| x ∈ set xs; (y, x) ∈ r |]
        ==> ∃ys. (ys, xs) ∈ step1 r ∧ y ∈ set ys"
      apply (unfold step1_def)
      apply (drule in_set_conv_decomp [THEN iffD1])
      apply force
      done

    lemma lists_accI: "xs ∈ acc (step1 r) ==> xs ∈ lists (acc r)"
      apply (erule acc_induct)
      apply clarify
      apply (rule accI)
      apply (drule ex_step1I, assumption)
      apply blast
      done

    end

lemma step1_converse:

      step1 (r^-1) = (step1 r)^-1

lemma in_step1_converse:

      (p ∈ step1 (r^-1)) = (p ∈ (step1 r)^-1)

lemma not_Nil_step1:

      ([], xs) ∉ step1 r

lemma not_step1_Nil:

      (xs, []) ∉ step1 r

lemma Cons_step1_Cons:

      ((y # ys, x # xs) ∈ step1 r) =
      ((y, x) ∈ r ∧ xs = ys ∨ x = y ∧ (ys, xs) ∈ step1 r)

lemma append_step1I:

      (ys, xs) ∈ step1 r ∧ vs = us ∨ ys = xs ∧ (vs, us) ∈ step1 r
      ==> (ys @ vs, xs @ us) ∈ step1 r

lemma Cons_step1E:

      [| (ys, x # xs) ∈ step1 r; !!y. [| ys = y # xs; (y, x) ∈ r |] ==> R;
         !!zs. [| ys = x # zs; (zs, xs) ∈ step1 r |] ==> R |]
      ==> R

lemma Snoc_step1_SnocD:

      (ys @ [y], xs @ [x]) ∈ step1 r
      ==> (ys, xs) ∈ step1 r ∧ y = x ∨ ys = xs ∧ (y, x) ∈ r

lemma Cons_acc_step1I:

      [| x ∈ acc r; xs ∈ acc (step1 r) |] ==> x # xs ∈ acc (step1 r)

lemma lists_accD:

      xs ∈ lists (acc r) ==> xs ∈ acc (step1 r)

lemma ex_step1I:

      [| x ∈ set xs; (y, x) ∈ r |] ==> ∃ys. (ys, xs) ∈ step1 r ∧ y ∈ set ys

lemma lists_accI:

      xs ∈ acc (step1 r) ==> xs ∈ lists (acc r)