1 theory FSet_ballbex

     2 imports "../../../Nominal/FSet"

     3 begin

     4 

     5 notation

     6   list_eq (infix "\<approx>" 50)

     7 

     8 lemma test:

     9   "\<forall>xs \<in> (\<lambda>xs. memb x xs). memb x (y # xs)"

    10   apply (simp add: memb_def)

    11   apply (metis mem_def)

    12   done

    13 

    14 thm test[quot_lifted]

    15 

    16 lemma "\<forall>xs \<in> (\<lambda>xs. x |\<in>| xs). x |\<in>| finsert y xs"

    17   unfolding Ball_def

    18   by (lifting test[unfolded Ball_def])

    19 

    20 ML {* Quotient_Tacs.lifted @{context} [@{typ "'a fset"}] @{thms Ball_def Bex_def} @{thm test}*}

    21 

    22 lemma test2:

    23   "\<exists>xs \<in> (\<lambda>xs. xs \<approx> []). xs \<approx> []"

    24   apply (rule_tac x="[]" in bexI)

    25   apply (auto simp add: mem_def)

    26   done

    27 

    28 thm test2[quot_lifted]

    29 

    30 lemma "\<exists>xs \<in> (\<lambda>xs. xs = {||}). xs = {||}"

    31   unfolding Bex_def

    32   by (lifting test2[unfolded Bex_def])

    33 

    34 ML {* Quotient_Tacs.lifted @{context} [@{typ "'a fset"}] @{thms Bex_def} @{thm test2}*}

    35 

    36 end