src/ZF/ex/llist_eq.ML
author lcp
Tue Aug 16 18:58:42 1994 +0200 (1994-08-16)
changeset 532 851df239ac8b
parent 279 7738aed3f84d
permissions -rw-r--r--
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
     1 (*  Title: 	ZF/ex/llist_eq.ML
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 Equality for llist(A) as a greatest fixed point
     7 ***)
     8 
     9 (*Previously used <*> in the domain and variant pairs as elements.  But
    10   standard pairs work just as well.  To use variant pairs, must change prefix
    11   a q/Q to the Sigma, Pair and converse rules.*)
    12 
    13 structure LList_Eq = CoInductive_Fun
    14  (val thy = LList.thy addconsts [(["lleq"],"i=>i")]
    15   val rec_doms   = [("lleq", "llist(A) * llist(A)")]
    16   val sintrs     = 
    17         ["<LNil, LNil> : lleq(A)",
    18          "[| a:A; <l,l'>: lleq(A) |] ==> <LCons(a,l), LCons(a,l')>: lleq(A)"]
    19   val monos      = []
    20   val con_defs   = []
    21   val type_intrs = LList.intrs @ [SigmaI]
    22   val type_elims = [SigmaE2]);
    23 
    24 (** Alternatives for above:
    25   val con_defs = LList.con_defs
    26   val type_intrs = codatatype_intrs
    27   val type_elims = [quniv_QPair_E]
    28 **)
    29 
    30 val lleq_cs = subset_cs
    31 	addSIs [QPair_Int_Vset_subset_UN RS subset_trans, QPair_mono]
    32         addSEs [Ord_in_Ord, Pair_inject];
    33 
    34 (*Lemma for proving finality.  Unfold the lazy list; use induction hypothesis*)
    35 goal LList_Eq.thy
    36    "!!i. Ord(i) ==> ALL l l'. <l,l'> : lleq(A) --> l Int Vset(i) <= l'";
    37 by (etac trans_induct 1);
    38 by (REPEAT (resolve_tac [allI, impI] 1));
    39 by (etac LList_Eq.elim 1);
    40 by (rewrite_goals_tac (QInr_def::LList.con_defs));
    41 by (safe_tac lleq_cs);
    42 by (fast_tac (subset_cs addSEs [Ord_trans, make_elim bspec]) 1);
    43 val lleq_Int_Vset_subset_lemma = result();
    44 
    45 val lleq_Int_Vset_subset = standard
    46 	(lleq_Int_Vset_subset_lemma RS spec RS spec RS mp);
    47 
    48 
    49 (*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*)
    50 val [prem] = goal LList_Eq.thy "<l,l'> : lleq(A) ==> <l',l> : lleq(A)";
    51 by (rtac (prem RS converseI RS LList_Eq.coinduct) 1);
    52 by (rtac (LList_Eq.dom_subset RS converse_type) 1);
    53 by (safe_tac converse_cs);
    54 by (etac LList_Eq.elim 1);
    55 by (ALLGOALS (fast_tac qconverse_cs));
    56 val lleq_symmetric = result();
    57 
    58 goal LList_Eq.thy "!!l l'. <l,l'> : lleq(A) ==> l=l'";
    59 by (rtac equalityI 1);
    60 by (REPEAT (ares_tac [lleq_Int_Vset_subset RS Int_Vset_subset] 1
    61      ORELSE etac lleq_symmetric 1));
    62 val lleq_implies_equal = result();
    63 
    64 val [eqprem,lprem] = goal LList_Eq.thy
    65     "[| l=l';  l: llist(A) |] ==> <l,l'> : lleq(A)";
    66 by (res_inst_tac [("X", "{<l,l>. l: llist(A)}")] LList_Eq.coinduct 1);
    67 by (rtac (lprem RS RepFunI RS (eqprem RS subst)) 1);
    68 by (safe_tac qpair_cs);
    69 by (etac LList.elim 1);
    70 by (ALLGOALS (fast_tac pair_cs));
    71 val equal_llist_implies_leq = result();
    72