author | clasohm |
Tue, 24 Oct 1995 14:45:35 +0100 | |
changeset 1294 | 1358dc040edb |
parent 1264 | 3eb91524b938 |
child 1465 | 5d7a7e439cec |
permissions | -rw-r--r-- |
923 | 1 |
(* Title: HOL/lfp.ML |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1992 University of Cambridge |
|
5 |
||
6 |
For lfp.thy. The Knaster-Tarski Theorem |
|
7 |
*) |
|
8 |
||
9 |
open Lfp; |
|
10 |
||
11 |
(*** Proof of Knaster-Tarski Theorem ***) |
|
12 |
||
13 |
(* lfp(f) is the greatest lower bound of {u. f(u) <= u} *) |
|
14 |
||
15 |
val prems = goalw Lfp.thy [lfp_def] "[| f(A) <= A |] ==> lfp(f) <= A"; |
|
16 |
by (rtac (CollectI RS Inter_lower) 1); |
|
17 |
by (resolve_tac prems 1); |
|
18 |
qed "lfp_lowerbound"; |
|
19 |
||
20 |
val prems = goalw Lfp.thy [lfp_def] |
|
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 |
||
26 |
val [mono] = goal Lfp.thy "mono(f) ==> f(lfp(f)) <= lfp(f)"; |
|
27 |
by (EVERY1 [rtac lfp_greatest, rtac subset_trans, |
|
28 |
rtac (mono RS monoD), rtac lfp_lowerbound, atac, atac]); |
|
29 |
qed "lfp_lemma2"; |
|
30 |
||
31 |
val [mono] = goal Lfp.thy "mono(f) ==> lfp(f) <= f(lfp(f))"; |
|
32 |
by (EVERY1 [rtac lfp_lowerbound, rtac (mono RS monoD), |
|
33 |
rtac lfp_lemma2, rtac mono]); |
|
34 |
qed "lfp_lemma3"; |
|
35 |
||
36 |
val [mono] = goal Lfp.thy "mono(f) ==> lfp(f) = f(lfp(f))"; |
|
37 |
by (REPEAT (resolve_tac [equalityI,lfp_lemma2,lfp_lemma3,mono] 1)); |
|
38 |
qed "lfp_Tarski"; |
|
39 |
||
40 |
(*** General induction rule for least fixed points ***) |
|
41 |
||
42 |
val [lfp,mono,indhyp] = goal Lfp.thy |
|
43 |
"[| a: lfp(f); mono(f); \ |
|
44 |
\ !!x. [| x: f(lfp(f) Int {x.P(x)}) |] ==> P(x) \ |
|
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, |
|
49 |
rtac (Int_lower1 RS (mono RS monoD)), |
|
50 |
rtac (mono RS lfp_lemma2), |
|
51 |
rtac (CollectI RS subsetI), rtac indhyp, atac]); |
|
52 |
qed "induct"; |
|
53 |
||
1114 | 54 |
val major::prems = goal Lfp.thy |
55 |
"[| (a,b) : lfp f; mono f; \ |
|
56 |
\ !!a b. (a,b) : f(lfp f Int Collect(split P)) ==> P a b |] ==> P a b"; |
|
57 |
by(res_inst_tac [("c1","P")] (split RS subst) 1); |
|
58 |
br (major RS induct) 1; |
|
59 |
brs prems 1; |
|
60 |
by(res_inst_tac[("p","x")]PairE 1); |
|
61 |
by(hyp_subst_tac 1); |
|
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1125
diff
changeset
|
62 |
by(asm_simp_tac (!simpset addsimps prems) 1); |
1114 | 63 |
qed"induct2"; |
64 |
||
1125 | 65 |
(*** Fixpoint induction a la David Park ***) |
66 |
goal Lfp.thy "!!f. [| mono f; f A <= A |] ==> lfp(f) <= A"; |
|
67 |
br subsetI 1; |
|
68 |
by(EVERY[etac induct 1, atac 1, etac subsetD 1, rtac subsetD 1, |
|
69 |
atac 2, fast_tac (set_cs addSEs [monoD]) 1]); |
|
70 |
qed "Park_induct"; |
|
71 |
||
923 | 72 |
(** Definition forms of lfp_Tarski and induct, to control unfolding **) |
73 |
||
74 |
val [rew,mono] = goal Lfp.thy "[| h==lfp(f); mono(f) |] ==> h = f(h)"; |
|
75 |
by (rewtac rew); |
|
76 |
by (rtac (mono RS lfp_Tarski) 1); |
|
77 |
qed "def_lfp_Tarski"; |
|
78 |
||
79 |
val rew::prems = goal Lfp.thy |
|
80 |
"[| A == lfp(f); mono(f); a:A; \ |
|
81 |
\ !!x. [| x: f(A Int {x.P(x)}) |] ==> P(x) \ |
|
82 |
\ |] ==> P(a)"; |
|
83 |
by (EVERY1 [rtac induct, (*backtracking to force correct induction*) |
|
84 |
REPEAT1 o (ares_tac (map (rewrite_rule [rew]) prems))]); |
|
85 |
qed "def_induct"; |
|
86 |
||
87 |
(*Monotonicity of lfp!*) |
|
88 |
val [prem] = goal Lfp.thy "[| !!Z. f(Z)<=g(Z) |] ==> lfp(f) <= lfp(g)"; |
|
89 |
br (lfp_lowerbound RS lfp_greatest) 1; |
|
90 |
be (prem RS subset_trans) 1; |
|
91 |
qed "lfp_mono"; |