src/HOL/Set.thy
changeset 32117 0762b9ad83df
parent 32115 8f10fb3bb46e
child 32120 53a21a5e6889
     1.1 --- a/src/HOL/Set.thy	Tue Jul 21 07:55:56 2009 +0200
     1.2 +++ b/src/HOL/Set.thy	Tue Jul 21 11:09:50 2009 +0200
     1.3 @@ -80,12 +80,30 @@
     1.4  lemma Collect_cong: "(!!x. P x = Q x) ==> {x. P(x)} = {x. Q(x)}"
     1.5    by simp
     1.6  
     1.7 +text {*
     1.8 +Simproc for pulling @{text "x=t"} in @{text "{x. \<dots> & x=t & \<dots>}"}
     1.9 +to the front (and similarly for @{text "t=x"}):
    1.10 +*}
    1.11 +
    1.12 +setup {*
    1.13 +let
    1.14 +  val Coll_perm_tac = rtac @{thm Collect_cong} 1 THEN rtac @{thm iffI} 1 THEN
    1.15 +    ALLGOALS(EVERY'[REPEAT_DETERM o (etac @{thm conjE}),
    1.16 +                    DEPTH_SOLVE_1 o (ares_tac [@{thm conjI}])])
    1.17 +  val defColl_regroup = Simplifier.simproc @{theory}
    1.18 +    "defined Collect" ["{x. P x & Q x}"]
    1.19 +    (Quantifier1.rearrange_Coll Coll_perm_tac)
    1.20 +in
    1.21 +  Simplifier.map_simpset (fn ss => ss addsimprocs [defColl_regroup])
    1.22 +end
    1.23 +*}
    1.24 +
    1.25  lemmas CollectE = CollectD [elim_format]
    1.26  
    1.27  text {* Set enumerations *}
    1.28  
    1.29  definition empty :: "'a set" ("{}") where
    1.30 -  "empty \<equiv> {x. False}"
    1.31 +  "empty = {x. False}"
    1.32  
    1.33  definition insert :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    1.34    insert_compr: "insert a B = {x. x = a \<or> x \<in> B}"
    1.35 @@ -311,6 +329,23 @@
    1.36    in [("Collect", setcompr_tr')] end;
    1.37  *}
    1.38  
    1.39 +setup {*
    1.40 +let
    1.41 +  val unfold_bex_tac = unfold_tac @{thms "Bex_def"};
    1.42 +  fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
    1.43 +  val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
    1.44 +  val unfold_ball_tac = unfold_tac @{thms "Ball_def"};
    1.45 +  fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
    1.46 +  val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
    1.47 +  val defBEX_regroup = Simplifier.simproc @{theory}
    1.48 +    "defined BEX" ["EX x:A. P x & Q x"] rearrange_bex;
    1.49 +  val defBALL_regroup = Simplifier.simproc @{theory}
    1.50 +    "defined BALL" ["ALL x:A. P x --> Q x"] rearrange_ball;
    1.51 +in
    1.52 +  Simplifier.map_simpset (fn ss => ss addsimprocs [defBALL_regroup, defBEX_regroup])
    1.53 +end
    1.54 +*}
    1.55 +
    1.56  lemma ballI [intro!]: "(!!x. x:A ==> P x) ==> ALL x:A. P x"
    1.57    by (simp add: Ball_def)
    1.58  
    1.59 @@ -319,20 +354,6 @@
    1.60  lemma bspec [dest?]: "ALL x:A. P x ==> x:A ==> P x"
    1.61    by (simp add: Ball_def)
    1.62  
    1.63 -lemma ballE [elim]: "ALL x:A. P x ==> (P x ==> Q) ==> (x ~: A ==> Q) ==> Q"
    1.64 -  by (unfold Ball_def) blast
    1.65 -
    1.66 -ML {* bind_thm ("rev_ballE", Thm.permute_prems 1 1 @{thm ballE}) *}
    1.67 -
    1.68 -text {*
    1.69 -  \medskip This tactic takes assumptions @{prop "ALL x:A. P x"} and
    1.70 -  @{prop "a:A"}; creates assumption @{prop "P a"}.
    1.71 -*}
    1.72 -
    1.73 -ML {*
    1.74 -  fun ball_tac i = etac @{thm ballE} i THEN contr_tac (i + 1)
    1.75 -*}
    1.76 -
    1.77  text {*
    1.78    Gives better instantiation for bound:
    1.79  *}
    1.80 @@ -341,6 +362,26 @@
    1.81    Classical.map_cs (fn cs => cs addbefore ("bspec", datac @{thm bspec} 1))
    1.82  *}
    1.83  
    1.84 +ML {*
    1.85 +structure Simpdata =
    1.86 +struct
    1.87 +
    1.88 +open Simpdata;
    1.89 +
    1.90 +val mksimps_pairs = [(@{const_name Ball}, @{thms bspec})] @ mksimps_pairs;
    1.91 +
    1.92 +end;
    1.93 +
    1.94 +open Simpdata;
    1.95 +*}
    1.96 +
    1.97 +declaration {* fn _ =>
    1.98 +  Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs))
    1.99 +*}
   1.100 +
   1.101 +lemma ballE [elim]: "ALL x:A. P x ==> (P x ==> Q) ==> (x ~: A ==> Q) ==> Q"
   1.102 +  by (unfold Ball_def) blast
   1.103 +
   1.104  lemma bexI [intro]: "P x ==> x:A ==> EX x:A. P x"
   1.105    -- {* Normally the best argument order: @{prop "P x"} constrains the
   1.106      choice of @{prop "x:A"}. *}
   1.107 @@ -382,24 +423,6 @@
   1.108  lemma ball_one_point2 [simp]: "(ALL x:A. a = x --> P x) = (a:A --> P a)"
   1.109    by blast
   1.110  
   1.111 -ML {*
   1.112 -  local
   1.113 -    val unfold_bex_tac = unfold_tac @{thms "Bex_def"};
   1.114 -    fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
   1.115 -    val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
   1.116 -
   1.117 -    val unfold_ball_tac = unfold_tac @{thms "Ball_def"};
   1.118 -    fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
   1.119 -    val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
   1.120 -  in
   1.121 -    val defBEX_regroup = Simplifier.simproc @{theory}
   1.122 -      "defined BEX" ["EX x:A. P x & Q x"] rearrange_bex;
   1.123 -    val defBALL_regroup = Simplifier.simproc @{theory}
   1.124 -      "defined BALL" ["ALL x:A. P x --> Q x"] rearrange_ball;
   1.125 -  end;
   1.126 -
   1.127 -  Addsimprocs [defBALL_regroup, defBEX_regroup];
   1.128 -*}
   1.129  
   1.130  text {* Congruence rules *}
   1.131  
   1.132 @@ -450,25 +473,12 @@
   1.133    \medskip Converts @{prop "A \<subseteq> B"} to @{prop "x \<in> A ==> x \<in> B"}.
   1.134  *}
   1.135  
   1.136 -ML {*
   1.137 -  fun impOfSubs th = th RSN (2, @{thm rev_subsetD})
   1.138 -*}
   1.139 -
   1.140  lemma subsetCE [elim]: "A \<subseteq>  B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
   1.141    -- {* Classical elimination rule. *}
   1.142    by (unfold mem_def) blast
   1.143  
   1.144  lemma subset_eq: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
   1.145  
   1.146 -text {*
   1.147 -  \medskip Takes assumptions @{prop "A \<subseteq> B"}; @{prop "c \<in> A"} and
   1.148 -  creates the assumption @{prop "c \<in> B"}.
   1.149 -*}
   1.150 -
   1.151 -ML {*
   1.152 -  fun set_mp_tac i = etac @{thm subsetCE} i THEN mp_tac i
   1.153 -*}
   1.154 -
   1.155  lemma contra_subsetD: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
   1.156    by blast
   1.157  
   1.158 @@ -538,7 +548,7 @@
   1.159  subsubsection {* The universal set -- UNIV *}
   1.160  
   1.161  definition UNIV :: "'a set" where
   1.162 -  "UNIV \<equiv> {x. True}"
   1.163 +  "UNIV = {x. True}"
   1.164  
   1.165  lemma UNIV_I [simp]: "x : UNIV"
   1.166    by (simp add: UNIV_def)
   1.167 @@ -647,7 +657,7 @@
   1.168  subsubsection {* Binary union -- Un *}
   1.169  
   1.170  definition Un :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
   1.171 -  "A Un B \<equiv> {x. x \<in> A \<or> x \<in> B}"
   1.172 +  "A Un B = {x. x \<in> A \<or> x \<in> B}"
   1.173  
   1.174  notation (xsymbols)
   1.175    "Un"  (infixl "\<union>" 65)
   1.176 @@ -678,7 +688,7 @@
   1.177  lemma UnE [elim!]: "c : A Un B ==> (c:A ==> P) ==> (c:B ==> P) ==> P"
   1.178    by (unfold Un_def) blast
   1.179  
   1.180 -lemma insert_def: "insert a B \<equiv> {x. x = a} \<union> B"
   1.181 +lemma insert_def: "insert a B = {x. x = a} \<union> B"
   1.182    by (simp add: Collect_def mem_def insert_compr Un_def)
   1.183  
   1.184  lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"
   1.185 @@ -690,7 +700,7 @@
   1.186  subsubsection {* Binary intersection -- Int *}
   1.187  
   1.188  definition Int :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
   1.189 -  "A Int B \<equiv> {x. x \<in> A \<and> x \<in> B}"
   1.190 +  "A Int B = {x. x \<in> A \<and> x \<in> B}"
   1.191  
   1.192  notation (xsymbols)
   1.193    "Int"  (infixl "\<inter>" 70)
   1.194 @@ -883,34 +893,15 @@
   1.195    by blast
   1.196  
   1.197  
   1.198 -subsubsection {* Some proof tools *}
   1.199 +subsubsection {* Some rules with @{text "if"} *}
   1.200  
   1.201  text{* Elimination of @{text"{x. \<dots> & x=t & \<dots>}"}. *}
   1.202  
   1.203  lemma Collect_conv_if: "{x. x=a & P x} = (if P a then {a} else {})"
   1.204 -by auto
   1.205 +  by auto
   1.206  
   1.207  lemma Collect_conv_if2: "{x. a=x & P x} = (if P a then {a} else {})"
   1.208 -by auto
   1.209 -
   1.210 -text {*
   1.211 -Simproc for pulling @{text "x=t"} in @{text "{x. \<dots> & x=t & \<dots>}"}
   1.212 -to the front (and similarly for @{text "t=x"}):
   1.213 -*}
   1.214 -
   1.215 -ML{*
   1.216 -  local
   1.217 -    val Coll_perm_tac = rtac @{thm Collect_cong} 1 THEN rtac @{thm iffI} 1 THEN
   1.218 -    ALLGOALS(EVERY'[REPEAT_DETERM o (etac @{thm conjE}),
   1.219 -                    DEPTH_SOLVE_1 o (ares_tac [@{thm conjI}])])
   1.220 -  in
   1.221 -    val defColl_regroup = Simplifier.simproc @{theory}
   1.222 -      "defined Collect" ["{x. P x & Q x}"]
   1.223 -      (Quantifier1.rearrange_Coll Coll_perm_tac)
   1.224 -  end;
   1.225 -
   1.226 -  Addsimprocs [defColl_regroup];
   1.227 -*}
   1.228 +  by auto
   1.229  
   1.230  text {*
   1.231    Rewrite rules for boolean case-splitting: faster than @{text
   1.232 @@ -945,13 +936,6 @@
   1.233     ("Collect", [CollectD]), ("Inter", [InterD]), ("INTER", [INT_D])]
   1.234   *)
   1.235  
   1.236 -ML {*
   1.237 -  val mksimps_pairs = [(@{const_name Ball}, @{thms bspec})] @ mksimps_pairs;
   1.238 -*}
   1.239 -declaration {* fn _ =>
   1.240 -  Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs))
   1.241 -*}
   1.242 -
   1.243  
   1.244  subsection {* Complete lattices *}
   1.245  
   1.246 @@ -1029,10 +1013,10 @@
   1.247    using top_greatest [of x] by (simp add: le_iff_inf inf_commute)
   1.248  
   1.249  definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
   1.250 -  "SUPR A f == \<Squnion> (f ` A)"
   1.251 +  "SUPR A f = \<Squnion> (f ` A)"
   1.252  
   1.253  definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
   1.254 -  "INFI A f == \<Sqinter> (f ` A)"
   1.255 +  "INFI A f = \<Sqinter> (f ` A)"
   1.256  
   1.257  end
   1.258  
   1.259 @@ -1215,12 +1199,12 @@
   1.260    by (simp add: SUPR_def UNION_eq_Union_image Sup_set_eq)
   1.261  
   1.262  lemma Union_def:
   1.263 -  "\<Union>S \<equiv> \<Union>x\<in>S. x"
   1.264 +  "\<Union>S = (\<Union>x\<in>S. x)"
   1.265    by (simp add: UNION_eq_Union_image image_def)
   1.266  
   1.267  lemma UNION_def [noatp]:
   1.268 -  "UNION A B \<equiv> {y. \<exists>x\<in>A. y \<in> B x}"
   1.269 -  by (rule eq_reflection) (auto simp add: UNION_eq_Union_image Union_eq)
   1.270 +  "UNION A B = {y. \<exists>x\<in>A. y \<in> B x}"
   1.271 +  by (auto simp add: UNION_eq_Union_image Union_eq)
   1.272    
   1.273  lemma Union_image_eq [simp]:
   1.274    "\<Union>(B`A) = (\<Union>x\<in>A. B x)"
   1.275 @@ -1325,12 +1309,12 @@
   1.276    by (simp add: INFI_def INTER_eq_Inter_image Inf_set_eq)
   1.277  
   1.278  lemma Inter_def:
   1.279 -  "Inter S \<equiv> INTER S (\<lambda>x. x)"
   1.280 +  "Inter S = INTER S (\<lambda>x. x)"
   1.281    by (simp add: INTER_eq_Inter_image image_def)
   1.282  
   1.283  lemma INTER_def:
   1.284 -  "INTER A B \<equiv> {y. \<forall>x\<in>A. y \<in> B x}"
   1.285 -  by (rule eq_reflection) (auto simp add: INTER_eq_Inter_image Inter_eq)
   1.286 +  "INTER A B = {y. \<forall>x\<in>A. y \<in> B x}"
   1.287 +  by (auto simp add: INTER_eq_Inter_image Inter_eq)
   1.288  
   1.289  lemma Inter_image_eq [simp]:
   1.290    "\<Inter>(B`A) = (\<Inter>x\<in>A. B x)"
   1.291 @@ -2476,23 +2460,24 @@
   1.292  
   1.293  text {* Rudimentary code generation *}
   1.294  
   1.295 -lemma empty_code [code]: "{} x \<longleftrightarrow> False"
   1.296 -  unfolding empty_def Collect_def ..
   1.297 -
   1.298 -lemma UNIV_code [code]: "UNIV x \<longleftrightarrow> True"
   1.299 -  unfolding UNIV_def Collect_def ..
   1.300 +lemma [code]: "{} = bot"
   1.301 +  by (rule sym) (fact bot_set_eq)
   1.302 +
   1.303 +lemma [code]: "UNIV = top"
   1.304 +  by (rule sym) (fact top_set_eq)
   1.305 +
   1.306 +lemma [code]: "op \<inter> = inf"
   1.307 +  by (rule ext)+ (simp add: inf_set_eq)
   1.308 +
   1.309 +lemma [code]: "op \<union> = sup"
   1.310 +  by (rule ext)+ (simp add: sup_set_eq)
   1.311  
   1.312  lemma insert_code [code]: "insert y A x \<longleftrightarrow> y = x \<or> A x"
   1.313 -  unfolding insert_def Collect_def mem_def Un_def by auto
   1.314 -
   1.315 -lemma inter_code [code]: "(A \<inter> B) x \<longleftrightarrow> A x \<and> B x"
   1.316 -  unfolding Int_def Collect_def mem_def ..
   1.317 -
   1.318 -lemma union_code [code]: "(A \<union> B) x \<longleftrightarrow> A x \<or> B x"
   1.319 -  unfolding Un_def Collect_def mem_def ..
   1.320 +  by (auto simp add: insert_compr Collect_def mem_def)
   1.321  
   1.322  lemma vimage_code [code]: "(f -` A) x = A (f x)"
   1.323 -  unfolding vimage_def Collect_def mem_def ..
   1.324 +  by (simp add: vimage_def Collect_def mem_def)
   1.325 +
   1.326  
   1.327  text {* Misc theorem and ML bindings *}
   1.328