--- a/Nominal/ExCoreHaskell.thy	Fri Mar 26 09:23:23 2010 +0100
+++ b/Nominal/ExCoreHaskell.thy	Fri Mar 26 10:07:26 2010 +0100
@@ -6,7 +6,6 @@
 
 ML {* val _ = recursive := false *}
 ML {* val _ = cheat_const_rsp := true *}
-ML {* val _ = cheat_alpha_bn_rsp := true *}
 atom_decl var
 atom_decl tvar
 

--- a/Nominal/ExLet.thy	Fri Mar 26 09:23:23 2010 +0100
+++ b/Nominal/ExLet.thy	Fri Mar 26 10:07:26 2010 +0100
@@ -22,8 +22,6 @@
   "bn Lnil = {}"
 | "bn (Lcons x t l) = {atom x} \<union> (bn l)"
 
-
-
 thm trm_lts.fv
 thm trm_lts.eq_iff
 thm trm_lts.bn

--- a/Nominal/Fv.thy	Fri Mar 26 09:23:23 2010 +0100
+++ b/Nominal/Fv.thy	Fri Mar 26 10:07:26 2010 +0100
@@ -198,11 +198,6 @@
       if a = b then a else
       HOLogic.mk_binop @{const_name sup} (a, b)) (rev sets) noatoms;
   val mk_inter = foldr1 (HOLogic.mk_binop @{const_name inf})
-  fun mk_conjl props =
-    fold (fn a => fn b =>
-      if a = @{term True} then b else
-      if b = @{term True} then a else
-      HOLogic.mk_conj (a, b)) (rev props) @{term True};
   fun mk_diff a b =
     if b = noatoms then a else
     if b = a then noatoms else
@@ -597,102 +592,7 @@
 end
 *}
 
-(*
-atom_decl name
-datatype lam =
-  VAR "name"
-| APP "lam" "lam"
-| LET "bp" "lam"
-and bp =
-  BP "name" "lam"
-primrec
-  bi::"bp \<Rightarrow> atom set"
-where
-  "bi (BP x t) = {atom x}"
-setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Fv.lam") 2 *}
-local_setup {*
-  snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.lam")
-  [[[], [], [(SOME (@{term bi}, true), 0, 1)]], [[]]] [(@{term bi}, 1, [[0]])] *}
-print_theorems
-*)
 
-(*atom_decl name
-datatype rtrm1 =
-  rVr1 "name"
-| rAp1 "rtrm1" "rtrm1"
-| rLm1 "name" "rtrm1"        --"name is bound in trm1"
-| rLt1 "bp" "rtrm1" "rtrm1"   --"all variables in bp are bound in the 2nd trm1"
-and bp =
-  BUnit
-| BVr "name"
-| BPr "bp" "bp"
-primrec
-  bv1
-where
-  "bv1 (BUnit) = {}"
-| "bv1 (BVr x) = {atom x}"
-| "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)"
-setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Fv.rtrm1") 2 *}
-local_setup {*
-  snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.rtrm1")
-  [[[], [], [(NONE, 0, 1)], [(SOME (@{term bv1}, false), 0, 2)]],
-  [[], [], []]] [(@{term bv1}, 1, [[], [0], [0, 1]])] *}
-print_theorems
-*)
-
-(*
-atom_decl name
-datatype rtrm5 =
-  rVr5 "name"
-| rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)"
-and rlts =
-  rLnil
-| rLcons "name" "rtrm5" "rlts"
-primrec
-  rbv5
-where
-  "rbv5 rLnil = {}"
-| "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)"
-setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Fv.rtrm5") 2 *}
-local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.rtrm5")
-  [[[], [(SOME (@{term rbv5}, false), 0, 1)]], [[], []]] [(@{term rbv5}, 1, [[], [0, 2]])] *}
-print_theorems
-*)
-
-ML {*
-fun alpha_inj_tac dist_inj intrs elims =
-  SOLVED' (asm_full_simp_tac (HOL_ss addsimps intrs)) ORELSE'
-  (rtac @{thm iffI} THEN' RANGE [
-     (eresolve_tac elims THEN_ALL_NEW
-       asm_full_simp_tac (HOL_ss addsimps dist_inj)
-     ),
-     asm_full_simp_tac (HOL_ss addsimps intrs)])
-*}
-
-ML {*
-fun build_alpha_inj_gl thm =
-  let
-    val prop = prop_of thm;
-    val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop);
-    val hyps = map HOLogic.dest_Trueprop (Logic.strip_imp_prems prop);
-    fun list_conj l = foldr1 HOLogic.mk_conj l;
-  in
-    if hyps = [] then concl
-    else HOLogic.mk_eq (concl, list_conj hyps)
-  end;
-*}
-
-ML {*
-fun build_alpha_inj intrs dist_inj elims ctxt =
-let
-  val ((_, thms_imp), ctxt') = Variable.import false intrs ctxt;
-  val gls = map (HOLogic.mk_Trueprop o build_alpha_inj_gl) thms_imp;
-  fun tac _ = alpha_inj_tac dist_inj intrs elims 1;
-  val thms = map (fn gl => Goal.prove ctxt' [] [] gl tac) gls;
-in
-  Variable.export ctxt' ctxt thms
-end
-*}
 
 ML {*
 fun build_alpha_sym_trans_gl alphas (x, y, z) =
@@ -746,8 +646,8 @@
 fun reflp_tac induct eq_iff ctxt =
   rtac induct THEN_ALL_NEW
   simp_tac ((mk_minimal_ss ctxt) addsimps eq_iff) THEN_ALL_NEW
-  split_conjs THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]}
-  THEN_ALL_NEW split_conjs THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps
+  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
        add_0_left supp_zero_perm Int_empty_left split_conv})
 *}
