# HG changeset patch
# User wenzelm
# Date 1294848867 -3600
# Node ID 276078f01ada4db73a0902a8b3a4b5b6251c628a
# Parent  924106faa45f3417dc549751ef2781f8beefcb75
eliminated global prems;
tuned proofs;

diff -r 924106faa45f -r 276078f01ada src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Wed Jan 12 16:41:49 2011 +0100
+++ b/src/HOL/Algebra/Coset.thy	Wed Jan 12 17:14:27 2011 +0100
@@ -388,7 +388,7 @@
 
 lemma (in group) normalI: 
   "subgroup H G \<Longrightarrow> (\<forall>x \<in> carrier G. H #> x = x <# H) \<Longrightarrow> H \<lhd> G"
-  by (simp add: normal_def normal_axioms_def prems) 
+  by (simp add: normal_def normal_axioms_def is_group)
 
 lemma (in normal) inv_op_closed1:
      "\<lbrakk>x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> (inv x) \<otimes> h \<otimes> x \<in> H"
@@ -532,23 +532,20 @@
   shows "set_inv (H #> x) = H #> (inv x)" 
 proof (simp add: r_coset_def SET_INV_def x inv_mult_group, safe)
   fix h
-  assume "h \<in> H"
+  assume h: "h \<in> H"
   show "inv x \<otimes> inv h \<in> (\<Union>j\<in>H. {j \<otimes> inv x})"
   proof
     show "inv x \<otimes> inv h \<otimes> x \<in> H"
-      by (simp add: inv_op_closed1 prems)
+      by (simp add: inv_op_closed1 h x)
     show "inv x \<otimes> inv h \<in> {inv x \<otimes> inv h \<otimes> x \<otimes> inv x}"
-      by (simp add: prems m_assoc)
+      by (simp add: h x m_assoc)
   qed
-next
-  fix h
-  assume "h \<in> H"
   show "h \<otimes> inv x \<in> (\<Union>j\<in>H. {inv x \<otimes> inv j})"
   proof
     show "x \<otimes> inv h \<otimes> inv x \<in> H"
-      by (simp add: inv_op_closed2 prems)
+      by (simp add: inv_op_closed2 h x)
     show "h \<otimes> inv x \<in> {inv x \<otimes> inv (x \<otimes> inv h \<otimes> inv x)}"
-      by (simp add: prems m_assoc [symmetric] inv_mult_group)
+      by (simp add: h x m_assoc [symmetric] inv_mult_group)
   qed
 qed
 
@@ -580,7 +577,7 @@
      "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
       \<Longrightarrow> (H <#> (H #> x)) #> y = H #> (x \<otimes> y)"
 by (simp add: setmult_rcos_assoc coset_mult_assoc
-              subgroup_mult_id normal.axioms subset prems)
+              subgroup_mult_id normal.axioms subset normal_axioms)
 
 lemma (in normal) rcos_sum:
      "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
@@ -590,7 +587,7 @@
 lemma (in normal) rcosets_mult_eq: "M \<in> rcosets H \<Longrightarrow> H <#> M = M"
   -- {* generalizes @{text subgroup_mult_id} *}
   by (auto simp add: RCOSETS_def subset
-        setmult_rcos_assoc subgroup_mult_id normal.axioms prems)
+        setmult_rcos_assoc subgroup_mult_id normal.axioms normal_axioms)
 
 
 subsubsection{*An Equivalence Relation*}
@@ -676,8 +673,9 @@
   shows "a \<inter> b = {}"
 proof -
   interpret subgroup H G by fact
-  from p show ?thesis apply (simp add: RCOSETS_def r_coset_def)
-    apply (blast intro: rcos_equation prems sym)
+  from p show ?thesis
+    apply (simp add: RCOSETS_def r_coset_def)
+    apply (blast intro: rcos_equation assms sym)
     done
 qed
 
@@ -770,7 +768,7 @@
   show ?thesis
     apply (rule equalityI)
     apply (force simp add: RCOSETS_def r_coset_def)
-    apply (auto simp add: RCOSETS_def intro: rcos_self prems)
+    apply (auto simp add: RCOSETS_def intro: rcos_self assms)
     done
 qed
 
@@ -860,7 +858,7 @@
 
 lemma (in normal) rcosets_inv_mult_group_eq:
      "M \<in> rcosets H \<Longrightarrow> set_inv M <#> M = H"
-by (auto simp add: RCOSETS_def rcos_inv rcos_sum subgroup.subset normal.axioms prems)
+by (auto simp add: RCOSETS_def rcos_inv rcos_sum subgroup.subset normal.axioms normal_axioms)
 
 theorem (in normal) factorgroup_is_group:
   "group (G Mod H)"
@@ -902,7 +900,7 @@
 
 lemma (in group_hom) subgroup_kernel: "subgroup (kernel G H h) G"
 apply (rule subgroup.intro) 
-apply (auto simp add: kernel_def group.intro prems) 
+apply (auto simp add: kernel_def group.intro is_group) 
 done
 
 text{*The kernel of a homomorphism is a normal subgroup*}
diff -r 924106faa45f -r 276078f01ada src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Wed Jan 12 16:41:49 2011 +0100
+++ b/src/HOL/Algebra/Group.thy	Wed Jan 12 17:14:27 2011 +0100
@@ -469,9 +469,9 @@
 lemma (in subgroup) finite_imp_card_positive:
   "finite (carrier G) ==> 0 < card H"
 proof (rule classical)
-  assume "finite (carrier G)" "~ 0 < card H"
+  assume "finite (carrier G)" and a: "~ 0 < card H"
   then have "finite H" by (blast intro: finite_subset [OF subset])
-  with prems have "subgroup {} G" by simp
+  with is_subgroup a have "subgroup {} G" by simp
   with subgroup_nonempty show ?thesis by contradiction
 qed
 
