author  haftmann 
Sat, 23 Mar 2013 20:50:39 +0100  
changeset 51489  f738e6dbd844 
parent 49834  b27bbb021df1 
child 58880  0baae4311a9f 
permissions  rwrr 
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 

49834  17 
typedef 'a pd_basis = "pd_basis :: 'a compact_basis set set" 
45694
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" 

51489  99 
where "fold_pd g f t = semilattice_set.F f (g ` Rep_pd_basis t)" 
25904  100 

26927  101 
lemma fold_pd_PDUnit: 
51489  102 
assumes "semilattice f" 
26927  103 
shows "fold_pd g f (PDUnit x) = g x" 
51489  104 
proof  
105 
from assms interpret semilattice_set f by (rule semilattice_set.intro) 

106 
show ?thesis by (simp add: fold_pd_def Rep_PDUnit) 

107 
qed 

25904  108 

26927  109 
lemma fold_pd_PDPlus: 
51489  110 
assumes "semilattice f" 
26927  111 
shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)" 
28611  112 
proof  
51489  113 
from assms interpret semilattice_set f by (rule semilattice_set.intro) 
114 
show ?thesis by (simp add: image_Un fold_pd_def Rep_PDPlus union) 

28611  115 
qed 
25904  116 

117 
end 

51489  118 