# HG changeset patch # User clasohm # Date 823606951 -3600 # Node ID 21eb5e156d919036afb0d395d161ff235537558e # Parent 2b8c2a7547ab977ded189ba455b90c70463d19b8 expanded tabs diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/Cfun1.thy --- 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 *) diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/Cfun2.thy --- 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 diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/Cfun3.thy --- 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 diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/Cont.thy --- 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: *) diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/Cprod1.thy --- 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 diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/Cprod2.thy --- 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 diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/Cprod3.thy --- 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 - "" == ">" - "" == "cpair`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))" diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/Fix.thy --- 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)" diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/Fun1.thy --- 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 *) diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/Fun2.thy --- 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 diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/Fun3.thy --- 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 diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/HOLCF.thy --- 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 diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/Holcfb.thy --- 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)))" diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/Lift1.thy --- 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<bool) = less_lift" +inst_lift_po "((op <<)::[('a)u,('a)u]=>bool) = less_lift" end diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/Lift3.thy --- 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" diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/One.thy --- 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 diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/Pcpo.thy --- 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 *) diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/Porder.thy --- 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 << u)" +is_ub "S <| x == ! y.y:S --> y< x << u)" (* Arbitrary chains are total orders *) -is_tord "is_tord(S) == ! x y. x:S & y:S --> (x< (x< 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< x = y" - (* witness antisym_less_void *) +antisym_less "[|x< x = y" + (* witness antisym_less_void *) -trans_less "[|x< x< x<bool) = less_void" +inst_void_po "((op <<)::[void,void]=>bool) = less_void" (* start 8bit 1 *) (* end 8bit 1 *) diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/Sprod0.thy --- 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 *) diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/Sprod1.thy --- 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 diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/Sprod2.thy --- 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 diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/Sprod3.thy --- 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 *) diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/Ssum0.thy --- 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 *) diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/Ssum1.thy --- 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 diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/Ssum2.thy --- 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 diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/Ssum3.thy --- 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" diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/Tr1.thy --- 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 *) diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/Tr2.thy --- 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" diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/Void.thy --- 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 diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/ccc1.thy --- 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 diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/ex/Fix2.thy --- 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 diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/ex/Hoare.thy --- 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 diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/ex/Loop.thy --- 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 diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/explicit_domains/Coind.thy --- 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)) *) diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/explicit_domains/Dagstuhl.thy --- 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" diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/explicit_domains/Dlist.thy --- 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 & diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/explicit_domains/Dnat.thy --- 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 diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/explicit_domains/Dnat2.thy --- 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) *) diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/explicit_domains/Focus_ex.thy --- 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 - = f` + = f` 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` = --> Rf(i1,i2,o1,o2) + f` = --> 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. = f` & - ! oy hz. = f` --> z << hz + ? z. = f` & + ! oy hz. = f` --> 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`))>)) ) - + g = (LAM x. cfst`(f`))>)) ) + 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` = --> Rf(i1,i2,o1,o2))" +is_f "is_f f == (! i1 i2 o1 o2. + f` = --> Rf(i1,i2,o1,o2))" -is_net_g "is_net_g f x y == (? z. - = f` & - (! oy hz. = f` --> z << hz))" +is_net_g "is_net_g f x y == (? z. + = f` & + (! oy hz. = f` --> 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`))>)))" +def_g "def_g g == (? f. + is_f f & + g = (LAM x. cfst`(f`))>)))" end diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/explicit_domains/Stream.thy --- 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)))" diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/explicit_domains/Stream2.thy --- 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) *)