--- a/Nominal/ExCoreHaskell.thy	Fri Mar 26 10:55:13 2010 +0100
+++ b/Nominal/ExCoreHaskell.thy	Fri Mar 26 16:20:39 2010 +0100
@@ -5,7 +5,7 @@
 (* core haskell *)
 
 ML {* val _ = recursive := false *}
-ML {* val _ = cheat_const_rsp := true *}
+
 atom_decl var
 atom_decl tvar
 

--- a/Nominal/ExPS3.thy	Fri Mar 26 10:55:13 2010 +0100
+++ b/Nominal/ExPS3.thy	Fri Mar 26 16:20:39 2010 +0100
@@ -11,17 +11,17 @@
   VarP "name"
 | AppP "exp" "exp"
 | LamP x::"name" e::"exp" bind x in e
-| LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind x in e2, bind "bp'' p" in e1
+| LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind x in e2, bind "bp p" in e1
 and pat3 =
   PVar "name"
 | PUnit
 | PPair "pat3" "pat3"
 binder
-  bp'' :: "pat3 \<Rightarrow> atom set"
+  bp :: "pat3 \<Rightarrow> atom set"
 where
-  "bp'' (PVar x) = {atom x}"
-| "bp'' (PUnit) = {}"
-| "bp'' (PPair p1 p2) = bp'' p1 \<union> bp'' p2"
+  "bp (PVar x) = {atom x}"
+| "bp (PUnit) = {}"
+| "bp (PPair p1 p2) = bp p1 \<union> bp p2"
 
 thm exp_pat3.fv
 thm exp_pat3.eq_iff
@@ -30,7 +30,7 @@
 thm exp_pat3.induct
 thm exp_pat3.distinct
 thm exp_pat3.fv
-thm exp_pat3.supp (* The bindings are too complicated *)
+thm exp_pat3.supp
 
 end
 

--- a/Nominal/ExPS6.thy	Fri Mar 26 10:55:13 2010 +0100
+++ b/Nominal/ExPS6.thy	Fri Mar 26 16:20:39 2010 +0100
@@ -8,7 +8,6 @@
 
 (* The binding structure is too complicated, so equivalence the
    way we define it is not true *)
-ML {* val _ = cheat_equivp := true *}
 
 ML {* val _ = recursive := false  *}
 nominal_datatype exp6 =

--- a/Nominal/Fv.thy	Fri Mar 26 10:55:13 2010 +0100
+++ b/Nominal/Fv.thy	Fri Mar 26 16:20:39 2010 +0100
@@ -144,13 +144,9 @@
 
 fun is_atom_fset thy (Type ("FSet.fset", [t])) = is_atom thy t
   | is_atom_fset thy _ = false;
-
-val fset_to_set = @{term "fset_to_set :: atom fset \<Rightarrow> atom set"}
 *}
 
 
-
-
 (* Like map2, only if the second list is empty passes empty lists insted of error *)
 ML {*
 fun map2i _ [] [] = []
@@ -215,6 +211,7 @@
       val ty = fastype_of t;
       val atom_ty = dest_fsetT ty --> @{typ atom};
       val fmap_ty = atom_ty --> ty --> @{typ "atom fset"};
+      val fset_to_set = @{term "fset_to_set :: atom fset \<Rightarrow> atom set"}
     in
       fset_to_set $ ((Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t))
     end;
@@ -241,8 +238,6 @@
 end;
 *}
 
