1440
+ − 1 theory Abs
1804
+ − 2 imports "../Nominal-General/Nominal2_Atoms"
+ − 3 "../Nominal-General/Nominal2_Eqvt"
+ − 4 "../Nominal-General/Nominal2_Supp"
+ − 5 "Quotient"
1933
9eab1dfc14d2
moved lemmas from FSet.thy to do with atom to Nominal2_Base, and to do with 'a::at set to Nominal2_Atoms; moved Nominal2_Eqvt.thy one up to be loaded before Nominal2_Atoms
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 6 "Quotient_List"
1804
+ − 7 "Quotient_Product"
1440
+ − 8 begin
+ − 9
+ − 10 fun
+ − 11 alpha_gen
+ − 12 where
+ − 13 alpha_gen[simp del]:
1465
+ − 14 "alpha_gen (bs, x) R f pi (cs, y) \<longleftrightarrow>
+ − 15 f x - bs = f y - cs \<and>
+ − 16 (f x - bs) \<sharp>* pi \<and>
+ − 17 R (pi \<bullet> x) y \<and>
+ − 18 pi \<bullet> bs = cs"
1440
+ − 19
1557
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 20 fun
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 21 alpha_res
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 22 where
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 23 alpha_res[simp del]:
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 24 "alpha_res (bs, x) R f pi (cs, y) \<longleftrightarrow>
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 25 f x - bs = f y - cs \<and>
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 26 (f x - bs) \<sharp>* pi \<and>
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 27 R (pi \<bullet> x) y"
1440
+ − 28
1557
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 29 fun
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 30 alpha_lst
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 31 where
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 32 alpha_lst[simp del]:
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 33 "alpha_lst (bs, x) R f pi (cs, y) \<longleftrightarrow>
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 34 f x - set bs = f y - set cs \<and>
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 35 (f x - set bs) \<sharp>* pi \<and>
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 36 R (pi \<bullet> x) y \<and>
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 37 pi \<bullet> bs = cs"
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 38
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 39 lemmas alphas = alpha_gen.simps alpha_res.simps alpha_lst.simps
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 40
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 41 notation
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 42 alpha_gen ("_ \<approx>gen _ _ _ _" [100, 100, 100, 100, 100] 100) and
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 43 alpha_res ("_ \<approx>res _ _ _ _" [100, 100, 100, 100, 100] 100) and
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 44 alpha_lst ("_ \<approx>lst _ _ _ _" [100, 100, 100, 100, 100] 100)
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 45
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 46 (* monos *)
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 47 lemma [mono]:
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 48 shows "R1 \<le> R2 \<Longrightarrow> alpha_gen bs R1 \<le> alpha_gen bs R2"
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 49 and "R1 \<le> R2 \<Longrightarrow> alpha_res bs R1 \<le> alpha_res bs R2"
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 50 and "R1 \<le> R2 \<Longrightarrow> alpha_lst cs R1 \<le> alpha_lst cs R2"
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 51 by (case_tac [!] bs, case_tac [!] cs)
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 52 (auto simp add: le_fun_def le_bool_def alphas)
1440
+ − 53
2311
+ − 54 (* equivariance *)
+ − 55 lemma alpha_gen_eqvt[eqvt]:
+ − 56 shows "(bs, x) \<approx>gen R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>gen (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
+ − 57 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)"
+ − 58 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)"
+ − 59 unfolding alphas
+ − 60 unfolding permute_eqvt[symmetric]
+ − 61 unfolding set_eqvt[symmetric]
+ − 62 unfolding permute_fun_app_eq[symmetric]
+ − 63 unfolding Diff_eqvt[symmetric]
+ − 64 by (auto simp add: permute_bool_def fresh_star_permute_iff)
+ − 65
+ − 66 (* equivalence *)
+ − 67 lemma alpha_gen_refl:
+ − 68 assumes a: "R x x"
+ − 69 shows "(bs, x) \<approx>gen R f 0 (bs, x)"
+ − 70 and "(bs, x) \<approx>res R f 0 (bs, x)"
+ − 71 and "(cs, x) \<approx>lst R f 0 (cs, x)"
+ − 72 using a
+ − 73 unfolding alphas
+ − 74 unfolding fresh_star_def
+ − 75 by (simp_all add: fresh_zero_perm)
+ − 76
+ − 77 lemma alpha_gen_sym:
+ − 78 assumes a: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x"
+ − 79 shows "(bs, x) \<approx>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)"
+ − 80 and "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)"
+ − 81 and "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)"
+ − 82 unfolding alphas fresh_star_def
+ − 83 using a
+ − 84 by (auto simp add: fresh_minus_perm)
+ − 85
+ − 86 lemma alpha_gen_sym_eqvt:
+ − 87 assumes a: "R (p \<bullet> x) y \<Longrightarrow> R y (p \<bullet> x)"
+ − 88 and b: "p \<bullet> R = R"
+ − 89 shows "(bs, x) \<approx>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)"
+ − 90 and "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)"
2313
+ − 91 and "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)"
+ − 92 apply(auto intro!: alpha_gen_sym)
+ − 93 apply(drule_tac [!] a)
+ − 94 apply(rule_tac [!] p="p" in permute_boolE)
+ − 95 apply(perm_simp add: permute_minus_cancel b)
+ − 96 apply(assumption)
+ − 97 apply(perm_simp add: permute_minus_cancel b)
+ − 98 apply(assumption)
+ − 99 apply(perm_simp add: permute_minus_cancel b)
+ − 100 apply(assumption)
+ − 101 done
2311
+ − 102
+ − 103 lemma alpha_gen_trans:
+ − 104 assumes a: "\<lbrakk>R (p \<bullet> x) y; R (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((q + p) \<bullet> x) z"
+ − 105 shows "\<lbrakk>(bs, x) \<approx>gen R f p (cs, y); (cs, y) \<approx>gen R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>gen R f (q + p) (ds, z)"
+ − 106 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)"
+ − 107 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)"
+ − 108 using a
+ − 109 unfolding alphas fresh_star_def
+ − 110 by (simp_all add: fresh_plus_perm)
+ − 111
+ − 112
2313
+ − 113 lemma alpha_gen_trans_eqvt:
+ − 114 assumes b: "(cs, y) \<approx>gen R f q (ds, z)"
+ − 115 and a: "(bs, x) \<approx>gen R f p (cs, y)"
+ − 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)"
+ − 118 shows "(bs, x) \<approx>gen R f (q + p) (ds, z)"
+ − 119 apply(rule alpha_gen_trans)
+ − 120 defer
+ − 121 apply(rule a)
+ − 122 apply(rule b)
+ − 123 apply(drule c)
+ − 124 apply(rule_tac p="q" in permute_boolE)
+ − 125 apply(perm_simp add: permute_minus_cancel d)
+ − 126 apply(assumption)
+ − 127 apply(rotate_tac -1)
+ − 128 apply(drule_tac p="q" in permute_boolI)
+ − 129 apply(perm_simp add: permute_minus_cancel d)
+ − 130 apply(simp add: permute_eqvt[symmetric])
+ − 131 done
+ − 132
+ − 133 lemma alpha_res_trans_eqvt:
+ − 134 assumes b: "(cs, y) \<approx>res R f q (ds, z)"
+ − 135 and a: "(bs, x) \<approx>res R f p (cs, y)"
+ − 136 and d: "q \<bullet> R = R"
+ − 137 and c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"
+ − 138 shows "(bs, x) \<approx>res R f (q + p) (ds, z)"
+ − 139 apply(rule alpha_gen_trans)
+ − 140 defer
+ − 141 apply(rule a)
+ − 142 apply(rule b)
+ − 143 apply(drule c)
+ − 144 apply(rule_tac p="q" in permute_boolE)
+ − 145 apply(perm_simp add: permute_minus_cancel d)
+ − 146 apply(assumption)
+ − 147 apply(rotate_tac -1)
+ − 148 apply(drule_tac p="q" in permute_boolI)
+ − 149 apply(perm_simp add: permute_minus_cancel d)
+ − 150 apply(simp add: permute_eqvt[symmetric])
+ − 151 done
+ − 152
+ − 153 lemma alpha_lst_trans_eqvt:
+ − 154 assumes b: "(cs, y) \<approx>lst R f q (ds, z)"
+ − 155 and a: "(bs, x) \<approx>lst R f p (cs, y)"
+ − 156 and d: "q \<bullet> R = R"
+ − 157 and c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"
+ − 158 shows "(bs, x) \<approx>lst R f (q + p) (ds, z)"
+ − 159 apply(rule alpha_gen_trans)
+ − 160 defer
+ − 161 apply(rule a)
+ − 162 apply(rule b)
+ − 163 apply(drule c)
+ − 164 apply(rule_tac p="q" in permute_boolE)
+ − 165 apply(perm_simp add: permute_minus_cancel d)
+ − 166 apply(assumption)
+ − 167 apply(rotate_tac -1)
+ − 168 apply(drule_tac p="q" in permute_boolI)
+ − 169 apply(perm_simp add: permute_minus_cancel d)
+ − 170 apply(simp add: permute_eqvt[symmetric])
+ − 171 done
+ − 172
+ − 173 lemmas alpha_trans_eqvt = alpha_gen_trans_eqvt alpha_res_trans_eqvt alpha_lst_trans_eqvt
+ − 174
+ − 175 lemma test:
+ − 176 shows "(as, t) \<approx>gen R f pi (bs, s) \<Longrightarrow> R (pi \<bullet> t) s"
+ − 177 and "(as, t) \<approx>res R f pi (bs, s) \<Longrightarrow> R (pi \<bullet> t) s"
+ − 178 and "(cs, t) \<approx>lst R f pi (ds, s) \<Longrightarrow> R (pi \<bullet> t) s"
+ − 179 by (simp_all add: alphas)
+ − 180
2311
+ − 181
+ − 182 section {* General Abstractions *}
+ − 183
1440
+ − 184 fun
+ − 185 alpha_abs
+ − 186 where
1666
+ − 187 [simp del]:
1558
+ − 188 "alpha_abs (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))"
1440
+ − 189
1657
+ − 190 fun
+ − 191 alpha_abs_lst
+ − 192 where
1666
+ − 193 [simp del]:
1657
+ − 194 "alpha_abs_lst (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>lst (op=) supp p (cs, y))"
+ − 195
+ − 196 fun
+ − 197 alpha_abs_res
+ − 198 where
1666
+ − 199 [simp del]:
1657
+ − 200 "alpha_abs_res (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op=) supp p (cs, y))"
+ − 201
1440
+ − 202 notation
1666
+ − 203 alpha_abs (infix "\<approx>abs" 50) and
+ − 204 alpha_abs_lst (infix "\<approx>abs'_lst" 50) and
+ − 205 alpha_abs_res (infix "\<approx>abs'_res" 50)
1657
+ − 206
+ − 207 lemmas alphas_abs = alpha_abs.simps alpha_abs_res.simps alpha_abs_lst.simps
+ − 208
+ − 209 lemma alphas_abs_refl:
+ − 210 shows "(bs, x) \<approx>abs (bs, x)"
+ − 211 and "(bs, x) \<approx>abs_res (bs, x)"
+ − 212 and "(cs, x) \<approx>abs_lst (cs, x)"
+ − 213 unfolding alphas_abs
+ − 214 unfolding alphas
+ − 215 unfolding fresh_star_def
+ − 216 by (rule_tac [!] x="0" in exI)
+ − 217 (simp_all add: fresh_zero_perm)
+ − 218
+ − 219 lemma alphas_abs_sym:
+ − 220 shows "(bs, x) \<approx>abs (cs, y) \<Longrightarrow> (cs, y) \<approx>abs (bs, x)"
+ − 221 and "(bs, x) \<approx>abs_res (cs, y) \<Longrightarrow> (cs, y) \<approx>abs_res (bs, x)"
+ − 222 and "(ds, x) \<approx>abs_lst (es, y) \<Longrightarrow> (es, y) \<approx>abs_lst (ds, x)"
+ − 223 unfolding alphas_abs
+ − 224 unfolding alphas
+ − 225 unfolding fresh_star_def
+ − 226 by (erule_tac [!] exE, rule_tac [!] x="-p" in exI)
+ − 227 (auto simp add: fresh_minus_perm)
1440
+ − 228
1657
+ − 229 lemma alphas_abs_trans:
+ − 230 shows "\<lbrakk>(bs, x) \<approx>abs (cs, y); (cs, y) \<approx>abs (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>abs (ds, z)"
+ − 231 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)"
+ − 232 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)"
+ − 233 unfolding alphas_abs
+ − 234 unfolding alphas
+ − 235 unfolding fresh_star_def
+ − 236 apply(erule_tac [!] exE, erule_tac [!] exE)
+ − 237 apply(rule_tac [!] x="pa + p" in exI)
+ − 238 by (simp_all add: fresh_plus_perm)
+ − 239
+ − 240 lemma alphas_abs_eqvt:
+ − 241 shows "(bs, x) \<approx>abs (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>abs (p \<bullet> cs, p \<bullet> y)"
+ − 242 and "(bs, x) \<approx>abs_res (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>abs_res (p \<bullet> cs, p \<bullet> y)"
+ − 243 and "(ds, x) \<approx>abs_lst (es, y) \<Longrightarrow> (p \<bullet> ds, p \<bullet> x) \<approx>abs_lst (p \<bullet> es, p \<bullet> y)"
+ − 244 unfolding alphas_abs
+ − 245 unfolding alphas
+ − 246 unfolding set_eqvt[symmetric]
+ − 247 unfolding supp_eqvt[symmetric]
+ − 248 unfolding Diff_eqvt[symmetric]
+ − 249 apply(erule_tac [!] exE)
+ − 250 apply(rule_tac [!] x="p \<bullet> pa" in exI)
+ − 251 by (auto simp add: fresh_star_permute_iff permute_eqvt[symmetric])
+ − 252
+ − 253 quotient_type
+ − 254 'a abs_gen = "(atom set \<times> 'a::pt)" / "alpha_abs"
+ − 255 and 'b abs_res = "(atom set \<times> 'b::pt)" / "alpha_abs_res"
+ − 256 and 'c abs_lst = "(atom list \<times> 'c::pt)" / "alpha_abs_lst"
+ − 257 apply(rule_tac [!] equivpI)
1440
+ − 258 unfolding reflp_def symp_def transp_def
1657
+ − 259 by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:)
1440
+ − 260
+ − 261 quotient_definition
1932
+ − 262 Abs ("[_]set. _" [60, 60] 60)
+ − 263 where
1558
+ − 264 "Abs::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_gen"
1440
+ − 265 is
+ − 266 "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"
+ − 267
1657
+ − 268 quotient_definition
1932
+ − 269 Abs_res ("[_]res. _" [60, 60] 60)
+ − 270 where
1657
+ − 271 "Abs_res::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_res"
+ − 272 is
+ − 273 "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"
+ − 274
+ − 275 quotient_definition
1932
+ − 276 Abs_lst ("[_]lst. _" [60, 60] 60)
+ − 277 where
1657
+ − 278 "Abs_lst::atom list \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_lst"
+ − 279 is
+ − 280 "Pair::atom list \<Rightarrow> ('a::pt) \<Rightarrow> (atom list \<times> 'a)"
+ − 281
1440
+ − 282 lemma [quot_respect]:
1657
+ − 283 shows "(op= ===> op= ===> alpha_abs) Pair Pair"
+ − 284 and "(op= ===> op= ===> alpha_abs_res) Pair Pair"
+ − 285 and "(op= ===> op= ===> alpha_abs_lst) Pair Pair"
+ − 286 unfolding fun_rel_def
+ − 287 by (auto intro: alphas_abs_refl simp only:)
1440
+ − 288
+ − 289 lemma [quot_respect]:
1657
+ − 290 shows "(op= ===> alpha_abs ===> alpha_abs) permute permute"
+ − 291 and "(op= ===> alpha_abs_res ===> alpha_abs_res) permute permute"
+ − 292 and "(op= ===> alpha_abs_lst ===> alpha_abs_lst) permute permute"
+ − 293 unfolding fun_rel_def
+ − 294 by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt)
1440
+ − 295
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
+ − 296 lemma abs_exhausts:
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
+ − 297 shows "(\<And>as (x::'a::pt). y1 = Abs as x \<Longrightarrow> P1) \<Longrightarrow> P1"
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
+ − 298 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
+ − 299 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
+ − 300 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
+ − 301 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
+ − 302 prod.exhaust[where 'a="atom list" and 'b="'a"])
1440
+ − 303
1662
+ − 304 lemma abs_eq_iff:
+ − 305 shows "Abs bs x = Abs cs y \<longleftrightarrow> (bs, x) \<approx>abs (cs, y)"
+ − 306 and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (bs, x) \<approx>abs_res (cs, y)"
+ − 307 and "Abs_lst ds x = Abs_lst hs y \<longleftrightarrow> (ds, x) \<approx>abs_lst (hs, y)"
1932
+ − 308 unfolding alphas_abs
+ − 309 by (lifting alphas_abs)
1662
+ − 310
1558
+ − 311 instantiation abs_gen :: (pt) pt
1440
+ − 312 begin
+ − 313
+ − 314 quotient_definition
1558
+ − 315 "permute_abs_gen::perm \<Rightarrow> ('a::pt abs_gen) \<Rightarrow> 'a abs_gen"
1440
+ − 316 is
+ − 317 "permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)"
+ − 318
1657
+ − 319 lemma permute_Abs[simp]:
1558
+ − 320 fixes x::"'a::pt"
1440
+ − 321 shows "(p \<bullet> (Abs as x)) = Abs (p \<bullet> as) (p \<bullet> x)"
1657
+ − 322 by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"])
1440
+ − 323
+ − 324 instance
+ − 325 apply(default)
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
+ − 326 apply(case_tac [!] x rule: abs_exhausts(1))
1657
+ − 327 apply(simp_all)
+ − 328 done
+ − 329
+ − 330 end
+ − 331
+ − 332 instantiation abs_res :: (pt) pt
+ − 333 begin
+ − 334
+ − 335 quotient_definition
+ − 336 "permute_abs_res::perm \<Rightarrow> ('a::pt abs_res) \<Rightarrow> 'a abs_res"
+ − 337 is
+ − 338 "permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)"
+ − 339
+ − 340 lemma permute_Abs_res[simp]:
+ − 341 fixes x::"'a::pt"
+ − 342 shows "(p \<bullet> (Abs_res as x)) = Abs_res (p \<bullet> as) (p \<bullet> x)"
+ − 343 by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"])
+ − 344
+ − 345 instance
+ − 346 apply(default)
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
+ − 347 apply(case_tac [!] x rule: abs_exhausts(2))
1657
+ − 348 apply(simp_all)
+ − 349 done
+ − 350
+ − 351 end
+ − 352
+ − 353 instantiation abs_lst :: (pt) pt
+ − 354 begin
+ − 355
+ − 356 quotient_definition
+ − 357 "permute_abs_lst::perm \<Rightarrow> ('a::pt abs_lst) \<Rightarrow> 'a abs_lst"
+ − 358 is
+ − 359 "permute:: perm \<Rightarrow> (atom list \<times> 'a::pt) \<Rightarrow> (atom list \<times> 'a::pt)"
+ − 360
+ − 361 lemma permute_Abs_lst[simp]:
+ − 362 fixes x::"'a::pt"
+ − 363 shows "(p \<bullet> (Abs_lst as x)) = Abs_lst (p \<bullet> as) (p \<bullet> x)"
+ − 364 by (lifting permute_prod.simps[where 'a="atom list" and 'b="'a"])
+ − 365
+ − 366 instance
+ − 367 apply(default)
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
+ − 368 apply(case_tac [!] x rule: abs_exhausts(3))
1440
+ − 369 apply(simp_all)
+ − 370 done
+ − 371
+ − 372 end
+ − 373
1657
+ − 374 lemmas permute_abs = permute_Abs permute_Abs_res permute_Abs_lst
+ − 375
1662
+ − 376 lemma abs_swap1:
+ − 377 assumes a1: "a \<notin> (supp x) - bs"
+ − 378 and a2: "b \<notin> (supp x) - bs"
+ − 379 shows "Abs bs x = Abs ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
+ − 380 and "Abs_res bs x = Abs_res ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
+ − 381 unfolding abs_eq_iff
+ − 382 unfolding alphas_abs
+ − 383 unfolding alphas
+ − 384 unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric]
+ − 385 unfolding fresh_star_def fresh_def
+ − 386 unfolding swap_set_not_in[OF a1 a2]
+ − 387 using a1 a2
+ − 388 by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)
+ − 389 (auto simp add: supp_perm swap_atom)
+ − 390
+ − 391 lemma abs_swap2:
+ − 392 assumes a1: "a \<notin> (supp x) - (set bs)"
+ − 393 and a2: "b \<notin> (supp x) - (set bs)"
+ − 394 shows "Abs_lst bs x = Abs_lst ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
+ − 395 unfolding abs_eq_iff
+ − 396 unfolding alphas_abs
+ − 397 unfolding alphas
+ − 398 unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] set_eqvt[symmetric]
+ − 399 unfolding fresh_star_def fresh_def
+ − 400 unfolding swap_set_not_in[OF a1 a2]
+ − 401 using a1 a2
+ − 402 by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)
+ − 403 (auto simp add: supp_perm swap_atom)
+ − 404
+ − 405 lemma abs_supports:
+ − 406 shows "((supp x) - as) supports (Abs as x)"
+ − 407 and "((supp x) - as) supports (Abs_res as x)"
+ − 408 and "((supp x) - (set bs)) supports (Abs_lst bs x)"
+ − 409 unfolding supports_def
+ − 410 unfolding permute_abs
+ − 411 by (simp_all add: abs_swap1[symmetric] abs_swap2[symmetric])
1657
+ − 412
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
+ − 413 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
+ − 414 supp_gen :: "('a::pt) abs_gen \<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
+ − 415 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
+ − 416 "supp_gen (Abs as x) = supp x - as"
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
+ − 417 apply(case_tac x rule: abs_exhausts(1))
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
+ − 418 apply(simp)
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
+ − 419 apply(simp add: abs_eq_iff alphas_abs alphas)
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
+ − 420 done
1657
+ − 421
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
+ − 422 termination supp_gen
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
+ − 423 by (auto intro!: local.termination)
1440
+ − 424
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
+ − 425 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
+ − 426 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
+ − 427 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
+ − 428 "supp_res (Abs_res as x) = supp x - as"
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
+ − 429 apply(case_tac x rule: abs_exhausts(2))
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
+ − 430 apply(simp)
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
+ − 431 apply(simp add: abs_eq_iff alphas_abs alphas)
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
+ − 432 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
+ − 433
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
+ − 434 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
+ − 435 by (auto intro!: local.termination)
1440
+ − 436
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
+ − 437 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
+ − 438 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
+ − 439 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
+ − 440 "supp_lst (Abs_lst cs x) = (supp x) - (set cs)"
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
+ − 441 apply(case_tac x rule: abs_exhausts(3))
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
+ − 442 apply(simp)
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
+ − 443 apply(simp add: abs_eq_iff alphas_abs alphas)
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
+ − 444 done
1440
+ − 445
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
+ − 446 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
+ − 447 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
+ − 448
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
+ − 449 lemma [eqvt]:
1657
+ − 450 shows "(p \<bullet> supp_gen x) = supp_gen (p \<bullet> x)"
+ − 451 and "(p \<bullet> supp_res y) = supp_res (p \<bullet> y)"
+ − 452 and "(p \<bullet> supp_lst z) = supp_lst (p \<bullet> z)"
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
+ − 453 apply(case_tac x rule: abs_exhausts(1))
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
+ − 454 apply(simp add: supp_eqvt Diff_eqvt)
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
+ − 455 apply(case_tac y rule: abs_exhausts(2))
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
+ − 456 apply(simp add: supp_eqvt Diff_eqvt)
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
+ − 457 apply(case_tac z rule: abs_exhausts(3))
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
+ − 458 apply(simp add: supp_eqvt Diff_eqvt set_eqvt)
1440
+ − 459 done
+ − 460
1657
+ − 461 lemma aux_fresh:
+ − 462 shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_gen (Abs bs x)"
+ − 463 and "a \<sharp> Abs_res bs x \<Longrightarrow> a \<sharp> supp_res (Abs_res bs x)"
+ − 464 and "a \<sharp> Abs_lst cs x \<Longrightarrow> a \<sharp> supp_lst (Abs_lst cs x)"
1932
+ − 465 by (rule_tac [!] fresh_fun_eqvt_app)
+ − 466 (simp_all add: eqvts_raw)
1657
+ − 467
+ − 468 lemma supp_abs_subset1:
+ − 469 assumes a: "finite (supp x)"
1440
+ − 470 shows "(supp x) - as \<subseteq> supp (Abs as x)"
1657
+ − 471 and "(supp x) - as \<subseteq> supp (Abs_res as x)"
+ − 472 and "(supp x) - (set bs) \<subseteq> supp (Abs_lst bs x)"
+ − 473 unfolding supp_conv_fresh
1932
+ − 474 by (auto dest!: aux_fresh)
+ − 475 (simp_all add: fresh_def supp_finite_atom_set a)
1440
+ − 476
1657
+ − 477 lemma supp_abs_subset2:
+ − 478 assumes a: "finite (supp x)"
1440
+ − 479 shows "supp (Abs as x) \<subseteq> (supp x) - as"
1657
+ − 480 and "supp (Abs_res as x) \<subseteq> (supp x) - as"
+ − 481 and "supp (Abs_lst bs x) \<subseteq> (supp x) - (set bs)"
1932
+ − 482 by (rule_tac [!] supp_is_subset)
+ − 483 (simp_all add: abs_supports a)
1478
+ − 484
1657
+ − 485 lemma abs_finite_supp:
+ − 486 assumes a: "finite (supp x)"
1478
+ − 487 shows "supp (Abs as x) = (supp x) - as"
1657
+ − 488 and "supp (Abs_res as x) = (supp x) - as"
+ − 489 and "supp (Abs_lst bs x) = (supp x) - (set bs)"
1932
+ − 490 by (rule_tac [!] subset_antisym)
+ − 491 (simp_all add: supp_abs_subset1[OF a] supp_abs_subset2[OF a])
1440
+ − 492
1657
+ − 493 lemma supp_abs:
1440
+ − 494 fixes x::"'a::fs"
+ − 495 shows "supp (Abs as x) = (supp x) - as"
1657
+ − 496 and "supp (Abs_res as x) = (supp x) - as"
+ − 497 and "supp (Abs_lst bs x) = (supp x) - (set bs)"
1932
+ − 498 by (rule_tac [!] abs_finite_supp)
+ − 499 (simp_all add: finite_supp)
1440
+ − 500
1558
+ − 501 instance abs_gen :: (fs) fs
1440
+ − 502 apply(default)
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
+ − 503 apply(case_tac x rule: abs_exhausts(1))
1657
+ − 504 apply(simp add: supp_abs finite_supp)
1440
+ − 505 done
+ − 506
1657
+ − 507 instance abs_res :: (fs) fs
+ − 508 apply(default)
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
+ − 509 apply(case_tac x rule: abs_exhausts(2))
1657
+ − 510 apply(simp add: supp_abs finite_supp)
+ − 511 done
+ − 512
+ − 513 instance abs_lst :: (fs) fs
+ − 514 apply(default)
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
+ − 515 apply(case_tac x rule: abs_exhausts(3))
1657
+ − 516 apply(simp add: supp_abs finite_supp)
1440
+ − 517 done
+ − 518
1657
+ − 519 lemma abs_fresh_iff:
+ − 520 fixes x::"'a::fs"
+ − 521 shows "a \<sharp> Abs bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"
+ − 522 and "a \<sharp> Abs_res bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"
+ − 523 and "a \<sharp> Abs_lst cs x \<longleftrightarrow> a \<in> (set cs) \<or> (a \<notin> (set cs) \<and> a \<sharp> x)"
+ − 524 unfolding fresh_def
+ − 525 unfolding supp_abs
+ − 526 by auto
1460
+ − 527
1657
+ − 528 section {* BELOW is stuff that may or may not be needed *}
1440
+ − 529
+ − 530 lemma supp_atom_image:
+ − 531 fixes as::"'a::at_base set"
+ − 532 shows "supp (atom ` as) = supp as"
+ − 533 apply(simp add: supp_def)
+ − 534 apply(simp add: image_eqvt)
1933
9eab1dfc14d2
moved lemmas from FSet.thy to do with atom to Nominal2_Base, and to do with 'a::at set to Nominal2_Atoms; moved Nominal2_Eqvt.thy one up to be loaded before Nominal2_Atoms
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 535 apply(simp add: eqvts_raw)
1440
+ − 536 apply(simp add: atom_image_cong)
+ − 537 done
+ − 538
2324
+ − 539 lemma swap_atom_image_fresh:
+ − 540 "\<lbrakk>a \<sharp> atom ` (fn :: ('a :: at_base set)); b \<sharp> atom ` fn\<rbrakk> \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> fn = fn"
1460
+ − 541 apply (simp add: fresh_def)
+ − 542 apply (simp add: supp_atom_image)
+ − 543 apply (fold fresh_def)
+ − 544 apply (simp add: swap_fresh_fresh)
1440
+ − 545 done
+ − 546
1467
+ − 547 (* TODO: The following lemmas can be moved somewhere... *)
1657
+ − 548
+ − 549 lemma Abs_eq_iff:
+ − 550 shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"
1675
+ − 551 and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))"
+ − 552 and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))"
+ − 553 by (lifting alphas_abs)
1657
+ − 554
1467
+ − 555 lemma split_rsp2[quot_respect]: "((R1 ===> R2 ===> prod_rel R1 R2 ===> op =) ===>
+ − 556 prod_rel R1 R2 ===> prod_rel R1 R2 ===> op =) split split"
+ − 557 by auto
+ − 558
+ − 559 lemma split_prs2[quot_preserve]:
+ − 560 assumes q1: "Quotient R1 Abs1 Rep1"
+ − 561 and q2: "Quotient R2 Abs2 Rep2"
+ − 562 shows "((Abs1 ---> Abs2 ---> prod_fun Abs1 Abs2 ---> id) ---> prod_fun Rep1 Rep2 ---> prod_fun Rep1 Rep2 ---> id) split = split"
+ − 563 by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
+ − 564
1673
e8cf0520c820
New compose lemmas. Reverted alpha_gen sym/trans changes. Equivp for alpha_res should work now.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 565 lemma alphas2:
1467
+ − 566 "(bs, x1, x2) \<approx>gen (\<lambda>(x1, y1) (x2, y2). R1 x1 x2 \<and> R2 y1 y2) (\<lambda>(a, b). f1 a \<union> f2 b) pi (cs, y1, y2) =
1470
+ − 567 (f1 x1 \<union> f2 x2 - bs = f1 y1 \<union> f2 y2 - cs \<and> (f1 x1 \<union> f2 x2 - bs) \<sharp>* pi \<and> R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2
+ − 568 \<and> pi \<bullet> bs = cs)"
1673
e8cf0520c820
New compose lemmas. Reverted alpha_gen sym/trans changes. Equivp for alpha_res should work now.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 569 "(bs, x1, x2) \<approx>res (\<lambda>(x1, y1) (x2, y2). R1 x1 x2 \<and> R2 y1 y2) (\<lambda>(a, b). f1 a \<union> f2 b) pi (cs, y1, y2) =
e8cf0520c820
New compose lemmas. Reverted alpha_gen sym/trans changes. Equivp for alpha_res should work now.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 570 (f1 x1 \<union> f2 x2 - bs = f1 y1 \<union> f2 y2 - cs \<and> (f1 x1 \<union> f2 x2 - bs) \<sharp>* pi \<and> R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2)"
e8cf0520c820
New compose lemmas. Reverted alpha_gen sym/trans changes. Equivp for alpha_res should work now.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 571 "(bsl, x1, x2) \<approx>lst (\<lambda>(x1, y1) (x2, y2). R1 x1 x2 \<and> R2 y1 y2) (\<lambda>(a, b). f1 a \<union> f2 b) pi (csl, y1, y2) =
e8cf0520c820
New compose lemmas. Reverted alpha_gen sym/trans changes. Equivp for alpha_res should work now.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 572 (f1 x1 \<union> f2 x2 - set bsl = f1 y1 \<union> f2 y2 - set csl \<and> (f1 x1 \<union> f2 x2 - set bsl) \<sharp>* pi \<and> R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2
e8cf0520c820
New compose lemmas. Reverted alpha_gen sym/trans changes. Equivp for alpha_res should work now.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 573 \<and> pi \<bullet> bsl = csl)"
e8cf0520c820
New compose lemmas. Reverted alpha_gen sym/trans changes. Equivp for alpha_res should work now.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 574 by (simp_all add: alphas)
1544
+ − 575
1744
+ − 576 lemma alphas3:
+ − 577 "(bsl, x1, x2, x3) \<approx>lst (\<lambda>(x1, y1, z1) (x2, y2, z2). R1 x1 x2 \<and> R2 y1 y2 \<and> R3 z1 z2) (\<lambda>(a, b, c). f1 a \<union> (f2 b \<union> f3 c)) pi (csl, y1, y2, y3) = (f1 x1 \<union> (f2 x2 \<union> f3 x3) - set bsl = f1 y1 \<union> (f2 y2 \<union> f3 y3) - set csl \<and>
+ − 578 (f1 x1 \<union> (f2 x2 \<union> f3 x3) - set bsl) \<sharp>* pi \<and>
+ − 579 R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2 \<and> R3 (pi \<bullet> x3) y3 \<and> pi \<bullet> bsl = csl)"
+ − 580 by (simp add: alphas)
+ − 581
1691
+ − 582 lemma alpha_gen_simpler:
+ − 583 assumes fv_rsp: "\<And>x y. R y x \<Longrightarrow> f x = f y"
+ − 584 and fin_fv: "finite (f x)"
+ − 585 and fv_eqvt: "pi \<bullet> f x = f (pi \<bullet> x)"
+ − 586 shows "alpha_gen (bs, x) R f pi (cs, y) \<longleftrightarrow>
+ − 587 (f x - bs) \<sharp>* pi \<and>
+ − 588 R (pi \<bullet> x) y \<and>
+ − 589 pi \<bullet> bs = cs"
+ − 590 apply rule
+ − 591 unfolding alpha_gen
+ − 592 apply clarify
+ − 593 apply (erule conjE)+
+ − 594 apply (simp)
+ − 595 apply (subgoal_tac "f y - cs = pi \<bullet> (f x - bs)")
+ − 596 apply (rule sym)
+ − 597 apply simp
+ − 598 apply (rule supp_perm_eq)
+ − 599 apply (subst supp_finite_atom_set)
+ − 600 apply (rule finite_Diff)
+ − 601 apply (rule fin_fv)
+ − 602 apply (assumption)
+ − 603 apply (simp add: eqvts fv_eqvt)
+ − 604 apply (subst fv_rsp)
+ − 605 apply assumption
+ − 606 apply (simp)
+ − 607 done
+ − 608
+ − 609 lemma alpha_lst_simpler:
+ − 610 assumes fv_rsp: "\<And>x y. R y x \<Longrightarrow> f x = f y"
+ − 611 and fin_fv: "finite (f x)"
+ − 612 and fv_eqvt: "pi \<bullet> f x = f (pi \<bullet> x)"
+ − 613 shows "alpha_lst (bs, x) R f pi (cs, y) \<longleftrightarrow>
+ − 614 (f x - set bs) \<sharp>* pi \<and>
+ − 615 R (pi \<bullet> x) y \<and>
+ − 616 pi \<bullet> bs = cs"
+ − 617 apply rule
+ − 618 unfolding alpha_lst
+ − 619 apply clarify
+ − 620 apply (erule conjE)+
+ − 621 apply (simp)
+ − 622 apply (subgoal_tac "f y - set cs = pi \<bullet> (f x - set bs)")
+ − 623 apply (rule sym)
+ − 624 apply simp
+ − 625 apply (rule supp_perm_eq)
+ − 626 apply (subst supp_finite_atom_set)
+ − 627 apply (rule finite_Diff)
+ − 628 apply (rule fin_fv)
+ − 629 apply (assumption)
+ − 630 apply (simp add: eqvts fv_eqvt)
+ − 631 apply (subst fv_rsp)
+ − 632 apply assumption
+ − 633 apply (simp)
+ − 634 done
+ − 635
2068
+ − 636 fun
+ − 637 prod_fv :: "('a \<Rightarrow> atom set) \<Rightarrow> ('b \<Rightarrow> atom set) \<Rightarrow> ('a \<times> 'b) \<Rightarrow> atom set"
+ − 638 where
+ − 639 "prod_fv fvx fvy (x, y) = (fvx x \<union> fvy y)"
+ − 640
2296
+ − 641 definition
+ − 642 prod_alpha :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool)"
+ − 643 where
+ − 644 "prod_alpha = prod_rel"
+ − 645
+ − 646
2068
+ − 647 lemma [quot_respect]:
2296
+ − 648 shows "((R1 ===> op =) ===> (R2 ===> op =) ===> prod_rel R1 R2 ===> op =) prod_fv prod_fv"
2068
+ − 649 by auto
+ − 650
+ − 651 lemma [quot_preserve]:
+ − 652 assumes q1: "Quotient R1 abs1 rep1"
+ − 653 and q2: "Quotient R2 abs2 rep2"
+ − 654 shows "((abs1 ---> id) ---> (abs2 ---> id) ---> prod_fun rep1 rep2 ---> id) prod_fv = prod_fv"
+ − 655 by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
1691
+ − 656
2296
+ − 657 lemma [mono]:
2302
+ − 658 shows "A <= B \<Longrightarrow> C <= D ==> prod_alpha A C <= prod_alpha B D"
+ − 659 unfolding prod_alpha_def
2092
+ − 660 by auto
+ − 661
2124
+ − 662 lemma [eqvt]:
2296
+ − 663 shows "p \<bullet> prod_alpha A B x y = prod_alpha (p \<bullet> A) (p \<bullet> B) (p \<bullet> x) (p \<bullet> y)"
+ − 664 unfolding prod_alpha_def
2124
+ − 665 unfolding prod_rel.simps
+ − 666 by (perm_simp) (rule refl)
2092
+ − 667
2124
+ − 668 lemma [eqvt]:
+ − 669 shows "p \<bullet> prod_fv A B (x, y) = prod_fv (p \<bullet> A) (p \<bullet> B) (p \<bullet> x, p \<bullet> y)"
+ − 670 unfolding prod_fv.simps
+ − 671 by (perm_simp) (rule refl)
2092
+ − 672
2302
+ − 673
1440
+ − 674 end
+ − 675