equal
deleted
inserted
replaced
172 FIXME: All below is your construction code; mostly commented out as it |
172 FIXME: All below is your construction code; mostly commented out as it |
173 does not work. |
173 does not work. |
174 *) |
174 *) |
175 |
175 |
176 ML {* |
176 ML {* |
177 mk_regularize_trm @{context} |
177 regularize_trm @{context} |
178 @{term "\<forall>i j k. my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"} |
178 @{term "\<forall>i j k. my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"} |
179 @{term "\<forall>i j k. PLUS (PLUS i j) k = PLUS i (PLUS j k)"} |
179 @{term "\<forall>i j k. PLUS (PLUS i j) k = PLUS i (PLUS j k)"} |
180 |> Syntax.string_of_term @{context} |
180 |> Syntax.string_of_term @{context} |
181 |> writeln |
181 |> writeln |
182 *} |
182 *} |
183 |
183 |
184 lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)" |
184 lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)" |
185 apply(tactic {* procedure_tac @{thm plus_assoc_pre} @{context} 1 *}) |
185 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) |
186 apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *}) |
186 apply(tactic {* regularize_tac @{context} [rel_eqv] rel_refl 1 *}) |
187 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *}) |
187 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *}) |
188 apply(tactic {* clean_tac @{context} quot @{thms PLUS_def} reps_same 1 *}) |
188 oops |
189 done |
|
190 |
189 |
191 |
190 |
192 (* |
191 (* |
193 |
192 |
194 ML {* |
193 ML {* |