# HG changeset patch
# User slotosch
# Date 859284792 -3600
# Node ID 2e908f29bc3dc6a45f9081abf2318a951504ecb8
# Parent  dee1c7f1f576fe6f57b89cd7918136b7ac2ecc7a
changed continuous functions from pcpo to cpo (including instances)

diff -r dee1c7f1f576 -r 2e908f29bc3d src/HOLCF/Cfun1.ML
--- a/src/HOLCF/Cfun1.ML	Tue Mar 25 10:43:01 1997 +0100
+++ b/src/HOLCF/Cfun1.ML	Tue Mar 25 11:13:12 1997 +0100
@@ -35,14 +35,14 @@
 (* less_cfun is a partial order on type 'a -> 'b                            *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goalw "refl_less_cfun" thy [less_cfun_def] "less(f::'a::pcpo->'b::pcpo) f"
+qed_goalw "refl_less_cfun" thy [less_cfun_def] "less(f::'a->'b) f"
 (fn prems =>
         [
         (rtac refl_less 1)
         ]);
 
 qed_goalw "antisym_less_cfun" thy [less_cfun_def] 
-        "[|less (f1::'a::pcpo->'b::pcpo) f2; less f2 f1|] ==> f1 = f2"
+        "[|less (f1::'a->'b) f2; less f2 f1|] ==> f1 = f2"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -55,7 +55,7 @@
         ]);
 
 qed_goalw "trans_less_cfun" thy [less_cfun_def] 
-        "[|less (f1::'a::pcpo->'b::pcpo) f2; less f2 f3|] ==> less f1 f3"
+        "[|less (f1::'a->'b) f2; less f2 f3|] ==> less f1 f3"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -129,7 +129,3 @@
         (rtac Cfunapp2 1),
         (atac 1)
         ]);
-
-
-
-
diff -r dee1c7f1f576 -r 2e908f29bc3d src/HOLCF/Cfun1.thy
--- a/src/HOLCF/Cfun1.thy	Tue Mar 25 10:43:01 1997 +0100
+++ b/src/HOLCF/Cfun1.thy	Tue Mar 25 11:13:12 1997 +0100
@@ -9,6 +9,8 @@
 
 Cfun1 = Cont +
 
+default cpo
+
 typedef (CFun)  ('a, 'b) "->" (infixr 0) = "{f. cont f}" (CfunI)
 
 consts  
diff -r dee1c7f1f576 -r 2e908f29bc3d src/HOLCF/Cfun2.ML
--- a/src/HOLCF/Cfun2.ML	Tue Mar 25 10:43:01 1997 +0100
+++ b/src/HOLCF/Cfun2.ML	Tue Mar 25 11:13:12 1997 +0100
@@ -41,7 +41,7 @@
 
 bind_thm ("UU_cfun_def",minimal_cfun RS minimal2UU RS sym);
 
-qed_goal "least_cfun" thy "? x::'a->'b.!y.x<<y"
+qed_goal "least_cfun" thy "? x::'a->'b::pcpo.!y.x<<y"
 (fn prems =>
         [
         (res_inst_tac [("x","fabs(% x.UU)")] exI 1),
@@ -237,7 +237,7 @@
 *)
 
 qed_goal "cpo_cfun" thy 
-  "is_chain(CCF::nat=>('a::pcpo->'b::pcpo)) ==> ? x. range(CCF) <<| x"
+  "is_chain(CCF::nat=>('a->'b)) ==> ? x. range(CCF) <<| x"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
diff -r dee1c7f1f576 -r 2e908f29bc3d src/HOLCF/Cfun2.thy
--- a/src/HOLCF/Cfun2.thy	Tue Mar 25 10:43:01 1997 +0100
+++ b/src/HOLCF/Cfun2.thy	Tue Mar 25 11:13:12 1997 +0100
@@ -3,12 +3,12 @@
     Author:     Franz Regensburger
     Copyright   1993 Technische Universitaet Muenchen
 
-Class Instance ->::(pcpo,pcpo)po
+Class Instance ->::(cpo,cpo)po
 
 *)
 
 Cfun2 = Cfun1 + 
 
