# HG changeset patch
# User wenzelm
# Date 1181838811 -7200
# Node ID aaca6a8e5414a2259e0155d8bb8c5c87f4b24401
# Parent  77645da0db85b3949c73b34f4b56c10a9b7342c3
tuned proofs: avoid implicit prems;

diff -r 77645da0db85 -r aaca6a8e5414 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Thu Jun 14 18:33:29 2007 +0200
+++ b/src/HOL/Finite_Set.thy	Thu Jun 14 18:33:31 2007 +0200
@@ -35,7 +35,7 @@
   assume "finite F"
   thus "P F"
   proof induct
-    show "P {}" .
+    show "P {}" by fact
     fix x F assume F: "finite F" and P: "P F"
     show "P (insert x F)"
     proof cases
@@ -61,30 +61,35 @@
   case (insert x F)
   show ?case
   proof cases
-    assume "F = {}" thus ?thesis using insert(4) by simp
+    assume "F = {}"
+    thus ?thesis using `P {x}` by simp
   next
-    assume "F \<noteq> {}" thus ?thesis using insert by blast
+    assume "F \<noteq> {}"
+    thus ?thesis using insert by blast
   qed
 qed
 
 lemma finite_subset_induct [consumes 2, case_names empty insert]:
-  "finite F ==> F \<subseteq> A ==>
-    P {} ==> (!!a F. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)) ==>
-    P F"
+  assumes "finite F" and "F \<subseteq> A"
+    and empty: "P {}"
+    and insert: "!!a F. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)"
+  shows "P F"
 proof -
-  assume "P {}" and insert:
-    "!!a F. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)"
-  assume "finite F"
-  thus "F \<subseteq> A ==> P F"
+  from `finite F` and `F \<subseteq> A`
+  show ?thesis
   proof induct
-    show "P {}" .
-    fix x F assume "finite F" and "x \<notin> F"
-      and P: "F \<subseteq> A ==> P F" and i: "insert x F \<subseteq> A"
+    show "P {}" by fact
+  next
+    fix x F
+    assume "finite F" and "x \<notin> F" and
+      P: "F \<subseteq> A ==> P F" and i: "insert x F \<subseteq> A"
     show "P (insert x F)"
     proof (rule insert)
       from i show "x \<in> A" by blast
       from i have "F \<subseteq> A" by blast
       with P show "P F" .
+      show "finite F" by fact
+      show "x \<notin> F" by fact
     qed
   qed
 qed
@@ -102,7 +107,7 @@
   qed
 next
   case (insert a A)
-  have notinA: "a \<notin> A" .
+  have notinA: "a \<notin> A" by fact
   from insert.hyps obtain n f
     where "A = f ` {i::nat. i < n}" "inj_on f {i. i < n}" by blast
   hence "insert a A = f(n:=a) ` {i. i < Suc n}"
@@ -151,17 +156,17 @@
     thus ?case by simp
   next
     case (insert x F A)
-    have A: "A \<subseteq> insert x F" and r: "A - {x} \<subseteq> F ==> finite (A - {x})" .
+    have A: "A \<subseteq> insert x F" and r: "A - {x} \<subseteq> F ==> finite (A - {x})" by fact+
     show "finite A"
     proof cases
       assume x: "x \<in> A"
       with A have "A - {x} \<subseteq> F" by (simp add: subset_insert_iff)
       with r have "finite (A - {x})" .
       hence "finite (insert x (A - {x}))" ..
-      also have "insert x (A - {x}) = A" by (rule insert_Diff)
+      also have "insert x (A - {x}) = A" using x by (rule insert_Diff)
       finally show ?thesis .
     next
-      show "A \<subseteq> F ==> ?thesis" .
+      show "A \<subseteq> F ==> ?thesis" by fact
       assume "x \<notin> A"
       with A show "A \<subseteq> F" by (simp add: subset_insert_iff)
     qed
@@ -188,35 +193,37 @@
 by (induct rule:finite_induct) simp_all
 
 lemma finite_empty_induct:
-  "finite A ==>
-  P A ==> (!!a A. finite A ==> a:A ==> P A ==> P (A - {a})) ==> P {}"
+  assumes "finite A"
+    and "P A"
+    and "!!a A. finite A ==> a:A ==> P A ==> P (A - {a})"
+  shows "P {}"
 proof -
