section ‹Admissibility and compactness›
theory Adm
imports Cont
begin
default_sort cpo
subsection ‹Definitions›
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 ‹Admissibility on chain-finite types›
text ‹For chain-finite (easy) types every formula is admissible.›
lemma adm_chfin [simp]: "adm (P::'a::chfin ⇒ bool)"
by (rule admI, frule chfin, auto simp add: maxinch_is_thelub)
subsection ‹Admissibility of special formulae and propagation›
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 ‹Admissibility for disjunction is hard to prove. It requires 2 lemmas.›
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 -
def f ≡ "λi. LEAST j. i ≤ j ∧ P (Y j)"
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 ‹admissibility and continuity›
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 \<notsqsubseteq> u)"
by (rule admI, simp add: cont2contlubE ch2ch_cont lub_below_iff)
subsection ‹Compactness›
definition
compact :: "'a::cpo ⇒ bool" where
"compact k = adm (λx. k \<notsqsubseteq> x)"
lemma compactI: "adm (λx. k \<notsqsubseteq> x) ⟹ compact k"
unfolding compact_def .
lemma compactD: "compact k ⟹ adm (λx. k \<notsqsubseteq> 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::'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 ‹admissibility and compactness›
lemma adm_compact_not_below [simp]:
"⟦compact k; cont (λx. t x)⟧ ⟹ adm (λx. k \<notsqsubseteq> 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 ‹Any upward-closed predicate is admissible.›
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