1 (* Title: ZF/ex/CoUnit.thy |
1 (* Title: ZF/ex/CoUnit.thy |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Copyright 1994 University of Cambridge |
3 Copyright 1994 University of Cambridge |
4 *) |
4 *) |
5 |
5 |
6 section {* Trivial codatatype definitions, one of which goes wrong! *} |
6 section \<open>Trivial codatatype definitions, one of which goes wrong!\<close> |
7 |
7 |
8 theory CoUnit imports Main begin |
8 theory CoUnit imports Main begin |
9 |
9 |
10 text {* |
10 text \<open> |
11 See discussion in: L C Paulson. A Concrete Final Coalgebra Theorem |
11 See discussion in: L C Paulson. A Concrete Final Coalgebra Theorem |
12 for ZF Set Theory. Report 334, Cambridge University Computer |
12 for ZF Set Theory. Report 334, Cambridge University Computer |
13 Laboratory. 1994. |
13 Laboratory. 1994. |
14 |
14 |
15 \bigskip |
15 \bigskip |
16 |
16 |
17 This degenerate definition does not work well because the one |
17 This degenerate definition does not work well because the one |
18 constructor's definition is trivial! The same thing occurs with |
18 constructor's definition is trivial! The same thing occurs with |
19 Aczel's Special Final Coalgebra Theorem. |
19 Aczel's Special Final Coalgebra Theorem. |
20 *} |
20 \<close> |
21 |
21 |
22 consts |
22 consts |
23 counit :: i |
23 counit :: i |
24 codatatype |
24 codatatype |
25 "counit" = Con ("x \<in> counit") |
25 "counit" = Con ("x \<in> counit") |
26 |
26 |
27 inductive_cases ConE: "Con(x) \<in> counit" |
27 inductive_cases ConE: "Con(x) \<in> counit" |
28 -- {* USELESS because folding on @{term "Con(xa) == xa"} fails. *} |
28 -- \<open>USELESS because folding on @{term "Con(xa) == xa"} fails.\<close> |
29 |
29 |
30 lemma Con_iff: "Con(x) = Con(y) \<longleftrightarrow> x = y" |
30 lemma Con_iff: "Con(x) = Con(y) \<longleftrightarrow> x = y" |
31 -- {* Proving freeness results. *} |
31 -- \<open>Proving freeness results.\<close> |
32 by (auto elim!: counit.free_elims) |
32 by (auto elim!: counit.free_elims) |
33 |
33 |
34 lemma counit_eq_univ: "counit = quniv(0)" |
34 lemma counit_eq_univ: "counit = quniv(0)" |
35 -- {* Should be a singleton, not everything! *} |
35 -- \<open>Should be a singleton, not everything!\<close> |
36 apply (rule counit.dom_subset [THEN equalityI]) |
36 apply (rule counit.dom_subset [THEN equalityI]) |
37 apply (rule subsetI) |
37 apply (rule subsetI) |
38 apply (erule counit.coinduct) |
38 apply (erule counit.coinduct) |
39 apply (rule subset_refl) |
39 apply (rule subset_refl) |
40 apply (unfold counit.con_defs) |
40 apply (unfold counit.con_defs) |
41 apply fast |
41 apply fast |
42 done |
42 done |
43 |
43 |
44 |
44 |
45 text {* |
45 text \<open> |
46 \medskip A similar example, but the constructor is non-degenerate |
46 \medskip A similar example, but the constructor is non-degenerate |
47 and it works! The resulting set is a singleton. |
47 and it works! The resulting set is a singleton. |
48 *} |
48 \<close> |
49 |
49 |
50 consts |
50 consts |
51 counit2 :: i |
51 counit2 :: i |
52 codatatype |
52 codatatype |
53 "counit2" = Con2 ("x \<in> counit2", "y \<in> counit2") |
53 "counit2" = Con2 ("x \<in> counit2", "y \<in> counit2") |
54 |
54 |
55 |
55 |
56 inductive_cases Con2E: "Con2(x, y) \<in> counit2" |
56 inductive_cases Con2E: "Con2(x, y) \<in> counit2" |
57 |
57 |
58 lemma Con2_iff: "Con2(x, y) = Con2(x', y') \<longleftrightarrow> x = x' & y = y'" |
58 lemma Con2_iff: "Con2(x, y) = Con2(x', y') \<longleftrightarrow> x = x' & y = y'" |
59 -- {* Proving freeness results. *} |
59 -- \<open>Proving freeness results.\<close> |
60 by (fast elim!: counit2.free_elims) |
60 by (fast elim!: counit2.free_elims) |
61 |
61 |
62 lemma Con2_bnd_mono: "bnd_mono(univ(0), %x. Con2(x, x))" |
62 lemma Con2_bnd_mono: "bnd_mono(univ(0), %x. Con2(x, x))" |
63 apply (unfold counit2.con_defs) |
63 apply (unfold counit2.con_defs) |
64 apply (rule bnd_monoI) |
64 apply (rule bnd_monoI) |
72 apply (fast intro!: Con2_bnd_mono [THEN lfp_unfold]) |
72 apply (fast intro!: Con2_bnd_mono [THEN lfp_unfold]) |
73 done |
73 done |
74 |
74 |
75 lemma counit2_Int_Vset_subset [rule_format]: |
75 lemma counit2_Int_Vset_subset [rule_format]: |
76 "Ord(i) ==> \<forall>x y. x \<in> counit2 \<longrightarrow> y \<in> counit2 \<longrightarrow> x \<inter> Vset(i) \<subseteq> y" |
76 "Ord(i) ==> \<forall>x y. x \<in> counit2 \<longrightarrow> y \<in> counit2 \<longrightarrow> x \<inter> Vset(i) \<subseteq> y" |
77 -- {* Lemma for proving finality. *} |
77 -- \<open>Lemma for proving finality.\<close> |
78 apply (erule trans_induct) |
78 apply (erule trans_induct) |
79 apply (tactic "safe_tac (put_claset subset_cs @{context})") |
79 apply (tactic "safe_tac (put_claset subset_cs @{context})") |
80 apply (erule counit2.cases) |
80 apply (erule counit2.cases) |
81 apply (erule counit2.cases) |
81 apply (erule counit2.cases) |
82 apply (unfold counit2.con_defs) |
82 apply (unfold counit2.con_defs) |
83 apply (tactic {* fast_tac (put_claset subset_cs @{context} |
83 apply (tactic \<open>fast_tac (put_claset subset_cs @{context} |
84 addSIs [@{thm QPair_Int_Vset_subset_UN} RS @{thm subset_trans}, @{thm QPair_mono}] |
84 addSIs [@{thm QPair_Int_Vset_subset_UN} RS @{thm subset_trans}, @{thm QPair_mono}] |
85 addSEs [@{thm Ord_in_Ord}, @{thm Pair_inject}]) 1 *}) |
85 addSEs [@{thm Ord_in_Ord}, @{thm Pair_inject}]) 1\<close>) |
86 done |
86 done |
87 |
87 |
88 lemma counit2_implies_equal: "[| x \<in> counit2; y \<in> counit2 |] ==> x = y" |
88 lemma counit2_implies_equal: "[| x \<in> counit2; y \<in> counit2 |] ==> x = y" |
89 apply (rule equalityI) |
89 apply (rule equalityI) |
90 apply (assumption | rule conjI counit2_Int_Vset_subset [THEN Int_Vset_subset])+ |
90 apply (assumption | rule conjI counit2_Int_Vset_subset [THEN Int_Vset_subset])+ |