# HG changeset patch
# User haftmann
# Date 1209406871 -7200
# Node ID e775accff967eaa09103c9181dd13c64d38fc8c6
# Parent  6634a641b961d3aecbb140a20b35005d40ef3970
thms Max_ge, Min_le: dropped superfluous premise

diff -r 6634a641b961 -r e775accff967 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Mon Apr 28 14:42:13 2008 +0200
+++ b/src/HOL/Finite_Set.thy	Mon Apr 28 20:21:11 2008 +0200
@@ -2140,32 +2140,36 @@
 qed
 
 lemma fold1_belowI:
-  assumes "finite A" "A \<noteq> {}"
+  assumes "finite A"
     and "a \<in> A"
   shows "fold1 inf A \<le> a"
-using assms proof (induct rule: finite_ne_induct)
-  case singleton thus ?case by simp
-next
-  interpret ab_semigroup_idem_mult [inf]
-    by (rule ab_semigroup_idem_mult_inf)
-  case (insert x F)
-  from insert(5) have "a = x \<or> a \<in> F" by simp
-  thus ?case
-  proof
-    assume "a = x" thus ?thesis using insert
-      by (simp add: mult_ac_idem)
+proof -
+  from assms have "A \<noteq> {}" by auto
+  from `finite A` `A \<noteq> {}` `a \<in> A` show ?thesis
+  proof (induct rule: finite_ne_induct)
+    case singleton thus ?case by simp
   next
-    assume "a \<in> F"
-    hence bel: "fold1 inf F \<le> a" by (rule insert)
-    have "inf (fold1 inf (insert x F)) a = inf x (inf (fold1 inf F) a)"
-      using insert by (simp add: mult_ac_idem)
-    also have "inf (fold1 inf F) a = fold1 inf F"
-      using bel by (auto intro: antisym)
-    also have "inf x \<dots> = fold1 inf (insert x F)"
-      using insert by (simp add: mult_ac_idem)
-    finally have aux: "inf (fold1 inf (insert x F)) a = fold1 inf (insert x F)" .
-    moreover have "inf (fold1 inf (insert x F)) a \<le> a" by simp
-    ultimately show ?thesis by simp
+    interpret ab_semigroup_idem_mult [inf]
+      by (rule ab_semigroup_idem_mult_inf)
+    case (insert x F)
+    from insert(5) have "a = x \<or> a \<in> F" by simp
+    thus ?case
+    proof
+      assume "a = x" thus ?thesis using insert
+        by (simp add: mult_ac_idem)
+    next
+      assume "a \<in> F"
+      hence bel: "fold1 inf F \<le> a" by (rule insert)
+      have "inf (fold1 inf (insert x F)) a = inf x (inf (fold1 inf F) a)"
+        using insert by (simp add: mult_ac_idem)
+      also have "inf (fold1 inf F) a = fold1 inf F"
+        using bel by (auto intro: antisym)
+      also have "inf x \<dots> = fold1 inf (insert x F)"
+        using insert by (simp add: mult_ac_idem)
+      finally have aux: "inf (fold1 inf (insert x F)) a = fold1 inf (insert x F)" .
+      moreover have "inf (fold1 inf (insert x F)) a \<le> a" by simp
+      ultimately show ?thesis by simp
+    qed
   qed
 qed
 
@@ -2195,18 +2199,18 @@
 prefer 2 apply blast
 apply(erule exE)
 apply(rule order_trans)
-apply(erule (2) fold1_belowI)
-apply(erule (2) lower_semilattice.fold1_belowI [OF dual_lattice])
+apply(erule (1) fold1_belowI)
+apply(erule (1) lower_semilattice.fold1_belowI [OF dual_lattice])
 done
 
 lemma sup_Inf_absorb [simp]:
-  "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (sup a (\<Sqinter>\<^bsub>fin\<^esub>A)) = a"
+  "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a (\<Sqinter>\<^bsub>fin\<^esub>A) = a"
 apply(subst sup_commute)
 apply(simp add: Inf_fin_def sup_absorb2 fold1_belowI)
 done
 
 lemma inf_Sup_absorb [simp]:
-  "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (inf a (\<Squnion>\<^bsub>fin\<^esub>A)) = a"
+  "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>\<^bsub>fin\<^esub>A) = a"
 by (simp add: Sup_fin_def inf_absorb1
   lower_semilattice.fold1_belowI [OF dual_lattice])
 
@@ -2522,7 +2526,7 @@
 qed
 
 lemma Min_le [simp]:
-  assumes "finite A" and "A \<noteq> {}" and "x \<in> A"
+  assumes "finite A" and "x \<in> A"
   shows "Min A \<le> x"
 proof -
   interpret lower_semilattice ["op \<le>" "op <" min]
@@ -2531,7 +2535,7 @@
 qed
 
 lemma Max_ge [simp]:
