author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46884  154dc6ec0041 
child 47399  b72fa7bf9a10 
permissions  rwrr 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

1 
(* Title: HOL/Predicate.thy 
46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

2 
Author: 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 

46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

5 
header {* Predicates as 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 
46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

8 
imports List 
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 
41082  12 
bot ("\<bottom>") and 
13 
top ("\<top>") and 

30328  14 
inf (infixl "\<sqinter>" 70) and 
15 
sup (infixl "\<squnion>" 65) and 

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

41082  17 
Sup ("\<Squnion>_" [900] 900) 
30328  18 

41080  19 
syntax (xsymbols) 
41082  20 
"_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10) 
21 
"_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10) 

41080  22 
"_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10) 
23 
"_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10) 

24 

46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

25 
subsection {* The type of predicate enumerations (a monad) *} 
30328  26 

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

28 

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

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

31 

32 
lemma Pred_eval [simp]: 

33 
"Pred (eval x) = x" 

34 
by (cases x) simp 

35 

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

36 
lemma pred_eqI: 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

37 
"(\<And>w. eval P w \<longleftrightarrow> eval Q w) \<Longrightarrow> P = Q" 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

38 
by (cases P, cases Q) (auto simp add: fun_eq_iff) 
30328  39 

46038
bb2f7488a0f1
conversions from sets to predicates and vice versa; extensionality on predicates
haftmann
parents:
45970
diff
changeset

40 
lemma pred_eq_iff: 
bb2f7488a0f1
conversions from sets to predicates and vice versa; extensionality on predicates
haftmann
parents:
45970
diff
changeset

41 
"P = Q \<Longrightarrow> (\<And>w. eval P w \<longleftrightarrow> eval Q w)" 
bb2f7488a0f1
conversions from sets to predicates and vice versa; extensionality on predicates
haftmann
parents:
45970
diff
changeset

42 
by (simp add: pred_eqI) 
bb2f7488a0f1
conversions from sets to predicates and vice versa; extensionality on predicates
haftmann
parents:
45970
diff
changeset

43 

44033  44 
instantiation pred :: (type) complete_lattice 
30328  45 
begin 
46 

47 
definition 

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

49 

50 
definition 

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

52 

53 
definition 

54 
"\<bottom> = Pred \<bottom>" 

55 

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

56 
lemma eval_bot [simp]: 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

57 
"eval \<bottom> = \<bottom>" 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

58 
by (simp add: bot_pred_def) 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

59 

30328  60 
definition 
61 
"\<top> = Pred \<top>" 

62 

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

63 
lemma eval_top [simp]: 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

64 
"eval \<top> = \<top>" 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

65 
by (simp add: top_pred_def) 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

66 

30328  67 
definition 
68 
"P \<sqinter> Q = Pred (eval P \<sqinter> eval Q)" 

69 

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

70 
lemma eval_inf [simp]: 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

71 
"eval (P \<sqinter> Q) = eval P \<sqinter> eval Q" 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

72 
by (simp add: inf_pred_def) 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

73 

30328  74 
definition 
75 
"P \<squnion> Q = Pred (eval P \<squnion> eval Q)" 

76 

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

77 
lemma eval_sup [simp]: 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

78 
"eval (P \<squnion> Q) = eval P \<squnion> eval Q" 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

79 
by (simp add: sup_pred_def) 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

80 

30328  81 
definition 
37767  82 
"\<Sqinter>A = Pred (INFI A eval)" 
30328  83 

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

84 
lemma eval_Inf [simp]: 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

85 
"eval (\<Sqinter>A) = INFI A eval" 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

86 
by (simp add: Inf_pred_def) 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

87 

30328  88 
definition 
37767  89 
"\<Squnion>A = Pred (SUPR A eval)" 
30328  90 

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

91 
lemma eval_Sup [simp]: 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

92 
"eval (\<Squnion>A) = SUPR A eval" 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

93 
by (simp add: Sup_pred_def) 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

94 

44033  95 
instance proof 
44415  96 
qed (auto intro!: pred_eqI simp add: less_eq_pred_def less_pred_def le_fun_def less_fun_def) 
44033  97 

98 
end 

99 

100 
lemma eval_INFI [simp]: 

101 
"eval (INFI A f) = INFI A (eval \<circ> f)" 

44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
44415
diff
changeset

102 
by (simp only: INF_def eval_Inf image_compose) 
44033  103 

104 
lemma eval_SUPR [simp]: 

105 
"eval (SUPR A f) = SUPR A (eval \<circ> f)" 

44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
44415
diff
changeset

106 
by (simp only: SUP_def eval_Sup image_compose) 
44033  107 

108 
instantiation pred :: (type) complete_boolean_algebra 

109 
begin 

110 

32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

111 
definition 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

112 
" P = Pred ( eval P)" 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

113 

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

114 
lemma eval_compl [simp]: 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

115 
"eval ( P) =  eval P" 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

116 
by (simp add: uminus_pred_def) 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

117 

32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

118 
definition 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

119 
"P  Q = Pred (eval P  eval Q)" 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

120 

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

121 
lemma eval_minus [simp]: 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

122 
"eval (P  Q) = eval P  eval Q" 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

123 
by (simp add: minus_pred_def) 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

124 

32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

125 
instance proof 
46884  126 
qed (auto intro!: pred_eqI) 
30328  127 

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

128 
end 
30328  129 

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

130 
definition single :: "'a \<Rightarrow> 'a pred" where 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

131 
"single x = Pred ((op =) x)" 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

132 

c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

133 
lemma eval_single [simp]: 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

134 
"eval (single x) = (op =) x" 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

135 
by (simp add: single_def) 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

136 

c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

137 
definition bind :: "'a pred \<Rightarrow> ('a \<Rightarrow> 'b pred) \<Rightarrow> 'b pred" (infixl "\<guillemotright>=" 70) where 
41080  138 
"P \<guillemotright>= f = (SUPR {x. eval P x} f)" 
40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

139 

c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

140 
lemma eval_bind [simp]: 
41080  141 
"eval (P \<guillemotright>= f) = eval (SUPR {x. eval P x} f)" 
40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

142 
by (simp add: bind_def) 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

143 

30328  144 
lemma bind_bind: 
145 
"(P \<guillemotright>= Q) \<guillemotright>= R = P \<guillemotright>= (\<lambda>x. Q x \<guillemotright>= R)" 

46884  146 
by (rule pred_eqI) auto 
30328  147 

148 
lemma bind_single: 

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

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

150 
by (rule pred_eqI) auto 
30328  151 

152 
lemma single_bind: 

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

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

154 
by (rule pred_eqI) auto 
30328  155 

156 
lemma bottom_bind: 

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

40674
54dbe6a1c349
adhere established Collect/mem convention more closely
haftmann
parents:
40616
diff
changeset

158 
by (rule pred_eqI) auto 
30328  159 

160 
lemma sup_bind: 

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

40674
54dbe6a1c349
adhere established Collect/mem convention more closely
haftmann
parents:
40616
diff
changeset

162 
by (rule pred_eqI) auto 
30328  163 

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

164 
lemma Sup_bind: 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

165 
"(\<Squnion>A \<guillemotright>= f) = \<Squnion>((\<lambda>x. x \<guillemotright>= f) ` A)" 
46884  166 
by (rule pred_eqI) auto 
30328  167 

168 
lemma pred_iffI: 

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

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

171 
shows "A = B" 

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

172 
using assms by (auto intro: pred_eqI) 
30328  173 

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

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

175 
by simp 
30328  176 

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

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

178 
by simp 
30328  179 

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

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

181 
by simp 
30328  182 

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

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

184 
by simp 
30328  185 

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

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

187 
by auto 
30328  188 

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

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

190 
by auto 
30328  191 

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

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

193 
by auto 
30328  194 

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

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

196 
by auto 
30328  197 

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

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

199 
by auto 
30328  200 

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

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

202 
by auto 
30328  203 

32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

204 
lemma single_not_bot [simp]: 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

205 
"single x \<noteq> \<bottom>" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

206 
by (auto simp add: single_def bot_pred_def fun_eq_iff) 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

207 

22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

208 
lemma not_bot: 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

209 
assumes "A \<noteq> \<bottom>" 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

210 
obtains x where "eval A x" 
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45630
diff
changeset

211 
using assms by (cases A) (auto simp add: bot_pred_def) 
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45630
diff
changeset

212 

32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

213 

46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

214 
subsection {* Emptiness check and definite choice *} 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

215 

22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

216 
definition is_empty :: "'a pred \<Rightarrow> bool" where 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

217 
"is_empty A \<longleftrightarrow> A = \<bottom>" 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

218 

22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

219 
lemma is_empty_bot: 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

220 
"is_empty \<bottom>" 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

221 
by (simp add: is_empty_def) 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

222 

22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

223 
lemma not_is_empty_single: 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

224 
"\<not> is_empty (single x)" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

225 
by (auto simp add: is_empty_def single_def bot_pred_def fun_eq_iff) 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

226 

22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

227 
lemma is_empty_sup: 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

228 
"is_empty (A \<squnion> B) \<longleftrightarrow> is_empty A \<and> is_empty B" 
36008  229 
by (auto simp add: is_empty_def) 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

230 

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

231 
definition singleton :: "(unit \<Rightarrow> 'a) \<Rightarrow> 'a pred \<Rightarrow> 'a" where 
33111  232 
"singleton dfault A = (if \<exists>!x. eval A x then THE x. eval A x else dfault ())" 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

233 

22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

234 
lemma singleton_eqI: 
33110  235 
"\<exists>!x. eval A x \<Longrightarrow> eval A x \<Longrightarrow> singleton dfault A = x" 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

236 
by (auto simp add: singleton_def) 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

237 

22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

238 
lemma eval_singletonI: 
33110  239 
"\<exists>!x. eval A x \<Longrightarrow> eval A (singleton dfault A)" 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

240 
proof  
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

241 
assume assm: "\<exists>!x. eval A x" 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

242 
then obtain x where "eval A x" .. 
33110  243 
moreover with assm have "singleton dfault A = x" by (rule singleton_eqI) 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

244 
ultimately show ?thesis by simp 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

245 
qed 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

246 

22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

247 
lemma single_singleton: 
33110  248 
"\<exists>!x. eval A x \<Longrightarrow> single (singleton dfault A) = A" 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

249 
proof  
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

250 
assume assm: "\<exists>!x. eval A x" 
33110  251 
then have "eval A (singleton dfault A)" 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

252 
by (rule eval_singletonI) 
33110  253 
moreover from assm have "\<And>x. eval A x \<Longrightarrow> singleton dfault A = x" 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

254 
by (rule singleton_eqI) 
33110  255 
ultimately have "eval (single (singleton dfault A)) = eval A" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

256 
by (simp (no_asm_use) add: single_def fun_eq_iff) blast 
40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

257 
then have "\<And>x. eval (single (singleton dfault A)) x = eval A x" 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

258 
by simp 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

259 
then show ?thesis by (rule pred_eqI) 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

260 
qed 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

261 

22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

262 
lemma singleton_undefinedI: 
33111  263 
"\<not> (\<exists>!x. eval A x) \<Longrightarrow> singleton dfault A = dfault ()" 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

264 
by (simp add: singleton_def) 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

265 

22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

266 
lemma singleton_bot: 
33111  267 
"singleton dfault \<bottom> = dfault ()" 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

268 
by (auto simp add: bot_pred_def intro: singleton_undefinedI) 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

269 

22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

270 
lemma singleton_single: 
33110  271 
"singleton dfault (single x) = x" 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

272 
by (auto simp add: intro: singleton_eqI singleI elim: singleE) 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

273 

22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

274 
lemma singleton_sup_single_single: 
33111  275 
"singleton dfault (single x \<squnion> single y) = (if x = y then x else dfault ())" 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

276 
proof (cases "x = y") 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

277 
case True then show ?thesis by (simp add: singleton_single) 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

278 
next 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

279 
case False 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

280 
have "eval (single x \<squnion> single y) x" 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

281 
and "eval (single x \<squnion> single y) y" 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

282 
by (auto intro: supI1 supI2 singleI) 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

283 
with False have "\<not> (\<exists>!z. eval (single x \<squnion> single y) z)" 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

284 
by blast 
33111  285 
then have "singleton dfault (single x \<squnion> single y) = dfault ()" 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

286 
by (rule singleton_undefinedI) 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

287 
with False show ?thesis by simp 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

288 
qed 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

289 

22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

290 
lemma singleton_sup_aux: 
33110  291 
"singleton dfault (A \<squnion> B) = (if A = \<bottom> then singleton dfault B 
292 
else if B = \<bottom> then singleton dfault A 

293 
else singleton dfault 

294 
(single (singleton dfault A) \<squnion> single (singleton dfault B)))" 

32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

295 
proof (cases "(\<exists>!x. eval A x) \<and> (\<exists>!y. eval B y)") 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

296 
case True then show ?thesis by (simp add: single_singleton) 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

297 
next 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

298 
case False 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

299 
from False have A_or_B: 
33111  300 
"singleton dfault A = dfault () \<or> singleton dfault B = dfault ()" 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

301 
by (auto intro!: singleton_undefinedI) 
33110  302 
then have rhs: "singleton dfault 
33111  303 
(single (singleton dfault A) \<squnion> single (singleton dfault B)) = dfault ()" 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

304 
by (auto simp add: singleton_sup_single_single singleton_single) 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

305 
from False have not_unique: 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

306 
"\<not> (\<exists>!x. eval A x) \<or> \<not> (\<exists>!y. eval B y)" by simp 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

307 
show ?thesis proof (cases "A \<noteq> \<bottom> \<and> B \<noteq> \<bottom>") 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

308 
case True 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

309 
then obtain a b where a: "eval A a" and b: "eval B b" 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

310 
by (blast elim: not_bot) 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

311 
with True not_unique have "\<not> (\<exists>!x. eval (A \<squnion> B) x)" 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

312 
by (auto simp add: sup_pred_def bot_pred_def) 
33111  313 
then have "singleton dfault (A \<squnion> B) = dfault ()" by (rule singleton_undefinedI) 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

314 
with True rhs show ?thesis by simp 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

315 
next 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

316 
case False then show ?thesis by auto 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

317 
qed 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

318 
qed 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

319 

22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

320 
lemma singleton_sup: 
33110  321 
"singleton dfault (A \<squnion> B) = (if A = \<bottom> then singleton dfault B 
322 
else if B = \<bottom> then singleton dfault A 

33111  323 
else if singleton dfault A = singleton dfault B then singleton dfault A else dfault ())" 
33110  324 
using singleton_sup_aux [of dfault A B] by (simp only: singleton_sup_single_single) 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

