Juan Perna wrote:
> 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?
You can either use the injectivity and distinctness theorems that
Peter mentioned explicitly, or you can use the (srw_ss()) simpset.
Thus, you might write
FULL_SIMP_TAC (srw_ss())) []
The srw_ss() value will include the "useful" rewrites from the theory
of sets that you quoted explicitly.
The SRW_TAC tactic simplifies the goal, not the assumptions.
It's more than possible that I will add
FSRW_TAC [][]
as an abbreviation for the FULL_SIMP_TAC call above in a future
release. If you want to define it yourself, its definition would be
fun FSRW_TAC ssfrags thlist =
FULL_SIMP_TAC
(List.foldl (fn (sf,ss) => ss ++ sf) (srw_ss()) ssfrags)
thlist
Regards,
Michael.
-------------------------------------------------------------------------
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
