(* Title: HOL/HOLCF/Adm.thy
Author: Franz Regensburger and Brian Huffman
*)
section \<open>Admissibility and compactness\<close>
theory Adm
imports Cont
begin
default_sort cpo
subsection \<open>Definitions\<close>
definition adm :: "('a::cpo \ bool) \ bool"
where "adm P \ (\Y. chain Y \ (\i. P (Y i)) \ P (\i. Y i))"
lemma admI: "(\Y. \chain Y; \i. P (Y i)\ \ P (\i. Y i)) \ adm P"
unfolding adm_def by fast
lemma admD: "adm P \ chain Y \ (\i. P (Y i)) \ P (\i. Y i)"
unfolding adm_def by fast
lemma admD2: "adm (\x. \ P x) \ chain Y \ P (\i. Y i) \ \i. P (Y i)"
unfolding adm_def by fast
lemma triv_admI: "\x. P x \ adm P"
by (rule admI) (erule spec)
subsection \<open>Admissibility on chain-finite types\<close>
text \<open>For chain-finite (easy) types every formula is admissible.\<close>
lemma adm_chfin [simp]: "adm P"
for P :: "'a::chfin \ bool"
by (rule admI, frule chfin, auto simp add: maxinch_is_thelub)
subsection \<open>Admissibility of special formulae and propagation\<close>
lemma adm_const [simp]: "adm (\x. t)"
by (rule admI, simp)
lemma adm_conj [simp]: "adm (\x. P x) \ adm (\x. Q x) \ adm (\x. P x \ Q x)"
by (fast intro: admI elim: admD)
lemma adm_all [simp]: "(\y. adm (\x. P x y)) \ adm (\x. \y. P x y)"
by (fast intro: admI elim: admD)
lemma adm_ball [simp]: "(\y. y \ A \ adm (\x. P x y)) \ adm (\x. \y\A. P x y)"
by (fast intro: admI elim: admD)
text \<open>Admissibility for disjunction is hard to prove. It requires 2 lemmas.\<close>
lemma adm_disj_lemma1:
assumes adm: "adm P"
assumes chain: "chain Y"
assumes P: "\i. \j\i. P (Y j)"
shows "P (\i. Y i)"
proof -
define f where "f i = (LEAST j. i \ j \ P (Y j))" for i
have chain': "chain (\i. Y (f i))"
unfolding f_def
apply (rule chainI)
apply (rule chain_mono [OF chain])
apply (rule Least_le)
apply (rule LeastI2_ex)
apply (simp_all add: P)
done
have f1: "\i. i \ f i" and f2: "\i. P (Y (f i))"
using LeastI_ex [OF P [rule_format]] by (simp_all add: f_def)
have lub_eq: "(\i. Y i) = (\i. Y (f i))"
apply (rule below_antisym)
apply (rule lub_mono [OF chain chain'])
apply (rule chain_mono [OF chain f1])
apply (rule lub_range_mono [OF _ chain chain'])
apply clarsimp
done
show "P (\i. Y i)"
unfolding lub_eq using adm chain' f2 by (rule admD)
qed
lemma adm_disj_lemma2: "\n::nat. P n \ Q n \ (\i. \j\i. P j) \ (\i. \j\i. Q j)"
apply (erule contrapos_pp)
apply (clarsimp, rename_tac a b)
apply (rule_tac x="max a b" in exI)
apply simp
done
lemma adm_disj [simp]: "adm (\x. P x) \ adm (\x. Q x) \ adm (\x. P x \ Q x)"
apply (rule admI)
apply (erule adm_disj_lemma2 [THEN disjE])
apply (erule (2) adm_disj_lemma1 [THEN disjI1])
apply (erule (2) adm_disj_lemma1 [THEN disjI2])
done
lemma adm_imp [simp]: "adm (\x. \ P x) \ adm (\x. Q x) \ adm (\x. P x \ Q x)"
by (subst imp_conv_disj) (rule adm_disj)
lemma adm_iff [simp]: "adm (\x. P x \ Q x) \ adm (\x. Q x \ P x) \ adm (\x. P x \ Q x)"
by (subst iff_conv_conj_imp) (rule adm_conj)
text \<open>admissibility and continuity\<close>
lemma adm_below [simp]: "cont (\x. u x) \ cont (\x. v x) \ adm (\x. u x \ v x)"
by (simp add: adm_def cont2contlubE lub_mono ch2ch_cont)
lemma adm_eq [simp]: "cont (\x. u x) \ cont (\x. v x) \ adm (\x. u x = v x)"
by (simp add: po_eq_conv)
lemma adm_subst: "cont (\x. t x) \ adm P \ adm (\x. P (t x))"
by (simp add: adm_def cont2contlubE ch2ch_cont)
lemma adm_not_below [simp]: "cont (\x. t x) \ adm (\x. t x \ u)"
by (rule admI) (simp add: cont2contlubE ch2ch_cont lub_below_iff)
subsection \<open>Compactness\<close>
definition compact :: "'a::cpo \ bool"
where "compact k = adm (\x. k \ x)"
lemma compactI: "adm (\x. k \ x) \ compact k"
unfolding compact_def .
lemma compactD: "compact k \ adm (\x. k \ x)"
unfolding compact_def .
lemma compactI2: "(\Y. \chain Y; x \ (\i. Y i)\ \ \i. x \ Y i) \ compact x"
unfolding compact_def adm_def by fast
lemma compactD2: "compact x \ chain Y \ x \ (\i. Y i) \ \i. x \ Y i"
unfolding compact_def adm_def by fast
lemma compact_below_lub_iff: "compact x \ chain Y \ x \ (\i. Y i) \ (\i. x \ Y i)"
by (fast intro: compactD2 elim: below_lub)
lemma compact_chfin [simp]: "compact x"
for x :: "'a::chfin"
by (rule compactI [OF adm_chfin])
lemma compact_imp_max_in_chain: "chain Y \ compact (\i. Y i) \ \i. max_in_chain i Y"
apply (drule (1) compactD2, simp)
apply (erule exE, rule_tac x=i in exI)
apply (rule max_in_chainI)
apply (rule below_antisym)
apply (erule (1) chain_mono)
apply (erule (1) below_trans [OF is_ub_thelub])
done
text \<open>admissibility and compactness\<close>
lemma adm_compact_not_below [simp]:
"compact k \ cont (\x. t x) \ adm (\x. k \ t x)"
unfolding compact_def by (rule adm_subst)
lemma adm_neq_compact [simp]: "compact k \ cont (\x. t x) \ adm (\x. t x \ k)"
by (simp add: po_eq_conv)
lemma adm_compact_neq [simp]: "compact k \ cont (\x. t x) \ adm (\x. k \ t x)"
by (simp add: po_eq_conv)
lemma compact_bottom [simp, intro]: "compact \"
by (rule compactI) simp
text \<open>Any upward-closed predicate is admissible.\<close>
lemma adm_upward:
assumes P: "\x y. \P x; x \ y\ \ P y"
shows "adm P"
by (rule admI, drule spec, erule P, erule is_ub_thelub)
lemmas adm_lemmas =
adm_const adm_conj adm_all adm_ball adm_disj adm_imp adm_iff
adm_below adm_eq adm_not_below
adm_compact_not_below adm_compact_neq adm_neq_compact
end
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
