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
