author  kuncar 
Thu, 10 Apr 2014 17:48:32 +0200  
changeset 56525  b5b6ad5dc2ae 
parent 56524  f4ba736040fa 
child 56646  360a05d60761 
permissions  rwrr 
53953  1 
(* Title: HOL/Library/FSet.thy 
2 
Author: Ondrej Kuncar, TU Muenchen 

3 
Author: Cezary Kaliszyk and Christian Urban 

55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

4 
Author: Andrei Popescu, TU Muenchen 
53953  5 
*) 
6 

7 
header {* Type of finite sets defined as a subtype of sets *} 

8 

9 
theory FSet 

55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

10 
imports Conditionally_Complete_Lattices 
53953  11 
begin 
12 

13 
subsection {* Definition of the type *} 

14 

15 
typedef 'a fset = "{A :: 'a set. finite A}" morphisms fset Abs_fset 

16 
by auto 

17 

18 
setup_lifting type_definition_fset 

19 

55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

20 

53953  21 
subsection {* Basic operations and type class instantiations *} 
22 

23 
(* FIXME transfer and right_total vs. bi_total *) 

24 
instantiation fset :: (finite) finite 

25 
begin 

26 
instance by default (transfer, simp) 

27 
end 

28 

29 
instantiation fset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}" 

30 
begin 

31 

32 
interpretation lifting_syntax . 

33 

34 
lift_definition bot_fset :: "'a fset" is "{}" parametric empty_transfer by simp 

35 

36 
lift_definition less_eq_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" is subset_eq parametric subset_transfer 

55565
f663fc1e653b
simplify proofs because of the stronger reflexivity prover
kuncar
parents:
55414
diff
changeset

37 
. 
53953  38 

39 
definition less_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where "xs < ys \<equiv> xs \<le> ys \<and> xs \<noteq> (ys::'a fset)" 

40 

41 
lemma less_fset_transfer[transfer_rule]: 

42 
assumes [transfer_rule]: "bi_unique A" 

43 
shows "((pcr_fset A) ===> (pcr_fset A) ===> op =) op \<subset> op <" 

44 
unfolding less_fset_def[abs_def] psubset_eq[abs_def] by transfer_prover 

45 

46 

47 
lift_definition sup_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is union parametric union_transfer 

48 
by simp 

49 

50 
lift_definition inf_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is inter parametric inter_transfer 

51 
by simp 

52 

53 
lift_definition minus_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is minus parametric Diff_transfer 

54 
by simp 

55 

56 
instance 

57 
by default (transfer, auto)+ 

58 

59 
end 

60 

61 
abbreviation fempty :: "'a fset" ("{}") where "{} \<equiv> bot" 

62 
abbreviation fsubset_eq :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "\<subseteq>" 50) where "xs \<subseteq> ys \<equiv> xs \<le> ys" 

63 
abbreviation fsubset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "\<subset>" 50) where "xs \<subset> ys \<equiv> xs < ys" 

64 
abbreviation funion :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" (infixl "\<union>" 65) where "xs \<union> ys \<equiv> sup xs ys" 

65 
abbreviation finter :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" (infixl "\<inter>" 65) where "xs \<inter> ys \<equiv> inf xs ys" 

66 
abbreviation fminus :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" (infixl "" 65) where "xs  ys \<equiv> minus xs ys" 

67 

54014  68 
instantiation fset :: (equal) equal 
69 
begin 

70 
definition "HOL.equal A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" 

71 
instance by intro_classes (auto simp add: equal_fset_def) 

72 
end 

73 

53953  74 
instantiation fset :: (type) conditionally_complete_lattice 
75 
begin 

76 

77 
interpretation lifting_syntax . 

78 

79 
lemma right_total_Inf_fset_transfer: 

80 
assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "right_total A" 

55938  81 
shows "(rel_set (rel_set A) ===> rel_set A) 
53953  82 
(\<lambda>S. if finite (Inter S \<inter> Collect (Domainp A)) then Inter S \<inter> Collect (Domainp A) else {}) 
83 
(\<lambda>S. if finite (Inf S) then Inf S else {})" 

84 
by transfer_prover 

85 

86 
lemma Inf_fset_transfer: 

87 
assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "bi_total A" 

55938  88 
shows "(rel_set (rel_set A) ===> rel_set A) (\<lambda>A. if finite (Inf A) then Inf A else {}) 
53953  89 
(\<lambda>A. if finite (Inf A) then Inf A else {})" 
90 
by transfer_prover 

91 

92 
lift_definition Inf_fset :: "'a fset set \<Rightarrow> 'a fset" is "\<lambda>A. if finite (Inf A) then Inf A else {}" 

93 
parametric right_total_Inf_fset_transfer Inf_fset_transfer by simp 

94 

95 
lemma Sup_fset_transfer: 

96 
assumes [transfer_rule]: "bi_unique A" 

55938  97 
shows "(rel_set (rel_set A) ===> rel_set A) (\<lambda>A. if finite (Sup A) then Sup A else {}) 
53953  98 
(\<lambda>A. if finite (Sup A) then Sup A else {})" by transfer_prover 
99 

100 
lift_definition Sup_fset :: "'a fset set \<Rightarrow> 'a fset" is "\<lambda>A. if finite (Sup A) then Sup A else {}" 

101 
parametric Sup_fset_transfer by simp 

102 

103 
lemma finite_Sup: "\<exists>z. finite z \<and> (\<forall>a. a \<in> X \<longrightarrow> a \<le> z) \<Longrightarrow> finite (Sup X)" 

104 
by (auto intro: finite_subset) 

105 

55938  106 
lemma transfer_bdd_below[transfer_rule]: "(rel_set (pcr_fset op =) ===> op =) bdd_below bdd_below" 
54258
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54014
diff
changeset

107 
by auto 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54014
diff
changeset

108 

53953  109 
instance 
110 
proof 

111 
fix x z :: "'a fset" 

112 
fix X :: "'a fset set" 

113 
{ 

54258
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54014
diff
changeset

114 
assume "x \<in> X" "bdd_below X" 
53953  115 
then show "Inf X \<subseteq> x" by transfer auto 
116 
next 

117 
assume "X \<noteq> {}" "(\<And>x. x \<in> X \<Longrightarrow> z \<subseteq> x)" 

118 
then show "z \<subseteq> Inf X" by transfer (clarsimp, blast) 

119 
next 

54258
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54014
diff
changeset

120 
assume "x \<in> X" "bdd_above X" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54014
diff
changeset

121 
then obtain z where "x \<in> X" "(\<And>x. x \<in> X \<Longrightarrow> x \<subseteq> z)" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54014
diff
changeset

122 
by (auto simp: bdd_above_def) 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54014
diff
changeset

123 
then show "x \<subseteq> Sup X" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54014
diff
changeset

124 
by transfer (auto intro!: finite_Sup) 
53953  125 
next 
126 
assume "X \<noteq> {}" "(\<And>x. x \<in> X \<Longrightarrow> x \<subseteq> z)" 

127 
then show "Sup X \<subseteq> z" by transfer (clarsimp, blast) 

128 
} 

129 
qed 

130 
end 

131 

132 
instantiation fset :: (finite) complete_lattice 

133 
begin 

134 

135 
lift_definition top_fset :: "'a fset" is UNIV parametric right_total_UNIV_transfer UNIV_transfer by simp 

136 

137 
instance by default (transfer, auto)+ 

138 
end 

139 

140 
instantiation fset :: (finite) complete_boolean_algebra 

141 
begin 

142 

143 
lift_definition uminus_fset :: "'a fset \<Rightarrow> 'a fset" is uminus 

144 
parametric right_total_Compl_transfer Compl_transfer by simp 

145 

56166  146 
instance by (default, simp_all only: INF_def SUP_def) (transfer, simp add: Compl_partition Diff_eq)+ 
53953  147 

148 
end 

149 

150 
abbreviation fUNIV :: "'a::finite fset" where "fUNIV \<equiv> top" 

151 
abbreviation fuminus :: "'a::finite fset \<Rightarrow> 'a fset" (" _" [81] 80) where " x \<equiv> uminus x" 

152 

55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

153 

53953  154 
subsection {* Other operations *} 
155 

156 
lift_definition finsert :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is insert parametric Lifting_Set.insert_transfer 

