generalized theorems and class instances for Cprod.
authorslotosch
Wed Mar 26 13:44:05 1997 +0100 (1997-03-26)
changeset 28407e03e61612b0
parent 2839 7ca787c6efca
child 2841 c2508f4ab739
generalized theorems and class instances for Cprod.
Now "*"::(cpo,cpo)cpo and "*"::(pcpo,pcpo)pcpo
src/HOLCF/Cprod1.thy
src/HOLCF/Cprod2.ML
src/HOLCF/Cprod2.thy
src/HOLCF/Cprod3.ML
src/HOLCF/Cprod3.thy
     1.1 --- a/src/HOLCF/Cprod1.thy	Tue Mar 25 11:19:09 1997 +0100
     1.2 +++ b/src/HOLCF/Cprod1.thy	Wed Mar 26 13:44:05 1997 +0100
     1.3 @@ -10,6 +10,8 @@
     1.4  
     1.5  Cprod1 = Cfun3 +
     1.6  
     1.7 +default cpo
     1.8 +
     1.9  defs
    1.10  
    1.11    less_cprod_def "less p1 p2 == (fst p1<<fst p2 & snd p1 << snd p2)"
     2.1 --- a/src/HOLCF/Cprod2.ML	Tue Mar 25 11:19:09 1997 +0100
     2.2 +++ b/src/HOLCF/Cprod2.ML	Wed Mar 26 13:44:05 1997 +0100
     2.3 @@ -147,7 +147,7 @@
     2.4  
     2.5  *)
     2.6  
     2.7 -qed_goal "cpo_cprod" thy "is_chain(S::nat=>'a*'b)==>? x.range S<<| x"
     2.8 +qed_goal "cpo_cprod" thy "is_chain(S::nat=>'a::cpo*'b::cpo)==>? x.range S<<| x"
     2.9  (fn prems =>
    2.10          [
    2.11          (cut_facts_tac prems 1),
     3.1 --- a/src/HOLCF/Cprod2.thy	Tue Mar 25 11:19:09 1997 +0100
     3.2 +++ b/src/HOLCF/Cprod2.thy	Wed Mar 26 13:44:05 1997 +0100
     3.3 @@ -9,7 +9,9 @@
     3.4  
     3.5  Cprod2 = Cprod1 + 
     3.6  
     3.7 -instance "*"::(pcpo,pcpo)po 
     3.8 +default pcpo
     3.9 +
    3.10 +instance "*"::(cpo,cpo)po 
    3.11  	(refl_less_cprod,antisym_less_cprod,trans_less_cprod)
    3.12  end
    3.13  
     4.1 --- a/src/HOLCF/Cprod3.ML	Tue Mar 25 11:19:09 1997 +0100
     4.2 +++ b/src/HOLCF/Cprod3.ML	Wed Mar 26 13:44:05 1997 +0100
     4.3 @@ -20,8 +20,8 @@
     4.4  (* ------------------------------------------------------------------------ *)
     4.5  
     4.6  qed_goal "Cprod3_lemma1" Cprod3.thy 
     4.7 -"is_chain(Y::(nat=>'a)) ==>\
     4.8 -\ (lub(range(Y)),(x::'b)) =\
     4.9 +"is_chain(Y::(nat=>'a::cpo)) ==>\
    4.10 +\ (lub(range(Y)),(x::'b::cpo)) =\
    4.11  \ (lub(range(%i. fst(Y i,x))),lub(range(%i. snd(Y i,x))))"
    4.12   (fn prems =>
    4.13          [
    4.14 @@ -57,8 +57,8 @@
    4.15          ]);
    4.16  
    4.17  qed_goal "Cprod3_lemma2" Cprod3.thy 
    4.18 -"is_chain(Y::(nat=>'a)) ==>\
    4.19 -\ ((x::'b),lub(range Y)) =\
    4.20 +"is_chain(Y::(nat=>'a::cpo)) ==>\
    4.21 +\ ((x::'b::cpo),lub(range Y)) =\
    4.22  \ (lub(range(%i. fst(x,Y i))),lub(range(%i. snd(x, Y i))))"
    4.23   (fn prems =>
    4.24          [
     5.1 --- a/src/HOLCF/Cprod3.thy	Tue Mar 25 11:19:09 1997 +0100
     5.2 +++ b/src/HOLCF/Cprod3.thy	Wed Mar 26 13:44:05 1997 +0100
     5.3 @@ -9,7 +9,8 @@
     5.4  
     5.5  Cprod3 = Cprod2 +
     5.6  
     5.7 -instance "*" :: (pcpo,pcpo)pcpo   (least_cprod,cpo_cprod)
     5.8 +instance "*" :: (cpo,cpo)cpo   	  (cpo_cprod)
     5.9 +instance "*" :: (pcpo,pcpo)pcpo   (least_cprod)
    5.10  
    5.11  consts  
    5.12          cpair        :: "'a -> 'b -> ('a*'b)" (* continuous  pairing *)