1%  MICROCODED COMPUTER PROOF : HOL                                      %
2%                                                                       %
3%  'next.ml'                                                            %
4%                                                                       %
5%  Description                                                          % 
6%                                                                       %
7%     This theory defines the 'NEXT' relation which relates a time      %
8%  't2' to a earlier time 't1' as the next time the signal 'sig' is     %
9%  is true after t1.                                                    %
10%     The definition of NEXT and NEXT_INC_INTERVAL_LEMMA are taken      %
11%  from Tom Melham's FACTORIAL example (slightly modified).             %
12%                                                                       %
13%  Author:  Jeff Joyce                                                  %
14%  Date:    August 4, 1985                                              %
15
16new_theory `next`;;
17
18let NEXT = new_definition
19(
20 `NEXT`, 
21  "NEXT (t1,t2) sig =
22   (t1 < t2) /\ (sig t2)  /\ (!t. (t1 < t) /\ (t < t2) ==> ~sig t)"
23);;
24
25% Some preliminary lemmas %
26
27let A_AND_NOT_A_LEMMA =
28 TAC_PROOF
29 (
30  ([],"!t:bool. (t /\ ~t) = F"),
31  GEN_TAC THEN (ASM_CASES_TAC "t:bool") THEN (ASM_REWRITE_TAC [])
32 );;
33
34let NOT_EQ_LEMMA =
35 let lemma =
36 (
37  MP
38   (SPEC_ALL LESS_CASES_IMP)
39   (LIST_CONJ [(ASSUME "~(m < n)");(ASSUME "~(m = n)")])
40 ) in
41 TAC_PROOF
42 (
43  ([],"!m:num. !n:num. ~(m = n) ==> ((m < n) \/ (n < m))"),
44  (REPEAT GEN_TAC) THEN
45  (ASM_CASES_TAC "(m < n):bool") THENL
46  [
47   (STRIP_TAC THEN DISJ1_TAC THEN (ASM_REWRITE_TAC []));
48   (STRIP_TAC THEN DISJ2_TAC THEN (ASM_REWRITE_TAC [lemma]))
49  ]
50 );;
51
52%  NEXT (t1,t2) sig is true when t2 = (t1 + 1) and sig is true at t2.   %
53%                                                                       %
54%        |- !sig t1. sig(t1 + 1) ==> NEXT(t1,t1 + 1)sig                 %
55
56let NEXT_INC_LEMMA =
57 save_thm
58 (
59  `NEXT_INC_LEMMA`,
60   TAC_PROOF
61   (
62    ([],"!sig:num->bool. !t1:num. (sig (t1 + 1) ==> NEXT (t1,(t1 + 1)) sig)"),
63    (REPEAT GEN_TAC) THEN
64    STRIP_TAC THEN
65    (PURE_REWRITE_TAC [NEXT]) THEN
66    CONJ_TAC THENL
67    [
68     (PURE_REWRITE_TAC [PURE_REWRITE_RULE [ADD1] LESS_SUC_REFL]);
69     (
70      CONJ_TAC THENL
71      [
72       (ASM_REWRITE_TAC []);
73       (
74        GEN_TAC THEN
75        (REWRITE_TAC
76         [SPECL ["t1:num";"t:num"] (PURE_REWRITE_RULE [ADD1] LESS_LESS_SUC)])
77       )
78      ]
79     )
80    ]));;
81
82%  There is a unique time when sig is next true.                        %
83%                                                                       %
84%  |- !sig t1 t2 t2'. NEXT(t1,t2)sig /\ NEXT(t1,t2')sig ==> (t2 = t2')  %
85
86let NEXT_IDENTITY_LEMMA =
87 save_thm
88 (
89  `NEXT_IDENTITY_LEMMA`,
90   let asm =
91    PURE_REWRITE_RULE [NEXT]
92      (ASSUME "NEXT (t1,t2) sig /\ NEXT (t1,t2') sig") in
93   GENL ["sig";"t1"]
94    (GENL ["t2";"t2'"]
95     (DISCH_ALL
96      (CCONTR "(t2 = t2')"
97       (DISJ_CASES
98        (MP (SPECL ["t2:num";"t2':num"] NOT_EQ_LEMMA) (ASSUME "~(t2 = t2')"))
99         (
100          SUBS
101           [SPEC "(sig t2):bool" A_AND_NOT_A_LEMMA]
102           (LIST_CONJ
103            [
104             (CONJUNCT1 (CONJUNCT2 (CONJUNCT1 asm)));
105             (MP
106              (SPEC "t2:num" (CONJUNCT2 (CONJUNCT2 (CONJUNCT2 asm))))
107              (LIST_CONJ [CONJUNCT1 (CONJUNCT1 asm);(ASSUME "t2 < t2'")])
108             )
109            ]
110           )
111         )
112         (
113          SUBS
114           [SPEC "(sig t2'):bool" A_AND_NOT_A_LEMMA]
115           (LIST_CONJ
116            [
117             (CONJUNCT1 (CONJUNCT2 (CONJUNCT2 asm)));
118             (MP
119              (SPEC "t2':num" (CONJUNCT2 (CONJUNCT2 (CONJUNCT1 asm))))
120              (LIST_CONJ [CONJUNCT1 (CONJUNCT2 asm);(ASSUME "t2' < t2")])
121             )
122            ]
123           )
124          ))))));;
125
126%  Lemma for increasing the interval covered by NEXT.                   %
127%                                                                       %
128%  |- !sig t1 t2. ~sig(t1 + 1) /\ NEXT(t1 + 1,t2)sig ==> NEXT(t1,t2)sig %
129
130let NEXT_INC_INTERVAL_LEMMA =
131 save_thm
132 (
133  `NEXT_INC_INTERVAL_LEMMA`,
134   TAC_PROOF
135   (
136    (
137     [],
138     "!sig t1 t2.
139     ~(sig (t1 + 1)) /\ NEXT ((t1 + 1),t2) sig ==> NEXT (t1,t2) sig"
140    ),
141    (REWRITE_TAC [NEXT]) THEN
142    (REPEAT STRIP_TAC) THEN
143    (IMP_RES_TAC
144     (REWRITE_RULE [LESS_OR_EQ] (PURE_REWRITE_RULE [ADD1] OR_LESS))) THEN
145    (ASM_REWRITE_TAC []) THEN
146    (DISJ_CASES_TAC
147     (REWRITE_RULE [LESS_OR_EQ]
148      (UNDISCH
149       (SPECL ["t1";"t"]
150        (PURE_REWRITE_RULE [ADD1] LESS_SUC_EQ))))) THEN
151    (IMP_RES_TAC
152     (DISCH_ALL
153      (SUBS [SYM (ASSUME "(t1 + 1) = t")]
154       (ASSUME "sig t:bool")))) THEN
155    RES_TAC
156   )
157 );;
158
159close_theory ();;
160