1(*  Title:      HOL/HOLCF/Adm.thy
2    Author:     Franz Regensburger and Brian Huffman
3*)
4
5section \<open>Admissibility and compactness\<close>
6
7theory Adm
8  imports Cont
9begin
10
11default_sort cpo
12
13subsection \<open>Definitions\<close>
14
15definition adm :: "('a::cpo \<Rightarrow> bool) \<Rightarrow> bool"
16  where "adm P \<longleftrightarrow> (\<forall>Y. chain Y \<longrightarrow> (\<forall>i. P (Y i)) \<longrightarrow> P (\<Squnion>i. Y i))"
17
18lemma admI: "(\<And>Y. \<lbrakk>chain Y; \<forall>i. P (Y i)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)) \<Longrightarrow> adm P"
19  unfolding adm_def by fast
20
21lemma admD: "adm P \<Longrightarrow> chain Y \<Longrightarrow> (\<And>i. P (Y i)) \<Longrightarrow> P (\<Squnion>i. Y i)"
22  unfolding adm_def by fast
23
24lemma admD2: "adm (\<lambda>x. \<not> P x) \<Longrightarrow> chain Y \<Longrightarrow> P (\<Squnion>i. Y i) \<Longrightarrow> \<exists>i. P (Y i)"
25  unfolding adm_def by fast
26
27lemma triv_admI: "\<forall>x. P x \<Longrightarrow> adm P"
28  by (rule admI) (erule spec)
29
30
31subsection \<open>Admissibility on chain-finite types\<close>
32
33text \<open>For chain-finite (easy) types every formula is admissible.\<close>
34
35lemma adm_chfin [simp]: "adm P"
36  for P :: "'a::chfin \<Rightarrow> bool"
37  by (rule admI, frule chfin, auto simp add: maxinch_is_thelub)
38
39
40subsection \<open>Admissibility of special formulae and propagation\<close>
41
42lemma adm_const [simp]: "adm (\<lambda>x. t)"
43  by (rule admI, simp)
44
45lemma adm_conj [simp]: "adm (\<lambda>x. P x) \<Longrightarrow> adm (\<lambda>x. Q x) \<Longrightarrow> adm (\<lambda>x. P x \<and> Q x)"
46  by (fast intro: admI elim: admD)
47
48lemma adm_all [simp]: "(\<And>y. adm (\<lambda>x. P x y)) \<Longrightarrow> adm (\<lambda>x. \<forall>y. P x y)"
49  by (fast intro: admI elim: admD)
50
51lemma adm_ball [simp]: "(\<And>y. y \<in> A \<Longrightarrow> adm (\<lambda>x. P x y)) \<Longrightarrow> adm (\<lambda>x. \<forall>y\<in>A. P x y)"
52  by (fast intro: admI elim: admD)
53
54text \<open>Admissibility for disjunction is hard to prove. It requires 2 lemmas.\<close>
55
56lemma adm_disj_lemma1:
57  assumes adm: "adm P"
58  assumes chain: "chain Y"
59  assumes P: "\<forall>i. \<exists>j\<ge>i. P (Y j)"
60  shows "P (\<Squnion>i. Y i)"
61proof -
62  define f where "f i = (LEAST j. i \<le> j \<and> P (Y j))" for i
63  have chain': "chain (\<lambda>i. Y (f i))"
64    unfolding f_def
65    apply (rule chainI)
66    apply (rule chain_mono [OF chain])
67    apply (rule Least_le)
68    apply (rule LeastI2_ex)
69     apply (simp_all add: P)
70    done
71  have f1: "\<And>i. i \<le> f i" and f2: "\<And>i. P (Y (f i))"
72    using LeastI_ex [OF P [rule_format]] by (simp_all add: f_def)
73  have lub_eq: "(\<Squnion>i. Y i) = (\<Squnion>i. Y (f i))"
74    apply (rule below_antisym)
75     apply (rule lub_mono [OF chain chain'])
76     apply (rule chain_mono [OF chain f1])
77    apply (rule lub_range_mono [OF _ chain chain'])
78    apply clarsimp
79    done
80  show "P (\<Squnion>i. Y i)"
81    unfolding lub_eq using adm chain' f2 by (rule admD)
82qed
83
84lemma adm_disj_lemma2: "\<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)"
85  apply (erule contrapos_pp)
86  apply (clarsimp, rename_tac a b)
87  apply (rule_tac x="max a b" in exI)
88  apply simp
89  done
90
91lemma adm_disj [simp]: "adm (\<lambda>x. P x) \<Longrightarrow> adm (\<lambda>x. Q x) \<Longrightarrow> adm (\<lambda>x. P x \<or> Q x)"
92  apply (rule admI)
93  apply (erule adm_disj_lemma2 [THEN disjE])
94   apply (erule (2) adm_disj_lemma1 [THEN disjI1])
95  apply (erule (2) adm_disj_lemma1 [THEN disjI2])
96  done
97
98lemma adm_imp [simp]: "adm (\<lambda>x. \<not> P x) \<Longrightarrow> adm (\<lambda>x. Q x) \<Longrightarrow> adm (\<lambda>x. P x \<longrightarrow> Q x)"
99  by (subst imp_conv_disj) (rule adm_disj)
100
101lemma adm_iff [simp]: "adm (\<lambda>x. P x \<longrightarrow> Q x) \<Longrightarrow> adm (\<lambda>x. Q x \<longrightarrow> P x) \<Longrightarrow> adm (\<lambda>x. P x \<longleftrightarrow> Q x)"
102  by (subst iff_conv_conj_imp) (rule adm_conj)
103
104text \<open>admissibility and continuity\<close>
105
106lemma adm_below [simp]: "cont (\<lambda>x. u x) \<Longrightarrow> cont (\<lambda>x. v x) \<Longrightarrow> adm (\<lambda>x. u x \<sqsubseteq> v x)"
107  by (simp add: adm_def cont2contlubE lub_mono ch2ch_cont)
108
109lemma adm_eq [simp]: "cont (\<lambda>x. u x) \<Longrightarrow> cont (\<lambda>x. v x) \<Longrightarrow> adm (\<lambda>x. u x = v x)"
110  by (simp add: po_eq_conv)
111
112lemma adm_subst: "cont (\<lambda>x. t x) \<Longrightarrow> adm P \<Longrightarrow> adm (\<lambda>x. P (t x))"
113  by (simp add: adm_def cont2contlubE ch2ch_cont)
114
115lemma adm_not_below [simp]: "cont (\<lambda>x. t x) \<Longrightarrow> adm (\<lambda>x. t x \<notsqsubseteq> u)"
116  by (rule admI) (simp add: cont2contlubE ch2ch_cont lub_below_iff)
117
118
119subsection \<open>Compactness\<close>
120
121definition compact :: "'a::cpo \<Rightarrow> bool"
122  where "compact k = adm (\<lambda>x. k \<notsqsubseteq> x)"
123
124lemma compactI: "adm (\<lambda>x. k \<notsqsubseteq> x) \<Longrightarrow> compact k"
125  unfolding compact_def .
126
127lemma compactD: "compact k \<Longrightarrow> adm (\<lambda>x. k \<notsqsubseteq> x)"
128  unfolding compact_def .
129
130lemma compactI2: "(\<And>Y. \<lbrakk>chain Y; x \<sqsubseteq> (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. x \<sqsubseteq> Y i) \<Longrightarrow> compact x"
131  unfolding compact_def adm_def by fast
132
133lemma compactD2: "compact x \<Longrightarrow> chain Y \<Longrightarrow> x \<sqsubseteq> (\<Squnion>i. Y i) \<Longrightarrow> \<exists>i. x \<sqsubseteq> Y i"
134  unfolding compact_def adm_def by fast
135
136lemma compact_below_lub_iff: "compact x \<Longrightarrow> chain Y \<Longrightarrow> x \<sqsubseteq> (\<Squnion>i. Y i) \<longleftrightarrow> (\<exists>i. x \<sqsubseteq> Y i)"
137  by (fast intro: compactD2 elim: below_lub)
138
139lemma compact_chfin [simp]: "compact x"
140  for x :: "'a::chfin"
141  by (rule compactI [OF adm_chfin])
142
143lemma compact_imp_max_in_chain: "chain Y \<Longrightarrow> compact (\<Squnion>i. Y i) \<Longrightarrow> \<exists>i. max_in_chain i Y"
144  apply (drule (1) compactD2, simp)
145  apply (erule exE, rule_tac x=i in exI)
146  apply (rule max_in_chainI)
147  apply (rule below_antisym)
148   apply (erule (1) chain_mono)
149  apply (erule (1) below_trans [OF is_ub_thelub])
150  done
151
152text \<open>admissibility and compactness\<close>
153
154lemma adm_compact_not_below [simp]:
155  "compact k \<Longrightarrow> cont (\<lambda>x. t x) \<Longrightarrow> adm (\<lambda>x. k \<notsqsubseteq> t x)"
156  unfolding compact_def by (rule adm_subst)
157
158lemma adm_neq_compact [simp]: "compact k \<Longrightarrow> cont (\<lambda>x. t x) \<Longrightarrow> adm (\<lambda>x. t x \<noteq> k)"
159  by (simp add: po_eq_conv)
160
161lemma adm_compact_neq [simp]: "compact k \<Longrightarrow> cont (\<lambda>x. t x) \<Longrightarrow> adm (\<lambda>x. k \<noteq> t x)"
162  by (simp add: po_eq_conv)
163
164lemma compact_bottom [simp, intro]: "compact \<bottom>"
165  by (rule compactI) simp
166
167text \<open>Any upward-closed predicate is admissible.\<close>
168
169lemma adm_upward:
170  assumes P: "\<And>x y. \<lbrakk>P x; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> P y"
171  shows "adm P"
172  by (rule admI, drule spec, erule P, erule is_ub_thelub)
173
174lemmas adm_lemmas =
175  adm_const adm_conj adm_all adm_ball adm_disj adm_imp adm_iff
176  adm_below adm_eq adm_not_below
177  adm_compact_not_below adm_compact_neq adm_neq_compact
178
179end
180