equal
deleted
inserted
replaced
162 |
162 |
163 lemma ho_tst: "foldl my_plus x [] = x" |
163 lemma ho_tst: "foldl my_plus x [] = x" |
164 apply simp |
164 apply simp |
165 done |
165 done |
166 |
166 |
|
167 lemma map_prs: "map REP_my_int (map ABS_my_int x) = x" |
|
168 sorry |
|
169 |
167 lemma "foldl PLUS x [] = x" |
170 lemma "foldl PLUS x [] = x" |
168 apply (tactic {* lift_tac_fset @{context} @{thm ho_tst} 1 *}) |
171 apply (tactic {* lift_tac_fset @{context} @{thm ho_tst} 1 *}) |
|
172 apply (simp_all only: map_prs) |
169 sorry |
173 sorry |
170 |
174 |
171 (* |
175 (* |
172 FIXME: All below is your construction code; mostly commented out as it |
176 FIXME: All below is your construction code; mostly commented out as it |
173 does not work. |
177 does not work. |