1657
+ − 1
theory Abs_equiv
+ − 2
imports Abs
+ − 3
begin
+ − 4
+ − 5
(*
+ − 6
below is a construction site for showing that in the
+ − 7
single-binder case, the old and new alpha equivalence
+ − 8
coincide
+ − 9
*)
+ − 10
+ − 11
fun
+ − 12
alpha1
+ − 13
where
+ − 14
"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)"
+ − 15
+ − 16
notation
+ − 17
alpha1 ("_ \<approx>abs1 _")
+ − 18
+ − 19
fun
+ − 20
alpha2
+ − 21
where
+ − 22
"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))"
+ − 23
+ − 24
notation
+ − 25
alpha2 ("_ \<approx>abs2 _")
+ − 26
+ − 27
lemma alpha_old_new:
+ − 28
assumes a: "(a, x) \<approx>abs1 (b, y)" "sort_of a = sort_of b"
+ − 29
shows "({a}, x) \<approx>abs ({b}, y)"
+ − 30
using a
+ − 31
apply(simp)
+ − 32
apply(erule disjE)
+ − 33
apply(simp)
+ − 34
apply(rule exI)
+ − 35
apply(rule alpha_gen_refl)
+ − 36
apply(simp)
+ − 37
apply(rule_tac x="(a \<rightleftharpoons> b)" in exI)
+ − 38
apply(simp add: alpha_gen)
+ − 39
apply(simp add: fresh_def)
+ − 40
apply(rule conjI)
+ − 41
apply(rule_tac ?p1="(a \<rightleftharpoons> b)" in permute_eq_iff[THEN iffD1])
+ − 42
apply(rule trans)
+ − 43
apply(simp add: Diff_eqvt supp_eqvt)
+ − 44
apply(subst swap_set_not_in)
+ − 45
back
+ − 46
apply(simp)
+ − 47
apply(simp)
+ − 48
apply(simp add: permute_set_eq)
+ − 49
apply(rule conjI)
+ − 50
apply(rule_tac ?p1="(a \<rightleftharpoons> b)" in fresh_star_permute_iff[THEN iffD1])
+ − 51
apply(simp add: permute_self)
+ − 52
apply(simp add: Diff_eqvt supp_eqvt)
+ − 53
apply(simp add: permute_set_eq)
+ − 54
apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}")
+ − 55
apply(simp add: fresh_star_def fresh_def)
+ − 56
apply(blast)
+ − 57
apply(simp add: supp_swap)
+ − 58
apply(simp add: eqvts)
+ − 59
done
+ − 60
+ − 61
+ − 62
lemma perm_induct_test:
+ − 63
fixes P :: "perm => bool"
+ − 64
assumes fin: "finite (supp p)"
+ − 65
assumes zero: "P 0"
+ − 66
assumes swap: "\<And>a b. \<lbrakk>sort_of a = sort_of b; a \<noteq> b\<rbrakk> \<Longrightarrow> P (a \<rightleftharpoons> b)"
+ − 67
assumes plus: "\<And>p1 p2. \<lbrakk>supp p1 \<inter> supp p2 = {}; P p1; P p2\<rbrakk> \<Longrightarrow> P (p1 + p2)"
+ − 68
shows "P p"
+ − 69
using fin
+ − 70
apply(induct F\<equiv>"supp p" arbitrary: p rule: finite_induct)
+ − 71
oops
+ − 72
+ − 73
lemma ii:
+ − 74
assumes "\<forall>x \<in> A. p \<bullet> x = x"
+ − 75
shows "p \<bullet> A = A"
+ − 76
using assms
+ − 77
apply(auto)
+ − 78
apply (metis Collect_def Collect_mem_eq Int_absorb assms eqvt_bound inf_Int_eq mem_def mem_permute_iff)
+ − 79
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)
+ − 80
done
+ − 81
+ − 82
+ − 83
+ − 84
lemma alpha_abs_Pair:
+ − 85
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))
+ − 86
\<longleftrightarrow> ((bs, x1) \<approx>gen (op=) supp p (cs, y1) \<and> (bs, x2) \<approx>gen (op=) supp p (cs, y2))"
+ − 87
apply(simp add: alpha_gen)
+ − 88
apply(simp add: fresh_star_def)
+ − 89
apply(simp add: ball_Un Un_Diff)
+ − 90
apply(rule iffI)
+ − 91
apply(simp)
+ − 92
defer
+ − 93
apply(simp)
+ − 94
apply(rule conjI)
+ − 95
apply(clarify)
+ − 96
apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric])
+ − 97
apply(rule sym)
+ − 98
apply(rule ii)
+ − 99
apply(simp add: fresh_def supp_perm)
+ − 100
apply(clarify)
+ − 101
apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric])
+ − 102
apply(simp add: fresh_def supp_perm)
+ − 103
apply(rule sym)
+ − 104
apply(rule ii)
+ − 105
apply(simp)
+ − 106
done
+ − 107
+ − 108
+ − 109
lemma yy:
+ − 110
assumes "S1 - {x} = S2 - {x}" "x \<in> S1" "x \<in> S2"
+ − 111
shows "S1 = S2"
+ − 112
using assms
+ − 113
apply (metis insert_Diff_single insert_absorb)
+ − 114
done
+ − 115
+ − 116
lemma kk:
+ − 117
assumes a: "p \<bullet> x = y"
+ − 118
shows "\<forall>a \<in> supp x. (p \<bullet> a) \<in> supp y"
+ − 119
using a
+ − 120
apply(auto)
+ − 121
apply(rule_tac p="- p" in permute_boolE)
+ − 122
apply(simp add: mem_eqvt supp_eqvt)
+ − 123
done
+ − 124
+ − 125
lemma ww:
+ − 126
assumes "a \<notin> supp x" "b \<in> supp x" "a \<noteq> b" "sort_of a = sort_of b"
+ − 127
shows "((a \<rightleftharpoons> b) \<bullet> x) \<noteq> x"
+ − 128
apply(subgoal_tac "(supp x) supports x")
+ − 129
apply(simp add: supports_def)
+ − 130
using assms
+ − 131
apply -
+ − 132
apply(drule_tac x="a" in spec)
+ − 133
defer
+ − 134
apply(rule supp_supports)
+ − 135
apply(auto)
+ − 136
apply(rotate_tac 1)
+ − 137
apply(drule_tac p="(a \<rightleftharpoons> b)" in permute_boolI)
+ − 138
apply(simp add: mem_eqvt supp_eqvt)
+ − 139
done
+ − 140
+ − 141
lemma alpha_abs_sym:
+ − 142
assumes a: "({a}, x) \<approx>abs ({b}, y)"
+ − 143
shows "({b}, y) \<approx>abs ({a}, x)"
+ − 144
using a
+ − 145
apply(simp)
+ − 146
apply(erule exE)
+ − 147
apply(rule_tac x="- p" in exI)
+ − 148
apply(simp add: alpha_gen)
+ − 149
apply(simp add: fresh_star_def fresh_minus_perm)
+ − 150
apply (metis permute_minus_cancel(2))
+ − 151
done
+ − 152
+ − 153
lemma alpha_abs_trans:
+ − 154
assumes a: "({a1}, x1) \<approx>abs ({a2}, x2)"
+ − 155
assumes b: "({a2}, x2) \<approx>abs ({a3}, x3)"
+ − 156
shows "({a1}, x1) \<approx>abs ({a3}, x3)"
+ − 157
using a b
+ − 158
apply(simp)
+ − 159
apply(erule exE)+
+ − 160
apply(rule_tac x="pa + p" in exI)
+ − 161
apply(simp add: alpha_gen)
+ − 162
apply(simp add: fresh_star_def fresh_plus_perm)
+ − 163
done
+ − 164
+ − 165
lemma alpha_equal:
+ − 166
assumes a: "({a}, x) \<approx>abs ({a}, y)"
+ − 167
shows "(a, x) \<approx>abs1 (a, y)"
+ − 168
using a
+ − 169
apply(simp)
+ − 170
apply(erule exE)
+ − 171
apply(simp add: alpha_gen)
+ − 172
apply(erule conjE)+
+ − 173
apply(case_tac "a \<notin> supp x")
+ − 174
apply(simp)
+ − 175
apply(subgoal_tac "supp x \<sharp>* p")
+ − 176
apply(drule supp_perm_eq)
+ − 177
apply(simp)
+ − 178
apply(simp)
+ − 179
apply(simp)
+ − 180
apply(case_tac "a \<notin> supp y")
+ − 181
apply(simp)
+ − 182
apply(drule supp_perm_eq)
+ − 183
apply(clarify)
+ − 184
apply(simp (no_asm_use))
+ − 185
apply(simp)
+ − 186
apply(simp)
+ − 187
apply(drule yy)
+ − 188
apply(simp)
+ − 189
apply(simp)
+ − 190
apply(simp)
+ − 191
apply(case_tac "a \<sharp> p")
+ − 192
apply(subgoal_tac "supp y \<sharp>* p")
+ − 193
apply(drule supp_perm_eq)
+ − 194
apply(clarify)
+ − 195
apply(simp (no_asm_use))
+ − 196
apply(metis)
+ − 197
apply(auto simp add: fresh_star_def)[1]
+ − 198
apply(frule_tac kk)
+ − 199
apply(drule_tac x="a" in bspec)
+ − 200
apply(simp)
+ − 201
apply(simp add: fresh_def)
+ − 202
apply(simp add: supp_perm)
+ − 203
apply(subgoal_tac "((p \<bullet> a) \<sharp> p)")
+ − 204
apply(simp add: fresh_def supp_perm)
+ − 205
apply(simp add: fresh_star_def)
+ − 206
done
+ − 207
+ − 208
lemma alpha_unequal:
+ − 209
assumes a: "({a}, x) \<approx>abs ({b}, y)" "sort_of a = sort_of b" "a \<noteq> b"
+ − 210
shows "(a, x) \<approx>abs1 (b, y)"
+ − 211
using a
+ − 212
apply -
+ − 213
apply(subgoal_tac "a \<notin> supp x - {a}")
+ − 214
apply(subgoal_tac "b \<notin> supp x - {a}")
+ − 215
defer
+ − 216
apply(simp add: alpha_gen)
+ − 217
apply(simp)
+ − 218
apply(drule_tac abs_swap1)
+ − 219
apply(assumption)
+ − 220
apply(simp only: insert_eqvt empty_eqvt swap_atom_simps)
+ − 221
apply(simp only: abs_eq_iff)
+ − 222
apply(drule alphas_abs_sym)
+ − 223
apply(rotate_tac 4)
+ − 224
apply(drule_tac alpha_abs_trans)
+ − 225
apply(assumption)
+ − 226
apply(drule alpha_equal)
+ − 227
apply(rule_tac p="(a \<rightleftharpoons> b)" in permute_boolE)
+ − 228
apply(simp add: fresh_eqvt)
+ − 229
apply(simp add: fresh_def)
+ − 230
done
+ − 231
+ − 232
lemma alpha_new_old:
+ − 233
assumes a: "({a}, x) \<approx>abs ({b}, y)" "sort_of a = sort_of b"
+ − 234
shows "(a, x) \<approx>abs1 (b, y)"
+ − 235
using a
+ − 236
apply(case_tac "a=b")
+ − 237
apply(simp only: alpha_equal)
+ − 238
apply(drule alpha_unequal)
+ − 239
apply(simp)
+ − 240
apply(simp)
+ − 241
apply(simp)
+ − 242
done
+ − 243
+ − 244
end