src/ZF/ex/LListFn.ML
author lcp
Tue Aug 16 18:58:42 1994 +0200 (1994-08-16)
changeset 532 851df239ac8b
parent 173 85071e6ad295
permissions -rw-r--r--
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
     1 (*  Title: 	ZF/ex/llist-fn.ML
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 Functions for Lazy Lists in Zermelo-Fraenkel Set Theory 
     7 
     8 Examples of coinduction for type-checking and to prove llist equations
     9 *)
    10 
    11 open LListFn;
    12 
    13 (*** lconst -- defined directly using lfp, but equivalent to a LList_corec ***)
    14 
    15 goalw LListFn.thy LList.con_defs "bnd_mono(univ(a), %l. LCons(a,l))";
    16 by (rtac bnd_monoI 1);
    17 by (REPEAT (ares_tac [subset_refl, QInr_mono, QPair_mono] 2));
    18 by (REPEAT (ares_tac [subset_refl, A_subset_univ, 
    19 		      QInr_subset_univ, QPair_subset_univ] 1));
    20 val lconst_fun_bnd_mono = result();
    21 
    22 (* lconst(a) = LCons(a,lconst(a)) *)
    23 val lconst = standard 
    24     ([lconst_def, lconst_fun_bnd_mono] MRS def_lfp_Tarski);
    25 
    26 val lconst_subset = lconst_def RS def_lfp_subset;
    27 
    28 val member_subset_Union_eclose = standard (arg_into_eclose RS Union_upper);
    29 
    30 goal LListFn.thy "!!a A. a : A ==> lconst(a) : quniv(A)";
    31 by (rtac (lconst_subset RS subset_trans RS qunivI) 1);
    32 by (etac (arg_into_eclose RS eclose_subset RS univ_mono) 1);
    33 val lconst_in_quniv = result();
    34 
    35 goal LListFn.thy "!!a A. a:A ==> lconst(a): llist(A)";
    36 by (rtac (singletonI RS LList.coinduct) 1);
    37 by (fast_tac (ZF_cs addSIs [lconst_in_quniv]) 1);
    38 by (fast_tac (ZF_cs addSIs [lconst]) 1);
    39 val lconst_type = result();
    40 
    41 (*** flip --- equations merely assumed; certain consequences proved ***)
    42 
    43 val flip_ss = ZF_ss addsimps [flip_LNil, flip_LCons, not_type];
    44 
    45 goal QUniv.thy "!!b. b:bool ==> b Int X <= univ(eclose(A))";
    46 by (fast_tac (quniv_cs addSEs [boolE]) 1);
    47 val bool_Int_subset_univ = result();
    48 
    49 val flip_cs = quniv_cs addSIs [not_type]
    50                        addIs  [bool_Int_subset_univ];
    51 
    52 (*Reasoning borrowed from llist_eq.ML; a similar proof works for all
    53   "productive" functions -- cf Coquand's "Infinite Objects in Type Theory".*)
    54 goal LListFn.thy
    55    "!!i. Ord(i) ==> ALL l: llist(bool). flip(l) Int Vset(i) <= \
    56 \                   univ(eclose(bool))";
    57 by (etac trans_induct 1);
    58 by (rtac ballI 1);
    59 by (etac LList.elim 1);
    60 by (asm_simp_tac flip_ss 1);
    61 by (asm_simp_tac flip_ss 2);
    62 by (rewrite_goals_tac ([QInl_def,QInr_def]@LList.con_defs));
    63 (*LNil case*)
    64 by (fast_tac flip_cs 1);
    65 (*LCons case*)
    66 by (safe_tac flip_cs);
    67 by (ALLGOALS (fast_tac (flip_cs addSEs [Ord_trans, make_elim bspec])));
    68 val flip_llist_quniv_lemma = result();
    69 
    70 goal LListFn.thy "!!l. l: llist(bool) ==> flip(l) : quniv(bool)";
    71 by (rtac (flip_llist_quniv_lemma RS bspec RS Int_Vset_subset RS qunivI) 1);
    72 by (REPEAT (assume_tac 1));
    73 val flip_in_quniv = result();
    74 
    75 val [prem] = goal LListFn.thy "l : llist(bool) ==> flip(l): llist(bool)";
    76 by (res_inst_tac [("X", "{flip(l) . l:llist(bool)}")]
    77        LList.coinduct 1);
    78 by (rtac (prem RS RepFunI) 1);
    79 by (fast_tac (ZF_cs addSIs [flip_in_quniv]) 1);
    80 by (etac RepFunE 1);
    81 by (etac LList.elim 1);
    82 by (asm_simp_tac flip_ss 1);
    83 by (asm_simp_tac flip_ss 1);
    84 by (fast_tac (ZF_cs addSIs [not_type]) 1);
    85 val flip_type = result();
    86 
    87 val [prem] = goal LListFn.thy
    88     "l : llist(bool) ==> flip(flip(l)) = l";
    89 by (res_inst_tac [("X1", "{<flip(flip(l)),l> . l:llist(bool)}")]
    90        (LList_Eq.coinduct RS lleq_implies_equal) 1);
    91 by (rtac (prem RS RepFunI) 1);
    92 by (fast_tac (ZF_cs addSIs [flip_type]) 1);
    93 by (etac RepFunE 1);
    94 by (etac LList.elim 1);
    95 by (asm_simp_tac flip_ss 1);
    96 by (asm_simp_tac (flip_ss addsimps [flip_type, not_not]) 1);
    97 by (fast_tac (ZF_cs addSIs [not_type]) 1);
    98 val flip_flip = result();