be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
authorhaftmann
Tue Sep 22 15:36:55 2009 +0200 (2009-09-22)
changeset 32642026e7c6a6d08
parent 32637 827cac8abecc
child 32643 72979e93f919
be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
NEWS
src/HOL/Complete_Lattice.thy
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Decision_Procs/Ferrack.thy
src/HOL/Finite_Set.thy
src/HOL/Hoare_Parallel/Graph.thy
src/HOL/Lattices.thy
src/HOL/Lim.thy
src/HOL/MicroJava/BV/Effect.thy
src/HOL/MicroJava/BV/LBVSpec.thy
src/HOL/MicroJava/Comp/CorrCompTp.thy
src/HOL/OrderedGroup.thy
src/HOL/UNITY/Simple/Common.thy
src/HOL/Word/BinBoolList.thy
src/HOL/Word/BinGeneral.thy
src/HOL/Word/WordDefinition.thy
src/HOL/Word/WordShift.thy
     1.1 --- a/NEWS	Mon Sep 21 16:11:36 2009 +0200
     1.2 +++ b/NEWS	Tue Sep 22 15:36:55 2009 +0200
     1.3 @@ -102,6 +102,10 @@
     1.4  
     1.5    INCOMPATIBILITY.
     1.6  
     1.7 +* Rules inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no
     1.8 +simp rules by default any longer.  The same applies to
     1.9 +min_max.inf_absorb1 etc.!  INCOMPATIBILITY.
    1.10 +
    1.11  * Power operations on relations and functions are now one dedicate
    1.12  constant "compow" with infix syntax "^^".  Power operations on
    1.13  multiplicative monoids retains syntax "^" and is now defined generic
     2.1 --- a/src/HOL/Complete_Lattice.thy	Mon Sep 21 16:11:36 2009 +0200
     2.2 +++ b/src/HOL/Complete_Lattice.thy	Tue Sep 22 15:36:55 2009 +0200
     2.3 @@ -76,11 +76,11 @@
     2.4  
     2.5  lemma sup_bot [simp]:
     2.6    "x \<squnion> bot = x"
     2.7 -  using bot_least [of x] by (simp add: sup_commute)
     2.8 +  using bot_least [of x] by (simp add: sup_commute sup_absorb2)
     2.9  
    2.10  lemma inf_top [simp]:
    2.11    "x \<sqinter> top = x"
    2.12 -  using top_greatest [of x] by (simp add: inf_commute)
    2.13 +  using top_greatest [of x] by (simp add: inf_commute inf_absorb2)
    2.14  
    2.15  definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
    2.16    "SUPR A f = \<Squnion> (f ` A)"
     3.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Mon Sep 21 16:11:36 2009 +0200
     3.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Tue Sep 22 15:36:55 2009 +0200
     3.3 @@ -1904,7 +1904,7 @@
     3.4  	show "0 < real x * 2/3" using * by auto
     3.5  	show "real ?max + 1 \<le> real x * 2/3" using * up
     3.6  	  by (cases "0 < real x * real (lapprox_posrat prec 2 3) - 1",
     3.7 -	      auto simp add: real_of_float_max)
     3.8 +	      auto simp add: real_of_float_max min_max.sup_absorb1)
     3.9        qed
    3.10        finally have "real (?lb_horner (Float 1 -1)) + real (?lb_horner ?max)
    3.11  	\<le> ln (real x)"
     4.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Mon Sep 21 16:11:36 2009 +0200
     4.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Tue Sep 22 15:36:55 2009 +0200
     4.3 @@ -512,7 +512,7 @@
     4.4    assumes g0: "numgcd t = 0"
     4.5    shows "Inum bs t = 0"
     4.6    using g0[simplified numgcd_def] 
     4.7 -  by (induct t rule: numgcdh.induct, auto simp add: natabs0 maxcoeff_pos)
     4.8 +  by (induct t rule: numgcdh.induct, auto simp add: natabs0 maxcoeff_pos min_max.sup_absorb2)
     4.9  
    4.10  lemma numgcdh_pos: assumes gp: "g \<ge> 0" shows "numgcdh t g \<ge> 0"
    4.11    using gp
     5.1 --- a/src/HOL/Finite_Set.thy	Mon Sep 21 16:11:36 2009 +0200
     5.2 +++ b/src/HOL/Finite_Set.thy	Tue Sep 22 15:36:55 2009 +0200
     5.3 @@ -2966,11 +2966,11 @@
     5.4  
     5.5  lemma dual_max:
     5.6    "ord.max (op \<ge>) = min"
     5.7 -  by (auto simp add: ord.max_def_raw expand_fun_eq)
     5.8 +  by (auto simp add: ord.max_def_raw min_def expand_fun_eq)
     5.9  
    5.10  lemma dual_min:
    5.11    "ord.min (op \<ge>) = max"
    5.12 -  by (auto simp add: ord.min_def_raw expand_fun_eq)
    5.13 +  by (auto simp add: ord.min_def_raw max_def expand_fun_eq)
    5.14  
    5.15  lemma strict_below_fold1_iff:
    5.16    assumes "finite A" and "A \<noteq> {}"
     6.1 --- a/src/HOL/Hoare_Parallel/Graph.thy	Mon Sep 21 16:11:36 2009 +0200
     6.2 +++ b/src/HOL/Hoare_Parallel/Graph.thy	Tue Sep 22 15:36:55 2009 +0200
     6.3 @@ -187,6 +187,8 @@
     6.4  
     6.5  subsubsection{* Graph 3 *}
     6.6  
     6.7 +declare min_max.inf_absorb1 [simp] min_max.inf_absorb2 [simp]
     6.8 +
     6.9  lemma Graph3: 
    6.10    "\<lbrakk> T\<in>Reach E; R<length E \<rbrakk> \<Longrightarrow> Reach(E[R:=(fst(E!R),T)]) \<subseteq> Reach E"
    6.11  apply (unfold Reach_def)
    6.12 @@ -307,6 +309,8 @@
    6.13  apply force
    6.14  done
    6.15  
    6.16 +declare min_max.inf_absorb1 [simp del] min_max.inf_absorb2 [simp del]
    6.17 +
    6.18  subsubsection {* Graph 5 *}
    6.19  
    6.20  lemma Graph5: 
     7.1 --- a/src/HOL/Lattices.thy	Mon Sep 21 16:11:36 2009 +0200
     7.2 +++ b/src/HOL/Lattices.thy	Tue Sep 22 15:36:55 2009 +0200
     7.3 @@ -127,10 +127,10 @@
     7.4  lemma inf_left_idem[simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
     7.5    by (rule antisym) (auto intro: le_infI2)
     7.6  
     7.7 -lemma inf_absorb1[simp]: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
     7.8 +lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
     7.9    by (rule antisym) auto
    7.10  
    7.11 -lemma inf_absorb2[simp]: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
    7.12 +lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
    7.13    by (rule antisym) auto
    7.14  
    7.15  lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
    7.16 @@ -155,10 +155,10 @@
    7.17  lemma sup_left_idem[simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
    7.18    by (rule antisym) (auto intro: le_supI2)
    7.19  
    7.20 -lemma sup_absorb1[simp]: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
    7.21 +lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
    7.22    by (rule antisym) auto
    7.23  
    7.24 -lemma sup_absorb2[simp]: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
    7.25 +lemma sup_absorb2: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
    7.26    by (rule antisym) auto
    7.27  
    7.28  lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
    7.29 @@ -229,11 +229,11 @@
    7.30  
    7.31  lemma less_infI1:
    7.32    "a \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x"
    7.33 -  by (auto simp add: less_le intro: le_infI1)
    7.34 +  by (auto simp add: less_le inf_absorb1 intro: le_infI1)
    7.35  
    7.36  lemma less_infI2:
    7.37    "b \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x"
    7.38 -  by (auto simp add: less_le intro: le_infI2)
    7.39 +  by (auto simp add: less_le inf_absorb2 intro: le_infI2)
    7.40  
    7.41  end
    7.42  
     8.1 --- a/src/HOL/Lim.thy	Mon Sep 21 16:11:36 2009 +0200
     8.2 +++ b/src/HOL/Lim.thy	Tue Sep 22 15:36:55 2009 +0200
     8.3 @@ -544,7 +544,7 @@
     8.4      case True thus ?thesis using `0 < s` by auto
     8.5    next
     8.6      case False hence "s / 2 \<ge> (x - b) / 2" by auto
     8.7 -    hence "?x = (x + b) / 2" by(simp add:field_simps)
     8.8 +    hence "?x = (x + b) / 2" by (simp add: field_simps min_max.inf_absorb2)
     8.9      thus ?thesis using `b < x` by auto
    8.10    qed
    8.11    hence "0 \<le> f ?x" using all_le `?x < x` by auto
     9.1 --- a/src/HOL/MicroJava/BV/Effect.thy	Mon Sep 21 16:11:36 2009 +0200
     9.2 +++ b/src/HOL/MicroJava/BV/Effect.thy	Tue Sep 22 15:36:55 2009 +0200
     9.3 @@ -1,5 +1,4 @@
     9.4  (*  Title:      HOL/MicroJava/BV/Effect.thy
     9.5 -    ID:         $Id$
     9.6      Author:     Gerwin Klein
     9.7      Copyright   2000 Technische Universitaet Muenchen
     9.8  *)
     9.9 @@ -391,7 +390,7 @@
    9.10    with Pair 
    9.11    have "?app s \<Longrightarrow> ?P s" by (simp only:)
    9.12    moreover
    9.13 -  have "?P s \<Longrightarrow> ?app s" by (unfold app_def) (clarsimp)
    9.14 +  have "?P s \<Longrightarrow> ?app s" by (clarsimp simp add: min_max.inf_absorb2)
    9.15    ultimately
    9.16    show ?thesis by (rule iffI) 
    9.17  qed 
    10.1 --- a/src/HOL/MicroJava/BV/LBVSpec.thy	Mon Sep 21 16:11:36 2009 +0200
    10.2 +++ b/src/HOL/MicroJava/BV/LBVSpec.thy	Tue Sep 22 15:36:55 2009 +0200
    10.3 @@ -1,5 +1,4 @@
    10.4  (*  Title:      HOL/MicroJava/BV/LBVSpec.thy
    10.5 -    ID:         $Id$
    10.6      Author:     Gerwin Klein
    10.7      Copyright   1999 Technische Universitaet Muenchen
    10.8  *)
    10.9 @@ -293,7 +292,7 @@
   10.10    shows "wtl (take (pc+1) is) c 0 s = wtc c pc (wtl (take pc is) c 0 s)"
   10.11  proof -
   10.12    from suc have "take (pc+1) is=(take pc is)@[is!pc]" by (simp add: take_Suc)
   10.13 -  with suc wtl show ?thesis by (simp)
   10.14 +  with suc wtl show ?thesis by (simp add: min_max.inf_absorb2)
   10.15  qed
   10.16  
   10.17  lemma (in lbv) wtl_all:
   10.18 @@ -308,7 +307,7 @@
   10.19    with all have take: "?wtl (take pc is@i#r) \<noteq> \<top>" by simp 
   10.20    from pc have "is!pc = drop pc is ! 0" by simp
   10.21    with Cons have "is!pc = i" by simp
   10.22 -  with take pc show ?thesis by (auto)
   10.23 +  with take pc show ?thesis by (auto simp add: min_max.inf_absorb2)
   10.24  qed
   10.25  
   10.26  section "preserves-type"
    11.1 --- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Mon Sep 21 16:11:36 2009 +0200
    11.2 +++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Tue Sep 22 15:36:55 2009 +0200
    11.3 @@ -1,5 +1,4 @@
    11.4  (*  Title:      HOL/MicroJava/Comp/CorrCompTp.thy
    11.5 -    ID:         $Id$
    11.6      Author:     Martin Strecker
    11.7  *)
    11.8  
    11.9 @@ -1058,7 +1057,7 @@
   11.10  lemma bc_mt_corresp_New: "\<lbrakk>is_class cG cname \<rbrakk>
   11.11    \<Longrightarrow> bc_mt_corresp [New cname] (pushST [Class cname]) (ST, LT) cG rT mxr (Suc 0)"
   11.12  apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
   11.13 -    max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
   11.14 +    max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
   11.15  apply (intro strip)
   11.16  apply (rule conjI)
   11.17  apply (rule check_type_mono, assumption, simp)
   11.18 @@ -1069,7 +1068,7 @@
   11.19    bc_mt_corresp [Pop] (popST (Suc 0)) (T # ST, LT) cG rT mxr (Suc 0)"
   11.20    apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def)
   11.21    apply (simp add: max_ssize_def ssize_sto_def max_of_list_def) 
   11.22 -  apply (simp add: check_type_simps)
   11.23 +  apply (simp add: check_type_simps min_max.sup_absorb1)
   11.24    apply clarify
   11.25    apply (rule_tac x="(length ST)" in exI)
   11.26    apply simp+
   11.27 @@ -1092,7 +1091,7 @@
   11.28    \<Longrightarrow> bc_mt_corresp [LitPush val] (pushST [T]) sttp cG rT mxr (Suc 0)"
   11.29  apply (subgoal_tac "\<exists> ST LT. sttp= (ST, LT)", (erule exE)+)
   11.30    apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
   11.31 -              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
   11.32 +              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
   11.33    apply (intro strip)
   11.34    apply (rule conjI)
   11.35    apply (rule check_type_mono, assumption, simp)
   11.36 @@ -1111,7 +1110,7 @@
   11.37    \<Longrightarrow> bc_mt_corresp [LitPush val] (pushST [T']) sttp cG rT mxr (Suc 0)"
   11.38  apply (subgoal_tac "\<exists> ST LT. sttp= (ST, LT)", (erule exE)+)
   11.39    apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
   11.40 -              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
   11.41 +              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
   11.42    apply (intro strip)
   11.43    apply (rule conjI)
   11.44    apply (rule check_type_mono, assumption, simp)
   11.45 @@ -1127,7 +1126,7 @@
   11.46    \<Longrightarrow> bc_mt_corresp [Load i] 
   11.47           (\<lambda>(ST, LT). pushST [ok_val (LT ! i)] (ST, LT)) (ST, LT) cG rT mxr (Suc 0)"
   11.48  apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
   11.49 -            max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
   11.50 +            max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
   11.51    apply (intro strip)
   11.52    apply (rule conjI)
   11.53    apply (rule check_type_mono, assumption, simp)
   11.54 @@ -1148,10 +1147,10 @@
   11.55  lemma bc_mt_corresp_Store_init: "\<lbrakk> i < length LT \<rbrakk>
   11.56    \<Longrightarrow> bc_mt_corresp [Store i] (storeST i T) (T # ST, LT) cG rT mxr (Suc 0)"
   11.57   apply (simp add: bc_mt_corresp_def storeST_def wt_instr_altern_def eff_def norm_eff_def)
   11.58 -  apply (simp add: max_ssize_def  max_of_list_def )
   11.59 +  apply (simp add: max_ssize_def  max_of_list_def)
   11.60    apply (simp add: ssize_sto_def)
   11.61    apply (intro strip)
   11.62 -apply (simp add: check_type_simps)
   11.63 +apply (simp add: check_type_simps min_max.sup_absorb1)
   11.64  apply clarify
   11.65  apply (rule conjI)
   11.66  apply (rule_tac x="(length ST)" in exI)
   11.67 @@ -1159,14 +1158,13 @@
   11.68  done
   11.69  
   11.70  
   11.71 -
   11.72  lemma bc_mt_corresp_Store: "\<lbrakk> i < length LT; cG  \<turnstile>  LT[i := OK T] <=l LT \<rbrakk>
   11.73    \<Longrightarrow> bc_mt_corresp [Store i] (popST (Suc 0)) (T # ST, LT) cG rT mxr (Suc 0)"
   11.74    apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def)
   11.75    apply (simp add: sup_state_conv)
   11.76    apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
   11.77   apply (intro strip)
   11.78 -apply (simp add: check_type_simps)
   11.79 +apply (simp add: check_type_simps min_max.sup_absorb1)
   11.80  apply clarify
   11.81  apply (rule_tac x="(length ST)" in exI)
   11.82  apply simp+
   11.83 @@ -1176,7 +1174,7 @@
   11.84  lemma bc_mt_corresp_Dup: "
   11.85    bc_mt_corresp [Dup] dupST (T # ST, LT) cG rT mxr (Suc 0)"
   11.86   apply (simp add: bc_mt_corresp_def dupST_def wt_instr_altern_def
   11.87 -             max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
   11.88 +             max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
   11.89    apply (intro strip)
   11.90    apply (rule conjI)
   11.91    apply (rule check_type_mono, assumption, simp)
   11.92 @@ -1189,7 +1187,7 @@
   11.93  lemma bc_mt_corresp_Dup_x1: "
   11.94    bc_mt_corresp [Dup_x1] dup_x1ST (T1 # T2 # ST, LT) cG rT mxr (Suc 0)"
   11.95    apply (simp add: bc_mt_corresp_def dup_x1ST_def wt_instr_altern_def
   11.96 -              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
   11.97 +              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
   11.98    apply (intro strip)
   11.99    apply (rule conjI)
  11.100    apply (rule check_type_mono, assumption, simp)
  11.101 @@ -1206,7 +1204,7 @@
  11.102           (PrimT Integer # PrimT Integer # ST, LT) cG rT mxr (Suc 0)"
  11.103    apply (simp add: bc_mt_corresp_def replST_def wt_instr_altern_def eff_def norm_eff_def)
  11.104    apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
  11.105 -  apply (simp add: check_type_simps)
  11.106 +  apply (simp add: check_type_simps min_max.sup_absorb1)
  11.107    apply clarify
  11.108    apply (rule_tac x="Suc (length ST)" in exI)
  11.109    apply simp+
  11.110 @@ -1249,7 +1247,7 @@
  11.111    apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
  11.112  
  11.113    apply (intro strip)
  11.114 -apply (simp add: check_type_simps)
  11.115 +apply (simp add: check_type_simps min_max.sup_absorb1)
  11.116  apply clarify
  11.117  apply (rule_tac x="Suc (length ST)" in exI)
  11.118  apply simp+
    12.1 --- a/src/HOL/OrderedGroup.thy	Mon Sep 21 16:11:36 2009 +0200
    12.2 +++ b/src/HOL/OrderedGroup.thy	Tue Sep 22 15:36:55 2009 +0200
    12.3 @@ -1075,17 +1075,16 @@
    12.4  lemma nprt_0[simp]: "nprt 0 = 0" by (simp add: nprt_def)
    12.5  
    12.6  lemma pprt_eq_id [simp, noatp]: "0 \<le> x \<Longrightarrow> pprt x = x"
    12.7 -by (simp add: pprt_def sup_aci)
    12.8 -
    12.9 +  by (simp add: pprt_def sup_aci sup_absorb1)
   12.10  
   12.11  lemma nprt_eq_id [simp, noatp]: "x \<le> 0 \<Longrightarrow> nprt x = x"
   12.12 -by (simp add: nprt_def inf_aci)
   12.13 +  by (simp add: nprt_def inf_aci inf_absorb1)
   12.14  
   12.15  lemma pprt_eq_0 [simp, noatp]: "x \<le> 0 \<Longrightarrow> pprt x = 0"
   12.16 -by (simp add: pprt_def sup_aci)
   12.17 +  by (simp add: pprt_def sup_aci sup_absorb2)
   12.18  
   12.19  lemma nprt_eq_0 [simp, noatp]: "0 \<le> x \<Longrightarrow> nprt x = 0"
   12.20 -by (simp add: nprt_def inf_aci)
   12.21 +  by (simp add: nprt_def inf_aci inf_absorb2)
   12.22  
   12.23  lemma sup_0_imp_0: "sup a (- a) = 0 \<Longrightarrow> a = 0"
   12.24  proof -
   12.25 @@ -1119,7 +1118,7 @@
   12.26    "0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
   12.27  proof
   12.28    assume "0 <= a + a"
   12.29 -  hence a:"inf (a+a) 0 = 0" by (simp add: inf_commute)
   12.30 +  hence a:"inf (a+a) 0 = 0" by (simp add: inf_commute inf_absorb1)
   12.31    have "(inf a 0)+(inf a 0) = inf (inf (a+a) 0) a" (is "?l=_")
   12.32      by (simp add: add_sup_inf_distribs inf_aci)
   12.33    hence "?l = 0 + inf a 0" by (simp add: a, simp add: inf_commute)
   12.34 @@ -1135,7 +1134,7 @@
   12.35    assume assm: "a + a = 0"
   12.36    then have "a + a + - a = - a" by simp
   12.37    then have "a + (a + - a) = - a" by (simp only: add_assoc)
   12.38 -  then have a: "- a = a" by simp (*FIXME tune proof*)
   12.39 +  then have a: "- a = a" by simp
   12.40    show "a = 0" apply (rule antisym)
   12.41    apply (unfold neg_le_iff_le [symmetric, of a])
   12.42    unfolding a apply simp
   12.43 @@ -1275,7 +1274,7 @@
   12.44  proof -
   12.45    note add_le_cancel_right [of a a "- a", symmetric, simplified]
   12.46    moreover note add_le_cancel_right [of "-a" a a, symmetric, simplified]
   12.47 -  then show ?thesis by (auto simp: sup_max)
   12.48 +  then show ?thesis by (auto simp: sup_max min_max.sup_absorb1 min_max.sup_absorb2)
   12.49  qed
   12.50  
   12.51  lemma abs_if_lattice:
    13.1 --- a/src/HOL/UNITY/Simple/Common.thy	Mon Sep 21 16:11:36 2009 +0200
    13.2 +++ b/src/HOL/UNITY/Simple/Common.thy	Tue Sep 22 15:36:55 2009 +0200
    13.3 @@ -1,5 +1,4 @@
    13.4  (*  Title:      HOL/UNITY/Common
    13.5 -    ID:         $Id$
    13.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    13.7      Copyright   1998  University of Cambridge
    13.8  
    13.9 @@ -10,7 +9,9 @@
   13.10  From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1.
   13.11  *)
   13.12  
   13.13 -theory Common imports "../UNITY_Main" begin
   13.14 +theory Common
   13.15 +imports "../UNITY_Main"
   13.16 +begin
   13.17  
   13.18  consts
   13.19    ftime :: "nat=>nat"
   13.20 @@ -65,7 +66,7 @@
   13.21  lemma "mk_total_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}, UNIV)
   13.22         \<in> {m} co (maxfg m)"
   13.23  apply (simp add: mk_total_program_def) 
   13.24 -apply (simp add: constrains_def maxfg_def gasc)
   13.25 +apply (simp add: constrains_def maxfg_def gasc min_max.sup_absorb2)
   13.26  done
   13.27  
   13.28  (*This one is  t := t+1 if t <max (ftime t) (gtime t) *)
   13.29 @@ -73,7 +74,7 @@
   13.30            (UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }, UNIV)   
   13.31         \<in> {m} co (maxfg m)"
   13.32  apply (simp add: mk_total_program_def) 
   13.33 -apply (simp add: constrains_def maxfg_def gasc)
   13.34 +apply (simp add: constrains_def maxfg_def gasc min_max.sup_absorb2)
   13.35  done
   13.36  
   13.37  
    14.1 --- a/src/HOL/Word/BinBoolList.thy	Mon Sep 21 16:11:36 2009 +0200
    14.2 +++ b/src/HOL/Word/BinBoolList.thy	Tue Sep 22 15:36:55 2009 +0200
    14.3 @@ -919,7 +919,7 @@
    14.4    apply (drule spec)
    14.5    apply (erule trans)
    14.6    apply (drule_tac x = "bin_cat y n a" in spec)
    14.7 -  apply (simp add : bin_cat_assoc_sym)
    14.8 +  apply (simp add : bin_cat_assoc_sym min_max.inf_absorb2)
    14.9    done
   14.10  
   14.11  lemma bin_rcat_bl:
    15.1 --- a/src/HOL/Word/BinGeneral.thy	Mon Sep 21 16:11:36 2009 +0200
    15.2 +++ b/src/HOL/Word/BinGeneral.thy	Tue Sep 22 15:36:55 2009 +0200
    15.3 @@ -508,7 +508,7 @@
    15.4  lemma sbintrunc_sbintrunc_min [simp]:
    15.5    "sbintrunc m (sbintrunc n w) = sbintrunc (min m n) w"
    15.6    apply (rule bin_eqI)
    15.7 -  apply (auto simp: nth_sbintr)
    15.8 +  apply (auto simp: nth_sbintr min_max.inf_absorb1 min_max.inf_absorb2)
    15.9    done
   15.10  
   15.11  lemmas bintrunc_Pls = 
    16.1 --- a/src/HOL/Word/WordDefinition.thy	Mon Sep 21 16:11:36 2009 +0200
    16.2 +++ b/src/HOL/Word/WordDefinition.thy	Tue Sep 22 15:36:55 2009 +0200
    16.3 @@ -381,14 +381,14 @@
    16.4    apply (unfold word_size)
    16.5    apply (subst word_ubin.norm_Rep [symmetric]) 
    16.6    apply (simp only: bintrunc_bintrunc_min word_size)
    16.7 -  apply simp
    16.8 +  apply (simp add: min_max.inf_absorb2)
    16.9    done
   16.10  
   16.11  lemma wi_bintr': 
   16.12    "wb = word_of_int bin ==> n >= size wb ==> 
   16.13      word_of_int (bintrunc n bin) = wb"
   16.14    unfolding word_size
   16.15 -  by (clarsimp simp add : word_ubin.norm_eq_iff [symmetric])
   16.16 +  by (clarsimp simp add: word_ubin.norm_eq_iff [symmetric] min_max.inf_absorb1)
   16.17  
   16.18  lemmas bintr_uint = bintr_uint' [unfolded word_size]
   16.19  lemmas wi_bintr = wi_bintr' [unfolded word_size]
    17.1 --- a/src/HOL/Word/WordShift.thy	Mon Sep 21 16:11:36 2009 +0200
    17.2 +++ b/src/HOL/Word/WordShift.thy	Tue Sep 22 15:36:55 2009 +0200
    17.3 @@ -1017,8 +1017,8 @@
    17.4    (word_cat (word_of_int w :: 'b word) (b :: 'c word) :: 'a word) = 
    17.5    word_of_int (bin_cat w (size b) (uint b))"
    17.6    apply (unfold word_cat_def word_size) 
    17.7 -  apply (clarsimp simp add : word_ubin.norm_eq_iff [symmetric]
    17.8 -      word_ubin.eq_norm bintr_cat)
    17.9 +  apply (clarsimp simp add: word_ubin.norm_eq_iff [symmetric]
   17.10 +      word_ubin.eq_norm bintr_cat min_max.inf_absorb1)
   17.11    done
   17.12  
   17.13  lemma word_cat_split_alt: