# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1344362092 -3600
# Node ID 25d11b449e920f48d531851a2c84d6a85d43b29a
# Parent  ca6ca6fc28afc7527d16276a69a2574e34c13549
definition of an auxiliary graph in nominal-primrec definitions

diff -r ca6ca6fc28af -r 25d11b449e92 Nominal/Ex/CPS/CPS1_Plotkin.thy
--- a/Nominal/Ex/CPS/CPS1_Plotkin.thy	Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/Ex/CPS/CPS1_Plotkin.thy	Tue Aug 07 18:54:52 2012 +0100
@@ -10,8 +10,8 @@
 | "atom k \<sharp> (x, M) \<Longrightarrow> (Lam x M)* = Lam k (k~ $$ Lam x (M*))"
 | "atom k \<sharp> (M, N) \<Longrightarrow> atom m \<sharp> (N, k) \<Longrightarrow> atom n \<sharp> (k, m) \<Longrightarrow>
     (M $$ N)* = Lam k (M* $$ Lam m (N* $$ Lam n (m~ $$ n~ $$ k~)))"
-unfolding eqvt_def CPS_graph_def
-apply (rule, perm_simp, rule, rule)
+unfolding eqvt_def CPS_graph_aux_def
+apply (simp)
 using [[simproc del: alpha_lst]]
 apply (simp_all add: fresh_Pair_elim)
 apply (rule_tac y="x" in lt.exhaust)
@@ -80,8 +80,9 @@
   "(Var x)+ = Var x"
 | "(Lam x M)+ = Lam x (M*)"
 | "(M $$ N)+ = M $$ N"
-  unfolding convert_graph_def eqvt_def
-  apply (rule, perm_simp, rule, rule)
+  unfolding convert_graph_aux_def eqvt_def
+  apply (simp)
+  apply(rule TrueI)
   apply (erule lt.exhaust)
   using [[simproc del: alpha_lst]]
   apply (simp_all)
@@ -114,8 +115,8 @@
     Kapply (M $$ N) K = N; (Lam n (M+ $$ Var n $$ K))"
 | "\<not>isValue M \<Longrightarrow> atom m \<sharp> N \<Longrightarrow> atom m \<sharp> K \<Longrightarrow> atom n \<sharp> m \<Longrightarrow> atom n \<sharp> K \<Longrightarrow>
     Kapply (M $$ N) K = M; (Lam m (N*  $$ (Lam n (Var m $$ Var n $$ K))))"
-  unfolding Kapply_graph_def eqvt_def
-  apply (rule, perm_simp, rule, rule)
+  unfolding Kapply_graph_aux_def eqvt_def
+  apply (simp)
 using [[simproc del: alpha_lst]]
 apply (simp_all)
 apply (case_tac x)
diff -r ca6ca6fc28af -r 25d11b449e92 Nominal/Ex/CPS/CPS2_DanvyNielsen.thy
--- a/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy	Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy	Tue Aug 07 18:54:52 2012 +0100
@@ -16,8 +16,8 @@
 | fill_fun  : "(CFun C N)<M> = (C<M>) $$ N"
 | fill_arg  : "(CArg N C)<M> = N $$ (C<M>)"
 | fill_abs  : "atom x \<sharp> M \<Longrightarrow> (CAbs x C)<M> = Lam x (C<M>)"
-  unfolding eqvt_def fill_graph_def
-  apply perm_simp
+  unfolding eqvt_def fill_graph_aux_def
+  apply simp
   using [[simproc del: alpha_lst]]
   apply auto
   apply (rule_tac y="a" and c="b" in cpsctxt.strong_exhaust)
@@ -41,8 +41,8 @@
 | "atom x \<sharp> C' \<Longrightarrow> ccomp (CAbs x C) C' = CAbs x (ccomp C C')"
 | "ccomp (CArg N C) C' = CArg N (ccomp C C')"
 | "ccomp (CFun C N) C'  = CFun (ccomp C C') N"
-  unfolding eqvt_def ccomp_graph_def
-  apply perm_simp
+  unfolding eqvt_def ccomp_graph_aux_def
+  apply simp
   using [[simproc del: alpha_lst]]
   apply auto
   apply (rule_tac y="a" and c="b" in cpsctxt.strong_exhaust)
diff -r ca6ca6fc28af -r 25d11b449e92 Nominal/Ex/CPS/CPS3_DanvyFilinski.thy
--- a/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy	Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy	Tue Aug 07 18:54:52 2012 +0100
@@ -13,8 +13,7 @@
 | "(x~)^l = l $$ (x~)"
 | "(M$$N)^l = M*(%m. (N*(%n.((m $$ n) $$ l))))"
 | "atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)^l = l $$ (Lam x (Lam c (M^(c~))))"
-  apply (simp only: eqvt_def CPS1_CPS2_graph_def)
-  apply (rule, perm_simp, rule)
+  apply (simp add: eqvt_def CPS1_CPS2_graph_aux_def)
   using [[simproc del: alpha_lst]]
   apply auto
   apply (case_tac x)
diff -r ca6ca6fc28af -r 25d11b449e92 Nominal/Ex/CPS/CPS3_DanvyFilinski_FCB2.thy
--- a/Nominal/Ex/CPS/CPS3_DanvyFilinski_FCB2.thy	Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski_FCB2.thy	Tue Aug 07 18:54:52 2012 +0100
@@ -15,8 +15,7 @@
 | "(x~)^l = l $$ (x~)"
 | "(M $$ N)^l = M*(%m. (N*(%n.((m $$ n) $$ l))))"
 | "atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)^l = l $$ (Lam x (Lam c (M^(c~))))"
-  apply (simp only: eqvt_def CPS1_CPS2_graph_def)
-  apply (rule, perm_simp, rule)
+  apply (simp add: eqvt_def CPS1_CPS2_graph_aux_def)
   apply (auto simp only:)
   apply (case_tac x)
   apply (case_tac a)
