| author | Christian Urban <urbanc@in.tum.de> |
| Thu, 14 Oct 2010 17:32:06 +0100 | |
| changeset 2527 | 40187684fc16 |
| parent 2524 | 693562f03eee |
| child 2535 | 05f98e2ee48b |
| 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" |
| 2302 | 3 |
"../Nominal-General/Nominal2_Eqvt" |
| 1806 | 4 |
FSet |
|
1534
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
5 |
begin |
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
6 |
|
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
7 |
lemma permute_rsp_fset[quot_respect]: |
| 2447 | 8 |
shows "(op = ===> list_eq ===> list_eq) permute permute" |
9 |
apply(simp) |
|
10 |
apply(clarify) |
|
| 2468 | 11 |
apply(rule_tac p="-x" in permute_boolE) |
12 |
apply(perm_simp add: permute_minus_cancel) |
|
| 2447 | 13 |
apply(simp) |
|
1534
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
14 |
done |
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
15 |
|
|
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 |
instantiation fset :: (pt) pt |
|
1534
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
17 |
begin |
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
18 |
|
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
19 |
quotient_definition |
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
20 |
"permute_fset :: perm \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
21 |
is |
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
22 |
"permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
23 |
|
|
1815
4135198bbb8a
moved equivariance of map into Nominal2_Eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
1806
diff
changeset
|
24 |
instance |
|
4135198bbb8a
moved equivariance of map into Nominal2_Eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
1806
diff
changeset
|
25 |
proof |
| 1782 | 26 |
fix x :: "'a fset" and p q :: "perm" |
|
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
|
27 |
show "0 \<bullet> x = x" by (descending) (simp) |
|
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
|
28 |
show "(p + q) \<bullet> x = p \<bullet> q \<bullet> x" by (descending) (simp) |
| 1782 | 29 |
qed |
|
1534
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
30 |
|
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
31 |
end |
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
32 |
|
|
2466
47c840599a6b
cleaned a bit various thy-files in Nominal-General
Christian Urban <urbanc@in.tum.de>
parents:
2447
diff
changeset
|
33 |
lemma permute_fset[simp, eqvt]: |
|
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
|
34 |
fixes S::"('a::pt) fset"
|
|
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
|
35 |
shows "(p \<bullet> {||}) = ({||} ::('a::pt) fset)"
|
|
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
|
36 |
and "p \<bullet> finsert x S = finsert (p \<bullet> x) (p \<bullet> S)" |
|
1534
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
37 |
by (lifting permute_list.simps) |
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
38 |
|
|
1815
4135198bbb8a
moved equivariance of map into Nominal2_Eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
1806
diff
changeset
|
39 |
lemma fmap_eqvt[eqvt]: |
|
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
|
40 |
shows "p \<bullet> (fmap f S) = fmap (p \<bullet> f) (p \<bullet> S)" |
|
1534
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
41 |
by (lifting map_eqvt) |
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
42 |
|
|
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
|
43 |
lemma fset_eqvt[eqvt]: |
|
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
|
44 |
shows "p \<bullet> (fset S) = fset (p \<bullet> S)" |
|
1534
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
45 |
by (lifting set_eqvt) |
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
46 |
|
|
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
|
47 |
lemma supp_fset: |
|
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
|
48 |
shows "supp (fset S) = supp S" |
|
2340
b1549d391ea7
removed an "eqvt"-warning
Christian Urban <urbanc@in.tum.de>
parents:
2302
diff
changeset
|
49 |
unfolding supp_def |
|
b1549d391ea7
removed an "eqvt"-warning
Christian Urban <urbanc@in.tum.de>
parents:
2302
diff
changeset
|
50 |
by (perm_simp) (simp add: 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
|
51 |
|
| 2447 | 52 |
lemma supp_fempty: |
53 |
shows "supp {||} = {}"
|
|
54 |
unfolding supp_def |
|
55 |
by simp |
|
56 |
||
|
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
|
57 |
lemma supp_finsert: |
|
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
|
58 |
fixes x::"'a::fs" |
|
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
|
59 |
and S::"'a fset" |
|
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
|
60 |
shows "supp (finsert x S) = supp x \<union> supp S" |
|
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
|
61 |
apply(subst supp_fset[symmetric]) |
|
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
|
62 |
apply(simp add: supp_fset) |
|
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
|
63 |
apply(simp add: supp_of_fin_insert) |
|
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
|
64 |
apply(simp add: supp_fset) |
|
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
|
65 |
done |
|
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
|
66 |
|
|
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
|
67 |
|
|
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
|
68 |
instance fset :: (fs) fs |
|
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
|
69 |
apply (default) |
|
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
|
70 |
apply (induct_tac x rule: fset_induct) |
|
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
|
71 |
apply (simp add: supp_fempty) |
|
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
|
72 |
apply (simp add: supp_finsert) |
|
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
|
73 |
apply (simp add: finite_supp) |
|
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
|
74 |
done |
|
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
|
75 |
|
|
1534
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
76 |
lemma atom_fmap_cong: |
|
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
|
77 |
shows "fmap atom x = fmap atom y \<longleftrightarrow> x = y" |
|
1534
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
78 |
apply(rule inj_fmap_eq_iff) |
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
79 |
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
|
80 |
done |
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
81 |
|
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
82 |
lemma supp_fmap_atom: |
|
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
|
83 |
shows "supp (fmap atom S) = supp S" |
|
1818
37480540c1af
made everything to compile
Christian Urban <urbanc@in.tum.de>
parents:
1815
diff
changeset
|
84 |
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
|
85 |
apply(perm_simp) |
|
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
|
86 |
apply(simp add: atom_fmap_cong) |
|
1568
2311a9fc4624
Strong induction for Type Schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1542
diff
changeset
|
87 |
done |
|
2311a9fc4624
Strong induction for Type Schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1542
diff
changeset
|
88 |
|
|
2311a9fc4624
Strong induction for Type Schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1542
diff
changeset
|
89 |
lemma supp_at_fset: |
|
1973
fc5ce7f22b74
use the more general type-class at_base
Christian Urban <urbanc@in.tum.de>
parents:
1933
diff
changeset
|
90 |
fixes S::"('a::at_base) fset"
|
|
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
|
91 |
shows "supp S = fset (fmap atom S)" |
|
1973
fc5ce7f22b74
use the more general type-class at_base
Christian Urban <urbanc@in.tum.de>
parents:
1933
diff
changeset
|
92 |
apply (induct S) |
|
1568
2311a9fc4624
Strong induction for Type Schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1542
diff
changeset
|
93 |
apply (simp add: supp_fempty) |
|
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
|
94 |
apply (simp add: supp_finsert) |
|
1542
63e327e95abd
Showed the instance: fset::(at) fs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1534
diff
changeset
|
95 |
apply (simp add: supp_at_base) |
|
63e327e95abd
Showed the instance: fset::(at) fs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1534
diff
changeset
|
96 |
done |
|
1534
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
97 |
|
|
2178
e559513143e9
reversing the direction of fresh_star
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2004
diff
changeset
|
98 |
lemma fresh_star_atom: |
| 2447 | 99 |
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
|
100 |
shows "fset S \<sharp>* a \<Longrightarrow> atom a \<sharp> fset S" |
| 2447 | 101 |
apply (induct S) |
|
2178
e559513143e9
reversing the direction of fresh_star
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2004
diff
changeset
|
102 |
apply (simp add: fresh_set_empty) |
|
e559513143e9
reversing the direction of fresh_star
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2004
diff
changeset
|
103 |
apply simp |
|
e559513143e9
reversing the direction of fresh_star
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2004
diff
changeset
|
104 |
apply (unfold fresh_def) |
|
2466
47c840599a6b
cleaned a bit various thy-files in Nominal-General
Christian Urban <urbanc@in.tum.de>
parents:
2447
diff
changeset
|
105 |
apply (simp add: supp_of_fin_insert) |
|
2178
e559513143e9
reversing the direction of fresh_star
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2004
diff
changeset
|
106 |
apply (rule conjI) |
|
e559513143e9
reversing the direction of fresh_star
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2004
diff
changeset
|
107 |
apply (unfold fresh_star_def) |
|
e559513143e9
reversing the direction of fresh_star
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2004
diff
changeset
|
108 |
apply simp |
|
e559513143e9
reversing the direction of fresh_star
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2004
diff
changeset
|
109 |
apply (unfold fresh_def) |
|
e559513143e9
reversing the direction of fresh_star
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2004
diff
changeset
|
110 |
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
|
111 |
apply clarify |
|
e559513143e9
reversing the direction of fresh_star
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2004
diff
changeset
|
112 |
apply auto |
|
e559513143e9
reversing the direction of fresh_star
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2004
diff
changeset
|
113 |
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
|
114 |
|
|
1534
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
115 |
end |