Dear All,
I'm trying to model a counter circuit which is consist of n JK-flip-flops. This
is the definition:
- val JKtype =
new_definition
("JKtype",
``!ck set reset j k out.
JKtype(ck,set,reset,j,k,out) =
!t. out (t+1) =
if ((set t) = T ) then T
else if ((reset t) = T ) then F
else if (( Down ck t ) = T) /\ ((set
t) = F ) /\ ((reset t) = (F:bool))
then (((j t) /\~(out
t)) \/ (~(k t)/\(out t)))
else out(t)
``);
- val Counter_IMP = Define `
Counter_IMP(ck,Init,h1::t1) =
?l0 l1.
(GND l0) /\ (VCC l1) /\
(JKtype (ck,l0,Init,l1,l1,h1))/\
(Counter_IMP(h1,Init,t1))
`;
The problems are that:
First , I don't know how to define the terminating condition when the
list is empty such as :
(!n. DROP n [] = []) /\
!n x xs. DROP n (x::xs) = if n = 0 then x::xs else DROP (n - 1) xs
Second ,when prove the definition ,Rewrite tactic cannot expand the
definition.
Is there any other way to define the counter functions.
Thank you for the attention and help.------------------------------------------------------------------------------
Find and fix application performance issues faster with Applications Manager
Applications Manager provides deep performance insights into multiple tiers of
your business applications. It resolves application problems quickly and
reduces your MTTR. Get your free trial!
https://ad.doubleclick.net/ddm/clk/302982198;130105516;z
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
