Theory List_Order_Impl

(*
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_Impl
imports 
  QTRS.List_Order
begin

type_synonym 'a list_ext_impl = "('a ⇒ 'a ⇒ bool × bool) ⇒ 'a list ⇒ 'a list ⇒ bool × bool"

locale list_order_extension_impl = list_order_extension s_list ns_list for
  s_list ns_list :: "'a list_ext" +
  fixes list_ext :: "'a list_ext_impl"
  assumes list_ext_s: "⋀ s ns. s_list {(a,b). s a b} {(a,b). ns a b} = {(as,bs). fst (list_ext (λ a b. (s a b, ns a b)) as bs)}"
     and  list_ext_ns: "⋀ s ns. ns_list {(a,b). s a b} {(a,b). ns a b} = {(as,bs). snd (list_ext (λ a b. (s a b, ns a b)) as bs)}"
    and s_ext_local_mono: "⋀ s ns s' ns' as bs. (set as × set bs) ∩ ns ⊆ ns' ⟹ (set as × set bs) ∩ s ⊆ s' ⟹ (as,bs) ∈ s_list ns s ⟹ (as,bs) ∈ s_list ns' s'"
    and ns_ext_local_mono: "⋀ s ns s' ns' as bs. (set as × set bs) ∩ ns ⊆ ns' ⟹ (set as × set bs) ∩ s ⊆ s' ⟹ (as,bs) ∈ ns_list ns s ⟹ (as,bs) ∈ ns_list ns' s'"

end