Hi Juan,
Although it is useful, RW_TAC is not the only reasoning tool to
use in HOL, as you are finding. In your example, if you want to
get to a state
> seq IN
> setSeqLast
> (setSeqConcat
> (setSetConcat
> (seqSetConcat (CombBlk {CA (SignalLink (P_s c') s0)} Empty)
> (sm c'))
> (seqSetConcat
> (CombBlk {CA (SignalLink (P_s c0) (P_f c'))} Empty) (sm
> c0)))
> (Link {CA (SignalLink s (P_f c0))} Empty)) ==>
> ?hwa. seq = Link hwa Empty
> ----------------------------------------------------------
> 1 ~((sm c') = {})
> 2 ~((sm c0) = {})
> 3 ...
> .
> .
> .
> n ~((setSetConcat
> (seqSetConcat (CombBlk {CA (SignalLink (P_s c') s0)} Empty)
> (sm c'))
> (seqSetConcat
> (CombBlk {CA (SignalLink (P_s c0) (P_f c'))} Empty) (sm c0)))
> = {})
where the last hypothesis will solve the goal, I'd explicitly state the
last hypothesis as a new sub-goal, prove it in isolation, and
then return to the main line of the proof. To do this, I'd start
by doing
e (`~((setSetConcat
(seqSetConcat (CombBlk {CA (SignalLink (P_s c') s0)} Empty)
(sm c'))
(seqSetConcat
(CombBlk {CA (SignalLink (P_s c0) (P_f c'))} Empty) (sm c0)))
= {})`
by ALL_TAC);
and then apply some lemmas (maybe using METIS_TAC) that propagate
non-emptiness under the operations in your formula. Once you are
doing with proving the hypothesis, it will appear on your assumption
list and you should be able to finish your proof then.
Konrad.
On Sep 25, 2007, at 10:51 AM, Juan Perna wrote:
> Hello,
>
> This is probably a simple question, but I couldn't find a way of doing
> it...
>
> I am proving this subgoal:
>
> seq IN
> setSeqLast
> (setSeqConcat
> (setSetConcat
> (seqSetConcat (CombBlk {CA (SignalLink (P_s c') s0)} Empty)
> (sm c'))
> (seqSetConcat
> (CombBlk {CA (SignalLink (P_s c0) (P_f c'))} Empty) (sm
> c0)))
> (Link {CA (SignalLink s (P_f c0))} Empty)) ==>
> ?hwa. seq = Link hwa Empty
>
> this looks quite ugly, but it can be "abstracted" to:
>
> seq IN
> setSeqLast
> (setSeqConcat
> setOfTraces
> (Link {CA (SignalLink s (P_f c0))} Empty)) ==>
> ?hwa. seq = Link hwa Empty
>
> I have a couple of results that should be enough to solve the proof,
> the
> main one being:
>
> setSeqLastSetSeqConcat |-
> ~(seq = Empty) /\ ~(seqSet = {}) ==>
> (setSeqLast (setSeqConcat seqSet seq) = {seqLast seq})
>
> under valid assumptions, this should reduce the goal to something like:
> seq IN
> {seqLast (Link {CA (SignalLink s (P_f c0))} Empty))} ==>
> ?hwa. seq = Link hwa Empty
>
> and from there it is possible to finish it.
>
> The problem is how to "add" the assumptions that setSeqLastSetSeqConcat
> needs (i.e., that the setOfTraces is not the empty set). In this
> direction, I have some results that would provide what is needed (for
> example: I have a thm telling me: !c. ~((sm c) = {})). My problem here
> is that I don't know how to tell HOL how to use this theorems.
>
> I tried with RW_TAC std_ss [all pertinent thms here], but nothing
> happened (I think it was not possible for HOL to infer what I wanted to
> do). I also tried with ACCEPT_TAC, but doesn't seem to be what I need
> (as none of these theorems will solve the goal just by themselves).
>
> What I need is a way of adding assumptions to the proof. For example, I
> think it would be necessary to add that ~((sm c) = {}) to the
> assumptions (knowing this is valid assumption given the result I
> mentioned before). With this, I think I should be getting something
> like:
>
> seq IN
> setSeqLast
> (setSeqConcat
> (setSetConcat
> (seqSetConcat (CombBlk {CA (SignalLink (P_s c') s0)} Empty)
> (sm c'))
> (seqSetConcat
> (CombBlk {CA (SignalLink (P_s c0) (P_f c'))} Empty) (sm
> c0)))
> (Link {CA (SignalLink s (P_f c0))} Empty)) ==>
> ?hwa. seq = Link hwa Empty
> ----------------------------------------------------------
> 1 ~((sm c') = {})
> 2 ~((sm c0) = {})
> 3 ...
> .
> .
> .
> n ~((setSetConcat
> (seqSetConcat (CombBlk {CA (SignalLink (P_s c') s0)} Empty)
> (sm c'))
> (seqSetConcat
> (CombBlk {CA (SignalLink (P_s c0) (P_f c'))} Empty) (sm c0)))
> = {})
>
> with this additional hypothesis, I think a RW_TAC std_ss
> [setSeqLastSetSeqConcat] should get me where I want to go...
>
> Thank you,
>
> 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
-------------------------------------------------------------------------
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