325 

30328  326 

46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

327 
subsection {* Derived operations *} 
30328  328 

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

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

331 

33754
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

332 
definition holds :: "unit pred \<Rightarrow> bool" where 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

333 
holds_eq: "holds P = eval P ()" 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

334 

30328  335 
definition not_pred :: "unit pred \<Rightarrow> unit pred" where 
336 
not_pred_eq: "not_pred P = (if eval P () then \<bottom> else single ())" 

337 

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

339 
unfolding if_pred_eq by (auto intro: singleI) 

340 

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

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

343 

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

345 
unfolding not_pred_eq eval_pred by (auto intro: singleI) 

346 

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

348 
unfolding not_pred_eq by (auto intro: singleI) 

349 

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

351 
unfolding not_pred_eq 

352 
by (auto split: split_if_asm elim: botE) 

353 

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

355 
unfolding not_pred_eq 

356 
by (auto split: split_if_asm elim: botE) 

33754
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

357 
lemma "f () = False \<or> f () = True" 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

358 
by simp 
30328  359 

37549  360 
lemma closure_of_bool_cases [no_atp]: 
44007  361 
fixes f :: "unit \<Rightarrow> bool" 
362 
assumes "f = (\<lambda>u. False) \<Longrightarrow> P f" 

363 
assumes "f = (\<lambda>u. True) \<Longrightarrow> P f" 

