1 theory Height |
1 theory Height |
2 imports "../Nominal2" |
2 imports "Lambda" |
3 begin |
3 begin |
4 |
4 |
5 text {* |
5 text {* |
6 A small problem suggested by D. Wang. It shows how |
6 A small problem suggested by D. Wang. It shows how |
7 the height of a lambda-terms behaves under substitution. |
7 the height of a lambda-terms behaves under substitution. |
8 *} |
8 *} |
9 |
9 |
10 atom_decl name |
|
11 |
|
12 nominal_datatype lam = |
|
13 Var "name" |
|
14 | App "lam" "lam" |
|
15 | Lam x::"name" l::"lam" bind x in l ("Lam [_]._" [100,100] 100) |
|
16 |
|
17 |
|
18 text {* Definition of the height-function on lambda-terms. *} |
|
19 |
|
20 function |
|
21 height :: "lam \<Rightarrow> int" |
|
22 where |
|
23 "height (Var x) = 1" |
|
24 | "height (App t1 t2) = (max (height t1) (height t2)) + 1" |
|
25 | "height (Lam [a].t) = (height t) + 1" |
|
26 apply(rule_tac y="x" in lam.exhaust) |
|
27 apply(simp_all)[3] |
|
28 apply(simp add: lam.eq_iff) |
|
29 apply(simp add: lam.distinct) |
|
30 apply(simp add: lam.distinct) |
|
31 apply(simp add: lam.eq_iff) |
|
32 apply(simp add: lam.distinct) |
|
33 apply(simp add: lam.eq_iff) |
|
34 sorry |
|
35 |
|
36 termination |
|
37 apply(relation "measure size") |
|
38 apply(simp_all add: lam.size) |
|
39 done |
|
40 |
|
41 text {* Definition of capture-avoiding substitution. *} |
|
42 |
|
43 function |
|
44 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [100,100,100] 100) |
|
45 where |
|
46 "(Var x)[y::=t'] = (if x=y then t' else (Var x))" |
|
47 | "(App t1 t2)[y::=t'] = App (t1[y::=t']) (t2[y::=t'])" |
|
48 | "\<lbrakk>atom x \<sharp> y; atom x \<sharp> t'\<rbrakk> \<Longrightarrow> (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])" |
|
49 apply(case_tac x) |
|
50 apply(simp) |
|
51 apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust) |
|
52 apply(simp_all)[3] |
|
53 apply(blast) |
|
54 apply(blast) |
|
55 apply(simp add: fresh_star_def fresh_Pair) |
|
56 apply(blast) |
|
57 apply(simp add: lam.eq_iff) |
|
58 apply(simp add: lam.distinct) |
|
59 apply(simp add: lam.distinct) |
|
60 apply(simp add: lam.eq_iff) |
|
61 apply(simp add: lam.distinct) |
|
62 apply(simp add: lam.eq_iff) |
|
63 sorry |
|
64 |
|
65 termination |
|
66 apply(relation "measure (size o fst)") |
|
67 apply(simp_all add: lam.size) |
|
68 done |
|
69 |
|
70 text{* The next lemma is needed in the Var-case of the theorem below. *} |
|
71 |
10 |
72 lemma height_ge_one: |
11 lemma height_ge_one: |
73 shows "1 \<le> (height e)" |
12 shows "1 \<le> (height e)" |
74 apply(nominal_induct e rule: lam.strong_induct) |
13 by (induct e rule: lam.induct) |
75 apply(simp_all) |
14 (simp_all) |
76 done |
|
77 |
|
78 text {* |
|
79 Unlike the proplem suggested by Wang, however, the |
|
80 theorem is here formulated entirely by using functions. |
|
81 *} |
|
82 |
15 |
83 theorem height_subst: |
16 theorem height_subst: |
84 shows "height (e[x::=e']) \<le> ((height e) - 1) + (height e')" |
17 shows "height (e[x::=e']) \<le> height e - 1 + height e'" |
85 proof (nominal_induct e avoiding: x e' rule: lam.strong_induct) |
18 proof (nominal_induct e avoiding: x e' rule: lam.strong_induct) |
86 case (Var y) |
19 case (Var y) |
87 have "1 \<le> height e'" by (rule height_ge_one) |
20 have "1 \<le> height e'" using height_ge_one by simp |
88 then show "height (Var y[x::=e']) \<le> height (Var y) - 1 + height e'" by simp |
21 then show "height (Var y[x::=e']) \<le> height (Var y) - 1 + height e'" by simp |
89 next |
22 next |
90 case (Lam y e1) |
23 case (Lam y e1) |
91 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 |
92 moreover |
25 moreover |
93 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 *) |
94 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 |
95 next |
28 next |
96 case (App e1 e2) |
29 case (App e1 e2) |
97 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'" |
98 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+ |
99 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 |
100 qed |
33 qed |
101 |
34 |
102 end |
35 end |