diff -r ca6ca6fc28af -r 25d11b449e92 Nominal/Ex/CPS/Lt.thy
--- a/Nominal/Ex/CPS/Lt.thy	Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/Ex/CPS/Lt.thy	Tue Aug 07 18:54:52 2012 +0100
@@ -16,7 +16,7 @@
   "(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])"
-  unfolding eqvt_def subst_graph_def
+  unfolding eqvt_def subst_graph_aux_def
   apply (simp)
   apply(rule TrueI)
   using [[simproc del: alpha_lst]]
@@ -51,8 +51,8 @@
   "isValue (Var x) = True"
 | "isValue (Lam y N) = True"
 | "isValue (A $$ B) = False"
-  unfolding eqvt_def isValue_graph_def
-  by (perm_simp, auto)
+  unfolding eqvt_def isValue_graph_aux_def
+  by (auto)
      (erule lt.exhaust, auto)
 
 termination (eqvt)
diff -r ca6ca6fc28af -r 25d11b449e92 Nominal/Ex/Classical.thy
--- a/Nominal/Ex/Classical.thy	Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/Ex/Classical.thy	Tue Aug 07 18:54:52 2012 +0100
@@ -67,7 +67,7 @@
           (if b=d then ImpR (x).<a>.(M[d\<turnstile>c>e]) e else ImpR (x).<a>.(M[d\<turnstile>c>e]) b)"
 | "atom a \<sharp> (d, e) \<Longrightarrow> (ImpL <a>.M (x).N y)[d\<turnstile>c>e] = ImpL <a>.(M[d\<turnstile>c>e]) (x).(N[d\<turnstile>c>e]) y"
   apply(simp only: eqvt_def)
-  apply(simp only: crename_graph_def)
+  apply(simp only: crename_graph_aux_def)
   apply (rule, perm_simp, rule)
   apply(rule TrueI)
   -- "covered all cases"
@@ -272,7 +272,7 @@
 | "atom x \<sharp> (u, v) \<Longrightarrow> (ImpL <a>.M (x).N y)[u\<turnstile>n>v] = 
         (if y=u then ImpL <a>.(M[u\<turnstile>n>v]) (x).(N[u\<turnstile>n>v]) v else ImpL <a>.(M[u\<turnstile>n>v]) (x).(N[u\<turnstile>n>v]) y)"
   apply(simp only: eqvt_def)
-  apply(simp only: nrename_graph_def)
+  apply(simp only: nrename_graph_aux_def)
   apply (rule, perm_simp, rule)
   apply(rule TrueI)
   -- "covered all cases"
@@ -474,7 +474,7 @@
      (if y=z then Cut <c>.P (z').ImpL <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}) z' 
       else ImpL <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}) z)"
   apply(simp only: eqvt_def)
-  apply(simp only: substn_graph_def)
+  apply(simp only: substn_graph_aux_def)
   apply (rule, perm_simp, rule)
   apply(rule TrueI)
   -- "covered all cases"
diff -r ca6ca6fc28af -r 25d11b449e92 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/Ex/Lambda.thy	Tue Aug 07 18:54:52 2012 +0100
@@ -7,7 +7,6 @@
 
 atom_decl name
 
-
 ML {* trace := true *}
 
 nominal_datatype lam =
@@ -39,7 +38,7 @@
   "is_app (Var x) = False"
 | "is_app (App t1 t2) = True"
 | "is_app (Lam [x]. t) = False"
-apply(simp add: eqvt_def is_app_graph_def)
+apply(simp add: eqvt_def is_app_graph_aux_def)
 apply(rule TrueI)
 apply(rule_tac y="x" in lam.exhaust)
 apply(auto)[3]
@@ -59,7 +58,7 @@
   "rator (Var x) = None"
 | "rator (App t1 t2) = Some t1"
 | "rator (Lam [x]. t) = None"
-apply(simp add: eqvt_def rator_graph_def)
+apply(simp add: eqvt_def rator_graph_aux_def)
 apply(rule TrueI)
 apply(rule_tac y="x" in lam.exhaust)
 apply(auto)[3]
@@ -74,7 +73,7 @@
   "rand (Var x) = None"
 | "rand (App t1 t2) = Some t2"
 | "rand (Lam [x]. t) = None"
-apply(simp add: eqvt_def rand_graph_def)
+apply(simp add: eqvt_def rand_graph_aux_def)
 apply(rule TrueI)
 apply(rule_tac y="x" in lam.exhaust)
 apply(auto)[3]
@@ -90,7 +89,7 @@
 | "is_eta_nf (App t1 t2) = (is_eta_nf t1 \<and> is_eta_nf t2)"
 | "is_eta_nf (Lam [x]. t) = (is_eta_nf t \<and> 
                              ((is_app t \<and> rand t = Some (Var x)) \<longrightarrow> atom x \<in> supp (rator t)))"
-apply(simp add: eqvt_def is_eta_nf_graph_def)
+apply(simp add: eqvt_def is_eta_nf_graph_aux_def)
 apply(rule TrueI)
 apply(rule_tac y="x" in lam.exhaust)
 apply(auto)[3]
@@ -120,7 +119,7 @@
   "var_pos y (Var x) = (if y = x then {[]} else {})"
 | "var_pos y (App t1 t2) = (Cons Left ` (var_pos y t1)) \<union> (Cons Right ` (var_pos y t2))"
 | "atom x \<sharp> y \<Longrightarrow> var_pos y (Lam [x]. t) = (Cons In ` (var_pos y t))"
-apply(simp add: eqvt_def var_pos_graph_def)
+apply(simp add: eqvt_def var_pos_graph_aux_def)
 apply(rule TrueI)
 apply(case_tac x)
 apply(rule_tac y="b" and c="a" in lam.strong_exhaust)
@@ -166,7 +165,7 @@
   "(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 ::== (App (Var y) s)])"
