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