515

1 
(* Title: ZF/ex/CoUnit.ML

365

2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory

515

4 
Copyright 1994 University of Cambridge

365

5 


6 
Trivial codatatype definitions, one of which goes wrong!


7 

515

8 
See discussion in


9 
L C Paulson. A Concrete Final Coalgebra Theorem for ZF Set Theory.


10 
Report 334, Cambridge University Computer Laboratory. 1994.

365

11 
*)


12 

515

13 
open CoUnit;

365

14 


15 
(*USELESS because folding on Con(?xa) == ?xa fails*)

515

16 
val ConE = counit.mk_cases counit.con_defs "Con(x) : counit";

365

17 


18 
(*Proving freeness results*)

515

19 
val Con_iff = counit.mk_free "Con(x)=Con(y) <> x=y";

365

20 


21 
(*Should be a singleton, not everything!*)


22 
goal CoUnit.thy "counit = quniv(0)";

515

23 
by (rtac (counit.dom_subset RS equalityI) 1);

365

24 
by (rtac subsetI 1);

515

25 
by (etac counit.coinduct 1);

365

26 
by (rtac subset_refl 1);

515

27 
by (rewrite_goals_tac counit.con_defs);

365

28 
by (fast_tac ZF_cs 1);


29 
val counit_eq_univ = result();


30 


31 


32 
(*A similar example, but the constructor is nondegenerate and it works!


33 
The resulting set is a singleton.


34 
*)


35 

515

36 
val Con2E = counit2.mk_cases counit2.con_defs "Con2(x,y) : counit2";

365

37 


38 
(*Proving freeness results*)

515

39 
val Con2_iff = counit2.mk_free "Con2(x,y)=Con2(x',y') <> x=x' & y=y'";

365

40 

515

41 
goalw CoUnit.thy counit2.con_defs "bnd_mono(univ(0), %x. Con2(x,x))";

365

42 
by (rtac bnd_monoI 1);


43 
by (REPEAT (ares_tac [subset_refl, QPair_subset_univ, QPair_mono] 1));


44 
val Con2_bnd_mono = result();


45 

515

46 
goal CoUnit.thy "lfp(univ(0), %x. Con2(x,x)) : counit2";


47 
by (rtac (singletonI RS counit2.coinduct) 1);

365

48 
by (rtac (qunivI RS singleton_subsetI) 1);


49 
by (rtac ([lfp_subset, empty_subsetI RS univ_mono] MRS subset_trans) 1);


50 
by (fast_tac (ZF_cs addSIs [Con2_bnd_mono RS lfp_Tarski]) 1);


51 
val lfp_Con2_in_counit2 = result();


52 


53 
(*Lemma for proving finality. Borrowed from ex/llist_eq.ML!*)

515

54 
goal CoUnit.thy

365

55 
"!!i. Ord(i) ==> ALL x y. x: counit2 & y: counit2 > x Int Vset(i) <= y";


56 
by (etac trans_induct 1);


57 
by (safe_tac subset_cs);

515

58 
by (etac counit2.elim 1);


59 
by (etac counit2.elim 1);


60 
by (rewrite_goals_tac counit2.con_defs);

527

61 
val lleq_cs = subset_cs


62 
addSIs [QPair_Int_Vset_subset_UN RS subset_trans, QPair_mono]


63 
addSEs [Ord_in_Ord, Pair_inject];

365

64 
by (fast_tac lleq_cs 1);


65 
val counit2_Int_Vset_subset_lemma = result();


66 


67 
val counit2_Int_Vset_subset = standard


68 
(counit2_Int_Vset_subset_lemma RS spec RS spec RS mp);


69 

515

70 
goal CoUnit.thy "!!x y. [ x: counit2; y: counit2 ] ==> x=y";

365

71 
by (rtac equalityI 1);


72 
by (REPEAT (ares_tac [conjI, counit2_Int_Vset_subset RS Int_Vset_subset] 1));


73 
val counit2_implies_equal = result();


74 

515

75 
goal CoUnit.thy "counit2 = {lfp(univ(0), %x. Con2(x,x))}";

365

76 
by (rtac equalityI 1);


77 
by (rtac (lfp_Con2_in_counit2 RS singleton_subsetI) 2);


78 
by (rtac subsetI 1);


79 
by (dtac (lfp_Con2_in_counit2 RS counit2_implies_equal) 1);


80 
by (etac subst 1);


81 
by (rtac singletonI 1);


82 
val counit2_eq_univ = result();