-ML {* @{term "\<lambda>(x, y, z). \<lambda>(x', y', z'). R x x' \<and> R2 y y' \<and> R3 z z'"} *}
-
 (* Given [R1, R2, R3] creates %(x,x'). %(y,y'). %(z,z'). R x x' \<and> R y y' \<and> R z z' *)
 ML {*
 fun mk_compound_alpha Rs =
@@ -259,8 +254,6 @@
 end;
 *}
 
-ML {* cterm_of @{theory} (mk_compound_alpha [@{term "R :: 'a \<Rightarrow> 'a \<Rightarrow> bool"}, @{term "R2 :: 'b \<Rightarrow> 'b \<Rightarrow> bool"}, @{term "R3 :: 'b \<Rightarrow> 'b \<Rightarrow> bool"}]) *}
-
 ML {* fun add_perm (p1, p2) = Const(@{const_name plus}, @{typ "perm \<Rightarrow> perm \<Rightarrow> perm"}) $ p1 $ p2 *}
 
 ML {*
@@ -645,7 +638,7 @@
 ML {*
 fun reflp_tac induct eq_iff ctxt =
   rtac induct THEN_ALL_NEW
-  simp_tac ((mk_minimal_ss ctxt) addsimps eq_iff) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps eq_iff) THEN_ALL_NEW
   split_conj_tac THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]}
   THEN_ALL_NEW split_conj_tac THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps
      @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv
@@ -662,36 +655,6 @@
 end
 *}
 
-ML {*
-fun build_alpha_alphabn fv_alphas_lst inducts eq_iff ctxt  =
-let
-  val (fvs_alphas, ls) = split_list fv_alphas_lst;
-  val (_, alpha_ts) = split_list fvs_alphas;
-  val tys = map (domain_type o fastype_of) alpha_ts;
-  val names = Datatype_Prop.make_tnames tys;
-  val names2 = Name.variant_list names names;
-  val args = map Free (names ~~ tys);
-  val args2 = map Free (names2 ~~ tys);
-  fun alpha_alphabn ((alpha, (arg, arg2)), (no, l)) =
-    if l = [] then [] else
-    let
-      val alpha_bns = map snd l;
-      val lhs = alpha $ arg $ arg2;
-      val rhs = foldr1 HOLogic.mk_conj (map (fn x => x $ arg $ arg2) alpha_bns);
-      val gl = Logic.mk_implies (HOLogic.mk_Trueprop lhs, HOLogic.mk_Trueprop rhs);
-      fun tac _ = (etac (nth inducts no) THEN_ALL_NEW TRY o rtac @{thm TrueI}
-        THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps eq_iff)) 1
-      val th = Goal.prove ctxt (names @ names2) [] gl tac;
-    in
-      Project_Rule.projects ctxt (1 upto length l) th
-    end;
-  val eqs = map alpha_alphabn ((alpha_ts ~~ (args ~~ args2)) ~~ ((0 upto (length ls - 1)) ~~ ls));
-in
-  flat eqs
-end
-*}
-
-
 lemma exi_neg: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (- p)) \<Longrightarrow> \<exists>pi. Q pi"
 apply (erule exE)
 apply (rule_tac x="-pi" in exI)
@@ -700,7 +663,7 @@
 ML {*
 fun symp_tac induct inj eqvt ctxt =
   rel_indtac induct THEN_ALL_NEW
-  simp_tac ((mk_minimal_ss ctxt) addsimps inj) THEN_ALL_NEW split_conj_tac
+  simp_tac (HOL_basic_ss addsimps inj) THEN_ALL_NEW split_conj_tac
   THEN_ALL_NEW
   REPEAT o etac @{thm exi_neg}
   THEN_ALL_NEW
@@ -710,55 +673,25 @@
   (asm_full_simp_tac (HOL_ss addsimps (eqvt @ all_eqvts ctxt)))
 *}
 
-ML {*
-fun imp_elim_tac case_rules =
-  Subgoal.FOCUS (fn {concl, context, ...} =>
-    case term_of concl of
-      _ $ (_ $ asm $ _) =>
-        let
-          fun filter_fn case_rule = (
-            case Logic.strip_assums_hyp (prop_of case_rule) of
-              ((_ $ asmc) :: _) =>
-                let
-                  val thy = ProofContext.theory_of context
-                in
-                  Pattern.matches thy (asmc, asm)
-                end
-            | _ => false)
-          val matching_rules = filter filter_fn case_rules
-        in
-         (rtac impI THEN' rotate_tac (~1) THEN' eresolve_tac matching_rules) 1
-        end
-    | _ => no_tac
-  )
-*}
-
 
 lemma exi_sum: "\<exists>(pi :: perm). P pi \<Longrightarrow> \<exists>(pi :: perm). Q pi \<Longrightarrow> (\<And>(p :: perm) (pi :: perm). P p \<Longrightarrow> Q pi \<Longrightarrow> R (pi + p)) \<Longrightarrow> \<exists>pi. R pi"
 apply (erule exE)+
 apply (rule_tac x="pia + pi" in exI)
 by auto
 
