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
|
1806
|
2 |
imports "../Nominal-General/Nominal2_Supp"
|
|
3 |
FSet
|
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 |
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
6 |
lemma permute_rsp_fset[quot_respect]:
|
1682
|
7 |
"(op = ===> list_eq ===> list_eq) permute permute"
|
1534
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
8 |
apply (simp add: eqvts[symmetric])
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
9 |
apply clarify
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
10 |
apply (subst permute_minus_cancel(1)[symmetric, of "xb"])
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
11 |
apply (subst mem_eqvt[symmetric])
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
12 |
apply (subst (2) permute_minus_cancel(1)[symmetric, of "xb"])
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
13 |
apply (subst mem_eqvt[symmetric])
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
14 |
apply (erule_tac x="- x \<bullet> xb" in allE)
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
15 |
apply simp
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
16 |
done
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
17 |
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
18 |
instantiation FSet.fset :: (pt) pt
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
19 |
begin
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
20 |
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
21 |
quotient_definition
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
22 |
"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
|
23 |
is
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
24 |
"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
|
25 |
|
1815
|
26 |
instance
|
|
27 |
proof
|
1782
|
28 |
fix x :: "'a fset" and p q :: "perm"
|
|
29 |
show "0 \<bullet> x = x"
|
|
30 |
by (lifting permute_zero [where 'a="'a list"])
|
|
31 |
show "(p + q) \<bullet> x = p \<bullet> q \<bullet> x"
|
|
32 |
by (lifting permute_plus [where 'a="'a list"])
|
|
33 |
qed
|
1534
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
34 |
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
35 |
end
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
36 |
|
1675
|
37 |
lemma permute_fset[eqvt]:
|
1815
|
38 |
"(p \<bullet> {||}) = ({||} :: 'a::pt fset)"
|
1534
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
39 |
"p \<bullet> finsert (x :: 'a :: pt) xs = finsert (p \<bullet> x) (p \<bullet> xs)"
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
40 |
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
|
41 |
|
1815
|
42 |
lemma fmap_eqvt[eqvt]:
|
1818
|
43 |
shows "p \<bullet> (fmap f l) = fmap (p \<bullet> f) (p \<bullet> l)"
|
1534
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
44 |
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
|
45 |
|
1818
|
46 |
lemma fset_to_set_eqvt[eqvt]:
|
|
47 |
shows "p \<bullet> (fset_to_set x) = fset_to_set (p \<bullet> x)"
|
1534
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
48 |
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
|
49 |
|
1542
|
50 |
lemma fin_fset_to_set:
|
1818
|
51 |
shows "finite (fset_to_set x)"
|
1542
|
52 |
by (induct x) (simp_all)
|
|
53 |
|
1534
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
54 |
lemma supp_fset_to_set:
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
55 |
"supp (fset_to_set x) = supp x"
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
56 |
apply (simp add: supp_def)
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
57 |
apply (simp add: eqvts)
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
58 |
apply (simp add: fset_cong)
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
59 |
done
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
60 |
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
61 |
lemma atom_fmap_cong:
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
62 |
shows "(fmap atom x = fmap atom y) = (x = y)"
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
63 |
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
|
64 |
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
|
65 |
done
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
66 |
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
67 |
lemma supp_fmap_atom:
|
1818
|
68 |
shows "supp (fmap atom x) = supp x"
|
|
69 |
unfolding supp_def
|
|
70 |
apply (perm_simp)
|
|
71 |
apply (simp add: atom_fmap_cong)
|
1534
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
72 |
done
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
73 |
|
1542
|
74 |
lemma supp_atom_finsert:
|
|
75 |
"supp (finsert (x :: atom) S) = supp x \<union> supp S"
|
1534
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
76 |
apply (subst supp_fset_to_set[symmetric])
|
1542
|
77 |
apply (simp add: supp_finite_atom_set)
|
|
78 |
apply (simp add: supp_atom_insert[OF fin_fset_to_set])
|
|
79 |
apply (simp add: supp_fset_to_set)
|
|
80 |
done
|
1534
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
81 |
|
1542
|
82 |
lemma supp_at_finsert:
|
1973
|
83 |
fixes a::"'a::at_base"
|
|
84 |
shows "supp (finsert a S) = supp a \<union> supp S"
|
1542
|
85 |
apply (subst supp_fset_to_set[symmetric])
|
|
86 |
apply (simp add: supp_finite_atom_set)
|
1973
|
87 |
apply (simp add: supp_at_base_insert[OF fin_fset_to_set])
|
1542
|
88 |
apply (simp add: supp_fset_to_set)
|
|
89 |
done
|
|
90 |
|
1568
|
91 |
lemma supp_fempty:
|
|
92 |
"supp {||} = {}"
|
|
93 |
by (simp add: supp_def eqvts)
|
|
94 |
|
1973
|
95 |
instance fset :: (at_base) fs
|
1534
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
96 |
apply (default)
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
97 |
apply (induct_tac x rule: fset_induct)
|
1568
|
98 |
apply (simp add: supp_fempty)
|
|
99 |
apply (simp add: supp_at_finsert)
|
|
100 |
apply (simp add: supp_at_base)
|
|
101 |
done
|
|
102 |
|
|
103 |
lemma supp_at_fset:
|
1973
|
104 |
fixes S::"('a::at_base) fset"
|
|
105 |
shows "supp S = fset_to_set (fmap atom S)"
|
|
106 |
apply (induct S)
|
1568
|
107 |
apply (simp add: supp_fempty)
|
1542
|
108 |
apply (simp add: supp_at_finsert)
|
|
109 |
apply (simp add: supp_at_base)
|
|
110 |
done
|
1534
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
111 |
|
984ea1299cd7
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
112 |
end
|