1 (* Title: ZF/ex/CoUnit.ML |
1 (* Title: ZF/ex/CoUnit.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1994 University of Cambridge |
4 Copyright 1994 University of Cambridge |
5 |
5 |
6 Trivial codatatype definitions, one of which goes wrong! |
6 Trivial codatatype definitions, one of which goes wrong! |
7 |
7 |
8 See discussion in |
8 See discussion in |
57 by (safe_tac subset_cs); |
57 by (safe_tac subset_cs); |
58 by (etac counit2.elim 1); |
58 by (etac counit2.elim 1); |
59 by (etac counit2.elim 1); |
59 by (etac counit2.elim 1); |
60 by (rewrite_goals_tac counit2.con_defs); |
60 by (rewrite_goals_tac counit2.con_defs); |
61 val lleq_cs = subset_cs |
61 val lleq_cs = subset_cs |
62 addSIs [QPair_Int_Vset_subset_UN RS subset_trans, QPair_mono] |
62 addSIs [QPair_Int_Vset_subset_UN RS subset_trans, QPair_mono] |
63 addSEs [Ord_in_Ord, Pair_inject]; |
63 addSEs [Ord_in_Ord, Pair_inject]; |
64 by (fast_tac lleq_cs 1); |
64 by (fast_tac lleq_cs 1); |
65 qed "counit2_Int_Vset_subset_lemma"; |
65 qed "counit2_Int_Vset_subset_lemma"; |
66 |
66 |
67 val counit2_Int_Vset_subset = standard |
67 val counit2_Int_Vset_subset = standard |
68 (counit2_Int_Vset_subset_lemma RS spec RS spec RS mp); |
68 (counit2_Int_Vset_subset_lemma RS spec RS spec RS mp); |
69 |
69 |
70 goal CoUnit.thy "!!x y. [| x: counit2; y: counit2 |] ==> x=y"; |
70 goal CoUnit.thy "!!x y. [| x: counit2; y: counit2 |] ==> x=y"; |
71 by (rtac equalityI 1); |
71 by (rtac equalityI 1); |
72 by (REPEAT (ares_tac [conjI, counit2_Int_Vset_subset RS Int_Vset_subset] 1)); |
72 by (REPEAT (ares_tac [conjI, counit2_Int_Vset_subset RS Int_Vset_subset] 1)); |
73 qed "counit2_implies_equal"; |
73 qed "counit2_implies_equal"; |