133 lemma test2: "my_plus a = my_plus a" |
133 lemma test2: "my_plus a = my_plus a" |
134 apply(rule refl) |
134 apply(rule refl) |
135 done |
135 done |
136 |
136 |
137 lemma "PLUS a = PLUS a" |
137 lemma "PLUS a = PLUS a" |
138 apply(tactic {* procedure_tac @{context} @{thm test2} 1 *}) |
138 apply(lifting_setup test2) |
139 apply(rule impI) |
139 apply(rule impI) |
140 apply(rule ballI) |
140 apply(rule ballI) |
141 apply(rule apply_rsp[OF Quotient_my_int plus_rsp]) |
141 apply(rule apply_rsp[OF Quotient_my_int plus_rsp]) |
142 apply(simp only: in_respects) |
142 apply(simp only: in_respects) |
143 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |
143 apply(injection) |
144 apply(tactic {* clean_tac @{context} 1 *}) |
144 apply(cleaning) |
145 done |
145 done |
146 |
146 |
147 lemma test3: "my_plus = my_plus" |
147 lemma test3: "my_plus = my_plus" |
148 apply(rule refl) |
148 apply(rule refl) |
149 done |
149 done |
150 |
150 |
151 lemma "PLUS = PLUS" |
151 lemma "PLUS = PLUS" |
152 apply(tactic {* procedure_tac @{context} @{thm test3} 1 *}) |
152 apply(lifting_setup test3) |
153 apply(rule impI) |
153 apply(rule impI) |
154 apply(rule plus_rsp) |
154 apply(rule plus_rsp) |
155 apply(injection) |
155 apply(injection) |
156 apply(cleaning) |
156 apply(cleaning) |
157 done |
157 done |
158 |
158 |
159 |
159 |
160 lemma "PLUS a b = PLUS b a" |
160 lemma "PLUS a b = PLUS b a" |
161 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) |
161 apply(lifting plus_sym_pre) |
162 apply(tactic {* regularize_tac @{context} 1 *}) |
|
163 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |
|
164 apply(tactic {* clean_tac @{context} 1 *}) |
|
165 done |
162 done |
166 |
163 |
167 lemma plus_assoc_pre: |
164 lemma plus_assoc_pre: |
168 shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)" |
165 shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)" |
169 apply (cases i) |
166 apply (cases i) |
171 apply (cases k) |
168 apply (cases k) |
172 apply (simp) |
169 apply (simp) |
173 done |
170 done |
174 |
171 |
175 lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)" |
172 lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)" |
176 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) |
173 apply(lifting plus_assoc_pre) |
177 apply(tactic {* regularize_tac @{context} 1 *}) |
|
178 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |
|
179 apply(tactic {* clean_tac @{context} 1 *}) |
|
180 done |
174 done |
181 |
175 |
182 lemma int_induct_raw: |
176 lemma int_induct_raw: |
183 assumes a: "P (0::nat, 0)" |
177 assumes a: "P (0::nat, 0)" |
184 and b: "\<And>i. P i \<Longrightarrow> P (my_plus i (1,0))" |
178 and b: "\<And>i. P i \<Longrightarrow> P (my_plus i (1,0))" |
233 apply(lifting lam_tst) |
224 apply(lifting lam_tst) |
234 done |
225 done |
235 |
226 |
236 lemma lam_tst2: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)" |
227 lemma lam_tst2: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)" |
237 by simp |
228 by simp |
238 |
|
239 (* test about lifting identity equations *) |
|
240 |
|
241 ML {* |
|
242 (* helper code from QuotMain *) |
|
243 val pat_ball = @{term "Ball (Respects (R1 ===> R2)) P"} |
|
244 val pat_bex = @{term "Bex (Respects (R1 ===> R2)) P"} |
|
245 val simproc = Simplifier.simproc_i @{theory} "" [pat_ball, pat_bex] (K (ball_bex_range_simproc)) |
|
246 val simpset = (mk_minimal_ss @{context}) |
|
247 addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv} |
|
248 addsimprocs [simproc] addSolver equiv_solver |
|
249 *} |
|
250 |
|
251 (* What regularising does *) |
|
252 (*========================*) |
|
253 |
|
254 (* 0. preliminary simplification step *) |
|
255 thm ball_reg_eqv bex_reg_eqv (* of no use: babs_reg_eqv *) |
|
256 ball_reg_eqv_range bex_reg_eqv_range |
|
257 (* 1. first two rtacs *) |
|
258 thm ball_reg_right bex_reg_left |
|
259 (* 2. monos *) |
|
260 (* 3. commutation rules *) |
|
261 thm ball_all_comm bex_ex_comm |
|
262 (* 4. then rel-equality *) |
|
263 thm eq_imp_rel |
|
264 (* 5. then simplification like 0 *) |
|
265 (* finally jump to 1 *) |
|
266 |
|
267 |
|
268 (* What cleaning does *) |
|
269 (*====================*) |
|
270 |
|
271 (* 1. conversion *) |
|
272 thm lambda_prs |
|
273 (* 2. simplification with *) |
|
274 thm all_prs ex_prs |
|
275 (* 3. Simplification with *) |
|
276 thm fun_map.simps id_simps Quotient_abs_rep Quotient_rel_rep |
|
277 (* 4. Test for refl *) |
|
278 |
229 |
279 lemma |
230 lemma |
280 shows "equivp (op \<approx>)" |
231 shows "equivp (op \<approx>)" |
281 and "equivp ((op \<approx>) ===> (op \<approx>))" |
232 and "equivp ((op \<approx>) ===> (op \<approx>))" |
282 (* Nitpick finds a counterexample! *) |
233 (* Nitpick finds a counterexample! *) |
293 apply (rule babs_rsp[OF Quotient_my_int]) |
244 apply (rule babs_rsp[OF Quotient_my_int]) |
294 apply (simp add: id_rsp) |
245 apply (simp add: id_rsp) |
295 done |
246 done |
296 |
247 |
297 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)" |
248 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)" |
298 apply(tactic {* procedure_tac @{context} @{thm lam_tst3a} 1 *}) |
249 apply(lifting lam_tst3a) |
299 apply(rule impI) |
250 apply(rule impI) |
300 apply(rule lam_tst3a_reg) |
251 apply(rule lam_tst3a_reg) |
301 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |
|
302 apply(tactic {* clean_tac @{context} 1 *}) |
|
303 done |
252 done |
304 |
253 |
305 lemma lam_tst3b: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)" |
254 lemma lam_tst3b: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)" |
306 by auto |
255 by auto |
307 |
256 |