moved most fundamental lemmas upwards
authorhaftmann
Fri Dec 10 16:10:50 2010 +0100 (2010-12-10)
changeset 411078795cd75965e
parent 41103 eaefbe8aac1c
child 41108 3f22550e442f
moved most fundamental lemmas upwards
src/HOL/Set.thy
     1.1 --- a/src/HOL/Set.thy	Fri Dec 10 09:18:17 2010 +0100
     1.2 +++ b/src/HOL/Set.thy	Fri Dec 10 16:10:50 2010 +0100
     1.3 @@ -39,6 +39,8 @@
     1.4    not_member  ("op \<notin>") and
     1.5    not_member  ("(_/ \<notin> _)" [50, 51] 50)
     1.6  
     1.7 +
     1.8 +
     1.9  text {* Set comprehensions *}
    1.10  
    1.11  syntax
    1.12 @@ -53,19 +55,19 @@
    1.13  translations
    1.14    "{x:A. P}" => "{x. x:A & P}"
    1.15  
    1.16 -lemma mem_Collect_eq [iff]: "(a : {x. P(x)}) = P(a)"
    1.17 +lemma mem_Collect_eq [iff]: "a \<in> {x. P x} = P a"
    1.18    by (simp add: Collect_def mem_def)
    1.19  
    1.20 -lemma Collect_mem_eq [simp]: "{x. x:A} = A"
    1.21 +lemma Collect_mem_eq [simp]: "{x. x \<in> A} = A"
    1.22    by (simp add: Collect_def mem_def)
    1.23  
    1.24 -lemma CollectI: "P(a) ==> a : {x. P(x)}"
    1.25 +lemma CollectI: "P a \<Longrightarrow> a \<in> {x. P x}"
    1.26    by simp
    1.27  
    1.28 -lemma CollectD: "a : {x. P(x)} ==> P(a)"
    1.29 +lemma CollectD: "a \<in> {x. P x} \<Longrightarrow> P a"
    1.30    by simp
    1.31  
    1.32 -lemma Collect_cong: "(!!x. P x = Q x) ==> {x. P(x)} = {x. Q(x)}"
    1.33 +lemma Collect_cong: "(\<And>x. P x = Q x) ==> {x. P x} = {x. Q x}"
    1.34    by simp
    1.35  
    1.36  text {*
    1.37 @@ -88,6 +90,18 @@
    1.38  
    1.39  lemmas CollectE = CollectD [elim_format]
    1.40  
    1.41 +lemma set_eqI:
    1.42 +  assumes "\<And>x. x \<in> A \<longleftrightarrow> x \<in> B"
    1.43 +  shows "A = B"
    1.44 +proof -
    1.45 +  from assms have "{x. x \<in> A} = {x. x \<in> B}" by simp
    1.46 +  then show ?thesis by simp
    1.47 +qed
    1.48 +
    1.49 +lemma set_eq_iff [no_atp]:
    1.50 +  "A = B \<longleftrightarrow> (\<forall>x. x \<in> A \<longleftrightarrow> x \<in> B)"
    1.51 +  by (auto intro:set_eqI)
    1.52 +
    1.53  text {* Set enumerations *}
    1.54  
    1.55  abbreviation empty :: "'a set" ("{}") where
    1.56 @@ -489,15 +503,6 @@
    1.57  
    1.58  subsubsection {* Equality *}
    1.59  
    1.60 -lemma set_eqI: assumes prem: "(!!x. (x:A) = (x:B))" shows "A = B"
    1.61 -  apply (rule prem [THEN ext, THEN arg_cong, THEN box_equals])
    1.62 -   apply (rule Collect_mem_eq)
    1.63 -  apply (rule Collect_mem_eq)
    1.64 -  done
    1.65 -
    1.66 -lemma set_eq_iff [no_atp]: "(A = B) = (ALL x. (x:A) = (x:B))"
    1.67 -by(auto intro:set_eqI)
    1.68 -
    1.69  lemma subset_antisym [intro!]: "A \<subseteq> B ==> B \<subseteq> A ==> A = B"
    1.70    -- {* Anti-symmetry of the subset relation. *}
    1.71    by (iprover intro: set_eqI subsetD)