@@ -799,12 +699,12 @@
 
 ML {*
 fun symp_tac induct inj eqvt ctxt =
-  ind_tac induct THEN_ALL_NEW
-  simp_tac ((mk_minimal_ss ctxt) addsimps inj) THEN_ALL_NEW split_conjs
+  rel_indtac induct THEN_ALL_NEW
+  simp_tac ((mk_minimal_ss ctxt) addsimps inj) THEN_ALL_NEW split_conj_tac
   THEN_ALL_NEW
   REPEAT o etac @{thm exi_neg}
   THEN_ALL_NEW
-  split_conjs THEN_ALL_NEW
+  split_conj_tac THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps @{thms supp_minus_perm minus_add[symmetric]}) THEN_ALL_NEW
   TRY o (rtac @{thm alpha_gen_compose_sym2} ORELSE' rtac @{thm alpha_gen_compose_sym}) THEN_ALL_NEW
   (asm_full_simp_tac (HOL_ss addsimps (eqvt @ all_eqvts ctxt)))
@@ -864,12 +764,12 @@
 
 ML {*
 fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt =
-  ind_tac induct THEN_ALL_NEW
+  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
-  split_conjs THEN_ALL_NEW REPEAT o (eetac @{thm exi_sum} ctxt) THEN_ALL_NEW split_conjs
+  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_conjs THEN_ALL_NEW
+  THEN_ALL_NEW split_conj_tac THEN_ALL_NEW
   TRY o (etac @{thm alpha_gen_compose_trans2} ORELSE' etac @{thm alpha_gen_compose_trans}) THEN_ALL_NEW
   (asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ eqvt @ term_inj @ distinct)))
 *}
