7 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50) |
7 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50) |
8 where |
8 where |
9 "intrel (x, y) (u, v) = (x + v = u + y)" |
9 "intrel (x, y) (u, v) = (x + v = u + y)" |
10 |
10 |
11 quotient my_int = "nat \<times> nat" / intrel |
11 quotient my_int = "nat \<times> nat" / intrel |
12 apply(unfold EQUIV_def) |
12 apply(unfold equivp_def) |
13 apply(auto simp add: mem_def expand_fun_eq) |
13 apply(auto simp add: mem_def expand_fun_eq) |
14 done |
14 done |
15 |
15 |
16 thm quotient_thm |
16 thm quotient_thm |
17 |
17 |
18 thm my_int_equiv |
18 thm my_int_equivp |
19 |
19 |
20 print_theorems |
20 print_theorems |
21 print_quotients |
21 print_quotients |
22 |
22 |
23 quotient_def |
23 quotient_def |
196 apply simp |
196 apply simp |
197 done |
197 done |
198 |
198 |
199 |
199 |
200 lemma foldr_prs: |
200 lemma foldr_prs: |
201 assumes a: "QUOTIENT R1 abs1 rep1" |
201 assumes a: "Quotient R1 abs1 rep1" |
202 and b: "QUOTIENT R2 abs2 rep2" |
202 and b: "Quotient R2 abs2 rep2" |
203 shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e" |
203 shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e" |
204 apply (induct l) |
204 apply (induct l) |
205 apply (simp add: QUOTIENT_ABS_REP[OF b]) |
205 apply (simp add: Quotient_ABS_REP[OF b]) |
206 apply (simp add: QUOTIENT_ABS_REP[OF a] QUOTIENT_ABS_REP[OF b]) |
206 apply (simp add: Quotient_ABS_REP[OF a] Quotient_ABS_REP[OF b]) |
207 done |
207 done |
208 |
208 |
209 lemma foldl_prs: |
209 lemma foldl_prs: |
210 assumes a: "QUOTIENT R1 abs1 rep1" |
210 assumes a: "Quotient R1 abs1 rep1" |
211 and b: "QUOTIENT R2 abs2 rep2" |
211 and b: "Quotient R2 abs2 rep2" |
212 shows "abs1 (foldl ((abs1 ---> abs2 ---> rep1) f) (rep1 e) (map rep2 l)) = foldl f e l" |
212 shows "abs1 (foldl ((abs1 ---> abs2 ---> rep1) f) (rep1 e) (map rep2 l)) = foldl f e l" |
213 apply (induct l arbitrary:e) |
213 apply (induct l arbitrary:e) |
214 apply (simp add: QUOTIENT_ABS_REP[OF a]) |
214 apply (simp add: Quotient_ABS_REP[OF a]) |
215 apply (simp add: QUOTIENT_ABS_REP[OF a] QUOTIENT_ABS_REP[OF b]) |
215 apply (simp add: Quotient_ABS_REP[OF a] Quotient_ABS_REP[OF b]) |
216 done |
216 done |
217 |
217 |
218 lemma map_prs: |
218 lemma map_prs: |
219 assumes a: "QUOTIENT R1 abs1 rep1" |
219 assumes a: "Quotient R1 abs1 rep1" |
220 and b: "QUOTIENT R2 abs2 rep2" |
220 and b: "Quotient R2 abs2 rep2" |
221 shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l" |
221 shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l" |
222 apply (induct l) |
222 apply (induct l) |
223 apply (simp) |
223 apply (simp) |
224 apply (simp add: QUOTIENT_ABS_REP[OF a] QUOTIENT_ABS_REP[OF b]) |
224 apply (simp add: Quotient_ABS_REP[OF a] Quotient_ABS_REP[OF b]) |
225 done |
225 done |
226 |
226 |
227 |
227 |
228 (* Removed unneeded assumption: "QUOTIENT R abs1 rep1" *) |
228 (* Removed unneeded assumption: "QUOTIENT R abs1 rep1" *) |
229 lemma nil_prs: |
229 lemma nil_prs: |
230 shows "map abs1 [] = []" |
230 shows "map abs1 [] = []" |
231 by simp |
231 by simp |
232 |
232 |
233 lemma cons_prs: |
233 lemma cons_prs: |
234 assumes a: "QUOTIENT R1 abs1 rep1" |
234 assumes a: "Quotient R1 abs1 rep1" |
235 shows "(map abs1) ((rep1 h) # (map rep1 t)) = h # t" |
235 shows "(map abs1) ((rep1 h) # (map rep1 t)) = h # t" |
236 apply (induct t) |
236 apply (induct t) |
237 by (simp_all add: QUOTIENT_ABS_REP[OF a]) |
237 by (simp_all add: Quotient_ABS_REP[OF a]) |
238 |
238 |
239 lemma cons_rsp[quotient_rsp]: |
239 lemma cons_rsp[quotient_rsp]: |
240 "(op \<approx> ===> LIST_REL op \<approx> ===> LIST_REL op \<approx>) op # op #" |
240 "(op \<approx> ===> LIST_REL op \<approx> ===> LIST_REL op \<approx>) op # op #" |
241 by simp |
241 by simp |
242 |
242 |
262 |
262 |
263 lemma "foldl PLUS x [] = x" |
263 lemma "foldl PLUS x [] = x" |
264 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *}) |
264 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *}) |
265 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
265 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
266 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
266 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
267 apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int]) |
267 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int]) |
268 apply(simp only: nil_prs) |
268 apply(simp only: nil_prs) |
269 apply(tactic {* clean_tac @{context} 1 *}) |
269 apply(tactic {* clean_tac @{context} 1 *}) |
270 done |
270 done |
271 |
271 |
272 lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)" |
272 lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)" |
274 |
274 |
275 lemma "foldl PLUS x (h # t) = PLUS h (foldl PLUS x t)" |
275 lemma "foldl PLUS x (h # t) = PLUS h (foldl PLUS x t)" |
276 apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *}) |
276 apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *}) |
277 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
277 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
278 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
278 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
279 apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int]) |
279 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int]) |
280 apply(simp only: cons_prs[OF QUOTIENT_my_int]) |
280 apply(simp only: cons_prs[OF Quotient_my_int]) |
281 apply(tactic {* clean_tac @{context} 1 *}) |
281 apply(tactic {* clean_tac @{context} 1 *}) |
282 done |
282 done |
283 |
283 |