# HG changeset patch
# User nipkow
# Date 1251478361 -7200
# Node ID 10cd49e0c067a137feeaf6cd658817678ef8fecc
# Parent  711d680eab260ebeab61a34193128f3c78b9d625
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules

diff -r 711d680eab26 -r 10cd49e0c067 src/HOL/Algebra/UnivPoly.thy
--- 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"
diff -r 711d680eab26 -r 10cd49e0c067 src/HOL/Algebra/poly/UnivPoly2.thy
--- 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"
diff -r 711d680eab26 -r 10cd49e0c067 src/HOL/Complete_Lattice.thy
--- 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)"
diff -r 711d680eab26 -r 10cd49e0c067 src/HOL/Lattices.thy
--- 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)
diff -r 711d680eab26 -r 10cd49e0c067 src/HOL/Lim.thy
--- 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
diff -r 711d680eab26 -r 10cd49e0c067 src/HOL/MicroJava/Comp/CorrCompTp.thy
--- 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
diff -r 711d680eab26 -r 10cd49e0c067 src/HOL/OrderedGroup.thy
--- 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
 
diff -r 711d680eab26 -r 10cd49e0c067 src/HOL/SEQ.thy
--- 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"
diff -r 711d680eab26 -r 10cd49e0c067 src/HOL/SetInterval.thy
--- 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 *}