--- a/Nominal/Fv.thy	Wed Mar 03 14:46:14 2010 +0100
+++ b/Nominal/Fv.thy	Wed Mar 03 17:51:47 2010 +0100
@@ -1,5 +1,5 @@
 theory Fv
-imports "Nominal2_Atoms" "Abs" "Perm" (* For testing *)
+imports "Nominal2_Atoms" "Abs" "Perm" "Rsp"
 begin
 
 (* Bindings are given as a list which has a length being equal
@@ -312,29 +312,34 @@
 *}
 
 ML {*
-fun reflp_tac induct inj =
+fun reflp_tac induct inj ctxt =
   rtac induct THEN_ALL_NEW
-  asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW
-(*  TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW*)
-  (rtac @{thm exI[of _ "0 :: perm"]} THEN'
-   asm_full_simp_tac (HOL_ss addsimps
-     @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv}))
+  simp_tac ((mk_minimal_ss ctxt) addsimps inj) 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
+     @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv
+       add_0_left supp_zero_perm Int_empty_left})
 *}
 
+
 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)
 by auto
 
 ML {*
-fun symp_tac induct inj eqvt =
-  (((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW
-  asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW
-  (REPEAT o etac conjE THEN' etac @{thm exi_neg} THEN' REPEAT o etac conjE THEN'
-  (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI))) THEN_ALL_NEW
-  (asm_full_simp_tac HOL_ss) THEN_ALL_NEW
-  (etac @{thm alpha_gen_compose_sym} THEN' 
-    (asm_full_simp_tac (HOL_ss addsimps (@{thm atom_eqvt} :: eqvt)))))
+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
+  THEN_ALL_NEW
+  REPEAT o etac @{thm exi_neg}
+  THEN_ALL_NEW
+  split_conjs THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps @{thms supp_minus_perm minus_add[symmetric]}) THEN_ALL_NEW
+  (rtac @{thm alpha_gen_compose_sym} THEN' RANGE [
+    (asm_full_simp_tac (HOL_ss addsimps @{thms plus_perm_eq})),
+    (asm_full_simp_tac (HOL_ss addsimps (eqvt @ all_eqvts ctxt)))
+  ])
 *}
 
 ML {*
@@ -400,8 +405,8 @@
 let
   val ([x, y, z], ctxt') = Variable.variant_fixes ["x","y","z"] ctxt;
   val (reflg, (symg, transg)) = build_alpha_refl_gl alphas (x, y, z)
-  fun reflp_tac' _ = reflp_tac term_induct alpha_inj 1;
-  fun symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt 1;
+  fun reflp_tac' _ = reflp_tac term_induct alpha_inj ctxt 1;
+  fun symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt ctxt 1;
   fun transp_tac' _ = transp_tac ctxt alpha_induct alpha_inj term_inj distinct cases eqvt 1;
   val reflt = Goal.prove ctxt' [] [] reflg reflp_tac';
   val symt = Goal.prove ctxt' [] [] symg symp_tac';

--- a/Nominal/Rsp.thy	Wed Mar 03 14:46:14 2010 +0100
+++ b/Nominal/Rsp.thy	Wed Mar 03 17:51:47 2010 +0100
@@ -146,7 +146,9 @@
 by auto
 
 ML {*
-  fun indtac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct
+fun ind_tac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct
+*}
+ML {*
   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)
@@ -161,7 +163,7 @@
 
 ML {*
 fun alpha_eqvt_tac induct simps ctxt =
-  indtac induct THEN_ALL_NEW
+  ind_tac 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
   asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW

--- a/Nominal/Test.thy	Wed Mar 03 14:46:14 2010 +0100
+++ b/Nominal/Test.thy	Wed Mar 03 17:51:47 2010 +0100
@@ -1,5 +1,5 @@
 theory Test
-imports "Parser"
+imports "Parser" "../Attic/Prove"
 begin
 
 text {* weirdo example from Peter Sewell's bestiary *}
@@ -14,6 +14,66 @@
 thm alpha_weird_raw.intros[no_vars]
 thm fv_weird_raw.simps[no_vars]
 
+thm eqvts
+
+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 {*
+(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)) *}
+
+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
+  )
+*}
+
+
+prove {* (snd o snd) (build_alpha_refl_gl [@{term alpha_weird_raw}] ("x","y","z")) *}
+ML_prf {*
+fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt =
+  ind_tac 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
+*}
+
+apply (tactic {* transp_tac @{context} @{thm alpha_weird_raw.induct} @{thms weird_inj}  @{thms weird_raw.inject} @{thms weird_raw.distinct} @{thms alpha_weird_raw.cases} @{thms alpha_eqvt} 1 *})
+apply (simp_all)
+apply (erule alpha_gen_compose_trans)
+apply assumption
+apply (simp add: alpha_eqvt)
+defer defer
+apply (erule alpha_gen_compose_trans)
+apply assumption
+apply (simp add: alpha_eqvt)
+apply (subgoal_tac "pia + pb + (pib + pa) = (pia + pib) + (pb + pa)")
+apply simp
+apply (erule alpha_gen_compose_trans)
+apply assumption
+apply (simp add: alpha_eqvt)
+sorry
+
+
 
 abbreviation "WBind \<equiv> WBind_raw"
 abbreviation "WP \<equiv> WP_raw"