equal
deleted
inserted
replaced
112 by (rtac rtrancl_refl 1); |
112 by (rtac rtrancl_refl 1); |
113 by (blast_tac (claset() addIs [rtrancl_trans]) 1); |
113 by (blast_tac (claset() addIs [rtrancl_trans]) 1); |
114 by (etac r_into_rtrancl 1); |
114 by (etac r_into_rtrancl 1); |
115 qed "rtrancl_idemp"; |
115 qed "rtrancl_idemp"; |
116 Addsimps [rtrancl_idemp]; |
116 Addsimps [rtrancl_idemp]; |
|
117 |
|
118 goal thy "R^* O R^* = R^*"; |
|
119 br set_ext 1; |
|
120 by(split_all_tac 1); |
|
121 by(blast_tac (claset() addIs [rtrancl_trans]) 1); |
|
122 qed "rtrancl_idemp_self_comp"; |
|
123 Addsimps [rtrancl_idemp_self_comp]; |
117 |
124 |
118 goal Trancl.thy "!!r s. r <= s^* ==> r^* <= s^*"; |
125 goal Trancl.thy "!!r s. r <= s^* ==> r^* <= s^*"; |
119 by (dtac rtrancl_mono 1); |
126 by (dtac rtrancl_mono 1); |
120 by (Asm_full_simp_tac 1); |
127 by (Asm_full_simp_tac 1); |
121 qed "rtrancl_subset_rtrancl"; |
128 qed "rtrancl_subset_rtrancl"; |