128 apply(cases a) |
128 apply(cases a) |
129 apply(cases b) |
129 apply(cases b) |
130 apply(auto) |
130 apply(auto) |
131 done |
131 done |
132 |
132 |
133 lemma list_equiv_rsp[quotient_rsp]: |
133 lemma plus_rsp[quotient_rsp]: |
134 shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>" |
|
135 by auto |
|
136 |
|
137 lemma ho_plus_rsp[quotient_rsp]: |
|
138 shows "(intrel ===> intrel ===> intrel) my_plus my_plus" |
134 shows "(intrel ===> intrel ===> intrel) my_plus my_plus" |
139 by (simp) |
135 by (simp) |
140 |
136 |
141 ML {* val qty = @{typ "my_int"} *} |
137 ML {* val qty = @{typ "my_int"} *} |
142 ML {* val ty_name = "my_int" *} |
|
143 ML {* val rsp_thms = @{thms ho_plus_rsp} *} |
|
144 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
138 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
145 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *} |
139 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *} |
146 |
140 |
147 ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] *} |
141 ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] *} |
148 |
142 |
172 done |
166 done |
173 |
167 |
174 lemma "PLUS a = PLUS a" |
168 lemma "PLUS a = PLUS a" |
175 apply(tactic {* procedure_tac @{context} @{thm test2} 1 *}) |
169 apply(tactic {* procedure_tac @{context} @{thm test2} 1 *}) |
176 apply(rule ballI) |
170 apply(rule ballI) |
177 apply(rule apply_rsp[OF Quotient_my_int ho_plus_rsp]) |
171 apply(rule apply_rsp[OF Quotient_my_int plus_rsp]) |
178 apply(simp only: in_respects) |
172 apply(simp only: in_respects) |
179 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
173 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
180 apply(tactic {* clean_tac @{context} 1 *}) |
174 apply(tactic {* clean_tac @{context} 1 *}) |
181 done |
175 done |
182 |
176 |
236 |
230 |
237 lemma "foldl PLUS x [] = x" |
231 lemma "foldl PLUS x [] = x" |
238 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *}) |
232 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *}) |
239 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
233 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
240 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
234 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
241 apply(rule nil_rsp) |
235 apply(tactic {* clean_tac @{context} 1 *}) |
242 apply(tactic {* quotient_tac @{context} 1*}) |
236 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int]) |
243 apply(simp only: fun_map.simps id_simps) |
|
244 apply(simp only: Quotient_abs_rep[OF fun_quotient[OF Quotient_my_int fun_quotient[OF Quotient_my_int Quotient_my_int]]]) |
|
245 apply(simp only: Quotient_abs_rep[OF list_quotient[OF Quotient_my_int]]) |
|
246 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int]) |
|
247 apply(tactic {* clean_tac @{context} 1 *}) |
|
248 apply(simp) (* FIXME: why is this needed *) |
|
249 done |
237 done |
250 |
238 |
251 lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)" |
239 lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)" |
252 sorry |
240 sorry |
253 |
241 |
254 lemma "foldl PLUS x (h # t) = PLUS h (foldl PLUS x t)" |
242 lemma "foldl PLUS x (h # t) = PLUS h (foldl PLUS x t)" |
255 apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *}) |
243 apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *}) |
256 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
244 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
257 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
245 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
258 apply(rule cons_rsp) |
246 apply(tactic {* clean_tac @{context} 1 *}) |
259 apply(tactic {* quotient_tac @{context} 1 *}) |
247 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] cons_prs[OF Quotient_my_int]) |
260 apply(simp only: fun_map.simps id_simps) |
248 done |
261 apply(simp only: Quotient_abs_rep[OF fun_quotient[OF Quotient_my_int fun_quotient[OF Quotient_my_int Quotient_my_int]]]) |
249 |
262 apply(simp only: Quotient_abs_rep[OF list_quotient[OF Quotient_my_int]]) |
|
263 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int]) |
|
264 apply(simp only: cons_prs[OF Quotient_my_int]) |
|
265 apply(tactic {* clean_tac @{context} 1 *}) |
|
266 done |
|
267 |
|