-  assume "finite A"
-    and "P A" and "!!a A. finite A ==> a:A ==> P A ==> P (A - {a})"
   have "P (A - A)"
   proof -
-    fix c b :: "'a set"
-    presume c: "finite c" and b: "finite b"
-      and P1: "P b" and P2: "!!x y. finite y ==> x \<in> y ==> P y ==> P (y - {x})"
-    from c show "c \<subseteq> b ==> P (b - c)"
-    proof induct
-      case empty
-      from P1 show ?case by simp
-    next
-      case (insert x F)
-      have "P (b - F - {x})"
-      proof (rule P2)
-        from _ b show "finite (b - F)" by (rule finite_subset) blast
-        from insert show "x \<in> b - F" by simp
-        from insert show "P (b - F)" by simp
+    {
+      fix c b :: "'a set"
+      assume c: "finite c" and b: "finite b"
+	and P1: "P b" and P2: "!!x y. finite y ==> x \<in> y ==> P y ==> P (y - {x})"
+      have "c \<subseteq> b ==> P (b - c)"
+	using c
+      proof induct
+	case empty
+	from P1 show ?case by simp
+      next
+	case (insert x F)
+	have "P (b - F - {x})"
+	proof (rule P2)
+          from _ b show "finite (b - F)" by (rule finite_subset) blast
+          from insert show "x \<in> b - F" by simp
+          from insert show "P (b - F)" by simp
+	qed
+	also have "b - F - {x} = b - insert x F" by (rule Diff_insert [symmetric])
+	finally show ?case .
       qed
-      also have "b - F - {x} = b - insert x F" by (rule Diff_insert [symmetric])
-      finally show ?case .
-    qed
-  next
-    show "A \<subseteq> A" ..
+    }
+    then show ?thesis by this (simp_all add: assms)
   qed
-  thus "P {}" by simp
+  then show ?thesis by simp
 qed
 
 lemma finite_Diff [simp]: "finite B ==> finite (B - Ba)"
@@ -526,7 +533,7 @@
   case 0 thus ?thesis using aA by auto
 next
   case (Suc m)
-  have nSuc: "n = Suc m" . 
+  have nSuc: "n = Suc m" by fact
   have mlessn: "m<n" by (simp add: nSuc)
   from aA obtain k where hkeq: "h k = a" and klessn: "k<n" by (blast elim!: equalityE)
   let ?hm = "swap k m h"
@@ -557,9 +564,9 @@
   case (less n)
     have IH: "!!m h A x x'. 
                \<lbrakk>m<n; A = h ` {i. i<m}; inj_on h {i. i<m}; 
-                foldSet f g z A x; foldSet f g z A x'\<rbrakk> \<Longrightarrow> x' = x" .
+                foldSet f g z A x; foldSet f g z A x'\<rbrakk> \<Longrightarrow> x' = x" by fact
     have Afoldx: "foldSet f g z A x" and Afoldx': "foldSet f g z A x'"
-     and A: "A = h`{i. i<n}" and injh: "inj_on h {i. i<n}" .
+     and A: "A = h`{i. i<n}" and injh: "inj_on h {i. i<n}" by fact+
     show ?case
     proof (rule foldSet.cases [OF Afoldx])
       assume "A = {}" and "x = z"
diff -r 77645da0db85 -r aaca6a8e5414 src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Thu Jun 14 18:33:29 2007 +0200
+++ b/src/HOL/Groebner_Basis.thy	Thu Jun 14 18:33:31 2007 +0200
@@ -163,7 +163,7 @@
 lemma "axioms" [normalizer
     semiring ops: semiring_ops
     semiring rules: semiring_rules]:
-  "gb_semiring add mul pwr r0 r1" .
+  "gb_semiring add mul pwr r0 r1" by fact
 
 end
 
@@ -232,7 +232,7 @@
   semiring rules: semiring_rules
   ring ops: ring_ops
   ring rules: ring_rules]:
-  "gb_ring add mul pwr r0 r1 sub neg" .
+  "gb_ring add mul pwr r0 r1 sub neg" by fact
 
 end
 
@@ -273,7 +273,7 @@
   semiring rules: semiring_rules
   ring ops: ring_ops
   ring rules: ring_rules]:
-  "gb_field add mul pwr r0 r1 sub neg divide inverse" .
+  "gb_field add mul pwr r0 r1 sub neg divide inverse" by fact
 
 end
 
