equal
deleted
inserted
replaced
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) |
141 done |
141 done |
142 |
142 |
143 lemma "PLUS a b = PLUS a b" |
143 lemma "PLUS a b = PLUS a b" |
144 apply(lifting_setup rule: test1) |
144 apply(lifting_setup test1) |
145 apply(regularize) |
145 apply(regularize) |
146 apply(injection) |
146 apply(injection) |
147 apply(cleaning) |
147 apply(cleaning) |
148 done |
148 done |
149 |
149 |
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(lifting rule: ho_tst) |
206 apply(lifting ho_tst) |
207 apply(tactic {* clean_tac @{context} 1 *}) |
207 apply(tactic {* clean_tac @{context} 1 *}) |
208 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]) |
209 done |
209 done |
210 |
210 |
211 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)" |
341 apply (case_tac a) |
341 apply (case_tac a) |
342 apply simp |
342 apply simp |
343 done |
343 done |
344 |
344 |
345 lemma "map (\<lambda>x. PLUS x ZERO) l = l" |
345 lemma "map (\<lambda>x. PLUS x ZERO) l = l" |
346 apply(lifting rule: lam_tst4) |
346 apply(lifting lam_tst4) |
347 apply(cleaning) |
347 apply(cleaning) |
348 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]) |
349 apply(simp only: map_prs[OF Quotient_my_int Quotient_my_int, symmetric]) |
349 apply(simp only: map_prs[OF Quotient_my_int Quotient_my_int, symmetric]) |
350 done |
350 done |
351 |
351 |