--- a/Nominal/Parser.thy	Thu Mar 04 15:15:44 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 04 15:55:53 2010 +0100
@@ -209,6 +209,21 @@
 
 ML {* add_primrec_wrapper *}
 
+lemma equivp_hack: "equivp x"
+sorry
+ML {*
+fun equivp_hack ctxt rel =
+let
+  val thy = ProofContext.theory_of ctxt
+  val ty = domain_type (fastype_of rel)
+  val cty = ctyp_of thy ty
+  val ct = cterm_of thy rel
+in
+  Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack}
+end
+*}
+
+
 ML {* 
 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy =
 let
@@ -249,12 +264,13 @@
   val alpha_cases = #elims alpha
   val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases lthy4
   val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc
-  val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
+(*  val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
   val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc perms
     ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) induct lthy5;
   val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms
     (raw_perm_def @ alpha_inj_loc) alpha_induct_loc lthy6;
   val alpha_eqvt = ProofContext.export lthy6 lthy2 alpha_eqvt_loc;
+  val alpha_equivp_loc = map (equivp_hack lthy6) alpha_ts_loc
   val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc
     inject alpha_inj_loc distinct alpha_cases alpha_eqvt_loc lthy6;
   val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc;
@@ -299,11 +315,15 @@
   val (_, lthy16) = Local_Theory.note ((Binding.name (q_name ^ "_fv"), []), q_fv) lthy15;
   val q_bn = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy16, th))) raw_bn_eqs;
   val (_, lthy17) = Local_Theory.note ((Binding.name (q_name ^ "_bn"), []), q_bn) lthy16;
+  val inj_unfolded = map (LocalDefs.unfold lthy17 @{thms alpha_gen}) alpha_inj
+  val q_inj_pre = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy17, th))) inj_unfolded;
+  val q_inj = map (LocalDefs.fold lthy17 @{thms alpha_gen}) q_inj_pre
+  val (_, lthy18) = Local_Theory.note ((Binding.name (q_name ^ "_inject"), []), q_inj) lthy17;*)
 in
-  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy17)
+  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4)
 end
 *}
-
+ML fold
 ML name_of_typ
 
 ML {* 

--- a/Nominal/Test.thy	Thu Mar 04 15:15:44 2010 +0100
+++ b/Nominal/Test.thy	Thu Mar 04 15:55:53 2010 +0100
@@ -4,7 +4,7 @@
 
 text {* weirdo example from Peter Sewell's bestiary *}
 
-(*nominal_datatype weird =
+nominal_datatype weird =
   WBind x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird"
     bind x in p1, bind x in p2, bind y in p2, bind y in p3
 | WV "name"
@@ -19,7 +19,7 @@
 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding weird_inj}, []), (build_alpha_inj @{thms alpha_weird_raw.intros} @{thms weird_raw.distinct weird_raw.inject} @{thms alpha_weird_raw.cases} ctxt)) ctxt)) *}
 thm weird_inj
 
-local_setup {*
+(*local_setup {*
 (fn ctxt => snd (Local_Theory.note ((@{binding alpha_eqvt}, []),
 build_alpha_eqvts [@{term alpha_weird_raw}] [@{term "permute :: perm \<Rightarrow> weird_raw \<Rightarrow> weird_raw"}] @{thms permute_weird_raw.simps weird_inj} @{thm alpha_weird_raw.induct} ctxt) ctxt)) *}
 
@@ -144,10 +144,11 @@
 thm permute_lam_raw_permute_bp_raw.simps
 thm alpha_lam_raw_alpha_bp_raw.intros[no_vars]
 thm fv_lam_raw_fv_bp_raw.simps[no_vars]
-thm lam_bp_induct
+(*thm lam_bp_induct
 thm lam_bp_perm
 thm lam_bp_fv
 thm lam_bp_bn
+thm lam_bp_inject*)
 
 text {* example 2 *}
 
@@ -171,10 +172,11 @@
 thm alpha_trm'_raw_alpha_pat'_raw.intros[no_vars]
 thm fv_trm'_raw_fv_pat'_raw.simps[no_vars]
 thm f_raw.simps
-thm trm'_pat'_induct
+(*thm trm'_pat'_induct
 thm trm'_pat'_perm
 thm trm'_pat'_fv
 thm trm'_pat'_bn
+thm trm'_pat'_inject*)
 
 nominal_datatype trm0 =
   Var0 "name"
@@ -193,10 +195,10 @@
 | "f0 (PD0 p1 p2) = (f0 p1) \<union> (f0 p2)"
 
 thm f0_raw.simps
-thm trm0_pat0_induct
+(*thm trm0_pat0_induct
 thm trm0_pat0_perm
 thm trm0_pat0_fv
-thm trm0_pat0_bn
+thm trm0_pat0_bn*)
 
 text {* example type schemes *}
 
@@ -210,12 +212,11 @@
 *)
 
 
-(* alpha_eqvt fails...
 nominal_datatype t = 
   Var "name" 
 | Fun "t" "t"
 and  tyS = 
-  All xs::"name set" ty::"t" bind xs in ty *)
+  All xs::"name set" ty::"t" bind xs in ty
 
 (* example 1 from Terms.thy *)
 
@@ -271,13 +272,13 @@
 
 (* fv_eqvt does not work, we need to repaire defined permute functions
    defined fv and defined alpha... *)
-(*nominal_datatype trm4 =
+nominal_datatype trm4 =
   Vr4 "name"
 | Ap4 "trm4" "trm4 list"
 | Lm4 x::"name" t::"trm4"  bind x in t
 
 thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars]
-thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]*)
+thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]
 
 (* example 5 from Terms.thy *)
 
