1440
+ − 1
theory Abs
1460
+ − 2
imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient" "../Quotient_Product"
1440
+ − 3
begin
+ − 4
1465
+ − 5
lemma permute_boolI:
+ − 6
fixes P::"bool"
+ − 7
shows "p \<bullet> P \<Longrightarrow> P"
+ − 8
apply(simp add: permute_bool_def)
+ − 9
done
+ − 10
+ − 11
lemma permute_boolE:
+ − 12
fixes P::"bool"
+ − 13
shows "P \<Longrightarrow> p \<bullet> P"
+ − 14
apply(simp add: permute_bool_def)
+ − 15
done
+ − 16
1440
+ − 17
fun
+ − 18
alpha_gen
+ − 19
where
+ − 20
alpha_gen[simp del]:
1465
+ − 21
"alpha_gen (bs, x) R f pi (cs, y) \<longleftrightarrow>
+ − 22
f x - bs = f y - cs \<and>
+ − 23
(f x - bs) \<sharp>* pi \<and>
+ − 24
R (pi \<bullet> x) y \<and>
+ − 25
pi \<bullet> bs = cs"
1440
+ − 26
+ − 27
notation
+ − 28
alpha_gen ("_ \<approx>gen _ _ _ _" [100, 100, 100, 100, 100] 100)
+ − 29
1460
+ − 30
lemma [mono]: "R1 \<le> R2 \<Longrightarrow> alpha_gen x R1 \<le> alpha_gen x R2"
+ − 31
by (cases x) (auto simp add: le_fun_def le_bool_def alpha_gen.simps)
1440
+ − 32
+ − 33
lemma alpha_gen_refl:
+ − 34
assumes a: "R x x"
1460
+ − 35
shows "(bs, x) \<approx>gen R f 0 (bs, x)"
1440
+ − 36
using a by (simp add: alpha_gen fresh_star_def fresh_zero_perm)
+ − 37
+ − 38
lemma alpha_gen_sym:
1460
+ − 39
assumes a: "(bs, x) \<approx>gen R f p (cs, y)"
1440
+ − 40
and b: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x"
1460
+ − 41
shows "(cs, y) \<approx>gen R f (- p) (bs, x)"
1465
+ − 42
using a b
+ − 43
apply (simp add: alpha_gen fresh_star_def fresh_def supp_minus_perm)
+ − 44
apply(clarify)
+ − 45
apply(simp)
+ − 46
done
1440
+ − 47
+ − 48
lemma alpha_gen_trans:
1460
+ − 49
assumes a: "(bs, x) \<approx>gen R f p1 (cs, y)"
+ − 50
and b: "(cs, y) \<approx>gen R f p2 (ds, z)"
+ − 51
and c: "\<lbrakk>R (p1 \<bullet> x) y; R (p2 \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((p2 + p1) \<bullet> x) z"
+ − 52
shows "(bs, x) \<approx>gen R f (p2 + p1) (ds, z)"
+ − 53
using a b c using supp_plus_perm
1440
+ − 54
apply(simp add: alpha_gen fresh_star_def fresh_def)
+ − 55
apply(blast)
+ − 56
done
+ − 57
+ − 58
lemma alpha_gen_eqvt:
+ − 59
assumes a: "(bs, x) \<approx>gen R f q (cs, y)"
+ − 60
and b: "R (q \<bullet> x) y \<Longrightarrow> R (p \<bullet> (q \<bullet> x)) (p \<bullet> y)"
+ − 61
and c: "p \<bullet> (f x) = f (p \<bullet> x)"
+ − 62
and d: "p \<bullet> (f y) = f (p \<bullet> y)"
+ − 63
shows "(p \<bullet> bs, p \<bullet> x) \<approx>gen R f (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
+ − 64
using a b
+ − 65
apply(simp add: alpha_gen c[symmetric] d[symmetric] Diff_eqvt[symmetric])
+ − 66
apply(simp add: permute_eqvt[symmetric])
+ − 67
apply(simp add: fresh_star_permute_iff)
+ − 68
apply(clarsimp)
+ − 69
done
+ − 70
1460
+ − 71
lemma alpha_gen_compose_sym:
+ − 72
fixes pi
+ − 73
assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)"
+ − 74
and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
+ − 75
shows "(ab, s) \<approx>gen R f (- pi) (aa, t)"
+ − 76
using b apply -
+ − 77
apply(simp add: alpha_gen.simps)
+ − 78
apply(erule conjE)+
+ − 79
apply(rule conjI)
+ − 80
apply(simp add: fresh_star_def fresh_minus_perm)
+ − 81
apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))")
+ − 82
apply simp
1465
+ − 83
apply(clarify)
+ − 84
apply(simp)
1460
+ − 85
apply(rule a)
+ − 86
apply assumption
+ − 87
done
+ − 88
+ − 89
lemma alpha_gen_compose_trans:
+ − 90
fixes pi pia
+ − 91
assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)"
+ − 92
and c: "(ab, ta) \<approx>gen R f pia (ac, sa)"
+ − 93
and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
+ − 94
shows "(aa, t) \<approx>gen R f (pia + pi) (ac, sa)"
+ − 95
using b c apply -
+ − 96
apply(simp add: alpha_gen.simps)
+ − 97
apply(erule conjE)+
+ − 98
apply(simp add: fresh_star_plus)
+ − 99
apply(drule_tac x="- pia \<bullet> sa" in spec)
+ − 100
apply(drule mp)
1465
+ − 101
apply(rotate_tac 5)
1460
+ − 102
apply(drule_tac pi="- pia" in a)
+ − 103
apply(simp)
1465
+ − 104
apply(rotate_tac 7)
1460
+ − 105
apply(drule_tac pi="pia" in a)
+ − 106
apply(simp)
+ − 107
done
+ − 108
+ − 109
lemma alpha_gen_compose_eqvt:
+ − 110
fixes pia
+ − 111
assumes b: "(g d, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2)) f pia (g e, s)"
+ − 112
and c: "\<And>y. pi \<bullet> (g y) = g (pi \<bullet> y)"
+ − 113
and a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)"
+ − 114
shows "(g (pi \<bullet> d), pi \<bullet> t) \<approx>gen R f (pi \<bullet> pia) (g (pi \<bullet> e), pi \<bullet> s)"
+ − 115
using b
+ − 116
apply -
+ − 117
apply(simp add: alpha_gen.simps)
+ − 118
apply(erule conjE)+
+ − 119
apply(rule conjI)
+ − 120
apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
+ − 121
apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt c[symmetric])
+ − 122
apply(rule conjI)
+ − 123
apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
+ − 124
apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt c[symmetric])
+ − 125
apply(subst permute_eqvt[symmetric])
+ − 126
apply(simp)
1465
+ − 127
sorry
1440
+ − 128
+ − 129
fun
+ − 130
alpha_abs
+ − 131
where
1460
+ − 132
"alpha_abs (bs, x) (cs, y) = (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))"
1440
+ − 133
+ − 134
notation
+ − 135
alpha_abs ("_ \<approx>abs _")
+ − 136
1465
+ − 137
+ − 138
1440
+ − 139
lemma alpha_abs_swap:
+ − 140
assumes a1: "a \<notin> (supp x) - bs"
+ − 141
and a2: "b \<notin> (supp x) - bs"
+ − 142
shows "(bs, x) \<approx>abs ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)"
+ − 143
apply(simp)
+ − 144
apply(rule_tac x="(a \<rightleftharpoons> b)" in exI)
1460
+ − 145
apply(simp add: alpha_gen)
1440
+ − 146
apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric])
+ − 147
apply(simp add: swap_set_not_in[OF a1 a2])
+ − 148
apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}")
+ − 149
using a1 a2
+ − 150
apply(simp add: fresh_star_def fresh_def)
+ − 151
apply(blast)
+ − 152
apply(simp add: supp_swap)
+ − 153
done
+ − 154
1460
+ − 155
lemma alpha_gen_swap_fun:
+ − 156
assumes f_eqvt: "\<And>pi. (pi \<bullet> (f x)) = f (pi \<bullet> x)"
+ − 157
assumes a1: "a \<notin> (f x) - bs"
+ − 158
and a2: "b \<notin> (f x) - bs"
+ − 159
shows "\<exists>pi. (bs, x) \<approx>gen (op=) f pi ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)"
1440
+ − 160
apply(rule_tac x="(a \<rightleftharpoons> b)" in exI)
1460
+ − 161
apply(simp add: alpha_gen)
+ − 162
apply(simp add: f_eqvt[symmetric] Diff_eqvt[symmetric])
1440
+ − 163
apply(simp add: swap_set_not_in[OF a1 a2])
+ − 164
apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}")
+ − 165
using a1 a2
+ − 166
apply(simp add: fresh_star_def fresh_def)
+ − 167
apply(blast)
+ − 168
apply(simp add: supp_swap)
+ − 169
done
+ − 170
1460
+ − 171
1440
+ − 172
fun
+ − 173
supp_abs_fun
1460
+ − 174
where
1440
+ − 175
"supp_abs_fun (bs, x) = (supp x) - bs"
+ − 176
+ − 177
lemma supp_abs_fun_lemma:
+ − 178
assumes a: "x \<approx>abs y"
+ − 179
shows "supp_abs_fun x = supp_abs_fun y"
+ − 180
using a
+ − 181
apply(induct rule: alpha_abs.induct)
+ − 182
apply(simp add: alpha_gen)
+ − 183
done
+ − 184
+ − 185
quotient_type 'a abs = "(atom set \<times> 'a::pt)" / "alpha_abs"
+ − 186
apply(rule equivpI)
+ − 187
unfolding reflp_def symp_def transp_def
+ − 188
apply(simp_all)
+ − 189
(* refl *)
+ − 190
apply(clarify)
+ − 191
apply(rule exI)
+ − 192
apply(rule alpha_gen_refl)
+ − 193
apply(simp)
+ − 194
(* symm *)
+ − 195
apply(clarify)
+ − 196
apply(rule exI)
+ − 197
apply(rule alpha_gen_sym)
+ − 198
apply(assumption)
+ − 199
apply(clarsimp)
+ − 200
(* trans *)
+ − 201
apply(clarify)
+ − 202
apply(rule exI)
+ − 203
apply(rule alpha_gen_trans)
+ − 204
apply(assumption)
+ − 205
apply(assumption)
+ − 206
apply(simp)
+ − 207
done
+ − 208
+ − 209
quotient_definition
+ − 210
"Abs::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs"
+ − 211
is
+ − 212
"Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"
+ − 213
+ − 214
lemma [quot_respect]:
+ − 215
shows "((op =) ===> (op =) ===> alpha_abs) Pair Pair"
+ − 216
apply(clarsimp)
+ − 217
apply(rule exI)
+ − 218
apply(rule alpha_gen_refl)
+ − 219
apply(simp)
+ − 220
done
+ − 221
+ − 222
lemma [quot_respect]:
+ − 223
shows "((op =) ===> alpha_abs ===> alpha_abs) permute permute"
+ − 224
apply(clarsimp)
+ − 225
apply(rule exI)
+ − 226
apply(rule alpha_gen_eqvt)
+ − 227
apply(assumption)
+ − 228
apply(simp_all add: supp_eqvt)
+ − 229
done
+ − 230
+ − 231
lemma [quot_respect]:
+ − 232
shows "(alpha_abs ===> (op =)) supp_abs_fun supp_abs_fun"
+ − 233
apply(simp add: supp_abs_fun_lemma)
+ − 234
done
+ − 235
+ − 236
lemma abs_induct:
+ − 237
"\<lbrakk>\<And>as (x::'a::pt). P (Abs as x)\<rbrakk> \<Longrightarrow> P t"
+ − 238
apply(lifting prod.induct[where 'a="atom set" and 'b="'a"])
+ − 239
done
+ − 240
+ − 241
(* TEST case *)
+ − 242
lemmas abs_induct2 = prod.induct[where 'a="atom set" and 'b="'a::pt", quot_lifted]
+ − 243
thm abs_induct abs_induct2
+ − 244
+ − 245
instantiation abs :: (pt) pt
+ − 246
begin
+ − 247
+ − 248
quotient_definition
+ − 249
"permute_abs::perm \<Rightarrow> ('a::pt abs) \<Rightarrow> 'a abs"
+ − 250
is
+ − 251
"permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)"
+ − 252
+ − 253
lemma permute_ABS [simp]:
+ − 254
fixes x::"'a::pt" (* ??? has to be 'a \<dots> 'b does not work *)
+ − 255
shows "(p \<bullet> (Abs as x)) = Abs (p \<bullet> as) (p \<bullet> x)"
+ − 256
by (lifting permute_prod.simps(1)[where 'a="atom set" and 'b="'a"])
+ − 257
+ − 258
instance
+ − 259
apply(default)
+ − 260
apply(induct_tac [!] x rule: abs_induct)
+ − 261
apply(simp_all)
+ − 262
done
+ − 263
+ − 264
end
+ − 265
+ − 266
quotient_definition
+ − 267
"supp_Abs_fun :: ('a::pt) abs \<Rightarrow> atom \<Rightarrow> bool"
+ − 268
is
+ − 269
"supp_abs_fun"
+ − 270
+ − 271
lemma supp_Abs_fun_simp:
+ − 272
shows "supp_Abs_fun (Abs bs x) = (supp x) - bs"
+ − 273
by (lifting supp_abs_fun.simps(1))
+ − 274
+ − 275
lemma supp_Abs_fun_eqvt [eqvt]:
+ − 276
shows "(p \<bullet> supp_Abs_fun x) = supp_Abs_fun (p \<bullet> x)"
+ − 277
apply(induct_tac x rule: abs_induct)
+ − 278
apply(simp add: supp_Abs_fun_simp supp_eqvt Diff_eqvt)
+ − 279
done
+ − 280
+ − 281
lemma supp_Abs_fun_fresh:
+ − 282
shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_Abs_fun (Abs bs x)"
+ − 283
apply(rule fresh_fun_eqvt_app)
+ − 284
apply(simp add: eqvts_raw)
+ − 285
apply(simp)
+ − 286
done
+ − 287
+ − 288
lemma Abs_swap:
+ − 289
assumes a1: "a \<notin> (supp x) - bs"
+ − 290
and a2: "b \<notin> (supp x) - bs"
+ − 291
shows "(Abs bs x) = (Abs ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x))"
1460
+ − 292
using a1 a2 by (lifting alpha_abs_swap)
1440
+ − 293
+ − 294
lemma Abs_supports:
1460
+ − 295
shows "((supp x) - as) supports (Abs as x)"
1440
+ − 296
unfolding supports_def
+ − 297
apply(clarify)
+ − 298
apply(simp (no_asm))
+ − 299
apply(subst Abs_swap[symmetric])
+ − 300
apply(simp_all)
+ − 301
done
+ − 302
+ − 303
lemma supp_Abs_subset1:
+ − 304
fixes x::"'a::fs"
+ − 305
shows "(supp x) - as \<subseteq> supp (Abs as x)"
+ − 306
apply(simp add: supp_conv_fresh)
+ − 307
apply(auto)
+ − 308
apply(drule_tac supp_Abs_fun_fresh)
+ − 309
apply(simp only: supp_Abs_fun_simp)
+ − 310
apply(simp add: fresh_def)
+ − 311
apply(simp add: supp_finite_atom_set finite_supp)
+ − 312
done
+ − 313
+ − 314
lemma supp_Abs_subset2:
+ − 315
fixes x::"'a::fs"
+ − 316
shows "supp (Abs as x) \<subseteq> (supp x) - as"
+ − 317
apply(rule supp_is_subset)
+ − 318
apply(rule Abs_supports)
+ − 319
apply(simp add: finite_supp)
+ − 320
done
+ − 321
+ − 322
lemma supp_Abs:
+ − 323
fixes x::"'a::fs"
+ − 324
shows "supp (Abs as x) = (supp x) - as"
+ − 325
apply(rule_tac subset_antisym)
+ − 326
apply(rule supp_Abs_subset2)
+ − 327
apply(rule supp_Abs_subset1)
+ − 328
done
+ − 329
+ − 330
instance abs :: (fs) fs
+ − 331
apply(default)
+ − 332
apply(induct_tac x rule: abs_induct)
+ − 333
apply(simp add: supp_Abs)
+ − 334
apply(simp add: finite_supp)
+ − 335
done
+ − 336
+ − 337
lemma Abs_fresh_iff:
+ − 338
fixes x::"'a::fs"
+ − 339
shows "a \<sharp> Abs bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"
+ − 340
apply(simp add: fresh_def)
+ − 341
apply(simp add: supp_Abs)
+ − 342
apply(auto)
+ − 343
done
+ − 344
+ − 345
lemma Abs_eq_iff:
+ − 346
shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"
+ − 347
by (lifting alpha_abs.simps(1))
+ − 348
+ − 349
+ − 350
+ − 351
(*
+ − 352
below is a construction site for showing that in the
+ − 353
single-binder case, the old and new alpha equivalence
+ − 354
coincide
+ − 355
*)
+ − 356
+ − 357
fun
+ − 358
alpha1
+ − 359
where
+ − 360
"alpha1 (a, x) (b, y) \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)"
+ − 361
+ − 362
notation
+ − 363
alpha1 ("_ \<approx>abs1 _")
+ − 364
1460
+ − 365
fun
+ − 366
alpha2
+ − 367
where
+ − 368
"alpha2 (a, x) (b, y) \<longleftrightarrow> (\<exists>c. c \<sharp> (a,b,x,y) \<and> ((c \<rightleftharpoons> a) \<bullet> x) = ((c \<rightleftharpoons> b) \<bullet> y))"
+ − 369
+ − 370
notation
+ − 371
alpha2 ("_ \<approx>abs2 _")
+ − 372
+ − 373
lemma alpha_old_new:
1440
+ − 374
assumes a: "(a, x) \<approx>abs1 (b, y)" "sort_of a = sort_of b"
+ − 375
shows "({a}, x) \<approx>abs ({b}, y)"
+ − 376
using a
+ − 377
apply(simp)
+ − 378
apply(erule disjE)
+ − 379
apply(simp)
+ − 380
apply(rule exI)
+ − 381
apply(rule alpha_gen_refl)
+ − 382
apply(simp)
+ − 383
apply(rule_tac x="(a \<rightleftharpoons> b)" in exI)
+ − 384
apply(simp add: alpha_gen)
+ − 385
apply(simp add: fresh_def)
+ − 386
apply(rule conjI)
1460
+ − 387
apply(rule_tac ?p1="(a \<rightleftharpoons> b)" in permute_eq_iff[THEN iffD1])
1440
+ − 388
apply(rule trans)
+ − 389
apply(simp add: Diff_eqvt supp_eqvt)
+ − 390
apply(subst swap_set_not_in)
+ − 391
back
+ − 392
apply(simp)
+ − 393
apply(simp)
+ − 394
apply(simp add: permute_set_eq)
1465
+ − 395
apply(rule conjI)
1460
+ − 396
apply(rule_tac ?p1="(a \<rightleftharpoons> b)" in fresh_star_permute_iff[THEN iffD1])
1440
+ − 397
apply(simp add: permute_self)
+ − 398
apply(simp add: Diff_eqvt supp_eqvt)
+ − 399
apply(simp add: permute_set_eq)
+ − 400
apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}")
+ − 401
apply(simp add: fresh_star_def fresh_def)
+ − 402
apply(blast)
+ − 403
apply(simp add: supp_swap)
1465
+ − 404
apply(simp add: eqvts)
1440
+ − 405
done
+ − 406
+ − 407
lemma perm_zero:
+ − 408
assumes a: "\<forall>x::atom. p \<bullet> x = x"
+ − 409
shows "p = 0"
+ − 410
using a
+ − 411
by (simp add: expand_perm_eq)
+ − 412
+ − 413
fun
+ − 414
add_perm
+ − 415
where
+ − 416
"add_perm [] = 0"
+ − 417
| "add_perm ((a, b) # xs) = (a \<rightleftharpoons> b) + add_perm xs"
+ − 418
+ − 419
fun
+ − 420
elem_perm
+ − 421
where
+ − 422
"elem_perm [] = {}"
+ − 423
| "elem_perm ((a, b) # xs) = {a, b} \<union> elem_perm xs"
+ − 424
+ − 425
+ − 426
lemma add_perm_apend:
+ − 427
shows "add_perm (xs @ ys) = add_perm xs + add_perm ys"
+ − 428
apply(induct xs arbitrary: ys)
+ − 429
apply(auto simp add: add_assoc)
+ − 430
done
+ − 431
+ − 432
lemma perm_list_exists:
+ − 433
fixes p::perm
+ − 434
shows "\<exists>xs. p = add_perm xs \<and> supp xs \<subseteq> supp p"
+ − 435
apply(induct p taking: "\<lambda>p::perm. card (supp p)" rule: measure_induct)
+ − 436
apply(rename_tac p)
+ − 437
apply(case_tac "supp p = {}")
+ − 438
apply(simp)
+ − 439
apply(simp add: supp_perm)
+ − 440
apply(drule perm_zero)
+ − 441
apply(simp)
+ − 442
apply(rule_tac x="[]" in exI)
+ − 443
apply(simp add: supp_Nil)
+ − 444
apply(subgoal_tac "\<exists>x. x \<in> supp p")
+ − 445
defer
+ − 446
apply(auto)[1]
+ − 447
apply(erule exE)
+ − 448
apply(drule_tac x="p + (((- p) \<bullet> x) \<rightleftharpoons> x)" in spec)
+ − 449
apply(drule mp)
+ − 450
defer
+ − 451
apply(erule exE)
+ − 452
apply(rule_tac x="xs @ [((- p) \<bullet> x, x)]" in exI)
+ − 453
apply(simp add: add_perm_apend)
+ − 454
apply(erule conjE)
+ − 455
apply(drule sym)
+ − 456
apply(simp)
+ − 457
apply(simp add: expand_perm_eq)
+ − 458
apply(simp add: supp_append)
+ − 459
apply(simp add: supp_perm supp_Cons supp_Nil supp_Pair supp_atom)
+ − 460
apply(rule conjI)
+ − 461
prefer 2
+ − 462
apply(auto)[1]
+ − 463
apply (metis left_minus minus_unique permute_atom_def_raw permute_minus_cancel(2))
+ − 464
defer
+ − 465
apply(rule psubset_card_mono)
+ − 466
apply(simp add: finite_supp)
+ − 467
apply(rule psubsetI)
+ − 468
defer
+ − 469
apply(subgoal_tac "x \<notin> supp (p + (- p \<bullet> x \<rightleftharpoons> x))")
+ − 470
apply(blast)
+ − 471
apply(simp add: supp_perm)
+ − 472
defer
+ − 473
apply(auto simp add: supp_perm)[1]
+ − 474
apply(case_tac "x = xa")
+ − 475
apply(simp)
+ − 476
apply(case_tac "((- p) \<bullet> x) = xa")
+ − 477
apply(simp)
+ − 478
apply(case_tac "sort_of xa = sort_of x")
+ − 479
apply(simp)
+ − 480
apply(auto)[1]
+ − 481
apply(simp)
+ − 482
apply(simp)
+ − 483
apply(subgoal_tac "{a. p \<bullet> (- p \<bullet> x \<rightleftharpoons> x) \<bullet> a \<noteq> a} \<subseteq> {a. p \<bullet> a \<noteq> a}")
+ − 484
apply(blast)
+ − 485
apply(auto simp add: supp_perm)[1]
+ − 486
apply(case_tac "x = xa")
+ − 487
apply(simp)
+ − 488
apply(case_tac "((- p) \<bullet> x) = xa")
+ − 489
apply(simp)
+ − 490
apply(case_tac "sort_of xa = sort_of x")
+ − 491
apply(simp)
+ − 492
apply(auto)[1]
+ − 493
apply(simp)
+ − 494
apply(simp)
+ − 495
done
+ − 496
+ − 497
lemma tt0:
+ − 498
fixes p::perm
+ − 499
shows "(supp x) \<sharp>* p \<Longrightarrow> \<forall>a \<in> supp p. a \<sharp> x"
+ − 500
apply(auto simp add: fresh_star_def supp_perm fresh_def)
+ − 501
done
+ − 502
+ − 503
lemma uu0:
+ − 504
shows "(\<forall>a \<in> elem_perm xs. a \<sharp> x) \<Longrightarrow> (add_perm xs \<bullet> x) = x"
+ − 505
apply(induct xs rule: add_perm.induct)
+ − 506
apply(simp)
+ − 507
apply(simp add: swap_fresh_fresh)
+ − 508
done
+ − 509
+ − 510
lemma yy0:
+ − 511
fixes xs::"(atom \<times> atom) list"
+ − 512
shows "supp xs = elem_perm xs"
+ − 513
apply(induct xs rule: elem_perm.induct)
+ − 514
apply(auto simp add: supp_Nil supp_Cons supp_Pair supp_atom)
+ − 515
done
+ − 516
+ − 517
lemma tt1:
+ − 518
shows "(supp x) \<sharp>* p \<Longrightarrow> p \<bullet> x = x"
+ − 519
apply(drule tt0)
+ − 520
apply(subgoal_tac "\<exists>xs. p = add_perm xs \<and> supp xs \<subseteq> supp p")
+ − 521
prefer 2
+ − 522
apply(rule perm_list_exists)
+ − 523
apply(erule exE)
+ − 524
apply(simp only: yy0)
+ − 525
apply(rule uu0)
+ − 526
apply(auto)
+ − 527
done
+ − 528
+ − 529
+ − 530
lemma perm_induct_test:
+ − 531
fixes P :: "perm => bool"
+ − 532
assumes fin: "finite (supp p)"
+ − 533
assumes zero: "P 0"
+ − 534
assumes swap: "\<And>a b. \<lbrakk>sort_of a = sort_of b; a \<noteq> b\<rbrakk> \<Longrightarrow> P (a \<rightleftharpoons> b)"
+ − 535
assumes plus: "\<And>p1 p2. \<lbrakk>supp p1 \<inter> supp p2 = {}; P p1; P p2\<rbrakk> \<Longrightarrow> P (p1 + p2)"
+ − 536
shows "P p"
+ − 537
using fin
+ − 538
apply(induct F\<equiv>"supp p" arbitrary: p rule: finite_induct)
+ − 539
apply(simp add: supp_perm)
+ − 540
apply(drule perm_zero)
+ − 541
apply(simp add: zero)
+ − 542
apply(rotate_tac 3)
+ − 543
oops
1465
+ − 544
+ − 545
lemma ii:
+ − 546
assumes "\<forall>x \<in> A. p \<bullet> x = x"
+ − 547
shows "p \<bullet> A = A"
+ − 548
using assms
+ − 549
apply(auto)
+ − 550
apply (metis Collect_def Collect_mem_eq Int_absorb assms eqvt_bound inf_Int_eq mem_def mem_permute_iff)
+ − 551
apply (metis Collect_def Collect_mem_eq Int_absorb assms eqvt_apply eqvt_bound eqvt_lambda inf_Int_eq mem_def mem_permute_iff permute_minus_cancel(2) permute_pure)
+ − 552
done
+ − 553
+ − 554
+ − 555
+ − 556
lemma alpha_abs_Pair:
+ − 557
shows "(bs, (x1, x2)) \<approx>gen (\<lambda>(x1,x2) (y1,y2). x1=y1 \<and> x2=y2) (\<lambda>(x,y). supp x \<union> supp y) p (cs, (y1, y2))
+ − 558
\<longleftrightarrow> ((bs, x1) \<approx>gen (op=) supp p (cs, y1) \<and> (bs, x2) \<approx>gen (op=) supp p (cs, y2))"
+ − 559
apply(simp add: alpha_gen)
+ − 560
apply(simp add: fresh_star_def)
+ − 561
apply(simp add: ball_Un Un_Diff)
+ − 562
apply(rule iffI)
+ − 563
apply(simp)
+ − 564
defer
+ − 565
apply(simp)
+ − 566
apply(rule conjI)
+ − 567
apply(clarify)
+ − 568
apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric])
+ − 569
apply(rule sym)
+ − 570
apply(rule ii)
+ − 571
apply(simp add: fresh_def supp_perm)
+ − 572
apply(clarify)
+ − 573
apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric])
+ − 574
apply(simp add: fresh_def supp_perm)
+ − 575
apply(rule sym)
+ − 576
apply(rule ii)
+ − 577
apply(simp)
+ − 578
done
+ − 579
1440
+ − 580
+ − 581
lemma yy:
+ − 582
assumes "S1 - {x} = S2 - {x}" "x \<in> S1" "x \<in> S2"
+ − 583
shows "S1 = S2"
+ − 584
using assms
+ − 585
apply (metis insert_Diff_single insert_absorb)
+ − 586
done
+ − 587
+ − 588
lemma kk:
+ − 589
assumes a: "p \<bullet> x = y"
+ − 590
shows "\<forall>a \<in> supp x. (p \<bullet> a) \<in> supp y"
+ − 591
using a
+ − 592
apply(auto)
+ − 593
apply(rule_tac p="- p" in permute_boolI)
+ − 594
apply(simp add: mem_eqvt supp_eqvt)
+ − 595
done
+ − 596
+ − 597
lemma ww:
+ − 598
assumes "a \<notin> supp x" "b \<in> supp x" "a \<noteq> b" "sort_of a = sort_of b"
+ − 599
shows "((a \<rightleftharpoons> b) \<bullet> x) \<noteq> x"
+ − 600
apply(subgoal_tac "(supp x) supports x")
+ − 601
apply(simp add: supports_def)
+ − 602
using assms
+ − 603
apply -
+ − 604
apply(drule_tac x="a" in spec)
+ − 605
defer
+ − 606
apply(rule supp_supports)
+ − 607
apply(auto)
+ − 608
apply(rotate_tac 1)
+ − 609
apply(drule_tac p="(a \<rightleftharpoons> b)" in permute_boolE)
+ − 610
apply(simp add: mem_eqvt supp_eqvt)
+ − 611
done
+ − 612
+ − 613
lemma alpha_abs_sym:
+ − 614
assumes a: "({a}, x) \<approx>abs ({b}, y)"
+ − 615
shows "({b}, y) \<approx>abs ({a}, x)"
+ − 616
using a
+ − 617
apply(simp)
+ − 618
apply(erule exE)
+ − 619
apply(rule_tac x="- p" in exI)
+ − 620
apply(simp add: alpha_gen)
+ − 621
apply(simp add: fresh_star_def fresh_minus_perm)
+ − 622
apply (metis permute_minus_cancel(2))
+ − 623
done
+ − 624
+ − 625
lemma alpha_abs_trans:
+ − 626
assumes a: "({a1}, x1) \<approx>abs ({a2}, x2)"
+ − 627
assumes b: "({a2}, x2) \<approx>abs ({a3}, x3)"
+ − 628
shows "({a1}, x1) \<approx>abs ({a3}, x3)"
+ − 629
using a b
+ − 630
apply(simp)
+ − 631
apply(erule exE)+
+ − 632
apply(rule_tac x="pa + p" in exI)
+ − 633
apply(simp add: alpha_gen)
+ − 634
apply(simp add: fresh_star_def fresh_plus_perm)
+ − 635
done
+ − 636
+ − 637
lemma alpha_equal:
+ − 638
assumes a: "({a}, x) \<approx>abs ({a}, y)"
+ − 639
shows "(a, x) \<approx>abs1 (a, y)"
+ − 640
using a
+ − 641
apply(simp)
+ − 642
apply(erule exE)
+ − 643
apply(simp add: alpha_gen)
+ − 644
apply(erule conjE)+
+ − 645
apply(case_tac "a \<notin> supp x")
+ − 646
apply(simp)
+ − 647
apply(subgoal_tac "supp x \<sharp>* p")
+ − 648
apply(drule tt1)
+ − 649
apply(simp)
+ − 650
apply(simp)
+ − 651
apply(simp)
+ − 652
apply(case_tac "a \<notin> supp y")
+ − 653
apply(simp)
+ − 654
apply(drule tt1)
+ − 655
apply(clarify)
+ − 656
apply(simp (no_asm_use))
+ − 657
apply(simp)
+ − 658
apply(simp)
+ − 659
apply(drule yy)
+ − 660
apply(simp)
+ − 661
apply(simp)
+ − 662
apply(simp)
+ − 663
apply(case_tac "a \<sharp> p")
+ − 664
apply(subgoal_tac "supp y \<sharp>* p")
+ − 665
apply(drule tt1)
+ − 666
apply(clarify)
+ − 667
apply(simp (no_asm_use))
+ − 668
apply(metis)
+ − 669
apply(auto simp add: fresh_star_def)[1]
+ − 670
apply(frule_tac kk)
+ − 671
apply(drule_tac x="a" in bspec)
+ − 672
apply(simp)
+ − 673
apply(simp add: fresh_def)
+ − 674
apply(simp add: supp_perm)
+ − 675
apply(subgoal_tac "((p \<bullet> a) \<sharp> p)")
+ − 676
apply(simp add: fresh_def supp_perm)
+ − 677
apply(simp add: fresh_star_def)
+ − 678
done
+ − 679
+ − 680
lemma alpha_unequal:
+ − 681
assumes a: "({a}, x) \<approx>abs ({b}, y)" "sort_of a = sort_of b" "a \<noteq> b"
+ − 682
shows "(a, x) \<approx>abs1 (b, y)"
+ − 683
using a
+ − 684
apply -
+ − 685
apply(subgoal_tac "a \<notin> supp x - {a}")
+ − 686
apply(subgoal_tac "b \<notin> supp x - {a}")
+ − 687
defer
+ − 688
apply(simp add: alpha_gen)
+ − 689
apply(simp)
+ − 690
apply(drule_tac alpha_abs_swap)
+ − 691
apply(assumption)
+ − 692
apply(simp only: insert_eqvt empty_eqvt swap_atom_simps)
+ − 693
apply(drule alpha_abs_sym)
+ − 694
apply(rotate_tac 4)
+ − 695
apply(drule_tac alpha_abs_trans)
+ − 696
apply(assumption)
+ − 697
apply(drule alpha_equal)
+ − 698
apply(simp)
+ − 699
apply(rule_tac p="(a \<rightleftharpoons> b)" in permute_boolI)
+ − 700
apply(simp add: fresh_eqvt)
+ − 701
apply(simp add: fresh_def)
+ − 702
done
+ − 703
+ − 704
lemma alpha_new_old:
+ − 705
assumes a: "({a}, x) \<approx>abs ({b}, y)" "sort_of a = sort_of b"
+ − 706
shows "(a, x) \<approx>abs1 (b, y)"
+ − 707
using a
+ − 708
apply(case_tac "a=b")
+ − 709
apply(simp only: alpha_equal)
+ − 710
apply(drule alpha_unequal)
+ − 711
apply(simp)
+ − 712
apply(simp)
+ − 713
apply(simp)
+ − 714
done
+ − 715
1460
+ − 716
fun
+ − 717
distinct_perms
+ − 718
where
+ − 719
"distinct_perms [] = True"
+ − 720
| "distinct_perms (p # ps) = (supp p \<inter> supp ps = {} \<and> distinct_perms ps)"
+ − 721
1440
+ − 722
(* support of concrete atom sets *)
+ − 723
+ − 724
lemma atom_eqvt_raw:
+ − 725
fixes p::"perm"
+ − 726
shows "(p \<bullet> atom) = atom"
+ − 727
by (simp add: expand_fun_eq permute_fun_def atom_eqvt)
+ − 728
+ − 729
lemma atom_image_cong:
+ − 730
shows "(atom ` X = atom ` Y) = (X = Y)"
+ − 731
apply(rule inj_image_eq_iff)
+ − 732
apply(simp add: inj_on_def)
+ − 733
done
+ − 734
+ − 735
lemma supp_atom_image:
+ − 736
fixes as::"'a::at_base set"
+ − 737
shows "supp (atom ` as) = supp as"
+ − 738
apply(simp add: supp_def)
+ − 739
apply(simp add: image_eqvt)
+ − 740
apply(simp add: atom_eqvt_raw)
+ − 741
apply(simp add: atom_image_cong)
+ − 742
done
+ − 743
1460
+ − 744
lemma swap_atom_image_fresh: "\<lbrakk>a \<sharp> atom ` (fn :: ('a :: at_base set)); b \<sharp> atom ` fn\<rbrakk> \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> fn = fn"
+ − 745
apply (simp add: fresh_def)
+ − 746
apply (simp add: supp_atom_image)
+ − 747
apply (fold fresh_def)
+ − 748
apply (simp add: swap_fresh_fresh)
1440
+ − 749
done
+ − 750
1467
+ − 751
(* TODO: The following lemmas can be moved somewhere... *)
+ − 752
lemma split_rsp2[quot_respect]: "((R1 ===> R2 ===> prod_rel R1 R2 ===> op =) ===>
+ − 753
prod_rel R1 R2 ===> prod_rel R1 R2 ===> op =) split split"
+ − 754
by auto
+ − 755
+ − 756
lemma split_prs2[quot_preserve]:
+ − 757
assumes q1: "Quotient R1 Abs1 Rep1"
+ − 758
and q2: "Quotient R2 Abs2 Rep2"
+ − 759
shows "((Abs1 ---> Abs2 ---> prod_fun Abs1 Abs2 ---> id) ---> prod_fun Rep1 Rep2 ---> prod_fun Rep1 Rep2 ---> id) split = split"
+ − 760
by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
+ − 761
+ − 762
lemma alpha_gen2:
+ − 763
"(bs, x1, x2) \<approx>gen (\<lambda>(x1, y1) (x2, y2). R1 x1 x2 \<and> R2 y1 y2) (\<lambda>(a, b). f1 a \<union> f2 b) pi (cs, y1, y2) =
1470
+ − 764
(f1 x1 \<union> f2 x2 - bs = f1 y1 \<union> f2 y2 - cs \<and> (f1 x1 \<union> f2 x2 - bs) \<sharp>* pi \<and> R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2
+ − 765
\<and> pi \<bullet> bs = cs)"
1467
+ − 766
by (simp add: alpha_gen)
+ − 767
1440
+ − 768
end
+ − 769