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
2469
+ − 12 alpha_set
1440
+ − 13 where
2469
+ − 14 alpha_set[simp del]:
+ − 15 "alpha_set (bs, x) R f pi (cs, y) \<longleftrightarrow>
1465
+ − 16 f x - bs = f y - cs \<and>
+ − 17 (f x - bs) \<sharp>* pi \<and>
+ − 18 R (pi \<bullet> x) y \<and>
+ − 19 pi \<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]:
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 25 "alpha_res (bs, x) R f pi (cs, y) \<longleftrightarrow>
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 26 f x - bs = f y - cs \<and>
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 27 (f x - bs) \<sharp>* pi \<and>
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 28 R (pi \<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]:
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 34 "alpha_lst (bs, x) R f pi (cs, y) \<longleftrightarrow>
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 35 f x - set bs = f y - set cs \<and>
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 36 (f x - set bs) \<sharp>* pi \<and>
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 37 R (pi \<bullet> x) y \<and>
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 38 pi \<bullet> bs = cs"
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)
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 54 (auto simp add: 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]
+ − 67 by (auto simp add: permute_bool_def fresh_star_permute_iff)
+ − 68
2385
+ − 69
+ − 70 section {* Equivalence *}
+ − 71
+ − 72 lemma alpha_refl:
2311
+ − 73 assumes a: "R x x"
2469
+ − 74 shows "(bs, x) \<approx>set R f 0 (bs, x)"
2311
+ − 75 and "(bs, x) \<approx>res R f 0 (bs, x)"
+ − 76 and "(cs, x) \<approx>lst R f 0 (cs, x)"
+ − 77 using a
+ − 78 unfolding alphas
+ − 79 unfolding fresh_star_def
+ − 80 by (simp_all add: fresh_zero_perm)
+ − 81
2385
+ − 82 lemma alpha_sym:
2311
+ − 83 assumes a: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x"
2469
+ − 84 shows "(bs, x) \<approx>set R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>set R f (- p) (bs, x)"
2311
+ − 85 and "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)"
+ − 86 and "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)"
+ − 87 unfolding alphas fresh_star_def
+ − 88 using a
+ − 89 by (auto simp add: fresh_minus_perm)
+ − 90
2385
+ − 91 lemma alpha_trans:
+ − 92 assumes a: "\<lbrakk>R (p \<bullet> x) y; R (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((q + p) \<bullet> x) z"
2469
+ − 93 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
+ − 94 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)"
+ − 95 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)"
+ − 96 using a
+ − 97 unfolding alphas fresh_star_def
+ − 98 by (simp_all add: fresh_plus_perm)
+ − 99
+ − 100 lemma alpha_sym_eqvt:
2311
+ − 101 assumes a: "R (p \<bullet> x) y \<Longrightarrow> R y (p \<bullet> x)"
+ − 102 and b: "p \<bullet> R = R"
2469
+ − 103 shows "(bs, x) \<approx>set R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>set R f (- p) (bs, x)"
2311
+ − 104 and "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)"
2313
+ − 105 and "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)"
2385
+ − 106 apply(auto intro!: alpha_sym)
2313
+ − 107 apply(drule_tac [!] a)
+ − 108 apply(rule_tac [!] p="p" in permute_boolE)
+ − 109 apply(perm_simp add: permute_minus_cancel b)
+ − 110 apply(assumption)
+ − 111 apply(perm_simp add: permute_minus_cancel b)
+ − 112 apply(assumption)
+ − 113 apply(perm_simp add: permute_minus_cancel b)
+ − 114 apply(assumption)
+ − 115 done
2311
+ − 116
2469
+ − 117 lemma alpha_set_trans_eqvt:
+ − 118 assumes b: "(cs, y) \<approx>set R f q (ds, z)"
+ − 119 and a: "(bs, x) \<approx>set R f p (cs, y)"
2313
+ − 120 and d: "q \<bullet> R = R"
+ − 121 and c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"
2469
+ − 122 shows "(bs, x) \<approx>set R f (q + p) (ds, z)"
2385
+ − 123 apply(rule alpha_trans)
2313
+ − 124 defer
+ − 125 apply(rule a)
+ − 126 apply(rule b)
+ − 127 apply(drule c)
+ − 128 apply(rule_tac p="q" in permute_boolE)
+ − 129 apply(perm_simp add: permute_minus_cancel d)
+ − 130 apply(assumption)
+ − 131 apply(rotate_tac -1)
+ − 132 apply(drule_tac p="q" in permute_boolI)
+ − 133 apply(perm_simp add: permute_minus_cancel d)
+ − 134 apply(simp add: permute_eqvt[symmetric])
+ − 135 done
+ − 136
+ − 137 lemma alpha_res_trans_eqvt:
+ − 138 assumes b: "(cs, y) \<approx>res R f q (ds, z)"
+ − 139 and a: "(bs, x) \<approx>res R f p (cs, y)"
+ − 140 and d: "q \<bullet> R = R"
+ − 141 and c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"
+ − 142 shows "(bs, x) \<approx>res R f (q + p) (ds, z)"
2385
+ − 143 apply(rule alpha_trans)
2313
+ − 144 defer
+ − 145 apply(rule a)
+ − 146 apply(rule b)
+ − 147 apply(drule c)
+ − 148 apply(rule_tac p="q" in permute_boolE)
+ − 149 apply(perm_simp add: permute_minus_cancel d)
+ − 150 apply(assumption)
+ − 151 apply(rotate_tac -1)
+ − 152 apply(drule_tac p="q" in permute_boolI)
+ − 153 apply(perm_simp add: permute_minus_cancel d)
+ − 154 apply(simp add: permute_eqvt[symmetric])
+ − 155 done
+ − 156
+ − 157 lemma alpha_lst_trans_eqvt:
+ − 158 assumes b: "(cs, y) \<approx>lst R f q (ds, z)"
+ − 159 and a: "(bs, x) \<approx>lst R f p (cs, y)"
+ − 160 and d: "q \<bullet> R = R"
+ − 161 and c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"
+ − 162 shows "(bs, x) \<approx>lst R f (q + p) (ds, z)"
2385
+ − 163 apply(rule alpha_trans)
2313
+ − 164 defer
+ − 165 apply(rule a)
+ − 166 apply(rule b)
+ − 167 apply(drule c)
+ − 168 apply(rule_tac p="q" in permute_boolE)
+ − 169 apply(perm_simp add: permute_minus_cancel d)
+ − 170 apply(assumption)
+ − 171 apply(rotate_tac -1)
+ − 172 apply(drule_tac p="q" in permute_boolI)
+ − 173 apply(perm_simp add: permute_minus_cancel d)
+ − 174 apply(simp add: permute_eqvt[symmetric])
+ − 175 done
+ − 176
2469
+ − 177 lemmas alpha_trans_eqvt = alpha_set_trans_eqvt alpha_res_trans_eqvt alpha_lst_trans_eqvt
2313
+ − 178
2311
+ − 179
+ − 180 section {* General Abstractions *}
+ − 181
1440
+ − 182 fun
2469
+ − 183 alpha_abs_set
1440
+ − 184 where
1666
+ − 185 [simp del]:
2469
+ − 186 "alpha_abs_set (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op=) supp p (cs, y))"
1440
+ − 187
1657
+ − 188 fun
+ − 189 alpha_abs_lst
+ − 190 where
1666
+ − 191 [simp del]:
1657
+ − 192 "alpha_abs_lst (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>lst (op=) supp p (cs, y))"
+ − 193
+ − 194 fun
+ − 195 alpha_abs_res
+ − 196 where
1666
+ − 197 [simp del]:
1657
+ − 198 "alpha_abs_res (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op=) supp p (cs, y))"
+ − 199
1440
+ − 200 notation
2469
+ − 201 alpha_abs_set (infix "\<approx>abs'_set" 50) and
1666
+ − 202 alpha_abs_lst (infix "\<approx>abs'_lst" 50) and
+ − 203 alpha_abs_res (infix "\<approx>abs'_res" 50)
1657
+ − 204
2469
+ − 205 lemmas alphas_abs = alpha_abs_set.simps alpha_abs_res.simps alpha_abs_lst.simps
1657
+ − 206
2385
+ − 207
1657
+ − 208 lemma alphas_abs_refl:
2469
+ − 209 shows "(bs, x) \<approx>abs_set (bs, x)"
1657
+ − 210 and "(bs, x) \<approx>abs_res (bs, x)"
+ − 211 and "(cs, x) \<approx>abs_lst (cs, x)"
+ − 212 unfolding alphas_abs
+ − 213 unfolding alphas
+ − 214 unfolding fresh_star_def
+ − 215 by (rule_tac [!] x="0" in exI)
+ − 216 (simp_all add: fresh_zero_perm)
+ − 217
+ − 218 lemma alphas_abs_sym:
2469
+ − 219 shows "(bs, x) \<approx>abs_set (cs, y) \<Longrightarrow> (cs, y) \<approx>abs_set (bs, x)"
1657
+ − 220 and "(bs, x) \<approx>abs_res (cs, y) \<Longrightarrow> (cs, y) \<approx>abs_res (bs, x)"
+ − 221 and "(ds, x) \<approx>abs_lst (es, y) \<Longrightarrow> (es, y) \<approx>abs_lst (ds, x)"
+ − 222 unfolding alphas_abs
+ − 223 unfolding alphas
+ − 224 unfolding fresh_star_def
+ − 225 by (erule_tac [!] exE, rule_tac [!] x="-p" in exI)
+ − 226 (auto simp add: fresh_minus_perm)
1440
+ − 227
1657
+ − 228 lemma alphas_abs_trans:
2469
+ − 229 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
+ − 230 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)"
+ − 231 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)"
+ − 232 unfolding alphas_abs
+ − 233 unfolding alphas
+ − 234 unfolding fresh_star_def
+ − 235 apply(erule_tac [!] exE, erule_tac [!] exE)
+ − 236 apply(rule_tac [!] x="pa + p" in exI)
+ − 237 by (simp_all add: fresh_plus_perm)
+ − 238
+ − 239 lemma alphas_abs_eqvt:
2469
+ − 240 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
+ − 241 and "(bs, x) \<approx>abs_res (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>abs_res (p \<bullet> cs, p \<bullet> y)"
+ − 242 and "(ds, x) \<approx>abs_lst (es, y) \<Longrightarrow> (p \<bullet> ds, p \<bullet> x) \<approx>abs_lst (p \<bullet> es, p \<bullet> y)"
+ − 243 unfolding alphas_abs
+ − 244 unfolding alphas
+ − 245 unfolding set_eqvt[symmetric]
+ − 246 unfolding supp_eqvt[symmetric]
+ − 247 unfolding Diff_eqvt[symmetric]
+ − 248 apply(erule_tac [!] exE)
+ − 249 apply(rule_tac [!] x="p \<bullet> pa" in exI)
+ − 250 by (auto simp add: fresh_star_permute_iff permute_eqvt[symmetric])
+ − 251
2668
+ − 252
+ − 253 section {* Strengthening the equivalence *}
+ − 254
+ − 255 lemma disjoint_right_eq:
+ − 256 assumes a: "A \<union> B1 = A \<union> B2"
+ − 257 and b: "A \<inter> B1 = {}" "A \<inter> B2 = {}"
+ − 258 shows "B1 = B2"
+ − 259 using a b
+ − 260 by (metis Int_Un_distrib2 Int_absorb2 Int_commute Un_upper2)
+ − 261
+ − 262 lemma supp_property_res:
+ − 263 assumes a: "(as, x) \<approx>res (op =) supp p (as', x')"
+ − 264 shows "p \<bullet> (supp x \<inter> as) = supp x' \<inter> as'"
+ − 265 proof -
+ − 266 from a have "(supp x - as) \<sharp>* p" by (auto simp only: alphas)
+ − 267 then have *: "p \<bullet> (supp x - as) = (supp x - as)"
+ − 268 by (simp add: atom_set_perm_eq)
+ − 269 have "(supp x' - as') \<union> (supp x' \<inter> as') = supp x'" by auto
+ − 270 also have "\<dots> = supp (p \<bullet> x)" using a by (simp add: alphas)
+ − 271 also have "\<dots> = p \<bullet> (supp x)" by (simp add: supp_eqvt)
+ − 272 also have "\<dots> = p \<bullet> ((supp x - as) \<union> (supp x \<inter> as))" by auto
+ − 273 also have "\<dots> = (p \<bullet> (supp x - as)) \<union> (p \<bullet> (supp x \<inter> as))" by (simp add: union_eqvt)
+ − 274 also have "\<dots> = (supp x - as) \<union> (p \<bullet> (supp x \<inter> as))" using * by simp
+ − 275 also have "\<dots> = (supp x' - as') \<union> (p \<bullet> (supp x \<inter> as))" using a by (simp add: alphas)
+ − 276 finally have "(supp x' - as') \<union> (supp x' \<inter> as') = (supp x' - as') \<union> (p \<bullet> (supp x \<inter> as))" .
+ − 277 moreover
+ − 278 have "(supp x' - as') \<inter> (supp x' \<inter> as') = {}" by auto
+ − 279 moreover
+ − 280 have "(supp x - as) \<inter> (supp x \<inter> as) = {}" by auto
+ − 281 then have "p \<bullet> ((supp x - as) \<inter> (supp x \<inter> as) = {})" by (simp add: permute_bool_def)
+ − 282 then have "(p \<bullet> (supp x - as)) \<inter> (p \<bullet> (supp x \<inter> as)) = {}" by (perm_simp) (simp)
+ − 283 then have "(supp x - as) \<inter> (p \<bullet> (supp x \<inter> as)) = {}" using * by simp
+ − 284 then have "(supp x' - as') \<inter> (p \<bullet> (supp x \<inter> as)) = {}" using a by (simp add: alphas)
+ − 285 ultimately show "p \<bullet> (supp x \<inter> as) = supp x' \<inter> as'"
+ − 286 by (auto dest: disjoint_right_eq)
2712
+ − 287 qed
2668
+ − 288
2674
+ − 289 lemma alpha_abs_res_stronger1_aux:
2671
+ − 290 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
+ − 291 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
+ − 292 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
+ − 293 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
+ − 294 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
+ − 295 by (simp add: atom_set_perm_eq)
2673
+ − 296 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"
+ − 297 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
+ − 298 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
+ − 299 from 0 have 1: "(supp x - as) \<sharp>* p" using *
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 by (auto simp add: fresh_star_def fresh_perm)
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 then have 2: "(supp x - as) \<inter> supp p = {}"
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 by (auto simp add: fresh_star_def fresh_def)
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
+ − 303 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
+ − 304 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
+ − 305 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
+ − 306 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
+ − 307 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
+ − 308 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
+ − 309 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
+ − 310 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
+ − 311 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
+ − 312 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
+ − 313 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
+ − 314 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
+ − 315 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
+ − 316 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
+ − 317 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
+ − 318 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
+ − 319 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
+ − 320 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
+ − 321
2712
+ − 322 lemma alpha_abs_res_minimal:
+ − 323 assumes asm: "(as, x) \<approx>res (op =) supp p (as', x')"
+ − 324 shows "(as \<inter> supp x, x) \<approx>res (op =) supp p (as' \<inter> supp x', x')"
+ − 325 using asm unfolding alpha_res by (auto simp add: Diff_Int)
+ − 326
+ − 327 lemma alpha_abs_res_abs_set:
+ − 328 assumes asm: "(as, x) \<approx>res (op =) supp p (as', x')"
+ − 329 shows "(as \<inter> supp x, x) \<approx>set (op =) supp p (as' \<inter> supp x', x')"
+ − 330 proof -
+ − 331 have c: "p \<bullet> x = x'"
+ − 332 using alpha_abs_res_minimal[OF asm] unfolding alpha_res by clarify
+ − 333 then have a: "supp x - as \<inter> supp x = supp (p \<bullet> x) - as' \<inter> supp (p \<bullet> x)"
+ − 334 using alpha_abs_res_minimal[OF asm] by (simp add: alpha_res)
+ − 335 have b: "(supp x - as \<inter> supp x) \<sharp>* p"
+ − 336 using alpha_abs_res_minimal[OF asm] unfolding alpha_res by clarify
+ − 337 have "p \<bullet> (as \<inter> supp x) = as' \<inter> supp (p \<bullet> x)"
+ − 338 by (metis Int_commute asm c supp_property_res)
+ − 339 then show ?thesis using a b c unfolding alpha_set by simp
+ − 340 qed
+ − 341
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
+ − 342 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
+ − 343 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
+ − 344 shows "(as, x) \<approx>res (op =) supp p (as', 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
+ − 345 using asm unfolding alphas by (auto simp add: Diff_Int)
a84999edbcb3
More properties that relate abs_res and abs_set. Also abs_res with less binders.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 346
2674
+ − 347 lemma alpha_abs_res_stronger1:
+ − 348 assumes asm: "(as, x) \<approx>res (op =) supp p' (as', x')"
+ − 349 shows "\<exists>p. (as, x) \<approx>res (op =) supp p (as', x') \<and> supp p \<subseteq> as \<union> as'"
+ − 350 using alpha_abs_res_stronger1_aux[OF asm] by auto
+ − 351
2671
+ − 352 lemma alpha_abs_set_stronger1:
2673
+ − 353 assumes asm: "(as, x) \<approx>set (op =) supp p' (as', x')"
2671
+ − 354 shows "\<exists>p. (as, x) \<approx>set (op =) supp p (as', x') \<and> supp p \<subseteq> as \<union> as'"
+ − 355 proof -
+ − 356 from asm have 0: "(supp x - as) \<sharp>* p'" by (auto simp only: alphas)
+ − 357 then have #: "p' \<bullet> (supp x - as) = (supp x - as)"
+ − 358 by (simp add: atom_set_perm_eq)
2673
+ − 359 obtain p where *: "\<forall>b \<in> (supp x \<union> as). p \<bullet> b = p' \<bullet> b"
+ − 360 and **: "supp p \<subseteq> (supp x \<union> as) \<union> p' \<bullet> (supp x \<union> as)"
+ − 361 using set_renaming_perm2 by blast
2671
+ − 362 from * have "\<forall>b \<in> supp x. p \<bullet> b = p' \<bullet> b" by blast
+ − 363 then have a: "p \<bullet> x = p' \<bullet> x" using supp_perm_perm_eq by auto
+ − 364 from * have "\<forall>b \<in> as. p \<bullet> b = p' \<bullet> b" by blast
2673
+ − 365 then have zb: "p \<bullet> as = p' \<bullet> as"
+ − 366 apply(auto simp add: permute_set_eq)
+ − 367 apply(rule_tac x="xa" in exI)
+ − 368 apply(simp)
+ − 369 done
2671
+ − 370 have zc: "p' \<bullet> as = as'" using asm by (simp add: alphas)
+ − 371 from 0 have 1: "(supp x - as) \<sharp>* p" using *
+ − 372 by (auto simp add: fresh_star_def fresh_perm)
+ − 373 then have 2: "(supp x - as) \<inter> supp p = {}"
+ − 374 by (auto simp add: fresh_star_def fresh_def)
+ − 375 have b: "supp x = (supp x - as) \<union> (supp x \<inter> as)" by auto
+ − 376 have "supp p \<subseteq> supp x \<union> as \<union> p' \<bullet> supp x \<union> p' \<bullet> as" using ** using union_eqvt by blast
+ − 377 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"
+ − 378 using b by simp
2673
+ − 379 also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> as \<union>
+ − 380 ((p' \<bullet> (supp x - as)) \<union> (p' \<bullet> (supp x \<inter> as))) \<union> p' \<bullet> as" by (simp add: union_eqvt)
2671
+ − 381 also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> as \<union> (p' \<bullet> (supp x \<inter> as)) \<union> p' \<bullet> as"
+ − 382 using # by auto
+ − 383 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
+ − 384 by auto
+ − 385 also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> as \<union> p' \<bullet> as"
+ − 386 by (metis Int_commute Un_commute sup_inf_absorb)
2673
+ − 387 also have "\<dots> = (supp x - as) \<union> as \<union> p' \<bullet> as" by blast
2671
+ − 388 finally have "supp p \<subseteq> (supp x - as) \<union> as \<union> p' \<bullet> as" .
+ − 389 then have "supp p \<subseteq> as \<union> p' \<bullet> as" using 2 by blast
+ − 390 moreover
+ − 391 have "(as, x) \<approx>set (op =) supp p (as', x')" using asm 1 a zb by (simp add: alphas)
+ − 392 ultimately
+ − 393 show "\<exists>p. (as, x) \<approx>set (op =) supp p (as', x') \<and> supp p \<subseteq> as \<union> as'" using zc by blast
+ − 394 qed
+ − 395
2674
+ − 396 lemma alpha_abs_lst_stronger1:
+ − 397 assumes asm: "(as, x) \<approx>lst (op =) supp p' (as', x')"
+ − 398 shows "\<exists>p. (as, x) \<approx>lst (op =) supp p (as', x') \<and> supp p \<subseteq> set as \<union> set as'"
+ − 399 proof -
+ − 400 from asm have 0: "(supp x - set as) \<sharp>* p'" by (auto simp only: alphas)
+ − 401 then have #: "p' \<bullet> (supp x - set as) = (supp x - set as)"
+ − 402 by (simp add: atom_set_perm_eq)
+ − 403 obtain p where *: "\<forall>b \<in> (supp x \<union> set as). p \<bullet> b = p' \<bullet> b"
+ − 404 and **: "supp p \<subseteq> (supp x \<union> set as) \<union> p' \<bullet> (supp x \<union> set as)"
+ − 405 using set_renaming_perm2 by blast
+ − 406 from * have "\<forall>b \<in> supp x. p \<bullet> b = p' \<bullet> b" by blast
+ − 407 then have a: "p \<bullet> x = p' \<bullet> x" using supp_perm_perm_eq by auto
+ − 408 from * have "\<forall>b \<in> set as. p \<bullet> b = p' \<bullet> b" by blast
+ − 409 then have zb: "p \<bullet> as = p' \<bullet> as" by (induct as) (auto)
+ − 410 have zc: "p' \<bullet> set as = set as'" using asm by (simp add: alphas set_eqvt)
+ − 411 from 0 have 1: "(supp x - set as) \<sharp>* p" using *
+ − 412 by (auto simp add: fresh_star_def fresh_perm)
+ − 413 then have 2: "(supp x - set as) \<inter> supp p = {}"
+ − 414 by (auto simp add: fresh_star_def fresh_def)
+ − 415 have b: "supp x = (supp x - set as) \<union> (supp x \<inter> set as)" by auto
+ − 416 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
+ − 417 also have "\<dots> = (supp x - set as) \<union> (supp x \<inter> set as) \<union> set as \<union>
+ − 418 (p' \<bullet> ((supp x - set as) \<union> (supp x \<inter> set as))) \<union> p' \<bullet> set as" using b by simp
+ − 419 also have "\<dots> = (supp x - set as) \<union> (supp x \<inter> set as) \<union> set as \<union>
+ − 420 ((p' \<bullet> (supp x - set as)) \<union> (p' \<bullet> (supp x \<inter> set as))) \<union> p' \<bullet> set as" by (simp add: union_eqvt)
+ − 421 also have "\<dots> = (supp x - set as) \<union> (supp x \<inter> set as) \<union> set as \<union>
+ − 422 (p' \<bullet> (supp x \<inter> set as)) \<union> p' \<bullet> set as" using # by auto
+ − 423 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)"
+ − 424 using union_eqvt by auto
+ − 425 also have "\<dots> = (supp x - set as) \<union> (supp x \<inter> set as) \<union> set as \<union> p' \<bullet> set as"
+ − 426 by (metis Int_commute Un_commute sup_inf_absorb)
+ − 427 also have "\<dots> = (supp x - set as) \<union> set as \<union> p' \<bullet> set as" by blast
+ − 428 finally have "supp p \<subseteq> (supp x - set as) \<union> set as \<union> p' \<bullet> set as" .
+ − 429 then have "supp p \<subseteq> set as \<union> p' \<bullet> set as" using 2 by blast
+ − 430 moreover
+ − 431 have "(as, x) \<approx>lst (op =) supp p (as', x')" using asm 1 a zb by (simp add: alphas)
+ − 432 ultimately
+ − 433 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
+ − 434 qed
2668
+ − 435
2674
+ − 436 lemma alphas_abs_stronger:
+ − 437 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')"
+ − 438 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')"
+ − 439 and "(bs, x) \<approx>abs_lst (bs', x') \<longleftrightarrow>
+ − 440 (\<exists>p. (bs, x) \<approx>lst (op =) supp p (bs', x') \<and> supp p \<subseteq> set bs \<union> set bs')"
+ − 441 apply(rule iffI)
+ − 442 apply(auto simp add: alphas_abs alpha_abs_set_stronger1)[1]
+ − 443 apply(auto simp add: alphas_abs)[1]
+ − 444 apply(rule iffI)
+ − 445 apply(auto simp add: alphas_abs alpha_abs_res_stronger1)[1]
+ − 446 apply(auto simp add: alphas_abs)[1]
+ − 447 apply(rule iffI)
+ − 448 apply(auto simp add: alphas_abs alpha_abs_lst_stronger1)[1]
+ − 449 apply(auto simp add: alphas_abs)[1]
+ − 450 done
2668
+ − 451
+ − 452 section {* Quotient types *}
+ − 453
1657
+ − 454 quotient_type
2469
+ − 455 'a abs_set = "(atom set \<times> 'a::pt)" / "alpha_abs_set"
1657
+ − 456 and 'b abs_res = "(atom set \<times> 'b::pt)" / "alpha_abs_res"
+ − 457 and 'c abs_lst = "(atom list \<times> 'c::pt)" / "alpha_abs_lst"
+ − 458 apply(rule_tac [!] equivpI)
2592
+ − 459 unfolding reflp_def refl_on_def symp_def sym_def transp_def trans_def
1657
+ − 460 by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:)
1440
+ − 461
+ − 462 quotient_definition
2469
+ − 463 Abs_set ("[_]set. _" [60, 60] 60)
1932
+ − 464 where
2469
+ − 465 "Abs_set::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_set"
1440
+ − 466 is
+ − 467 "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"
+ − 468
1657
+ − 469 quotient_definition
1932
+ − 470 Abs_res ("[_]res. _" [60, 60] 60)
+ − 471 where
1657
+ − 472 "Abs_res::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_res"
+ − 473 is
+ − 474 "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"
+ − 475
+ − 476 quotient_definition
1932
+ − 477 Abs_lst ("[_]lst. _" [60, 60] 60)
+ − 478 where
1657
+ − 479 "Abs_lst::atom list \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_lst"
+ − 480 is
+ − 481 "Pair::atom list \<Rightarrow> ('a::pt) \<Rightarrow> (atom list \<times> 'a)"
+ − 482
1440
+ − 483 lemma [quot_respect]:
2469
+ − 484 shows "(op= ===> op= ===> alpha_abs_set) Pair Pair"
1657
+ − 485 and "(op= ===> op= ===> alpha_abs_res) Pair Pair"
+ − 486 and "(op= ===> op= ===> alpha_abs_lst) Pair Pair"
+ − 487 unfolding fun_rel_def
2385
+ − 488 by (auto intro: alphas_abs_refl)
1440
+ − 489
+ − 490 lemma [quot_respect]:
2469
+ − 491 shows "(op= ===> alpha_abs_set ===> alpha_abs_set) permute permute"
1657
+ − 492 and "(op= ===> alpha_abs_res ===> alpha_abs_res) permute permute"
+ − 493 and "(op= ===> alpha_abs_lst ===> alpha_abs_lst) permute permute"
+ − 494 unfolding fun_rel_def
+ − 495 by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt)
1440
+ − 496
2491
+ − 497 lemma Abs_eq_iff:
+ − 498 shows "Abs_set bs x = Abs_set cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op =) supp p (cs, y))"
+ − 499 and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))"
+ − 500 and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))"
+ − 501 by (lifting alphas_abs)
+ − 502
2674
+ − 503 lemma Abs_eq_iff2:
+ − 504 shows "Abs_set bs x = Abs_set cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op =) supp p (cs, y) \<and> supp p \<subseteq> bs \<union> cs)"
+ − 505 and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y) \<and> supp p \<subseteq> bs \<union> cs)"
+ − 506 and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow>
+ − 507 (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y) \<and> supp p \<subseteq> set bsl \<union> set csl)"
+ − 508 by (lifting alphas_abs_stronger)
+ − 509
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
+ − 510 lemma Abs_eq_res_set:
a84999edbcb3
More properties that relate abs_res and abs_set. Also abs_res with less binders.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 511 "(([bs]res. x) = ([cs]res. y)) = (([(bs \<inter> supp x)]set. x) = ([(cs \<inter> supp y)]set. y))"
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
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 using alpha_abs_set_abs_res alpha_abs_res_abs_set
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 auto
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 apply (rule_tac x="p" 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
+ − 516 apply assumption
a84999edbcb3
More properties that relate abs_res and abs_set. Also abs_res with less binders.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 517 apply (rule_tac x="p" 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
+ − 518 apply assumption
a84999edbcb3
More properties that relate abs_res and abs_set. Also abs_res with less binders.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 519 done
a84999edbcb3
More properties that relate abs_res and abs_set. Also abs_res with less binders.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 520
a84999edbcb3
More properties that relate abs_res and abs_set. Also abs_res with less binders.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 521 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
+ − 522 assumes asm: "supp x \<subseteq> bs"
a84999edbcb3
More properties that relate abs_res and abs_set. Also abs_res with less binders.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 523 shows "([as]res. x) = ([as \<inter> bs]res. 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
+ − 524 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
+ − 525 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
+ − 526 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
+ − 527 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
+ − 528
2491
+ − 529 lemma Abs_exhausts:
2469
+ − 530 shows "(\<And>as (x::'a::pt). y1 = Abs_set as x \<Longrightarrow> P1) \<Longrightarrow> P1"
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
+ − 531 and "(\<And>as (x::'a::pt). y2 = Abs_res as x \<Longrightarrow> P2) \<Longrightarrow> P2"
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
+ − 532 and "(\<And>as (x::'a::pt). y3 = Abs_lst as x \<Longrightarrow> P3) \<Longrightarrow> P3"
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
+ − 533 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
+ − 534 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
+ − 535 prod.exhaust[where 'a="atom list" and 'b="'a"])
1440
+ − 536
2679
+ − 537
2469
+ − 538 instantiation abs_set :: (pt) pt
1440
+ − 539 begin
+ − 540
+ − 541 quotient_definition
2469
+ − 542 "permute_abs_set::perm \<Rightarrow> ('a::pt abs_set) \<Rightarrow> 'a abs_set"
1440
+ − 543 is
+ − 544 "permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)"
+ − 545
2491
+ − 546 lemma permute_Abs_set[simp]:
1558
+ − 547 fixes x::"'a::pt"
2469
+ − 548 shows "(p \<bullet> (Abs_set as x)) = Abs_set (p \<bullet> as) (p \<bullet> x)"
1657
+ − 549 by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"])
1440
+ − 550
+ − 551 instance
+ − 552 apply(default)
2491
+ − 553 apply(case_tac [!] x rule: Abs_exhausts(1))
1657
+ − 554 apply(simp_all)
+ − 555 done
+ − 556
+ − 557 end
+ − 558
+ − 559 instantiation abs_res :: (pt) pt
+ − 560 begin
+ − 561
+ − 562 quotient_definition
+ − 563 "permute_abs_res::perm \<Rightarrow> ('a::pt abs_res) \<Rightarrow> 'a abs_res"
+ − 564 is
+ − 565 "permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)"
+ − 566
+ − 567 lemma permute_Abs_res[simp]:
+ − 568 fixes x::"'a::pt"
+ − 569 shows "(p \<bullet> (Abs_res as x)) = Abs_res (p \<bullet> as) (p \<bullet> x)"
+ − 570 by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"])
+ − 571
+ − 572 instance
+ − 573 apply(default)
2491
+ − 574 apply(case_tac [!] x rule: Abs_exhausts(2))
1657
+ − 575 apply(simp_all)
+ − 576 done
+ − 577
+ − 578 end
+ − 579
+ − 580 instantiation abs_lst :: (pt) pt
+ − 581 begin
+ − 582
+ − 583 quotient_definition
+ − 584 "permute_abs_lst::perm \<Rightarrow> ('a::pt abs_lst) \<Rightarrow> 'a abs_lst"
+ − 585 is
+ − 586 "permute:: perm \<Rightarrow> (atom list \<times> 'a::pt) \<Rightarrow> (atom list \<times> 'a::pt)"
+ − 587
+ − 588 lemma permute_Abs_lst[simp]:
+ − 589 fixes x::"'a::pt"
+ − 590 shows "(p \<bullet> (Abs_lst as x)) = Abs_lst (p \<bullet> as) (p \<bullet> x)"
+ − 591 by (lifting permute_prod.simps[where 'a="atom list" and 'b="'a"])
+ − 592
+ − 593 instance
+ − 594 apply(default)
2491
+ − 595 apply(case_tac [!] x rule: Abs_exhausts(3))
1440
+ − 596 apply(simp_all)
+ − 597 done
+ − 598
+ − 599 end
+ − 600
2491
+ − 601 lemmas permute_Abs[eqvt] = permute_Abs_set permute_Abs_res permute_Abs_lst
1657
+ − 602
2385
+ − 603
2491
+ − 604 lemma Abs_swap1:
1662
+ − 605 assumes a1: "a \<notin> (supp x) - bs"
+ − 606 and a2: "b \<notin> (supp x) - bs"
2469
+ − 607 shows "Abs_set bs x = Abs_set ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
1662
+ − 608 and "Abs_res bs x = Abs_res ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
2491
+ − 609 unfolding Abs_eq_iff
1662
+ − 610 unfolding alphas
+ − 611 unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric]
+ − 612 unfolding fresh_star_def fresh_def
+ − 613 unfolding swap_set_not_in[OF a1 a2]
+ − 614 using a1 a2
+ − 615 by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)
+ − 616 (auto simp add: supp_perm swap_atom)
+ − 617
2491
+ − 618 lemma Abs_swap2:
1662
+ − 619 assumes a1: "a \<notin> (supp x) - (set bs)"
+ − 620 and a2: "b \<notin> (supp x) - (set bs)"
+ − 621 shows "Abs_lst bs x = Abs_lst ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
2491
+ − 622 unfolding Abs_eq_iff
1662
+ − 623 unfolding alphas
+ − 624 unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] set_eqvt[symmetric]
+ − 625 unfolding fresh_star_def fresh_def
+ − 626 unfolding swap_set_not_in[OF a1 a2]
+ − 627 using a1 a2
+ − 628 by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)
+ − 629 (auto simp add: supp_perm swap_atom)
+ − 630
2491
+ − 631 lemma Abs_supports:
2469
+ − 632 shows "((supp x) - as) supports (Abs_set as x)"
1662
+ − 633 and "((supp x) - as) supports (Abs_res as x)"
2385
+ − 634 and "((supp x) - set bs) supports (Abs_lst bs x)"
1662
+ − 635 unfolding supports_def
2491
+ − 636 unfolding permute_Abs
+ − 637 by (simp_all add: Abs_swap1[symmetric] Abs_swap2[symmetric])
1657
+ − 638
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
+ − 639 function
2469
+ − 640 supp_set :: "('a::pt) abs_set \<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
+ − 641 where
2469
+ − 642 "supp_set (Abs_set as x) = supp x - as"
2491
+ − 643 apply(case_tac x rule: Abs_exhausts(1))
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
+ − 644 apply(simp)
2491
+ − 645 apply(simp add: Abs_eq_iff alphas_abs alphas)
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
2469
+ − 648 termination supp_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
+ − 649 by (auto intro!: local.termination)
1440
+ − 650
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
+ − 651 function
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
+ − 652 supp_res :: "('a::pt) abs_res \<Rightarrow> atom set"
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
+ − 653 where
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
+ − 654 "supp_res (Abs_res as x) = supp x - as"
2491
+ − 655 apply(case_tac x rule: Abs_exhausts(2))
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
+ − 656 apply(simp)
2491
+ − 657 apply(simp add: Abs_eq_iff alphas_abs alphas)
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
+ − 658 done
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
+ − 659
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
+ − 660 termination supp_res
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
+ − 661 by (auto intro!: local.termination)
1440
+ − 662
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
+ − 663 function
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
+ − 664 supp_lst :: "('a::pt) abs_lst \<Rightarrow> atom set"
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
+ − 665 where
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
+ − 666 "supp_lst (Abs_lst cs x) = (supp x) - (set cs)"
2491
+ − 667 apply(case_tac x rule: Abs_exhausts(3))
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
+ − 668 apply(simp)
2491
+ − 669 apply(simp add: Abs_eq_iff alphas_abs alphas)
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
+ − 670 done
1440
+ − 671
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
+ − 672 termination supp_lst
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
+ − 673 by (auto intro!: local.termination)
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
+ − 674
2663
+ − 675 lemma supp_funs_eqvt[eqvt]:
2469
+ − 676 shows "(p \<bullet> supp_set x) = supp_set (p \<bullet> x)"
1657
+ − 677 and "(p \<bullet> supp_res y) = supp_res (p \<bullet> y)"
+ − 678 and "(p \<bullet> supp_lst z) = supp_lst (p \<bullet> z)"
2491
+ − 679 apply(case_tac x rule: Abs_exhausts(1))
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
+ − 680 apply(simp add: supp_eqvt Diff_eqvt)
2491
+ − 681 apply(case_tac y rule: Abs_exhausts(2))
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
+ − 682 apply(simp add: supp_eqvt Diff_eqvt)
2491
+ − 683 apply(case_tac z rule: Abs_exhausts(3))
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
+ − 684 apply(simp add: supp_eqvt Diff_eqvt set_eqvt)
1440
+ − 685 done
+ − 686
2491
+ − 687 lemma Abs_fresh_aux:
2469
+ − 688 shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_set (Abs bs x)"
1657
+ − 689 and "a \<sharp> Abs_res bs x \<Longrightarrow> a \<sharp> supp_res (Abs_res bs x)"
+ − 690 and "a \<sharp> Abs_lst cs x \<Longrightarrow> a \<sharp> supp_lst (Abs_lst cs x)"
1932
+ − 691 by (rule_tac [!] fresh_fun_eqvt_app)
2663
+ − 692 (auto simp only: eqvt_def eqvts_raw)
1657
+ − 693
2491
+ − 694 lemma Abs_supp_subset1:
1657
+ − 695 assumes a: "finite (supp x)"
2469
+ − 696 shows "(supp x) - as \<subseteq> supp (Abs_set as x)"
1657
+ − 697 and "(supp x) - as \<subseteq> supp (Abs_res as x)"
+ − 698 and "(supp x) - (set bs) \<subseteq> supp (Abs_lst bs x)"
+ − 699 unfolding supp_conv_fresh
2491
+ − 700 by (auto dest!: Abs_fresh_aux)
1932
+ − 701 (simp_all add: fresh_def supp_finite_atom_set a)
1440
+ − 702
2491
+ − 703 lemma Abs_supp_subset2:
1657
+ − 704 assumes a: "finite (supp x)"
2469
+ − 705 shows "supp (Abs_set as x) \<subseteq> (supp x) - as"
1657
+ − 706 and "supp (Abs_res as x) \<subseteq> (supp x) - as"
+ − 707 and "supp (Abs_lst bs x) \<subseteq> (supp x) - (set bs)"
1932
+ − 708 by (rule_tac [!] supp_is_subset)
2491
+ − 709 (simp_all add: Abs_supports a)
1478
+ − 710
2491
+ − 711 lemma Abs_finite_supp:
1657
+ − 712 assumes a: "finite (supp x)"
2469
+ − 713 shows "supp (Abs_set as x) = (supp x) - as"
1657
+ − 714 and "supp (Abs_res as x) = (supp x) - as"
+ − 715 and "supp (Abs_lst bs x) = (supp x) - (set bs)"
1932
+ − 716 by (rule_tac [!] subset_antisym)
2491
+ − 717 (simp_all add: Abs_supp_subset1[OF a] Abs_supp_subset2[OF a])
1440
+ − 718
2491
+ − 719 lemma supp_Abs:
1440
+ − 720 fixes x::"'a::fs"
2469
+ − 721 shows "supp (Abs_set as x) = (supp x) - as"
1657
+ − 722 and "supp (Abs_res as x) = (supp x) - as"
+ − 723 and "supp (Abs_lst bs x) = (supp x) - (set bs)"
2491
+ − 724 by (rule_tac [!] Abs_finite_supp)
1932
+ − 725 (simp_all add: finite_supp)
1440
+ − 726
2469
+ − 727 instance abs_set :: (fs) fs
1440
+ − 728 apply(default)
2491
+ − 729 apply(case_tac x rule: Abs_exhausts(1))
+ − 730 apply(simp add: supp_Abs finite_supp)
1440
+ − 731 done
+ − 732
1657
+ − 733 instance abs_res :: (fs) fs
+ − 734 apply(default)
2491
+ − 735 apply(case_tac x rule: Abs_exhausts(2))
+ − 736 apply(simp add: supp_Abs finite_supp)
1657
+ − 737 done
+ − 738
+ − 739 instance abs_lst :: (fs) fs
+ − 740 apply(default)
2491
+ − 741 apply(case_tac x rule: Abs_exhausts(3))
+ − 742 apply(simp add: supp_Abs finite_supp)
1440
+ − 743 done
+ − 744
2491
+ − 745 lemma Abs_fresh_iff:
1657
+ − 746 fixes x::"'a::fs"
2469
+ − 747 shows "a \<sharp> Abs_set bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"
1657
+ − 748 and "a \<sharp> Abs_res bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"
+ − 749 and "a \<sharp> Abs_lst cs x \<longleftrightarrow> a \<in> (set cs) \<or> (a \<notin> (set cs) \<and> a \<sharp> x)"
+ − 750 unfolding fresh_def
2491
+ − 751 unfolding supp_Abs
1657
+ − 752 by auto
1460
+ − 753
2591
+ − 754 lemma Abs_fresh_star_iff:
+ − 755 fixes x::"'a::fs"
+ − 756 shows "as \<sharp>* Abs_set bs x \<longleftrightarrow> (as - bs) \<sharp>* x"
+ − 757 and "as \<sharp>* Abs_res bs x \<longleftrightarrow> (as - bs) \<sharp>* x"
+ − 758 and "as \<sharp>* Abs_lst cs x \<longleftrightarrow> (as - set cs) \<sharp>* x"
+ − 759 unfolding fresh_star_def
+ − 760 by (auto simp add: Abs_fresh_iff)
+ − 761
2491
+ − 762 lemma Abs_fresh_star:
+ − 763 fixes x::"'a::fs"
2584
+ − 764 shows "as \<subseteq> as' \<Longrightarrow> as \<sharp>* Abs_set as' x"
+ − 765 and "as \<subseteq> as' \<Longrightarrow> as \<sharp>* Abs_res as' x"
+ − 766 and "bs \<subseteq> set bs' \<Longrightarrow> bs \<sharp>* Abs_lst bs' x"
2491
+ − 767 unfolding fresh_star_def
2584
+ − 768 by(auto simp add: Abs_fresh_iff)
2468
+ − 769
2730
+ − 770 lemma Abs_fresh_star2:
+ − 771 fixes x::"'a::fs"
+ − 772 shows "as \<inter> bs = {} \<Longrightarrow> as \<sharp>* Abs_set bs x \<longleftrightarrow> as \<sharp>* x"
+ − 773 and "as \<inter> bs = {} \<Longrightarrow> as \<sharp>* Abs_res bs x \<longleftrightarrow> as \<sharp>* x"
+ − 774 and "cs \<inter> set ds = {} \<Longrightarrow> cs \<sharp>* Abs_lst ds x \<longleftrightarrow> cs \<sharp>* x"
+ − 775 unfolding fresh_star_def Abs_fresh_iff
+ − 776 by auto
+ − 777
+ − 778
2679
+ − 779 lemma Abs1_eq:
+ − 780 fixes x::"'a::fs"
+ − 781 shows "Abs_set {a} x = Abs_set {a} y \<longleftrightarrow> x = y"
+ − 782 and "Abs_res {a} x = Abs_res {a} y \<longleftrightarrow> x = y"
+ − 783 and "Abs_lst [c] x = Abs_lst [c] y \<longleftrightarrow> x = y"
+ − 784 unfolding Abs_eq_iff2 alphas
+ − 785 apply(simp_all add: supp_perm_singleton fresh_star_def fresh_zero_perm)
+ − 786 apply(blast)+
+ − 787 done
+ − 788
+ − 789
+ − 790 lemma Abs1_eq_iff:
+ − 791 fixes x::"'a::fs"
+ − 792 assumes "sort_of a = sort_of b"
+ − 793 and "sort_of c = sort_of d"
+ − 794 shows "Abs_set {a} x = Abs_set {b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)"
+ − 795 and "Abs_res {a} x = Abs_res {b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)"
+ − 796 and "Abs_lst [c] x = Abs_lst [d] y \<longleftrightarrow> (c = d \<and> x = y) \<or> (c \<noteq> d \<and> x = (c \<rightleftharpoons> d) \<bullet> y \<and> c \<sharp> y)"
+ − 797 proof -
+ − 798 { assume "a = b"
2683
+ − 799 then have "Abs_set {a} x = Abs_set {b} y \<longleftrightarrow> (a = b \<and> x = y)" by (simp add: Abs1_eq)
2679
+ − 800 }
+ − 801 moreover
+ − 802 { assume *: "a \<noteq> b" and **: "Abs_set {a} x = Abs_set {b} y"
+ − 803 have #: "a \<sharp> Abs_set {b} y" by (simp add: **[symmetric] Abs_fresh_iff)
+ − 804 have "Abs_set {a} ((a \<rightleftharpoons> b) \<bullet> y) = (a \<rightleftharpoons> b) \<bullet> (Abs_set {b} y)" by (simp add: permute_set_eq assms)
+ − 805 also have "\<dots> = Abs_set {b} y"
+ − 806 by (rule swap_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)
+ − 807 also have "\<dots> = Abs_set {a} x" using ** by simp
+ − 808 finally have "a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y" using # * by (simp add: Abs1_eq Abs_fresh_iff)
+ − 809 }
+ − 810 moreover
+ − 811 { assume *: "a \<noteq> b" and **: "x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y"
+ − 812 have "Abs_set {a} x = Abs_set {a} ((a \<rightleftharpoons> b) \<bullet> y)" using ** by simp
+ − 813 also have "\<dots> = (a \<rightleftharpoons> b) \<bullet> Abs_set {b} y" by (simp add: permute_set_eq assms)
+ − 814 also have "\<dots> = Abs_set {b} y"
+ − 815 by (rule swap_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)
+ − 816 finally have "Abs_set {a} x = Abs_set {b} y" .
+ − 817 }
+ − 818 ultimately
+ − 819 show "Abs_set {a} x = Abs_set {b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)"
+ − 820 by blast
+ − 821 next
+ − 822 { assume "a = b"
2683
+ − 823 then have "Abs_res {a} x = Abs_res {b} y \<longleftrightarrow> (a = b \<and> x = y)" by (simp add: Abs1_eq)
2679
+ − 824 }
+ − 825 moreover
+ − 826 { assume *: "a \<noteq> b" and **: "Abs_res {a} x = Abs_res {b} y"
+ − 827 have #: "a \<sharp> Abs_res {b} y" by (simp add: **[symmetric] Abs_fresh_iff)
+ − 828 have "Abs_res {a} ((a \<rightleftharpoons> b) \<bullet> y) = (a \<rightleftharpoons> b) \<bullet> (Abs_res {b} y)" by (simp add: permute_set_eq assms)
+ − 829 also have "\<dots> = Abs_res {b} y"
+ − 830 by (rule swap_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)
+ − 831 also have "\<dots> = Abs_res {a} x" using ** by simp
+ − 832 finally have "a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y" using # * by (simp add: Abs1_eq Abs_fresh_iff)
+ − 833 }
+ − 834 moreover
+ − 835 { assume *: "a \<noteq> b" and **: "x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y"
+ − 836 have "Abs_res {a} x = Abs_res {a} ((a \<rightleftharpoons> b) \<bullet> y)" using ** by simp
+ − 837 also have "\<dots> = (a \<rightleftharpoons> b) \<bullet> Abs_res {b} y" by (simp add: permute_set_eq assms)
+ − 838 also have "\<dots> = Abs_res {b} y"
+ − 839 by (rule swap_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)
+ − 840 finally have "Abs_res {a} x = Abs_res {b} y" .
+ − 841 }
+ − 842 ultimately
+ − 843 show "Abs_res {a} x = Abs_res {b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)"
+ − 844 by blast
+ − 845 next
+ − 846 { assume "c = d"
2683
+ − 847 then have "Abs_lst [c] x = Abs_lst [d] y \<longleftrightarrow> (c = d \<and> x = y)" by (simp add: Abs1_eq)
2679
+ − 848 }
+ − 849 moreover
+ − 850 { assume *: "c \<noteq> d" and **: "Abs_lst [c] x = Abs_lst [d] y"
+ − 851 have #: "c \<sharp> Abs_lst [d] y" by (simp add: **[symmetric] Abs_fresh_iff)
+ − 852 have "Abs_lst [c] ((c \<rightleftharpoons> d) \<bullet> y) = (c \<rightleftharpoons> d) \<bullet> (Abs_lst [d] y)" by (simp add: assms)
+ − 853 also have "\<dots> = Abs_lst [d] y"
+ − 854 by (rule swap_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)
+ − 855 also have "\<dots> = Abs_lst [c] x" using ** by simp
+ − 856 finally have "c \<noteq> d \<and> x = (c \<rightleftharpoons> d) \<bullet> y \<and> c \<sharp> y" using # * by (simp add: Abs1_eq Abs_fresh_iff)
+ − 857 }
+ − 858 moreover
+ − 859 { assume *: "c \<noteq> d" and **: "x = (c \<rightleftharpoons> d) \<bullet> y \<and> c \<sharp> y"
+ − 860 have "Abs_lst [c] x = Abs_lst [c] ((c \<rightleftharpoons> d) \<bullet> y)" using ** by simp
+ − 861 also have "\<dots> = (c \<rightleftharpoons> d) \<bullet> Abs_lst [d] y" by (simp add: assms)
+ − 862 also have "\<dots> = Abs_lst [d] y"
+ − 863 by (rule swap_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)
+ − 864 finally have "Abs_lst [c] x = Abs_lst [d] y" .
+ − 865 }
+ − 866 ultimately
+ − 867 show "Abs_lst [c] x = Abs_lst [d] y \<longleftrightarrow> (c = d \<and> x = y) \<or> (c \<noteq> d \<and> x = (c \<rightleftharpoons> d) \<bullet> y \<and> c \<sharp> y)"
+ − 868 by blast
+ − 869 qed
+ − 870
2683
+ − 871 lemma Abs1_eq_iff':
+ − 872 fixes x::"'a::fs"
+ − 873 assumes "sort_of a = sort_of b"
+ − 874 and "sort_of c = sort_of d"
+ − 875 shows "Abs_set {a} x = Abs_set {b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<rightleftharpoons> a) \<bullet> x = y \<and> b \<sharp> x)"
+ − 876 and "Abs_res {a} x = Abs_res {b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<rightleftharpoons> a) \<bullet> x = y \<and> b \<sharp> x)"
+ − 877 and "Abs_lst [c] x = Abs_lst [d] y \<longleftrightarrow> (c = d \<and> x = y) \<or> (c \<noteq> d \<and> (d \<rightleftharpoons> c) \<bullet> x = y \<and> d \<sharp> x)"
+ − 878 using assms by (auto simp add: Abs1_eq_iff fresh_permute_left)
+ − 879
2468
+ − 880
2599
+ − 881 subsection {* Renaming of bodies of abstractions *}
+ − 882
2674
+ − 883 (* FIXME: finiteness assumption is not needed *)
2599
+ − 884
+ − 885 lemma Abs_rename_set:
+ − 886 fixes x::"'a::fs"
2659
+ − 887 assumes a: "(p \<bullet> bs) \<sharp>* x"
2599
+ − 888 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
+ − 889 shows "\<exists>q. [bs]set. x = [p \<bullet> bs]set. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"
2599
+ − 890 proof -
2659
+ − 891 from b set_renaming_perm
2668
+ − 892 obtain q where *: "\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" by blast
+ − 893 have ***: "q \<bullet> bs = p \<bullet> bs" using b * by (induct) (simp add: permute_set_eq, simp add: insert_eqvt)
2599
+ − 894 have "[bs]set. x = q \<bullet> ([bs]set. x)"
+ − 895 apply(rule perm_supp_eq[symmetric])
+ − 896 using a **
+ − 897 unfolding Abs_fresh_star_iff
+ − 898 unfolding fresh_star_def
+ − 899 by auto
+ − 900 also have "\<dots> = [q \<bullet> bs]set. (q \<bullet> x)" by simp
2668
+ − 901 finally have "[bs]set. x = [p \<bullet> bs]set. (q \<bullet> x)" by (simp add: ***)
+ − 902 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
+ − 903 qed
+ − 904
+ − 905 lemma Abs_rename_res:
+ − 906 fixes x::"'a::fs"
2659
+ − 907 assumes a: "(p \<bullet> bs) \<sharp>* x"
2599
+ − 908 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
+ − 909 shows "\<exists>q. [bs]res. x = [p \<bullet> bs]res. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"
2599
+ − 910 proof -
2659
+ − 911 from b set_renaming_perm
2668
+ − 912 obtain q where *: "\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" by blast
+ − 913 have ***: "q \<bullet> bs = p \<bullet> bs" using b * by (induct) (simp add: permute_set_eq, simp add: insert_eqvt)
2599
+ − 914 have "[bs]res. x = q \<bullet> ([bs]res. x)"
+ − 915 apply(rule perm_supp_eq[symmetric])
+ − 916 using a **
+ − 917 unfolding Abs_fresh_star_iff
+ − 918 unfolding fresh_star_def
+ − 919 by auto
+ − 920 also have "\<dots> = [q \<bullet> bs]res. (q \<bullet> x)" by simp
2668
+ − 921 finally have "[bs]res. x = [p \<bullet> bs]res. (q \<bullet> x)" by (simp add: ***)
+ − 922 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
+ − 923 qed
+ − 924
2611
3d101f2f817c
simple cases for strong inducts done; infrastructure for the difficult ones is there
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 925 lemma Abs_rename_lst:
2599
+ − 926 fixes x::"'a::fs"
2659
+ − 927 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
+ − 928 shows "\<exists>q. [bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"
2599
+ − 929 proof -
2659
+ − 930 from a list_renaming_perm
2668
+ − 931 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
+ − 932 have ***: "q \<bullet> bs = p \<bullet> bs" using * by (induct bs) (simp_all add: insert_eqvt)
2599
+ − 933 have "[bs]lst. x = q \<bullet> ([bs]lst. x)"
+ − 934 apply(rule perm_supp_eq[symmetric])
+ − 935 using a **
+ − 936 unfolding Abs_fresh_star_iff
+ − 937 unfolding fresh_star_def
+ − 938 by auto
+ − 939 also have "\<dots> = [q \<bullet> bs]lst. (q \<bullet> x)" by simp
2668
+ − 940 finally have "[bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x)" by (simp add: ***)
+ − 941 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
+ − 942 qed
+ − 943
+ − 944
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
+ − 945 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
+ − 946
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
+ − 947 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
+ − 948 fixes x::"'a::fs"
2659
+ − 949 assumes a: "(p \<bullet> 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
+ − 950 and b: "finite 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
+ − 951 shows "\<exists>q. [bs]set. x = [q \<bullet> bs]set. (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
+ − 952 using Abs_rename_set[OF a b] by metis
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
+ − 953
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
+ − 954 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
+ − 955 fixes x::"'a::fs"
2659
+ − 956 assumes a: "(p \<bullet> 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
+ − 957 and b: "finite 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
+ − 958 shows "\<exists>q. [bs]res. x = [q \<bullet> bs]res. (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
+ − 959 using Abs_rename_res[OF a b] by metis
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
+ − 960
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
+ − 961 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
+ − 962 fixes x::"'a::fs"
2659
+ − 963 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
+ − 964 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
+ − 965 using Abs_rename_lst[OF a] by metis
2599
+ − 966
2468
+ − 967 section {* Infrastructure for building tuples of relations and functions *}
+ − 968
2385
+ − 969 fun
+ − 970 prod_fv :: "('a \<Rightarrow> atom set) \<Rightarrow> ('b \<Rightarrow> atom set) \<Rightarrow> ('a \<times> 'b) \<Rightarrow> atom set"
+ − 971 where
+ − 972 "prod_fv fv1 fv2 (x, y) = fv1 x \<union> fv2 y"
+ − 973
+ − 974 definition
+ − 975 prod_alpha :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool)"
+ − 976 where
+ − 977 "prod_alpha = prod_rel"
+ − 978
+ − 979 lemma [quot_respect]:
+ − 980 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
+ − 981 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
+ − 982 unfolding prod_rel_def
2385
+ − 983 by auto
+ − 984
+ − 985 lemma [quot_preserve]:
+ − 986 assumes q1: "Quotient R1 abs1 rep1"
+ − 987 and q2: "Quotient R2 abs2 rep2"
2574
+ − 988 shows "((abs1 ---> id) ---> (abs2 ---> id) ---> map_pair rep1 rep2 ---> id) prod_fv = prod_fv"
2479
+ − 989 by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
2385
+ − 990
+ − 991 lemma [mono]:
+ − 992 shows "A <= B \<Longrightarrow> C <= D ==> prod_alpha A C <= prod_alpha B D"
+ − 993 unfolding prod_alpha_def
+ − 994 by auto
+ − 995
+ − 996 lemma [eqvt]:
+ − 997 shows "p \<bullet> prod_alpha A B x y = prod_alpha (p \<bullet> A) (p \<bullet> B) (p \<bullet> x) (p \<bullet> y)"
+ − 998 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
+ − 999 unfolding prod_rel_def
2385
+ − 1000 by (perm_simp) (rule refl)
+ − 1001
+ − 1002 lemma [eqvt]:
+ − 1003 shows "p \<bullet> prod_fv A B (x, y) = prod_fv (p \<bullet> A) (p \<bullet> B) (p \<bullet> x, p \<bullet> y)"
+ − 1004 unfolding prod_fv.simps
+ − 1005 by (perm_simp) (rule refl)
+ − 1006
2489
+ − 1007 lemma prod_fv_supp:
+ − 1008 shows "prod_fv supp supp = supp"
+ − 1009 by (rule ext)
+ − 1010 (auto simp add: prod_fv.simps supp_Pair)
+ − 1011
+ − 1012 lemma prod_alpha_eq:
+ − 1013 shows "prod_alpha (op=) (op=) = (op=)"
+ − 1014 unfolding prod_alpha_def
+ − 1015 by (auto intro!: ext)
+ − 1016
2385
+ − 1017
1440
+ − 1018 end
+ − 1019