author  haftmann 
Sun, 08 Mar 2009 15:25:29 +0100  
changeset 30376  e8cc806a3755 
parent 30328  ab47f43f7581 
child 30378  e0247e990702 
permissions  rwrr 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

1 
(* Title: HOL/Predicate.thy 
30328  2 
Author: Stefan Berghofer and Lukas Bulwahn and Florian Haftmann, TU Muenchen 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

3 
*) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

4 

30328  5 
header {* Predicates as relations and enumerations *} 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

6 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

7 
theory Predicate 
23708  8 
imports Inductive Relation 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

9 
begin 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

10 

30328  11 
notation 
12 
inf (infixl "\<sqinter>" 70) and 

13 
sup (infixl "\<squnion>" 65) and 

14 
Inf ("\<Sqinter>_" [900] 900) and 

15 
Sup ("\<Squnion>_" [900] 900) and 

16 
top ("\<top>") and 

17 
bot ("\<bottom>") 

18 

19 

20 
subsection {* Predicates as (complete) lattices *} 

21 

22 
subsubsection {* @{const sup} on @{typ bool} *} 

23 

24 
lemma sup_boolI1: 

25 
"P \<Longrightarrow> P \<squnion> Q" 

26 
by (simp add: sup_bool_eq) 

27 

28 
lemma sup_boolI2: 

29 
"Q \<Longrightarrow> P \<squnion> Q" 

30 
by (simp add: sup_bool_eq) 

31 

32 
lemma sup_boolE: 

33 
"P \<squnion> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R" 

34 
by (auto simp add: sup_bool_eq) 

35 

36 

37 
subsubsection {* Equality and Subsets *} 

22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

38 

26797
a6cb51c314f2
 Added mem_def and predicate1I in some of the proofs
berghofe
parents:
24345
diff
changeset

39 
lemma pred_equals_eq: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) = (R = S)" 
a6cb51c314f2
 Added mem_def and predicate1I in some of the proofs
berghofe
parents:
24345
diff
changeset

40 
by (simp add: mem_def) 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

41 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

42 
lemma pred_equals_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) = (\<lambda>x y. (x, y) \<in> S)) = (R = S)" 
26797
a6cb51c314f2
 Added mem_def and predicate1I in some of the proofs
berghofe
parents:
24345
diff
changeset

43 
by (simp add: expand_fun_eq mem_def) 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

44 

26797
a6cb51c314f2
 Added mem_def and predicate1I in some of the proofs
berghofe
parents:
24345
diff
changeset

45 
lemma pred_subset_eq: "((\<lambda>x. x \<in> R) <= (\<lambda>x. x \<in> S)) = (R <= S)" 
a6cb51c314f2
 Added mem_def and predicate1I in some of the proofs
berghofe
parents:
24345
diff
changeset

46 
by (simp add: mem_def) 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

47 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

48 
lemma pred_subset_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) <= (\<lambda>x y. (x, y) \<in> S)) = (R <= S)" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

49 
by fast 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

50 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

51 

30328  52 
subsubsection {* Top and bottom elements *} 
23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

53 

1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

54 
lemma top1I [intro!]: "top x" 
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

55 
by (simp add: top_fun_eq top_bool_eq) 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

56 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

57 
lemma top2I [intro!]: "top x y" 
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

58 
by (simp add: top_fun_eq top_bool_eq) 
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

59 

1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

60 
lemma bot1E [elim!]: "bot x \<Longrightarrow> P" 
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

61 
by (simp add: bot_fun_eq bot_bool_eq) 
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

62 

1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

63 
lemma bot2E [elim!]: "bot x y \<Longrightarrow> P" 
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

64 
by (simp add: bot_fun_eq bot_bool_eq) 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

65 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

66 

30328  67 
subsubsection {* The empty set *} 
23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

68 

1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

69 
lemma bot_empty_eq: "bot = (\<lambda>x. x \<in> {})" 
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

70 
by (auto simp add: expand_fun_eq) 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

71 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

72 
lemma bot_empty_eq2: "bot = (\<lambda>x y. (x, y) \<in> {})" 
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

