src/HOLCF/Adm.thy
author huffman
Sat Jun 25 01:09:14 2005 +0200 (2005-06-25)
changeset 16565 00a3bf006881
parent 16207 d67baef02f78
child 16623 f3fcfa388ecb
permissions -rw-r--r--
cleaned up
     1 (*  Title:      HOLCF/Adm.thy
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4 *)
     5 
     6 header {* Admissibility *}
     7 
     8 theory Adm
     9 imports Cont
    10 begin
    11 
    12 defaultsort cpo
    13 
    14 subsection {* Definitions *}
    15 
    16 constdefs
    17   adm :: "('a::cpo \<Rightarrow> bool) \<Rightarrow> bool"
    18   "adm P \<equiv> \<forall>Y. chain Y \<longrightarrow> (\<forall>i. P (Y i)) \<longrightarrow> P (lub (range Y))"
    19 
    20 subsection {* Admissibility and fixed point induction *}
    21 
    22 text {* access to definitions *}
    23 
    24 lemma admI:
    25    "(\<And>Y. \<lbrakk>chain Y; \<forall>i. P (Y i)\<rbrakk> \<Longrightarrow> P (lub (range Y))) \<Longrightarrow> adm P"
    26 apply (unfold adm_def)
    27 apply blast
    28 done
    29 
    30 lemma triv_admI: "\<forall>x. P x \<Longrightarrow> adm P"
    31 apply (rule admI)
    32 apply (erule spec)
    33 done
    34 
    35 lemma admD: "\<lbrakk>adm P; chain Y; \<forall>i. P (Y i)\<rbrakk> \<Longrightarrow> P (lub (range Y))"
    36 apply (unfold adm_def)
    37 apply blast
    38 done
    39 
    40 text {* for chain-finite (easy) types every formula is admissible *}
    41 
    42 lemma adm_max_in_chain: 
    43   "\<forall>Y. chain (Y::nat=>'a) \<longrightarrow> (\<exists>n. max_in_chain n Y) \<Longrightarrow> adm (P::'a=>bool)"
    44 apply (unfold adm_def)
    45 apply (intro strip)
    46 apply (drule spec)
    47 apply (drule mp)
    48 apply assumption
    49 apply (erule exE)
    50 apply (subst lub_finch1 [THEN thelubI])
    51 apply assumption
    52 apply assumption
    53 apply (erule spec)
    54 done
    55 
    56 lemmas adm_chfin = chfin [THEN adm_max_in_chain, standard]
    57 
    58 text {* improved admissibility introduction *}
    59 
    60 lemma admI2:
    61   "(\<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> 
    62     \<Longrightarrow> P (lub (range Y))) \<Longrightarrow> adm P"
    63 apply (rule admI)
    64 apply (erule increasing_chain_adm_lemma)
    65 apply assumption
    66 apply fast
    67 done
    68 
    69 text {* admissibility of special formulae and propagation *}
    70 
    71 lemma adm_less [simp]: "\<lbrakk>cont u; cont v\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x \<sqsubseteq> v x)"
    72 apply (rule admI)
    73 apply (simp add: cont2contlub [THEN contlubE])
    74 apply (rule lub_mono)
    75 apply (erule (1) cont2mono [THEN ch2ch_monofun])
    76 apply (erule (1) cont2mono [THEN ch2ch_monofun])
    77 apply assumption
    78 done
    79 
    80 lemma adm_conj: "\<lbrakk>adm P; adm Q\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<and> Q x)"
    81 by (fast elim: admD intro: admI)
    82 
    83 lemma adm_not_free: "adm (\<lambda>x. t)"
    84 by (rule admI, simp)
    85 
    86 lemma adm_not_less: "cont t \<Longrightarrow> adm (\<lambda>x. \<not> t x \<sqsubseteq> u)"
    87 apply (rule admI)
    88 apply (drule_tac x=0 in spec)
    89 apply (erule contrapos_nn)
    90 apply (rule trans_less)
    91 prefer 2 apply (assumption)
    92 apply (erule cont2mono [THEN monofun_fun_arg])
    93 apply (erule is_ub_thelub)
    94 done
    95 
    96 lemma adm_all: "\<forall>y. adm (P y) \<Longrightarrow> adm (\<lambda>x. \<forall>y. P y x)"
    97 by (fast intro: admI elim: admD)
    98 
    99 lemmas adm_all2 = allI [THEN adm_all, standard]
   100 
   101 lemma adm_subst: "\<lbrakk>cont t; adm P\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P (t x))"
   102 apply (rule admI)
   103 apply (simp add: cont2contlub [THEN contlubE])
   104 apply (erule admD)
   105 apply (erule cont2mono [THEN ch2ch_monofun])
   106 apply assumption
   107 apply assumption
   108 done
   109 
   110 lemma adm_UU_not_less: "adm (\<lambda>x. \<not> \<bottom> \<sqsubseteq> t x)"
   111 by (simp add: adm_not_free)
   112 
   113 lemma adm_not_UU: "cont t \<Longrightarrow> adm (\<lambda>x. \<not> t x = \<bottom>)"
   114 by (simp add: eq_UU_iff adm_not_less)
   115 
   116 lemma adm_eq: "\<lbrakk>cont u; cont v\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x = v x)"
   117 by (simp add: po_eq_conv adm_conj)
   118 
   119 text {* admissibility for disjunction is hard to prove. It takes 7 Lemmas *}
   120 
   121 lemma adm_disj_lemma1:
   122   "\<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)"
   123 apply (erule contrapos_pp)
   124 apply clarsimp
   125 apply (rule exI)
   126 apply (rule conjI)
   127 apply (drule spec, erule mp)
   128 apply (rule le_maxI1)
   129 apply (drule spec, erule mp)
   130 apply (rule le_maxI2)
   131 done
   132 
   133 lemma adm_disj_lemma2:
   134   "\<lbrakk>adm P; \<exists>X. chain X \<and> (\<forall>n. P (X n)) \<and> 
   135     lub (range Y) = lub (range X)\<rbrakk> \<Longrightarrow> P (lub (range Y))"
   136 by (force elim: admD)
   137 
   138 lemma adm_disj_lemma3: 
   139   "\<lbrakk>chain (Y::nat=>'a::cpo); \<forall>i. \<exists>j\<ge>i. P (Y j)\<rbrakk> \<Longrightarrow>
   140     chain (\<lambda>m. Y (LEAST j. m \<le> j \<and> P (Y j)))"
   141 apply (rule chainI)
   142 apply (erule chain_mono3)
   143 apply (rule Least_le)
   144 apply (rule conjI)
   145 apply (rule Suc_leD)
   146 apply (erule allE)
   147 apply (erule exE)
   148 apply (erule LeastI [THEN conjunct1])
   149 apply (erule allE)
   150 apply (erule exE)
   151 apply (erule LeastI [THEN conjunct2])
   152 done
   153 
   154 lemma adm_disj_lemma4: 
   155   "\<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)))"
   156 apply (rule allI)
   157 apply (erule allE)
   158 apply (erule exE)
   159 apply (erule LeastI [THEN conjunct2])
   160 done
   161 
   162 lemma adm_disj_lemma5: 
   163   "\<lbrakk>chain (Y::nat=>'a::cpo); \<forall>i. \<exists>j\<ge>i. P(Y j)\<rbrakk> \<Longrightarrow> 
   164     lub (range Y) = (LUB m. Y (LEAST j. m \<le> j \<and> P (Y j)))"
   165  apply (rule antisym_less)
   166   apply (rule lub_mono)
   167     apply assumption
   168    apply (erule (1) adm_disj_lemma3)
   169   apply (rule allI)
   170   apply (erule chain_mono3)
   171   apply (erule allE)
   172   apply (erule exE)
   173   apply (erule LeastI [THEN conjunct1])
   174  apply (rule lub_mono3)
   175    apply (erule (1) adm_disj_lemma3)
   176   apply assumption
   177  apply (rule allI)
   178  apply (rule exI)
   179  apply (rule refl_less)
   180 done
   181 
   182 lemma adm_disj_lemma6:
   183   "\<lbrakk>chain (Y::nat=>'a::cpo); \<forall>i. \<exists>j\<ge>i. P(Y j)\<rbrakk> \<Longrightarrow>
   184     \<exists>X. chain X \<and> (\<forall>n. P (X n)) \<and> lub (range Y) = lub (range X)"
   185 apply (rule_tac x = "\<lambda>m. Y (LEAST j. m \<le> j \<and> P (Y j))" in exI)
   186 apply (fast intro!: adm_disj_lemma3 adm_disj_lemma4 adm_disj_lemma5)
   187 done
   188 
   189 lemma adm_disj_lemma7:
   190   "\<lbrakk>adm P; chain Y; \<forall>i. \<exists>j\<ge>i. P (Y j)\<rbrakk> \<Longrightarrow> P (lub (range Y))"
   191 apply (erule adm_disj_lemma2)
   192 apply (erule (1) adm_disj_lemma6)
   193 done
   194 
   195 lemma adm_disj: "[| adm P; adm Q |] ==> adm(%x. P x | Q x)"
   196 apply (rule admI)
   197 apply (erule adm_disj_lemma1 [THEN disjE])
   198 apply (rule disjI1)
   199 apply (erule (2) adm_disj_lemma7)
   200 apply (rule disjI2)
   201 apply (erule (2) adm_disj_lemma7)
   202 done
   203 
   204 lemma adm_imp: "\<lbrakk>adm (\<lambda>x. \<not> P x); adm Q\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<longrightarrow> Q x)"
   205 by (subst imp_conv_disj, rule adm_disj)
   206 
   207 lemma adm_iff:
   208   "\<lbrakk>adm (\<lambda>x. P x \<longrightarrow> Q x); adm (\<lambda>x. Q x \<longrightarrow> P x)\<rbrakk>  
   209     \<Longrightarrow> adm (\<lambda>x. P x = Q x)"
   210 by (subst iff_conv_conj_imp, rule adm_conj)
   211 
   212 lemma adm_not_conj:
   213   "\<lbrakk>adm (\<lambda>x. \<not> P x); adm (\<lambda>x. \<not> Q x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. \<not> (P x \<and> Q x))"
   214 by (subst de_Morgan_conj, rule adm_disj)
   215 
   216 lemmas adm_lemmas =
   217   adm_conj adm_not_free adm_imp adm_disj adm_eq adm_not_UU
   218   adm_UU_not_less adm_all2 adm_not_less adm_not_conj adm_iff
   219 
   220 declare adm_lemmas [simp]
   221 
   222 (* legacy ML bindings *)
   223 ML
   224 {*
   225 val adm_def = thm "adm_def";
   226 val admI = thm "admI";
   227 val triv_admI = thm "triv_admI";
   228 val admD = thm "admD";
   229 val adm_max_in_chain = thm "adm_max_in_chain";
   230 val adm_chfin = thm "adm_chfin";
   231 val admI2 = thm "admI2";
   232 val adm_less = thm "adm_less";
   233 val adm_conj = thm "adm_conj";
   234 val adm_not_free = thm "adm_not_free";
   235 val adm_not_less = thm "adm_not_less";
   236 val adm_all = thm "adm_all";
   237 val adm_all2 = thm "adm_all2";
   238 val adm_subst = thm "adm_subst";
   239 val adm_UU_not_less = thm "adm_UU_not_less";
   240 val adm_not_UU = thm "adm_not_UU";
   241 val adm_eq = thm "adm_eq";
   242 val adm_disj_lemma1 = thm "adm_disj_lemma1";
   243 val adm_disj_lemma2 = thm "adm_disj_lemma2";
   244 val adm_disj_lemma3 = thm "adm_disj_lemma3";
   245 val adm_disj_lemma4 = thm "adm_disj_lemma4";
   246 val adm_disj_lemma5 = thm "adm_disj_lemma5";
   247 val adm_disj_lemma6 = thm "adm_disj_lemma6";
   248 val adm_disj_lemma7 = thm "adm_disj_lemma7";
   249 val adm_disj = thm "adm_disj";
   250 val adm_imp = thm "adm_imp";
   251 val adm_iff = thm "adm_iff";
   252 val adm_not_conj = thm "adm_not_conj";
   253 val adm_lemmas = thms "adm_lemmas";
   254 *}
   255 
   256 end
   257