# Theory ListOrder

theory ListOrder
imports Main
```(*  Title:      HOL/UNITY/ListOrder.thy
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

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!
*)

section ‹The Prefix Ordering on Lists›

theory ListOrder
imports Main
begin

inductive_set
genPrefix :: "('a * 'a)set => ('a list * 'a list)set"
for r :: "('a * 'a)set"
where
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)"

instantiation list :: (type) ord
begin

definition
prefix_def:        "xs <= zs ⟷  (xs, zs) ∈ genPrefix Id"

definition
strict_prefix_def: "xs < zs  ⟷  xs ≤ zs ∧ ¬ zs ≤ (xs :: 'a list)"

instance ..

(*Constants for the <= and >= relations, used below in translations*)

end

definition Le :: "(nat*nat) set" where
"Le == {(x,y). x <= y}"

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

abbreviation
pfixLe :: "[nat list, nat list] => bool"  (infixl "pfixLe" 50)  where
"xs pfixLe ys == (xs,ys) ∈ genPrefix Le"

abbreviation
pfixGe :: "[nat list, nat list] => bool"  (infixl "pfixGe" 50)  where
"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 |]
==> (∀x xs. xs' = x#xs ⟶ (∃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: "refl r ==> refl (genPrefix r)"
apply (unfold refl_on_def, auto)
apply (induct_tac "x")
prefer 2 apply (blast intro: genPrefix.prepend)
apply (blast intro: genPrefix.Nil)
done

lemma genPrefix_refl [simp]: "refl r ⟹ (l,l) ∈ genPrefix r"
by (erule refl_onD [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:
"(xs @ ys, zs) ∈ genPrefix r ⟹ (xs, zs) ∈ genPrefix r"
by (induct xs arbitrary: zs) auto

(*Lemma proving transitivity and more*)
lemma genPrefix_trans_O:
assumes "(x, y) ∈ genPrefix r"
shows "⋀z. (y, z) ∈ genPrefix s ⟹ (x, z) ∈ genPrefix (r O s)"
apply (atomize (full))
using assms
apply induct
apply blast
apply (blast intro: genPrefix.prepend)
apply (blast dest: append_genPrefix)
done

lemma genPrefix_trans:
"(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:
"[| x<=y;  (y,z) ∈ genPrefix r |] ==> (x, z) ∈ genPrefix r"
apply (unfold prefix_def)
apply (drule genPrefix_trans_O, assumption)
apply simp
done

lemma genPrefix_prefix_trans:
"[| (x,y) ∈ genPrefix r;  y<=z |] ==> (x,z) ∈ genPrefix r"
apply (unfold prefix_def)
apply (drule genPrefix_trans_O, assumption)
apply simp
done

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

(** Antisymmetry **)

lemma genPrefix_antisym:
assumes 1: "(xs, ys) ∈ genPrefix r"
and 2: "antisym r"
and 3: "(ys, xs) ∈ genPrefix r"
shows "xs = ys"
using 1 3
proof induct
case Nil
then show ?case by blast
next
case prepend
then show ?case using 2 by (simp add: antisym_def)
next
case (append xs ys zs)
then show ?case
apply -
apply (subgoal_tac "length zs = 0", force)
apply (drule genPrefix_length_le)+
apply (simp del: length_0_conv)
done
qed

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 = [])"
by (induct xs) auto

lemma same_genPrefix_genPrefix [simp]:
"refl r ⟹ ((xs@ys, xs@zs) ∈ genPrefix r) = ((ys,zs) ∈ genPrefix r)"
by (induct xs) (simp_all add: refl_on_def)

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

lemma genPrefix_take_append:
"[| refl 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:
"[| refl r;  (xs,ys) ∈ genPrefix r;  length xs = length ys |]
==>  (xs@zs, ys @ zs) ∈ genPrefix r"
apply (drule genPrefix_take_append, assumption)
apply simp
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;  refl 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;  refl 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:
"i < length xs ⟹ (xs, ys) ∈ genPrefix r ⟹ (xs ! i, ys ! i) ∈ r"
apply (induct xs arbitrary: i ys)
apply auto
apply (case_tac i)
apply auto
done

lemma nth_imp_genPrefix:
"length xs <= length ys ⟹
(∀i. i < length xs ⟶ (xs ! i, ys ! i) ∈ r) ⟹
(xs, ys) ∈ genPrefix r"
apply (induct xs arbitrary: ys)
apply (case_tac ys)
apply (force+)
done

lemma genPrefix_iff_nth:
"((xs,ys) ∈ genPrefix r) =
(length xs <= length ys & (∀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 refl_Id [iff]
antisym_Id [iff]
trans_Id [iff]

lemma prefix_refl [iff]: "xs <= (xs::'a list)"

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_not_le: "!!xs::'a list. (xs < zs) = (xs <= zs & ¬ zs ≤ xs)"
by (unfold strict_prefix_def, auto)

instance list :: (type) order
by (intro_classes,
(assumption | rule prefix_refl prefix_trans prefix_antisym
prefix_less_le_not_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"

lemma prefix_Nil [simp]: "(xs <= []) = (xs = [])"

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

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

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))"

lemma append_one_prefix:
"[| xs <= ys; length xs < length ys |] ==> xs @ [ys ! length xs] <= ys"
apply (unfold prefix_def)
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) = (∃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)
done

lemma prefix_snoc [simp]: "(xs <= ys@[y]) = (xs = ys@[y] | xs <= ys)"
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:
fixes xs ys zs :: "'a list"
shows "xs <= zs ⟹ ys <= zs ⟹ xs <= ys | ys <= xs"
by (induct zs rule: rev_induct) auto

subsection‹pfixLe, pfixGe: properties inherited from the translations›

(** pfixLe **)

lemma refl_Le [iff]: "refl Le"
by (unfold refl_on_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 refl_Ge [iff]: "refl Ge"
by (unfold refl_on_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
```