73 
by (auto simp add: expand_fun_eq) 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

74 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

75 

30328  76 
subsubsection {* Binary union *} 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

77 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

78 
lemma sup1_iff [simp]: "sup A B x \<longleftrightarrow> A x  B x" 
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

79 
by (simp add: sup_fun_eq sup_bool_eq) 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

80 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

81 
lemma sup2_iff [simp]: "sup A B x y \<longleftrightarrow> A x y  B x y" 
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

82 
by (simp add: sup_fun_eq sup_bool_eq) 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

83 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

84 
lemma sup_Un_eq [pred_set_conv]: "sup (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)" 
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

85 
by (simp add: expand_fun_eq) 
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

86 

1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

87 
lemma sup_Un_eq2 [pred_set_conv]: "sup (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<union> S)" 
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

88 
by (simp add: expand_fun_eq) 
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

89 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

90 
lemma sup1I1 [elim?]: "A x \<Longrightarrow> sup A B x" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

91 
by simp 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

92 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

93 
lemma sup2I1 [elim?]: "A x y \<Longrightarrow> sup A B x y" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

94 
by simp 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

95 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

96 
lemma sup1I2 [elim?]: "B x \<Longrightarrow> sup A B x" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

97 
by simp 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

98 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

99 
lemma sup2I2 [elim?]: "B x y \<Longrightarrow> sup A B x y" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

100 
by simp 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

101 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

102 
text {* 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

103 
\medskip Classical introduction rule: no commitment to @{text A} vs 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

104 
@{text B}. 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

105 
*} 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

106 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

107 
lemma sup1CI [intro!]: "(~ B x ==> A x) ==> sup A B x" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

108 
by auto 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

109 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

110 
lemma sup2CI [intro!]: "(~ B x y ==> A x y) ==> sup A B x y" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

111 
by auto 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

112 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

113 
lemma sup1E [elim!]: "sup A B x ==> (A x ==> P) ==> (B x ==> P) ==> P" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

114 
by simp iprover 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

115 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

116 
lemma sup2E [elim!]: "sup A B x y ==> (A x y ==> P) ==> (B x y ==> P) ==> P" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

117 
by simp iprover 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

118 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

119 

30328  120 
subsubsection {* Binary intersection *} 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

121 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

122 
lemma inf1_iff [simp]: "inf A B x \<longleftrightarrow> A x \<and> B x" 
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

123 
by (simp add: inf_fun_eq inf_bool_eq) 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

124 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

125 
lemma inf2_iff [simp]: "inf A B x y \<longleftrightarrow> A x y \<and> B x y" 
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

126 
by (simp add: inf_fun_eq inf_bool_eq) 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

127 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

128 
lemma inf_Int_eq [pred_set_conv]: "inf (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)" 
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

129 
by (simp add: expand_fun_eq) 
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

130 

1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

131 
lemma inf_Int_eq2 [pred_set_conv]: "inf (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<inter> S)" 
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

132 
by (simp add: expand_fun_eq) 
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

133 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

134 
lemma inf1I [intro!]: "A x ==> B x ==> inf A B x" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

135 
by simp 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

136 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

137 
lemma inf2I [intro!]: "A x y ==> B x y ==> inf A B x y" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

138 
by simp 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

139 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

140 
lemma inf1D1: "inf A B x ==> A x" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

141 
by simp 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

142 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

143 
lemma inf2D1: "inf A B x y ==> A x y" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

144 
by simp 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

145 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

146 
lemma inf1D2: "inf A B x ==> B x" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

147 
by simp 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

148 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

149 
lemma inf2D2: "inf A B x y ==> B x y" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

150 
by simp 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

151 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

152 
lemma inf1E [elim!]: "inf A B x ==> (A x ==> B x ==> P) ==> P" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

153 
by simp 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

154 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

155 
lemma inf2E [elim!]: "inf A B x y ==> (A x y ==> B x y ==> P) ==> P" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

156 
by simp 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

157 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

158 

30328  159 
subsubsection {* Unions of families *} 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

160 

22430
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

