# HG changeset patch
# User haftmann
# Date 1387983145 -3600
# Node ID 64ff7f16d5b7ca6845596c2f7502d0ee2801ba3f
# Parent  c1c3341985047b9bffd0a0ca8cb2ce6edb328326
prefer abstract simp rule

diff -r c1c334198504 -r 64ff7f16d5b7 src/HOL/Bali/TypeSafe.thy
--- a/src/HOL/Bali/TypeSafe.thy	Wed Dec 25 10:09:43 2013 +0100
+++ b/src/HOL/Bali/TypeSafe.thy	Wed Dec 25 15:52:25 2013 +0100
@@ -2946,7 +2946,7 @@
           by simp
         from da_e1 s0_s1 True obtain E1' where
           "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e1\<guillemotright> E1'"
-          by - (rule da_weakenE, auto iff del: Un_subset_iff le_sup_iff)
+          by - (rule da_weakenE, auto iff del: Un_subset_iff sup.bounded_iff)
         with conf_s1 wt_e1
         obtain 
           "s2\<Colon>\<preceq>(G, L)"
@@ -2965,7 +2965,7 @@
           by simp
         from da_e2 s0_s1 False obtain E2' where
           "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e2\<guillemotright> E2'"
-          by - (rule da_weakenE, auto iff del: Un_subset_iff le_sup_iff)
+          by - (rule da_weakenE, auto iff del: Un_subset_iff sup.bounded_iff)
         with conf_s1 wt_e2
         obtain 
           "s2\<Colon>\<preceq>(G, L)"
diff -r c1c334198504 -r 64ff7f16d5b7 src/HOL/Hoare_Parallel/RG_Hoare.thy
--- a/src/HOL/Hoare_Parallel/RG_Hoare.thy	Wed Dec 25 10:09:43 2013 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy	Wed Dec 25 15:52:25 2013 +0100
@@ -4,7 +4,7 @@
 
 subsection {* Proof System for Component Programs *}
 
-declare Un_subset_iff [simp del] le_sup_iff [simp del]
+declare Un_subset_iff [simp del] sup.bounded_iff [simp del]
 
 definition stable :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool" where  
   "stable \<equiv> \<lambda>f g. (\<forall>x y. x \<in> f \<longrightarrow> (x, y) \<in> g \<longrightarrow> y \<in> f)" 
diff -r c1c334198504 -r 64ff7f16d5b7 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Wed Dec 25 10:09:43 2013 +0100
+++ b/src/HOL/Lattices.thy	Wed Dec 25 15:52:25 2013 +0100
@@ -98,14 +98,14 @@
   obtains "a \<preceq> b" and "a \<preceq> c"
   using assms by (blast intro: trans cobounded1 cobounded2)
 
-lemma bounded_iff (* [simp] CANDIDATE *):
+lemma bounded_iff [simp]:
   "a \<preceq> b * c \<longleftrightarrow> a \<preceq> b \<and> a \<preceq> c"
   by (blast intro: boundedI elim: boundedE)
 
 lemma strict_boundedE:
   assumes "a \<prec> b * c"
   obtains "a \<prec> b" and "a \<prec> c"
-  using assms by (auto simp add: commute strict_iff_order bounded_iff elim: orderE intro!: that)+
+  using assms by (auto simp add: commute strict_iff_order elim: orderE intro!: that)+
 
 lemma coboundedI1:
   "a \<preceq> c \<Longrightarrow> a * b \<preceq> c"
@@ -128,10 +128,10 @@
   by (blast intro: boundedI coboundedI1 coboundedI2)
 
 lemma absorb1: "a \<preceq> b \<Longrightarrow> a * b = a"
-  by (rule antisym) (auto simp add: bounded_iff refl)
+  by (rule antisym) (auto simp add: refl)
 
 lemma absorb2: "b \<preceq> a \<Longrightarrow> a * b = b"
