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 nominal_primrec |
|
14 Z :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam" |
|
15 where |
|
16 "Z (App M N) k = Z M (%m. (Z N (%n.(App m n))))" |
|
17 unfolding eqvt_def Z_graph_def |
|
18 apply (rule, perm_simp, rule) |
|
19 oops |
|
20 |
12 |
21 |
13 |
22 inductive |
14 inductive |
23 triv :: "lam \<Rightarrow> nat \<Rightarrow> bool" |
15 triv :: "lam \<Rightarrow> nat \<Rightarrow> bool" |
24 where |
16 where |
575 apply(rule refl) |
567 apply(rule refl) |
576 oops |
568 oops |
577 |
569 |
578 text {* "HO" functions *} |
570 text {* "HO" functions *} |
579 |
571 |
580 |
|
581 nominal_primrec |
572 nominal_primrec |
582 trans2 :: "lam \<Rightarrow> atom list \<Rightarrow> db option" |
573 trans2 :: "lam \<Rightarrow> atom list \<Rightarrow> db option" |
583 where |
574 where |
584 "trans2 (Var x) xs = (index xs 0 (atom x) \<guillemotright>= (\<lambda>n. Some (DBVar n)))" |
575 "trans2 (Var x) xs = (index xs 0 (atom x) \<guillemotright>= (\<lambda>n. Some (DBVar n)))" |
585 | "trans2 (App t1 t2) xs = ((trans2 t1 xs) \<guillemotright>= (\<lambda>db1. (trans2 t2 xs) \<guillemotright>= (\<lambda>db2. Some (DBApp db1 db2))))" |
576 | "trans2 (App t1 t2) xs = ((trans2 t1 xs) \<guillemotright>= (\<lambda>db1. (trans2 t2 xs) \<guillemotright>= (\<lambda>db2. Some (DBApp db1 db2))))" |
599 Z :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam" |
590 Z :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam" |
600 where |
591 where |
601 "Z (App M N) k = Z M (%m. (Z N (%n.(App m n))))" |
592 "Z (App M N) k = Z M (%m. (Z N (%n.(App m n))))" |
602 unfolding eqvt_def Z_graph_def |
593 unfolding eqvt_def Z_graph_def |
603 apply (rule, perm_simp, rule) |
594 apply (rule, perm_simp, rule) |
604 prefer 2 |
|
605 ML_prf {* prop_of (hd (#prems (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))))) *} |
|
606 oops |
595 oops |
607 |
596 |
608 (* function tests *) |
597 (* function tests *) |
609 |
598 |
610 (* similar problem with function package *) |
599 (* similar problem with function package *) |