src/HOLCF/Adm.thy
author huffman
Sat, 04 Jun 2005 00:22:08 +0200
changeset 16221 879400e029bf
parent 16207 d67baef02f78
child 16565 00a3bf006881
permissions -rw-r--r--
New theory with lemmas for the fixrec package
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
16056
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
     1
(*  Title:      HOLCF/Adm.thy
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
     2
    ID:         $Id$
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
     3
    Author:     Franz Regensburger
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
     4
*)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
     5
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
     6
header {* Admissibility *}
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
     7
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
     8
theory Adm
16079
757e1c4a8081 moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun
huffman
parents: 16070
diff changeset
     9
imports Cont
16056
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    10
begin
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    11
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    12
defaultsort cpo
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    13
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    14
subsection {* Definitions *}
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    15
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    16
consts
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    17
adm		:: "('a::cpo=>bool)=>bool"
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    18
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    19
defs
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    20
adm_def:       "adm P == !Y. chain(Y) --> 
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    21
                        (!i. P(Y i)) --> P(lub(range Y))"
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    22
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    23
subsection {* Admissibility and fixed point induction *}
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    24
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    25
text {* access to definitions *}
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    26
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    27
lemma admI:
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    28
   "(!!Y. [| chain Y; !i. P (Y i) |] ==> P (lub (range Y))) ==> adm P"
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    29
apply (unfold adm_def)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    30
apply blast
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    31
done
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    32
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    33
lemma triv_admI: "!x. P x ==> adm P"
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    34
apply (rule admI)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    35
apply (erule spec)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    36
done
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    37
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    38
lemma admD: "[| adm(P); chain(Y); !i. P(Y(i)) |] ==> P(lub(range(Y)))"
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    39
apply (unfold adm_def)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    40
apply blast
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    41
done
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    42
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    43
text {* for chain-finite (easy) types every formula is admissible *}
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    44
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    45
lemma adm_max_in_chain: 
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    46
"!Y. chain(Y::nat=>'a) --> (? n. max_in_chain n Y) ==> adm(P::'a=>bool)"
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    47
apply (unfold adm_def)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    48
apply (intro strip)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    49
apply (rule exE)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    50
apply (rule mp)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    51
apply (erule spec)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    52
apply assumption
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    53
apply (subst lub_finch1 [THEN thelubI])
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    54
apply assumption
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    55
apply assumption
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    56
apply (erule spec)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    57
done
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    58
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    59
lemmas adm_chfin = chfin [THEN adm_max_in_chain, standard]
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    60
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    61
text {* improved admissibility introduction *}
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    62
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    63
lemma admI2:
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    64
 "(!!Y. [| chain Y; !i. P (Y i); !i. ? j. i < j & Y i ~= Y j & Y i << Y j |] 
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    65
  ==> P(lub (range Y))) ==> adm P"
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    66
apply (unfold adm_def)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    67
apply (intro strip)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    68
apply (erule increasing_chain_adm_lemma)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    69
apply assumption
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    70
apply fast
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    71
done
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    72
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    73
text {* admissibility of special formulae and propagation *}
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    74
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    75
lemma adm_less [simp]: "[|cont u;cont v|]==> adm(%x. u x << v x)"
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    76
apply (unfold adm_def)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    77
apply (intro strip)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    78
apply (frule_tac f = "u" in cont2mono [THEN ch2ch_monofun])
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    79
apply assumption
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    80
apply (frule_tac f = "v" in cont2mono [THEN ch2ch_monofun])
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    81
apply assumption
16207
d67baef02f78 changed to work with new contlubE rule
huffman
parents: 16079
diff changeset
    82
apply (erule cont2contlub [THEN contlubE, THEN ssubst])
16056
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    83
apply assumption
16207
d67baef02f78 changed to work with new contlubE rule
huffman
parents: 16079
diff changeset
    84
