Belatedly: the constant behind HOL4's set comprehensions, GSPEC, is really just a version of IMAGE, so if you can think of a monotonicity theorem for IMAGE, that should be something you could transform to be suitable for GSPEC too.
Michael On 04/04/13 00:56, Ramana Kumar wrote: > I found a way around it: use a subset instead of the exact desired set. > That is, make the premise > tt s n1 n2 /\ (!n. n IN s ==> n < LENGTH v1 /\ n < LENGTH v2 /\ vv (EL n v1) > (EL > n v2)) > > > On Wed, Apr 3, 2013 at 2:11 PM, Ramana Kumar <[email protected] > <mailto:[email protected]>> wrote: > > I'm trying to write an inductive relation that relates equivalent > expressions in a programming language with respect to a context of pairs > of > variables assumed equivalent. > > I ran into this problem: > Exception raised at IndDefLib.Hol_reln: > at IndDefLib.Hol_mono_reln: > at IndDefRules.derive_strong_induction: > at Thm.EQ_MP > > I think what I need is a monotonicity rule for GSPEC, but I can't figure > out > what it should look like. Am I thinking in the right direction? > > Here is a very cut down example that exhibits the same problem: > > Hol_datatype`v = Cl of v list => num` > Hol_reln`(n IN s ==> tt s n n)` > > (* fails *) > Hol_reln` > (tt { n | n < LENGTH v1 /\ n < LENGTH v2 /\ vv (EL n v1) (EL n v2)} n1 > n2 > ==> vv (Cl v1 n1) (Cl v2 n2))` > > (* sanity check: works *) > Hol_reln` > n1 < LENGTH v1 /\ n1 < LENGTH v2 /\ vv (EL n1 v1) (EL n1 v2) /\ > (n1 = n2) > ==> vv (Cl v1 n1) (Cl v2 n2)` > > In my real example, vv and tt would be mutually recursive - does that make > it significantly harder? > > > > > ------------------------------------------------------------------------------ > Minimize network downtime and maximize team effectiveness. > Reduce network management and security costs.Learn how to hire > the most talented Cisco Certified professionals. Visit the > Employer Resources Portal > http://www.cisco.com/web/learning/employer_resources/index.html > > > > _______________________________________________ > hol-info mailing list > [email protected] > https://lists.sourceforge.net/lists/listinfo/hol-info >
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Minimize network downtime and maximize team effectiveness. Reduce network management and security costs.Learn how to hire the most talented Cisco Certified professionals. Visit the Employer Resources Portal http://www.cisco.com/web/learning/employer_resources/index.html
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
