imports Stream
```(*  Title:      HOL/HOLCF/FOCUS/Stream_adm.thy
Author:     David von Oheimb, TU Muenchen
*)

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)"

(* ----------------------------------------------------------------------- *)

"⟦Porder.chain Y; ∀i. P (Y i);
⋀Y. ⟦Porder.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

"⟦Porder.chain Y;  ∀i. P (Y i); ⋀Y. ⟦Porder.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 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

assumes 1: "Porder.chain Y"
assumes 2: "∀i. P (Y i)"
assumes 3: "(⋀Y. [| Porder.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. [| Porder.chain Y; ∀i. P (Y i);
∀k. ∃j. enat k < #((Y j)::'a::flat stream)|] ==> P(LUB i. Y i))|]==> adm P"
apply (intro strip)
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 (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

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

"⋀X. [|∀i x y. x << y ⟶ y ∈ (F ^^ i) top ⟶ x ∈ (F ^^ i) top; inf_continuous F |]
==> adm (λu. ¬ u ∈ gfp F)"
apply (fast dest!: is_ub_thelub)
done

section "antitonP"

lemma antitonPD: "[| antitonP P; y ∈ P; x<<y |] ==> x ∈ P"
apply (unfold antitonP_def)
apply auto
done

lemma antitonPI: "∀x y. y ∈ P ⟶ x<<y --> x ∈ P ⟹ antitonP P"
apply (unfold antitonP_def)
apply (fast)
done

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} ⟹
apply (simp)
apply (rule antitonPI)
apply (drule gfp_upperbound)
apply (fast)
done

"{⨆i. Y i |Y. Porder.chain Y ∧ (∀i. Y i ∈ P)} ⊆ P ⟹ adm (λx. x∈P)"