equal
deleted
inserted
replaced
22 next |
22 next |
23 case (Lam y e1) |
23 case (Lam y e1) |
24 have ih: "height (e1[x::=e']) \<le> height e1 - 1 + height e'" by fact |
24 have ih: "height (e1[x::=e']) \<le> height e1 - 1 + height e'" by fact |
25 moreover |
25 moreover |
26 have vc: "atom y \<sharp> x" "atom y \<sharp> e'" by fact+ (* usual variable convention *) |
26 have vc: "atom y \<sharp> x" "atom y \<sharp> e'" by fact+ (* usual variable convention *) |
27 ultimately show "height ((Lam y e1)[x::=e']) \<le> height (Lam y e1) - 1 + height e'" by simp |
27 ultimately show "height ((Lam [y].e1)[x::=e']) \<le> height (Lam [y].e1) - 1 + height e'" by simp |
28 next |
28 next |
29 case (App e1 e2) |
29 case (App e1 e2) |
30 have ih1: "height (e1[x::=e']) \<le> (height e1) - 1 + height e'" |
30 have ih1: "height (e1[x::=e']) \<le> (height e1) - 1 + height e'" |
31 and ih2: "height (e2[x::=e']) \<le> (height e2) - 1 + height e'" by fact+ |
31 and ih2: "height (e2[x::=e']) \<le> (height e2) - 1 + height e'" by fact+ |
32 then show "height ((App e1 e2)[x::=e']) \<le> height (App e1 e2) - 1 + height e'" by simp |
32 then show "height ((App e1 e2)[x::=e']) \<le> height (App e1 e2) - 1 + height e'" by simp |