# HG changeset patch
# User slotosch
# Date 864578725 -7200
# Node ID 9b8e638f8602f0fb86fa7102072edf15f5bdfd94
# Parent  930c9bed5a091d82de2c707fee09a51918fae54b
Eliminated ccc1. Moved ID,oo into Cfun.

diff -r 930c9bed5a09 -r 9b8e638f8602 src/HOLCF/Cfun3.ML
--- a/src/HOLCF/Cfun3.ML	Sun May 25 16:59:40 1997 +0200
+++ b/src/HOLCF/Cfun3.ML	Sun May 25 18:45:25 1997 +0200
@@ -520,3 +520,81 @@
 	(contr_tac 1),(atac 1)
 ]);
 
+
+(* ------------------------------------------------------------------------ *)
+(* Access to definitions                                                    *)
+(* ------------------------------------------------------------------------ *)
+
+
+qed_goalw "ID1" thy [ID_def] "ID`x=x"
+ (fn prems =>
+        [
+        (stac beta_cfun 1),
+        (rtac cont_id 1),
+        (rtac refl 1)
+        ]);
+
+qed_goalw "cfcomp1" thy [oo_def] "(f oo g)=(LAM x.f`(g`x))" (fn _ => [
+        (stac beta_cfun 1),
+        (Simp_tac 1),
+        (stac beta_cfun 1),
+        (Simp_tac 1),
+	(rtac refl 1)
+        ]);
+
+qed_goal "cfcomp2" thy  "(f oo g)`x=f`(g`x)" (fn _ => [
+        (stac cfcomp1 1),
+        (stac beta_cfun 1),
+        (Simp_tac 1),
+	(rtac refl 1)
+        ]);
+
+
+(* ------------------------------------------------------------------------ *)
+(* Show that interpretation of (pcpo,_->_) is a category                    *)
+(* The class of objects is interpretation of syntactical class pcpo         *)
+(* The class of arrows  between objects 'a and 'b is interpret. of 'a -> 'b *)
+(* The identity arrow is interpretation of ID                               *)
+(* The composition of f and g is interpretation of oo                       *)
+(* ------------------------------------------------------------------------ *)
+
+
+qed_goal "ID2" thy "f oo ID = f "
+ (fn prems =>
+        [
+        (rtac ext_cfun 1),
+        (stac cfcomp2 1),
+        (stac ID1 1),
+        (rtac refl 1)
+        ]);
+
+qed_goal "ID3" thy "ID oo f = f "
+ (fn prems =>
+        [
+        (rtac ext_cfun 1),
+        (stac cfcomp2 1),
+        (stac ID1 1),
+        (rtac refl 1)
+        ]);
+
+
+qed_goal "assoc_oo" thy "f oo (g oo h) = (f oo g) oo h"
+ (fn prems =>
+        [
+        (rtac ext_cfun 1),
+        (res_inst_tac [("s","f`(g`(h`x))")] trans  1),
+        (stac cfcomp2 1),
+        (stac cfcomp2 1),
+        (rtac refl 1),
+        (stac cfcomp2 1),
+        (stac cfcomp2 1),
+        (rtac refl 1)
+        ]);
+
+(* ------------------------------------------------------------------------ *)
+(* Merge the different rewrite rules for the simplifier                     *)
+(* ------------------------------------------------------------------------ *)
+
+Addsimps ([ID1,ID2,ID3,cfcomp2]);
+
+
diff -r 930c9bed5a09 -r 9b8e638f8602 src/HOLCF/Cfun3.thy
--- a/src/HOLCF/Cfun3.thy	Sun May 25 16:59:40 1997 +0200
+++ b/src/HOLCF/Cfun3.thy	Sun May 25 18:45:25 1997 +0200
@@ -22,4 +22,17 @@
 Istrictify_def  "Istrictify f x == if x=UU then UU else f`x"    
 strictify_def   "strictify == (LAM f x.Istrictify f x)"
 
+consts
+        ID      :: "('a::cpo) -> 'a"
+        cfcomp  :: "('b->'c)->(('a::cpo)->('b::cpo))->'a->('c::cpo)"
+
+syntax  "@oo"   :: "('b->'c)=>('a->'b)=>'a->'c" ("_ oo _" [101,100] 100)
+     
+translations    "f1 oo f2" == "cfcomp`f1`f2"
+
+defs
+
+  ID_def        "ID ==(LAM x.x)"
+  oo_def        "cfcomp == (LAM f g x.f`(g`x))" 
+
 end
diff -r 930c9bed5a09 -r 9b8e638f8602 src/HOLCF/Fun1.thy
--- a/src/HOLCF/Fun1.thy	Sun May 25 16:59:40 1997 +0200
+++ b/src/HOLCF/Fun1.thy	Sun May 25 18:45:25 1997 +0200
@@ -12,6 +12,8 @@
 
 Fun1 = Pcpo +
 
+instance flat<chfin (flat_imp_chain_finite)
+
 (* to make << defineable: *)
 instance fun  :: (term,sq_ord)sq_ord
 
diff -r 930c9bed5a09 -r 9b8e638f8602 src/HOLCF/HOLCF.thy
--- a/src/HOLCF/HOLCF.thy	Sun May 25 16:59:40 1997 +0200
+++ b/src/HOLCF/HOLCF.thy	Sun May 25 18:45:25 1997 +0200
@@ -8,4 +8,4 @@
 
 *)
 
-HOLCF = Discrete + One + Tr
+HOLCF = Sprod3 + Ssum3 + Up3 + Lift + Discrete + One + Tr
diff -r 930c9bed5a09 -r 9b8e638f8602 src/HOLCF/Lift1.thy
--- a/src/HOLCF/Lift1.thy	Sun May 25 16:59:40 1997 +0200
+++ b/src/HOLCF/Lift1.thy	Sun May 25 18:45:25 1997 +0200
@@ -6,7 +6,7 @@
 Lifting types of class term to flat pcpo's
 *)
 
