update fresh_fun_simp for debugging purposes
authornarboux
Tue Apr 24 18:06:04 2007 +0200 (2007-04-24)
changeset 2278785e7e32e6004
parent 22786 d8d7a53ffb63
child 22788 3038bd211582
update fresh_fun_simp for debugging purposes
src/HOL/Nominal/nominal_fresh_fun.ML
     1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Tue Apr 24 17:16:55 2007 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Tue Apr 24 18:06:04 2007 +0200
     1.3 @@ -57,7 +57,7 @@
     1.4  compile time. *)
     1.5  
     1.6  val at_exists_fresh' = thm "at_exists_fresh'";
     1.7 -val fresh_fun_app = thm "fresh_fun_app";
     1.8 +val fresh_fun_app' = thm "fresh_fun_app'";
     1.9  val fresh_prod = thm "fresh_prod";
    1.10  
    1.11  (* A tactic to generate a name fresh for 
    1.12 @@ -131,7 +131,7 @@
    1.13      val abs_fresh = PureThy.get_thms thy (Name "abs_fresh");
    1.14      val ss' = ss addsimps fresh_prod::abs_fresh;
    1.15      val x = hd (tl (term_vars (prop_of exI)));
    1.16 -    val goal = List.nth(prems_of thm, i-1);
    1.17 +    val goal = nth (prems_of thm) (i-1);
    1.18      val atom_name_opt = get_inner_fresh_fun goal;
    1.19      val n = List.length (Logic.strip_params goal);
    1.20      (* Here we rely on the fact that the variable introduced by generate_fresh_tac is the last one in the list, the inner one *)
    1.21 @@ -143,20 +143,27 @@
    1.22      val atom_basename = Sign.base_name atom_name;
    1.23      val pt_name_inst = get_dyn_thm thy ("pt_"^atom_basename^"_inst") atom_basename;
    1.24      val at_name_inst = get_dyn_thm thy ("at_"^atom_basename^"_inst") atom_basename;
    1.25 -    fun tac_a i = 
    1.26 -      res_inst_tac_term' [(x,Bound n)] false exI i THEN
    1.27 -      asm_full_simp_tac ss' i                      THEN 
    1.28 -      NominalPermeq.fresh_guess_tac HOL_ss i;
    1.29 +    fun inst_fresh vars params i st =
    1.30 +   let val vars' = term_vars (prop_of st);
    1.31 +       val thy = theory_of_thm st;
    1.32 +   in case vars' \\ vars of 
    1.33 +     [x] => Seq.single (Thm.instantiate ([],[(cterm_of thy x,cterm_of thy (list_abs (params,Bound 0)))]) st)
    1.34 +    | _ => error "fresh_fun_simp: Too many variables, please report."
    1.35 +  end
    1.36    in
    1.37 -  (generate_fresh_tac atom_name i      THEN 
    1.38 -   subst_outer_tac ctx fresh_fun_app i THENL 
    1.39 +  ( (* generate_fresh_tac atom_name i      THEN *) 
    1.40 +  (fn st =>
    1.41 +  let 
    1.42 +    val vars = term_vars (prop_of st);
    1.43 +    val params = Logic.strip_params (nth (prems_of st) (i-1))
    1.44 +  in
    1.45 +   (subst_outer_tac ctx fresh_fun_app' i THENL 
    1.46     [rtac pt_name_inst,
    1.47 -    rtac at_name_inst, 
    1.48 -    (fn i => TRY (NominalPermeq.finite_guess_tac HOL_ss i)),   
    1.49 -    tac_a, 
    1.50 -    (fn i => TRY (NominalPermeq.fresh_guess_tac  HOL_ss i)),
    1.51 -    (fn i => auto_tac (HOL_cs, HOL_ss)) 
    1.52 -]) thm 
    1.53 +    rtac at_name_inst,
    1.54 +    (K all_tac),
    1.55 +    inst_fresh vars params]) st
    1.56 +  end)) thm
    1.57 +  
    1.58    end
    1.59    end
    1.60