1% PROOF		: Transistor Implementation of a Counter		%
2% FILE		: toplevel.ml						%
3%									%
4% DESCRIPTION	: Top-level implementation using the counter and	%
5%		  some I/0 devices.					%
6%									%
7% AUTHOR	: J.Joyce						%
8% DATE		: 1 April 1987						%
9
10new_theory `toplevel`;;
11
12loadt `misc`;;
13loadt `types`;;
14
15new_parent `count`;;
16
17let BUTTON = new_definition (
18	`BUTTON`,
19	"BUTTON (g:^wire,i:^boolsig,o:^wire) =
20	  (!t. Def ((o when (isHi g)) t)) /\
21	  (!t. (i t = BoolAbs ((o when (isHi g)) t)))");;
22
23let SWITCHES = new_definition (
24	`SWITCHES`,
25	"SWITCHES n (g:^wire,i:^numsig,o:^bus) =
26	  (!t. Defn n ((o when (isHi g)) t)) /\
27	  (!t. (i t = WordVal n (WordAbs ((o when (isHi g)) t))))");;
28
29let DISPLAY = new_definition (
30	`DISPLAY`,
31	"DISPLAY n (g:^wire,i:^bus,o:^numsig) =
32	  !t.
33	    Defn n ((i when (isHi g)) t) ==>
34	    (o t = WordVal n (WordAbs ((i when (isHi g)) t)))");;
35
36let DEVICE_IMP = new_definition (
37	`DEVICE_IMP`,
38	"DEVICE_IMP n (button:^boolsig,switches:^numsig,display:^numsig) =
39	  ?phiA w1 b1 b2.
40	    BUTTON (phiA,button,w1) /\
41	    SWITCHES n (phiA,switches,b1) /\
42	    DISPLAY n (phiA,b2,display) /\
43	    COUNT_IMP n (phiA,w1,b1,b2) /\
44	    isBus n b1 /\
45	    isBus n b2");;
46
47let Def_DISJ_CASES = theorem `dataabs` `Def_DISJ_CASES`;;
48let BoolAbs_THM = theorem `dataabs` `BoolAbs_THM`;;
49let COUNT_CORRECT = theorem `count` `COUNT_CORRECT2`;;
50
51let LESS_OR_EQ_ADD = TAC_PROOF(
52	([],"!m n. m <= n = (?p. p + m = n)"),
53	REPEAT GEN_TAC THEN
54	EQ_TAC THENL
55	[PURE_REWRITE_TAC [LESS_OR_EQ] THEN
56	 REPEAT STRIP_TAC THENL
57	 [IMP_RES_TAC LESS_ADD;
58	  EXISTS_TAC "0" THEN ASM_REWRITE_TAC [ADD_CLAUSES]];
59	 REPEAT STRIP_TAC THEN
60	 FIRST_ASSUM (SUBST1_TAC o SYM) THEN
61	 SUBST1_TAC (SPECL ["p";"m"] ADD_SYM) THEN
62	 REWRITE_TAC [LESS_EQ_ADD]]);;
63
64let ASSUM_LIST_SPEC_TAC tm =
65	ASSUM_LIST (MAP_EVERY
66	    (\thm.
67	      if not (is_forall (concl thm)) then ALL_TAC
68	      else let var = fst (dest_forall (concl thm)) in
69	      if not (type_of tm = type_of var) then ALL_TAC
70	      else ASSUME_TAC (SPEC tm thm) ?
71	      failwith `ASSUM_LIST_SPEC_TAC`));;
72
73let lemma1 = TAC_PROOF ((
74	[],
75	"!w t.
76	  Def (w t) ==> (b t = BoolAbs (w t)) ==> (b t = T) ==> (w t = Hi)"),
77	REPEAT GEN_TAC THEN
78	DISCH_THEN (STRIP_THM_THEN SUBST1_TAC o(MATCH_MP Def_DISJ_CASES)) THEN
79	DISCH_THEN SUBST1_TAC THEN REWRITE_TAC [BoolAbs_THM]);;
80
81let lemma2 =
82	GEN_ALL
83	  (SUBS [SPECL ["m";"n"] ADD_SYM] (SPECL ["m";"n"] LESS_EQ_ADD));;
84
85let th1 = CONJUNCT1 (CONJUNCT2 (CONJUNCT2 ADD_CLAUSES));;
86let th2 = (DEPTH_CONV (REWRITE_CONV th1)) "((SUC n') + sysinit)";;
87let th3 = SYM (TRANS th2 ((REWRITE_CONV ADD1) (rhs (concl th2))));;
88let th4 = ASSUME
89	"display((n' + sysinit) + 1) =
90	  WordVal n(WordAbs((b2 when (isHi phiA))((n' + sysinit) + 1)))";;
91let th5 = SUBS [th3] th4;;
92
93let TOPLEVEL_CORRECT = prove_thm (
94	`TOPLEVEL_CORRECT`,
95	"!n.
96	  let max = 2 EXP (n + 1) in
97	    !button switches display sysinit.
98	      DEVICE_IMP n (button,switches,display) /\
99	      (button sysinit = T)
100	      ==>
101	      !t. sysinit <= t ==>
102	        (display (t + 1) =
103	          button t => switches t | (((display t) + 1) MOD max))",
104	GEN_TAC THEN
105	SUBST1_TAC (SYM (SPEC "n" ADD1)) THEN
106	PURE_REWRITE_TAC [LET_DEF;DEVICE_IMP;BUTTON;SWITCHES;DISPLAY] THEN
107	BETA_TAC THEN
108	REPEAT GEN_TAC THEN STRIP_TAC THEN GEN_TAC THEN
109	PURE_REWRITE_TAC [LESS_OR_EQ_ADD] THEN
110	DISCH_THEN (STRIP_THM_THEN (SUBST1_TAC o SYM)) THEN
111	ASSUM_LIST_SPEC_TAC "sysinit" THEN
112	IMP_RES_TAC lemma1 THEN
113	DISJ_CASES_THENL
114	  [SUBST1_TAC;STRIP_THM_THEN SUBST1_TAC] (SPEC "p" num_CASES) THENL
115	[PURE_REWRITE_TAC [ADD_CLAUSES] THEN
116	 ASSUME_TAC (SPEC "sysinit" LESS_EQ_REFL) THEN
117	 IMP_RES_TAC COUNT_CORRECT THEN
118	 RES_TAC THEN
119	 ASM_REWRITE_TAC [BoolAbs_THM];
120	 ASSUME_TAC (SPECL ["sysinit";"n'"] lemma2) THEN
121	 ASSUME_TAC (SPECL ["sysinit";"SUC n'"] lemma2) THEN
122	 IMP_RES_TAC COUNT_CORRECT THEN
123	 RES_TAC THEN
124	 ASM_REWRITE_TAC [] THEN
125	 SUBST1_TAC th5 THEN
126	 ASM_REWRITE_TAC []]);;
127
128close_theory ();;
129