src/HOL/Gfp.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
 paulson@15381 ` 1` ```(* ID: \$Id\$ ``` clasohm@1475 ` 2` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` clasohm@923 ` 3` ``` Copyright 1994 University of Cambridge ``` clasohm@923 ` 4` clasohm@923 ` 5` ```*) ``` clasohm@923 ` 6` paulson@15386 ` 7` ```header{*Greatest Fixed Points and the Knaster-Tarski Theorem*} ``` paulson@15381 ` 8` paulson@15381 ` 9` ```theory Gfp ``` nipkow@15140 ` 10` ```imports Lfp ``` nipkow@15131 ` 11` ```begin ``` clasohm@1558 ` 12` clasohm@1558 ` 13` ```constdefs ``` skalberg@14169 ` 14` ``` gfp :: "['a set=>'a set] => 'a set" ``` paulson@15381 ` 15` ``` "gfp(f) == Union({u. u \ f(u)})" ``` paulson@15381 ` 16` paulson@15381 ` 17` paulson@15381 ` 18` paulson@15386 ` 19` ```subsection{*Proof of Knaster-Tarski Theorem using @{term gfp}*} ``` paulson@15381 ` 20` paulson@15381 ` 21` paulson@15386 ` 22` ```text{*@{term "gfp f"} is the greatest lower bound of ``` paulson@15381 ` 23` ``` the set @{term "{u. u \ f(u)}"} *} ``` paulson@15381 ` 24` paulson@15381 ` 25` ```lemma gfp_upperbound: "[| X \ f(X) |] ==> X \ gfp(f)" ``` paulson@15381 ` 26` ```by (auto simp add: gfp_def) ``` paulson@15381 ` 27` paulson@15381 ` 28` ```lemma gfp_least: "[| !!u. u \ f(u) ==> u\X |] ==> gfp(f) \ X" ``` paulson@15381 ` 29` ```by (auto simp add: gfp_def) ``` paulson@15381 ` 30` paulson@15381 ` 31` ```lemma gfp_lemma2: "mono(f) ==> gfp(f) \ f(gfp(f))" ``` paulson@15381 ` 32` ```by (rules intro: gfp_least subset_trans monoD gfp_upperbound) ``` paulson@15381 ` 33` paulson@15381 ` 34` ```lemma gfp_lemma3: "mono(f) ==> f(gfp(f)) \ gfp(f)" ``` paulson@15381 ` 35` ```by (rules intro: gfp_lemma2 monoD gfp_upperbound) ``` paulson@15381 ` 36` paulson@15381 ` 37` ```lemma gfp_unfold: "mono(f) ==> gfp(f) = f(gfp(f))" ``` paulson@15381 ` 38` ```by (rules intro: equalityI gfp_lemma2 gfp_lemma3) ``` paulson@15381 ` 39` paulson@15381 ` 40` ```subsection{*Coinduction rules for greatest fixed points*} ``` paulson@15381 ` 41` paulson@15381 ` 42` ```text{*weak version*} ``` paulson@15381 ` 43` ```lemma weak_coinduct: "[| a: X; X \ f(X) |] ==> a : gfp(f)" ``` paulson@15381 ` 44` ```by (rule gfp_upperbound [THEN subsetD], auto) ``` paulson@15381 ` 45` paulson@15381 ` 46` ```lemma weak_coinduct_image: "!!X. [| a : X; g`X \ f (g`X) |] ==> g a : gfp f" ``` paulson@15381 ` 47` ```apply (erule gfp_upperbound [THEN subsetD]) ``` paulson@15381 ` 48` ```apply (erule imageI) ``` paulson@15381 ` 49` ```done ``` paulson@15381 ` 50` paulson@15381 ` 51` ```lemma coinduct_lemma: ``` paulson@15381 ` 52` ``` "[| X \ f(X Un gfp(f)); mono(f) |] ==> X Un gfp(f) \ f(X Un gfp(f))" ``` paulson@15381 ` 53` ```by (blast dest: gfp_lemma2 mono_Un) ``` paulson@15381 ` 54` paulson@15381 ` 55` ```text{*strong version, thanks to Coen and Frost*} ``` paulson@15381 ` 56` ```lemma coinduct: "[| mono(f); a: X; X \ f(X Un gfp(f)) |] ==> a : gfp(f)" ``` paulson@15381 ` 57` ```by (blast intro: weak_coinduct [OF _ coinduct_lemma]) ``` paulson@15381 ` 58` paulson@15381 ` 59` ```lemma gfp_fun_UnI2: "[| mono(f); a: gfp(f) |] ==> a: f(X Un gfp(f))" ``` paulson@15381 ` 60` ```by (blast dest: gfp_lemma2 mono_Un) ``` paulson@15381 ` 61` paulson@15381 ` 62` ```subsection{*Even Stronger Coinduction Rule, by Martin Coen*} ``` paulson@15381 ` 63` paulson@15381 ` 64` ```text{* Weakens the condition @{term "X \ f(X)"} to one expressed using both ``` paulson@15381 ` 65` ``` @{term lfp} and @{term gfp}*} ``` paulson@15381 ` 66` paulson@15381 ` 67` ```lemma coinduct3_mono_lemma: "mono(f) ==> mono(%x. f(x) Un X Un B)" ``` paulson@15381 ` 68` ```by (rules intro: subset_refl monoI Un_mono monoD) ``` paulson@15381 ` 69` paulson@15381 ` 70` ```lemma coinduct3_lemma: ``` paulson@15381 ` 71` ``` "[| X \ f(lfp(%x. f(x) Un X Un gfp(f))); mono(f) |] ``` paulson@15381 ` 72` ``` ==> lfp(%x. f(x) Un X Un gfp(f)) \ f(lfp(%x. f(x) Un X Un gfp(f)))" ``` paulson@15381 ` 73` ```apply (rule subset_trans) ``` paulson@15381 ` 74` ```apply (erule coinduct3_mono_lemma [THEN lfp_lemma3]) ``` paulson@15381 ` 75` ```apply (rule Un_least [THEN Un_least]) ``` paulson@15381 ` 76` ```apply (rule subset_refl, assumption) ``` paulson@15381 ` 77` ```apply (rule gfp_unfold [THEN equalityD1, THEN subset_trans], assumption) ``` paulson@15381 ` 78` ```apply (rule monoD, assumption) ``` paulson@15381 ` 79` ```apply (subst coinduct3_mono_lemma [THEN lfp_unfold], auto) ``` paulson@15381 ` 80` ```done ``` paulson@15381 ` 81` paulson@15381 ` 82` ```lemma coinduct3: ``` paulson@15381 ` 83` ``` "[| mono(f); a:X; X \ f(lfp(%x. f(x) Un X Un gfp(f))) |] ==> a : gfp(f)" ``` paulson@15381 ` 84` ```apply (rule coinduct3_lemma [THEN [2] weak_coinduct]) ``` paulson@15381 ` 85` ```apply (rule coinduct3_mono_lemma [THEN lfp_unfold, THEN ssubst], auto) ``` paulson@15381 ` 86` ```done ``` paulson@15381 ` 87` paulson@15381 ` 88` paulson@15381 ` 89` ```text{*Definition forms of @{text gfp_unfold} and @{text coinduct}, ``` paulson@15381 ` 90` ``` to control unfolding*} ``` paulson@15381 ` 91` paulson@15381 ` 92` ```lemma def_gfp_unfold: "[| A==gfp(f); mono(f) |] ==> A = f(A)" ``` paulson@15381 ` 93` ```by (auto intro!: gfp_unfold) ``` paulson@15381 ` 94` paulson@15381 ` 95` ```lemma def_coinduct: ``` paulson@15381 ` 96` ``` "[| A==gfp(f); mono(f); a:X; X \ f(X Un A) |] ==> a: A" ``` paulson@15381 ` 97` ```by (auto intro!: coinduct) ``` paulson@15381 ` 98` paulson@15381 ` 99` ```(*The version used in the induction/coinduction package*) ``` paulson@15381 ` 100` ```lemma def_Collect_coinduct: ``` paulson@15381 ` 101` ``` "[| A == gfp(%w. Collect(P(w))); mono(%w. Collect(P(w))); ``` paulson@15381 ` 102` ``` a: X; !!z. z: X ==> P (X Un A) z |] ==> ``` paulson@15381 ` 103` ``` a : A" ``` paulson@15381 ` 104` ```apply (erule def_coinduct, auto) ``` paulson@15381 ` 105` ```done ``` paulson@15381 ` 106` paulson@15381 ` 107` ```lemma def_coinduct3: ``` paulson@15381 ` 108` ``` "[| A==gfp(f); mono(f); a:X; X \ f(lfp(%x. f(x) Un X Un A)) |] ==> a: A" ``` paulson@15381 ` 109` ```by (auto intro!: coinduct3) ``` paulson@15381 ` 110` paulson@15381 ` 111` ```text{*Monotonicity of @{term gfp}!*} ``` paulson@15381 ` 112` ```lemma gfp_mono: "[| !!Z. f(Z)\g(Z) |] ==> gfp(f) \ gfp(g)" ``` paulson@15381 ` 113` ```by (rule gfp_upperbound [THEN gfp_least], blast) ``` paulson@15381 ` 114` paulson@15381 ` 115` paulson@15381 ` 116` ```ML ``` paulson@15381 ` 117` ```{* ``` paulson@15381 ` 118` ```val gfp_def = thm "gfp_def"; ``` paulson@15381 ` 119` ```val gfp_upperbound = thm "gfp_upperbound"; ``` paulson@15381 ` 120` ```val gfp_least = thm "gfp_least"; ``` paulson@15381 ` 121` ```val gfp_unfold = thm "gfp_unfold"; ``` paulson@15381 ` 122` ```val weak_coinduct = thm "weak_coinduct"; ``` paulson@15381 ` 123` ```val weak_coinduct_image = thm "weak_coinduct_image"; ``` paulson@15381 ` 124` ```val coinduct = thm "coinduct"; ``` paulson@15381 ` 125` ```val gfp_fun_UnI2 = thm "gfp_fun_UnI2"; ``` paulson@15381 ` 126` ```val coinduct3 = thm "coinduct3"; ``` paulson@15381 ` 127` ```val def_gfp_unfold = thm "def_gfp_unfold"; ``` paulson@15381 ` 128` ```val def_coinduct = thm "def_coinduct"; ``` paulson@15381 ` 129` ```val def_Collect_coinduct = thm "def_Collect_coinduct"; ``` paulson@15381 ` 130` ```val def_coinduct3 = thm "def_coinduct3"; ``` paulson@15381 ` 131` ```val gfp_mono = thm "gfp_mono"; ``` paulson@15381 ` 132` ```*} ``` paulson@15381 ` 133` clasohm@1558 ` 134` clasohm@923 ` 135` ```end ```