changed continuous functions from pcpo to cpo (including instances)
authorslotosch
Tue Mar 25 11:13:12 1997 +0100 (1997-03-25)
changeset 28382e908f29bc3d
parent 2837 dee1c7f1f576
child 2839 7ca787c6efca
changed continuous functions from pcpo to cpo (including instances)
src/HOLCF/Cfun1.ML
src/HOLCF/Cfun1.thy
src/HOLCF/Cfun2.ML
src/HOLCF/Cfun2.thy
src/HOLCF/Cfun3.thy
src/HOLCF/Cont.ML
src/HOLCF/Cont.thy
src/HOLCF/Fun2.ML
src/HOLCF/Fun3.thy
     1.1 --- a/src/HOLCF/Cfun1.ML	Tue Mar 25 10:43:01 1997 +0100
     1.2 +++ b/src/HOLCF/Cfun1.ML	Tue Mar 25 11:13:12 1997 +0100
     1.3 @@ -35,14 +35,14 @@
     1.4  (* less_cfun is a partial order on type 'a -> 'b                            *)
     1.5  (* ------------------------------------------------------------------------ *)
     1.6  
     1.7 -qed_goalw "refl_less_cfun" thy [less_cfun_def] "less(f::'a::pcpo->'b::pcpo) f"
     1.8 +qed_goalw "refl_less_cfun" thy [less_cfun_def] "less(f::'a->'b) f"
     1.9  (fn prems =>
    1.10          [
    1.11          (rtac refl_less 1)
    1.12          ]);
    1.13  
    1.14  qed_goalw "antisym_less_cfun" thy [less_cfun_def] 
    1.15 -        "[|less (f1::'a::pcpo->'b::pcpo) f2; less f2 f1|] ==> f1 = f2"
    1.16 +        "[|less (f1::'a->'b) f2; less f2 f1|] ==> f1 = f2"
    1.17  (fn prems =>
    1.18          [
    1.19          (cut_facts_tac prems 1),
    1.20 @@ -55,7 +55,7 @@
    1.21          ]);
    1.22  
    1.23  qed_goalw "trans_less_cfun" thy [less_cfun_def] 
    1.24 -        "[|less (f1::'a::pcpo->'b::pcpo) f2; less f2 f3|] ==> less f1 f3"
    1.25 +        "[|less (f1::'a->'b) f2; less f2 f3|] ==> less f1 f3"
    1.26  (fn prems =>
    1.27          [
    1.28          (cut_facts_tac prems 1),
    1.29 @@ -129,7 +129,3 @@
    1.30          (rtac Cfunapp2 1),
    1.31          (atac 1)
    1.32          ]);
    1.33 -
    1.34 -
    1.35 -
    1.36 -
     2.1 --- a/src/HOLCF/Cfun1.thy	Tue Mar 25 10:43:01 1997 +0100
     2.2 +++ b/src/HOLCF/Cfun1.thy	Tue Mar 25 11:13:12 1997 +0100
     2.3 @@ -9,6 +9,8 @@
     2.4  
     2.5  Cfun1 = Cont +
     2.6  
     2.7 +default cpo
     2.8 +
     2.9  typedef (CFun)  ('a, 'b) "->" (infixr 0) = "{f. cont f}" (CfunI)
    2.10  
    2.11  consts  
     3.1 --- a/src/HOLCF/Cfun2.ML	Tue Mar 25 10:43:01 1997 +0100
     3.2 +++ b/src/HOLCF/Cfun2.ML	Tue Mar 25 11:13:12 1997 +0100
     3.3 @@ -41,7 +41,7 @@
     3.4  
     3.5  bind_thm ("UU_cfun_def",minimal_cfun RS minimal2UU RS sym);
     3.6  
     3.7 -qed_goal "least_cfun" thy "? x::'a->'b.!y.x<<y"
     3.8 +qed_goal "least_cfun" thy "? x::'a->'b::pcpo.!y.x<<y"
     3.9  (fn prems =>
    3.10          [
    3.11          (res_inst_tac [("x","fabs(% x.UU)")] exI 1),
    3.12 @@ -237,7 +237,7 @@
    3.13  *)
    3.14  
    3.15  qed_goal "cpo_cfun" thy 
    3.16 -  "is_chain(CCF::nat=>('a::pcpo->'b::pcpo)) ==> ? x. range(CCF) <<| x"
    3.17 +  "is_chain(CCF::nat=>('a->'b)) ==> ? x. range(CCF) <<| x"
    3.18  (fn prems =>
    3.19          [
    3.20          (cut_facts_tac prems 1),
     4.1 --- a/src/HOLCF/Cfun2.thy	Tue Mar 25 10:43:01 1997 +0100
     4.2 +++ b/src/HOLCF/Cfun2.thy	Tue Mar 25 11:13:12 1997 +0100
     4.3 @@ -3,12 +3,12 @@
     4.4      Author:     Franz Regensburger
     4.5      Copyright   1993 Technische Universitaet Muenchen
     4.6  
     4.7 -Class Instance ->::(pcpo,pcpo)po
     4.8 +Class Instance ->::(cpo,cpo)po
     4.9  
    4.10  *)
    4.11  
    4.12  Cfun2 = Cfun1 + 
    4.13  
    4.14 -instance "->"::(pcpo,pcpo)po (refl_less_cfun,antisym_less_cfun,trans_less_cfun)
    4.15 +instance "->"::(cpo,cpo)po (refl_less_cfun,antisym_less_cfun,trans_less_cfun)
    4.16  
    4.17  end
     5.1 --- a/src/HOLCF/Cfun3.thy	Tue Mar 25 10:43:01 1997 +0100
     5.2 +++ b/src/HOLCF/Cfun3.thy	Tue Mar 25 11:13:12 1997 +0100
     5.3 @@ -9,7 +9,10 @@
     5.4  
     5.5  Cfun3 = Cfun2 +
     5.6  
     5.7 -instance "->" :: (pcpo,pcpo)pcpo              (least_cfun,cpo_cfun)
     5.8 +instance "->" :: (cpo,cpo)cpo              (cpo_cfun)
     5.9 +instance "->" :: (cpo,pcpo)pcpo            (least_cfun)
    5.10 +
    5.11 +default pcpo
    5.12  
    5.13  consts  
    5.14          Istrictify   :: "('a->'b)=>'a=>'b"
     6.1 --- a/src/HOLCF/Cont.ML	Tue Mar 25 10:43:01 1997 +0100
     6.2 +++ b/src/HOLCF/Cont.ML	Tue Mar 25 11:13:12 1997 +0100
     6.3 @@ -229,8 +229,8 @@
     6.4  
     6.5  
     6.6  qed_goal "ch2ch_lubMF2R" thy 
     6.7 -"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
     6.8 -\  !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
     6.9 +"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
    6.10 +\  !f.monofun(MF2(f)::('b::po=>'c::cpo));\
    6.11  \       is_chain(F);is_chain(Y)|] ==> \
    6.12  \       is_chain(%j. lub(range(%i. MF2 (F j) (Y i))))"
    6.13  (fn prems =>
    6.14 @@ -249,8 +249,8 @@
    6.15  
    6.16  
    6.17  qed_goal "ch2ch_lubMF2L" thy 
    6.18 -"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
    6.19 -\  !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
    6.20 +"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
    6.21 +\  !f.monofun(MF2(f)::('b::po=>'c::cpo));\
    6.22  \       is_chain(F);is_chain(Y)|] ==> \
    6.23  \       is_chain(%i. lub(range(%j. MF2 (F j) (Y i))))"
    6.24  (fn prems =>
    6.25 @@ -269,8 +269,8 @@
    6.26  
    6.27  
    6.28  qed_goal "lub_MF2_mono" thy 
    6.29 -"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
    6.30 -\  !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
    6.31 +"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
    6.32 +\  !f.monofun(MF2(f)::('b::po=>'c::cpo));\
    6.33  \       is_chain(F)|] ==> \
    6.34  \       monofun(% x.lub(range(% j.MF2 (F j) (x))))"
    6.35  (fn prems =>
    6.36 @@ -289,8 +289,8 @@
    6.37          ]);
    6.38  
    6.39  qed_goal "ex_lubMF2" thy 
    6.40 -"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
    6.41 -\  !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
    6.42 +"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
    6.43 +\  !f.monofun(MF2(f)::('b::po=>'c::cpo));\
    6.44  \       is_chain(F); is_chain(Y)|] ==> \
    6.45  \               lub(range(%j. lub(range(%i. MF2(F j) (Y i))))) =\
    6.46  \               lub(range(%i. lub(range(%j. MF2(F j) (Y i)))))"
    6.47 @@ -328,8 +328,8 @@
    6.48  
    6.49  
    6.50  qed_goal "diag_lubMF2_1" thy 
    6.51 -"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
    6.52 -\  !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
    6.53 +"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
    6.54 +\  !f.monofun(MF2(f)::('b::po=>'c::cpo));\
    6.55  \  is_chain(FY);is_chain(TY)|] ==>\
    6.56  \ lub(range(%i. lub(range(%j. MF2(FY(j))(TY(i)))))) =\
    6.57  \ lub(range(%i. MF2(FY(i))(TY(i))))"
    6.58 @@ -372,8 +372,8 @@
    6.59          ]);
    6.60  
    6.61  qed_goal "diag_lubMF2_2" thy 
    6.62 -"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
    6.63 -\  !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
    6.64 +"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
    6.65 +\  !f.monofun(MF2(f)::('b::po=>'c::cpo));\
    6.66  \  is_chain(FY);is_chain(TY)|] ==>\
    6.67  \ lub(range(%j. lub(range(%i. MF2(FY(j))(TY(i)))))) =\
    6.68  \ lub(range(%i. MF2(FY(i))(TY(i))))"
    6.69 @@ -388,8 +388,6 @@
    6.70          ]);
    6.71  
    6.72  
    6.73 -
    6.74 -
    6.75  (* ------------------------------------------------------------------------ *)
    6.76  (* The following results are about a curried function that is continuous    *)
    6.77  (* in both arguments                                                        *)
    6.78 @@ -520,14 +518,13 @@
    6.79          (atac 1)
    6.80          ]);
    6.81  
    6.82 -
    6.83  (* ------------------------------------------------------------------------ *)
    6.84  (* What D.A.Schmidt calls continuity of abstraction                         *)
    6.85  (* never used here                                                          *)
    6.86  (* ------------------------------------------------------------------------ *)
    6.87  
    6.88  qed_goal "contlub_abstraction" thy
    6.89 -"[|is_chain(Y::nat=>'a);!y.cont(%x.(c::'a=>'b=>'c) x y)|] ==>\
    6.90 +"[|is_chain(Y::nat=>'a);!y.cont(%x.(c::'a::cpo=>'b::cpo=>'c::cpo) x y)|] ==>\
    6.91  \ (%y.lub(range(%i.c (Y i) y))) = (lub(range(%i.%y.c (Y i) y)))"
    6.92   (fn prems =>
    6.93          [
    6.94 @@ -542,7 +539,6 @@
    6.95          (atac 1)
    6.96          ]);
    6.97  
    6.98 -
    6.99  qed_goal "mono2mono_app" thy 
   6.100  "[|monofun(ft);!x.monofun(ft(x));monofun(tt)|] ==>\
   6.101  \        monofun(%x.(ft(x))(tt(x)))"
     7.1 --- a/src/HOLCF/Cont.thy	Tue Mar 25 10:43:01 1997 +0100
     7.2 +++ b/src/HOLCF/Cont.thy	Tue Mar 25 11:13:12 1997 +0100
     7.3 @@ -16,12 +16,12 @@
     7.4  *)
     7.5  
     7.6  
     7.7 -default pcpo
     7.8 +default po
     7.9  
    7.10  consts  
    7.11 -        monofun :: "('a::po => 'b::po) => bool" (* monotonicity    *)
    7.12 -        contlub :: "('a => 'b) => bool"         (* first cont. def *)
    7.13 -        cont    :: "('a => 'b) => bool"         (* secnd cont. def *)
    7.14 +        monofun :: "('a => 'b) => bool" (* monotonicity    *)
    7.15 +        contlub :: "('a::cpo => 'b::cpo) => bool"         (* first cont. def *)
    7.16 +        cont    :: "('a::cpo => 'b::cpo) => bool"         (* secnd cont. def *)
    7.17  
    7.18  defs 
    7.19  
     8.1 --- a/src/HOLCF/Fun2.ML	Tue Mar 25 10:43:01 1997 +0100
     8.2 +++ b/src/HOLCF/Fun2.ML	Tue Mar 25 11:13:12 1997 +0100
     8.3 @@ -86,7 +86,7 @@
     8.4  (* ------------------------------------------------------------------------ *)
     8.5  
     8.6  qed_goal "lub_fun"  Fun2.thy
     8.7 -        "is_chain(S::nat=>('a::term => 'b::pcpo)) ==> \
     8.8 +        "is_chain(S::nat=>('a::term => 'b::cpo)) ==> \
     8.9  \        range(S) <<| (% x.lub(range(% i.S(i)(x))))"
    8.10  (fn prems =>
    8.11          [
    8.12 @@ -111,7 +111,7 @@
    8.13  (* is_chain ?S1 ==> lub (range ?S1) = (%x. lub (range (%i. ?S1 i x))) *)
    8.14  
    8.15  qed_goal "cpo_fun"  Fun2.thy
    8.16 -        "is_chain(S::nat=>('a::term => 'b::pcpo)) ==> ? x. range(S) <<| x"
    8.17 +        "is_chain(S::nat=>('a::term => 'b::cpo)) ==> ? x. range(S) <<| x"
    8.18  (fn prems =>
    8.19          [
    8.20          (cut_facts_tac prems 1),
     9.1 --- a/src/HOLCF/Fun3.thy	Tue Mar 25 10:43:01 1997 +0100
     9.2 +++ b/src/HOLCF/Fun3.thy	Tue Mar 25 11:13:12 1997 +0100
     9.3 @@ -11,7 +11,8 @@
     9.4  
     9.5  (* default class is still term *)
     9.6  
     9.7 -instance fun  :: (term,pcpo)pcpo         (least_fun,cpo_fun)
     9.8 +instance fun  :: (term,cpo)cpo         (cpo_fun)
     9.9 +instance fun  :: (term,pcpo)pcpo       (least_fun)
    9.10  
    9.11  end
    9.12