82 apply(simp) |
82 apply(simp) |
83 apply(simp add: eqvt_at_def eqvts) |
83 apply(simp add: eqvt_at_def eqvts) |
84 apply(simp) |
84 apply(simp) |
85 done |
85 done |
86 |
86 |
87 print_theorems |
|
88 |
|
89 termination |
87 termination |
90 by (relation "measure size") (auto simp add: lam.size) |
88 by (relation "measure size") (auto simp add: lam.size) |
91 |
89 |
92 |
|
93 thm frees_set.simps |
90 thm frees_set.simps |
|
91 thm frees_set.induct |
|
92 |
|
93 lemma "frees_set t = supp t" |
|
94 apply(induct rule: frees_set.induct) |
|
95 apply(simp_all add: lam.supp supp_at_base) |
|
96 done |
94 |
97 |
95 lemma fresh_fun_eqvt_app3: |
98 lemma fresh_fun_eqvt_app3: |
96 assumes a: "eqvt f" |
99 assumes a: "eqvt f" |
97 and b: "a \<sharp> x" "a \<sharp> y" "a \<sharp> z" |
100 and b: "a \<sharp> x" "a \<sharp> y" "a \<sharp> z" |
98 shows "a \<sharp> f x y z" |
101 shows "a \<sharp> f x y z" |
205 "height (Var x) = 1" |
206 "height (Var x) = 1" |
206 | "height (App t1 t2) = max (height t1) (height t2) + 1" |
207 | "height (App t1 t2) = max (height t1) (height t2) + 1" |
207 | "height (Lam [x].t) = height t + 1" |
208 | "height (Lam [x].t) = height t + 1" |
208 unfolding eqvt_def height_graph_def |
209 unfolding eqvt_def height_graph_def |
209 apply (rule, perm_simp, rule) |
210 apply (rule, perm_simp, rule) |
|
211 apply(rule TrueI) |
210 apply(rule_tac y="x" in lam.exhaust) |
212 apply(rule_tac y="x" in lam.exhaust) |
211 apply(auto simp add: lam.distinct lam.eq_iff) |
213 apply(auto simp add: lam.distinct lam.eq_iff) |
212 apply (erule Abs1_eq_fdest) |
214 apply (erule Abs1_eq_fdest) |
213 apply(simp_all add: fresh_def pure_supp eqvt_at_def) |
215 apply(simp_all add: fresh_def pure_supp eqvt_at_def) |
214 done |
216 done |
227 "frees_lst (Var x) = [atom x]" |
229 "frees_lst (Var x) = [atom x]" |
228 | "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2" |
230 | "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2" |
229 | "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)" |
231 | "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)" |
230 unfolding eqvt_def frees_lst_graph_def |
232 unfolding eqvt_def frees_lst_graph_def |
231 apply (rule, perm_simp, rule) |
233 apply (rule, perm_simp, rule) |
|
234 apply(rule TrueI) |
232 apply(rule_tac y="x" in lam.exhaust) |
235 apply(rule_tac y="x" in lam.exhaust) |
233 apply(auto) |
236 apply(auto) |
234 apply (erule Abs1_eq_fdest) |
237 apply (erule Abs1_eq_fdest) |
235 apply(simp add: supp_removeAll fresh_def) |
238 apply(simp add: supp_removeAll fresh_def) |
236 apply(drule supp_eqvt_at) |
239 apply(drule supp_eqvt_at) |
256 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
259 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
257 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
260 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
258 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])" |
261 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])" |
259 unfolding eqvt_def subst_graph_def |
262 unfolding eqvt_def subst_graph_def |
260 apply (rule, perm_simp, rule) |
263 apply (rule, perm_simp, rule) |
|
264 apply(rule TrueI) |
261 apply(auto simp add: lam.distinct lam.eq_iff) |
265 apply(auto simp add: lam.distinct lam.eq_iff) |
262 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) |
266 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) |
263 apply(blast)+ |
267 apply(blast)+ |
264 apply(simp_all add: fresh_star_def fresh_Pair_elim) |
268 apply(simp_all add: fresh_star_def fresh_Pair_elim) |
265 apply (erule Abs1_eq_fdest) |
269 apply (erule Abs1_eq_fdest) |
411 lookup :: "name list \<Rightarrow> nat \<Rightarrow> name \<Rightarrow> ln" |
415 lookup :: "name list \<Rightarrow> nat \<Rightarrow> name \<Rightarrow> ln" |
412 where |
416 where |
413 "lookup [] n x = LNVar x" |
417 "lookup [] n x = LNVar x" |
414 | "lookup (y # ys) n x = (if x = y then LNBnd n else (lookup ys (n + 1) x))" |
418 | "lookup (y # ys) n x = (if x = y then LNBnd n else (lookup ys (n + 1) x))" |
415 |
419 |
|
420 lemma supp_lookup: |
|
421 shows "supp (lookup xs n x) \<subseteq> supp x" |
|
422 apply(induct arbitrary: n rule: lookup.induct) |
|
423 apply(simp add: ln.supp) |
|
424 apply(simp add: ln.supp pure_supp) |
|
425 done |
|
426 |
|
427 |
416 lemma [eqvt]: |
428 lemma [eqvt]: |
417 shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)" |
429 shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)" |
418 by (induct xs arbitrary: n) (simp_all add: permute_pure) |
430 by (induct xs arbitrary: n) (simp_all add: permute_pure) |
419 |
431 |
420 nominal_primrec |
432 nominal_primrec (invariant "\<lambda>x y. supp y \<subseteq> supp x") |
421 trans :: "lam \<Rightarrow> name list \<Rightarrow> ln" |
433 trans :: "lam \<Rightarrow> name list \<Rightarrow> ln" |
422 where |
434 where |
423 "trans (Var x) xs = lookup xs 0 x" |
435 "trans (Var x) xs = lookup xs 0 x" |
424 | "trans (App t1 t2) xs = LNApp (trans t1 xs) (trans t2 xs)" |
436 | "trans (App t1 t2) xs = LNApp (trans t1 xs) (trans t2 xs)" |
425 | "atom x \<sharp> xs \<Longrightarrow> trans (Lam [x]. t) xs = LNLam (trans t (x # xs))" |
437 | "atom x \<sharp> xs \<Longrightarrow> trans (Lam [x]. t) xs = LNLam (trans t (x # xs))" |
426 unfolding eqvt_def trans_graph_def |
438 apply(simp add: eqvt_def trans_graph_def) |
427 apply (rule, perm_simp, rule) |
439 apply (rule, perm_simp, rule) |
|
440 defer |
428 apply(case_tac x) |
441 apply(case_tac x) |
429 apply(simp) |
442 apply(simp) |
430 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
443 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
431 apply(simp_all add: fresh_star_def)[3] |
444 apply(simp_all add: fresh_star_def)[3] |
432 apply(blast) |
445 apply(blast) |
433 apply(blast) |
446 apply(blast) |
434 apply(simp_all add: lam.distinct lam.eq_iff) |
447 apply(simp_all) |
435 apply(elim conjE) |
448 apply(elim conjE) |
436 apply clarify |
449 apply clarify |
437 apply (erule Abs1_eq_fdest) |
450 apply (erule Abs1_eq_fdest) |
438 apply (simp_all add: ln.fresh) |
451 apply (simp_all add: ln.fresh) |
439 prefer 2 |
452 prefer 2 |
441 apply (auto simp add: finite_supp supp_Pair fresh_def supp_Cons supp_at_base)[2] |
454 apply (auto simp add: finite_supp supp_Pair fresh_def supp_Cons supp_at_base)[2] |
442 prefer 2 |
455 prefer 2 |
443 apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> xsa = xsa") |
456 apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> xsa = xsa") |
444 apply (simp add: eqvt_at_def) |
457 apply (simp add: eqvt_at_def) |
445 apply (metis atom_name_def swap_fresh_fresh) |
458 apply (metis atom_name_def swap_fresh_fresh) |
|
459 apply(simp add: fresh_def) |
|
460 defer |
|
461 apply(erule trans_graph.induct) |
|
462 defer |
|
463 apply(simp add: lam.supp ln.supp) |
|
464 apply(blast) |
|
465 apply(simp add: lam.supp ln.supp) |
446 oops |
466 oops |
447 |
467 |
448 (* lemma helpr: "atom x \<sharp> ta \<Longrightarrow> Lam [xa]. ta = Lam [x]. ((xa \<leftrightarrow> x) \<bullet> ta)" |
468 (* lemma helpr: "atom x \<sharp> ta \<Longrightarrow> Lam [xa]. ta = Lam [x]. ((xa \<leftrightarrow> x) \<bullet> ta)" |
449 apply (case_tac "x = xa") |
469 apply (case_tac "x = xa") |
450 apply simp |
470 apply simp |
547 lemma vindex_eqvt[eqvt]: |
567 lemma vindex_eqvt[eqvt]: |
548 "(p \<bullet> vindex l v n) = vindex (p \<bullet> l) (p \<bullet> v) (p \<bullet> n)" |
568 "(p \<bullet> vindex l v n) = vindex (p \<bullet> l) (p \<bullet> v) (p \<bullet> n)" |
549 by (induct l arbitrary: n) (simp_all add: permute_pure) |
569 by (induct l arbitrary: n) (simp_all add: permute_pure) |
550 |
570 |
551 nominal_primrec |
571 nominal_primrec |
552 trans :: "lam \<Rightarrow> name list \<Rightarrow> db option" |
572 transdb :: "lam \<Rightarrow> name list \<Rightarrow> db option" |
553 where |
573 where |
554 "trans (Var x) l = vindex l x 0" |
574 "transdb (Var x) l = vindex l x 0" |
555 | "trans (App t1 t2) xs = dbapp_in (trans t1 xs) (trans t2 xs)" |
575 | "transdb (App t1 t2) xs = dbapp_in (transdb t1 xs) (transdb t2 xs)" |
556 | "x \<notin> set xs \<Longrightarrow> trans (Lam [x].t) xs = dblam_in (trans t (x # xs))" |
576 | "x \<notin> set xs \<Longrightarrow> transdb (Lam [x].t) xs = dblam_in (transdb t (x # xs))" |
557 unfolding eqvt_def trans_graph_def |
577 unfolding eqvt_def transdb_graph_def |
558 apply (rule, perm_simp, rule) |
578 apply (rule, perm_simp, rule) |
|
579 apply(rule TrueI) |
559 apply (case_tac x) |
580 apply (case_tac x) |
560 apply (rule_tac y="a" and c="b" in lam.strong_exhaust) |
581 apply (rule_tac y="a" and c="b" in lam.strong_exhaust) |
561 apply (auto simp add: fresh_star_def fresh_at_list) |
582 apply (auto simp add: fresh_star_def fresh_at_list) |
562 apply (rule_tac f="dblam_in" in arg_cong) |
583 apply (rule_tac f="dblam_in" in arg_cong) |
563 apply (erule Abs1_eq_fdest) |
584 apply (erule Abs1_eq_fdest) |
568 done |
589 done |
569 |
590 |
570 termination |
591 termination |
571 by (relation "measure (\<lambda>(t,_). size t)") (simp_all add: lam.size) |
592 by (relation "measure (\<lambda>(t,_). size t)") (simp_all add: lam.size) |
572 |
593 |
573 lemma trans_eqvt[eqvt]: |
594 lemma transdb_eqvt[eqvt]: |
574 "p \<bullet> trans t l = trans (p \<bullet>t) (p \<bullet>l)" |
595 "p \<bullet> transdb t l = transdb (p \<bullet>t) (p \<bullet>l)" |
575 apply (nominal_induct t avoiding: l p rule: lam.strong_induct) |
596 apply (nominal_induct t avoiding: l p rule: lam.strong_induct) |
576 apply (simp add: vindex_eqvt) |
597 apply (simp add: vindex_eqvt) |
577 apply (simp_all add: permute_pure) |
598 apply (simp_all add: permute_pure) |
578 apply (simp add: fresh_at_list) |
599 apply (simp add: fresh_at_list) |
579 apply (subst trans.simps) |
600 apply (subst transdb.simps) |
580 apply (simp add: fresh_at_list[symmetric]) |
601 apply (simp add: fresh_at_list[symmetric]) |
581 apply (drule_tac x="name # l" in meta_spec) |
602 apply (drule_tac x="name # l" in meta_spec) |
582 apply auto |
603 apply auto |
583 done |
604 done |
584 |
605 |
657 | "eqvt f \<Longrightarrow> map_term f (App t1 t2) = App (f t1) (f t2)" |
678 | "eqvt f \<Longrightarrow> map_term f (App t1 t2) = App (f t1) (f t2)" |
658 | "eqvt f \<Longrightarrow> map_term f (Lam [x].t) = Lam [x].(f t)" |
679 | "eqvt f \<Longrightarrow> map_term f (Lam [x].t) = Lam [x].(f t)" |
659 | "\<not>eqvt f \<Longrightarrow> map_term f t = t" |
680 | "\<not>eqvt f \<Longrightarrow> map_term f t = t" |
660 apply (simp add: eqvt_def map_term_graph_def) |
681 apply (simp add: eqvt_def map_term_graph_def) |
661 apply (rule, perm_simp, rule) |
682 apply (rule, perm_simp, rule) |
|
683 apply(rule TrueI) |
662 apply (case_tac x, case_tac "eqvt a", case_tac b rule: lam.exhaust) |
684 apply (case_tac x, case_tac "eqvt a", case_tac b rule: lam.exhaust) |
663 apply auto |
685 apply auto |
664 apply (erule Abs1_eq_fdest) |
686 apply (erule Abs1_eq_fdest) |
665 apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app) |
687 apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app) |
666 apply (simp add: eqvt_def permute_fun_app_eq) |
688 apply (simp add: eqvt_def permute_fun_app_eq) |