author  huffman 
Wed, 06 Oct 2010 10:49:27 0700  
changeset 39974  b525988432e9 
parent 39967  1c6dce3ef477 
child 39981  fdff0444fa7d 
permissions  rwrr 
25904  1 
(* Title: HOLCF/CompactBasis.thy 
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 

7 
theory CompactBasis 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

8 
imports Algebraic 
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 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

11 
default_sort sfp 
25904  12 

13 
subsection {* A compact basis for powerdomains *} 

14 

15 
typedef 'a pd_basis = 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

16 
"{S::'a compact_basis set. finite S \<and> S \<noteq> {}}" 
25904  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 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

25 
text {* The powerdomain basis type is countable. *} 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

26 

b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

27 
lemma pd_basis_countable: "\<exists>f::'a::sfp pd_basis \<Rightarrow> nat. inj f" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

28 
proof  
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

29 
obtain g :: "'a compact_basis \<Rightarrow> nat" where "inj g" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

30 
using compact_basis.countable .. 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

31 
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

32 
by (rule inj_image_eq_iff) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

33 
have "inj (\<lambda>t. set_encode (g ` Rep_pd_basis t))" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

34 
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

35 
thus ?thesis by  (rule exI) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

36 
(* FIXME: why doesn't ".." or "by (rule exI)" work? *) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

37 
qed 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

38 

b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

39 
subsection {* Unit and plus constructors *} 
25904  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) 

35901
12f09bf2c77f
fix LaTeX overfull hbox warnings in HOLCF document
huffman
parents:
31076
diff
changeset

78 
apply (simp add: PDUnit_def PDPlus_def 
12f09bf2c77f
fix LaTeX overfull hbox warnings in HOLCF document
huffman
parents:
31076
diff
changeset

79 
Abs_pd_basis_inverse [unfolded pd_basis_def]) 
25904  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 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

90 
subsection {* Fold operator *} 
25904  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 

26927  97 
lemma fold_pd_PDUnit: 
36635
080b755377c0
locale predicates of classes carry a mandatory "class" prefix
haftmann
parents:
36452
diff
changeset

98 
assumes "class.ab_semigroup_idem_mult f" 
26927  99 
shows "fold_pd g f (PDUnit x) = g x" 
25904  100 
unfolding fold_pd_def Rep_PDUnit by simp 
101 

26927  102 
lemma fold_pd_PDPlus: 
36635
080b755377c0
locale predicates of classes carry a mandatory "class" prefix
haftmann
parents:
36452
diff
changeset

103 
assumes "class.ab_semigroup_idem_mult f" 
26927  104 
shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)" 
28611  105 
proof  
29511
7071b017cb35
migrated class package to new locale implementation
haftmann
parents:
29252
diff
changeset

106 
interpret ab_semigroup_idem_mult f by fact 
35901
12f09bf2c77f
fix LaTeX overfull hbox warnings in HOLCF document
huffman
parents:
31076
diff
changeset

107 
show ?thesis unfolding fold_pd_def Rep_PDPlus 
12f09bf2c77f
fix LaTeX overfull hbox warnings in HOLCF document
huffman
parents:
31076
diff
changeset

108 
by (simp add: image_Un fold1_Un2) 
28611  109 
qed 
25904  110 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

111 
subsection {* Lemmas for proving ifandonlyif inequalities *} 
25904  112 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

113 
lemma chain_max_below_iff: 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

114 
assumes Y: "chain Y" shows "Y (max i j) \<sqsubseteq> x \<longleftrightarrow> Y i \<sqsubseteq> x \<and> Y j \<sqsubseteq> x" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

115 
apply auto 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

116 
apply (erule below_trans [OF chain_mono [OF Y le_maxI1]]) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

117 
apply (erule below_trans [OF chain_mono [OF Y le_maxI2]]) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

118 
apply (simp add: max_def) 
25904  119 
done 
120 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

121 
lemma all_ex_below_disj_iff: 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

122 
assumes "chain X" and "chain Y" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

123 
shows "(\<forall>i. \<exists>j. X i \<sqsubseteq> Z j \<or> Y i \<sqsubseteq> Z j) \<longleftrightarrow> 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

124 
(\<forall>i. \<exists>j. X i \<sqsubseteq> Z j) \<or> (\<forall>i. \<exists>j. Y i \<sqsubseteq> Z j)" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

125 
by (metis chain_max_below_iff assms) 
25904  126 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

127 
lemma all_ex_below_conj_iff: 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

128 
assumes "chain X" and "chain Y" and "chain Z" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

129 
shows "(\<forall>i. \<exists>j. X i \<sqsubseteq> Z j \<and> Y i \<sqsubseteq> Z j) \<longleftrightarrow> 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

130 
(\<forall>i. \<exists>j. X i \<sqsubseteq> Z j) \<and> (\<forall>i. \<exists>j. Y i \<sqsubseteq> Z j)" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

131 
oops 
25904  132 

133 
end 