470 

   471 section {* Support of Finite Sets of Finitely Supported Elements *}

   472 

   473 lemma Union_fresh:

   474   shows "a \<sharp> S \<Longrightarrow> a \<sharp> (\<Union>x \<in> S. supp x)"

   475   unfolding Union_image_eq[symmetric]

   476   apply(rule_tac f="\<lambda>S. \<Union> supp ` S" in fresh_fun_eqvt_app)

   477   apply(perm_simp)

   478   apply(rule refl)

   479   apply(assumption)

   480   done

   481 

   482 lemma Union_supports_set:

   483   shows "(\<Union>x \<in> S. supp x) supports S"

   484   apply(simp add: supports_def fresh_def[symmetric])

   485   apply(rule allI)+

   486   apply(rule impI)

   487   apply(erule conjE)

   488   apply(simp add: permute_set_eq)

   489   apply(auto)

   490   apply(subgoal_tac "(a \<rightleftharpoons> b) \<bullet> xa = xa")(*A*)

   491   apply(simp)

   492   apply(rule swap_fresh_fresh)

   493   apply(force)

   494   apply(force)

   495   apply(rule_tac x="x" in exI)

   496   apply(simp)

   497   apply(rule sym)

   498   apply(rule swap_fresh_fresh)

   499   apply(auto)

   500   done

   501 

   502 lemma Union_of_fin_supp_sets:

   503   fixes S::"('a::fs set)"

   504   assumes fin: "finite S"   

   505   shows "finite (\<Union>x\<in>S. supp x)"

   506   using fin by (induct) (auto simp add: finite_supp)

   507 

   508 lemma Union_included_in_supp:

   509   fixes S::"('a::fs set)"

   510   assumes fin: "finite S"

   511   shows "(\<Union>x\<in>S. supp x) \<subseteq> supp S"

   512 proof -

   513   have "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)"

   514     apply(rule supp_finite_atom_set[symmetric])

   515     apply(rule Union_of_fin_supp_sets)

   516     apply(rule fin)

   517     done

   518   also have "\<dots> \<subseteq> supp S"

   519     apply(rule supp_subset_fresh)

   520     apply(simp add: Union_fresh)

   521     done

   522   finally show ?thesis .

   523 qed

   524 

   525 lemma supp_of_fin_sets:

   526   fixes S::"('a::fs set)"

   527   assumes fin: "finite S"

   528   shows "(supp S) = (\<Union>x\<in>S. supp x)"

   529 apply(rule subset_antisym)

   530 apply(rule supp_is_subset)

   531 apply(rule Union_supports_set)

   532 apply(rule Union_of_fin_supp_sets[OF fin])

   533 apply(rule Union_included_in_supp[OF fin])

   534 done

   535 

   536 lemma supp_of_fin_union:

   537   fixes S T::"('a::fs) set"

   538   assumes fin1: "finite S"

   539   and     fin2: "finite T"

   540   shows "supp (S \<union> T) = supp S \<union> supp T"

   541   using fin1 fin2

   542   by (simp add: supp_of_fin_sets)

   543 

   544 lemma supp_of_fin_insert:

   545   fixes S::"('a::fs) set"

   546   assumes fin:  "finite S"

   547   shows "supp (insert x S) = supp x \<union> supp S"

   548   using fin

   549   by (simp add: supp_of_fin_sets)

   550