-instance "->"::(pcpo,pcpo)po (refl_less_cfun,antisym_less_cfun,trans_less_cfun)
+instance "->"::(cpo,cpo)po (refl_less_cfun,antisym_less_cfun,trans_less_cfun)
 
 end
diff -r dee1c7f1f576 -r 2e908f29bc3d src/HOLCF/Cfun3.thy
--- a/src/HOLCF/Cfun3.thy	Tue Mar 25 10:43:01 1997 +0100
+++ b/src/HOLCF/Cfun3.thy	Tue Mar 25 11:13:12 1997 +0100
@@ -9,7 +9,10 @@
 
 Cfun3 = Cfun2 +
 
-instance "->" :: (pcpo,pcpo)pcpo              (least_cfun,cpo_cfun)
+instance "->" :: (cpo,cpo)cpo              (cpo_cfun)
+instance "->" :: (cpo,pcpo)pcpo            (least_cfun)
+
+default pcpo
 
 consts  
         Istrictify   :: "('a->'b)=>'a=>'b"
diff -r dee1c7f1f576 -r 2e908f29bc3d src/HOLCF/Cont.ML
--- a/src/HOLCF/Cont.ML	Tue Mar 25 10:43:01 1997 +0100
+++ b/src/HOLCF/Cont.ML	Tue Mar 25 11:13:12 1997 +0100
@@ -229,8 +229,8 @@
 
 
 qed_goal "ch2ch_lubMF2R" thy 
-"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
-\  !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
+"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
+\  !f.monofun(MF2(f)::('b::po=>'c::cpo));\
 \       is_chain(F);is_chain(Y)|] ==> \
 \       is_chain(%j. lub(range(%i. MF2 (F j) (Y i))))"
 (fn prems =>
@@ -249,8 +249,8 @@
 
 
 qed_goal "ch2ch_lubMF2L" thy 
-"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
-\  !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
+"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
+\  !f.monofun(MF2(f)::('b::po=>'c::cpo));\
 \       is_chain(F);is_chain(Y)|] ==> \
 \       is_chain(%i. lub(range(%j. MF2 (F j) (Y i))))"
 (fn prems =>
@@ -269,8 +269,8 @@
 
 
 qed_goal "lub_MF2_mono" thy 
-"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
-\  !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
+"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
+\  !f.monofun(MF2(f)::('b::po=>'c::cpo));\
 \       is_chain(F)|] ==> \
 \       monofun(% x.lub(range(% j.MF2 (F j) (x))))"
 (fn prems =>
@@ -289,8 +289,8 @@
         ]);
 
 qed_goal "ex_lubMF2" thy 
-"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
-\  !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
+"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
+\  !f.monofun(MF2(f)::('b::po=>'c::cpo));\
 \       is_chain(F); is_chain(Y)|] ==> \
 \               lub(range(%j. lub(range(%i. MF2(F j) (Y i))))) =\
 \               lub(range(%i. lub(range(%j. MF2(F j) (Y i)))))"
@@ -328,8 +328,8 @@
 
 
 qed_goal "diag_lubMF2_1" thy 
-"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
-\  !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
+"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
+\  !f.monofun(MF2(f)::('b::po=>'c::cpo));\
 \  is_chain(FY);is_chain(TY)|] ==>\
 \ lub(range(%i. lub(range(%j. MF2(FY(j))(TY(i)))))) =\
 \ lub(range(%i. MF2(FY(i))(TY(i))))"
@@ -372,8 +372,8 @@
         ]);
 
 qed_goal "diag_lubMF2_2" thy 
-"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
-\  !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
+"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
+\  !f.monofun(MF2(f)::('b::po=>'c::cpo));\
 \  is_chain(FY);is_chain(TY)|] ==>\
 \ lub(range(%j. lub(range(%i. MF2(FY(j))(TY(i)))))) =\
 \ lub(range(%i. MF2(FY(i))(TY(i))))"