-  apply(simp add: eqvt_def subst'_graph_def)
+  apply(simp add: eqvt_def subst'_graph_aux_def)
   apply(rule TrueI)
   apply(case_tac x)
   apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust)
@@ -200,9 +199,7 @@
   "frees_lst (Var x) = [atom x]"
 | "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2"
 | "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)"
-  unfolding eqvt_def
-  unfolding frees_lst_graph_def
-apply(simp)
+apply(simp add: eqvt_def frees_lst_graph_aux_def)
 apply(rule TrueI)
 apply(rule_tac y="x" in lam.exhaust)
 using [[simproc del: alpha_lst]]
@@ -228,7 +225,7 @@
   "frees_set (Var x) = {atom x}"
 | "frees_set (App t1 t2) = frees_set t1 \<union> frees_set t2"
 | "frees_set (Lam [x]. t) = (frees_set t) - {atom x}"
-  apply(simp add: eqvt_def frees_set_graph_def)
+  apply(simp add: eqvt_def frees_set_graph_aux_def)
   apply(erule frees_set_graph.induct)
   apply(auto)[9]
   apply(rule_tac y="x" in lam.exhaust)
@@ -256,7 +253,7 @@
   "height (Var x) = 1"
 | "height (App t1 t2) = max (height t1) (height t2) + 1"
 | "height (Lam [x].t) = height t + 1"
-  apply(simp add: eqvt_def height_graph_def)
+  apply(simp add: eqvt_def height_graph_aux_def)
   apply(rule TrueI)
   apply(rule_tac y="x" in lam.exhaust)
   using [[simproc del: alpha_lst]]
@@ -279,8 +276,7 @@
   "(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])"
-  unfolding eqvt_def subst_graph_def
-  apply(simp)
+  apply(simp add: eqvt_def subst_graph_aux_def)
   apply(rule TrueI)
   using [[simproc del: alpha_lst]]
   apply(auto)
@@ -468,7 +464,7 @@
   "trans (Var x) xs = lookup xs 0 x"
 | "trans (App t1 t2) xs = LNApp (trans t1 xs) (trans t2 xs)"
 | "atom x \<sharp> xs \<Longrightarrow> trans (Lam [x]. t) xs = LNLam (trans t (x # xs))"
-  apply (simp add: eqvt_def trans_graph_def)
+  apply (simp add: eqvt_def trans_graph_aux_def)
   apply (erule trans_graph.induct)
   apply (auto simp add: ln.fresh)[3]
   apply (simp add: supp_lookup_fresh)
@@ -503,7 +499,7 @@
   "cntlams (Var x) = 0"
 | "cntlams (App t1 t2) = (cntlams t1) + (cntlams t2)"
 | "cntlams (Lam [x]. t) = Suc (cntlams t)"
-  apply(simp add: eqvt_def cntlams_graph_def)
+  apply(simp add: eqvt_def cntlams_graph_aux_def)
   apply(rule TrueI)
   apply(rule_tac y="x" in lam.exhaust)
   apply(auto)[3]
@@ -530,7 +526,7 @@
   "cntbvs (Var x) xs = (if x \<in> set xs then 1 else 0)"
 | "cntbvs (App t1 t2) xs = (cntbvs t1 xs) + (cntbvs t2 xs)"
 | "atom x \<sharp> xs \<Longrightarrow> cntbvs (Lam [x]. t) xs = cntbvs t (x # xs)"
-  apply(simp add: eqvt_def cntbvs_graph_def)
+  apply(simp add: eqvt_def cntbvs_graph_aux_def)
   apply(rule TrueI)
   apply(case_tac x)
   apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
@@ -589,8 +585,7 @@
 | "transdb (App t1 t2) xs = 
       Option.bind (transdb t1 xs) (\<lambda>d1. Option.bind (transdb t2 xs) (\<lambda>d2. Some (DBApp d1 d2)))"
 | "x \<notin> set xs \<Longrightarrow> transdb (Lam [x].t) xs = Option.map DBLam (transdb t (x # xs))"
-  unfolding eqvt_def transdb_graph_def
-  apply(simp)
+  apply(simp add: eqvt_def transdb_graph_aux_def)
   apply(rule TrueI)
   apply (case_tac x)
   apply (rule_tac y="a" and c="b" in lam.strong_exhaust)
@@ -651,7 +646,7 @@
 | "apply_subst (Var x) t2 = App (Var x) t2"
 | "apply_subst (App t0 t1) t2 = App (App t0 t1) t2"
 | "atom x \<sharp> t2 \<Longrightarrow> apply_subst (Lam [x].t1) t2 = eval (t1[x::= t2])"
-  apply(simp add: eval_apply_subst_graph_def eqvt_def)
+  apply(simp add: eval_apply_subst_graph_aux_def eqvt_def)
   apply(rule TrueI)
   apply (case_tac x)
   apply (case_tac a rule: lam.exhaust)
@@ -703,8 +698,7 @@
   "atom c \<sharp> (x, M) \<Longrightarrow> q (Lam [x]. M) (N :: lam) = Lam [x]. (Lam [c]. (App M (q (Var c) N)))"
 | "q (Var x) N = Var x"
 | "q (App l r) N = App l r"
-unfolding eqvt_def q_graph_def
-apply (simp)
+apply(simp add: eqvt_def q_graph_aux_def)
 apply (rule TrueI)
 apply (case_tac x)
 apply (rule_tac y="a" in lam.exhaust)
@@ -732,7 +726,7 @@
 | "eqvt f \<Longrightarrow> map_term f (App t1 t2) = App (f t1) (f t2)"
 | "eqvt f \<Longrightarrow> map_term f (Lam [x].t) = Lam [x].(f t)"
 | "\<not>eqvt f \<Longrightarrow> map_term f t = t"
-  apply (simp add: eqvt_def map_term_graph_def)
+  apply (simp add: eqvt_def map_term_graph_aux_def)
   apply(rule TrueI)
   apply (case_tac x, case_tac "eqvt a", case_tac b rule: lam.exhaust)
   using [[simproc del: alpha_lst]]
@@ -812,7 +806,7 @@
 where
   "Z (App M N) k = Z M (%m. (Z N (%n.(App m n))))"
 | "Z (App M N) k = Z M (%m. (Z N (%n.(App (App m n) (Abs b (k (Var b)))))))"
-unfolding eqvt_def Z_graph_def
+apply(simp add: eqvt_def Z_graph_aux_def)
 apply (rule, perm_simp, rule)
 oops
 
@@ -852,7 +846,7 @@
 | "aux (Lam [x].t) (App t1 t2) xs = False"
 | "\<lbrakk>{atom x} \<sharp>* (s, xs); {atom y} \<sharp>* (t, xs); x \<noteq> y\<rbrakk> \<Longrightarrow> 
        aux (Lam [x].t) (Lam [y].s) xs = aux t s ((x, y) # xs)"
-  apply (simp add: eqvt_def aux_graph_def)
+  apply (simp add: eqvt_def aux_graph_aux_def)
   apply(erule aux_graph.induct)
   apply(simp_all add: fresh_star_def pure_fresh)[9]
   apply(case_tac x)
@@ -899,8 +893,8 @@
 | "aux2 (Lam [x].t) (Var y) = False"
 | "aux2 (Lam [x].t) (App t1 t2) = False"
 | "x = y \<Longrightarrow> aux2 (Lam [x].t) (Lam [y].s) = aux2 t s"
-  apply(simp add: eqvt_def aux2_graph_def)
-  apply(simp)
+  apply(simp add: eqvt_def aux2_graph_aux_def)
+  apply(rule TrueI)
   apply(case_tac x)
   apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
   apply(rule_tac y="b" in lam.exhaust)
diff -r ca6ca6fc28af -r 25d11b449e92 Nominal/Ex/Let.thy
--- a/Nominal/Ex/Let.thy	Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/Ex/Let.thy	Tue Aug 07 18:54:52 2012 +0100
@@ -115,7 +115,7 @@
 | "height_trm (App l r) = max (height_trm l) (height_trm r)"
 | "height_trm (Lam v b) = 1 + (height_trm b)"
 | "height_trm (Let as b) = max (apply_assn height_trm as) (height_trm b)"
-  apply (simp only: eqvt_def height_trm_graph_def)
+  apply (simp only: eqvt_def height_trm_graph_aux_def)
   apply (rule, perm_simp, rule, rule TrueI)
   apply (case_tac x rule: trm_assn.exhaust(1))
   apply (auto)[4]
@@ -169,7 +169,7 @@
 | "subst s t (App l r) = App (subst s t l) (subst s t r)"
 | "atom v \<sharp> (s, t) \<Longrightarrow> subst s t (Lam v b) = Lam v (subst s t b)"
 | "set (bn as) \<sharp>* (s, t) \<Longrightarrow> subst s t (Let as b) = Let (apply_assn2 (subst s t) as) (subst s t b)"
-  apply (simp only: eqvt_def subst_graph_def)
+  apply (simp only: eqvt_def subst_graph_aux_def)
   apply (rule, perm_simp, rule)
   apply (rule TrueI)
   apply (case_tac x)
diff -r ca6ca6fc28af -r 25d11b449e92 Nominal/Ex/LetRec.thy
--- a/Nominal/Ex/LetRec.thy	Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/Ex/LetRec.thy	Tue Aug 07 18:54:52 2012 +0100
@@ -37,8 +37,8 @@
 | "height_trm (Lam v b) = 1 + (height_trm b)"
 | "height_trm (Let_Rec bp b) = max (height_bp bp) (height_trm b)"
 | "height_bp (Bp v t) = height_trm t"
-  apply (simp only: eqvt_def height_trm_height_bp_graph_def)
-  apply (rule, perm_simp, rule, rule TrueI)
+  apply (simp add: eqvt_def height_trm_height_bp_graph_aux_def)
+  apply(rule TrueI)
   using [[simproc del: alpha_set]]
   apply auto
   apply (case_tac x)
diff -r ca6ca6fc28af -r 25d11b449e92 Nominal/Ex/Pi.thy
--- a/Nominal/Ex/Pi.thy	Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/Ex/Pi.thy	Tue Aug 07 18:54:52 2012 +0100
@@ -32,29 +32,9 @@
 where
   "subst_name_list a [] = a"
 | "subst_name_list a ((b, c)#xs) = (if (a = b) then c else (subst_name_list a xs))"
+  apply(simp add: eqvt_def subst_name_list_graph_aux_def)
+  apply(simp)
   apply(auto)
-  apply(subgoal_tac "\<And>p x r. subst_name_list_graph x r \<Longrightarrow> subst_name_list_graph (p \<bullet> x) (p \<bullet> r)")
-  unfolding eqvt_def
-  apply(simp only: permute_fun_def)
-  apply(rule allI)
-  apply(rule ext)
-  apply(rule ext)
-  apply(simp only: 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_name_list_graph.induct)
-  apply(perm_simp)
-  apply(rule subst_name_list_graph.intros)
-  apply(perm_simp)
-  apply(rule subst_name_list_graph.intros)
-  apply(simp)
   apply(rule_tac y="b" in list.exhaust)
   by(auto)
 
@@ -181,97 +161,7 @@
 | "(succ\<onesuperior>)[x::=\<onesuperior>y] = succ\<onesuperior>"
   using [[simproc del: alpha_lst]]
   apply(auto simp add: piMix_distinct piMix_eq_iff)
-  apply(subgoal_tac "\<And>p x r. subsGuard_mix_subsList_mix_subs_mix_graph x r \<Longrightarrow> subsGuard_mix_subsList_mix_subs_mix_graph (p \<bullet> x) (p \<bullet> r)")
-  unfolding eqvt_def
-  apply(rule allI)
-  apply(simp only: permute_fun_def)
-  apply(rule ext)
-  apply(rule ext)
-  apply(simp only: 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)
-  --"Equivariance"
-  apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.induct)
-  apply(simp (no_asm_use) only: eqvts)
-  apply(subst testrr)
-  apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)
-  apply(blast)+
-  apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)
-  apply(simp)
-  apply(simp (no_asm_use) only: eqvts)
-  apply(subst testrr)
-  apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)
-  apply(blast)+
-  apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)
-  apply(simp only: atom_eqvt[symmetric] Pair_eqvt[symmetric] fresh_eqvt[symmetric] permute_bool_def)
-  apply(simp)
-  apply(simp (no_asm_use) only: eqvts)
-  apply(subst testrr)
-  apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)
-  apply(blast)+
-  apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)
-  apply(simp)
-  apply(simp (no_asm_use) only: eqvts)
-  apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)
-  apply(simp (no_asm_use) only: eqvts)  
-  apply(subst testl)
-  apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)
-  apply(blast)+
-  apply(subst testlr)
-  apply(rotate_tac 2)
-  apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)
-  apply(blast)+
-  apply(perm_simp)
-  apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)
-  apply(blast)
-  apply(blast)
-  apply(simp (no_asm_use) only: eqvts)
-  apply(subst testrr)
-  apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)
-  apply(blast)+
-  apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)
-  apply(simp only: atom_eqvt[symmetric] Pair_eqvt[symmetric] fresh_eqvt[symmetric] permute_bool_def)
-  apply(simp)
-  apply(simp (no_asm_use) only: eqvts)
-  apply(subst testrr)
-  apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)
-  apply(blast)+
-  apply(subst testrr)
-  apply(rotate_tac 2)
-  apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)
-  apply(blast)+
-  apply(perm_simp)
-  apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)
-  apply(blast)
-  apply(blast)
-  apply(simp (no_asm_use) only: eqvts)
-  apply(subst testrr)
-  apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)
-  apply(blast)+
-  apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)
-  apply(blast)
-  apply(simp (no_asm_use) only: eqvts)
-  apply(subst testlr)
-  apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)
-  apply(blast)+
-  apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)
-  apply(blast)
-  apply(simp (no_asm_use) only: eqvts)
-  apply(subst testrr)
-  apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)
-  apply(blast)+
-  apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)
-  apply(simp only: atom_eqvt[symmetric] Pair_eqvt[symmetric] fresh_eqvt[symmetric] permute_bool_def)
-  apply(blast)
-  apply(perm_simp)
-  apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)
+  apply(simp add: eqvt_def  subsGuard_mix_subsList_mix_subs_mix_graph_aux_def)
   --"Covered all cases"
   apply(case_tac x)
   apply(simp)
