equal
deleted
inserted
replaced
62 and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f bs y c) = f (p \<bullet> bs) (p \<bullet> y) c" |
62 and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f bs y c) = f (p \<bullet> bs) (p \<bullet> y) c" |
63 and ba_inj: "\<And>q r. q \<bullet> ba as = r \<bullet> ba bs \<Longrightarrow> q \<bullet> as = r \<bullet> bs" |
63 and ba_inj: "\<And>q r. q \<bullet> ba as = r \<bullet> ba bs \<Longrightarrow> q \<bullet> as = r \<bullet> bs" |
64 shows "f as x c = f bs y c" |
64 shows "f as x c = f bs y c" |
65 sorry |
65 sorry |
66 |
66 |
67 nominal_primrec |
67 nominal_function |
68 height_trm :: "trm \<Rightarrow> nat" |
68 height_trm :: "trm \<Rightarrow> nat" |
69 and height_assn :: "assn \<Rightarrow> nat" |
69 and height_assn :: "assn \<Rightarrow> nat" |
70 where |
70 where |
71 "height_trm (Var x) = 1" |
71 "height_trm (Var x) = 1" |
72 | "height_trm (App l r) = max (height_trm l) (height_trm r)" |
72 | "height_trm (App l r) = max (height_trm l) (height_trm r)" |