src/HOL/Library/Cset.thy
author hoelzl
Tue Jul 19 14:37:49 2011 +0200 (2011-07-19)
changeset 43922 c6f35921056e
parent 43241 93b1183e43e5
child 43971 892030194015
permissions -rw-r--r--
add nat => enat coercion
     1 
     2 (* Author: Florian Haftmann, TU Muenchen *)
     3 
     4 header {* A dedicated set type which is executable on its finite part *}
     5 
     6 theory Cset
     7 imports More_Set More_List
     8 begin
     9 
    10 subsection {* Lifting *}
    11 
    12 typedef (open) 'a set = "UNIV :: 'a set set"
    13   morphisms member Set by rule+
    14 hide_type (open) set
    15 
    16 lemma member_Set [simp]:
    17   "member (Set A) = A"
    18   by (rule Set_inverse) rule
    19 
    20 lemma Set_member [simp]:
    21   "Set (member A) = A"
    22   by (fact member_inverse)
    23 
    24 lemma Set_inject [simp]:
    25   "Set A = Set B \<longleftrightarrow> A = B"
    26   by (simp add: Set_inject)
    27 
    28 lemma set_eq_iff:
    29   "A = B \<longleftrightarrow> member A = member B"
    30   by (simp add: member_inject)
    31 hide_fact (open) set_eq_iff
    32 
    33 lemma set_eqI:
    34   "member A = member B \<Longrightarrow> A = B"
    35   by (simp add: Cset.set_eq_iff)
    36 hide_fact (open) set_eqI
    37 
    38 subsection {* Lattice instantiation *}
    39 
    40 instantiation Cset.set :: (type) boolean_algebra
    41 begin
    42 
    43 definition less_eq_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
    44   [simp]: "A \<le> B \<longleftrightarrow> member A \<subseteq> member B"
    45 
    46 definition less_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
    47   [simp]: "A < B \<longleftrightarrow> member A \<subset> member B"
    48 
    49 definition inf_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
    50   [simp]: "inf A B = Set (member A \<inter> member B)"
    51 
    52 definition sup_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
    53   [simp]: "sup A B = Set (member A \<union> member B)"
    54 
    55 definition bot_set :: "'a Cset.set" where
    56   [simp]: "bot = Set {}"
    57 
    58 definition top_set :: "'a Cset.set" where
    59   [simp]: "top = Set UNIV"
    60 
    61 definition uminus_set :: "'a Cset.set \<Rightarrow> 'a Cset.set" where
    62   [simp]: "- A = Set (- (member A))"
    63 
    64 definition minus_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
    65   [simp]: "A - B = Set (member A - member B)"
    66 
    67 instance proof
    68 qed (auto intro: Cset.set_eqI)
    69 
    70 end
    71 
    72 instantiation Cset.set :: (type) complete_lattice
    73 begin
    74 
    75 definition Inf_set :: "'a Cset.set set \<Rightarrow> 'a Cset.set" where
    76   [simp]: "Inf_set As = Set (Inf (image member As))"
    77 
    78 definition Sup_set :: "'a Cset.set set \<Rightarrow> 'a Cset.set" where
    79   [simp]: "Sup_set As = Set (Sup (image member As))"
    80 
    81 instance proof
    82 qed (auto simp add: le_fun_def le_bool_def)
    83 
    84 end
    85 
    86 
    87 subsection {* Basic operations *}
    88 
    89 definition is_empty :: "'a Cset.set \<Rightarrow> bool" where
    90   [simp]: "is_empty A \<longleftrightarrow> More_Set.is_empty (member A)"
    91 
    92 definition insert :: "'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
    93   [simp]: "insert x A = Set (Set.insert x (member A))"
    94 
    95 definition remove :: "'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
    96   [simp]: "remove x A = Set (More_Set.remove x (member A))"
    97 
    98 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a Cset.set \<Rightarrow> 'b Cset.set" where
    99   [simp]: "map f A = Set (image f (member A))"
   100 
   101 enriched_type map: map
   102   by (simp_all add: fun_eq_iff image_compose)
   103 
   104 definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
   105   [simp]: "filter P A = Set (More_Set.project P (member A))"
   106 
   107 definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
   108   [simp]: "forall P A \<longleftrightarrow> Ball (member A) P"
   109 
   110 definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
   111   [simp]: "exists P A \<longleftrightarrow> Bex (member A) P"
   112 
   113 definition card :: "'a Cset.set \<Rightarrow> nat" where
   114   [simp]: "card A = Finite_Set.card (member A)"
   115   
   116 context complete_lattice
   117 begin
   118 
   119 definition Infimum :: "'a Cset.set \<Rightarrow> 'a" where
   120   [simp]: "Infimum A = Inf (member A)"
   121 
   122 definition Supremum :: "'a Cset.set \<Rightarrow> 'a" where
   123   [simp]: "Supremum A = Sup (member A)"
   124 
   125 end
   126 
   127 
   128 subsection {* Simplified simprules *}
   129 
   130 lemma is_empty_simp [simp]:
   131   "is_empty A \<longleftrightarrow> member A = {}"
   132   by (simp add: More_Set.is_empty_def)
   133 declare is_empty_def [simp del]
   134 
   135 lemma remove_simp [simp]:
   136   "remove x A = Set (member A - {x})"
   137   by (simp add: More_Set.remove_def)
   138 declare remove_def [simp del]
   139 
   140 lemma filter_simp [simp]:
   141   "filter P A = Set {x \<in> member A. P x}"
   142   by (simp add: More_Set.project_def)
   143 declare filter_def [simp del]
   144 
   145 declare mem_def [simp del]
   146 
   147 
   148 hide_const (open) is_empty insert remove map filter forall exists card
   149   Inter Union
   150 
   151 end