--- a/src/HOL/Nominal/Examples/Height.thy Wed Mar 12 08:47:37 2008 +0100
+++ b/src/HOL/Nominal/Examples/Height.thy Wed Mar 12 11:57:12 2008 +0100
@@ -5,7 +5,7 @@
begin
text {*
- A trivial problem suggested by D. Wang. It shows how
+ A small problem suggested by D. Wang. It shows how
the height of a lambda-terms behaves under substitution.
*}
@@ -17,7 +17,6 @@
| Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
text {* Definition of the height-function on lambda-terms. *}
-
consts
height :: "lam \<Rightarrow> int"
@@ -46,7 +45,7 @@
apply(fresh_guess)+
done
-text{* The next lemma is needed in the Var-case of the theorem. *}
+text{* The next lemma is needed in the Var-case of the theorem below. *}
lemma height_ge_one:
shows "1 \<le> (height e)"
@@ -54,26 +53,46 @@
text {*
Unlike the proplem suggested by Wang, however, the
- theorem is here formulated entirely by using functions.
+ theorem is here formulated entirely by using functions.
*}
theorem height_subst:
- shows "height (e[x::=e']) \<le> (((height e) - 1) + (height e'))"
+ shows "height (e[x::=e']) \<le> ((height e) - 1) + (height e')"
proof (nominal_induct e avoiding: x e' rule: lam.induct)
case (Var y)
have "1 \<le> height e'" by (rule height_ge_one)
then show "height (Var y[x::=e']) \<le> height (Var y) - 1 + height e'" by simp
next
case (Lam y e1)
- hence ih: "height (e1[x::=e']) \<le> (((height e1) - 1) + (height e'))" by simp
+ hence ih: "height (e1[x::=e']) \<le> ((height e1) - 1) + (height e')" by simp
moreover
have vc: "y\<sharp>x" "y\<sharp>e'" by fact+ (* usual variable convention *)
ultimately show "height ((Lam [y].e1)[x::=e']) \<le> height (Lam [y].e1) - 1 + height e'" by simp
next
case (App e1 e2)
- hence ih1: "height (e1[x::=e']) \<le> (((height e1) - 1) + (height e'))"
- and ih2: "height (e2[x::=e']) \<le> (((height e2) - 1) + (height e'))" by simp_all
+ hence ih1: "height (e1[x::=e']) \<le> ((height e1) - 1) + (height e')"
+ and ih2: "height (e2[x::=e']) \<le> ((height e2) - 1) + (height e')" by simp_all
then show "height ((App e1 e2)[x::=e']) \<le> height (App e1 e2) - 1 + height e'" by simp
qed
+theorem height_subst:
+ shows "height (e[x::=e']) \<le> ((height e) - 1) + (height e')"
+proof (nominal_induct e avoiding: x e' rule: lam.induct)
+ case (Var y)
+ have "1 \<le> height e'" by (rule height_ge_one)
+ then show "height (Var y[x::=e']) \<le> height (Var y) - 1 + height e'" by simp
+next
+ case (Lam y e1)
+ hence ih: "height (e1[x::=e']) \<le> ((height e1) - 1) + (height e')" by simp
+ moreover
+ have vc: "y\<sharp>x" "y\<sharp>e'" by fact+ (* usual variable convention *)
+ ultimately show "height ((Lam [y].e1)[x::=e']) \<le> height (Lam [y].e1) - 1 + height e'" by simp
+next
+ case (App e1 e2)
+ hence ih1: "height (e1[x::=e']) \<le> ((height e1) - 1) + (height e')"
+ and ih2: "height (e2[x::=e']) \<le> ((height e2) - 1) + (height e')" by simp_all
+ then show "height ((App e1 e2)[x::=e']) \<le> height (App e1 e2) - 1 + height e'" by simp
+qed
+
+
end
--- a/src/HOL/Nominal/Examples/Support.thy Wed Mar 12 08:47:37 2008 +0100
+++ b/src/HOL/Nominal/Examples/Support.thy Wed Mar 12 11:57:12 2008 +0100
@@ -9,11 +9,10 @@
x\<sharp>(A \<union> B) does not imply x\<sharp>A and x\<sharp>B
- with A and B being sets. For this we set A to the set of
- even atoms and B to the set of odd atoms. Then A \<union> B, that
- is the set of all atoms, has empty support. The sets A,
- respectively B, however have the set of all atoms as
- their support.
+ For this we set A to the set of even atoms and B to
+ the set of odd atoms. Then A \<union> B, that is the set of
+ all atoms, has empty support. The sets A, respectively B,
+ however have the set of all atoms as their support.
*}
atom_decl atom
@@ -38,7 +37,7 @@
text {*
The union of even and odd atoms is the set of all atoms.
- Unfortunately I do not know a simpler proof of this fact. *}
+ (Unfortunately I do not know a simpler proof of this fact.) *}
lemma EVEN_union_ODD:
shows "EVEN \<union> ODD = UNIV"
using even_or_odd
@@ -84,7 +83,7 @@
qed
text {*
- A general fact about a set S of names that is both infinite and
+ A general fact about a set S of atoms that is both infinite and
coinfinite. Then S has all atoms as its support. Steve Zdancewick
helped with proving this fact. *}
--- a/src/HOL/Nominal/Examples/VC_Condition.thy Wed Mar 12 08:47:37 2008 +0100
+++ b/src/HOL/Nominal/Examples/VC_Condition.thy Wed Mar 12 11:57:12 2008 +0100
@@ -5,7 +5,7 @@
begin
text {*
- We give here two examples that show if we use the variable
+ We give here two examples showing that if we use the variable
convention carelessly in rule inductions, we might end
up with faulty lemmas. The point is that the examples
are not variable-convention compatible and therefore in the
@@ -109,7 +109,7 @@
text {*
Now comes the first faulty lemma. It is derived using the
variable convention (i.e. our strong induction principle).
- This faulty lemma states that if t unbinds to x::xs and t',
+ This faulty lemma states that if t unbinds to x#xs and t',
and x is a free variable in t', then it is also a free
variable in bind xs t'. We show this lemma by assuming that
the binder x is fresh w.r.t. to the xs unbound previously. *}
@@ -183,30 +183,27 @@
then show "False" by (simp add: fresh_atm)
qed
-text {*
- Moral: Who would have thought that the variable convention
- is in general an unsound reasoning principle.
- *}
-
-
-text
- {* BTW: A similar effect can be achieved by using naive (that
- is strong) inversion rules. *}
+text {* A similar effect can be achieved by using naive inversion
+ on rules. *}
lemma false3:
shows "False"
proof -
have "Lam [x].(Var x) \<rightarrow> (Var x)" by (auto intro: strip.intros)
- moreover obtain y::name where y: "y\<sharp>x"
- by (rule exists_fresh) (rule fin_supp)
+ moreover obtain y::"name" where fc: "y\<sharp>x" by (rule exists_fresh) (rule fin_supp)
then have "Lam [x].(Var x) = Lam [y].(Var y)"
by (simp add: lam.inject alpha calc_atm fresh_atm)
ultimately have "Lam [y].(Var y) \<rightarrow> (Var x)" by simp
- then have "Var y \<rightarrow> Var x" using y
- by (cases rule: strip.strong_cases [where x=y])
+ then have "Var y \<rightarrow> Var x" using fc
+ by (cases rule: strip.strong_cases[where x=y])
(simp_all add: lam.inject alpha abs_fresh)
- then show "False" using y
+ then show "False" using fc
by (cases) (simp_all add: lam.inject fresh_atm)
qed
+text {*
+ Moral: Who would have thought that the variable convention
+ is in general an unsound reasoning principle.
+ *}
+
end
\ No newline at end of file
--- a/src/HOL/Nominal/Examples/Weakening.thy Wed Mar 12 08:47:37 2008 +0100
+++ b/src/HOL/Nominal/Examples/Weakening.thy Wed Mar 12 11:57:12 2008 +0100
@@ -150,8 +150,10 @@
oops
text{*
- To show that the proof is not simple, here proof without using
- the variable convention.
+ To show that the proof with explicit renaming is not simple,
+ here is the proof without using the variable convention. It
+ crucially depends on the equivariance property of the typing
+ relation.
*}
@@ -197,7 +199,7 @@
then show "\<Gamma>2 \<turnstile> Lam [c].([(c,x)]\<bullet>t) : T1 \<rightarrow> T2" using fc1 by auto
qed
ultimately show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" by simp
-qed (auto)
+qed (auto) (* var and app cases *)
text {*
Moral: compare the proof with explicit renamings to weakening_version1