149 lemma "PLUS a b = PLUS b a" |
149 lemma "PLUS a b = PLUS b a" |
150 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) |
150 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) |
151 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
151 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
152 prefer 2 |
152 prefer 2 |
153 apply(tactic {* clean_tac @{context} [quot] defs 1 *}) |
153 apply(tactic {* clean_tac @{context} [quot] defs 1 *}) |
154 apply(simp add: id_def) |
|
155 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
156 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
157 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
154 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
158 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
155 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
159 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
156 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
160 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
157 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
161 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
158 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
188 done |
185 done |
189 |
186 |
190 lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)" |
187 lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)" |
191 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) |
188 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) |
192 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
189 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
193 apply(simp) |
|
194 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
190 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
195 apply(tactic {* clean_tac @{context} [quot] defs 1 *}) |
191 apply(tactic {* clean_tac @{context} [quot] defs 1 *}) |
196 done |
192 done |
197 |
193 |
198 lemma ho_tst: "foldl my_plus x [] = x" |
194 lemma ho_tst: "foldl my_plus x [] = x" |
199 apply simp |
195 apply simp |
200 done |
196 done |
201 |
197 |
202 (* FIXME/TODO: is this a respectfulness theorem? Does not look like one. *) |
198 |
203 lemma map_prs: |
199 lemma foldr_prs: |
204 "map REP_my_int (map ABS_my_int x) = x" |
200 assumes a: "QUOTIENT R1 abs1 rep1" |
|
201 and b: "QUOTIENT R2 abs2 rep2" |
|
202 shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e" |
|
203 apply (induct l) |
|
204 apply (simp add: QUOTIENT_ABS_REP[OF b]) |
|
205 apply (simp add: QUOTIENT_ABS_REP[OF a] QUOTIENT_ABS_REP[OF b]) |
|
206 done |
|
207 |
|
208 lemma foldl_prs: |
|
209 assumes a: "QUOTIENT R1 abs1 rep1" |
|
210 and b: "QUOTIENT R2 abs2 rep2" |
|
211 shows "abs1 (foldl ((abs1 ---> abs2 ---> rep1) f) (rep1 e) (map rep2 l)) = foldl f e l" |
|
212 apply (induct l arbitrary:e) |
|
213 apply (simp add: QUOTIENT_ABS_REP[OF a]) |
|
214 apply (simp add: QUOTIENT_ABS_REP[OF a] QUOTIENT_ABS_REP[OF b]) |
|
215 done |
|
216 |
|
217 lemma map_prs: |
|
218 assumes a: "QUOTIENT R1 abs1 rep1" |
|
219 and b: "QUOTIENT R2 abs2 rep2" |
|
220 shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l" |
|
221 apply (induct l) |
|
222 apply (simp) |
|
223 apply (simp add: QUOTIENT_ABS_REP[OF a] QUOTIENT_ABS_REP[OF b]) |
|
224 done |
|
225 |
|
226 |
|
227 (* Removed unneeded assumption: "QUOTIENT R abs1 rep1" *) |
|
228 lemma nil_prs: |
|
229 shows "map abs1 [] = []" |
|
230 by simp |
|
231 |
|
232 lemma cons_prs: |
|
233 assumes a: "QUOTIENT R1 abs1 rep1" |
|
234 shows "(map abs1) ((rep1 h) # (map rep1 t)) = h # t" |
|
235 apply (induct t) |
|
236 by (simp_all add: QUOTIENT_ABS_REP[OF a]) |
|
237 |
|
238 lemma cons_rsp[quot_rsp]: |
|
239 "(op \<approx> ===> LIST_REL op \<approx> ===> LIST_REL op \<approx>) op # op #" |
|
240 by simp |
|
241 |
|
242 (* I believe it's true. *) |
|
243 lemma foldl_rsp[quot_rsp]: |
|
244 "((op \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> LIST_REL op \<approx> ===> op \<approx>) foldl foldl" |
|
245 apply (simp only: FUN_REL.simps) |
|
246 apply (rule allI) |
|
247 apply (rule allI) |
|
248 apply (rule impI) |
|
249 apply (rule allI) |
|
250 apply (rule allI) |
|
251 apply (rule impI) |
|
252 apply (rule allI) |
|
253 apply (rule allI) |
|
254 apply (rule impI) |
|
255 apply (induct_tac xb yb rule:list_induct2) (* To finish I need to give it: arbitrary:xa ya *) |
205 sorry |
256 sorry |
206 |
257 |
207 lemma foldl_prs[quot_rsp]: |
258 lemma nil_listrel_rsp[quot_rsp]: |
208 "((op \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> op = ===> op \<approx>) foldl foldl" |
259 "(LIST_REL R) [] []" |
209 sorry |
260 by simp |
210 |
261 |
211 lemma "foldl PLUS x [] = x" |
262 lemma "foldl PLUS x [] = x" |
212 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *}) |
263 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *}) |
213 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
264 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
214 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
265 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
215 apply(simp add: map_prs) |
266 apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int]) |
216 apply(simp only: map_prs) |
267 apply(simp only: nil_prs) |
217 apply(tactic {* clean_tac @{context} [quot] defs 1 *}) |
268 apply(tactic {* clean_tac @{context} [quot] defs 1 *}) |
|
269 done |
|
270 |
|
271 lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)" |
218 sorry |
272 sorry |
219 |
273 |
220 (* |
274 lemma "foldl PLUS x (h # t) = PLUS h (foldl PLUS x t)" |
221 FIXME: All below is your construction code; mostly commented out as it |
275 apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *}) |
222 does not work. |
276 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
223 *) |
277 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
224 |
278 apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int]) |
225 lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)" |
279 apply(simp only: cons_prs[OF QUOTIENT_my_int]) |
226 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) |
280 apply(tactic {* clean_tac @{context} [quot] defs 1 *}) |
227 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
281 done |
228 apply(simp) |
282 |
229 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
|
230 apply(tactic {* clean_tac @{context} [quot] defs 1 *}) |
|
231 done |
|
232 |
|
233 |
|