--- 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)"
--- 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)"
--- 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
--- 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*)