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 apply(rule ballI) |
176 apply(rule ballI) |
177 apply(rule apply_rsp[OF Quotient_my_int ho_plus_rsp]) |
177 apply(rule apply_rsp[OF Quotient_my_int ho_plus_rsp]) |
178 apply(simp only: in_respects) |
178 apply(simp only: in_respects) |
179 |
179 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
180 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
180 apply(tactic {* clean_tac @{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]]) |
181 apply(simp only: Quotient_rel_rep[OF fun_quotient[OF Quotient_my_int Quotient_my_int]]) |
202 done |
182 done |
203 |
183 |
204 lemma test3: "my_plus = my_plus" |
184 lemma test3: "my_plus = my_plus" |
205 apply(rule refl) |
185 apply(rule refl) |
206 done |
186 done |
207 |
187 |
208 lemma "PLUS = PLUS" |
188 lemma "PLUS = PLUS" |
209 apply(tactic {* procedure_tac @{context} @{thm test3} 1 *}) |
189 apply(tactic {* procedure_tac @{context} @{thm test3} 1 *}) |
210 apply(rule ho_plus_rsp) |
190 apply(rule ho_plus_rsp) |
211 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
191 apply(tactic {* all_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 *}) |
192 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]]]) |
193 apply(simp only: Quotient_rel_rep[OF fun_quotient[OF Quotient_my_int fun_quotient[OF Quotient_my_int Quotient_my_int]]]) |
221 done |
194 done |
222 |
195 |
223 |
196 |