--- a/src/ZF/ex/CoUnit.ML Fri Nov 16 22:09:44 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,78 +0,0 @@
-(* Title: ZF/ex/CoUnit.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1994 University of Cambridge
-
-Trivial codatatype definitions, one of which goes wrong!
-
-See discussion in
- L C Paulson. A Concrete Final Coalgebra Theorem for ZF Set Theory.
- Report 334, Cambridge University Computer Laboratory. 1994.
-*)
-
-(*USELESS because folding on Con(?xa) == ?xa fails*)
-val ConE = counit.mk_cases "Con(x) \\<in> counit";
-
-(*Proving freeness results*)
-val Con_iff = counit.mk_free "Con(x)=Con(y) <-> x=y";
-
-(*Should be a singleton, not everything!*)
-Goal "counit = quniv(0)";
-by (rtac (counit.dom_subset RS equalityI) 1);
-by (rtac subsetI 1);
-by (etac counit.coinduct 1);
-by (rtac subset_refl 1);
-by (rewrite_goals_tac counit.con_defs);
-by (Fast_tac 1);
-qed "counit_eq_univ";
-
-
-(*A similar example, but the constructor is non-degenerate and it works!
- The resulting set is a singleton.
-*)
-
-val Con2E = counit2.mk_cases "Con2(x,y) \\<in> counit2";
-
-(*Proving freeness results*)
-val Con2_iff = counit2.mk_free "Con2(x,y)=Con2(x',y') <-> x=x' & y=y'";
-
-Goalw counit2.con_defs "bnd_mono(univ(0), %x. Con2(x,x))";
-by (rtac bnd_monoI 1);
-by (REPEAT (ares_tac [subset_refl, QPair_subset_univ, QPair_mono] 1));
-qed "Con2_bnd_mono";
-
-Goal "lfp(univ(0), %x. Con2(x,x)) \\<in> counit2";
-by (rtac (singletonI RS counit2.coinduct) 1);
-by (rtac (qunivI RS singleton_subsetI) 1);
-by (rtac ([lfp_subset, empty_subsetI RS univ_mono] MRS subset_trans) 1);
-by (fast_tac (claset() addSIs [Con2_bnd_mono RS lfp_unfold]) 1);
-qed "lfp_Con2_in_counit2";
-
-(*Lemma for proving finality. Borrowed from ex/llist_eq.ML!*)
-Goal "Ord(i) ==> \\<forall>x y. x \\<in> counit2 & y \\<in> counit2 --> x Int Vset(i) \\<subseteq> y";
-by (etac trans_induct 1);
-by (safe_tac subset_cs);
-by (etac counit2.elim 1);
-by (etac counit2.elim 1);
-by (rewrite_goals_tac counit2.con_defs);
-by (fast_tac (subset_cs
- addSIs [QPair_Int_Vset_subset_UN RS subset_trans, QPair_mono]
- addSEs [Ord_in_Ord, Pair_inject]) 1);
-qed "counit2_Int_Vset_subset_lemma";
-
-val counit2_Int_Vset_subset = standard
- (counit2_Int_Vset_subset_lemma RS spec RS spec RS mp);
-
-Goal "[| x \\<in> counit2; y \\<in> counit2 |] ==> x=y";
-by (rtac equalityI 1);
-by (REPEAT (ares_tac [conjI, counit2_Int_Vset_subset RS Int_Vset_subset] 1));
-qed "counit2_implies_equal";
-
-Goal "counit2 = {lfp(univ(0), %x. Con2(x,x))}";
-by (rtac equalityI 1);
-by (rtac (lfp_Con2_in_counit2 RS singleton_subsetI) 2);
-by (rtac subsetI 1);
-by (dtac (lfp_Con2_in_counit2 RS counit2_implies_equal) 1);
-by (etac subst 1);
-by (rtac singletonI 1);
-qed "counit2_eq_univ";
--- a/src/ZF/ex/CoUnit.thy Fri Nov 16 22:09:44 2001 +0100
+++ b/src/ZF/ex/CoUnit.thy Fri Nov 16 22:10:27 2001 +0100
@@ -2,33 +2,102 @@
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
-
-Trivial codatatype definitions, one of which goes wrong!
-
-See discussion in
- L C Paulson. A Concrete Final Coalgebra Theorem for ZF Set Theory.
- Report 334, Cambridge University Computer Laboratory. 1994.
*)
-CoUnit = Main +
+header {* Trivial codatatype definitions, one of which goes wrong! *}
+
+theory CoUnit = Main:
-(*This degenerate definition does not work well because the one constructor's
- definition is trivial! The same thing occurs with Aczel's Special Final
- Coalgebra Theorem
-*)
+text {*
+ See discussion in: L C Paulson. A Concrete Final Coalgebra Theorem
+ for ZF Set Theory. Report 334, Cambridge University Computer
+ Laboratory. 1994.
+
+ \bigskip
+
+ This degenerate definition does not work well because the one
+ constructor's definition is trivial! The same thing occurs with
+ Aczel's Special Final Coalgebra Theorem.
+*}
+
consts
counit :: i
codatatype
- "counit" = Con ("x \\<in> counit")
+ "counit" = Con ("x \<in> counit")
+
+inductive_cases ConE: "Con(x) \<in> counit"
+ -- {* USELESS because folding on @{term "Con(xa) == xa"} fails. *}
+
+lemma Con_iff: "Con(x) = Con(y) <-> x = y"
+ -- {* Proving freeness results. *}
+ by (auto elim!: counit.free_elims)
+
+lemma counit_eq_univ: "counit = quniv(0)"
+ -- {* Should be a singleton, not everything! *}
+ apply (rule counit.dom_subset [THEN equalityI])
+ apply (rule subsetI)
+ apply (erule counit.coinduct)
+ apply (rule subset_refl)
+ apply (unfold counit.con_defs)
+ apply fast
+ done
-(*A similar example, but the constructor is non-degenerate and it works!
- The resulting set is a singleton.
-*)
+text {*
+ \medskip A similar example, but the constructor is non-degenerate
+ and it works! The resulting set is a singleton.
+*}
consts
counit2 :: i
codatatype
- "counit2" = Con2 ("x \\<in> counit2", "y \\<in> counit2")
+ "counit2" = Con2 ("x \<in> counit2", "y \<in> counit2")
+
+
+inductive_cases Con2E: "Con2(x, y) \<in> counit2"
+
+lemma Con2_iff: "Con2(x, y) = Con2(x', y') <-> x = x' & y = y'"
+ -- {* Proving freeness results. *}
+ by (fast elim!: counit2.free_elims)
+
+lemma Con2_bnd_mono: "bnd_mono(univ(0), %x. Con2(x, x))"
+ apply (unfold counit2.con_defs)
+ apply (rule bnd_monoI)
+ apply (assumption | rule subset_refl QPair_subset_univ QPair_mono)+
+ done
+
+lemma lfp_Con2_in_counit2: "lfp(univ(0), %x. Con2(x,x)) \<in> counit2"
+ apply (rule singletonI [THEN counit2.coinduct])
+ apply (rule qunivI [THEN singleton_subsetI])
+ apply (rule subset_trans [OF lfp_subset empty_subsetI [THEN univ_mono]])
+ apply (fast intro!: Con2_bnd_mono [THEN lfp_unfold])
+ done
+
+lemma counit2_Int_Vset_subset [rule_format]:
+ "Ord(i) ==> \<forall>x y. x \<in> counit2 --> y \<in> counit2 --> x Int Vset(i) \<subseteq> y"
+ -- {* Lemma for proving finality. *}
+ apply (erule trans_induct)
+ apply (tactic "safe_tac subset_cs")
+ apply (erule counit2.cases)
+ apply (erule counit2.cases)
+ apply (unfold counit2.con_defs)
+ apply (tactic {* fast_tac (subset_cs
+ addSIs [QPair_Int_Vset_subset_UN RS subset_trans, QPair_mono]
+ addSEs [Ord_in_Ord, Pair_inject]) 1 *})
+ done
+
+lemma counit2_implies_equal: "[| x \<in> counit2; y \<in> counit2 |] ==> x = y"
+ apply (rule equalityI)
+ apply (assumption | rule conjI counit2_Int_Vset_subset [THEN Int_Vset_subset])+
+ done
+
+lemma counit2_eq_univ: "counit2 = {lfp(univ(0), %x. Con2(x,x))}"
+ apply (rule equalityI)
+ apply (rule_tac [2] lfp_Con2_in_counit2 [THEN singleton_subsetI])
+ apply (rule subsetI)
+ apply (drule lfp_Con2_in_counit2 [THEN counit2_implies_equal])
+ apply (erule subst)
+ apply (rule singletonI)
+ done
end