equal
deleted
inserted
replaced
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 |
|
180 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
179 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
181 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
180 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
182 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
181 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
183 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
182 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
184 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
183 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
194 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
193 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
195 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
194 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
196 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
195 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
197 apply(fold PLUS_def) |
196 apply(fold PLUS_def) |
198 apply(tactic {* clean_tac @{context} 1 *}) |
197 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 |
198 done |
203 |
199 |
204 lemma test3: "my_plus = my_plus" |
200 lemma test3: "my_plus = my_plus" |
205 apply(rule refl) |
201 apply(rule refl) |
206 done |
202 done |
215 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
211 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
216 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
212 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
217 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
213 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
218 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
214 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
219 apply(tactic {* clean_tac @{context} 1 *}) |
215 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 |
216 done |
222 |
217 |
223 |
218 |
224 lemma "PLUS a b = PLUS b a" |
219 lemma "PLUS a b = PLUS b a" |
225 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) |
220 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) |