tuned proofs: avoid implicit prems;
authorwenzelm
Thu Jun 14 18:33:31 2007 +0200 (2007-06-14)
changeset 23389aaca6a8e5414
parent 23388 77645da0db85
child 23390 01ef1135de73
tuned proofs: avoid implicit prems;
src/HOL/Finite_Set.thy
src/HOL/Groebner_Basis.thy
src/HOL/HOL.thy
src/HOL/Import/HOL4Compat.thy
src/HOL/Inductive.thy
src/HOL/Lattices.thy
src/HOL/Library/SCT_Theorem.thy
src/HOL/NatBin.thy
src/HOL/Numeral.thy
src/HOL/OrderedGroup.thy
src/HOL/Predicate.thy
src/HOL/Presburger.thy
src/HOL/Real/ContNotDenum.thy
src/HOL/Real/PReal.thy
src/HOL/Real/RComplete.thy
src/HOL/Ring_and_Field.thy
src/HOL/Wellfounded_Recursion.thy
src/HOL/ex/CTL.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Thu Jun 14 18:33:29 2007 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Thu Jun 14 18:33:31 2007 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4    assume "finite F"
     1.5    thus "P F"
     1.6    proof induct
     1.7 -    show "P {}" .
     1.8 +    show "P {}" by fact
     1.9      fix x F assume F: "finite F" and P: "P F"
    1.10      show "P (insert x F)"
    1.11      proof cases
    1.12 @@ -61,30 +61,35 @@
    1.13    case (insert x F)
    1.14    show ?case
    1.15    proof cases
    1.16 -    assume "F = {}" thus ?thesis using insert(4) by simp
    1.17 +    assume "F = {}"
    1.18 +    thus ?thesis using `P {x}` by simp
    1.19    next
    1.20 -    assume "F \<noteq> {}" thus ?thesis using insert by blast
    1.21 +    assume "F \<noteq> {}"
    1.22 +    thus ?thesis using insert by blast
    1.23    qed
    1.24  qed
    1.25  
    1.26  lemma finite_subset_induct [consumes 2, case_names empty insert]:
    1.27 -  "finite F ==> F \<subseteq> A ==>
    1.28 -    P {} ==> (!!a F. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)) ==>
    1.29 -    P F"
    1.30 +  assumes "finite F" and "F \<subseteq> A"
    1.31 +    and empty: "P {}"
    1.32 +    and insert: "!!a F. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)"
    1.33 +  shows "P F"
    1.34  proof -
    1.35 -  assume "P {}" and insert:
    1.36 -    "!!a F. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)"
    1.37 -  assume "finite F"
    1.38 -  thus "F \<subseteq> A ==> P F"
    1.39 +  from `finite F` and `F \<subseteq> A`
    1.40 +  show ?thesis
    1.41    proof induct
    1.42 -    show "P {}" .
    1.43 -    fix x F assume "finite F" and "x \<notin> F"
    1.44 -      and P: "F \<subseteq> A ==> P F" and i: "insert x F \<subseteq> A"
    1.45 +    show "P {}" by fact
    1.46 +  next
    1.47 +    fix x F
    1.48 +    assume "finite F" and "x \<notin> F" and
    1.49 +      P: "F \<subseteq> A ==> P F" and i: "insert x F \<subseteq> A"
    1.50      show "P (insert x F)"
    1.51      proof (rule insert)
    1.52        from i show "x \<in> A" by blast
    1.53        from i have "F \<subseteq> A" by blast
    1.54        with P show "P F" .
    1.55 +      show "finite F" by fact
    1.56 +      show "x \<notin> F" by fact
    1.57      qed
    1.58    qed
    1.59  qed
    1.60 @@ -102,7 +107,7 @@
    1.61    qed
    1.62  next
    1.63    case (insert a A)
    1.64 -  have notinA: "a \<notin> A" .
    1.65 +  have notinA: "a \<notin> A" by fact
    1.66    from insert.hyps obtain n f
    1.67      where "A = f ` {i::nat. i < n}" "inj_on f {i. i < n}" by blast
    1.68    hence "insert a A = f(n:=a) ` {i. i < Suc n}"
    1.69 @@ -151,17 +156,17 @@
    1.70      thus ?case by simp
    1.71    next
    1.72      case (insert x F A)
    1.73 -    have A: "A \<subseteq> insert x F" and r: "A - {x} \<subseteq> F ==> finite (A - {x})" .
    1.74 +    have A: "A \<subseteq> insert x F" and r: "A - {x} \<subseteq> F ==> finite (A - {x})" by fact+
    1.75      show "finite A"
    1.76      proof cases
    1.77        assume x: "x \<in> A"
    1.78        with A have "A - {x} \<subseteq> F" by (simp add: subset_insert_iff)
    1.79        with r have "finite (A - {x})" .
    1.80        hence "finite (insert x (A - {x}))" ..
    1.81 -      also have "insert x (A - {x}) = A" by (rule insert_Diff)
    1.82 +      also have "insert x (A - {x}) = A" using x by (rule insert_Diff)
    1.83        finally show ?thesis .
    1.84      next
    1.85 -      show "A \<subseteq> F ==> ?thesis" .
    1.86 +      show "A \<subseteq> F ==> ?thesis" by fact
    1.87        assume "x \<notin> A"
    1.88        with A show "A \<subseteq> F" by (simp add: subset_insert_iff)
    1.89      qed
    1.90 @@ -188,35 +193,37 @@
    1.91  by (induct rule:finite_induct) simp_all
    1.92  
    1.93  lemma finite_empty_induct:
    1.94 -  "finite A ==>
    1.95 -  P A ==> (!!a A. finite A ==> a:A ==> P A ==> P (A - {a})) ==> P {}"
    1.96 +  assumes "finite A"
    1.97 +    and "P A"
    1.98 +    and "!!a A. finite A ==> a:A ==> P A ==> P (A - {a})"
    1.99 +  shows "P {}"
   1.100  proof -
   1.101 -  assume "finite A"
   1.102 -    and "P A" and "!!a A. finite A ==> a:A ==> P A ==> P (A - {a})"
   1.103    have "P (A - A)"
   1.104    proof -
   1.105 -    fix c b :: "'a set"
   1.106 -    presume c: "finite c" and b: "finite b"
   1.107 -      and P1: "P b" and P2: "!!x y. finite y ==> x \<in> y ==> P y ==> P (y - {x})"
   1.108 -    from c show "c \<subseteq> b ==> P (b - c)"
   1.109 -    proof induct
   1.110 -      case empty
   1.111 -      from P1 show ?case by simp
   1.112 -    next
   1.113 -      case (insert x F)
   1.114 -      have "P (b - F - {x})"
   1.115 -      proof (rule P2)
   1.116 -        from _ b show "finite (b - F)" by (rule finite_subset) blast
   1.117 -        from insert show "x \<in> b - F" by simp
   1.118 -        from insert show "P (b - F)" by simp
   1.119 +    {
   1.120 +      fix c b :: "'a set"
   1.121 +      assume c: "finite c" and b: "finite b"
   1.122 +	and P1: "P b" and P2: "!!x y. finite y ==> x \<in> y ==> P y ==> P (y - {x})"
   1.123 +      have "c \<subseteq> b ==> P (b - c)"
   1.124 +	using c
   1.125 +      proof induct
   1.126 +	case empty
   1.127 +	from P1 show ?case by simp
   1.128 +      next
   1.129 +	case (insert x F)
   1.130 +	have "P (b - F - {x})"
   1.131 +	proof (rule P2)
   1.132 +          from _ b show "finite (b - F)" by (rule finite_subset) blast
   1.133 +          from insert show "x \<in> b - F" by simp
   1.134 +          from insert show "P (b - F)" by simp
   1.135 +	qed
   1.136 +	also have "b - F - {x} = b - insert x F" by (rule Diff_insert [symmetric])
   1.137 +	finally show ?case .
   1.138        qed
   1.139 -      also have "b - F - {x} = b - insert x F" by (rule Diff_insert [symmetric])
   1.140 -      finally show ?case .
   1.141 -    qed
   1.142 -  next
   1.143 -    show "A \<subseteq> A" ..
   1.144 +    }
   1.145 +    then show ?thesis by this (simp_all add: assms)
   1.146    qed
   1.147 -  thus "P {}" by simp
   1.148 +  then show ?thesis by simp
   1.149  qed
   1.150  
   1.151  lemma finite_Diff [simp]: "finite B ==> finite (B - Ba)"
   1.152 @@ -526,7 +533,7 @@
   1.153    case 0 thus ?thesis using aA by auto
   1.154  next
   1.155    case (Suc m)
   1.156 -  have nSuc: "n = Suc m" . 
   1.157 +  have nSuc: "n = Suc m" by fact
   1.158    have mlessn: "m<n" by (simp add: nSuc)
   1.159    from aA obtain k where hkeq: "h k = a" and klessn: "k<n" by (blast elim!: equalityE)
   1.160    let ?hm = "swap k m h"
   1.161 @@ -557,9 +564,9 @@
   1.162    case (less n)
   1.163      have IH: "!!m h A x x'. 
   1.164                 \<lbrakk>m<n; A = h ` {i. i<m}; inj_on h {i. i<m}; 
   1.165 -                foldSet f g z A x; foldSet f g z A x'\<rbrakk> \<Longrightarrow> x' = x" .
   1.166 +                foldSet f g z A x; foldSet f g z A x'\<rbrakk> \<Longrightarrow> x' = x" by fact
   1.167      have Afoldx: "foldSet f g z A x" and Afoldx': "foldSet f g z A x'"
   1.168 -     and A: "A = h`{i. i<n}" and injh: "inj_on h {i. i<n}" .
   1.169 +     and A: "A = h`{i. i<n}" and injh: "inj_on h {i. i<n}" by fact+
   1.170      show ?case
   1.171      proof (rule foldSet.cases [OF Afoldx])
   1.172        assume "A = {}" and "x = z"
     2.1 --- a/src/HOL/Groebner_Basis.thy	Thu Jun 14 18:33:29 2007 +0200
     2.2 +++ b/src/HOL/Groebner_Basis.thy	Thu Jun 14 18:33:31 2007 +0200
     2.3 @@ -163,7 +163,7 @@
     2.4  lemma "axioms" [normalizer
     2.5      semiring ops: semiring_ops
     2.6      semiring rules: semiring_rules]:
     2.7 -  "gb_semiring add mul pwr r0 r1" .
     2.8 +  "gb_semiring add mul pwr r0 r1" by fact
     2.9  
    2.10  end
    2.11  
    2.12 @@ -232,7 +232,7 @@
    2.13    semiring rules: semiring_rules
    2.14    ring ops: ring_ops
    2.15    ring rules: ring_rules]:
    2.16 -  "gb_ring add mul pwr r0 r1 sub neg" .
    2.17 +  "gb_ring add mul pwr r0 r1 sub neg" by fact
    2.18  
    2.19  end
    2.20  
    2.21 @@ -273,7 +273,7 @@
    2.22    semiring rules: semiring_rules
    2.23    ring ops: ring_ops
    2.24    ring rules: ring_rules]:
    2.25 -  "gb_field add mul pwr r0 r1 sub neg divide inverse" .
    2.26 +  "gb_field add mul pwr r0 r1 sub neg divide inverse" by fact
    2.27  
    2.28  end
    2.29  
    2.30 @@ -311,7 +311,7 @@
    2.31    semiring ops: semiring_ops
    2.32    semiring rules: semiring_rules
    2.33    idom rules: noteq_reduce add_scale_eq_noteq]:
    2.34 -  "semiringb add mul pwr r0 r1" .
    2.35 +  "semiringb add mul pwr r0 r1" by fact
    2.36  
    2.37  end
    2.38  
    2.39 @@ -326,7 +326,7 @@
    2.40    ring ops: ring_ops
    2.41    ring rules: ring_rules
    2.42    idom rules: noteq_reduce add_scale_eq_noteq]:
    2.43 -  "ringb add mul pwr r0 r1 sub neg" .
    2.44 +  "ringb add mul pwr r0 r1 sub neg" by fact
    2.45  
    2.46  end
    2.47  
     3.1 --- a/src/HOL/HOL.thy	Thu Jun 14 18:33:29 2007 +0200
     3.2 +++ b/src/HOL/HOL.thy	Thu Jun 14 18:33:31 2007 +0200
     3.3 @@ -768,7 +768,7 @@
     3.4  lemma atomize_all [atomize]: "(!!x. P x) == Trueprop (ALL x. P x)"
     3.5  proof
     3.6    assume "!!x. P x"
     3.7 -  show "ALL x. P x" by (rule allI)
     3.8 +  then show "ALL x. P x" ..
     3.9  next
    3.10    assume "ALL x. P x"
    3.11    thus "!!x. P x" by (rule allE)
    3.12 @@ -1219,11 +1219,11 @@
    3.13  
    3.14  lemma True_implies_equals: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
    3.15  proof
    3.16 -  assume prem: "True \<Longrightarrow> PROP P"
    3.17 -  from prem [OF TrueI] show "PROP P" . 
    3.18 +  assume "True \<Longrightarrow> PROP P"
    3.19 +  from this [OF TrueI] show "PROP P" .
    3.20  next
    3.21    assume "PROP P"
    3.22 -  show "PROP P" .
    3.23 +  then show "PROP P" .
    3.24  qed
    3.25  
    3.26  lemma ex_simps:
     4.1 --- a/src/HOL/Import/HOL4Compat.thy	Thu Jun 14 18:33:29 2007 +0200
     4.2 +++ b/src/HOL/Import/HOL4Compat.thy	Thu Jun 14 18:33:31 2007 +0200
     4.3 @@ -157,7 +157,7 @@
     4.4      fix k
     4.5      show "!q. q + k = m \<longrightarrow> P q"
     4.6      proof (induct k,simp_all)
     4.7 -      show "P m" .
     4.8 +      show "P m" by fact
     4.9      next
    4.10        fix k
    4.11        assume ind: "!q. q + k = m \<longrightarrow> P q"
    4.12 @@ -406,7 +406,7 @@
    4.13    assume allt: "!t. P t \<longrightarrow> (!h. P (h # t))"
    4.14    show "P l"
    4.15    proof (induct l)
    4.16 -    show "P []" .
    4.17 +    show "P []" by fact
    4.18    next
    4.19      fix h t
    4.20      assume "P t"
     5.1 --- a/src/HOL/Inductive.thy	Thu Jun 14 18:33:29 2007 +0200
     5.2 +++ b/src/HOL/Inductive.thy	Thu Jun 14 18:33:31 2007 +0200
     5.3 @@ -89,7 +89,7 @@
     5.4    then show P ..
     5.5  next
     5.6    assume "\<And>P\<Colon>bool. P"
     5.7 -  then show False ..
     5.8 +  then show False .
     5.9  qed
    5.10  
    5.11  lemma not_eq_False:
     6.1 --- a/src/HOL/Lattices.thy	Thu Jun 14 18:33:29 2007 +0200
     6.2 +++ b/src/HOL/Lattices.thy	Thu Jun 14 18:33:31 2007 +0200
     6.3 @@ -259,7 +259,7 @@
     6.4    and greatest: "\<And>x y z. x \<^loc>\<le> y \<Longrightarrow> x \<^loc>\<le> z \<Longrightarrow> x \<^loc>\<le> y \<triangle> z"
     6.5    shows "x \<sqinter> y = x \<triangle> y"
     6.6  proof (rule antisym)
     6.7 -  show "x \<triangle> y \<^loc>\<le> x \<sqinter> y" by (rule le_infI) (rule le1 le2)
     6.8 +  show "x \<triangle> y \<^loc>\<le> x \<sqinter> y" by (rule le_infI) (rule le1, rule le2)
     6.9  next
    6.10    have leI: "\<And>x y z. x \<^loc>\<le> y \<Longrightarrow> x \<^loc>\<le> z \<Longrightarrow> x \<^loc>\<le> y \<triangle> z" by (blast intro: greatest)
    6.11    show "x \<sqinter> y \<^loc>\<le> x \<triangle> y" by (rule leI) simp_all
    6.12 @@ -271,7 +271,7 @@
    6.13    and least: "\<And>x y z. y \<^loc>\<le> x \<Longrightarrow> z \<^loc>\<le> x \<Longrightarrow> y \<nabla> z \<^loc>\<le> x"
    6.14    shows "x \<squnion> y = x \<nabla> y"
    6.15  proof (rule antisym)
    6.16 -  show "x \<squnion> y \<^loc>\<le> x \<nabla> y" by (rule le_supI) (rule ge1 ge2)
    6.17 +  show "x \<squnion> y \<^loc>\<le> x \<nabla> y" by (rule le_supI) (rule ge1, rule ge2)
    6.18  next
    6.19    have leI: "\<And>x y z. x \<^loc>\<le> z \<Longrightarrow> y \<^loc>\<le> z \<Longrightarrow> x \<nabla> y \<^loc>\<le> z" by (blast intro: least)
    6.20    show "x \<nabla> y \<^loc>\<le> x \<squnion> y" by (rule leI) simp_all
     7.1 --- a/src/HOL/Library/SCT_Theorem.thy	Thu Jun 14 18:33:29 2007 +0200
     7.2 +++ b/src/HOL/Library/SCT_Theorem.thy	Thu Jun 14 18:33:31 2007 +0200
     7.3 @@ -1139,12 +1139,12 @@
     7.4         (auto simp:index_less)
     7.5    then obtain T i
     7.6      where inf: "infinite T"
     7.7 -    and "i < length l"
     7.8 +    and i: "i < length l"
     7.9      and d: "\<And>x y. \<lbrakk>x \<in> T; y\<in>T; x \<noteq> y\<rbrakk>
    7.10      \<Longrightarrow> index_of l (f (set2pair {x, y})) = i"
    7.11      by auto
    7.12  
    7.13 -  have  "l ! i \<in> S" unfolding S
    7.14 +  have "l ! i \<in> S" unfolding S using i
    7.15      by (rule nth_mem)
    7.16    moreover
    7.17    have "\<And>x y. x \<in> T \<Longrightarrow> y\<in>T \<Longrightarrow> x < y
     8.1 --- a/src/HOL/NatBin.thy	Thu Jun 14 18:33:29 2007 +0200
     8.2 +++ b/src/HOL/NatBin.thy	Thu Jun 14 18:33:31 2007 +0200
     8.3 @@ -376,13 +376,13 @@
     8.4       "(a::'a::{ordered_idom,recpower}) < 0 ==> a ^ Suc(2*n) < 0"
     8.5  proof (induct "n")
     8.6    case 0
     8.7 -    show ?case by (simp add: Power.power_Suc)
     8.8 +  then show ?case by (simp add: Power.power_Suc)
     8.9  next
    8.10    case (Suc n)
    8.11 -    have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)" 
    8.12 -      by (simp add: mult_ac power_add power2_eq_square Power.power_Suc)
    8.13 -    thus ?case
    8.14 -      by (simp add: prems mult_less_0_iff mult_neg_neg)
    8.15 +  have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)" 
    8.16 +    by (simp add: mult_ac power_add power2_eq_square Power.power_Suc)
    8.17 +  thus ?case
    8.18 +    by (simp add: prems mult_less_0_iff mult_neg_neg)
    8.19  qed
    8.20  
    8.21  lemma odd_0_le_power_imp_0_le:
     9.1 --- a/src/HOL/Numeral.thy	Thu Jun 14 18:33:29 2007 +0200
     9.2 +++ b/src/HOL/Numeral.thy	Thu Jun 14 18:33:31 2007 +0200
     9.3 @@ -339,7 +339,7 @@
     9.4    assumes le: "0 \<le> z"
     9.5    shows "(0::int) < 1 + z"
     9.6  proof -
     9.7 -  have "0 \<le> z" .
     9.8 +  have "0 \<le> z" by fact
     9.9    also have "... < z + 1" by (rule less_add_one) 
    9.10    also have "... = 1 + z" by (simp add: add_ac)
    9.11    finally show "0 < 1 + z" .
    10.1 --- a/src/HOL/OrderedGroup.thy	Thu Jun 14 18:33:29 2007 +0200
    10.2 +++ b/src/HOL/OrderedGroup.thy	Thu Jun 14 18:33:31 2007 +0200
    10.3 @@ -377,10 +377,10 @@
    10.4  subsection {* Ordering Rules for Unary Minus *}
    10.5  
    10.6  lemma le_imp_neg_le:
    10.7 -      assumes "a \<le> (b::'a::{pordered_ab_semigroup_add_imp_le, ab_group_add})" shows "-b \<le> -a"
    10.8 +  assumes "a \<le> (b::'a::{pordered_ab_semigroup_add_imp_le, ab_group_add})" shows "-b \<le> -a"
    10.9  proof -
   10.10    have "-a+a \<le> -a+b"
   10.11 -    by (rule add_left_mono) 
   10.12 +    using `a \<le> b` by (rule add_left_mono) 
   10.13    hence "0 \<le> -a+b"
   10.14      by simp
   10.15    hence "0 + (-b) \<le> (-a + b) + (-b)"
    11.1 --- a/src/HOL/Predicate.thy	Thu Jun 14 18:33:29 2007 +0200
    11.2 +++ b/src/HOL/Predicate.thy	Thu Jun 14 18:33:31 2007 +0200
    11.3 @@ -34,11 +34,11 @@
    11.4  proof
    11.5    fix S
    11.6    assume "!!S. PROP P S"
    11.7 -  show "PROP P (Collect S)" .
    11.8 +  then show "PROP P (Collect S)" .
    11.9  next
   11.10    fix S
   11.11    assume "!!S. PROP P (Collect S)"
   11.12 -  have "PROP P {x. x : S}" .
   11.13 +  then have "PROP P {x. x : S}" .
   11.14    thus "PROP P S" by simp
   11.15  qed
   11.16  
   11.17 @@ -46,11 +46,11 @@
   11.18  proof
   11.19    fix S
   11.20    assume "!!S. PROP P S"
   11.21 -  show "PROP P (member S)" .
   11.22 +  then show "PROP P (member S)" .
   11.23  next
   11.24    fix S
   11.25    assume "!!S. PROP P (member S)"
   11.26 -  have "PROP P (member {x. S x})" .
   11.27 +  then have "PROP P (member {x. S x})" .
   11.28    thus "PROP P S" by simp
   11.29  qed
   11.30  
   11.31 @@ -96,11 +96,11 @@
   11.32  proof
   11.33    fix S
   11.34    assume "!!S. PROP P S"
   11.35 -  show "PROP P (Collect2 S)" .
   11.36 +  then show "PROP P (Collect2 S)" .
   11.37  next
   11.38    fix S
   11.39    assume "!!S. PROP P (Collect2 S)"
   11.40 -  have "PROP P (Collect2 (member2 S))" .
   11.41 +  then have "PROP P (Collect2 (member2 S))" .
   11.42    thus "PROP P S" by simp
   11.43  qed
   11.44  
   11.45 @@ -108,11 +108,11 @@
   11.46  proof
   11.47    fix S
   11.48    assume "!!S. PROP P S"
   11.49 -  show "PROP P (member2 S)" .
   11.50 +  then show "PROP P (member2 S)" .
   11.51  next
   11.52    fix S
   11.53    assume "!!S. PROP P (member2 S)"
   11.54 -  have "PROP P (member2 (Collect2 S))" .
   11.55 +  then have "PROP P (member2 (Collect2 S))" .
   11.56    thus "PROP P S" by simp
   11.57  qed
   11.58  
    12.1 --- a/src/HOL/Presburger.thy	Thu Jun 14 18:33:29 2007 +0200
    12.2 +++ b/src/HOL/Presburger.thy	Thu Jun 14 18:33:31 2007 +0200
    12.3 @@ -200,8 +200,8 @@
    12.4      have "P(x mod d)" using dpos P Pmod by(simp add:pos_mod_sign pos_mod_bound)
    12.5      moreover have "x mod d : {1..d}"
    12.6      proof -
    12.7 -      have "0 \<le> x mod d" by(rule pos_mod_sign)
    12.8 -      moreover have "x mod d < d" by(rule pos_mod_bound)
    12.9 +      from dpos have "0 \<le> x mod d" by(rule pos_mod_sign)
   12.10 +      moreover from dpos have "x mod d < d" by(rule pos_mod_bound)
   12.11        ultimately show ?thesis using not0 by(simp add:atLeastAtMost_iff)
   12.12      qed
   12.13      ultimately show ?RHS ..
   12.14 @@ -243,7 +243,7 @@
   12.15  qed
   12.16  
   12.17  lemma  minusinfinity:
   12.18 -  assumes "0 < d" and
   12.19 +  assumes dpos: "0 < d" and
   12.20      P1eqP1: "ALL x k. P1 x = P1(x - k*d)" and ePeqP1: "EX z::int. ALL x. x < z \<longrightarrow> (P x = P1 x)"
   12.21    shows "(EX x. P1 x) \<longrightarrow> (EX x. P x)"
   12.22  proof
   12.23 @@ -251,7 +251,7 @@
   12.24    then obtain x where P1: "P1 x" ..
   12.25    from ePeqP1 obtain z where P1eqP: "ALL x. x < z \<longrightarrow> (P x = P1 x)" ..
   12.26    let ?w = "x - (abs(x-z)+1) * d"
   12.27 -  have w: "?w < z" by(rule decr_lemma)
   12.28 +  from dpos have w: "?w < z" by(rule decr_lemma)
   12.29    have "P1 x = P1 ?w" using P1eqP1 by blast
   12.30    also have "\<dots> = P(?w)" using w P1eqP by blast
   12.31    finally have "P ?w" using P1 by blast
   12.32 @@ -289,7 +289,7 @@
   12.33  subsection {* The @{text "+\<infinity>"} Version*}
   12.34  
   12.35  lemma  plusinfinity:
   12.36 -  assumes "(0::int) < d" and
   12.37 +  assumes dpos: "(0::int) < d" and
   12.38      P1eqP1: "\<forall>x k. P' x = P'(x - k*d)" and ePeqP1: "\<exists> z. \<forall> x>z. P x = P' x"
   12.39    shows "(\<exists> x. P' x) \<longrightarrow> (\<exists> x. P x)"
   12.40  proof
   12.41 @@ -299,7 +299,7 @@
   12.42    let ?w' = "x + (abs(x-z)+1) * d"
   12.43    let ?w = "x - (-(abs(x-z) + 1))*d"
   12.44    have ww'[simp]: "?w = ?w'" by (simp add: ring_eq_simps)
   12.45 -  have w: "?w > z" by(simp only: ww', rule incr_lemma)
   12.46 +  from dpos have w: "?w > z" by(simp only: ww' incr_lemma)
   12.47    hence "P' x = P' ?w" using P1eqP1 by blast
   12.48    also have "\<dots> = P(?w)" using w P1eqP by blast
   12.49    finally have "P ?w" using P1 by blast
    13.1 --- a/src/HOL/Real/ContNotDenum.thy	Thu Jun 14 18:33:29 2007 +0200
    13.2 +++ b/src/HOL/Real/ContNotDenum.thy	Thu Jun 14 18:33:31 2007 +0200
    13.3 @@ -85,7 +85,7 @@
    13.4  lemma closed_mem:
    13.5    assumes "a \<le> c" and "c \<le> b"
    13.6    shows "c \<in> closed_int a b"
    13.7 -  by (unfold closed_int_def) auto
    13.8 +  using assms unfolding closed_int_def by auto
    13.9  
   13.10  lemma closed_subset:
   13.11    assumes ac: "a \<le> b"  "c \<le> d" 
    14.1 --- a/src/HOL/Real/PReal.thy	Thu Jun 14 18:33:29 2007 +0200
    14.2 +++ b/src/HOL/Real/PReal.thy	Thu Jun 14 18:33:31 2007 +0200
    14.3 @@ -437,7 +437,7 @@
    14.4        show "z = (z/y)*y"
    14.5  	by (simp add: divide_inverse mult_commute [of y] mult_assoc
    14.6  		      order_less_imp_not_eq2)
    14.7 -      show "y \<in> B" .
    14.8 +      show "y \<in> B" by fact
    14.9      qed
   14.10    next
   14.11      show "z/y \<in> A"
   14.12 @@ -527,7 +527,7 @@
   14.13            show "x = (x/v)*v"
   14.14  	    by (simp add: divide_inverse mult_assoc vpos
   14.15                            order_less_imp_not_eq2)
   14.16 -          show "v \<in> A" .
   14.17 +          show "v \<in> A" by fact
   14.18          qed
   14.19        qed
   14.20      qed
   14.21 @@ -1280,8 +1280,8 @@
   14.22      by (simp add: mult_ac)
   14.23    also have "... = x/y" using zpos
   14.24      by (simp add: divide_inverse)
   14.25 -  also have "... < z"
   14.26 -    by (simp add: pos_divide_less_eq [OF ypos] mult_commute) 
   14.27 +  also from xless have "... < z"
   14.28 +    by (simp add: pos_divide_less_eq [OF ypos] mult_commute)
   14.29    finally show ?thesis .
   14.30  qed
   14.31  
    15.1 --- a/src/HOL/Real/RComplete.thy	Thu Jun 14 18:33:29 2007 +0200
    15.2 +++ b/src/HOL/Real/RComplete.thy	Thu Jun 14 18:33:31 2007 +0200
    15.3 @@ -59,16 +59,16 @@
    15.4      then obtain py where y_is_py: "y = real_of_preal py"
    15.5        by (auto simp add: real_gt_zero_preal_Ex)
    15.6  
    15.7 -    obtain a where a_in_P: "a \<in> P" using not_empty_P ..
    15.8 -    have a_pos: "0 < a" using positive_P ..
    15.9 +    obtain a where "a \<in> P" using not_empty_P ..
   15.10 +    with positive_P have a_pos: "0 < a" ..
   15.11      then obtain pa where "a = real_of_preal pa"
   15.12        by (auto simp add: real_gt_zero_preal_Ex)
   15.13 -    hence "pa \<in> ?pP" using a_in_P by auto
   15.14 +    hence "pa \<in> ?pP" using `a \<in> P` by auto
   15.15      hence pP_not_empty: "?pP \<noteq> {}" by auto
   15.16  
   15.17      obtain sup where sup: "\<forall>x \<in> P. x < sup"
   15.18        using upper_bound_Ex ..
   15.19 -    hence  "a < sup" ..
   15.20 +    from this and `a \<in> P` have "a < sup" ..
   15.21      hence "0 < sup" using a_pos by arith
   15.22      then obtain possup where "sup = real_of_preal possup"
   15.23        by (auto simp add: real_gt_zero_preal_Ex)
   15.24 @@ -521,9 +521,9 @@
   15.25    assumes a1: "real m \<le> r" and a2: "r < real n + 1"
   15.26    shows "m \<le> (n::int)"
   15.27  proof -
   15.28 -  have "real m < real n + 1" by (rule order_le_less_trans)
   15.29 -  also have "... = real(n+1)" by simp
   15.30 -  finally have "m < n+1" by (simp only: real_of_int_less_iff)
   15.31 +  have "real m < real n + 1" using a1 a2 by (rule order_le_less_trans)
   15.32 +  also have "... = real (n + 1)" by simp
   15.33 +  finally have "m < n + 1" by (simp only: real_of_int_less_iff)
   15.34    thus ?thesis by arith
   15.35  qed
   15.36  
    16.1 --- a/src/HOL/Ring_and_Field.thy	Thu Jun 14 18:33:29 2007 +0200
    16.2 +++ b/src/HOL/Ring_and_Field.thy	Thu Jun 14 18:33:31 2007 +0200
    16.3 @@ -170,6 +170,7 @@
    16.4  class division_by_zero = zero + inverse +
    16.5    assumes inverse_zero [simp]: "inverse \<^loc>0 = \<^loc>0"
    16.6  
    16.7 +
    16.8  subsection {* Distribution rules *}
    16.9  
   16.10  theorems ring_distrib = right_distrib left_distrib
   16.11 @@ -343,6 +344,7 @@
   16.12  apply (simp add: compare_rls minus_mult_left [symmetric]) 
   16.13  done
   16.14  
   16.15 +
   16.16  subsection {* Ordering Rules for Multiplication *}
   16.17  
   16.18  lemma mult_left_le_imp_le:
   16.19 @@ -386,6 +388,7 @@
   16.20  apply (simp_all add: minus_mult_right [symmetric]) 
   16.21  done
   16.22  
   16.23 +
   16.24  subsection{* Products of Signs *}
   16.25  
   16.26  lemma mult_pos_pos: "[| (0::'a::ordered_semiring_strict) < a; 0 < b |] ==> 0 < a*b"
   16.27 @@ -501,6 +504,7 @@
   16.28  lemma not_one_less_zero [simp]: "~ (1::'a::ordered_semidom) < 0"
   16.29  by (simp add: linorder_not_less) 
   16.30  
   16.31 +
   16.32  subsection{*More Monotonicity*}
   16.33  
   16.34  text{*Strict monotonicity in both arguments*}
   16.35 @@ -559,6 +563,7 @@
   16.36    apply simp
   16.37  done
   16.38  
   16.39 +
   16.40  subsection{*Cancellation Laws for Relationships With a Common Factor*}
   16.41  
   16.42  text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},
   16.43 @@ -621,7 +626,7 @@
   16.44  proof (rule ccontr)
   16.45    assume "~ a < b"
   16.46    hence "b \<le> a" by (simp add: linorder_not_less)
   16.47 -  hence "c*b \<le> c*a" by (rule mult_left_mono)
   16.48 +  hence "c*b \<le> c*a" using nonneg by (rule mult_left_mono)
   16.49    with this and less show False 
   16.50      by (simp add: linorder_not_less [symmetric])
   16.51  qed
   16.52 @@ -632,7 +637,7 @@
   16.53  proof (rule ccontr)
   16.54    assume "~ a < b"
   16.55    hence "b \<le> a" by (simp add: linorder_not_less)
   16.56 -  hence "b*c \<le> a*c" by (rule mult_right_mono)
   16.57 +  hence "b*c \<le> a*c" using nonneg by (rule mult_right_mono)
   16.58    with this and less show False 
   16.59      by (simp add: linorder_not_less [symmetric])
   16.60  qed  
   16.61 @@ -746,6 +751,7 @@
   16.62    add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2
   16.63    diff_eq_eq eq_diff_eq *)
   16.64      
   16.65 +
   16.66  subsection {* Fields *}
   16.67  
   16.68  lemma right_inverse_eq: "b \<noteq> 0 ==> (a / b = 1) = (a = (b::'a::field))"
   16.69 @@ -968,6 +974,7 @@
   16.70        "inverse (a/b) = b / (a::'a::{field,division_by_zero})"
   16.71    by (simp add: divide_inverse mult_commute)
   16.72  
   16.73 +
   16.74  subsection {* Calculations with fractions *}
   16.75  
   16.76  lemma nonzero_mult_divide_cancel_left:
   16.77 @@ -1038,6 +1045,7 @@
   16.78    apply assumption
   16.79  done
   16.80  
   16.81 +
   16.82  subsubsection{*Special Cancellation Simprules for Division*}
   16.83  
   16.84  lemma mult_divide_cancel_left_if [simp]:
   16.85 @@ -1136,6 +1144,7 @@
   16.86    apply simp_all
   16.87  done
   16.88  
   16.89 +
   16.90  subsection {* Ordered Fields *}
   16.91  
   16.92  lemma positive_imp_inverse_positive: 
   16.93 @@ -1171,15 +1180,15 @@
   16.94    qed
   16.95  
   16.96  lemma inverse_positive_imp_positive:
   16.97 -      assumes inv_gt_0: "0 < inverse a"
   16.98 -          and [simp]:   "a \<noteq> 0"
   16.99 -        shows "0 < (a::'a::ordered_field)"
  16.100 -  proof -
  16.101 +  assumes inv_gt_0: "0 < inverse a"
  16.102 +    and nz: "a \<noteq> 0"
  16.103 +  shows "0 < (a::'a::ordered_field)"
  16.104 +proof -
  16.105    have "0 < inverse (inverse a)"
  16.106 -    by (rule positive_imp_inverse_positive)
  16.107 +    using inv_gt_0 by (rule positive_imp_inverse_positive)
  16.108    thus "0 < a"
  16.109 -    by (simp add: nonzero_inverse_inverse_eq)
  16.110 -  qed
  16.111 +    using nz by (simp add: nonzero_inverse_inverse_eq)
  16.112 +qed
  16.113  
  16.114  lemma inverse_positive_iff_positive [simp]:
  16.115        "(0 < inverse a) = (0 < (a::'a::{ordered_field,division_by_zero}))"
  16.116 @@ -1188,15 +1197,15 @@
  16.117  done
  16.118  
  16.119  lemma inverse_negative_imp_negative:
  16.120 -      assumes inv_less_0: "inverse a < 0"
  16.121 -          and [simp]:   "a \<noteq> 0"
  16.122 -        shows "a < (0::'a::ordered_field)"
  16.123 -  proof -
  16.124 +  assumes inv_less_0: "inverse a < 0"
  16.125 +    and nz:  "a \<noteq> 0"
  16.126 +  shows "a < (0::'a::ordered_field)"
  16.127 +proof -
  16.128    have "inverse (inverse a) < 0"
  16.129 -    by (rule negative_imp_inverse_negative)
  16.130 +    using inv_less_0 by (rule negative_imp_inverse_negative)
  16.131    thus "a < 0"
  16.132 -    by (simp add: nonzero_inverse_inverse_eq)
  16.133 -  qed
  16.134 +    using nz by (simp add: nonzero_inverse_inverse_eq)
  16.135 +qed
  16.136  
  16.137  lemma inverse_negative_iff_negative [simp]:
  16.138        "(inverse a < 0) = (a < (0::'a::{ordered_field,division_by_zero}))"
  16.139 @@ -1334,6 +1343,7 @@
  16.140     "(inverse x \<le> 1) = (x \<le> 0 | 1 \<le> (x::'a::{ordered_field,division_by_zero}))"
  16.141  by (simp add: linorder_not_less [symmetric] one_less_inverse_iff) 
  16.142  
  16.143 +
  16.144  subsection{*Simplification of Inequalities Involving Literal Divisors*}
  16.145  
  16.146  lemma pos_le_divide_eq: "0 < (c::'a::ordered_field) ==> (a \<le> b/c) = (a*c \<le> b)"
  16.147 @@ -1500,6 +1510,7 @@
  16.148    apply (erule nonzero_divide_eq_eq) 
  16.149  done
  16.150  
  16.151 +
  16.152  subsection{*Division and Signs*}
  16.153  
  16.154  lemma zero_less_divide_iff:
  16.155 @@ -1578,6 +1589,7 @@
  16.156    apply simp
  16.157  done
  16.158  
  16.159 +
  16.160  subsection{*Cancellation Laws for Division*}
  16.161  
  16.162  lemma divide_cancel_right [simp]:
  16.163 @@ -1592,6 +1604,7 @@
  16.164  apply (simp add: divide_inverse field_mult_cancel_left) 
  16.165  done
  16.166  
  16.167 +
  16.168  subsection {* Division and the Number One *}
  16.169  
  16.170  text{*Simplify expressions equated with 1*}
  16.171 @@ -1629,6 +1642,7 @@
  16.172  declare zero_le_divide_1_iff [simp]
  16.173  declare divide_le_0_1_iff [simp]
  16.174  
  16.175 +
  16.176  subsection {* Ordering Rules for Division *}
  16.177  
  16.178  lemma divide_strict_right_mono:
  16.179 @@ -1706,6 +1720,7 @@
  16.180    shows "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)"
  16.181  by (auto simp add: divide_less_eq)
  16.182  
  16.183 +
  16.184  subsection{*Conditional Simplification Rules: No Case Splits*}
  16.185  
  16.186  lemma le_divide_eq_1_pos [simp]:
  16.187 @@ -1758,6 +1773,7 @@
  16.188    shows "(b/a = 1) = ((a \<noteq> 0 & a = b))"
  16.189  by (auto simp add: divide_eq_eq)
  16.190  
  16.191 +
  16.192  subsection {* Reasoning about inequalities with division *}
  16.193  
  16.194  lemma mult_right_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1
  16.195 @@ -1823,6 +1839,7 @@
  16.196  
  16.197  declare times_divide_eq [simp]
  16.198  
  16.199 +
  16.200  subsection {* Ordered Fields are Dense *}
  16.201  
  16.202  lemma less_add_one: "a < (a+1::'a::ordered_semidom)"
  16.203 @@ -1995,6 +2012,7 @@
  16.204    apply (simp add: order_less_imp_le);
  16.205  done;
  16.206  
  16.207 +
  16.208  subsection {* Bounds of products via negative and positive Part *}
  16.209  
  16.210  lemma mult_le_prts:
  16.211 @@ -2063,6 +2081,7 @@
  16.212    then show ?thesis by simp
  16.213  qed
  16.214  
  16.215 +
  16.216  subsection {* Theorems for proof tools *}
  16.217  
  16.218  lemma add_mono_thms_ordered_semiring:
    17.1 --- a/src/HOL/Wellfounded_Recursion.thy	Thu Jun 14 18:33:29 2007 +0200
    17.2 +++ b/src/HOL/Wellfounded_Recursion.thy	Thu Jun 14 18:33:31 2007 +0200
    17.3 @@ -301,7 +301,7 @@
    17.4            with A2 show "y \<notin> Q" .
    17.5          qed
    17.6        qed
    17.7 -      thus ?thesis ..
    17.8 +      with `z' \<in> Q` show ?thesis ..
    17.9      qed
   17.10    qed
   17.11  qed
    18.1 --- a/src/HOL/ex/CTL.thy	Thu Jun 14 18:33:29 2007 +0200
    18.2 +++ b/src/HOL/ex/CTL.thy	Thu Jun 14 18:33:31 2007 +0200
    18.3 @@ -99,7 +99,7 @@
    18.4        then have "f (- u) \<subseteq> - u" by auto
    18.5        then have "lfp f \<subseteq> - u" by (rule lfp_lowerbound)
    18.6        from l and this have "x \<notin> u" by auto
    18.7 -      then show False by contradiction
    18.8 +      with `x \<in> u` show False by contradiction
    18.9      qed
   18.10    qed
   18.11    show "- gfp (\<lambda>s. - f (- s)) \<subseteq> lfp f"