Theory Adm

(*  Title:      HOL/HOLCF/Adm.thy
    Author:     Franz Regensburger and Brian Huffman
*)

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"
  for 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 -
  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 ‹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"
  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 ‹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