--- a/src/HOL/Finite_Set.thy Fri Aug 24 14:17:54 2007 +0200
+++ b/src/HOL/Finite_Set.thy Fri Aug 24 14:21:33 2007 +0200
@@ -1507,7 +1507,7 @@
lemma card_empty [simp]: "card {} = 0"
by (simp add: card_def)
-lemma card_infinite [simp,noatp]: "~ finite A ==> card A = 0"
+lemma card_infinite [simp]: "~ finite A ==> card A = 0"
by (simp add: card_def)
lemma card_eq_setsum: "card A = setsum (%x. 1) A"
@@ -2579,12 +2579,12 @@
lemmas Min_insert [simp] = ACIf.fold1_insert_idem_def [OF ACIf_min Min_def]
lemmas Max_insert [simp] = ACIf.fold1_insert_idem_def [OF ACIf_max Max_def]
-lemma Min_in [simp,noatp]:
+lemma Min_in [simp]:
shows "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> Min A \<in> A"
using ACf.fold1_in [OF ACf_min]
by (fastsimp simp: Min_def min_def)
-lemma Max_in [simp,noatp]:
+lemma Max_in [simp]:
shows "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> Max A \<in> A"
using ACf.fold1_in [OF ACf_max]
by (fastsimp simp: Max_def max_def)
@@ -2595,10 +2595,10 @@
lemma Max_mono: "\<lbrakk> M \<subseteq> N; M \<noteq> {}; finite N \<rbrakk> \<Longrightarrow> Max M \<^loc>\<le> Max N"
by (simp add: Max_def ACIfSLlin.fold1_antimono [OF ACIfSLlin_max])
-lemma Min_le [simp,noatp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> Min A \<^loc>\<le> x"
+lemma Min_le [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> Min A \<^loc>\<le> x"
by (simp add: Min_def ACIfSL.fold1_belowI [OF ACIfSL_min])
-lemma Max_ge [simp,noatp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> x \<^loc>\<le> Max A"
+lemma Max_ge [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> x \<^loc>\<le> Max A"
by (simp add: Max_def ACIfSL.fold1_belowI [OF ACIfSL_max])
lemma Min_ge_iff [simp,noatp]:
@@ -2690,7 +2690,7 @@
lemma finite [simp]: "finite (A::'a::finite set)"
by (rule finite_subset [OF subset_UNIV finite_UNIV])
-lemma univ_unit:
+lemma univ_unit [noatp]:
"UNIV = {()}" by auto
instance unit :: finite
@@ -2702,7 +2702,7 @@
lemmas [code func] = univ_unit
-lemma univ_bool:
+lemma univ_bool [noatp]:
"UNIV = {False, True}" by auto
instance bool :: finite
@@ -2723,7 +2723,7 @@
qed
qed
-lemma univ_prod [code func]:
+lemma univ_prod [noatp, code func]:
"UNIV = (UNIV \<Colon> 'a\<Colon>finite set) \<times> (UNIV \<Colon> 'b\<Colon>finite set)"
unfolding UNIV_Times_UNIV ..
@@ -2736,7 +2736,7 @@
thus "finite (UNIV :: ('a + 'b) set)" by simp
qed
-lemma univ_sum [code func]:
+lemma univ_sum [noatp, code func]:
"UNIV = (UNIV \<Colon> 'a\<Colon>finite set) <+> (UNIV \<Colon> 'b\<Colon>finite set)"
unfolding UNIV_Plus_UNIV ..
@@ -2752,7 +2752,7 @@
finally show "finite (UNIV :: 'a option set)" .
qed
-lemma univ_option [code func]:
+lemma univ_option [noatp, code func]:
"UNIV = insert (None \<Colon> 'a\<Colon>finite option) (image Some UNIV)"
unfolding insert_None_conv_UNIV ..
@@ -2764,7 +2764,7 @@
thus "finite (UNIV :: 'a set set)" by simp
qed
-lemma univ_set [code func]:
+lemma univ_set [noatp, code func]:
"UNIV = Pow (UNIV \<Colon> 'a\<Colon>finite set)" unfolding Pow_UNIV ..
lemma inj_graph: "inj (%f. {(x, y). y = f x})"
--- a/src/HOL/Ring_and_Field.thy Fri Aug 24 14:17:54 2007 +0200
+++ b/src/HOL/Ring_and_Field.thy Fri Aug 24 14:21:33 2007 +0200
@@ -994,7 +994,7 @@
field} but none for class @{text field} and @{text nonzero_divides}
because the latter are covered by a simproc. *}
-lemma nonzero_mult_divide_mult_cancel_left[simp]:
+lemma nonzero_mult_divide_mult_cancel_left[simp,noatp]:
assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" shows "(c*a)/(c*b) = a/(b::'a::field)"
proof -
have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"
@@ -1013,7 +1013,7 @@
apply (simp_all add: nonzero_mult_divide_mult_cancel_left)
done
-lemma nonzero_mult_divide_mult_cancel_right:
+lemma nonzero_mult_divide_mult_cancel_right [noatp]:
"[|b\<noteq>0; c\<noteq>0|] ==> (a*c) / (b*c) = a/(b::'a::field)"
by (simp add: mult_commute [of _ c] nonzero_mult_divide_mult_cancel_left)
@@ -1059,34 +1059,34 @@
subsubsection{*Special Cancellation Simprules for Division*}
-lemma mult_divide_mult_cancel_left_if[simp]:
+lemma mult_divide_mult_cancel_left_if[simp,noatp]:
fixes c :: "'a :: {field,division_by_zero}"
shows "(c*a) / (c*b) = (if c=0 then 0 else a/b)"
by (simp add: mult_divide_mult_cancel_left)
-lemma nonzero_mult_divide_cancel_right[simp]:
+lemma nonzero_mult_divide_cancel_right[simp,noatp]:
"b \<noteq> 0 \<Longrightarrow> a * b / b = (a::'a::field)"
using nonzero_mult_divide_mult_cancel_right[of 1 b a] by simp
-lemma nonzero_mult_divide_cancel_left[simp]:
+lemma nonzero_mult_divide_cancel_left[simp,noatp]:
"a \<noteq> 0 \<Longrightarrow> a * b / a = (b::'a::field)"
using nonzero_mult_divide_mult_cancel_left[of 1 a b] by simp
-lemma nonzero_divide_mult_cancel_right[simp]:
+lemma nonzero_divide_mult_cancel_right[simp,noatp]:
"\<lbrakk> a\<noteq>0; b\<noteq>0 \<rbrakk> \<Longrightarrow> b / (a * b) = 1/(a::'a::field)"
using nonzero_mult_divide_mult_cancel_right[of a b 1] by simp
-lemma nonzero_divide_mult_cancel_left[simp]:
+lemma nonzero_divide_mult_cancel_left[simp,noatp]:
"\<lbrakk> a\<noteq>0; b\<noteq>0 \<rbrakk> \<Longrightarrow> a / (a * b) = 1/(b::'a::field)"
using nonzero_mult_divide_mult_cancel_left[of b a 1] by simp
-lemma nonzero_mult_divide_mult_cancel_left2[simp]:
+lemma nonzero_mult_divide_mult_cancel_left2[simp,noatp]:
"[|b\<noteq>0; c\<noteq>0|] ==> (c*a) / (b*c) = a/(b::'a::field)"
using nonzero_mult_divide_mult_cancel_left[of b c a] by(simp add:mult_ac)
-lemma nonzero_mult_divide_mult_cancel_right2[simp]:
+lemma nonzero_mult_divide_mult_cancel_right2[simp,noatp]:
"[|b\<noteq>0; c\<noteq>0|] ==> (a*c) / (c*b) = a/(b::'a::field)"
using nonzero_mult_divide_mult_cancel_right[of b c a] by(simp add:mult_ac)
@@ -2116,7 +2116,7 @@
subsection {* Theorems for proof tools *}
-lemma add_mono_thms_ordered_semiring:
+lemma add_mono_thms_ordered_semiring [noatp]:
fixes i j k :: "'a\<Colon>pordered_ab_semigroup_add"
shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
@@ -2124,7 +2124,7 @@
and "i = j \<and> k = l \<Longrightarrow> i + k = j + l"
by (rule add_mono, clarify+)+
-lemma add_mono_thms_ordered_field:
+lemma add_mono_thms_ordered_field [noatp]:
fixes i j k :: "'a\<Colon>pordered_cancel_ab_semigroup_add"
shows "i < j \<and> k = l \<Longrightarrow> i + k < j + l"
and "i = j \<and> k < l \<Longrightarrow> i + k < j + l"