73 |
74 |
74 definition "MYUNDEFINED \<equiv> undefined" |
75 definition "MYUNDEFINED \<equiv> undefined" |
75 |
76 |
76 --"The following is accepted by 'function' but not by 'nominal_primrec'" |
77 --"The following is accepted by 'function' but not by 'nominal_primrec'" |
77 |
78 |
78 function (default "\<lambda>(x :: (name \<times> ty) list \<times> ty + (name \<times> ty) list \<times> tys). sum_case (\<lambda>x. Inl (undefined :: ty)) (\<lambda>x. Inr (undefined :: tys)) x") |
79 function (default "sum_case (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)") |
79 subst :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty" |
80 subst :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty" |
80 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" |
81 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" |
81 where |
82 where |
82 "subst \<theta> (Var X) = lookup \<theta> X" |
83 "subst \<theta> (Var X) = lookup \<theta> X" |
83 | "subst \<theta> (Fun T1 T2) = Fun (subst \<theta> T1) (subst \<theta> T2)" |
84 | "subst \<theta> (Fun T1 T2) = Fun (subst \<theta> T1) (subst \<theta> T2)" |
84 | "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs T) = All xs (subst \<theta> T)" |
85 | "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs T) = All xs (subst \<theta> T)" |
|
86 thm subst_substs_graph_def |
|
87 thm subst_substs_sumC_def |
85 oops |
88 oops |
|
89 |
|
90 lemma Abs_res_fcb: |
|
91 fixes xs ys :: "('a :: at_base) set" |
|
92 and S T :: "'b :: fs" |
|
93 assumes e: "(Abs_res (atom ` xs) T) = (Abs_res (atom ` ys) S)" |
|
94 and f1: "\<And>x. x \<in> atom ` xs \<Longrightarrow> x \<in> supp T \<Longrightarrow> x \<sharp> f xs T" |
|
95 and f2: "\<And>x. supp T - atom ` xs = supp S - atom ` ys \<Longrightarrow> x \<in> atom ` ys \<Longrightarrow> x \<in> supp S \<Longrightarrow> x \<sharp> f xs T" |
|
96 and eqv: "\<And>p. p \<bullet> T = S \<Longrightarrow> supp p \<subseteq> atom ` xs \<inter> supp T \<union> atom ` ys \<inter> supp S |
|
97 \<Longrightarrow> p \<bullet> (atom ` xs \<inter> supp T) = atom ` ys \<inter> supp S \<Longrightarrow> p \<bullet> (f xs T) = f ys S" |
|
98 shows "f xs T = f ys S" |
|
99 using e apply - |
|
100 apply (subst (asm) Abs_eq_res_set) |
|
101 apply (subst (asm) Abs_eq_iff2) |
|
102 apply (simp add: alphas) |
|
103 apply (elim exE conjE) |
|
104 apply(rule trans) |
|
105 apply (rule_tac p="p" in supp_perm_eq[symmetric]) |
|
106 apply(rule fresh_star_supp_conv) |
|
107 apply(drule fresh_star_perm_set_conv) |
|
108 apply (rule finite_Diff) |
|
109 apply (rule finite_supp) |
|
110 apply (subgoal_tac "(atom ` xs \<inter> supp T \<union> atom ` ys \<inter> supp S) \<sharp>* f xs T") |
|
111 apply (metis Un_absorb2 fresh_star_Un) |
|
112 apply (subst fresh_star_Un) |
|
113 apply (rule conjI) |
|
114 apply (simp add: fresh_star_def f1) |
|
115 apply (subgoal_tac "supp T - atom ` xs = supp S - atom ` ys") |
|
116 apply (simp add: fresh_star_def f2) |
|
117 apply blast |
|
118 apply (simp add: eqv) |
|
119 done |
86 |
120 |
87 nominal_primrec (default "\<lambda>(x :: (name \<times> ty) list \<times> ty + (name \<times> ty) list \<times> tys). MYUNDEFINED :: ty + tys") |
121 nominal_primrec (default "\<lambda>(x :: (name \<times> ty) list \<times> ty + (name \<times> ty) list \<times> tys). MYUNDEFINED :: ty + tys") |
88 subst :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty" |
122 subst :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty" |
89 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" |
123 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" |
90 where |
124 where |
209 apply simp apply clarify |
239 apply simp apply clarify |
210 apply (rule_tac ya="b" and c="a" in ty_tys.strong_exhaust(2)) |
240 apply (rule_tac ya="b" and c="a" in ty_tys.strong_exhaust(2)) |
211 apply (auto)[1] |
241 apply (auto)[1] |
212 apply (auto)[5] |
242 apply (auto)[5] |
213 --"LAST GOAL" |
243 --"LAST GOAL" |
214 apply(simp del: ty_tys.eq_iff) |
|
215 apply (simp add: meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff]) |
244 apply (simp add: meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff]) |
216 apply (subgoal_tac "eqvt_at (\<lambda>(l, r). subst l r) (\<theta>', T)") |
245 apply (subgoal_tac "eqvt_at (\<lambda>(l, r). subst l r) (\<theta>', T)") |
217 apply (thin_tac "eqvt_at subst_substs_sumC (Inl (\<theta>', T))") |
246 apply (thin_tac "eqvt_at subst_substs_sumC (Inl (\<theta>', T))") |
218 defer |
247 prefer 2 |
219 apply (simp add: eqvt_at_def subst_def) |
248 apply (simp add: eqvt_at_def subst_def) |
220 apply rule |
249 apply rule |
221 apply (subgoal_tac "\<And>x. subst_substs_sumC (Inl (x)) = Inl (?y x)") |
250 apply (subgoal_tac "\<And>x. subst_substs_sumC (Inl (x)) = Inl (?y x)") |
222 apply (subst test2) |
251 apply (subst test2) |
223 apply (drule_tac x="(\<theta>', T)" in meta_spec) |
252 apply (drule_tac x="(\<theta>', T)" in meta_spec) |
246 apply (rule the1_equality) |
275 apply (rule the1_equality) |
247 apply metis apply assumption |
276 apply metis apply assumption |
248 apply clarify |
277 apply clarify |
249 --"This is exactly the assumption for the properly defined function" |
278 --"This is exactly the assumption for the properly defined function" |
250 defer |
279 defer |
251 apply (simp only: Abs_eq_res_set) |
280 apply clarify |
252 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)") |
281 apply (frule supp_eqvt_at) |
253 apply (subst (asm) Abs_eq_iff2) |
282 apply (simp add: finite_supp) |
254 apply (clarify) |
283 apply (erule Abs_res_fcb) |
255 apply (simp add: alphas) |
284 apply (simp add: Abs_fresh_iff) |
256 apply (clarify) |
285 apply (simp add: Abs_fresh_iff) |
257 apply (rule trans) |
286 apply auto[1] |
258 apply(rule_tac p="p" in supp_perm_eq[symmetric]) |
287 apply (simp add: fresh_def fresh_star_def) |
259 apply(rule fresh_star_supp_conv) |
288 apply (erule contra_subsetD) |
260 thm fresh_star_perm_set_conv |
289 apply (simp add: supp_Pair) |
261 apply(drule fresh_star_perm_set_conv) |
290 apply blast |
262 apply (rule finite_Diff) |
291 apply clarify |
263 apply (rule finite_supp) |
292 apply (simp) |
264 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)") |
293 apply (simp add: eqvt_at_def) |
265 apply (metis Un_absorb2 fresh_star_Un) |
294 apply (subst Abs_eq_iff) |
266 apply (simp add: fresh_star_Un) |
295 apply (rule_tac x="0::perm" in exI) |
267 apply (rule conjI) |
296 apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'") |
268 apply (simp (no_asm) add: fresh_star_def) |
297 apply (simp add: alphas fresh_star_zero) |
269 |
298 apply (subgoal_tac "\<And>x. x \<in> supp (subst \<theta>' (p \<bullet> T)) \<Longrightarrow> x \<in> p \<bullet> atom ` fset xs \<longleftrightarrow> x \<in> atom ` fset xsa") |
270 apply rule |
299 apply blast |
271 apply(simp (no_asm) only: Abs_fresh_iff) |
300 apply (subgoal_tac "x \<in> supp(p \<bullet> \<theta>', p \<bullet> T)") |
272 apply(clarify) |
301 apply (simp add: supp_Pair eqvts eqvts_raw) |
273 apply auto[1] |
302 apply auto[1] |
274 apply (simp add: fresh_star_def fresh_def) |
303 apply (subgoal_tac "(atom ` fset (p \<bullet> xs)) \<sharp>* \<theta>'") |
275 |
304 apply (simp add: fresh_star_def fresh_def) |
276 apply (simp (no_asm) add: fresh_star_def) |
305 apply(drule_tac p1="p" in iffD2[OF fresh_star_permute_iff]) |
277 apply rule |
306 apply (simp add: eqvts eqvts_raw) |
278 apply auto[1] |
307 apply (simp add: fresh_star_def fresh_def) |
279 apply(simp (no_asm) only: Abs_fresh_iff) |
308 apply (simp (no_asm) only: supp_eqvt[symmetric] Pair_eqvt[symmetric]) |
280 apply(clarify) |
309 apply (subgoal_tac "p \<bullet> supp (subst \<theta>' T) \<subseteq> p \<bullet> supp (\<theta>', T)") |
281 apply auto[1] |
310 apply (erule subsetD) |
282 apply(drule_tac a="atom x" in fresh_eqvt_at) |
311 apply (simp add: supp_eqvt) |
283 apply (simp add: supp_Pair finite_supp) |
312 apply (metis le_eqvt permute_boolI) |
284 apply (simp add: fresh_Pair) |
313 apply (rule perm_supp_eq) |
285 apply(auto simp add: Abs_fresh_iff fresh_star_def)[2] |
314 apply (simp add: fresh_def fresh_star_def) |
286 apply (simp add: fresh_def) |
315 apply blast |
287 apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'") |
316 oops |
288 prefer 2 |
|
289 apply (rule perm_supp_eq) |
|
290 apply (subgoal_tac "(atom ` fset xs \<inter> supp T \<union> atom ` fset xsa \<inter> supp (p \<bullet> T)) \<sharp>* \<theta>'") |
|
291 apply (auto simp add: fresh_star_def)[1] |
|
292 apply (simp add: fresh_star_Un fresh_star_def) |
|
293 apply blast |
|
294 apply(simp add: eqvt_at_def inter_eqvt supp_eqvt) |
|
295 apply (simp only: Abs_eq_res_set[symmetric]) |
|
296 apply (simp add: Abs_eq_iff alphas) |
|
297 apply rule |
|
298 prefer 2 |
|
299 apply (rule_tac x="0 :: perm" in exI) |
|
300 apply (simp add: fresh_star_zero) |
|
301 apply (rule helper) |
|
302 prefer 3 |
|
303 apply (subgoal_tac "supp ((\<lambda>(l, r). subst l r) (\<theta>', (p \<bullet> T))) \<subseteq> supp \<theta>' \<union> supp (p \<bullet> T)") |
|
304 apply simp |
|
305 apply (subst supp_Pair[symmetric]) |
|
306 apply (rule supp_eqvt_at) |
|
307 apply (simp add: eqvt_at_def) |
|
308 apply (thin_tac " p \<bullet> atom ` fset xs \<inter> supp (p \<bullet> T) = atom ` fset xsa \<inter> supp (p \<bullet> T)") |
|
309 apply (thin_tac "supp T - atom ` fset xs \<inter> supp T = supp (p \<bullet> T) - atom ` fset xsa \<inter> supp (p \<bullet> T)") |
|
310 apply (thin_tac "supp p \<subseteq> atom ` fset xs \<inter> supp T \<union> atom ` fset xsa \<inter> supp (p \<bullet> T)") |
|
311 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)") |
|
312 apply (thin_tac "atom ` fset xs \<sharp>* \<theta>'") |
|
313 apply (thin_tac "atom ` fset xsa \<sharp>* \<theta>'") |
|
314 apply (thin_tac "(supp (p \<bullet> T) - atom ` fset xsa \<inter> supp (p \<bullet> T)) \<sharp>* p") |
|
315 apply (rule) |
|
316 apply (subgoal_tac "\<forall>p. p \<bullet> subst \<theta>' T = subst (p \<bullet> \<theta>') (p \<bullet> T)") |
|
317 apply (erule_tac x="p" in allE) |
|
318 apply (erule_tac x="pa + p" in allE) |
|
319 apply (metis permute_plus) |
|
320 apply assumption |
|
321 apply (simp add: supp_Pair finite_supp) |
|
322 prefer 2 apply blast |
|
323 prefer 2 apply (metis finite_UNIV finite_imageI obtain_at_base rangeI) |
|
324 apply (rule_tac s="supp \<theta>'" in trans) |
|
325 apply (subgoal_tac "(p \<bullet> atom ` fset xs) \<sharp>* \<theta>'") |
|
326 apply (auto simp add: fresh_star_def fresh_def)[1] |
|
327 apply (subgoal_tac "supp p \<sharp>* \<theta>'") |
|
328 apply (metis fresh_star_permute_iff) |
|
329 apply (subgoal_tac "(atom ` fset xs \<union> atom ` fset xsa) \<sharp>* \<theta>'") |
|
330 apply (auto simp add: fresh_star_def)[1] |
|
331 apply (simp add: fresh_star_Un) |
|
332 apply (auto simp add: fresh_star_def fresh_def)[1] |
|
333 oops |
|
334 |
317 |
335 section {* defined as two separate nominal datatypes *} |
318 section {* defined as two separate nominal datatypes *} |
336 |
319 |
337 nominal_datatype ty2 = |
320 nominal_datatype ty2 = |
338 Var2 "name" |
321 Var2 "name" |
399 |
382 |
400 lemma fresh_star_inter1: |
383 lemma fresh_star_inter1: |
401 "xs \<sharp>* z \<Longrightarrow> (xs \<inter> ys) \<sharp>* z" |
384 "xs \<sharp>* z \<Longrightarrow> (xs \<inter> ys) \<sharp>* z" |
402 unfolding fresh_star_def by blast |
385 unfolding fresh_star_def by blast |
403 |
386 |
404 lemma Abs_res_fcb: |
|
405 fixes xs ys :: "('a :: at_base) set" |
|
406 and S T :: "'b :: fs" |
|
407 assumes e: "(Abs_res (atom ` xs) T) = (Abs_res (atom ` ys) S)" |
|
408 and f1: "\<And>x. x \<in> atom ` xs \<Longrightarrow> x \<in> supp T \<Longrightarrow> x \<sharp> f xs T" |
|
409 and f2: "\<And>x. supp T - atom ` xs = supp S - atom ` ys \<Longrightarrow> x \<in> atom ` ys \<Longrightarrow> x \<in> supp S \<Longrightarrow> x \<sharp> f xs T" |
|
410 and eqv: "\<And>p. p \<bullet> T = S \<Longrightarrow> supp p \<subseteq> atom ` xs \<inter> supp T \<union> atom ` ys \<inter> supp S |
|
411 \<Longrightarrow> p \<bullet> (atom ` xs \<inter> supp T) = atom ` ys \<inter> supp S \<Longrightarrow> p \<bullet> (f xs T) = f ys S" |
|
412 shows "f xs T = f ys S" |
|
413 using e apply - |
|
414 apply (subst (asm) Abs_eq_res_set) |
|
415 apply (subst (asm) Abs_eq_iff2) |
|
416 apply (simp add: alphas) |
|
417 apply (elim exE conjE) |
|
418 apply(rule trans) |
|
419 apply (rule_tac p="p" in supp_perm_eq[symmetric]) |
|
420 apply(rule fresh_star_supp_conv) |
|
421 apply(drule fresh_star_perm_set_conv) |
|
422 apply (rule finite_Diff) |
|
423 apply (rule finite_supp) |
|
424 apply (subgoal_tac "(atom ` xs \<inter> supp T \<union> atom ` ys \<inter> supp S) \<sharp>* f xs T") |
|
425 apply (metis Un_absorb2 fresh_star_Un) |
|
426 apply (subst fresh_star_Un) |
|
427 apply (rule conjI) |
|
428 apply (simp add: fresh_star_def f1) |
|
429 apply (subgoal_tac "supp T - atom ` xs = supp S - atom ` ys") |
|
430 apply (simp add: fresh_star_def f2) |
|
431 apply blast |
|
432 apply (simp add: eqv) |
|
433 done |
|
434 |
|
435 nominal_primrec |
387 nominal_primrec |
436 substs :: "(name \<times> ty2) list \<Rightarrow> tys2 \<Rightarrow> tys2" |
388 substs :: "(name \<times> ty2) list \<Rightarrow> tys2 \<Rightarrow> tys2" |
437 where |
389 where |
438 "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All2 xs t) = All2 xs (subst \<theta> t)" |
390 "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All2 xs t) = All2 xs (subst \<theta> t)" |
439 unfolding eqvt_def substs_graph_def |
391 unfolding eqvt_def substs_graph_def |
453 apply (simp add: subst_eqvt) |
405 apply (simp add: subst_eqvt) |
454 apply (subst Abs_eq_iff) |
406 apply (subst Abs_eq_iff) |
455 apply (rule_tac x="0::perm" in exI) |
407 apply (rule_tac x="0::perm" in exI) |
456 apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'") |
408 apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'") |
457 apply (simp add: alphas fresh_star_zero) |
409 apply (simp add: alphas fresh_star_zero) |
|
410 apply (subgoal_tac "\<And>x. x \<in> supp (subst \<theta>' (p \<bullet> t)) \<Longrightarrow> x \<in> p \<bullet> atom ` fset xs \<longleftrightarrow> x \<in> atom ` fset xsa") |
|
411 apply blast |
|
412 apply (subgoal_tac "x \<in> supp(p \<bullet> \<theta>', p \<bullet> t)") |
|
413 apply (simp add: supp_Pair eqvts eqvts_raw) |
458 apply auto[1] |
414 apply auto[1] |
459 apply (subgoal_tac "atom xa \<in> p \<bullet> (atom ` fset xs \<inter> supp t)") |
415 apply (subgoal_tac "(atom ` fset (p \<bullet> xs)) \<sharp>* \<theta>'") |
460 apply (simp add: inter_eqvt) |
416 apply (simp add: fresh_star_def fresh_def) |
461 apply blast |
417 apply(drule_tac p1="p" in iffD2[OF fresh_star_permute_iff]) |
462 apply (subgoal_tac "atom xa \<in> supp(p \<bullet> t)") |
418 apply (simp add: eqvts eqvts_raw) |
463 apply (auto simp add: IntI image_eqI) |
419 apply (simp add: fresh_star_def fresh_def) |
464 apply (drule subsetD[OF supp_subst]) |
420 apply (drule subsetD[OF supp_subst]) |
465 apply (simp add: fresh_star_def fresh_def) |
421 apply (simp add: supp_Pair) |
466 apply (subgoal_tac "x \<in> p \<bullet> (atom ` fset xs \<inter> supp t)") |
|
467 apply (simp) |
|
468 apply (subgoal_tac "x \<in> supp(p \<bullet> t)") |
|
469 apply (metis inf1I inter_eqvt mem_def supp_eqvt) |
|
470 apply (subgoal_tac "x \<notin> supp \<theta>'") |
|
471 apply (metis UnE subsetD supp_subst) |
|
472 apply (subgoal_tac "(p \<bullet> (atom ` fset xs)) \<sharp>* (p \<bullet> \<theta>')") |
|
473 apply (simp add: fresh_star_def fresh_def) |
|
474 apply (simp (no_asm) add: fresh_star_permute_iff) |
|
475 apply (rule perm_supp_eq) |
422 apply (rule perm_supp_eq) |
476 apply (simp add: fresh_def fresh_star_def) |
423 apply (simp add: fresh_def fresh_star_def) |
477 apply blast |
424 apply blast |
478 done |
425 done |
479 |
426 |