@@ -955,7 +855,7 @@
 ML {*
 fun supports_tac perm =
   simp_tac (HOL_ss addsimps @{thms supports_def not_in_union} @ perm) THEN_ALL_NEW (
-    REPEAT o rtac allI THEN' REPEAT o rtac impI THEN' split_conjs THEN'
+    REPEAT o rtac allI THEN' REPEAT o rtac impI THEN' split_conj_tac THEN'
     asm_full_simp_tac (HOL_ss addsimps @{thms fresh_def[symmetric]
       swap_fresh_fresh fresh_atom swap_at_base_simps(3) swap_atom_image_fresh
       supp_fset_to_set supp_fmap_atom}))
@@ -1009,7 +909,7 @@
 *}
 
 ML {*
-fun fs_tac induct supports = ind_tac induct THEN_ALL_NEW (
+fun fs_tac induct supports = rel_indtac induct THEN_ALL_NEW (
   rtac @{thm supports_finite} THEN' resolve_tac supports) THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps @{thms supp_atom supp_atom_image supp_fset_to_set
     supp_fmap_atom finite_insert finite.emptyI finite_Un finite_supp})
@@ -1079,7 +979,7 @@
 
 ML {*
 fun supp_eq_tac ind fv perm eqiff ctxt =
-  ind_tac ind THEN_ALL_NEW
+  rel_indtac ind THEN_ALL_NEW
   asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW
   asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_Abs[symmetric]}) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW
@@ -1099,32 +999,7 @@
   simp_tac (HOL_ss addsimps @{thms Collect_const finite.emptyI})
 *}
 
-(* Given function for buildng a goal for an input, prepares a
-   one common goals for all the inputs and proves it by induction
-   together *)
-ML {*
-fun prove_by_induct tys build_goal ind utac inputs ctxt =
-let
-  val names = Datatype_Prop.make_tnames tys;
-  val (names', ctxt') = Variable.variant_fixes names ctxt;
-  val frees = map Free (names' ~~ tys);
-  val (gls_lists, ctxt'') = fold_map (build_goal (tys ~~ frees)) inputs ctxt';
-  val gls = flat gls_lists;
-  fun trm_gls_map t = filter (exists_subterm (fn s => s = t)) gls;
-  val trm_gl_lists = map trm_gls_map frees;
-  val trm_gl_insts = map2 (fn n => fn l => [NONE, if l = [] then NONE else SOME n]) names' trm_gl_lists
-  val trm_gls = map mk_conjl trm_gl_lists;
-  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj trm_gls);
-  fun tac {context,...} = ((fn _ => print_tac (PolyML.makestring names')) THEN'
-    InductTacs.induct_rules_tac context [(flat trm_gl_insts)] [ind]
-    THEN_ALL_NEW split_conjs THEN_ALL_NEW utac) 1
-  val th_loc = Goal.prove ctxt'' [] [] gl tac
-  val ths_loc = HOLogic.conj_elims th_loc
-  val ths = Variable.export ctxt'' ctxt ths_loc
-in
-  filter (fn x => not (prop_of x = prop_of @{thm TrueI})) ths
-end
-*}
+
 
 ML {*
 fun build_eqvt_gl pi frees fnctn ctxt =
@@ -1151,34 +1026,6 @@
 *}
 
 ML {*
-fun prove_by_alpha_induct alphas build_goal ind utac inputs ctxt =
-let
-  val tys = map (domain_type o fastype_of) alphas;
-  val names = Datatype_Prop.make_tnames tys;
-  val (namesl, ctxt') = Variable.variant_fixes names ctxt;
-  val (namesr, ctxt'') = Variable.variant_fixes names ctxt';
-  val freesl = map Free (namesl ~~ tys);
-  val freesr = map Free (namesr ~~ tys);
-  val (gls_lists, ctxt'') = fold_map (build_goal (tys ~~ (freesl ~~ freesr))) inputs ctxt'';
-  val gls = flat gls_lists;
-  fun trm_gls_map t = filter (exists_subterm (fn s => s = t)) gls;
-  val trm_gl_lists = map trm_gls_map freesl;
-  val trm_gls = map mk_conjl trm_gl_lists;
-  val pgls = map
-    (fn ((alpha, gl), (l, r)) => HOLogic.mk_imp (alpha $ l $ r, gl)) 
-    ((alphas ~~ trm_gls) ~~ (freesl ~~ freesr))
-  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj pgls);
-(*  val _ = tracing (PolyML.makestring gl); *)
-  fun tac {context,...} = (ind_tac ind THEN_ALL_NEW split_conjs THEN_ALL_NEW utac) 1
-  val th_loc = Goal.prove ctxt'' [] [] gl tac
-  val ths_loc = HOLogic.conj_elims th_loc
-  val ths = Variable.export ctxt'' ctxt ths_loc
-in
-  filter (fn x => not (prop_of x = prop_of @{thm TrueI})) ths
-end
-*}
-
-ML {*
 fun build_rsp_gl alphas fnctn ctxt =
 let
   val typ = domain_type (fastype_of fnctn);
@@ -1199,7 +1046,7 @@
 
 ML {*
 fun build_fvbv_rsps alphas ind simps fnctns ctxt =
-  prove_by_alpha_induct alphas build_rsp_gl ind (fvbv_rsp_tac' simps ctxt) fnctns ctxt
+  prove_by_rel_induct alphas build_rsp_gl ind (fvbv_rsp_tac' simps) fnctns ctxt
 *}
 
 end

--- a/Nominal/Parser.thy	Fri Mar 26 09:23:23 2010 +0100
+++ b/Nominal/Parser.thy	Fri Mar 26 10:07:26 2010 +0100
@@ -286,12 +286,10 @@
 end
 *}
 
+ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *}
 ML {* val cheat_equivp = Unsynchronized.ref false *}
-ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *}
-ML {* val cheat_bn_rsp = Unsynchronized.ref false *}
 ML {* val cheat_fv_rsp = Unsynchronized.ref false *}
 ML {* val cheat_const_rsp = Unsynchronized.ref false *}
-ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref false *}
 
 ML {* fun map_option _ NONE = NONE
         | map_option f (SOME x) = SOME (f x) *}
@@ -342,7 +340,7 @@
     (rel_distinct ~~ alpha_ts_nobn));
   val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases)
     ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn))
