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)