157 
by simp 

158 

159 
syntax 

160 
"_insert_fset" :: "args => 'a fset" ("{(_)}") 

161 

162 
translations 

163 
"{x, xs}" == "CONST finsert x {xs}" 

164 
"{x}" == "CONST finsert x {}" 

165 

166 
lift_definition fmember :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "\<in>" 50) is Set.member 

55565
f663fc1e653b
simplify proofs because of the stronger reflexivity prover
kuncar
parents:
55414
diff
changeset

167 
parametric member_transfer . 
53953  168 

169 
abbreviation notin_fset :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "\<notin>" 50) where "x \<notin> S \<equiv> \<not> (x \<in> S)" 

170 

171 
context 

172 
begin 

55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

173 

53953  174 
interpretation lifting_syntax . 
175 

176 
lift_definition ffilter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is Set.filter 

177 
parametric Lifting_Set.filter_transfer unfolding Set.filter_def by simp 

178 

179 
lift_definition fPow :: "'a fset \<Rightarrow> 'a fset fset" is Pow parametric Pow_transfer 

55732  180 
by (simp add: finite_subset) 
53953  181 

55565
f663fc1e653b
simplify proofs because of the stronger reflexivity prover
kuncar
parents:
55414
diff
changeset

182 
lift_definition fcard :: "'a fset \<Rightarrow> nat" is card parametric card_transfer . 
53953  183 

