--- 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