--- 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)
]);
-
-
-
-
--- 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
--- 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),
--- 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
--- 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"
--- 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)))"
--- 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
--- 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),
--- 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