author | wenzelm |
Thu, 14 Jun 2018 17:50:23 +0200 | |
changeset 68449 | 6d0f1a5a16ea |
parent 66453 | cc19f7ca2ed6 |
child 80914 | d97fdabd9e2b |
permissions | -rw-r--r-- |
25751 | 1 |
theory Height |
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
63167
diff
changeset
|
2 |
imports "HOL-Nominal.Nominal" |
25751 | 3 |
begin |
19752
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
4 |
|
63167 | 5 |
text \<open> |
26262 | 6 |
A small problem suggested by D. Wang. It shows how |
25751 | 7 |
the height of a lambda-terms behaves under substitution. |
63167 | 8 |
\<close> |
19752
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
9 |
|
20396
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
10 |
atom_decl name |
4d0c33719348
used the recursion combinator for the height and substitution function
urbanc
parents:
19752
diff
changeset
|
11 |
|
22829
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
22418
diff
changeset
|
12 |
nominal_datatype lam = |
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
22418
diff
changeset
|
13 |
Var "name" |
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
22418
diff
changeset
|
14 |
| App "lam" "lam" |
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
22418
diff
changeset
|
15 |
| 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
|
16 |
|
63167 | 17 |
text \<open>Definition of the height-function on lambda-terms.\<close> |
19752
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
18 |
|
21555 | 19 |
nominal_primrec |
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
26966
diff
changeset
|
20 |
height :: "lam \<Rightarrow> int" |
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
26966
diff
changeset
|
21 |
where |
21555 | 22 |
"height (Var x) = 1" |
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
26966
diff
changeset
|
23 |
| "height (App t1 t2) = (max (height t1) (height t2)) + 1" |
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
26966
diff
changeset
|
24 |
| "height (Lam [a].t) = (height t) + 1" |
21555 | 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 |
|
63167 | 31 |
text \<open>Definition of capture-avoiding substitution.\<close> |
19752
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
32 |
|
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
26966
diff
changeset
|
33 |
nominal_primrec |
21555 | 34 |
subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [100,100,100] 100) |
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
26966
diff
changeset
|
35 |
where |
21555 | 36 |
"(Var x)[y::=t'] = (if x=y then t' else (Var x))" |
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
26966
diff
changeset
|
37 |
| "(App t1 t2)[y::=t'] = App (t1[y::=t']) (t2[y::=t'])" |
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
26966
diff
changeset
|
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 |
|
63167 | 45 |
text\<open>The next lemma is needed in the Var-case of the theorem below.\<close> |
19752
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)" |
26966
071f40487734
made the naming of the induction principles consistent: weak_induct is
urbanc
parents:
26648
diff
changeset
|
49 |
by (nominal_induct e rule: lam.strong_induct) (simp_all) |
19752
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
50 |
|
63167 | 51 |
text \<open> |
25751 | 52 |
Unlike the proplem suggested by Wang, however, the |
26262 | 53 |
theorem is here formulated entirely by using functions. |
63167 | 54 |
\<close> |
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: |
26262 | 57 |
shows "height (e[x::=e']) \<le> ((height e) - 1) + (height e')" |
26966
071f40487734
made the naming of the induction principles consistent: weak_induct is
urbanc
parents:
26648
diff
changeset
|
58 |
proof (nominal_induct e avoiding: x e' rule: lam.strong_induct) |
19752
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) |
26262 | 64 |
hence ih: "height (e1[x::=e']) \<le> ((height e1) - 1) + (height e')" by simp |
19752
18e5aa65fb8b
added an example suggested by D. Wang on the PoplMark-mailing list;
urbanc
parents:
diff
changeset
|
65 |
moreover |
23393 | 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) |
26262 | 70 |
hence ih1: "height (e1[x::=e']) \<le> ((height e1) - 1) + (height e')" |
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 |