author | urbanc |
Tue, 06 Mar 2007 15:28:22 +0100 | |
changeset 22418 | 49e2d9744ae1 |
parent 21555 | 229c0158de92 |
child 22829 | f1db55c7534d |
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 |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
21555
diff
changeset
|
3 |
(* Simple problem suggested by D. Wang *) |
19752
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 |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
21555
diff
changeset
|
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 |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
21555
diff
changeset
|
15 |
text {* definition of the height-function on lambda-terms *} |
20396
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
16 |
|
21555 | 17 |
consts |
19752
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
18 |
height :: "lam \<Rightarrow> int" |
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
19 |
|
21555 | 20 |
nominal_primrec |
21 |
"height (Var x) = 1" |
|
22 |
"height (App t1 t2) = (max (height t1) (height t2)) + 1" |
|
23 |
"height (Lam [a].t) = (height t) + 1" |
|
24 |
apply(finite_guess add: perm_int_def)+ |
|
25 |
apply(rule TrueI)+ |
|
26 |
apply(simp add: fresh_int) |
|
27 |
apply(fresh_guess add: perm_int_def)+ |
|
28 |
done |
|
21087 | 29 |
|
21555 | 30 |
text {* definition of capture-avoiding substitution *} |
19752
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
31 |
|
21555 | 32 |
consts |
33 |
subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [100,100,100] 100) |
|
20396
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
34 |
|
21555 | 35 |
nominal_primrec |
36 |
"(Var x)[y::=t'] = (if x=y then t' else (Var x))" |
|
37 |
"(App t1 t2)[y::=t'] = App (t1[y::=t']) (t2[y::=t'])" |
|
38 |
"\<lbrakk>x\<sharp>y; x\<sharp>t'\<rbrakk> \<Longrightarrow> (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])" |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
21555
diff
changeset
|
39 |
apply(finite_guess)+ |
21555 | 40 |
apply(rule TrueI)+ |
41 |
apply(simp add: abs_fresh) |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
21555
diff
changeset
|
42 |
apply(fresh_guess)+ |
20396
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
43 |
done |
19752
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
44 |
|
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
45 |
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
|
46 |
|
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
47 |
lemma height_ge_one: |
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
48 |
shows "1 \<le> (height e)" |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
21555
diff
changeset
|
49 |
by (nominal_induct e rule: lam.induct) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
21555
diff
changeset
|
50 |
(simp | arith)+ |
19752
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
51 |
|
21053 | 52 |
text {* unlike the proplem suggested by Wang, however, the |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
21555
diff
changeset
|
53 |
theorem is here formulated entirely by using |
21555 | 54 |
functions *} |
19752
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
55 |
|
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
56 |
theorem height_subst: |
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
57 |
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
|
58 |
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
|
59 |
case (Var y) |
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
60 |
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
|
61 |
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
|
62 |
next |
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
63 |
case (Lam y e1) |
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
64 |
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
|
65 |
moreover |
21053 | 66 |
have vc: "y\<sharp>x" "y\<sharp>e'" by fact (* usual variable convention *) |
21555 | 67 |
ultimately show "height ((Lam [y].e1)[x::=e']) \<le> height (Lam [y].e1) - 1 + height e'" by simp |
19752
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
68 |
next |
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
69 |
case (App e1 e2) |
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
70 |
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
|
71 |
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
|
72 |
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
|
73 |
qed |
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
74 |
|
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
75 |
end |
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
76 |