src/ZF/ex/llistfn.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 120 09287f26bfb8
permissions -rw-r--r--
Initial revision
clasohm@0
     1
(*  Title: 	ZF/ex/llist-fn.ML
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
clasohm@0
     6
Functions for Lazy Lists in Zermelo-Fraenkel Set Theory 
clasohm@0
     7
*)
clasohm@0
     8
clasohm@0
     9
open LListFn;
clasohm@0
    10
clasohm@0
    11
(*** lconst -- defined directly using lfp, but equivalent to a LList_corec ***)
clasohm@0
    12
clasohm@0
    13
goalw LListFn.thy LList.con_defs "bnd_mono(univ(a), %l. LCons(a,l))";
clasohm@0
    14
by (rtac bnd_monoI 1);
clasohm@0
    15
by (REPEAT (ares_tac [subset_refl, QInr_mono, QPair_mono] 2));
clasohm@0
    16
by (REPEAT (ares_tac [subset_refl, A_subset_univ, 
clasohm@0
    17
		      QInr_subset_univ, QPair_subset_univ] 1));
clasohm@0
    18
val lconst_fun_bnd_mono = result();
clasohm@0
    19
clasohm@0
    20
(* lconst(a) = LCons(a,lconst(a)) *)
clasohm@0
    21
val lconst = standard 
clasohm@0
    22
    ([lconst_def, lconst_fun_bnd_mono] MRS def_lfp_Tarski);
clasohm@0
    23
clasohm@0
    24
val lconst_subset = lconst_def RS def_lfp_subset;
clasohm@0
    25
clasohm@0
    26
val member_subset_Union_eclose = standard (arg_into_eclose RS Union_upper);
clasohm@0
    27
clasohm@0
    28
goal LListFn.thy "!!a A. a : A ==> lconst(a) : quniv(A)";
clasohm@0
    29
by (rtac (lconst_subset RS subset_trans RS qunivI) 1);
clasohm@0
    30
by (etac (arg_into_eclose RS eclose_subset RS univ_mono) 1);
clasohm@0
    31
val lconst_in_quniv = result();
clasohm@0
    32
clasohm@0
    33
goal LListFn.thy "!!a A. a:A ==> lconst(a): llist(A)";
clasohm@0
    34
by (rtac (singletonI RS LList.co_induct) 1);
clasohm@0
    35
by (fast_tac (ZF_cs addSIs [lconst_in_quniv]) 1);
clasohm@0
    36
by (fast_tac (ZF_cs addSIs [lconst]) 1);
clasohm@0
    37
val lconst_type = result();