-ML {*
-fun is_ex (Const ("Ex", _) $ Abs _) = true
-  | is_ex _ = false;
-*}
 
 ML {*
-fun eetac rule = Subgoal.FOCUS_PARAMS 
-  (fn (focus) =>
-     let
-       val concl = #concl focus
-       val prems = Logic.strip_imp_prems (term_of concl)
-       val exs = filter (fn x => is_ex (HOLogic.dest_Trueprop x)) prems
-       val cexs = map (SOME o (cterm_of (ProofContext.theory_of (#context focus)))) exs
-       val thins = map (fn cex => Drule.instantiate' [] [cex] Drule.thin_rl) cexs
-     in
-     (etac rule THEN' RANGE[
-        atac,
-        eresolve_tac thins
-     ]) 1
-     end
+fun eetac rule = 
+  Subgoal.FOCUS_PARAMS (fn focus =>
+    let
+      val concl = #concl focus
+      val prems = Logic.strip_imp_prems (term_of concl)
+      val exs = filter (fn x => is_ex (HOLogic.dest_Trueprop x)) prems
+      val cexs = map (SOME o (cterm_of (ProofContext.theory_of (#context focus)))) exs
+      val thins = map (fn cex => Drule.instantiate' [] [cex] Drule.thin_rl) cexs
+    in
+      (etac rule THEN' RANGE[atac, eresolve_tac thins]) 1
+    end
   )
 *}
 
@@ -766,7 +699,7 @@
 fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt =
   rel_indtac induct THEN_ALL_NEW
   (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW
-  asm_full_simp_tac ((mk_minimal_ss ctxt) addsimps alpha_inj) THEN_ALL_NEW
+  asm_full_simp_tac (HOL_basic_ss addsimps alpha_inj) THEN_ALL_NEW
   split_conj_tac THEN_ALL_NEW REPEAT o (eetac @{thm exi_sum} ctxt) THEN_ALL_NEW split_conj_tac
   THEN_ALL_NEW (asm_full_simp_tac (HOL_ss addsimps (term_inj @ distinct)))
   THEN_ALL_NEW split_conj_tac THEN_ALL_NEW
@@ -815,40 +748,6 @@
 end
 *}
 
-(*
-Tests:
-prove alpha1_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *}
-by (tactic {* reflp_tac @{thm rtrm1_bp.induct} @{thms alpha1_inj} 1 *})
-
-prove alpha1_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *}
-by (tactic {* symp_tac @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} @{thms alpha1_eqvt} 1 *})
-
-prove alpha1_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *}
-by (tactic {* transp_tac @{context} @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} @{thms rtrm1.inject bp.inject} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} 1 *})
-
-lemma alpha1_equivp:
-  "equivp alpha_rtrm1"
-  "equivp alpha_bp"
-apply (tactic {*
-  (simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def})
-  THEN' rtac @{thm conjI} THEN' rtac @{thm allI} THEN'
-  resolve_tac (HOLogic.conj_elims @{thm alpha1_reflp_aux})
-  THEN' rtac @{thm conjI} THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN'
-  resolve_tac (HOLogic.conj_elims @{thm alpha1_symp_aux}) THEN' rtac @{thm transp_aux}
-  THEN' resolve_tac (HOLogic.conj_elims @{thm alpha1_transp_aux})
-)
-1 *})
-done*)
-
-ML {*
-fun dtyp_no_of_typ _ (TFree (n, _)) = error "dtyp_no_of_typ: Illegal free"
-  | dtyp_no_of_typ _ (TVar _) = error "dtyp_no_of_typ: Illegal schematic"
-  | dtyp_no_of_typ dts (Type (tname, Ts)) =
-      case try (find_index (curry op = tname o fst)) dts of
-        NONE => error "dtyp_no_of_typ: Illegal recursion"
-      | SOME i => i
-*}
-
 lemma not_in_union: "c \<notin> a \<union> b \<equiv> (c \<notin> a \<and> c \<notin> b)"
 by auto
 
@@ -1025,28 +924,4 @@
 end
 *}
 
-ML {*
-fun build_rsp_gl alphas fnctn ctxt =
-let
-  val typ = domain_type (fastype_of fnctn);
-  val (argl, argr) = the (AList.lookup (op=) alphas typ);
-in
-  ([HOLogic.mk_eq (fnctn $ argl, fnctn $ argr)], ctxt)
 end
-*}
-
-ML {*
-fun fvbv_rsp_tac' simps ctxt =
-  asm_full_simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW
-  asm_full_simp_tac (HOL_ss addsimps (@{thm alpha_gen} :: simps)) THEN_ALL_NEW
-  REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW
-  asm_full_simp_tac (HOL_ss addsimps simps) THEN_ALL_NEW
-  TRY o blast_tac (claset_of ctxt)
-*}
-
-ML {*
-fun build_fvbv_rsps alphas ind simps fnctns ctxt =
-  prove_by_rel_induct alphas build_rsp_gl ind (fvbv_rsp_tac' simps) fnctns ctxt
-*}
-
-end

--- a/Nominal/Lift.thy	Fri Mar 26 10:55:13 2010 +0100
+++ b/Nominal/Lift.thy	Fri Mar 26 16:20:39 2010 +0100
@@ -3,6 +3,18 @@
 begin
 
 ML {*
+fun define_quotient_type args tac ctxt =
+let
+  val mthd = Method.SIMPLE_METHOD tac
+  val mthdt = Method.Basic (fn _ => mthd)
+  val bymt = Proof.global_terminal_proof (mthdt, NONE)
+in
+  bymt (Quotient_Type.quotient_type args ctxt)
+end
+*}
+
+(* Renames schematic variables in a theorem *)
+ML {*
 fun rename_vars fnctn thm =
 let
   val vars = Term.add_vars (prop_of thm) []

--- a/Nominal/Manual/LamEx.thy	Fri Mar 26 10:55:13 2010 +0100
+++ b/Nominal/Manual/LamEx.thy	Fri Mar 26 16:20:39 2010 +0100
@@ -95,8 +95,8 @@
        \<Longrightarrow> rLam a t \<approx>a rLam b s"
 
 lemma a3_inverse:
-  assumes "rLam a t \<approx> rLam b s"
-  shows "\<exists>pi. (rfv t - {atom a} = rfv s - {atom b} \<and> (rfv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx> s)"
+  assumes "rLam a t \<approx>a rLam b s"
+  shows "\<exists>pi. (rfv t - {atom a} = rfv s - {atom b} \<and> (rfv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx>a s)"
 using assms
 apply(erule_tac alpha.cases)
 apply(auto)
@@ -104,7 +104,7 @@
 
 text {* should be automatic with new version of eqvt-machinery *}
 lemma alpha_eqvt:
-  shows "t \<approx> s \<Longrightarrow> (pi \<bullet> t) \<approx> (pi \<bullet> s)"
+  shows "t \<approx>a s \<Longrightarrow> (pi \<bullet> t) \<approx>a (pi \<bullet> s)"
 apply(induct rule: alpha.induct)
 apply(simp add: a1)
 apply(simp add: a2)
@@ -126,7 +126,7 @@
 done
 
 lemma alpha_refl:
-  shows "t \<approx> t"
+  shows "t \<approx>a t"
 apply(induct t rule: rlam.induct)
 apply(simp add: a1)
 apply(simp add: a2)
@@ -136,7 +136,7 @@
 done
 
 lemma alpha_sym:
-  shows "t \<approx> s \<Longrightarrow> s \<approx> t"
+  shows "t \<approx>a s \<Longrightarrow> s \<approx>a t"
 apply(induct rule: alpha.induct)
 apply(simp add: a1)
 apply(simp add: a2)
@@ -152,7 +152,7 @@
 done
 
 lemma alpha_trans:
-  shows "t1 \<approx> t2 \<Longrightarrow> t2 \<approx> t3 \<Longrightarrow> t1 \<approx> t3"
+  shows "t1 \<approx>a t2 \<Longrightarrow> t2 \<approx>a t3 \<Longrightarrow> t1 \<approx>a t3"
 apply(induct arbitrary: t3 rule: alpha.induct)
 apply(erule alpha.cases)
 apply(simp_all)
@@ -188,22 +188,22 @@
   done
 
 lemma alpha_rfv:
-  shows "t \<approx> s \<Longrightarrow> rfv t = rfv s"
+  shows "t \<approx>a s \<Longrightarrow> rfv t = rfv s"
   apply(induct rule: alpha.induct)
   apply(simp_all)
   done
 
 inductive
-    alpha2 :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100)
+    alpha2 :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx>a2 _" [100, 100] 100)
 where
-  a21: "a = b \<Longrightarrow> (rVar a) \<approx>2 (rVar b)"
-| a22: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx>2 rApp t2 s2"
-| a23: "(a = b \<and> t \<approx>2 s) \<or> (a \<noteq> b \<and> ((a \<leftrightarrow> b) \<bullet> t) \<approx>2 s \<and> atom b \<notin> rfv t)\<Longrightarrow> rLam a t \<approx>2 rLam b s"
+  a21: "a = b \<Longrightarrow> (rVar a) \<approx>a2 (rVar b)"
+| a22: "\<lbrakk>t1 \<approx>a2 t2; s1 \<approx>a2 s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx>a2 rApp t2 s2"
+| a23: "(a = b \<and> t \<approx>a2 s) \<or> (a \<noteq> b \<and> ((a \<leftrightarrow> b) \<bullet> t) \<approx>a2 s \<and> atom b \<notin> rfv t)\<Longrightarrow> rLam a t \<approx>a2 rLam b s"
 
 lemma fv_vars:
   fixes a::name
   assumes a1: "\<forall>x \<in> rfv t - {atom a}. pi \<bullet> x = x"
-  shows "(pi \<bullet> t) \<approx>2 ((a \<leftrightarrow> (pi \<bullet> a)) \<bullet> t)"
+  shows "(pi \<bullet> t) \<approx>a2 ((a \<leftrightarrow> (pi \<bullet> a)) \<bullet> t)"
 using a1
 apply(induct t)
 apply(auto)
@@ -222,8 +222,8 @@
 
 
 lemma 
-  assumes a1: "t \<approx>2 s"
-  shows "t \<approx> s"
+  assumes a1: "t \<approx>a2 s"
+  shows "t \<approx>a s"
 using a1
 apply(induct)
 apply(rule alpha.intros)
@@ -254,8 +254,8 @@
 sorry
 
 lemma 
-  assumes a1: "t \<approx> s"
-  shows "t \<approx>2 s"
+  assumes a1: "t \<approx>a s"
+  shows "t \<approx>a2 s"
 using a1
 apply(induct)
 apply(rule alpha2.intros)
@@ -445,12 +445,12 @@
 done
 
 lemma rlam_distinct:
-  shows "\<not>(rVar nam \<approx> rApp rlam1' rlam2')"
-  and   "\<not>(rApp rlam1' rlam2' \<approx> rVar nam)"
-  and   "\<not>(rVar nam \<approx> rLam nam' rlam')"
-  and   "\<not>(rLam nam' rlam' \<approx> rVar nam)"
-  and   "\<not>(rApp rlam1 rlam2 \<approx> rLam nam' rlam')"
-  and   "\<not>(rLam nam' rlam' \<approx> rApp rlam1 rlam2)"
+  shows "\<not>(rVar nam \<approx>a rApp rlam1' rlam2')"
+  and   "\<not>(rApp rlam1' rlam2' \<approx>a rVar nam)"
+  and   "\<not>(rVar nam \<approx>a rLam nam' rlam')"
+  and   "\<not>(rLam nam' rlam' \<approx>a rVar nam)"
+  and   "\<not>(rApp rlam1 rlam2 \<approx>a rLam nam' rlam')"
+  and   "\<not>(rLam nam' rlam' \<approx>a rApp rlam1 rlam2)"
 apply auto
 apply (erule alpha.cases)
 apply (simp_all only: rlam.distinct)

--- a/Nominal/Parser.thy	Fri Mar 26 10:55:13 2010 +0100
+++ b/Nominal/Parser.thy	Fri Mar 26 16:20:39 2010 +0100
@@ -386,15 +386,16 @@
   val fv_rsp = flat (map snd fv_rsp_pre);
   val (perms_rsp, lthy11) = prove_const_rsp Binding.empty perms
     (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
+  val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff @ rel_dists @ rel_dists_bn) alpha_equivp exhausts alpha_ts_bn lthy11;
+  val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]
+        (fn _ => asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1)) alpha_ts_bn lthy11
+(*  val _ = map tracing (map PolyML.makestring alpha_bn_rsps);*)
   fun const_rsp_tac _ =
     if !cheat_const_rsp then Skip_Proof.cheat_tac thy
-    else let val alpha_alphabn = build_alpha_alphabn fv_alpha_all alpha_inducts alpha_eq_iff lthy11
+    else let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff alpha_ts_bn lthy11a
       in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end
-  val (const_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]
-    const_rsp_tac) raw_consts lthy11
-  val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff @ rel_dists @ rel_dists_bn) alpha_equivp exhausts alpha_ts_bn lthy11a;
-  val (alpha_bn_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]
-        (fn _ => asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1)) alpha_ts_bn lthy11a
+  val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]
+    const_rsp_tac) raw_consts lthy11a
   val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) ordered_fv_ts
   val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export (qfv_names ~~ ordered_fv_ts) lthy12;
   val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts;

