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