equal
deleted
inserted
replaced
140 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *} |
140 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *} |
141 ML {* val consts = lookup_quot_consts defs *} |
141 ML {* val consts = lookup_quot_consts defs *} |
142 |
142 |
143 ML {* |
143 ML {* |
144 fun lift_tac_fset lthy t = |
144 fun lift_tac_fset lthy t = |
145 lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs |
145 lift_tac lthy t [rel_eqv] rty [quot] trans2 rsp_thms defs |
146 *} |
146 *} |
147 |
147 |
148 lemma "PLUS a b = PLUS b a" |
148 lemma "PLUS a b = PLUS b a" |
149 by (tactic {* lift_tac_fset @{context} @{thm plus_sym_pre} 1 *}) |
149 by (tactic {* lift_tac_fset @{context} @{thm plus_sym_pre} 1 *}) |
150 |
150 |
165 done |
165 done |
166 |
166 |
167 lemma map_prs: "map REP_my_int (map ABS_my_int x) = x" |
167 lemma map_prs: "map REP_my_int (map ABS_my_int x) = x" |
168 sorry |
168 sorry |
169 |
169 |
|
170 lemma foldl_prs: "((op \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> op = ===> op \<approx>) foldl foldl" |
|
171 sorry |
|
172 |
170 lemma "foldl PLUS x [] = x" |
173 lemma "foldl PLUS x [] = x" |
171 apply (tactic {* lift_tac_fset @{context} @{thm ho_tst} 1 *}) |
174 apply (tactic {* lift_tac_fset @{context} @{thm ho_tst} 1 *}) |
172 apply (simp_all only: map_prs) |
175 apply (simp_all only: map_prs foldl_prs) |
173 sorry |
176 sorry |
174 |
177 |
175 (* |
178 (* |
176 FIXME: All below is your construction code; mostly commented out as it |
179 FIXME: All below is your construction code; mostly commented out as it |
177 does not work. |
180 does not work. |
185 |> writeln |
188 |> writeln |
186 *} |
189 *} |
187 |
190 |
188 lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)" |
191 lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)" |
189 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) |
192 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) |
190 apply(tactic {* regularize_tac @{context} [rel_eqv] rel_refl 1 *}) |
193 apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *}) |
191 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *}) |
194 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty [quot] [rel_refl] trans2 rsp_thms) 1 *}) |
192 oops |
195 oops |
193 |
196 |
194 |
197 |
195 (* |
198 (* |
196 |
199 |