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
1938
+ − 83
lemma list_rel_refl:
+ − 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])
+ − 91
show "list_rel op \<approx> r r" by (rule list_rel_refl)
+ − 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
+ − 106
lemma quotient_compose_list[quot_thm]:
+ − 107
shows "Quotient ((list_rel op \<approx>) OOO (op \<approx>))
+ − 108
(abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"
+ − 109
unfolding Quotient_def comp_def
+ − 110
proof (intro conjI allI)
+ − 111
fix a r s
+ − 112
show "abs_fset (map abs_fset (map rep_fset (rep_fset a))) = a"
+ − 113
by (simp add: abs_o_rep[OF Quotient_fset] Quotient_abs_rep[OF Quotient_fset] map_id)
+ − 114
have b: "list_rel op \<approx> (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
+ − 115
by (rule list_rel_refl)
+ − 116
have c: "(op \<approx> OO list_rel op \<approx>) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
+ − 117
by (rule, rule equivp_reflp[OF fset_equivp]) (rule b)
+ − 118
show "(list_rel op \<approx> OOO op \<approx>) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
+ − 119
by (rule, rule list_rel_refl) (rule c)
+ − 120
show "(list_rel op \<approx> OOO op \<approx>) r s = ((list_rel op \<approx> OOO op \<approx>) r r \<and>
+ − 121
(list_rel op \<approx> OOO op \<approx>) s s \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s))"
+ − 122
proof (intro iffI conjI)
+ − 123
show "(list_rel op \<approx> OOO op \<approx>) r r" by (rule compose_list_refl)
+ − 124
show "(list_rel op \<approx> OOO op \<approx>) s s" by (rule compose_list_refl)
+ − 125
next
+ − 126
assume a: "(list_rel op \<approx> OOO op \<approx>) r s"
2084
+ − 127
then have b: "map abs_fset r \<approx> map abs_fset s"
+ − 128
proof (elim pred_compE)
1935
+ − 129
fix b ba
+ − 130
assume c: "list_rel op \<approx> r b"
+ − 131
assume d: "b \<approx> ba"
+ − 132
assume e: "list_rel op \<approx> ba s"
+ − 133
have f: "map abs_fset r = map abs_fset b"
1938
+ − 134
using Quotient_rel[OF Quotient_fset_list] c by blast
+ − 135
have "map abs_fset ba = map abs_fset s"
+ − 136
using Quotient_rel[OF Quotient_fset_list] e by blast
+ − 137
then have g: "map abs_fset s = map abs_fset ba" by simp
+ − 138
then show "map abs_fset r \<approx> map abs_fset s" using d f map_rel_cong by simp
1935
+ − 139
qed
+ − 140
then show "abs_fset (map abs_fset r) = abs_fset (map abs_fset s)"
1938
+ − 141
using Quotient_rel[OF Quotient_fset] by blast
1935
+ − 142
next
+ − 143
assume a: "(list_rel op \<approx> OOO op \<approx>) r r \<and> (list_rel op \<approx> OOO op \<approx>) s s
+ − 144
\<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s)"
+ − 145
then have s: "(list_rel op \<approx> OOO op \<approx>) s s" by simp
+ − 146
have d: "map abs_fset r \<approx> map abs_fset s"
+ − 147
by (subst Quotient_rel[OF Quotient_fset]) (simp add: a)
+ − 148
have b: "map rep_fset (map abs_fset r) \<approx> map rep_fset (map abs_fset s)"
+ − 149
by (rule map_rel_cong[OF d])
+ − 150
have y: "list_rel op \<approx> (map rep_fset (map abs_fset s)) s"
+ − 151
by (fact rep_abs_rsp_left[OF Quotient_fset_list, OF list_rel_refl[of s]])
+ − 152
have c: "(op \<approx> OO list_rel op \<approx>) (map rep_fset (map abs_fset r)) s"
+ − 153
by (rule pred_compI) (rule b, rule y)
+ − 154
have z: "list_rel op \<approx> r (map rep_fset (map abs_fset r))"
+ − 155
by (fact rep_abs_rsp[OF Quotient_fset_list, OF list_rel_refl[of r]])
+ − 156
then show "(list_rel op \<approx> OOO op \<approx>) r s"
+ − 157
using a c pred_compI by simp
+ − 158
qed
+ − 159
qed
+ − 160
1909
+ − 161
text {* Respectfullness *}
1893
+ − 162
2187
+ − 163
lemma append_rsp[quot_respect]:
1895
+ − 164
shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
+ − 165
by auto
+ − 166
2190
+ − 167
lemma append_rsp_unfolded:
+ − 168
"\<lbrakk>x \<approx> y; v \<approx> w\<rbrakk> \<Longrightarrow> x @ v \<approx> y @ w"
+ − 169
by auto
+ − 170
1909
+ − 171
lemma [quot_respect]:
+ − 172
shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list"
+ − 173
by (auto simp add: sub_list_def)
+ − 174
+ − 175
lemma memb_rsp[quot_respect]:
+ − 176
shows "(op = ===> op \<approx> ===> op =) memb memb"
+ − 177
by (auto simp add: memb_def)
+ − 178
+ − 179
lemma nil_rsp[quot_respect]:
+ − 180
shows "[] \<approx> []"
+ − 181
by simp
+ − 182
+ − 183
lemma cons_rsp[quot_respect]:
+ − 184
shows "(op = ===> op \<approx> ===> op \<approx>) op # op #"
+ − 185
by simp
+ − 186
+ − 187
lemma map_rsp[quot_respect]:
+ − 188
shows "(op = ===> op \<approx> ===> op \<approx>) map map"
+ − 189
by auto
+ − 190
+ − 191
lemma set_rsp[quot_respect]:
+ − 192
"(op \<approx> ===> op =) set set"
+ − 193
by auto
+ − 194
+ − 195
lemma list_equiv_rsp[quot_respect]:
+ − 196
shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
+ − 197
by auto
+ − 198
+ − 199
lemma not_memb_nil:
+ − 200
shows "\<not> memb x []"
+ − 201
by (simp add: memb_def)
+ − 202
+ − 203
lemma memb_cons_iff:
+ − 204
shows "memb x (y # xs) = (x = y \<or> memb x xs)"
+ − 205
by (induct xs) (auto simp add: memb_def)
+ − 206
+ − 207
lemma memb_finter_raw:
+ − 208
"memb x (finter_raw xs ys) \<longleftrightarrow> memb x xs \<and> memb x ys"
+ − 209
by (induct xs) (auto simp add: not_memb_nil memb_cons_iff)
+ − 210
+ − 211
lemma [quot_respect]:
+ − 212
"(op \<approx> ===> op \<approx> ===> op \<approx>) finter_raw finter_raw"
+ − 213
by (simp add: memb_def[symmetric] memb_finter_raw)
+ − 214
+ − 215
lemma memb_delete_raw:
+ − 216
"memb x (delete_raw xs y) = (memb x xs \<and> x \<noteq> y)"
+ − 217
by (induct xs arbitrary: x y) (auto simp add: memb_def)
+ − 218
+ − 219
lemma [quot_respect]:
+ − 220
"(op \<approx> ===> op = ===> op \<approx>) delete_raw delete_raw"
+ − 221
by (simp add: memb_def[symmetric] memb_delete_raw)
+ − 222
2084
+ − 223
lemma fminus_raw_memb: "memb x (fminus_raw xs ys) = (memb x xs \<and> \<not> memb x ys)"
+ − 224
by (induct ys arbitrary: xs)
+ − 225
(simp_all add: not_memb_nil memb_delete_raw memb_cons_iff)
+ − 226
+ − 227
lemma [quot_respect]:
+ − 228
"(op \<approx> ===> op \<approx> ===> op \<approx>) fminus_raw fminus_raw"
+ − 229
by (simp add: memb_def[symmetric] fminus_raw_memb)
+ − 230
1909
+ − 231
lemma fcard_raw_gt_0:
+ − 232
assumes a: "x \<in> set xs"
+ − 233
shows "0 < fcard_raw xs"
+ − 234
using a by (induct xs) (auto simp add: memb_def)
+ − 235
+ − 236
lemma fcard_raw_delete_one:
+ − 237
shows "fcard_raw ([x \<leftarrow> xs. x \<noteq> y]) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"
+ − 238
by (induct xs) (auto dest: fcard_raw_gt_0 simp add: memb_def)
+ − 239
+ − 240
lemma fcard_raw_rsp_aux:
+ − 241
assumes a: "xs \<approx> ys"
+ − 242
shows "fcard_raw xs = fcard_raw ys"
+ − 243
using a
2084
+ − 244
proof (induct xs arbitrary: ys)
+ − 245
case Nil
+ − 246
show ?case using Nil.prems by simp
+ − 247
next
+ − 248
case (Cons a xs)
+ − 249
have a: "a # xs \<approx> ys" by fact
+ − 250
have b: "\<And>ys. xs \<approx> ys \<Longrightarrow> fcard_raw xs = fcard_raw ys" by fact
+ − 251
show ?case proof (cases "a \<in> set xs")
+ − 252
assume c: "a \<in> set xs"
+ − 253
have "\<forall>x. (x \<in> set xs) = (x \<in> set ys)"
+ − 254
proof (intro allI iffI)
+ − 255
fix x
+ − 256
assume "x \<in> set xs"
+ − 257
then show "x \<in> set ys" using a by auto
+ − 258
next
+ − 259
fix x
+ − 260
assume d: "x \<in> set ys"
+ − 261
have e: "(x \<in> set (a # xs)) = (x \<in> set ys)" using a by simp
+ − 262
show "x \<in> set xs" using c d e unfolding list_eq.simps by simp blast
+ − 263
qed
+ − 264
then show ?thesis using b c by (simp add: memb_def)
+ − 265
next
+ − 266
assume c: "a \<notin> set xs"
+ − 267
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
+ − 268
have "Suc (fcard_raw xs) = fcard_raw ys"
+ − 269
proof (cases "a \<in> set ys")
+ − 270
assume e: "a \<in> set ys"
+ − 271
have f: "\<forall>x. (x \<in> set xs) = (x \<in> set ys \<and> x \<noteq> a)" using a c
+ − 272
by (auto simp add: fcard_raw_delete_one)
+ − 273
have "fcard_raw ys = Suc (fcard_raw ys - 1)" by (rule Suc_pred'[OF fcard_raw_gt_0]) (rule e)
+ − 274
then show ?thesis using d e f by (simp_all add: fcard_raw_delete_one memb_def)
+ − 275
next
+ − 276
case False then show ?thesis using a c d by auto
+ − 277
qed
+ − 278
then show ?thesis using a c d by (simp add: memb_def)
+ − 279
qed
+ − 280
qed
1909
+ − 281
+ − 282
lemma fcard_raw_rsp[quot_respect]:
+ − 283
shows "(op \<approx> ===> op =) fcard_raw fcard_raw"
+ − 284
by (simp add: fcard_raw_rsp_aux)
+ − 285
+ − 286
lemma memb_absorb:
+ − 287
shows "memb x xs \<Longrightarrow> x # xs \<approx> xs"
+ − 288
by (induct xs) (auto simp add: memb_def)
+ − 289
+ − 290
lemma none_memb_nil:
+ − 291
"(\<forall>x. \<not> memb x xs) = (xs \<approx> [])"
+ − 292
by (simp add: memb_def)
+ − 293
+ − 294
lemma not_memb_delete_raw_ident:
+ − 295
shows "\<not> memb x xs \<Longrightarrow> delete_raw xs x = xs"
+ − 296
by (induct xs) (auto simp add: memb_def)
+ − 297
+ − 298
lemma memb_commute_ffold_raw:
+ − 299
"rsp_fold f \<Longrightarrow> memb h b \<Longrightarrow> ffold_raw f z b = f h (ffold_raw f z (delete_raw b h))"
+ − 300
apply (induct b)
+ − 301
apply (simp_all add: not_memb_nil)
+ − 302
apply (auto)
1938
+ − 303
apply (simp_all add: memb_delete_raw not_memb_delete_raw_ident rsp_fold_def memb_cons_iff)
1909
+ − 304
done
+ − 305
+ − 306
lemma ffold_raw_rsp_pre:
+ − 307
"\<forall>e. memb e a = memb e b \<Longrightarrow> ffold_raw f z a = ffold_raw f z b"
+ − 308
apply (induct a arbitrary: b)
+ − 309
apply (simp add: memb_absorb memb_def none_memb_nil)
+ − 310
apply (simp)
+ − 311
apply (rule conjI)
+ − 312
apply (rule_tac [!] impI)
+ − 313
apply (rule_tac [!] conjI)
+ − 314
apply (rule_tac [!] impI)
+ − 315
apply (subgoal_tac "\<forall>e. memb e a2 = memb e b")
+ − 316
apply (simp)
+ − 317
apply (simp add: memb_cons_iff memb_def)
+ − 318
apply (auto)[1]
+ − 319
apply (drule_tac x="e" in spec)
+ − 320
apply (blast)
+ − 321
apply (case_tac b)
+ − 322
apply (simp_all)
+ − 323
apply (subgoal_tac "ffold_raw f z b = f a1 (ffold_raw f z (delete_raw b a1))")
+ − 324
apply (simp only:)
+ − 325
apply (rule_tac f="f a1" in arg_cong)
+ − 326
apply (subgoal_tac "\<forall>e. memb e a2 = memb e (delete_raw b a1)")
+ − 327
apply (simp)
+ − 328
apply (simp add: memb_delete_raw)
+ − 329
apply (auto simp add: memb_cons_iff)[1]
+ − 330
apply (erule memb_commute_ffold_raw)
+ − 331
apply (drule_tac x="a1" in spec)
+ − 332
apply (simp add: memb_cons_iff)
+ − 333
apply (simp add: memb_cons_iff)
+ − 334
apply (case_tac b)
+ − 335
apply (simp_all)
+ − 336
done
+ − 337
+ − 338
lemma [quot_respect]:
+ − 339
"(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw"
+ − 340
by (simp add: memb_def[symmetric] ffold_raw_rsp_pre)
+ − 341
1935
+ − 342
lemma concat_rsp_pre:
+ − 343
assumes a: "list_rel op \<approx> x x'"
+ − 344
and b: "x' \<approx> y'"
+ − 345
and c: "list_rel op \<approx> y' y"
+ − 346
and d: "\<exists>x\<in>set x. xa \<in> set x"
+ − 347
shows "\<exists>x\<in>set y. xa \<in> set x"
+ − 348
proof -
+ − 349
obtain xb where e: "xb \<in> set x" and f: "xa \<in> set xb" using d by auto
+ − 350
have "\<exists>y. y \<in> set x' \<and> xb \<approx> y" by (rule list_rel_find_element[OF e a])
+ − 351
then obtain ya where h: "ya \<in> set x'" and i: "xb \<approx> ya" by auto
2084
+ − 352
have "ya \<in> set y'" using b h by simp
+ − 353
then have "\<exists>yb. yb \<in> set y \<and> ya \<approx> yb" using c by (rule list_rel_find_element)
1935
+ − 354
then show ?thesis using f i by auto
+ − 355
qed
+ − 356
2187
+ − 357
lemma concat_rsp[quot_respect]:
1935
+ − 358
shows "(list_rel op \<approx> OOO op \<approx> ===> op \<approx>) concat concat"
+ − 359
proof (rule fun_relI, elim pred_compE)
+ − 360
fix a b ba bb
+ − 361
assume a: "list_rel op \<approx> a ba"
+ − 362
assume b: "ba \<approx> bb"
+ − 363
assume c: "list_rel op \<approx> bb b"
+ − 364
have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof
+ − 365
fix x
+ − 366
show "(\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof
+ − 367
assume d: "\<exists>xa\<in>set a. x \<in> set xa"
+ − 368
show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d])
+ − 369
next
+ − 370
assume e: "\<exists>xa\<in>set b. x \<in> set xa"
+ − 371
have a': "list_rel op \<approx> ba a" by (rule list_rel_symp[OF list_eq_equivp, OF a])
+ − 372
have b': "bb \<approx> ba" by (rule equivp_symp[OF list_eq_equivp, OF b])
+ − 373
have c': "list_rel op \<approx> b bb" by (rule list_rel_symp[OF list_eq_equivp, OF c])
+ − 374
show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e])
+ − 375
qed
+ − 376
qed
+ − 377
then show "concat a \<approx> concat b" by simp
+ − 378
qed
+ − 379
2190
+ − 380
+ − 381
+ − 382
lemma concat_rsp_unfolded:
+ − 383
"\<lbrakk>list_rel op \<approx> a ba; ba \<approx> bb; list_rel op \<approx> bb b\<rbrakk> \<Longrightarrow> concat a \<approx> concat b"
+ − 384
proof -
+ − 385
fix a b ba bb
+ − 386
assume a: "list_rel op \<approx> a ba"
+ − 387
assume b: "ba \<approx> bb"
+ − 388
assume c: "list_rel op \<approx> bb b"
+ − 389
have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof
+ − 390
fix x
+ − 391
show "(\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof
+ − 392
assume d: "\<exists>xa\<in>set a. x \<in> set xa"
+ − 393
show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d])
+ − 394
next
+ − 395
assume e: "\<exists>xa\<in>set b. x \<in> set xa"
+ − 396
have a': "list_rel op \<approx> ba a" by (rule list_rel_symp[OF list_eq_equivp, OF a])
+ − 397
have b': "bb \<approx> ba" by (rule equivp_symp[OF list_eq_equivp, OF b])
+ − 398
have c': "list_rel op \<approx> b bb" by (rule list_rel_symp[OF list_eq_equivp, OF c])
+ − 399
show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e])
+ − 400
qed
+ − 401
qed
+ − 402
then show "concat a \<approx> concat b" by simp
+ − 403
qed
+ − 404
2084
+ − 405
lemma [quot_respect]:
+ − 406
"((op =) ===> op \<approx> ===> op \<approx>) filter filter"
+ − 407
by auto
+ − 408
1909
+ − 409
text {* Distributive lattice with bot *}
+ − 410
1893
+ − 411
lemma sub_list_not_eq:
+ − 412
"(sub_list x y \<and> \<not> list_eq x y) = (sub_list x y \<and> \<not> sub_list y x)"
+ − 413
by (auto simp add: sub_list_def)
+ − 414
+ − 415
lemma sub_list_refl:
+ − 416
"sub_list x x"
+ − 417
by (simp add: sub_list_def)
+ − 418
+ − 419
lemma sub_list_trans:
+ − 420
"sub_list x y \<Longrightarrow> sub_list y z \<Longrightarrow> sub_list x z"
+ − 421
by (simp add: sub_list_def)
+ − 422
+ − 423
lemma sub_list_empty:
+ − 424
"sub_list [] x"
+ − 425
by (simp add: sub_list_def)
+ − 426
1905
+ − 427
lemma sub_list_append_left:
+ − 428
"sub_list x (x @ y)"
+ − 429
by (simp add: sub_list_def)
+ − 430
+ − 431
lemma sub_list_append_right:
+ − 432
"sub_list y (x @ y)"
+ − 433
by (simp add: sub_list_def)
+ − 434
+ − 435
lemma sub_list_inter_left:
+ − 436
shows "sub_list (finter_raw x y) x"
+ − 437
by (simp add: sub_list_def memb_def[symmetric] memb_finter_raw)
+ − 438
+ − 439
lemma sub_list_inter_right:
+ − 440
shows "sub_list (finter_raw x y) y"
+ − 441
by (simp add: sub_list_def memb_def[symmetric] memb_finter_raw)
+ − 442
+ − 443
lemma sub_list_list_eq:
+ − 444
"sub_list x y \<Longrightarrow> sub_list y x \<Longrightarrow> list_eq x y"
+ − 445
unfolding sub_list_def list_eq.simps by blast
+ − 446
+ − 447
lemma sub_list_append:
+ − 448
"sub_list y x \<Longrightarrow> sub_list z x \<Longrightarrow> sub_list (y @ z) x"
+ − 449
unfolding sub_list_def by auto
+ − 450
+ − 451
lemma sub_list_inter:
+ − 452
"sub_list x y \<Longrightarrow> sub_list x z \<Longrightarrow> sub_list x (finter_raw y z)"
+ − 453
by (simp add: sub_list_def memb_def[symmetric] memb_finter_raw)
+ − 454
+ − 455
lemma append_inter_distrib:
+ − 456
"x @ (finter_raw y z) \<approx> finter_raw (x @ y) (x @ z)"
+ − 457
apply (induct x)
+ − 458
apply (simp_all add: memb_def)
+ − 459
apply (simp add: memb_def[symmetric] memb_finter_raw)
2084
+ − 460
apply (auto simp add: memb_def)
+ − 461
done
1905
+ − 462
2084
+ − 463
instantiation fset :: (type) "{bounded_lattice_bot,distrib_lattice,minus}"
1893
+ − 464
begin
+ − 465
+ − 466
quotient_definition
+ − 467
"bot :: 'a fset" is "[] :: 'a list"
+ − 468
+ − 469
abbreviation
+ − 470
fempty ("{||}")
+ − 471
where
+ − 472
"{||} \<equiv> bot :: 'a fset"
+ − 473
+ − 474
quotient_definition
+ − 475
"less_eq_fset \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> bool)"
+ − 476
is
+ − 477
"sub_list \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> bool)"
+ − 478
+ − 479
abbreviation
+ − 480
f_subset_eq :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subseteq>|" 50)
+ − 481
where
+ − 482
"xs |\<subseteq>| ys \<equiv> xs \<le> ys"
+ − 483
+ − 484
definition
+ − 485
less_fset:
+ − 486
"(xs :: 'a fset) < ys \<equiv> xs \<le> ys \<and> xs \<noteq> ys"
+ − 487
+ − 488
abbreviation
+ − 489
f_subset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subset>|" 50)
+ − 490
where
+ − 491
"xs |\<subset>| ys \<equiv> xs < ys"
+ − 492
1895
+ − 493
quotient_definition
+ − 494
"sup \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset)"
+ − 495
is
+ − 496
"(op @) \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> 'a list)"
+ − 497
+ − 498
abbreviation
2084
+ − 499
funion (infixl "|\<union>|" 65)
1895
+ − 500
where
+ − 501
"xs |\<union>| ys \<equiv> sup (xs :: 'a fset) ys"
+ − 502
1905
+ − 503
quotient_definition
2084
+ − 504
"inf \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset)"
1905
+ − 505
is
+ − 506
"finter_raw \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> 'a list)"
+ − 507
+ − 508
abbreviation
+ − 509
finter (infixl "|\<inter>|" 65)
+ − 510
where
+ − 511
"xs |\<inter>| ys \<equiv> inf (xs :: 'a fset) ys"
+ − 512
2084
+ − 513
quotient_definition
+ − 514
"minus \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset)"
+ − 515
is
+ − 516
"fminus_raw \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> 'a list)"
+ − 517
1895
+ − 518
instance
+ − 519
proof
1905
+ − 520
fix x y z :: "'a fset"
+ − 521
show "(x |\<subset>| y) = (x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x)"
+ − 522
unfolding less_fset by (lifting sub_list_not_eq)
+ − 523
show "x |\<subseteq>| x" by (lifting sub_list_refl)
+ − 524
show "{||} |\<subseteq>| x" by (lifting sub_list_empty)
1895
+ − 525
show "x |\<subseteq>| x |\<union>| y" by (lifting sub_list_append_left)
+ − 526
show "y |\<subseteq>| x |\<union>| y" by (lifting sub_list_append_right)
1905
+ − 527
show "x |\<inter>| y |\<subseteq>| x" by (lifting sub_list_inter_left)
+ − 528
show "x |\<inter>| y |\<subseteq>| y" by (lifting sub_list_inter_right)
+ − 529
show "x |\<union>| (y |\<inter>| z) = x |\<union>| y |\<inter>| (x |\<union>| z)" by (lifting append_inter_distrib)
+ − 530
next
+ − 531
fix x y z :: "'a fset"
+ − 532
assume a: "x |\<subseteq>| y"
+ − 533
assume b: "y |\<subseteq>| z"
+ − 534
show "x |\<subseteq>| z" using a b by (lifting sub_list_trans)
1895
+ − 535
next
+ − 536
fix x y :: "'a fset"
+ − 537
assume a: "x |\<subseteq>| y"
+ − 538
assume b: "y |\<subseteq>| x"
+ − 539
show "x = y" using a b by (lifting sub_list_list_eq)
+ − 540
next
+ − 541
fix x y z :: "'a fset"
+ − 542
assume a: "y |\<subseteq>| x"
+ − 543
assume b: "z |\<subseteq>| x"
+ − 544
show "y |\<union>| z |\<subseteq>| x" using a b by (lifting sub_list_append)
1905
+ − 545
next
+ − 546
fix x y z :: "'a fset"
+ − 547
assume a: "x |\<subseteq>| y"
+ − 548
assume b: "x |\<subseteq>| z"
+ − 549
show "x |\<subseteq>| y |\<inter>| z" using a b by (lifting sub_list_inter)
1895
+ − 550
qed
1905
+ − 551
1893
+ − 552
end
+ − 553
1909
+ − 554
section {* Finsert and Membership *}
1518
+ − 555
+ − 556
quotient_definition
1893
+ − 557
"finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
1518
+ − 558
is "op #"
+ − 559
+ − 560
syntax
+ − 561
"@Finset" :: "args => 'a fset" ("{|(_)|}")
+ − 562
+ − 563
translations
+ − 564
"{|x, xs|}" == "CONST finsert x {|xs|}"
+ − 565
"{|x|}" == "CONST finsert x {||}"
+ − 566
+ − 567
quotient_definition
1938
+ − 568
fin (infix "|\<in>|" 50)
1518
+ − 569
where
1816
+ − 570
"fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" is "memb"
1518
+ − 571
+ − 572
abbreviation
1938
+ − 573
fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50)
1518
+ − 574
where
1860
+ − 575
"x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
1518
+ − 576
2084
+ − 577
section {* Other constants on the Quotient Type *}
1935
+ − 578
+ − 579
quotient_definition
2084
+ − 580
"fcard :: 'a fset \<Rightarrow> nat"
1935
+ − 581
is
+ − 582
"fcard_raw"
+ − 583
+ − 584
quotient_definition
+ − 585
"fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
+ − 586
is
+ − 587
"map"
+ − 588
+ − 589
quotient_definition
2084
+ − 590
"fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset"
1935
+ − 591
is "delete_raw"
+ − 592
+ − 593
quotient_definition
2084
+ − 594
"fset_to_set :: 'a fset \<Rightarrow> 'a set"
1935
+ − 595
is "set"
+ − 596
+ − 597
quotient_definition
+ − 598
"ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b"
+ − 599
is "ffold_raw"
+ − 600
+ − 601
quotient_definition
+ − 602
"fconcat :: ('a fset) fset \<Rightarrow> 'a fset"
+ − 603
is
+ − 604
"concat"
+ − 605
2222
+ − 606
thm fconcat_def
+ − 607
2084
+ − 608
quotient_definition
+ − 609
"ffilter :: ('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+ − 610
is
+ − 611
"filter"
+ − 612
1935
+ − 613
text {* Compositional Respectfullness and Preservation *}
+ − 614
+ − 615
lemma [quot_respect]: "(list_rel op \<approx> OOO op \<approx>) [] []"
1938
+ − 616
by (fact compose_list_refl)
1935
+ − 617
+ − 618
lemma [quot_preserve]: "(abs_fset \<circ> map f) [] = abs_fset []"
+ − 619
by simp
+ − 620
+ − 621
lemma [quot_respect]:
+ − 622
"(op \<approx> ===> list_rel op \<approx> OOO op \<approx> ===> list_rel op \<approx> OOO op \<approx>) op # op #"
+ − 623
apply auto
+ − 624
apply (simp add: set_in_eq)
+ − 625
apply (rule_tac b="x # b" in pred_compI)
+ − 626
apply auto
+ − 627
apply (rule_tac b="x # ba" in pred_compI)
+ − 628
apply auto
+ − 629
done
+ − 630
2196
+ − 631
lemma insert_preserve2:
+ − 632
shows "((rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op #) =
+ − 633
(id ---> rep_fset ---> abs_fset) op #"
+ − 634
by (simp add: expand_fun_eq abs_o_rep[OF Quotient_fset] map_id Quotient_abs_rep[OF Quotient_fset])
+ − 635
1935
+ − 636
lemma [quot_preserve]:
+ − 637
"(rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op # = finsert"
+ − 638
by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset]
+ − 639
abs_o_rep[OF Quotient_fset] map_id finsert_def)
+ − 640
+ − 641
lemma [quot_preserve]:
1938
+ − 642
"((map rep_fset \<circ> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op @ = funion"
1935
+ − 643
by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset]
+ − 644
abs_o_rep[OF Quotient_fset] map_id sup_fset_def)
+ − 645
+ − 646
lemma list_rel_app_l:
+ − 647
assumes a: "reflp R"
+ − 648
and b: "list_rel R l r"
+ − 649
shows "list_rel R (z @ l) (z @ r)"
1938
+ − 650
by (induct z) (simp_all add: b rev_iffD1[OF a meta_eq_to_obj_eq[OF reflp_def]])
1935
+ − 651
+ − 652
lemma append_rsp2_pre0:
+ − 653
assumes a:"list_rel op \<approx> x x'"
+ − 654
shows "list_rel op \<approx> (x @ z) (x' @ z)"
+ − 655
using a apply (induct x x' rule: list_induct2')
1938
+ − 656
by simp_all (rule list_rel_refl)
1935
+ − 657
+ − 658
lemma append_rsp2_pre1:
+ − 659
assumes a:"list_rel op \<approx> x x'"
+ − 660
shows "list_rel op \<approx> (z @ x) (z @ x')"
+ − 661
using a apply (induct x x' arbitrary: z rule: list_induct2')
+ − 662
apply (rule list_rel_refl)
+ − 663
apply (simp_all del: list_eq.simps)
+ − 664
apply (rule list_rel_app_l)
+ − 665
apply (simp_all add: reflp_def)
+ − 666
done
+ − 667
+ − 668
lemma append_rsp2_pre:
+ − 669
assumes a:"list_rel op \<approx> x x'"
+ − 670
and b: "list_rel op \<approx> z z'"
+ − 671
shows "list_rel op \<approx> (x @ z) (x' @ z')"
+ − 672
apply (rule list_rel_transp[OF fset_equivp])
+ − 673
apply (rule append_rsp2_pre0)
+ − 674
apply (rule a)
+ − 675
using b apply (induct z z' rule: list_induct2')
+ − 676
apply (simp_all only: append_Nil2)
+ − 677
apply (rule list_rel_refl)
+ − 678
apply simp_all
+ − 679
apply (rule append_rsp2_pre1)
+ − 680
apply simp
+ − 681
done
+ − 682
+ − 683
lemma [quot_respect]:
+ − 684
"(list_rel op \<approx> OOO op \<approx> ===> list_rel op \<approx> OOO op \<approx> ===> list_rel op \<approx> OOO op \<approx>) op @ op @"
+ − 685
proof (intro fun_relI, elim pred_compE)
+ − 686
fix x y z w x' z' y' w' :: "'a list list"
+ − 687
assume a:"list_rel op \<approx> x x'"
+ − 688
and b: "x' \<approx> y'"
+ − 689
and c: "list_rel op \<approx> y' y"
+ − 690
assume aa: "list_rel op \<approx> z z'"
+ − 691
and bb: "z' \<approx> w'"
+ − 692
and cc: "list_rel op \<approx> w' w"
+ − 693
have a': "list_rel op \<approx> (x @ z) (x' @ z')" using a aa append_rsp2_pre by auto
+ − 694
have b': "x' @ z' \<approx> y' @ w'" using b bb by simp
+ − 695
have c': "list_rel op \<approx> (y' @ w') (y @ w)" using c cc append_rsp2_pre by auto
+ − 696
have d': "(op \<approx> OO list_rel op \<approx>) (x' @ z') (y @ w)"
+ − 697
by (rule pred_compI) (rule b', rule c')
+ − 698
show "(list_rel op \<approx> OOO op \<approx>) (x @ z) (y @ w)"
+ − 699
by (rule pred_compI) (rule a', rule d')
+ − 700
qed
+ − 701
+ − 702
text {* Raw theorems. Finsert, memb, singleron, sub_list *}
1518
+ − 703
1892
+ − 704
lemma nil_not_cons:
+ − 705
shows "\<not> ([] \<approx> x # xs)"
+ − 706
and "\<not> (x # xs \<approx> [])"
+ − 707
by auto
+ − 708
1878
+ − 709
lemma no_memb_nil:
+ − 710
"(\<forall>x. \<not> memb x xs) = (xs = [])"
+ − 711
by (simp add: memb_def)
+ − 712
1518
+ − 713
lemma memb_consI1:
+ − 714
shows "memb x (x # xs)"
+ − 715
by (simp add: memb_def)
+ − 716
+ − 717
lemma memb_consI2:
+ − 718
shows "memb x xs \<Longrightarrow> memb x (y # xs)"
+ − 719
by (simp add: memb_def)
+ − 720
+ − 721
lemma singleton_list_eq:
+ − 722
shows "[x] \<approx> [y] \<longleftrightarrow> x = y"
+ − 723
by (simp add: id_simps) auto
+ − 724
1892
+ − 725
lemma sub_list_cons:
+ − 726
"sub_list (x # xs) ys = (memb x ys \<and> sub_list xs ys)"
+ − 727
by (auto simp add: memb_def sub_list_def)
+ − 728
2084
+ − 729
lemma fminus_raw_red: "fminus_raw (x # xs) ys = (if memb x ys then fminus_raw xs ys else x # (fminus_raw xs ys))"
+ − 730
by (induct ys arbitrary: xs x)
+ − 731
(simp_all add: not_memb_nil memb_delete_raw memb_cons_iff)
+ − 732
1935
+ − 733
text {* Cardinality of finite sets *}
1518
+ − 734
1813
+ − 735
lemma fcard_raw_0:
1860
+ − 736
shows "fcard_raw xs = 0 \<longleftrightarrow> xs \<approx> []"
1821
+ − 737
by (induct xs) (auto simp add: memb_def)
1813
+ − 738
+ − 739
lemma fcard_raw_not_memb:
1860
+ − 740
shows "\<not> memb x xs \<longleftrightarrow> fcard_raw (x # xs) = Suc (fcard_raw xs)"
1813
+ − 741
by auto
+ − 742
+ − 743
lemma fcard_raw_suc:
1860
+ − 744
assumes a: "fcard_raw xs = Suc n"
+ − 745
shows "\<exists>x ys. \<not> (memb x ys) \<and> xs \<approx> (x # ys) \<and> fcard_raw ys = n"
+ − 746
using a
+ − 747
by (induct xs) (auto simp add: memb_def split: if_splits)
1819
+ − 748
1935
+ − 749
lemma singleton_fcard_1:
1860
+ − 750
shows "set xs = {x} \<Longrightarrow> fcard_raw xs = 1"
+ − 751
by (induct xs) (auto simp add: memb_def subset_insert)
1819
+ − 752
+ − 753
lemma fcard_raw_1:
1823
+ − 754
shows "fcard_raw xs = 1 \<longleftrightarrow> (\<exists>x. xs \<approx> [x])"
+ − 755
apply (auto dest!: fcard_raw_suc)
1819
+ − 756
apply (simp add: fcard_raw_0)
1821
+ − 757
apply (rule_tac x="x" in exI)
1819
+ − 758
apply simp
1821
+ − 759
apply (subgoal_tac "set xs = {x}")
1860
+ − 760
apply (drule singleton_fcard_1)
1819
+ − 761
apply auto
1813
+ − 762
done
+ − 763
1878
+ − 764
lemma fcard_raw_suc_memb:
+ − 765
assumes a: "fcard_raw A = Suc n"
+ − 766
shows "\<exists>a. memb a A"
+ − 767
using a
1938
+ − 768
by (induct A) (auto simp add: memb_def)
1878
+ − 769
1884
+ − 770
lemma memb_card_not_0:
1878
+ − 771
assumes a: "memb a A"
+ − 772
shows "\<not>(fcard_raw A = 0)"
1883
+ − 773
proof -
+ − 774
have "\<not>(\<forall>x. \<not> memb x A)" using a by auto
+ − 775
then have "\<not>A \<approx> []" using none_memb_nil[of A] by simp
+ − 776
then show ?thesis using fcard_raw_0[of A] by simp
+ − 777
qed
1878
+ − 778
1935
+ − 779
text {* fmap *}
1518
+ − 780
1813
+ − 781
lemma map_append:
1821
+ − 782
"map f (xs @ ys) \<approx> (map f xs) @ (map f ys)"
1813
+ − 783
by simp
+ − 784
1819
+ − 785
lemma memb_append:
1823
+ − 786
"memb x (xs @ ys) \<longleftrightarrow> memb x xs \<or> memb x ys"
1821
+ − 787
by (induct xs) (simp_all add: not_memb_nil memb_cons_iff)
1819
+ − 788
1518
+ − 789
lemma cons_left_comm:
1821
+ − 790
"x # y # xs \<approx> y # x # xs"
+ − 791
by auto
1518
+ − 792
+ − 793
lemma cons_left_idem:
1821
+ − 794
"x # x # xs \<approx> x # xs"
+ − 795
by auto
1518
+ − 796
1819
+ − 797
lemma fset_raw_strong_cases:
2084
+ − 798
obtains "xs = []"
+ − 799
| x ys where "\<not> memb x ys" and "xs \<approx> x # ys"
+ − 800
proof (induct xs arbitrary: x ys)
+ − 801
case Nil
+ − 802
then show thesis by simp
+ − 803
next
+ − 804
case (Cons a xs)
+ − 805
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
+ − 806
have b: "\<And>x' ys'. \<lbrakk>\<not> memb x' ys'; a # xs \<approx> x' # ys'\<rbrakk> \<Longrightarrow> thesis" by fact
+ − 807
have c: "xs = [] \<Longrightarrow> thesis" by (metis no_memb_nil singleton_list_eq b)
+ − 808
have "\<And>x ys. \<lbrakk>\<not> memb x ys; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis"
+ − 809
proof -
+ − 810
fix x :: 'a
+ − 811
fix ys :: "'a list"
+ − 812
assume d:"\<not> memb x ys"
+ − 813
assume e:"xs \<approx> x # ys"
+ − 814
show thesis
+ − 815
proof (cases "x = a")
+ − 816
assume h: "x = a"
+ − 817
then have f: "\<not> memb a ys" using d by simp
+ − 818
have g: "a # xs \<approx> a # ys" using e h by auto
+ − 819
show thesis using b f g by simp
+ − 820
next
+ − 821
assume h: "x \<noteq> a"
+ − 822
then have f: "\<not> memb x (a # ys)" using d unfolding memb_def by auto
+ − 823
have g: "a # xs \<approx> x # (a # ys)" using e h by auto
+ − 824
show thesis using b f g by simp
+ − 825
qed
+ − 826
qed
+ − 827
then show thesis using a c by blast
+ − 828
qed
1518
+ − 829
1860
+ − 830
section {* deletion *}
+ − 831
1819
+ − 832
lemma memb_delete_raw_ident:
1860
+ − 833
shows "\<not> memb x (delete_raw xs x)"
1821
+ − 834
by (induct xs) (auto simp add: memb_def)
1518
+ − 835
1819
+ − 836
lemma fset_raw_delete_raw_cases:
1821
+ − 837
"xs = [] \<or> (\<exists>x. memb x xs \<and> xs \<approx> x # delete_raw xs x)"
+ − 838
by (induct xs) (auto simp add: memb_def)
1518
+ − 839
1819
+ − 840
lemma fdelete_raw_filter:
+ − 841
"delete_raw xs y = [x \<leftarrow> xs. x \<noteq> y]"
+ − 842
by (induct xs) simp_all
1518
+ − 843
1819
+ − 844
lemma fcard_raw_delete:
+ − 845
"fcard_raw (delete_raw xs y) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"
+ − 846
by (simp add: fdelete_raw_filter fcard_raw_delete_one)
1518
+ − 847
1819
+ − 848
lemma finter_raw_empty:
+ − 849
"finter_raw l [] = []"
+ − 850
by (induct l) (simp_all add: not_memb_nil)
+ − 851
2084
+ − 852
lemma set_cong:
+ − 853
shows "(x \<approx> y) = (set x = set y)"
1821
+ − 854
by auto
1533
+ − 855
+ − 856
lemma inj_map_eq_iff:
+ − 857
"inj f \<Longrightarrow> (map f l \<approx> map f m) = (l \<approx> m)"
+ − 858
by (simp add: expand_set_eq[symmetric] inj_image_eq_iff)
+ − 859
1888
+ − 860
text {* alternate formulation with a different decomposition principle
+ − 861
and a proof of equivalence *}
+ − 862
+ − 863
inductive
+ − 864
list_eq2
+ − 865
where
+ − 866
"list_eq2 (a # b # xs) (b # a # xs)"
+ − 867
| "list_eq2 [] []"
+ − 868
| "list_eq2 xs ys \<Longrightarrow> list_eq2 ys xs"
+ − 869
| "list_eq2 (a # a # xs) (a # xs)"
+ − 870
| "list_eq2 xs ys \<Longrightarrow> list_eq2 (a # xs) (a # ys)"
+ − 871
| "\<lbrakk>list_eq2 xs1 xs2; list_eq2 xs2 xs3\<rbrakk> \<Longrightarrow> list_eq2 xs1 xs3"
+ − 872
+ − 873
lemma list_eq2_refl:
+ − 874
shows "list_eq2 xs xs"
+ − 875
by (induct xs) (auto intro: list_eq2.intros)
+ − 876
+ − 877
lemma cons_delete_list_eq2:
+ − 878
shows "list_eq2 (a # (delete_raw A a)) (if memb a A then A else a # A)"
+ − 879
apply (induct A)
+ − 880
apply (simp add: memb_def list_eq2_refl)
+ − 881
apply (case_tac "memb a (aa # A)")
+ − 882
apply (simp_all only: memb_cons_iff)
+ − 883
apply (case_tac [!] "a = aa")
1909
+ − 884
apply (simp_all)
1888
+ − 885
apply (case_tac "memb a A")
+ − 886
apply (auto simp add: memb_def)[2]
+ − 887
apply (metis list_eq2.intros(3) list_eq2.intros(4) list_eq2.intros(5) list_eq2.intros(6))
1895
+ − 888
apply (metis list_eq2.intros(1) list_eq2.intros(5) list_eq2.intros(6))
1888
+ − 889
apply (auto simp add: list_eq2_refl not_memb_delete_raw_ident)
+ − 890
done
+ − 891
+ − 892
lemma memb_delete_list_eq2:
+ − 893
assumes a: "memb e r"
+ − 894
shows "list_eq2 (e # delete_raw r e) r"
+ − 895
using a cons_delete_list_eq2[of e r]
+ − 896
by simp
+ − 897
1909
+ − 898
lemma delete_raw_rsp:
+ − 899
"xs \<approx> ys \<Longrightarrow> delete_raw xs x \<approx> delete_raw ys x"
+ − 900
by (simp add: memb_def[symmetric] memb_delete_raw)
+ − 901
1888
+ − 902
lemma list_eq2_equiv:
+ − 903
"(l \<approx> r) \<longleftrightarrow> (list_eq2 l r)"
+ − 904
proof
+ − 905
show "list_eq2 l r \<Longrightarrow> l \<approx> r" by (induct rule: list_eq2.induct) auto
1938
+ − 906
next
+ − 907
{
+ − 908
fix n
+ − 909
assume a: "fcard_raw l = n" and b: "l \<approx> r"
+ − 910
have "list_eq2 l r"
+ − 911
using a b
+ − 912
proof (induct n arbitrary: l r)
+ − 913
case 0
+ − 914
have "fcard_raw l = 0" by fact
+ − 915
then have "\<forall>x. \<not> memb x l" using memb_card_not_0[of _ l] by auto
+ − 916
then have z: "l = []" using no_memb_nil by auto
+ − 917
then have "r = []" using `l \<approx> r` by simp
+ − 918
then show ?case using z list_eq2_refl by simp
+ − 919
next
+ − 920
case (Suc m)
+ − 921
have b: "l \<approx> r" by fact
+ − 922
have d: "fcard_raw l = Suc m" by fact
2084
+ − 923
then have "\<exists>a. memb a l" by (rule fcard_raw_suc_memb)
1938
+ − 924
then obtain a where e: "memb a l" by auto
+ − 925
then have e': "memb a r" using list_eq.simps[simplified memb_def[symmetric], of l r] b by auto
+ − 926
have f: "fcard_raw (delete_raw l a) = m" using fcard_raw_delete[of l a] e d by simp
+ − 927
have g: "delete_raw l a \<approx> delete_raw r a" using delete_raw_rsp[OF b] by simp
2084
+ − 928
have "list_eq2 (delete_raw l a) (delete_raw r a)" by (rule Suc.hyps[OF f g])
+ − 929
then have h: "list_eq2 (a # delete_raw l a) (a # delete_raw r a)" by (rule list_eq2.intros(5))
1938
+ − 930
have i: "list_eq2 l (a # delete_raw l a)"
+ − 931
by (rule list_eq2.intros(3)[OF memb_delete_list_eq2[OF e]])
+ − 932
have "list_eq2 l (a # delete_raw r a)" by (rule list_eq2.intros(6)[OF i h])
+ − 933
then show ?case using list_eq2.intros(6)[OF _ memb_delete_list_eq2[OF e']] by simp
+ − 934
qed
+ − 935
}
+ − 936
then show "l \<approx> r \<Longrightarrow> list_eq2 l r" by blast
1888
+ − 937
qed
+ − 938
2084
+ − 939
text {* Set *}
+ − 940
+ − 941
lemma sub_list_set: "sub_list xs ys = (set xs \<subseteq> set ys)"
+ − 942
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)
+ − 943
+ − 944
lemma sub_list_neq_set: "(sub_list xs ys \<and> \<not> list_eq xs ys) = (set xs \<subset> set ys)"
+ − 945
by (auto simp add: sub_list_set)
+ − 946
+ − 947
lemma fcard_raw_set: "fcard_raw xs = card (set xs)"
+ − 948
by (induct xs) (auto simp add: insert_absorb memb_def card_insert_disjoint finite_set)
+ − 949
+ − 950
lemma memb_set: "memb x xs = (x \<in> set xs)"
+ − 951
by (simp only: memb_def)
+ − 952
+ − 953
lemma filter_set: "set (filter P xs) = P \<inter> (set xs)"
+ − 954
by (induct xs, simp)
+ − 955
(metis Int_insert_right_if0 Int_insert_right_if1 List.set.simps(2) filter.simps(2) mem_def)
+ − 956
+ − 957
lemma delete_raw_set: "set (delete_raw xs x) = set xs - {x}"
+ − 958
by (induct xs) auto
+ − 959
+ − 960
lemma inter_raw_set: "set (finter_raw xs ys) = set xs \<inter> set ys"
+ − 961
by (induct xs) (simp_all add: memb_def)
+ − 962
+ − 963
lemma fminus_raw_set: "set (fminus_raw xs ys) = set xs - set ys"
+ − 964
by (induct ys arbitrary: xs)
+ − 965
(simp_all add: fminus_raw.simps delete_raw_set, blast)
+ − 966
+ − 967
text {* Raw theorems of ffilter *}
+ − 968
+ − 969
lemma sub_list_filter: "sub_list (filter P xs) (filter Q xs) = (\<forall> x. memb x xs \<longrightarrow> P x \<longrightarrow> Q x)"
+ − 970
unfolding sub_list_def memb_def by auto
+ − 971
+ − 972
lemma list_eq_filter: "list_eq (filter P xs) (filter Q xs) = (\<forall>x. memb x xs \<longrightarrow> P x = Q x)"
+ − 973
unfolding memb_def by auto
+ − 974
1935
+ − 975
text {* Lifted theorems *}
1518
+ − 976
1819
+ − 977
lemma not_fin_fnil: "x |\<notin>| {||}"
+ − 978
by (lifting not_memb_nil)
1518
+ − 979
+ − 980
lemma fin_finsert_iff[simp]:
+ − 981
"x |\<in>| finsert y S = (x = y \<or> x |\<in>| S)"
+ − 982
by (lifting memb_cons_iff)
+ − 983
+ − 984
lemma
+ − 985
shows finsertI1: "x |\<in>| finsert x S"
+ − 986
and finsertI2: "x |\<in>| S \<Longrightarrow> x |\<in>| finsert y S"
+ − 987
by (lifting memb_consI1, lifting memb_consI2)
+ − 988
+ − 989
lemma finsert_absorb[simp]:
+ − 990
shows "x |\<in>| S \<Longrightarrow> finsert x S = S"
+ − 991
by (lifting memb_absorb)
+ − 992
+ − 993
lemma fempty_not_finsert[simp]:
1533
+ − 994
"{||} \<noteq> finsert x S"
+ − 995
"finsert x S \<noteq> {||}"
1518
+ − 996
by (lifting nil_not_cons)
+ − 997
+ − 998
lemma finsert_left_comm:
1822
+ − 999
"finsert x (finsert y S) = finsert y (finsert x S)"
1518
+ − 1000
by (lifting cons_left_comm)
+ − 1001
+ − 1002
lemma finsert_left_idem:
1822
+ − 1003
"finsert x (finsert x S) = finsert x S"
1518
+ − 1004
by (lifting cons_left_idem)
+ − 1005
+ − 1006
lemma fsingleton_eq[simp]:
+ − 1007
shows "{|x|} = {|y|} \<longleftrightarrow> x = y"
+ − 1008
by (lifting singleton_list_eq)
+ − 1009
+ − 1010
text {* fset_to_set *}
+ − 1011
1533
+ − 1012
lemma fset_to_set_simps[simp]:
1819
+ − 1013
"fset_to_set {||} = ({} :: 'a set)"
+ − 1014
"fset_to_set (finsert (h :: 'a) t) = insert h (fset_to_set t)"
+ − 1015
by (lifting set.simps)
1518
+ − 1016
+ − 1017
lemma in_fset_to_set:
1822
+ − 1018
"x \<in> fset_to_set S \<equiv> x |\<in>| S"
1518
+ − 1019
by (lifting memb_def[symmetric])
+ − 1020
1819
+ − 1021
lemma none_fin_fempty:
1824
+ − 1022
"(\<forall>x. x |\<notin>| S) = (S = {||})"
+ − 1023
by (lifting none_memb_nil)
1518
+ − 1024
1533
+ − 1025
lemma fset_cong:
2084
+ − 1026
"(S = T) = (fset_to_set S = fset_to_set T)"
1533
+ − 1027
by (lifting set_cong)
+ − 1028
1518
+ − 1029
text {* fcard *}
+ − 1030
+ − 1031
lemma fcard_fempty [simp]:
+ − 1032
shows "fcard {||} = 0"
+ − 1033
by (lifting fcard_raw_nil)
+ − 1034
+ − 1035
lemma fcard_finsert_if [simp]:
+ − 1036
shows "fcard (finsert x S) = (if x |\<in>| S then fcard S else Suc (fcard S))"
+ − 1037
by (lifting fcard_raw_cons)
+ − 1038
1822
+ − 1039
lemma fcard_0: "(fcard S = 0) = (S = {||})"
1813
+ − 1040
by (lifting fcard_raw_0)
+ − 1041
1821
+ − 1042
lemma fcard_1:
1822
+ − 1043
shows "(fcard S = 1) = (\<exists>x. S = {|x|})"
1819
+ − 1044
by (lifting fcard_raw_1)
+ − 1045
2084
+ − 1046
lemma fcard_gt_0:
1860
+ − 1047
shows "x \<in> fset_to_set S \<Longrightarrow> 0 < fcard S"
1518
+ − 1048
by (lifting fcard_raw_gt_0)
+ − 1049
2084
+ − 1050
lemma fcard_not_fin:
1860
+ − 1051
shows "(x |\<notin>| S) = (fcard (finsert x S) = Suc (fcard S))"
1813
+ − 1052
by (lifting fcard_raw_not_memb)
+ − 1053
1822
+ − 1054
lemma fcard_suc: "fcard S = Suc n \<Longrightarrow> \<exists>x T. x |\<notin>| T \<and> S = finsert x T \<and> fcard T = n"
1813
+ − 1055
by (lifting fcard_raw_suc)
+ − 1056
1819
+ − 1057
lemma fcard_delete:
1822
+ − 1058
"fcard (fdelete S y) = (if y |\<in>| S then fcard S - 1 else fcard S)"
1819
+ − 1059
by (lifting fcard_raw_delete)
+ − 1060
1878
+ − 1061
lemma fcard_suc_memb: "fcard A = Suc n \<Longrightarrow> \<exists>a. a |\<in>| A"
+ − 1062
by (lifting fcard_raw_suc_memb)
+ − 1063
+ − 1064
lemma fin_fcard_not_0: "a |\<in>| A \<Longrightarrow> fcard A \<noteq> 0"
1887
+ − 1065
by (lifting memb_card_not_0)
1878
+ − 1066
1518
+ − 1067
text {* funion *}
+ − 1068
2084
+ − 1069
lemmas [simp] =
+ − 1070
sup_bot_left[where 'a="'a fset", standard]
+ − 1071
sup_bot_right[where 'a="'a fset", standard]
1518
+ − 1072
2084
+ − 1073
lemma funion_finsert[simp]:
+ − 1074
shows "finsert x S |\<union>| T = finsert x (S |\<union>| T)"
+ − 1075
by (lifting append.simps(2))
1887
+ − 1076
+ − 1077
lemma singleton_union_left:
+ − 1078
"{|a|} |\<union>| S = finsert a S"
+ − 1079
by simp
+ − 1080
+ − 1081
lemma singleton_union_right:
+ − 1082
"S |\<union>| {|a|} = finsert a S"
1907
+ − 1083
by (subst sup.commute) simp
1887
+ − 1084
1518
+ − 1085
section {* Induction and Cases rules for finite sets *}
+ − 1086
+ − 1087
lemma fset_strong_cases:
2084
+ − 1088
obtains "xs = {||}"
+ − 1089
| x ys where "x |\<notin>| ys" and "xs = finsert x ys"
1819
+ − 1090
by (lifting fset_raw_strong_cases)
1518
+ − 1091
+ − 1092
lemma fset_exhaust[case_names fempty finsert, cases type: fset]:
+ − 1093
shows "\<lbrakk>S = {||} \<Longrightarrow> P; \<And>x S'. S = finsert x S' \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
+ − 1094
by (lifting list.exhaust)
+ − 1095
1533
+ − 1096
lemma fset_induct_weak[case_names fempty finsert]:
1518
+ − 1097
shows "\<lbrakk>P {||}; \<And>x S. P S \<Longrightarrow> P (finsert x S)\<rbrakk> \<Longrightarrow> P S"
+ − 1098
by (lifting list.induct)
+ − 1099
1533
+ − 1100
lemma fset_induct[case_names fempty finsert, induct type: fset]:
2084
+ − 1101
assumes prem1: "P {||}"
1518
+ − 1102
and prem2: "\<And>x S. \<lbrakk>x |\<notin>| S; P S\<rbrakk> \<Longrightarrow> P (finsert x S)"
+ − 1103
shows "P S"
1533
+ − 1104
proof(induct S rule: fset_induct_weak)
1518
+ − 1105
case fempty
+ − 1106
show "P {||}" by (rule prem1)
+ − 1107
next
+ − 1108
case (finsert x S)
+ − 1109
have asm: "P S" by fact
+ − 1110
show "P (finsert x S)"
1938
+ − 1111
by (cases "x |\<in>| S") (simp_all add: asm prem2)
1518
+ − 1112
qed
+ − 1113
1533
+ − 1114
lemma fset_induct2:
+ − 1115
"P {||} {||} \<Longrightarrow>
+ − 1116
(\<And>x xs. x |\<notin>| xs \<Longrightarrow> P (finsert x xs) {||}) \<Longrightarrow>
+ − 1117
(\<And>y ys. y |\<notin>| ys \<Longrightarrow> P {||} (finsert y ys)) \<Longrightarrow>
+ − 1118
(\<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>
+ − 1119
P xsa ysa"
+ − 1120
apply (induct xsa arbitrary: ysa)
+ − 1121
apply (induct_tac x rule: fset_induct)
+ − 1122
apply simp_all
+ − 1123
apply (induct_tac xa rule: fset_induct)
+ − 1124
apply simp_all
+ − 1125
done
1518
+ − 1126
2084
+ − 1127
lemma fset_fcard_induct:
+ − 1128
assumes a: "P {||}"
+ − 1129
and b: "\<And>xs ys. Suc (fcard xs) = (fcard ys) \<Longrightarrow> P xs \<Longrightarrow> P ys"
+ − 1130
shows "P zs"
+ − 1131
proof (induct zs)
+ − 1132
show "P {||}" by (rule a)
+ − 1133
next
+ − 1134
fix x :: 'a and zs :: "'a fset"
+ − 1135
assume h: "P zs"
+ − 1136
assume "x |\<notin>| zs"
+ − 1137
then have H1: "Suc (fcard zs) = fcard (finsert x zs)" using fcard_suc by auto
+ − 1138
then show "P (finsert x zs)" using b h by simp
+ − 1139
qed
+ − 1140
1819
+ − 1141
text {* fmap *}
+ − 1142
1533
+ − 1143
lemma fmap_simps[simp]:
+ − 1144
"fmap (f :: 'a \<Rightarrow> 'b) {||} = {||}"
1822
+ − 1145
"fmap f (finsert x S) = finsert (f x) (fmap f S)"
1533
+ − 1146
by (lifting map.simps)
+ − 1147
+ − 1148
lemma fmap_set_image:
1822
+ − 1149
"fset_to_set (fmap f S) = f ` (fset_to_set S)"
2084
+ − 1150
by (induct S) simp_all
1533
+ − 1151
+ − 1152
lemma inj_fmap_eq_iff:
1822
+ − 1153
"inj f \<Longrightarrow> (fmap f S = fmap f T) = (S = T)"
1533
+ − 1154
by (lifting inj_map_eq_iff)
+ − 1155
1822
+ − 1156
lemma fmap_funion: "fmap f (S |\<union>| T) = fmap f S |\<union>| fmap f T"
1813
+ − 1157
by (lifting map_append)
+ − 1158
1819
+ − 1159
lemma fin_funion:
1822
+ − 1160
"x |\<in>| S |\<union>| T \<longleftrightarrow> x |\<in>| S \<or> x |\<in>| T"
1819
+ − 1161
by (lifting memb_append)
+ − 1162
2084
+ − 1163
text {* to_set *}
+ − 1164
+ − 1165
lemma fin_set: "(x |\<in>| xs) = (x \<in> fset_to_set xs)"
+ − 1166
by (lifting memb_set)
+ − 1167
+ − 1168
lemma fnotin_set: "(x |\<notin>| xs) = (x \<notin> fset_to_set xs)"
+ − 1169
by (simp add: fin_set)
+ − 1170
+ − 1171
lemma fcard_set: "fcard xs = card (fset_to_set xs)"
+ − 1172
by (lifting fcard_raw_set)
+ − 1173
+ − 1174
lemma fsubseteq_set: "(xs |\<subseteq>| ys) = (fset_to_set xs \<subseteq> fset_to_set ys)"
+ − 1175
by (lifting sub_list_set)
+ − 1176
+ − 1177
lemma fsubset_set: "(xs |\<subset>| ys) = (fset_to_set xs \<subset> fset_to_set ys)"
+ − 1178
unfolding less_fset by (lifting sub_list_neq_set)
+ − 1179
+ − 1180
lemma ffilter_set: "fset_to_set (ffilter P xs) = P \<inter> fset_to_set xs"
+ − 1181
by (lifting filter_set)
+ − 1182
+ − 1183
lemma fdelete_set: "fset_to_set (fdelete xs x) = fset_to_set xs - {x}"
+ − 1184
by (lifting delete_raw_set)
+ − 1185
+ − 1186
lemma inter_set: "fset_to_set (xs |\<inter>| ys) = fset_to_set xs \<inter> fset_to_set ys"
+ − 1187
by (lifting inter_raw_set)
+ − 1188
+ − 1189
lemma union_set: "fset_to_set (xs |\<union>| ys) = fset_to_set xs \<union> fset_to_set ys"
+ − 1190
by (lifting set_append)
+ − 1191
+ − 1192
lemma fminus_set: "fset_to_set (xs - ys) = fset_to_set xs - fset_to_set ys"
+ − 1193
by (lifting fminus_raw_set)
+ − 1194
+ − 1195
lemmas fset_to_set_trans =
+ − 1196
fin_set fnotin_set fcard_set fsubseteq_set fsubset_set
+ − 1197
inter_set union_set ffilter_set fset_to_set_simps
+ − 1198
fset_cong fdelete_set fmap_set_image fminus_set
+ − 1199
+ − 1200
1819
+ − 1201
text {* ffold *}
+ − 1202
+ − 1203
lemma ffold_nil: "ffold f z {||} = z"
+ − 1204
by (lifting ffold_raw.simps(1)[where 'a="'b" and 'b="'a"])
+ − 1205
+ − 1206
lemma ffold_finsert: "ffold f z (finsert a A) =
+ − 1207
(if rsp_fold f then if a |\<in>| A then ffold f z A else f a (ffold f z A) else z)"
+ − 1208
by (lifting ffold_raw.simps(2)[where 'a="'b" and 'b="'a"])
+ − 1209
+ − 1210
lemma fin_commute_ffold:
+ − 1211
"\<lbrakk>rsp_fold f; h |\<in>| b\<rbrakk> \<Longrightarrow> ffold f z b = f h (ffold f z (fdelete b h))"
+ − 1212
by (lifting memb_commute_ffold_raw)
+ − 1213
+ − 1214
text {* fdelete *}
+ − 1215
2084
+ − 1216
lemma fin_fdelete:
1822
+ − 1217
shows "x |\<in>| fdelete S y \<longleftrightarrow> x |\<in>| S \<and> x \<noteq> y"
1819
+ − 1218
by (lifting memb_delete_raw)
+ − 1219
2084
+ − 1220
lemma fin_fdelete_ident:
1822
+ − 1221
shows "x |\<notin>| fdelete S x"
1819
+ − 1222
by (lifting memb_delete_raw_ident)
+ − 1223
2084
+ − 1224
lemma not_memb_fdelete_ident:
1822
+ − 1225
shows "x |\<notin>| S \<Longrightarrow> fdelete S x = S"
1819
+ − 1226
by (lifting not_memb_delete_raw_ident)
+ − 1227
+ − 1228
lemma fset_fdelete_cases:
1822
+ − 1229
shows "S = {||} \<or> (\<exists>x. x |\<in>| S \<and> S = finsert x (fdelete S x))"
1819
+ − 1230
by (lifting fset_raw_delete_raw_cases)
+ − 1231
+ − 1232
text {* inter *}
+ − 1233
1822
+ − 1234
lemma finter_empty_l: "({||} |\<inter>| S) = {||}"
1819
+ − 1235
by (lifting finter_raw.simps(1))
+ − 1236
1822
+ − 1237
lemma finter_empty_r: "(S |\<inter>| {||}) = {||}"
1819
+ − 1238
by (lifting finter_raw_empty)
+ − 1239
+ − 1240
lemma finter_finsert:
1822
+ − 1241
"finsert x S |\<inter>| T = (if x |\<in>| T then finsert x (S |\<inter>| T) else S |\<inter>| T)"
1819
+ − 1242
by (lifting finter_raw.simps(2))
+ − 1243
+ − 1244
lemma fin_finter:
1822
+ − 1245
"x |\<in>| (S |\<inter>| T) \<longleftrightarrow> x |\<in>| S \<and> x |\<in>| T"
1819
+ − 1246
by (lifting memb_finter_raw)
+ − 1247
1893
+ − 1248
lemma fsubset_finsert:
+ − 1249
"(finsert x xs |\<subseteq>| ys) = (x |\<in>| ys \<and> xs |\<subseteq>| ys)"
+ − 1250
by (lifting sub_list_cons)
+ − 1251
1936
+ − 1252
lemma "xs |\<subseteq>| ys \<equiv> \<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys"
+ − 1253
by (lifting sub_list_def[simplified memb_def[symmetric]])
1893
+ − 1254
+ − 1255
lemma fsubset_fin: "xs |\<subseteq>| ys = (\<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys)"
+ − 1256
by (rule meta_eq_to_obj_eq)
+ − 1257
(lifting sub_list_def[simplified memb_def[symmetric]])
+ − 1258
2084
+ − 1259
lemma fminus_fin: "(x |\<in>| xs - ys) = (x |\<in>| xs \<and> x |\<notin>| ys)"
+ − 1260
by (lifting fminus_raw_memb)
+ − 1261
+ − 1262
lemma fminus_red: "finsert x xs - ys = (if x |\<in>| ys then xs - ys else finsert x (xs - ys))"
+ − 1263
by (lifting fminus_raw_red)
+ − 1264
+ − 1265
lemma fminus_red_fin[simp]: "x |\<in>| ys \<Longrightarrow> finsert x xs - ys = xs - ys"
+ − 1266
by (simp add: fminus_red)
+ − 1267
+ − 1268
lemma fminus_red_fnotin[simp]: "x |\<notin>| ys \<Longrightarrow> finsert x xs - ys = finsert x (xs - ys)"
+ − 1269
by (simp add: fminus_red)
+ − 1270
1820
+ − 1271
lemma expand_fset_eq:
1822
+ − 1272
"(S = T) = (\<forall>x. (x |\<in>| S) = (x |\<in>| T))"
1820
+ − 1273
by (lifting list_eq.simps[simplified memb_def[symmetric]])
+ − 1274
1888
+ − 1275
(* We cannot write it as "assumes .. shows" since Isabelle changes
+ − 1276
the quantifiers to schematic variables and reintroduces them in
+ − 1277
a different order *)
+ − 1278
lemma fset_eq_cases:
+ − 1279
"\<lbrakk>a1 = a2;
+ − 1280
\<And>a b xs. \<lbrakk>a1 = finsert a (finsert b xs); a2 = finsert b (finsert a xs)\<rbrakk> \<Longrightarrow> P;
+ − 1281
\<lbrakk>a1 = {||}; a2 = {||}\<rbrakk> \<Longrightarrow> P; \<And>xs ys. \<lbrakk>a1 = ys; a2 = xs; xs = ys\<rbrakk> \<Longrightarrow> P;
+ − 1282
\<And>a xs. \<lbrakk>a1 = finsert a (finsert a xs); a2 = finsert a xs\<rbrakk> \<Longrightarrow> P;
+ − 1283
\<And>xs ys a. \<lbrakk>a1 = finsert a xs; a2 = finsert a ys; xs = ys\<rbrakk> \<Longrightarrow> P;
+ − 1284
\<And>xs1 xs2 xs3. \<lbrakk>a1 = xs1; a2 = xs3; xs1 = xs2; xs2 = xs3\<rbrakk> \<Longrightarrow> P\<rbrakk>
+ − 1285
\<Longrightarrow> P"
+ − 1286
by (lifting list_eq2.cases[simplified list_eq2_equiv[symmetric]])
+ − 1287
+ − 1288
lemma fset_eq_induct:
+ − 1289
assumes "x1 = x2"
+ − 1290
and "\<And>a b xs. P (finsert a (finsert b xs)) (finsert b (finsert a xs))"
+ − 1291
and "P {||} {||}"
+ − 1292
and "\<And>xs ys. \<lbrakk>xs = ys; P xs ys\<rbrakk> \<Longrightarrow> P ys xs"
+ − 1293
and "\<And>a xs. P (finsert a (finsert a xs)) (finsert a xs)"
+ − 1294
and "\<And>xs ys a. \<lbrakk>xs = ys; P xs ys\<rbrakk> \<Longrightarrow> P (finsert a xs) (finsert a ys)"
+ − 1295
and "\<And>xs1 xs2 xs3. \<lbrakk>xs1 = xs2; P xs1 xs2; xs2 = xs3; P xs2 xs3\<rbrakk> \<Longrightarrow> P xs1 xs3"
+ − 1296
shows "P x1 x2"
+ − 1297
using assms
+ − 1298
by (lifting list_eq2.induct[simplified list_eq2_equiv[symmetric]])
1820
+ − 1299
1935
+ − 1300
text {* concat *}
+ − 1301
+ − 1302
lemma fconcat_empty:
+ − 1303
shows "fconcat {||} = {||}"
+ − 1304
by (lifting concat.simps(1))
+ − 1305
+ − 1306
lemma fconcat_insert:
+ − 1307
shows "fconcat (finsert x S) = x |\<union>| fconcat S"
+ − 1308
by (lifting concat.simps(2))
+ − 1309
+ − 1310
lemma "fconcat (xs |\<union>| ys) = fconcat xs |\<union>| fconcat ys"
+ − 1311
by (lifting concat_append)
+ − 1312
2084
+ − 1313
text {* ffilter *}
+ − 1314
+ − 1315
lemma subseteq_filter: "ffilter P xs <= ffilter Q xs = (\<forall> x. x |\<in>| xs \<longrightarrow> P x \<longrightarrow> Q x)"
+ − 1316
by (lifting sub_list_filter)
+ − 1317
+ − 1318
lemma eq_ffilter: "(ffilter P xs = ffilter Q xs) = (\<forall>x. x |\<in>| xs \<longrightarrow> P x = Q x)"
+ − 1319
by (lifting list_eq_filter)
+ − 1320
+ − 1321
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"
+ − 1322
unfolding less_fset by (auto simp add: subseteq_filter eq_ffilter)
+ − 1323
+ − 1324
section {* lemmas transferred from Finite_Set theory *}
+ − 1325
+ − 1326
text {* finiteness for finite sets holds *}
+ − 1327
lemma finite_fset: "finite (fset_to_set S)"
+ − 1328
by (induct S) auto
+ − 1329
+ − 1330
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)"
+ − 1331
unfolding fset_to_set_trans
+ − 1332
by (rule finite_set_choice[simplified Ball_def, OF finite_fset])
+ − 1333
+ − 1334
lemma fsubseteq_fnil: "xs |\<subseteq>| {||} = (xs = {||})"
+ − 1335
unfolding fset_to_set_trans
+ − 1336
by (rule subset_empty)
+ − 1337
+ − 1338
lemma not_fsubset_fnil: "\<not> xs |\<subset>| {||}"
+ − 1339
unfolding fset_to_set_trans
+ − 1340
by (rule not_psubset_empty)
+ − 1341
+ − 1342
lemma fcard_mono: "xs |\<subseteq>| ys \<Longrightarrow> fcard xs \<le> fcard ys"
+ − 1343
unfolding fset_to_set_trans
+ − 1344
by (rule card_mono[OF finite_fset])
+ − 1345
+ − 1346
lemma fcard_fseteq: "xs |\<subseteq>| ys \<Longrightarrow> fcard ys \<le> fcard xs \<Longrightarrow> xs = ys"
+ − 1347
unfolding fset_to_set_trans
+ − 1348
by (rule card_seteq[OF finite_fset])
+ − 1349
+ − 1350
lemma psubset_fcard_mono: "xs |\<subset>| ys \<Longrightarrow> fcard xs < fcard ys"
+ − 1351
unfolding fset_to_set_trans
+ − 1352
by (rule psubset_card_mono[OF finite_fset])
+ − 1353
+ − 1354
lemma fcard_funion_finter: "fcard xs + fcard ys = fcard (xs |\<union>| ys) + fcard (xs |\<inter>| ys)"
+ − 1355
unfolding fset_to_set_trans
+ − 1356
by (rule card_Un_Int[OF finite_fset finite_fset])
+ − 1357
+ − 1358
lemma fcard_funion_disjoint: "xs |\<inter>| ys = {||} \<Longrightarrow> fcard (xs |\<union>| ys) = fcard xs + fcard ys"
+ − 1359
unfolding fset_to_set_trans
+ − 1360
by (rule card_Un_disjoint[OF finite_fset finite_fset])
+ − 1361
+ − 1362
lemma fcard_delete1_less: "x |\<in>| xs \<Longrightarrow> fcard (fdelete xs x) < fcard xs"
+ − 1363
unfolding fset_to_set_trans
+ − 1364
by (rule card_Diff1_less[OF finite_fset])
+ − 1365
+ − 1366
lemma fcard_delete2_less: "x |\<in>| xs \<Longrightarrow> y |\<in>| xs \<Longrightarrow> fcard (fdelete (fdelete xs x) y) < fcard xs"
+ − 1367
unfolding fset_to_set_trans
+ − 1368
by (rule card_Diff2_less[OF finite_fset])
+ − 1369
+ − 1370
lemma fcard_delete1_le: "fcard (fdelete xs x) <= fcard xs"
+ − 1371
unfolding fset_to_set_trans
+ − 1372
by (rule card_Diff1_le[OF finite_fset])
+ − 1373
+ − 1374
lemma fcard_psubset: "ys |\<subseteq>| xs \<Longrightarrow> fcard ys < fcard xs \<Longrightarrow> ys |\<subset>| xs"
+ − 1375
unfolding fset_to_set_trans
+ − 1376
by (rule card_psubset[OF finite_fset])
+ − 1377
+ − 1378
lemma fcard_fmap_le: "fcard (fmap f xs) \<le> fcard xs"
+ − 1379
unfolding fset_to_set_trans
+ − 1380
by (rule card_image_le[OF finite_fset])
+ − 1381
+ − 1382
lemma fin_fminus_fnotin: "x |\<in>| F - S \<Longrightarrow> x |\<notin>| S"
+ − 1383
unfolding fset_to_set_trans
+ − 1384
by blast
+ − 1385
+ − 1386
lemma fin_fnotin_fminus: "x |\<in>| S \<Longrightarrow> x |\<notin>| F - S"
+ − 1387
unfolding fset_to_set_trans
+ − 1388
by blast
+ − 1389
+ − 1390
lemma fin_mdef: "x |\<in>| F = ((x |\<notin>| (F - {|x|})) & (F = finsert x (F - {|x|})))"
+ − 1391
unfolding fset_to_set_trans
+ − 1392
by blast
+ − 1393
+ − 1394
lemma fcard_fminus_finsert[simp]:
+ − 1395
assumes "a |\<in>| A" and "a |\<notin>| B"
+ − 1396
shows "fcard(A - finsert a B) = fcard(A - B) - 1"
+ − 1397
using assms unfolding fset_to_set_trans
+ − 1398
by (rule card_Diff_insert[OF finite_fset])
+ − 1399
+ − 1400
lemma fcard_fminus_fsubset:
+ − 1401
assumes "B |\<subseteq>| A"
+ − 1402
shows "fcard (A - B) = fcard A - fcard B"
+ − 1403
using assms unfolding fset_to_set_trans
+ − 1404
by (rule card_Diff_subset[OF finite_fset])
+ − 1405
+ − 1406
lemma fcard_fminus_subset_finter:
+ − 1407
"fcard (A - B) = fcard A - fcard (A |\<inter>| B)"
+ − 1408
unfolding fset_to_set_trans
+ − 1409
by (rule card_Diff_subset_Int) (fold inter_set, rule finite_fset)
+ − 1410
+ − 1411
1533
+ − 1412
ML {*
2084
+ − 1413
fun dest_fsetT (Type (@{type_name fset}, [T])) = T
1533
+ − 1414
| dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
+ − 1415
*}
1518
+ − 1416
1682
+ − 1417
no_notation
+ − 1418
list_eq (infix "\<approx>" 50)
+ − 1419
2234
+ − 1420
ML {*
+ − 1421
open Quotient_Info;
+ − 1422
+ − 1423
exception LIFT_MATCH of string
+ − 1424
+ − 1425
+ − 1426
+ − 1427
(*** Aggregate Rep/Abs Function ***)
+ − 1428
+ − 1429
+ − 1430
(* The flag RepF is for types in negative position; AbsF is for types
+ − 1431
in positive position. Because of this, function types need to be
+ − 1432
treated specially, since there the polarity changes.
+ − 1433
*)
+ − 1434
+ − 1435
datatype flag = AbsF | RepF
+ − 1436
+ − 1437
fun negF AbsF = RepF
+ − 1438
| negF RepF = AbsF
+ − 1439
+ − 1440
fun is_identity (Const (@{const_name "id"}, _)) = true
+ − 1441
| is_identity _ = false
+ − 1442
+ − 1443
fun mk_identity ty = Const (@{const_name "id"}, ty --> ty)
+ − 1444
+ − 1445
fun mk_fun_compose flag (trm1, trm2) =
+ − 1446
case flag of
+ − 1447
AbsF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2
+ − 1448
| RepF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1
+ − 1449
+ − 1450
fun get_mapfun ctxt s =
+ − 1451
let
+ − 1452
val thy = ProofContext.theory_of ctxt
+ − 1453
val exn = LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
+ − 1454
val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn
+ − 1455
in
+ − 1456
Const (mapfun, dummyT)
1518
+ − 1457
end
2234
+ − 1458
+ − 1459
(* makes a Free out of a TVar *)
+ − 1460
fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT)
+ − 1461
+ − 1462
(* produces an aggregate map function for the
+ − 1463
rty-part of a quotient definition; abstracts
+ − 1464
over all variables listed in vs (these variables
+ − 1465
correspond to the type variables in rty)
+ − 1466
+ − 1467
for example for: (?'a list * ?'b)
+ − 1468
it produces: %a b. prod_map (map a) b
+ − 1469
*)
+ − 1470
fun mk_mapfun ctxt vs rty =
+ − 1471
let
+ − 1472
val vs' = map (mk_Free) vs
+ − 1473
+ − 1474
fun mk_mapfun_aux rty =
+ − 1475
case rty of
+ − 1476
TVar _ => mk_Free rty
+ − 1477
| Type (_, []) => mk_identity rty
+ − 1478
| Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys)
+ − 1479
| _ => raise LIFT_MATCH "mk_mapfun (default)"
+ − 1480
in
+ − 1481
fold_rev Term.lambda vs' (mk_mapfun_aux rty)
+ − 1482
end
+ − 1483
+ − 1484
(* looks up the (varified) rty and qty for
+ − 1485
a quotient definition
+ − 1486
*)
+ − 1487
fun get_rty_qty ctxt s =
+ − 1488
let
+ − 1489
val thy = ProofContext.theory_of ctxt
+ − 1490
val exn = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
+ − 1491
val qdata = (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn
+ − 1492
in
+ − 1493
(#rtyp qdata, #qtyp qdata)
+ − 1494
end
+ − 1495
+ − 1496
(* takes two type-environments and looks
+ − 1497
up in both of them the variable v, which
+ − 1498
must be listed in the environment
+ − 1499
*)
+ − 1500
fun double_lookup rtyenv qtyenv v =
+ − 1501
let
+ − 1502
val v' = fst (dest_TVar v)
+ − 1503
in
+ − 1504
(snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v')))
+ − 1505
end
+ − 1506
+ − 1507
(* matches a type pattern with a type *)
+ − 1508
fun match ctxt err ty_pat ty =
+ − 1509
let
+ − 1510
val thy = ProofContext.theory_of ctxt
+ − 1511
in
+ − 1512
Sign.typ_match thy (ty_pat, ty) Vartab.empty
+ − 1513
handle MATCH_TYPE => err ctxt ty_pat ty
+ − 1514
end
+ − 1515
+ − 1516
(* produces the rep or abs constant for a qty *)
+ − 1517
fun absrep_const flag ctxt qty_str =
+ − 1518
let
+ − 1519
val qty_name = Long_Name.base_name qty_str
+ − 1520
val qualifier = Long_Name.qualifier qty_str
+ − 1521
in
+ − 1522
case flag of
+ − 1523
AbsF => Const (Long_Name.qualify qualifier ("abs_" ^ qty_name), dummyT)
+ − 1524
| RepF => Const (Long_Name.qualify qualifier ("rep_" ^ qty_name), dummyT)
+ − 1525
end
+ − 1526
+ − 1527
(* Lets Nitpick represent elements of quotient types as elements of the raw type *)
+ − 1528
fun absrep_const_chk flag ctxt qty_str =
+ − 1529
Syntax.check_term ctxt (absrep_const flag ctxt qty_str)
+ − 1530
+ − 1531
fun absrep_match_err ctxt ty_pat ty =
+ − 1532
let
+ − 1533
val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
+ − 1534
val ty_str = Syntax.string_of_typ ctxt ty
+ − 1535
in
+ − 1536
raise LIFT_MATCH (space_implode " "
+ − 1537
["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
+ − 1538
end
+ − 1539
+ − 1540
+ − 1541
(** generation of an aggregate absrep function **)
+ − 1542
+ − 1543
(* - In case of equal types we just return the identity.
+ − 1544
+ − 1545
- In case of TFrees we also return the identity.
+ − 1546
+ − 1547
- In case of function types we recurse taking
+ − 1548
the polarity change into account.
+ − 1549
+ − 1550
- If the type constructors are equal, we recurse for the
+ − 1551
arguments and build the appropriate map function.
+ − 1552
+ − 1553
- If the type constructors are unequal, there must be an
+ − 1554
instance of quotient types:
+ − 1555
+ − 1556
- we first look up the corresponding rty_pat and qty_pat
+ − 1557
from the quotient definition; the arguments of qty_pat
+ − 1558
must be some distinct TVars
+ − 1559
- we then match the rty_pat with rty and qty_pat with qty;
+ − 1560
if matching fails the types do not correspond -> error
+ − 1561
- the matching produces two environments; we look up the
+ − 1562
assignments for the qty_pat variables and recurse on the
+ − 1563
assignments
+ − 1564
- we prefix the aggregate map function for the rty_pat,
+ − 1565
which is an abstraction over all type variables
+ − 1566
- finally we compose the result with the appropriate
+ − 1567
absrep function in case at least one argument produced
+ − 1568
a non-identity function /
+ − 1569
otherwise we just return the appropriate absrep
+ − 1570
function
+ − 1571
+ − 1572
The composition is necessary for types like
+ − 1573
+ − 1574
('a list) list / ('a foo) foo
+ − 1575
+ − 1576
The matching is necessary for types like
+ − 1577
+ − 1578
('a * 'a) list / 'a bar
+ − 1579
+ − 1580
The test is necessary in order to eliminate superfluous
+ − 1581
identity maps.
+ − 1582
*)
+ − 1583
+ − 1584
fun absrep_fun flag ctxt (rty, qty) =
+ − 1585
if rty = qty
+ − 1586
then mk_identity rty
+ − 1587
else
+ − 1588
case (rty, qty) of
+ − 1589
(Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) =>
+ − 1590
let
+ − 1591
val arg1 = absrep_fun (negF flag) ctxt (ty1, ty1')
+ − 1592
val arg2 = absrep_fun flag ctxt (ty2, ty2')
+ − 1593
in
+ − 1594
list_comb (get_mapfun ctxt "fun", [arg1, arg2])
+ − 1595
end
+ − 1596
| (Type (s, tys), Type (s', tys')) =>
+ − 1597
if s = s'
+ − 1598
then
+ − 1599
let
+ − 1600
val args = map (absrep_fun flag ctxt) (tys ~~ tys')
+ − 1601
in
+ − 1602
list_comb (get_mapfun ctxt s, args)
+ − 1603
end
+ − 1604
else
+ − 1605
let
+ − 1606
val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
+ − 1607
val rtyenv = match ctxt absrep_match_err rty_pat rty
+ − 1608
val qtyenv = match ctxt absrep_match_err qty_pat qty
+ − 1609
val args_aux = map (double_lookup rtyenv qtyenv) vs
+ − 1610
val args = map (absrep_fun flag ctxt) args_aux
+ − 1611
val map_fun = mk_mapfun ctxt vs rty_pat
+ − 1612
val result = list_comb (map_fun, args)
+ − 1613
in
+ − 1614
(*if forall is_identity args
+ − 1615
then absrep_const flag ctxt s'
+ − 1616
else*) mk_fun_compose flag (absrep_const flag ctxt s', result)
+ − 1617
end
+ − 1618
| (TFree x, TFree x') =>
+ − 1619
if x = x'
+ − 1620
then mk_identity rty
+ − 1621
else raise (LIFT_MATCH "absrep_fun (frees)")
+ − 1622
| (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)")
+ − 1623
| _ => raise (LIFT_MATCH "absrep_fun (default)")
+ − 1624
+ − 1625
+ − 1626
*}
+ − 1627
+ − 1628
ML {*
2238
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1629
let
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1630
val parser = Args.context -- Scan.lift Args.name_source
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1631
fun typ_pat (ctxt, str) =
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1632
str |> Syntax.parse_typ ctxt
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1633
|> ML_Syntax.print_typ
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1634
|> ML_Syntax.atomic
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1635
in
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1636
ML_Antiquote.inline "typ_pat" (parser >> typ_pat)
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1637
end
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1638
*}
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1639
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1640
ML {*
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1641
mk_mapfun @{context} [@{typ_pat "?'a"}] @{typ_pat "(?'a list) * nat"}
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1642
|> Syntax.check_term @{context}
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1643
|> fastype_of
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1644
|> Syntax.string_of_typ @{context}
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1645
|> warning
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1646
*}
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1647
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1648
ML {*
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1649
mk_mapfun @{context} [@{typ_pat "?'a"}] @{typ_pat "(?'a list) * nat"}
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1650
|> Syntax.check_term @{context}
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1651
|> Syntax.string_of_term @{context}
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1652
|> warning
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1653
*}
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1654
8ddf1330f2ed
completed proof and started section about respectfulness and preservation
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1655
ML {*
2234
+ − 1656
absrep_fun AbsF @{context} (@{typ "('a list) list \<Rightarrow> 'a list"}, @{typ "('a fset) fset \<Rightarrow> 'a fset"})
+ − 1657
|> Syntax.string_of_term @{context}
+ − 1658
|> writeln
+ − 1659
*}
+ − 1660
+ − 1661
lemma "(\<lambda> (c::'s \<Rightarrow> bool). \<exists>(x::'s). c = rel x) = {c. \<exists>x. c = rel x}"
+ − 1662
apply(auto simp add: mem_def)
+ − 1663
done
+ − 1664
2249
+ − 1665
lemma ball_reg_right_unfolded: "(\<forall>x. R x \<longrightarrow> P x \<longrightarrow> Q x) \<longrightarrow> (All P \<longrightarrow> Ball R Q)"
+ − 1666
apply rule
+ − 1667
apply (rule ball_reg_right)
+ − 1668
apply auto
+ − 1669
done
2234
+ − 1670
+ − 1671
end