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