# Theory Lfp

Up to index of Isabelle/CCL

theory Lfp
imports Set
uses subset.ML equalities.ML mono.ML [Lfp.ML]
begin

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

    header {* The Knaster-Tarski Theorem *}

    theory Lfp
    imports Set
    uses "subset.ML" "equalities.ML" "mono.ML"
    begin

    constdefs
      lfp :: "['a set=>'a set] => 'a set"     (*least fixed point*)
      "lfp(f) == Inter({u. f(u) <= u})"

    ML {* use_legacy_bindings (the_context ()) *}

    end

theorem Union_upper:

      B : A ==> B <= Union(A)

theorem Union_least:

      (!!X. X : A ==> X <= C) ==> Union(A) <= C

theorem Inter_lower:

      B : A ==> Inter(A) <= B

theorem Inter_greatest:

      (!!X. X : A ==> C <= X) ==> C <= Inter(A)

theorem Un_upper1:

      A <= A Un B

theorem Un_upper2:

      B <= A Un B

theorem Un_least:

      [| A <= C; B <= C |] ==> A Un B <= C

theorem Int_lower1:

      A Int B <= A

theorem Int_lower2:

      A Int B <= B

theorem Int_greatest:

      [| C <= A; C <= B |] ==> C <= A Int B

theorem monoI:

      (!!A B. A <= B ==> f(A) <= f(B)) ==> mono(f)

theorem monoD:

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

theorem mono_Un:

      mono(f) ==> f(A) Un f(B) <= f(A Un B)

theorem mono_Int:

      mono(f) ==> f(A Int B) <= f(A) Int f(B)

theorem Int_absorb:

      A Int A = A

theorem Int_commute:

      A Int B = B Int A

theorem Int_assoc:

      A Int B Int C = A Int (B Int C)

theorem Int_Un_distrib:

      (A Un B) Int C = A Int C Un B Int C

theorem subset_Int_eq:

      A <= B <-> A Int B = A

theorem Un_absorb:

      A Un A = A

theorem Un_commute:

      A Un B = B Un A

theorem Un_assoc:

      A Un B Un C = A Un (B Un C)

theorem Un_Int_distrib:

      A Int B Un C = (A Un C) Int (B Un C)

theorem Un_Int_crazy:

      A Int B Un B Int C Un C Int A = (A Un B) Int (B Un C) Int (C Un A)

theorem subset_Un_eq:

      A <= B <-> A Un B = B

theorem Compl_disjoint:

      A Int Compl(A) = {x. False}

theorem Compl_partition:

      A Un Compl(A) = {x. True}

theorem double_complement:

      Compl(Compl(A)) = A

theorem Compl_Un:

      Compl(A Un B) = Compl(A) Int Compl(B)

theorem Compl_Int:

      Compl(A Int B) = Compl(A) Un Compl(B)

theorem Compl_UN:

      Compl(UNION(A, B)) = (INT x:A. Compl(B(x)))

theorem Compl_INT:

      Compl(INTER(A, B)) = (UN x:A. Compl(B(x)))

theorem Un_Int_assoc_eq:

      A Int B Un C = A Int (B Un C) <-> C <= A

theorem Union_Un_distrib:

      Union(A Un B) = Union(A) Un Union(B)

theorem Union_disjoint:

      Union(C) Int A = {x. False} <-> (ALL B:C. B Int A = {x. False})

theorem Inter_Un_distrib:

      Inter(A Un B) = Inter(A) Int Inter(B)

theorem UN_eq:

      UNION(A, B) = Union({Y. EX x:A. Y = B(x)})

theorem INT_eq:

      INTER(A, B) = Inter({Y. EX x:A. Y = B(x)})

theorem Int_Union_image:

      A Int Union(B) = UNION(B, op Int(A))

theorem Un_Inter_image:

      A Un Inter(B) = INTER(B, op Un(A))

theorem Union_mono:

      A <= B ==> Union(A) <= Union(B)

theorem Inter_anti_mono:

      B <= A ==> Inter(A) <= Inter(B)

theorem UN_mono:

      [| A <= B; !!x. x : A ==> f(x) <= g(x) |] ==> UNION(A, f) <= UNION(B, g)

theorem INT_anti_mono:

      [| B <= A; !!x. x : A ==> f(x) <= g(x) |] ==> INTER(A, f) <= INTER(A, g)

theorem Un_mono:

      [| A <= C; B <= D |] ==> A Un B <= C Un D

theorem Int_mono:

      [| A <= C; B <= D |] ==> A Int B <= C Int D

theorem Compl_anti_mono:

      A <= B ==> Compl(B) <= Compl(A)

theorem lfp_lowerbound:

      f(A) <= A ==> lfp(f) <= A

theorem lfp_greatest:

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

theorem lfp_lemma2:

      mono(f) ==> f(lfp(f)) <= lfp(f)

theorem lfp_lemma3:

      mono(f) ==> lfp(f) <= f(lfp(f))

theorem lfp_Tarski:

      mono(f) ==> lfp(f) = f(lfp(f))

theorem induct:

      [| a : lfp(f); mono(f); !!x. x : f(lfp(f) Int Collect(P)) ==> P(x) |] ==> P(a)

theorem def_lfp_Tarski:

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

theorem def_induct:

      [| A == lfp(f); a : A; mono(f); !!x. x : f(A Int Collect(P)) ==> P(x) |]
      ==> P(a)

theorem lfp_mono:

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