# HG changeset patch
# User huffman
# Date 1289427647 28800
# Node ID ee9c8d36318ee1f737c18e99ec3cb88aa63c0f76
# Parent  827983e714210a7f8150fd70adc87bf07991a121
add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas

diff -r 827983e71421 -r ee9c8d36318e src/HOLCF/Adm.thy
--- a/src/HOLCF/Adm.thy	Wed Nov 10 13:22:39 2010 -0800
+++ b/src/HOLCF/Adm.thy	Wed Nov 10 14:20:47 2010 -0800
@@ -146,7 +146,7 @@
 
 lemma compact_below_lub_iff:
   "\<lbrakk>compact x; chain Y\<rbrakk> \<Longrightarrow> x \<sqsubseteq> (\<Squnion>i. Y i) \<longleftrightarrow> (\<exists>i. x \<sqsubseteq> Y i)"
-by (fast intro: compactD2 elim: below_trans is_ub_thelub)
+by (fast intro: compactD2 elim: below_lub)
 
 lemma compact_chfin [simp]: "compact (x::'a::chfin)"
 by (rule compactI [OF adm_chfin])
diff -r 827983e71421 -r ee9c8d36318e src/HOLCF/Completion.thy
--- a/src/HOLCF/Completion.thy	Wed Nov 10 13:22:39 2010 -0800
+++ b/src/HOLCF/Completion.thy	Wed Nov 10 14:20:47 2010 -0800
@@ -351,11 +351,9 @@
     apply (rule ub_imageI, rename_tac a)
     apply (clarsimp simp add: rep_x)
     apply (drule f_mono)
-    apply (erule below_trans)
-    apply (rule is_ub_thelub [OF chain])
-    apply (rule is_lub_thelub [OF chain])
-    apply (rule ub_rangeI)
-    apply (drule_tac x="Y i" in ub_imageD)
+    apply (erule below_lub [OF chain])
+    apply (rule lub_below [OF chain])
+    apply (drule_tac x="Y n" in ub_imageD)
     apply (simp add: rep_x, fast intro: r_refl)
     apply assumption
     done
diff -r 827983e71421 -r ee9c8d36318e src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Wed Nov 10 13:22:39 2010 -0800
+++ b/src/HOLCF/Fix.thy	Wed Nov 10 14:20:47 2010 -0800
@@ -82,9 +82,8 @@
 
 lemma fix_least_below: "F\<cdot>x \<sqsubseteq> x \<Longrightarrow> fix\<cdot>F \<sqsubseteq> x"
 apply (simp add: fix_def2)
-apply (rule is_lub_thelub)
+apply (rule lub_below)
 apply (rule chain_iterate)
-apply (rule ub_rangeI)
 apply (induct_tac i)
 apply simp
 apply simp
diff -r 827983e71421 -r ee9c8d36318e src/HOLCF/Pcpo.thy
--- a/src/HOLCF/Pcpo.thy	Wed Nov 10 13:22:39 2010 -0800
+++ b/src/HOLCF/Pcpo.thy	Wed Nov 10 14:20:47 2010 -0800
@@ -36,11 +36,16 @@
 lemma lub_below_iff: "chain S \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x \<longleftrightarrow> (\<forall>i. S i \<sqsubseteq> x)"
   by (simp add: is_lub_below_iff [OF cpo_lubI] is_ub_def)
 
+lemma lub_below: "\<lbrakk>chain S; \<And>i. S i \<sqsubseteq> x\<rbrakk> \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x"
+  by (simp add: lub_below_iff)
+
+lemma below_lub: "\<lbrakk>chain S; x \<sqsubseteq> S i\<rbrakk> \<Longrightarrow> x \<sqsubseteq> (\<Squnion>i. S i)"
+  by (erule below_trans, erule is_ub_thelub)
+
 lemma lub_range_mono:
   "\<lbrakk>range X \<subseteq> range Y; chain Y; chain X\<rbrakk>
     \<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)"
-apply (erule is_lub_thelub)
-apply (rule ub_rangeI)
+apply (erule lub_below)
 apply (subgoal_tac "\<exists>j. X i = Y j")
 apply  clarsimp
 apply  (erule is_ub_thelub)
@@ -54,14 +59,12 @@
 apply    fast
 apply   assumption
 apply (erule chain_shift)
-apply (rule is_lub_thelub)
+apply (rule lub_below)
 apply assumption
-apply (rule ub_rangeI)
-apply (rule_tac y="Y (i + j)" in below_trans)
+apply (rule_tac i="i" in below_lub)
+apply (erule chain_shift)
 apply (erule chain_mono)
 apply (rule le_add1)
