author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 10186  499637e8f2c6 
child 11335  c150861633da 
permissions  rwrr 
9422  1 
(* Title: HOL/Gfp.ML 
923  2 
ID: $Id$ 
1465  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
923  4 
Copyright 1993 University of Cambridge 
5 

5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5069
diff
changeset

6 
The KnasterTarski Theorem for greatest fixed points. 
923  7 
*) 
8 

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

10 

11 
(* gfp(f) is the least upper bound of {u. u <= f(u)} *) 

12 

5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5069
diff
changeset

13 
Goalw [gfp_def] "[ X <= f(X) ] ==> X <= gfp(f)"; 
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5069
diff
changeset

14 
by (etac (CollectI RS Union_upper) 1); 
923  15 
qed "gfp_upperbound"; 
16 

10067  17 
val prems = Goalw [gfp_def] 
923  18 
"[ !!u. u <= f(u) ==> u<=X ] ==> gfp(f) <= X"; 
19 
by (REPEAT (ares_tac ([Union_least]@prems) 1)); 

20 
by (etac CollectD 1); 

21 
qed "gfp_least"; 

22 

5316  23 
Goal "mono(f) ==> gfp(f) <= f(gfp(f))"; 
923  24 
by (EVERY1 [rtac gfp_least, rtac subset_trans, atac, 
5316  25 
etac monoD, rtac gfp_upperbound, atac]); 
923  26 
qed "gfp_lemma2"; 
27 

5316  28 
Goal "mono(f) ==> f(gfp(f)) <= gfp(f)"; 
29 
by (EVERY1 [rtac gfp_upperbound, rtac monoD, assume_tac, 

30 
etac gfp_lemma2]); 

923  31 
qed "gfp_lemma3"; 
32 

5316  33 
Goal "mono(f) ==> gfp(f) = f(gfp(f))"; 
34 
by (REPEAT (ares_tac [equalityI,gfp_lemma2,gfp_lemma3] 1)); 

10186  35 
qed "gfp_unfold"; 
923  36 

37 
(*** Coinduction rules for greatest fixed points ***) 

38 

39 
(*weak version*) 

5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5069
diff
changeset

40 
Goal "[ a: X; X <= f(X) ] ==> a : gfp(f)"; 
923  41 
by (rtac (gfp_upperbound RS subsetD) 1); 
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5069
diff
changeset

42 
by Auto_tac; 
923  43 
qed "weak_coinduct"; 
44 

10067  45 
Goal "[ X <= f(X Un gfp(f)); mono(f) ] ==> \ 
923  46 
\ X Un gfp(f) <= f(X Un gfp(f))"; 
10067  47 
by (blast_tac (claset() addDs [gfp_lemma2, mono_Un]) 1); 
923  48 
qed "coinduct_lemma"; 
49 

50 
(*strong version, thanks to Coen & Frost*) 

5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5069
diff
changeset

51 
Goal "[ mono(f); a: X; X <= f(X Un gfp(f)) ] ==> a : gfp(f)"; 
923  52 
by (rtac (coinduct_lemma RSN (2, weak_coinduct)) 1); 
53 
by (REPEAT (ares_tac [UnI1, Un_least] 1)); 

54 
qed "coinduct"; 

55 

10067  56 
Goal "[ mono(f); a: gfp(f) ] ==> a: f(X Un gfp(f))"; 
57 
by (blast_tac (claset() addDs [gfp_lemma2, mono_Un]) 1); 

923  58 
qed "gfp_fun_UnI2"; 
59 

60 
(*** Even Stronger version of coinduct [by Martin Coen] 

61 
 instead of the condition X <= f(X) 

62 
consider X <= (f(X) Un f(f(X)) ...) Un gfp(X) ***) 

63 

5316  64 
Goal "mono(f) ==> mono(%x. f(x) Un X Un B)"; 
65 
by (REPEAT (ares_tac [subset_refl, monoI, Un_mono] 1 ORELSE etac monoD 1)); 

923  66 
qed "coinduct3_mono_lemma"; 
67 

10067  68 
Goal "[ X <= f(lfp(%x. f(x) Un X Un gfp(f))); mono(f) ] ==> \ 
3842  69 
\ lfp(%x. f(x) Un X Un gfp(f)) <= f(lfp(%x. f(x) Un X Un gfp(f)))"; 
923  70 
by (rtac subset_trans 1); 
10067  71 
by (etac (coinduct3_mono_lemma RS lfp_lemma3) 1); 
923  72 
by (rtac (Un_least RS Un_least) 1); 
73 
by (rtac subset_refl 1); 

10067  74 
by (assume_tac 1); 
10186  75 
by (rtac (gfp_unfold RS equalityD1 RS subset_trans) 1); 
10067  76 
by (assume_tac 1); 
77 
by (rtac monoD 1 THEN assume_tac 1); 

10186  78 
by (stac (coinduct3_mono_lemma RS lfp_unfold) 1); 
10067  79 
by Auto_tac; 
923  80 
qed "coinduct3_lemma"; 
81 

5316  82 
Goal 
83 
"[ mono(f); a:X; X <= f(lfp(%x. f(x) Un X Un gfp(f))) ] ==> a : gfp(f)"; 

923  84 
by (rtac (coinduct3_lemma RSN (2,weak_coinduct)) 1); 
10186  85 
by (resolve_tac [coinduct3_mono_lemma RS lfp_unfold RS ssubst] 1); 
5316  86 
by Auto_tac; 
923  87 
qed "coinduct3"; 
88 

89 

10186  90 
(** Definition forms of gfp_unfold and coinduct, to control unfolding **) 
923  91 

10067  92 
Goal "[ A==gfp(f); mono(f) ] ==> A = f(A)"; 
10186  93 
by (auto_tac (claset() addSIs [gfp_unfold], simpset())); 
94 
qed "def_gfp_unfold"; 

923  95 

10067  96 
Goal "[ A==gfp(f); mono(f); a:X; X <= f(X Un A) ] ==> a: A"; 
97 
by (auto_tac (claset() addSIs [coinduct], simpset())); 

923  98 
qed "def_coinduct"; 
99 

100 
(*The version used in the induction/coinduction package*) 

5316  101 
val prems = Goal 
923  102 
"[ A == gfp(%w. Collect(P(w))); mono(%w. Collect(P(w))); \ 
103 
\ a: X; !!z. z: X ==> P (X Un A) z ] ==> \ 

104 
\ a : A"; 

105 
by (rtac def_coinduct 1); 

106 
by (REPEAT (ares_tac (prems @ [subsetI,CollectI]) 1)); 

107 
qed "def_Collect_coinduct"; 

108 

10067  109 
Goal "[ A==gfp(f); mono(f); a:X; X <= f(lfp(%x. f(x) Un X Un A)) ] \ 
110 
\ ==> a: A"; 

111 
by (auto_tac (claset() addSIs [coinduct3], simpset())); 

923  112 
qed "def_coinduct3"; 
113 

114 
(*Monotonicity of gfp!*) 

5316  115 
val [prem] = Goal "[ !!Z. f(Z)<=g(Z) ] ==> gfp(f) <= gfp(g)"; 
1465  116 
by (rtac (gfp_upperbound RS gfp_least) 1); 
117 
by (etac (prem RSN (2,subset_trans)) 1); 

923  118 
qed "gfp_mono"; 