--- a/src/HOL/MicroJava/BV/Semilat.thy Wed Apr 03 10:21:13 2002 +0200
+++ b/src/HOL/MicroJava/BV/Semilat.thy Thu Apr 04 16:47:44 2002 +0200
@@ -122,28 +122,52 @@
"closed A f"
by (insert semilat) (simp add: semilat_Def)
-lemma (in semilat) ub1 [simp]:
+lemma closedD:
+ "\<lbrakk> closed A f; x:A; y:A \<rbrakk> \<Longrightarrow> x +_f y : A"
+ by (unfold closed_def) blast
+
+lemma closed_UNIV [simp]: "closed UNIV f"
+ by (simp add: closed_def)
+
+
+lemma (in semilat) closed_f [simp, intro]:
+ "\<lbrakk>x:A; y:A\<rbrakk> \<Longrightarrow> x +_f y : A"
+ by (simp add: closedD [OF closedI])
+
+lemma (in semilat) refl_r [intro, simp]:
+ "x <=_r x"
+ by simp
+
+lemma (in semilat) antisym_r [intro?]:
+ "\<lbrakk> x <=_r y; y <=_r x \<rbrakk> \<Longrightarrow> x = y"
+ by (rule order_antisym) auto
+
+lemma (in semilat) trans_r [trans, intro?]:
+ "\<lbrakk>x <=_r y; y <=_r z\<rbrakk> \<Longrightarrow> x <=_r z"
+ by (auto intro: order_trans)
+
+
+lemma (in semilat) ub1 [simp, intro?]:
"\<lbrakk> x:A; y:A \<rbrakk> \<Longrightarrow> x <=_r x +_f y"
by (insert semilat) (unfold semilat_Def, simp)
-lemma (in semilat) ub2 [simp]:
+lemma (in semilat) ub2 [simp, intro?]:
"\<lbrakk> x:A; y:A \<rbrakk> \<Longrightarrow> y <=_r x +_f y"
by (insert semilat) (unfold semilat_Def, simp)
-lemma (in semilat) lub [simp]:
+lemma (in semilat) lub [simp, intro?]:
"\<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
+ by (blast intro: ub1 ub2 lub order_trans)
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 (blast intro: antisym_r refl_r lub ub2)
apply (erule subst)
apply simp
done
@@ -157,34 +181,17 @@
done
-lemma closedD:
- "\<lbrakk> closed A f; x:A; y:A \<rbrakk> \<Longrightarrow> x +_f y : A"
-apply (unfold closed_def)
-apply blast
-done
-
-lemma closed_UNIV [simp]: "closed UNIV f"
- by (simp add: closed_def)
-
-
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 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" ..
from b c have bc: "b +_f c \<in> A" ..
from a this have abc': "a +_f (b +_f c) \<in> A" ..
- from order show ?thesis
- proof (rule order_antisym)
+ show ?thesis
+ proof
show "a +_f (b +_f c) <=_r (a +_f b) +_f c"
proof -
from a b have "a <=_r a +_f b" ..
@@ -216,15 +223,11 @@
"\<lbrakk>a \<in> A; b \<in> A\<rbrakk> \<Longrightarrow> a +_f b <=_r b +_f a"
proof -
assume a: "a \<in> A" and b: "b \<in> A"
- from b a have "a <=_r b +_f a" by (rule ub2)
- moreover
- from b a have "b <=_r b +_f a" by (rule ub1)
- moreover
- note a b
- moreover
- from b a have "b +_f a \<in> A" by (rule closedD [OF closedI])
- ultimately
- show ?thesis by (rule lub)
+ from b a have "a <=_r b +_f a" ..
+ moreover from b a have "b <=_r b +_f a" ..
+ moreover note a b
+ moreover from b a have "b +_f a \<in> A" ..
+ ultimately show ?thesis ..
qed
lemma (in semilat) plus_commutative:
--- a/src/HOL/MicroJava/BV/SemilatAlg.thy Wed Apr 03 10:21:13 2002 +0200
+++ b/src/HOL/MicroJava/BV/SemilatAlg.thy Thu Apr 04 16:47:44 2002 +0200
@@ -70,8 +70,8 @@
assume y: "y \<in> A" and xs: "set (x#xs) \<subseteq> A"
assume IH: "\<And>y. \<lbrakk> set xs \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> xs ++_f y \<in> A"
from xs obtain x: "x \<in> A" and "set xs \<subseteq> A" by simp
- from semilat x y have "(x +_f y) \<in> A" by (simp add: closedD)
- with semilat xs have "xs ++_f (x +_f y) \<in> A" by - (rule IH)
+ from x y have "(x +_f y) \<in> A" ..
+ with xs have "xs ++_f (x +_f y) \<in> A" by - (rule IH)
thus "(x#xs) ++_f y \<in> A" by simp
qed
@@ -87,10 +87,8 @@
assume "\<And>y. \<lbrakk>set l \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> y <=_r l ++_f y"
hence IH: "\<And>y. y \<in> A \<Longrightarrow> y <=_r l ++_f y" .
- have "order r" .. note order_trans [OF this, trans]
-
- from a y have "y <=_r a +_f y" by (rule ub2)
- also from a y have "a +_f y \<in> A" by (simp add: closedD)
+ from a y have "y <=_r a +_f y" ..
+ also from a y have "a +_f y \<in> A" ..
hence "(a +_f y) <=_r l ++_f (a +_f y)" by (rule IH)
finally have "y <=_r l ++_f (a +_f y)" .
thus "y <=_r (a#l) ++_f y" by simp
@@ -103,7 +101,6 @@
show "\<And>y. x \<in> set [] \<Longrightarrow> x <=_r [] ++_f y" by simp
fix y s ls
- have "order r" .. note order_trans [OF this, trans]
assume "set (s#ls) \<subseteq> A"
then obtain s: "s \<in> A" and ls: "set ls \<subseteq> A" by simp
assume y: "y \<in> A"
@@ -116,8 +113,8 @@
then obtain xls: "x = s \<or> x \<in> set ls" by simp
moreover {
assume xs: "x = s"
- from s y have "s <=_r s +_f y" by (rule ub1)
- also from s y have "s +_f y \<in> A" by (simp add: closedD)
+ from s y have "s <=_r s +_f y" ..
+ also from s y have "s +_f y \<in> A" ..
with ls have "(s +_f y) <=_r ls ++_f (s +_f y)" by (rule pp_ub2)
finally have "s <=_r ls ++_f (s +_f y)" .
with xs have "x <=_r ls ++_f (s +_f y)" by simp
@@ -125,7 +122,7 @@
moreover {
assume "x \<in> set ls"
hence "\<And>y. y \<in> A \<Longrightarrow> x <=_r ls ++_f y" by (rule IH)
- moreover from s y have "s +_f y \<in> A" by (simp add: closedD)
+ moreover from s y have "s +_f y \<in> A" ..
ultimately have "x <=_r ls ++_f (s +_f y)" .
}
ultimately
@@ -145,14 +142,14 @@
then obtain l: "l \<in> A" and ls: "set ls \<subseteq> A" by auto
assume "\<forall>x \<in> set (l#ls). x <=_r z"
then obtain "l <=_r z" and lsz: "\<forall>x \<in> set ls. x <=_r z" by auto
- assume "y <=_r z" have "l +_f y <=_r z" by (rule lub)
+ assume "y <=_r z" have "l +_f y <=_r z" ..
moreover
- from l y have "l +_f y \<in> A" by (fast intro: closedD)
+ from l y have "l +_f y \<in> A" ..
moreover
assume "\<And>y. y \<in> A \<Longrightarrow> set ls \<subseteq> A \<Longrightarrow> \<forall>x \<in> set ls. x <=_r z \<Longrightarrow> y <=_r z
\<Longrightarrow> ls ++_f y <=_r z"
ultimately
- have "ls ++_f (l +_f y) <=_r z" by - (insert ls lsz)
+ have "ls ++_f (l +_f y) <=_r z" using ls lsz by -
thus "(l#ls) ++_f y <=_r z" by simp
qed