# HG changeset patch # User nipkow # Date 903601038 -7200 # Node ID d014d7e57337df6cff29fe82b96d14192cc34042 # Parent bc9748ad849104efaf030428bbce373ca5603720 Added converse_rtranclE(2) diff -r bc9748ad8491 -r d014d7e57337 src/HOL/Trancl.ML --- a/src/HOL/Trancl.ML Thu Aug 20 09:25:59 1998 +0200 +++ b/src/HOL/Trancl.ML Thu Aug 20 10:17:18 1998 +0200 @@ -170,19 +170,8 @@ by (blast_tac (claset() addIs prems addSDs[rtrancl_converseD])1); qed "converse_rtrancl_induct"; -val prems = Goal - "[| ((a,b),(c,d)) : r^*; P c d; \ -\ !!x y z u.[| ((x,y),(z,u)) : r; ((z,u),(c,d)) : r^*; P z u |] ==> P x y\ -\ |] ==> P a b"; -by (res_inst_tac[("R","P")]splitD 1); -by (res_inst_tac[("P","split P")]converse_rtrancl_induct 1); -by (resolve_tac prems 1); -by (Simp_tac 1); -by (resolve_tac prems 1); -by (split_all_tac 1); -by (Asm_full_simp_tac 1); -by (REPEAT(ares_tac prems 1)); -qed "converse_rtrancl_induct2"; +bind_thm ("converse_rtrancl_induct2", split_rule + (read_instantiate [("a","(ax,ay)"),("b","(bx,by)")]converse_rtrancl_induct)); val major::prems = Goal "[| (x,z):r^*; \ @@ -194,10 +183,13 @@ by (blast_tac (claset() addIs prems) 2); by (blast_tac (claset() addIs prems) 2); by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1)); -qed "rtranclE2"; +qed "converse_rtranclE"; + +bind_thm ("converse_rtranclE2", split_rule + (read_instantiate [("x","(xa,xb)"), ("z","(za,zb)")] converse_rtranclE)); Goal "r O r^* = r^* O r"; -by (blast_tac (claset() addEs [rtranclE, rtranclE2] +by (blast_tac (claset() addEs [rtranclE, converse_rtranclE] addIs [rtrancl_into_rtrancl, rtrancl_into_rtrancl2]) 1); qed "r_comp_rtrancl_eq";