364 
shows "P f" 

33754
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

365 
proof  
44007  366 
have "f = (\<lambda>u. False) \<or> f = (\<lambda>u. True)" 
33754
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

367 
apply (cases "f ()") 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

368 
apply (rule disjI2) 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

369 
apply (rule ext) 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

370 
apply (simp add: unit_eq) 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

371 
apply (rule disjI1) 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

372 
apply (rule ext) 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

373 
apply (simp add: unit_eq) 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

374 
done 
41550  375 
from this assms show ?thesis by blast 
33754
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

376 
qed 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

377 

f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

378 
lemma unit_pred_cases: 
44007  379 
assumes "P \<bottom>" 
380 
assumes "P (single ())" 

381 
shows "P Q" 

44415  382 
using assms unfolding bot_pred_def bot_fun_def bot_bool_def empty_def single_def proof (cases Q) 
44007  383 
fix f 
384 
assume "P (Pred (\<lambda>u. False))" "P (Pred (\<lambda>u. () = u))" 

385 
then have "P (Pred f)" 

386 
by (cases _ f rule: closure_of_bool_cases) simp_all 

387 
moreover assume "Q = Pred f" 

388 
ultimately show "P Q" by simp 

389 
qed 

390 

33754
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

391 
lemma holds_if_pred: 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

