(* Title: HOL/HOLCF/FOCUS/Stream_adm.thy
Author: David von Oheimb, TU Muenchen
*)
section ‹Admissibility
for streams
›
theory Stream_adm
imports "HOLCF-Library.Stream" "HOL-Library.Order_Continuity"
begin
definition
stream_monoP ::
"(('a stream) set \ ('a stream) set) \ bool" where
"stream_monoP F = (\Q i. \P s. enat i \ #s \
(s
∈ F P) = (stream_take i
⋅s
∈ Q
∧ iterate i
⋅rt
⋅s
∈ P))
"
definition
stream_antiP ::
"(('a stream) set \ ('a stream) set) \ bool" where
"stream_antiP F = (\P x. \Q i.
(#x < enat i
⟶ (
∀y. x
⊑ y
⟶ y
∈ F P
⟶ x
∈ F P))
∧
(enat i <= #x
⟶ (
∀y. x
⊑ y
⟶
(y
∈ F P) = (stream_take i
⋅y
∈ Q
∧ iterate i
⋅rt
⋅y
∈ P))))
"
definition
antitonP ::
"'a set => bool" where
"antitonP P = (\x y. x \ y \ y\P \ x\P)"
(* ----------------------------------------------------------------------- *)
section "admissibility"
lemma infinite_chain_adm_lemma:
"\chain Y; \i. P (Y i);
∧Y.
[chain Y;
∀i. P (Y i);
¬ finite_chain Y
] ==> P (
⊔i. Y i)
]
==> P (
⊔i. Y i)
"
apply (case_tac
"finite_chain Y")
prefer 2
apply fast
apply (unfold finite_chain_def)
apply safe
apply (erule lub_finch1 [
THEN lub_eqI,
THEN ssubst])
apply assumption
apply (erule spec)
done
lemma increasing_chain_adm_lemma:
"\chain Y; \i. P (Y i); \Y. \chain Y; \i. P (Y i);
∀i.
∃j>i. Y i
≠ Y j
∧ Y i
⊑ Y j
] ==> P (
⊔i. Y i)
]
==> P (
⊔i. Y i)
"
apply (erule infinite_chain_adm_lemma)
apply assumption
apply (erule thin_rl)
apply (unfold finite_chain_def)
apply (unfold max_in_chain_def)
apply (fast dest: le_imp_less_or_eq elim: chain_mono_less)
done
lemma flatstream_adm_lemma:
assumes 1:
"chain Y"
assumes 2:
"\i. P (Y i)"
assumes 3:
"(\Y. [| chain Y; \i. P (Y i); \k. \j. enat k < #((Y j)::'a::flat stream)|]
==> P(LUB i. Y i))
"
shows "P(LUB i. Y i)"
apply (rule increasing_chain_adm_lemma [OF 1 2])
apply (erule 3, assumption)
apply (erule thin_rl)
apply (rule allI)
apply (case_tac
"\j. stream_finite (Y j)")
apply ( rule chain_incr)
apply ( rule allI)
apply ( drule spec)
apply ( safe)
apply ( rule exI)
apply ( rule slen_strict_mono)
apply ( erule spec)
apply ( assumption)
apply ( assumption)
apply (metis enat_ord_code(4) slen_infinite)
done
(* should be without reference to stream length? *)
lemma flatstream_admI:
"[|(\Y. [| chain Y; \i. P (Y i);
∀k.
∃j. enat k < #((Y j)::
'a::flat stream)|] ==> P(LUB i. Y i))|]==> adm P"
apply (unfold adm_def)
apply (intro strip)
apply (erule (1) flatstream_adm_lemma)
apply (fast)
done
(* context (theory "Extended_Nat");*)
lemma ile_lemma:
"enat (i + j) <= x ==> enat i <= x"
by (rule order_trans) auto
lemma stream_monoP2I:
"\X. stream_monoP F \ \i. \l. \x y.
enat l
≤ #x
⟶ (x::
'a::flat stream) << y --> x \ (F ^^ i) top \ y \ (F ^^ i) top"
apply (unfold stream_monoP_def)
apply (safe)
apply (rule_tac x=
"i*ia" in exI)
apply (induct_tac
"ia")
apply ( simp)
apply (simp)
apply (intro strip)
apply (erule allE, erule all_dupE, drule mp, erule ile_lemma)
apply (drule_tac P=
"%x. x" in subst, assumption)
apply (erule allE, drule mp, rule ile_lemma)
back
apply ( erule order_trans)
apply ( erule slen_mono)
apply (erule ssubst)
apply (safe)
apply ( erule (2) ile_lemma [
THEN slen_take_lemma3,
THEN subst])
apply (erule allE)
apply (drule mp)
apply ( erule slen_rt_mult)
apply (erule allE)
apply (drule mp)
apply (erule monofun_rt_mult)
apply (drule (1) mp)
apply (assumption)
done
lemma stream_monoP2_gfp_admI:
"[| \i. \l. \x y.
enat l
≤ #x
⟶ (x::
'a::flat stream) << y \ x \ (F ^^ i) top \ y \ (F ^^ i) top;
inf_continuous F |] ==> adm (λx. x
∈ gfp F)
"
apply (erule inf_continuous_gfp[of F,
THEN ssubst])
apply (simp (no_asm))
apply (rule adm_lemmas)
apply (rule flatstream_admI)
apply (erule allE)
apply (erule exE)
apply (erule allE, erule exE)
apply (erule allE, erule allE, drule mp)
(* stream_monoP *)
apply ( drule ileI1)
apply ( drule order_trans)
apply ( rule ile_eSuc)
apply ( drule eSuc_ile_mono [
THEN iffD1])
apply ( assumption)
apply (drule mp)
apply ( erule is_ub_thelub)
apply (fast)
done
lemmas fstream_gfp_admI = stream_monoP2I [
THEN stream_monoP2_gfp_admI]
lemma stream_antiP2I:
"\X. [|stream_antiP (F::(('a::flat stream)set => ('a stream set)))|]
==>
∀i x y. x << y
⟶ y
∈ (F ^^ i) top
⟶ x
∈ (F ^^ i) top
"
apply (unfold stream_antiP_def)
apply (rule allI)
apply (induct_tac
"i")
apply ( simp)
apply (simp)
apply (intro strip)
apply (erule allE, erule all_dupE, erule exE, erule exE)
apply (erule conjE)
apply (case_tac
"#x < enat i")
apply ( fast)
apply (unfold linorder_not_less)
apply (drule (1) mp)
apply (erule all_dupE, drule mp, rule below_refl)
apply (erule ssubst)
apply (erule allE, drule (1) mp)
apply (drule_tac P=
"%x. x" in subst, assumption)
apply (erule conjE, rule conjI)
apply ( erule slen_take_lemma3 [
THEN ssubst], assumption)
apply ( assumption)
apply (erule allE, erule allE, drule mp, erule monofun_rt_mult)
apply (drule (1) mp)
apply (assumption)
done
lemma stream_antiP2_non_gfp_admI:
"\X. [|\i x y. x << y \ y \ (F ^^ i) top \ x \ (F ^^ i) top; inf_continuous F |]
==> adm (λu.
¬ u
∈ gfp F)
"
apply (unfold adm_def)
apply (simp add: inf_continuous_gfp)
apply (fast dest!: is_ub_thelub)
done
lemmas fstream_non_gfp_admI = stream_antiP2I [
THEN stream_antiP2_non_gfp_admI]
(**new approach for adm********************************************************)
section "antitonP"
lemma antitonPD:
"[| antitonP P; y \ P; x< x \ P"
apply (unfold antitonP_def)
apply auto
done
lemma antitonPI:
"\x y. y \ P \ x< x \ P \ antitonP P"
apply (unfold antitonP_def)
apply (fast)
done
lemma antitonP_adm_non_P:
"antitonP P \ adm (\u. u \ P)"
apply (unfold adm_def)
apply (auto dest: antitonPD elim: is_ub_thelub)
done
lemma def_gfp_adm_nonP:
"P \ gfp F \ {y. \x::'a::pcpo. y \ x \ x \ P} \ F {y. \x. y \ x \ x \ P} \
adm (λu. u
∉P)
"
apply (simp)
apply (rule antitonP_adm_non_P)
apply (rule antitonPI)
apply (drule gfp_upperbound)
apply (fast)
done
lemma adm_set:
"{\i. Y i |Y. chain Y \ (\i. Y i \ P)} \ P \ adm (\x. x\P)"
apply (unfold adm_def)
apply (fast)
done
lemma def_gfp_admI:
"P \ gfp F \ {\i. Y i |Y. chain Y \ (\i. Y i \ P)} \
F {
⊔i. Y i |Y. chain Y
∧ (
∀i. Y i
∈ P)}
==> adm (λx. x
∈P)
"
apply (simp)
apply (rule adm_set)
apply (erule gfp_upperbound)
done
end
