--- a/Tutorial/Lambda.thy	Wed Feb 29 17:14:31 2012 +0000
+++ b/Tutorial/Lambda.thy	Mon Mar 05 16:27:28 2012 +0000
@@ -15,7 +15,7 @@
 nominal_datatype lam =
   Var "name"
 | App "lam" "lam"
-| Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100)
+| Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100)
 
 
 text {* some automatically derived theorems *}
@@ -38,43 +38,17 @@
   "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(simp add: eqvt_def height_graph_def)
+apply (rule, perm_simp, rule)
+apply(rule TrueI)
 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: eqvt_at_def)
+apply(auto)
+apply(erule_tac c="()" in Abs_lst1_fcb2)
+apply(simp_all add: fresh_def pure_supp eqvt_at_def fresh_star_def)
 done
 
-termination
-  by (relation "measure size") (simp_all add: lam.size)
+termination (eqvt)
+  by lexicographic_order
   
 
 subsection {* Capture-Avoiding Substitution *}
@@ -85,78 +59,22 @@
   "(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)+
-apply(simp add: fresh_star_def)
-apply(subgoal_tac "atom xa \<sharp> [[atom x]]lst. t \<and> atom x \<sharp> [[atom xa]]lst. ta")
-apply(subst (asm) Abs_eq_iff2)
-apply(simp add: alphas atom_eqvt)
-apply(clarify)
-apply(rule trans)
-apply(rule_tac p="p" in supp_perm_eq[symmetric])
-apply(rule fresh_star_supp_conv)
-apply(drule fresh_star_perm_set_conv)
-apply(simp add: finite_supp)
-apply(subgoal_tac "{atom (p \<bullet> x), atom x} \<sharp>* ([[atom x]]lst. subst_sumC (t, ya, sa))")
-apply(auto simp add: fresh_star_def)[1]
-apply(simp (no_asm) add: fresh_star_def)
-apply(rule conjI)
-apply(simp (no_asm) add: Abs_fresh_iff)
-apply(clarify)
-apply(drule_tac a="atom (p \<bullet> x)" in fresh_eqvt_at)
-apply(simp add: finite_supp)
-apply(simp (no_asm_use) add: fresh_Pair)
-apply(simp add: Abs_fresh_iff)
-apply(simp)
-apply(simp add: Abs_fresh_iff)
-apply(subgoal_tac "p \<bullet> ya = ya")
-apply(subgoal_tac "p \<bullet> sa = sa")
-apply(simp add: atom_eqvt eqvt_at_def)
-apply(rule perm_supp_eq)
-apply(auto simp add: fresh_star_def fresh_Pair)[1]
-apply(rule perm_supp_eq)
-apply(auto simp add: fresh_star_def fresh_Pair)[1]
-apply(rule conjI)
-apply(simp add: Abs_fresh_iff)
-apply(drule sym)
-apply(simp add: Abs_fresh_iff)
+  unfolding eqvt_def subst_graph_def
+  apply(rule, perm_simp, rule)
+  apply(rule TrueI)
+  apply(auto)
+  apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)
+  apply(blast)+
+  apply(simp_all add: fresh_star_def fresh_Pair_elim)
+  apply(erule_tac c="(ya,sa)" in Abs_lst1_fcb2)
+  apply(simp_all add: Abs_fresh_iff)
+  apply(simp add: fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 done
 
-termination
-  by (relation "measure (\<lambda>(t, _, _). size t)")
-     (simp_all add: lam.size)
-
-lemma subst_eqvt[eqvt]:
-  shows "(p \<bullet> t[x ::= s]) = (p \<bullet> t)[(p \<bullet> x) ::= (p \<bullet> s)]"
-by (induct t x s rule: subst.induct) (simp_all)
+termination (eqvt)
+  by lexicographic_order
 
 lemma fresh_fact:
   assumes a: "atom z \<sharp> s"