src/ZF/ex/LList.ML
author lcp
Tue Aug 16 18:58:42 1994 +0200 (1994-08-16)
changeset 532 851df239ac8b
parent 529 f0d16216e394
child 576 469279790410
permissions -rw-r--r--
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
     1 (*  Title: 	ZF/ex/LList.ML
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 
     6 Codatatype definition of Lazy Lists
     7 *)
     8 
     9 open LList;
    10 
    11 (*An elimination rule, for type-checking*)
    12 val LConsE = llist.mk_cases llist.con_defs "LCons(a,l) : llist(A)";
    13 
    14 (*Proving freeness results*)
    15 val LCons_iff      = llist.mk_free "LCons(a,l)=LCons(a',l') <-> a=a' & l=l'";
    16 val LNil_LCons_iff = llist.mk_free "~ LNil=LCons(a,l)";
    17 
    18 goal LList.thy "llist(A) = {0} <+> (A <*> llist(A))";
    19 let open llist;  val rew = rewrite_rule con_defs in  
    20 by (fast_tac (qsum_cs addSIs (equalityI :: map rew intrs)
    21                       addEs [rew elim]) 1)
    22 end;
    23 val llist_unfold = result();
    24 
    25 (*** Lemmas to justify using "llist" in other recursive type definitions ***)
    26 
    27 goalw LList.thy llist.defs "!!A B. A<=B ==> llist(A) <= llist(B)";
    28 by (rtac gfp_mono 1);
    29 by (REPEAT (rtac llist.bnd_mono 1));
    30 by (REPEAT (ares_tac (quniv_mono::basic_monos) 1));
    31 val llist_mono = result();
    32 
    33 (** Closure of quniv(A) under llist -- why so complex?  Its a gfp... **)
    34 
    35 val quniv_cs = subset_cs addSIs [QPair_Int_Vset_subset_UN RS subset_trans, 
    36 				 QPair_subset_univ,
    37 				 empty_subsetI, one_in_quniv RS qunivD]
    38                  addIs  [Int_lower1 RS subset_trans]
    39 		 addSDs [qunivD]
    40                  addSEs [Ord_in_Ord];
    41 
    42 goal LList.thy
    43    "!!i. Ord(i) ==> ALL l: llist(quniv(A)). l Int Vset(i) <= univ(eclose(A))";
    44 by (etac trans_induct 1);
    45 by (rtac ballI 1);
    46 by (etac llist.elim 1);
    47 by (rewrite_goals_tac ([QInl_def,QInr_def]@llist.con_defs));
    48 (*LNil case*)
    49 by (fast_tac quniv_cs 1);
    50 (*LCons case*)
    51 by (safe_tac quniv_cs);
    52 by (ALLGOALS (fast_tac (quniv_cs addSEs [Ord_trans, make_elim bspec])));
    53 val llist_quniv_lemma = result();
    54 
    55 goal LList.thy "llist(quniv(A)) <= quniv(A)";
    56 by (rtac (qunivI RS subsetI) 1);
    57 by (rtac Int_Vset_subset 1);
    58 by (REPEAT (ares_tac [llist_quniv_lemma RS bspec] 1));
    59 val llist_quniv = result();
    60 
    61 val llist_subset_quniv = standard
    62     (llist_mono RS (llist_quniv RSN (2,subset_trans)));
    63 
    64 
    65 (*** Lazy List Equality: lleq ***)
    66 
    67 val lleq_cs = subset_cs
    68 	addSIs [QPair_Int_Vset_subset_UN RS subset_trans, QPair_mono]
    69         addSEs [Ord_in_Ord, Pair_inject];
    70 
    71 (*Lemma for proving finality.  Unfold the lazy list; use induction hypothesis*)
    72 goal LList.thy
    73    "!!i. Ord(i) ==> ALL l l'. <l,l'> : lleq(A) --> l Int Vset(i) <= l'";
    74 by (etac trans_induct 1);
    75 by (REPEAT (resolve_tac [allI, impI] 1));
    76 by (etac lleq.elim 1);
    77 by (rewrite_goals_tac (QInr_def::llist.con_defs));
    78 by (safe_tac lleq_cs);
    79 by (fast_tac (subset_cs addSEs [Ord_trans, make_elim bspec]) 1);
    80 val lleq_Int_Vset_subset_lemma = result();
    81 
    82 val lleq_Int_Vset_subset = standard
    83 	(lleq_Int_Vset_subset_lemma RS spec RS spec RS mp);
    84 
    85 
    86 (*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*)
    87 val [prem] = goal LList.thy "<l,l'> : lleq(A) ==> <l',l> : lleq(A)";
    88 by (rtac (prem RS converseI RS lleq.coinduct) 1);
    89 by (rtac (lleq.dom_subset RS converse_type) 1);
    90 by (safe_tac converse_cs);
    91 by (etac lleq.elim 1);
    92 by (ALLGOALS (fast_tac qconverse_cs));
    93 val lleq_symmetric = result();
    94 
    95 goal LList.thy "!!l l'. <l,l'> : lleq(A) ==> l=l'";
    96 by (rtac equalityI 1);
    97 by (REPEAT (ares_tac [lleq_Int_Vset_subset RS Int_Vset_subset] 1
    98      ORELSE etac lleq_symmetric 1));
    99 val lleq_implies_equal = result();
   100 
   101 val [eqprem,lprem] = goal LList.thy
   102     "[| l=l';  l: llist(A) |] ==> <l,l'> : lleq(A)";
   103 by (res_inst_tac [("X", "{<l,l>. l: llist(A)}")] lleq.coinduct 1);
   104 by (rtac (lprem RS RepFunI RS (eqprem RS subst)) 1);
   105 by (safe_tac qpair_cs);
   106 by (etac llist.elim 1);
   107 by (ALLGOALS (fast_tac pair_cs));
   108 val equal_llist_implies_leq = result();
   109 
   110 
   111 (*** Lazy List Functions ***)
   112 
   113 (*Examples of coinduction for type-checking and to prove llist equations*)
   114 
   115 (*** lconst -- defined directly using lfp, but equivalent to a LList_corec ***)
   116 
   117 goalw LList.thy llist.con_defs "bnd_mono(univ(a), %l. LCons(a,l))";
   118 by (rtac bnd_monoI 1);
   119 by (REPEAT (ares_tac [subset_refl, QInr_mono, QPair_mono] 2));
   120 by (REPEAT (ares_tac [subset_refl, A_subset_univ, 
   121 		      QInr_subset_univ, QPair_subset_univ] 1));
   122 val lconst_fun_bnd_mono = result();
   123 
   124 (* lconst(a) = LCons(a,lconst(a)) *)
   125 val lconst = standard 
   126     ([lconst_def, lconst_fun_bnd_mono] MRS def_lfp_Tarski);
   127 
   128 val lconst_subset = lconst_def RS def_lfp_subset;
   129 
   130 val member_subset_Union_eclose = standard (arg_into_eclose RS Union_upper);
   131 
   132 goal LList.thy "!!a A. a : A ==> lconst(a) : quniv(A)";
   133 by (rtac (lconst_subset RS subset_trans RS qunivI) 1);
   134 by (etac (arg_into_eclose RS eclose_subset RS univ_mono) 1);
   135 val lconst_in_quniv = result();
   136 
   137 goal LList.thy "!!a A. a:A ==> lconst(a): llist(A)";
   138 by (rtac (singletonI RS llist.coinduct) 1);
   139 by (fast_tac (ZF_cs addSIs [lconst_in_quniv]) 1);
   140 by (fast_tac (ZF_cs addSIs [lconst]) 1);
   141 val lconst_type = result();
   142 
   143 (*** flip --- equations merely assumed; certain consequences proved ***)
   144 
   145 val flip_ss = ZF_ss addsimps [flip_LNil, flip_LCons, not_type];
   146 
   147 goal QUniv.thy "!!b. b:bool ==> b Int X <= univ(eclose(A))";
   148 by (fast_tac (quniv_cs addSEs [boolE]) 1);
   149 val bool_Int_subset_univ = result();
   150 
   151 val flip_cs = quniv_cs addSIs [not_type]
   152                        addIs  [bool_Int_subset_univ];
   153 
   154 (*Reasoning borrowed from lleq.ML; a similar proof works for all
   155   "productive" functions -- cf Coquand's "Infinite Objects in Type Theory".*)
   156 goal LList.thy
   157    "!!i. Ord(i) ==> ALL l: llist(bool). flip(l) Int Vset(i) <= \
   158 \                   univ(eclose(bool))";
   159 by (etac trans_induct 1);
   160 by (rtac ballI 1);
   161 by (etac llist.elim 1);
   162 by (asm_simp_tac flip_ss 1);
   163 by (asm_simp_tac flip_ss 2);
   164 by (rewrite_goals_tac ([QInl_def,QInr_def]@llist.con_defs));
   165 (*LNil case*)
   166 by (fast_tac flip_cs 1);
   167 (*LCons case*)
   168 by (safe_tac flip_cs);
   169 by (ALLGOALS (fast_tac (flip_cs addSEs [Ord_trans, make_elim bspec])));
   170 val flip_llist_quniv_lemma = result();
   171 
   172 goal LList.thy "!!l. l: llist(bool) ==> flip(l) : quniv(bool)";
   173 by (rtac (flip_llist_quniv_lemma RS bspec RS Int_Vset_subset RS qunivI) 1);
   174 by (REPEAT (assume_tac 1));
   175 val flip_in_quniv = result();
   176 
   177 val [prem] = goal LList.thy "l : llist(bool) ==> flip(l): llist(bool)";
   178 by (res_inst_tac [("X", "{flip(l) . l:llist(bool)}")]
   179        llist.coinduct 1);
   180 by (rtac (prem RS RepFunI) 1);
   181 by (fast_tac (ZF_cs addSIs [flip_in_quniv]) 1);
   182 by (etac RepFunE 1);
   183 by (etac llist.elim 1);
   184 by (asm_simp_tac flip_ss 1);
   185 by (asm_simp_tac flip_ss 1);
   186 by (fast_tac (ZF_cs addSIs [not_type]) 1);
   187 val flip_type = result();
   188 
   189 val [prem] = goal LList.thy
   190     "l : llist(bool) ==> flip(flip(l)) = l";
   191 by (res_inst_tac [("X1", "{<flip(flip(l)),l> . l:llist(bool)}")]
   192        (lleq.coinduct RS lleq_implies_equal) 1);
   193 by (rtac (prem RS RepFunI) 1);
   194 by (fast_tac (ZF_cs addSIs [flip_type]) 1);
   195 by (etac RepFunE 1);
   196 by (etac llist.elim 1);
   197 by (asm_simp_tac flip_ss 1);
   198 by (asm_simp_tac (flip_ss addsimps [flip_type, not_not]) 1);
   199 by (fast_tac (ZF_cs addSIs [not_type]) 1);
   200 val flip_flip = result();