Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
authornipkow
Fri Aug 28 18:52:41 2009 +0200 (2009-08-28)
changeset 3243610cd49e0c067
parent 32435 711d680eab26
child 32437 66f1a0dfe7d9
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
src/HOL/Algebra/UnivPoly.thy
src/HOL/Algebra/poly/UnivPoly2.thy
src/HOL/Complete_Lattice.thy
src/HOL/Lattices.thy
src/HOL/Lim.thy
src/HOL/MicroJava/Comp/CorrCompTp.thy
src/HOL/OrderedGroup.thy
src/HOL/SEQ.thy
src/HOL/SetInterval.thy
     1.1 --- a/src/HOL/Algebra/UnivPoly.thy	Fri Aug 28 18:11:42 2009 +0200
     1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Fri Aug 28 18:52:41 2009 +0200
     1.3 @@ -817,15 +817,9 @@
     1.4  text {* Degree and polynomial operations *}
     1.5  
     1.6  lemma deg_add [simp]:
     1.7 -  assumes R: "p \<in> carrier P" "q \<in> carrier P"
     1.8 -  shows "deg R (p \<oplus>\<^bsub>P\<^esub> q) <= max (deg R p) (deg R q)"
     1.9 -proof (cases "deg R p <= deg R q")
    1.10 -  case True show ?thesis
    1.11 -    by (rule deg_aboveI) (simp_all add: True R deg_aboveD)
    1.12 -next
    1.13 -  case False show ?thesis
    1.14 -    by (rule deg_aboveI) (simp_all add: False R deg_aboveD)
    1.15 -qed
    1.16 +  "p \<in> carrier P \<Longrightarrow> q \<in> carrier P \<Longrightarrow>
    1.17 +  deg R (p \<oplus>\<^bsub>P\<^esub> q) <= max (deg R p) (deg R q)"
    1.18 +by(rule deg_aboveI)(simp_all add: deg_aboveD)
    1.19  
    1.20  lemma deg_monom_le:
    1.21    "a \<in> carrier R ==> deg R (monom P a n) <= n"
     2.1 --- a/src/HOL/Algebra/poly/UnivPoly2.thy	Fri Aug 28 18:11:42 2009 +0200
     2.2 +++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Fri Aug 28 18:52:41 2009 +0200
     2.3 @@ -563,11 +563,7 @@
     2.4  
     2.5  lemma deg_add [simp]:
     2.6    "deg ((p::'a::ring up) + q) <= max (deg p) (deg q)"
     2.7 -proof (cases "deg p <= deg q")
     2.8 -  case True show ?thesis by (rule deg_aboveI) (simp add: True deg_aboveD) 
     2.9 -next
    2.10 -  case False show ?thesis by (rule deg_aboveI) (simp add: False deg_aboveD)
    2.11 -qed
    2.12 +by (rule deg_aboveI) (simp add: deg_aboveD)
    2.13  
    2.14  lemma deg_monom_ring:
    2.15    "deg (monom a n::'a::ring up) <= n"
     3.1 --- a/src/HOL/Complete_Lattice.thy	Fri Aug 28 18:11:42 2009 +0200
     3.2 +++ b/src/HOL/Complete_Lattice.thy	Fri Aug 28 18:52:41 2009 +0200
     3.3 @@ -76,11 +76,11 @@
     3.4  
     3.5  lemma sup_bot [simp]:
     3.6    "x \<squnion> bot = x"
     3.7 -  using bot_least [of x] by (simp add: le_iff_sup sup_commute)
     3.8 +  using bot_least [of x] by (simp add: sup_commute)
     3.9  
    3.10  lemma inf_top [simp]:
    3.11    "x \<sqinter> top = x"
    3.12 -  using top_greatest [of x] by (simp add: le_iff_inf inf_commute)
    3.13 +  using top_greatest [of x] by (simp add: inf_commute)
    3.14  
    3.15  definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
    3.16    "SUPR A f = \<Squnion> (f ` A)"
     4.1 --- a/src/HOL/Lattices.thy	Fri Aug 28 18:11:42 2009 +0200
     4.2 +++ b/src/HOL/Lattices.thy	Fri Aug 28 18:52:41 2009 +0200
     4.3 @@ -125,10 +125,10 @@
     4.4  lemma inf_left_idem[simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
     4.5    by (rule antisym) (auto intro: le_infI2)
     4.6  
     4.7 -lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
     4.8 +lemma inf_absorb1[simp]: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
     4.9    by (rule antisym) auto
    4.10  
    4.11 -lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
    4.12 +lemma inf_absorb2[simp]: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
    4.13    by (rule antisym) auto
    4.14  
    4.15  lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
    4.16 @@ -153,10 +153,10 @@
    4.17  lemma sup_left_idem[simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
    4.18    by (rule antisym) (auto intro: le_supI2)
    4.19  
    4.20 -lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
    4.21 +lemma sup_absorb1[simp]: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
    4.22    by (rule antisym) auto
    4.23  
    4.24 -lemma sup_absorb2: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
    4.25 +lemma sup_absorb2[simp]: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
    4.26    by (rule antisym) auto
    4.27  
    4.28  lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
    4.29 @@ -199,7 +199,7 @@
    4.30  shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
    4.31  proof-
    4.32    have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by(simp add:sup_inf_absorb)
    4.33 -  also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))" by(simp add:D inf_commute sup_assoc)
    4.34 +  also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))" by(simp add:D inf_commute sup_assoc del:sup_absorb1)
    4.35    also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)"
    4.36      by(simp add:inf_sup_absorb inf_commute)
    4.37    also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:D)
    4.38 @@ -211,7 +211,7 @@
    4.39  shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
    4.40  proof-
    4.41    have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)" by(simp add:inf_sup_absorb)
    4.42 -  also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))" by(simp add:D sup_commute inf_assoc)
    4.43 +  also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))" by(simp add:D sup_commute inf_assoc del:inf_absorb1)
    4.44    also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)"
    4.45      by(simp add:sup_inf_absorb sup_commute)
    4.46    also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by(simp add:D)
     5.1 --- a/src/HOL/Lim.thy	Fri Aug 28 18:11:42 2009 +0200
     5.2 +++ b/src/HOL/Lim.thy	Fri Aug 28 18:52:41 2009 +0200
     5.3 @@ -544,8 +544,7 @@
     5.4      case True thus ?thesis using `0 < s` by auto
     5.5    next
     5.6      case False hence "s / 2 \<ge> (x - b) / 2" by auto
     5.7 -    from inf_absorb2[OF this, unfolded inf_real_def]
     5.8 -    have "?x = (x + b) / 2" by auto
     5.9 +    hence "?x = (x + b) / 2" by(simp add:field_simps)
    5.10      thus ?thesis using `b < x` by auto
    5.11    qed
    5.12    hence "0 \<le> f ?x" using all_le `?x < x` by auto
     6.1 --- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Fri Aug 28 18:11:42 2009 +0200
     6.2 +++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Fri Aug 28 18:52:41 2009 +0200
     6.3 @@ -1070,7 +1070,6 @@
     6.4    bc_mt_corresp [Pop] (popST (Suc 0)) (T # ST, LT) cG rT mxr (Suc 0)"
     6.5    apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def)
     6.6    apply (simp add: max_ssize_def ssize_sto_def max_of_list_def) 
     6.7 -  apply (simp add: max_def)
     6.8    apply (simp add: check_type_simps)
     6.9    apply clarify
    6.10    apply (rule_tac x="(length ST)" in exI)
    6.11 @@ -1154,7 +1153,7 @@
    6.12    \<Longrightarrow> bc_mt_corresp [Store i] (storeST i T) (T # ST, LT) cG rT mxr (Suc 0)"
    6.13   apply (simp add: bc_mt_corresp_def storeST_def wt_instr_altern_def eff_def norm_eff_def)
    6.14    apply (simp add: max_ssize_def  max_of_list_def )
    6.15 -  apply (simp add: ssize_sto_def) apply (simp add: max_def)
    6.16 +  apply (simp add: ssize_sto_def)
    6.17    apply (intro strip)
    6.18  apply (simp add: check_type_simps)
    6.19  apply clarify
    6.20 @@ -1170,7 +1169,6 @@
    6.21    apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def)
    6.22    apply (simp add: sup_state_conv)
    6.23    apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
    6.24 -  apply (simp add: max_def)
    6.25   apply (intro strip)
    6.26  apply (simp add: check_type_simps)
    6.27  apply clarify
     7.1 --- a/src/HOL/OrderedGroup.thy	Fri Aug 28 18:11:42 2009 +0200
     7.2 +++ b/src/HOL/OrderedGroup.thy	Fri Aug 28 18:52:41 2009 +0200
     7.3 @@ -1075,16 +1075,17 @@
     7.4  lemma nprt_0[simp]: "nprt 0 = 0" by (simp add: nprt_def)
     7.5  
     7.6  lemma pprt_eq_id [simp, noatp]: "0 \<le> x \<Longrightarrow> pprt x = x"
     7.7 -by (simp add: pprt_def le_iff_sup sup_aci)
     7.8 +by (simp add: pprt_def sup_aci)
     7.9 +
    7.10  
    7.11  lemma nprt_eq_id [simp, noatp]: "x \<le> 0 \<Longrightarrow> nprt x = x"
    7.12 -by (simp add: nprt_def le_iff_inf inf_aci)
    7.13 +by (simp add: nprt_def inf_aci)
    7.14  
    7.15  lemma pprt_eq_0 [simp, noatp]: "x \<le> 0 \<Longrightarrow> pprt x = 0"
    7.16 -by (simp add: pprt_def le_iff_sup sup_aci)
    7.17 +by (simp add: pprt_def sup_aci)
    7.18  
    7.19  lemma nprt_eq_0 [simp, noatp]: "0 \<le> x \<Longrightarrow> nprt x = 0"
    7.20 -by (simp add: nprt_def le_iff_inf inf_aci)
    7.21 +by (simp add: nprt_def inf_aci)
    7.22  
    7.23  lemma sup_0_imp_0: "sup a (- a) = 0 \<Longrightarrow> a = 0"
    7.24  proof -
    7.25 @@ -1118,13 +1119,13 @@
    7.26    "0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
    7.27  proof
    7.28    assume "0 <= a + a"
    7.29 -  hence a:"inf (a+a) 0 = 0" by (simp add: le_iff_inf inf_commute)
    7.30 +  hence a:"inf (a+a) 0 = 0" by (simp add: inf_commute)
    7.31    have "(inf a 0)+(inf a 0) = inf (inf (a+a) 0) a" (is "?l=_")
    7.32      by (simp add: add_sup_inf_distribs inf_aci)
    7.33    hence "?l = 0 + inf a 0" by (simp add: a, simp add: inf_commute)
    7.34    hence "inf a 0 = 0" by (simp only: add_right_cancel)
    7.35 -  then show "0 <= a" by (simp add: le_iff_inf inf_commute)    
    7.36 -next  
    7.37 +  then show "0 <= a" unfolding le_iff_inf by (simp add: inf_commute)
    7.38 +next
    7.39    assume a: "0 <= a"
    7.40    show "0 <= a + a" by (simp add: add_mono[OF a a, simplified])
    7.41  qed
    7.42 @@ -1194,22 +1195,22 @@
    7.43  qed
    7.44  
    7.45  lemma zero_le_iff_zero_nprt: "0 \<le> a \<longleftrightarrow> nprt a = 0"
    7.46 -by (simp add: le_iff_inf nprt_def inf_commute)
    7.47 +unfolding le_iff_inf by (simp add: nprt_def inf_commute)
    7.48  
    7.49  lemma le_zero_iff_zero_pprt: "a \<le> 0 \<longleftrightarrow> pprt a = 0"
    7.50 -by (simp add: le_iff_sup pprt_def sup_commute)
    7.51 +unfolding le_iff_sup by (simp add: pprt_def sup_commute)
    7.52  
    7.53  lemma le_zero_iff_pprt_id: "0 \<le> a \<longleftrightarrow> pprt a = a"
    7.54 -by (simp add: le_iff_sup pprt_def sup_commute)
    7.55 +unfolding le_iff_sup by (simp add: pprt_def sup_commute)
    7.56  
    7.57  lemma zero_le_iff_nprt_id: "a \<le> 0 \<longleftrightarrow> nprt a = a"
    7.58 -by (simp add: le_iff_inf nprt_def inf_commute)
    7.59 +unfolding le_iff_inf by (simp add: nprt_def inf_commute)
    7.60  
    7.61  lemma pprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> pprt a \<le> pprt b"
    7.62 -by (simp add: le_iff_sup pprt_def sup_aci sup_assoc [symmetric, of a])
    7.63 +unfolding le_iff_sup by (simp add: pprt_def sup_aci sup_assoc [symmetric, of a])
    7.64  
    7.65  lemma nprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> nprt a \<le> nprt b"
    7.66 -by (simp add: le_iff_inf nprt_def inf_aci inf_assoc [symmetric, of a])
    7.67 +unfolding le_iff_inf by (simp add: nprt_def inf_aci inf_assoc [symmetric, of a])
    7.68  
    7.69  end
    7.70  
     8.1 --- a/src/HOL/SEQ.thy	Fri Aug 28 18:11:42 2009 +0200
     8.2 +++ b/src/HOL/SEQ.thy	Fri Aug 28 18:52:41 2009 +0200
     8.3 @@ -582,7 +582,7 @@
     8.4        ultimately
     8.5        have "a (max no n) < a n" by auto
     8.6        with monotone[where m=n and n="max no n"]
     8.7 -      show False by auto
     8.8 +      show False by (auto simp:max_def split:split_if_asm)
     8.9      qed
    8.10    } note top_down = this
    8.11    { fix x n m fix a :: "nat \<Rightarrow> real"
     9.1 --- a/src/HOL/SetInterval.thy	Fri Aug 28 18:11:42 2009 +0200
     9.2 +++ b/src/HOL/SetInterval.thy	Fri Aug 28 18:52:41 2009 +0200
     9.3 @@ -181,9 +181,10 @@
     9.4    "(i : {l..u}) = (l <= i & i <= u)"
     9.5  by (simp add: atLeastAtMost_def)
     9.6  
     9.7 -text {* The above four lemmas could be declared as iffs.
     9.8 -  If we do so, a call to blast in Hyperreal/Star.ML, lemma @{text STAR_Int}
     9.9 -  seems to take forever (more than one hour). *}
    9.10 +text {* The above four lemmas could be declared as iffs. Unfortunately this
    9.11 +breaks many proofs. Since it only helps blast, it is better to leave well
    9.12 +alone *}
    9.13 +
    9.14  end
    9.15  
    9.16  subsubsection{* Emptyness, singletons, subset *}