1475

1 
(* Title: HOL/Lfp.thy

923

2 
ID: $Id$

1475

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory

923

4 
Copyright 1992 University of Cambridge

15386

5 
*)

923

6 

15386

7 
header{*Least Fixed Points and the KnasterTarski Theorem*}

923

8 

15131

9 
theory Lfp

15140

10 
imports Product_Type

15131

11 
begin

1558

12 


13 
constdefs

14169

14 
lfp :: "['a set \<Rightarrow> 'a set] \<Rightarrow> 'a set"

15386

15 
"lfp(f) == Inter({u. f(u) \<subseteq> u})" {*least fixed point*}


16 


17 


18 


19 
subsection{*Proof of KnasterTarski Theorem using @{term lfp}*}


20 


21 


22 
text{*@{term "lfp f"} is the least upper bound of


23 
the set @{term "{u. f(u) \<subseteq> u}"} *}


24 


25 
lemma lfp_lowerbound: "f(A) \<subseteq> A ==> lfp(f) \<subseteq> A"


26 
by (auto simp add: lfp_def)


27 


28 
lemma lfp_greatest: "[ !!u. f(u) \<subseteq> u ==> A\<subseteq>u ] ==> A \<subseteq> lfp(f)"


29 
by (auto simp add: lfp_def)


30 


31 
lemma lfp_lemma2: "mono(f) ==> f(lfp(f)) \<subseteq> lfp(f)"


32 
by (rules intro: lfp_greatest subset_trans monoD lfp_lowerbound)


33 


34 
lemma lfp_lemma3: "mono(f) ==> lfp(f) \<subseteq> f(lfp(f))"


35 
by (rules intro: lfp_lemma2 monoD lfp_lowerbound)


36 


37 
lemma lfp_unfold: "mono(f) ==> lfp(f) = f(lfp(f))"


38 
by (rules intro: equalityI lfp_lemma2 lfp_lemma3)


39 


40 
subsection{*General induction rules for greatest fixed points*}


41 


42 
lemma lfp_induct:


43 
assumes lfp: "a: lfp(f)"


44 
and mono: "mono(f)"


45 
and indhyp: "!!x. [ x: f(lfp(f) Int {x. P(x)}) ] ==> P(x)"


46 
shows "P(a)"


47 
apply (rule_tac a=a in Int_lower2 [THEN subsetD, THEN CollectD])


48 
apply (rule lfp [THEN [2] lfp_lowerbound [THEN subsetD]])


49 
apply (rule Int_greatest)


50 
apply (rule subset_trans [OF Int_lower1 [THEN mono [THEN monoD]]


51 
mono [THEN lfp_lemma2]])


52 
apply (blast intro: indhyp)


53 
done


54 


55 


56 
text{*Version of induction for binary relations*}


57 
lemmas lfp_induct2 = lfp_induct [of "(a,b)", split_format (complete)]


58 


59 


60 
lemma lfp_ordinal_induct:


61 
assumes mono: "mono f"


62 
shows "[ !!S. P S ==> P(f S); !!M. !S:M. P S ==> P(Union M) ]


63 
==> P(lfp f)"


64 
apply(subgoal_tac "lfp f = Union{S. S \<subseteq> lfp f & P S}")


65 
apply (erule ssubst, simp)


66 
apply(subgoal_tac "Union{S. S \<subseteq> lfp f & P S} \<subseteq> lfp f")


67 
prefer 2 apply blast


68 
apply(rule equalityI)


69 
prefer 2 apply assumption


70 
apply(drule mono [THEN monoD])


71 
apply (cut_tac mono [THEN lfp_unfold], simp)


72 
apply (rule lfp_lowerbound, auto)


73 
done


74 


75 


76 
text{*Definition forms of @{text lfp_unfold} and @{text lfp_induct},


77 
to control unfolding*}


78 


79 
lemma def_lfp_unfold: "[ h==lfp(f); mono(f) ] ==> h = f(h)"


80 
by (auto intro!: lfp_unfold)


81 


82 
lemma def_lfp_induct:


83 
"[ A == lfp(f); mono(f); a:A;


84 
!!x. [ x: f(A Int {x. P(x)}) ] ==> P(x)


85 
] ==> P(a)"


86 
by (blast intro: lfp_induct)


87 


88 
(*Monotonicity of lfp!*)


89 
lemma lfp_mono: "[ !!Z. f(Z)\<subseteq>g(Z) ] ==> lfp(f) \<subseteq> lfp(g)"


90 
by (rule lfp_lowerbound [THEN lfp_greatest], blast)


91 


92 


93 
ML


94 
{*


95 
val lfp_def = thm "lfp_def";


96 
val lfp_lowerbound = thm "lfp_lowerbound";


97 
val lfp_greatest = thm "lfp_greatest";


98 
val lfp_unfold = thm "lfp_unfold";


99 
val lfp_induct = thm "lfp_induct";


100 
val lfp_induct2 = thm "lfp_induct2";


101 
val lfp_ordinal_induct = thm "lfp_ordinal_induct";


102 
val def_lfp_unfold = thm "def_lfp_unfold";


103 
val def_lfp_induct = thm "def_lfp_induct";


104 
val lfp_mono = thm "lfp_mono";


105 
*}

1558

106 

923

107 
end
