--- a/src/HOLCF/Cfun1.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/Cfun1.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOLCF/cfun1.thy
+(* Title: HOLCF/cfun1.thy
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Definition of the type -> of continuous functions
@@ -14,38 +14,38 @@
types "->" 2 (infixr 5)
-arities "->" :: (pcpo,pcpo)term (* No properties for ->'s range *)
+arities "->" :: (pcpo,pcpo)term (* No properties for ->'s range *)
consts
- Cfun :: "('a => 'b)set"
- fapp :: "('a -> 'b)=>('a => 'b)" (* usually Rep_Cfun *)
- (* application *)
+ Cfun :: "('a => 'b)set"
+ fapp :: "('a -> 'b)=>('a => 'b)" (* usually Rep_Cfun *)
+ (* application *)
- fabs :: "('a => 'b)=>('a -> 'b)" (binder "LAM " 10)
- (* usually Abs_Cfun *)
- (* abstraction *)
+ fabs :: "('a => 'b)=>('a -> 'b)" (binder "LAM " 10)
+ (* usually Abs_Cfun *)
+ (* abstraction *)
- less_cfun :: "[('a -> 'b),('a -> 'b)]=>bool"
+ less_cfun :: "[('a -> 'b),('a -> 'b)]=>bool"
syntax "@fapp" :: "('a -> 'b)=>('a => 'b)" ("_`_" [999,1000] 999)
translations "f`x" == "fapp f x"
defs
- Cfun_def "Cfun == {f. cont(f)}"
+ Cfun_def "Cfun == {f. cont(f)}"
rules
(*faking a type definition... *)
(* -> is isomorphic to Cfun *)
- Rep_Cfun "fapp fo : Cfun"
- Rep_Cfun_inverse "fabs (fapp fo) = fo"
- Abs_Cfun_inverse "f:Cfun ==> fapp(fabs f) = f"
+ Rep_Cfun "fapp fo : Cfun"
+ Rep_Cfun_inverse "fabs (fapp fo) = fo"
+ Abs_Cfun_inverse "f:Cfun ==> fapp(fabs f) = f"
defs
(*defining the abstract constants*)
- less_cfun_def "less_cfun fo1 fo2 == ( fapp fo1 << fapp fo2 )"
+ less_cfun_def "less_cfun fo1 fo2 == ( fapp fo1 << fapp fo2 )"
(* start 8bit 1 *)
(* end 8bit 1 *)
--- a/src/HOLCF/Cfun2.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/Cfun2.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOLCF/cfun2.thy
+(* Title: HOLCF/cfun2.thy
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Class Instance ->::(pcpo,pcpo)po
@@ -12,19 +12,19 @@
(* Witness for the above arity axiom is cfun1.ML *)
arities "->" :: (pcpo,pcpo)po
-consts
- UU_cfun :: "'a->'b"
+consts
+ UU_cfun :: "'a->'b"
rules
(* instance of << for type ['a -> 'b] *)
-inst_cfun_po "((op <<)::['a->'b,'a->'b]=>bool) = less_cfun"
+inst_cfun_po "((op <<)::['a->'b,'a->'b]=>bool) = less_cfun"
defs
(* The least element in type 'a->'b *)
-UU_cfun_def "UU_cfun == fabs(% x.UU)"
+UU_cfun_def "UU_cfun == fabs(% x.UU)"
end
--- a/src/HOLCF/Cfun3.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/Cfun3.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOLCF/cfun3.thy
+(* Title: HOLCF/cfun3.thy
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Class instance of -> for class pcpo
@@ -9,21 +9,21 @@
Cfun3 = Cfun2 +
-arities "->" :: (pcpo,pcpo)pcpo (* Witness cfun2.ML *)
+arities "->" :: (pcpo,pcpo)pcpo (* Witness cfun2.ML *)
consts
- Istrictify :: "('a->'b)=>'a=>'b"
- strictify :: "('a->'b)->'a->'b"
+ Istrictify :: "('a->'b)=>'a=>'b"
+ strictify :: "('a->'b)->'a->'b"
rules
-inst_cfun_pcpo "(UU::'a->'b) = UU_cfun"
+inst_cfun_pcpo "(UU::'a->'b) = UU_cfun"
defs
-Istrictify_def "Istrictify f x == if x=UU then UU else f`x"
+Istrictify_def "Istrictify f x == if x=UU then UU else f`x"
-strictify_def "strictify == (LAM f x.Istrictify f x)"
+strictify_def "strictify == (LAM f x.Istrictify f x)"
end
--- a/src/HOLCF/Cont.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/Cont.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOLCF/cont.thy
+(* Title: HOLCF/cont.thy
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Results about continuity and monotonicity
@@ -19,19 +19,19 @@
default pcpo
consts
- monofun :: "('a::po => 'b::po) => bool" (* monotonicity *)
- contlub :: "('a => 'b) => bool" (* first cont. def *)
- cont :: "('a => 'b) => bool" (* secnd cont. def *)
+ monofun :: "('a::po => 'b::po) => bool" (* monotonicity *)
+ contlub :: "('a => 'b) => bool" (* first cont. def *)
+ cont :: "('a => 'b) => bool" (* secnd cont. def *)
defs
-monofun "monofun(f) == ! x y. x << y --> f(x) << f(y)"
+monofun "monofun(f) == ! x y. x << y --> f(x) << f(y)"
-contlub "contlub(f) == ! Y. is_chain(Y) -->
- f(lub(range(Y))) = lub(range(% i.f(Y(i))))"
+contlub "contlub(f) == ! Y. is_chain(Y) -->
+ f(lub(range(Y))) = lub(range(% i.f(Y(i))))"
-cont "cont(f) == ! Y. is_chain(Y) -->
- range(% i.f(Y(i))) <<| f(lub(range(Y)))"
+cont "cont(f) == ! Y. is_chain(Y) -->
+ range(% i.f(Y(i))) <<| f(lub(range(Y)))"
(* ------------------------------------------------------------------------ *)
(* the main purpose of cont.thy is to show: *)
--- a/src/HOLCF/Cprod1.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/Cprod1.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOLCF/cprod1.thy
+(* Title: HOLCF/cprod1.thy
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
@@ -12,12 +12,12 @@
consts
- less_cprod :: "[('a::pcpo * 'b::pcpo),('a * 'b)] => bool"
+ less_cprod :: "[('a::pcpo * 'b::pcpo),('a * 'b)] => bool"
defs
less_cprod_def "less_cprod p1 p2 == ( fst(p1) << fst(p2) &
- snd(p1) << snd(p2))"
+ snd(p1) << snd(p2))"
end
--- a/src/HOLCF/Cprod2.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/Cprod2.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOLCF/cprod2.thy
+(* Title: HOLCF/cprod2.thy
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Class Instance *::(pcpo,pcpo)po
@@ -17,7 +17,7 @@
(* instance of << for type ['a * 'b] *)
-inst_cprod_po "((op <<)::['a * 'b,'a * 'b]=>bool) = less_cprod"
+inst_cprod_po "((op <<)::['a * 'b,'a * 'b]=>bool) = less_cprod"
end
--- a/src/HOLCF/Cprod3.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/Cprod3.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOLCF/cprod3.thy
+(* Title: HOLCF/cprod3.thy
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
@@ -10,31 +10,31 @@
Cprod3 = Cprod2 +
-arities "*" :: (pcpo,pcpo)pcpo (* Witness cprod2.ML *)
+arities "*" :: (pcpo,pcpo)pcpo (* Witness cprod2.ML *)
consts
- cpair :: "'a -> 'b -> ('a*'b)" (* continuous pairing *)
- cfst :: "('a*'b)->'a"
- csnd :: "('a*'b)->'b"
- csplit :: "('a->'b->'c)->('a*'b)->'c"
+ cpair :: "'a -> 'b -> ('a*'b)" (* continuous pairing *)
+ cfst :: "('a*'b)->'a"
+ csnd :: "('a*'b)->'b"
+ csplit :: "('a->'b->'c)->('a*'b)->'c"
-syntax
- "@ctuple" :: "['a, args] => 'a * 'b" ("(1<_,/ _>)")
+syntax
+ "@ctuple" :: "['a, args] => 'a * 'b" ("(1<_,/ _>)")
translations
- "<x, y, z>" == "<x, <y, z>>"
- "<x, y>" == "cpair`x`y"
+ "<x, y, z>" == "<x, <y, z>>"
+ "<x, y>" == "cpair`x`y"
rules
-inst_cprod_pcpo "(UU::'a*'b) = (UU,UU)"
+inst_cprod_pcpo "(UU::'a*'b) = (UU,UU)"
defs
-cpair_def "cpair == (LAM x y.(x,y))"
-cfst_def "cfst == (LAM p.fst(p))"
-csnd_def "csnd == (LAM p.snd(p))"
-csplit_def "csplit == (LAM f p.f`(cfst`p)`(csnd`p))"
+cpair_def "cpair == (LAM x y.(x,y))"
+cfst_def "cfst == (LAM p.fst(p))"
+csnd_def "csnd == (LAM p.snd(p))"
+csplit_def "csplit == (LAM f p.f`(cfst`p)`(csnd`p))"
--- a/src/HOLCF/Fix.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/Fix.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOLCF/fix.thy
+(* Title: HOLCF/fix.thy
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
@@ -30,7 +30,7 @@
(!i.P(Y i)) --> P(lub(range Y))"
admw_def "admw P == !F. (!n.P (iterate n F UU)) -->
- P (lub(range (%i. iterate i F UU)))"
+ P (lub(range (%i. iterate i F UU)))"
chain_finite_def "chain_finite (x::'a)==
!Y. is_chain (Y::nat=>'a) --> (? n.max_in_chain n Y)"
--- a/src/HOLCF/Fun1.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/Fun1.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOLCF/fun1.thy
+(* Title: HOLCF/fun1.thy
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
@@ -15,7 +15,7 @@
(* default class is still term *)
consts
- less_fun :: "['a=>'b::po,'a=>'b] => bool"
+ less_fun :: "['a=>'b::po,'a=>'b] => bool"
defs
(* definition of the ordering less_fun *)
--- a/src/HOLCF/Fun2.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/Fun2.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOLCF/fun2.thy
+(* Title: HOLCF/fun2.thy
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Class Instance =>::(term,po)po
@@ -15,20 +15,20 @@
arities fun :: (term,po)po
-consts
- UU_fun :: "'a::term => 'b::pcpo"
+consts
+ UU_fun :: "'a::term => 'b::pcpo"
rules
(* instance of << for type ['a::term => 'b::po] *)
-inst_fun_po "((op <<)::['a=>'b::po,'a=>'b::po ]=>bool) = less_fun"
+inst_fun_po "((op <<)::['a=>'b::po,'a=>'b::po ]=>bool) = less_fun"
defs
(* The least element in type 'a::term => 'b::pcpo *)
-UU_fun_def "UU_fun == (% x.UU)"
+UU_fun_def "UU_fun == (% x.UU)"
end
--- a/src/HOLCF/Fun3.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/Fun3.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOLCF/fun3.thy
+(* Title: HOLCF/fun3.thy
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Class instance of => (fun) for class pcpo
@@ -11,11 +11,11 @@
(* default class is still term *)
-arities fun :: (term,pcpo)pcpo (* Witness fun2.ML *)
+arities fun :: (term,pcpo)pcpo (* Witness fun2.ML *)
rules
-inst_fun_pcpo "(UU::'a=>'b::pcpo) = UU_fun"
+inst_fun_pcpo "(UU::'a=>'b::pcpo) = UU_fun"
end
--- a/src/HOLCF/HOLCF.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/HOLCF.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOLCF/HOLCF.thy
+(* Title: HOLCF/HOLCF.thy
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
--- a/src/HOLCF/Holcfb.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/Holcfb.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOLCF/holcfb.thy
+(* Title: HOLCF/holcfb.thy
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Basic definitions for the embedding of LCF into HOL.
@@ -10,7 +10,7 @@
Holcfb = Nat +
consts
- theleast :: "(nat=>bool)=>nat"
+ theleast :: "(nat=>bool)=>nat"
defs
theleast_def "theleast P == (@z.(P z & (!n.P n --> z<=n)))"
--- a/src/HOLCF/Lift1.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/Lift1.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOLCF/Lift1.thy
+(* Title: HOLCF/Lift1.thy
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
@@ -14,12 +14,12 @@
types "u" 1
-arities "u" :: (pcpo)term
+arities "u" :: (pcpo)term
consts
- Rep_Lift :: "('a)u => (void + 'a)"
- Abs_Lift :: "(void + 'a) => ('a)u"
+ Rep_Lift :: "('a)u => (void + 'a)"
+ Abs_Lift :: "(void + 'a) => ('a)u"
Iup :: "'a => ('a)u"
UU_lift :: "('a)u"
@@ -31,8 +31,8 @@
(*faking a type definition... *)
(* ('a)u is isomorphic to void + 'a *)
- Rep_Lift_inverse "Abs_Lift(Rep_Lift(p)) = p"
- Abs_Lift_inverse "Rep_Lift(Abs_Lift(p)) = p"
+ Rep_Lift_inverse "Abs_Lift(Rep_Lift(p)) = p"
+ Abs_Lift_inverse "Rep_Lift(Abs_Lift(p)) = p"
(*defining the abstract constants*)
@@ -43,11 +43,11 @@
Ilift_def "Ilift(f)(x)==
case Rep_Lift(x) of Inl(y) => UU | Inr(z) => f`z"
- less_lift_def "less_lift(x1)(x2) ==
- (case Rep_Lift(x1) of
- Inl(y1) => True
- | Inr(y2) =>
- (case Rep_Lift(x2) of Inl(z1) => False
+ less_lift_def "less_lift(x1)(x2) ==
+ (case Rep_Lift(x1) of
+ Inl(y1) => True
+ | Inr(y2) =>
+ (case Rep_Lift(x2) of Inl(z1) => False
| Inr(z2) => y2<<z2))"
end
--- a/src/HOLCF/Lift2.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/Lift2.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOLCF/lift2.thy
+(* Title: HOLCF/lift2.thy
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Class Instance u::(pcpo)po
@@ -17,7 +17,7 @@
(* instance of << for type ('a)u *)
-inst_lift_po "((op <<)::[('a)u,('a)u]=>bool) = less_lift"
+inst_lift_po "((op <<)::[('a)u,('a)u]=>bool) = less_lift"
end
--- a/src/HOLCF/Lift3.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/Lift3.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOLCF/lift3.thy
+(* Title: HOLCF/lift3.thy
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
@@ -10,19 +10,19 @@
Lift3 = Lift2 +
-arities "u" :: (pcpo)pcpo (* Witness lift2.ML *)
+arities "u" :: (pcpo)pcpo (* Witness lift2.ML *)
consts
- up :: "'a -> ('a)u"
- lift :: "('a->'c)-> ('a)u -> 'c"
+ up :: "'a -> ('a)u"
+ lift :: "('a->'c)-> ('a)u -> 'c"
rules
- inst_lift_pcpo "(UU::('a)u) = UU_lift"
+ inst_lift_pcpo "(UU::('a)u) = UU_lift"
defs
- up_def "up == (LAM x.Iup(x))"
- lift_def "lift == (LAM f p.Ilift(f)(p))"
+ up_def "up == (LAM x.Iup(x))"
+ lift_def "lift == (LAM f p.Ilift(f)(p))"
translations
"case l of up`x => t1" == "lift`(LAM x.t1)`l"
--- a/src/HOLCF/One.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/One.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOLCF/one.thy
+(* Title: HOLCF/one.thy
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Introduce atomic type one = (void)u
@@ -23,17 +23,17 @@
arities one :: pcpo
consts
- abs_one :: "(void)u -> one"
- rep_one :: "one -> (void)u"
- one :: "one"
- one_when :: "'c -> one -> 'c"
+ abs_one :: "(void)u -> one"
+ rep_one :: "one -> (void)u"
+ one :: "one"
+ one_when :: "'c -> one -> 'c"
rules
- abs_one_iso "abs_one`(rep_one`u) = u"
- rep_one_iso "rep_one`(abs_one`x) = x"
+ abs_one_iso "abs_one`(rep_one`u) = u"
+ rep_one_iso "rep_one`(abs_one`x) = x"
defs
- one_def "one == abs_one`(up`UU)"
+ one_def "one == abs_one`(up`UU)"
one_when_def "one_when == (LAM c u.lift`(LAM x.c)`(rep_one`u))"
translations
--- a/src/HOLCF/Pcpo.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/Pcpo.thy Tue Feb 06 12:42:31 1996 +0100
@@ -3,15 +3,15 @@
classes pcpo < po
arities void :: pcpo
-consts
- UU :: "'a::pcpo"
+consts
+ UU :: "'a::pcpo"
rules
- minimal "UU << x"
- cpo "is_chain(S) ==> ? x. range(S) <<| (x::'a::pcpo)"
+ minimal "UU << x"
+ cpo "is_chain(S) ==> ? x. range(S) <<| (x::'a::pcpo)"
-inst_void_pcpo "(UU::void) = UU_void"
+inst_void_pcpo "(UU::void) = UU_void"
(* start 8bit 1 *)
(* end 8bit 1 *)
--- a/src/HOLCF/Porder.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/Porder.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOLCF/porder.thy
+(* Title: HOLCF/porder.thy
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Conservative extension of theory Porder0 by constant definitions
@@ -9,28 +9,28 @@
Porder = Porder0 +
-consts
- "<|" :: "['a set,'a::po] => bool" (infixl 55)
- "<<|" :: "['a set,'a::po] => bool" (infixl 55)
- lub :: "'a set => 'a::po"
- is_tord :: "'a::po set => bool"
- is_chain :: "(nat=>'a::po) => bool"
- max_in_chain :: "[nat,nat=>'a::po]=>bool"
- finite_chain :: "(nat=>'a::po)=>bool"
+consts
+ "<|" :: "['a set,'a::po] => bool" (infixl 55)
+ "<<|" :: "['a set,'a::po] => bool" (infixl 55)
+ lub :: "'a set => 'a::po"
+ is_tord :: "'a::po set => bool"
+ is_chain :: "(nat=>'a::po) => bool"
+ max_in_chain :: "[nat,nat=>'a::po]=>bool"
+ finite_chain :: "(nat=>'a::po)=>bool"
defs
(* class definitions *)
-is_ub "S <| x == ! y.y:S --> y<<x"
-is_lub "S <<| x == S <| x & (! u. S <| u --> x << u)"
+is_ub "S <| x == ! y.y:S --> y<<x"
+is_lub "S <<| x == S <| x & (! u. S <| u --> x << u)"
(* Arbitrary chains are total orders *)
-is_tord "is_tord(S) == ! x y. x:S & y:S --> (x<<y | y<<x)"
+is_tord "is_tord(S) == ! x y. x:S & y:S --> (x<<y | y<<x)"
(* Here we use countable chains and I prefer to code them as functions! *)
-is_chain "is_chain(F) == (! i.F(i) << F(Suc(i)))"
+is_chain "is_chain(F) == (! i.F(i) << F(Suc(i)))"
(* finite chains, needed for monotony of continouous functions *)
@@ -40,7 +40,7 @@
rules
-lub "lub(S) = (@x. S <<| x)"
+lub "lub(S) = (@x. S <<| x)"
(* start 8bit 1 *)
(* end 8bit 1 *)
--- a/src/HOLCF/Porder0.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/Porder0.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOLCF/porder0.thy
+(* Title: HOLCF/porder0.thy
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Definition of class porder (partial order)
@@ -20,24 +20,24 @@
arities void :: po
-consts "<<" :: "['a,'a::po] => bool" (infixl 55)
+consts "<<" :: "['a,'a::po] => bool" (infixl 55)
rules
(* class axioms: justification is theory Void *)
-refl_less "x << x"
- (* witness refl_less_void *)
+refl_less "x << x"
+ (* witness refl_less_void *)
-antisym_less "[|x<<y ; y<<x |] ==> x = y"
- (* witness antisym_less_void *)
+antisym_less "[|x<<y ; y<<x |] ==> x = y"
+ (* witness antisym_less_void *)
-trans_less "[|x<<y ; y<<z |] ==> x<<z"
- (* witness trans_less_void *)
+trans_less "[|x<<y ; y<<z |] ==> x<<z"
+ (* witness trans_less_void *)
(* instance of << for the prototype void *)
-inst_void_po "((op <<)::[void,void]=>bool) = less_void"
+inst_void_po "((op <<)::[void,void]=>bool) = less_void"
(* start 8bit 1 *)
(* end 8bit 1 *)
--- a/src/HOLCF/Sprod0.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/Sprod0.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOLCF/sprod0.thy
+(* Title: HOLCF/sprod0.thy
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Strict product
@@ -12,43 +12,43 @@
types "**" 2 (infixr 20)
-arities "**" :: (pcpo,pcpo)term
+arities "**" :: (pcpo,pcpo)term
consts
- Sprod :: "('a => 'b => bool)set"
- Spair_Rep :: "['a,'b] => ['a,'b] => bool"
- Rep_Sprod :: "('a ** 'b) => ('a => 'b => bool)"
- Abs_Sprod :: "('a => 'b => bool) => ('a ** 'b)"
- Ispair :: "['a,'b] => ('a ** 'b)"
- Isfst :: "('a ** 'b) => 'a"
- Issnd :: "('a ** 'b) => 'b"
+ Sprod :: "('a => 'b => bool)set"
+ Spair_Rep :: "['a,'b] => ['a,'b] => bool"
+ Rep_Sprod :: "('a ** 'b) => ('a => 'b => bool)"
+ Abs_Sprod :: "('a => 'b => bool) => ('a ** 'b)"
+ Ispair :: "['a,'b] => ('a ** 'b)"
+ Isfst :: "('a ** 'b) => 'a"
+ Issnd :: "('a ** 'b) => 'b"
defs
- Spair_Rep_def "Spair_Rep == (%a b. %x y.
- (~a=UU & ~b=UU --> x=a & y=b ))"
+ Spair_Rep_def "Spair_Rep == (%a b. %x y.
+ (~a=UU & ~b=UU --> x=a & y=b ))"
- Sprod_def "Sprod == {f. ? a b. f = Spair_Rep a b}"
+ Sprod_def "Sprod == {f. ? a b. f = Spair_Rep a b}"
rules
(*faking a type definition... *)
(* "**" is isomorphic to Sprod *)
- Rep_Sprod "Rep_Sprod(p):Sprod"
- Rep_Sprod_inverse "Abs_Sprod(Rep_Sprod(p)) = p"
- Abs_Sprod_inverse "f:Sprod ==> Rep_Sprod(Abs_Sprod(f)) = f"
+ Rep_Sprod "Rep_Sprod(p):Sprod"
+ Rep_Sprod_inverse "Abs_Sprod(Rep_Sprod(p)) = p"
+ Abs_Sprod_inverse "f:Sprod ==> Rep_Sprod(Abs_Sprod(f)) = f"
defs
(*defining the abstract constants*)
- Ispair_def "Ispair a b == Abs_Sprod(Spair_Rep a b)"
+ Ispair_def "Ispair a b == Abs_Sprod(Spair_Rep a b)"
- Isfst_def "Isfst(p) == @z.
- (p=Ispair UU UU --> z=UU)
- &(! a b. ~a=UU & ~b=UU & p=Ispair a b --> z=a)"
+ Isfst_def "Isfst(p) == @z.
+ (p=Ispair UU UU --> z=UU)
+ &(! a b. ~a=UU & ~b=UU & p=Ispair a b --> z=a)"
- Issnd_def "Issnd(p) == @z.
- (p=Ispair UU UU --> z=UU)
- &(! a b. ~a=UU & ~b=UU & p=Ispair a b --> z=b)"
+ Issnd_def "Issnd(p) == @z.
+ (p=Ispair UU UU --> z=UU)
+ &(! a b. ~a=UU & ~b=UU & p=Ispair a b --> z=b)"
(* start 8bit 1 *)
(* end 8bit 1 *)
--- a/src/HOLCF/Sprod1.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/Sprod1.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOLCF/sprod1.thy
+(* Title: HOLCF/sprod1.thy
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Partial ordering for the strict product
@@ -9,12 +9,12 @@
Sprod1 = Sprod0 +
consts
- less_sprod :: "[('a ** 'b),('a ** 'b)] => bool"
+ less_sprod :: "[('a ** 'b),('a ** 'b)] => bool"
defs
less_sprod_def "less_sprod p1 p2 ==
- if p1 = Ispair UU UU
- then True
- else Isfst p1 << Isfst p2 & Issnd p1 << Issnd p2"
+ if p1 = Ispair UU UU
+ then True
+ else Isfst p1 << Isfst p2 & Issnd p1 << Issnd p2"
end
--- a/src/HOLCF/Sprod2.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/Sprod2.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOLCF/sprod2.thy
+(* Title: HOLCF/sprod2.thy
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Class Instance **::(pcpo,pcpo)po
@@ -16,7 +16,7 @@
(* instance of << for type ['a ** 'b] *)
-inst_sprod_po "((op <<)::['a ** 'b,'a ** 'b]=>bool) = less_sprod"
+inst_sprod_po "((op <<)::['a ** 'b,'a ** 'b]=>bool) = less_sprod"
end
--- a/src/HOLCF/Sprod3.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/Sprod3.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOLCF/sprod3.thy
+(* Title: HOLCF/sprod3.thy
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Class instance of ** for class pcpo
@@ -8,30 +8,30 @@
Sprod3 = Sprod2 +
-arities "**" :: (pcpo,pcpo)pcpo (* Witness sprod2.ML *)
+arities "**" :: (pcpo,pcpo)pcpo (* Witness sprod2.ML *)
consts
- spair :: "'a -> 'b -> ('a**'b)" (* continuous strict pairing *)
- sfst :: "('a**'b)->'a"
- ssnd :: "('a**'b)->'b"
- ssplit :: "('a->'b->'c)->('a**'b)->'c"
+ spair :: "'a -> 'b -> ('a**'b)" (* continuous strict pairing *)
+ sfst :: "('a**'b)->'a"
+ ssnd :: "('a**'b)->'b"
+ ssplit :: "('a->'b->'c)->('a**'b)->'c"
syntax
- "@stuple" :: "['a, args] => 'a ** 'b" ("(1'(|_,/ _|'))")
+ "@stuple" :: "['a, args] => 'a ** 'b" ("(1'(|_,/ _|'))")
translations
- "(|x, y, z|)" == "(|x, (|y, z|)|)"
- "(|x, y|)" == "spair`x`y"
+ "(|x, y, z|)" == "(|x, (|y, z|)|)"
+ "(|x, y|)" == "spair`x`y"
rules
-inst_sprod_pcpo "(UU::'a**'b) = Ispair UU UU"
+inst_sprod_pcpo "(UU::'a**'b) = Ispair UU UU"
defs
-spair_def "spair == (LAM x y.Ispair x y)"
-sfst_def "sfst == (LAM p.Isfst p)"
-ssnd_def "ssnd == (LAM p.Issnd p)"
-ssplit_def "ssplit == (LAM f. strictify`(LAM p.f`(sfst`p)`(ssnd`p)))"
+spair_def "spair == (LAM x y.Ispair x y)"
+sfst_def "sfst == (LAM p.Isfst p)"
+ssnd_def "ssnd == (LAM p.Issnd p)"
+ssplit_def "ssplit == (LAM f. strictify`(LAM p.f`(sfst`p)`(ssnd`p)))"
(* start 8bit 1 *)
(* end 8bit 1 *)
--- a/src/HOLCF/Ssum0.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/Ssum0.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOLCF/ssum0.thy
+(* Title: HOLCF/ssum0.thy
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Strict sum
@@ -12,44 +12,44 @@
types "++" 2 (infixr 10)
-arities "++" :: (pcpo,pcpo)term
+arities "++" :: (pcpo,pcpo)term
consts
- Ssum :: "(['a,'b,bool]=>bool)set"
- Sinl_Rep :: "['a,'a,'b,bool]=>bool"
- Sinr_Rep :: "['b,'a,'b,bool]=>bool"
- Rep_Ssum :: "('a ++ 'b) => (['a,'b,bool]=>bool)"
- Abs_Ssum :: "(['a,'b,bool]=>bool) => ('a ++ 'b)"
- Isinl :: "'a => ('a ++ 'b)"
- Isinr :: "'b => ('a ++ 'b)"
- Iwhen :: "('a->'c)=>('b->'c)=>('a ++ 'b)=> 'c"
+ Ssum :: "(['a,'b,bool]=>bool)set"
+ Sinl_Rep :: "['a,'a,'b,bool]=>bool"
+ Sinr_Rep :: "['b,'a,'b,bool]=>bool"
+ Rep_Ssum :: "('a ++ 'b) => (['a,'b,bool]=>bool)"
+ Abs_Ssum :: "(['a,'b,bool]=>bool) => ('a ++ 'b)"
+ Isinl :: "'a => ('a ++ 'b)"
+ Isinr :: "'b => ('a ++ 'b)"
+ Iwhen :: "('a->'c)=>('b->'c)=>('a ++ 'b)=> 'c"
defs
- Sinl_Rep_def "Sinl_Rep == (%a.%x y p.
- (a~=UU --> x=a & p))"
+ Sinl_Rep_def "Sinl_Rep == (%a.%x y p.
+ (a~=UU --> x=a & p))"
- Sinr_Rep_def "Sinr_Rep == (%b.%x y p.
- (b~=UU --> y=b & ~p))"
+ Sinr_Rep_def "Sinr_Rep == (%b.%x y p.
+ (b~=UU --> y=b & ~p))"
- Ssum_def "Ssum =={f.(? a.f=Sinl_Rep(a))|(? b.f=Sinr_Rep(b))}"
+ Ssum_def "Ssum =={f.(? a.f=Sinl_Rep(a))|(? b.f=Sinr_Rep(b))}"
rules
(*faking a type definition... *)
(* "++" is isomorphic to Ssum *)
- Rep_Ssum "Rep_Ssum(p):Ssum"
- Rep_Ssum_inverse "Abs_Ssum(Rep_Ssum(p)) = p"
- Abs_Ssum_inverse "f:Ssum ==> Rep_Ssum(Abs_Ssum(f)) = f"
+ Rep_Ssum "Rep_Ssum(p):Ssum"
+ Rep_Ssum_inverse "Abs_Ssum(Rep_Ssum(p)) = p"
+ Abs_Ssum_inverse "f:Ssum ==> Rep_Ssum(Abs_Ssum(f)) = f"
defs (*defining the abstract constants*)
- Isinl_def "Isinl(a) == Abs_Ssum(Sinl_Rep(a))"
- Isinr_def "Isinr(b) == Abs_Ssum(Sinr_Rep(b))"
+ Isinl_def "Isinl(a) == Abs_Ssum(Sinl_Rep(a))"
+ Isinr_def "Isinr(b) == Abs_Ssum(Sinr_Rep(b))"
- Iwhen_def "Iwhen(f)(g)(s) == @z.
- (s=Isinl(UU) --> z=UU)
- &(!a. a~=UU & s=Isinl(a) --> z=f`a)
- &(!b. b~=UU & s=Isinr(b) --> z=g`b)"
+ Iwhen_def "Iwhen(f)(g)(s) == @z.
+ (s=Isinl(UU) --> z=UU)
+ &(!a. a~=UU & s=Isinl(a) --> z=f`a)
+ &(!b. b~=UU & s=Isinr(b) --> z=g`b)"
(* start 8bit 1 *)
(* end 8bit 1 *)
--- a/src/HOLCF/Ssum1.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/Ssum1.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOLCF/ssum1.thy
+(* Title: HOLCF/ssum1.thy
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Partial ordering for the strict sum ++
@@ -10,15 +10,15 @@
consts
- less_ssum :: "[('a ++ 'b),('a ++ 'b)] => bool"
+ less_ssum :: "[('a ++ 'b),('a ++ 'b)] => bool"
rules
less_ssum_def "less_ssum s1 s2 == (@z.
- (! u x.s1=Isinl(u) & s2=Isinl(x) --> z = (u << x))
- &(! v y.s1=Isinr(v) & s2=Isinr(y) --> z = (v << y))
- &(! u y.s1=Isinl(u) & s2=Isinr(y) --> z = (u = UU))
- &(! v x.s1=Isinr(v) & s2=Isinl(x) --> z = (v = UU)))"
+ (! u x.s1=Isinl(u) & s2=Isinl(x) --> z = (u << x))
+ &(! v y.s1=Isinr(v) & s2=Isinr(y) --> z = (v << y))
+ &(! u y.s1=Isinl(u) & s2=Isinr(y) --> z = (u = UU))
+ &(! v x.s1=Isinr(v) & s2=Isinl(x) --> z = (v = UU)))"
end
--- a/src/HOLCF/Ssum2.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/Ssum2.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOLCF/ssum2.thy
+(* Title: HOLCF/ssum2.thy
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Class Instance ++::(pcpo,pcpo)po
@@ -15,7 +15,7 @@
(* instance of << for type ['a ++ 'b] *)
-inst_ssum_po "((op <<)::['a ++ 'b,'a ++ 'b]=>bool) = less_ssum"
+inst_ssum_po "((op <<)::['a ++ 'b,'a ++ 'b]=>bool) = less_ssum"
end
--- a/src/HOLCF/Ssum3.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/Ssum3.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOLCF/ssum3.thy
+(* Title: HOLCF/ssum3.thy
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Class instance of ++ for class pcpo
@@ -8,23 +8,23 @@
Ssum3 = Ssum2 +
-arities "++" :: (pcpo,pcpo)pcpo (* Witness ssum2.ML *)
+arities "++" :: (pcpo,pcpo)pcpo (* Witness ssum2.ML *)
consts
- sinl :: "'a -> ('a++'b)"
- sinr :: "'b -> ('a++'b)"
- sswhen :: "('a->'c)->('b->'c)->('a ++ 'b)-> 'c"
+ sinl :: "'a -> ('a++'b)"
+ sinr :: "'b -> ('a++'b)"
+ sswhen :: "('a->'c)->('b->'c)->('a ++ 'b)-> 'c"
rules
-inst_ssum_pcpo "(UU::'a++'b) = Isinl(UU)"
+inst_ssum_pcpo "(UU::'a++'b) = Isinl(UU)"
defs
-sinl_def "sinl == (LAM x.Isinl(x))"
-sinr_def "sinr == (LAM x.Isinr(x))"
-sswhen_def "sswhen == (LAM f g s.Iwhen(f)(g)(s))"
+sinl_def "sinl == (LAM x.Isinl(x))"
+sinr_def "sinr == (LAM x.Isinr(x))"
+sswhen_def "sswhen == (LAM f g s.Iwhen(f)(g)(s))"
translations
"case s of sinl`x => t1 | sinr`y => t2" == "sswhen`(LAM x.t1)`(LAM y.t2)`s"
--- a/src/HOLCF/Tr1.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/Tr1.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOLCF/tr1.thy
+(* Title: HOLCF/tr1.thy
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Introduce the domain of truth values tr = one ++ one
@@ -23,24 +23,24 @@
arities tr :: pcpo
consts
- abs_tr :: "one ++ one -> tr"
- rep_tr :: "tr -> one ++ one"
- TT :: "tr"
- FF :: "tr"
- tr_when :: "'c -> 'c -> tr -> 'c"
+ abs_tr :: "one ++ one -> tr"
+ rep_tr :: "tr -> one ++ one"
+ TT :: "tr"
+ FF :: "tr"
+ tr_when :: "'c -> 'c -> tr -> 'c"
rules
- abs_tr_iso "abs_tr`(rep_tr`u) = u"
- rep_tr_iso "rep_tr`(abs_tr`x) = x"
+ abs_tr_iso "abs_tr`(rep_tr`u) = u"
+ rep_tr_iso "rep_tr`(abs_tr`x) = x"
defs
- TT_def "TT == abs_tr`(sinl`one)"
- FF_def "FF == abs_tr`(sinr`one)"
+ TT_def "TT == abs_tr`(sinl`one)"
+ FF_def "FF == abs_tr`(sinr`one)"
tr_when_def "tr_when ==
- (LAM e1 e2 t. sswhen`(LAM x.e1)`(LAM y.e2)`(rep_tr`t))"
+ (LAM e1 e2 t. sswhen`(LAM x.e1)`(LAM y.e2)`(rep_tr`t))"
(* start 8bit 1 *)
(* end 8bit 1 *)
--- a/src/HOLCF/Tr2.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/Tr2.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOLCF/tr2.thy
+(* Title: HOLCF/tr2.thy
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Introduce infix if_then_else_fi and boolean connectives andalso, orelse
@@ -9,15 +9,15 @@
Tr2 = Tr1 +
consts
- Icifte :: "tr -> 'c -> 'c -> 'c"
- trand :: "tr -> tr -> tr"
- tror :: "tr -> tr -> tr"
- neg :: "tr -> tr"
+ Icifte :: "tr -> 'c -> 'c -> 'c"
+ trand :: "tr -> tr -> tr"
+ tror :: "tr -> tr -> tr"
+ neg :: "tr -> tr"
-syntax "@cifte" :: "tr=>'c=>'c=>'c"
+syntax "@cifte" :: "tr=>'c=>'c=>'c"
("(3If _/ (then _/ else _) fi)" 60)
- "@andalso" :: "tr => tr => tr" ("_ andalso _" [36,35] 35)
- "@orelse" :: "tr => tr => tr" ("_ orelse _" [31,30] 30)
+ "@andalso" :: "tr => tr => tr" ("_ andalso _" [36,35] 35)
+ "@orelse" :: "tr => tr => tr" ("_ orelse _" [31,30] 30)
translations "x andalso y" == "trand`x`y"
"x orelse y" == "tror`x`y"
--- a/src/HOLCF/Void.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/Void.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOLCF/void.thy
+(* Title: HOLCF/void.thy
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Definition of type void with partial order. Void is the prototype for
@@ -16,23 +16,23 @@
arities void :: term
consts
- Void :: "bool set"
- UU_void_Rep :: "bool"
- Rep_Void :: "void => bool"
- Abs_Void :: "bool => void"
- UU_void :: "void"
- less_void :: "[void,void] => bool"
+ Void :: "bool set"
+ UU_void_Rep :: "bool"
+ Rep_Void :: "void => bool"
+ Abs_Void :: "bool => void"
+ UU_void :: "void"
+ less_void :: "[void,void] => bool"
defs
(* The unique element in Void is False:bool *)
- UU_void_Rep_def "UU_void_Rep == False"
- Void_def "Void == {x. x = UU_void_Rep}"
+ UU_void_Rep_def "UU_void_Rep == False"
+ Void_def "Void == {x. x = UU_void_Rep}"
(*defining the abstract constants*)
- UU_void_def "UU_void == Abs_Void(UU_void_Rep)"
+ UU_void_def "UU_void == Abs_Void(UU_void_Rep)"
less_void_def "less_void x y == (Rep_Void x = Rep_Void y)"
rules
@@ -40,9 +40,9 @@
(*faking a type definition... *)
(* void is isomorphic to Void *)
- Rep_Void "Rep_Void(x):Void"
- Rep_Void_inverse "Abs_Void(Rep_Void(x)) = x"
- Abs_Void_inverse "y:Void ==> Rep_Void(Abs_Void(y)) = y"
+ Rep_Void "Rep_Void(x):Void"
+ Rep_Void_inverse "Abs_Void(Rep_Void(x)) = x"
+ Abs_Void_inverse "y:Void ==> Rep_Void(Abs_Void(y)) = y"
end
--- a/src/HOLCF/ccc1.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/ccc1.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOLCF/ccc1.thy
+(* Title: HOLCF/ccc1.thy
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Merge Theories Cprof, Sprod, Ssum, Lift, Fix and
@@ -10,17 +10,17 @@
ccc1 = Cprod3 + Sprod3 + Ssum3 + Lift3 + Fix +
consts
- ID :: "'a -> 'a"
- cfcomp :: "('b->'c)->('a->'b)->'a->'c"
+ ID :: "'a -> 'a"
+ cfcomp :: "('b->'c)->('a->'b)->'a->'c"
-syntax "@oo" :: "('b->'c)=>('a->'b)=>'a->'c" ("_ oo _" [101,100] 100)
+syntax "@oo" :: "('b->'c)=>('a->'b)=>'a->'c" ("_ oo _" [101,100] 100)
-translations "f1 oo f2" == "cfcomp`f1`f2"
+translations "f1 oo f2" == "cfcomp`f1`f2"
defs
- ID_def "ID ==(LAM x.x)"
- oo_def "cfcomp == (LAM f g x.f`(g`x))"
+ ID_def "ID ==(LAM x.x)"
+ oo_def "cfcomp == (LAM f g x.f`(g`x))"
end
--- a/src/HOLCF/ex/Fix2.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/ex/Fix2.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,7 +1,7 @@
-(* Title: HOLCF/ex/Fix2.thy
+(* Title: HOLCF/ex/Fix2.thy
ID: $Id$
- Author: Franz Regensburger
- Copyright 1995 Technische Universitaet Muenchen
+ Author: Franz Regensburger
+ Copyright 1995 Technische Universitaet Muenchen
Show that fix is the unique least fixed-point operator.
From axioms gix1_def,gix2_def it follows that fix = gix
--- a/src/HOLCF/ex/Hoare.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/ex/Hoare.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,7 +1,7 @@
-(* Title: HOLCF/ex/hoare.thy
+(* Title: HOLCF/ex/hoare.thy
ID: $Id$
- Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ Author: Franz Regensburger
+ Copyright 1993 Technische Universitaet Muenchen
Theory for an example by C.A.R. Hoare
@@ -24,11 +24,11 @@
Hoare = Tr2 +
consts
- b1:: "'a -> tr"
- b2:: "'a -> tr"
- g:: "'a -> 'a"
- p :: "'a -> 'a"
- q :: "'a -> 'a"
+ b1:: "'a -> tr"
+ b2:: "'a -> tr"
+ g:: "'a -> 'a"
+ p :: "'a -> 'a"
+ q :: "'a -> 'a"
defs
--- a/src/HOLCF/ex/Loop.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/ex/Loop.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,7 +1,7 @@
-(* Title: HOLCF/ex/Loop.thy
+(* Title: HOLCF/ex/Loop.thy
ID: $Id$
- Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ Author: Franz Regensburger
+ Copyright 1993 Technische Universitaet Muenchen
Theory for a loop primitive like while
*)
@@ -10,13 +10,13 @@
consts
- step :: "('a -> tr)->('a -> 'a)->'a->'a"
- while :: "('a -> tr)->('a -> 'a)->'a->'a"
+ step :: "('a -> tr)->('a -> 'a)->'a->'a"
+ while :: "('a -> tr)->('a -> 'a)->'a->'a"
defs
- step_def "step == (LAM b g x. If b`x then g`x else x fi)"
- while_def "while == (LAM b g. fix`(LAM f x.
+ step_def "step == (LAM b g x. If b`x then g`x else x fi)"
+ while_def "while == (LAM b g. fix`(LAM f x.
If b`x then f`(g`x) else x fi))"
end
--- a/src/HOLCF/explicit_domains/Coind.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/explicit_domains/Coind.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOLCF/Coind.thy
+(* Title: HOLCF/Coind.thy
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Example for co-induction on streams
@@ -11,23 +11,23 @@
consts
- nats :: "dnat stream"
- from :: "dnat -> dnat stream"
+ nats :: "dnat stream"
+ from :: "dnat -> dnat stream"
defs
- nats_def "nats == fix`(LAM h.scons`dzero`(smap`dsucc`h))"
+ nats_def "nats == fix`(LAM h.scons`dzero`(smap`dsucc`h))"
- from_def "from == fix`(LAM h n.scons`n`(h`(dsucc`n)))"
+ from_def "from == fix`(LAM h n.scons`n`(h`(dsucc`n)))"
end
(*
- smap`f`UU = UU
+ smap`f`UU = UU
x~=UU --> smap`f`(scons`x`xs) = scons`(f`x)`(smap`f`xs)
- nats = scons`dzero`(smap`dsucc`nats)
+ nats = scons`dzero`(smap`dsucc`nats)
- from`n = scons`n`(from`(dsucc`n))
+ from`n = scons`n`(from`(dsucc`n))
*)
--- a/src/HOLCF/explicit_domains/Dagstuhl.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/explicit_domains/Dagstuhl.thy Tue Feb 06 12:42:31 1996 +0100
@@ -4,7 +4,7 @@
Dagstuhl = Stream2 +
consts
- y :: "'a"
+ y :: "'a"
YS :: "'a stream"
YYS :: "'a stream"
--- a/src/HOLCF/explicit_domains/Dlist.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/explicit_domains/Dlist.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOLCF/Dlist.thy
+(* Title: HOLCF/Dlist.thy
- Author: Franz Regensburger
+ Author: Franz Regensburger
ID: $ $
Copyright 1994 Technische Universitaet Muenchen
@@ -34,24 +34,24 @@
(* ----------------------------------------------------------------------- *)
(* essential constants *)
-dlist_rep :: "('a dlist) -> (one ++ 'a ** 'a dlist)"
-dlist_abs :: "(one ++ 'a ** 'a dlist) -> ('a dlist)"
+dlist_rep :: "('a dlist) -> (one ++ 'a ** 'a dlist)"
+dlist_abs :: "(one ++ 'a ** 'a dlist) -> ('a dlist)"
(* ----------------------------------------------------------------------- *)
(* abstract constants and auxiliary constants *)
-dlist_copy :: "('a dlist -> 'a dlist) ->'a dlist -> 'a dlist"
+dlist_copy :: "('a dlist -> 'a dlist) ->'a dlist -> 'a dlist"
dnil :: "'a dlist"
-dcons :: "'a -> 'a dlist -> 'a dlist"
-dlist_when :: " 'b -> ('a -> 'a dlist -> 'b) -> 'a dlist -> 'b"
-is_dnil :: "'a dlist -> tr"
-is_dcons :: "'a dlist -> tr"
-dhd :: "'a dlist -> 'a"
-dtl :: "'a dlist -> 'a dlist"
-dlist_take :: "nat => 'a dlist -> 'a dlist"
-dlist_finite :: "'a dlist => bool"
-dlist_bisim :: "('a dlist => 'a dlist => bool) => bool"
+dcons :: "'a -> 'a dlist -> 'a dlist"
+dlist_when :: " 'b -> ('a -> 'a dlist -> 'b) -> 'a dlist -> 'b"
+is_dnil :: "'a dlist -> tr"
+is_dcons :: "'a dlist -> tr"
+dhd :: "'a dlist -> 'a"
+dtl :: "'a dlist -> 'a dlist"
+dlist_take :: "nat => 'a dlist -> 'a dlist"
+dlist_finite :: "'a dlist => bool"
+dlist_bisim :: "('a dlist => 'a dlist => bool) => bool"
rules
@@ -66,12 +66,12 @@
(* dlist_abs is an isomorphism with inverse dlist_rep *)
(* identity is the least endomorphism on 'a dlist *)
-dlist_abs_iso "dlist_rep`(dlist_abs`x) = x"
-dlist_rep_iso "dlist_abs`(dlist_rep`x) = x"
-dlist_copy_def "dlist_copy == (LAM f. dlist_abs oo \
-\ (sswhen`sinl`(sinr oo (ssplit`(LAM x y. (|x,f`y|) ))))\
+dlist_abs_iso "dlist_rep`(dlist_abs`x) = x"
+dlist_rep_iso "dlist_abs`(dlist_rep`x) = x"
+dlist_copy_def "dlist_copy == (LAM f. dlist_abs oo \
+\ (sswhen`sinl`(sinr oo (ssplit`(LAM x y. (|x,f`y|) ))))\
\ oo dlist_rep)"
-dlist_reach "(fix`dlist_copy)`x=x"
+dlist_reach "(fix`dlist_copy)`x=x"
defs
@@ -80,8 +80,8 @@
(* ----------------------------------------------------------------------- *)
(* constructors *)
-dnil_def "dnil == dlist_abs`(sinl`one)"
-dcons_def "dcons == (LAM x l. dlist_abs`(sinr`(|x,l|) ))"
+dnil_def "dnil == dlist_abs`(sinl`one)"
+dcons_def "dcons == (LAM x l. dlist_abs`(sinr`(|x,l|) ))"
(* ----------------------------------------------------------------------- *)
(* discriminator functional *)
@@ -93,10 +93,10 @@
(* ----------------------------------------------------------------------- *)
(* discriminators and selectors *)
-is_dnil_def "is_dnil == dlist_when`TT`(LAM x l.FF)"
-is_dcons_def "is_dcons == dlist_when`FF`(LAM x l.TT)"
-dhd_def "dhd == dlist_when`UU`(LAM x l.x)"
-dtl_def "dtl == dlist_when`UU`(LAM x l.l)"
+is_dnil_def "is_dnil == dlist_when`TT`(LAM x l.FF)"
+is_dcons_def "is_dcons == dlist_when`FF`(LAM x l.TT)"
+dhd_def "dhd == dlist_when`UU`(LAM x l.x)"
+dtl_def "dtl == dlist_when`UU`(LAM x l.l)"
(* ----------------------------------------------------------------------- *)
(* the taker for dlists *)
@@ -105,7 +105,7 @@
(* ----------------------------------------------------------------------- *)
-dlist_finite_def "dlist_finite == (%s.? n.dlist_take n`s=s)"
+dlist_finite_def "dlist_finite == (%s.? n.dlist_take n`s=s)"
(* ----------------------------------------------------------------------- *)
(* definition of bisimulation is determined by domain equation *)
@@ -113,7 +113,7 @@
dlist_bisim_def "dlist_bisim ==
( %R.!l1 l2.
- R l1 l2 -->
+ R l1 l2 -->
((l1=UU & l2=UU) |
(l1=dnil & l2=dnil) |
(? x l11 l21. x~=UU & l11~=UU & l21~=UU &
--- a/src/HOLCF/explicit_domains/Dnat.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/explicit_domains/Dnat.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOLCF/Dnat.thy
+(* Title: HOLCF/Dnat.thy
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Theory for the domain of natural numbers dnat = one ++ dnat
@@ -31,22 +31,22 @@
(* ----------------------------------------------------------------------- *)
(* essential constants *)
-dnat_rep :: " dnat -> (one ++ dnat)"
-dnat_abs :: "(one ++ dnat) -> dnat"
+dnat_rep :: " dnat -> (one ++ dnat)"
+dnat_abs :: "(one ++ dnat) -> dnat"
(* ----------------------------------------------------------------------- *)
(* abstract constants and auxiliary constants *)
-dnat_copy :: "(dnat -> dnat) -> dnat -> dnat"
+dnat_copy :: "(dnat -> dnat) -> dnat -> dnat"
-dzero :: "dnat"
-dsucc :: "dnat -> dnat"
-dnat_when :: "'b -> (dnat -> 'b) -> dnat -> 'b"
-is_dzero :: "dnat -> tr"
-is_dsucc :: "dnat -> tr"
-dpred :: "dnat -> dnat"
-dnat_take :: "nat => dnat -> dnat"
-dnat_bisim :: "(dnat => dnat => bool) => bool"
+dzero :: "dnat"
+dsucc :: "dnat -> dnat"
+dnat_when :: "'b -> (dnat -> 'b) -> dnat -> 'b"
+is_dzero :: "dnat -> tr"
+is_dsucc :: "dnat -> tr"
+dpred :: "dnat -> dnat"
+dnat_take :: "nat => dnat -> dnat"
+dnat_bisim :: "(dnat => dnat => bool) => bool"
rules
@@ -61,11 +61,11 @@
(* dnat_abs is an isomorphism with inverse dnat_rep *)
(* identity is the least endomorphism on dnat *)
-dnat_abs_iso "dnat_rep`(dnat_abs`x) = x"
-dnat_rep_iso "dnat_abs`(dnat_rep`x) = x"
-dnat_copy_def "dnat_copy == (LAM f. dnat_abs oo
- (sswhen`sinl`(sinr oo f)) oo dnat_rep )"
-dnat_reach "(fix`dnat_copy)`x=x"
+dnat_abs_iso "dnat_rep`(dnat_abs`x) = x"
+dnat_rep_iso "dnat_abs`(dnat_rep`x) = x"
+dnat_copy_def "dnat_copy == (LAM f. dnat_abs oo
+ (sswhen`sinl`(sinr oo f)) oo dnat_rep )"
+dnat_reach "(fix`dnat_copy)`x=x"
defs
@@ -74,21 +74,21 @@
(* ----------------------------------------------------------------------- *)
(* constructors *)
-dzero_def "dzero == dnat_abs`(sinl`one)"
-dsucc_def "dsucc == (LAM n. dnat_abs`(sinr`n))"
+dzero_def "dzero == dnat_abs`(sinl`one)"
+dsucc_def "dsucc == (LAM n. dnat_abs`(sinr`n))"
(* ----------------------------------------------------------------------- *)
(* discriminator functional *)
-dnat_when_def "dnat_when == (LAM f1 f2 n.sswhen`(LAM x.f1)`f2`(dnat_rep`n))"
+dnat_when_def "dnat_when == (LAM f1 f2 n.sswhen`(LAM x.f1)`f2`(dnat_rep`n))"
(* ----------------------------------------------------------------------- *)
(* discriminators and selectors *)
-is_dzero_def "is_dzero == dnat_when`TT`(LAM x.FF)"
-is_dsucc_def "is_dsucc == dnat_when`FF`(LAM x.TT)"
-dpred_def "dpred == dnat_when`UU`(LAM x.x)"
+is_dzero_def "is_dzero == dnat_when`TT`(LAM x.FF)"
+is_dsucc_def "is_dsucc == dnat_when`FF`(LAM x.TT)"
+dpred_def "dpred == dnat_when`UU`(LAM x.x)"
(* ----------------------------------------------------------------------- *)
@@ -102,9 +102,9 @@
dnat_bisim_def "dnat_bisim ==
(%R.!s1 s2.
- R s1 s2 -->
+ R s1 s2 -->
((s1=UU & s2=UU) |(s1=dzero & s2=dzero) |
(? s11 s21. s11~=UU & s21~=UU & s1=dsucc`s11 &
- s2 = dsucc`s21 & R s11 s21)))"
+ s2 = dsucc`s21 & R s11 s21)))"
end
--- a/src/HOLCF/explicit_domains/Dnat2.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/explicit_domains/Dnat2.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOLCF/Dnat2.thy
+(* Title: HOLCF/Dnat2.thy
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Additional constants for dnat
@@ -11,19 +11,19 @@
consts
-iterator :: "dnat -> ('a -> 'a) -> 'a -> 'a"
+iterator :: "dnat -> ('a -> 'a) -> 'a -> 'a"
defs
-iterator_def "iterator == fix`(LAM h n f x.
- dnat_when `x `(LAM m.f`(h`m`f`x)) `n)"
+iterator_def "iterator == fix`(LAM h n f x.
+ dnat_when `x `(LAM m.f`(h`m`f`x)) `n)"
end
(*
- iterator`UU`f`x = UU
- iterator`dzero`f`x = x
+ iterator`UU`f`x = UU
+ iterator`dzero`f`x = x
n~=UU --> iterator`(dsucc`n)`f`x = f`(iterator`n`f`x)
*)
--- a/src/HOLCF/explicit_domains/Focus_ex.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/explicit_domains/Focus_ex.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
(*
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1995 Technische Universitaet Muenchen
*)
@@ -27,17 +27,17 @@
-----------------------------------------------------------------
agent f
- input channel i1:'b i2: ('b,'c) tc
- output channel o1:'c o2: ('b,'c) tc
+ input channel i1:'b i2: ('b,'c) tc
+ output channel o1:'c o2: ('b,'c) tc
is
- Rf(i1,i2,o1,o2) (left open in the example)
+ Rf(i1,i2,o1,o2) (left open in the example)
end f
agent g
- input channel x:'b
- output channel y:'c
+ input channel x:'b
+ output channel y:'c
is network
- <y,z> = f`<x,z>
+ <y,z> = f`<x,z>
end network
end g
@@ -51,37 +51,37 @@
Specification of agent f ist translated to predicate is_f
is_f :: ('b stream * ('b,'c) tc stream ->
- 'c stream * ('b,'c) tc stream) => bool
+ 'c stream * ('b,'c) tc stream) => bool
is_f f = ! i1 i2 o1 o2.
- f`<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2)
+ f`<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2)
Specification of agent g is translated to predicate is_g which uses
predicate is_net_g
is_net_g :: ('b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) =>
- 'b stream => 'c stream => bool
+ 'b stream => 'c stream => bool
is_net_g f x y =
- ? z. <y,z> = f`<x,z> &
- ! oy hz. <oy,hz> = f`<x,hz> --> z << hz
+ ? z. <y,z> = f`<x,z> &
+ ! oy hz. <oy,hz> = f`<x,hz> --> z << hz
is_g :: ('b stream -> 'c stream) => bool
is_g g = ? f. is_f f & (! x y. g`x = y --> is_net_g f x y
-
+
Third step: (show conservativity)
-----------
Suppose we have a model for the theory TH1 which contains the axiom
- ? f. is_f f
+ ? f. is_f f
In this case there is also a model for the theory TH2 that enriches TH1 by
axiom
- ? g. is_g g
+ ? g. is_g g
The result is proved by showing that there is a definitional extension
that extends TH1 by a definition of g.
@@ -91,17 +91,17 @@
def_g g =
(? f. is_f f &
- g = (LAM x. cfst`(f`<x,fix`(LAM k.csnd`(f`<x,k>))>)) )
-
+ g = (LAM x. cfst`(f`<x,fix`(LAM k.csnd`(f`<x,k>))>)) )
+
Now we prove:
- (?f. is_f f ) --> (? g. is_g g)
+ (?f. is_f f ) --> (? g. is_g g)
using the theorems
-loopback_eq) def_g = is_g (real work)
+loopback_eq) def_g = is_g (real work)
-L1) (? f. is_f f ) --> (? g. def_g g) (trivial)
+L1) (? f. is_f f ) --> (? g. def_g g) (trivial)
*)
@@ -116,28 +116,28 @@
is_f ::
"('b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) => bool"
is_net_g :: "('b stream *('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) =>
- 'b stream => 'c stream => bool"
+ 'b stream => 'c stream => bool"
is_g :: "('b stream -> 'c stream) => bool"
def_g :: "('b stream -> 'c stream) => bool"
-Rf ::
+Rf ::
"('b stream * ('b,'c) tc stream * 'c stream * ('b,'c) tc stream) => bool"
defs
-is_f "is_f f == (! i1 i2 o1 o2.
- f`<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2))"
+is_f "is_f f == (! i1 i2 o1 o2.
+ f`<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2))"
-is_net_g "is_net_g f x y == (? z.
- <y,z> = f`<x,z> &
- (! oy hz. <oy,hz> = f`<x,hz> --> z << hz))"
+is_net_g "is_net_g f x y == (? z.
+ <y,z> = f`<x,z> &
+ (! oy hz. <oy,hz> = f`<x,hz> --> z << hz))"
-is_g "is_g g == (? f.
- is_f f &
- (!x y. g`x = y --> is_net_g f x y))"
+is_g "is_g g == (? f.
+ is_f f &
+ (!x y. g`x = y --> is_net_g f x y))"
-def_g "def_g g == (? f.
- is_f f &
- g = (LAM x. cfst`(f`<x,fix`(LAM k.csnd`(f`<x,k>))>)))"
+def_g "def_g g == (? f.
+ is_f f &
+ g = (LAM x. cfst`(f`<x,fix`(LAM k.csnd`(f`<x,k>))>)))"
end
--- a/src/HOLCF/explicit_domains/Stream.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/explicit_domains/Stream.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
(*
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Theory for streams without defined empty stream
@@ -32,22 +32,22 @@
(* ----------------------------------------------------------------------- *)
(* essential constants *)
-stream_rep :: "('a stream) -> ('a ** ('a stream)u)"
-stream_abs :: "('a ** ('a stream)u) -> ('a stream)"
+stream_rep :: "('a stream) -> ('a ** ('a stream)u)"
+stream_abs :: "('a ** ('a stream)u) -> ('a stream)"
(* ----------------------------------------------------------------------- *)
(* abstract constants and auxiliary constants *)
-stream_copy :: "('a stream -> 'a stream) ->'a stream -> 'a stream"
+stream_copy :: "('a stream -> 'a stream) ->'a stream -> 'a stream"
-scons :: "'a -> 'a stream -> 'a stream"
-stream_when :: "('a -> 'a stream -> 'b) -> 'a stream -> 'b"
-is_scons :: "'a stream -> tr"
-shd :: "'a stream -> 'a"
-stl :: "'a stream -> 'a stream"
-stream_take :: "nat => 'a stream -> 'a stream"
-stream_finite :: "'a stream => bool"
-stream_bisim :: "('a stream => 'a stream => bool) => bool"
+scons :: "'a -> 'a stream -> 'a stream"
+stream_when :: "('a -> 'a stream -> 'b) -> 'a stream -> 'b"
+is_scons :: "'a stream -> tr"
+shd :: "'a stream -> 'a"
+stl :: "'a stream -> 'a stream"
+stream_take :: "nat => 'a stream -> 'a stream"
+stream_finite :: "'a stream => bool"
+stream_bisim :: "('a stream => 'a stream => bool) => bool"
rules
@@ -62,11 +62,11 @@
(* stream_abs is an isomorphism with inverse stream_rep *)
(* identity is the least endomorphism on 'a stream *)
-stream_abs_iso "stream_rep`(stream_abs`x) = x"
-stream_rep_iso "stream_abs`(stream_rep`x) = x"
-stream_copy_def "stream_copy == (LAM f. stream_abs oo
- (ssplit`(LAM x y. (|x , (lift`(up oo f))`y|) )) oo stream_rep)"
-stream_reach "(fix`stream_copy)`x = x"
+stream_abs_iso "stream_rep`(stream_abs`x) = x"
+stream_rep_iso "stream_abs`(stream_rep`x) = x"
+stream_copy_def "stream_copy == (LAM f. stream_abs oo
+ (ssplit`(LAM x y. (|x , (lift`(up oo f))`y|) )) oo stream_rep)"
+stream_reach "(fix`stream_copy)`x = x"
defs
(* ----------------------------------------------------------------------- *)
@@ -74,7 +74,7 @@
(* ----------------------------------------------------------------------- *)
(* constructors *)
-scons_def "scons == (LAM x l. stream_abs`(| x, up`l |))"
+scons_def "scons == (LAM x l. stream_abs`(| x, up`l |))"
(* ----------------------------------------------------------------------- *)
(* discriminator functional *)
@@ -85,9 +85,9 @@
(* ----------------------------------------------------------------------- *)
(* discriminators and selectors *)
-is_scons_def "is_scons == stream_when`(LAM x l.TT)"
-shd_def "shd == stream_when`(LAM x l.x)"
-stl_def "stl == stream_when`(LAM x l.l)"
+is_scons_def "is_scons == stream_when`(LAM x l.TT)"
+shd_def "shd == stream_when`(LAM x l.x)"
+stl_def "stl == stream_when`(LAM x l.l)"
(* ----------------------------------------------------------------------- *)
(* the taker for streams *)
@@ -96,7 +96,7 @@
(* ----------------------------------------------------------------------- *)
-stream_finite_def "stream_finite == (%s.? n.stream_take n `s=s)"
+stream_finite_def "stream_finite == (%s.? n.stream_take n `s=s)"
(* ----------------------------------------------------------------------- *)
(* definition of bisimulation is determined by domain equation *)
@@ -104,7 +104,7 @@
stream_bisim_def "stream_bisim ==
(%R.!s1 s2.
- R s1 s2 -->
+ R s1 s2 -->
((s1=UU & s2=UU) |
(? x s11 s21. x~=UU & s1=scons`x`s11 & s2 = scons`x`s21 & R s11 s21)))"
--- a/src/HOLCF/explicit_domains/Stream2.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/explicit_domains/Stream2.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
(*
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Additional constants for stream
@@ -10,7 +10,7 @@
consts
-smap :: "('a -> 'b) -> 'a stream -> 'b stream"
+smap :: "('a -> 'b) -> 'a stream -> 'b stream"
defs
@@ -22,7 +22,7 @@
(*
- smap`f`UU = UU
+ smap`f`UU = UU
x~=UU --> smap`f`(scons`x`xs) = scons `(f`x) `(smap`f`xs)
*)