Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOLCF/Dlist.thy
changeset 1168 74be52691d62
parent 1150 66512c9e6bd6 
--- a/src/HOLCF/Dlist.thy	Thu Jun 29 16:16:24 1995 +0200
+++ b/src/HOLCF/Dlist.thy	Thu Jun 29 16:28:40 1995 +0200
@@ -66,44 +66,46 @@
 (* 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 
- 		(when[sinl][sinr oo (ssplit[LAM x y. x ## f[y]])])
-                                oo dlist_rep)"
-dlist_reach	"(fix[dlist_copy])[x]=x"
+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"
 
+
+defs
 (* ----------------------------------------------------------------------- *)
 (* properties of additional constants                                      *)
 (* ----------------------------------------------------------------------- *)
 (* 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                                                *)
 
 dlist_when_def 
-"dlist_when == (LAM f1 f2 l.
-   when[LAM x.f1][ssplit[LAM x l.f2[x][l]]][dlist_rep[l]])"
+"dlist_when == (LAM f1 f2 l.\
+\   sswhen`(LAM x.f1) `(ssplit`(LAM x l.f2`x`l)) `(dlist_rep`l))"
 
 (* ----------------------------------------------------------------------- *)
 (* 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                                                   *)
 
-dlist_take_def "dlist_take == (%n.iterate(n,dlist_copy,UU))"
+dlist_take_def "dlist_take == (%n.iterate n dlist_copy UU)"
 
 (* ----------------------------------------------------------------------- *)
 
-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             *)
@@ -111,11 +113,11 @@
 
 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 & 
-               l1=dcons[x][l11] & l2 = dcons[x][l21] & R(l11,l21))))"
+               l1=dcons`x`l11 & l2 = dcons`x`l21 & R l11 l21)))"
 
 end
isabelle