equal
deleted
inserted
replaced
20 thm lam.perm_simps |
20 thm lam.perm_simps |
21 thm lam.eq_iff |
21 thm lam.eq_iff |
22 thm lam.fv_bn_eqvt |
22 thm lam.fv_bn_eqvt |
23 thm lam.size_eqvt |
23 thm lam.size_eqvt |
24 |
24 |
|
25 definition |
|
26 "eqvt_at f x \<equiv> \<forall>p. p \<bullet> (f x) = f (p \<bullet> x)" |
|
27 |
|
28 function |
|
29 depth :: "lam \<Rightarrow> nat" |
|
30 where |
|
31 "depth (Var x) = 1" |
|
32 | "depth (App t1 t2) = (max (depth t1) (depth t2)) + 1" |
|
33 | "depth (Lam x t) = (depth t) + 1" |
|
34 oops |
25 |
35 |
26 section {* Matching *} |
36 section {* Matching *} |
27 |
37 |
28 definition |
38 definition |
29 MATCH :: "('c::pt \<Rightarrow> (bool * 'a::pt * 'b::pt)) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b" |
39 MATCH :: "('c::pt \<Rightarrow> (bool * 'a::pt * 'b::pt)) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b" |