diff -r 69d815b0e1eb -r 21291189b51e 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);