171 apply(rule refl) |
171 apply(rule refl) |
172 done |
172 done |
173 |
173 |
174 lemma "PLUS a = PLUS a" |
174 lemma "PLUS a = PLUS a" |
175 apply(tactic {* procedure_tac @{context} @{thm test2} 1 *}) |
175 apply(tactic {* procedure_tac @{context} @{thm test2} 1 *}) |
176 oops |
176 apply(rule ballI) |
|
177 apply(rule apply_rsp[OF Quotient_my_int ho_plus_rsp]) |
|
178 apply(simp only: in_respects) |
|
179 |
|
180 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
181 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
182 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
183 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
184 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
185 apply(rule quot_rel_rsp) |
|
186 apply(tactic {* quotient_tac @{context} 1 *}) |
|
187 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
188 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
189 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
190 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
191 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
192 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
193 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
194 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
195 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
196 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
197 apply(fold PLUS_def) |
|
198 apply(tactic {* clean_tac @{context} 1 *}) |
|
199 thm Quotient_rel_rep |
|
200 thm Quotient_rel_rep[OF fun_quotient[OF Quotient_my_int Quotient_my_int]] |
|
201 apply(simp only: Quotient_rel_rep[OF fun_quotient[OF Quotient_my_int Quotient_my_int]]) |
|
202 done |
177 |
203 |
178 lemma test3: "my_plus = my_plus" |
204 lemma test3: "my_plus = my_plus" |
179 apply(rule refl) |
205 apply(rule refl) |
180 done |
206 done |
181 |
207 |
182 lemma "PLUS = PLUS" |
208 lemma "PLUS = PLUS" |
183 apply(tactic {* procedure_tac @{context} @{thm test3} 1 *}) |
209 apply(tactic {* procedure_tac @{context} @{thm test3} 1 *}) |
184 oops |
210 apply(rule ho_plus_rsp) |
|
211 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
212 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
213 apply(rule quot_rel_rsp) |
|
214 apply(tactic {* quotient_tac @{context} 1 *}) |
|
215 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
216 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
217 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
218 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
219 apply(tactic {* clean_tac @{context} 1 *}) |
|
220 apply(simp only: Quotient_rel_rep[OF fun_quotient[OF Quotient_my_int fun_quotient[OF Quotient_my_int Quotient_my_int]]]) |
|
221 done |
185 |
222 |
186 |
223 |
187 lemma "PLUS a b = PLUS b a" |
224 lemma "PLUS a b = PLUS b a" |
188 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) |
225 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) |
189 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
226 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |