src/HOL/Set.thy
changeset 61955 e96292f32c3c
parent 61799 4cf66f21b764
child 62083 7582b39f51ed
     1.1 --- a/src/HOL/Set.thy	Mon Dec 28 19:23:15 2015 +0100
     1.2 +++ b/src/HOL/Set.thy	Mon Dec 28 21:47:32 2015 +0100
     1.3 @@ -12,41 +12,39 @@
     1.4  
     1.5  axiomatization Collect :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set" \<comment> "comprehension"
     1.6    and member :: "'a \<Rightarrow> 'a set \<Rightarrow> bool" \<comment> "membership"
     1.7 -where
     1.8 -  mem_Collect_eq [iff, code_unfold]: "member a (Collect P) = P a"
     1.9 +where mem_Collect_eq [iff, code_unfold]: "member a (Collect P) = P a"
    1.10    and Collect_mem_eq [simp]: "Collect (\<lambda>x. member x A) = A"
    1.11  
    1.12  notation
    1.13 +  member  ("op \<in>") and
    1.14 +  member  ("(_/ \<in> _)" [51, 51] 50)
    1.15 +
    1.16 +abbreviation not_member
    1.17 +  where "not_member x A \<equiv> \<not> (x \<in> A)" \<comment> "non-membership"
    1.18 +notation
    1.19 +  not_member  ("op \<notin>") and
    1.20 +  not_member  ("(_/ \<notin> _)" [51, 51] 50)
    1.21 +
    1.22 +notation (ASCII)
    1.23    member  ("op :") and
    1.24 -  member  ("(_/ : _)" [51, 51] 50)
    1.25 -
    1.26 -abbreviation not_member where
    1.27 -  "not_member x A \<equiv> ~ (x : A)" \<comment> "non-membership"
    1.28 -
    1.29 -notation
    1.30 +  member  ("(_/ : _)" [51, 51] 50) and
    1.31    not_member  ("op ~:") and
    1.32    not_member  ("(_/ ~: _)" [51, 51] 50)
    1.33  
    1.34 -notation (xsymbols)
    1.35 -  member      ("op \<in>") and
    1.36 -  member      ("(_/ \<in> _)" [51, 51] 50) and
    1.37 -  not_member  ("op \<notin>") and
    1.38 -  not_member  ("(_/ \<notin> _)" [51, 51] 50)
    1.39 -
    1.40  
    1.41  text \<open>Set comprehensions\<close>
    1.42  
    1.43  syntax
    1.44    "_Coll" :: "pttrn => bool => 'a set"    ("(1{_./ _})")
    1.45  translations
    1.46 -  "{x. P}" == "CONST Collect (%x. P)"
    1.47 -
    1.48 +  "{x. P}" \<rightleftharpoons> "CONST Collect (\<lambda>x. P)"
    1.49 +
    1.50 +syntax (ASCII)
    1.51 +  "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set"  ("(1{_ :/ _./ _})")
    1.52  syntax
    1.53 -  "_Collect" :: "pttrn => 'a set => bool => 'a set"    ("(1{_ :/ _./ _})")
    1.54 -syntax (xsymbols)
    1.55 -  "_Collect" :: "pttrn => 'a set => bool => 'a set"    ("(1{_ \<in>/ _./ _})")
    1.56 +  "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set"  ("(1{_ \<in>/ _./ _})")
    1.57  translations
    1.58 -  "{p:A. P}" => "CONST Collect (%p. p:A & P)"
    1.59 +  "{p:A. P}" \<rightharpoonup> "CONST Collect (\<lambda>p. p \<in> A \<and> P)"
    1.60  
    1.61  lemma CollectI: "P a \<Longrightarrow> a \<in> {x. P x}"
    1.62    by simp
    1.63 @@ -141,21 +139,13 @@
    1.64  
    1.65  subsection \<open>Subsets and bounded quantifiers\<close>
    1.66  
    1.67 -abbreviation
    1.68 -  subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
    1.69 -  "subset \<equiv> less"
    1.70 -
    1.71 -abbreviation
    1.72 -  subset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
    1.73 -  "subset_eq \<equiv> less_eq"
    1.74 -
    1.75 -notation (output)
    1.76 -  subset  ("op <") and
    1.77 -  subset  ("(_/ < _)" [51, 51] 50) and
    1.78 -  subset_eq  ("op <=") and
    1.79 -  subset_eq  ("(_/ <= _)" [51, 51] 50)
    1.80 -
    1.81 -notation (xsymbols)
    1.82 +abbreviation subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
    1.83 +  where "subset \<equiv> less"
    1.84 +
    1.85 +abbreviation subset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
    1.86 +  where "subset_eq \<equiv> less_eq"
    1.87 +
    1.88 +notation
    1.89    subset  ("op \<subset>") and
    1.90    subset  ("(_/ \<subset> _)" [51, 51] 50) and
    1.91    subset_eq  ("op \<subseteq>") and
    1.92 @@ -169,19 +159,25 @@
    1.93    supset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
    1.94    "supset_eq \<equiv> greater_eq"
    1.95  
    1.96 -notation (xsymbols)
    1.97 +notation
    1.98    supset  ("op \<supset>") and
    1.99    supset  ("(_/ \<supset> _)" [51, 51] 50) and
   1.100    supset_eq  ("op \<supseteq>") and
   1.101    supset_eq  ("(_/ \<supseteq> _)" [51, 51] 50)
   1.102  
   1.103 +notation (ASCII output)
   1.104 +  subset  ("op <") and
   1.105 +  subset  ("(_/ < _)" [51, 51] 50) and
   1.106 +  subset_eq  ("op <=") and
   1.107 +  subset_eq  ("(_/ <= _)" [51, 51] 50)
   1.108 +
   1.109  definition Ball :: "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
   1.110    "Ball A P \<longleftrightarrow> (\<forall>x. x \<in> A \<longrightarrow> P x)"   \<comment> "bounded universal quantifiers"
   1.111  
   1.112  definition Bex :: "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
   1.113    "Bex A P \<longleftrightarrow> (\<exists>x. x \<in> A \<and> P x)"   \<comment> "bounded existential quantifiers"
   1.114  
   1.115 -syntax
   1.116 +syntax (ASCII)
   1.117    "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3ALL _:_./ _)" [0, 0, 10] 10)
   1.118    "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3EX _:_./ _)" [0, 0, 10] 10)
   1.119    "_Bex1"       :: "pttrn => 'a set => bool => bool"      ("(3EX! _:_./ _)" [0, 0, 10] 10)
   1.120 @@ -192,32 +188,25 @@
   1.121    "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3? _:_./ _)" [0, 0, 10] 10)
   1.122    "_Bex1"       :: "pttrn => 'a set => bool => bool"      ("(3?! _:_./ _)" [0, 0, 10] 10)
   1.123  
   1.124 -syntax (xsymbols)
   1.125 +syntax
   1.126    "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
   1.127    "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
   1.128    "_Bex1"       :: "pttrn => 'a set => bool => bool"      ("(3\<exists>!_\<in>_./ _)" [0, 0, 10] 10)
   1.129    "_Bleast"     :: "id => 'a set => bool => 'a"           ("(3LEAST_\<in>_./ _)" [0, 0, 10] 10)
   1.130  
   1.131  translations
   1.132 -  "ALL x:A. P" == "CONST Ball A (%x. P)"
   1.133 -  "EX x:A. P" == "CONST Bex A (%x. P)"
   1.134 -  "EX! x:A. P" => "EX! x. x:A & P"
   1.135 -  "LEAST x:A. P" => "LEAST x. x:A & P"
   1.136 -
   1.137 -syntax (output)
   1.138 +  "\<forall>x\<in>A. P" \<rightleftharpoons> "CONST Ball A (\<lambda>x. P)"
   1.139 +  "\<exists>x\<in>A. P" \<rightleftharpoons> "CONST Bex A (\<lambda>x. P)"
   1.140 +  "\<exists>!x\<in>A. P" \<rightharpoonup> "\<exists>!x. x \<in> A \<and> P"
   1.141 +  "LEAST x:A. P" \<rightharpoonup> "LEAST x. x \<in> A \<and> P"
   1.142 +
   1.143 +syntax (ASCII output)
   1.144    "_setlessAll" :: "[idt, 'a, bool] => bool"  ("(3ALL _<_./ _)"  [0, 0, 10] 10)
   1.145    "_setlessEx"  :: "[idt, 'a, bool] => bool"  ("(3EX _<_./ _)"  [0, 0, 10] 10)
   1.146    "_setleAll"   :: "[idt, 'a, bool] => bool"  ("(3ALL _<=_./ _)" [0, 0, 10] 10)
   1.147    "_setleEx"    :: "[idt, 'a, bool] => bool"  ("(3EX _<=_./ _)" [0, 0, 10] 10)
   1.148    "_setleEx1"   :: "[idt, 'a, bool] => bool"  ("(3EX! _<=_./ _)" [0, 0, 10] 10)
   1.149  
   1.150 -syntax (xsymbols)
   1.151 -  "_setlessAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<subset>_./ _)"  [0, 0, 10] 10)
   1.152 -  "_setlessEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<subset>_./ _)"  [0, 0, 10] 10)
   1.153 -  "_setleAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<subseteq>_./ _)" [0, 0, 10] 10)
   1.154 -  "_setleEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<subseteq>_./ _)" [0, 0, 10] 10)
   1.155 -  "_setleEx1"   :: "[idt, 'a, bool] => bool"   ("(3\<exists>!_\<subseteq>_./ _)" [0, 0, 10] 10)
   1.156 -
   1.157  syntax (HOL output)
   1.158    "_setlessAll" :: "[idt, 'a, bool] => bool"   ("(3! _<_./ _)"  [0, 0, 10] 10)
   1.159    "_setlessEx"  :: "[idt, 'a, bool] => bool"   ("(3? _<_./ _)"  [0, 0, 10] 10)
   1.160 @@ -225,12 +214,19 @@
   1.161    "_setleEx"    :: "[idt, 'a, bool] => bool"   ("(3? _<=_./ _)" [0, 0, 10] 10)
   1.162    "_setleEx1"   :: "[idt, 'a, bool] => bool"   ("(3?! _<=_./ _)" [0, 0, 10] 10)
   1.163  
   1.164 +syntax
   1.165 +  "_setlessAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<subset>_./ _)"  [0, 0, 10] 10)
   1.166 +  "_setlessEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<subset>_./ _)"  [0, 0, 10] 10)
   1.167 +  "_setleAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<subseteq>_./ _)" [0, 0, 10] 10)
   1.168 +  "_setleEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<subseteq>_./ _)" [0, 0, 10] 10)
   1.169 +  "_setleEx1"   :: "[idt, 'a, bool] => bool"   ("(3\<exists>!_\<subseteq>_./ _)" [0, 0, 10] 10)
   1.170 +
   1.171  translations
   1.172 - "\<forall>A\<subset>B. P"   =>  "ALL A. A \<subset> B --> P"
   1.173 - "\<exists>A\<subset>B. P"   =>  "EX A. A \<subset> B & P"
   1.174 - "\<forall>A\<subseteq>B. P"   =>  "ALL A. A \<subseteq> B --> P"
   1.175 - "\<exists>A\<subseteq>B. P"   =>  "EX A. A \<subseteq> B & P"
   1.176 - "\<exists>!A\<subseteq>B. P"  =>  "EX! A. A \<subseteq> B & P"
   1.177 + "\<forall>A\<subset>B. P"   \<rightharpoonup>  "\<forall>A. A \<subset> B \<longrightarrow> P"
   1.178 + "\<exists>A\<subset>B. P"   \<rightharpoonup>  "\<exists>A. A \<subset> B \<and> P"
   1.179 + "\<forall>A\<subseteq>B. P"   \<rightharpoonup>  "\<forall>A. A \<subseteq> B \<longrightarrow> P"
   1.180 + "\<exists>A\<subseteq>B. P"   \<rightharpoonup>  "\<exists>A. A \<subseteq> B \<and> P"
   1.181 + "\<exists>!A\<subseteq>B. P"  \<rightharpoonup>  "\<exists>!A. A \<subseteq> B \<and> P"
   1.182  
   1.183  print_translation \<open>
   1.184    let
   1.185 @@ -669,11 +665,11 @@
   1.186  
   1.187  subsubsection \<open>Binary intersection\<close>
   1.188  
   1.189 -abbreviation inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
   1.190 -  "op Int \<equiv> inf"
   1.191 -
   1.192 -notation (xsymbols)
   1.193 -  inter  (infixl "\<inter>" 70)
   1.194 +abbreviation inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "\<inter>" 70)
   1.195 +  where "op \<inter> \<equiv> inf"
   1.196 +
   1.197 +notation (ASCII)
   1.198 +  inter  (infixl "Int" 70)
   1.199  
   1.200  lemma Int_def:
   1.201    "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"
   1.202 @@ -700,11 +696,11 @@
   1.203  
   1.204  subsubsection \<open>Binary union\<close>
   1.205  
   1.206 -abbreviation union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
   1.207 -  "union \<equiv> sup"
   1.208 -
   1.209 -notation (xsymbols)
   1.210 -  union  (infixl "\<union>" 65)
   1.211 +abbreviation union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "\<union>" 65)
   1.212 +  where "union \<equiv> sup"
   1.213 +
   1.214 +notation (ASCII)
   1.215 +  union  (infixl "Un" 65)
   1.216  
   1.217  lemma Un_def:
   1.218    "A \<union> B = {x. x \<in> A \<or> x \<in> B}"