--- 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";
--- 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