Hello,
I am trying to prove:
g `WiresRTC((CA (HighSignal str)),s) ==> ((CA (HighSignal str)) IN s) \/
?str1. WiresRTC((CA (HighSignal str1)),s) /\
((CA (SignalLink str str1)) IN s)`;
which is an intermediate result I need to prove WiresRTC (the
reflexive-transitive closure of a set of actions) being reflexive.
As the definition of WiresRTC is:
val (WiresRTC_rules, WiresRTC_ind, WiresRTC_cases) =
Hol_reln
`(!str aSet. (CA (HighSignal str) IN aSet)
==> WiresRTC(CA (HighSignal str), aSet)) /\
(!str str1 aSet. (CA (SignalLink str str1) IN aSet)
==> WiresRTC(CA (SignalLink str str1), aSet)) /\
(!ct aSet. ((CT ct) IN aSet)
==> WiresRTC((CT ct), aSet)) /\
(!str str1 aSet.
WiresRTC(CA (HighSignal str1), aSet) /\
(CA (SignalLink str str1) IN aSet)
==> WiresRTC(CA (HighSignal str),aSet))`;
the proof I am attempting should be quite straightforward (at least, in
principle).
I think the key for the proof to work will be to "expand" the first
occurrence of WiresRTC (probably using "WiresRTC_cases") and try to go
on from there. The problem with this idea is that none of the standard
"rewrite" tactics will expand ONLY the first occurrence (i.e., they will
also expand the second one in this case).
I found that it should be possible to achieve the behaviour I want by
means of something like:
e (GEN_REWRITE_TAC (RATOR_CONV o ONCE_DEPTH_CONV)[][WiresRTC_cases]);
but I am getting this error:
! Toplevel input:
! e (GEN_REWRITE_TAC (RATOR_CONV o ONCE_DEPTH_CONV) [][WiresRTC_cases]);
! ^
! Type clash: expression of type
! 'a list
! cannot have type
! rewrites
This is the same kind of application I have seen in some other examples
in the web... so I am not sure what is HOL complaining about (I am using
HOL4 Kananaskis 5).There is even a example in the documentation that
states:
GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [] [ADD_SYM]
(that seems to have the same structure I am using, but calling a
different theorem at the end...). Can you provide me with any hints of
what I am doing wrong here?
I would also like to know if there is any way of defining the
reflexive-transitive closure of a relation in a better way (i.e., so
that HOL knows what it is and there is no need to prove, for example,
that WiresRTC(WiresRTC(a)) = WiresRTC(a)).
Thank you very much,
Juan
-------------------------------------------------------------------------
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2005.
http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