@@ -398,6 +288,99 @@
   apply(simp add: eqvt_at_def)
   apply(drule_tac x="(b \<leftrightarrow> ba)" in spec)
   apply(simp)
+  apply (simp only: meta_eq_to_obj_eq[OF subs_mix_def, symmetric, unfolded fun_eq_iff])
+  apply(rename_tac b P ba xa ya Pa)
+ apply (subgoal_tac "eqvt_at (\<lambda>(a, b, c). subs_mix a b c) (P, xa, ya)")
+  apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (P, xa, ya)))")
+  apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (Pa, xa, ya)))")
+  prefer 2
+  apply (simp only: eqvt_at_def subs_mix_def)
+  apply rule
+  apply(simp (no_asm))
+  apply (subst testrr)
+  apply (simp add: subsGuard_mix_subsList_mix_subs_mix_sumC_def)
+  apply (simp add: THE_default_def)
+apply (case_tac "Ex1 (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya))))")
+apply simp_all[2]
+apply auto[1]
+apply (erule_tac x="x" in allE)
+apply simp
+apply (thin_tac "\<forall>p\<Colon>perm.
+           p \<bullet> The (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya)))) =
+           (if \<exists>!x\<Colon>guardedTerm_mix + sumList_mix + piMix.
+                  subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x
+            then THE x\<Colon>guardedTerm_mix + sumList_mix + piMix.
+                    subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x
+            else Inr (Inr undefined))")
+apply (thin_tac "\<forall>p\<Colon>perm.
+           p \<bullet> (if \<exists>!x\<Colon>guardedTerm_mix + sumList_mix + piMix.
+                      subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x
+                then THE x\<Colon>guardedTerm_mix + sumList_mix + piMix.
+                        subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x
+                else Inr (Inr undefined)) =
+           (if \<exists>!x\<Colon>guardedTerm_mix + sumList_mix + piMix.
+                  subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x
+            then THE x\<Colon>guardedTerm_mix + sumList_mix + piMix.
+                    subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x
+            else Inr (Inr undefined))")
+apply (thin_tac "atom b \<sharp> (xa, ya)")
+apply (thin_tac "atom ba \<sharp> (xa, ya)")
+apply (thin_tac "[[atom b]]lst. P = [[atom ba]]lst. Pa")
+apply(cases rule: subsGuard_mix_subsList_mix_subs_mix_graph.cases)
+apply assumption
+apply (metis Inr_not_Inl)
+apply (metis Inr_not_Inl)
+apply (metis Inr_not_Inl)
+apply (metis Inr_inject Inr_not_Inl)
+apply (metis Inr_inject Inr_not_Inl)
+apply (rule_tac x="<\<nu>a>\<onesuperior>Sum_Type.Projr
+                            (Sum_Type.Projr
+                              (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI)
+apply clarify
+apply (rule the1_equality)
+apply blast apply assumption
+apply (rule_tac x="Sum_Type.Projr
+                       (Sum_Type.Projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y))))) \<parallel>\<onesuperior>
+                      Sum_Type.Projr
+                       (Sum_Type.Projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Q, xb, y)))))" in exI)
+apply clarify
+apply (rule the1_equality)
+apply blast apply assumption
+apply (rule_tac x="[(a[xb:::=y])\<frown>\<onesuperior>(bb[xb:::=y])]Sum_Type.Projr
+                                                    (Sum_Type.Projr
+(subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI)
+apply clarify
+apply (rule the1_equality)
+apply blast apply assumption
+apply (rule_tac x="\<oplus>\<onesuperior>{Sum_Type.Projl
+                          (Sum_Type.Projr
+                            (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inl (xg, xb, y)))))}" in exI)
+apply clarify
+apply (rule the1_equality)
+apply blast apply assumption
+apply (rule_tac x="\<infinity>(a[xb:::=y])?<bb>\<onesuperior>.Sum_Type.Projr
+                                           (Sum_Type.Projr
+                                             (subsGuard_mix_subsList_mix_subs_mix_sum
+                                               (Inr (Inr (Pb, xb, y)))))" in exI)
+apply clarify
+apply (rule the1_equality)
+apply blast apply assumption
+apply (rule_tac x="succ\<onesuperior>" in exI)
+apply clarify
+apply (rule the1_equality)
+apply blast apply assumption
+apply simp
+(* Here the only real goal compatibility is left *)
+  apply (erule Abs_lst1_fcb)
+  apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app)
+  apply (subgoal_tac "atom ba \<sharp> (\<lambda>(a, x, y). subs_mix a x y) (P, xa, ya)")
+  apply simp
+  apply (erule fresh_eqvt_at)
+  apply(simp add: finite_supp)
+  apply(simp)
+  apply(simp add: eqvt_at_def)
+  apply(drule_tac x="(b \<leftrightarrow> ba)" in spec)
+  apply(simp)
   done
 
 termination (eqvt)
