# HG changeset patch
# User huffman
# Date 1288827563 25200
# Node ID 3128c2a54785e383f42a0eac6cb2ac56e3cff691
# Parent  61a1519d985f7d095151d41f7ad72fd8cf33f742
remove some unnecessary lemmas; move monofun_LAM to Cfun.thy

diff -r 61a1519d985f -r 3128c2a54785 src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Wed Nov 03 15:57:39 2010 -0700
+++ b/src/HOLCF/Cfun.thy	Wed Nov 03 16:39:23 2010 -0700
@@ -355,16 +355,13 @@
   "(\<And>y::'a::discrete_cpo. cont (\<lambda>x. f x y)) \<Longrightarrow> cont (\<lambda>x. \<Lambda> y. f x y)"
 by (simp add: cont2cont_LAM)
 
-lemmas cont_lemmas1 =
-  cont_const cont_id cont_Rep_cfun2 cont2cont_APP cont2cont_LAM
-
 subsection {* Miscellaneous *}
 
 text {* Monotonicity of @{term Abs_cfun} *}
 
-lemma semi_monofun_Abs_cfun:
-  "\<lbrakk>cont f; cont g; f \<sqsubseteq> g\<rbrakk> \<Longrightarrow> Abs_cfun f \<sqsubseteq> Abs_cfun g"
-by (simp add: below_cfun_def Abs_cfun_inverse2)
+lemma monofun_LAM:
+  "\<lbrakk>cont f; cont g; \<And>x. f x \<sqsubseteq> g x\<rbrakk> \<Longrightarrow> (\<Lambda> x. f x) \<sqsubseteq> (\<Lambda> x. g x)"
+by (simp add: cfun_below_iff)
 
 text {* some lemmata for functions with flat/chfin domain/range types *}
 
@@ -418,29 +415,6 @@
   "\<lbrakk>\<forall>x. f\<cdot>(g\<cdot>x) = x; z \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> g\<cdot>z \<noteq> \<bottom>"
 by (erule contrapos_nn, rule injection_defined_rev)
 
-text {* propagation of flatness and chain-finiteness by retractions *}
-
-lemma chfin2chfin:
-  "\<forall>y. (f::'a::chfin \<rightarrow> 'b)\<cdot>(g\<cdot>y) = y
-    \<Longrightarrow> \<forall>Y::nat \<Rightarrow> 'b. chain Y \<longrightarrow> (\<exists>n. max_in_chain n Y)"
-apply clarify
-apply (drule_tac f=g in chain_monofun)
-apply (drule chfin)
-apply (unfold max_in_chain_def)
-apply (simp add: injection_eq)
-done
-
-lemma flat2flat:
-  "\<forall>y. (f::'a::flat \<rightarrow> 'b::pcpo)\<cdot>(g\<cdot>y) = y
-    \<Longrightarrow> \<forall>x y::'b. x \<sqsubseteq> y \<longrightarrow> x = \<bottom> \<or> x = y"
-apply clarify
-apply (drule_tac f=g in monofun_cfun_arg)
-apply (drule ax_flat)
-apply (erule disjE)
-apply (simp add: injection_defined_rev)
-apply (simp add: injection_eq)
-done
-
 text {* a result about functions with flat codomain *}
 
 lemma flat_eqI: "\<lbrakk>(x::'a::flat) \<sqsubseteq> y; x \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> x = y"
diff -r 61a1519d985f -r 3128c2a54785 src/HOLCF/ConvexPD.thy
--- a/src/HOLCF/ConvexPD.thy	Wed Nov 03 15:57:39 2010 -0700
+++ b/src/HOLCF/ConvexPD.thy	Wed Nov 03 16:39:23 2010 -0700
@@ -329,10 +329,6 @@
 apply (rule fold_pd_PDPlus [OF ACI_convex_bind])
 done
 
-lemma monofun_LAM:
-  "\<lbrakk>cont f; cont g; \<And>x. f x \<sqsubseteq> g x\<rbrakk> \<Longrightarrow> (\<Lambda> x. f x) \<sqsubseteq> (\<Lambda> x. g x)"
-by (simp add: cfun_below_iff)
-
 lemma convex_bind_basis_mono:
   "t \<le>\<natural> u \<Longrightarrow> convex_bind_basis t \<sqsubseteq> convex_bind_basis u"
 apply (erule convex_le_induct)
diff -r 61a1519d985f -r 3128c2a54785 src/HOLCF/Porder.thy
--- a/src/HOLCF/Porder.thy	Wed Nov 03 15:57:39 2010 -0700
+++ b/src/HOLCF/Porder.thy	Wed Nov 03 16:39:23 2010 -0700
@@ -34,19 +34,9 @@
   assumes below_antisym: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y"
 begin
 
-text {* minimal fixes least element *}
-
-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"
-  by simp
-
 lemma box_below: "a \<sqsubseteq> b \<Longrightarrow> c \<sqsubseteq> a \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> c \<sqsubseteq> d"
   by (rule below_trans [OF below_trans])