-  val alpha_eq_iff = build_alpha_inj alpha_intros (inject @ distincts) alpha_cases lthy4
+  val alpha_eq_iff = build_rel_inj alpha_intros (inject @ distincts) alpha_cases lthy4
   val _ = tracing "Proving equivariance";
   val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4
   val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct (fv_def @ raw_perm_def) (fv_ts_nobn @ fv_ts_bn) lthy5
@@ -394,13 +392,9 @@
       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 _ =>
-      if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy
-      else
-        let val alpha_bn_rsp_pre = flat (map (prove_alpha_bn_rsp alpha_ts_nobn alpha_inducts exhausts
-        (alpha_eq_iff @ rel_dists @ rel_dists_bn) (alpha_equivp) lthy11a) (alpha_ts_bn ~~ bn_nos)) in
-        asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end)) alpha_ts_bn lthy11a
+        (fn _ => asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1)) alpha_ts_bn 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/Rsp.thy	Fri Mar 26 09:23:23 2010 +0100
+++ b/Nominal/Rsp.thy	Fri Mar 26 10:07:26 2010 +0100
@@ -1,5 +1,5 @@
 theory Rsp
-imports Abs
+imports Abs Tacs
 begin
 
 ML {*
@@ -74,12 +74,8 @@
 *}
 
 ML {*
-fun ind_tac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct
-*}
-
-ML {*
 fun fvbv_rsp_tac induct fvbv_simps ctxt =
-  ind_tac induct THEN_ALL_NEW
+  rel_indtac induct THEN_ALL_NEW
   (TRY o rtac @{thm TrueI}) THEN_ALL_NEW
   asm_full_simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps)) THEN_ALL_NEW
@@ -92,13 +88,12 @@
 fun sym_eqvts ctxt = map (fn x => sym OF [x]) (Nominal_ThmDecls.get_eqvts_thms ctxt)
 fun all_eqvts ctxt =
   Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt
-val split_conjs = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)
 *}
 
 ML {*
 fun constr_rsp_tac inj rsp =
   REPEAT o rtac impI THEN'
-  simp_tac (HOL_ss addsimps inj) THEN' split_conjs THEN_ALL_NEW
+  simp_tac (HOL_ss addsimps inj) THEN' split_conj_tac THEN_ALL_NEW
   (asm_simp_tac HOL_ss THEN_ALL_NEW (
    REPEAT o rtac @{thm exI[of _ "0 :: perm"]} THEN_ALL_NEW
    simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW
@@ -107,23 +102,6 @@
   ))
 *}
 