@@ -388,8 +388,6 @@
         ]);
 
 
-
-
 (* ------------------------------------------------------------------------ *)
 (* The following results are about a curried function that is continuous    *)
 (* in both arguments                                                        *)
@@ -520,14 +518,13 @@
         (atac 1)
         ]);
 
-
 (* ------------------------------------------------------------------------ *)
 (* What D.A.Schmidt calls continuity of abstraction                         *)
 (* never used here                                                          *)
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "contlub_abstraction" thy
-"[|is_chain(Y::nat=>'a);!y.cont(%x.(c::'a=>'b=>'c) x y)|] ==>\
+"[|is_chain(Y::nat=>'a);!y.cont(%x.(c::'a::cpo=>'b::cpo=>'c::cpo) x y)|] ==>\
 \ (%y.lub(range(%i.c (Y i) y))) = (lub(range(%i.%y.c (Y i) y)))"
  (fn prems =>
         [
@@ -542,7 +539,6 @@
         (atac 1)
         ]);
 
-
 qed_goal "mono2mono_app" thy 
 "[|monofun(ft);!x.monofun(ft(x));monofun(tt)|] ==>\
 \        monofun(%x.(ft(x))(tt(x)))"
diff -r dee1c7f1f576 -r 2e908f29bc3d src/HOLCF/Cont.thy
--- a/src/HOLCF/Cont.thy	Tue Mar 25 10:43:01 1997 +0100
+++ b/src/HOLCF/Cont.thy	Tue Mar 25 11:13:12 1997 +0100
@@ -16,12 +16,12 @@
 *)
 
 
-default pcpo
+default po
 
 consts  
-        monofun :: "('a::po => 'b::po) => bool" (* monotonicity    *)
-        contlub :: "('a => 'b) => bool"         (* first cont. def *)
-        cont    :: "('a => 'b) => bool"         (* secnd cont. def *)
+        monofun :: "('a => 'b) => bool" (* monotonicity    *)
+        contlub :: "('a::cpo => 'b::cpo) => bool"         (* first cont. def *)
+        cont    :: "('a::cpo => 'b::cpo) => bool"         (* secnd cont. def *)
 
 defs 
 
diff -r dee1c7f1f576 -r 2e908f29bc3d src/HOLCF/Fun2.ML
--- a/src/HOLCF/Fun2.ML	Tue Mar 25 10:43:01 1997 +0100
+++ b/src/HOLCF/Fun2.ML	Tue Mar 25 11:13:12 1997 +0100
@@ -86,7 +86,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "lub_fun"  Fun2.thy
-        "is_chain(S::nat=>('a::term => 'b::pcpo)) ==> \
+        "is_chain(S::nat=>('a::term => 'b::cpo)) ==> \
 \        range(S) <<| (% x.lub(range(% i.S(i)(x))))"
 (fn prems =>
         [
@@ -111,7 +111,7 @@
 (* is_chain ?S1 ==> lub (range ?S1) = (%x. lub (range (%i. ?S1 i x))) *)
 
 qed_goal "cpo_fun"  Fun2.thy
-        "is_chain(S::nat=>('a::term => 'b::pcpo)) ==> ? x. range(S) <<| x"
+        "is_chain(S::nat=>('a::term => 'b::cpo)) ==> ? x. range(S) <<| x"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
diff -r dee1c7f1f576 -r 2e908f29bc3d src/HOLCF/Fun3.thy
--- a/src/HOLCF/Fun3.thy	Tue Mar 25 10:43:01 1997 +0100
+++ b/src/HOLCF/Fun3.thy	Tue Mar 25 11:13:12 1997 +0100
@@ -11,7 +11,8 @@
 
 (* default class is still term *)
 
-instance fun  :: (term,pcpo)pcpo         (least_fun,cpo_fun)
+instance fun  :: (term,cpo)cpo         (cpo_fun)
+instance fun  :: (term,pcpo)pcpo       (least_fun)
 
 end