2084
+ − 1
(* Title: HOL/Quotient_Examples/FSet.thy
+ − 2
Author: Cezary Kaliszyk, TU Munich
+ − 3
Author: Christian Urban, TU Munich
1823
+ − 4
2084
+ − 5
A reasoning infrastructure for the type of finite sets.
1823
+ − 6
*)
2084
+ − 7
1518
+ − 8
theory FSet
2238
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 9
imports Quotient_List Quotient_Product
1518
+ − 10
begin
+ − 11
1909
+ − 12
text {* Definiton of List relation and the quotient type *}
+ − 13
1518
+ − 14
fun
+ − 15
list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50)
+ − 16
where
+ − 17
"list_eq xs ys = (\<forall>x. x \<in> set xs \<longleftrightarrow> x \<in> set ys)"
+ − 18
+ − 19
lemma list_eq_equivp:
+ − 20
shows "equivp list_eq"
1909
+ − 21
unfolding equivp_reflp_symp_transp
1889
+ − 22
unfolding reflp_def symp_def transp_def
+ − 23
by auto
+ − 24
1909
+ − 25
quotient_type
+ − 26
'a fset = "'a list" / "list_eq"
+ − 27
by (rule list_eq_equivp)
+ − 28
+ − 29
text {* Raw definitions *}
+ − 30
1889
+ − 31
definition
+ − 32
memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
+ − 33
where
+ − 34
"memb x xs \<equiv> x \<in> set xs"
+ − 35
+ − 36
definition
+ − 37
sub_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
+ − 38
where
+ − 39
"sub_list xs ys \<equiv> (\<forall>x. x \<in> set xs \<longrightarrow> x \<in> set ys)"
+ − 40
1909
+ − 41
fun
+ − 42
fcard_raw :: "'a list \<Rightarrow> nat"
+ − 43
where
+ − 44
fcard_raw_nil: "fcard_raw [] = 0"
+ − 45
| fcard_raw_cons: "fcard_raw (x # xs) = (if memb x xs then fcard_raw xs else Suc (fcard_raw xs))"
1518
+ − 46
1909
+ − 47
primrec
+ − 48
finter_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+ − 49
where
+ − 50
"finter_raw [] l = []"
+ − 51
| "finter_raw (h # t) l =
+ − 52
(if memb h l then h # (finter_raw t l) else finter_raw t l)"
1893
+ − 53
2084
+ − 54
primrec
1909
+ − 55
delete_raw :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list"
+ − 56
where
+ − 57
"delete_raw [] x = []"
2084
+ − 58
| "delete_raw (a # xs) x = (if (a = x) then delete_raw xs x else a # (delete_raw xs x))"
+ − 59
+ − 60
primrec
+ − 61
fminus_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+ − 62
where
+ − 63
"fminus_raw l [] = l"
+ − 64
| "fminus_raw l (h # t) = fminus_raw (delete_raw l h) t"
1909
+ − 65
+ − 66
definition
+ − 67
rsp_fold
+ − 68
where
+ − 69
"rsp_fold f = (\<forall>u v w. (f u (f v w) = f v (f u w)))"
1893
+ − 70
1909
+ − 71
primrec
+ − 72
ffold_raw :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"
+ − 73
where
+ − 74
"ffold_raw f z [] = z"
2084
+ − 75
| "ffold_raw f z (a # xs) =
1909
+ − 76
(if (rsp_fold f) then
2084
+ − 77
if memb a xs then ffold_raw f z xs
+ − 78
else f a (ffold_raw f z xs)
1909
+ − 79
else z)"
+ − 80
1935
+ − 81
text {* Composition Quotient *}
+ − 82
2266
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 83
lemma list_rel_refl1:
1938
+ − 84
shows "(list_rel op \<approx>) r r"
+ − 85
by (rule list_rel_refl) (metis equivp_def fset_equivp)
+ − 86
1935
+ − 87
lemma compose_list_refl:
+ − 88
shows "(list_rel op \<approx> OOO op \<approx>) r r"
+ − 89
proof
2084
+ − 90
have *: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp])
2266
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 91
show "list_rel op \<approx> r r" by (rule list_rel_refl1)
2084
+ − 92
with * show "(op \<approx> OO list_rel op \<approx>) r r" ..
1935
+ − 93
qed
+ − 94
+ − 95
lemma Quotient_fset_list:
+ − 96
shows "Quotient (list_rel op \<approx>) (map abs_fset) (map rep_fset)"
+ − 97
by (fact list_quotient[OF Quotient_fset])
+ − 98
2084
+ − 99
lemma set_in_eq: "(\<forall>e. ((e \<in> xs) \<longleftrightarrow> (e \<in> ys))) \<equiv> xs = ys"
1935
+ − 100
by (rule eq_reflection) auto
+ − 101
+ − 102
lemma map_rel_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba"
+ − 103
unfolding list_eq.simps
+ − 104
by (simp only: set_map set_in_eq)
+ − 105
2266
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 106
1935
+ − 107
lemma quotient_compose_list[quot_thm]:
+ − 108
shows "Quotient ((list_rel op \<approx>) OOO (op \<approx>))
+ − 109
(abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"
+ − 110
unfolding Quotient_def comp_def
+ − 111
proof (intro conjI allI)
+ − 112
fix a r s
+ − 113
show "abs_fset (map abs_fset (map rep_fset (rep_fset a))) = a"
+ − 114
by (simp add: abs_o_rep[OF Quotient_fset] Quotient_abs_rep[OF Quotient_fset] map_id)
+ − 115
have b: "list_rel op \<approx> (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
2266
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 116
by (rule list_rel_refl1)
1935
+ − 117
have c: "(op \<approx> OO list_rel op \<approx>) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
+ − 118
by (rule, rule equivp_reflp[OF fset_equivp]) (rule b)
+ − 119
show "(list_rel op \<approx> OOO op \<approx>) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
2266
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 120
by (rule, rule list_rel_refl1) (rule c)
1935
+ − 121
show "(list_rel op \<approx> OOO op \<approx>) r s = ((list_rel op \<approx> OOO op \<approx>) r r \<and>
+ − 122
(list_rel op \<approx> OOO op \<approx>) s s \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s))"
+ − 123
proof (intro iffI conjI)
+ − 124
show "(list_rel op \<approx> OOO op \<approx>) r r" by (rule compose_list_refl)
+ − 125
show "(list_rel op \<approx> OOO op \<approx>) s s" by (rule compose_list_refl)
+ − 126
next
+ − 127
assume a: "(list_rel op \<approx> OOO op \<approx>) r s"
2084
+ − 128
then have b: "map abs_fset r \<approx> map abs_fset s"
+ − 129
proof (elim pred_compE)
1935
+ − 130
fix b ba
+ − 131
assume c: "list_rel op \<approx> r b"
+ − 132
assume d: "b \<approx> ba"
+ − 133
assume e: "list_rel op \<approx> ba s"
+ − 134
have f: "map abs_fset r = map abs_fset b"
1938
+ − 135
using Quotient_rel[OF Quotient_fset_list] c by blast
+ − 136
have "map abs_fset ba = map abs_fset s"
+ − 137
using Quotient_rel[OF Quotient_fset_list] e by blast
+ − 138
then have g: "map abs_fset s = map abs_fset ba" by simp
+ − 139
then show "map abs_fset r \<approx> map abs_fset s" using d f map_rel_cong by simp
1935
+ − 140
qed
+ − 141
then show "abs_fset (map abs_fset r) = abs_fset (map abs_fset s)"
1938
+ − 142
using Quotient_rel[OF Quotient_fset] by blast
1935
+ − 143
next
+ − 144
assume a: "(list_rel op \<approx> OOO op \<approx>) r r \<and> (list_rel op \<approx> OOO op \<approx>) s s
+ − 145
\<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s)"
+ − 146
then have s: "(list_rel op \<approx> OOO op \<approx>) s s" by simp
+ − 147
have d: "map abs_fset r \<approx> map abs_fset s"
+ − 148
by (subst Quotient_rel[OF Quotient_fset]) (simp add: a)
+ − 149
have b: "map rep_fset (map abs_fset r) \<approx> map rep_fset (map abs_fset s)"
+ − 150
by (rule map_rel_cong[OF d])
+ − 151
have y: "list_rel op \<approx> (map rep_fset (map abs_fset s)) s"
2266
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 152
by (fact rep_abs_rsp_left[OF Quotient_fset_list, OF list_rel_refl1[of s]])
1935
+ − 153
have c: "(op \<approx> OO list_rel op \<approx>) (map rep_fset (map abs_fset r)) s"
+ − 154
by (rule pred_compI) (rule b, rule y)
+ − 155
have z: "list_rel op \<approx> r (map rep_fset (map abs_fset r))"
2266
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 156
by (fact rep_abs_rsp[OF Quotient_fset_list, OF list_rel_refl1[of r]])
1935
+ − 157
then show "(list_rel op \<approx> OOO op \<approx>) r s"
+ − 158
using a c pred_compI by simp
+ − 159
qed
+ − 160
qed
+ − 161
1909
+ − 162
text {* Respectfullness *}
1893
+ − 163
2187
+ − 164
lemma append_rsp[quot_respect]:
1895
+ − 165
shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
2278
+ − 166
apply(simp del: list_eq.simps)
1895
+ − 167
by auto
+ − 168
2190
+ − 169
lemma append_rsp_unfolded:
+ − 170
"\<lbrakk>x \<approx> y; v \<approx> w\<rbrakk> \<Longrightarrow> x @ v \<approx> y @ w"
+ − 171
by auto
+ − 172
1909
+ − 173
lemma [quot_respect]:
+ − 174
shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list"
+ − 175
by (auto simp add: sub_list_def)
+ − 176
+ − 177
lemma memb_rsp[quot_respect]:
+ − 178
shows "(op = ===> op \<approx> ===> op =) memb memb"
+ − 179
by (auto simp add: memb_def)
+ − 180
+ − 181
lemma nil_rsp[quot_respect]:
+ − 182
shows "[] \<approx> []"
+ − 183
by simp
+ − 184
+ − 185
lemma cons_rsp[quot_respect]:
+ − 186
shows "(op = ===> op \<approx> ===> op \<approx>) op # op #"
+ − 187
by simp
+ − 188
+ − 189
lemma map_rsp[quot_respect]:
+ − 190
shows "(op = ===> op \<approx> ===> op \<approx>) map map"
+ − 191
by auto
+ − 192
+ − 193
lemma set_rsp[quot_respect]:
+ − 194
"(op \<approx> ===> op =) set set"
+ − 195
by auto
+ − 196
+ − 197
lemma list_equiv_rsp[quot_respect]:
+ − 198
shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
+ − 199
by auto
+ − 200
+ − 201
lemma not_memb_nil:
+ − 202
shows "\<not> memb x []"
+ − 203
by (simp add: memb_def)
+ − 204
+ − 205
lemma memb_cons_iff:
+ − 206
shows "memb x (y # xs) = (x = y \<or> memb x xs)"
+ − 207
by (induct xs) (auto simp add: memb_def)
+ − 208
+ − 209
lemma memb_finter_raw:
+ − 210
"memb x (finter_raw xs ys) \<longleftrightarrow> memb x xs \<and> memb x ys"
+ − 211
by (induct xs) (auto simp add: not_memb_nil memb_cons_iff)
+ − 212
+ − 213
lemma [quot_respect]:
+ − 214
"(op \<approx> ===> op \<approx> ===> op \<approx>) finter_raw finter_raw"
+ − 215
by (simp add: memb_def[symmetric] memb_finter_raw)
+ − 216
+ − 217
lemma memb_delete_raw:
+ − 218
"memb x (delete_raw xs y) = (memb x xs \<and> x \<noteq> y)"
+ − 219
by (induct xs arbitrary: x y) (auto simp add: memb_def)
+ − 220
+ − 221
lemma [quot_respect]:
+ − 222
"(op \<approx> ===> op = ===> op \<approx>) delete_raw delete_raw"
+ − 223
by (simp add: memb_def[symmetric] memb_delete_raw)
+ − 224
2084
+ − 225
lemma fminus_raw_memb: "memb x (fminus_raw xs ys) = (memb x xs \<and> \<not> memb x ys)"
+ − 226
by (induct ys arbitrary: xs)
+ − 227
(simp_all add: not_memb_nil memb_delete_raw memb_cons_iff)
+ − 228
+ − 229
lemma [quot_respect]:
+ − 230
"(op \<approx> ===> op \<approx> ===> op \<approx>) fminus_raw fminus_raw"
+ − 231
by (simp add: memb_def[symmetric] fminus_raw_memb)
+ − 232
1909
+ − 233
lemma fcard_raw_gt_0:
+ − 234
assumes a: "x \<in> set xs"
+ − 235
shows "0 < fcard_raw xs"
+ − 236
using a by (induct xs) (auto simp add: memb_def)
+ − 237
+ − 238
lemma fcard_raw_delete_one:
+ − 239
shows "fcard_raw ([x \<leftarrow> xs. x \<noteq> y]) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"
+ − 240
by (induct xs) (auto dest: fcard_raw_gt_0 simp add: memb_def)
+ − 241
+ − 242
lemma fcard_raw_rsp_aux:
+ − 243
assumes a: "xs \<approx> ys"
+ − 244
shows "fcard_raw xs = fcard_raw ys"
+ − 245
using a
2084
+ − 246
proof (induct xs arbitrary: ys)
+ − 247
case Nil
+ − 248
show ?case using Nil.prems by simp
+ − 249
next
+ − 250
case (Cons a xs)
+ − 251
have a: "a # xs \<approx> ys" by fact
+ − 252
have b: "\<And>ys. xs \<approx> ys \<Longrightarrow> fcard_raw xs = fcard_raw ys" by fact
+ − 253
show ?case proof (cases "a \<in> set xs")
+ − 254
assume c: "a \<in> set xs"
+ − 255
have "\<forall>x. (x \<in> set xs) = (x \<in> set ys)"
+ − 256
proof (intro allI iffI)
+ − 257
fix x
+ − 258
assume "x \<in> set xs"
+ − 259
then show "x \<in> set ys" using a by auto
+ − 260
next
+ − 261
fix x
+ − 262
assume d: "x \<in> set ys"
+ − 263
have e: "(x \<in> set (a # xs)) = (x \<in> set ys)" using a by simp
+ − 264
show "x \<in> set xs" using c d e unfolding list_eq.simps by simp blast
+ − 265
qed
+ − 266
then show ?thesis using b c by (simp add: memb_def)
+ − 267
next
+ − 268
assume c: "a \<notin> set xs"
+ − 269
have d: "xs \<approx> [x\<leftarrow>ys . x \<noteq> a] \<Longrightarrow> fcard_raw xs = fcard_raw [x\<leftarrow>ys . x \<noteq> a]" using b by simp
+ − 270
have "Suc (fcard_raw xs) = fcard_raw ys"
+ − 271
proof (cases "a \<in> set ys")
+ − 272
assume e: "a \<in> set ys"
+ − 273
have f: "\<forall>x. (x \<in> set xs) = (x \<in> set ys \<and> x \<noteq> a)" using a c
+ − 274
by (auto simp add: fcard_raw_delete_one)
+ − 275
have "fcard_raw ys = Suc (fcard_raw ys - 1)" by (rule Suc_pred'[OF fcard_raw_gt_0]) (rule e)
+ − 276
then show ?thesis using d e f by (simp_all add: fcard_raw_delete_one memb_def)
+ − 277
next
+ − 278
case False then show ?thesis using a c d by auto
+ − 279
qed
+ − 280
then show ?thesis using a c d by (simp add: memb_def)
+ − 281
qed
+ − 282
qed
1909
+ − 283
+ − 284
lemma fcard_raw_rsp[quot_respect]:
+ − 285
shows "(op \<approx> ===> op =) fcard_raw fcard_raw"
+ − 286
by (simp add: fcard_raw_rsp_aux)
+ − 287
+ − 288
lemma memb_absorb:
+ − 289
shows "memb x xs \<Longrightarrow> x # xs \<approx> xs"
+ − 290
by (induct xs) (auto simp add: memb_def)
+ − 291
+ − 292
lemma none_memb_nil:
+ − 293
"(\<forall>x. \<not> memb x xs) = (xs \<approx> [])"
+ − 294
by (simp add: memb_def)
+ − 295
+ − 296
lemma not_memb_delete_raw_ident:
+ − 297
shows "\<not> memb x xs \<Longrightarrow> delete_raw xs x = xs"
+ − 298
by (induct xs) (auto simp add: memb_def)
+ − 299
+ − 300
lemma memb_commute_ffold_raw:
+ − 301
"rsp_fold f \<Longrightarrow> memb h b \<Longrightarrow> ffold_raw f z b = f h (ffold_raw f z (delete_raw b h))"
+ − 302
apply (induct b)
+ − 303
apply (simp_all add: not_memb_nil)
+ − 304
apply (auto)
1938
+ − 305
apply (simp_all add: memb_delete_raw not_memb_delete_raw_ident rsp_fold_def memb_cons_iff)
1909
+ − 306
done
+ − 307
+ − 308
lemma ffold_raw_rsp_pre:
+ − 309
"\<forall>e. memb e a = memb e b \<Longrightarrow> ffold_raw f z a = ffold_raw f z b"
+ − 310
apply (induct a arbitrary: b)
+ − 311
apply (simp add: memb_absorb memb_def none_memb_nil)
+ − 312
apply (simp)
+ − 313
apply (rule conjI)
+ − 314
apply (rule_tac [!] impI)
+ − 315
apply (rule_tac [!] conjI)
+ − 316
apply (rule_tac [!] impI)
+ − 317
apply (subgoal_tac "\<forall>e. memb e a2 = memb e b")
+ − 318
apply (simp)
+ − 319
apply (simp add: memb_cons_iff memb_def)
+ − 320
apply (auto)[1]
+ − 321
apply (drule_tac x="e" in spec)
+ − 322
apply (blast)
+ − 323
apply (case_tac b)
+ − 324
apply (simp_all)
+ − 325
apply (subgoal_tac "ffold_raw f z b = f a1 (ffold_raw f z (delete_raw b a1))")
+ − 326
apply (simp only:)
+ − 327
apply (rule_tac f="f a1" in arg_cong)
+ − 328
apply (subgoal_tac "\<forall>e. memb e a2 = memb e (delete_raw b a1)")
+ − 329
apply (simp)
+ − 330
apply (simp add: memb_delete_raw)
+ − 331
apply (auto simp add: memb_cons_iff)[1]
+ − 332
apply (erule memb_commute_ffold_raw)
+ − 333
apply (drule_tac x="a1" in spec)
+ − 334
apply (simp add: memb_cons_iff)
+ − 335
apply (simp add: memb_cons_iff)
+ − 336
apply (case_tac b)
+ − 337
apply (simp_all)
+ − 338
done
+ − 339
+ − 340
lemma [quot_respect]:
+ − 341
"(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw"
+ − 342
by (simp add: memb_def[symmetric] ffold_raw_rsp_pre)
+ − 343
1935
+ − 344
lemma concat_rsp_pre:
+ − 345
assumes a: "list_rel op \<approx> x x'"
+ − 346
and b: "x' \<approx> y'"
+ − 347
and c: "list_rel op \<approx> y' y"
+ − 348
and d: "\<exists>x\<in>set x. xa \<in> set x"
+ − 349
shows "\<exists>x\<in>set y. xa \<in> set x"
+ − 350
proof -
+ − 351
obtain xb where e: "xb \<in> set x" and f: "xa \<in> set xb" using d by auto
+ − 352
have "\<exists>y. y \<in> set x' \<and> xb \<approx> y" by (rule list_rel_find_element[OF e a])
+ − 353
then obtain ya where h: "ya \<in> set x'" and i: "xb \<approx> ya" by auto
2084
+ − 354
have "ya \<in> set y'" using b h by simp
+ − 355
then have "\<exists>yb. yb \<in> set y \<and> ya \<approx> yb" using c by (rule list_rel_find_element)
1935
+ − 356
then show ?thesis using f i by auto
+ − 357
qed
+ − 358
2187
+ − 359
lemma concat_rsp[quot_respect]:
1935
+ − 360
shows "(list_rel op \<approx> OOO op \<approx> ===> op \<approx>) concat concat"
+ − 361
proof (rule fun_relI, elim pred_compE)
+ − 362
fix a b ba bb
+ − 363
assume a: "list_rel op \<approx> a ba"
+ − 364
assume b: "ba \<approx> bb"
+ − 365
assume c: "list_rel op \<approx> bb b"
+ − 366
have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof
+ − 367
fix x
+ − 368
show "(\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof
+ − 369
assume d: "\<exists>xa\<in>set a. x \<in> set xa"
+ − 370
show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d])
+ − 371
next
+ − 372
assume e: "\<exists>xa\<in>set b. x \<in> set xa"
+ − 373
have a': "list_rel op \<approx> ba a" by (rule list_rel_symp[OF list_eq_equivp, OF a])
+ − 374
have b': "bb \<approx> ba" by (rule equivp_symp[OF list_eq_equivp, OF b])
+ − 375
have c': "list_rel op \<approx> b bb" by (rule list_rel_symp[OF list_eq_equivp, OF c])
+ − 376
show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e])
+ − 377
qed
+ − 378
qed
+ − 379
then show "concat a \<approx> concat b" by simp
+ − 380
qed
+ − 381
2190
+ − 382
+ − 383
+ − 384
lemma concat_rsp_unfolded:
+ − 385
"\<lbrakk>list_rel op \<approx> a ba; ba \<approx> bb; list_rel op \<approx> bb b\<rbrakk> \<Longrightarrow> concat a \<approx> concat b"
+ − 386
proof -
+ − 387
fix a b ba bb
+ − 388
assume a: "list_rel op \<approx> a ba"
+ − 389
assume b: "ba \<approx> bb"
+ − 390
assume c: "list_rel op \<approx> bb b"
+ − 391
have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof
+ − 392
fix x
+ − 393
show "(\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof
+ − 394
assume d: "\<exists>xa\<in>set a. x \<in> set xa"
+ − 395
show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d])
+ − 396
next
+ − 397
assume e: "\<exists>xa\<in>set b. x \<in> set xa"
+ − 398
have a': "list_rel op \<approx> ba a" by (rule list_rel_symp[OF list_eq_equivp, OF a])
+ − 399
have b': "bb \<approx> ba" by (rule equivp_symp[OF list_eq_equivp, OF b])
+ − 400
have c': "list_rel op \<approx> b bb" by (rule list_rel_symp[OF list_eq_equivp, OF c])
+ − 401
show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e])
+ − 402
qed
+ − 403
qed
+ − 404
then show "concat a \<approx> concat b" by simp
+ − 405
qed
+ − 406
2084
+ − 407
lemma [quot_respect]:
+ − 408
"((op =) ===> op \<approx> ===> op \<approx>) filter filter"
+ − 409
by auto
+ − 410
1909
+ − 411
text {* Distributive lattice with bot *}
+ − 412
1893
+ − 413
lemma sub_list_not_eq:
+ − 414
"(sub_list x y \<and> \<not> list_eq x y) = (sub_list x y \<and> \<not> sub_list y x)"
+ − 415
by (auto simp add: sub_list_def)
+ − 416
+ − 417
lemma sub_list_refl:
+ − 418
"sub_list x x"
+ − 419
by (simp add: sub_list_def)
+ − 420
+ − 421
lemma sub_list_trans:
+ − 422
"sub_list x y \<Longrightarrow> sub_list y z \<Longrightarrow> sub_list x z"
+ − 423
by (simp add: sub_list_def)
+ − 424
+ − 425
lemma sub_list_empty:
+ − 426
"sub_list [] x"
+ − 427
by (simp add: sub_list_def)
+ − 428
1905
+ − 429
lemma sub_list_append_left:
+ − 430
"sub_list x (x @ y)"
+ − 431
by (simp add: sub_list_def)
+ − 432
+ − 433
lemma sub_list_append_right:
+ − 434
"sub_list y (x @ y)"
+ − 435
by (simp add: sub_list_def)
+ − 436
+ − 437
lemma sub_list_inter_left:
+ − 438
shows "sub_list (finter_raw x y) x"
+ − 439
by (simp add: sub_list_def memb_def[symmetric] memb_finter_raw)
+ − 440
+ − 441
lemma sub_list_inter_right:
+ − 442
shows "sub_list (finter_raw x y) y"
+ − 443
by (simp add: sub_list_def memb_def[symmetric] memb_finter_raw)
+ − 444
+ − 445
lemma sub_list_list_eq:
+ − 446
"sub_list x y \<Longrightarrow> sub_list y x \<Longrightarrow> list_eq x y"
+ − 447
unfolding sub_list_def list_eq.simps by blast
+ − 448
+ − 449
lemma sub_list_append:
+ − 450
"sub_list y x \<Longrightarrow> sub_list z x \<Longrightarrow> sub_list (y @ z) x"
+ − 451
unfolding sub_list_def by auto
+ − 452
+ − 453
lemma sub_list_inter:
+ − 454
"sub_list x y \<Longrightarrow> sub_list x z \<Longrightarrow> sub_list x (finter_raw y z)"
+ − 455
by (simp add: sub_list_def memb_def[symmetric] memb_finter_raw)
+ − 456
+ − 457
lemma append_inter_distrib:
+ − 458
"x @ (finter_raw y z) \<approx> finter_raw (x @ y) (x @ z)"
+ − 459
apply (induct x)
+ − 460
apply (simp_all add: memb_def)
+ − 461
apply (simp add: memb_def[symmetric] memb_finter_raw)
2084
+ − 462
apply (auto simp add: memb_def)
+ − 463
done
1905
+ − 464
2084
+ − 465
instantiation fset :: (type) "{bounded_lattice_bot,distrib_lattice,minus}"
1893
+ − 466
begin
+ − 467
+ − 468
quotient_definition
+ − 469
"bot :: 'a fset" is "[] :: 'a list"
+ − 470
+ − 471
abbreviation
+ − 472
fempty ("{||}")
+ − 473
where
+ − 474
"{||} \<equiv> bot :: 'a fset"
+ − 475
+ − 476
quotient_definition
+ − 477
"less_eq_fset \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> bool)"
+ − 478
is
+ − 479
"sub_list \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> bool)"
+ − 480
+ − 481
abbreviation
+ − 482
f_subset_eq :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subseteq>|" 50)
+ − 483
where
+ − 484
"xs |\<subseteq>| ys \<equiv> xs \<le> ys"
+ − 485
+ − 486
definition
+ − 487
less_fset:
+ − 488
"(xs :: 'a fset) < ys \<equiv> xs \<le> ys \<and> xs \<noteq> ys"
+ − 489
+ − 490
abbreviation
+ − 491
f_subset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subset>|" 50)
+ − 492
where
+ − 493
"xs |\<subset>| ys \<equiv> xs < ys"
+ − 494
1895
+ − 495
quotient_definition
+ − 496
"sup \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset)"
+ − 497
is
+ − 498
"(op @) \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> 'a list)"
+ − 499
+ − 500
abbreviation
2084
+ − 501
funion (infixl "|\<union>|" 65)
1895
+ − 502
where
+ − 503
"xs |\<union>| ys \<equiv> sup (xs :: 'a fset) ys"
+ − 504
1905
+ − 505
quotient_definition
2084
+ − 506
"inf \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset)"
1905
+ − 507
is
+ − 508
"finter_raw \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> 'a list)"
+ − 509
+ − 510
abbreviation
+ − 511
finter (infixl "|\<inter>|" 65)
+ − 512
where
+ − 513
"xs |\<inter>| ys \<equiv> inf (xs :: 'a fset) ys"
+ − 514
2084
+ − 515
quotient_definition
+ − 516
"minus \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset)"
+ − 517
is
+ − 518
"fminus_raw \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> 'a list)"
+ − 519
1895
+ − 520
instance
+ − 521
proof
1905
+ − 522
fix x y z :: "'a fset"
+ − 523
show "(x |\<subset>| y) = (x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x)"
+ − 524
unfolding less_fset by (lifting sub_list_not_eq)
+ − 525
show "x |\<subseteq>| x" by (lifting sub_list_refl)
+ − 526
show "{||} |\<subseteq>| x" by (lifting sub_list_empty)
1895
+ − 527
show "x |\<subseteq>| x |\<union>| y" by (lifting sub_list_append_left)
+ − 528
show "y |\<subseteq>| x |\<union>| y" by (lifting sub_list_append_right)
1905
+ − 529
show "x |\<inter>| y |\<subseteq>| x" by (lifting sub_list_inter_left)
+ − 530
show "x |\<inter>| y |\<subseteq>| y" by (lifting sub_list_inter_right)
+ − 531
show "x |\<union>| (y |\<inter>| z) = x |\<union>| y |\<inter>| (x |\<union>| z)" by (lifting append_inter_distrib)
+ − 532
next
+ − 533
fix x y z :: "'a fset"
+ − 534
assume a: "x |\<subseteq>| y"
+ − 535
assume b: "y |\<subseteq>| z"
+ − 536
show "x |\<subseteq>| z" using a b by (lifting sub_list_trans)
1895
+ − 537
next
+ − 538
fix x y :: "'a fset"
+ − 539
assume a: "x |\<subseteq>| y"
+ − 540
assume b: "y |\<subseteq>| x"
+ − 541
show "x = y" using a b by (lifting sub_list_list_eq)
+ − 542
next
+ − 543
fix x y z :: "'a fset"
+ − 544
assume a: "y |\<subseteq>| x"
+ − 545
assume b: "z |\<subseteq>| x"
+ − 546
show "y |\<union>| z |\<subseteq>| x" using a b by (lifting sub_list_append)
1905
+ − 547
next
+ − 548
fix x y z :: "'a fset"
+ − 549
assume a: "x |\<subseteq>| y"
+ − 550
assume b: "x |\<subseteq>| z"
+ − 551
show "x |\<subseteq>| y |\<inter>| z" using a b by (lifting sub_list_inter)
1895
+ − 552
qed
1905
+ − 553
1893
+ − 554
end
+ − 555
1909
+ − 556
section {* Finsert and Membership *}
1518
+ − 557
+ − 558
quotient_definition
1893
+ − 559
"finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
1518
+ − 560
is "op #"
+ − 561
+ − 562
syntax
+ − 563
"@Finset" :: "args => 'a fset" ("{|(_)|}")
+ − 564
+ − 565
translations
+ − 566
"{|x, xs|}" == "CONST finsert x {|xs|}"
+ − 567
"{|x|}" == "CONST finsert x {||}"
+ − 568
+ − 569
quotient_definition
1938
+ − 570
fin (infix "|\<in>|" 50)
1518
+ − 571
where
1816
+ − 572
"fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" is "memb"
1518
+ − 573
+ − 574
abbreviation
1938
+ − 575
fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50)
1518
+ − 576
where
1860
+ − 577
"x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
1518
+ − 578
2084
+ − 579
section {* Other constants on the Quotient Type *}
1935
+ − 580
+ − 581
quotient_definition
2084
+ − 582
"fcard :: 'a fset \<Rightarrow> nat"
1935
+ − 583
is
+ − 584
"fcard_raw"
+ − 585
+ − 586
quotient_definition
+ − 587
"fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
+ − 588
is
+ − 589
"map"
+ − 590
+ − 591
quotient_definition
2084
+ − 592
"fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset"
1935
+ − 593
is "delete_raw"
+ − 594
+ − 595
quotient_definition
2084
+ − 596
"fset_to_set :: 'a fset \<Rightarrow> 'a set"
1935
+ − 597
is "set"
+ − 598
+ − 599
quotient_definition
+ − 600
"ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b"
+ − 601
is "ffold_raw"
+ − 602
+ − 603
quotient_definition
+ − 604
"fconcat :: ('a fset) fset \<Rightarrow> 'a fset"
+ − 605
is
+ − 606
"concat"
+ − 607
2222
+ − 608
thm fconcat_def
+ − 609
2084
+ − 610
quotient_definition
+ − 611
"ffilter :: ('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+ − 612
is
+ − 613
"filter"
+ − 614
1935
+ − 615
text {* Compositional Respectfullness and Preservation *}
+ − 616
+ − 617
lemma [quot_respect]: "(list_rel op \<approx> OOO op \<approx>) [] []"
1938
+ − 618
by (fact compose_list_refl)
1935
+ − 619
+ − 620
lemma [quot_preserve]: "(abs_fset \<circ> map f) [] = abs_fset []"
+ − 621
by simp
+ − 622
+ − 623
lemma [quot_respect]:
+ − 624
"(op \<approx> ===> list_rel op \<approx> OOO op \<approx> ===> list_rel op \<approx> OOO op \<approx>) op # op #"
+ − 625
apply auto
+ − 626
apply (simp add: set_in_eq)
+ − 627
apply (rule_tac b="x # b" in pred_compI)
+ − 628
apply auto
+ − 629
apply (rule_tac b="x # ba" in pred_compI)
+ − 630
apply auto
+ − 631
done
+ − 632
2196
+ − 633
lemma insert_preserve2:
+ − 634
shows "((rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op #) =
+ − 635
(id ---> rep_fset ---> abs_fset) op #"
+ − 636
by (simp add: expand_fun_eq abs_o_rep[OF Quotient_fset] map_id Quotient_abs_rep[OF Quotient_fset])
+ − 637
1935
+ − 638
lemma [quot_preserve]:
+ − 639
"(rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op # = finsert"
+ − 640
by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset]
+ − 641
abs_o_rep[OF Quotient_fset] map_id finsert_def)
+ − 642
+ − 643
lemma [quot_preserve]:
1938
+ − 644
"((map rep_fset \<circ> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op @ = funion"
1935
+ − 645
by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset]
+ − 646
abs_o_rep[OF Quotient_fset] map_id sup_fset_def)
+ − 647
+ − 648
lemma list_rel_app_l:
+ − 649
assumes a: "reflp R"
+ − 650
and b: "list_rel R l r"
+ − 651
shows "list_rel R (z @ l) (z @ r)"
1938
+ − 652
by (induct z) (simp_all add: b rev_iffD1[OF a meta_eq_to_obj_eq[OF reflp_def]])
1935
+ − 653
+ − 654
lemma append_rsp2_pre0:
+ − 655
assumes a:"list_rel op \<approx> x x'"
+ − 656
shows "list_rel op \<approx> (x @ z) (x' @ z)"
+ − 657
using a apply (induct x x' rule: list_induct2')
2266
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 658
by simp_all (rule list_rel_refl1)
1935
+ − 659
+ − 660
lemma append_rsp2_pre1:
+ − 661
assumes a:"list_rel op \<approx> x x'"
+ − 662
shows "list_rel op \<approx> (z @ x) (z @ x')"
+ − 663
using a apply (induct x x' arbitrary: z rule: list_induct2')
2266
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 664
apply (rule list_rel_refl1)
1935
+ − 665
apply (simp_all del: list_eq.simps)
+ − 666
apply (rule list_rel_app_l)
+ − 667
apply (simp_all add: reflp_def)
+ − 668
done
+ − 669
+ − 670
lemma append_rsp2_pre:
+ − 671
assumes a:"list_rel op \<approx> x x'"
+ − 672
and b: "list_rel op \<approx> z z'"
+ − 673
shows "list_rel op \<approx> (x @ z) (x' @ z')"
+ − 674
apply (rule list_rel_transp[OF fset_equivp])
+ − 675
apply (rule append_rsp2_pre0)
+ − 676
apply (rule a)
+ − 677
using b apply (induct z z' rule: list_induct2')
+ − 678
apply (simp_all only: append_Nil2)
2266
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 679
apply (rule list_rel_refl1)
1935
+ − 680
apply simp_all
+ − 681
apply (rule append_rsp2_pre1)
+ − 682
apply simp
+ − 683
done
+ − 684
+ − 685
lemma [quot_respect]:
+ − 686
"(list_rel op \<approx> OOO op \<approx> ===> list_rel op \<approx> OOO op \<approx> ===> list_rel op \<approx> OOO op \<approx>) op @ op @"
+ − 687
proof (intro fun_relI, elim pred_compE)
+ − 688
fix x y z w x' z' y' w' :: "'a list list"
+ − 689
assume a:"list_rel op \<approx> x x'"
+ − 690
and b: "x' \<approx> y'"
+ − 691
and c: "list_rel op \<approx> y' y"
+ − 692
assume aa: "list_rel op \<approx> z z'"
+ − 693
and bb: "z' \<approx> w'"
+ − 694
and cc: "list_rel op \<approx> w' w"
+ − 695
have a': "list_rel op \<approx> (x @ z) (x' @ z')" using a aa append_rsp2_pre by auto
+ − 696
have b': "x' @ z' \<approx> y' @ w'" using b bb by simp
+ − 697
have c': "list_rel op \<approx> (y' @ w') (y @ w)" using c cc append_rsp2_pre by auto
+ − 698
have d': "(op \<approx> OO list_rel op \<approx>) (x' @ z') (y @ w)"
+ − 699
by (rule pred_compI) (rule b', rule c')
+ − 700
show "(list_rel op \<approx> OOO op \<approx>) (x @ z) (y @ w)"
+ − 701
by (rule pred_compI) (rule a', rule d')
+ − 702
qed
+ − 703
+ − 704
text {* Raw theorems. Finsert, memb, singleron, sub_list *}
1518
+ − 705
1892
+ − 706
lemma nil_not_cons:
+ − 707
shows "\<not> ([] \<approx> x # xs)"
+ − 708
and "\<not> (x # xs \<approx> [])"
+ − 709
by auto
+ − 710
1878
+ − 711
lemma no_memb_nil:
+ − 712
"(\<forall>x. \<not> memb x xs) = (xs = [])"
+ − 713
by (simp add: memb_def)
+ − 714
1518
+ − 715
lemma memb_consI1:
+ − 716
shows "memb x (x # xs)"
+ − 717
by (simp add: memb_def)
+ − 718
+ − 719
lemma memb_consI2:
+ − 720
shows "memb x xs \<Longrightarrow> memb x (y # xs)"
+ − 721
by (simp add: memb_def)
+ − 722
+ − 723
lemma singleton_list_eq:
+ − 724
shows "[x] \<approx> [y] \<longleftrightarrow> x = y"
+ − 725
by (simp add: id_simps) auto
+ − 726
1892
+ − 727
lemma sub_list_cons:
+ − 728
"sub_list (x # xs) ys = (memb x ys \<and> sub_list xs ys)"
+ − 729
by (auto simp add: memb_def sub_list_def)
+ − 730
2084
+ − 731
lemma fminus_raw_red: "fminus_raw (x # xs) ys = (if memb x ys then fminus_raw xs ys else x # (fminus_raw xs ys))"
+ − 732
by (induct ys arbitrary: xs x)
+ − 733
(simp_all add: not_memb_nil memb_delete_raw memb_cons_iff)
+ − 734
1935
+ − 735
text {* Cardinality of finite sets *}
1518
+ − 736
1813
+ − 737
lemma fcard_raw_0:
1860
+ − 738
shows "fcard_raw xs = 0 \<longleftrightarrow> xs \<approx> []"
1821
+ − 739
by (induct xs) (auto simp add: memb_def)
1813
+ − 740
+ − 741
lemma fcard_raw_not_memb:
1860
+ − 742
shows "\<not> memb x xs \<longleftrightarrow> fcard_raw (x # xs) = Suc (fcard_raw xs)"
1813
+ − 743
by auto
+ − 744
+ − 745
lemma fcard_raw_suc:
1860
+ − 746
assumes a: "fcard_raw xs = Suc n"
+ − 747
shows "\<exists>x ys. \<not> (memb x ys) \<and> xs \<approx> (x # ys) \<and> fcard_raw ys = n"
+ − 748
using a
+ − 749
by (induct xs) (auto simp add: memb_def split: if_splits)
1819
+ − 750
1935
+ − 751
lemma singleton_fcard_1:
1860
+ − 752
shows "set xs = {x} \<Longrightarrow> fcard_raw xs = 1"
+ − 753
by (induct xs) (auto simp add: memb_def subset_insert)
1819
+ − 754
+ − 755
lemma fcard_raw_1:
1823
+ − 756
shows "fcard_raw xs = 1 \<longleftrightarrow> (\<exists>x. xs \<approx> [x])"
+ − 757
apply (auto dest!: fcard_raw_suc)
1819
+ − 758
apply (simp add: fcard_raw_0)
1821
+ − 759
apply (rule_tac x="x" in exI)
1819
+ − 760
apply simp
1821
+ − 761
apply (subgoal_tac "set xs = {x}")
1860
+ − 762
apply (drule singleton_fcard_1)
1819
+ − 763
apply auto
1813
+ − 764
done
+ − 765
1878
+ − 766
lemma fcard_raw_suc_memb:
+ − 767
assumes a: "fcard_raw A = Suc n"
+ − 768
shows "\<exists>a. memb a A"
+ − 769
using a
1938
+ − 770
by (induct A) (auto simp add: memb_def)
1878
+ − 771
1884
+ − 772
lemma memb_card_not_0:
1878
+ − 773
assumes a: "memb a A"
+ − 774
shows "\<not>(fcard_raw A = 0)"
1883
+ − 775
proof -
+ − 776
have "\<not>(\<forall>x. \<not> memb x A)" using a by auto
+ − 777
then have "\<not>A \<approx> []" using none_memb_nil[of A] by simp
+ − 778
then show ?thesis using fcard_raw_0[of A] by simp
+ − 779
qed
1878
+ − 780
1935
+ − 781
text {* fmap *}
1518
+ − 782
1813
+ − 783
lemma map_append:
1821
+ − 784
"map f (xs @ ys) \<approx> (map f xs) @ (map f ys)"
1813
+ − 785
by simp
+ − 786
1819
+ − 787
lemma memb_append:
1823
+ − 788
"memb x (xs @ ys) \<longleftrightarrow> memb x xs \<or> memb x ys"
1821
+ − 789
by (induct xs) (simp_all add: not_memb_nil memb_cons_iff)
1819
+ − 790
1518
+ − 791
lemma cons_left_comm:
1821
+ − 792
"x # y # xs \<approx> y # x # xs"
+ − 793
by auto
1518
+ − 794
+ − 795
lemma cons_left_idem:
1821
+ − 796
"x # x # xs \<approx> x # xs"
+ − 797
by auto
1518
+ − 798
1819
+ − 799
lemma fset_raw_strong_cases:
2084
+ − 800
obtains "xs = []"
+ − 801
| x ys where "\<not> memb x ys" and "xs \<approx> x # ys"
+ − 802
proof (induct xs arbitrary: x ys)
+ − 803
case Nil
+ − 804
then show thesis by simp
+ − 805
next
+ − 806
case (Cons a xs)
+ − 807
have a: "\<lbrakk>xs = [] \<Longrightarrow> thesis; \<And>x ys. \<lbrakk>\<not> memb x ys; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis" by fact
+ − 808
have b: "\<And>x' ys'. \<lbrakk>\<not> memb x' ys'; a # xs \<approx> x' # ys'\<rbrakk> \<Longrightarrow> thesis" by fact
+ − 809
have c: "xs = [] \<Longrightarrow> thesis" by (metis no_memb_nil singleton_list_eq b)
+ − 810
have "\<And>x ys. \<lbrakk>\<not> memb x ys; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis"
+ − 811
proof -
+ − 812
fix x :: 'a
+ − 813
fix ys :: "'a list"
+ − 814
assume d:"\<not> memb x ys"
+ − 815
assume e:"xs \<approx> x # ys"
+ − 816
show thesis
+ − 817
proof (cases "x = a")
+ − 818
assume h: "x = a"
+ − 819
then have f: "\<not> memb a ys" using d by simp
+ − 820
have g: "a # xs \<approx> a # ys" using e h by auto
+ − 821
show thesis using b f g by simp
+ − 822
next
+ − 823
assume h: "x \<noteq> a"
+ − 824
then have f: "\<not> memb x (a # ys)" using d unfolding memb_def by auto
+ − 825
have g: "a # xs \<approx> x # (a # ys)" using e h by auto
+ − 826
show thesis using b f g by simp
+ − 827
qed
+ − 828
qed
+ − 829
then show thesis using a c by blast
+ − 830
qed
1518
+ − 831
1860
+ − 832
section {* deletion *}
+ − 833
1819
+ − 834
lemma memb_delete_raw_ident:
1860
+ − 835
shows "\<not> memb x (delete_raw xs x)"
1821
+ − 836
by (induct xs) (auto simp add: memb_def)
1518
+ − 837
1819
+ − 838
lemma fset_raw_delete_raw_cases:
1821
+ − 839
"xs = [] \<or> (\<exists>x. memb x xs \<and> xs \<approx> x # delete_raw xs x)"
+ − 840
by (induct xs) (auto simp add: memb_def)
1518
+ − 841
1819
+ − 842
lemma fdelete_raw_filter:
+ − 843
"delete_raw xs y = [x \<leftarrow> xs. x \<noteq> y]"
+ − 844
by (induct xs) simp_all
1518
+ − 845
1819
+ − 846
lemma fcard_raw_delete:
+ − 847
"fcard_raw (delete_raw xs y) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"
+ − 848
by (simp add: fdelete_raw_filter fcard_raw_delete_one)
1518
+ − 849
1819
+ − 850
lemma finter_raw_empty:
+ − 851
"finter_raw l [] = []"
+ − 852
by (induct l) (simp_all add: not_memb_nil)
+ − 853
2084
+ − 854
lemma set_cong:
+ − 855
shows "(x \<approx> y) = (set x = set y)"
1821
+ − 856
by auto
1533
+ − 857
+ − 858
lemma inj_map_eq_iff:
+ − 859
"inj f \<Longrightarrow> (map f l \<approx> map f m) = (l \<approx> m)"
+ − 860
by (simp add: expand_set_eq[symmetric] inj_image_eq_iff)
+ − 861
1888
+ − 862
text {* alternate formulation with a different decomposition principle
+ − 863
and a proof of equivalence *}
+ − 864
+ − 865
inductive
+ − 866
list_eq2
+ − 867
where
+ − 868
"list_eq2 (a # b # xs) (b # a # xs)"
+ − 869
| "list_eq2 [] []"
+ − 870
| "list_eq2 xs ys \<Longrightarrow> list_eq2 ys xs"
+ − 871
| "list_eq2 (a # a # xs) (a # xs)"
+ − 872
| "list_eq2 xs ys \<Longrightarrow> list_eq2 (a # xs) (a # ys)"
+ − 873
| "\<lbrakk>list_eq2 xs1 xs2; list_eq2 xs2 xs3\<rbrakk> \<Longrightarrow> list_eq2 xs1 xs3"
+ − 874
+ − 875
lemma list_eq2_refl:
+ − 876
shows "list_eq2 xs xs"
+ − 877
by (induct xs) (auto intro: list_eq2.intros)
+ − 878
+ − 879
lemma cons_delete_list_eq2:
+ − 880
shows "list_eq2 (a # (delete_raw A a)) (if memb a A then A else a # A)"
+ − 881
apply (induct A)
+ − 882
apply (simp add: memb_def list_eq2_refl)
+ − 883
apply (case_tac "memb a (aa # A)")
+ − 884
apply (simp_all only: memb_cons_iff)
+ − 885
apply (case_tac [!] "a = aa")
1909
+ − 886
apply (simp_all)
1888
+ − 887
apply (case_tac "memb a A")
+ − 888
apply (auto simp add: memb_def)[2]
+ − 889
apply (metis list_eq2.intros(3) list_eq2.intros(4) list_eq2.intros(5) list_eq2.intros(6))
1895
+ − 890
apply (metis list_eq2.intros(1) list_eq2.intros(5) list_eq2.intros(6))
1888
+ − 891
apply (auto simp add: list_eq2_refl not_memb_delete_raw_ident)
+ − 892
done
+ − 893
+ − 894
lemma memb_delete_list_eq2:
+ − 895
assumes a: "memb e r"
+ − 896
shows "list_eq2 (e # delete_raw r e) r"
+ − 897
using a cons_delete_list_eq2[of e r]
+ − 898
by simp
+ − 899
1909
+ − 900
lemma delete_raw_rsp:
+ − 901
"xs \<approx> ys \<Longrightarrow> delete_raw xs x \<approx> delete_raw ys x"
+ − 902
by (simp add: memb_def[symmetric] memb_delete_raw)
+ − 903
1888
+ − 904
lemma list_eq2_equiv:
+ − 905
"(l \<approx> r) \<longleftrightarrow> (list_eq2 l r)"
+ − 906
proof
+ − 907
show "list_eq2 l r \<Longrightarrow> l \<approx> r" by (induct rule: list_eq2.induct) auto
1938
+ − 908
next
+ − 909
{
+ − 910
fix n
+ − 911
assume a: "fcard_raw l = n" and b: "l \<approx> r"
+ − 912
have "list_eq2 l r"
+ − 913
using a b
+ − 914
proof (induct n arbitrary: l r)
+ − 915
case 0
+ − 916
have "fcard_raw l = 0" by fact
+ − 917
then have "\<forall>x. \<not> memb x l" using memb_card_not_0[of _ l] by auto
+ − 918
then have z: "l = []" using no_memb_nil by auto
+ − 919
then have "r = []" using `l \<approx> r` by simp
+ − 920
then show ?case using z list_eq2_refl by simp
+ − 921
next
+ − 922
case (Suc m)
+ − 923
have b: "l \<approx> r" by fact
+ − 924
have d: "fcard_raw l = Suc m" by fact
2084
+ − 925
then have "\<exists>a. memb a l" by (rule fcard_raw_suc_memb)
1938
+ − 926
then obtain a where e: "memb a l" by auto
+ − 927
then have e': "memb a r" using list_eq.simps[simplified memb_def[symmetric], of l r] b by auto
+ − 928
have f: "fcard_raw (delete_raw l a) = m" using fcard_raw_delete[of l a] e d by simp
+ − 929
have g: "delete_raw l a \<approx> delete_raw r a" using delete_raw_rsp[OF b] by simp
2084
+ − 930
have "list_eq2 (delete_raw l a) (delete_raw r a)" by (rule Suc.hyps[OF f g])
+ − 931
then have h: "list_eq2 (a # delete_raw l a) (a # delete_raw r a)" by (rule list_eq2.intros(5))
1938
+ − 932
have i: "list_eq2 l (a # delete_raw l a)"
+ − 933
by (rule list_eq2.intros(3)[OF memb_delete_list_eq2[OF e]])
+ − 934
have "list_eq2 l (a # delete_raw r a)" by (rule list_eq2.intros(6)[OF i h])
+ − 935
then show ?case using list_eq2.intros(6)[OF _ memb_delete_list_eq2[OF e']] by simp
+ − 936
qed
+ − 937
}
+ − 938
then show "l \<approx> r \<Longrightarrow> list_eq2 l r" by blast
1888
+ − 939
qed
+ − 940
2084
+ − 941
text {* Set *}
+ − 942
+ − 943
lemma sub_list_set: "sub_list xs ys = (set xs \<subseteq> set ys)"
+ − 944
by (metis rev_append set_append set_cong set_rev sub_list_append sub_list_append_left sub_list_def sub_list_not_eq subset_Un_eq)
+ − 945
+ − 946
lemma sub_list_neq_set: "(sub_list xs ys \<and> \<not> list_eq xs ys) = (set xs \<subset> set ys)"
+ − 947
by (auto simp add: sub_list_set)
+ − 948
+ − 949
lemma fcard_raw_set: "fcard_raw xs = card (set xs)"
+ − 950
by (induct xs) (auto simp add: insert_absorb memb_def card_insert_disjoint finite_set)
+ − 951
+ − 952
lemma memb_set: "memb x xs = (x \<in> set xs)"
+ − 953
by (simp only: memb_def)
+ − 954
+ − 955
lemma filter_set: "set (filter P xs) = P \<inter> (set xs)"
+ − 956
by (induct xs, simp)
+ − 957
(metis Int_insert_right_if0 Int_insert_right_if1 List.set.simps(2) filter.simps(2) mem_def)
+ − 958
+ − 959
lemma delete_raw_set: "set (delete_raw xs x) = set xs - {x}"
+ − 960
by (induct xs) auto
+ − 961
+ − 962
lemma inter_raw_set: "set (finter_raw xs ys) = set xs \<inter> set ys"
+ − 963
by (induct xs) (simp_all add: memb_def)
+ − 964
+ − 965
lemma fminus_raw_set: "set (fminus_raw xs ys) = set xs - set ys"
+ − 966
by (induct ys arbitrary: xs)
+ − 967
(simp_all add: fminus_raw.simps delete_raw_set, blast)
+ − 968
+ − 969
text {* Raw theorems of ffilter *}
+ − 970
+ − 971
lemma sub_list_filter: "sub_list (filter P xs) (filter Q xs) = (\<forall> x. memb x xs \<longrightarrow> P x \<longrightarrow> Q x)"
+ − 972
unfolding sub_list_def memb_def by auto
+ − 973
+ − 974
lemma list_eq_filter: "list_eq (filter P xs) (filter Q xs) = (\<forall>x. memb x xs \<longrightarrow> P x = Q x)"
+ − 975
unfolding memb_def by auto
+ − 976
1935
+ − 977
text {* Lifted theorems *}
1518
+ − 978
1819
+ − 979
lemma not_fin_fnil: "x |\<notin>| {||}"
+ − 980
by (lifting not_memb_nil)
1518
+ − 981
+ − 982
lemma fin_finsert_iff[simp]:
+ − 983
"x |\<in>| finsert y S = (x = y \<or> x |\<in>| S)"
+ − 984
by (lifting memb_cons_iff)
+ − 985
+ − 986
lemma
+ − 987
shows finsertI1: "x |\<in>| finsert x S"
+ − 988
and finsertI2: "x |\<in>| S \<Longrightarrow> x |\<in>| finsert y S"
+ − 989
by (lifting memb_consI1, lifting memb_consI2)
+ − 990
+ − 991
lemma finsert_absorb[simp]:
+ − 992
shows "x |\<in>| S \<Longrightarrow> finsert x S = S"
+ − 993
by (lifting memb_absorb)
+ − 994
+ − 995
lemma fempty_not_finsert[simp]:
1533
+ − 996
"{||} \<noteq> finsert x S"
+ − 997
"finsert x S \<noteq> {||}"
1518
+ − 998
by (lifting nil_not_cons)
+ − 999
+ − 1000
lemma finsert_left_comm:
1822
+ − 1001
"finsert x (finsert y S) = finsert y (finsert x S)"
1518
+ − 1002
by (lifting cons_left_comm)
+ − 1003
+ − 1004
lemma finsert_left_idem:
1822
+ − 1005
"finsert x (finsert x S) = finsert x S"
1518
+ − 1006
by (lifting cons_left_idem)
+ − 1007
+ − 1008
lemma fsingleton_eq[simp]:
+ − 1009
shows "{|x|} = {|y|} \<longleftrightarrow> x = y"
+ − 1010
by (lifting singleton_list_eq)
+ − 1011
+ − 1012
text {* fset_to_set *}
+ − 1013
1533
+ − 1014
lemma fset_to_set_simps[simp]:
1819
+ − 1015
"fset_to_set {||} = ({} :: 'a set)"
+ − 1016
"fset_to_set (finsert (h :: 'a) t) = insert h (fset_to_set t)"
+ − 1017
by (lifting set.simps)
1518
+ − 1018
+ − 1019
lemma in_fset_to_set:
1822
+ − 1020
"x \<in> fset_to_set S \<equiv> x |\<in>| S"
1518
+ − 1021
by (lifting memb_def[symmetric])
+ − 1022
1819
+ − 1023
lemma none_fin_fempty:
1824
+ − 1024
"(\<forall>x. x |\<notin>| S) = (S = {||})"
+ − 1025
by (lifting none_memb_nil)
1518
+ − 1026
1533
+ − 1027
lemma fset_cong:
2084
+ − 1028
"(S = T) = (fset_to_set S = fset_to_set T)"
1533
+ − 1029
by (lifting set_cong)
+ − 1030
1518
+ − 1031
text {* fcard *}
+ − 1032
+ − 1033
lemma fcard_fempty [simp]:
+ − 1034
shows "fcard {||} = 0"
+ − 1035
by (lifting fcard_raw_nil)
+ − 1036
+ − 1037
lemma fcard_finsert_if [simp]:
+ − 1038
shows "fcard (finsert x S) = (if x |\<in>| S then fcard S else Suc (fcard S))"
+ − 1039
by (lifting fcard_raw_cons)
+ − 1040
1822
+ − 1041
lemma fcard_0: "(fcard S = 0) = (S = {||})"
1813
+ − 1042
by (lifting fcard_raw_0)
+ − 1043
1821
+ − 1044
lemma fcard_1:
1822
+ − 1045
shows "(fcard S = 1) = (\<exists>x. S = {|x|})"
1819
+ − 1046
by (lifting fcard_raw_1)
+ − 1047
2084
+ − 1048
lemma fcard_gt_0:
1860
+ − 1049
shows "x \<in> fset_to_set S \<Longrightarrow> 0 < fcard S"
1518
+ − 1050
by (lifting fcard_raw_gt_0)
+ − 1051
2084
+ − 1052
lemma fcard_not_fin:
1860
+ − 1053
shows "(x |\<notin>| S) = (fcard (finsert x S) = Suc (fcard S))"
1813
+ − 1054
by (lifting fcard_raw_not_memb)
+ − 1055
1822
+ − 1056
lemma fcard_suc: "fcard S = Suc n \<Longrightarrow> \<exists>x T. x |\<notin>| T \<and> S = finsert x T \<and> fcard T = n"
1813
+ − 1057
by (lifting fcard_raw_suc)
+ − 1058
1819
+ − 1059
lemma fcard_delete:
1822
+ − 1060
"fcard (fdelete S y) = (if y |\<in>| S then fcard S - 1 else fcard S)"
1819
+ − 1061
by (lifting fcard_raw_delete)
+ − 1062
1878
+ − 1063
lemma fcard_suc_memb: "fcard A = Suc n \<Longrightarrow> \<exists>a. a |\<in>| A"
+ − 1064
by (lifting fcard_raw_suc_memb)
+ − 1065
+ − 1066
lemma fin_fcard_not_0: "a |\<in>| A \<Longrightarrow> fcard A \<noteq> 0"
1887
+ − 1067
by (lifting memb_card_not_0)
1878
+ − 1068
1518
+ − 1069
text {* funion *}
+ − 1070
2084
+ − 1071
lemmas [simp] =
+ − 1072
sup_bot_left[where 'a="'a fset", standard]
+ − 1073
sup_bot_right[where 'a="'a fset", standard]
1518
+ − 1074
2084
+ − 1075
lemma funion_finsert[simp]:
+ − 1076
shows "finsert x S |\<union>| T = finsert x (S |\<union>| T)"
+ − 1077
by (lifting append.simps(2))
1887
+ − 1078
+ − 1079
lemma singleton_union_left:
+ − 1080
"{|a|} |\<union>| S = finsert a S"
+ − 1081
by simp
+ − 1082
+ − 1083
lemma singleton_union_right:
+ − 1084
"S |\<union>| {|a|} = finsert a S"
1907
+ − 1085
by (subst sup.commute) simp
1887
+ − 1086
1518
+ − 1087
section {* Induction and Cases rules for finite sets *}
+ − 1088
+ − 1089
lemma fset_strong_cases:
2084
+ − 1090
obtains "xs = {||}"
+ − 1091
| x ys where "x |\<notin>| ys" and "xs = finsert x ys"
1819
+ − 1092
by (lifting fset_raw_strong_cases)
1518
+ − 1093
+ − 1094
lemma fset_exhaust[case_names fempty finsert, cases type: fset]:
+ − 1095
shows "\<lbrakk>S = {||} \<Longrightarrow> P; \<And>x S'. S = finsert x S' \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
+ − 1096
by (lifting list.exhaust)
+ − 1097
1533
+ − 1098
lemma fset_induct_weak[case_names fempty finsert]:
1518
+ − 1099
shows "\<lbrakk>P {||}; \<And>x S. P S \<Longrightarrow> P (finsert x S)\<rbrakk> \<Longrightarrow> P S"
+ − 1100
by (lifting list.induct)
+ − 1101
1533
+ − 1102
lemma fset_induct[case_names fempty finsert, induct type: fset]:
2084
+ − 1103
assumes prem1: "P {||}"
1518
+ − 1104
and prem2: "\<And>x S. \<lbrakk>x |\<notin>| S; P S\<rbrakk> \<Longrightarrow> P (finsert x S)"
+ − 1105
shows "P S"
1533
+ − 1106
proof(induct S rule: fset_induct_weak)
1518
+ − 1107
case fempty
+ − 1108
show "P {||}" by (rule prem1)
+ − 1109
next
+ − 1110
case (finsert x S)
+ − 1111
have asm: "P S" by fact
+ − 1112
show "P (finsert x S)"
1938
+ − 1113
by (cases "x |\<in>| S") (simp_all add: asm prem2)
1518
+ − 1114
qed
+ − 1115
1533
+ − 1116
lemma fset_induct2:
+ − 1117
"P {||} {||} \<Longrightarrow>
+ − 1118
(\<And>x xs. x |\<notin>| xs \<Longrightarrow> P (finsert x xs) {||}) \<Longrightarrow>
+ − 1119
(\<And>y ys. y |\<notin>| ys \<Longrightarrow> P {||} (finsert y ys)) \<Longrightarrow>
+ − 1120
(\<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>
+ − 1121
P xsa ysa"
+ − 1122
apply (induct xsa arbitrary: ysa)
+ − 1123
apply (induct_tac x rule: fset_induct)
+ − 1124
apply simp_all
+ − 1125
apply (induct_tac xa rule: fset_induct)
+ − 1126
apply simp_all
+ − 1127
done
1518
+ − 1128
2084
+ − 1129
lemma fset_fcard_induct:
+ − 1130
assumes a: "P {||}"
+ − 1131
and b: "\<And>xs ys. Suc (fcard xs) = (fcard ys) \<Longrightarrow> P xs \<Longrightarrow> P ys"
+ − 1132
shows "P zs"
+ − 1133
proof (induct zs)
+ − 1134
show "P {||}" by (rule a)
+ − 1135
next
+ − 1136
fix x :: 'a and zs :: "'a fset"
+ − 1137
assume h: "P zs"
+ − 1138
assume "x |\<notin>| zs"
+ − 1139
then have H1: "Suc (fcard zs) = fcard (finsert x zs)" using fcard_suc by auto
+ − 1140
then show "P (finsert x zs)" using b h by simp
+ − 1141
qed
+ − 1142
1819
+ − 1143
text {* fmap *}
+ − 1144
1533
+ − 1145
lemma fmap_simps[simp]:
+ − 1146
"fmap (f :: 'a \<Rightarrow> 'b) {||} = {||}"
1822
+ − 1147
"fmap f (finsert x S) = finsert (f x) (fmap f S)"
1533
+ − 1148
by (lifting map.simps)
+ − 1149
+ − 1150
lemma fmap_set_image:
1822
+ − 1151
"fset_to_set (fmap f S) = f ` (fset_to_set S)"
2084
+ − 1152
by (induct S) simp_all
1533
+ − 1153
+ − 1154
lemma inj_fmap_eq_iff:
1822
+ − 1155
"inj f \<Longrightarrow> (fmap f S = fmap f T) = (S = T)"
1533
+ − 1156
by (lifting inj_map_eq_iff)
+ − 1157
1822
+ − 1158
lemma fmap_funion: "fmap f (S |\<union>| T) = fmap f S |\<union>| fmap f T"
1813
+ − 1159
by (lifting map_append)
+ − 1160
1819
+ − 1161
lemma fin_funion:
1822
+ − 1162
"x |\<in>| S |\<union>| T \<longleftrightarrow> x |\<in>| S \<or> x |\<in>| T"
1819
+ − 1163
by (lifting memb_append)
+ − 1164
2084
+ − 1165
text {* to_set *}
+ − 1166
+ − 1167
lemma fin_set: "(x |\<in>| xs) = (x \<in> fset_to_set xs)"
+ − 1168
by (lifting memb_set)
+ − 1169
+ − 1170
lemma fnotin_set: "(x |\<notin>| xs) = (x \<notin> fset_to_set xs)"
+ − 1171
by (simp add: fin_set)
+ − 1172
+ − 1173
lemma fcard_set: "fcard xs = card (fset_to_set xs)"
+ − 1174
by (lifting fcard_raw_set)
+ − 1175
+ − 1176
lemma fsubseteq_set: "(xs |\<subseteq>| ys) = (fset_to_set xs \<subseteq> fset_to_set ys)"
+ − 1177
by (lifting sub_list_set)
+ − 1178
+ − 1179
lemma fsubset_set: "(xs |\<subset>| ys) = (fset_to_set xs \<subset> fset_to_set ys)"
+ − 1180
unfolding less_fset by (lifting sub_list_neq_set)
+ − 1181
+ − 1182
lemma ffilter_set: "fset_to_set (ffilter P xs) = P \<inter> fset_to_set xs"
+ − 1183
by (lifting filter_set)
+ − 1184
+ − 1185
lemma fdelete_set: "fset_to_set (fdelete xs x) = fset_to_set xs - {x}"
+ − 1186
by (lifting delete_raw_set)
+ − 1187
+ − 1188
lemma inter_set: "fset_to_set (xs |\<inter>| ys) = fset_to_set xs \<inter> fset_to_set ys"
+ − 1189
by (lifting inter_raw_set)
+ − 1190
+ − 1191
lemma union_set: "fset_to_set (xs |\<union>| ys) = fset_to_set xs \<union> fset_to_set ys"
+ − 1192
by (lifting set_append)
+ − 1193
+ − 1194
lemma fminus_set: "fset_to_set (xs - ys) = fset_to_set xs - fset_to_set ys"
+ − 1195
by (lifting fminus_raw_set)
+ − 1196
+ − 1197
lemmas fset_to_set_trans =
+ − 1198
fin_set fnotin_set fcard_set fsubseteq_set fsubset_set
+ − 1199
inter_set union_set ffilter_set fset_to_set_simps
+ − 1200
fset_cong fdelete_set fmap_set_image fminus_set
+ − 1201
+ − 1202
1819
+ − 1203
text {* ffold *}
+ − 1204
+ − 1205
lemma ffold_nil: "ffold f z {||} = z"
+ − 1206
by (lifting ffold_raw.simps(1)[where 'a="'b" and 'b="'a"])
+ − 1207
+ − 1208
lemma ffold_finsert: "ffold f z (finsert a A) =
+ − 1209
(if rsp_fold f then if a |\<in>| A then ffold f z A else f a (ffold f z A) else z)"
+ − 1210
by (lifting ffold_raw.simps(2)[where 'a="'b" and 'b="'a"])
+ − 1211
+ − 1212
lemma fin_commute_ffold:
+ − 1213
"\<lbrakk>rsp_fold f; h |\<in>| b\<rbrakk> \<Longrightarrow> ffold f z b = f h (ffold f z (fdelete b h))"
+ − 1214
by (lifting memb_commute_ffold_raw)
+ − 1215
+ − 1216
text {* fdelete *}
+ − 1217
2084
+ − 1218
lemma fin_fdelete:
1822
+ − 1219
shows "x |\<in>| fdelete S y \<longleftrightarrow> x |\<in>| S \<and> x \<noteq> y"
1819
+ − 1220
by (lifting memb_delete_raw)
+ − 1221
2084
+ − 1222
lemma fin_fdelete_ident:
1822
+ − 1223
shows "x |\<notin>| fdelete S x"
1819
+ − 1224
by (lifting memb_delete_raw_ident)
+ − 1225
2084
+ − 1226
lemma not_memb_fdelete_ident:
1822
+ − 1227
shows "x |\<notin>| S \<Longrightarrow> fdelete S x = S"
1819
+ − 1228
by (lifting not_memb_delete_raw_ident)
+ − 1229
+ − 1230
lemma fset_fdelete_cases:
1822
+ − 1231
shows "S = {||} \<or> (\<exists>x. x |\<in>| S \<and> S = finsert x (fdelete S x))"
1819
+ − 1232
by (lifting fset_raw_delete_raw_cases)
+ − 1233
+ − 1234
text {* inter *}
+ − 1235
1822
+ − 1236
lemma finter_empty_l: "({||} |\<inter>| S) = {||}"
1819
+ − 1237
by (lifting finter_raw.simps(1))
+ − 1238
1822
+ − 1239
lemma finter_empty_r: "(S |\<inter>| {||}) = {||}"
1819
+ − 1240
by (lifting finter_raw_empty)
+ − 1241
+ − 1242
lemma finter_finsert:
1822
+ − 1243
"finsert x S |\<inter>| T = (if x |\<in>| T then finsert x (S |\<inter>| T) else S |\<inter>| T)"
1819
+ − 1244
by (lifting finter_raw.simps(2))
+ − 1245
+ − 1246
lemma fin_finter:
1822
+ − 1247
"x |\<in>| (S |\<inter>| T) \<longleftrightarrow> x |\<in>| S \<and> x |\<in>| T"
1819
+ − 1248
by (lifting memb_finter_raw)
+ − 1249
1893
+ − 1250
lemma fsubset_finsert:
+ − 1251
"(finsert x xs |\<subseteq>| ys) = (x |\<in>| ys \<and> xs |\<subseteq>| ys)"
+ − 1252
by (lifting sub_list_cons)
+ − 1253
1936
+ − 1254
lemma "xs |\<subseteq>| ys \<equiv> \<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys"
+ − 1255
by (lifting sub_list_def[simplified memb_def[symmetric]])
1893
+ − 1256
+ − 1257
lemma fsubset_fin: "xs |\<subseteq>| ys = (\<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys)"
+ − 1258
by (rule meta_eq_to_obj_eq)
+ − 1259
(lifting sub_list_def[simplified memb_def[symmetric]])
+ − 1260
2084
+ − 1261
lemma fminus_fin: "(x |\<in>| xs - ys) = (x |\<in>| xs \<and> x |\<notin>| ys)"
+ − 1262
by (lifting fminus_raw_memb)
+ − 1263
+ − 1264
lemma fminus_red: "finsert x xs - ys = (if x |\<in>| ys then xs - ys else finsert x (xs - ys))"
+ − 1265
by (lifting fminus_raw_red)
+ − 1266
+ − 1267
lemma fminus_red_fin[simp]: "x |\<in>| ys \<Longrightarrow> finsert x xs - ys = xs - ys"
+ − 1268
by (simp add: fminus_red)
+ − 1269
+ − 1270
lemma fminus_red_fnotin[simp]: "x |\<notin>| ys \<Longrightarrow> finsert x xs - ys = finsert x (xs - ys)"
+ − 1271
by (simp add: fminus_red)
+ − 1272
1820
+ − 1273
lemma expand_fset_eq:
1822
+ − 1274
"(S = T) = (\<forall>x. (x |\<in>| S) = (x |\<in>| T))"
1820
+ − 1275
by (lifting list_eq.simps[simplified memb_def[symmetric]])
+ − 1276
1888
+ − 1277
(* We cannot write it as "assumes .. shows" since Isabelle changes
+ − 1278
the quantifiers to schematic variables and reintroduces them in
+ − 1279
a different order *)
+ − 1280
lemma fset_eq_cases:
+ − 1281
"\<lbrakk>a1 = a2;
+ − 1282
\<And>a b xs. \<lbrakk>a1 = finsert a (finsert b xs); a2 = finsert b (finsert a xs)\<rbrakk> \<Longrightarrow> P;
+ − 1283
\<lbrakk>a1 = {||}; a2 = {||}\<rbrakk> \<Longrightarrow> P; \<And>xs ys. \<lbrakk>a1 = ys; a2 = xs; xs = ys\<rbrakk> \<Longrightarrow> P;
+ − 1284
\<And>a xs. \<lbrakk>a1 = finsert a (finsert a xs); a2 = finsert a xs\<rbrakk> \<Longrightarrow> P;
+ − 1285
\<And>xs ys a. \<lbrakk>a1 = finsert a xs; a2 = finsert a ys; xs = ys\<rbrakk> \<Longrightarrow> P;
+ − 1286
\<And>xs1 xs2 xs3. \<lbrakk>a1 = xs1; a2 = xs3; xs1 = xs2; xs2 = xs3\<rbrakk> \<Longrightarrow> P\<rbrakk>
+ − 1287
\<Longrightarrow> P"
+ − 1288
by (lifting list_eq2.cases[simplified list_eq2_equiv[symmetric]])
+ − 1289
+ − 1290
lemma fset_eq_induct:
+ − 1291
assumes "x1 = x2"
+ − 1292
and "\<And>a b xs. P (finsert a (finsert b xs)) (finsert b (finsert a xs))"
+ − 1293
and "P {||} {||}"
+ − 1294
and "\<And>xs ys. \<lbrakk>xs = ys; P xs ys\<rbrakk> \<Longrightarrow> P ys xs"
+ − 1295
and "\<And>a xs. P (finsert a (finsert a xs)) (finsert a xs)"
+ − 1296
and "\<And>xs ys a. \<lbrakk>xs = ys; P xs ys\<rbrakk> \<Longrightarrow> P (finsert a xs) (finsert a ys)"
+ − 1297
and "\<And>xs1 xs2 xs3. \<lbrakk>xs1 = xs2; P xs1 xs2; xs2 = xs3; P xs2 xs3\<rbrakk> \<Longrightarrow> P xs1 xs3"
+ − 1298
shows "P x1 x2"
+ − 1299
using assms
+ − 1300
by (lifting list_eq2.induct[simplified list_eq2_equiv[symmetric]])
1820
+ − 1301
1935
+ − 1302
text {* concat *}
+ − 1303
+ − 1304
lemma fconcat_empty:
+ − 1305
shows "fconcat {||} = {||}"
+ − 1306
by (lifting concat.simps(1))
+ − 1307
+ − 1308
lemma fconcat_insert:
+ − 1309
shows "fconcat (finsert x S) = x |\<union>| fconcat S"
+ − 1310
by (lifting concat.simps(2))
+ − 1311
+ − 1312
lemma "fconcat (xs |\<union>| ys) = fconcat xs |\<union>| fconcat ys"
+ − 1313
by (lifting concat_append)
+ − 1314
2084
+ − 1315
text {* ffilter *}
+ − 1316
+ − 1317
lemma subseteq_filter: "ffilter P xs <= ffilter Q xs = (\<forall> x. x |\<in>| xs \<longrightarrow> P x \<longrightarrow> Q x)"
+ − 1318
by (lifting sub_list_filter)
+ − 1319
+ − 1320
lemma eq_ffilter: "(ffilter P xs = ffilter Q xs) = (\<forall>x. x |\<in>| xs \<longrightarrow> P x = Q x)"
+ − 1321
by (lifting list_eq_filter)
+ − 1322
+ − 1323
lemma subset_ffilter: "(\<And>x. x |\<in>| xs \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| xs & \<not> P x & Q x) \<Longrightarrow> ffilter P xs < ffilter Q xs"
+ − 1324
unfolding less_fset by (auto simp add: subseteq_filter eq_ffilter)
+ − 1325
+ − 1326
section {* lemmas transferred from Finite_Set theory *}
+ − 1327
+ − 1328
text {* finiteness for finite sets holds *}
+ − 1329
lemma finite_fset: "finite (fset_to_set S)"
+ − 1330
by (induct S) auto
+ − 1331
+ − 1332
lemma fset_choice: "\<forall>x. x |\<in>| A \<longrightarrow> (\<exists>y. P x y) \<Longrightarrow> \<exists>f. \<forall>x. x |\<in>| A \<longrightarrow> P x (f x)"
+ − 1333
unfolding fset_to_set_trans
+ − 1334
by (rule finite_set_choice[simplified Ball_def, OF finite_fset])
+ − 1335
+ − 1336
lemma fsubseteq_fnil: "xs |\<subseteq>| {||} = (xs = {||})"
+ − 1337
unfolding fset_to_set_trans
+ − 1338
by (rule subset_empty)
+ − 1339
+ − 1340
lemma not_fsubset_fnil: "\<not> xs |\<subset>| {||}"
+ − 1341
unfolding fset_to_set_trans
+ − 1342
by (rule not_psubset_empty)
+ − 1343
+ − 1344
lemma fcard_mono: "xs |\<subseteq>| ys \<Longrightarrow> fcard xs \<le> fcard ys"
+ − 1345
unfolding fset_to_set_trans
+ − 1346
by (rule card_mono[OF finite_fset])
+ − 1347
+ − 1348
lemma fcard_fseteq: "xs |\<subseteq>| ys \<Longrightarrow> fcard ys \<le> fcard xs \<Longrightarrow> xs = ys"
+ − 1349
unfolding fset_to_set_trans
+ − 1350
by (rule card_seteq[OF finite_fset])
+ − 1351
+ − 1352
lemma psubset_fcard_mono: "xs |\<subset>| ys \<Longrightarrow> fcard xs < fcard ys"
+ − 1353
unfolding fset_to_set_trans
+ − 1354
by (rule psubset_card_mono[OF finite_fset])
+ − 1355
+ − 1356
lemma fcard_funion_finter: "fcard xs + fcard ys = fcard (xs |\<union>| ys) + fcard (xs |\<inter>| ys)"
+ − 1357
unfolding fset_to_set_trans
+ − 1358
by (rule card_Un_Int[OF finite_fset finite_fset])
+ − 1359
+ − 1360
lemma fcard_funion_disjoint: "xs |\<inter>| ys = {||} \<Longrightarrow> fcard (xs |\<union>| ys) = fcard xs + fcard ys"
+ − 1361
unfolding fset_to_set_trans
+ − 1362
by (rule card_Un_disjoint[OF finite_fset finite_fset])
+ − 1363
+ − 1364
lemma fcard_delete1_less: "x |\<in>| xs \<Longrightarrow> fcard (fdelete xs x) < fcard xs"
+ − 1365
unfolding fset_to_set_trans
+ − 1366
by (rule card_Diff1_less[OF finite_fset])
+ − 1367
+ − 1368
lemma fcard_delete2_less: "x |\<in>| xs \<Longrightarrow> y |\<in>| xs \<Longrightarrow> fcard (fdelete (fdelete xs x) y) < fcard xs"
+ − 1369
unfolding fset_to_set_trans
+ − 1370
by (rule card_Diff2_less[OF finite_fset])
+ − 1371
+ − 1372
lemma fcard_delete1_le: "fcard (fdelete xs x) <= fcard xs"
+ − 1373
unfolding fset_to_set_trans
+ − 1374
by (rule card_Diff1_le[OF finite_fset])
+ − 1375
+ − 1376
lemma fcard_psubset: "ys |\<subseteq>| xs \<Longrightarrow> fcard ys < fcard xs \<Longrightarrow> ys |\<subset>| xs"
+ − 1377
unfolding fset_to_set_trans
+ − 1378
by (rule card_psubset[OF finite_fset])
+ − 1379
+ − 1380
lemma fcard_fmap_le: "fcard (fmap f xs) \<le> fcard xs"
+ − 1381
unfolding fset_to_set_trans
+ − 1382
by (rule card_image_le[OF finite_fset])
+ − 1383
+ − 1384
lemma fin_fminus_fnotin: "x |\<in>| F - S \<Longrightarrow> x |\<notin>| S"
+ − 1385
unfolding fset_to_set_trans
+ − 1386
by blast
+ − 1387
+ − 1388
lemma fin_fnotin_fminus: "x |\<in>| S \<Longrightarrow> x |\<notin>| F - S"
+ − 1389
unfolding fset_to_set_trans
+ − 1390
by blast
+ − 1391
+ − 1392
lemma fin_mdef: "x |\<in>| F = ((x |\<notin>| (F - {|x|})) & (F = finsert x (F - {|x|})))"
+ − 1393
unfolding fset_to_set_trans
+ − 1394
by blast
+ − 1395
+ − 1396
lemma fcard_fminus_finsert[simp]:
+ − 1397
assumes "a |\<in>| A" and "a |\<notin>| B"
+ − 1398
shows "fcard(A - finsert a B) = fcard(A - B) - 1"
+ − 1399
using assms unfolding fset_to_set_trans
+ − 1400
by (rule card_Diff_insert[OF finite_fset])
+ − 1401
+ − 1402
lemma fcard_fminus_fsubset:
+ − 1403
assumes "B |\<subseteq>| A"
+ − 1404
shows "fcard (A - B) = fcard A - fcard B"
+ − 1405
using assms unfolding fset_to_set_trans
+ − 1406
by (rule card_Diff_subset[OF finite_fset])
+ − 1407
+ − 1408
lemma fcard_fminus_subset_finter:
+ − 1409
"fcard (A - B) = fcard A - fcard (A |\<inter>| B)"
+ − 1410
unfolding fset_to_set_trans
+ − 1411
by (rule card_Diff_subset_Int) (fold inter_set, rule finite_fset)
+ − 1412
2249
+ − 1413
lemma ball_reg_right_unfolded: "(\<forall>x. R x \<longrightarrow> P x \<longrightarrow> Q x) \<longrightarrow> (All P \<longrightarrow> Ball R Q)"
+ − 1414
apply rule
+ − 1415
apply (rule ball_reg_right)
+ − 1416
apply auto
+ − 1417
done
2234
+ − 1418
2266
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1419
lemma list_rel_refl:
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1420
assumes q: "equivp R"
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1421
shows "(list_rel R) r r"
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1422
by (rule list_rel_refl) (metis equivp_def fset_equivp q)
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1423
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1424
lemma compose_list_refl2:
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1425
assumes q: "equivp R"
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1426
shows "(list_rel R OOO op \<approx>) r r"
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1427
proof
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1428
have *: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp])
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1429
show "list_rel R r r" by (rule list_rel_refl[OF q])
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1430
with * show "(op \<approx> OO list_rel R) r r" ..
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1431
qed
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1432
2285
+ − 1433
lemma quotient_compose_list_g:
2266
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1434
assumes q: "Quotient R Abs Rep"
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1435
and e: "equivp R"
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1436
shows "Quotient ((list_rel R) OOO (op \<approx>))
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1437
(abs_fset \<circ> (map Abs)) ((map Rep) \<circ> rep_fset)"
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1438
unfolding Quotient_def comp_def
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1439
proof (intro conjI allI)
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1440
fix a r s
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1441
show "abs_fset (map Abs (map Rep (rep_fset a))) = a"
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1442
by (simp add: abs_o_rep[OF q] Quotient_abs_rep[OF Quotient_fset] map_id)
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1443
have b: "list_rel R (map Rep (rep_fset a)) (map Rep (rep_fset a))"
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1444
by (rule list_rel_refl[OF e])
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1445
have c: "(op \<approx> OO list_rel R) (map Rep (rep_fset a)) (map Rep (rep_fset a))"
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1446
by (rule, rule equivp_reflp[OF fset_equivp]) (rule b)
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1447
show "(list_rel R OOO op \<approx>) (map Rep (rep_fset a)) (map Rep (rep_fset a))"
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1448
by (rule, rule list_rel_refl[OF e]) (rule c)
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1449
show "(list_rel R OOO op \<approx>) r s = ((list_rel R OOO op \<approx>) r r \<and>
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1450
(list_rel R OOO op \<approx>) s s \<and> abs_fset (map Abs r) = abs_fset (map Abs s))"
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1451
proof (intro iffI conjI)
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1452
show "(list_rel R OOO op \<approx>) r r" by (rule compose_list_refl2[OF e])
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1453
show "(list_rel R OOO op \<approx>) s s" by (rule compose_list_refl2[OF e])
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1454
next
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1455
assume a: "(list_rel R OOO op \<approx>) r s"
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1456
then have b: "map Abs r \<approx> map Abs s"
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1457
proof (elim pred_compE)
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1458
fix b ba
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1459
assume c: "list_rel R r b"
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1460
assume d: "b \<approx> ba"
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1461
assume e: "list_rel R ba s"
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1462
have f: "map Abs r = map Abs b"
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1463
using Quotient_rel[OF list_quotient[OF q]] c by blast
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1464
have "map Abs ba = map Abs s"
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1465
using Quotient_rel[OF list_quotient[OF q]] e by blast
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1466
then have g: "map Abs s = map Abs ba" by simp
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1467
then show "map Abs r \<approx> map Abs s" using d f map_rel_cong by simp
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1468
qed
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1469
then show "abs_fset (map Abs r) = abs_fset (map Abs s)"
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1470
using Quotient_rel[OF Quotient_fset] by blast
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1471
next
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1472
assume a: "(list_rel R OOO op \<approx>) r r \<and> (list_rel R OOO op \<approx>) s s
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1473
\<and> abs_fset (map Abs r) = abs_fset (map Abs s)"
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1474
then have s: "(list_rel R OOO op \<approx>) s s" by simp
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1475
have d: "map Abs r \<approx> map Abs s"
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1476
by (subst Quotient_rel[OF Quotient_fset]) (simp add: a)
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1477
have b: "map Rep (map Abs r) \<approx> map Rep (map Abs s)"
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1478
by (rule map_rel_cong[OF d])
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1479
have y: "list_rel R (map Rep (map Abs s)) s"
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1480
by (fact rep_abs_rsp_left[OF list_quotient[OF q], OF list_rel_refl[OF e, of s]])
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1481
have c: "(op \<approx> OO list_rel R) (map Rep (map Abs r)) s"
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1482
by (rule pred_compI) (rule b, rule y)
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1483
have z: "list_rel R r (map Rep (map Abs r))"
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1484
by (fact rep_abs_rsp[OF list_quotient[OF q], OF list_rel_refl[OF e, of r]])
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1485
then show "(list_rel R OOO op \<approx>) r s"
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1486
using a c pred_compI by simp
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1487
qed
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1488
qed
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1489
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1490
no_notation
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1491
list_eq (infix "\<approx>" 50)
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1492
dcffc2f132c9
Qpaper / Clarify the typing system and composition of quotients issue.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1493
2234
+ − 1494
end