author  wenzelm 
Sat, 25 May 2013 17:40:44 +0200  
changeset 52147  9943f8067f11 
parent 32153  a0e57fb1b930 
child 58889  5b7a9633cfa8 
permissions  rwrr 
17456  1 
(* Title: CCL/Lfp.thy 
1474  2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  3 
Copyright 1992 University of Cambridge 
4 
*) 

5 

17456  6 
header {* The KnasterTarski Theorem *} 
7 

8 
theory Lfp 

9 
imports Set 

10 
begin 

11 

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

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

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

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

19 
unfolding lfp_def by blast 

20 

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

22 
unfolding lfp_def by blast 

23 

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

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

26 

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

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

29 

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

31 
by (rule equalityI lfp_lemma2 lfp_lemma3  assumption)+ 

32 

33 

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

35 

36 
lemma induct: 

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

38 
and mono: "mono(f)" 

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

40 
shows "P(a)" 

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

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

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

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

45 
done 

46 

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

48 

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

50 
apply unfold 

51 
apply (drule lfp_Tarski) 

52 
apply assumption 

53 
done 

54 

55 
lemma def_induct: 

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

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

58 
] ==> P(a)" 

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

60 
apply simp 

61 
apply assumption 

62 
apply blast 

63 
done 

64 

65 
(*Monotonicity of lfp!*) 

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

67 
apply (rule lfp_lowerbound) 

68 
apply (rule subset_trans) 

69 
apply (erule meta_spec) 

70 
apply (erule lfp_lemma2) 

71 
done 

17456  72 

0  73 
end 