src/HOL/HOLCF/Adm.thy
changeset 40774 0437dbc127b3
parent 40623 dafba3a1dc5b
child 41182 717404c7d59a
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/HOLCF/Adm.thy	Sat Nov 27 16:08:10 2010 -0800
     1.3 @@ -0,0 +1,193 @@
     1.4 +(*  Title:      HOLCF/Adm.thy
     1.5 +    Author:     Franz Regensburger and Brian Huffman
     1.6 +*)
     1.7 +
     1.8 +header {* Admissibility and compactness *}
     1.9 +
    1.10 +theory Adm
    1.11 +imports Cont
    1.12 +begin
    1.13 +
    1.14 +default_sort cpo
    1.15 +
    1.16 +subsection {* Definitions *}
    1.17 +
    1.18 +definition
    1.19 +  adm :: "('a::cpo \<Rightarrow> bool) \<Rightarrow> bool" where
    1.20 +  "adm P = (\<forall>Y. chain Y \<longrightarrow> (\<forall>i. P (Y i)) \<longrightarrow> P (\<Squnion>i. Y i))"
    1.21 +
    1.22 +lemma admI:
    1.23 +   "(\<And>Y. \<lbrakk>chain Y; \<forall>i. P (Y i)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)) \<Longrightarrow> adm P"
    1.24 +unfolding adm_def by fast
    1.25 +
    1.26 +lemma admD: "\<lbrakk>adm P; chain Y; \<And>i. P (Y i)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)"
    1.27 +unfolding adm_def by fast
    1.28 +
    1.29 +lemma admD2: "\<lbrakk>adm (\<lambda>x. \<not> P x); chain Y; P (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. P (Y i)"
    1.30 +unfolding adm_def by fast
    1.31 +
    1.32 +lemma triv_admI: "\<forall>x. P x \<Longrightarrow> adm P"
    1.33 +by (rule admI, erule spec)
    1.34 +
    1.35 +subsection {* Admissibility on chain-finite types *}
    1.36 +
    1.37 +text {* For chain-finite (easy) types every formula is admissible. *}
    1.38 +
    1.39 +lemma adm_chfin [simp]: "adm (P::'a::chfin \<Rightarrow> bool)"
    1.40 +by (rule admI, frule chfin, auto simp add: maxinch_is_thelub)
    1.41 +
    1.42 +subsection {* Admissibility of special formulae and propagation *}
    1.43 +
    1.44 +lemma adm_const [simp]: "adm (\<lambda>x. t)"
    1.45 +by (rule admI, simp)
    1.46 +
    1.47 +lemma adm_conj [simp]:
    1.48 +  "\<lbrakk>adm (\<lambda>x. P x); adm (\<lambda>x. Q x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<and> Q x)"
    1.49 +by (fast intro: admI elim: admD)
    1.50 +
    1.51 +lemma adm_all [simp]:
    1.52 +  "(\<And>y. adm (\<lambda>x. P x y)) \<Longrightarrow> adm (\<lambda>x. \<forall>y. P x y)"
    1.53 +by (fast intro: admI elim: admD)
    1.54 +
    1.55 +lemma adm_ball [simp]:
    1.56 +  "(\<And>y. y \<in> A \<Longrightarrow> adm (\<lambda>x. P x y)) \<Longrightarrow> adm (\<lambda>x. \<forall>y\<in>A. P x y)"
    1.57 +by (fast intro: admI elim: admD)
    1.58 +
    1.59 +text {* Admissibility for disjunction is hard to prove. It requires 2 lemmas. *}
    1.60 +
    1.61 +lemma adm_disj_lemma1:
    1.62 +  assumes adm: "adm P"
    1.63 +  assumes chain: "chain Y"
    1.64 +  assumes P: "\<forall>i. \<exists>j\<ge>i. P (Y j)"
    1.65 +  shows "P (\<Squnion>i. Y i)"
    1.66 +proof -
    1.67 +  def f \<equiv> "\<lambda>i. LEAST j. i \<le> j \<and> P (Y j)"
    1.68 +  have chain': "chain (\<lambda>i. Y (f i))"
    1.69 +    unfolding f_def
    1.70 +    apply (rule chainI)
    1.71 +    apply (rule chain_mono [OF chain])
    1.72 +    apply (rule Least_le)
    1.73 +    apply (rule LeastI2_ex)
    1.74 +    apply (simp_all add: P)
    1.75 +    done
    1.76 +  have f1: "\<And>i. i \<le> f i" and f2: "\<And>i. P (Y (f i))"
    1.77 +    using LeastI_ex [OF P [rule_format]] by (simp_all add: f_def)
    1.78 +  have lub_eq: "(\<Squnion>i. Y i) = (\<Squnion>i. Y (f i))"
    1.79 +    apply (rule below_antisym)
    1.80 +    apply (rule lub_mono [OF chain chain'])
    1.81 +    apply (rule chain_mono [OF chain f1])
    1.82 +    apply (rule lub_range_mono [OF _ chain chain'])
    1.83 +    apply clarsimp
    1.84 +    done
    1.85 +  show "P (\<Squnion>i. Y i)"
    1.86 +    unfolding lub_eq using adm chain' f2 by (rule admD)
    1.87 +qed
    1.88 +
    1.89 +lemma adm_disj_lemma2:
    1.90 +  "\<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)"
    1.91 +apply (erule contrapos_pp)
    1.92 +apply (clarsimp, rename_tac a b)
    1.93 +apply (rule_tac x="max a b" in exI)
    1.94 +apply simp
    1.95 +done
    1.96 +
    1.97 +lemma adm_disj [simp]:
    1.98 +  "\<lbrakk>adm (\<lambda>x. P x); adm (\<lambda>x. Q x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<or> Q x)"
    1.99 +apply (rule admI)
   1.100 +apply (erule adm_disj_lemma2 [THEN disjE])
   1.101 +apply (erule (2) adm_disj_lemma1 [THEN disjI1])
   1.102 +apply (erule (2) adm_disj_lemma1 [THEN disjI2])
   1.103 +done
   1.104 +
   1.105 +lemma adm_imp [simp]:
   1.106 +  "\<lbrakk>adm (\<lambda>x. \<not> P x); adm (\<lambda>x. Q x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<longrightarrow> Q x)"
   1.107 +by (subst imp_conv_disj, rule adm_disj)
   1.108 +
   1.109 +lemma adm_iff [simp]:
   1.110 +  "\<lbrakk>adm (\<lambda>x. P x \<longrightarrow> Q x); adm (\<lambda>x. Q x \<longrightarrow> P x)\<rbrakk>  
   1.111 +    \<Longrightarrow> adm (\<lambda>x. P x = Q x)"
   1.112 +by (subst iff_conv_conj_imp, rule adm_conj)
   1.113 +
   1.114 +text {* admissibility and continuity *}
   1.115 +
   1.116 +lemma adm_below [simp]:
   1.117 +  "\<lbrakk>cont (\<lambda>x. u x); cont (\<lambda>x. v x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x \<sqsubseteq> v x)"
   1.118 +by (simp add: adm_def cont2contlubE lub_mono ch2ch_cont)
   1.119 +
   1.120 +lemma adm_eq [simp]:
   1.121 +  "\<lbrakk>cont (\<lambda>x. u x); cont (\<lambda>x. v x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x = v x)"
   1.122 +by (simp add: po_eq_conv)
   1.123 +
   1.124 +lemma adm_subst: "\<lbrakk>cont (\<lambda>x. t x); adm P\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P (t x))"
   1.125 +by (simp add: adm_def cont2contlubE ch2ch_cont)
   1.126 +
   1.127 +lemma adm_not_below [simp]: "cont (\<lambda>x. t x) \<Longrightarrow> adm (\<lambda>x. \<not> t x \<sqsubseteq> u)"
   1.128 +by (rule admI, simp add: cont2contlubE ch2ch_cont lub_below_iff)
   1.129 +
   1.130 +subsection {* Compactness *}
   1.131 +
   1.132 +definition
   1.133 +  compact :: "'a::cpo \<Rightarrow> bool" where
   1.134 +  "compact k = adm (\<lambda>x. \<not> k \<sqsubseteq> x)"
   1.135 +
   1.136 +lemma compactI: "adm (\<lambda>x. \<not> k \<sqsubseteq> x) \<Longrightarrow> compact k"
   1.137 +unfolding compact_def .
   1.138 +
   1.139 +lemma compactD: "compact k \<Longrightarrow> adm (\<lambda>x. \<not> k \<sqsubseteq> x)"
   1.140 +unfolding compact_def .
   1.141 +
   1.142 +lemma compactI2:
   1.143 +  "(\<And>Y. \<lbrakk>chain Y; x \<sqsubseteq> (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. x \<sqsubseteq> Y i) \<Longrightarrow> compact x"
   1.144 +unfolding compact_def adm_def by fast
   1.145 +
   1.146 +lemma compactD2:
   1.147 +  "\<lbrakk>compact x; chain Y; x \<sqsubseteq> (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. x \<sqsubseteq> Y i"
   1.148 +unfolding compact_def adm_def by fast
   1.149 +
   1.150 +lemma compact_below_lub_iff:
   1.151 +  "\<lbrakk>compact x; chain Y\<rbrakk> \<Longrightarrow> x \<sqsubseteq> (\<Squnion>i. Y i) \<longleftrightarrow> (\<exists>i. x \<sqsubseteq> Y i)"
   1.152 +by (fast intro: compactD2 elim: below_lub)
   1.153 +
   1.154 +lemma compact_chfin [simp]: "compact (x::'a::chfin)"
   1.155 +by (rule compactI [OF adm_chfin])
   1.156 +
   1.157 +lemma compact_imp_max_in_chain:
   1.158 +  "\<lbrakk>chain Y; compact (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. max_in_chain i Y"
   1.159 +apply (drule (1) compactD2, simp)
   1.160 +apply (erule exE, rule_tac x=i in exI)
   1.161 +apply (rule max_in_chainI)
   1.162 +apply (rule below_antisym)
   1.163 +apply (erule (1) chain_mono)
   1.164 +apply (erule (1) below_trans [OF is_ub_thelub])
   1.165 +done
   1.166 +
   1.167 +text {* admissibility and compactness *}
   1.168 +
   1.169 +lemma adm_compact_not_below [simp]:
   1.170 +  "\<lbrakk>compact k; cont (\<lambda>x. t x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. \<not> k \<sqsubseteq> t x)"
   1.171 +unfolding compact_def by (rule adm_subst)
   1.172 +
   1.173 +lemma adm_neq_compact [simp]:
   1.174 +  "\<lbrakk>compact k; cont (\<lambda>x. t x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. t x \<noteq> k)"
   1.175 +by (simp add: po_eq_conv)
   1.176 +
   1.177 +lemma adm_compact_neq [simp]:
   1.178 +  "\<lbrakk>compact k; cont (\<lambda>x. t x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. k \<noteq> t x)"
   1.179 +by (simp add: po_eq_conv)
   1.180 +
   1.181 +lemma compact_UU [simp, intro]: "compact \<bottom>"
   1.182 +by (rule compactI, simp)
   1.183 +
   1.184 +text {* Any upward-closed predicate is admissible. *}
   1.185 +
   1.186 +lemma adm_upward:
   1.187 +  assumes P: "\<And>x y. \<lbrakk>P x; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> P y"
   1.188 +  shows "adm P"
   1.189 +by (rule admI, drule spec, erule P, erule is_ub_thelub)
   1.190 +
   1.191 +lemmas adm_lemmas =
   1.192 +  adm_const adm_conj adm_all adm_ball adm_disj adm_imp adm_iff
   1.193 +  adm_below adm_eq adm_not_below
   1.194 +  adm_compact_not_below adm_compact_neq adm_neq_compact
   1.195 +
   1.196 +end