src/HOL/Lfp.ML
 author paulson Thu Jan 08 18:10:34 1998 +0100 (1998-01-08) changeset 4537 4e835bd9fada parent 3842 b55686a7b22c child 5098 48e70d9fe05f permissions -rw-r--r--
Expressed most Oops rules using Notes instead of Says, and other tidying
 clasohm@1465 ` 1` ```(* Title: HOL/lfp.ML ``` clasohm@923 ` 2` ``` ID: \$Id\$ ``` clasohm@1465 ` 3` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` clasohm@923 ` 4` ``` Copyright 1992 University of Cambridge ``` clasohm@923 ` 5` clasohm@923 ` 6` ```For lfp.thy. The Knaster-Tarski Theorem ``` clasohm@923 ` 7` ```*) ``` clasohm@923 ` 8` clasohm@923 ` 9` ```open Lfp; ``` clasohm@923 ` 10` clasohm@923 ` 11` ```(*** Proof of Knaster-Tarski Theorem ***) ``` clasohm@923 ` 12` clasohm@923 ` 13` ```(* lfp(f) is the greatest lower bound of {u. f(u) <= u} *) ``` clasohm@923 ` 14` clasohm@923 ` 15` ```val prems = goalw Lfp.thy [lfp_def] "[| f(A) <= A |] ==> lfp(f) <= A"; ``` clasohm@923 ` 16` ```by (rtac (CollectI RS Inter_lower) 1); ``` clasohm@923 ` 17` ```by (resolve_tac prems 1); ``` clasohm@923 ` 18` ```qed "lfp_lowerbound"; ``` clasohm@923 ` 19` clasohm@923 ` 20` ```val prems = goalw Lfp.thy [lfp_def] ``` clasohm@923 ` 21` ``` "[| !!u. f(u) <= u ==> A<=u |] ==> A <= lfp(f)"; ``` clasohm@923 ` 22` ```by (REPEAT (ares_tac ([Inter_greatest]@prems) 1)); ``` clasohm@923 ` 23` ```by (etac CollectD 1); ``` clasohm@923 ` 24` ```qed "lfp_greatest"; ``` clasohm@923 ` 25` clasohm@923 ` 26` ```val [mono] = goal Lfp.thy "mono(f) ==> f(lfp(f)) <= lfp(f)"; ``` clasohm@923 ` 27` ```by (EVERY1 [rtac lfp_greatest, rtac subset_trans, ``` clasohm@1465 ` 28` ``` rtac (mono RS monoD), rtac lfp_lowerbound, atac, atac]); ``` clasohm@923 ` 29` ```qed "lfp_lemma2"; ``` clasohm@923 ` 30` clasohm@923 ` 31` ```val [mono] = goal Lfp.thy "mono(f) ==> lfp(f) <= f(lfp(f))"; ``` clasohm@923 ` 32` ```by (EVERY1 [rtac lfp_lowerbound, rtac (mono RS monoD), ``` clasohm@1465 ` 33` ``` rtac lfp_lemma2, rtac mono]); ``` clasohm@923 ` 34` ```qed "lfp_lemma3"; ``` clasohm@923 ` 35` clasohm@923 ` 36` ```val [mono] = goal Lfp.thy "mono(f) ==> lfp(f) = f(lfp(f))"; ``` clasohm@923 ` 37` ```by (REPEAT (resolve_tac [equalityI,lfp_lemma2,lfp_lemma3,mono] 1)); ``` clasohm@923 ` 38` ```qed "lfp_Tarski"; ``` clasohm@923 ` 39` clasohm@923 ` 40` ```(*** General induction rule for least fixed points ***) ``` clasohm@923 ` 41` clasohm@923 ` 42` ```val [lfp,mono,indhyp] = goal Lfp.thy ``` clasohm@1465 ` 43` ``` "[| a: lfp(f); mono(f); \ ``` wenzelm@3842 ` 44` ```\ !!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x) \ ``` clasohm@923 ` 45` ```\ |] ==> P(a)"; ``` clasohm@923 ` 46` ```by (res_inst_tac [("a","a")] (Int_lower2 RS subsetD RS CollectD) 1); ``` clasohm@923 ` 47` ```by (rtac (lfp RSN (2, lfp_lowerbound RS subsetD)) 1); ``` clasohm@923 ` 48` ```by (EVERY1 [rtac Int_greatest, rtac subset_trans, ``` clasohm@1465 ` 49` ``` rtac (Int_lower1 RS (mono RS monoD)), ``` clasohm@1465 ` 50` ``` rtac (mono RS lfp_lemma2), ``` clasohm@1465 ` 51` ``` rtac (CollectI RS subsetI), rtac indhyp, atac]); ``` clasohm@923 ` 52` ```qed "induct"; ``` clasohm@923 ` 53` nipkow@1746 ` 54` ```bind_thm ``` nipkow@1746 ` 55` ``` ("induct2", ``` nipkow@1746 ` 56` ``` Prod_Syntax.split_rule ``` nipkow@1746 ` 57` ``` (read_instantiate [("a","(a,b)")] induct)); ``` nipkow@1114 ` 58` nipkow@1125 ` 59` clasohm@923 ` 60` ```(** Definition forms of lfp_Tarski and induct, to control unfolding **) ``` clasohm@923 ` 61` clasohm@923 ` 62` ```val [rew,mono] = goal Lfp.thy "[| h==lfp(f); mono(f) |] ==> h = f(h)"; ``` clasohm@923 ` 63` ```by (rewtac rew); ``` clasohm@923 ` 64` ```by (rtac (mono RS lfp_Tarski) 1); ``` clasohm@923 ` 65` ```qed "def_lfp_Tarski"; ``` clasohm@923 ` 66` clasohm@923 ` 67` ```val rew::prems = goal Lfp.thy ``` clasohm@1465 ` 68` ``` "[| A == lfp(f); mono(f); a:A; \ ``` wenzelm@3842 ` 69` ```\ !!x. [| x: f(A Int {x. P(x)}) |] ==> P(x) \ ``` clasohm@923 ` 70` ```\ |] ==> P(a)"; ``` clasohm@1465 ` 71` ```by (EVERY1 [rtac induct, (*backtracking to force correct induction*) ``` clasohm@1465 ` 72` ``` REPEAT1 o (ares_tac (map (rewrite_rule [rew]) prems))]); ``` clasohm@923 ` 73` ```qed "def_induct"; ``` clasohm@923 ` 74` clasohm@923 ` 75` ```(*Monotonicity of lfp!*) ``` clasohm@923 ` 76` ```val [prem] = goal Lfp.thy "[| !!Z. f(Z)<=g(Z) |] ==> lfp(f) <= lfp(g)"; ``` clasohm@1465 ` 77` ```by (rtac (lfp_lowerbound RS lfp_greatest) 1); ``` clasohm@1465 ` 78` ```by (etac (prem RS subset_trans) 1); ``` clasohm@923 ` 79` ```qed "lfp_mono"; ```