2441
|
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"
|
2456
5e76af0a51f9
No need to unfold mem_def with rsp/prs (requires new isabelle).
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
17 |
unfolding Ball_def
|
5e76af0a51f9
No need to unfold mem_def with rsp/prs (requires new isabelle).
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
18 |
by (lifting test[unfolded Ball_def])
|
2441
|
19 |
|
2456
5e76af0a51f9
No need to unfold mem_def with rsp/prs (requires new isabelle).
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
20 |
ML {* Quotient_Tacs.lifted @{context} [@{typ "'a fset"}] @{thms Ball_def Bex_def} @{thm test}*}
|
2441
|
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 = {||}"
|
2456
5e76af0a51f9
No need to unfold mem_def with rsp/prs (requires new isabelle).
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
31 |
unfolding Bex_def
|
5e76af0a51f9
No need to unfold mem_def with rsp/prs (requires new isabelle).
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
32 |
by (lifting test2[unfolded Bex_def])
|
2441
|
33 |
|
2456
5e76af0a51f9
No need to unfold mem_def with rsp/prs (requires new isabelle).
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
34 |
ML {* Quotient_Tacs.lifted @{context} [@{typ "'a fset"}] @{thms Bex_def} @{thm test2}*}
|
2441
|
35 |
|
|
36 |
end
|