392 
"holds (if_pred b) = b" 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

393 
unfolding if_pred_eq holds_eq 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

394 
by (cases b) (auto intro: singleI elim: botE) 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

395 

f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

396 
lemma if_pred_holds: 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

397 
"if_pred (holds P) = P" 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

398 
unfolding if_pred_eq holds_eq 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

399 
by (rule unit_pred_cases) (auto intro: singleI elim: botE) 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

400 

f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

401 
lemma is_empty_holds: 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

402 
"is_empty P \<longleftrightarrow> \<not> holds P" 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

403 
unfolding is_empty_def holds_eq 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

404 
by (rule unit_pred_cases) (auto elim: botE intro: singleI) 
30328  405 

41311  406 
definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a pred \<Rightarrow> 'b pred" where 
407 
"map f P = P \<guillemotright>= (single o f)" 

408 

409 
lemma eval_map [simp]: 

44363  410 
"eval (map f P) = (\<Squnion>x\<in>{x. eval P x}. (\<lambda>y. f x = y))" 
44415  411 
by (auto simp add: map_def comp_def) 
41311  412 

41505
6d19301074cf
"enriched_type" replaces less specific "type_lifting"
haftmann
parents:
41372
diff
changeset

413 
enriched_type map: map 
44363  414 
by (rule ext, rule pred_eqI, auto)+ 
41311  415 

416 

46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

417 
subsection {* Implementation *} 
30328  418 

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

420 

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

44414  422 
"pred_of_seq Empty = \<bottom>" 
423 
 "pred_of_seq (Insert x P) = single x \<squnion> P" 

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

30328  425 

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

427 
"Seq f = pred_of_seq (f ())" 

428 

429 
code_datatype Seq 

430 

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

432 
"member Empty x \<longleftrightarrow> False" 

44414  433 
 "member (Insert y P) x \<longleftrightarrow> x = y \<or> eval P x" 
434 
 "member (Join P xq) x \<longleftrightarrow> eval P x \<or> member xq x" 

30328  435 

436 
lemma eval_member: 

437 
"member xq = eval (pred_of_seq xq)" 

438 
proof (induct xq) 

439 
case Empty show ?case 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

440 
by (auto simp add: fun_eq_iff elim: botE) 
30328  441 
next 
442 
case Insert show ?case 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

443 
by (auto simp add: fun_eq_iff elim: supE singleE intro: supI1 supI2 singleI) 
30328  444 
next 
445 
case Join then show ?case 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

446 
by (auto simp add: fun_eq_iff elim: supE intro: supI1 supI2) 
30328  447 
qed 
448 

46038
bb2f7488a0f1
conversions from sets to predicates and vice versa; extensionality on predicates
haftmann
parents:
45970
diff
changeset

449 
lemma eval_code [(* FIXME declare simp *)code]: "eval (Seq f) = member (f ())" 
30328  450 
unfolding Seq_def by (rule sym, rule eval_member) 
451 

452 
lemma single_code [code]: 

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

454 
unfolding Seq_def by simp 

455 

41080  456 
primrec "apply" :: "('a \<Rightarrow> 'b pred) \<Rightarrow> 'a seq \<Rightarrow> 'b seq" where 
44415  457 
"apply f Empty = Empty" 
458 
 "apply f (Insert x P) = Join (f x) (Join (P \<guillemotright>= f) Empty)" 

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

30328  460 

461 
lemma apply_bind: 

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

463 
proof (induct xq) 

464 
case Empty show ?case 

465 
by (simp add: bottom_bind) 

466 
next 

467 
case Insert show ?case 

468 
by (simp add: single_bind sup_bind) 

469 
next 

470 
case Join then show ?case 

471 
by (simp add: sup_bind) 

472 
qed 

473 

474 
lemma bind_code [code]: 

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

476 
unfolding Seq_def by (rule sym, rule apply_bind) 

477 

478 
lemma bot_set_code [code]: 

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