diff -r ca6ca6fc28af -r 25d11b449e92 Nominal/Ex/TypeSchemes1.thy
--- a/Nominal/Ex/TypeSchemes1.thy	Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/Ex/TypeSchemes1.thy	Tue Aug 07 18:54:52 2012 +0100
@@ -80,8 +80,7 @@
 where
   "\<theta><Var X> = lookup \<theta> X"
 | "\<theta><T1 \<rightarrow> T2> = (\<theta><T1>) \<rightarrow> (\<theta><T2>)"
-  unfolding eqvt_def subst_graph_def
-  apply (rule, perm_simp, rule)
+  apply(simp add: eqvt_def subst_graph_aux_def)
   apply(rule TrueI)
   apply(case_tac x)
   apply(rule_tac y="b" in ty.exhaust)
@@ -119,8 +118,7 @@
   substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" ("_<_>" [100,60] 120)
 where
   "fset (map_fset atom Xs) \<sharp>* \<theta> \<Longrightarrow> \<theta><All [Xs].T> = All [Xs].(\<theta><T>)"
-  unfolding eqvt_def substs_graph_def
-  apply (rule, perm_simp, rule)
+  apply(simp add: eqvt_def substs_graph_aux_def)
   apply auto[2]
   apply (rule_tac y="b" and c="a" in tys.strong_exhaust)
   apply auto[1]