-(* Testing code
-local_setup {* snd o prove_const_rsp @{binding fv_rtrm2_rsp} [@{term rbv2}]
-  (fn _ => fv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.inducts(2)} @{thms fv_rtrm2_fv_rassign.simps} 1) *}*)
-
-(*ML {*
-  val rsp_goals = map (const_rsp @{context}) [@{term rbv2}]
-  val (fixed, user_goals) = split_list (map (get_rsp_goal @{theory}) rsp_goals)
-  val fixed' = distinct (op =) (flat fixed)
-  val user_goal = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj user_goals)
-*}
-prove ug: {* user_goal *}
-ML_prf {*
-val induct = @{thm alpha_rtrm2_alpha_rassign.inducts(2)}
-val fv_simps = @{thms rbv2.simps}
-*} 
-*)
-
 ML {*
 fun perm_arg arg =
 let
@@ -150,13 +128,13 @@
 
 ML {*
 fun alpha_eqvt_tac induct simps ctxt =
-  ind_tac induct THEN_ALL_NEW
+  rel_indtac induct THEN_ALL_NEW
   simp_tac ((mk_minimal_ss ctxt) addsimps simps) THEN_ALL_NEW
-  REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conjs 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 
     @{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alpha_gen}) THEN_ALL_NEW
-  (split_conjs THEN_ALL_NEW TRY o resolve_tac
+  (split_conj_tac THEN_ALL_NEW TRY o resolve_tac
     @{thms fresh_star_permute_iff[of "- p", THEN iffD1] permute_eq_iff[of "- p", THEN iffD1]})
   THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps (@{thms split_conv permute_minus_cancel permute_plus permute_eqvt[symmetric]} @ all_eqvts ctxt @ simps))
@@ -231,6 +209,8 @@
 end
 *}
 
+(** alpha_bn_rsp **)
+
 lemma equivp_rspl:
   "equivp r \<Longrightarrow> r a b \<Longrightarrow> r a c = r b c"
   unfolding equivp_reflp_symp_transp symp_def transp_def 
