Hello everybody,
I am trying to prove something of the shape:
goal
--------------
<some hypothesis>
...
CA (SignalLink str str1) IN
c1Init' UNION {CA (HighSignal (P_s c1))}
The constructors used in the last hypothesis belong to the datatypes:
Hol_datatype
`hwAction = CA of combAction <--- THIS ONE
| CT of combTest
| PT of progTest
| LoopBack of circ`;
Hol_datatype
`combAction = ChanReader of string
| ChanWriter of string
| ChanVal of string => num
| HighSignal of string <--- THIS
| SignalLink of string => string`; <--- AND THIS ONE
Here I used `e (FULL_SIMP_TAC (std_ss ++ pred_setSimps.PRED_SET_ss) [pred_setTheory.IN_UNION])`
expecting to get rid of the option `CA (SignalLink str str1) IN {CA (HighSignal (P_s c1))}` to get
`CA (SignalLink str str1) IN c1Init` (which is what I need for the proof).
The problem is that I got two subgoals to prove after applying FULL_SIMP_TAC: one is the one I
expected and another one of the form:
goal
--------------
<some hypothesis>
...
CA (SignalLink str str1) = CA (HighSignal (P_s c1))
Why is this happening? They are different constructors for the same datatype (so, as far as I
understand, they cannot be equal). Am I missing something?
Thank you very much for your help.
Cheers,
Juan
PS: I attached a simplified version of the source file I am using in case you want to reproduce the
situation I am in (I am using HOL 4, Kananaskis 5).
load "stringTheory";
load "pred_setTheory";
load "pred_setSimps";
Hol_datatype
`combAction = ChanReader of string
| ChanWriter of string
| ChanVal of string => num
| HighSignal of string
| SignalLink of string => string`;
Hol_datatype
`combTest = SignalHigh of string
| ReaderPresence of string
| WriterPresence of string
| CT_not of combTest`;
Hol_datatype
`hwAction = CA of combAction
| CT of combTest`;
val (WiresRTC_rules, WiresRTC_ind, WiresRTC_cases) =
Hol_reln
`(!str aSet. (CA (HighSignal str) IN aSet)
==> WiresRTC(CA (HighSignal str), aSet)) /\
(!str str1 aSet. (CA (SignalLink str str1) IN aSet)
==> WiresRTC(CA (SignalLink str str1), aSet)) /\
(!ct aSet. ((CT ct) IN aSet)
==> WiresRTC((CT ct), aSet)) /\
(!str str1 aSet.
WiresRTC(CA (HighSignal str1), aSet) /\
(CA (SignalLink str str1) IN aSet)
==> WiresRTC(CA (HighSignal str),aSet))`;
val WiresRTC_INDUCT_TAC =
IndDefRules.RULE_INDUCT_THEN WiresRTC_ind STRIP_ASSUME_TAC STRIP_ASSUME_TAC;
val satTest_def =
Define `(satTest (CT (SignalHigh w)) s = WiresRTC((CA (HighSignal w)),s))
/\ (satTest a s = T)`;
val wireSAT_def =
Define `(wireSAT s =
!a wId. (a IN s) /\ (a = (CT (SignalHigh wId))) ==> (satTest a s))`;
(* PROPERTIES *)
g `wireSAT (c1Init UNION {CA (HighSignal (P_s c1))}) =
wireSAT (c1Init UNION {CA (HighSignal w);CA (SignalLink (P_s c1) w)})`;
e (EQ_TAC THEN RW_TAC (std_ss ++ pred_setSimps.PRED_SET_ss)
[wireSAT_def,satTest_def] THEN RES_TAC);
(* case ==>: *)
e (UNDISCH_TAC ``WiresRTC
(CA (HighSignal wId),c1Init UNION {CA (HighSignal (P_s c1))})``);
e (Q_TAC SUFF_TAC `!a. WiresRTC a ==> !c1Init. ((SND a) = (c1Init UNION {CA
(HighSignal (P_s c1))})) ==>
WiresRTC((FST a), (c1Init UNION {CA (HighSignal w);CA
(SignalLink (P_s c1) w)}))` THEN1 METIS_TAC [pairTheory.FST,pairTheory.SND]);
e (WiresRTC_INDUCT_TAC);
r 3;
e (RW_TAC std_ss [pairTheory.FST,pairTheory.SND]);
e (FULL_SIMP_TAC (std_ss ++ pred_setSimps.PRED_SET_ss)
[pairTheory.FST,pairTheory.SND,pred_setTheory.IN_UNION]);
-------------------------------------------------------------------------
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