@@ -279,10 +277,7 @@
 where
   "atom ` (fset Xs) \<sharp>* T \<Longrightarrow>  
      T \<prec>\<prec> All [Xs].T' \<longleftrightarrow> (\<exists>\<theta>. T = \<theta><T'> \<and> atom ` Dom \<theta> = atom ` fset Xs \<inter> supp T')"
-unfolding generalises_graph_def
-unfolding eqvt_def
-apply(perm_simp)
-apply(simp)
+apply(simp add: generalises_graph_aux_def eqvt_def)
 apply(rule TrueI)
 apply(case_tac x)
 apply(simp)
@@ -409,8 +404,7 @@
 where
   "ftv (Var X) = {|X|}"
 | "ftv (T1 \<rightarrow> T2) = (ftv T1) |\<union>| (ftv T2)"
-  unfolding eqvt_def ftv_graph_def
-  apply (rule, perm_simp, rule)
+  apply(simp add: eqvt_def ftv_graph_aux_def)
   apply(rule TrueI)
   apply(rule_tac y="x" in ty.exhaust)
   apply(blast)
diff -r ca6ca6fc28af -r 25d11b449e92 Nominal/Ex/TypeSchemes2.thy
--- a/Nominal/Ex/TypeSchemes2.thy	Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/Ex/TypeSchemes2.thy	Tue Aug 07 18:54:52 2012 +0100
@@ -80,117 +80,7 @@
   "subst \<theta> (Var X) = lookup \<theta> X"
 | "subst \<theta> (Fun T1 T2) = Fun (subst \<theta> T1) (subst \<theta> T2)"
 | "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs T) = All xs (subst \<theta> T)"