480 
unfolding Seq_def by simp 

481 

30376  482 
primrec adjunct :: "'a pred \<Rightarrow> 'a seq \<Rightarrow> 'a seq" where 
44415  483 
"adjunct P Empty = Join P Empty" 
484 
 "adjunct P (Insert x Q) = Insert x (Q \<squnion> P)" 

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

30376  486 

487 
lemma adjunct_sup: 

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

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

490 

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

493 
of Empty \<Rightarrow> g () 

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

30376  495 
 Join P xq \<Rightarrow> adjunct (Seq g) (Join P xq))" 
30328  496 
proof (cases "f ()") 
497 
case Empty 

498 
thus ?thesis 

34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
33988
diff
changeset

499 
unfolding Seq_def by (simp add: sup_commute [of "\<bottom>"]) 
30328  500 
next 
501 
case Insert 

502 
thus ?thesis 

503 
unfolding Seq_def by (simp add: sup_assoc) 

504 
next 

505 
case Join 

506 
thus ?thesis 

30376  507 
unfolding Seq_def 
508 
by (simp add: adjunct_sup sup_assoc sup_commute sup_left_commute) 

30328  509 
qed 
510 

46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

511 
lemma [code]: 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

512 
"size (P :: 'a Predicate.pred) = 0" by (cases P) simp 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

513 

1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

514 
lemma [code]: 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

515 
"pred_size f P = 0" by (cases P) simp 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

516 

30430
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

517 
primrec contained :: "'a seq \<Rightarrow> 'a pred \<Rightarrow> bool" where 
44415  518 
"contained Empty Q \<longleftrightarrow> True" 
519 
 "contained (Insert x P) Q \<longleftrightarrow> eval Q x \<and> P \<le> Q" 

520 
 "contained (Join P xq) Q \<longleftrightarrow> P \<le> Q \<and> contained xq Q" 

30430
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

521 

42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

522 
lemma single_less_eq_eval: 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

523 
"single x \<le> P \<longleftrightarrow> eval P x" 
44415  524 
by (auto simp add: less_eq_pred_def le_fun_def) 
30430
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

525 

42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

526 
lemma contained_less_eq: 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

527 
"contained xq Q \<longleftrightarrow> pred_of_seq xq \<le> Q" 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

528 
by (induct xq) (simp_all add: single_less_eq_eval) 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

529 

42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

530 
lemma less_eq_pred_code [code]: 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

531 
"Seq f \<le> Q = (case f () 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

532 
of Empty \<Rightarrow> True 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

533 
 Insert x P \<Rightarrow> eval Q x \<and> P \<le> Q 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

534 
 Join P xq \<Rightarrow> P \<le> Q \<and> contained xq Q)" 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

535 
by (cases "f ()") 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

536 
(simp_all add: Seq_def single_less_eq_eval contained_less_eq) 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

537 

42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

538 
lemma eq_pred_code [code]: 
31133  539 
fixes P Q :: "'a pred" 
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38651
diff
changeset

540 
shows "HOL.equal P Q \<longleftrightarrow> P \<le> Q \<and> Q \<le> P" 
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38651
diff
changeset

541 
by (auto simp add: equal) 
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38651
diff
changeset

542 

97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38651
diff
changeset

543 
lemma [code nbe]: 
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38651
diff
changeset

544 
"HOL.equal (x :: 'a pred) x \<longleftrightarrow> True" 
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38651
diff
changeset

545 
by (fact equal_refl) 
30430
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

546 

42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

547 
lemma [code]: 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

548 
"pred_case f P = f (eval P)" 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

549 
by (cases P) simp 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

550 

42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

551 
lemma [code]: 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

552 
"pred_rec f P = f (eval P)" 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

553 
by (cases P) simp 
30328  554 

31105
95f66b234086
added general preprocessing of equality in predicates for code generation
bulwahn
parents:
30430
diff
changeset

555 
inductive eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where "eq x x" 
95f66b234086
added general preprocessing of equality in predicates for code generation
bulwahn
parents:
30430
diff
changeset

556 

95f66b234086
added general preprocessing of equality in predicates for code generation
bulwahn
parents:
30430
diff
changeset

557 
lemma eq_is_eq: "eq x y \<equiv> (x = y)" 
31108  558 
by (rule eq_reflection) (auto intro: eq.intros elim: eq.cases) 
30948  559 

32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

560 
primrec null :: "'a seq \<Rightarrow> bool" where 
44415  561 
"null Empty \<longleftrightarrow> True" 
562 
 "null (Insert x P) \<longleftrightarrow> False" 

563 
 "null (Join P xq) \<longleftrightarrow> is_empty P \<and> null xq" 

32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

564 

22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

565 
lemma null_is_empty: 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

566 
"null xq \<longleftrightarrow> is_empty (pred_of_seq xq)" 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

567 
by (induct xq) (simp_all add: is_empty_bot not_is_empty_single is_empty_sup) 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

568 

22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

569 
lemma is_empty_code [code]: 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

570 
"is_empty (Seq f) \<longleftrightarrow> null (f ())" 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

571 
by (simp add: null_is_empty Seq_def) 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

572 

33111  573 
primrec the_only :: "(unit \<Rightarrow> 'a) \<Rightarrow> 'a seq \<Rightarrow> 'a" where 
574 
[code del]: "the_only dfault Empty = dfault ()" 