diff -r 924106faa45f -r 276078f01ada src/HOL/Library/Abstract_Rat.thy
--- a/src/HOL/Library/Abstract_Rat.thy	Wed Jan 12 16:41:49 2011 +0100
+++ b/src/HOL/Library/Abstract_Rat.thy	Wed Jan 12 17:14:27 2011 +0100
@@ -44,7 +44,7 @@
     let ?b' = "b div ?g"
     let ?g' = "gcd ?a' ?b'"
     from anz bnz have "?g \<noteq> 0" by simp  with gcd_ge_0_int[of a b] 
-    have gpos: "?g > 0"  by arith
+    have gpos: "?g > 0" by arith
     have gdvd: "?g dvd a" "?g dvd b" by arith+ 
     from zdvd_mult_div_cancel[OF gdvd(1)] zdvd_mult_div_cancel[OF gdvd(2)]
     anz bnz
@@ -140,7 +140,7 @@
     (cases "fst x = 0", auto simp add: gcd_commute_int)
 
 lemma isnormNum_int[simp]: 
-  "isnormNum 0\<^sub>N" "isnormNum (1::int)\<^sub>N" "i \<noteq> 0 \<Longrightarrow> isnormNum i\<^sub>N"
+  "isnormNum 0\<^sub>N" "isnormNum ((1::int)\<^sub>N)" "i \<noteq> 0 \<Longrightarrow> isnormNum (i\<^sub>N)"
   by (simp_all add: isnormNum_def)
 
 
@@ -179,7 +179,7 @@
 definition
   "INum = (\<lambda>(a,b). of_int a / of_int b)"
 
-lemma INum_int [simp]: "INum i\<^sub>N = ((of_int i) ::'a::field)" "INum 0\<^sub>N = (0::'a::field)"
+lemma INum_int [simp]: "INum (i\<^sub>N) = ((of_int i) ::'a::field)" "INum 0\<^sub>N = (0::'a::field)"
   by (simp_all add: INum_def)
 
 lemma isnormNum_unique[simp]: 
@@ -195,9 +195,9 @@
   moreover
   { assume az: "a \<noteq> 0" and bz: "b \<noteq> 0" and a'z: "a'\<noteq>0" and b'z: "b'\<noteq>0"
     from az bz a'z b'z na nb have pos: "b > 0" "b' > 0" by (simp_all add: isnormNum_def)
-    from prems have eq:"a * b' = a'*b" 
+    from H bz b'z have eq:"a * b' = a'*b" 
       by (simp add: INum_def  eq_divide_eq divide_eq_eq of_int_mult[symmetric] del: of_int_mult)
-    from prems have gcd1: "gcd a b = 1" "gcd b a = 1" "gcd a' b' = 1" "gcd b' a' = 1"       
+    from az a'z na nb have gcd1: "gcd a b = 1" "gcd b a = 1" "gcd a' b' = 1" "gcd b' a' = 1"       
       by (simp_all add: isnormNum_def add: gcd_commute_int)
     from eq have raw_dvd: "a dvd a'*b" "b dvd b'*a" "a' dvd a*b'" "b' dvd b*a'"
       apply - 
@@ -208,7 +208,7 @@
       done
     from zdvd_antisym_abs[OF coprime_dvd_mult_int[OF gcd1(2) raw_dvd(2)]
       coprime_dvd_mult_int[OF gcd1(4) raw_dvd(4)]]
-      have eq1: "b = b'" using pos by arith  
+      have eq1: "b = b'" using pos by arith
       with eq have "a = a'" using pos by simp
       with eq1 have ?rhs by simp}
   ultimately show ?rhs by blast
@@ -225,7 +225,6 @@
     of_int (x div d) + (of_int (x mod d)) / ((of_int d)::'a)"
 proof -
   assume "d ~= 0"
-  hence dz: "of_int d \<noteq> (0::'a)" by (simp add: of_int_eq_0_iff)
   let ?t = "of_int (x div d) * ((of_int d)::'a) + of_int(x mod d)"
   let ?f = "\<lambda>x. x / of_int d"
   have "x = (x div d) * d + x mod d"
@@ -234,7 +233,7 @@
     by (simp only: of_int_mult[symmetric] of_int_add [symmetric])
   then have "of_int x / of_int d = ?t / of_int d" 
     using cong[OF refl[of ?f] eq] by simp
-  then show ?thesis by (simp add: add_divide_distrib algebra_simps prems)
+  then show ?thesis by (simp add: add_divide_distrib algebra_simps `d ~= 0`)
 qed
 
 lemma of_int_div: "(d::int) ~= 0 ==> d dvd n ==>
@@ -294,9 +293,9 @@
       have ?thesis using aa' bb' z gz
         of_int_div[where ?'a = 'a, OF gz gcd_dvd1_int[where x="a * b' + b * a'" and y="b*b'"]]  of_int_div[where ?'a = 'a,
         OF gz gcd_dvd2_int[where x="a * b' + b * a'" and y="b*b'"]]
-        by (simp add: x y Nadd_def INum_def normNum_def Let_def add_divide_distrib)}
+        by (simp add: Nadd_def INum_def normNum_def Let_def add_divide_distrib)}
     ultimately have ?thesis using aa' bb' 
-      by (simp add: Nadd_def INum_def normNum_def x y Let_def) }
+      by (simp add: Nadd_def INum_def normNum_def Let_def) }
   ultimately show ?thesis by blast
 qed
 
@@ -512,7 +511,7 @@
     have n0: "isnormNum 0\<^sub>N" by simp
     show ?thesis using nx ny 
       apply (simp only: isnormNum_unique[where ?'a = 'a, OF  Nmul_normN[OF nx ny] n0, symmetric] Nmul[where ?'a = 'a])
-      by (simp add: INum_def split_def isnormNum_def fst_conv snd_conv split: split_if_asm)
+      by (simp add: INum_def split_def isnormNum_def split: split_if_asm)
   }
 qed
 lemma Nneg_Nneg[simp]: "~\<^sub>N (~\<^sub>N c) = c"
@@ -520,7 +519,7 @@
 
 lemma Nmul1[simp]: 
   "isnormNum c \<Longrightarrow> 1\<^sub>N *\<^sub>N c = c" 
