equal
deleted
inserted
replaced
160 |
160 |
161 lemma "PLUS a b = PLUS a b" |
161 lemma "PLUS a b = PLUS a b" |
162 apply(tactic {* procedure_tac @{context} @{thm test1} 1 *}) |
162 apply(tactic {* procedure_tac @{context} @{thm test1} 1 *}) |
163 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
163 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
164 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
164 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
165 apply(tactic {* simp_tac (HOL_basic_ss addSolver quotient_solver addsimps @{thms all_prs}) 1 *}) |
|
166 apply(tactic {* clean_tac @{context} 1 *}) |
165 apply(tactic {* clean_tac @{context} 1 *}) |
167 done |
166 done |
168 |
167 |
169 lemma test2: "my_plus a = my_plus a" |
168 lemma test2: "my_plus a = my_plus a" |
170 apply(rule refl) |
169 apply(rule refl) |
215 |
214 |
216 lemma ho_tst: "foldl my_plus x [] = x" |
215 lemma ho_tst: "foldl my_plus x [] = x" |
217 apply simp |
216 apply simp |
218 done |
217 done |
219 |
218 |
220 (* I believe it's true. *) |
|
221 lemma foldl_rsp[quotient_rsp]: |
|
222 "((op \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> list_rel op \<approx> ===> op \<approx>) foldl foldl" |
|
223 apply (simp only: fun_rel.simps) |
|
224 apply (rule allI) |
|
225 apply (rule allI) |
|
226 apply (rule impI) |
|
227 apply (rule allI) |
|
228 apply (rule allI) |
|
229 apply (rule impI) |
|
230 apply (rule allI) |
|
231 apply (rule allI) |
|
232 apply (rule impI) |
|
233 apply (induct_tac xb yb rule: list_induct2) (* To finish I need to give it: arbitrary:xa ya *) |
|
234 sorry |
|
235 |
|
236 lemma "foldl PLUS x [] = x" |
219 lemma "foldl PLUS x [] = x" |
237 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *}) |
220 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *}) |
238 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
221 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
239 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
222 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
240 apply(tactic {* clean_tac @{context} 1 *}) |
223 apply(tactic {* clean_tac @{context} 1 *}) |