equal
deleted
inserted
replaced
1 theory Lambda |
1 theory Lambda |
2 imports "../Nominal2" |
2 imports "../Nominal2" |
3 begin |
3 begin |
|
4 |
4 |
5 |
5 atom_decl name |
6 atom_decl name |
6 |
7 |
7 nominal_datatype lam = |
8 nominal_datatype lam = |
8 Var "name" |
9 Var "name" |
9 | App "lam" "lam" |
10 | App "lam" "lam" |
10 | 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 inductive |
|
14 triv :: "lam \<Rightarrow> nat \<Rightarrow> bool" |
|
15 where |
|
16 Var: "triv (Var x) n" |
|
17 |
|
18 equivariance triv |
|
19 nominal_inductive triv avoids Var : "{}::name set" |
|
20 apply(auto simp add: fresh_star_def) |
|
21 done |
|
22 |
11 |
23 |
12 text {* height function *} |
24 text {* height function *} |
13 |
25 |
14 nominal_primrec |
26 nominal_primrec |
15 height :: "lam \<Rightarrow> int" |
27 height :: "lam \<Rightarrow> int" |
492 | "trans (Lam [x].t) xs = (trans t (atom x # xs) \<guillemotright>= (\<lambda>db. Some (DBLam db)))" |
504 | "trans (Lam [x].t) xs = (trans t (atom x # xs) \<guillemotright>= (\<lambda>db. Some (DBLam db)))" |
493 *) |
505 *) |
494 |
506 |
495 |
507 |
496 |
508 |
497 |
|
498 end |
509 end |
499 |
510 |
500 |
511 |
501 |
512 |