-Lift1 = ccc1 + 
+Lift1 = Cprod3 + 
 
 default term
 
diff -r 930c9bed5a09 -r 9b8e638f8602 src/HOLCF/Tr.thy
--- a/src/HOLCF/Tr.thy	Sun May 25 16:59:40 1997 +0200
+++ b/src/HOLCF/Tr.thy	Sun May 25 18:45:25 1997 +0200
@@ -6,7 +6,7 @@
 Introduce infix if_then_else_fi and boolean connectives andalso, orelse
 *)
 
-Tr = Lift +
+Tr = Lift + Fix +
 
 types
   tr = "bool lift"
diff -r 930c9bed5a09 -r 9b8e638f8602 src/HOLCF/Up3.ML
--- a/src/HOLCF/Up3.ML	Sun May 25 16:59:40 1997 +0200
+++ b/src/HOLCF/Up3.ML	Sun May 25 18:45:25 1997 +0200
@@ -345,5 +345,4 @@
 (* install simplifier for ('a)u                                             *)
 (* ------------------------------------------------------------------------ *)
 
-val up_rews = [fup1,fup2,defined_up];
-
+Addsimps [fup1,fup2,defined_up];
diff -r 930c9bed5a09 -r 9b8e638f8602 src/HOLCF/ccc1.ML
--- a/src/HOLCF/ccc1.ML	Sun May 25 16:59:40 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,90 +0,0 @@
-(*  Title:      HOLCF/ccc1.ML
-    ID:         $Id$
-    Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
-
-Lemmas for ccc1.thy 
-*)
-
-open ccc1;
-
-
-(* ------------------------------------------------------------------------ *)
-(* Access to definitions                                                    *)
-(* ------------------------------------------------------------------------ *)
-
-
-qed_goalw "ID1" ccc1.thy [ID_def] "ID`x=x"
- (fn prems =>
-        [
-        (stac beta_cfun 1),
-        (rtac cont_id 1),
-        (rtac refl 1)
-        ]);
-
-qed_goalw "cfcomp1" ccc1.thy [oo_def] "(f oo g)=(LAM x.f`(g`x))" (fn _ => [
-        (stac beta_cfun 1),
-        (Simp_tac 1),
-        (stac beta_cfun 1),
-        (Simp_tac 1),
-	(rtac refl 1)
-        ]);
-
-qed_goal "cfcomp2" ccc1.thy  "(f oo g)`x=f`(g`x)" (fn _ => [
-        (stac cfcomp1 1),
-        (stac beta_cfun 1),
-        (Simp_tac 1),
-	(rtac refl 1)
-        ]);
-
-
-(* ------------------------------------------------------------------------ *)
-(* Show that interpretation of (pcpo,_->_) is a category                    *)
-(* The class of objects is interpretation of syntactical class pcpo         *)
-(* The class of arrows  between objects 'a and 'b is interpret. of 'a -> 'b *)
-(* The identity arrow is interpretation of ID                               *)
-(* The composition of f and g is interpretation of oo                       *)
-(* ------------------------------------------------------------------------ *)
-
-
-qed_goal "ID2" ccc1.thy "f oo ID = f "
- (fn prems =>
-        [
-        (rtac ext_cfun 1),
-        (stac cfcomp2 1),
-        (stac ID1 1),
-        (rtac refl 1)
-        ]);
-
-qed_goal "ID3" ccc1.thy "ID oo f = f "
- (fn prems =>
-        [
-        (rtac ext_cfun 1),
-        (stac cfcomp2 1),
-        (stac ID1 1),
-        (rtac refl 1)
-        ]);
-
-
-qed_goal "assoc_oo" ccc1.thy "f oo (g oo h) = (f oo g) oo h"
- (fn prems =>
-        [
-        (rtac ext_cfun 1),
-        (res_inst_tac [("s","f`(g`(h`x))")] trans  1),
-        (stac cfcomp2 1),
-        (stac cfcomp2 1),
-        (rtac refl 1),
-        (stac cfcomp2 1),
-        (stac cfcomp2 1),
-        (rtac refl 1)
-        ]);
-
-(* ------------------------------------------------------------------------ *)
-(* Merge the different rewrite rules for the simplifier                     *)
-(* ------------------------------------------------------------------------ *)
-
-Addsimps (up_rews @ [ID1,ID2,ID3,cfcomp2]);
-
-
-
-
diff -r 930c9bed5a09 -r 9b8e638f8602 src/HOLCF/ccc1.thy
--- a/src/HOLCF/ccc1.thy	Sun May 25 16:59:40 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-(*  Title:      HOLCF/ccc1.thy
-    ID:         $Id$
-    Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
-
-Merge Theories Cprof, Sprod, Ssum, Up, Fix and
-define constants for categorical reasoning
-*)
-
-ccc1 = Cprod3 + Sprod3 + Ssum3 + Up3 + Fix + 
-
-instance flat<chfin (flat_imp_chain_finite)
-
-consts
-        ID      :: "('a::cpo) -> 'a"
-        cfcomp  :: "('b->'c)->(('a::cpo)->('b::cpo))->'a->('c::cpo)"
-
-syntax  "@oo"   :: "('b->'c)=>('a->'b)=>'a->'c" ("_ oo _" [101,100] 100)
-     
-translations    "f1 oo f2" == "cfcomp`f1`f2"
-
-defs
-
-  ID_def        "ID ==(LAM x.x)"
-  oo_def        "cfcomp == (LAM f g x.f`(g`x))" 
-
-end
-
-
-
-