tuned lemma positions and proofs
authorhaftmann
Thu Jul 14 00:20:43 2011 +0200 (2011-07-14)
changeset 43818fcc5d3ffb6f5
parent 43817 d53350bc65a4
child 43819 89082fd9e32d
tuned lemma positions and proofs
src/HOL/Complete_Lattice.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/Complete_Lattice.thy	Thu Jul 14 00:16:41 2011 +0200
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Thu Jul 14 00:20:43 2011 +0200
     1.3 @@ -6,14 +6,6 @@
     1.4  imports Set
     1.5  begin
     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  notation
    1.16    less_eq (infix "\<sqsubseteq>" 50) and
    1.17    less (infix "\<sqsubset>" 50) and
     2.1 --- a/src/HOL/Set.thy	Thu Jul 14 00:16:41 2011 +0200
     2.2 +++ b/src/HOL/Set.thy	Thu Jul 14 00:20:43 2011 +0200
     2.3 @@ -416,6 +416,14 @@
     2.4  lemma ball_one_point2 [simp]: "(ALL x:A. a = x --> P x) = (a:A --> P a)"
     2.5    by blast
     2.6  
     2.7 +lemma ball_conj_distrib:
     2.8 +  "(\<forall>x\<in>A. P x \<and> Q x) \<longleftrightarrow> ((\<forall>x\<in>A. P x) \<and> (\<forall>x\<in>A. Q x))"
     2.9 +  by blast
    2.10 +
    2.11 +lemma bex_disj_distrib:
    2.12 +  "(\<exists>x\<in>A. P x \<or> Q x) \<longleftrightarrow> ((\<exists>x\<in>A. P x) \<or> (\<exists>x\<in>A. Q x))"
    2.13 +  by blast
    2.14 +
    2.15  
    2.16  text {* Congruence rules *}
    2.17  
    2.18 @@ -535,7 +543,7 @@
    2.19  
    2.20  lemma empty_def:
    2.21    "{} = {x. False}"
    2.22 -  by (simp add: bot_fun_def bot_bool_def Collect_def)
    2.23 +  by (simp add: bot_fun_def Collect_def)
    2.24  
    2.25  lemma empty_iff [simp]: "(c : {}) = False"
    2.26    by (simp add: empty_def)
    2.27 @@ -568,7 +576,7 @@
    2.28  
    2.29  lemma UNIV_def:
    2.30    "UNIV = {x. True}"
    2.31 -  by (simp add: top_fun_def top_bool_def Collect_def)
    2.32 +  by (simp add: top_fun_def Collect_def)
    2.33  
    2.34  lemma UNIV_I [simp]: "x : UNIV"
    2.35    by (simp add: UNIV_def)
    2.36 @@ -627,7 +635,7 @@
    2.37  subsubsection {* Set complement *}
    2.38  
    2.39  lemma Compl_iff [simp]: "(c \<in> -A) = (c \<notin> A)"
    2.40 -  by (simp add: mem_def fun_Compl_def bool_Compl_def)
    2.41 +  by (simp add: mem_def fun_Compl_def)
    2.42  
    2.43  lemma ComplI [intro!]: "(c \<in> A ==> False) ==> c \<in> -A"
    2.44    by (unfold mem_def fun_Compl_def bool_Compl_def) blast
    2.45 @@ -638,7 +646,7 @@
    2.46    right side of the notional turnstile ... *}
    2.47  
    2.48  lemma ComplD [dest!]: "c : -A ==> c~:A"
    2.49 -  by (simp add: mem_def fun_Compl_def bool_Compl_def)
    2.50 +  by (simp add: mem_def fun_Compl_def)
    2.51  
    2.52  lemmas ComplE = ComplD [elim_format]
    2.53  
    2.54 @@ -658,7 +666,7 @@
    2.55  
    2.56  lemma Int_def:
    2.57    "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"
    2.58 -  by (simp add: inf_fun_def inf_bool_def Collect_def mem_def)
    2.59 +  by (simp add: inf_fun_def Collect_def mem_def)
    2.60  
    2.61  lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)"
    2.62    by (unfold Int_def) blast
    2.63 @@ -692,7 +700,7 @@
    2.64  
    2.65  lemma Un_def:
    2.66    "A \<union> B = {x. x \<in> A \<or> x \<in> B}"
    2.67 -  by (simp add: sup_fun_def sup_bool_def Collect_def mem_def)
    2.68 +  by (simp add: sup_fun_def Collect_def mem_def)
    2.69  
    2.70  lemma Un_iff [simp]: "(c : A Un B) = (c:A | c:B)"
    2.71    by (unfold Un_def) blast
    2.72 @@ -724,7 +732,7 @@
    2.73  subsubsection {* Set difference *}
    2.74  
    2.75  lemma Diff_iff [simp]: "(c : A - B) = (c:A & c~:B)"
    2.76 -  by (simp add: mem_def fun_diff_def bool_diff_def)
    2.77 +  by (simp add: mem_def fun_diff_def)
    2.78  
    2.79  lemma DiffI [intro!]: "c : A ==> c ~: B ==> c : A - B"
    2.80    by simp