9422

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 

9422

6 
The KnasterTarski Theorem.

923

7 
*)


8 


9 
(*** Proof of KnasterTarski Theorem ***)


10 


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


12 

5316

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

923

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

5316

15 
by (assume_tac 1);

923

16 
qed "lfp_lowerbound";


17 

5316

18 
val prems = Goalw [lfp_def]

923

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


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


21 
by (etac CollectD 1);


22 
qed "lfp_greatest";


23 

5316

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

923

25 
by (EVERY1 [rtac lfp_greatest, rtac subset_trans,

5316

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

923

27 
qed "lfp_lemma2";


28 

5316

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


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


31 
etac lfp_lemma2]);

923

32 
qed "lfp_lemma3";


33 

5316

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


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

10186

36 
qed "lfp_unfold";

923

37 


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


39 

5316

40 
val [lfp,mono,indhyp] = Goal

1465

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

3842

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

923

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


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


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


46 
by (EVERY1 [rtac Int_greatest, rtac subset_trans,

1465

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


48 
rtac (mono RS lfp_lemma2),


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

10202

50 
qed "lfp_induct";

923

51 

10202

52 
bind_thm ("lfp_induct2",


53 
split_rule (read_instantiate [("a","(a,b)")] lfp_induct));

1114

54 

1125

55 

10202

56 
(** Definition forms of lfp_unfold and lfp_induct, to control unfolding **)

923

57 

10067

58 
Goal "[ h==lfp(f); mono(f) ] ==> h = f(h)";

10186

59 
by (auto_tac (claset() addSIs [lfp_unfold], simpset()));


60 
qed "def_lfp_unfold";

923

61 

5316

62 
val rew::prems = Goal

1465

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

3842

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

923

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

10202

66 
by (EVERY1 [rtac lfp_induct, (*backtracking to force correct induction*)

1465

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

10202

68 
qed "def_lfp_induct";

923

69 


70 
(*Monotonicity of lfp!*)

5316

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

1465

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


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

923

74 
qed "lfp_mono";
