# HG changeset patch
# User huffman
# Date 1112231002 -7200
# Node ID b389f108c4854c439920511a115628ad79a558e3
# Parent  2d1d6ea579a1cb6cc283a015e42892434ecb09b6
added theorems eta_cfun and cont2cont_eta

diff -r 2d1d6ea579a1 -r b389f108c485 src/HOLCF/Cfun.ML
--- a/src/HOLCF/Cfun.ML	Thu Mar 31 03:01:21 2005 +0200
+++ b/src/HOLCF/Cfun.ML	Thu Mar 31 03:03:22 2005 +0200
@@ -14,6 +14,7 @@
 val Abs_Cfun_inverse2 = thm "Abs_Cfun_inverse2";
 val Cfunapp2 = thm "Cfunapp2";
 val beta_cfun = thm "beta_cfun";
+val eta_cfun = thm "eta_cfun";
 val inst_cfun_po = thm "inst_cfun_po";
 val less_cfun = thm "less_cfun";
 val minimal_cfun = thm "minimal_cfun";
@@ -55,6 +56,7 @@
 val cont2cont_Rep_CFun = thm "cont2cont_Rep_CFun";
 val cont2mono_LAM = thm "cont2mono_LAM";
 val cont2cont_LAM = thm "cont2cont_LAM";
+val cont2cont_eta = thm "cont2cont_eta";
 val cont_lemmas1 = [cont_const, cont_id, cont_Rep_CFun2,
                     cont2cont_Rep_CFun, cont2cont_LAM];
 val strict_Rep_CFun1 = thm "strict_Rep_CFun1";
diff -r 2d1d6ea579a1 -r b389f108c485 src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Thu Mar 31 03:01:21 2005 +0200
+++ b/src/HOLCF/Cfun.thy	Thu Mar 31 03:03:22 2005 +0200
@@ -70,6 +70,11 @@
 lemma beta_cfun: "cont(c1) ==> (LAM x .c1 x)$u = c1 u"
 by (rule Cfunapp2)
 
+text {* Eta - equality for continuous functions *}
+
+lemma eta_cfun: "(LAM x. f$x) = f"
+by (rule Rep_CFun_inverse)
+
 subsection {* Type @{typ "'a -> 'b"} is a partial order *}
 
 instance "->"  :: (cpo, cpo) sq_ord ..
@@ -424,6 +429,11 @@
 apply (erule p2 [THEN cont2contlub, THEN contlubE, THEN spec, THEN mp])
 done
 
+text {* cont2cont Lemma for @{term "%x. LAM y. c1 x$y"} *}
+
+lemma cont2cont_eta: "cont c1 ==> cont (%x. LAM y. c1 x$y)"
+by (simp only: eta_cfun)
+
 text {* cont2cont tactic *}
 
 lemmas cont_lemmas1 = cont_const cont_id cont_Rep_CFun2