44415  575 
 "the_only dfault (Insert x P) = (if is_empty P then x else let y = singleton dfault P in if x = y then x else dfault ())" 
576 
 "the_only dfault (Join P xq) = (if is_empty P then the_only dfault xq else if null xq then singleton dfault P 

33110  577 
else let x = singleton dfault P; y = the_only dfault xq in 
33111  578 
if x = y then x else dfault ())" 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

579 

22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

580 
lemma the_only_singleton: 
33110  581 
"the_only dfault xq = singleton dfault (pred_of_seq xq)" 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

582 
by (induct xq) 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

583 
(auto simp add: singleton_bot singleton_single is_empty_def 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

584 
null_is_empty Let_def singleton_sup) 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

585 

22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

586 
lemma singleton_code [code]: 
33110  587 
"singleton dfault (Seq f) = (case f () 
33111  588 
of Empty \<Rightarrow> dfault () 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

589 
 Insert x P \<Rightarrow> if is_empty P then x 
33110  590 
else let y = singleton dfault P in 
33111  591 
if x = y then x else dfault () 
33110  592 
 Join P xq \<Rightarrow> if is_empty P then the_only dfault xq 
593 
else if null xq then singleton dfault P 

594 
else let x = singleton dfault P; y = the_only dfault xq in 

33111  595 
if x = y then x else dfault ())" 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

596 
by (cases "f ()") 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

597 
(auto simp add: Seq_def the_only_singleton is_empty_def 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

598 
null_is_empty singleton_bot singleton_single singleton_sup Let_def) 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

599 

44414  600 
definition the :: "'a pred \<Rightarrow> 'a" where 
37767  601 
"the A = (THE x. eval A x)" 
33111  602 

40674
54dbe6a1c349
adhere established Collect/mem convention more closely
haftmann
parents:
40616
diff
changeset

603 
lemma the_eqI: 
41080  604 
"(THE x. eval P x) = x \<Longrightarrow> the P = x" 
40674
54dbe6a1c349
adhere established Collect/mem convention more closely
haftmann
parents:
40616
diff
changeset

605 
by (simp add: the_def) 
54dbe6a1c349
adhere established Collect/mem convention more closely
haftmann
parents:
40616
diff
changeset

606 

44414  607 
definition not_unique :: "'a pred \<Rightarrow> 'a" where 
608 
[code del]: "not_unique A = (THE x. eval A x)" 

609 

610 
code_abort not_unique 

611 

40674
54dbe6a1c349
adhere established Collect/mem convention more closely
haftmann
parents:
40616
diff
changeset

612 
lemma the_eq [code]: "the A = singleton (\<lambda>x. not_unique A) A" 
54dbe6a1c349
adhere established Collect/mem convention more closely
haftmann
parents:
40616
diff
changeset

613 
by (rule the_eqI) (simp add: singleton_def not_unique_def) 
33110  614 

36531
19f6e3b0d9b6
code_reflect: specify module name directly after keyword
haftmann
parents:
36513
diff
changeset

615 
code_reflect Predicate 
36513  616 
datatypes pred = Seq and seq = Empty  Insert  Join 
617 
functions map 

618 

30948  619 
ML {* 
620 
signature PREDICATE = 

621 
sig 

622 
datatype 'a pred = Seq of (unit > 'a seq) 

623 
and 'a seq = Empty  Insert of 'a * 'a pred  Join of 'a pred * 'a seq 

30959
458e55fd0a33
fixed compilation of predicate types in ML environment
haftmann
parents:
30948
diff
changeset

624 
val yield: 'a pred > ('a * 'a pred) option 
458e55fd0a33
fixed compilation of predicate types in ML environment
haftmann
parents:
30948
diff
changeset

625 
val yieldn: int > 'a pred > 'a list * 'a pred 
31222  626 
val map: ('a > 'b) > 'a pred > 'b pred 
30948  627 
end; 
628 

629 
structure Predicate : PREDICATE = 

630 
struct 

631 

36513  632 
datatype pred = datatype Predicate.pred 
633 
datatype seq = datatype Predicate.seq 

634 

635 
fun map f = Predicate.map f; 

30959
458e55fd0a33
fixed compilation of predicate types in ML environment
haftmann
parents:
30948
diff
changeset

636 

36513  637 
fun yield (Seq f) = next (f ()) 
638 
and next Empty = NONE 

639 
 next (Insert (x, P)) = SOME (x, P) 

640 
 next (Join (P, xq)) = (case yield P 

30959
458e55fd0a33
fixed compilation of predicate types in ML environment
haftmann
parents:
30948
diff
changeset

641 
of NONE => next xq 
36513  642 
 SOME (x, Q) => SOME (x, Seq (fn _ => Join (Q, xq)))); 
30959
458e55fd0a33
fixed compilation of predicate types in ML environment
haftmann
parents:
30948
diff
changeset

643 

458e55fd0a33
fixed compilation of predicate types in ML environment
haftmann
parents:
30948
diff
changeset