184 
lift_definition fimage :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" (infixr "`" 90) is image 

185 
parametric image_transfer by simp 

186 

55565
f663fc1e653b
simplify proofs because of the stronger reflexivity prover
kuncar
parents:
55414
diff
changeset

187 
lift_definition fthe_elem :: "'a fset \<Rightarrow> 'a" is the_elem . 
53953  188 

55738  189 
lift_definition fbind :: "'a fset \<Rightarrow> ('a \<Rightarrow> 'b fset) \<Rightarrow> 'b fset" is Set.bind parametric bind_transfer 
190 
by (simp add: Set.bind_def) 

53953  191 

55732  192 
lift_definition ffUnion :: "'a fset fset \<Rightarrow> 'a fset" is Union parametric Union_transfer by simp 
53953  193 

55565
f663fc1e653b
simplify proofs because of the stronger reflexivity prover
kuncar
parents:
55414
diff
changeset

194 
lift_definition fBall :: "'a fset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" is Ball parametric Ball_transfer . 
f663fc1e653b
simplify proofs because of the stronger reflexivity prover
kuncar
parents:
55414
diff
changeset

195 
lift_definition fBex :: "'a fset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" is Bex parametric Bex_transfer . 
53953  196 

55565
f663fc1e653b
simplify proofs because of the stronger reflexivity prover
kuncar
parents:
55414
diff
changeset

197 
lift_definition ffold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" is Finite_Set.fold . 
53963  198 

55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

199 

53953  200 
subsection {* Transferred lemmas from Set.thy *} 
201 

202 
lemmas fset_eqI = set_eqI[Transfer.transferred] 

203 
lemmas fset_eq_iff[no_atp] = set_eq_iff[Transfer.transferred] 

204 
lemmas fBallI[intro!] = ballI[Transfer.transferred] 

205 
lemmas fbspec[dest?] = bspec[Transfer.transferred] 

206 
lemmas fBallE[elim] = ballE[Transfer.transferred] 

207 
lemmas fBexI[intro] = bexI[Transfer.transferred] 

208 
lemmas rev_fBexI[intro?] = rev_bexI[Transfer.transferred] 

209 
lemmas fBexCI = bexCI[Transfer.transferred] 

210 
lemmas fBexE[elim!] = bexE[Transfer.transferred] 

211 
lemmas fBall_triv[simp] = ball_triv[Transfer.transferred] 

212 
lemmas fBex_triv[simp] = bex_triv[Transfer.transferred] 

213 
lemmas fBex_triv_one_point1[simp] = bex_triv_one_point1[Transfer.transferred] 

214 
lemmas fBex_triv_one_point2[simp] = bex_triv_one_point2[Transfer.transferred] 

215 
lemmas fBex_one_point1[simp] = bex_one_point1[Transfer.transferred] 

216 
lemmas fBex_one_point2[simp] = bex_one_point2[Transfer.transferred] 

217 
lemmas fBall_one_point1[simp] = ball_one_point1[Transfer.transferred] 

218 
lemmas fBall_one_point2[simp] = ball_one_point2[Transfer.transferred] 

219 
lemmas fBall_conj_distrib = ball_conj_distrib[Transfer.transferred] 

220 
lemmas fBex_disj_distrib = bex_disj_distrib[Transfer.transferred] 

221 
lemmas fBall_cong = ball_cong[Transfer.transferred] 

222 
lemmas fBex_cong = bex_cong[Transfer.transferred] 

53964  223 
lemmas fsubsetI[intro!] = subsetI[Transfer.transferred] 
224 
lemmas fsubsetD[elim, intro?] = subsetD[Transfer.transferred] 

225 
lemmas rev_fsubsetD[no_atp,intro?] = rev_subsetD[Transfer.transferred] 

226 
lemmas fsubsetCE[no_atp,elim] = subsetCE[Transfer.transferred] 

227 
lemmas fsubset_eq[no_atp] = subset_eq[Transfer.transferred] 

228 
lemmas contra_fsubsetD[no_atp] = contra_subsetD[Transfer.transferred] 

229 
lemmas fsubset_refl = subset_refl[Transfer.transferred] 

230 
lemmas fsubset_trans = subset_trans[Transfer.transferred] 

53953  231 
lemmas fset_rev_mp = set_rev_mp[Transfer.transferred] 
232 
lemmas fset_mp = set_mp[Transfer.transferred] 

53964  233 
lemmas fsubset_not_fsubset_eq[code] = subset_not_subset_eq[Transfer.transferred] 
53953  234 
lemmas eq_fmem_trans = eq_mem_trans[Transfer.transferred] 
53964  235 
lemmas fsubset_antisym[intro!] = subset_antisym[Transfer.transferred] 
53953  236 
lemmas fequalityD1 = equalityD1[Transfer.transferred] 
237 
lemmas fequalityD2 = equalityD2[Transfer.transferred] 

238 
lemmas fequalityE = equalityE[Transfer.transferred] 

239 
lemmas fequalityCE[elim] = equalityCE[Transfer.transferred] 

240 
lemmas eqfset_imp_iff = eqset_imp_iff[Transfer.transferred] 

241 
lemmas eqfelem_imp_iff = eqelem_imp_iff[Transfer.transferred] 

242 
lemmas fempty_iff[simp] = empty_iff[Transfer.transferred] 

53964  243 
lemmas fempty_fsubsetI[iff] = empty_subsetI[Transfer.transferred] 
53953  244 
lemmas equalsffemptyI = equals0I[Transfer.transferred] 
245 
lemmas equalsffemptyD = equals0D[Transfer.transferred] 

246 
lemmas fBall_fempty[simp] = ball_empty[Transfer.transferred] 

247 
lemmas fBex_fempty[simp] = bex_empty[Transfer.transferred] 

248 
lemmas fPow_iff[iff] = Pow_iff[Transfer.transferred] 

249 
lemmas fPowI = PowI[Transfer.transferred] 

250 
lemmas fPowD = PowD[Transfer.transferred] 

251 
lemmas fPow_bottom = Pow_bottom[Transfer.transferred] 

252 
lemmas fPow_top = Pow_top[Transfer.transferred] 

253 
lemmas fPow_not_fempty = Pow_not_empty[Transfer.transferred] 

254 
lemmas finter_iff[simp] = Int_iff[Transfer.transferred] 

255 
lemmas finterI[intro!] = IntI[Transfer.transferred] 

256 
lemmas finterD1 = IntD1[Transfer.transferred] 

257 
lemmas finterD2 = IntD2[Transfer.transferred] 

258 
lemmas finterE[elim!] = IntE[Transfer.transferred] 

259 
lemmas funion_iff[simp] = Un_iff[Transfer.transferred] 

260 
lemmas funionI1[elim?] = UnI1[Transfer.transferred] 

261 
lemmas funionI2[elim?] = UnI2[Transfer.transferred] 

262 
lemmas funionCI[intro!] = UnCI[Transfer.transferred] 

263 
lemmas funionE[elim!] = UnE[Transfer.transferred] 

264 
lemmas fminus_iff[simp] = Diff_iff[Transfer.transferred] 

265 
lemmas fminusI[intro!] = DiffI[Transfer.transferred] 

266 
lemmas fminusD1 = DiffD1[Transfer.transferred] 

267 
lemmas fminusD2 = DiffD2[Transfer.transferred] 

268 
lemmas fminusE[elim!] = DiffE[Transfer.transferred] 

269 
lemmas finsert_iff[simp] = insert_iff[Transfer.transferred] 

270 
lemmas finsertI1 = insertI1[Transfer.transferred] 

271 
lemmas finsertI2 = insertI2[Transfer.transferred] 

272 
lemmas finsertE[elim!] = insertE[Transfer.transferred] 

273 
lemmas finsertCI[intro!] = insertCI[Transfer.transferred] 

53964  274 
lemmas fsubset_finsert_iff = subset_insert_iff[Transfer.transferred] 
53953  275 
lemmas finsert_ident = insert_ident[Transfer.transferred] 
276 
lemmas fsingletonI[intro!,no_atp] = singletonI[Transfer.transferred] 

277 
lemmas fsingletonD[dest!,no_atp] = singletonD[Transfer.transferred] 

278 
lemmas fsingleton_iff = singleton_iff[Transfer.transferred] 

279 
lemmas fsingleton_inject[dest!] = singleton_inject[Transfer.transferred] 

280 
lemmas fsingleton_finsert_inj_eq[iff,no_atp] = singleton_insert_inj_eq[Transfer.transferred] 

281 
lemmas fsingleton_finsert_inj_eq'[iff,no_atp] = singleton_insert_inj_eq'[Transfer.transferred] 

53964  282 
lemmas fsubset_fsingletonD = subset_singletonD[Transfer.transferred] 
53953  283 
lemmas fminus_single_finsert = diff_single_insert[Transfer.transferred] 
284 
lemmas fdoubleton_eq_iff = doubleton_eq_iff[Transfer.transferred] 

285 
lemmas funion_fsingleton_iff = Un_singleton_iff[Transfer.transferred] 

286 
lemmas fsingleton_funion_iff = singleton_Un_iff[Transfer.transferred] 

287 
lemmas fimage_eqI[simp, intro] = image_eqI[Transfer.transferred] 

288 
lemmas fimageI = imageI[Transfer.transferred] 

289 
lemmas rev_fimage_eqI = rev_image_eqI[Transfer.transferred] 

290 
lemmas fimageE[elim!] = imageE[Transfer.transferred] 

291 
lemmas Compr_fimage_eq = Compr_image_eq[Transfer.transferred] 

292 
lemmas fimage_funion = image_Un[Transfer.transferred] 

293 
lemmas fimage_iff = image_iff[Transfer.transferred] 

53964  294 
lemmas fimage_fsubset_iff[no_atp] = image_subset_iff[Transfer.transferred] 
295 
lemmas fimage_fsubsetI = image_subsetI[Transfer.transferred] 

53953  296 
lemmas fimage_ident[simp] = image_ident[Transfer.transferred] 
297 
lemmas split_if_fmem1 = split_if_mem1[Transfer.transferred] 

298 
lemmas split_if_fmem2 = split_if_mem2[Transfer.transferred] 

53964  299 
lemmas pfsubsetI[intro!,no_atp] = psubsetI[Transfer.transferred] 
300 
lemmas pfsubsetE[elim!,no_atp] = psubsetE[Transfer.transferred] 

301 
lemmas pfsubset_finsert_iff = psubset_insert_iff[Transfer.transferred] 

302 
lemmas pfsubset_eq = psubset_eq[Transfer.transferred] 

303 
lemmas pfsubset_imp_fsubset = psubset_imp_subset[Transfer.transferred] 

304 
lemmas pfsubset_trans = psubset_trans[Transfer.transferred] 

305 
lemmas pfsubsetD = psubsetD[Transfer.transferred] 

306 
lemmas pfsubset_fsubset_trans = psubset_subset_trans[Transfer.transferred] 

307 
lemmas fsubset_pfsubset_trans = subset_psubset_trans[Transfer.transferred] 

308 
lemmas pfsubset_imp_ex_fmem = psubset_imp_ex_mem[Transfer.transferred] 

53953  309 
lemmas fimage_fPow_mono = image_Pow_mono[Transfer.transferred] 
310 
lemmas fimage_fPow_surj = image_Pow_surj[Transfer.transferred] 

53964  311 
lemmas fsubset_finsertI = subset_insertI[Transfer.transferred] 
312 
lemmas fsubset_finsertI2 = subset_insertI2[Transfer.transferred] 

313 
lemmas fsubset_finsert = subset_insert[Transfer.transferred] 

53953  314 
lemmas funion_upper1 = Un_upper1[Transfer.transferred] 
315 
lemmas funion_upper2 = Un_upper2[Transfer.transferred] 

316 
lemmas funion_least = Un_least[Transfer.transferred] 

317 
lemmas finter_lower1 = Int_lower1[Transfer.transferred] 

318 
lemmas finter_lower2 = Int_lower2[Transfer.transferred] 

319 
lemmas finter_greatest = Int_greatest[Transfer.transferred] 

53964  320 
lemmas fminus_fsubset = Diff_subset[Transfer.transferred] 
321 
lemmas fminus_fsubset_conv = Diff_subset_conv[Transfer.transferred] 

322 
lemmas fsubset_fempty[simp] = subset_empty[Transfer.transferred] 

323 
lemmas not_pfsubset_fempty[iff] = not_psubset_empty[Transfer.transferred] 

53953  324 
lemmas finsert_is_funion = insert_is_Un[Transfer.transferred] 
325 
lemmas finsert_not_fempty[simp] = insert_not_empty[Transfer.transferred] 

326 
lemmas fempty_not_finsert = empty_not_insert[Transfer.transferred] 

327 
lemmas finsert_absorb = insert_absorb[Transfer.transferred] 

328 
lemmas finsert_absorb2[simp] = insert_absorb2[Transfer.transferred] 

329 
lemmas finsert_commute = insert_commute[Transfer.transferred] 

53964  330 
lemmas finsert_fsubset[simp] = insert_subset[Transfer.transferred] 
53953  331 
lemmas finsert_inter_finsert[simp] = insert_inter_insert[Transfer.transferred] 
332 
lemmas finsert_disjoint[simp,no_atp] = insert_disjoint[Transfer.transferred] 

333 
lemmas disjoint_finsert[simp,no_atp] = disjoint_insert[Transfer.transferred] 

334 
lemmas fimage_fempty[simp] = image_empty[Transfer.transferred] 

335 
lemmas fimage_finsert[simp] = image_insert[Transfer.transferred] 

336 
lemmas fimage_constant = image_constant[Transfer.transferred] 

337 
lemmas fimage_constant_conv = image_constant_conv[Transfer.transferred] 

338 
lemmas fimage_fimage = image_image[Transfer.transferred] 

339 
lemmas finsert_fimage[simp] = insert_image[Transfer.transferred] 

340 
lemmas fimage_is_fempty[iff] = image_is_empty[Transfer.transferred] 

341 
lemmas fempty_is_fimage[iff] = empty_is_image[Transfer.transferred] 

342 
lemmas fimage_cong = image_cong[Transfer.transferred] 

53964  343 
lemmas fimage_finter_fsubset = image_Int_subset[Transfer.transferred] 
344 
lemmas fimage_fminus_fsubset = image_diff_subset[Transfer.transferred] 

53953  345 
lemmas finter_absorb = Int_absorb[Transfer.transferred] 
346 
lemmas finter_left_absorb = Int_left_absorb[Transfer.transferred] 

347 
lemmas finter_commute = Int_commute[Transfer.transferred] 

348 
lemmas finter_left_commute = Int_left_commute[Transfer.transferred] 

349 
lemmas finter_assoc = Int_assoc[Transfer.transferred] 

350 
lemmas finter_ac = Int_ac[Transfer.transferred] 

351 
lemmas finter_absorb1 = Int_absorb1[Transfer.transferred] 

352 
lemmas finter_absorb2 = Int_absorb2[Transfer.transferred] 

353 
lemmas finter_fempty_left = Int_empty_left[Transfer.transferred] 

354 
lemmas finter_fempty_right = Int_empty_right[Transfer.transferred] 

355 
lemmas disjoint_iff_fnot_equal = disjoint_iff_not_equal[Transfer.transferred] 

356 
lemmas finter_funion_distrib = Int_Un_distrib[Transfer.transferred] 

357 
lemmas finter_funion_distrib2 = Int_Un_distrib2[Transfer.transferred] 

53964  358 
lemmas finter_fsubset_iff[no_atp, simp] = Int_subset_iff[Transfer.transferred] 
53953  359 
lemmas funion_absorb = Un_absorb[Transfer.transferred] 
360 
lemmas funion_left_absorb = Un_left_absorb[Transfer.transferred] 

361 
lemmas funion_commute = Un_commute[Transfer.transferred] 

362 
lemmas funion_left_commute = Un_left_commute[Transfer.transferred] 

363 
lemmas funion_assoc = Un_assoc[Transfer.transferred] 

364 
lemmas funion_ac = Un_ac[Transfer.transferred] 

365 
lemmas funion_absorb1 = Un_absorb1[Transfer.transferred] 

366 
lemmas funion_absorb2 = Un_absorb2[Transfer.transferred] 

367 
lemmas funion_fempty_left = Un_empty_left[Transfer.transferred] 

368 
lemmas funion_fempty_right = Un_empty_right[Transfer.transferred] 

369 
lemmas funion_finsert_left[simp] = Un_insert_left[Transfer.transferred] 

370 
lemmas funion_finsert_right[simp] = Un_insert_right[Transfer.transferred] 

371 
lemmas finter_finsert_left = Int_insert_left[Transfer.transferred] 

372 
lemmas finter_finsert_left_ifffempty[simp] = Int_insert_left_if0[Transfer.transferred] 

373 
lemmas finter_finsert_left_if1[simp] = Int_insert_left_if1[Transfer.transferred] 

374 
lemmas finter_finsert_right = Int_insert_right[Transfer.transferred] 

375 
lemmas finter_finsert_right_ifffempty[simp] = Int_insert_right_if0[Transfer.transferred] 

376 
lemmas finter_finsert_right_if1[simp] = Int_insert_right_if1[Transfer.transferred] 

377 
lemmas funion_finter_distrib = Un_Int_distrib[Transfer.transferred] 

378 
lemmas funion_finter_distrib2 = Un_Int_distrib2[Transfer.transferred] 

379 
lemmas funion_finter_crazy = Un_Int_crazy[Transfer.transferred] 

53964  380 
lemmas fsubset_funion_eq = subset_Un_eq[Transfer.transferred] 
53953  381 
lemmas funion_fempty[iff] = Un_empty[Transfer.transferred] 
53964  382 
lemmas funion_fsubset_iff[no_atp, simp] = Un_subset_iff[Transfer.transferred] 
53953  383 
lemmas funion_fminus_finter = Un_Diff_Int[Transfer.transferred] 
384 
lemmas fminus_finter2 = Diff_Int2[Transfer.transferred] 

385 
lemmas funion_finter_assoc_eq = Un_Int_assoc_eq[Transfer.transferred] 

386 
lemmas fBall_funion = ball_Un[Transfer.transferred] 

387 
lemmas fBex_funion = bex_Un[Transfer.transferred] 

388 
lemmas fminus_eq_fempty_iff[simp,no_atp] = Diff_eq_empty_iff[Transfer.transferred] 

389 
lemmas fminus_cancel[simp] = Diff_cancel[Transfer.transferred] 

390 
lemmas fminus_idemp[simp] = Diff_idemp[Transfer.transferred] 

391 
lemmas fminus_triv = Diff_triv[Transfer.transferred] 

392 
lemmas fempty_fminus[simp] = empty_Diff[Transfer.transferred] 

393 
lemmas fminus_fempty[simp] = Diff_empty[Transfer.transferred] 

394 
lemmas fminus_finsertffempty[simp,no_atp] = Diff_insert0[Transfer.transferred] 

395 
lemmas fminus_finsert = Diff_insert[Transfer.transferred] 

396 
lemmas fminus_finsert2 = Diff_insert2[Transfer.transferred] 

397 
lemmas finsert_fminus_if = insert_Diff_if[Transfer.transferred] 

398 
lemmas finsert_fminus1[simp] = insert_Diff1[Transfer.transferred] 

399 
lemmas finsert_fminus_single[simp] = insert_Diff_single[Transfer.transferred] 

400 
lemmas finsert_fminus = insert_Diff[Transfer.transferred] 

401 
lemmas fminus_finsert_absorb = Diff_insert_absorb[Transfer.transferred] 

402 
lemmas fminus_disjoint[simp] = Diff_disjoint[Transfer.transferred] 

403 
lemmas fminus_partition = Diff_partition[Transfer.transferred] 

404 
lemmas double_fminus = double_diff[Transfer.transferred] 

405 
lemmas funion_fminus_cancel[simp] = Un_Diff_cancel[Transfer.transferred] 

406 
lemmas funion_fminus_cancel2[simp] = Un_Diff_cancel2[Transfer.transferred] 

407 
lemmas fminus_funion = Diff_Un[Transfer.transferred] 

408 
lemmas fminus_finter = Diff_Int[Transfer.transferred] 

409 
lemmas funion_fminus = Un_Diff[Transfer.transferred] 

410 
lemmas finter_fminus = Int_Diff[Transfer.transferred] 

411 
lemmas fminus_finter_distrib = Diff_Int_distrib[Transfer.transferred] 

412 
lemmas fminus_finter_distrib2 = Diff_Int_distrib2[Transfer.transferred] 

413 
lemmas fUNIV_bool[no_atp] = UNIV_bool[Transfer.transferred] 

414 
lemmas fPow_fempty[simp] = Pow_empty[Transfer.transferred] 

415 
lemmas fPow_finsert = Pow_insert[Transfer.transferred] 

53964  416 
lemmas funion_fPow_fsubset = Un_Pow_subset[Transfer.transferred] 
53953  417 
lemmas fPow_finter_eq[simp] = Pow_Int_eq[Transfer.transferred] 
53964  418 
lemmas fset_eq_fsubset = set_eq_subset[Transfer.transferred] 
419 
lemmas fsubset_iff[no_atp] = subset_iff[Transfer.transferred] 

420 
lemmas fsubset_iff_pfsubset_eq = subset_iff_psubset_eq[Transfer.transferred] 

53953  421 
lemmas all_not_fin_conv[simp] = all_not_in_conv[Transfer.transferred] 
422 
lemmas ex_fin_conv = ex_in_conv[Transfer.transferred] 

423 
lemmas fimage_mono = image_mono[Transfer.transferred] 

424 
lemmas fPow_mono = Pow_mono[Transfer.transferred] 

425 
lemmas finsert_mono = insert_mono[Transfer.transferred] 

426 
lemmas funion_mono = Un_mono[Transfer.transferred] 

427 
lemmas finter_mono = Int_mono[Transfer.transferred] 

428 
lemmas fminus_mono = Diff_mono[Transfer.transferred] 

429 
lemmas fin_mono = in_mono[Transfer.transferred] 

430 
lemmas fthe_felem_eq[simp] = the_elem_eq[Transfer.transferred] 

431 
lemmas fLeast_mono = Least_mono[Transfer.transferred] 

432 
lemmas fbind_fbind = bind_bind[Transfer.transferred] 

433 
lemmas fempty_fbind[simp] = empty_bind[Transfer.transferred] 

434 
lemmas nonfempty_fbind_const = nonempty_bind_const[Transfer.transferred] 

435 
lemmas fbind_const = bind_const[Transfer.transferred] 

436 
lemmas ffmember_filter[simp] = member_filter[Transfer.transferred] 

437 
lemmas fequalityI = equalityI[Transfer.transferred] 

438 

55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

439 

53953  440 
subsection {* Additional lemmas*} 
441 

53969  442 
subsubsection {* @{text fsingleton} *} 
53953  443 

444 
lemmas fsingletonE = fsingletonD [elim_format] 

445 

55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

446 

53969  447 
subsubsection {* @{text femepty} *} 
53953  448 

449 
lemma fempty_ffilter[simp]: "ffilter (\<lambda>_. False) A = {}" 

450 
by transfer auto 

451 

452 
(* FIXME, transferred doesn't work here *) 

453 
lemma femptyE [elim!]: "a \<in> {} \<Longrightarrow> P" 

454 
by simp 

455 

55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

456 

53969  457 
subsubsection {* @{text fset} *} 
53953  458 

53963  459 
lemmas fset_simps[simp] = bot_fset.rep_eq finsert.rep_eq 
53953  460 

461 
lemma finite_fset [simp]: 

462 
shows "finite (fset S)" 

463 
by transfer simp 

464 

53963  465 
lemmas fset_cong = fset_inject 
53953  466 

467 
lemma filter_fset [simp]: 

468 
shows "fset (ffilter P xs) = Collect P \<inter> fset xs" 

469 
by transfer auto 

470 

53963  471 
lemma notin_fset: "x \<notin> S \<longleftrightarrow> x \<notin> fset S" by (simp add: fmember.rep_eq) 
472 

473 
lemmas inter_fset[simp] = inf_fset.rep_eq 

53953  474 

53963  475 
lemmas union_fset[simp] = sup_fset.rep_eq 
53953  476 

53963  477 
lemmas minus_fset[simp] = minus_fset.rep_eq 
53953  478 

55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

479 

53969  480 
subsubsection {* @{text filter_fset} *} 
53953  481 

482 
lemma subset_ffilter: 

483 
"ffilter P A \<subseteq> ffilter Q A = (\<forall> x. x \<in> A \<longrightarrow> P x \<longrightarrow> Q x)" 

484 
by transfer auto 

485 

486 
lemma eq_ffilter: 

487 
"(ffilter P A = ffilter Q A) = (\<forall>x. x \<in> A \<longrightarrow> P x = Q x)" 

488 
by transfer auto 

489 

53964  490 
lemma pfsubset_ffilter: 
53953  491 
"(\<And>x. x \<in> A \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x \<in> A & \<not> P x & Q x) \<Longrightarrow> 
492 
ffilter P A \<subset> ffilter Q A" 

493 
unfolding less_fset_def by (auto simp add: subset_ffilter eq_ffilter) 

494 

55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

495 

53969  496 
subsubsection {* @{text finsert} *} 
53953  497 

498 
(* FIXME, transferred doesn't work here *) 

499 
lemma set_finsert: 

500 
assumes "x \<in> A" 

501 
obtains B where "A = finsert x B" and "x \<notin> B" 

502 
using assms by transfer (metis Set.set_insert finite_insert) 

503 

504 
lemma mk_disjoint_finsert: "a \<in> A \<Longrightarrow> \<exists>B. A = finsert a B \<and> a \<notin> B" 

505 
by (rule_tac x = "A  {a}" in exI, blast) 

506 

55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

507 

53969  508 
subsubsection {* @{text fimage} *} 
53953  509 

510 
lemma subset_fimage_iff: "(B \<subseteq> f`A) = (\<exists> AA. AA \<subseteq> A \<and> B = f`AA)" 

511 
by transfer (metis mem_Collect_eq rev_finite_subset subset_image_iff) 

512 

55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

513 

53953  514 
subsubsection {* bounded quantification *} 
515 

516 
lemma bex_simps [simp, no_atp]: 

517 
"\<And>A P Q. fBex A (\<lambda>x. P x \<and> Q) = (fBex A P \<and> Q)" 

518 
"\<And>A P Q. fBex A (\<lambda>x. P \<and> Q x) = (P \<and> fBex A Q)" 

519 
"\<And>P. fBex {} P = False" 

520 
"\<And>a B P. fBex (finsert a B) P = (P a \<or> fBex B P)" 

521 
"\<And>A P f. fBex (f ` A) P = fBex A (\<lambda>x. P (f x))" 