-  "isnormNum c \<Longrightarrow> c *\<^sub>N 1\<^sub>N  = c" 
+  "isnormNum c \<Longrightarrow> c *\<^sub>N (1\<^sub>N) = c" 
   apply (simp_all add: Nmul_def Let_def split_def isnormNum_def)
   apply (cases "fst c = 0", simp_all, cases c, simp_all)+
   done
diff -r 924106faa45f -r 276078f01ada src/HOL/Library/BigO.thy
--- a/src/HOL/Library/BigO.thy	Wed Jan 12 16:41:49 2011 +0100
+++ b/src/HOL/Library/BigO.thy	Wed Jan 12 17:14:27 2011 +0100
@@ -351,33 +351,30 @@
   apply (auto simp add: algebra_simps)
   done
 
-lemma bigo_mult5: "ALL x. f x ~= 0 ==>
-    O(f * g) <= (f::'a => ('b::linordered_field)) *o O(g)"
-proof -
-  assume "ALL x. f x ~= 0"
-  show "O(f * g) <= f *o O(g)"
-  proof
-    fix h
-    assume "h : O(f * g)"
-    then have "(%x. 1 / (f x)) * h : (%x. 1 / f x) *o O(f * g)"
-      by auto
-    also have "... <= O((%x. 1 / f x) * (f * g))"
-      by (rule bigo_mult2)
-    also have "(%x. 1 / f x) * (f * g) = g"
-      apply (simp add: func_times) 
-      apply (rule ext)
-      apply (simp add: prems nonzero_divide_eq_eq mult_ac)
-      done
-    finally have "(%x. (1::'b) / f x) * h : O(g)".
-    then have "f * ((%x. (1::'b) / f x) * h) : f *o O(g)"
-      by auto
-    also have "f * ((%x. (1::'b) / f x) * h) = h"
-      apply (simp add: func_times) 
-      apply (rule ext)
-      apply (simp add: prems nonzero_divide_eq_eq mult_ac)
-      done
-    finally show "h : f *o O(g)".
-  qed
+lemma bigo_mult5:
+  assumes "ALL x. f x ~= 0"
+  shows "O(f * g) <= (f::'a => ('b::linordered_field)) *o O(g)"
+proof
+  fix h
+  assume "h : O(f * g)"
+  then have "(%x. 1 / (f x)) * h : (%x. 1 / f x) *o O(f * g)"
+    by auto
+  also have "... <= O((%x. 1 / f x) * (f * g))"
+    by (rule bigo_mult2)
+  also have "(%x. 1 / f x) * (f * g) = g"
+    apply (simp add: func_times) 
+    apply (rule ext)
+    apply (simp add: assms nonzero_divide_eq_eq mult_ac)
+    done
+  finally have "(%x. (1::'b) / f x) * h : O(g)" .
+  then have "f * ((%x. (1::'b) / f x) * h) : f *o O(g)"
+    by auto
+  also have "f * ((%x. (1::'b) / f x) * h) = h"
+    apply (simp add: func_times) 
+    apply (rule ext)
+    apply (simp add: assms nonzero_divide_eq_eq mult_ac)
+    done
+  finally show "h : f *o O(g)" .
 qed
 
 lemma bigo_mult6: "ALL x. f x ~= 0 ==>
@@ -413,7 +410,7 @@
   done
 
 lemma bigo_minus3: "O(-f) = O(f)"
-  by (auto simp add: bigo_def fun_Compl_def abs_minus_cancel)
+  by (auto simp add: bigo_def fun_Compl_def)
 
 lemma bigo_plus_absorb_lemma1: "f : O(g) ==> f +o O(g) <= O(g)"
 proof -
@@ -428,7 +425,7 @@
       from a have "O(f) <= O(g)" by (auto del: subsetI)
       thus ?thesis by (auto del: subsetI)
     qed
-    also have "... <= O(g)" by (simp add: bigo_plus_idemp)
+    also have "... <= O(g)" by simp
     finally show ?thesis .
   qed
 qed
@@ -523,7 +520,7 @@
   apply (rule order_trans)
   apply (rule bigo_mult2)
   apply (simp add: func_times)
-  apply (auto intro!: subsetI simp add: bigo_def elt_set_times_def func_times)
+  apply (auto intro!: simp add: bigo_def elt_set_times_def func_times)
   apply (rule_tac x = "%y. inverse c * x y" in exI)
   apply (simp add: mult_assoc [symmetric] abs_mult)
   apply (rule_tac x = "abs (inverse c) * ca" in exI)
@@ -535,8 +532,7 @@
   done
 
 lemma bigo_const_mult6 [intro]: "(%x. c) *o O(f) <= O(f)"
-  apply (auto intro!: subsetI
-    simp add: bigo_def elt_set_times_def func_times)
+  apply (auto intro!: simp add: bigo_def elt_set_times_def func_times)
   apply (rule_tac x = "ca * (abs c)" in exI)
   apply (rule allI)
   apply (subgoal_tac "ca * abs(c) * abs(f x) = abs(c) * (ca * abs(f x))")
diff -r 924106faa45f -r 276078f01ada src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Wed Jan 12 16:41:49 2011 +0100
+++ b/src/HOL/Library/Float.thy	Wed Jan 12 17:14:27 2011 +0100
@@ -66,7 +66,7 @@
   by (simp only:number_of_float_def Float_num[unfolded number_of_is_id])
 
 lemma float_number_of_int[simp]: "real (Float n 0) = real n"
-  by (simp add: Float_num[unfolded number_of_is_id] real_of_float_simp pow2_def)
+  by simp
 
 lemma pow2_0[simp]: "pow2 0 = 1" by simp
 lemma pow2_1[simp]: "pow2 1 = 2" by simp
@@ -107,7 +107,7 @@
     show ?case by simp
   next
     case (Suc m)
-    show ?case by (auto simp add: algebra_simps pow2_add1 prems)
+    then show ?case by (auto simp add: algebra_simps pow2_add1)
   qed
 next
   case (2 n)