@@ -311,7 +311,7 @@
   semiring ops: semiring_ops
   semiring rules: semiring_rules
   idom rules: noteq_reduce add_scale_eq_noteq]:
-  "semiringb add mul pwr r0 r1" .
+  "semiringb add mul pwr r0 r1" by fact
 
 end
 
@@ -326,7 +326,7 @@
   ring ops: ring_ops
   ring rules: ring_rules
   idom rules: noteq_reduce add_scale_eq_noteq]:
-  "ringb add mul pwr r0 r1 sub neg" .
+  "ringb add mul pwr r0 r1 sub neg" by fact
 
 end
 
diff -r 77645da0db85 -r aaca6a8e5414 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Jun 14 18:33:29 2007 +0200
+++ b/src/HOL/HOL.thy	Thu Jun 14 18:33:31 2007 +0200
@@ -768,7 +768,7 @@
 lemma atomize_all [atomize]: "(!!x. P x) == Trueprop (ALL x. P x)"
 proof
   assume "!!x. P x"
-  show "ALL x. P x" by (rule allI)
+  then show "ALL x. P x" ..
 next
   assume "ALL x. P x"
   thus "!!x. P x" by (rule allE)
@@ -1219,11 +1219,11 @@
 
 lemma True_implies_equals: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
 proof
-  assume prem: "True \<Longrightarrow> PROP P"
-  from prem [OF TrueI] show "PROP P" . 
+  assume "True \<Longrightarrow> PROP P"
+  from this [OF TrueI] show "PROP P" .
 next
   assume "PROP P"
-  show "PROP P" .
+  then show "PROP P" .
 qed
 
 lemma ex_simps:
diff -r 77645da0db85 -r aaca6a8e5414 src/HOL/Import/HOL4Compat.thy
--- a/src/HOL/Import/HOL4Compat.thy	Thu Jun 14 18:33:29 2007 +0200
+++ b/src/HOL/Import/HOL4Compat.thy	Thu Jun 14 18:33:31 2007 +0200
@@ -157,7 +157,7 @@
     fix k
     show "!q. q + k = m \<longrightarrow> P q"
     proof (induct k,simp_all)
-      show "P m" .
+      show "P m" by fact
     next
       fix k
       assume ind: "!q. q + k = m \<longrightarrow> P q"
@@ -406,7 +406,7 @@
   assume allt: "!t. P t \<longrightarrow> (!h. P (h # t))"
   show "P l"
   proof (induct l)
-    show "P []" .
+    show "P []" by fact
   next
     fix h t
     assume "P t"
diff -r 77645da0db85 -r aaca6a8e5414 src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Thu Jun 14 18:33:29 2007 +0200
+++ b/src/HOL/Inductive.thy	Thu Jun 14 18:33:31 2007 +0200
@@ -89,7 +89,7 @@
   then show P ..
 next
   assume "\<And>P\<Colon>bool. P"
-  then show False ..
+  then show False .
 qed
 
 lemma not_eq_False:
diff -r 77645da0db85 -r aaca6a8e5414 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Thu Jun 14 18:33:29 2007 +0200
+++ b/src/HOL/Lattices.thy	Thu Jun 14 18:33:31 2007 +0200
@@ -259,7 +259,7 @@
   and greatest: "\<And>x y z. x \<^loc>\<le> y \<Longrightarrow> x \<^loc>\<le> z \<Longrightarrow> x \<^loc>\<le> y \<triangle> z"
   shows "x \<sqinter> y = x \<triangle> y"
 proof (rule antisym)
-  show "x \<triangle> y \<^loc>\<le> x \<sqinter> y" by (rule le_infI) (rule le1 le2)
+  show "x \<triangle> y \<^loc>\<le> x \<sqinter> y" by (rule le_infI) (rule le1, rule le2)
 next
   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)
   show "x \<sqinter> y \<^loc>\<le> x \<triangle> y" by (rule leI) simp_all
@@ -271,7 +271,7 @@
   and least: "\<And>x y z. y \<^loc>\<le> x \<Longrightarrow> z \<^loc>\<le> x \<Longrightarrow> y \<nabla> z \<^loc>\<le> x"
   shows "x \<squnion> y = x \<nabla> y"
 proof (rule antisym)
