equal
deleted
inserted
replaced
10 |
10 |
11 default_sort bifinite |
11 default_sort bifinite |
12 |
12 |
13 subsection {* A compact basis for powerdomains *} |
13 subsection {* A compact basis for powerdomains *} |
14 |
14 |
15 typedef 'a pd_basis = |
15 definition "pd_basis = {S::'a compact_basis set. finite S \<and> S \<noteq> {}}" |
16 "{S::'a compact_basis set. finite S \<and> S \<noteq> {}}" |
16 |
17 by (rule_tac x="{arbitrary}" in exI, simp) |
17 typedef (open) 'a pd_basis = "pd_basis :: 'a compact_basis set set" |
|
18 unfolding pd_basis_def |
|
19 apply (rule_tac x="{arbitrary}" in exI) |
|
20 apply simp |
|
21 done |
18 |
22 |
19 lemma finite_Rep_pd_basis [simp]: "finite (Rep_pd_basis u)" |
23 lemma finite_Rep_pd_basis [simp]: "finite (Rep_pd_basis u)" |
20 by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp |
24 by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp |
21 |
25 |
22 lemma Rep_pd_basis_nonempty [simp]: "Rep_pd_basis u \<noteq> {}" |
26 lemma Rep_pd_basis_nonempty [simp]: "Rep_pd_basis u \<noteq> {}" |