src/HOL/HOLCF/Adm.thy
author wenzelm
Sun Nov 02 17:16:01 2014 +0100 (2014-11-02)
changeset 58880 0baae4311a9f
parent 41959 b460124855b8
child 62175 8ffc4d0e652d
permissions -rw-r--r--
modernized header;
     1 (*  Title:      HOL/HOLCF/Adm.thy
     2     Author:     Franz Regensburger and Brian Huffman
     3 *)
     4 
     5 section {* 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 subsection {* Admissibility on chain-finite types *}
    33 
    34 text {* For chain-finite (easy) types every formula is admissible. *}
    35 
    36 lemma adm_chfin [simp]: "adm (P::'a::chfin \<Rightarrow> bool)"
    37 by (rule admI, frule chfin, auto simp add: maxinch_is_thelub)
    38 
    39 subsection {* Admissibility of special formulae and propagation *}
    40 
    41 lemma adm_const [simp]: "adm (\<lambda>x. t)"
    42 by (rule admI, simp)
    43 
    44 lemma adm_conj [simp]:
    45   "\<lbrakk>adm (\<lambda>x. P x); adm (\<lambda>x. Q x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<and> Q x)"
    46 by (fast intro: admI elim: admD)
    47 
    48 lemma adm_all [simp]:
    49   "(\<And>y. adm (\<lambda>x. P x y)) \<Longrightarrow> adm (\<lambda>x. \<forall>y. P x y)"
    50 by (fast intro: admI elim: admD)
    51 
    52 lemma adm_ball [simp]:
    53   "(\<And>y. y \<in> A \<Longrightarrow> adm (\<lambda>x. P x y)) \<Longrightarrow> adm (\<lambda>x. \<forall>y\<in>A. P x y)"
    54 by (fast intro: admI elim: admD)
    55 
    56 text {* Admissibility for disjunction is hard to prove. It requires 2 lemmas. *}
    57 
    58 lemma adm_disj_lemma1:
    59   assumes adm: "adm P"
    60   assumes chain: "chain Y"
    61   assumes P: "\<forall>i. \<exists>j\<ge>i. P (Y j)"
    62   shows "P (\<Squnion>i. Y i)"
    63 proof -
    64   def f \<equiv> "\<lambda>i. LEAST j. i \<le> j \<and> P (Y j)"
    65   have chain': "chain (\<lambda>i. Y (f i))"
    66     unfolding f_def
    67     apply (rule chainI)
    68     apply (rule chain_mono [OF chain])
    69     apply (rule Least_le)
    70     apply (rule LeastI2_ex)
    71     apply (simp_all add: P)
    72     done
    73   have f1: "\<And>i. i \<le> f i" and f2: "\<And>i. P (Y (f i))"
    74     using LeastI_ex [OF P [rule_format]] by (simp_all add: f_def)
    75   have lub_eq: "(\<Squnion>i. Y i) = (\<Squnion>i. Y (f i))"
    76     apply (rule below_antisym)
    77     apply (rule lub_mono [OF chain chain'])
    78     apply (rule chain_mono [OF chain f1])
    79     apply (rule lub_range_mono [OF _ chain chain'])
    80     apply clarsimp
    81     done
    82   show "P (\<Squnion>i. Y i)"
    83     unfolding lub_eq using adm chain' f2 by (rule admD)
    84 qed
    85 
    86 lemma adm_disj_lemma2:
    87   "\<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)"
    88 apply (erule contrapos_pp)
    89 apply (clarsimp, rename_tac a b)
    90 apply (rule_tac x="max a b" in exI)
    91 apply simp
    92 done
    93 
    94 lemma adm_disj [simp]:
    95   "\<lbrakk>adm (\<lambda>x. P x); adm (\<lambda>x. Q x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<or> Q x)"
    96 apply (rule admI)
    97 apply (erule adm_disj_lemma2 [THEN disjE])
    98 apply (erule (2) adm_disj_lemma1 [THEN disjI1])
    99 apply (erule (2) adm_disj_lemma1 [THEN disjI2])
   100 done
   101 
   102 lemma adm_imp [simp]:
   103   "\<lbrakk>adm (\<lambda>x. \<not> P x); adm (\<lambda>x. Q x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<longrightarrow> Q x)"
   104 by (subst imp_conv_disj, rule adm_disj)
   105 
   106 lemma adm_iff [simp]:
   107   "\<lbrakk>adm (\<lambda>x. P x \<longrightarrow> Q x); adm (\<lambda>x. Q x \<longrightarrow> P x)\<rbrakk>  
   108     \<Longrightarrow> adm (\<lambda>x. P x = Q x)"
   109 by (subst iff_conv_conj_imp, rule adm_conj)
   110 
   111 text {* admissibility and continuity *}
   112 
   113 lemma adm_below [simp]:
   114   "\<lbrakk>cont (\<lambda>x. u x); cont (\<lambda>x. v x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x \<sqsubseteq> v x)"
   115 by (simp add: adm_def cont2contlubE lub_mono ch2ch_cont)
   116 
   117 lemma adm_eq [simp]:
   118   "\<lbrakk>cont (\<lambda>x. u x); cont (\<lambda>x. v x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x = v x)"
   119 by (simp add: po_eq_conv)
   120 
   121 lemma adm_subst: "\<lbrakk>cont (\<lambda>x. t x); adm P\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P (t x))"
   122 by (simp add: adm_def cont2contlubE ch2ch_cont)
   123 
   124 lemma adm_not_below [simp]: "cont (\<lambda>x. t x) \<Longrightarrow> adm (\<lambda>x. t x \<notsqsubseteq> u)"
   125 by (rule admI, simp add: cont2contlubE ch2ch_cont lub_below_iff)
   126 
   127 subsection {* Compactness *}
   128 
   129 definition
   130   compact :: "'a::cpo \<Rightarrow> bool" where
   131   "compact k = adm (\<lambda>x. k \<notsqsubseteq> x)"
   132 
   133 lemma compactI: "adm (\<lambda>x. k \<notsqsubseteq> x) \<Longrightarrow> compact k"
   134 unfolding compact_def .
   135 
   136 lemma compactD: "compact k \<Longrightarrow> adm (\<lambda>x. k \<notsqsubseteq> x)"
   137 unfolding compact_def .
   138 
   139 lemma compactI2:
   140   "(\<And>Y. \<lbrakk>chain Y; x \<sqsubseteq> (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. x \<sqsubseteq> Y i) \<Longrightarrow> compact x"
   141 unfolding compact_def adm_def by fast
   142 
   143 lemma compactD2:
   144   "\<lbrakk>compact x; chain Y; x \<sqsubseteq> (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. x \<sqsubseteq> Y i"
   145 unfolding compact_def adm_def by fast
   146 
   147 lemma compact_below_lub_iff:
   148   "\<lbrakk>compact x; chain Y\<rbrakk> \<Longrightarrow> x \<sqsubseteq> (\<Squnion>i. Y i) \<longleftrightarrow> (\<exists>i. x \<sqsubseteq> Y i)"
   149 by (fast intro: compactD2 elim: below_lub)
   150 
   151 lemma compact_chfin [simp]: "compact (x::'a::chfin)"
   152 by (rule compactI [OF adm_chfin])
   153 
   154 lemma compact_imp_max_in_chain:
   155   "\<lbrakk>chain Y; compact (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. max_in_chain i Y"
   156 apply (drule (1) compactD2, simp)
   157 apply (erule exE, rule_tac x=i in exI)
   158 apply (rule max_in_chainI)
   159 apply (rule below_antisym)
   160 apply (erule (1) chain_mono)
   161 apply (erule (1) below_trans [OF is_ub_thelub])
   162 done
   163 
   164 text {* admissibility and compactness *}
   165 
   166 lemma adm_compact_not_below [simp]:
   167   "\<lbrakk>compact k; cont (\<lambda>x. t x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. k \<notsqsubseteq> t x)"
   168 unfolding compact_def by (rule adm_subst)
   169 
   170 lemma adm_neq_compact [simp]:
   171   "\<lbrakk>compact k; cont (\<lambda>x. t x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. t x \<noteq> k)"
   172 by (simp add: po_eq_conv)
   173 
   174 lemma adm_compact_neq [simp]:
   175   "\<lbrakk>compact k; cont (\<lambda>x. t x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. k \<noteq> t x)"
   176 by (simp add: po_eq_conv)
   177 
   178 lemma compact_bottom [simp, intro]: "compact \<bottom>"
   179 by (rule compactI, simp)
   180 
   181 text {* Any upward-closed predicate is admissible. *}
   182 
   183 lemma adm_upward:
   184   assumes P: "\<And>x y. \<lbrakk>P x; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> P y"
   185   shows "adm P"
   186 by (rule admI, drule spec, erule P, erule is_ub_thelub)
   187 
   188 lemmas adm_lemmas =
   189   adm_const adm_conj adm_all adm_ball adm_disj adm_imp adm_iff
   190   adm_below adm_eq adm_not_below
   191   adm_compact_not_below adm_compact_neq adm_neq_compact
   192 
   193 end