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