# HG changeset patch # User huffman # Date 1286887712 25200 # Node ID 3e3611136a1318bc090b0b45c7828b34c0f33f0b # Parent 9f6ed6840e8d66d45e4ddd342ebf97522d7490c9 remove unused lemmas diff -r 9f6ed6840e8d -r 3e3611136a13 src/HOLCF/Cfun.thy --- a/src/HOLCF/Cfun.thy Tue Oct 12 05:48:15 2010 -0700 +++ b/src/HOLCF/Cfun.thy Tue Oct 12 05:48:32 2010 -0700 @@ -293,29 +293,6 @@ apply (rule minimal [THEN monofun_cfun_arg]) done -text {* the lub of a chain of continous functions is monotone *} - -lemma lub_cfun_mono: "chain F \ monofun (\x. \i. F i\x)" -apply (drule ch2ch_monofun [OF monofun_Rep_CFun]) -apply (simp add: thelub_fun [symmetric]) -apply (erule monofun_lub_fun) -apply (simp add: monofun_Rep_CFun2) -done - -text {* a lemma about the exchange of lubs for type @{typ "'a -> 'b"} *} - -lemma ex_lub_cfun: - "\chain F; chain Y\ \ (\j. \i. F j\(Y i)) = (\i. \j. F j\(Y i))" -by (simp add: diag_lub) - -text {* the lub of a chain of cont. functions is continuous *} - -lemma cont_lub_cfun: "chain F \ cont (\x. \i. F i\x)" -apply (rule cont2cont_lub) -apply (erule monofun_Rep_CFun [THEN ch2ch_monofun]) -apply (rule cont_Rep_CFun2) -done - text {* type @{typ "'a -> 'b"} is chain complete *} lemma lub_cfun: "chain F \ range F <<| (\ x. \i. F i\x)"