Added weak congruence rules to HOL: if_weak_cong, case_weak_cong,
split_weak_cong, nat_case_weak_cong, nat_rec_weak_cong. Used in llist.ML
to make simplifications faster.
HOL/gfp: re-ordered premises to put mono(f) early (first or right after
A==gfp(f) in the def_ rules). Renamed some variables in rules, A to X and
h to A. Renamed coinduct to weak_coinduct, coinduct2 to coinduct.
Strengthened coinduct as suggested by j. Frost, to have the premise X <= f(X
Un gfp(f)).
HOL/llist: used stronger coinduct rule to strengthen LList_coinduct,
LList_equalityI, llist_equalityI, llist_fun_equalityI and to delete the "2"
form of those rules. Proved List_Fun_LList_I, LListD_Fun_diag_I and
llistD_Fun_range_I to help use the new coinduction rules; most proofs
involving them required small changes. Proved prod_fun_range_eq_diag as
lemma for llist_equalityI.
(* Title: HOL/list
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
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
*)
List = Sexp +
types
list 1
arities
list :: (term) term
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"
Cons :: "['a, 'a list] => 'a list"
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 :: "'a list => 'a list"
list_all :: "('a => bool) => ('a list => bool)"
map :: "('a=>'b) => ('a list => 'b list)"
list_case :: "['a list, 'b, ['a, 'a list]=>'b] => 'b"
(* List Enumeration *)
"[]" :: "'a list" ("[]")
"@List" :: "args => 'a list" ("[(_)]")
translations
"[x, xs]" == "Cons(x, [xs])"
"[x]" == "Cons(x, [])"
"[]" == "Nil"
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"
(* Defining the Concrete Constructors *)
NIL_def "NIL == In0(Numb(0))"
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)))"
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 *)
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_rec_def
"list_rec(l, c, d) == \
\ 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. Cons(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)"
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, Nil, %x l r. Cons(f(x), r))"
list_case_def "list_case(xs, a, f) == list_rec(xs, a, %x xs r.f(x, xs))"
end