Up to index of Isabelle/CCL
theory Lfp(* 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)