161 
lemma SUP1_iff [simp]: "(SUP x:A. B x) b = (EX x:A. B x b)" 
24345  162 
by (simp add: SUPR_def Sup_fun_def Sup_bool_def) blast 
22430
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

163 

6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

164 
lemma SUP2_iff [simp]: "(SUP x:A. B x) b c = (EX x:A. B x b c)" 
24345  165 
by (simp add: SUPR_def Sup_fun_def Sup_bool_def) blast 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

166 

22430
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

167 
lemma SUP1_I [intro]: "a : A ==> B a b ==> (SUP x:A. B x) b" 
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

168 
by auto 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

169 

22430
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

170 
lemma SUP2_I [intro]: "a : A ==> B a b c ==> (SUP x:A. B x) b c" 
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

171 
by auto 
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

172 

6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

173 
lemma SUP1_E [elim!]: "(SUP x:A. B x) b ==> (!!x. x : A ==> B x b ==> R) ==> R" 
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

174 
by auto 
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

175 

6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

176 
lemma SUP2_E [elim!]: "(SUP x:A. B x) b c ==> (!!x. x : A ==> B x b c ==> R) ==> R" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

177 
by auto 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

178 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

179 
lemma SUP_UN_eq: "(SUP i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (UN i. r i))" 
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

180 
by (simp add: expand_fun_eq) 
22430
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

181 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

182 
lemma SUP_UN_eq2: "(SUP i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (UN i. r i))" 
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

183 
by (simp add: expand_fun_eq) 
22430
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

184 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

185 

30328  186 
subsubsection {* Intersections of families *} 
22430
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

187 

6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

188 
lemma INF1_iff [simp]: "(INF x:A. B x) b = (ALL x:A. B x b)" 
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

189 
by (simp add: INFI_def Inf_fun_def Inf_bool_def) blast 
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

190 

6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

191 
lemma INF2_iff [simp]: "(INF x:A. B x) b c = (ALL x:A. B x b c)" 
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

192 
by (simp add: INFI_def Inf_fun_def Inf_bool_def) blast 
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

193 

6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

194 
lemma INF1_I [intro!]: "(!!x. x : A ==> B x b) ==> (INF x:A. B x) b" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

195 
by auto 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

196 

22430
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

197 
lemma INF2_I [intro!]: "(!!x. x : A ==> B x b c) ==> (INF x:A. B x) b c" 
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

198 
by auto 
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

199 

6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

200 
lemma INF1_D [elim]: "(INF x:A. B x) b ==> a : A ==> B a b" 
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

201 
by auto 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

202 

22430
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

203 
lemma INF2_D [elim]: "(INF x:A. B x) b c ==> a : A ==> B a b c" 
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

204 
by auto 
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

205 

6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

206 
lemma INF1_E [elim]: "(INF x:A. B x) b ==> (B a b ==> R) ==> (a ~: A ==> R) ==> R" 
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

207 
by auto 
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

208 

6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

209 
lemma INF2_E [elim]: "(INF x:A. B x) b c ==> (B a b c ==> R) ==> (a ~: A ==> R) ==> R" 
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

210 
by auto 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

211 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

212 
lemma INF_INT_eq: "(INF i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (INT i. r i))" 
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

213 
by (simp add: expand_fun_eq) 
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

214 

1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

215 
lemma INF_INT_eq2: "(INF i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (INT i. r i))" 
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

216 
by (simp add: expand_fun_eq) 
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

217 

22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

218 

30328  219 
subsection {* Predicates as relations *} 
220 

221 
subsubsection {* Composition *} 

22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

222 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

223 
inductive 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

224 
pred_comp :: "['b => 'c => bool, 'a => 'b => bool] => 'a => 'c => bool" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

225 
(infixr "OO" 75) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

226 
for r :: "'b => 'c => bool" and s :: "'a => 'b => bool" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

227 
where 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

228 
pred_compI [intro]: "s a b ==> r b c ==> (r OO s) a c" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

229 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

230 
inductive_cases pred_compE [elim!]: "(r OO s) a c" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

231 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

232 
lemma pred_comp_rel_comp_eq [pred_set_conv]: 
23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

