equal
deleted
inserted
replaced
12 nominal_datatype lam = |
12 nominal_datatype lam = |
13 Var "name" |
13 Var "name" |
14 | App "lam" "lam" |
14 | App "lam" "lam" |
15 | Lam x::"name" l::"lam" bind x in l ("Lam [_]._" [100,100] 100) |
15 | Lam x::"name" l::"lam" bind x in l ("Lam [_]._" [100,100] 100) |
16 |
16 |
17 thm lam.strong_induct |
|
18 |
17 |
19 text {* Definition of the height-function on lambda-terms. *} |
18 text {* Definition of the height-function on lambda-terms. *} |
20 |
19 |
21 function |
20 function |
22 height :: "lam \<Rightarrow> int" |
21 height :: "lam \<Rightarrow> int" |
82 *} |
81 *} |
83 |
82 |
84 theorem height_subst: |
83 theorem height_subst: |
85 shows "height (e[x::=e']) \<le> ((height e) - 1) + (height e')" |
84 shows "height (e[x::=e']) \<le> ((height e) - 1) + (height e')" |
86 proof (nominal_induct e avoiding: x e' rule: lam.strong_induct) |
85 proof (nominal_induct e avoiding: x e' rule: lam.strong_induct) |
87 case (1 y) |
86 case (Var y) |
88 have "1 \<le> height e'" by (rule height_ge_one) |
87 have "1 \<le> height e'" by (rule height_ge_one) |
89 then show "height (Var y[x::=e']) \<le> height (Var y) - 1 + height e'" by simp |
88 then show "height (Var y[x::=e']) \<le> height (Var y) - 1 + height e'" by simp |
90 next |
89 next |
91 case (3 y e1) |
90 case (Lam y e1) |
92 have ih: "height (e1[x::=e']) \<le> ((height e1) - 1) + (height e')" by fact |
91 have ih: "height (e1[x::=e']) \<le> ((height e1) - 1) + (height e')" by fact |
93 moreover |
92 moreover |
94 have vc: "atom y \<sharp> x" "atom y \<sharp> e'" by fact+ (* usual variable convention *) |
93 have vc: "atom y \<sharp> x" "atom y \<sharp> e'" by fact+ (* usual variable convention *) |
95 ultimately show "height ((Lam [y].e1)[x::=e']) \<le> height (Lam [y].e1) - 1 + height e'" by simp |
94 ultimately show "height ((Lam [y].e1)[x::=e']) \<le> height (Lam [y].e1) - 1 + height e'" by simp |
96 next |
95 next |
97 case (2 e1 e2) |
96 case (App e1 e2) |
98 have ih1: "height (e1[x::=e']) \<le> ((height e1) - 1) + (height e')" |
97 have ih1: "height (e1[x::=e']) \<le> ((height e1) - 1) + (height e')" |
99 and ih2: "height (e2[x::=e']) \<le> ((height e2) - 1) + (height e')" by fact+ |
98 and ih2: "height (e2[x::=e']) \<le> ((height e2) - 1) + (height e')" by fact+ |
100 then show "height ((App e1 e2)[x::=e']) \<le> height (App e1 e2) - 1 + height e'" by simp |
99 then show "height ((App e1 e2)[x::=e']) \<le> height (App e1 e2) - 1 + height e'" by simp |
101 qed |
100 qed |
102 |
101 |