522 
"\<And>A P. (\<not> fBex A P) = fBall A (\<lambda>x. \<not> P x)" 

523 
by auto 

524 

525 
lemma ball_simps [simp, no_atp]: 

526 
"\<And>A P Q. fBall A (\<lambda>x. P x \<or> Q) = (fBall A P \<or> Q)" 

527 
"\<And>A P Q. fBall A (\<lambda>x. P \<or> Q x) = (P \<or> fBall A Q)" 

528 
"\<And>A P Q. fBall A (\<lambda>x. P \<longrightarrow> Q x) = (P \<longrightarrow> fBall A Q)" 

529 
"\<And>A P Q. fBall A (\<lambda>x. P x \<longrightarrow> Q) = (fBex A P \<longrightarrow> Q)" 

530 
"\<And>P. fBall {} P = True" 

531 
"\<And>a B P. fBall (finsert a B) P = (P a \<and> fBall B P)" 

532 
"\<And>A P f. fBall (f ` A) P = fBall A (\<lambda>x. P (f x))" 

533 
"\<And>A P. (\<not> fBall A P) = fBex A (\<lambda>x. \<not> P x)" 

534 
by auto 

535 

536 
lemma atomize_fBall: 

537 
"(\<And>x. x \<in> A ==> P x) == Trueprop (fBall A (\<lambda>x. P x))" 

