eliminated global prems;
authorwenzelm
Wed Jan 12 17:14:27 2011 +0100 (2011-01-12)
changeset 41528276078f01ada
parent 41527 924106faa45f
child 41529 ba60efa2fd08
eliminated global prems;
tuned proofs;
src/HOL/Algebra/Coset.thy
src/HOL/Algebra/Group.thy
src/HOL/Library/Abstract_Rat.thy
src/HOL/Library/BigO.thy
src/HOL/Library/Float.thy
src/HOL/Library/Lattice_Algebras.thy
src/HOL/ZF/Games.thy
src/HOL/ZF/LProd.thy
     1.1 --- a/src/HOL/Algebra/Coset.thy	Wed Jan 12 16:41:49 2011 +0100
     1.2 +++ b/src/HOL/Algebra/Coset.thy	Wed Jan 12 17:14:27 2011 +0100
     1.3 @@ -388,7 +388,7 @@
     1.4  
     1.5  lemma (in group) normalI: 
     1.6    "subgroup H G \<Longrightarrow> (\<forall>x \<in> carrier G. H #> x = x <# H) \<Longrightarrow> H \<lhd> G"
     1.7 -  by (simp add: normal_def normal_axioms_def prems) 
     1.8 +  by (simp add: normal_def normal_axioms_def is_group)
     1.9  
    1.10  lemma (in normal) inv_op_closed1:
    1.11       "\<lbrakk>x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> (inv x) \<otimes> h \<otimes> x \<in> H"
    1.12 @@ -532,23 +532,20 @@
    1.13    shows "set_inv (H #> x) = H #> (inv x)" 
    1.14  proof (simp add: r_coset_def SET_INV_def x inv_mult_group, safe)
    1.15    fix h
    1.16 -  assume "h \<in> H"
    1.17 +  assume h: "h \<in> H"
    1.18    show "inv x \<otimes> inv h \<in> (\<Union>j\<in>H. {j \<otimes> inv x})"
    1.19    proof
    1.20      show "inv x \<otimes> inv h \<otimes> x \<in> H"
    1.21 -      by (simp add: inv_op_closed1 prems)
    1.22 +      by (simp add: inv_op_closed1 h x)
    1.23      show "inv x \<otimes> inv h \<in> {inv x \<otimes> inv h \<otimes> x \<otimes> inv x}"
    1.24 -      by (simp add: prems m_assoc)
    1.25 +      by (simp add: h x m_assoc)
    1.26    qed
    1.27 -next
    1.28 -  fix h
    1.29 -  assume "h \<in> H"
    1.30    show "h \<otimes> inv x \<in> (\<Union>j\<in>H. {inv x \<otimes> inv j})"
    1.31    proof
    1.32      show "x \<otimes> inv h \<otimes> inv x \<in> H"
    1.33 -      by (simp add: inv_op_closed2 prems)
    1.34 +      by (simp add: inv_op_closed2 h x)
    1.35      show "h \<otimes> inv x \<in> {inv x \<otimes> inv (x \<otimes> inv h \<otimes> inv x)}"
    1.36 -      by (simp add: prems m_assoc [symmetric] inv_mult_group)
    1.37 +      by (simp add: h x m_assoc [symmetric] inv_mult_group)
    1.38    qed
    1.39  qed
    1.40  
    1.41 @@ -580,7 +577,7 @@
    1.42       "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
    1.43        \<Longrightarrow> (H <#> (H #> x)) #> y = H #> (x \<otimes> y)"
    1.44  by (simp add: setmult_rcos_assoc coset_mult_assoc
    1.45 -              subgroup_mult_id normal.axioms subset prems)
    1.46 +              subgroup_mult_id normal.axioms subset normal_axioms)
    1.47  
    1.48  lemma (in normal) rcos_sum:
    1.49       "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
    1.50 @@ -590,7 +587,7 @@
    1.51  lemma (in normal) rcosets_mult_eq: "M \<in> rcosets H \<Longrightarrow> H <#> M = M"
    1.52    -- {* generalizes @{text subgroup_mult_id} *}
    1.53    by (auto simp add: RCOSETS_def subset
    1.54 -        setmult_rcos_assoc subgroup_mult_id normal.axioms prems)
    1.55 +        setmult_rcos_assoc subgroup_mult_id normal.axioms normal_axioms)
    1.56  
    1.57  
    1.58  subsubsection{*An Equivalence Relation*}
    1.59 @@ -676,8 +673,9 @@
    1.60    shows "a \<inter> b = {}"
    1.61  proof -
    1.62    interpret subgroup H G by fact
    1.63 -  from p show ?thesis apply (simp add: RCOSETS_def r_coset_def)
    1.64 -    apply (blast intro: rcos_equation prems sym)
    1.65 +  from p show ?thesis
    1.66 +    apply (simp add: RCOSETS_def r_coset_def)
    1.67 +    apply (blast intro: rcos_equation assms sym)
    1.68      done
    1.69  qed
    1.70  
    1.71 @@ -770,7 +768,7 @@
    1.72    show ?thesis
    1.73      apply (rule equalityI)
    1.74      apply (force simp add: RCOSETS_def r_coset_def)
    1.75 -    apply (auto simp add: RCOSETS_def intro: rcos_self prems)
    1.76 +    apply (auto simp add: RCOSETS_def intro: rcos_self assms)
    1.77      done
    1.78  qed
    1.79  
    1.80 @@ -860,7 +858,7 @@
    1.81  
    1.82  lemma (in normal) rcosets_inv_mult_group_eq:
    1.83       "M \<in> rcosets H \<Longrightarrow> set_inv M <#> M = H"
    1.84 -by (auto simp add: RCOSETS_def rcos_inv rcos_sum subgroup.subset normal.axioms prems)
    1.85 +by (auto simp add: RCOSETS_def rcos_inv rcos_sum subgroup.subset normal.axioms normal_axioms)
    1.86  
    1.87  theorem (in normal) factorgroup_is_group:
    1.88    "group (G Mod H)"
    1.89 @@ -902,7 +900,7 @@
    1.90  
    1.91  lemma (in group_hom) subgroup_kernel: "subgroup (kernel G H h) G"
    1.92  apply (rule subgroup.intro) 
    1.93 -apply (auto simp add: kernel_def group.intro prems) 
    1.94 +apply (auto simp add: kernel_def group.intro is_group) 
    1.95  done
    1.96  
    1.97  text{*The kernel of a homomorphism is a normal subgroup*}
     2.1 --- a/src/HOL/Algebra/Group.thy	Wed Jan 12 16:41:49 2011 +0100
     2.2 +++ b/src/HOL/Algebra/Group.thy	Wed Jan 12 17:14:27 2011 +0100
     2.3 @@ -469,9 +469,9 @@
     2.4  lemma (in subgroup) finite_imp_card_positive:
     2.5    "finite (carrier G) ==> 0 < card H"
     2.6  proof (rule classical)
     2.7 -  assume "finite (carrier G)" "~ 0 < card H"
     2.8 +  assume "finite (carrier G)" and a: "~ 0 < card H"
     2.9    then have "finite H" by (blast intro: finite_subset [OF subset])
    2.10 -  with prems have "subgroup {} G" by simp
    2.11 +  with is_subgroup a have "subgroup {} G" by simp
    2.12    with subgroup_nonempty show ?thesis by contradiction
    2.13  qed
    2.14  
     3.1 --- a/src/HOL/Library/Abstract_Rat.thy	Wed Jan 12 16:41:49 2011 +0100
     3.2 +++ b/src/HOL/Library/Abstract_Rat.thy	Wed Jan 12 17:14:27 2011 +0100
     3.3 @@ -44,7 +44,7 @@
     3.4      let ?b' = "b div ?g"
     3.5      let ?g' = "gcd ?a' ?b'"
     3.6      from anz bnz have "?g \<noteq> 0" by simp  with gcd_ge_0_int[of a b] 
     3.7 -    have gpos: "?g > 0"  by arith
     3.8 +    have gpos: "?g > 0" by arith
     3.9      have gdvd: "?g dvd a" "?g dvd b" by arith+ 
    3.10      from zdvd_mult_div_cancel[OF gdvd(1)] zdvd_mult_div_cancel[OF gdvd(2)]
    3.11      anz bnz
    3.12 @@ -140,7 +140,7 @@
    3.13      (cases "fst x = 0", auto simp add: gcd_commute_int)
    3.14  
    3.15  lemma isnormNum_int[simp]: 
    3.16 -  "isnormNum 0\<^sub>N" "isnormNum (1::int)\<^sub>N" "i \<noteq> 0 \<Longrightarrow> isnormNum i\<^sub>N"
    3.17 +  "isnormNum 0\<^sub>N" "isnormNum ((1::int)\<^sub>N)" "i \<noteq> 0 \<Longrightarrow> isnormNum (i\<^sub>N)"
    3.18    by (simp_all add: isnormNum_def)
    3.19  
    3.20  
    3.21 @@ -179,7 +179,7 @@
    3.22  definition
    3.23    "INum = (\<lambda>(a,b). of_int a / of_int b)"
    3.24  
    3.25 -lemma INum_int [simp]: "INum i\<^sub>N = ((of_int i) ::'a::field)" "INum 0\<^sub>N = (0::'a::field)"
    3.26 +lemma INum_int [simp]: "INum (i\<^sub>N) = ((of_int i) ::'a::field)" "INum 0\<^sub>N = (0::'a::field)"
    3.27    by (simp_all add: INum_def)
    3.28  
    3.29  lemma isnormNum_unique[simp]: 
    3.30 @@ -195,9 +195,9 @@
    3.31    moreover
    3.32    { assume az: "a \<noteq> 0" and bz: "b \<noteq> 0" and a'z: "a'\<noteq>0" and b'z: "b'\<noteq>0"
    3.33      from az bz a'z b'z na nb have pos: "b > 0" "b' > 0" by (simp_all add: isnormNum_def)
    3.34 -    from prems have eq:"a * b' = a'*b" 
    3.35 +    from H bz b'z have eq:"a * b' = a'*b" 
    3.36        by (simp add: INum_def  eq_divide_eq divide_eq_eq of_int_mult[symmetric] del: of_int_mult)
    3.37 -    from prems have gcd1: "gcd a b = 1" "gcd b a = 1" "gcd a' b' = 1" "gcd b' a' = 1"       
    3.38 +    from az a'z na nb have gcd1: "gcd a b = 1" "gcd b a = 1" "gcd a' b' = 1" "gcd b' a' = 1"       
    3.39        by (simp_all add: isnormNum_def add: gcd_commute_int)
    3.40      from eq have raw_dvd: "a dvd a'*b" "b dvd b'*a" "a' dvd a*b'" "b' dvd b*a'"
    3.41        apply - 
    3.42 @@ -208,7 +208,7 @@
    3.43        done
    3.44      from zdvd_antisym_abs[OF coprime_dvd_mult_int[OF gcd1(2) raw_dvd(2)]
    3.45        coprime_dvd_mult_int[OF gcd1(4) raw_dvd(4)]]
    3.46 -      have eq1: "b = b'" using pos by arith  
    3.47 +      have eq1: "b = b'" using pos by arith
    3.48        with eq have "a = a'" using pos by simp
    3.49        with eq1 have ?rhs by simp}
    3.50    ultimately show ?rhs by blast
    3.51 @@ -225,7 +225,6 @@
    3.52      of_int (x div d) + (of_int (x mod d)) / ((of_int d)::'a)"
    3.53  proof -
    3.54    assume "d ~= 0"
    3.55 -  hence dz: "of_int d \<noteq> (0::'a)" by (simp add: of_int_eq_0_iff)
    3.56    let ?t = "of_int (x div d) * ((of_int d)::'a) + of_int(x mod d)"
    3.57    let ?f = "\<lambda>x. x / of_int d"
    3.58    have "x = (x div d) * d + x mod d"
    3.59 @@ -234,7 +233,7 @@
    3.60      by (simp only: of_int_mult[symmetric] of_int_add [symmetric])
    3.61    then have "of_int x / of_int d = ?t / of_int d" 
    3.62      using cong[OF refl[of ?f] eq] by simp
    3.63 -  then show ?thesis by (simp add: add_divide_distrib algebra_simps prems)
    3.64 +  then show ?thesis by (simp add: add_divide_distrib algebra_simps `d ~= 0`)
    3.65  qed
    3.66  
    3.67  lemma of_int_div: "(d::int) ~= 0 ==> d dvd n ==>
    3.68 @@ -294,9 +293,9 @@
    3.69        have ?thesis using aa' bb' z gz
    3.70          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,
    3.71          OF gz gcd_dvd2_int[where x="a * b' + b * a'" and y="b*b'"]]
    3.72 -        by (simp add: x y Nadd_def INum_def normNum_def Let_def add_divide_distrib)}
    3.73 +        by (simp add: Nadd_def INum_def normNum_def Let_def add_divide_distrib)}
    3.74      ultimately have ?thesis using aa' bb' 
    3.75 -      by (simp add: Nadd_def INum_def normNum_def x y Let_def) }
    3.76 +      by (simp add: Nadd_def INum_def normNum_def Let_def) }
    3.77    ultimately show ?thesis by blast
    3.78  qed
    3.79  
    3.80 @@ -512,7 +511,7 @@
    3.81      have n0: "isnormNum 0\<^sub>N" by simp
    3.82      show ?thesis using nx ny 
    3.83        apply (simp only: isnormNum_unique[where ?'a = 'a, OF  Nmul_normN[OF nx ny] n0, symmetric] Nmul[where ?'a = 'a])
    3.84 -      by (simp add: INum_def split_def isnormNum_def fst_conv snd_conv split: split_if_asm)
    3.85 +      by (simp add: INum_def split_def isnormNum_def split: split_if_asm)
    3.86    }
    3.87  qed
    3.88  lemma Nneg_Nneg[simp]: "~\<^sub>N (~\<^sub>N c) = c"
    3.89 @@ -520,7 +519,7 @@
    3.90  
    3.91  lemma Nmul1[simp]: 
    3.92    "isnormNum c \<Longrightarrow> 1\<^sub>N *\<^sub>N c = c" 
    3.93 -  "isnormNum c \<Longrightarrow> c *\<^sub>N 1\<^sub>N  = c" 
    3.94 +  "isnormNum c \<Longrightarrow> c *\<^sub>N (1\<^sub>N) = c" 
    3.95    apply (simp_all add: Nmul_def Let_def split_def isnormNum_def)
    3.96    apply (cases "fst c = 0", simp_all, cases c, simp_all)+
    3.97    done
     4.1 --- a/src/HOL/Library/BigO.thy	Wed Jan 12 16:41:49 2011 +0100
     4.2 +++ b/src/HOL/Library/BigO.thy	Wed Jan 12 17:14:27 2011 +0100
     4.3 @@ -351,33 +351,30 @@
     4.4    apply (auto simp add: algebra_simps)
     4.5    done
     4.6  
     4.7 -lemma bigo_mult5: "ALL x. f x ~= 0 ==>
     4.8 -    O(f * g) <= (f::'a => ('b::linordered_field)) *o O(g)"
     4.9 -proof -
    4.10 -  assume "ALL x. f x ~= 0"
    4.11 -  show "O(f * g) <= f *o O(g)"
    4.12 -  proof
    4.13 -    fix h
    4.14 -    assume "h : O(f * g)"
    4.15 -    then have "(%x. 1 / (f x)) * h : (%x. 1 / f x) *o O(f * g)"
    4.16 -      by auto
    4.17 -    also have "... <= O((%x. 1 / f x) * (f * g))"
    4.18 -      by (rule bigo_mult2)
    4.19 -    also have "(%x. 1 / f x) * (f * g) = g"
    4.20 -      apply (simp add: func_times) 
    4.21 -      apply (rule ext)
    4.22 -      apply (simp add: prems nonzero_divide_eq_eq mult_ac)
    4.23 -      done
    4.24 -    finally have "(%x. (1::'b) / f x) * h : O(g)".
    4.25 -    then have "f * ((%x. (1::'b) / f x) * h) : f *o O(g)"
    4.26 -      by auto
    4.27 -    also have "f * ((%x. (1::'b) / f x) * h) = h"
    4.28 -      apply (simp add: func_times) 
    4.29 -      apply (rule ext)
    4.30 -      apply (simp add: prems nonzero_divide_eq_eq mult_ac)
    4.31 -      done
    4.32 -    finally show "h : f *o O(g)".
    4.33 -  qed
    4.34 +lemma bigo_mult5:
    4.35 +  assumes "ALL x. f x ~= 0"
    4.36 +  shows "O(f * g) <= (f::'a => ('b::linordered_field)) *o O(g)"
    4.37 +proof
    4.38 +  fix h
    4.39 +  assume "h : O(f * g)"
    4.40 +  then have "(%x. 1 / (f x)) * h : (%x. 1 / f x) *o O(f * g)"
    4.41 +    by auto
    4.42 +  also have "... <= O((%x. 1 / f x) * (f * g))"
    4.43 +    by (rule bigo_mult2)
    4.44 +  also have "(%x. 1 / f x) * (f * g) = g"
    4.45 +    apply (simp add: func_times) 
    4.46 +    apply (rule ext)
    4.47 +    apply (simp add: assms nonzero_divide_eq_eq mult_ac)
    4.48 +    done
    4.49 +  finally have "(%x. (1::'b) / f x) * h : O(g)" .
    4.50 +  then have "f * ((%x. (1::'b) / f x) * h) : f *o O(g)"
    4.51 +    by auto
    4.52 +  also have "f * ((%x. (1::'b) / f x) * h) = h"
    4.53 +    apply (simp add: func_times) 
    4.54 +    apply (rule ext)
    4.55 +    apply (simp add: assms nonzero_divide_eq_eq mult_ac)
    4.56 +    done
    4.57 +  finally show "h : f *o O(g)" .
    4.58  qed
    4.59  
    4.60  lemma bigo_mult6: "ALL x. f x ~= 0 ==>
    4.61 @@ -413,7 +410,7 @@
    4.62    done
    4.63  
    4.64  lemma bigo_minus3: "O(-f) = O(f)"
    4.65 -  by (auto simp add: bigo_def fun_Compl_def abs_minus_cancel)
    4.66 +  by (auto simp add: bigo_def fun_Compl_def)
    4.67  
    4.68  lemma bigo_plus_absorb_lemma1: "f : O(g) ==> f +o O(g) <= O(g)"
    4.69  proof -
    4.70 @@ -428,7 +425,7 @@
    4.71        from a have "O(f) <= O(g)" by (auto del: subsetI)
    4.72        thus ?thesis by (auto del: subsetI)
    4.73      qed
    4.74 -    also have "... <= O(g)" by (simp add: bigo_plus_idemp)
    4.75 +    also have "... <= O(g)" by simp
    4.76      finally show ?thesis .
    4.77    qed
    4.78  qed
    4.79 @@ -523,7 +520,7 @@
    4.80    apply (rule order_trans)
    4.81    apply (rule bigo_mult2)
    4.82    apply (simp add: func_times)
    4.83 -  apply (auto intro!: subsetI simp add: bigo_def elt_set_times_def func_times)
    4.84 +  apply (auto intro!: simp add: bigo_def elt_set_times_def func_times)
    4.85    apply (rule_tac x = "%y. inverse c * x y" in exI)
    4.86    apply (simp add: mult_assoc [symmetric] abs_mult)
    4.87    apply (rule_tac x = "abs (inverse c) * ca" in exI)
    4.88 @@ -535,8 +532,7 @@
    4.89    done
    4.90  
    4.91  lemma bigo_const_mult6 [intro]: "(%x. c) *o O(f) <= O(f)"
    4.92 -  apply (auto intro!: subsetI
    4.93 -    simp add: bigo_def elt_set_times_def func_times)
    4.94 +  apply (auto intro!: simp add: bigo_def elt_set_times_def func_times)
    4.95    apply (rule_tac x = "ca * (abs c)" in exI)
    4.96    apply (rule allI)
    4.97    apply (subgoal_tac "ca * abs(c) * abs(f x) = abs(c) * (ca * abs(f x))")
     5.1 --- a/src/HOL/Library/Float.thy	Wed Jan 12 16:41:49 2011 +0100
     5.2 +++ b/src/HOL/Library/Float.thy	Wed Jan 12 17:14:27 2011 +0100
     5.3 @@ -66,7 +66,7 @@
     5.4    by (simp only:number_of_float_def Float_num[unfolded number_of_is_id])
     5.5  
     5.6  lemma float_number_of_int[simp]: "real (Float n 0) = real n"
     5.7 -  by (simp add: Float_num[unfolded number_of_is_id] real_of_float_simp pow2_def)
     5.8 +  by simp
     5.9  
    5.10  lemma pow2_0[simp]: "pow2 0 = 1" by simp
    5.11  lemma pow2_1[simp]: "pow2 1 = 2" by simp
    5.12 @@ -107,7 +107,7 @@
    5.13      show ?case by simp
    5.14    next
    5.15      case (Suc m)
    5.16 -    show ?case by (auto simp add: algebra_simps pow2_add1 prems)
    5.17 +    then show ?case by (auto simp add: algebra_simps pow2_add1)
    5.18    qed
    5.19  next
    5.20    case (2 n)
    5.21 @@ -124,6 +124,7 @@
    5.22        apply (subst pow2_neg[of "-a"])
    5.23        apply (simp)
    5.24        done
    5.25 +  next
    5.26      case (Suc m)
    5.27      have a: "int m - (a + -2) =  1 + (int m - a + 1)" by arith
    5.28      have b: "int m - -2 = 1 + (int m + 1)" by arith
    5.29 @@ -138,15 +139,15 @@
    5.30        apply (subst pow2_neg[of "int m - a + 1"])
    5.31        apply (subst pow2_neg[of "int m + 1"])
    5.32        apply auto
    5.33 -      apply (insert prems)
    5.34 +      apply (insert Suc)
    5.35        apply (auto simp add: algebra_simps)
    5.36        done
    5.37    qed
    5.38  qed
    5.39  
    5.40 -lemma float_components[simp]: "Float (mantissa f) (scale f) = f" by (cases f, auto)
    5.41 +lemma float_components[simp]: "Float (mantissa f) (scale f) = f" by (cases f) auto
    5.42  
    5.43 -lemma float_split: "\<exists> a b. x = Float a b" by (cases x, auto)
    5.44 +lemma float_split: "\<exists> a b. x = Float a b" by (cases x) auto
    5.45  
    5.46  lemma float_split2: "(\<forall> a b. x \<noteq> Float a b) = False" by (auto simp add: float_split)
    5.47  
    5.48 @@ -156,7 +157,9 @@
    5.49  by arith
    5.50  
    5.51  function normfloat :: "float \<Rightarrow> float" where
    5.52 -"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)"
    5.53 +  "normfloat (Float a b) =
    5.54 +    (if a \<noteq> 0 \<and> even a then normfloat (Float (a div 2) (b+1))
    5.55 +     else if a=0 then Float 0 0 else Float a b)"
    5.56  by pat_completeness auto
    5.57  termination by (relation "measure (nat o abs o mantissa)") (auto intro: abs_div_2_less)
    5.58  declare normfloat.simps[simp del]
    5.59 @@ -168,7 +171,7 @@
    5.60      by auto
    5.61    show ?case
    5.62      apply (subst normfloat.simps)
    5.63 -    apply (auto simp add: float_zero)
    5.64 +    apply auto
    5.65      apply (subst 1[symmetric])
    5.66      apply (auto simp add: pow2_add even_def)
    5.67      done
    5.68 @@ -186,7 +189,10 @@
    5.69    {
    5.70      fix y
    5.71      have "0 <= y \<Longrightarrow> 0 < pow2 y"
    5.72 -      by (induct y, induct_tac n, simp_all add: pow2_add)
    5.73 +      apply (induct y)
    5.74 +      apply (induct_tac n)
    5.75 +      apply (simp_all add: pow2_add)
    5.76 +      done
    5.77    }
    5.78    note helper=this
    5.79    show ?thesis
    5.80 @@ -292,7 +298,7 @@
    5.81    from 
    5.82       float_eq_odd_helper[OF odd2 floateq] 
    5.83       float_eq_odd_helper[OF odd1 floateq[symmetric]]
    5.84 -  have beq: "b = b'"  by arith
    5.85 +  have beq: "b = b'" by arith
    5.86    with floateq show ?thesis by auto
    5.87  qed
    5.88  
    5.89 @@ -366,17 +372,17 @@
    5.90  end
    5.91  
    5.92  lemma real_of_float_add[simp]: "real (a + b) = real a + real (b :: float)"
    5.93 -  by (cases a, cases b, simp add: algebra_simps plus_float.simps, 
    5.94 +  by (cases a, cases b) (simp add: algebra_simps plus_float.simps, 
    5.95        auto simp add: pow2_int[symmetric] pow2_add[symmetric])
    5.96  
    5.97  lemma real_of_float_minus[simp]: "real (- a) = - real (a :: float)"
    5.98 -  by (cases a, simp add: uminus_float.simps)
    5.99 +  by (cases a) (simp add: uminus_float.simps)
   5.100  
   5.101  lemma real_of_float_sub[simp]: "real (a - b) = real a - real (b :: float)"
   5.102 -  by (cases a, cases b, simp add: minus_float_def)
   5.103 +  by (cases a, cases b) (simp add: minus_float_def)
   5.104  
   5.105  lemma real_of_float_mult[simp]: "real (a*b) = real a * real (b :: float)"
   5.106 -  by (cases a, cases b, simp add: times_float.simps pow2_add)
   5.107 +  by (cases a, cases b) (simp add: times_float.simps pow2_add)
   5.108  
   5.109  lemma real_of_float_0[simp]: "real (0 :: float) = 0"
   5.110    by (auto simp add: zero_float_def float_zero)
   5.111 @@ -419,35 +425,36 @@
   5.112  declare real_of_float_simp[simp del]
   5.113  
   5.114  lemma real_of_float_pprt[simp]: "real (float_pprt a) = pprt (real a)"
   5.115 -  by (cases a, auto simp add: float_pprt.simps zero_le_float float_le_zero float_zero)
   5.116 +  by (cases a) (auto simp add: zero_le_float float_le_zero)
   5.117  
   5.118  lemma real_of_float_nprt[simp]: "real (float_nprt a) = nprt (real a)"
   5.119 -  by (cases a,  auto simp add: float_nprt.simps zero_le_float float_le_zero float_zero)
   5.120 +  by (cases a) (auto simp add: zero_le_float float_le_zero)
   5.121  
   5.122  instance float :: ab_semigroup_add
   5.123  proof (intro_classes)
   5.124    fix a b c :: float
   5.125    show "a + b + c = a + (b + c)"
   5.126 -    by (cases a, cases b, cases c, auto simp add: algebra_simps power_add[symmetric] plus_float.simps)
   5.127 +    by (cases a, cases b, cases c)
   5.128 +      (auto simp add: algebra_simps power_add[symmetric] plus_float.simps)
   5.129  next
   5.130    fix a b :: float
   5.131    show "a + b = b + a"
   5.132 -    by (cases a, cases b, simp add: plus_float.simps)
   5.133 +    by (cases a, cases b) (simp add: plus_float.simps)
   5.134  qed
   5.135  
   5.136  instance float :: comm_monoid_mult
   5.137  proof (intro_classes)
   5.138    fix a b c :: float
   5.139    show "a * b * c = a * (b * c)"
   5.140 -    by (cases a, cases b, cases c, simp add: times_float.simps)
   5.141 +    by (cases a, cases b, cases c) (simp add: times_float.simps)
   5.142  next
   5.143    fix a b :: float
   5.144    show "a * b = b * a"
   5.145 -    by (cases a, cases b, simp add: times_float.simps)
   5.146 +    by (cases a, cases b) (simp add: times_float.simps)
   5.147  next
   5.148    fix a :: float
   5.149    show "1 * a = a"
   5.150 -    by (cases a, simp add: times_float.simps one_float_def)
   5.151 +    by (cases a) (simp add: times_float.simps one_float_def)
   5.152  qed
   5.153  
   5.154  (* Floats do NOT form a cancel_semigroup_add: *)
   5.155 @@ -458,7 +465,7 @@
   5.156  proof (intro_classes)
   5.157    fix a b c :: float
   5.158    show "(a + b) * c = a * c + b * c"
   5.159 -    by (cases a, cases b, cases c, simp, simp add: plus_float.simps times_float.simps algebra_simps)
   5.160 +    by (cases a, cases b, cases c) (simp add: plus_float.simps times_float.simps algebra_simps)
   5.161  qed
   5.162  
   5.163  (* Floats do NOT form an order, because "(x < y) = (x <= y & x <> y)" does NOT hold *)
   5.164 @@ -903,11 +910,31 @@
   5.165    and D: "\<And>x y prec. \<lbrakk>0 \<le> x; y < 0; ps = (prec, x, y)\<rbrakk> \<Longrightarrow> P"
   5.166    shows P
   5.167  proof -
   5.168 -  obtain prec x y where [simp]: "ps = (prec, x, y)" by (cases ps, auto)
   5.169 +  obtain prec x y where [simp]: "ps = (prec, x, y)" by (cases ps) auto
   5.170    from Y have "y = 0 \<Longrightarrow> P" by auto
   5.171 -  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 } 
   5.172 -  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 }
   5.173 -  ultimately show P by (cases "y = 0 \<or> 0 < y \<or> y < 0", auto)
   5.174 +  moreover {
   5.175 +    assume "0 < y"
   5.176 +    have P
   5.177 +    proof (cases "0 \<le> x")
   5.178 +      case True
   5.179 +      with A and `0 < y` show P by auto
   5.180 +    next
   5.181 +      case False
   5.182 +      with B and `0 < y` show P by auto
   5.183 +    qed
   5.184 +  } 
   5.185 +  moreover {
   5.186 +    assume "y < 0"
   5.187 +    have P
   5.188 +    proof (cases "0 \<le> x")
   5.189 +      case True
   5.190 +      with D and `y < 0` show P by auto
   5.191 +    next
   5.192 +      case False
   5.193 +      with C and `y < 0` show P by auto
   5.194 +    qed
   5.195 +  }
   5.196 +  ultimately show P by (cases "y = 0 \<or> 0 < y \<or> y < 0") auto
   5.197  qed
   5.198  
   5.199  function lapprox_rat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float"
   5.200 @@ -1011,10 +1038,14 @@
   5.201  lemma rapprox_rat_nonpos_pos: assumes "x \<le> 0" and "0 < y"
   5.202    shows "real (rapprox_rat n x y) \<le> 0"
   5.203  proof (cases "x = 0") 
   5.204 -  case True hence "0 \<le> x" by auto show ?thesis unfolding rapprox_rat.simps(2)[OF `0 \<le> x` `0 < y`]
   5.205 -    unfolding True rapprox_posrat_def Let_def by auto
   5.206 +  case True
   5.207 +  hence "0 \<le> x" by auto show ?thesis
   5.208 +    unfolding rapprox_rat.simps(2)[OF `0 \<le> x` `0 < y`]
   5.209 +    unfolding True rapprox_posrat_def Let_def
   5.210 +    by auto
   5.211  next
   5.212 -  case False hence "x < 0" using assms by auto
   5.213 +  case False
   5.214 +  hence "x < 0" using assms by auto
   5.215    show ?thesis using rapprox_rat_neg[OF `x < 0` `0 < y`] .
   5.216  qed
   5.217  
   5.218 @@ -1064,19 +1095,31 @@
   5.219  proof (cases x, cases y)
   5.220    fix xm xe ym ye :: int
   5.221    assume x_eq: "x = Float xm xe" and y_eq: "y = Float ym ye"
   5.222 -  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
   5.223 -  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
   5.224 +  have "0 \<le> xm"
   5.225 +    using `0 \<le> x`[unfolded x_eq le_float_def real_of_float_simp real_of_float_0 zero_le_mult_iff]
   5.226 +    by auto
   5.227 +  have "0 < ym"
   5.228 +    using `0 < y`[unfolded y_eq less_float_def real_of_float_simp real_of_float_0 zero_less_mult_iff]
   5.229 +    by auto
   5.230  
   5.231 -  have "\<And>n. 0 \<le> real (Float 1 n)" unfolding real_of_float_simp using zero_le_pow2 by auto
   5.232 -  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`])
   5.233 +  have "\<And>n. 0 \<le> real (Float 1 n)"
   5.234 +    unfolding real_of_float_simp using zero_le_pow2 by auto
   5.235 +  moreover have "0 \<le> real (lapprox_rat prec xm ym)"
   5.236 +    apply (rule order_trans[OF _ lapprox_rat_bottom[OF `0 \<le> xm` `0 < ym`]])
   5.237 +    apply (auto simp add: `0 \<le> xm` pos_imp_zdiv_nonneg_iff[OF `0 < ym`])
   5.238 +    done
   5.239    ultimately show "0 \<le> float_divl prec x y"
   5.240 -    unfolding x_eq y_eq float_divl.simps Let_def le_float_def real_of_float_0 by (auto intro!: mult_nonneg_nonneg)
   5.241 +    unfolding x_eq y_eq float_divl.simps Let_def le_float_def real_of_float_0
   5.242 +    by (auto intro!: mult_nonneg_nonneg)
   5.243  qed
   5.244  
   5.245 -lemma float_divl_pos_less1_bound: assumes "0 < x" and "x < 1" and "0 < prec" shows "1 \<le> float_divl prec 1 x"
   5.246 +lemma float_divl_pos_less1_bound:
   5.247 +  assumes "0 < x" and "x < 1" and "0 < prec"
   5.248 +  shows "1 \<le> float_divl prec 1 x"
   5.249  proof (cases x)
   5.250    case (Float m e)
   5.251 -  from `0 < x` `x < 1` have "0 < m" "e < 0" using float_pos_m_pos float_pos_less1_e_neg unfolding Float by auto
   5.252 +  from `0 < x` `x < 1` have "0 < m" "e < 0"
   5.253 +    using float_pos_m_pos float_pos_less1_e_neg unfolding Float by auto
   5.254    let ?b = "nat (bitlen m)" and ?e = "nat (-e)"
   5.255    have "1 \<le> m" and "m \<noteq> 0" using `0 < m` by auto
   5.256    with bitlen_bounds[OF `0 < m`] have "m < 2^?b" and "(2::int) \<le> 2^?b" by auto
   5.257 @@ -1087,22 +1130,29 @@
   5.258  
   5.259    from float_less1_mantissa_bound `0 < x` `x < 1` Float 
   5.260    have "m < 2^?e" by auto
   5.261 -  with bitlen_bounds[OF `0 < m`, THEN conjunct1]
   5.262 -  have "(2::int)^nat (bitlen m - 1) < 2^?e" by (rule order_le_less_trans)
   5.263 +  with bitlen_bounds[OF `0 < m`, THEN conjunct1] have "(2::int)^nat (bitlen m - 1) < 2^?e"
   5.264 +    by (rule order_le_less_trans)
   5.265    from power_less_imp_less_exp[OF _ this]
   5.266    have "bitlen m \<le> - e" by auto
   5.267    hence "(2::real)^?b \<le> 2^?e" by auto
   5.268 -  hence "(2::real)^?b * inverse (2^?b) \<le> 2^?e * inverse (2^?b)" by (rule mult_right_mono, auto)
   5.269 +  hence "(2::real)^?b * inverse (2^?b) \<le> 2^?e * inverse (2^?b)"
   5.270 +    by (rule mult_right_mono) auto
   5.271    hence "(1::real) \<le> 2^?e * inverse (2^?b)" by auto
   5.272    also
   5.273    let ?d = "real (2 ^ nat (int prec + bitlen m - 1) div m) * inverse (2 ^ nat (int prec + bitlen m - 1))"
   5.274 -  { 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)
   5.275 -    also have "\<dots> = 2 ^ nat (int prec + bitlen m - 1)" unfolding pow_split zpower_zadd_distrib by auto
   5.276 -    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)
   5.277 -    hence "2^(prec - 1) \<le> 2 ^ nat (int prec + bitlen m - 1) div m" unfolding div_mult_self2_is_id[OF `m \<noteq> 0`] .
   5.278 +  {
   5.279 +    have "2^(prec - 1) * m \<le> 2^(prec - 1) * 2^?b"
   5.280 +      using `m < 2^?b`[THEN less_imp_le] by (rule mult_left_mono) auto
   5.281 +    also have "\<dots> = 2 ^ nat (int prec + bitlen m - 1)"
   5.282 +      unfolding pow_split zpower_zadd_distrib by auto
   5.283 +    finally have "2^(prec - 1) * m div m \<le> 2 ^ nat (int prec + bitlen m - 1) div m"
   5.284 +      using `0 < m` by (rule zdiv_mono1)
   5.285 +    hence "2^(prec - 1) \<le> 2 ^ nat (int prec + bitlen m - 1) div m"
   5.286 +      unfolding div_mult_self2_is_id[OF `m \<noteq> 0`] .
   5.287      hence "2^(prec - 1) * inverse (2 ^ nat (int prec + bitlen m - 1)) \<le> ?d"
   5.288 -      unfolding real_of_int_le_iff[of "2^(prec - 1)", symmetric] by auto }
   5.289 -  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"]
   5.290 +      unfolding real_of_int_le_iff[of "2^(prec - 1)", symmetric] by auto
   5.291 +  }
   5.292 +  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"]
   5.293    have "2^?e * inverse (2^?b) \<le> 2^?e * ?d" unfolding pow_split power_add by auto
   5.294    finally have "1 \<le> 2^?e * ?d" .
   5.295    
   5.296 @@ -1110,8 +1160,11 @@
   5.297    have "bitlen 1 = 1" using bitlen.simps by auto
   5.298    
   5.299    show ?thesis 
   5.300 -    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`
   5.301 -    unfolding le_float_def real_of_float_mult normfloat real_of_float_simp pow2_minus pow2_int e_nat
   5.302 +    unfolding one_float_def Float float_divl.simps Let_def
   5.303 +      lapprox_rat.simps(2)[OF zero_le_one `0 < m`]
   5.304 +      lapprox_posrat_def `bitlen 1 = 1`
   5.305 +    unfolding le_float_def real_of_float_mult normfloat real_of_float_simp
   5.306 +      pow2_minus pow2_int e_nat
   5.307      using `1 \<le> 2^?e * ?d` by (auto simp add: pow2_def)
   5.308  qed
   5.309  
     6.1 --- a/src/HOL/Library/Lattice_Algebras.thy	Wed Jan 12 16:41:49 2011 +0100
     6.2 +++ b/src/HOL/Library/Lattice_Algebras.thy	Wed Jan 12 17:14:27 2011 +0100
     6.3 @@ -253,7 +253,7 @@
     6.4    "a + a \<le> 0 \<longleftrightarrow> a \<le> 0" 
     6.5  proof -
     6.6    have "a + a \<le> 0 \<longleftrightarrow> 0 \<le> - (a + a)" by (subst le_minus_iff, simp)
     6.7 -  moreover have "\<dots> \<longleftrightarrow> a \<le> 0" by (simp add: zero_le_double_add_iff_zero_le_single_add)
     6.8 +  moreover have "\<dots> \<longleftrightarrow> a \<le> 0" by simp
     6.9    ultimately show ?thesis by blast
    6.10  qed
    6.11  
    6.12 @@ -261,7 +261,7 @@
    6.13    "a + a < 0 \<longleftrightarrow> a < 0"
    6.14  proof -
    6.15    have "a + a < 0 \<longleftrightarrow> 0 < - (a + a)" by (subst less_minus_iff, simp)
    6.16 -  moreover have "\<dots> \<longleftrightarrow> a < 0" by (simp add: zero_less_double_add_iff_zero_less_single_add)
    6.17 +  moreover have "\<dots> \<longleftrightarrow> a < 0" by simp
    6.18    ultimately show ?thesis by blast
    6.19  qed
    6.20  
    6.21 @@ -428,7 +428,7 @@
    6.22  instance lattice_ring \<subseteq> ordered_ring_abs
    6.23  proof
    6.24    fix a b :: "'a\<Colon> lattice_ring"
    6.25 -  assume "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0)"
    6.26 +  assume a: "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0)"
    6.27    show "abs (a*b) = abs a * abs b"
    6.28    proof -
    6.29      have s: "(0 <= a*b) | (a*b <= 0)"
    6.30 @@ -437,7 +437,7 @@
    6.31        apply (rule_tac contrapos_np[of "a*b <= 0"])
    6.32        apply (simp)
    6.33        apply (rule_tac split_mult_neg_le)
    6.34 -      apply (insert prems)
    6.35 +      apply (insert a)
    6.36        apply (blast)
    6.37        done
    6.38      have mulprts: "a * b = (pprt a + nprt a) * (pprt b + nprt b)"
    6.39 @@ -447,7 +447,7 @@
    6.40        assume "0 <= a * b"
    6.41        then show ?thesis
    6.42          apply (simp_all add: mulprts abs_prts)
    6.43 -        apply (insert prems)
    6.44 +        apply (insert a)
    6.45          apply (auto simp add: 
    6.46            algebra_simps 
    6.47            iffD1[OF zero_le_iff_zero_nprt] iffD1[OF le_zero_iff_zero_pprt]
    6.48 @@ -460,7 +460,7 @@
    6.49        with s have "a*b <= 0" by simp
    6.50        then show ?thesis
    6.51          apply (simp_all add: mulprts abs_prts)
    6.52 -        apply (insert prems)
    6.53 +        apply (insert a)
    6.54          apply (auto simp add: algebra_simps)
    6.55          apply(drule (1) mult_nonneg_nonneg[of a b],simp)
    6.56          apply(drule (1) mult_nonpos_nonpos[of a b],simp)
    6.57 @@ -485,31 +485,31 @@
    6.58    then have "a * b = pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
    6.59      by (simp add: algebra_simps)
    6.60    moreover have "pprt a * pprt b <= pprt a2 * pprt b2"
    6.61 -    by (simp_all add: prems mult_mono)
    6.62 +    by (simp_all add: assms mult_mono)
    6.63    moreover have "pprt a * nprt b <= pprt a1 * nprt b2"
    6.64    proof -
    6.65      have "pprt a * nprt b <= pprt a * nprt b2"
    6.66 -      by (simp add: mult_left_mono prems)
    6.67 +      by (simp add: mult_left_mono assms)
    6.68      moreover have "pprt a * nprt b2 <= pprt a1 * nprt b2"
    6.69 -      by (simp add: mult_right_mono_neg prems)
    6.70 +      by (simp add: mult_right_mono_neg assms)
    6.71      ultimately show ?thesis
    6.72        by simp
    6.73    qed
    6.74    moreover have "nprt a * pprt b <= nprt a2 * pprt b1"
    6.75    proof - 
    6.76      have "nprt a * pprt b <= nprt a2 * pprt b"
    6.77 -      by (simp add: mult_right_mono prems)
    6.78 +      by (simp add: mult_right_mono assms)
    6.79      moreover have "nprt a2 * pprt b <= nprt a2 * pprt b1"
    6.80 -      by (simp add: mult_left_mono_neg prems)
    6.81 +      by (simp add: mult_left_mono_neg assms)
    6.82      ultimately show ?thesis
    6.83        by simp
    6.84    qed
    6.85    moreover have "nprt a * nprt b <= nprt a1 * nprt b1"
    6.86    proof -
    6.87      have "nprt a * nprt b <= nprt a * nprt b1"
    6.88 -      by (simp add: mult_left_mono_neg prems)
    6.89 +      by (simp add: mult_left_mono_neg assms)
    6.90      moreover have "nprt a * nprt b1 <= nprt a1 * nprt b1"
    6.91 -      by (simp add: mult_right_mono_neg prems)
    6.92 +      by (simp add: mult_right_mono_neg assms)
    6.93      ultimately show ?thesis
    6.94        by simp
    6.95    qed
    6.96 @@ -526,9 +526,9 @@
    6.97    shows
    6.98    "a * b >= nprt a1 * pprt b2 + nprt a2 * nprt b2 + pprt a1 * pprt b1 + pprt a2 * nprt b1"
    6.99  proof - 
   6.100 -  from prems have a1:"- a2 <= -a" by auto
   6.101 -  from prems have a2: "-a <= -a1" by auto
   6.102 -  from mult_le_prts[of "-a2" "-a" "-a1" "b1" b "b2", OF a1 a2 prems(3) prems(4), simplified nprt_neg pprt_neg] 
   6.103 +  from assms have a1:"- a2 <= -a" by auto
   6.104 +  from assms have a2: "-a <= -a1" by auto
   6.105 +  from mult_le_prts[of "-a2" "-a" "-a1" "b1" b "b2", OF a1 a2 assms(3) assms(4), simplified nprt_neg pprt_neg] 
   6.106    have le: "- (a * b) <= - nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1" by simp  
   6.107    then have "-(- nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1) <= a * b"
   6.108      by (simp only: minus_le_iff)
     7.1 --- a/src/HOL/ZF/Games.thy	Wed Jan 12 16:41:49 2011 +0100
     7.2 +++ b/src/HOL/ZF/Games.thy	Wed Jan 12 17:14:27 2011 +0100
     7.3 @@ -165,7 +165,7 @@
     7.4    shows "opt \<in> games_lfp"
     7.5    apply (rule games_option_stable[where g=g])
     7.6    apply (simp add: games_lfp_unfold[symmetric])
     7.7 -  apply (simp_all add: prems)
     7.8 +  apply (simp_all add: assms)
     7.9    done
    7.10  
    7.11  lemma is_option_of_imp_games:
    7.12 @@ -466,10 +466,10 @@
    7.13          proof -
    7.14            { fix xr
    7.15              assume xr:"zin xr (right_options x)"
    7.16 -            assume "ge_game (z, xr)"
    7.17 +            assume a: "ge_game (z, xr)"
    7.18              have "ge_game (y, xr)"
    7.19                apply (rule 1[rule_format, where y="[y,z,xr]"])
    7.20 -              apply (auto intro: xr lprod_3_1 simp add: prems)
    7.21 +              apply (auto intro: xr lprod_3_1 simp add: goal1 a)
    7.22                done
    7.23              moreover from xr have "\<not> ge_game (y, xr)"
    7.24                by (simp add: goal1(2)[simplified ge_game_eq[of x y], rule_format, of xr, simplified xr])
    7.25 @@ -478,10 +478,10 @@
    7.26            note xr = this
    7.27            { fix zl
    7.28              assume zl:"zin zl (left_options z)"
    7.29 -            assume "ge_game (zl, x)"
    7.30 +            assume a: "ge_game (zl, x)"
    7.31              have "ge_game (zl, y)"
    7.32                apply (rule 1[rule_format, where y="[zl,x,y]"])
    7.33 -              apply (auto intro: zl lprod_3_2 simp add: prems)
    7.34 +              apply (auto intro: zl lprod_3_2 simp add: goal1 a)
    7.35                done
    7.36              moreover from zl have "\<not> ge_game (zl, y)"
    7.37                by (simp add: goal1(3)[simplified ge_game_eq[of y z], rule_format, of zl, simplified zl])
    7.38 @@ -495,7 +495,7 @@
    7.39      qed
    7.40    } 
    7.41    note trans = this[of "[x, y, z]", simplified, rule_format]    
    7.42 -  with prems show ?thesis by blast
    7.43 +  with assms show ?thesis by blast
    7.44  qed
    7.45  
    7.46  lemma eq_game_trans: "eq_game a b \<Longrightarrow> eq_game b c \<Longrightarrow> eq_game a c"
    7.47 @@ -522,7 +522,7 @@
    7.48      by (auto simp add: 
    7.49        plus_game.simps[where G=G and H=H] 
    7.50        plus_game.simps[where G=H and H=G]
    7.51 -      Game_ext zet_ext_eq zunion zimage_iff prems)
    7.52 +      Game_ext zet_ext_eq zunion zimage_iff 1)
    7.53  qed
    7.54  
    7.55  lemma game_ext_eq: "(G = H) = (left_options G = left_options H \<and> right_options G = right_options H)"
    7.56 @@ -545,10 +545,10 @@
    7.57      have "H = zero_game \<longrightarrow> plus_game G H = G "
    7.58      proof (induct G H rule: plus_game.induct, rule impI)
    7.59        case (goal1 G H)
    7.60 -      note induct_hyp = prems[simplified goal1, simplified] and prems
    7.61 +      note induct_hyp = this[simplified goal1, simplified] and this
    7.62        show ?case
    7.63          apply (simp only: plus_game.simps[where G=G and H=H])
    7.64 -        apply (simp add: game_ext_eq prems)
    7.65 +        apply (simp add: game_ext_eq goal1)
    7.66          apply (auto simp add: 
    7.67            zimage_cong[where f = "\<lambda> g. plus_game g zero_game" and g = "id"] 
    7.68            induct_hyp)
    7.69 @@ -626,7 +626,7 @@
    7.70      by (auto simp add: opt_ops
    7.71        neg_game.simps[of "plus_game G H"]
    7.72        plus_game.simps[of "neg_game G" "neg_game H"]
    7.73 -      Game_ext zet_ext_eq zunion zimage_iff prems)
    7.74 +      Game_ext zet_ext_eq zunion zimage_iff 1)
    7.75  qed
    7.76  
    7.77  lemma eq_game_plus_inverse: "eq_game (plus_game x (neg_game x)) zero_game"
    7.78 @@ -635,7 +635,7 @@
    7.79    { fix y
    7.80      assume "zin y (options x)"
    7.81      then have "eq_game (plus_game y (neg_game y)) zero_game"
    7.82 -      by (auto simp add: prems)
    7.83 +      by (auto simp add: goal1)
    7.84    }
    7.85    note ihyp = this
    7.86    {
    7.87 @@ -645,7 +645,7 @@
    7.88        apply (subst ge_game.simps, simp)
    7.89        apply (rule exI[where x="plus_game y (neg_game y)"])
    7.90        apply (auto simp add: ihyp[of y, simplified y right_imp_options eq_game_def])
    7.91 -      apply (auto simp add: left_options_plus left_options_neg zunion zimage_iff intro: prems)
    7.92 +      apply (auto simp add: left_options_plus left_options_neg zunion zimage_iff intro: y)
    7.93        done
    7.94    }
    7.95    note case1 = this
    7.96 @@ -656,7 +656,7 @@
    7.97        apply (subst ge_game.simps, simp)
    7.98        apply (rule exI[where x="plus_game y (neg_game y)"])
    7.99        apply (auto simp add: ihyp[of y, simplified y left_imp_options eq_game_def])
   7.100 -      apply (auto simp add: left_options_plus zunion zimage_iff intro: prems)
   7.101 +      apply (auto simp add: left_options_plus zunion zimage_iff intro: y)
   7.102        done
   7.103    }
   7.104    note case2 = this
   7.105 @@ -667,7 +667,7 @@
   7.106        apply (subst ge_game.simps, simp)
   7.107        apply (rule exI[where x="plus_game y (neg_game y)"])
   7.108        apply (auto simp add: ihyp[of y, simplified y left_imp_options eq_game_def])
   7.109 -      apply (auto simp add: right_options_plus right_options_neg zunion zimage_iff intro: prems)
   7.110 +      apply (auto simp add: right_options_plus right_options_neg zunion zimage_iff intro: y)
   7.111        done
   7.112    }
   7.113    note case3 = this
   7.114 @@ -678,7 +678,7 @@
   7.115        apply (subst ge_game.simps, simp)
   7.116        apply (rule exI[where x="plus_game y (neg_game y)"])
   7.117        apply (auto simp add: ihyp[of y, simplified y right_imp_options eq_game_def])
   7.118 -      apply (auto simp add: right_options_plus zunion zimage_iff intro: prems)
   7.119 +      apply (auto simp add: right_options_plus zunion zimage_iff intro: y)
   7.120        done
   7.121    }
   7.122    note case4 = this
     8.1 --- a/src/HOL/ZF/LProd.thy	Wed Jan 12 16:41:49 2011 +0100
     8.2 +++ b/src/HOL/ZF/LProd.thy	Wed Jan 12 17:14:27 2011 +0100
     8.3 @@ -42,12 +42,12 @@
     8.4    show ?case by (auto intro: lprod_single step)
     8.5  next
     8.6    case (lprod_list ah at bh bt a b)
     8.7 -  from prems have transR: "trans R" by auto
     8.8 +  then have transR: "trans R" by auto
     8.9    have as: "multiset_of (ah @ a # at) = multiset_of (ah @ at) + {#a#}" (is "_ = ?ma + _")
    8.10      by (simp add: algebra_simps)
    8.11    have bs: "multiset_of (bh @ b # bt) = multiset_of (bh @ bt) + {#b#}" (is "_ = ?mb + _")
    8.12      by (simp add: algebra_simps)
    8.13 -  from prems have "(?ma, ?mb) \<in> mult R"
    8.14 +  from lprod_list have "(?ma, ?mb) \<in> mult R"
    8.15      by auto
    8.16    with mult_implies_one_step[OF transR] have 
    8.17      "\<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)"
    8.18 @@ -136,12 +136,12 @@
    8.19  
    8.20  lemma lprod_3_1: assumes "(x', x) \<in> R" shows "([y, z, x'], [x, y, z]) \<in> lprod R"
    8.21    apply (rule lprod_list[where a="y" and b="y" and ah="[]" and at="[z,x']" and bh="[x]" and bt="[z]", simplified])
    8.22 -  apply (auto simp add: lprod_2_1 prems)
    8.23 +  apply (auto simp add: lprod_2_1 assms)
    8.24    done
    8.25  
    8.26  lemma lprod_3_2: assumes "(z',z) \<in> R" shows "([z', x, y], [x,y,z]) \<in> lprod R"
    8.27    apply (rule lprod_list[where a="y" and b="y" and ah="[z',x]" and at="[]" and bh="[x]" and bt="[z]", simplified])
    8.28 -  apply (auto simp add: lprod_2_2 prems)
    8.29 +  apply (auto simp add: lprod_2_2 assms)
    8.30    done
    8.31  
    8.32  lemma lprod_3_3: assumes xr: "(xr, x) \<in> R" shows "([xr, y, z], [x, y, z]) \<in> lprod R"