author wenzelm Mon, 14 Apr 2008 21:44:53 +0200 changeset 26648 25c07f3878b0 parent 26647 147c920ed5f7 child 26649 a053f13bc9da
removed duplicate lemmas;
```--- a/src/HOL/Nominal/Examples/Class.thy	Mon Apr 14 21:44:53 2008 +0200
+++ b/src/HOL/Nominal/Examples/Class.thy	Mon Apr 14 21:44:53 2008 +0200
@@ -5244,10 +5244,6 @@
shows "M \<longrightarrow>\<^isub>a* M'"
using a by blast

-lemma a_star_refl:
-  shows "M \<longrightarrow>\<^isub>a* M"
-  by blast
-
lemma a_starE:
assumes a: "M \<longrightarrow>\<^isub>a* M'"
shows "M = M' \<or> (\<exists>N. M \<longrightarrow>\<^isub>a N \<and> N \<longrightarrow>\<^isub>a* M')"```
```--- a/src/HOL/Nominal/Examples/Height.thy	Mon Apr 14 21:44:53 2008 +0200
+++ b/src/HOL/Nominal/Examples/Height.thy	Mon Apr 14 21:44:53 2008 +0200
@@ -75,24 +75,4 @@
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```