1% PROOF : Transistor Implementation of a Counter % 2% FILE : tempabs.ml % 3% % 4% DESCRIPTION : Defines the predicates `Next`, `Inf`, `IsTimeOf` % 5% and `TimeOf` and derives several major theorems % 6% which provide a basis for temporal abstraction. % 7% % 8% These predicates and theorems are taken from % 9% T.Melham's paper, "Abstraction Mechanisms for % 10% Hardware Verification", Hardware Verification % 11% Workshop, University of Calgary, January 1987. % 12% % 13% AUTHOR : J.Joyce % 14% DATE : 31 March 1987 % 15 16new_theory `tempabs`;; 17 18new_parent `wop`;; 19 20let Next = new_definition ( 21 `Next`, 22 "Next (t1,t2) g = 23 (t1 < t2) /\ (g t2) /\ (!t. (t1 < t) /\ (t < t2) ==> ~g t)");; 24 25let Inf = new_definition ( 26 `Inf`, 27 "Inf g = !t.?t'. t'>t /\ (g t')");; 28 29let IsTimeOf = new_prim_rec_definition ( 30 `IsTimeOf`, 31 "(IsTimeOf 0 g t = g (t) /\ !t'. t' < t ==> ~g (t')) /\ 32 (IsTimeOf (SUC n) g t = 33 g (t) /\ 34 ?t'. 35 t' < t /\ 36 IsTimeOf n g t' /\ 37 (!t''. ((t' < t'') /\ (t'' < t)) ==> ~g (t'')))");; 38 39let TimeOf = new_definition ( 40 `TimeOf`, 41 "TimeOf g n = @t. IsTimeOf n g t");; 42 43let when = new_infix_definition ( 44 `when`, 45 "when (s1:num->*) (s2:num->bool) = (\n. s1 (TimeOf s2 n))");; 46 47let WOP = theorem `wop` `WOP`;; 48 49let BETA_RULE = CONV_RULE (DEPTH_CONV BETA_CONV);; 50 51let Next_ADD1 = prove_thm ( 52 `Next_ADD1`, 53 "!s t. (s (t + 1) ==> Next (t,t + 1) s)", 54 PURE_REWRITE_TAC [Next;SYM (SPEC "t" ADD1)] THEN 55 REPEAT STRIP_TAC THENL 56 [REWRITE_TAC [LESS_SUC_REFL]; 57 FIRST_ASSUM ACCEPT_TAC; 58 IMP_RES_TAC LESS_NOT_EQ THEN 59 ASSUME_TAC (NOT_EQ_SYM (ASSUME "~(t = t')")) THEN 60 IMP_RES_TAC LESS_SUC_IMP THEN 61 IMP_RES_TAC LESS_ANTISYM]);; 62 63let Next_INCREASE = prove_thm ( 64 `Next_INCREASE`, 65 "!s t1 t2. 66 (~(s (t1 + 1)) /\ Next (t1 + 1,t2) s) ==> Next (t1,t2) s", 67 PURE_REWRITE_TAC [Next;SYM (SPEC "t" ADD1)] THEN 68 REPEAT STRIP_TAC THENL 69 [IMP_RES_TAC SUC_LESS; 70 FIRST_ASSUM ACCEPT_TAC; 71 IMP_RES_TAC LESS_SUC_EQ THEN 72 DISJ_CASES_TAC 73 (PURE_REWRITE_RULE [LESS_OR_EQ] (ASSUME "(SUC t1) <= t")) THENL 74 [RES_TAC; 75 ASSUME_TAC (SUBS [ASSUME "SUC t1 = t"] (ASSUME "~s(SUC t1)")) THEN 76 RES_TAC]]);; 77 78let Next_IDENTITY = prove_thm ( 79 `Next_IDENTITY`, 80 "!s t1 t2 t3. 81 (Next (t1,t2) s /\ Next (t1,t3) s) ==> (t2 = t3)", 82 PURE_REWRITE_TAC [Next] THEN 83 REPEAT STRIP_TAC THEN 84 DISJ_CASES_TAC (SPEC "t2 = t3" EXCLUDED_MIDDLE) THENL 85 [FIRST_ASSUM ACCEPT_TAC; 86 DISJ_CASES_TAC (SPEC "t2 < t3" EXCLUDED_MIDDLE) THENL 87 [RES_TAC;IMP_RES_TAC LESS_CASES_IMP THEN RES_TAC]]);; 88 89% lemma1 = . |- ?n. g n /\ (!m. m < n ==> ~g m) % 90let th1 = SPEC "t" (PURE_REWRITE_RULE [Inf] (ASSUME "Inf g"));; 91let th2 = ASSUME (snd (dest_exists (concl th1)));; 92let th3 = CONJUNCT2 th2;; 93let th4 = EXISTS (mk_exists ("t'",concl th3),"t'") th3;; 94let th5 = CHOOSE ("t'",th1) th4;; 95let lemma1 = MATCH_MP WOP th5;; 96 97let lemma2 = TAC_PROOF ( 98 ([],"(a ==> ~(b /\ c)) = ((b /\ a) ==> ~c)"), 99 REWRITE_TAC [DE_MORGAN_THM;SYM (SPEC_ALL IMP_DISJ_THM)] THEN 100 EQ_TAC THEN (REPEAT STRIP_TAC) THEN RES_TAC);; 101 102% 103lemma3 = 104.. |- ?t'. 105 g t' /\ 106 (?t. t < t' /\ IsTimeOf n g t /\ (!m. t < m /\ m < t' ==> ~g m)) 107% 108let th1 = ASSUME "?t. IsTimeOf n g t";; 109let th2 = ASSUME (snd (dest_exists (concl th1)));; 110let th3 = SPEC "t" (PURE_REWRITE_RULE [Inf] (ASSUME "Inf g"));; 111let th4 = ASSUME (snd (dest_exists (concl th3)));; 112let th5 = BETA_CONV (mk_comb (mk_abs ("t'",concl th4),"t'"));; 113let th6 = EQ_MP (SYM th5) th4;; 114let th7 = EXISTS (mk_exists ("t'",concl th6),"t'") th6;; 115let th8 = CHOOSE ("t'",th3) th7;; 116let th9 = BETA_RULE (MATCH_MP WOP th8);; 117let th10 = EQ_MP (GEN_ALPHA_CONV "t'" (concl th9)) th9;; 118let th11 = PURE_REWRITE_RULE [GREATER;lemma2] th10;; 119let th12 = ASSUME (snd (dest_exists (concl th11)));; 120let th13 = CONJUNCT1 (CONJUNCT1 th12);; 121let th14 = CONJUNCT2 (CONJUNCT1 th12);; 122let th15 = CONJUNCT2 th12;; 123let th16 = LIST_CONJ [th13;th2;th15];; 124let th17 = EXISTS (mk_exists ("t",concl th16),"t") th16;; 125let th18 = LIST_CONJ [th14;th17];; 126let th19 = EXISTS (mk_exists ("t'",concl th18),"t'") th18;; 127let th20 = CHOOSE ("t'",th11) th19;; 128let lemma3 = CHOOSE ("t",th1) th20;; 129 130let IsTimeOf_EXISTS = prove_thm ( 131 `IsTimeOf_EXISTS`, 132 "!g. Inf g ==> !n. ?t. IsTimeOf n g t", 133 GEN_TAC THEN DISCH_TAC THEN INDUCT_TAC THENL 134 [REWRITE_TAC [IsTimeOf;lemma1];REWRITE_TAC [IsTimeOf;lemma3]]);; 135 136let TimeOf_DEFINED = prove_thm ( 137 `TimeOf_DEFINED`, 138 "!g. Inf g ==> !n. IsTimeOf n g (TimeOf g n)", 139 REPEAT STRIP_TAC THEN 140 IMP_RES_TAC IsTimeOf_EXISTS THEN 141 ACCEPT_TAC 142 (PURE_REWRITE_RULE [SYM TimeOf] 143 (SELECT_RULE (SPEC "n" (ASSUME "!n. ?t. IsTimeOf n g t")))));; 144 145let TimeOf_TRUE = prove_thm ( 146 `TimeOf_TRUE`, 147 "!g. Inf g ==> !n. g (TimeOf g n)", 148 REPEAT STRIP_TAC THEN 149 IMP_RES_TAC TimeOf_DEFINED THEN 150 DISJ_CASES_TAC (SPEC "n" num_CASES) THENL 151 [SUBST1_TAC (ASSUME "n = 0") THEN 152 STRIP_ASSUME_TAC 153 (PURE_REWRITE_RULE [IsTimeOf] 154 (SPEC "0" (ASSUME "!n. IsTimeOf n g (TimeOf g n)"))); 155 FIRST_ASSUM 156 (\thm. 157 if is_exists (concl thm) 158 then (CHOOSE_THEN SUBST1_TAC thm) else NO_TAC) THEN 159 STRIP_ASSUME_TAC 160 (PURE_REWRITE_RULE [IsTimeOf] 161 (SPEC "SUC n'" (ASSUME "!n. IsTimeOf n g (TimeOf g n)")))]);; 162 163let tm = "!t''. t' < t'' /\ t'' < t1 ==> ~g t''";; 164 165let IsTimeOf_IDENTITY = prove_thm ( 166 `IsTimeOf_IDENTITY`, 167 "!g n t1 t2. IsTimeOf n g t1 /\ IsTimeOf n g t2 ==> (t1 = t2)", 168 GEN_TAC THEN 169 INDUCT_TAC THENL 170 [PURE_REWRITE_TAC [IsTimeOf] THEN 171 REPEAT STRIP_TAC THEN 172 DISJ_CASES_TAC (SPECL ["t1";"t2"] LESS_CASES) THENL 173 [RES_TAC; 174 DISJ_CASES_TAC 175 (PURE_REWRITE_RULE [LESS_OR_EQ] (ASSUME "t2 <= t1")) THENL 176 [RES_TAC;ACCEPT_TAC (SYM (ASSUME "t2 = t1"))]]; 177 PURE_REWRITE_TAC [IsTimeOf] THEN 178 REPEAT STRIP_TAC THEN 179 RES_TAC THEN 180 ASSUME_TAC 181 (SUBS [ASSUME "t'' = t'"] 182 (ASSUME "!t'''. t'' < t''' /\ t''' < t2 ==> ~g t'''")) THEN 183 ASSUME_TAC 184 (SUBS [ASSUME "t' = t''"] 185 (EQ_MP (GEN_ALPHA_CONV "t''':num" tm) (ASSUME tm))) THEN 186 DISJ_CASES_TAC (SPECL ["t1";"t2"] LESS_CASES) THENL 187 [RES_TAC; 188 DISJ_CASES_TAC 189 (PURE_REWRITE_RULE [LESS_OR_EQ] (ASSUME "t2 <= t1")) THENL 190 [RES_TAC; 191 ASSUME_TAC (SYM (ASSUME "t2 = t1")) THEN 192 RES_TAC THEN 193 ACCEPT_TAC (SYM (ASSUME "t2 = t1"))]]]);; 194 195% 196TimeOf_INCREASING = 197|- !g. Inf g ==> (!n. (TimeOf g n) < (TimeOf g(n + 1))) 198% 199let th1 = 200 PURE_REWRITE_RULE [IsTimeOf] 201 (SPEC "SUC n" (UNDISCH (SPEC "g" TimeOf_DEFINED)));; 202let th2 = CONJUNCT2 th1;; 203let th3 = ASSUME (snd (dest_exists (concl th2)));; 204let th4 = CONJUNCT1 th3;; 205let th5 = CONJUNCT1 (CONJUNCT2 th3);; 206let th6 = SPEC "n" (UNDISCH (SPEC "g" TimeOf_DEFINED));; 207let th7 = MATCH_MP IsTimeOf_IDENTITY (LIST_CONJ [th5;th6]);; 208let th8 = SUBS [th7] th4;; 209let th9 = CHOOSE ("t'",th2) th8;; 210let th10 = GEN "g" (DISCH_ALL (GEN "n" th9));; 211let th11 = PURE_REWRITE_RULE [ADD1] th10;; 212let TimeOf_INCREASING = save_thm (`TimeOf_INCREASING`,th11);; 213 214% 215TimeOf_INTERVAL = 216|- !g. 217 Inf g ==> (!n t. (TimeOf g n) < t /\ t < (TimeOf g(n + 1)) ==> ~g t) 218% 219let th1 = 220 PURE_REWRITE_RULE [IsTimeOf] 221 (SPEC "SUC n" (UNDISCH (SPEC "g" TimeOf_DEFINED)));; 222let th2 = CONJUNCT2 th1;; 223let th3 = ASSUME (snd (dest_exists (concl th2)));; 224let th4 = CONJUNCT2 (CONJUNCT2 th3);; 225let th5 = CONJUNCT1 (CONJUNCT2 th3);; 226let th6 = SPEC "n" (UNDISCH (SPEC "g" TimeOf_DEFINED));; 227let th7 = MATCH_MP IsTimeOf_IDENTITY (LIST_CONJ [th5;th6]);; 228let th8 = SUBS [th7] th4;; 229let th9 = EQ_MP (GEN_ALPHA_CONV "t" (concl th8)) th8;; 230let th10 = CHOOSE ("t'",th2) th9;; 231let th11 = GEN "g" (DISCH_ALL (GEN "n" th10));; 232let th12 = PURE_REWRITE_RULE [ADD1] th11;; 233let TimeOf_INTERVAL = save_thm (`TimeOf_Interval`,th12);; 234 235let TimeOf_Next = prove_thm ( 236 `TimeOf_Next`, 237 "!g. Inf g ==> Next (TimeOf g n,TimeOf g (n+1)) g", 238 PURE_REWRITE_TAC [Next] THEN 239 REPEAT STRIP_TAC THEN 240 IMP_RES_THEN (\thm. REWRITE_TAC [thm]) TimeOf_INCREASING THEN 241 IMP_RES_THEN (\thm. REWRITE_TAC [thm]) TimeOf_TRUE THEN 242 IMP_RES_THEN (\thm. REWRITE_TAC [thm]) TimeOf_INTERVAL);; 243 244close_theory ();; 245