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