95
|
1 |
(* Title: ZF/ex/counit.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1993 University of Cambridge
|
|
5 |
|
120
|
6 |
Trivial codatatype definitions, one of which goes wrong!
|
95
|
7 |
|
120
|
8 |
Need to find sufficient conditions for codatatypes to work correctly!
|
95
|
9 |
*)
|
|
10 |
|
|
11 |
(*This degenerate definition does not work well because the one constructor's
|
173
|
12 |
definition is trivial! The same thing occurs with Aczel's Special Final
|
|
13 |
Coalgebra Theorem
|
95
|
14 |
*)
|
120
|
15 |
structure CoUnit = CoDatatype_Fun
|
95
|
16 |
(val thy = QUniv.thy;
|
|
17 |
val rec_specs =
|
|
18 |
[("counit", "quniv(0)",
|
|
19 |
[(["Con"], "i=>i")])];
|
|
20 |
val rec_styp = "i";
|
|
21 |
val ext = None
|
|
22 |
val sintrs = ["x: counit ==> Con(x) : counit"];
|
|
23 |
val monos = [];
|
120
|
24 |
val type_intrs = codatatype_intrs
|
|
25 |
val type_elims = codatatype_elims);
|
95
|
26 |
|
|
27 |
val [ConI] = CoUnit.intrs;
|
|
28 |
|
|
29 |
(*USELESS because folding on Con(?xa) == ?xa fails*)
|
|
30 |
val ConE = CoUnit.mk_cases CoUnit.con_defs "Con(x) : counit";
|
|
31 |
|
|
32 |
(*Proving freeness results*)
|
|
33 |
val Con_iff = CoUnit.mk_free "Con(x)=Con(y) <-> x=y";
|
|
34 |
|
|
35 |
(*Should be a singleton, not everything!*)
|
|
36 |
goal CoUnit.thy "counit = quniv(0)";
|
|
37 |
by (rtac (CoUnit.dom_subset RS equalityI) 1);
|
|
38 |
by (rtac subsetI 1);
|
120
|
39 |
by (etac CoUnit.coinduct 1);
|
95
|
40 |
by (rtac subset_refl 1);
|
|
41 |
by (rewrite_goals_tac CoUnit.con_defs);
|
|
42 |
by (fast_tac ZF_cs 1);
|
|
43 |
val counit_eq_univ = result();
|
|
44 |
|
|
45 |
|
|
46 |
(*****************************************************************)
|
|
47 |
|
|
48 |
(*A similar example, but the constructor is non-degenerate and it works!
|
|
49 |
The resulting set is a singleton.
|
|
50 |
*)
|
|
51 |
|
120
|
52 |
structure CoUnit2 = CoDatatype_Fun
|
95
|
53 |
(val thy = QUniv.thy;
|
|
54 |
val rec_specs =
|
|
55 |
[("counit2", "quniv(0)",
|
|
56 |
[(["Con2"], "[i,i]=>i")])];
|
|
57 |
val rec_styp = "i";
|
|
58 |
val ext = None
|
|
59 |
val sintrs = ["[| x: counit2; y: counit2 |] ==> Con2(x,y) : counit2"];
|
|
60 |
val monos = [];
|
120
|
61 |
val type_intrs = codatatype_intrs
|
|
62 |
val type_elims = codatatype_elims);
|
95
|
63 |
|
|
64 |
val [Con2I] = CoUnit2.intrs;
|
|
65 |
|
|
66 |
val Con2E = CoUnit2.mk_cases CoUnit2.con_defs "Con2(x,y) : counit2";
|
|
67 |
|
|
68 |
(*Proving freeness results*)
|
|
69 |
val Con2_iff = CoUnit2.mk_free "Con2(x,y)=Con2(x',y') <-> x=x' & y=y'";
|
|
70 |
|
|
71 |
goalw CoUnit2.thy CoUnit2.con_defs "bnd_mono(univ(0), %x. Con2(x,x))";
|
|
72 |
by (rtac bnd_monoI 1);
|
|
73 |
by (REPEAT (ares_tac [subset_refl, QPair_subset_univ, QPair_mono] 1));
|
|
74 |
val Con2_bnd_mono = result();
|
|
75 |
|
|
76 |
goal CoUnit2.thy "lfp(univ(0), %x. Con2(x,x)) : counit2";
|
120
|
77 |
by (rtac (singletonI RS CoUnit2.coinduct) 1);
|
95
|
78 |
by (rtac (qunivI RS singleton_subsetI) 1);
|
|
79 |
by (rtac ([lfp_subset, empty_subsetI RS univ_mono] MRS subset_trans) 1);
|
|
80 |
by (fast_tac (ZF_cs addSIs [Con2_bnd_mono RS lfp_Tarski]) 1);
|
|
81 |
val lfp_Con2_in_counit2 = result();
|
|
82 |
|
173
|
83 |
(*Lemma for proving finality. Borrowed from ex/llist_eq.ML!*)
|
95
|
84 |
goal CoUnit2.thy
|
|
85 |
"!!i. Ord(i) ==> ALL x y. x: counit2 & y: counit2 --> x Int Vset(i) <= y";
|
|
86 |
by (etac trans_induct 1);
|
|
87 |
by (safe_tac subset_cs);
|
|
88 |
by (etac CoUnit2.elim 1);
|
|
89 |
by (etac CoUnit2.elim 1);
|
|
90 |
by (rewrite_goals_tac CoUnit2.con_defs);
|
|
91 |
by (fast_tac lleq_cs 1);
|
|
92 |
val counit2_Int_Vset_subset_lemma = result();
|
|
93 |
|
|
94 |
val counit2_Int_Vset_subset = standard
|
|
95 |
(counit2_Int_Vset_subset_lemma RS spec RS spec RS mp);
|
|
96 |
|
|
97 |
goal CoUnit2.thy "!!x y. [| x: counit2; y: counit2 |] ==> x=y";
|
|
98 |
by (rtac equalityI 1);
|
|
99 |
by (REPEAT (ares_tac [conjI, counit2_Int_Vset_subset RS Int_Vset_subset] 1));
|
|
100 |
val counit2_implies_equal = result();
|
|
101 |
|
|
102 |
goal CoUnit2.thy "counit2 = {lfp(univ(0), %x. Con2(x,x))}";
|
|
103 |
by (rtac equalityI 1);
|
|
104 |
by (rtac (lfp_Con2_in_counit2 RS singleton_subsetI) 2);
|
|
105 |
by (rtac subsetI 1);
|
|
106 |
by (dtac (lfp_Con2_in_counit2 RS counit2_implies_equal) 1);
|
|
107 |
by (etac subst 1);
|
|
108 |
by (rtac singletonI 1);
|
|
109 |
val counit2_eq_univ = result();
|