Lines Matching defs:compatible
272 (* Define compatible relations on the term/method language. *)
277 val compatible =
278 new_definition ("compatible",
279 ���compatible R =
305 (compatible R /\
313 (compatible R /\
320 ���!R:^term_rel. compatible R ==> compatible (RC R)���,
321 REWRITE_TAC[compatible]
336 compatible R ==>
344 [ REWRITE_TAC[compatible]
364 ���!(R:^term_rel). compatible R ==> compatible (TC R)���,
367 THEN REWRITE_TAC[compatible]
379 (* page 51. This is the compatible closure of R. *)
631 (* 1) compatible (in the sense of Barendregt, Definition 3.1.1, pg 50 *)
632 (* 2) the compatible closure of the R relation, in the sense of *)
639 ���!R:^term_rel. compatible (RED1 R)���,
640 REWRITE_TAC[compatible]
652 ���!R:^term_rel. compatible (RC (RED1 R))���,
660 ���!R:^term_rel. compatible (TC (RC (RED1 R)))���,
754 (* 1) compatible (in the sense of Barendregt, Definition 3.1.1, pg 50 *)
789 ���!R:^term_rel. compatible (RED R)���,
790 REWRITE_TAC[compatible]
796 THEN IMP_RES_TAC (REWRITE_RULE[compatible] RED1_compatible)
802 (REWRITE_RULE[compatible] RED_compatible));
904 (* 1) compatible (in the sense of Barendregt, Definition 3.1.1, pg 50 *)
908 (* 4) an equality relation, as a compatible equivalence relation. *)
948 ���!R:^term_rel. compatible (REQUAL R)���,
949 REWRITE_TAC[compatible]
962 REWRITE_RULE[compatible] REQUAL_compatible);