Theory Set_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 Set_Order_Impl
imports 
  Set_Order
  List_Order_Impl
begin

definition set_ext :: "'a list_ext_impl" where "set_ext s_ns ≡ λ as bs. 
  (as ≠ [] ∧ (∀ b ∈ set bs. ∃ a ∈ set as. fst (s_ns a b)),  
  (∀ b ∈ set bs. ∃ a ∈ set as. snd (s_ns a b)))"


lemma set_ext_list_ext: "∃ s ns. list_order_extension_impl s ns set_ext"
proof(intro exI)
  let ?s = "set_s_order"
  let ?ns = "set_ns_order"
  show "list_order_extension_impl ?s ?ns set_ext"
  proof
    fix s ns
    show "?s {(a,b). s a b} {(a,b). ns a b} = {(as,bs). fst (set_ext (λ a b. (s a b, ns a b)) as bs)}" unfolding set_ext_def set_s_order_def by auto
  next
    fix s ns
    show "?ns {(a,b). s a b} {(a,b). ns a b} = {(as,bs). snd (set_ext (λ a b. (s a b, ns a b)) as bs)}" unfolding set_ext_def set_ns_order_def by auto
  next
    fix s ns s' ns' as bs
    assume "set as × set bs ∩ ns ⊆ ns'"
           "set as × set bs ∩ s ⊆ s'"
           "(as,bs) ∈ ?s s ns"
    thus "(as,bs) ∈ ?s s' ns'" unfolding set_s_order_def by blast
  next
    fix s ns s' ns' as bs
    assume "set as × set bs ∩ ns ⊆ ns'"
           "set as × set bs ∩ s ⊆ s'"
           "(as,bs) ∈ ?ns s ns"
    thus "(as,bs) ∈ ?ns s' ns'" unfolding set_ns_order_def by blast
  qed
qed

end