1 (* $Id$ *) |
1 (* $Id$ *) |
2 |
2 |
3 (* Simple, but artificial, problem suggested by D. Wang *) |
3 (* Simple problem suggested by D. Wang *) |
4 |
4 |
5 theory Height |
5 theory Height |
6 imports "Nominal" |
6 imports "../Nominal" |
7 begin |
7 begin |
8 |
8 |
9 atom_decl name |
9 atom_decl name |
10 |
10 |
11 nominal_datatype lam = Var "name" |
11 nominal_datatype lam = Var "name" |
12 | App "lam" "lam" |
12 | App "lam" "lam" |
13 | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100) |
13 | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100) |
14 |
14 |
15 text {* definition of the height-function *} |
15 text {* definition of the height-function on lambda-terms *} |
16 |
16 |
17 consts |
17 consts |
18 height :: "lam \<Rightarrow> int" |
18 height :: "lam \<Rightarrow> int" |
19 |
19 |
20 nominal_primrec |
20 nominal_primrec |
27 apply(fresh_guess add: perm_int_def)+ |
27 apply(fresh_guess add: perm_int_def)+ |
28 done |
28 done |
29 |
29 |
30 text {* definition of capture-avoiding substitution *} |
30 text {* definition of capture-avoiding substitution *} |
31 |
31 |
32 lemma eq_eqvt: |
|
33 fixes pi::"name prm" |
|
34 and x::"'a::pt_name" |
|
35 shows "pi\<bullet>(x=y) = ((pi\<bullet>x)=(pi\<bullet>y))" |
|
36 apply(simp add: perm_bool perm_bij) |
|
37 done |
|
38 |
|
39 consts |
32 consts |
40 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [100,100,100] 100) |
33 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [100,100,100] 100) |
41 |
34 |
42 nominal_primrec |
35 nominal_primrec |
43 "(Var x)[y::=t'] = (if x=y then t' else (Var x))" |
36 "(Var x)[y::=t'] = (if x=y then t' else (Var x))" |
44 "(App t1 t2)[y::=t'] = App (t1[y::=t']) (t2[y::=t'])" |
37 "(App t1 t2)[y::=t'] = App (t1[y::=t']) (t2[y::=t'])" |
45 "\<lbrakk>x\<sharp>y; x\<sharp>t'\<rbrakk> \<Longrightarrow> (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])" |
38 "\<lbrakk>x\<sharp>y; x\<sharp>t'\<rbrakk> \<Longrightarrow> (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])" |
46 apply(finite_guess add: eq_eqvt perm_if fs_name1)+ |
39 apply(finite_guess)+ |
47 apply(rule TrueI)+ |
40 apply(rule TrueI)+ |
48 apply(simp add: abs_fresh) |
41 apply(simp add: abs_fresh) |
49 apply(fresh_guess add: eq_eqvt perm_if fs_name1)+ |
42 apply(fresh_guess)+ |
50 done |
43 done |
51 |
44 |
52 text{* the next lemma is needed in the Var-case of the theorem *} |
45 text{* the next lemma is needed in the Var-case of the theorem *} |
53 |
46 |
54 lemma height_ge_one: |
47 lemma height_ge_one: |
55 shows "1 \<le> (height e)" |
48 shows "1 \<le> (height e)" |
56 by (nominal_induct e rule: lam.induct) |
49 by (nominal_induct e rule: lam.induct) |
57 (simp | arith)+ |
50 (simp | arith)+ |
58 |
51 |
59 text {* unlike the proplem suggested by Wang, however, the |
52 text {* unlike the proplem suggested by Wang, however, the |
60 theorem is here formulated here entirely by using |
53 theorem is here formulated entirely by using |
61 functions *} |
54 functions *} |
62 |
55 |
63 theorem height_subst: |
56 theorem height_subst: |
64 shows "height (e[x::=e']) \<le> (((height e) - 1) + (height e'))" |
57 shows "height (e[x::=e']) \<le> (((height e) - 1) + (height e'))" |
65 proof (nominal_induct e avoiding: x e' rule: lam.induct) |
58 proof (nominal_induct e avoiding: x e' rule: lam.induct) |