9 "\<forall>xs \<in> (\<lambda>xs. memb x xs). memb x (y # xs)" |
9 "\<forall>xs \<in> (\<lambda>xs. memb x xs). memb x (y # xs)" |
10 apply (simp add: memb_def) |
10 apply (simp add: memb_def) |
11 apply (metis mem_def) |
11 apply (metis mem_def) |
12 done |
12 done |
13 |
13 |
14 (* Should not work and doesn't. |
|
15 thm test[quot_lifted] |
14 thm test[quot_lifted] |
16 *) |
|
17 |
15 |
18 lemma "\<forall>xs \<in> (\<lambda>xs. x |\<in>| xs). x |\<in>| finsert y xs" |
16 lemma "\<forall>xs \<in> (\<lambda>xs. x |\<in>| xs). x |\<in>| finsert y xs" |
19 unfolding Ball_def mem_def |
17 unfolding Ball_def |
20 by (lifting test[unfolded Ball_def mem_def]) |
18 by (lifting test[unfolded Ball_def]) |
21 |
19 |
22 ML {* Quotient_Tacs.lifted @{context} [@{typ "'a fset"}] @{thms Ball_def Bex_def mem_def} @{thm test}*} |
20 ML {* Quotient_Tacs.lifted @{context} [@{typ "'a fset"}] @{thms Ball_def Bex_def} @{thm test}*} |
23 |
21 |
24 lemma test2: |
22 lemma test2: |
25 "\<exists>xs \<in> (\<lambda>xs. xs \<approx> []). xs \<approx> []" |
23 "\<exists>xs \<in> (\<lambda>xs. xs \<approx> []). xs \<approx> []" |
26 apply (rule_tac x="[]" in bexI) |
24 apply (rule_tac x="[]" in bexI) |
27 apply (auto simp add: mem_def) |
25 apply (auto simp add: mem_def) |
28 done |
26 done |
29 |
27 |
30 (* Should not work and doesn't |
|
31 thm test2[quot_lifted] |
28 thm test2[quot_lifted] |
32 *) |
|
33 |
29 |
34 lemma "\<exists>xs \<in> (\<lambda>xs. xs = {||}). xs = {||}" |
30 lemma "\<exists>xs \<in> (\<lambda>xs. xs = {||}). xs = {||}" |
35 unfolding Bex_def mem_def |
31 unfolding Bex_def |
36 by (lifting test2[unfolded Bex_def mem_def]) |
32 by (lifting test2[unfolded Bex_def]) |
37 |
33 |
38 ML {* Quotient_Tacs.lifted @{context} [@{typ "'a fset"}] @{thms Bex_def mem_def} @{thm test2}*} |
34 ML {* Quotient_Tacs.lifted @{context} [@{typ "'a fset"}] @{thms Bex_def} @{thm test2}*} |
39 |
35 |
40 end |
36 end |