@@ -242,39 +222,38 @@
   by blast
 
 ML {*
-fun prove_alpha_bn_rsp alphas inducts exhausts inj_dis equivps ctxt (alpha_bn, n) =
+fun alpha_bn_rsp_tac simps res exhausts a ctxt =
+  rtac allI THEN_ALL_NEW
+  case_rules_tac ctxt a exhausts THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps simps) THEN_ALL_NEW
+  TRY o REPEAT_ALL_NEW (rtac @{thm arg_cong2[of _ _ _ _ "op \<and>"]}) THEN_ALL_NEW
+  TRY o eresolve_tac res THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps simps);
+*}
+
+
+ML {*
+fun build_alpha_bn_rsp_gl a alphas alpha_bn ctxt =
 let
-  val alpha = nth alphas n;
-  val ty = domain_type (fastype_of alpha);
-  val ([x, y, a], ctxt') = Variable.variant_fixes ["x","y","a"] ctxt;
-  val [l, r] = map (fn x => (Free (x, ty))) [x, y]
-  val lhs = HOLogic.mk_Trueprop (alpha $ l $ r)
-  val g1 =
-    Logic.mk_implies (lhs,
-      HOLogic.mk_Trueprop (HOLogic.mk_all (a, ty,
-        HOLogic.mk_eq (alpha_bn $ l $ Bound 0, alpha_bn $ r $ Bound 0))));
-  val g2 =
-    Logic.mk_implies (lhs,
-      HOLogic.mk_Trueprop (HOLogic.mk_all (a, ty,
-        HOLogic.mk_eq (alpha_bn $ Bound 0 $ l, alpha_bn $ Bound 0 $ r))));
-  val resl = map (fn x => @{thm equivp_rspl} OF [x]) equivps;
-  val resr = map (fn x => @{thm equivp_rspr} OF [x]) equivps;
-  fun tac {context, ...} = (
-    etac (nth inducts n) THEN_ALL_NEW
-    (TRY o rtac @{thm TrueI}) THEN_ALL_NEW rtac allI THEN_ALL_NEW
-    split_conjs THEN_ALL_NEW
-    InductTacs.case_rule_tac context a (nth exhausts n) THEN_ALL_NEW
-    asm_full_simp_tac (HOL_ss addsimps inj_dis) THEN_ALL_NEW
-    TRY o REPEAT_ALL_NEW (rtac @{thm arg_cong2[of _ _ _ _ "op \<and>"]}) THEN_ALL_NEW
-    TRY o eresolve_tac (resl @ resr) THEN_ALL_NEW
-    asm_full_simp_tac (HOL_ss addsimps inj_dis)
-  ) 1;
-  val t1 = Goal.prove ctxt [] [] g1 tac;
-  val t2 = Goal.prove ctxt [] [] g2 tac;
+  val ty = domain_type (fastype_of alpha_bn);
+  val (l, r) = the (AList.lookup (op=) alphas ty);
 in
-  Variable.export ctxt' ctxt [t1, t2]
+  ([HOLogic.mk_all (a, ty, HOLogic.mk_eq (alpha_bn $ l $ Bound 0, alpha_bn $ r $ Bound 0)),
+    HOLogic.mk_all (a, ty, HOLogic.mk_eq (alpha_bn $ Bound 0 $ l, alpha_bn $ Bound 0 $ r))], ctxt)
 end
 *}
 
+ML {*
+fun prove_alpha_bn_rsp alphas ind simps equivps exhausts alpha_bns ctxt =
+let
+  val ([a], ctxt') = Variable.variant_fixes ["a"] ctxt;
+  val resl = map (fn x => @{thm equivp_rspl} OF [x]) equivps;
+  val resr = map (fn x => @{thm equivp_rspr} OF [x]) equivps;
+  val ths_loc = prove_by_rel_induct alphas (build_alpha_bn_rsp_gl a) ind
+    (alpha_bn_rsp_tac simps (resl @ resr) exhausts a) alpha_bns ctxt
+in
+  Variable.export ctxt' ctxt ths_loc
+end
+*}
 
 end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Tacs.thy	Fri Mar 26 10:07:26 2010 +0100
@@ -0,0 +1,129 @@
+theory Tacs
+imports Main
+begin
+
+(* General not-nominal/quotient functionality useful for proving *)
+
+(* A version of case_rule_tac that takes more exhaust rules *)
+ML {*
+fun case_rules_tac ctxt0 s rules i st =
+let
+  val (_, ctxt) = Variable.focus_subgoal i st ctxt0;
+  val ty = fastype_of (ProofContext.read_term_schematic ctxt s)
+  fun exhaust_ty thm = fastype_of (hd (Induct.vars_of (Thm.term_of (Thm.cprem_of thm 1))));
+  val ty_rules = filter (fn x => exhaust_ty x = ty) rules;
+in
+  InductTacs.case_rule_tac ctxt0 s (hd ty_rules) i st
+end
+*}
+
+ML {*
+fun mk_conjl props =
+  fold (fn a => fn b =>
+    if a = @{term True} then b else
+    if b = @{term True} then a else
+    HOLogic.mk_conj (a, b)) (rev props) @{term True};
+*}
+
+ML {*
+val split_conj_tac = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)
+*}
+
+(* Given function for buildng a goal for an input, prepares a
+   one common goals for all the inputs and proves it by induction
+   together *)
+ML {*
+fun prove_by_induct tys build_goal ind utac inputs ctxt =
+let
+  val names = Datatype_Prop.make_tnames tys;
+  val (names', ctxt') = Variable.variant_fixes names ctxt;
+  val frees = map Free (names' ~~ tys);
+  val (gls_lists, ctxt'') = fold_map (build_goal (tys ~~ frees)) inputs ctxt';
+  val gls = flat gls_lists;
+  fun trm_gls_map t = filter (exists_subterm (fn s => s = t)) gls;
+  val trm_gl_lists = map trm_gls_map frees;
+  val trm_gl_insts = map2 (fn n => fn l => [NONE, if l = [] then NONE else SOME n]) names' trm_gl_lists
+  val trm_gls = map mk_conjl trm_gl_lists;
+  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj trm_gls);
+  fun tac {context,...} = (
+    InductTacs.induct_rules_tac context [(flat trm_gl_insts)] [ind]
+    THEN_ALL_NEW split_conj_tac THEN_ALL_NEW utac) 1
+  val th_loc = Goal.prove ctxt'' [] [] gl tac
+  val ths_loc = HOLogic.conj_elims th_loc
+  val ths = Variable.export ctxt'' ctxt ths_loc
+in
+  filter (fn x => not (prop_of x = prop_of @{thm TrueI})) ths
+end
+*}
+
+(* An induction for a single relation is "R x y \<Longrightarrow> P x y"
+   but for multiple relations is "(R1 x y \<longrightarrow> P x y) \<and> (R2 a b \<longrightarrow> P2 a b)" *)
+ML {*
+fun rel_indtac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct
+*}
+
+ML {*
+fun prove_by_rel_induct alphas build_goal ind utac inputs ctxt =
+let
+  val tys = map (domain_type o fastype_of) alphas;
+  val names = Datatype_Prop.make_tnames tys;
+  val (namesl, ctxt') = Variable.variant_fixes names ctxt;
+  val (namesr, ctxt'') = Variable.variant_fixes names ctxt';
+  val freesl = map Free (namesl ~~ tys);
+  val freesr = map Free (namesr ~~ tys);
+  val (gls_lists, ctxt'') = fold_map (build_goal (tys ~~ (freesl ~~ freesr))) inputs ctxt'';
+  val gls = flat gls_lists;
+  fun trm_gls_map t = filter (exists_subterm (fn s => s = t)) gls;
+  val trm_gl_lists = map trm_gls_map freesl;
+  val trm_gls = map mk_conjl trm_gl_lists;
+  val pgls = map
+    (fn ((alpha, gl), (l, r)) => HOLogic.mk_imp (alpha $ l $ r, gl)) 
+    ((alphas ~~ trm_gls) ~~ (freesl ~~ freesr))
+  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj pgls);
+  fun tac {context,...} = (rel_indtac ind THEN_ALL_NEW split_conj_tac THEN_ALL_NEW
+    TRY o rtac @{thm TrueI} THEN_ALL_NEW utac context) 1
+  val th_loc = Goal.prove ctxt'' [] [] gl tac
+  val ths_loc = HOLogic.conj_elims th_loc
+  val ths = Variable.export ctxt'' ctxt ths_loc
+in
+  filter (fn x => not (prop_of x = prop_of @{thm TrueI})) ths
+end
+*}
+(* Code for transforming an inductive relation to a function *)
+ML {*
+fun rel_inj_tac dist_inj intrs elims =
+  SOLVED' (asm_full_simp_tac (HOL_ss addsimps intrs)) ORELSE'
+  (rtac @{thm iffI} THEN' RANGE [
+     (eresolve_tac elims THEN_ALL_NEW
+       asm_full_simp_tac (HOL_ss addsimps dist_inj)
+     ),
+     asm_full_simp_tac (HOL_ss addsimps intrs)])
+*}
+
+ML {*
+fun build_rel_inj_gl thm =
+  let
+    val prop = prop_of thm;
+    val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop);
+    val hyps = map HOLogic.dest_Trueprop (Logic.strip_imp_prems prop);
+    fun list_conj l = foldr1 HOLogic.mk_conj l;
+  in
+    if hyps = [] then concl
+    else HOLogic.mk_eq (concl, list_conj hyps)
+  end;
+*}
+
+ML {*
+fun build_rel_inj intrs dist_inj elims ctxt =
+let
+  val ((_, thms_imp), ctxt') = Variable.import false intrs ctxt;
+  val gls = map (HOLogic.mk_Trueprop o build_rel_inj_gl) thms_imp;
+  fun tac _ = rel_inj_tac dist_inj intrs elims 1;
+  val thms = map (fn gl => Goal.prove ctxt' [] [] gl tac) gls;
+in
+  Variable.export ctxt' ctxt thms
+end
+*}
+
+end
+