-  show "x \<squnion> y \<^loc>\<le> x \<nabla> y" by (rule le_supI) (rule ge1 ge2)
+  show "x \<squnion> y \<^loc>\<le> x \<nabla> y" by (rule le_supI) (rule ge1, rule ge2)
 next
   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)
   show "x \<nabla> y \<^loc>\<le> x \<squnion> y" by (rule leI) simp_all
diff -r 77645da0db85 -r aaca6a8e5414 src/HOL/Library/SCT_Theorem.thy
--- a/src/HOL/Library/SCT_Theorem.thy	Thu Jun 14 18:33:29 2007 +0200
+++ b/src/HOL/Library/SCT_Theorem.thy	Thu Jun 14 18:33:31 2007 +0200
@@ -1139,12 +1139,12 @@
        (auto simp:index_less)
   then obtain T i
     where inf: "infinite T"
-    and "i < length l"
+    and i: "i < length l"
     and d: "\<And>x y. \<lbrakk>x \<in> T; y\<in>T; x \<noteq> y\<rbrakk>
     \<Longrightarrow> index_of l (f (set2pair {x, y})) = i"
     by auto
 
-  have  "l ! i \<in> S" unfolding S
+  have "l ! i \<in> S" unfolding S using i
     by (rule nth_mem)
   moreover
   have "\<And>x y. x \<in> T \<Longrightarrow> y\<in>T \<Longrightarrow> x < y
diff -r 77645da0db85 -r aaca6a8e5414 src/HOL/NatBin.thy
--- a/src/HOL/NatBin.thy	Thu Jun 14 18:33:29 2007 +0200
+++ b/src/HOL/NatBin.thy	Thu Jun 14 18:33:31 2007 +0200
@@ -376,13 +376,13 @@
      "(a::'a::{ordered_idom,recpower}) < 0 ==> a ^ Suc(2*n) < 0"
 proof (induct "n")
   case 0
-    show ?case by (simp add: Power.power_Suc)
+  then show ?case by (simp add: Power.power_Suc)
 next
   case (Suc n)
-    have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)" 
-      by (simp add: mult_ac power_add power2_eq_square Power.power_Suc)
-    thus ?case
-      by (simp add: prems mult_less_0_iff mult_neg_neg)
+  have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)" 
+    by (simp add: mult_ac power_add power2_eq_square Power.power_Suc)
+  thus ?case
+    by (simp add: prems mult_less_0_iff mult_neg_neg)
 qed
 
 lemma odd_0_le_power_imp_0_le:
diff -r 77645da0db85 -r aaca6a8e5414 src/HOL/Numeral.thy
--- a/src/HOL/Numeral.thy	Thu Jun 14 18:33:29 2007 +0200
+++ b/src/HOL/Numeral.thy	Thu Jun 14 18:33:31 2007 +0200
@@ -339,7 +339,7 @@
   assumes le: "0 \<le> z"
   shows "(0::int) < 1 + z"
 proof -
-  have "0 \<le> z" .
+  have "0 \<le> z" by fact
   also have "... < z + 1" by (rule less_add_one) 
   also have "... = 1 + z" by (simp add: add_ac)
   finally show "0 < 1 + z" .
diff -r 77645da0db85 -r aaca6a8e5414 src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Thu Jun 14 18:33:29 2007 +0200
+++ b/src/HOL/OrderedGroup.thy	Thu Jun 14 18:33:31 2007 +0200
@@ -377,10 +377,10 @@
 subsection {* Ordering Rules for Unary Minus *}
 
 lemma le_imp_neg_le:
-      assumes "a \<le> (b::'a::{pordered_ab_semigroup_add_imp_le, ab_group_add})" shows "-b \<le> -a"
+  assumes "a \<le> (b::'a::{pordered_ab_semigroup_add_imp_le, ab_group_add})" shows "-b \<le> -a"
 proof -
   have "-a+a \<le> -a+b"
-    by (rule add_left_mono) 
+    using `a \<le> b` by (rule add_left_mono) 
   hence "0 \<le> -a+b"
     by simp
   hence "0 + (-b) \<le> (-a + b) + (-b)"
diff -r 77645da0db85 -r aaca6a8e5414 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Thu Jun 14 18:33:29 2007 +0200
+++ b/src/HOL/Predicate.thy	Thu Jun 14 18:33:31 2007 +0200
@@ -34,11 +34,11 @@
 proof
   fix S
   assume "!!S. PROP P S"
-  show "PROP P (Collect S)" .
+  then show "PROP P (Collect S)" .
 next
   fix S
   assume "!!S. PROP P (Collect S)"
