src/HOL/Nominal/nominal_fresh_fun.ML
changeset 56230 3e449273942a
parent 55952 2f85cc6c27d4
child 56253 83b3c110f22d
     1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Mar 20 19:24:51 2014 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Mar 20 19:58:33 2014 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  a tactic to analyse instances of the fresh_fun.
     1.5  *)
     1.6  
     1.7 -(* FIXME proper ML structure *)
     1.8 +(* FIXME proper ML structure! *)
     1.9  
    1.10  (* FIXME res_inst_tac mostly obsolete, cf. Subgoal.FOCUS *)
    1.11  
    1.12 @@ -52,12 +52,11 @@
    1.13  (* A tactic to generate a name fresh for  all the free *)
    1.14  (* variables and parameters of the goal                *)
    1.15  
    1.16 -fun generate_fresh_tac atom_name i thm =
    1.17 +fun generate_fresh_tac ctxt atom_name = SUBGOAL (fn (goal, _) =>
    1.18   let
    1.19 -   val thy = theory_of_thm thm;
    1.20 +   val thy = Proof_Context.theory_of ctxt;
    1.21  (* the parsing function returns a qualified name, we get back the base name *)
    1.22     val atom_basename = Long_Name.base_name atom_name;
    1.23 -   val goal = nth (prems_of thm) (i - 1);
    1.24     val ps = Logic.strip_params goal;
    1.25     val Ts = rev (map snd ps);
    1.26     fun is_of_fs_name T = Sign.of_sort thy (T, [Sign.intern_class thy ("fs_"^atom_basename)]);
    1.27 @@ -76,11 +75,12 @@
    1.28  (* find the variable we want to instantiate *)
    1.29     val x = hd (Misc_Legacy.term_vars (prop_of exists_fresh'));
    1.30   in
    1.31 +   fn st =>
    1.32     (cut_inst_tac_term' [(x,s)] exists_fresh' 1 THEN
    1.33     rtac fs_name_thm 1 THEN
    1.34 -   etac exE 1) thm
    1.35 -  handle List.Empty  => all_tac thm (* if we collected no variables then we do nothing *)
    1.36 -  end;
    1.37 +   etac exE 1) st
    1.38 +  handle List.Empty  => all_tac st (* if we collected no variables then we do nothing *)
    1.39 + end) 1;
    1.40  
    1.41  fun get_inner_fresh_fun (Bound j) = NONE
    1.42    | get_inner_fresh_fun (v as Free _) = NONE
    1.43 @@ -97,15 +97,14 @@
    1.44  (* This tactic generates a fresh name of the atom type *)
    1.45  (* given by the innermost fresh_fun                    *)
    1.46  
    1.47 -fun generate_fresh_fun_tac i thm =
    1.48 +fun generate_fresh_fun_tac ctxt = SUBGOAL (fn (goal, _) =>
    1.49    let
    1.50 -    val goal = nth (prems_of thm) (i - 1);
    1.51      val atom_name_opt = get_inner_fresh_fun goal;
    1.52    in
    1.53    case atom_name_opt of
    1.54 -    NONE => all_tac thm
    1.55 -  | SOME atom_name  => generate_fresh_tac atom_name i thm
    1.56 -  end
    1.57 +    NONE => all_tac
    1.58 +  | SOME atom_name  => generate_fresh_tac ctxt atom_name
    1.59 +  end) 1;
    1.60  
    1.61  (* Two substitution tactics which looks for the innermost occurence in
    1.62     one assumption or in the conclusion *)
    1.63 @@ -123,24 +122,23 @@
    1.64    curry (curry (FIRST' (map uncurry (map uncurry (map subst_inner_asm_tac_aux
    1.65              (1 upto Thm.nprems_of th)))))) ctxt th;
    1.66  
    1.67 -fun fresh_fun_tac ctxt no_asm i thm =
    1.68 +fun fresh_fun_tac ctxt no_asm = SUBGOAL (fn (goal, i) =>
    1.69    (* Find the variable we instantiate *)
    1.70    let
    1.71 -    val thy = theory_of_thm thm;
    1.72 +    val thy = Proof_Context.theory_of ctxt;
    1.73      val abs_fresh = Global_Theory.get_thms thy "abs_fresh";
    1.74      val fresh_perm_app = Global_Theory.get_thms thy "fresh_perm_app";
    1.75      val simp_ctxt =
    1.76        ctxt addsimps (fresh_prod :: abs_fresh)
    1.77        addsimps fresh_perm_app;
    1.78      val x = hd (tl (Misc_Legacy.term_vars (prop_of exI)));
    1.79 -    val goal = nth (prems_of thm) (i-1);
    1.80      val atom_name_opt = get_inner_fresh_fun goal;
    1.81      val n = length (Logic.strip_params goal);
    1.82      (* Here we rely on the fact that the variable introduced by generate_fresh_tac *)
    1.83      (* is the last one in the list, the inner one *)
    1.84    in
    1.85    case atom_name_opt of
    1.86 -    NONE => all_tac thm
    1.87 +    NONE => all_tac
    1.88    | SOME atom_name =>
    1.89    let
    1.90      val atom_basename = Long_Name.base_name atom_name;
    1.91 @@ -173,21 +171,7 @@
    1.92      (subst_inner_asm_tac ctxt fresh_fun_app' i THEN (RANGE post_rewrite_tacs i)))
    1.93      ORELSE
    1.94      (subst_inner_tac ctxt fresh_fun_app' i THEN (RANGE post_rewrite_tacs i))) st
    1.95 -  end)) thm
    1.96 -
    1.97 +  end))
    1.98    end
    1.99 -  end
   1.100 +  end)
   1.101  
   1.102 -(* syntax for options, given "(no_asm)" will give back true, without
   1.103 -   gives back false *)
   1.104 -val options_syntax =
   1.105 -    (Args.parens (Args.$$$ "no_asm") >> (K true)) ||
   1.106 -     (Scan.succeed false);
   1.107 -
   1.108 -fun setup_generate_fresh x =
   1.109 -  (Args.goal_spec -- Args.type_name {proper = true, strict = true} >>
   1.110 -    (fn (quant, s) => K (SIMPLE_METHOD'' quant (generate_fresh_tac s)))) x;
   1.111 -
   1.112 -fun setup_fresh_fun_simp x =
   1.113 -  (Scan.lift options_syntax >> (fn b => fn ctxt => SIMPLE_METHOD' (fresh_fun_tac ctxt b))) x;
   1.114 -