--- a/Tutorial/Lambda.thy	Thu Feb 03 02:57:04 2011 +0000
+++ b/Tutorial/Lambda.thy	Fri Feb 04 03:52:38 2011 +0000
@@ -38,12 +38,38 @@
   "height (Var x) = 1"
 | "height (App t1 t2) = max (height t1) (height t2) + 1"
 | "height (Lam [x].t) = height t + 1"
+apply(subgoal_tac "\<And>p x r. height_graph x r \<Longrightarrow> height_graph (p \<bullet> x) (p \<bullet> r)") 
+unfolding eqvt_def
+apply(rule allI)
+apply(simp add: permute_fun_def)
+apply(rule ext)
+apply(rule ext)
+apply(simp add: permute_bool_def)
+apply(rule iffI)
+apply(drule_tac x="p" in meta_spec)
+apply(drule_tac x="- p \<bullet> x" in meta_spec)
+apply(drule_tac x="- p \<bullet> xa" in meta_spec)
+apply(simp)
+apply(drule_tac x="-p" in meta_spec)
+apply(drule_tac x="x" in meta_spec)
+apply(drule_tac x="xa" in meta_spec)
+apply(simp)
+apply(erule height_graph.induct)
+apply(perm_simp)
+apply(rule height_graph.intros)
+apply(perm_simp)
+apply(rule height_graph.intros)
+apply(assumption)
+apply(assumption)
+apply(perm_simp)
+apply(rule height_graph.intros)
+apply(assumption)
 apply(rule_tac y="x" in lam.exhaust)
 apply(auto simp add: lam.distinct lam.eq_iff)
 apply(simp add: Abs_eq_iff alphas)
 apply(clarify)
 apply(subst (4) supp_perm_eq[where p="p", symmetric])
-apply(simp add: pure_supp fresh_star_def)
+apply(simp add: pure_supp  fresh_star_def)
 apply(simp add: eqvt_at_def)
 done
 
@@ -59,6 +85,33 @@
   "(Var x)[y ::= s] = (if x = y then s else (Var x))"
 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])"
 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])"
+apply(subgoal_tac "\<And>p x r. subst_graph x r \<Longrightarrow> subst_graph (p \<bullet> x) (p \<bullet> r)") 
+unfolding eqvt_def
+apply(rule allI)
+apply(simp add: permute_fun_def)
+apply(rule ext)
+apply(rule ext)
+apply(simp add: permute_bool_def)
+apply(rule iffI)
+apply(drule_tac x="p" in meta_spec)
+apply(drule_tac x="- p \<bullet> x" in meta_spec)
+apply(drule_tac x="- p \<bullet> xa" in meta_spec)
+apply(simp)
+apply(drule_tac x="-p" in meta_spec)
+apply(drule_tac x="x" in meta_spec)
+apply(drule_tac x="xa" in meta_spec)
+apply(simp)
+apply(erule subst_graph.induct)
+apply(perm_simp)
+apply(rule subst_graph.intros)
+apply(perm_simp)
+apply(rule subst_graph.intros)
+apply(assumption)
+apply(assumption)
+apply(perm_simp)
+apply(rule subst_graph.intros)
+apply(simp add: fresh_Pair)
+apply(assumption)
 apply(auto simp add: lam.distinct lam.eq_iff)
 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)
 apply(blast)+