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