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