@@ -124,6 +124,7 @@
       apply (subst pow2_neg[of "-a"])
       apply (simp)
       done
+  next
     case (Suc m)
     have a: "int m - (a + -2) =  1 + (int m - a + 1)" by arith
     have b: "int m - -2 = 1 + (int m + 1)" by arith
@@ -138,15 +139,15 @@
       apply (subst pow2_neg[of "int m - a + 1"])
       apply (subst pow2_neg[of "int m + 1"])
       apply auto
-      apply (insert prems)
+      apply (insert Suc)
       apply (auto simp add: algebra_simps)
       done
   qed
 qed
 
-lemma float_components[simp]: "Float (mantissa f) (scale f) = f" by (cases f, auto)
+lemma float_components[simp]: "Float (mantissa f) (scale f) = f" by (cases f) auto
 
-lemma float_split: "\<exists> a b. x = Float a b" by (cases x, auto)
+lemma float_split: "\<exists> a b. x = Float a b" by (cases x) auto
 
 lemma float_split2: "(\<forall> a b. x \<noteq> Float a b) = False" by (auto simp add: float_split)
 
@@ -156,7 +157,9 @@
 by arith
 
 function normfloat :: "float \<Rightarrow> float" where
-"normfloat (Float a b) = (if a \<noteq> 0 \<and> even a then normfloat (Float (a div 2) (b+1)) else if a=0 then Float 0 0 else Float a b)"
+  "normfloat (Float a b) =
+    (if a \<noteq> 0 \<and> even a then normfloat (Float (a div 2) (b+1))
+     else if a=0 then Float 0 0 else Float a b)"
 by pat_completeness auto
 termination by (relation "measure (nat o abs o mantissa)") (auto intro: abs_div_2_less)
 declare normfloat.simps[simp del]
@@ -168,7 +171,7 @@
     by auto
   show ?case
     apply (subst normfloat.simps)
-    apply (auto simp add: float_zero)
+    apply auto
     apply (subst 1[symmetric])
     apply (auto simp add: pow2_add even_def)
     done
@@ -186,7 +189,10 @@
   {
     fix y
     have "0 <= y \<Longrightarrow> 0 < pow2 y"
-      by (induct y, induct_tac n, simp_all add: pow2_add)
+      apply (induct y)
+      apply (induct_tac n)
+      apply (simp_all add: pow2_add)
+      done
   }
   note helper=this
   show ?thesis
@@ -292,7 +298,7 @@
   from 
      float_eq_odd_helper[OF odd2 floateq] 
      float_eq_odd_helper[OF odd1 floateq[symmetric]]
-  have beq: "b = b'"  by arith
+  have beq: "b = b'" by arith
   with floateq show ?thesis by auto
 qed
 
@@ -366,17 +372,17 @@
 end
 
 lemma real_of_float_add[simp]: "real (a + b) = real a + real (b :: float)"
