equal
deleted
inserted
replaced
125 |
125 |
126 subsection {* Church-Rosser *} |
126 subsection {* Church-Rosser *} |
127 |
127 |
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 (put_claset HOL_cs @{context}) *}) |
131 apply (tactic {* |
131 apply (tactic {* |
132 blast_tac (HOL_cs addIs |
132 blast_tac (put_claset HOL_cs @{context} addIs |
133 [@{thm sup_ge2} RS @{thm rtranclp_mono} RS @{thm predicate2D} RS @{thm rtranclp_trans}, |
133 [@{thm sup_ge2} RS @{thm rtranclp_mono} RS @{thm predicate2D} RS @{thm rtranclp_trans}, |
134 @{thm rtranclp_converseI}, @{thm conversepI}, |
134 @{thm rtranclp_converseI}, @{thm conversepI}, |
135 @{thm sup_ge1} RS @{thm rtranclp_mono} RS @{thm predicate2D}]) 1 *}) |
135 @{thm sup_ge1} RS @{thm rtranclp_mono} RS @{thm predicate2D}]) 1 *}) |
136 apply (erule rtranclp_induct) |
136 apply (erule rtranclp_induct) |
137 apply blast |
137 apply blast |