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