--- a/Nominal/ROOT.ML	Fri Mar 26 10:55:13 2010 +0100
+++ b/Nominal/ROOT.ML	Fri Mar 26 16:20:39 2010 +0100
@@ -15,8 +15,9 @@
     "ExLetRec",
     "ExTySch",
     "ExLeroy",
+    "ExPS3",
+    "ExPS7",
+    "ExCoreHaskell",
     "Test"
-(*  "ExCoreHaskell", *)
-(*  "ExPS3", *)
 (*  "ExPS6", *)
     ];

--- a/Nominal/Rsp.thy	Fri Mar 26 10:55:13 2010 +0100
+++ b/Nominal/Rsp.thy	Fri Mar 26 16:20:39 2010 +0100
@@ -3,17 +3,6 @@
 begin
 
 ML {*
-fun define_quotient_type args tac ctxt =
-let
-  val mthd = Method.SIMPLE_METHOD tac
-  val mthdt = Method.Basic (fn _ => mthd)
-  val bymt = Proof.global_terminal_proof (mthdt, NONE)
-in
-  bymt (Quotient_Type.quotient_type args ctxt)
-end
-*}
-
-ML {*
 fun const_rsp lthy const =
 let
   val nty = fastype_of (Quotient_Term.quotient_lift_const ("", const) lthy)
@@ -50,10 +39,6 @@
 *}
 
 ML {*
-fun repeat_mp thm = repeat_mp (mp OF [thm]) handle THM _ => thm
-*}
-
-ML {*
 fun prove_const_rsp bind consts tac ctxt =
 let
   val rsp_goals = map (const_rsp ctxt) consts
@@ -120,16 +105,9 @@
 
 
 ML {*
-fun mk_minimal_ss ctxt =
-  Simplifier.context ctxt empty_ss
-    setsubgoaler asm_simp_tac
-    setmksimps (mksimps [])
-*}
-
-ML {*
 fun alpha_eqvt_tac induct simps ctxt =
   rel_indtac induct THEN_ALL_NEW
-  simp_tac ((mk_minimal_ss ctxt) addsimps simps) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps simps) THEN_ALL_NEW
   REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conj_tac THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps 
@@ -153,8 +131,6 @@
 end
 *}
 