-  have "PROP P {x. x : S}" .
+  then have "PROP P {x. x : S}" .
   thus "PROP P S" by simp
 qed
 
@@ -46,11 +46,11 @@
 proof
   fix S
   assume "!!S. PROP P S"
-  show "PROP P (member S)" .
+  then show "PROP P (member S)" .
 next
   fix S
   assume "!!S. PROP P (member S)"
-  have "PROP P (member {x. S x})" .
+  then have "PROP P (member {x. S x})" .
   thus "PROP P S" by simp
 qed
 
@@ -96,11 +96,11 @@
 proof
   fix S
   assume "!!S. PROP P S"
-  show "PROP P (Collect2 S)" .
+  then show "PROP P (Collect2 S)" .
 next
   fix S
   assume "!!S. PROP P (Collect2 S)"
-  have "PROP P (Collect2 (member2 S))" .
+  then have "PROP P (Collect2 (member2 S))" .
   thus "PROP P S" by simp
 qed
 
@@ -108,11 +108,11 @@
 proof
   fix S
   assume "!!S. PROP P S"
-  show "PROP P (member2 S)" .
+  then show "PROP P (member2 S)" .
 next
   fix S
   assume "!!S. PROP P (member2 S)"
-  have "PROP P (member2 (Collect2 S))" .
+  then have "PROP P (member2 (Collect2 S))" .
   thus "PROP P S" by simp
 qed
 
diff -r 77645da0db85 -r aaca6a8e5414 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Thu Jun 14 18:33:29 2007 +0200
+++ b/src/HOL/Presburger.thy	Thu Jun 14 18:33:31 2007 +0200
@@ -200,8 +200,8 @@
     have "P(x mod d)" using dpos P Pmod by(simp add:pos_mod_sign pos_mod_bound)
     moreover have "x mod d : {1..d}"
     proof -
-      have "0 \<le> x mod d" by(rule pos_mod_sign)
-      moreover have "x mod d < d" by(rule pos_mod_bound)
+      from dpos have "0 \<le> x mod d" by(rule pos_mod_sign)
+      moreover from dpos have "x mod d < d" by(rule pos_mod_bound)
       ultimately show ?thesis using not0 by(simp add:atLeastAtMost_iff)
     qed
     ultimately show ?RHS ..
@@ -243,7 +243,7 @@
 qed
 
 lemma  minusinfinity:
-  assumes "0 < d" and
+  assumes dpos: "0 < d" and
     P1eqP1: "ALL x k. P1 x = P1(x - k*d)" and ePeqP1: "EX z::int. ALL x. x < z \<longrightarrow> (P x = P1 x)"
   shows "(EX x. P1 x) \<longrightarrow> (EX x. P x)"
 proof
@@ -251,7 +251,7 @@
   then obtain x where P1: "P1 x" ..
   from ePeqP1 obtain z where P1eqP: "ALL x. x < z \<longrightarrow> (P x = P1 x)" ..
   let ?w = "x - (abs(x-z)+1) * d"
-  have w: "?w < z" by(rule decr_lemma)
+  from dpos have w: "?w < z" by(rule decr_lemma)
   have "P1 x = P1 ?w" using P1eqP1 by blast
   also have "\<dots> = P(?w)" using w P1eqP by blast
   finally have "P ?w" using P1 by blast
@@ -289,7 +289,7 @@
 subsection {* The @{text "+\<infinity>"} Version*}
 
 lemma  plusinfinity:
-  assumes "(0::int) < d" and
+  assumes dpos: "(0::int) < d" and
     P1eqP1: "\<forall>x k. P' x = P'(x - k*d)" and ePeqP1: "\<exists> z. \<forall> x>z. P x = P' x"
   shows "(\<exists> x. P' x) \<longrightarrow> (\<exists> x. P x)"
 proof
@@ -299,7 +299,7 @@
   let ?w' = "x + (abs(x-z)+1) * d"
   let ?w = "x - (-(abs(x-z) + 1))*d"
   have ww'[simp]: "?w = ?w'" by (simp add: ring_eq_simps)
