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