theory FSet_ballbex

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

begin

notation

  list_eq (infix "\<approx>" 50)

lemma test:

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

  apply (simp add: memb_def)

  apply (metis mem_def)

  done

(* Should not work and doesn't.

thm test[quot_lifted]

*)

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

  unfolding Ball_def mem_def

  by (lifting test[unfolded Ball_def mem_def])

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

lemma test2:

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

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

  apply (auto simp add: mem_def)

  done

(* Should not work and doesn't

thm test2[quot_lifted]

*)

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

  unfolding Bex_def mem_def

  by (lifting test2[unfolded Bex_def mem_def])

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

end