src/HOL/Complete_Lattice.thy
changeset 35828 46cfc4b8112e
parent 35629 57f1a5e93b6b
child 36364 0e2679025aeb
     1.1 --- a/src/HOL/Complete_Lattice.thy	Wed Mar 17 19:37:44 2010 +0100
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Thu Mar 18 12:58:52 2010 +0100
     1.3 @@ -231,7 +231,7 @@
     1.4      by (simp add: Sup_fun_def Sup_bool_def) (simp add: mem_def)
     1.5  qed
     1.6  
     1.7 -lemma Union_iff [simp, noatp]:
     1.8 +lemma Union_iff [simp, no_atp]:
     1.9    "A \<in> \<Union>C \<longleftrightarrow> (\<exists>X\<in>C. A\<in>X)"
    1.10    by (unfold Union_eq) blast
    1.11  
    1.12 @@ -269,10 +269,10 @@
    1.13  lemma Union_Int_subset: "\<Union>(A \<inter> B) \<subseteq> \<Union>A \<inter> \<Union>B"
    1.14    by blast
    1.15  
    1.16 -lemma Union_empty_conv [simp,noatp]: "(\<Union>A = {}) = (\<forall>x\<in>A. x = {})"
    1.17 +lemma Union_empty_conv [simp,no_atp]: "(\<Union>A = {}) = (\<forall>x\<in>A. x = {})"
    1.18    by blast
    1.19  
    1.20 -lemma empty_Union_conv [simp,noatp]: "({} = \<Union>A) = (\<forall>x\<in>A. x = {})"
    1.21 +lemma empty_Union_conv [simp,no_atp]: "({} = \<Union>A) = (\<forall>x\<in>A. x = {})"
    1.22    by blast
    1.23  
    1.24  lemma Union_disjoint: "(\<Union>C \<inter> A = {}) = (\<forall>B\<in>C. B \<inter> A = {})"
    1.25 @@ -332,7 +332,7 @@
    1.26    "\<Union>S = (\<Union>x\<in>S. x)"
    1.27    by (simp add: UNION_eq_Union_image image_def)
    1.28  
    1.29 -lemma UNION_def [noatp]:
    1.30 +lemma UNION_def [no_atp]:
    1.31    "(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"
    1.32    by (auto simp add: UNION_eq_Union_image Union_eq)
    1.33    
    1.34 @@ -368,13 +368,13 @@
    1.35  lemma UN_least: "(!!x. x \<in> A ==> B x \<subseteq> C) ==> (\<Union>x\<in>A. B x) \<subseteq> C"
    1.36    by (iprover intro: subsetI elim: UN_E dest: subsetD)
    1.37  
    1.38 -lemma Collect_bex_eq [noatp]: "{x. \<exists>y\<in>A. P x y} = (\<Union>y\<in>A. {x. P x y})"
    1.39 +lemma Collect_bex_eq [no_atp]: "{x. \<exists>y\<in>A. P x y} = (\<Union>y\<in>A. {x. P x y})"
    1.40    by blast
    1.41  
    1.42  lemma UN_insert_distrib: "u \<in> A ==> (\<Union>x\<in>A. insert a (B x)) = insert a (\<Union>x\<in>A. B x)"
    1.43    by blast
    1.44  
    1.45 -lemma UN_empty [simp,noatp]: "(\<Union>x\<in>{}. B x) = {}"
    1.46 +lemma UN_empty [simp,no_atp]: "(\<Union>x\<in>{}. B x) = {}"
    1.47    by blast
    1.48  
    1.49  lemma UN_empty2 [simp]: "(\<Union>x\<in>A. {}) = {}"
    1.50 @@ -412,7 +412,7 @@
    1.51    "((UN x:A. B x) = {}) = (\<forall>x\<in>A. B x = {})"
    1.52  by blast+
    1.53  
    1.54 -lemma Collect_ex_eq [noatp]: "{x. \<exists>y. P x y} = (\<Union>y. {x. P x y})"
    1.55 +lemma Collect_ex_eq [no_atp]: "{x. \<exists>y. P x y} = (\<Union>y. {x. P x y})"
    1.56    by blast
    1.57  
    1.58  lemma ball_UN: "(\<forall>z \<in> UNION A B. P z) = (\<forall>x\<in>A. \<forall>z \<in> B x. P z)"
    1.59 @@ -467,7 +467,7 @@
    1.60      by (simp add: Inf_fun_def Inf_bool_def) (simp add: mem_def)
    1.61  qed
    1.62  
    1.63 -lemma Inter_iff [simp,noatp]: "(A : Inter C) = (ALL X:C. A:X)"
    1.64 +lemma Inter_iff [simp,no_atp]: "(A : Inter C) = (ALL X:C. A:X)"
    1.65    by (unfold Inter_eq) blast
    1.66  
    1.67  lemma InterI [intro!]: "(!!X. X:C ==> A:X) ==> A : Inter C"
    1.68 @@ -515,7 +515,7 @@
    1.69  lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
    1.70    by blast
    1.71  
    1.72 -lemma Inter_UNIV_conv [simp,noatp]:
    1.73 +lemma Inter_UNIV_conv [simp,no_atp]:
    1.74    "(\<Inter>A = UNIV) = (\<forall>x\<in>A. x = UNIV)"
    1.75    "(UNIV = \<Inter>A) = (\<forall>x\<in>A. x = UNIV)"
    1.76    by blast+
    1.77 @@ -724,7 +724,7 @@
    1.78    "!!A B f. (INT x:f`A. B x)    = (INT a:A. B (f a))"
    1.79    by auto
    1.80  
    1.81 -lemma ball_simps [simp,noatp]:
    1.82 +lemma ball_simps [simp,no_atp]:
    1.83    "!!A P Q. (ALL x:A. P x | Q) = ((ALL x:A. P x) | Q)"
    1.84    "!!A P Q. (ALL x:A. P | Q x) = (P | (ALL x:A. Q x))"
    1.85    "!!A P Q. (ALL x:A. P --> Q x) = (P --> (ALL x:A. Q x))"
    1.86 @@ -739,7 +739,7 @@
    1.87    "!!A P. (~(ALL x:A. P x)) = (EX x:A. ~P x)"
    1.88    by auto
    1.89  
    1.90 -lemma bex_simps [simp,noatp]:
    1.91 +lemma bex_simps [simp,no_atp]:
    1.92    "!!A P Q. (EX x:A. P x & Q) = ((EX x:A. P x) & Q)"
    1.93    "!!A P Q. (EX x:A. P & Q x) = (P & (EX x:A. Q x))"
    1.94    "!!P. (EX x:{}. P x) = False"