blob: a53baa4023c1ce930c64a3ab0d398c8b86a2bd6b (
plain)
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
|
#use "hol.ml";;
needs "Examples/prime.ml";;
#use "TacticRecording/main.ml";;
let egcd = define
`egcd(m,n) = if m = 0 then n
else if n = 0 then m
else if m <= n then egcd(m,n - m)
else egcd(m - n,n)`;;
let egcd = theorem_wrap "egcd" egcd;;
let DIVIDES_0 = theorem_wrap "DIVIDES_0" DIVIDES_0;;
let WF_INDUCT_TAC = term_tactic_wrap "WF_INDUCT_TAC" WF_INDUCT_TAC;;
g `!m n d. d divides egcd(m,n) <=> d divides m /\ d divides n`;;
e (GEN_TAC THEN GEN_TAC THEN WF_INDUCT_TAC `m + n` THEN
GEN_TAC THEN ONCE_REWRITE_TAC[egcd] THEN
ASM_CASES_TAC `m = 0` THEN ASM_REWRITE_TAC[DIVIDES_0] THEN
ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[DIVIDES_0] THEN
COND_CASES_TAC);;
top_goal ();;
print_executed_proof ();;
print_flat_proof ();;
print_thenl_proof ();;
print_optimal_proof ();;
is_empty [23];;
not true or not true;;
let EGCD_INVARIANT = prove
(`!m n d. d divides egcd(m,n) <=> d divides m /\ d divides n`,
GEN_TAC THEN GEN_TAC THEN WF_INDUCT_TAC `m + n` THEN
GEN_TAC THEN ONCE_REWRITE_TAC[egcd] THEN
ASM_CASES_TAC `m = 0` THEN ASM_REWRITE_TAC[DIVIDES_0] THEN
ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[DIVIDES_0] THEN
COND_CASES_TAC THEN
(W(fun (asl,w) -> FIRST_X_ASSUM(fun th ->
MP_TAC(PART_MATCH (lhs o snd o dest_forall o rand) th (lhand w)))) THEN
ANTS_TAC THENL [REPEAT(POP_ASSUM MP_TAC) THEN ARITH_TAC; ALL_TAC]) THEN
ASM_MESON_TAC[DIVIDES_SUB; DIVIDES_ADD; SUB_ADD; LE_CASES]);;
|
