equal
deleted
inserted
replaced
6 |
6 |
7 theory Compact_Basis |
7 theory Compact_Basis |
8 imports Universal |
8 imports Universal |
9 begin |
9 begin |
10 |
10 |
11 default_sort bifinite |
|
12 |
|
13 |
|
14 subsection \<open>A compact basis for powerdomains\<close> |
11 subsection \<open>A compact basis for powerdomains\<close> |
15 |
12 |
16 definition "pd_basis = {S::'a compact_basis set. finite S \<and> S \<noteq> {}}" |
13 definition "pd_basis = {S::'a::bifinite compact_basis set. finite S \<and> S \<noteq> {}}" |
17 |
14 |
18 typedef 'a pd_basis = "pd_basis :: 'a compact_basis set set" |
15 typedef 'a::bifinite pd_basis = "pd_basis :: 'a compact_basis set set" |
19 unfolding pd_basis_def |
16 unfolding pd_basis_def |
20 apply (rule_tac x="{_}" in exI) |
17 apply (rule_tac x="{_}" in exI) |
21 apply simp |
18 apply simp |
22 done |
19 done |
23 |
20 |
27 lemma Rep_pd_basis_nonempty [simp]: "Rep_pd_basis u \<noteq> {}" |
24 lemma Rep_pd_basis_nonempty [simp]: "Rep_pd_basis u \<noteq> {}" |
28 by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp |
25 by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp |
29 |
26 |
30 text \<open>The powerdomain basis type is countable.\<close> |
27 text \<open>The powerdomain basis type is countable.\<close> |
31 |
28 |
32 lemma pd_basis_countable: "\<exists>f::'a pd_basis \<Rightarrow> nat. inj f" |
29 lemma pd_basis_countable: "\<exists>f::'a::bifinite pd_basis \<Rightarrow> nat. inj f" |
33 proof - |
30 proof - |
34 obtain g :: "'a compact_basis \<Rightarrow> nat" where "inj g" |
31 obtain g :: "'a compact_basis \<Rightarrow> nat" where "inj g" |
35 using compact_basis.countable .. |
32 using compact_basis.countable .. |
36 hence image_g_eq: "\<And>A B. g ` A = g ` B \<longleftrightarrow> A = B" |
33 hence image_g_eq: "\<And>A B. g ` A = g ` B \<longleftrightarrow> A = B" |
37 by (rule inj_image_eq_iff) |
34 by (rule inj_image_eq_iff) |
43 |
40 |
44 |
41 |
45 subsection \<open>Unit and plus constructors\<close> |
42 subsection \<open>Unit and plus constructors\<close> |
46 |
43 |
47 definition |
44 definition |
48 PDUnit :: "'a compact_basis \<Rightarrow> 'a pd_basis" where |
45 PDUnit :: "'a::bifinite compact_basis \<Rightarrow> 'a pd_basis" where |
49 "PDUnit = (\<lambda>x. Abs_pd_basis {x})" |
46 "PDUnit = (\<lambda>x. Abs_pd_basis {x})" |
50 |
47 |
51 definition |
48 definition |
52 PDPlus :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> 'a pd_basis" where |
49 PDPlus :: "'a::bifinite pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> 'a pd_basis" where |
53 "PDPlus t u = Abs_pd_basis (Rep_pd_basis t \<union> Rep_pd_basis u)" |
50 "PDPlus t u = Abs_pd_basis (Rep_pd_basis t \<union> Rep_pd_basis u)" |
54 |
51 |
55 lemma Rep_PDUnit: |
52 lemma Rep_PDUnit: |
56 "Rep_pd_basis (PDUnit x) = {x}" |
53 "Rep_pd_basis (PDUnit x) = {x}" |
57 unfolding PDUnit_def by (rule Abs_pd_basis_inverse) (simp add: pd_basis_def) |
54 unfolding PDUnit_def by (rule Abs_pd_basis_inverse) (simp add: pd_basis_def) |
96 |
93 |
97 subsection \<open>Fold operator\<close> |
94 subsection \<open>Fold operator\<close> |
98 |
95 |
99 definition |
96 definition |
100 fold_pd :: |
97 fold_pd :: |
101 "('a compact_basis \<Rightarrow> 'b::type) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a pd_basis \<Rightarrow> 'b" |
98 "('a::bifinite compact_basis \<Rightarrow> 'b::type) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a pd_basis \<Rightarrow> 'b" |
102 where "fold_pd g f t = semilattice_set.F f (g ` Rep_pd_basis t)" |
99 where "fold_pd g f t = semilattice_set.F f (g ` Rep_pd_basis t)" |
103 |
100 |
104 lemma fold_pd_PDUnit: |
101 lemma fold_pd_PDUnit: |
105 assumes "semilattice f" |
102 assumes "semilattice f" |
106 shows "fold_pd g f (PDUnit x) = g x" |
103 shows "fold_pd g f (PDUnit x) = g x" |