-  have w: "?w > z" by(simp only: ww', rule incr_lemma)
+  from dpos have w: "?w > z" by(simp only: ww' incr_lemma)
   hence "P' x = P' ?w" using P1eqP1 by blast
   also have "\<dots> = P(?w)" using w P1eqP by blast
   finally have "P ?w" using P1 by blast
diff -r 77645da0db85 -r aaca6a8e5414 src/HOL/Real/ContNotDenum.thy
--- a/src/HOL/Real/ContNotDenum.thy	Thu Jun 14 18:33:29 2007 +0200
+++ b/src/HOL/Real/ContNotDenum.thy	Thu Jun 14 18:33:31 2007 +0200
@@ -85,7 +85,7 @@
 lemma closed_mem:
   assumes "a \<le> c" and "c \<le> b"
   shows "c \<in> closed_int a b"
-  by (unfold closed_int_def) auto
+  using assms unfolding closed_int_def by auto
 
 lemma closed_subset:
   assumes ac: "a \<le> b"  "c \<le> d" 
diff -r 77645da0db85 -r aaca6a8e5414 src/HOL/Real/PReal.thy
--- a/src/HOL/Real/PReal.thy	Thu Jun 14 18:33:29 2007 +0200
+++ b/src/HOL/Real/PReal.thy	Thu Jun 14 18:33:31 2007 +0200
@@ -437,7 +437,7 @@
       show "z = (z/y)*y"
 	by (simp add: divide_inverse mult_commute [of y] mult_assoc
 		      order_less_imp_not_eq2)
-      show "y \<in> B" .
+      show "y \<in> B" by fact
     qed
   next
     show "z/y \<in> A"
@@ -527,7 +527,7 @@
           show "x = (x/v)*v"
 	    by (simp add: divide_inverse mult_assoc vpos
                           order_less_imp_not_eq2)
-          show "v \<in> A" .
+          show "v \<in> A" by fact
         qed
       qed
     qed
@@ -1280,8 +1280,8 @@
     by (simp add: mult_ac)
   also have "... = x/y" using zpos
     by (simp add: divide_inverse)
-  also have "... < z"
-    by (simp add: pos_divide_less_eq [OF ypos] mult_commute) 
+  also from xless have "... < z"
+    by (simp add: pos_divide_less_eq [OF ypos] mult_commute)
   finally show ?thesis .
 qed
 
diff -r 77645da0db85 -r aaca6a8e5414 src/HOL/Real/RComplete.thy
--- a/src/HOL/Real/RComplete.thy	Thu Jun 14 18:33:29 2007 +0200
+++ b/src/HOL/Real/RComplete.thy	Thu Jun 14 18:33:31 2007 +0200
@@ -59,16 +59,16 @@
     then obtain py where y_is_py: "y = real_of_preal py"
       by (auto simp add: real_gt_zero_preal_Ex)
 
-    obtain a where a_in_P: "a \<in> P" using not_empty_P ..
-    have a_pos: "0 < a" using positive_P ..
+    obtain a where "a \<in> P" using not_empty_P ..
+    with positive_P have a_pos: "0 < a" ..
     then obtain pa where "a = real_of_preal pa"
       by (auto simp add: real_gt_zero_preal_Ex)
-    hence "pa \<in> ?pP" using a_in_P by auto
+    hence "pa \<in> ?pP" using `a \<in> P` by auto
     hence pP_not_empty: "?pP \<noteq> {}" by auto
 
     obtain sup where sup: "\<forall>x \<in> P. x < sup"
       using upper_bound_Ex ..
-    hence  "a < sup" ..
+    from this and `a \<in> P` have "a < sup" ..
     hence "0 < sup" using a_pos by arith
     then obtain possup where "sup = real_of_preal possup"
       by (auto simp add: real_gt_zero_preal_Ex)
@@ -521,9 +521,9 @@
   assumes a1: "real m \<le> r" and a2: "r < real n + 1"
   shows "m \<le> (n::int)"
 proof -
-  have "real m < real n + 1" by (rule order_le_less_trans)
-  also have "... = real(n+1)" by simp
-  finally have "m < n+1" by (simp only: real_of_int_less_iff)
+  have "real m < real n + 1" using a1 a2 by (rule order_le_less_trans)
+  also have "... = real (n + 1)" by simp
+  finally have "m < n + 1" by (simp only: real_of_int_less_iff)
   thus ?thesis by arith
 qed
 
diff -r 77645da0db85 -r aaca6a8e5414 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Thu Jun 14 18:33:29 2007 +0200
+++ b/src/HOL/Ring_and_Field.thy	Thu Jun 14 18:33:31 2007 +0200
@@ -170,6 +170,7 @@
 class division_by_zero = zero + inverse +
   assumes inverse_zero [simp]: "inverse \<^loc>0 = \<^loc>0"
 
+
 subsection {* Distribution rules *}
 
 theorems ring_distrib = right_distrib left_distrib
@@ -343,6 +344,7 @@
 apply (simp add: compare_rls minus_mult_left [symmetric]) 
 done
 
+
 subsection {* Ordering Rules for Multiplication *}
 
 lemma mult_left_le_imp_le:
@@ -386,6 +388,7 @@
 apply (simp_all add: minus_mult_right [symmetric]) 
 done
 
+
 subsection{* Products of Signs *}
 
 lemma mult_pos_pos: "[| (0::'a::ordered_semiring_strict) < a; 0 < b |] ==> 0 < a*b"
@@ -501,6 +504,7 @@
 lemma not_one_less_zero [simp]: "~ (1::'a::ordered_semidom) < 0"
 by (simp add: linorder_not_less) 
 
+
 subsection{*More Monotonicity*}
 
 text{*Strict monotonicity in both arguments*}
@@ -559,6 +563,7 @@
   apply simp
 done
 
+
 subsection{*Cancellation Laws for Relationships With a Common Factor*}
 
 text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},
@@ -621,7 +626,7 @@
 proof (rule ccontr)
   assume "~ a < b"
   hence "b \<le> a" by (simp add: linorder_not_less)
-  hence "c*b \<le> c*a" by (rule mult_left_mono)
+  hence "c*b \<le> c*a" using nonneg by (rule mult_left_mono)
   with this and less show False 
     by (simp add: linorder_not_less [symmetric])
 qed
@@ -632,7 +637,7 @@
 proof (rule ccontr)
   assume "~ a < b"
   hence "b \<le> a" by (simp add: linorder_not_less)
-  hence "b*c \<le> a*c" by (rule mult_right_mono)
+  hence "b*c \<le> a*c" using nonneg by (rule mult_right_mono)
   with this and less show False 
     by (simp add: linorder_not_less [symmetric])
 qed  
@@ -746,6 +751,7 @@
   add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2
   diff_eq_eq eq_diff_eq *)
     
