8 nominal_datatype lam = |
8 nominal_datatype lam = |
9 Var "name" |
9 Var "name" |
10 | App "lam" "lam" |
10 | App "lam" "lam" |
11 | Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100) |
11 | Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100) |
12 |
12 |
13 |
13 text {* free name function *} |
14 text {* free name function - returns an atom list *} |
14 |
|
15 text {* first returns an atom list *} |
15 |
16 |
16 nominal_primrec |
17 nominal_primrec |
17 frees_lst :: "lam \<Rightarrow> atom list" |
18 frees_lst :: "lam \<Rightarrow> atom list" |
18 where |
19 where |
19 "frees_lst (Var x) = [atom x]" |
20 "frees_lst (Var x) = [atom x]" |
36 |
37 |
37 text {* a small test lemma *} |
38 text {* a small test lemma *} |
38 lemma shows "supp t = set (frees_lst t)" |
39 lemma shows "supp t = set (frees_lst t)" |
39 by (induct t rule: frees_lst.induct) (simp_all add: lam.supp supp_at_base) |
40 by (induct t rule: frees_lst.induct) (simp_all add: lam.supp supp_at_base) |
40 |
41 |
41 text {* free name function - returns an atom set *} |
42 text {* second returns an atom set - therefore needs an invariant *} |
42 |
43 |
43 nominal_primrec (invariant "\<lambda>x (y::atom set). finite y") |
44 nominal_primrec (invariant "\<lambda>x (y::atom set). finite y") |
44 frees_set :: "lam \<Rightarrow> atom set" |
45 frees_set :: "lam \<Rightarrow> atom set" |
45 where |
46 where |
46 "frees_set (Var x) = {atom x}" |
47 "frees_set (Var x) = {atom x}" |
171 apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> ya = ya") |
172 apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> ya = ya") |
172 apply(simp add: eqvt_at_def) |
173 apply(simp add: eqvt_at_def) |
173 apply(simp_all add: swap_fresh_fresh) |
174 apply(simp_all add: swap_fresh_fresh) |
174 done |
175 done |
175 |
176 |
176 declare lam.size[simp] |
|
177 |
|
178 termination |
177 termination |
179 by lexicographic_order |
178 by lexicographic_order |
180 |
179 |
181 lemma subst_eqvt[eqvt]: |
180 lemma subst_eqvt[eqvt]: |
182 shows "(p \<bullet> t[x ::= s]) = (p \<bullet> t)[(p \<bullet> x) ::= (p \<bullet> s)]" |
181 shows "(p \<bullet> t[x ::= s]) = (p \<bullet> t)[(p \<bullet> x) ::= (p \<bullet> s)]" |
519 by (induct t x s rule: subst.induct) (auto simp add: lam.supp lam.fresh fresh_at_base) |
518 by (induct t x s rule: subst.induct) (auto simp add: lam.supp lam.fresh fresh_at_base) |
520 |
519 |
521 (* function that evaluates a lambda term *) |
520 (* function that evaluates a lambda term *) |
522 nominal_primrec |
521 nominal_primrec |
523 eval :: "lam \<Rightarrow> lam" and |
522 eval :: "lam \<Rightarrow> lam" and |
524 app :: "lam \<Rightarrow> lam \<Rightarrow> lam" |
523 apply_subst :: "lam \<Rightarrow> lam \<Rightarrow> lam" |
525 where |
524 where |
526 "eval (Var x) = Var x" |
525 "eval (Var x) = Var x" |
527 | "eval (Lam [x].t) = Lam [x].(eval t)" |
526 | "eval (Lam [x].t) = Lam [x].(eval t)" |
528 | "eval (App t1 t2) = sub (eval t1) (eval t2)" |
527 | "eval (App t1 t2) = apply_subst (eval t1) (eval t2)" |
529 | "app (Var x) t2 = App (Var x) t2" |
528 | "apply_subst (Var x) t2 = App (Var x) t2" |
530 | "app (App t0 t1) t2 = App (App t0 t1) t2" |
529 | "apply_subst (App t0 t1) t2 = App (App t0 t1) t2" |
531 | "atom x \<sharp> t2 \<Longrightarrow> app (Lam [x].t1) t2 = eval (t1[x::= t2])" |
530 | "atom x \<sharp> t2 \<Longrightarrow> apply_subst (Lam [x].t1) t2 = eval (t1[x::= t2])" |
532 apply(simp add: eval_app_graph_def eqvt_def) |
531 apply(simp add: eval_apply_subst_graph_def eqvt_def) |
533 apply(rule, perm_simp, rule) |
532 apply(rule, perm_simp, rule) |
534 apply(rule TrueI) |
533 apply(rule TrueI) |
535 apply (case_tac x) |
534 apply (case_tac x) |
536 apply (case_tac a rule: lam.exhaust) |
535 apply (case_tac a rule: lam.exhaust) |
537 apply simp_all[3] |
536 apply simp_all[3] |
549 apply (erule fresh_eqvt_at) |
548 apply (erule fresh_eqvt_at) |
550 apply (simp add: finite_supp) |
549 apply (simp add: finite_supp) |
551 apply (simp add: fresh_Inl) |
550 apply (simp add: fresh_Inl) |
552 apply (simp add: eqvt_at_def) |
551 apply (simp add: eqvt_at_def) |
553 apply simp |
552 apply simp |
554 defer |
|
555 apply clarify |
553 apply clarify |
556 apply(erule Abs_lst1_fcb) |
554 apply(erule Abs_lst1_fcb) |
557 apply (erule fresh_eqvt_at) |
555 apply (erule fresh_eqvt_at) |
558 apply (simp add: finite_supp) |
556 apply (simp add: finite_supp) |
559 apply (simp add: fresh_Inl var_fresh_subst) |
557 apply (simp add: fresh_Inl var_fresh_subst) |
565 apply (simp add: eqvt_at_def subst_eqvt) |
563 apply (simp add: eqvt_at_def subst_eqvt) |
566 apply (subst (2) swap_fresh_fresh) |
564 apply (subst (2) swap_fresh_fresh) |
567 apply assumption+ |
565 apply assumption+ |
568 apply rule |
566 apply rule |
569 apply simp |
567 apply simp |
570 oops (* can this be defined ? *) |
568 done |
571 (* Yes, if "sub" is a constant. *) |
569 |
572 |
570 |
573 text {* TODO: nominal_primrec throws RSN if an argument is not in FS, but function works *} |
571 (* a small test |
574 function q where |
572 termination sorry |
575 "q (Lam [x]. M) N = Lam [x]. (Lam [x]. (App M (q (Var x) N)))" |
573 |
576 | "q (Var x) N = Var x" |
574 lemma |
577 | "q (App l r) N = App l r" |
575 assumes "x \<noteq> y" |
578 oops |
576 shows "eval (App (Lam [x].App (Var x) (Var x)) (Var y)) = App (Var y) (Var y)" |
|
577 using assms |
|
578 apply(simp add: lam.supp fresh_def supp_at_base) |
|
579 done |
|
580 *) |
|
581 |
579 |
582 |
580 text {* TODO: eqvt_at for the other side *} |
583 text {* TODO: eqvt_at for the other side *} |
581 nominal_primrec q where |
584 nominal_primrec q where |
582 "atom c \<sharp> (x, M) \<Longrightarrow> q (Lam [x]. M) (N :: lam) = Lam [x]. (Lam [c]. (App M (q (Var c) N)))" |
585 "atom c \<sharp> (x, M) \<Longrightarrow> q (Lam [x]. M) (N :: lam) = Lam [x]. (Lam [c]. (App M (q (Var c) N)))" |
583 | "q (Var x) N = Var x" |
586 | "q (Var x) N = Var x" |