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