146 |
146 |
147 ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] *} |
147 ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] *} |
148 |
148 |
149 ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy [rel_refl] [trans2] *} |
149 ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy [rel_refl] [trans2] *} |
150 ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy [rel_refl] [trans2] *} |
150 ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy [rel_refl] [trans2] *} |
|
151 |
|
152 lemma test1: "my_plus a b = my_plus a b" |
|
153 apply(rule refl) |
|
154 done |
|
155 |
|
156 lemma "PLUS a b = PLUS a b" |
|
157 apply(tactic {* procedure_tac @{context} @{thm test1} 1 *}) |
|
158 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
|
159 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
160 (* does not work yet *) |
|
161 oops |
|
162 |
|
163 lemma test2: "my_plus a = my_plus a" |
|
164 apply(rule refl) |
|
165 done |
|
166 |
|
167 lemma "PLUS a = PLUS a" |
|
168 apply(tactic {* procedure_tac @{context} @{thm test2} 1 *}) |
|
169 (* does not work yet *) |
|
170 oops |
|
171 |
|
172 lemma test3: "my_plus = my_plus" |
|
173 apply(rule refl) |
|
174 done |
|
175 |
|
176 lemma "PLUS = PLUS" |
|
177 apply(tactic {* procedure_tac @{context} @{thm test3} 1 *}) |
|
178 apply(rule ho_plus_rsp) |
|
179 (* does not work yet *) |
|
180 oops |
151 |
181 |
152 |
182 |
153 lemma "PLUS a b = PLUS b a" |
183 lemma "PLUS a b = PLUS b a" |
154 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) |
184 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) |
155 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
185 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |