thms Max_ge, Min_le: dropped superfluous premise
authorhaftmann
Mon Apr 28 20:21:11 2008 +0200 (2008-04-28)
changeset 26757e775accff967
parent 26756 6634a641b961
child 26758 72af85f6d70b
thms Max_ge, Min_le: dropped superfluous premise
src/HOL/Finite_Set.thy
src/HOL/Hyperreal/SEQ.thy
src/HOL/Library/Primes.thy
src/HOL/Matrix/MatrixGeneral.thy
     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