equal
deleted
inserted
replaced
14 triv :: "lam \<Rightarrow> nat \<Rightarrow> bool" |
14 triv :: "lam \<Rightarrow> nat \<Rightarrow> bool" |
15 where |
15 where |
16 Var: "triv (Var x) n" |
16 Var: "triv (Var x) n" |
17 |
17 |
18 equivariance triv |
18 equivariance triv |
19 nominal_inductive triv avoids Var : "{}::name set" |
19 nominal_inductive triv avoids Var: "{}::name set" |
20 apply(auto simp add: fresh_star_def) |
20 apply(auto simp add: fresh_star_def) |
21 done |
21 done |
|
22 |
|
23 inductive |
|
24 triv2 :: "lam \<Rightarrow> nat \<Rightarrow> bool" |
|
25 where |
|
26 Var1: "triv2 (Var x) 0" |
|
27 | Var2: "triv2 (Var x) (n + n)" |
|
28 | Var3: "triv2 (Var x) n" |
|
29 |
|
30 equivariance triv2 |
|
31 nominal_inductive triv2 . |
22 |
32 |
23 |
33 |
24 text {* height function *} |
34 text {* height function *} |
25 |
35 |
26 nominal_primrec |
36 nominal_primrec |