Juan, you could try
e(CONV_TAC (RATOR_CONV (ONCE_REWRITE_CONV [WiresRTC_cases])));
This should apply the cases theorem as a rewrite rule just once and
just to the operator ("RATOR") of the current goal.
Peter
On 9/24/07, Juan Perna <[EMAIL PROTECTED]> wrote:
> 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
>
--
"In Your majesty ride prosperously
because of truth, humility, and righteousness;
and Your right hand shall teach You awesome things." (Psalm 45:4)
-------------------------------------------------------------------------
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
