Author:     Franz Regensburger and Brian Huffman
*)

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"

lemma admD: "adm P  chain Y  (i. P (Y i))  P (i. Y i)"

lemma admD2: "adm (λx. ¬ P x)  chain Y  P (i. Y i)  i. P (Y i)"

text ‹For chain-finite (easy) types every formula is admissible.›

for P :: "'a::chfin  bool"

subsection ‹Admissibility of special formulae and propagation›

lemma adm_ball [simp]: "(y. y  A  adm (λx. P x y))  adm (λx. yA. P x y)"

text ‹Admissibility for disjunction is hard to prove. It requires 2 lemmas.›

assumes chain: "chain Y"
assumes P: "i. ji. 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)
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)"
qed

lemma adm_disj_lemma2: "n::nat. P n  Q n  (i. ji. P j)  (i. ji. Q j)"
apply (erule contrapos_pp)
apply (clarsimp, rename_tac a b)
apply (rule_tac x="max a b" in exI)
apply simp
done

apply (erule (2) adm_disj_lemma1 [THEN disjI1])
apply (erule (2) adm_disj_lemma1 [THEN disjI2])
done

lemma adm_below [simp]: "cont (λx. u x)  cont (λx. v x)  adm (λx. u x  v x)"

lemma adm_eq [simp]: "cont (λx. u x)  cont (λx. v x)  adm (λx. u x = v x)"

lemma adm_not_below [simp]: "cont (λx. t x)  adm (λx. t x \<notsqsubseteq> u)"

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"

lemma compactD2: "compact x  chain Y  x  (i. Y i)  i. x  Y i"

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"

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

"compact k  cont (λx. t x)  adm (λx. k \<notsqsubseteq> t x)"

lemma adm_neq_compact [simp]: "compact k  cont (λx. t x)  adm (λx. t x  k)"

lemma adm_compact_neq [simp]: "compact k  cont (λx. t x)  adm (λx. k  t x)"

lemma compact_bottom [simp, intro]: "compact "
by (rule compactI) simp

text ‹Any upward-closed predicate is admissible.›