1(* Title: HOL/HOLCF/Adm.thy 2 Author: Franz Regensburger and Brian Huffman 3*) 4 5section \<open>Admissibility and compactness\<close> 6 7theory Adm 8 imports Cont 9begin 10 11default_sort cpo 12 13subsection \<open>Definitions\<close> 14 15definition adm :: "('a::cpo \<Rightarrow> bool) \<Rightarrow> bool" 16 where "adm P \<longleftrightarrow> (\<forall>Y. chain Y \<longrightarrow> (\<forall>i. P (Y i)) \<longrightarrow> P (\<Squnion>i. Y i))" 17 18lemma admI: "(\<And>Y. \<lbrakk>chain Y; \<forall>i. P (Y i)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)) \<Longrightarrow> adm P" 19 unfolding adm_def by fast 20 21lemma admD: "adm P \<Longrightarrow> chain Y \<Longrightarrow> (\<And>i. P (Y i)) \<Longrightarrow> P (\<Squnion>i. Y i)" 22 unfolding adm_def by fast 23 24lemma admD2: "adm (\<lambda>x. \<not> P x) \<Longrightarrow> chain Y \<Longrightarrow> P (\<Squnion>i. Y i) \<Longrightarrow> \<exists>i. P (Y i)" 25 unfolding adm_def by fast 26 27lemma triv_admI: "\<forall>x. P x \<Longrightarrow> adm P" 28 by (rule admI) (erule spec) 29 30 31subsection \<open>Admissibility on chain-finite types\<close> 32 33text \<open>For chain-finite (easy) types every formula is admissible.\<close> 34 35lemma adm_chfin [simp]: "adm P" 36 for P :: "'a::chfin \<Rightarrow> bool" 37 by (rule admI, frule chfin, auto simp add: maxinch_is_thelub) 38 39 40subsection \<open>Admissibility of special formulae and propagation\<close> 41 42lemma adm_const [simp]: "adm (\<lambda>x. t)" 43 by (rule admI, simp) 44 45lemma adm_conj [simp]: "adm (\<lambda>x. P x) \<Longrightarrow> adm (\<lambda>x. Q x) \<Longrightarrow> adm (\<lambda>x. P x \<and> Q x)" 46 by (fast intro: admI elim: admD) 47 48lemma adm_all [simp]: "(\<And>y. adm (\<lambda>x. P x y)) \<Longrightarrow> adm (\<lambda>x. \<forall>y. P x y)" 49 by (fast intro: admI elim: admD) 50 51lemma adm_ball [simp]: "(\<And>y. y \<in> A \<Longrightarrow> adm (\<lambda>x. P x y)) \<Longrightarrow> adm (\<lambda>x. \<forall>y\<in>A. P x y)" 52 by (fast intro: admI elim: admD) 53 54text \<open>Admissibility for disjunction is hard to prove. It requires 2 lemmas.\<close> 55 56lemma adm_disj_lemma1: 57 assumes adm: "adm P" 58 assumes chain: "chain Y" 59 assumes P: "\<forall>i. \<exists>j\<ge>i. P (Y j)" 60 shows "P (\<Squnion>i. Y i)" 61proof - 62 define f where "f i = (LEAST j. i \<le> j \<and> P (Y j))" for i 63 have chain': "chain (\<lambda>i. Y (f i))" 64 unfolding f_def 65 apply (rule chainI) 66 apply (rule chain_mono [OF chain]) 67 apply (rule Least_le) 68 apply (rule LeastI2_ex) 69 apply (simp_all add: P) 70 done 71 have f1: "\<And>i. i \<le> f i" and f2: "\<And>i. P (Y (f i))" 72 using LeastI_ex [OF P [rule_format]] by (simp_all add: f_def) 73 have lub_eq: "(\<Squnion>i. Y i) = (\<Squnion>i. Y (f i))" 74 apply (rule below_antisym) 75 apply (rule lub_mono [OF chain chain']) 76 apply (rule chain_mono [OF chain f1]) 77 apply (rule lub_range_mono [OF _ chain chain']) 78 apply clarsimp 79 done 80 show "P (\<Squnion>i. Y i)" 81 unfolding lub_eq using adm chain' f2 by (rule admD) 82qed 83 84lemma adm_disj_lemma2: "\<forall>n::nat. P n \<or> Q n \<Longrightarrow> (\<forall>i. \<exists>j\<ge>i. P j) \<or> (\<forall>i. \<exists>j\<ge>i. Q j)" 85 apply (erule contrapos_pp) 86 apply (clarsimp, rename_tac a b) 87 apply (rule_tac x="max a b" in exI) 88 apply simp 89 done 90 91lemma adm_disj [simp]: "adm (\<lambda>x. P x) \<Longrightarrow> adm (\<lambda>x. Q x) \<Longrightarrow> adm (\<lambda>x. P x \<or> Q x)" 92 apply (rule admI) 93 apply (erule adm_disj_lemma2 [THEN disjE]) 94 apply (erule (2) adm_disj_lemma1 [THEN disjI1]) 95 apply (erule (2) adm_disj_lemma1 [THEN disjI2]) 96 done 97 98lemma adm_imp [simp]: "adm (\<lambda>x. \<not> P x) \<Longrightarrow> adm (\<lambda>x. Q x) \<Longrightarrow> adm (\<lambda>x. P x \<longrightarrow> Q x)" 99 by (subst imp_conv_disj) (rule adm_disj) 100 101lemma adm_iff [simp]: "adm (\<lambda>x. P x \<longrightarrow> Q x) \<Longrightarrow> adm (\<lambda>x. Q x \<longrightarrow> P x) \<Longrightarrow> adm (\<lambda>x. P x \<longleftrightarrow> Q x)" 102 by (subst iff_conv_conj_imp) (rule adm_conj) 103 104text \<open>admissibility and continuity\<close> 105 106lemma adm_below [simp]: "cont (\<lambda>x. u x) \<Longrightarrow> cont (\<lambda>x. v x) \<Longrightarrow> adm (\<lambda>x. u x \<sqsubseteq> v x)" 107 by (simp add: adm_def cont2contlubE lub_mono ch2ch_cont) 108 109lemma adm_eq [simp]: "cont (\<lambda>x. u x) \<Longrightarrow> cont (\<lambda>x. v x) \<Longrightarrow> adm (\<lambda>x. u x = v x)" 110 by (simp add: po_eq_conv) 111 112lemma adm_subst: "cont (\<lambda>x. t x) \<Longrightarrow> adm P \<Longrightarrow> adm (\<lambda>x. P (t x))" 113 by (simp add: adm_def cont2contlubE ch2ch_cont) 114 115lemma adm_not_below [simp]: "cont (\<lambda>x. t x) \<Longrightarrow> adm (\<lambda>x. t x \<notsqsubseteq> u)" 116 by (rule admI) (simp add: cont2contlubE ch2ch_cont lub_below_iff) 117 118 119subsection \<open>Compactness\<close> 120 121definition compact :: "'a::cpo \<Rightarrow> bool" 122 where "compact k = adm (\<lambda>x. k \<notsqsubseteq> x)" 123 124lemma compactI: "adm (\<lambda>x. k \<notsqsubseteq> x) \<Longrightarrow> compact k" 125 unfolding compact_def . 126 127lemma compactD: "compact k \<Longrightarrow> adm (\<lambda>x. k \<notsqsubseteq> x)" 128 unfolding compact_def . 129 130lemma compactI2: "(\<And>Y. \<lbrakk>chain Y; x \<sqsubseteq> (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. x \<sqsubseteq> Y i) \<Longrightarrow> compact x" 131 unfolding compact_def adm_def by fast 132 133lemma compactD2: "compact x \<Longrightarrow> chain Y \<Longrightarrow> x \<sqsubseteq> (\<Squnion>i. Y i) \<Longrightarrow> \<exists>i. x \<sqsubseteq> Y i" 134 unfolding compact_def adm_def by fast 135 136lemma compact_below_lub_iff: "compact x \<Longrightarrow> chain Y \<Longrightarrow> x \<sqsubseteq> (\<Squnion>i. Y i) \<longleftrightarrow> (\<exists>i. x \<sqsubseteq> Y i)" 137 by (fast intro: compactD2 elim: below_lub) 138 139lemma compact_chfin [simp]: "compact x" 140 for x :: "'a::chfin" 141 by (rule compactI [OF adm_chfin]) 142 143lemma compact_imp_max_in_chain: "chain Y \<Longrightarrow> compact (\<Squnion>i. Y i) \<Longrightarrow> \<exists>i. max_in_chain i Y" 144 apply (drule (1) compactD2, simp) 145 apply (erule exE, rule_tac x=i in exI) 146 apply (rule max_in_chainI) 147 apply (rule below_antisym) 148 apply (erule (1) chain_mono) 149 apply (erule (1) below_trans [OF is_ub_thelub]) 150 done 151 152text \<open>admissibility and compactness\<close> 153 154lemma adm_compact_not_below [simp]: 155 "compact k \<Longrightarrow> cont (\<lambda>x. t x) \<Longrightarrow> adm (\<lambda>x. k \<notsqsubseteq> t x)" 156 unfolding compact_def by (rule adm_subst) 157 158lemma adm_neq_compact [simp]: "compact k \<Longrightarrow> cont (\<lambda>x. t x) \<Longrightarrow> adm (\<lambda>x. t x \<noteq> k)" 159 by (simp add: po_eq_conv) 160 161lemma adm_compact_neq [simp]: "compact k \<Longrightarrow> cont (\<lambda>x. t x) \<Longrightarrow> adm (\<lambda>x. k \<noteq> t x)" 162 by (simp add: po_eq_conv) 163 164lemma compact_bottom [simp, intro]: "compact \<bottom>" 165 by (rule compactI) simp 166 167text \<open>Any upward-closed predicate is admissible.\<close> 168 169lemma adm_upward: 170 assumes P: "\<And>x y. \<lbrakk>P x; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> P y" 171 shows "adm P" 172 by (rule admI, drule spec, erule P, erule is_ub_thelub) 173 174lemmas adm_lemmas = 175 adm_const adm_conj adm_all adm_ball adm_disj adm_imp adm_iff 176 adm_below adm_eq adm_not_below 177 adm_compact_not_below adm_compact_neq adm_neq_compact 178 179end 180