List.thy

   Rep_List      :: "'a list => 'a node set"
   Abs_List      :: "'a node set => 'a list"
   NIL           :: "'a node set"
   CONS          :: "['a node set, 'a node set] => 'a node set"
   Nil           :: "'a list"
-  Cons          :: "['a, 'a list] => 'a list"
+  "#"           :: "['a, 'a list] => 'a list"                   (infixr 65)
   List_case     :: "['a node set, 'b, ['a node set, 'a node set]=>'b] => 'b"
   List_rec      :: "['a node set, 'b, ['a node set, 'a node set, 'b]=>'b] => 'b"
   list_rec      :: "['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b"
   Rep_map       :: "('b => 'a node set) => ('b list => 'a node set)"
   Abs_map       :: "('a node set => 'b) => 'a node set => 'b list"

   hd            :: "'a list => 'a"
   tl,ttl        :: "'a list => 'a list"
   mem		:: "['a, 'a list] => bool"			(infixl 55)
   list_all      :: "('a => bool) => ('a list => bool)"
   map           :: "('a=>'b) => ('a list => 'b list)"
-  "@"		:: "['a list, 'a list] => 'a list"		(infixr 65)
+  "@"		:: "['a list, 'a list] => 'a list"		(infixl 65)
   list_case     :: "['a list, 'b, ['a, 'a list]=>'b] => 'b"
   filter	:: "['a => bool, 'a list] => 'a list"
 
   (* List Enumeration *)
 

   (* Special syntax for list_all and filter *)
   "@Alls"	:: "[idt, 'a list, bool] => bool"	("(2Alls _:_./ _)" 10)
   "@filter"	:: "[idt, 'a list, bool] => 'a list"	("(1[_:_ ./ _])")
 
 translations
-  "[x, xs]"     == "Cons(x, [xs])"
-  "[x]"         == "Cons(x, [])"
+  "[x, xs]"     == "x#[xs]"
+  "[x]"         == "x#[]"
   "[]"          == "Nil"
 
-  "case xs of Nil => a | Cons(y,ys) => b" == "list_case(xs,a,%y ys.b)"
+  "case xs of Nil => a | y#ys => b" == "list_case(xs,a,%y ys.b)"
 
   "[x:xs . P]"	== "filter(%x.P,xs)"
   "Alls x:xs.P"	== "list_all(%x.P,xs)"
 
 rules

   Abs_List_inverse  "M: List(range(Leaf)) ==> Rep_List(Abs_List(M)) = M"
 
   (* Defining the Concrete Constructors *)
 
   NIL_def       "NIL == In0(Numb(0))"
-  CONS_def      "CONS(M, N) == In1(M . N)"
+  CONS_def      "CONS(M, N) == In1(M $ N)"
 
   (* Defining the Abstract Constructors *)
 
   Nil_def       "Nil == Abs_List(NIL)"
-  Cons_def      "Cons(x, xs) == Abs_List(CONS(Leaf(x), Rep_List(xs)))"
+  Cons_def      "x#xs == Abs_List(CONS(Leaf(x), Rep_List(xs)))"
 
   List_case_def "List_case(M, c, d) == Case(M, %x.c, %u. Split(u, %x y.d(x, y)))"
 
   (* List Recursion -- the trancl is Essential; see list.ML *)
 

   (* Generalized Map Functionals *)
 
   Rep_map_def
    "Rep_map(f, xs) == list_rec(xs, NIL, %x l r. CONS(f(x), r))"
   Abs_map_def
-   "Abs_map(g, M) == List_rec(M, Nil, %N L r. Cons(g(N), r))"
+   "Abs_map(g, M) == List_rec(M, Nil, %N L r. g(N)#r)"
 
   null_def      "null(xs)            == list_rec(xs, True, %x xs r.False)"
   hd_def        "hd(xs)              == list_rec(xs, @x.True, %x xs r.x)"
   tl_def        "tl(xs)              == list_rec(xs, @xs.True, %x xs r.xs)"
   (* a total version of tl: *)
   ttl_def	"ttl(xs)             == list_rec(xs, [], %x xs r.xs)"
   mem_def	"x mem xs            == \
 \		   list_rec(xs, False, %y ys r. if(y=x, True, r))"
   list_all_def  "list_all(P, xs)     == list_rec(xs, True, %x l r. P(x) & r)"
-  map_def       "map(f, xs)          == list_rec(xs, [], %x l r. Cons(f(x),r))"
-  append_def	"xs@ys               == list_rec(xs, ys, %x l r. Cons(x,r))"
+  map_def       "map(f, xs)          == list_rec(xs, [], %x l r. f(x)#r)"
+  append_def	"xs@ys               == list_rec(xs, ys, %x l r. x#r)"
   filter_def	"filter(P,xs)        == \
-\                  list_rec(xs, [], %x xs r. if(P(x), Cons(x,r), r))"
+\                  list_rec(xs, [], %x xs r. if(P(x), x#r, r))"
   list_case_def "list_case(xs, a, f) == list_rec(xs, a, %x xs r.f(x, xs))"
 
 end