author haftmann Mon Apr 28 20:21:11 2008 +0200 (2008-04-28) changeset 26757 e775accff967 parent 26756 6634a641b961 child 26758 72af85f6d70b
thms Max_ge, Min_le: dropped superfluous premise
 src/HOL/Finite_Set.thy file | annotate | diff | revisions src/HOL/Hyperreal/SEQ.thy file | annotate | diff | revisions src/HOL/Library/Primes.thy file | annotate | diff | revisions src/HOL/Matrix/MatrixGeneral.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Finite_Set.thy	Mon Apr 28 14:42:13 2008 +0200
1.2 +++ b/src/HOL/Finite_Set.thy	Mon Apr 28 20:21:11 2008 +0200
1.3 @@ -2140,32 +2140,36 @@
1.4  qed
1.5
1.6  lemma fold1_belowI:
1.7 -  assumes "finite A" "A \<noteq> {}"
1.8 +  assumes "finite A"
1.9      and "a \<in> A"
1.10    shows "fold1 inf A \<le> a"
1.11 -using assms proof (induct rule: finite_ne_induct)
1.12 -  case singleton thus ?case by simp
1.13 -next
1.14 -  interpret ab_semigroup_idem_mult [inf]
1.15 -    by (rule ab_semigroup_idem_mult_inf)
1.16 -  case (insert x F)
1.17 -  from insert(5) have "a = x \<or> a \<in> F" by simp
1.18 -  thus ?case
1.19 -  proof
1.20 -    assume "a = x" thus ?thesis using insert
1.21 -      by (simp add: mult_ac_idem)
1.22 +proof -
1.23 +  from assms have "A \<noteq> {}" by auto
1.24 +  from `finite A` `A \<noteq> {}` `a \<in> A` show ?thesis
1.25 +  proof (induct rule: finite_ne_induct)
1.26 +    case singleton thus ?case by simp
1.27    next
1.28 -    assume "a \<in> F"
1.29 -    hence bel: "fold1 inf F \<le> a" by (rule insert)
1.30 -    have "inf (fold1 inf (insert x F)) a = inf x (inf (fold1 inf F) a)"
1.31 -      using insert by (simp add: mult_ac_idem)
1.32 -    also have "inf (fold1 inf F) a = fold1 inf F"
1.33 -      using bel by (auto intro: antisym)
1.34 -    also have "inf x \<dots> = fold1 inf (insert x F)"
1.35 -      using insert by (simp add: mult_ac_idem)
1.36 -    finally have aux: "inf (fold1 inf (insert x F)) a = fold1 inf (insert x F)" .
1.37 -    moreover have "inf (fold1 inf (insert x F)) a \<le> a" by simp
1.38 -    ultimately show ?thesis by simp
1.39 +    interpret ab_semigroup_idem_mult [inf]
1.40 +      by (rule ab_semigroup_idem_mult_inf)
1.41 +    case (insert x F)
1.42 +    from insert(5) have "a = x \<or> a \<in> F" by simp
1.43 +    thus ?case
1.44 +    proof
1.45 +      assume "a = x" thus ?thesis using insert
1.46 +        by (simp add: mult_ac_idem)
1.47 +    next
1.48 +      assume "a \<in> F"
1.49 +      hence bel: "fold1 inf F \<le> a" by (rule insert)
1.50 +      have "inf (fold1 inf (insert x F)) a = inf x (inf (fold1 inf F) a)"
1.51 +        using insert by (simp add: mult_ac_idem)
1.52 +      also have "inf (fold1 inf F) a = fold1 inf F"
1.53 +        using bel by (auto intro: antisym)
1.54 +      also have "inf x \<dots> = fold1 inf (insert x F)"
1.55 +        using insert by (simp add: mult_ac_idem)
1.56 +      finally have aux: "inf (fold1 inf (insert x F)) a = fold1 inf (insert x F)" .
1.57 +      moreover have "inf (fold1 inf (insert x F)) a \<le> a" by simp
1.58 +      ultimately show ?thesis by simp
1.59 +    qed
1.60    qed
1.61  qed
1.62
1.63 @@ -2195,18 +2199,18 @@
1.64  prefer 2 apply blast
1.65  apply(erule exE)
1.66  apply(rule order_trans)
1.67 -apply(erule (2) fold1_belowI)
1.68 -apply(erule (2) lower_semilattice.fold1_belowI [OF dual_lattice])
1.69 +apply(erule (1) fold1_belowI)
1.70 +apply(erule (1) lower_semilattice.fold1_belowI [OF dual_lattice])
1.71  done
1.72
1.73  lemma sup_Inf_absorb [simp]:
1.74 -  "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (sup a (\<Sqinter>\<^bsub>fin\<^esub>A)) = a"
1.75 +  "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a (\<Sqinter>\<^bsub>fin\<^esub>A) = a"
1.76  apply(subst sup_commute)
1.77  apply(simp add: Inf_fin_def sup_absorb2 fold1_belowI)
1.78  done
1.79
1.80  lemma inf_Sup_absorb [simp]:
1.81 -  "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (inf a (\<Squnion>\<^bsub>fin\<^esub>A)) = a"
1.82 +  "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>\<^bsub>fin\<^esub>A) = a"
1.83  by (simp add: Sup_fin_def inf_absorb1
1.84    lower_semilattice.fold1_belowI [OF dual_lattice])
1.85
1.86 @@ -2522,7 +2526,7 @@
1.87  qed
1.88
1.89  lemma Min_le [simp]:
1.90 -  assumes "finite A" and "A \<noteq> {}" and "x \<in> A"
1.91 +  assumes "finite A" and "x \<in> A"
1.92    shows "Min A \<le> x"
1.93  proof -
1.94    interpret lower_semilattice ["op \<le>" "op <" min]
1.95 @@ -2531,7 +2535,7 @@
1.96  qed
1.97
1.98  lemma Max_ge [simp]:
1.99 -  assumes "finite A" and "A \<noteq> {}" and "x \<in> A"
1.100 +  assumes "finite A" and "x \<in> A"
1.101    shows "x \<le> Max A"
1.102  proof -
1.103    invoke lower_semilattice ["op \<ge>" "op >" max]
1.104 @@ -2651,7 +2655,7 @@
1.105    and "finite A" and "P {}"
1.106    and step: "!!A b. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)"
1.107    show "P A"
1.108 -  proof cases
1.109 +  proof (cases "A = {}")
1.110      assume "A = {}" thus "P A" using `P {}` by simp
1.111    next
1.112      let ?B = "A - {Max A}" let ?A = "insert (Max A) ?B"
1.113 @@ -2662,7 +2666,7 @@
1.114      moreover have "finite ?B" using `finite A` by simp
1.115      ultimately have "P ?B" using `P {}` step IH by blast
1.116      moreover have "\<forall>a\<in>?B. a < Max A"
1.117 -      using Max_ge[OF `finite A` `A \<noteq> {}`] by fastsimp
1.118 +      using Max_ge [OF `finite A`] by fastsimp
1.119      ultimately show "P A"
1.120        using A insert_Diff_single step[OF `finite ?B`] by fastsimp
1.121    qed
```
```     2.1 --- a/src/HOL/Hyperreal/SEQ.thy	Mon Apr 28 14:42:13 2008 +0200
2.2 +++ b/src/HOL/Hyperreal/SEQ.thy	Mon Apr 28 20:21:11 2008 +0200
2.3 @@ -73,7 +73,6 @@
2.4  proof (rule BseqI')
2.5    let ?A = "norm ` X ` {..N}"
2.6    have 1: "finite ?A" by simp
2.7 -  have 2: "?A \<noteq> {}" by auto
2.8    fix n::nat
2.9    show "norm (X n) \<le> max K (Max ?A)"
2.10    proof (cases rule: linorder_le_cases)
2.11 @@ -83,7 +82,7 @@
2.12    next
2.13      assume "n \<le> N"
2.14      hence "norm (X n) \<in> ?A" by simp
2.15 -    with 1 2 have "norm (X n) \<le> Max ?A" by (rule Max_ge)
2.16 +    with 1 have "norm (X n) \<le> Max ?A" by (rule Max_ge)
2.17      thus "norm (X n) \<le> max K (Max ?A)" by simp
2.18    qed
2.19  qed
```
```     3.1 --- a/src/HOL/Library/Primes.thy	Mon Apr 28 14:42:13 2008 +0200
3.2 +++ b/src/HOL/Library/Primes.thy	Mon Apr 28 20:21:11 2008 +0200
3.3 @@ -690,9 +690,9 @@
3.4    let ?m = "Max ?P"
3.5    have P0: "?P \<noteq> {}" using two_is_prime by auto
3.6    from H have fP: "finite ?P" using finite_conv_nat_seg_image by blast
3.7 -  from Max_in[OF fP P0]  have "?m \<in> ?P" .
3.8 -  from Max_ge[OF fP P0] have contr: "\<forall> p. prime p \<longrightarrow> p \<le> ?m" by blast
3.9 -  from euclid[of ?m] obtain q where q: "prime q" "q > ?m" by blast
3.10 +  from Max_in [OF fP P0] have "?m \<in> ?P" .
3.11 +  from Max_ge [OF fP] have contr: "\<forall> p. prime p \<longrightarrow> p \<le> ?m" by blast
3.12 +  from euclid [of ?m] obtain q where q: "prime q" "q > ?m" by blast
3.13    with contr show False by auto
3.14  qed
3.15
3.16 @@ -1045,4 +1045,5 @@
3.17
3.18  declare power_Suc0[simp del]
3.19  declare even_dvd[simp del]
3.20 +
3.21  end
```
```     4.1 --- a/src/HOL/Matrix/MatrixGeneral.thy	Mon Apr 28 14:42:13 2008 +0200
4.2 +++ b/src/HOL/Matrix/MatrixGeneral.thy	Mon Apr 28 20:21:11 2008 +0200
4.3 @@ -3,7 +3,9 @@
4.4      Author:     Steven Obua
4.5  *)
4.6
4.7 -theory MatrixGeneral imports Main begin
4.8 +theory MatrixGeneral
4.9 +imports Main
4.10 +begin
4.11
4.12  types 'a infmatrix = "[nat, nat] \<Rightarrow> 'a"
4.13
4.14 @@ -36,12 +38,11 @@
4.15  next
4.16    assume a: "nonzero_positions(Rep_matrix A) \<noteq> {}"
4.17    let ?S = "fst`(nonzero_positions(Rep_matrix A))"
4.18 -  from a have b: "?S \<noteq> {}" by (simp)
4.19    have c: "finite (?S)" by (simp add: finite_nonzero_positions)
4.20    from hyp have d: "Max (?S) < m" by (simp add: a nrows_def)
4.21    have "m \<notin> ?S"
4.22      proof -
4.23 -      have "m \<in> ?S \<Longrightarrow> m <= Max(?S)" by (simp add: Max_ge[OF c b])
4.24 +      have "m \<in> ?S \<Longrightarrow> m <= Max(?S)" by (simp add: Max_ge [OF c])
4.25        moreover from d have "~(m <= Max ?S)" by (simp)
4.26        ultimately show "m \<notin> ?S" by (auto)
4.27      qed
```