summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Mon, 28 Apr 2008 20:21:11 +0200 | |

changeset 26757 | e775accff967 |

parent 26756 | 6634a641b961 |

child 26758 | 72af85f6d70b |

thms Max_ge, Min_le: dropped superfluous premise

--- 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

--- 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

--- 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

--- 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