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