-ML {* fold_map build_alpha_eqvt *}
-
 ML {*
 fun build_alpha_eqvts funs tac ctxt =
 let
@@ -256,4 +232,44 @@
 end
 *}
 
+ML {*
+fun build_alpha_alpha_bn_gl alphas alpha_bn ctxt =
+let
+  val ty = domain_type (fastype_of alpha_bn);
+  val (l, r) = the (AList.lookup (op=) alphas ty);
+in
+  ([alpha_bn $ l $ r], ctxt)
 end
+*}
+
+ML {*
+fun prove_alpha_alphabn alphas ind simps alpha_bns ctxt =
+  prove_by_rel_induct alphas build_alpha_alpha_bn_gl ind
+    (fn _ => asm_full_simp_tac (HOL_ss addsimps simps)) alpha_bns ctxt
+*}
+
+ML {*
+fun build_rsp_gl alphas fnctn ctxt =
+let
+  val typ = domain_type (fastype_of fnctn);
+  val (argl, argr) = the (AList.lookup (op=) alphas typ);
+in
+  ([HOLogic.mk_eq (fnctn $ argl, fnctn $ argr)], ctxt)
+end
+*}
+
+ML {*
+fun fvbv_rsp_tac' simps ctxt =
+  asm_full_simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps (@{thm alpha_gen} :: simps)) THEN_ALL_NEW
+  REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps simps) THEN_ALL_NEW
+  TRY o blast_tac (claset_of ctxt)
+*}
+
+ML {*
+fun build_fvbv_rsps alphas ind simps fnctns ctxt =
+  prove_by_rel_induct alphas build_rsp_gl ind (fvbv_rsp_tac' simps) fnctns ctxt
+*}
+
+end

--- a/Nominal/Tacs.thy	Fri Mar 26 10:55:13 2010 +0100
+++ b/Nominal/Tacs.thy	Fri Mar 26 16:20:39 2010 +0100
@@ -125,5 +125,46 @@
 end
 *}
 
