--- a/List.thy Thu Aug 25 10:47:33 1994 +0200
+++ b/List.thy Thu Aug 25 11:01:45 1994 +0200
@@ -5,9 +5,9 @@
Definition of type 'a list by a least fixed point
-We use List(A) == lfp(%Z. {NUMB(0)} <+> A <*> Z)
-and not List == lfp(%Z. {NUMB(0)} <+> range(Leaf) <*> Z)
-so that List can serve as a "functor" for defining other recursive types
+We use list(A) == lfp(%Z. {NUMB(0)} <+> A <*> Z)
+and not list == lfp(%Z. {NUMB(0)} <+> range(Leaf) <*> Z)
+so that list can serve as a "functor" for defining other recursive types
*)
List = Sexp +
@@ -21,19 +21,19 @@
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"
+ list :: "'a item set => 'a item set"
+ Rep_list :: "'a list => 'a item"
+ Abs_list :: "'a item => 'a list"
+ NIL :: "'a item"
+ CONS :: "['a item, 'a item] => 'a item"
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_case :: "['b, ['a item, 'a item]=>'b, 'a item] => 'b"
+ List_rec :: "['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b"
+ list_case :: "['b, ['a, 'a list]=>'b, 'a list] => '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"
+ Rep_map :: "('b => 'a item) => ('b list => 'a item)"
+ Abs_map :: "('a item => 'b) => 'a item => 'b list"
null :: "'a list => bool"
hd :: "'a list => 'a"
tl,ttl :: "'a list => 'a list"
@@ -41,13 +41,12 @@
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 *)
+ (* list Enumeration *)
"[]" :: "'a list" ("[]")
- "@List" :: "args => 'a list" ("[(_)]")
+ "@list" :: "args => 'a list" ("[(_)]")
(* Special syntax for list_all and filter *)
"@Alls" :: "[idt, 'a list, bool] => bool" ("(2Alls _:_./ _)" 10)
@@ -63,51 +62,51 @@
"[x:xs . P]" == "filter(%x.P,xs)"
"Alls x:xs.P" == "list_all(%x.P,xs)"
-rules
-
- List_Fun_def "List_Fun(A) == (%Z. {Numb(0)} <+> A <*> Z)"
- List_def "List(A) == lfp(List_Fun(A))"
-
- (* Faking a Type Definition ... *)
-
- Rep_List "Rep_List(xs): List(range(Leaf))"
- Rep_List_inverse "Abs_List(Rep_List(xs)) = xs"
- Abs_List_inverse "M: List(range(Leaf)) ==> Rep_List(Abs_List(M)) = M"
-
+defs
(* Defining the Concrete Constructors *)
-
NIL_def "NIL == In0(Numb(0))"
CONS_def "CONS(M, N) == In1(M $ N)"
- (* Defining the Abstract Constructors *)
+inductive "list(A)"
+ intrs
+ NIL_I "NIL: list(A)"
+ CONS_I "[| a: A; M: list(A) |] ==> CONS(a,M) : list(A)"
- Nil_def "Nil == Abs_List(NIL)"
- Cons_def "x#xs == Abs_List(CONS(Leaf(x), Rep_List(xs)))"
+rules
+ (* Faking a Type Definition ... *)
+ Rep_list "Rep_list(xs): list(range(Leaf))"
+ Rep_list_inverse "Abs_list(Rep_list(xs)) = xs"
+ Abs_list_inverse "M: list(range(Leaf)) ==> Rep_list(Abs_list(M)) = M"
+
+
+defs
+ (* Defining the Abstract Constructors *)
+ Nil_def "Nil == Abs_list(NIL)"
+ Cons_def "x#xs == Abs_list(CONS(Leaf(x), Rep_list(xs)))"
List_case_def "List_case(c, d) == Case(%x.c, Split(d))"
- (* List Recursion -- the trancl is Essential; see list.ML *)
+ (* list Recursion -- the trancl is Essential; see list.ML *)
List_rec_def
- "List_rec(M, c, d) == wfrec(trancl(pred_Sexp), M, \
+ "List_rec(M, c, d) == wfrec(trancl(pred_sexp), M, \
\ List_case(%g.c, %x y g. d(x, y, g(y))))"
list_rec_def
"list_rec(l, c, d) == \
-\ List_rec(Rep_List(l), c, %x y r. d(Inv(Leaf, x), Abs_List(y), r))"
+\ List_rec(Rep_list(l), c, %x y r. d(Inv(Leaf, x), Abs_list(y), r))"
(* 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. g(N)#r)"
+ 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. 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)"
@@ -115,6 +114,7 @@
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(a, f, xs) == list_rec(xs, a, %x xs r.f(x, xs))"
end