author | sultana |
Tue, 17 Apr 2012 16:14:06 +0100 (2012-04-17) | |
changeset 47509 | 6f215c2ebd72 |
parent 45694 | 4a8743618257 |
child 49834 | b27bbb021df1 |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/Compact_Basis.thy |
25904 | 2 |
Author: Brian Huffman |
3 |
*) |
|
4 |
||
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
5 |
header {* A compact basis for powerdomains *} |
25904 | 6 |
|
41284 | 7 |
theory Compact_Basis |
41289
f655912ac235
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
huffman
parents:
41288
diff
changeset
|
8 |
imports Universal |
26420
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset
|
9 |
begin |
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset
|
10 |
|
41288
a19edebad961
powerdomain theories require class 'bifinite' instead of 'domain'
huffman
parents:
41285
diff
changeset
|
11 |
default_sort bifinite |
25904 | 12 |
|
13 |
subsection {* A compact basis for powerdomains *} |
|
14 |
||
45694
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
42151
diff
changeset
|
15 |
definition "pd_basis = {S::'a compact_basis set. finite S \<and> S \<noteq> {}}" |
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
42151
diff
changeset
|
16 |
|
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
42151
diff
changeset
|
17 |
typedef (open) 'a pd_basis = "pd_basis :: 'a compact_basis set set" |
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
42151
diff
changeset
|
18 |
unfolding pd_basis_def |
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
42151
diff
changeset
|
19 |
apply (rule_tac x="{arbitrary}" in exI) |
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
42151
diff
changeset
|
20 |
apply simp |
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
42151
diff
changeset
|
21 |
done |
25904 | 22 |
|
23 |
lemma finite_Rep_pd_basis [simp]: "finite (Rep_pd_basis u)" |
|
24 |
by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp |
|
25 |
||
26 |
lemma Rep_pd_basis_nonempty [simp]: "Rep_pd_basis u \<noteq> {}" |
|
27 |
by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp |
|
28 |
||
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
29 |
text {* The powerdomain basis type is countable. *} |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
30 |
|
39986 | 31 |
lemma pd_basis_countable: "\<exists>f::'a pd_basis \<Rightarrow> nat. inj f" |
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
32 |
proof - |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
33 |
obtain g :: "'a compact_basis \<Rightarrow> nat" where "inj g" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
34 |
using compact_basis.countable .. |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
35 |
hence image_g_eq: "\<And>A B. g ` A = g ` B \<longleftrightarrow> A = B" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
36 |
by (rule inj_image_eq_iff) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
37 |
have "inj (\<lambda>t. set_encode (g ` Rep_pd_basis t))" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
38 |
by (simp add: inj_on_def set_encode_eq image_g_eq Rep_pd_basis_inject) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
39 |
thus ?thesis by - (rule exI) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
40 |
(* FIXME: why doesn't ".." or "by (rule exI)" work? *) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
41 |
qed |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
42 |
|
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
43 |
subsection {* Unit and plus constructors *} |
25904 | 44 |
|
45 |
definition |
|
46 |
PDUnit :: "'a compact_basis \<Rightarrow> 'a pd_basis" where |
|
47 |
"PDUnit = (\<lambda>x. Abs_pd_basis {x})" |
|
48 |
||
49 |
definition |
|
50 |
PDPlus :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> 'a pd_basis" where |
|
51 |
"PDPlus t u = Abs_pd_basis (Rep_pd_basis t \<union> Rep_pd_basis u)" |
|
52 |
||
53 |
lemma Rep_PDUnit: |
|
54 |
"Rep_pd_basis (PDUnit x) = {x}" |
|
55 |
unfolding PDUnit_def by (rule Abs_pd_basis_inverse) (simp add: pd_basis_def) |
|
56 |
||
57 |
lemma Rep_PDPlus: |
|
58 |
"Rep_pd_basis (PDPlus u v) = Rep_pd_basis u \<union> Rep_pd_basis v" |
|
59 |
unfolding PDPlus_def by (rule Abs_pd_basis_inverse) (simp add: pd_basis_def) |
|
60 |
||
61 |
lemma PDUnit_inject [simp]: "(PDUnit a = PDUnit b) = (a = b)" |
|
62 |
unfolding Rep_pd_basis_inject [symmetric] Rep_PDUnit by simp |
|
63 |
||
64 |
lemma PDPlus_assoc: "PDPlus (PDPlus t u) v = PDPlus t (PDPlus u v)" |
|
65 |
unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_assoc) |
|
66 |
||
67 |
lemma PDPlus_commute: "PDPlus t u = PDPlus u t" |
|
68 |
unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_commute) |
|
69 |
||
70 |
lemma PDPlus_absorb: "PDPlus t t = t" |
|
71 |
unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_absorb) |
|
72 |
||
73 |
lemma pd_basis_induct1: |
|
74 |
assumes PDUnit: "\<And>a. P (PDUnit a)" |
|
75 |
assumes PDPlus: "\<And>a t. P t \<Longrightarrow> P (PDPlus (PDUnit a) t)" |
|
76 |
shows "P x" |
|
77 |
apply (induct x, unfold pd_basis_def, clarify) |
|
78 |
apply (erule (1) finite_ne_induct) |
|
79 |
apply (cut_tac a=x in PDUnit) |
|
80 |
apply (simp add: PDUnit_def) |
|
81 |
apply (drule_tac a=x in PDPlus) |
|
35901
12f09bf2c77f
fix LaTeX overfull hbox warnings in HOLCF document
huffman
parents:
31076
diff
changeset
|
82 |
apply (simp add: PDUnit_def PDPlus_def |
12f09bf2c77f
fix LaTeX overfull hbox warnings in HOLCF document
huffman
parents:
31076
diff
changeset
|
83 |
Abs_pd_basis_inverse [unfolded pd_basis_def]) |
25904 | 84 |
done |
85 |
||
86 |
lemma pd_basis_induct: |
|
87 |
assumes PDUnit: "\<And>a. P (PDUnit a)" |
|
88 |
assumes PDPlus: "\<And>t u. \<lbrakk>P t; P u\<rbrakk> \<Longrightarrow> P (PDPlus t u)" |
|
89 |
shows "P x" |
|
90 |
apply (induct x rule: pd_basis_induct1) |
|
91 |
apply (rule PDUnit, erule PDPlus [OF PDUnit]) |
|
92 |
done |
|
93 |
||
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
94 |
subsection {* Fold operator *} |
25904 | 95 |
|
96 |
definition |
|
97 |
fold_pd :: |
|
98 |
"('a compact_basis \<Rightarrow> 'b::type) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a pd_basis \<Rightarrow> 'b" |
|
99 |
where "fold_pd g f t = fold1 f (g ` Rep_pd_basis t)" |
|
100 |
||
26927 | 101 |
lemma fold_pd_PDUnit: |
36635
080b755377c0
locale predicates of classes carry a mandatory "class" prefix
haftmann
parents:
36452
diff
changeset
|
102 |
assumes "class.ab_semigroup_idem_mult f" |
26927 | 103 |
shows "fold_pd g f (PDUnit x) = g x" |
25904 | 104 |
unfolding fold_pd_def Rep_PDUnit by simp |
105 |
||
26927 | 106 |
lemma fold_pd_PDPlus: |
36635
080b755377c0
locale predicates of classes carry a mandatory "class" prefix
haftmann
parents:
36452
diff
changeset
|
107 |
assumes "class.ab_semigroup_idem_mult f" |
26927 | 108 |
shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)" |
28611 | 109 |
proof - |
29511
7071b017cb35
migrated class package to new locale implementation
haftmann
parents:
29252
diff
changeset
|
110 |
interpret ab_semigroup_idem_mult f by fact |
35901
12f09bf2c77f
fix LaTeX overfull hbox warnings in HOLCF document
huffman
parents:
31076
diff
changeset
|
111 |
show ?thesis unfolding fold_pd_def Rep_PDPlus |
12f09bf2c77f
fix LaTeX overfull hbox warnings in HOLCF document
huffman
parents:
31076
diff
changeset
|
112 |
by (simp add: image_Un fold1_Un2) |
28611 | 113 |
qed |
25904 | 114 |
|
115 |
end |