# HG changeset patch
# User narboux
# Date 1179757196 -7200
# Node ID d1bbe5afa279c8ec84414fe7c756422dc17fe2b3
# Parent  03fe1dafa4189a415d49608c1d173ef2a482d0d3
change fresh_fun_simp to treat occurences in assumptions and try to solve the generated subgoals

diff -r 03fe1dafa418 -r d1bbe5afa279 src/HOL/Nominal/nominal_fresh_fun.ML
--- a/src/HOL/Nominal/nominal_fresh_fun.ML	Sun May 20 18:48:52 2007 +0200
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Mon May 21 16:19:56 2007 +0200
@@ -19,6 +19,9 @@
  tac THEN
   (EVERY (map  (fn (tac,i) => tac i) (rev tacs ~~ (length tacs downto 1))))
 
+fun SOLVEI t = t THEN_ALL_NEW (fn i => no_tac);
+fun TRY' tac i =  TRY (tac i);
+
 fun gen_res_inst_tac_term instf tyinst tinst elim th i st =
   let
     val thy = theory_of_thm st;
@@ -120,7 +123,13 @@
 
 (* A substitution tactic, FIXME : change the search function to get the inner occurence of fresh_fun (bottom -> up search ) *)
 
-fun subst_outer_tac ctx = EqSubst.eqsubst_tac' ctx (curry (Seq.flat o (uncurry EqSubst.searchf_lr_unify_valid)));
+val search_fun     = curry (Seq.flat o (uncurry EqSubst.searchf_lr_unify_valid));
+val search_fun_asm = EqSubst.skip_first_asm_occs_search EqSubst.searchf_lr_unify_valid;
+
+fun subst_outer_tac           ctx = EqSubst.eqsubst_tac' ctx search_fun;
+fun subst_outer_asm_tac_aux i ctx = EqSubst.eqsubst_asm_tac' ctx search_fun_asm i;
+
+fun subst_outer_asm_tac ctx th =  curry (curry (FIRST' (map uncurry (map uncurry (map subst_outer_asm_tac_aux (1 upto Thm.nprems_of th)))))) ctx th;
 
 fun fresh_fun_tac i thm = 
   (* Find the variable we instantiate *)
@@ -129,7 +138,9 @@
     val ctx = Context.init_proof thy;
     val ss = simpset_of thy;
     val abs_fresh = PureThy.get_thms thy (Name "abs_fresh");
+    val fresh_perm_app = PureThy.get_thms thy (Name "fresh_perm_app");
     val ss' = ss addsimps fresh_prod::abs_fresh;
+    val ss'' = ss' addsimps fresh_perm_app;
     val x = hd (tl (term_vars (prop_of exI)));
     val goal = nth (prems_of thm) (i-1);
     val atom_name_opt = get_inner_fresh_fun goal;
@@ -156,12 +167,16 @@
   let 
     val vars = term_vars (prop_of st);
     val params = Logic.strip_params (nth (prems_of st) (i-1))
-  in
-   (subst_outer_tac ctx fresh_fun_app' i THENL 
-   [rtac pt_name_inst,
-    rtac at_name_inst,
-    (K all_tac),
-    inst_fresh vars params]) st
+    val post_rewrite_tacs =  
+          [rtac pt_name_inst,
+           rtac at_name_inst,
+           TRY' (SOLVEI (NominalPermeq.finite_guess_tac ss'')),
+           inst_fresh vars params THEN'
+           (TRY' (SOLVEI (NominalPermeq.fresh_guess_tac ss''))) THEN'
+           (TRY' (SOLVEI (asm_full_simp_tac ss'')))] 
+  in 
+   ((subst_outer_asm_tac ctx fresh_fun_app' i THENL post_rewrite_tacs) ORELSE 
+    (subst_outer_tac     ctx fresh_fun_app' i THENL post_rewrite_tacs)) st
   end)) thm
   
   end