Theory LList_Topology

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

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}))"
  by (simp add: T_def is_open_def)

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

lemma (in trace_top) adh_lemma:
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
  finally show ?thesis by (simp add: adhs_def)
qed

lemma (in trace_top) topology [iff]:
  "topology T"
by (simp add: T_def)

lemma (in trace_top) safety_closed_iff:
  "P ⊆ A⇧∞ ⟹  safety A P = (P closed)"
by (auto simp: safety_def topology.closed_adh adh_lemma ttop_carrier)

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)"
    by (simp add: liveness_def)
  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
    by (simp add: adh_lemma)
  also have "… = (A⇧∞ ⊆ closure P)" using P
    by (auto simp: adh_closure_iff ttop_carrier)
  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"
    by (simp add: safety_closed_iff ttop_carrier)
  moreover from Lsub Ldense have "liveness A L"
    by (simp add: liveness_dense_iff ttop_carrier)
  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}))"
  by (simp add: T_def is_open_def)

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 
    from P xclos have adhx: "adh T P x" by (auto intro!: closure_imp_adh)
    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
*)
lemma (in itrace_top) adh_lemma:
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
  finally show ?thesis by (simp add: adhs_def)
qed

lemma (in itrace_top) infsafety_closed_iff:
  "P ⊆ A⇧ω ⟹  infsafety A P = (P closed)"
  by (auto simp: infsafety_def topology.closed_adh adh_lemma itop_carrier)

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)"
    by (simp add: infliveness_def)
  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
    by (simp add: adh_lemma)
  also have "… = (A⇧ω ⊆ closure P)" using P
    by (auto simp: adh_closure_iff itop_carrier)
  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"
    by (simp add: infsafety_closed_iff itop_carrier)
  moreover from notempty Lsub Ldense have "infliveness A L"
    by (simp add: infliveness_dense_iff itop_carrier)
  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}))"
  by (simp add: T_def is_open_def)

lemma (in ptrace_top) topology [iff]: "topology T"
  by (simp add: T_def)

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)

lemma (in ptrace_top) adh_lemma:
  assumes xpoint: "x ∈ A⇧♠"
  and  P_subset_A: "P ⊆ A⇧♠"
  shows "x adh P = (∀ r ∈ pfinpref A x. ∃ s ∈ A⇧∞. r @@ s ∈ P)"
proof
  assume adh_x: "x adh P"
  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
    with adh_x have  "?u ∩ P ≠ {}" by (auto elim!:adhCE)
    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"
  show "x adh 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)"
  by (auto simp: possafety_def topology.closed_adh ptop_carrier adh_lemma)
(*
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)"
    by (simp add: posliveness_def)
  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"
    by (simp add: possafety_closed_iff ptop_carrier)
  moreover from Lsub Ldense have "posliveness A L"
    by (simp add: posliveness_dense_iff ptop_carrier)
  ultimately show ?thesis using Pinter
    by auto
qed

end