| author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
| Mon, 30 Aug 2010 15:55:08 +0900 | |
| changeset 2456 | 5e76af0a51f9 |
| parent 2441 | fc3e8f79e698 |
| permissions | -rw-r--r-- |
|
2441
fc3e8f79e698
Ball Bex can be lifted after unfolding.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
1 |
theory FSet_ballbex |
|
fc3e8f79e698
Ball Bex can be lifted after unfolding.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
2 |
imports "../../../Nominal/FSet" |
|
fc3e8f79e698
Ball Bex can be lifted after unfolding.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
3 |
begin |
|
fc3e8f79e698
Ball Bex can be lifted after unfolding.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
4 |
|
|
fc3e8f79e698
Ball Bex can be lifted after unfolding.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
5 |
notation |
|
fc3e8f79e698
Ball Bex can be lifted after unfolding.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
6 |
list_eq (infix "\<approx>" 50) |
|
fc3e8f79e698
Ball Bex can be lifted after unfolding.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
7 |
|
|
fc3e8f79e698
Ball Bex can be lifted after unfolding.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
8 |
lemma test: |
|
fc3e8f79e698
Ball Bex can be lifted after unfolding.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
9 |
"\<forall>xs \<in> (\<lambda>xs. memb x xs). memb x (y # xs)" |
|
fc3e8f79e698
Ball Bex can be lifted after unfolding.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
10 |
apply (simp add: memb_def) |
|
fc3e8f79e698
Ball Bex can be lifted after unfolding.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
11 |
apply (metis mem_def) |
|
fc3e8f79e698
Ball Bex can be lifted after unfolding.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
12 |
done |
|
fc3e8f79e698
Ball Bex can be lifted after unfolding.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
13 |
|
|
fc3e8f79e698
Ball Bex can be lifted after unfolding.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
14 |
thm test[quot_lifted] |
|
fc3e8f79e698
Ball Bex can be lifted after unfolding.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
15 |
|
|
fc3e8f79e698
Ball Bex can be lifted after unfolding.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
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>
parents:
2441
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>
parents:
2441
diff
changeset
|
18 |
by (lifting test[unfolded Ball_def]) |
|
2441
fc3e8f79e698
Ball Bex can be lifted after unfolding.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
19 |
|
|
2456
5e76af0a51f9
No need to unfold mem_def with rsp/prs (requires new isabelle).
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2441
diff
changeset
|
20 |
ML {* Quotient_Tacs.lifted @{context} [@{typ "'a fset"}] @{thms Ball_def Bex_def} @{thm test}*}
|
|
2441
fc3e8f79e698
Ball Bex can be lifted after unfolding.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
21 |
|
|
fc3e8f79e698
Ball Bex can be lifted after unfolding.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
22 |
lemma test2: |
|
fc3e8f79e698
Ball Bex can be lifted after unfolding.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
23 |
"\<exists>xs \<in> (\<lambda>xs. xs \<approx> []). xs \<approx> []" |
|
fc3e8f79e698
Ball Bex can be lifted after unfolding.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
24 |
apply (rule_tac x="[]" in bexI) |
|
fc3e8f79e698
Ball Bex can be lifted after unfolding.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
25 |
apply (auto simp add: mem_def) |
|
fc3e8f79e698
Ball Bex can be lifted after unfolding.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
26 |
done |
|
fc3e8f79e698
Ball Bex can be lifted after unfolding.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
27 |
|
|
fc3e8f79e698
Ball Bex can be lifted after unfolding.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
28 |
thm test2[quot_lifted] |
|
fc3e8f79e698
Ball Bex can be lifted after unfolding.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
29 |
|
|
fc3e8f79e698
Ball Bex can be lifted after unfolding.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
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>
parents:
2441
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>
parents:
2441
diff
changeset
|
32 |
by (lifting test2[unfolded Bex_def]) |
|
2441
fc3e8f79e698
Ball Bex can be lifted after unfolding.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
33 |
|
|
2456
5e76af0a51f9
No need to unfold mem_def with rsp/prs (requires new isabelle).
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2441
diff
changeset
|
34 |
ML {* Quotient_Tacs.lifted @{context} [@{typ "'a fset"}] @{thms Bex_def} @{thm test2}*}
|
|
2441
fc3e8f79e698
Ball Bex can be lifted after unfolding.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
35 |
|
|
fc3e8f79e698
Ball Bex can be lifted after unfolding.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
36 |
end |