theory Set_Order
imports
"../Auxiliaries/Multiset_Extension2"
QTRS.List_Order
begin
definition set_s_order :: "'a list_ext" where "set_s_order s ns ≡ {(as,bs). as ≠ [] ∧ (∀ b ∈ set bs. ∃ a ∈ set as. (a,b) ∈ s)}"
definition set_ns_order :: "'a list_ext" where "set_ns_order s ns ≡ {(as,bs). (∀ b ∈ set bs. ∃ a ∈ set as. (a,b) ∈ ns)}"
interpretation list_order_extension set_s_order set_ns_order
proof(intro list_order_extension.intro)
fix s ns
assume op: "SN_order_pair s ns"
then interpret SN_order_pair s ns .
let ?S = "set_s_order s ns"
let ?NS = "set_ns_order s ns"
note d = set_s_order_def set_ns_order_def
show "SN_order_pair ?S ?NS"
proof
show "refl ?NS" using refl_NS unfolding refl_on_def d by auto
next
show "trans ?S" using trans_S unfolding trans_def d by blast
next
show "trans ?NS" using trans_NS unfolding trans_def d by blast
next
show "?NS O ?S ⊆ ?S" using compat_NS_S_point unfolding d by force
next
show "?S O ?NS ⊆ ?S" using compat_S_NS_point unfolding d by blast
next
let ?m = mset
let ?S' = "{(as,bs). (?m as, ?m bs) ∈ s_mul_ext ns s}"
from mul_ext_list.extension[OF op]
interpret SN_order_pair ?S'
"{(as,bs). (?m as, ?m bs) ∈ ns_mul_ext ns s}" .
show "SN ?S"
proof (rule SN_subset[OF SN])
show "?S ⊆ ?S'"
proof
fix as bs
assume "(as,bs) ∈ ?S"
hence as: "as ≠ []" and bs: "⋀ b. b ∈ set bs ⟹ ∃ a ∈ set as. (a,b) ∈ s" unfolding set_s_order_def by auto
then have "(?m as, ?m bs) ∈ s_mul_ext ns s" unfolding s_mul_ext_def
by (auto intro!: mult2_alt_sI[of _ "{#}" _ _ "{#}"] simp: in_multiset_in_set Bex_def)
thus "(as,bs) ∈ ?S'" by simp
qed
qed
qed
next
fix S f NS as bs
assume "⋀ a b. (a,b) ∈ S ⟹ (f a,f b) ∈ S"
"(as,bs) ∈ set_s_order S NS"
thus "(map f as, map f bs) ∈ set_s_order S NS" unfolding set_s_order_def by force
next
fix S f NS as bs
assume "⋀ a b. (a,b) ∈ NS ⟹ (f a,f b) ∈ NS"
"(as,bs) ∈ set_ns_order S NS"
thus "(map f as, map f bs) ∈ set_ns_order S NS" unfolding set_ns_order_def by force
next
fix as bs :: "'a list" and NS S
assume "length as = length bs" "⋀ i. i < length bs ⟹ (as ! i, bs ! i) ∈ NS"
thus "(as,bs) ∈ set_ns_order S NS" unfolding set_ns_order_def set_conv_nth by force
qed
end