author  huffman 
Sat, 04 Jun 2005 00:22:08 +0200  
changeset 16221  879400e029bf 
parent 16207  d67baef02f78 
child 16565  00a3bf006881 
permissions  rwrr 
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 chainfinite (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  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  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  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  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 