examples/lambda/etaScript.sml

91 (* This defines TC in the logic as TC R is the transitive closure of R,  *)
94 (* induction tactics, cases theorems, etc.  It's theory "TC".            *)
105           val (TC,Ru'v') = strip_comb ant
110           (*val (TC,[R,u',v']) = strip_comb ant*)
111           (*val {Name = "TC",...} = dest_const TC*)
112           val _ = if #Name(dest_const TC) = "TC" then true else raise Match
397     ���!R1 R2 (a:'a) b. TC (R1 UNION_R R2) a b ==>
400                (?d. (R1 UNION_R R2) b d /\ TC (R1 UNION_R R2) c d)))���),
430     ���!R1 R2 (a:'a) b. TC (R1 UNION_R R2) a b ==>
432            (!c. TC (R1 UNION_R R2) a c ==>
433                (?d. TC (R1 UNION_R R2) b d /\ TC (R1 UNION_R R2) c d)))���),
467           DIAMOND (TC (R1 UNION_R R2))���,
572                       TC (RED R1 UNION_R RED R2) t1 t2���),
628     ���!R1 R2 t1:^term t2. TC (RED R1 UNION_R RED R2) t1 t2 ==>
652     ���!R1:^term_rel R2. RED (R1 UNION_R R2) = TC (RED R1 UNION_R RED R2)���,
691                       ?d. TC (RC R2) b d /\ RC R1 c d) ==>
693                    ?d. RC R1 b d /\ TC (RC R2) c d)���),
715                       ?d. TC (RC R2) b d /\ RC R1 c d) ==>
717                    ?d. TC (RC R2) b d /\ RC R1 c d)���),
734           TC (RC R2) a b ==>
737                       ?d. TC (RC R2) b d /\ RC R1 c d) ==>
739                    ?d. RC R1 b d /\ TC (RC R2) c d)���),
758           TC (RC R1) a b ==>
761                       ?d. TC (RC R2) b d /\ RC R1 c d) ==>
762           (!c. TC (RC R2) a c ==>
763                    ?d. TC (RC R2) b d /\ TC (RC R1) c d)���),
788                    ?d. TC (RC R2) b d /\ RC R1 c d) ==>
789           (TC (RC R1) <=> TC (RC R2))���,
1147          ?M3. RC (RED1 BETA_R) M1 M3 /\ TC (RC (RED1 ETA_R)) M2 M3���,
1207          ?M3. TC (RC (RED1 ETA_R)) M1 M3 /\ RC (RED1 BETA_R) M2 M3���,