|
1 signature INDUCTION = |
|
2 sig |
|
3 val induction_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list -> |
|
4 (string * typ) list list -> term option list -> thm list option -> |
|
5 thm list -> int -> cases_tactic |
|
6 val setup: theory -> theory |
|
7 end |
|
8 |
|
9 structure Induction: INDUCTION = |
|
10 struct |
|
11 |
|
12 val ind_hypsN = "IH"; |
|
13 |
|
14 fun preds_of t = |
|
15 (case strip_comb t of |
|
16 (p as Var _, _) => [p] |
|
17 | (p as Free _, _) => [p] |
|
18 | (_, ts) => flat(map preds_of ts)) |
|
19 |
|
20 fun name_hyps thy (arg as ((cases,consumes),th)) = |
|
21 if not(forall (null o #2 o #1) cases) then arg |
|
22 else |
|
23 let |
|
24 val (prems, concl) = Logic.strip_horn (prop_of th); |
|
25 val prems' = drop consumes prems; |
|
26 val ps = preds_of concl; |
|
27 |
|
28 fun hname_of t = |
|
29 if exists_subterm (member (op =) ps) t |
|
30 then ind_hypsN else Rule_Cases.case_hypsN |
|
31 |
|
32 val hnamess = map (map hname_of o Logic.strip_assums_hyp) prems' |
|
33 val n = Int.min (length hnamess, length cases) |
|
34 val cases' = map (fn (((cn,_),concls),hns) => ((cn,hns),concls)) |
|
35 (take n cases ~~ take n hnamess) |
|
36 in ((cases',consumes),th) end |
|
37 |
|
38 val induction_tac = Induct.gen_induct_tac name_hyps |
|
39 |
|
40 val setup = Induct.gen_induct_setup @{binding induction} induction_tac |
|
41 |
|
42 end |
|
43 |