apply (erule cont2contlub [THEN contlubE, THEN ssubst])
16056
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    85
apply assumption
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    86
apply (blast intro: lub_mono)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    87
done
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    88
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    89
lemma adm_conj [simp]: "[| adm P; adm Q |] ==> adm(%x. P x & Q x)"
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    90
by (fast elim: admD intro: admI)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    91
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    92
lemma adm_not_free [simp]: "adm(%x. t)"
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    93
apply (unfold adm_def)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    94
apply fast
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    95
done
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    96
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    97
lemma adm_not_less: "cont t ==> adm(%x.~ (t x) << u)"
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    98
apply (unfold adm_def)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    99
apply (intro strip)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   100
apply (rule contrapos_nn)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   101
apply (erule spec)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   102
apply (rule trans_less)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   103
prefer 2 apply (assumption)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   104
apply (erule cont2mono [THEN monofun_fun_arg])
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   105
apply (rule is_ub_thelub)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   106
apply assumption
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   107
done
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   108
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   109
lemma adm_all: "!y. adm(P y) ==> adm(%x.!y. P y x)"
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   110
by (fast intro: admI elim: admD)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   111
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   112
lemmas adm_all2 = allI [THEN adm_all, standard]
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   113
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   114
lemma adm_subst: "[|cont t; adm P|] ==> adm(%x. P (t x))"
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   115
apply (rule admI)
16207
d67baef02f78 changed to work with new contlubE rule
huffman
parents: 16079
diff changeset
   116
apply (simplesubst cont2contlub [THEN contlubE])
16056
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   117
apply assumption
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   118
apply assumption
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   119
apply (erule admD)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   120
apply (erule cont2mono [THEN ch2ch_monofun])
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   121
apply assumption
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   122
apply assumption
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   123
done
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   124
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   125
lemma adm_UU_not_less: "adm(%x.~ UU << t(x))"
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   126
by simp
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   127
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   128
lemma adm_not_UU: "cont(t)==> adm(%x.~ (t x) = UU)"
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   129
apply (unfold adm_def)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   130
apply (intro strip)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   131
apply (rule contrapos_nn)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   132
apply (erule spec)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   133
apply (rule chain_UU_I [THEN spec])
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   134
apply (erule cont2mono [THEN ch2ch_monofun])
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   135
apply assumption
16207
d67baef02f78 changed to work with new contlubE rule
huffman
parents: 16079
diff changeset
   136
apply (erule cont2contlub [THEN contlubE, THEN subst])
16056
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   137
apply assumption
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   138
apply assumption
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   139
done
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   140
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   141
lemma adm_eq: "[|cont u ; cont v|]==> adm(%x. u x = v x)"
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   142
by (simp add: po_eq_conv)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   143
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   144
text {* admissibility for disjunction is hard to prove. It takes 7 Lemmas *}
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   145
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   146
lemma adm_disj_lemma1:
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   147
  "\<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)"
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   148
apply (erule contrapos_pp)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   149
apply clarsimp
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   150
apply (rule exI)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   151
apply (rule conjI)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   152
apply (drule spec, erule mp)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   153
apply (rule le_maxI1)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   154
apply (drule spec, erule mp)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   155
apply (rule le_maxI2)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   156
done
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   157
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   158
lemma adm_disj_lemma2: "[| adm P; \<exists>X. chain X & (!n. P(X n)) & 
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   159
      lub(range Y)=lub(range X)|] ==> P(lub(range Y))"
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   160
by (force elim: admD)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   161
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   162
lemma adm_disj_lemma3: 
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   163
  "[| chain(Y::nat=>'a::cpo); \<forall>i. \<exists>j\<ge>i. P (Y j) |] ==> 
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   164
            chain(%m. Y (LEAST j. m\<le>j \<and> P(Y j)))"
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   165
apply (rule chainI)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   166
apply (erule chain_mono3)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   167
apply (rule Least_le)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   168
apply (rule conjI)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   169
apply (rule Suc_leD)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   170
apply (erule allE)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   171
apply (erule exE)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   172
apply (erule LeastI [THEN conjunct1])
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   173
apply (erule allE)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   174
apply (erule exE)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   175
apply (erule LeastI [THEN conjunct2])
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   176
done
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   177
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   178
lemma adm_disj_lemma4: 
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   179
  "[| \<forall>i. \<exists>j\<ge>i. P (Y j) |] ==> ! m. P(Y(LEAST j::nat. m\<le>j & P(Y j)))"
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   180
apply (rule allI)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   181
apply (erule allE)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   182
apply (erule exE)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   183
apply (erule LeastI [THEN conjunct2])
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   184
done
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   185
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   186
lemma adm_disj_lemma5: 
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   187
  "[| chain(Y::nat=>'a::cpo); \<forall>i. \<exists>j\<ge>i. P(Y j) |] ==> 
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   188
            lub(range(Y)) = (LUB m. Y(LEAST j. m\<le>j & P(Y j)))"
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   189
 apply (rule antisym_less)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   190
  apply (rule lub_mono)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   191
    apply assumption
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   192
   apply (erule adm_disj_lemma3)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   193
   apply assumption
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   194
  apply (rule allI)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   195
  apply (erule chain_mono3)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   196
  apply (erule allE)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   197
  apply (erule exE)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   198
  apply (erule LeastI [THEN conjunct1])
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   199
 apply (rule lub_mono3)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   200
   apply (erule adm_disj_lemma3)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   201
   apply assumption
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   202
  apply assumption
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   203
 apply (rule allI)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   204
 apply (rule exI)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   205
 apply (rule refl_less)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   206