-apply (rule is_ub_thelub)
-apply (erule chain_shift)
 done
 
 lemma maxinch_is_thelub:
@@ -80,52 +83,14 @@
 lemma lub_mono:
   "\<lbrakk>chain X; chain Y; \<And>i. X i \<sqsubseteq> Y i\<rbrakk> 
     \<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)"
-apply (erule is_lub_thelub)
-apply (rule ub_rangeI)
-apply (rule below_trans)
-apply (erule meta_spec)
-apply (erule is_ub_thelub)
-done
+by (fast elim: lub_below below_lub)
 
 text {* the = relation between two chains is preserved by their lubs *}
 
-lemma lub_equal:
-  "\<lbrakk>chain X; chain Y; \<forall>k. X k = Y k\<rbrakk>
-    \<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)"
-  by (simp only: fun_eq_iff [symmetric])
-
 lemma lub_eq:
   "(\<And>i. X i = Y i) \<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)"
   by simp
 
-text {* more results about mono and = of lubs of chains *}
-
-lemma lub_mono2:
-  "\<lbrakk>\<exists>j. \<forall>i>j. X i = Y i; chain X; chain Y\<rbrakk>
-    \<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)"
-apply (erule exE)
-apply (subgoal_tac "(\<Squnion>i. X (i + Suc j)) \<sqsubseteq> (\<Squnion>i. Y (i + Suc j))")
-apply (thin_tac "\<forall>i>j. X i = Y i")
-apply (simp only: lub_range_shift)
-apply simp
-done
-
-lemma lub_equal2:
-  "\<lbrakk>\<exists>j. \<forall>i>j. X i = Y i; chain X; chain Y\<rbrakk>
-    \<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)"
-  by (blast intro: below_antisym lub_mono2 sym)
-
-lemma lub_mono3:
-  "\<lbrakk>chain Y; chain X; \<forall>i. \<exists>j. Y i \<sqsubseteq> X j\<rbrakk>
-    \<Longrightarrow> (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. X i)"
-apply (erule is_lub_thelub)
-apply (rule ub_rangeI)
-apply (erule allE)
-apply (erule exE)
-apply (erule below_trans)
-apply (erule is_ub_thelub)
-done
-
 lemma ch2ch_lub:
   assumes 1: "\<And>j. chain (\<lambda>i. Y i j)"
   assumes 2: "\<And>i. chain (\<lambda>j. Y i j)"
@@ -149,10 +114,9 @@
   have 4: "chain (\<lambda>i. \<Squnion>j. Y i j)"
     by (rule ch2ch_lub [OF 1 2])
   show "(\<Squnion>i. \<Squnion>j. Y i j) \<sqsubseteq> (\<Squnion>i. Y i i)"
-    apply (rule is_lub_thelub [OF 4])
-    apply (rule ub_rangeI)
-    apply (rule lub_mono3 [rule_format, OF 2 3])
-    apply (rule exI)
+    apply (rule lub_below [OF 4])
+    apply (rule lub_below [OF 2])
+    apply (rule below_lub [OF 3])
     apply (rule below_trans)
     apply (rule chain_mono [OF 1 le_maxI1])
     apply (rule chain_mono [OF 2 le_maxI2])
diff -r 827983e71421 -r ee9c8d36318e src/HOLCF/Universal.thy
--- a/src/HOLCF/Universal.thy	Wed Nov 10 13:22:39 2010 -0800
+++ b/src/HOLCF/Universal.thy	Wed Nov 10 14:20:47 2010 -0800
@@ -851,7 +851,7 @@
     unfolding approximants_def
     apply safe
     apply (simp add: compactD2 [OF compact_Rep_compact_basis Y])
-    apply (erule below_trans, rule is_ub_thelub [OF Y])
+    apply (erule below_lub [OF Y])
     done
 next
   fix a :: "'a compact_basis"
@@ -990,14 +990,12 @@
 lemma lub_udom_approx [simp]: "(\<Squnion>i. udom_approx i) = ID"
 apply (rule cfun_eqI, simp add: contlub_cfun_fun)
 apply (rule below_antisym)
-apply (rule is_lub_thelub)
+apply (rule lub_below)
 apply (simp)
-apply (rule ub_rangeI)
 apply (rule udom_approx.below)
 apply (rule_tac x=x in udom.principal_induct)
 apply (simp add: lub_distribs)
-apply (rule rev_below_trans)
-apply (rule_tac x=a in is_ub_thelub)
+apply (rule_tac i=a in below_lub)
 apply simp
 apply (simp add: udom_approx_principal)
 apply (simp add: ubasis_until_same ubasis_le_refl)