538 
apply (simp only: atomize_all atomize_imp) 

539 
apply (rule equal_intr_rule) 

540 
by (transfer, simp)+ 

541 

53963  542 
end 
543 

55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

544 

53969  545 
subsubsection {* @{text fcard} *} 
53963  546 

53964  547 
(* FIXME: improve transferred to handle bounded meta quantification *) 
548 

53963  549 
lemma fcard_fempty: 
550 
"fcard {} = 0" 

551 
by transfer (rule card_empty) 

552 

553 
lemma fcard_finsert_disjoint: 

554 
"x \<notin> A \<Longrightarrow> fcard (finsert x A) = Suc (fcard A)" 

555 
by transfer (rule card_insert_disjoint) 

556 

557 
lemma fcard_finsert_if: 

558 
"fcard (finsert x A) = (if x \<in> A then fcard A else Suc (fcard A))" 

559 
by transfer (rule card_insert_if) 

560 

561 
lemma card_0_eq [simp, no_atp]: 

562 
"fcard A = 0 \<longleftrightarrow> A = {}" 

563 
by transfer (rule card_0_eq) 

564 

565 
lemma fcard_Suc_fminus1: 

566 
"x \<in> A \<Longrightarrow> Suc (fcard (A  {x})) = fcard A" 

567 
by transfer (rule card_Suc_Diff1) 

568 

569 
lemma fcard_fminus_fsingleton: 

570 
"x \<in> A \<Longrightarrow> fcard (A  {x}) = fcard A  1" 

571 
by transfer (rule card_Diff_singleton) 

572 

573 
lemma fcard_fminus_fsingleton_if: 

574 
"fcard (A  {x}) = (if x \<in> A then fcard A  1 else fcard A)" 

575 
by transfer (rule card_Diff_singleton_if) 

576 

577 
lemma fcard_fminus_finsert[simp]: 

578 
assumes "a \<in> A" and "a \<notin> B" 

579 
shows "fcard (A  finsert a B) = fcard (A  B)  1" 

580 
using assms by transfer (rule card_Diff_insert) 

581 

582 
lemma fcard_finsert: "fcard (finsert x A) = Suc (fcard (A  {x}))" 

583 
by transfer (rule card_insert) 

584 

585 
lemma fcard_finsert_le: "fcard A \<le> fcard (finsert x A)" 

586 
by transfer (rule card_insert_le) 

587 

588 
lemma fcard_mono: 

589 
"A \<subseteq> B \<Longrightarrow> fcard A \<le> fcard B" 

590 
by transfer (rule card_mono) 

591 

592 
lemma fcard_seteq: "A \<subseteq> B \<Longrightarrow> fcard B \<le> fcard A \<Longrightarrow> A = B" 

593 
by transfer (rule card_seteq) 

594 

595 
lemma pfsubset_fcard_mono: "A \<subset> B \<Longrightarrow> fcard A < fcard B" 

596 
by transfer (rule psubset_card_mono) 

597 

598 
lemma fcard_funion_finter: 

599 
"fcard A + fcard B = fcard (A \<union> B) + fcard (A \<inter> B)" 

600 
by transfer (rule card_Un_Int) 

601 

602 
lemma fcard_funion_disjoint: 

