1795
|
1 |
theory TypeSchemes
|
2454
|
2 |
imports "../Nominal2"
|
1795
|
3 |
begin
|
|
4 |
|
|
5 |
section {*** Type Schemes ***}
|
|
6 |
|
2709
|
7 |
|
2556
8ed62410236e
added a test about subtyping; disabled two tests, because of problem with function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
8 |
atom_decl name
|
8ed62410236e
added a test about subtyping; disabled two tests, because of problem with function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
9 |
|
2486
|
10 |
(* defined as a single nominal datatype *)
|
1795
|
11 |
|
|
12 |
nominal_datatype ty =
|
|
13 |
Var "name"
|
|
14 |
| Fun "ty" "ty"
|
|
15 |
and tys =
|
2714
|
16 |
All xs::"name fset" ty::"ty" bind (set+) xs in ty
|
2434
|
17 |
|
2468
|
18 |
thm ty_tys.distinct
|
|
19 |
thm ty_tys.induct
|
2617
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
20 |
thm ty_tys.inducts
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
21 |
thm ty_tys.exhaust ty_tys.strong_exhaust
|
2468
|
22 |
thm ty_tys.fv_defs
|
|
23 |
thm ty_tys.bn_defs
|
|
24 |
thm ty_tys.perm_simps
|
|
25 |
thm ty_tys.eq_iff
|
|
26 |
thm ty_tys.fv_bn_eqvt
|
|
27 |
thm ty_tys.size_eqvt
|
|
28 |
thm ty_tys.supports
|
2493
|
29 |
thm ty_tys.supp
|
2494
|
30 |
thm ty_tys.fresh
|
1795
|
31 |
|
2707
|
32 |
fun
|
|
33 |
lookup :: "(name \<times> ty) list \<Rightarrow> name \<Rightarrow> ty"
|
|
34 |
where
|
|
35 |
"lookup [] Y = Var Y"
|
|
36 |
| "lookup ((X, T) # Ts) Y = (if X = Y then T else lookup Ts Y)"
|
|
37 |
|
|
38 |
lemma lookup_eqvt[eqvt]:
|
|
39 |
shows "(p \<bullet> lookup Ts T) = lookup (p \<bullet> Ts) (p \<bullet> T)"
|
|
40 |
apply(induct Ts T rule: lookup.induct)
|
|
41 |
apply(simp_all)
|
|
42 |
done
|
|
43 |
|
2709
|
44 |
lemma test:
|
|
45 |
assumes a: "f x = Inl y"
|
|
46 |
shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl ((p \<bullet> f) (p \<bullet> x))"
|
|
47 |
using a
|
|
48 |
apply(frule_tac p="p" in permute_boolI)
|
|
49 |
apply(simp (no_asm_use) only: eqvts)
|
|
50 |
apply(subst (asm) permute_fun_app_eq)
|
|
51 |
back
|
|
52 |
apply(simp)
|
|
53 |
done
|
|
54 |
|
2710
|
55 |
lemma test2:
|
|
56 |
assumes a: "f x = Inl y"
|
|
57 |
shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl (p \<bullet> (f x))"
|
|
58 |
using a
|
|
59 |
apply(frule_tac p="p" in permute_boolI)
|
|
60 |
apply(simp (no_asm_use) only: eqvts)
|
|
61 |
apply(subst (asm) permute_fun_app_eq)
|
|
62 |
back
|
2709
|
63 |
apply(simp)
|
2710
|
64 |
done
|
2709
|
65 |
|
2727
|
66 |
lemma helper:
|
|
67 |
assumes "A - C = A - D"
|
|
68 |
and "B - C = B - D"
|
|
69 |
and "E \<subseteq> A \<union> B"
|
|
70 |
shows "E - C = E - D"
|
|
71 |
using assms
|
|
72 |
by blast
|
|
73 |
|
2707
|
74 |
nominal_primrec
|
|
75 |
subst :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty"
|
|
76 |
and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys"
|
|
77 |
where
|
|
78 |
"subst \<theta> (Var X) = lookup \<theta> X"
|
|
79 |
| "subst \<theta> (Fun T1 T2) = Fun (subst \<theta> T1) (subst \<theta> T2)"
|
|
80 |
| "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs T) = All xs (subst \<theta> T)"
|
2709
|
81 |
|
2707
|
82 |
term subst_substs_sumC
|
2709
|
83 |
thm subst_substs_sumC_def
|
2707
|
84 |
term Inl
|
|
85 |
thm subst_substs_graph.induct
|
|
86 |
thm subst_substs_graph.intros
|
|
87 |
thm Projl.simps
|
|
88 |
apply(subgoal_tac "\<And>p x r. subst_substs_graph x r \<Longrightarrow> subst_substs_graph (p \<bullet> x) (p \<bullet> r)")
|
|
89 |
apply(simp add: eqvt_def)
|
|
90 |
apply(rule allI)
|
|
91 |
apply(simp add: permute_fun_def permute_bool_def)
|
|
92 |
apply(rule ext)
|
|
93 |
apply(rule ext)
|
|
94 |
apply(rule iffI)
|
|
95 |
apply(drule_tac x="p" in meta_spec)
|
|
96 |
apply(drule_tac x="- p \<bullet> x" in meta_spec)
|
|
97 |
apply(drule_tac x="- p \<bullet> xa" in meta_spec)
|
|
98 |
apply(simp)
|
|
99 |
apply(drule_tac x="-p" in meta_spec)
|
|
100 |
apply(drule_tac x="x" in meta_spec)
|
|
101 |
apply(drule_tac x="xa" in meta_spec)
|
|
102 |
apply(simp)
|
2710
|
103 |
--"Eqvt One way"
|
2707
|
104 |
thm subst_substs_graph.induct
|
|
105 |
thm subst_substs_graph.intros
|
|
106 |
thm Projl.simps
|
|
107 |
apply(erule subst_substs_graph.induct)
|
|
108 |
apply(perm_simp)
|
|
109 |
apply(rule subst_substs_graph.intros)
|
2709
|
110 |
thm subst_substs_graph.cases
|
|
111 |
apply(erule subst_substs_graph.cases)
|
|
112 |
apply(simp (no_asm_use) only: eqvts)
|
|
113 |
apply(subst test)
|
|
114 |
back
|
|
115 |
apply(assumption)
|
|
116 |
apply(rotate_tac 1)
|
|
117 |
apply(erule subst_substs_graph.cases)
|
|
118 |
apply(subst test)
|
|
119 |
back
|
|
120 |
apply(assumption)
|
|
121 |
apply(perm_simp)
|
|
122 |
apply(rule subst_substs_graph.intros)
|
|
123 |
apply(assumption)
|
|
124 |
apply(assumption)
|
|
125 |
apply(subst test)
|
|
126 |
back
|
|
127 |
apply(assumption)
|
|
128 |
apply(perm_simp)
|
|
129 |
apply(rule subst_substs_graph.intros)
|
|
130 |
apply(assumption)
|
|
131 |
apply(assumption)
|
|
132 |
apply(simp)
|
|
133 |
--"A"
|
|
134 |
apply(simp (no_asm_use) only: eqvts)
|
|
135 |
apply(subst test)
|
|
136 |
back
|
|
137 |
apply(assumption)
|
|
138 |
apply(rotate_tac 1)
|
|
139 |
apply(erule subst_substs_graph.cases)
|
|
140 |
apply(subst test)
|
|
141 |
back
|
|
142 |
apply(assumption)
|
|
143 |
apply(perm_simp)
|
|
144 |
apply(rule subst_substs_graph.intros)
|
|
145 |
apply(assumption)
|
|
146 |
apply(assumption)
|
|
147 |
apply(subst test)
|
|
148 |
back
|
|
149 |
apply(assumption)
|
|
150 |
apply(perm_simp)
|
|
151 |
apply(rule subst_substs_graph.intros)
|
|
152 |
apply(assumption)
|
|
153 |
apply(assumption)
|
|
154 |
apply(simp)
|
|
155 |
--"A"
|
|
156 |
apply(simp)
|
|
157 |
apply(erule subst_substs_graph.cases)
|
|
158 |
apply(simp (no_asm_use) only: eqvts)
|
|
159 |
apply(subst test)
|
|
160 |
back
|
|
161 |
back
|
|
162 |
apply(assumption)
|
|
163 |
apply(rule subst_substs_graph.intros)
|
2710
|
164 |
apply (simp add: eqvts)
|
|
165 |
apply (subgoal_tac "(p \<bullet> (atom ` fset xs)) \<sharp>* (p \<bullet> \<theta>)")
|
|
166 |
apply (simp add: image_eqvt eqvts_raw eqvts)
|
|
167 |
apply (simp add: fresh_star_permute_iff)
|
2709
|
168 |
apply(perm_simp)
|
|
169 |
apply(assumption)
|
|
170 |
apply(simp (no_asm_use) only: eqvts)
|
|
171 |
apply(subst test)
|
|
172 |
back
|
|
173 |
back
|
|
174 |
apply(assumption)
|
|
175 |
apply(rule subst_substs_graph.intros)
|
2710
|
176 |
apply (simp add: eqvts)
|
|
177 |
apply (subgoal_tac "(p \<bullet> (atom ` fset xs)) \<sharp>* (p \<bullet> \<theta>)")
|
|
178 |
apply (simp add: image_eqvt eqvts_raw eqvts)
|
|
179 |
apply (simp add: fresh_star_permute_iff)
|
2709
|
180 |
apply(perm_simp)
|
|
181 |
apply(assumption)
|
|
182 |
apply(simp)
|
2710
|
183 |
--"Eqvt done"
|
|
184 |
apply (case_tac x)
|
|
185 |
apply simp apply clarify
|
|
186 |
apply (rule_tac y="b" in ty_tys.exhaust(1))
|
2787
1a6593bc494d
added eq_iff and distinct lemmas of nominal datatypes to the simplifier
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
187 |
apply (auto)[1]
|
1a6593bc494d
added eq_iff and distinct lemmas of nominal datatypes to the simplifier
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
188 |
apply (auto)[1]
|
2710
|
189 |
apply simp apply clarify
|
|
190 |
apply (rule_tac ya="b" and c="a" in ty_tys.strong_exhaust(2))
|
2787
1a6593bc494d
added eq_iff and distinct lemmas of nominal datatypes to the simplifier
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
191 |
apply (auto)[1]
|
1a6593bc494d
added eq_iff and distinct lemmas of nominal datatypes to the simplifier
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
192 |
apply (auto)[5]
|
2710
|
193 |
--"LAST GOAL"
|
2787
1a6593bc494d
added eq_iff and distinct lemmas of nominal datatypes to the simplifier
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
194 |
apply(simp del: ty_tys.eq_iff)
|
2710
|
195 |
thm meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff]
|
|
196 |
apply (simp add: meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff])
|
|
197 |
apply (subgoal_tac "eqvt_at (\<lambda>(l, r). subst l r) (\<theta>', T)")
|
|
198 |
apply (thin_tac "eqvt_at subst_substs_sumC (Inl (\<theta>', T))")
|
2709
|
199 |
defer
|
2710
|
200 |
apply (simp add: eqvt_at_def subst_def)
|
|
201 |
apply rule
|
|
202 |
apply (subgoal_tac "\<And>x. subst_substs_sumC (Inl (x)) = Inl (?y x)")
|
|
203 |
apply (subst test2)
|
|
204 |
apply (drule_tac x="(\<theta>', T)" in meta_spec)
|
|
205 |
apply assumption
|
|
206 |
apply simp
|
|
207 |
--"We require that for Inl it returns Inl. It doesn't work for undefined, but it does work for the following"
|
|
208 |
apply (subgoal_tac "\<And>y. \<exists>z. (\<lambda>x. THE_default (sum_case (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined) x) (subst_substs_graph x)) (Inl y) = (Inl z)")
|
|
209 |
prefer 2
|
|
210 |
apply (simp add: THE_default_def)
|
|
211 |
apply (case_tac "Ex1 (subst_substs_graph (Inl y))")
|
|
212 |
prefer 2
|
|
213 |
apply simp
|
|
214 |
apply (simp add: the1_equality)
|
|
215 |
apply auto[1]
|
|
216 |
apply (erule_tac x="x" in allE)
|
|
217 |
apply simp
|
|
218 |
apply(cases rule: subst_substs_graph.cases)
|
|
219 |
apply assumption
|
|
220 |
apply (rule_tac x="lookup \<theta> X" in exI)
|
|
221 |
apply clarify
|
|
222 |
apply (rule the1_equality)
|
|
223 |
apply metis apply assumption
|
|
224 |
apply (rule_tac x="(Fun (Sum_Type.Projl (subst_substs_sum (Inl (\<theta>, T1))))
|
|
225 |
(Sum_Type.Projl (subst_substs_sum (Inl (\<theta>, T2)))))" in exI)
|
|
226 |
apply clarify
|
|
227 |
apply (rule the1_equality)
|
|
228 |
apply metis apply assumption
|
|
229 |
apply clarify
|
|
230 |
--"This is exactly the assumption for the properly defined function"
|
|
231 |
defer
|
2714
|
232 |
apply (simp only: Abs_eq_res_set)
|
2727
|
233 |
apply (subgoal_tac "(atom ` fset xsa \<inter> supp Ta - atom ` fset xs \<inter> supp T) \<sharp>* ([atom ` fset xs \<inter> supp (subst \<theta>' T)]set. T)")
|
2710
|
234 |
apply (subst (asm) Abs_eq_iff2)
|
2714
|
235 |
apply (clarify)
|
2711
ec1a7ef740b8
Showing that the binders difference is fresh for the left side solves the goal for 'set'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
236 |
apply (simp add: alphas)
|
2710
|
237 |
apply (clarify)
|
|
238 |
apply (rule trans)
|
|
239 |
apply(rule_tac p="p" in supp_perm_eq[symmetric])
|
|
240 |
apply(rule fresh_star_supp_conv)
|
|
241 |
thm fresh_star_perm_set_conv
|
|
242 |
apply(drule fresh_star_perm_set_conv)
|
|
243 |
apply (rule finite_Diff)
|
|
244 |
apply (rule finite_supp)
|
2714
|
245 |
apply (subgoal_tac "(atom ` fset xs \<inter> supp T \<union> atom ` fset xsa \<inter> supp (p \<bullet> T)) \<sharp>* ([atom ` fset xs \<inter> supp (subst \<theta>' T)]set. subst \<theta>' T)")
|
2710
|
246 |
apply (metis Un_absorb2 fresh_star_Un)
|
|
247 |
apply (simp add: fresh_star_Un)
|
|
248 |
apply (rule conjI)
|
2714
|
249 |
apply (simp (no_asm) add: fresh_star_def)
|
|
250 |
|
2711
ec1a7ef740b8
Showing that the binders difference is fresh for the left side solves the goal for 'set'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
251 |
apply rule
|
ec1a7ef740b8
Showing that the binders difference is fresh for the left side solves the goal for 'set'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
252 |
apply(simp (no_asm) only: Abs_fresh_iff)
|
ec1a7ef740b8
Showing that the binders difference is fresh for the left side solves the goal for 'set'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
253 |
apply(clarify)
|
2714
|
254 |
apply auto[1]
|
|
255 |
apply (simp add: fresh_star_def fresh_def)
|
2728
|
256 |
|
2714
|
257 |
apply (simp (no_asm) add: fresh_star_def)
|
|
258 |
apply rule
|
|
259 |
apply auto[1]
|
|
260 |
apply(simp (no_asm) only: Abs_fresh_iff)
|
|
261 |
apply(clarify)
|
|
262 |
apply auto[1]
|
|
263 |
apply(drule_tac a="atom x" in fresh_eqvt_at)
|
2711
ec1a7ef740b8
Showing that the binders difference is fresh for the left side solves the goal for 'set'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
264 |
apply (simp add: supp_Pair finite_supp)
|
ec1a7ef740b8
Showing that the binders difference is fresh for the left side solves the goal for 'set'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
265 |
apply (simp add: fresh_Pair)
|
2728
|
266 |
apply(auto simp add: Abs_fresh_iff fresh_star_def)[2]
|
|
267 |
apply (simp add: fresh_def)
|
2710
|
268 |
apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'")
|
|
269 |
prefer 2
|
|
270 |
apply (rule perm_supp_eq)
|
2714
|
271 |
apply (subgoal_tac "(atom ` fset xs \<inter> supp T \<union> atom ` fset xsa \<inter> supp (p \<bullet> T)) \<sharp>* \<theta>'")
|
|
272 |
apply (auto simp add: fresh_star_def)[1]
|
|
273 |
apply (simp add: fresh_star_Un fresh_star_def)
|
|
274 |
apply blast
|
|
275 |
apply(simp add: eqvt_at_def inter_eqvt supp_eqvt)
|
|
276 |
apply (simp only: Abs_eq_res_set[symmetric])
|
2727
|
277 |
apply (simp add: Abs_eq_iff alphas)
|
|
278 |
apply rule
|
|
279 |
prefer 2
|
|
280 |
apply (rule_tac x="0 :: perm" in exI)
|
|
281 |
apply (simp add: fresh_star_zero)
|
|
282 |
apply (rule helper)
|
|
283 |
prefer 3
|
|
284 |
apply (subgoal_tac "supp ((\<lambda>(l, r). subst l r) (\<theta>', (p \<bullet> T))) \<subseteq> supp \<theta>' \<union> supp (p \<bullet> T)")
|
|
285 |
apply simp
|
|
286 |
apply (subst supp_Pair[symmetric])
|
|
287 |
apply (rule supp_eqvt_at)
|
|
288 |
apply (simp add: eqvt_at_def)
|
2728
|
289 |
apply (thin_tac " p \<bullet> atom ` fset xs \<inter> supp (p \<bullet> T) = atom ` fset xsa \<inter> supp (p \<bullet> T)")
|
|
290 |
apply (thin_tac "supp T - atom ` fset xs \<inter> supp T = supp (p \<bullet> T) - atom ` fset xsa \<inter> supp (p \<bullet> T)")
|
|
291 |
apply (thin_tac "supp p \<subseteq> atom ` fset xs \<inter> supp T \<union> atom ` fset xsa \<inter> supp (p \<bullet> T)")
|
|
292 |
apply (thin_tac "(atom ` fset xsa \<inter> supp (p \<bullet> T) - atom ` fset xs \<inter> supp T) \<sharp>* ([atom ` fset xs \<inter> supp (subst \<theta>' T)]set. T)")
|
|
293 |
apply (thin_tac "atom ` fset xs \<sharp>* \<theta>'")
|
|
294 |
apply (thin_tac "atom ` fset xsa \<sharp>* \<theta>'")
|
|
295 |
apply (thin_tac "(supp (p \<bullet> T) - atom ` fset xsa \<inter> supp (p \<bullet> T)) \<sharp>* p")
|
|
296 |
apply (rule)
|
|
297 |
apply (subgoal_tac "\<forall>p. p \<bullet> subst \<theta>' T = subst (p \<bullet> \<theta>') (p \<bullet> T)")
|
|
298 |
apply (erule_tac x="p" in allE)
|
|
299 |
apply (erule_tac x="pa + p" in allE)
|
|
300 |
apply (metis permute_plus)
|
|
301 |
apply assumption
|
2727
|
302 |
apply (simp add: supp_Pair finite_supp)
|
|
303 |
prefer 2 apply blast
|
|
304 |
prefer 2 apply (metis finite_UNIV finite_imageI obtain_at_base rangeI)
|
2728
|
305 |
apply (rule_tac s="supp \<theta>'" in trans)
|
|
306 |
apply (subgoal_tac "(p \<bullet> atom ` fset xs) \<sharp>* \<theta>'")
|
|
307 |
apply (auto simp add: fresh_star_def fresh_def)[1]
|
|
308 |
apply (subgoal_tac "supp p \<sharp>* \<theta>'")
|
|
309 |
apply (metis fresh_star_permute_iff)
|
|
310 |
apply (subgoal_tac "(atom ` fset xs \<union> atom ` fset xsa) \<sharp>* \<theta>'")
|
|
311 |
apply (auto simp add: fresh_star_def)[1]
|
|
312 |
apply (simp add: fresh_star_Un)
|
|
313 |
apply (auto simp add: fresh_star_def fresh_def)[1]
|
2707
|
314 |
oops
|
|
315 |
|
2676
|
316 |
section {* defined as two separate nominal datatypes *}
|
2486
|
317 |
|
2308
|
318 |
nominal_datatype ty2 =
|
|
319 |
Var2 "name"
|
|
320 |
| Fun2 "ty2" "ty2"
|
|
321 |
|
|
322 |
nominal_datatype tys2 =
|
2634
3ce1089cdbf3
changed res keyword to set+ for restrictions; comment by a referee
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
323 |
All2 xs::"name fset" ty::"ty2" bind (set+) xs in ty
|
2337
|
324 |
|
2468
|
325 |
thm tys2.distinct
|
2630
|
326 |
thm tys2.induct tys2.strong_induct
|
2617
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
327 |
thm tys2.exhaust tys2.strong_exhaust
|
2468
|
328 |
thm tys2.fv_defs
|
|
329 |
thm tys2.bn_defs
|
|
330 |
thm tys2.perm_simps
|
|
331 |
thm tys2.eq_iff
|
|
332 |
thm tys2.fv_bn_eqvt
|
|
333 |
thm tys2.size_eqvt
|
|
334 |
thm tys2.supports
|
2493
|
335 |
thm tys2.supp
|
2494
|
336 |
thm tys2.fresh
|
2468
|
337 |
|
2676
|
338 |
fun
|
2707
|
339 |
lookup2 :: "(name \<times> ty2) list \<Rightarrow> name \<Rightarrow> ty2"
|
2676
|
340 |
where
|
2707
|
341 |
"lookup2 [] Y = Var2 Y"
|
|
342 |
| "lookup2 ((X, T) # Ts) Y = (if X = Y then T else lookup2 Ts Y)"
|
2556
8ed62410236e
added a test about subtyping; disabled two tests, because of problem with function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
343 |
|
2707
|
344 |
lemma lookup2_eqvt[eqvt]:
|
|
345 |
shows "(p \<bullet> lookup2 Ts T) = lookup2 (p \<bullet> Ts) (p \<bullet> T)"
|
|
346 |
apply(induct Ts T rule: lookup2.induct)
|
2676
|
347 |
apply(simp_all)
|
|
348 |
done
|
|
349 |
|
2707
|
350 |
nominal_primrec
|
2676
|
351 |
subst :: "(name \<times> ty2) list \<Rightarrow> ty2 \<Rightarrow> ty2"
|
|
352 |
where
|
2707
|
353 |
"subst \<theta> (Var2 X) = lookup2 \<theta> X"
|
2676
|
354 |
| "subst \<theta> (Fun2 T1 T2) = Fun2 (subst \<theta> T1) (subst \<theta> T2)"
|
2707
|
355 |
defer
|
2676
|
356 |
apply(case_tac x)
|
|
357 |
apply(simp)
|
|
358 |
apply(rule_tac y="b" in ty2.exhaust)
|
|
359 |
apply(blast)
|
|
360 |
apply(blast)
|
|
361 |
apply(simp_all add: ty2.distinct)
|
2707
|
362 |
apply(subgoal_tac "\<And>p x r. subst_graph x r \<Longrightarrow> subst_graph (p \<bullet> x) (p \<bullet> r)")
|
|
363 |
apply(simp add: eqvt_def)
|
|
364 |
apply(rule allI)
|
|
365 |
apply(simp add: permute_fun_def permute_bool_def)
|
|
366 |
apply(rule ext)
|
|
367 |
apply(rule ext)
|
|
368 |
apply(rule iffI)
|
|
369 |
apply(drule_tac x="p" in meta_spec)
|
|
370 |
apply(drule_tac x="- p \<bullet> x" in meta_spec)
|
|
371 |
apply(drule_tac x="- p \<bullet> xa" in meta_spec)
|
|
372 |
apply(simp)
|
|
373 |
apply(drule_tac x="-p" in meta_spec)
|
|
374 |
apply(drule_tac x="x" in meta_spec)
|
|
375 |
apply(drule_tac x="xa" in meta_spec)
|
|
376 |
apply(simp)
|
|
377 |
apply(erule subst_graph.induct)
|
|
378 |
apply(perm_simp)
|
|
379 |
apply(rule subst_graph.intros)
|
|
380 |
apply(perm_simp)
|
|
381 |
apply(rule subst_graph.intros)
|
|
382 |
apply(assumption)
|
|
383 |
apply(assumption)
|
2676
|
384 |
done
|
|
385 |
|
|
386 |
termination
|
|
387 |
apply(relation "measure (size o snd)")
|
|
388 |
apply(simp_all add: ty2.size)
|
|
389 |
done
|
|
390 |
|
|
391 |
lemma subst_eqvt[eqvt]:
|
|
392 |
shows "(p \<bullet> subst \<theta> T) = subst (p \<bullet> \<theta>) (p \<bullet> T)"
|
|
393 |
apply(induct \<theta> T rule: subst.induct)
|
2707
|
394 |
apply(simp_all add: lookup2_eqvt)
|
2676
|
395 |
done
|
|
396 |
|
|
397 |
lemma j:
|
|
398 |
assumes "a \<sharp> Ts" " a \<sharp> X"
|
2707
|
399 |
shows "a \<sharp> lookup2 Ts X"
|
2676
|
400 |
using assms
|
2707
|
401 |
apply(induct Ts X rule: lookup2.induct)
|
2676
|
402 |
apply(auto simp add: ty2.fresh fresh_Cons fresh_Pair)
|
|
403 |
done
|
|
404 |
|
|
405 |
lemma i:
|
|
406 |
assumes "a \<sharp> t" " a \<sharp> \<theta>"
|
|
407 |
shows "a \<sharp> subst \<theta> t"
|
|
408 |
using assms
|
|
409 |
apply(induct \<theta> t rule: subst.induct)
|
|
410 |
apply(auto simp add: ty2.fresh j)
|
|
411 |
done
|
|
412 |
|
|
413 |
lemma k:
|
|
414 |
assumes "as \<sharp>* t" " as \<sharp>* \<theta>"
|
|
415 |
shows "as \<sharp>* subst \<theta> t"
|
|
416 |
using assms
|
|
417 |
by (simp add: fresh_star_def i)
|
|
418 |
|
|
419 |
lemma h:
|
|
420 |
assumes "as \<subseteq> bs \<union> cs"
|
|
421 |
and " cs \<sharp>* x"
|
|
422 |
shows "(as - bs) \<sharp>* x"
|
|
423 |
using assms
|
|
424 |
by (auto simp add: fresh_star_def)
|
|
425 |
|
|
426 |
nominal_primrec
|
|
427 |
substs :: "(name \<times> ty2) list \<Rightarrow> tys2 \<Rightarrow> tys2"
|
|
428 |
where
|
|
429 |
"fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All2 xs t) = All2 xs (subst \<theta> t)"
|
|
430 |
oops
|
|
431 |
|
|
432 |
|
|
433 |
text {* Some Tests about Alpha-Equality *}
|
1795
|
434 |
|
|
435 |
lemma
|
|
436 |
shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))"
|
2676
|
437 |
apply(simp add: ty_tys.eq_iff Abs_eq_iff)
|
1795
|
438 |
apply(rule_tac x="0::perm" in exI)
|
2676
|
439 |
apply(simp add: alphas fresh_star_def ty_tys.supp supp_at_base)
|
1795
|
440 |
done
|
|
441 |
|
|
442 |
lemma
|
|
443 |
shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var b) (Var a))"
|
2566
a59d8e1e3a17
moved rest of the lemmas from Nominal2_FSet to the TypeScheme example
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
444 |
apply(simp add: ty_tys.eq_iff Abs_eq_iff)
|
1795
|
445 |
apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
|
2566
a59d8e1e3a17
moved rest of the lemmas from Nominal2_FSet to the TypeScheme example
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
446 |
apply(simp add: alphas fresh_star_def supp_at_base ty_tys.supp)
|
1795
|
447 |
done
|
|
448 |
|
|
449 |
lemma
|
|
450 |
shows "All {|a, b, c|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var a) (Var b))"
|
2566
a59d8e1e3a17
moved rest of the lemmas from Nominal2_FSet to the TypeScheme example
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
451 |
apply(simp add: ty_tys.eq_iff Abs_eq_iff)
|
1795
|
452 |
apply(rule_tac x="0::perm" in exI)
|
2566
a59d8e1e3a17
moved rest of the lemmas from Nominal2_FSet to the TypeScheme example
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
453 |
apply(simp add: alphas fresh_star_def ty_tys.supp supp_at_base)
|
1795
|
454 |
done
|
|
455 |
|
|
456 |
lemma
|
|
457 |
assumes a: "a \<noteq> b"
|
|
458 |
shows "\<not>(All {|a, b|} (Fun (Var a) (Var b)) = All {|c|} (Fun (Var c) (Var c)))"
|
|
459 |
using a
|
2566
a59d8e1e3a17
moved rest of the lemmas from Nominal2_FSet to the TypeScheme example
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
460 |
apply(simp add: ty_tys.eq_iff Abs_eq_iff)
|
1795
|
461 |
apply(clarify)
|
2566
a59d8e1e3a17
moved rest of the lemmas from Nominal2_FSet to the TypeScheme example
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
462 |
apply(simp add: alphas fresh_star_def ty_tys.eq_iff ty_tys.supp supp_at_base)
|
1795
|
463 |
apply auto
|
|
464 |
done
|
|
465 |
|
2566
a59d8e1e3a17
moved rest of the lemmas from Nominal2_FSet to the TypeScheme example
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
466 |
|
1795
|
467 |
|
|
468 |
|
|
469 |
end
|