233 
"((\<lambda>x y. (x, y) \<in> r) OO (\<lambda>x y. (x, y) \<in> s)) = (\<lambda>x y. (x, y) \<in> r O s)" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

234 
by (auto simp add: expand_fun_eq elim: pred_compE) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

235 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

236 

30328  237 
subsubsection {* Converse *} 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

238 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

239 
inductive 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

240 
conversep :: "('a => 'b => bool) => 'b => 'a => bool" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

241 
("(_^1)" [1000] 1000) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

242 
for r :: "'a => 'b => bool" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

243 
where 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

244 
conversepI: "r a b ==> r^1 b a" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

245 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

246 
notation (xsymbols) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

247 
conversep ("(_\<inverse>\<inverse>)" [1000] 1000) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

248 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

249 
lemma conversepD: 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

250 
assumes ab: "r^1 a b" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

251 
shows "r b a" using ab 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

252 
by cases simp 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

253 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

254 
lemma conversep_iff [iff]: "r^1 a b = r b a" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

255 
by (iprover intro: conversepI dest: conversepD) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

256 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

257 
lemma conversep_converse_eq [pred_set_conv]: 
23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

258 
"(\<lambda>x y. (x, y) \<in> r)^1 = (\<lambda>x y. (x, y) \<in> r^1)" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

259 
by (auto simp add: expand_fun_eq) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

260 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

261 
lemma conversep_conversep [simp]: "(r^1)^1 = r" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

262 
by (iprover intro: order_antisym conversepI dest: conversepD) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

263 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

264 
lemma converse_pred_comp: "(r OO s)^1 = s^1 OO r^1" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

265 
by (iprover intro: order_antisym conversepI pred_compI 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

266 
elim: pred_compE dest: conversepD) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

267 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

268 
lemma converse_meet: "(inf r s)^1 = inf r^1 s^1" 
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

269 
by (simp add: inf_fun_eq inf_bool_eq) 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

270 
(iprover intro: conversepI ext dest: conversepD) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

271 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

272 
lemma converse_join: "(sup r s)^1 = sup r^1 s^1" 
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

273 
by (simp add: sup_fun_eq sup_bool_eq) 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

274 
(iprover intro: conversepI ext dest: conversepD) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

275 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

276 
lemma conversep_noteq [simp]: "(op ~=)^1 = op ~=" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

277 
by (auto simp add: expand_fun_eq) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

278 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

279 
lemma conversep_eq [simp]: "(op =)^1 = op =" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

280 
by (auto simp add: expand_fun_eq) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

281 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

282 

30328  283 
subsubsection {* Domain *} 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

284 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

285 
inductive 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

286 
DomainP :: "('a => 'b => bool) => 'a => bool" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

287 
for r :: "'a => 'b => bool" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

288 
where 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

289 
DomainPI [intro]: "r a b ==> DomainP r a" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

290 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

291 
inductive_cases DomainPE [elim!]: "DomainP r a" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

292 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

293 
lemma DomainP_Domain_eq [pred_set_conv]: "DomainP (\<lambda>x y. (x, y) \<in> r) = (\<lambda>x. x \<in> Domain r)" 
26797
a6cb51c314f2
 Added mem_def and predicate1I in some of the proofs
berghofe
parents:
24345
diff
changeset

294 
by (blast intro!: Orderings.order_antisym predicate1I) 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

295 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

296 

30328  297 
subsubsection {* Range *} 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

298 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

299 
inductive 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

300 
RangeP :: "('a => 'b => bool) => 'b => bool" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

301 
for r :: "'a => 'b => bool" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

302 
where 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

303 
RangePI [intro]: "r a b ==> RangeP r b" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

304 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

305 
inductive_cases RangePE [elim!]: "RangeP r b" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

306 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

307 
lemma RangeP_Range_eq [pred_set_conv]: "RangeP (\<lambda>x y. (x, y) \<in> r) = (\<lambda>x. x \<in> Range r)" 
26797
a6cb51c314f2
 Added mem_def and predicate1I in some of the proofs
