# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268211523 -3600
# Node ID 9d70a07337863ad97b8255ca379dbc9395c186ac
# Parent  0511e879a6872b85758c2bd85a1315efe0cae12c
rhs of alpha_bn, and template for the arguments.

diff -r 0511e879a687 -r 9d70a0733786 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Wed Mar 10 09:45:38 2010 +0100
+++ b/Nominal/Fv.thy	Wed Mar 10 09:58:43 2010 +0100
@@ -204,14 +204,22 @@
   fun alpha_bn_constr (cname, dts) args_in_bn =
   let
     val Ts = map (typ_of_dtyp descr sorts) dts;
+    val pi = Free("pi", @{typ perm})
     val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts);
     val names2 = Name.variant_list ("pi" :: names) (Datatype_Prop.make_tnames Ts);
     val args = map Free (names ~~ Ts);
     val args2 = map Free (names2 ~~ Ts);
     val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp));
-    (*...*)
+    val rhs = HOLogic.mk_Trueprop
+      (alpha_bn_free $ pi $ (list_comb (c, args)) $ (list_comb (c, args2)));
+    fun lhs_arg ((dt, arg_no), (arg, arg2)) =
+      (*...*)
+      @{term True}
+    val arg_nos = 0 upto (length dts - 1)
+    val lhss = mk_conjl (map lhs_arg (dts ~~ arg_nos ~~ (args ~~ args2)))
+    val eq = Logic.mk_implies (HOLogic.mk_Trueprop lhss, rhs)
   in
-    []
+    eq
   end
   val (_, (_, _, constrs)) = nth descr ith_dtyp;
   val eqs = map2i alpha_bn_constr constrs args_in_bns