151 |
151 |
152 lemma test1: "my_plus a b = my_plus a b" |
152 lemma test1: "my_plus a b = my_plus a b" |
153 apply(rule refl) |
153 apply(rule refl) |
154 done |
154 done |
155 |
155 |
|
156 abbreviation |
|
157 "Abs \<equiv> ABS_my_int" |
|
158 abbreviation |
|
159 "Rep \<equiv> REP_my_int" |
|
160 abbreviation |
|
161 "Resp \<equiv> Respects" |
|
162 |
156 lemma "PLUS a b = PLUS a b" |
163 lemma "PLUS a b = PLUS a b" |
157 apply(tactic {* procedure_tac @{context} @{thm test1} 1 *}) |
164 apply(tactic {* procedure_tac @{context} @{thm test1} 1 *}) |
158 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
165 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
159 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
166 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
160 (* does not work yet *) |
167 apply(tactic {* clean_tac @{context} 1 *}) |
161 oops |
168 done |
162 |
169 |
163 lemma test2: "my_plus a = my_plus a" |
170 lemma test2: "my_plus a = my_plus a" |
164 apply(rule refl) |
171 apply(rule refl) |
165 done |
172 done |
166 |
173 |
167 lemma "PLUS a = PLUS a" |
174 lemma "PLUS a = PLUS a" |
168 apply(tactic {* procedure_tac @{context} @{thm test2} 1 *}) |
175 apply(tactic {* procedure_tac @{context} @{thm test2} 1 *}) |
169 (* does not work yet *) |
|
170 oops |
176 oops |
171 |
177 |
172 lemma test3: "my_plus = my_plus" |
178 lemma test3: "my_plus = my_plus" |
173 apply(rule refl) |
179 apply(rule refl) |
174 done |
180 done |
175 |
181 |
176 lemma "PLUS = PLUS" |
182 lemma "PLUS = PLUS" |
177 apply(tactic {* procedure_tac @{context} @{thm test3} 1 *}) |
183 apply(tactic {* procedure_tac @{context} @{thm test3} 1 *}) |
178 apply(rule ho_plus_rsp) |
|
179 (* does not work yet *) |
|
180 oops |
184 oops |
181 |
185 |
182 |
186 |
183 lemma "PLUS a b = PLUS b a" |
187 lemma "PLUS a b = PLUS b a" |
184 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) |
188 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) |