Hi, I'm having a problem in matching pairs when using inductive relation for proof. It can be demonstrated by the following example.
Suppose I define a relation: val (PEQ_rules, PEQ_ind, PEW_cases) = Hol_reln ` (!l1:num a1:num l2:num a2:num. (l1 = l2) ==> PEQ (l1,a1) (l2,a2))` val [PEQ_INS] = CONJUNCTS PEQ_rules Then, I'd like to prove the following goal: g`!p1 p2 p3. PEQ p1 p2 ==> PEQ p2 p3 ==> PEQ p1 p3` Everything is fine, after these two tactics: NTAC 3 STRIP_TAC THEN RULE_INDUCT_THEN PEQ_ind ASSUME_TAC ASSUME_TAC However, problem begins to show up. I need to change the tuple of (l2,a2) into a single variable in order to use RULE_INDUCT_THEN one more time. However, this obscures the relation of "l2 = FST p3." RULE_INDUCT_THEN introduces a free variable for (FST p3), which is not related to l2, resulting in the failure of proof. `?p2. (l2,a2) = p2` by METIS_TAC [] \\ ASM_REWRITE_TAC [] RULE_INDUCT_THEN PEQ_ind ASSUME_TAC ASSUME_TAC RULE_TAC PEQ_INS This example may be resolved by using Define for PEQ, but I'm deal with sets and other customized operations which do not have a constructor. Using inductive relation is the only option in my mind. Any method to solve this or an alternative way is very welcomed. Thank you very much. Lu ------------------------------------------------------------------------------ Come build with us! The BlackBerry(R) Developer Conference in SF, CA is the only developer event you need to attend this year. Jumpstart your developing skills, take BlackBerry mobile applications to market and stay ahead of the curve. Join us from November 9 - 12, 2009. Register now! http://p.sf.net/sfu/devconference _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
