# HG changeset patch # User wenzelm # Date 1395341913 -3600 # Node ID 3e449273942ab6b15f3a604c2e7cafb53a5e447b # Parent f61eaab6bec345b4f3ff387da9cee33f86e265e9 more standard method_setup; enforce subgoal boundaries via SUBGOAL -- clean tactical failure if out-of-range; diff -r f61eaab6bec3 -r 3e449273942a src/HOL/Nominal/Nominal.thy --- a/src/HOL/Nominal/Nominal.thy Thu Mar 20 19:24:51 2014 +0100 +++ b/src/HOL/Nominal/Nominal.thy Thu Mar 20 19:58:33 2014 +0100 @@ -3638,13 +3638,15 @@ (* tactics for generating fresh names and simplifying fresh_funs *) ML_file "nominal_fresh_fun.ML" -method_setup generate_fresh = - {* setup_generate_fresh *} - {* tactic to generate a name fresh for all the variables in the goal *} - -method_setup fresh_fun_simp = - {* setup_fresh_fun_simp *} - {* tactic to delete one inner occurence of fresh_fun *} +method_setup generate_fresh = {* + Args.type_name {proper = true, strict = true} >> + (fn s => fn ctxt => SIMPLE_METHOD (generate_fresh_tac ctxt s)) +*} "generate a name fresh for all the variables in the goal" + +method_setup fresh_fun_simp = {* + Scan.lift (Args.parens (Args.$$$ "no_asm") >> K true || Scan.succeed false) >> + (fn b => fn ctxt => SIMPLE_METHOD' (fresh_fun_tac ctxt b)) +*} "delete one inner occurence of fresh_fun" (************************************************) diff -r f61eaab6bec3 -r 3e449273942a src/HOL/Nominal/nominal_fresh_fun.ML --- a/src/HOL/Nominal/nominal_fresh_fun.ML Thu Mar 20 19:24:51 2014 +0100 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML Thu Mar 20 19:58:33 2014 +0100 @@ -5,7 +5,7 @@ a tactic to analyse instances of the fresh_fun. *) -(* FIXME proper ML structure *) +(* FIXME proper ML structure! *) (* FIXME res_inst_tac mostly obsolete, cf. Subgoal.FOCUS *) @@ -52,12 +52,11 @@ (* A tactic to generate a name fresh for all the free *) (* variables and parameters of the goal *) -fun generate_fresh_tac atom_name i thm = +fun generate_fresh_tac ctxt atom_name = SUBGOAL (fn (goal, _) => let - val thy = theory_of_thm thm; + val thy = Proof_Context.theory_of ctxt; (* the parsing function returns a qualified name, we get back the base name *) val atom_basename = Long_Name.base_name atom_name; - val goal = nth (prems_of thm) (i - 1); val ps = Logic.strip_params goal; val Ts = rev (map snd ps); fun is_of_fs_name T = Sign.of_sort thy (T, [Sign.intern_class thy ("fs_"^atom_basename)]); @@ -76,11 +75,12 @@ (* find the variable we want to instantiate *) val x = hd (Misc_Legacy.term_vars (prop_of exists_fresh')); in + fn st => (cut_inst_tac_term' [(x,s)] exists_fresh' 1 THEN rtac fs_name_thm 1 THEN - etac exE 1) thm - handle List.Empty => all_tac thm (* if we collected no variables then we do nothing *) - end; + etac exE 1) st + handle List.Empty => all_tac st (* if we collected no variables then we do nothing *) + end) 1; fun get_inner_fresh_fun (Bound j) = NONE | get_inner_fresh_fun (v as Free _) = NONE @@ -97,15 +97,14 @@ (* This tactic generates a fresh name of the atom type *) (* given by the innermost fresh_fun *) -fun generate_fresh_fun_tac i thm = +fun generate_fresh_fun_tac ctxt = SUBGOAL (fn (goal, _) => let - val goal = nth (prems_of thm) (i - 1); val atom_name_opt = get_inner_fresh_fun goal; in case atom_name_opt of - NONE => all_tac thm - | SOME atom_name => generate_fresh_tac atom_name i thm - end + NONE => all_tac + | SOME atom_name => generate_fresh_tac ctxt atom_name + end) 1; (* Two substitution tactics which looks for the innermost occurence in one assumption or in the conclusion *) @@ -123,24 +122,23 @@ curry (curry (FIRST' (map uncurry (map uncurry (map subst_inner_asm_tac_aux (1 upto Thm.nprems_of th)))))) ctxt th; -fun fresh_fun_tac ctxt no_asm i thm = +fun fresh_fun_tac ctxt no_asm = SUBGOAL (fn (goal, i) => (* Find the variable we instantiate *) let - val thy = theory_of_thm thm; + val thy = Proof_Context.theory_of ctxt; val abs_fresh = Global_Theory.get_thms thy "abs_fresh"; val fresh_perm_app = Global_Theory.get_thms thy "fresh_perm_app"; val simp_ctxt = ctxt addsimps (fresh_prod :: abs_fresh) addsimps fresh_perm_app; val x = hd (tl (Misc_Legacy.term_vars (prop_of exI))); - val goal = nth (prems_of thm) (i-1); val atom_name_opt = get_inner_fresh_fun goal; val n = length (Logic.strip_params goal); (* Here we rely on the fact that the variable introduced by generate_fresh_tac *) (* is the last one in the list, the inner one *) in case atom_name_opt of - NONE => all_tac thm + NONE => all_tac | SOME atom_name => let val atom_basename = Long_Name.base_name atom_name; @@ -173,21 +171,7 @@ (subst_inner_asm_tac ctxt fresh_fun_app' i THEN (RANGE post_rewrite_tacs i))) ORELSE (subst_inner_tac ctxt fresh_fun_app' i THEN (RANGE post_rewrite_tacs i))) st - end)) thm - + end)) end - end + end) -(* syntax for options, given "(no_asm)" will give back true, without - gives back false *) -val options_syntax = - (Args.parens (Args.$$$ "no_asm") >> (K true)) || - (Scan.succeed false); - -fun setup_generate_fresh x = - (Args.goal_spec -- Args.type_name {proper = true, strict = true} >> - (fn (quant, s) => K (SIMPLE_METHOD'' quant (generate_fresh_tac s)))) x; - -fun setup_fresh_fun_simp x = - (Scan.lift options_syntax >> (fn b => fn ctxt => SIMPLE_METHOD' (fresh_fun_tac ctxt b))) x; - diff -r f61eaab6bec3 -r 3e449273942a src/HOL/Nominal/nominal_permeq.ML --- a/src/HOL/Nominal/nominal_permeq.ML Thu Mar 20 19:24:51 2014 +0100 +++ b/src/HOL/Nominal/nominal_permeq.ML Thu Mar 20 19:58:33 2014 +0100 @@ -142,7 +142,7 @@ (* stac contains the simplifiation tactic that is *) (* applied (see (no_asm) options below *) fun perm_simp_gen stac dyn_thms eqvt_thms ctxt i = - ("general simplification of permutations", fn st => + ("general simplification of permutations", fn st => SUBGOAL (fn _ => let val ctxt' = ctxt addsimps (maps (dynamic_thms st) dyn_thms @ eqvt_thms) @@ -150,8 +150,8 @@ |> fold Simplifier.del_cong weak_congs |> fold Simplifier.add_cong strong_congs in - stac ctxt' i st - end); + stac ctxt' i + end) i st); (* general simplification of permutations and permutation that arose from eqvt-problems *) fun perm_simp stac ctxt =