Hi Juan,
Seems to be something about the way the goal is stated.
You've got
>> `!a. smPred a ==>
>> !sec c. (a = (c,seq)) ==> ?hwa. ((seqLast seq) = (Link hwa Empty))`
If this is restated as
!a. smPred a ==> ?hwa. seqLast (SND a) = Link hwa Empty
then the IHs end up looking like what you want.
Konrad.
On Oct 5, 2007, at 4:49 AM, Juan Ignacio Perna wrote:
> Hello everybody,
>
> I am using an inductively defined predicate "smPred" defined as:
>
> val (smPred_rules, smPred_ind, smPred_cases) =
> Hol_reln
> (* DELAY *)
> `(!s f. smPred((Delay s f),(Link {} Empty))) /\
>
> (* SEQUENTIAL COMPOSITION *)
> (!s f c1 c2 c1Seq c2Seq. smPred(c1,c1Seq) /\ smPred(c2,c2Seq)
> ==> smPred((SeqComp s f c1 c2),
> (concat
> (concat c1Seq c2Seq)
> (Link {(CA (SignalLink f (P_f c2)))} Empty))))`;
>
> that relates a circuit with the sequences of actions that describe its
> semantics.
>
> I also have a function that returns the last element of a given
> sequence
> ("seqLast") (I am attaching a simple version of the source file so you
> can have a look if you want).
>
> I am trying to prove that the last element of a sequence (for all
> sequences generated by the predicate) is always of the form "?hwa.
> (Link hwa Empty)" (which we can say is true by inspecting the way in
> which the predicate "builds" the sequences).
>
> I am intending to use smPred_ind to make the proof, so I stated the
> goal as:
>
> `!a. smPred a ==>
> !sec c. (a = (c,seq)) ==> ?hwa. ((seqLast seq) = (Link hwa Empty))`
>
> After doing "e (HO_MATCH_MP_TAC smPred_ind)", stripping the goal and
> proving the base case, I end up with:
>
> ?hwa. seqLast seq = Link hwa Empty
> ------------------------------------
> 0. !sec c.
> ((c1,c1Seq) = (c,seq)) ==> ?hwa. seqLast seq = Link hwa Empty
> 1. !sec c.
> ((c2,c2Seq) = (c,seq)) ==> ?hwa. seqLast seq = Link hwa Empty
> 2. (SeqComp s f c1 c2,
> concat (concat c1Seq c2Seq)
> (Link {CA (SignalLink f (P_f c2))} Empty)) =
> (c,seq)
>
> I have tried to reduce/simplify/transform:
>
> 0. !sec c.
> ((c1,c1Seq) = (c,seq)) ==> ?hwa. seqLast seq = Link hwa Empty
>
> into: "?hwa. seqLast c1Seq = Link hwa Empty" which is the inductive
> hypothesis I was expecting to get (one of them), but I haven't been
> able
> to make much progress. The problem seems to be in the way the
> variables are quantified (i.e., it doesn't allow me to instantiate
> "seq" to "c1Seq" that is what I need).
>
> Is there any way to get the inductive hypothesis in a more "useful"
> way? (Is there any transformation I haven't check?). Should I try to
> re-state the goal in a different way? (I tried to do this, but I
> wasn't able to use HO_MATCH_TAC with the induction principle on them).
>
> I also explored the possibility of using Tom Melham's "IndDefRules"
> and defined the induction tactic for smPred as:
>
> val smPred_INDUCT_TAC =
> IndDefRules.RULE_INDUCT_THEN smPred_ind STRIP_ASSUME_TAC
> STRIP_ASSUME_TAC;
>
> but it seems to accept goals only in the form required by
> "HO_MATCH_TAC smPred_ind" (and it produces the same results). I tried
> to use it with some other versions of the goal (such as: `!seq c.
> smPred(c, seq) ==> ?hwa. ((seqLast seq) = (Link hwa Empty))`) but got
> the exception: "Inappropriate goal" (I read Tom Melham's paper about
> IndDefRules that comes with the HOL source files, but I wasn't able to
> find a precise description of the "format" of the goal that the tactic
> expects). Is there any further information about this somewhere?
>
> I also found a curious thing when trying to prove the goal from Tom
> Melham's package. The sub-goal of the proof related to the inductive
> step of the definition is:
>
> !sec c.
> ((SeqComp s f c1 c2,
> concat (concat c1Seq c2Seq) (Link {SignalLink f (P_f c2)} Empty)) =
> (c,seq)) ==>
> ?hwa. seqLast seq = Link hwa Empty
> ------------------------------------
> 0. !sec c.
> ((c1,c1Seq) = (c,seq)) ==> ?hwa. seqLast seq = Link hwa Empty
> 1. !sec c.
> ((c2,c2Seq) = (c,seq)) ==> ?hwa. seqLast seq = Link hwa Empty
>
> if we do (FULL_SIMP_TAC std_ss []), we get the two "seq" in the
> assumptions abstracted (together with some simplification in the goal
> as well):
>
> (concat (concat c1Seq c2Seq) (Link {SignalLink f (P_f c2)} Empty) =
> seq) ==>
> ?hwa. seqLast seq = Link hwa Empty
> ------------------------------------
> 0. (c1Seq = seq) ==> ?hwa. seqLast seq = Link hwa Empty
> 1. (c2Seq = seq) ==> ?hwa. seqLast seq = Link hwa Empty
>
> if we do "RW_TAC std_ss []" here, we get the two "seq" occurrences in
> the assumptions expanded with the information in the goal:
>
> ?hwa.
> seqLast
> (concat (concat c1Seq c2Seq) (Link {SignalLink f (P_f c2)} Empty))
> =
> Link hwa Empty
> ------------------------------------
> 0. (c1Seq =
> concat (concat c1Seq c2Seq)
> (Link {SignalLink f (P_f c2)} Empty)) ==>
> ?hwa.
> seqLast
> (concat (concat c1Seq c2Seq)
> (Link {SignalLink f (P_f c2)} Empty)) =
> Link hwa Empty
> 1. (c2Seq =
> concat (concat c1Seq c2Seq)
> (Link {SignalLink f (P_f c2)} Empty)) ==>
> ?hwa.
> seqLast
> (concat (concat c1Seq c2Seq)
> (Link {SignalLink f (P_f c2)} Empty)) =
> Link hwa Empty
>
> I am not completely sure, but this doesn't seem to be right thing to
> do in this case. Is this the intended behaviour?
>
>
> Thank you very much for your help,
>
> Juan
> load "stringTheory";
> load "pred_setTheory";
>
> Hol_datatype
> `combAction = HighSignal of string
> | SignalLink of string => string`;
>
> Hol_datatype
> `circ = Delay of string => string
> | SeqComp of string => string => circ => circ`;
>
>
> Hol_datatype
> `seq =
> Empty
> | CombBlk of combAction set => seq
> | Link of combAction set => seq`;
>
> (* ---------------- concatenation function -------------- *)
> val concat_def =
> Define `(concat Empty s = s)
> /\ (concat (CombBlk a rst) s = CombBlk a (concat rst s))
> /\ (concat (Link cas rst) s = Link cas (concat rst s))`;
>
> (* ------------ Projection functions --------------- *)
> val P_s_def =
> Define `(P_s (Delay start finish) = start)
> /\ (P_s (SeqComp start finish c1 c2) = start)`;
>
> val P_f_def =
> Define `(P_f (Delay start finish) = finish)
> /\ (P_f (SeqComp start finish c1 c2) = finish)`;
>
> (* ------------------- Semantic function --------------------*)
> val (smPred_rules, smPred_ind, smPred_cases) =
> Hol_reln
> (* DELAY *)
> `(!s f. smPred((Delay s f),(Link {} Empty))) /\
>
> (* SEQUENTIAL COMPOSITION *)
> (!s f c1 c2 c1Seq c2Seq. smPred(c1,c1Seq) /\ smPred(c2,c2Seq)
> ==> smPred((SeqComp s f c1 c2),
> (concat
> (concat c1Seq c2Seq)
> (Link {(SignalLink f (P_f c2))} Empty))))`;
>
>
> val smPred_INDUCT_TAC =
> IndDefRules.RULE_INDUCT_THEN smPred_ind STRIP_ASSUME_TAC
> STRIP_ASSUME_TAC;
>
> (* ---------------------- Sm(c) always produces a Link at the
> end----------------------- *)
>
> val seqLast_def =
> Define `(seqLast Empty = Empty)
> /\ (seqLast (CombBlk hwa rst) =
> if (rst = Empty)
> then (CombBlk hwa Empty)
> else (seqLast rst))
> /\ (seqLast (Link hwa rst) =
> if (rst = Empty)
> then (Link hwa Empty)
> else (seqLast rst))`;
> -----------------------------------------------------------------------
> --
> 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
-------------------------------------------------------------------------
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
