--- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Fri Mar 27 11:38:26 2015 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Fri Mar 27 17:46:08 2015 +0100
@@ -176,7 +176,7 @@
val tacs1 = [
quant_tac ctxt 1,
simp_tac (put_simpset HOL_ss ctxt) 1,
- Induct_Tacs.induct_tac ctxt [[SOME "n"]] 1,
+ Induct_Tacs.induct_tac ctxt [[SOME "n"]] NONE 1,
simp_tac (put_simpset take_ss ctxt addsimps prems) 1,
TRY (safe_tac (put_claset HOL_cs ctxt))]
fun con_tac _ =
--- a/src/HOL/MicroJava/J/JTypeSafe.thy Fri Mar 27 11:38:26 2015 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy Fri Mar 27 17:46:08 2015 +0100
@@ -244,7 +244,7 @@
THEN_ALL_NEW (full_simp_tac @{context}), REPEAT o (etac conjE), hyp_subst_tac @{context}] 3*})
-- "for if"
-apply( tactic {* (Induct_Tacs.case_tac @{context} "the_Bool v" [] THEN_ALL_NEW
+apply( tactic {* (Induct_Tacs.case_tac @{context} "the_Bool v" [] NONE THEN_ALL_NEW
(asm_full_simp_tac @{context})) 7*})
apply (tactic "forward_hyp_tac @{context}")
--- a/src/HOL/Nominal/nominal_atoms.ML Fri Mar 27 11:38:26 2015 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML Fri Mar 27 17:46:08 2015 +0100
@@ -131,7 +131,7 @@
(HOLogic.mk_exists ("x",@{typ nat},HOLogic.mk_eq (y,Const (ak_sign,inj_type) $ Bound 0)))
val proof2 = fn {prems, context = ctxt} =>
- Induct_Tacs.case_tac ctxt "y" [] 1 THEN
+ Induct_Tacs.case_tac ctxt "y" [] NONE 1 THEN
asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simp1) 1 THEN
rtac @{thm exI} 1 THEN
rtac @{thm refl} 1
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy Fri Mar 27 11:38:26 2015 +0100
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Fri Mar 27 17:46:08 2015 +0100
@@ -798,7 +798,7 @@
fun split_idle_tac ctxt =
SELECT_GOAL
(TRY (rtac @{thm actionI} 1) THEN
- Induct_Tacs.case_tac ctxt "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" [] 1 THEN
+ Induct_Tacs.case_tac ctxt "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" [] NONE 1 THEN
rewrite_goals_tac ctxt @{thms action_rews} THEN
forward_tac ctxt [temp_use ctxt @{thm Step1_4_7}] 1 THEN
asm_full_simp_tac ctxt 1);
--- a/src/Tools/induct_tacs.ML Fri Mar 27 11:38:26 2015 +0100
+++ b/src/Tools/induct_tacs.ML Fri Mar 27 17:46:08 2015 +0100
@@ -7,11 +7,9 @@
signature INDUCT_TACS =
sig
val case_tac: Proof.context -> string -> (binding * string option * mixfix) list ->
- int -> tactic
- val case_rule_tac: Proof.context -> string -> (binding * string option * mixfix) list ->
- thm -> int -> tactic
- val induct_tac: Proof.context -> string option list list -> int -> tactic
- val induct_rules_tac: Proof.context -> string option list list -> thm list -> int -> tactic
+ thm option -> int -> tactic
+ val induct_tac: Proof.context -> string option list list ->
+ thm list option -> int -> tactic
end
structure Induct_Tacs: INDUCT_TACS =
@@ -28,7 +26,7 @@
quote (Syntax.string_of_term ctxt u) ^ Position.here pos);
in (u, U) end;
-fun gen_case_tac ctxt s fixes opt_rule i st =
+fun case_tac ctxt s fixes opt_rule i st =
let
val rule =
(case opt_rule of
@@ -55,9 +53,6 @@
in Rule_Insts.res_inst_tac ctxt [((xi, Position.none), s)] fixes rule i st end
handle THM _ => Seq.empty;
-fun case_tac ctxt s xs = gen_case_tac ctxt s xs NONE;
-fun case_rule_tac ctxt s xs rule = gen_case_tac ctxt s xs (SOME rule);
-
(* induction *)
@@ -72,7 +67,7 @@
in
-fun gen_induct_tac ctxt0 varss opt_rules i st =
+fun induct_tac ctxt0 varss opt_rules i st =
let
val ((_, goal), ctxt) = Variable.focus_subgoal i st ctxt0;
val (prems, concl) = Logic.strip_horn (Thm.term_of goal);
@@ -117,9 +112,6 @@
end;
-fun induct_tac ctxt args = gen_induct_tac ctxt args NONE;
-fun induct_rules_tac ctxt args rules = gen_induct_tac ctxt args (SOME rules);
-
(* method syntax *)
@@ -139,14 +131,13 @@
Theory.setup
(Method.setup @{binding case_tac}
(Args.goal_spec -- Scan.lift (Args.name_inner_syntax -- Parse.for_fixes) -- opt_rule >>
- (fn ((quant, (s, xs)), r) => fn ctxt => SIMPLE_METHOD'' quant (gen_case_tac ctxt s xs r)))
+ (fn ((quant, (s, xs)), r) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s xs r)))
"unstructured case analysis on types" #>
Method.setup @{binding induct_tac}
(Args.goal_spec -- varss -- opt_rules >>
- (fn ((quant, vs), rs) => fn ctxt => SIMPLE_METHOD'' quant (gen_induct_tac ctxt vs rs)))
+ (fn ((quant, vs), rs) => fn ctxt => SIMPLE_METHOD'' quant (induct_tac ctxt vs rs)))
"unstructured induction on types");
end;
end;
-