--- a/List.ML Thu Aug 18 12:38:12 1994 +0200
+++ b/List.ML Thu Aug 18 12:42:19 1994 +0200
@@ -1,9 +1,9 @@
-(* Title: HOL/list
+(* Title: HOL/List
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
-For list.thy.
+For List.thy.
*)
open List;
@@ -172,11 +172,11 @@
(** Conversion rules for List_case: case analysis operator **)
-goalw List.thy [List_case_def,NIL_def] "List_case(NIL,c,h) = c";
+goalw List.thy [List_case_def,NIL_def] "List_case(c, h, NIL) = c";
by (rtac Case_In0 1);
val List_case_NIL = result();
-goalw List.thy [List_case_def,CONS_def] "List_case(CONS(M,N), c, h) = h(M,N)";
+goalw List.thy [List_case_def,CONS_def] "List_case(c, h, CONS(M,N)) = h(M,N)";
by (simp_tac (HOL_ss addsimps [Split,Case_In1]) 1);
val List_case_CONS = result();
@@ -213,20 +213,20 @@
goal List.thy "List_rec(NIL,c,h) = c";
by (rtac (List_rec_unfold RS trans) 1);
-by (rtac List_case_NIL 1);
+by (simp_tac (HOL_ss addsimps [List_case_NIL]) 1);
val List_rec_NIL = result();
goal List.thy "!!M. [| M: Sexp; N: Sexp |] ==> \
\ List_rec(CONS(M,N), c, h) = h(M, N, List_rec(N,c,h))";
by (rtac (List_rec_unfold RS trans) 1);
-by (rtac (List_case_CONS RS trans) 1);
-by(asm_simp_tac(HOL_ss addsimps [CONS_I, pred_Sexp_CONS_I2, cut_apply])1);
+by (asm_simp_tac
+ (HOL_ss addsimps [List_case_CONS, CONS_I, pred_Sexp_CONS_I2, cut_apply])1);
val List_rec_CONS = result();
(*** list_rec -- by List_rec ***)
val Rep_List_in_Sexp =
- Rep_List RS (range_Leaf_subset_Sexp RS List_subset_Sexp RS subsetD);
+ [range_Leaf_subset_Sexp RS List_subset_Sexp, Rep_List] MRS subsetD;
local
val list_rec_simps = list_free_simps @
@@ -392,7 +392,7 @@
(** list_case **)
goal List.thy
- "P(list_case(xs,a,f)) = ((xs=[] --> P(a)) & \
+ "P(list_case(a,f,xs)) = ((xs=[] --> P(a)) & \
\ (!y ys. xs=y#ys --> P(f(y,ys))))";
by(list_ind_tac "xs" 1);
by(ALLGOALS(asm_simp_tac list_ss));
--- a/List.thy Thu Aug 18 12:38:12 1994 +0200
+++ b/List.thy Thu Aug 18 12:42:19 1994 +0200
@@ -21,33 +21,33 @@
consts
- List_Fun :: "['a node set set, 'a node set set] => 'a node set set"
- List :: "'a node set set => 'a node set set"
- 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"
- "#" :: "['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"
- null :: "'a list => bool"
- hd :: "'a list => 'a"
- tl,ttl :: "'a list => 'a list"
+ List_Fun :: "['a node set set, 'a node set set] => 'a node set set"
+ List :: "'a node set set => 'a node set set"
+ 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"
+ "#" :: "['a, 'a list] => 'a list" (infixr 65)
+ List_case :: "['b, ['a node set, 'a node set]=>'b, 'a node set] => '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"
+ null :: "'a list => bool"
+ 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)
- list_case :: "['a list, 'b, ['a, 'a list]=>'b] => 'b"
- filter :: "['a => bool, 'a list] => 'a list"
+ list_all :: "('a => bool) => ('a list => bool)"
+ map :: "('a=>'b) => ('a list => 'b list)"
+ "@" :: "['a list, 'a list] => 'a list" (infixr 65)
+ list_case :: "['b, ['a, 'a list]=>'b, 'a list] => 'b"
+ filter :: "['a => bool, 'a list] => 'a list"
(* List Enumeration *)
- "[]" :: "'a list" ("[]")
- "@List" :: "args => 'a list" ("[(_)]")
+ "[]" :: "'a list" ("[]")
+ "@List" :: "args => 'a list" ("[(_)]")
(* Special syntax for list_all and filter *)
"@Alls" :: "[idt, 'a list, bool] => bool" ("(2Alls _:_./ _)" 10)
@@ -58,7 +58,7 @@
"[x]" == "x#[]"
"[]" == "Nil"
- "case xs of Nil => a | y#ys => b" == "list_case(xs,a,%y ys.b)"
+ "case xs of Nil => a | y#ys => b" == "list_case(a, %y ys.b, xs)"
"[x:xs . P]" == "filter(%x.P,xs)"
"Alls x:xs.P" == "list_all(%x.P,xs)"
@@ -84,13 +84,13 @@
Nil_def "Nil == Abs_List(NIL)"
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_case_def "List_case(c, d) == Case(%x.c, Split(d))"
(* List Recursion -- the trancl is Essential; see list.ML *)
List_rec_def
"List_rec(M, c, d) == wfrec(trancl(pred_Sexp), M, \
-\ %z g. List_case(z, c, %x y. d(x, y, g(y))))"
+\ List_case(%g.c, %x y g. d(x, y, g(y))))"
list_rec_def
"list_rec(l, c, d) == \
@@ -115,6 +115,6 @@
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), x#r, r))"
- list_case_def "list_case(xs, a, f) == list_rec(xs, a, %x xs r.f(x, xs))"
+ list_case_def "list_case(a, f, xs) == list_rec(xs, a, %x xs r.f(x, xs))"
end