603 
"A \<inter> B = {} \<Longrightarrow> fcard (A \<union> B) = fcard A + fcard B" 

604 
by transfer (rule card_Un_disjoint) 

605 

606 
lemma fcard_funion_fsubset: 

607 
"B \<subseteq> A \<Longrightarrow> fcard (A  B) = fcard A  fcard B" 

608 
by transfer (rule card_Diff_subset) 

609 

610 
lemma diff_fcard_le_fcard_fminus: 

611 
"fcard A  fcard B \<le> fcard(A  B)" 

612 
by transfer (rule diff_card_le_card_Diff) 

613 

614 
lemma fcard_fminus1_less: "x \<in> A \<Longrightarrow> fcard (A  {x}) < fcard A" 

615 
by transfer (rule card_Diff1_less) 

616 

617 
lemma fcard_fminus2_less: 

618 
"x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> fcard (A  {x}  {y}) < fcard A" 

619 
by transfer (rule card_Diff2_less) 

620 

621 
lemma fcard_fminus1_le: "fcard (A  {x}) \<le> fcard A" 

622 
by transfer (rule card_Diff1_le) 

623 

624 
lemma fcard_pfsubset: "A \<subseteq> B \<Longrightarrow> fcard A < fcard B \<Longrightarrow> A < B" 

625 
by transfer (rule card_psubset) 

626 

55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

627 

53969  628 
subsubsection {* @{text ffold} *} 
53963  629 

630 
(* FIXME: improve transferred to handle bounded meta quantification *) 

631 

632 
context comp_fun_commute 

633 
begin 

634 
lemmas ffold_empty[simp] = fold_empty[Transfer.transferred] 

635 

636 
lemma ffold_finsert [simp]: 

637 
assumes "x \<notin> A" 

638 
shows "ffold f z (finsert x A) = f x (ffold f z A)" 

639 
using assms by (transfer fixing: f) (rule fold_insert) 

640 

641 
lemma ffold_fun_left_comm: 

642 
"f x (ffold f z A) = ffold f (f x z) A" 

643 
by (transfer fixing: f) (rule fold_fun_left_comm) 

644 

645 
lemma ffold_finsert2: 

646 
"x \<notin> A \<Longrightarrow> ffold f z (finsert x A) = ffold f (f x z) A" 

647 
by (transfer fixing: f) (rule fold_insert2) 

648 

649 
lemma ffold_rec: 

650 
assumes "x \<in> A" 

651 
shows "ffold f z A = f x (ffold f z (A  {x}))" 

652 
using assms by (transfer fixing: f) (rule fold_rec) 

653 

654 
lemma ffold_finsert_fremove: 

655 
"ffold f z (finsert x A) = f x (ffold f z (A  {x}))" 

656 
by (transfer fixing: f) (rule fold_insert_remove) 

657 
end 

658 

659 
lemma ffold_fimage: 

660 
assumes "inj_on g (fset A)" 

661 
shows "ffold f z (g ` A) = ffold (f \<circ> g) z A" 

662 
using assms by transfer' (rule fold_image) 

663 

664 
lemma ffold_cong: 

665 
assumes "comp_fun_commute f" "comp_fun_commute g" 

666 
"\<And>x. x \<in> A \<Longrightarrow> f x = g x" 

667 
and "s = t" and "A = B" 

668 
shows "ffold f s A = ffold g t B" 

669 
using assms by transfer (metis Finite_Set.fold_cong) 

670 

671 
context comp_fun_idem 

672 
begin 

673 

674 
lemma ffold_finsert_idem: 

675 
"ffold f z (finsert x A) = f x (ffold f z A)" 

676 
by (transfer fixing: f) (rule fold_insert_idem) 

677 

678 
declare ffold_finsert [simp del] ffold_finsert_idem [simp] 

679 

680 
lemma ffold_finsert_idem2: 

681 
"ffold f z (finsert x A) = ffold f (f x z) A" 

682 
by (transfer fixing: f) (rule fold_insert_idem2) 

683 

684 
end 

685 

55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

686 

53953  687 
subsection {* Choice in fsets *} 
688 

689 
lemma fset_choice: 

690 
assumes "\<forall>x. x \<in> A \<longrightarrow> (\<exists>y. P x y)" 

691 
shows "\<exists>f. \<forall>x. x \<in> A \<longrightarrow> P x (f x)" 

692 
using assms by transfer metis 

693 

55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

694 

53953  695 
subsection {* Induction and Cases rules for fsets *} 
696 

697 
lemma fset_exhaust [case_names empty insert, cases type: fset]: 

698 
assumes fempty_case: "S = {} \<Longrightarrow> P" 

699 
and finsert_case: "\<And>x S'. S = finsert x S' \<Longrightarrow> P" 

700 
shows "P" 

701 
using assms by transfer blast 

702 

703 
lemma fset_induct [case_names empty insert]: 

704 
assumes fempty_case: "P {}" 

705 
and finsert_case: "\<And>x S. P S \<Longrightarrow> P (finsert x S)" 

706 
shows "P S" 

707 
proof  

708 
(* FIXME transfer and right_total vs. bi_total *) 

709 
note Domainp_forall_transfer[transfer_rule] 

710 
show ?thesis 

711 
using assms by transfer (auto intro: finite_induct) 

712 
qed 

713 

714 
lemma fset_induct_stronger [case_names empty insert, induct type: fset]: 

715 
assumes empty_fset_case: "P {}" 

716 
and insert_fset_case: "\<And>x S. \<lbrakk>x \<notin> S; P S\<rbrakk> \<Longrightarrow> P (finsert x S)" 

717 
shows "P S" 

718 
proof  

719 
(* FIXME transfer and right_total vs. bi_total *) 

720 
note Domainp_forall_transfer[transfer_rule] 

721 
show ?thesis 

722 
using assms by transfer (auto intro: finite_induct) 

723 
qed 

724 

725 
lemma fset_card_induct: 

726 
assumes empty_fset_case: "P {}" 

727 
and card_fset_Suc_case: "\<And>S T. Suc (fcard S) = (fcard T) \<Longrightarrow> P S \<Longrightarrow> P T" 

728 
shows "P S" 

729 
proof (induct S) 

730 
case empty 

731 
show "P {}" by (rule empty_fset_case) 

732 
next 

733 
case (insert x S) 

734 
have h: "P S" by fact 

735 
have "x \<notin> S" by fact 

736 
then have "Suc (fcard S) = fcard (finsert x S)" 

737 
by transfer auto 

738 
then show "P (finsert x S)" 

739 
using h card_fset_Suc_case by simp 

740 
qed 

741 

742 
lemma fset_strong_cases: 

743 
obtains "xs = {}" 

744 
 ys x where "x \<notin> ys" and "xs = finsert x ys" 

745 
by transfer blast 

746 

747 
lemma fset_induct2: 

748 
"P {} {} \<Longrightarrow> 

749 
(\<And>x xs. x \<notin> xs \<Longrightarrow> P (finsert x xs) {}) \<Longrightarrow> 

750 
(\<And>y ys. y \<notin> ys \<Longrightarrow> P {} (finsert y ys)) \<Longrightarrow> 

751 
(\<And>x xs y ys. \<lbrakk>P xs ys; x \<notin> xs; y \<notin> ys\<rbrakk> \<Longrightarrow> P (finsert x xs) (finsert y ys)) \<Longrightarrow> 

752 
P xsa ysa" 

753 
apply (induct xsa arbitrary: ysa) 

754 
apply (induct_tac x rule: fset_induct_stronger) 

755 
apply simp_all 

756 
apply (induct_tac xa rule: fset_induct_stronger) 

757 
apply simp_all 

758 
done 

759 

55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

760 

53953  761 
subsection {* Setup for Lifting/Transfer *} 
762 

763 
subsubsection {* Relator and predicator properties *} 

764 

55938  765 
lift_definition rel_fset :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'b fset \<Rightarrow> bool" is rel_set 
766 
parametric rel_set_transfer . 

53953  767 

55933  768 
lemma rel_fset_alt_def: "rel_fset R = (\<lambda>A B. (\<forall>x.\<exists>y. x\<in>A \<longrightarrow> y\<in>B \<and> R x y) 
53953  769 
\<and> (\<forall>y. \<exists>x. y\<in>B \<longrightarrow> x\<in>A \<and> R x y))" 
770 
apply (rule ext)+ 

