(* 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
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
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
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)