Hello,
I am trying to prove a goal of the form:
g `(stepWise s1 s2) /\ (seqWireSAT s1) /\ (seqWireSAT s2) ==> seqWireSAT
(parMerge s1 s2)`;
were `s1` and `s2` are of type seq as follows:
Hol_datatype
`seq =
Empty
| CombBlk of hwAction set => seq
| ClkBlk of clkAction set => seq`;
and `stepWise` is a boolean predicate capturing the notion of structural
equivalence (i.e., both
sequences follow the same pattern of constructors).
My question is whether there is a way of inducting on both `s1` and `s2` as a
"whole" (probably as a
pair). I am asking for this because I have attempted this proof by doing the
induction in sequential
order (i.e., Induct_on `s1` THEN Induct_on `s2`) and the inductive hypotheses I
got weren't useful
to prove the goal.
In particular, the case where I got stuck when inducting independently looks
like:
seqWireSAT(parMerge (CombBlk f s1) (CombBlk f' s2))
-------------------------------------------------------
<some hypotheses>
n. stepWise (CombBlk f s1) (CombBlk f' s2)
n+1. seqWireSAT s1
n+2. seqWireSAT s2
n+3. stepWise s1 (CombBlk f s2) ==>
seqWireSAT(parMerge s1 (CombBlk f' s2))
The problem here seems to be that inductive hypotheses are related to
individual increments either
of `s1` or `s2` (as the case of hyp. n+3) and if the property holds in the case
described by the
inductive hypotheses, then it does not hold when the other sequence "catches
up" (which is the case
described in the goal under the current inductive schema).
I also tried to define my goal in terms of a pair of sequences (rather than
`s1` and `s2`), but I
got an error ("not a forall") when trying to use induction from it.
I think that an inductive approach of the form:
a) base case: P(Empty,Empty) holds
b) assume P(s1,s2)
c) prove for:
- P((ClkBlk ca s1),(ClkBlk ca' s2))
- P((ClkBlk ca s1),(CombBlk a s2))
- (and all the other possible combinations)
should allow me to prove what I need.
Is there anything like this in HOL? If there is not, do you have any
suggestions about how could I
attack the proof I am not able to complete?
Thank you very much for your help,
Juan
-------------------------------------------------------------------------
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
