1% PROOF : Transistor Implementation of a Counter % 2% FILE : dataabs.ml % 3% % 4% DESCRIPTION : Defines data abstractions from the four-valued % 5% logic to boolean logic for single bits and for % 6% arbitrary sized words and from words to numbers. % 7% % 8% Hilbert's choice operator "@" is used to simulate % 9% the partial mapping of values in the four-valued % 10% logic to booleans. The predicates Def and Defn % 11% determine when the abstraction is valid. Alternate % 12% ways of abstracting to boolean logic would include % 13% the use of relations or else mapping instead to a % 14% three-valued logic consisting of T,F and bottom. % 15% % 16% The Def predicate is taken from Inder Dhingra's % 17% paper, "Formal Validation of an Integrated Circuit % 18% Design Style", Hardware Verification Workshop, % 19% University of Calgary, January 1987. % 20% % 21% AUTHOR : J.Joyce % 22% DATE : 31 March 1987 % 23 24new_theory `dataabs`;; 25 26loadt `misc`;; 27loadt `types`;; 28 29new_parent `mos`;; 30 31let Def = new_definition ( 32 `Def`, 33 "Def (v:^val) = (v = Lo) \/ (v = Hi)");; 34 35let Defn = new_prim_rec_definition ( 36 `Defn`, 37 "(Defn 0 (v:^vec) = Def (v 0)) /\ 38 (Defn (SUC n) (v:^vec) = Def (v (SUC n)) /\ Defn n v)");; 39 40let BoolAbs = new_definition ( 41 `BoolAbs`, 42 "BoolAbs (v:^val) = 43 @b. ((v = Lo) /\ (b = F)) \/ ((v = Hi) /\ (b = T))");; 44 45let WordAbs = new_definition ( 46 `WordAbs`, 47 "WordAbs (v:^vec) = \p. BoolAbs (v p)");; 48 49let BoolVal = new_definition ( 50 `BoolVal`, 51 "BoolVal (b:bool) = (b => 1 | 0)");; 52 53let WordVal = new_prim_rec_definition ( 54 `WordVal`, 55 "(WordVal 0 (w:^word) = BoolVal (w 0)) /\ 56 (WordVal (SUC n) (w:^word) = 57 ((2 EXP (SUC n)) * (BoolVal (w (SUC n)))) + (WordVal n w))");; 58 59let isBus = new_definition ( 60 `isBus`, 61 "isBus n (b:^bus) = !m. n < m ==> !t. b t m = Er");; 62 63let DEST_BUS = new_definition ( 64 `DEST_BUS`, 65 "DEST_BUS (b:^bus) = \p. \t. b t p");; 66 67let After = new_definition (`After`,"After t c = !t'. t <= t' ==> c t'");; 68 69let val_not_eq_ax = axiom `mos` `val_not_eq_ax`;; 70 71let CHOOSE_TRUE = SELECT_RULE (EXISTS ("?b.b","T") TRUTH);; 72 73let NOT_CHOOSE_FALSE = 74 SELECT_RULE 75 (EXISTS ("?b.~b","F") 76 (SUBS [SYM (CONJUNCT2 (CONJUNCT2 NOT_CLAUSES))] TRUTH));; 77 78let Def_DISJ_CASES = save_thm ( 79 `Def_DISJ_CASES`, 80 GEN_ALL (fst (EQ_IMP_RULE Def)));; 81 82let BoolAbs_THM = prove_thm ( 83 `BoolAbs_THM`, 84 "(BoolAbs Hi = T) /\ (BoolAbs Lo = F)", 85 REWRITE_TAC [BoolAbs;val_not_eq_ax;CHOOSE_TRUE;NOT_CHOOSE_FALSE]);; 86 87let isBus_THM = prove_thm ( 88 `isBus_THM`, 89 "!n b1 b2. 90 isBus n b1 /\ 91 isBus n b2 92 ==> 93 !t1 t2. (b1 t1 = b2 t2) = (!m. m <= n ==> (b1 t1 m = b2 t2 m))", 94 let thm = INST_TYPE [":^posn",":*";":^val",":**"] EQ_EXT 95 in 96 PURE_REWRITE_TAC [isBus] THEN 97 BETA_TAC THEN 98 REPEAT STRIP_TAC THEN 99 EQ_TAC THENL 100 [STRIP_TAC THEN ASM_REWRITE_TAC []; 101 REPEAT STRIP_TAC THEN 102 (\g. IMP_TAC (SPECL [lhs (snd g);rhs (snd g)] thm) g) THEN 103 GEN_TAC THEN 104 DISJ_CASES_TAC (SPECL ["n:num";"x:num"] LESS_CASES) THEN 105 RES_TAC THEN 106 ASM_REWRITE_TAC []]);; 107 108close_theory ();; 109