1 theory QuotientSet

     2 imports 

     3   "../Nominal2"

     4 begin

     5 

     6 lemma supp_quot:

     7   "(supp (R, x)) supports (R `` {x})"

     8 unfolding supports_def

     9 unfolding fresh_def[symmetric]

    10 apply(perm_simp)

    11 apply(simp add: swap_fresh_fresh)

    12 done

    13 

    14 lemma

    15   assumes "equiv UNIV R"

    16   and "(x, y) \<in> R"

    17   shows "R `` {x} = R `` {y}"

    18 using assms

    19 by (rule equiv_class_eq)

    20 

    21 lemma s1:

    22   assumes "equiv UNIV R"

    23   and "(x, y) \<in> R"

    24   shows "a \<sharp> (R `` {x}) \<longleftrightarrow> a \<sharp> (R `` {y})"

    25 using assms

    26 apply(subst equiv_class_eq)

    27 apply(auto)

    28 done

    29 

    30 lemma s2:

    31   fixes x::"'a::fs"

    32   assumes "equiv UNIV R"

    33   and     "supp R = {}"

    34   shows "\<Inter>{supp y | y. (x, y) \<in> R} supports (R `` {x})"

    35 unfolding supports_def

    36 apply(rule allI)+

    37 apply(rule impI)

    38 apply(rule swap_fresh_fresh)

    39 apply(drule conjunct1)

    40 apply(auto)[1]

    41 apply(subst s1)

    42 apply(rule assms)

    43 apply(assumption)

    44 apply(rule supports_fresh)

    45 apply(rule supp_quot)

    46 apply(simp add: supp_Pair finite_supp assms)

    47 apply(simp add: supp_Pair assms)

    48 apply(drule conjunct2)

    49 apply(auto)[1]

    50 apply(subst s1)

    51 apply(rule assms)

    52 apply(assumption)

    53 apply(rule supports_fresh)

    54 apply(rule supp_quot)

    55 apply(simp add: supp_Pair finite_supp assms)

    56 apply(simp add: supp_Pair assms)

    57 done

    58 

    59 lemma s3:

    60   fixes S::"'a::fs set"

    61   assumes "finite S"

    62   and "S \<noteq> {}"

    63   and "a \<sharp> S"

    64   shows "\<exists>x \<in> S. a \<sharp> x"

    65 using assms

    66 apply(auto simp add: fresh_def)

    67 apply(subst (asm) supp_of_finite_sets)

    68 apply(auto)

    69 done

    70 

    71 (*

    72 lemma supp_inter:

    73   fixes x::"'a::fs"

    74   assumes "equiv UNIV R"

    75   and     "supp R = {}"

    76   shows "supp (R `` {x}) = \<Inter>{supp y | y. (x, y) \<in> R}"

    77 apply(rule finite_supp_unique)

    78 apply(rule s2)

    79 apply(rule assms)

    80 apply(rule assms)

    81 apply(metis (lam_lifting, no_types) at_base_infinite finite_UNIV)

    82 *)

    83 

    84   

    85 

    86 

    87 

    88 end

    89 

    90 

    91