author | huffman |
Sat, 16 Oct 2010 14:41:11 -0700 | |
changeset 40024 | a0f760ef6995 |
parent 40007 | bb04a995bbd3 |
child 40430 | 483a4876e428 |
permissions | -rw-r--r-- |
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset
|
1 |
(* Title: 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 |
text {* improved admissibility introduction *} |
f3fcfa388ecb
cleaned up; added adm_less to adm_lemmas; added subsection headings
huffman
parents:
16565
diff
changeset
|
33 |
|
f3fcfa388ecb
cleaned up; added adm_less to adm_lemmas; added subsection headings
huffman
parents:
16565
diff
changeset
|
34 |
lemma admI2: |
f3fcfa388ecb
cleaned up; added adm_less to adm_lemmas; added subsection headings
huffman
parents:
16565
diff
changeset
|
35 |
"(\<And>Y. \<lbrakk>chain Y; \<forall>i. P (Y i); \<forall>i. \<exists>j>i. Y i \<noteq> Y j \<and> Y i \<sqsubseteq> Y j\<rbrakk> |
f3fcfa388ecb
cleaned up; added adm_less to adm_lemmas; added subsection headings
huffman
parents:
16565
diff
changeset
|
36 |
\<Longrightarrow> P (\<Squnion>i. Y i)) \<Longrightarrow> adm P" |
f3fcfa388ecb
cleaned up; added adm_less to adm_lemmas; added subsection headings
huffman
parents:
16565
diff
changeset
|
37 |
apply (rule admI) |
f3fcfa388ecb
cleaned up; added adm_less to adm_lemmas; added subsection headings
huffman
parents:
16565
diff
changeset
|
38 |
apply (erule (1) increasing_chain_adm_lemma) |
f3fcfa388ecb
cleaned up; added adm_less to adm_lemmas; added subsection headings
huffman
parents:
16565
diff
changeset
|
39 |
apply fast |
f3fcfa388ecb
cleaned up; added adm_less to adm_lemmas; added subsection headings
huffman
parents:
16565
diff
changeset
|
40 |
done |
f3fcfa388ecb
cleaned up; added adm_less to adm_lemmas; added subsection headings
huffman
parents:
16565
diff
changeset
|
41 |
|
f3fcfa388ecb
cleaned up; added adm_less to adm_lemmas; added subsection headings
huffman
parents:
16565
diff
changeset
|
42 |
subsection {* Admissibility on chain-finite types *} |
f3fcfa388ecb
cleaned up; added adm_less to adm_lemmas; added subsection headings
huffman
parents:
16565
diff
changeset
|
43 |
|
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset
|
44 |
text {* for chain-finite (easy) types every formula is admissible *} |
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset
|
45 |
|
25921 | 46 |
lemma adm_chfin: "adm (P::'a::chfin \<Rightarrow> bool)" |
47 |
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
|
48 |
|
16623
f3fcfa388ecb
cleaned up; added adm_less to adm_lemmas; added subsection headings
huffman
parents:
16565
diff
changeset
|
49 |
subsection {* Admissibility of special formulae and propagation *} |
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset
|
50 |
|
40007 | 51 |
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
|
52 |
by (rule admI, simp) |
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset
|
53 |
|
40007 | 54 |
lemma adm_conj [simp]: |
55 |
"\<lbrakk>adm (\<lambda>x. P x); adm (\<lambda>x. Q x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<and> Q x)" |
|
25925 | 56 |
by (fast intro: admI elim: admD) |
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset
|
57 |
|
40007 | 58 |
lemma adm_all [simp]: |
59 |
"(\<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
|
60 |
by (fast intro: admI elim: admD) |
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset
|
61 |
|
40007 | 62 |
lemma adm_ball [simp]: |
63 |
"(\<And>y. y \<in> A \<Longrightarrow> adm (\<lambda>x. P x y)) \<Longrightarrow> adm (\<lambda>x. \<forall>y\<in>A. P x y)" |
|
17586 | 64 |
by (fast intro: admI elim: admD) |
65 |
||
40007 | 66 |
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
|
67 |
|
40007 | 68 |
lemma adm_disj_lemma1: |
69 |
assumes adm: "adm P" |
|
70 |
assumes chain: "chain Y" |
|
71 |
assumes P: "\<forall>i. \<exists>j\<ge>i. P (Y j)" |
|
72 |
shows "P (\<Squnion>i. Y i)" |
|
73 |
proof - |
|
74 |
def f \<equiv> "\<lambda>i. LEAST j. i \<le> j \<and> P (Y j)" |
|
75 |
have chain': "chain (\<lambda>i. Y (f i))" |
|
76 |
unfolding f_def |
|
77 |
apply (rule chainI) |
|
78 |
apply (rule chain_mono [OF chain]) |
|
79 |
apply (rule Least_le) |
|
80 |
apply (rule LeastI2_ex) |
|
81 |
apply (simp_all add: P) |
|
82 |
done |
|
83 |
have f1: "\<And>i. i \<le> f i" and f2: "\<And>i. P (Y (f i))" |
|
84 |
using LeastI_ex [OF P [rule_format]] by (simp_all add: f_def) |
|
85 |
have lub_eq: "(\<Squnion>i. Y i) = (\<Squnion>i. Y (f i))" |
|
86 |
apply (rule below_antisym) |
|
87 |
apply (rule lub_mono [OF chain chain']) |
|
88 |
apply (rule chain_mono [OF chain f1]) |
|
89 |
apply (rule lub_range_mono [OF _ chain chain']) |
|
90 |
apply clarsimp |
|
91 |
done |
|
92 |
show "P (\<Squnion>i. Y i)" |
|
93 |
unfolding lub_eq using adm chain' f2 by (rule admD) |
|
94 |
qed |
|
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset
|
95 |
|
40007 | 96 |
lemma adm_disj_lemma2: |
17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset
|
97 |
"\<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
|
98 |
apply (erule contrapos_pp) |
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset
|
99 |
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
|
100 |
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
|
101 |
apply simp |
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset
|
102 |
done |
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset
|
103 |
|
40007 | 104 |
lemma adm_disj [simp]: |
105 |
"\<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
|
106 |
apply (rule admI) |
40007 | 107 |
apply (erule adm_disj_lemma2 [THEN disjE]) |
108 |
apply (erule (2) adm_disj_lemma1 [THEN disjI1]) |
|
109 |
apply (erule (2) adm_disj_lemma1 [THEN disjI2]) |
|
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset
|
110 |
done |
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset
|
111 |
|
40007 | 112 |
lemma adm_imp [simp]: |
113 |
"\<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
|
114 |
by (subst imp_conv_disj, rule adm_disj) |
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset
|
115 |
|
40007 | 116 |
lemma adm_iff [simp]: |
16565 | 117 |
"\<lbrakk>adm (\<lambda>x. P x \<longrightarrow> Q x); adm (\<lambda>x. Q x \<longrightarrow> P x)\<rbrakk> |
118 |
\<Longrightarrow> adm (\<lambda>x. P x = Q x)" |
|
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset
|
119 |
by (subst iff_conv_conj_imp, rule adm_conj) |
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset
|
120 |
|
17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset
|
121 |
text {* admissibility and continuity *} |
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset
|
122 |
|
40007 | 123 |
lemma adm_below [simp]: |
124 |
"\<lbrakk>cont (\<lambda>x. u x); cont (\<lambda>x. v x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x \<sqsubseteq> v x)" |
|
17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset
|
125 |
apply (rule admI) |
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset
|
126 |
apply (simp add: cont2contlubE) |
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset
|
127 |
apply (rule lub_mono) |
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset
|
128 |
apply (erule (1) ch2ch_cont) |
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset
|
129 |
apply (erule (1) ch2ch_cont) |
25923 | 130 |
apply (erule spec) |
17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset
|
131 |
done |
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset
|
132 |
|
40007 | 133 |
lemma adm_eq [simp]: |
134 |
"\<lbrakk>cont (\<lambda>x. u x); cont (\<lambda>x. v x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x = v x)" |
|
135 |
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
|
136 |
|
40007 | 137 |
lemma adm_subst: "\<lbrakk>cont (\<lambda>x. t x); adm P\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P (t x))" |
17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset
|
138 |
apply (rule admI) |
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset
|
139 |
apply (simp add: cont2contlubE) |
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset
|
140 |
apply (erule admD) |
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset
|
141 |
apply (erule (1) ch2ch_cont) |
25925 | 142 |
apply (erule spec) |
17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset
|
143 |
done |
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset
|
144 |
|
40007 | 145 |
lemma adm_not_below [simp]: "cont (\<lambda>x. t x) \<Longrightarrow> adm (\<lambda>x. \<not> t x \<sqsubseteq> u)" |
146 |
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
|
147 |
|
25880 | 148 |
subsection {* Compactness *} |
149 |
||
150 |
definition |
|
151 |
compact :: "'a::cpo \<Rightarrow> bool" where |
|
152 |
"compact k = adm (\<lambda>x. \<not> k \<sqsubseteq> x)" |
|
153 |
||
154 |
lemma compactI: "adm (\<lambda>x. \<not> k \<sqsubseteq> x) \<Longrightarrow> compact k" |
|
155 |
unfolding compact_def . |
|
156 |
||
157 |
lemma compactD: "compact k \<Longrightarrow> adm (\<lambda>x. \<not> k \<sqsubseteq> x)" |
|
158 |
unfolding compact_def . |
|
159 |
||
160 |
lemma compactI2: |
|
27413 | 161 |
"(\<And>Y. \<lbrakk>chain Y; x \<sqsubseteq> (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. x \<sqsubseteq> Y i) \<Longrightarrow> compact x" |
25880 | 162 |
unfolding compact_def adm_def by fast |
163 |
||
164 |
lemma compactD2: |
|
27413 | 165 |
"\<lbrakk>compact x; chain Y; x \<sqsubseteq> (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. x \<sqsubseteq> Y i" |
25880 | 166 |
unfolding compact_def adm_def by fast |
167 |
||
39969 | 168 |
lemma compact_below_lub_iff: |
169 |
"\<lbrakk>compact x; chain Y\<rbrakk> \<Longrightarrow> x \<sqsubseteq> (\<Squnion>i. Y i) \<longleftrightarrow> (\<exists>i. x \<sqsubseteq> Y i)" |
|
170 |
by (fast intro: compactD2 elim: below_trans is_ub_thelub) |
|
171 |
||
25880 | 172 |
lemma compact_chfin [simp]: "compact (x::'a::chfin)" |
173 |
by (rule compactI [OF adm_chfin]) |
|
174 |
||
175 |
lemma compact_imp_max_in_chain: |
|
176 |
"\<lbrakk>chain Y; compact (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. max_in_chain i Y" |
|
177 |
apply (drule (1) compactD2, simp) |
|
178 |
apply (erule exE, rule_tac x=i in exI) |
|
179 |
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
|
180 |
apply (rule below_antisym) |
25922
cb04d05e95fb
rename lemma chain_mono3 -> chain_mono, chain_mono -> chain_mono_less
huffman
parents:
25921
diff
changeset
|
181 |
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
|
182 |
apply (erule (1) below_trans [OF is_ub_thelub]) |
25880 | 183 |
done |
184 |
||
17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset
|
185 |
text {* admissibility and compactness *} |
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset
|
186 |
|
40007 | 187 |
lemma adm_compact_not_below [simp]: |
188 |
"\<lbrakk>compact k; cont (\<lambda>x. t x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. \<not> k \<sqsubseteq> t x)" |
|
25880 | 189 |
unfolding compact_def by (rule adm_subst) |
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset
|
190 |
|
40007 | 191 |
lemma adm_neq_compact [simp]: |
192 |
"\<lbrakk>compact k; cont (\<lambda>x. t x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. t x \<noteq> k)" |
|
193 |
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
|
194 |
|
40007 | 195 |
lemma adm_compact_neq [simp]: |
196 |
"\<lbrakk>compact k; cont (\<lambda>x. t x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. k \<noteq> t x)" |
|
197 |
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
|
198 |
|
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset
|
199 |
lemma compact_UU [simp, intro]: "compact \<bottom>" |
40007 | 200 |
by (rule compactI, simp) |
17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset
|
201 |
|
25802 | 202 |
text {* Any upward-closed predicate is admissible. *} |
203 |
||
204 |
lemma adm_upward: |
|
205 |
assumes P: "\<And>x y. \<lbrakk>P x; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> P y" |
|
206 |
shows "adm P" |
|
207 |
by (rule admI, drule spec, erule P, erule is_ub_thelub) |
|
208 |
||
40007 | 209 |
lemmas adm_lemmas = |
210 |
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
|
211 |
adm_below adm_eq adm_not_below |
40007 | 212 |
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
|
213 |
|
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset
|
214 |
end |