change fresh_fun_simp to treat occurences in assumptions and try to solve the generated subgoals
authornarboux
Mon May 21 16:19:56 2007 +0200 (2007-05-21)
changeset 23054d1bbe5afa279
parent 23053 03fe1dafa418
child 23055 34158639dc12
change fresh_fun_simp to treat occurences in assumptions and try to solve the generated subgoals
src/HOL/Nominal/nominal_fresh_fun.ML
     1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Sun May 20 18:48:52 2007 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Mon May 21 16:19:56 2007 +0200
     1.3 @@ -19,6 +19,9 @@
     1.4   tac THEN
     1.5    (EVERY (map  (fn (tac,i) => tac i) (rev tacs ~~ (length tacs downto 1))))
     1.6  
     1.7 +fun SOLVEI t = t THEN_ALL_NEW (fn i => no_tac);
     1.8 +fun TRY' tac i =  TRY (tac i);
     1.9 +
    1.10  fun gen_res_inst_tac_term instf tyinst tinst elim th i st =
    1.11    let
    1.12      val thy = theory_of_thm st;
    1.13 @@ -120,7 +123,13 @@
    1.14  
    1.15  (* A substitution tactic, FIXME : change the search function to get the inner occurence of fresh_fun (bottom -> up search ) *)
    1.16  
    1.17 -fun subst_outer_tac ctx = EqSubst.eqsubst_tac' ctx (curry (Seq.flat o (uncurry EqSubst.searchf_lr_unify_valid)));
    1.18 +val search_fun     = curry (Seq.flat o (uncurry EqSubst.searchf_lr_unify_valid));
    1.19 +val search_fun_asm = EqSubst.skip_first_asm_occs_search EqSubst.searchf_lr_unify_valid;
    1.20 +
    1.21 +fun subst_outer_tac           ctx = EqSubst.eqsubst_tac' ctx search_fun;
    1.22 +fun subst_outer_asm_tac_aux i ctx = EqSubst.eqsubst_asm_tac' ctx search_fun_asm i;
    1.23 +
    1.24 +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;
    1.25  
    1.26  fun fresh_fun_tac i thm = 
    1.27    (* Find the variable we instantiate *)
    1.28 @@ -129,7 +138,9 @@
    1.29      val ctx = Context.init_proof thy;
    1.30      val ss = simpset_of thy;
    1.31      val abs_fresh = PureThy.get_thms thy (Name "abs_fresh");
    1.32 +    val fresh_perm_app = PureThy.get_thms thy (Name "fresh_perm_app");
    1.33      val ss' = ss addsimps fresh_prod::abs_fresh;
    1.34 +    val ss'' = ss' addsimps fresh_perm_app;
    1.35      val x = hd (tl (term_vars (prop_of exI)));
    1.36      val goal = nth (prems_of thm) (i-1);
    1.37      val atom_name_opt = get_inner_fresh_fun goal;
    1.38 @@ -156,12 +167,16 @@
    1.39    let 
    1.40      val vars = term_vars (prop_of st);
    1.41      val params = Logic.strip_params (nth (prems_of st) (i-1))
    1.42 -  in
    1.43 -   (subst_outer_tac ctx fresh_fun_app' i THENL 
    1.44 -   [rtac pt_name_inst,
    1.45 -    rtac at_name_inst,
    1.46 -    (K all_tac),
    1.47 -    inst_fresh vars params]) st
    1.48 +    val post_rewrite_tacs =  
    1.49 +          [rtac pt_name_inst,
    1.50 +           rtac at_name_inst,
    1.51 +           TRY' (SOLVEI (NominalPermeq.finite_guess_tac ss'')),
    1.52 +           inst_fresh vars params THEN'
    1.53 +           (TRY' (SOLVEI (NominalPermeq.fresh_guess_tac ss''))) THEN'
    1.54 +           (TRY' (SOLVEI (asm_full_simp_tac ss'')))] 
    1.55 +  in 
    1.56 +   ((subst_outer_asm_tac ctx fresh_fun_app' i THENL post_rewrite_tacs) ORELSE 
    1.57 +    (subst_outer_tac     ctx fresh_fun_app' i THENL post_rewrite_tacs)) st
    1.58    end)) thm
    1.59    
    1.60    end