# HG changeset patch
# User huffman
# Date 1288825059 25200
# Node ID 61a1519d985f7d095151d41f7ad72fd8cf33f742
# Parent  682d6c4556705bac2ef9a1c19d19b63b779480a1
add lemma eq_imp_below

diff -r 682d6c455670 -r 61a1519d985f src/HOLCF/IOA/meta_theory/CompoTraces.thy
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Wed Nov 03 15:47:46 2010 -0700
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Wed Nov 03 15:57:39 2010 -0700
@@ -260,8 +260,8 @@
 apply auto
 
 (* a: act A; a: act B *)
-apply (frule sym [THEN below_antisym_inverse, THEN conjunct1, THEN divide_Seq])
-apply (frule sym [THEN below_antisym_inverse, THEN conjunct1, THEN divide_Seq])
+apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
+apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
 back
 apply (erule conjE)+
 (* Finite (tw iA x) and Finite (tw iB y) *)
@@ -275,7 +275,7 @@
 apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
 
 (* a: act B; a~: act A *)
-apply (frule sym [THEN below_antisym_inverse, THEN conjunct1, THEN divide_Seq])
+apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
 
 apply (erule conjE)+
 (* Finite (tw iB y) *)
@@ -287,7 +287,7 @@
 apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
 
 (* a~: act B; a: act A *)
-apply (frule sym [THEN below_antisym_inverse, THEN conjunct1, THEN divide_Seq])
+apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
 
 apply (erule conjE)+
 (* Finite (tw iA x) *)
@@ -327,7 +327,7 @@
 apply (erule conjE)+
 apply simp
 (* divide_Seq on s *)
-apply (frule sym [THEN below_antisym_inverse, THEN conjunct1, THEN divide_Seq])
+apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
 apply (erule conjE)+
 (* transform assumption f eB y = f B (s@z) *)
 apply (drule_tac x = "y" and g = "Filter (%a. a:act B) $ (s@@z) " in subst_lemma2)
@@ -373,7 +373,7 @@
 apply (erule conjE)+
 apply simp
 (* divide_Seq on s *)
-apply (frule sym [THEN below_antisym_inverse, THEN conjunct1, THEN divide_Seq])
+apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
 apply (erule conjE)+
 (* transform assumption f eA x = f A (s@z) *)
 apply (drule_tac x = "x" and g = "Filter (%a. a:act A) $ (s@@z) " in subst_lemma2)
@@ -557,7 +557,7 @@
 prefer 2 apply fast
 
 (* bring in divide Seq for s *)
-apply (frule sym [THEN below_antisym_inverse, THEN conjunct1, THEN divide_Seq])
+apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
 apply (erule conjE)+
 
 (* subst divide_Seq in conclusion, but only at the righest occurence *)
@@ -610,7 +610,7 @@
 prefer 2 apply (fast)
 
 (* bring in divide Seq for s *)
-apply (frule sym [THEN below_antisym_inverse, THEN conjunct1, THEN divide_Seq])
+apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
 apply (erule conjE)+
 
 (* subst divide_Seq in conclusion, but only at the righest occurence *)
@@ -628,7 +628,7 @@
 apply (simp add: ext_and_act)
 
 (* divide_Seq for schB2 *)
-apply (frule_tac y = "y2" in sym [THEN below_antisym_inverse, THEN conjunct1, THEN divide_Seq])
+apply (frule_tac y = "y2" in sym [THEN eq_imp_below, THEN divide_Seq])
 apply (erule conjE)+
 (* assumption schA *)
 apply (drule_tac x = "schA" and g = "Filter (%a. a:act A) $rs" in subst_lemma2)
@@ -776,7 +776,7 @@
 prefer 2 apply (fast)
 
 (* bring in divide Seq for s *)
-apply (frule sym [THEN below_antisym_inverse, THEN conjunct1, THEN divide_Seq])
+apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
 apply (erule conjE)+
 
 (* subst divide_Seq in conclusion, but only at the righest occurence *)
@@ -827,7 +827,7 @@
 prefer 2 apply (fast)
 
 (* bring in divide Seq for s *)
-apply (frule sym [THEN below_antisym_inverse, THEN conjunct1, THEN divide_Seq])
+apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
 apply (erule conjE)+
 
 (* subst divide_Seq in conclusion, but only at the righest occurence *)
@@ -845,7 +845,7 @@
 apply (simp add: ext_and_act)
 
 (* divide_Seq for schB2 *)
-apply (frule_tac y = "x2" in sym [THEN below_antisym_inverse, THEN conjunct1, THEN divide_Seq])
+apply (frule_tac y = "x2" in sym [THEN eq_imp_below, THEN divide_Seq])
 apply (erule conjE)+
 (* assumption schA *)
 apply (drule_tac x = "schB" and g = "Filter (%a. a:act B) $rs" in subst_lemma2)
diff -r 682d6c455670 -r 61a1519d985f src/HOLCF/Porder.thy
--- a/src/HOLCF/Porder.thy	Wed Nov 03 15:47:46 2010 -0700
+++ b/src/HOLCF/Porder.thy	Wed Nov 03 15:57:39 2010 -0700
@@ -39,6 +39,9 @@
 lemma minimal2UU[OF allI] : "\<forall>x. uu \<sqsubseteq> x \<Longrightarrow> uu = (THE u. \<forall>y. u \<sqsubseteq> y)"
   by (blast intro: theI2 below_antisym)
 
+lemma eq_imp_below: "x = y \<Longrightarrow> x \<sqsubseteq> y"
+  by simp
+
 text {* the reverse law of anti-symmetry of @{term "op <<"} *}
 (* Is this rule ever useful? *)
 lemma below_antisym_inverse: "x = y \<Longrightarrow> x \<sqsubseteq> y \<and> y \<sqsubseteq> x"