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
71
72
73
74
75
76
77
78
79
80
81
82
83
|
% ===================================================================== %
% FILE : rtc.ml %
% DESCRIPTION : reflexitive-transitive closure of a relation. %
% %
% AUTHOR : T. Melham %
% DATE : 90.04.29 %
% ===================================================================== %
% --------------------------------------------------------------------- %
% Create the new theory. %
% --------------------------------------------------------------------- %
new_theory `rtc`;;
% --------------------------------------------------------------------- %
% Load the inductive definitions package %
% --------------------------------------------------------------------- %
load_library `ind_defs`;;
% --------------------------------------------------------------------- %
% Inductive definition the reflexive-transitive closure of a relation. %
% --------------------------------------------------------------------- %
let (rules,ind) =
let RTC = "RTC:(*->*->bool)->*->*->bool" in
new_inductive_definition false `RTC_DEF`
("^RTC R x y", ["R:*->*->bool"])
[ [
% ------------------------------ % "R (x:*) (y:*):bool"],
"^RTC R x y" ;
[
%------------------------------- % ],
"^RTC R x x" ;
[ "^RTC R x z"; "^RTC R z y"
%------------------------------- % ],
"^RTC R x y" ];;
% --------------------------------------------------------------------- %
% Tactics for RTC proofs. %
% --------------------------------------------------------------------- %
let [IN_TAC;REFL_TAC;TRANS_TAC] = map RULE_TAC rules;;
% --------------------------------------------------------------------- %
% Strong form of rule induction. %
% --------------------------------------------------------------------- %
let sind = derive_strong_induction_thm (rules,ind);;
% --------------------------------------------------------------------- %
% Cases theorem for RTC. %
% --------------------------------------------------------------------- %
let cases = derive_cases_thm (rules,ind);;
% --------------------------------------------------------------------- %
% Rule induction tactic for RTC. %
% --------------------------------------------------------------------- %
let RTC_INDUCT_TAC = RULE_INDUCT_THEN ind STRIP_ASSUME_TAC STRIP_ASSUME_TAC;;
% --------------------------------------------------------------------- %
% Prove that taking the reflexive-transitive closure preserves symmetry %
% --------------------------------------------------------------------- %
let RTC_PRESERVES_SYMMETRY =
prove_thm
(`RTC_PRESERVES_SYMMETRY`,
"!R. (!a (b:*). R a b ==> R b a) ==>
(!a b. RTC R a b ==> RTC R b a)",
GEN_TAC THEN DISCH_TAC THEN
RTC_INDUCT_TAC THENL
[IN_TAC THEN RES_TAC;
REFL_TAC;
TRANS_TAC THEN EXISTS_TAC "z:*" THEN
CONJ_TAC THEN FIRST_ASSUM ACCEPT_TAC]);;
|
