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 (* Should not work and doesn't.

    15 thm test[quot_lifted]

    16 *)

    17 

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

    19   unfolding Ball_def mem_def

    20   by (lifting test[unfolded Ball_def mem_def])

    21 

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

    23 

    24 lemma test2:

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

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

    27   apply (auto simp add: mem_def)

    28   done

    29 

    30 (* Should not work and doesn't

    31 thm test2[quot_lifted]

    32 *)

    33 

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

    35   unfolding Bex_def mem_def

    36   by (lifting test2[unfolded Bex_def mem_def])

    37 

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

    39 

    40 end