equal
deleted
inserted
replaced
10 quotient my_int = "nat \<times> nat" / intrel |
10 quotient my_int = "nat \<times> nat" / intrel |
11 apply(unfold equivp_def) |
11 apply(unfold equivp_def) |
12 apply(auto simp add: mem_def expand_fun_eq) |
12 apply(auto simp add: mem_def expand_fun_eq) |
13 done |
13 done |
14 |
14 |
15 thm quotient_equiv |
15 thm quot_equiv |
16 |
16 |
17 thm quotient_thm |
17 thm quot_thm |
18 |
18 |
19 thm my_int_equivp |
19 thm my_int_equivp |
20 |
20 |
21 print_theorems |
21 print_theorems |
22 print_quotients |
22 print_quotients |
130 apply(cases a) |
130 apply(cases a) |
131 apply(cases b) |
131 apply(cases b) |
132 apply(auto) |
132 apply(auto) |
133 done |
133 done |
134 |
134 |
135 lemma plus_rsp[quotient_rsp]: |
135 lemma plus_rsp[quot_respect]: |
136 shows "(intrel ===> intrel ===> intrel) my_plus my_plus" |
136 shows "(intrel ===> intrel ===> intrel) my_plus my_plus" |
137 by (simp) |
137 by (simp) |
138 |
138 |
139 lemma test1: "my_plus a b = my_plus a b" |
139 lemma test1: "my_plus a b = my_plus a b" |
140 apply(rule refl) |
140 apply(rule refl) |
169 |
169 |
170 lemma "PLUS = PLUS" |
170 lemma "PLUS = PLUS" |
171 apply(tactic {* procedure_tac @{context} @{thm test3} 1 *}) |
171 apply(tactic {* procedure_tac @{context} @{thm test3} 1 *}) |
172 apply(rule impI) |
172 apply(rule impI) |
173 apply(rule plus_rsp) |
173 apply(rule plus_rsp) |
174 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |
174 apply(injection) |
175 apply(tactic {* clean_tac @{context} 1 *}) |
175 apply(cleaning) |
176 done |
176 done |
177 |
177 |
178 |
178 |
179 lemma "PLUS a b = PLUS b a" |
179 lemma "PLUS a b = PLUS b a" |
180 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) |
180 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) |
201 lemma ho_tst: "foldl my_plus x [] = x" |
201 lemma ho_tst: "foldl my_plus x [] = x" |
202 apply simp |
202 apply simp |
203 done |
203 done |
204 |
204 |
205 lemma "foldl PLUS x [] = x" |
205 lemma "foldl PLUS x [] = x" |
206 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *}) |
206 apply(lifting rule: ho_tst) |
207 apply(tactic {* regularize_tac @{context} 1 *}) |
|
208 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |
|
209 apply(tactic {* clean_tac @{context} 1 *}) |
207 apply(tactic {* clean_tac @{context} 1 *}) |
210 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int]) |
208 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int]) |
211 done |
209 done |
212 |
210 |
213 lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)" |
211 lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)" |
343 apply (case_tac a) |
341 apply (case_tac a) |
344 apply simp |
342 apply simp |
345 done |
343 done |
346 |
344 |
347 lemma "map (\<lambda>x. PLUS x ZERO) l = l" |
345 lemma "map (\<lambda>x. PLUS x ZERO) l = l" |
348 apply(tactic {* procedure_tac @{context} @{thm lam_tst4} 1 *}) |
346 apply(lifting rule: lam_tst4) |
349 apply(tactic {* regularize_tac @{context} 1 *}) |
347 apply(cleaning) |
350 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |
|
351 apply(tactic {* clean_tac @{context} 1*}) |
|
352 apply(simp only: babs_prs[OF Quotient_my_int Quotient_my_int]) |
348 apply(simp only: babs_prs[OF Quotient_my_int Quotient_my_int]) |
353 apply(simp only: map_prs[OF Quotient_my_int Quotient_my_int]) |
349 apply(simp only: map_prs[OF Quotient_my_int Quotient_my_int, symmetric]) |
354 apply(tactic {* lambda_prs_tac @{context} 1 *}) |
|
355 apply(rule refl) |
|
356 done |
350 done |
357 |
351 |
358 end |
352 end |