# HG changeset patch # User wenzelm # Date 1005945027 -3600 # Node ID 9e5d3c96111a30c81fde70d2a2008a545bd5f056 # Parent c654c2c03f1d48de4e82a559db7f58125455b04e converted; diff -r c654c2c03f1d -r 9e5d3c96111a src/ZF/ex/CoUnit.ML --- 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) \\ 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) \\ 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)) \\ 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) ==> \\x y. x \\ counit2 & y \\ counit2 --> x Int Vset(i) \\ 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 \\ counit2; y \\ 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"; diff -r c654c2c03f1d -r 9e5d3c96111a src/ZF/ex/CoUnit.thy --- 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 \\ counit") + "counit" = Con ("x \ counit") + +inductive_cases ConE: "Con(x) \ 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 \\ counit2", "y \\ counit2") + "counit2" = Con2 ("x \ counit2", "y \ counit2") + + +inductive_cases Con2E: "Con2(x, y) \ 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)) \ 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) ==> \x y. x \ counit2 --> y \ counit2 --> x Int Vset(i) \ 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 \ counit2; y \ 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