author  blanchet 
Mon, 26 Nov 2012 13:35:05 +0100  
changeset 50222  40e3c3be6bca 
parent 45014  0e847655b2d8 
child 56506  c1f04411d43f 
permissions  rwrr 
45014
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

1 
signature INDUCTION = 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

2 
sig 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

3 
val induction_tac: Proof.context > bool > (binding option * (term * bool)) option list list > 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

4 
(string * typ) list list > term option list > thm list option > 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

5 
thm list > int > cases_tactic 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

6 
val setup: theory > theory 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

7 
end 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

8 

0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

9 
structure Induction: INDUCTION = 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

10 
struct 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

11 

0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

12 
val ind_hypsN = "IH"; 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

13 

0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

14 
fun preds_of t = 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

15 
(case strip_comb t of 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

16 
(p as Var _, _) => [p] 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

17 
 (p as Free _, _) => [p] 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

18 
 (_, ts) => flat(map preds_of ts)) 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

19 

0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

20 
fun name_hyps thy (arg as ((cases,consumes),th)) = 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

21 
if not(forall (null o #2 o #1) cases) then arg 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

22 
else 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

23 
let 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

24 
val (prems, concl) = Logic.strip_horn (prop_of th); 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

25 
val prems' = drop consumes prems; 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

26 
val ps = preds_of concl; 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

27 

0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

28 
fun hname_of t = 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

29 
if exists_subterm (member (op =) ps) t 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

30 
then ind_hypsN else Rule_Cases.case_hypsN 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

31 

0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

32 
val hnamess = map (map hname_of o Logic.strip_assums_hyp) prems' 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

33 
val n = Int.min (length hnamess, length cases) 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

34 
val cases' = map (fn (((cn,_),concls),hns) => ((cn,hns),concls)) 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

35 
(take n cases ~~ take n hnamess) 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

36 
in ((cases',consumes),th) end 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

37 

0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

38 
val induction_tac = Induct.gen_induct_tac name_hyps 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

39 

0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

40 
val setup = Induct.gen_induct_setup @{binding induction} induction_tac 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

41 

0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

42 
end 
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff
changeset

43 