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
