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