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
