1440
+ − 1
theory Abs
2467
+ − 2
imports "../Nominal-General/Nominal2_Base"
1804
+ − 3
"../Nominal-General/Nominal2_Eqvt"
+ − 4
"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
+ − 5
"Quotient_List"
1804
+ − 6
"Quotient_Product"
1440
+ − 7
begin
+ − 8
2473
+ − 9
+ − 10
section {* Abstractions *}
+ − 11
1440
+ − 12
fun
2469
+ − 13
alpha_set
1440
+ − 14
where
2469
+ − 15
alpha_set[simp del]:
+ − 16
"alpha_set (bs, x) R f pi (cs, y) \<longleftrightarrow>
1465
+ − 17
f x - bs = f y - cs \<and>
+ − 18
(f x - bs) \<sharp>* pi \<and>
+ − 19
R (pi \<bullet> x) y \<and>
+ − 20
pi \<bullet> bs = cs"
1440
+ − 21
1557
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 22
fun
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 23
alpha_res
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 24
where
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 25
alpha_res[simp del]:
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 26
"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
+ − 27
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
+ − 28
(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
+ − 29
R (pi \<bullet> x) y"
1440
+ − 30
1557
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 31
fun
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 32
alpha_lst
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 33
where
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 34
alpha_lst[simp del]:
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 35
"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
+ − 36
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
+ − 37
(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
+ − 38
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
+ − 39
pi \<bullet> bs = cs"
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 40
2469
+ − 41
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
+ − 42
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 43
notation
2469
+ − 44
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
+ − 45
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
+ − 46
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
+ − 47
2385
+ − 48
section {* Mono *}
+ − 49
1557
fee2389789ad
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 50
lemma [mono]:
2469
+ − 51
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
+ − 52
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
+ − 53
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
+ − 54
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
+ − 55
(auto simp add: le_fun_def le_bool_def alphas)
1440
+ − 56
2385
+ − 57
section {* Equivariance *}
+ − 58
+ − 59
lemma alpha_eqvt[eqvt]:
2469
+ − 60
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
+ − 61
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)"
+ − 62
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)"
+ − 63
unfolding alphas
+ − 64
unfolding permute_eqvt[symmetric]
+ − 65
unfolding set_eqvt[symmetric]
+ − 66
unfolding permute_fun_app_eq[symmetric]
+ − 67
unfolding Diff_eqvt[symmetric]
+ − 68
by (auto simp add: permute_bool_def fresh_star_permute_iff)
+ − 69
2385
+ − 70
+ − 71
section {* Equivalence *}
+ − 72
+ − 73
lemma alpha_refl:
2311
+ − 74
assumes a: "R x x"
2469
+ − 75
shows "(bs, x) \<approx>set R f 0 (bs, x)"
2311
+ − 76
and "(bs, x) \<approx>res R f 0 (bs, x)"
+ − 77
and "(cs, x) \<approx>lst R f 0 (cs, x)"
+ − 78
using a
+ − 79
unfolding alphas
+ − 80
unfolding fresh_star_def
+ − 81
by (simp_all add: fresh_zero_perm)
+ − 82
2385
+ − 83
lemma alpha_sym:
2311
+ − 84
assumes a: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x"
2469
+ − 85
shows "(bs, x) \<approx>set R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>set R f (- p) (bs, x)"
2311
+ − 86
and "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)"
+ − 87
and "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)"
+ − 88
unfolding alphas fresh_star_def
+ − 89
using a
+ − 90
by (auto simp add: fresh_minus_perm)
+ − 91
2385
+ − 92
lemma alpha_trans:
+ − 93
assumes a: "\<lbrakk>R (p \<bullet> x) y; R (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((q + p) \<bullet> x) z"
2469
+ − 94
shows "\<lbrakk>(bs, x) \<approx>set R f p (cs, y); (cs, y) \<approx>set R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>set R f (q + p) (ds, z)"
2385
+ − 95
and "\<lbrakk>(bs, x) \<approx>res R f p (cs, y); (cs, y) \<approx>res R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>res R f (q + p) (ds, z)"
+ − 96
and "\<lbrakk>(es, x) \<approx>lst R f p (gs, y); (gs, y) \<approx>lst R f q (hs, z)\<rbrakk> \<Longrightarrow> (es, x) \<approx>lst R f (q + p) (hs, z)"
+ − 97
using a
+ − 98
unfolding alphas fresh_star_def
+ − 99
by (simp_all add: fresh_plus_perm)
+ − 100
+ − 101
lemma alpha_sym_eqvt:
2311
+ − 102
assumes a: "R (p \<bullet> x) y \<Longrightarrow> R y (p \<bullet> x)"
+ − 103
and b: "p \<bullet> R = R"
2469
+ − 104
shows "(bs, x) \<approx>set R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>set R f (- p) (bs, x)"
2311
+ − 105
and "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)"
2313
+ − 106
and "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)"
2385
+ − 107
apply(auto intro!: alpha_sym)
2313
+ − 108
apply(drule_tac [!] a)
+ − 109
apply(rule_tac [!] p="p" in permute_boolE)
+ − 110
apply(perm_simp add: permute_minus_cancel b)
+ − 111
apply(assumption)
+ − 112
apply(perm_simp add: permute_minus_cancel b)
+ − 113
apply(assumption)
+ − 114
apply(perm_simp add: permute_minus_cancel b)
+ − 115
apply(assumption)
+ − 116
done
2311
+ − 117
2469
+ − 118
lemma alpha_set_trans_eqvt:
+ − 119
assumes b: "(cs, y) \<approx>set R f q (ds, z)"
+ − 120
and a: "(bs, x) \<approx>set R f p (cs, y)"
2313
+ − 121
and d: "q \<bullet> R = R"
+ − 122
and c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"
2469
+ − 123
shows "(bs, x) \<approx>set R f (q + p) (ds, z)"
2385
+ − 124
apply(rule alpha_trans)
2313
+ − 125
defer
+ − 126
apply(rule a)
+ − 127
apply(rule b)
+ − 128
apply(drule c)
+ − 129
apply(rule_tac p="q" in permute_boolE)
+ − 130
apply(perm_simp add: permute_minus_cancel d)
+ − 131
apply(assumption)
+ − 132
apply(rotate_tac -1)
+ − 133
apply(drule_tac p="q" in permute_boolI)
+ − 134
apply(perm_simp add: permute_minus_cancel d)
+ − 135
apply(simp add: permute_eqvt[symmetric])
+ − 136
done
+ − 137
+ − 138
lemma alpha_res_trans_eqvt:
+ − 139
assumes b: "(cs, y) \<approx>res R f q (ds, z)"
+ − 140
and a: "(bs, x) \<approx>res R f p (cs, y)"
+ − 141
and d: "q \<bullet> R = R"
+ − 142
and c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"
+ − 143
shows "(bs, x) \<approx>res R f (q + p) (ds, z)"
2385
+ − 144
apply(rule alpha_trans)
2313
+ − 145
defer
+ − 146
apply(rule a)
+ − 147
apply(rule b)
+ − 148
apply(drule c)
+ − 149
apply(rule_tac p="q" in permute_boolE)
+ − 150
apply(perm_simp add: permute_minus_cancel d)
+ − 151
apply(assumption)
+ − 152
apply(rotate_tac -1)
+ − 153
apply(drule_tac p="q" in permute_boolI)
+ − 154
apply(perm_simp add: permute_minus_cancel d)
+ − 155
apply(simp add: permute_eqvt[symmetric])
+ − 156
done
+ − 157
+ − 158
lemma alpha_lst_trans_eqvt:
+ − 159
assumes b: "(cs, y) \<approx>lst R f q (ds, z)"
+ − 160
and a: "(bs, x) \<approx>lst R f p (cs, y)"
+ − 161
and d: "q \<bullet> R = R"
+ − 162
and c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"
+ − 163
shows "(bs, x) \<approx>lst R f (q + p) (ds, z)"
2385
+ − 164
apply(rule alpha_trans)
2313
+ − 165
defer
+ − 166
apply(rule a)
+ − 167
apply(rule b)
+ − 168
apply(drule c)
+ − 169
apply(rule_tac p="q" in permute_boolE)
+ − 170
apply(perm_simp add: permute_minus_cancel d)
+ − 171
apply(assumption)
+ − 172
apply(rotate_tac -1)
+ − 173
apply(drule_tac p="q" in permute_boolI)
+ − 174
apply(perm_simp add: permute_minus_cancel d)
+ − 175
apply(simp add: permute_eqvt[symmetric])
+ − 176
done
+ − 177
2469
+ − 178
lemmas alpha_trans_eqvt = alpha_set_trans_eqvt alpha_res_trans_eqvt alpha_lst_trans_eqvt
2313
+ − 179
2311
+ − 180
+ − 181
section {* General Abstractions *}
+ − 182
1440
+ − 183
fun
2469
+ − 184
alpha_abs_set
1440
+ − 185
where
1666
+ − 186
[simp del]:
2469
+ − 187
"alpha_abs_set (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op=) supp p (cs, y))"
1440
+ − 188
1657
+ − 189
fun
+ − 190
alpha_abs_lst
+ − 191
where
1666
+ − 192
[simp del]:
1657
+ − 193
"alpha_abs_lst (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>lst (op=) supp p (cs, y))"
+ − 194
+ − 195
fun
+ − 196
alpha_abs_res
+ − 197
where
1666
+ − 198
[simp del]:
1657
+ − 199
"alpha_abs_res (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op=) supp p (cs, y))"
+ − 200
1440
+ − 201
notation
2469
+ − 202
alpha_abs_set (infix "\<approx>abs'_set" 50) and
1666
+ − 203
alpha_abs_lst (infix "\<approx>abs'_lst" 50) and
+ − 204
alpha_abs_res (infix "\<approx>abs'_res" 50)
1657
+ − 205
2469
+ − 206
lemmas alphas_abs = alpha_abs_set.simps alpha_abs_res.simps alpha_abs_lst.simps
1657
+ − 207
2385
+ − 208
1657
+ − 209
lemma alphas_abs_refl:
2469
+ − 210
shows "(bs, x) \<approx>abs_set (bs, x)"
1657
+ − 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:
2469
+ − 220
shows "(bs, x) \<approx>abs_set (cs, y) \<Longrightarrow> (cs, y) \<approx>abs_set (bs, x)"
1657
+ − 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:
2469
+ − 230
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
+ − 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:
2469
+ − 241
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
+ − 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
2469
+ − 254
'a abs_set = "(atom set \<times> 'a::pt)" / "alpha_abs_set"
1657
+ − 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
2469
+ − 262
Abs_set ("[_]set. _" [60, 60] 60)
1932
+ − 263
where
2469
+ − 264
"Abs_set::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_set"
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]:
2469
+ − 283
shows "(op= ===> op= ===> alpha_abs_set) Pair Pair"
1657
+ − 284
and "(op= ===> op= ===> alpha_abs_res) Pair Pair"
+ − 285
and "(op= ===> op= ===> alpha_abs_lst) Pair Pair"
+ − 286
unfolding fun_rel_def
2385
+ − 287
by (auto intro: alphas_abs_refl)
1440
+ − 288
+ − 289
lemma [quot_respect]:
2469
+ − 290
shows "(op= ===> alpha_abs_set ===> alpha_abs_set) permute permute"
1657
+ − 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
2491
+ − 296
lemma Abs_eq_iff:
+ − 297
shows "Abs_set bs x = Abs_set cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op =) supp p (cs, y))"
+ − 298
and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))"
+ − 299
and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))"
+ − 300
by (lifting alphas_abs)
+ − 301
+ − 302
lemma Abs_exhausts:
2469
+ − 303
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
+ − 304
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
+ − 305
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
+ − 306
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
+ − 307
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
+ − 308
prod.exhaust[where 'a="atom list" and 'b="'a"])
1440
+ − 309
2469
+ − 310
instantiation abs_set :: (pt) pt
1440
+ − 311
begin
+ − 312
+ − 313
quotient_definition
2469
+ − 314
"permute_abs_set::perm \<Rightarrow> ('a::pt abs_set) \<Rightarrow> 'a abs_set"
1440
+ − 315
is
+ − 316
"permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)"
+ − 317
2491
+ − 318
lemma permute_Abs_set[simp]:
1558
+ − 319
fixes x::"'a::pt"
2469
+ − 320
shows "(p \<bullet> (Abs_set as x)) = Abs_set (p \<bullet> as) (p \<bullet> x)"
1657
+ − 321
by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"])
1440
+ − 322
+ − 323
instance
+ − 324
apply(default)
2491
+ − 325
apply(case_tac [!] x rule: Abs_exhausts(1))
1657
+ − 326
apply(simp_all)
+ − 327
done
+ − 328
+ − 329
end
+ − 330
+ − 331
instantiation abs_res :: (pt) pt
+ − 332
begin
+ − 333
+ − 334
quotient_definition
+ − 335
"permute_abs_res::perm \<Rightarrow> ('a::pt abs_res) \<Rightarrow> 'a abs_res"
+ − 336
is
+ − 337
"permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)"
+ − 338
+ − 339
lemma permute_Abs_res[simp]:
+ − 340
fixes x::"'a::pt"
+ − 341
shows "(p \<bullet> (Abs_res as x)) = Abs_res (p \<bullet> as) (p \<bullet> x)"
+ − 342
by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"])
+ − 343
+ − 344
instance
+ − 345
apply(default)
2491
+ − 346
apply(case_tac [!] x rule: Abs_exhausts(2))
1657
+ − 347
apply(simp_all)
+ − 348
done
+ − 349
+ − 350
end
+ − 351
+ − 352
instantiation abs_lst :: (pt) pt
+ − 353
begin
+ − 354
+ − 355
quotient_definition
+ − 356
"permute_abs_lst::perm \<Rightarrow> ('a::pt abs_lst) \<Rightarrow> 'a abs_lst"
+ − 357
is
+ − 358
"permute:: perm \<Rightarrow> (atom list \<times> 'a::pt) \<Rightarrow> (atom list \<times> 'a::pt)"
+ − 359
+ − 360
lemma permute_Abs_lst[simp]:
+ − 361
fixes x::"'a::pt"
+ − 362
shows "(p \<bullet> (Abs_lst as x)) = Abs_lst (p \<bullet> as) (p \<bullet> x)"
+ − 363
by (lifting permute_prod.simps[where 'a="atom list" and 'b="'a"])
+ − 364
+ − 365
instance
+ − 366
apply(default)
2491
+ − 367
apply(case_tac [!] x rule: Abs_exhausts(3))
1440
+ − 368
apply(simp_all)
+ − 369
done
+ − 370
+ − 371
end
+ − 372
2491
+ − 373
lemmas permute_Abs[eqvt] = permute_Abs_set permute_Abs_res permute_Abs_lst
1657
+ − 374
2385
+ − 375
2491
+ − 376
lemma Abs_swap1:
1662
+ − 377
assumes a1: "a \<notin> (supp x) - bs"
+ − 378
and a2: "b \<notin> (supp x) - bs"
2469
+ − 379
shows "Abs_set bs x = Abs_set ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
1662
+ − 380
and "Abs_res bs x = Abs_res ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
2491
+ − 381
unfolding Abs_eq_iff
1662
+ − 382
unfolding alphas
+ − 383
unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric]
+ − 384
unfolding fresh_star_def fresh_def
+ − 385
unfolding swap_set_not_in[OF a1 a2]
+ − 386
using a1 a2
+ − 387
by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)
+ − 388
(auto simp add: supp_perm swap_atom)
+ − 389
2491
+ − 390
lemma Abs_swap2:
1662
+ − 391
assumes a1: "a \<notin> (supp x) - (set bs)"
+ − 392
and a2: "b \<notin> (supp x) - (set bs)"
+ − 393
shows "Abs_lst bs x = Abs_lst ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
2491
+ − 394
unfolding Abs_eq_iff
1662
+ − 395
unfolding alphas
+ − 396
unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] set_eqvt[symmetric]
+ − 397
unfolding fresh_star_def fresh_def
+ − 398
unfolding swap_set_not_in[OF a1 a2]
+ − 399
using a1 a2
+ − 400
by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)
+ − 401
(auto simp add: supp_perm swap_atom)
+ − 402
2491
+ − 403
lemma Abs_supports:
2469
+ − 404
shows "((supp x) - as) supports (Abs_set as x)"
1662
+ − 405
and "((supp x) - as) supports (Abs_res as x)"
2385
+ − 406
and "((supp x) - set bs) supports (Abs_lst bs x)"
1662
+ − 407
unfolding supports_def
2491
+ − 408
unfolding permute_Abs
+ − 409
by (simp_all add: Abs_swap1[symmetric] Abs_swap2[symmetric])
1657
+ − 410
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
+ − 411
function
2469
+ − 412
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
+ − 413
where
2469
+ − 414
"supp_set (Abs_set as x) = supp x - as"
2491
+ − 415
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
+ − 416
apply(simp)
2491
+ − 417
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
+ − 418
done
1657
+ − 419
2469
+ − 420
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
+ − 421
by (auto intro!: local.termination)
1440
+ − 422
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
+ − 423
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
+ − 424
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
+ − 425
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
+ − 426
"supp_res (Abs_res as x) = supp x - as"
2491
+ − 427
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
+ − 428
apply(simp)
2491
+ − 429
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
+ − 430
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
+ − 431
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
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
+ − 433
by (auto intro!: local.termination)
1440
+ − 434
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
+ − 435
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
+ − 436
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
+ − 437
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
+ − 438
"supp_lst (Abs_lst cs x) = (supp x) - (set cs)"
2491
+ − 439
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
+ − 440
apply(simp)
2491
+ − 441
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
+ − 442
done
1440
+ − 443
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
+ − 444
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
+ − 445
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
+ − 446
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
lemma [eqvt]:
2469
+ − 448
shows "(p \<bullet> supp_set x) = supp_set (p \<bullet> x)"
1657
+ − 449
and "(p \<bullet> supp_res y) = supp_res (p \<bullet> y)"
+ − 450
and "(p \<bullet> supp_lst z) = supp_lst (p \<bullet> z)"
2491
+ − 451
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
+ − 452
apply(simp add: supp_eqvt Diff_eqvt)
2491
+ − 453
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
+ − 454
apply(simp add: supp_eqvt Diff_eqvt)
2491
+ − 455
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
+ − 456
apply(simp add: supp_eqvt Diff_eqvt set_eqvt)
1440
+ − 457
done
+ − 458
2491
+ − 459
lemma Abs_fresh_aux:
2469
+ − 460
shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_set (Abs bs x)"
1657
+ − 461
and "a \<sharp> Abs_res bs x \<Longrightarrow> a \<sharp> supp_res (Abs_res bs x)"
+ − 462
and "a \<sharp> Abs_lst cs x \<Longrightarrow> a \<sharp> supp_lst (Abs_lst cs x)"
1932
+ − 463
by (rule_tac [!] fresh_fun_eqvt_app)
2468
+ − 464
(simp_all only: eqvts_raw)
1657
+ − 465
2491
+ − 466
lemma Abs_supp_subset1:
1657
+ − 467
assumes a: "finite (supp x)"
2469
+ − 468
shows "(supp x) - as \<subseteq> supp (Abs_set as x)"
1657
+ − 469
and "(supp x) - as \<subseteq> supp (Abs_res as x)"
+ − 470
and "(supp x) - (set bs) \<subseteq> supp (Abs_lst bs x)"
+ − 471
unfolding supp_conv_fresh
2491
+ − 472
by (auto dest!: Abs_fresh_aux)
1932
+ − 473
(simp_all add: fresh_def supp_finite_atom_set a)
1440
+ − 474
2491
+ − 475
lemma Abs_supp_subset2:
1657
+ − 476
assumes a: "finite (supp x)"
2469
+ − 477
shows "supp (Abs_set as x) \<subseteq> (supp x) - as"
1657
+ − 478
and "supp (Abs_res as x) \<subseteq> (supp x) - as"
+ − 479
and "supp (Abs_lst bs x) \<subseteq> (supp x) - (set bs)"
1932
+ − 480
by (rule_tac [!] supp_is_subset)
2491
+ − 481
(simp_all add: Abs_supports a)
1478
+ − 482
2491
+ − 483
lemma Abs_finite_supp:
1657
+ − 484
assumes a: "finite (supp x)"
2469
+ − 485
shows "supp (Abs_set as x) = (supp x) - as"
1657
+ − 486
and "supp (Abs_res as x) = (supp x) - as"
+ − 487
and "supp (Abs_lst bs x) = (supp x) - (set bs)"
1932
+ − 488
by (rule_tac [!] subset_antisym)
2491
+ − 489
(simp_all add: Abs_supp_subset1[OF a] Abs_supp_subset2[OF a])
1440
+ − 490
2491
+ − 491
lemma supp_Abs:
1440
+ − 492
fixes x::"'a::fs"
2469
+ − 493
shows "supp (Abs_set as x) = (supp x) - as"
1657
+ − 494
and "supp (Abs_res as x) = (supp x) - as"
+ − 495
and "supp (Abs_lst bs x) = (supp x) - (set bs)"
2491
+ − 496
by (rule_tac [!] Abs_finite_supp)
1932
+ − 497
(simp_all add: finite_supp)
1440
+ − 498
2469
+ − 499
instance abs_set :: (fs) fs
1440
+ − 500
apply(default)
2491
+ − 501
apply(case_tac x rule: Abs_exhausts(1))
+ − 502
apply(simp add: supp_Abs finite_supp)
1440
+ − 503
done
+ − 504
1657
+ − 505
instance abs_res :: (fs) fs
+ − 506
apply(default)
2491
+ − 507
apply(case_tac x rule: Abs_exhausts(2))
+ − 508
apply(simp add: supp_Abs finite_supp)
1657
+ − 509
done
+ − 510
+ − 511
instance abs_lst :: (fs) fs
+ − 512
apply(default)
2491
+ − 513
apply(case_tac x rule: Abs_exhausts(3))
+ − 514
apply(simp add: supp_Abs finite_supp)
1440
+ − 515
done
+ − 516
2491
+ − 517
lemma Abs_fresh_iff:
1657
+ − 518
fixes x::"'a::fs"
2469
+ − 519
shows "a \<sharp> Abs_set bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"
1657
+ − 520
and "a \<sharp> Abs_res bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"
+ − 521
and "a \<sharp> Abs_lst cs x \<longleftrightarrow> a \<in> (set cs) \<or> (a \<notin> (set cs) \<and> a \<sharp> x)"
+ − 522
unfolding fresh_def
2491
+ − 523
unfolding supp_Abs
1657
+ − 524
by auto
1460
+ − 525
2491
+ − 526
lemma Abs_fresh_star:
+ − 527
fixes x::"'a::fs"
+ − 528
shows "as \<sharp>* Abs_set as x"
+ − 529
and "as \<sharp>* Abs_res as x"
+ − 530
and "set bs \<sharp>* Abs_lst bs x"
+ − 531
unfolding fresh_star_def
+ − 532
by(simp_all add: Abs_fresh_iff)
2468
+ − 533
+ − 534
+ − 535
section {* Infrastructure for building tuples of relations and functions *}
+ − 536
2385
+ − 537
fun
+ − 538
prod_fv :: "('a \<Rightarrow> atom set) \<Rightarrow> ('b \<Rightarrow> atom set) \<Rightarrow> ('a \<times> 'b) \<Rightarrow> atom set"
+ − 539
where
+ − 540
"prod_fv fv1 fv2 (x, y) = fv1 x \<union> fv2 y"
+ − 541
+ − 542
definition
+ − 543
prod_alpha :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool)"
+ − 544
where
+ − 545
"prod_alpha = prod_rel"
+ − 546
+ − 547
lemma [quot_respect]:
+ − 548
shows "((R1 ===> op =) ===> (R2 ===> op =) ===> prod_rel R1 R2 ===> op =) prod_fv prod_fv"
+ − 549
by auto
+ − 550
+ − 551
lemma [quot_preserve]:
+ − 552
assumes q1: "Quotient R1 abs1 rep1"
+ − 553
and q2: "Quotient R2 abs2 rep2"
+ − 554
shows "((abs1 ---> id) ---> (abs2 ---> id) ---> prod_fun rep1 rep2 ---> id) prod_fv = prod_fv"
2479
+ − 555
by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
2385
+ − 556
+ − 557
lemma [mono]:
+ − 558
shows "A <= B \<Longrightarrow> C <= D ==> prod_alpha A C <= prod_alpha B D"
+ − 559
unfolding prod_alpha_def
+ − 560
by auto
+ − 561
+ − 562
lemma [eqvt]:
+ − 563
shows "p \<bullet> prod_alpha A B x y = prod_alpha (p \<bullet> A) (p \<bullet> B) (p \<bullet> x) (p \<bullet> y)"
+ − 564
unfolding prod_alpha_def
+ − 565
unfolding prod_rel.simps
+ − 566
by (perm_simp) (rule refl)
+ − 567
+ − 568
lemma [eqvt]:
+ − 569
shows "p \<bullet> prod_fv A B (x, y) = prod_fv (p \<bullet> A) (p \<bullet> B) (p \<bullet> x, p \<bullet> y)"
+ − 570
unfolding prod_fv.simps
+ − 571
by (perm_simp) (rule refl)
+ − 572
2489
+ − 573
lemma prod_fv_supp:
+ − 574
shows "prod_fv supp supp = supp"
+ − 575
by (rule ext)
+ − 576
(auto simp add: prod_fv.simps supp_Pair)
+ − 577
+ − 578
lemma prod_alpha_eq:
+ − 579
shows "prod_alpha (op=) (op=) = (op=)"
+ − 580
unfolding prod_alpha_def
+ − 581
by (auto intro!: ext)
+ − 582
2385
+ − 583
1440
+ − 584
end
+ − 585