# Theory Gfp

Up to index of Isabelle/CCL

theory Gfp
imports Lfp
uses [Gfp.ML]
begin

    (*  Title:      CCL/Gfp.thy
        ID:         $Id: Gfp.thy,v 1.3 2005/09/17 15:35:27 wenzelm Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   1992  University of Cambridge
    *)

    header {* Greatest fixed points *}

    theory Gfp
    imports Lfp
    begin

    constdefs
      gfp :: "['a set=>'a set] => 'a set"    (*greatest fixed point*)
      "gfp(f) == Union({u. u <= f(u)})"

    ML {* use_legacy_bindings (the_context ()) *}

    end

theorem gfp_upperbound:

      A <= f(A) ==> A <= gfp(f)

theorem gfp_least:

      (!!u. u <= f(u) ==> u <= A) ==> gfp(f) <= A

theorem gfp_lemma2:

      mono(f) ==> gfp(f) <= f(gfp(f))

theorem gfp_lemma3:

      mono(f) ==> f(gfp(f)) <= gfp(f)

theorem gfp_Tarski:

      mono(f) ==> gfp(f) = f(gfp(f))

theorem coinduct:

      [| a : A; A <= f(A) |] ==> a : gfp(f)

theorem coinduct2_lemma:

      [| A <= f(A) Un gfp(f); mono(f) |] ==> A Un gfp(f) <= f(A Un gfp(f))

theorem coinduct2:

      [| a : A; A <= f(A) Un gfp(f); mono(f) |] ==> a : gfp(f)

theorem coinduct3_mono_lemma:

      mono(f) ==> mono(%x. f(x) Un A Un B)

theorem coinduct3_lemma:

      [| A <= f(lfp(%x. f(x) Un A Un gfp(f))); mono(f) |]
      ==> lfp(%x. f(x) Un A Un gfp(f)) <= f(lfp(%x. f(x) Un A Un gfp(f)))

theorem coinduct3:

      [| a : A; A <= f(lfp(%x. f(x) Un A Un gfp(f))); mono(f) |] ==> a : gfp(f)

theorem def_gfp_Tarski:

      [| h == gfp(f); mono(f) |] ==> h = f(h)

theorem def_coinduct:

      [| h == gfp(f); a : A; A <= f(A) |] ==> a : h

theorem def_coinduct2:

      [| h == gfp(f); a : A; A <= f(A) Un h; mono(f) |] ==> a : h

theorem def_coinduct3:

      [| h == gfp(f); a : A; A <= f(lfp(%x. f(x) Un A Un h)); mono(f) |] ==> a : h

theorem gfp_mono:

      [| mono(f); !!Z. f(Z) <= g(Z) |] ==> gfp(f) <= gfp(g)