more standard method_setup;
authorwenzelm
Thu Mar 20 19:58:33 2014 +0100 (2014-03-20)
changeset 562303e449273942a
parent 56229 f61eaab6bec3
child 56231 b98813774a63
more standard method_setup;
enforce subgoal boundaries via SUBGOAL -- clean tactical failure if out-of-range;
src/HOL/Nominal/Nominal.thy
src/HOL/Nominal/nominal_fresh_fun.ML
src/HOL/Nominal/nominal_permeq.ML
     1.1 --- a/src/HOL/Nominal/Nominal.thy	Thu Mar 20 19:24:51 2014 +0100
     1.2 +++ b/src/HOL/Nominal/Nominal.thy	Thu Mar 20 19:58:33 2014 +0100
     1.3 @@ -3638,13 +3638,15 @@
     1.4  (* tactics for generating fresh names and simplifying fresh_funs *)
     1.5  ML_file "nominal_fresh_fun.ML"
     1.6  
     1.7 -method_setup generate_fresh = 
     1.8 -  {* setup_generate_fresh *} 
     1.9 -  {* tactic to generate a name fresh for all the variables in the goal *}
    1.10 -
    1.11 -method_setup fresh_fun_simp = 
    1.12 -  {* setup_fresh_fun_simp *} 
    1.13 -  {* tactic to delete one inner occurence of fresh_fun *}
    1.14 +method_setup generate_fresh = {*
    1.15 +  Args.type_name {proper = true, strict = true} >>
    1.16 +    (fn s => fn ctxt => SIMPLE_METHOD (generate_fresh_tac ctxt s))
    1.17 +*} "generate a name fresh for all the variables in the goal"
    1.18 +
    1.19 +method_setup fresh_fun_simp = {*
    1.20 +  Scan.lift (Args.parens (Args.$$$ "no_asm") >> K true || Scan.succeed false) >>
    1.21 +    (fn b => fn ctxt => SIMPLE_METHOD' (fresh_fun_tac ctxt b))
    1.22 +*} "delete one inner occurence of fresh_fun"
    1.23  
    1.24  
    1.25  (************************************************)
     2.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Mar 20 19:24:51 2014 +0100
     2.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Mar 20 19:58:33 2014 +0100
     2.3 @@ -5,7 +5,7 @@
     2.4  a tactic to analyse instances of the fresh_fun.
     2.5  *)
     2.6  
     2.7 -(* FIXME proper ML structure *)
     2.8 +(* FIXME proper ML structure! *)
     2.9  
    2.10  (* FIXME res_inst_tac mostly obsolete, cf. Subgoal.FOCUS *)
    2.11  
    2.12 @@ -52,12 +52,11 @@
    2.13  (* A tactic to generate a name fresh for  all the free *)
    2.14  (* variables and parameters of the goal                *)
    2.15  
    2.16 -fun generate_fresh_tac atom_name i thm =
    2.17 +fun generate_fresh_tac ctxt atom_name = SUBGOAL (fn (goal, _) =>
    2.18   let
    2.19 -   val thy = theory_of_thm thm;
    2.20 +   val thy = Proof_Context.theory_of ctxt;
    2.21  (* the parsing function returns a qualified name, we get back the base name *)
    2.22     val atom_basename = Long_Name.base_name atom_name;
    2.23 -   val goal = nth (prems_of thm) (i - 1);
    2.24     val ps = Logic.strip_params goal;
    2.25     val Ts = rev (map snd ps);
    2.26     fun is_of_fs_name T = Sign.of_sort thy (T, [Sign.intern_class thy ("fs_"^atom_basename)]);
    2.27 @@ -76,11 +75,12 @@
    2.28  (* find the variable we want to instantiate *)
    2.29     val x = hd (Misc_Legacy.term_vars (prop_of exists_fresh'));
    2.30   in
    2.31 +   fn st =>
    2.32     (cut_inst_tac_term' [(x,s)] exists_fresh' 1 THEN
    2.33     rtac fs_name_thm 1 THEN
    2.34 -   etac exE 1) thm
    2.35 -  handle List.Empty  => all_tac thm (* if we collected no variables then we do nothing *)
    2.36 -  end;
    2.37 +   etac exE 1) st
    2.38 +  handle List.Empty  => all_tac st (* if we collected no variables then we do nothing *)
    2.39 + end) 1;
    2.40  
    2.41  fun get_inner_fresh_fun (Bound j) = NONE
    2.42    | get_inner_fresh_fun (v as Free _) = NONE
    2.43 @@ -97,15 +97,14 @@
    2.44  (* This tactic generates a fresh name of the atom type *)
    2.45  (* given by the innermost fresh_fun                    *)
    2.46  
    2.47 -fun generate_fresh_fun_tac i thm =
    2.48 +fun generate_fresh_fun_tac ctxt = SUBGOAL (fn (goal, _) =>
    2.49    let
    2.50 -    val goal = nth (prems_of thm) (i - 1);
    2.51      val atom_name_opt = get_inner_fresh_fun goal;
    2.52    in
    2.53    case atom_name_opt of
    2.54 -    NONE => all_tac thm
    2.55 -  | SOME atom_name  => generate_fresh_tac atom_name i thm
    2.56 -  end
    2.57 +    NONE => all_tac
    2.58 +  | SOME atom_name  => generate_fresh_tac ctxt atom_name
    2.59 +  end) 1;
    2.60  
    2.61  (* Two substitution tactics which looks for the innermost occurence in
    2.62     one assumption or in the conclusion *)
    2.63 @@ -123,24 +122,23 @@
    2.64    curry (curry (FIRST' (map uncurry (map uncurry (map subst_inner_asm_tac_aux
    2.65              (1 upto Thm.nprems_of th)))))) ctxt th;
    2.66  
    2.67 -fun fresh_fun_tac ctxt no_asm i thm =
    2.68 +fun fresh_fun_tac ctxt no_asm = SUBGOAL (fn (goal, i) =>
    2.69    (* Find the variable we instantiate *)
    2.70    let
    2.71 -    val thy = theory_of_thm thm;
    2.72 +    val thy = Proof_Context.theory_of ctxt;
    2.73      val abs_fresh = Global_Theory.get_thms thy "abs_fresh";
    2.74      val fresh_perm_app = Global_Theory.get_thms thy "fresh_perm_app";
    2.75      val simp_ctxt =
    2.76        ctxt addsimps (fresh_prod :: abs_fresh)
    2.77        addsimps fresh_perm_app;
    2.78      val x = hd (tl (Misc_Legacy.term_vars (prop_of exI)));
    2.79 -    val goal = nth (prems_of thm) (i-1);
    2.80      val atom_name_opt = get_inner_fresh_fun goal;
    2.81      val n = length (Logic.strip_params goal);
    2.82      (* Here we rely on the fact that the variable introduced by generate_fresh_tac *)
    2.83      (* is the last one in the list, the inner one *)
    2.84    in
    2.85    case atom_name_opt of
    2.86 -    NONE => all_tac thm
    2.87 +    NONE => all_tac
    2.88    | SOME atom_name =>
    2.89    let
    2.90      val atom_basename = Long_Name.base_name atom_name;
    2.91 @@ -173,21 +171,7 @@
    2.92      (subst_inner_asm_tac ctxt fresh_fun_app' i THEN (RANGE post_rewrite_tacs i)))
    2.93      ORELSE
    2.94      (subst_inner_tac ctxt fresh_fun_app' i THEN (RANGE post_rewrite_tacs i))) st
    2.95 -  end)) thm
    2.96 -
    2.97 +  end))
    2.98    end
    2.99 -  end
   2.100 +  end)
   2.101  
   2.102 -(* syntax for options, given "(no_asm)" will give back true, without
   2.103 -   gives back false *)
   2.104 -val options_syntax =
   2.105 -    (Args.parens (Args.$$$ "no_asm") >> (K true)) ||
   2.106 -     (Scan.succeed false);
   2.107 -
   2.108 -fun setup_generate_fresh x =
   2.109 -  (Args.goal_spec -- Args.type_name {proper = true, strict = true} >>
   2.110 -    (fn (quant, s) => K (SIMPLE_METHOD'' quant (generate_fresh_tac s)))) x;
   2.111 -
   2.112 -fun setup_fresh_fun_simp x =
   2.113 -  (Scan.lift options_syntax >> (fn b => fn ctxt => SIMPLE_METHOD' (fresh_fun_tac ctxt b))) x;
   2.114 -
     3.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Thu Mar 20 19:24:51 2014 +0100
     3.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Thu Mar 20 19:58:33 2014 +0100
     3.3 @@ -142,7 +142,7 @@
     3.4  (* stac contains the simplifiation tactic that is *)
     3.5  (* applied (see (no_asm) options below            *)
     3.6  fun perm_simp_gen stac dyn_thms eqvt_thms ctxt i = 
     3.7 -    ("general simplification of permutations", fn st =>
     3.8 +    ("general simplification of permutations", fn st => SUBGOAL (fn _ =>
     3.9      let
    3.10         val ctxt' = ctxt
    3.11           addsimps (maps (dynamic_thms st) dyn_thms @ eqvt_thms)
    3.12 @@ -150,8 +150,8 @@
    3.13           |> fold Simplifier.del_cong weak_congs
    3.14           |> fold Simplifier.add_cong strong_congs
    3.15      in
    3.16 -      stac ctxt' i st
    3.17 -    end);
    3.18 +      stac ctxt' i
    3.19 +    end) i st);
    3.20  
    3.21  (* general simplification of permutations and permutation that arose from eqvt-problems *)
    3.22  fun perm_simp stac ctxt =