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]>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