berghofe
parents:
24345
diff
changeset

308 
by (blast intro!: Orderings.order_antisym predicate1I) 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

309 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

310 

30328  311 
subsubsection {* Inverse image *} 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

312 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

313 
definition 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

314 
inv_imagep :: "('b => 'b => bool) => ('a => 'b) => 'a => 'a => bool" where 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

315 
"inv_imagep r f == %x y. r (f x) (f y)" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

316 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

317 
lemma [pred_set_conv]: "inv_imagep (\<lambda>x y. (x, y) \<in> r) f = (\<lambda>x y. (x, y) \<in> inv_image r f)" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

318 
by (simp add: inv_image_def inv_imagep_def) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

319 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

320 
lemma in_inv_imagep [simp]: "inv_imagep r f x y = r (f x) (f y)" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

321 
by (simp add: inv_imagep_def) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

322 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

323 

30328  324 
subsubsection {* Powerset *} 
23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

325 

1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

326 
definition Powp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where 
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

327 
"Powp A == \<lambda>B. \<forall>x \<in> B. A x" 
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

328 

1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

329 
lemma Powp_Pow_eq [pred_set_conv]: "Powp (\<lambda>x. x \<in> A) = (\<lambda>x. x \<in> Pow A)" 
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

330 
by (auto simp add: Powp_def expand_fun_eq) 
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

331 

26797
a6cb51c314f2
 Added mem_def and predicate1I in some of the proofs
berghofe
parents:
24345
diff
changeset

332 
lemmas Powp_mono [mono] = Pow_mono [to_pred pred_subset_eq] 
a6cb51c314f2
 Added mem_def and predicate1I in some of the proofs
berghofe
parents:
24345
diff
changeset

333 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

334 

30328  335 
subsubsection {* Properties of relations *} 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

336 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

337 
abbreviation antisymP :: "('a => 'a => bool) => bool" where 
23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

338 
"antisymP r == antisym {(x, y). r x y}" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

339 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

340 
abbreviation transP :: "('a => 'a => bool) => bool" where 
23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

341 
"transP r == trans {(x, y). r x y}" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

342 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

343 
abbreviation single_valuedP :: "('a => 'b => bool) => bool" where 
23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

344 
"single_valuedP r == single_valued {(x, y). r x y}" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

345 

30328  346 

347 
subsection {* Predicates as enumerations *} 

348 

349 
subsubsection {* The type of predicate enumerations (a monad) *} 

350 

351 
datatype 'a pred = Pred "'a \<Rightarrow> bool" 

352 

353 
primrec eval :: "'a pred \<Rightarrow> 'a \<Rightarrow> bool" where 

354 
eval_pred: "eval (Pred f) = f" 

355 

356 
lemma Pred_eval [simp]: 

357 
"Pred (eval x) = x" 

358 
by (cases x) simp 

359 

360 
lemma eval_inject: "eval x = eval y \<longleftrightarrow> x = y" 

361 
by (cases x) auto 

362 

363 
definition single :: "'a \<Rightarrow> 'a pred" where 

364 
"single x = Pred ((op =) x)" 

365 

366 
definition bind :: "'a pred \<Rightarrow> ('a \<Rightarrow> 'b pred) \<Rightarrow> 'b pred" (infixl "\<guillemotright>=" 70) where 

367 
"P \<guillemotright>= f = Pred (\<lambda>x. (\<exists>y. eval P y \<and> eval (f y) x))" 

368 

369 
instantiation pred :: (type) complete_lattice 

370 
begin 

371 

372 
definition 

373 
"P \<le> Q \<longleftrightarrow> eval P \<le> eval Q" 

374 

375 
definition 

376 
"P < Q \<longleftrightarrow> eval P < eval Q" 

377 

378 
definition 

379 
"\<bottom> = Pred \<bottom>" 

380 

381 
definition 

382 
"\<top> = Pred \<top>" 

383 

384 
definition 

385 
"P \<sqinter> Q = Pred (eval P \<sqinter> eval Q)" 

386 

387 
definition 

388 
"P \<squnion> Q = Pred (eval P \<squnion> eval Q)" 

