# HG changeset patch
# User wenzelm
# Date 1635532756 -7200
# Node ID f1099c7330b7cf9e9f39d020c8043521fbd8f30e
# Parent  779ae499ca8b78071df0bb5a5ecdbe68d08103f4
more robust subgoal addressing;

diff -r 779ae499ca8b -r f1099c7330b7 src/HOL/Analysis/metric_arith.ML
--- a/src/HOL/Analysis/metric_arith.ML	Fri Oct 29 20:15:59 2021 +0200
+++ b/src/HOL/Analysis/metric_arith.ML	Fri Oct 29 20:39:16 2021 +0200
@@ -224,10 +224,11 @@
   in Argo_Tactic.argo_tac ctxt' dist_thms i end)
 
 fun basic_metric_arith_tac ctxt metric_ty =
-  HEADGOAL (dist_refl_sym_tac ctxt THEN'
-  IF_UNSOLVED o (embedding_tac ctxt metric_ty) THEN'
-  IF_UNSOLVED o (pre_arith_tac ctxt) THEN'
-  IF_UNSOLVED o (lin_real_arith_tac ctxt metric_ty))
+  SELECT_GOAL (
+    dist_refl_sym_tac ctxt 1 THEN
+    IF_UNSOLVED (embedding_tac ctxt metric_ty 1) THEN
+    IF_UNSOLVED (pre_arith_tac ctxt 1) THEN
+    IF_UNSOLVED (lin_real_arith_tac ctxt metric_ty 1))
 
 (* tries to infer the metric space from ct from dist terms,
    if no dist terms are present, equality terms will be used *)
@@ -258,9 +259,9 @@
     end
 
 (* solve \<exists> by proving the goal for a single witness from the metric space *)
-fun exists_tac ctxt st =
+fun exists_tac ctxt = CSUBGOAL (fn (goal, i) =>
   let
-    val goal = Thm.cprem_of st 1
+    val _ = \<^assert> (i = 1)
     val metric_ty = guess_metric ctxt (Thm.term_of goal)
     val points = find_points ctxt metric_ty goal
 
@@ -274,32 +275,33 @@
         (*variable doesn't occur in body*)
         resolve_tac ctxt @{thms exI}) THEN
         trace_tac ctxt ("Removed existential quantifier, try " ^ @{make_string} pt) THEN
-        try_points_tac ctxt
+        HEADGOAL (try_points_tac ctxt)
       end
-    and try_points_tac ctxt st = (
-      if is_exists (Thm.major_prem_of st) then
+    and try_points_tac ctxt = SUBGOAL (fn (g, _) =>
+      if is_exists g then
         FIRST (map (try_point_tac ctxt) points)
-      else if is_forall (Thm.major_prem_of st) then
-        HEADGOAL (resolve_tac ctxt @{thms HOL.allI} THEN'
+      else if is_forall g then
+        resolve_tac ctxt @{thms HOL.allI} 1 THEN
         Subgoal.FOCUS (fn {context = ctxt', ...} =>
           trace_tac ctxt "Removed universal quantifier" THEN
-          try_points_tac ctxt') ctxt)
-      else basic_metric_arith_tac ctxt metric_ty) st
-  in try_points_tac ctxt st end
+          try_points_tac ctxt' 1) ctxt 1
+      else basic_metric_arith_tac ctxt metric_ty 1)
+  in try_points_tac ctxt 1 end)
 
 fun metric_arith_tac ctxt =
-  (*unfold common definitions to get rid of sets*)
-  unfold_tac ctxt THEN'
-  (*remove all meta-level connectives*)
-  IF_UNSOLVED o (Object_Logic.full_atomize_tac ctxt) THEN'
-  (*convert goal to prenex form*)
-  IF_UNSOLVED o (prenex_tac ctxt) THEN'
-  (*and NNF to ?*)
-  IF_UNSOLVED o (nnf_tac ctxt) THEN'
-  (*turn all universally quantified variables into free variables, by focusing the subgoal*)
-  REPEAT o (resolve_tac ctxt @{thms HOL.allI}) THEN'
-  IF_UNSOLVED o SUBPROOF (fn {context = ctxt', ...} =>
-    trace_tac ctxt' "Focused on subgoal" THEN
-    exists_tac ctxt') ctxt
+  SELECT_GOAL (
+    (*unfold common definitions to get rid of sets*)
+    unfold_tac ctxt 1 THEN
+    (*remove all meta-level connectives*)
+    IF_UNSOLVED (Object_Logic.full_atomize_tac ctxt 1) THEN
+    (*convert goal to prenex form*)
+    IF_UNSOLVED (prenex_tac ctxt 1) THEN
+    (*and NNF to ?*)
+    IF_UNSOLVED (nnf_tac ctxt 1) THEN
+    (*turn all universally quantified variables into free variables, by focusing the subgoal*)
+    REPEAT (HEADGOAL (resolve_tac ctxt @{thms HOL.allI})) THEN
+    IF_UNSOLVED (SUBPROOF (fn {context = ctxt', ...} =>
+      trace_tac ctxt' "Focused on subgoal" THEN
+      exists_tac ctxt' 1) ctxt 1))
 
 end