enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
--- a/src/HOL/Tools/Function/lexicographic_order.ML Thu Mar 20 19:58:33 2014 +0100
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Thu Mar 20 21:07:57 2014 +0100
@@ -174,7 +174,7 @@
(** The Main Function **)
-fun lex_order_tac quiet ctxt solve_tac (st: thm) =
+fun lex_order_tac quiet ctxt solve_tac st = SUBGOAL (fn _ =>
let
val thy = Proof_Context.theory_of ctxt
val ((_ $ (_ $ rel)) :: tl) = prems_of st
@@ -187,26 +187,27 @@
val table = (* 2: create table *)
map (fn t => map (mk_cell thy solve_tac (dest_term t)) measure_funs) tl
in
- case search_table table of
- NONE => if quiet then no_tac st else error (no_order_msg ctxt table tl measure_funs)
- | SOME order =>
- let
- val clean_table = map (fn x => map (nth x) order) table
- val relation = mk_measures domT (map (nth measure_funs) order)
- val _ =
- if not quiet then
- Pretty.writeln (Pretty.block
- [Pretty.str "Found termination order:", Pretty.brk 1,
- Pretty.quote (Syntax.pretty_term ctxt relation)])
- else ()
-
- in (* 4: proof reconstruction *)
- st |> (PRIMITIVE (cterm_instantiate [(cterm_of thy rel, cterm_of thy relation)])
- THEN (REPEAT (rtac @{thm "wf_mlex"} 1))
- THEN (rtac @{thm "wf_empty"} 1)
- THEN EVERY (map prove_row clean_table))
- end
- end
+ fn st =>
+ case search_table table of
+ NONE => if quiet then no_tac st else error (no_order_msg ctxt table tl measure_funs)
+ | SOME order =>
+ let
+ val clean_table = map (fn x => map (nth x) order) table
+ val relation = mk_measures domT (map (nth measure_funs) order)
+ val _ =
+ if not quiet then
+ Pretty.writeln (Pretty.block
+ [Pretty.str "Found termination order:", Pretty.brk 1,
+ Pretty.quote (Syntax.pretty_term ctxt relation)])
+ else ()
+
+ in (* 4: proof reconstruction *)
+ st |> (PRIMITIVE (cterm_instantiate [(cterm_of thy rel, cterm_of thy relation)])
+ THEN (REPEAT (rtac @{thm "wf_mlex"} 1))
+ THEN (rtac @{thm "wf_empty"} 1)
+ THEN EVERY (map prove_row clean_table))
+ end
+ end) 1 st;
fun lexicographic_order_tac quiet ctxt =
TRY (Function_Common.apply_termination_rule ctxt 1) THEN
--- a/src/HOL/Tools/Function/termination.ML Thu Mar 20 19:58:33 2014 +0100
+++ b/src/HOL/Tools/Function/termination.ML Thu Mar 20 21:07:57 2014 +0100
@@ -272,10 +272,10 @@
in
-fun wf_union_tac ctxt st =
+fun wf_union_tac ctxt st = SUBGOAL (fn _ =>
let
val thy = Proof_Context.theory_of ctxt
- val cert = cterm_of (theory_of_thm st)
+ val cert = cterm_of thy
val ((_ $ (_ $ rel)) :: ineqs) = prems_of st
fun mk_compr ineq =
@@ -304,8 +304,8 @@
in
(PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)])
THEN ALLGOALS (fn i => if i = 1 then all_tac else solve_membership_tac i)
- THEN rewrite_goal_tac ctxt Un_aci_simps 1) st (* eliminate duplicates *)
- end
+ THEN rewrite_goal_tac ctxt Un_aci_simps 1) (* eliminate duplicates *)
+ end) 1 st
end
--- a/src/HOL/Tools/coinduction.ML Thu Mar 20 19:58:33 2014 +0100
+++ b/src/HOL/Tools/coinduction.ML Thu Mar 20 21:07:57 2014 +0100
@@ -40,19 +40,20 @@
(THEN_ALL_NEW_SKIP skip tac (REPEAT_DETERM_N n o etac thin_rl)) i st
end;
-fun coinduction_tac ctxt raw_vars opt_raw_thm prems st =
+fun coinduction_tac ctxt raw_vars opt_raw_thm prems = HEADGOAL (SUBGOAL_CASES (fn (goal, _, _) =>
let
val lhs_of_eq = HOLogic.dest_Trueprop #> HOLogic.dest_eq #> fst;
fun find_coinduct t =
Induct.find_coinductP ctxt t @
(try (Induct.find_coinductT ctxt o fastype_of o lhs_of_eq) t |> the_default [])
- val raw_thm = case opt_raw_thm
- of SOME raw_thm => raw_thm
- | NONE => st |> prems_of |> hd |> Logic.strip_assums_concl |> find_coinduct |> hd;
+ val raw_thm =
+ (case opt_raw_thm of
+ SOME raw_thm => raw_thm
+ | NONE => goal |> Logic.strip_assums_concl |> find_coinduct |> hd);
val skip = Integer.max 1 (Rule_Cases.get_consumes raw_thm) - 1
val cases = Rule_Cases.get raw_thm |> fst
in
- NO_CASES (HEADGOAL (
+ HEADGOAL (
Object_Logic.rulify_tac ctxt THEN'
Method.insert_tac prems THEN'
Object_Logic.atomize_prems_tac ctxt THEN'
@@ -110,10 +111,10 @@
unfold_thms_tac ctxt eqs
end)) ctxt)))])
end) ctxt) THEN'
- K (prune_params_tac ctxt))) st
- |> Seq.maps (fn (_, st) =>
+ K (prune_params_tac ctxt))
+ #> Seq.maps (fn st =>
CASES (Rule_Cases.make_common (Proof_Context.theory_of ctxt, prop_of st) cases) all_tac st)
- end;
+ end));
local
--- a/src/HOL/Topological_Spaces.thy Thu Mar 20 19:58:33 2014 +0100
+++ b/src/HOL/Topological_Spaces.thy Thu Mar 20 21:07:57 2014 +0100
@@ -373,7 +373,7 @@
qed
ML {*
- fun eventually_elim_tac ctxt thms thm =
+ fun eventually_elim_tac ctxt thms = SUBGOAL_CASES (fn (_, _, st) =>
let
val thy = Proof_Context.theory_of ctxt
val mp_thms = thms RL [@{thm eventually_rev_mp}]
@@ -381,11 +381,11 @@
(@{thm allI} RS @{thm always_eventually})
|> fold (fn thm1 => fn thm2 => thm2 RS thm1) mp_thms
|> fold (fn _ => fn thm => @{thm impI} RS thm) thms
- val cases_prop = prop_of (raw_elim_thm RS thm)
+ val cases_prop = prop_of (raw_elim_thm RS st)
val cases = (Rule_Cases.make_common (thy, cases_prop) [(("elim", []), [])])
in
- CASES cases (rtac raw_elim_thm 1) thm
- end
+ CASES cases (rtac raw_elim_thm 1)
+ end) 1
*}
method_setup eventually_elim = {*
--- a/src/Pure/Isar/rule_cases.ML Thu Mar 20 19:58:33 2014 +0100
+++ b/src/Pure/Isar/rule_cases.ML Thu Mar 20 21:07:57 2014 +0100
@@ -12,7 +12,7 @@
type cases_tactic
val CASES: cases -> tactic -> cases_tactic
val NO_CASES: tactic -> cases_tactic
- val SUBGOAL_CASES: ((term * int) -> cases_tactic) -> int -> cases_tactic
+ val SUBGOAL_CASES: ((term * int * thm) -> cases_tactic) -> int -> cases_tactic
val THEN_ALL_NEW_CASES: (int -> cases_tactic) * (int -> tactic) -> int -> cases_tactic
end
@@ -190,7 +190,7 @@
fun SUBGOAL_CASES tac i st =
(case try Logic.nth_prem (i, Thm.prop_of st) of
- SOME goal => tac (goal, i) st
+ SOME goal => tac (goal, i, st) st
| NONE => Seq.empty);
fun (tac1 THEN_ALL_NEW_CASES tac2) i st =
--- a/src/Pure/tactical.ML Thu Mar 20 19:58:33 2014 +0100
+++ b/src/Pure/tactical.ML Thu Mar 20 21:07:57 2014 +0100
@@ -334,15 +334,14 @@
(*Returns all states that have changed in subgoal i, counted from the LAST
subgoal. For stac, for example.*)
fun CHANGED_GOAL tac i st =
- let val np = Thm.nprems_of st
- val d = np-i (*distance from END*)
- val t = Thm.term_of (Thm.cprem_of st i)
- fun diff st' =
- Thm.nprems_of st' - d <= 0 (*the subgoal no longer exists*)
- orelse
- not (Envir.aeconv (t, Thm.term_of (Thm.cprem_of st' (Thm.nprems_of st' - d))))
- in Seq.filter diff (tac i st) end
- handle General.Subscript => Seq.empty (*no subgoal i*);
+ SUBGOAL (fn (t, _) =>
+ let
+ val np = Thm.nprems_of st;
+ val d = np - i; (*distance from END*)
+ fun diff st' =
+ Thm.nprems_of st' - d <= 0 orelse (*the subgoal no longer exists*)
+ not (Envir.aeconv (t, Thm.term_of (Thm.cprem_of st' (Thm.nprems_of st' - d))));
+ in Seq.filter diff o tac i end) i st;
(*Returns all states where some subgoals have been solved. For
subgoal-based tactics this means subgoal i has been solved
--- a/src/Tools/induct.ML Thu Mar 20 19:58:33 2014 +0100
+++ b/src/Tools/induct.ML Thu Mar 20 21:07:57 2014 +0100
@@ -741,71 +741,71 @@
type case_data = (((string * string list) * string list) list * int);
fun gen_induct_tac mod_cases ctxt simp def_insts arbitrary taking opt_rule facts =
- let
- val thy = Proof_Context.theory_of ctxt;
-
- val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
- val atomized_defs = map (map (Conv.fconv_rule (atomize_cterm defs_ctxt))) defs;
-
- fun inst_rule (concls, r) =
- (if null insts then `Rule_Cases.get r
- else (align_left "Rule has fewer conclusions than arguments given"
- (map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts
- |> maps (prep_inst ctxt align_right (atomize_term thy))
- |> Drule.cterm_instantiate) r |> pair (Rule_Cases.get r))
- |> mod_cases thy
- |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
-
- val ruleq =
- (case opt_rule of
- SOME rs => Seq.single (inst_rule (Rule_Cases.strict_mutual_rule ctxt rs))
- | NONE =>
- (get_inductP ctxt facts @
- map (special_rename_params defs_ctxt insts) (get_inductT ctxt insts))
- |> map_filter (Rule_Cases.mutual_rule ctxt)
- |> tap (trace_rules ctxt inductN o map #2)
- |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
-
- fun rule_cases ctxt rule cases =
- let
- val rule' = Rule_Cases.internalize_params rule;
- val rule'' = rule' |> simp ? simplified_rule ctxt;
- val nonames = map (fn ((cn, _), cls) => ((cn, []), cls));
- val cases' = if Thm.eq_thm_prop (rule', rule'') then cases else nonames cases;
- in Rule_Cases.make_nested (Thm.prop_of rule'') (rulified_term rule'') cases' end;
- in
- (fn i => fn st =>
- ruleq
- |> Seq.maps (Rule_Cases.consume defs_ctxt (flat defs) facts)
- |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
- (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
- (CONJUNCTS (ALLGOALS
- let
- val adefs = nth_list atomized_defs (j - 1);
- val frees = fold (Term.add_frees o Thm.prop_of) adefs [];
- val xs = nth_list arbitrary (j - 1);
- val k = nth concls (j - 1) + more_consumes
- in
- Method.insert_tac (more_facts @ adefs) THEN'
- (if simp then
- rotate_tac k (length adefs) THEN'
- arbitrary_tac defs_ctxt k (List.partition (member op = frees) xs |> op @)
- else
- arbitrary_tac defs_ctxt k xs)
- end)
- THEN' inner_atomize_tac defs_ctxt) j))
- THEN' atomize_tac defs_ctxt) i st |> Seq.maps (fn st' =>
- guess_instance ctxt (internalize ctxt more_consumes rule) i st'
- |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
- |> Seq.maps (fn rule' =>
- CASES (rule_cases ctxt rule' cases)
- (rtac rule' i THEN
- PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st'))))
- THEN_ALL_NEW_CASES
- ((if simp then simplify_tac ctxt THEN' (TRY o trivial_tac)
- else K all_tac)
- THEN_ALL_NEW rulify_tac ctxt)
- end;
+ SUBGOAL_CASES (fn (_, i, st) =>
+ let
+ val thy = Proof_Context.theory_of ctxt;
+
+ val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
+ val atomized_defs = map (map (Conv.fconv_rule (atomize_cterm defs_ctxt))) defs;
+
+ fun inst_rule (concls, r) =
+ (if null insts then `Rule_Cases.get r
+ else (align_left "Rule has fewer conclusions than arguments given"
+ (map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts
+ |> maps (prep_inst ctxt align_right (atomize_term thy))
+ |> Drule.cterm_instantiate) r |> pair (Rule_Cases.get r))
+ |> mod_cases thy
+ |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
+
+ val ruleq =
+ (case opt_rule of
+ SOME rs => Seq.single (inst_rule (Rule_Cases.strict_mutual_rule ctxt rs))
+ | NONE =>
+ (get_inductP ctxt facts @
+ map (special_rename_params defs_ctxt insts) (get_inductT ctxt insts))
+ |> map_filter (Rule_Cases.mutual_rule ctxt)
+ |> tap (trace_rules ctxt inductN o map #2)
+ |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
+
+ fun rule_cases ctxt rule cases =
+ let
+ val rule' = Rule_Cases.internalize_params rule;
+ val rule'' = rule' |> simp ? simplified_rule ctxt;
+ val nonames = map (fn ((cn, _), cls) => ((cn, []), cls));
+ val cases' = if Thm.eq_thm_prop (rule', rule'') then cases else nonames cases;
+ in Rule_Cases.make_nested (Thm.prop_of rule'') (rulified_term rule'') cases' end;
+ in
+ fn st =>
+ ruleq
+ |> Seq.maps (Rule_Cases.consume defs_ctxt (flat defs) facts)
+ |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
+ (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
+ (CONJUNCTS (ALLGOALS
+ let
+ val adefs = nth_list atomized_defs (j - 1);
+ val frees = fold (Term.add_frees o Thm.prop_of) adefs [];
+ val xs = nth_list arbitrary (j - 1);
+ val k = nth concls (j - 1) + more_consumes
+ in
+ Method.insert_tac (more_facts @ adefs) THEN'
+ (if simp then
+ rotate_tac k (length adefs) THEN'
+ arbitrary_tac defs_ctxt k (List.partition (member op = frees) xs |> op @)
+ else
+ arbitrary_tac defs_ctxt k xs)
+ end)
+ THEN' inner_atomize_tac defs_ctxt) j))
+ THEN' atomize_tac defs_ctxt) i st |> Seq.maps (fn st' =>
+ guess_instance ctxt (internalize ctxt more_consumes rule) i st'
+ |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
+ |> Seq.maps (fn rule' =>
+ CASES (rule_cases ctxt rule' cases)
+ (rtac rule' i THEN
+ PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st')))
+ end)
+ THEN_ALL_NEW_CASES
+ ((if simp then simplify_tac ctxt THEN' (TRY o trivial_tac) else K all_tac)
+ THEN_ALL_NEW rulify_tac ctxt);
val induct_tac = gen_induct_tac (K I);
@@ -832,7 +832,7 @@
in
-fun coinduct_tac ctxt inst taking opt_rule facts =
+fun coinduct_tac ctxt inst taking opt_rule facts = SUBGOAL_CASES (fn (goal, i, st) =>
let
val thy = Proof_Context.theory_of ctxt;
@@ -849,7 +849,7 @@
|> tap (trace_rules ctxt coinductN)
|> Seq.of_list |> Seq.maps (Seq.try inst_rule));
in
- SUBGOAL_CASES (fn (goal, i) => fn st =>
+ fn st =>
ruleq goal
|> Seq.maps (Rule_Cases.consume ctxt [] facts)
|> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
@@ -858,8 +858,8 @@
|> Seq.maps (fn rule' =>
CASES (Rule_Cases.make_common (thy,
Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
- (Method.insert_tac more_facts i THEN rtac rule' i) st)))
- end;
+ (Method.insert_tac more_facts i THEN rtac rule' i) st))
+ end);
end;
--- a/src/ZF/Tools/induct_tacs.ML Thu Mar 20 19:58:33 2014 +0100
+++ b/src/ZF/Tools/induct_tacs.ML Thu Mar 20 21:07:57 2014 +0100
@@ -89,7 +89,7 @@
(2) exhaustion works for VARIABLES in the premises, not general terms
**)
-fun exhaust_induct_tac exh ctxt var i state =
+fun exhaust_induct_tac exh ctxt var i state = SUBGOAL (fn _ =>
let
val thy = Proof_Context.theory_of ctxt
val ({context = ctxt', asms, ...}, _) = Subgoal.focus ctxt i state
@@ -102,12 +102,12 @@
[] => error "induction is not available for this datatype"
| major::_ => FOLogic.dest_Trueprop major)
in
- eres_inst_tac ctxt [(ixn, var)] rule i state
+ eres_inst_tac ctxt [(ixn, var)] rule i
end
handle Find_tname msg =>
if exh then (*try boolean case analysis instead*)
- case_tac ctxt var i state
- else error msg;
+ case_tac ctxt var i
+ else error msg) i state;
val exhaust_tac = exhaust_induct_tac true;
val induct_tac = exhaust_induct_tac false;