644 
fun anamorph f k x = (if k = 0 then ([], x) 
458e55fd0a33
fixed compilation of predicate types in ML environment
haftmann
parents:
30948
diff
changeset

645 
else case f x 
458e55fd0a33
fixed compilation of predicate types in ML environment
haftmann
parents:
30948
diff
changeset

646 
of NONE => ([], x) 
458e55fd0a33
fixed compilation of predicate types in ML environment
haftmann
parents:
30948
diff
changeset

647 
 SOME (v, y) => let 
458e55fd0a33
fixed compilation of predicate types in ML environment
haftmann
parents:
30948
diff
changeset

648 
val (vs, z) = anamorph f (k  1) y 
33607  649 
in (v :: vs, z) end); 
30959
458e55fd0a33
fixed compilation of predicate types in ML environment
haftmann
parents:
30948
diff
changeset

650 

458e55fd0a33
fixed compilation of predicate types in ML environment
haftmann
parents:
30948
diff
changeset

651 
fun yieldn P = anamorph yield P; 
30948  652 

653 
end; 

654 
*} 

655 

46038
bb2f7488a0f1
conversions from sets to predicates and vice versa; extensionality on predicates
haftmann
parents:
45970
diff
changeset

656 
text {* Conversion from and to sets *} 
bb2f7488a0f1
conversions from sets to predicates and vice versa; extensionality on predicates
haftmann
parents:
45970
diff
changeset

657 

bb2f7488a0f1
conversions from sets to predicates and vice versa; extensionality on predicates
haftmann
parents:
45970
diff
changeset

658 
definition pred_of_set :: "'a set \<Rightarrow> 'a pred" where 
bb2f7488a0f1
conversions from sets to predicates and vice versa; extensionality on predicates
haftmann
parents:
45970
diff
changeset

659 
"pred_of_set = Pred \<circ> (\<lambda>A x. x \<in> A)" 
bb2f7488a0f1
conversions from sets to predicates and vice versa; extensionality on predicates
haftmann
parents:
45970
diff
changeset

660 

bb2f7488a0f1
conversions from sets to predicates and vice versa; extensionality on predicates
haftmann
parents:
45970
diff
changeset

661 
lemma eval_pred_of_set [simp]: 
bb2f7488a0f1
conversions from sets to predicates and vice versa; extensionality on predicates
haftmann
parents:
45970
diff
changeset

662 
"eval (pred_of_set A) x \<longleftrightarrow> x \<in>A" 
bb2f7488a0f1
conversions from sets to predicates and vice versa; extensionality on predicates
haftmann
parents:
45970
diff
changeset

663 
by (simp add: pred_of_set_def) 
bb2f7488a0f1
conversions from sets to predicates and vice versa; extensionality on predicates
haftmann
parents:
45970
diff
changeset

664 

bb2f7488a0f1
conversions from sets to predicates and vice versa; extensionality on predicates
haftmann
parents:
45970
diff
changeset

665 
definition set_of_pred :: "'a pred \<Rightarrow> 'a set" where 
bb2f7488a0f1
conversions from sets to predicates and vice versa; extensionality on predicates
haftmann
parents:
45970
diff
changeset

666 
"set_of_pred = Collect \<circ> eval" 
bb2f7488a0f1
conversions from sets to predicates and vice versa; extensionality on predicates
haftmann
parents:
45970
diff
changeset

667 

bb2f7488a0f1
conversions from sets to predicates and vice versa; extensionality on predicates
haftmann
parents:
45970
diff
changeset

668 
lemma member_set_of_pred [simp]: 
bb2f7488a0f1
conversions from sets to predicates and vice versa; extensionality on predicates
haftmann
parents:
45970
diff
changeset

669 
"x \<in> set_of_pred P \<longleftrightarrow> Predicate.eval P x" 
bb2f7488a0f1
conversions from sets to predicates and vice versa; extensionality on predicates
haftmann
parents:
45970
diff
changeset

670 
by (simp add: set_of_pred_def) 
bb2f7488a0f1
conversions from sets to predicates and vice versa; extensionality on predicates
haftmann
parents:
45970
diff
changeset

671 

bb2f7488a0f1
conversions from sets to predicates and vice versa; extensionality on predicates
haftmann
parents:
45970
diff
changeset

672 
definition set_of_seq :: "'a seq \<Rightarrow> 'a set" where 
bb2f7488a0f1
conversions from sets to predicates and vice versa; extensionality on predicates
haftmann
parents:
45970
diff
changeset

673 
"set_of_seq = set_of_pred \<circ> pred_of_seq" 
bb2f7488a0f1
conversions from sets to predicates and vice versa; extensionality on predicates
haftmann
parents:
45970
diff
changeset

674 

bb2f7488a0f1
conversions from sets to predicates and vice versa; extensionality on predicates
haftmann
parents:
45970
diff
changeset

675 
lemma member_set_of_seq [simp]: 
bb2f7488a0f1
conversions from sets to predicates and vice versa; extensionality on predicates
haftmann
parents:
45970
diff
changeset

676 
"x \<in> set_of_seq xq = Predicate.member xq x" 
bb2f7488a0f1
conversions from sets to predicates and vice versa; extensionality on predicates
haftmann
parents:
45970
diff
changeset

677 
by (simp add: set_of_seq_def eval_member) 
bb2f7488a0f1
conversions from sets to predicates and vice versa; extensionality on predicates
haftmann
parents:
45970
diff
changeset

678 

bb2f7488a0f1
conversions from sets to predicates and vice versa; extensionality on predicates
haftmann
parents:
45970
diff
changeset

679 
lemma of_pred_code [code]: 
bb2f7488a0f1
conversions from sets to predicates and vice versa; extensionality on predicates
haftmann
parents:
45970
diff
changeset

