added theorems eta_cfun and cont2cont_eta
authorhuffman
Thu Mar 31 03:03:22 2005 +0200 (2005-03-31 ago)
changeset 15641b389f108c485
parent 15640 2d1d6ea579a1
child 15642 028059faa963
added theorems eta_cfun and cont2cont_eta
src/HOLCF/Cfun.ML
src/HOLCF/Cfun.thy
     1.1 --- a/src/HOLCF/Cfun.ML	Thu Mar 31 03:01:21 2005 +0200
     1.2 +++ b/src/HOLCF/Cfun.ML	Thu Mar 31 03:03:22 2005 +0200
     1.3 @@ -14,6 +14,7 @@
     1.4  val Abs_Cfun_inverse2 = thm "Abs_Cfun_inverse2";
     1.5  val Cfunapp2 = thm "Cfunapp2";
     1.6  val beta_cfun = thm "beta_cfun";
     1.7 +val eta_cfun = thm "eta_cfun";
     1.8  val inst_cfun_po = thm "inst_cfun_po";
     1.9  val less_cfun = thm "less_cfun";
    1.10  val minimal_cfun = thm "minimal_cfun";
    1.11 @@ -55,6 +56,7 @@
    1.12  val cont2cont_Rep_CFun = thm "cont2cont_Rep_CFun";
    1.13  val cont2mono_LAM = thm "cont2mono_LAM";
    1.14  val cont2cont_LAM = thm "cont2cont_LAM";
    1.15 +val cont2cont_eta = thm "cont2cont_eta";
    1.16  val cont_lemmas1 = [cont_const, cont_id, cont_Rep_CFun2,
    1.17                      cont2cont_Rep_CFun, cont2cont_LAM];
    1.18  val strict_Rep_CFun1 = thm "strict_Rep_CFun1";
     2.1 --- a/src/HOLCF/Cfun.thy	Thu Mar 31 03:01:21 2005 +0200
     2.2 +++ b/src/HOLCF/Cfun.thy	Thu Mar 31 03:03:22 2005 +0200
     2.3 @@ -70,6 +70,11 @@
     2.4  lemma beta_cfun: "cont(c1) ==> (LAM x .c1 x)$u = c1 u"
     2.5  by (rule Cfunapp2)
     2.6  
     2.7 +text {* Eta - equality for continuous functions *}
     2.8 +
     2.9 +lemma eta_cfun: "(LAM x. f$x) = f"
    2.10 +by (rule Rep_CFun_inverse)
    2.11 +
    2.12  subsection {* Type @{typ "'a -> 'b"} is a partial order *}
    2.13  
    2.14  instance "->"  :: (cpo, cpo) sq_ord ..
    2.15 @@ -424,6 +429,11 @@
    2.16  apply (erule p2 [THEN cont2contlub, THEN contlubE, THEN spec, THEN mp])
    2.17  done
    2.18  
    2.19 +text {* cont2cont Lemma for @{term "%x. LAM y. c1 x$y"} *}
    2.20 +
    2.21 +lemma cont2cont_eta: "cont c1 ==> cont (%x. LAM y. c1 x$y)"
    2.22 +by (simp only: eta_cfun)
    2.23 +
    2.24  text {* cont2cont tactic *}
    2.25  
    2.26  lemmas cont_lemmas1 = cont_const cont_id cont_Rep_CFun2