146 ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy [rel_refl] [trans2] *} |
146 ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy [rel_refl] [trans2] *} |
147 |
147 |
148 lemma test1: "my_plus a b = my_plus a b" |
148 lemma test1: "my_plus a b = my_plus a b" |
149 apply(rule refl) |
149 apply(rule refl) |
150 done |
150 done |
151 |
|
152 |
|
153 (* |
|
154 lemma yy: |
|
155 "(REP_my_int ---> id) |
|
156 (\<lambda>x. Ball (Respects op \<approx>) |
|
157 ((ABS_my_int ---> id) |
|
158 ((REP_my_int ---> id) |
|
159 (\<lambda>b. (ABS_my_int ---> ABS_my_int ---> REP_my_int) |
|
160 ((REP_my_int ---> REP_my_int ---> ABS_my_int) my_plus) |
|
161 (REP_my_int (ABS_my_int x)) (REP_my_int (ABS_my_int b)) \<approx> |
|
162 (ABS_my_int ---> ABS_my_int ---> REP_my_int) |
|
163 ((REP_my_int ---> REP_my_int ---> ABS_my_int) my_plus) |
|
164 (REP_my_int (ABS_my_int x)) (REP_my_int (ABS_my_int b)))))) = |
|
165 (\<lambda>x. Ball (Respects op \<approx>) |
|
166 ((ABS_my_int ---> id) |
|
167 ((REP_my_int ---> id) |
|
168 (\<lambda>b. (ABS_my_int ---> ABS_my_int ---> REP_my_int) |
|
169 ((REP_my_int ---> REP_my_int ---> ABS_my_int) my_plus) (REP_my_int x) |
|
170 (REP_my_int (ABS_my_int b)) \<approx> |
|
171 (ABS_my_int ---> ABS_my_int ---> REP_my_int) |
|
172 ((REP_my_int ---> REP_my_int ---> ABS_my_int) my_plus) (REP_my_int x) |
|
173 (REP_my_int (ABS_my_int b))))))" |
|
174 apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [lambda_prs2 @{theory}]) 1*}) |
|
175 |
|
176 apply(rule lambda_prs) |
|
177 apply(tactic {* quotient_tac @{context} 1 *}) |
|
178 apply(simp add: id_simps) |
|
179 apply(tactic {* quotient_tac @{context} 1 *}) |
|
180 done |
|
181 *) |
|
182 |
151 |
183 lemma "PLUS a b = PLUS a b" |
152 lemma "PLUS a b = PLUS a b" |
184 apply(tactic {* procedure_tac @{context} @{thm test1} 1 *}) |
153 apply(tactic {* procedure_tac @{context} @{thm test1} 1 *}) |
185 apply(tactic {* regularize_tac @{context} 1 *}) |
154 apply(tactic {* regularize_tac @{context} 1 *}) |
186 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
155 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |