/usr/share/hol88-2.02.19940316/contrib/CSP/restrict.ml is in hol88-contrib-source 2.02.19940316-14.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
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 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 | % Extends The Basic Theory For TRACES In CSP %
% %
% FILE : restrict.ml %
% DESCRIPTION : Defines the restriction operator and proves some of %
% its properties. Restriction is defined over finite %
% traces and infinite alphabets. %
% %
% LOADS LIBRARY : sets %
% READS FILES : traces.th, boolarith2.th %
% WRITES FILES : restrict.th %
% %
% AUTHOR : Albert J Camilleri %
% AFFILIATION : Hewlett-Packard Laboratories, Bristol %
% DATE : 89.02.06 %
% REVISED : 91.10.01 %
new_theory `restrict`;;
load_library `sets`;;
map new_parent [`traces`; `boolarith2`];;
map (load_theorem `boolarith2`) [`INV_SUC_LEQ`; `LESS_EQ_0_N`];;
load_theorem `boolarith1` `NOT_EQ_LEQ`;;
load_theorem `list_lib1` `NOT_LENGTH_EQ`;;
let RESTRICT =
new_list_rec_definition
(`RESTRICT`,
"(RESTRICT [] (A:(*)set) = []) /\
(RESTRICT (CONS (x:*) t) (A:(*)set) =
(x IN A) => (CONS x (RESTRICT t A)) | (RESTRICT t A))");;
let STRICT_REST =
prove_thm
(`STRICT_REST`,
"! A:(*)set. RESTRICT [] A = []",
REWRITE_TAC [CONJUNCT1 RESTRICT]);;
let DISTRIB_REST =
prove_thm
(`DISTRIB_REST`,
"! s t (A:(*)set).
RESTRICT (APPEND s t) A = (APPEND (RESTRICT s A) (RESTRICT t A))",
LIST_INDUCT_TAC THEN
REWRITE_TAC [APPEND; RESTRICT] THEN
REPEAT STRIP_TAC THEN
DISJ_CASES_TAC (SPEC "(h:*) IN (A:(*)set)" EXCLUDED_MIDDLE) THEN
ASM_REWRITE_TAC[APPEND]);;
let RESTR_EMPTY =
prove_thm
(`RESTR_EMPTY`,
"! s:* list. RESTRICT s {} = []",
LIST_INDUCT_TAC THEN
ASM_REWRITE_TAC [RESTRICT; NOT_IN_EMPTY]);;
let REP_RESTR =
prove_thm
(`REP_RESTR`,
"! s (A B:(*)set).
(RESTRICT (RESTRICT s A) B) = (RESTRICT s (A INTER B))",
LIST_INDUCT_TAC THEN
REWRITE_TAC [RESTRICT] THEN
REPEAT GEN_TAC THEN
DISJ_CASES_TAC (SPEC "(h:*) IN (A:(*)set)" EXCLUDED_MIDDLE) THEN
ASM_REWRITE_TAC [RESTRICT] THEN
DISJ_CASES_TAC (SPEC "(h:*) IN (B:(*)set)" EXCLUDED_MIDDLE) THEN
ASM_REWRITE_TAC[IN_INTER]);;
let LEQ_ID =
GEN_ALL
(REWRITE_RULE [SYM (SPEC_ALL ADD1)] (SPECL ["m:num";"1"] LESS_EQ_ADD));;
let MAX_LEN_REST =
prove_thm
(`MAX_LEN_REST`,
"! (A:(*)set) s. LENGTH (RESTRICT s A) <= LENGTH s",
GEN_TAC THEN
LIST_INDUCT_TAC THENL
[REWRITE_TAC [RESTRICT;LENGTH;LESS_EQ_0_N];
GEN_TAC THEN
DISJ_CASES_TAC (SPEC "(h:*) IN (A:(*)set)" EXCLUDED_MIDDLE) THEN
ASM_REWRITE_TAC[RESTRICT;LENGTH;INV_SUC_LEQ] THEN
ASSUME_TAC (SPEC "LENGTH (s:* list)" LEQ_ID) THEN
IMP_RES_TAC LESS_EQ_TRANS THEN
ASM_REWRITE_TAC []]);;
let REST_LEMMA =
prove_thm
(`REST_LEMMA`,
"!(A:(*)set) (s:(*)list) a.
~((LENGTH (RESTRICT s A)) = (LENGTH (CONS a s)))",
REWRITE_TAC
[NOT_EQ_LEQ;
LENGTH;
REWRITE_RULE
[GEN_ALL (SYM (SPEC_ALL (LESS_OR_EQ)))]
(ONCE_REWRITE_RULE [DISJ_SYM] LESS_THM);
MAX_LEN_REST]);;
let REST_CONS_THM =
save_thm
(`REST_CONS_THM`,
GEN_ALL
(MP (SPECL ["CONS a (s:* list)"; "RESTRICT s (A:(*)set)"]
NOT_LENGTH_EQ)
(SPEC_ALL REST_LEMMA)));;
close_theory();;
|