Theory Min_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 Min_Set_Order_Impl
imports
  List_Order_Impl
  Min_Set_Order
begin

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

lemma min_set_ext_list_ext:
  "∃ s ns. list_order_extension_impl s ns min_set_ext"
proof(intro exI)
  interpret list_order_extension min_set_s_order min_set_ns_order by (rule min_set_order)
  show "list_order_extension_impl min_set_s_order min_set_ns_order min_set_ext"
    by (unfold_locales, (force simp: min_set_ext_def min_set_s_order_def min_set_ns_order_def)+)
qed

end