389 

390 
definition 

391 
"\<Sqinter>A = Pred (INFI A eval)" 

392 

393 
definition 

394 
"\<Squnion>A = Pred (SUPR A eval)" 

395 

396 
instance by default 

397 
(auto simp add: less_eq_pred_def less_pred_def 

398 
inf_pred_def sup_pred_def bot_pred_def top_pred_def 

399 
Inf_pred_def Sup_pred_def, 

400 
auto simp add: le_fun_def less_fun_def le_bool_def less_bool_def 

401 
eval_inject mem_def) 

402 

22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

403 
end 
30328  404 

405 
lemma bind_bind: 

406 
"(P \<guillemotright>= Q) \<guillemotright>= R = P \<guillemotright>= (\<lambda>x. Q x \<guillemotright>= R)" 

407 
by (auto simp add: bind_def expand_fun_eq) 

408 

409 
lemma bind_single: 

410 
"P \<guillemotright>= single = P" 

411 
by (simp add: bind_def single_def) 

412 

413 
lemma single_bind: 

414 
"single x \<guillemotright>= P = P x" 

415 
by (simp add: bind_def single_def) 

416 

417 
lemma bottom_bind: 

418 
"\<bottom> \<guillemotright>= P = \<bottom>" 

419 
by (auto simp add: bot_pred_def bind_def expand_fun_eq) 

420 

421 
lemma sup_bind: 

422 
"(P \<squnion> Q) \<guillemotright>= R = P \<guillemotright>= R \<squnion> Q \<guillemotright>= R" 

423 
by (auto simp add: bind_def sup_pred_def expand_fun_eq) 

424 

425 
lemma Sup_bind: "(\<Squnion>A \<guillemotright>= f) = \<Squnion>((\<lambda>x. x \<guillemotright>= f) ` A)" 

426 
by (auto simp add: bind_def Sup_pred_def expand_fun_eq) 

427 

428 
lemma pred_iffI: 

429 
assumes "\<And>x. eval A x \<Longrightarrow> eval B x" 

430 
and "\<And>x. eval B x \<Longrightarrow> eval A x" 

431 
shows "A = B" 

432 
proof  

433 
from assms have "\<And>x. eval A x \<longleftrightarrow> eval B x" by blast 

434 
then show ?thesis by (cases A, cases B) (simp add: expand_fun_eq) 

435 
qed 

436 

437 
lemma singleI: "eval (single x) x" 

438 
unfolding single_def by simp 

439 

440 
lemma singleI_unit: "eval (single ()) x" 

441 
by simp (rule singleI) 

442 

443 
lemma singleE: "eval (single x) y \<Longrightarrow> (y = x \<Longrightarrow> P) \<Longrightarrow> P" 

444 
unfolding single_def by simp 

445 

446 
lemma singleE': "eval (single x) y \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> P" 

447 
by (erule singleE) simp 

448 

449 
lemma bindI: "eval P x \<Longrightarrow> eval (Q x) y \<Longrightarrow> eval (P \<guillemotright>= Q) y" 

450 
unfolding bind_def by auto 

451 

452 
lemma bindE: "eval (R \<guillemotright>= Q) y \<Longrightarrow> (\<And>x. eval R x \<Longrightarrow> eval (Q x) y \<Longrightarrow> P) \<Longrightarrow> P" 

453 
unfolding bind_def by auto 

454 

455 
lemma botE: "eval \<bottom> x \<Longrightarrow> P" 

456 
unfolding bot_pred_def by auto 

457 

458 
lemma supI1: "eval A x \<Longrightarrow> eval (A \<squnion> B) x" 

459 
unfolding sup_pred_def by simp 

460 

461 
lemma supI2: "eval B x \<Longrightarrow> eval (A \<squnion> B) x" 

462 
unfolding sup_pred_def by simp 

463 

464 
lemma supE: "eval (A \<squnion> B) x \<Longrightarrow> (eval A x \<Longrightarrow> P) \<Longrightarrow> (eval B x \<Longrightarrow> P) \<Longrightarrow> P" 

