Eliminated ccc1. Moved ID,oo into Cfun.
--- 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]);
+
+
--- 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
--- 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
--- 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
--- 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
--- 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"
--- 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];
--- 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]);
-
-
-
-
--- 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
-
-
-
-