+
 subsection {* Fields *}
 
 lemma right_inverse_eq: "b \<noteq> 0 ==> (a / b = 1) = (a = (b::'a::field))"
@@ -968,6 +974,7 @@
       "inverse (a/b) = b / (a::'a::{field,division_by_zero})"
   by (simp add: divide_inverse mult_commute)
 
+
 subsection {* Calculations with fractions *}
 
 lemma nonzero_mult_divide_cancel_left:
@@ -1038,6 +1045,7 @@
   apply assumption
 done
 
+
 subsubsection{*Special Cancellation Simprules for Division*}
 
 lemma mult_divide_cancel_left_if [simp]:
@@ -1136,6 +1144,7 @@
   apply simp_all
 done
 
+
 subsection {* Ordered Fields *}
 
 lemma positive_imp_inverse_positive: 
@@ -1171,15 +1180,15 @@
   qed
 
 lemma inverse_positive_imp_positive:
-      assumes inv_gt_0: "0 < inverse a"
-          and [simp]:   "a \<noteq> 0"
-        shows "0 < (a::'a::ordered_field)"
-  proof -
+  assumes inv_gt_0: "0 < inverse a"
+    and nz: "a \<noteq> 0"
+  shows "0 < (a::'a::ordered_field)"
+proof -
   have "0 < inverse (inverse a)"
-    by (rule positive_imp_inverse_positive)
+    using inv_gt_0 by (rule positive_imp_inverse_positive)
   thus "0 < a"
-    by (simp add: nonzero_inverse_inverse_eq)
-  qed
+    using nz by (simp add: nonzero_inverse_inverse_eq)
+qed
 
 lemma inverse_positive_iff_positive [simp]:
       "(0 < inverse a) = (0 < (a::'a::{ordered_field,division_by_zero}))"
@@ -1188,15 +1197,15 @@
 done
 
 lemma inverse_negative_imp_negative:
-      assumes inv_less_0: "inverse a < 0"
-          and [simp]:   "a \<noteq> 0"
-        shows "a < (0::'a::ordered_field)"
-  proof -
+  assumes inv_less_0: "inverse a < 0"
+    and nz:  "a \<noteq> 0"
+  shows "a < (0::'a::ordered_field)"
+proof -
   have "inverse (inverse a) < 0"
