src/HOLCF/Adm.thy
changeset 16565 00a3bf006881
parent 16207 d67baef02f78
child 16623 f3fcfa388ecb
     1.1 --- a/src/HOLCF/Adm.thy	Sat Jun 25 01:04:01 2005 +0200
     1.2 +++ b/src/HOLCF/Adm.thy	Sat Jun 25 01:09:14 2005 +0200
     1.3 @@ -13,29 +13,26 @@
     1.4  
     1.5  subsection {* Definitions *}
     1.6  
     1.7 -consts
     1.8 -adm		:: "('a::cpo=>bool)=>bool"
     1.9 -
    1.10 -defs
    1.11 -adm_def:       "adm P == !Y. chain(Y) --> 
    1.12 -                        (!i. P(Y i)) --> P(lub(range Y))"
    1.13 +constdefs
    1.14 +  adm :: "('a::cpo \<Rightarrow> bool) \<Rightarrow> bool"
    1.15 +  "adm P \<equiv> \<forall>Y. chain Y \<longrightarrow> (\<forall>i. P (Y i)) \<longrightarrow> P (lub (range Y))"
    1.16  
    1.17  subsection {* Admissibility and fixed point induction *}
    1.18  
    1.19  text {* access to definitions *}
    1.20  
    1.21  lemma admI:
    1.22 -   "(!!Y. [| chain Y; !i. P (Y i) |] ==> P (lub (range Y))) ==> adm P"
    1.23 +   "(\<And>Y. \<lbrakk>chain Y; \<forall>i. P (Y i)\<rbrakk> \<Longrightarrow> P (lub (range Y))) \<Longrightarrow> adm P"
    1.24  apply (unfold adm_def)
    1.25  apply blast
    1.26  done
    1.27  
    1.28 -lemma triv_admI: "!x. P x ==> adm P"
    1.29 +lemma triv_admI: "\<forall>x. P x \<Longrightarrow> adm P"
    1.30  apply (rule admI)
    1.31  apply (erule spec)
    1.32  done
    1.33  
    1.34 -lemma admD: "[| adm(P); chain(Y); !i. P(Y(i)) |] ==> P(lub(range(Y)))"
    1.35 +lemma admD: "\<lbrakk>adm P; chain Y; \<forall>i. P (Y i)\<rbrakk> \<Longrightarrow> P (lub (range Y))"
    1.36  apply (unfold adm_def)
    1.37  apply blast
    1.38  done
    1.39 @@ -43,13 +40,13 @@
    1.40  text {* for chain-finite (easy) types every formula is admissible *}
    1.41  
    1.42  lemma adm_max_in_chain: 
    1.43 -"!Y. chain(Y::nat=>'a) --> (? n. max_in_chain n Y) ==> adm(P::'a=>bool)"
    1.44 +  "\<forall>Y. chain (Y::nat=>'a) \<longrightarrow> (\<exists>n. max_in_chain n Y) \<Longrightarrow> adm (P::'a=>bool)"
    1.45  apply (unfold adm_def)
    1.46  apply (intro strip)
    1.47 -apply (rule exE)
    1.48 -apply (rule mp)
    1.49 -apply (erule spec)
    1.50 +apply (drule spec)
    1.51 +apply (drule mp)
    1.52  apply assumption
    1.53 +apply (erule exE)
    1.54  apply (subst lub_finch1 [THEN thelubI])
    1.55  apply assumption
    1.56  apply assumption
    1.57 @@ -61,10 +58,9 @@
    1.58  text {* improved admissibility introduction *}
    1.59  
    1.60  lemma admI2:
    1.61 - "(!!Y. [| chain Y; !i. P (Y i); !i. ? j. i < j & Y i ~= Y j & Y i << Y j |] 
    1.62 -  ==> P(lub (range Y))) ==> adm P"
    1.63 -apply (unfold adm_def)
    1.64 -apply (intro strip)
    1.65 +  "(\<And>Y. \<lbrakk>chain Y; \<forall>i. P (Y i); \<forall>i. \<exists>j>i. Y i \<noteq> Y j \<and> Y i \<sqsubseteq> Y j\<rbrakk> 
    1.66 +    \<Longrightarrow> P (lub (range Y))) \<Longrightarrow> adm P"
    1.67 +apply (rule admI)
    1.68  apply (erule increasing_chain_adm_lemma)
    1.69  apply assumption
    1.70  apply fast
    1.71 @@ -72,74 +68,53 @@
    1.72  
    1.73  text {* admissibility of special formulae and propagation *}
    1.74  
    1.75 -lemma adm_less [simp]: "[|cont u;cont v|]==> adm(%x. u x << v x)"
    1.76 -apply (unfold adm_def)
    1.77 -apply (intro strip)
    1.78 -apply (frule_tac f = "u" in cont2mono [THEN ch2ch_monofun])
    1.79 +lemma adm_less [simp]: "\<lbrakk>cont u; cont v\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x \<sqsubseteq> v x)"
    1.80 +apply (rule admI)
    1.81 +apply (simp add: cont2contlub [THEN contlubE])
    1.82 +apply (rule lub_mono)
    1.83 +apply (erule (1) cont2mono [THEN ch2ch_monofun])
    1.84 +apply (erule (1) cont2mono [THEN ch2ch_monofun])
    1.85  apply assumption
    1.86 -apply (frule_tac f = "v" in cont2mono [THEN ch2ch_monofun])
    1.87 -apply assumption
    1.88 -apply (erule cont2contlub [THEN contlubE, THEN ssubst])
    1.89 -apply assumption
    1.90 -apply (erule cont2contlub [THEN contlubE, THEN ssubst])
    1.91 -apply assumption
    1.92 -apply (blast intro: lub_mono)
    1.93  done
    1.94  
    1.95 -lemma adm_conj [simp]: "[| adm P; adm Q |] ==> adm(%x. P x & Q x)"
    1.96 +lemma adm_conj: "\<lbrakk>adm P; adm Q\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<and> Q x)"
    1.97  by (fast elim: admD intro: admI)
    1.98  
    1.99 -lemma adm_not_free [simp]: "adm(%x. t)"
   1.100 -apply (unfold adm_def)
   1.101 -apply fast
   1.102 -done
   1.103 +lemma adm_not_free: "adm (\<lambda>x. t)"
   1.104 +by (rule admI, simp)
   1.105  
   1.106 -lemma adm_not_less: "cont t ==> adm(%x.~ (t x) << u)"
   1.107 -apply (unfold adm_def)
   1.108 -apply (intro strip)
   1.109 -apply (rule contrapos_nn)
   1.110 -apply (erule spec)
   1.111 +lemma adm_not_less: "cont t \<Longrightarrow> adm (\<lambda>x. \<not> t x \<sqsubseteq> u)"
   1.112 +apply (rule admI)
   1.113 +apply (drule_tac x=0 in spec)
   1.114 +apply (erule contrapos_nn)
   1.115  apply (rule trans_less)
   1.116  prefer 2 apply (assumption)
   1.117  apply (erule cont2mono [THEN monofun_fun_arg])
   1.118 -apply (rule is_ub_thelub)
   1.119 -apply assumption
   1.120 +apply (erule is_ub_thelub)
   1.121  done
   1.122  
   1.123 -lemma adm_all: "!y. adm(P y) ==> adm(%x.!y. P y x)"
   1.124 +lemma adm_all: "\<forall>y. adm (P y) \<Longrightarrow> adm (\<lambda>x. \<forall>y. P y x)"
   1.125  by (fast intro: admI elim: admD)
   1.126  
   1.127  lemmas adm_all2 = allI [THEN adm_all, standard]
   1.128  
   1.129 -lemma adm_subst: "[|cont t; adm P|] ==> adm(%x. P (t x))"
   1.130 +lemma adm_subst: "\<lbrakk>cont t; adm P\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P (t x))"
   1.131  apply (rule admI)
   1.132 -apply (simplesubst cont2contlub [THEN contlubE])
   1.133 -apply assumption
   1.134 -apply assumption
   1.135 +apply (simp add: cont2contlub [THEN contlubE])
   1.136  apply (erule admD)
   1.137  apply (erule cont2mono [THEN ch2ch_monofun])
   1.138  apply assumption
   1.139  apply assumption
   1.140  done
   1.141  
   1.142 -lemma adm_UU_not_less: "adm(%x.~ UU << t(x))"
   1.143 -by simp
   1.144 +lemma adm_UU_not_less: "adm (\<lambda>x. \<not> \<bottom> \<sqsubseteq> t x)"
   1.145 +by (simp add: adm_not_free)
   1.146  
   1.147 -lemma adm_not_UU: "cont(t)==> adm(%x.~ (t x) = UU)"
   1.148 -apply (unfold adm_def)
   1.149 -apply (intro strip)
   1.150 -apply (rule contrapos_nn)
   1.151 -apply (erule spec)
   1.152 -apply (rule chain_UU_I [THEN spec])
   1.153 -apply (erule cont2mono [THEN ch2ch_monofun])
   1.154 -apply assumption
   1.155 -apply (erule cont2contlub [THEN contlubE, THEN subst])
   1.156 -apply assumption
   1.157 -apply assumption
   1.158 -done
   1.159 +lemma adm_not_UU: "cont t \<Longrightarrow> adm (\<lambda>x. \<not> t x = \<bottom>)"
   1.160 +by (simp add: eq_UU_iff adm_not_less)
   1.161  
   1.162 -lemma adm_eq: "[|cont u ; cont v|]==> adm(%x. u x = v x)"
   1.163 -by (simp add: po_eq_conv)
   1.164 +lemma adm_eq: "\<lbrakk>cont u; cont v\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x = v x)"
   1.165 +by (simp add: po_eq_conv adm_conj)
   1.166  
   1.167  text {* admissibility for disjunction is hard to prove. It takes 7 Lemmas *}
   1.168  
   1.169 @@ -155,13 +130,14 @@
   1.170  apply (rule le_maxI2)
   1.171  done
   1.172  
   1.173 -lemma adm_disj_lemma2: "[| adm P; \<exists>X. chain X & (!n. P(X n)) & 
   1.174 -      lub(range Y)=lub(range X)|] ==> P(lub(range Y))"
   1.175 +lemma adm_disj_lemma2:
   1.176 +  "\<lbrakk>adm P; \<exists>X. chain X \<and> (\<forall>n. P (X n)) \<and> 
   1.177 +    lub (range Y) = lub (range X)\<rbrakk> \<Longrightarrow> P (lub (range Y))"
   1.178  by (force elim: admD)
   1.179  
   1.180  lemma adm_disj_lemma3: 
   1.181 -  "[| chain(Y::nat=>'a::cpo); \<forall>i. \<exists>j\<ge>i. P (Y j) |] ==> 
   1.182 -            chain(%m. Y (LEAST j. m\<le>j \<and> P(Y j)))"
   1.183 +  "\<lbrakk>chain (Y::nat=>'a::cpo); \<forall>i. \<exists>j\<ge>i. P (Y j)\<rbrakk> \<Longrightarrow>
   1.184 +    chain (\<lambda>m. Y (LEAST j. m \<le> j \<and> P (Y j)))"
   1.185  apply (rule chainI)
   1.186  apply (erule chain_mono3)
   1.187  apply (rule Least_le)
   1.188 @@ -176,7 +152,7 @@
   1.189  done
   1.190  
   1.191  lemma adm_disj_lemma4: 
   1.192 -  "[| \<forall>i. \<exists>j\<ge>i. P (Y j) |] ==> ! m. P(Y(LEAST j::nat. m\<le>j & P(Y j)))"
   1.193 +  "\<lbrakk>\<forall>i. \<exists>j\<ge>i. P (Y j)\<rbrakk> \<Longrightarrow> \<forall>m. P (Y (LEAST j::nat. m \<le> j \<and> P (Y j)))"
   1.194  apply (rule allI)
   1.195  apply (erule allE)
   1.196  apply (erule exE)
   1.197 @@ -184,21 +160,19 @@
   1.198  done
   1.199  
   1.200  lemma adm_disj_lemma5: 
   1.201 -  "[| chain(Y::nat=>'a::cpo); \<forall>i. \<exists>j\<ge>i. P(Y j) |] ==> 
   1.202 -            lub(range(Y)) = (LUB m. Y(LEAST j. m\<le>j & P(Y j)))"
   1.203 +  "\<lbrakk>chain (Y::nat=>'a::cpo); \<forall>i. \<exists>j\<ge>i. P(Y j)\<rbrakk> \<Longrightarrow> 
   1.204 +    lub (range Y) = (LUB m. Y (LEAST j. m \<le> j \<and> P (Y j)))"
   1.205   apply (rule antisym_less)
   1.206    apply (rule lub_mono)
   1.207      apply assumption
   1.208 -   apply (erule adm_disj_lemma3)
   1.209 -   apply assumption
   1.210 +   apply (erule (1) adm_disj_lemma3)
   1.211    apply (rule allI)
   1.212    apply (erule chain_mono3)
   1.213    apply (erule allE)
   1.214    apply (erule exE)
   1.215    apply (erule LeastI [THEN conjunct1])
   1.216   apply (rule lub_mono3)
   1.217 -   apply (erule adm_disj_lemma3)
   1.218 -   apply assumption
   1.219 +   apply (erule (1) adm_disj_lemma3)
   1.220    apply assumption
   1.221   apply (rule allI)
   1.222   apply (rule exI)
   1.223 @@ -206,44 +180,42 @@
   1.224  done
   1.225  
   1.226  lemma adm_disj_lemma6:
   1.227 -  "[| chain(Y::nat=>'a::cpo); \<forall>i. \<exists>j\<ge>i. P(Y j) |] ==> 
   1.228 -            \<exists>X. chain X & (\<forall>n. P(X n)) & lub(range Y) = lub(range X)"
   1.229 -apply (rule_tac x = "%m. Y (LEAST j. m\<le>j & P (Y j))" in exI)
   1.230 +  "\<lbrakk>chain (Y::nat=>'a::cpo); \<forall>i. \<exists>j\<ge>i. P(Y j)\<rbrakk> \<Longrightarrow>
   1.231 +    \<exists>X. chain X \<and> (\<forall>n. P (X n)) \<and> lub (range Y) = lub (range X)"
   1.232 +apply (rule_tac x = "\<lambda>m. Y (LEAST j. m \<le> j \<and> P (Y j))" in exI)
   1.233  apply (fast intro!: adm_disj_lemma3 adm_disj_lemma4 adm_disj_lemma5)
   1.234  done
   1.235  
   1.236  lemma adm_disj_lemma7:
   1.237 -"[| adm(P); chain(Y); \<forall>i. \<exists>j\<ge>i. P(Y j) |]==>P(lub(range(Y)))"
   1.238 +  "\<lbrakk>adm P; chain Y; \<forall>i. \<exists>j\<ge>i. P (Y j)\<rbrakk> \<Longrightarrow> P (lub (range Y))"
   1.239  apply (erule adm_disj_lemma2)
   1.240 -apply (erule adm_disj_lemma6)
   1.241 -apply assumption
   1.242 +apply (erule (1) adm_disj_lemma6)
   1.243  done
   1.244  
   1.245  lemma adm_disj: "[| adm P; adm Q |] ==> adm(%x. P x | Q x)"
   1.246  apply (rule admI)
   1.247  apply (erule adm_disj_lemma1 [THEN disjE])
   1.248  apply (rule disjI1)
   1.249 -apply (erule adm_disj_lemma7)
   1.250 -apply assumption
   1.251 -apply assumption
   1.252 +apply (erule (2) adm_disj_lemma7)
   1.253  apply (rule disjI2)
   1.254 -apply (erule adm_disj_lemma7)
   1.255 -apply assumption
   1.256 -apply assumption
   1.257 +apply (erule (2) adm_disj_lemma7)
   1.258  done
   1.259  
   1.260 -lemma adm_imp: "[| adm(%x.~(P x)); adm Q |] ==> adm(%x. P x --> Q x)"
   1.261 +lemma adm_imp: "\<lbrakk>adm (\<lambda>x. \<not> P x); adm Q\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<longrightarrow> Q x)"
   1.262  by (subst imp_conv_disj, rule adm_disj)
   1.263  
   1.264 -lemma adm_iff: "[| adm (%x. P x --> Q x); adm (%x. Q x --> P x) |]  
   1.265 -            ==> adm (%x. P x = Q x)"
   1.266 +lemma adm_iff:
   1.267 +  "\<lbrakk>adm (\<lambda>x. P x \<longrightarrow> Q x); adm (\<lambda>x. Q x \<longrightarrow> P x)\<rbrakk>  
   1.268 +    \<Longrightarrow> adm (\<lambda>x. P x = Q x)"
   1.269  by (subst iff_conv_conj_imp, rule adm_conj)
   1.270  
   1.271 -lemma adm_not_conj: "[| adm (%x. ~ P x); adm (%x. ~ Q x) |] ==> adm (%x. ~ (P x & Q x))"
   1.272 +lemma adm_not_conj:
   1.273 +  "\<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.274  by (subst de_Morgan_conj, rule adm_disj)
   1.275  
   1.276 -lemmas adm_lemmas = adm_not_free adm_imp adm_disj adm_eq adm_not_UU
   1.277 -        adm_UU_not_less adm_all2 adm_not_less adm_not_conj adm_iff
   1.278 +lemmas adm_lemmas =
   1.279 +  adm_conj adm_not_free adm_imp adm_disj adm_eq adm_not_UU
   1.280 +  adm_UU_not_less adm_all2 adm_not_less adm_not_conj adm_iff
   1.281  
   1.282  declare adm_lemmas [simp]
   1.283  
   1.284 @@ -278,8 +250,7 @@
   1.285  val adm_imp = thm "adm_imp";
   1.286  val adm_iff = thm "adm_iff";
   1.287  val adm_not_conj = thm "adm_not_conj";
   1.288 -val adm_lemmas = [adm_not_free, adm_imp, adm_disj, adm_eq, adm_not_UU,
   1.289 -        adm_UU_not_less, adm_all2, adm_not_less, adm_not_conj, adm_iff]
   1.290 +val adm_lemmas = thms "adm_lemmas";
   1.291  *}
   1.292  
   1.293  end