(* Title: CCL/Lfp.ML ID: $Id: Lfp.ML,v 1.5 2005/09/17 15:35:28 wenzelm Exp $ *) (*** Proof of Knaster-Tarski Theorem ***) (* lfp(f) is the greatest lower bound of {u. f(u) <= u} *) val prems = goalw (the_context ()) [lfp_def] "[| f(A) <= A |] ==> lfp(f) <= A"; by (rtac (CollectI RS Inter_lower) 1); by (resolve_tac prems 1); qed "lfp_lowerbound"; val prems = goalw (the_context ()) [lfp_def] "[| !!u. f(u) <= u ==> A<=u |] ==> A <= lfp(f)"; by (REPEAT (ares_tac ([Inter_greatest]@prems) 1)); by (etac CollectD 1); qed "lfp_greatest"; val [mono] = goal (the_context ()) "mono(f) ==> f(lfp(f)) <= lfp(f)"; by (EVERY1 [rtac lfp_greatest, rtac subset_trans, rtac (mono RS monoD), rtac lfp_lowerbound, atac, atac]); qed "lfp_lemma2"; val [mono] = goal (the_context ()) "mono(f) ==> lfp(f) <= f(lfp(f))"; by (EVERY1 [rtac lfp_lowerbound, rtac (mono RS monoD), rtac lfp_lemma2, rtac mono]); qed "lfp_lemma3"; val [mono] = goal (the_context ()) "mono(f) ==> lfp(f) = f(lfp(f))"; by (REPEAT (resolve_tac [equalityI,lfp_lemma2,lfp_lemma3,mono] 1)); qed "lfp_Tarski"; (*** General induction rule for least fixed points ***) val [lfp,mono,indhyp] = goal (the_context ()) "[| a: lfp(f); mono(f); \ \ !!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x) \ \ |] ==> P(a)"; by (res_inst_tac [("a","a")] (Int_lower2 RS subsetD RS CollectD) 1); by (rtac (lfp RSN (2, lfp_lowerbound RS subsetD)) 1); by (EVERY1 [rtac Int_greatest, rtac subset_trans, rtac (Int_lower1 RS (mono RS monoD)), rtac (mono RS lfp_lemma2), rtac (CollectI RS subsetI), rtac indhyp, atac]); qed "induct"; (** Definition forms of lfp_Tarski and induct, to control unfolding **) val [rew,mono] = goal (the_context ()) "[| h==lfp(f); mono(f) |] ==> h = f(h)"; by (rewtac rew); by (rtac (mono RS lfp_Tarski) 1); qed "def_lfp_Tarski"; val rew::prems = goal (the_context ()) "[| A == lfp(f); a:A; mono(f); \ \ !!x. [| x: f(A Int {x. P(x)}) |] ==> P(x) \ \ |] ==> P(a)"; by (EVERY1 [rtac induct, (*backtracking to force correct induction*) REPEAT1 o (ares_tac (map (rewrite_rule [rew]) prems))]); qed "def_induct"; (*Monotonicity of lfp!*) val prems = goal (the_context ()) "[| mono(g); !!Z. f(Z)<=g(Z) |] ==> lfp(f) <= lfp(g)"; by (rtac lfp_lowerbound 1); by (rtac subset_trans 1); by (resolve_tac prems 1); by (rtac lfp_lemma2 1); by (resolve_tac prems 1); qed "lfp_mono";