Theory List_Lexord_Alt

(******************************************************************************)
(* Project: Isabelle/UTP Toolkit                                              *)
(* File: List_Lexord_Alt.thy                                                  *)
(* Authors: Simon Foster and Frank Zeyda                                      *)
(* Emails: simon.foster@york.ac.uk and frank.zeyda@york.ac.uk                 *)
(******************************************************************************)

section ‹Alternative List Lexicographic Order›

theory List_Lexord_Alt
  imports Main
begin

text ‹ Since we can't instantiate the order class twice for lists, and we want prefix as
  the default order for the UTP we here add syntax for the lexicographic order relation. ›

definition list_lex_less :: "'a::linorder list ⇒ 'a list ⇒ bool" (infix "<⇩l" 50)
where "xs <⇩l ys ⟷ (xs, ys) ∈ lexord {(u, v). u < v}"

lemma list_lex_less_neq [simp]: "x <⇩l y ⟹ x ≠ y"
  apply (simp add: list_lex_less_def)
  apply (meson case_prodD less_irrefl lexord_irreflexive mem_Collect_eq)
done

lemma not_less_Nil [simp]: "¬ x <⇩l []"
  by (simp add: list_lex_less_def)

lemma Nil_less_Cons [simp]: "[] <⇩l a # x"
  by (simp add: list_lex_less_def)

lemma Cons_less_Cons [simp]: "a # x <⇩l b # y ⟷ a < b ∨ a = b ∧ x <⇩l y"
  by (simp add: list_lex_less_def)
end