# Theory ListOrder

Up to index of Isabelle/HOL/UNITY

theory ListOrder
imports Main
begin

    (*  Title:      HOL/UNITY/ListOrder
        ID:         $Id: ListOrder.thy,v 1.6 2005/06/17 14:13:10 haftmann Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   1998  University of Cambridge

    Lists are partially ordered by Charpentier's Generalized Prefix Relation
       (xs,ys) : genPrefix(r)
         if ys = xs' @ zs where length xs = length xs'
         and corresponding elements of xs, xs' are pairwise related by r

    Also overloads <= and < for lists!

    Based on Lex/Prefix
    *)

    header {*The Prefix Ordering on Lists*}

    theory ListOrder imports Main begin

    consts
      genPrefix :: "('a * 'a)set => ('a list * 'a list)set"

    inductive "genPrefix(r)"
     intros
       Nil:     "([],[]) : genPrefix(r)"

       prepend: "[| (xs,ys) : genPrefix(r);  (x,y) : r |] ==>
                 (x#xs, y#ys) : genPrefix(r)"

       append:  "(xs,ys) : genPrefix(r) ==> (xs, ys@zs) : genPrefix(r)"

    instance list :: (type)ord ..

    defs
      prefix_def:        "xs <= zs  ==  (xs,zs) : genPrefix Id"

      strict_prefix_def: "xs < zs  ==  xs <= zs & xs ~= (zs::'a list)"

    (*Constants for the <= and >= relations, used below in translations*)
    constdefs
      Le :: "(nat*nat) set"
        "Le == {(x,y). x <= y}"

      Ge :: "(nat*nat) set"
        "Ge == {(x,y). y <= x}"

    syntax
      pfixLe :: "[nat list, nat list] => bool"          (infixl "pfixLe" 50)
      pfixGe :: "[nat list, nat list] => bool"          (infixl "pfixGe" 50)

    translations
      "xs pfixLe ys" == "(xs,ys) : genPrefix Le"

      "xs pfixGe ys" == "(xs,ys) : genPrefix Ge"

    subsection{*preliminary lemmas*}

    lemma Nil_genPrefix [iff]: "([], xs) : genPrefix r"
    by (cut_tac genPrefix.Nil [THEN genPrefix.append], auto)

    lemma genPrefix_length_le: "(xs,ys) : genPrefix r ==> length xs <= length ys"
    by (erule genPrefix.induct, auto)

    lemma cdlemma:
         "[| (xs', ys'): genPrefix r |]
          ==> (ALL x xs. xs' = x#xs --> (EX y ys. ys' = y#ys & (x,y) : r & (xs, ys) : genPrefix r))"
    apply (erule genPrefix.induct, blast, blast)
    apply (force intro: genPrefix.append)
    done

    (*As usual converting it to an elimination rule is tiresome*)
    lemma cons_genPrefixE [elim!]:
         "[| (x#xs, zs): genPrefix r;
             !!y ys. [| zs = y#ys;  (x,y) : r;  (xs, ys) : genPrefix r |] ==> P
          |] ==> P"
    by (drule cdlemma, simp, blast)

    lemma Cons_genPrefix_Cons [iff]:
         "((x#xs,y#ys) : genPrefix r) = ((x,y) : r & (xs,ys) : genPrefix r)"
    by (blast intro: genPrefix.prepend)

    subsection{*genPrefix is a partial order*}

    lemma refl_genPrefix: "reflexive r ==> reflexive (genPrefix r)"

    apply (unfold refl_def, auto)
    apply (induct_tac "x")
    prefer 2 apply (blast intro: genPrefix.prepend)
    apply (blast intro: genPrefix.Nil)
    done

    lemma genPrefix_refl [simp]: "reflexive r ==> (l,l) : genPrefix r"
    by (erule reflD [OF refl_genPrefix UNIV_I])

    lemma genPrefix_mono: "r<=s ==> genPrefix r <= genPrefix s"
    apply clarify
    apply (erule genPrefix.induct)
    apply (auto intro: genPrefix.append)
    done

    (** Transitivity **)

    (*A lemma for proving genPrefix_trans_O*)
    lemma append_genPrefix [rule_format]:
         "ALL zs. (xs @ ys, zs) : genPrefix r --> (xs, zs) : genPrefix r"
    by (induct_tac "xs", auto)

    (*Lemma proving transitivity and more*)
    lemma genPrefix_trans_O [rule_format]:
         "(x, y) : genPrefix r
          ==> ALL z. (y,z) : genPrefix s --> (x, z) : genPrefix (s O r)"
    apply (erule genPrefix.induct)
      prefer 3 apply (blast dest: append_genPrefix)
     prefer 2 apply (blast intro: genPrefix.prepend, blast)
    done

    lemma genPrefix_trans [rule_format]:
         "[| (x,y) : genPrefix r;  (y,z) : genPrefix r;  trans r |]
          ==> (x,z) : genPrefix r"
    apply (rule trans_O_subset [THEN genPrefix_mono, THEN subsetD])
     apply assumption
    apply (blast intro: genPrefix_trans_O)
    done

    lemma prefix_genPrefix_trans [rule_format]:
         "[| x<=y;  (y,z) : genPrefix r |] ==> (x, z) : genPrefix r"
    apply (unfold prefix_def)
    apply (subst R_O_Id [symmetric], erule genPrefix_trans_O, assumption)
    done

    lemma genPrefix_prefix_trans [rule_format]:
         "[| (x,y) : genPrefix r;  y<=z |] ==> (x,z) : genPrefix r"
    apply (unfold prefix_def)
    apply (subst Id_O_R [symmetric], erule genPrefix_trans_O, assumption)
    done

    lemma trans_genPrefix: "trans r ==> trans (genPrefix r)"
    by (blast intro: transI genPrefix_trans)

    (** Antisymmetry **)

    lemma genPrefix_antisym [rule_format]:
         "[| (xs,ys) : genPrefix r;  antisym r |]
          ==> (ys,xs) : genPrefix r --> xs = ys"
    apply (erule genPrefix.induct)
      txt{*Base case*}
      apply blast
     txt{*prepend case*}
     apply (simp add: antisym_def)
    txt{*append case is the hardest*}
    apply clarify
    apply (subgoal_tac "length zs = 0", force)
    apply (drule genPrefix_length_le)+
    apply (simp del: length_0_conv)
    done

    lemma antisym_genPrefix: "antisym r ==> antisym (genPrefix r)"
    by (blast intro: antisymI genPrefix_antisym)

    subsection{*recursion equations*}

    lemma genPrefix_Nil [simp]: "((xs, []) : genPrefix r) = (xs = [])"
    apply (induct_tac "xs")
    prefer 2 apply blast
    apply simp
    done

    lemma same_genPrefix_genPrefix [simp]:
        "reflexive r ==> ((xs@ys, xs@zs) : genPrefix r) = ((ys,zs) : genPrefix r)"
    apply (unfold refl_def)
    apply (induct_tac "xs")
    apply (simp_all (no_asm_simp))
    done

    lemma genPrefix_Cons:
         "((xs, y#ys) : genPrefix r) =
          (xs=[] | (EX z zs. xs=z#zs & (z,y) : r & (zs,ys) : genPrefix r))"
    by (case_tac "xs", auto)

    lemma genPrefix_take_append:
         "[| reflexive r;  (xs,ys) : genPrefix r |]
          ==>  (xs@zs, take (length xs) ys @ zs) : genPrefix r"
    apply (erule genPrefix.induct)
    apply (frule_tac [3] genPrefix_length_le)
    apply (simp_all (no_asm_simp) add: diff_is_0_eq [THEN iffD2])
    done

    lemma genPrefix_append_both:
         "[| reflexive r;  (xs,ys) : genPrefix r;  length xs = length ys |]
          ==>  (xs@zs, ys @ zs) : genPrefix r"
    apply (drule genPrefix_take_append, assumption)
    apply (simp add: take_all)
    done

    (*NOT suitable for rewriting since [y] has the form y#ys*)
    lemma append_cons_eq: "xs @ y # ys = (xs @ [y]) @ ys"
    by auto

    lemma aolemma:
         "[| (xs,ys) : genPrefix r;  reflexive r |]
          ==> length xs < length ys --> (xs @ [ys ! length xs], ys) : genPrefix r"
    apply (erule genPrefix.induct)
      apply blast
     apply simp
    txt{*Append case is hardest*}
    apply simp
    apply (frule genPrefix_length_le [THEN le_imp_less_or_eq])
    apply (erule disjE)
    apply (simp_all (no_asm_simp) add: neq_Nil_conv nth_append)
    apply (blast intro: genPrefix.append, auto)
    apply (subst append_cons_eq, fast intro: genPrefix_append_both genPrefix.append)
    done

    lemma append_one_genPrefix:
         "[| (xs,ys) : genPrefix r;  length xs < length ys;  reflexive r |]
          ==> (xs @ [ys ! length xs], ys) : genPrefix r"
    by (blast intro: aolemma [THEN mp])

    (** Proving the equivalence with Charpentier's definition **)

    lemma genPrefix_imp_nth [rule_format]:
         "ALL i ys. i < length xs
                    --> (xs, ys) : genPrefix r --> (xs ! i, ys ! i) : r"
    apply (induct_tac "xs", auto)
    apply (case_tac "i", auto)
    done

    lemma nth_imp_genPrefix [rule_format]:
         "ALL ys. length xs <= length ys
          --> (ALL i. i < length xs --> (xs ! i, ys ! i) : r)
          --> (xs, ys) : genPrefix r"
    apply (induct_tac "xs")
    apply (simp_all (no_asm_simp) add: less_Suc_eq_0_disj all_conj_distrib)
    apply clarify
    apply (case_tac "ys")
    apply (force+)
    done

    lemma genPrefix_iff_nth:
         "((xs,ys) : genPrefix r) =
          (length xs <= length ys & (ALL i. i < length xs --> (xs!i, ys!i) : r))"
    apply (blast intro: genPrefix_length_le genPrefix_imp_nth nth_imp_genPrefix)
    done

    subsection{*The type of lists is partially ordered*}

    declare reflexive_Id [iff]
            antisym_Id [iff]
            trans_Id [iff]

    lemma prefix_refl [iff]: "xs <= (xs::'a list)"
    by (simp add: prefix_def)

    lemma prefix_trans: "!!xs::'a list. [| xs <= ys; ys <= zs |] ==> xs <= zs"
    apply (unfold prefix_def)
    apply (blast intro: genPrefix_trans)
    done

    lemma prefix_antisym: "!!xs::'a list. [| xs <= ys; ys <= xs |] ==> xs = ys"
    apply (unfold prefix_def)
    apply (blast intro: genPrefix_antisym)
    done

    lemma prefix_less_le: "!!xs::'a list. (xs < zs) = (xs <= zs & xs ~= zs)"
    by (unfold strict_prefix_def, auto)

    instance list :: (type) order
      by (intro_classes,
          (assumption | rule prefix_refl prefix_trans prefix_antisym
                         prefix_less_le)+)

    (*Monotonicity of "set" operator WRT prefix*)
    lemma set_mono: "xs <= ys ==> set xs <= set ys"
    apply (unfold prefix_def)
    apply (erule genPrefix.induct, auto)
    done

    (** recursion equations **)

    lemma Nil_prefix [iff]: "[] <= xs"
    apply (unfold prefix_def)
    apply (simp add: Nil_genPrefix)
    done

    lemma prefix_Nil [simp]: "(xs <= []) = (xs = [])"
    apply (unfold prefix_def)
    apply (simp add: genPrefix_Nil)
    done

    lemma Cons_prefix_Cons [simp]: "(x#xs <= y#ys) = (x=y & xs<=ys)"
    by (simp add: prefix_def)

    lemma same_prefix_prefix [simp]: "(xs@ys <= xs@zs) = (ys <= zs)"
    by (simp add: prefix_def)

    lemma append_prefix [iff]: "(xs@ys <= xs) = (ys <= [])"
    by (insert same_prefix_prefix [of xs ys "[]"], simp)

    lemma prefix_appendI [simp]: "xs <= ys ==> xs <= ys@zs"
    apply (unfold prefix_def)
    apply (erule genPrefix.append)
    done

    lemma prefix_Cons:
       "(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))"
    by (simp add: prefix_def genPrefix_Cons)

    lemma append_one_prefix:
      "[| xs <= ys; length xs < length ys |] ==> xs @ [ys ! length xs] <= ys"
    apply (unfold prefix_def)
    apply (simp add: append_one_genPrefix)
    done

    lemma prefix_length_le: "xs <= ys ==> length xs <= length ys"
    apply (unfold prefix_def)
    apply (erule genPrefix_length_le)
    done

    lemma splemma: "xs<=ys ==> xs~=ys --> length xs < length ys"
    apply (unfold prefix_def)
    apply (erule genPrefix.induct, auto)
    done

    lemma strict_prefix_length_less: "xs < ys ==> length xs < length ys"
    apply (unfold strict_prefix_def)
    apply (blast intro: splemma [THEN mp])
    done

    lemma mono_length: "mono length"
    by (blast intro: monoI prefix_length_le)

    (*Equivalence to the definition used in Lex/Prefix.thy*)
    lemma prefix_iff: "(xs <= zs) = (EX ys. zs = xs@ys)"
    apply (unfold prefix_def)
    apply (auto simp add: genPrefix_iff_nth nth_append)
    apply (rule_tac x = "drop (length xs) zs" in exI)
    apply (rule nth_equalityI)
    apply (simp_all (no_asm_simp) add: nth_append)
    done

    lemma prefix_snoc [simp]: "(xs <= ys@[y]) = (xs = ys@[y] | xs <= ys)"
    apply (simp add: prefix_iff)
    apply (rule iffI)
     apply (erule exE)
     apply (rename_tac "zs")
     apply (rule_tac xs = zs in rev_exhaust)
      apply simp
     apply clarify
     apply (simp del: append_assoc add: append_assoc [symmetric], force)
    done

    lemma prefix_append_iff:
         "(xs <= ys@zs) = (xs <= ys | (? us. xs = ys@us & us <= zs))"
    apply (rule_tac xs = zs in rev_induct)
     apply force
    apply (simp del: append_assoc add: append_assoc [symmetric], force)
    done

    (*Although the prefix ordering is not linear, the prefixes of a list
      are linearly ordered.*)
    lemma common_prefix_linear [rule_format]:
         "!!zs::'a list. xs <= zs --> ys <= zs --> xs <= ys | ys <= xs"
    by (rule_tac xs = zs in rev_induct, auto)

    subsection{*pfixLe, pfixGe: properties inherited from the translations*}

    (** pfixLe **)

    lemma reflexive_Le [iff]: "reflexive Le"
    by (unfold refl_def Le_def, auto)

    lemma antisym_Le [iff]: "antisym Le"
    by (unfold antisym_def Le_def, auto)

    lemma trans_Le [iff]: "trans Le"
    by (unfold trans_def Le_def, auto)

    lemma pfixLe_refl [iff]: "x pfixLe x"
    by simp

    lemma pfixLe_trans: "[| x pfixLe y; y pfixLe z |] ==> x pfixLe z"
    by (blast intro: genPrefix_trans)

    lemma pfixLe_antisym: "[| x pfixLe y; y pfixLe x |] ==> x = y"
    by (blast intro: genPrefix_antisym)

    lemma prefix_imp_pfixLe: "xs<=ys ==> xs pfixLe ys"
    apply (unfold prefix_def Le_def)
    apply (blast intro: genPrefix_mono [THEN [2] rev_subsetD])
    done

    lemma reflexive_Ge [iff]: "reflexive Ge"
    by (unfold refl_def Ge_def, auto)

    lemma antisym_Ge [iff]: "antisym Ge"
    by (unfold antisym_def Ge_def, auto)

    lemma trans_Ge [iff]: "trans Ge"
    by (unfold trans_def Ge_def, auto)

    lemma pfixGe_refl [iff]: "x pfixGe x"
    by simp

    lemma pfixGe_trans: "[| x pfixGe y; y pfixGe z |] ==> x pfixGe z"
    by (blast intro: genPrefix_trans)

    lemma pfixGe_antisym: "[| x pfixGe y; y pfixGe x |] ==> x = y"
    by (blast intro: genPrefix_antisym)

    lemma prefix_imp_pfixGe: "xs<=ys ==> xs pfixGe ys"
    apply (unfold prefix_def Ge_def)
    apply (blast intro: genPrefix_mono [THEN [2] rev_subsetD])
    done

    end

### preliminary lemmas

lemma Nil_genPrefix:

      ([], xs) ∈ genPrefix r

lemma genPrefix_length_le:

      (xs, ys) ∈ genPrefix r ==> length xs ≤ length ys

lemma cdlemma:

      (xs', ys') ∈ genPrefix r
      ==> ∀x xs. xs' = x # xs -->
                 (∃y ys. ys' = y # ys ∧ (x, y) ∈ r ∧ (xs, ys) ∈ genPrefix r)

lemma cons_genPrefixE:

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

lemma Cons_genPrefix_Cons:

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

### genPrefix is a partial order

lemma refl_genPrefix:

      reflexive r ==> reflexive (genPrefix r)

lemma genPrefix_refl:

      reflexive r ==> (l, l) ∈ genPrefix r

lemma genPrefix_mono:

      r ⊆ s ==> genPrefix r ⊆ genPrefix s

lemma append_genPrefix:

      (xs @ ys, zs) ∈ genPrefix r ==> (xs, zs) ∈ genPrefix r

lemma genPrefix_trans_O:

      [| (x, y) ∈ genPrefix r; (y, z) ∈ genPrefix s |] ==> (x, z) ∈ genPrefix (s O r)

lemma genPrefix_trans:

      [| (x, y) ∈ genPrefix r; (y, z) ∈ genPrefix r; trans r |]
      ==> (x, z) ∈ genPrefix r

lemma prefix_genPrefix_trans:

      [| x ≤ y; (y, z) ∈ genPrefix r |] ==> (x, z) ∈ genPrefix r

lemma genPrefix_prefix_trans:

      [| (x, y) ∈ genPrefix r; y ≤ z |] ==> (x, z) ∈ genPrefix r

lemma trans_genPrefix:

      trans r ==> trans (genPrefix r)

lemma genPrefix_antisym:

      [| (xs, ys) ∈ genPrefix r; antisym r; (ys, xs) ∈ genPrefix r |] ==> xs = ys

lemma antisym_genPrefix:

      antisym r ==> antisym (genPrefix r)

### recursion equations

lemma genPrefix_Nil:

      ((xs, []) ∈ genPrefix r) = (xs = [])

lemma same_genPrefix_genPrefix:

      reflexive r ==> ((xs @ ys, xs @ zs) ∈ genPrefix r) = ((ys, zs) ∈ genPrefix r)

lemma genPrefix_Cons:

      ((xs, y # ys) ∈ genPrefix r) =
      (xs = [] ∨ (∃z zs. xs = z # zs ∧ (z, y) ∈ r ∧ (zs, ys) ∈ genPrefix r))

lemma genPrefix_take_append:

      [| reflexive r; (xs, ys) ∈ genPrefix r |]
      ==> (xs @ zs, take (length xs) ys @ zs) ∈ genPrefix r

lemma genPrefix_append_both:

      [| reflexive r; (xs, ys) ∈ genPrefix r; length xs = length ys |]
      ==> (xs @ zs, ys @ zs) ∈ genPrefix r

lemma append_cons_eq:

      xs @ y # ys = (xs @ [y]) @ ys

lemma aolemma:

      [| (xs, ys) ∈ genPrefix r; reflexive r |]
      ==> length xs < length ys --> (xs @ [ys ! length xs], ys) ∈ genPrefix r

lemma append_one_genPrefix:

      [| (xs, ys) ∈ genPrefix r; length xs < length ys; reflexive r |]
      ==> (xs @ [ys ! length xs], ys) ∈ genPrefix r

lemma genPrefix_imp_nth:

      [| i < length xs; (xs, ys) ∈ genPrefix r |] ==> (xs ! i, ys ! i) ∈ r

lemma nth_imp_genPrefix:

      [| length xs ≤ length ys; !!i. i < length xs ==> (xs ! i, ys ! i) ∈ r |]
      ==> (xs, ys) ∈ genPrefix r

lemma genPrefix_iff_nth:

      ((xs, ys) ∈ genPrefix r) =
      (length xs ≤ length ys ∧ (∀i<length xs. (xs ! i, ys ! i) ∈ r))

### The type of lists is partially ordered

lemma prefix_refl:

      xs ≤ xs

lemma prefix_trans:

      [| xs ≤ ys; ys ≤ zs |] ==> xs ≤ zs

lemma prefix_antisym:

      [| xs ≤ ys; ys ≤ xs |] ==> xs = ys

lemma prefix_less_le:

      (xs < zs) = (xs ≤ zs ∧ xs ≠ zs)

lemma set_mono:

      xs ≤ ys ==> set xs ⊆ set ys

lemma Nil_prefix:

      [] ≤ xs

lemma prefix_Nil:

      (xs ≤ []) = (xs = [])

lemma Cons_prefix_Cons:

      (x # xs ≤ y # ys) = (x = y ∧ xs ≤ ys)

lemma same_prefix_prefix:

      (xs @ ys ≤ xs @ zs) = (ys ≤ zs)

lemma append_prefix:

      (xs @ ys ≤ xs) = (ys ≤ [])

lemma prefix_appendI:

      xs ≤ ys ==> xs ≤ ys @ zs

lemma prefix_Cons:

      (xs ≤ y # ys) = (xs = [] ∨ (∃zs. xs = y # zs ∧ zs ≤ ys))

lemma append_one_prefix:

      [| xs ≤ ys; length xs < length ys |] ==> xs @ [ys ! length xs] ≤ ys

lemma prefix_length_le:

      xs ≤ ys ==> length xs ≤ length ys

lemma splemma:

      xs ≤ ys ==> xs ≠ ys --> length xs < length ys

lemma strict_prefix_length_less:

      xs < ys ==> length xs < length ys

lemma mono_length:

      mono size

lemma prefix_iff:

      (xs ≤ zs) = (∃ys. zs = xs @ ys)

lemma prefix_snoc:

      (xs ≤ ys @ [y]) = (xs = ys @ [y] ∨ xs ≤ ys)

lemma prefix_append_iff:

      (xs ≤ ys @ zs) = (xs ≤ ys ∨ (∃us. xs = ys @ us ∧ us ≤ zs))

lemma common_prefix_linear:

      [| xs ≤ zs; ys ≤ zs |] ==> xs ≤ ys ∨ ys ≤ xs

### pfixLe, pfixGe: properties inherited from the translations

lemma reflexive_Le:

      reflexive Le

lemma antisym_Le:

      antisym Le

lemma trans_Le:

      trans Le

lemma pfixLe_refl:

      x pfixLe x

lemma pfixLe_trans:

      [| x pfixLe y; y pfixLe z |] ==> x pfixLe z

lemma pfixLe_antisym:

      [| x pfixLe y; y pfixLe x |] ==> x = y

lemma prefix_imp_pfixLe:

      xs ≤ ys ==> xs pfixLe ys

lemma reflexive_Ge:

      reflexive Ge

lemma antisym_Ge:

      antisym Ge

lemma trans_Ge:

      trans Ge

lemma pfixGe_refl:

      x pfixGe x

lemma pfixGe_trans:

      [| x pfixGe y; y pfixGe z |] ==> x pfixGe z

lemma pfixGe_antisym:

      [| x pfixGe y; y pfixGe x |] ==> x = y

lemma prefix_imp_pfixGe:

      xs ≤ ys ==> xs pfixGe ys