-(*unfolding subst_substs_graph_def eqvt_def
-apply rule
-apply perm_simp
-apply (subst test3)
-defer
-apply (subst test3)
-defer
-apply (subst test3)
-defer
-apply rule*)
-thm subst_substs_graph.intros
-apply(subgoal_tac "\<And>p x r. subst_substs_graph x r \<Longrightarrow> subst_substs_graph (p \<bullet> x) (p \<bullet> r)")
-apply(simp add: eqvt_def)
-apply(rule allI)
-apply(simp add: permute_fun_def permute_bool_def)
-apply(rule ext)
-apply(rule ext)
-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)
---"Eqvt One way"
-apply(erule subst_substs_graph.induct)
-apply(perm_simp)
-apply(rule subst_substs_graph.intros)
-apply(erule subst_substs_graph.cases)
-apply(simp (no_asm_use) only: eqvts)
-apply(subst test)
-back
-apply (rule exI)
-apply(assumption)
-apply(rotate_tac 1)
-apply(erule subst_substs_graph.cases)
-apply(subst test)
-back
-apply (rule exI)
-apply(assumption)
-apply(perm_simp)
-apply(rule subst_substs_graph.intros)
-apply(assumption)
-apply(assumption)
-apply(subst test)
-back
-apply (rule exI)
-apply(assumption)
-apply(perm_simp)
-apply(rule subst_substs_graph.intros)
-apply(assumption)
-apply(assumption)
-apply(simp)
---"A"
-apply(simp (no_asm_use) only: eqvts)
-apply(subst test)
-back
-apply (rule exI)
-apply(assumption)
-apply(rotate_tac 1)
-apply(erule subst_substs_graph.cases)
-apply(subst test)
-back
-apply (rule exI)
-apply(assumption)
-apply(perm_simp)
-apply(rule subst_substs_graph.intros)
-apply(assumption)
-apply(assumption)
-apply(subst test)
-back
-apply (rule exI)
-apply(assumption)
-apply(perm_simp)
-apply(rule subst_substs_graph.intros)
-apply(assumption)
-apply(assumption)
-apply(simp)
---"A"
-apply(simp)
-apply(erule subst_substs_graph.cases)
-apply(simp (no_asm_use) only: eqvts)
-apply(subst test)
-back
-back
-apply (rule exI)
-apply(assumption)
-apply(rule subst_substs_graph.intros)
-apply (simp add: eqvts)
-apply (subgoal_tac "(p \<bullet> (atom ` fset xs)) \<sharp>* (p \<bullet> \<theta>)")
-apply (simp add: image_eqvt eqvts_raw eqvts)
-apply (simp only: fresh_star_permute_iff)
-apply(perm_simp)
-apply(assumption)
-apply(simp (no_asm_use) only: eqvts)
-apply(subst test)
-back
-back
-apply (rule exI)
-apply(assumption)
-apply(rule subst_substs_graph.intros)
-apply (simp add: eqvts)
-apply (subgoal_tac "(p \<bullet> (atom ` fset xs)) \<sharp>* (p \<bullet> \<theta>)")
-apply (simp add: image_eqvt eqvts_raw eqvts)
-apply (simp only: fresh_star_permute_iff)
-apply(perm_simp)
-apply(assumption)
-apply(simp)
---"Eqvt done"
+apply(simp add: subst_substs_graph_aux_def eqvt_def)
 apply(rule TrueI)
 apply (case_tac x)
 apply simp apply clarify 
diff -r ca6ca6fc28af -r 25d11b449e92 Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/Nominal2_Base.thy	Tue Aug 07 18:54:52 2012 +0100
@@ -2099,7 +2099,7 @@
 
 subsection {* Type @{typ "'a multiset"} is finitely supported *}
 
-lemma set_of_eqvt[eqvt]:
+lemma set_of_eqvt [eqvt]:
   shows "p \<bullet> (set_of M) = set_of (p \<bullet> M)"
 by (induct M) (simp_all add: insert_eqvt empty_eqvt)
 
@@ -2886,7 +2886,7 @@
   assumes atom_eq_iff [simp]: "atom a = atom b \<longleftrightarrow> a = b"
   assumes atom_eqvt: "p \<bullet> (atom a) = atom (p \<bullet> a)"
 
-declare atom_eqvt[eqvt]
+declare atom_eqvt [eqvt]
 
 class at = at_base +
   assumes sort_of_atom_eq [simp]: "sort_of (atom a) = sort_of (atom b)"
diff -r ca6ca6fc28af -r 25d11b449e92 Nominal/nominal_function_core.ML
--- a/Nominal/nominal_function_core.ML	Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/nominal_function_core.ML	Tue Aug 07 18:54:52 2012 +0100
@@ -18,10 +18,15 @@
     -> ((bstring * typ) list * term list * term * term) list (* specification *)
     -> local_theory
     -> (term   (* f *)
+        * term (* G(raph) *)
+        * thm list (* GIntros *)
+        * thm (* Ginduct *) 
         * thm  (* goalstate *)
         * (thm -> Nominal_Function_Common.nominal_function_result) (* continuation *)
        ) * local_theory
 
+  val inductive_def : (binding * typ) * mixfix -> term list -> local_theory 
+    -> (term * thm list * thm * thm) * local_theory
 end
 
 structure Nominal_Function_Core : NOMINAL_FUNCTION_CORE =
@@ -586,7 +591,7 @@
 
 (* wrapper -- restores quantifiers in rule specifications *)
 fun inductive_def (binding as ((R, T), _)) intrs lthy =
-  let
+  let 
     val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, raw_induct, ...}, lthy) =
       lthy
       |> Local_Theory.conceal
@@ -1083,7 +1088,7 @@
           termination=total_intro, domintros=dom_intros, eqvts=[f_eqvt]}
       end
   in
-    ((f, goalstate, mk_partial_rules), lthy)
+    ((f, G, GIntro_thms, G_induct, goalstate, mk_partial_rules), lthy)
   end
 
 
diff -r ca6ca6fc28af -r 25d11b449e92 Nominal/nominal_mutual.ML
--- a/Nominal/nominal_mutual.ML	Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/nominal_mutual.ML	Tue Aug 07 18:54:52 2012 +0100
@@ -4,6 +4,8 @@
     heavily based on the code of Alexander Krauss
     (code forked on 14 January 2011)
 
+    Joachim Breitner helped with the auxiliary graph
+    definitions (7 August 2012)
 
 Mutual recursive nominal function definitions.
 *)
@@ -384,19 +386,114 @@
   end
 
 (* nominal *)
+fun subst_all s (Q $ Abs(_, _, t)) = 
+  let
+    val vs = map Free (Term.add_frees s [])
+  in
+    fold Logic.all vs (subst_bound (s, t))
+  end
+
+fun mk_comp_dummy t s = Const (@{const_name comp}, dummyT) $ t $ s
+
+fun all v t = 
+  let
+    val T = Term.fastype_of v
+  in
+    Logic.all_const T $ absdummy T (abstract_over (v, t)) 
+  end
+
+(* nominal *)
 fun prepare_nominal_function_mutual config defname fixes eqss lthy =
   let
     val mutual as Mutual {fsum_var=(n, T), qglrs, ...} =
       analyze_eqs lthy defname (map fst fixes) (map Envir.beta_eta_contract eqss)
 
