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)