--- a/src/HOL/Tools/Function/partial_function.ML Mon Dec 14 10:14:19 2015 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML Mon Dec 14 11:20:31 2015 +0100
@@ -93,7 +93,7 @@
| SOME (arg, conv) =>
let open Conv in
if Term.is_open arg then no_tac
- else ((DETERM o Method.NO_CONTEXT_TACTIC ctxt o Induct.cases_tac false [[SOME arg]] NONE [])
+ else ((DETERM o Induct.cases_tac ctxt false [[SOME arg]] NONE [])
THEN_ALL_NEW (rewrite_with_asm_tac ctxt 0)
THEN_ALL_NEW eresolve_tac ctxt @{thms thin_rl}
THEN_ALL_NEW (CONVERSION
--- a/src/HOL/Tools/coinduction.ML Mon Dec 14 10:14:19 2015 +0100
+++ b/src/HOL/Tools/coinduction.ML Mon Dec 14 11:20:31 2015 +0100
@@ -8,7 +8,8 @@
signature COINDUCTION =
sig
- val coinduction_tac: term list -> thm option -> thm list -> int -> context_tactic
+ val coinduction_context_tactic: term list -> thm option -> thm list -> int -> context_tactic
+ val coinduction_tac: Proof.context -> term list -> thm option -> thm list -> int -> tactic
end;
structure Coinduction : COINDUCTION =
@@ -37,7 +38,7 @@
(THEN_ALL_NEW_SKIP skip tac (REPEAT_DETERM_N n o eresolve0_tac [thin_rl])) i st
end;
-fun coinduction_tac raw_vars opt_raw_thm prems =
+fun coinduction_context_tactic raw_vars opt_raw_thm prems =
CONTEXT_SUBGOAL (fn (goal, i) => fn (ctxt, st) =>
let
val lhs_of_eq = HOLogic.dest_Trueprop #> HOLogic.dest_eq #> fst;
@@ -117,6 +118,10 @@
CONTEXT_CASES (Rule_Cases.make_common ctxt (Thm.prop_of st') cases) all_tac (ctxt, st'))
end);
+fun coinduction_tac ctxt x1 x2 x3 x4 =
+ Method.NO_CONTEXT_TACTIC ctxt (coinduction_context_tactic x1 x2 x3 x4);
+
+
local
val ruleN = "rule"
@@ -153,7 +158,7 @@
(Method.setup @{binding coinduction}
(arbitrary -- Scan.option coinduct_rule >>
(fn (arbitrary, opt_rule) => fn _ => fn facts =>
- Seq.DETERM (coinduction_tac arbitrary opt_rule facts 1)))
+ Seq.DETERM (coinduction_context_tactic arbitrary opt_rule facts 1)))
"coinduction on types or predicates/sets");
end;
--- a/src/Tools/induct.ML Mon Dec 14 10:14:19 2015 +0100
+++ b/src/Tools/induct.ML Mon Dec 14 11:20:31 2015 +0100
@@ -71,17 +71,32 @@
val rotate_tac: int -> int -> int -> tactic
val internalize: Proof.context -> int -> thm -> thm
val guess_instance: Proof.context -> thm -> int -> thm -> thm Seq.seq
- val cases_tac: bool -> term option list list -> thm option -> thm list -> int -> context_tactic
+ val cases_context_tactic: bool -> term option list list -> thm option ->
+ thm list -> int -> context_tactic
+ val cases_tac: Proof.context -> bool -> term option list list -> thm option ->
+ thm list -> int -> tactic
val get_inductT: Proof.context -> term option list list -> thm list list
- val gen_induct_tac: ((Rule_Cases.info * int) * thm -> (Rule_Cases.info * int) * thm) ->
+ val gen_induct_context_tactic: ((Rule_Cases.info * int) * thm -> (Rule_Cases.info * int) * thm) ->
bool -> (binding option * (term * bool)) option list list ->
(string * typ) list list -> term option list -> thm list option ->
thm list -> int -> context_tactic
- val induct_tac: bool -> (binding option * (term * bool)) option list list ->
+ val gen_induct_tac: Proof.context ->
+ ((Rule_Cases.info * int) * thm -> (Rule_Cases.info * int) * thm) ->
+ bool -> (binding option * (term * bool)) option list list ->
+ (string * typ) list list -> term option list -> thm list option ->
+ thm list -> int -> tactic
+ val induct_context_tactic: bool ->
+ (binding option * (term * bool)) option list list ->
(string * typ) list list -> term option list -> thm list option ->
thm list -> int -> context_tactic
- val coinduct_tac: term option list -> term option list -> thm option ->
+ val induct_tac: Proof.context -> bool ->
+ (binding option * (term * bool)) option list list ->
+ (string * typ) list list -> term option list -> thm list option ->
+ thm list -> int -> tactic
+ val coinduct_context_tactic: term option list -> term option list -> thm option ->
thm list -> int -> context_tactic
+ val coinduct_tac: Proof.context -> term option list -> term option list -> thm option ->
+ thm list -> int -> tactic
val gen_induct_setup: binding ->
(bool -> (binding option * (term * bool)) option list list ->
(string * typ) list list -> term option list -> thm list option ->
@@ -477,7 +492,7 @@
in
-fun cases_tac simp insts opt_rule facts i : context_tactic =
+fun cases_context_tactic simp insts opt_rule facts i : context_tactic =
fn (ctxt, st) =>
let
fun inst_rule r =
@@ -518,6 +533,9 @@
end)
end;
+fun cases_tac ctxt x1 x2 x3 x4 x5 =
+ Method.NO_CONTEXT_TACTIC ctxt (cases_context_tactic x1 x2 x3 x4 x5);
+
end;
@@ -739,7 +757,7 @@
fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact))
| get_inductP _ _ = [];
-fun gen_induct_tac mod_cases simp def_insts arbitrary taking opt_rule facts =
+fun gen_induct_context_tactic mod_cases simp def_insts arbitrary taking opt_rule facts =
CONTEXT_SUBGOAL (fn (_, i) => fn (ctxt, st) =>
let
val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
@@ -806,7 +824,13 @@
THEN_ALL_NEW rulify_tac ctxt)) i (ctxt, st)
end)
-val induct_tac = gen_induct_tac I;
+val induct_context_tactic = gen_induct_context_tactic I;
+
+fun gen_induct_tac ctxt x1 x2 x3 x4 x5 x6 x7 x8 =
+ Method.NO_CONTEXT_TACTIC ctxt (gen_induct_context_tactic x1 x2 x3 x4 x5 x6 x7 x8);
+
+fun induct_tac ctxt x1 x2 x3 x4 x5 x6 x7 =
+ Method.NO_CONTEXT_TACTIC ctxt (induct_context_tactic x1 x2 x3 x4 x5 x6 x7);
@@ -831,7 +855,7 @@
in
-fun coinduct_tac inst taking opt_rule facts =
+fun coinduct_context_tactic inst taking opt_rule facts =
CONTEXT_SUBGOAL (fn (goal, i) => fn (ctxt, st) =>
let
fun inst_rule r =
@@ -856,6 +880,9 @@
(Method.insert_tac ctxt more_facts i THEN resolve_tac ctxt [rule'] i) (ctxt, st)))
end);
+fun coinduct_tac ctxt x1 x2 x3 x4 x5 =
+ Method.NO_CONTEXT_TACTIC ctxt (coinduct_context_tactic x1 x2 x3 x4 x5);
+
end;
@@ -930,13 +957,13 @@
(Parse.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >>
(fn (no_simp, (insts, opt_rule)) => fn _ =>
CONTEXT_METHOD (fn facts =>
- Seq.DETERM (cases_tac (not no_simp) insts opt_rule facts 1))))
+ Seq.DETERM (cases_context_tactic (not no_simp) insts opt_rule facts 1))))
"case analysis on types or predicates/sets" #>
- gen_induct_setup @{binding induct} induct_tac #>
+ gen_induct_setup @{binding induct} induct_context_tactic #>
Method.local_setup @{binding coinduct}
(Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >>
(fn ((insts, taking), opt_rule) => fn _ => fn facts =>
- Seq.DETERM (coinduct_tac insts taking opt_rule facts 1)))
+ Seq.DETERM (coinduct_context_tactic insts taking opt_rule facts 1)))
"coinduction on types or predicates/sets");
end;
--- a/src/Tools/induction.ML Mon Dec 14 10:14:19 2015 +0100
+++ b/src/Tools/induction.ML Mon Dec 14 11:20:31 2015 +0100
@@ -7,9 +7,12 @@
signature INDUCTION =
sig
- val induction_tac: bool -> (binding option * (term * bool)) option list list ->
+ val induction_context_tactic: bool -> (binding option * (term * bool)) option list list ->
(string * typ) list list -> term option list -> thm list option ->
thm list -> int -> context_tactic
+ val induction_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
+ (string * typ) list list -> term option list -> thm list option ->
+ thm list -> int -> tactic
end
structure Induction: INDUCTION =
@@ -23,27 +26,30 @@
| (p as Free _, _) => [p]
| (_, ts) => maps preds_of ts);
-fun name_hyps (arg as ((cases, consumes), th)) =
- if not (forall (null o #2 o #1) cases) then arg
- else
- let
- val (prems, concl) = Logic.strip_horn (Thm.prop_of th);
- val prems' = drop consumes prems;
- val ps = preds_of concl;
+val induction_context_tactic =
+ Induct.gen_induct_context_tactic (fn arg as ((cases, consumes), th) =>
+ if not (forall (null o #2 o #1) cases) then arg
+ else
+ let
+ val (prems, concl) = Logic.strip_horn (Thm.prop_of th);
+ val prems' = drop consumes prems;
+ val ps = preds_of concl;
+
+ fun hname_of t =
+ if exists_subterm (member (op aconv) ps) t
+ then ind_hypsN else Rule_Cases.case_hypsN;
+
+ val hnamess = map (map hname_of o Logic.strip_assums_hyp) prems';
+ val n = Int.min (length hnamess, length cases);
+ val cases' =
+ map (fn (((cn, _), concls), hns) => ((cn, hns), concls))
+ (take n cases ~~ take n hnamess);
+ in ((cases', consumes), th) end);
- fun hname_of t =
- if exists_subterm (member (op aconv) ps) t
- then ind_hypsN else Rule_Cases.case_hypsN;
+fun induction_tac ctxt x1 x2 x3 x4 x5 x6 x7 =
+ Method.NO_CONTEXT_TACTIC ctxt (induction_context_tactic x1 x2 x3 x4 x5 x6 x7);
- val hnamess = map (map hname_of o Logic.strip_assums_hyp) prems';
- val n = Int.min (length hnamess, length cases);
- val cases' =
- map (fn (((cn, _), concls), hns) => ((cn, hns), concls))
- (take n cases ~~ take n hnamess);
- in ((cases', consumes), th) end;
-
-val induction_tac = Induct.gen_induct_tac name_hyps;
-
-val _ = Theory.local_setup (Induct.gen_induct_setup @{binding induction} induction_tac);
+val _ =
+ Theory.local_setup (Induct.gen_induct_setup @{binding induction} induction_context_tactic);
end