diff -r 066bb557570f -r 7619080e49f0 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Wed Aug 15 09:02:11 2007 +0200 +++ b/src/HOL/Finite_Set.thy Wed Aug 15 12:52:56 2007 +0200 @@ -1507,7 +1507,7 @@ lemma card_empty [simp]: "card {} = 0" by (simp add: card_def) -lemma card_infinite [simp]: "~ finite A ==> card A = 0" +lemma card_infinite [simp,noatp]: "~ finite A ==> card A = 0" by (simp add: card_def) lemma card_eq_setsum: "card A = setsum (%x. 1) A" @@ -1521,7 +1521,7 @@ "finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))" by (simp add: insert_absorb) -lemma card_0_eq [simp]: "finite A ==> (card A = 0) = (A = {})" +lemma card_0_eq [simp,noatp]: "finite A ==> (card A = 0) = (A = {})" apply auto apply (drule_tac a = x in mk_disjoint_insert, clarify, auto) done @@ -2034,7 +2034,7 @@ then show ?thesis by (simp add: below_def) qed -lemma below_f_conv [simp]: "x \ y \ z = (x \ y \ x \ z)" +lemma below_f_conv [simp,noatp]: "x \ y \ z = (x \ y \ x \ z)" proof assume "x \ y \ z" hence xyzx: "x \ (y \ z) = x" by(simp add: below_def) @@ -2099,7 +2099,7 @@ qed qed -lemma strict_below_f_conv[simp]: "x \ y \ z = (x \ y \ x \ z)" +lemma strict_below_f_conv[simp,noatp]: "x \ y \ z = (x \ y \ x \ z)" apply(simp add: strict_below_def) using lin[of y z] by (auto simp:below_def ACI) @@ -2575,12 +2575,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]: +lemma Min_in [simp,noatp]: shows "finite A \ A \ {} \ Min A \ A" using ACf.fold1_in [OF ACf_min] by (fastsimp simp: Min_def min_def) -lemma Max_in [simp]: +lemma Max_in [simp,noatp]: shows "finite A \ A \ {} \ Max A \ A" using ACf.fold1_in [OF ACf_max] by (fastsimp simp: Max_def max_def) @@ -2591,41 +2591,41 @@ lemma Max_mono: "\ M \ N; M \ {}; finite N \ \ Max M \<^loc>\ Max N" by (simp add: Max_def ACIfSLlin.fold1_antimono [OF ACIfSLlin_max]) -lemma Min_le [simp]: "\ finite A; A \ {}; x \ A \ \ Min A \<^loc>\ x" +lemma Min_le [simp,noatp]: "\ finite A; A \ {}; x \ A \ \ Min A \<^loc>\ x" by (simp add: Min_def ACIfSL.fold1_belowI [OF ACIfSL_min]) -lemma Max_ge [simp]: "\ finite A; A \ {}; x \ A \ \ x \<^loc>\ Max A" +lemma Max_ge [simp,noatp]: "\ finite A; A \ {}; x \ A \ \ x \<^loc>\ Max A" by (simp add: Max_def ACIfSL.fold1_belowI [OF ACIfSL_max]) -lemma Min_ge_iff [simp]: +lemma Min_ge_iff [simp,noatp]: "\ finite A; A \ {} \ \ x \<^loc>\ Min A \ (\a\A. x \<^loc>\ a)" by (simp add: Min_def ACIfSL.below_fold1_iff [OF ACIfSL_min]) -lemma Max_le_iff [simp]: +lemma Max_le_iff [simp,noatp]: "\ finite A; A \ {} \ \ Max A \<^loc>\ x \ (\a\A. a \<^loc>\ x)" by (simp add: Max_def ACIfSL.below_fold1_iff [OF ACIfSL_max]) -lemma Min_gr_iff [simp]: +lemma Min_gr_iff [simp,noatp]: "\ finite A; A \ {} \ \ x \<^loc>< Min A \ (\a\A. x \<^loc>< a)" by (simp add: Min_def ACIfSLlin.strict_below_fold1_iff [OF ACIfSLlin_min]) -lemma Max_less_iff [simp]: +lemma Max_less_iff [simp,noatp]: "\ finite A; A \ {} \ \ Max A \<^loc>< x \ (\a\A. a \<^loc>< x)" by (simp add: Max_def ACIfSLlin.strict_below_fold1_iff [OF ACIfSLlin_max]) -lemma Min_le_iff: +lemma Min_le_iff [noatp]: "\ finite A; A \ {} \ \ Min A \<^loc>\ x \ (\a\A. a \<^loc>\ x)" by (simp add: Min_def ACIfSLlin.fold1_below_iff [OF ACIfSLlin_min]) -lemma Max_ge_iff: +lemma Max_ge_iff [noatp]: "\ finite A; A \ {} \ \ x \<^loc>\ Max A \ (\a\A. x \<^loc>\ a)" by (simp add: Max_def ACIfSLlin.fold1_below_iff [OF ACIfSLlin_max]) -lemma Min_less_iff: +lemma Min_less_iff [noatp]: "\ finite A; A \ {} \ \ Min A \<^loc>< x \ (\a\A. a \<^loc>< x)" by (simp add: Min_def ACIfSLlin.fold1_strict_below_iff [OF ACIfSLlin_min]) -lemma Max_gr_iff: +lemma Max_gr_iff [noatp]: "\ finite A; A \ {} \ \ x \<^loc>< Max A \ (\a\A. x \<^loc>< a)" by (simp add: Max_def ACIfSLlin.fold1_strict_below_iff [OF ACIfSLlin_max])