| author | Christian Urban <urbanc@in.tum.de> |
| Sun, 14 Nov 2010 11:05:22 +0000 | |
| changeset 2565 | 6bf332360510 |
| parent 2559 | add799cf0817 |
| child 2566 | a59d8e1e3a17 |
| permissions | -rw-r--r-- |
|
1534
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
1 |
theory Nominal2_FSet |
|
2467
67b3933c3190
got rid of Nominal_Atoms (folded into Nominal2_Base)
Christian Urban <urbanc@in.tum.de>
parents:
2466
diff
changeset
|
2 |
imports "../Nominal-General/Nominal2_Base" |
|
2565
6bf332360510
moved most material fron Nominal2_FSet into the Nominal_Base theory
Christian Urban <urbanc@in.tum.de>
parents:
2559
diff
changeset
|
3 |
"../Nominal-General/Nominal2_Eqvt" |
|
1534
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
4 |
begin |
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
5 |
|
|
2004
b96e8cf86891
generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements)
Christian Urban <urbanc@in.tum.de>
parents:
1973
diff
changeset
|
6 |
|
|
2540
135ac0fb2686
naming scheme is now *_fset (not f*_)
Christian Urban <urbanc@in.tum.de>
parents:
2535
diff
changeset
|
7 |
lemma atom_map_fset_cong: |
|
135ac0fb2686
naming scheme is now *_fset (not f*_)
Christian Urban <urbanc@in.tum.de>
parents:
2535
diff
changeset
|
8 |
shows "map_fset atom x = map_fset atom y \<longleftrightarrow> x = y" |
| 2542 | 9 |
apply(rule inj_map_fset_cong) |
|
1534
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
10 |
apply(simp add: inj_on_def) |
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
11 |
done |
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
12 |
|
|
2540
135ac0fb2686
naming scheme is now *_fset (not f*_)
Christian Urban <urbanc@in.tum.de>
parents:
2535
diff
changeset
|
13 |
lemma supp_map_fset_atom: |
|
135ac0fb2686
naming scheme is now *_fset (not f*_)
Christian Urban <urbanc@in.tum.de>
parents:
2535
diff
changeset
|
14 |
shows "supp (map_fset atom S) = supp S" |
|
1818
37480540c1af
made everything to compile
Christian Urban <urbanc@in.tum.de>
parents:
1815
diff
changeset
|
15 |
unfolding supp_def |
|
2004
b96e8cf86891
generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements)
Christian Urban <urbanc@in.tum.de>
parents:
1973
diff
changeset
|
16 |
apply(perm_simp) |
|
2540
135ac0fb2686
naming scheme is now *_fset (not f*_)
Christian Urban <urbanc@in.tum.de>
parents:
2535
diff
changeset
|
17 |
apply(simp add: atom_map_fset_cong) |
|
1568
2311a9fc4624
Strong induction for Type Schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1542
diff
changeset
|
18 |
done |
|
2311a9fc4624
Strong induction for Type Schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1542
diff
changeset
|
19 |
|
|
2311a9fc4624
Strong induction for Type Schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1542
diff
changeset
|
20 |
lemma supp_at_fset: |
|
1973
fc5ce7f22b74
use the more general type-class at_base
Christian Urban <urbanc@in.tum.de>
parents:
1933
diff
changeset
|
21 |
fixes S::"('a::at_base) fset"
|
|
2540
135ac0fb2686
naming scheme is now *_fset (not f*_)
Christian Urban <urbanc@in.tum.de>
parents:
2535
diff
changeset
|
22 |
shows "supp S = fset (map_fset atom S)" |
|
1973
fc5ce7f22b74
use the more general type-class at_base
Christian Urban <urbanc@in.tum.de>
parents:
1933
diff
changeset
|
23 |
apply (induct S) |
|
2540
135ac0fb2686
naming scheme is now *_fset (not f*_)
Christian Urban <urbanc@in.tum.de>
parents:
2535
diff
changeset
|
24 |
apply (simp add: supp_empty_fset) |
|
135ac0fb2686
naming scheme is now *_fset (not f*_)
Christian Urban <urbanc@in.tum.de>
parents:
2535
diff
changeset
|
25 |
apply (simp add: supp_insert_fset) |
|
1542
63e327e95abd
Showed the instance: fset::(at) fs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1534
diff
changeset
|
26 |
apply (simp add: supp_at_base) |
|
63e327e95abd
Showed the instance: fset::(at) fs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1534
diff
changeset
|
27 |
done |
|
1534
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
28 |
|
|
2178
e559513143e9
reversing the direction of fresh_star
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2004
diff
changeset
|
29 |
lemma fresh_star_atom: |
| 2447 | 30 |
fixes a::"'a::at_base" |
|
2524
693562f03eee
major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Christian Urban <urbanc@in.tum.de>
parents:
2471
diff
changeset
|
31 |
shows "fset S \<sharp>* a \<Longrightarrow> atom a \<sharp> fset S" |
| 2447 | 32 |
apply (induct S) |
|
2178
e559513143e9
reversing the direction of fresh_star
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2004
diff
changeset
|
33 |
apply (simp add: fresh_set_empty) |
|
e559513143e9
reversing the direction of fresh_star
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2004
diff
changeset
|
34 |
apply simp |
|
e559513143e9
reversing the direction of fresh_star
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2004
diff
changeset
|
35 |
apply (unfold fresh_def) |
|
2565
6bf332360510
moved most material fron Nominal2_FSet into the Nominal_Base theory
Christian Urban <urbanc@in.tum.de>
parents:
2559
diff
changeset
|
36 |
apply (simp add: supp_of_finite_insert) |
|
2178
e559513143e9
reversing the direction of fresh_star
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2004
diff
changeset
|
37 |
apply (rule conjI) |
|
e559513143e9
reversing the direction of fresh_star
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2004
diff
changeset
|
38 |
apply (unfold fresh_star_def) |
|
e559513143e9
reversing the direction of fresh_star
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2004
diff
changeset
|
39 |
apply simp |
|
e559513143e9
reversing the direction of fresh_star
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2004
diff
changeset
|
40 |
apply (unfold fresh_def) |
|
e559513143e9
reversing the direction of fresh_star
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2004
diff
changeset
|
41 |
apply (simp add: supp_at_base supp_atom) |
|
e559513143e9
reversing the direction of fresh_star
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2004
diff
changeset
|
42 |
apply clarify |
|
e559513143e9
reversing the direction of fresh_star
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2004
diff
changeset
|
43 |
apply auto |
|
e559513143e9
reversing the direction of fresh_star
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2004
diff
changeset
|
44 |
done |
|
2004
b96e8cf86891
generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements)
Christian Urban <urbanc@in.tum.de>
parents:
1973
diff
changeset
|
45 |
|
|
1534
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
46 |
end |