src/ZF/ex/CoUnit.ML
author lcp
Fri Aug 12 12:28:46 1994 +0200 (1994-08-12)
changeset 515 abcc438e7c27
parent 477 53fc8ad84b33
child 527 35c70ab82940
permissions -rw-r--r--
installation of new inductive/datatype sections
lcp@515
     1
(*  Title: 	ZF/ex/CoUnit.ML
lcp@365
     2
    ID:         $Id$
lcp@365
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@515
     4
    Copyright   1994  University of Cambridge
lcp@365
     5
lcp@365
     6
Trivial codatatype definitions, one of which goes wrong!
lcp@365
     7
lcp@515
     8
See discussion in 
lcp@515
     9
  L C Paulson.  A Concrete Final Coalgebra Theorem for ZF Set Theory.
lcp@515
    10
  Report 334,  Cambridge University Computer Laboratory.  1994.
lcp@365
    11
*)
lcp@365
    12
lcp@515
    13
open CoUnit;
lcp@365
    14
  
lcp@365
    15
(*USELESS because folding on Con(?xa) == ?xa fails*)
lcp@515
    16
val ConE = counit.mk_cases counit.con_defs "Con(x) : counit";
lcp@365
    17
lcp@365
    18
(*Proving freeness results*)
lcp@515
    19
val Con_iff = counit.mk_free "Con(x)=Con(y) <-> x=y";
lcp@365
    20
lcp@365
    21
(*Should be a singleton, not everything!*)
lcp@365
    22
goal CoUnit.thy "counit = quniv(0)";
lcp@515
    23
by (rtac (counit.dom_subset RS equalityI) 1);
lcp@365
    24
by (rtac subsetI 1);
lcp@515
    25
by (etac counit.coinduct 1);
lcp@365
    26
by (rtac subset_refl 1);
lcp@515
    27
by (rewrite_goals_tac counit.con_defs);
lcp@365
    28
by (fast_tac ZF_cs 1);
lcp@365
    29
val counit_eq_univ = result();
lcp@365
    30
lcp@365
    31
lcp@365
    32
(*A similar example, but the constructor is non-degenerate and it works!
lcp@365
    33
  The resulting set is a singleton.
lcp@365
    34
*)
lcp@365
    35
lcp@515
    36
val Con2E = counit2.mk_cases counit2.con_defs "Con2(x,y) : counit2";
lcp@365
    37
lcp@365
    38
(*Proving freeness results*)
lcp@515
    39
val Con2_iff = counit2.mk_free "Con2(x,y)=Con2(x',y') <-> x=x' & y=y'";
lcp@365
    40
lcp@515
    41
goalw CoUnit.thy counit2.con_defs "bnd_mono(univ(0), %x. Con2(x,x))";
lcp@365
    42
by (rtac bnd_monoI 1);
lcp@365
    43
by (REPEAT (ares_tac [subset_refl, QPair_subset_univ, QPair_mono] 1));
lcp@365
    44
val Con2_bnd_mono = result();
lcp@365
    45
lcp@515
    46
goal CoUnit.thy "lfp(univ(0), %x. Con2(x,x)) : counit2";
lcp@515
    47
by (rtac (singletonI RS counit2.coinduct) 1);
lcp@365
    48
by (rtac (qunivI RS singleton_subsetI) 1);
lcp@365
    49
by (rtac ([lfp_subset, empty_subsetI RS univ_mono] MRS subset_trans) 1);
lcp@365
    50
by (fast_tac (ZF_cs addSIs [Con2_bnd_mono RS lfp_Tarski]) 1);
lcp@365
    51
val lfp_Con2_in_counit2 = result();
lcp@365
    52
lcp@365
    53
(*Lemma for proving finality.  Borrowed from ex/llist_eq.ML!*)
lcp@515
    54
goal CoUnit.thy
lcp@365
    55
    "!!i. Ord(i) ==> ALL x y. x: counit2 & y: counit2 --> x Int Vset(i) <= y";
lcp@365
    56
by (etac trans_induct 1);
lcp@365
    57
by (safe_tac subset_cs);
lcp@515
    58
by (etac counit2.elim 1);
lcp@515
    59
by (etac counit2.elim 1);
lcp@515
    60
by (rewrite_goals_tac counit2.con_defs);
lcp@365
    61
by (fast_tac lleq_cs 1);
lcp@365
    62
val counit2_Int_Vset_subset_lemma = result();
lcp@365
    63
lcp@365
    64
val counit2_Int_Vset_subset = standard
lcp@365
    65
	(counit2_Int_Vset_subset_lemma RS spec RS spec RS mp);
lcp@365
    66
lcp@515
    67
goal CoUnit.thy "!!x y. [| x: counit2;  y: counit2 |] ==> x=y";
lcp@365
    68
by (rtac equalityI 1);
lcp@365
    69
by (REPEAT (ares_tac [conjI, counit2_Int_Vset_subset RS Int_Vset_subset] 1));
lcp@365
    70
val counit2_implies_equal = result();
lcp@365
    71
lcp@515
    72
goal CoUnit.thy "counit2 = {lfp(univ(0), %x. Con2(x,x))}";
lcp@365
    73
by (rtac equalityI 1);
lcp@365
    74
by (rtac (lfp_Con2_in_counit2 RS singleton_subsetI) 2);
lcp@365
    75
by (rtac subsetI 1);
lcp@365
    76
by (dtac (lfp_Con2_in_counit2 RS counit2_implies_equal) 1);
lcp@365
    77
by (etac subst 1);
lcp@365
    78
by (rtac singletonI 1);
lcp@365
    79
val counit2_eq_univ = result();