--- a/src/HOL/Algebra/UnivPoly.thy Fri Aug 28 18:11:42 2009 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy Fri Aug 28 18:52:41 2009 +0200
@@ -817,15 +817,9 @@
text {* Degree and polynomial operations *}
lemma deg_add [simp]:
- assumes R: "p \<in> carrier P" "q \<in> carrier P"
- shows "deg R (p \<oplus>\<^bsub>P\<^esub> q) <= max (deg R p) (deg R q)"
-proof (cases "deg R p <= deg R q")
- case True show ?thesis
- by (rule deg_aboveI) (simp_all add: True R deg_aboveD)
-next
- case False show ?thesis
- by (rule deg_aboveI) (simp_all add: False R deg_aboveD)
-qed
+ "p \<in> carrier P \<Longrightarrow> q \<in> carrier P \<Longrightarrow>
+ deg R (p \<oplus>\<^bsub>P\<^esub> q) <= max (deg R p) (deg R q)"
+by(rule deg_aboveI)(simp_all add: deg_aboveD)
lemma deg_monom_le:
"a \<in> carrier R ==> deg R (monom P a n) <= n"
--- a/src/HOL/Algebra/poly/UnivPoly2.thy Fri Aug 28 18:11:42 2009 +0200
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy Fri Aug 28 18:52:41 2009 +0200
@@ -563,11 +563,7 @@
lemma deg_add [simp]:
"deg ((p::'a::ring up) + q) <= max (deg p) (deg q)"
-proof (cases "deg p <= deg q")
- case True show ?thesis by (rule deg_aboveI) (simp add: True deg_aboveD)
-next
- case False show ?thesis by (rule deg_aboveI) (simp add: False deg_aboveD)
-qed
+by (rule deg_aboveI) (simp add: deg_aboveD)
lemma deg_monom_ring:
"deg (monom a n::'a::ring up) <= n"
--- a/src/HOL/Complete_Lattice.thy Fri Aug 28 18:11:42 2009 +0200
+++ b/src/HOL/Complete_Lattice.thy Fri Aug 28 18:52:41 2009 +0200
@@ -76,11 +76,11 @@
lemma sup_bot [simp]:
"x \<squnion> bot = x"
- using bot_least [of x] by (simp add: le_iff_sup sup_commute)
+ using bot_least [of x] by (simp add: sup_commute)
lemma inf_top [simp]:
"x \<sqinter> top = x"
- using top_greatest [of x] by (simp add: le_iff_inf inf_commute)
+ using top_greatest [of x] by (simp add: inf_commute)
definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
"SUPR A f = \<Squnion> (f ` A)"
--- a/src/HOL/Lattices.thy Fri Aug 28 18:11:42 2009 +0200
+++ b/src/HOL/Lattices.thy Fri Aug 28 18:52:41 2009 +0200
@@ -125,10 +125,10 @@
lemma inf_left_idem[simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
by (rule antisym) (auto intro: le_infI2)
-lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
+lemma inf_absorb1[simp]: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
by (rule antisym) auto
-lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
+lemma inf_absorb2[simp]: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
by (rule antisym) auto
lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
@@ -153,10 +153,10 @@
lemma sup_left_idem[simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
by (rule antisym) (auto intro: le_supI2)
-lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
+lemma sup_absorb1[simp]: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
by (rule antisym) auto
-lemma sup_absorb2: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
+lemma sup_absorb2[simp]: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
by (rule antisym) auto
lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
@@ -199,7 +199,7 @@
shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
proof-
have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by(simp add:sup_inf_absorb)
- also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))" by(simp add:D inf_commute sup_assoc)
+ also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))" by(simp add:D inf_commute sup_assoc del:sup_absorb1)
also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)"
by(simp add:inf_sup_absorb inf_commute)
also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:D)
@@ -211,7 +211,7 @@
shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
proof-
have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)" by(simp add:inf_sup_absorb)
- also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))" by(simp add:D sup_commute inf_assoc)
+ also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))" by(simp add:D sup_commute inf_assoc del:inf_absorb1)
also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)"
by(simp add:sup_inf_absorb sup_commute)
also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by(simp add:D)
--- a/src/HOL/Lim.thy Fri Aug 28 18:11:42 2009 +0200
+++ b/src/HOL/Lim.thy Fri Aug 28 18:52:41 2009 +0200
@@ -544,8 +544,7 @@
case True thus ?thesis using `0 < s` by auto
next
case False hence "s / 2 \<ge> (x - b) / 2" by auto
- from inf_absorb2[OF this, unfolded inf_real_def]
- have "?x = (x + b) / 2" by auto
+ hence "?x = (x + b) / 2" by(simp add:field_simps)
thus ?thesis using `b < x` by auto
qed
hence "0 \<le> f ?x" using all_le `?x < x` by auto
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Fri Aug 28 18:11:42 2009 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Fri Aug 28 18:52:41 2009 +0200
@@ -1070,7 +1070,6 @@
bc_mt_corresp [Pop] (popST (Suc 0)) (T # ST, LT) cG rT mxr (Suc 0)"
apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def)
apply (simp add: max_ssize_def ssize_sto_def max_of_list_def)
- apply (simp add: max_def)
apply (simp add: check_type_simps)
apply clarify
apply (rule_tac x="(length ST)" in exI)
@@ -1154,7 +1153,7 @@
\<Longrightarrow> bc_mt_corresp [Store i] (storeST i T) (T # ST, LT) cG rT mxr (Suc 0)"
apply (simp add: bc_mt_corresp_def storeST_def wt_instr_altern_def eff_def norm_eff_def)
apply (simp add: max_ssize_def max_of_list_def )
- apply (simp add: ssize_sto_def) apply (simp add: max_def)
+ apply (simp add: ssize_sto_def)
apply (intro strip)
apply (simp add: check_type_simps)
apply clarify
@@ -1170,7 +1169,6 @@
apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def)
apply (simp add: sup_state_conv)
apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
- apply (simp add: max_def)
apply (intro strip)
apply (simp add: check_type_simps)
apply clarify
--- a/src/HOL/OrderedGroup.thy Fri Aug 28 18:11:42 2009 +0200
+++ b/src/HOL/OrderedGroup.thy Fri Aug 28 18:52:41 2009 +0200
@@ -1075,16 +1075,17 @@
lemma nprt_0[simp]: "nprt 0 = 0" by (simp add: nprt_def)
lemma pprt_eq_id [simp, noatp]: "0 \<le> x \<Longrightarrow> pprt x = x"
-by (simp add: pprt_def le_iff_sup sup_aci)
+by (simp add: pprt_def sup_aci)
+
lemma nprt_eq_id [simp, noatp]: "x \<le> 0 \<Longrightarrow> nprt x = x"
-by (simp add: nprt_def le_iff_inf inf_aci)
+by (simp add: nprt_def inf_aci)
lemma pprt_eq_0 [simp, noatp]: "x \<le> 0 \<Longrightarrow> pprt x = 0"
-by (simp add: pprt_def le_iff_sup sup_aci)
+by (simp add: pprt_def sup_aci)
lemma nprt_eq_0 [simp, noatp]: "0 \<le> x \<Longrightarrow> nprt x = 0"
-by (simp add: nprt_def le_iff_inf inf_aci)
+by (simp add: nprt_def inf_aci)
lemma sup_0_imp_0: "sup a (- a) = 0 \<Longrightarrow> a = 0"
proof -
@@ -1118,13 +1119,13 @@
"0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
proof
assume "0 <= a + a"
- hence a:"inf (a+a) 0 = 0" by (simp add: le_iff_inf inf_commute)
+ hence a:"inf (a+a) 0 = 0" by (simp add: inf_commute)
have "(inf a 0)+(inf a 0) = inf (inf (a+a) 0) a" (is "?l=_")
by (simp add: add_sup_inf_distribs inf_aci)
hence "?l = 0 + inf a 0" by (simp add: a, simp add: inf_commute)
hence "inf a 0 = 0" by (simp only: add_right_cancel)
- then show "0 <= a" by (simp add: le_iff_inf inf_commute)
-next
+ then show "0 <= a" unfolding le_iff_inf by (simp add: inf_commute)
+next
assume a: "0 <= a"
show "0 <= a + a" by (simp add: add_mono[OF a a, simplified])
qed
@@ -1194,22 +1195,22 @@
qed
lemma zero_le_iff_zero_nprt: "0 \<le> a \<longleftrightarrow> nprt a = 0"
-by (simp add: le_iff_inf nprt_def inf_commute)
+unfolding le_iff_inf by (simp add: nprt_def inf_commute)
lemma le_zero_iff_zero_pprt: "a \<le> 0 \<longleftrightarrow> pprt a = 0"
-by (simp add: le_iff_sup pprt_def sup_commute)
+unfolding le_iff_sup by (simp add: pprt_def sup_commute)
lemma le_zero_iff_pprt_id: "0 \<le> a \<longleftrightarrow> pprt a = a"
-by (simp add: le_iff_sup pprt_def sup_commute)
+unfolding le_iff_sup by (simp add: pprt_def sup_commute)
lemma zero_le_iff_nprt_id: "a \<le> 0 \<longleftrightarrow> nprt a = a"
-by (simp add: le_iff_inf nprt_def inf_commute)
+unfolding le_iff_inf by (simp add: nprt_def inf_commute)
lemma pprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> pprt a \<le> pprt b"
-by (simp add: le_iff_sup pprt_def sup_aci sup_assoc [symmetric, of a])
+unfolding le_iff_sup by (simp add: pprt_def sup_aci sup_assoc [symmetric, of a])
lemma nprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> nprt a \<le> nprt b"
-by (simp add: le_iff_inf nprt_def inf_aci inf_assoc [symmetric, of a])
+unfolding le_iff_inf by (simp add: nprt_def inf_aci inf_assoc [symmetric, of a])
end
--- a/src/HOL/SEQ.thy Fri Aug 28 18:11:42 2009 +0200
+++ b/src/HOL/SEQ.thy Fri Aug 28 18:52:41 2009 +0200
@@ -582,7 +582,7 @@
ultimately
have "a (max no n) < a n" by auto
with monotone[where m=n and n="max no n"]
- show False by auto
+ show False by (auto simp:max_def split:split_if_asm)
qed
} note top_down = this
{ fix x n m fix a :: "nat \<Rightarrow> real"
--- a/src/HOL/SetInterval.thy Fri Aug 28 18:11:42 2009 +0200
+++ b/src/HOL/SetInterval.thy Fri Aug 28 18:52:41 2009 +0200
@@ -181,9 +181,10 @@
"(i : {l..u}) = (l <= i & i <= u)"
by (simp add: atLeastAtMost_def)
-text {* The above four lemmas could be declared as iffs.
- If we do so, a call to blast in Hyperreal/Star.ML, lemma @{text STAR_Int}
- seems to take forever (more than one hour). *}
+text {* The above four lemmas could be declared as iffs. Unfortunately this
+breaks many proofs. Since it only helps blast, it is better to leave well
+alone *}
+
end
subsubsection{* Emptyness, singletons, subset *}