-  by (rule antisym) (auto simp add: bounded_iff refl)
+  by (rule antisym) (auto simp add: refl)
 
 lemma absorb_iff1: "a \<preceq> b \<longleftrightarrow> a * b = a"
   using order_iff by auto
@@ -210,13 +210,13 @@
 lemma le_infE: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
   by (blast intro: order_trans inf_le1 inf_le2)
 
-lemma le_inf_iff [simp]:
+lemma le_inf_iff:
   "x \<sqsubseteq> y \<sqinter> z \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<sqsubseteq> z"
   by (blast intro: le_infI elim: le_infE)
 
 lemma le_iff_inf:
   "x \<sqsubseteq> y \<longleftrightarrow> x \<sqinter> y = x"
-  by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1])
+  by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1] simp add: le_inf_iff)
 
 lemma inf_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> a \<sqinter> b \<sqsubseteq> c \<sqinter> d"
   by (fast intro: inf_greatest le_infI1 le_infI2)
@@ -247,13 +247,13 @@
   "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
   by (blast intro: order_trans sup_ge1 sup_ge2)
 
-lemma le_sup_iff [simp]:
+lemma le_sup_iff:
   "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
   by (blast intro: le_supI elim: le_supE)
 
 lemma le_iff_sup:
   "x \<sqsubseteq> y \<longleftrightarrow> x \<squnion> y = y"
-  by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1])
+  by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1] simp add: le_sup_iff)
 
 lemma sup_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> a \<squnion> b \<sqsubseteq> c \<squnion> d"
   by (fast intro: sup_least le_supI1 le_supI2)
@@ -275,11 +275,11 @@
 proof
   fix a b c
   show "(a \<sqinter> b) \<sqinter> c = a \<sqinter> (b \<sqinter> c)"
-    by (rule antisym) (auto intro: le_infI1 le_infI2)
+    by (rule antisym) (auto intro: le_infI1 le_infI2 simp add: le_inf_iff)
   show "a \<sqinter> b = b \<sqinter> a"
-    by (rule antisym) auto
+    by (rule antisym) (auto simp add: le_inf_iff)
   show "a \<sqinter> a = a"
-    by (rule antisym) auto
+    by (rule antisym) (auto simp add: le_inf_iff)
 qed
 
 sublocale inf!: semilattice_order inf less_eq less
@@ -320,11 +320,11 @@
 proof
   fix a b c
   show "(a \<squnion> b) \<squnion> c = a \<squnion> (b \<squnion> c)"
-    by (rule antisym) (auto intro: le_supI1 le_supI2)
+    by (rule antisym) (auto intro: le_supI1 le_supI2 simp add: le_sup_iff)
   show "a \<squnion> b = b \<squnion> a"
-    by (rule antisym) auto
+    by (rule antisym) (auto simp add: le_sup_iff)
   show "a \<squnion> a = a"
-    by (rule antisym) auto
+    by (rule antisym) (auto simp add: le_sup_iff)
 qed
 
 sublocale sup!: semilattice_order sup greater_eq greater
diff -r c1c334198504 -r 64ff7f16d5b7 src/HOL/UNITY/Follows.thy
--- a/src/HOL/UNITY/Follows.thy	Wed Dec 25 10:09:43 2013 +0100
+++ b/src/HOL/UNITY/Follows.thy	Wed Dec 25 15:52:25 2013 +0100
@@ -158,7 +158,7 @@
 lemma Follows_Un: 
     "[| F \<in> f' Fols f;  F \<in> g' Fols g |]  
      ==> F \<in> (%s. (f' s) \<union> (g' s)) Fols (%s. (f s) \<union> (g s))"
-apply (simp add: Follows_def Increasing_Un Always_Un del: Un_subset_iff le_sup_iff, auto)
+apply (simp add: Follows_def Increasing_Un Always_Un del: Un_subset_iff sup.bounded_iff, auto)
 apply (rule LeadsTo_Trans)
 apply (blast intro: Follows_Un_lemma)
 (*Weakening is used to exchange Un's arguments*)