Hi all, I am trying to write a formula stating that one term is a substitution of another, eg `is_sub P Q <=> P[z/x] = Q`, so that `is_sub (x+y) (z+y)` should be true.
I cannot seem to find access to substitutions inside term syntax is this correct? I also tried defining substitution myself like so: `sub (z, x) y = if x = y then z else y` but then `sub (z,x) (x+y)` becomes `z+(if x = y then z else y)` which is not `z+y`. I assume this is because the equality testing in the above definition of `sub` is not syntactic equality. Is there anyway to ask for syntactic equality? I should note that I am working in Hol Light, so if that changes things, I wuold like to know that as well... best Rasmus ------------------------------------------------------------------------------ Start uncovering the many advantages of virtual appliances and start using them to simplify application deployment and accelerate your shift to cloud computing. http://p.sf.net/sfu/novell-sfdev2dev _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
