src/CCL/lfp.ML
 author paulson Fri Feb 16 17:24:51 1996 +0100 (1996-02-16) changeset 1511 09354d37a5ab parent 0 a5a9c433f639 permissions -rw-r--r--
Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.
 clasohm@0 1 (* Title: CCL/lfp clasohm@0 2 ID: \$Id\$ clasohm@0 3 clasohm@0 4 Modified version of clasohm@0 5 Title: HOL/lfp.ML clasohm@0 6 Author: Lawrence C Paulson, Cambridge University Computer Laboratory clasohm@0 7 Copyright 1992 University of Cambridge clasohm@0 8 clasohm@0 9 For lfp.thy. The Knaster-Tarski Theorem clasohm@0 10 *) clasohm@0 11 clasohm@0 12 open Lfp; clasohm@0 13 clasohm@0 14 (*** Proof of Knaster-Tarski Theorem ***) clasohm@0 15 clasohm@0 16 (* lfp(f) is the greatest lower bound of {u. f(u) <= u} *) clasohm@0 17 clasohm@0 18 val prems = goalw Lfp.thy [lfp_def] "[| f(A) <= A |] ==> lfp(f) <= A"; clasohm@0 19 by (rtac (CollectI RS Inter_lower) 1); clasohm@0 20 by (resolve_tac prems 1); clasohm@0 21 val lfp_lowerbound = result(); clasohm@0 22 clasohm@0 23 val prems = goalw Lfp.thy [lfp_def] clasohm@0 24 "[| !!u. f(u) <= u ==> A<=u |] ==> A <= lfp(f)"; clasohm@0 25 by (REPEAT (ares_tac ([Inter_greatest]@prems) 1)); clasohm@0 26 by (etac CollectD 1); clasohm@0 27 val lfp_greatest = result(); clasohm@0 28 clasohm@0 29 val [mono] = goal Lfp.thy "mono(f) ==> f(lfp(f)) <= lfp(f)"; clasohm@0 30 by (EVERY1 [rtac lfp_greatest, rtac subset_trans, clasohm@0 31 rtac (mono RS monoD), rtac lfp_lowerbound, atac, atac]); clasohm@0 32 val lfp_lemma2 = result(); clasohm@0 33 clasohm@0 34 val [mono] = goal Lfp.thy "mono(f) ==> lfp(f) <= f(lfp(f))"; clasohm@0 35 by (EVERY1 [rtac lfp_lowerbound, rtac (mono RS monoD), clasohm@0 36 rtac lfp_lemma2, rtac mono]); clasohm@0 37 val lfp_lemma3 = result(); clasohm@0 38 clasohm@0 39 val [mono] = goal Lfp.thy "mono(f) ==> lfp(f) = f(lfp(f))"; clasohm@0 40 by (REPEAT (resolve_tac [equalityI,lfp_lemma2,lfp_lemma3,mono] 1)); clasohm@0 41 val lfp_Tarski = result(); clasohm@0 42 clasohm@0 43 clasohm@0 44 (*** General induction rule for least fixed points ***) clasohm@0 45 clasohm@0 46 val [lfp,mono,indhyp] = goal Lfp.thy clasohm@0 47 "[| a: lfp(f); mono(f); \ clasohm@0 48 \ !!x. [| x: f(lfp(f) Int {x.P(x)}) |] ==> P(x) \ clasohm@0 49 \ |] ==> P(a)"; clasohm@0 50 by (res_inst_tac [("a","a")] (Int_lower2 RS subsetD RS CollectD) 1); clasohm@0 51 by (rtac (lfp RSN (2, lfp_lowerbound RS subsetD)) 1); clasohm@0 52 by (EVERY1 [rtac Int_greatest, rtac subset_trans, clasohm@0 53 rtac (Int_lower1 RS (mono RS monoD)), clasohm@0 54 rtac (mono RS lfp_lemma2), clasohm@0 55 rtac (CollectI RS subsetI), rtac indhyp, atac]); clasohm@0 56 val induct = result(); clasohm@0 57 clasohm@0 58 (** Definition forms of lfp_Tarski and induct, to control unfolding **) clasohm@0 59 clasohm@0 60 val [rew,mono] = goal Lfp.thy "[| h==lfp(f); mono(f) |] ==> h = f(h)"; clasohm@0 61 by (rewtac rew); clasohm@0 62 by (rtac (mono RS lfp_Tarski) 1); clasohm@0 63 val def_lfp_Tarski = result(); clasohm@0 64 clasohm@0 65 val rew::prems = goal Lfp.thy clasohm@0 66 "[| A == lfp(f); a:A; mono(f); \ clasohm@0 67 \ !!x. [| x: f(A Int {x.P(x)}) |] ==> P(x) \ clasohm@0 68 \ |] ==> P(a)"; clasohm@0 69 by (EVERY1 [rtac induct, (*backtracking to force correct induction*) clasohm@0 70 REPEAT1 o (ares_tac (map (rewrite_rule [rew]) prems))]); clasohm@0 71 val def_induct = result(); clasohm@0 72 clasohm@0 73 (*Monotonicity of lfp!*) clasohm@0 74 val prems = goal Lfp.thy clasohm@0 75 "[| mono(g); !!Z. f(Z)<=g(Z) |] ==> lfp(f) <= lfp(g)"; clasohm@0 76 by (rtac lfp_lowerbound 1); clasohm@0 77 by (rtac subset_trans 1); clasohm@0 78 by (resolve_tac prems 1); clasohm@0 79 by (rtac lfp_lemma2 1); clasohm@0 80 by (resolve_tac prems 1); clasohm@0 81 val lfp_mono = result(); clasohm@0 82