Hi,
If I try to define RTC manually (like those in HOL tutorial, chapter 6,
page 74):
val (RTC1_rules, RTC1_ind, RTC1_cases) = Hol_reln `
(!x. RTC1 R x x) /\
(!x y z. R x y /\ RTC1 R y z ==> RTC1 R x z)`;
It seems that (maybe) I can also define the "same" relation with a
different transitive rule:
val (RTC2_rules, RTC2_ind, RTC2_cases) = Hol_reln `
(!x. RTC2 R x x) /\
(!x y z. RTC2 R x y /\ R y z ==> RTC2 R x z)`;
Here are some observations:
1. If I directly use the RTC definition from HOL's relationTheory, above
two transitive rules are both true, easily provable by theorems RTC_CASES1
and RTC_CASES2 (relationTheory):
> RTC_CASES1;
val it =
|- ∀R x y. R^* x y ⇔ (x = y) ∨ ∃u. R x u ∧ R^* u y:
thm
> RTC_CASES2;
val it =
|- ∀R x y. R^* x y ⇔ (x = y) ∨ ∃u. R^* x u ∧ R u y:
thm
2. The theorem RTC1_ind (generated by Hol_reln) is the same as theorem
RTC_INDUCT (relationTheory):
val RTC1_ind =
|- ∀R RTC1'.
(∀x. RTC1' x x) ∧ (∀x y z. R x y ∧ RTC1' y z ⇒ RTC1' x z) ⇒
∀a0 a1. RTC1 R a0 a1 ⇒ RTC1' a0 a1:
thm
> RTC_INDUCT;
val it =
|- ∀R P.
(∀x. P x x) ∧ (∀x y z. R x y ∧ P y z ⇒ P x z) ⇒
∀x y. R^* x y ⇒ P x y:
thm
Now my questions are:
1. Given any R, are the two relations (RTC1 R) and (RTC2 R) really the
same? i.e. is ``!R x y. RTC1 R x y = RTC2 R x y`` a theorem? (and if so,
how to prove it?)
2. (If the answer of last question is yes) Is it possible to prove the
following theorem RTC_INDUCT2 in relationTheory? (which looks like RTC2_ind
generated in above definition)
val RTC_INDUCT2 = store_thm(
"RTC_INDUCT2",
``!R P. (!x. P x x) /\ (!x y z. P x y /\ R y z ==> P x z) ==>
(!x (y:'a). RTC R x y ==> P x y)``,
cheat);
(and the corresponding RTC_STRONG_INDUCT2).
Regards,
--
Chun Tian (binghe)
University of Bologna (Italy)
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
