1062
+ − 1
(* Title: Nominal2_Supp
+ − 2
Authors: Brian Huffman, Christian Urban
+ − 3
+ − 4
Supplementary Lemmas and Definitions for
+ − 5
Nominal Isabelle.
+ − 6
*)
+ − 7
theory Nominal2_Supp
+ − 8
imports Nominal2_Base Nominal2_Eqvt Nominal2_Atoms
+ − 9
begin
+ − 10
+ − 11
+ − 12
section {* Fresh-Star *}
+ − 13
1930
+ − 14
1062
+ − 15
text {* The fresh-star generalisation of fresh is used in strong
+ − 16
induction principles. *}
+ − 17
+ − 18
definition
+ − 19
fresh_star :: "atom set \<Rightarrow> 'a::pt \<Rightarrow> bool" ("_ \<sharp>* _" [80,80] 80)
+ − 20
where
1506
+ − 21
"as \<sharp>* x \<equiv> \<forall>a \<in> as. a \<sharp> x"
1062
+ − 22
+ − 23
lemma fresh_star_prod:
1506
+ − 24
fixes as::"atom set"
2012
+ − 25
shows "as \<sharp>* (x, y) = (as \<sharp>* x \<and> as \<sharp>* y)"
1062
+ − 26
by (auto simp add: fresh_star_def fresh_Pair)
+ − 27
+ − 28
lemma fresh_star_union:
1506
+ − 29
shows "(as \<union> bs) \<sharp>* x = (as \<sharp>* x \<and> bs \<sharp>* x)"
1062
+ − 30
by (auto simp add: fresh_star_def)
+ − 31
+ − 32
lemma fresh_star_insert:
1506
+ − 33
shows "(insert a as) \<sharp>* x = (a \<sharp> x \<and> as \<sharp>* x)"
1062
+ − 34
by (auto simp add: fresh_star_def)
+ − 35
+ − 36
lemma fresh_star_Un_elim:
1506
+ − 37
"((as \<union> bs) \<sharp>* x \<Longrightarrow> PROP C) \<equiv> (as \<sharp>* x \<Longrightarrow> bs \<sharp>* x \<Longrightarrow> PROP C)"
1062
+ − 38
unfolding fresh_star_def
+ − 39
apply(rule)
+ − 40
apply(erule meta_mp)
+ − 41
apply(auto)
+ − 42
done
+ − 43
+ − 44
lemma fresh_star_insert_elim:
1506
+ − 45
"(insert a as \<sharp>* x \<Longrightarrow> PROP C) \<equiv> (a \<sharp> x \<Longrightarrow> as \<sharp>* x \<Longrightarrow> PROP C)"
1062
+ − 46
unfolding fresh_star_def
+ − 47
by rule (simp_all add: fresh_star_def)
+ − 48
+ − 49
lemma fresh_star_empty_elim:
1506
+ − 50
"({} \<sharp>* x \<Longrightarrow> PROP C) \<equiv> PROP C"
1062
+ − 51
by (simp add: fresh_star_def)
+ − 52
+ − 53
lemma fresh_star_unit_elim:
+ − 54
shows "(a \<sharp>* () \<Longrightarrow> PROP C) \<equiv> PROP C"
+ − 55
by (simp add: fresh_star_def fresh_unit)
+ − 56
+ − 57
lemma fresh_star_prod_elim:
+ − 58
shows "(a \<sharp>* (x, y) \<Longrightarrow> PROP C) \<equiv> (a \<sharp>* x \<Longrightarrow> a \<sharp>* y \<Longrightarrow> PROP C)"
+ − 59
by (rule, simp_all add: fresh_star_prod)
+ − 60
1436
+ − 61
lemma fresh_star_plus:
+ − 62
fixes p q::perm
+ − 63
shows "\<lbrakk>a \<sharp>* p; a \<sharp>* q\<rbrakk> \<Longrightarrow> a \<sharp>* (p + q)"
+ − 64
unfolding fresh_star_def
+ − 65
by (simp add: fresh_plus_perm)
+ − 66
+ − 67
lemma fresh_star_permute_iff:
+ − 68
shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x"
+ − 69
unfolding fresh_star_def
2012
+ − 70
by (metis mem_permute_iff permute_minus_cancel(1) fresh_permute_iff)
1436
+ − 71
1861
+ − 72
lemma fresh_star_eqvt[eqvt]:
1436
+ − 73
shows "(p \<bullet> (as \<sharp>* x)) = (p \<bullet> as) \<sharp>* (p \<bullet> x)"
+ − 74
unfolding fresh_star_def
+ − 75
unfolding Ball_def
+ − 76
apply(simp add: all_eqvt)
+ − 77
apply(subst permute_fun_def)
+ − 78
apply(simp add: imp_eqvt fresh_eqvt mem_eqvt)
+ − 79
done
1062
+ − 80
+ − 81
section {* Avoiding of atom sets *}
+ − 82
+ − 83
text {*
+ − 84
For every set of atoms, there is another set of atoms
+ − 85
avoiding a finitely supported c and there is a permutation
+ − 86
which 'translates' between both sets.
+ − 87
*}
+ − 88
+ − 89
lemma at_set_avoiding_aux:
+ − 90
fixes Xs::"atom set"
+ − 91
and As::"atom set"
+ − 92
assumes b: "Xs \<subseteq> As"
+ − 93
and c: "finite As"
+ − 94
shows "\<exists>p. (p \<bullet> Xs) \<inter> As = {} \<and> (supp p) \<subseteq> (Xs \<union> (p \<bullet> Xs))"
+ − 95
proof -
+ − 96
from b c have "finite Xs" by (rule finite_subset)
+ − 97
then show ?thesis using b
+ − 98
proof (induct rule: finite_subset_induct)
+ − 99
case empty
+ − 100
have "0 \<bullet> {} \<inter> As = {}" by simp
+ − 101
moreover
+ − 102
have "supp (0::perm) \<subseteq> {} \<union> 0 \<bullet> {}" by (simp add: supp_zero_perm)
+ − 103
ultimately show ?case by blast
+ − 104
next
+ − 105
case (insert x Xs)
+ − 106
then obtain p where
+ − 107
p1: "(p \<bullet> Xs) \<inter> As = {}" and
+ − 108
p2: "supp p \<subseteq> (Xs \<union> (p \<bullet> Xs))" by blast
+ − 109
from `x \<in> As` p1 have "x \<notin> p \<bullet> Xs" by fast
+ − 110
with `x \<notin> Xs` p2 have "x \<notin> supp p" by fast
+ − 111
hence px: "p \<bullet> x = x" unfolding supp_perm by simp
+ − 112
have "finite (As \<union> p \<bullet> Xs)"
+ − 113
using `finite As` `finite Xs`
+ − 114
by (simp add: permute_set_eq_image)
+ − 115
then obtain y where "y \<notin> (As \<union> p \<bullet> Xs)" "sort_of y = sort_of x"
+ − 116
by (rule obtain_atom)
+ − 117
hence y: "y \<notin> As" "y \<notin> p \<bullet> Xs" "sort_of y = sort_of x"
+ − 118
by simp_all
+ − 119
let ?q = "(x \<rightleftharpoons> y) + p"
+ − 120
have q: "?q \<bullet> insert x Xs = insert y (p \<bullet> Xs)"
+ − 121
unfolding insert_eqvt
+ − 122
using `p \<bullet> x = x` `sort_of y = sort_of x`
+ − 123
using `x \<notin> p \<bullet> Xs` `y \<notin> p \<bullet> Xs`
+ − 124
by (simp add: swap_atom swap_set_not_in)
+ − 125
have "?q \<bullet> insert x Xs \<inter> As = {}"
+ − 126
using `y \<notin> As` `p \<bullet> Xs \<inter> As = {}`
+ − 127
unfolding q by simp
+ − 128
moreover
+ − 129
have "supp ?q \<subseteq> insert x Xs \<union> ?q \<bullet> insert x Xs"
+ − 130
using p2 unfolding q
1930
+ − 131
by (intro subset_trans [OF supp_plus_perm])
+ − 132
(auto simp add: supp_swap)
1062
+ − 133
ultimately show ?case by blast
+ − 134
qed
+ − 135
qed
+ − 136
+ − 137
lemma at_set_avoiding:
+ − 138
assumes a: "finite Xs"
+ − 139
and b: "finite (supp c)"
+ − 140
obtains p::"perm" where "(p \<bullet> Xs)\<sharp>*c" and "(supp p) \<subseteq> (Xs \<union> (p \<bullet> Xs))"
+ − 141
using a b at_set_avoiding_aux [where Xs="Xs" and As="Xs \<union> supp c"]
+ − 142
unfolding fresh_star_def fresh_def by blast
+ − 143
1879
+ − 144
lemma at_set_avoiding2:
+ − 145
assumes "finite xs"
+ − 146
and "finite (supp c)" "finite (supp x)"
+ − 147
and "xs \<sharp>* x"
+ − 148
shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp x \<sharp>* p"
+ − 149
using assms
+ − 150
apply(erule_tac c="(c, x)" in at_set_avoiding)
+ − 151
apply(simp add: supp_Pair)
+ − 152
apply(rule_tac x="p" in exI)
+ − 153
apply(simp add: fresh_star_prod)
+ − 154
apply(subgoal_tac "\<forall>a \<in> supp p. a \<sharp> x")
+ − 155
apply(auto simp add: fresh_star_def fresh_def supp_perm)[1]
+ − 156
apply(auto simp add: fresh_star_def fresh_def)
+ − 157
done
+ − 158
+ − 159
lemma at_set_avoiding2_atom:
+ − 160
assumes "finite (supp c)" "finite (supp x)"
1930
+ − 161
and b: "a \<sharp> x"
+ − 162
shows "\<exists>p. (p \<bullet> a) \<sharp> c \<and> supp x \<sharp>* p"
1879
+ − 163
proof -
1930
+ − 164
have a: "{a} \<sharp>* x" unfolding fresh_star_def by (simp add: b)
+ − 165
obtain p where p1: "(p \<bullet> {a}) \<sharp>* c" and p2: "supp x \<sharp>* p"
+ − 166
using at_set_avoiding2[of "{a}" "c" "x"] assms a by blast
+ − 167
have c: "(p \<bullet> a) \<sharp> c" using p1
1879
+ − 168
unfolding fresh_star_def Ball_def
2012
+ − 169
by(erule_tac x="p \<bullet> a" in allE) (simp add: permute_set_eq)
1930
+ − 170
hence "p \<bullet> a \<sharp> c \<and> supp x \<sharp>* p" using p2 by blast
+ − 171
then show "\<exists>p. (p \<bullet> a) \<sharp> c \<and> supp x \<sharp>* p" by blast
1879
+ − 172
qed
1062
+ − 173
1930
+ − 174
+ − 175
section {* The freshness lemma according to Andy Pitts *}
1062
+ − 176
+ − 177
lemma freshness_lemma:
+ − 178
fixes h :: "'a::at \<Rightarrow> 'b::pt"
+ − 179
assumes a: "\<exists>a. atom a \<sharp> (h, h a)"
+ − 180
shows "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"
+ − 181
proof -
+ − 182
from a obtain b where a1: "atom b \<sharp> h" and a2: "atom b \<sharp> h b"
+ − 183
by (auto simp add: fresh_Pair)
+ − 184
show "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"
+ − 185
proof (intro exI allI impI)
+ − 186
fix a :: 'a
+ − 187
assume a3: "atom a \<sharp> h"
+ − 188
show "h a = h b"
+ − 189
proof (cases "a = b")
+ − 190
assume "a = b"
+ − 191
thus "h a = h b" by simp
+ − 192
next
+ − 193
assume "a \<noteq> b"
1080
+ − 194
hence "atom a \<sharp> b" by (simp add: fresh_at_base)
1879
+ − 195
with a3 have "atom a \<sharp> h b"
+ − 196
by (rule fresh_fun_app)
1062
+ − 197
with a2 have d1: "(atom b \<rightleftharpoons> atom a) \<bullet> (h b) = (h b)"
+ − 198
by (rule swap_fresh_fresh)
+ − 199
from a1 a3 have d2: "(atom b \<rightleftharpoons> atom a) \<bullet> h = h"
+ − 200
by (rule swap_fresh_fresh)
+ − 201
from d1 have "h b = (atom b \<rightleftharpoons> atom a) \<bullet> (h b)" by simp
+ − 202
also have "\<dots> = ((atom b \<rightleftharpoons> atom a) \<bullet> h) ((atom b \<rightleftharpoons> atom a) \<bullet> b)"
+ − 203
by (rule permute_fun_app_eq)
+ − 204
also have "\<dots> = h a"
+ − 205
using d2 by simp
+ − 206
finally show "h a = h b" by simp
+ − 207
qed
+ − 208
qed
+ − 209
qed
+ − 210
+ − 211
lemma freshness_lemma_unique:
+ − 212
fixes h :: "'a::at \<Rightarrow> 'b::pt"
+ − 213
assumes a: "\<exists>a. atom a \<sharp> (h, h a)"
+ − 214
shows "\<exists>!x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"
+ − 215
proof (rule ex_ex1I)
+ − 216
from a show "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"
+ − 217
by (rule freshness_lemma)
+ − 218
next
+ − 219
fix x y
+ − 220
assume x: "\<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"
+ − 221
assume y: "\<forall>a. atom a \<sharp> h \<longrightarrow> h a = y"
+ − 222
from a x y show "x = y"
+ − 223
by (auto simp add: fresh_Pair)
+ − 224
qed
+ − 225
+ − 226
text {* packaging the freshness lemma into a function *}
+ − 227
+ − 228
definition
+ − 229
fresh_fun :: "('a::at \<Rightarrow> 'b::pt) \<Rightarrow> 'b"
+ − 230
where
+ − 231
"fresh_fun h = (THE x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x)"
+ − 232
+ − 233
lemma fresh_fun_app:
+ − 234
fixes h :: "'a::at \<Rightarrow> 'b::pt"
+ − 235
assumes a: "\<exists>a. atom a \<sharp> (h, h a)"
+ − 236
assumes b: "atom a \<sharp> h"
+ − 237
shows "fresh_fun h = h a"
+ − 238
unfolding fresh_fun_def
+ − 239
proof (rule the_equality)
+ − 240
show "\<forall>a'. atom a' \<sharp> h \<longrightarrow> h a' = h a"
+ − 241
proof (intro strip)
+ − 242
fix a':: 'a
+ − 243
assume c: "atom a' \<sharp> h"
+ − 244
from a have "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x" by (rule freshness_lemma)
+ − 245
with b c show "h a' = h a" by auto
+ − 246
qed
+ − 247
next
+ − 248
fix fr :: 'b
+ − 249
assume "\<forall>a. atom a \<sharp> h \<longrightarrow> h a = fr"
+ − 250
with b show "fr = h a" by auto
+ − 251
qed
+ − 252
+ − 253
lemma fresh_fun_app':
+ − 254
fixes h :: "'a::at \<Rightarrow> 'b::pt"
+ − 255
assumes a: "atom a \<sharp> h" "atom a \<sharp> h a"
+ − 256
shows "fresh_fun h = h a"
+ − 257
apply (rule fresh_fun_app)
+ − 258
apply (auto simp add: fresh_Pair intro: a)
+ − 259
done
+ − 260
+ − 261
lemma fresh_fun_eqvt:
+ − 262
fixes h :: "'a::at \<Rightarrow> 'b::pt"
+ − 263
assumes a: "\<exists>a. atom a \<sharp> (h, h a)"
+ − 264
shows "p \<bullet> (fresh_fun h) = fresh_fun (p \<bullet> h)"
+ − 265
using a
+ − 266
apply (clarsimp simp add: fresh_Pair)
+ − 267
apply (subst fresh_fun_app', assumption+)
+ − 268
apply (drule fresh_permute_iff [where p=p, THEN iffD2])
+ − 269
apply (drule fresh_permute_iff [where p=p, THEN iffD2])
+ − 270
apply (simp add: atom_eqvt permute_fun_app_eq [where f=h])
+ − 271
apply (erule (1) fresh_fun_app' [symmetric])
+ − 272
done
+ − 273
+ − 274
lemma fresh_fun_supports:
+ − 275
fixes h :: "'a::at \<Rightarrow> 'b::pt"
+ − 276
assumes a: "\<exists>a. atom a \<sharp> (h, h a)"
+ − 277
shows "(supp h) supports (fresh_fun h)"
+ − 278
apply (simp add: supports_def fresh_def [symmetric])
+ − 279
apply (simp add: fresh_fun_eqvt [OF a] swap_fresh_fresh)
+ − 280
done
+ − 281
+ − 282
notation fresh_fun (binder "FRESH " 10)
+ − 283
+ − 284
lemma FRESH_f_iff:
+ − 285
fixes P :: "'a::at \<Rightarrow> 'b::pure"
+ − 286
fixes f :: "'b \<Rightarrow> 'c::pure"
+ − 287
assumes P: "finite (supp P)"
+ − 288
shows "(FRESH x. f (P x)) = f (FRESH x. P x)"
+ − 289
proof -
+ − 290
obtain a::'a where "atom a \<notin> supp P"
+ − 291
using P by (rule obtain_at_base)
+ − 292
hence "atom a \<sharp> P"
+ − 293
by (simp add: fresh_def)
+ − 294
show "(FRESH x. f (P x)) = f (FRESH x. P x)"
+ − 295
apply (subst fresh_fun_app' [where a=a, OF _ pure_fresh])
+ − 296
apply (cut_tac `atom a \<sharp> P`)
+ − 297
apply (simp add: fresh_conv_MOST)
+ − 298
apply (elim MOST_rev_mp, rule MOST_I, clarify)
+ − 299
apply (simp add: permute_fun_def permute_pure expand_fun_eq)
+ − 300
apply (subst fresh_fun_app' [where a=a, OF `atom a \<sharp> P` pure_fresh])
+ − 301
apply (rule refl)
+ − 302
done
+ − 303
qed
+ − 304
+ − 305
lemma FRESH_binop_iff:
+ − 306
fixes P :: "'a::at \<Rightarrow> 'b::pure"
+ − 307
fixes Q :: "'a::at \<Rightarrow> 'c::pure"
+ − 308
fixes binop :: "'b \<Rightarrow> 'c \<Rightarrow> 'd::pure"
+ − 309
assumes P: "finite (supp P)"
+ − 310
and Q: "finite (supp Q)"
+ − 311
shows "(FRESH x. binop (P x) (Q x)) = binop (FRESH x. P x) (FRESH x. Q x)"
+ − 312
proof -
+ − 313
from assms have "finite (supp P \<union> supp Q)" by simp
+ − 314
then obtain a::'a where "atom a \<notin> (supp P \<union> supp Q)"
+ − 315
by (rule obtain_at_base)
+ − 316
hence "atom a \<sharp> P" and "atom a \<sharp> Q"
+ − 317
by (simp_all add: fresh_def)
+ − 318
show ?thesis
+ − 319
apply (subst fresh_fun_app' [where a=a, OF _ pure_fresh])
+ − 320
apply (cut_tac `atom a \<sharp> P` `atom a \<sharp> Q`)
+ − 321
apply (simp add: fresh_conv_MOST)
+ − 322
apply (elim MOST_rev_mp, rule MOST_I, clarify)
+ − 323
apply (simp add: permute_fun_def permute_pure expand_fun_eq)
+ − 324
apply (subst fresh_fun_app' [where a=a, OF `atom a \<sharp> P` pure_fresh])
+ − 325
apply (subst fresh_fun_app' [where a=a, OF `atom a \<sharp> Q` pure_fresh])
+ − 326
apply (rule refl)
+ − 327
done
+ − 328
qed
+ − 329
+ − 330
lemma FRESH_conj_iff:
+ − 331
fixes P Q :: "'a::at \<Rightarrow> bool"
+ − 332
assumes P: "finite (supp P)" and Q: "finite (supp Q)"
+ − 333
shows "(FRESH x. P x \<and> Q x) \<longleftrightarrow> (FRESH x. P x) \<and> (FRESH x. Q x)"
+ − 334
using P Q by (rule FRESH_binop_iff)
+ − 335
+ − 336
lemma FRESH_disj_iff:
+ − 337
fixes P Q :: "'a::at \<Rightarrow> bool"
+ − 338
assumes P: "finite (supp P)" and Q: "finite (supp Q)"
+ − 339
shows "(FRESH x. P x \<or> Q x) \<longleftrightarrow> (FRESH x. P x) \<or> (FRESH x. Q x)"
+ − 340
using P Q by (rule FRESH_binop_iff)
+ − 341
+ − 342
1930
+ − 343
section {* @{const nat_of} is an example of a function
+ − 344
without finite support *}
1062
+ − 345
+ − 346
+ − 347
lemma not_fresh_nat_of:
+ − 348
shows "\<not> a \<sharp> nat_of"
+ − 349
unfolding fresh_def supp_def
+ − 350
proof (clarsimp)
+ − 351
assume "finite {b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of}"
+ − 352
hence "finite ({a} \<union> {b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of})"
+ − 353
by simp
+ − 354
then obtain b where
+ − 355
b1: "b \<noteq> a" and
+ − 356
b2: "sort_of b = sort_of a" and
+ − 357
b3: "(a \<rightleftharpoons> b) \<bullet> nat_of = nat_of"
+ − 358
by (rule obtain_atom) auto
+ − 359
have "nat_of a = (a \<rightleftharpoons> b) \<bullet> (nat_of a)" by (simp add: permute_nat_def)
+ − 360
also have "\<dots> = ((a \<rightleftharpoons> b) \<bullet> nat_of) ((a \<rightleftharpoons> b) \<bullet> a)" by (simp add: permute_fun_app_eq)
+ − 361
also have "\<dots> = nat_of ((a \<rightleftharpoons> b) \<bullet> a)" using b3 by simp
+ − 362
also have "\<dots> = nat_of b" using b2 by simp
+ − 363
finally have "nat_of a = nat_of b" by simp
1930
+ − 364
with b2 have "a = b" by (simp add: atom_components_eq_iff)
1062
+ − 365
with b1 show "False" by simp
+ − 366
qed
+ − 367
+ − 368
lemma supp_nat_of:
+ − 369
shows "supp nat_of = UNIV"
+ − 370
using not_fresh_nat_of [unfolded fresh_def] by auto
+ − 371
+ − 372
1930
+ − 373
section {* Induction principle for permutations *}
1563
+ − 374
1918
e2e963f4e90d
added an improved version of the induction principle for permutations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 375
e2e963f4e90d
added an improved version of the induction principle for permutations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 376
lemma perm_struct_induct[consumes 1, case_names zero swap]:
1778
88ec05a09772
added an induction principle for permutations; removed add_perm construction
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 377
assumes S: "supp p \<subseteq> S"
1930
+ − 378
and zero: "P 0"
+ − 379
and swap: "\<And>p a b. \<lbrakk>P p; supp p \<subseteq> S; a \<in> S; b \<in> S; a \<noteq> b; sort_of a = sort_of b\<rbrakk> \<Longrightarrow> P ((a \<rightleftharpoons> b) + p)"
1778
88ec05a09772
added an induction principle for permutations; removed add_perm construction
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 380
shows "P p"
1777
+ − 381
proof -
+ − 382
have "finite (supp p)" by (simp add: finite_supp)
1918
e2e963f4e90d
added an improved version of the induction principle for permutations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 383
then show "P p" using S
1778
88ec05a09772
added an induction principle for permutations; removed add_perm construction
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 384
proof(induct A\<equiv>"supp p" arbitrary: p rule: finite_psubset_induct)
1777
+ − 385
case (psubset p)
1778
88ec05a09772
added an induction principle for permutations; removed add_perm construction
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 386
then have ih: "\<And>q. supp q \<subset> supp p \<Longrightarrow> P q" by auto
88ec05a09772
added an induction principle for permutations; removed add_perm construction
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 387
have as: "supp p \<subseteq> S" by fact
1777
+ − 388
{ assume "supp p = {}"
+ − 389
then have "p = 0" by (simp add: supp_perm expand_perm_eq)
1778
88ec05a09772
added an induction principle for permutations; removed add_perm construction
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 390
then have "P p" using zero by simp
1777
+ − 391
}
+ − 392
moreover
+ − 393
{ assume "supp p \<noteq> {}"
+ − 394
then obtain a where a0: "a \<in> supp p" by blast
1918
e2e963f4e90d
added an improved version of the induction principle for permutations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 395
then have a1: "p \<bullet> a \<in> S" "a \<in> S" "sort_of (p \<bullet> a) = sort_of a" "p \<bullet> a \<noteq> a" using as
1778
88ec05a09772
added an induction principle for permutations; removed add_perm construction
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 396
by (auto simp add: supp_atom supp_perm swap_atom)
1918
e2e963f4e90d
added an improved version of the induction principle for permutations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 397
let ?q = "(p \<bullet> a \<rightleftharpoons> a) + p"
1778
88ec05a09772
added an induction principle for permutations; removed add_perm construction
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 398
have a2: "supp ?q \<subseteq> supp p" unfolding supp_perm by (auto simp add: swap_atom)
1777
+ − 399
moreover
+ − 400
have "a \<notin> supp ?q" by (simp add: supp_perm)
+ − 401
then have "supp ?q \<noteq> supp p" using a0 by auto
1918
e2e963f4e90d
added an improved version of the induction principle for permutations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 402
ultimately have "supp ?q \<subset> supp p" using a2 by auto
1778
88ec05a09772
added an induction principle for permutations; removed add_perm construction
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 403
then have "P ?q" using ih by simp
88ec05a09772
added an induction principle for permutations; removed add_perm construction
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 404
moreover
88ec05a09772
added an induction principle for permutations; removed add_perm construction
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 405
have "supp ?q \<subseteq> S" using as a2 by simp
1918
e2e963f4e90d
added an improved version of the induction principle for permutations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 406
ultimately have "P ((p \<bullet> a \<rightleftharpoons> a) + ?q)" using as a1 swap by simp
1777
+ − 407
moreover
1918
e2e963f4e90d
added an improved version of the induction principle for permutations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 408
have "p = (p \<bullet> a \<rightleftharpoons> a) + ?q" by (simp add: expand_perm_eq)
1778
88ec05a09772
added an induction principle for permutations; removed add_perm construction
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 409
ultimately have "P p" by simp
1777
+ − 410
}
1778
88ec05a09772
added an induction principle for permutations; removed add_perm construction
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 411
ultimately show "P p" by blast
1777
+ − 412
qed
+ − 413
qed
1062
+ − 414
1930
+ − 415
lemma perm_simple_struct_induct[case_names zero swap]:
1923
+ − 416
assumes zero: "P 0"
1930
+ − 417
and swap: "\<And>p a b. \<lbrakk>P p; a \<noteq> b; sort_of a = sort_of b\<rbrakk> \<Longrightarrow> P ((a \<rightleftharpoons> b) + p)"
1923
+ − 418
shows "P p"
+ − 419
by (rule_tac S="supp p" in perm_struct_induct)
+ − 420
(auto intro: zero swap)
+ − 421
1930
+ − 422
lemma perm_subset_induct[consumes 1, case_names zero swap plus]:
1778
88ec05a09772
added an induction principle for permutations; removed add_perm construction
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 423
assumes S: "supp p \<subseteq> S"
88ec05a09772
added an induction principle for permutations; removed add_perm construction
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 424
assumes zero: "P 0"
88ec05a09772
added an induction principle for permutations; removed add_perm construction
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 425
assumes swap: "\<And>a b. \<lbrakk>sort_of a = sort_of b; a \<noteq> b; a \<in> S; b \<in> S\<rbrakk> \<Longrightarrow> P (a \<rightleftharpoons> b)"
88ec05a09772
added an induction principle for permutations; removed add_perm construction
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 426
assumes plus: "\<And>p1 p2. \<lbrakk>P p1; P p2; supp p1 \<subseteq> S; supp p2 \<subseteq> S\<rbrakk> \<Longrightarrow> P (p1 + p2)"
88ec05a09772
added an induction principle for permutations; removed add_perm construction
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 427
shows "P p"
1918
e2e963f4e90d
added an improved version of the induction principle for permutations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 428
using S
e2e963f4e90d
added an improved version of the induction principle for permutations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 429
by (induct p rule: perm_struct_induct)
e2e963f4e90d
added an improved version of the induction principle for permutations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 430
(auto intro: zero plus swap simp add: supp_swap)
1563
+ − 431
+ − 432
lemma supp_perm_eq:
1778
88ec05a09772
added an induction principle for permutations; removed add_perm construction
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 433
assumes "(supp x) \<sharp>* p"
1563
+ − 434
shows "p \<bullet> x = x"
+ − 435
proof -
1778
88ec05a09772
added an induction principle for permutations; removed add_perm construction
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 436
from assms have "supp p \<subseteq> {a. a \<sharp> x}"
88ec05a09772
added an induction principle for permutations; removed add_perm construction
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 437
unfolding supp_perm fresh_star_def fresh_def by auto
88ec05a09772
added an induction principle for permutations; removed add_perm construction
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 438
then show "p \<bullet> x = x"
1918
e2e963f4e90d
added an improved version of the induction principle for permutations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 439
proof (induct p rule: perm_struct_induct)
e2e963f4e90d
added an improved version of the induction principle for permutations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 440
case zero
e2e963f4e90d
added an improved version of the induction principle for permutations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 441
show "0 \<bullet> x = x" by simp
e2e963f4e90d
added an improved version of the induction principle for permutations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 442
next
e2e963f4e90d
added an improved version of the induction principle for permutations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 443
case (swap p a b)
e2e963f4e90d
added an improved version of the induction principle for permutations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 444
then have "a \<sharp> x" "b \<sharp> x" "p \<bullet> x = x" by simp_all
e2e963f4e90d
added an improved version of the induction principle for permutations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 445
then show "((a \<rightleftharpoons> b) + p) \<bullet> x = x" by (simp add: swap_fresh_fresh)
e2e963f4e90d
added an improved version of the induction principle for permutations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 446
qed
e2e963f4e90d
added an improved version of the induction principle for permutations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 447
qed
e2e963f4e90d
added an improved version of the induction principle for permutations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 448
e2e963f4e90d
added an improved version of the induction principle for permutations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 449
lemma supp_perm_eq_test:
e2e963f4e90d
added an improved version of the induction principle for permutations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 450
assumes "(supp x) \<sharp>* p"
e2e963f4e90d
added an improved version of the induction principle for permutations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 451
shows "p \<bullet> x = x"
e2e963f4e90d
added an improved version of the induction principle for permutations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 452
proof -
e2e963f4e90d
added an improved version of the induction principle for permutations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 453
from assms have "supp p \<subseteq> {a. a \<sharp> x}"
e2e963f4e90d
added an improved version of the induction principle for permutations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 454
unfolding supp_perm fresh_star_def fresh_def by auto
e2e963f4e90d
added an improved version of the induction principle for permutations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 455
then show "p \<bullet> x = x"
1778
88ec05a09772
added an induction principle for permutations; removed add_perm construction
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 456
proof (induct p rule: perm_subset_induct)
88ec05a09772
added an induction principle for permutations; removed add_perm construction
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 457
case zero
88ec05a09772
added an induction principle for permutations; removed add_perm construction
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 458
show "0 \<bullet> x = x" by simp
88ec05a09772
added an induction principle for permutations; removed add_perm construction
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 459
next
88ec05a09772
added an induction principle for permutations; removed add_perm construction
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 460
case (swap a b)
88ec05a09772
added an induction principle for permutations; removed add_perm construction
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 461
then have "a \<sharp> x" "b \<sharp> x" by simp_all
88ec05a09772
added an induction principle for permutations; removed add_perm construction
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 462
then show "(a \<rightleftharpoons> b) \<bullet> x = x" by (simp add: swap_fresh_fresh)
88ec05a09772
added an induction principle for permutations; removed add_perm construction
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 463
next
88ec05a09772
added an induction principle for permutations; removed add_perm construction
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 464
case (plus p1 p2)
88ec05a09772
added an induction principle for permutations; removed add_perm construction
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 465
have "p1 \<bullet> x = x" "p2 \<bullet> x = x" by fact+
88ec05a09772
added an induction principle for permutations; removed add_perm construction
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 466
then show "(p1 + p2) \<bullet> x = x" by simp
88ec05a09772
added an induction principle for permutations; removed add_perm construction
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 467
qed
1563
+ − 468
qed
+ − 469
2003
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 470
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 471
section {* Support of Finite Sets of Finitely Supported Elements *}
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 472
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 473
lemma Union_fresh:
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 474
shows "a \<sharp> S \<Longrightarrow> a \<sharp> (\<Union>x \<in> S. supp x)"
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 475
unfolding Union_image_eq[symmetric]
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 476
apply(rule_tac f="\<lambda>S. \<Union> supp ` S" in fresh_fun_eqvt_app)
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 477
apply(perm_simp)
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 478
apply(rule refl)
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 479
apply(assumption)
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 480
done
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 481
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 482
lemma Union_supports_set:
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 483
shows "(\<Union>x \<in> S. supp x) supports S"
2012
+ − 484
proof -
+ − 485
{ fix a b
+ − 486
have "\<forall>x \<in> S. (a \<rightleftharpoons> b) \<bullet> x = x \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> S = S"
+ − 487
unfolding permute_set_eq by force
+ − 488
}
+ − 489
then show "(\<Union>x \<in> S. supp x) supports S"
+ − 490
unfolding supports_def
+ − 491
by (simp add: fresh_def[symmetric] swap_fresh_fresh)
+ − 492
qed
2003
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 493
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 494
lemma Union_of_fin_supp_sets:
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 495
fixes S::"('a::fs set)"
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 496
assumes fin: "finite S"
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 497
shows "finite (\<Union>x\<in>S. supp x)"
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 498
using fin by (induct) (auto simp add: finite_supp)
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 499
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 500
lemma Union_included_in_supp:
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 501
fixes S::"('a::fs set)"
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 502
assumes fin: "finite S"
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 503
shows "(\<Union>x\<in>S. supp x) \<subseteq> supp S"
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 504
proof -
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 505
have "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)"
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 506
apply(rule supp_finite_atom_set[symmetric])
2012
+ − 507
apply(rule Union_of_fin_supp_sets[OF fin])
2003
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 508
done
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 509
also have "\<dots> \<subseteq> supp S"
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 510
apply(rule supp_subset_fresh)
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 511
apply(simp add: Union_fresh)
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 512
done
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 513
finally show ?thesis .
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 514
qed
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 515
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 516
lemma supp_of_fin_sets:
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 517
fixes S::"('a::fs set)"
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 518
assumes fin: "finite S"
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 519
shows "(supp S) = (\<Union>x\<in>S. supp x)"
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 520
apply(rule subset_antisym)
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 521
apply(rule supp_is_subset)
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 522
apply(rule Union_supports_set)
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 523
apply(rule Union_of_fin_supp_sets[OF fin])
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 524
apply(rule Union_included_in_supp[OF fin])
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 525
done
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 526
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 527
lemma supp_of_fin_union:
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 528
fixes S T::"('a::fs) set"
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 529
assumes fin1: "finite S"
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 530
and fin2: "finite T"
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 531
shows "supp (S \<union> T) = supp S \<union> supp T"
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 532
using fin1 fin2
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 533
by (simp add: supp_of_fin_sets)
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 534
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 535
lemma supp_of_fin_insert:
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 536
fixes S::"('a::fs) set"
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 537
assumes fin: "finite S"
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 538
shows "supp (insert x S) = supp x \<union> supp S"
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 539
using fin
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 540
by (simp add: supp_of_fin_sets)
b53e98bfb298
added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 541
1567
+ − 542
end