KnasterTarski[U:Type] : THEORY
BEGIN

Set : TYPE = [U->bool]

A,B : VAR Set

subset (A,B ) : bool = 
        FORALL (x:U) :(A (x) IMPLIES B(x))

equalset(A,B) : bool =
         subset (A,B) AND subset(B,A)

union (A,B) : Set =  {x:U |  A(x) AND B(x)}

intersection (A,B) : Set =  {x:U |  A(x) OR B(x)}

Class : TYPE = [Set -> bool]

K,L : VAR Class

Intersection (K) : Set = {x:U | FORALL (A:Set) : K(A) IMPLIES A(x)}

lemmaIntersection : LEMMA
   K(A) IMPLIES (subset(Intersection(K),A))

f : [Set -> Set]

monotonic : AXIOM subset(A,B) IMPLIES subset(f(A),f(B))

prefixpoints : Class = { A:Set | subset(f(A),A) }

FP : Set = Intersection(prefixpoints)

% The lemma's below lead up to the Knaster-Tarski fixpoint theorem,
% which states that FP is a fixpoint of f, ie
%
%     KnasterTarski: THEOREM equalset(FP,f(FP))
%
% In the lemma's below the main trick is finding out which
% definitions to expanded, and which instantiations to choose.
%
% Instead of expanding the definition of say "FP" everywhere
% using 
%      (expand FP)
% it's better to expand only one occurrence at the time, eg using
%    (expand FP -2)
% to expand "FP" only in line -2, or even
%    (expand FP -2 2)
% to expand only the second occurrence of "FP" in line -2.
%
% Also, before doing this it's good to make a copy of assumption -2 
% with the definition intact, using
%       (copy -2)
%
% When instatiating a formula, say -2 with "A!", do not use
%         (inst -2 "A!!")
% but use
%         (inst-cp -2 "A!!")
% instead. Try them both to see the difference.
%
% A last hint: it is useful to try and do the proof of
% Knaster-Tarski on paper first, before trying it in PVS. 
% It that case, instead of using lemma1 up to lemma6 below, 
% you may prefer to use some different lemmas to prove Knaster-Tarski.

lemma1: LEMMA 
       prefixpoints(A) IMPLIES subset(FP,A)

lemma2: LEMMA
          (FORALL (B) : prefixpoints(B) IMPLIES subset(A,B))
       IMPLIES
          subset(A,FP)

lemma3: LEMMA prefixpoints(A) IMPLIES subset(f(FP),f(A))

lem_subset : LEMMA
	 FORALL (A,B,C :Set): subset(A,B) AND subset(B,C) IMPLIES subset(A,C) 

lemma4: LEMMA prefixpoints(A) IMPLIES subset(f(FP),A)

lemma5: THEOREM subset(f(FP),FP)

lemma6: THEOREM subset(FP,f(FP))

KnasterTarski: THEOREM equalset(FP,f(FP))



END KnasterTarski