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