-  by (cases a, cases b, simp add: algebra_simps plus_float.simps, 
+  by (cases a, cases b) (simp add: algebra_simps plus_float.simps, 
       auto simp add: pow2_int[symmetric] pow2_add[symmetric])
 
 lemma real_of_float_minus[simp]: "real (- a) = - real (a :: float)"
-  by (cases a, simp add: uminus_float.simps)
+  by (cases a) (simp add: uminus_float.simps)
 
 lemma real_of_float_sub[simp]: "real (a - b) = real a - real (b :: float)"
-  by (cases a, cases b, simp add: minus_float_def)
+  by (cases a, cases b) (simp add: minus_float_def)
 
 lemma real_of_float_mult[simp]: "real (a*b) = real a * real (b :: float)"
-  by (cases a, cases b, simp add: times_float.simps pow2_add)
+  by (cases a, cases b) (simp add: times_float.simps pow2_add)
 
 lemma real_of_float_0[simp]: "real (0 :: float) = 0"
   by (auto simp add: zero_float_def float_zero)
@@ -419,35 +425,36 @@
 declare real_of_float_simp[simp del]
 
 lemma real_of_float_pprt[simp]: "real (float_pprt a) = pprt (real a)"
-  by (cases a, auto simp add: float_pprt.simps zero_le_float float_le_zero float_zero)
+  by (cases a) (auto simp add: zero_le_float float_le_zero)
 
 lemma real_of_float_nprt[simp]: "real (float_nprt a) = nprt (real a)"
-  by (cases a,  auto simp add: float_nprt.simps zero_le_float float_le_zero float_zero)
+  by (cases a) (auto simp add: zero_le_float float_le_zero)
 
 instance float :: ab_semigroup_add
 proof (intro_classes)
   fix a b c :: float
   show "a + b + c = a + (b + c)"
-    by (cases a, cases b, cases c, auto simp add: algebra_simps power_add[symmetric] plus_float.simps)
+    by (cases a, cases b, cases c)
+      (auto simp add: algebra_simps power_add[symmetric] plus_float.simps)
 next
   fix a b :: float
   show "a + b = b + a"
-    by (cases a, cases b, simp add: plus_float.simps)
+    by (cases a, cases b) (simp add: plus_float.simps)
 qed
 
 instance float :: comm_monoid_mult
 proof (intro_classes)
   fix a b c :: float
   show "a * b * c = a * (b * c)"
-    by (cases a, cases b, cases c, simp add: times_float.simps)
+    by (cases a, cases b, cases c) (simp add: times_float.simps)
 next
   fix a b :: float
   show "a * b = b * a"
-    by (cases a, cases b, simp add: times_float.simps)
+    by (cases a, cases b) (simp add: times_float.simps)
 next
   fix a :: float
   show "1 * a = a"
-    by (cases a, simp add: times_float.simps one_float_def)
+    by (cases a) (simp add: times_float.simps one_float_def)
 qed
 
 (* Floats do NOT form a cancel_semigroup_add: *)
@@ -458,7 +465,7 @@
 proof (intro_classes)
   fix a b c :: float
   show "(a + b) * c = a * c + b * c"
-    by (cases a, cases b, cases c, simp, simp add: plus_float.simps times_float.simps algebra_simps)
+    by (cases a, cases b, cases c) (simp add: plus_float.simps times_float.simps algebra_simps)
 qed
 
 (* Floats do NOT form an order, because "(x < y) = (x <= y & x <> y)" does NOT hold *)
@@ -903,11 +910,31 @@
   and D: "\<And>x y prec. \<lbrakk>0 \<le> x; y < 0; ps = (prec, x, y)\<rbrakk> \<Longrightarrow> P"
   shows P
 proof -
-  obtain prec x y where [simp]: "ps = (prec, x, y)" by (cases ps, auto)
+  obtain prec x y where [simp]: "ps = (prec, x, y)" by (cases ps) auto
   from Y have "y = 0 \<Longrightarrow> P" by auto
-  moreover { assume "0 < y" have P proof (cases "0 \<le> x") case True with A and `0 < y` show P by auto next case False with B and `0 < y` show P by auto qed } 
-  moreover { assume "y < 0" have P proof (cases "0 \<le> x") case True with D and `y < 0` show P by auto next case False with C and `y < 0` show P by auto qed }
-  ultimately show P by (cases "y = 0 \<or> 0 < y \<or> y < 0", auto)
+  moreover {
+    assume "0 < y"
+    have P
+    proof (cases "0 \<le> x")
+      case True
+      with A and `0 < y` show P by auto
+    next
+      case False
+      with B and `0 < y` show P by auto
+    qed
+  } 
+  moreover {
+    assume "y < 0"
+    have P
+    proof (cases "0 \<le> x")
+      case True
+      with D and `y < 0` show P by auto
+    next
+      case False
+      with C and `y < 0` show P by auto
+    qed
+  }
+  ultimately show P by (cases "y = 0 \<or> 0 < y \<or> y < 0") auto
 qed
 
 function lapprox_rat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float"
@@ -1011,10 +1038,14 @@
 lemma rapprox_rat_nonpos_pos: assumes "x \<le> 0" and "0 < y"
   shows "real (rapprox_rat n x y) \<le> 0"
 proof (cases "x = 0") 
-  case True hence "0 \<le> x" by auto show ?thesis unfolding rapprox_rat.simps(2)[OF `0 \<le> x` `0 < y`]
-    unfolding True rapprox_posrat_def Let_def by auto
+  case True
+  hence "0 \<le> x" by auto show ?thesis
+    unfolding rapprox_rat.simps(2)[OF `0 \<le> x` `0 < y`]
+    unfolding True rapprox_posrat_def Let_def
+    by auto
 next
-  case False hence "x < 0" using assms by auto
+  case False
+  hence "x < 0" using assms by auto
   show ?thesis using rapprox_rat_neg[OF `x < 0` `0 < y`] .
 qed
 
@@ -1064,19 +1095,31 @@
 proof (cases x, cases y)
   fix xm xe ym ye :: int
   assume x_eq: "x = Float xm xe" and y_eq: "y = Float ym ye"
-  have "0 \<le> xm" using `0 \<le> x`[unfolded x_eq le_float_def real_of_float_simp real_of_float_0 zero_le_mult_iff] by auto
-  have "0 < ym" using `0 < y`[unfolded y_eq less_float_def real_of_float_simp real_of_float_0 zero_less_mult_iff] by auto
+  have "0 \<le> xm"
+    using `0 \<le> x`[unfolded x_eq le_float_def real_of_float_simp real_of_float_0 zero_le_mult_iff]
+    by auto
+  have "0 < ym"
+    using `0 < y`[unfolded y_eq less_float_def real_of_float_simp real_of_float_0 zero_less_mult_iff]
+    by auto
 
-  have "\<And>n. 0 \<le> real (Float 1 n)" unfolding real_of_float_simp using zero_le_pow2 by auto
-  moreover have "0 \<le> real (lapprox_rat prec xm ym)" by (rule order_trans[OF _ lapprox_rat_bottom[OF `0 \<le> xm` `0 < ym`]], auto simp add: `0 \<le> xm` pos_imp_zdiv_nonneg_iff[OF `0 < ym`])
+  have "\<And>n. 0 \<le> real (Float 1 n)"
+    unfolding real_of_float_simp using zero_le_pow2 by auto
+  moreover have "0 \<le> real (lapprox_rat prec xm ym)"
+    apply (rule order_trans[OF _ lapprox_rat_bottom[OF `0 \<le> xm` `0 < ym`]])
+    apply (auto simp add: `0 \<le> xm` pos_imp_zdiv_nonneg_iff[OF `0 < ym`])
+    done
   ultimately show "0 \<le> float_divl prec x y"
-    unfolding x_eq y_eq float_divl.simps Let_def le_float_def real_of_float_0 by (auto intro!: mult_nonneg_nonneg)
+    unfolding x_eq y_eq float_divl.simps Let_def le_float_def real_of_float_0
+    by (auto intro!: mult_nonneg_nonneg)
 qed
 
-lemma float_divl_pos_less1_bound: assumes "0 < x" and "x < 1" and "0 < prec" shows "1 \<le> float_divl prec 1 x"
+lemma float_divl_pos_less1_bound:
+  assumes "0 < x" and "x < 1" and "0 < prec"
+  shows "1 \<le> float_divl prec 1 x"
 proof (cases x)
   case (Float m e)
-  from `0 < x` `x < 1` have "0 < m" "e < 0" using float_pos_m_pos float_pos_less1_e_neg unfolding Float by auto
+  from `0 < x` `x < 1` have "0 < m" "e < 0"
+    using float_pos_m_pos float_pos_less1_e_neg unfolding Float by auto
   let ?b = "nat (bitlen m)" and ?e = "nat (-e)"
   have "1 \<le> m" and "m \<noteq> 0" using `0 < m` by auto
   with bitlen_bounds[OF `0 < m`] have "m < 2^?b" and "(2::int) \<le> 2^?b" by auto
@@ -1087,22 +1130,29 @@
 
   from float_less1_mantissa_bound `0 < x` `x < 1` Float 
   have "m < 2^?e" by auto
-  with bitlen_bounds[OF `0 < m`, THEN conjunct1]
-  have "(2::int)^nat (bitlen m - 1) < 2^?e" by (rule order_le_less_trans)
+  with bitlen_bounds[OF `0 < m`, THEN conjunct1] have "(2::int)^nat (bitlen m - 1) < 2^?e"
+    by (rule order_le_less_trans)
   from power_less_imp_less_exp[OF _ this]
   have "bitlen m \<le> - e" by auto
   hence "(2::real)^?b \<le> 2^?e" by auto
-  hence "(2::real)^?b * inverse (2^?b) \<le> 2^?e * inverse (2^?b)" by (rule mult_right_mono, auto)
+  hence "(2::real)^?b * inverse (2^?b) \<le> 2^?e * inverse (2^?b)"
+    by (rule mult_right_mono) auto
   hence "(1::real) \<le> 2^?e * inverse (2^?b)" by auto
   also
   let ?d = "real (2 ^ nat (int prec + bitlen m - 1) div m) * inverse (2 ^ nat (int prec + bitlen m - 1))"
-  { have "2^(prec - 1) * m \<le> 2^(prec - 1) * 2^?b" using `m < 2^?b`[THEN less_imp_le] by (rule mult_left_mono, auto)
-    also have "\<dots> = 2 ^ nat (int prec + bitlen m - 1)" unfolding pow_split zpower_zadd_distrib by auto
-    finally have "2^(prec - 1) * m div m \<le> 2 ^ nat (int prec + bitlen m - 1) div m" using `0 < m` by (rule zdiv_mono1)
-    hence "2^(prec - 1) \<le> 2 ^ nat (int prec + bitlen m - 1) div m" unfolding div_mult_self2_is_id[OF `m \<noteq> 0`] .
+  {
+    have "2^(prec - 1) * m \<le> 2^(prec - 1) * 2^?b"
+      using `m < 2^?b`[THEN less_imp_le] by (rule mult_left_mono) auto
+    also have "\<dots> = 2 ^ nat (int prec + bitlen m - 1)"
+      unfolding pow_split zpower_zadd_distrib by auto
+    finally have "2^(prec - 1) * m div m \<le> 2 ^ nat (int prec + bitlen m - 1) div m"
+      using `0 < m` by (rule zdiv_mono1)
+    hence "2^(prec - 1) \<le> 2 ^ nat (int prec + bitlen m - 1) div m"
+      unfolding div_mult_self2_is_id[OF `m \<noteq> 0`] .
     hence "2^(prec - 1) * inverse (2 ^ nat (int prec + bitlen m - 1)) \<le> ?d"
-      unfolding real_of_int_le_iff[of "2^(prec - 1)", symmetric] by auto }
-  from mult_left_mono[OF this[unfolded pow_split power_add inverse_mult_distrib mult_assoc[symmetric] right_inverse[OF pow_not0] mult_1_left], of "2^?e"]
+      unfolding real_of_int_le_iff[of "2^(prec - 1)", symmetric] by auto
+  }
+  from mult_left_mono[OF this [unfolded pow_split power_add inverse_mult_distrib mult_assoc[symmetric] right_inverse[OF pow_not0] mult_1_left], of "2^?e"]
   have "2^?e * inverse (2^?b) \<le> 2^?e * ?d" unfolding pow_split power_add by auto
   finally have "1 \<le> 2^?e * ?d" .
   
@@ -1110,8 +1160,11 @@
   have "bitlen 1 = 1" using bitlen.simps by auto
   
   show ?thesis 
-    unfolding one_float_def Float float_divl.simps Let_def lapprox_rat.simps(2)[OF zero_le_one `0 < m`] lapprox_posrat_def `bitlen 1 = 1`
-    unfolding le_float_def real_of_float_mult normfloat real_of_float_simp pow2_minus pow2_int e_nat
+    unfolding one_float_def Float float_divl.simps Let_def
+      lapprox_rat.simps(2)[OF zero_le_one `0 < m`]
+      lapprox_posrat_def `bitlen 1 = 1`
+    unfolding le_float_def real_of_float_mult normfloat real_of_float_simp
+      pow2_minus pow2_int e_nat
     using `1 \<le> 2^?e * ?d` by (auto simp add: pow2_def)
 qed
 
diff -r 924106faa45f -r 276078f01ada src/HOL/Library/Lattice_Algebras.thy
--- a/src/HOL/Library/Lattice_Algebras.thy	Wed Jan 12 16:41:49 2011 +0100
+++ b/src/HOL/Library/Lattice_Algebras.thy	Wed Jan 12 17:14:27 2011 +0100
@@ -253,7 +253,7 @@
   "a + a \<le> 0 \<longleftrightarrow> a \<le> 0" 
 proof -
   have "a + a \<le> 0 \<longleftrightarrow> 0 \<le> - (a + a)" by (subst le_minus_iff, simp)
-  moreover have "\<dots> \<longleftrightarrow> a \<le> 0" by (simp add: zero_le_double_add_iff_zero_le_single_add)
+  moreover have "\<dots> \<longleftrightarrow> a \<le> 0" by simp
   ultimately show ?thesis by blast
 qed
 
@@ -261,7 +261,7 @@
   "a + a < 0 \<longleftrightarrow> a < 0"
 proof -
   have "a + a < 0 \<longleftrightarrow> 0 < - (a + a)" by (subst less_minus_iff, simp)
-  moreover have "\<dots> \<longleftrightarrow> a < 0" by (simp add: zero_less_double_add_iff_zero_less_single_add)
+  moreover have "\<dots> \<longleftrightarrow> a < 0" by simp
   ultimately show ?thesis by blast
 qed
 
@@ -428,7 +428,7 @@
 instance lattice_ring \<subseteq> ordered_ring_abs
 proof
   fix a b :: "'a\<Colon> lattice_ring"
-  assume "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0)"
+  assume a: "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0)"
   show "abs (a*b) = abs a * abs b"
   proof -
     have s: "(0 <= a*b) | (a*b <= 0)"
@@ -437,7 +437,7 @@
       apply (rule_tac contrapos_np[of "a*b <= 0"])
       apply (simp)
       apply (rule_tac split_mult_neg_le)
-      apply (insert prems)
+      apply (insert a)
       apply (blast)
       done
     have mulprts: "a * b = (pprt a + nprt a) * (pprt b + nprt b)"
@@ -447,7 +447,7 @@
       assume "0 <= a * b"
       then show ?thesis
         apply (simp_all add: mulprts abs_prts)
-        apply (insert prems)
+        apply (insert a)
         apply (auto simp add: 
           algebra_simps 
           iffD1[OF zero_le_iff_zero_nprt] iffD1[OF le_zero_iff_zero_pprt]
@@ -460,7 +460,7 @@
       with s have "a*b <= 0" by simp
       then show ?thesis
         apply (simp_all add: mulprts abs_prts)
-        apply (insert prems)
+        apply (insert a)
         apply (auto simp add: algebra_simps)
         apply(drule (1) mult_nonneg_nonneg[of a b],simp)
         apply(drule (1) mult_nonpos_nonpos[of a b],simp)
@@ -485,31 +485,31 @@
   then have "a * b = pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
     by (simp add: algebra_simps)
   moreover have "pprt a * pprt b <= pprt a2 * pprt b2"
-    by (simp_all add: prems mult_mono)
+    by (simp_all add: assms mult_mono)
   moreover have "pprt a * nprt b <= pprt a1 * nprt b2"
   proof -
     have "pprt a * nprt b <= pprt a * nprt b2"
-      by (simp add: mult_left_mono prems)
+      by (simp add: mult_left_mono assms)
     moreover have "pprt a * nprt b2 <= pprt a1 * nprt b2"
-      by (simp add: mult_right_mono_neg prems)
+      by (simp add: mult_right_mono_neg assms)
     ultimately show ?thesis
       by simp
   qed
   moreover have "nprt a * pprt b <= nprt a2 * pprt b1"
   proof - 
     have "nprt a * pprt b <= nprt a2 * pprt b"
-      by (simp add: mult_right_mono prems)
+      by (simp add: mult_right_mono assms)
     moreover have "nprt a2 * pprt b <= nprt a2 * pprt b1"
-      by (simp add: mult_left_mono_neg prems)
+      by (simp add: mult_left_mono_neg assms)
     ultimately show ?thesis
       by simp
   qed
   moreover have "nprt a * nprt b <= nprt a1 * nprt b1"
   proof -
     have "nprt a * nprt b <= nprt a * nprt b1"
-      by (simp add: mult_left_mono_neg prems)
+      by (simp add: mult_left_mono_neg assms)
     moreover have "nprt a * nprt b1 <= nprt a1 * nprt b1"
-      by (simp add: mult_right_mono_neg prems)
+      by (simp add: mult_right_mono_neg assms)
     ultimately show ?thesis
       by simp
   qed
@@ -526,9 +526,9 @@
   shows
   "a * b >= nprt a1 * pprt b2 + nprt a2 * nprt b2 + pprt a1 * pprt b1 + pprt a2 * nprt b1"
 proof - 
-  from prems have a1:"- a2 <= -a" by auto
-  from prems have a2: "-a <= -a1" by auto
-  from mult_le_prts[of "-a2" "-a" "-a1" "b1" b "b2", OF a1 a2 prems(3) prems(4), simplified nprt_neg pprt_neg] 
+  from assms have a1:"- a2 <= -a" by auto
+  from assms have a2: "-a <= -a1" by auto
+  from mult_le_prts[of "-a2" "-a" "-a1" "b1" b "b2", OF a1 a2 assms(3) assms(4), simplified nprt_neg pprt_neg] 
   have le: "- (a * b) <= - nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1" by simp  
   then have "-(- nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1) <= a * b"
     by (simp only: minus_le_iff)
diff -r 924106faa45f -r 276078f01ada src/HOL/ZF/Games.thy
--- a/src/HOL/ZF/Games.thy	Wed Jan 12 16:41:49 2011 +0100
+++ b/src/HOL/ZF/Games.thy	Wed Jan 12 17:14:27 2011 +0100
@@ -165,7 +165,7 @@
   shows "opt \<in> games_lfp"
   apply (rule games_option_stable[where g=g])
   apply (simp add: games_lfp_unfold[symmetric])
-  apply (simp_all add: prems)
+  apply (simp_all add: assms)
   done
 
 lemma is_option_of_imp_games:
@@ -466,10 +466,10 @@
         proof -
           { fix xr
             assume xr:"zin xr (right_options x)"
-            assume "ge_game (z, xr)"
+            assume a: "ge_game (z, xr)"
             have "ge_game (y, xr)"
               apply (rule 1[rule_format, where y="[y,z,xr]"])
-              apply (auto intro: xr lprod_3_1 simp add: prems)
+              apply (auto intro: xr lprod_3_1 simp add: goal1 a)
               done
             moreover from xr have "\<not> ge_game (y, xr)"
               by (simp add: goal1(2)[simplified ge_game_eq[of x y], rule_format, of xr, simplified xr])
@@ -478,10 +478,10 @@
           note xr = this
           { fix zl
             assume zl:"zin zl (left_options z)"
-            assume "ge_game (zl, x)"
+            assume a: "ge_game (zl, x)"
             have "ge_game (zl, y)"
               apply (rule 1[rule_format, where y="[zl,x,y]"])
-              apply (auto intro: zl lprod_3_2 simp add: prems)
+              apply (auto intro: zl lprod_3_2 simp add: goal1 a)
               done
             moreover from zl have "\<not> ge_game (zl, y)"
               by (simp add: goal1(3)[simplified ge_game_eq[of y z], rule_format, of zl, simplified zl])
@@ -495,7 +495,7 @@
     qed
   } 
   note trans = this[of "[x, y, z]", simplified, rule_format]    
-  with prems show ?thesis by blast
+  with assms show ?thesis by blast
 qed
 
 lemma eq_game_trans: "eq_game a b \<Longrightarrow> eq_game b c \<Longrightarrow> eq_game a c"
@@ -522,7 +522,7 @@
     by (auto simp add: 
       plus_game.simps[where G=G and H=H] 
       plus_game.simps[where G=H and H=G]
-      Game_ext zet_ext_eq zunion zimage_iff prems)
+      Game_ext zet_ext_eq zunion zimage_iff 1)
 qed
 
 lemma game_ext_eq: "(G = H) = (left_options G = left_options H \<and> right_options G = right_options H)"
@@ -545,10 +545,10 @@
     have "H = zero_game \<longrightarrow> plus_game G H = G "
     proof (induct G H rule: plus_game.induct, rule impI)
       case (goal1 G H)
-      note induct_hyp = prems[simplified goal1, simplified] and prems
+      note induct_hyp = this[simplified goal1, simplified] and this
       show ?case
         apply (simp only: plus_game.simps[where G=G and H=H])
-        apply (simp add: game_ext_eq prems)
+        apply (simp add: game_ext_eq goal1)
         apply (auto simp add: 
           zimage_cong[where f = "\<lambda> g. plus_game g zero_game" and g = "id"] 
           induct_hyp)
@@ -626,7 +626,7 @@
     by (auto simp add: opt_ops
       neg_game.simps[of "plus_game G H"]
       plus_game.simps[of "neg_game G" "neg_game H"]
-      Game_ext zet_ext_eq zunion zimage_iff prems)
+      Game_ext zet_ext_eq zunion zimage_iff 1)
 qed
 
 lemma eq_game_plus_inverse: "eq_game (plus_game x (neg_game x)) zero_game"
@@ -635,7 +635,7 @@
   { fix y
     assume "zin y (options x)"
     then have "eq_game (plus_game y (neg_game y)) zero_game"
-      by (auto simp add: prems)
+      by (auto simp add: goal1)
   }
   note ihyp = this
   {
@@ -645,7 +645,7 @@
       apply (subst ge_game.simps, simp)
       apply (rule exI[where x="plus_game y (neg_game y)"])
       apply (auto simp add: ihyp[of y, simplified y right_imp_options eq_game_def])
-      apply (auto simp add: left_options_plus left_options_neg zunion zimage_iff intro: prems)
+      apply (auto simp add: left_options_plus left_options_neg zunion zimage_iff intro: y)
       done
   }
   note case1 = this
@@ -656,7 +656,7 @@
       apply (subst ge_game.simps, simp)
       apply (rule exI[where x="plus_game y (neg_game y)"])
       apply (auto simp add: ihyp[of y, simplified y left_imp_options eq_game_def])
-      apply (auto simp add: left_options_plus zunion zimage_iff intro: prems)
+      apply (auto simp add: left_options_plus zunion zimage_iff intro: y)
       done
   }
   note case2 = this
