On 10/12/07, Juan Perna <[EMAIL PROTECTED]> wrote:
> Hello everybody,
>
> I am trying to prove something of the shape:
>
> goal
> --------------
> <some hypothesis>
> ...
> CA (SignalLink str str1) IN
> c1Init' UNION {CA (HighSignal (P_s c1))}
>
> The constructors used in the last hypothesis belong to the datatypes:
>
> Hol_datatype
> `hwAction = CA of combAction <--- THIS ONE
> | CT of combTest
> | PT of progTest
> | LoopBack of circ`;
>
>
> Hol_datatype
> `combAction = ChanReader of string
> | ChanWriter of string
> | ChanVal of string => num
> | HighSignal of string <--- THIS
> | SignalLink of string => string`; <--- AND THIS ONE
>
> Here I used `e (FULL_SIMP_TAC (std_ss ++ pred_setSimps.PRED_SET_ss)
> [pred_setTheory.IN_UNION])`
> expecting to get rid of the option `CA (SignalLink str str1) IN {CA
> (HighSignal (P_s c1))}` to get
> `CA (SignalLink str str1) IN c1Init` (which is what I need for the proof).
>
> The problem is that I got two subgoals to prove after applying FULL_SIMP_TAC:
> one is the one I
> expected and another one of the form:
>
>
> goal
> --------------
> <some hypothesis>
> ...
> CA (SignalLink str str1) = CA (HighSignal (P_s c1))
>
> Why is this happening? They are different constructors for the same datatype
> (so, as far as I
> understand, they cannot be equal). Am I missing something?
>
> Thank you very much for your help.
>
> Cheers,
>
> Juan
Dear Juan,
You need to add the one-to-one and distinctiveness properties of those
datatypes to the call to FULL_SIMP_TAC, as
FULL_SIMP_TAC (std_ss ++ pred_setSimps.PRED_SET_ss)
[pairTheory.FST,pairTheory.SND,pred_setTheory.IN_UNION,
TypeBase.one_one_of ``:hwAction``, TypeBase.distinct_of ``:hwAction``,
TypeBase.one_one_of ``:combAction``, TypeBase.distinct_of ``:combAction``]
SRW_TAC would include these automatically.
Peter
--
"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: Splunk Inc.
Still grepping through log files to find problems? Stop.
Now Search log events and configuration files using AJAX and a browser.
Download your FREE copy of Splunk now >> http://get.splunk.com/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
