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