# Theory CoUnit

Up to index of Isabelle/ZF/ex

theory CoUnit
imports Main
begin

    (*  Title:      ZF/ex/CoUnit.ML
        ID:         $Id: CoUnit.thy,v 1.8 2005/06/17 14:15:11 haftmann Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   1994  University of Cambridge
    *)

    header {* Trivial codatatype definitions, one of which goes wrong! *}

    theory CoUnit imports Main begin

    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")

    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

    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")

    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

lemmas ConE:

      [| Con(x) ∈ counit; x ∈ counit ==> Q |] ==> Q

lemma Con_iff:

      Con(x) = Con(y) <-> x = y

lemma counit_eq_univ:

      counit = quniv(0)

lemmas Con2E:

      [| Con2(x, y) ∈ counit2; [| x ∈ counit2; y ∈ counit2 |] ==> Q |] ==> Q

lemma Con2_iff:

      Con2(x, y) = Con2(x', y') <-> x = x' ∧ y = y'

lemma Con2_bnd_mono:

      bnd_mono(univ(0), %x. Con2(x, x))

lemma lfp_Con2_in_counit2:

      lfp(univ(0), %x. Con2(x, x)) ∈ counit2

lemma counit2_Int_Vset_subset:

      [| Ord(i); x ∈ counit2; y ∈ counit2 |] ==> x ∩ Vset(i) ⊆ y

lemma counit2_implies_equal:

      [| x ∈ counit2; y ∈ counit2 |] ==> x = y

lemma counit2_eq_univ:

      counit2 = {lfp(univ(0), %x. Con2(x, x))}