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