Theory Quasi_Order

theory Quasi_Order
imports Main
begin

locale quasi_order =
fixes qle :: "'a ⇒ 'a ⇒ bool" (infix ‹≼› 60)
assumes qle_refl[iff]: "x ≼ x"
and qle_trans: "x ≼ y ⟹ y ≼ z ⟹ x ≼ z"
begin

definition in_qle :: "'a ⇒ 'a set ⇒ bool"  (infix ‹∈⇩≼› 60) where
 "x ∈⇩≼ M ≡ ∃y ∈ M. x ≼ y"

definition subseteq_qle :: "'a set ⇒ 'a set ⇒ bool" (infix ‹⊆⇩≼› 60) where
 "M ⊆⇩≼ N ≡ ∀x ∈ M. x ∈⇩≼ N"

definition seteq_qle :: "'a set ⇒ 'a set ⇒ bool" (infix ‹=⇩≼› 60) where
 "M =⇩≼ N  ≡  M ⊆⇩≼ N ∧ N ⊆⇩≼ M"

lemmas "defs" = in_qle_def subseteq_qle_def seteq_qle_def

lemma subseteq_qle_refl[simp]: "M ⊆⇩≼ M"
by(auto simp add: subseteq_qle_def in_qle_def)

lemma subseteq_qle_trans: "A ⊆⇩≼ B ⟹ B ⊆⇩≼ C ⟹ A ⊆⇩≼ C"
by (simp add: subseteq_qle_def in_qle_def) (metis qle_trans)

lemma empty_subseteq_qle[simp]: "{} ⊆⇩≼ A"
by (simp add: subseteq_qle_def)

lemma subseteq_qleI2: "(⋀x. x ∈ M ⟹ ∃y ∈ N. x ≼ y) ⟹ M ⊆⇩≼ N"
by (auto simp add: subseteq_qle_def in_qle_def)

lemma subseteq_qleD2: "M ⊆⇩≼ N ⟹ x ∈ M ⟹ ∃y ∈ N. x ≼ y"
by (auto simp add: subseteq_qle_def in_qle_def)

lemma seteq_qle_refl[iff]: "A =⇩≼ A"
by (simp add: seteq_qle_def)

lemma seteq_qle_trans: "A =⇩≼ B ⟹ B =⇩≼ C ⟹ A =⇩≼ C"
by (simp add: seteq_qle_def) (metis subseteq_qle_trans)

end

end