Theory Fixedpt

(*  Title:      ZF/Fixedpt.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1992  University of Cambridge

section‹Least and Greatest Fixed Points; the Knaster-Tarski Theorem›

theory Fixedpt imports equalities begin

  (*monotone operator from Pow(D) to itself*)
  bnd_mono :: "[i,ii]o"  where
     "bnd_mono(D,h)  h(D)<=D  (W X. W<=X  X<=D  h(W)  h(X))"

  lfp      :: "[i,ii]i"  where
     "lfp(D,h)  ({X: Pow(D). h(X)  X})"

  gfp      :: "[i,ii]i"  where
     "gfp(D,h)  ({X: Pow(D). X  h(X)})"

text‹The theorem is proved in the lattice of subsets of termD, 
      namely termPow(D), with Inter as the greatest lower bound.›

subsection‹Monotone Operators›

lemma bnd_monoI:
        W X. W<=D;  X<=D;  W<=X  h(W)  h(X)   
by (unfold bnd_mono_def, clarify, blast)  

lemma bnd_monoD1: "bnd_mono(D,h)  h(D)  D"
  unfolding bnd_mono_def
apply (erule conjunct1)

lemma bnd_monoD2: "bnd_mono(D,h);  W<=X;  X<=D  h(W)  h(X)"
by (unfold bnd_mono_def, blast)

lemma bnd_mono_subset:
    "bnd_mono(D,h);  X<=D  h(X)  D"
by (unfold bnd_mono_def, clarify, blast) 

lemma bnd_mono_Un:
     "bnd_mono(D,h);  A  D;  B  D  h(A)  h(B)  h(A  B)"
  unfolding bnd_mono_def
apply (rule Un_least, blast+)

lemma bnd_mono_UN:
     "bnd_mono(D,h);  iI. A(i)  D 
       (iI. h(A(i)))  h((iI. A(i)))"
  unfolding bnd_mono_def 
apply (rule UN_least)
apply (elim conjE) 
apply (drule_tac x="A(i)" in spec)
apply (drule_tac x="(iI. A(i))" in spec) 
apply blast 

lemma bnd_mono_Int:
     "bnd_mono(D,h);  A  D;  B  D  h(A  B)  h(A)  h(B)"
apply (rule Int_greatest) 
apply (erule bnd_monoD2, rule Int_lower1, assumption) 
apply (erule bnd_monoD2, rule Int_lower2, assumption) 

subsection‹Proof of Knaster-Tarski Theorem using termlfp

(*lfp is contained in each pre-fixedpoint*)
lemma lfp_lowerbound: 
    "h(A)  A;  A<=D  lfp(D,h)  A"
by (unfold lfp_def, blast)

(*Unfolding the defn of Inter dispenses with the premise bnd_mono(D,h)!*)
lemma lfp_subset: "lfp(D,h)  D"
by (unfold lfp_def Inter_def, blast)

(*Used in datatype package*)
lemma def_lfp_subset:  "A  lfp(D,h)  A  D"
apply simp
apply (rule lfp_subset)

lemma lfp_greatest:  
    "h(D)  D;  X. h(X)  X;  X<=D  A<=X  A  lfp(D,h)"
by (unfold lfp_def, blast) 

lemma lfp_lemma1:  
    "bnd_mono(D,h);  h(A)<=A;  A<=D  h(lfp(D,h))  A"
apply (erule bnd_monoD2 [THEN subset_trans])
apply (rule lfp_lowerbound, assumption+)

lemma lfp_lemma2: "bnd_mono(D,h)  h(lfp(D,h))  lfp(D,h)"
apply (rule bnd_monoD1 [THEN lfp_greatest])
apply (rule_tac [2] lfp_lemma1)
apply (assumption+)

lemma lfp_lemma3: 
    "bnd_mono(D,h)  lfp(D,h)  h(lfp(D,h))"
apply (rule lfp_lowerbound)
apply (rule bnd_monoD2, assumption)
apply (rule lfp_lemma2, assumption)
apply (erule_tac [2] bnd_mono_subset)
apply (rule lfp_subset)+

lemma lfp_unfold: "bnd_mono(D,h)  lfp(D,h) = h(lfp(D,h))"
apply (rule equalityI) 
apply (erule lfp_lemma3) 
apply (erule lfp_lemma2) 

(*Definition form, to control unfolding*)
lemma def_lfp_unfold:
    "Alfp(D,h);  bnd_mono(D,h)  A = h(A)"
apply simp
apply (erule lfp_unfold)

subsection‹General Induction Rule for Least Fixedpoints›

lemma Collect_is_pre_fixedpt:
    "bnd_mono(D,h);  x. x  h(Collect(lfp(D,h),P))  P(x)
      h(Collect(lfp(D,h),P))  Collect(lfp(D,h),P)"
by (blast intro: lfp_lemma2 [THEN subsetD] bnd_monoD2 [THEN subsetD] 
                 lfp_subset [THEN subsetD]) 

(*This rule yields an induction hypothesis in which the components of a
  data structure may be assumed to be elements of lfp(D,h)*)
lemma induct:
    "bnd_mono(D,h);  a  lfp(D,h);                    
        x. x  h(Collect(lfp(D,h),P))  P(x)         
apply (rule Collect_is_pre_fixedpt
              [THEN lfp_lowerbound, THEN subsetD, THEN CollectD2])
apply (rule_tac [3] lfp_subset [THEN Collect_subset [THEN subset_trans]], 

(*Definition form, to control unfolding*)
lemma def_induct:
    "A  lfp(D,h);  bnd_mono(D,h);  a:A;    
        x. x  h(Collect(A,P))  P(x)  
by (rule induct, blast+)

(*This version is useful when "A" is not a subset of D
  second premise could simply be h(D ∩ A) ⊆ D or ⋀X. X<=D ⟹ h(X)<=D *)
lemma lfp_Int_lowerbound:
    "h(D  A)  A;  bnd_mono(D,h)  lfp(D,h)  A" 
apply (rule lfp_lowerbound [THEN subset_trans])
apply (erule bnd_mono_subset [THEN Int_greatest], blast+)

(*Monotonicity of lfp, where h precedes i under a domain-like partial order
  monotonicity of h is not strictly necessary; h must be bounded by D*)
lemma lfp_mono:
  assumes hmono: "bnd_mono(D,h)"
      and imono: "bnd_mono(E,i)"
      and subhi: "X. X<=D  h(X)  i(X)"
    shows "lfp(D,h)  lfp(E,i)"
apply (rule bnd_monoD1 [THEN lfp_greatest])
apply (rule imono)
apply (rule hmono [THEN [2] lfp_Int_lowerbound])
apply (rule Int_lower1 [THEN subhi, THEN subset_trans])
apply (rule imono [THEN bnd_monoD2, THEN subset_trans], auto) 

(*This (unused) version illustrates that monotonicity is not really needed,
  but both lfp's must be over the SAME set D;  Inter is anti-monotonic!*)
lemma lfp_mono2:
    "i(D)  D;  X. X<=D  h(X)  i(X)  lfp(D,h)  lfp(D,i)"
apply (rule lfp_greatest, assumption)
apply (rule lfp_lowerbound, blast, assumption)

lemma lfp_cong:
     "D=D'; X. X  D'  h(X) = h'(X)  lfp(D,h) = lfp(D',h')"
apply (simp add: lfp_def)
apply (rule_tac t=Inter in subst_context)
apply (rule Collect_cong, simp_all) 

subsection‹Proof of Knaster-Tarski Theorem using termgfp

(*gfp contains each post-fixedpoint that is contained in D*)
lemma gfp_upperbound: "A  h(A);  A<=D  A  gfp(D,h)"
  unfolding gfp_def
apply (rule PowI [THEN CollectI, THEN Union_upper])
apply (assumption+)

lemma gfp_subset: "gfp(D,h)  D"
by (unfold gfp_def, blast)

(*Used in datatype package*)
lemma def_gfp_subset: "Agfp(D,h)  A  D"
apply simp
apply (rule gfp_subset)

lemma gfp_least: 
    "bnd_mono(D,h);  X. X  h(X);  X<=D  X<=A   
     gfp(D,h)  A"
  unfolding gfp_def
apply (blast dest: bnd_monoD1) 

lemma gfp_lemma1: 
    "bnd_mono(D,h);  A<=h(A);  A<=D  A  h(gfp(D,h))"
apply (rule subset_trans, assumption)
apply (erule bnd_monoD2)
apply (rule_tac [2] gfp_subset)
apply (simp add: gfp_upperbound)

lemma gfp_lemma2: "bnd_mono(D,h)  gfp(D,h)  h(gfp(D,h))"
apply (rule gfp_least)
apply (rule_tac [2] gfp_lemma1)
apply (assumption+)

lemma gfp_lemma3: 
    "bnd_mono(D,h)  h(gfp(D,h))  gfp(D,h)"
apply (rule gfp_upperbound)
apply (rule bnd_monoD2, assumption)
apply (rule gfp_lemma2, assumption)
apply (erule bnd_mono_subset, rule gfp_subset)+

lemma gfp_unfold: "bnd_mono(D,h)  gfp(D,h) = h(gfp(D,h))"
apply (rule equalityI) 
apply (erule gfp_lemma2) 
apply (erule gfp_lemma3) 

(*Definition form, to control unfolding*)
lemma def_gfp_unfold:
    "Agfp(D,h);  bnd_mono(D,h)  A = h(A)"
apply simp
apply (erule gfp_unfold)

subsection‹Coinduction Rules for Greatest Fixed Points›

(*weak version*)
lemma weak_coinduct: "a: X;  X  h(X);  X  D  a  gfp(D,h)"
by (blast intro: gfp_upperbound [THEN subsetD])

lemma coinduct_lemma:
    "X  h(X  gfp(D,h));  X  D;  bnd_mono(D,h)    
     X  gfp(D,h)  h(X  gfp(D,h))"
apply (erule Un_least)
apply (rule gfp_lemma2 [THEN subset_trans], assumption)
apply (rule Un_upper2 [THEN subset_trans])
apply (rule bnd_mono_Un, assumption+) 
apply (rule gfp_subset)

(*strong version*)
lemma coinduct:
     "bnd_mono(D,h);  a: X;  X  h(X  gfp(D,h));  X  D
       a  gfp(D,h)"
apply (rule weak_coinduct)
apply (erule_tac [2] coinduct_lemma)
apply (simp_all add: gfp_subset Un_subset_iff) 

(*Definition form, to control unfolding*)
lemma def_coinduct:
    "A  gfp(D,h);  bnd_mono(D,h);  a: X;  X  h(X  A);  X  D   
     a  A"
apply simp
apply (rule coinduct, assumption+)

(*The version used in the induction/coinduction package*)
lemma def_Collect_coinduct:
    "A  gfp(D, λw. Collect(D,P(w)));  bnd_mono(D, λw. Collect(D,P(w)));   
        a: X;  X  D;  z. z: X  P(X  A, z)   
     a  A"
apply (rule def_coinduct, assumption+, blast+)

(*Monotonicity of gfp!*)
lemma gfp_mono:
    "bnd_mono(D,h);  D  E;                  
        X. X<=D  h(X)  i(X)  gfp(D,h)  gfp(E,i)"
apply (rule gfp_upperbound)
apply (rule gfp_lemma2 [THEN subset_trans], assumption)
apply (blast del: subsetI intro: gfp_subset) 
apply (blast del: subsetI intro: subset_trans gfp_subset)