author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 41959  b460124855b8 
child 58880  0baae4311a9f 
permissions  rwrr 
41959  1 
(* Title: HOL/HOLCF/Adm.thy 
25895
0eaadfa8889e
converted adm_all and adm_ball to rule_format; cleaned up
huffman
parents:
25880
diff
changeset

2 
Author: Franz Regensburger and Brian Huffman 
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

3 
*) 
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

4 

17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

5 
header {* Admissibility and compactness *} 
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

6 

32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

7 
theory Adm 
27181  8 
imports Cont 
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

9 
begin 
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

10 

36452  11 
default_sort cpo 
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

12 

32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

13 
subsection {* Definitions *} 
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

14 

25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19440
diff
changeset

15 
definition 
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19440
diff
changeset

16 
adm :: "('a::cpo \<Rightarrow> bool) \<Rightarrow> bool" where 
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19440
diff
changeset

17 
"adm P = (\<forall>Y. chain Y \<longrightarrow> (\<forall>i. P (Y i)) \<longrightarrow> P (\<Squnion>i. Y i))" 
16056
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 
lemma admI: 
16623
f3fcfa388ecb
cleaned up; added adm_less to adm_lemmas; added subsection headings
huffman
parents:
16565
diff
changeset

20 
"(\<And>Y. \<lbrakk>chain Y; \<forall>i. P (Y i)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)) \<Longrightarrow> adm P" 
25895
0eaadfa8889e
converted adm_all and adm_ball to rule_format; cleaned up
huffman
parents:
25880
diff
changeset

21 
unfolding adm_def by fast 
0eaadfa8889e
converted adm_all and adm_ball to rule_format; cleaned up
huffman
parents:
25880
diff
changeset

22 

25925  23 
lemma admD: "\<lbrakk>adm P; chain Y; \<And>i. P (Y i)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)" 
25895
0eaadfa8889e
converted adm_all and adm_ball to rule_format; cleaned up
huffman
parents:
25880
diff
changeset

24 
unfolding adm_def by fast 
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

25 

27181  26 
lemma admD2: "\<lbrakk>adm (\<lambda>x. \<not> P x); chain Y; P (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. P (Y i)" 
27 
unfolding adm_def by fast 

28 

16565  29 
lemma triv_admI: "\<forall>x. P x \<Longrightarrow> adm P" 
17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

30 
by (rule admI, erule spec) 
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

31 

16623
f3fcfa388ecb
cleaned up; added adm_less to adm_lemmas; added subsection headings
huffman
parents:
16565
diff
changeset

32 
subsection {* Admissibility on chainfinite types *} 
f3fcfa388ecb
cleaned up; added adm_less to adm_lemmas; added subsection headings
huffman
parents:
16565
diff
changeset

33 

40623  34 
text {* For chainfinite (easy) types every formula is admissible. *} 
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

35 

40623  36 
lemma adm_chfin [simp]: "adm (P::'a::chfin \<Rightarrow> bool)" 
25921  37 
by (rule admI, frule chfin, auto simp add: maxinch_is_thelub) 
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

38 

16623
f3fcfa388ecb
cleaned up; added adm_less to adm_lemmas; added subsection headings
huffman
parents:
16565
diff
changeset

39 
subsection {* Admissibility of special formulae and propagation *} 
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

40 

40007  41 
lemma adm_const [simp]: "adm (\<lambda>x. t)" 
17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

42 
by (rule admI, simp) 
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

43 

40007  44 
lemma adm_conj [simp]: 
45 
"\<lbrakk>adm (\<lambda>x. P x); adm (\<lambda>x. Q x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<and> Q x)" 

25925  46 
by (fast intro: admI elim: admD) 
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

47 

40007  48 
lemma adm_all [simp]: 
49 
"(\<And>y. adm (\<lambda>x. P x y)) \<Longrightarrow> adm (\<lambda>x. \<forall>y. P x y)" 

16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

50 
by (fast intro: admI elim: admD) 
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

51 

40007  52 
lemma adm_ball [simp]: 
53 
"(\<And>y. y \<in> A \<Longrightarrow> adm (\<lambda>x. P x y)) \<Longrightarrow> adm (\<lambda>x. \<forall>y\<in>A. P x y)" 

17586  54 
by (fast intro: admI elim: admD) 
55 