-    val ((fsum, goalstate, cont), lthy') =
+    val ((fsum, G, GIntro_thms, G_induct, goalstate, cont), lthy') =
       Nominal_Function_Core.prepare_nominal_function config defname [((n, T), NoSyn)] qglrs lthy
 
-    val (mutual', lthy'') = define_projections fixes mutual fsum lthy'
+    val (mutual' as Mutual {n', parts, ST, RST, ...}, lthy'') = define_projections fixes mutual fsum lthy'
 
     val mutual_cont = mk_partial_rules_mutual lthy'' cont mutual'
+
+    (* XXX *)
+
+    (* defining the auxiliary graph *)
+    fun mk_cases (MutualPart {i', fvar as (n, T), ...}) =
+      let
+        val (tys, ty) = strip_type T
+        val fun_var = Free (n ^ "_aux", HOLogic.mk_tupleT tys --> ty)
+        val inj_fun = absdummy dummyT (SumTree.mk_inj RST n' i' (Bound 0))
+      in
+        Syntax.check_term lthy'' (mk_comp_dummy inj_fun fun_var)
+      end
+
+    val sum_case_exp = map mk_cases parts
+      |> SumTree.mk_sumcases RST 
+   
+    val (G_name, G_type) = dest_Free G 
+    val G_name_aux = G_name ^ "_aux"
+    val subst = [(G, Free (G_name_aux, G_type))]
+    val GIntros_aux = GIntro_thms
+      |> map prop_of
+      |> map (Term.subst_free subst)
+      |> map (subst_all sum_case_exp)
+
+    val ((G_aux, GIntro_aux_thms, _, G_aux_induct), lthy''') = 
+      Nominal_Function_Core.inductive_def ((Binding.name G_name_aux, G_type), NoSyn) GIntros_aux lthy''
+
+    (* proof of equivalence between graph and auxiliary graph *)
+    val x = Var(("x", 0), ST)
+    val y = Var(("y", 1), RST)
+    val G_aux_prem = HOLogic.mk_Trueprop (G_aux $ x $ y)
+    val G_prem = HOLogic.mk_Trueprop (G $ x $ y)
+
+    fun mk_inj_goal  (MutualPart {i', ...}) =
+      let
+        val injs = SumTree.mk_inj ST n' i' (Bound 0)
+        val projs = y
+          |> SumTree.mk_proj RST n' i'
+          |> SumTree.mk_inj RST n' i'
+      in
+        Const (@{const_name "All"}, dummyT) $ absdummy dummyT
+          (HOLogic.mk_imp (HOLogic.mk_eq(x, injs), HOLogic.mk_eq(projs, y)))
+      end
+
+    val goal_inj = Logic.mk_implies (G_aux_prem, 
+      HOLogic.mk_Trueprop (fold_conj (map mk_inj_goal parts)))
+      |> all x |> all y
+      |> Syntax.check_term lthy'''
+    val goal_iff1 = Logic.mk_implies (G_aux_prem, G_prem)
+      |> all x |> all y
+    val goal_iff2 = Logic.mk_implies (G_prem, G_aux_prem)
+      |> all x |> all y
+
+    val simp_thms = @{thms Projl.simps Projr.simps sum.inject sum.cases sum.distinct o_apply}
+    val ss0 = HOL_basic_ss addsimps simp_thms
+    val ss1 = HOL_ss addsimps simp_thms
+
+    val inj_thm = Goal.prove lthy''' [] [] goal_inj 
+      (K (HEADGOAL (DETERM o etac G_aux_induct THEN_ALL_NEW asm_simp_tac ss1)))
+
+    fun aux_tac thm = 
+      rtac (Drule.gen_all thm) THEN_ALL_NEW (asm_full_simp_tac (ss1 addsimps [inj_thm]))
+    
+    val iff1_thm = Goal.prove lthy''' [] [] goal_iff1 
+      (K (HEADGOAL (DETERM o etac G_aux_induct THEN' RANGE (map aux_tac GIntro_thms))))
+      |> Drule.gen_all
+    val iff2_thm = Goal.prove lthy''' [] [] goal_iff2 
+      (K (HEADGOAL (DETERM o etac G_induct THEN' RANGE (map (aux_tac o simplify ss0) GIntro_aux_thms))))
+      |> Drule.gen_all
+
+    val iff_thm = Goal.prove lthy''' [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (G, G_aux)))
+      (K (HEADGOAL (EVERY' ((map rtac @{thms ext ext iffI}) @ [etac iff2_thm, etac iff1_thm]))))
+ 
+    val tac = HEADGOAL (simp_tac (HOL_basic_ss addsimps [iff_thm]))
+    val goalstate' = 
+      case (SINGLE tac) goalstate of
+        NONE => error "auxiliary equivalence proof failed"
+      | SOME st => st
   in
-    ((goalstate, mutual_cont), lthy'')
+    ((goalstate', mutual_cont), lthy''')
   end
 
 end
diff -r ca6ca6fc28af -r 25d11b449e92 Tutorial/Lambda.thy
--- a/Tutorial/Lambda.thy	Tue Aug 07 18:53:50 2012 +0100
+++ b/Tutorial/Lambda.thy	Tue Aug 07 18:54:52 2012 +0100
@@ -38,7 +38,7 @@
   "height (Var x) = 1"
 | "height (App t1 t2) = max (height t1) (height t2) + 1"
 | "height (Lam [x].t) = height t + 1"
-apply(simp add: eqvt_def height_graph_def)
+apply(simp add: eqvt_def height_graph_aux_def)
 apply(rule TrueI)
 apply(rule_tac y="x" in lam.exhaust)
 using [[simproc del: alpha_lst]]
@@ -59,8 +59,8 @@
   "(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])"
-  unfolding eqvt_def subst_graph_def
-  apply(rule, perm_simp, rule)
+  unfolding eqvt_def subst_graph_aux_def
+  apply(simp)
   apply(rule TrueI)
   using [[simproc del: alpha_lst]]
   apply(auto)