src/HOL/Product_Type.thy
changeset 24286 7619080e49f0
parent 24162 8dfd5dd65d82
child 24699 c6674504103f
     1.1 --- a/src/HOL/Product_Type.thy	Wed Aug 15 09:02:11 2007 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Wed Aug 15 12:52:56 2007 +0200
     1.3 @@ -22,7 +22,7 @@
     1.4    Unity :: unit    ("'(')")
     1.5    "() == Abs_unit True"
     1.6  
     1.7 -lemma unit_eq: "u = ()"
     1.8 +lemma unit_eq [noatp]: "u = ()"
     1.9    by (induct u) (simp add: unit_def Unity_def)
    1.10  
    1.11  text {*
    1.12 @@ -46,7 +46,7 @@
    1.13  lemma unit_all_eq2: "(!!x::unit. PROP P) == PROP P"
    1.14    by (rule triv_forall_equality)
    1.15  
    1.16 -lemma unit_induct [induct type: unit]: "P () ==> P x"
    1.17 +lemma unit_induct [noatp,induct type: unit]: "P () ==> P x"
    1.18    by simp
    1.19  
    1.20  text {*
    1.21 @@ -55,7 +55,7 @@
    1.22    f} rather than by @{term [source] "%u. f ()"}.
    1.23  *}
    1.24  
    1.25 -lemma unit_abs_eta_conv [simp]: "(%u::unit. f ()) = f"
    1.26 +lemma unit_abs_eta_conv [simp,noatp]: "(%u::unit. f ()) = f"
    1.27    by (rule ext) simp
    1.28  
    1.29  
    1.30 @@ -443,7 +443,7 @@
    1.31  lemma split_beta: "(%(x, y). P x y) z = P (fst z) (snd z)"
    1.32    by (subst surjective_pairing, rule split_conv)
    1.33  
    1.34 -lemma split_split: "R (split c p) = (ALL x y. p = (x, y) --> R (c x y))"
    1.35 +lemma split_split [noatp]: "R(split c p) = (ALL x y. p = (x, y) --> R(c x y))"
    1.36    -- {* For use with @{text split} and the Simplifier. *}
    1.37    by (insert surj_pair [of p], clarify, simp)
    1.38  
    1.39 @@ -454,7 +454,7 @@
    1.40    current goal contains one of those constants.
    1.41  *}
    1.42  
    1.43 -lemma split_split_asm: "R (split c p) = (~(EX x y. p = (x, y) & (~R (c x y))))"
    1.44 +lemma split_split_asm [noatp]: "R (split c p) = (~(EX x y. p = (x, y) & (~R (c x y))))"
    1.45  by (subst split_split, simp)
    1.46  
    1.47  
    1.48 @@ -525,10 +525,10 @@
    1.49  change_claset (fn cs => cs addSbefore ("split_conv_tac", split_conv_tac));
    1.50  *}
    1.51  
    1.52 -lemma split_eta_SetCompr [simp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
    1.53 +lemma split_eta_SetCompr [simp,noatp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
    1.54    by (rule ext) fast
    1.55  
    1.56 -lemma split_eta_SetCompr2 [simp]: "(%u. EX x y. u = (x, y) & P x y) = split P"
    1.57 +lemma split_eta_SetCompr2 [simp,noatp]: "(%u. EX x y. u = (x, y) & P x y) = split P"
    1.58    by (rule ext) fast
    1.59  
    1.60  lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & split Q ab)"
    1.61 @@ -696,11 +696,11 @@
    1.62    -- {* Suggested by Pierre Chartier *}
    1.63    by blast
    1.64  
    1.65 -lemma split_paired_Ball_Sigma [simp]:
    1.66 +lemma split_paired_Ball_Sigma [simp,noatp]:
    1.67      "(ALL z: Sigma A B. P z) = (ALL x:A. ALL y: B x. P(x,y))"
    1.68    by blast
    1.69  
    1.70 -lemma split_paired_Bex_Sigma [simp]:
    1.71 +lemma split_paired_Bex_Sigma [simp,noatp]:
    1.72      "(EX z: Sigma A B. P z) = (EX x:A. EX y: B x. P(x,y))"
    1.73    by blast
    1.74