src/HOL/Lfp.thy
 author paulson Tue Jun 28 15:27:45 2005 +0200 (2005-06-28) changeset 16587 b34c8aa657a5 parent 15386 06757406d8cf permissions -rw-r--r--
Constant "If" is now local
 clasohm@1475 ` 1` ```(* Title: HOL/Lfp.thy ``` clasohm@923 ` 2` ``` ID: \$Id\$ ``` clasohm@1475 ` 3` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` clasohm@923 ` 4` ``` Copyright 1992 University of Cambridge ``` paulson@15386 ` 5` ```*) ``` clasohm@923 ` 6` paulson@15386 ` 7` ```header{*Least Fixed Points and the Knaster-Tarski Theorem*} ``` clasohm@923 ` 8` nipkow@15131 ` 9` ```theory Lfp ``` nipkow@15140 ` 10` ```imports Product_Type ``` nipkow@15131 ` 11` ```begin ``` clasohm@1558 ` 12` clasohm@1558 ` 13` ```constdefs ``` skalberg@14169 ` 14` ``` lfp :: "['a set \ 'a set] \ 'a set" ``` paulson@15386 ` 15` ``` "lfp(f) == Inter({u. f(u) \ u})" --{*least fixed point*} ``` paulson@15386 ` 16` paulson@15386 ` 17` paulson@15386 ` 18` paulson@15386 ` 19` ```subsection{*Proof of Knaster-Tarski Theorem using @{term lfp}*} ``` paulson@15386 ` 20` paulson@15386 ` 21` paulson@15386 ` 22` ```text{*@{term "lfp f"} is the least upper bound of ``` paulson@15386 ` 23` ``` the set @{term "{u. f(u) \ u}"} *} ``` paulson@15386 ` 24` paulson@15386 ` 25` ```lemma lfp_lowerbound: "f(A) \ A ==> lfp(f) \ A" ``` paulson@15386 ` 26` ```by (auto simp add: lfp_def) ``` paulson@15386 ` 27` paulson@15386 ` 28` ```lemma lfp_greatest: "[| !!u. f(u) \ u ==> A\u |] ==> A \ lfp(f)" ``` paulson@15386 ` 29` ```by (auto simp add: lfp_def) ``` paulson@15386 ` 30` paulson@15386 ` 31` ```lemma lfp_lemma2: "mono(f) ==> f(lfp(f)) \ lfp(f)" ``` paulson@15386 ` 32` ```by (rules intro: lfp_greatest subset_trans monoD lfp_lowerbound) ``` paulson@15386 ` 33` paulson@15386 ` 34` ```lemma lfp_lemma3: "mono(f) ==> lfp(f) \ f(lfp(f))" ``` paulson@15386 ` 35` ```by (rules intro: lfp_lemma2 monoD lfp_lowerbound) ``` paulson@15386 ` 36` paulson@15386 ` 37` ```lemma lfp_unfold: "mono(f) ==> lfp(f) = f(lfp(f))" ``` paulson@15386 ` 38` ```by (rules intro: equalityI lfp_lemma2 lfp_lemma3) ``` paulson@15386 ` 39` paulson@15386 ` 40` ```subsection{*General induction rules for greatest fixed points*} ``` paulson@15386 ` 41` paulson@15386 ` 42` ```lemma lfp_induct: ``` paulson@15386 ` 43` ``` assumes lfp: "a: lfp(f)" ``` paulson@15386 ` 44` ``` and mono: "mono(f)" ``` paulson@15386 ` 45` ``` and indhyp: "!!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)" ``` paulson@15386 ` 46` ``` shows "P(a)" ``` paulson@15386 ` 47` ```apply (rule_tac a=a in Int_lower2 [THEN subsetD, THEN CollectD]) ``` paulson@15386 ` 48` ```apply (rule lfp [THEN [2] lfp_lowerbound [THEN subsetD]]) ``` paulson@15386 ` 49` ```apply (rule Int_greatest) ``` paulson@15386 ` 50` ``` apply (rule subset_trans [OF Int_lower1 [THEN mono [THEN monoD]] ``` paulson@15386 ` 51` ``` mono [THEN lfp_lemma2]]) ``` paulson@15386 ` 52` ```apply (blast intro: indhyp) ``` paulson@15386 ` 53` ```done ``` paulson@15386 ` 54` paulson@15386 ` 55` paulson@15386 ` 56` ```text{*Version of induction for binary relations*} ``` paulson@15386 ` 57` ```lemmas lfp_induct2 = lfp_induct [of "(a,b)", split_format (complete)] ``` paulson@15386 ` 58` paulson@15386 ` 59` paulson@15386 ` 60` ```lemma lfp_ordinal_induct: ``` paulson@15386 ` 61` ``` assumes mono: "mono f" ``` paulson@15386 ` 62` ``` shows "[| !!S. P S ==> P(f S); !!M. !S:M. P S ==> P(Union M) |] ``` paulson@15386 ` 63` ``` ==> P(lfp f)" ``` paulson@15386 ` 64` ```apply(subgoal_tac "lfp f = Union{S. S \ lfp f & P S}") ``` paulson@15386 ` 65` ``` apply (erule ssubst, simp) ``` paulson@15386 ` 66` ```apply(subgoal_tac "Union{S. S \ lfp f & P S} \ lfp f") ``` paulson@15386 ` 67` ``` prefer 2 apply blast ``` paulson@15386 ` 68` ```apply(rule equalityI) ``` paulson@15386 ` 69` ``` prefer 2 apply assumption ``` paulson@15386 ` 70` ```apply(drule mono [THEN monoD]) ``` paulson@15386 ` 71` ```apply (cut_tac mono [THEN lfp_unfold], simp) ``` paulson@15386 ` 72` ```apply (rule lfp_lowerbound, auto) ``` paulson@15386 ` 73` ```done ``` paulson@15386 ` 74` paulson@15386 ` 75` paulson@15386 ` 76` ```text{*Definition forms of @{text lfp_unfold} and @{text lfp_induct}, ``` paulson@15386 ` 77` ``` to control unfolding*} ``` paulson@15386 ` 78` paulson@15386 ` 79` ```lemma def_lfp_unfold: "[| h==lfp(f); mono(f) |] ==> h = f(h)" ``` paulson@15386 ` 80` ```by (auto intro!: lfp_unfold) ``` paulson@15386 ` 81` paulson@15386 ` 82` ```lemma def_lfp_induct: ``` paulson@15386 ` 83` ``` "[| A == lfp(f); mono(f); a:A; ``` paulson@15386 ` 84` ``` !!x. [| x: f(A Int {x. P(x)}) |] ==> P(x) ``` paulson@15386 ` 85` ``` |] ==> P(a)" ``` paulson@15386 ` 86` ```by (blast intro: lfp_induct) ``` paulson@15386 ` 87` paulson@15386 ` 88` ```(*Monotonicity of lfp!*) ``` paulson@15386 ` 89` ```lemma lfp_mono: "[| !!Z. f(Z)\g(Z) |] ==> lfp(f) \ lfp(g)" ``` paulson@15386 ` 90` ```by (rule lfp_lowerbound [THEN lfp_greatest], blast) ``` paulson@15386 ` 91` paulson@15386 ` 92` paulson@15386 ` 93` ```ML ``` paulson@15386 ` 94` ```{* ``` paulson@15386 ` 95` ```val lfp_def = thm "lfp_def"; ``` paulson@15386 ` 96` ```val lfp_lowerbound = thm "lfp_lowerbound"; ``` paulson@15386 ` 97` ```val lfp_greatest = thm "lfp_greatest"; ``` paulson@15386 ` 98` ```val lfp_unfold = thm "lfp_unfold"; ``` paulson@15386 ` 99` ```val lfp_induct = thm "lfp_induct"; ``` paulson@15386 ` 100` ```val lfp_induct2 = thm "lfp_induct2"; ``` paulson@15386 ` 101` ```val lfp_ordinal_induct = thm "lfp_ordinal_induct"; ``` paulson@15386 ` 102` ```val def_lfp_unfold = thm "def_lfp_unfold"; ``` paulson@15386 ` 103` ```val def_lfp_induct = thm "def_lfp_induct"; ``` paulson@15386 ` 104` ```val lfp_mono = thm "lfp_mono"; ``` paulson@15386 ` 105` ```*} ``` clasohm@1558 ` 106` clasohm@923 ` 107` ```end ```