enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
authorwenzelm
Thu Mar 20 21:07:57 2014 +0100 (2014-03-20)
changeset 56231b98813774a63
parent 56230 3e449273942a
child 56232 31e283f606e2
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
src/HOL/Tools/Function/lexicographic_order.ML
src/HOL/Tools/Function/termination.ML
src/HOL/Tools/coinduction.ML
src/HOL/Topological_Spaces.thy
src/Pure/Isar/rule_cases.ML
src/Pure/tactical.ML
src/Tools/induct.ML
src/ZF/Tools/induct_tacs.ML
     1.1 --- a/src/HOL/Tools/Function/lexicographic_order.ML	Thu Mar 20 19:58:33 2014 +0100
     1.2 +++ b/src/HOL/Tools/Function/lexicographic_order.ML	Thu Mar 20 21:07:57 2014 +0100
     1.3 @@ -174,7 +174,7 @@
     1.4  
     1.5  (** The Main Function **)
     1.6  
     1.7 -fun lex_order_tac quiet ctxt solve_tac (st: thm) =
     1.8 +fun lex_order_tac quiet ctxt solve_tac st = SUBGOAL (fn _ =>
     1.9    let
    1.10      val thy = Proof_Context.theory_of ctxt
    1.11      val ((_ $ (_ $ rel)) :: tl) = prems_of st
    1.12 @@ -187,26 +187,27 @@
    1.13      val table = (* 2: create table *)
    1.14        map (fn t => map (mk_cell thy solve_tac (dest_term t)) measure_funs) tl
    1.15    in
    1.16 -    case search_table table of
    1.17 -      NONE => if quiet then no_tac st else error (no_order_msg ctxt table tl measure_funs)
    1.18 -    | SOME order =>
    1.19 -      let
    1.20 -        val clean_table = map (fn x => map (nth x) order) table
    1.21 -        val relation = mk_measures domT (map (nth measure_funs) order)
    1.22 -        val _ =
    1.23 -          if not quiet then
    1.24 -            Pretty.writeln (Pretty.block
    1.25 -              [Pretty.str "Found termination order:", Pretty.brk 1,
    1.26 -                Pretty.quote (Syntax.pretty_term ctxt relation)])
    1.27 -          else ()
    1.28 -
    1.29 -      in (* 4: proof reconstruction *)
    1.30 -        st |> (PRIMITIVE (cterm_instantiate [(cterm_of thy rel, cterm_of thy relation)])
    1.31 -        THEN (REPEAT (rtac @{thm "wf_mlex"} 1))
    1.32 -        THEN (rtac @{thm "wf_empty"} 1)
    1.33 -        THEN EVERY (map prove_row clean_table))
    1.34 -      end
    1.35 -  end
    1.36 +    fn st =>
    1.37 +      case search_table table of
    1.38 +        NONE => if quiet then no_tac st else error (no_order_msg ctxt table tl measure_funs)
    1.39 +      | SOME order =>
    1.40 +        let
    1.41 +          val clean_table = map (fn x => map (nth x) order) table
    1.42 +          val relation = mk_measures domT (map (nth measure_funs) order)
    1.43 +          val _ =
    1.44 +            if not quiet then
    1.45 +              Pretty.writeln (Pretty.block
    1.46 +                [Pretty.str "Found termination order:", Pretty.brk 1,
    1.47 +                  Pretty.quote (Syntax.pretty_term ctxt relation)])
    1.48 +            else ()
    1.49 +  
    1.50 +        in (* 4: proof reconstruction *)
    1.51 +          st |> (PRIMITIVE (cterm_instantiate [(cterm_of thy rel, cterm_of thy relation)])
    1.52 +          THEN (REPEAT (rtac @{thm "wf_mlex"} 1))
    1.53 +          THEN (rtac @{thm "wf_empty"} 1)
    1.54 +          THEN EVERY (map prove_row clean_table))
    1.55 +        end
    1.56 +  end) 1 st;
    1.57  
    1.58  fun lexicographic_order_tac quiet ctxt =
    1.59    TRY (Function_Common.apply_termination_rule ctxt 1) THEN
     2.1 --- a/src/HOL/Tools/Function/termination.ML	Thu Mar 20 19:58:33 2014 +0100
     2.2 +++ b/src/HOL/Tools/Function/termination.ML	Thu Mar 20 21:07:57 2014 +0100
     2.3 @@ -272,10 +272,10 @@
     2.4  
     2.5  in
     2.6  
     2.7 -fun wf_union_tac ctxt st =
     2.8 +fun wf_union_tac ctxt st = SUBGOAL (fn _ =>
     2.9    let
    2.10      val thy = Proof_Context.theory_of ctxt
    2.11 -    val cert = cterm_of (theory_of_thm st)
    2.12 +    val cert = cterm_of thy
    2.13      val ((_ $ (_ $ rel)) :: ineqs) = prems_of st
    2.14  
    2.15      fun mk_compr ineq =
    2.16 @@ -304,8 +304,8 @@
    2.17    in
    2.18      (PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)])
    2.19       THEN ALLGOALS (fn i => if i = 1 then all_tac else solve_membership_tac i)
    2.20 -     THEN rewrite_goal_tac ctxt Un_aci_simps 1) st  (* eliminate duplicates *)
    2.21 -  end
    2.22 +     THEN rewrite_goal_tac ctxt Un_aci_simps 1)  (* eliminate duplicates *)
    2.23 +  end) 1 st
    2.24  
    2.25  end
    2.26  
     3.1 --- a/src/HOL/Tools/coinduction.ML	Thu Mar 20 19:58:33 2014 +0100
     3.2 +++ b/src/HOL/Tools/coinduction.ML	Thu Mar 20 21:07:57 2014 +0100
     3.3 @@ -40,19 +40,20 @@
     3.4      (THEN_ALL_NEW_SKIP skip tac (REPEAT_DETERM_N n o etac thin_rl)) i st
     3.5    end;
     3.6  
     3.7 -fun coinduction_tac ctxt raw_vars opt_raw_thm prems st =
     3.8 +fun coinduction_tac ctxt raw_vars opt_raw_thm prems = HEADGOAL (SUBGOAL_CASES (fn (goal, _, _) =>
     3.9    let
    3.10      val lhs_of_eq = HOLogic.dest_Trueprop #> HOLogic.dest_eq #> fst;
    3.11      fun find_coinduct t = 
    3.12        Induct.find_coinductP ctxt t @
    3.13        (try (Induct.find_coinductT ctxt o fastype_of o lhs_of_eq) t |> the_default [])
    3.14 -    val raw_thm = case opt_raw_thm
    3.15 -      of SOME raw_thm => raw_thm
    3.16 -       | NONE => st |> prems_of |> hd |> Logic.strip_assums_concl |> find_coinduct |> hd;
    3.17 +    val raw_thm =
    3.18 +      (case opt_raw_thm of
    3.19 +        SOME raw_thm => raw_thm
    3.20 +      | NONE => goal |> Logic.strip_assums_concl |> find_coinduct |> hd);
    3.21      val skip = Integer.max 1 (Rule_Cases.get_consumes raw_thm) - 1
    3.22      val cases = Rule_Cases.get raw_thm |> fst
    3.23    in
    3.24 -    NO_CASES (HEADGOAL (
    3.25 +    HEADGOAL (
    3.26        Object_Logic.rulify_tac ctxt THEN'
    3.27        Method.insert_tac prems THEN'
    3.28        Object_Logic.atomize_prems_tac ctxt THEN'
    3.29 @@ -110,10 +111,10 @@
    3.30                          unfold_thms_tac ctxt eqs
    3.31                        end)) ctxt)))])
    3.32          end) ctxt) THEN'
    3.33 -      K (prune_params_tac ctxt))) st
    3.34 -    |> Seq.maps (fn (_, st) =>
    3.35 +      K (prune_params_tac ctxt))
    3.36 +    #> Seq.maps (fn st =>
    3.37        CASES (Rule_Cases.make_common (Proof_Context.theory_of ctxt, prop_of st) cases) all_tac st)
    3.38 -  end;
    3.39 +  end));
    3.40  
    3.41  local
    3.42  
     4.1 --- a/src/HOL/Topological_Spaces.thy	Thu Mar 20 19:58:33 2014 +0100
     4.2 +++ b/src/HOL/Topological_Spaces.thy	Thu Mar 20 21:07:57 2014 +0100
     4.3 @@ -373,7 +373,7 @@
     4.4  qed
     4.5  
     4.6  ML {*
     4.7 -  fun eventually_elim_tac ctxt thms thm =
     4.8 +  fun eventually_elim_tac ctxt thms = SUBGOAL_CASES (fn (_, _, st) =>
     4.9      let
    4.10        val thy = Proof_Context.theory_of ctxt
    4.11        val mp_thms = thms RL [@{thm eventually_rev_mp}]
    4.12 @@ -381,11 +381,11 @@
    4.13          (@{thm allI} RS @{thm always_eventually})
    4.14          |> fold (fn thm1 => fn thm2 => thm2 RS thm1) mp_thms
    4.15          |> fold (fn _ => fn thm => @{thm impI} RS thm) thms
    4.16 -      val cases_prop = prop_of (raw_elim_thm RS thm)
    4.17 +      val cases_prop = prop_of (raw_elim_thm RS st)
    4.18        val cases = (Rule_Cases.make_common (thy, cases_prop) [(("elim", []), [])])
    4.19      in
    4.20 -      CASES cases (rtac raw_elim_thm 1) thm
    4.21 -    end
    4.22 +      CASES cases (rtac raw_elim_thm 1)
    4.23 +    end) 1
    4.24  *}
    4.25  
    4.26  method_setup eventually_elim = {*
     5.1 --- a/src/Pure/Isar/rule_cases.ML	Thu Mar 20 19:58:33 2014 +0100
     5.2 +++ b/src/Pure/Isar/rule_cases.ML	Thu Mar 20 21:07:57 2014 +0100
     5.3 @@ -12,7 +12,7 @@
     5.4    type cases_tactic
     5.5    val CASES: cases -> tactic -> cases_tactic
     5.6    val NO_CASES: tactic -> cases_tactic
     5.7 -  val SUBGOAL_CASES: ((term * int) -> cases_tactic) -> int -> cases_tactic
     5.8 +  val SUBGOAL_CASES: ((term * int * thm) -> cases_tactic) -> int -> cases_tactic
     5.9    val THEN_ALL_NEW_CASES: (int -> cases_tactic) * (int -> tactic) -> int -> cases_tactic
    5.10  end
    5.11  
    5.12 @@ -190,7 +190,7 @@
    5.13  
    5.14  fun SUBGOAL_CASES tac i st =
    5.15    (case try Logic.nth_prem (i, Thm.prop_of st) of
    5.16 -    SOME goal => tac (goal, i) st
    5.17 +    SOME goal => tac (goal, i, st) st
    5.18    | NONE => Seq.empty);
    5.19  
    5.20  fun (tac1 THEN_ALL_NEW_CASES tac2) i st =
     6.1 --- a/src/Pure/tactical.ML	Thu Mar 20 19:58:33 2014 +0100
     6.2 +++ b/src/Pure/tactical.ML	Thu Mar 20 21:07:57 2014 +0100
     6.3 @@ -334,15 +334,14 @@
     6.4  (*Returns all states that have changed in subgoal i, counted from the LAST
     6.5    subgoal.  For stac, for example.*)
     6.6  fun CHANGED_GOAL tac i st =
     6.7 -    let val np = Thm.nprems_of st
     6.8 -        val d = np-i                 (*distance from END*)
     6.9 -        val t = Thm.term_of (Thm.cprem_of st i)
    6.10 -        fun diff st' =
    6.11 -            Thm.nprems_of st' - d <= 0   (*the subgoal no longer exists*)
    6.12 -            orelse
    6.13 -             not (Envir.aeconv (t, Thm.term_of (Thm.cprem_of st' (Thm.nprems_of st' - d))))
    6.14 -    in  Seq.filter diff (tac i st)  end
    6.15 -    handle General.Subscript => Seq.empty  (*no subgoal i*);
    6.16 +  SUBGOAL (fn (t, _) =>
    6.17 +    let
    6.18 +      val np = Thm.nprems_of st;
    6.19 +      val d = np - i;  (*distance from END*)
    6.20 +      fun diff st' =
    6.21 +        Thm.nprems_of st' - d <= 0 orelse  (*the subgoal no longer exists*)
    6.22 +        not (Envir.aeconv (t, Thm.term_of (Thm.cprem_of st' (Thm.nprems_of st' - d))));
    6.23 +    in Seq.filter diff o tac i end) i st;
    6.24  
    6.25  (*Returns all states where some subgoals have been solved.  For
    6.26    subgoal-based tactics this means subgoal i has been solved
     7.1 --- a/src/Tools/induct.ML	Thu Mar 20 19:58:33 2014 +0100
     7.2 +++ b/src/Tools/induct.ML	Thu Mar 20 21:07:57 2014 +0100
     7.3 @@ -741,71 +741,71 @@
     7.4  type case_data = (((string * string list) * string list) list * int);
     7.5  
     7.6  fun gen_induct_tac mod_cases ctxt simp def_insts arbitrary taking opt_rule facts =
     7.7 -  let
     7.8 -    val thy = Proof_Context.theory_of ctxt;
     7.9 -
    7.10 -    val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
    7.11 -    val atomized_defs = map (map (Conv.fconv_rule (atomize_cterm defs_ctxt))) defs;
    7.12 -
    7.13 -    fun inst_rule (concls, r) =
    7.14 -      (if null insts then `Rule_Cases.get r
    7.15 -       else (align_left "Rule has fewer conclusions than arguments given"
    7.16 -          (map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts
    7.17 -        |> maps (prep_inst ctxt align_right (atomize_term thy))
    7.18 -        |> Drule.cterm_instantiate) r |> pair (Rule_Cases.get r))
    7.19 -      |> mod_cases thy
    7.20 -      |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
    7.21 -
    7.22 -    val ruleq =
    7.23 -      (case opt_rule of
    7.24 -        SOME rs => Seq.single (inst_rule (Rule_Cases.strict_mutual_rule ctxt rs))
    7.25 -      | NONE =>
    7.26 -          (get_inductP ctxt facts @
    7.27 -            map (special_rename_params defs_ctxt insts) (get_inductT ctxt insts))
    7.28 -          |> map_filter (Rule_Cases.mutual_rule ctxt)
    7.29 -          |> tap (trace_rules ctxt inductN o map #2)
    7.30 -          |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
    7.31 -
    7.32 -    fun rule_cases ctxt rule cases =
    7.33 -      let
    7.34 -        val rule' = Rule_Cases.internalize_params rule;
    7.35 -        val rule'' = rule' |> simp ? simplified_rule ctxt;
    7.36 -        val nonames = map (fn ((cn, _), cls) => ((cn, []), cls));
    7.37 -        val cases' = if Thm.eq_thm_prop (rule', rule'') then cases else nonames cases;
    7.38 -      in Rule_Cases.make_nested (Thm.prop_of rule'') (rulified_term rule'') cases' end;
    7.39 -  in
    7.40 -    (fn i => fn st =>
    7.41 -      ruleq
    7.42 -      |> Seq.maps (Rule_Cases.consume defs_ctxt (flat defs) facts)
    7.43 -      |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
    7.44 -        (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
    7.45 -          (CONJUNCTS (ALLGOALS
    7.46 -            let
    7.47 -              val adefs = nth_list atomized_defs (j - 1);
    7.48 -              val frees = fold (Term.add_frees o Thm.prop_of) adefs [];
    7.49 -              val xs = nth_list arbitrary (j - 1);
    7.50 -              val k = nth concls (j - 1) + more_consumes
    7.51 -            in
    7.52 -              Method.insert_tac (more_facts @ adefs) THEN'
    7.53 -                (if simp then
    7.54 -                   rotate_tac k (length adefs) THEN'
    7.55 -                   arbitrary_tac defs_ctxt k (List.partition (member op = frees) xs |> op @)
    7.56 -                 else
    7.57 -                   arbitrary_tac defs_ctxt k xs)
    7.58 -             end)
    7.59 -          THEN' inner_atomize_tac defs_ctxt) j))
    7.60 -        THEN' atomize_tac defs_ctxt) i st |> Seq.maps (fn st' =>
    7.61 -            guess_instance ctxt (internalize ctxt more_consumes rule) i st'
    7.62 -            |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
    7.63 -            |> Seq.maps (fn rule' =>
    7.64 -              CASES (rule_cases ctxt rule' cases)
    7.65 -                (rtac rule' i THEN
    7.66 -                  PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st'))))
    7.67 -    THEN_ALL_NEW_CASES
    7.68 -      ((if simp then simplify_tac ctxt THEN' (TRY o trivial_tac)
    7.69 -        else K all_tac)
    7.70 -       THEN_ALL_NEW rulify_tac ctxt)
    7.71 -  end;
    7.72 +  SUBGOAL_CASES (fn (_, i, st) =>
    7.73 +    let
    7.74 +      val thy = Proof_Context.theory_of ctxt;
    7.75 +  
    7.76 +      val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
    7.77 +      val atomized_defs = map (map (Conv.fconv_rule (atomize_cterm defs_ctxt))) defs;
    7.78 +  
    7.79 +      fun inst_rule (concls, r) =
    7.80 +        (if null insts then `Rule_Cases.get r
    7.81 +         else (align_left "Rule has fewer conclusions than arguments given"
    7.82 +            (map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts
    7.83 +          |> maps (prep_inst ctxt align_right (atomize_term thy))
    7.84 +          |> Drule.cterm_instantiate) r |> pair (Rule_Cases.get r))
    7.85 +        |> mod_cases thy
    7.86 +        |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
    7.87 +  
    7.88 +      val ruleq =
    7.89 +        (case opt_rule of
    7.90 +          SOME rs => Seq.single (inst_rule (Rule_Cases.strict_mutual_rule ctxt rs))
    7.91 +        | NONE =>
    7.92 +            (get_inductP ctxt facts @
    7.93 +              map (special_rename_params defs_ctxt insts) (get_inductT ctxt insts))
    7.94 +            |> map_filter (Rule_Cases.mutual_rule ctxt)
    7.95 +            |> tap (trace_rules ctxt inductN o map #2)
    7.96 +            |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
    7.97 +  
    7.98 +      fun rule_cases ctxt rule cases =
    7.99 +        let
   7.100 +          val rule' = Rule_Cases.internalize_params rule;
   7.101 +          val rule'' = rule' |> simp ? simplified_rule ctxt;
   7.102 +          val nonames = map (fn ((cn, _), cls) => ((cn, []), cls));
   7.103 +          val cases' = if Thm.eq_thm_prop (rule', rule'') then cases else nonames cases;
   7.104 +        in Rule_Cases.make_nested (Thm.prop_of rule'') (rulified_term rule'') cases' end;
   7.105 +    in
   7.106 +      fn st =>
   7.107 +        ruleq
   7.108 +        |> Seq.maps (Rule_Cases.consume defs_ctxt (flat defs) facts)
   7.109 +        |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
   7.110 +          (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
   7.111 +            (CONJUNCTS (ALLGOALS
   7.112 +              let
   7.113 +                val adefs = nth_list atomized_defs (j - 1);
   7.114 +                val frees = fold (Term.add_frees o Thm.prop_of) adefs [];
   7.115 +                val xs = nth_list arbitrary (j - 1);
   7.116 +                val k = nth concls (j - 1) + more_consumes
   7.117 +              in
   7.118 +                Method.insert_tac (more_facts @ adefs) THEN'
   7.119 +                  (if simp then
   7.120 +                     rotate_tac k (length adefs) THEN'
   7.121 +                     arbitrary_tac defs_ctxt k (List.partition (member op = frees) xs |> op @)
   7.122 +                   else
   7.123 +                     arbitrary_tac defs_ctxt k xs)
   7.124 +               end)
   7.125 +            THEN' inner_atomize_tac defs_ctxt) j))
   7.126 +          THEN' atomize_tac defs_ctxt) i st |> Seq.maps (fn st' =>
   7.127 +              guess_instance ctxt (internalize ctxt more_consumes rule) i st'
   7.128 +              |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
   7.129 +              |> Seq.maps (fn rule' =>
   7.130 +                CASES (rule_cases ctxt rule' cases)
   7.131 +                  (rtac rule' i THEN
   7.132 +                    PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st')))
   7.133 +      end)
   7.134 +      THEN_ALL_NEW_CASES
   7.135 +        ((if simp then simplify_tac ctxt THEN' (TRY o trivial_tac) else K all_tac)
   7.136 +         THEN_ALL_NEW rulify_tac ctxt);
   7.137  
   7.138  val induct_tac = gen_induct_tac (K I);
   7.139  
   7.140 @@ -832,7 +832,7 @@
   7.141  
   7.142  in
   7.143  
   7.144 -fun coinduct_tac ctxt inst taking opt_rule facts =
   7.145 +fun coinduct_tac ctxt inst taking opt_rule facts = SUBGOAL_CASES (fn (goal, i, st) =>
   7.146    let
   7.147      val thy = Proof_Context.theory_of ctxt;
   7.148  
   7.149 @@ -849,7 +849,7 @@
   7.150            |> tap (trace_rules ctxt coinductN)
   7.151            |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
   7.152    in
   7.153 -    SUBGOAL_CASES (fn (goal, i) => fn st =>
   7.154 +    fn st =>
   7.155        ruleq goal
   7.156        |> Seq.maps (Rule_Cases.consume ctxt [] facts)
   7.157        |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
   7.158 @@ -858,8 +858,8 @@
   7.159          |> Seq.maps (fn rule' =>
   7.160            CASES (Rule_Cases.make_common (thy,
   7.161                Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
   7.162 -            (Method.insert_tac more_facts i THEN rtac rule' i) st)))
   7.163 -  end;
   7.164 +            (Method.insert_tac more_facts i THEN rtac rule' i) st))
   7.165 +  end);
   7.166  
   7.167  end;
   7.168  
     8.1 --- a/src/ZF/Tools/induct_tacs.ML	Thu Mar 20 19:58:33 2014 +0100
     8.2 +++ b/src/ZF/Tools/induct_tacs.ML	Thu Mar 20 21:07:57 2014 +0100
     8.3 @@ -89,7 +89,7 @@
     8.4        (2) exhaustion works for VARIABLES in the premises, not general terms
     8.5  **)
     8.6  
     8.7 -fun exhaust_induct_tac exh ctxt var i state =
     8.8 +fun exhaust_induct_tac exh ctxt var i state = SUBGOAL (fn _ =>
     8.9    let
    8.10      val thy = Proof_Context.theory_of ctxt
    8.11      val ({context = ctxt', asms, ...}, _) = Subgoal.focus ctxt i state
    8.12 @@ -102,12 +102,12 @@
    8.13               [] => error "induction is not available for this datatype"
    8.14             | major::_ => FOLogic.dest_Trueprop major)
    8.15    in
    8.16 -    eres_inst_tac ctxt [(ixn, var)] rule i state
    8.17 +    eres_inst_tac ctxt [(ixn, var)] rule i
    8.18    end
    8.19    handle Find_tname msg =>
    8.20              if exh then (*try boolean case analysis instead*)
    8.21 -                case_tac ctxt var i state
    8.22 -            else error msg;
    8.23 +                case_tac ctxt var i
    8.24 +            else error msg) i state;
    8.25  
    8.26  val exhaust_tac = exhaust_induct_tac true;
    8.27  val induct_tac = exhaust_induct_tac false;