5 name "IH". |
5 name "IH". |
6 *) |
6 *) |
7 |
7 |
8 signature INDUCTION = |
8 signature INDUCTION = |
9 sig |
9 sig |
10 val induction_tac: bool -> (binding option * (term * bool)) option list list -> |
10 val induction_context_tactic: bool -> (binding option * (term * bool)) option list list -> |
11 (string * typ) list list -> term option list -> thm list option -> |
11 (string * typ) list list -> term option list -> thm list option -> |
12 thm list -> int -> context_tactic |
12 thm list -> int -> context_tactic |
|
13 val induction_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list -> |
|
14 (string * typ) list list -> term option list -> thm list option -> |
|
15 thm list -> int -> tactic |
13 end |
16 end |
14 |
17 |
15 structure Induction: INDUCTION = |
18 structure Induction: INDUCTION = |
16 struct |
19 struct |
17 |
20 |
21 (case strip_comb t of |
24 (case strip_comb t of |
22 (p as Var _, _) => [p] |
25 (p as Var _, _) => [p] |
23 | (p as Free _, _) => [p] |
26 | (p as Free _, _) => [p] |
24 | (_, ts) => maps preds_of ts); |
27 | (_, ts) => maps preds_of ts); |
25 |
28 |
26 fun name_hyps (arg as ((cases, consumes), th)) = |
29 val induction_context_tactic = |
27 if not (forall (null o #2 o #1) cases) then arg |
30 Induct.gen_induct_context_tactic (fn arg as ((cases, consumes), th) => |
28 else |
31 if not (forall (null o #2 o #1) cases) then arg |
29 let |
32 else |
30 val (prems, concl) = Logic.strip_horn (Thm.prop_of th); |
33 let |
31 val prems' = drop consumes prems; |
34 val (prems, concl) = Logic.strip_horn (Thm.prop_of th); |
32 val ps = preds_of concl; |
35 val prems' = drop consumes prems; |
|
36 val ps = preds_of concl; |
|
37 |
|
38 fun hname_of t = |
|
39 if exists_subterm (member (op aconv) ps) t |
|
40 then ind_hypsN else Rule_Cases.case_hypsN; |
|
41 |
|
42 val hnamess = map (map hname_of o Logic.strip_assums_hyp) prems'; |
|
43 val n = Int.min (length hnamess, length cases); |
|
44 val cases' = |
|
45 map (fn (((cn, _), concls), hns) => ((cn, hns), concls)) |
|
46 (take n cases ~~ take n hnamess); |
|
47 in ((cases', consumes), th) end); |
33 |
48 |
34 fun hname_of t = |
49 fun induction_tac ctxt x1 x2 x3 x4 x5 x6 x7 = |
35 if exists_subterm (member (op aconv) ps) t |
50 Method.NO_CONTEXT_TACTIC ctxt (induction_context_tactic x1 x2 x3 x4 x5 x6 x7); |
36 then ind_hypsN else Rule_Cases.case_hypsN; |
|
37 |
51 |
38 val hnamess = map (map hname_of o Logic.strip_assums_hyp) prems'; |
52 val _ = |
39 val n = Int.min (length hnamess, length cases); |
53 Theory.local_setup (Induct.gen_induct_setup @{binding induction} induction_context_tactic); |
40 val cases' = |
|
41 map (fn (((cn, _), concls), hns) => ((cn, hns), concls)) |
|
42 (take n cases ~~ take n hnamess); |
|
43 in ((cases', consumes), th) end; |
|
44 |
|
45 val induction_tac = Induct.gen_induct_tac name_hyps; |
|
46 |
|
47 val _ = Theory.local_setup (Induct.gen_induct_setup @{binding induction} induction_tac); |
|
48 |
54 |
49 end |
55 end |