@@ -296,7 +297,7 @@
 
 (* example 6 from Terms.thy *)
 
-(* BV is not respectful, needs to fail
+(* BV is not respectful, needs to fail*)
 nominal_datatype trm6 =
   Vr6 "name"
 | Lm6 x::"name" t::"trm6"         bind x in t
@@ -306,11 +307,10 @@
 where
   "bv6 (Vr6 n) = {}"
 | "bv6 (Lm6 n t) = {atom n} \<union> bv6 t"
-| "bv6 (Lt6 l r) = bv6 l \<union> bv6 r" *)
-
+| "bv6 (Lt6 l r) = bv6 l \<union> bv6 r"
 (* example 7 from Terms.thy *)
 
-(* BV is not respectful, needs to fail
+(* BV is not respectful, needs to fail*)
 nominal_datatype trm7 =
   Vr7 "name"
 | Lm7 l::"name" r::"trm7"   bind l in r
@@ -320,7 +320,7 @@
 where
   "bv7 (Vr7 n) = {atom n}"
 | "bv7 (Lm7 n t) = bv7 t - {atom n}"
-| "bv7 (Lt7 l r) = bv7 l \<union> bv7 r" *)
+| "bv7 (Lt7 l r) = bv7 l \<union> bv7 r"
 
 (* example 8 from Terms.thy *)
 
@@ -338,7 +338,7 @@
 
 (* example 9 from Terms.thy *)
 
-(* BV is not respectful, needs to fail
+(* BV is not respectful, needs to fail*)
 nominal_datatype lam9 =
   Var9 "name"
 | Lam9 n::"name" l::"lam9" bind n in l
@@ -348,13 +348,13 @@
   bv9
 where
   "bv9 (Var9 x) = {}"
-| "bv9 (Lam9 x b) = {atom x}" *)
+| "bv9 (Lam9 x b) = {atom x}"
 
 (* example from my PHD *)
 
 atom_decl coname
 
-(*nominal_datatype phd =
+nominal_datatype phd =
    Ax "name" "coname"
 |  Cut n::"coname" t1::"phd" c::"coname" t2::"phd"              bind n in t1, bind c in t2
 |  AndR c1::"coname" t1::"phd" c2::"coname" t2::"phd" "coname"  bind c1 in t1, bind c2 in t2
@@ -365,7 +365,7 @@
 
 thm alpha_phd_raw.intros[no_vars]
 thm fv_phd_raw.simps[no_vars]
-*)
+
 
 (* example form Leroy 96 about modules; OTT *)
 
@@ -498,7 +498,7 @@
 
 thm quot_respect
 (* example 6 from Peter Sewell's bestiary *)
-(*nominal_datatype exp6 =
+nominal_datatype exp6 =
   EVar name
 | EPair exp6 exp6
 | ELetRec x::name p::pat6 e1::exp6 e2::exp6 bind x in e1, bind x in e2, bind "bp6 p" in e1
@@ -511,10 +511,10 @@
 where
   "bp6 (PVar' x) = {atom x}"
 | "bp6 (PUnit') = {}"
-| "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2"*)
+| "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2"
 
 (* example 7 from Peter Sewell's bestiary *)
-(*nominal_datatype exp7 =
+nominal_datatype exp7 =
   EVar name
 | EUnit
 | EPair exp7 exp7
@@ -530,10 +530,10 @@
 where
   "b7 (Assign x e) = {atom x}"
 | "b7s (Single a) = b7 a"
-| "b7s (More a as) = (b7 a) \<union> (b7s as)"*)
+| "b7s (More a as) = (b7 a) \<union> (b7s as)"
 
 (* example 8 from Peter Sewell's bestiary *)
-(*nominal_datatype exp8 =
+nominal_datatype exp8 =
   EVar name
 | EUnit
 | EPair exp8 exp8
@@ -567,7 +567,7 @@
 | "b_fnclauses (S fc) = (b_fnclause fc)"
 | "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)"
 | "b_lrb8 (Clause fcs) = (b_fnclauses fcs)"
-| "b_fnclause (K x pat exp8) = {atom x}"*)
+| "b_fnclause (K x pat exp8) = {atom x}"