src/ZF/ex/LListFn.ML

ZF/ex/llist_eq/lleq_Int_Vset_subset_lemma,
ZF/ex/counit/counit2_Int_Vset_subset_lemma: now uses QPair_Int_Vset_subset_UN

ZF/ex/llistfn/flip_llist_quniv_lemma: now uses transfinite induction and
QPair_Int_Vset_subset_UN

ZF/ex/llist/llist_quniv_lemma: now uses transfinite induction and
QPair_Int_Vset_subset_UN

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

Functions for Lazy Lists in Zermelo-Fraenkel Set Theory 

Examples of coinduction for type-checking and to prove llist equations
*)

open LListFn;

(*** lconst -- defined directly using lfp, but equivalent to a LList_corec ***)

goalw LListFn.thy LList.con_defs "bnd_mono(univ(a), %l. LCons(a,l))";
by (rtac bnd_monoI 1);
by (REPEAT (ares_tac [subset_refl, QInr_mono, QPair_mono] 2));
by (REPEAT (ares_tac [subset_refl, A_subset_univ, 
		      QInr_subset_univ, QPair_subset_univ] 1));
val lconst_fun_bnd_mono = result();

(* lconst(a) = LCons(a,lconst(a)) *)
val lconst = standard 
    ([lconst_def, lconst_fun_bnd_mono] MRS def_lfp_Tarski);

val lconst_subset = lconst_def RS def_lfp_subset;

val member_subset_Union_eclose = standard (arg_into_eclose RS Union_upper);

goal LListFn.thy "!!a A. a : A ==> lconst(a) : quniv(A)";
by (rtac (lconst_subset RS subset_trans RS qunivI) 1);
by (etac (arg_into_eclose RS eclose_subset RS univ_mono) 1);
val lconst_in_quniv = result();

goal LListFn.thy "!!a A. a:A ==> lconst(a): llist(A)";
by (rtac (singletonI RS LList.coinduct) 1);
by (fast_tac (ZF_cs addSIs [lconst_in_quniv]) 1);
by (fast_tac (ZF_cs addSIs [lconst]) 1);
val lconst_type = result();

(*** flip --- equations merely assumed; certain consequences proved ***)

val flip_ss = ZF_ss addsimps [flip_LNil, flip_LCons, not_type];

goal QUniv.thy "!!b. b:bool ==> b Int X <= univ(eclose(A))";
by (fast_tac (quniv_cs addSEs [boolE]) 1);
val bool_Int_subset_univ = result();

val flip_cs = quniv_cs addSIs [not_type]
                       addIs  [bool_Int_subset_univ];

(*Reasoning borrowed from llist_eq.ML; a similar proof works for all
  "productive" functions -- cf Coquand's "Infinite Objects in Type Theory".*)
goal LListFn.thy
   "!!i. Ord(i) ==> ALL l: llist(bool). flip(l) Int Vset(i) <= \
\                   univ(eclose(bool))";
by (etac trans_induct 1);
by (rtac ballI 1);
by (etac LList.elim 1);
by (asm_simp_tac flip_ss 1);
by (asm_simp_tac flip_ss 2);
by (rewrite_goals_tac ([QInl_def,QInr_def]@LList.con_defs));
(*LNil case*)
by (fast_tac flip_cs 1);
(*LCons case*)
by (safe_tac flip_cs);
by (ALLGOALS (fast_tac (flip_cs addSEs [Ord_trans, make_elim bspec])));
val flip_llist_quniv_lemma = result();

goal LListFn.thy "!!l. l: llist(bool) ==> flip(l) : quniv(bool)";
by (rtac (flip_llist_quniv_lemma RS bspec RS Int_Vset_subset RS qunivI) 1);
by (REPEAT (assume_tac 1));
val flip_in_quniv = result();

val [prem] = goal LListFn.thy "l : llist(bool) ==> flip(l): llist(bool)";
by (res_inst_tac [("X", "{flip(l) . l:llist(bool)}")]
       LList.coinduct 1);
by (rtac (prem RS RepFunI) 1);
by (fast_tac (ZF_cs addSIs [flip_in_quniv]) 1);
by (etac RepFunE 1);
by (etac LList.elim 1);
by (asm_simp_tac flip_ss 1);
by (asm_simp_tac flip_ss 1);
by (fast_tac (ZF_cs addSIs [not_type]) 1);
val flip_type = result();

val [prem] = goal LListFn.thy
    "l : llist(bool) ==> flip(flip(l)) = l";
by (res_inst_tac [("X1", "{<flip(flip(l)),l> . l:llist(bool)}")]
       (LList_Eq.coinduct RS lleq_implies_equal) 1);
by (rtac (prem RS RepFunI) 1);
by (fast_tac (ZF_cs addSIs [flip_type]) 1);
by (etac RepFunE 1);
by (etac LList.elim 1);
by (asm_simp_tac flip_ss 1);
by (asm_simp_tac (flip_ss addsimps [flip_type, not_not]) 1);
by (fast_tac (ZF_cs addSIs [not_type]) 1);
val flip_flip = result();