465 
unfolding sup_pred_def by auto 

466 

467 

468 
subsubsection {* Derived operations *} 

469 

470 
definition if_pred :: "bool \<Rightarrow> unit pred" where 

471 
if_pred_eq: "if_pred b = (if b then single () else \<bottom>)" 

472 

473 
definition eq_pred :: "'a \<Rightarrow> 'a \<Rightarrow> unit pred" where 

474 
eq_pred_eq: "eq_pred a b = if_pred (a = b)" 

475 

476 
definition not_pred :: "unit pred \<Rightarrow> unit pred" where 

477 
not_pred_eq: "not_pred P = (if eval P () then \<bottom> else single ())" 

478 

479 
lemma if_predI: "P \<Longrightarrow> eval (if_pred P) ()" 

480 
unfolding if_pred_eq by (auto intro: singleI) 

481 

482 
lemma if_predE: "eval (if_pred b) x \<Longrightarrow> (b \<Longrightarrow> x = () \<Longrightarrow> P) \<Longrightarrow> P" 

483 
unfolding if_pred_eq by (cases b) (auto elim: botE) 

484 

485 
lemma eq_predI: "eval (eq_pred a a) ()" 

486 
unfolding eq_pred_eq if_pred_eq by (auto intro: singleI) 

487 

488 
lemma eq_predE: "eval (eq_pred a b) x \<Longrightarrow> (a = b \<Longrightarrow> x = () \<Longrightarrow> P) \<Longrightarrow> P" 

489 
unfolding eq_pred_eq by (erule if_predE) 

490 

491 
lemma not_predI: "\<not> P \<Longrightarrow> eval (not_pred (Pred (\<lambda>u. P))) ()" 

492 
unfolding not_pred_eq eval_pred by (auto intro: singleI) 

493 

494 
lemma not_predI': "\<not> eval P () \<Longrightarrow> eval (not_pred P) ()" 

495 
unfolding not_pred_eq by (auto intro: singleI) 

496 

497 
lemma not_predE: "eval (not_pred (Pred (\<lambda>u. P))) x \<Longrightarrow> (\<not> P \<Longrightarrow> thesis) \<Longrightarrow> thesis" 

498 
unfolding not_pred_eq 

499 
by (auto split: split_if_asm elim: botE) 

500 

501 
lemma not_predE': "eval (not_pred P) x \<Longrightarrow> (\<not> eval P x \<Longrightarrow> thesis) \<Longrightarrow> thesis" 

502 
unfolding not_pred_eq 

503 
by (auto split: split_if_asm elim: botE) 

504 

505 

506 
subsubsection {* Implementation *} 

507 

508 
datatype 'a seq = Empty  Insert "'a" "'a pred"  Join "'a pred" "'a seq" 

509 

510 
primrec pred_of_seq :: "'a seq \<Rightarrow> 'a pred" where 

511 
"pred_of_seq Empty = \<bottom>" 

512 
 "pred_of_seq (Insert x P) = single x \<squnion> P" 

513 
 "pred_of_seq (Join P xq) = P \<squnion> pred_of_seq xq" 

514 

515 
definition Seq :: "(unit \<Rightarrow> 'a seq) \<Rightarrow> 'a pred" where 

516 
"Seq f = pred_of_seq (f ())" 

517 

518 
code_datatype Seq 

519 

520 
primrec member :: "'a seq \<Rightarrow> 'a \<Rightarrow> bool" where 

521 
"member Empty x \<longleftrightarrow> False" 

522 
 "member (Insert y P) x \<longleftrightarrow> x = y \<or> eval P x" 

523 
 "member (Join P xq) x \<longleftrightarrow> eval P x \<or> member xq x" 

524 

525 
lemma eval_member: 

526 
"member xq = eval (pred_of_seq xq)" 

527 
proof (induct xq) 

528 
case Empty show ?case 

529 
by (auto simp add: expand_fun_eq elim: botE) 

530 
next 

531 
case Insert show ?case 

532 
by (auto simp add: expand_fun_eq elim: supE singleE intro: supI1 supI2 singleI) 

533 
next 

