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