equal
deleted
inserted
replaced
18 thm lam.eq_iff |
18 thm lam.eq_iff |
19 thm lam.fv_bn_eqvt |
19 thm lam.fv_bn_eqvt |
20 thm lam.size_eqvt |
20 thm lam.size_eqvt |
21 |
21 |
22 nominal_primrec |
22 nominal_primrec |
23 depth :: "lam \<Rightarrow> nat" |
23 height :: "lam \<Rightarrow> int" |
24 where |
24 where |
25 "depth (Var x) = 1" |
25 "height (Var x) = 1" |
26 | "depth (App t1 t2) = (max (depth t1) (depth t2)) + 1" |
26 | "height (App t1 t2) = (max (height t1) (height t2)) + 1" |
27 | "depth (Lam x t) = (depth t) + 1" |
27 | "height (Lam x t) = (height t) + 1" |
28 apply(rule_tac y="x" in lam.exhaust) |
28 apply(rule_tac y="x" in lam.exhaust) |
29 apply(simp_all)[3] |
29 apply(simp_all)[3] |
30 apply(simp_all only: lam.distinct) |
30 apply(simp_all only: lam.distinct) |
31 apply(simp add: lam.eq_iff) |
31 apply(simp add: lam.eq_iff) |
32 apply(simp add: lam.eq_iff) |
32 apply(simp add: lam.eq_iff) |
156 apply(rule perm_supp_eq) |
156 apply(rule perm_supp_eq) |
157 apply(auto simp add: fresh_star_def fresh_Pair)[1] |
157 apply(auto simp add: fresh_star_def fresh_Pair)[1] |
158 apply(rule perm_supp_eq) |
158 apply(rule perm_supp_eq) |
159 apply(auto simp add: fresh_star_def fresh_Pair)[1] |
159 apply(auto simp add: fresh_star_def fresh_Pair)[1] |
160 done |
160 done |
|
161 |
|
162 termination |
|
163 apply(relation "measure (\<lambda>(t,_,_). size t)") |
|
164 apply(simp_all add: lam.size) |
|
165 done |
161 |
166 |
162 nominal_datatype ln = |
167 nominal_datatype ln = |
163 LNBnd nat |
168 LNBnd nat |
164 | LNVar name |
169 | LNVar name |
165 | LNApp ln ln |
170 | LNApp ln ln |