equal
deleted
inserted
replaced
1387 lemma supp_empty_fset [simp]: |
1387 lemma supp_empty_fset [simp]: |
1388 shows "supp {||} = {}" |
1388 shows "supp {||} = {}" |
1389 unfolding supp_def |
1389 unfolding supp_def |
1390 by simp |
1390 by simp |
1391 |
1391 |
|
1392 lemma fresh_empty_fset: |
|
1393 shows "a \<sharp> {||}" |
|
1394 unfolding fresh_def |
|
1395 by (simp) |
|
1396 |
1392 lemma supp_insert_fset [simp]: |
1397 lemma supp_insert_fset [simp]: |
1393 fixes x::"'a::fs" |
1398 fixes x::"'a::fs" |
1394 and S::"'a fset" |
1399 and S::"'a fset" |
1395 shows "supp (insert_fset x S) = supp x \<union> supp S" |
1400 shows "supp (insert_fset x S) = supp x \<union> supp S" |
1396 apply(subst supp_fset[symmetric]) |
1401 apply(subst supp_fset[symmetric]) |
1397 apply(simp add: supp_of_finite_insert) |
1402 apply(simp add: supp_of_finite_insert) |
1398 done |
1403 done |
|
1404 |
|
1405 lemma fresh_insert_fset: |
|
1406 fixes x::"'a::fs" |
|
1407 and S::"'a fset" |
|
1408 shows "a \<sharp> insert_fset x S \<longleftrightarrow> a \<sharp> x \<and> a \<sharp> S" |
|
1409 unfolding fresh_def |
|
1410 by (simp) |
1399 |
1411 |
1400 lemma fset_finite_supp: |
1412 lemma fset_finite_supp: |
1401 fixes S::"('a::fs) fset" |
1413 fixes S::"('a::fs) fset" |
1402 shows "finite (supp S)" |
1414 shows "finite (supp S)" |
1403 by (induct S) (simp_all add: finite_supp) |
1415 by (induct S) (simp_all add: finite_supp) |