# HG changeset patch # User wenzelm # Date 1395346077 -3600 # Node ID b98813774a633d15dfeb37c012c6a2fff72c1291 # Parent 3e449273942ab6b15f3a604c2e7cafb53a5e447b enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range; diff -r 3e449273942a -r b98813774a63 src/HOL/Tools/Function/lexicographic_order.ML --- 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 diff -r 3e449273942a -r b98813774a63 src/HOL/Tools/Function/termination.ML --- 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 diff -r 3e449273942a -r b98813774a63 src/HOL/Tools/coinduction.ML --- 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 diff -r 3e449273942a -r b98813774a63 src/HOL/Topological_Spaces.thy --- 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 = {* diff -r 3e449273942a -r b98813774a63 src/Pure/Isar/rule_cases.ML --- 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 = diff -r 3e449273942a -r b98813774a63 src/Pure/tactical.ML --- 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 diff -r 3e449273942a -r b98813774a63 src/Tools/induct.ML --- 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; diff -r 3e449273942a -r b98813774a63 src/ZF/Tools/induct_tacs.ML --- 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;