2568
8193bbaa07fe
merged Nominal-General directory into Nominal; renamed Abs.thy to Nominal2_Abs.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1 theory Nominal2_Abs
8193bbaa07fe
merged Nominal-General directory into Nominal; renamed Abs.thy to Nominal2_Abs.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 2 imports "Nominal2_Base"
2635
+ − 3 "~~/src/HOL/Quotient"
+ − 4 "~~/src/HOL/Library/Quotient_List"
+ − 5 "~~/src/HOL/Library/Quotient_Product"
1440
+ − 6 begin
+ − 7
2473
+ − 8
+ − 9 section {* Abstractions *}
+ − 10
1440
+ − 11 fun
3214
+ − 12 alpha_set
1440
+ − 13 where
2469
+ − 14 alpha_set[simp del]:
3199
+ − 15 "alpha_set (bs, x) R f p (cs, y) \<longleftrightarrow>
1465
+ − 16 f x - bs = f y - cs \<and>
3199
+ − 17 (f x - bs) \<sharp>* p \<and>
+ − 18 R (p \<bullet> x) y \<and>
+ − 19 p \<bullet> bs = cs"
1440
+ − 20
1557
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 21 fun
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 22 alpha_res
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 23 where
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 24 alpha_res[simp del]:
3199
+ − 25 "alpha_res (bs, x) R f p (cs, y) \<longleftrightarrow>
1557
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 26 f x - bs = f y - cs \<and>
3199
+ − 27 (f x - bs) \<sharp>* p \<and>
+ − 28 R (p \<bullet> x) y"
1440
+ − 29
1557
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 30 fun
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 31 alpha_lst
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 32 where
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 33 alpha_lst[simp del]:
3199
+ − 34 "alpha_lst (bs, x) R f p (cs, y) \<longleftrightarrow>
1557
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 = f y - set cs \<and>
3199
+ − 36 (f x - set bs) \<sharp>* p \<and>
+ − 37 R (p \<bullet> x) y \<and>
+ − 38 p \<bullet> bs = cs"
1557
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 39
2469
+ − 40 lemmas alphas = alpha_set.simps alpha_res.simps alpha_lst.simps
1557
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 41
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 42 notation
2469
+ − 43 alpha_set ("_ \<approx>set _ _ _ _" [100, 100, 100, 100, 100] 100) and
1557
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 44 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
+ − 45 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
+ − 46
2385
+ − 47 section {* Mono *}
+ − 48
1557
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 49 lemma [mono]:
2469
+ − 50 shows "R1 \<le> R2 \<Longrightarrow> alpha_set bs R1 \<le> alpha_set bs R2"
1557
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 51 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
+ − 52 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
+ − 53 by (case_tac [!] bs, case_tac [!] cs)
3224
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 54 (auto simp: le_fun_def le_bool_def alphas)
1440
+ − 55
2385
+ − 56 section {* Equivariance *}
+ − 57
+ − 58 lemma alpha_eqvt[eqvt]:
2469
+ − 59 shows "(bs, x) \<approx>set R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>set (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
2311
+ − 60 and "(bs, x) \<approx>res R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>res (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
+ − 61 and "(ds, x) \<approx>lst R f q (es, y) \<Longrightarrow> (p \<bullet> ds, p \<bullet> x) \<approx>lst (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> es, p \<bullet> y)"
+ − 62 unfolding alphas
+ − 63 unfolding permute_eqvt[symmetric]
+ − 64 unfolding set_eqvt[symmetric]
+ − 65 unfolding permute_fun_app_eq[symmetric]
+ − 66 unfolding Diff_eqvt[symmetric]
3004
+ − 67 unfolding eq_eqvt[symmetric]
+ − 68 unfolding fresh_star_eqvt[symmetric]
3199
+ − 69 by (auto simp only: permute_bool_def)
2385
+ − 70
+ − 71 section {* Equivalence *}
+ − 72
+ − 73 lemma alpha_refl:
2311
+ − 74 assumes a: "R x x"
2469
+ − 75 shows "(bs, x) \<approx>set R f 0 (bs, x)"
2311
+ − 76 and "(bs, x) \<approx>res R f 0 (bs, x)"
+ − 77 and "(cs, x) \<approx>lst R f 0 (cs, x)"
+ − 78 using a
+ − 79 unfolding alphas
+ − 80 unfolding fresh_star_def
+ − 81 by (simp_all add: fresh_zero_perm)
+ − 82
2385
+ − 83 lemma alpha_sym:
2311
+ − 84 assumes a: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x"
2469
+ − 85 shows "(bs, x) \<approx>set R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>set R f (- p) (bs, x)"
2311
+ − 86 and "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)"
+ − 87 and "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)"
+ − 88 unfolding alphas fresh_star_def
+ − 89 using a
3224
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 90 by (auto simp: fresh_minus_perm)
2311
+ − 91
2385
+ − 92 lemma alpha_trans:
+ − 93 assumes a: "\<lbrakk>R (p \<bullet> x) y; R (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((q + p) \<bullet> x) z"
2469
+ − 94 shows "\<lbrakk>(bs, x) \<approx>set R f p (cs, y); (cs, y) \<approx>set R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>set R f (q + p) (ds, z)"
2385
+ − 95 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)"
+ − 96 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)"
+ − 97 using a
+ − 98 unfolding alphas fresh_star_def
+ − 99 by (simp_all add: fresh_plus_perm)
+ − 100
+ − 101 lemma alpha_sym_eqvt:
2311
+ − 102 assumes a: "R (p \<bullet> x) y \<Longrightarrow> R y (p \<bullet> x)"
+ − 103 and b: "p \<bullet> R = R"
2469
+ − 104 shows "(bs, x) \<approx>set R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>set R f (- p) (bs, x)"
2311
+ − 105 and "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)"
2313
+ − 106 and "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)"
2385
+ − 107 apply(auto intro!: alpha_sym)
2313
+ − 108 apply(drule_tac [!] a)
+ − 109 apply(rule_tac [!] p="p" in permute_boolE)
3199
+ − 110 apply(simp_all add: b permute_self)
2313
+ − 111 done
2311
+ − 112
2469
+ − 113 lemma alpha_set_trans_eqvt:
+ − 114 assumes b: "(cs, y) \<approx>set R f q (ds, z)"
+ − 115 and a: "(bs, x) \<approx>set R f p (cs, y)"
2313
+ − 116 and d: "q \<bullet> R = R"
+ − 117 and c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"
2469
+ − 118 shows "(bs, x) \<approx>set R f (q + p) (ds, z)"
3199
+ − 119 apply(rule alpha_trans(1)[OF _ a b])
2313
+ − 120 apply(drule c)
+ − 121 apply(rule_tac p="q" in permute_boolE)
3199
+ − 122 apply(simp add: d permute_self)
2313
+ − 123 apply(rotate_tac -1)
+ − 124 apply(drule_tac p="q" in permute_boolI)
3199
+ − 125 apply(simp add: d permute_self permute_eqvt[symmetric])
2313
+ − 126 done
+ − 127
+ − 128 lemma alpha_res_trans_eqvt:
+ − 129 assumes b: "(cs, y) \<approx>res R f q (ds, z)"
+ − 130 and a: "(bs, x) \<approx>res R f p (cs, y)"
+ − 131 and d: "q \<bullet> R = R"
+ − 132 and c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"
+ − 133 shows "(bs, x) \<approx>res R f (q + p) (ds, z)"
3199
+ − 134 apply(rule alpha_trans(2)[OF _ a b])
2313
+ − 135 apply(drule c)
+ − 136 apply(rule_tac p="q" in permute_boolE)
3199
+ − 137 apply(simp add: d permute_self)
2313
+ − 138 apply(rotate_tac -1)
+ − 139 apply(drule_tac p="q" in permute_boolI)
3199
+ − 140 apply(simp add: d permute_self permute_eqvt[symmetric])
2313
+ − 141 done
+ − 142
+ − 143 lemma alpha_lst_trans_eqvt:
+ − 144 assumes b: "(cs, y) \<approx>lst R f q (ds, z)"
+ − 145 and a: "(bs, x) \<approx>lst R f p (cs, y)"
+ − 146 and d: "q \<bullet> R = R"
+ − 147 and c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"
+ − 148 shows "(bs, x) \<approx>lst R f (q + p) (ds, z)"
3199
+ − 149 apply(rule alpha_trans(3)[OF _ a b])
2313
+ − 150 apply(drule c)
+ − 151 apply(rule_tac p="q" in permute_boolE)
3199
+ − 152 apply(simp add: d permute_self)
2313
+ − 153 apply(rotate_tac -1)
+ − 154 apply(drule_tac p="q" in permute_boolI)
3199
+ − 155 apply(simp add: d permute_self permute_eqvt[symmetric])
2313
+ − 156 done
+ − 157
2469
+ − 158 lemmas alpha_trans_eqvt = alpha_set_trans_eqvt alpha_res_trans_eqvt alpha_lst_trans_eqvt
2313
+ − 159
2311
+ − 160
+ − 161 section {* General Abstractions *}
+ − 162
1440
+ − 163 fun
2469
+ − 164 alpha_abs_set
1440
+ − 165 where
1666
+ − 166 [simp del]:
2469
+ − 167 "alpha_abs_set (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op=) supp p (cs, y))"
1440
+ − 168
1657
+ − 169 fun
+ − 170 alpha_abs_lst
+ − 171 where
1666
+ − 172 [simp del]:
1657
+ − 173 "alpha_abs_lst (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>lst (op=) supp p (cs, y))"
+ − 174
+ − 175 fun
+ − 176 alpha_abs_res
+ − 177 where
1666
+ − 178 [simp del]:
1657
+ − 179 "alpha_abs_res (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op=) supp p (cs, y))"
+ − 180
1440
+ − 181 notation
2469
+ − 182 alpha_abs_set (infix "\<approx>abs'_set" 50) and
1666
+ − 183 alpha_abs_lst (infix "\<approx>abs'_lst" 50) and
+ − 184 alpha_abs_res (infix "\<approx>abs'_res" 50)
1657
+ − 185
2469
+ − 186 lemmas alphas_abs = alpha_abs_set.simps alpha_abs_res.simps alpha_abs_lst.simps
1657
+ − 187
2385
+ − 188
1657
+ − 189 lemma alphas_abs_refl:
2469
+ − 190 shows "(bs, x) \<approx>abs_set (bs, x)"
1657
+ − 191 and "(bs, x) \<approx>abs_res (bs, x)"
+ − 192 and "(cs, x) \<approx>abs_lst (cs, x)"
+ − 193 unfolding alphas_abs
+ − 194 unfolding alphas
+ − 195 unfolding fresh_star_def
+ − 196 by (rule_tac [!] x="0" in exI)
+ − 197 (simp_all add: fresh_zero_perm)
+ − 198
+ − 199 lemma alphas_abs_sym:
2469
+ − 200 shows "(bs, x) \<approx>abs_set (cs, y) \<Longrightarrow> (cs, y) \<approx>abs_set (bs, x)"
1657
+ − 201 and "(bs, x) \<approx>abs_res (cs, y) \<Longrightarrow> (cs, y) \<approx>abs_res (bs, x)"
+ − 202 and "(ds, x) \<approx>abs_lst (es, y) \<Longrightarrow> (es, y) \<approx>abs_lst (ds, x)"
+ − 203 unfolding alphas_abs
+ − 204 unfolding alphas
+ − 205 unfolding fresh_star_def
+ − 206 by (erule_tac [!] exE, rule_tac [!] x="-p" in exI)
3224
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 207 (auto simp: fresh_minus_perm)
1440
+ − 208
1657
+ − 209 lemma alphas_abs_trans:
2469
+ − 210 shows "\<lbrakk>(bs, x) \<approx>abs_set (cs, y); (cs, y) \<approx>abs_set (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>abs_set (ds, z)"
1657
+ − 211 and "\<lbrakk>(bs, x) \<approx>abs_res (cs, y); (cs, y) \<approx>abs_res (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>abs_res (ds, z)"
+ − 212 and "\<lbrakk>(es, x) \<approx>abs_lst (gs, y); (gs, y) \<approx>abs_lst (hs, z)\<rbrakk> \<Longrightarrow> (es, x) \<approx>abs_lst (hs, z)"
+ − 213 unfolding alphas_abs
+ − 214 unfolding alphas
+ − 215 unfolding fresh_star_def
+ − 216 apply(erule_tac [!] exE, erule_tac [!] exE)
+ − 217 apply(rule_tac [!] x="pa + p" in exI)
+ − 218 by (simp_all add: fresh_plus_perm)
+ − 219
+ − 220 lemma alphas_abs_eqvt:
2469
+ − 221 shows "(bs, x) \<approx>abs_set (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>abs_set (p \<bullet> cs, p \<bullet> y)"
1657
+ − 222 and "(bs, x) \<approx>abs_res (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>abs_res (p \<bullet> cs, p \<bullet> y)"
+ − 223 and "(ds, x) \<approx>abs_lst (es, y) \<Longrightarrow> (p \<bullet> ds, p \<bullet> x) \<approx>abs_lst (p \<bullet> es, p \<bullet> y)"
+ − 224 unfolding alphas_abs
+ − 225 unfolding alphas
+ − 226 unfolding set_eqvt[symmetric]
+ − 227 unfolding supp_eqvt[symmetric]
+ − 228 unfolding Diff_eqvt[symmetric]
+ − 229 apply(erule_tac [!] exE)
+ − 230 apply(rule_tac [!] x="p \<bullet> pa" in exI)
3183
313e6f2cdd89
added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 231 by (auto simp only: fresh_star_permute_iff permute_eqvt[symmetric])
1657
+ − 232
2668
+ − 233
+ − 234 section {* Strengthening the equivalence *}
+ − 235
+ − 236 lemma disjoint_right_eq:
+ − 237 assumes a: "A \<union> B1 = A \<union> B2"
+ − 238 and b: "A \<inter> B1 = {}" "A \<inter> B2 = {}"
+ − 239 shows "B1 = B2"
+ − 240 using a b
+ − 241 by (metis Int_Un_distrib2 Int_absorb2 Int_commute Un_upper2)
+ − 242
+ − 243 lemma supp_property_res:
+ − 244 assumes a: "(as, x) \<approx>res (op =) supp p (as', x')"
+ − 245 shows "p \<bullet> (supp x \<inter> as) = supp x' \<inter> as'"
+ − 246 proof -
+ − 247 from a have "(supp x - as) \<sharp>* p" by (auto simp only: alphas)
+ − 248 then have *: "p \<bullet> (supp x - as) = (supp x - as)"
+ − 249 by (simp add: atom_set_perm_eq)
+ − 250 have "(supp x' - as') \<union> (supp x' \<inter> as') = supp x'" by auto
+ − 251 also have "\<dots> = supp (p \<bullet> x)" using a by (simp add: alphas)
+ − 252 also have "\<dots> = p \<bullet> (supp x)" by (simp add: supp_eqvt)
+ − 253 also have "\<dots> = p \<bullet> ((supp x - as) \<union> (supp x \<inter> as))" by auto
+ − 254 also have "\<dots> = (p \<bullet> (supp x - as)) \<union> (p \<bullet> (supp x \<inter> as))" by (simp add: union_eqvt)
+ − 255 also have "\<dots> = (supp x - as) \<union> (p \<bullet> (supp x \<inter> as))" using * by simp
+ − 256 also have "\<dots> = (supp x' - as') \<union> (p \<bullet> (supp x \<inter> as))" using a by (simp add: alphas)
+ − 257 finally have "(supp x' - as') \<union> (supp x' \<inter> as') = (supp x' - as') \<union> (p \<bullet> (supp x \<inter> as))" .
+ − 258 moreover
+ − 259 have "(supp x' - as') \<inter> (supp x' \<inter> as') = {}" by auto
+ − 260 moreover
+ − 261 have "(supp x - as) \<inter> (supp x \<inter> as) = {}" by auto
+ − 262 then have "p \<bullet> ((supp x - as) \<inter> (supp x \<inter> as) = {})" by (simp add: permute_bool_def)
+ − 263 then have "(p \<bullet> (supp x - as)) \<inter> (p \<bullet> (supp x \<inter> as)) = {}" by (perm_simp) (simp)
+ − 264 then have "(supp x - as) \<inter> (p \<bullet> (supp x \<inter> as)) = {}" using * by simp
+ − 265 then have "(supp x' - as') \<inter> (p \<bullet> (supp x \<inter> as)) = {}" using a by (simp add: alphas)
+ − 266 ultimately show "p \<bullet> (supp x \<inter> as) = supp x' \<inter> as'"
+ − 267 by (auto dest: disjoint_right_eq)
2712
+ − 268 qed
2668
+ − 269
2674
+ − 270 lemma alpha_abs_res_stronger1_aux:
2671
+ − 271 assumes asm: "(as, x) \<approx>res (op =) supp p' (as', x')"
2669
1d1772a89026
the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 272 shows "\<exists>p. (as, x) \<approx>res (op =) supp p (as', x') \<and> supp p \<subseteq> (supp x \<inter> as) \<union> (supp x' \<inter> as')"
1d1772a89026
the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 273 proof -
1d1772a89026
the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 274 from asm have 0: "(supp x - as) \<sharp>* p'" by (auto simp only: alphas)
1d1772a89026
the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 275 then have #: "p' \<bullet> (supp x - as) = (supp x - as)"
1d1772a89026
the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 276 by (simp add: atom_set_perm_eq)
2673
+ − 277 obtain p where *: "\<forall>b \<in> supp x. p \<bullet> b = p' \<bullet> b" and **: "supp p \<subseteq> supp x \<union> p' \<bullet> supp x"
+ − 278 using set_renaming_perm2 by blast
2669
1d1772a89026
the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 279 from * have a: "p \<bullet> x = p' \<bullet> x" using supp_perm_perm_eq by auto
1d1772a89026
the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 280 from 0 have 1: "(supp x - as) \<sharp>* p" using *
3224
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 281 by (auto simp: fresh_star_def fresh_perm)
2669
1d1772a89026
the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 282 then have 2: "(supp x - as) \<inter> supp p = {}"
3224
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 283 by (auto simp: fresh_star_def fresh_def)
2669
1d1772a89026
the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 284 have b: "supp x = (supp x - as) \<union> (supp x \<inter> as)" by auto
1d1772a89026
the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 285 have "supp p \<subseteq> supp x \<union> p' \<bullet> supp x" using ** by simp
1d1772a89026
the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 286 also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> (p' \<bullet> ((supp x - as) \<union> (supp x \<inter> as)))"
1d1772a89026
the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 287 using b by simp
1d1772a89026
the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 288 also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> ((p' \<bullet> (supp x - as)) \<union> (p' \<bullet> (supp x \<inter> as)))"
1d1772a89026
the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 289 by (simp add: union_eqvt)
1d1772a89026
the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 290 also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> (p' \<bullet> (supp x \<inter> as))"
1d1772a89026
the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 291 using # by auto
1d1772a89026
the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 292 also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> (supp x' \<inter> as')" using asm
1d1772a89026
the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 293 by (simp add: supp_property_res)
1d1772a89026
the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 294 finally have "supp p \<subseteq> (supp x - as) \<union> (supp x \<inter> as) \<union> (supp x' \<inter> as')" .
1d1772a89026
the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 295 then
1d1772a89026
the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 296 have "supp p \<subseteq> (supp x \<inter> as) \<union> (supp x' \<inter> as')" using 2 by auto
1d1772a89026
the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 297 moreover
1d1772a89026
the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 298 have "(as, x) \<approx>res (op =) supp p (as', x')" using asm 1 a by (simp add: alphas)
1d1772a89026
the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 299 ultimately
1d1772a89026
the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 300 show "\<exists>p. (as, x) \<approx>res (op =) supp p (as', x') \<and> supp p \<subseteq> (supp x \<inter> as) \<union> (supp x' \<inter> as')" by blast
1d1772a89026
the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 301 qed
1d1772a89026
the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 302
2712
+ − 303 lemma alpha_abs_res_minimal:
+ − 304 assumes asm: "(as, x) \<approx>res (op =) supp p (as', x')"
+ − 305 shows "(as \<inter> supp x, x) \<approx>res (op =) supp p (as' \<inter> supp x', x')"
3224
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 306 using asm unfolding alpha_res by (auto simp: Diff_Int)
2712
+ − 307
+ − 308 lemma alpha_abs_res_abs_set:
+ − 309 assumes asm: "(as, x) \<approx>res (op =) supp p (as', x')"
+ − 310 shows "(as \<inter> supp x, x) \<approx>set (op =) supp p (as' \<inter> supp x', x')"
+ − 311 proof -
+ − 312 have c: "p \<bullet> x = x'"
+ − 313 using alpha_abs_res_minimal[OF asm] unfolding alpha_res by clarify
+ − 314 then have a: "supp x - as \<inter> supp x = supp (p \<bullet> x) - as' \<inter> supp (p \<bullet> x)"
+ − 315 using alpha_abs_res_minimal[OF asm] by (simp add: alpha_res)
+ − 316 have b: "(supp x - as \<inter> supp x) \<sharp>* p"
+ − 317 using alpha_abs_res_minimal[OF asm] unfolding alpha_res by clarify
+ − 318 have "p \<bullet> (as \<inter> supp x) = as' \<inter> supp (p \<bullet> x)"
+ − 319 by (metis Int_commute asm c supp_property_res)
+ − 320 then show ?thesis using a b c unfolding alpha_set by simp
+ − 321 qed
+ − 322
2713
a84999edbcb3
More properties that relate abs_res and abs_set. Also abs_res with less binders.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 323 lemma alpha_abs_set_abs_res:
a84999edbcb3
More properties that relate abs_res and abs_set. Also abs_res with less binders.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 324 assumes asm: "(as \<inter> supp x, x) \<approx>set (op =) supp p (as' \<inter> supp x', x')"
a84999edbcb3
More properties that relate abs_res and abs_set. Also abs_res with less binders.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 325 shows "(as, x) \<approx>res (op =) supp p (as', x')"
3224
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 326 using asm unfolding alphas by (auto simp: Diff_Int)
2713
a84999edbcb3
More properties that relate abs_res and abs_set. Also abs_res with less binders.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 327
2674
+ − 328 lemma alpha_abs_res_stronger1:
+ − 329 assumes asm: "(as, x) \<approx>res (op =) supp p' (as', x')"
+ − 330 shows "\<exists>p. (as, x) \<approx>res (op =) supp p (as', x') \<and> supp p \<subseteq> as \<union> as'"
+ − 331 using alpha_abs_res_stronger1_aux[OF asm] by auto
+ − 332
2671
+ − 333 lemma alpha_abs_set_stronger1:
2673
+ − 334 assumes asm: "(as, x) \<approx>set (op =) supp p' (as', x')"
2671
+ − 335 shows "\<exists>p. (as, x) \<approx>set (op =) supp p (as', x') \<and> supp p \<subseteq> as \<union> as'"
+ − 336 proof -
+ − 337 from asm have 0: "(supp x - as) \<sharp>* p'" by (auto simp only: alphas)
+ − 338 then have #: "p' \<bullet> (supp x - as) = (supp x - as)"
+ − 339 by (simp add: atom_set_perm_eq)
2673
+ − 340 obtain p where *: "\<forall>b \<in> (supp x \<union> as). p \<bullet> b = p' \<bullet> b"
+ − 341 and **: "supp p \<subseteq> (supp x \<union> as) \<union> p' \<bullet> (supp x \<union> as)"
+ − 342 using set_renaming_perm2 by blast
2671
+ − 343 from * have "\<forall>b \<in> supp x. p \<bullet> b = p' \<bullet> b" by blast
+ − 344 then have a: "p \<bullet> x = p' \<bullet> x" using supp_perm_perm_eq by auto
+ − 345 from * have "\<forall>b \<in> as. p \<bullet> b = p' \<bullet> b" by blast
2673
+ − 346 then have zb: "p \<bullet> as = p' \<bullet> as"
3224
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 347 apply(auto simp: permute_set_def)
2673
+ − 348 apply(rule_tac x="xa" in exI)
+ − 349 apply(simp)
+ − 350 done
2671
+ − 351 have zc: "p' \<bullet> as = as'" using asm by (simp add: alphas)
+ − 352 from 0 have 1: "(supp x - as) \<sharp>* p" using *
3224
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 353 by (auto simp: fresh_star_def fresh_perm)
2671
+ − 354 then have 2: "(supp x - as) \<inter> supp p = {}"
3224
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 355 by (auto simp: fresh_star_def fresh_def)
2671
+ − 356 have b: "supp x = (supp x - as) \<union> (supp x \<inter> as)" by auto
+ − 357 have "supp p \<subseteq> supp x \<union> as \<union> p' \<bullet> supp x \<union> p' \<bullet> as" using ** using union_eqvt by blast
+ − 358 also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> as \<union> (p' \<bullet> ((supp x - as) \<union> (supp x \<inter> as))) \<union> p' \<bullet> as"
+ − 359 using b by simp
2673
+ − 360 also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> as \<union>
+ − 361 ((p' \<bullet> (supp x - as)) \<union> (p' \<bullet> (supp x \<inter> as))) \<union> p' \<bullet> as" by (simp add: union_eqvt)
2671
+ − 362 also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> as \<union> (p' \<bullet> (supp x \<inter> as)) \<union> p' \<bullet> as"
+ − 363 using # by auto
+ − 364 also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> as \<union> p' \<bullet> ((supp x \<inter> as) \<union> as)" using union_eqvt
+ − 365 by auto
+ − 366 also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> as \<union> p' \<bullet> as"
+ − 367 by (metis Int_commute Un_commute sup_inf_absorb)
2673
+ − 368 also have "\<dots> = (supp x - as) \<union> as \<union> p' \<bullet> as" by blast
2671
+ − 369 finally have "supp p \<subseteq> (supp x - as) \<union> as \<union> p' \<bullet> as" .
+ − 370 then have "supp p \<subseteq> as \<union> p' \<bullet> as" using 2 by blast
+ − 371 moreover
+ − 372 have "(as, x) \<approx>set (op =) supp p (as', x')" using asm 1 a zb by (simp add: alphas)
+ − 373 ultimately
+ − 374 show "\<exists>p. (as, x) \<approx>set (op =) supp p (as', x') \<and> supp p \<subseteq> as \<union> as'" using zc by blast
+ − 375 qed
+ − 376
2674
+ − 377 lemma alpha_abs_lst_stronger1:
+ − 378 assumes asm: "(as, x) \<approx>lst (op =) supp p' (as', x')"
+ − 379 shows "\<exists>p. (as, x) \<approx>lst (op =) supp p (as', x') \<and> supp p \<subseteq> set as \<union> set as'"
+ − 380 proof -
+ − 381 from asm have 0: "(supp x - set as) \<sharp>* p'" by (auto simp only: alphas)
+ − 382 then have #: "p' \<bullet> (supp x - set as) = (supp x - set as)"
+ − 383 by (simp add: atom_set_perm_eq)
+ − 384 obtain p where *: "\<forall>b \<in> (supp x \<union> set as). p \<bullet> b = p' \<bullet> b"
+ − 385 and **: "supp p \<subseteq> (supp x \<union> set as) \<union> p' \<bullet> (supp x \<union> set as)"
+ − 386 using set_renaming_perm2 by blast
+ − 387 from * have "\<forall>b \<in> supp x. p \<bullet> b = p' \<bullet> b" by blast
+ − 388 then have a: "p \<bullet> x = p' \<bullet> x" using supp_perm_perm_eq by auto
+ − 389 from * have "\<forall>b \<in> set as. p \<bullet> b = p' \<bullet> b" by blast
+ − 390 then have zb: "p \<bullet> as = p' \<bullet> as" by (induct as) (auto)
+ − 391 have zc: "p' \<bullet> set as = set as'" using asm by (simp add: alphas set_eqvt)
+ − 392 from 0 have 1: "(supp x - set as) \<sharp>* p" using *
3224
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 393 by (auto simp: fresh_star_def fresh_perm)
2674
+ − 394 then have 2: "(supp x - set as) \<inter> supp p = {}"
3224
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 395 by (auto simp: fresh_star_def fresh_def)
2674
+ − 396 have b: "supp x = (supp x - set as) \<union> (supp x \<inter> set as)" by auto
+ − 397 have "supp p \<subseteq> supp x \<union> set as \<union> p' \<bullet> supp x \<union> p' \<bullet> set as" using ** using union_eqvt by blast
+ − 398 also have "\<dots> = (supp x - set as) \<union> (supp x \<inter> set as) \<union> set as \<union>
+ − 399 (p' \<bullet> ((supp x - set as) \<union> (supp x \<inter> set as))) \<union> p' \<bullet> set as" using b by simp
+ − 400 also have "\<dots> = (supp x - set as) \<union> (supp x \<inter> set as) \<union> set as \<union>
+ − 401 ((p' \<bullet> (supp x - set as)) \<union> (p' \<bullet> (supp x \<inter> set as))) \<union> p' \<bullet> set as" by (simp add: union_eqvt)
+ − 402 also have "\<dots> = (supp x - set as) \<union> (supp x \<inter> set as) \<union> set as \<union>
+ − 403 (p' \<bullet> (supp x \<inter> set as)) \<union> p' \<bullet> set as" using # by auto
+ − 404 also have "\<dots> = (supp x - set as) \<union> (supp x \<inter> set as) \<union> set as \<union> p' \<bullet> ((supp x \<inter> set as) \<union> set as)"
+ − 405 using union_eqvt by auto
+ − 406 also have "\<dots> = (supp x - set as) \<union> (supp x \<inter> set as) \<union> set as \<union> p' \<bullet> set as"
+ − 407 by (metis Int_commute Un_commute sup_inf_absorb)
+ − 408 also have "\<dots> = (supp x - set as) \<union> set as \<union> p' \<bullet> set as" by blast
+ − 409 finally have "supp p \<subseteq> (supp x - set as) \<union> set as \<union> p' \<bullet> set as" .
+ − 410 then have "supp p \<subseteq> set as \<union> p' \<bullet> set as" using 2 by blast
+ − 411 moreover
+ − 412 have "(as, x) \<approx>lst (op =) supp p (as', x')" using asm 1 a zb by (simp add: alphas)
+ − 413 ultimately
+ − 414 show "\<exists>p. (as, x) \<approx>lst (op =) supp p (as', x') \<and> supp p \<subseteq> set as \<union> set as'" using zc by blast
+ − 415 qed
2668
+ − 416
2674
+ − 417 lemma alphas_abs_stronger:
+ − 418 shows "(as, x) \<approx>abs_set (as', x') \<longleftrightarrow> (\<exists>p. (as, x) \<approx>set (op =) supp p (as', x') \<and> supp p \<subseteq> as \<union> as')"
+ − 419 and "(as, x) \<approx>abs_res (as', x') \<longleftrightarrow> (\<exists>p. (as, x) \<approx>res (op =) supp p (as', x') \<and> supp p \<subseteq> as \<union> as')"
+ − 420 and "(bs, x) \<approx>abs_lst (bs', x') \<longleftrightarrow>
+ − 421 (\<exists>p. (bs, x) \<approx>lst (op =) supp p (bs', x') \<and> supp p \<subseteq> set bs \<union> set bs')"
+ − 422 apply(rule iffI)
3224
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 423 apply(auto simp: alphas_abs alpha_abs_set_stronger1)[1]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 424 apply(auto simp: alphas_abs)[1]
2674
+ − 425 apply(rule iffI)
3224
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 426 apply(auto simp: alphas_abs alpha_abs_res_stronger1)[1]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 427 apply(auto simp: alphas_abs)[1]
2674
+ − 428 apply(rule iffI)
3224
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 429 apply(auto simp: alphas_abs alpha_abs_lst_stronger1)[1]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 430 apply(auto simp: alphas_abs)[1]
2674
+ − 431 done
2668
+ − 432
3058
+ − 433 lemma alpha_res_alpha_set:
+ − 434 "(bs, x) \<approx>res op = supp p (cs, y) \<longleftrightarrow> (bs \<inter> supp x, x) \<approx>set op = supp p (cs \<inter> supp y, y)"
+ − 435 using alpha_abs_set_abs_res alpha_abs_res_abs_set by blast
+ − 436
2668
+ − 437 section {* Quotient types *}
+ − 438
3172
4cf3a4d36799
Added workaround for broken quotient_type in tip isabelle.
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
diff
changeset
+ − 439 quotient_type
2469
+ − 440 'a abs_set = "(atom set \<times> 'a::pt)" / "alpha_abs_set"
3199
+ − 441 apply(rule equivpI)
3172
4cf3a4d36799
Added workaround for broken quotient_type in tip isabelle.
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
diff
changeset
+ − 442 unfolding reflp_def refl_on_def symp_def sym_def transp_def trans_def
4cf3a4d36799
Added workaround for broken quotient_type in tip isabelle.
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
diff
changeset
+ − 443 by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:)
4cf3a4d36799
Added workaround for broken quotient_type in tip isabelle.
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
diff
changeset
+ − 444
4cf3a4d36799
Added workaround for broken quotient_type in tip isabelle.
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
diff
changeset
+ − 445 quotient_type
4cf3a4d36799
Added workaround for broken quotient_type in tip isabelle.
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
diff
changeset
+ − 446 'b abs_res = "(atom set \<times> 'b::pt)" / "alpha_abs_res"
3199
+ − 447 apply(rule equivpI)
3172
4cf3a4d36799
Added workaround for broken quotient_type in tip isabelle.
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
diff
changeset
+ − 448 unfolding reflp_def refl_on_def symp_def sym_def transp_def trans_def
4cf3a4d36799
Added workaround for broken quotient_type in tip isabelle.
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
diff
changeset
+ − 449 by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:)
4cf3a4d36799
Added workaround for broken quotient_type in tip isabelle.
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
diff
changeset
+ − 450
4cf3a4d36799
Added workaround for broken quotient_type in tip isabelle.
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
diff
changeset
+ − 451 quotient_type
4cf3a4d36799
Added workaround for broken quotient_type in tip isabelle.
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
diff
changeset
+ − 452 'c abs_lst = "(atom list \<times> 'c::pt)" / "alpha_abs_lst"
1657
+ − 453 apply(rule_tac [!] equivpI)
2592
+ − 454 unfolding reflp_def refl_on_def symp_def sym_def transp_def trans_def
1657
+ − 455 by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:)
1440
+ − 456
+ − 457 quotient_definition
2469
+ − 458 Abs_set ("[_]set. _" [60, 60] 60)
1932
+ − 459 where
2469
+ − 460 "Abs_set::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_set"
1440
+ − 461 is
3152
+ − 462 "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)" .
1440
+ − 463
1657
+ − 464 quotient_definition
1932
+ − 465 Abs_res ("[_]res. _" [60, 60] 60)
+ − 466 where
1657
+ − 467 "Abs_res::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_res"
+ − 468 is
3152
+ − 469 "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)" .
1657
+ − 470
+ − 471 quotient_definition
1932
+ − 472 Abs_lst ("[_]lst. _" [60, 60] 60)
+ − 473 where
1657
+ − 474 "Abs_lst::atom list \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_lst"
+ − 475 is
3152
+ − 476 "Pair::atom list \<Rightarrow> ('a::pt) \<Rightarrow> (atom list \<times> 'a)" .
1657
+ − 477
1440
+ − 478 lemma [quot_respect]:
2469
+ − 479 shows "(op= ===> op= ===> alpha_abs_set) Pair Pair"
1657
+ − 480 and "(op= ===> op= ===> alpha_abs_res) Pair Pair"
+ − 481 and "(op= ===> op= ===> alpha_abs_lst) Pair Pair"
+ − 482 unfolding fun_rel_def
2385
+ − 483 by (auto intro: alphas_abs_refl)
1440
+ − 484
+ − 485 lemma [quot_respect]:
2469
+ − 486 shows "(op= ===> alpha_abs_set ===> alpha_abs_set) permute permute"
1657
+ − 487 and "(op= ===> alpha_abs_res ===> alpha_abs_res) permute permute"
+ − 488 and "(op= ===> alpha_abs_lst ===> alpha_abs_lst) permute permute"
+ − 489 unfolding fun_rel_def
+ − 490 by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt)
1440
+ − 491
2491
+ − 492 lemma Abs_eq_iff:
3058
+ − 493 shows "[bs]set. x = [bs']set. y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op =) supp p (bs', y))"
+ − 494 and "[bs]res. x = [bs']res. y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (bs', y))"
+ − 495 and "[cs]lst. x = [cs']lst. y \<longleftrightarrow> (\<exists>p. (cs, x) \<approx>lst (op =) supp p (cs', y))"
2491
+ − 496 by (lifting alphas_abs)
+ − 497
2674
+ − 498 lemma Abs_eq_iff2:
3058
+ − 499 shows "[bs]set. x = [bs']set. y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op=) supp p (bs', y) \<and> supp p \<subseteq> bs \<union> bs')"
+ − 500 and "[bs]res. x = [bs']res. y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op=) supp p (bs', y) \<and> supp p \<subseteq> bs \<union> bs')"
+ − 501 and "[cs]lst. x = [cs']lst. y \<longleftrightarrow> (\<exists>p. (cs, x) \<approx>lst (op=) supp p (cs', y) \<and> supp p \<subseteq> set cs \<union> set cs')"
2674
+ − 502 by (lifting alphas_abs_stronger)
+ − 503
3024
+ − 504
2713
a84999edbcb3
More properties that relate abs_res and abs_set. Also abs_res with less binders.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 505 lemma Abs_eq_res_set:
3058
+ − 506 shows "[bs]res. x = [cs]res. y \<longleftrightarrow> [bs \<inter> supp x]set. x = [cs \<inter> supp y]set. y"
3024
+ − 507 unfolding Abs_eq_iff alpha_res_alpha_set by rule
2713
a84999edbcb3
More properties that relate abs_res and abs_set. Also abs_res with less binders.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 508
a84999edbcb3
More properties that relate abs_res and abs_set. Also abs_res with less binders.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 509 lemma Abs_eq_res_supp:
a84999edbcb3
More properties that relate abs_res and abs_set. Also abs_res with less binders.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 510 assumes asm: "supp x \<subseteq> bs"
3058
+ − 511 shows "[as]res. x = [as \<inter> bs]res. x"
2713
a84999edbcb3
More properties that relate abs_res and abs_set. Also abs_res with less binders.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 512 unfolding Abs_eq_iff alphas
a84999edbcb3
More properties that relate abs_res and abs_set. Also abs_res with less binders.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 513 apply (rule_tac x="0::perm" in exI)
a84999edbcb3
More properties that relate abs_res and abs_set. Also abs_res with less binders.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 514 apply (simp add: fresh_star_zero)
a84999edbcb3
More properties that relate abs_res and abs_set. Also abs_res with less binders.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 515 using asm by blast
a84999edbcb3
More properties that relate abs_res and abs_set. Also abs_res with less binders.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 516
3199
+ − 517 lemma Abs_exhausts[cases type]:
3058
+ − 518 shows "(\<And>as (x::'a::pt). y1 = [as]set. x \<Longrightarrow> P1) \<Longrightarrow> P1"
+ − 519 and "(\<And>as (x::'a::pt). y2 = [as]res. x \<Longrightarrow> P2) \<Longrightarrow> P2"
+ − 520 and "(\<And>bs (x::'a::pt). y3 = [bs]lst. x \<Longrightarrow> P3) \<Longrightarrow> P3"
1686
7b3dd407f6b3
got rid of the aux-function on the raw level, by defining it with function on the quotient level
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 521 by (lifting prod.exhaust[where 'a="atom set" and 'b="'a"]
7b3dd407f6b3
got rid of the aux-function on the raw level, by defining it with function on the quotient level
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 522 prod.exhaust[where 'a="atom set" and 'b="'a"]
7b3dd407f6b3
got rid of the aux-function on the raw level, by defining it with function on the quotient level
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 523 prod.exhaust[where 'a="atom list" and 'b="'a"])
1440
+ − 524
2469
+ − 525 instantiation abs_set :: (pt) pt
1440
+ − 526 begin
+ − 527
+ − 528 quotient_definition
2469
+ − 529 "permute_abs_set::perm \<Rightarrow> ('a::pt abs_set) \<Rightarrow> 'a abs_set"
1440
+ − 530 is
3152
+ − 531 "permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)"
+ − 532 by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt)
1440
+ − 533
2491
+ − 534 lemma permute_Abs_set[simp]:
1558
+ − 535 fixes x::"'a::pt"
3058
+ − 536 shows "(p \<bullet> ([as]set. x)) = [p \<bullet> as]set. (p \<bullet> x)"
1657
+ − 537 by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"])
1440
+ − 538
+ − 539 instance
+ − 540 apply(default)
3199
+ − 541 apply(case_tac [!] x)
1657
+ − 542 apply(simp_all)
+ − 543 done
+ − 544
+ − 545 end
+ − 546
+ − 547 instantiation abs_res :: (pt) pt
+ − 548 begin
+ − 549
+ − 550 quotient_definition
+ − 551 "permute_abs_res::perm \<Rightarrow> ('a::pt abs_res) \<Rightarrow> 'a abs_res"
+ − 552 is
+ − 553 "permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)"
3152
+ − 554 by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt)
1657
+ − 555
+ − 556 lemma permute_Abs_res[simp]:
+ − 557 fixes x::"'a::pt"
3058
+ − 558 shows "(p \<bullet> ([as]res. x)) = [p \<bullet> as]res. (p \<bullet> x)"
1657
+ − 559 by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"])
+ − 560
+ − 561 instance
+ − 562 apply(default)
3199
+ − 563 apply(case_tac [!] x)
1657
+ − 564 apply(simp_all)
+ − 565 done
+ − 566
+ − 567 end
+ − 568
+ − 569 instantiation abs_lst :: (pt) pt
+ − 570 begin
+ − 571
+ − 572 quotient_definition
+ − 573 "permute_abs_lst::perm \<Rightarrow> ('a::pt abs_lst) \<Rightarrow> 'a abs_lst"
+ − 574 is
+ − 575 "permute:: perm \<Rightarrow> (atom list \<times> 'a::pt) \<Rightarrow> (atom list \<times> 'a::pt)"
3152
+ − 576 by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt)
1657
+ − 577
+ − 578 lemma permute_Abs_lst[simp]:
+ − 579 fixes x::"'a::pt"
3058
+ − 580 shows "(p \<bullet> ([as]lst. x)) = [p \<bullet> as]lst. (p \<bullet> x)"
1657
+ − 581 by (lifting permute_prod.simps[where 'a="atom list" and 'b="'a"])
+ − 582
+ − 583 instance
+ − 584 apply(default)
3199
+ − 585 apply(case_tac [!] x)
1440
+ − 586 apply(simp_all)
+ − 587 done
+ − 588
+ − 589 end
+ − 590
2491
+ − 591 lemmas permute_Abs[eqvt] = permute_Abs_set permute_Abs_res permute_Abs_lst
1657
+ − 592
2385
+ − 593
2491
+ − 594 lemma Abs_swap1:
1662
+ − 595 assumes a1: "a \<notin> (supp x) - bs"
+ − 596 and a2: "b \<notin> (supp x) - bs"
3058
+ − 597 shows "[bs]set. x = [(a \<rightleftharpoons> b) \<bullet> bs]set. ((a \<rightleftharpoons> b) \<bullet> x)"
+ − 598 and "[bs]res. x = [(a \<rightleftharpoons> b) \<bullet> bs]res. ((a \<rightleftharpoons> b) \<bullet> x)"
2491
+ − 599 unfolding Abs_eq_iff
1662
+ − 600 unfolding alphas
+ − 601 unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric]
+ − 602 unfolding fresh_star_def fresh_def
+ − 603 unfolding swap_set_not_in[OF a1 a2]
+ − 604 using a1 a2
+ − 605 by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)
3224
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 606 (auto simp: supp_perm swap_atom)
1662
+ − 607
2491
+ − 608 lemma Abs_swap2:
1662
+ − 609 assumes a1: "a \<notin> (supp x) - (set bs)"
+ − 610 and a2: "b \<notin> (supp x) - (set bs)"
3058
+ − 611 shows "[bs]lst. x = [(a \<rightleftharpoons> b) \<bullet> bs]lst. ((a \<rightleftharpoons> b) \<bullet> x)"
2491
+ − 612 unfolding Abs_eq_iff
1662
+ − 613 unfolding alphas
+ − 614 unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] set_eqvt[symmetric]
+ − 615 unfolding fresh_star_def fresh_def
+ − 616 unfolding swap_set_not_in[OF a1 a2]
+ − 617 using a1 a2
+ − 618 by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)
3224
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 619 (auto simp: supp_perm swap_atom)
1662
+ − 620
2491
+ − 621 lemma Abs_supports:
3058
+ − 622 shows "((supp x) - as) supports ([as]set. x)"
+ − 623 and "((supp x) - as) supports ([as]res. x)"
+ − 624 and "((supp x) - set bs) supports ([bs]lst. x)"
1662
+ − 625 unfolding supports_def
2491
+ − 626 unfolding permute_Abs
+ − 627 by (simp_all add: Abs_swap1[symmetric] Abs_swap2[symmetric])
1657
+ − 628
1686
7b3dd407f6b3
got rid of the aux-function on the raw level, by defining it with function on the quotient level
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 629 function
3199
+ − 630 supp_set :: "('a::pt) abs_set \<Rightarrow> atom set" and
+ − 631 supp_res :: "('a::pt) abs_res \<Rightarrow> atom set" and
+ − 632 supp_lst :: "('a::pt) abs_lst \<Rightarrow> atom set"
1686
7b3dd407f6b3
got rid of the aux-function on the raw level, by defining it with function on the quotient level
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 633 where
3058
+ − 634 "supp_set ([as]set. x) = supp x - as"
3199
+ − 635 | "supp_res ([as]res. x) = supp x - as"
+ − 636 | "supp_lst (Abs_lst cs x) = (supp x) - (set cs)"
+ − 637 apply(simp_all add: Abs_eq_iff alphas_abs alphas)
+ − 638 apply(case_tac x)
+ − 639 apply(case_tac a)
1686
7b3dd407f6b3
got rid of the aux-function on the raw level, by defining it with function on the quotient level
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 640 apply(simp)
3199
+ − 641 apply(case_tac b)
+ − 642 apply(case_tac a)
+ − 643 apply(simp)
+ − 644 apply(case_tac ba)
+ − 645 apply(simp)
1686
7b3dd407f6b3
got rid of the aux-function on the raw level, by defining it with function on the quotient level
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 646 done
1657
+ − 647
3199
+ − 648 termination
3058
+ − 649 by lexicographic_order
1686
7b3dd407f6b3
got rid of the aux-function on the raw level, by defining it with function on the quotient level
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 650
2663
+ − 651 lemma supp_funs_eqvt[eqvt]:
2469
+ − 652 shows "(p \<bullet> supp_set x) = supp_set (p \<bullet> x)"
1657
+ − 653 and "(p \<bullet> supp_res y) = supp_res (p \<bullet> y)"
+ − 654 and "(p \<bullet> supp_lst z) = supp_lst (p \<bullet> z)"
3199
+ − 655 apply(case_tac x)
+ − 656 apply(simp)
+ − 657 apply(case_tac y)
+ − 658 apply(simp)
+ − 659 apply(case_tac z)
+ − 660 apply(simp)
1440
+ − 661 done
+ − 662
2491
+ − 663 lemma Abs_fresh_aux:
3058
+ − 664 shows "a \<sharp> [bs]set. x \<Longrightarrow> a \<sharp> supp_set ([bs]set. x)"
+ − 665 and "a \<sharp> [bs]res. x \<Longrightarrow> a \<sharp> supp_res ([bs]res. x)"
+ − 666 and "a \<sharp> [cs]lst. x \<Longrightarrow> a \<sharp> supp_lst ([cs]lst. x)"
1932
+ − 667 by (rule_tac [!] fresh_fun_eqvt_app)
2663
+ − 668 (auto simp only: eqvt_def eqvts_raw)
1657
+ − 669
2491
+ − 670 lemma Abs_supp_subset1:
1657
+ − 671 assumes a: "finite (supp x)"
3058
+ − 672 shows "(supp x) - as \<subseteq> supp ([as]set. x)"
+ − 673 and "(supp x) - as \<subseteq> supp ([as]res. x)"
+ − 674 and "(supp x) - (set bs) \<subseteq> supp ([bs]lst. x)"
1657
+ − 675 unfolding supp_conv_fresh
2491
+ − 676 by (auto dest!: Abs_fresh_aux)
1932
+ − 677 (simp_all add: fresh_def supp_finite_atom_set a)
1440
+ − 678
2491
+ − 679 lemma Abs_supp_subset2:
1657
+ − 680 assumes a: "finite (supp x)"
3058
+ − 681 shows "supp ([as]set. x) \<subseteq> (supp x) - as"
+ − 682 and "supp ([as]res. x) \<subseteq> (supp x) - as"
+ − 683 and "supp ([bs]lst. x) \<subseteq> (supp x) - (set bs)"
1932
+ − 684 by (rule_tac [!] supp_is_subset)
2491
+ − 685 (simp_all add: Abs_supports a)
1478
+ − 686
2491
+ − 687 lemma Abs_finite_supp:
1657
+ − 688 assumes a: "finite (supp x)"
3058
+ − 689 shows "supp ([as]set. x) = (supp x) - as"
+ − 690 and "supp ([as]res. x) = (supp x) - as"
+ − 691 and "supp ([bs]lst. x) = (supp x) - (set bs)"
+ − 692 using Abs_supp_subset1[OF a] Abs_supp_subset2[OF a]
+ − 693 by blast+
1440
+ − 694
2491
+ − 695 lemma supp_Abs:
1440
+ − 696 fixes x::"'a::fs"
3058
+ − 697 shows "supp ([as]set. x) = (supp x) - as"
+ − 698 and "supp ([as]res. x) = (supp x) - as"
+ − 699 and "supp ([bs]lst. x) = (supp x) - (set bs)"
+ − 700 by (simp_all add: Abs_finite_supp finite_supp)
1440
+ − 701
2469
+ − 702 instance abs_set :: (fs) fs
1440
+ − 703 apply(default)
3199
+ − 704 apply(case_tac x)
2491
+ − 705 apply(simp add: supp_Abs finite_supp)
1440
+ − 706 done
+ − 707
1657
+ − 708 instance abs_res :: (fs) fs
+ − 709 apply(default)
3199
+ − 710 apply(case_tac x)
2491
+ − 711 apply(simp add: supp_Abs finite_supp)
1657
+ − 712 done
+ − 713
+ − 714 instance abs_lst :: (fs) fs
+ − 715 apply(default)
3199
+ − 716 apply(case_tac x)
2491
+ − 717 apply(simp add: supp_Abs finite_supp)
1440
+ − 718 done
+ − 719
2491
+ − 720 lemma Abs_fresh_iff:
1657
+ − 721 fixes x::"'a::fs"
3058
+ − 722 shows "a \<sharp> [bs]set. x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"
+ − 723 and "a \<sharp> [bs]res. x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"
+ − 724 and "a \<sharp> [cs]lst. x \<longleftrightarrow> a \<in> (set cs) \<or> (a \<notin> (set cs) \<and> a \<sharp> x)"
1657
+ − 725 unfolding fresh_def
2491
+ − 726 unfolding supp_Abs
1657
+ − 727 by auto
1460
+ − 728
2591
+ − 729 lemma Abs_fresh_star_iff:
+ − 730 fixes x::"'a::fs"
3058
+ − 731 shows "as \<sharp>* ([bs]set. x) \<longleftrightarrow> (as - bs) \<sharp>* x"
+ − 732 and "as \<sharp>* ([bs]res. x) \<longleftrightarrow> (as - bs) \<sharp>* x"
+ − 733 and "as \<sharp>* ([cs]lst. x) \<longleftrightarrow> (as - set cs) \<sharp>* x"
2591
+ − 734 unfolding fresh_star_def
3224
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 735 by (auto simp: Abs_fresh_iff)
2591
+ − 736
2491
+ − 737 lemma Abs_fresh_star:
+ − 738 fixes x::"'a::fs"
3058
+ − 739 shows "as \<subseteq> as' \<Longrightarrow> as \<sharp>* ([as']set. x)"
+ − 740 and "as \<subseteq> as' \<Longrightarrow> as \<sharp>* ([as']res. x)"
+ − 741 and "bs \<subseteq> set bs' \<Longrightarrow> bs \<sharp>* ([bs']lst. x)"
2491
+ − 742 unfolding fresh_star_def
3224
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 743 by(auto simp: Abs_fresh_iff)
2468
+ − 744
2730
+ − 745 lemma Abs_fresh_star2:
+ − 746 fixes x::"'a::fs"
3058
+ − 747 shows "as \<inter> bs = {} \<Longrightarrow> as \<sharp>* ([bs]set. x) \<longleftrightarrow> as \<sharp>* x"
+ − 748 and "as \<inter> bs = {} \<Longrightarrow> as \<sharp>* ([bs]res. x) \<longleftrightarrow> as \<sharp>* x"
+ − 749 and "cs \<inter> set ds = {} \<Longrightarrow> cs \<sharp>* ([ds]lst. x) \<longleftrightarrow> cs \<sharp>* x"
2730
+ − 750 unfolding fresh_star_def Abs_fresh_iff
+ − 751 by auto
+ − 752
+ − 753
3058
+ − 754 section {* Abstractions of single atoms *}
+ − 755
3199
+ − 756
2679
+ − 757 lemma Abs1_eq:
3191
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 758 fixes x y::"'a::fs"
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 759 shows "[{atom a}]set. x = [{atom a}]set. y \<longleftrightarrow> x = y"
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 760 and "[{atom a}]res. x = [{atom a}]res. y \<longleftrightarrow> x = y"
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 761 and "[[atom a]]lst. x = [[atom a]]lst. y \<longleftrightarrow> x = y"
2679
+ − 762 unfolding Abs_eq_iff2 alphas
3224
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 763 by (auto simp: supp_perm_singleton fresh_star_def fresh_zero_perm)
2679
+ − 764
3192
+ − 765 lemma Abs1_eq_iff_fresh:
3191
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 766 fixes x y::"'a::fs"
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 767 and a b c::"'b::at"
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 768 assumes "atom c \<sharp> (a, b, x, y)"
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 769 shows "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y"
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 770 and "[{atom a}]res. x = [{atom b}]res. y \<longleftrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y"
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 771 and "[[atom a]]lst. x = [[atom b]]lst. y \<longleftrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y"
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 772 proof -
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 773 have "[{atom a}]set. x = (a \<leftrightarrow> c) \<bullet> ([{atom a}]set. x)"
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 774 by (rule_tac flip_fresh_fresh[symmetric]) (simp_all add: Abs_fresh_iff assms)
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 775 then have "[{atom a}]set. x = [{atom c}]set. ((a \<leftrightarrow> c) \<bullet> x)" by simp
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 776 moreover
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 777 have "[{atom b}]set. y = (b \<leftrightarrow> c) \<bullet> ([{atom b}]set. y)"
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 778 by (rule_tac flip_fresh_fresh[symmetric]) (simp_all add: Abs_fresh_iff assms)
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 779 then have "[{atom b}]set. y = [{atom c}]set. ((b \<leftrightarrow> c) \<bullet> y)" by simp
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 780 ultimately
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 781 show "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y"
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 782 by (simp add: Abs1_eq)
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 783 next
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 784 have "[{atom a}]res. x = (a \<leftrightarrow> c) \<bullet> ([{atom a}]res. x)"
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 785 by (rule_tac flip_fresh_fresh[symmetric]) (simp_all add: Abs_fresh_iff assms)
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 786 then have "[{atom a}]res. x = [{atom c}]res. ((a \<leftrightarrow> c) \<bullet> x)" by simp
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 787 moreover
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 788 have "[{atom b}]res. y = (b \<leftrightarrow> c) \<bullet> ([{atom b}]res. y)"
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 789 by (rule_tac flip_fresh_fresh[symmetric]) (simp_all add: Abs_fresh_iff assms)
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 790 then have "[{atom b}]res. y = [{atom c}]res. ((b \<leftrightarrow> c) \<bullet> y)" by simp
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 791 ultimately
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 792 show "[{atom a}]res. x = [{atom b}]res. y \<longleftrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y"
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 793 by (simp add: Abs1_eq)
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 794 next
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 795 have "[[atom a]]lst. x = (a \<leftrightarrow> c) \<bullet> ([[atom a]]lst. x)"
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 796 by (rule_tac flip_fresh_fresh[symmetric]) (simp_all add: Abs_fresh_iff assms)
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 797 then have "[[atom a]]lst. x = [[atom c]]lst. ((a \<leftrightarrow> c) \<bullet> x)" by simp
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 798 moreover
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 799 have "[[atom b]]lst. y = (b \<leftrightarrow> c) \<bullet> ([[atom b]]lst. y)"
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 800 by (rule_tac flip_fresh_fresh[symmetric]) (simp_all add: Abs_fresh_iff assms)
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 801 then have "[[atom b]]lst. y = [[atom c]]lst. ((b \<leftrightarrow> c) \<bullet> y)" by simp
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 802 ultimately
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 803 show "[[atom a]]lst. x = [[atom b]]lst. y \<longleftrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y"
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 804 by (simp add: Abs1_eq)
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 805 qed
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 806
3192
+ − 807 lemma Abs1_eq_iff_all:
3191
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 808 fixes x y::"'a::fs"
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 809 and z::"'c::fs"
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 810 and a b::"'b::at"
3224
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 811 shows "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (\<forall>c. atom c \<sharp> z \<longrightarrow> atom c \<sharp> (a, b, x, y) \<longrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 812 and "[{atom a}]res. x = [{atom b}]res. y \<longleftrightarrow> (\<forall>c. atom c \<sharp> z \<longrightarrow> atom c \<sharp> (a, b, x, y) \<longrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 813 and "[[atom a]]lst. x = [[atom b]]lst. y \<longleftrightarrow> (\<forall>c. atom c \<sharp> z \<longrightarrow> atom c \<sharp> (a, b, x, y) \<longrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y)"
3191
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 814 apply(auto)
3192
+ − 815 apply(simp add: Abs1_eq_iff_fresh(1)[symmetric])
3191
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 816 apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh)
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 817 apply(drule_tac x="aa" in spec)
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 818 apply(simp)
3192
+ − 819 apply(subst Abs1_eq_iff_fresh(1))
3224
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 820 apply(auto simp: fresh_Pair)[2]
3192
+ − 821 apply(simp add: Abs1_eq_iff_fresh(2)[symmetric])
3191
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 822 apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh)
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 823 apply(drule_tac x="aa" in spec)
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 824 apply(simp)
3192
+ − 825 apply(subst Abs1_eq_iff_fresh(2))
3224
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 826 apply(auto simp: fresh_Pair)[2]
3192
+ − 827 apply(simp add: Abs1_eq_iff_fresh(3)[symmetric])
3191
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 828 apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh)
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 829 apply(drule_tac x="aa" in spec)
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 830 apply(simp)
3192
+ − 831 apply(subst Abs1_eq_iff_fresh(3))
3224
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 832 apply(auto simp: fresh_Pair)[2]
3191
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 833 done
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 834
2679
+ − 835 lemma Abs1_eq_iff:
3191
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 836 fixes x y::"'a::fs"
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 837 and a b::"'b::at"
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 838 shows "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y)"
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 839 and "[{atom a}]res. x = [{atom b}]res. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y)"
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 840 and "[[atom a]]lst. x = [[atom b]]lst. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y)"
2679
+ − 841 proof -
+ − 842 { assume "a = b"
3191
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 843 then have "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (a = b \<and> x = y)" by (simp add: Abs1_eq)
2679
+ − 844 }
+ − 845 moreover
3199
+ − 846 { assume *: "a \<noteq> b" and **: "[{atom a}]set. x = [{atom b}]set. y"
+ − 847 have #: "atom a \<sharp> [{atom b}]set. y" by (simp add: **[symmetric] Abs_fresh_iff)
+ − 848 have "[{atom a}]set. ((a \<leftrightarrow> b) \<bullet> y) = (a \<leftrightarrow> b) \<bullet> ([{atom b}]set. y)" by (simp)
+ − 849 also have "\<dots> = [{atom b}]set. y"
3191
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 850 by (rule flip_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)
3199
+ − 851 also have "\<dots> = [{atom a}]set. x" using ** by simp
3191
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 852 finally have "a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y" using # * by (simp add: Abs1_eq Abs_fresh_iff)
2679
+ − 853 }
+ − 854 moreover
3191
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 855 { assume *: "a \<noteq> b" and **: "x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y"
3199
+ − 856 have "[{atom a}]set. x = [{atom a}]set. ((a \<leftrightarrow> b) \<bullet> y)" using ** by simp
+ − 857 also have "\<dots> = (a \<leftrightarrow> b) \<bullet> ([{atom b}]set. y)" by (simp add: permute_set_def assms)
+ − 858 also have "\<dots> = [{atom b}]set. y"
3191
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 859 by (rule flip_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)
3199
+ − 860 finally have "[{atom a}]set. x = [{atom b}]set. y" .
2679
+ − 861 }
+ − 862 ultimately
3199
+ − 863 show "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y)"
2679
+ − 864 by blast
+ − 865 next
+ − 866 { assume "a = b"
3191
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 867 then have "Abs_res {atom a} x = Abs_res {atom b} y \<longleftrightarrow> (a = b \<and> x = y)" by (simp add: Abs1_eq)
2679
+ − 868 }
+ − 869 moreover
3191
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 870 { assume *: "a \<noteq> b" and **: "Abs_res {atom a} x = Abs_res {atom b} y"
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 871 have #: "atom a \<sharp> Abs_res {atom b} y" by (simp add: **[symmetric] Abs_fresh_iff)
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 872 have "Abs_res {atom a} ((a \<leftrightarrow> b) \<bullet> y) = (a \<leftrightarrow> b) \<bullet> (Abs_res {atom b} y)" by (simp add: assms)
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 873 also have "\<dots> = Abs_res {atom b} y"
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 874 by (rule flip_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 875 also have "\<dots> = Abs_res {atom a} x" using ** by simp
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 876 finally have "a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y" using # * by (simp add: Abs1_eq Abs_fresh_iff)
2679
+ − 877 }
+ − 878 moreover
3191
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 879 { assume *: "a \<noteq> b" and **: "x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y"
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 880 have "Abs_res {atom a} x = Abs_res {atom a} ((a \<leftrightarrow> b) \<bullet> y)" using ** by simp
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 881 also have "\<dots> = (a \<leftrightarrow> b) \<bullet> Abs_res {atom b} y" by (simp add: permute_set_def assms)
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 882 also have "\<dots> = Abs_res {atom b} y"
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 883 by (rule flip_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 884 finally have "Abs_res {atom a} x = Abs_res {atom b} y" .
2679
+ − 885 }
+ − 886 ultimately
3191
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 887 show "Abs_res {atom a} x = Abs_res {atom b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y)"
2679
+ − 888 by blast
+ − 889 next
3191
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 890 { assume "a = b"
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 891 then have "Abs_lst [atom a] x = Abs_lst [atom b] y \<longleftrightarrow> (a = b \<and> x = y)" by (simp add: Abs1_eq)
2679
+ − 892 }
+ − 893 moreover
3191
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 894 { assume *: "a \<noteq> b" and **: "Abs_lst [atom a] x = Abs_lst [atom b] y"
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 895 have #: "atom a \<sharp> Abs_lst [atom b] y" by (simp add: **[symmetric] Abs_fresh_iff)
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 896 have "Abs_lst [atom a] ((a \<leftrightarrow> b) \<bullet> y) = (a \<leftrightarrow> b) \<bullet> (Abs_lst [atom b] y)" by (simp add: assms)
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 897 also have "\<dots> = Abs_lst [atom b] y"
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 898 by (rule flip_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 899 also have "\<dots> = Abs_lst [atom a] x" using ** by simp
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 900 finally have "a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y" using # * by (simp add: Abs1_eq Abs_fresh_iff)
2679
+ − 901 }
+ − 902 moreover
3191
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 903 { assume *: "a \<noteq> b" and **: "x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y"
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 904 have "Abs_lst [atom a] x = Abs_lst [atom a] ((a \<leftrightarrow> b) \<bullet> y)" using ** by simp
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 905 also have "\<dots> = (a \<leftrightarrow> b) \<bullet> Abs_lst [atom b] y" by (simp add: assms)
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 906 also have "\<dots> = Abs_lst [atom b] y"
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 907 by (rule flip_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 908 finally have "Abs_lst [atom a] x = Abs_lst [atom b] y" .
2679
+ − 909 }
+ − 910 ultimately
3191
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 911 show "Abs_lst [atom a] x = Abs_lst [atom b] y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y)"
2679
+ − 912 by blast
+ − 913 qed
+ − 914
2683
+ − 915 lemma Abs1_eq_iff':
+ − 916 fixes x::"'a::fs"
3191
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 917 and a b::"'b::at"
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 918 shows "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<leftrightarrow> a) \<bullet> x = y \<and> atom b \<sharp> x)"
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 919 and "[{atom a}]res. x = [{atom b}]res. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<leftrightarrow> a) \<bullet> x = y \<and> atom b \<sharp> x)"
0440bc1a2438
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 920 and "[[atom a]]lst. x = [[atom b]]lst. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<leftrightarrow> a) \<bullet> x = y \<and> atom b \<sharp> x)"
3224
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 921 using assms by (auto simp: Abs1_eq_iff fresh_permute_left)
2683
+ − 922
2468
+ − 923
3192
+ − 924 ML {*
3218
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 925 fun alpha_single_simproc thm _ ctxt ctrm =
3192
+ − 926 let
+ − 927 val thy = Proof_Context.theory_of ctxt
+ − 928 val _ $ (_ $ x) $ (_ $ y) = term_of ctrm
+ − 929 val cvrs = union (op =) (Term.add_frees x []) (Term.add_frees y [])
+ − 930 |> filter (fn (_, ty) => Sign.of_sort thy (ty, @{sort fs}))
+ − 931 |> map Free
+ − 932 |> HOLogic.mk_tuple
+ − 933 |> Thm.cterm_of thy
+ − 934 val cvrs_ty = ctyp_of_term cvrs
+ − 935 val thm' = thm
+ − 936 |> Drule.instantiate' [NONE, NONE, SOME cvrs_ty] [NONE, NONE, NONE, NONE, SOME cvrs]
+ − 937 in
+ − 938 SOME thm'
+ − 939 end
+ − 940 *}
+ − 941
+ − 942 simproc_setup alpha_set ("[{atom a}]set. x = [{atom b}]set. y") =
+ − 943 {* alpha_single_simproc @{thm Abs1_eq_iff_all(1)[THEN eq_reflection]} *}
+ − 944
+ − 945 simproc_setup alpha_res ("[{atom a}]res. x = [{atom b}]res. y") =
+ − 946 {* alpha_single_simproc @{thm Abs1_eq_iff_all(2)[THEN eq_reflection]} *}
+ − 947
+ − 948 simproc_setup alpha_lst ("[[atom a]]lst. x = [[atom b]]lst. y") =
+ − 949 {* alpha_single_simproc @{thm Abs1_eq_iff_all(3)[THEN eq_reflection]} *}
+ − 950
+ − 951
2599
+ − 952 subsection {* Renaming of bodies of abstractions *}
+ − 953
+ − 954 lemma Abs_rename_set:
+ − 955 fixes x::"'a::fs"
2659
+ − 956 assumes a: "(p \<bullet> bs) \<sharp>* x"
3060
+ − 957 (*and b: "finite bs"*)
2616
dd7490fdd998
all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 958 shows "\<exists>q. [bs]set. x = [p \<bullet> bs]set. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"
2599
+ − 959 proof -
3058
+ − 960 from set_renaming_perm2
2668
+ − 961 obtain q where *: "\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" by blast
3060
+ − 962 have ***: "q \<bullet> bs = p \<bullet> bs" using *
+ − 963 unfolding permute_set_eq_image image_def by auto
2599
+ − 964 have "[bs]set. x = q \<bullet> ([bs]set. x)"
+ − 965 apply(rule perm_supp_eq[symmetric])
+ − 966 using a **
+ − 967 unfolding Abs_fresh_star_iff
+ − 968 unfolding fresh_star_def
+ − 969 by auto
+ − 970 also have "\<dots> = [q \<bullet> bs]set. (q \<bullet> x)" by simp
2668
+ − 971 finally have "[bs]set. x = [p \<bullet> bs]set. (q \<bullet> x)" by (simp add: ***)
+ − 972 then show "\<exists>q. [bs]set. x = [p \<bullet> bs]set. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" using *** by metis
2599
+ − 973 qed
+ − 974
+ − 975 lemma Abs_rename_res:
+ − 976 fixes x::"'a::fs"
2659
+ − 977 assumes a: "(p \<bullet> bs) \<sharp>* x"
3060
+ − 978 (*and b: "finite bs"*)
2616
dd7490fdd998
all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 979 shows "\<exists>q. [bs]res. x = [p \<bullet> bs]res. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"
2599
+ − 980 proof -
3058
+ − 981 from set_renaming_perm2
2668
+ − 982 obtain q where *: "\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" by blast
3060
+ − 983 have ***: "q \<bullet> bs = p \<bullet> bs" using *
+ − 984 unfolding permute_set_eq_image image_def by auto
2599
+ − 985 have "[bs]res. x = q \<bullet> ([bs]res. x)"
+ − 986 apply(rule perm_supp_eq[symmetric])
+ − 987 using a **
+ − 988 unfolding Abs_fresh_star_iff
+ − 989 unfolding fresh_star_def
+ − 990 by auto
+ − 991 also have "\<dots> = [q \<bullet> bs]res. (q \<bullet> x)" by simp
2668
+ − 992 finally have "[bs]res. x = [p \<bullet> bs]res. (q \<bullet> x)" by (simp add: ***)
+ − 993 then show "\<exists>q. [bs]res. x = [p \<bullet> bs]res. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" using *** by metis
2599
+ − 994 qed
+ − 995
2611
3d101f2f817c
simple cases for strong inducts done; infrastructure for the difficult ones is there
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 996 lemma Abs_rename_lst:
2599
+ − 997 fixes x::"'a::fs"
2659
+ − 998 assumes a: "(p \<bullet> (set bs)) \<sharp>* x"
2616
dd7490fdd998
all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 999 shows "\<exists>q. [bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"
2599
+ − 1000 proof -
3058
+ − 1001 from list_renaming_perm
2668
+ − 1002 obtain q where *: "\<forall>b \<in> set bs. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> set bs \<union> (p \<bullet> set bs)" by blast
+ − 1003 have ***: "q \<bullet> bs = p \<bullet> bs" using * by (induct bs) (simp_all add: insert_eqvt)
2599
+ − 1004 have "[bs]lst. x = q \<bullet> ([bs]lst. x)"
+ − 1005 apply(rule perm_supp_eq[symmetric])
+ − 1006 using a **
+ − 1007 unfolding Abs_fresh_star_iff
+ − 1008 unfolding fresh_star_def
+ − 1009 by auto
+ − 1010 also have "\<dots> = [q \<bullet> bs]lst. (q \<bullet> x)" by simp
2668
+ − 1011 finally have "[bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x)" by (simp add: ***)
+ − 1012 then show "\<exists>q. [bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" using *** by metis
2599
+ − 1013 qed
+ − 1014
+ − 1015
2616
dd7490fdd998
all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1016 text {* for deep recursive binders *}
dd7490fdd998
all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1017
dd7490fdd998
all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1018 lemma Abs_rename_set':
dd7490fdd998
all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1019 fixes x::"'a::fs"
2659
+ − 1020 assumes a: "(p \<bullet> bs) \<sharp>* x"
3060
+ − 1021 (*and b: "finite bs"*)
2616
dd7490fdd998
all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1022 shows "\<exists>q. [bs]set. x = [q \<bullet> bs]set. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"
3060
+ − 1023 using Abs_rename_set[OF a] by metis
2616
dd7490fdd998
all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1024
dd7490fdd998
all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1025 lemma Abs_rename_res':
dd7490fdd998
all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1026 fixes x::"'a::fs"
2659
+ − 1027 assumes a: "(p \<bullet> bs) \<sharp>* x"
3060
+ − 1028 (*and b: "finite bs"*)
2616
dd7490fdd998
all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1029 shows "\<exists>q. [bs]res. x = [q \<bullet> bs]res. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"
3060
+ − 1030 using Abs_rename_res[OF a] by metis
2616
dd7490fdd998
all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1031
dd7490fdd998
all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1032 lemma Abs_rename_lst':
dd7490fdd998
all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1033 fixes x::"'a::fs"
2659
+ − 1034 assumes a: "(p \<bullet> (set bs)) \<sharp>* x"
2616
dd7490fdd998
all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1035 shows "\<exists>q. [bs]lst. x = [q \<bullet> bs]lst. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"
dd7490fdd998
all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1036 using Abs_rename_lst[OF a] by metis
2599
+ − 1037
2468
+ − 1038 section {* Infrastructure for building tuples of relations and functions *}
+ − 1039
2385
+ − 1040 fun
+ − 1041 prod_fv :: "('a \<Rightarrow> atom set) \<Rightarrow> ('b \<Rightarrow> atom set) \<Rightarrow> ('a \<times> 'b) \<Rightarrow> atom set"
+ − 1042 where
+ − 1043 "prod_fv fv1 fv2 (x, y) = fv1 x \<union> fv2 y"
+ − 1044
+ − 1045 definition
+ − 1046 prod_alpha :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool)"
+ − 1047 where
+ − 1048 "prod_alpha = prod_rel"
+ − 1049
+ − 1050 lemma [quot_respect]:
+ − 1051 shows "((R1 ===> op =) ===> (R2 ===> op =) ===> prod_rel R1 R2 ===> op =) prod_fv prod_fv"
2559
add799cf0817
adapted to changes by Florian on the quotient package and removed local fix for function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1052 unfolding fun_rel_def
add799cf0817
adapted to changes by Florian on the quotient package and removed local fix for function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1053 unfolding prod_rel_def
2385
+ − 1054 by auto
+ − 1055
+ − 1056 lemma [quot_preserve]:
3157
de89c95c5377
updated to latest changes (10 April) to quotient package (lift_raw_const only takes dummy theorem TrueI....in the future this will not work anymore)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1057 assumes q1: "Quotient3 R1 abs1 rep1"
de89c95c5377
updated to latest changes (10 April) to quotient package (lift_raw_const only takes dummy theorem TrueI....in the future this will not work anymore)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1058 and q2: "Quotient3 R2 abs2 rep2"
2574
+ − 1059 shows "((abs1 ---> id) ---> (abs2 ---> id) ---> map_pair rep1 rep2 ---> id) prod_fv = prod_fv"
3157
de89c95c5377
updated to latest changes (10 April) to quotient package (lift_raw_const only takes dummy theorem TrueI....in the future this will not work anymore)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1060 by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2])
2385
+ − 1061
+ − 1062 lemma [mono]:
+ − 1063 shows "A <= B \<Longrightarrow> C <= D ==> prod_alpha A C <= prod_alpha B D"
+ − 1064 unfolding prod_alpha_def
+ − 1065 by auto
+ − 1066
+ − 1067 lemma [eqvt]:
+ − 1068 shows "p \<bullet> prod_alpha A B x y = prod_alpha (p \<bullet> A) (p \<bullet> B) (p \<bullet> x) (p \<bullet> y)"
+ − 1069 unfolding prod_alpha_def
2559
add799cf0817
adapted to changes by Florian on the quotient package and removed local fix for function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1070 unfolding prod_rel_def
2385
+ − 1071 by (perm_simp) (rule refl)
+ − 1072
+ − 1073 lemma [eqvt]:
+ − 1074 shows "p \<bullet> prod_fv A B (x, y) = prod_fv (p \<bullet> A) (p \<bullet> B) (p \<bullet> x, p \<bullet> y)"
+ − 1075 unfolding prod_fv.simps
+ − 1076 by (perm_simp) (rule refl)
+ − 1077
2489
+ − 1078 lemma prod_fv_supp:
+ − 1079 shows "prod_fv supp supp = supp"
+ − 1080 by (rule ext)
3224
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1081 (auto simp: supp_Pair)
2489
+ − 1082
+ − 1083 lemma prod_alpha_eq:
+ − 1084 shows "prod_alpha (op=) (op=) = (op=)"
2843
+ − 1085 unfolding prod_alpha_def
+ − 1086 by (auto intro!: ext)
+ − 1087
1440
+ − 1088 end