Theory List_Order

(*
Author:  Christian Sternagel <c.sternagel@gmail.com> (2011-2015)
Author:  René Thiemann <rene.thiemann@uibk.ac.at> (2011-2015)
License: LGPL (see file COPYING.LESSER)
*)
theory List_Order
imports
  Knuth_Bendix_Order.Order_Pair
begin

type_synonym 'a list_ext = "'a rel ⇒ 'a rel ⇒ 'a list rel"

locale list_order_extension =
  fixes s_list :: "'a list_ext"
   and ns_list :: "'a list_ext"
  assumes extension: "SN_order_pair S NS ⟹ SN_order_pair (s_list S NS) (ns_list S NS)"
     and s_map: "⟦⋀ a b. (a,b) ∈ S ⟹ (f a,f b) ∈ S; ⋀ a b. (a,b) ∈ NS ⟹ (f a,f b) ∈ NS⟧ ⟹ (as,bs) ∈ s_list S NS ⟹ (map f as, map f bs) ∈ s_list S NS" 
     and ns_map: "⟦⋀ a b. (a,b) ∈ S ⟹ (f a,f b) ∈ S; ⋀ a b. (a,b) ∈ NS ⟹ (f a,f b) ∈ NS⟧ ⟹ (as,bs) ∈ ns_list S NS ⟹ (map f as, map f bs) ∈ ns_list S NS" 
     and all_ns_imp_ns: "length as = length bs ⟹ ⟦⋀ i. i < length bs ⟹  (as ! i, bs ! i) ∈ NS⟧ ⟹ (as,bs) ∈ ns_list S NS"

end