# HG changeset patch
# User paulson
# Date 1187958093 -7200
# Node ID bc5cf3b09ff391aa4f3526e96aef9181b473282f
# Parent  d89e409cfe4e3f2cb4ae91087885180d6627c0a8
revised blacklisting for ATP linkup

diff -r d89e409cfe4e -r bc5cf3b09ff3 src/HOL/Finite_Set.thy
--- 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})"
diff -r d89e409cfe4e -r bc5cf3b09ff3 src/HOL/Ring_and_Field.thy
--- 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"