58 thm list_induct2'[no_vars]

    59 

    60 lemma fset_induct2:

    61     "Pa {||} {||} \<Longrightarrow>

    62     (\<forall>x xs. Pa (finsert x xs) {||}) \<Longrightarrow>

    63     (\<forall>y ys. Pa {||} (finsert y ys)) \<Longrightarrow>

    64     (\<forall>x xs y ys. Pa xs ys \<longrightarrow> Pa (finsert x xs) (finsert y ys)) \<Longrightarrow>

    65     Pa xsa ysa"

    66 by (lifting list_induct2')

    67 

    68 lemma set_cong: "(set x = set y) = (x \<approx> y)"

    69   apply rule

    70   apply simp_all

    71   apply (induct x y rule: list_induct2')

    72   apply simp_all

    73   apply auto

    74   done

    75 

    76 lemma fset_cong:

    77   "(fset_to_set x = fset_to_set y) = (x = y)"

    78   by (lifting set_cong)

    79 

    80 lemma supp_fset_to_set:

    81   "supp (fset_to_set x) = supp x"

    82   apply (simp add: supp_def)

    83   apply (simp add: eqvts)

    84   apply (simp add: fset_cong)

    85   done

    86 

    87 lemma inj_map_eq_iff:

    88   "inj f \<Longrightarrow> (map f l \<approx> map f m) = (l \<approx> m)"

    89   by (simp add: Set.expand_set_eq[symmetric] inj_image_eq_iff)

    90 

    91 lemma inj_fmap_eq_iff:

    92   "inj f \<Longrightarrow> (fmap f l = fmap f m) = (l = m)"

    93   by (lifting inj_map_eq_iff)

    94 

    95 lemma atom_fmap_cong:

    96   shows "(fmap atom x = fmap atom y) = (x = y)"

    97   apply(rule inj_fmap_eq_iff)

    98   apply(simp add: inj_on_def)

    99   done

   100 

   109 

   110 lemma supp_fmap_atom:

   111   "supp (fmap atom x) = supp x"

   112   apply (simp add: supp_def)

   113   apply (simp add: eqvts eqvts_raw atom_fmap_cong)

   114   done