--- 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*}
--- 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
--- 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
--- 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))")
--- 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
--- 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)
--- 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
--- 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"