1465

1 
(* Title: HOL/lfp.ML

923

2 
ID: $Id$

1465

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory

923

4 
Copyright 1992 University of Cambridge


5 

5316

6 
The KnasterTarski Theorem

923

7 
*)


8 


9 
open Lfp;


10 


11 
(*** Proof of KnasterTarski Theorem ***)


12 


13 
(* lfp(f) is the greatest lower bound of {u. f(u) <= u} *)


14 

5316

15 
Goalw [lfp_def] "f(A) <= A ==> lfp(f) <= A";

923

16 
by (rtac (CollectI RS Inter_lower) 1);

5316

17 
by (assume_tac 1);

923

18 
qed "lfp_lowerbound";


19 

5316

20 
val prems = Goalw [lfp_def]

923

21 
"[ !!u. f(u) <= u ==> A<=u ] ==> A <= lfp(f)";


22 
by (REPEAT (ares_tac ([Inter_greatest]@prems) 1));


23 
by (etac CollectD 1);


24 
qed "lfp_greatest";


25 

5316

26 
Goal "mono(f) ==> f(lfp(f)) <= lfp(f)";

923

27 
by (EVERY1 [rtac lfp_greatest, rtac subset_trans,

5316

28 
etac monoD, rtac lfp_lowerbound, atac, atac]);

923

29 
qed "lfp_lemma2";


30 

5316

31 
Goal "mono(f) ==> lfp(f) <= f(lfp(f))";


32 
by (EVERY1 [rtac lfp_lowerbound, rtac monoD, assume_tac,


33 
etac lfp_lemma2]);

923

34 
qed "lfp_lemma3";


35 

5316

36 
Goal "mono(f) ==> lfp(f) = f(lfp(f))";


37 
by (REPEAT (ares_tac [equalityI,lfp_lemma2,lfp_lemma3] 1));

923

38 
qed "lfp_Tarski";


39 


40 
(*** General induction rule for least fixed points ***)


41 

5316

42 
val [lfp,mono,indhyp] = Goal

1465

43 
"[ a: lfp(f); mono(f); \

3842

44 
\ !!x. [ x: f(lfp(f) Int {x. P(x)}) ] ==> P(x) \

923

45 
\ ] ==> P(a)";


46 
by (res_inst_tac [("a","a")] (Int_lower2 RS subsetD RS CollectD) 1);


47 
by (rtac (lfp RSN (2, lfp_lowerbound RS subsetD)) 1);


48 
by (EVERY1 [rtac Int_greatest, rtac subset_trans,

1465

49 
rtac (Int_lower1 RS (mono RS monoD)),


50 
rtac (mono RS lfp_lemma2),


51 
rtac (CollectI RS subsetI), rtac indhyp, atac]);

923

52 
qed "induct";


53 

5098

54 
bind_thm ("induct2",


55 
split_rule (read_instantiate [("a","(a,b)")] induct));

1114

56 

1125

57 

923

58 
(** Definition forms of lfp_Tarski and induct, to control unfolding **)


59 


60 
val [rew,mono] = goal Lfp.thy "[ h==lfp(f); mono(f) ] ==> h = f(h)";


61 
by (rewtac rew);


62 
by (rtac (mono RS lfp_Tarski) 1);


63 
qed "def_lfp_Tarski";


64 

5316

65 
val rew::prems = Goal

1465

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

3842

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

923

68 
\ ] ==> P(a)";

1465

69 
by (EVERY1 [rtac induct, (*backtracking to force correct induction*)


70 
REPEAT1 o (ares_tac (map (rewrite_rule [rew]) prems))]);

923

71 
qed "def_induct";


72 


73 
(*Monotonicity of lfp!*)

5316

74 
val [prem] = Goal "[ !!Z. f(Z)<=g(Z) ] ==> lfp(f) <= lfp(g)";

1465

75 
by (rtac (lfp_lowerbound RS lfp_greatest) 1);


76 
by (etac (prem RS subset_trans) 1);

923

77 
qed "lfp_mono";
