src/HOL/Set.thy
changeset 43818 fcc5d3ffb6f5
parent 42459 38b9f023cc34
child 43866 8a50dc70cbff
     1.1 --- a/src/HOL/Set.thy	Thu Jul 14 00:16:41 2011 +0200
     1.2 +++ b/src/HOL/Set.thy	Thu Jul 14 00:20:43 2011 +0200
     1.3 @@ -416,6 +416,14 @@
     1.4  lemma ball_one_point2 [simp]: "(ALL x:A. a = x --> P x) = (a:A --> P a)"
     1.5    by blast
     1.6  
     1.7 +lemma ball_conj_distrib:
     1.8 +  "(\<forall>x\<in>A. P x \<and> Q x) \<longleftrightarrow> ((\<forall>x\<in>A. P x) \<and> (\<forall>x\<in>A. Q x))"
     1.9 +  by blast
    1.10 +
    1.11 +lemma bex_disj_distrib:
    1.12 +  "(\<exists>x\<in>A. P x \<or> Q x) \<longleftrightarrow> ((\<exists>x\<in>A. P x) \<or> (\<exists>x\<in>A. Q x))"
    1.13 +  by blast
    1.14 +
    1.15  
    1.16  text {* Congruence rules *}
    1.17  
    1.18 @@ -535,7 +543,7 @@
    1.19  
    1.20  lemma empty_def:
    1.21    "{} = {x. False}"
    1.22 -  by (simp add: bot_fun_def bot_bool_def Collect_def)
    1.23 +  by (simp add: bot_fun_def Collect_def)
    1.24  
    1.25  lemma empty_iff [simp]: "(c : {}) = False"
    1.26    by (simp add: empty_def)
    1.27 @@ -568,7 +576,7 @@
    1.28  
    1.29  lemma UNIV_def:
    1.30    "UNIV = {x. True}"
    1.31 -  by (simp add: top_fun_def top_bool_def Collect_def)
    1.32 +  by (simp add: top_fun_def Collect_def)
    1.33  
    1.34  lemma UNIV_I [simp]: "x : UNIV"
    1.35    by (simp add: UNIV_def)
    1.36 @@ -627,7 +635,7 @@
    1.37  subsubsection {* Set complement *}
    1.38  
    1.39  lemma Compl_iff [simp]: "(c \<in> -A) = (c \<notin> A)"
    1.40 -  by (simp add: mem_def fun_Compl_def bool_Compl_def)
    1.41 +  by (simp add: mem_def fun_Compl_def)
    1.42  
    1.43  lemma ComplI [intro!]: "(c \<in> A ==> False) ==> c \<in> -A"
    1.44    by (unfold mem_def fun_Compl_def bool_Compl_def) blast
    1.45 @@ -638,7 +646,7 @@
    1.46    right side of the notional turnstile ... *}
    1.47  
    1.48  lemma ComplD [dest!]: "c : -A ==> c~:A"
    1.49 -  by (simp add: mem_def fun_Compl_def bool_Compl_def)
    1.50 +  by (simp add: mem_def fun_Compl_def)
    1.51  
    1.52  lemmas ComplE = ComplD [elim_format]
    1.53  
    1.54 @@ -658,7 +666,7 @@
    1.55  
    1.56  lemma Int_def:
    1.57    "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"
    1.58 -  by (simp add: inf_fun_def inf_bool_def Collect_def mem_def)
    1.59 +  by (simp add: inf_fun_def Collect_def mem_def)
    1.60  
    1.61  lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)"
    1.62    by (unfold Int_def) blast
    1.63 @@ -692,7 +700,7 @@
    1.64  
    1.65  lemma Un_def:
    1.66    "A \<union> B = {x. x \<in> A \<or> x \<in> B}"
    1.67 -  by (simp add: sup_fun_def sup_bool_def Collect_def mem_def)
    1.68 +  by (simp add: sup_fun_def Collect_def mem_def)
    1.69  
    1.70  lemma Un_iff [simp]: "(c : A Un B) = (c:A | c:B)"
    1.71    by (unfold Un_def) blast
    1.72 @@ -724,7 +732,7 @@
    1.73  subsubsection {* Set difference *}
    1.74  
    1.75  lemma Diff_iff [simp]: "(c : A - B) = (c:A & c~:B)"
    1.76 -  by (simp add: mem_def fun_diff_def bool_diff_def)
    1.77 +  by (simp add: mem_def fun_diff_def)
    1.78  
    1.79  lemma DiffI [intro!]: "c : A ==> c ~: B ==> c : A - B"
    1.80    by simp