1440
+ − 1
theory Abs
1804
+ − 2
imports "../Nominal-General/Nominal2_Atoms"
+ − 3
"../Nominal-General/Nominal2_Eqvt"
+ − 4
"../Nominal-General/Nominal2_Supp"
1807
+ − 5
"Nominal2_FSet"
1804
+ − 6
"Quotient"
+ − 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
+ − 54
fun
+ − 55
alpha_abs
+ − 56
where
1666
+ − 57
[simp del]:
1558
+ − 58
"alpha_abs (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))"
1440
+ − 59
1657
+ − 60
fun
+ − 61
alpha_abs_lst
+ − 62
where
1666
+ − 63
[simp del]:
1657
+ − 64
"alpha_abs_lst (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>lst (op=) supp p (cs, y))"
+ − 65
+ − 66
fun
+ − 67
alpha_abs_res
+ − 68
where
1666
+ − 69
[simp del]:
1657
+ − 70
"alpha_abs_res (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op=) supp p (cs, y))"
+ − 71
1440
+ − 72
notation
1666
+ − 73
alpha_abs (infix "\<approx>abs" 50) and
+ − 74
alpha_abs_lst (infix "\<approx>abs'_lst" 50) and
+ − 75
alpha_abs_res (infix "\<approx>abs'_res" 50)
1657
+ − 76
+ − 77
lemmas alphas_abs = alpha_abs.simps alpha_abs_res.simps alpha_abs_lst.simps
+ − 78
+ − 79
lemma alphas_abs_refl:
+ − 80
shows "(bs, x) \<approx>abs (bs, x)"
+ − 81
and "(bs, x) \<approx>abs_res (bs, x)"
+ − 82
and "(cs, x) \<approx>abs_lst (cs, x)"
+ − 83
unfolding alphas_abs
+ − 84
unfolding alphas
+ − 85
unfolding fresh_star_def
+ − 86
by (rule_tac [!] x="0" in exI)
+ − 87
(simp_all add: fresh_zero_perm)
+ − 88
+ − 89
lemma alphas_abs_sym:
+ − 90
shows "(bs, x) \<approx>abs (cs, y) \<Longrightarrow> (cs, y) \<approx>abs (bs, x)"
+ − 91
and "(bs, x) \<approx>abs_res (cs, y) \<Longrightarrow> (cs, y) \<approx>abs_res (bs, x)"
+ − 92
and "(ds, x) \<approx>abs_lst (es, y) \<Longrightarrow> (es, y) \<approx>abs_lst (ds, x)"
+ − 93
unfolding alphas_abs
+ − 94
unfolding alphas
+ − 95
unfolding fresh_star_def
+ − 96
by (erule_tac [!] exE, rule_tac [!] x="-p" in exI)
+ − 97
(auto simp add: fresh_minus_perm)
1440
+ − 98
1657
+ − 99
lemma alphas_abs_trans:
+ − 100
shows "\<lbrakk>(bs, x) \<approx>abs (cs, y); (cs, y) \<approx>abs (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>abs (ds, z)"
+ − 101
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)"
+ − 102
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)"
+ − 103
unfolding alphas_abs
+ − 104
unfolding alphas
+ − 105
unfolding fresh_star_def
+ − 106
apply(erule_tac [!] exE, erule_tac [!] exE)
+ − 107
apply(rule_tac [!] x="pa + p" in exI)
+ − 108
by (simp_all add: fresh_plus_perm)
+ − 109
+ − 110
lemma alphas_abs_eqvt:
+ − 111
shows "(bs, x) \<approx>abs (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>abs (p \<bullet> cs, p \<bullet> y)"
+ − 112
and "(bs, x) \<approx>abs_res (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>abs_res (p \<bullet> cs, p \<bullet> y)"
+ − 113
and "(ds, x) \<approx>abs_lst (es, y) \<Longrightarrow> (p \<bullet> ds, p \<bullet> x) \<approx>abs_lst (p \<bullet> es, p \<bullet> y)"
+ − 114
unfolding alphas_abs
+ − 115
unfolding alphas
+ − 116
unfolding set_eqvt[symmetric]
+ − 117
unfolding supp_eqvt[symmetric]
+ − 118
unfolding Diff_eqvt[symmetric]
+ − 119
apply(erule_tac [!] exE)
+ − 120
apply(rule_tac [!] x="p \<bullet> pa" in exI)
+ − 121
by (auto simp add: fresh_star_permute_iff permute_eqvt[symmetric])
+ − 122
+ − 123
quotient_type
+ − 124
'a abs_gen = "(atom set \<times> 'a::pt)" / "alpha_abs"
+ − 125
and 'b abs_res = "(atom set \<times> 'b::pt)" / "alpha_abs_res"
+ − 126
and 'c abs_lst = "(atom list \<times> 'c::pt)" / "alpha_abs_lst"
+ − 127
apply(rule_tac [!] equivpI)
1440
+ − 128
unfolding reflp_def symp_def transp_def
1657
+ − 129
by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:)
1440
+ − 130
+ − 131
quotient_definition
1558
+ − 132
"Abs::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_gen"
1440
+ − 133
is
+ − 134
"Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"
+ − 135
1657
+ − 136
quotient_definition
+ − 137
"Abs_res::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_res"
+ − 138
is
+ − 139
"Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"
+ − 140
+ − 141
quotient_definition
+ − 142
"Abs_lst::atom list \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_lst"
+ − 143
is
+ − 144
"Pair::atom list \<Rightarrow> ('a::pt) \<Rightarrow> (atom list \<times> 'a)"
+ − 145
1440
+ − 146
lemma [quot_respect]:
1657
+ − 147
shows "(op= ===> op= ===> alpha_abs) Pair Pair"
+ − 148
and "(op= ===> op= ===> alpha_abs_res) Pair Pair"
+ − 149
and "(op= ===> op= ===> alpha_abs_lst) Pair Pair"
+ − 150
unfolding fun_rel_def
+ − 151
by (auto intro: alphas_abs_refl simp only:)
1440
+ − 152
+ − 153
lemma [quot_respect]:
1657
+ − 154
shows "(op= ===> alpha_abs ===> alpha_abs) permute permute"
+ − 155
and "(op= ===> alpha_abs_res ===> alpha_abs_res) permute permute"
+ − 156
and "(op= ===> alpha_abs_lst ===> alpha_abs_lst) permute permute"
+ − 157
unfolding fun_rel_def
+ − 158
by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt)
1440
+ − 159
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
+ − 160
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
+ − 161
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
+ − 162
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
+ − 163
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
+ − 164
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
+ − 165
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
+ − 166
prod.exhaust[where 'a="atom list" and 'b="'a"])
1440
+ − 167
1662
+ − 168
lemma abs_eq_iff:
+ − 169
shows "Abs bs x = Abs cs y \<longleftrightarrow> (bs, x) \<approx>abs (cs, y)"
+ − 170
and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (bs, x) \<approx>abs_res (cs, y)"
+ − 171
and "Abs_lst ds x = Abs_lst hs y \<longleftrightarrow> (ds, x) \<approx>abs_lst (hs, y)"
1666
+ − 172
apply(simp_all add: alphas_abs)
1662
+ − 173
apply(lifting alphas_abs)
+ − 174
done
+ − 175
1558
+ − 176
instantiation abs_gen :: (pt) pt
1440
+ − 177
begin
+ − 178
+ − 179
quotient_definition
1558
+ − 180
"permute_abs_gen::perm \<Rightarrow> ('a::pt abs_gen) \<Rightarrow> 'a abs_gen"
1440
+ − 181
is
+ − 182
"permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)"
+ − 183
1657
+ − 184
lemma permute_Abs[simp]:
1558
+ − 185
fixes x::"'a::pt"
1440
+ − 186
shows "(p \<bullet> (Abs as x)) = Abs (p \<bullet> as) (p \<bullet> x)"
1657
+ − 187
by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"])
1440
+ − 188
+ − 189
instance
+ − 190
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
+ − 191
apply(case_tac [!] x rule: abs_exhausts(1))
1657
+ − 192
apply(simp_all)
+ − 193
done
+ − 194
+ − 195
end
+ − 196
+ − 197
instantiation abs_res :: (pt) pt
+ − 198
begin
+ − 199
+ − 200
quotient_definition
+ − 201
"permute_abs_res::perm \<Rightarrow> ('a::pt abs_res) \<Rightarrow> 'a abs_res"
+ − 202
is
+ − 203
"permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)"
+ − 204
+ − 205
lemma permute_Abs_res[simp]:
+ − 206
fixes x::"'a::pt"
+ − 207
shows "(p \<bullet> (Abs_res as x)) = Abs_res (p \<bullet> as) (p \<bullet> x)"
+ − 208
by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"])
+ − 209
+ − 210
instance
+ − 211
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
+ − 212
apply(case_tac [!] x rule: abs_exhausts(2))
1657
+ − 213
apply(simp_all)
+ − 214
done
+ − 215
+ − 216
end
+ − 217
+ − 218
instantiation abs_lst :: (pt) pt
+ − 219
begin
+ − 220
+ − 221
quotient_definition
+ − 222
"permute_abs_lst::perm \<Rightarrow> ('a::pt abs_lst) \<Rightarrow> 'a abs_lst"
+ − 223
is
+ − 224
"permute:: perm \<Rightarrow> (atom list \<times> 'a::pt) \<Rightarrow> (atom list \<times> 'a::pt)"
+ − 225
+ − 226
lemma permute_Abs_lst[simp]:
+ − 227
fixes x::"'a::pt"
+ − 228
shows "(p \<bullet> (Abs_lst as x)) = Abs_lst (p \<bullet> as) (p \<bullet> x)"
+ − 229
by (lifting permute_prod.simps[where 'a="atom list" and 'b="'a"])
+ − 230
+ − 231
instance
+ − 232
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
+ − 233
apply(case_tac [!] x rule: abs_exhausts(3))
1440
+ − 234
apply(simp_all)
+ − 235
done
+ − 236
+ − 237
end
+ − 238
1657
+ − 239
lemmas permute_abs = permute_Abs permute_Abs_res permute_Abs_lst
+ − 240
1662
+ − 241
lemma abs_swap1:
+ − 242
assumes a1: "a \<notin> (supp x) - bs"
+ − 243
and a2: "b \<notin> (supp x) - bs"
+ − 244
shows "Abs bs x = Abs ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
+ − 245
and "Abs_res bs x = Abs_res ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
+ − 246
unfolding abs_eq_iff
+ − 247
unfolding alphas_abs
+ − 248
unfolding alphas
+ − 249
unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric]
+ − 250
unfolding fresh_star_def fresh_def
+ − 251
unfolding swap_set_not_in[OF a1 a2]
+ − 252
using a1 a2
+ − 253
by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)
+ − 254
(auto simp add: supp_perm swap_atom)
+ − 255
+ − 256
lemma abs_swap2:
+ − 257
assumes a1: "a \<notin> (supp x) - (set bs)"
+ − 258
and a2: "b \<notin> (supp x) - (set bs)"
+ − 259
shows "Abs_lst bs x = Abs_lst ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
+ − 260
unfolding abs_eq_iff
+ − 261
unfolding alphas_abs
+ − 262
unfolding alphas
+ − 263
unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] set_eqvt[symmetric]
+ − 264
unfolding fresh_star_def fresh_def
+ − 265
unfolding swap_set_not_in[OF a1 a2]
+ − 266
using a1 a2
+ − 267
by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)
+ − 268
(auto simp add: supp_perm swap_atom)
+ − 269
+ − 270
lemma abs_supports:
+ − 271
shows "((supp x) - as) supports (Abs as x)"
+ − 272
and "((supp x) - as) supports (Abs_res as x)"
+ − 273
and "((supp x) - (set bs)) supports (Abs_lst bs x)"
+ − 274
unfolding supports_def
+ − 275
unfolding permute_abs
+ − 276
by (simp_all add: abs_swap1[symmetric] abs_swap2[symmetric])
1657
+ − 277
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
+ − 278
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
+ − 279
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
+ − 280
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
+ − 281
"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
+ − 282
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
+ − 283
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
+ − 284
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
+ − 285
done
1657
+ − 286
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
+ − 287
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
+ − 288
by (auto intro!: local.termination)
1440
+ − 289
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
+ − 290
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
+ − 291
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
+ − 292
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
+ − 293
"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
+ − 294
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
+ − 295
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
+ − 296
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
+ − 297
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
+ − 298
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
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
+ − 300
by (auto intro!: local.termination)
1440
+ − 301
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
+ − 302
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
+ − 303
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
+ − 304
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
+ − 305
"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
+ − 306
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
+ − 307
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
+ − 308
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
+ − 309
done
1440
+ − 310
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
+ − 311
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
+ − 312
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
+ − 313
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
+ − 314
lemma [eqvt]:
1657
+ − 315
shows "(p \<bullet> supp_gen x) = supp_gen (p \<bullet> x)"
+ − 316
and "(p \<bullet> supp_res y) = supp_res (p \<bullet> y)"
+ − 317
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
+ − 318
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
+ − 319
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
+ − 320
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
+ − 321
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
+ − 322
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
+ − 323
apply(simp add: supp_eqvt Diff_eqvt set_eqvt)
1440
+ − 324
done
+ − 325
1657
+ − 326
lemma aux_fresh:
+ − 327
shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_gen (Abs bs x)"
+ − 328
and "a \<sharp> Abs_res bs x \<Longrightarrow> a \<sharp> supp_res (Abs_res bs x)"
+ − 329
and "a \<sharp> Abs_lst cs x \<Longrightarrow> a \<sharp> supp_lst (Abs_lst cs x)"
+ − 330
apply(rule_tac [!] fresh_fun_eqvt_app)
+ − 331
apply(simp_all add: eqvts_raw)
+ − 332
done
+ − 333
+ − 334
lemma supp_abs_subset1:
+ − 335
assumes a: "finite (supp x)"
1440
+ − 336
shows "(supp x) - as \<subseteq> supp (Abs as x)"
1657
+ − 337
and "(supp x) - as \<subseteq> supp (Abs_res as x)"
+ − 338
and "(supp x) - (set bs) \<subseteq> supp (Abs_lst bs x)"
+ − 339
unfolding supp_conv_fresh
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
+ − 340
apply(auto dest!: aux_fresh)
1657
+ − 341
apply(simp_all add: fresh_def supp_finite_atom_set a)
1440
+ − 342
done
+ − 343
1657
+ − 344
lemma supp_abs_subset2:
+ − 345
assumes a: "finite (supp x)"
1440
+ − 346
shows "supp (Abs as x) \<subseteq> (supp x) - as"
1657
+ − 347
and "supp (Abs_res as x) \<subseteq> (supp x) - as"
+ − 348
and "supp (Abs_lst bs x) \<subseteq> (supp x) - (set bs)"
+ − 349
apply(rule_tac [!] supp_is_subset)
+ − 350
apply(simp_all add: abs_supports a)
1478
+ − 351
done
+ − 352
1657
+ − 353
lemma abs_finite_supp:
+ − 354
assumes a: "finite (supp x)"
1478
+ − 355
shows "supp (Abs as x) = (supp x) - as"
1657
+ − 356
and "supp (Abs_res as x) = (supp x) - as"
+ − 357
and "supp (Abs_lst bs x) = (supp x) - (set bs)"
+ − 358
apply(rule_tac [!] subset_antisym)
+ − 359
apply(simp_all add: supp_abs_subset1[OF a] supp_abs_subset2[OF a])
1440
+ − 360
done
+ − 361
1657
+ − 362
lemma supp_abs:
1440
+ − 363
fixes x::"'a::fs"
+ − 364
shows "supp (Abs as x) = (supp x) - as"
1657
+ − 365
and "supp (Abs_res as x) = (supp x) - as"
+ − 366
and "supp (Abs_lst bs x) = (supp x) - (set bs)"
+ − 367
apply(rule_tac [!] abs_finite_supp)
+ − 368
apply(simp_all add: finite_supp)
1440
+ − 369
done
+ − 370
1558
+ − 371
instance abs_gen :: (fs) fs
1440
+ − 372
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
+ − 373
apply(case_tac x rule: abs_exhausts(1))
1657
+ − 374
apply(simp add: supp_abs finite_supp)
1440
+ − 375
done
+ − 376
1657
+ − 377
instance abs_res :: (fs) fs
+ − 378
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
+ − 379
apply(case_tac x rule: abs_exhausts(2))
1657
+ − 380
apply(simp add: supp_abs finite_supp)
+ − 381
done
+ − 382
+ − 383
instance abs_lst :: (fs) fs
+ − 384
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
+ − 385
apply(case_tac x rule: abs_exhausts(3))
1657
+ − 386
apply(simp add: supp_abs finite_supp)
1440
+ − 387
done
+ − 388
1657
+ − 389
lemma abs_fresh_iff:
+ − 390
fixes x::"'a::fs"
+ − 391
shows "a \<sharp> Abs bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"
+ − 392
and "a \<sharp> Abs_res bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"
+ − 393
and "a \<sharp> Abs_lst cs x \<longleftrightarrow> a \<in> (set cs) \<or> (a \<notin> (set cs) \<and> a \<sharp> x)"
+ − 394
unfolding fresh_def
+ − 395
unfolding supp_abs
+ − 396
by auto
1460
+ − 397
1657
+ − 398
section {* BELOW is stuff that may or may not be needed *}
1440
+ − 399
1919
+ − 400
1440
+ − 401
lemma supp_atom_image:
+ − 402
fixes as::"'a::at_base set"
+ − 403
shows "supp (atom ` as) = supp as"
+ − 404
apply(simp add: supp_def)
+ − 405
apply(simp add: image_eqvt)
+ − 406
apply(simp add: atom_eqvt_raw)
+ − 407
apply(simp add: atom_image_cong)
+ − 408
done
+ − 409
1460
+ − 410
lemma swap_atom_image_fresh: "\<lbrakk>a \<sharp> atom ` (fn :: ('a :: at_base set)); b \<sharp> atom ` fn\<rbrakk> \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> fn = fn"
+ − 411
apply (simp add: fresh_def)
+ − 412
apply (simp add: supp_atom_image)
+ − 413
apply (fold fresh_def)
+ − 414
apply (simp add: swap_fresh_fresh)
1440
+ − 415
done
+ − 416
1467
+ − 417
(* TODO: The following lemmas can be moved somewhere... *)
1657
+ − 418
+ − 419
lemma Abs_eq_iff:
+ − 420
shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"
1675
+ − 421
and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))"
+ − 422
and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))"
+ − 423
by (lifting alphas_abs)
1657
+ − 424
1467
+ − 425
lemma split_rsp2[quot_respect]: "((R1 ===> R2 ===> prod_rel R1 R2 ===> op =) ===>
+ − 426
prod_rel R1 R2 ===> prod_rel R1 R2 ===> op =) split split"
+ − 427
by auto
+ − 428
+ − 429
lemma split_prs2[quot_preserve]:
+ − 430
assumes q1: "Quotient R1 Abs1 Rep1"
+ − 431
and q2: "Quotient R2 Abs2 Rep2"
+ − 432
shows "((Abs1 ---> Abs2 ---> prod_fun Abs1 Abs2 ---> id) ---> prod_fun Rep1 Rep2 ---> prod_fun Rep1 Rep2 ---> id) split = split"
+ − 433
by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
+ − 434
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
+ − 435
lemma alphas2:
1467
+ − 436
"(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
+ − 437
(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
+ − 438
\<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
+ − 439
"(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
+ − 440
(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
+ − 441
"(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
+ − 442
(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
+ − 443
\<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
+ − 444
by (simp_all add: alphas)
1544
+ − 445
1744
+ − 446
lemma alphas3:
+ − 447
"(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>
+ − 448
(f1 x1 \<union> (f2 x2 \<union> f3 x3) - set bsl) \<sharp>* pi \<and>
+ − 449
R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2 \<and> R3 (pi \<bullet> x3) y3 \<and> pi \<bullet> bsl = csl)"
+ − 450
by (simp add: alphas)
+ − 451
1558
+ − 452
lemma alpha_gen_compose_sym:
+ − 453
fixes pi
+ − 454
assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)"
+ − 455
and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
+ − 456
shows "(ab, s) \<approx>gen R f (- pi) (aa, t)"
+ − 457
using b apply -
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
+ − 458
apply(simp add: alphas)
1558
+ − 459
apply(erule conjE)+
+ − 460
apply(rule conjI)
+ − 461
apply(simp add: fresh_star_def fresh_minus_perm)
+ − 462
apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))")
+ − 463
apply simp
+ − 464
apply(clarify)
+ − 465
apply(simp)
+ − 466
apply(rule a)
+ − 467
apply assumption
+ − 468
done
+ − 469
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
+ − 470
lemma alpha_res_compose_sym:
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
+ − 471
fixes pi
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
+ − 472
assumes b: "(aa, t) \<approx>res (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)"
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
+ − 473
and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
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
+ − 474
shows "(ab, s) \<approx>res R f (- pi) (aa, t)"
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
+ − 475
using b apply -
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
+ − 476
apply(simp add: alphas)
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
+ − 477
apply(erule conjE)+
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
+ − 478
apply(rule conjI)
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
+ − 479
apply(simp add: fresh_star_def fresh_minus_perm)
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
+ − 480
apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))")
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
+ − 481
apply simp
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
+ − 482
apply(rule a)
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
+ − 483
apply assumption
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
+ − 484
done
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
+ − 485
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
+ − 486
lemma alpha_lst_compose_sym:
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
+ − 487
fixes pi
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
+ − 488
assumes b: "(aa, t) \<approx>lst (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)"
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
+ − 489
and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
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
+ − 490
shows "(ab, s) \<approx>lst R f (- pi) (aa, t)"
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
+ − 491
using b apply -
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
+ − 492
apply(simp add: alphas)
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
+ − 493
apply(erule conjE)+
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
+ − 494
apply(rule conjI)
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
+ − 495
apply(simp add: fresh_star_def fresh_minus_perm)
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
+ − 496
apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))")
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
+ − 497
apply simp
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
+ − 498
apply(clarify)
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
+ − 499
apply(simp)
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
+ − 500
apply(rule a)
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
+ − 501
apply assumption
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
+ − 502
done
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
+ − 503
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
+ − 504
lemmas alphas_compose_sym = alpha_gen_compose_sym alpha_res_compose_sym alpha_lst_compose_sym
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
+ − 505
1558
+ − 506
lemma alpha_gen_compose_sym2:
+ − 507
assumes a: "(aa, t1, t2) \<approx>gen (\<lambda>(x11, x12) (x21, x22).
+ − 508
(R1 x11 x21 \<and> R1 x21 x11) \<and> R2 x12 x22 \<and> R2 x22 x12) (\<lambda>(b, a). fb b \<union> fa a) pi (ab, s1, s2)"
+ − 509
and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)"
+ − 510
and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)"
+ − 511
shows "(ab, s1, s2) \<approx>gen (\<lambda>(a, b) (d, c). R1 a d \<and> R2 b c) (\<lambda>(b, a). fb b \<union> fa a) (- pi) (aa, t1, t2)"
+ − 512
using a
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
+ − 513
apply(simp add: alphas)
1558
+ − 514
apply clarify
+ − 515
apply (rule conjI)
+ − 516
apply(simp add: fresh_star_def fresh_minus_perm)
+ − 517
apply (rule conjI)
+ − 518
apply (rotate_tac 3)
+ − 519
apply (drule_tac pi="- pi" in r1)
+ − 520
apply simp
+ − 521
apply (rule conjI)
+ − 522
apply (rotate_tac -1)
+ − 523
apply (drule_tac pi="- pi" in r2)
+ − 524
apply simp_all
+ − 525
done
+ − 526
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
+ − 527
lemma alpha_res_compose_sym2:
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
+ − 528
assumes a: "(aa, t1, t2) \<approx>res (\<lambda>(x11, x12) (x21, x22).
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
+ − 529
(R1 x11 x21 \<and> R1 x21 x11) \<and> R2 x12 x22 \<and> R2 x22 x12) (\<lambda>(b, a). fb b \<union> fa a) pi (ab, s1, s2)"
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
+ − 530
and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)"
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
+ − 531
and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)"
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
+ − 532
shows "(ab, s1, s2) \<approx>res (\<lambda>(a, b) (d, c). R1 a d \<and> R2 b c) (\<lambda>(b, a). fb b \<union> fa a) (- pi) (aa, t1, t2)"
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
+ − 533
using a
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
+ − 534
apply(simp add: alphas)
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
+ − 535
apply clarify
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
+ − 536
apply (rule conjI)
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
+ − 537
apply(simp add: fresh_star_def fresh_minus_perm)
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
+ − 538
apply (rule conjI)
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
+ − 539
apply (rotate_tac 3)
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
+ − 540
apply (drule_tac pi="- pi" in r1)
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
+ − 541
apply simp
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
+ − 542
apply (rotate_tac -1)
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
+ − 543
apply (drule_tac pi="- pi" in r2)
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
+ − 544
apply simp
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
+ − 545
done
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
+ − 546
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
+ − 547
lemma alpha_lst_compose_sym2:
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
+ − 548
assumes a: "(aa, t1, t2) \<approx>lst (\<lambda>(x11, x12) (x21, x22).
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
+ − 549
(R1 x11 x21 \<and> R1 x21 x11) \<and> R2 x12 x22 \<and> R2 x22 x12) (\<lambda>(b, a). fb b \<union> fa a) pi (ab, s1, s2)"
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
+ − 550
and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)"
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
+ − 551
and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)"
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
+ − 552
shows "(ab, s1, s2) \<approx>lst (\<lambda>(a, b) (d, c). R1 a d \<and> R2 b c) (\<lambda>(b, a). fb b \<union> fa a) (- pi) (aa, t1, t2)"
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
+ − 553
using a
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
+ − 554
apply(simp add: alphas)
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
+ − 555
apply clarify
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
+ − 556
apply (rule conjI)
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
+ − 557
apply(simp add: fresh_star_def fresh_minus_perm)
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
+ − 558
apply (rule conjI)
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
+ − 559
apply (rotate_tac 3)
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
+ − 560
apply (drule_tac pi="- pi" in r1)
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
+ − 561
apply simp
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
+ − 562
apply (rule conjI)
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
+ − 563
apply (rotate_tac -1)
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
+ − 564
apply (drule_tac pi="- pi" in r2)
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
apply simp_all
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
+ − 566
done
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
+ − 567
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
+ − 568
lemmas alphas_compose_sym2 = alpha_gen_compose_sym2 alpha_res_compose_sym2 alpha_lst_compose_sym2
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
1558
+ − 570
lemma alpha_gen_compose_trans:
+ − 571
fixes pi pia
+ − 572
assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)"
+ − 573
and c: "(ab, ta) \<approx>gen R f pia (ac, sa)"
+ − 574
and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
+ − 575
shows "(aa, t) \<approx>gen R f (pia + pi) (ac, sa)"
+ − 576
using b c apply -
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
+ − 577
apply(simp add: alphas)
1558
+ − 578
apply(erule conjE)+
+ − 579
apply(simp add: fresh_star_plus)
+ − 580
apply(drule_tac x="- pia \<bullet> sa" in spec)
+ − 581
apply(drule mp)
+ − 582
apply(rotate_tac 5)
+ − 583
apply(drule_tac pi="- pia" in a)
+ − 584
apply(simp)
+ − 585
apply(rotate_tac 7)
+ − 586
apply(drule_tac pi="pia" in a)
+ − 587
apply(simp)
+ − 588
done
+ − 589
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
+ − 590
lemma alpha_res_compose_trans:
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
+ − 591
fixes pi pia
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
+ − 592
assumes b: "(aa, t) \<approx>res (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)"
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
+ − 593
and c: "(ab, ta) \<approx>res R f pia (ac, sa)"
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
+ − 594
and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
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
+ − 595
shows "(aa, t) \<approx>res R f (pia + pi) (ac, sa)"
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
+ − 596
using b c apply -
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
+ − 597
apply(simp add: alphas)
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
+ − 598
apply(erule conjE)+
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
+ − 599
apply(simp add: fresh_star_plus)
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
+ − 600
apply(drule_tac x="- pia \<bullet> sa" in spec)
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
+ − 601
apply(drule mp)
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
+ − 602
apply(drule_tac pi="- pia" in a)
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
+ − 603
apply(simp)
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
+ − 604
apply(rotate_tac 6)
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
+ − 605
apply(drule_tac pi="pia" in a)
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
+ − 606
apply(simp)
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
+ − 607
done
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
+ − 608
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
+ − 609
lemma alpha_lst_compose_trans:
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
+ − 610
fixes pi pia
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
+ − 611
assumes b: "(aa, t) \<approx>lst (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)"
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
+ − 612
and c: "(ab, ta) \<approx>lst R f pia (ac, sa)"
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
+ − 613
and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
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
+ − 614
shows "(aa, t) \<approx>lst R f (pia + pi) (ac, sa)"
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
+ − 615
using b c apply -
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
+ − 616
apply(simp add: alphas)
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
+ − 617
apply(erule conjE)+
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
+ − 618
apply(simp add: fresh_star_plus)
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
+ − 619
apply(drule_tac x="- pia \<bullet> sa" in spec)
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
+ − 620
apply(drule mp)
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
+ − 621
apply(rotate_tac 5)
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
+ − 622
apply(drule_tac pi="- pia" in a)
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
+ − 623
apply(simp)
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
+ − 624
apply(rotate_tac 7)
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
+ − 625
apply(drule_tac pi="pia" in a)
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
+ − 626
apply(simp)
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
+ − 627
done
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
+ − 628
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
+ − 629
lemmas alphas_compose_trans = alpha_gen_compose_trans alpha_res_compose_trans alpha_lst_compose_trans
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
+ − 630
1581
6b1eea8dcdc0
equivp_cheat can be removed for all one-permutation examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 631
lemma alpha_gen_compose_trans2:
6b1eea8dcdc0
equivp_cheat can be removed for all one-permutation examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 632
fixes pi pia
6b1eea8dcdc0
equivp_cheat can be removed for all one-permutation examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 633
assumes b: "(aa, (t1, t2)) \<approx>gen
6b1eea8dcdc0
equivp_cheat can be removed for all one-permutation examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 634
(\<lambda>(b, a) (d, c). R1 b d \<and> (\<forall>z. R1 d z \<longrightarrow> R1 b z) \<and> R2 a c \<and> (\<forall>z. R2 c z \<longrightarrow> R2 a z))
6b1eea8dcdc0
equivp_cheat can be removed for all one-permutation examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 635
(\<lambda>(b, a). fv_a b \<union> fv_b a) pi (ab, (ta1, ta2))"
6b1eea8dcdc0
equivp_cheat can be removed for all one-permutation examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 636
and c: "(ab, (ta1, ta2)) \<approx>gen (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a)
6b1eea8dcdc0
equivp_cheat can be removed for all one-permutation examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 637
pia (ac, (sa1, sa2))"
6b1eea8dcdc0
equivp_cheat can be removed for all one-permutation examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 638
and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)"
6b1eea8dcdc0
equivp_cheat can be removed for all one-permutation examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 639
and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)"
6b1eea8dcdc0
equivp_cheat can be removed for all one-permutation examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 640
shows "(aa, (t1, t2)) \<approx>gen (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a)
6b1eea8dcdc0
equivp_cheat can be removed for all one-permutation examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 641
(pia + pi) (ac, (sa1, sa2))"
6b1eea8dcdc0
equivp_cheat can be removed for all one-permutation examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 642
using b c apply -
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
+ − 643
apply(simp add: alphas2)
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
+ − 644
apply(simp add: alphas)
1581
6b1eea8dcdc0
equivp_cheat can be removed for all one-permutation examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 645
apply(erule conjE)+
6b1eea8dcdc0
equivp_cheat can be removed for all one-permutation examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 646
apply(simp add: fresh_star_plus)
6b1eea8dcdc0
equivp_cheat can be removed for all one-permutation examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 647
apply(drule_tac x="- pia \<bullet> sa1" in spec)
6b1eea8dcdc0
equivp_cheat can be removed for all one-permutation examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 648
apply(drule mp)
6b1eea8dcdc0
equivp_cheat can be removed for all one-permutation examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 649
apply(rotate_tac 5)
6b1eea8dcdc0
equivp_cheat can be removed for all one-permutation examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 650
apply(drule_tac pi="- pia" in r1)
6b1eea8dcdc0
equivp_cheat can be removed for all one-permutation examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 651
apply(simp)
6b1eea8dcdc0
equivp_cheat can be removed for all one-permutation examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 652
apply(rotate_tac -1)
6b1eea8dcdc0
equivp_cheat can be removed for all one-permutation examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 653
apply(drule_tac pi="pia" in r1)
6b1eea8dcdc0
equivp_cheat can be removed for all one-permutation examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 654
apply(simp)
6b1eea8dcdc0
equivp_cheat can be removed for all one-permutation examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 655
apply(drule_tac x="- pia \<bullet> sa2" in spec)
6b1eea8dcdc0
equivp_cheat can be removed for all one-permutation examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 656
apply(drule mp)
6b1eea8dcdc0
equivp_cheat can be removed for all one-permutation examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 657
apply(rotate_tac 6)
6b1eea8dcdc0
equivp_cheat can be removed for all one-permutation examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 658
apply(drule_tac pi="- pia" in r2)
6b1eea8dcdc0
equivp_cheat can be removed for all one-permutation examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 659
apply(simp)
6b1eea8dcdc0
equivp_cheat can be removed for all one-permutation examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 660
apply(rotate_tac -1)
6b1eea8dcdc0
equivp_cheat can be removed for all one-permutation examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 661
apply(drule_tac pi="pia" in r2)
6b1eea8dcdc0
equivp_cheat can be removed for all one-permutation examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 662
apply(simp)
6b1eea8dcdc0
equivp_cheat can be removed for all one-permutation examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 663
done
6b1eea8dcdc0
equivp_cheat can be removed for all one-permutation examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 664
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
+ − 665
lemma alpha_res_compose_trans2:
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
+ − 666
fixes pi pia
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
+ − 667
assumes b: "(aa, (t1, t2)) \<approx>res
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
+ − 668
(\<lambda>(b, a) (d, c). R1 b d \<and> (\<forall>z. R1 d z \<longrightarrow> R1 b z) \<and> R2 a c \<and> (\<forall>z. R2 c z \<longrightarrow> R2 a z))
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
+ − 669
(\<lambda>(b, a). fv_a b \<union> fv_b a) pi (ab, (ta1, ta2))"
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
+ − 670
and c: "(ab, (ta1, ta2)) \<approx>res (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a)
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
+ − 671
pia (ac, (sa1, sa2))"
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
+ − 672
and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)"
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
+ − 673
and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)"
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
+ − 674
shows "(aa, (t1, t2)) \<approx>res (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a)
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
+ − 675
(pia + pi) (ac, (sa1, sa2))"
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
+ − 676
using b c apply -
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
+ − 677
apply(simp add: alphas2)
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
+ − 678
apply(simp add: alphas)
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
+ − 679
apply(erule conjE)+
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
+ − 680
apply(simp add: fresh_star_plus)
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
+ − 681
apply(drule_tac x="- pia \<bullet> sa1" in spec)
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
+ − 682
apply(drule mp)
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
+ − 683
apply(rotate_tac 5)
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
+ − 684
apply(drule_tac pi="- pia" in r1)
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
+ − 685
apply(simp)
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
+ − 686
apply(rotate_tac -1)
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
+ − 687
apply(drule_tac pi="pia" in r1)
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
+ − 688
apply(simp)
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
+ − 689
apply(drule_tac x="- pia \<bullet> sa2" in spec)
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
+ − 690
apply(drule mp)
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
+ − 691
apply(rotate_tac 6)
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
+ − 692
apply(drule_tac pi="- pia" in r2)
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
+ − 693
apply(simp)
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
+ − 694
apply(rotate_tac -1)
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
+ − 695
apply(drule_tac pi="pia" in r2)
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
+ − 696
apply(simp)
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
+ − 697
done
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
+ − 698
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
+ − 699
lemma alpha_lst_compose_trans2:
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
+ − 700
fixes pi pia
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
+ − 701
assumes b: "(aa, (t1, t2)) \<approx>lst
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
+ − 702
(\<lambda>(b, a) (d, c). R1 b d \<and> (\<forall>z. R1 d z \<longrightarrow> R1 b z) \<and> R2 a c \<and> (\<forall>z. R2 c z \<longrightarrow> R2 a z))
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
+ − 703
(\<lambda>(b, a). fv_a b \<union> fv_b a) pi (ab, (ta1, ta2))"
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
+ − 704
and c: "(ab, (ta1, ta2)) \<approx>lst (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a)
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
+ − 705
pia (ac, (sa1, sa2))"
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
+ − 706
and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)"
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
+ − 707
and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)"
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
+ − 708
shows "(aa, (t1, t2)) \<approx>lst (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a)
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
+ − 709
(pia + pi) (ac, (sa1, sa2))"
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
+ − 710
using b c apply -
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
+ − 711
apply(simp add: alphas2)
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
+ − 712
apply(simp add: alphas)
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
+ − 713
apply(erule conjE)+
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
+ − 714
apply(simp add: fresh_star_plus)
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
+ − 715
apply(drule_tac x="- pia \<bullet> sa1" in spec)
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
+ − 716
apply(drule mp)
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
+ − 717
apply(rotate_tac 5)
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
+ − 718
apply(drule_tac pi="- pia" in r1)
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
+ − 719
apply(simp)
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
+ − 720
apply(rotate_tac -1)
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
+ − 721
apply(drule_tac pi="pia" in r1)
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
+ − 722
apply(simp)
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
+ − 723
apply(drule_tac x="- pia \<bullet> sa2" in spec)
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
+ − 724
apply(drule mp)
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
+ − 725
apply(rotate_tac 6)
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
+ − 726
apply(drule_tac pi="- pia" in r2)
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
+ − 727
apply(simp)
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
+ − 728
apply(rotate_tac -1)
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
+ − 729
apply(drule_tac pi="pia" in r2)
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
+ − 730
apply(simp)
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
+ − 731
done
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
+ − 732
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
+ − 733
lemmas alphas_compose_trans2 = alpha_gen_compose_trans2 alpha_res_compose_trans2 alpha_lst_compose_trans2
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
+ − 734
1657
+ − 735
lemma alpha_gen_refl:
+ − 736
assumes a: "R x x"
+ − 737
shows "(bs, x) \<approx>gen R f 0 (bs, x)"
+ − 738
and "(bs, x) \<approx>res R f 0 (bs, x)"
+ − 739
and "(cs, x) \<approx>lst R f 0 (cs, x)"
+ − 740
using a
+ − 741
unfolding alphas
+ − 742
unfolding fresh_star_def
+ − 743
by (simp_all add: fresh_zero_perm)
+ − 744
+ − 745
lemma alpha_gen_sym:
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
+ − 746
assumes a: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x"
1657
+ − 747
shows "(bs, x) \<approx>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)"
+ − 748
and "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)"
+ − 749
and "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)"
1664
aa999d263b10
Modified abs_gen_sym and abs_gen_trans so it becomes usable in the proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 750
unfolding alphas fresh_star_def
1657
+ − 751
using a
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
+ − 752
by (auto simp add: fresh_minus_perm)
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
+ − 753
1657
+ − 754
lemma alpha_gen_trans:
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
+ − 755
assumes a: "\<lbrakk>R (p \<bullet> x) y; R (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((q + p) \<bullet> x) z"
1657
+ − 756
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)"
+ − 757
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)"
+ − 758
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)"
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
+ − 759
using a
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
+ − 760
unfolding alphas fresh_star_def
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
+ − 761
by (simp_all add: fresh_plus_perm)
1657
+ − 762
1804
+ − 763
1845
b7423c6b5564
deleted offending [eqvt]-attribute in Abs; Lambda works again, but there is now a problem in CoreHaskell
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 764
lemma alpha_gen_eqvt(*[eqvt]*):
1804
+ − 765
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)"
+ − 766
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)"
+ − 767
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)"
+ − 768
unfolding alphas
+ − 769
unfolding permute_eqvt[symmetric]
+ − 770
unfolding set_eqvt[symmetric]
+ − 771
unfolding permute_fun_app_eq[symmetric]
+ − 772
unfolding Diff_eqvt[symmetric]
+ − 773
by (auto simp add: permute_bool_def fresh_star_permute_iff)
+ − 774
1691
+ − 775
lemma alpha_gen_simpler:
+ − 776
assumes fv_rsp: "\<And>x y. R y x \<Longrightarrow> f x = f y"
+ − 777
and fin_fv: "finite (f x)"
+ − 778
and fv_eqvt: "pi \<bullet> f x = f (pi \<bullet> x)"
+ − 779
shows "alpha_gen (bs, x) R f pi (cs, y) \<longleftrightarrow>
+ − 780
(f x - bs) \<sharp>* pi \<and>
+ − 781
R (pi \<bullet> x) y \<and>
+ − 782
pi \<bullet> bs = cs"
+ − 783
apply rule
+ − 784
unfolding alpha_gen
+ − 785
apply clarify
+ − 786
apply (erule conjE)+
+ − 787
apply (simp)
+ − 788
apply (subgoal_tac "f y - cs = pi \<bullet> (f x - bs)")
+ − 789
apply (rule sym)
+ − 790
apply simp
+ − 791
apply (rule supp_perm_eq)
+ − 792
apply (subst supp_finite_atom_set)
+ − 793
apply (rule finite_Diff)
+ − 794
apply (rule fin_fv)
+ − 795
apply (assumption)
+ − 796
apply (simp add: eqvts fv_eqvt)
+ − 797
apply (subst fv_rsp)
+ − 798
apply assumption
+ − 799
apply (simp)
+ − 800
done
+ − 801
+ − 802
lemma alpha_lst_simpler:
+ − 803
assumes fv_rsp: "\<And>x y. R y x \<Longrightarrow> f x = f y"
+ − 804
and fin_fv: "finite (f x)"
+ − 805
and fv_eqvt: "pi \<bullet> f x = f (pi \<bullet> x)"
+ − 806
shows "alpha_lst (bs, x) R f pi (cs, y) \<longleftrightarrow>
+ − 807
(f x - set bs) \<sharp>* pi \<and>
+ − 808
R (pi \<bullet> x) y \<and>
+ − 809
pi \<bullet> bs = cs"
+ − 810
apply rule
+ − 811
unfolding alpha_lst
+ − 812
apply clarify
+ − 813
apply (erule conjE)+
+ − 814
apply (simp)
+ − 815
apply (subgoal_tac "f y - set cs = pi \<bullet> (f x - set bs)")
+ − 816
apply (rule sym)
+ − 817
apply simp
+ − 818
apply (rule supp_perm_eq)
+ − 819
apply (subst supp_finite_atom_set)
+ − 820
apply (rule finite_Diff)
+ − 821
apply (rule fin_fv)
+ − 822
apply (assumption)
+ − 823
apply (simp add: eqvts fv_eqvt)
+ − 824
apply (subst fv_rsp)
+ − 825
apply assumption
+ − 826
apply (simp)
+ − 827
done
+ − 828
+ − 829
1440
+ − 830
end
+ − 831