done
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   207
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   208
lemma adm_disj_lemma6:
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   209
  "[| chain(Y::nat=>'a::cpo); \<forall>i. \<exists>j\<ge>i. P(Y j) |] ==> 
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   210
            \<exists>X. chain X & (\<forall>n. P(X n)) & lub(range Y) = lub(range X)"
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   211
apply (rule_tac x = "%m. Y (LEAST j. m\<le>j & P (Y j))" in exI)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   212
apply (fast intro!: adm_disj_lemma3 adm_disj_lemma4 adm_disj_lemma5)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   213
done
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   214
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   215
lemma adm_disj_lemma7:
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   216
"[| adm(P); chain(Y); \<forall>i. \<exists>j\<ge>i. P(Y j) |]==>P(lub(range(Y)))"
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   217
apply (erule adm_disj_lemma2)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   218
apply (erule adm_disj_lemma6)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   219
apply assumption
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   220
done
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   221
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   222
lemma adm_disj: "[| adm P; adm Q |] ==> adm(%x. P x | Q x)"
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   223
apply (rule admI)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   224
apply (erule adm_disj_lemma1 [THEN disjE])
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   225
apply (rule disjI1)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   226
apply (erule adm_disj_lemma7)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   227
apply assumption
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   228
apply assumption
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   229
apply (rule disjI2)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   230
apply (erule adm_disj_lemma7)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   231
apply assumption
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   232
apply assumption
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   233
done
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   234
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   235
lemma adm_imp: "[| adm(%x.~(P x)); adm Q |] ==> adm(%x. P x --> Q x)"
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   236
by (subst imp_conv_disj, rule adm_disj)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   237
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   238
lemma adm_iff: "[| adm (%x. P x --> Q x); adm (%x. Q x --> P x) |]  
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   239
            ==> adm (%x. P x = Q x)"
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   240
by (subst iff_conv_conj_imp, rule adm_conj)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   241
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   242
lemma adm_not_conj: "[| adm (%x. ~ P x); adm (%x. ~ Q x) |] ==> adm (%x. ~ (P x & Q x))"
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   243
by (subst de_Morgan_conj, rule adm_disj)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   244
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   245
lemmas adm_lemmas = adm_not_free adm_imp adm_disj adm_eq adm_not_UU
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   246
        adm_UU_not_less adm_all2 adm_not_less adm_not_conj adm_iff
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   247
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   248
declare adm_lemmas [simp]
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   249
16062
f8110bd9957f cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents: 16056
diff changeset
   250
