# HG changeset patch # User wenzelm # Date 975519760 -3600 # Node ID 92cd56dfc17e78d8002d3e2a8fa624341b9d02a7 # Parent fdec07d4f04759a3602de1be0ddc092754b135d1 resolveq_cases_tac moved here from Pure/Isar/method.ML; induct: proper handling of non-consumed facts; diff -r fdec07d4f047 -r 92cd56dfc17e src/HOL/Tools/induct_method.ML --- a/src/HOL/Tools/induct_method.ML Wed Nov 29 18:41:43 2000 +0100 +++ b/src/HOL/Tools/induct_method.ML Wed Nov 29 18:42:40 2000 +0100 @@ -91,6 +91,22 @@ end; +(* resolution and cases *) + +local + +fun gen_resolveq_tac tac rules i st = + Seq.flat (Seq.map (fn rule => tac rule i st) rules); + +in + +fun resolveq_cases_tac make tac = gen_resolveq_tac (fn (rule, (cases, facts)) => fn i => fn st => + Seq.map (rpair (make rule cases)) + ((Method.insert_tac facts THEN' tac THEN' Tactic.rtac rule) i st)); + +end; + + (** cases method **) @@ -161,7 +177,7 @@ fun prep_rule (thm, (cases, n)) = Seq.map (apsnd (rpair (drop (n, facts))) o cond_simp cases) (Method.multi_resolves (take (n, facts)) [thm]); in - Method.resolveq_cases_tac (RuleCases.make open_parms) + resolveq_cases_tac (RuleCases.make open_parms) (K all_tac) (Seq.flat (Seq.map prep_rule (Seq.of_list rules))) end; @@ -277,11 +293,10 @@ fun prep_rule (thm, (cases, n)) = Seq.map (rpair (cases, drop (n, facts))) (Method.multi_resolves (take (n, facts)) [thm]); - val tac = Method.resolveq_cases_tac (rulify_cases cert open_parms) + val tac = resolveq_cases_tac (rulify_cases cert open_parms) atomize_tac (Seq.flat (Seq.map prep_rule (Seq.of_list rules))); in - (fn i => Seq.THEN (atomize_tac i, tac i)) THEN_ALL_NEW_CASES - (rulify_tac THEN' (if stripped then weak_strip_tac else K all_tac)) + tac THEN_ALL_NEW_CASES (rulify_tac THEN' (if stripped then weak_strip_tac else K all_tac)) end; in