equal
deleted
inserted
replaced
12 |
12 |
13 inductive |
13 inductive |
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 |
|
18 lemma |
|
19 "p \<bullet> (triv t x) = triv (p \<bullet> t) (p \<bullet> x)" |
|
20 unfolding triv_def |
|
21 apply(perm_simp) |
|
22 oops |
|
23 (*apply(perm_simp)*) |
17 |
24 |
18 equivariance triv |
25 equivariance triv |
19 nominal_inductive triv avoids Var: "{}::name set" |
26 nominal_inductive triv avoids Var: "{}::name set" |
20 apply(auto simp add: fresh_star_def) |
27 apply(auto simp add: fresh_star_def) |
21 done |
28 done |