@@ -667,7 +667,7 @@
       apply (subst ge_game.simps, simp)
       apply (rule exI[where x="plus_game y (neg_game y)"])
       apply (auto simp add: ihyp[of y, simplified y left_imp_options eq_game_def])
-      apply (auto simp add: right_options_plus right_options_neg zunion zimage_iff intro: prems)
+      apply (auto simp add: right_options_plus right_options_neg zunion zimage_iff intro: y)
       done
   }
   note case3 = this
@@ -678,7 +678,7 @@
       apply (subst ge_game.simps, simp)
       apply (rule exI[where x="plus_game y (neg_game y)"])
       apply (auto simp add: ihyp[of y, simplified y right_imp_options eq_game_def])
-      apply (auto simp add: right_options_plus zunion zimage_iff intro: prems)
+      apply (auto simp add: right_options_plus zunion zimage_iff intro: y)
       done
   }
   note case4 = this
diff -r 924106faa45f -r 276078f01ada src/HOL/ZF/LProd.thy
--- a/src/HOL/ZF/LProd.thy	Wed Jan 12 16:41:49 2011 +0100
+++ b/src/HOL/ZF/LProd.thy	Wed Jan 12 17:14:27 2011 +0100
@@ -42,12 +42,12 @@
   show ?case by (auto intro: lprod_single step)
 next
   case (lprod_list ah at bh bt a b)
