equal
deleted
inserted
replaced
128 lemma Church_Rosser_confluent: "Church_Rosser R = confluent R" |
128 lemma Church_Rosser_confluent: "Church_Rosser R = confluent R" |
129 apply (unfold square_def commute_def diamond_def Church_Rosser_def) |
129 apply (unfold square_def commute_def diamond_def Church_Rosser_def) |
130 apply (tactic {* safe_tac HOL_cs *}) |
130 apply (tactic {* safe_tac HOL_cs *}) |
131 apply (tactic {* |
131 apply (tactic {* |
132 blast_tac (HOL_cs addIs |
132 blast_tac (HOL_cs addIs |
133 [Un_upper2 RS rtrancl_mono RS subsetD RS rtrancl_trans, |
133 [thm "Un_upper2" RS thm "rtrancl_mono" RS thm "subsetD" RS thm "rtrancl_trans", |
134 rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD]) 1 *}) |
134 thm "rtrancl_converseI", thm "converseI", |
|
135 thm "Un_upper1" RS thm "rtrancl_mono" RS thm "subsetD"]) 1 *}) |
135 apply (erule rtrancl_induct) |
136 apply (erule rtrancl_induct) |
136 apply blast |
137 apply blast |
137 apply (blast del: rtrancl_refl intro: rtrancl_trans) |
138 apply (blast del: rtrancl_refl intro: rtrancl_trans) |
138 done |
139 done |
139 |
140 |