Hi, I'm having the following error when I attempt to define a relation with Hol_reln:
Exception raised at IndDefLib.Hol_reln: at IndDefLib.Hol_mono_reln: at IndDefRules.derive_strong_induction: at Thm.EQ_MP: The failure of "derive_strong_induction" happens for a situation like the following. It is not exactly what I use (for rel1 and V_OK), which I don't show, since my actual version has a long definition dependency list, but the structure of the relation definition is identical (Hol_reln). val rel1_def = Define `rel1 (u:word32) v x y z = v x y z /\ x /\ y u /\ z`; val V_OK_def = Define `V_OK x y z = T`; Hol_reln ` (!p c q. rel1 u V_OK p c q ==> rel2 u p c q) /\ (!p c q. rel1 u (rel2 u) p c q ==> rel2 u p c q)` I'm trying to create a new relation "rel2" based on an existing relation "rel1," which has a parameter "v." When "v" is satisfied by the base case (rel2 u p c q), I want to say that (rel2 u) can be a new parameter to rel1, and that with the new parameter of rel1, I can have the relation rel2 again. I define the rel2 relation in order to limit how rel2 may be constructed (this is the only reason), and I don't need to use its strong induction theorem. How can I define this kind of relation, or is there another option to define such thing? Thanks a lot. Lu ------------------------------------------------------------------------------ The ultimate all-in-one performance toolkit: Intel(R) Parallel Studio XE: Pinpoint memory and threading errors before they happen. Find and fix more than 250 security defects in the development cycle. Locate bottlenecks in serial and parallel code that limit performance. http://p.sf.net/sfu/intel-dev2devfeb _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
