be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
--- a/NEWS Mon Sep 21 16:11:36 2009 +0200
+++ b/NEWS Tue Sep 22 15:36:55 2009 +0200
@@ -102,6 +102,10 @@
INCOMPATIBILITY.
+* Rules inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no
+simp rules by default any longer. The same applies to
+min_max.inf_absorb1 etc.! INCOMPATIBILITY.
+
* Power operations on relations and functions are now one dedicate
constant "compow" with infix syntax "^^". Power operations on
multiplicative monoids retains syntax "^" and is now defined generic
--- a/src/HOL/Complete_Lattice.thy Mon Sep 21 16:11:36 2009 +0200
+++ b/src/HOL/Complete_Lattice.thy Tue Sep 22 15:36:55 2009 +0200
@@ -76,11 +76,11 @@
lemma sup_bot [simp]:
"x \<squnion> bot = x"
- using bot_least [of x] by (simp add: sup_commute)
+ using bot_least [of x] by (simp add: sup_commute sup_absorb2)
lemma inf_top [simp]:
"x \<sqinter> top = x"
- using top_greatest [of x] by (simp add: inf_commute)
+ using top_greatest [of x] by (simp add: inf_commute inf_absorb2)
definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
"SUPR A f = \<Squnion> (f ` A)"
--- a/src/HOL/Decision_Procs/Approximation.thy Mon Sep 21 16:11:36 2009 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Tue Sep 22 15:36:55 2009 +0200
@@ -1904,7 +1904,7 @@
show "0 < real x * 2/3" using * by auto
show "real ?max + 1 \<le> real x * 2/3" using * up
by (cases "0 < real x * real (lapprox_posrat prec 2 3) - 1",
- auto simp add: real_of_float_max)
+ auto simp add: real_of_float_max min_max.sup_absorb1)
qed
finally have "real (?lb_horner (Float 1 -1)) + real (?lb_horner ?max)
\<le> ln (real x)"
--- a/src/HOL/Decision_Procs/Ferrack.thy Mon Sep 21 16:11:36 2009 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy Tue Sep 22 15:36:55 2009 +0200
@@ -512,7 +512,7 @@
assumes g0: "numgcd t = 0"
shows "Inum bs t = 0"
using g0[simplified numgcd_def]
- by (induct t rule: numgcdh.induct, auto simp add: natabs0 maxcoeff_pos)
+ by (induct t rule: numgcdh.induct, auto simp add: natabs0 maxcoeff_pos min_max.sup_absorb2)
lemma numgcdh_pos: assumes gp: "g \<ge> 0" shows "numgcdh t g \<ge> 0"
using gp
--- a/src/HOL/Finite_Set.thy Mon Sep 21 16:11:36 2009 +0200
+++ b/src/HOL/Finite_Set.thy Tue Sep 22 15:36:55 2009 +0200
@@ -2966,11 +2966,11 @@
lemma dual_max:
"ord.max (op \<ge>) = min"
- by (auto simp add: ord.max_def_raw expand_fun_eq)
+ by (auto simp add: ord.max_def_raw min_def expand_fun_eq)
lemma dual_min:
"ord.min (op \<ge>) = max"
- by (auto simp add: ord.min_def_raw expand_fun_eq)
+ by (auto simp add: ord.min_def_raw max_def expand_fun_eq)
lemma strict_below_fold1_iff:
assumes "finite A" and "A \<noteq> {}"
--- a/src/HOL/Hoare_Parallel/Graph.thy Mon Sep 21 16:11:36 2009 +0200
+++ b/src/HOL/Hoare_Parallel/Graph.thy Tue Sep 22 15:36:55 2009 +0200
@@ -187,6 +187,8 @@
subsubsection{* Graph 3 *}
+declare min_max.inf_absorb1 [simp] min_max.inf_absorb2 [simp]
+
lemma Graph3:
"\<lbrakk> T\<in>Reach E; R<length E \<rbrakk> \<Longrightarrow> Reach(E[R:=(fst(E!R),T)]) \<subseteq> Reach E"
apply (unfold Reach_def)
@@ -307,6 +309,8 @@
apply force
done
+declare min_max.inf_absorb1 [simp del] min_max.inf_absorb2 [simp del]
+
subsubsection {* Graph 5 *}
lemma Graph5:
--- a/src/HOL/Lattices.thy Mon Sep 21 16:11:36 2009 +0200
+++ b/src/HOL/Lattices.thy Tue Sep 22 15:36:55 2009 +0200
@@ -127,10 +127,10 @@
lemma inf_left_idem[simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
by (rule antisym) (auto intro: le_infI2)
-lemma inf_absorb1[simp]: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
+lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
by (rule antisym) auto
-lemma inf_absorb2[simp]: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
+lemma inf_absorb2: "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)"
@@ -155,10 +155,10 @@
lemma sup_left_idem[simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
by (rule antisym) (auto intro: le_supI2)
-lemma sup_absorb1[simp]: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
+lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
by (rule antisym) auto
-lemma sup_absorb2[simp]: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
+lemma sup_absorb2: "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)"
@@ -229,11 +229,11 @@
lemma less_infI1:
"a \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x"
- by (auto simp add: less_le intro: le_infI1)
+ by (auto simp add: less_le inf_absorb1 intro: le_infI1)
lemma less_infI2:
"b \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x"
- by (auto simp add: less_le intro: le_infI2)
+ by (auto simp add: less_le inf_absorb2 intro: le_infI2)
end
--- a/src/HOL/Lim.thy Mon Sep 21 16:11:36 2009 +0200
+++ b/src/HOL/Lim.thy Tue Sep 22 15:36:55 2009 +0200
@@ -544,7 +544,7 @@
case True thus ?thesis using `0 < s` by auto
next
case False hence "s / 2 \<ge> (x - b) / 2" by auto
- hence "?x = (x + b) / 2" by(simp add:field_simps)
+ hence "?x = (x + b) / 2" by (simp add: field_simps min_max.inf_absorb2)
thus ?thesis using `b < x` by auto
qed
hence "0 \<le> f ?x" using all_le `?x < x` by auto
--- a/src/HOL/MicroJava/BV/Effect.thy Mon Sep 21 16:11:36 2009 +0200
+++ b/src/HOL/MicroJava/BV/Effect.thy Tue Sep 22 15:36:55 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/MicroJava/BV/Effect.thy
- ID: $Id$
Author: Gerwin Klein
Copyright 2000 Technische Universitaet Muenchen
*)
@@ -391,7 +390,7 @@
with Pair
have "?app s \<Longrightarrow> ?P s" by (simp only:)
moreover
- have "?P s \<Longrightarrow> ?app s" by (unfold app_def) (clarsimp)
+ have "?P s \<Longrightarrow> ?app s" by (clarsimp simp add: min_max.inf_absorb2)
ultimately
show ?thesis by (rule iffI)
qed
--- a/src/HOL/MicroJava/BV/LBVSpec.thy Mon Sep 21 16:11:36 2009 +0200
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy Tue Sep 22 15:36:55 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/MicroJava/BV/LBVSpec.thy
- ID: $Id$
Author: Gerwin Klein
Copyright 1999 Technische Universitaet Muenchen
*)
@@ -293,7 +292,7 @@
shows "wtl (take (pc+1) is) c 0 s = wtc c pc (wtl (take pc is) c 0 s)"
proof -
from suc have "take (pc+1) is=(take pc is)@[is!pc]" by (simp add: take_Suc)
- with suc wtl show ?thesis by (simp)
+ with suc wtl show ?thesis by (simp add: min_max.inf_absorb2)
qed
lemma (in lbv) wtl_all:
@@ -308,7 +307,7 @@
with all have take: "?wtl (take pc is@i#r) \<noteq> \<top>" by simp
from pc have "is!pc = drop pc is ! 0" by simp
with Cons have "is!pc = i" by simp
- with take pc show ?thesis by (auto)
+ with take pc show ?thesis by (auto simp add: min_max.inf_absorb2)
qed
section "preserves-type"
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Mon Sep 21 16:11:36 2009 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Tue Sep 22 15:36:55 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/MicroJava/Comp/CorrCompTp.thy
- ID: $Id$
Author: Martin Strecker
*)
@@ -1058,7 +1057,7 @@
lemma bc_mt_corresp_New: "\<lbrakk>is_class cG cname \<rbrakk>
\<Longrightarrow> bc_mt_corresp [New cname] (pushST [Class cname]) (ST, LT) cG rT mxr (Suc 0)"
apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
- max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
+ max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
apply (intro strip)
apply (rule conjI)
apply (rule check_type_mono, assumption, simp)
@@ -1069,7 +1068,7 @@
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: check_type_simps)
+ apply (simp add: check_type_simps min_max.sup_absorb1)
apply clarify
apply (rule_tac x="(length ST)" in exI)
apply simp+
@@ -1092,7 +1091,7 @@
\<Longrightarrow> bc_mt_corresp [LitPush val] (pushST [T]) sttp cG rT mxr (Suc 0)"
apply (subgoal_tac "\<exists> ST LT. sttp= (ST, LT)", (erule exE)+)
apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
- max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
+ max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
apply (intro strip)
apply (rule conjI)
apply (rule check_type_mono, assumption, simp)
@@ -1111,7 +1110,7 @@
\<Longrightarrow> bc_mt_corresp [LitPush val] (pushST [T']) sttp cG rT mxr (Suc 0)"
apply (subgoal_tac "\<exists> ST LT. sttp= (ST, LT)", (erule exE)+)
apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
- max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
+ max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
apply (intro strip)
apply (rule conjI)
apply (rule check_type_mono, assumption, simp)
@@ -1127,7 +1126,7 @@
\<Longrightarrow> bc_mt_corresp [Load i]
(\<lambda>(ST, LT). pushST [ok_val (LT ! i)] (ST, LT)) (ST, LT) cG rT mxr (Suc 0)"
apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
- max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
+ max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
apply (intro strip)
apply (rule conjI)
apply (rule check_type_mono, assumption, simp)
@@ -1148,10 +1147,10 @@
lemma bc_mt_corresp_Store_init: "\<lbrakk> i < length LT \<rbrakk>
\<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: max_ssize_def max_of_list_def)
apply (simp add: ssize_sto_def)
apply (intro strip)
-apply (simp add: check_type_simps)
+apply (simp add: check_type_simps min_max.sup_absorb1)
apply clarify
apply (rule conjI)
apply (rule_tac x="(length ST)" in exI)
@@ -1159,14 +1158,13 @@
done
-
lemma bc_mt_corresp_Store: "\<lbrakk> i < length LT; cG \<turnstile> LT[i := OK T] <=l LT \<rbrakk>
\<Longrightarrow> bc_mt_corresp [Store i] (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: sup_state_conv)
apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
apply (intro strip)
-apply (simp add: check_type_simps)
+apply (simp add: check_type_simps min_max.sup_absorb1)
apply clarify
apply (rule_tac x="(length ST)" in exI)
apply simp+
@@ -1176,7 +1174,7 @@
lemma bc_mt_corresp_Dup: "
bc_mt_corresp [Dup] dupST (T # ST, LT) cG rT mxr (Suc 0)"
apply (simp add: bc_mt_corresp_def dupST_def wt_instr_altern_def
- max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
+ max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
apply (intro strip)
apply (rule conjI)
apply (rule check_type_mono, assumption, simp)
@@ -1189,7 +1187,7 @@
lemma bc_mt_corresp_Dup_x1: "
bc_mt_corresp [Dup_x1] dup_x1ST (T1 # T2 # ST, LT) cG rT mxr (Suc 0)"
apply (simp add: bc_mt_corresp_def dup_x1ST_def wt_instr_altern_def
- max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
+ max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
apply (intro strip)
apply (rule conjI)
apply (rule check_type_mono, assumption, simp)
@@ -1206,7 +1204,7 @@
(PrimT Integer # PrimT Integer # ST, LT) cG rT mxr (Suc 0)"
apply (simp add: bc_mt_corresp_def replST_def wt_instr_altern_def eff_def norm_eff_def)
apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
- apply (simp add: check_type_simps)
+ apply (simp add: check_type_simps min_max.sup_absorb1)
apply clarify
apply (rule_tac x="Suc (length ST)" in exI)
apply simp+
@@ -1249,7 +1247,7 @@
apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
apply (intro strip)
-apply (simp add: check_type_simps)
+apply (simp add: check_type_simps min_max.sup_absorb1)
apply clarify
apply (rule_tac x="Suc (length ST)" in exI)
apply simp+
--- a/src/HOL/OrderedGroup.thy Mon Sep 21 16:11:36 2009 +0200
+++ b/src/HOL/OrderedGroup.thy Tue Sep 22 15:36:55 2009 +0200
@@ -1075,17 +1075,16 @@
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 sup_aci)
-
+ by (simp add: pprt_def sup_aci sup_absorb1)
lemma nprt_eq_id [simp, noatp]: "x \<le> 0 \<Longrightarrow> nprt x = x"
-by (simp add: nprt_def inf_aci)
+ by (simp add: nprt_def inf_aci inf_absorb1)
lemma pprt_eq_0 [simp, noatp]: "x \<le> 0 \<Longrightarrow> pprt x = 0"
-by (simp add: pprt_def sup_aci)
+ by (simp add: pprt_def sup_aci sup_absorb2)
lemma nprt_eq_0 [simp, noatp]: "0 \<le> x \<Longrightarrow> nprt x = 0"
-by (simp add: nprt_def inf_aci)
+ by (simp add: nprt_def inf_aci inf_absorb2)
lemma sup_0_imp_0: "sup a (- a) = 0 \<Longrightarrow> a = 0"
proof -
@@ -1119,7 +1118,7 @@
"0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
proof
assume "0 <= a + a"
- hence a:"inf (a+a) 0 = 0" by (simp add: inf_commute)
+ hence a:"inf (a+a) 0 = 0" by (simp add: inf_commute inf_absorb1)
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)
@@ -1135,7 +1134,7 @@
assume assm: "a + a = 0"
then have "a + a + - a = - a" by simp
then have "a + (a + - a) = - a" by (simp only: add_assoc)
- then have a: "- a = a" by simp (*FIXME tune proof*)
+ then have a: "- a = a" by simp
show "a = 0" apply (rule antisym)
apply (unfold neg_le_iff_le [symmetric, of a])
unfolding a apply simp
@@ -1275,7 +1274,7 @@
proof -
note add_le_cancel_right [of a a "- a", symmetric, simplified]
moreover note add_le_cancel_right [of "-a" a a, symmetric, simplified]
- then show ?thesis by (auto simp: sup_max)
+ then show ?thesis by (auto simp: sup_max min_max.sup_absorb1 min_max.sup_absorb2)
qed
lemma abs_if_lattice:
--- a/src/HOL/UNITY/Simple/Common.thy Mon Sep 21 16:11:36 2009 +0200
+++ b/src/HOL/UNITY/Simple/Common.thy Tue Sep 22 15:36:55 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/UNITY/Common
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
@@ -10,7 +9,9 @@
From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1.
*)
-theory Common imports "../UNITY_Main" begin
+theory Common
+imports "../UNITY_Main"
+begin
consts
ftime :: "nat=>nat"
@@ -65,7 +66,7 @@
lemma "mk_total_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}, UNIV)
\<in> {m} co (maxfg m)"
apply (simp add: mk_total_program_def)
-apply (simp add: constrains_def maxfg_def gasc)
+apply (simp add: constrains_def maxfg_def gasc min_max.sup_absorb2)
done
(*This one is t := t+1 if t <max (ftime t) (gtime t) *)
@@ -73,7 +74,7 @@
(UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }, UNIV)
\<in> {m} co (maxfg m)"
apply (simp add: mk_total_program_def)
-apply (simp add: constrains_def maxfg_def gasc)
+apply (simp add: constrains_def maxfg_def gasc min_max.sup_absorb2)
done
--- a/src/HOL/Word/BinBoolList.thy Mon Sep 21 16:11:36 2009 +0200
+++ b/src/HOL/Word/BinBoolList.thy Tue Sep 22 15:36:55 2009 +0200
@@ -919,7 +919,7 @@
apply (drule spec)
apply (erule trans)
apply (drule_tac x = "bin_cat y n a" in spec)
- apply (simp add : bin_cat_assoc_sym)
+ apply (simp add : bin_cat_assoc_sym min_max.inf_absorb2)
done
lemma bin_rcat_bl:
--- a/src/HOL/Word/BinGeneral.thy Mon Sep 21 16:11:36 2009 +0200
+++ b/src/HOL/Word/BinGeneral.thy Tue Sep 22 15:36:55 2009 +0200
@@ -508,7 +508,7 @@
lemma sbintrunc_sbintrunc_min [simp]:
"sbintrunc m (sbintrunc n w) = sbintrunc (min m n) w"
apply (rule bin_eqI)
- apply (auto simp: nth_sbintr)
+ apply (auto simp: nth_sbintr min_max.inf_absorb1 min_max.inf_absorb2)
done
lemmas bintrunc_Pls =
--- a/src/HOL/Word/WordDefinition.thy Mon Sep 21 16:11:36 2009 +0200
+++ b/src/HOL/Word/WordDefinition.thy Tue Sep 22 15:36:55 2009 +0200
@@ -381,14 +381,14 @@
apply (unfold word_size)
apply (subst word_ubin.norm_Rep [symmetric])
apply (simp only: bintrunc_bintrunc_min word_size)
- apply simp
+ apply (simp add: min_max.inf_absorb2)
done
lemma wi_bintr':
"wb = word_of_int bin ==> n >= size wb ==>
word_of_int (bintrunc n bin) = wb"
unfolding word_size
- by (clarsimp simp add : word_ubin.norm_eq_iff [symmetric])
+ by (clarsimp simp add: word_ubin.norm_eq_iff [symmetric] min_max.inf_absorb1)
lemmas bintr_uint = bintr_uint' [unfolded word_size]
lemmas wi_bintr = wi_bintr' [unfolded word_size]
--- a/src/HOL/Word/WordShift.thy Mon Sep 21 16:11:36 2009 +0200
+++ b/src/HOL/Word/WordShift.thy Tue Sep 22 15:36:55 2009 +0200
@@ -1017,8 +1017,8 @@
(word_cat (word_of_int w :: 'b word) (b :: 'c word) :: 'a word) =
word_of_int (bin_cat w (size b) (uint b))"
apply (unfold word_cat_def word_size)
- apply (clarsimp simp add : word_ubin.norm_eq_iff [symmetric]
- word_ubin.eq_norm bintr_cat)
+ apply (clarsimp simp add: word_ubin.norm_eq_iff [symmetric]
+ word_ubin.eq_norm bintr_cat min_max.inf_absorb1)
done
lemma word_cat_split_alt: