# HG changeset patch
# User wenzelm
# Date 1263337736 -3600
# Node ID 6587c24ef6d889d0935775a2861ad2225b22bf03
# Parent  62fcc25162dd804e3abfb3173066f92a70fc0a70
added SOLVED' -- a more direct version of THEN_ALL_NEW (K no_tac) -- strictly speaking it does not even depend on subgoal addressing, but it would be too confusing without it;

diff -r 62fcc25162dd -r 6587c24ef6d8 src/HOL/Nominal/nominal_fresh_fun.ML
--- a/src/HOL/Nominal/nominal_fresh_fun.ML	Tue Jan 12 22:53:18 2010 +0100
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Jan 13 00:08:56 2010 +0100
@@ -7,10 +7,6 @@
 
 (* First some functions that should be in the library *)
 
-(* A tactic which only succeeds when the argument *)
-(* tactic solves completely the specified subgoal *)
-fun SOLVEI t = t THEN_ALL_NEW (fn i => no_tac);
-
 fun gen_res_inst_tac_term instf tyinst tinst elim th i st =
   let
     val thy = theory_of_thm st;
@@ -165,10 +161,10 @@
     val post_rewrite_tacs =
           [rtac pt_name_inst,
            rtac at_name_inst,
-           TRY o SOLVEI (NominalPermeq.finite_guess_tac ss''),
+           TRY o SOLVED' (NominalPermeq.finite_guess_tac ss''),
            inst_fresh vars params THEN'
-           (TRY o SOLVEI (NominalPermeq.fresh_guess_tac ss'')) THEN'
-           (TRY o SOLVEI (asm_full_simp_tac ss''))]
+           (TRY o SOLVED' (NominalPermeq.fresh_guess_tac ss'')) THEN'
+           (TRY o SOLVED' (asm_full_simp_tac ss''))]
   in
    ((if no_asm then no_tac else
     (subst_inner_asm_tac ctxt fresh_fun_app' i THEN (RANGE post_rewrite_tacs i)))
diff -r 62fcc25162dd -r 6587c24ef6d8 src/HOL/Nominal/nominal_permeq.ML
--- a/src/HOL/Nominal/nominal_permeq.ML	Tue Jan 12 22:53:18 2010 +0100
+++ b/src/HOL/Nominal/nominal_permeq.ML	Wed Jan 13 00:08:56 2010 +0100
@@ -80,10 +80,6 @@
 (* needed to avoid warnings about overwritten congs *)
 val weak_congs   = [@{thm "if_weak_cong"}]
 
-(* FIXME comment *)
-(* a tactical which fails if the tactic taken as an argument generates does not solve the sub goal i *)
-fun SOLVEI t = t THEN_ALL_NEW (fn i => no_tac);
-
 (* debugging *)
 fun DEBUG_tac (msg,tac) = 
     CHANGED (EVERY [print_tac ("before "^msg), tac, print_tac ("after "^msg)]); 
@@ -410,7 +406,7 @@
 fun basic_simp_meth_setup debug tac =
   Scan.depend (fn ctxt => Scan.succeed (Simplifier.map_ss (fn _ => HOL_basic_ss) ctxt, ())) --
   Method.sections (Simplifier.simp_modifiers' @ Splitter.split_modifiers) >>
-  (K (SIMPLE_METHOD' o (fn ss => if debug then tac ss else SOLVEI (tac ss)) o simpset_of));
+  (K (SIMPLE_METHOD' o (if debug then tac else SOLVED' o tac) o simpset_of));
 
 val perm_simp_meth_debug        = local_simp_meth_setup dperm_simp_tac;
 val perm_extend_simp_meth       = local_simp_meth_setup perm_extend_simp_tac;
diff -r 62fcc25162dd -r 6587c24ef6d8 src/Pure/tactical.ML
--- a/src/Pure/tactical.ML	Tue Jan 12 22:53:18 2010 +0100
+++ b/src/Pure/tactical.ML	Wed Jan 13 00:08:56 2010 +0100
@@ -58,6 +58,7 @@
   val CSUBGOAL: ((cterm * int) -> tactic) -> int -> tactic
   val SUBGOAL: ((term * int) -> tactic) -> int -> tactic
   val CHANGED_GOAL: (int -> tactic) -> int -> tactic
+  val SOLVED': (int -> tactic) -> int -> tactic
   val THEN_ALL_NEW: (int -> tactic) * (int -> tactic) -> int -> tactic
   val REPEAT_ALL_NEW: (int -> tactic) -> int -> tactic
   val PRIMSEQ: (thm -> thm Seq.seq) -> tactic
@@ -356,10 +357,18 @@
     in  Seq.filter diff (tac i st)  end
     handle Subscript => Seq.empty  (*no subgoal i*);
 
+(*Returns all states where some subgoals have been solved.  For
+  subgoal-based tactics this means subgoal i has been solved
+  altogether -- no new subgoals have emerged.*)
+fun SOLVED' tac i st =
+  tac i st |> Seq.filter (fn st' => nprems_of st' < nprems_of st);
+
+(*Apply second tactic to all subgoals emerging from the first --
+  following usual convention for subgoal-based tactics.*)
 fun (tac1 THEN_ALL_NEW tac2) i st =
   st |> (tac1 i THEN (fn st' => Seq.INTERVAL tac2 i (i + nprems_of st' - nprems_of st) st'));
 
-(*repeatedly dig into any emerging subgoals*)
+(*Repeatedly dig into any emerging subgoals.*)
 fun REPEAT_ALL_NEW tac =
   tac THEN_ALL_NEW (TRY o (fn i => REPEAT_ALL_NEW tac i));