# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268754666 -3600
# Node ID 91fe914e1befa35d69610653e5ba4c70adaa76ff
# Parent  686c58ea7a24c513bdbed7bb7814ea1f56f962bf
alpha_bn doesn't need the permutation in non-recursive case.

diff -r 686c58ea7a24 -r 91fe914e1bef Nominal/Fv.thy
--- a/Nominal/Fv.thy	Tue Mar 16 16:17:05 2010 +0100
+++ b/Nominal/Fv.thy	Tue Mar 16 16:51:06 2010 +0100
@@ -209,19 +209,22 @@
   val {descr, sorts, ...} = dt_info;
   fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
   val alpha_bn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Const bn)));
-  val alpha_bn_type = @{typ perm} --> nth_dtyp ith_dtyp --> nth_dtyp ith_dtyp --> @{typ bool}
+  val alpha_bn_type = 
+    if is_rec then @{typ perm} --> nth_dtyp ith_dtyp --> nth_dtyp ith_dtyp --> @{typ bool}
+    else nth_dtyp ith_dtyp --> nth_dtyp ith_dtyp --> @{typ bool};
   val alpha_bn_free = Free(alpha_bn_name, alpha_bn_type);
+  val pi = Free("pi", @{typ perm})
+  val alpha_bn_pi = if is_rec then alpha_bn_free $ pi else alpha_bn_free;
   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)));
+      (alpha_bn_pi $ (list_comb (c, args)) $ (list_comb (c, args2)));
     fun lhs_arg ((dt, arg_no), (arg, arg2)) =
       let
         val argty = fastype_of arg;
@@ -229,7 +232,7 @@
         val permarg = if is_rec then permute $ pi $ arg else arg
       in
       if is_rec_type dt then
-        if arg_no mem args_in_bn then alpha_bn_free $ pi $ arg $ arg2
+        if arg_no mem args_in_bn then alpha_bn_pi $ arg $ arg2
         else (nth alpha_frees (body_index dt)) $ permarg $ arg2
       else
         if arg_no mem args_in_bn then @{term True}
@@ -351,9 +354,12 @@
               if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2)
               else (HOLogic.mk_eq (arg, arg2))
           | (_, [], []) => @{term True}
-          | ([], ((((SOME (bn, _)), _, _), pi) :: _), []) =>
+          | ([], ((((SOME (bn, is_rec)), _, _), pi) :: _), []) =>
             let
-              val alpha_bn = nth alpha_bn_frees (find_index (fn (b, _, _) => b = bn) bns) $ pi $ arg $ arg2
+              val alpha_bn_const =
+                nth alpha_bn_frees (find_index (fn (b, _, _) => b = bn) bns)
+              val alpha_bn =
+                if is_rec then alpha_bn_const $ pi $ arg $ arg2 else alpha_bn_const $ arg $ arg2
               val ty = fastype_of (bn $ arg)
               val permute = Const(@{const_name permute}, @{typ perm} --> ty --> ty)
             in
diff -r 686c58ea7a24 -r 91fe914e1bef Nominal/Test.thy
--- a/Nominal/Test.thy	Tue Mar 16 16:17:05 2010 +0100
+++ b/Nominal/Test.thy	Tue Mar 16 16:51:06 2010 +0100
@@ -59,7 +59,7 @@
 term alpha_bi
 
 lemma alpha_bi:
-  shows "alpha_bi pi b b' = True"
+  shows "alpha_bi b b' = True"
 apply(induct b rule: lam_bp_inducts(2))
 apply(simp_all)
 apply(induct b' rule: lam_bp_inducts(2))