771 
apply transfer' 

55938  772 
apply (subst rel_set_def[unfolded fun_eq_iff]) 
53953  773 
by blast 
774 

55938  775 
lemma finite_rel_set: 
53953  776 
assumes fin: "finite X" "finite Z" 
55938  777 
assumes R_S: "rel_set (R OO S) X Z" 
778 
shows "\<exists>Y. finite Y \<and> rel_set R X Y \<and> rel_set S Y Z" 

53953  779 
proof  
780 
obtain f where f: "\<forall>x\<in>X. R x (f x) \<and> (\<exists>z\<in>Z. S (f x) z)" 

781 
apply atomize_elim 

782 
apply (subst bchoice_iff[symmetric]) 

55938  783 
using R_S[unfolded rel_set_def OO_def] by blast 
53953  784 

785 
obtain g where g: "\<forall>z\<in>Z. S (g z) z \<and> (\<exists>x\<in>X. R x (g z))" 

786 
apply atomize_elim 

787 
apply (subst bchoice_iff[symmetric]) 

55938  788 
using R_S[unfolded rel_set_def OO_def] by blast 
53953  789 

790 
let ?Y = "f ` X \<union> g ` Z" 

791 
have "finite ?Y" by (simp add: fin) 

55938  792 
moreover have "rel_set R X ?Y" 
793 
unfolding rel_set_def 

53953  794 
using f g by clarsimp blast 
55938  795 
moreover have "rel_set S ?Y Z" 
796 
unfolding rel_set_def 

53953  797 
using f g by clarsimp blast 
798 
ultimately show ?thesis by metis 

799 
qed 

800 

801 
subsubsection {* Transfer rules for the Transfer package *} 

802 

803 
text {* Unconditional transfer rules *} 

804 

53963  805 
context 
806 
begin 

807 

808 
interpretation lifting_syntax . 

809 

53953  810 
lemmas fempty_transfer [transfer_rule] = empty_transfer[Transfer.transferred] 
811 

812 
lemma finsert_transfer [transfer_rule]: 

55933  813 
"(A ===> rel_fset A ===> rel_fset A) finsert finsert" 
55945  814 
unfolding rel_fun_def rel_fset_alt_def by blast 
53953  815 

816 
lemma funion_transfer [transfer_rule]: 

55933  817 
"(rel_fset A ===> rel_fset A ===> rel_fset A) funion funion" 
55945  818 
unfolding rel_fun_def rel_fset_alt_def by blast 
53953  819 

820 
lemma ffUnion_transfer [transfer_rule]: 

55933  821 
"(rel_fset (rel_fset A) ===> rel_fset A) ffUnion ffUnion" 
55945  822 
unfolding rel_fun_def rel_fset_alt_def by transfer (simp, fast) 
53953  823 

824 
lemma fimage_transfer [transfer_rule]: 

55933  825 
"((A ===> B) ===> rel_fset A ===> rel_fset B) fimage fimage" 
55945  826 
unfolding rel_fun_def rel_fset_alt_def by simp blast 
53953  827 

828 
lemma fBall_transfer [transfer_rule]: 

55933  829 
"(rel_fset A ===> (A ===> op =) ===> op =) fBall fBall" 
55945  830 
unfolding rel_fset_alt_def rel_fun_def by blast 
53953  831 

832 
lemma fBex_transfer [transfer_rule]: 

55933  833 
"(rel_fset A ===> (A ===> op =) ===> op =) fBex fBex" 
55945  834 
unfolding rel_fset_alt_def rel_fun_def by blast 
53953  835 

836 
(* FIXME transfer doesn't work here *) 

837 
lemma fPow_transfer [transfer_rule]: 

55933  838 
"(rel_fset A ===> rel_fset (rel_fset A)) fPow fPow" 
55945  839 
unfolding rel_fun_def 
840 
using Pow_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] 

53953  841 
by blast 
842 

55933  843 
lemma rel_fset_transfer [transfer_rule]: 
844 
"((A ===> B ===> op =) ===> rel_fset A ===> rel_fset B ===> op =) 

845 
rel_fset rel_fset" 

55945  846 
unfolding rel_fun_def 
847 
using rel_set_transfer[unfolded rel_fun_def,rule_format, Transfer.transferred, where A = A and B = B] 

53953  848 
by simp 
849 

850 
lemma bind_transfer [transfer_rule]: 

55933  851 
"(rel_fset A ===> (A ===> rel_fset B) ===> rel_fset B) fbind fbind" 
55945  852 
using assms unfolding rel_fun_def 
853 
using bind_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast 

53953  854 

855 
text {* Rules requiring biunique, bitotal or righttotal relations *} 

856 

857 
lemma fmember_transfer [transfer_rule]: 

858 
assumes "bi_unique A" 

55933  859 
shows "(A ===> rel_fset A ===> op =) (op \<in>) (op \<in>)" 
55945  860 
using assms unfolding rel_fun_def rel_fset_alt_def bi_unique_def by metis 
53953  861 

862 
lemma finter_transfer [transfer_rule]: 

863 
assumes "bi_unique A" 

55933  864 
shows "(rel_fset A ===> rel_fset A ===> rel_fset A) finter finter" 
55945  865 
using assms unfolding rel_fun_def 
866 
using inter_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast 

53953  867 

53963  868 
lemma fminus_transfer [transfer_rule]: 
53953  869 
assumes "bi_unique A" 
55933  870 
shows "(rel_fset A ===> rel_fset A ===> rel_fset A) (op ) (op )" 
55945  871 
using assms unfolding rel_fun_def 
872 
using Diff_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast 

53953  873 

874 
lemma fsubset_transfer [transfer_rule]: 

875 
assumes "bi_unique A" 

55933  876 
shows "(rel_fset A ===> rel_fset A ===> op =) (op \<subseteq>) (op \<subseteq>)" 
55945  877 
using assms unfolding rel_fun_def 
878 
using subset_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast 

53953  879 

880 
lemma fSup_transfer [transfer_rule]: 

55938  881 
"bi_unique A \<Longrightarrow> (rel_set (rel_fset A) ===> rel_fset A) Sup Sup" 
55945  882 
using assms unfolding rel_fun_def 
53953  883 
apply clarify 
884 
apply transfer' 

55945  885 
using Sup_fset_transfer[unfolded rel_fun_def] by blast 
53953  886 

887 
(* FIXME: add right_total_fInf_transfer *) 

888 

889 
lemma fInf_transfer [transfer_rule]: 

890 
assumes "bi_unique A" and "bi_total A" 

55938  891 
shows "(rel_set (rel_fset A) ===> rel_fset A) Inf Inf" 
55945  892 
using assms unfolding rel_fun_def 
53953  893 
apply clarify 
894 
apply transfer' 

55945  895 
using Inf_fset_transfer[unfolded rel_fun_def] by blast 
53953  896 

897 
lemma ffilter_transfer [transfer_rule]: 

898 
assumes "bi_unique A" 

55933  899 
shows "((A ===> op=) ===> rel_fset A ===> rel_fset A) ffilter ffilter" 
55945  900 
using assms unfolding rel_fun_def 
901 
using Lifting_Set.filter_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast 

53953  902 

903 
lemma card_transfer [transfer_rule]: 

55933  904 
"bi_unique A \<Longrightarrow> (rel_fset A ===> op =) fcard fcard" 
55945  905 
using assms unfolding rel_fun_def 
906 
using card_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast 

53953  907 

908 
end 

909 

910 
lifting_update fset.lifting 

911 
lifting_forget fset.lifting 

912 

55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

913 

26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

914 
subsection {* BNF setup *} 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

915 

26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

916 
context 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

917 
includes fset.lifting 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

918 
begin 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

919 

55933  920 
lemma rel_fset_alt: 
921 
"rel_fset R a b \<longleftrightarrow> (\<forall>t \<in> fset a. \<exists>u \<in> fset b. R t u) \<and> (\<forall>t \<in> fset b. \<exists>u \<in> fset a. R u t)" 

55938  922 
by transfer (simp add: rel_set_def) 
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

923 

26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

924 
lemma fset_to_fset: "finite A \<Longrightarrow> fset (the_inv fset A) = A" 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

