author | urbanc |
Wed, 18 Oct 2006 23:15:16 +0200 | |
changeset 21053 | 7d0962594902 |
parent 20398 | 1db76dd407bb |
child 21087 | 3e56528a39f7 |
permissions | -rw-r--r-- |
19752
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
1 |
(* $Id$ *) |
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
2 |
|
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
3 |
(* Simple, but artificial, problem suggested by D. Wang *) |
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
4 |
|
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
5 |
theory Height |
21053 | 6 |
imports "Nominal" |
19752
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
7 |
begin |
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
8 |
|
20396
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
9 |
atom_decl name |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
10 |
|
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
11 |
nominal_datatype lam = Var "name" |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
12 |
| App "lam" "lam" |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
13 |
| Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100) |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
14 |
|
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
15 |
text {* definition of the height-function by "structural recursion" ;o) *} |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
16 |
|
19752
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
17 |
constdefs |
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
18 |
height_Var :: "name \<Rightarrow> int" |
20396
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
19 |
"height_Var \<equiv> \<lambda>_. 1" |
19752
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
20 |
|
20396
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
21 |
height_App :: "lam\<Rightarrow>lam\<Rightarrow>int\<Rightarrow>int\<Rightarrow>int" |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
22 |
"height_App \<equiv> \<lambda>_ _ n1 n2. (max n1 n2)+1" |
19752
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
23 |
|
20396
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
24 |
height_Lam :: "name\<Rightarrow>lam\<Rightarrow>int\<Rightarrow>int" |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
25 |
"height_Lam \<equiv> \<lambda>_ _ n. n+1" |
19752
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
26 |
|
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
27 |
height :: "lam \<Rightarrow> int" |
20398 | 28 |
"height \<equiv> lam_rec height_Var height_App height_Lam" |
19752
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
29 |
|
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
30 |
text {* show that height is a function *} |
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
31 |
lemma fin_supp_height: |
20396
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
32 |
shows "finite ((supp height_Var)::name set)" |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
33 |
and "finite ((supp height_App)::name set)" |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
34 |
and "finite ((supp height_Lam)::name set)" |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
35 |
by (finite_guess add: height_Var_def height_App_def height_Lam_def perm_int_def fs_name1)+ |
19752
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
36 |
|
20396
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
37 |
lemma fcb_height_Lam: |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
38 |
assumes fr: "a\<sharp>height_Lam" |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
39 |
shows "a\<sharp>height_Lam a t n" |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
40 |
apply(simp add: height_Lam_def perm_int_def fresh_def supp_int) |
19752
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
41 |
done |
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
42 |
|
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
43 |
text {* derive the characteristic equations for height from the iteration combinator *} |
21053 | 44 |
lemma height[simp]: |
19752
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
45 |
shows "height (Var c) = 1" |
21053 | 46 |
and "height (App t1 t2) = (max (height t1) (height t2))+1" |
47 |
and "height (Lam [a].t) = (height t)+1" |
|
20398 | 48 |
apply(simp add: height_def) |
49 |
apply(simp add: lam.recs[where P="\<lambda>_. True", simplified, OF fin_supp_height, OF fcb_height_Lam]) |
|
19752
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
50 |
apply(simp add: height_Var_def) |
20398 | 51 |
apply(simp add: height_def) |
52 |
apply(simp add: lam.recs[where P="\<lambda>_. True", simplified, OF fin_supp_height, OF fcb_height_Lam]) |
|
19752
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
53 |
apply(simp add: height_App_def) |
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
54 |
apply(simp add: height_def) |
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
55 |
apply(rule trans) |
20398 | 56 |
apply(rule lam.recs[where P="\<lambda>_. True", simplified, OF fin_supp_height, OF fcb_height_Lam]) |
57 |
apply(assumption) |
|
20396
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
58 |
apply(fresh_guess add: height_Var_def perm_int_def) |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
59 |
apply(fresh_guess add: height_App_def perm_int_def) |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
60 |
apply(fresh_guess add: height_Lam_def perm_int_def) |
19752
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
61 |
apply(simp add: height_Lam_def) |
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
62 |
done |
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
63 |
|
21053 | 64 |
text {* define capture-avoiding substitution *} |
19752
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
65 |
|
20396
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
66 |
constdefs |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
67 |
subst_Var :: "name \<Rightarrow> lam \<Rightarrow> name \<Rightarrow> lam" |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
68 |
"subst_Var x t' \<equiv> \<lambda>y. (if y=x then t' else (Var y))" |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
69 |
|
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
70 |
subst_App :: "name \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam" |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
71 |
"subst_App x t' \<equiv> \<lambda>_ _ r1 r2. App r1 r2" |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
72 |
|
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
73 |
subst_Lam :: "name \<Rightarrow> lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam" |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
74 |
"subst_Lam x t' \<equiv> \<lambda>a _ r. Lam [a].r" |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
75 |
|
21053 | 76 |
subst_lam :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [100,100,100] 100) |
77 |
"t[x::=t'] \<equiv> (lam_rec (subst_Var x t') (subst_App x t') (subst_Lam x t')) t" |
|
20396
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
78 |
|
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
79 |
lemma supports_subst_Var: |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
80 |
shows "((supp (x,t))::name set) supports (subst_Var x t)" |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
81 |
apply(supports_simp add: subst_Var_def) |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
82 |
apply(rule impI) |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
83 |
apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst]) |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
84 |
apply(perm_simp) |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
85 |
done |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
86 |
|
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
87 |
lemma fin_supp_subst: |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
88 |
shows "finite ((supp (subst_Var x t))::name set)" |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
89 |
and "finite ((supp (subst_App x t))::name set)" |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
90 |
and "finite ((supp (subst_Lam x t))::name set)" |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
91 |
proof - |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
92 |
case goal1 |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
93 |
have f: "finite ((supp (x,t))::name set)" by (simp add: fs_name1) |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
94 |
then have "supp (subst_Var x t) \<subseteq> ((supp (x,t))::name set)" |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
95 |
using supp_is_subset[OF supports_subst_Var] by simp |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
96 |
then show "finite ((supp (subst_Var x t))::name set)" using f by (simp add: finite_subset) |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
97 |
qed (finite_guess add: subst_App_def subst_Lam_def fs_name1)+ |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
98 |
|
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
99 |
lemma fcb_subst_Lam: |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
100 |
assumes fr: "a\<sharp>(subst_Lam y t')" |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
101 |
shows "a\<sharp>(subst_Lam y t') a t r" |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
102 |
by (simp add: subst_Lam_def abs_fresh) |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
103 |
|
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
104 |
lemma subst_lam[simp]: |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
105 |
shows "(Var x)[y::=t'] = (if x=y then t' else (Var x))" |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
106 |
and "(App t1 t2)[y::=t'] = App (t1[y::=t']) (t2[y::=t'])" |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
107 |
and "\<lbrakk>a\<sharp>y; a\<sharp>t'\<rbrakk> \<Longrightarrow> (Lam [a].t)[y::=t'] = Lam [a].(t[y::=t'])" |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
108 |
apply(unfold subst_lam_def) |
20398 | 109 |
apply(simp only: lam.recs[where P="\<lambda>_. True", simplified, OF fin_supp_subst, OF fcb_subst_Lam]) |
110 |
apply(simp add: subst_Var_def) |
|
111 |
apply(simp only: lam.recs[where P="\<lambda>_. True", simplified, OF fin_supp_subst, OF fcb_subst_Lam]) |
|
20396
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
112 |
apply(simp only: subst_App_def) |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
113 |
apply(rule trans) |
20398 | 114 |
apply(rule lam.recs[where P="\<lambda>_. True", simplified, OF fin_supp_subst, OF fcb_subst_Lam]) |
20396
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
115 |
apply(assumption) |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
116 |
apply(rule supports_fresh, rule supports_subst_Var, simp add: fs_name1, simp add: fresh_def supp_prod) |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
117 |
apply(fresh_guess add: fresh_prod subst_App_def fs_name1) |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
118 |
apply(fresh_guess add: fresh_prod subst_Lam_def fs_name1) |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
119 |
apply(simp add: subst_Lam_def) |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
120 |
done |
19752
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
121 |
|
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
122 |
text{* the next lemma is needed in the Var-case of the theorem *} |
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
123 |
|
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
124 |
lemma height_ge_one: |
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
125 |
shows "1 \<le> (height e)" |
21053 | 126 |
by (nominal_induct e rule: lam.induct) |
127 |
(simp | arith)+ |
|
19752
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
128 |
|
21053 | 129 |
text {* unlike the proplem suggested by Wang, however, the |
130 |
theorem is formulated here entirely by using functions *} |
|
19752
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
131 |
|
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
132 |
theorem height_subst: |
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
133 |
shows "height (e[x::=e']) \<le> (((height e) - 1) + (height e'))" |
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
134 |
proof (nominal_induct e avoiding: x e' rule: lam.induct) |
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
135 |
case (Var y) |
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
136 |
have "1 \<le> height e'" by (rule height_ge_one) |
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
137 |
then show "height (Var y[x::=e']) \<le> height (Var y) - 1 + height e'" by simp |
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
138 |
next |
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
139 |
case (Lam y e1) |
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
140 |
hence ih: "height (e1[x::=e']) \<le> (((height e1) - 1) + (height e'))" by simp |
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
141 |
moreover |
21053 | 142 |
have vc: "y\<sharp>x" "y\<sharp>e'" by fact (* usual variable convention *) |
19752
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
143 |
ultimately show "height ((Lam [y].e1)[x::=e']) \<le> height (Lam [y].e1) - 1 + height e'" by simp |
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
144 |
next |
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
145 |
case (App e1 e2) |
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
146 |
hence ih1: "height (e1[x::=e']) \<le> (((height e1) - 1) + (height e'))" |
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
147 |
and ih2: "height (e2[x::=e']) \<le> (((height e2) - 1) + (height e'))" by simp_all |
20396
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
148 |
then show "height ((App e1 e2)[x::=e']) \<le> height (App e1 e2) - 1 + height e'" by simp |
19752
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
149 |
qed |
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
150 |
|
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
151 |
end |
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
152 |