Theory List_Order

subsection ‹Interface for extending an order pair on lists›

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"

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