author | clasohm |
Mon, 05 Feb 1996 21:29:06 +0100 | |
changeset 1476 | 608483c2122a |
parent 1465 | 5d7a7e439cec |
child 1552 | 6f71b5d46700 |
permissions | -rw-r--r-- |
1465 | 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 |
||
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, |
|
1465 | 28 |
rtac (mono RS monoD), rtac lfp_lowerbound, atac, atac]); |
923 | 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), |
|
1465 | 33 |
rtac lfp_lemma2, rtac mono]); |
923 | 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 |
|
1465 | 43 |
"[| a: lfp(f); mono(f); \ |
44 |
\ !!x. [| x: f(lfp(f) Int {x.P(x)}) |] ==> P(x) \ |
|
923 | 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, |
|
1465 | 49 |
rtac (Int_lower1 RS (mono RS monoD)), |
50 |
rtac (mono RS lfp_lemma2), |
|
51 |
rtac (CollectI RS subsetI), rtac indhyp, atac]); |
|
923 | 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); |
|
1465 | 58 |
by (rtac (major RS induct) 1); |
59 |
by (resolve_tac prems 1); |
|
1114 | 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"; |
|
1465 | 67 |
by (rtac subsetI 1); |
1125 | 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 |
|
1465 | 80 |
"[| A == lfp(f); mono(f); a:A; \ |
81 |
\ !!x. [| x: f(A Int {x.P(x)}) |] ==> P(x) \ |
|
923 | 82 |
\ |] ==> P(a)"; |
1465 | 83 |
by (EVERY1 [rtac induct, (*backtracking to force correct induction*) |
84 |
REPEAT1 o (ares_tac (map (rewrite_rule [rew]) prems))]); |
|
923 | 85 |
qed "def_induct"; |
86 |
||
87 |
(*Monotonicity of lfp!*) |
|
88 |
val [prem] = goal Lfp.thy "[| !!Z. f(Z)<=g(Z) |] ==> lfp(f) <= lfp(g)"; |
|
1465 | 89 |
by (rtac (lfp_lowerbound RS lfp_greatest) 1); |
90 |
by (etac (prem RS subset_trans) 1); |
|
923 | 91 |
qed "lfp_mono"; |