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