cleaned up Adm.thy
authorhuffman
Tue Oct 12 07:46:44 2010 -0700 (2010-10-12)
changeset 40007bb04a995bbd3
parent 40006 116e94f9543b
child 40008 58ead6f77f8e
cleaned up Adm.thy
src/HOLCF/Adm.thy
     1.1 --- a/src/HOLCF/Adm.thy	Tue Oct 12 06:20:05 2010 -0700
     1.2 +++ b/src/HOLCF/Adm.thy	Tue Oct 12 07:46:44 2010 -0700
     1.3 @@ -48,52 +48,52 @@
     1.4  
     1.5  subsection {* Admissibility of special formulae and propagation *}
     1.6  
     1.7 -lemma adm_not_free: "adm (\<lambda>x. t)"
     1.8 +lemma adm_const [simp]: "adm (\<lambda>x. t)"
     1.9  by (rule admI, simp)
    1.10  
    1.11 -lemma adm_conj: "\<lbrakk>adm P; adm Q\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<and> Q x)"
    1.12 +lemma adm_conj [simp]:
    1.13 +  "\<lbrakk>adm (\<lambda>x. P x); adm (\<lambda>x. Q x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<and> Q x)"
    1.14  by (fast intro: admI elim: admD)
    1.15  
    1.16 -lemma adm_all: "(\<And>y. adm (\<lambda>x. P x y)) \<Longrightarrow> adm (\<lambda>x. \<forall>y. P x y)"
    1.17 +lemma adm_all [simp]:
    1.18 +  "(\<And>y. adm (\<lambda>x. P x y)) \<Longrightarrow> adm (\<lambda>x. \<forall>y. P x y)"
    1.19  by (fast intro: admI elim: admD)
    1.20  
    1.21 -lemma adm_ball: "(\<And>y. y \<in> A \<Longrightarrow> adm (\<lambda>x. P x y)) \<Longrightarrow> adm (\<lambda>x. \<forall>y\<in>A. P x y)"
    1.22 +lemma adm_ball [simp]:
    1.23 +  "(\<And>y. y \<in> A \<Longrightarrow> adm (\<lambda>x. P x y)) \<Longrightarrow> adm (\<lambda>x. \<forall>y\<in>A. P x y)"
    1.24  by (fast intro: admI elim: admD)
    1.25  
    1.26 -text {* Admissibility for disjunction is hard to prove. It takes 5 Lemmas *}
    1.27 -
    1.28 -lemma adm_disj_lemma1: 
    1.29 -  "\<lbrakk>chain (Y::nat \<Rightarrow> 'a::cpo); \<forall>i. \<exists>j\<ge>i. P (Y j)\<rbrakk>
    1.30 -    \<Longrightarrow> chain (\<lambda>i. Y (LEAST j. i \<le> j \<and> P (Y j)))"
    1.31 -apply (rule chainI)
    1.32 -apply (erule chain_mono)
    1.33 -apply (rule Least_le)
    1.34 -apply (rule LeastI2_ex)
    1.35 -apply simp_all
    1.36 -done
    1.37 -
    1.38 -lemmas adm_disj_lemma2 = LeastI_ex [of "\<lambda>j. i \<le> j \<and> P (Y j)", standard]
    1.39 +text {* Admissibility for disjunction is hard to prove. It requires 2 lemmas. *}
    1.40  
    1.41 -lemma adm_disj_lemma3: 
    1.42 -  "\<lbrakk>chain (Y::nat \<Rightarrow> 'a::cpo); \<forall>i. \<exists>j\<ge>i. P (Y j)\<rbrakk> \<Longrightarrow> 
    1.43 -    (\<Squnion>i. Y i) = (\<Squnion>i. Y (LEAST j. i \<le> j \<and> P (Y j)))"
    1.44 - apply (frule (1) adm_disj_lemma1)
    1.45 - apply (rule below_antisym)
    1.46 -  apply (rule lub_mono, assumption+)
    1.47 -  apply (erule chain_mono)
    1.48 -  apply (simp add: adm_disj_lemma2)
    1.49 - apply (rule lub_range_mono, fast, assumption+)
    1.50 -done
    1.51 +lemma adm_disj_lemma1:
    1.52 +  assumes adm: "adm P"
    1.53 +  assumes chain: "chain Y"
    1.54 +  assumes P: "\<forall>i. \<exists>j\<ge>i. P (Y j)"
    1.55 +  shows "P (\<Squnion>i. Y i)"
    1.56 +proof -
    1.57 +  def f \<equiv> "\<lambda>i. LEAST j. i \<le> j \<and> P (Y j)"
    1.58 +  have chain': "chain (\<lambda>i. Y (f i))"
    1.59 +    unfolding f_def
    1.60 +    apply (rule chainI)
    1.61 +    apply (rule chain_mono [OF chain])
    1.62 +    apply (rule Least_le)
    1.63 +    apply (rule LeastI2_ex)
    1.64 +    apply (simp_all add: P)
    1.65 +    done
    1.66 +  have f1: "\<And>i. i \<le> f i" and f2: "\<And>i. P (Y (f i))"
    1.67 +    using LeastI_ex [OF P [rule_format]] by (simp_all add: f_def)
    1.68 +  have lub_eq: "(\<Squnion>i. Y i) = (\<Squnion>i. Y (f i))"
    1.69 +    apply (rule below_antisym)
    1.70 +    apply (rule lub_mono [OF chain chain'])
    1.71 +    apply (rule chain_mono [OF chain f1])
    1.72 +    apply (rule lub_range_mono [OF _ chain chain'])
    1.73 +    apply clarsimp
    1.74 +    done
    1.75 +  show "P (\<Squnion>i. Y i)"
    1.76 +    unfolding lub_eq using adm chain' f2 by (rule admD)
    1.77 +qed
    1.78  
    1.79 -lemma adm_disj_lemma4:
    1.80 -  "\<lbrakk>adm P; chain Y; \<forall>i. \<exists>j\<ge>i. P (Y j)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)"
    1.81 -apply (subst adm_disj_lemma3, assumption+)
    1.82 -apply (erule admD)
    1.83 -apply (simp add: adm_disj_lemma1)
    1.84 -apply (simp add: adm_disj_lemma2)
    1.85 -done
    1.86 -
    1.87 -lemma adm_disj_lemma5:
    1.88 +lemma adm_disj_lemma2:
    1.89    "\<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.90  apply (erule contrapos_pp)
    1.91  apply (clarsimp, rename_tac a b)
    1.92 @@ -101,28 +101,27 @@
    1.93  apply simp
    1.94  done
    1.95  
    1.96 -lemma adm_disj: "\<lbrakk>adm P; adm Q\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<or> Q x)"
    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_lemma5 [THEN disjE])
   1.101 -apply (erule (2) adm_disj_lemma4 [THEN disjI1])
   1.102 -apply (erule (2) adm_disj_lemma4 [THEN disjI2])
   1.103 +apply (erule adm_disj_lemma2 [THEN disjE])
   1.104 +apply (erule (2) adm_disj_lemma1 [THEN disjI1])
   1.105 +apply (erule (2) adm_disj_lemma1 [THEN disjI2])
   1.106  done
   1.107  
   1.108 -lemma adm_imp: "\<lbrakk>adm (\<lambda>x. \<not> P x); adm Q\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<longrightarrow> Q x)"
   1.109 +lemma adm_imp [simp]:
   1.110 +  "\<lbrakk>adm (\<lambda>x. \<not> P x); adm (\<lambda>x. Q x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<longrightarrow> Q x)"
   1.111  by (subst imp_conv_disj, rule adm_disj)
   1.112  
   1.113 -lemma adm_iff:
   1.114 +lemma adm_iff [simp]:
   1.115    "\<lbrakk>adm (\<lambda>x. P x \<longrightarrow> Q x); adm (\<lambda>x. Q x \<longrightarrow> P x)\<rbrakk>  
   1.116      \<Longrightarrow> adm (\<lambda>x. P x = Q x)"
   1.117  by (subst iff_conv_conj_imp, rule adm_conj)
   1.118  
   1.119 -lemma adm_not_conj:
   1.120 -  "\<lbrakk>adm (\<lambda>x. \<not> P x); adm (\<lambda>x. \<not> Q x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. \<not> (P x \<and> Q x))"
   1.121 -by (simp add: adm_imp)
   1.122 -
   1.123  text {* admissibility and continuity *}
   1.124  
   1.125 -lemma adm_below: "\<lbrakk>cont u; cont v\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x \<sqsubseteq> v x)"
   1.126 +lemma adm_below [simp]:
   1.127 +  "\<lbrakk>cont (\<lambda>x. u x); cont (\<lambda>x. v x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x \<sqsubseteq> v x)"
   1.128  apply (rule admI)
   1.129  apply (simp add: cont2contlubE)
   1.130  apply (rule lub_mono)
   1.131 @@ -131,10 +130,11 @@
   1.132  apply (erule spec)
   1.133  done
   1.134  
   1.135 -lemma adm_eq: "\<lbrakk>cont u; cont v\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x = v x)"
   1.136 -by (simp add: po_eq_conv adm_conj adm_below)
   1.137 +lemma adm_eq [simp]:
   1.138 +  "\<lbrakk>cont (\<lambda>x. u x); cont (\<lambda>x. v x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x = v x)"
   1.139 +by (simp add: po_eq_conv)
   1.140  
   1.141 -lemma adm_subst: "\<lbrakk>cont t; adm P\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P (t x))"
   1.142 +lemma adm_subst: "\<lbrakk>cont (\<lambda>x. t x); adm P\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P (t x))"
   1.143  apply (rule admI)
   1.144  apply (simp add: cont2contlubE)
   1.145  apply (erule admD)
   1.146 @@ -142,14 +142,8 @@
   1.147  apply (erule spec)
   1.148  done
   1.149  
   1.150 -lemma adm_not_below: "cont t \<Longrightarrow> adm (\<lambda>x. \<not> t x \<sqsubseteq> u)"
   1.151 -apply (rule admI)
   1.152 -apply (drule_tac x=0 in spec)
   1.153 -apply (erule contrapos_nn)
   1.154 -apply (erule rev_below_trans)
   1.155 -apply (erule cont2mono [THEN monofunE])
   1.156 -apply (erule is_ub_thelub)
   1.157 -done
   1.158 +lemma adm_not_below [simp]: "cont (\<lambda>x. t x) \<Longrightarrow> adm (\<lambda>x. \<not> t x \<sqsubseteq> u)"
   1.159 +by (rule admI, simp add: cont2contlubE ch2ch_cont lub_below_iff)
   1.160  
   1.161  subsection {* Compactness *}
   1.162  
   1.163 @@ -190,20 +184,20 @@
   1.164  
   1.165  text {* admissibility and compactness *}
   1.166  
   1.167 -lemma adm_compact_not_below: "\<lbrakk>compact k; cont t\<rbrakk> \<Longrightarrow> adm (\<lambda>x. \<not> k \<sqsubseteq> t x)"
   1.168 +lemma adm_compact_not_below [simp]:
   1.169 +  "\<lbrakk>compact k; cont (\<lambda>x. t x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. \<not> k \<sqsubseteq> t x)"
   1.170  unfolding compact_def by (rule adm_subst)
   1.171  
   1.172 -lemma adm_neq_compact: "\<lbrakk>compact k; cont t\<rbrakk> \<Longrightarrow> adm (\<lambda>x. t x \<noteq> k)"
   1.173 -by (simp add: po_eq_conv adm_imp adm_not_below adm_compact_not_below)
   1.174 +lemma adm_neq_compact [simp]:
   1.175 +  "\<lbrakk>compact k; cont (\<lambda>x. t x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. t x \<noteq> k)"
   1.176 +by (simp add: po_eq_conv)
   1.177  
   1.178 -lemma adm_compact_neq: "\<lbrakk>compact k; cont t\<rbrakk> \<Longrightarrow> adm (\<lambda>x. k \<noteq> t x)"
   1.179 -by (simp add: po_eq_conv adm_imp adm_not_below adm_compact_not_below)
   1.180 +lemma adm_compact_neq [simp]:
   1.181 +  "\<lbrakk>compact k; cont (\<lambda>x. t x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. k \<noteq> t x)"
   1.182 +by (simp add: po_eq_conv)
   1.183  
   1.184  lemma compact_UU [simp, intro]: "compact \<bottom>"
   1.185 -by (rule compactI, simp add: adm_not_free)
   1.186 -
   1.187 -lemma adm_not_UU: "cont t \<Longrightarrow> adm (\<lambda>x. t x \<noteq> \<bottom>)"
   1.188 -by (simp add: adm_neq_compact)
   1.189 +by (rule compactI, simp)
   1.190  
   1.191  text {* Any upward-closed predicate is admissible. *}
   1.192  
   1.193 @@ -212,9 +206,9 @@
   1.194    shows "adm P"
   1.195  by (rule admI, drule spec, erule P, erule is_ub_thelub)
   1.196  
   1.197 -lemmas adm_lemmas [simp] =
   1.198 -  adm_not_free adm_conj adm_all adm_ball adm_disj adm_imp adm_iff
   1.199 +lemmas adm_lemmas =
   1.200 +  adm_const adm_conj adm_all adm_ball adm_disj adm_imp adm_iff
   1.201    adm_below adm_eq adm_not_below
   1.202 -  adm_compact_not_below adm_compact_neq adm_neq_compact adm_not_UU
   1.203 +  adm_compact_not_below adm_compact_neq adm_neq_compact
   1.204  
   1.205  end