(* Title: ZF/ex/CoUnit.thy Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge
*)
section \<open>Trivial codatatype definitions, one of which goes wrong!\<close>
theory CoUnit imports ZF begin
text\<open>
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. \<close>
consts
counit :: i
codatatype "counit" = Con ("x \ counit")
inductive_cases ConE: "Con(x) \ counit" \<comment> \<open>USELESS because folding on \<^term>\<open>Con(xa) \<equiv> xa\<close> fails.\<close>
lemma Con_iff: "Con(x) = Con(y) \ x = y" \<comment> \<open>Proving freeness results.\<close> by (auto elim!: counit.free_elims)
lemma counit_eq_univ: "counit = quniv(0)" \<comment> \<open>Should be a singleton, not everything!\<close> apply (rule counit.dom_subset [THEN equalityI]) apply (rule subsetI) apply (erule counit.coinduct) apply (rule subset_refl) unfolding counit.con_defs apply fast done
text\<open> \medskip A similar example, but the constructor is non-degenerate and it works! The resulting set is a singleton. \<close>
consts
counit2 :: i
codatatype "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'" \<comment> \<open>Proving freeness results.\<close> by (fast elim!: counit2.free_elims)
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
