author  haftmann 
Tue, 10 Jul 2007 17:30:50 +0200  
changeset 23709  fd31da8f752a 
parent 21404  eb85850d3eb7 
child 32153  a0e57fb1b930 
permissions  rwrr 
17456  1 
(* Title: CCL/Lfp.thy 
0  2 
ID: $Id$ 
1474  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1992 University of Cambridge 
5 
*) 

6 

17456  7 
header {* The KnasterTarski Theorem *} 
8 

9 
theory Lfp 

10 
imports Set 

11 
begin 

12 

20140  13 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20140
diff
changeset

14 
lfp :: "['a set=>'a set] => 'a set" where  "least fixed point" 
17456  15 
"lfp(f) == Inter({u. f(u) <= u})" 
16 

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

19 
lemma lfp_lowerbound: "[ f(A) <= A ] ==> lfp(f) <= A" 

20 
unfolding lfp_def by blast 

21 

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

23 
unfolding lfp_def by blast 

24 

25 
lemma lfp_lemma2: "mono(f) ==> f(lfp(f)) <= lfp(f)" 

26 
by (rule lfp_greatest, rule subset_trans, drule monoD, rule lfp_lowerbound, assumption+) 

27 

28 
lemma lfp_lemma3: "mono(f) ==> lfp(f) <= f(lfp(f))" 

29 
by (rule lfp_lowerbound, frule monoD, drule lfp_lemma2, assumption+) 

30 

31 
lemma lfp_Tarski: "mono(f) ==> lfp(f) = f(lfp(f))" 

32 
by (rule equalityI lfp_lemma2 lfp_lemma3  assumption)+ 

33 

34 

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

36 

37 
lemma induct: 

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

39 
and mono: "mono(f)" 

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

41 
shows "P(a)" 

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

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

44 
apply (rule Int_greatest, rule subset_trans, rule Int_lower1 [THEN mono [THEN monoD]], 

45 
rule mono [THEN lfp_lemma2], rule CollectI [THEN subsetI], rule indhyp, assumption) 

46 
done 

47 

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

49 

50 
lemma def_lfp_Tarski: "[ h==lfp(f); mono(f) ] ==> h = f(h)" 

51 
apply unfold 

52 
apply (drule lfp_Tarski) 

53 
apply assumption 

54 
done 

55 

56 
lemma def_induct: 

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

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

59 
] ==> P(a)" 

60 
apply (rule induct [of concl: P a]) 

61 
apply simp 

62 
apply assumption 

63 
apply blast 

64 
done 

65 

66 
(*Monotonicity of lfp!*) 

67 
lemma lfp_mono: "[ mono(g); !!Z. f(Z)<=g(Z) ] ==> lfp(f) <= lfp(g)" 

68 
apply (rule lfp_lowerbound) 

69 
apply (rule subset_trans) 

70 
apply (erule meta_spec) 

71 
apply (erule lfp_lemma2) 

72 
done 

17456  73 

0  74 
end 