1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
|
% FILE : num_tac.ml %
% DESCRIPTION : contains the rule and tactic for general induction. %
% %
% %
% AUTHOR : E. L. Gunter %
% DATE : 89.3.23 %
% %
%-----------------------------------------------------------------------%
% add_lib_path `group`;; Not needed for HOL88.1.05 (MJCG 14 April, 1989)%
ml_curried_infix `and_then`;;
%GEN_INDUCTION =
|- !P. P 0 /\ (!n. (!m. m < n ==> P m) ==> P n) ==> (!n. P n)%
% GEN_INDUCT_RULE : thm -> thm -> thm
A1 |- P(0) A2 |- (!n. (!m. m < n ==> P(m)) ==> P(n))
--------------------------------------------------------
A1 u A2 |- !n. P(n)
%
let GEN_INDUCT_RULE (thm1:thm) (thm2:thm)=(
let var1,(test1,prop1)=((fst(dest_forall(concl thm2))),
(dest_imp(snd(dest_forall(concl thm2)))))
in
let var2=fst(dest_forall test1) in
let P = "\^var1.^prop1" in
let x and_then f = f x in
let IND_thm =
(EQ_MP
(ALPHA "!P.P 0/\(!n.(!m.m<n ==> P m) ==> P n) ==> (!n.P n)"
"!P.P 0/\(!^var1.(!^var2.^var2<^var1 ==> P ^var2) ==> P ^var1)
==> (!^var1.P ^var1)")
(theorem `ineq` `GEN_INDUCTION`)) and_then
(SPEC P) and_then
(\thm.EQ_MP (((DEPTH_CONV BETA_CONV)o concl)thm) thm)
in
(MP IND_thm (CONJ thm1 thm2)) )?failwith `GEN_INDUCT_RULE`;;
% GEN_INDUCT_TAC : tactic
[A] !n. P n
======================================================
[A] P(0) [A;(!m. m < n ==> P m)] P(n)
%
let GEN_INDUCT_TAC ((hypoth,aim):goal) =(
let var,prop=dest_forall(aim) in
let var1=variant ((frees aim) @ (freesl hypoth)) var in
let prop1=subst [(var1,var)] prop in
let var2=variant (frees prop) "m:num" in
let assum="!^var2.(^var2 < ^var1)==>^(subst [(var2,var)] prop)" in
let x and_then f = f x in
([(hypoth,(subst [("0",var)] prop));(assum.hypoth,prop1)],
(\[thm1;thm2].(GEN_INDUCT_RULE thm1 (GEN var1 (DISCH assum thm2)))and_then
(\thm.(EQ_MP (ALPHA (concl thm) aim) thm)) ))
)?failwith `GEN_INDUCT_TAC`;;
|
