# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268650212 -3600
# Node ID 3246c5e1a9d71afb5d425398e6081275e48e65bb
# Parent  aca9a6380c3fbc3a87c248904b4f4ddb34adce13
cheat_alpha_eqvt no longer needed; the proofs work.

diff -r aca9a6380c3f -r 3246c5e1a9d7 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Mon Mar 15 10:36:09 2010 +0100
+++ b/Nominal/Parser.thy	Mon Mar 15 11:50:12 2010 +0100
@@ -339,8 +339,9 @@
   fun alpha_eqvt_tac' _ =
     if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy
     else alpha_eqvt_tac alpha_induct_loc (raw_perm_def @ alpha_inj_loc) lthy4 1
-  val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc_nobn perms alpha_eqvt_tac' lthy4;
+  val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc alpha_eqvt_tac' lthy4;
   val alpha_eqvt = ProofContext.export lthy4 lthy2 alpha_eqvt_loc;
+  val _ = map tracing (map PolyML.makestring alpha_eqvt)
   val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
   val fv_eqvt_tac =
     if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy)
diff -r aca9a6380c3f -r 3246c5e1a9d7 Nominal/Rsp.thy
--- a/Nominal/Rsp.thy	Mon Mar 15 10:36:09 2010 +0100
+++ b/Nominal/Rsp.thy	Mon Mar 15 11:50:12 2010 +0100
@@ -135,6 +135,16 @@
 *}
 
 ML {*
+fun perm_arg arg =
+let
+  val ty = fastype_of arg
+in
+  Const (@{const_name permute}, @{typ perm} --> ty --> ty)
+end
+*}
+
+
+ML {*
 fun build_eqvts bind funs tac ctxt =
 let
   val pi = Free ("p", @{typ perm});
@@ -142,7 +152,6 @@
   val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames types);
   val args = map Free (indnames ~~ types);
   val perm_at = @{term "permute :: perm \<Rightarrow> atom set \<Rightarrow> atom set"}
-  fun perm_arg arg = Const (@{const_name permute}, @{typ perm} --> fastype_of arg --> fastype_of arg)
   fun eqvtc (fnctn, arg) =
     HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm_arg arg $ pi $ arg)))
   val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ args)))
@@ -181,19 +190,26 @@
 *}
 
 ML {*
-fun build_alpha_eqvts funs perms tac ctxt =
+fun build_alpha_eqvt alpha names =
 let
   val pi = Free ("p", @{typ perm});
-  val types = map (domain_type o fastype_of) funs;
-  val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames (map body_type types));
-  val indnames2 = Name.variant_list ("p" :: indnames) (Datatype_Prop.make_tnames (map body_type types));
-  val args = map Free (indnames ~~ types);
-  val args2 = map Free (indnames2 ~~ types);
-  fun eqvtc ((alpha, perm), (arg, arg2)) =
-    HOLogic.mk_imp (alpha $ arg $ arg2,
-      (alpha $ (perm $ pi $ arg) $ (perm $ pi $ arg2)))
-  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc ((funs ~~ perms) ~~ (args ~~ args2))))
-  val thm = Goal.prove ctxt ("p" :: indnames @ indnames2) [] gl tac
+  val (tys, _) = strip_type (fastype_of alpha)
+  val indnames = Name.variant_list names (Datatype_Prop.make_tnames (map body_type tys));
+  val args = map Free (indnames ~~ tys);
+  val perm_args = map (fn x => perm_arg x $ pi $ x) args
+in
+  (HOLogic.mk_imp (list_comb (alpha, args), list_comb (alpha, perm_args)), indnames @ names)
+end
+*}
+
+ML {* fold_map build_alpha_eqvt *}
+
+ML {*
+fun build_alpha_eqvts funs tac ctxt =
+let
+  val (gls, names) = fold_map build_alpha_eqvt funs ["p"]
+  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj gls)
+  val thm = Goal.prove ctxt names [] gl tac
 in
   map (fn x => mp OF [x]) (HOLogic.conj_elims thm)
 end
diff -r aca9a6380c3f -r 3246c5e1a9d7 Nominal/Test.thy
--- a/Nominal/Test.thy	Mon Mar 15 10:36:09 2010 +0100
+++ b/Nominal/Test.thy	Mon Mar 15 11:50:12 2010 +0100
@@ -6,6 +6,8 @@
 
 atom_decl name
 
+ML {* val cheat_alpha_eqvt = ref false *}
+
 nominal_datatype lam =
   VAR "name"
 | APP "lam" "lam"