src/HOLCF/Adm.thy
author huffman
Tue Oct 12 06:20:05 2010 -0700 (2010-10-12)
changeset 40006 116e94f9543b
parent 39969 0b8e19f588a4
child 40007 bb04a995bbd3
permissions -rw-r--r--
remove unneeded lemmas from Fun_Cpo.thy
     1 (*  Title:      HOLCF/Adm.thy
     2     Author:     Franz Regensburger and Brian Huffman
     3 *)
     4 
     5 header {* Admissibility and compactness *}
     6 
     7 theory Adm
     8 imports Cont
     9 begin
    10 
    11 default_sort cpo
    12 
    13 subsection {* Definitions *}
    14 
    15 definition
    16   adm :: "('a::cpo \<Rightarrow> bool) \<Rightarrow> bool" where
    17   "adm P = (\<forall>Y. chain Y \<longrightarrow> (\<forall>i. P (Y i)) \<longrightarrow> P (\<Squnion>i. Y i))"
    18 
    19 lemma admI:
    20    "(\<And>Y. \<lbrakk>chain Y; \<forall>i. P (Y i)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)) \<Longrightarrow> adm P"
    21 unfolding adm_def by fast
    22 
    23 lemma admD: "\<lbrakk>adm P; chain Y; \<And>i. P (Y i)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)"
    24 unfolding adm_def by fast
    25 
    26 lemma admD2: "\<lbrakk>adm (\<lambda>x. \<not> P x); chain Y; P (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. P (Y i)"
    27 unfolding adm_def by fast
    28 
    29 lemma triv_admI: "\<forall>x. P x \<Longrightarrow> adm P"
    30 by (rule admI, erule spec)
    31 
    32 text {* improved admissibility introduction *}
    33 
    34 lemma admI2:
    35   "(\<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> 
    36     \<Longrightarrow> P (\<Squnion>i. Y i)) \<Longrightarrow> adm P"
    37 apply (rule admI)
    38 apply (erule (1) increasing_chain_adm_lemma)
    39 apply fast
    40 done
    41 
    42 subsection {* Admissibility on chain-finite types *}
    43 
    44 text {* for chain-finite (easy) types every formula is admissible *}
    45 
    46 lemma adm_chfin: "adm (P::'a::chfin \<Rightarrow> bool)"
    47 by (rule admI, frule chfin, auto simp add: maxinch_is_thelub)
    48 
    49 subsection {* Admissibility of special formulae and propagation *}
    50 
    51 lemma adm_not_free: "adm (\<lambda>x. t)"
    52 by (rule admI, simp)
    53 
    54 lemma adm_conj: "\<lbrakk>adm P; adm Q\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<and> Q x)"
    55 by (fast intro: admI elim: admD)
    56 
    57 lemma adm_all: "(\<And>y. adm (\<lambda>x. P x y)) \<Longrightarrow> adm (\<lambda>x. \<forall>y. P x y)"
    58 by (fast intro: admI elim: admD)
    59 
    60 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)"
    61 by (fast intro: admI elim: admD)
    62 
    63 text {* Admissibility for disjunction is hard to prove. It takes 5 Lemmas *}
    64 
    65 lemma adm_disj_lemma1: 
    66   "\<lbrakk>chain (Y::nat \<Rightarrow> 'a::cpo); \<forall>i. \<exists>j\<ge>i. P (Y j)\<rbrakk>
    67     \<Longrightarrow> chain (\<lambda>i. Y (LEAST j. i \<le> j \<and> P (Y j)))"
    68 apply (rule chainI)
    69 apply (erule chain_mono)
    70 apply (rule Least_le)
    71 apply (rule LeastI2_ex)
    72 apply simp_all
    73 done
    74 
    75 lemmas adm_disj_lemma2 = LeastI_ex [of "\<lambda>j. i \<le> j \<and> P (Y j)", standard]
    76 
    77 lemma adm_disj_lemma3: 
    78   "\<lbrakk>chain (Y::nat \<Rightarrow> 'a::cpo); \<forall>i. \<exists>j\<ge>i. P (Y j)\<rbrakk> \<Longrightarrow> 
    79     (\<Squnion>i. Y i) = (\<Squnion>i. Y (LEAST j. i \<le> j \<and> P (Y j)))"
    80  apply (frule (1) adm_disj_lemma1)
    81  apply (rule below_antisym)
    82   apply (rule lub_mono, assumption+)
    83   apply (erule chain_mono)
    84   apply (simp add: adm_disj_lemma2)
    85  apply (rule lub_range_mono, fast, assumption+)
    86 done
    87 
    88 lemma adm_disj_lemma4:
    89   "\<lbrakk>adm P; chain Y; \<forall>i. \<exists>j\<ge>i. P (Y j)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)"
    90 apply (subst adm_disj_lemma3, assumption+)
    91 apply (erule admD)
    92 apply (simp add: adm_disj_lemma1)
    93 apply (simp add: adm_disj_lemma2)
    94 done
    95 
    96 lemma adm_disj_lemma5:
    97   "\<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)"
    98 apply (erule contrapos_pp)
    99 apply (clarsimp, rename_tac a b)
   100 apply (rule_tac x="max a b" in exI)
   101 apply simp
   102 done
   103 
   104 lemma adm_disj: "\<lbrakk>adm P; adm Q\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<or> Q x)"
   105 apply (rule admI)
   106 apply (erule adm_disj_lemma5 [THEN disjE])
   107 apply (erule (2) adm_disj_lemma4 [THEN disjI1])
   108 apply (erule (2) adm_disj_lemma4 [THEN disjI2])
   109 done
   110 
   111 lemma adm_imp: "\<lbrakk>adm (\<lambda>x. \<not> P x); adm Q\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<longrightarrow> Q x)"
   112 by (subst imp_conv_disj, rule adm_disj)
   113 
   114 lemma adm_iff:
   115   "\<lbrakk>adm (\<lambda>x. P x \<longrightarrow> Q x); adm (\<lambda>x. Q x \<longrightarrow> P x)\<rbrakk>  
   116     \<Longrightarrow> adm (\<lambda>x. P x = Q x)"
   117 by (subst iff_conv_conj_imp, rule adm_conj)
   118 
   119 lemma adm_not_conj:
   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))"
   121 by (simp add: adm_imp)
   122 
   123 text {* admissibility and continuity *}
   124 
   125 lemma adm_below: "\<lbrakk>cont u; cont v\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x \<sqsubseteq> v x)"
   126 apply (rule admI)
   127 apply (simp add: cont2contlubE)
   128 apply (rule lub_mono)
   129 apply (erule (1) ch2ch_cont)
   130 apply (erule (1) ch2ch_cont)
   131 apply (erule spec)
   132 done
   133 
   134 lemma adm_eq: "\<lbrakk>cont u; cont v\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x = v x)"
   135 by (simp add: po_eq_conv adm_conj adm_below)
   136 
   137 lemma adm_subst: "\<lbrakk>cont t; adm P\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P (t x))"
   138 apply (rule admI)
   139 apply (simp add: cont2contlubE)
   140 apply (erule admD)
   141 apply (erule (1) ch2ch_cont)
   142 apply (erule spec)
   143 done
   144 
   145 lemma adm_not_below: "cont t \<Longrightarrow> adm (\<lambda>x. \<not> t x \<sqsubseteq> u)"
   146 apply (rule admI)
   147 apply (drule_tac x=0 in spec)
   148 apply (erule contrapos_nn)
   149 apply (erule rev_below_trans)
   150 apply (erule cont2mono [THEN monofunE])
   151 apply (erule is_ub_thelub)
   152 done
   153 
   154 subsection {* Compactness *}
   155 
   156 definition
   157   compact :: "'a::cpo \<Rightarrow> bool" where
   158   "compact k = adm (\<lambda>x. \<not> k \<sqsubseteq> x)"
   159 
   160 lemma compactI: "adm (\<lambda>x. \<not> k \<sqsubseteq> x) \<Longrightarrow> compact k"
   161 unfolding compact_def .
   162 
   163 lemma compactD: "compact k \<Longrightarrow> adm (\<lambda>x. \<not> k \<sqsubseteq> x)"
   164 unfolding compact_def .
   165 
   166 lemma compactI2:
   167   "(\<And>Y. \<lbrakk>chain Y; x \<sqsubseteq> (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. x \<sqsubseteq> Y i) \<Longrightarrow> compact x"
   168 unfolding compact_def adm_def by fast
   169 
   170 lemma compactD2:
   171   "\<lbrakk>compact x; chain Y; x \<sqsubseteq> (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. x \<sqsubseteq> Y i"
   172 unfolding compact_def adm_def by fast
   173 
   174 lemma compact_below_lub_iff:
   175   "\<lbrakk>compact x; chain Y\<rbrakk> \<Longrightarrow> x \<sqsubseteq> (\<Squnion>i. Y i) \<longleftrightarrow> (\<exists>i. x \<sqsubseteq> Y i)"
   176 by (fast intro: compactD2 elim: below_trans is_ub_thelub)
   177 
   178 lemma compact_chfin [simp]: "compact (x::'a::chfin)"
   179 by (rule compactI [OF adm_chfin])
   180 
   181 lemma compact_imp_max_in_chain:
   182   "\<lbrakk>chain Y; compact (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. max_in_chain i Y"
   183 apply (drule (1) compactD2, simp)
   184 apply (erule exE, rule_tac x=i in exI)
   185 apply (rule max_in_chainI)
   186 apply (rule below_antisym)
   187 apply (erule (1) chain_mono)
   188 apply (erule (1) below_trans [OF is_ub_thelub])
   189 done
   190 
   191 text {* admissibility and compactness *}
   192 
   193 lemma adm_compact_not_below: "\<lbrakk>compact k; cont t\<rbrakk> \<Longrightarrow> adm (\<lambda>x. \<not> k \<sqsubseteq> t x)"
   194 unfolding compact_def by (rule adm_subst)
   195 
   196 lemma adm_neq_compact: "\<lbrakk>compact k; cont t\<rbrakk> \<Longrightarrow> adm (\<lambda>x. t x \<noteq> k)"
   197 by (simp add: po_eq_conv adm_imp adm_not_below adm_compact_not_below)
   198 
   199 lemma adm_compact_neq: "\<lbrakk>compact k; cont t\<rbrakk> \<Longrightarrow> adm (\<lambda>x. k \<noteq> t x)"
   200 by (simp add: po_eq_conv adm_imp adm_not_below adm_compact_not_below)
   201 
   202 lemma compact_UU [simp, intro]: "compact \<bottom>"
   203 by (rule compactI, simp add: adm_not_free)
   204 
   205 lemma adm_not_UU: "cont t \<Longrightarrow> adm (\<lambda>x. t x \<noteq> \<bottom>)"
   206 by (simp add: adm_neq_compact)
   207 
   208 text {* Any upward-closed predicate is admissible. *}
   209 
   210 lemma adm_upward:
   211   assumes P: "\<And>x y. \<lbrakk>P x; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> P y"
   212   shows "adm P"
   213 by (rule admI, drule spec, erule P, erule is_ub_thelub)
   214 
   215 lemmas adm_lemmas [simp] =
   216   adm_not_free adm_conj adm_all adm_ball adm_disj adm_imp adm_iff
   217   adm_below adm_eq adm_not_below
   218   adm_compact_not_below adm_compact_neq adm_neq_compact adm_not_UU
   219 
   220 end