List.ML

--- a/List.ML	Thu Feb 24 14:45:57 1994 +0100
+++ b/List.ML	Wed Mar 02 12:26:55 1994 +0100
@@ -52,7 +52,7 @@
 (*Induction for the type 'a list *)
 val prems = goalw List.thy [Nil_def,Cons_def]
     "[| P(Nil);   \
-\       !!x xs. P(xs) ==> P(Cons(x,xs)) |]  ==> P(l)";
+\       !!x xs. P(xs) ==> P(x # xs) |]  ==> P(l)";
 by (rtac (Rep_List_inverse RS subst) 1);   (*types force good instantiation*)
 by (rtac (Rep_List RS List_induct) 1);
 by (REPEAT (ares_tac prems 1
@@ -104,7 +104,7 @@
 val CONS_neq_NIL = standard (CONS_not_NIL RS notE);
 val NIL_neq_CONS = sym RS CONS_neq_NIL;
 
-goalw List.thy [Nil_def,Cons_def] "Cons(x,xs) ~= Nil";
+goalw List.thy [Nil_def,Cons_def] "x # xs ~= Nil";
 by (rtac (CONS_not_NIL RS (inj_onto_Abs_List RS inj_onto_contraD)) 1);
 by (REPEAT (resolve_tac [rangeI, NIL_I, CONS_I, Rep_List] 1));
 val Cons_not_Nil = result();
@@ -128,7 +128,7 @@
 		     addSDs [inj_onto_Abs_List RS inj_ontoD,
 			     inj_Rep_List RS injD, Leaf_inject];
 
-goalw List.thy [Cons_def] "(Cons(x,xs)=Cons(y,ys)) = (x=y & xs=ys)";
+goalw List.thy [Cons_def] "(x#xs=y#ys) = (x=y & xs=ys)";
 by (fast_tac List_cs 1);
 val Cons_Cons_eq = result();
 val Cons_inject = standard (Cons_Cons_eq RS iffD1 RS conjE);
@@ -157,13 +157,13 @@
 by (ALLGOALS (asm_simp_tac list_free_ss));
 val not_CONS_self = result();
 
-goal List.thy "!x. l ~= Cons(x,l)";
+goal List.thy "!x. l ~= x#l";
 by (list_ind_tac "l" 1);
 by (ALLGOALS (asm_simp_tac list_free_ss));
 val not_Cons_self = result();
 
 
-goal List.thy "(xs ~= []) = (? y ys. xs = Cons(y,ys))";
+goal List.thy "(xs ~= []) = (? y ys. xs = y#ys)";
 by(list_ind_tac "xs" 1);
 by(simp_tac list_free_ss 1);
 by(asm_simp_tac list_free_ss 1);
@@ -240,7 +240,7 @@
    (fn _=> [simp_tac (HOL_ss addsimps list_rec_simps) 1]);
 
   val list_rec_Cons = prove_goalw List.thy [list_rec_def, Cons_def]
-      "list_rec(Cons(a,l), c, h) = h(a, l, list_rec(l,c,h))"
+      "list_rec(a#l, c, h) = h(a, l, list_rec(l,c,h))"
    (fn _=> [simp_tac (HOL_ss addsimps list_rec_simps) 1]);
 end;
 
@@ -269,7 +269,7 @@
 val Rep_map_Nil = result();
 
 goalw List.thy [Rep_map_def]
-    "Rep_map(f, Cons(x,xs)) = CONS(f(x), Rep_map(f,xs))";
+    "Rep_map(f, x#xs) = CONS(f(x), Rep_map(f,xs))";
 by (rtac list_rec_Cons 1);
 val Rep_map_Cons = result();
 
@@ -284,7 +284,7 @@
 
 val prems = goalw List.thy [Abs_map_def]
     "[| M: Sexp;  N: Sexp |] ==> \
-\    Abs_map(g, CONS(M,N)) = Cons(g(M), Abs_map(g,N))";
+\    Abs_map(g, CONS(M,N)) = g(M) # Abs_map(g,N)";
 by (REPEAT (resolve_tac (List_rec_CONS::prems) 1));
 val Abs_map_CONS = result();
 
@@ -296,7 +296,7 @@
 val def_list_rec_Nil = result();
 
 val [rew] = goal List.thy
-    "[| !!xs. f(xs) == list_rec(xs,c,h) |] ==> f(Cons(x,xs)) = h(x,xs,f(xs))";
+    "[| !!xs. f(xs) == list_rec(xs,c,h) |] ==> f(x#xs) = h(x,xs,f(xs))";
 by (rewtac rew);
 by (rtac list_rec_Cons 1);
 val def_list_rec_Cons = result();
@@ -393,7 +393,7 @@
 
 goal List.thy
  "P(list_case(xs,a,f)) = ((xs=[] --> P(a)) & \
-\                         (!y ys. xs=Cons(y,ys) --> P(f(y,ys))))";
+\                         (!y ys. xs=y#ys --> P(f(y,ys))))";
 by(list_ind_tac "xs" 1);
 by(ALLGOALS(asm_simp_tac list_ss));
 by(fast_tac HOL_cs 1);