author | paulson |
Fri, 13 Oct 2000 11:15:56 +0200 | |
changeset 10216 | e928bdf62014 |
parent 6141 | a6922171b396 |
child 11316 | b4e71bd751e4 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/ex/CoUnit.ML |
365 | 2 |
ID: $Id$ |
1461 | 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 |
||
13 |
(*USELESS because folding on Con(?xa) == ?xa fails*) |
|
6141 | 14 |
val ConE = counit.mk_cases "Con(x) : counit"; |
365 | 15 |
|
16 |
(*Proving freeness results*) |
|
515 | 17 |
val Con_iff = counit.mk_free "Con(x)=Con(y) <-> x=y"; |
365 | 18 |
|
19 |
(*Should be a singleton, not everything!*) |
|
5068 | 20 |
Goal "counit = quniv(0)"; |
515 | 21 |
by (rtac (counit.dom_subset RS equalityI) 1); |
365 | 22 |
by (rtac subsetI 1); |
515 | 23 |
by (etac counit.coinduct 1); |
365 | 24 |
by (rtac subset_refl 1); |
515 | 25 |
by (rewrite_goals_tac counit.con_defs); |
2469 | 26 |
by (Fast_tac 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
27 |
qed "counit_eq_univ"; |
365 | 28 |
|
29 |
||
30 |
(*A similar example, but the constructor is non-degenerate and it works! |
|
31 |
The resulting set is a singleton. |
|
32 |
*) |
|
33 |
||
6141 | 34 |
val Con2E = counit2.mk_cases "Con2(x,y) : counit2"; |
365 | 35 |
|
36 |
(*Proving freeness results*) |
|
515 | 37 |
val Con2_iff = counit2.mk_free "Con2(x,y)=Con2(x',y') <-> x=x' & y=y'"; |
365 | 38 |
|
5068 | 39 |
Goalw counit2.con_defs "bnd_mono(univ(0), %x. Con2(x,x))"; |
365 | 40 |
by (rtac bnd_monoI 1); |
41 |
by (REPEAT (ares_tac [subset_refl, QPair_subset_univ, QPair_mono] 1)); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
42 |
qed "Con2_bnd_mono"; |
365 | 43 |
|
5068 | 44 |
Goal "lfp(univ(0), %x. Con2(x,x)) : counit2"; |
515 | 45 |
by (rtac (singletonI RS counit2.coinduct) 1); |
365 | 46 |
by (rtac (qunivI RS singleton_subsetI) 1); |
47 |
by (rtac ([lfp_subset, empty_subsetI RS univ_mono] MRS subset_trans) 1); |
|
10216 | 48 |
by (fast_tac (claset() addSIs [Con2_bnd_mono RS lfp_unfold]) 1); |
760 | 49 |
qed "lfp_Con2_in_counit2"; |
365 | 50 |
|
51 |
(*Lemma for proving finality. Borrowed from ex/llist_eq.ML!*) |
|
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
52 |
Goal "Ord(i) ==> ALL x y. x: counit2 & y: counit2 --> x Int Vset(i) <= y"; |
365 | 53 |
by (etac trans_induct 1); |
54 |
by (safe_tac subset_cs); |
|
515 | 55 |
by (etac counit2.elim 1); |
56 |
by (etac counit2.elim 1); |
|
57 |
by (rewrite_goals_tac counit2.con_defs); |
|
2469 | 58 |
by (fast_tac (subset_cs |
59 |
addSIs [QPair_Int_Vset_subset_UN RS subset_trans, QPair_mono] |
|
60 |
addSEs [Ord_in_Ord, Pair_inject]) 1); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
61 |
qed "counit2_Int_Vset_subset_lemma"; |
365 | 62 |
|
63 |
val counit2_Int_Vset_subset = standard |
|
1461 | 64 |
(counit2_Int_Vset_subset_lemma RS spec RS spec RS mp); |
365 | 65 |
|
5137 | 66 |
Goal "[| x: counit2; y: counit2 |] ==> x=y"; |
365 | 67 |
by (rtac equalityI 1); |
68 |
by (REPEAT (ares_tac [conjI, counit2_Int_Vset_subset RS Int_Vset_subset] 1)); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
69 |
qed "counit2_implies_equal"; |
365 | 70 |
|
5068 | 71 |
Goal "counit2 = {lfp(univ(0), %x. Con2(x,x))}"; |
365 | 72 |
by (rtac equalityI 1); |
73 |
by (rtac (lfp_Con2_in_counit2 RS singleton_subsetI) 2); |
|
74 |
by (rtac subsetI 1); |
|
75 |
by (dtac (lfp_Con2_in_counit2 RS counit2_implies_equal) 1); |
|
76 |
by (etac subst 1); |
|
77 |
by (rtac singletonI 1); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
78 |
qed "counit2_eq_univ"; |