-    by (rule negative_imp_inverse_negative)
+    using inv_less_0 by (rule negative_imp_inverse_negative)
   thus "a < 0"
-    by (simp add: nonzero_inverse_inverse_eq)
-  qed
+    using nz by (simp add: nonzero_inverse_inverse_eq)
+qed
 
 lemma inverse_negative_iff_negative [simp]:
       "(inverse a < 0) = (a < (0::'a::{ordered_field,division_by_zero}))"
@@ -1334,6 +1343,7 @@
    "(inverse x \<le> 1) = (x \<le> 0 | 1 \<le> (x::'a::{ordered_field,division_by_zero}))"
 by (simp add: linorder_not_less [symmetric] one_less_inverse_iff) 
 
+
 subsection{*Simplification of Inequalities Involving Literal Divisors*}
 
 lemma pos_le_divide_eq: "0 < (c::'a::ordered_field) ==> (a \<le> b/c) = (a*c \<le> b)"
@@ -1500,6 +1510,7 @@
   apply (erule nonzero_divide_eq_eq) 
 done
 
+
 subsection{*Division and Signs*}
 
 lemma zero_less_divide_iff:
@@ -1578,6 +1589,7 @@
   apply simp
 done
 
+
 subsection{*Cancellation Laws for Division*}
 
 lemma divide_cancel_right [simp]:
@@ -1592,6 +1604,7 @@
 apply (simp add: divide_inverse field_mult_cancel_left) 
 done
 
+
 subsection {* Division and the Number One *}
 
 text{*Simplify expressions equated with 1*}
@@ -1629,6 +1642,7 @@
 declare zero_le_divide_1_iff [simp]
 declare divide_le_0_1_iff [simp]
 
+
 subsection {* Ordering Rules for Division *}
 
 lemma divide_strict_right_mono:
@@ -1706,6 +1720,7 @@
   shows "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)"
 by (auto simp add: divide_less_eq)
 
+
 subsection{*Conditional Simplification Rules: No Case Splits*}
 
 lemma le_divide_eq_1_pos [simp]:
@@ -1758,6 +1773,7 @@
   shows "(b/a = 1) = ((a \<noteq> 0 & a = b))"
 by (auto simp add: divide_eq_eq)
 
+
 subsection {* Reasoning about inequalities with division *}
 
 lemma mult_right_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1
@@ -1823,6 +1839,7 @@
 
 declare times_divide_eq [simp]
 
+
 subsection {* Ordered Fields are Dense *}
 
 lemma less_add_one: "a < (a+1::'a::ordered_semidom)"
@@ -1995,6 +2012,7 @@
   apply (simp add: order_less_imp_le);
 done;
 
+
 subsection {* Bounds of products via negative and positive Part *}
 
 lemma mult_le_prts:
@@ -2063,6 +2081,7 @@
   then show ?thesis by simp
 qed
 
+
 subsection {* Theorems for proof tools *}
 
 lemma add_mono_thms_ordered_semiring:
diff -r 77645da0db85 -r aaca6a8e5414 src/HOL/Wellfounded_Recursion.thy
--- a/src/HOL/Wellfounded_Recursion.thy	Thu Jun 14 18:33:29 2007 +0200
+++ b/src/HOL/Wellfounded_Recursion.thy	Thu Jun 14 18:33:31 2007 +0200
@@ -301,7 +301,7 @@
           with A2 show "y \<notin> Q" .
         qed
       qed
-      thus ?thesis ..
+      with `z' \<in> Q` show ?thesis ..
     qed
   qed
 qed
diff -r 77645da0db85 -r aaca6a8e5414 src/HOL/ex/CTL.thy
--- a/src/HOL/ex/CTL.thy	Thu Jun 14 18:33:29 2007 +0200
+++ b/src/HOL/ex/CTL.thy	Thu Jun 14 18:33:31 2007 +0200
@@ -99,7 +99,7 @@
       then have "f (- u) \<subseteq> - u" by auto
       then have "lfp f \<subseteq> - u" by (rule lfp_lowerbound)
       from l and this have "x \<notin> u" by auto
-      then show False by contradiction
+      with `x \<in> u` show False by contradiction
     qed
   qed
   show "- gfp (\<lambda>s. - f (- s)) \<subseteq> lfp f"