-  assumes "finite A" and "A \<noteq> {}" and "x \<in> A"
+  assumes "finite A" and "x \<in> A"
   shows "x \<le> Max A"
 proof -
   invoke lower_semilattice ["op \<ge>" "op >" max]
@@ -2651,7 +2655,7 @@
   and "finite A" and "P {}"
   and step: "!!A b. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)"
   show "P A"
-  proof cases
+  proof (cases "A = {}")
     assume "A = {}" thus "P A" using `P {}` by simp
   next
     let ?B = "A - {Max A}" let ?A = "insert (Max A) ?B"
@@ -2662,7 +2666,7 @@
     moreover have "finite ?B" using `finite A` by simp
     ultimately have "P ?B" using `P {}` step IH by blast
     moreover have "\<forall>a\<in>?B. a < Max A"
-      using Max_ge[OF `finite A` `A \<noteq> {}`] by fastsimp
+      using Max_ge [OF `finite A`] by fastsimp
     ultimately show "P A"
       using A insert_Diff_single step[OF `finite ?B`] by fastsimp
   qed
diff -r 6634a641b961 -r e775accff967 src/HOL/Hyperreal/SEQ.thy
--- a/src/HOL/Hyperreal/SEQ.thy	Mon Apr 28 14:42:13 2008 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy	Mon Apr 28 20:21:11 2008 +0200
@@ -73,7 +73,6 @@
 proof (rule BseqI')
   let ?A = "norm ` X ` {..N}"
   have 1: "finite ?A" by simp
-  have 2: "?A \<noteq> {}" by auto
   fix n::nat
   show "norm (X n) \<le> max K (Max ?A)"
   proof (cases rule: linorder_le_cases)
@@ -83,7 +82,7 @@
   next
     assume "n \<le> N"
     hence "norm (X n) \<in> ?A" by simp
-    with 1 2 have "norm (X n) \<le> Max ?A" by (rule Max_ge)
+    with 1 have "norm (X n) \<le> Max ?A" by (rule Max_ge)
     thus "norm (X n) \<le> max K (Max ?A)" by simp
   qed
 qed
diff -r 6634a641b961 -r e775accff967 src/HOL/Library/Primes.thy
--- a/src/HOL/Library/Primes.thy	Mon Apr 28 14:42:13 2008 +0200
+++ b/src/HOL/Library/Primes.thy	Mon Apr 28 20:21:11 2008 +0200
@@ -690,9 +690,9 @@
   let ?m = "Max ?P"
   have P0: "?P \<noteq> {}" using two_is_prime by auto
   from H have fP: "finite ?P" using finite_conv_nat_seg_image by blast 
-  from Max_in[OF fP P0]  have "?m \<in> ?P" . 
-  from Max_ge[OF fP P0] have contr: "\<forall> p. prime p \<longrightarrow> p \<le> ?m" by blast
-  from euclid[of ?m] obtain q where q: "prime q" "q > ?m" by blast
+  from Max_in [OF fP P0] have "?m \<in> ?P" . 
+  from Max_ge [OF fP] have contr: "\<forall> p. prime p \<longrightarrow> p \<le> ?m" by blast
+  from euclid [of ?m] obtain q where q: "prime q" "q > ?m" by blast
   with contr show False by auto
 qed
 
@@ -1045,4 +1045,5 @@
 
 declare power_Suc0[simp del]
 declare even_dvd[simp del]
+
 end
diff -r 6634a641b961 -r e775accff967 src/HOL/Matrix/MatrixGeneral.thy
--- a/src/HOL/Matrix/MatrixGeneral.thy	Mon Apr 28 14:42:13 2008 +0200
+++ b/src/HOL/Matrix/MatrixGeneral.thy	Mon Apr 28 20:21:11 2008 +0200
@@ -3,7 +3,9 @@
     Author:     Steven Obua
 *)
 
-theory MatrixGeneral imports Main begin
+theory MatrixGeneral
+imports Main
+begin
 
 types 'a infmatrix = "[nat, nat] \<Rightarrow> 'a"
 
@@ -36,12 +38,11 @@
 next
   assume a: "nonzero_positions(Rep_matrix A) \<noteq> {}"
   let ?S = "fst`(nonzero_positions(Rep_matrix A))"
-  from a have b: "?S \<noteq> {}" by (simp)
   have c: "finite (?S)" by (simp add: finite_nonzero_positions)
   from hyp have d: "Max (?S) < m" by (simp add: a nrows_def)
   have "m \<notin> ?S"
     proof -
-      have "m \<in> ?S \<Longrightarrow> m <= Max(?S)" by (simp add: Max_ge[OF c b])
+      have "m \<in> ?S \<Longrightarrow> m <= Max(?S)" by (simp add: Max_ge [OF c])
       moreover from d have "~(m <= Max ?S)" by (simp)
       ultimately show "m \<notin> ?S" by (auto)
     qed