src/HOL/Set.thy
changeset 35828 46cfc4b8112e
parent 35576 5f6bd3ac99f9
child 36009 9cdbc5ffc15c
     1.1 --- a/src/HOL/Set.thy	Wed Mar 17 19:37:44 2010 +0100
     1.2 +++ b/src/HOL/Set.thy	Thu Mar 18 12:58:52 2010 +0100
     1.3 @@ -462,7 +462,7 @@
     1.4    unfolding mem_def by (erule le_funE, erule le_boolE)
     1.5    -- {* Rule in Modus Ponens style. *}
     1.6  
     1.7 -lemma rev_subsetD [noatp,intro?]: "c \<in> A ==> A \<subseteq> B ==> c \<in> B"
     1.8 +lemma rev_subsetD [no_atp,intro?]: "c \<in> A ==> A \<subseteq> B ==> c \<in> B"
     1.9    -- {* The same, with reversed premises for use with @{text erule} --
    1.10        cf @{text rev_mp}. *}
    1.11    by (rule subsetD)
    1.12 @@ -471,13 +471,13 @@
    1.13    \medskip Converts @{prop "A \<subseteq> B"} to @{prop "x \<in> A ==> x \<in> B"}.
    1.14  *}
    1.15  
    1.16 -lemma subsetCE [noatp,elim]: "A \<subseteq> B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
    1.17 +lemma subsetCE [no_atp,elim]: "A \<subseteq> B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
    1.18    -- {* Classical elimination rule. *}
    1.19    unfolding mem_def by (blast dest: le_funE le_boolE)
    1.20  
    1.21 -lemma subset_eq [noatp]: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
    1.22 +lemma subset_eq [no_atp]: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
    1.23  
    1.24 -lemma contra_subsetD [noatp]: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
    1.25 +lemma contra_subsetD [no_atp]: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
    1.26    by blast
    1.27  
    1.28  lemma subset_refl [simp]: "A \<subseteq> A"
    1.29 @@ -791,11 +791,11 @@
    1.30  
    1.31  subsubsection {* Singletons, using insert *}
    1.32  
    1.33 -lemma singletonI [intro!,noatp]: "a : {a}"
    1.34 +lemma singletonI [intro!,no_atp]: "a : {a}"
    1.35      -- {* Redundant? But unlike @{text insertCI}, it proves the subgoal immediately! *}
    1.36    by (rule insertI1)
    1.37  
    1.38 -lemma singletonD [dest!,noatp]: "b : {a} ==> b = a"
    1.39 +lemma singletonD [dest!,no_atp]: "b : {a} ==> b = a"
    1.40    by blast
    1.41  
    1.42  lemmas singletonE = singletonD [elim_format]
    1.43 @@ -806,11 +806,11 @@
    1.44  lemma singleton_inject [dest!]: "{a} = {b} ==> a = b"
    1.45    by blast
    1.46  
    1.47 -lemma singleton_insert_inj_eq [iff,noatp]:
    1.48 +lemma singleton_insert_inj_eq [iff,no_atp]:
    1.49       "({b} = insert a A) = (a = b & A \<subseteq> {b})"
    1.50    by blast
    1.51  
    1.52 -lemma singleton_insert_inj_eq' [iff,noatp]:
    1.53 +lemma singleton_insert_inj_eq' [iff,no_atp]:
    1.54       "(insert a A = {b}) = (a = b & A \<subseteq> {b})"
    1.55    by blast
    1.56  
    1.57 @@ -837,7 +837,7 @@
    1.58  *}
    1.59  
    1.60  definition image :: "('a => 'b) => 'a set => 'b set" (infixr "`" 90) where
    1.61 -  image_def [noatp]: "f ` A = {y. EX x:A. y = f(x)}"
    1.62 +  image_def [no_atp]: "f ` A = {y. EX x:A. y = f(x)}"
    1.63  
    1.64  abbreviation
    1.65    range :: "('a => 'b) => 'b set" where -- "of function"
    1.66 @@ -942,10 +942,10 @@
    1.67  
    1.68  subsubsection {* The ``proper subset'' relation *}
    1.69  
    1.70 -lemma psubsetI [intro!,noatp]: "A \<subseteq> B ==> A \<noteq> B ==> A \<subset> B"
    1.71 +lemma psubsetI [intro!,no_atp]: "A \<subseteq> B ==> A \<noteq> B ==> A \<subset> B"
    1.72    by (unfold less_le) blast
    1.73  
    1.74 -lemma psubsetE [elim!,noatp]: 
    1.75 +lemma psubsetE [elim!,no_atp]: 
    1.76      "[|A \<subset> B;  [|A \<subseteq> B; ~ (B\<subseteq>A)|] ==> R|] ==> R"
    1.77    by (unfold less_le) blast
    1.78  
    1.79 @@ -1102,12 +1102,12 @@
    1.80  lemma insert_inter_insert[simp]: "insert a A \<inter> insert a B = insert a (A \<inter> B)"
    1.81    by blast
    1.82  
    1.83 -lemma insert_disjoint [simp,noatp]:
    1.84 +lemma insert_disjoint [simp,no_atp]:
    1.85   "(insert a A \<inter> B = {}) = (a \<notin> B \<and> A \<inter> B = {})"
    1.86   "({} = insert a A \<inter> B) = (a \<notin> B \<and> {} = A \<inter> B)"
    1.87    by auto
    1.88  
    1.89 -lemma disjoint_insert [simp,noatp]:
    1.90 +lemma disjoint_insert [simp,no_atp]:
    1.91   "(B \<inter> insert a A = {}) = (a \<notin> B \<and> B \<inter> A = {})"
    1.92   "({} = A \<inter> insert b B) = (b \<notin> A \<and> {} = A \<inter> B)"
    1.93    by auto
    1.94 @@ -1139,7 +1139,7 @@
    1.95  by blast
    1.96  
    1.97  
    1.98 -lemma image_Collect [noatp]: "f ` {x. P x} = {f x | x. P x}"
    1.99 +lemma image_Collect [no_atp]: "f ` {x. P x} = {f x | x. P x}"
   1.100    -- {* NOT suitable as a default simprule: the RHS isn't simpler than the LHS,
   1.101        with its implicit quantifier and conjunction.  Also image enjoys better
   1.102        equational properties than does the RHS. *}
   1.103 @@ -1156,7 +1156,7 @@
   1.104  
   1.105  text {* \medskip @{text range}. *}
   1.106  
   1.107 -lemma full_SetCompr_eq [noatp]: "{u. \<exists>x. u = f x} = range f"
   1.108 +lemma full_SetCompr_eq [no_atp]: "{u. \<exists>x. u = f x} = range f"
   1.109    by auto
   1.110  
   1.111  lemma range_composition: "range (\<lambda>x. f (g x)) = f`range g"
   1.112 @@ -1213,7 +1213,7 @@
   1.113  lemma Int_Un_distrib2: "(B \<union> C) \<inter> A = (B \<inter> A) \<union> (C \<inter> A)"
   1.114    by blast
   1.115  
   1.116 -lemma Int_UNIV [simp,noatp]: "(A \<inter> B = UNIV) = (A = UNIV & B = UNIV)"
   1.117 +lemma Int_UNIV [simp,no_atp]: "(A \<inter> B = UNIV) = (A = UNIV & B = UNIV)"
   1.118    by blast
   1.119  
   1.120  lemma Int_subset_iff [simp]: "(C \<subseteq> A \<inter> B) = (C \<subseteq> A & C \<subseteq> B)"
   1.121 @@ -1376,7 +1376,7 @@
   1.122  lemma Diff_eq: "A - B = A \<inter> (-B)"
   1.123    by blast
   1.124  
   1.125 -lemma Diff_eq_empty_iff [simp,noatp]: "(A - B = {}) = (A \<subseteq> B)"
   1.126 +lemma Diff_eq_empty_iff [simp,no_atp]: "(A - B = {}) = (A \<subseteq> B)"
   1.127    by blast
   1.128  
   1.129  lemma Diff_cancel [simp]: "A - A = {}"
   1.130 @@ -1397,7 +1397,7 @@
   1.131  lemma Diff_UNIV [simp]: "A - UNIV = {}"
   1.132    by blast
   1.133  
   1.134 -lemma Diff_insert0 [simp,noatp]: "x \<notin> A ==> A - insert x B = A - B"
   1.135 +lemma Diff_insert0 [simp,no_atp]: "x \<notin> A ==> A - insert x B = A - B"
   1.136    by blast
   1.137  
   1.138  lemma Diff_insert: "A - insert a B = A - B - {a}"
   1.139 @@ -1639,7 +1639,7 @@
   1.140    -- {* monotonicity *}
   1.141    by blast
   1.142  
   1.143 -lemma vimage_image_eq [noatp]: "f -` (f ` A) = {y. EX x:A. f x = f y}"
   1.144 +lemma vimage_image_eq [no_atp]: "f -` (f ` A) = {y. EX x:A. f x = f y}"
   1.145  by (blast intro: sym)
   1.146  
   1.147  lemma image_vimage_subset: "f ` (f -` A) <= A"