src/HOL/Product_Type.thy

 
 constdefs
   Unity :: unit    ("'(')")
   "() == Abs_unit True"
 
-lemma unit_eq: "u = ()"
+lemma unit_eq [noatp]: "u = ()"
   by (induct u) (simp add: unit_def Unity_def)
 
 text {*
   Simplification procedure for @{thm [source] unit_eq}.  Cannot use
   this rule directly --- it loops!

   by simp
 
 lemma unit_all_eq2: "(!!x::unit. PROP P) == PROP P"
   by (rule triv_forall_equality)
 
-lemma unit_induct [induct type: unit]: "P () ==> P x"
+lemma unit_induct [noatp,induct type: unit]: "P () ==> P x"
   by simp
 
 text {*
   This rewrite counters the effect of @{text unit_eq_proc} on @{term
   [source] "%u::unit. f u"}, replacing it by @{term [source]
   f} rather than by @{term [source] "%u. f ()"}.
 *}
 
-lemma unit_abs_eta_conv [simp]: "(%u::unit. f ()) = f"
+lemma unit_abs_eta_conv [simp,noatp]: "(%u::unit. f ()) = f"
   by (rule ext) simp
 
 
 subsection {* Pairs *}
 

 *}
 
 lemma split_beta: "(%(x, y). P x y) z = P (fst z) (snd z)"
   by (subst surjective_pairing, rule split_conv)
 
-lemma split_split: "R (split c p) = (ALL x y. p = (x, y) --> R (c x y))"
+lemma split_split [noatp]: "R(split c p) = (ALL x y. p = (x, y) --> R(c x y))"
   -- {* For use with @{text split} and the Simplifier. *}
   by (insert surj_pair [of p], clarify, simp)
 
 text {*
   @{thm [source] split_split} could be declared as @{text "[split]"}
   done after the Splitter has been speeded up significantly;
   precompute the constants involved and don't do anything unless the
   current goal contains one of those constants.
 *}
 
-lemma split_split_asm: "R (split c p) = (~(EX x y. p = (x, y) & (~R (c x y))))"
+lemma split_split_asm [noatp]: "R (split c p) = (~(EX x y. p = (x, y) & (~R (c x y))))"
 by (subst split_split, simp)
 
 
 text {*
   \medskip @{term split} used as a logical connective or set former.

 (* This prevents applications of splitE for already splitted arguments leading
    to quite time-consuming computations (in particular for nested tuples) *)
 change_claset (fn cs => cs addSbefore ("split_conv_tac", split_conv_tac));
 *}
 
-lemma split_eta_SetCompr [simp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
+lemma split_eta_SetCompr [simp,noatp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
   by (rule ext) fast
 
-lemma split_eta_SetCompr2 [simp]: "(%u. EX x y. u = (x, y) & P x y) = split P"
+lemma split_eta_SetCompr2 [simp,noatp]: "(%u. EX x y. u = (x, y) & P x y) = split P"
   by (rule ext) fast
 
 lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & split Q ab)"
   -- {* Allows simplifications of nested splits in case of independent predicates. *}
   by (rule ext) blast

 lemma UN_Times_distrib:
   "(UN (a,b):(A <*> B). E a <*> F b) = (UNION A E) <*> (UNION B F)"
   -- {* Suggested by Pierre Chartier *}
   by blast
 
-lemma split_paired_Ball_Sigma [simp]:
+lemma split_paired_Ball_Sigma [simp,noatp]:
     "(ALL z: Sigma A B. P z) = (ALL x:A. ALL y: B x. P(x,y))"
   by blast
 
-lemma split_paired_Bex_Sigma [simp]:
+lemma split_paired_Bex_Sigma [simp,noatp]:
     "(EX z: Sigma A B. P z) = (EX x:A. EX y: B x. P(x,y))"
   by blast
 
 lemma Sigma_Un_distrib1: "(SIGMA i:I Un J. C(i)) = (SIGMA i:I. C(i)) Un (SIGMA j:J. C(j))"
   by blast