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