925 
apply (rule f_the_inv_into_f[unfolded inj_on_def]) 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

926 
apply (simp add: fset_inject) 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

927 
apply (rule range_eqI Abs_fset_inverse[symmetric] CollectI)+ 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

928 
. 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

929 

55933  930 
lemma rel_fset_aux: 
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

931 
"(\<forall>t \<in> fset a. \<exists>u \<in> fset b. R t u) \<and> (\<forall>u \<in> fset b. \<exists>t \<in> fset a. R t u) \<longleftrightarrow> 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

932 
((BNF_Util.Grp {a. fset a \<subseteq> {(a, b). R a b}} (fimage fst))\<inverse>\<inverse> OO 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

933 
BNF_Util.Grp {a. fset a \<subseteq> {(a, b). R a b}} (fimage snd)) a b" (is "?L = ?R") 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

934 
proof 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

935 
assume ?L 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

936 
def R' \<equiv> "the_inv fset (Collect (split R) \<inter> (fset a \<times> fset b))" (is "the_inv fset ?L'") 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

937 
have "finite ?L'" by (intro finite_Int[OF disjI2] finite_cartesian_product) (transfer, simp)+ 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

938 
hence *: "fset R' = ?L'" unfolding R'_def by (intro fset_to_fset) 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

939 
show ?R unfolding Grp_def relcompp.simps conversep.simps 
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55129
diff
changeset

940 
proof (intro CollectI case_prodI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl) 
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

941 
from * show "a = fimage fst R'" using conjunct1[OF `?L`] 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

942 
by (transfer, auto simp add: image_def Int_def split: prod.splits) 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

943 
from * show "b = fimage snd R'" using conjunct2[OF `?L`] 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

944 
by (transfer, auto simp add: image_def Int_def split: prod.splits) 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

945 
qed (auto simp add: *) 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

946 
next 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

947 
assume ?R thus ?L unfolding Grp_def relcompp.simps conversep.simps 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

948 
apply (simp add: subset_eq Ball_def) 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

949 
apply (rule conjI) 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

950 
apply (transfer, clarsimp, metis snd_conv) 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

951 
by (transfer, clarsimp, metis fst_conv) 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

952 
qed 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

953 

26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

954 
bnf "'a fset" 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

955 
map: fimage 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

956 
sets: fset 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

957 
bd: natLeq 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

958 
wits: "{}" 
55933  959 
rel: rel_fset 
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

960 
apply  
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

961 
apply transfer' apply simp 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

962 
apply transfer' apply force 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

963 
apply transfer apply force 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

964 
apply transfer' apply force 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

965 
apply (rule natLeq_card_order) 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

966 
apply (rule natLeq_cinfinite) 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

967 
apply transfer apply (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq) 
55933  968 
apply (fastforce simp: rel_fset_alt) 
969 
apply (simp add: Grp_def relcompp.simps conversep.simps fun_eq_iff rel_fset_alt rel_fset_aux) 

55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

970 
apply transfer apply simp 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

971 
done 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

972 

55938  973 
lemma rel_fset_fset: "rel_set \<chi> (fset A1) (fset A2) = rel_fset \<chi> A1 A2" 
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

974 
by transfer (rule refl) 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

975 

53953  976 
end 
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

977 

26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

978 
lemmas [simp] = fset.map_comp fset.map_id fset.set_map 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

979 

26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

980 

26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

981 
subsection {* Advanced relator customization *} 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

982 

26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

983 
(* Set vs. sum relators: *) 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

984 

55943  985 
lemma rel_set_rel_sum[simp]: 
986 
"rel_set (rel_sum \<chi> \<phi>) A1 A2 \<longleftrightarrow> 

55938  987 
rel_set \<chi> (Inl ` A1) (Inl ` A2) \<and> rel_set \<phi> (Inr ` A1) (Inr ` A2)" 
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

988 
(is "?L \<longleftrightarrow> ?Rl \<and> ?Rr") 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

989 
proof safe 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

990 
assume L: "?L" 
55938  991 
show ?Rl unfolding rel_set_def Bex_def vimage_eq proof safe 
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

992 
fix l1 assume "Inl l1 \<in> A1" 
55943  993 
then obtain a2 where a2: "a2 \<in> A2" and "rel_sum \<chi> \<phi> (Inl l1) a2" 
55938  994 
using L unfolding rel_set_def by auto 
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

995 
then obtain l2 where "a2 = Inl l2 \<and> \<chi> l1 l2" by (cases a2, auto) 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

996 
thus "\<exists> l2. Inl l2 \<in> A2 \<and> \<chi> l1 l2" using a2 by auto 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

997 
next 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

998 
fix l2 assume "Inl l2 \<in> A2" 
55943  999 
then obtain a1 where a1: "a1 \<in> A1" and "rel_sum \<chi> \<phi> a1 (Inl l2)" 
55938  1000 
using L unfolding rel_set_def by auto 
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

1001 
then obtain l1 where "a1 = Inl l1 \<and> \<chi> l1 l2" by (cases a1, auto) 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

1002 
thus "\<exists> l1. Inl l1 \<in> A1 \<and> \<chi> l1 l2" using a1 by auto 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

1003 
qed 
55938  1004 
show ?Rr unfolding rel_set_def Bex_def vimage_eq proof safe 
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

1005 
fix r1 assume "Inr r1 \<in> A1" 
55943  1006 
then obtain a2 where a2: "a2 \<in> A2" and "rel_sum \<chi> \<phi> (Inr r1) a2" 
55938  1007 
using L unfolding rel_set_def by auto 
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

1008 
then obtain r2 where "a2 = Inr r2 \<and> \<phi> r1 r2" by (cases a2, auto) 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

1009 
thus "\<exists> r2. Inr r2 \<in> A2 \<and> \<phi> r1 r2" using a2 by auto 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

1010 
next 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

1011 
fix r2 assume "Inr r2 \<in> A2" 
55943  1012 
then obtain a1 where a1: "a1 \<in> A1" and "rel_sum \<chi> \<phi> a1 (Inr r2)" 
55938  1013 
using L unfolding rel_set_def by auto 
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

1014 
then obtain r1 where "a1 = Inr r1 \<and> \<phi> r1 r2" by (cases a1, auto) 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

1015 
thus "\<exists> r1. Inr r1 \<in> A1 \<and> \<phi> r1 r2" using a1 by auto 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

1016 
qed 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

1017 
next 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

1018 
assume Rl: "?Rl" and Rr: "?Rr" 
55938  1019 
show ?L unfolding rel_set_def Bex_def vimage_eq proof safe 
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

1020 
fix a1 assume a1: "a1 \<in> A1" 
55943  1021 
show "\<exists> a2. a2 \<in> A2 \<and> rel_sum \<chi> \<phi> a1 a2" 
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

1022 
proof(cases a1) 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

1023 
case (Inl l1) then obtain l2 where "Inl l2 \<in> A2 \<and> \<chi> l1 l2" 
55938  1024 
using Rl a1 unfolding rel_set_def by blast 
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

1025 
thus ?thesis unfolding Inl by auto 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

1026 
next 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

1027 
case (Inr r1) then obtain r2 where "Inr r2 \<in> A2 \<and> \<phi> r1 r2" 
55938  1028 
using Rr a1 unfolding rel_set_def by blast 
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

1029 
thus ?thesis unfolding Inr by auto 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

1030 
qed 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

1031 
next 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

1032 
fix a2 assume a2: "a2 \<in> A2" 
55943  1033 
show "\<exists> a1. a1 \<in> A1 \<and> rel_sum \<chi> \<phi> a1 a2" 
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

1034 
proof(cases a2) 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

1035 
case (Inl l2) then obtain l1 where "Inl l1 \<in> A1 \<and> \<chi> l1 l2" 
55938  1036 
using Rl a2 unfolding rel_set_def by blast 
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

1037 
thus ?thesis unfolding Inl by auto 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

1038 
next 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

1039 
case (Inr r2) then obtain r1 where "Inr r1 \<in> A1 \<and> \<phi> r1 r2" 
55938  1040 
using Rr a2 unfolding rel_set_def by blast 
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

1041 
thus ?thesis unfolding Inr by auto 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

1042 
qed 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

1043 
qed 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

1044 
qed 
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

1045 

26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset

1046 
end 