40007  56 
text {* Admissibility for disjunction is hard to prove. It requires 2 lemmas. *} 
17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

57 

40007  58 
lemma adm_disj_lemma1: 
59 
assumes adm: "adm P" 

60 
assumes chain: "chain Y" 

61 
assumes P: "\<forall>i. \<exists>j\<ge>i. P (Y j)" 

62 
shows "P (\<Squnion>i. Y i)" 

63 
proof  

64 
def f \<equiv> "\<lambda>i. LEAST j. i \<le> j \<and> P (Y j)" 

65 
have chain': "chain (\<lambda>i. Y (f i))" 

66 
unfolding f_def 

67 
apply (rule chainI) 

68 
apply (rule chain_mono [OF chain]) 

69 
apply (rule Least_le) 

70 
apply (rule LeastI2_ex) 

71 
apply (simp_all add: P) 

72 
done 

73 
have f1: "\<And>i. i \<le> f i" and f2: "\<And>i. P (Y (f i))" 

74 
using LeastI_ex [OF P [rule_format]] by (simp_all add: f_def) 

75 
have lub_eq: "(\<Squnion>i. Y i) = (\<Squnion>i. Y (f i))" 

76 
apply (rule below_antisym) 

77 
apply (rule lub_mono [OF chain chain']) 

78 
apply (rule chain_mono [OF chain f1]) 

79 
apply (rule lub_range_mono [OF _ chain chain']) 

80 
apply clarsimp 

81 
done 

82 
show "P (\<Squnion>i. Y i)" 

83 
unfolding lub_eq using adm chain' f2 by (rule admD) 

84 
qed 

16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

85 

40007  86 
lemma adm_disj_lemma2: 
17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

87 
"\<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)" 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

88 
apply (erule contrapos_pp) 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

89 
apply (clarsimp, rename_tac a b) 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

90 
apply (rule_tac x="max a b" in exI) 
25895
0eaadfa8889e
converted adm_all and adm_ball to rule_format; cleaned up
huffman
parents:
25880
diff
changeset

91 
apply simp 
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

92 
done 
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

93 

40007  94 
lemma adm_disj [simp]: 
95 
"\<lbrakk>adm (\<lambda>x. P x); adm (\<lambda>x. Q x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<or> Q x)" 

16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

96 
apply (rule admI) 
40007  97 
apply (erule adm_disj_lemma2 [THEN disjE]) 
98 
apply (erule (2) adm_disj_lemma1 [THEN disjI1]) 

99 
apply (erule (2) adm_disj_lemma1 [THEN disjI2]) 

16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

100 
done 
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

101 

40007  102 
lemma adm_imp [simp]: 
103 
"\<lbrakk>adm (\<lambda>x. \<not> P x); adm (\<lambda>x. Q x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<longrightarrow> Q x)" 

16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

104 
by (subst imp_conv_disj, rule adm_disj) 
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

105 

40007  106 
lemma adm_iff [simp]: 
16565  107 
"\<lbrakk>adm (\<lambda>x. P x \<longrightarrow> Q x); adm (\<lambda>x. Q x \<longrightarrow> P x)\<rbrakk> 
108 
\<Longrightarrow> adm (\<lambda>x. P x = Q x)" 

16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

109 
by (subst iff_conv_conj_imp, rule adm_conj) 
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

110 

17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

111 
text {* admissibility and continuity *} 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

112 

40007  113 
lemma adm_below [simp]: 
114 
"\<lbrakk>cont (\<lambda>x. u x); cont (\<lambda>x. v x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x \<sqsubseteq> v x)" 

40435  115 
by (simp add: adm_def cont2contlubE lub_mono ch2ch_cont) 
17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

116 

40007  117 
lemma adm_eq [simp]: 
118 
"\<lbrakk>cont (\<lambda>x. u x); cont (\<lambda>x. v x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x = v x)" 

119 
by (simp add: po_eq_conv) 

17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

120 

40007  121 
lemma adm_subst: "\<lbrakk>cont (\<lambda>x. t x); adm P\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P (t x))" 
40435  122 
by (simp add: adm_def cont2contlubE ch2ch_cont) 
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

123 

41182  124 
lemma adm_not_below [simp]: "cont (\<lambda>x. t x) \<Longrightarrow> adm (\<lambda>x. t x \<notsqsubseteq> u)" 
40007  125 
by (rule admI, simp add: cont2contlubE ch2ch_cont lub_below_iff) 
17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

126 

25880  127 
subsection {* Compactness *} 
128 

129 
definition 

130 
compact :: "'a::cpo \<Rightarrow> bool" where 

41182  131 
"compact k = adm (\<lambda>x. k \<notsqsubseteq> x)" 
25880  132 

41182  133 
lemma compactI: "adm (\<lambda>x. k \<notsqsubseteq> x) \<Longrightarrow> compact k" 
25880  134 
unfolding compact_def . 
135 

41182  136 
lemma compactD: "compact k \<Longrightarrow> adm (\<lambda>x. k \<notsqsubseteq> x)" 
25880  137 
unfolding compact_def . 
138 

139 
lemma compactI2: 

27413  140 
"(\<And>Y. \<lbrakk>chain Y; x \<sqsubseteq> (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. x \<sqsubseteq> Y i) \<Longrightarrow> compact x" 
25880  141 
unfolding compact_def adm_def by fast 
142 

143 
lemma compactD2: 

27413  144 
"\<lbrakk>compact x; chain Y; x \<sqsubseteq> (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. x \<sqsubseteq> Y i" 
25880  145 
unfolding compact_def adm_def by fast 
146 

39969  147 
lemma compact_below_lub_iff: 
148 
"\<lbrakk>compact x; chain Y\<rbrakk> \<Longrightarrow> x \<sqsubseteq> (\<Squnion>i. Y i) \<longleftrightarrow> (\<exists>i. x \<sqsubseteq> Y i)" 

40500
ee9c8d36318e
add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman
parents:
40435
diff
changeset

149 
by (fast intro: compactD2 elim: below_lub) 
39969  150 

25880  151 
lemma compact_chfin [simp]: "compact (x::'a::chfin)" 
152 
by (rule compactI [OF adm_chfin]) 

153 

154 
lemma compact_imp_max_in_chain: 

155 
"\<lbrakk>chain Y; compact (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. max_in_chain i Y" 

156 
apply (drule (1) compactD2, simp) 

157 
apply (erule exE, rule_tac x=i in exI) 

158 
apply (rule max_in_chainI) 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29138
diff
changeset

159 
apply (rule below_antisym) 
25922
cb04d05e95fb
rename lemma chain_mono3 > chain_mono, chain_mono > chain_mono_less
huffman
parents:
25921
diff
changeset

160 
apply (erule (1) chain_mono) 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29138
diff
changeset

161 
apply (erule (1) below_trans [OF is_ub_thelub]) 
25880  162 
done 
163 

17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

164 
text {* admissibility and compactness *} 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

165 

40007  166 
lemma adm_compact_not_below [simp]: 
41182  167 
"\<lbrakk>compact k; cont (\<lambda>x. t x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. k \<notsqsubseteq> t x)" 
25880  168 
unfolding compact_def by (rule adm_subst) 
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

169 

40007  170 
lemma adm_neq_compact [simp]: 
171 
"\<lbrakk>compact k; cont (\<lambda>x. t x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. t x \<noteq> k)" 

172 
by (simp add: po_eq_conv) 

17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

173 

40007  174 
lemma adm_compact_neq [simp]: 
175 
"\<lbrakk>compact k; cont (\<lambda>x. t x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. k \<noteq> t x)" 

176 
by (simp add: po_eq_conv) 

17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

177 

41430
1aa23e9f2c87
change some lemma names containing 'UU' to 'bottom'
huffman
parents:
41182
diff
changeset

178 
lemma compact_bottom [simp, intro]: "compact \<bottom>" 
40007  179 
by (rule compactI, simp) 
17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

180 

25802  181 
text {* Any upwardclosed predicate is admissible. *} 
182 

183 
lemma adm_upward: 

184 
assumes P: "\<And>x y. \<lbrakk>P x; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> P y" 

185 
shows "adm P" 

186 
by (rule admI, drule spec, erule P, erule is_ub_thelub) 

187 

40007  188 
lemmas adm_lemmas = 
189 
adm_const adm_conj adm_all adm_ball adm_disj adm_imp adm_iff 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29138
diff
changeset

190 
adm_below adm_eq adm_not_below 
40007  191 
adm_compact_not_below adm_compact_neq adm_neq_compact 
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

192 

32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

193 
end 