1 (* Title: HOLCF/CompactBasis.thy |
|
2 Author: Brian Huffman |
|
3 *) |
|
4 |
|
5 header {* A compact basis for powerdomains *} |
|
6 |
|
7 theory CompactBasis |
|
8 imports Bifinite |
|
9 begin |
|
10 |
|
11 default_sort "domain" |
|
12 |
|
13 subsection {* A compact basis for powerdomains *} |
|
14 |
|
15 typedef 'a pd_basis = |
|
16 "{S::'a compact_basis set. finite S \<and> S \<noteq> {}}" |
|
17 by (rule_tac x="{arbitrary}" in exI, simp) |
|
18 |
|
19 lemma finite_Rep_pd_basis [simp]: "finite (Rep_pd_basis u)" |
|
20 by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp |
|
21 |
|
22 lemma Rep_pd_basis_nonempty [simp]: "Rep_pd_basis u \<noteq> {}" |
|
23 by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp |
|
24 |
|
25 text {* The powerdomain basis type is countable. *} |
|
26 |
|
27 lemma pd_basis_countable: "\<exists>f::'a pd_basis \<Rightarrow> nat. inj f" |
|
28 proof - |
|
29 obtain g :: "'a compact_basis \<Rightarrow> nat" where "inj g" |
|
30 using compact_basis.countable .. |
|
31 hence image_g_eq: "\<And>A B. g ` A = g ` B \<longleftrightarrow> A = B" |
|
32 by (rule inj_image_eq_iff) |
|
33 have "inj (\<lambda>t. set_encode (g ` Rep_pd_basis t))" |
|
34 by (simp add: inj_on_def set_encode_eq image_g_eq Rep_pd_basis_inject) |
|
35 thus ?thesis by - (rule exI) |
|
36 (* FIXME: why doesn't ".." or "by (rule exI)" work? *) |
|
37 qed |
|
38 |
|
39 subsection {* Unit and plus constructors *} |
|
40 |
|
41 definition |
|
42 PDUnit :: "'a compact_basis \<Rightarrow> 'a pd_basis" where |
|
43 "PDUnit = (\<lambda>x. Abs_pd_basis {x})" |
|
44 |
|
45 definition |
|
46 PDPlus :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> 'a pd_basis" where |
|
47 "PDPlus t u = Abs_pd_basis (Rep_pd_basis t \<union> Rep_pd_basis u)" |
|
48 |
|
49 lemma Rep_PDUnit: |
|
50 "Rep_pd_basis (PDUnit x) = {x}" |
|
51 unfolding PDUnit_def by (rule Abs_pd_basis_inverse) (simp add: pd_basis_def) |
|
52 |
|
53 lemma Rep_PDPlus: |
|
54 "Rep_pd_basis (PDPlus u v) = Rep_pd_basis u \<union> Rep_pd_basis v" |
|
55 unfolding PDPlus_def by (rule Abs_pd_basis_inverse) (simp add: pd_basis_def) |
|
56 |
|
57 lemma PDUnit_inject [simp]: "(PDUnit a = PDUnit b) = (a = b)" |
|
58 unfolding Rep_pd_basis_inject [symmetric] Rep_PDUnit by simp |
|
59 |
|
60 lemma PDPlus_assoc: "PDPlus (PDPlus t u) v = PDPlus t (PDPlus u v)" |
|
61 unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_assoc) |
|
62 |
|
63 lemma PDPlus_commute: "PDPlus t u = PDPlus u t" |
|
64 unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_commute) |
|
65 |
|
66 lemma PDPlus_absorb: "PDPlus t t = t" |
|
67 unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_absorb) |
|
68 |
|
69 lemma pd_basis_induct1: |
|
70 assumes PDUnit: "\<And>a. P (PDUnit a)" |
|
71 assumes PDPlus: "\<And>a t. P t \<Longrightarrow> P (PDPlus (PDUnit a) t)" |
|
72 shows "P x" |
|
73 apply (induct x, unfold pd_basis_def, clarify) |
|
74 apply (erule (1) finite_ne_induct) |
|
75 apply (cut_tac a=x in PDUnit) |
|
76 apply (simp add: PDUnit_def) |
|
77 apply (drule_tac a=x in PDPlus) |
|
78 apply (simp add: PDUnit_def PDPlus_def |
|
79 Abs_pd_basis_inverse [unfolded pd_basis_def]) |
|
80 done |
|
81 |
|
82 lemma pd_basis_induct: |
|
83 assumes PDUnit: "\<And>a. P (PDUnit a)" |
|
84 assumes PDPlus: "\<And>t u. \<lbrakk>P t; P u\<rbrakk> \<Longrightarrow> P (PDPlus t u)" |
|
85 shows "P x" |
|
86 apply (induct x rule: pd_basis_induct1) |
|
87 apply (rule PDUnit, erule PDPlus [OF PDUnit]) |
|
88 done |
|
89 |
|
90 subsection {* Fold operator *} |
|
91 |
|
92 definition |
|
93 fold_pd :: |
|
94 "('a compact_basis \<Rightarrow> 'b::type) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a pd_basis \<Rightarrow> 'b" |
|
95 where "fold_pd g f t = fold1 f (g ` Rep_pd_basis t)" |
|
96 |
|
97 lemma fold_pd_PDUnit: |
|
98 assumes "class.ab_semigroup_idem_mult f" |
|
99 shows "fold_pd g f (PDUnit x) = g x" |
|
100 unfolding fold_pd_def Rep_PDUnit by simp |
|
101 |
|
102 lemma fold_pd_PDPlus: |
|
103 assumes "class.ab_semigroup_idem_mult f" |
|
104 shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)" |
|
105 proof - |
|
106 interpret ab_semigroup_idem_mult f by fact |
|
107 show ?thesis unfolding fold_pd_def Rep_PDPlus |
|
108 by (simp add: image_Un fold1_Un2) |
|
109 qed |
|
110 |
|
111 end |
|