# 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 @@ "(\y::'a::discrete_cpo. cont (\x. f x y)) \ cont (\x. \ 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: - "\cont f; cont g; f \ g\ \ Abs_cfun f \ Abs_cfun g" -by (simp add: below_cfun_def Abs_cfun_inverse2) +lemma monofun_LAM: + "\cont f; cont g; \x. f x \ g x\ \ (\ x. f x) \ (\ x. g x)" +by (simp add: cfun_below_iff) text {* some lemmata for functions with flat/chfin domain/range types *} @@ -418,29 +415,6 @@ "\\x. f\(g\x) = x; z \ \\ \ g\z \ \" by (erule contrapos_nn, rule injection_defined_rev) -text {* propagation of flatness and chain-finiteness by retractions *} - -lemma chfin2chfin: - "\y. (f::'a::chfin \ 'b)\(g\y) = y - \ \Y::nat \ 'b. chain Y \ (\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: - "\y. (f::'a::flat \ 'b::pcpo)\(g\y) = y - \ \x y::'b. x \ y \ x = \ \ 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: "\(x::'a::flat) \ y; x \ \\ \ 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: - "\cont f; cont g; \x. f x \ g x\ \ (\ x. f x) \ (\ x. g x)" -by (simp add: cfun_below_iff) - lemma convex_bind_basis_mono: "t \\ u \ convex_bind_basis t \ 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 \ y \ y \ x \ x = y" begin -text {* minimal fixes least element *} - -lemma minimal2UU[OF allI] : "\x. uu \ x \ uu = (THE u. \y. u \ y)" - by (blast intro: theI2 below_antisym) - lemma eq_imp_below: "x = y \ x \ y" by simp -text {* the reverse law of anti-symmetry of @{term "op <<"} *} -(* Is this rule ever useful? *) -lemma below_antisym_inverse: "x = y \ x \ y \ y \ x" - by simp - lemma box_below: "a \ b \ c \ a \ b \ d \ c \ d" by (rule below_trans [OF below_trans])