(* legacy ML bindings *)
f8110bd9957f cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents: 16056
diff changeset
   251
ML
f8110bd9957f cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents: 16056
diff changeset
   252
{*
f8110bd9957f cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents: 16056
diff changeset
   253
val adm_def = thm "adm_def";
f8110bd9957f cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents: 16056
diff changeset
   254
val admI = thm "admI";
f8110bd9957f cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents: 16056
diff changeset
   255
val triv_admI = thm "triv_admI";
f8110bd9957f cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents: 16056
diff changeset
   256
val admD = thm "admD";
f8110bd9957f cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents: 16056
diff changeset
   257
val adm_max_in_chain = thm "adm_max_in_chain";
f8110bd9957f cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents: 16056
diff changeset
   258
val adm_chfin = thm "adm_chfin";
f8110bd9957f cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents: 16056
diff changeset
   259
val admI2 = thm "admI2";
f8110bd9957f cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents: 16056
diff changeset
   260
val adm_less = thm "adm_less";
f8110bd9957f cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents: 16056
diff changeset
   261
val adm_conj = thm "adm_conj";
f8110bd9957f cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents: 16056
diff changeset
   262
val adm_not_free = thm "adm_not_free";
f8110bd9957f cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents: 16056
diff changeset
   263
val adm_not_less = thm "adm_not_less";
f8110bd9957f cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents: 16056
diff changeset
   264
val adm_all = thm "adm_all";
f8110bd9957f cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents: 16056
diff changeset
   265
val adm_all2 = thm "adm_all2";
f8110bd9957f cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents: 16056
diff changeset
   266
val adm_subst = thm "adm_subst";
f8110bd9957f cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents: 16056
diff changeset
   267
val adm_UU_not_less = thm "adm_UU_not_less";
f8110bd9957f cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents: 16056
diff changeset
   268
val adm_not_UU = thm "adm_not_UU";
f8110bd9957f cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents: 16056
diff changeset
   269
val adm_eq = thm "adm_eq";
f8110bd9957f cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents: 16056
diff changeset
   270
val adm_disj_lemma1 = thm "adm_disj_lemma1";
f8110bd9957f cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents: 16056
diff changeset
   271
val adm_disj_lemma2 = thm "adm_disj_lemma2";
f8110bd9957f cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents: 16056
diff changeset
   272
val adm_disj_lemma3 = thm "adm_disj_lemma3";
f8110bd9957f cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents: 16056
diff changeset
   273
val adm_disj_lemma4 = thm "adm_disj_lemma4";
f8110bd9957f cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents: 16056
diff changeset
   274
val adm_disj_lemma5 = thm "adm_disj_lemma5";
f8110bd9957f cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents: 16056
diff changeset
   275
val adm_disj_lemma6 = thm "adm_disj_lemma6";
f8110bd9957f cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents: 16056
diff changeset
   276
val adm_disj_lemma7 = thm "adm_disj_lemma7";
f8110bd9957f cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents: 16056
diff changeset
   277
val adm_disj = thm "adm_disj";
f8110bd9957f cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents: 16056
diff changeset
   278
val adm_imp = thm "adm_imp";
f8110bd9957f cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents: 16056
diff changeset
   279
val adm_iff = thm "adm_iff";
f8110bd9957f cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents: 16056
diff changeset
   280
val adm_not_conj = thm "adm_not_conj";
f8110bd9957f cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents: 16056
diff changeset
   281
val adm_lemmas = [adm_not_free, adm_imp, adm_disj, adm_eq, adm_not_UU,
f8110bd9957f cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents: 16056
diff changeset
   282
        adm_UU_not_less, adm_all2, adm_not_less, adm_not_conj, adm_iff]
f8110bd9957f cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents: 16056
diff changeset
   283
*}
f8110bd9957f cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents: 16056
diff changeset
   284
16056
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   285
end
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   286