(* Author: Florian Haftmann, TU Muenchen *)
header {* A dedicated set type which is executable on its finite part *}
theory Cset
imports More_Set More_List
begin
subsection {* Lifting *}
typedef (open) 'a set = "UNIV :: 'a set set"
morphisms member Set by rule+
hide_type (open) set
lemma member_Set [simp]:
"member (Set A) = A"
by (rule Set_inverse) rule
lemma Set_member [simp]:
"Set (member A) = A"
by (fact member_inverse)
lemma Set_inject [simp]:
"Set A = Set B \<longleftrightarrow> A = B"
by (simp add: Set_inject)
lemma set_eq_iff:
"A = B \<longleftrightarrow> member A = member B"
by (simp add: member_inject)
hide_fact (open) set_eq_iff
lemma set_eqI:
"member A = member B \<Longrightarrow> A = B"
by (simp add: Cset.set_eq_iff)
hide_fact (open) set_eqI
subsection {* Lattice instantiation *}
instantiation Cset.set :: (type) boolean_algebra
begin
definition less_eq_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
[simp]: "A \<le> B \<longleftrightarrow> member A \<subseteq> member B"
definition less_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
[simp]: "A < B \<longleftrightarrow> member A \<subset> member B"
definition inf_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
[simp]: "inf A B = Set (member A \<inter> member B)"
definition sup_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
[simp]: "sup A B = Set (member A \<union> member B)"
definition bot_set :: "'a Cset.set" where
[simp]: "bot = Set {}"
definition top_set :: "'a Cset.set" where
[simp]: "top = Set UNIV"
definition uminus_set :: "'a Cset.set \<Rightarrow> 'a Cset.set" where
[simp]: "- A = Set (- (member A))"
definition minus_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
[simp]: "A - B = Set (member A - member B)"
instance proof
qed (auto intro: Cset.set_eqI)
end
instantiation Cset.set :: (type) complete_lattice
begin
definition Inf_set :: "'a Cset.set set \<Rightarrow> 'a Cset.set" where
[simp]: "Inf_set As = Set (Inf (image member As))"
definition Sup_set :: "'a Cset.set set \<Rightarrow> 'a Cset.set" where
[simp]: "Sup_set As = Set (Sup (image member As))"
instance proof
qed (auto simp add: le_fun_def le_bool_def)
end
subsection {* Basic operations *}
definition is_empty :: "'a Cset.set \<Rightarrow> bool" where
[simp]: "is_empty A \<longleftrightarrow> More_Set.is_empty (member A)"
definition insert :: "'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
[simp]: "insert x A = Set (Set.insert x (member A))"
definition remove :: "'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
[simp]: "remove x A = Set (More_Set.remove x (member A))"
definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a Cset.set \<Rightarrow> 'b Cset.set" where
[simp]: "map f A = Set (image f (member A))"
enriched_type map: map
by (simp_all add: fun_eq_iff image_compose)
definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
[simp]: "filter P A = Set (More_Set.project P (member A))"
definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
[simp]: "forall P A \<longleftrightarrow> Ball (member A) P"
definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
[simp]: "exists P A \<longleftrightarrow> Bex (member A) P"
definition card :: "'a Cset.set \<Rightarrow> nat" where
[simp]: "card A = Finite_Set.card (member A)"
context complete_lattice
begin
definition Infimum :: "'a Cset.set \<Rightarrow> 'a" where
[simp]: "Infimum A = Inf (member A)"
definition Supremum :: "'a Cset.set \<Rightarrow> 'a" where
[simp]: "Supremum A = Sup (member A)"
end
subsection {* Simplified simprules *}
lemma is_empty_simp [simp]:
"is_empty A \<longleftrightarrow> member A = {}"
by (simp add: More_Set.is_empty_def)
declare is_empty_def [simp del]
lemma remove_simp [simp]:
"remove x A = Set (member A - {x})"
by (simp add: More_Set.remove_def)
declare remove_def [simp del]
lemma filter_simp [simp]:
"filter P A = Set {x \<in> member A. P x}"
by (simp add: More_Set.project_def)
declare filter_def [simp del]
declare mem_def [simp del]
hide_const (open) is_empty insert remove map filter forall exists card
Inter Union
end