--- a/src/HOL/MicroJava/BV/Semilat.thy Thu Mar 28 16:28:12 2002 +0100
+++ b/src/HOL/MicroJava/BV/Semilat.thy Tue Apr 02 13:47:01 2002 +0200
@@ -61,8 +61,13 @@
"is_lub r x y u == is_ub r x y u & (!z. is_ub r x y z \<longrightarrow> (u,z):r)"
some_lub :: "('a*'a)set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
-"some_lub r x y == SOME z. is_lub r x y z"
+"some_lub r x y == SOME z. is_lub r x y z";
+locale semilat =
+ fixes A :: "'a set"
+ and r :: "'a ord"
+ and f :: "'a binop"
+ assumes semilat: "semilat(A,r,f)"
lemma order_refl [simp, intro]:
"order r \<Longrightarrow> x <=_r x";
@@ -71,7 +76,7 @@
lemma order_antisym:
"\<lbrakk> order r; x <=_r y; y <=_r x \<rbrakk> \<Longrightarrow> x = y"
apply (unfold order_def)
-apply (simp (no_asm_simp))
+apply (simp (no_asm_simp))
done
lemma order_trans:
@@ -109,48 +114,44 @@
apply (rule refl [THEN eq_reflection])
done
-lemma semilatDorderI [simp, intro]:
- "semilat(A,r,f) \<Longrightarrow> order r"
- by (simp add: semilat_Def)
+lemma (in semilat) orderI [simp, intro]:
+ "order r"
+ by (insert semilat) (simp add: semilat_Def)
+
+lemma (in semilat) closedI [simp, intro]:
+ "closed A f"
+ by (insert semilat) (simp add: semilat_Def)
+
+lemma (in semilat) ub1 [simp]:
+ "\<lbrakk> x:A; y:A \<rbrakk> \<Longrightarrow> x <=_r x +_f y"
+ by (insert semilat) (unfold semilat_Def, simp)
+
+lemma (in semilat) ub2 [simp]:
+ "\<lbrakk> x:A; y:A \<rbrakk> \<Longrightarrow> y <=_r x +_f y"
+ by (insert semilat) (unfold semilat_Def, simp)
-lemma semilatDclosedI [simp, intro]:
- "semilat(A,r,f) \<Longrightarrow> closed A f"
-apply (unfold semilat_Def)
+lemma (in semilat) lub [simp]:
+ "\<lbrakk> x <=_r z; y <=_r z; x:A; y:A; z:A \<rbrakk> \<Longrightarrow> x +_f y <=_r z";
+ by (insert semilat) (unfold semilat_Def, simp)
+
+
+lemma (in semilat) plus_le_conv [simp]:
+ "\<lbrakk> x:A; y:A; z:A \<rbrakk> \<Longrightarrow> (x +_f y <=_r z) = (x <=_r z & y <=_r z)"
+apply (blast intro: ub1 ub2 lub order_trans)
+done
+
+lemma (in semilat) le_iff_plus_unchanged:
+ "\<lbrakk> x:A; y:A \<rbrakk> \<Longrightarrow> (x <=_r y) = (x +_f y = y)"
+apply (rule iffI)
+ apply (blast intro: order_antisym lub order_refl ub2);
+apply (erule subst)
apply simp
done
-lemma semilat_ub1 [simp]:
- "\<lbrakk> semilat(A,r,f); x:A; y:A \<rbrakk> \<Longrightarrow> x <=_r x +_f y"
- by (unfold semilat_Def, simp)
-
-lemma semilat_ub2 [simp]:
- "\<lbrakk> semilat(A,r,f); x:A; y:A \<rbrakk> \<Longrightarrow> y <=_r x +_f y"
- by (unfold semilat_Def, simp)
-
-lemma semilat_lub [simp]:
- "\<lbrakk> x <=_r z; y <=_r z; semilat(A,r,f); x:A; y:A; z:A \<rbrakk> \<Longrightarrow> x +_f y <=_r z";
- by (unfold semilat_Def, simp)
-
-
-lemma plus_le_conv [simp]:
- "\<lbrakk> x:A; y:A; z:A; semilat(A,r,f) \<rbrakk>
- \<Longrightarrow> (x +_f y <=_r z) = (x <=_r z & y <=_r z)"
-apply (unfold semilat_Def)
-apply (blast intro: semilat_ub1 semilat_ub2 semilat_lub order_trans)
-done
-
-lemma le_iff_plus_unchanged:
- "\<lbrakk> x:A; y:A; semilat(A,r,f) \<rbrakk> \<Longrightarrow> (x <=_r y) = (x +_f y = y)"
+lemma (in semilat) le_iff_plus_unchanged2:
+ "\<lbrakk> x:A; y:A \<rbrakk> \<Longrightarrow> (x <=_r y) = (y +_f x = y)"
apply (rule iffI)
- apply (intro semilatDorderI order_antisym semilat_lub order_refl semilat_ub2, assumption+)
-apply (erule subst)
-apply simp
-done
-
-lemma le_iff_plus_unchanged2:
- "\<lbrakk> x:A; y:A; semilat(A,r,f) \<rbrakk> \<Longrightarrow> (x <=_r y) = (y +_f x = y)"
-apply (rule iffI)
- apply (intro semilatDorderI order_antisym semilat_lub order_refl semilat_ub1, assumption+)
+ apply (blast intro: order_antisym lub order_refl ub1)
apply (erule subst)
apply simp
done
@@ -160,23 +161,22 @@
"\<lbrakk> closed A f; x:A; y:A \<rbrakk> \<Longrightarrow> x +_f y : A"
apply (unfold closed_def)
apply blast
-done
+done
lemma closed_UNIV [simp]: "closed UNIV f"
by (simp add: closed_def)
-lemma plus_assoc [simp]:
- assumes semi: "semilat (A,r,f)"
+lemma (in semilat) plus_assoc [simp]:
assumes a: "a \<in> A" and b: "b \<in> A" and c: "c \<in> A"
shows "a +_f (b +_f c) = a +_f b +_f c"
proof -
have order: "order r" ..
note order_trans [OF order,trans]
- note closedD [OF semilatDclosedI [OF semi], intro]
- note semilat_ub1 [OF semi, intro]
- note semilat_ub2 [OF semi, intro]
- note semilat_lub [OF _ _ semi, intro]
+ note closedD [OF closedI, intro]
+ note ub1 [intro]
+ note ub2 [intro]
+ note lub [intro]
from a b have ab: "a +_f b \<in> A" ..
from this c have abc: "(a +_f b) +_f c \<in> A" ..
@@ -186,7 +186,7 @@
from order show ?thesis
proof (rule order_antisym)
show "a +_f (b +_f c) <=_r (a +_f b) +_f c"
- proof -
+ proof -
from a b have "a <=_r a +_f b" ..
also from ab c have "\<dots> <=_r \<dots> +_f c" ..
finally have "a<": "a <=_r (a +_f b) +_f c" .
@@ -212,28 +212,24 @@
qed
qed
-lemma plus_com_lemma:
- "\<lbrakk>semilat (A,r,f); a \<in> A; b \<in> A\<rbrakk> \<Longrightarrow> a +_f b <=_r b +_f a"
+lemma (in semilat) plus_com_lemma:
+ "\<lbrakk>a \<in> A; b \<in> A\<rbrakk> \<Longrightarrow> a +_f b <=_r b +_f a"
proof -
- assume semi: "semilat (A,r,f)" and a: "a \<in> A" and b: "b \<in> A"
- from semi b a have "a <=_r b +_f a" by (rule semilat_ub2)
+ assume a: "a \<in> A" and b: "b \<in> A"
+ from b a have "a <=_r b +_f a" by (rule ub2)
moreover
- from semi b a have "b <=_r b +_f a" by (rule semilat_ub1)
+ from b a have "b <=_r b +_f a" by (rule ub1)
moreover
- note semi a b
+ note a b
moreover
- from semi b a have "b +_f a \<in> A" by (rule closedD [OF semilatDclosedI])
+ from b a have "b +_f a \<in> A" by (rule closedD [OF closedI])
ultimately
- show ?thesis by (rule semilat_lub)
+ show ?thesis by (rule lub)
qed
-lemma plus_commutative:
- "\<lbrakk>semilat (A,r,f); a \<in> A; b \<in> A\<rbrakk> \<Longrightarrow> a +_f b = b +_f a"
- apply (frule semilatDorderI)
- apply (erule order_antisym)
- apply (rule plus_com_lemma, assumption+)
- apply (rule plus_com_lemma, assumption+)
- done
+lemma (in semilat) plus_commutative:
+ "\<lbrakk>a \<in> A; b \<in> A\<rbrakk> \<Longrightarrow> a +_f b = b +_f a"
+by(blast intro: order_antisym plus_com_lemma)
lemma is_lubD:
"is_lub r x y u \<Longrightarrow> is_ub r x y u & (!z. is_ub r x y z \<longrightarrow> (u,z):r)"