Theory LList_Topology

```(*  Title:      LList_Topology.thy
Author:     Stefan Friedrich
Maintainer: Stefan Friedrich
*)

section ‹The topology of llists›

theory LList_Topology
imports Topology "Lazy-Lists-II.LList2"
begin

subsection‹The topology of all llists›

text‹
This theory introduces the topologies of all llists, of infinite
llists, and of the non-empty llists. For all three cases it is
proved that safety properties are closed sets and that liveness
properties are dense sets. Finally, we prove in each of the the
three different topologies the respective theorem of Alpern and
Schneider \<^cite>‹"alpern85:_defin_liven"›, which states that every
property can be represented as an intersection of a safety property
and a liveness property.›

definition
ttop :: "'a set ⇒ 'a llist top" where
"ttop A = topo (⋃ s∈A⇧⋆. {suff A s})"

lemma ttop_topology [iff]: "topology (ttop A)"
by (auto simp: ttop_def)

locale suffixes =
fixes A and B
defines [simp]: "B ≡ (⋃ s∈A⇧⋆. {suff A s})"

locale trace_top = suffixes + topobase

lemma (in trace_top) open_iff [iff]:
"m open = (m ∈ topo (⋃ s∈A⇧⋆. {suff A s}))"

lemma (in trace_top) suff_open [intro!]:
"r ∈ A⇧⋆ ⟹ suff A r open"
by auto

lemma (in trace_top) ttop_carrier: "A⇧∞ = carrier"
by (auto simp: carrier_topo suff_def)

lemma (in trace_top) suff_nhd_base:
assumes unhd: "u ∈ nhds t"
and H: "⋀r. ⟦ r ∈ finpref A t; suff A r ⊆ u ⟧ ⟹ R"
shows "R"
proof-
from unhd obtain m where
uA: "u ⊆ A⇧∞" and
mopen: "m open" and
tm: "t ∈ m" and
mu: "m ⊆ u"
by (auto simp: ttop_carrier [THEN sym])
from mopen tm have
"∃r ∈ finpref A t. suff A r ⊆ m"
proof (induct "m")
case (basic a)
then obtain s where sA: "s ∈ A⇧⋆" and as: "a = suff A s" and ta: "t ∈ a"
by auto
from sA as ta have "s ∈ finpref A t" by (auto dest: suff_finpref)
thus ?case using as by auto
next case (inter a b)
then obtain r r' where
rt: "r ∈ finpref A t" and ra: "suff A r ⊆ a" and
r't: "r' ∈ finpref A t" and r'b: "suff A r' ⊆ b"
by auto
from rt r't have "r ≤ r' ∨ r' ≤ r"
by (auto simp: finpref_def dest: pref_locally_linear)
thus ?case
proof
assume "r ≤ r'"
hence "suff A r' ⊆ suff A r" by (rule suff_mono2)
thus ?case using r't ra r'b by auto
next assume "r' ≤ r"
hence "suff A r ⊆ suff A r'" by (rule suff_mono2)
thus ?case using rt r'b ra by auto
qed
next case (union M)
then obtain v where
"t ∈ v" and vM: "v ∈ M"
by blast
then obtain r where "r∈finpref A t" "suff A r ⊆ v" using union
by auto
thus ?case using vM by auto
qed
with mu show ?thesis by (auto intro: H)
qed

lemma (in trace_top) nhds_LNil [simp]: "nhds LNil = {A⇧∞}"
proof
show "nhds LNil ⊆ {A⇧∞}"
proof clarify
fix x assume xnhd: "x ∈ nhds LNil"
then obtain r
where rfinpref: "r ∈ finpref A LNil" and suffsub: "suff A r ⊆ x"
by (rule suff_nhd_base)
from rfinpref have "r = LNil" by auto
hence "suff A r = A⇧∞" by auto
with suffsub have "A⇧∞ ⊆ x" by auto
moreover from xnhd have "x ⊆ A⇧∞" by(auto simp: ttop_carrier elim!: nhdE)
ultimately show "x = A⇧∞" by auto
qed
next
show "{A⇧∞} ⊆ nhds LNil" by (auto simp: ttop_carrier)
qed

assumes xpoint: "x ∈ A⇧∞"
and  PA: "P ⊆ A⇧∞"
shows "(x adh P) = (∀ r ∈ finpref A x. ∃ s ∈ A⇧∞. r @@ s ∈ P)"
proof-
from PA have "⋀r. r ∈ A⇧⋆ ⟹ (∃ s ∈ A⇧∞. r @@ s ∈ P) =
(∃ s ∈ P. r ≤ s)"
by (auto simp: llist_le_def iff: lapp_allT_iff)
hence  "(∀ r ∈ finpref A x. ∃ s ∈ A⇧∞. r @@ s ∈ P) =
(∀ r ∈ finpref A x. ∃ s ∈ P. r ≤ s)"
by (auto simp: finpref_def)
also have "… = (∀ r ∈ finpref A x. suff A r ∩ P ≠ {})"
proof-
have "⋀r. (∃s∈P. r ≤ s) = ({ra. ra ∈ A⇧∞ ∧ r ≤ ra} ∩ P ≠ {})" using PA
by blast
thus ?thesis by (simp add: suff_def)
qed
also have "… = (∀ u ∈ nhds x. u ∩ P ≠ {})"
proof safe
fix r assume uP: "∀u∈nhds x. u ∩ P ≠ {}" and
rfinpref: "r ∈ finpref A x" and rP: "suff A r ∩ P = {}"
from rfinpref have "suff A r open" by (auto dest!: finpref_fin)
hence "suff A r ∈ nhds x" using xpoint rfinpref
by auto
with uP rP show "False" by auto
next
fix u assume
inter:     "∀r∈finpref A x. suff A r ∩ P ≠ {}" and
unhd:   "u ∈ nhds x" and
uinter: "u ∩ P = {}"
from unhd obtain r where
"r ∈ finpref A x" and "suff A r ⊆ u"
by (rule suff_nhd_base)
with inter uinter show "False" by auto
qed
qed

lemma (in trace_top) topology [iff]:
"topology T"

lemma (in trace_top) safety_closed_iff:
"P ⊆ A⇧∞ ⟹  safety A P = (P closed)"

lemma (in trace_top) liveness_dense_iff:
assumes P: "P ⊆ A⇧∞"
shows "liveness A P = (P dense)"
proof-
have "liveness A P = (∀r∈A⇧⋆. ∃ s ∈ A⇧∞. r @@ s ∈ P)"
also have "… = (∀x∈A⇧∞. ∀ r ∈ finpref A x. ∃ s ∈ A⇧∞. r @@ s ∈ P)"
by (auto simp: finpref_def dest: finsubsetall)
also have "… = (∀x∈A⇧∞. x adh P)" using P
also have "… = (A⇧∞ ⊆ closure P)" using P
also have "… = (P dense)"
by (simp add: liveness_def is_dense_def is_densein_def ttop_carrier)
finally show ?thesis .
qed

lemma (in trace_top) LNil_safety: "safety A {LNil}"
proof (unfold safety_def, clarify)
fix t
assume adh: "t ∈ A⇧∞" "∀r∈finpref A t. ∃s∈A⇧∞. r @@ s ∈ {LNil}"
thus "t = LNil" by (cases t)(auto simp: finpref_def)
qed

lemma (in trace_top) LNil_closed: "{LNil} closed"
by (auto intro: iffD1 [OF safety_closed_iff] LNil_safety)

theorem (in trace_top) alpern_schneider:
assumes Psub:     "P ⊆ A⇧∞"
shows "∃ S L. safety A S ∧ liveness A L ∧ P = S ∩ L"
proof-
from Psub have "P ⊆ carrier" by (simp add: ttop_carrier)
then obtain L S where
Lsub: "L ⊆ carrier" and
Ssub: "S ⊆ carrier" and
Sclosed: "S closed" and
Ldense: "L dense" and
Pinter: "P = S ∩ L"
by (blast elim: topology.ex_dense_closure_interE [OF topology])
from Ssub Sclosed have "safety A S"
moreover from Lsub Ldense have "liveness A L"
ultimately show ?thesis using Pinter
by auto
qed

subsection‹The topology of infinite llists›

definition
itop :: "'a set ⇒ 'a llist top" where
"itop A = topo (⋃ s∈A⇧⋆. {infsuff A s})"

locale infsuffixes =
fixes A and B
defines [simp]: "B ≡ (⋃ s∈A⇧⋆. {infsuff A s})"

locale itrace_top = infsuffixes + topobase

lemma (in itrace_top) open_iff [iff]:
"m open = (m ∈ topo (⋃ s∈A⇧⋆. {infsuff A s}))"

lemma (in itrace_top) topology [iff]: "topology T"
by (auto simp: T_def)

lemma (in itrace_top) infsuff_open [intro!]:
"r ∈ A⇧⋆ ⟹ infsuff A r open"
by auto

lemma (in itrace_top) itop_carrier: "carrier = A⇧ω"
by (auto simp: carrier_topo infsuff_def)

lemma itop_sub_ttop_base:
fixes A :: "'a set"
and B :: "'a llist set set"
and C :: "'a llist set set"
defines [simp]: "B ≡ ⋃s∈A⇧⋆. {suff A s}" and [simp]: "C ≡ ⋃s∈A⇧⋆. {infsuff A s}"
shows "C = (⋃ t∈B. {t ∩ ⋃C})"
by (auto simp: infsuff_def suff_def)

lemma itop_sub_ttop [folded ttop_def itop_def]:
fixes A and C and S (structure)
defines "C ≡ ⋃s∈A⇧⋆. {infsuff A s}" and "S ≡ topo C"
fixes B and T (structure)
defines "B ≡ ⋃s∈A⇧⋆. {suff A s}" and "T ≡ topo B"
shows "subtopology S T"
proof -
interpret itrace_top A C S by fact+
interpret trace_top A B T by fact+
show ?thesis
by (auto intro: itop_sub_ttop_base [THEN subtop_lemma] simp: S_def T_def)
qed

lemma (in itrace_top) infsuff_nhd_base:
assumes unhd: "u ∈ nhds t"
and H: "⋀r. ⟦ r ∈ finpref A t; infsuff A r ⊆ u ⟧ ⟹ R"
shows "R"
proof-
from unhd obtain m where
uA: "u ⊆ A⇧ω" and
mopen: "m open" and
tm: "t ∈ m" and
mu: "m ⊆ u"
by (auto simp: itop_carrier)
from mopen tm have
"∃r ∈ finpref A t. infsuff A r ⊆ m"
proof (induct "m")
case (basic a)
then obtain s where sA: "s ∈ A⇧⋆" and as: "a = infsuff A s" and ta: "t ∈ a"
by auto
from sA as ta have "s ∈ finpref A t" by (auto dest: infsuff_finpref)
thus ?case using as by auto
next case (inter a b)
then obtain r r' where
rt: "r ∈ finpref A t" and ra: "infsuff A r ⊆ a" and
r't: "r' ∈ finpref A t" and r'b: "infsuff A r' ⊆ b"
by auto
from rt r't have "r ≤ r' ∨ r' ≤ r"
by (auto simp: finpref_def dest: pref_locally_linear)
thus ?case
proof
assume "r ≤ r'"
hence "infsuff A r' ⊆ infsuff A r" by (rule infsuff_mono2)
thus ?case using r't ra r'b by auto
next assume "r' ≤ r"
hence "infsuff A r ⊆ infsuff A r'" by (rule infsuff_mono2)
thus ?case using rt r'b ra by auto
qed
next case (union M)
then obtain v where
"t ∈ v" and vM: "v ∈ M"
by blast
then obtain r where "r∈finpref A t" "infsuff A r ⊆ v" using union
by auto
thus ?case using vM by auto
qed
with mu show ?thesis by (auto intro: H)
qed

lemma (in itrace_top) hausdorff [iff]: "T2 T"
proof(rule T2I, clarify)
fix x y assume xpoint: "x ∈ carrier"
and ypoint: "y ∈ carrier"
and neq: "x ≠ y"
from xpoint ypoint have xA: "x ∈ A⇧ω" and yA: "y ∈ A⇧ω"
by (auto simp: itop_carrier)
then obtain s where
sA: "s ∈ A⇧⋆" and sx: "s ≤ x" and sy: "¬ s ≤ y" using neq
by (rule inf_neqE) auto
from neq have "y ≠ x" ..
with yA xA obtain t where
tA: "t ∈ A⇧⋆" and ty: "t ≤ y" and tx: "¬ t ≤ x"
by (rule inf_neqE) auto
let ?u = "infsuff A s" and ?v = "infsuff A t"
have inter: "?u ∩ ?v = {}"
proof (rule ccontr, auto)
fix z assume "z ∈ ?u" and "z ∈ ?v"
hence "s ≤ z" and  "t ≤ z" by (unfold infsuff_def) auto
hence "s ≤ t ∨ t ≤ s" by (rule pref_locally_linear)
thus False using sx sy tx ty by (auto dest: llist_le_trans)
qed
moreover {
from sA tA have "?u open" and "?v open"
by auto
moreover from xA yA sx ty have "x ∈ ?u" and "y ∈ ?v"
by (auto simp: infsuff_def)
ultimately have "infsuff A s ∈ nhds x" and
"infsuff A t ∈ nhds y"
by auto }
ultimately show "∃ u ∈ nhds x. ∃ v ∈ nhds y. u ∩ v = {}"
by auto
qed

corollary (in itrace_top) unique_convergence:
"⟦ x ∈ carrier;
y ∈ carrier;
F ∈ Filters ;
F ⤏ x;
F ⤏ y ⟧ ⟹ x = y"
apply (rule T2.unique_convergence)
prefer 2
apply (rule filter.intro)
apply auto
done

(*
lemma safty_closed:
fixes   A :: "'a set"
defines "T ≡ itop A"
assumes P: "P ⊆ A⇧ω"
and safety: "safety A P"
shows "P iscl T"
proof-
have istopT [iff]: "istop T" by (simp add: T_def)
have carrT [simp]: "carr T = A⇧ω" by (simp add: T_def itop_carr)
show ?thesis
proof (rule closure_eq_closed, auto)
fix x assume xclos: "x ∈ clos T P"
with P have "x ∈ carr T"
by (intro subsetD [OF closure_subset]) auto
hence xA: "x ∈ A⇧ω" by simp
moreover
have "∀ r ∈ finpref A x. ∃ s ∈ A⇧ω. r @@ s ∈ P"
proof
fix r assume "r ∈ finpref A x"
hence "x ∈ infsuff A r" and rA: "r ∈ A⇧⋆" using xA
by (auto simp: finpref_def infsuff_def)
hence "infsuff A r ∈ nhds T x" by (auto simp: T_def)
with adhx have  "infsuff A r ∩ P ≠ {}" by (elim adhCE) auto
then obtain t where "t ∈ infsuff A r" and tP: "t ∈ P" by auto
then obtain s where "s ∈ A⇧ω" and "t = r @@ s" using rA
by (auto elim!: infsuff_appE)
thus "∃ s ∈ A⇧ω. r @@ s ∈ P" using tP by auto
qed
ultimately show "x ∈ P" using safety
by (auto elim: safetyE)
qed
qed
*)
assumes xpoint: "x ∈ A⇧ω"
and  PA: "P ⊆ A⇧ω"
shows "x adh P = (∀ r ∈ finpref A x. ∃ s ∈ A⇧ω. r @@ s ∈ P)"
proof-
from PA have "⋀r. r ∈ A⇧⋆ ⟹ (∃ s ∈ A⇧ω. r @@ s ∈ P) =
(∃ s ∈ P. r ≤ s)"
by (auto simp: llist_le_def iff: lapp_infT)
hence  "(∀ r ∈ finpref A x. ∃ s ∈ A⇧ω. r @@ s ∈ P) =
(∀ r ∈ finpref A x. ∃ s ∈ P. r ≤ s)"
by (auto simp: finpref_def)
also have "… = (∀ r ∈ finpref A x. infsuff A r ∩ P ≠ {})"
proof-
have "⋀r. (∃s∈P. r ≤ s) = ({ra. ra ∈ A⇧ω ∧ r ≤ ra} ∩ P ≠ {})" using PA
by blast
thus ?thesis by (simp add: infsuff_def)
qed
also have "… = (∀ u ∈ nhds x. u ∩ P ≠ {})"
proof safe
fix r assume uP: "∀ u ∈ nhds x. u ∩ P ≠ {}" and
rfinpref: "r ∈ finpref A x" and rP: "infsuff A r ∩ P = {}"
from rfinpref have "infsuff A r open" by (auto dest!: finpref_fin)
hence "infsuff A r ∈ nhds x" using xpoint rfinpref
by auto
with uP rP show "False" by auto
next
fix u assume
inter:     "∀r∈finpref A x. infsuff A r ∩ P ≠ {}" and
unhd:   "u ∈ nhds x" and
uinter: "u ∩ P = {}"
from unhd obtain r where
"r ∈ finpref A x" and "infsuff A r ⊆ u"
by (rule infsuff_nhd_base)
with inter uinter show "False" by auto
qed
qed

lemma (in itrace_top) infsafety_closed_iff:
"P ⊆ A⇧ω ⟹  infsafety A P = (P closed)"

lemma (in itrace_top) empty:
"A = {} ⟹ T = {{}}"
proof (auto simp: T_def)
fix m x assume "m ∈ topo {{}}" and  xm: "x ∈ m"
thus False
by (induct m) auto
qed

lemma itop_empty: "itop {} = {{}}"
proof (auto simp: itop_def)
fix m x assume "m ∈ topo {{}}" and  xm: "x ∈ m"
thus False
by (induct m) auto
qed

lemma infliveness_empty:
"infliveness {} P ⟹ False"
by (auto simp: infliveness_def)

lemma (in trivial) dense:
"P dense"
by auto

lemma (in itrace_top) infliveness_dense_iff:
assumes notempty: "A ≠ {}"
and P: "P ⊆ A⇧ω"
shows "infliveness A P = (P dense)"
proof-
have "infliveness A P = (∀r∈A⇧⋆. ∃ s ∈ A⇧ω. r @@ s ∈ P)"
also have "… = (∀x∈A⇧ω. ∀ r ∈ finpref A x. ∃ s ∈ A⇧ω. r @@ s ∈ P)"
proof-
from notempty obtain a where "a ∈ A"
by auto
hence lc: "lconst a ∈ A⇧ω"
by (rule lconstT)
hence "⋀P. (∀x∈A⇧ω. ∀r∈finpref A x. P r) = (∀ r∈A⇧⋆. P r)"
proof (auto dest: finpref_fin)
fix P r  assume lc: "lconst a ∈ A⇧ω"
and Pr: "∀x∈A⇧ω. ∀r∈finpref A x. P r"
and rA: "r ∈ A⇧⋆"
from rA lc have rlc: "r @@ lconst a ∈ A⇧ω" by (rule lapp_fin_infT)
moreover from rA rlc have "r ∈ finpref A (r @@ lconst a)"
by (auto simp: finpref_def llist_le_def)
ultimately show "P r" using Pr by auto
qed
thus ?thesis by simp
qed
also have "… = (∀x∈A⇧ω. x adh P)" using P
also have "… = (A⇧ω ⊆ closure P)" using P
also have "… = (P dense)"
by (simp add: infliveness_def is_dense_def is_densein_def itop_carrier)
finally show ?thesis .
qed

theorem (in itrace_top) alpern_schneider:
assumes notempty: "A ≠ {}"
and   Psub:     "P ⊆ A⇧ω"
shows "∃ S L. infsafety A S ∧ infliveness A L ∧ P = S ∩ L"
proof-
from Psub have "P ⊆ carrier"
by (simp add: itop_carrier [THEN sym])
then obtain L S where
Lsub: "L ⊆ carrier" and
Ssub: "S ⊆ carrier" and
Sclosed: "S closed" and
Ldense: "L dense" and
Pinter: "P = S ∩ L"
by (rule topology.ex_dense_closure_interE [OF topology]) auto
from Ssub Sclosed have "infsafety A S"
moreover from notempty Lsub Ldense have "infliveness A L"
ultimately show ?thesis using Pinter
by auto
qed

subsection‹The topology of non-empty llists›

definition
ptop :: "'a set ⇒ 'a llist top" where
"ptop A ≡ topo (⋃ s∈A⇧♣. {suff A s})"

locale possuffixes =
fixes A and B
defines [simp]: "B ≡ (⋃ s∈A⇧♣. {suff A s})"

locale ptrace_top = possuffixes + topobase

lemma (in ptrace_top) open_iff [iff]:
"m open = (m ∈ topo (⋃ s∈A⇧♣. {suff A s}))"

lemma (in ptrace_top) topology [iff]: "topology T"

lemma (in ptrace_top) ptop_carrier: "carrier = A⇧♠"
by (auto simp add: carrier_topo suff_def)
(auto elim: alllsts.cases)

lemma pptop_subtop_ttop:
fixes S (structure)
fixes A and B and T (structure)
defines "B ≡ ⋃s∈A⇧⋆. {suff A s}" and "T ≡ topo B"
defines "S ≡ ⋃ t ∈ T. {t - {LNil}}"
shows "subtopology S T"
by (rule subtopology.intro, auto simp add: is_open_def S_def carr_def)

lemma pptop_top:
fixes S (structure)
fixes A and B and T (structure)
defines "B ≡ ⋃s∈A⇧⋆. {suff A s}" and "T ≡ topo B"
defines "S ≡ ⋃ t ∈ T. {t - {LNil}}"
shows  "topology (⋃ t ∈ T. {t - {LNil}})"
proof -
interpret trace_top A B T by fact+
show ?thesis
by (auto intro!: subtopology.subtop_topology [OF pptop_subtop_ttop]
trace_top.topology simp: T_def)
qed

(*
lemma
includes ptrace_top A B S
includes trace_top  A C T
fixes S' (structure)
defines  "S' ≡ (⋃ t ∈ T. {t - {LNil}})"
shows "S = S'"
proof-
have [iff]: "⋀ m. m open⇩3 = (∃t. t open⇩2 ∧ m = t - {LNil})"
by (auto simp add: S'_def is_open_def)
show ?thesis
proof
fix m assume "m open"
thus "m open⇩3"
proof (induct m)
case (basic m) thus ?case by auto
next case (inter u v) thus ?case
by (blast intro: topology.Int_open [OF pptop_top])
next case (union M) thus ?case
by (auto intro!: topology.union_open [OF pptop_top] simp: S'_def T_def)
qed
next
fix m assume "m open⇩3"
then obtain t where "t open⇩2" and mt: "m = t - {LNil}" by auto
hence "t - {LNil} open⇩1"
proof (induct t)
case (basic x)
then obtain s where sfin: "s ∈ A⇧⋆" and
ms: "x = suff A s"
by auto
thus ?case
proof (cases s)
case LNil_fin with ms
have "x - {LNil} = carrier" by (auto simp: ptop_carrier)
thus ?thesis by (auto intro!: topology.carrier_open [OF pptop_top])
next
case (LCons_fin a l) with ms show ?thesis
by (auto simp: ptop_def)
qed
next case (inter u v)
hence "(u - {LNil}) ∩ (v - {LNil}) ∈ ptop A" by auto
moreover have "(u - {LNil}) ∩ (v - {LNil}) = (u ∩ v) - {LNil}"
by auto
ultimately show ?case by auto
next case (union M)
hence "⋃{u. ∃x∈M. u = x - {LNil}} ∈ ptop A" by auto
moreover have "⋃{u. ∃x∈M. u = x - {LNil}} = ⋃M - {LNil}" by auto
ultimately show ?case by auto
qed
thus "x ∈ ptop A" using xt by auto
qed
qed
*)
lemma (in ptrace_top) suff_open [intro!]:
"r ∈ A⇧♣ ⟹ suff A r open"
by auto

lemma (in ptrace_top) suff_ptop_nhd_base:
assumes unhd: "u ∈ nhds t"
and H: "⋀r. ⟦ r ∈ pfinpref A t; suff A r ⊆ u ⟧ ⟹ R"
shows "R"
proof-
from unhd obtain m where
uA: "u ⊆ A⇧♠" and
mopen: "m open" and
tm: "t ∈ m" and
mu: "m ⊆ u"
by (auto simp: ptop_carrier)
from mopen tm have
"∃r ∈ pfinpref A t. suff A r ⊆ m"
proof (induct "m")
case (basic a)
then obtain s where sA: "s ∈ A⇧♣" and as: "a = suff A s" and ta: "t ∈ a"
by auto
from sA as ta have "s ∈ pfinpref A t"
by (auto simp: pfinpref_def dest: suff_finpref)
thus ?case using as by auto
next case (inter a b)
then obtain r r' where
rt: "r ∈ pfinpref A t" and ra: "suff A r ⊆ a" and
r't: "r' ∈ pfinpref A t" and r'b: "suff A r' ⊆ b"
by auto
from rt r't have "r ≤ r' ∨ r' ≤ r"
by (auto simp: pfinpref_def finpref_def dest: pref_locally_linear)
thus ?case
proof
assume "r ≤ r'"
hence "suff A r' ⊆ suff A r" by (rule suff_mono2)
thus ?case using r't ra r'b by auto
next assume "r' ≤ r"
hence "suff A r ⊆ suff A r'" by (rule suff_mono2)
thus ?case using rt r'b ra by auto
qed
next case (union M)
then obtain v where
"t ∈ v" and vM: "v ∈ M"
by blast
then obtain r where "r∈pfinpref A t" "suff A r ⊆ v" using union
by auto
thus ?case using vM by auto
qed
with mu show ?thesis by (auto intro: H)
qed

lemma pfinpref_LNil [simp]: "pfinpref A LNil = {}"
by (auto simp: pfinpref_def)

assumes xpoint: "x ∈ A⇧♠"
and  P_subset_A: "P ⊆ A⇧♠"
shows "x adh P = (∀ r ∈ pfinpref A x. ∃ s ∈ A⇧∞. r @@ s ∈ P)"
proof
show "∀r∈pfinpref A x. ∃s∈A⇧∞. r @@ s ∈ P"
proof
fix r let ?u = "suff A r"
assume r_pfinpref_x: "r ∈ pfinpref A x"
hence r_pos: "r ∈ A⇧♣" by (auto dest: finpref_fin)
hence "?u open" by auto
hence "?u ∈ nhds x" using xpoint r_pfinpref_x
by auto
then obtain t where tu: "t ∈ ?u" and tP: "t ∈ P"
by auto
from tu obtain s where "t = r @@ s" using r_pos
by (auto elim!: suff_appE)
with tP show "∃s∈A⇧∞. r @@ s ∈ P" using P_subset_A r_pos
by (auto iff: lapp_allT_iff)
qed
next
assume H: "∀r∈pfinpref A x. ∃s∈A⇧∞. r @@ s ∈ P"
proof
fix U assume unhd: "U ∈ nhds x"
then obtain r where r_pfinpref_x: "r ∈ pfinpref A x" and
suff_subset_U: "suff A r ⊆ U" by (elim suff_ptop_nhd_base)
from r_pfinpref_x have rpos: "r ∈ A⇧♣" by (auto intro: finpref_fin)
show "U ∩ P ≠ {}" using rpos
proof (cases r)
case (LCons a l)
hence r_pfinpref_x: "r ∈ pfinpref A x" using r_pfinpref_x
by auto
with H obtain s where sA: "s ∈ A⇧∞" and asP: "r@@s ∈ P"
by  auto
moreover have "r @@ s ∈ suff A r" using sA rpos
by (auto simp: suff_def iff: lapp_allT_iff)
ultimately show ?thesis using suff_subset_U by auto
qed
qed
qed

lemma (in ptrace_top) possafety_closed_iff:
"P ⊆ A⇧♠ ⟹  possafety A P = (P closed)"
(*
lemma ptop_empty: "ptop {} = {{}}"
proof (auto simp: ptop_def intro!: topobase.basic)
fix m x assume "m ∈ topo {}" and  xm: "x ∈ m"
thus False
by (induct m) auto
qed

lemma posliveness_empty:
"posliveness {} P"
by (auto simp: posliveness_def)
*)

lemma (in ptrace_top) posliveness_dense_iff:
assumes P: "P ⊆ A⇧♠"
shows "posliveness A P = (P dense)"
proof-
have "posliveness A P = (∀r∈A⇧♣. ∃ s ∈ A⇧∞. r @@ s ∈ P)"
also have "… = (∀x∈A⇧♠. ∀ r ∈ pfinpref A x. ∃ s ∈ A⇧∞. r @@ s ∈ P)"
by (auto simp: pfinpref_def finpref_def dest: finsubsetall)
also have "… = (∀x∈A⇧♠. x adh P)" using P
by (auto simp: adh_lemma simp del: poslsts_iff)
also have "… = (A⇧♠ ⊆ closure P)" using P
by (auto simp: adh_closure_iff ptop_carrier simp del: poslsts_iff)
also have "… = (P dense)"
by (simp add: posliveness_def is_dense_def is_densein_def ptop_carrier)
finally show ?thesis .
qed

theorem (in ptrace_top) alpern_schneider:
assumes Psub: "P ⊆ A⇧♠"
shows "∃ S L. possafety A S ∧ posliveness A L ∧ P = S ∩ L"
proof-
from Psub have "P ⊆ carrier" by (simp add: ptop_carrier)
then obtain L S where
Lsub: "L ⊆ carrier" and
Ssub: "S ⊆ carrier" and
Sclosed: "S closed" and
Ldense: "L dense" and
Pinter: "P = S ∩ L"
by (blast elim: topology.ex_dense_closure_interE [OF topology])
from Ssub Sclosed have "possafety A S"