534 
case Join then show ?case 

535 
by (auto simp add: expand_fun_eq elim: supE intro: supI1 supI2) 

536 
qed 

537 

538 
lemma eval_code [code]: "eval (Seq f) = member (f ())" 

539 
unfolding Seq_def by (rule sym, rule eval_member) 

540 

541 
lemma single_code [code]: 

542 
"single x = Seq (\<lambda>u. Insert x \<bottom>)" 

543 
unfolding Seq_def by simp 

544 

545 
primrec "apply" :: "('a \<Rightarrow> 'b Predicate.pred) \<Rightarrow> 'a seq \<Rightarrow> 'b seq" where 

546 
"apply f Empty = Empty" 

547 
 "apply f (Insert x P) = Join (f x) (Join (P \<guillemotright>= f) Empty)" 

548 
 "apply f (Join P xq) = Join (P \<guillemotright>= f) (apply f xq)" 

549 

550 
lemma apply_bind: 

551 
"pred_of_seq (apply f xq) = pred_of_seq xq \<guillemotright>= f" 

552 
proof (induct xq) 

553 
case Empty show ?case 

554 
by (simp add: bottom_bind) 

555 
next 

556 
case Insert show ?case 

557 
by (simp add: single_bind sup_bind) 

558 
next 

559 
case Join then show ?case 

560 
by (simp add: sup_bind) 

561 
qed 

562 

563 
lemma bind_code [code]: 

564 
"Seq g \<guillemotright>= f = Seq (\<lambda>u. apply f (g ()))" 

565 
unfolding Seq_def by (rule sym, rule apply_bind) 

566 

567 
lemma bot_set_code [code]: 

568 
"\<bottom> = Seq (\<lambda>u. Empty)" 

569 
unfolding Seq_def by simp 

570 

30376  571 
primrec adjunct :: "'a pred \<Rightarrow> 'a seq \<Rightarrow> 'a seq" where 
572 
"adjunct P Empty = Join P Empty" 

573 
 "adjunct P (Insert x Q) = Insert x (Q \<squnion> P)" 

574 
 "adjunct P (Join Q xq) = Join Q (adjunct P xq)" 

575 

576 
lemma adjunct_sup: 

577 
"pred_of_seq (adjunct P xq) = P \<squnion> pred_of_seq xq" 

578 
by (induct xq) (simp_all add: sup_assoc sup_commute sup_left_commute) 

579 

30328  580 
lemma sup_code [code]: 
581 
"Seq f \<squnion> Seq g = Seq (\<lambda>u. case f () 

582 
of Empty \<Rightarrow> g () 

583 
 Insert x P \<Rightarrow> Insert x (P \<squnion> Seq g) 

30376  584 
 Join P xq \<Rightarrow> adjunct (Seq g) (Join P xq))" 
30328  585 
proof (cases "f ()") 
586 
case Empty 

587 
thus ?thesis 

30376  588 
unfolding Seq_def by (simp add: sup_commute [of "\<bottom>"] sup_bot) 
30328  589 
next 
590 
case Insert 

591 
thus ?thesis 

592 
unfolding Seq_def by (simp add: sup_assoc) 

593 
next 

594 
case Join 

595 
thus ?thesis 

30376  596 
unfolding Seq_def 
597 
by (simp add: adjunct_sup sup_assoc sup_commute sup_left_commute) 

30328  598 
qed 
599 

600 
declare eq_pred_def [code, code del] 

601 

602 
no_notation 

603 
inf (infixl "\<sqinter>" 70) and 

604 
sup (infixl "\<squnion>" 65) and 

605 
Inf ("\<Sqinter>_" [900] 900) and 

606 
Sup ("\<Squnion>_" [900] 900) and 

607 
top ("\<top>") and 

608 
bot ("\<bottom>") and 

609 
bind (infixl "\<guillemotright>=" 70) 

610 

611 
hide (open) type pred seq 

612 
hide (open) const Pred eval single bind if_pred eq_pred not_pred 

30376  613 
Empty Insert Join Seq member "apply" adjunct 
30328  614 

615 
end 