(* 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