equal
deleted
inserted
replaced
7 |
7 |
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 |
|
13 |
12 |
14 inductive |
13 inductive |
15 triv :: "lam \<Rightarrow> nat \<Rightarrow> bool" |
14 triv :: "lam \<Rightarrow> nat \<Rightarrow> bool" |
16 where |
15 where |
17 Var: "triv (Var x) n" |
16 Var: "triv (Var x) n" |
561 apply(perm_simp) |
560 apply(perm_simp) |
562 apply(rule allI) |
561 apply(rule allI) |
563 apply(rule refl) |
562 apply(rule refl) |
564 oops |
563 oops |
565 |
564 |
566 text {* not working yet *} |
565 text {* "HO" functions *} |
567 |
566 |
568 (* not working yet |
567 nominal_primrec |
569 nominal_primrec |
568 trans2 :: "lam \<Rightarrow> atom list \<Rightarrow> db option" |
570 trans :: "lam \<Rightarrow> atom list \<Rightarrow> db option" |
569 where |
571 where |
570 "trans2 (Var x) xs = (index xs 0 (atom x) \<guillemotright>= (\<lambda>n. Some (DBVar n)))" |
572 "trans (Var x) xs = (index xs 0 (atom x) \<guillemotright>= (\<lambda>n. Some (DBVar n)))" |
571 | "trans2 (App t1 t2) xs = ((trans2 t1 xs) \<guillemotright>= (\<lambda>db1. (trans2 t2 xs) \<guillemotright>= (\<lambda>db2. Some (DBApp db1 db2))))" |
573 | "trans (App t1 t2) xs = ((trans t1 xs) \<guillemotright>= (\<lambda>db1. (trans t2 xs) \<guillemotright>= (\<lambda>db2. Some (DBApp db1 db2))))" |
572 | "trans2 (Lam [x].t) xs = (trans2 t (atom x # xs) \<guillemotright>= (\<lambda>db. Some (DBLam db)))" |
574 | "trans (Lam [x].t) xs = (trans t (atom x # xs) \<guillemotright>= (\<lambda>db. Some (DBLam db)))" |
573 oops |
575 *) |
574 |
576 |
|
577 (* not working yet |
|
578 nominal_primrec |
575 nominal_primrec |
579 CPS :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam" |
576 CPS :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam" |
580 where |
577 where |
581 "CPS (Var x) k = Var x" |
578 "CPS (Var x) k = Var x" |
582 | "CPS (App M N) k = CPS M (\<lambda>m. CPS N (\<lambda>n. n))" |
579 | "CPS (App M N) k = CPS M (\<lambda>m. CPS N (\<lambda>n. n))" |
583 *) |
580 oops |
584 |
581 |
585 |
582 |
586 (* function tests *) |
583 (* function tests *) |
587 |
584 |
588 (* similar problem with function package *) |
585 (* similar problem with function package *) |