# HG changeset patch # User huffman # Date 1291663362 28800 # Node ID 9883d1417ce1c4ef6fce0354309cd1746c242b9d # Parent ff7d177128ef0da39e48e27747dd333fcd9eac14 remove lemma cont_cfun; rename thelub_cfun to lub_cfun diff -r ff7d177128ef -r 9883d1417ce1 NEWS --- a/NEWS Mon Dec 06 10:08:33 2010 -0800 +++ b/NEWS Mon Dec 06 11:22:42 2010 -0800 @@ -526,6 +526,7 @@ lub_bin_chain ~> is_lub_bin_chain lub_fun ~> is_lub_fun thelub_fun ~> lub_fun + thelub_cfun ~> lub_cfun thelub_Pair ~> lub_Pair lub_cprod ~> is_lub_prod thelub_cprod ~> lub_prod diff -r ff7d177128ef -r 9883d1417ce1 src/HOL/HOLCF/Cfun.thy --- a/src/HOL/HOLCF/Cfun.thy Mon Dec 06 10:08:33 2010 -0800 +++ b/src/HOL/HOLCF/Cfun.thy Mon Dec 06 11:22:42 2010 -0800 @@ -248,13 +248,6 @@ "\chain F; chain Y\ \ (\i. F i\(Y i)) = (\i. F i)\(\i. Y i)" by (simp add: contlub_cfun_fun contlub_cfun_arg diag_lub) -lemma cont_cfun: - "\chain F; chain Y\ \ range (\i. F i\(Y i)) <<| (\i. F i)\(\i. Y i)" -apply (rule thelubE) -apply (simp only: ch2ch_Rep_cfun) -apply (simp only: lub_APP) -done - lemma lub_LAM: "\\x. chain (\i. F i x); \i. cont (\x. F i x)\ \ (\i. \ x. F i x) = (\ x. \i. F i x)" @@ -275,11 +268,8 @@ text {* type @{typ "'a -> 'b"} is chain complete *} -lemma lub_cfun: "chain F \ range F <<| (\ x. \i. F i\x)" -by (simp only: contlub_cfun_fun [symmetric] eta_cfun cpo_lubI) - -lemma thelub_cfun: "chain F \ (\i. F i) = (\ x. \i. F i\x)" -by (rule lub_cfun [THEN lub_eqI]) +lemma lub_cfun: "chain F \ (\i. F i) = (\ x. \i. F i\x)" +by (simp add: lub_cfun lub_fun ch2ch_lambda) subsection {* Continuity simplification procedure *}