680 
"set_of_pred (Predicate.Seq f) = (case f () of 
bb2f7488a0f1
conversions from sets to predicates and vice versa; extensionality on predicates
haftmann
parents:
45970
diff
changeset

681 
Predicate.Empty \<Rightarrow> {} 
bb2f7488a0f1
conversions from sets to predicates and vice versa; extensionality on predicates
haftmann
parents:
45970
diff
changeset

682 
 Predicate.Insert x P \<Rightarrow> insert x (set_of_pred P) 
bb2f7488a0f1
conversions from sets to predicates and vice versa; extensionality on predicates
haftmann
parents:
45970
diff
changeset

683 
 Predicate.Join P xq \<Rightarrow> set_of_pred P \<union> set_of_seq xq)" 
bb2f7488a0f1
conversions from sets to predicates and vice versa; extensionality on predicates
haftmann
parents:
45970
diff
changeset

684 
by (auto split: seq.split simp add: eval_code) 
bb2f7488a0f1
conversions from sets to predicates and vice versa; extensionality on predicates
haftmann
parents:
45970
diff
changeset

685 

bb2f7488a0f1
conversions from sets to predicates and vice versa; extensionality on predicates
haftmann
parents:
45970
diff
changeset

686 
lemma of_seq_code [code]: 
bb2f7488a0f1
conversions from sets to predicates and vice versa; extensionality on predicates
haftmann
parents:
45970
diff
changeset

687 
"set_of_seq Predicate.Empty = {}" 
bb2f7488a0f1
conversions from sets to predicates and vice versa; extensionality on predicates
haftmann
parents:
45970
diff
changeset

688 
"set_of_seq (Predicate.Insert x P) = insert x (set_of_pred P)" 
bb2f7488a0f1
conversions from sets to predicates and vice versa; extensionality on predicates
haftmann
parents:
45970
diff
changeset

689 
"set_of_seq (Predicate.Join P xq) = set_of_pred P \<union> set_of_seq xq" 
bb2f7488a0f1
conversions from sets to predicates and vice versa; extensionality on predicates
haftmann
parents:
45970
diff
changeset

690 
by auto 
bb2f7488a0f1
conversions from sets to predicates and vice versa; extensionality on predicates
haftmann
parents:
45970
diff
changeset

691 

46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

692 
text {* Lazy Evaluation of an indexed function *} 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

693 

1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

694 
function iterate_upto :: "(code_numeral \<Rightarrow> 'a) \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<Rightarrow> 'a Predicate.pred" 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

695 
where 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

696 
"iterate_upto f n m = 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

697 
Predicate.Seq (%u. if n > m then Predicate.Empty 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

698 
else Predicate.Insert (f n) (iterate_upto f (n + 1) m))" 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

699 
by pat_completeness auto 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

700 

1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

701 
termination by (relation "measure (%(f, n, m). Code_Numeral.nat_of (m + 1  n))") auto 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

702 

1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

703 
text {* Misc *} 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

704 

1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

705 
declare Inf_set_foldr [where 'a = "'a Predicate.pred", code] Sup_set_foldr [where 'a = "'a Predicate.pred", code] 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

706 

1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

707 
(* FIXME: better implement conversion by bisection *) 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

708 

1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

709 
lemma pred_of_set_fold_sup: 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

710 
assumes "finite A" 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

711 
shows "pred_of_set A = Finite_Set.fold sup bot (Predicate.single ` A)" (is "?lhs = ?rhs") 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

712 
proof (rule sym) 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

713 
interpret comp_fun_idem "sup :: 'a Predicate.pred \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'a Predicate.pred" 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

714 
by (fact comp_fun_idem_sup) 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

715 
from `finite A` show "?rhs = ?lhs" by (induct A) (auto intro!: pred_eqI) 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

716 
qed 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

717 

1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

718 
lemma pred_of_set_set_fold_sup: 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

719 
"pred_of_set (set xs) = fold sup (List.map Predicate.single xs) bot" 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

720 
proof  
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

721 
interpret comp_fun_idem "sup :: 'a Predicate.pred \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'a Predicate.pred" 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

722 
by (fact comp_fun_idem_sup) 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

723 
show ?thesis by (simp add: pred_of_set_fold_sup fold_set_fold [symmetric]) 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

724 
qed 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

725 

1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

726 
lemma pred_of_set_set_foldr_sup [code]: 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

727 
"pred_of_set (set xs) = foldr sup (List.map Predicate.single xs) bot" 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

728 
by (simp add: pred_of_set_set_fold_sup ac_simps foldr_fold fun_eq_iff) 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

729 

30328  730 
no_notation 
41082  731 
bot ("\<bottom>") and 
732 
top ("\<top>") and 

30328  733 
inf (infixl "\<sqinter>" 70) and 
734 
sup (infixl "\<squnion>" 65) and 

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

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

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

738 

41080  739 
no_syntax (xsymbols) 
41082  740 
"_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10) 
741 
"_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10) 

41080  742 
"_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10) 
743 
"_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10) 

744 

36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
36008
diff
changeset

745 
hide_type (open) pred seq 
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
36008
diff
changeset

746 
hide_const (open) Pred eval single bind is_empty singleton if_pred not_pred holds 
33111  747 
Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map not_unique the 
46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

748 
iterate_upto 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

749 
hide_fact (open) null_def member_def 
30328  750 

751 
end 

46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

752 