author lcp
Thu, 30 Sep 1993 10:10:21 +0100
changeset 14 1c0926788772
parent 0 a5a9c433f639
child 43 eb7ad4a7dc4f
permissions -rw-r--r--
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext domrange/image_subset,vimage_subset: deleted needless premise! misc: This slightly simplifies two proofs in Schroeder-Bernstein Theorem ind-syntax/rule_concl: recoded to avoid exceptions intr-elim: now checks conclusions of introduction rules func/fun_disjoint_Un: now uses ex_ex1I list-fn/hd,tl,drop: new simpdata/bquant_simps: new list/list_case_type: restored! bool.thy: changed 1 from a "def" to a translation Removed occurreces of one_def in bool.ML, nat.ML, univ.ML, ex/integ.ML nat/succ_less_induct: new induction principle arith/add_mono: new results about monotonicity simpdata/mem_simps: removed the ones for succ and cons; added succI1, consI2 to ZF_ss upair/succ_iff: new, for use with simp_tac (cons_iff already existed) ordinal/Ord_0_in_succ: renamed from Ord_0_mem_succ nat/nat_0_in_succ: new ex/prop-log/hyps_thms_if: split up the fast_tac call for more speed

(*  Title: 	ZF/list-fn
    ID:         $Id$
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1993  University of Cambridge

Functions for Lists in Zermelo-Fraenkel Set Theory 

map is a binding operator -- it applies to meta-level functions, not 
object-level functions.  This simplifies the final form of term_rec_conv,
although complicating its derivation.

ListFn = List +
  "@"	     :: "[i,i]=>i"      			(infixr 60)
  list_rec   :: "[i, i, [i,i,i]=>i] => i"
  map 	     :: "[i=>i, i] => i"
  length,rev :: "i=>i"
  flat       :: "i=>i"
  list_add   :: "i=>i"
  hd,tl      :: "i=>i"
  drop	     :: "[i,i]=>i"

 (* List Enumeration *)
 "[]"        :: "i" 	                           	("[]")
 "@List"     :: "args => i" 	                   	("[(_)]")

  "[x, xs]"     == "Cons(x, [xs])"
  "[x]"         == "Cons(x, [])"
  "[]"          == "Nil"


  hd_def	"hd(l)	     == list_case(0, %x xs.x, l)"
  tl_def	"tl(l)       == list_case(Nil, %x xs.xs, l)"
  drop_def	"drop(i,l)   == rec(i, l, %j r. tl(r))"

      "list_rec(l,c,h) == Vrec(l, %l g.list_case(c, %x xs. h(x, xs, g`xs), l))"

  map_def       "map(f,l)    == list_rec(l,  Nil,  %x xs r. Cons(f(x), r))"
  length_def    "length(l)   == list_rec(l,  0,  %x xs r. succ(r))"
  app_def       "xs@ys       == list_rec(xs, ys, %x xs r. Cons(x,r))"
  rev_def       "rev(l)      == list_rec(l,  Nil,  %x xs r. r @ [x])"
  flat_def      "flat(ls)    == list_rec(ls, Nil,  %l ls r. l @ r)"
  list_add_def  "list_add(l) == list_rec(l, 0,  %x xs r. x#+r)"