# Theory Adm

Up to index of Isabelle/HOLCF

theory Adm
imports Cont
begin

    (*  Title:      HOLCF/Adm.thy
        ID:         $Id: Adm.thy,v 1.9 2005/09/22 17:06:34 huffman Exp $
        Author:     Franz Regensburger
    *)

    header {* Admissibility *}

    theory Adm
    imports Cont
    begin

    defaultsort cpo

    subsection {* Definitions *}

    constdefs
      adm :: "('a::cpo => bool) => bool"
      "adm P ≡ ∀Y. chain Y --> (∀i. P (Y i)) --> P (\<Squnion>i. Y i)"

    lemma admI:
       "(!!Y. [|chain Y; ∀i. P (Y i)|] ==> P (\<Squnion>i. Y i)) ==> adm P"
    apply (unfold adm_def)
    apply blast
    done

    lemma triv_admI: "∀x. P x ==> adm P"
    apply (rule admI)
    apply (erule spec)
    done

    lemma admD: "[|adm P; chain Y; ∀i. P (Y i)|] ==> P (\<Squnion>i. Y i)"
    apply (unfold adm_def)
    apply blast
    done

    text {* improved admissibility introduction *}

    lemma admI2:
      "(!!Y. [|chain Y; ∀i. P (Y i); ∀i. ∃j>i. Y i ≠ Y j ∧ Y i \<sqsubseteq> Y j|]
        ==> P (\<Squnion>i. Y i)) ==> adm P"
    apply (rule admI)
    apply (erule (1) increasing_chain_adm_lemma)
    apply fast
    done

    subsection {* Admissibility on chain-finite types *}

    text {* for chain-finite (easy) types every formula is admissible *}

    lemma adm_max_in_chain:
      "∀Y. chain (Y::nat => 'a) --> (∃n. max_in_chain n Y)
        ==> adm (P::'a => bool)"
    apply (unfold adm_def)
    apply (intro strip)
    apply (drule spec)
    apply (drule mp)
    apply assumption
    apply (erule exE)
    apply (simp add: maxinch_is_thelub)
    done

    lemmas adm_chfin = chfin [THEN adm_max_in_chain, standard]

    subsection {* Admissibility of special formulae and propagation *}

    lemma adm_less: "[|cont u; cont v|] ==> adm (λx. u x \<sqsubseteq> v x)"
    apply (rule admI)
    apply (simp add: cont2contlubE)
    apply (rule lub_mono)
    apply (erule (1) ch2ch_cont)
    apply (erule (1) ch2ch_cont)
    apply assumption
    done

    lemma adm_conj: "[|adm P; adm Q|] ==> adm (λx. P x ∧ Q x)"
    by (fast elim: admD intro: admI)

    lemma adm_not_free: "adm (λx. t)"
    by (rule admI, simp)

    lemma adm_not_less: "cont t ==> adm (λx. ¬ t x \<sqsubseteq> u)"
    apply (rule admI)
    apply (drule_tac x=0 in spec)
    apply (erule contrapos_nn)
    apply (rule trans_less)
    prefer 2 apply (assumption)
    apply (erule cont2mono [THEN monofun_fun_arg])
    apply (erule is_ub_thelub)
    done

    lemma adm_all: "∀y. adm (P y) ==> adm (λx. ∀y. P y x)"
    by (fast intro: admI elim: admD)

    lemmas adm_all2 = adm_all [rule_format]

    lemma adm_ball: "∀y∈A. adm (P y) ==> adm (λx. ∀y∈A. P y x)"
    by (fast intro: admI elim: admD)

    lemmas adm_ball2 = adm_ball [rule_format]

    lemma adm_subst: "[|cont t; adm P|] ==> adm (λx. P (t x))"
    apply (rule admI)
    apply (simp add: cont2contlubE)
    apply (erule admD)
    apply (erule (1) ch2ch_cont)
    apply assumption
    done

    lemma adm_UU_not_less: "adm (λx. ¬ ⊥ \<sqsubseteq> t x)"
    by (simp add: adm_not_free)

    lemma adm_not_UU: "cont t ==> adm (λx. ¬ t x = ⊥)"
    by (simp add: eq_UU_iff adm_not_less)

    lemma adm_eq: "[|cont u; cont v|] ==> adm (λx. u x = v x)"
    by (simp add: po_eq_conv adm_conj adm_less)

    text {* admissibility for disjunction is hard to prove. It takes 7 Lemmas *}

    lemma adm_disj_lemma1:
      "∀n::nat. P n ∨ Q n ==> (∀i. ∃j≥i. P j) ∨ (∀i. ∃j≥i. Q j)"
    apply (erule contrapos_pp)
    apply clarsimp
    apply (rule exI)
    apply (rule conjI)
    apply (drule spec, erule mp)
    apply (rule le_maxI1)
    apply (drule spec, erule mp)
    apply (rule le_maxI2)
    done

    lemma adm_disj_lemma2:
      "[|adm P; ∃X. chain X ∧ (∀n. P (X n)) ∧ (\<Squnion>i. Y i) = (\<Squnion>i. X i)|]
        ==> P (\<Squnion>i. Y i)"
    by (force elim: admD)

    lemma adm_disj_lemma3:
      "[|chain (Y::nat => 'a::cpo); ∀i. ∃j≥i. P (Y j)|]
        ==> chain (λm. Y (LEAST j. m ≤ j ∧ P (Y j)))"
    apply (rule chainI)
    apply (erule chain_mono3)
    apply (rule Least_le)
    apply (drule_tac x="Suc i" in spec)
    apply (rule conjI)
    apply (rule Suc_leD)
    apply (erule LeastI_ex [THEN conjunct1])
    apply (erule LeastI_ex [THEN conjunct2])
    done

    lemma adm_disj_lemma4:
      "[|∀i. ∃j≥i. P (Y j)|] ==> ∀m. P (Y (LEAST j::nat. m ≤ j ∧ P (Y j)))"
    apply (rule allI)
    apply (drule_tac x=m in spec)
    apply (erule LeastI_ex [THEN conjunct2])
    done

    lemma adm_disj_lemma5:
      "[|chain (Y::nat => 'a::cpo); ∀i. ∃j≥i. P (Y j)|] ==>
        (\<Squnion>m. Y m) = (\<Squnion>m. Y (LEAST j. m ≤ j ∧ P (Y j)))"
     apply (rule antisym_less)
      apply (rule lub_mono)
        apply assumption
       apply (erule (1) adm_disj_lemma3)
      apply (rule allI)
      apply (erule chain_mono3)
      apply (drule_tac x=k in spec)
      apply (erule LeastI_ex [THEN conjunct1])
     apply (rule lub_mono3)
       apply (erule (1) adm_disj_lemma3)
      apply assumption
     apply (rule allI)
     apply (rule exI)
     apply (rule refl_less)
    done

    lemma adm_disj_lemma6:
      "[|chain (Y::nat => 'a::cpo); ∀i. ∃j≥i. P(Y j)|] ==>
        ∃X. chain X ∧ (∀n. P (X n)) ∧ (\<Squnion>i. Y i) = (\<Squnion>i. X i)"
    apply (rule_tac x = "λm. Y (LEAST j. m ≤ j ∧ P (Y j))" in exI)
    apply (fast intro!: adm_disj_lemma3 adm_disj_lemma4 adm_disj_lemma5)
    done

    lemma adm_disj_lemma7:
      "[|adm P; chain Y; ∀i. ∃j≥i. P (Y j)|] ==> P (\<Squnion>i. Y i)"
    apply (erule adm_disj_lemma2)
    apply (erule (1) adm_disj_lemma6)
    done

    lemma adm_disj: "[|adm P; adm Q|] ==> adm (λx. P x ∨ Q x)"
    apply (rule admI)
    apply (erule adm_disj_lemma1 [THEN disjE])
    apply (rule disjI1)
    apply (erule (2) adm_disj_lemma7)
    apply (rule disjI2)
    apply (erule (2) adm_disj_lemma7)
    done

    lemma adm_imp: "[|adm (λx. ¬ P x); adm Q|] ==> adm (λx. P x --> Q x)"
    by (subst imp_conv_disj, rule adm_disj)

    lemma adm_iff:
      "[|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)

    lemma adm_not_conj:
      "[|adm (λx. ¬ P x); adm (λx. ¬ Q x)|] ==> adm (λx. ¬ (P x ∧ Q x))"
    by (subst de_Morgan_conj, rule adm_disj)

    lemmas adm_lemmas =
      adm_less adm_conj adm_not_free adm_imp adm_disj adm_eq adm_not_UU
      adm_UU_not_less adm_all2 adm_not_less adm_not_conj adm_iff

    declare adm_lemmas [simp]

    (* legacy ML bindings *)
    ML
    {*
    val adm_def = thm "adm_def";
    val admI = thm "admI";
    val triv_admI = thm "triv_admI";
    val admD = thm "admD";
    val adm_max_in_chain = thm "adm_max_in_chain";
    val adm_chfin = thm "adm_chfin";
    val admI2 = thm "admI2";
    val adm_less = thm "adm_less";
    val adm_conj = thm "adm_conj";
    val adm_not_free = thm "adm_not_free";
    val adm_not_less = thm "adm_not_less";
    val adm_all = thm "adm_all";
    val adm_all2 = thm "adm_all2";
    val adm_ball = thm "adm_ball";
    val adm_ball2 = thm "adm_ball2";
    val adm_subst = thm "adm_subst";
    val adm_UU_not_less = thm "adm_UU_not_less";
    val adm_not_UU = thm "adm_not_UU";
    val adm_eq = thm "adm_eq";
    val adm_disj_lemma1 = thm "adm_disj_lemma1";
    val adm_disj_lemma2 = thm "adm_disj_lemma2";
    val adm_disj_lemma3 = thm "adm_disj_lemma3";
    val adm_disj_lemma4 = thm "adm_disj_lemma4";
    val adm_disj_lemma5 = thm "adm_disj_lemma5";
    val adm_disj_lemma6 = thm "adm_disj_lemma6";
    val adm_disj_lemma7 = thm "adm_disj_lemma7";
    val adm_disj = thm "adm_disj";
    val adm_imp = thm "adm_imp";
    val adm_iff = thm "adm_iff";
    val adm_not_conj = thm "adm_not_conj";
    val adm_lemmas = thms "adm_lemmas";
    *}

    end

### Definitions

lemma admI:

      (!!Y. [| chain Y; ∀i. P (Y i) |] ==> P (lub (range Y))) ==> adm P

lemma triv_admI:

      ∀x. P x ==> adm P

lemma admD:

      [| adm P; chain Y; ∀i. P (Y i) |] ==> P (lub (range Y))

lemma admI2:

      (!!Y. [| chain Y; ∀i. P (Y i); ∀i. ∃j. i < j ∧ Y i ≠ Y j ∧ Y i << Y j |]
            ==> P (lub (range Y)))
      ==> adm P

### Admissibility on chain-finite types

lemma adm_max_in_chain:

      ∀Y. chain Y --> (∃n. max_in_chain n Y) ==> adm P

lemmas adm_chfin:

      adm P

lemmas adm_chfin:

      adm P

### Admissibility of special formulae and propagation

lemma adm_less:

      [| cont u; cont v |] ==> adm (%x. u x << v x)

lemma adm_conj:

      [| adm P; adm Q |] ==> adm (%x. P x ∧ Q x)

lemma adm_not_free:

      adm (%x. t)

lemma adm_not_less:

      cont t ==> adm (%x. ¬ t x << u)

lemma adm_all:

      ∀y. adm (P y) ==> adm (%x. ∀y. P y x)

lemmas adm_all2:

      (!!y. adm (P y)) ==> adm (%x. ∀y. P y x)

lemmas adm_all2:

      (!!y. adm (P y)) ==> adm (%x. ∀y. P y x)

lemma adm_ball:

      ∀y∈A. adm (P y) ==> adm (%x. ∀y∈A. P y x)

lemmas adm_ball2:

      (!!y. y ∈ A ==> adm (P y)) ==> adm (%x. ∀y∈A. P y x)

lemmas adm_ball2:

      (!!y. y ∈ A ==> adm (P y)) ==> adm (%x. ∀y∈A. P y x)

lemma adm_subst:

      [| cont t; adm P |] ==> adm (%x. P (t x))

lemma adm_UU_not_less:

      adm (%x. ¬ UU << t x)

lemma adm_not_UU:

      cont t ==> adm (%x. t x ≠ UU)

lemma adm_eq:

      [| cont u; cont v |] ==> adm (%x. u x = v x)

lemma adm_disj_lemma1:

      ∀n. P n ∨ Q n ==> (∀i. ∃j. i ≤ j ∧ P j) ∨ (∀i. ∃j. i ≤ j ∧ Q j)

lemma adm_disj_lemma2:

      [| adm P; ∃X. chain X ∧ (∀n. P (X n)) ∧ lub (range Y) = lub (range X) |]
      ==> P (lub (range Y))

lemma adm_disj_lemma3:

      [| chain Y; ∀i. ∃j. i ≤ j ∧ P (Y j) |]
      ==> chain (%m. Y (LEAST j. m ≤ j ∧ P (Y j)))

lemma adm_disj_lemma4:

      ∀i. ∃j. i ≤ j ∧ P (Y j) ==> ∀m. P (Y (LEAST j. m ≤ j ∧ P (Y j)))

lemma adm_disj_lemma5:

      [| chain Y; ∀i. ∃j. i ≤ j ∧ P (Y j) |]
      ==> lub (range Y) = (LUB m. Y (LEAST j. m ≤ j ∧ P (Y j)))

lemma adm_disj_lemma6:

      [| chain Y; ∀i. ∃j. i ≤ j ∧ P (Y j) |]
      ==> ∃X. chain X ∧ (∀n. P (X n)) ∧ lub (range Y) = lub (range X)

lemma adm_disj_lemma7:

      [| adm P; chain Y; ∀i. ∃j. i ≤ j ∧ P (Y j) |] ==> P (lub (range Y))

lemma adm_disj:

      [| adm P; adm Q |] ==> adm (%x. P x ∨ Q x)

lemma adm_imp:

      [| adm (%x. ¬ P x); adm Q |] ==> adm (%x. P x --> Q x)

lemma adm_iff:

      [| adm (%x. P x --> Q x); adm (%x. Q x --> P x) |] ==> adm (%x. P x = Q x)

lemma adm_not_conj:

      [| adm (%x. ¬ P x); adm (%x. ¬ Q x) |] ==> adm (%x. ¬ (P x ∧ Q x))

lemmas adm_lemmas:

      [| cont u; cont v |] ==> adm (%x. u x << v x)

      [| adm P; adm Q |] ==> adm (%x. P x ∧ Q x)

      adm (%x. t)

      [| adm (%x. ¬ P x); adm Q |] ==> adm (%x. P x --> Q x)

      [| adm P; adm Q |] ==> adm (%x. P x ∨ Q x)

      [| cont u; cont v |] ==> adm (%x. u x = v x)

      cont t ==> adm (%x. t x ≠ UU)

      adm (%x. ¬ UU << t x)

      (!!y. adm (P y)) ==> adm (%x. ∀y. P y x)

      cont t ==> adm (%x. ¬ t x << u)

      [| adm (%x. ¬ P x); adm (%x. ¬ Q x) |] ==> adm (%x. ¬ (P x ∧ Q x))

      [| adm (%x. P x --> Q x); adm (%x. Q x --> P x) |] ==> adm (%x. P x = Q x)

lemmas adm_lemmas:

      [| cont u; cont v |] ==> adm (%x. u x << v x)

      [| adm P; adm Q |] ==> adm (%x. P x ∧ Q x)

      adm (%x. t)

      [| adm (%x. ¬ P x); adm Q |] ==> adm (%x. P x --> Q x)

      [| adm P; adm Q |] ==> adm (%x. P x ∨ Q x)

      [| cont u; cont v |] ==> adm (%x. u x = v x)

      cont t ==> adm (%x. t x ≠ UU)

      adm (%x. ¬ UU << t x)

      (!!y. adm (P y)) ==> adm (%x. ∀y. P y x)

      cont t ==> adm (%x. ¬ t x << u)

      [| adm (%x. ¬ P x); adm (%x. ¬ Q x) |] ==> adm (%x. ¬ (P x ∧ Q x))

      [| adm (%x. P x --> Q x); adm (%x. Q x --> P x) |] ==> adm (%x. P x = Q x)