theory Quasi_Order
imports Main
begin
locale quasi_order =
fixes qle :: "'a => 'a => bool" (infix "\<preceq>" 60)
assumes qle_refl[iff]: "x \<preceq> x"
and qle_trans: "x \<preceq> y ==> y \<preceq> z ==> x \<preceq> z"
begin
definition in_qle :: "'a => 'a set => bool" (infix "∈⇣\<preceq>" 60) where
"x ∈⇣\<preceq> M ≡ ∃y ∈ M. x \<preceq> y"
definition subseteq_qle :: "'a set => 'a set => bool" (infix "⊆⇣\<preceq>" 60) where
"M ⊆⇣\<preceq> N ≡ ∀x ∈ M. x ∈⇣\<preceq> N"
definition seteq_qle :: "'a set => 'a set => bool" (infix "=⇣\<preceq>" 60) where
"M =⇣\<preceq> N ≡ M ⊆⇣\<preceq> N ∧ N ⊆⇣\<preceq> M"
lemmas "defs" = in_qle_def subseteq_qle_def seteq_qle_def
lemma subseteq_qle_refl[simp]: "M ⊆⇣\<preceq> M"
by(auto simp add: subseteq_qle_def in_qle_def)
lemma subseteq_qle_trans: "A ⊆⇣\<preceq> B ==> B ⊆⇣\<preceq> C ==> A ⊆⇣\<preceq> C"
by (simp add: subseteq_qle_def in_qle_def) (metis qle_trans)
lemma empty_subseteq_qle[simp]: "{} ⊆⇣\<preceq> A"
by (simp add: subseteq_qle_def)
lemma subseteq_qleI2: "(!!x. x ∈ M ==> EX y : N. x \<preceq> y) ==> M ⊆⇣\<preceq> N"
by (auto simp add: subseteq_qle_def in_qle_def)
lemma subseteq_qleD2: "M ⊆⇣\<preceq> N ==> x ∈ M ==> EX y : N. x \<preceq> y"
by (auto simp add: subseteq_qle_def in_qle_def)
lemma seteq_qle_refl[iff]: "A =⇣\<preceq> A"
by (simp add: seteq_qle_def)
lemma seteq_qle_trans: "A =⇣\<preceq> B ==> B =⇣\<preceq> C ==> A =⇣\<preceq> C"
by (simp add: seteq_qle_def) (metis subseteq_qle_trans)
end
end