+ML {*
+fun repeat_mp thm = repeat_mp (mp OF [thm]) handle THM _ => thm
+*}
+
+(* Introduces an implication and immediately eliminates it by cases *)
+ML {*
+fun imp_elim_tac case_rules =
+  Subgoal.FOCUS (fn {concl, context, ...} =>
+    case term_of concl of
+      _ $ (_ $ asm $ _) =>
+        let
+          fun filter_fn case_rule = (
+            case Logic.strip_assums_hyp (prop_of case_rule) of
+              ((_ $ asmc) :: _) =>
+                let
+                  val thy = ProofContext.theory_of context
+                in
+                  Pattern.matches thy (asmc, asm)
+                end
+            | _ => false)
+          val matching_rules = filter filter_fn case_rules
+        in
+         (rtac impI THEN' rotate_tac (~1) THEN' eresolve_tac matching_rules) 1
+        end
+    | _ => no_tac)
+*}
+
+ML {*
+fun is_ex (Const ("Ex", _) $ Abs _) = true
+  | is_ex _ = false;
+*}
+
+ML {*
+fun dtyp_no_of_typ _ (TFree (n, _)) = error "dtyp_no_of_typ: Illegal free"
+  | dtyp_no_of_typ _ (TVar _) = error "dtyp_no_of_typ: Illegal schematic"
+  | dtyp_no_of_typ dts (Type (tname, Ts)) =
+      case try (find_index (curry op = tname o fst)) dts of
+        NONE => error "dtyp_no_of_typ: Illegal recursion"
+      | SOME i => i
+*}
+
 end