-  from prems have transR: "trans R" by auto
+  then have transR: "trans R" by auto
   have as: "multiset_of (ah @ a # at) = multiset_of (ah @ at) + {#a#}" (is "_ = ?ma + _")
     by (simp add: algebra_simps)
   have bs: "multiset_of (bh @ b # bt) = multiset_of (bh @ bt) + {#b#}" (is "_ = ?mb + _")
     by (simp add: algebra_simps)
-  from prems have "(?ma, ?mb) \<in> mult R"
+  from lprod_list have "(?ma, ?mb) \<in> mult R"
     by auto
   with mult_implies_one_step[OF transR] have 
     "\<exists>I J K. ?mb = I + J \<and> ?ma = I + K \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_of K. \<exists>j\<in>set_of J. (k, j) \<in> R)"
@@ -136,12 +136,12 @@
 
 lemma lprod_3_1: assumes "(x', x) \<in> R" shows "([y, z, x'], [x, y, z]) \<in> lprod R"
   apply (rule lprod_list[where a="y" and b="y" and ah="[]" and at="[z,x']" and bh="[x]" and bt="[z]", simplified])
-  apply (auto simp add: lprod_2_1 prems)
+  apply (auto simp add: lprod_2_1 assms)
   done
 
 lemma lprod_3_2: assumes "(z',z) \<in> R" shows "([z', x, y], [x,y,z]) \<in> lprod R"
   apply (rule lprod_list[where a="y" and b="y" and ah="[z',x]" and at="[]" and bh="[x]" and bt="[z]", simplified])
-  apply (auto simp add: lprod_2_2 prems)
+  apply (auto simp add: lprod_2_2 assms)
   done
 
 lemma lprod_3_3: assumes xr: "(xr, x) \<in> R" shows "([xr, y, z], [x, y, z]) \<in> lprod R"